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