# HG changeset patch # User wenzelm # Date 1181752216 -7200 # Node ID 45cd7db985b38ca2d698436b901f0b0172a0f214 # Parent a2f492c599e09f8224b50a65711f4346b00d8ff7 tuned proofs: avoid implicit prems; major cleanup of proofs/document; diff -r a2f492c599e0 -r 45cd7db985b3 src/HOL/Library/Word.thy --- a/src/HOL/Library/Word.thy Wed Jun 13 18:30:15 2007 +0200 +++ b/src/HOL/Library/Word.thy Wed Jun 13 18:30:16 2007 +0200 @@ -20,31 +20,28 @@ shows "max (f x) (f y) \ f (max x y)" proof - from mf and le_maxI1 [of x y] - have fx: "f x \ f (max x y)" - by (rule monoD) + have fx: "f x \ f (max x y)" by (rule monoD) from mf and le_maxI2 [of y x] - have fy: "f y \ f (max x y)" - by (rule monoD) + 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 + show "max (f x) (f y) \ f (max x y)" by auto qed declare zero_le_power [intro] - and zero_less_power [intro] + and zero_less_power [intro] lemma int_nat_two_exp: "2 ^ k = int (2 ^ k)" by (simp add: zpower_int [symmetric]) + subsection {* Bits *} -datatype bit - = Zero ("\") +datatype bit = + Zero ("\") | One ("\") consts bitval :: "bit => nat" - primrec "bitval \ = 0" "bitval \ = 1" @@ -84,16 +81,17 @@ bitxor_one: "(\ bitxor y) = (bitnot y)" lemma bitnot_bitnot [simp]: "(bitnot (bitnot b)) = b" - by (cases b,simp_all) + by (cases b) simp_all lemma bitand_cancel [simp]: "(b bitand b) = b" - by (cases b,simp_all) + by (cases b) simp_all lemma bitor_cancel [simp]: "(b bitor b) = b" - by (cases b,simp_all) + by (cases b) simp_all lemma bitxor_cancel [simp]: "(b bitxor b) = \" - by (cases b,simp_all) + by (cases b) simp_all + subsection {* Bit Vectors *} @@ -107,24 +105,19 @@ shows "P w" proof (cases w) assume "w = []" - thus ?thesis - by (rule empty) + 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) + hence "w = \ # bs" by simp + thus ?thesis by (rule zero) next assume "b = \" - hence "w = \ # bs" - by simp - thus ?thesis - by (rule one) + hence "w = \ # bs" by simp + thus ?thesis by (rule one) qed qed @@ -133,11 +126,11 @@ and zero: "!!bs. P bs ==> P (\#bs)" and one: "!!bs. P bs ==> P (\#bs)" shows "P w" -proof (induct w,simp_all add: empty) +proof (induct w, simp_all add: empty) fix b bs - assume [intro!]: "P bs" - show "P (b#bs)" - by (cases b,auto intro!: zero one) + assume "P bs" + then show "P (b#bs)" + by (cases b) (auto intro!: zero one) qed definition @@ -162,7 +155,7 @@ 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) + by (rule bit_list_induct [of _ w]) simp_all lemma bv_msb_Nil [simp]: "bv_msb [] = \" by (simp add: bv_msb_def) @@ -171,13 +164,13 @@ 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) + by (cases w) simp_all lemma bv_msb_one_length [simp,intro]: "bv_msb w = \ ==> 0 < length w" - by (cases w,simp_all) + by (cases w) simp_all lemma length_bv_not [simp]: "length (bv_not w) = length w" - by (induct w,simp_all) + by (induct w) simp_all definition bv_to_nat :: "bit list => nat" where @@ -191,7 +184,8 @@ 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 + case Nil + show ?case by simp next case (Cons x xs base) show ?case @@ -212,26 +206,19 @@ by simp lemma bv_to_nat_upper_range: "bv_to_nat w < 2 ^ length w" -proof (induct w,simp_all) +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" - . - also have "... < 2 * 2 ^ length bs" - by auto - finally show "bv_to_nat bs < 2 * 2 ^ length bs" - by simp + 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" - . - 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 + 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 @@ -250,20 +237,18 @@ 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) + by (subst s) rule also have "... = (replicate (n - Suc (length w)) b @ replicate 1 b) @ w" - by (subst replicate_add,rule) + 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)" - . + finally show "bv_extend n b w = bv_extend n b (b#w)" . qed consts rem_initial :: "bit => bit list => bit list" - primrec "rem_initial b [] = []" "rem_initial b (x#xs) = (if b = x then rem_initial b xs else x#xs)" @@ -276,7 +261,7 @@ 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) + 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)" @@ -284,50 +269,42 @@ show "rem_initial b xs = b#xs" by auto qed - thus ?thesis - .. + 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) +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))" + 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)" + 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" + 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 "... = + (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" - . + 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" -proof - - have "rem_initial b xs ~= [] --> rem_initial b (xs @ ys) = rem_initial b xs @ ys" (is "?P xs ys") - by (induct xs,auto) - thus ?thesis - .. -qed + 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" -proof - - have "rem_initial b xs = [] --> rem_initial b (xs @ ys) = rem_initial b ys" (is "?P xs ys") - by (induct xs,auto) - thus ?thesis - .. -qed + using assms by (induct xs) auto definition norm_unsigned :: "bit list => bit list" where @@ -347,7 +324,6 @@ consts nat_to_bv_helper :: "nat => bit list => bit list" - recdef nat_to_bv_helper "measure (\n. n)" "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)))" @@ -367,17 +343,12 @@ shows "R" proof (cases "n = 0") assume "n = 0" - thus R - by (rule zero) + thus R by (rule zero) next assume "n ~= 0" - hence nn0: "0 < n" - by simp - hence "n div 2 < n" - by arith - from this and nn0 - show R - by (rule div) + 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: @@ -387,7 +358,7 @@ 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) + by (rule ind) (simp add: int_ge_less_than_def) qed lemma unfold_nat_to_bv_helper: @@ -438,8 +409,7 @@ qed qed qed - thus ?thesis - .. + thus ?thesis .. qed lemma nat_to_bv_non0 [simp]: "0 < n ==> nat_to_bv n = nat_to_bv (n div 2) @ [if n mod 2 = 0 then \ else \]" @@ -478,8 +448,7 @@ qed qed qed - thus ?thesis - .. + thus ?thesis .. qed lemma bv_nat_bv [simp]: "bv_to_nat (nat_to_bv n) = n" @@ -488,17 +457,14 @@ 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 [simp]: "n = 0" - show ?thesis - by simp + 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 + 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]) @@ -523,13 +489,13 @@ qed lemma bv_to_nat_type [simp]: "bv_to_nat (norm_unsigned w) = bv_to_nat w" - by (rule bit_list_induct,simp_all) + 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) + 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) + 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]) @@ -540,10 +506,8 @@ 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 + 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 @@ -551,26 +515,22 @@ 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) - also have "... = 0" - by simp + 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" + 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 + thus ?thesis by simp qed lemmas [simp del] = nat_to_bv_non0 @@ -584,25 +544,21 @@ 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" +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" +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 [rule_format]: - "bv_to_nat w = 0 \ norm_unsigned w = []" - by (rule bit_list_induct [of _ w],simp_all) +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: - assumes "bv_to_nat w \ 0" - shows "norm_unsigned w \ []" -proof - - have "bv_to_nat w \ 0 --> norm_unsigned w \ []" - by (rule bit_list_induct [of _ w],simp_all) - thus ?thesis - .. -qed + "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" @@ -622,22 +578,21 @@ also have "... = 1" by (subst mod_add1_eq) simp finally have eq1: "?lhs = 1" . - have "?rhs = 0" - by simp + have "?rhs = 0" by simp with orig and eq1 show "nat_to_bv (Suc (2 * bv_to_nat w) div 2) @ [\] = norm_unsigned (w @ [\])" by simp next - have "nat_to_bv (Suc (2 * bv_to_nat w) div 2) @ [\] = nat_to_bv ((1 + 2 * bv_to_nat w) div 2) @ [\]" + 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) + by (subst div_add1_eq) simp also have "... = norm_unsigned w @ [\]" - by (subst ass,rule refl) + by (subst ass) (rule refl) also have "... = norm_unsigned (w @ [\])" - by (cases "norm_unsigned w",simp_all) - finally show "nat_to_bv (Suc (2 * bv_to_nat w) div 2) @ [\] = norm_unsigned (w @ [\])" - . + by (cases "norm_unsigned w") simp_all + finally show "nat_to_bv (Suc (2 * bv_to_nat w) div 2) @ [\] = norm_unsigned (w @ [\])" . qed next assume [simp]: "x = \" @@ -671,9 +626,8 @@ assume ind: "\ys. length ys < length xs --> ?P ys" show "?P xs" proof (cases xs) - assume [simp]: "xs = []" - show ?thesis - by (simp add: nat_to_bv_non0) + assume "xs = []" + then show ?thesis by (simp add: nat_to_bv_non0) next fix y ys assume [simp]: "xs = y # ys" @@ -703,24 +657,22 @@ 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]" - . + 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 + 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 = 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" @@ -750,9 +702,8 @@ "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 + by (subst nat_bv_nat) simp + also have "... = nat_to_bv n" by simp finally show ?thesis . qed @@ -769,25 +720,16 @@ 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 + 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 + 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 + with n0 have "2 ^ k - 1 < n" by arith + with nk show False by simp qed qed @@ -796,20 +738,16 @@ 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 + 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 + also from lnk have "... \ 2 ^ k" by simp finally have "n < 2 ^ k" . - with nk - show False - by simp + with nk show False by simp qed + subsection {* Unsigned Arithmetic Operations *} definition @@ -830,17 +768,15 @@ 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)" + 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!: le_maxI1 le_maxI2) - also have "... = 2 * max (2 ^ length w1 - 1) (2 ^ length w2 - 1)" - by simp + 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 + 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 @@ -850,12 +786,9 @@ 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 + 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) @@ -899,10 +832,12 @@ consts norm_signed :: "bit list => bit list" - primrec 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)" + 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 @@ -933,27 +868,30 @@ 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))))" +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) +proof (rule bit_list_induct [of _ w], simp_all) fix xs - assume "norm_signed (norm_signed xs) = norm_signed 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 [symmetric,simp]: "xs = \#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 "norm_signed (norm_signed xs) = norm_signed 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 [symmetric,simp]: "xs = \#ys" + assume "xs = \#ys" + from this [symmetric] and eq show "norm_signed (norm_signed (\#ys)) = norm_signed (\#ys)" by simp qed @@ -975,11 +913,11 @@ 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) +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) + proof (rule bit_list_cases [of xs], simp_all) fix ys assume [simp]: "xs = \#ys" from ind @@ -990,7 +928,7 @@ 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 (bv_not xs)) + -1" - proof (rule bit_list_cases [of xs],simp_all) + proof (rule bit_list_cases [of xs], simp_all) fix ys assume [simp]: "xs = \#ys" from ind @@ -1007,23 +945,17 @@ by (simp add: int_nat_two_exp) next fix bs - have "- int (bv_to_nat (bv_not bs)) + -1 \ 0" - by simp - also have "... < 2 ^ length bs" - by (induct bs,simp_all) - finally show "- int (bv_to_nat (bv_not bs)) + -1 < 2 ^ length bs" - . + have "- int (bv_to_nat (bv_not bs)) + -1 \ 0" by simp + also have "... < 2 ^ length bs" by (induct bs) simp_all + finally show "- int (bv_to_nat (bv_not bs)) + -1 < 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)" - . + 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"] @@ -1063,20 +995,20 @@ qed lemma bv_int_bv [simp]: "bv_to_int (int_to_bv i) = i" - by (cases "0 \ i",simp_all) + 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) + 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 (cases w, simp_all) apply (subst norm_signed_Cons) - apply (case_tac "a",simp_all) + 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) +proof (rule bit_list_cases [of w], simp_all) fix xs assume "length (norm_signed (\#xs)) = Suc (length xs)" thus "norm_signed (\#xs) = \#xs" @@ -1135,18 +1067,13 @@ 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 + 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 + 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)" @@ -1172,25 +1099,20 @@ 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 "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 + 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) + 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'" @@ -1201,8 +1123,7 @@ hence "norm_unsigned w' = []" by (simp add: bv_to_nat_zero_imp_empty) with w'0 - show False - by simp + show False by simp qed with bv_to_nat_lower_limit [of w'] show "2 ^ (length (norm_unsigned w') - Suc 0) \ int (bv_to_nat w')" @@ -1211,15 +1132,10 @@ next fix w' assume "w = \ # w'" - from w0 - have "bv_msb w = \" - by simp - with prems - show ?thesis - by simp + from w0 have "bv_msb w = \" by simp + with prems show ?thesis by simp qed - also have "... = bv_to_int w" - by simp + also have "... = bv_to_int w" by simp finally show ?thesis . qed @@ -1235,19 +1151,14 @@ 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 + 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 + with p show False by simp qed lemma bv_to_int_upper_limit_lem1: @@ -1255,61 +1166,41 @@ shows "bv_to_int w < - (2 ^ (length (norm_signed w) - 2))" proof - from w0 - have "bv_to_int w < 0" - by simp + 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 + 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) + proof safe assume "norm_signed w = []" - hence "bv_to_int (norm_signed w) = 0" - by simp - with w0 - show ?thesis - by simp + 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 + 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 + 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 + 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 + 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 + 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''" @@ -1323,9 +1214,7 @@ next fix w'' assume w'eq: "w' = \ # w''" - with weq and msb_tl - show ?thesis - by simp + with weq and msb_tl show ?thesis by simp qed qed qed @@ -1341,28 +1230,20 @@ 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 "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 + from w0 show "0 < bv_to_int (int_to_bv i)" by simp qed - thus ?thesis - by simp + thus ?thesis by simp qed finally have "2 ^ (k - 1) \ i" . - with wk - show False - by simp + with wk show False by simp qed lemma pos_length_pos: @@ -1373,26 +1254,21 @@ 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 + 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) + 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 - . + finally show ?thesis . qed lemma neg_length_pos: @@ -1404,25 +1280,19 @@ 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 + 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) + 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 - . + finally show ?thesis . qed lemma length_int_to_bv_lower_limit_gt0: @@ -1430,18 +1300,15 @@ 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" - . + 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 + hence "length (int_to_bv i) \ k" by simp with lii0 have a: "length (int_to_bv i) - 1 \ k - 1" by arith @@ -1454,11 +1321,9 @@ finally show ?thesis . qed also have "(2::int) ^ (length (int_to_bv i) - 1) \ 2 ^ (k - 1)" using a - by simp + by simp finally have "i < 2 ^ (k - 1)" . - with wk - show False - by simp + with wk show False by simp qed lemma length_int_to_bv_upper_limit_lem1: @@ -1467,15 +1332,11 @@ shows "length (int_to_bv i) \ k" proof (rule ccontr) from w1 wk - have k1: "1 < k" - by (cases "k - 1",simp_all) + 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 "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)" @@ -1486,46 +1347,36 @@ 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 + 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 + 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 + 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 + 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) + 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 + 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 + 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)" @@ -1535,11 +1386,10 @@ finally show ?thesis . qed finally have "-(2 ^ (k - 1)) \ i" . - with wk - show False - by simp + with wk show False by simp qed + subsection {* Signed Arithmetic Operations *} subsubsection {* Conversion from unsigned to signed *} @@ -1558,14 +1408,13 @@ 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) +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 + hence "bv_to_nat (norm_unsigned w) = 0" by simp + thus "bv_to_nat w = 0" by simp qed + subsubsection {* Unary minus *} definition @@ -1592,23 +1441,17 @@ done show ?thesis proof (simp add: bv_uminus_def,rule length_int_to_bv_upper_limit_gt0,simp_all) - from prems - show "bv_to_int w < 0" - by simp + from prems 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 + 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) + hence lw: "0 < length w" by (cases w) simp_all from p show ?thesis apply (simp add: bv_uminus_def) @@ -1617,12 +1460,10 @@ done next assume "- bv_to_int w = 0" - thus ?thesis - by (simp add: bv_uminus_def) + thus ?thesis by (simp add: bv_uminus_def) next assume p: "- bv_to_int w = -1" - thus ?thesis - by (simp add: bv_uminus_def) + thus ?thesis by (simp add: bv_uminus_def) next assume p: "- bv_to_int w < -1" show ?thesis @@ -1634,8 +1475,7 @@ 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 + finally show "bv_to_int w \ 2 ^ length w" by simp qed qed qed @@ -1643,17 +1483,14 @@ 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" - apply (simp add: bv_to_int_utos) - by arith + 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) + thus ?thesis by (simp add: bv_uminus_def) next assume "-bv_to_int (utos w) = -1" - thus ?thesis - by (simp add: bv_uminus_def) + thus ?thesis by (simp add: bv_uminus_def) next assume p: "-bv_to_int (utos w) < -1" show ?thesis @@ -1684,7 +1521,8 @@ 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)" + have "((2::int) ^ (length w1 - 1)) + (2 ^ (length w2 - 1)) \ + 2 ^ (max (length w1) (length w2) - 1) + 2 ^ (max (length w1) (length w2) - 1)" apply (cases "length w1 \ length w2") apply (auto simp add: max_def) done @@ -1713,15 +1551,12 @@ show "w2 \ []" proof (rule ccontr,simp) assume [simp]: "w2 = []" - from p - show False - by simp + from p show False by simp qed qed qed - have "0 < ?Q \ ?Q = 0 \ ?Q = -1 \ ?Q < -1" - by arith + have "0 < ?Q \ ?Q = 0 \ ?Q = -1 \ ?Q < -1" by arith thus ?thesis proof safe assume "?Q = 0" @@ -1750,8 +1585,7 @@ using p apply simp done - finally show "?Q < 2 ^ max (length w1) (length w2)" - . + finally show "?Q < 2 ^ max (length w1) (length w2)" . qed next assume p: "?Q < -1" @@ -1802,20 +1636,16 @@ by (rule le_maxI1) also have "... \ Suc (max (length w1) (length w2))" by arith - finally show "length (norm_signed w1) \ Suc (max (length w1) (length w2))" - . + 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 + 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 + have "0 < ?Q \ ?Q = 0 \ ?Q = -1 \ ?Q < -1" by arith thus ?thesis proof safe assume "?Q = 0" @@ -1833,8 +1663,7 @@ 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 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 zadd_zless_mono) apply (rule bv_to_int_upper_range [of w1]) @@ -1844,8 +1673,7 @@ apply (rule adder_helper) apply (rule lmw) done - finally show "?Q < 2 ^ max (length w1) (length w2)" - by simp + finally show "?Q < 2 ^ max (length w1) (length w2)" by simp qed next assume p: "?Q < -1" @@ -1866,8 +1694,7 @@ using bv_to_int_upper_range [of w2] apply simp done - finally show "- (2^max (length w1) (length w2)) \ ?Q" - by simp + finally show "- (2^max (length w1) (length w2)) \ ?Q" by simp qed qed qed @@ -1889,20 +1716,16 @@ proof - let ?Q = "bv_to_int w1 * bv_to_int w2" - have lmw: "?Q \ 0 ==> 0 < length w1 \ 0 < length w2" - by auto + have lmw: "?Q \ 0 ==> 0 < length w1 \ 0 < length w2" by auto - have "0 < ?Q \ ?Q = 0 \ ?Q = -1 \ ?Q < -1" - by arith + have "0 < ?Q \ ?Q = 0 \ ?Q = -1 \ ?Q < -1" by arith thus ?thesis proof (safe dest!: iffD1 [OF mult_eq_0_iff]) assume "bv_to_int w1 = 0" - thus ?thesis - by (simp add: bv_smult_def) + thus ?thesis by (simp add: bv_smult_def) next assume "bv_to_int w2 = 0" - thus ?thesis - by (simp add: bv_smult_def) + thus ?thesis by (simp add: bv_smult_def) next assume p: "?Q = -1" show ?thesis @@ -1937,8 +1760,7 @@ apply (subst zpower_zadd_distrib [symmetric]) apply simp done - finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)" - . + finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)" . qed next assume bi1: "bv_to_int w1 < 0" @@ -2028,33 +1850,28 @@ by simp qed qed - finally show "-(2 ^ (length w1 + length w2 - Suc 0)) \ ?Q" - . + finally show "-(2 ^ (length w1 + length w2 - Suc 0)) \ ?Q" . qed qed qed lemma bv_msb_one: "bv_msb w = \ ==> 0 < bv_to_nat w" - by (cases w,simp_all) + by (cases w) simp_all lemma bv_smult_length_utos: "length (bv_smult (utos w1) w2) \ length w1 + length w2" proof - let ?Q = "bv_to_int (utos w1) * bv_to_int w2" - have lmw: "?Q \ 0 ==> 0 < length (utos w1) \ 0 < length w2" - by auto + have lmw: "?Q \ 0 ==> 0 < length (utos w1) \ 0 < length w2" by auto - have "0 < ?Q \ ?Q = 0 \ ?Q = -1 \ ?Q < -1" - by arith + have "0 < ?Q \ ?Q = 0 \ ?Q = -1 \ ?Q < -1" by arith thus ?thesis proof (safe dest!: iffD1 [OF mult_eq_0_iff]) assume "bv_to_int (utos w1) = 0" - thus ?thesis - by (simp add: bv_smult_def) + thus ?thesis by (simp add: bv_smult_def) next assume "bv_to_int w2 = 0" - thus ?thesis - by (simp add: bv_smult_def) + thus ?thesis by (simp add: bv_smult_def) next assume p: "0 < ?Q" thus ?thesis @@ -2083,13 +1900,11 @@ using p apply auto done - finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)" - . + finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)" . qed next assume "bv_to_int (utos w1) < 0" - thus ?thesis - by (simp add: bv_to_int_utos) + thus ?thesis by (simp add: bv_to_int_utos) qed next assume p: "?Q = -1" @@ -2147,8 +1962,7 @@ by (simp add: bv_to_int_utos) qed qed - finally show "-(2 ^ (length w1 + length w2 - Suc 0)) \ ?Q" - . + finally show "-(2 ^ (length w1 + length w2 - Suc 0)) \ ?Q" . qed qed qed @@ -2183,9 +1997,7 @@ show "xs ! (length xs - Suc n) = rev xs ! n" proof (cases xs) assume "xs = []" - with notx - show ?thesis - by simp + with notx show ?thesis by simp next fix y ys assume [simp]: "xs = y # ys" @@ -2195,33 +2007,23 @@ from spec [OF ind,of ys] have "\n. n < length ys --> ys ! (length ys - Suc n) = rev ys ! n" by simp - hence "n < length ys --> ys ! (length ys - Suc n) = rev ys ! n" - .. - hence "ys ! (length ys - Suc n) = rev ys ! n" - .. + hence "n < length ys --> ys ! (length ys - Suc n) = rev ys ! n" .. + from this and noty + have "ys ! (length ys - Suc n) = rev ys ! n" .. thus "(y # ys) ! (length ys - n) = rev ys ! n" by (simp add: nth_Cons' noty linorder_not_less [symmetric]) next assume "~ n < length ys" - hence x: "length ys \ n" - by simp - from notx - have "n < Suc (length ys)" - by simp - hence "n \ length ys" - by simp - with x - have "length ys = n" - by simp - thus "y = [y] ! (n - length ys)" - by simp + hence x: "length ys \ n" by simp + from notx have "n < Suc (length ys)" by simp + hence "n \ length ys" by simp + with x have "length ys = n" by simp + thus "y = [y] ! (n - length ys)" by simp qed qed qed - hence "n < length w --> bv_select w n = rev w ! n" - .. - thus ?thesis - .. + then have "n < length w --> bv_select w n = rev w ! n" .. + from this and notnull show ?thesis .. qed lemma bv_chop_append: "bv_chop (w1 @ w2) (length w2) = (w1,w2)" @@ -2252,12 +2054,10 @@ apply (rule ccontr) proof - assume "~ n < 2 ^ length (nat_to_bv n)" - hence "2 ^ length (nat_to_bv n) \ n" - by simp + hence "2 ^ length (nat_to_bv n) \ n" by simp hence "length (nat_to_bv n) < length (nat_to_bv n)" by (rule length_nat_to_bv_lower_limit) - thus False - by simp + thus False by simp qed lemma length_nat_0 [simp]: "length_nat 0 = 0" @@ -2281,8 +2081,8 @@ lemma length_int: "length (int_to_bv i) = length_int i" proof (cases "0 < i") assume i0: "0 < i" - hence "length (int_to_bv i) = length (norm_signed (\ # norm_unsigned (nat_to_bv (nat i))))" - by simp + hence "length (int_to_bv i) = + length (norm_signed (\ # norm_unsigned (nat_to_bv (nat i))))" by simp also from norm_unsigned_result [of "nat_to_bv (nat i)"] have "... = Suc (length_nat (nat i))" apply safe @@ -2303,19 +2103,16 @@ by (simp add: length_int_def) next assume "~ 0 < i" - hence i0: "i \ 0" - by simp + hence i0: "i \ 0" by simp show ?thesis proof (cases "i = 0") assume "i = 0" - thus ?thesis - by (simp add: length_int_def) + thus ?thesis by (simp add: length_int_def) next assume "i \ 0" - with i0 - have i0: "i < 0" - by simp - hence "length (int_to_bv i) = length (norm_signed (\ # bv_not (norm_unsigned (nat_to_bv (nat (- i) - 1)))))" + with i0 have i0: "i < 0" by simp + hence "length (int_to_bv i) = + length (norm_signed (\ # bv_not (norm_unsigned (nat_to_bv (nat (- i) - 1)))))" by (simp add: int_to_bv_def nat_diff_distrib) also from norm_unsigned_result [of "nat_to_bv (nat (- i) - 1)"] have "... = Suc (length_nat (nat (- i) - 1))" @@ -2333,8 +2130,7 @@ done finally show ?thesis - using i0 - by (simp add: length_int_def nat_diff_distrib del: int_to_bv_lt0) + using i0 by (simp add: length_int_def nat_diff_distrib del: int_to_bv_lt0) qed qed @@ -2413,14 +2209,11 @@ shows "bv_to_int (bv_extend n b w) = bv_to_int w" proof (cases "bv_msb w") assume [simp]: "bv_msb w = \" - with a have [simp]: "b = \" - by simp - show ?thesis - by (simp add: bv_to_int_def) + with a have [simp]: "b = \" by simp + show ?thesis by (simp add: bv_to_int_def) next assume [simp]: "bv_msb w = \" - with a have [simp]: "b = \" - by simp + with a have [simp]: "b = \" by simp show ?thesis apply (simp add: bv_to_int_def) apply (simp add: bv_extend_def) @@ -2447,26 +2240,21 @@ apply (cases "0 \ y") apply (induct y,simp_all) done - with xx - have "y < x" by simp - with xy - show False - by simp + with xx have "y < x" by simp + with xy show False by simp qed lemma length_nat_mono_int [simp]: "x \ y ==> length_nat x \ length_nat y" - apply (rule length_nat_mono) - apply arith - done + by (rule length_nat_mono) arith lemma length_nat_pos [simp,intro!]: "0 < x ==> 0 < length_nat x" by (simp add: length_nat_non0) lemma length_int_mono_gt0: "[| 0 \ x ; x \ y |] ==> length_int x \ length_int y" - by (cases "x = 0",simp_all add: length_int_gt0 nat_le_eq_zle) + by (cases "x = 0") (simp_all add: length_int_gt0 nat_le_eq_zle) -lemma length_int_mono_lt0: "[| x \ y ; y \ 0 |] ==> length_int y \ length_int x" apply (cases "y = 0",simp_all add: length_int_lt0) - done +lemma length_int_mono_lt0: "[| x \ y ; y \ 0 |] ==> length_int y \ length_int x" + by (cases "y = 0") (simp_all add: length_int_lt0) lemmas [simp] = length_nat_non0 @@ -2475,18 +2263,21 @@ consts fast_bv_to_nat_helper :: "[bit list, int] => int" - primrec fast_bv_to_nat_Nil: "fast_bv_to_nat_helper [] k = k" - fast_bv_to_nat_Cons: "fast_bv_to_nat_helper (b#bs) k = fast_bv_to_nat_helper bs (k BIT (bit_case bit.B0 bit.B1 b))" + fast_bv_to_nat_Cons: "fast_bv_to_nat_helper (b#bs) k = + fast_bv_to_nat_helper bs (k BIT (bit_case bit.B0 bit.B1 b))" -lemma fast_bv_to_nat_Cons0: "fast_bv_to_nat_helper (\#bs) bin = fast_bv_to_nat_helper bs (bin BIT bit.B0)" +lemma fast_bv_to_nat_Cons0: "fast_bv_to_nat_helper (\#bs) bin = + fast_bv_to_nat_helper bs (bin BIT bit.B0)" by simp -lemma fast_bv_to_nat_Cons1: "fast_bv_to_nat_helper (\#bs) bin = fast_bv_to_nat_helper bs (bin BIT bit.B1)" +lemma fast_bv_to_nat_Cons1: "fast_bv_to_nat_helper (\#bs) bin = + fast_bv_to_nat_helper bs (bin BIT bit.B1)" by simp -lemma fast_bv_to_nat_def: "bv_to_nat bs == number_of (fast_bv_to_nat_helper bs Numeral.Pls)" +lemma fast_bv_to_nat_def: + "bv_to_nat bs == number_of (fast_bv_to_nat_helper bs Numeral.Pls)" proof (simp add: bv_to_nat_def) 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)" apply (induct bs,simp) @@ -2547,7 +2338,7 @@ in map (split f) (zip (g w1) (g w2)))" lemma bv_length_bv_mapzip [simp]: - "length (bv_mapzip f w1 w2) = max (length w1) (length w2)" + "length (bv_mapzip f w1 w2) = max (length w1) (length w2)" by (simp add: bv_mapzip_def Let_def split: split_max) lemma bv_mapzip_Nil [simp]: "bv_mapzip f [] [] = []"