--- 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)