--- a/src/HOL/Word/Misc_Typedef.thy Thu Nov 17 21:31:29 2011 +0100
+++ b/src/HOL/Word/Misc_Typedef.thy Thu Nov 17 21:58:10 2011 +0100
@@ -25,9 +25,7 @@
context type_definition
begin
-lemmas Rep' [iff] = Rep [simplified] (* if A is given as Collect .. *)
-
-declare Rep_inverse [simp] Rep_inject [simp]
+declare Rep [iff] Rep_inverse [simp] Rep_inject [simp]
lemma Abs_eqD: "Abs x = Abs y ==> x \<in> A ==> y \<in> A ==> x = y"
by (simp add: Abs_inject)
@@ -38,7 +36,7 @@
lemma Rep_comp_inverse:
"Rep o f = g ==> Abs o g = f"
- using Rep_inverse by (auto intro: ext)
+ using Rep_inverse by auto
lemma Rep_eqD [elim!]: "Rep x = Rep y ==> x = y"
by simp
@@ -48,7 +46,7 @@
lemma comp_Abs_inverse:
"f o Abs = g ==> g o Rep = f"
- using Rep_inverse by (auto intro: ext)
+ using Rep_inverse by auto
lemma set_Rep:
"A = range Rep"
@@ -84,7 +82,7 @@
lemma fns4:
"Rep o fa o Abs = fr ==>
Rep o fa = fr o Rep & fa o Abs = Abs o fr"
- by (auto intro!: ext)
+ by auto
end
@@ -133,7 +131,7 @@
by (drule comp_Abs_inverse [symmetric]) simp
lemma eq_norm': "Rep o Abs = norm"
- by (auto simp: eq_norm intro!: ext)
+ by (auto simp: eq_norm)
lemma norm_Rep [simp]: "norm (Rep x) = Rep x"
by (auto simp: eq_norm' intro: td_th)
@@ -165,7 +163,7 @@
lemma fns5:
"Rep o fa o Abs = fr ==>
fr o norm = fr & norm o fr = fr"
- by (fold eq_norm') (auto intro!: ext)
+ by (fold eq_norm') auto
(* following give conditions for converses to td_fns1
the condition (norm o fr o norm = fr o norm) says that
--- a/src/HOL/Word/Word.thy Thu Nov 17 21:31:29 2011 +0100
+++ b/src/HOL/Word/Word.thy Thu Nov 17 21:58:10 2011 +0100
@@ -650,6 +650,8 @@
"{bl. length bl = len_of TYPE('a::len0)}"
by (rule td_bl)
+lemmas word_bl_Rep' = word_bl.Rep [simplified, iff]
+
lemma word_size_bl: "size w = size (to_bl w)"
unfolding word_size by auto
@@ -668,7 +670,7 @@
lemmas word_rev_gal' = sym [THEN word_rev_gal, symmetric, standard]
-lemmas length_bl_gt_0 [iff] = xtr1 [OF word_bl.Rep' len_gt_0, standard]
+lemmas length_bl_gt_0 [iff] = xtr1 [OF word_bl_Rep' len_gt_0, standard]
lemmas bl_not_Nil [iff] =
length_bl_gt_0 [THEN length_greater_0_conv [THEN iffD1], standard]
lemmas length_bl_neq_0 [iff] = length_bl_gt_0 [THEN gr_implies_not0]
@@ -818,7 +820,7 @@
unfolding of_bl_def uint_bl
by (clarsimp simp add: bl_bin_bl_rtf word_ubin.eq_norm word_size)
-lemmas word_rev_tf = refl [THEN word_rev_tf', unfolded word_bl.Rep', standard]
+lemmas word_rev_tf = refl [THEN word_rev_tf', unfolded word_bl_Rep', standard]
lemmas word_rep_drop = word_rev_tf [simplified takefill_alt,
simplified, simplified rev_take, simplified]
@@ -2545,9 +2547,6 @@
"(\<lambda>h i. h i \<and> i < len_of TYPE('a::len0))"
by (rule td_ext_nth)
-declare test_bit.Rep' [simp del]
-declare test_bit.Rep' [rule del]
-
lemmas td_nth = test_bit.td_thm
lemma word_set_set_same:
@@ -3096,7 +3095,7 @@
lemmas shiftr_bl_of = refl [THEN shiftr_bl_of', unfolded word_size]
-lemmas shiftr_bl = word_bl.Rep' [THEN eq_imp_le, THEN shiftr_bl_of,
+lemmas shiftr_bl = word_bl_Rep' [THEN eq_imp_le, THEN shiftr_bl_of,
simplified word_size, simplified, THEN eq_reflection, standard]
lemma msb_shift': "msb (w::'a::len word) <-> (w >> (size w - 1)) ~= 0"
@@ -4126,7 +4125,7 @@
lemmas blrs0 = rotate_eqs [THEN to_bl_rotl [THEN trans]]
lemmas word_rotl_eqs =
- blrs0 [simplified word_bl.Rep' word_bl.Rep_inject to_bl_rotl [symmetric]]
+ blrs0 [simplified word_bl_Rep' word_bl.Rep_inject to_bl_rotl [symmetric]]
lemma to_bl_rotr:
"to_bl (word_rotr n w) = rotater n (to_bl w)"
@@ -4135,7 +4134,7 @@
lemmas brrs0 = rotater_eqs [THEN to_bl_rotr [THEN trans]]
lemmas word_rotr_eqs =
- brrs0 [simplified word_bl.Rep' word_bl.Rep_inject to_bl_rotr [symmetric]]
+ brrs0 [simplified word_bl_Rep' word_bl.Rep_inject to_bl_rotr [symmetric]]
declare word_rotr_eqs (1) [simp]
declare word_rotl_eqs (1) [simp]
@@ -4228,7 +4227,7 @@
lemmas blwl_syms [symmetric] = bl_word_not bl_word_and bl_word_or bl_word_xor
-lemmas lbl_lbl = trans [OF word_bl.Rep' word_bl.Rep' [symmetric]]
+lemmas lbl_lbl = trans [OF word_bl_Rep' word_bl_Rep' [symmetric]]
lemmas ths_map2 [OF lbl_lbl] = rotate_map2 rotater_map2
@@ -4255,10 +4254,10 @@
lemmas word_rot_logs = word_rotate.word_rot_logs
lemmas bl_word_rotl_dt = trans [OF to_bl_rotl rotate_drop_take,
- simplified word_bl.Rep', standard]
+ simplified word_bl_Rep', standard]
lemmas bl_word_rotr_dt = trans [OF to_bl_rotr rotater_drop_take,
- simplified word_bl.Rep', standard]
+ simplified word_bl_Rep', standard]
lemma bl_word_roti_dt':
"n = nat ((- i) mod int (size (w :: 'a :: len word))) \<Longrightarrow>