src/HOL/Library/Word.thy
 author paulson Tue Jul 20 14:23:09 2004 +0200 (2004-07-20) changeset 15067 02be3516e90b parent 15013 34264f5e4691 child 15131 c69542757a4d permissions -rw-r--r--
removed some obsolete proofs
 skalberg@14494 ` 1` ```(* Title: HOL/Library/Word.thy ``` skalberg@14494 ` 2` ``` ID: \$Id\$ ``` skalberg@14494 ` 3` ``` Author: Sebastian Skalberg (TU Muenchen) ``` skalberg@14494 ` 4` ```*) ``` skalberg@14494 ` 5` wenzelm@14706 ` 6` ```header {* Binary Words *} ``` wenzelm@14589 ` 7` skalberg@14494 ` 8` ```theory Word = Main files "word_setup.ML": ``` skalberg@14494 ` 9` skalberg@14494 ` 10` ```subsection {* Auxilary Lemmas *} ``` skalberg@14494 ` 11` skalberg@14494 ` 12` ```lemma max_le [intro!]: "[| x \ z; y \ z |] ==> max x y \ z" ``` skalberg@14494 ` 13` ``` by (simp add: max_def) ``` skalberg@14494 ` 14` skalberg@14494 ` 15` ```lemma max_mono: ``` paulson@15067 ` 16` ``` fixes x :: "'a::linorder" ``` skalberg@14494 ` 17` ``` assumes mf: "mono f" ``` paulson@15067 ` 18` ``` shows "max (f x) (f y) \ f (max x y)" ``` skalberg@14494 ` 19` ```proof - ``` skalberg@14494 ` 20` ``` from mf and le_maxI1 [of x y] ``` skalberg@14494 ` 21` ``` have fx: "f x \ f (max x y)" ``` skalberg@14494 ` 22` ``` by (rule monoD) ``` skalberg@14494 ` 23` ``` from mf and le_maxI2 [of y x] ``` skalberg@14494 ` 24` ``` have fy: "f y \ f (max x y)" ``` skalberg@14494 ` 25` ``` by (rule monoD) ``` skalberg@14494 ` 26` ``` from fx and fy ``` skalberg@14494 ` 27` ``` show "max (f x) (f y) \ f (max x y)" ``` skalberg@14494 ` 28` ``` by auto ``` skalberg@14494 ` 29` ```qed ``` skalberg@14494 ` 30` paulson@15067 ` 31` ```declare zero_le_power [intro] ``` paulson@15067 ` 32` ``` and zero_less_power [intro] ``` skalberg@14494 ` 33` skalberg@14494 ` 34` ```lemma int_nat_two_exp: "2 ^ k = int (2 ^ k)" ``` skalberg@14494 ` 35` ``` by (induct k,simp_all) ``` skalberg@14494 ` 36` wenzelm@14589 ` 37` ```subsection {* Bits *} ``` skalberg@14494 ` 38` skalberg@14494 ` 39` ```datatype bit ``` skalberg@14494 ` 40` ``` = Zero ("\") ``` skalberg@14494 ` 41` ``` | One ("\") ``` skalberg@14494 ` 42` skalberg@14494 ` 43` ```consts ``` skalberg@14494 ` 44` ``` bitval :: "bit => int" ``` skalberg@14494 ` 45` skalberg@14494 ` 46` ```primrec ``` skalberg@14494 ` 47` ``` "bitval \ = 0" ``` skalberg@14494 ` 48` ``` "bitval \ = 1" ``` skalberg@14494 ` 49` skalberg@14494 ` 50` ```consts ``` skalberg@14494 ` 51` ``` bitnot :: "bit => bit" ``` skalberg@14494 ` 52` ``` bitand :: "bit => bit => bit" (infixr "bitand" 35) ``` skalberg@14494 ` 53` ``` bitor :: "bit => bit => bit" (infixr "bitor" 30) ``` skalberg@14494 ` 54` ``` bitxor :: "bit => bit => bit" (infixr "bitxor" 30) ``` skalberg@14494 ` 55` skalberg@14494 ` 56` ```syntax (xsymbols) ``` skalberg@14494 ` 57` ``` bitnot :: "bit => bit" ("\\<^sub>b _" [40] 40) ``` skalberg@14494 ` 58` ``` bitand :: "bit => bit => bit" (infixr "\\<^sub>b" 35) ``` skalberg@14494 ` 59` ``` bitor :: "bit => bit => bit" (infixr "\\<^sub>b" 30) ``` skalberg@14494 ` 60` ``` bitxor :: "bit => bit => bit" (infixr "\\<^sub>b" 30) ``` skalberg@14494 ` 61` kleing@14565 ` 62` ```syntax (HTML output) ``` kleing@14565 ` 63` ``` bitnot :: "bit => bit" ("\\<^sub>b _" [40] 40) ``` kleing@14565 ` 64` ``` bitand :: "bit => bit => bit" (infixr "\\<^sub>b" 35) ``` kleing@14565 ` 65` ``` bitor :: "bit => bit => bit" (infixr "\\<^sub>b" 30) ``` kleing@14565 ` 66` ``` bitxor :: "bit => bit => bit" (infixr "\\<^sub>b" 30) ``` kleing@14565 ` 67` skalberg@14494 ` 68` ```primrec ``` skalberg@14494 ` 69` ``` bitnot_zero: "(bitnot \) = \" ``` skalberg@14494 ` 70` ``` bitnot_one : "(bitnot \) = \" ``` skalberg@14494 ` 71` skalberg@14494 ` 72` ```primrec ``` skalberg@14494 ` 73` ``` bitand_zero: "(\ bitand y) = \" ``` skalberg@14494 ` 74` ``` bitand_one: "(\ bitand y) = y" ``` skalberg@14494 ` 75` skalberg@14494 ` 76` ```primrec ``` skalberg@14494 ` 77` ``` bitor_zero: "(\ bitor y) = y" ``` skalberg@14494 ` 78` ``` bitor_one: "(\ bitor y) = \" ``` skalberg@14494 ` 79` skalberg@14494 ` 80` ```primrec ``` skalberg@14494 ` 81` ``` bitxor_zero: "(\ bitxor y) = y" ``` skalberg@14494 ` 82` ``` bitxor_one: "(\ bitxor y) = (bitnot y)" ``` skalberg@14494 ` 83` skalberg@14494 ` 84` ```lemma [simp]: "(bitnot (bitnot b)) = b" ``` skalberg@14494 ` 85` ``` by (cases b,simp_all) ``` skalberg@14494 ` 86` skalberg@14494 ` 87` ```lemma [simp]: "(b bitand b) = b" ``` skalberg@14494 ` 88` ``` by (cases b,simp_all) ``` skalberg@14494 ` 89` skalberg@14494 ` 90` ```lemma [simp]: "(b bitor b) = b" ``` skalberg@14494 ` 91` ``` by (cases b,simp_all) ``` skalberg@14494 ` 92` skalberg@14494 ` 93` ```lemma [simp]: "(b bitxor b) = \" ``` skalberg@14494 ` 94` ``` by (cases b,simp_all) ``` skalberg@14494 ` 95` wenzelm@14589 ` 96` ```subsection {* Bit Vectors *} ``` skalberg@14494 ` 97` skalberg@14494 ` 98` ```text {* First, a couple of theorems expressing case analysis and ``` skalberg@14494 ` 99` ```induction principles for bit vectors. *} ``` skalberg@14494 ` 100` skalberg@14494 ` 101` ```lemma bit_list_cases: ``` skalberg@14494 ` 102` ``` assumes empty: "w = [] ==> P w" ``` skalberg@14494 ` 103` ``` and zero: "!!bs. w = \ # bs ==> P w" ``` skalberg@14494 ` 104` ``` and one: "!!bs. w = \ # bs ==> P w" ``` skalberg@14494 ` 105` ``` shows "P w" ``` skalberg@14494 ` 106` ```proof (cases w) ``` skalberg@14494 ` 107` ``` assume "w = []" ``` skalberg@14494 ` 108` ``` thus ?thesis ``` skalberg@14494 ` 109` ``` by (rule empty) ``` skalberg@14494 ` 110` ```next ``` skalberg@14494 ` 111` ``` fix b bs ``` skalberg@14494 ` 112` ``` assume [simp]: "w = b # bs" ``` skalberg@14494 ` 113` ``` show "P w" ``` skalberg@14494 ` 114` ``` proof (cases b) ``` skalberg@14494 ` 115` ``` assume "b = \" ``` skalberg@14494 ` 116` ``` hence "w = \ # bs" ``` skalberg@14494 ` 117` ``` by simp ``` skalberg@14494 ` 118` ``` thus ?thesis ``` skalberg@14494 ` 119` ``` by (rule zero) ``` skalberg@14494 ` 120` ``` next ``` skalberg@14494 ` 121` ``` assume "b = \" ``` skalberg@14494 ` 122` ``` hence "w = \ # bs" ``` skalberg@14494 ` 123` ``` by simp ``` skalberg@14494 ` 124` ``` thus ?thesis ``` skalberg@14494 ` 125` ``` by (rule one) ``` skalberg@14494 ` 126` ``` qed ``` skalberg@14494 ` 127` ```qed ``` skalberg@14494 ` 128` skalberg@14494 ` 129` ```lemma bit_list_induct: ``` skalberg@14494 ` 130` ``` assumes empty: "P []" ``` skalberg@14494 ` 131` ``` and zero: "!!bs. P bs ==> P (\#bs)" ``` skalberg@14494 ` 132` ``` and one: "!!bs. P bs ==> P (\#bs)" ``` skalberg@14494 ` 133` ``` shows "P w" ``` skalberg@14494 ` 134` ```proof (induct w,simp_all add: empty) ``` skalberg@14494 ` 135` ``` fix b bs ``` skalberg@14494 ` 136` ``` assume [intro!]: "P bs" ``` skalberg@14494 ` 137` ``` show "P (b#bs)" ``` skalberg@14494 ` 138` ``` by (cases b,auto intro!: zero one) ``` skalberg@14494 ` 139` ```qed ``` skalberg@14494 ` 140` skalberg@14494 ` 141` ```constdefs ``` skalberg@14494 ` 142` ``` bv_msb :: "bit list => bit" ``` skalberg@14494 ` 143` ``` "bv_msb w == if w = [] then \ else hd w" ``` skalberg@14494 ` 144` ``` bv_extend :: "[nat,bit,bit list]=>bit list" ``` skalberg@14494 ` 145` ``` "bv_extend i b w == (replicate (i - length w) b) @ w" ``` skalberg@14494 ` 146` ``` bv_not :: "bit list => bit list" ``` skalberg@14494 ` 147` ``` "bv_not w == map bitnot w" ``` skalberg@14494 ` 148` skalberg@14494 ` 149` ```lemma bv_length_extend [simp]: "length w \ i ==> length (bv_extend i b w) = i" ``` skalberg@14494 ` 150` ``` by (simp add: bv_extend_def) ``` skalberg@14494 ` 151` skalberg@14494 ` 152` ```lemma [simp]: "bv_not [] = []" ``` skalberg@14494 ` 153` ``` by (simp add: bv_not_def) ``` skalberg@14494 ` 154` skalberg@14494 ` 155` ```lemma [simp]: "bv_not (b#bs) = (bitnot b) # bv_not bs" ``` skalberg@14494 ` 156` ``` by (simp add: bv_not_def) ``` skalberg@14494 ` 157` skalberg@14494 ` 158` ```lemma [simp]: "bv_not (bv_not w) = w" ``` skalberg@14494 ` 159` ``` by (rule bit_list_induct [of _ w],simp_all) ``` skalberg@14494 ` 160` skalberg@14494 ` 161` ```lemma [simp]: "bv_msb [] = \" ``` skalberg@14494 ` 162` ``` by (simp add: bv_msb_def) ``` skalberg@14494 ` 163` skalberg@14494 ` 164` ```lemma [simp]: "bv_msb (b#bs) = b" ``` skalberg@14494 ` 165` ``` by (simp add: bv_msb_def) ``` skalberg@14494 ` 166` skalberg@14494 ` 167` ```lemma [simp]: "0 < length w ==> bv_msb (bv_not w) = (bitnot (bv_msb w))" ``` skalberg@14494 ` 168` ``` by (cases w,simp_all) ``` skalberg@14494 ` 169` skalberg@14494 ` 170` ```lemma [simp,intro]: "bv_msb w = \ ==> 0 < length w" ``` skalberg@14494 ` 171` ``` by (cases w,simp_all) ``` skalberg@14494 ` 172` skalberg@14494 ` 173` ```lemma [simp]: "length (bv_not w) = length w" ``` skalberg@14494 ` 174` ``` by (induct w,simp_all) ``` skalberg@14494 ` 175` skalberg@14494 ` 176` ```constdefs ``` skalberg@14494 ` 177` ``` bv_to_nat :: "bit list => int" ``` paulson@15013 ` 178` ``` "bv_to_nat bv == number_of (foldl (%bn b. bn BIT (b = \)) Numeral.Pls bv)" ``` skalberg@14494 ` 179` skalberg@14494 ` 180` ```lemma [simp]: "bv_to_nat [] = 0" ``` skalberg@14494 ` 181` ``` by (simp add: bv_to_nat_def) ``` skalberg@14494 ` 182` paulson@15013 ` 183` ```lemma pos_number_of: ``` paulson@15013 ` 184` ``` "number_of (w BIT b) = (2::int) * number_of w + (if b then 1 else 0)" ``` paulson@15013 ` 185` ```by (simp add: mult_2) ``` skalberg@14494 ` 186` skalberg@14494 ` 187` ```lemma bv_to_nat_helper [simp]: "bv_to_nat (b # bs) = bitval b * 2 ^ length bs + bv_to_nat bs" ``` skalberg@14494 ` 188` ```proof - ``` skalberg@14494 ` 189` ``` def bv_to_nat' == "%base bv. number_of (foldl (% bn b. bn BIT (b = \)) base bv)::int" ``` skalberg@14494 ` 190` ``` have bv_to_nat'_def: "!!base bv. bv_to_nat' base bv == number_of (foldl (% bn b. bn BIT (b = \)) base bv)::int" ``` skalberg@14494 ` 191` ``` by (simp add: bv_to_nat'_def) ``` skalberg@14494 ` 192` ``` have [rule_format]: "\ base bs. (0::int) \ number_of base --> (\ b. bv_to_nat' base (b # bs) = bv_to_nat' (base BIT (b = \)) bs)" ``` skalberg@14494 ` 193` ``` by (simp add: bv_to_nat'_def) ``` paulson@15013 ` 194` ``` have helper [rule_format]: "\ base. (0::int) \ number_of base --> bv_to_nat' base bs = number_of base * 2 ^ length bs + bv_to_nat' Numeral.Pls bs" ``` skalberg@14494 ` 195` ``` proof (induct bs,simp add: bv_to_nat'_def,clarify) ``` skalberg@14494 ` 196` ``` fix x xs base ``` paulson@15013 ` 197` ``` assume ind [rule_format]: "\ base. (0::int) \ number_of base --> bv_to_nat' base xs = number_of base * 2 ^ length xs + bv_to_nat' Numeral.Pls xs" ``` skalberg@14494 ` 198` ``` assume base_pos: "(0::int) \ number_of base" ``` skalberg@14494 ` 199` ``` def qq == "number_of base::int" ``` paulson@15013 ` 200` ``` show "bv_to_nat' base (x # xs) = number_of base * 2 ^ (length (x # xs)) + bv_to_nat' Numeral.Pls (x # xs)" ``` skalberg@14494 ` 201` ``` apply (unfold bv_to_nat'_def) ``` skalberg@14494 ` 202` ``` apply (simp only: foldl.simps) ``` skalberg@14494 ` 203` ``` apply (fold bv_to_nat'_def) ``` skalberg@14494 ` 204` ``` apply (subst ind [of "base BIT (x = \)"]) ``` skalberg@14494 ` 205` ``` using base_pos ``` skalberg@14494 ` 206` ``` apply simp ``` paulson@15013 ` 207` ``` apply (subst ind [of "Numeral.Pls BIT (x = \)"]) ``` skalberg@14494 ` 208` ``` apply simp ``` skalberg@14494 ` 209` ``` apply (subst pos_number_of [of "base" "x = \"]) ``` skalberg@14494 ` 210` ``` using base_pos ``` paulson@15013 ` 211` ``` apply (subst pos_number_of [of "Numeral.Pls" "x = \"]) ``` skalberg@14494 ` 212` ``` apply (fold qq_def) ``` skalberg@14494 ` 213` ``` apply (simp add: ring_distrib) ``` skalberg@14494 ` 214` ``` done ``` skalberg@14494 ` 215` ``` qed ``` skalberg@14494 ` 216` ``` show ?thesis ``` skalberg@14494 ` 217` ``` apply (unfold bv_to_nat_def [of "b # bs"]) ``` skalberg@14494 ` 218` ``` apply (simp only: foldl.simps) ``` skalberg@14494 ` 219` ``` apply (fold bv_to_nat'_def) ``` skalberg@14494 ` 220` ``` apply (subst helper) ``` skalberg@14494 ` 221` ``` apply simp ``` skalberg@14494 ` 222` ``` apply (cases "b::bit") ``` skalberg@14494 ` 223` ``` apply (simp add: bv_to_nat'_def bv_to_nat_def) ``` skalberg@14494 ` 224` ``` apply (simp add: iszero_def) ``` skalberg@14494 ` 225` ``` apply (simp add: bv_to_nat'_def bv_to_nat_def) ``` skalberg@14494 ` 226` ``` done ``` skalberg@14494 ` 227` ```qed ``` skalberg@14494 ` 228` skalberg@14494 ` 229` ```lemma bv_to_nat0 [simp]: "bv_to_nat (\#bs) = bv_to_nat bs" ``` skalberg@14494 ` 230` ``` by simp ``` skalberg@14494 ` 231` skalberg@14494 ` 232` ```lemma bv_to_nat1 [simp]: "bv_to_nat (\#bs) = 2 ^ length bs + bv_to_nat bs" ``` skalberg@14494 ` 233` ``` by simp ``` skalberg@14494 ` 234` skalberg@14494 ` 235` ```lemma bv_to_nat_lower_range [intro,simp]: "0 \ bv_to_nat w" ``` skalberg@14494 ` 236` ``` apply (induct w,simp_all) ``` skalberg@14494 ` 237` ``` apply (case_tac a,simp_all) ``` skalberg@14494 ` 238` ``` apply (rule add_increasing) ``` skalberg@14494 ` 239` ``` apply auto ``` skalberg@14494 ` 240` ``` done ``` skalberg@14494 ` 241` skalberg@14494 ` 242` ```lemma bv_to_nat_upper_range: "bv_to_nat w < 2 ^ length w" ``` skalberg@14494 ` 243` ```proof (induct w,simp_all) ``` skalberg@14494 ` 244` ``` fix b bs ``` skalberg@14494 ` 245` ``` assume "bv_to_nat bs < 2 ^ length bs" ``` skalberg@14494 ` 246` ``` show "bitval b * 2 ^ length bs + bv_to_nat bs < 2 * 2 ^ length bs" ``` skalberg@14494 ` 247` ``` proof (cases b,simp_all) ``` skalberg@14494 ` 248` ``` have "bv_to_nat bs < 2 ^ length bs" ``` skalberg@14494 ` 249` ``` . ``` skalberg@14494 ` 250` ``` also have "... < 2 * 2 ^ length bs" ``` skalberg@14494 ` 251` ``` by auto ``` skalberg@14494 ` 252` ``` finally show "bv_to_nat bs < 2 * 2 ^ length bs" ``` skalberg@14494 ` 253` ``` by simp ``` skalberg@14494 ` 254` ``` next ``` skalberg@14494 ` 255` ``` have "bv_to_nat bs < 2 ^ length bs" ``` skalberg@14494 ` 256` ``` . ``` skalberg@14494 ` 257` ``` hence "2 ^ length bs + bv_to_nat bs < 2 ^ length bs + 2 ^ length bs" ``` skalberg@14494 ` 258` ``` by arith ``` skalberg@14494 ` 259` ``` also have "... = 2 * (2 ^ length bs)" ``` skalberg@14494 ` 260` ``` by simp ``` skalberg@14494 ` 261` ``` finally show "bv_to_nat bs < 2 ^ length bs" ``` skalberg@14494 ` 262` ``` by simp ``` skalberg@14494 ` 263` ``` qed ``` skalberg@14494 ` 264` ```qed ``` skalberg@14494 ` 265` skalberg@14494 ` 266` ```lemma [simp]: ``` skalberg@14494 ` 267` ``` assumes wn: "n \ length w" ``` skalberg@14494 ` 268` ``` shows "bv_extend n b w = w" ``` skalberg@14494 ` 269` ``` by (simp add: bv_extend_def wn) ``` skalberg@14494 ` 270` skalberg@14494 ` 271` ```lemma [simp]: ``` skalberg@14494 ` 272` ``` assumes wn: "length w < n" ``` skalberg@14494 ` 273` ``` shows "bv_extend n b w = bv_extend n b (b#w)" ``` skalberg@14494 ` 274` ```proof - ``` skalberg@14494 ` 275` ``` from wn ``` skalberg@14494 ` 276` ``` have s: "n - Suc (length w) + 1 = n - length w" ``` skalberg@14494 ` 277` ``` by arith ``` skalberg@14494 ` 278` ``` have "bv_extend n b w = replicate (n - length w) b @ w" ``` skalberg@14494 ` 279` ``` by (simp add: bv_extend_def) ``` skalberg@14494 ` 280` ``` also have "... = replicate (n - Suc (length w) + 1) b @ w" ``` skalberg@14494 ` 281` ``` by (subst s,rule) ``` skalberg@14494 ` 282` ``` also have "... = (replicate (n - Suc (length w)) b @ replicate 1 b) @ w" ``` skalberg@14494 ` 283` ``` by (subst replicate_add,rule) ``` skalberg@14494 ` 284` ``` also have "... = replicate (n - Suc (length w)) b @ b # w" ``` skalberg@14494 ` 285` ``` by simp ``` skalberg@14494 ` 286` ``` also have "... = bv_extend n b (b#w)" ``` skalberg@14494 ` 287` ``` by (simp add: bv_extend_def) ``` skalberg@14494 ` 288` ``` finally show "bv_extend n b w = bv_extend n b (b#w)" ``` skalberg@14494 ` 289` ``` . ``` skalberg@14494 ` 290` ```qed ``` skalberg@14494 ` 291` skalberg@14494 ` 292` ```consts ``` skalberg@14494 ` 293` ``` rem_initial :: "bit => bit list => bit list" ``` skalberg@14494 ` 294` skalberg@14494 ` 295` ```primrec ``` skalberg@14494 ` 296` ``` "rem_initial b [] = []" ``` skalberg@14494 ` 297` ``` "rem_initial b (x#xs) = (if b = x then rem_initial b xs else x#xs)" ``` skalberg@14494 ` 298` skalberg@14494 ` 299` ```lemma rem_initial_length: "length (rem_initial b w) \ length w" ``` skalberg@14494 ` 300` ``` by (rule bit_list_induct [of _ w],simp_all (no_asm),safe,simp_all) ``` skalberg@14494 ` 301` skalberg@14494 ` 302` ```lemma rem_initial_equal: ``` skalberg@14494 ` 303` ``` assumes p: "length (rem_initial b w) = length w" ``` skalberg@14494 ` 304` ``` shows "rem_initial b w = w" ``` skalberg@14494 ` 305` ```proof - ``` skalberg@14494 ` 306` ``` have "length (rem_initial b w) = length w --> rem_initial b w = w" ``` skalberg@14494 ` 307` ``` proof (induct w,simp_all,clarify) ``` skalberg@14494 ` 308` ``` fix xs ``` skalberg@14494 ` 309` ``` assume "length (rem_initial b xs) = length xs --> rem_initial b xs = xs" ``` skalberg@14494 ` 310` ``` assume f: "length (rem_initial b xs) = Suc (length xs)" ``` skalberg@14494 ` 311` ``` with rem_initial_length [of b xs] ``` skalberg@14494 ` 312` ``` show "rem_initial b xs = b#xs" ``` skalberg@14494 ` 313` ``` by auto ``` skalberg@14494 ` 314` ``` qed ``` skalberg@14494 ` 315` ``` thus ?thesis ``` skalberg@14494 ` 316` ``` .. ``` skalberg@14494 ` 317` ```qed ``` skalberg@14494 ` 318` skalberg@14494 ` 319` ```lemma bv_extend_rem_initial: "bv_extend (length w) b (rem_initial b w) = w" ``` skalberg@14494 ` 320` ```proof (induct w,simp_all,safe) ``` skalberg@14494 ` 321` ``` fix xs ``` skalberg@14494 ` 322` ``` assume ind: "bv_extend (length xs) b (rem_initial b xs) = xs" ``` skalberg@14494 ` 323` ``` from rem_initial_length [of b xs] ``` skalberg@14494 ` 324` ``` have [simp]: "Suc (length xs) - length (rem_initial b xs) = 1 + (length xs - length (rem_initial b xs))" ``` skalberg@14494 ` 325` ``` by arith ``` skalberg@14494 ` 326` ``` have "bv_extend (Suc (length xs)) b (rem_initial b xs) = replicate (Suc (length xs) - length (rem_initial b xs)) b @ (rem_initial b xs)" ``` skalberg@14494 ` 327` ``` by (simp add: bv_extend_def) ``` skalberg@14494 ` 328` ``` also have "... = replicate (1 + (length xs - length (rem_initial b xs))) b @ rem_initial b xs" ``` skalberg@14494 ` 329` ``` by simp ``` skalberg@14494 ` 330` ``` also have "... = (replicate 1 b @ replicate (length xs - length (rem_initial b xs)) b) @ rem_initial b xs" ``` skalberg@14494 ` 331` ``` by (subst replicate_add,rule refl) ``` skalberg@14494 ` 332` ``` also have "... = b # bv_extend (length xs) b (rem_initial b xs)" ``` skalberg@14494 ` 333` ``` by (auto simp add: bv_extend_def [symmetric]) ``` skalberg@14494 ` 334` ``` also have "... = b # xs" ``` skalberg@14494 ` 335` ``` by (simp add: ind) ``` skalberg@14494 ` 336` ``` finally show "bv_extend (Suc (length xs)) b (rem_initial b xs) = b # xs" ``` skalberg@14494 ` 337` ``` . ``` skalberg@14494 ` 338` ```qed ``` skalberg@14494 ` 339` skalberg@14494 ` 340` ```lemma rem_initial_append1: ``` skalberg@14494 ` 341` ``` assumes "rem_initial b xs ~= []" ``` skalberg@14494 ` 342` ``` shows "rem_initial b (xs @ ys) = rem_initial b xs @ ys" ``` skalberg@14494 ` 343` ```proof - ``` skalberg@14494 ` 344` ``` have "rem_initial b xs ~= [] --> rem_initial b (xs @ ys) = rem_initial b xs @ ys" (is "?P xs ys") ``` skalberg@14494 ` 345` ``` by (induct xs,auto) ``` skalberg@14494 ` 346` ``` thus ?thesis ``` skalberg@14494 ` 347` ``` .. ``` skalberg@14494 ` 348` ```qed ``` skalberg@14494 ` 349` skalberg@14494 ` 350` ```lemma rem_initial_append2: ``` skalberg@14494 ` 351` ``` assumes "rem_initial b xs = []" ``` skalberg@14494 ` 352` ``` shows "rem_initial b (xs @ ys) = rem_initial b ys" ``` skalberg@14494 ` 353` ```proof - ``` skalberg@14494 ` 354` ``` have "rem_initial b xs = [] --> rem_initial b (xs @ ys) = rem_initial b ys" (is "?P xs ys") ``` skalberg@14494 ` 355` ``` by (induct xs,auto) ``` skalberg@14494 ` 356` ``` thus ?thesis ``` skalberg@14494 ` 357` ``` .. ``` skalberg@14494 ` 358` ```qed ``` skalberg@14494 ` 359` skalberg@14494 ` 360` ```constdefs ``` skalberg@14494 ` 361` ``` norm_unsigned :: "bit list => bit list" ``` skalberg@14494 ` 362` ``` "norm_unsigned == rem_initial \" ``` skalberg@14494 ` 363` skalberg@14494 ` 364` ```lemma [simp]: "norm_unsigned [] = []" ``` skalberg@14494 ` 365` ``` by (simp add: norm_unsigned_def) ``` skalberg@14494 ` 366` skalberg@14494 ` 367` ```lemma [simp]: "norm_unsigned (\#bs) = norm_unsigned bs" ``` skalberg@14494 ` 368` ``` by (simp add: norm_unsigned_def) ``` skalberg@14494 ` 369` skalberg@14494 ` 370` ```lemma [simp]: "norm_unsigned (\#bs) = \#bs" ``` skalberg@14494 ` 371` ``` by (simp add: norm_unsigned_def) ``` skalberg@14494 ` 372` skalberg@14494 ` 373` ```lemma [simp]: "norm_unsigned (norm_unsigned w) = norm_unsigned w" ``` skalberg@14494 ` 374` ``` by (rule bit_list_induct [of _ w],simp_all) ``` skalberg@14494 ` 375` skalberg@14494 ` 376` ```consts ``` skalberg@14494 ` 377` ``` nat_to_bv_helper :: "int => bit list => bit list" ``` skalberg@14494 ` 378` skalberg@14494 ` 379` ```recdef nat_to_bv_helper "measure nat" ``` skalberg@14494 ` 380` ``` "nat_to_bv_helper n = (%bs. (if n \ 0 then bs ``` skalberg@14494 ` 381` ``` else nat_to_bv_helper (n div 2) ((if n mod 2 = 0 then \ else \)#bs)))" ``` skalberg@14494 ` 382` skalberg@14494 ` 383` ```constdefs ``` skalberg@14494 ` 384` ``` nat_to_bv :: "int => bit list" ``` skalberg@14494 ` 385` ``` "nat_to_bv n == nat_to_bv_helper n []" ``` skalberg@14494 ` 386` skalberg@14494 ` 387` ```lemma nat_to_bv0 [simp]: "nat_to_bv 0 = []" ``` skalberg@14494 ` 388` ``` by (simp add: nat_to_bv_def) ``` skalberg@14494 ` 389` skalberg@14494 ` 390` ```lemmas [simp del] = nat_to_bv_helper.simps ``` skalberg@14494 ` 391` skalberg@14494 ` 392` ```lemma n_div_2_cases: ``` skalberg@14494 ` 393` ``` assumes n0 : "0 \ n" ``` skalberg@14494 ` 394` ``` and zero: "(n::int) = 0 ==> R" ``` skalberg@14494 ` 395` ``` and div : "[| n div 2 < n ; 0 < n |] ==> R" ``` skalberg@14494 ` 396` ``` shows "R" ``` skalberg@14494 ` 397` ```proof (cases "n = 0") ``` skalberg@14494 ` 398` ``` assume "n = 0" ``` skalberg@14494 ` 399` ``` thus R ``` skalberg@14494 ` 400` ``` by (rule zero) ``` skalberg@14494 ` 401` ```next ``` skalberg@14494 ` 402` ``` assume "n ~= 0" ``` skalberg@14494 ` 403` ``` with n0 ``` skalberg@14494 ` 404` ``` have nn0: "0 < n" ``` skalberg@14494 ` 405` ``` by simp ``` skalberg@14494 ` 406` ``` hence "n div 2 < n" ``` skalberg@14494 ` 407` ``` by arith ``` skalberg@14494 ` 408` ``` from this and nn0 ``` skalberg@14494 ` 409` ``` show R ``` skalberg@14494 ` 410` ``` by (rule div) ``` skalberg@14494 ` 411` ```qed ``` skalberg@14494 ` 412` skalberg@14494 ` 413` ```lemma int_wf_ge_induct: ``` skalberg@14494 ` 414` ``` assumes base: "P (k::int)" ``` skalberg@14494 ` 415` ``` and ind : "!!i. (!!j. [| k \ j ; j < i |] ==> P j) ==> P i" ``` skalberg@14494 ` 416` ``` and valid: "k \ i" ``` skalberg@14494 ` 417` ``` shows "P i" ``` skalberg@14494 ` 418` ```proof - ``` skalberg@14494 ` 419` ``` have a: "\ j. k \ j \ j < i --> P j" ``` skalberg@14494 ` 420` ``` proof (rule int_ge_induct) ``` skalberg@14494 ` 421` ``` show "k \ i" ``` skalberg@14494 ` 422` ``` . ``` skalberg@14494 ` 423` ``` next ``` skalberg@14494 ` 424` ``` show "\ j. k \ j \ j < k --> P j" ``` skalberg@14494 ` 425` ``` by auto ``` skalberg@14494 ` 426` ``` next ``` skalberg@14494 ` 427` ``` fix i ``` skalberg@14494 ` 428` ``` assume "k \ i" ``` skalberg@14494 ` 429` ``` assume a: "\ j. k \ j \ j < i --> P j" ``` skalberg@14494 ` 430` ``` have pi: "P i" ``` skalberg@14494 ` 431` ``` proof (rule ind) ``` skalberg@14494 ` 432` ``` fix j ``` skalberg@14494 ` 433` ``` assume "k \ j" and "j < i" ``` skalberg@14494 ` 434` ``` with a ``` skalberg@14494 ` 435` ``` show "P j" ``` skalberg@14494 ` 436` ``` by auto ``` skalberg@14494 ` 437` ``` qed ``` skalberg@14494 ` 438` ``` show "\ j. k \ j \ j < i + 1 --> P j" ``` skalberg@14494 ` 439` ``` proof auto ``` skalberg@14494 ` 440` ``` fix j ``` skalberg@14494 ` 441` ``` assume kj: "k \ j" ``` skalberg@14494 ` 442` ``` assume ji: "j \ i" ``` skalberg@14494 ` 443` ``` show "P j" ``` skalberg@14494 ` 444` ``` proof (cases "j = i") ``` skalberg@14494 ` 445` ``` assume "j = i" ``` skalberg@14494 ` 446` ``` with pi ``` skalberg@14494 ` 447` ``` show "P j" ``` skalberg@14494 ` 448` ``` by simp ``` skalberg@14494 ` 449` ``` next ``` skalberg@14494 ` 450` ``` assume "j ~= i" ``` skalberg@14494 ` 451` ``` with ji ``` skalberg@14494 ` 452` ``` have "j < i" ``` skalberg@14494 ` 453` ``` by simp ``` skalberg@14494 ` 454` ``` with kj and a ``` skalberg@14494 ` 455` ``` show "P j" ``` skalberg@14494 ` 456` ``` by blast ``` skalberg@14494 ` 457` ``` qed ``` skalberg@14494 ` 458` ``` qed ``` skalberg@14494 ` 459` ``` qed ``` skalberg@14494 ` 460` ``` show "P i" ``` skalberg@14494 ` 461` ``` proof (rule ind) ``` skalberg@14494 ` 462` ``` fix j ``` skalberg@14494 ` 463` ``` assume "k \ j" and "j < i" ``` skalberg@14494 ` 464` ``` with a ``` skalberg@14494 ` 465` ``` show "P j" ``` skalberg@14494 ` 466` ``` by auto ``` skalberg@14494 ` 467` ``` qed ``` skalberg@14494 ` 468` ```qed ``` skalberg@14494 ` 469` skalberg@14494 ` 470` ```lemma unfold_nat_to_bv_helper: ``` skalberg@14494 ` 471` ``` "0 \ b ==> nat_to_bv_helper b l = nat_to_bv_helper b [] @ l" ``` skalberg@14494 ` 472` ```proof - ``` skalberg@14494 ` 473` ``` assume "0 \ b" ``` skalberg@14494 ` 474` ``` have "\l. nat_to_bv_helper b l = nat_to_bv_helper b [] @ l" ``` skalberg@14494 ` 475` ``` proof (rule int_wf_ge_induct [where ?i = b]) ``` skalberg@14494 ` 476` ``` show "0 \ b" ``` skalberg@14494 ` 477` ``` . ``` skalberg@14494 ` 478` ``` next ``` skalberg@14494 ` 479` ``` show "\ l. nat_to_bv_helper 0 l = nat_to_bv_helper 0 [] @ l" ``` skalberg@14494 ` 480` ``` by (simp add: nat_to_bv_helper.simps) ``` skalberg@14494 ` 481` ``` next ``` skalberg@14494 ` 482` ``` fix n ``` skalberg@14494 ` 483` ``` assume ind: "!!j. [| 0 \ j ; j < n |] ==> \ l. nat_to_bv_helper j l = nat_to_bv_helper j [] @ l" ``` skalberg@14494 ` 484` ``` show "\l. nat_to_bv_helper n l = nat_to_bv_helper n [] @ l" ``` skalberg@14494 ` 485` ``` proof ``` skalberg@14494 ` 486` ``` fix l ``` skalberg@14494 ` 487` ``` show "nat_to_bv_helper n l = nat_to_bv_helper n [] @ l" ``` skalberg@14494 ` 488` ``` proof (cases "n < 0") ``` skalberg@14494 ` 489` ``` assume "n < 0" ``` skalberg@14494 ` 490` ``` thus ?thesis ``` skalberg@14494 ` 491` ``` by (simp add: nat_to_bv_helper.simps) ``` skalberg@14494 ` 492` ``` next ``` skalberg@14494 ` 493` ``` assume "~n < 0" ``` skalberg@14494 ` 494` ``` show ?thesis ``` skalberg@14494 ` 495` ``` proof (rule n_div_2_cases [of n]) ``` skalberg@14494 ` 496` ``` from prems ``` skalberg@14494 ` 497` ``` show "0 \ n" ``` skalberg@14494 ` 498` ``` by simp ``` skalberg@14494 ` 499` ``` next ``` skalberg@14494 ` 500` ``` assume [simp]: "n = 0" ``` skalberg@14494 ` 501` ``` show ?thesis ``` skalberg@14494 ` 502` ``` apply (subst nat_to_bv_helper.simps [of n]) ``` skalberg@14494 ` 503` ``` apply simp ``` skalberg@14494 ` 504` ``` done ``` skalberg@14494 ` 505` ``` next ``` skalberg@14494 ` 506` ``` assume n2n: "n div 2 < n" ``` skalberg@14494 ` 507` ``` assume [simp]: "0 < n" ``` skalberg@14494 ` 508` ``` hence n20: "0 \ n div 2" ``` skalberg@14494 ` 509` ``` by arith ``` skalberg@14494 ` 510` ``` from ind [of "n div 2"] and n2n n20 ``` skalberg@14494 ` 511` ``` have ind': "\l. nat_to_bv_helper (n div 2) l = nat_to_bv_helper (n div 2) [] @ l" ``` skalberg@14494 ` 512` ``` by blast ``` skalberg@14494 ` 513` ``` show ?thesis ``` skalberg@14494 ` 514` ``` apply (subst nat_to_bv_helper.simps [of n]) ``` skalberg@14494 ` 515` ``` apply simp ``` skalberg@14494 ` 516` ``` apply (subst spec [OF ind',of "\#l"]) ``` skalberg@14494 ` 517` ``` apply (subst spec [OF ind',of "\#l"]) ``` skalberg@14494 ` 518` ``` apply (subst spec [OF ind',of "[\]"]) ``` skalberg@14494 ` 519` ``` apply (subst spec [OF ind',of "[\]"]) ``` skalberg@14494 ` 520` ``` apply simp ``` skalberg@14494 ` 521` ``` done ``` skalberg@14494 ` 522` ``` qed ``` skalberg@14494 ` 523` ``` qed ``` skalberg@14494 ` 524` ``` qed ``` skalberg@14494 ` 525` ``` qed ``` skalberg@14494 ` 526` ``` thus ?thesis ``` skalberg@14494 ` 527` ``` .. ``` skalberg@14494 ` 528` ```qed ``` skalberg@14494 ` 529` skalberg@14494 ` 530` ```lemma nat_to_bv_non0 [simp]: "0 < n ==> nat_to_bv n = nat_to_bv (n div 2) @ [if n mod 2 = 0 then \ else \]" ``` skalberg@14494 ` 531` ```proof - ``` skalberg@14494 ` 532` ``` assume [simp]: "0 < n" ``` skalberg@14494 ` 533` ``` show ?thesis ``` skalberg@14494 ` 534` ``` apply (subst nat_to_bv_def [of n]) ``` skalberg@14494 ` 535` ``` apply (subst nat_to_bv_helper.simps [of n]) ``` skalberg@14494 ` 536` ``` apply (subst unfold_nat_to_bv_helper) ``` skalberg@14494 ` 537` ``` using prems ``` skalberg@14494 ` 538` ``` apply arith ``` skalberg@14494 ` 539` ``` apply simp ``` skalberg@14494 ` 540` ``` apply (subst nat_to_bv_def [of "n div 2"]) ``` skalberg@14494 ` 541` ``` apply auto ``` skalberg@14494 ` 542` ``` using prems ``` skalberg@14494 ` 543` ``` apply auto ``` skalberg@14494 ` 544` ``` done ``` skalberg@14494 ` 545` ```qed ``` skalberg@14494 ` 546` skalberg@14494 ` 547` ```lemma bv_to_nat_dist_append: "bv_to_nat (l1 @ l2) = bv_to_nat l1 * 2 ^ length l2 + bv_to_nat l2" ``` skalberg@14494 ` 548` ```proof - ``` skalberg@14494 ` 549` ``` have "\l2. bv_to_nat (l1 @ l2) = bv_to_nat l1 * 2 ^ length l2 + bv_to_nat l2" ``` skalberg@14494 ` 550` ``` proof (induct l1,simp_all) ``` skalberg@14494 ` 551` ``` fix x xs ``` skalberg@14494 ` 552` ``` assume ind: "\l2. bv_to_nat (xs @ l2) = bv_to_nat xs * 2 ^ length l2 + bv_to_nat l2" ``` skalberg@14494 ` 553` ``` show "\l2. bitval x * 2 ^ (length xs + length l2) + bv_to_nat xs * 2 ^ length l2 = (bitval x * 2 ^ length xs + bv_to_nat xs) * 2 ^ length l2" ``` skalberg@14494 ` 554` ``` proof ``` skalberg@14494 ` 555` ``` fix l2 ``` skalberg@14494 ` 556` ``` show "bitval x * 2 ^ (length xs + length l2) + bv_to_nat xs * 2 ^ length l2 = (bitval x * 2 ^ length xs + bv_to_nat xs) * 2 ^ length l2" ``` skalberg@14494 ` 557` ``` proof - ``` skalberg@14494 ` 558` ``` have "(2::int) ^ (length xs + length l2) = 2 ^ length xs * 2 ^ length l2" ``` skalberg@14494 ` 559` ``` by (induct "length xs",simp_all) ``` skalberg@14494 ` 560` ``` hence "bitval x * 2 ^ (length xs + length l2) + bv_to_nat xs * 2 ^ length l2 = ``` skalberg@14494 ` 561` ``` bitval x * 2 ^ length xs * 2 ^ length l2 + bv_to_nat xs * 2 ^ length l2" ``` skalberg@14494 ` 562` ``` by simp ``` skalberg@14494 ` 563` ``` also have "... = (bitval x * 2 ^ length xs + bv_to_nat xs) * 2 ^ length l2" ``` skalberg@14494 ` 564` ``` by (simp add: ring_distrib) ``` skalberg@14494 ` 565` ``` finally show ?thesis . ``` skalberg@14494 ` 566` ``` qed ``` skalberg@14494 ` 567` ``` qed ``` skalberg@14494 ` 568` ``` qed ``` skalberg@14494 ` 569` ``` thus ?thesis ``` skalberg@14494 ` 570` ``` .. ``` skalberg@14494 ` 571` ```qed ``` skalberg@14494 ` 572` skalberg@14494 ` 573` ```lemma bv_nat_bv [simp]: ``` skalberg@14494 ` 574` ``` assumes n0: "0 \ n" ``` skalberg@14494 ` 575` ``` shows "bv_to_nat (nat_to_bv n) = n" ``` skalberg@14494 ` 576` ```proof - ``` skalberg@14494 ` 577` ``` have "0 \ n --> bv_to_nat (nat_to_bv n) = n" ``` skalberg@14494 ` 578` ``` proof (rule int_wf_ge_induct [where ?k = 0],simp_all,clarify) ``` skalberg@14494 ` 579` ``` fix n ``` skalberg@14494 ` 580` ``` assume ind: "!!j. [| 0 \ j; j < n |] ==> bv_to_nat (nat_to_bv j) = j" ``` skalberg@14494 ` 581` ``` assume n0: "0 \ n" ``` skalberg@14494 ` 582` ``` show "bv_to_nat (nat_to_bv n) = n" ``` skalberg@14494 ` 583` ``` proof (rule n_div_2_cases [of n]) ``` skalberg@14494 ` 584` ``` show "0 \ n" ``` skalberg@14494 ` 585` ``` . ``` skalberg@14494 ` 586` ``` next ``` skalberg@14494 ` 587` ``` assume [simp]: "n = 0" ``` skalberg@14494 ` 588` ``` show ?thesis ``` skalberg@14494 ` 589` ``` by simp ``` skalberg@14494 ` 590` ``` next ``` skalberg@14494 ` 591` ``` assume nn: "n div 2 < n" ``` skalberg@14494 ` 592` ``` assume n0: "0 < n" ``` skalberg@14494 ` 593` ``` hence n20: "0 \ n div 2" ``` skalberg@14494 ` 594` ``` by arith ``` skalberg@14494 ` 595` ``` from ind and n20 nn ``` skalberg@14494 ` 596` ``` have ind': "bv_to_nat (nat_to_bv (n div 2)) = n div 2" ``` skalberg@14494 ` 597` ``` by blast ``` skalberg@14494 ` 598` ``` from n0 have n0': "~ n \ 0" ``` skalberg@14494 ` 599` ``` by simp ``` skalberg@14494 ` 600` ``` show ?thesis ``` skalberg@14494 ` 601` ``` apply (subst nat_to_bv_def) ``` skalberg@14494 ` 602` ``` apply (subst nat_to_bv_helper.simps [of n]) ``` skalberg@14494 ` 603` ``` apply (simp add: n0' split del: split_if) ``` skalberg@14494 ` 604` ``` apply (subst unfold_nat_to_bv_helper) ``` skalberg@14494 ` 605` ``` apply (rule n20) ``` skalberg@14494 ` 606` ``` apply (subst bv_to_nat_dist_append) ``` skalberg@14494 ` 607` ``` apply (fold nat_to_bv_def) ``` skalberg@14494 ` 608` ``` apply (simp add: ind' split del: split_if) ``` skalberg@14494 ` 609` ``` apply (cases "n mod 2 = 0") ``` skalberg@14494 ` 610` ``` proof simp_all ``` skalberg@14494 ` 611` ``` assume "n mod 2 = 0" ``` skalberg@14494 ` 612` ``` with zmod_zdiv_equality [of n 2] ``` skalberg@14494 ` 613` ``` show "n div 2 * 2 = n" ``` skalberg@14494 ` 614` ``` by simp ``` skalberg@14494 ` 615` ``` next ``` skalberg@14494 ` 616` ``` assume "n mod 2 = 1" ``` skalberg@14494 ` 617` ``` with zmod_zdiv_equality [of n 2] ``` skalberg@14494 ` 618` ``` show "n div 2 * 2 + 1 = n" ``` skalberg@14494 ` 619` ``` by simp ``` skalberg@14494 ` 620` ``` qed ``` skalberg@14494 ` 621` ``` qed ``` skalberg@14494 ` 622` ``` qed ``` skalberg@14494 ` 623` ``` with n0 ``` skalberg@14494 ` 624` ``` show ?thesis ``` skalberg@14494 ` 625` ``` by auto ``` skalberg@14494 ` 626` ```qed ``` skalberg@14494 ` 627` skalberg@14494 ` 628` ```lemma [simp]: "bv_to_nat (norm_unsigned w) = bv_to_nat w" ``` skalberg@14494 ` 629` ``` by (rule bit_list_induct,simp_all) ``` skalberg@14494 ` 630` skalberg@14494 ` 631` ```lemma [simp]: "length (norm_unsigned w) \ length w" ``` skalberg@14494 ` 632` ``` by (rule bit_list_induct,simp_all) ``` skalberg@14494 ` 633` skalberg@14494 ` 634` ```lemma bv_to_nat_rew_msb: "bv_msb w = \ ==> bv_to_nat w = 2 ^ (length w - 1) + bv_to_nat (tl w)" ``` skalberg@14494 ` 635` ``` by (rule bit_list_cases [of w],simp_all) ``` skalberg@14494 ` 636` skalberg@14494 ` 637` ```lemma norm_unsigned_result: "norm_unsigned xs = [] \ bv_msb (norm_unsigned xs) = \" ``` skalberg@14494 ` 638` ```proof (rule length_induct [of _ xs]) ``` skalberg@14494 ` 639` ``` fix xs :: "bit list" ``` skalberg@14494 ` 640` ``` assume ind: "\ys. length ys < length xs --> norm_unsigned ys = [] \ bv_msb (norm_unsigned ys) = \" ``` skalberg@14494 ` 641` ``` show "norm_unsigned xs = [] \ bv_msb (norm_unsigned xs) = \" ``` skalberg@14494 ` 642` ``` proof (rule bit_list_cases [of xs],simp_all) ``` skalberg@14494 ` 643` ``` fix bs ``` skalberg@14494 ` 644` ``` assume [simp]: "xs = \#bs" ``` skalberg@14494 ` 645` ``` from ind ``` skalberg@14494 ` 646` ``` have "length bs < length xs --> norm_unsigned bs = [] \ bv_msb (norm_unsigned bs) = \" ``` skalberg@14494 ` 647` ``` .. ``` skalberg@14494 ` 648` ``` thus "norm_unsigned bs = [] \ bv_msb (norm_unsigned bs) = \" ``` skalberg@14494 ` 649` ``` by simp ``` skalberg@14494 ` 650` ``` qed ``` skalberg@14494 ` 651` ```qed ``` skalberg@14494 ` 652` skalberg@14494 ` 653` ```lemma norm_empty_bv_to_nat_zero: ``` skalberg@14494 ` 654` ``` assumes nw: "norm_unsigned w = []" ``` skalberg@14494 ` 655` ``` shows "bv_to_nat w = 0" ``` skalberg@14494 ` 656` ```proof - ``` skalberg@14494 ` 657` ``` have "bv_to_nat w = bv_to_nat (norm_unsigned w)" ``` skalberg@14494 ` 658` ``` by simp ``` skalberg@14494 ` 659` ``` also have "... = bv_to_nat []" ``` skalberg@14494 ` 660` ``` by (subst nw,rule) ``` skalberg@14494 ` 661` ``` also have "... = 0" ``` skalberg@14494 ` 662` ``` by simp ``` skalberg@14494 ` 663` ``` finally show ?thesis . ``` skalberg@14494 ` 664` ```qed ``` skalberg@14494 ` 665` skalberg@14494 ` 666` ```lemma bv_to_nat_lower_limit: ``` skalberg@14494 ` 667` ``` assumes w0: "0 < bv_to_nat w" ``` skalberg@14494 ` 668` ``` shows "2 ^ (length (norm_unsigned w) - 1) \ bv_to_nat w" ``` skalberg@14494 ` 669` ```proof - ``` skalberg@14494 ` 670` ``` from w0 and norm_unsigned_result [of w] ``` skalberg@14494 ` 671` ``` have msbw: "bv_msb (norm_unsigned w) = \" ``` skalberg@14494 ` 672` ``` by (auto simp add: norm_empty_bv_to_nat_zero) ``` skalberg@14494 ` 673` ``` have "2 ^ (length (norm_unsigned w) - 1) \ bv_to_nat (norm_unsigned w)" ``` skalberg@14494 ` 674` ``` by (subst bv_to_nat_rew_msb [OF msbw],simp) ``` skalberg@14494 ` 675` ``` thus ?thesis ``` skalberg@14494 ` 676` ``` by simp ``` skalberg@14494 ` 677` ```qed ``` skalberg@14494 ` 678` skalberg@14494 ` 679` ```lemmas [simp del] = nat_to_bv_non0 ``` skalberg@14494 ` 680` skalberg@14494 ` 681` ```lemma norm_unsigned_length [intro!]: "length (norm_unsigned w) \ length w" ``` skalberg@14494 ` 682` ``` by (subst norm_unsigned_def,rule rem_initial_length) ``` skalberg@14494 ` 683` skalberg@14494 ` 684` ```lemma norm_unsigned_equal: "length (norm_unsigned w) = length w ==> norm_unsigned w = w" ``` skalberg@14494 ` 685` ``` by (simp add: norm_unsigned_def,rule rem_initial_equal) ``` skalberg@14494 ` 686` skalberg@14494 ` 687` ```lemma bv_extend_norm_unsigned: "bv_extend (length w) \ (norm_unsigned w) = w" ``` skalberg@14494 ` 688` ``` by (simp add: norm_unsigned_def,rule bv_extend_rem_initial) ``` skalberg@14494 ` 689` skalberg@14494 ` 690` ```lemma norm_unsigned_append1 [simp]: "norm_unsigned xs \ [] ==> norm_unsigned (xs @ ys) = norm_unsigned xs @ ys" ``` skalberg@14494 ` 691` ``` by (simp add: norm_unsigned_def,rule rem_initial_append1) ``` skalberg@14494 ` 692` skalberg@14494 ` 693` ```lemma norm_unsigned_append2 [simp]: "norm_unsigned xs = [] ==> norm_unsigned (xs @ ys) = norm_unsigned ys" ``` skalberg@14494 ` 694` ``` by (simp add: norm_unsigned_def,rule rem_initial_append2) ``` skalberg@14494 ` 695` skalberg@14494 ` 696` ```lemma bv_to_nat_zero_imp_empty: ``` skalberg@14494 ` 697` ``` assumes "bv_to_nat w = 0" ``` skalberg@14494 ` 698` ``` shows "norm_unsigned w = []" ``` skalberg@14494 ` 699` ```proof - ``` skalberg@14494 ` 700` ``` have "bv_to_nat w = 0 --> norm_unsigned w = []" ``` skalberg@14494 ` 701` ``` apply (rule bit_list_induct [of _ w],simp_all) ``` skalberg@14494 ` 702` ``` apply (subgoal_tac "0 < 2 ^ length bs + bv_to_nat bs") ``` skalberg@14494 ` 703` ``` apply simp ``` skalberg@14494 ` 704` ``` apply (subgoal_tac "(0::int) < 2 ^ length bs") ``` skalberg@14494 ` 705` ``` apply (subgoal_tac "0 \ bv_to_nat bs") ``` skalberg@14494 ` 706` ``` apply arith ``` skalberg@14494 ` 707` ``` apply auto ``` skalberg@14494 ` 708` ``` done ``` skalberg@14494 ` 709` ``` thus ?thesis ``` skalberg@14494 ` 710` ``` .. ``` skalberg@14494 ` 711` ```qed ``` skalberg@14494 ` 712` skalberg@14494 ` 713` ```lemma bv_to_nat_nzero_imp_nempty: ``` skalberg@14494 ` 714` ``` assumes "bv_to_nat w \ 0" ``` skalberg@14494 ` 715` ``` shows "norm_unsigned w \ []" ``` skalberg@14494 ` 716` ```proof - ``` skalberg@14494 ` 717` ``` have "bv_to_nat w \ 0 --> norm_unsigned w \ []" ``` skalberg@14494 ` 718` ``` by (rule bit_list_induct [of _ w],simp_all) ``` skalberg@14494 ` 719` ``` thus ?thesis ``` skalberg@14494 ` 720` ``` .. ``` skalberg@14494 ` 721` ```qed ``` skalberg@14494 ` 722` skalberg@14494 ` 723` ```lemma nat_helper1: ``` skalberg@14494 ` 724` ``` assumes ass: "nat_to_bv (bv_to_nat w) = norm_unsigned w" ``` skalberg@14494 ` 725` ``` shows "nat_to_bv (2 * bv_to_nat w + bitval x) = norm_unsigned (w @ [x])" ``` skalberg@14494 ` 726` ```proof (cases x) ``` skalberg@14494 ` 727` ``` assume [simp]: "x = \" ``` skalberg@14494 ` 728` ``` show ?thesis ``` skalberg@14494 ` 729` ``` apply (simp add: nat_to_bv_non0) ``` skalberg@14494 ` 730` ``` apply safe ``` skalberg@14494 ` 731` ``` proof - ``` skalberg@14494 ` 732` ``` fix q ``` skalberg@14494 ` 733` ``` assume "(2 * bv_to_nat w) + 1 = 2 * q" ``` skalberg@14494 ` 734` ``` hence orig: "(2 * bv_to_nat w + 1) mod 2 = 2 * q mod 2" (is "?lhs = ?rhs") ``` skalberg@14494 ` 735` ``` by simp ``` skalberg@14494 ` 736` ``` have "?lhs = (1 + 2 * bv_to_nat w) mod 2" ``` skalberg@14494 ` 737` ``` by (simp add: add_commute) ``` skalberg@14494 ` 738` ``` also have "... = 1" ``` skalberg@14494 ` 739` ``` by (simp add: zmod_zadd1_eq) ``` skalberg@14494 ` 740` ``` finally have eq1: "?lhs = 1" . ``` skalberg@14494 ` 741` ``` have "?rhs = 0" ``` skalberg@14494 ` 742` ``` by simp ``` skalberg@14494 ` 743` ``` with orig and eq1 ``` skalberg@14494 ` 744` ``` have "(1::int) = 0" ``` skalberg@14494 ` 745` ``` by simp ``` skalberg@14494 ` 746` ``` thus "nat_to_bv ((2 * bv_to_nat w + 1) div 2) @ [\] = norm_unsigned (w @ [\])" ``` skalberg@14494 ` 747` ``` by simp ``` skalberg@14494 ` 748` ``` next ``` skalberg@14494 ` 749` ``` have "nat_to_bv ((2 * bv_to_nat w + 1) div 2) @ [\] = nat_to_bv ((1 + 2 * bv_to_nat w) div 2) @ [\]" ``` skalberg@14494 ` 750` ``` by (simp add: add_commute) ``` skalberg@14494 ` 751` ``` also have "... = nat_to_bv (bv_to_nat w) @ [\]" ``` skalberg@14494 ` 752` ``` by (subst zdiv_zadd1_eq,simp) ``` skalberg@14494 ` 753` ``` also have "... = norm_unsigned w @ [\]" ``` skalberg@14494 ` 754` ``` by (subst ass,rule refl) ``` skalberg@14494 ` 755` ``` also have "... = norm_unsigned (w @ [\])" ``` skalberg@14494 ` 756` ``` by (cases "norm_unsigned w",simp_all) ``` skalberg@14494 ` 757` ``` finally show "nat_to_bv ((2 * bv_to_nat w + 1) div 2) @ [\] = norm_unsigned (w @ [\])" ``` skalberg@14494 ` 758` ``` . ``` skalberg@14494 ` 759` ``` qed ``` skalberg@14494 ` 760` ```next ``` skalberg@14494 ` 761` ``` assume [simp]: "x = \" ``` skalberg@14494 ` 762` ``` show ?thesis ``` skalberg@14494 ` 763` ``` proof (cases "bv_to_nat w = 0") ``` skalberg@14494 ` 764` ``` assume "bv_to_nat w = 0" ``` skalberg@14494 ` 765` ``` thus ?thesis ``` skalberg@14494 ` 766` ``` by (simp add: bv_to_nat_zero_imp_empty) ``` skalberg@14494 ` 767` ``` next ``` skalberg@14494 ` 768` ``` assume "bv_to_nat w \ 0" ``` skalberg@14494 ` 769` ``` thus ?thesis ``` skalberg@14494 ` 770` ``` apply simp ``` skalberg@14494 ` 771` ``` apply (subst nat_to_bv_non0) ``` skalberg@14494 ` 772` ``` apply simp ``` skalberg@14494 ` 773` ``` apply auto ``` skalberg@14494 ` 774` ``` apply (cut_tac bv_to_nat_lower_range [of w]) ``` skalberg@14494 ` 775` ``` apply arith ``` skalberg@14494 ` 776` ``` apply (subst ass) ``` skalberg@14494 ` 777` ``` apply (cases "norm_unsigned w") ``` skalberg@14494 ` 778` ``` apply (simp_all add: norm_empty_bv_to_nat_zero) ``` skalberg@14494 ` 779` ``` done ``` skalberg@14494 ` 780` ``` qed ``` skalberg@14494 ` 781` ```qed ``` skalberg@14494 ` 782` skalberg@14494 ` 783` ```lemma nat_helper2: "nat_to_bv (2 ^ length xs + bv_to_nat xs) = \ # xs" ``` skalberg@14494 ` 784` ```proof - ``` skalberg@14494 ` 785` ``` have "\xs. nat_to_bv (2 ^ length (rev xs) + bv_to_nat (rev xs)) = \ # (rev xs)" (is "\xs. ?P xs") ``` skalberg@14494 ` 786` ``` proof ``` skalberg@14494 ` 787` ``` fix xs ``` skalberg@14494 ` 788` ``` show "?P xs" ``` skalberg@14494 ` 789` ``` proof (rule length_induct [of _ xs]) ``` skalberg@14494 ` 790` ``` fix xs :: "bit list" ``` skalberg@14494 ` 791` ``` assume ind: "\ys. length ys < length xs --> ?P ys" ``` skalberg@14494 ` 792` ``` show "?P xs" ``` skalberg@14494 ` 793` ``` proof (cases xs) ``` skalberg@14494 ` 794` ``` assume [simp]: "xs = []" ``` skalberg@14494 ` 795` ``` show ?thesis ``` skalberg@14494 ` 796` ``` by (simp add: nat_to_bv_non0) ``` skalberg@14494 ` 797` ``` next ``` skalberg@14494 ` 798` ``` fix y ys ``` skalberg@14494 ` 799` ``` assume [simp]: "xs = y # ys" ``` skalberg@14494 ` 800` ``` show ?thesis ``` skalberg@14494 ` 801` ``` apply simp ``` skalberg@14494 ` 802` ``` apply (subst bv_to_nat_dist_append) ``` skalberg@14494 ` 803` ``` apply simp ``` skalberg@14494 ` 804` ``` proof - ``` skalberg@14494 ` 805` ``` have "nat_to_bv (2 * 2 ^ length ys + (bv_to_nat (rev ys) * 2 + bitval y)) = ``` skalberg@14494 ` 806` ``` nat_to_bv (2 * (2 ^ length ys + bv_to_nat (rev ys)) + bitval y)" ``` skalberg@14494 ` 807` ``` by (simp add: add_ac mult_ac) ``` skalberg@14494 ` 808` ``` also have "... = nat_to_bv (2 * (bv_to_nat (\#rev ys)) + bitval y)" ``` skalberg@14494 ` 809` ``` by simp ``` skalberg@14494 ` 810` ``` also have "... = norm_unsigned (\#rev ys) @ [y]" ``` skalberg@14494 ` 811` ``` proof - ``` skalberg@14494 ` 812` ``` from ind ``` skalberg@14494 ` 813` ``` have "nat_to_bv (2 ^ length (rev ys) + bv_to_nat (rev ys)) = \ # rev ys" ``` skalberg@14494 ` 814` ``` by auto ``` skalberg@14494 ` 815` ``` hence [simp]: "nat_to_bv (2 ^ length ys + bv_to_nat (rev ys)) = \ # rev ys" ``` skalberg@14494 ` 816` ``` by simp ``` skalberg@14494 ` 817` ``` show ?thesis ``` skalberg@14494 ` 818` ``` apply (subst nat_helper1) ``` skalberg@14494 ` 819` ``` apply simp_all ``` skalberg@14494 ` 820` ``` done ``` skalberg@14494 ` 821` ``` qed ``` skalberg@14494 ` 822` ``` also have "... = (\#rev ys) @ [y]" ``` skalberg@14494 ` 823` ``` by simp ``` skalberg@14494 ` 824` ``` also have "... = \ # rev ys @ [y]" ``` skalberg@14494 ` 825` ``` by simp ``` skalberg@14494 ` 826` ``` finally show "nat_to_bv (2 * 2 ^ length ys + (bv_to_nat (rev ys) * 2 + bitval y)) = \ # rev ys @ [y]" ``` skalberg@14494 ` 827` ``` . ``` skalberg@14494 ` 828` ``` qed ``` skalberg@14494 ` 829` ``` qed ``` skalberg@14494 ` 830` ``` qed ``` skalberg@14494 ` 831` ``` qed ``` skalberg@14494 ` 832` ``` hence "nat_to_bv (2 ^ length (rev (rev xs)) + bv_to_nat (rev (rev xs))) = \ # rev (rev xs)" ``` skalberg@14494 ` 833` ``` .. ``` skalberg@14494 ` 834` ``` thus ?thesis ``` skalberg@14494 ` 835` ``` by simp ``` skalberg@14494 ` 836` ```qed ``` skalberg@14494 ` 837` skalberg@14494 ` 838` ```lemma nat_bv_nat [simp]: "nat_to_bv (bv_to_nat w) = norm_unsigned w" ``` skalberg@14494 ` 839` ```proof (rule bit_list_induct [of _ w],simp_all) ``` skalberg@14494 ` 840` ``` fix xs ``` skalberg@14494 ` 841` ``` assume "nat_to_bv (bv_to_nat xs) = norm_unsigned xs" ``` skalberg@14494 ` 842` ``` have "bv_to_nat xs = bv_to_nat (norm_unsigned xs)" ``` skalberg@14494 ` 843` ``` by simp ``` skalberg@14494 ` 844` ``` have "bv_to_nat xs < 2 ^ length xs" ``` skalberg@14494 ` 845` ``` by (rule bv_to_nat_upper_range) ``` skalberg@14494 ` 846` ``` show "nat_to_bv (2 ^ length xs + bv_to_nat xs) = \ # xs" ``` skalberg@14494 ` 847` ``` by (rule nat_helper2) ``` skalberg@14494 ` 848` ```qed ``` skalberg@14494 ` 849` skalberg@14494 ` 850` ```lemma [simp]: "bv_to_nat (norm_unsigned xs) = bv_to_nat xs" ``` skalberg@14494 ` 851` ``` by (rule bit_list_induct [of _ w],simp_all) ``` skalberg@14494 ` 852` skalberg@14494 ` 853` ```lemma bv_to_nat_qinj: ``` skalberg@14494 ` 854` ``` assumes one: "bv_to_nat xs = bv_to_nat ys" ``` skalberg@14494 ` 855` ``` and len: "length xs = length ys" ``` skalberg@14494 ` 856` ``` shows "xs = ys" ``` skalberg@14494 ` 857` ```proof - ``` skalberg@14494 ` 858` ``` from one ``` skalberg@14494 ` 859` ``` have "nat_to_bv (bv_to_nat xs) = nat_to_bv (bv_to_nat ys)" ``` skalberg@14494 ` 860` ``` by simp ``` skalberg@14494 ` 861` ``` hence xsys: "norm_unsigned xs = norm_unsigned ys" ``` skalberg@14494 ` 862` ``` by simp ``` skalberg@14494 ` 863` ``` have "xs = bv_extend (length xs) \ (norm_unsigned xs)" ``` skalberg@14494 ` 864` ``` by (simp add: bv_extend_norm_unsigned) ``` skalberg@14494 ` 865` ``` also have "... = bv_extend (length ys) \ (norm_unsigned ys)" ``` skalberg@14494 ` 866` ``` by (simp add: xsys len) ``` skalberg@14494 ` 867` ``` also have "... = ys" ``` skalberg@14494 ` 868` ``` by (simp add: bv_extend_norm_unsigned) ``` skalberg@14494 ` 869` ``` finally show ?thesis . ``` skalberg@14494 ` 870` ```qed ``` skalberg@14494 ` 871` skalberg@14494 ` 872` ```lemma norm_unsigned_nat_to_bv [simp]: ``` skalberg@14494 ` 873` ``` assumes [simp]: "0 \ n" ``` skalberg@14494 ` 874` ``` shows "norm_unsigned (nat_to_bv n) = nat_to_bv n" ``` skalberg@14494 ` 875` ```proof - ``` skalberg@14494 ` 876` ``` have "norm_unsigned (nat_to_bv n) = nat_to_bv (bv_to_nat (norm_unsigned (nat_to_bv n)))" ``` skalberg@14494 ` 877` ``` by (subst nat_bv_nat,simp) ``` skalberg@14494 ` 878` ``` also have "... = nat_to_bv n" ``` skalberg@14494 ` 879` ``` by simp ``` skalberg@14494 ` 880` ``` finally show ?thesis . ``` skalberg@14494 ` 881` ```qed ``` skalberg@14494 ` 882` skalberg@14494 ` 883` ```lemma length_nat_to_bv_upper_limit: ``` skalberg@14494 ` 884` ``` assumes nk: "n \ 2 ^ k - 1" ``` skalberg@14494 ` 885` ``` shows "length (nat_to_bv n) \ k" ``` skalberg@14494 ` 886` ```proof (cases "n \ 0") ``` skalberg@14494 ` 887` ``` assume "n \ 0" ``` skalberg@14494 ` 888` ``` thus ?thesis ``` skalberg@14494 ` 889` ``` by (simp add: nat_to_bv_def nat_to_bv_helper.simps) ``` skalberg@14494 ` 890` ```next ``` skalberg@14494 ` 891` ``` assume "~ n \ 0" ``` skalberg@14494 ` 892` ``` hence n0: "0 < n" ``` skalberg@14494 ` 893` ``` by simp ``` skalberg@14494 ` 894` ``` hence n00: "0 \ n" ``` skalberg@14494 ` 895` ``` by simp ``` skalberg@14494 ` 896` ``` show ?thesis ``` skalberg@14494 ` 897` ``` proof (rule ccontr) ``` skalberg@14494 ` 898` ``` assume "~ length (nat_to_bv n) \ k" ``` skalberg@14494 ` 899` ``` hence "k < length (nat_to_bv n)" ``` skalberg@14494 ` 900` ``` by simp ``` skalberg@14494 ` 901` ``` hence "k \ length (nat_to_bv n) - 1" ``` skalberg@14494 ` 902` ``` by arith ``` skalberg@14494 ` 903` ``` hence "(2::int) ^ k \ 2 ^ (length (nat_to_bv n) - 1)" ``` skalberg@14494 ` 904` ``` by simp ``` skalberg@14494 ` 905` ``` also have "... = 2 ^ (length (norm_unsigned (nat_to_bv n)) - 1)" ``` skalberg@14494 ` 906` ``` by (simp add: n00) ``` skalberg@14494 ` 907` ``` also have "... \ bv_to_nat (nat_to_bv n)" ``` skalberg@14494 ` 908` ``` by (rule bv_to_nat_lower_limit,simp add: n00 n0) ``` skalberg@14494 ` 909` ``` also have "... = n" ``` skalberg@14494 ` 910` ``` by (simp add: n00) ``` skalberg@14494 ` 911` ``` finally have "2 ^ k \ n" . ``` skalberg@14494 ` 912` ``` with n0 ``` skalberg@14494 ` 913` ``` have "2 ^ k - 1 < n" ``` skalberg@14494 ` 914` ``` by arith ``` skalberg@14494 ` 915` ``` with nk ``` skalberg@14494 ` 916` ``` show False ``` skalberg@14494 ` 917` ``` by simp ``` skalberg@14494 ` 918` ``` qed ``` skalberg@14494 ` 919` ```qed ``` skalberg@14494 ` 920` skalberg@14494 ` 921` ```lemma length_nat_to_bv_lower_limit: ``` skalberg@14494 ` 922` ``` assumes nk: "2 ^ k \ n" ``` skalberg@14494 ` 923` ``` shows "k < length (nat_to_bv n)" ``` skalberg@14494 ` 924` ```proof (rule ccontr) ``` skalberg@14494 ` 925` ``` have "(0::int) \ 2 ^ k" ``` skalberg@14494 ` 926` ``` by auto ``` skalberg@14494 ` 927` ``` with nk ``` skalberg@14494 ` 928` ``` have [simp]: "0 \ n" ``` skalberg@14494 ` 929` ``` by auto ``` skalberg@14494 ` 930` ``` assume "~ k < length (nat_to_bv n)" ``` skalberg@14494 ` 931` ``` hence lnk: "length (nat_to_bv n) \ k" ``` skalberg@14494 ` 932` ``` by simp ``` skalberg@14494 ` 933` ``` have "n = bv_to_nat (nat_to_bv n)" ``` skalberg@14494 ` 934` ``` by simp ``` skalberg@14494 ` 935` ``` also have "... < 2 ^ length (nat_to_bv n)" ``` skalberg@14494 ` 936` ``` by (rule bv_to_nat_upper_range) ``` skalberg@14494 ` 937` ``` also from lnk have "... \ 2 ^ k" ``` skalberg@14494 ` 938` ``` by simp ``` skalberg@14494 ` 939` ``` finally have "n < 2 ^ k" . ``` skalberg@14494 ` 940` ``` with nk ``` skalberg@14494 ` 941` ``` show False ``` skalberg@14494 ` 942` ``` by simp ``` skalberg@14494 ` 943` ```qed ``` skalberg@14494 ` 944` wenzelm@14589 ` 945` ```subsection {* Unsigned Arithmetic Operations *} ``` skalberg@14494 ` 946` skalberg@14494 ` 947` ```constdefs ``` skalberg@14494 ` 948` ``` bv_add :: "[bit list, bit list ] => bit list" ``` skalberg@14494 ` 949` ``` "bv_add w1 w2 == nat_to_bv (bv_to_nat w1 + bv_to_nat w2)" ``` skalberg@14494 ` 950` skalberg@14494 ` 951` ```lemma [simp]: "bv_add (norm_unsigned w1) w2 = bv_add w1 w2" ``` skalberg@14494 ` 952` ``` by (simp add: bv_add_def) ``` skalberg@14494 ` 953` skalberg@14494 ` 954` ```lemma [simp]: "bv_add w1 (norm_unsigned w2) = bv_add w1 w2" ``` skalberg@14494 ` 955` ``` by (simp add: bv_add_def) ``` skalberg@14494 ` 956` skalberg@14494 ` 957` ```lemma [simp]: "norm_unsigned (bv_add w1 w2) = bv_add w1 w2" ``` skalberg@14494 ` 958` ``` apply (simp add: bv_add_def) ``` skalberg@14494 ` 959` ``` apply (rule norm_unsigned_nat_to_bv) ``` skalberg@14494 ` 960` ``` apply (subgoal_tac "0 \ bv_to_nat w1") ``` skalberg@14494 ` 961` ``` apply (subgoal_tac "0 \ bv_to_nat w2") ``` skalberg@14494 ` 962` ``` apply arith ``` skalberg@14494 ` 963` ``` apply simp_all ``` skalberg@14494 ` 964` ``` done ``` skalberg@14494 ` 965` skalberg@14494 ` 966` ```lemma bv_add_length: "length (bv_add w1 w2) \ Suc (max (length w1) (length w2))" ``` skalberg@14494 ` 967` ```proof (unfold bv_add_def,rule length_nat_to_bv_upper_limit) ``` skalberg@14494 ` 968` ``` from bv_to_nat_upper_range [of w1] and bv_to_nat_upper_range [of w2] ``` skalberg@14494 ` 969` ``` have "bv_to_nat w1 + bv_to_nat w2 \ (2 ^ length w1 - 1) + (2 ^ length w2 - 1)" ``` skalberg@14494 ` 970` ``` by arith ``` skalberg@14494 ` 971` ``` also have "... \ max (2 ^ length w1 - 1) (2 ^ length w2 - 1) + max (2 ^ length w1 - 1) (2 ^ length w2 - 1)" ``` skalberg@14494 ` 972` ``` by (rule add_mono,safe intro!: le_maxI1 le_maxI2) ``` skalberg@14494 ` 973` ``` also have "... = 2 * max (2 ^ length w1 - 1) (2 ^ length w2 - 1)" ``` skalberg@14494 ` 974` ``` by simp ``` skalberg@14494 ` 975` ``` also have "... \ 2 ^ Suc (max (length w1) (length w2)) - 2" ``` skalberg@14494 ` 976` ``` proof (cases "length w1 \ length w2") ``` skalberg@14494 ` 977` ``` assume [simp]: "length w1 \ length w2" ``` skalberg@14494 ` 978` ``` hence "(2::int) ^ length w1 \ 2 ^ length w2" ``` skalberg@14494 ` 979` ``` by simp ``` skalberg@14494 ` 980` ``` hence [simp]: "(2::int) ^ length w1 - 1 \ 2 ^ length w2 - 1" ``` skalberg@14494 ` 981` ``` by arith ``` skalberg@14494 ` 982` ``` show ?thesis ``` skalberg@14494 ` 983` ``` by (simp split: split_max) ``` skalberg@14494 ` 984` ``` next ``` skalberg@14494 ` 985` ``` assume [simp]: "~ (length w1 \ length w2)" ``` skalberg@14494 ` 986` ``` have "~ ((2::int) ^ length w1 - 1 \ 2 ^ length w2 - 1)" ``` skalberg@14494 ` 987` ``` proof ``` skalberg@14494 ` 988` ``` assume "(2::int) ^ length w1 - 1 \ 2 ^ length w2 - 1" ``` skalberg@14494 ` 989` ``` hence "((2::int) ^ length w1 - 1) + 1 \ (2 ^ length w2 - 1) + 1" ``` skalberg@14494 ` 990` ``` by (rule add_right_mono) ``` skalberg@14494 ` 991` ``` hence "(2::int) ^ length w1 \ 2 ^ length w2" ``` skalberg@14494 ` 992` ``` by simp ``` skalberg@14494 ` 993` ``` hence "length w1 \ length w2" ``` skalberg@14494 ` 994` ``` by simp ``` skalberg@14494 ` 995` ``` thus False ``` skalberg@14494 ` 996` ``` by simp ``` skalberg@14494 ` 997` ``` qed ``` skalberg@14494 ` 998` ``` thus ?thesis ``` skalberg@14494 ` 999` ``` by (simp split: split_max) ``` skalberg@14494 ` 1000` ``` qed ``` skalberg@14494 ` 1001` ``` finally show "bv_to_nat w1 + bv_to_nat w2 \ 2 ^ Suc (max (length w1) (length w2)) - 1" ``` skalberg@14494 ` 1002` ``` by arith ``` skalberg@14494 ` 1003` ```qed ``` skalberg@14494 ` 1004` skalberg@14494 ` 1005` ```constdefs ``` skalberg@14494 ` 1006` ``` bv_mult :: "[bit list, bit list ] => bit list" ``` skalberg@14494 ` 1007` ``` "bv_mult w1 w2 == nat_to_bv (bv_to_nat w1 * bv_to_nat w2)" ``` skalberg@14494 ` 1008` skalberg@14494 ` 1009` ```lemma [simp]: "bv_mult (norm_unsigned w1) w2 = bv_mult w1 w2" ``` skalberg@14494 ` 1010` ``` by (simp add: bv_mult_def) ``` skalberg@14494 ` 1011` skalberg@14494 ` 1012` ```lemma [simp]: "bv_mult w1 (norm_unsigned w2) = bv_mult w1 w2" ``` skalberg@14494 ` 1013` ``` by (simp add: bv_mult_def) ``` skalberg@14494 ` 1014` skalberg@14494 ` 1015` ```lemma [simp]: "norm_unsigned (bv_mult w1 w2) = bv_mult w1 w2" ``` skalberg@14494 ` 1016` ``` apply (simp add: bv_mult_def) ``` skalberg@14494 ` 1017` ``` apply (rule norm_unsigned_nat_to_bv) ``` skalberg@14494 ` 1018` ``` apply (subgoal_tac "0 * 0 \ bv_to_nat w1 * bv_to_nat w2") ``` skalberg@14494 ` 1019` ``` apply simp ``` skalberg@14494 ` 1020` ``` apply (rule mult_mono,simp_all) ``` skalberg@14494 ` 1021` ``` done ``` skalberg@14494 ` 1022` skalberg@14494 ` 1023` ```lemma bv_mult_length: "length (bv_mult w1 w2) \ length w1 + length w2" ``` skalberg@14494 ` 1024` ```proof (unfold bv_mult_def,rule length_nat_to_bv_upper_limit) ``` skalberg@14494 ` 1025` ``` from bv_to_nat_upper_range [of w1] and bv_to_nat_upper_range [of w2] ``` skalberg@14494 ` 1026` ``` have h: "bv_to_nat w1 \ 2 ^ length w1 - 1 \ bv_to_nat w2 \ 2 ^ length w2 - 1" ``` skalberg@14494 ` 1027` ``` by arith ``` skalberg@14494 ` 1028` ``` have "bv_to_nat w1 * bv_to_nat w2 \ (2 ^ length w1 - 1) * (2 ^ length w2 - 1)" ``` skalberg@14494 ` 1029` ``` apply (cut_tac h) ``` skalberg@14494 ` 1030` ``` apply (rule mult_mono) ``` skalberg@14494 ` 1031` ``` apply auto ``` skalberg@14494 ` 1032` ``` done ``` skalberg@14494 ` 1033` ``` also have "... < 2 ^ length w1 * 2 ^ length w2" ``` skalberg@14494 ` 1034` ``` by (rule mult_strict_mono,auto) ``` skalberg@14494 ` 1035` ``` also have "... = 2 ^ (length w1 + length w2)" ``` skalberg@14494 ` 1036` ``` by (simp add: power_add) ``` skalberg@14494 ` 1037` ``` finally show "bv_to_nat w1 * bv_to_nat w2 \ 2 ^ (length w1 + length w2) - 1" ``` skalberg@14494 ` 1038` ``` by arith ``` skalberg@14494 ` 1039` ```qed ``` skalberg@14494 ` 1040` wenzelm@14589 ` 1041` ```subsection {* Signed Vectors *} ``` skalberg@14494 ` 1042` skalberg@14494 ` 1043` ```consts ``` skalberg@14494 ` 1044` ``` norm_signed :: "bit list => bit list" ``` skalberg@14494 ` 1045` skalberg@14494 ` 1046` ```primrec ``` skalberg@14494 ` 1047` ``` norm_signed_Nil: "norm_signed [] = []" ``` skalberg@14494 ` 1048` ``` norm_signed_Cons: "norm_signed (b#bs) = (case b of \ => if norm_unsigned bs = [] then [] else b#norm_unsigned bs | \ => b#rem_initial b bs)" ``` skalberg@14494 ` 1049` skalberg@14494 ` 1050` ```lemma [simp]: "norm_signed [\] = []" ``` skalberg@14494 ` 1051` ``` by simp ``` skalberg@14494 ` 1052` skalberg@14494 ` 1053` ```lemma [simp]: "norm_signed [\] = [\]" ``` skalberg@14494 ` 1054` ``` by simp ``` skalberg@14494 ` 1055` skalberg@14494 ` 1056` ```lemma [simp]: "norm_signed (\#\#xs) = \#\#xs" ``` skalberg@14494 ` 1057` ``` by simp ``` skalberg@14494 ` 1058` skalberg@14494 ` 1059` ```lemma [simp]: "norm_signed (\#\#xs) = norm_signed (\#xs)" ``` skalberg@14494 ` 1060` ``` by simp ``` skalberg@14494 ` 1061` skalberg@14494 ` 1062` ```lemma [simp]: "norm_signed (\#\#xs) = \#\#xs" ``` skalberg@14494 ` 1063` ``` by simp ``` skalberg@14494 ` 1064` skalberg@14494 ` 1065` ```lemma [simp]: "norm_signed (\#\#xs) = norm_signed (\#xs)" ``` skalberg@14494 ` 1066` ``` by simp ``` skalberg@14494 ` 1067` skalberg@14494 ` 1068` ```lemmas [simp del] = norm_signed_Cons ``` skalberg@14494 ` 1069` skalberg@14494 ` 1070` ```constdefs ``` skalberg@14494 ` 1071` ``` int_to_bv :: "int => bit list" ``` skalberg@14494 ` 1072` ``` "int_to_bv n == if 0 \ n ``` skalberg@14494 ` 1073` ``` then norm_signed (\#nat_to_bv n) ``` skalberg@14494 ` 1074` ``` else norm_signed (bv_not (\#nat_to_bv (-n- 1)))" ``` skalberg@14494 ` 1075` skalberg@14494 ` 1076` ```lemma int_to_bv_ge0 [simp]: "0 \ n ==> int_to_bv n = norm_signed (\ # nat_to_bv n)" ``` skalberg@14494 ` 1077` ``` by (simp add: int_to_bv_def) ``` skalberg@14494 ` 1078` skalberg@14494 ` 1079` ```lemma int_to_bv_lt0 [simp]: "n < 0 ==> int_to_bv n = norm_signed (bv_not (\#nat_to_bv (-n- 1)))" ``` skalberg@14494 ` 1080` ``` by (simp add: int_to_bv_def) ``` skalberg@14494 ` 1081` skalberg@14494 ` 1082` ```lemma [simp]: "norm_signed (norm_signed w) = norm_signed w" ``` skalberg@14494 ` 1083` ```proof (rule bit_list_induct [of _ w],simp_all) ``` skalberg@14494 ` 1084` ``` fix xs ``` skalberg@14494 ` 1085` ``` assume "norm_signed (norm_signed xs) = norm_signed xs" ``` skalberg@14494 ` 1086` ``` show "norm_signed (norm_signed (\#xs)) = norm_signed (\#xs)" ``` skalberg@14494 ` 1087` ``` proof (rule bit_list_cases [of xs],simp_all) ``` skalberg@14494 ` 1088` ``` fix ys ``` skalberg@14494 ` 1089` ``` assume [symmetric,simp]: "xs = \#ys" ``` skalberg@14494 ` 1090` ``` show "norm_signed (norm_signed (\#ys)) = norm_signed (\#ys)" ``` skalberg@14494 ` 1091` ``` by simp ``` skalberg@14494 ` 1092` ``` qed ``` skalberg@14494 ` 1093` ```next ``` skalberg@14494 ` 1094` ``` fix xs ``` skalberg@14494 ` 1095` ``` assume "norm_signed (norm_signed xs) = norm_signed xs" ``` skalberg@14494 ` 1096` ``` show "norm_signed (norm_signed (\#xs)) = norm_signed (\#xs)" ``` skalberg@14494 ` 1097` ``` proof (rule bit_list_cases [of xs],simp_all) ``` skalberg@14494 ` 1098` ``` fix ys ``` skalberg@14494 ` 1099` ``` assume [symmetric,simp]: "xs = \#ys" ``` skalberg@14494 ` 1100` ``` show "norm_signed (norm_signed (\#ys)) = norm_signed (\#ys)" ``` skalberg@14494 ` 1101` ``` by simp ``` skalberg@14494 ` 1102` ``` qed ``` skalberg@14494 ` 1103` ```qed ``` skalberg@14494 ` 1104` skalberg@14494 ` 1105` ```constdefs ``` skalberg@14494 ` 1106` ``` bv_to_int :: "bit list => int" ``` skalberg@14494 ` 1107` ``` "bv_to_int w == case bv_msb w of \ => bv_to_nat w | \ => -(bv_to_nat (bv_not w) + 1)" ``` skalberg@14494 ` 1108` skalberg@14494 ` 1109` ```lemma [simp]: "bv_to_int [] = 0" ``` skalberg@14494 ` 1110` ``` by (simp add: bv_to_int_def) ``` skalberg@14494 ` 1111` skalberg@14494 ` 1112` ```lemma [simp]: "bv_to_int (\#bs) = bv_to_nat bs" ``` skalberg@14494 ` 1113` ``` by (simp add: bv_to_int_def) ``` skalberg@14494 ` 1114` skalberg@14494 ` 1115` ```lemma [simp]: "bv_to_int (\#bs) = -(bv_to_nat (bv_not bs) + 1)" ``` skalberg@14494 ` 1116` ``` by (simp add: bv_to_int_def) ``` skalberg@14494 ` 1117` skalberg@14494 ` 1118` ```lemma [simp]: "bv_to_int (norm_signed w) = bv_to_int w" ``` skalberg@14494 ` 1119` ```proof (rule bit_list_induct [of _ w],simp_all) ``` skalberg@14494 ` 1120` ``` fix xs ``` skalberg@14494 ` 1121` ``` assume ind: "bv_to_int (norm_signed xs) = bv_to_int xs" ``` skalberg@14494 ` 1122` ``` show "bv_to_int (norm_signed (\#xs)) = bv_to_nat xs" ``` skalberg@14494 ` 1123` ``` proof (rule bit_list_cases [of xs],simp_all) ``` skalberg@14494 ` 1124` ``` fix ys ``` skalberg@14494 ` 1125` ``` assume [simp]: "xs = \#ys" ``` skalberg@14494 ` 1126` ``` from ind ``` skalberg@14494 ` 1127` ``` show "bv_to_int (norm_signed (\#ys)) = bv_to_nat ys" ``` skalberg@14494 ` 1128` ``` by simp ``` skalberg@14494 ` 1129` ``` qed ``` skalberg@14494 ` 1130` ```next ``` skalberg@14494 ` 1131` ``` fix xs ``` skalberg@14494 ` 1132` ``` assume ind: "bv_to_int (norm_signed xs) = bv_to_int xs" ``` skalberg@14494 ` 1133` ``` show "bv_to_int (norm_signed (\#xs)) = - bv_to_nat (bv_not xs) + -1" ``` skalberg@14494 ` 1134` ``` proof (rule bit_list_cases [of xs],simp_all) ``` skalberg@14494 ` 1135` ``` fix ys ``` skalberg@14494 ` 1136` ``` assume [simp]: "xs = \#ys" ``` skalberg@14494 ` 1137` ``` from ind ``` skalberg@14494 ` 1138` ``` show "bv_to_int (norm_signed (\#ys)) = - bv_to_nat (bv_not ys) + -1" ``` skalberg@14494 ` 1139` ``` by simp ``` skalberg@14494 ` 1140` ``` qed ``` skalberg@14494 ` 1141` ```qed ``` skalberg@14494 ` 1142` skalberg@14494 ` 1143` ```lemma bv_to_int_upper_range: "bv_to_int w < 2 ^ (length w - 1)" ``` skalberg@14494 ` 1144` ```proof (rule bit_list_cases [of w],simp_all) ``` skalberg@14494 ` 1145` ``` fix bs ``` skalberg@14494 ` 1146` ``` show "bv_to_nat bs < 2 ^ length bs" ``` skalberg@14494 ` 1147` ``` by (rule bv_to_nat_upper_range) ``` skalberg@14494 ` 1148` ```next ``` skalberg@14494 ` 1149` ``` fix bs ``` skalberg@14494 ` 1150` ``` have "- (bv_to_nat (bv_not bs)) + -1 \ 0 + 0" ``` skalberg@14494 ` 1151` ``` by (rule add_mono,simp_all) ``` skalberg@14494 ` 1152` ``` also have "... < 2 ^ length bs" ``` skalberg@14494 ` 1153` ``` by (induct bs,simp_all) ``` skalberg@14494 ` 1154` ``` finally show "- (bv_to_nat (bv_not bs)) + -1 < 2 ^ length bs" ``` skalberg@14494 ` 1155` ``` . ``` skalberg@14494 ` 1156` ```qed ``` skalberg@14494 ` 1157` skalberg@14494 ` 1158` ```lemma bv_to_int_lower_range: "- (2 ^ (length w - 1)) \ bv_to_int w" ``` skalberg@14494 ` 1159` ```proof (rule bit_list_cases [of w],simp_all) ``` skalberg@14494 ` 1160` ``` fix bs :: "bit list" ``` skalberg@14494 ` 1161` ``` have "- (2 ^ length bs) \ (0::int)" ``` skalberg@14494 ` 1162` ``` by (induct bs,simp_all) ``` skalberg@14494 ` 1163` ``` also have "... \ bv_to_nat bs" ``` skalberg@14494 ` 1164` ``` by simp ``` skalberg@14494 ` 1165` ``` finally show "- (2 ^ length bs) \ bv_to_nat bs" ``` skalberg@14494 ` 1166` ``` . ``` skalberg@14494 ` 1167` ```next ``` skalberg@14494 ` 1168` ``` fix bs ``` skalberg@14494 ` 1169` ``` from bv_to_nat_upper_range [of "bv_not bs"] ``` skalberg@14494 ` 1170` ``` have "bv_to_nat (bv_not bs) < 2 ^ length bs" ``` skalberg@14494 ` 1171` ``` by simp ``` skalberg@14494 ` 1172` ``` hence "bv_to_nat (bv_not bs) + 1 \ 2 ^ length bs" ``` skalberg@14494 ` 1173` ``` by simp ``` skalberg@14494 ` 1174` ``` thus "- (2 ^ length bs) \ - bv_to_nat (bv_not bs) + -1" ``` skalberg@14494 ` 1175` ``` by simp ``` skalberg@14494 ` 1176` ```qed ``` skalberg@14494 ` 1177` skalberg@14494 ` 1178` ```lemma int_bv_int [simp]: "int_to_bv (bv_to_int w) = norm_signed w" ``` skalberg@14494 ` 1179` ```proof (rule bit_list_cases [of w],simp) ``` skalberg@14494 ` 1180` ``` fix xs ``` skalberg@14494 ` 1181` ``` assume [simp]: "w = \#xs" ``` skalberg@14494 ` 1182` ``` show ?thesis ``` skalberg@14494 ` 1183` ``` apply simp ``` skalberg@14494 ` 1184` ``` apply (subst norm_signed_Cons [of "\" "xs"]) ``` skalberg@14494 ` 1185` ``` apply simp ``` skalberg@14494 ` 1186` ``` using norm_unsigned_result [of xs] ``` skalberg@14494 ` 1187` ``` apply safe ``` skalberg@14494 ` 1188` ``` apply (rule bit_list_cases [of "norm_unsigned xs"]) ``` skalberg@14494 ` 1189` ``` apply simp_all ``` skalberg@14494 ` 1190` ``` done ``` skalberg@14494 ` 1191` ```next ``` skalberg@14494 ` 1192` ``` fix xs ``` skalberg@14494 ` 1193` ``` assume [simp]: "w = \#xs" ``` skalberg@14494 ` 1194` ``` show ?thesis ``` skalberg@14494 ` 1195` ``` apply simp ``` skalberg@14494 ` 1196` ``` apply (rule bit_list_induct [of _ xs]) ``` skalberg@14494 ` 1197` ``` apply simp ``` skalberg@14494 ` 1198` ``` apply (subst int_to_bv_lt0) ``` skalberg@14494 ` 1199` ``` apply (subgoal_tac "- bv_to_nat (bv_not (\ # bs)) + -1 < 0 + 0") ``` skalberg@14494 ` 1200` ``` apply simp ``` skalberg@14494 ` 1201` ``` apply (rule add_le_less_mono) ``` skalberg@14494 ` 1202` ``` apply simp ``` skalberg@14494 ` 1203` ``` apply (rule order_trans [of _ 0]) ``` skalberg@14494 ` 1204` ``` apply simp ``` paulson@15067 ` 1205` ``` apply (rule zero_le_power,simp) ``` skalberg@14494 ` 1206` ``` apply simp ``` skalberg@14494 ` 1207` ``` apply simp ``` skalberg@14494 ` 1208` ``` apply (simp del: bv_to_nat1 bv_to_nat_helper) ``` skalberg@14494 ` 1209` ``` apply simp ``` skalberg@14494 ` 1210` ``` done ``` skalberg@14494 ` 1211` ```qed ``` skalberg@14494 ` 1212` skalberg@14494 ` 1213` ```lemma bv_int_bv [simp]: "bv_to_int (int_to_bv i) = i" ``` skalberg@14494 ` 1214` ``` by (cases "0 \ i",simp_all) ``` skalberg@14494 ` 1215` skalberg@14494 ` 1216` ```lemma bv_msb_norm [simp]: "bv_msb (norm_signed w) = bv_msb w" ``` skalberg@14494 ` 1217` ``` by (rule bit_list_cases [of w],simp_all add: norm_signed_Cons) ``` skalberg@14494 ` 1218` skalberg@14494 ` 1219` ```lemma norm_signed_length: "length (norm_signed w) \ length w" ``` skalberg@14494 ` 1220` ``` apply (cases w,simp_all) ``` skalberg@14494 ` 1221` ``` apply (subst norm_signed_Cons) ``` skalberg@14494 ` 1222` ``` apply (case_tac "a",simp_all) ``` skalberg@14494 ` 1223` ``` apply (rule rem_initial_length) ``` skalberg@14494 ` 1224` ``` done ``` skalberg@14494 ` 1225` skalberg@14494 ` 1226` ```lemma norm_signed_equal: "length (norm_signed w) = length w ==> norm_signed w = w" ``` skalberg@14494 ` 1227` ```proof (rule bit_list_cases [of w],simp_all) ``` skalberg@14494 ` 1228` ``` fix xs ``` skalberg@14494 ` 1229` ``` assume "length (norm_signed (\#xs)) = Suc (length xs)" ``` skalberg@14494 ` 1230` ``` thus "norm_signed (\#xs) = \#xs" ``` skalberg@14494 ` 1231` ``` apply (simp add: norm_signed_Cons) ``` skalberg@14494 ` 1232` ``` apply safe ``` skalberg@14494 ` 1233` ``` apply simp_all ``` skalberg@14494 ` 1234` ``` apply (rule norm_unsigned_equal) ``` skalberg@14494 ` 1235` ``` apply assumption ``` skalberg@14494 ` 1236` ``` done ``` skalberg@14494 ` 1237` ```next ``` skalberg@14494 ` 1238` ``` fix xs ``` skalberg@14494 ` 1239` ``` assume "length (norm_signed (\#xs)) = Suc (length xs)" ``` skalberg@14494 ` 1240` ``` thus "norm_signed (\#xs) = \#xs" ``` skalberg@14494 ` 1241` ``` apply (simp add: norm_signed_Cons) ``` skalberg@14494 ` 1242` ``` apply (rule rem_initial_equal) ``` skalberg@14494 ` 1243` ``` apply assumption ``` skalberg@14494 ` 1244` ``` done ``` skalberg@14494 ` 1245` ```qed ``` skalberg@14494 ` 1246` skalberg@14494 ` 1247` ```lemma bv_extend_norm_signed: "bv_msb w = b ==> bv_extend (length w) b (norm_signed w) = w" ``` skalberg@14494 ` 1248` ```proof (rule bit_list_cases [of w],simp_all) ``` skalberg@14494 ` 1249` ``` fix xs ``` skalberg@14494 ` 1250` ``` show "bv_extend (Suc (length xs)) \ (norm_signed (\#xs)) = \#xs" ``` skalberg@14494 ` 1251` ``` proof (simp add: norm_signed_list_def,auto) ``` skalberg@14494 ` 1252` ``` assume "norm_unsigned xs = []" ``` skalberg@14494 ` 1253` ``` hence xx: "rem_initial \ xs = []" ``` skalberg@14494 ` 1254` ``` by (simp add: norm_unsigned_def) ``` skalberg@14494 ` 1255` ``` have "bv_extend (Suc (length xs)) \ (\#rem_initial \ xs) = \#xs" ``` skalberg@14494 ` 1256` ``` apply (simp add: bv_extend_def replicate_app_Cons_same) ``` skalberg@14494 ` 1257` ``` apply (fold bv_extend_def) ``` skalberg@14494 ` 1258` ``` apply (rule bv_extend_rem_initial) ``` skalberg@14494 ` 1259` ``` done ``` skalberg@14494 ` 1260` ``` thus "bv_extend (Suc (length xs)) \ [\] = \#xs" ``` skalberg@14494 ` 1261` ``` by (simp add: xx) ``` skalberg@14494 ` 1262` ``` next ``` skalberg@14494 ` 1263` ``` show "bv_extend (Suc (length xs)) \ (\#norm_unsigned xs) = \#xs" ``` skalberg@14494 ` 1264` ``` apply (simp add: norm_unsigned_def) ``` skalberg@14494 ` 1265` ``` apply (simp add: bv_extend_def replicate_app_Cons_same) ``` skalberg@14494 ` 1266` ``` apply (fold bv_extend_def) ``` skalberg@14494 ` 1267` ``` apply (rule bv_extend_rem_initial) ``` skalberg@14494 ` 1268` ``` done ``` skalberg@14494 ` 1269` ``` qed ``` skalberg@14494 ` 1270` ```next ``` skalberg@14494 ` 1271` ``` fix xs ``` skalberg@14494 ` 1272` ``` show "bv_extend (Suc (length xs)) \ (norm_signed (\#xs)) = \#xs" ``` skalberg@14494 ` 1273` ``` apply (simp add: norm_signed_Cons) ``` skalberg@14494 ` 1274` ``` apply (simp add: bv_extend_def replicate_app_Cons_same) ``` skalberg@14494 ` 1275` ``` apply (fold bv_extend_def) ``` skalberg@14494 ` 1276` ``` apply (rule bv_extend_rem_initial) ``` skalberg@14494 ` 1277` ``` done ``` skalberg@14494 ` 1278` ```qed ``` skalberg@14494 ` 1279` skalberg@14494 ` 1280` ```lemma bv_to_int_qinj: ``` skalberg@14494 ` 1281` ``` assumes one: "bv_to_int xs = bv_to_int ys" ``` skalberg@14494 ` 1282` ``` and len: "length xs = length ys" ``` skalberg@14494 ` 1283` ``` shows "xs = ys" ``` skalberg@14494 ` 1284` ```proof - ``` skalberg@14494 ` 1285` ``` from one ``` skalberg@14494 ` 1286` ``` have "int_to_bv (bv_to_int xs) = int_to_bv (bv_to_int ys)" ``` skalberg@14494 ` 1287` ``` by simp ``` skalberg@14494 ` 1288` ``` hence xsys: "norm_signed xs = norm_signed ys" ``` skalberg@14494 ` 1289` ``` by simp ``` skalberg@14494 ` 1290` ``` hence xsys': "bv_msb xs = bv_msb ys" ``` skalberg@14494 ` 1291` ``` proof - ``` skalberg@14494 ` 1292` ``` have "bv_msb xs = bv_msb (norm_signed xs)" ``` skalberg@14494 ` 1293` ``` by simp ``` skalberg@14494 ` 1294` ``` also have "... = bv_msb (norm_signed ys)" ``` skalberg@14494 ` 1295` ``` by (simp add: xsys) ``` skalberg@14494 ` 1296` ``` also have "... = bv_msb ys" ``` skalberg@14494 ` 1297` ``` by simp ``` skalberg@14494 ` 1298` ``` finally show ?thesis . ``` skalberg@14494 ` 1299` ``` qed ``` skalberg@14494 ` 1300` ``` have "xs = bv_extend (length xs) (bv_msb xs) (norm_signed xs)" ``` skalberg@14494 ` 1301` ``` by (simp add: bv_extend_norm_signed) ``` skalberg@14494 ` 1302` ``` also have "... = bv_extend (length ys) (bv_msb ys) (norm_signed ys)" ``` skalberg@14494 ` 1303` ``` by (simp add: xsys xsys' len) ``` skalberg@14494 ` 1304` ``` also have "... = ys" ``` skalberg@14494 ` 1305` ``` by (simp add: bv_extend_norm_signed) ``` skalberg@14494 ` 1306` ``` finally show ?thesis . ``` skalberg@14494 ` 1307` ```qed ``` skalberg@14494 ` 1308` skalberg@14494 ` 1309` ```lemma [simp]: "norm_signed (int_to_bv w) = int_to_bv w" ``` skalberg@14494 ` 1310` ``` by (simp add: int_to_bv_def) ``` skalberg@14494 ` 1311` skalberg@14494 ` 1312` ```lemma bv_to_int_msb0: "0 \ bv_to_int w1 ==> bv_msb w1 = \" ``` skalberg@14494 ` 1313` ``` apply (rule bit_list_cases,simp_all) ``` skalberg@14494 ` 1314` ``` apply (subgoal_tac "0 \ bv_to_nat (bv_not bs)") ``` skalberg@14494 ` 1315` ``` apply simp_all ``` skalberg@14494 ` 1316` ``` done ``` skalberg@14494 ` 1317` skalberg@14494 ` 1318` ```lemma bv_to_int_msb1: "bv_to_int w1 < 0 ==> bv_msb w1 = \" ``` skalberg@14494 ` 1319` ``` apply (rule bit_list_cases,simp_all) ``` skalberg@14494 ` 1320` ``` apply (subgoal_tac "0 \ bv_to_nat bs") ``` skalberg@14494 ` 1321` ``` apply simp_all ``` skalberg@14494 ` 1322` ``` done ``` skalberg@14494 ` 1323` skalberg@14494 ` 1324` ```lemma bv_to_int_lower_limit_gt0: ``` skalberg@14494 ` 1325` ``` assumes w0: "0 < bv_to_int w" ``` skalberg@14494 ` 1326` ``` shows "2 ^ (length (norm_signed w) - 2) \ bv_to_int w" ``` skalberg@14494 ` 1327` ```proof - ``` skalberg@14494 ` 1328` ``` from w0 ``` skalberg@14494 ` 1329` ``` have "0 \ bv_to_int w" ``` skalberg@14494 ` 1330` ``` by simp ``` skalberg@14494 ` 1331` ``` hence [simp]: "bv_msb w = \" ``` skalberg@14494 ` 1332` ``` by (rule bv_to_int_msb0) ``` skalberg@14494 ` 1333` ``` have "2 ^ (length (norm_signed w) - 2) \ bv_to_int (norm_signed w)" ``` skalberg@14494 ` 1334` ``` proof (rule bit_list_cases [of w]) ``` skalberg@14494 ` 1335` ``` assume "w = []" ``` skalberg@14494 ` 1336` ``` with w0 ``` skalberg@14494 ` 1337` ``` show ?thesis ``` skalberg@14494 ` 1338` ``` by simp ``` skalberg@14494 ` 1339` ``` next ``` skalberg@14494 ` 1340` ``` fix w' ``` skalberg@14494 ` 1341` ``` assume weq: "w = \ # w'" ``` skalberg@14494 ` 1342` ``` thus ?thesis ``` skalberg@14494 ` 1343` ``` proof (simp add: norm_signed_Cons,safe) ``` skalberg@14494 ` 1344` ``` assume "norm_unsigned w' = []" ``` skalberg@14494 ` 1345` ``` with weq and w0 ``` skalberg@14494 ` 1346` ``` show False ``` skalberg@14494 ` 1347` ``` by (simp add: norm_empty_bv_to_nat_zero) ``` skalberg@14494 ` 1348` ``` next ``` skalberg@14494 ` 1349` ``` assume w'0: "norm_unsigned w' \ []" ``` skalberg@14494 ` 1350` ``` have "0 < bv_to_nat w'" ``` skalberg@14494 ` 1351` ``` proof (rule ccontr) ``` skalberg@14494 ` 1352` ``` assume "~ (0 < bv_to_nat w')" ``` skalberg@14494 ` 1353` ``` with bv_to_nat_lower_range [of w'] ``` skalberg@14494 ` 1354` ``` have "bv_to_nat w' = 0" ``` skalberg@14494 ` 1355` ``` by arith ``` skalberg@14494 ` 1356` ``` hence "norm_unsigned w' = []" ``` skalberg@14494 ` 1357` ``` by (simp add: bv_to_nat_zero_imp_empty) ``` skalberg@14494 ` 1358` ``` with w'0 ``` skalberg@14494 ` 1359` ``` show False ``` skalberg@14494 ` 1360` ``` by simp ``` skalberg@14494 ` 1361` ``` qed ``` skalberg@14494 ` 1362` ``` with bv_to_nat_lower_limit [of w'] ``` skalberg@14494 ` 1363` ``` have "2 ^ (length (norm_unsigned w') - 1) \ bv_to_nat w'" ``` skalberg@14494 ` 1364` ``` . ``` skalberg@14494 ` 1365` ``` thus "2 ^ (length (norm_unsigned w') - Suc 0) \ bv_to_nat w'" ``` skalberg@14494 ` 1366` ``` by simp ``` skalberg@14494 ` 1367` ``` qed ``` skalberg@14494 ` 1368` ``` next ``` skalberg@14494 ` 1369` ``` fix w' ``` skalberg@14494 ` 1370` ``` assume "w = \ # w'" ``` skalberg@14494 ` 1371` ``` from w0 ``` skalberg@14494 ` 1372` ``` have "bv_msb w = \" ``` skalberg@14494 ` 1373` ``` by simp ``` skalberg@14494 ` 1374` ``` with prems ``` skalberg@14494 ` 1375` ``` show ?thesis ``` skalberg@14494 ` 1376` ``` by simp ``` skalberg@14494 ` 1377` ``` qed ``` skalberg@14494 ` 1378` ``` also have "... = bv_to_int w" ``` skalberg@14494 ` 1379` ``` by simp ``` skalberg@14494 ` 1380` ``` finally show ?thesis . ``` skalberg@14494 ` 1381` ```qed ``` skalberg@14494 ` 1382` skalberg@14494 ` 1383` ```lemma norm_signed_result: "norm_signed w = [] \ norm_signed w = [\] \ bv_msb (norm_signed w) \ bv_msb (tl (norm_signed w))" ``` skalberg@14494 ` 1384` ``` apply (rule bit_list_cases [of w],simp_all) ``` skalberg@14494 ` 1385` ``` apply (case_tac "bs",simp_all) ``` skalberg@14494 ` 1386` ``` apply (case_tac "a",simp_all) ``` skalberg@14494 ` 1387` ``` apply (simp add: norm_signed_Cons) ``` skalberg@14494 ` 1388` ``` apply safe ``` skalberg@14494 ` 1389` ``` apply simp ``` skalberg@14494 ` 1390` ```proof - ``` skalberg@14494 ` 1391` ``` fix l ``` skalberg@14494 ` 1392` ``` assume msb: "\ = bv_msb (norm_unsigned l)" ``` skalberg@14494 ` 1393` ``` assume "norm_unsigned l \ []" ``` skalberg@14494 ` 1394` ``` with norm_unsigned_result [of l] ``` skalberg@14494 ` 1395` ``` have "bv_msb (norm_unsigned l) = \" ``` skalberg@14494 ` 1396` ``` by simp ``` skalberg@14494 ` 1397` ``` with msb ``` skalberg@14494 ` 1398` ``` show False ``` skalberg@14494 ` 1399` ``` by simp ``` skalberg@14494 ` 1400` ```next ``` skalberg@14494 ` 1401` ``` fix xs ``` skalberg@14494 ` 1402` ``` assume p: "\ = bv_msb (tl (norm_signed (\ # xs)))" ``` skalberg@14494 ` 1403` ``` have "\ \ bv_msb (tl (norm_signed (\ # xs)))" ``` skalberg@14494 ` 1404` ``` by (rule bit_list_induct [of _ xs],simp_all) ``` skalberg@14494 ` 1405` ``` with p ``` skalberg@14494 ` 1406` ``` show False ``` skalberg@14494 ` 1407` ``` by simp ``` skalberg@14494 ` 1408` ```qed ``` skalberg@14494 ` 1409` skalberg@14494 ` 1410` ```lemma bv_to_int_upper_limit_lem1: ``` skalberg@14494 ` 1411` ``` assumes w0: "bv_to_int w < -1" ``` skalberg@14494 ` 1412` ``` shows "bv_to_int w < - (2 ^ (length (norm_signed w) - 2))" ``` skalberg@14494 ` 1413` ```proof - ``` skalberg@14494 ` 1414` ``` from w0 ``` skalberg@14494 ` 1415` ``` have "bv_to_int w < 0" ``` skalberg@14494 ` 1416` ``` by simp ``` skalberg@14494 ` 1417` ``` hence msbw [simp]: "bv_msb w = \" ``` skalberg@14494 ` 1418` ``` by (rule bv_to_int_msb1) ``` skalberg@14494 ` 1419` ``` have "bv_to_int w = bv_to_int (norm_signed w)" ``` skalberg@14494 ` 1420` ``` by simp ``` skalberg@14494 ` 1421` ``` also from norm_signed_result [of w] ``` skalberg@14494 ` 1422` ``` have "... < - (2 ^ (length (norm_signed w) - 2))" ``` skalberg@14494 ` 1423` ``` proof (safe) ``` skalberg@14494 ` 1424` ``` assume "norm_signed w = []" ``` skalberg@14494 ` 1425` ``` hence "bv_to_int (norm_signed w) = 0" ``` skalberg@14494 ` 1426` ``` by simp ``` skalberg@14494 ` 1427` ``` with w0 ``` skalberg@14494 ` 1428` ``` show ?thesis ``` skalberg@14494 ` 1429` ``` by simp ``` skalberg@14494 ` 1430` ``` next ``` skalberg@14494 ` 1431` ``` assume "norm_signed w = [\]" ``` skalberg@14494 ` 1432` ``` hence "bv_to_int (norm_signed w) = -1" ``` skalberg@14494 ` 1433` ``` by simp ``` skalberg@14494 ` 1434` ``` with w0 ``` skalberg@14494 ` 1435` ``` show ?thesis ``` skalberg@14494 ` 1436` ``` by simp ``` skalberg@14494 ` 1437` ``` next ``` skalberg@14494 ` 1438` ``` assume "bv_msb (norm_signed w) \ bv_msb (tl (norm_signed w))" ``` skalberg@14494 ` 1439` ``` hence msb_tl: "\ \ bv_msb (tl (norm_signed w))" ``` skalberg@14494 ` 1440` ``` by simp ``` skalberg@14494 ` 1441` ``` show "bv_to_int (norm_signed w) < - (2 ^ (length (norm_signed w) - 2))" ``` skalberg@14494 ` 1442` ``` proof (rule bit_list_cases [of "norm_signed w"]) ``` skalberg@14494 ` 1443` ``` assume "norm_signed w = []" ``` skalberg@14494 ` 1444` ``` hence "bv_to_int (norm_signed w) = 0" ``` skalberg@14494 ` 1445` ``` by simp ``` skalberg@14494 ` 1446` ``` with w0 ``` skalberg@14494 ` 1447` ``` show ?thesis ``` skalberg@14494 ` 1448` ``` by simp ``` skalberg@14494 ` 1449` ``` next ``` skalberg@14494 ` 1450` ``` fix w' ``` skalberg@14494 ` 1451` ``` assume nw: "norm_signed w = \ # w'" ``` skalberg@14494 ` 1452` ``` from msbw ``` skalberg@14494 ` 1453` ``` have "bv_msb (norm_signed w) = \" ``` skalberg@14494 ` 1454` ``` by simp ``` skalberg@14494 ` 1455` ``` with nw ``` skalberg@14494 ` 1456` ``` show ?thesis ``` skalberg@14494 ` 1457` ``` by simp ``` skalberg@14494 ` 1458` ``` next ``` skalberg@14494 ` 1459` ``` fix w' ``` skalberg@14494 ` 1460` ``` assume weq: "norm_signed w = \ # w'" ``` skalberg@14494 ` 1461` ``` show ?thesis ``` skalberg@14494 ` 1462` ``` proof (rule bit_list_cases [of w']) ``` skalberg@14494 ` 1463` ``` assume w'eq: "w' = []" ``` skalberg@14494 ` 1464` ``` from w0 ``` skalberg@14494 ` 1465` ``` have "bv_to_int (norm_signed w) < -1" ``` skalberg@14494 ` 1466` ``` by simp ``` skalberg@14494 ` 1467` ``` with w'eq and weq ``` skalberg@14494 ` 1468` ``` show ?thesis ``` skalberg@14494 ` 1469` ``` by simp ``` skalberg@14494 ` 1470` ``` next ``` skalberg@14494 ` 1471` ``` fix w'' ``` skalberg@14494 ` 1472` ``` assume w'eq: "w' = \ # w''" ``` skalberg@14494 ` 1473` ``` show ?thesis ``` skalberg@14494 ` 1474` ``` apply (simp add: weq w'eq) ``` skalberg@14494 ` 1475` ``` apply (subgoal_tac "-bv_to_nat (bv_not w'') + -1 < 0 + 0") ``` skalberg@14494 ` 1476` ``` apply simp ``` skalberg@14494 ` 1477` ``` apply (rule add_le_less_mono) ``` skalberg@14494 ` 1478` ``` apply simp_all ``` skalberg@14494 ` 1479` ``` done ``` skalberg@14494 ` 1480` ``` next ``` skalberg@14494 ` 1481` ``` fix w'' ``` skalberg@14494 ` 1482` ``` assume w'eq: "w' = \ # w''" ``` skalberg@14494 ` 1483` ``` with weq and msb_tl ``` skalberg@14494 ` 1484` ``` show ?thesis ``` skalberg@14494 ` 1485` ``` by simp ``` skalberg@14494 ` 1486` ``` qed ``` skalberg@14494 ` 1487` ``` qed ``` skalberg@14494 ` 1488` ``` qed ``` skalberg@14494 ` 1489` ``` finally show ?thesis . ``` skalberg@14494 ` 1490` ```qed ``` skalberg@14494 ` 1491` skalberg@14494 ` 1492` ```lemma length_int_to_bv_upper_limit_gt0: ``` skalberg@14494 ` 1493` ``` assumes w0: "0 < i" ``` skalberg@14494 ` 1494` ``` and wk: "i \ 2 ^ (k - 1) - 1" ``` skalberg@14494 ` 1495` ``` shows "length (int_to_bv i) \ k" ``` skalberg@14494 ` 1496` ```proof (rule ccontr) ``` skalberg@14494 ` 1497` ``` from w0 wk ``` skalberg@14494 ` 1498` ``` have k1: "1 < k" ``` skalberg@14494 ` 1499` ``` by (cases "k - 1",simp_all,arith) ``` skalberg@14494 ` 1500` ``` assume "~ length (int_to_bv i) \ k" ``` skalberg@14494 ` 1501` ``` hence "k < length (int_to_bv i)" ``` skalberg@14494 ` 1502` ``` by simp ``` skalberg@14494 ` 1503` ``` hence "k \ length (int_to_bv i) - 1" ``` skalberg@14494 ` 1504` ``` by arith ``` skalberg@14494 ` 1505` ``` hence a: "k - 1 \ length (int_to_bv i) - 2" ``` skalberg@14494 ` 1506` ``` by arith ``` paulson@15067 ` 1507` ``` hence "(2::int) ^ (k - 1) \ 2 ^ (length (int_to_bv i) - 2)" by simp ``` skalberg@14494 ` 1508` ``` also have "... \ i" ``` skalberg@14494 ` 1509` ``` proof - ``` skalberg@14494 ` 1510` ``` have "2 ^ (length (norm_signed (int_to_bv i)) - 2) \ bv_to_int (int_to_bv i)" ``` skalberg@14494 ` 1511` ``` proof (rule bv_to_int_lower_limit_gt0) ``` skalberg@14494 ` 1512` ``` from w0 ``` skalberg@14494 ` 1513` ``` show "0 < bv_to_int (int_to_bv i)" ``` skalberg@14494 ` 1514` ``` by simp ``` skalberg@14494 ` 1515` ``` qed ``` skalberg@14494 ` 1516` ``` thus ?thesis ``` skalberg@14494 ` 1517` ``` by simp ``` skalberg@14494 ` 1518` ``` qed ``` skalberg@14494 ` 1519` ``` finally have "2 ^ (k - 1) \ i" . ``` skalberg@14494 ` 1520` ``` with wk ``` skalberg@14494 ` 1521` ``` show False ``` skalberg@14494 ` 1522` ``` by simp ``` skalberg@14494 ` 1523` ```qed ``` skalberg@14494 ` 1524` skalberg@14494 ` 1525` ```lemma pos_length_pos: ``` skalberg@14494 ` 1526` ``` assumes i0: "0 < bv_to_int w" ``` skalberg@14494 ` 1527` ``` shows "0 < length w" ``` skalberg@14494 ` 1528` ```proof - ``` skalberg@14494 ` 1529` ``` from norm_signed_result [of w] ``` skalberg@14494 ` 1530` ``` have "0 < length (norm_signed w)" ``` skalberg@14494 ` 1531` ``` proof (auto) ``` skalberg@14494 ` 1532` ``` assume ii: "norm_signed w = []" ``` skalberg@14494 ` 1533` ``` have "bv_to_int (norm_signed w) = 0" ``` skalberg@14494 ` 1534` ``` by (subst ii,simp) ``` skalberg@14494 ` 1535` ``` hence "bv_to_int w = 0" ``` skalberg@14494 ` 1536` ``` by simp ``` skalberg@14494 ` 1537` ``` with i0 ``` skalberg@14494 ` 1538` ``` show False ``` skalberg@14494 ` 1539` ``` by simp ``` skalberg@14494 ` 1540` ``` next ``` skalberg@14494 ` 1541` ``` assume ii: "norm_signed w = []" ``` skalberg@14494 ` 1542` ``` assume jj: "bv_msb w \ \" ``` skalberg@14494 ` 1543` ``` have "\ = bv_msb (norm_signed w)" ``` skalberg@14494 ` 1544` ``` by (subst ii,simp) ``` skalberg@14494 ` 1545` ``` also have "... \ \" ``` skalberg@14494 ` 1546` ``` by (simp add: jj) ``` skalberg@14494 ` 1547` ``` finally show False by simp ``` skalberg@14494 ` 1548` ``` qed ``` skalberg@14494 ` 1549` ``` also have "... \ length w" ``` skalberg@14494 ` 1550` ``` by (rule norm_signed_length) ``` skalberg@14494 ` 1551` ``` finally show ?thesis ``` skalberg@14494 ` 1552` ``` . ``` skalberg@14494 ` 1553` ```qed ``` skalberg@14494 ` 1554` skalberg@14494 ` 1555` ```lemma neg_length_pos: ``` skalberg@14494 ` 1556` ``` assumes i0: "bv_to_int w < -1" ``` skalberg@14494 ` 1557` ``` shows "0 < length w" ``` skalberg@14494 ` 1558` ```proof - ``` skalberg@14494 ` 1559` ``` from norm_signed_result [of w] ``` skalberg@14494 ` 1560` ``` have "0 < length (norm_signed w)" ``` skalberg@14494 ` 1561` ``` proof (auto) ``` skalberg@14494 ` 1562` ``` assume ii: "norm_signed w = []" ``` skalberg@14494 ` 1563` ``` have "bv_to_int (norm_signed w) = 0" ``` skalberg@14494 ` 1564` ``` by (subst ii,simp) ``` skalberg@14494 ` 1565` ``` hence "bv_to_int w = 0" ``` skalberg@14494 ` 1566` ``` by simp ``` skalberg@14494 ` 1567` ``` with i0 ``` skalberg@14494 ` 1568` ``` show False ``` skalberg@14494 ` 1569` ``` by simp ``` skalberg@14494 ` 1570` ``` next ``` skalberg@14494 ` 1571` ``` assume ii: "norm_signed w = []" ``` skalberg@14494 ` 1572` ``` assume jj: "bv_msb w \ \" ``` skalberg@14494 ` 1573` ``` have "\ = bv_msb (norm_signed w)" ``` skalberg@14494 ` 1574` ``` by (subst ii,simp) ``` skalberg@14494 ` 1575` ``` also have "... \ \" ``` skalberg@14494 ` 1576` ``` by (simp add: jj) ``` skalberg@14494 ` 1577` ``` finally show False by simp ``` skalberg@14494 ` 1578` ``` qed ``` skalberg@14494 ` 1579` ``` also have "... \ length w" ``` skalberg@14494 ` 1580` ``` by (rule norm_signed_length) ``` skalberg@14494 ` 1581` ``` finally show ?thesis ``` skalberg@14494 ` 1582` ``` . ``` skalberg@14494 ` 1583` ```qed ``` skalberg@14494 ` 1584` skalberg@14494 ` 1585` ```lemma length_int_to_bv_lower_limit_gt0: ``` skalberg@14494 ` 1586` ``` assumes wk: "2 ^ (k - 1) \ i" ``` skalberg@14494 ` 1587` ``` shows "k < length (int_to_bv i)" ``` skalberg@14494 ` 1588` ```proof (rule ccontr) ``` skalberg@14494 ` 1589` ``` have "0 < (2::int) ^ (k - 1)" ``` paulson@15067 ` 1590` ``` by (rule zero_less_power,simp) ``` skalberg@14494 ` 1591` ``` also have "... \ i" ``` skalberg@14494 ` 1592` ``` by (rule wk) ``` skalberg@14494 ` 1593` ``` finally have i0: "0 < i" ``` skalberg@14494 ` 1594` ``` . ``` skalberg@14494 ` 1595` ``` have lii0: "0 < length (int_to_bv i)" ``` skalberg@14494 ` 1596` ``` apply (rule pos_length_pos) ``` skalberg@14494 ` 1597` ``` apply (simp,rule i0) ``` skalberg@14494 ` 1598` ``` done ``` skalberg@14494 ` 1599` ``` assume "~ k < length (int_to_bv i)" ``` skalberg@14494 ` 1600` ``` hence "length (int_to_bv i) \ k" ``` skalberg@14494 ` 1601` ``` by simp ``` skalberg@14494 ` 1602` ``` with lii0 ``` skalberg@14494 ` 1603` ``` have a: "length (int_to_bv i) - 1 \ k - 1" ``` skalberg@14494 ` 1604` ``` by arith ``` skalberg@14494 ` 1605` ``` have "i < 2 ^ (length (int_to_bv i) - 1)" ``` skalberg@14494 ` 1606` ``` proof - ``` skalberg@14494 ` 1607` ``` have "i = bv_to_int (int_to_bv i)" ``` skalberg@14494 ` 1608` ``` by simp ``` skalberg@14494 ` 1609` ``` also have "... < 2 ^ (length (int_to_bv i) - 1)" ``` skalberg@14494 ` 1610` ``` by (rule bv_to_int_upper_range) ``` skalberg@14494 ` 1611` ``` finally show ?thesis . ``` skalberg@14494 ` 1612` ``` qed ``` paulson@15067 ` 1613` ``` also have "(2::int) ^ (length (int_to_bv i) - 1) \ 2 ^ (k - 1)" using a ``` paulson@15067 ` 1614` ``` by simp ``` skalberg@14494 ` 1615` ``` finally have "i < 2 ^ (k - 1)" . ``` skalberg@14494 ` 1616` ``` with wk ``` skalberg@14494 ` 1617` ``` show False ``` skalberg@14494 ` 1618` ``` by simp ``` skalberg@14494 ` 1619` ```qed ``` skalberg@14494 ` 1620` skalberg@14494 ` 1621` ```lemma length_int_to_bv_upper_limit_lem1: ``` skalberg@14494 ` 1622` ``` assumes w1: "i < -1" ``` skalberg@14494 ` 1623` ``` and wk: "- (2 ^ (k - 1)) \ i" ``` skalberg@14494 ` 1624` ``` shows "length (int_to_bv i) \ k" ``` skalberg@14494 ` 1625` ```proof (rule ccontr) ``` skalberg@14494 ` 1626` ``` from w1 wk ``` skalberg@14494 ` 1627` ``` have k1: "1 < k" ``` skalberg@14494 ` 1628` ``` by (cases "k - 1",simp_all,arith) ``` skalberg@14494 ` 1629` ``` assume "~ length (int_to_bv i) \ k" ``` skalberg@14494 ` 1630` ``` hence "k < length (int_to_bv i)" ``` skalberg@14494 ` 1631` ``` by simp ``` skalberg@14494 ` 1632` ``` hence "k \ length (int_to_bv i) - 1" ``` skalberg@14494 ` 1633` ``` by arith ``` skalberg@14494 ` 1634` ``` hence a: "k - 1 \ length (int_to_bv i) - 2" ``` skalberg@14494 ` 1635` ``` by arith ``` skalberg@14494 ` 1636` ``` have "i < - (2 ^ (length (int_to_bv i) - 2))" ``` skalberg@14494 ` 1637` ``` proof - ``` skalberg@14494 ` 1638` ``` have "i = bv_to_int (int_to_bv i)" ``` skalberg@14494 ` 1639` ``` by simp ``` skalberg@14494 ` 1640` ``` also have "... < - (2 ^ (length (norm_signed (int_to_bv i)) - 2))" ``` skalberg@14494 ` 1641` ``` by (rule bv_to_int_upper_limit_lem1,simp,rule w1) ``` skalberg@14494 ` 1642` ``` finally show ?thesis by simp ``` skalberg@14494 ` 1643` ``` qed ``` skalberg@14494 ` 1644` ``` also have "... \ -(2 ^ (k - 1))" ``` skalberg@14494 ` 1645` ``` proof - ``` paulson@15067 ` 1646` ``` have "(2::int) ^ (k - 1) \ 2 ^ (length (int_to_bv i) - 2)" using a ``` paulson@15067 ` 1647` ``` by simp ``` skalberg@14494 ` 1648` ``` thus ?thesis ``` skalberg@14494 ` 1649` ``` by simp ``` skalberg@14494 ` 1650` ``` qed ``` skalberg@14494 ` 1651` ``` finally have "i < -(2 ^ (k - 1))" . ``` skalberg@14494 ` 1652` ``` with wk ``` skalberg@14494 ` 1653` ``` show False ``` skalberg@14494 ` 1654` ``` by simp ``` skalberg@14494 ` 1655` ```qed ``` skalberg@14494 ` 1656` skalberg@14494 ` 1657` ```lemma length_int_to_bv_lower_limit_lem1: ``` skalberg@14494 ` 1658` ``` assumes wk: "i < -(2 ^ (k - 1))" ``` skalberg@14494 ` 1659` ``` shows "k < length (int_to_bv i)" ``` skalberg@14494 ` 1660` ```proof (rule ccontr) ``` skalberg@14494 ` 1661` ``` from wk ``` skalberg@14494 ` 1662` ``` have "i \ -(2 ^ (k - 1)) - 1" ``` skalberg@14494 ` 1663` ``` by simp ``` skalberg@14494 ` 1664` ``` also have "... < -1" ``` skalberg@14494 ` 1665` ``` proof - ``` skalberg@14494 ` 1666` ``` have "0 < (2::int) ^ (k - 1)" ``` paulson@15067 ` 1667` ``` by (rule zero_less_power,simp) ``` skalberg@14494 ` 1668` ``` hence "-((2::int) ^ (k - 1)) < 0" ``` skalberg@14494 ` 1669` ``` by simp ``` skalberg@14494 ` 1670` ``` thus ?thesis by simp ``` skalberg@14494 ` 1671` ``` qed ``` skalberg@14494 ` 1672` ``` finally have i1: "i < -1" . ``` skalberg@14494 ` 1673` ``` have lii0: "0 < length (int_to_bv i)" ``` skalberg@14494 ` 1674` ``` apply (rule neg_length_pos) ``` skalberg@14494 ` 1675` ``` apply (simp,rule i1) ``` skalberg@14494 ` 1676` ``` done ``` skalberg@14494 ` 1677` ``` assume "~ k < length (int_to_bv i)" ``` skalberg@14494 ` 1678` ``` hence "length (int_to_bv i) \ k" ``` skalberg@14494 ` 1679` ``` by simp ``` skalberg@14494 ` 1680` ``` with lii0 ``` skalberg@14494 ` 1681` ``` have a: "length (int_to_bv i) - 1 \ k - 1" ``` skalberg@14494 ` 1682` ``` by arith ``` paulson@15067 ` 1683` ``` hence "(2::int) ^ (length (int_to_bv i) - 1) \ 2 ^ (k - 1)" by simp ``` skalberg@14494 ` 1684` ``` hence "-((2::int) ^ (k - 1)) \ - (2 ^ (length (int_to_bv i) - 1))" ``` skalberg@14494 ` 1685` ``` by simp ``` skalberg@14494 ` 1686` ``` also have "... \ i" ``` skalberg@14494 ` 1687` ``` proof - ``` skalberg@14494 ` 1688` ``` have "- (2 ^ (length (int_to_bv i) - 1)) \ bv_to_int (int_to_bv i)" ``` skalberg@14494 ` 1689` ``` by (rule bv_to_int_lower_range) ``` skalberg@14494 ` 1690` ``` also have "... = i" ``` skalberg@14494 ` 1691` ``` by simp ``` skalberg@14494 ` 1692` ``` finally show ?thesis . ``` skalberg@14494 ` 1693` ``` qed ``` skalberg@14494 ` 1694` ``` finally have "-(2 ^ (k - 1)) \ i" . ``` skalberg@14494 ` 1695` ``` with wk ``` skalberg@14494 ` 1696` ``` show False ``` skalberg@14494 ` 1697` ``` by simp ``` skalberg@14494 ` 1698` ```qed ``` skalberg@14494 ` 1699` wenzelm@14589 ` 1700` ```subsection {* Signed Arithmetic Operations *} ``` skalberg@14494 ` 1701` wenzelm@14589 ` 1702` ```subsubsection {* Conversion from unsigned to signed *} ``` skalberg@14494 ` 1703` skalberg@14494 ` 1704` ```constdefs ``` skalberg@14494 ` 1705` ``` utos :: "bit list => bit list" ``` skalberg@14494 ` 1706` ``` "utos w == norm_signed (\ # w)" ``` skalberg@14494 ` 1707` skalberg@14494 ` 1708` ```lemma [simp]: "utos (norm_unsigned w) = utos w" ``` skalberg@14494 ` 1709` ``` by (simp add: utos_def norm_signed_Cons) ``` skalberg@14494 ` 1710` skalberg@14494 ` 1711` ```lemma [simp]: "norm_signed (utos w) = utos w" ``` skalberg@14494 ` 1712` ``` by (simp add: utos_def) ``` skalberg@14494 ` 1713` skalberg@14494 ` 1714` ```lemma utos_length: "length (utos w) \ Suc (length w)" ``` skalberg@14494 ` 1715` ``` by (simp add: utos_def norm_signed_Cons) ``` skalberg@14494 ` 1716` skalberg@14494 ` 1717` ```lemma bv_to_int_utos: "bv_to_int (utos w) = bv_to_nat w" ``` skalberg@14494 ` 1718` ```proof (simp add: utos_def norm_signed_Cons,safe) ``` skalberg@14494 ` 1719` ``` assume "norm_unsigned w = []" ``` skalberg@14494 ` 1720` ``` hence "bv_to_nat (norm_unsigned w) = 0" ``` skalberg@14494 ` 1721` ``` by simp ``` skalberg@14494 ` 1722` ``` thus "bv_to_nat w = 0" ``` skalberg@14494 ` 1723` ``` by simp ``` skalberg@14494 ` 1724` ```qed ``` skalberg@14494 ` 1725` wenzelm@14589 ` 1726` ```subsubsection {* Unary minus *} ``` skalberg@14494 ` 1727` skalberg@14494 ` 1728` ```constdefs ``` skalberg@14494 ` 1729` ``` bv_uminus :: "bit list => bit list" ``` skalberg@14494 ` 1730` ``` "bv_uminus w == int_to_bv (- bv_to_int w)" ``` skalberg@14494 ` 1731` skalberg@14494 ` 1732` ```lemma [simp]: "bv_uminus (norm_signed w) = bv_uminus w" ``` skalberg@14494 ` 1733` ``` by (simp add: bv_uminus_def) ``` skalberg@14494 ` 1734` skalberg@14494 ` 1735` ```lemma [simp]: "norm_signed (bv_uminus w) = bv_uminus w" ``` skalberg@14494 ` 1736` ``` by (simp add: bv_uminus_def) ``` skalberg@14494 ` 1737` skalberg@14494 ` 1738` ```lemma bv_uminus_length: "length (bv_uminus w) \ Suc (length w)" ``` skalberg@14494 ` 1739` ```proof - ``` skalberg@14494 ` 1740` ``` have "1 < -bv_to_int w \ -bv_to_int w = 1 \ -bv_to_int w = 0 \ -bv_to_int w = -1 \ -bv_to_int w < -1" ``` skalberg@14494 ` 1741` ``` by arith ``` skalberg@14494 ` 1742` ``` thus ?thesis ``` skalberg@14494 ` 1743` ``` proof safe ``` skalberg@14494 ` 1744` ``` assume p: "1 < - bv_to_int w" ``` skalberg@14494 ` 1745` ``` have lw: "0 < length w" ``` skalberg@14494 ` 1746` ``` apply (rule neg_length_pos) ``` skalberg@14494 ` 1747` ``` using p ``` skalberg@14494 ` 1748` ``` apply simp ``` skalberg@14494 ` 1749` ``` done ``` skalberg@14494 ` 1750` ``` show ?thesis ``` skalberg@14494 ` 1751` ``` proof (simp add: bv_uminus_def,rule length_int_to_bv_upper_limit_gt0,simp_all) ``` skalberg@14494 ` 1752` ``` from prems ``` skalberg@14494 ` 1753` ``` show "bv_to_int w < 0" ``` skalberg@14494 ` 1754` ``` by simp ``` skalberg@14494 ` 1755` ``` next ``` skalberg@14494 ` 1756` ``` have "-(2^(length w - 1)) \ bv_to_int w" ``` skalberg@14494 ` 1757` ``` by (rule bv_to_int_lower_range) ``` skalberg@14494 ` 1758` ``` hence "- bv_to_int w \ 2^(length w - 1)" ``` skalberg@14494 ` 1759` ``` by simp ``` skalberg@14494 ` 1760` ``` also from lw have "... < 2 ^ length w" ``` skalberg@14494 ` 1761` ``` by simp ``` skalberg@14494 ` 1762` ``` finally show "- bv_to_int w < 2 ^ length w" ``` skalberg@14494 ` 1763` ``` by simp ``` skalberg@14494 ` 1764` ``` qed ``` skalberg@14494 ` 1765` ``` next ``` skalberg@14494 ` 1766` ``` assume p: "- bv_to_int w = 1" ``` skalberg@14494 ` 1767` ``` hence lw: "0 < length w" ``` skalberg@14494 ` 1768` ``` by (cases w,simp_all) ``` skalberg@14494 ` 1769` ``` from p ``` skalberg@14494 ` 1770` ``` show ?thesis ``` skalberg@14494 ` 1771` ``` apply (simp add: bv_uminus_def) ``` skalberg@14494 ` 1772` ``` using lw ``` skalberg@14494 ` 1773` ``` apply (simp (no_asm) add: nat_to_bv_non0) ``` skalberg@14494 ` 1774` ``` done ``` skalberg@14494 ` 1775` ``` next ``` skalberg@14494 ` 1776` ``` assume "- bv_to_int w = 0" ``` skalberg@14494 ` 1777` ``` thus ?thesis ``` skalberg@14494 ` 1778` ``` by (simp add: bv_uminus_def) ``` skalberg@14494 ` 1779` ``` next ``` skalberg@14494 ` 1780` ``` assume p: "- bv_to_int w = -1" ``` skalberg@14494 ` 1781` ``` thus ?thesis ``` skalberg@14494 ` 1782` ``` by (simp add: bv_uminus_def) ``` skalberg@14494 ` 1783` ``` next ``` skalberg@14494 ` 1784` ``` assume p: "- bv_to_int w < -1" ``` skalberg@14494 ` 1785` ``` show ?thesis ``` skalberg@14494 ` 1786` ``` apply (simp add: bv_uminus_def) ``` skalberg@14494 ` 1787` ``` apply (rule length_int_to_bv_upper_limit_lem1) ``` skalberg@14494 ` 1788` ``` apply (rule p) ``` skalberg@14494 ` 1789` ``` apply simp ``` skalberg@14494 ` 1790` ``` proof - ``` skalberg@14494 ` 1791` ``` have "bv_to_int w < 2 ^ (length w - 1)" ``` skalberg@14494 ` 1792` ``` by (rule bv_to_int_upper_range) ``` paulson@15067 ` 1793` ``` also have "... \ 2 ^ length w" by simp ``` skalberg@14494 ` 1794` ``` finally show "bv_to_int w \ 2 ^ length w" ``` skalberg@14494 ` 1795` ``` by simp ``` skalberg@14494 ` 1796` ``` qed ``` skalberg@14494 ` 1797` ``` qed ``` skalberg@14494 ` 1798` ```qed ``` skalberg@14494 ` 1799` skalberg@14494 ` 1800` ```lemma bv_uminus_length_utos: "length (bv_uminus (utos w)) \ Suc (length w)" ``` skalberg@14494 ` 1801` ```proof - ``` skalberg@14494 ` 1802` ``` have "-bv_to_int (utos w) = 0 \ -bv_to_int (utos w) = -1 \ -bv_to_int (utos w) < -1" ``` skalberg@14494 ` 1803` ``` apply (simp add: bv_to_int_utos) ``` skalberg@14494 ` 1804` ``` apply (cut_tac bv_to_nat_lower_range [of w]) ``` skalberg@14494 ` 1805` ``` by arith ``` skalberg@14494 ` 1806` ``` thus ?thesis ``` skalberg@14494 ` 1807` ``` proof safe ``` skalberg@14494 ` 1808` ``` assume "-bv_to_int (utos w) = 0" ``` skalberg@14494 ` 1809` ``` thus ?thesis ``` skalberg@14494 ` 1810` ``` by (simp add: bv_uminus_def) ``` skalberg@14494 ` 1811` ``` next ``` skalberg@14494 ` 1812` ``` assume "-bv_to_int (utos w) = -1" ``` skalberg@14494 ` 1813` ``` thus ?thesis ``` skalberg@14494 ` 1814` ``` by (simp add: bv_uminus_def) ``` skalberg@14494 ` 1815` ``` next ``` skalberg@14494 ` 1816` ``` assume p: "-bv_to_int (utos w) < -1" ``` skalberg@14494 ` 1817` ``` show ?thesis ``` skalberg@14494 ` 1818` ``` apply (simp add: bv_uminus_def) ``` skalberg@14494 ` 1819` ``` apply (rule length_int_to_bv_upper_limit_lem1) ``` skalberg@14494 ` 1820` ``` apply (rule p) ``` skalberg@14494 ` 1821` ``` apply (simp add: bv_to_int_utos) ``` skalberg@14494 ` 1822` ``` using bv_to_nat_upper_range [of w] ``` skalberg@14494 ` 1823` ``` apply simp ``` skalberg@14494 ` 1824` ``` done ``` skalberg@14494 ` 1825` ``` qed ``` skalberg@14494 ` 1826` ```qed ``` skalberg@14494 ` 1827` skalberg@14494 ` 1828` ```constdefs ``` skalberg@14494 ` 1829` ``` bv_sadd :: "[bit list, bit list ] => bit list" ``` skalberg@14494 ` 1830` ``` "bv_sadd w1 w2 == int_to_bv (bv_to_int w1 + bv_to_int w2)" ``` skalberg@14494 ` 1831` skalberg@14494 ` 1832` ```lemma [simp]: "bv_sadd (norm_signed w1) w2 = bv_sadd w1 w2" ``` skalberg@14494 ` 1833` ``` by (simp add: bv_sadd_def) ``` skalberg@14494 ` 1834` skalberg@14494 ` 1835` ```lemma [simp]: "bv_sadd w1 (norm_signed w2) = bv_sadd w1 w2" ``` skalberg@14494 ` 1836` ``` by (simp add: bv_sadd_def) ``` skalberg@14494 ` 1837` skalberg@14494 ` 1838` ```lemma [simp]: "norm_signed (bv_sadd w1 w2) = bv_sadd w1 w2" ``` skalberg@14494 ` 1839` ``` by (simp add: bv_sadd_def) ``` skalberg@14494 ` 1840` skalberg@14494 ` 1841` ```lemma adder_helper: ``` skalberg@14494 ` 1842` ``` assumes lw: "0 < max (length w1) (length w2)" ``` skalberg@14494 ` 1843` ``` shows "((2::int) ^ (length w1 - 1)) + (2 ^ (length w2 - 1)) \ 2 ^ max (length w1) (length w2)" ``` skalberg@14494 ` 1844` ```proof - ``` skalberg@14494 ` 1845` ``` have "((2::int) ^ (length w1 - 1)) + (2 ^ (length w2 - 1)) \ 2 ^ (max (length w1) (length w2) - 1) + 2 ^ (max (length w1) (length w2) - 1)" ``` skalberg@14494 ` 1846` ``` apply (cases "length w1 \ length w2") ``` skalberg@14494 ` 1847` ``` apply (auto simp add: max_def) ``` skalberg@14494 ` 1848` ``` apply arith ``` skalberg@14494 ` 1849` ``` apply arith ``` skalberg@14494 ` 1850` ``` done ``` skalberg@14494 ` 1851` ``` also have "... = 2 ^ max (length w1) (length w2)" ``` skalberg@14494 ` 1852` ``` proof - ``` skalberg@14494 ` 1853` ``` from lw ``` skalberg@14494 ` 1854` ``` show ?thesis ``` skalberg@14494 ` 1855` ``` apply simp ``` skalberg@14494 ` 1856` ``` apply (subst power_Suc [symmetric]) ``` skalberg@14494 ` 1857` ``` apply (simp del: power.simps) ``` skalberg@14494 ` 1858` ``` done ``` skalberg@14494 ` 1859` ``` qed ``` skalberg@14494 ` 1860` ``` finally show ?thesis . ``` skalberg@14494 ` 1861` ```qed ``` skalberg@14494 ` 1862` skalberg@14494 ` 1863` ```lemma bv_sadd_length: "length (bv_sadd w1 w2) \ Suc (max (length w1) (length w2))" ``` skalberg@14494 ` 1864` ```proof - ``` skalberg@14494 ` 1865` ``` let ?Q = "bv_to_int w1 + bv_to_int w2" ``` skalberg@14494 ` 1866` skalberg@14494 ` 1867` ``` have helper: "?Q \ 0 ==> 0 < max (length w1) (length w2)" ``` skalberg@14494 ` 1868` ``` proof - ``` skalberg@14494 ` 1869` ``` assume p: "?Q \ 0" ``` skalberg@14494 ` 1870` ``` show "0 < max (length w1) (length w2)" ``` skalberg@14494 ` 1871` ``` proof (simp add: less_max_iff_disj,rule) ``` skalberg@14494 ` 1872` ``` assume [simp]: "w1 = []" ``` skalberg@14494 ` 1873` ``` show "w2 \ []" ``` skalberg@14494 ` 1874` ``` proof (rule ccontr,simp) ``` skalberg@14494 ` 1875` ``` assume [simp]: "w2 = []" ``` skalberg@14494 ` 1876` ``` from p ``` skalberg@14494 ` 1877` ``` show False ``` skalberg@14494 ` 1878` ``` by simp ``` skalberg@14494 ` 1879` ``` qed ``` skalberg@14494 ` 1880` ``` qed ``` skalberg@14494 ` 1881` ``` qed ``` skalberg@14494 ` 1882` skalberg@14494 ` 1883` ``` have "0 < ?Q \ ?Q = 0 \ ?Q = -1 \ ?Q < -1" ``` skalberg@14494 ` 1884` ``` by arith ``` skalberg@14494 ` 1885` ``` thus ?thesis ``` skalberg@14494 ` 1886` ``` proof safe ``` skalberg@14494 ` 1887` ``` assume "?Q = 0" ``` skalberg@14494 ` 1888` ``` thus ?thesis ``` skalberg@14494 ` 1889` ``` by (simp add: bv_sadd_def) ``` skalberg@14494 ` 1890` ``` next ``` skalberg@14494 ` 1891` ``` assume "?Q = -1" ``` skalberg@14494 ` 1892` ``` thus ?thesis ``` skalberg@14494 ` 1893` ``` by (simp add: bv_sadd_def) ``` skalberg@14494 ` 1894` ``` next ``` skalberg@14494 ` 1895` ``` assume p: "0 < ?Q" ``` skalberg@14494 ` 1896` ``` show ?thesis ``` skalberg@14494 ` 1897` ``` apply (simp add: bv_sadd_def) ``` skalberg@14494 ` 1898` ``` apply (rule length_int_to_bv_upper_limit_gt0) ``` skalberg@14494 ` 1899` ``` apply (rule p) ``` skalberg@14494 ` 1900` ``` proof simp ``` skalberg@14494 ` 1901` ``` from bv_to_int_upper_range [of w2] ``` skalberg@14494 ` 1902` ``` have "bv_to_int w2 \ 2 ^ (length w2 - 1)" ``` skalberg@14494 ` 1903` ``` by simp ``` skalberg@14494 ` 1904` ``` with bv_to_int_upper_range [of w1] ``` skalberg@14494 ` 1905` ``` have "bv_to_int w1 + bv_to_int w2 < (2 ^ (length w1 - 1)) + (2 ^ (length w2 - 1))" ``` skalberg@14494 ` 1906` ``` by (rule zadd_zless_mono) ``` skalberg@14494 ` 1907` ``` also have "... \ 2 ^ max (length w1) (length w2)" ``` skalberg@14494 ` 1908` ``` apply (rule adder_helper) ``` skalberg@14494 ` 1909` ``` apply (rule helper) ``` skalberg@14494 ` 1910` ``` using p ``` skalberg@14494 ` 1911` ``` apply simp ``` skalberg@14494 ` 1912` ``` done ``` skalberg@14494 ` 1913` ``` finally show "?Q < 2 ^ max (length w1) (length w2)" ``` skalberg@14494 ` 1914` ``` . ``` skalberg@14494 ` 1915` ``` qed ``` skalberg@14494 ` 1916` ``` next ``` skalberg@14494 ` 1917` ``` assume p: "?Q < -1" ``` skalberg@14494 ` 1918` ``` show ?thesis ``` skalberg@14494 ` 1919` ``` apply (simp add: bv_sadd_def) ``` skalberg@14494 ` 1920` ``` apply (rule length_int_to_bv_upper_limit_lem1,simp_all) ``` skalberg@14494 ` 1921` ``` apply (rule p) ``` skalberg@14494 ` 1922` ``` proof - ``` skalberg@14494 ` 1923` ``` have "(2 ^ (length w1 - 1)) + 2 ^ (length w2 - 1) \ (2::int) ^ max (length w1) (length w2)" ``` skalberg@14494 ` 1924` ``` apply (rule adder_helper) ``` skalberg@14494 ` 1925` ``` apply (rule helper) ``` skalberg@14494 ` 1926` ``` using p ``` skalberg@14494 ` 1927` ``` apply simp ``` skalberg@14494 ` 1928` ``` done ``` skalberg@14494 ` 1929` ``` hence "-((2::int) ^ max (length w1) (length w2)) \ - (2 ^ (length w1 - 1)) + -(2 ^ (length w2 - 1))" ``` skalberg@14494 ` 1930` ``` by simp ``` skalberg@14494 ` 1931` ``` also have "- (2 ^ (length w1 - 1)) + -(2 ^ (length w2 - 1)) \ ?Q" ``` skalberg@14494 ` 1932` ``` apply (rule add_mono) ``` skalberg@14494 ` 1933` ``` apply (rule bv_to_int_lower_range [of w1]) ``` skalberg@14494 ` 1934` ``` apply (rule bv_to_int_lower_range [of w2]) ``` skalberg@14494 ` 1935` ``` done ``` skalberg@14494 ` 1936` ``` finally show "- (2^max (length w1) (length w2)) \ ?Q" . ``` skalberg@14494 ` 1937` ``` qed ``` skalberg@14494 ` 1938` ``` qed ``` skalberg@14494 ` 1939` ```qed ``` skalberg@14494 ` 1940` skalberg@14494 ` 1941` ```constdefs ``` skalberg@14494 ` 1942` ``` bv_sub :: "[bit list, bit list] => bit list" ``` skalberg@14494 ` 1943` ``` "bv_sub w1 w2 == bv_sadd w1 (bv_uminus w2)" ``` skalberg@14494 ` 1944` skalberg@14494 ` 1945` ```lemma [simp]: "bv_sub (norm_signed w1) w2 = bv_sub w1 w2" ``` skalberg@14494 ` 1946` ``` by (simp add: bv_sub_def) ``` skalberg@14494 ` 1947` skalberg@14494 ` 1948` ```lemma [simp]: "bv_sub w1 (norm_signed w2) = bv_sub w1 w2" ``` skalberg@14494 ` 1949` ``` by (simp add: bv_sub_def) ``` skalberg@14494 ` 1950` skalberg@14494 ` 1951` ```lemma [simp]: "norm_signed (bv_sub w1 w2) = bv_sub w1 w2" ``` skalberg@14494 ` 1952` ``` by (simp add: bv_sub_def) ``` skalberg@14494 ` 1953` skalberg@14494 ` 1954` ```lemma bv_sub_length: "length (bv_sub w1 w2) \ Suc (max (length w1) (length w2))" ``` skalberg@14494 ` 1955` ```proof (cases "bv_to_int w2 = 0") ``` skalberg@14494 ` 1956` ``` assume p: "bv_to_int w2 = 0" ``` skalberg@14494 ` 1957` ``` show ?thesis ``` skalberg@14494 ` 1958` ``` proof (simp add: bv_sub_def bv_sadd_def bv_uminus_def p) ``` skalberg@14494 ` 1959` ``` have "length (norm_signed w1) \ length w1" ``` skalberg@14494 ` 1960` ``` by (rule norm_signed_length) ``` skalberg@14494 ` 1961` ``` also have "... \ max (length w1) (length w2)" ``` skalberg@14494 ` 1962` ``` by (rule le_maxI1) ``` skalberg@14494 ` 1963` ``` also have "... \ Suc (max (length w1) (length w2))" ``` skalberg@14494 ` 1964` ``` by arith ``` skalberg@14494 ` 1965` ``` finally show "length (norm_signed w1) \ Suc (max (length w1) (length w2))" ``` skalberg@14494 ` 1966` ``` . ``` skalberg@14494 ` 1967` ``` qed ``` skalberg@14494 ` 1968` ```next ``` skalberg@14494 ` 1969` ``` assume "bv_to_int w2 \ 0" ``` skalberg@14494 ` 1970` ``` hence "0 < length w2" ``` skalberg@14494 ` 1971` ``` by (cases w2,simp_all) ``` skalberg@14494 ` 1972` ``` hence lmw: "0 < max (length w1) (length w2)" ``` skalberg@14494 ` 1973` ``` by arith ``` skalberg@14494 ` 1974` skalberg@14494 ` 1975` ``` let ?Q = "bv_to_int w1 - bv_to_int w2" ``` skalberg@14494 ` 1976` skalberg@14494 ` 1977` ``` have "0 < ?Q \ ?Q = 0 \ ?Q = -1 \ ?Q < -1" ``` skalberg@14494 ` 1978` ``` by arith ``` skalberg@14494 ` 1979` ``` thus ?thesis ``` skalberg@14494 ` 1980` ``` proof safe ``` skalberg@14494 ` 1981` ``` assume "?Q = 0" ``` skalberg@14494 ` 1982` ``` thus ?thesis ``` skalberg@14494 ` 1983` ``` by (simp add: bv_sub_def bv_sadd_def bv_uminus_def) ``` skalberg@14494 ` 1984` ``` next ``` skalberg@14494 ` 1985` ``` assume "?Q = -1" ``` skalberg@14494 ` 1986` ``` thus ?thesis ``` skalberg@14494 ` 1987` ``` by (simp add: bv_sub_def bv_sadd_def bv_uminus_def) ``` skalberg@14494 ` 1988` ``` next ``` skalberg@14494 ` 1989` ``` assume p: "0 < ?Q" ``` skalberg@14494 ` 1990` ``` show ?thesis ``` skalberg@14494 ` 1991` ``` apply (simp add: bv_sub_def bv_sadd_def bv_uminus_def) ``` skalberg@14494 ` 1992` ``` apply (rule length_int_to_bv_upper_limit_gt0) ``` skalberg@14494 ` 1993` ``` apply (rule p) ``` skalberg@14494 ` 1994` ``` proof simp ``` skalberg@14494 ` 1995` ``` from bv_to_int_lower_range [of w2] ``` skalberg@14494 ` 1996` ``` have v2: "- bv_to_int w2 \ 2 ^ (length w2 - 1)" ``` skalberg@14494 ` 1997` ``` by simp ``` skalberg@14494 ` 1998` ``` have "bv_to_int w1 + - bv_to_int w2 < (2 ^ (length w1 - 1)) + (2 ^ (length w2 - 1))" ``` skalberg@14494 ` 1999` ``` apply (rule zadd_zless_mono) ``` skalberg@14494 ` 2000` ``` apply (rule bv_to_int_upper_range [of w1]) ``` skalberg@14494 ` 2001` ``` apply (rule v2) ``` skalberg@14494 ` 2002` ``` done ``` skalberg@14494 ` 2003` ``` also have "... \ 2 ^ max (length w1) (length w2)" ``` skalberg@14494 ` 2004` ``` apply (rule adder_helper) ``` skalberg@14494 ` 2005` ``` apply (rule lmw) ``` skalberg@14494 ` 2006` ``` done ``` skalberg@14494 ` 2007` ``` finally show "?Q < 2 ^ max (length w1) (length w2)" ``` skalberg@14494 ` 2008` ``` by simp ``` skalberg@14494 ` 2009` ``` qed ``` skalberg@14494 ` 2010` ``` next ``` skalberg@14494 ` 2011` ``` assume p: "?Q < -1" ``` skalberg@14494 ` 2012` ``` show ?thesis ``` skalberg@14494 ` 2013` ``` apply (simp add: bv_sub_def bv_sadd_def bv_uminus_def) ``` skalberg@14494 ` 2014` ``` apply (rule length_int_to_bv_upper_limit_lem1) ``` skalberg@14494 ` 2015` ``` apply (rule p) ``` skalberg@14494 ` 2016` ``` proof simp ``` skalberg@14494 ` 2017` ``` have "(2 ^ (length w1 - 1)) + 2 ^ (length w2 - 1) \ (2::int) ^ max (length w1) (length w2)" ``` skalberg@14494 ` 2018` ``` apply (rule adder_helper) ``` skalberg@14494 ` 2019` ``` apply (rule lmw) ``` skalberg@14494 ` 2020` ``` done ``` skalberg@14494 ` 2021` ``` hence "-((2::int) ^ max (length w1) (length w2)) \ - (2 ^ (length w1 - 1)) + -(2 ^ (length w2 - 1))" ``` skalberg@14494 ` 2022` ``` by simp ``` skalberg@14494 ` 2023` ``` also have "- (2 ^ (length w1 - 1)) + -(2 ^ (length w2 - 1)) \ bv_to_int w1 + -bv_to_int w2" ``` skalberg@14494 ` 2024` ``` apply (rule add_mono) ``` skalberg@14494 ` 2025` ``` apply (rule bv_to_int_lower_range [of w1]) ``` skalberg@14494 ` 2026` ``` using bv_to_int_upper_range [of w2] ``` skalberg@14494 ` 2027` ``` apply simp ``` skalberg@14494 ` 2028` ``` done ``` skalberg@14494 ` 2029` ``` finally show "- (2^max (length w1) (length w2)) \ ?Q" ``` skalberg@14494 ` 2030` ``` by simp ``` skalberg@14494 ` 2031` ``` qed ``` skalberg@14494 ` 2032` ``` qed ``` skalberg@14494 ` 2033` ```qed ``` skalberg@14494 ` 2034` skalberg@14494 ` 2035` ```constdefs ``` skalberg@14494 ` 2036` ``` bv_smult :: "[bit list, bit list] => bit list" ``` skalberg@14494 ` 2037` ``` "bv_smult w1 w2 == int_to_bv (bv_to_int w1 * bv_to_int w2)" ``` skalberg@14494 ` 2038` skalberg@14494 ` 2039` ```lemma [simp]: "bv_smult (norm_signed w1) w2 = bv_smult w1 w2" ``` skalberg@14494 ` 2040` ``` by (simp add: bv_smult_def) ``` skalberg@14494 ` 2041` skalberg@14494 ` 2042` ```lemma [simp]: "bv_smult w1 (norm_signed w2) = bv_smult w1 w2" ``` skalberg@14494 ` 2043` ``` by (simp add: bv_smult_def) ``` skalberg@14494 ` 2044` skalberg@14494 ` 2045` ```lemma [simp]: "norm_signed (bv_smult w1 w2) = bv_smult w1 w2" ``` skalberg@14494 ` 2046` ``` by (simp add: bv_smult_def) ``` skalberg@14494 ` 2047` skalberg@14494 ` 2048` ```lemma bv_smult_length: "length (bv_smult w1 w2) \ length w1 + length w2" ``` skalberg@14494 ` 2049` ```proof - ``` skalberg@14494 ` 2050` ``` let ?Q = "bv_to_int w1 * bv_to_int w2" ``` skalberg@14494 ` 2051` skalberg@14494 ` 2052` ``` have lmw: "?Q \ 0 ==> 0 < length w1 \ 0 < length w2" ``` skalberg@14494 ` 2053` ``` by auto ``` skalberg@14494 ` 2054` skalberg@14494 ` 2055` ``` have "0 < ?Q \ ?Q = 0 \ ?Q = -1 \ ?Q < -1" ``` skalberg@14494 ` 2056` ``` by arith ``` skalberg@14494 ` 2057` ``` thus ?thesis ``` skalberg@14494 ` 2058` ``` proof (safe dest!: iffD1 [OF mult_eq_0_iff]) ``` skalberg@14494 ` 2059` ``` assume "bv_to_int w1 = 0" ``` skalberg@14494 ` 2060` ``` thus ?thesis ``` skalberg@14494 ` 2061` ``` by (simp add: bv_smult_def) ``` skalberg@14494 ` 2062` ``` next ``` skalberg@14494 ` 2063` ``` assume "bv_to_int w2 = 0" ``` skalberg@14494 ` 2064` ``` thus ?thesis ``` skalberg@14494 ` 2065` ``` by (simp add: bv_smult_def) ``` skalberg@14494 ` 2066` ``` next ``` skalberg@14494 ` 2067` ``` assume p: "?Q = -1" ``` skalberg@14494 ` 2068` ``` show ?thesis ``` skalberg@14494 ` 2069` ``` apply (simp add: bv_smult_def p) ``` skalberg@14494 ` 2070` ``` apply (cut_tac lmw) ``` skalberg@14494 ` 2071` ``` apply arith ``` skalberg@14494 ` 2072` ``` using p ``` skalberg@14494 ` 2073` ``` apply simp ``` skalberg@14494 ` 2074` ``` done ``` skalberg@14494 ` 2075` ``` next ``` skalberg@14494 ` 2076` ``` assume p: "0 < ?Q" ``` skalberg@14494 ` 2077` ``` thus ?thesis ``` skalberg@14494 ` 2078` ``` proof (simp add: zero_less_mult_iff,safe) ``` skalberg@14494 ` 2079` ``` assume bi1: "0 < bv_to_int w1" ``` skalberg@14494 ` 2080` ``` assume bi2: "0 < bv_to_int w2" ``` skalberg@14494 ` 2081` ``` show ?thesis ``` skalberg@14494 ` 2082` ``` apply (simp add: bv_smult_def) ``` skalberg@14494 ` 2083` ``` apply (rule length_int_to_bv_upper_limit_gt0) ``` skalberg@14494 ` 2084` ``` apply (rule p) ``` skalberg@14494 ` 2085` ``` proof simp ``` skalberg@14494 ` 2086` ``` have "?Q < 2 ^ (length w1 - 1) * 2 ^ (length w2 - 1)" ``` skalberg@14494 ` 2087` ``` apply (rule mult_strict_mono) ``` skalberg@14494 ` 2088` ``` apply (rule bv_to_int_upper_range) ``` skalberg@14494 ` 2089` ``` apply (rule bv_to_int_upper_range) ``` paulson@15067 ` 2090` ``` apply (rule zero_less_power) ``` skalberg@14494 ` 2091` ``` apply simp ``` skalberg@14494 ` 2092` ``` using bi2 ``` skalberg@14494 ` 2093` ``` apply simp ``` skalberg@14494 ` 2094` ``` done ``` skalberg@14494 ` 2095` ``` also have "... \ 2 ^ (length w1 + length w2 - Suc 0)" ``` skalberg@14494 ` 2096` ``` apply simp ``` skalberg@14494 ` 2097` ``` apply (subst zpower_zadd_distrib [symmetric]) ``` skalberg@14494 ` 2098` ``` apply simp ``` skalberg@14494 ` 2099` ``` apply arith ``` skalberg@14494 ` 2100` ``` done ``` skalberg@14494 ` 2101` ``` finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)" ``` skalberg@14494 ` 2102` ``` . ``` skalberg@14494 ` 2103` ``` qed ``` skalberg@14494 ` 2104` ``` next ``` skalberg@14494 ` 2105` ``` assume bi1: "bv_to_int w1 < 0" ``` skalberg@14494 ` 2106` ``` assume bi2: "bv_to_int w2 < 0" ``` skalberg@14494 ` 2107` ``` show ?thesis ``` skalberg@14494 ` 2108` ``` apply (simp add: bv_smult_def) ``` skalberg@14494 ` 2109` ``` apply (rule length_int_to_bv_upper_limit_gt0) ``` skalberg@14494 ` 2110` ``` apply (rule p) ``` skalberg@14494 ` 2111` ``` proof simp ``` skalberg@14494 ` 2112` ``` have "-bv_to_int w1 * -bv_to_int w2 \ 2 ^ (length w1 - 1) * 2 ^(length w2 - 1)" ``` skalberg@14494 ` 2113` ``` apply (rule mult_mono) ``` skalberg@14494 ` 2114` ``` using bv_to_int_lower_range [of w1] ``` skalberg@14494 ` 2115` ``` apply simp ``` skalberg@14494 ` 2116` ``` using bv_to_int_lower_range [of w2] ``` skalberg@14494 ` 2117` ``` apply simp ``` paulson@15067 ` 2118` ``` apply (rule zero_le_power,simp) ``` skalberg@14494 ` 2119` ``` using bi2 ``` skalberg@14494 ` 2120` ``` apply simp ``` skalberg@14494 ` 2121` ``` done ``` skalberg@14494 ` 2122` ``` hence "?Q \ 2 ^ (length w1 - 1) * 2 ^(length w2 - 1)" ``` skalberg@14494 ` 2123` ``` by simp ``` skalberg@14494 ` 2124` ``` also have "... < 2 ^ (length w1 + length w2 - Suc 0)" ``` skalberg@14494 ` 2125` ``` apply simp ``` skalberg@14494 ` 2126` ``` apply (subst zpower_zadd_distrib [symmetric]) ``` skalberg@14494 ` 2127` ``` apply simp ``` skalberg@14494 ` 2128` ``` apply (cut_tac lmw) ``` skalberg@14494 ` 2129` ``` apply arith ``` skalberg@14494 ` 2130` ``` apply (cut_tac p) ``` skalberg@14494 ` 2131` ``` apply arith ``` skalberg@14494 ` 2132` ``` done ``` skalberg@14494 ` 2133` ``` finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)" . ``` skalberg@14494 ` 2134` ``` qed ``` skalberg@14494 ` 2135` ``` qed ``` skalberg@14494 ` 2136` ``` next ``` skalberg@14494 ` 2137` ``` assume p: "?Q < -1" ``` skalberg@14494 ` 2138` ``` show ?thesis ``` skalberg@14494 ` 2139` ``` apply (subst bv_smult_def) ``` skalberg@14494 ` 2140` ``` apply (rule length_int_to_bv_upper_limit_lem1) ``` skalberg@14494 ` 2141` ``` apply (rule p) ``` skalberg@14494 ` 2142` ``` proof simp ``` skalberg@14494 ` 2143` ``` have "(2::int) ^ (length w1 - 1) * 2 ^(length w2 - 1) \ 2 ^ (length w1 + length w2 - Suc 0)" ``` skalberg@14494 ` 2144` ``` apply simp ``` skalberg@14494 ` 2145` ``` apply (subst zpower_zadd_distrib [symmetric]) ``` skalberg@14494 ` 2146` ``` apply simp ``` skalberg@14494 ` 2147` ``` apply (cut_tac lmw) ``` skalberg@14494 ` 2148` ``` apply arith ``` skalberg@14494 ` 2149` ``` apply (cut_tac p) ``` skalberg@14494 ` 2150` ``` apply arith ``` skalberg@14494 ` 2151` ``` done ``` skalberg@14494 ` 2152` ``` hence "-((2::int) ^ (length w1 + length w2 - Suc 0)) \ -(2^(length w1 - 1) * 2 ^ (length w2 - 1))" ``` skalberg@14494 ` 2153` ``` by simp ``` skalberg@14494 ` 2154` ``` also have "... \ ?Q" ``` skalberg@14494 ` 2155` ``` proof - ``` skalberg@14494 ` 2156` ``` from p ``` skalberg@14494 ` 2157` ``` have q: "bv_to_int w1 * bv_to_int w2 < 0" ``` skalberg@14494 ` 2158` ``` by simp ``` skalberg@14494 ` 2159` ``` thus ?thesis ``` skalberg@14494 ` 2160` ``` proof (simp add: mult_less_0_iff,safe) ``` skalberg@14494 ` 2161` ``` assume bi1: "0 < bv_to_int w1" ``` skalberg@14494 ` 2162` ``` assume bi2: "bv_to_int w2 < 0" ``` skalberg@14494 ` 2163` ``` have "-bv_to_int w2 * bv_to_int w1 \ ((2::int)^(length w2 - 1)) * (2 ^ (length w1 - 1))" ``` skalberg@14494 ` 2164` ``` apply (rule mult_mono) ``` skalberg@14494 ` 2165` ``` using bv_to_int_lower_range [of w2] ``` skalberg@14494 ` 2166` ``` apply simp ``` skalberg@14494 ` 2167` ``` using bv_to_int_upper_range [of w1] ``` skalberg@14494 ` 2168` ``` apply simp ``` paulson@15067 ` 2169` ``` apply (rule zero_le_power,simp) ``` skalberg@14494 ` 2170` ``` using bi1 ``` skalberg@14494 ` 2171` ``` apply simp ``` skalberg@14494 ` 2172` ``` done ``` skalberg@14494 ` 2173` ``` hence "-?Q \ ((2::int)^(length w1 - 1)) * (2 ^ (length w2 - 1))" ``` skalberg@14494 ` 2174` ``` by (simp add: zmult_ac) ``` skalberg@14494 ` 2175` ``` thus "-(((2::int)^(length w1 - Suc 0)) * (2 ^ (length w2 - Suc 0))) \ ?Q" ``` skalberg@14494 ` 2176` ``` by simp ``` skalberg@14494 ` 2177` ``` next ``` skalberg@14494 ` 2178` ``` assume bi1: "bv_to_int w1 < 0" ``` skalberg@14494 ` 2179` ``` assume bi2: "0 < bv_to_int w2" ``` skalberg@14494 ` 2180` ``` have "-bv_to_int w1 * bv_to_int w2 \ ((2::int)^(length w1 - 1)) * (2 ^ (length w2 - 1))" ``` skalberg@14494 ` 2181` ``` apply (rule mult_mono) ``` skalberg@14494 ` 2182` ``` using bv_to_int_lower_range [of w1] ``` skalberg@14494 ` 2183` ``` apply simp ``` skalberg@14494 ` 2184` ``` using bv_to_int_upper_range [of w2] ``` skalberg@14494 ` 2185` ``` apply simp ``` paulson@15067 ` 2186` ``` apply (rule zero_le_power,simp) ``` skalberg@14494 ` 2187` ``` using bi2 ``` skalberg@14494 ` 2188` ``` apply simp ``` skalberg@14494 ` 2189` ``` done ``` skalberg@14494 ` 2190` ``` hence "-?Q \ ((2::int)^(length w1 - 1)) * (2 ^ (length w2 - 1))" ``` skalberg@14494 ` 2191` ``` by (simp add: zmult_ac) ``` skalberg@14494 ` 2192` ``` thus "-(((2::int)^(length w1 - Suc 0)) * (2 ^ (length w2 - Suc 0))) \ ?Q" ``` skalberg@14494 ` 2193` ``` by simp ``` skalberg@14494 ` 2194` ``` qed ``` skalberg@14494 ` 2195` ``` qed ``` skalberg@14494 ` 2196` ``` finally show "-(2 ^ (length w1 + length w2 - Suc 0)) \ ?Q" ``` skalberg@14494 ` 2197` ``` . ``` skalberg@14494 ` 2198` ``` qed ``` skalberg@14494 ` 2199` ``` qed ``` skalberg@14494 ` 2200` ```qed ``` skalberg@14494 ` 2201` skalberg@14494 ` 2202` ```lemma bv_msb_one: "bv_msb w = \ ==> 0 < bv_to_nat w" ``` skalberg@14494 ` 2203` ``` apply (cases w,simp_all) ``` skalberg@14494 ` 2204` ``` apply (subgoal_tac "0 + 0 < 2 ^ length list + bv_to_nat list") ``` skalberg@14494 ` 2205` ``` apply simp ``` skalberg@14494 ` 2206` ``` apply (rule add_less_le_mono) ``` paulson@15067 ` 2207` ``` apply (rule zero_less_power) ``` skalberg@14494 ` 2208` ``` apply simp_all ``` skalberg@14494 ` 2209` ``` done ``` skalberg@14494 ` 2210` skalberg@14494 ` 2211` ```lemma bv_smult_length_utos: "length (bv_smult (utos w1) w2) \ length w1 + length w2" ``` skalberg@14494 ` 2212` ```proof - ``` skalberg@14494 ` 2213` ``` let ?Q = "bv_to_int (utos w1) * bv_to_int w2" ``` skalberg@14494 ` 2214` skalberg@14494 ` 2215` ``` have lmw: "?Q \ 0 ==> 0 < length (utos w1) \ 0 < length w2" ``` skalberg@14494 ` 2216` ``` by auto ``` skalberg@14494 ` 2217` skalberg@14494 ` 2218` ``` have "0 < ?Q \ ?Q = 0 \ ?Q = -1 \ ?Q < -1" ``` skalberg@14494 ` 2219` ``` by arith ``` skalberg@14494 ` 2220` ``` thus ?thesis ``` skalberg@14494 ` 2221` ``` proof (safe dest!: iffD1 [OF mult_eq_0_iff]) ``` skalberg@14494 ` 2222` ``` assume "bv_to_int (utos w1) = 0" ``` skalberg@14494 ` 2223` ``` thus ?thesis ``` skalberg@14494 ` 2224` ``` by (simp add: bv_smult_def) ``` skalberg@14494 ` 2225` ``` next ``` skalberg@14494 ` 2226` ``` assume "bv_to_int w2 = 0" ``` skalberg@14494 ` 2227` ``` thus ?thesis ``` skalberg@14494 ` 2228` ``` by (simp add: bv_smult_def) ``` skalberg@14494 ` 2229` ``` next ``` skalberg@14494 ` 2230` ``` assume p: "0 < ?Q" ``` skalberg@14494 ` 2231` ``` thus ?thesis ``` skalberg@14494 ` 2232` ``` proof (simp add: zero_less_mult_iff,safe) ``` skalberg@14494 ` 2233` ``` assume biw2: "0 < bv_to_int w2" ``` skalberg@14494 ` 2234` ``` show ?thesis ``` skalberg@14494 ` 2235` ``` apply (simp add: bv_smult_def) ``` skalberg@14494 ` 2236` ``` apply (rule length_int_to_bv_upper_limit_gt0) ``` skalberg@14494 ` 2237` ``` apply (rule p) ``` skalberg@14494 ` 2238` ``` proof simp ``` skalberg@14494 ` 2239` ``` have "?Q < 2 ^ length w1 * 2 ^ (length w2 - 1)" ``` skalberg@14494 ` 2240` ``` apply (rule mult_strict_mono) ``` skalberg@14494 ` 2241` ``` apply (simp add: bv_to_int_utos) ``` skalberg@14494 ` 2242` ``` apply (rule bv_to_nat_upper_range) ``` skalberg@14494 ` 2243` ``` apply (rule bv_to_int_upper_range) ``` paulson@15067 ` 2244` ``` apply (rule zero_less_power,simp) ``` skalberg@14494 ` 2245` ``` using biw2 ``` skalberg@14494 ` 2246` ``` apply simp ``` skalberg@14494 ` 2247` ``` done ``` skalberg@14494 ` 2248` ``` also have "... \ 2 ^ (length w1 + length w2 - Suc 0)" ``` skalberg@14494 ` 2249` ``` apply simp ``` skalberg@14494 ` 2250` ``` apply (subst zpower_zadd_distrib [symmetric]) ``` skalberg@14494 ` 2251` ``` apply simp ``` skalberg@14494 ` 2252` ``` apply (cut_tac lmw) ``` skalberg@14494 ` 2253` ``` apply arith ``` skalberg@14494 ` 2254` ``` using p ``` skalberg@14494 ` 2255` ``` apply auto ``` skalberg@14494 ` 2256` ``` done ``` skalberg@14494 ` 2257` ``` finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)" ``` skalberg@14494 ` 2258` ``` . ``` skalberg@14494 ` 2259` ``` qed ``` skalberg@14494 ` 2260` ``` next ``` skalberg@14494 ` 2261` ``` assume "bv_to_int (utos w1) < 0" ``` skalberg@14494 ` 2262` ``` thus ?thesis ``` skalberg@14494 ` 2263` ``` apply (simp add: bv_to_int_utos) ``` skalberg@14494 ` 2264` ``` using bv_to_nat_lower_range [of w1] ``` skalberg@14494 ` 2265` ``` apply simp ``` skalberg@14494 ` 2266` ``` done ``` skalberg@14494 ` 2267` ``` qed ``` skalberg@14494 ` 2268` ``` next ``` skalberg@14494 ` 2269` ``` assume p: "?Q = -1" ``` skalberg@14494 ` 2270` ``` thus ?thesis ``` skalberg@14494 ` 2271` ``` apply (simp add: bv_smult_def) ``` skalberg@14494 ` 2272` ``` apply (cut_tac lmw) ``` skalberg@14494 ` 2273` ``` apply arith ``` skalberg@14494 ` 2274` ``` apply simp ``` skalberg@14494 ` 2275` ``` done ``` skalberg@14494 ` 2276` ``` next ``` skalberg@14494 ` 2277` ``` assume p: "?Q < -1" ``` skalberg@14494 ` 2278` ``` show ?thesis ``` skalberg@14494 ` 2279` ``` apply (subst bv_smult_def) ``` skalberg@14494 ` 2280` ``` apply (rule length_int_to_bv_upper_limit_lem1) ``` skalberg@14494 ` 2281` ``` apply (rule p) ``` skalberg@14494 ` 2282` ``` proof simp ``` skalberg@14494 ` 2283` ``` have "(2::int) ^ length w1 * 2 ^(length w2 - 1) \ 2 ^ (length w1 + length w2 - Suc 0)" ``` skalberg@14494 ` 2284` ``` apply simp ``` skalberg@14494 ` 2285` ``` apply (subst zpower_zadd_distrib [symmetric]) ``` skalberg@14494 ` 2286` ``` apply simp ``` skalberg@14494 ` 2287` ``` apply (cut_tac lmw) ``` skalberg@14494 ` 2288` ``` apply arith ``` skalberg@14494 ` 2289` ``` apply (cut_tac p) ``` skalberg@14494 ` 2290` ``` apply arith ``` skalberg@14494 ` 2291` ``` done ``` skalberg@14494 ` 2292` ``` hence "-((2::int) ^ (length w1 + length w2 - Suc 0)) \ -(2^ length w1 * 2 ^ (length w2 - 1))" ``` skalberg@14494 ` 2293` ``` by simp ``` skalberg@14494 ` 2294` ``` also have "... \ ?Q" ``` skalberg@14494 ` 2295` ``` proof - ``` skalberg@14494 ` 2296` ``` from p ``` skalberg@14494 ` 2297` ``` have q: "bv_to_int (utos w1) * bv_to_int w2 < 0" ``` skalberg@14494 ` 2298` ``` by simp ``` skalberg@14494 ` 2299` ``` thus ?thesis ``` skalberg@14494 ` 2300` ``` proof (simp add: mult_less_0_iff,safe) ``` skalberg@14494 ` 2301` ``` assume bi1: "0 < bv_to_int (utos w1)" ``` skalberg@14494 ` 2302` ``` assume bi2: "bv_to_int w2 < 0" ``` skalberg@14494 ` 2303` ``` have "-bv_to_int w2 * bv_to_int (utos w1) \ ((2::int)^(length w2 - 1)) * (2 ^ length w1)" ``` skalberg@14494 ` 2304` ``` apply (rule mult_mono) ``` skalberg@14494 ` 2305` ``` using bv_to_int_lower_range [of w2] ``` skalberg@14494 ` 2306` ``` apply simp ``` skalberg@14494 ` 2307` ``` apply (simp add: bv_to_int_utos) ``` skalberg@14494 ` 2308` ``` using bv_to_nat_upper_range [of w1] ``` skalberg@14494 ` 2309` ``` apply simp ``` paulson@15067 ` 2310` ``` apply (rule zero_le_power,simp) ``` skalberg@14494 ` 2311` ``` using bi1 ``` skalberg@14494 ` 2312` ``` apply simp ``` skalberg@14494 ` 2313` ``` done ``` skalberg@14494 ` 2314` ``` hence "-?Q \ ((2::int)^length w1) * (2 ^ (length w2 - 1))" ``` skalberg@14494 ` 2315` ``` by (simp add: zmult_ac) ``` skalberg@14494 ` 2316` ``` thus "-(((2::int)^length w1) * (2 ^ (length w2 - Suc 0))) \ ?Q" ``` skalberg@14494 ` 2317` ``` by simp ``` skalberg@14494 ` 2318` ``` next ``` skalberg@14494 ` 2319` ``` assume bi1: "bv_to_int (utos w1) < 0" ``` skalberg@14494 ` 2320` ``` thus "-(((2::int)^length w1) * (2 ^ (length w2 - Suc 0))) \ ?Q" ``` skalberg@14494 ` 2321` ``` apply (simp add: bv_to_int_utos) ``` skalberg@14494 ` 2322` ``` using bv_to_nat_lower_range [of w1] ``` skalberg@14494 ` 2323` ``` apply simp ``` skalberg@14494 ` 2324` ``` done ``` skalberg@14494 ` 2325` ``` qed ``` skalberg@14494 ` 2326` ``` qed ``` skalberg@14494 ` 2327` ``` finally show "-(2 ^ (length w1 + length w2 - Suc 0)) \ ?Q" ``` skalberg@14494 ` 2328` ``` . ``` skalberg@14494 ` 2329` ``` qed ``` skalberg@14494 ` 2330` ``` qed ``` skalberg@14494 ` 2331` ```qed ``` skalberg@14494 ` 2332` skalberg@14494 ` 2333` ```lemma bv_smult_sym: "bv_smult w1 w2 = bv_smult w2 w1" ``` skalberg@14494 ` 2334` ``` by (simp add: bv_smult_def zmult_ac) ``` skalberg@14494 ` 2335` wenzelm@14589 ` 2336` ```subsection {* Structural operations *} ``` skalberg@14494 ` 2337` skalberg@14494 ` 2338` ```constdefs ``` skalberg@14494 ` 2339` ``` bv_select :: "[bit list,nat] => bit" ``` skalberg@14494 ` 2340` ``` "bv_select w i == w ! (length w - 1 - i)" ``` skalberg@14494 ` 2341` ``` bv_chop :: "[bit list,nat] => bit list * bit list" ``` skalberg@14494 ` 2342` ``` "bv_chop w i == let len = length w in (take (len - i) w,drop (len - i) w)" ``` skalberg@14494 ` 2343` ``` bv_slice :: "[bit list,nat*nat] => bit list" ``` skalberg@14494 ` 2344` ``` "bv_slice w == \(b,e). fst (bv_chop (snd (bv_chop w (b+1))) e)" ``` skalberg@14494 ` 2345` skalberg@14494 ` 2346` ```lemma bv_select_rev: ``` skalberg@14494 ` 2347` ``` assumes notnull: "n < length w" ``` skalberg@14494 ` 2348` ``` shows "bv_select w n = rev w ! n" ``` skalberg@14494 ` 2349` ```proof - ``` skalberg@14494 ` 2350` ``` have "\n. n < length w --> bv_select w n = rev w ! n" ``` skalberg@14494 ` 2351` ``` proof (rule length_induct [of _ w],auto simp add: bv_select_def) ``` skalberg@14494 ` 2352` ``` fix xs :: "bit list" ``` skalberg@14494 ` 2353` ``` fix n ``` skalberg@14494 ` 2354` ``` assume ind: "\ys::bit list. length ys < length xs --> (\n. n < length ys --> ys ! (length ys - Suc n) = rev ys ! n)" ``` skalberg@14494 ` 2355` ``` assume notx: "n < length xs" ``` skalberg@14494 ` 2356` ``` show "xs ! (length xs - Suc n) = rev xs ! n" ``` skalberg@14494 ` 2357` ``` proof (cases xs) ``` skalberg@14494 ` 2358` ``` assume "xs = []" ``` skalberg@14494 ` 2359` ``` with notx ```