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