(* Author: Sebastian Skalberg, TU Muenchen *) section ‹Binary Words› theory Word imports Main begin subsection ‹Auxilary Lemmas› lemma max_le [intro!]: "[| x ≤ z; y ≤ z |] ==> max x y ≤ z" by (simp add: max_def) lemma max_mono: fixes x :: "'a::linorder" assumes mf: "mono f" shows "max (f x) (f y) ≤ f (max x y)" proof - from mf and max.cobounded1 [of x y] have fx: "f x ≤ f (max x y)" by (rule monoD) from mf and max.cobounded2 [of y x] have fy: "f y ≤ f (max x y)" by (rule monoD) from fx and fy show "max (f x) (f y) ≤ f (max x y)" by auto qed declare zero_le_power [intro] and zero_less_power [intro] lemma int_nat_two_exp: "2 ^ k = int (2 ^ k)" by simp subsection ‹Bits› datatype bit = Zero ("𝟬") | One ("𝟭") primrec bitval :: "bit => nat" where "bitval 𝟬 = 0" | "bitval 𝟭 = 1" primrec bitnot :: "bit => bit" ("¬⇩_{b}_" [40] 40) where bitnot_zero: "(¬⇩_{b}𝟬) = 𝟭" | bitnot_one : "(¬⇩_{b}𝟭) = 𝟬" primrec bitand :: "bit => bit => bit" (infixr "∧⇩_{b}" 35) where bitand_zero: "(𝟬 ∧⇩_{b}y) = 𝟬" | bitand_one: "(𝟭 ∧⇩_{b}y) = y" primrec bitor :: "bit => bit => bit" (infixr "∨⇩_{b}" 30) where bitor_zero: "(𝟬 ∨⇩_{b}y) = y" | bitor_one: "(𝟭 ∨⇩_{b}y) = 𝟭" primrec bitxor :: "bit => bit => bit" (infixr "⊕⇩_{b}" 30) where bitxor_zero: "(𝟬 ⊕⇩_{b}y) = y" | bitxor_one: "(𝟭 ⊕⇩_{b}y) = (bitnot y)" lemma bitnot_bitnot [simp]: "(bitnot (bitnot b)) = b" by (cases b) simp_all lemma bitand_cancel [simp]: "(b ∧⇩_{b}b) = b" by (cases b) simp_all lemma bitor_cancel [simp]: "(b ∨⇩_{b}b) = b" by (cases b) simp_all lemma bitxor_cancel [simp]: "(b ⊕⇩_{b}b) = 𝟬" by (cases b) simp_all subsection ‹Bit Vectors› text ‹First, a couple of theorems expressing case analysis and induction principles for bit vectors.› lemma bit_list_cases: assumes empty: "w = [] ==> P w" and zero: "!!bs. w = 𝟬 # bs ==> P w" and one: "!!bs. w = 𝟭 # bs ==> P w" shows "P w" proof (cases w) assume "w = []" thus ?thesis by (rule empty) next fix b bs assume [simp]: "w = b # bs" show "P w" proof (cases b) assume "b = 𝟬" hence "w = 𝟬 # bs" by simp thus ?thesis by (rule zero) next assume "b = 𝟭" hence "w = 𝟭 # bs" by simp thus ?thesis by (rule one) qed qed lemma bit_list_induct: assumes empty: "P []" and zero: "!!bs. P bs ==> P (𝟬#bs)" and one: "!!bs. P bs ==> P (𝟭#bs)" shows "P w" proof (induct w, simp_all add: empty) fix b bs assume "P bs" then show "P (b#bs)" by (cases b) (auto intro!: zero one) qed definition bv_msb :: "bit list => bit" where "bv_msb w = (if w = [] then 𝟬 else hd w)" definition bv_extend :: "[nat,bit,bit list]=>bit list" where "bv_extend i b w = (replicate (i - length w) b) @ w" definition bv_not :: "bit list => bit list" where "bv_not w = map bitnot w" lemma bv_length_extend [simp]: "length w ≤ i ==> length (bv_extend i b w) = i" by (simp add: bv_extend_def) lemma bv_not_Nil [simp]: "bv_not [] = []" by (simp add: bv_not_def) lemma bv_not_Cons [simp]: "bv_not (b#bs) = (bitnot b) # bv_not bs" by (simp add: bv_not_def) lemma bv_not_bv_not [simp]: "bv_not (bv_not w) = w" by (rule bit_list_induct [of _ w]) simp_all lemma bv_msb_Nil [simp]: "bv_msb [] = 𝟬" by (simp add: bv_msb_def) lemma bv_msb_Cons [simp]: "bv_msb (b#bs) = b" by (simp add: bv_msb_def) lemma bv_msb_bv_not [simp]: "0 < length w ==> bv_msb (bv_not w) = (bitnot (bv_msb w))" by (cases w) simp_all lemma bv_msb_one_length [simp,intro]: "bv_msb w = 𝟭 ==> 0 < length w" by (cases w) simp_all lemma length_bv_not [simp]: "length (bv_not w) = length w" by (induct w) simp_all definition bv_to_nat :: "bit list => nat" where "bv_to_nat = foldl (%bn b. 2 * bn + bitval b) 0" lemma bv_to_nat_Nil [simp]: "bv_to_nat [] = 0" by (simp add: bv_to_nat_def) lemma bv_to_nat_helper [simp]: "bv_to_nat (b # bs) = bitval b * 2 ^ length bs + bv_to_nat bs" proof - let ?bv_to_nat' = "foldl (λbn b. 2 * bn + bitval b)" have helper: "⋀base. ?bv_to_nat' base bs = base * 2 ^ length bs + ?bv_to_nat' 0 bs" proof (induct bs) case Nil show ?case by simp next case (Cons x xs base) show ?case apply (simp only: foldl_Cons) apply (subst Cons [of "2 * base + bitval x"]) apply simp apply (subst Cons [of "bitval x"]) apply (simp add: add_mult_distrib) done qed show ?thesis by (simp add: bv_to_nat_def) (rule helper) qed lemma bv_to_nat0 [simp]: "bv_to_nat (𝟬#bs) = bv_to_nat bs" by simp lemma bv_to_nat1 [simp]: "bv_to_nat (𝟭#bs) = 2 ^ length bs + bv_to_nat bs" by simp lemma bv_to_nat_upper_range: "bv_to_nat w < 2 ^ length w" proof (induct w, simp_all) fix b bs assume "bv_to_nat bs < 2 ^ length bs" show "bitval b * 2 ^ length bs + bv_to_nat bs < 2 * 2 ^ length bs" proof (cases b, simp_all) have "bv_to_nat bs < 2 ^ length bs" by fact also have "... < 2 * 2 ^ length bs" by auto finally show "bv_to_nat bs < 2 * 2 ^ length bs" by simp next have "bv_to_nat bs < 2 ^ length bs" by fact hence "2 ^ length bs + bv_to_nat bs < 2 ^ length bs + 2 ^ length bs" by arith also have "... = 2 * (2 ^ length bs)" by simp finally show "bv_to_nat bs < 2 ^ length bs" by simp qed qed lemma bv_extend_longer [simp]: assumes wn: "n ≤ length w" shows "bv_extend n b w = w" by (simp add: bv_extend_def wn) lemma bv_extend_shorter [simp]: assumes wn: "length w < n" shows "bv_extend n b w = bv_extend n b (b#w)" proof - from wn have s: "n - Suc (length w) + 1 = n - length w" by arith have "bv_extend n b w = replicate (n - length w) b @ w" by (simp add: bv_extend_def) also have "... = replicate (n - Suc (length w) + 1) b @ w" by (subst s) rule also have "... = (replicate (n - Suc (length w)) b @ replicate 1 b) @ w" by (subst replicate_add) rule also have "... = replicate (n - Suc (length w)) b @ b # w" by simp also have "... = bv_extend n b (b#w)" by (simp add: bv_extend_def) finally show "bv_extend n b w = bv_extend n b (b#w)" . qed primrec rem_initial :: "bit => bit list => bit list" where "rem_initial b [] = []" | "rem_initial b (x#xs) = (if b = x then rem_initial b xs else x#xs)" lemma rem_initial_length: "length (rem_initial b w) ≤ length w" by (rule bit_list_induct [of _ w],simp_all (no_asm),safe,simp_all) lemma rem_initial_equal: assumes p: "length (rem_initial b w) = length w" shows "rem_initial b w = w" proof - have "length (rem_initial b w) = length w --> rem_initial b w = w" proof (induct w, simp_all, clarify) fix xs assume "length (rem_initial b xs) = length xs --> rem_initial b xs = xs" assume f: "length (rem_initial b xs) = Suc (length xs)" with rem_initial_length [of b xs] show "rem_initial b xs = b#xs" by auto qed from this and p show ?thesis .. qed lemma bv_extend_rem_initial: "bv_extend (length w) b (rem_initial b w) = w" proof (induct w, simp_all, safe) fix xs assume ind: "bv_extend (length xs) b (rem_initial b xs) = xs" from rem_initial_length [of b xs] have [simp]: "Suc (length xs) - length (rem_initial b xs) = 1 + (length xs - length (rem_initial b xs))" by arith have "bv_extend (Suc (length xs)) b (rem_initial b xs) = replicate (Suc (length xs) - length (rem_initial b xs)) b @ (rem_initial b xs)" by (simp add: bv_extend_def) also have "... = replicate (1 + (length xs - length (rem_initial b xs))) b @ rem_initial b xs" by simp also have "... = (replicate 1 b @ replicate (length xs - length (rem_initial b xs)) b) @ rem_initial b xs" by (subst replicate_add) (rule refl) also have "... = b # bv_extend (length xs) b (rem_initial b xs)" by (auto simp add: bv_extend_def [symmetric]) also have "... = b # xs" by (simp add: ind) finally show "bv_extend (Suc (length xs)) b (rem_initial b xs) = b # xs" . qed lemma rem_initial_append1: assumes "rem_initial b xs ~= []" shows "rem_initial b (xs @ ys) = rem_initial b xs @ ys" using assms by (induct xs) auto lemma rem_initial_append2: assumes "rem_initial b xs = []" shows "rem_initial b (xs @ ys) = rem_initial b ys" using assms by (induct xs) auto definition norm_unsigned :: "bit list => bit list" where "norm_unsigned = rem_initial 𝟬" lemma norm_unsigned_Nil [simp]: "norm_unsigned [] = []" by (simp add: norm_unsigned_def) lemma norm_unsigned_Cons0 [simp]: "norm_unsigned (𝟬#bs) = norm_unsigned bs" by (simp add: norm_unsigned_def) lemma norm_unsigned_Cons1 [simp]: "norm_unsigned (𝟭#bs) = 𝟭#bs" by (simp add: norm_unsigned_def) lemma norm_unsigned_idem [simp]: "norm_unsigned (norm_unsigned w) = norm_unsigned w" by (rule bit_list_induct [of _ w],simp_all) fun nat_to_bv_helper :: "nat => bit list => bit list" where "nat_to_bv_helper n bs = (if n = 0 then bs else nat_to_bv_helper (n div 2) ((if n mod 2 = 0 then 𝟬 else 𝟭)#bs))" definition nat_to_bv :: "nat => bit list" where "nat_to_bv n = nat_to_bv_helper n []" lemma nat_to_bv0 [simp]: "nat_to_bv 0 = []" by (simp add: nat_to_bv_def) lemmas [simp del] = nat_to_bv_helper.simps lemma n_div_2_cases: assumes zero: "(n::nat) = 0 ==> R" and div : "[| n div 2 < n ; 0 < n |] ==> R" shows "R" proof (cases "n = 0") assume "n = 0" thus R by (rule zero) next assume "n ~= 0" hence "0 < n" by simp hence "n div 2 < n" by arith from this and ‹0 < n› show R by (rule div) qed lemma int_wf_ge_induct: assumes ind : "!!i::int. (!!j. [| k ≤ j ; j < i |] ==> P j) ==> P i" shows "P i" proof (rule wf_induct_rule [OF wf_int_ge_less_than]) fix x assume ih: "(⋀y::int. (y, x) ∈ int_ge_less_than k ⟹ P y)" thus "P x" by (rule ind) (simp add: int_ge_less_than_def) qed lemma unfold_nat_to_bv_helper: "nat_to_bv_helper b l = nat_to_bv_helper b [] @ l" proof - have "∀l. nat_to_bv_helper b l = nat_to_bv_helper b [] @ l" proof (induct b rule: less_induct) fix n assume ind: "!!j. j < n ⟹ ∀ l. nat_to_bv_helper j l = nat_to_bv_helper j [] @ l" show "∀l. nat_to_bv_helper n l = nat_to_bv_helper n [] @ l" proof fix l show "nat_to_bv_helper n l = nat_to_bv_helper n [] @ l" proof (cases "n < 0") assume "n < 0" thus ?thesis by (simp add: nat_to_bv_helper.simps) next assume "~n < 0" show ?thesis proof (rule n_div_2_cases [of n]) assume [simp]: "n = 0" show ?thesis apply (simp only: nat_to_bv_helper.simps [of n]) apply simp done next assume n2n: "n div 2 < n" assume [simp]: "0 < n" hence n20: "0 ≤ n div 2" by arith from ind [of "n div 2"] and n2n n20 have ind': "∀l. nat_to_bv_helper (n div 2) l = nat_to_bv_helper (n div 2) [] @ l" by blast show ?thesis apply (simp only: nat_to_bv_helper.simps [of n]) apply (cases "n=0") apply simp apply (simp only: if_False) apply simp apply (subst spec [OF ind',of "𝟬#l"]) apply (subst spec [OF ind',of "𝟭#l"]) apply (subst spec [OF ind',of "[𝟭]"]) apply (subst spec [OF ind',of "[𝟬]"]) apply simp done qed qed qed qed thus ?thesis .. qed 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 𝟭]" proof - assume n: "n≠0" show ?thesis apply (subst nat_to_bv_def [of n]) apply (simp only: nat_to_bv_helper.simps [of n]) apply (subst unfold_nat_to_bv_helper) apply (simp add: n) apply (subst nat_to_bv_def [of "n div 2"]) apply auto done qed lemma bv_to_nat_dist_append: "bv_to_nat (l1 @ l2) = bv_to_nat l1 * 2 ^ length l2 + bv_to_nat l2" proof - have "∀l2. bv_to_nat (l1 @ l2) = bv_to_nat l1 * 2 ^ length l2 + bv_to_nat l2" proof (induct l1, simp_all) fix x xs assume ind: "∀l2. bv_to_nat (xs @ l2) = bv_to_nat xs * 2 ^ length l2 + bv_to_nat l2" 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" proof fix l2 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" proof - have "(2::nat) ^ (length xs + length l2) = 2 ^ length xs * 2 ^ length l2" by (induct ("length xs")) simp_all hence "bitval x * 2 ^ (length xs + length l2) + bv_to_nat xs * 2 ^ length l2 = bitval x * 2 ^ length xs * 2 ^ length l2 + bv_to_nat xs * 2 ^ length l2" by simp also have "... = (bitval x * 2 ^ length xs + bv_to_nat xs) * 2 ^ length l2" by (simp add: ring_distribs) finally show ?thesis by simp qed qed qed thus ?thesis .. qed lemma bv_nat_bv [simp]: "bv_to_nat (nat_to_bv n) = n" proof (induct n rule: less_induct) fix n assume ind: "!!j. j < n ⟹ bv_to_nat (nat_to_bv j) = j" show "bv_to_nat (nat_to_bv n) = n" proof (rule n_div_2_cases [of n]) assume "n = 0" then show ?thesis by simp next assume nn: "n div 2 < n" assume n0: "0 < n" from ind and nn have ind': "bv_to_nat (nat_to_bv (n div 2)) = n div 2" by blast from n0 have n0': "n ≠ 0" by simp show ?thesis apply (subst nat_to_bv_def) apply (simp only: nat_to_bv_helper.simps [of n]) apply (simp only: n0' if_False) apply (subst unfold_nat_to_bv_helper) apply (subst bv_to_nat_dist_append) apply (fold nat_to_bv_def) apply (simp add: ind' split del: if_split) apply (cases "n mod 2 = 0") proof (simp_all) assume "n mod 2 = 0" with div_mult_mod_eq [of n 2] show "n div 2 * 2 = n" by simp next assume "n mod 2 = Suc 0" with div_mult_mod_eq [of n 2] show "Suc (n div 2 * 2) = n" by arith qed qed qed lemma bv_to_nat_type [simp]: "bv_to_nat (norm_unsigned w) = bv_to_nat w" by (rule bit_list_induct) simp_all lemma length_norm_unsigned_le [simp]: "length (norm_unsigned w) ≤ length w" by (rule bit_list_induct) simp_all lemma bv_to_nat_rew_msb: "bv_msb w = 𝟭 ==> bv_to_nat w = 2 ^ (length w - 1) + bv_to_nat (tl w)" by (rule bit_list_cases [of w]) simp_all lemma norm_unsigned_result: "norm_unsigned xs = [] ∨ bv_msb (norm_unsigned xs) = 𝟭" proof (rule length_induct [of _ xs]) fix xs :: "bit list" assume ind: "∀ys. length ys < length xs --> norm_unsigned ys = [] ∨ bv_msb (norm_unsigned ys) = 𝟭" show "norm_unsigned xs = [] ∨ bv_msb (norm_unsigned xs) = 𝟭" proof (rule bit_list_cases [of xs],simp_all) fix bs assume [simp]: "xs = 𝟬#bs" from ind have "length bs < length xs --> norm_unsigned bs = [] ∨ bv_msb (norm_unsigned bs) = 𝟭" .. thus "norm_unsigned bs = [] ∨ bv_msb (norm_unsigned bs) = 𝟭" by simp qed qed lemma norm_empty_bv_to_nat_zero: assumes nw: "norm_unsigned w = []" shows "bv_to_nat w = 0" proof - have "bv_to_nat w = bv_to_nat (norm_unsigned w)" by simp also have "... = bv_to_nat []" by (subst nw) (rule refl) also have "... = 0" by simp finally show ?thesis . qed lemma bv_to_nat_lower_limit: assumes w0: "0 < bv_to_nat w" shows "2 ^ (length (norm_unsigned w) - 1) ≤ bv_to_nat w" proof - from w0 and norm_unsigned_result [of w] have msbw: "bv_msb (norm_unsigned w) = 𝟭" by (auto simp add: norm_empty_bv_to_nat_zero) have "2 ^ (length (norm_unsigned w) - 1) ≤ bv_to_nat (norm_unsigned w)" by (subst bv_to_nat_rew_msb [OF msbw],simp) thus ?thesis by simp qed lemmas [simp del] = nat_to_bv_non0 lemma norm_unsigned_length [intro!]: "length (norm_unsigned w) ≤ length w" by (subst norm_unsigned_def,rule rem_initial_length) lemma norm_unsigned_equal: "length (norm_unsigned w) = length w ==> norm_unsigned w = w" by (simp add: norm_unsigned_def,rule rem_initial_equal) lemma bv_extend_norm_unsigned: "bv_extend (length w) 𝟬 (norm_unsigned w) = w" by (simp add: norm_unsigned_def,rule bv_extend_rem_initial) lemma norm_unsigned_append1 [simp]: "norm_unsigned xs ≠ [] ==> norm_unsigned (xs @ ys) = norm_unsigned xs @ ys" by (simp add: norm_unsigned_def,rule rem_initial_append1) lemma norm_unsigned_append2 [simp]: "norm_unsigned xs = [] ==> norm_unsigned (xs @ ys) = norm_unsigned ys" by (simp add: norm_unsigned_def,rule rem_initial_append2) lemma bv_to_nat_zero_imp_empty: "bv_to_nat w = 0 ⟹ norm_unsigned w = []" by (atomize (full), induct w rule: bit_list_induct) simp_all lemma bv_to_nat_nzero_imp_nempty: "bv_to_nat w ≠ 0 ⟹ norm_unsigned w ≠ []" by (induct w rule: bit_list_induct) simp_all lemma nat_helper1: assumes ass: "nat_to_bv (bv_to_nat w) = norm_unsigned w" shows "nat_to_bv (2 * bv_to_nat w + bitval x) = norm_unsigned (w @ [x])" proof (cases x) assume [simp]: "x = 𝟭" have "nat_to_bv (Suc (2 * bv_to_nat w) div 2) @ [𝟭] = nat_to_bv ((1 + 2 * bv_to_nat w) div 2) @ [𝟭]" by (simp add: add.commute) also have "... = nat_to_bv (bv_to_nat w) @ [𝟭]" by (subst div_add1_eq) simp also have "... = norm_unsigned w @ [𝟭]" by (subst ass) (rule refl) also have "... = norm_unsigned (w @ [𝟭])" by (cases "norm_unsigned w") simp_all finally have "nat_to_bv (Suc (2 * bv_to_nat w) div 2) @ [𝟭] = norm_unsigned (w @ [𝟭])" . then show ?thesis by (simp add: nat_to_bv_non0) next assume [simp]: "x = 𝟬" show ?thesis proof (cases "bv_to_nat w = 0") assume "bv_to_nat w = 0" thus ?thesis by (simp add: bv_to_nat_zero_imp_empty) next assume "bv_to_nat w ≠ 0" thus ?thesis apply simp apply (subst nat_to_bv_non0) apply simp apply auto apply (subst ass) apply (cases "norm_unsigned w") apply (simp_all add: norm_empty_bv_to_nat_zero) done qed qed lemma nat_helper2: "nat_to_bv (2 ^ length xs + bv_to_nat xs) = 𝟭 # xs" proof - have "∀xs. nat_to_bv (2 ^ length (rev xs) + bv_to_nat (rev xs)) = 𝟭 # (rev xs)" (is "∀xs. ?P xs") proof fix xs show "?P xs" proof (rule length_induct [of _ xs]) fix xs :: "bit list" assume ind: "∀ys. length ys < length xs --> ?P ys" show "?P xs" proof (cases xs) assume "xs = []" then show ?thesis by (simp add: nat_to_bv_non0) next fix y ys assume [simp]: "xs = y # ys" show ?thesis apply simp apply (subst bv_to_nat_dist_append) apply simp proof - have "nat_to_bv (2 * 2 ^ length ys + (bv_to_nat (rev ys) * 2 + bitval y)) = nat_to_bv (2 * (2 ^ length ys + bv_to_nat (rev ys)) + bitval y)" by (simp add: ac_simps ac_simps) also have "... = nat_to_bv (2 * (bv_to_nat (𝟭#rev ys)) + bitval y)" by simp also have "... = norm_unsigned (𝟭#rev ys) @ [y]" proof - from ind have "nat_to_bv (2 ^ length (rev ys) + bv_to_nat (rev ys)) = 𝟭 # rev ys" by auto hence [simp]: "nat_to_bv (2 ^ length ys + bv_to_nat (rev ys)) = 𝟭 # rev ys" by simp show ?thesis apply (subst nat_helper1) apply simp_all done qed also have "... = (𝟭#rev ys) @ [y]" by simp also have "... = 𝟭 # rev ys @ [y]" by simp finally show "nat_to_bv (2 * 2 ^ length ys + (bv_to_nat (rev ys) * 2 + bitval y)) = 𝟭 # rev ys @ [y]" . qed qed qed qed hence "nat_to_bv (2 ^ length (rev (rev xs)) + bv_to_nat (rev (rev xs))) = 𝟭 # rev (rev xs)" .. thus ?thesis by simp qed lemma nat_bv_nat [simp]: "nat_to_bv (bv_to_nat w) = norm_unsigned w" proof (rule bit_list_induct [of _ w],simp_all) fix xs assume "nat_to_bv (bv_to_nat xs) = norm_unsigned xs" have "bv_to_nat xs = bv_to_nat (norm_unsigned xs)" by simp have "bv_to_nat xs < 2 ^ length xs" by (rule bv_to_nat_upper_range) show "nat_to_bv (2 ^ length xs + bv_to_nat xs) = 𝟭 # xs" by (rule nat_helper2) qed lemma bv_to_nat_qinj: assumes one: "bv_to_nat xs = bv_to_nat ys" and len: "length xs = length ys" shows "xs = ys" proof - from one have "nat_to_bv (bv_to_nat xs) = nat_to_bv (bv_to_nat ys)" by simp hence xsys: "norm_unsigned xs = norm_unsigned ys" by simp have "xs = bv_extend (length xs) 𝟬 (norm_unsigned xs)" by (simp add: bv_extend_norm_unsigned) also have "... = bv_extend (length ys) 𝟬 (norm_unsigned ys)" by (simp add: xsys len) also have "... = ys" by (simp add: bv_extend_norm_unsigned) finally show ?thesis . qed lemma norm_unsigned_nat_to_bv [simp]: "norm_unsigned (nat_to_bv n) = nat_to_bv n" proof - have "norm_unsigned (nat_to_bv n) = nat_to_bv (bv_to_nat (norm_unsigned (nat_to_bv n)))" by (subst nat_bv_nat) simp also have "... = nat_to_bv n" by simp finally show ?thesis . qed lemma length_nat_to_bv_upper_limit: assumes nk: "n ≤ 2 ^ k - 1" shows "length (nat_to_bv n) ≤ k" proof (cases "n = 0") case True thus ?thesis by (simp add: nat_to_bv_def nat_to_bv_helper.simps) next case False hence n0: "0 < n" by simp show ?thesis proof (rule ccontr) assume "~ length (nat_to_bv n) ≤ k" hence "k < length (nat_to_bv n)" by simp hence "k ≤ length (nat_to_bv n) - 1" by arith hence "(2::nat) ^ k ≤ 2 ^ (length (nat_to_bv n) - 1)" by simp also have "... = 2 ^ (length (norm_unsigned (nat_to_bv n)) - 1)" by simp also have "... ≤ bv_to_nat (nat_to_bv n)" by (rule bv_to_nat_lower_limit) (simp add: n0) also have "... = n" by simp finally have "2 ^ k ≤ n" . with n0 have "2 ^ k - 1 < n" by arith with nk show False by simp qed qed lemma length_nat_to_bv_lower_limit: assumes nk: "2 ^ k ≤ n" shows "k < length (nat_to_bv n)" proof (rule ccontr) assume "~ k < length (nat_to_bv n)" hence lnk: "length (nat_to_bv n) ≤ k" by simp have "n = bv_to_nat (nat_to_bv n)" by simp also have "... < 2 ^ length (nat_to_bv n)" by (rule bv_to_nat_upper_range) also from lnk have "... ≤ 2 ^ k" by simp finally have "n < 2 ^ k" . with nk show False by simp qed subsection ‹Unsigned Arithmetic Operations› definition bv_add :: "[bit list, bit list ] => bit list" where "bv_add w1 w2 = nat_to_bv (bv_to_nat w1 + bv_to_nat w2)" lemma bv_add_type1 [simp]: "bv_add (norm_unsigned w1) w2 = bv_add w1 w2" by (simp add: bv_add_def) lemma bv_add_type2 [simp]: "bv_add w1 (norm_unsigned w2) = bv_add w1 w2" by (simp add: bv_add_def) lemma bv_add_returntype [simp]: "norm_unsigned (bv_add w1 w2) = bv_add w1 w2" by (simp add: bv_add_def) lemma bv_add_length: "length (bv_add w1 w2) ≤ Suc (max (length w1) (length w2))" proof (unfold bv_add_def,rule length_nat_to_bv_upper_limit) from bv_to_nat_upper_range [of w1] and bv_to_nat_upper_range [of w2] have "bv_to_nat w1 + bv_to_nat w2 ≤ (2 ^ length w1 - 1) + (2 ^ length w2 - 1)" by arith also have "... ≤ max (2 ^ length w1 - 1) (2 ^ length w2 - 1) + max (2 ^ length w1 - 1) (2 ^ length w2 - 1)" by (rule add_mono,safe intro!: max.cobounded1 max.cobounded2) also have "... = 2 * max (2 ^ length w1 - 1) (2 ^ length w2 - 1)" by simp also have "... ≤ 2 ^ Suc (max (length w1) (length w2)) - 2" proof (cases "length w1 ≤ length w2") assume w1w2: "length w1 ≤ length w2" hence "(2::nat) ^ length w1 ≤ 2 ^ length w2" by simp hence "(2::nat) ^ length w1 - 1 ≤ 2 ^ length w2 - 1" by arith with w1w2 show ?thesis by (simp add: diff_mult_distrib2 split: split_max) next assume [simp]: "~ (length w1 ≤ length w2)" have "~ ((2::nat) ^ length w1 - 1 ≤ 2 ^ length w2 - 1)" proof assume "(2::nat) ^ length w1 - 1 ≤ 2 ^ length w2 - 1" hence "((2::nat) ^ length w1 - 1) + 1 ≤ (2 ^ length w2 - 1) + 1" by (rule add_right_mono) hence "(2::nat) ^ length w1 ≤ 2 ^ length w2" by simp hence "length w1 ≤ length w2" by simp thus False by simp qed thus ?thesis by (simp add: diff_mult_distrib2 split: split_max) qed finally show "bv_to_nat w1 + bv_to_nat w2 ≤ 2 ^ Suc (max (length w1) (length w2)) - 1" by arith qed definition bv_mult :: "[bit list, bit list ] => bit list" where "bv_mult w1 w2 = nat_to_bv (bv_to_nat w1 * bv_to_nat w2)" lemma bv_mult_type1 [simp]: "bv_mult (norm_unsigned w1) w2 = bv_mult w1 w2" by (simp add: bv_mult_def) lemma bv_mult_type2 [simp]: "bv_mult w1 (norm_unsigned w2) = bv_mult w1 w2" by (simp add: bv_mult_def) lemma bv_mult_returntype [simp]: "norm_unsigned (bv_mult w1 w2) = bv_mult w1 w2" by (simp add: bv_mult_def) lemma bv_mult_length: "length (bv_mult w1 w2) ≤ length w1 + length w2" proof (unfold bv_mult_def,rule length_nat_to_bv_upper_limit) from bv_to_nat_upper_range [of w1] and bv_to_nat_upper_range [of w2] have h: "bv_to_nat w1 ≤ 2 ^ length w1 - 1 ∧ bv_to_nat w2 ≤ 2 ^ length w2 - 1" by arith have "bv_to_nat w1 * bv_to_nat w2 ≤ (2 ^ length w1 - 1) * (2 ^ length w2 - 1)" apply (cut_tac h) apply (rule mult_mono) apply auto done also have "... < 2 ^ length w1 * 2 ^ length w2" by (rule mult_strict_mono,auto) also have "... = 2 ^ (length w1 + length w2)" by (simp add: power_add) finally show "bv_to_nat w1 * bv_to_nat w2 ≤ 2 ^ (length w1 + length w2) - 1" by arith qed subsection ‹Signed Vectors› primrec norm_signed :: "bit list => bit list" where norm_signed_Nil: "norm_signed [] = []" | norm_signed_Cons: "norm_signed (b#bs) = (case b of 𝟬 => if norm_unsigned bs = [] then [] else b#norm_unsigned bs | 𝟭 => b#rem_initial b bs)" lemma norm_signed0 [simp]: "norm_signed [𝟬] = []" by simp lemma norm_signed1 [simp]: "norm_signed [𝟭] = [𝟭]" by simp lemma norm_signed01 [simp]: "norm_signed (𝟬#𝟭#xs) = 𝟬#𝟭#xs" by simp lemma norm_signed00 [simp]: "norm_signed (𝟬#𝟬#xs) = norm_signed (𝟬#xs)" by simp lemma norm_signed10 [simp]: "norm_signed (𝟭#𝟬#xs) = 𝟭#𝟬#xs" by simp lemma norm_signed11 [simp]: "norm_signed (𝟭#𝟭#xs) = norm_signed (𝟭#xs)" by simp lemmas [simp del] = norm_signed_Cons definition int_to_bv :: "int => bit list" where "int_to_bv n = (if 0 ≤ n then norm_signed (𝟬#nat_to_bv (nat n)) else norm_signed (bv_not (𝟬#nat_to_bv (nat (-n- 1)))))" lemma int_to_bv_ge0 [simp]: "0 ≤ n ==> int_to_bv n = norm_signed (𝟬 # nat_to_bv (nat n))" by (simp add: int_to_bv_def) lemma int_to_bv_lt0 [simp]: "n < 0 ==> int_to_bv n = norm_signed (bv_not (𝟬#nat_to_bv (nat (-n- 1))))" by (simp add: int_to_bv_def) lemma norm_signed_idem [simp]: "norm_signed (norm_signed w) = norm_signed w" proof (rule bit_list_induct [of _ w], simp_all) fix xs assume eq: "norm_signed (norm_signed xs) = norm_signed xs" show "norm_signed (norm_signed (𝟬#xs)) = norm_signed (𝟬#xs)" proof (rule bit_list_cases [of xs],simp_all) fix ys assume "xs = 𝟬#ys" from this [symmetric] and eq show "norm_signed (norm_signed (𝟬#ys)) = norm_signed (𝟬#ys)" by simp qed next fix xs assume eq: "norm_signed (norm_signed xs) = norm_signed xs" show "norm_signed (norm_signed (𝟭#xs)) = norm_signed (𝟭#xs)" proof (rule bit_list_cases [of xs],simp_all) fix ys assume "xs = 𝟭#ys" from this [symmetric] and eq show "norm_signed (norm_signed (𝟭#ys)) = norm_signed (𝟭#ys)" by simp qed qed definition bv_to_int :: "bit list => int" where "bv_to_int w = (case bv_msb w of 𝟬 => int (bv_to_nat w) | 𝟭 => - int (bv_to_nat (bv_not w) + 1))" lemma bv_to_int_Nil [simp]: "bv_to_int [] = 0" by (simp add: bv_to_int_def) lemma bv_to_int_Cons0 [simp]: "bv_to_int (𝟬#bs) = int (bv_to_nat bs)" by (simp add: bv_to_int_def) lemma bv_to_int_Cons1 [simp]: "bv_to_int (𝟭#bs) = - int (bv_to_nat (bv_not bs) + 1)" by (simp add: bv_to_int_def) lemma bv_to_int_type [simp]: "bv_to_int (norm_signed w) = bv_to_int w" proof (rule bit_list_induct [of _ w], simp_all) fix xs assume ind: "bv_to_int (norm_signed xs) = bv_to_int xs" show "bv_to_int (norm_signed (𝟬#xs)) = int (bv_to_nat xs)" proof (rule bit_list_cases [of xs], simp_all) fix ys assume [simp]: "xs = 𝟬#ys" from ind show "bv_to_int (norm_signed (𝟬#ys)) = int (bv_to_nat ys)" by simp qed next fix xs assume ind: "bv_to_int (norm_signed xs) = bv_to_int xs" show "bv_to_int (norm_signed (𝟭#xs)) = -1 - int (bv_to_nat (bv_not xs))" proof (rule bit_list_cases [of xs], simp_all) fix ys assume [simp]: "xs = 𝟭#ys" from ind show "bv_to_int (norm_signed (𝟭#ys)) = -1 - int (bv_to_nat (bv_not ys))" by simp qed qed lemma bv_to_int_upper_range: "bv_to_int w < 2 ^ (length w - 1)" proof (rule bit_list_cases [of w],simp_all add: bv_to_nat_upper_range) fix bs have "-1 - int (bv_to_nat (bv_not bs)) ≤ 0" by simp also have "... < 2 ^ length bs" by (induct bs) simp_all finally show "-1 - int (bv_to_nat (bv_not bs)) < 2 ^ length bs" . qed lemma bv_to_int_lower_range: "- (2 ^ (length w - 1)) ≤ bv_to_int w" proof (rule bit_list_cases [of w],simp_all) fix bs :: "bit list" have "- (2 ^ length bs) ≤ (0::int)" by (induct bs) simp_all also have "... ≤ int (bv_to_nat bs)" by simp finally show "- (2 ^ length bs) ≤ int (bv_to_nat bs)" . next fix bs from bv_to_nat_upper_range [of "bv_not bs"] show "- (2 ^ length bs) ≤ -1 - int (bv_to_nat (bv_not bs))" apply (simp add: algebra_simps) by (metis of_nat_power add.commute not_less of_nat_numeral zle_add1_eq_le of_nat_le_iff) qed lemma int_bv_int [simp]: "int_to_bv (bv_to_int w) = norm_signed w" proof (rule bit_list_cases [of w],simp) fix xs assume [simp]: "w = 𝟬#xs" show ?thesis apply simp apply (subst norm_signed_Cons [of "𝟬" "xs"]) apply simp using norm_unsigned_result [of xs] apply safe apply (rule bit_list_cases [of "norm_unsigned xs"]) apply simp_all done next fix xs assume [simp]: "w = 𝟭#xs" show ?thesis apply (simp del: int_to_bv_lt0) apply (rule bit_list_induct [of _ xs], simp) apply (subst int_to_bv_lt0) apply linarith apply simp apply (metis add.commute bitnot_zero bv_not_Cons bv_not_bv_not int_nat_two_exp length_bv_not nat_helper2 nat_int norm_signed10 of_nat_add) apply simp done qed lemma bv_int_bv [simp]: "bv_to_int (int_to_bv i) = i" by (cases "0 ≤ i") simp_all lemma bv_msb_norm [simp]: "bv_msb (norm_signed w) = bv_msb w" by (rule bit_list_cases [of w]) (simp_all add: norm_signed_Cons) lemma norm_signed_length: "length (norm_signed w) ≤ length w" apply (cases w, simp_all) apply (subst norm_signed_Cons) apply (case_tac a, simp_all) apply (rule rem_initial_length) done lemma norm_signed_equal: "length (norm_signed w) = length w ==> norm_signed w = w" proof (rule bit_list_cases [of w], simp_all) fix xs assume "length (norm_signed (𝟬#xs)) = Suc (length xs)" thus "norm_signed (𝟬#xs) = 𝟬#xs" by (simp add: norm_signed_Cons norm_unsigned_equal [THEN eqTrueI] split: if_split_asm) next fix xs assume "length (norm_signed (𝟭#xs)) = Suc (length xs)" thus "norm_signed (𝟭#xs) = 𝟭#xs" apply (simp add: norm_signed_Cons) apply (rule rem_initial_equal) apply assumption done qed lemma bv_extend_norm_signed: "bv_msb w = b ==> bv_extend (length w) b (norm_signed w) = w" proof (rule bit_list_cases [of w],simp_all) fix xs show "bv_extend (Suc (length xs)) 𝟬 (norm_signed (𝟬#xs)) = 𝟬#xs" proof (simp add: norm_signed_def,auto) assume "norm_unsigned xs = []" hence xx: "rem_initial 𝟬 xs = []" by (simp add: norm_unsigned_def) have "bv_extend (Suc (length xs)) 𝟬 (𝟬#rem_initial 𝟬 xs) = 𝟬#xs" apply (simp add: bv_extend_def replicate_app_Cons_same) apply (fold bv_extend_def) apply (rule bv_extend_rem_initial) done thus "bv_extend (Suc (length xs)) 𝟬 [𝟬] = 𝟬#xs" by (simp add: xx) next show "bv_extend (Suc (length xs)) 𝟬 (𝟬#norm_unsigned xs) = 𝟬#xs" apply (simp add: norm_unsigned_def) apply (simp add: bv_extend_def replicate_app_Cons_same) apply (fold bv_extend_def) apply (rule bv_extend_rem_initial) done qed next fix xs show "bv_extend (Suc (length xs)) 𝟭 (norm_signed (𝟭#xs)) = 𝟭#xs" apply (simp add: norm_signed_Cons) apply (simp add: bv_extend_def replicate_app_Cons_same) apply (fold bv_extend_def) apply (rule bv_extend_rem_initial) done qed lemma bv_to_int_qinj: assumes one: "bv_to_int xs = bv_to_int ys" and len: "length xs = length ys" shows "xs = ys" proof - from one have "int_to_bv (bv_to_int xs) = int_to_bv (bv_to_int ys)" by simp hence xsys: "norm_signed xs = norm_signed ys" by simp hence xsys': "bv_msb xs = bv_msb ys" proof - have "bv_msb xs = bv_msb (norm_signed xs)" by simp also have "... = bv_msb (norm_signed ys)" by (simp add: xsys) also have "... = bv_msb ys" by simp finally show ?thesis . qed have "xs = bv_extend (length xs) (bv_msb xs) (norm_signed xs)" by (simp add: bv_extend_norm_signed) also have "... = bv_extend (length ys) (bv_msb ys) (norm_signed ys)" by (simp add: xsys xsys' len) also have "... = ys" by (simp add: bv_extend_norm_signed) finally show ?thesis . qed lemma int_to_bv_returntype [simp]: "norm_signed (int_to_bv w) = int_to_bv w" by (simp add: int_to_bv_def) lemma bv_to_int_msb0: "0 ≤ bv_to_int w1 ==> bv_msb w1 = 𝟬" by (rule bit_list_cases,simp_all) lemma bv_to_int_msb1: "bv_to_int w1 < 0 ==> bv_msb w1 = 𝟭" by (rule bit_list_cases,simp_all) lemma bv_to_int_lower_limit_gt0: assumes w0: "0 < bv_to_int w" shows "2 ^ (length (norm_signed w) - 2) ≤ bv_to_int w" proof - from w0 have "0 ≤ bv_to_int w" by simp hence [simp]: "bv_msb w = 𝟬" by (rule bv_to_int_msb0) have "2 ^ (length (norm_signed w) - 2) ≤ bv_to_int (norm_signed w)" proof (rule bit_list_cases [of w]) assume "w = []" with w0 show ?thesis by simp next fix w' assume weq: "w = 𝟬 # w'" thus ?thesis proof (simp add: norm_signed_Cons,safe) assume "norm_unsigned w' = []" with weq and w0 show False by (simp add: norm_empty_bv_to_nat_zero) next assume w'0: "norm_unsigned w' ≠ []" have "0 < bv_to_nat w'" proof (rule ccontr) assume "~ (0 < bv_to_nat w')" hence "bv_to_nat w' = 0" by arith hence "norm_unsigned w' = []" by (simp add: bv_to_nat_zero_imp_empty) with w'0 show False by simp qed with bv_to_nat_lower_limit [of w'] show "2 ^ (length (norm_unsigned w') - Suc 0) ≤ bv_to_nat w'" using One_nat_def int_nat_two_exp by presburger qed next fix w' assume weq: "w = 𝟭 # w'" from w0 have "bv_msb w = 𝟬" by simp with weq show ?thesis by simp qed also have "... = bv_to_int w" by simp finally show ?thesis . qed lemma norm_signed_result: "norm_signed w = [] ∨ norm_signed w = [𝟭] ∨ bv_msb (norm_signed w) ≠ bv_msb (tl (norm_signed w))" apply (rule bit_list_cases [of w],simp_all) apply (case_tac "bs",simp_all) apply (case_tac "a",simp_all) apply (simp add: norm_signed_Cons) apply safe apply simp proof - fix l assume msb: "𝟬 = bv_msb (norm_unsigned l)" assume "norm_unsigned l ≠ []" with norm_unsigned_result [of l] have "bv_msb (norm_unsigned l) = 𝟭" by simp with msb show False by simp next fix xs assume p: "𝟭 = bv_msb (tl (norm_signed (𝟭 # xs)))" have "𝟭 ≠ bv_msb (tl (norm_signed (𝟭 # xs)))" by (rule bit_list_induct [of _ xs],simp_all) with p show False by simp qed lemma bv_to_int_upper_limit_lem1: assumes w0: "bv_to_int w < -1" shows "bv_to_int w < - (2 ^ (length (norm_signed w) - 2))" proof - from w0 have "bv_to_int w < 0" by simp hence msbw [simp]: "bv_msb w = 𝟭" by (rule bv_to_int_msb1) have "bv_to_int w = bv_to_int (norm_signed w)" by simp also from norm_signed_result [of w] have "... < - (2 ^ (length (norm_signed w) - 2))" proof safe assume "norm_signed w = []" hence "bv_to_int (norm_signed w) = 0" by simp with w0 show ?thesis by simp next assume "norm_signed w = [𝟭]" hence "bv_to_int (norm_signed w) = -1" by simp with w0 show ?thesis by simp next assume "bv_msb (norm_signed w) ≠ bv_msb (tl (norm_signed w))" hence msb_tl: "𝟭 ≠ bv_msb (tl (norm_signed w))" by simp show "bv_to_int (norm_signed w) < - (2 ^ (length (norm_signed w) - 2))" proof (rule bit_list_cases [of "norm_signed w"]) assume "norm_signed w = []" hence "bv_to_int (norm_signed w) = 0" by simp with w0 show ?thesis by simp next fix w' assume nw: "norm_signed w = 𝟬 # w'" from msbw have "bv_msb (norm_signed w) = 𝟭" by simp with nw show ?thesis by simp next fix w' assume weq: "norm_signed w = 𝟭 # w'" show ?thesis proof (rule bit_list_cases [of w']) assume w'eq: "w' = []" from w0 have "bv_to_int (norm_signed w) < -1" by simp with w'eq and weq show ?thesis by simp next fix w'' assume w'eq: "w' = 𝟬 # w''" show ?thesis by (simp add: weq w'eq) next fix w'' assume w'eq: "w' = 𝟭 # w''" with weq and msb_tl show ?thesis by simp qed qed qed finally show ?thesis . qed lemma length_int_to_bv_upper_limit_gt0: assumes w0: "0 < i" and wk: "i ≤ 2 ^ (k - 1) - 1" shows "length (int_to_bv i) ≤ k" proof (rule ccontr) from w0 wk have k1: "1 < k" by (cases "k - 1",simp_all) assume "~ length (int_to_bv i) ≤ k" hence "k < length (int_to_bv i)" by simp hence "k ≤ length (int_to_bv i) - 1" by arith hence a: "k - 1 ≤ length (int_to_bv i) - 2" by arith hence "(2::int) ^ (k - 1) ≤ 2 ^ (length (int_to_bv i) - 2)" by simp also have "... ≤ i" proof - have "2 ^ (length (norm_signed (int_to_bv i)) - 2) ≤ bv_to_int (int_to_bv i)" proof (rule bv_to_int_lower_limit_gt0) from w0 show "0 < bv_to_int (int_to_bv i)" by simp qed thus ?thesis by simp qed finally have "2 ^ (k - 1) ≤ i" . with wk show False by simp qed lemma pos_length_pos: assumes i0: "0 < bv_to_int w" shows "0 < length w" proof - from norm_signed_result [of w] have "0 < length (norm_signed w)" proof (auto) assume ii: "norm_signed w = []" have "bv_to_int (norm_signed w) = 0" by (subst ii) simp hence "bv_to_int w = 0" by simp with i0 show False by simp next assume ii: "norm_signed w = []" assume jj: "bv_msb w ≠ 𝟬" have "𝟬 = bv_msb (norm_signed w)" by (subst ii) simp also have "... ≠ 𝟬" by (simp add: jj) finally show False by simp qed also have "... ≤ length w" by (rule norm_signed_length) finally show ?thesis . qed lemma neg_length_pos: assumes i0: "bv_to_int w < -1" shows "0 < length w" proof - from norm_signed_result [of w] have "0 < length (norm_signed w)" proof (auto) assume ii: "norm_signed w = []" have "bv_to_int (norm_signed w) = 0" by (subst ii) simp hence "bv_to_int w = 0" by simp with i0 show False by simp next assume ii: "norm_signed w = []" assume jj: "bv_msb w ≠ 𝟬" have "𝟬 = bv_msb (norm_signed w)" by (subst ii) simp also have "... ≠ 𝟬" by (simp add: jj) finally show False by simp qed also have "... ≤ length w" by (rule norm_signed_length) finally show ?thesis . qed lemma length_int_to_bv_lower_limit_gt0: assumes wk: "2 ^ (k - 1) ≤ i" shows "k < length (int_to_bv i)" proof (rule ccontr) have "0 < (2::int) ^ (k - 1)" by (rule zero_less_power) simp also have "... ≤ i" by (rule wk) finally have i0: "0 < i" . have lii0: "0 < length (int_to_bv i)" apply (rule pos_length_pos) apply (simp,rule i0) done assume "~ k < length (int_to_bv i)" hence "length (int_to_bv i) ≤ k" by simp with lii0 have a: "length (int_to_bv i) - 1 ≤ k - 1" by arith have "i < 2 ^ (length (int_to_bv i) - 1)" proof - have "i = bv_to_int (int_to_bv i)" by simp also have "... < 2 ^ (length (int_to_bv i) - 1)" by (rule bv_to_int_upper_range) finally show ?thesis . qed also have "(2::int) ^ (length (int_to_bv i) - 1) ≤ 2 ^ (k - 1)" using a by simp finally have "i < 2 ^ (k - 1)" . with wk show False by simp qed lemma length_int_to_bv_upper_limit_lem1: assumes w1: "i < -1" and wk: "- (2 ^ (k - 1)) ≤ i" shows "length (int_to_bv i) ≤ k" proof (rule ccontr) from w1 wk have k1: "1 < k" by (cases "k - 1") simp_all assume "~ length (int_to_bv i) ≤ k" hence "k < length (int_to_bv i)" by simp hence "k ≤ length (int_to_bv i) - 1" by arith hence a: "k - 1 ≤ length (int_to_bv i) - 2" by arith have "i < - (2 ^ (length (int_to_bv i) - 2))" proof - have "i = bv_to_int (int_to_bv i)" by simp also have "... < - (2 ^ (length (norm_signed (int_to_bv i)) - 2))" by (rule bv_to_int_upper_limit_lem1,simp,rule w1) finally show ?thesis by simp qed also have "... ≤ -(2 ^ (k - 1))" proof - have "(2::int) ^ (k - 1) ≤ 2 ^ (length (int_to_bv i) - 2)" using a by simp thus ?thesis by simp qed finally have "i < -(2 ^ (k - 1))" . with wk show False by simp qed lemma length_int_to_bv_lower_limit_lem1: assumes wk: "i < -(2 ^ (k - 1))" shows "k < length (int_to_bv i)" proof (rule ccontr) from wk have "i ≤ -(2 ^ (k - 1)) - 1" by simp also have "... < -1" proof - have "0 < (2::int) ^ (k - 1)" by (rule zero_less_power) simp hence "-((2::int) ^ (k - 1)) < 0" by simp thus ?thesis by simp qed finally have i1: "i < -1" . have lii0: "0 < length (int_to_bv i)" apply (rule neg_length_pos) apply (simp, rule i1) done assume "~ k < length (int_to_bv i)" hence "length (int_to_bv i) ≤ k" by simp with lii0 have a: "length (int_to_bv i) - 1 ≤ k - 1" by arith hence "(2::int) ^ (length (int_to_bv i) - 1) ≤ 2 ^ (k - 1)" by simp hence "-((2::int) ^ (k - 1)) ≤ - (2 ^ (length (int_to_bv i) - 1))" by simp also have "... ≤ i" proof - have "- (2 ^ (length (int_to_bv i) - 1)) ≤ bv_to_int (int_to_bv i)" by (rule bv_to_int_lower_range) also have "... = i" by simp finally show ?thesis . qed finally have "-(2 ^ (k - 1)) ≤ i" . with wk show False by simp qed subsection ‹Signed Arithmetic Operations› subsubsection ‹Conversion from unsigned to signed› definition utos :: "bit list => bit list" where "utos w = norm_signed (𝟬 # w)" lemma utos_type [simp]: "utos (norm_unsigned w) = utos w" by (simp add: utos_def norm_signed_Cons) lemma utos_returntype [simp]: "norm_signed (utos w) = utos w" by (simp add: utos_def) lemma utos_length: "length (utos w) ≤ Suc (length w)" by (simp add: utos_def norm_signed_Cons) lemma bv_to_int_utos: "bv_to_int (utos w) = int (bv_to_nat w)" proof (simp add: utos_def norm_signed_Cons, safe) assume "norm_unsigned w = []" hence "bv_to_nat (norm_unsigned w) = 0" by simp thus "bv_to_nat w = 0" by simp qed subsubsection ‹Unary minus› definition bv_uminus :: "bit list => bit list" where "bv_uminus w = int_to_bv (- bv_to_int w)" lemma bv_uminus_type [simp]: "bv_uminus (norm_signed w) = bv_uminus w" by (simp add: bv_uminus_def) lemma bv_uminus_returntype [simp]: "norm_signed (bv_uminus w) = bv_uminus w" by (simp add: bv_uminus_def) lemma bv_uminus_length: "length (bv_uminus w) ≤ Suc (length w)" proof - 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" by arith thus ?thesis proof safe assume p: "1 < - bv_to_int w" have lw: "0 < length w" apply (rule neg_length_pos) using p apply simp done show ?thesis proof (simp add: bv_uminus_def,rule length_int_to_bv_upper_limit_gt0,simp_all) from p show "bv_to_int w < 0" by simp next have "-(2^(length w - 1)) ≤ bv_to_int w" by (rule bv_to_int_lower_range) hence "- bv_to_int w ≤ 2^(length w - 1)" by simp also from lw have "... < 2 ^ length w" by simp finally show "- bv_to_int w < 2 ^ length w" by simp qed next assume p: "- bv_to_int w = 1" hence lw: "0 < length w" by (cases w) simp_all from p show ?thesis apply (simp add: bv_uminus_def) using lw apply (simp (no_asm) add: nat_to_bv_non0) done next assume "- bv_to_int w = 0" thus ?thesis by (simp add: bv_uminus_def) next assume p: "- bv_to_int w = -1" thus ?thesis by (simp add: bv_uminus_def) next assume p: "- bv_to_int w < -1" show ?thesis apply (simp add: bv_uminus_def) apply (rule length_int_to_bv_upper_limit_lem1) apply (rule p) apply simp proof - have "bv_to_int w < 2 ^ (length w - 1)" by (rule bv_to_int_upper_range) also have "... ≤ 2 ^ length w" by simp finally show "bv_to_int w ≤ 2 ^ length w" by simp qed qed qed lemma bv_uminus_length_utos: "length (bv_uminus (utos w)) ≤ Suc (length w)" proof - have "-bv_to_int (utos w) = 0 ∨ -bv_to_int (utos w) = -1 ∨ -bv_to_int (utos w) < -1" by (simp add: bv_to_int_utos, arith) thus ?thesis proof safe assume "-bv_to_int (utos w) = 0" thus ?thesis by (simp add: bv_uminus_def) next assume "-bv_to_int (utos w) = -1" thus ?thesis by (simp add: bv_uminus_def) next assume p: "-bv_to_int (utos w) < -1" show ?thesis apply (simp add: bv_uminus_def) apply (rule length_int_to_bv_upper_limit_lem1) apply (rule p) apply (simp add: bv_to_int_utos) using bv_to_nat_upper_range [of w] int_nat_two_exp apply presburger done qed qed definition bv_sadd :: "[bit list, bit list ] => bit list" where "bv_sadd w1 w2 = int_to_bv (bv_to_int w1 + bv_to_int w2)" lemma bv_sadd_type1 [simp]: "bv_sadd (norm_signed w1) w2 = bv_sadd w1 w2" by (simp add: bv_sadd_def) lemma bv_sadd_type2 [simp]: "bv_sadd w1 (norm_signed w2) = bv_sadd w1 w2" by (simp add: bv_sadd_def) lemma bv_sadd_returntype [simp]: "norm_signed (bv_sadd w1 w2) = bv_sadd w1 w2" by (simp add: bv_sadd_def) lemma adder_helper: assumes lw: "0 < max (length w1) (length w2)" shows "((2::int) ^ (length w1 - 1)) + (2 ^ (length w2 - 1)) ≤ 2 ^ max (length w1) (length w2)" proof - have "((2::int) ^ (length w1 - 1)) + (2 ^ (length w2 - 1)) ≤ 2 ^ (max (length w1) (length w2) - 1) + 2 ^ (max (length w1) (length w2) - 1)" by (auto simp:max_def) also have "... = 2 ^ max (length w1) (length w2)" proof - from lw show ?thesis apply simp apply (subst power_Suc [symmetric]) apply simp done qed finally show ?thesis . qed lemma bv_sadd_length: "length (bv_sadd w1 w2) ≤ Suc (max (length w1) (length w2))" proof - let ?Q = "bv_to_int w1 + bv_to_int w2" have helper: "?Q ≠ 0 ==> 0 < max (length w1) (length w2)" proof - assume p: "?Q ≠ 0" show "0 < max (length w1) (length w2)" proof (simp add: less_max_iff_disj,rule) assume [simp]: "w1 = []" show "w2 ≠ []" proof (rule ccontr,simp) assume [simp]: "w2 = []" from p show False by simp qed qed qed have "0 < ?Q ∨ ?Q = 0 ∨ ?Q = -1 ∨ ?Q < -1" by arith thus ?thesis proof safe assume "?Q = 0" thus ?thesis by (simp add: bv_sadd_def) next assume "?Q = -1" thus ?thesis by (simp add: bv_sadd_def) next assume p: "0 < ?Q" show ?thesis apply (simp add: bv_sadd_def) apply (rule length_int_to_bv_upper_limit_gt0) apply (rule p) proof simp from bv_to_int_upper_range [of w2] have "bv_to_int w2 ≤ 2 ^ (length w2 - 1)" by simp with bv_to_int_upper_range [of w1] have "bv_to_int w1 + bv_to_int w2 < (2 ^ (length w1 - 1)) + (2 ^ (length w2 - 1))" by (rule add_less_le_mono) also have "... ≤ 2 ^ max (length w1) (length w2)" apply (rule adder_helper) apply (rule helper) using p apply simp done finally show "?Q < 2 ^ max (length w1) (length w2)" . qed next assume p: "?Q < -1" show ?thesis apply (simp add: bv_sadd_def) apply (rule length_int_to_bv_upper_limit_lem1,simp_all) apply (rule p) proof - have "(2 ^ (length w1 - 1)) + 2 ^ (length w2 - 1) ≤ (2::int) ^ max (length w1) (length w2)" apply (rule adder_helper) apply (rule helper) using p apply simp done hence "-((2::int) ^ max (length w1) (length w2)) ≤ - (2 ^ (length w1 - 1)) + -(2 ^ (length w2 - 1))" by simp also have "- (2 ^ (length w1 - 1)) + -(2 ^ (length w2 - 1)) ≤ ?Q" apply (rule add_mono) apply (rule bv_to_int_lower_range [of w1]) apply (rule bv_to_int_lower_range [of w2]) done finally show "- (2^max (length w1) (length w2)) ≤ ?Q" . qed qed qed definition bv_sub :: "[bit list, bit list] => bit list" where "bv_sub w1 w2 = bv_sadd w1 (bv_uminus w2)" lemma bv_sub_type1 [simp]: "bv_sub (norm_signed w1) w2 = bv_sub w1 w2" by (simp add: bv_sub_def) lemma bv_sub_type2 [simp]: "bv_sub w1 (norm_signed w2) = bv_sub w1 w2" by (simp add: bv_sub_def) lemma bv_sub_returntype [simp]: "norm_signed (bv_sub w1 w2) = bv_sub w1 w2" by (simp add: bv_sub_def) lemma bv_sub_length: "length (bv_sub w1 w2) ≤ Suc (max (length w1) (length w2))" proof (cases "bv_to_int w2 = 0") assume p: "bv_to_int w2 = 0" show ?thesis proof (simp add: bv_sub_def bv_sadd_def bv_uminus_def p) have "length (norm_signed w1) ≤ length w1" by (rule norm_signed_length) also have "... ≤ max (length w1) (length w2)" by (rule max.cobounded1) also have "... ≤ Suc (max (length w1) (length w2))" by arith finally show "length (norm_signed w1) ≤ Suc (max (length w1) (length w2))" . qed next assume "bv_to_int w2 ≠ 0" hence "0 < length w2" by (cases w2,simp_all) hence lmw: "0 < max (length w1) (length w2)" by arith let ?Q = "bv_to_int w1 - bv_to_int w2" have "0 < ?Q ∨ ?Q = 0 ∨ ?Q = -1 ∨ ?Q < -1" by arith thus ?thesis proof safe assume "?Q = 0" thus ?thesis by (simp add: bv_sub_def bv_sadd_def bv_uminus_def) next assume "?Q = -1" thus ?thesis by (simp add: bv_sub_def bv_sadd_def bv_uminus_def) next assume p: "0 < ?Q" show ?thesis apply (simp add: bv_sub_def bv_sadd_def bv_uminus_def) apply (rule length_int_to_bv_upper_limit_gt0) apply (rule p) proof simp from bv_to_int_lower_range [of w2] have v2: "- bv_to_int w2 ≤ 2 ^ (length w2 - 1)" by simp have "bv_to_int w1 + - bv_to_int w2 < (2 ^ (length w1 - 1)) + (2 ^ (length w2 - 1))" apply (rule add_less_le_mono) apply (rule bv_to_int_upper_range [of w1]) apply (rule v2) done also have "... ≤ 2 ^ max (length w1) (length w2)" apply (rule adder_helper) apply (rule lmw) done finally show "?Q < 2 ^ max (length w1) (length w2)" by simp qed next assume p: "?Q < -1" show ?thesis apply (simp add: bv_sub_def bv_sadd_def bv_uminus_def) apply (rule length_int_to_bv_upper_limit_lem1) apply (rule p) proof simp have "(2 ^ (length w1 - 1)) + 2 ^ (length w2 - 1) ≤ (2::int) ^ max (length w1) (length w2)" apply (