src/ZF/Bin.thy
 author wenzelm Tue Sep 25 22:36:06 2012 +0200 (2012-09-25 ago) changeset 49566 66cbf8bb4693 parent 48891 c0eafbd55de3 child 58022 464c1815fde9 permissions -rw-r--r--
basic integration of graphview into document model;
 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@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@45703 ` 104` ``` "_Int" :: "xnum_token => i" ("_") ``` wenzelm@35112 ` 105` wenzelm@48891 ` 106` ```ML_file "Tools/numeral_syntax.ML" ``` wenzelm@35123 ` 107` ```setup Numeral_Syntax.setup ``` wenzelm@23146 ` 108` wenzelm@23146 ` 109` wenzelm@23146 ` 110` ```declare bin.intros [simp,TC] ``` wenzelm@23146 ` 111` wenzelm@23146 ` 112` ```lemma NCons_Pls_0: "NCons(Pls,0) = Pls" ``` wenzelm@23146 ` 113` ```by simp ``` wenzelm@23146 ` 114` wenzelm@23146 ` 115` ```lemma NCons_Pls_1: "NCons(Pls,1) = Pls BIT 1" ``` wenzelm@23146 ` 116` ```by simp ``` wenzelm@23146 ` 117` wenzelm@23146 ` 118` ```lemma NCons_Min_0: "NCons(Min,0) = Min BIT 0" ``` wenzelm@23146 ` 119` ```by simp ``` wenzelm@23146 ` 120` wenzelm@23146 ` 121` ```lemma NCons_Min_1: "NCons(Min,1) = Min" ``` wenzelm@23146 ` 122` ```by simp ``` wenzelm@23146 ` 123` wenzelm@23146 ` 124` ```lemma NCons_BIT: "NCons(w BIT x,b) = w BIT x BIT b" ``` wenzelm@23146 ` 125` ```by (simp add: bin.case_eqns) ``` wenzelm@23146 ` 126` paulson@46820 ` 127` ```lemmas NCons_simps [simp] = ``` wenzelm@23146 ` 128` ``` NCons_Pls_0 NCons_Pls_1 NCons_Min_0 NCons_Min_1 NCons_BIT ``` wenzelm@23146 ` 129` wenzelm@23146 ` 130` wenzelm@23146 ` 131` wenzelm@23146 ` 132` ```(** Type checking **) ``` wenzelm@23146 ` 133` paulson@46953 ` 134` ```lemma integ_of_type [TC]: "w \ bin ==> integ_of(w) \ int" ``` wenzelm@23146 ` 135` ```apply (induct_tac "w") ``` wenzelm@23146 ` 136` ```apply (simp_all add: bool_into_nat) ``` wenzelm@23146 ` 137` ```done ``` wenzelm@23146 ` 138` paulson@46953 ` 139` ```lemma NCons_type [TC]: "[| w \ bin; b \ bool |] ==> NCons(w,b) \ bin" ``` wenzelm@23146 ` 140` ```by (induct_tac "w", auto) ``` wenzelm@23146 ` 141` paulson@46953 ` 142` ```lemma bin_succ_type [TC]: "w \ bin ==> bin_succ(w) \ bin" ``` wenzelm@23146 ` 143` ```by (induct_tac "w", auto) ``` wenzelm@23146 ` 144` paulson@46953 ` 145` ```lemma bin_pred_type [TC]: "w \ bin ==> bin_pred(w) \ bin" ``` wenzelm@23146 ` 146` ```by (induct_tac "w", auto) ``` wenzelm@23146 ` 147` paulson@46953 ` 148` ```lemma bin_minus_type [TC]: "w \ bin ==> bin_minus(w) \ bin" ``` wenzelm@23146 ` 149` ```by (induct_tac "w", auto) ``` wenzelm@23146 ` 150` wenzelm@23146 ` 151` ```(*This proof is complicated by the mutual recursion*) ``` wenzelm@23146 ` 152` ```lemma bin_add_type [rule_format,TC]: ``` paulson@46953 ` 153` ``` "v \ bin ==> \w\bin. bin_add(v,w) \ bin" ``` wenzelm@23146 ` 154` ```apply (unfold bin_add_def) ``` wenzelm@23146 ` 155` ```apply (induct_tac "v") ``` wenzelm@23146 ` 156` ```apply (rule_tac [3] ballI) ``` wenzelm@23146 ` 157` ```apply (rename_tac [3] "w'") ``` wenzelm@23146 ` 158` ```apply (induct_tac [3] "w'") ``` wenzelm@23146 ` 159` ```apply (simp_all add: NCons_type) ``` wenzelm@23146 ` 160` ```done ``` wenzelm@23146 ` 161` paulson@46953 ` 162` ```lemma bin_mult_type [TC]: "[| v \ bin; w \ bin |] ==> bin_mult(v,w) \ bin" ``` wenzelm@23146 ` 163` ```by (induct_tac "v", auto) ``` wenzelm@23146 ` 164` wenzelm@23146 ` 165` paulson@46820 ` 166` ```subsubsection{*The Carry and Borrow Functions, ``` wenzelm@23146 ` 167` ``` @{term bin_succ} and @{term bin_pred}*} ``` wenzelm@23146 ` 168` wenzelm@23146 ` 169` ```(*NCons preserves the integer value of its argument*) ``` wenzelm@23146 ` 170` ```lemma integ_of_NCons [simp]: ``` paulson@46953 ` 171` ``` "[| w \ bin; b \ bool |] ==> integ_of(NCons(w,b)) = integ_of(w BIT b)" ``` wenzelm@23146 ` 172` ```apply (erule bin.cases) ``` paulson@46820 ` 173` ```apply (auto elim!: boolE) ``` wenzelm@23146 ` 174` ```done ``` wenzelm@23146 ` 175` wenzelm@23146 ` 176` ```lemma integ_of_succ [simp]: ``` paulson@46953 ` 177` ``` "w \ bin ==> integ_of(bin_succ(w)) = \$#1 \$+ integ_of(w)" ``` wenzelm@23146 ` 178` ```apply (erule bin.induct) ``` paulson@46820 ` 179` ```apply (auto simp add: zadd_ac elim!: boolE) ``` wenzelm@23146 ` 180` ```done ``` wenzelm@23146 ` 181` wenzelm@23146 ` 182` ```lemma integ_of_pred [simp]: ``` paulson@46953 ` 183` ``` "w \ bin ==> integ_of(bin_pred(w)) = \$- (\$#1) \$+ integ_of(w)" ``` wenzelm@23146 ` 184` ```apply (erule bin.induct) ``` paulson@46820 ` 185` ```apply (auto simp add: zadd_ac elim!: boolE) ``` wenzelm@23146 ` 186` ```done ``` wenzelm@23146 ` 187` wenzelm@23146 ` 188` wenzelm@23146 ` 189` ```subsubsection{*@{term bin_minus}: Unary Negation of Binary Integers*} ``` wenzelm@23146 ` 190` paulson@46953 ` 191` ```lemma integ_of_minus: "w \ bin ==> integ_of(bin_minus(w)) = \$- integ_of(w)" ``` wenzelm@23146 ` 192` ```apply (erule bin.induct) ``` paulson@46820 ` 193` ```apply (auto simp add: zadd_ac zminus_zadd_distrib elim!: boolE) ``` wenzelm@23146 ` 194` ```done ``` wenzelm@23146 ` 195` wenzelm@23146 ` 196` wenzelm@23146 ` 197` ```subsubsection{*@{term bin_add}: Binary Addition*} ``` wenzelm@23146 ` 198` paulson@46953 ` 199` ```lemma bin_add_Pls [simp]: "w \ bin ==> bin_add(Pls,w) = w" ``` wenzelm@23146 ` 200` ```by (unfold bin_add_def, simp) ``` wenzelm@23146 ` 201` paulson@46953 ` 202` ```lemma bin_add_Pls_right: "w \ bin ==> bin_add(w,Pls) = w" ``` wenzelm@23146 ` 203` ```apply (unfold bin_add_def) ``` wenzelm@23146 ` 204` ```apply (erule bin.induct, auto) ``` wenzelm@23146 ` 205` ```done ``` wenzelm@23146 ` 206` paulson@46953 ` 207` ```lemma bin_add_Min [simp]: "w \ bin ==> bin_add(Min,w) = bin_pred(w)" ``` wenzelm@23146 ` 208` ```by (unfold bin_add_def, simp) ``` wenzelm@23146 ` 209` paulson@46953 ` 210` ```lemma bin_add_Min_right: "w \ bin ==> bin_add(w,Min) = bin_pred(w)" ``` wenzelm@23146 ` 211` ```apply (unfold bin_add_def) ``` wenzelm@23146 ` 212` ```apply (erule bin.induct, auto) ``` wenzelm@23146 ` 213` ```done ``` wenzelm@23146 ` 214` wenzelm@23146 ` 215` ```lemma bin_add_BIT_Pls [simp]: "bin_add(v BIT x,Pls) = v BIT x" ``` wenzelm@23146 ` 216` ```by (unfold bin_add_def, simp) ``` wenzelm@23146 ` 217` wenzelm@23146 ` 218` ```lemma bin_add_BIT_Min [simp]: "bin_add(v BIT x,Min) = bin_pred(v BIT x)" ``` wenzelm@23146 ` 219` ```by (unfold bin_add_def, simp) ``` wenzelm@23146 ` 220` wenzelm@23146 ` 221` ```lemma bin_add_BIT_BIT [simp]: ``` paulson@46953 ` 222` ``` "[| w \ bin; y \ bool |] ``` paulson@46820 ` 223` ``` ==> bin_add(v BIT x, w BIT y) = ``` wenzelm@23146 ` 224` ``` NCons(bin_add(v, cond(x and y, bin_succ(w), w)), x xor y)" ``` wenzelm@23146 ` 225` ```by (unfold bin_add_def, simp) ``` wenzelm@23146 ` 226` wenzelm@23146 ` 227` ```lemma integ_of_add [rule_format]: ``` paulson@46953 ` 228` ``` "v \ bin ==> ``` paulson@46820 ` 229` ``` \w\bin. integ_of(bin_add(v,w)) = integ_of(v) \$+ integ_of(w)" ``` wenzelm@23146 ` 230` ```apply (erule bin.induct, simp, simp) ``` wenzelm@23146 ` 231` ```apply (rule ballI) ``` wenzelm@23146 ` 232` ```apply (induct_tac "wa") ``` paulson@46820 ` 233` ```apply (auto simp add: zadd_ac elim!: boolE) ``` wenzelm@23146 ` 234` ```done ``` wenzelm@23146 ` 235` wenzelm@23146 ` 236` ```(*Subtraction*) ``` paulson@46820 ` 237` ```lemma diff_integ_of_eq: ``` paulson@46953 ` 238` ``` "[| v \ bin; w \ bin |] ``` wenzelm@23146 ` 239` ``` ==> integ_of(v) \$- integ_of(w) = integ_of(bin_add (v, bin_minus(w)))" ``` wenzelm@23146 ` 240` ```apply (unfold zdiff_def) ``` wenzelm@23146 ` 241` ```apply (simp add: integ_of_add integ_of_minus) ``` wenzelm@23146 ` 242` ```done ``` wenzelm@23146 ` 243` wenzelm@23146 ` 244` wenzelm@23146 ` 245` ```subsubsection{*@{term bin_mult}: Binary Multiplication*} ``` wenzelm@23146 ` 246` wenzelm@23146 ` 247` ```lemma integ_of_mult: ``` paulson@46953 ` 248` ``` "[| v \ bin; w \ bin |] ``` wenzelm@23146 ` 249` ``` ==> integ_of(bin_mult(v,w)) = integ_of(v) \$* integ_of(w)" ``` wenzelm@23146 ` 250` ```apply (induct_tac "v", simp) ``` wenzelm@23146 ` 251` ```apply (simp add: integ_of_minus) ``` paulson@46820 ` 252` ```apply (auto simp add: zadd_ac integ_of_add zadd_zmult_distrib elim!: boolE) ``` wenzelm@23146 ` 253` ```done ``` wenzelm@23146 ` 254` wenzelm@23146 ` 255` wenzelm@23146 ` 256` ```subsection{*Computations*} ``` wenzelm@23146 ` 257` wenzelm@23146 ` 258` ```(** extra rules for bin_succ, bin_pred **) ``` wenzelm@23146 ` 259` wenzelm@23146 ` 260` ```lemma bin_succ_1: "bin_succ(w BIT 1) = bin_succ(w) BIT 0" ``` wenzelm@23146 ` 261` ```by simp ``` wenzelm@23146 ` 262` wenzelm@23146 ` 263` ```lemma bin_succ_0: "bin_succ(w BIT 0) = NCons(w,1)" ``` wenzelm@23146 ` 264` ```by simp ``` wenzelm@23146 ` 265` wenzelm@23146 ` 266` ```lemma bin_pred_1: "bin_pred(w BIT 1) = NCons(w,0)" ``` wenzelm@23146 ` 267` ```by simp ``` wenzelm@23146 ` 268` wenzelm@23146 ` 269` ```lemma bin_pred_0: "bin_pred(w BIT 0) = bin_pred(w) BIT 1" ``` wenzelm@23146 ` 270` ```by simp ``` wenzelm@23146 ` 271` wenzelm@23146 ` 272` ```(** extra rules for bin_minus **) ``` wenzelm@23146 ` 273` wenzelm@23146 ` 274` ```lemma bin_minus_1: "bin_minus(w BIT 1) = bin_pred(NCons(bin_minus(w), 0))" ``` wenzelm@23146 ` 275` ```by simp ``` wenzelm@23146 ` 276` wenzelm@23146 ` 277` ```lemma bin_minus_0: "bin_minus(w BIT 0) = bin_minus(w) BIT 0" ``` wenzelm@23146 ` 278` ```by simp ``` wenzelm@23146 ` 279` wenzelm@23146 ` 280` ```(** extra rules for bin_add **) ``` wenzelm@23146 ` 281` paulson@46953 ` 282` ```lemma bin_add_BIT_11: "w \ bin ==> bin_add(v BIT 1, w BIT 1) = ``` wenzelm@23146 ` 283` ``` NCons(bin_add(v, bin_succ(w)), 0)" ``` wenzelm@23146 ` 284` ```by simp ``` wenzelm@23146 ` 285` paulson@46953 ` 286` ```lemma bin_add_BIT_10: "w \ bin ==> bin_add(v BIT 1, w BIT 0) = ``` wenzelm@23146 ` 287` ``` NCons(bin_add(v,w), 1)" ``` wenzelm@23146 ` 288` ```by simp ``` wenzelm@23146 ` 289` paulson@46953 ` 290` ```lemma bin_add_BIT_0: "[| w \ bin; y \ bool |] ``` wenzelm@23146 ` 291` ``` ==> bin_add(v BIT 0, w BIT y) = NCons(bin_add(v,w), y)" ``` wenzelm@23146 ` 292` ```by simp ``` wenzelm@23146 ` 293` wenzelm@23146 ` 294` ```(** extra rules for bin_mult **) ``` wenzelm@23146 ` 295` wenzelm@23146 ` 296` ```lemma bin_mult_1: "bin_mult(v BIT 1, w) = bin_add(NCons(bin_mult(v,w),0), w)" ``` wenzelm@23146 ` 297` ```by simp ``` wenzelm@23146 ` 298` wenzelm@23146 ` 299` ```lemma bin_mult_0: "bin_mult(v BIT 0, w) = NCons(bin_mult(v,w),0)" ``` wenzelm@23146 ` 300` ```by simp ``` wenzelm@23146 ` 301` wenzelm@23146 ` 302` wenzelm@23146 ` 303` ```(** Simplification rules with integer constants **) ``` wenzelm@23146 ` 304` wenzelm@23146 ` 305` ```lemma int_of_0: "\$#0 = #0" ``` wenzelm@23146 ` 306` ```by simp ``` wenzelm@23146 ` 307` wenzelm@23146 ` 308` ```lemma int_of_succ: "\$# succ(n) = #1 \$+ \$#n" ``` wenzelm@23146 ` 309` ```by (simp add: int_of_add [symmetric] natify_succ) ``` wenzelm@23146 ` 310` wenzelm@23146 ` 311` ```lemma zminus_0 [simp]: "\$- #0 = #0" ``` wenzelm@23146 ` 312` ```by simp ``` wenzelm@23146 ` 313` wenzelm@23146 ` 314` ```lemma zadd_0_intify [simp]: "#0 \$+ z = intify(z)" ``` wenzelm@23146 ` 315` ```by simp ``` wenzelm@23146 ` 316` wenzelm@23146 ` 317` ```lemma zadd_0_right_intify [simp]: "z \$+ #0 = intify(z)" ``` wenzelm@23146 ` 318` ```by simp ``` wenzelm@23146 ` 319` wenzelm@23146 ` 320` ```lemma zmult_1_intify [simp]: "#1 \$* z = intify(z)" ``` wenzelm@23146 ` 321` ```by simp ``` wenzelm@23146 ` 322` wenzelm@23146 ` 323` ```lemma zmult_1_right_intify [simp]: "z \$* #1 = intify(z)" ``` wenzelm@23146 ` 324` ```by (subst zmult_commute, simp) ``` wenzelm@23146 ` 325` wenzelm@23146 ` 326` ```lemma zmult_0 [simp]: "#0 \$* z = #0" ``` wenzelm@23146 ` 327` ```by simp ``` wenzelm@23146 ` 328` wenzelm@23146 ` 329` ```lemma zmult_0_right [simp]: "z \$* #0 = #0" ``` wenzelm@23146 ` 330` ```by (subst zmult_commute, simp) ``` wenzelm@23146 ` 331` wenzelm@23146 ` 332` ```lemma zmult_minus1 [simp]: "#-1 \$* z = \$-z" ``` wenzelm@23146 ` 333` ```by (simp add: zcompare_rls) ``` wenzelm@23146 ` 334` wenzelm@23146 ` 335` ```lemma zmult_minus1_right [simp]: "z \$* #-1 = \$-z" ``` wenzelm@23146 ` 336` ```apply (subst zmult_commute) ``` wenzelm@23146 ` 337` ```apply (rule zmult_minus1) ``` wenzelm@23146 ` 338` ```done ``` wenzelm@23146 ` 339` wenzelm@23146 ` 340` wenzelm@23146 ` 341` ```subsection{*Simplification Rules for Comparison of Binary Numbers*} ``` wenzelm@23146 ` 342` ```text{*Thanks to Norbert Voelker*} ``` wenzelm@23146 ` 343` wenzelm@23146 ` 344` ```(** Equals (=) **) ``` wenzelm@23146 ` 345` paulson@46820 ` 346` ```lemma eq_integ_of_eq: ``` paulson@46953 ` 347` ``` "[| v \ bin; w \ bin |] ``` paulson@46821 ` 348` ``` ==> ((integ_of(v)) = integ_of(w)) \ ``` wenzelm@23146 ` 349` ``` iszero (integ_of (bin_add (v, bin_minus(w))))" ``` wenzelm@23146 ` 350` ```apply (unfold iszero_def) ``` wenzelm@23146 ` 351` ```apply (simp add: zcompare_rls integ_of_add integ_of_minus) ``` wenzelm@23146 ` 352` ```done ``` wenzelm@23146 ` 353` wenzelm@23146 ` 354` ```lemma iszero_integ_of_Pls: "iszero (integ_of(Pls))" ``` wenzelm@23146 ` 355` ```by (unfold iszero_def, simp) ``` wenzelm@23146 ` 356` wenzelm@23146 ` 357` wenzelm@23146 ` 358` ```lemma nonzero_integ_of_Min: "~ iszero (integ_of(Min))" ``` wenzelm@23146 ` 359` ```apply (unfold iszero_def) ``` wenzelm@23146 ` 360` ```apply (simp add: zminus_equation) ``` wenzelm@23146 ` 361` ```done ``` wenzelm@23146 ` 362` paulson@46820 ` 363` ```lemma iszero_integ_of_BIT: ``` paulson@46953 ` 364` ``` "[| w \ bin; x \ bool |] ``` paulson@46821 ` 365` ``` ==> iszero (integ_of (w BIT x)) \ (x=0 & iszero (integ_of(w)))" ``` wenzelm@23146 ` 366` ```apply (unfold iszero_def, simp) ``` paulson@46820 ` 367` ```apply (subgoal_tac "integ_of (w) \ int") ``` wenzelm@23146 ` 368` ```apply typecheck ``` wenzelm@23146 ` 369` ```apply (drule int_cases) ``` wenzelm@23146 ` 370` ```apply (safe elim!: boolE) ``` wenzelm@23146 ` 371` ```apply (simp_all (asm_lr) add: zcompare_rls zminus_zadd_distrib [symmetric] ``` wenzelm@23146 ` 372` ``` int_of_add [symmetric]) ``` wenzelm@23146 ` 373` ```done ``` wenzelm@23146 ` 374` wenzelm@23146 ` 375` ```lemma iszero_integ_of_0: ``` paulson@46953 ` 376` ``` "w \ bin ==> iszero (integ_of (w BIT 0)) \ iszero (integ_of(w))" ``` paulson@46820 ` 377` ```by (simp only: iszero_integ_of_BIT, blast) ``` wenzelm@23146 ` 378` paulson@46953 ` 379` ```lemma iszero_integ_of_1: "w \ bin ==> ~ iszero (integ_of (w BIT 1))" ``` wenzelm@23146 ` 380` ```by (simp only: iszero_integ_of_BIT, blast) ``` wenzelm@23146 ` 381` wenzelm@23146 ` 382` wenzelm@23146 ` 383` wenzelm@23146 ` 384` ```(** Less-than (<) **) ``` wenzelm@23146 ` 385` paulson@46820 ` 386` ```lemma less_integ_of_eq_neg: ``` paulson@46953 ` 387` ``` "[| v \ bin; w \ bin |] ``` paulson@46820 ` 388` ``` ==> integ_of(v) \$< integ_of(w) ``` paulson@46821 ` 389` ``` \ znegative (integ_of (bin_add (v, bin_minus(w))))" ``` wenzelm@23146 ` 390` ```apply (unfold zless_def zdiff_def) ``` wenzelm@23146 ` 391` ```apply (simp add: integ_of_minus integ_of_add) ``` wenzelm@23146 ` 392` ```done ``` wenzelm@23146 ` 393` wenzelm@23146 ` 394` ```lemma not_neg_integ_of_Pls: "~ znegative (integ_of(Pls))" ``` wenzelm@23146 ` 395` ```by simp ``` wenzelm@23146 ` 396` wenzelm@23146 ` 397` ```lemma neg_integ_of_Min: "znegative (integ_of(Min))" ``` wenzelm@23146 ` 398` ```by simp ``` wenzelm@23146 ` 399` wenzelm@23146 ` 400` ```lemma neg_integ_of_BIT: ``` paulson@46953 ` 401` ``` "[| w \ bin; x \ bool |] ``` paulson@46821 ` 402` ``` ==> znegative (integ_of (w BIT x)) \ znegative (integ_of(w))" ``` wenzelm@23146 ` 403` ```apply simp ``` paulson@46820 ` 404` ```apply (subgoal_tac "integ_of (w) \ int") ``` wenzelm@23146 ` 405` ```apply typecheck ``` wenzelm@23146 ` 406` ```apply (drule int_cases) ``` wenzelm@23146 ` 407` ```apply (auto elim!: boolE simp add: int_of_add [symmetric] zcompare_rls) ``` paulson@46820 ` 408` ```apply (simp_all add: zminus_zadd_distrib [symmetric] zdiff_def ``` wenzelm@23146 ` 409` ``` int_of_add [symmetric]) ``` wenzelm@23146 ` 410` ```apply (subgoal_tac "\$#1 \$- \$# succ (succ (n #+ n)) = \$- \$# succ (n #+ n) ") ``` wenzelm@23146 ` 411` ``` apply (simp add: zdiff_def) ``` wenzelm@23146 ` 412` ```apply (simp add: equation_zminus int_of_diff [symmetric]) ``` wenzelm@23146 ` 413` ```done ``` wenzelm@23146 ` 414` wenzelm@23146 ` 415` ```(** Less-than-or-equals (<=) **) ``` wenzelm@23146 ` 416` wenzelm@23146 ` 417` ```lemma le_integ_of_eq_not_less: ``` paulson@46821 ` 418` ``` "(integ_of(x) \$<= (integ_of(w))) \ ~ (integ_of(w) \$< (integ_of(x)))" ``` wenzelm@23146 ` 419` ```by (simp add: not_zless_iff_zle [THEN iff_sym]) ``` wenzelm@23146 ` 420` wenzelm@23146 ` 421` wenzelm@23146 ` 422` ```(*Delete the original rewrites, with their clumsy conditional expressions*) ``` paulson@46820 ` 423` ```declare bin_succ_BIT [simp del] ``` paulson@46820 ` 424` ``` bin_pred_BIT [simp del] ``` wenzelm@23146 ` 425` ``` bin_minus_BIT [simp del] ``` wenzelm@23146 ` 426` ``` NCons_Pls [simp del] ``` wenzelm@23146 ` 427` ``` NCons_Min [simp del] ``` wenzelm@23146 ` 428` ``` bin_adder_BIT [simp del] ``` wenzelm@23146 ` 429` ``` bin_mult_BIT [simp del] ``` wenzelm@23146 ` 430` wenzelm@23146 ` 431` ```(*Hide the binary representation of integer constants*) ``` wenzelm@23146 ` 432` ```declare integ_of_Pls [simp del] integ_of_Min [simp del] integ_of_BIT [simp del] ``` wenzelm@23146 ` 433` wenzelm@23146 ` 434` wenzelm@23146 ` 435` ```lemmas bin_arith_extra_simps = ``` paulson@46820 ` 436` ``` integ_of_add [symmetric] ``` paulson@46820 ` 437` ``` integ_of_minus [symmetric] ``` paulson@46820 ` 438` ``` integ_of_mult [symmetric] ``` paulson@46820 ` 439` ``` bin_succ_1 bin_succ_0 ``` paulson@46820 ` 440` ``` bin_pred_1 bin_pred_0 ``` paulson@46820 ` 441` ``` bin_minus_1 bin_minus_0 ``` wenzelm@23146 ` 442` ``` bin_add_Pls_right bin_add_Min_right ``` wenzelm@23146 ` 443` ``` bin_add_BIT_0 bin_add_BIT_10 bin_add_BIT_11 ``` wenzelm@23146 ` 444` ``` diff_integ_of_eq ``` wenzelm@23146 ` 445` ``` bin_mult_1 bin_mult_0 NCons_simps ``` wenzelm@23146 ` 446` wenzelm@23146 ` 447` wenzelm@23146 ` 448` ```(*For making a minimal simpset, one must include these default simprules ``` wenzelm@23146 ` 449` ``` of thy. Also include simp_thms, or at least (~False)=True*) ``` wenzelm@23146 ` 450` ```lemmas bin_arith_simps = ``` wenzelm@23146 ` 451` ``` bin_pred_Pls bin_pred_Min ``` wenzelm@23146 ` 452` ``` bin_succ_Pls bin_succ_Min ``` wenzelm@23146 ` 453` ``` bin_add_Pls bin_add_Min ``` wenzelm@23146 ` 454` ``` bin_minus_Pls bin_minus_Min ``` paulson@46820 ` 455` ``` bin_mult_Pls bin_mult_Min ``` wenzelm@23146 ` 456` ``` bin_arith_extra_simps ``` wenzelm@23146 ` 457` wenzelm@23146 ` 458` ```(*Simplification of relational operations*) ``` wenzelm@23146 ` 459` ```lemmas bin_rel_simps = ``` wenzelm@23146 ` 460` ``` eq_integ_of_eq iszero_integ_of_Pls nonzero_integ_of_Min ``` wenzelm@23146 ` 461` ``` iszero_integ_of_0 iszero_integ_of_1 ``` wenzelm@23146 ` 462` ``` less_integ_of_eq_neg ``` wenzelm@23146 ` 463` ``` not_neg_integ_of_Pls neg_integ_of_Min neg_integ_of_BIT ``` wenzelm@23146 ` 464` ``` le_integ_of_eq_not_less ``` wenzelm@23146 ` 465` wenzelm@23146 ` 466` ```declare bin_arith_simps [simp] ``` wenzelm@23146 ` 467` ```declare bin_rel_simps [simp] ``` wenzelm@23146 ` 468` wenzelm@23146 ` 469` wenzelm@23146 ` 470` ```(** Simplification of arithmetic when nested to the right **) ``` wenzelm@23146 ` 471` wenzelm@23146 ` 472` ```lemma add_integ_of_left [simp]: ``` paulson@46953 ` 473` ``` "[| v \ bin; w \ bin |] ``` wenzelm@23146 ` 474` ``` ==> integ_of(v) \$+ (integ_of(w) \$+ z) = (integ_of(bin_add(v,w)) \$+ z)" ``` wenzelm@23146 ` 475` ```by (simp add: zadd_assoc [symmetric]) ``` wenzelm@23146 ` 476` wenzelm@23146 ` 477` ```lemma mult_integ_of_left [simp]: ``` paulson@46953 ` 478` ``` "[| v \ bin; w \ bin |] ``` wenzelm@23146 ` 479` ``` ==> integ_of(v) \$* (integ_of(w) \$* z) = (integ_of(bin_mult(v,w)) \$* z)" ``` wenzelm@23146 ` 480` ```by (simp add: zmult_assoc [symmetric]) ``` wenzelm@23146 ` 481` paulson@46820 ` 482` ```lemma add_integ_of_diff1 [simp]: ``` paulson@46953 ` 483` ``` "[| v \ bin; w \ bin |] ``` wenzelm@23146 ` 484` ``` ==> integ_of(v) \$+ (integ_of(w) \$- c) = integ_of(bin_add(v,w)) \$- (c)" ``` wenzelm@23146 ` 485` ```apply (unfold zdiff_def) ``` wenzelm@23146 ` 486` ```apply (rule add_integ_of_left, auto) ``` wenzelm@23146 ` 487` ```done ``` wenzelm@23146 ` 488` wenzelm@23146 ` 489` ```lemma add_integ_of_diff2 [simp]: ``` paulson@46953 ` 490` ``` "[| v \ bin; w \ bin |] ``` paulson@46820 ` 491` ``` ==> integ_of(v) \$+ (c \$- integ_of(w)) = ``` wenzelm@23146 ` 492` ``` integ_of (bin_add (v, bin_minus(w))) \$+ (c)" ``` wenzelm@23146 ` 493` ```apply (subst diff_integ_of_eq [symmetric]) ``` wenzelm@23146 ` 494` ```apply (simp_all add: zdiff_def zadd_ac) ``` wenzelm@23146 ` 495` ```done ``` wenzelm@23146 ` 496` wenzelm@23146 ` 497` wenzelm@23146 ` 498` ```(** More for integer constants **) ``` wenzelm@23146 ` 499` wenzelm@23146 ` 500` ```declare int_of_0 [simp] int_of_succ [simp] ``` wenzelm@23146 ` 501` wenzelm@23146 ` 502` ```lemma zdiff0 [simp]: "#0 \$- x = \$-x" ``` wenzelm@23146 ` 503` ```by (simp add: zdiff_def) ``` wenzelm@23146 ` 504` wenzelm@23146 ` 505` ```lemma zdiff0_right [simp]: "x \$- #0 = intify(x)" ``` wenzelm@23146 ` 506` ```by (simp add: zdiff_def) ``` wenzelm@23146 ` 507` wenzelm@23146 ` 508` ```lemma zdiff_self [simp]: "x \$- x = #0" ``` wenzelm@23146 ` 509` ```by (simp add: zdiff_def) ``` wenzelm@23146 ` 510` paulson@46953 ` 511` ```lemma znegative_iff_zless_0: "k \ int ==> znegative(k) \ k \$< #0" ``` wenzelm@23146 ` 512` ```by (simp add: zless_def) ``` wenzelm@23146 ` 513` paulson@46953 ` 514` ```lemma zero_zless_imp_znegative_zminus: "[|#0 \$< k; k \ int|] ==> znegative(\$-k)" ``` wenzelm@23146 ` 515` ```by (simp add: zless_def) ``` wenzelm@23146 ` 516` wenzelm@23146 ` 517` ```lemma zero_zle_int_of [simp]: "#0 \$<= \$# n" ``` wenzelm@23146 ` 518` ```by (simp add: not_zless_iff_zle [THEN iff_sym] znegative_iff_zless_0 [THEN iff_sym]) ``` wenzelm@23146 ` 519` wenzelm@23146 ` 520` ```lemma nat_of_0 [simp]: "nat_of(#0) = 0" ``` wenzelm@23146 ` 521` ```by (simp only: natify_0 int_of_0 [symmetric] nat_of_int_of) ``` wenzelm@23146 ` 522` paulson@46953 ` 523` ```lemma nat_le_int0_lemma: "[| z \$<= \$#0; z \ int |] ==> nat_of(z) = 0" ``` wenzelm@23146 ` 524` ```by (auto simp add: znegative_iff_zless_0 [THEN iff_sym] zle_def zneg_nat_of) ``` wenzelm@23146 ` 525` wenzelm@23146 ` 526` ```lemma nat_le_int0: "z \$<= \$#0 ==> nat_of(z) = 0" ``` wenzelm@23146 ` 527` ```apply (subgoal_tac "nat_of (intify (z)) = 0") ``` wenzelm@23146 ` 528` ```apply (rule_tac [2] nat_le_int0_lemma, auto) ``` wenzelm@23146 ` 529` ```done ``` wenzelm@23146 ` 530` wenzelm@23146 ` 531` ```lemma int_of_eq_0_imp_natify_eq_0: "\$# n = #0 ==> natify(n) = 0" ``` wenzelm@23146 ` 532` ```by (rule not_znegative_imp_zero, auto) ``` wenzelm@23146 ` 533` wenzelm@23146 ` 534` ```lemma nat_of_zminus_int_of: "nat_of(\$- \$# n) = 0" ``` wenzelm@23146 ` 535` ```by (simp add: nat_of_def int_of_def raw_nat_of zminus image_intrel_int) ``` wenzelm@23146 ` 536` wenzelm@23146 ` 537` ```lemma int_of_nat_of: "#0 \$<= z ==> \$# nat_of(z) = intify(z)" ``` wenzelm@23146 ` 538` ```apply (rule not_zneg_nat_of_intify) ``` wenzelm@23146 ` 539` ```apply (simp add: znegative_iff_zless_0 not_zless_iff_zle) ``` wenzelm@23146 ` 540` ```done ``` wenzelm@23146 ` 541` wenzelm@23146 ` 542` ```declare int_of_nat_of [simp] nat_of_zminus_int_of [simp] ``` wenzelm@23146 ` 543` wenzelm@23146 ` 544` ```lemma int_of_nat_of_if: "\$# nat_of(z) = (if #0 \$<= z then intify(z) else #0)" ``` wenzelm@23146 ` 545` ```by (simp add: int_of_nat_of znegative_iff_zless_0 not_zle_iff_zless) ``` wenzelm@23146 ` 546` paulson@46953 ` 547` ```lemma zless_nat_iff_int_zless: "[| m \ nat; z \ int |] ==> (m < nat_of(z)) \ (\$#m \$< z)" ``` wenzelm@23146 ` 548` ```apply (case_tac "znegative (z) ") ``` wenzelm@23146 ` 549` ```apply (erule_tac [2] not_zneg_nat_of [THEN subst]) ``` wenzelm@23146 ` 550` ```apply (auto dest: zless_trans dest!: zero_zle_int_of [THEN zle_zless_trans] ``` wenzelm@23146 ` 551` ``` simp add: znegative_iff_zless_0) ``` wenzelm@23146 ` 552` ```done ``` wenzelm@23146 ` 553` wenzelm@23146 ` 554` wenzelm@23146 ` 555` ```(** nat_of and zless **) ``` wenzelm@23146 ` 556` paulson@46820 ` 557` ```(*An alternative condition is @{term"\$#0 \ w"} *) ``` paulson@46821 ` 558` ```lemma zless_nat_conj_lemma: "\$#0 \$< z ==> (nat_of(w) < nat_of(z)) \ (w \$< z)" ``` wenzelm@23146 ` 559` ```apply (rule iff_trans) ``` wenzelm@23146 ` 560` ```apply (rule zless_int_of [THEN iff_sym]) ``` wenzelm@23146 ` 561` ```apply (auto simp add: int_of_nat_of_if simp del: zless_int_of) ``` wenzelm@23146 ` 562` ```apply (auto elim: zless_asym simp add: not_zle_iff_zless) ``` wenzelm@23146 ` 563` ```apply (blast intro: zless_zle_trans) ``` wenzelm@23146 ` 564` ```done ``` wenzelm@23146 ` 565` paulson@46821 ` 566` ```lemma zless_nat_conj: "(nat_of(w) < nat_of(z)) \ (\$#0 \$< z & w \$< z)" ``` wenzelm@23146 ` 567` ```apply (case_tac "\$#0 \$< z") ``` wenzelm@23146 ` 568` ```apply (auto simp add: zless_nat_conj_lemma nat_le_int0 not_zless_iff_zle) ``` wenzelm@23146 ` 569` ```done ``` wenzelm@23146 ` 570` wenzelm@23146 ` 571` ```(*This simprule cannot be added unless we can find a way to make eq_integ_of_eq ``` wenzelm@23146 ` 572` ``` unconditional! ``` wenzelm@23146 ` 573` ``` [The condition "True" is a hack to prevent looping. ``` wenzelm@23146 ` 574` ``` Conditional rewrite rules are tried after unconditional ones, so a rule ``` wenzelm@23146 ` 575` ``` like eq_nat_number_of will be tried first to eliminate #mm=#nn.] ``` wenzelm@23146 ` 576` ``` lemma integ_of_reorient [simp]: ``` paulson@46821 ` 577` ``` "True ==> (integ_of(w) = x) \ (x = integ_of(w))" ``` wenzelm@23146 ` 578` ``` by auto ``` wenzelm@23146 ` 579` ```*) ``` wenzelm@23146 ` 580` wenzelm@23146 ` 581` ```lemma integ_of_minus_reorient [simp]: ``` paulson@46821 ` 582` ``` "(integ_of(w) = \$- x) \ (\$- x = integ_of(w))" ``` wenzelm@23146 ` 583` ```by auto ``` wenzelm@23146 ` 584` wenzelm@23146 ` 585` ```lemma integ_of_add_reorient [simp]: ``` paulson@46821 ` 586` ``` "(integ_of(w) = x \$+ y) \ (x \$+ y = integ_of(w))" ``` wenzelm@23146 ` 587` ```by auto ``` wenzelm@23146 ` 588` wenzelm@23146 ` 589` ```lemma integ_of_diff_reorient [simp]: ``` paulson@46821 ` 590` ``` "(integ_of(w) = x \$- y) \ (x \$- y = integ_of(w))" ``` wenzelm@23146 ` 591` ```by auto ``` wenzelm@23146 ` 592` wenzelm@23146 ` 593` ```lemma integ_of_mult_reorient [simp]: ``` paulson@46821 ` 594` ``` "(integ_of(w) = x \$* y) \ (x \$* y = integ_of(w))" ``` wenzelm@23146 ` 595` ```by auto ``` wenzelm@23146 ` 596` wenzelm@23146 ` 597` ```end ```