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