# HG changeset patch
# User wenzelm
# Date 1321563490 -3600
# Node ID 1fffa81b9b83af43af217312270697b180dac63c
# Parent  8e3e004f1c318f7e4cc58f7bb2f8f694e58dc6f7
eliminated slightly odd Rep' with dynamically-scoped [simplified];
tuned proofs;

diff -r 8e3e004f1c31 -r 1fffa81b9b83 src/HOL/Word/Misc_Typedef.thy
--- 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 
diff -r 8e3e004f1c31 -r 1fffa81b9b83 src/HOL/Word/Word.thy
--- 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>