1(* Title: ZF/Bin.thy 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 1994 University of Cambridge 4 5 The sign Pls stands for an infinite string of leading 0's. 6 The sign Min stands for an infinite string of leading 1's. 7 8A number can have multiple representations, namely leading 0's with sign 9Pls and leading 1's with sign Min. See twos-compl.ML/int_of_binary for 10the numerical interpretation. 11 12The representation expects that (m mod 2) is 0 or 1, even if m is negative; 13For instance, ~5 div 2 = ~3 and ~5 mod 2 = 1; thus ~5 = (~3)*2 + 1 14*) 15 16section\<open>Arithmetic on Binary Integers\<close> 17 18theory Bin 19imports Int Datatype 20begin 21 22consts bin :: i 23datatype 24 "bin" = Pls 25 | Min 26 | Bit ("w \<in> bin", "b \<in> bool") (infixl \<open>BIT\<close> 90) 27 28consts 29 integ_of :: "i=>i" 30 NCons :: "[i,i]=>i" 31 bin_succ :: "i=>i" 32 bin_pred :: "i=>i" 33 bin_minus :: "i=>i" 34 bin_adder :: "i=>i" 35 bin_mult :: "[i,i]=>i" 36 37primrec 38 integ_of_Pls: "integ_of (Pls) = $# 0" 39 integ_of_Min: "integ_of (Min) = $-($#1)" 40 integ_of_BIT: "integ_of (w BIT b) = $#b $+ integ_of(w) $+ integ_of(w)" 41 42 (** recall that cond(1,b,c)=b and cond(0,b,c)=0 **) 43 44primrec (*NCons adds a bit, suppressing leading 0s and 1s*) 45 NCons_Pls: "NCons (Pls,b) = cond(b,Pls BIT b,Pls)" 46 NCons_Min: "NCons (Min,b) = cond(b,Min,Min BIT b)" 47 NCons_BIT: "NCons (w BIT c,b) = w BIT c BIT b" 48 49primrec (*successor. If a BIT, can change a 0 to a 1 without recursion.*) 50 bin_succ_Pls: "bin_succ (Pls) = Pls BIT 1" 51 bin_succ_Min: "bin_succ (Min) = Pls" 52 bin_succ_BIT: "bin_succ (w BIT b) = cond(b, bin_succ(w) BIT 0, NCons(w,1))" 53 54primrec (*predecessor*) 55 bin_pred_Pls: "bin_pred (Pls) = Min" 56 bin_pred_Min: "bin_pred (Min) = Min BIT 0" 57 bin_pred_BIT: "bin_pred (w BIT b) = cond(b, NCons(w,0), bin_pred(w) BIT 1)" 58 59primrec (*unary negation*) 60 bin_minus_Pls: 61 "bin_minus (Pls) = Pls" 62 bin_minus_Min: 63 "bin_minus (Min) = Pls BIT 1" 64 bin_minus_BIT: 65 "bin_minus (w BIT b) = cond(b, bin_pred(NCons(bin_minus(w),0)), 66 bin_minus(w) BIT 0)" 67 68primrec (*sum*) 69 bin_adder_Pls: 70 "bin_adder (Pls) = (\<lambda>w\<in>bin. w)" 71 bin_adder_Min: 72 "bin_adder (Min) = (\<lambda>w\<in>bin. bin_pred(w))" 73 bin_adder_BIT: 74 "bin_adder (v BIT x) = 75 (\<lambda>w\<in>bin. 76 bin_case (v BIT x, bin_pred(v BIT x), 77 %w y. NCons(bin_adder (v) ` cond(x and y, bin_succ(w), w), 78 x xor y), 79 w))" 80 81(*The bin_case above replaces the following mutually recursive function: 82primrec 83 "adding (v,x,Pls) = v BIT x" 84 "adding (v,x,Min) = bin_pred(v BIT x)" 85 "adding (v,x,w BIT y) = NCons(bin_adder (v, cond(x and y, bin_succ(w), w)), 86 x xor y)" 87*) 88 89definition 90 bin_add :: "[i,i]=>i" where 91 "bin_add(v,w) == bin_adder(v)`w" 92 93 94primrec 95 bin_mult_Pls: 96 "bin_mult (Pls,w) = Pls" 97 bin_mult_Min: 98 "bin_mult (Min,w) = bin_minus(w)" 99 bin_mult_BIT: 100 "bin_mult (v BIT b,w) = cond(b, bin_add(NCons(bin_mult(v,w),0),w), 101 NCons(bin_mult(v,w),0))" 102 103syntax 104 "_Int0" :: i (\<open>#' 0\<close>) 105 "_Int1" :: i (\<open>#' 1\<close>) 106 "_Int2" :: i (\<open>#' 2\<close>) 107 "_Neg_Int1" :: i (\<open>#-' 1\<close>) 108 "_Neg_Int2" :: i (\<open>#-' 2\<close>) 109translations 110 "#0" \<rightleftharpoons> "CONST integ_of(CONST Pls)" 111 "#1" \<rightleftharpoons> "CONST integ_of(CONST Pls BIT 1)" 112 "#2" \<rightleftharpoons> "CONST integ_of(CONST Pls BIT 1 BIT 0)" 113 "#-1" \<rightleftharpoons> "CONST integ_of(CONST Min)" 114 "#-2" \<rightleftharpoons> "CONST integ_of(CONST Min BIT 0)" 115 116syntax 117 "_Int" :: "num_token => i" (\<open>#_\<close> 1000) 118 "_Neg_Int" :: "num_token => i" (\<open>#-_\<close> 1000) 119 120ML_file \<open>Tools/numeral_syntax.ML\<close> 121 122 123declare bin.intros [simp,TC] 124 125lemma NCons_Pls_0: "NCons(Pls,0) = Pls" 126by simp 127 128lemma NCons_Pls_1: "NCons(Pls,1) = Pls BIT 1" 129by simp 130 131lemma NCons_Min_0: "NCons(Min,0) = Min BIT 0" 132by simp 133 134lemma NCons_Min_1: "NCons(Min,1) = Min" 135by simp 136 137lemma NCons_BIT: "NCons(w BIT x,b) = w BIT x BIT b" 138by (simp add: bin.case_eqns) 139 140lemmas NCons_simps [simp] = 141 NCons_Pls_0 NCons_Pls_1 NCons_Min_0 NCons_Min_1 NCons_BIT 142 143 144 145(** Type checking **) 146 147lemma integ_of_type [TC]: "w \<in> bin ==> integ_of(w) \<in> int" 148apply (induct_tac "w") 149apply (simp_all add: bool_into_nat) 150done 151 152lemma NCons_type [TC]: "[| w \<in> bin; b \<in> bool |] ==> NCons(w,b) \<in> bin" 153by (induct_tac "w", auto) 154 155lemma bin_succ_type [TC]: "w \<in> bin ==> bin_succ(w) \<in> bin" 156by (induct_tac "w", auto) 157 158lemma bin_pred_type [TC]: "w \<in> bin ==> bin_pred(w) \<in> bin" 159by (induct_tac "w", auto) 160 161lemma bin_minus_type [TC]: "w \<in> bin ==> bin_minus(w) \<in> bin" 162by (induct_tac "w", auto) 163 164(*This proof is complicated by the mutual recursion*) 165lemma bin_add_type [rule_format]: 166 "v \<in> bin ==> \<forall>w\<in>bin. bin_add(v,w) \<in> bin" 167apply (unfold bin_add_def) 168apply (induct_tac "v") 169apply (rule_tac [3] ballI) 170apply (rename_tac [3] "w'") 171apply (induct_tac [3] "w'") 172apply (simp_all add: NCons_type) 173done 174 175declare bin_add_type [TC] 176 177lemma bin_mult_type [TC]: "[| v \<in> bin; w \<in> bin |] ==> bin_mult(v,w) \<in> bin" 178by (induct_tac "v", auto) 179 180 181subsubsection\<open>The Carry and Borrow Functions, 182 \<^term>\<open>bin_succ\<close> and \<^term>\<open>bin_pred\<close>\<close> 183 184(*NCons preserves the integer value of its argument*) 185lemma integ_of_NCons [simp]: 186 "[| w \<in> bin; b \<in> bool |] ==> integ_of(NCons(w,b)) = integ_of(w BIT b)" 187apply (erule bin.cases) 188apply (auto elim!: boolE) 189done 190 191lemma integ_of_succ [simp]: 192 "w \<in> bin ==> integ_of(bin_succ(w)) = $#1 $+ integ_of(w)" 193apply (erule bin.induct) 194apply (auto simp add: zadd_ac elim!: boolE) 195done 196 197lemma integ_of_pred [simp]: 198 "w \<in> bin ==> integ_of(bin_pred(w)) = $- ($#1) $+ integ_of(w)" 199apply (erule bin.induct) 200apply (auto simp add: zadd_ac elim!: boolE) 201done 202 203 204subsubsection\<open>\<^term>\<open>bin_minus\<close>: Unary Negation of Binary Integers\<close> 205 206lemma integ_of_minus: "w \<in> bin ==> integ_of(bin_minus(w)) = $- integ_of(w)" 207apply (erule bin.induct) 208apply (auto simp add: zadd_ac zminus_zadd_distrib elim!: boolE) 209done 210 211 212subsubsection\<open>\<^term>\<open>bin_add\<close>: Binary Addition\<close> 213 214lemma bin_add_Pls [simp]: "w \<in> bin ==> bin_add(Pls,w) = w" 215by (unfold bin_add_def, simp) 216 217lemma bin_add_Pls_right: "w \<in> bin ==> bin_add(w,Pls) = w" 218apply (unfold bin_add_def) 219apply (erule bin.induct, auto) 220done 221 222lemma bin_add_Min [simp]: "w \<in> bin ==> bin_add(Min,w) = bin_pred(w)" 223by (unfold bin_add_def, simp) 224 225lemma bin_add_Min_right: "w \<in> bin ==> bin_add(w,Min) = bin_pred(w)" 226apply (unfold bin_add_def) 227apply (erule bin.induct, auto) 228done 229 230lemma bin_add_BIT_Pls [simp]: "bin_add(v BIT x,Pls) = v BIT x" 231by (unfold bin_add_def, simp) 232 233lemma bin_add_BIT_Min [simp]: "bin_add(v BIT x,Min) = bin_pred(v BIT x)" 234by (unfold bin_add_def, simp) 235 236lemma bin_add_BIT_BIT [simp]: 237 "[| w \<in> bin; y \<in> bool |] 238 ==> bin_add(v BIT x, w BIT y) = 239 NCons(bin_add(v, cond(x and y, bin_succ(w), w)), x xor y)" 240by (unfold bin_add_def, simp) 241 242lemma integ_of_add [rule_format]: 243 "v \<in> bin ==> 244 \<forall>w\<in>bin. integ_of(bin_add(v,w)) = integ_of(v) $+ integ_of(w)" 245apply (erule bin.induct, simp, simp) 246apply (rule ballI) 247apply (induct_tac "wa") 248apply (auto simp add: zadd_ac elim!: boolE) 249done 250 251(*Subtraction*) 252lemma diff_integ_of_eq: 253 "[| v \<in> bin; w \<in> bin |] 254 ==> integ_of(v) $- integ_of(w) = integ_of(bin_add (v, bin_minus(w)))" 255apply (unfold zdiff_def) 256apply (simp add: integ_of_add integ_of_minus) 257done 258 259 260subsubsection\<open>\<^term>\<open>bin_mult\<close>: Binary Multiplication\<close> 261 262lemma integ_of_mult: 263 "[| v \<in> bin; w \<in> bin |] 264 ==> integ_of(bin_mult(v,w)) = integ_of(v) $* integ_of(w)" 265apply (induct_tac "v", simp) 266apply (simp add: integ_of_minus) 267apply (auto simp add: zadd_ac integ_of_add zadd_zmult_distrib elim!: boolE) 268done 269 270 271subsection\<open>Computations\<close> 272 273(** extra rules for bin_succ, bin_pred **) 274 275lemma bin_succ_1: "bin_succ(w BIT 1) = bin_succ(w) BIT 0" 276by simp 277 278lemma bin_succ_0: "bin_succ(w BIT 0) = NCons(w,1)" 279by simp 280 281lemma bin_pred_1: "bin_pred(w BIT 1) = NCons(w,0)" 282by simp 283 284lemma bin_pred_0: "bin_pred(w BIT 0) = bin_pred(w) BIT 1" 285by simp 286 287(** extra rules for bin_minus **) 288 289lemma bin_minus_1: "bin_minus(w BIT 1) = bin_pred(NCons(bin_minus(w), 0))" 290by simp 291 292lemma bin_minus_0: "bin_minus(w BIT 0) = bin_minus(w) BIT 0" 293by simp 294 295(** extra rules for bin_add **) 296 297lemma bin_add_BIT_11: "w \<in> bin ==> bin_add(v BIT 1, w BIT 1) = 298 NCons(bin_add(v, bin_succ(w)), 0)" 299by simp 300 301lemma bin_add_BIT_10: "w \<in> bin ==> bin_add(v BIT 1, w BIT 0) = 302 NCons(bin_add(v,w), 1)" 303by simp 304 305lemma bin_add_BIT_0: "[| w \<in> bin; y \<in> bool |] 306 ==> bin_add(v BIT 0, w BIT y) = NCons(bin_add(v,w), y)" 307by simp 308 309(** extra rules for bin_mult **) 310 311lemma bin_mult_1: "bin_mult(v BIT 1, w) = bin_add(NCons(bin_mult(v,w),0), w)" 312by simp 313 314lemma bin_mult_0: "bin_mult(v BIT 0, w) = NCons(bin_mult(v,w),0)" 315by simp 316 317 318(** Simplification rules with integer constants **) 319 320lemma int_of_0: "$#0 = #0" 321by simp 322 323lemma int_of_succ: "$# succ(n) = #1 $+ $#n" 324by (simp add: int_of_add [symmetric] natify_succ) 325 326lemma zminus_0 [simp]: "$- #0 = #0" 327by simp 328 329lemma zadd_0_intify [simp]: "#0 $+ z = intify(z)" 330by simp 331 332lemma zadd_0_right_intify [simp]: "z $+ #0 = intify(z)" 333by simp 334 335lemma zmult_1_intify [simp]: "#1 $* z = intify(z)" 336by simp 337 338lemma zmult_1_right_intify [simp]: "z $* #1 = intify(z)" 339by (subst zmult_commute, simp) 340 341lemma zmult_0 [simp]: "#0 $* z = #0" 342by simp 343 344lemma zmult_0_right [simp]: "z $* #0 = #0" 345by (subst zmult_commute, simp) 346 347lemma zmult_minus1 [simp]: "#-1 $* z = $-z" 348by (simp add: zcompare_rls) 349 350lemma zmult_minus1_right [simp]: "z $* #-1 = $-z" 351apply (subst zmult_commute) 352apply (rule zmult_minus1) 353done 354 355 356subsection\<open>Simplification Rules for Comparison of Binary Numbers\<close> 357text\<open>Thanks to Norbert Voelker\<close> 358 359(** Equals (=) **) 360 361lemma eq_integ_of_eq: 362 "[| v \<in> bin; w \<in> bin |] 363 ==> ((integ_of(v)) = integ_of(w)) \<longleftrightarrow> 364 iszero (integ_of (bin_add (v, bin_minus(w))))" 365apply (unfold iszero_def) 366apply (simp add: zcompare_rls integ_of_add integ_of_minus) 367done 368 369lemma iszero_integ_of_Pls: "iszero (integ_of(Pls))" 370by (unfold iszero_def, simp) 371 372 373lemma nonzero_integ_of_Min: "~ iszero (integ_of(Min))" 374apply (unfold iszero_def) 375apply (simp add: zminus_equation) 376done 377 378lemma iszero_integ_of_BIT: 379 "[| w \<in> bin; x \<in> bool |] 380 ==> iszero (integ_of (w BIT x)) \<longleftrightarrow> (x=0 & iszero (integ_of(w)))" 381apply (unfold iszero_def, simp) 382apply (subgoal_tac "integ_of (w) \<in> int") 383apply typecheck 384apply (drule int_cases) 385apply (safe elim!: boolE) 386apply (simp_all (asm_lr) add: zcompare_rls zminus_zadd_distrib [symmetric] 387 int_of_add [symmetric]) 388done 389 390lemma iszero_integ_of_0: 391 "w \<in> bin ==> iszero (integ_of (w BIT 0)) \<longleftrightarrow> iszero (integ_of(w))" 392by (simp only: iszero_integ_of_BIT, blast) 393 394lemma iszero_integ_of_1: "w \<in> bin ==> ~ iszero (integ_of (w BIT 1))" 395by (simp only: iszero_integ_of_BIT, blast) 396 397 398 399(** Less-than (<) **) 400 401lemma less_integ_of_eq_neg: 402 "[| v \<in> bin; w \<in> bin |] 403 ==> integ_of(v) $< integ_of(w) 404 \<longleftrightarrow> znegative (integ_of (bin_add (v, bin_minus(w))))" 405apply (unfold zless_def zdiff_def) 406apply (simp add: integ_of_minus integ_of_add) 407done 408 409lemma not_neg_integ_of_Pls: "~ znegative (integ_of(Pls))" 410by simp 411 412lemma neg_integ_of_Min: "znegative (integ_of(Min))" 413by simp 414 415lemma neg_integ_of_BIT: 416 "[| w \<in> bin; x \<in> bool |] 417 ==> znegative (integ_of (w BIT x)) \<longleftrightarrow> znegative (integ_of(w))" 418apply simp 419apply (subgoal_tac "integ_of (w) \<in> int") 420apply typecheck 421apply (drule int_cases) 422apply (auto elim!: boolE simp add: int_of_add [symmetric] zcompare_rls) 423apply (simp_all add: zminus_zadd_distrib [symmetric] zdiff_def 424 int_of_add [symmetric]) 425apply (subgoal_tac "$#1 $- $# succ (succ (n #+ n)) = $- $# succ (n #+ n) ") 426 apply (simp add: zdiff_def) 427apply (simp add: equation_zminus int_of_diff [symmetric]) 428done 429 430(** Less-than-or-equals (<=) **) 431 432lemma le_integ_of_eq_not_less: 433 "(integ_of(x) $\<le> (integ_of(w))) \<longleftrightarrow> ~ (integ_of(w) $< (integ_of(x)))" 434by (simp add: not_zless_iff_zle [THEN iff_sym]) 435 436 437(*Delete the original rewrites, with their clumsy conditional expressions*) 438declare bin_succ_BIT [simp del] 439 bin_pred_BIT [simp del] 440 bin_minus_BIT [simp del] 441 NCons_Pls [simp del] 442 NCons_Min [simp del] 443 bin_adder_BIT [simp del] 444 bin_mult_BIT [simp del] 445 446(*Hide the binary representation of integer constants*) 447declare integ_of_Pls [simp del] integ_of_Min [simp del] integ_of_BIT [simp del] 448 449 450lemmas bin_arith_extra_simps = 451 integ_of_add [symmetric] 452 integ_of_minus [symmetric] 453 integ_of_mult [symmetric] 454 bin_succ_1 bin_succ_0 455 bin_pred_1 bin_pred_0 456 bin_minus_1 bin_minus_0 457 bin_add_Pls_right bin_add_Min_right 458 bin_add_BIT_0 bin_add_BIT_10 bin_add_BIT_11 459 diff_integ_of_eq 460 bin_mult_1 bin_mult_0 NCons_simps 461 462 463(*For making a minimal simpset, one must include these default simprules 464 of thy. Also include simp_thms, or at least (~False)=True*) 465lemmas bin_arith_simps = 466 bin_pred_Pls bin_pred_Min 467 bin_succ_Pls bin_succ_Min 468 bin_add_Pls bin_add_Min 469 bin_minus_Pls bin_minus_Min 470 bin_mult_Pls bin_mult_Min 471 bin_arith_extra_simps 472 473(*Simplification of relational operations*) 474lemmas bin_rel_simps = 475 eq_integ_of_eq iszero_integ_of_Pls nonzero_integ_of_Min 476 iszero_integ_of_0 iszero_integ_of_1 477 less_integ_of_eq_neg 478 not_neg_integ_of_Pls neg_integ_of_Min neg_integ_of_BIT 479 le_integ_of_eq_not_less 480 481declare bin_arith_simps [simp] 482declare bin_rel_simps [simp] 483 484 485(** Simplification of arithmetic when nested to the right **) 486 487lemma add_integ_of_left [simp]: 488 "[| v \<in> bin; w \<in> bin |] 489 ==> integ_of(v) $+ (integ_of(w) $+ z) = (integ_of(bin_add(v,w)) $+ z)" 490by (simp add: zadd_assoc [symmetric]) 491 492lemma mult_integ_of_left [simp]: 493 "[| v \<in> bin; w \<in> bin |] 494 ==> integ_of(v) $* (integ_of(w) $* z) = (integ_of(bin_mult(v,w)) $* z)" 495by (simp add: zmult_assoc [symmetric]) 496 497lemma add_integ_of_diff1 [simp]: 498 "[| v \<in> bin; w \<in> bin |] 499 ==> integ_of(v) $+ (integ_of(w) $- c) = integ_of(bin_add(v,w)) $- (c)" 500apply (unfold zdiff_def) 501apply (rule add_integ_of_left, auto) 502done 503 504lemma add_integ_of_diff2 [simp]: 505 "[| v \<in> bin; w \<in> bin |] 506 ==> integ_of(v) $+ (c $- integ_of(w)) = 507 integ_of (bin_add (v, bin_minus(w))) $+ (c)" 508apply (subst diff_integ_of_eq [symmetric]) 509apply (simp_all add: zdiff_def zadd_ac) 510done 511 512 513(** More for integer constants **) 514 515declare int_of_0 [simp] int_of_succ [simp] 516 517lemma zdiff0 [simp]: "#0 $- x = $-x" 518by (simp add: zdiff_def) 519 520lemma zdiff0_right [simp]: "x $- #0 = intify(x)" 521by (simp add: zdiff_def) 522 523lemma zdiff_self [simp]: "x $- x = #0" 524by (simp add: zdiff_def) 525 526lemma znegative_iff_zless_0: "k \<in> int ==> znegative(k) \<longleftrightarrow> k $< #0" 527by (simp add: zless_def) 528 529lemma zero_zless_imp_znegative_zminus: "[|#0 $< k; k \<in> int|] ==> znegative($-k)" 530by (simp add: zless_def) 531 532lemma zero_zle_int_of [simp]: "#0 $\<le> $# n" 533by (simp add: not_zless_iff_zle [THEN iff_sym] znegative_iff_zless_0 [THEN iff_sym]) 534 535lemma nat_of_0 [simp]: "nat_of(#0) = 0" 536by (simp only: natify_0 int_of_0 [symmetric] nat_of_int_of) 537 538lemma nat_le_int0_lemma: "[| z $\<le> $#0; z \<in> int |] ==> nat_of(z) = 0" 539by (auto simp add: znegative_iff_zless_0 [THEN iff_sym] zle_def zneg_nat_of) 540 541lemma nat_le_int0: "z $\<le> $#0 ==> nat_of(z) = 0" 542apply (subgoal_tac "nat_of (intify (z)) = 0") 543apply (rule_tac [2] nat_le_int0_lemma, auto) 544done 545 546lemma int_of_eq_0_imp_natify_eq_0: "$# n = #0 ==> natify(n) = 0" 547by (rule not_znegative_imp_zero, auto) 548 549lemma nat_of_zminus_int_of: "nat_of($- $# n) = 0" 550by (simp add: nat_of_def int_of_def raw_nat_of zminus image_intrel_int) 551 552lemma int_of_nat_of: "#0 $\<le> z ==> $# nat_of(z) = intify(z)" 553apply (rule not_zneg_nat_of_intify) 554apply (simp add: znegative_iff_zless_0 not_zless_iff_zle) 555done 556 557declare int_of_nat_of [simp] nat_of_zminus_int_of [simp] 558 559lemma int_of_nat_of_if: "$# nat_of(z) = (if #0 $\<le> z then intify(z) else #0)" 560by (simp add: int_of_nat_of znegative_iff_zless_0 not_zle_iff_zless) 561 562lemma zless_nat_iff_int_zless: "[| m \<in> nat; z \<in> int |] ==> (m < nat_of(z)) \<longleftrightarrow> ($#m $< z)" 563apply (case_tac "znegative (z) ") 564apply (erule_tac [2] not_zneg_nat_of [THEN subst]) 565apply (auto dest: zless_trans dest!: zero_zle_int_of [THEN zle_zless_trans] 566 simp add: znegative_iff_zless_0) 567done 568 569 570(** nat_of and zless **) 571 572(*An alternative condition is @{term"$#0 \<subseteq> w"} *) 573lemma zless_nat_conj_lemma: "$#0 $< z ==> (nat_of(w) < nat_of(z)) \<longleftrightarrow> (w $< z)" 574apply (rule iff_trans) 575apply (rule zless_int_of [THEN iff_sym]) 576apply (auto simp add: int_of_nat_of_if simp del: zless_int_of) 577apply (auto elim: zless_asym simp add: not_zle_iff_zless) 578apply (blast intro: zless_zle_trans) 579done 580 581lemma zless_nat_conj: "(nat_of(w) < nat_of(z)) \<longleftrightarrow> ($#0 $< z & w $< z)" 582apply (case_tac "$#0 $< z") 583apply (auto simp add: zless_nat_conj_lemma nat_le_int0 not_zless_iff_zle) 584done 585 586(*This simprule cannot be added unless we can find a way to make eq_integ_of_eq 587 unconditional! 588 [The condition "True" is a hack to prevent looping. 589 Conditional rewrite rules are tried after unconditional ones, so a rule 590 like eq_nat_number_of will be tried first to eliminate #mm=#nn.] 591 lemma integ_of_reorient [simp]: 592 "True ==> (integ_of(w) = x) \<longleftrightarrow> (x = integ_of(w))" 593 by auto 594*) 595 596lemma integ_of_minus_reorient [simp]: 597 "(integ_of(w) = $- x) \<longleftrightarrow> ($- x = integ_of(w))" 598by auto 599 600lemma integ_of_add_reorient [simp]: 601 "(integ_of(w) = x $+ y) \<longleftrightarrow> (x $+ y = integ_of(w))" 602by auto 603 604lemma integ_of_diff_reorient [simp]: 605 "(integ_of(w) = x $- y) \<longleftrightarrow> (x $- y = integ_of(w))" 606by auto 607 608lemma integ_of_mult_reorient [simp]: 609 "(integ_of(w) = x $* y) \<longleftrightarrow> (x $* y = integ_of(w))" 610by auto 611 612(** To simplify inequalities involving integer negation and literals, 613 such as -x = #3 614**) 615 616lemmas [simp] = 617 zminus_equation [where y = "integ_of(w)"] 618 equation_zminus [where x = "integ_of(w)"] 619 for w 620 621lemmas [iff] = 622 zminus_zless [where y = "integ_of(w)"] 623 zless_zminus [where x = "integ_of(w)"] 624 for w 625 626lemmas [iff] = 627 zminus_zle [where y = "integ_of(w)"] 628 zle_zminus [where x = "integ_of(w)"] 629 for w 630 631lemmas [simp] = 632 Let_def [where s = "integ_of(w)"] for w 633 634 635(*** Simprocs for numeric literals ***) 636 637(** Combining of literal coefficients in sums of products **) 638 639lemma zless_iff_zdiff_zless_0: "(x $< y) \<longleftrightarrow> (x$-y $< #0)" 640 by (simp add: zcompare_rls) 641 642lemma eq_iff_zdiff_eq_0: "[| x \<in> int; y \<in> int |] ==> (x = y) \<longleftrightarrow> (x$-y = #0)" 643 by (simp add: zcompare_rls) 644 645lemma zle_iff_zdiff_zle_0: "(x $\<le> y) \<longleftrightarrow> (x$-y $\<le> #0)" 646 by (simp add: zcompare_rls) 647 648 649(** For combine_numerals **) 650 651lemma left_zadd_zmult_distrib: "i$*u $+ (j$*u $+ k) = (i$+j)$*u $+ k" 652 by (simp add: zadd_zmult_distrib zadd_ac) 653 654 655(** For cancel_numerals **) 656 657lemma eq_add_iff1: "(i$*u $+ m = j$*u $+ n) \<longleftrightarrow> ((i$-j)$*u $+ m = intify(n))" 658 apply (simp add: zdiff_def zadd_zmult_distrib) 659 apply (simp add: zcompare_rls) 660 apply (simp add: zadd_ac) 661 done 662 663lemma eq_add_iff2: "(i$*u $+ m = j$*u $+ n) \<longleftrightarrow> (intify(m) = (j$-i)$*u $+ n)" 664 apply (simp add: zdiff_def zadd_zmult_distrib) 665 apply (simp add: zcompare_rls) 666 apply (simp add: zadd_ac) 667 done 668 669context fixes n :: i 670begin 671 672lemmas rel_iff_rel_0_rls = 673 zless_iff_zdiff_zless_0 [where y = "u $+ v"] 674 eq_iff_zdiff_eq_0 [where y = "u $+ v"] 675 zle_iff_zdiff_zle_0 [where y = "u $+ v"] 676 zless_iff_zdiff_zless_0 [where y = n] 677 eq_iff_zdiff_eq_0 [where y = n] 678 zle_iff_zdiff_zle_0 [where y = n] 679 for u v 680 681lemma less_add_iff1: "(i$*u $+ m $< j$*u $+ n) \<longleftrightarrow> ((i$-j)$*u $+ m $< n)" 682 apply (simp add: zdiff_def zadd_zmult_distrib zadd_ac rel_iff_rel_0_rls) 683 done 684 685lemma less_add_iff2: "(i$*u $+ m $< j$*u $+ n) \<longleftrightarrow> (m $< (j$-i)$*u $+ n)" 686 apply (simp add: zdiff_def zadd_zmult_distrib zadd_ac rel_iff_rel_0_rls) 687 done 688 689end 690 691lemma le_add_iff1: "(i$*u $+ m $\<le> j$*u $+ n) \<longleftrightarrow> ((i$-j)$*u $+ m $\<le> n)" 692 apply (simp add: zdiff_def zadd_zmult_distrib) 693 apply (simp add: zcompare_rls) 694 apply (simp add: zadd_ac) 695 done 696 697lemma le_add_iff2: "(i$*u $+ m $\<le> j$*u $+ n) \<longleftrightarrow> (m $\<le> (j$-i)$*u $+ n)" 698 apply (simp add: zdiff_def zadd_zmult_distrib) 699 apply (simp add: zcompare_rls) 700 apply (simp add: zadd_ac) 701 done 702 703ML_file \<open>int_arith.ML\<close> 704 705subsection \<open>examples:\<close> 706 707text \<open>\<open>combine_numerals_prod\<close> (products of separate literals)\<close> 708lemma "#5 $* x $* #3 = y" apply simp oops 709 710schematic_goal "y2 $+ ?x42 = y $+ y2" apply simp oops 711 712lemma "oo : int ==> l $+ (l $+ #2) $+ oo = oo" apply simp oops 713 714lemma "#9$*x $+ y = x$*#23 $+ z" apply simp oops 715lemma "y $+ x = x $+ z" apply simp oops 716 717lemma "x : int ==> x $+ y $+ z = x $+ z" apply simp oops 718lemma "x : int ==> y $+ (z $+ x) = z $+ x" apply simp oops 719lemma "z : int ==> x $+ y $+ z = (z $+ y) $+ (x $+ w)" apply simp oops 720lemma "z : int ==> x$*y $+ z = (z $+ y) $+ (y$*x $+ w)" apply simp oops 721 722lemma "#-3 $* x $+ y $\<le> x $* #2 $+ z" apply simp oops 723lemma "y $+ x $\<le> x $+ z" apply simp oops 724lemma "x $+ y $+ z $\<le> x $+ z" apply simp oops 725 726lemma "y $+ (z $+ x) $< z $+ x" apply simp oops 727lemma "x $+ y $+ z $< (z $+ y) $+ (x $+ w)" apply simp oops 728lemma "x$*y $+ z $< (z $+ y) $+ (y$*x $+ w)" apply simp oops 729 730lemma "l $+ #2 $+ #2 $+ #2 $+ (l $+ #2) $+ (oo $+ #2) = uu" apply simp oops 731lemma "u : int ==> #2 $* u = u" apply simp oops 732lemma "(i $+ j $+ #12 $+ k) $- #15 = y" apply simp oops 733lemma "(i $+ j $+ #12 $+ k) $- #5 = y" apply simp oops 734 735lemma "y $- b $< b" apply simp oops 736lemma "y $- (#3 $* b $+ c) $< b $- #2 $* c" apply simp oops 737 738lemma "(#2 $* x $- (u $* v) $+ y) $- v $* #3 $* u = w" apply simp oops 739lemma "(#2 $* x $* u $* v $+ (u $* v) $* #4 $+ y) $- v $* u $* #4 = w" apply simp oops 740lemma "(#2 $* x $* u $* v $+ (u $* v) $* #4 $+ y) $- v $* u = w" apply simp oops 741lemma "u $* v $- (x $* u $* v $+ (u $* v) $* #4 $+ y) = w" apply simp oops 742 743lemma "(i $+ j $+ #12 $+ k) = u $+ #15 $+ y" apply simp oops 744lemma "(i $+ j $* #2 $+ #12 $+ k) = j $+ #5 $+ y" apply simp oops 745 746lemma "#2 $* y $+ #3 $* z $+ #6 $* w $+ #2 $* y $+ #3 $* z $+ #2 $* u = #2 $* y' $+ #3 $* z' $+ #6 $* w' $+ #2 $* y' $+ #3 $* z' $+ u $+ vv" apply simp oops 747 748lemma "a $+ $-(b$+c) $+ b = d" apply simp oops 749lemma "a $+ $-(b$+c) $- b = d" apply simp oops 750 751text \<open>negative numerals\<close> 752lemma "(i $+ j $+ #-2 $+ k) $- (u $+ #5 $+ y) = zz" apply simp oops 753lemma "(i $+ j $+ #-3 $+ k) $< u $+ #5 $+ y" apply simp oops 754lemma "(i $+ j $+ #3 $+ k) $< u $+ #-6 $+ y" apply simp oops 755lemma "(i $+ j $+ #-12 $+ k) $- #15 = y" apply simp oops 756lemma "(i $+ j $+ #12 $+ k) $- #-15 = y" apply simp oops 757lemma "(i $+ j $+ #-12 $+ k) $- #-15 = y" apply simp oops 758 759text \<open>Multiplying separated numerals\<close> 760lemma "#6 $* ($# x $* #2) = uu" apply simp oops 761lemma "#4 $* ($# x $* $# x) $* (#2 $* $# x) = uu" apply simp oops 762 763end 764