# HG changeset patch
# User huffman
# Date 1324985226 -3600
# Node ID 13392893ea121d1ecf61597669b5f71f42b72383
# Parent  e69d631fe9af41ba2817ee9dad103d65d5d1e628
use 'induct arbitrary' instead of 'rule_format' attribute

diff -r e69d631fe9af -r 13392893ea12 src/HOL/Word/Bool_List_Representation.thy
--- a/src/HOL/Word/Bool_List_Representation.thy	Tue Dec 27 12:05:03 2011 +0100
+++ b/src/HOL/Word/Bool_List_Representation.thy	Tue Dec 27 12:27:06 2011 +0100
@@ -190,9 +190,9 @@
 lemma bin_to_bl_Pls: "bin_to_bl n Int.Pls = replicate n False"
   unfolding bin_to_bl_def by (simp add : bin_to_bl_Pls_aux)
 
-lemma bin_to_bl_Min_aux [rule_format] : 
-  "ALL bl. bin_to_bl_aux n Int.Min bl = replicate n True @ bl"
-  by (induct n) (auto simp: replicate_app_Cons_same)
+lemma bin_to_bl_Min_aux:
+  "bin_to_bl_aux n Int.Min bl = replicate n True @ bl"
+  by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same)
 
 lemma bin_to_bl_Min: "bin_to_bl n Int.Min = replicate n True"
   unfolding bin_to_bl_def by (simp add : bin_to_bl_Min_aux)
@@ -207,10 +207,10 @@
   "n <= m ==> bin_to_bl n (bintrunc m w) = bin_to_bl n w"
   by (auto intro: bl_to_bin_inj)
 
-lemma bin_to_bl_aux_bintr [rule_format] :
-  "ALL m bin bl. bin_to_bl_aux n (bintrunc m bin) bl = 
+lemma bin_to_bl_aux_bintr:
+  "bin_to_bl_aux n (bintrunc m bin) bl = 
     replicate (n - m) False @ bin_to_bl_aux (min n m) bin bl"
-  apply (induct n)
+  apply (induct n arbitrary: m bin bl)
    apply clarsimp
   apply clarsimp
   apply (case_tac "m")
@@ -256,13 +256,13 @@
   "hd (bin_to_bl (Suc n) w) = (bin_sign (sbintrunc n w) = Int.Min)"
   unfolding bin_to_bl_def by (rule bl_sbin_sign_aux)
 
-lemma bin_nth_of_bl_aux [rule_format]: 
-  "\<forall>w. bin_nth (bl_to_bin_aux bl w) n = 
+lemma bin_nth_of_bl_aux:
+  "bin_nth (bl_to_bin_aux bl w) n = 
     (n < size bl & rev bl ! n | n >= length bl & bin_nth w (n - size bl))"
-  apply (induct_tac bl)
+  apply (induct bl arbitrary: w)
    apply clarsimp
   apply clarsimp
-  apply (cut_tac x=n and y="size list" in linorder_less_linear)
+  apply (cut_tac x=n and y="size bl" in linorder_less_linear)
   apply (erule disjE, simp add: nth_append)+
   apply auto
   done
@@ -270,9 +270,8 @@
 lemma bin_nth_of_bl: "bin_nth (bl_to_bin bl) n = (n < length bl & rev bl ! n)"
   unfolding bl_to_bin_def by (simp add : bin_nth_of_bl_aux)
 
-lemma bin_nth_bl [rule_format] : "ALL m w. n < m --> 
-    bin_nth w n = nth (rev (bin_to_bl m w)) n"
-  apply (induct n)
+lemma bin_nth_bl: "n < m \<Longrightarrow> bin_nth w n = nth (rev (bin_to_bl m w)) n"
+  apply (induct n arbitrary: m w)
    apply clarsimp
    apply (case_tac m, clarsimp)
    apply (clarsimp simp: bin_to_bl_def)
@@ -283,38 +282,38 @@
   apply (simp add: bin_to_bl_aux_alt)
   done
 
-lemma nth_rev [rule_format] : 
-  "n < length xs --> rev xs ! n = xs ! (length xs - 1 - n)"
-  apply (induct_tac "xs")
+lemma nth_rev:
+  "n < length xs \<Longrightarrow> rev xs ! n = xs ! (length xs - 1 - n)"
+  apply (induct xs)
    apply simp
   apply (clarsimp simp add : nth_append nth.simps split add : nat.split)
-  apply (rule_tac f = "%n. list ! n" in arg_cong) 
+  apply (rule_tac f = "\<lambda>n. xs ! n" in arg_cong)
   apply arith
   done
 
 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 = 
+lemma nth_bin_to_bl_aux:
+  "n < m + length bl \<Longrightarrow> (bin_to_bl_aux m w bl) ! n = 
     (if n < m then bin_nth w (m - 1 - n) else bl ! (n - m))"
-  apply (induct m)
+  apply (induct m arbitrary: w n bl)
    apply clarsimp
   apply clarsimp
   apply (case_tac w rule: bin_exhaust)
   apply simp
   done
-  
+
 lemma nth_bin_to_bl: "n < m ==> (bin_to_bl m w) ! n = bin_nth w (m - Suc n)"
   unfolding bin_to_bl_def by (simp add : nth_bin_to_bl_aux)
 
-lemma bl_to_bin_lt2p_aux [rule_format]: 
-  "\<forall>w. bl_to_bin_aux bs w < (w + 1) * (2 ^ length bs)"
-  apply (induct bs)
+lemma bl_to_bin_lt2p_aux:
+  "bl_to_bin_aux bs w < (w + 1) * (2 ^ length bs)"
+  apply (induct bs arbitrary: w)
    apply clarsimp
   apply clarsimp
   apply safe
-  apply (erule allE, erule xtr8 [rotated],
+  apply (drule meta_spec, erule xtr8 [rotated],
          simp add: numeral_simps algebra_simps BIT_simps
          cong add: number_of_False_cong)+
   done
@@ -327,13 +326,13 @@
   apply simp
   done
 
-lemma bl_to_bin_ge2p_aux [rule_format] : 
-  "\<forall>w. bl_to_bin_aux bs w >= w * (2 ^ length bs)"
-  apply (induct bs)
+lemma bl_to_bin_ge2p_aux:
+  "bl_to_bin_aux bs w >= w * (2 ^ length bs)"
+  apply (induct bs arbitrary: w)
    apply clarsimp
   apply clarsimp
   apply safe
-   apply (erule allE, erule preorder_class.order_trans [rotated],
+   apply (drule meta_spec, erule preorder_class.order_trans [rotated],
           simp add: numeral_simps algebra_simps BIT_simps
           cong add: number_of_False_cong)+
   done
@@ -370,24 +369,24 @@
    apply (auto simp add: butlast_rest_bl2bin_aux)
   done
 
-lemma trunc_bl2bin_aux [rule_format]: 
-  "ALL w. bintrunc m (bl_to_bin_aux bl w) = 
+lemma trunc_bl2bin_aux:
+  "bintrunc m (bl_to_bin_aux bl w) = 
     bl_to_bin_aux (drop (length bl - m) bl) (bintrunc (m - length bl) w)"
-  apply (induct_tac bl)
+  apply (induct bl arbitrary: w)
    apply clarsimp
   apply clarsimp
   apply safe
-   apply (case_tac "m - size list")
+   apply (case_tac "m - size bl")
     apply (simp add : diff_is_0_eq [THEN iffD1, THEN Suc_diff_le])
    apply (simp add: BIT_simps)
-   apply (rule_tac f = "%nat. bl_to_bin_aux list (Int.Bit1 (bintrunc nat w))" 
-                   in arg_cong) 
+   apply (rule_tac f = "%nat. bl_to_bin_aux bl (Int.Bit1 (bintrunc nat w))" 
+                   in arg_cong)
    apply simp
-  apply (case_tac "m - size list")
+  apply (case_tac "m - size bl")
    apply (simp add: diff_is_0_eq [THEN iffD1, THEN Suc_diff_le])
   apply (simp add: BIT_simps)
-  apply (rule_tac f = "%nat. bl_to_bin_aux list (Int.Bit0 (bintrunc nat w))" 
-                  in arg_cong) 
+  apply (rule_tac f = "%nat. bl_to_bin_aux bl (Int.Bit0 (bintrunc nat w))" 
+                  in arg_cong)
   apply simp
   done
 
@@ -408,9 +407,9 @@
    apply auto
   done
 
-lemma nth_rest_power_bin [rule_format] :
-  "ALL n. bin_nth ((bin_rest ^^ k) w) n = bin_nth w (n + k)"
-  apply (induct k, clarsimp)
+lemma nth_rest_power_bin:
+  "bin_nth ((bin_rest ^^ k) w) n = bin_nth w (n + k)"
+  apply (induct k arbitrary: n, clarsimp)
   apply clarsimp
   apply (simp only: bin_nth.Suc [symmetric] add_Suc)
   done
@@ -442,11 +441,22 @@
 
 (** links between bit-wise operations and operations on bool lists **)
     
-lemma bl_xor_aux_bin [rule_format] : "ALL v w bs cs. 
-    map2 (%x y. x ~= y) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) = 
+lemma bl_xor_aux_bin:
+  "map2 (%x y. x ~= y) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) = 
     bin_to_bl_aux n (v XOR w) (map2 (%x y. x ~= y) bs cs)"
-  apply (induct_tac n)
-   apply safe
+  apply (induct n arbitrary: v w bs cs)
+   apply simp
+  apply (case_tac v rule: bin_exhaust)
+  apply (case_tac w rule: bin_exhaust)
+  apply clarsimp
+  apply (case_tac b)
+  apply (case_tac ba, safe, simp_all)+
+  done
+
+lemma bl_or_aux_bin:
+  "map2 (op | ) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) = 
+    bin_to_bl_aux n (v OR w) (map2 (op | ) bs cs)"
+  apply (induct n arbitrary: v w bs cs)
    apply simp
   apply (case_tac v rule: bin_exhaust)
   apply (case_tac w rule: bin_exhaust)
@@ -455,34 +465,20 @@
   apply (case_tac ba, safe, simp_all)+
   done
     
-lemma bl_or_aux_bin [rule_format] : "ALL v w bs cs. 
-    map2 (op | ) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) = 
-    bin_to_bl_aux n (v OR w) (map2 (op | ) bs cs)" 
-  apply (induct_tac n)
-   apply safe
-   apply simp
-  apply (case_tac v rule: bin_exhaust)
-  apply (case_tac w rule: bin_exhaust)
-  apply clarsimp
-  apply (case_tac b)
-  apply (case_tac ba, safe, simp_all)+
-  done
-    
-lemma bl_and_aux_bin [rule_format] : "ALL v w bs cs. 
-    map2 (op & ) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) = 
+lemma bl_and_aux_bin:
+  "map2 (op & ) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) = 
     bin_to_bl_aux n (v AND w) (map2 (op & ) bs cs)" 
-  apply (induct_tac n)
-   apply safe
+  apply (induct n arbitrary: v w bs cs)
    apply simp
   apply (case_tac v rule: bin_exhaust)
   apply (case_tac w rule: bin_exhaust)
   apply clarsimp
   done
     
-lemma bl_not_aux_bin [rule_format] : 
-  "ALL w cs. map Not (bin_to_bl_aux n w cs) = 
+lemma bl_not_aux_bin:
+  "map Not (bin_to_bl_aux n w cs) = 
     bin_to_bl_aux n (NOT w) (map Not cs)"
-  apply (induct n)
+  apply (induct n arbitrary: w cs)
    apply clarsimp
   apply clarsimp
   done
@@ -502,10 +498,10 @@
   "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) = 
+lemma drop_bin2bl_aux:
+  "drop m (bin_to_bl_aux n bin bs) = 
     bin_to_bl_aux (n - m) bin (drop (m - n) bs)"
-  apply (induct n, clarsimp)
+  apply (induct n arbitrary: m bin bs, clarsimp)
   apply clarsimp
   apply (case_tac bin rule: bin_exhaust)
   apply (case_tac "m <= n", simp)
@@ -518,28 +514,27 @@
 lemma drop_bin2bl: "drop m (bin_to_bl n bin) = bin_to_bl (n - m) bin"
   unfolding bin_to_bl_def by (simp add : drop_bin2bl_aux)
 
-lemma take_bin2bl_lem1 [rule_format] : 
-  "ALL w bs. take m (bin_to_bl_aux m w bs) = bin_to_bl m w"
-  apply (induct m, clarsimp)
+lemma take_bin2bl_lem1:
+  "take m (bin_to_bl_aux m w bs) = bin_to_bl m w"
+  apply (induct m arbitrary: w bs, clarsimp)
   apply clarsimp
   apply (simp add: bin_to_bl_aux_alt)
   apply (simp add: bin_to_bl_def)
   apply (simp add: bin_to_bl_aux_alt)
   done
 
-lemma take_bin2bl_lem [rule_format] : 
-  "ALL w bs. take m (bin_to_bl_aux (m + n) w bs) = 
+lemma take_bin2bl_lem:
+  "take m (bin_to_bl_aux (m + n) w bs) = 
     take m (bin_to_bl (m + n) w)"
-  apply (induct n)
-   apply clarify
+  apply (induct n arbitrary: w bs)
    apply (simp_all (no_asm) add: bin_to_bl_def take_bin2bl_lem1)
   apply simp
   done
 
-lemma bin_split_take [rule_format] : 
-  "ALL b c. bin_split n c = (a, b) --> 
+lemma bin_split_take:
+  "bin_split n c = (a, b) \<Longrightarrow>
     bin_to_bl m a = take m (bin_to_bl (m + n) c)"
-  apply (induct n)
+  apply (induct n arbitrary: b c)
    apply clarsimp
   apply (clarsimp simp: Let_def split: ls_splits)
   apply (simp add: bin_to_bl_def)
@@ -551,29 +546,26 @@
     bin_to_bl m a = take m (bin_to_bl k c)"
   by (auto elim: bin_split_take)
   
-lemma nth_takefill [rule_format] : "ALL m l. m < n --> 
+lemma nth_takefill: "m < n \<Longrightarrow>
     takefill fill n l ! m = (if m < length l then l ! m else fill)"
-  apply (induct n, clarsimp)
+  apply (induct n arbitrary: m l, clarsimp)
   apply clarsimp
   apply (case_tac m)
    apply (simp split: list.split)
-  apply clarsimp
-  apply (erule allE)+
-  apply (erule (1) impE)
   apply (simp split: list.split)
   done
 
-lemma takefill_alt [rule_format] :
-  "ALL l. takefill fill n l = take n l @ replicate (n - length l) fill"
-  by (induct n) (auto split: list.split)
+lemma takefill_alt:
+  "takefill fill n l = take n l @ replicate (n - length l) fill"
+  by (induct n arbitrary: l) (auto split: list.split)
 
 lemma takefill_replicate [simp]:
   "takefill fill n (replicate m fill) = replicate n fill"
   by (simp add : takefill_alt replicate_add [symmetric])
 
-lemma takefill_le' [rule_format] :
-  "ALL l n. n = m + k --> takefill x m (takefill x n l) = takefill x m l"
-  by (induct m) (auto split: list.split)
+lemma takefill_le':
+  "n = m + k \<Longrightarrow> takefill x m (takefill x n l) = takefill x m l"
+  by (induct m arbitrary: l n) (auto split: list.split)
 
 lemma length_takefill [simp]: "length (takefill fill n l) = n"
   by (simp add : takefill_alt)
@@ -716,9 +708,9 @@
   "(!!k. k < n ==> f k = g k) ==> bl_of_nth n f = bl_of_nth n g"
   by (induct n)  auto
 
-lemma bl_of_nth_nth_le [rule_format] : "ALL xs. 
-    length xs >= n --> bl_of_nth n (nth (rev xs)) = drop (length xs - n) xs"
-  apply (induct n, clarsimp)
+lemma bl_of_nth_nth_le:
+  "n \<le> length xs \<Longrightarrow> bl_of_nth n (nth (rev xs)) = drop (length xs - n) xs"
+  apply (induct n arbitrary: xs, clarsimp)
   apply clarsimp
   apply (rule trans [OF _ hd_Cons_tl])
    apply (frule Suc_le_lessD)
@@ -946,17 +938,16 @@
   "size (concat (map (bin_to_bl n) xs)) = length xs * n"
   by (induct xs) auto
 
-lemma bin_cat_foldl_lem [rule_format] :
-  "ALL x. foldl (%u. bin_cat u n) x xs = 
+lemma bin_cat_foldl_lem:
+  "foldl (%u. bin_cat u n) x xs = 
     bin_cat x (size xs * n) (foldl (%u. bin_cat u n) y xs)"
-  apply (induct xs)
+  apply (induct xs arbitrary: x)
    apply simp
-  apply clarify
   apply (simp (no_asm))
   apply (frule asm_rl)
-  apply (drule spec)
+  apply (drule meta_spec)
   apply (erule trans)
-  apply (drule_tac x = "bin_cat y n a" in spec)
+  apply (drule_tac x = "bin_cat y n a" in meta_spec)
   apply (simp add : bin_cat_assoc_sym min_max.inf_absorb2)
   done
 
@@ -1042,15 +1033,14 @@
 lemmas bthrs = bin_rsplit_simp_alt [THEN [2] trans]
 
 lemma bin_rsplit_size_sign' [rule_format] : 
-  "n > 0 ==> (ALL nw w. rev sw = bin_rsplit n (nw, w) --> 
-    (ALL v: set sw. bintrunc n v = v))"
-  apply (induct sw)
+  "\<lbrakk>n > 0; rev sw = bin_rsplit n (nw, w)\<rbrakk> \<Longrightarrow> 
+    (ALL v: set sw. bintrunc n v = v)"
+  apply (induct sw arbitrary: nw w v)
    apply clarsimp
   apply clarsimp
   apply (drule bthrs)
   apply (simp (no_asm_use) add: Let_def split: ls_splits)
   apply clarify
-  apply (erule impE, rule exI, erule exI)
   apply (drule split_bintrunc)
   apply simp
   done
@@ -1123,8 +1113,8 @@
   "n \<noteq> 0 --> ws = bin_rsplit n (nw, w) --> (length ws <= m) = (nw <= m * n)"
   unfolding bin_rsplit_def by (clarsimp simp add : bin_rsplit_aux_len_le)
  
-lemma bin_rsplit_aux_len [rule_format] :
-  "n\<noteq>0 --> length (bin_rsplit_aux n nw w cs) = 
+lemma bin_rsplit_aux_len:
+  "n \<noteq> 0 \<Longrightarrow> length (bin_rsplit_aux n nw w cs) =
     (nw + n - 1) div n + length cs"
   apply (induct n nw w cs rule: bin_rsplit_aux.induct)
   apply (subst bin_rsplit_aux.simps)