--- a/src/HOL/Word/Bit_Int.thy Tue Dec 13 12:10:43 2011 +0100
+++ b/src/HOL/Word/Bit_Int.thy Tue Dec 13 12:36:41 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)"
@@ -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:
--- a/src/HOL/Word/Bit_Representation.thy Tue Dec 13 12:10:43 2011 +0100
+++ b/src/HOL/Word/Bit_Representation.thy Tue Dec 13 12:36:41 2011 +0100
@@ -46,10 +46,10 @@
lemma BIT_eq: "u BIT b = v BIT c ==> u = v & b = c"
by (metis bin_rest_BIT bin_last_BIT)
-lemma BIT_B0_eq_Bit0 [simp]: "w BIT 0 = Int.Bit0 w"
+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
@@ -147,7 +147,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
+ unfolding bin_rl_char by (simp_all add: BIT_simps)
lemma bin_abs_lem:
"bin = (w BIT b) ==> ~ bin = Int.Min --> ~ bin = Int.Pls -->
@@ -183,11 +183,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]:
@@ -221,10 +221,10 @@
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"
@@ -236,14 +236,14 @@
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)
@@ -280,11 +280,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)
@@ -392,11 +392,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)"
@@ -433,11 +433,11 @@
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
@@ -453,11 +453,11 @@
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
@@ -506,12 +506,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
--- a/src/HOL/Word/Bool_List_Representation.thy Tue Dec 13 12:10:43 2011 +0100
+++ b/src/HOL/Word/Bool_List_Representation.thy Tue Dec 13 12:36:41 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
@@ -323,7 +323,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,7 +342,8 @@
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"
@@ -384,13 +386,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
@@ -688,10 +690,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 *)
@@ -754,7 +756,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 +766,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 +779,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 +865,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:
--- a/src/HOL/Word/Word.thy Tue Dec 13 12:10:43 2011 +0100
+++ b/src/HOL/Word/Word.thy Tue Dec 13 12:36:41 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