# HG changeset patch
# User huffman
# Date 1323674377 -3600
# Node ID 6a04efd99f256768275d26079db5e521b28e00aa
# Parent  a644ba1d7cf9d247a4a4db569410f57375b8d2f9
replace more uses of 'lemmas' with explicit 'lemma';
replace uses of 'simplified' attribute with 'unfolded';
remove unused intermediate lemmas.

diff -r a644ba1d7cf9 -r 6a04efd99f25 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Sun Dec 11 21:57:22 2011 +0100
+++ b/src/HOL/Word/Word.thy	Mon Dec 12 08:19:37 2011 +0100
@@ -140,7 +140,7 @@
 lemma 
   uint_0:"0 <= uint x" and 
   uint_lt: "uint (x::'a::len0 word) < 2 ^ len_of TYPE('a)"
-  by (auto simp: uint [simplified])
+  by (auto simp: uint [unfolded atLeastLessThan_iff])
 
 lemma uint_mod_same:
   "uint x mod 2 ^ len_of TYPE('a) = uint (x::'a::len0 word)"
@@ -169,7 +169,7 @@
 lemmas td_uint = word_uint.td_thm
 
 lemmas td_ext_ubin = td_ext_uint 
-  [simplified len_gt_0 no_bintr_alt1 [symmetric]]
+  [unfolded len_gt_0 no_bintr_alt1 [symmetric]]
 
 interpretation word_ubin:
   td_ext "uint::'a::len0 word \<Rightarrow> int" 
@@ -744,14 +744,14 @@
                   "{bl. length bl = len_of TYPE('a::len0)}"
   by (rule td_bl)
 
-lemmas word_bl_Rep' = word_bl.Rep [simplified, iff]
+lemmas word_bl_Rep' = word_bl.Rep [unfolded mem_Collect_eq, iff]
 
 lemma word_size_bl: "size w = size (to_bl w)"
   unfolding word_size by auto
 
 lemma to_bl_use_of_bl:
   "(to_bl w = bl) = (w = of_bl bl \<and> length bl = length (to_bl w))"
-  by (fastforce elim!: word_bl.Abs_inverse [simplified])
+  by (fastforce elim!: word_bl.Abs_inverse [unfolded mem_Collect_eq])
 
 lemma to_bl_word_rev: "to_bl (word_reverse w) = rev (to_bl w)"
   unfolding word_reverse_def by (simp add: word_bl.Abs_inverse)
@@ -1153,7 +1153,7 @@
   apply simp
   done
 
-lemmas size_0_same = size_0_same' [folded word_size]
+lemmas size_0_same = size_0_same' [unfolded word_size]
 
 lemmas unat_eq_0 = unat_0_iff
 lemmas unat_eq_zero = unat_0_iff
@@ -1222,7 +1222,8 @@
       simp add: pred_def succ_def add_commute mult_commute 
                 ring_distribs new_word_of_int_homs)+
 
-lemmas uint_cong = arg_cong [where f = uint]
+lemma uint_cong: "x = y \<Longrightarrow> uint x = uint y"
+  by simp
 
 lemmas uint_word_ariths = 
   word_arith_alts [THEN trans [OF uint_cong int_word_uint]]
@@ -1268,11 +1269,13 @@
   "0 <= (y :: 'a :: len0 word)"
   unfolding word_le_def by auto
   
-lemma word_m1_ge [simp] : "word_pred 0 >= y"
+lemma word_m1_ge [simp] : "word_pred 0 >= y" (* FIXME: delete *)
   unfolding word_le_def
   by (simp only : word_pred_0_n1 word_uint.eq_norm m1mod2k) auto
 
-lemmas word_n1_ge [simp]  = word_m1_ge [simplified word_sp_01]
+lemma word_n1_ge [simp]: "y \<le> (-1::'a::len0 word)"
+  unfolding word_le_def
+  by (simp only: word_m1_wi word_uint.eq_norm m1mod2k) auto
 
 lemmas word_not_simps [simp] = 
   word_zero_le [THEN leD] word_m1_ge [THEN leD] word_n1_ge [THEN leD]
@@ -1610,9 +1613,9 @@
   apply (rule uint_sub_ge)
   done
 
-lemmas udvd_incr_lem0 = udvd_incr_lem [where ua=0, simplified]
-lemmas udvd_incr0 = udvd_incr' [where ua=0, simplified]
-lemmas udvd_decr0 = udvd_decr' [where ua=0, simplified]
+lemmas udvd_incr_lem0 = udvd_incr_lem [where ua=0, unfolded add_0_left]
+lemmas udvd_incr0 = udvd_incr' [where ua=0, unfolded add_0_left]
+lemmas udvd_decr0 = udvd_decr' [where ua=0, unfolded add_0_left]
 
 lemma udvd_minus_le': 
   "xy < k \<Longrightarrow> z udvd xy \<Longrightarrow> z udvd k \<Longrightarrow> xy <= k - z"
@@ -1830,13 +1833,14 @@
   Abs_fnat_hom_1 word_arith_nat_div
   word_arith_nat_mod 
 
-lemmas unat_cong = arg_cong [where f = unat]
+lemma unat_cong: "x = y \<Longrightarrow> unat x = unat y"
+  by simp
   
 lemmas unat_word_ariths = word_arith_nat_defs
   [THEN trans [OF unat_cong unat_of_nat]]
 
 lemmas word_sub_less_iff = word_sub_le_iff
-  [simplified linorder_not_less [symmetric], simplified]
+  [unfolded linorder_not_less [symmetric] Not_eq_iff]
 
 lemma unat_add_lem: 
   "(unat x + unat y < 2 ^ len_of TYPE('a)) = 
@@ -2808,11 +2812,14 @@
    apply (auto simp add : shiftl1_rev)
   done
 
-lemmas rev_shiftl =
-  shiftl_rev [where w = "word_reverse w", simplified] for w
-
-lemmas shiftr_rev = rev_shiftl [THEN word_rev_gal']
-lemmas rev_shiftr = shiftl_rev [THEN word_rev_gal']
+lemma rev_shiftl: "word_reverse w << n = word_reverse (w >> n)"
+  by (simp add: shiftl_rev)
+
+lemma shiftr_rev: "w >> n = word_reverse (word_reverse w << n)"
+  by (simp add: rev_shiftl)
+
+lemma rev_shiftr: "word_reverse w >> n = word_reverse (w << n)"
+  by (simp add: shiftr_rev)
 
 lemma bl_sshiftr1:
   "to_bl (sshiftr1 (w :: 'a :: len word)) = hd (to_bl w) # butlast (to_bl w)"
@@ -3357,14 +3364,13 @@
 lemma ucast_slice: "ucast w = slice 0 w"
   unfolding slice_def by (simp add : ucast_slice1)
 
-lemmas slice_id = trans [OF ucast_slice [symmetric] ucast_id]
-
-lemma revcast_slice1': 
+lemma slice_id: "slice 0 t = t"
+  by (simp only: ucast_slice [symmetric] ucast_id)
+
+lemma revcast_slice1 [OF refl]: 
   "rc = revcast w \<Longrightarrow> slice1 (size rc) w = rc"
   unfolding slice1_def revcast_def' by (simp add : word_size)
 
-lemmas revcast_slice1 = refl [THEN revcast_slice1']
-
 lemma slice1_tf_tf': 
   "to_bl (slice1 n w :: 'a :: len0 word) = 
    rev (takefill False (len_of TYPE('a)) (rev (takefill False n (to_bl w))))"
@@ -3385,17 +3391,14 @@
   apply (simp add: word_bl.Abs_inverse)
   done
 
-lemma rev_slice': 
-  "res = slice n (word_reverse w) \<Longrightarrow> n + k + size res = size w \<Longrightarrow> 
-    res = word_reverse (slice k w)"
+lemma rev_slice:
+  "n + k + len_of TYPE('a::len0) = len_of TYPE('b::len0) \<Longrightarrow>
+    slice n (word_reverse (w::'b word)) = word_reverse (slice k w::'a word)"
   apply (unfold slice_def word_size)
-  apply clarify
   apply (rule rev_slice1)
   apply arith
   done
 
-lemmas rev_slice = refl [THEN rev_slice', unfolded word_size]
-
 lemmas sym_notr = 
   not_iff [THEN iffD2, THEN not_sym, THEN not_iff [THEN iffD1]]
 
@@ -3607,14 +3610,13 @@
    apply (rule word_eqI, clarsimp simp: nth_slice word_size)+
   done
 
-lemma slice_cat1':
+lemma slice_cat1 [OF refl]:
   "wc = word_cat a b \<Longrightarrow> size wc >= size a + size b \<Longrightarrow> slice (size b) wc = a"
   apply safe
   apply (rule word_eqI)
   apply (simp add: nth_slice test_bit_cat word_size)
   done
 
-lemmas slice_cat1 = refl [THEN slice_cat1']
 lemmas slice_cat2 = trans [OF slice_id word_cat_id]
 
 lemma cat_slices:
@@ -3688,11 +3690,10 @@
 
 lemmas td_gal_lt_len = len_gt_0 [THEN td_gal_lt]
 
-lemma nth_rcat_lem' [rule_format] :
-  "sw = size (hd wl  :: 'a :: len word) \<Longrightarrow> (ALL n. n < size wl * sw --> 
-    rev (concat (map to_bl wl)) ! n = 
-    rev (to_bl (rev wl ! (n div sw))) ! (n mod sw))"
-  apply (unfold word_size)
+lemma nth_rcat_lem:
+  "n < length (wl::'a word list) * len_of TYPE('a::len) \<Longrightarrow>
+    rev (concat (map to_bl wl)) ! n =
+    rev (to_bl (rev wl ! (n div len_of TYPE('a)))) ! (n mod len_of TYPE('a))"
   apply (induct "wl")
    apply clarsimp
   apply (clarsimp simp add : nth_append size_rcat_lem)
@@ -3701,8 +3702,6 @@
   apply clarsimp
   done
 
-lemmas nth_rcat_lem = refl [THEN nth_rcat_lem', unfolded word_size]
-
 lemma test_bit_rcat:
   "sw = size (hd wl :: 'a :: len word) \<Longrightarrow> rc = word_rcat wl \<Longrightarrow> rc !! n = 
     (n < size rc & n div sw < size wl & (rev wl) ! (n div sw) !! (n mod sw))"
@@ -3714,9 +3713,9 @@
     test_bit_bl word_size td_gal_lt_len [THEN iffD2, THEN nth_rcat_lem])
   done
 
-lemma foldl_eq_foldr [rule_format] :
-  "ALL x. foldl op + x xs = foldr op + (x # xs) (0 :: 'a :: comm_monoid_add)" 
-  by (induct xs) (auto simp add : add_assoc)
+lemma foldl_eq_foldr:
+  "foldl op + x xs = foldr op + (x # xs) (0 :: 'a :: comm_monoid_add)" 
+  by (induct xs arbitrary: x) (auto simp add : add_assoc)
 
 lemmas test_bit_cong = arg_cong [where f = "test_bit", THEN fun_cong]
 
@@ -3725,15 +3724,13 @@
   test_bit_rsplit [OF refl asm_rl diff_Suc_less]]
 
 -- "lazy way of expressing that u and v, and su and sv, have same types"
-lemma word_rsplit_len_indep':
+lemma word_rsplit_len_indep [OF refl refl refl refl]:
   "[u,v] = p \<Longrightarrow> [su,sv] = q \<Longrightarrow> word_rsplit u = su \<Longrightarrow> 
     word_rsplit v = sv \<Longrightarrow> length su = length sv"
   apply (unfold word_rsplit_def)
   apply (auto simp add : bin_rsplit_len_indep)
   done
 
-lemmas word_rsplit_len_indep = word_rsplit_len_indep' [OF refl refl refl refl]
-
 lemma length_word_rsplit_size: 
   "n = len_of TYPE ('a :: len) \<Longrightarrow> 
     (length (word_rsplit w :: 'a word list) <= m) = (size w <= m * n)"
@@ -3744,7 +3741,7 @@
 lemmas length_word_rsplit_lt_size = 
   length_word_rsplit_size [unfolded Not_eq_iff linorder_not_less [symmetric]]
 
-lemma length_word_rsplit_exp_size: 
+lemma length_word_rsplit_exp_size:
   "n = len_of TYPE ('a :: len) \<Longrightarrow> 
     length (word_rsplit w :: 'a word list) = (size w + n - 1) div n"
   unfolding word_rsplit_def by (clarsimp simp add : word_size bin_rsplit_len)
@@ -3770,24 +3767,21 @@
    apply (erule xtr7, rule len_gt_0 [THEN dtle])+
   done
 
-lemma size_word_rsplit_rcat_size':
-  "word_rcat (ws :: 'a :: len word list) = frcw \<Longrightarrow> 
-    size frcw = length ws * len_of TYPE ('a) \<Longrightarrow> 
-    size (hd [word_rsplit frcw, ws]) = size ws" 
+lemma size_word_rsplit_rcat_size:
+  "\<lbrakk>word_rcat (ws::'a::len word list) = (frcw::'b::len0 word);
+     size frcw = length ws * len_of TYPE('a)\<rbrakk>
+    \<Longrightarrow> length (word_rsplit frcw::'a word list) = length ws"
   apply (clarsimp simp add : word_size length_word_rsplit_exp_size')
   apply (fast intro: given_quot_alt)
   done
 
-lemmas size_word_rsplit_rcat_size = 
-  size_word_rsplit_rcat_size' [simplified]
-
 lemma msrevs:
   fixes n::nat
   shows "0 < n \<Longrightarrow> (k * n + m) div n = m div n + k"
   and   "(k * n + m) mod n = m mod n"
   by (auto simp: add_commute)
 
-lemma word_rsplit_rcat_size':
+lemma word_rsplit_rcat_size [OF refl]:
   "word_rcat (ws :: 'a :: len word list) = frcw \<Longrightarrow> 
     size frcw = length ws * len_of TYPE ('a) \<Longrightarrow> word_rsplit frcw = ws" 
   apply (frule size_word_rsplit_rcat_size, assumption)
@@ -3811,8 +3805,6 @@
    apply simp_all
   done
 
-lemmas word_rsplit_rcat_size = refl [THEN word_rsplit_rcat_size']
-
 
 subsection "Rotation"
 
@@ -3860,7 +3852,8 @@
 lemma rotater_rev': "rotater n (rev xs) = rev (rotate n xs)"
   unfolding rotater_def by (induct n) (auto intro: rotater1_rev')
 
-lemmas rotater_rev = rotater_rev' [where xs = "rev ys", simplified] for ys
+lemma rotater_rev: "rotater n ys = rev (rotate n (rev ys))"
+  using rotater_rev' [where xs = "rev ys"] by simp
 
 lemma rotater_drop_take: 
   "rotater n xs =