--- a/NEWS Tue May 18 00:01:03 2010 +0200
+++ b/NEWS Tue May 18 00:01:51 2010 +0200
@@ -143,6 +143,10 @@
*** HOL ***
+* Theory Library/Word.thy has been removed. Use library Word/Word.thy for
+future developements; former Library/Word.thy is still present in the AFP
+entry RSAPPS.
+
* Theorem Int.int_induct renamed to Int.int_of_nat_induct and is no
longer shadowed. INCOMPATIBILITY.
--- a/src/HOL/IsaMakefile Tue May 18 00:01:03 2010 +0200
+++ b/src/HOL/IsaMakefile Tue May 18 00:01:51 2010 +0200
@@ -410,7 +410,7 @@
Library/Library.thy Library/List_Prefix.thy Library/List_Set.thy \
Library/State_Monad.thy Library/Multiset.thy Library/Permutation.thy \
Library/Quotient_Type.thy Library/Quicksort.thy \
- Library/Nat_Infinity.thy Library/Word.thy Library/README.html \
+ Library/Nat_Infinity.thy Library/README.html \
Library/Continuity.thy Library/Order_Relation.thy \
Library/Nested_Environment.thy Library/Ramsey.thy Library/Zorn.thy \
Library/Library/ROOT.ML Library/Library/document/root.tex \
--- a/src/HOL/Library/Library.thy Tue May 18 00:01:03 2010 +0200
+++ b/src/HOL/Library/Library.thy Tue May 18 00:01:51 2010 +0200
@@ -61,7 +61,6 @@
Transitive_Closure_Table
Univ_Poly
While_Combinator
- Word
Zorn
begin
end
--- a/src/HOL/Library/Word.thy Tue May 18 00:01:03 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,2314 +0,0 @@
-(* Title: HOL/Library/Word.thy
- Author: Sebastian Skalberg, TU Muenchen
-*)
-
-header {* Binary Words *}
-
-theory Word
-imports Main
-begin
-
-subsection {* Auxilary Lemmas *}
-
-lemma max_le [intro!]: "[| x \<le> z; y \<le> z |] ==> max x y \<le> z"
- by (simp add: max_def)
-
-lemma max_mono:
- fixes x :: "'a::linorder"
- assumes mf: "mono f"
- shows "max (f x) (f y) \<le> f (max x y)"
-proof -
- from mf and le_maxI1 [of x y]
- have fx: "f x \<le> f (max x y)" by (rule monoD)
- from mf and le_maxI2 [of y x]
- have fy: "f y \<le> f (max x y)" by (rule monoD)
- from fx and fy
- show "max (f x) (f y) \<le> 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 add: zpower_int [symmetric])
-
-
-subsection {* Bits *}
-
-datatype bit =
- Zero ("\<zero>")
- | One ("\<one>")
-
-primrec bitval :: "bit => nat" where
- "bitval \<zero> = 0"
- | "bitval \<one> = 1"
-
-primrec bitnot :: "bit => bit" where
- bitnot_zero: "(bitnot \<zero>) = \<one>"
- | bitnot_one : "(bitnot \<one>) = \<zero>"
-
-primrec bitand :: "bit => bit => bit" (infixr "bitand" 35) where
- bitand_zero: "(\<zero> bitand y) = \<zero>"
- | bitand_one: "(\<one> bitand y) = y"
-
-primrec bitor :: "bit => bit => bit" (infixr "bitor" 30) where
- bitor_zero: "(\<zero> bitor y) = y"
- | bitor_one: "(\<one> bitor y) = \<one>"
-
-primrec bitxor :: "bit => bit => bit" (infixr "bitxor" 30) where
- bitxor_zero: "(\<zero> bitxor y) = y"
- | bitxor_one: "(\<one> bitxor y) = (bitnot y)"
-
-notation (xsymbols)
- bitnot ("\<not>\<^sub>b _" [40] 40) and
- bitand (infixr "\<and>\<^sub>b" 35) and
- bitor (infixr "\<or>\<^sub>b" 30) and
- bitxor (infixr "\<oplus>\<^sub>b" 30)
-
-notation (HTML output)
- bitnot ("\<not>\<^sub>b _" [40] 40) and
- bitand (infixr "\<and>\<^sub>b" 35) and
- bitor (infixr "\<or>\<^sub>b" 30) and
- bitxor (infixr "\<oplus>\<^sub>b" 30)
-
-lemma bitnot_bitnot [simp]: "(bitnot (bitnot b)) = b"
- by (cases b) simp_all
-
-lemma bitand_cancel [simp]: "(b bitand b) = b"
- by (cases b) simp_all
-
-lemma bitor_cancel [simp]: "(b bitor b) = b"
- by (cases b) simp_all
-
-lemma bitxor_cancel [simp]: "(b bitxor b) = \<zero>"
- 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 = \<zero> # bs ==> P w"
- and one: "!!bs. w = \<one> # 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 = \<zero>"
- hence "w = \<zero> # bs" by simp
- thus ?thesis by (rule zero)
- next
- assume "b = \<one>"
- hence "w = \<one> # bs" by simp
- thus ?thesis by (rule one)
- qed
-qed
-
-lemma bit_list_induct:
- assumes empty: "P []"
- and zero: "!!bs. P bs ==> P (\<zero>#bs)"
- and one: "!!bs. P bs ==> P (\<one>#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 \<zero> 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 \<le> 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 [] = \<zero>"
- 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 = \<one> ==> 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 (\<lambda>bn b. 2 * bn + bitval b)"
- have helper: "\<And>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.simps)
- 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 (\<zero>#bs) = bv_to_nat bs"
- by simp
-
-lemma bv_to_nat1 [simp]: "bv_to_nat (\<one>#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 \<le> 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) \<le> 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 \<zero>"
-
-lemma norm_unsigned_Nil [simp]: "norm_unsigned [] = []"
- by (simp add: norm_unsigned_def)
-
-lemma norm_unsigned_Cons0 [simp]: "norm_unsigned (\<zero>#bs) = norm_unsigned bs"
- by (simp add: norm_unsigned_def)
-
-lemma norm_unsigned_Cons1 [simp]: "norm_unsigned (\<one>#bs) = \<one>#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 \<zero> else \<one>)#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 \<le> 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: "(\<And>y\<Colon>int. (y, x) \<in> int_ge_less_than k \<Longrightarrow> 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 "\<forall>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 \<Longrightarrow> \<forall> l. nat_to_bv_helper j l = nat_to_bv_helper j [] @ l"
- show "\<forall>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 \<le> n div 2"
- by arith
- from ind [of "n div 2"] and n2n n20
- have ind': "\<forall>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 "\<zero>#l"])
- apply (subst spec [OF ind',of "\<one>#l"])
- apply (subst spec [OF ind',of "[\<one>]"])
- apply (subst spec [OF ind',of "[\<zero>]"])
- apply simp
- done
- qed
- qed
- qed
- qed
- thus ?thesis ..
-qed
-
-lemma nat_to_bv_non0 [simp]: "n\<noteq>0 ==> nat_to_bv n = nat_to_bv (n div 2) @ [if n mod 2 = 0 then \<zero> else \<one>]"
-proof -
- assume [simp]: "n\<noteq>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)
- using prems
- apply (simp)
- 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 "\<forall>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: "\<forall>l2. bv_to_nat (xs @ l2) = bv_to_nat xs * 2 ^ length l2 + bv_to_nat l2"
- show "\<forall>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 \<Longrightarrow> 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 \<noteq> 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: split_if)
- apply (cases "n mod 2 = 0")
- proof (simp_all)
- assume "n mod 2 = 0"
- with mod_div_equality [of n 2]
- show "n div 2 * 2 = n" by simp
- next
- assume "n mod 2 = Suc 0"
- with mod_div_equality [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) \<le> length w"
- by (rule bit_list_induct) simp_all
-
-lemma bv_to_nat_rew_msb: "bv_msb w = \<one> ==> 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 = [] \<or> bv_msb (norm_unsigned xs) = \<one>"
-proof (rule length_induct [of _ xs])
- fix xs :: "bit list"
- assume ind: "\<forall>ys. length ys < length xs --> norm_unsigned ys = [] \<or> bv_msb (norm_unsigned ys) = \<one>"
- show "norm_unsigned xs = [] \<or> bv_msb (norm_unsigned xs) = \<one>"
- proof (rule bit_list_cases [of xs],simp_all)
- fix bs
- assume [simp]: "xs = \<zero>#bs"
- from ind
- have "length bs < length xs --> norm_unsigned bs = [] \<or> bv_msb (norm_unsigned bs) = \<one>" ..
- thus "norm_unsigned bs = [] \<or> bv_msb (norm_unsigned bs) = \<one>" 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) \<le> bv_to_nat w"
-proof -
- from w0 and norm_unsigned_result [of w]
- have msbw: "bv_msb (norm_unsigned w) = \<one>"
- by (auto simp add: norm_empty_bv_to_nat_zero)
- have "2 ^ (length (norm_unsigned w) - 1) \<le> 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) \<le> 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) \<zero> (norm_unsigned w) = w"
-by (simp add: norm_unsigned_def,rule bv_extend_rem_initial)
-
-lemma norm_unsigned_append1 [simp]:
- "norm_unsigned xs \<noteq> [] ==> 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 \<Longrightarrow> 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 \<noteq> 0 \<Longrightarrow> norm_unsigned w \<noteq> []"
-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 = \<one>"
- have "nat_to_bv (Suc (2 * bv_to_nat w) div 2) @ [\<one>] =
- nat_to_bv ((1 + 2 * bv_to_nat w) div 2) @ [\<one>]"
- by (simp add: add_commute)
- also have "... = nat_to_bv (bv_to_nat w) @ [\<one>]"
- by (subst div_add1_eq) simp
- also have "... = norm_unsigned w @ [\<one>]"
- by (subst ass) (rule refl)
- also have "... = norm_unsigned (w @ [\<one>])"
- by (cases "norm_unsigned w") simp_all
- finally have "nat_to_bv (Suc (2 * bv_to_nat w) div 2) @ [\<one>] = norm_unsigned (w @ [\<one>])" .
- then show ?thesis by (simp add: nat_to_bv_non0)
-next
- assume [simp]: "x = \<zero>"
- 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 \<noteq> 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) = \<one> # xs"
-proof -
- have "\<forall>xs. nat_to_bv (2 ^ length (rev xs) + bv_to_nat (rev xs)) = \<one> # (rev xs)" (is "\<forall>xs. ?P xs")
- proof
- fix xs
- show "?P xs"
- proof (rule length_induct [of _ xs])
- fix xs :: "bit list"
- assume ind: "\<forall>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: add_ac mult_ac)
- also have "... = nat_to_bv (2 * (bv_to_nat (\<one>#rev ys)) + bitval y)"
- by simp
- also have "... = norm_unsigned (\<one>#rev ys) @ [y]"
- proof -
- from ind
- have "nat_to_bv (2 ^ length (rev ys) + bv_to_nat (rev ys)) = \<one> # rev ys"
- by auto
- hence [simp]: "nat_to_bv (2 ^ length ys + bv_to_nat (rev ys)) = \<one> # rev ys"
- by simp
- show ?thesis
- apply (subst nat_helper1)
- apply simp_all
- done
- qed
- also have "... = (\<one>#rev ys) @ [y]"
- by simp
- also have "... = \<one> # rev ys @ [y]"
- by simp
- finally show "nat_to_bv (2 * 2 ^ length ys + (bv_to_nat (rev ys) * 2 + bitval y)) =
- \<one> # rev ys @ [y]" .
- qed
- qed
- qed
- qed
- hence "nat_to_bv (2 ^ length (rev (rev xs)) + bv_to_nat (rev (rev xs))) =
- \<one> # 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) = \<one> # 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) \<zero> (norm_unsigned xs)"
- by (simp add: bv_extend_norm_unsigned)
- also have "... = bv_extend (length ys) \<zero> (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 \<le> 2 ^ k - 1"
- shows "length (nat_to_bv n) \<le> 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) \<le> k"
- hence "k < length (nat_to_bv n)" by simp
- hence "k \<le> length (nat_to_bv n) - 1" by arith
- hence "(2::nat) ^ k \<le> 2 ^ (length (nat_to_bv n) - 1)" by simp
- also have "... = 2 ^ (length (norm_unsigned (nat_to_bv n)) - 1)" by simp
- also have "... \<le> 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 \<le> 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 \<le> 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) \<le> 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 "... \<le> 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) \<le> 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 \<le> (2 ^ length w1 - 1) + (2 ^ length w2 - 1)"
- by arith
- also have "... \<le>
- 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 "... \<le> 2 ^ Suc (max (length w1) (length w2)) - 2"
- proof (cases "length w1 \<le> length w2")
- assume w1w2: "length w1 \<le> length w2"
- hence "(2::nat) ^ length w1 \<le> 2 ^ length w2" by simp
- hence "(2::nat) ^ length w1 - 1 \<le> 2 ^ length w2 - 1" by arith
- with w1w2 show ?thesis
- by (simp add: diff_mult_distrib2 split: split_max)
- next
- assume [simp]: "~ (length w1 \<le> length w2)"
- have "~ ((2::nat) ^ length w1 - 1 \<le> 2 ^ length w2 - 1)"
- proof
- assume "(2::nat) ^ length w1 - 1 \<le> 2 ^ length w2 - 1"
- hence "((2::nat) ^ length w1 - 1) + 1 \<le> (2 ^ length w2 - 1) + 1"
- by (rule add_right_mono)
- hence "(2::nat) ^ length w1 \<le> 2 ^ length w2" by simp
- hence "length w1 \<le> 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 \<le> 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) \<le> 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 \<le> 2 ^ length w1 - 1 \<and> bv_to_nat w2 \<le> 2 ^ length w2 - 1"
- by arith
- have "bv_to_nat w1 * bv_to_nat w2 \<le> (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 \<le> 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
- \<zero> => if norm_unsigned bs = [] then [] else b#norm_unsigned bs
- | \<one> => b#rem_initial b bs)"
-
-lemma norm_signed0 [simp]: "norm_signed [\<zero>] = []"
- by simp
-
-lemma norm_signed1 [simp]: "norm_signed [\<one>] = [\<one>]"
- by simp
-
-lemma norm_signed01 [simp]: "norm_signed (\<zero>#\<one>#xs) = \<zero>#\<one>#xs"
- by simp
-
-lemma norm_signed00 [simp]: "norm_signed (\<zero>#\<zero>#xs) = norm_signed (\<zero>#xs)"
- by simp
-
-lemma norm_signed10 [simp]: "norm_signed (\<one>#\<zero>#xs) = \<one>#\<zero>#xs"
- by simp
-
-lemma norm_signed11 [simp]: "norm_signed (\<one>#\<one>#xs) = norm_signed (\<one>#xs)"
- by simp
-
-lemmas [simp del] = norm_signed_Cons
-
-definition
- int_to_bv :: "int => bit list" where
- "int_to_bv n = (if 0 \<le> n
- then norm_signed (\<zero>#nat_to_bv (nat n))
- else norm_signed (bv_not (\<zero>#nat_to_bv (nat (-n- 1)))))"
-
-lemma int_to_bv_ge0 [simp]: "0 \<le> n ==> int_to_bv n = norm_signed (\<zero> # 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 (\<zero>#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 (\<zero>#xs)) = norm_signed (\<zero>#xs)"
- proof (rule bit_list_cases [of xs],simp_all)
- fix ys
- assume "xs = \<zero>#ys"
- from this [symmetric] and eq
- show "norm_signed (norm_signed (\<zero>#ys)) = norm_signed (\<zero>#ys)"
- by simp
- qed
-next
- fix xs
- assume eq: "norm_signed (norm_signed xs) = norm_signed xs"
- show "norm_signed (norm_signed (\<one>#xs)) = norm_signed (\<one>#xs)"
- proof (rule bit_list_cases [of xs],simp_all)
- fix ys
- assume "xs = \<one>#ys"
- from this [symmetric] and eq
- show "norm_signed (norm_signed (\<one>#ys)) = norm_signed (\<one>#ys)"
- by simp
- qed
-qed
-
-definition
- bv_to_int :: "bit list => int" where
- "bv_to_int w =
- (case bv_msb w of \<zero> => int (bv_to_nat w)
- | \<one> => - 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 (\<zero>#bs) = int (bv_to_nat bs)"
- by (simp add: bv_to_int_def)
-
-lemma bv_to_int_Cons1 [simp]: "bv_to_int (\<one>#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 (\<zero>#xs)) = int (bv_to_nat xs)"
- proof (rule bit_list_cases [of xs], simp_all)
- fix ys
- assume [simp]: "xs = \<zero>#ys"
- from ind
- show "bv_to_int (norm_signed (\<zero>#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 (\<one>#xs)) = -1 - int (bv_to_nat (bv_not xs))"
- proof (rule bit_list_cases [of xs], simp_all)
- fix ys
- assume [simp]: "xs = \<one>#ys"
- from ind
- show "bv_to_int (norm_signed (\<one>#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)
- fix bs
- from bv_to_nat_upper_range
- show "int (bv_to_nat bs) < 2 ^ length bs"
- by (simp add: int_nat_two_exp)
-next
- fix bs
- have "-1 - int (bv_to_nat (bv_not bs)) \<le> 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)) \<le> bv_to_int w"
-proof (rule bit_list_cases [of w],simp_all)
- fix bs :: "bit list"
- have "- (2 ^ length bs) \<le> (0::int)" by (induct bs) simp_all
- also have "... \<le> int (bv_to_nat bs)" by simp
- finally show "- (2 ^ length bs) \<le> int (bv_to_nat bs)" .
-next
- fix bs
- from bv_to_nat_upper_range [of "bv_not bs"]
- show "- (2 ^ length bs) \<le> -1 - int (bv_to_nat (bv_not bs))"
- by (simp add: int_nat_two_exp)
-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 = \<zero>#xs"
- show ?thesis
- apply simp
- apply (subst norm_signed_Cons [of "\<zero>" "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 = \<one>#xs"
- show ?thesis
- apply (simp del: int_to_bv_lt0)
- apply (rule bit_list_induct [of _ xs])
- apply simp
- apply (subst int_to_bv_lt0)
- apply (subgoal_tac "- int (bv_to_nat (bv_not (\<zero> # bs))) + -1 < 0 + 0")
- apply simp
- apply (rule add_le_less_mono)
- apply simp
- apply simp
- apply (simp del: bv_to_nat1 bv_to_nat_helper)
- apply simp
- done
-qed
-
-lemma bv_int_bv [simp]: "bv_to_int (int_to_bv i) = i"
- by (cases "0 \<le> 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) \<le> 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 (\<zero>#xs)) = Suc (length xs)"
- thus "norm_signed (\<zero>#xs) = \<zero>#xs"
- by (simp add: norm_signed_Cons norm_unsigned_equal [THEN eqTrueI]
- split: split_if_asm)
-next
- fix xs
- assume "length (norm_signed (\<one>#xs)) = Suc (length xs)"
- thus "norm_signed (\<one>#xs) = \<one>#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)) \<zero> (norm_signed (\<zero>#xs)) = \<zero>#xs"
- proof (simp add: norm_signed_def,auto)
- assume "norm_unsigned xs = []"
- hence xx: "rem_initial \<zero> xs = []"
- by (simp add: norm_unsigned_def)
- have "bv_extend (Suc (length xs)) \<zero> (\<zero>#rem_initial \<zero> xs) = \<zero>#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)) \<zero> [\<zero>] = \<zero>#xs"
- by (simp add: xx)
- next
- show "bv_extend (Suc (length xs)) \<zero> (\<zero>#norm_unsigned xs) = \<zero>#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)) \<one> (norm_signed (\<one>#xs)) = \<one>#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 \<le> bv_to_int w1 ==> bv_msb w1 = \<zero>"
- by (rule bit_list_cases,simp_all)
-
-lemma bv_to_int_msb1: "bv_to_int w1 < 0 ==> bv_msb w1 = \<one>"
- 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) \<le> bv_to_int w"
-proof -
- from w0
- have "0 \<le> bv_to_int w" by simp
- hence [simp]: "bv_msb w = \<zero>" by (rule bv_to_int_msb0)
- have "2 ^ (length (norm_signed w) - 2) \<le> 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 = \<zero> # 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' \<noteq> []"
- 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) \<le> int (bv_to_nat w')"
- by (simp add: int_nat_two_exp)
- qed
- next
- fix w'
- assume "w = \<one> # w'"
- from w0 have "bv_msb w = \<zero>" by simp
- with prems show ?thesis by simp
- qed
- also have "... = bv_to_int w" by simp
- finally show ?thesis .
-qed
-
-lemma norm_signed_result: "norm_signed w = [] \<or> norm_signed w = [\<one>] \<or> bv_msb (norm_signed w) \<noteq> 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: "\<zero> = bv_msb (norm_unsigned l)"
- assume "norm_unsigned l \<noteq> []"
- with norm_unsigned_result [of l]
- have "bv_msb (norm_unsigned l) = \<one>" by simp
- with msb show False by simp
-next
- fix xs
- assume p: "\<one> = bv_msb (tl (norm_signed (\<one> # xs)))"
- have "\<one> \<noteq> bv_msb (tl (norm_signed (\<one> # 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 = \<one>"
- 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 = [\<one>]"
- hence "bv_to_int (norm_signed w) = -1" by simp
- with w0 show ?thesis by simp
- next
- assume "bv_msb (norm_signed w) \<noteq> bv_msb (tl (norm_signed w))"
- hence msb_tl: "\<one> \<noteq> 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 = \<zero> # w'"
- from msbw have "bv_msb (norm_signed w) = \<one>" by simp
- with nw show ?thesis by simp
- next
- fix w'
- assume weq: "norm_signed w = \<one> # 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' = \<zero> # w''"
- show ?thesis
- apply (simp add: weq w'eq)
- apply (subgoal_tac "- int (bv_to_nat (bv_not w'')) + -1 < 0 + 0")
- apply (simp add: int_nat_two_exp)
- apply (rule add_le_less_mono)
- apply simp_all
- done
- next
- fix w''
- assume w'eq: "w' = \<one> # 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 \<le> 2 ^ (k - 1) - 1"
- shows "length (int_to_bv i) \<le> k"
-proof (rule ccontr)
- from w0 wk
- have k1: "1 < k"
- by (cases "k - 1",simp_all)
- assume "~ length (int_to_bv i) \<le> k"
- hence "k < length (int_to_bv i)" by simp
- hence "k \<le> length (int_to_bv i) - 1" by arith
- hence a: "k - 1 \<le> length (int_to_bv i) - 2" by arith
- hence "(2::int) ^ (k - 1) \<le> 2 ^ (length (int_to_bv i) - 2)" by simp
- also have "... \<le> i"
- proof -
- have "2 ^ (length (norm_signed (int_to_bv i)) - 2) \<le> 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) \<le> 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 \<noteq> \<zero>"
- have "\<zero> = bv_msb (norm_signed w)"
- by (subst ii) simp
- also have "... \<noteq> \<zero>"
- by (simp add: jj)
- finally show False by simp
- qed
- also have "... \<le> 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 \<noteq> \<zero>"
- have "\<zero> = bv_msb (norm_signed w)" by (subst ii) simp
- also have "... \<noteq> \<zero>" by (simp add: jj)
- finally show False by simp
- qed
- also have "... \<le> length w"
- by (rule norm_signed_length)
- finally show ?thesis .
-qed
-
-lemma length_int_to_bv_lower_limit_gt0:
- assumes wk: "2 ^ (k - 1) \<le> 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 "... \<le> 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) \<le> k" by simp
- with lii0
- have a: "length (int_to_bv i) - 1 \<le> 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) \<le> 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)) \<le> i"
- shows "length (int_to_bv i) \<le> k"
-proof (rule ccontr)
- from w1 wk
- have k1: "1 < k" by (cases "k - 1") simp_all
- assume "~ length (int_to_bv i) \<le> k"
- hence "k < length (int_to_bv i)" by simp
- hence "k \<le> length (int_to_bv i) - 1" by arith
- hence a: "k - 1 \<le> 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 "... \<le> -(2 ^ (k - 1))"
- proof -
- have "(2::int) ^ (k - 1) \<le> 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 \<le> -(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) \<le> k"
- by simp
- with lii0 have a: "length (int_to_bv i) - 1 \<le> k - 1" by arith
- hence "(2::int) ^ (length (int_to_bv i) - 1) \<le> 2 ^ (k - 1)" by simp
- hence "-((2::int) ^ (k - 1)) \<le> - (2 ^ (length (int_to_bv i) - 1))" by simp
- also have "... \<le> i"
- proof -
- have "- (2 ^ (length (int_to_bv i) - 1)) \<le> 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)) \<le> 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 (\<zero> # 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) \<le> 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) \<le> Suc (length w)"
-proof -
- have "1 < -bv_to_int w \<or> -bv_to_int w = 1 \<or> -bv_to_int w = 0 \<or> -bv_to_int w = -1 \<or> -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 prems show "bv_to_int w < 0" by simp
- next
- have "-(2^(length w - 1)) \<le> bv_to_int w"
- by (rule bv_to_int_lower_range)
- hence "- bv_to_int w \<le> 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 "... \<le> 2 ^ length w" by simp
- finally show "bv_to_int w \<le> 2 ^ length w" by simp
- qed
- qed
-qed
-
-lemma bv_uminus_length_utos: "length (bv_uminus (utos w)) \<le> Suc (length w)"
-proof -
- have "-bv_to_int (utos w) = 0 \<or> -bv_to_int (utos w) = -1 \<or> -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]
- apply (simp add: int_nat_two_exp)
- 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)) \<le> 2 ^ max (length w1) (length w2)"
-proof -
- have "((2::int) ^ (length w1 - 1)) + (2 ^ (length w2 - 1)) \<le>
- 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) \<le> Suc (max (length w1) (length w2))"
-proof -
- let ?Q = "bv_to_int w1 + bv_to_int w2"
-
- have helper: "?Q \<noteq> 0 ==> 0 < max (length w1) (length w2)"
- proof -
- assume p: "?Q \<noteq> 0"
- show "0 < max (length w1) (length w2)"
- proof (simp add: less_max_iff_disj,rule)
- assume [simp]: "w1 = []"
- show "w2 \<noteq> []"
- proof (rule ccontr,simp)
- assume [simp]: "w2 = []"
- from p show False by simp
- qed
- qed
- qed
-
- have "0 < ?Q \<or> ?Q = 0 \<or> ?Q = -1 \<or> ?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 \<le> 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 zadd_zless_mono)
- also have "... \<le> 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) \<le> (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)) \<le> - (2 ^ (length w1 - 1)) + -(2 ^ (length w2 - 1))"
- by simp
- also have "- (2 ^ (length w1 - 1)) + -(2 ^ (length w2 - 1)) \<le> ?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)) \<le> ?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) \<le> 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) \<le> length w1"
- by (rule norm_signed_length)
- also have "... \<le> max (length w1) (length w2)"
- by (rule le_maxI1)
- also have "... \<le> Suc (max (length w1) (length w2))"
- by arith
- finally show "length (norm_signed w1) \<le> Suc (max (length w1) (length w2))" .
- qed
-next
- assume "bv_to_int w2 \<noteq> 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 \<or> ?Q = 0 \<or> ?Q = -1 \<or> ?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 \<le> 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])
- apply (rule v2)
- done
- also have "... \<le> 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) \<le> (2::int) ^ max (length w1) (length w2)"
- apply (rule adder_helper)
- apply (rule lmw)
- done
- hence "-((2::int) ^ max (length w1) (length w2)) \<le> - (2 ^ (length w1 - 1)) + -(2 ^ (length w2 - 1))"
- by simp
- also have "- (2 ^ (length w1 - 1)) + -(2 ^ (length w2 - 1)) \<le> bv_to_int w1 + -bv_to_int w2"
- apply (rule add_mono)
- apply (rule bv_to_int_lower_range [of w1])
- using bv_to_int_upper_range [of w2]
- apply simp
- done
- finally show "- (2^max (length w1) (length w2)) \<le> ?Q" by simp
- qed
- qed
-qed
-
-definition
- bv_smult :: "[bit list, bit list] => bit list" where
- "bv_smult w1 w2 = int_to_bv (bv_to_int w1 * bv_to_int w2)"
-
-lemma bv_smult_type1 [simp]: "bv_smult (norm_signed w1) w2 = bv_smult w1 w2"
- by (simp add: bv_smult_def)
-
-lemma bv_smult_type2 [simp]: "bv_smult w1 (norm_signed w2) = bv_smult w1 w2"
- by (simp add: bv_smult_def)
-
-lemma bv_smult_returntype [simp]: "norm_signed (bv_smult w1 w2) = bv_smult w1 w2"
- by (simp add: bv_smult_def)
-
-lemma bv_smult_length: "length (bv_smult w1 w2) \<le> length w1 + length w2"
-proof -
- let ?Q = "bv_to_int w1 * bv_to_int w2"
-
- have lmw: "?Q \<noteq> 0 ==> 0 < length w1 \<and> 0 < length w2" by auto
-
- have "0 < ?Q \<or> ?Q = 0 \<or> ?Q = -1 \<or> ?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)
- next
- assume "bv_to_int w2 = 0"
- thus ?thesis by (simp add: bv_smult_def)
- next
- assume p: "?Q = -1"
- show ?thesis
- apply (simp add: bv_smult_def p)
- apply (cut_tac lmw)
- apply arith
- using p
- apply simp
- done
- next
- assume p: "0 < ?Q"
- thus ?thesis
- proof (simp add: zero_less_mult_iff,safe)
- assume bi1: "0 < bv_to_int w1"
- assume bi2: "0 < bv_to_int w2"
- show ?thesis
- apply (simp add: bv_smult_def)
- apply (rule length_int_to_bv_upper_limit_gt0)
- apply (rule p)
- proof simp
- have "?Q < 2 ^ (length w1 - 1) * 2 ^ (length w2 - 1)"
- apply (rule mult_strict_mono)
- apply (rule bv_to_int_upper_range)
- apply (rule bv_to_int_upper_range)
- apply (rule zero_less_power)
- apply simp
- using bi2
- apply simp
- done
- also have "... \<le> 2 ^ (length w1 + length w2 - Suc 0)"
- apply simp
- apply (subst zpower_zadd_distrib [symmetric])
- apply simp
- done
- finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)" .
- qed
- next
- assume bi1: "bv_to_int w1 < 0"
- assume bi2: "bv_to_int w2 < 0"
- show ?thesis
- apply (simp add: bv_smult_def)
- apply (rule length_int_to_bv_upper_limit_gt0)
- apply (rule p)
- proof simp
- have "-bv_to_int w1 * -bv_to_int w2 \<le> 2 ^ (length w1 - 1) * 2 ^(length w2 - 1)"
- apply (rule mult_mono)
- using bv_to_int_lower_range [of w1]
- apply simp
- using bv_to_int_lower_range [of w2]
- apply simp
- apply (rule zero_le_power,simp)
- using bi2
- apply simp
- done
- hence "?Q \<le> 2 ^ (length w1 - 1) * 2 ^(length w2 - 1)"
- by simp
- also have "... < 2 ^ (length w1 + length w2 - Suc 0)"
- apply simp
- apply (subst zpower_zadd_distrib [symmetric])
- apply simp
- apply (cut_tac lmw)
- apply arith
- apply (cut_tac p)
- apply arith
- done
- finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)" .
- qed
- qed
- next
- assume p: "?Q < -1"
- show ?thesis
- apply (subst bv_smult_def)
- apply (rule length_int_to_bv_upper_limit_lem1)
- apply (rule p)
- proof simp
- have "(2::int) ^ (length w1 - 1) * 2 ^(length w2 - 1) \<le> 2 ^ (length w1 + length w2 - Suc 0)"
- apply simp
- apply (subst zpower_zadd_distrib [symmetric])
- apply simp
- done
- hence "-((2::int) ^ (length w1 + length w2 - Suc 0)) \<le> -(2^(length w1 - 1) * 2 ^ (length w2 - 1))"
- by simp
- also have "... \<le> ?Q"
- proof -
- from p
- have q: "bv_to_int w1 * bv_to_int w2 < 0"
- by simp
- thus ?thesis
- proof (simp add: mult_less_0_iff,safe)
- assume bi1: "0 < bv_to_int w1"
- assume bi2: "bv_to_int w2 < 0"
- have "-bv_to_int w2 * bv_to_int w1 \<le> ((2::int)^(length w2 - 1)) * (2 ^ (length w1 - 1))"
- apply (rule mult_mono)
- using bv_to_int_lower_range [of w2]
- apply simp
- using bv_to_int_upper_range [of w1]
- apply simp
- apply (rule zero_le_power,simp)
- using bi1
- apply simp
- done
- hence "-?Q \<le> ((2::int)^(length w1 - 1)) * (2 ^ (length w2 - 1))"
- by (simp add: zmult_ac)
- thus "-(((2::int)^(length w1 - Suc 0)) * (2 ^ (length w2 - Suc 0))) \<le> ?Q"
- by simp
- next
- assume bi1: "bv_to_int w1 < 0"
- assume bi2: "0 < bv_to_int w2"
- have "-bv_to_int w1 * bv_to_int w2 \<le> ((2::int)^(length w1 - 1)) * (2 ^ (length w2 - 1))"
- apply (rule mult_mono)
- using bv_to_int_lower_range [of w1]
- apply simp
- using bv_to_int_upper_range [of w2]
- apply simp
- apply (rule zero_le_power,simp)
- using bi2
- apply simp
- done
- hence "-?Q \<le> ((2::int)^(length w1 - 1)) * (2 ^ (length w2 - 1))"
- by (simp add: zmult_ac)
- thus "-(((2::int)^(length w1 - Suc 0)) * (2 ^ (length w2 - Suc 0))) \<le> ?Q"
- by simp
- qed
- qed
- finally show "-(2 ^ (length w1 + length w2 - Suc 0)) \<le> ?Q" .
- qed
- qed
-qed
-
-lemma bv_msb_one: "bv_msb w = \<one> ==> bv_to_nat w \<noteq> 0"
-by (cases w) simp_all
-
-lemma bv_smult_length_utos: "length (bv_smult (utos w1) w2) \<le> length w1 + length w2"
-proof -
- let ?Q = "bv_to_int (utos w1) * bv_to_int w2"
-
- have lmw: "?Q \<noteq> 0 ==> 0 < length (utos w1) \<and> 0 < length w2" by auto
-
- have "0 < ?Q \<or> ?Q = 0 \<or> ?Q = -1 \<or> ?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)
- next
- assume "bv_to_int w2 = 0"
- thus ?thesis by (simp add: bv_smult_def)
- next
- assume p: "0 < ?Q"
- thus ?thesis
- proof (simp add: zero_less_mult_iff,safe)
- assume biw2: "0 < bv_to_int w2"
- show ?thesis
- apply (simp add: bv_smult_def)
- apply (rule length_int_to_bv_upper_limit_gt0)
- apply (rule p)
- proof simp
- have "?Q < 2 ^ length w1 * 2 ^ (length w2 - 1)"
- apply (rule mult_strict_mono)
- apply (simp add: bv_to_int_utos int_nat_two_exp)
- apply (rule bv_to_nat_upper_range)
- apply (rule bv_to_int_upper_range)
- apply (rule zero_less_power,simp)
- using biw2
- apply simp
- done
- also have "... \<le> 2 ^ (length w1 + length w2 - Suc 0)"
- apply simp
- apply (subst zpower_zadd_distrib [symmetric])
- apply simp
- apply (cut_tac lmw)
- apply arith
- using p
- apply auto
- done
- 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)
- qed
- next
- assume p: "?Q = -1"
- thus ?thesis
- apply (simp add: bv_smult_def)
- apply (cut_tac lmw)
- apply arith
- apply simp
- done
- next
- assume p: "?Q < -1"
- show ?thesis
- apply (subst bv_smult_def)
- apply (rule length_int_to_bv_upper_limit_lem1)
- apply (rule p)
- proof simp
- have "(2::int) ^ length w1 * 2 ^(length w2 - 1) \<le> 2 ^ (length w1 + length w2 - Suc 0)"
- apply simp
- apply (subst zpower_zadd_distrib [symmetric])
- apply simp
- apply (cut_tac lmw)
- apply arith
- apply (cut_tac p)
- apply arith
- done
- hence "-((2::int) ^ (length w1 + length w2 - Suc 0)) \<le> -(2^ length w1 * 2 ^ (length w2 - 1))"
- by simp
- also have "... \<le> ?Q"
- proof -
- from p
- have q: "bv_to_int (utos w1) * bv_to_int w2 < 0"
- by simp
- thus ?thesis
- proof (simp add: mult_less_0_iff,safe)
- assume bi1: "0 < bv_to_int (utos w1)"
- assume bi2: "bv_to_int w2 < 0"
- have "-bv_to_int w2 * bv_to_int (utos w1) \<le> ((2::int)^(length w2 - 1)) * (2 ^ length w1)"
- apply (rule mult_mono)
- using bv_to_int_lower_range [of w2]
- apply simp
- apply (simp add: bv_to_int_utos)
- using bv_to_nat_upper_range [of w1]
- apply (simp add: int_nat_two_exp)
- apply (rule zero_le_power,simp)
- using bi1
- apply simp
- done
- hence "-?Q \<le> ((2::int)^length w1) * (2 ^ (length w2 - 1))"
- by (simp add: zmult_ac)
- thus "-(((2::int)^length w1) * (2 ^ (length w2 - Suc 0))) \<le> ?Q"
- by simp
- next
- assume bi1: "bv_to_int (utos w1) < 0"
- thus "-(((2::int)^length w1) * (2 ^ (length w2 - Suc 0))) \<le> ?Q"
- by (simp add: bv_to_int_utos)
- qed
- qed
- finally show "-(2 ^ (length w1 + length w2 - Suc 0)) \<le> ?Q" .
- qed
- qed
-qed
-
-lemma bv_smult_sym: "bv_smult w1 w2 = bv_smult w2 w1"
- by (simp add: bv_smult_def zmult_ac)
-
-subsection {* Structural operations *}
-
-definition
- bv_select :: "[bit list,nat] => bit" where
- "bv_select w i = w ! (length w - 1 - i)"
-
-definition
- bv_chop :: "[bit list,nat] => bit list * bit list" where
- "bv_chop w i = (let len = length w in (take (len - i) w,drop (len - i) w))"
-
-definition
- bv_slice :: "[bit list,nat*nat] => bit list" where
- "bv_slice w = (\<lambda>(b,e). fst (bv_chop (snd (bv_chop w (b+1))) e))"
-
-lemma bv_select_rev:
- assumes notnull: "n < length w"
- shows "bv_select w n = rev w ! n"
-proof -
- have "\<forall>n. n < length w --> bv_select w n = rev w ! n"
- proof (rule length_induct [of _ w],auto simp add: bv_select_def)
- fix xs :: "bit list"
- fix n
- assume ind: "\<forall>ys::bit list. length ys < length xs --> (\<forall>n. n < length ys --> ys ! (length ys - Suc n) = rev ys ! n)"
- assume notx: "n < length xs"
- show "xs ! (length xs - Suc n) = rev xs ! n"
- proof (cases xs)
- assume "xs = []"
- with notx show ?thesis by simp
- next
- fix y ys
- assume [simp]: "xs = y # ys"
- show ?thesis
- proof (auto simp add: nth_append)
- assume noty: "n < length ys"
- from spec [OF ind,of ys]
- have "\<forall>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" ..
- 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 \<le> n" by simp
- from notx have "n < Suc (length ys)" by simp
- hence "n \<le> length ys" by simp
- with x have "length ys = n" by simp
- thus "y = [y] ! (n - length ys)" by simp
- qed
- qed
- qed
- 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)"
- by (simp add: bv_chop_def Let_def)
-
-lemma append_bv_chop_id: "fst (bv_chop w l) @ snd (bv_chop w l) = w"
- by (simp add: bv_chop_def Let_def)
-
-lemma bv_chop_length_fst [simp]: "length (fst (bv_chop w i)) = length w - i"
- by (simp add: bv_chop_def Let_def)
-
-lemma bv_chop_length_snd [simp]: "length (snd (bv_chop w i)) = min i (length w)"
- by (simp add: bv_chop_def Let_def)
-
-lemma bv_slice_length [simp]: "[| j \<le> i; i < length w |] ==> length (bv_slice w (i,j)) = i - j + 1"
- by (auto simp add: bv_slice_def)
-
-definition
- length_nat :: "nat => nat" where
- [code del]: "length_nat x = (LEAST n. x < 2 ^ n)"
-
-lemma length_nat: "length (nat_to_bv n) = length_nat n"
- apply (simp add: length_nat_def)
- apply (rule Least_equality [symmetric])
- prefer 2
- apply (rule length_nat_to_bv_upper_limit)
- apply arith
- apply (rule ccontr)
-proof -
- assume "~ n < 2 ^ length (nat_to_bv n)"
- hence "2 ^ length (nat_to_bv n) \<le> 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
-qed
-
-lemma length_nat_0 [simp]: "length_nat 0 = 0"
- by (simp add: length_nat_def Least_equality)
-
-lemma length_nat_non0:
- assumes n0: "n \<noteq> 0"
- shows "length_nat n = Suc (length_nat (n div 2))"
- apply (simp add: length_nat [symmetric])
- apply (subst nat_to_bv_non0 [of n])
- apply (simp_all add: n0)
- done
-
-definition
- length_int :: "int => nat" where
- "length_int x =
- (if 0 < x then Suc (length_nat (nat x))
- else if x = 0 then 0
- else Suc (length_nat (nat (-x - 1))))"
-
-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 (\<zero> # 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
- apply (simp del: norm_unsigned_nat_to_bv)
- apply (drule norm_empty_bv_to_nat_zero)
- using prems
- apply simp
- apply (cases "norm_unsigned (nat_to_bv (nat i))")
- apply (drule norm_empty_bv_to_nat_zero [of "nat_to_bv (nat i)"])
- using prems
- apply simp
- apply simp
- using prems
- apply (simp add: length_nat [symmetric])
- done
- finally show ?thesis
- using i0
- by (simp add: length_int_def)
-next
- assume "~ 0 < i"
- hence i0: "i \<le> 0" by simp
- show ?thesis
- proof (cases "i = 0")
- assume "i = 0"
- thus ?thesis by (simp add: length_int_def)
- next
- assume "i \<noteq> 0"
- with i0 have i0: "i < 0" by simp
- hence "length (int_to_bv i) =
- length (norm_signed (\<one> # 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))"
- apply safe
- apply (simp del: norm_unsigned_nat_to_bv)
- apply (drule norm_empty_bv_to_nat_zero [of "nat_to_bv (nat (-i) - Suc 0)"])
- using prems
- apply simp
- apply (cases "- i - 1 = 0")
- apply simp
- apply (simp add: length_nat [symmetric])
- apply (cases "norm_unsigned (nat_to_bv (nat (- i) - 1))")
- apply simp
- apply simp
- done
- finally
- show ?thesis
- using i0 by (simp add: length_int_def nat_diff_distrib del: int_to_bv_lt0)
- qed
-qed
-
-lemma length_int_0 [simp]: "length_int 0 = 0"
- by (simp add: length_int_def)
-
-lemma length_int_gt0: "0 < i ==> length_int i = Suc (length_nat (nat i))"
- by (simp add: length_int_def)
-
-lemma length_int_lt0: "i < 0 ==> length_int i = Suc (length_nat (nat (- i) - 1))"
- by (simp add: length_int_def nat_diff_distrib)
-
-lemma bv_chopI: "[| w = w1 @ w2 ; i = length w2 |] ==> bv_chop w i = (w1,w2)"
- by (simp add: bv_chop_def Let_def)
-
-lemma bv_sliceI: "[| j \<le> i ; i < length w ; w = w1 @ w2 @ w3 ; Suc i = length w2 + j ; j = length w3 |] ==> bv_slice w (i,j) = w2"
- apply (simp add: bv_slice_def)
- apply (subst bv_chopI [of "w1 @ w2 @ w3" w1 "w2 @ w3"])
- apply simp
- apply simp
- apply simp
- apply (subst bv_chopI [of "w2 @ w3" w2 w3],simp_all)
- done
-
-lemma bv_slice_bv_slice:
- assumes ki: "k \<le> i"
- and ij: "i \<le> j"
- and jl: "j \<le> l"
- and lw: "l < length w"
- shows "bv_slice w (j,i) = bv_slice (bv_slice w (l,k)) (j-k,i-k)"
-proof -
- def w1 == "fst (bv_chop w (Suc l))"
- and w2 == "fst (bv_chop (snd (bv_chop w (Suc l))) (Suc j))"
- and w3 == "fst (bv_chop (snd (bv_chop (snd (bv_chop w (Suc l))) (Suc j))) i)"
- and w4 == "fst (bv_chop (snd (bv_chop (snd (bv_chop (snd (bv_chop w (Suc l))) (Suc j))) i)) k)"
- and w5 == "snd (bv_chop (snd (bv_chop (snd (bv_chop (snd (bv_chop w (Suc l))) (Suc j))) i)) k)"
- note w_defs = this
-
- have w_def: "w = w1 @ w2 @ w3 @ w4 @ w5"
- by (simp add: w_defs append_bv_chop_id)
-
- from ki ij jl lw
- show ?thesis
- apply (subst bv_sliceI [where ?j = i and ?i = j and ?w = w and ?w1.0 = "w1 @ w2" and ?w2.0 = w3 and ?w3.0 = "w4 @ w5"])
- apply simp_all
- apply (rule w_def)
- apply (simp add: w_defs)
- apply (simp add: w_defs)
- apply (subst bv_sliceI [where ?j = k and ?i = l and ?w = w and ?w1.0 = w1 and ?w2.0 = "w2 @ w3 @ w4" and ?w3.0 = w5])
- apply simp_all
- apply (rule w_def)
- apply (simp add: w_defs)
- apply (simp add: w_defs)
- apply (subst bv_sliceI [where ?j = "i-k" and ?i = "j-k" and ?w = "w2 @ w3 @ w4" and ?w1.0 = w2 and ?w2.0 = w3 and ?w3.0 = w4])
- apply simp_all
- apply (simp_all add: w_defs)
- done
-qed
-
-lemma bv_to_nat_extend [simp]: "bv_to_nat (bv_extend n \<zero> w) = bv_to_nat w"
- apply (simp add: bv_extend_def)
- apply (subst bv_to_nat_dist_append)
- apply simp
- apply (induct ("n - length w"))
- apply simp_all
- done
-
-lemma bv_msb_extend_same [simp]: "bv_msb w = b ==> bv_msb (bv_extend n b w) = b"
- apply (simp add: bv_extend_def)
- apply (cases "n - length w")
- apply simp_all
- done
-
-lemma bv_to_int_extend [simp]:
- assumes a: "bv_msb w = b"
- shows "bv_to_int (bv_extend n b w) = bv_to_int w"
-proof (cases "bv_msb w")
- assume [simp]: "bv_msb w = \<zero>"
- with a have [simp]: "b = \<zero>" by simp
- show ?thesis by (simp add: bv_to_int_def)
-next
- assume [simp]: "bv_msb w = \<one>"
- with a have [simp]: "b = \<one>" by simp
- show ?thesis
- apply (simp add: bv_to_int_def)
- apply (simp add: bv_extend_def)
- apply (induct ("n - length w"), simp_all)
- done
-qed
-
-lemma length_nat_mono [simp]: "x \<le> y ==> length_nat x \<le> length_nat y"
-proof (rule ccontr)
- assume xy: "x \<le> y"
- assume "~ length_nat x \<le> length_nat y"
- hence lxly: "length_nat y < length_nat x"
- by simp
- hence "length_nat y < (LEAST n. x < 2 ^ n)"
- by (simp add: length_nat_def)
- hence "~ x < 2 ^ length_nat y"
- by (rule not_less_Least)
- hence xx: "2 ^ length_nat y \<le> x"
- by simp
- have yy: "y < 2 ^ length_nat y"
- apply (simp add: length_nat_def)
- apply (rule LeastI)
- apply (subgoal_tac "y < 2 ^ y",assumption)
- apply (cases "0 \<le> y")
- apply (induct y,simp_all)
- done
- with xx have "y < x" by simp
- with xy show False by simp
-qed
-
-lemma length_nat_mono_int [simp]: "x \<le> y ==> length_nat x \<le> length_nat y"
- 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 \<le> x ; x \<le> y |] ==> length_int x \<le> length_int y"
- by (cases "x = 0") (simp_all add: length_int_gt0 nat_le_eq_zle)
-
-lemma length_int_mono_lt0: "[| x \<le> y ; y \<le> 0 |] ==> length_int y \<le> length_int x"
- by (cases "y = 0") (simp_all add: length_int_lt0)
-
-lemmas [simp] = length_nat_non0
-
-lemma "nat_to_bv (number_of Int.Pls) = []"
- by simp
-
-primrec fast_bv_to_nat_helper :: "[bit list, int] => int" where
- 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 ((bit_case Int.Bit0 Int.Bit1 b) k)"
-
-declare fast_bv_to_nat_helper.simps [code del]
-
-lemma fast_bv_to_nat_Cons0: "fast_bv_to_nat_helper (\<zero>#bs) bin =
- fast_bv_to_nat_helper bs (Int.Bit0 bin)"
- by simp
-
-lemma fast_bv_to_nat_Cons1: "fast_bv_to_nat_helper (\<one>#bs) bin =
- fast_bv_to_nat_helper bs (Int.Bit1 bin)"
- by simp
-
-lemma fast_bv_to_nat_def:
- "bv_to_nat bs == number_of (fast_bv_to_nat_helper bs Int.Pls)"
-proof (simp add: bv_to_nat_def)
- have "\<forall> bin. \<not> (neg (number_of bin :: int)) \<longrightarrow> (foldl (%bn b. 2 * bn + bitval b) (number_of bin) bs) = number_of (fast_bv_to_nat_helper bs bin)"
- apply (induct bs,simp)
- apply (case_tac a,simp_all)
- done
- thus "foldl (\<lambda>bn b. 2 * bn + bitval b) 0 bs \<equiv> number_of (fast_bv_to_nat_helper bs Int.Pls)"
- by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric])
-qed
-
-declare fast_bv_to_nat_Cons [simp del]
-declare fast_bv_to_nat_Cons0 [simp]
-declare fast_bv_to_nat_Cons1 [simp]
-
-setup {*
-(*comments containing lcp are the removal of fast_bv_of_nat*)
-let
- fun is_const_bool (Const("True",_)) = true
- | is_const_bool (Const("False",_)) = true
- | is_const_bool _ = false
- fun is_const_bit (Const("Word.bit.Zero",_)) = true
- | is_const_bit (Const("Word.bit.One",_)) = true
- | is_const_bit _ = false
- fun num_is_usable (Const(@{const_name Int.Pls},_)) = true
- | num_is_usable (Const(@{const_name Int.Min},_)) = false
- | num_is_usable (Const(@{const_name Int.Bit0},_) $ w) =
- num_is_usable w
- | num_is_usable (Const(@{const_name Int.Bit1},_) $ w) =
- num_is_usable w
- | num_is_usable _ = false
- fun vec_is_usable (Const("List.list.Nil",_)) = true
- | vec_is_usable (Const("List.list.Cons",_) $ b $ bs) =
- vec_is_usable bs andalso is_const_bit b
- | vec_is_usable _ = false
- (*lcp** val fast1_th = PureThy.get_thm thy "Word.fast_nat_to_bv_def"*)
- val fast2_th = @{thm "Word.fast_bv_to_nat_def"};
- (*lcp** fun f sg thms (Const("Word.nat_to_bv",_) $ (Const(@{const_name Int.number_of},_) $ t)) =
- if num_is_usable t
- then SOME (Drule.cterm_instantiate [(cterm_of sg (Var (("w", 0), @{typ int})), cterm_of sg t)] fast1_th)
- else NONE
- | f _ _ _ = NONE *)
- fun g sg thms (Const("Word.bv_to_nat",_) $ (t as (Const("List.list.Cons",_) $ _ $ _))) =
- if vec_is_usable t then
- SOME (Drule.cterm_instantiate [(cterm_of sg (Var(("bs",0),Type("List.list",[Type("Word.bit",[])]))),cterm_of sg t)] fast2_th)
- else NONE
- | g _ _ _ = NONE
- (*lcp** val simproc1 = Simplifier.simproc thy "nat_to_bv" ["Word.nat_to_bv (number_of w)"] f *)
- val simproc2 = Simplifier.simproc @{theory} "bv_to_nat" ["Word.bv_to_nat (x # xs)"] g
-in
- Simplifier.map_simpset (fn ss => ss addsimprocs [(*lcp*simproc1,*)simproc2])
-end*}
-
-declare bv_to_nat1 [simp del]
-declare bv_to_nat_helper [simp del]
-
-definition
- bv_mapzip :: "[bit => bit => bit,bit list, bit list] => bit list" where
- "bv_mapzip f w1 w2 =
- (let g = bv_extend (max (length w1) (length w2)) \<zero>
- 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)"
- by (simp add: bv_mapzip_def Let_def split: split_max)
-
-lemma bv_mapzip_Nil [simp]: "bv_mapzip f [] [] = []"
- by (simp add: bv_mapzip_def Let_def)
-
-lemma bv_mapzip_Cons [simp]: "length w1 = length w2 ==>
- bv_mapzip f (x#w1) (y#w2) = f x y # bv_mapzip f w1 w2"
- by (simp add: bv_mapzip_def Let_def)
-
-end
--- a/src/HOL/Nat_Numeral.thy Tue May 18 00:01:03 2010 +0200
+++ b/src/HOL/Nat_Numeral.thy Tue May 18 00:01:51 2010 +0200
@@ -120,9 +120,9 @@
"a\<twosuperior> = 0 \<longleftrightarrow> a = 0"
unfolding power2_eq_square by simp
-lemma power2_eq_1_iff [simp]:
+lemma power2_eq_1_iff:
"a\<twosuperior> = 1 \<longleftrightarrow> a = 1 \<or> a = - 1"
- unfolding power2_eq_square by simp
+ unfolding power2_eq_square by (rule square_eq_1_iff)
end
--- a/src/HOL/Rings.thy Tue May 18 00:01:03 2010 +0200
+++ b/src/HOL/Rings.thy Tue May 18 00:01:51 2010 +0200
@@ -349,7 +349,7 @@
class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors
begin
-lemma square_eq_1_iff [simp]:
+lemma square_eq_1_iff:
"x * x = 1 \<longleftrightarrow> x = 1 \<or> x = - 1"
proof -
have "(x - 1) * (x + 1) = x * x - 1"
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Tue May 18 00:01:03 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Tue May 18 00:01:51 2010 +0200
@@ -34,8 +34,8 @@
axiom_clauses: (thm * (string * int)) list option,
filtered_clauses: (thm * (string * int)) list option}
datatype failure =
- Unprovable | TimedOut | OutOfResources | OldSpass | MalformedOutput |
- UnknownError
+ Unprovable | TimedOut | OutOfResources | OldSpass | MalformedInput |
+ MalformedOutput | UnknownError
type prover_result =
{outcome: failure option,
message: string,
@@ -95,8 +95,8 @@
filtered_clauses: (thm * (string * int)) list option};
datatype failure =
- Unprovable | TimedOut | OutOfResources | OldSpass | MalformedOutput |
- UnknownError
+ Unprovable | TimedOut | OutOfResources | OldSpass | MalformedInput |
+ MalformedOutput | UnknownError
type prover_result =
{outcome: failure option,
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Tue May 18 00:01:03 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Tue May 18 00:01:51 2010 +0200
@@ -100,6 +100,9 @@
(Path.variable "ISABELLE_HOME_USER" ::
map Path.basic ["etc", "components"]))) ^
"\" on a line of its own."
+ | string_for_failure MalformedInput =
+ "Internal Sledgehammer error: The ATP problem is malformed. Please report \
+ \this to the Isabelle developers."
| string_for_failure MalformedOutput = "Error: The ATP output is malformed."
| string_for_failure UnknownError = "Error: An unknown ATP error occurred."
@@ -336,7 +339,8 @@
known_failures =
[(Unprovable, "SPASS beiseite: Completion found"),
(TimedOut, "SPASS beiseite: Ran out of time"),
- (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded")],
+ (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
+ (MalformedInput, "Undefined symbol")],
max_axiom_clauses = 40,
prefers_theory_relevant = true}
val spass = dfg_prover "spass" spass_config
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Tue May 18 00:01:03 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Tue May 18 00:01:51 2010 +0200
@@ -141,9 +141,10 @@
in
if is_conjecture then
(Metis.Thm.axiom (Metis.LiteralSet.fromList mlits),
- add_type_literals types_sorts)
+ type_literals_for_types types_sorts)
else
- let val tylits = add_type_literals (filter (not o default_sort ctxt) types_sorts)
+ let val tylits = filter_out (default_sort ctxt) types_sorts
+ |> type_literals_for_types
val mtylits = if Config.get ctxt type_lits
then map (metis_of_type_literals false) tylits else []
in
@@ -216,6 +217,8 @@
fun strip_happ args (Metis.Term.Fn(".",[t,u])) = strip_happ (u::args) t
| strip_happ args x = (x, args);
+fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS)
+
fun fol_type_to_isa _ (Metis.Term.Var v) =
(case strip_prefix tvar_prefix v of
SOME w => make_tvar w
@@ -599,9 +602,9 @@
(*Extract TFree constraints from context to include as conjecture clauses*)
fun init_tfrees ctxt =
- let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts
- in
- add_type_literals (Vartab.fold add (#2 (Variable.constraints_of ctxt)) [])
+ let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts in
+ Vartab.fold add (#2 (Variable.constraints_of ctxt)) []
+ |> type_literals_for_types
end;
(*transform isabelle type / arity clause to metis clause *)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Tue May 18 00:01:03 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Tue May 18 00:01:51 2010 +0200
@@ -352,7 +352,7 @@
fun subtract_cls ax_clauses =
filter_out (Termtab.defined (mk_clause_table ax_clauses) o prop_of)
-fun all_valid_thms respect_no_atp ctxt =
+fun all_valid_thms respect_no_atp ctxt chain_ths =
let
val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt);
val local_facts = ProofContext.facts_of ctxt;
@@ -371,7 +371,8 @@
val name2 = Name_Space.extern full_space name;
val ths = filter_out bad_for_atp ths0;
in
- if Facts.is_concealed facts name orelse null ths orelse
+ if Facts.is_concealed facts name orelse
+ forall (member Thm.eq_thm chain_ths) ths orelse
(respect_no_atp andalso is_package_def name) then
I
else case find_first check_thms [name1, name2, name] of
@@ -396,10 +397,10 @@
(* The single-name theorems go after the multiple-name ones, so that single
names are preferred when both are available. *)
-fun name_thm_pairs respect_no_atp ctxt =
+fun name_thm_pairs respect_no_atp ctxt chain_ths =
let
val (mults, singles) =
- List.partition is_multi (all_valid_thms respect_no_atp ctxt)
+ List.partition is_multi (all_valid_thms respect_no_atp ctxt chain_ths)
val ps = [] |> fold add_single_names singles
|> fold add_multi_names mults
in ps |> respect_no_atp ? filter_out (No_ATPs.member ctxt o snd) end;
@@ -408,11 +409,11 @@
(warning ("No name for theorem " ^ Display.string_of_thm_without_context th); false)
| check_named _ = true;
-fun get_all_lemmas respect_no_atp ctxt =
+fun get_all_lemmas respect_no_atp ctxt chain_ths =
let val included_thms =
tap (fn ths => trace_msg
(fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems")))
- (name_thm_pairs respect_no_atp ctxt)
+ (name_thm_pairs respect_no_atp ctxt chain_ths)
in
filter check_named included_thms
end;
@@ -509,14 +510,14 @@
fun get_relevant_facts respect_no_atp relevance_threshold relevance_convergence
defs_relevant max_new theory_relevant
(relevance_override as {add, only, ...})
- (ctxt, (chain_ths, th)) goal_cls =
+ (ctxt, (chain_ths, _)) goal_cls =
if (only andalso null add) orelse relevance_threshold > 1.0 then
[]
else
let
val thy = ProofContext.theory_of ctxt
val is_FO = is_first_order thy goal_cls
- val included_cls = get_all_lemmas respect_no_atp ctxt
+ val included_cls = get_all_lemmas respect_no_atp ctxt chain_ths
|> cnf_rules_pairs thy |> make_unique
|> restrict_to_logic thy is_FO
|> remove_unwanted_clauses
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Tue May 18 00:01:03 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Tue May 18 00:01:51 2010 +0200
@@ -48,7 +48,7 @@
TyLitVar of string * name |
TyLitFree of string * name
exception CLAUSE of string * term
- val add_type_literals : typ list -> type_literal list
+ val type_literals_for_types : typ list -> type_literal list
val get_tvar_strs: typ list -> string list
datatype arLit =
TConsLit of class * string * string list
@@ -331,7 +331,8 @@
| pred_of_sort (TyLitFree (s, _)) = (s, 1)
(*Given a list of sorted type variables, return a list of type literals.*)
-fun add_type_literals Ts = fold (union (op =)) (map sorts_on_typs Ts) []
+fun type_literals_for_types Ts =
+ fold (union (op =)) (map sorts_on_typs Ts) []
(*The correct treatment of TFrees like 'a in lemmas (axiom clauses) is not clear.
* Ignoring them leads to unsound proofs, since we do nothing to ensure that 'a
@@ -520,7 +521,7 @@
dfg_forall vars ("or(" ^ commas lits ^ ")") ^ ",\n" ^
string_of_clausename (cls_id,ax_name) ^ ").\n\n";
-fun string_of_arity (name, num) = "(" ^ name ^ "," ^ Int.toString num ^ ")"
+fun string_of_arity (name, arity) = "(" ^ name ^ ", " ^ Int.toString arity ^ ")"
fun string_of_preds [] = ""
| string_of_preds preds = "predicates[" ^ commas(map string_of_arity preds) ^ "].\n";
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Tue May 18 00:01:03 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Tue May 18 00:01:51 2010 +0200
@@ -300,7 +300,7 @@
let
val (lits, pool) = pool_map (tptp_literal params) literals pool
val (tylits, pool) = pool_map (tptp_of_type_literal pos)
- (add_type_literals ctypes_sorts) pool
+ (type_literals_for_types ctypes_sorts) pool
in ((lits, tylits), pool) end
fun tptp_clause params (cls as HOLClause {axiom_name, clause_id, kind, ...})
@@ -320,7 +320,8 @@
fun dfg_type_literals params pos (HOLClause {literals, ctypes_sorts, ...}) =
pool_map (dfg_literal params) literals
- #>> rpair (map (dfg_of_type_literal pos) (add_type_literals ctypes_sorts))
+ #>> rpair (map (dfg_of_type_literal pos)
+ (type_literals_for_types ctypes_sorts))
fun get_uvars (CombConst _) vars pool = (vars, pool)
| get_uvars (CombVar (name, _)) vars pool =
@@ -531,6 +532,8 @@
(* DFG format *)
+fun dfg_tfree_predicate s = (first_field "(" s |> the |> fst, 1)
+
fun write_dfg_file full_types explicit_apply file clauses =
let
(* Some of the helper functions below are not name-pool-aware. However,
@@ -543,13 +546,16 @@
val params = (full_types, explicit_apply, cma, cnh)
val ((conjecture_clss, tfree_litss), pool) =
pool_map (dfg_clause params) conjectures pool |>> ListPair.unzip
- and problem_name = Path.implode (Path.base file)
+ val tfree_lits = union_all tfree_litss
+ val problem_name = Path.implode (Path.base file)
val (axstrs, pool) = pool_map (apfst fst oo dfg_clause params) axclauses pool
- val tfree_clss = map dfg_tfree_clause (union_all tfree_litss)
+ val tfree_clss = map dfg_tfree_clause tfree_lits
+ val tfree_preds = map dfg_tfree_predicate tfree_lits
val (helper_clauses_strs, pool) =
pool_map (apfst fst oo dfg_clause params) helper_clauses pool
val (funcs, cl_preds) = decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses
- and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses
+ val ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses
+ val preds = tfree_preds @ cl_preds @ ty_preds
val conjecture_offset =
length axclauses + length classrel_clauses + length arity_clauses
+ length helper_clauses
@@ -559,7 +565,7 @@
string_of_start problem_name ::
string_of_descrip problem_name ::
string_of_symbols (string_of_funcs funcs)
- (string_of_preds (cl_preds @ ty_preds)) ::
+ (string_of_preds preds) ::
"list_of_clauses(axioms, cnf).\n" ::
axstrs @
map dfg_classrel_clause classrel_clauses @
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue May 18 00:01:03 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue May 18 00:01:51 2010 +0200
@@ -14,7 +14,6 @@
val invert_const: string -> string
val invert_type_const: string -> string
val num_type_args: theory -> string -> int
- val make_tvar: string -> typ
val strip_prefix: string -> string -> string option
val metis_line: int -> int -> string list -> string
val metis_proof_text:
@@ -235,26 +234,27 @@
SOME c' => c'
| NONE => c;
-fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS);
-fun make_tparam s = TypeInfer.param 0 (s, HOLogic.typeS)
-fun make_var (b,T) = Var((b,0),T);
-
(* Type variables are given the basic sort "HOL.type". Some will later be
constrained by information from type literals, or by type inference. *)
-fun type_from_node (u as IntLeaf _) = raise NODE [u]
- | type_from_node (u as StrNode (a, us)) =
- let val Ts = map type_from_node us in
+fun type_from_node _ (u as IntLeaf _) = raise NODE [u]
+ | type_from_node tfrees (u as StrNode (a, us)) =
+ let val Ts = map (type_from_node tfrees) us in
case strip_prefix tconst_prefix a of
SOME b => Type (invert_type_const b, Ts)
| NONE =>
if not (null us) then
raise NODE [u] (* only "tconst"s have type arguments *)
else case strip_prefix tfree_prefix a of
- SOME b => TFree ("'" ^ b, HOLogic.typeS)
+ SOME b =>
+ let val s = "'" ^ b in
+ TFree (s, AList.lookup (op =) tfrees s |> the_default HOLogic.typeS)
+ end
| NONE =>
case strip_prefix tvar_prefix a of
- SOME b => make_tvar b
- | NONE => make_tparam a (* Variable from the ATP, say "X1" *)
+ SOME b => TVar (("'" ^ b, 0), HOLogic.typeS)
+ | NONE =>
+ (* Variable from the ATP, say "X1" *)
+ TypeInfer.param 0 (a, HOLogic.typeS)
end
(*Invert the table of translations between Isabelle and ATPs*)
@@ -287,7 +287,7 @@
(* First-order translation. No types are known for variables. "HOLogic.typeT"
should allow them to be inferred.*)
-fun term_from_node thy full_types =
+fun term_from_node thy full_types tfrees =
let
fun aux opt_T args u =
case u of
@@ -298,7 +298,8 @@
| StrNode (a, us) =>
if a = type_wrapper_name then
case us of
- [term_u, typ_u] => aux (SOME (type_from_node typ_u)) args term_u
+ [term_u, typ_u] =>
+ aux (SOME (type_from_node tfrees typ_u)) args term_u
| _ => raise NODE us
else case strip_prefix const_prefix a of
SOME "equal" =>
@@ -324,7 +325,8 @@
(* Extra args from "hAPP" come after any arguments
given directly to the constant. *)
Sign.const_instance thy (c,
- map type_from_node (drop num_term_args us)))
+ map (type_from_node tfrees)
+ (drop num_term_args us)))
in list_comb (t, ts) end
| NONE => (* a free or schematic variable *)
let
@@ -335,21 +337,22 @@
SOME b => Free (b, T)
| NONE =>
case strip_prefix schematic_var_prefix a of
- SOME b => make_var (b, T)
+ SOME b => Var ((b, 0), T)
| NONE =>
(* Variable from the ATP, say "X1" *)
- make_var (fix_atp_variable_name a, T)
+ Var ((fix_atp_variable_name a, 0), T)
in list_comb (t, ts) end
in aux end
(* Type class literal applied to a type. Returns triple of polarity, class,
type. *)
-fun type_constraint_from_node pos (StrNode ("c_Not", [u])) =
- type_constraint_from_node (not pos) u
- | type_constraint_from_node pos u = case u of
+fun type_constraint_from_node pos tfrees (StrNode ("c_Not", [u])) =
+ type_constraint_from_node (not pos) tfrees u
+ | type_constraint_from_node pos tfrees u = case u of
IntLeaf _ => raise NODE [u]
| StrNode (a, us) =>
- (case (strip_prefix class_prefix a, map type_from_node us) of
+ (case (strip_prefix class_prefix a,
+ map (type_from_node tfrees) us) of
(SOME b, [T]) => (pos, b, T)
| _ => raise NODE [u])
@@ -395,24 +398,24 @@
|> clause_for_literals thy
(*Accumulate sort constraints in vt, with "real" literals in lits.*)
-fun lits_of_nodes thy full_types (vt, lits) us =
- case us of
- [] => (vt, finish_clause thy lits)
- | (u :: us) =>
- lits_of_nodes thy full_types
- (add_type_constraint (type_constraint_from_node true u) vt, lits) us
- handle NODE _ =>
- lits_of_nodes thy full_types
- (vt, term_from_node thy full_types (SOME @{typ bool})
- [] u :: lits) us
+fun lits_of_nodes thy full_types tfrees =
+ let
+ fun aux (vt, lits) [] = (vt, finish_clause thy lits)
+ | aux (vt, lits) (u :: us) =
+ aux (add_type_constraint
+ (type_constraint_from_node true tfrees u) vt, lits) us
+ handle NODE _ =>
+ aux (vt, term_from_node thy full_types tfrees (SOME @{typ bool})
+ [] u :: lits) us
+ in aux end
-(*Update TVars/TFrees with detected sort constraints.*)
-fun repair_sorts vt =
+(* Update TVars with detected sort constraints. It's not totally clear when
+ this code is necessary. *)
+fun repair_tvar_sorts vt =
let
fun do_type (Type (a, Ts)) = Type (a, map do_type Ts)
| do_type (TVar (xi, s)) = TVar (xi, the_default s (Vartab.lookup vt xi))
- | do_type (TFree (x, s)) =
- TFree (x, the_default s (Vartab.lookup vt (x, ~1)))
+ | do_type (TFree z) = TFree z
fun do_term (Const (a, T)) = Const (a, do_type T)
| do_term (Free (a, T)) = Free (a, do_type T)
| do_term (Var (xi, T)) = Var (xi, do_type T)
@@ -444,45 +447,28 @@
(* Interpret a list of syntax trees as a clause, given by "real" literals and
sort constraints. "vt" holds the initial sort constraints, from the
conjecture clauses. *)
-fun clause_of_nodes ctxt full_types vt us =
+fun clause_of_nodes ctxt full_types tfrees us =
let
val thy = ProofContext.theory_of ctxt
- val (vt, t) = lits_of_nodes thy full_types (vt, []) us
- in repair_sorts vt t end
+ val (vt, t) = lits_of_nodes thy full_types tfrees (Vartab.empty, []) us
+ in repair_tvar_sorts vt t end
fun check_formula ctxt =
TypeInfer.constrain @{typ bool}
#> Syntax.check_term (ProofContext.set_mode ProofContext.mode_schematic ctxt)
-(** Global sort constraints on TFrees (from tfree_tcs) are positive unit
- clauses. **)
-
-fun add_tfree_constraint (true, cl, TFree (a, _)) = add_var ((a, ~1), cl)
- | add_tfree_constraint _ = I
-fun tfree_constraints_of_clauses vt [] = vt
- | tfree_constraints_of_clauses vt ([lit] :: uss) =
- (tfree_constraints_of_clauses (add_tfree_constraint
- (type_constraint_from_node true lit) vt) uss
- handle NODE _ => (* Not a positive type constraint? Ignore the literal. *)
- tfree_constraints_of_clauses vt uss)
- | tfree_constraints_of_clauses vt (_ :: uss) =
- tfree_constraints_of_clauses vt uss
-
(**** Translation of TSTP files to Isar Proofs ****)
fun unvarify_term (Var ((s, 0), T)) = Free (s, T)
| unvarify_term t = raise TERM ("unvarify_term: non-Var", [t])
-fun clauses_in_lines (Definition (_, u, us)) = u :: us
- | clauses_in_lines (Inference (_, us, _)) = us
-
-fun decode_line full_types vt (Definition (num, u, us)) ctxt =
+fun decode_line full_types tfrees (Definition (num, u, us)) ctxt =
let
- val t1 = clause_of_nodes ctxt full_types vt [u]
+ val t1 = clause_of_nodes ctxt full_types tfrees [u]
val vars = snd (strip_comb t1)
val frees = map unvarify_term vars
val unvarify_args = subst_atomic (vars ~~ frees)
- val t2 = clause_of_nodes ctxt full_types vt us
+ val t2 = clause_of_nodes ctxt full_types tfrees us
val (t1, t2) =
HOLogic.eq_const HOLogic.typeT $ t1 $ t2
|> unvarify_args |> uncombine_term |> check_formula ctxt
@@ -491,19 +477,16 @@
(Definition (num, t1, t2),
fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt)
end
- | decode_line full_types vt (Inference (num, us, deps)) ctxt =
+ | decode_line full_types tfrees (Inference (num, us, deps)) ctxt =
let
- val t = us |> clause_of_nodes ctxt full_types vt
+ val t = us |> clause_of_nodes ctxt full_types tfrees
|> unskolemize_term |> uncombine_term |> check_formula ctxt
in
(Inference (num, t, deps),
fold Variable.declare_term (OldTerm.term_frees t) ctxt)
end
-fun decode_lines ctxt full_types lines =
- let
- val vt = tfree_constraints_of_clauses Vartab.empty
- (map clauses_in_lines lines)
- in #1 (fold_map (decode_line full_types vt) lines ctxt) end
+fun decode_lines ctxt full_types tfrees lines =
+ fst (fold_map (decode_line full_types tfrees) lines ctxt)
fun aint_inference _ (Definition _) = true
| aint_inference t (Inference (_, t', _)) = not (t aconv t')
@@ -599,8 +582,7 @@
| extract_num _ = NONE
in atp_proof |> split_lines |> map_filter (extract_num o tokens_of) end
-(* Used to label theorems chained into the Sledgehammer call (or rather
- goal?) *)
+(* Used to label theorems chained into the goal. *)
val chained_hint = "sledgehammer_chained"
fun apply_command _ 1 = "by "
@@ -674,13 +656,13 @@
forall_vars t,
ByMetis (fold (add_fact_from_dep thm_names) deps ([], [])))
-fun proof_from_atp_proof pool ctxt full_types isar_shrink_factor atp_proof
- conjecture_shape thm_names params frees =
+fun proof_from_atp_proof pool ctxt full_types tfrees isar_shrink_factor
+ atp_proof conjecture_shape thm_names params frees =
let
val lines =
atp_proof ^ "$" (* the $ sign acts as a sentinel *)
|> parse_proof pool
- |> decode_lines ctxt full_types
+ |> decode_lines ctxt full_types tfrees
|> rpair [] |-> fold_rev (add_line conjecture_shape thm_names)
|> rpair [] |-> fold_rev add_nontrivial_line
|> rpair (0, []) |-> fold_rev (add_desired_line ctxt isar_shrink_factor
@@ -839,7 +821,7 @@
apfst (map (fn l => AList.lookup (op =) subst l |> the_default l))
fun do_step (step as Assume (l, t)) (proof, subst, assums) =
(case AList.lookup (op aconv) assums t of
- SOME l' => (proof, (l', l) :: subst, assums)
+ SOME l' => (proof, (l, l') :: subst, assums)
| NONE => (step :: proof, subst, (t, l) :: assums))
| do_step (Have (qs, l, t, by)) (proof, subst, assums) =
(Have (qs, l, t,
@@ -988,11 +970,12 @@
val thy = ProofContext.theory_of ctxt
val (params, hyp_ts, concl_t) = strip_subgoal goal i
val frees = fold Term.add_frees (concl_t :: hyp_ts) []
+ val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) []
val n = Logic.count_prems (prop_of goal)
val (one_line_proof, lemma_names) =
metis_proof_text (minimize_command, atp_proof, thm_names, goal, i)
fun isar_proof_for () =
- case proof_from_atp_proof pool ctxt full_types isar_shrink_factor
+ case proof_from_atp_proof pool ctxt full_types tfrees isar_shrink_factor
atp_proof conjecture_shape thm_names params
frees
|> redirect_proof thy conjecture_shape hyp_ts concl_t
--- a/src/HOL/Transcendental.thy Tue May 18 00:01:03 2010 +0200
+++ b/src/HOL/Transcendental.thy Tue May 18 00:01:51 2010 +0200
@@ -1778,7 +1778,7 @@
lemma sin_pi_half [simp]: "sin(pi/2) = 1"
apply (cut_tac x = "pi/2" in sin_cos_squared_add2)
apply (cut_tac sin_gt_zero [OF pi_half_gt_zero pi_half_less_two])
-apply (simp add: power2_eq_square)
+apply (simp add: power2_eq_1_iff)
done
lemma cos_pi [simp]: "cos pi = -1"
--- a/src/HOL/ex/Adder.thy Tue May 18 00:01:03 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,115 +0,0 @@
-(* Title: HOL/ex/Adder.thy
- ID: $Id$
- Author: Sergey Tverdyshev (Universitaet des Saarlandes)
-*)
-
-header {* Implementation of carry chain incrementor and adder *}
-
-theory Adder imports Main Word begin
-
-lemma [simp]: "bv_to_nat [b] = bitval b"
- by (simp add: bv_to_nat_helper)
-
-lemma bv_to_nat_helper':
- "bv \<noteq> [] ==> bv_to_nat bv = bitval (hd bv) * 2 ^ (length bv - 1) + bv_to_nat (tl bv)"
- by (cases bv) (simp_all add: bv_to_nat_helper)
-
-definition
- half_adder :: "[bit, bit] => bit list" where
- "half_adder a b = [a bitand b, a bitxor b]"
-
-lemma half_adder_correct: "bv_to_nat (half_adder a b) = bitval a + bitval b"
- apply (simp add: half_adder_def)
- apply (cases a, auto)
- apply (cases b, auto)
- done
-
-lemma [simp]: "length (half_adder a b) = 2"
- by (simp add: half_adder_def)
-
-definition
- full_adder :: "[bit, bit, bit] => bit list" where
- "full_adder a b c =
- (let x = a bitxor b in [a bitand b bitor c bitand x, x bitxor c])"
-
-lemma full_adder_correct:
- "bv_to_nat (full_adder a b c) = bitval a + bitval b + bitval c"
- apply (simp add: full_adder_def Let_def)
- apply (cases a, auto)
- apply (case_tac [!] b, auto)
- apply (case_tac [!] c, auto)
- done
-
-lemma [simp]: "length (full_adder a b c) = 2"
- by (simp add: full_adder_def Let_def)
-
-
-subsection {* Carry chain incrementor *}
-
-consts
- carry_chain_inc :: "[bit list, bit] => bit list"
-primrec
- "carry_chain_inc [] c = [c]"
- "carry_chain_inc (a#as) c =
- (let chain = carry_chain_inc as c
- in half_adder a (hd chain) @ tl chain)"
-
-lemma cci_nonnull: "carry_chain_inc as c \<noteq> []"
- by (cases as) (auto simp add: Let_def half_adder_def)
-
-lemma cci_length [simp]: "length (carry_chain_inc as c) = length as + 1"
- by (induct as) (simp_all add: Let_def)
-
-lemma cci_correct: "bv_to_nat (carry_chain_inc as c) = bv_to_nat as + bitval c"
- apply (induct as)
- apply (cases c, simp_all add: Let_def bv_to_nat_dist_append)
- apply (simp add: half_adder_correct bv_to_nat_helper' [OF cci_nonnull]
- ring_distribs bv_to_nat_helper)
- done
-
-consts
- carry_chain_adder :: "[bit list, bit list, bit] => bit list"
-primrec
- "carry_chain_adder [] bs c = [c]"
- "carry_chain_adder (a # as) bs c =
- (let chain = carry_chain_adder as (tl bs) c
- in full_adder a (hd bs) (hd chain) @ tl chain)"
-
-lemma cca_nonnull: "carry_chain_adder as bs c \<noteq> []"
- by (cases as) (auto simp add: full_adder_def Let_def)
-
-lemma cca_length: "length as = length bs \<Longrightarrow>
- length (carry_chain_adder as bs c) = Suc (length bs)"
- by (induct as arbitrary: bs) (auto simp add: Let_def)
-
-theorem cca_correct:
- "length as = length bs \<Longrightarrow>
- bv_to_nat (carry_chain_adder as bs c) =
- bv_to_nat as + bv_to_nat bs + bitval c"
-proof (induct as arbitrary: bs)
- case Nil
- then show ?case by simp
-next
- case (Cons a as xs)
- note ind = Cons.hyps
- from Cons.prems have len: "Suc (length as) = length xs" by simp
- show ?case
- proof (cases xs)
- case Nil
- with len show ?thesis by simp
- next
- case (Cons b bs)
- with len have len': "length as = length bs" by simp
- then have "bv_to_nat (carry_chain_adder as bs c) = bv_to_nat as + bv_to_nat bs + bitval c"
- by (rule ind)
- with len' and Cons
- show ?thesis
- apply (simp add: Let_def)
- apply (subst bv_to_nat_dist_append)
- apply (simp add: full_adder_correct bv_to_nat_helper' [OF cca_nonnull]
- ring_distribs bv_to_nat_helper cca_length)
- done
- qed
-qed
-
-end
--- a/src/HOL/ex/Codegenerator_Candidates.thy Tue May 18 00:01:03 2010 +0200
+++ b/src/HOL/ex/Codegenerator_Candidates.thy Tue May 18 00:01:51 2010 +0200
@@ -23,7 +23,6 @@
RBT
SetsAndFunctions
While_Combinator
- Word
begin
inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
--- a/src/HOL/ex/ROOT.ML Tue May 18 00:01:03 2010 +0200
+++ b/src/HOL/ex/ROOT.ML Tue May 18 00:01:51 2010 +0200
@@ -7,7 +7,6 @@
"State_Monad",
"Efficient_Nat_examples",
"FuncSet",
- "Word",
"Eval_Examples",
"Codegenerator_Test",
"Codegenerator_Pretty_Test",
@@ -46,7 +45,6 @@
"Unification",
"Primrec",
"Tarski",
- "Adder",
"Classical",
"set",
"Meson_Test",