src/ZF/Bin.thy
 author wenzelm Fri Jun 10 12:51:29 2011 +0200 (2011-06-10) changeset 43348 3e153e719039 parent 35123 e286d5df187a child 45703 c7a13ce60161 permissions -rw-r--r--
uniform use of flexflex_rule;
 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@23146 ` 16` ```header{*Arithmetic on Binary Integers*} ``` wenzelm@23146 ` 17` wenzelm@23146 ` 18` ```theory Bin ``` krauss@26056 ` 19` ```imports Int_ZF Datatype_ZF ``` wenzelm@26190 ` 20` ```uses ("Tools/numeral_syntax.ML") ``` wenzelm@23146 ` 21` ```begin ``` wenzelm@23146 ` 22` wenzelm@23146 ` 23` ```consts bin :: i ``` wenzelm@23146 ` 24` ```datatype ``` wenzelm@23146 ` 25` ``` "bin" = Pls ``` wenzelm@23146 ` 26` ``` | Min ``` wenzelm@32960 ` 27` ``` | Bit ("w: bin", "b: bool") (infixl "BIT" 90) ``` wenzelm@23146 ` 28` wenzelm@23146 ` 29` ```consts ``` wenzelm@23146 ` 30` ``` integ_of :: "i=>i" ``` wenzelm@23146 ` 31` ``` NCons :: "[i,i]=>i" ``` wenzelm@23146 ` 32` ``` bin_succ :: "i=>i" ``` wenzelm@23146 ` 33` ``` bin_pred :: "i=>i" ``` wenzelm@23146 ` 34` ``` bin_minus :: "i=>i" ``` wenzelm@23146 ` 35` ``` bin_adder :: "i=>i" ``` wenzelm@23146 ` 36` ``` bin_mult :: "[i,i]=>i" ``` wenzelm@23146 ` 37` wenzelm@23146 ` 38` ```primrec ``` wenzelm@23146 ` 39` ``` integ_of_Pls: "integ_of (Pls) = \$# 0" ``` wenzelm@23146 ` 40` ``` integ_of_Min: "integ_of (Min) = \$-(\$#1)" ``` wenzelm@23146 ` 41` ``` integ_of_BIT: "integ_of (w BIT b) = \$#b \$+ integ_of(w) \$+ integ_of(w)" ``` wenzelm@23146 ` 42` wenzelm@23146 ` 43` ``` (** recall that cond(1,b,c)=b and cond(0,b,c)=0 **) ``` wenzelm@23146 ` 44` wenzelm@23146 ` 45` ```primrec (*NCons adds a bit, suppressing leading 0s and 1s*) ``` wenzelm@23146 ` 46` ``` NCons_Pls: "NCons (Pls,b) = cond(b,Pls BIT b,Pls)" ``` wenzelm@23146 ` 47` ``` NCons_Min: "NCons (Min,b) = cond(b,Min,Min BIT b)" ``` wenzelm@23146 ` 48` ``` NCons_BIT: "NCons (w BIT c,b) = w BIT c BIT b" ``` wenzelm@23146 ` 49` wenzelm@23146 ` 50` ```primrec (*successor. If a BIT, can change a 0 to a 1 without recursion.*) ``` wenzelm@23146 ` 51` ``` bin_succ_Pls: "bin_succ (Pls) = Pls BIT 1" ``` wenzelm@23146 ` 52` ``` bin_succ_Min: "bin_succ (Min) = Pls" ``` wenzelm@23146 ` 53` ``` bin_succ_BIT: "bin_succ (w BIT b) = cond(b, bin_succ(w) BIT 0, NCons(w,1))" ``` wenzelm@23146 ` 54` wenzelm@23146 ` 55` ```primrec (*predecessor*) ``` wenzelm@23146 ` 56` ``` bin_pred_Pls: "bin_pred (Pls) = Min" ``` wenzelm@23146 ` 57` ``` bin_pred_Min: "bin_pred (Min) = Min BIT 0" ``` wenzelm@23146 ` 58` ``` bin_pred_BIT: "bin_pred (w BIT b) = cond(b, NCons(w,0), bin_pred(w) BIT 1)" ``` wenzelm@23146 ` 59` wenzelm@23146 ` 60` ```primrec (*unary negation*) ``` wenzelm@23146 ` 61` ``` bin_minus_Pls: ``` wenzelm@23146 ` 62` ``` "bin_minus (Pls) = Pls" ``` wenzelm@23146 ` 63` ``` bin_minus_Min: ``` wenzelm@23146 ` 64` ``` "bin_minus (Min) = Pls BIT 1" ``` wenzelm@23146 ` 65` ``` bin_minus_BIT: ``` wenzelm@23146 ` 66` ``` "bin_minus (w BIT b) = cond(b, bin_pred(NCons(bin_minus(w),0)), ``` wenzelm@32960 ` 67` ``` bin_minus(w) BIT 0)" ``` wenzelm@23146 ` 68` wenzelm@23146 ` 69` ```primrec (*sum*) ``` wenzelm@23146 ` 70` ``` bin_adder_Pls: ``` wenzelm@23146 ` 71` ``` "bin_adder (Pls) = (lam w:bin. w)" ``` wenzelm@23146 ` 72` ``` bin_adder_Min: ``` wenzelm@23146 ` 73` ``` "bin_adder (Min) = (lam w:bin. bin_pred(w))" ``` wenzelm@23146 ` 74` ``` bin_adder_BIT: ``` wenzelm@23146 ` 75` ``` "bin_adder (v BIT x) = ``` wenzelm@23146 ` 76` ``` (lam w:bin. ``` wenzelm@23146 ` 77` ``` bin_case (v BIT x, bin_pred(v BIT x), ``` wenzelm@23146 ` 78` ``` %w y. NCons(bin_adder (v) ` cond(x and y, bin_succ(w), w), ``` wenzelm@23146 ` 79` ``` x xor y), ``` wenzelm@23146 ` 80` ``` w))" ``` wenzelm@23146 ` 81` wenzelm@23146 ` 82` ```(*The bin_case above replaces the following mutually recursive function: ``` wenzelm@23146 ` 83` ```primrec ``` wenzelm@23146 ` 84` ``` "adding (v,x,Pls) = v BIT x" ``` wenzelm@23146 ` 85` ``` "adding (v,x,Min) = bin_pred(v BIT x)" ``` wenzelm@23146 ` 86` ``` "adding (v,x,w BIT y) = NCons(bin_adder (v, cond(x and y, bin_succ(w), w)), ``` wenzelm@32960 ` 87` ``` x xor y)" ``` wenzelm@23146 ` 88` ```*) ``` wenzelm@23146 ` 89` wenzelm@24893 ` 90` ```definition ``` wenzelm@24893 ` 91` ``` bin_add :: "[i,i]=>i" where ``` wenzelm@23146 ` 92` ``` "bin_add(v,w) == bin_adder(v)`w" ``` wenzelm@23146 ` 93` wenzelm@23146 ` 94` wenzelm@23146 ` 95` ```primrec ``` wenzelm@23146 ` 96` ``` bin_mult_Pls: ``` wenzelm@23146 ` 97` ``` "bin_mult (Pls,w) = Pls" ``` wenzelm@23146 ` 98` ``` bin_mult_Min: ``` wenzelm@23146 ` 99` ``` "bin_mult (Min,w) = bin_minus(w)" ``` wenzelm@23146 ` 100` ``` bin_mult_BIT: ``` wenzelm@23146 ` 101` ``` "bin_mult (v BIT b,w) = cond(b, bin_add(NCons(bin_mult(v,w),0),w), ``` wenzelm@32960 ` 102` ``` NCons(bin_mult(v,w),0))" ``` wenzelm@23146 ` 103` wenzelm@35112 ` 104` ```syntax ``` wenzelm@35112 ` 105` ``` "_Int" :: "xnum => i" ("_") ``` wenzelm@35112 ` 106` wenzelm@35112 ` 107` ```use "Tools/numeral_syntax.ML" ``` wenzelm@35123 ` 108` ```setup Numeral_Syntax.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` ```end ```