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