--- a/src/HOL/Word/Bit_Int.thy Tue Dec 13 23:22:27 2011 +0100
+++ b/src/HOL/Word/Bit_Int.thy Wed Dec 14 07:38:30 2011 +0100
@@ -54,7 +54,7 @@
lemma bin_rec_Bit:
"f = bin_rec f1 f2 f3 ==> f3 Int.Pls (0::bit) f1 = f1 ==>
f3 Int.Min (1::bit) f2 = f2 ==> f (w BIT b) = f3 w b (f w)"
- by (cases b, simp add: bin_rec_Bit0, simp add: bin_rec_Bit1)
+ by (cases b, simp add: bin_rec_Bit0 BIT_simps, simp add: bin_rec_Bit1 BIT_simps)
lemmas bin_rec_simps = refl [THEN bin_rec_Bit] bin_rec_Pls bin_rec_Min
bin_rec_Bit0 bin_rec_Bit1
@@ -95,7 +95,8 @@
"NOT (Int.Bit0 w) = Int.Bit1 (NOT w)"
"NOT (Int.Bit1 w) = Int.Bit0 (NOT w)"
"NOT (w BIT b) = (NOT w) BIT (NOT b)"
- unfolding int_not_def Pls_def [symmetric] Min_def [symmetric] by (simp_all add: bin_rec_simps)
+ unfolding int_not_def Pls_def [symmetric] Min_def [symmetric]
+ by (simp_all add: bin_rec_simps BIT_simps)
lemma int_xor_Pls [simp]:
"Int.Pls XOR x = x"
@@ -133,7 +134,8 @@
lemma int_or_Bits [simp]:
"(x BIT b) OR (y BIT c) = (x OR y) BIT (b OR c)"
- unfolding int_or_def Pls_def [symmetric] Min_def [symmetric] by (simp add: bin_rec_simps)
+ unfolding int_or_def Pls_def [symmetric] Min_def [symmetric]
+ by (simp add: bin_rec_simps BIT_simps)
lemma int_or_Bits2 [simp]:
"(Int.Bit0 x) OR (Int.Bit0 y) = Int.Bit0 (x OR y)"
@@ -144,7 +146,7 @@
lemma int_and_Pls [simp]:
"Int.Pls AND x = Int.Pls"
- unfolding int_and_def by (simp add: bin_rec_PM)
+ unfolding int_and_def Pls_def [symmetric] by (simp add: bin_rec_PM)
lemma int_and_Min [simp]:
"Int.Min AND x = x"
@@ -152,7 +154,8 @@
lemma int_and_Bits [simp]:
"(x BIT b) AND (y BIT c) = (x AND y) BIT (b AND c)"
- unfolding int_and_def Pls_def [symmetric] Min_def [symmetric] by (simp add: bin_rec_simps)
+ unfolding int_and_def Pls_def [symmetric] Min_def [symmetric]
+ by (simp add: bin_rec_simps BIT_simps)
lemma int_and_Bits2 [simp]:
"(Int.Bit0 x) AND (Int.Bit0 y) = Int.Bit0 (x AND y)"
@@ -322,7 +325,7 @@
apply (case_tac x rule: bin_exhaust)
apply (case_tac b)
apply (case_tac [!] bit)
- apply (auto simp: less_eq_int_code)
+ apply (auto simp: less_eq_int_code BIT_simps)
done
lemmas int_and_le =
@@ -334,7 +337,7 @@
apply (induct x rule: bin_induct)
apply clarsimp
apply clarsimp
- apply (case_tac bit, auto)
+ apply (case_tac bit, auto simp: BIT_simps)
done
subsubsection {* Truncating results of bit-wise operations *}
@@ -447,10 +450,10 @@
done
lemma bin_sc_FP [simp]: "bin_sc n 0 Int.Pls = Int.Pls"
- by (induct n) auto
+ by (induct n) (auto simp: BIT_simps)
lemma bin_sc_TM [simp]: "bin_sc n 1 Int.Min = Int.Min"
- by (induct n) auto
+ by (induct n) (auto simp: BIT_simps)
lemmas bin_sc_simps = bin_sc.Z bin_sc.Suc bin_sc_TM bin_sc_FP
@@ -566,7 +569,7 @@
lemma bin_split_Pls [simp]:
"bin_split n Int.Pls = (Int.Pls, Int.Pls)"
- by (induct n) (auto simp: Let_def split: ls_splits)
+ by (induct n) (auto simp: Let_def BIT_simps split: ls_splits)
lemma bin_split_Min [simp]:
"bin_split n Int.Min = (Int.Min, bintrunc n Int.Min)"
@@ -578,7 +581,7 @@
apply (induct n, clarsimp)
apply (simp add: bin_rest_trunc Let_def split: ls_splits)
apply (case_tac m)
- apply (auto simp: Let_def split: ls_splits)
+ apply (auto simp: Let_def BIT_simps split: ls_splits)
done
lemma bin_split_trunc1:
@@ -587,7 +590,7 @@
apply (induct n, clarsimp)
apply (simp add: bin_rest_trunc Let_def split: ls_splits)
apply (case_tac m)
- apply (auto simp: Let_def split: ls_splits)
+ apply (auto simp: Let_def BIT_simps split: ls_splits)
done
lemma bin_cat_num:
@@ -598,7 +601,7 @@
lemma bin_split_num:
"!!b. bin_split n b = (b div 2 ^ n, b mod 2 ^ n)"
- apply (induct n, clarsimp)
+ apply (induct n, simp add: Pls_def)
apply (simp add: bin_rest_def zdiv_zmult2_eq)
apply (case_tac b rule: bin_exhaust)
apply simp
--- a/src/HOL/Word/Bit_Representation.thy Tue Dec 13 23:22:27 2011 +0100
+++ b/src/HOL/Word/Bit_Representation.thy Wed Dec 14 07:38:30 2011 +0100
@@ -23,45 +23,66 @@
definition Bit :: "int \<Rightarrow> bit \<Rightarrow> int" (infixl "BIT" 90) where
"k BIT b = bitval b + k + k"
-lemma BIT_B0_eq_Bit0 [simp]: "w BIT 0 = Int.Bit0 w"
+definition bin_last :: "int \<Rightarrow> bit" where
+ "bin_last w = (if w mod 2 = 0 then (0::bit) else (1::bit))"
+
+definition bin_rest :: "int \<Rightarrow> int" where
+ "bin_rest w = w div 2"
+
+lemma bin_rl_simp [simp]:
+ "bin_rest w BIT bin_last w = w"
+ unfolding bin_rest_def bin_last_def Bit_def
+ using mod_div_equality [of w 2]
+ by (cases "w mod 2 = 0", simp_all)
+
+lemma bin_rest_BIT: "bin_rest (x BIT b) = x"
+ unfolding bin_rest_def Bit_def
+ by (cases b, simp_all)
+
+lemma bin_last_BIT: "bin_last (x BIT b) = b"
+ unfolding bin_last_def Bit_def
+ by (cases b, simp_all add: z1pmod2)
+
+lemma BIT_eq_iff [iff]: "u BIT b = v BIT c \<longleftrightarrow> u = v \<and> b = c"
+ by (metis bin_rest_BIT bin_last_BIT)
+
+lemma BIT_bin_simps [simp]:
+ "number_of w BIT 0 = number_of (Int.Bit0 w)"
+ "number_of w BIT 1 = number_of (Int.Bit1 w)"
+ unfolding Bit_def number_of_is_id numeral_simps by simp_all
+
+lemma BIT_special_simps [simp]:
+ shows "0 BIT 0 = 0" and "0 BIT 1 = 1" and "1 BIT 0 = 2" and "1 BIT 1 = 3"
+ unfolding Bit_def by simp_all
+
+lemma bin_last_numeral_simps [simp]:
+ "bin_last 0 = 0"
+ "bin_last 1 = 1"
+ "bin_last -1 = 1"
+ "bin_last (number_of (Int.Bit0 w)) = 0"
+ "bin_last (number_of (Int.Bit1 w)) = 1"
+ unfolding bin_last_def by simp_all
+
+lemma bin_rest_numeral_simps [simp]:
+ "bin_rest 0 = 0"
+ "bin_rest 1 = 0"
+ "bin_rest -1 = -1"
+ "bin_rest (number_of (Int.Bit0 w)) = number_of w"
+ "bin_rest (number_of (Int.Bit1 w)) = number_of w"
+ unfolding bin_rest_def by simp_all
+
+lemma BIT_B0_eq_Bit0: "w BIT 0 = Int.Bit0 w"
unfolding Bit_def Bit0_def by simp
-lemma BIT_B1_eq_Bit1 [simp]: "w BIT 1 = Int.Bit1 w"
+lemma BIT_B1_eq_Bit1: "w BIT 1 = Int.Bit1 w"
unfolding Bit_def Bit1_def by simp
lemmas BIT_simps = BIT_B0_eq_Bit0 BIT_B1_eq_Bit1
-lemma Min_ne_Pls [iff]:
- "Int.Min ~= Int.Pls"
- unfolding Min_def Pls_def by auto
-
-lemmas Pls_ne_Min [iff] = Min_ne_Pls [symmetric]
-
-lemmas PlsMin_defs [intro!] =
- Pls_def Min_def Pls_def [symmetric] Min_def [symmetric]
-
-lemmas PlsMin_simps [simp] = PlsMin_defs [THEN Eq_TrueI]
-
lemma number_of_False_cong:
"False \<Longrightarrow> number_of x = number_of y"
by (rule FalseE)
-(** ways in which type Bin resembles a datatype **)
-
-lemma BIT_eq: "u BIT b = v BIT c ==> u = v & b = c"
- apply (cases b) apply (simp_all)
- apply (cases c) apply (simp_all)
- apply (cases c) apply (simp_all)
- done
-
-lemmas BIT_eqE [elim!] = BIT_eq [THEN conjE]
-
-lemma BIT_eq_iff [simp]:
- "(u BIT b = v BIT c) = (u = v \<and> b = c)"
- by (rule iffI) auto
-
-lemmas BIT_eqI [intro!] = conjI [THEN BIT_eq_iff [THEN iffD2]]
-
lemma less_Bits:
"(v BIT b < w BIT c) = (v < w | v <= w & b = (0::bit) & c = (1::bit))"
unfolding Bit_def by (auto simp add: bitval_def split: bit.split)
@@ -127,21 +148,11 @@
subsection {* Destructors for binary integers *}
-definition bin_last :: "int \<Rightarrow> bit" where
- "bin_last w = (if w mod 2 = 0 then (0::bit) else (1::bit))"
-
-definition bin_rest :: "int \<Rightarrow> int" where
- "bin_rest w = w div 2"
-
definition bin_rl :: "int \<Rightarrow> int \<times> bit" where
"bin_rl w = (bin_rest w, bin_last w)"
lemma bin_rl_char: "bin_rl w = (r, l) \<longleftrightarrow> r BIT l = w"
- apply (cases l)
- apply (auto simp add: bin_rl_def bin_last_def bin_rest_def)
- unfolding Pls_def Min_def Bit0_def Bit1_def number_of_is_id
- apply arith+
- done
+ unfolding bin_rl_def by (auto simp: bin_rest_BIT bin_last_BIT)
primrec bin_nth where
Z: "bin_nth w 0 = (bin_last w = (1::bit))"
@@ -153,11 +164,7 @@
"bin_rl (Int.Bit0 r) = (r, (0::bit))"
"bin_rl (Int.Bit1 r) = (r, (1::bit))"
"bin_rl (r BIT b) = (r, b)"
- unfolding bin_rl_char by simp_all
-
-lemma bin_rl_simp [simp]:
- "bin_rest w BIT bin_last w = w"
- by (simp add: iffD1 [OF bin_rl_char bin_rl_def])
+ unfolding bin_rl_char by (simp_all add: BIT_simps)
lemma bin_abs_lem:
"bin = (w BIT b) ==> ~ bin = Int.Min --> ~ bin = Int.Pls -->
@@ -193,11 +200,11 @@
apply (rule Min)
apply (case_tac bit)
apply (case_tac "bin = Int.Pls")
- apply simp
- apply (simp add: Bit0)
+ apply (simp add: BIT_simps)
+ apply (simp add: Bit0 BIT_simps)
apply (case_tac "bin = Int.Min")
- apply simp
- apply (simp add: Bit1)
+ apply (simp add: BIT_simps)
+ apply (simp add: Bit1 BIT_simps)
done
lemma bin_rest_simps [simp]:
@@ -216,25 +223,14 @@
"bin_last (w BIT b) = b"
using bin_rl_simps bin_rl_def by auto
-lemma bin_r_l_extras [simp]:
- "bin_last 0 = (0::bit)"
- "bin_last (- 1) = (1::bit)"
- "bin_last -1 = (1::bit)"
- "bin_last 1 = (1::bit)"
- "bin_rest 1 = 0"
- "bin_rest 0 = 0"
- "bin_rest (- 1) = - 1"
- "bin_rest -1 = -1"
- by (simp_all add: bin_last_def bin_rest_def)
-
lemma Bit_div2 [simp]: "(w BIT b) div 2 = w"
unfolding bin_rest_def [symmetric] by auto
lemma Bit0_div2 [simp]: "(Int.Bit0 w) div 2 = w"
- using Bit_div2 [where b="(0::bit)"] by simp
+ using Bit_div2 [where b="(0::bit)"] by (simp add: BIT_simps)
lemma Bit1_div2 [simp]: "(Int.Bit1 w) div 2 = w"
- using Bit_div2 [where b="(1::bit)"] by simp
+ using Bit_div2 [where b="(1::bit)"] by (simp add: BIT_simps)
lemma bin_nth_lem [rule_format]:
"ALL y. bin_nth x = bin_nth y --> x = y"
@@ -246,20 +242,20 @@
apply (drule_tac x=0 in fun_cong, force)
apply (erule notE, rule ext,
drule_tac x="Suc x" in fun_cong, force)
- apply (drule_tac x=0 in fun_cong, force)
+ apply (drule_tac x=0 in fun_cong, force simp: BIT_simps)
apply (erule rev_mp)
apply (induct_tac y rule: bin_induct)
apply (safe del: subset_antisym)
apply (drule_tac x=0 in fun_cong, force)
apply (erule notE, rule ext,
drule_tac x="Suc x" in fun_cong, force)
- apply (drule_tac x=0 in fun_cong, force)
+ apply (drule_tac x=0 in fun_cong, force simp: BIT_simps)
apply (case_tac y rule: bin_exhaust)
apply clarify
apply (erule allE)
apply (erule impE)
prefer 2
- apply (erule BIT_eqI)
+ apply (erule conjI)
apply (drule_tac x=0 in fun_cong, force)
apply (rule ext)
apply (drule_tac x="Suc ?x" in fun_cong, force)
@@ -273,6 +269,9 @@
lemma bin_eq_iff: "x = y \<longleftrightarrow> (\<forall>n. bin_nth x n = bin_nth y n)"
by (auto intro!: bin_nth_lem del: equalityI)
+lemma bin_nth_zero [simp]: "\<not> bin_nth 0 n"
+ by (induct n) auto
+
lemma bin_nth_Pls [simp]: "~ bin_nth Int.Pls n"
by (induct n) auto
@@ -290,11 +289,11 @@
lemma bin_nth_minus_Bit0 [simp]:
"0 < n ==> bin_nth (Int.Bit0 w) n = bin_nth w (n - 1)"
- using bin_nth_minus [where b="(0::bit)"] by simp
+ using bin_nth_minus [where b="(0::bit)"] by (simp add: BIT_simps)
lemma bin_nth_minus_Bit1 [simp]:
"0 < n ==> bin_nth (Int.Bit1 w) n = bin_nth w (n - 1)"
- using bin_nth_minus [where b="(1::bit)"] by simp
+ using bin_nth_minus [where b="(1::bit)"] by (simp add: BIT_simps)
lemmas bin_nth_0 = bin_nth.simps(1)
lemmas bin_nth_Suc = bin_nth.simps(2)
@@ -306,16 +305,21 @@
subsection {* Truncating binary integers *}
-definition
+definition bin_sign :: "int \<Rightarrow> int" where
bin_sign_def: "bin_sign k = (if k \<ge> 0 then 0 else - 1)"
lemma bin_sign_simps [simp]:
+ "bin_sign 0 = 0"
+ "bin_sign -1 = -1"
+ "bin_sign (number_of (Int.Bit0 w)) = bin_sign (number_of w)"
+ "bin_sign (number_of (Int.Bit1 w)) = bin_sign (number_of w)"
"bin_sign Int.Pls = Int.Pls"
"bin_sign Int.Min = Int.Min"
"bin_sign (Int.Bit0 w) = bin_sign w"
"bin_sign (Int.Bit1 w) = bin_sign w"
"bin_sign (w BIT b) = bin_sign w"
- by (unfold bin_sign_def numeral_simps Bit_def bitval_def) (simp_all split: bit.split)
+ unfolding bin_sign_def numeral_simps Bit_def bitval_def number_of_is_id
+ by (simp_all split: bit.split)
lemma bin_sign_rest [simp]:
"bin_sign (bin_rest w) = bin_sign w"
@@ -334,7 +338,9 @@
"sbintrunc 0 bin =
(case bin_last bin of (1::bit) => - 1 | (0::bit) => 0)"
"sbintrunc (Suc n) bin = sbintrunc n (bin_rest bin) BIT (bin_last bin)"
- apply simp_all apply (cases "bin_last bin") apply simp apply (unfold Min_def number_of_is_id) apply simp done
+ apply simp_all
+ apply (simp only: Pls_def Min_def)
+ done
lemma sign_bintr:
"!!w. bin_sign (bintrunc n w) = Int.Pls"
@@ -342,7 +348,8 @@
lemma bintrunc_mod2p:
"!!w. bintrunc n w = (w mod 2 ^ n :: int)"
- apply (induct n, clarsimp)
+ apply (induct n)
+ apply (simp add: Pls_def)
apply (simp add: bin_last_def bin_rest_def Bit_def zmod_zmult2_eq
cong: number_of_False_cong)
done
@@ -354,7 +361,7 @@
apply (subst mod_add_left_eq)
apply (simp add: bin_last_def)
apply (simp add: number_of_eq)
- apply clarsimp
+ apply (simp add: Pls_def)
apply (simp add: bin_last_def bin_rest_def Bit_def
cong: number_of_False_cong)
apply (clarsimp simp: mod_mult_mult1 [symmetric]
@@ -366,6 +373,34 @@
subsection "Simplifications for (s)bintrunc"
+lemma bintrunc_n_0 [simp]: "bintrunc n 0 = 0"
+ by (induct n) (auto simp add: Int.Pls_def)
+
+lemma sbintrunc_n_0 [simp]: "sbintrunc n 0 = 0"
+ by (induct n) (auto simp add: Int.Pls_def)
+
+lemma sbintrunc_n_minus1 [simp]: "sbintrunc n -1 = -1"
+ by (induct n) (auto, simp add: number_of_is_id)
+
+lemma bintrunc_Suc_numeral:
+ "bintrunc (Suc n) 1 = 1"
+ "bintrunc (Suc n) -1 = bintrunc n -1 BIT 1"
+ "bintrunc (Suc n) (number_of (Int.Bit0 w)) = bintrunc n (number_of w) BIT 0"
+ "bintrunc (Suc n) (number_of (Int.Bit1 w)) = bintrunc n (number_of w) BIT 1"
+ by simp_all
+
+lemma sbintrunc_0_numeral [simp]:
+ "sbintrunc 0 1 = -1"
+ "sbintrunc 0 (number_of (Int.Bit0 w)) = 0"
+ "sbintrunc 0 (number_of (Int.Bit1 w)) = -1"
+ by (simp_all, unfold Pls_def number_of_is_id, simp_all)
+
+lemma sbintrunc_Suc_numeral:
+ "sbintrunc (Suc n) 1 = 1"
+ "sbintrunc (Suc n) (number_of (Int.Bit0 w)) = sbintrunc n (number_of w) BIT 0"
+ "sbintrunc (Suc n) (number_of (Int.Bit1 w)) = sbintrunc n (number_of w) BIT 1"
+ by simp_all
+
lemma bit_bool:
"(b = (b' = (1::bit))) = (b' = (if b then (1::bit) else (0::bit)))"
by (cases b') auto
@@ -399,11 +434,11 @@
lemma bin_nth_Bit0:
"bin_nth (Int.Bit0 w) n = (EX m. n = Suc m & bin_nth w m)"
- using bin_nth_Bit [where b="(0::bit)"] by simp
+ using bin_nth_Bit [where b="(0::bit)"] by (simp add: BIT_simps)
lemma bin_nth_Bit1:
"bin_nth (Int.Bit1 w) n = (n = 0 | (EX m. n = Suc m & bin_nth w m))"
- using bin_nth_Bit [where b="(1::bit)"] by simp
+ using bin_nth_Bit [where b="(1::bit)"] by (simp add: BIT_simps)
lemma bintrunc_bintrunc_l:
"n <= m ==> (bintrunc m (bintrunc n w) = bintrunc n w)"
@@ -440,14 +475,15 @@
lemma bintrunc_Bit0 [simp]:
"bintrunc (Suc n) (Int.Bit0 w) = Int.Bit0 (bintrunc n w)"
- using bintrunc_BIT [where b="(0::bit)"] by simp
+ using bintrunc_BIT [where b="(0::bit)"] by (simp add: BIT_simps)
lemma bintrunc_Bit1 [simp]:
"bintrunc (Suc n) (Int.Bit1 w) = Int.Bit1 (bintrunc n w)"
- using bintrunc_BIT [where b="(1::bit)"] by simp
+ using bintrunc_BIT [where b="(1::bit)"] by (simp add: BIT_simps)
lemmas bintrunc_Sucs = bintrunc_Pls bintrunc_Min bintrunc_BIT
bintrunc_Bit0 bintrunc_Bit1
+ bintrunc_Suc_numeral
lemmas sbintrunc_Suc_Pls =
sbintrunc.Suc [where bin="Int.Pls", simplified bin_last_simps bin_rest_simps]
@@ -460,14 +496,15 @@
lemma sbintrunc_Suc_Bit0 [simp]:
"sbintrunc (Suc n) (Int.Bit0 w) = Int.Bit0 (sbintrunc n w)"
- using sbintrunc_Suc_BIT [where b="(0::bit)"] by simp
+ using sbintrunc_Suc_BIT [where b="(0::bit)"] by (simp add: BIT_simps)
lemma sbintrunc_Suc_Bit1 [simp]:
"sbintrunc (Suc n) (Int.Bit1 w) = Int.Bit1 (sbintrunc n w)"
- using sbintrunc_Suc_BIT [where b="(1::bit)"] by simp
+ using sbintrunc_Suc_BIT [where b="(1::bit)"] by (simp add: BIT_simps)
lemmas sbintrunc_Sucs = sbintrunc_Suc_Pls sbintrunc_Suc_Min sbintrunc_Suc_BIT
sbintrunc_Suc_Bit0 sbintrunc_Suc_Bit1
+ sbintrunc_Suc_numeral
lemmas sbintrunc_Pls =
sbintrunc.Z [where bin="Int.Pls",
@@ -513,12 +550,12 @@
lemma bintrunc_n_Pls [simp]:
"bintrunc n Int.Pls = Int.Pls"
- by (induct n) auto
+ by (induct n) (auto simp: BIT_simps)
lemma sbintrunc_n_PM [simp]:
"sbintrunc n Int.Pls = Int.Pls"
"sbintrunc n Int.Min = Int.Min"
- by (induct n) auto
+ by (induct n) (auto simp: BIT_simps)
lemmas thobini1 = arg_cong [where f = "%w. w BIT b"] for b
@@ -531,9 +568,9 @@
lemmas bintrunc_BIT_minus_I = bmsts(3)
lemma bintrunc_0_Min: "bintrunc 0 Int.Min = Int.Pls"
- by auto
+ by (fact bintrunc.Z) (* FIXME: delete *)
lemma bintrunc_0_BIT: "bintrunc 0 (w BIT b) = Int.Pls"
- by auto
+ by (fact bintrunc.Z) (* FIXME: delete *)
lemma bintrunc_Suc_lem:
"bintrunc (Suc n) x = y ==> m = Suc n ==> bintrunc m x = y"
--- a/src/HOL/Word/Bool_List_Representation.thy Tue Dec 13 23:22:27 2011 +0100
+++ b/src/HOL/Word/Bool_List_Representation.thy Wed Dec 14 07:38:30 2011 +0100
@@ -184,7 +184,7 @@
done
lemma bl_to_bin_False: "bl_to_bin (False # bl) = bl_to_bin bl"
- unfolding bl_to_bin_def by auto
+ unfolding bl_to_bin_def by (auto simp: BIT_simps)
lemma bl_to_bin_Nil: "bl_to_bin [] = Int.Pls"
unfolding bl_to_bin_def by auto
@@ -231,8 +231,10 @@
apply auto
done
-lemmas bin_to_bl_bintr =
- bin_to_bl_aux_bintr [where bl = "[]", folded bin_to_bl_def]
+lemma bin_to_bl_bintr:
+ "bin_to_bl n (bintrunc m bin) =
+ replicate (n - m) False @ bin_to_bl (min n m) bin"
+ unfolding bin_to_bl_def by (rule bin_to_bl_aux_bintr)
lemma bl_to_bin_rep_False: "bl_to_bin (replicate n False) = Int.Pls"
by (induct n) auto
@@ -301,7 +303,8 @@
apply arith
done
-lemmas nth_rev_alt = nth_rev [where xs = "rev ys", simplified] for ys
+lemma nth_rev_alt: "n < length ys \<Longrightarrow> ys ! n = rev ys ! (length ys - Suc n)"
+ by (simp add: nth_rev)
lemma nth_bin_to_bl_aux [rule_format] :
"ALL w n bl. n < m + length bl --> (bin_to_bl_aux m w bl) ! n =
@@ -323,7 +326,8 @@
apply clarsimp
apply safe
apply (erule allE, erule xtr8 [rotated],
- simp add: numeral_simps algebra_simps cong add : number_of_False_cong)+
+ simp add: numeral_simps algebra_simps BIT_simps
+ cong add: number_of_False_cong)+
done
lemma bl_to_bin_lt2p: "bl_to_bin bs < (2 ^ length bs)"
@@ -341,14 +345,15 @@
apply clarsimp
apply safe
apply (erule allE, erule preorder_class.order_trans [rotated],
- simp add: numeral_simps algebra_simps cong add : number_of_False_cong)+
+ simp add: numeral_simps algebra_simps BIT_simps
+ cong add: number_of_False_cong)+
done
lemma bl_to_bin_ge0: "bl_to_bin bs >= 0"
apply (unfold bl_to_bin_def)
apply (rule xtr4)
apply (rule bl_to_bin_ge2p_aux)
- apply simp
+ apply (simp add: Pls_def)
done
lemma butlast_rest_bin:
@@ -360,8 +365,9 @@
apply (auto simp add: bin_to_bl_aux_alt)
done
-lemmas butlast_bin_rest = butlast_rest_bin
- [where w="bl_to_bin bl" and n="length bl", simplified] for bl
+lemma butlast_bin_rest:
+ "butlast bl = bin_to_bl (length bl - Suc 0) (bin_rest (bl_to_bin bl))"
+ using butlast_rest_bin [where w="bl_to_bin bl" and n="length bl"] by simp
lemma butlast_rest_bl2bin_aux:
"bl ~= [] \<Longrightarrow>
@@ -384,13 +390,13 @@
apply safe
apply (case_tac "m - size list")
apply (simp add : diff_is_0_eq [THEN iffD1, THEN Suc_diff_le])
- apply simp
+ apply (simp add: BIT_simps)
apply (rule_tac f = "%nat. bl_to_bin_aux list (Int.Bit1 (bintrunc nat w))"
in arg_cong)
apply simp
apply (case_tac "m - size list")
apply (simp add: diff_is_0_eq [THEN iffD1, THEN Suc_diff_le])
- apply simp
+ apply (simp add: BIT_simps)
apply (rule_tac f = "%nat. bl_to_bin_aux list (Int.Bit0 (bintrunc nat w))"
in arg_cong)
apply simp
@@ -400,8 +406,9 @@
"bintrunc m (bl_to_bin bl) = bl_to_bin (drop (length bl - m) bl)"
unfolding bl_to_bin_def by (simp add : trunc_bl2bin_aux)
-lemmas trunc_bl2bin_len [simp] =
- trunc_bl2bin [of "length bl" bl, simplified] for bl
+lemma trunc_bl2bin_len [simp]:
+ "bintrunc (length bl) (bl_to_bin bl) = bl_to_bin bl"
+ by (simp add: trunc_bl2bin)
lemma bl2bin_drop:
"bl_to_bin (drop k bl) = bintrunc (length bl - k) (bl_to_bin bl)"
@@ -491,17 +498,20 @@
apply clarsimp
done
-lemmas bl_not_bin = bl_not_aux_bin
- [where cs = "[]", unfolded bin_to_bl_def [symmetric] map.simps]
+lemma bl_not_bin: "map Not (bin_to_bl n w) = bin_to_bl n (NOT w)"
+ unfolding bin_to_bl_def by (simp add: bl_not_aux_bin)
-lemmas bl_and_bin = bl_and_aux_bin [where bs="[]" and cs="[]",
- unfolded map2_Nil, folded bin_to_bl_def]
+lemma bl_and_bin:
+ "map2 (op \<and>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v AND w)"
+ unfolding bin_to_bl_def by (simp add: bl_and_aux_bin)
-lemmas bl_or_bin = bl_or_aux_bin [where bs="[]" and cs="[]",
- unfolded map2_Nil, folded bin_to_bl_def]
+lemma bl_or_bin:
+ "map2 (op \<or>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v OR w)"
+ unfolding bin_to_bl_def by (simp add: bl_or_aux_bin)
-lemmas bl_xor_bin = bl_xor_aux_bin [where bs="[]" and cs="[]",
- unfolded map2_Nil, folded bin_to_bl_def]
+lemma bl_xor_bin:
+ "map2 (\<lambda>x y. x \<noteq> y) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v XOR w)"
+ unfolding bin_to_bl_def by (simp only: bl_xor_aux_bin map2_Nil)
lemma drop_bin2bl_aux [rule_format] :
"ALL m bin bs. drop m (bin_to_bl_aux n bin bs) =
@@ -615,10 +625,11 @@
lemma bl_bin_bl_rtf:
"bin_to_bl n (bl_to_bin bl) = rev (takefill False n (rev bl))"
by (simp add : takefill_bintrunc)
-
-lemmas bl_bin_bl_rep_drop =
- bl_bin_bl_rtf [simplified takefill_alt,
- simplified, simplified rev_take, simplified]
+
+lemma bl_bin_bl_rep_drop:
+ "bin_to_bl n (bl_to_bin bl) =
+ replicate (n - length bl) False @ drop (length bl - n) bl"
+ by (simp add: bl_bin_bl_rtf takefill_alt rev_take)
lemma tf_rev:
"n + k = m + length bl ==> takefill x m (rev (takefill y n bl)) =
@@ -660,12 +671,15 @@
bin_to_bl_aux nv v (bin_to_bl_aux nw w bs)"
by (induct nw) auto
-lemmas bl_to_bin_aux_alt =
- bl_to_bin_aux_cat [where nv = "0" and v = "Int.Pls",
- simplified bl_to_bin_def [symmetric], simplified]
+lemma bl_to_bin_aux_alt:
+ "bl_to_bin_aux bs w = bin_cat w (length bs) (bl_to_bin bs)"
+ using bl_to_bin_aux_cat [where nv = "0" and v = "Int.Pls"]
+ unfolding bl_to_bin_def [symmetric] by simp
-lemmas bin_to_bl_cat =
- bin_to_bl_aux_cat [where bs = "[]", folded bin_to_bl_def]
+lemma bin_to_bl_cat:
+ "bin_to_bl (nv + nw) (bin_cat v nw w) =
+ bin_to_bl_aux nv v (bin_to_bl nw w)"
+ unfolding bin_to_bl_def by (simp add: bin_to_bl_aux_cat)
lemmas bl_to_bin_aux_app_cat =
trans [OF bl_to_bin_aux_append bl_to_bin_aux_alt]
@@ -673,11 +687,13 @@
lemmas bin_to_bl_aux_cat_app =
trans [OF bin_to_bl_aux_cat bin_to_bl_aux_alt]
-lemmas bl_to_bin_app_cat = bl_to_bin_aux_app_cat
- [where w = "Int.Pls", folded bl_to_bin_def]
+lemma bl_to_bin_app_cat:
+ "bl_to_bin (bsa @ bs) = bin_cat (bl_to_bin bsa) (length bs) (bl_to_bin bs)"
+ by (simp only: bl_to_bin_aux_app_cat bl_to_bin_def)
-lemmas bin_to_bl_cat_app = bin_to_bl_aux_cat_app
- [where bs = "[]", folded bin_to_bl_def]
+lemma bin_to_bl_cat_app:
+ "bin_to_bl (n + nw) (bin_cat w nw wa) = bin_to_bl n w @ bin_to_bl nw wa"
+ by (simp only: bin_to_bl_def bin_to_bl_aux_cat_app)
(* bl_to_bin_app_cat_alt and bl_to_bin_app_cat are easily interderivable *)
lemma bl_to_bin_app_cat_alt:
@@ -688,10 +704,10 @@
Int.succ (bl_to_bin (replicate n True))"
apply (unfold bl_to_bin_def)
apply (induct n)
- apply simp
+ apply (simp add: BIT_simps)
apply (simp only: Suc_eq_plus1 replicate_add
append_Cons [symmetric] bl_to_bin_aux_append)
- apply simp
+ apply (simp add: BIT_simps)
done
(* function bl_of_nth *)
@@ -725,7 +741,8 @@
apply simp
done
-lemmas bl_of_nth_nth [simp] = order_refl [THEN bl_of_nth_nth_le, simplified]
+lemma bl_of_nth_nth [simp]: "bl_of_nth (length xs) (op ! (rev xs)) = xs"
+ by (simp add: bl_of_nth_nth_le)
lemma size_rbl_pred: "length (rbl_pred bl) = length bl"
by (induct bl) auto
@@ -754,7 +771,7 @@
apply clarsimp
apply (case_tac bin rule: bin_exhaust)
apply (case_tac b)
- apply (clarsimp simp: bin_to_bl_aux_alt)+
+ apply (clarsimp simp: bin_to_bl_aux_alt BIT_simps)+
done
lemma rbl_succ:
@@ -764,7 +781,7 @@
apply clarsimp
apply (case_tac bin rule: bin_exhaust)
apply (case_tac b)
- apply (clarsimp simp: bin_to_bl_aux_alt)+
+ apply (clarsimp simp: bin_to_bl_aux_alt BIT_simps)+
done
lemma rbl_add:
@@ -777,7 +794,7 @@
apply (case_tac binb rule: bin_exhaust)
apply (case_tac b)
apply (case_tac [!] "ba")
- apply (auto simp: rbl_succ succ_def bin_to_bl_aux_alt Let_def add_ac)
+ apply (auto simp: rbl_succ succ_def bin_to_bl_aux_alt Let_def add_ac BIT_simps)
done
lemma rbl_add_app2:
@@ -863,8 +880,8 @@
apply (case_tac binb rule: bin_exhaust)
apply (case_tac b)
apply (case_tac [!] "ba")
- apply (auto simp: bin_to_bl_aux_alt Let_def)
- apply (auto simp: rbbl_Cons rbl_mult_Suc rbl_add)
+ apply (auto simp: bin_to_bl_aux_alt Let_def BIT_simps)
+ apply (auto simp: rbbl_Cons rbl_mult_Suc rbl_add BIT_simps)
done
lemma rbl_add_split:
@@ -927,8 +944,9 @@
lemmas if_simps = if_x_Not if_Not_x if_cancel if_True if_False if_bool_simps
-lemmas seqr = eq_reflection [where x = "size w"] for w
+lemmas seqr = eq_reflection [where x = "size w"] for w (* FIXME: delete *)
+(* TODO: move name bindings to List.thy *)
lemmas tl_Nil = tl.simps (1)
lemmas tl_Cons = tl.simps (2)
--- a/src/HOL/Word/Word.thy Tue Dec 13 23:22:27 2011 +0100
+++ b/src/HOL/Word/Word.thy Wed Dec 14 07:38:30 2011 +0100
@@ -1255,7 +1255,7 @@
lemma word_sp_01 [simp] :
"word_succ -1 = 0 & word_succ 0 = 1 & word_pred 0 = -1 & word_pred 1 = 0"
- by (unfold word_0_no word_1_no) auto
+ by (unfold word_0_no word_1_no) (auto simp: BIT_simps)
(* alternative approach to lifting arithmetic equalities *)
lemma word_of_int_Ex:
@@ -2541,10 +2541,10 @@
apply clarsimp
apply (case_tac "n")
apply (clarsimp simp add : word_1_wi [symmetric])
- apply (clarsimp simp add : word_0_wi [symmetric])
+ apply (clarsimp simp add : word_0_wi [symmetric] BIT_simps)
apply (drule word_gt_0 [THEN iffD1])
apply (safe intro!: word_eqI bin_nth_lem ext)
- apply (auto simp add: test_bit_2p nth_2p_bin word_test_bit_def [symmetric])
+ apply (auto simp add: test_bit_2p nth_2p_bin word_test_bit_def [symmetric] BIT_simps)
done
lemma word_of_int_2p: "(word_of_int (2 ^ n) :: 'a :: len word) = 2 ^ n"
@@ -2556,7 +2556,7 @@
apply (rule box_equals)
apply (rule_tac [2] bintr_ariths (1))+
apply (clarsimp simp add : number_of_is_id)
- apply simp
+ apply (simp add: BIT_simps)
done
lemma bang_is_le: "x !! m \<Longrightarrow> 2 ^ m <= (x :: 'a :: len word)"
@@ -2599,7 +2599,7 @@
done
lemma shiftl1_0 [simp] : "shiftl1 0 = 0"
- unfolding word_0_no shiftl1_number by auto
+ unfolding word_0_no shiftl1_number by (auto simp: BIT_simps)
lemmas shiftl1_def_u = shiftl1_def [folded word_number_of_def]
@@ -2920,13 +2920,13 @@
(* note - the following results use 'a :: len word < number_ring *)
lemma shiftl1_2t: "shiftl1 (w :: 'a :: len word) = 2 * w"
- apply (simp add: shiftl1_def_u)
+ apply (simp add: shiftl1_def_u BIT_simps)
apply (simp only: double_number_of_Bit0 [symmetric])
apply simp
done
lemma shiftl1_p: "shiftl1 (w :: 'a :: len word) = w + w"
- apply (simp add: shiftl1_def_u)
+ apply (simp add: shiftl1_def_u BIT_simps)
apply (simp only: double_number_of_Bit0 [symmetric])
apply simp
done
@@ -4599,4 +4599,7 @@
setup {* SMT_Word.setup *}
+text {* Legacy simp rules *}
+declare BIT_simps [simp]
+
end