--- a/src/HOL/Word/Bit_Int.thy Tue Dec 27 09:45:10 2011 +0100
+++ b/src/HOL/Word/Bit_Int.thy Tue Dec 27 15:38:45 2011 +0100
@@ -471,11 +471,7 @@
subsection {* Splitting and concatenation *}
definition bin_rcat :: "nat \<Rightarrow> int list \<Rightarrow> int" where
- "bin_rcat n = foldl (%u v. bin_cat u n v) Int.Pls"
-
-lemma [code]:
"bin_rcat n = foldl (\<lambda>u v. bin_cat u n v) 0"
- by (simp add: bin_rcat_def Pls_def)
fun bin_rsplit_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" where
"bin_rsplit_aux n m c bs =
@@ -536,7 +532,7 @@
done
lemma bin_cat_zero [simp]: "bin_cat 0 n w = bintrunc n w"
- by (induct n arbitrary: w) (auto simp: Int.Pls_def)
+ by (induct n arbitrary: w) auto
lemma bin_cat_Pls [simp]: "bin_cat Int.Pls n w = bintrunc n w"
unfolding Pls_def by (rule bin_cat_zero)
@@ -570,7 +566,7 @@
by (induct n arbitrary: w) auto
lemma bin_split_zero [simp]: "bin_split n 0 = (0, 0)"
- by (induct n) (auto simp: Int.Pls_def)
+ by (induct n) auto
lemma bin_split_Pls [simp]:
"bin_split n Int.Pls = (Int.Pls, Int.Pls)"
@@ -586,7 +582,7 @@
apply (induct n arbitrary: m b c, clarsimp)
apply (simp add: bin_rest_trunc Let_def split: ls_splits)
apply (case_tac m)
- apply (auto simp: Let_def BIT_simps split: ls_splits)
+ apply (auto simp: Let_def split: ls_splits)
done
lemma bin_split_trunc1:
@@ -595,13 +591,13 @@
apply (induct n arbitrary: m b c, clarsimp)
apply (simp add: bin_rest_trunc Let_def split: ls_splits)
apply (case_tac m)
- apply (auto simp: Let_def BIT_simps split: ls_splits)
+ apply (auto simp: Let_def split: ls_splits)
done
lemma bin_cat_num:
"bin_cat a n b = a * 2 ^ n + bintrunc n b"
apply (induct n arbitrary: b, clarsimp)
- apply (simp add: Bit_def cong: number_of_False_cong)
+ apply (simp add: Bit_def)
done
lemma bin_split_num:
--- a/src/HOL/Word/Bit_Representation.thy Tue Dec 27 09:45:10 2011 +0100
+++ b/src/HOL/Word/Bit_Representation.thy Tue Dec 27 15:38:45 2011 +0100
@@ -326,28 +326,19 @@
by (cases w rule: bin_exhaust) auto
primrec bintrunc :: "nat \<Rightarrow> int \<Rightarrow> int" where
- Z : "bintrunc 0 bin = Int.Pls"
+ Z : "bintrunc 0 bin = 0"
| Suc : "bintrunc (Suc n) bin = bintrunc n (bin_rest bin) BIT (bin_last bin)"
primrec sbintrunc :: "nat => int => int" where
- Z : "sbintrunc 0 bin =
- (case bin_last bin of (1::bit) => Int.Min | (0::bit) => Int.Pls)"
+ Z : "sbintrunc 0 bin = (case bin_last bin of (1::bit) \<Rightarrow> -1 | (0::bit) \<Rightarrow> 0)"
| Suc : "sbintrunc (Suc n) bin = sbintrunc n (bin_rest bin) BIT (bin_last bin)"
-lemma [code]:
- "sbintrunc 0 bin =
- (case bin_last bin of (1::bit) => - 1 | (0::bit) => 0)"
- "sbintrunc (Suc n) bin = sbintrunc n (bin_rest bin) BIT (bin_last bin)"
- apply simp_all
- apply (simp only: Pls_def Min_def)
- done
-
-lemma sign_bintr: "bin_sign (bintrunc n w) = Int.Pls"
+lemma sign_bintr: "bin_sign (bintrunc n w) = 0"
by (induct n arbitrary: w) auto
lemma bintrunc_mod2p: "bintrunc n w = (w mod 2 ^ n)"
apply (induct n arbitrary: w)
- apply (simp add: Pls_def)
+ apply simp
apply (simp add: bin_last_def bin_rest_def Bit_def zmod_zmult2_eq)
done
@@ -356,10 +347,8 @@
apply clarsimp
apply (subst mod_add_left_eq)
apply (simp add: bin_last_def)
- apply (simp add: number_of_eq)
- apply (simp add: Pls_def)
- apply (simp add: bin_last_def bin_rest_def Bit_def
- cong: number_of_False_cong)
+ apply simp
+ apply (simp add: bin_last_def bin_rest_def Bit_def)
apply (clarsimp simp: mod_mult_mult1 [symmetric]
zmod_zdiv_equality [THEN diff_eq_eq [THEN iffD2 [THEN sym]]])
apply (rule trans [symmetric, OF _ emep1])
@@ -370,13 +359,13 @@
subsection "Simplifications for (s)bintrunc"
lemma bintrunc_n_0 [simp]: "bintrunc n 0 = 0"
- by (induct n) (auto simp add: Int.Pls_def)
+ by (induct n) auto
lemma sbintrunc_n_0 [simp]: "sbintrunc n 0 = 0"
- by (induct n) (auto simp add: Int.Pls_def)
+ by (induct n) auto
lemma sbintrunc_n_minus1 [simp]: "sbintrunc n -1 = -1"
- by (induct n) (auto, simp add: number_of_is_id)
+ by (induct n) auto
lemma bintrunc_Suc_numeral:
"bintrunc (Suc n) 1 = 1"
@@ -389,7 +378,7 @@
"sbintrunc 0 1 = -1"
"sbintrunc 0 (number_of (Int.Bit0 w)) = 0"
"sbintrunc 0 (number_of (Int.Bit1 w)) = -1"
- by (simp_all, unfold Pls_def number_of_is_id, simp_all)
+ by simp_all
lemma sbintrunc_Suc_numeral:
"sbintrunc (Suc n) 1 = 1"
@@ -403,7 +392,7 @@
lemmas bit_bool1 [simp] = refl [THEN bit_bool [THEN iffD1], symmetric]
-lemma bin_sign_lem: "(bin_sign (sbintrunc n bin) = Int.Min) = bin_nth bin n"
+lemma bin_sign_lem: "(bin_sign (sbintrunc n bin) = -1) = bin_nth bin n"
apply (induct n arbitrary: bin)
apply (case_tac bin rule: bin_exhaust, case_tac b, auto)+
done
@@ -516,10 +505,10 @@
sbintrunc.Z [where bin="w BIT (1::bit)",
simplified bin_last_simps bin_rest_simps bit.simps] for w
-lemma sbintrunc_0_Bit0 [simp]: "sbintrunc 0 (Int.Bit0 w) = Int.Pls"
+lemma sbintrunc_0_Bit0 [simp]: "sbintrunc 0 (Int.Bit0 w) = 0"
using sbintrunc_0_BIT_B0 by simp
-lemma sbintrunc_0_Bit1 [simp]: "sbintrunc 0 (Int.Bit1 w) = Int.Min"
+lemma sbintrunc_0_Bit1 [simp]: "sbintrunc 0 (Int.Bit1 w) = -1"
using sbintrunc_0_BIT_B1 by simp
lemmas sbintrunc_0_simps =
@@ -544,12 +533,12 @@
lemma bintrunc_n_Pls [simp]:
"bintrunc n Int.Pls = Int.Pls"
- by (induct n) (auto simp: BIT_simps)
+ unfolding Pls_def by simp
lemma sbintrunc_n_PM [simp]:
"sbintrunc n Int.Pls = Int.Pls"
"sbintrunc n Int.Min = Int.Min"
- by (induct n) (auto simp: BIT_simps)
+ unfolding Pls_def Min_def by simp_all
lemmas thobini1 = arg_cong [where f = "%w. w BIT b"] for b
@@ -561,11 +550,6 @@
lemmas bintrunc_Min_minus_I = bmsts(2)
lemmas bintrunc_BIT_minus_I = bmsts(3)
-lemma bintrunc_0_Min: "bintrunc 0 Int.Min = Int.Pls"
- by (fact bintrunc.Z) (* FIXME: delete *)
-lemma bintrunc_0_BIT: "bintrunc 0 (w BIT b) = Int.Pls"
- by (fact bintrunc.Z) (* FIXME: delete *)
-
lemma bintrunc_Suc_lem:
"bintrunc (Suc n) x = y ==> m = Suc n ==> bintrunc m x = y"
by auto
@@ -728,9 +712,9 @@
zmod_zsub_left_eq [where b = "1"]
lemmas bintr_arith1s =
- brdmod1s' [where c="2^n::int", folded pred_def succ_def bintrunc_mod2p] for n
+ brdmod1s' [where c="2^n::int", folded bintrunc_mod2p] for n
lemmas bintr_ariths =
- brdmods' [where c="2^n::int", folded pred_def succ_def bintrunc_mod2p] for n
+ brdmods' [where c="2^n::int", folded bintrunc_mod2p] for n
lemmas m2pths = pos_mod_sign pos_mod_bound [OF zless2p]
@@ -828,7 +812,7 @@
subsection {* Splitting and concatenation *}
primrec bin_split :: "nat \<Rightarrow> int \<Rightarrow> int \<times> int" where
- Z: "bin_split 0 w = (w, Int.Pls)"
+ Z: "bin_split 0 w = (w, 0)"
| Suc: "bin_split (Suc n) w = (let (w1, w2) = bin_split n (bin_rest w)
in (w1, w2 BIT bin_last w))"
--- a/src/HOL/Word/Bool_List_Representation.thy Tue Dec 27 09:45:10 2011 +0100
+++ b/src/HOL/Word/Bool_List_Representation.thy Tue Dec 27 15:38:45 2011 +0100
@@ -20,11 +20,7 @@
bl_to_bin_aux bs (w BIT (if b then 1 else 0))"
definition bl_to_bin :: "bool list \<Rightarrow> int" where
- bl_to_bin_def : "bl_to_bin bs = bl_to_bin_aux bs Int.Pls"
-
-lemma [code]:
- "bl_to_bin bs = bl_to_bin_aux bs 0"
- by (simp add: bl_to_bin_def Pls_def)
+ bl_to_bin_def: "bl_to_bin bs = bl_to_bin_aux bs 0"
primrec bin_to_bl_aux :: "nat \<Rightarrow> int \<Rightarrow> bool list \<Rightarrow> bool list" where
Z: "bin_to_bl_aux 0 w bl = bl"
@@ -89,6 +85,11 @@
"(butlast ^^ n) bl = take (length bl - n) bl"
by (induct n) (auto simp: butlast_take)
+lemma bin_to_bl_aux_zero_minus_simp [simp]:
+ "0 < n \<Longrightarrow> bin_to_bl_aux n 0 bl =
+ bin_to_bl_aux (n - 1) 0 (False # bl)"
+ by (cases n) auto
+
lemma bin_to_bl_aux_Pls_minus_simp [simp]:
"0 < n ==> bin_to_bl_aux n Int.Pls bl =
bin_to_bl_aux (n - 1) Int.Pls (False # bl)"
@@ -132,14 +133,14 @@
"bin_to_bl_aux n w bs = bin_to_bl n w @ bs"
unfolding bin_to_bl_def by (simp add : bin_to_bl_aux_append)
-lemma bin_to_bl_0: "bin_to_bl 0 bs = []"
+lemma bin_to_bl_0 [simp]: "bin_to_bl 0 bs = []"
unfolding bin_to_bl_def by auto
lemma size_bin_to_bl_aux:
"size (bin_to_bl_aux n w bs) = n + length bs"
by (induct n arbitrary: w bs) auto
-lemma size_bin_to_bl: "size (bin_to_bl n w) = n"
+lemma size_bin_to_bl [simp]: "size (bin_to_bl n w) = n"
unfolding bin_to_bl_def by (simp add : size_bin_to_bl_aux)
lemma bin_bl_bin':
@@ -147,7 +148,7 @@
bl_to_bin_aux bs (bintrunc n w)"
by (induct n arbitrary: w bs) (auto simp add : bl_to_bin_def)
-lemma bin_bl_bin: "bl_to_bin (bin_to_bl n w) = bintrunc n w"
+lemma bin_bl_bin [simp]: "bl_to_bin (bin_to_bl n w) = bintrunc n w"
unfolding bin_to_bl_def bin_bl_bin' by auto
lemma bl_bin_bl':
@@ -159,7 +160,7 @@
apply (auto simp add : bin_to_bl_def)
done
-lemma bl_bin_bl: "bin_to_bl (length bs) (bl_to_bin bs) = bs"
+lemma bl_bin_bl [simp]: "bin_to_bl (length bs) (bl_to_bin bs) = bs"
unfolding bl_to_bin_def
apply (rule box_equals)
apply (rule bl_bin_bl')
@@ -168,12 +169,6 @@
apply simp
done
-declare
- bin_to_bl_0 [simp]
- size_bin_to_bl [simp]
- bin_bl_bin [simp]
- bl_bin_bl [simp]
-
lemma bl_to_bin_inj:
"bl_to_bin bs = bl_to_bin cs ==> length bs = length cs ==> bs = cs"
apply (rule_tac box_equals)
@@ -183,12 +178,16 @@
apply simp
done
-lemma bl_to_bin_False: "bl_to_bin (False # bl) = bl_to_bin bl"
- unfolding bl_to_bin_def by (auto simp: BIT_simps)
-
-lemma bl_to_bin_Nil: "bl_to_bin [] = Int.Pls"
+lemma bl_to_bin_False [simp]: "bl_to_bin (False # bl) = bl_to_bin bl"
+ unfolding bl_to_bin_def by auto
+
+lemma bl_to_bin_Nil [simp]: "bl_to_bin [] = 0"
unfolding bl_to_bin_def by auto
+lemma bin_to_bl_zero_aux:
+ "bin_to_bl_aux n 0 bl = replicate n False @ bl"
+ by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same)
+
lemma bin_to_bl_Pls_aux:
"bin_to_bl_aux n Int.Pls bl = replicate n False @ bl"
by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same)
@@ -196,36 +195,31 @@
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)
lemma bl_to_bin_rep_F:
"bl_to_bin (replicate n False @ bl) = bl_to_bin bl"
- apply (simp add: bin_to_bl_Pls_aux [symmetric] bin_bl_bin')
+ apply (simp add: bin_to_bl_zero_aux [symmetric] bin_bl_bin')
apply (simp add: bl_to_bin_def)
done
-lemma bin_to_bl_trunc:
+lemma bin_to_bl_trunc [simp]:
"n <= m ==> bin_to_bl n (bintrunc m w) = bin_to_bl n w"
by (auto intro: bl_to_bin_inj)
-declare
- bin_to_bl_trunc [simp]
- bl_to_bin_False [simp]
- bl_to_bin_Nil [simp]
-
-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")
- apply (clarsimp simp: bin_to_bl_Pls_aux)
+ apply (clarsimp simp: bin_to_bl_zero_aux)
apply (erule thin_rl)
apply (induct_tac n)
apply auto
@@ -236,7 +230,7 @@
replicate (n - m) False @ bin_to_bl (min n m) bin"
unfolding bin_to_bl_def by (rule bin_to_bl_aux_bintr)
-lemma bl_to_bin_rep_False: "bl_to_bin (replicate n False) = Int.Pls"
+lemma bl_to_bin_rep_False: "bl_to_bin (replicate n False) = 0"
by (induct n) auto
lemma len_bin_to_bl_aux:
@@ -250,12 +244,12 @@
"bin_sign (bl_to_bin_aux bs w) = bin_sign w"
by (induct bs arbitrary: w) auto
-lemma sign_bl_bin: "bin_sign (bl_to_bin bs) = Int.Pls"
+lemma sign_bl_bin: "bin_sign (bl_to_bin bs) = 0"
unfolding bl_to_bin_def by (simp add : sign_bl_bin')
lemma bl_sbin_sign_aux:
"hd (bin_to_bl_aux (Suc n) w bs) =
- (bin_sign (sbintrunc n w) = Int.Min)"
+ (bin_sign (sbintrunc n w) = -1)"
apply (induct n arbitrary: w bs)
apply clarsimp
apply (cases w rule: bin_exhaust)
@@ -264,16 +258,16 @@
done
lemma bl_sbin_sign:
- "hd (bin_to_bl (Suc n) w) = (bin_sign (sbintrunc n w) = Int.Min)"
+ "hd (bin_to_bl (Suc n) w) = (bin_sign (sbintrunc n w) = -1)"
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
@@ -281,9 +275,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)
@@ -294,38 +287,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
@@ -338,13 +331,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
@@ -381,24 +374,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
@@ -419,9 +412,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
@@ -453,11 +446,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)
@@ -466,34 +470,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
@@ -513,10 +503,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)
@@ -529,28 +519,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)
@@ -562,29 +551,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)
@@ -673,7 +659,7 @@
lemma bl_to_bin_aux_alt:
"bl_to_bin_aux bs w = bin_cat w (length bs) (bl_to_bin bs)"
- using bl_to_bin_aux_cat [where nv = "0" and v = "Int.Pls"]
+ using bl_to_bin_aux_cat [where nv = "0" and v = "0"]
unfolding bl_to_bin_def [symmetric] by simp
lemma bin_to_bl_cat:
@@ -704,7 +690,7 @@
Int.succ (bl_to_bin (replicate n True))"
apply (unfold bl_to_bin_def)
apply (induct n)
- apply (simp add: BIT_simps)
+ apply (simp add: Int.succ_def)
apply (simp only: Suc_eq_plus1 replicate_add
append_Cons [symmetric] bl_to_bin_aux_append)
apply (simp add: BIT_simps)
@@ -727,9 +713,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)
@@ -957,17 +943,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
@@ -1036,8 +1021,6 @@
in (w1, w2 BIT bin_last w))"
by (simp only: nobm1 bin_split_minus_simp)
-declare bin_split_pred_simp [simp]
-
lemma bin_rsplit_aux_simp_alt:
"bin_rsplit_aux n m c bs =
(if m = 0 \<or> n = 0
@@ -1055,15 +1038,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
@@ -1136,8 +1118,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)
--- a/src/HOL/Word/Word.thy Tue Dec 27 09:45:10 2011 +0100
+++ b/src/HOL/Word/Word.thy Tue Dec 27 15:38:45 2011 +0100
@@ -115,8 +115,6 @@
definition word_int_case :: "(int => 'b) => ('a :: len0 word) => 'b" where
"word_int_case f w = f (uint w)"
-syntax
- of_int :: "int => 'a"
translations
"case x of CONST of_int y => b" == "CONST word_int_case (%y. b) x"
@@ -192,12 +190,12 @@
definition
word_succ :: "'a :: len0 word => 'a word"
where
- "word_succ a = word_of_int (Int.succ (uint a))"
+ "word_succ a = word_of_int (uint a + 1)"
definition
word_pred :: "'a :: len0 word => 'a word"
where
- "word_pred a = word_of_int (Int.pred (uint a))"
+ "word_pred a = word_of_int (uint a - 1)"
instantiation word :: (len0) "{number, Divides.div, comm_monoid_mult, comm_ring}"
begin
@@ -241,8 +239,8 @@
wi_hom_add: "word_of_int a + word_of_int b = word_of_int (a + b)" and
wi_hom_mult: "word_of_int a * word_of_int b = word_of_int (a * b)" and
wi_hom_neg: "- word_of_int a = word_of_int (- a)" and
- wi_hom_succ: "word_succ (word_of_int a) = word_of_int (Int.succ a)" and
- wi_hom_pred: "word_pred (word_of_int a) = word_of_int (Int.pred a)"
+ wi_hom_succ: "word_succ (word_of_int a) = word_of_int (a + 1)" and
+ wi_hom_pred: "word_pred (word_of_int a) = word_of_int (a - 1)"
by (auto simp: word_arith_wis arths)
lemmas wi_hom_syms = wi_homs [symmetric]
@@ -257,17 +255,17 @@
lemmas new_word_of_int_hom_syms = new_word_of_int_homs [symmetric]
lemmas word_of_int_hom_syms =
- new_word_of_int_hom_syms [unfolded succ_def pred_def]
+ new_word_of_int_hom_syms (* FIXME: duplicate *)
lemmas word_of_int_homs =
- new_word_of_int_homs [unfolded succ_def pred_def]
+ new_word_of_int_homs (* FIXME: duplicate *)
(* FIXME: provide only one copy of these theorems! *)
lemmas word_of_int_add_hom = wi_hom_add
lemmas word_of_int_mult_hom = wi_hom_mult
lemmas word_of_int_minus_hom = wi_hom_neg
-lemmas word_of_int_succ_hom = wi_hom_succ [unfolded succ_def]
-lemmas word_of_int_pred_hom = wi_hom_pred [unfolded pred_def]
+lemmas word_of_int_succ_hom = wi_hom_succ
+lemmas word_of_int_pred_hom = wi_hom_pred
lemmas word_of_int_0_hom = word_0_wi
lemmas word_of_int_1_hom = word_1_wi
@@ -379,16 +377,12 @@
definition
word_msb_def:
- "msb a \<longleftrightarrow> bin_sign (sint a) = Int.Min"
+ "msb a \<longleftrightarrow> bin_sign (sint a) = -1"
instance ..
end
-lemma [code]:
- "msb a \<longleftrightarrow> bin_sign (sint a) = (- 1 :: int)"
- by (simp only: word_msb_def Min_def)
-
definition setBit :: "'a :: len0 word => nat => 'a word" where
"setBit w n = set_bit w n True"
@@ -554,19 +548,17 @@
lemma uint_bintrunc [simp]:
"uint (number_of bin :: 'a word) =
- number_of (bintrunc (len_of TYPE ('a :: len0)) bin)"
- unfolding word_number_of_def number_of_eq
- by (auto intro: word_ubin.eq_norm)
+ bintrunc (len_of TYPE ('a :: len0)) (number_of bin)"
+ unfolding word_number_of_alt by (rule word_ubin.eq_norm)
lemma sint_sbintrunc [simp]:
"sint (number_of bin :: 'a word) =
- number_of (sbintrunc (len_of TYPE ('a :: len) - 1) bin)"
- unfolding word_number_of_def number_of_eq
- by (subst word_sbin.eq_norm) simp
+ sbintrunc (len_of TYPE ('a :: len) - 1) (number_of bin)"
+ unfolding word_number_of_alt by (rule word_sbin.eq_norm)
lemma unat_bintrunc [simp]:
"unat (number_of bin :: 'a :: len0 word) =
- number_of (bintrunc (len_of TYPE('a)) bin)"
+ nat (bintrunc (len_of TYPE('a)) (number_of bin))"
unfolding unat_def nat_number_of_def
by (simp only: uint_bintrunc)
@@ -632,15 +624,15 @@
2 ^ (len_of TYPE('a) - 1)"
unfolding word_number_of_alt by (rule int_word_sint)
-lemma word_of_int_0: "word_of_int 0 = 0"
+lemma word_of_int_0 [simp]: "word_of_int 0 = 0"
unfolding word_0_wi ..
-lemma word_of_int_1: "word_of_int 1 = 1"
+lemma word_of_int_1 [simp]: "word_of_int 1 = 1"
unfolding word_1_wi ..
lemma word_of_int_bin [simp] :
"(word_of_int (number_of bin) :: 'a :: len0 word) = (number_of bin)"
- unfolding word_number_of_alt by auto
+ unfolding word_number_of_alt ..
lemma word_int_case_wi:
"word_int_case f (word_of_int i :: 'b word) =
@@ -776,7 +768,7 @@
lemma length_bl_neq_0 [iff]: "length (to_bl (x::'a::len word)) \<noteq> 0"
by (fact length_bl_gt_0 [THEN gr_implies_not0])
-lemma hd_bl_sign_sint: "hd (to_bl w) = (bin_sign (sint w) = Int.Min)"
+lemma hd_bl_sign_sint: "hd (to_bl w) = (bin_sign (sint w) = -1)"
apply (unfold to_bl_def sint_uint)
apply (rule trans [OF _ bl_sbin_sign])
apply simp
@@ -892,14 +884,14 @@
(* for literal u(s)cast *)
-lemma ucast_bintr [simp]:
+lemma ucast_bintr [simp]:
"ucast (number_of w ::'a::len0 word) =
- number_of (bintrunc (len_of TYPE('a)) w)"
+ word_of_int (bintrunc (len_of TYPE('a)) (number_of w))"
unfolding ucast_def by simp
-lemma scast_sbintr [simp]:
+lemma scast_sbintr [simp]:
"scast (number_of w ::'a::len word) =
- number_of (sbintrunc (len_of TYPE('a) - Suc 0) w)"
+ word_of_int (sbintrunc (len_of TYPE('a) - Suc 0) (number_of w))"
unfolding scast_def by simp
lemmas source_size = source_size_def [unfolded Let_def word_size]
@@ -1106,7 +1098,7 @@
by (simp only: Pls_def word_0_wi)
lemma word_0_no: "(0::'a::len0 word) = Numeral0"
- by (simp add: word_number_of_alt word_0_wi)
+ by (simp add: word_number_of_alt)
lemma int_one_bin: "(1 :: int) = (Int.Pls BIT 1)"
unfolding Pls_def Bit_def by auto
@@ -1122,18 +1114,18 @@
by (simp add: word_m1_wi number_of_eq)
lemma word_0_bl [simp]: "of_bl [] = 0"
- unfolding word_0_wi of_bl_def by (simp add : Pls_def)
+ unfolding of_bl_def by (simp add: Pls_def)
lemma word_1_bl: "of_bl [True] = 1"
- unfolding word_1_wi of_bl_def
- by (simp add : bl_to_bin_def Bit_def Pls_def)
+ unfolding of_bl_def
+ by (simp add: bl_to_bin_def Bit_def Pls_def)
lemma uint_eq_0 [simp] : "(uint 0 = 0)"
unfolding word_0_wi
by (simp add: word_ubin.eq_norm Pls_def [symmetric])
-lemma of_bl_0 [simp] : "of_bl (replicate n False) = 0"
- by (simp add : word_0_wi of_bl_def bl_to_bin_rep_False Pls_def)
+lemma of_bl_0 [simp]: "of_bl (replicate n False) = 0"
+ by (simp add: of_bl_def bl_to_bin_rep_False Pls_def)
lemma to_bl_0 [simp]:
"to_bl (0::'a::len0 word) = replicate (len_of TYPE('a)) False"
@@ -1167,13 +1159,13 @@
by (auto simp: unat_0_iff [symmetric])
lemma ucast_0 [simp]: "ucast 0 = 0"
- unfolding ucast_def by (simp add: word_of_int_0)
+ unfolding ucast_def by simp
lemma sint_0 [simp]: "sint 0 = 0"
unfolding sint_uint by simp
lemma scast_0 [simp]: "scast 0 = 0"
- unfolding scast_def by (simp add: word_of_int_0)
+ unfolding scast_def by simp
lemma sint_n1 [simp] : "sint -1 = -1"
unfolding word_m1_wi by (simp add: word_sbin.eq_norm)
@@ -1183,22 +1175,22 @@
lemma uint_1 [simp]: "uint (1::'a::len word) = 1"
unfolding word_1_wi
- by (simp add: word_ubin.eq_norm bintrunc_minus_simps)
+ by (simp add: word_ubin.eq_norm bintrunc_minus_simps del: word_of_int_1)
lemma unat_1 [simp]: "unat (1::'a::len word) = 1"
unfolding unat_def by simp
lemma ucast_1 [simp]: "ucast (1::'a::len word) = 1"
- unfolding ucast_def by (simp add: word_of_int_1)
+ unfolding ucast_def by simp
(* now, to get the weaker results analogous to word_div/mod_def *)
lemmas word_arith_alts =
- word_sub_wi [unfolded succ_def pred_def]
- word_arith_wis [unfolded succ_def pred_def]
-
-lemmas word_succ_alt = word_arith_alts (5)
-lemmas word_pred_alt = word_arith_alts (6)
+ word_sub_wi
+ word_arith_wis (* FIXME: duplicate *)
+
+lemmas word_succ_alt = word_succ_def (* FIXME: duplicate *)
+lemmas word_pred_alt = word_pred_def (* FIXME: duplicate *)
subsection "Transferring goals from words to ints"
@@ -1211,8 +1203,9 @@
word_mult_succ: "word_succ a * b = b + a * b"
by (rule word_uint.Abs_cases [of b],
rule word_uint.Abs_cases [of a],
- simp add: pred_def succ_def add_commute mult_commute
- ring_distribs new_word_of_int_homs)+
+ simp add: add_commute mult_commute
+ ring_distribs new_word_of_int_homs
+ del: word_of_int_0 word_of_int_1)+
lemma uint_cong: "x = y \<Longrightarrow> uint x = uint y"
by simp
@@ -1243,7 +1236,8 @@
lemma succ_pred_no [simp]:
"word_succ (number_of bin) = number_of (Int.succ bin) &
word_pred (number_of bin) = number_of (Int.pred bin)"
- unfolding word_number_of_def by (simp add : new_word_of_int_homs)
+ unfolding word_number_of_def Int.succ_def Int.pred_def
+ by (simp add: new_word_of_int_homs)
lemma word_sp_01 [simp] :
"word_succ -1 = 0 & word_succ 0 = 1 & word_pred 0 = -1 & word_pred 1 = 0"
@@ -1639,7 +1633,7 @@
apply (unfold word_succ_def)
apply clarify
apply (simp add: to_bl_of_bin)
- apply (simp add: to_bl_def rbl_succ)
+ apply (simp add: to_bl_def rbl_succ Int.succ_def)
done
lemma word_pred_rbl:
@@ -1647,7 +1641,7 @@
apply (unfold word_pred_def)
apply clarify
apply (simp add: to_bl_of_bin)
- apply (simp add: to_bl_def rbl_pred)
+ apply (simp add: to_bl_def rbl_pred Int.pred_def)
done
lemma word_add_rbl:
@@ -1698,7 +1692,7 @@
lemma iszero_word_no [simp] :
"iszero (number_of bin :: 'a :: len word) =
- iszero (number_of (bintrunc (len_of TYPE('a)) bin) :: int)"
+ iszero (bintrunc (len_of TYPE('a)) (number_of bin))"
apply (simp add: zero_bintrunc number_of_is_id)
apply (unfold iszero_def Pls_def)
apply (rule refl)
@@ -1787,10 +1781,10 @@
by (simp add: word_of_nat word_of_int_succ_hom add_ac)
lemma Abs_fnat_hom_0: "(0::'a::len word) = of_nat 0"
- by (simp add: word_of_nat word_0_wi)
+ by simp
lemma Abs_fnat_hom_1: "(1::'a::len word) = of_nat (Suc 0)"
- by (simp add: word_of_nat word_1_wi)
+ by simp
lemmas Abs_fnat_homs =
Abs_fnat_hom_add Abs_fnat_hom_mult Abs_fnat_hom_Suc
@@ -1802,7 +1796,7 @@
lemma word_arith_nat_mult:
"a * b = of_nat (unat a * unat b)"
- by (simp add: Abs_fnat_hom_mult [symmetric])
+ by (simp add: of_nat_mult)
lemma word_arith_nat_Suc:
"word_succ a = of_nat (Suc (unat a))"
@@ -2067,7 +2061,7 @@
lemma word_of_int_power_hom:
"word_of_int a ^ n = (word_of_int (a ^ n) :: 'a :: len word)"
- by (induct n) (simp_all add: word_of_int_hom_syms)
+ by (induct n) (simp_all add: wi_hom_mult [symmetric])
lemma word_arith_power_alt:
"a ^ n = (word_of_int (uint a ^ n) :: 'a :: len word)"
@@ -2447,7 +2441,12 @@
assumes "m ~= n"
shows "set_bit (set_bit w m x) n y = set_bit (set_bit w n y) m x"
by (rule word_eqI) (clarsimp simp add: test_bit_set_gen word_size assms)
-
+
+lemma test_bit_wi [simp]:
+ "(word_of_int x::'a::len0 word) !! n \<longleftrightarrow> n < len_of TYPE('a) \<and> bin_nth x n"
+ unfolding word_test_bit_def
+ by (simp add: nth_bintr [symmetric] word_ubin.eq_norm)
+
lemma test_bit_no [simp]:
"(number_of bin :: 'a::len0 word) !! n \<equiv> n < len_of TYPE('a) \<and> bin_nth bin n"
unfolding word_test_bit_def word_number_of_def word_size
@@ -2469,19 +2468,18 @@
lemma word_set_no [simp]:
"set_bit (number_of bin::'a::len0 word) n b =
- number_of (bin_sc n (if b then 1 else 0) bin)"
- apply (unfold word_set_bit_def word_number_of_def [symmetric])
+ word_of_int (bin_sc n (if b then 1 else 0) (number_of bin))"
+ unfolding word_set_bit_def
apply (rule word_eqI)
- apply (clarsimp simp: word_size bin_nth_sc_gen number_of_is_id
- nth_bintr)
+ apply (simp add: word_size bin_nth_sc_gen nth_bintr)
done
lemma setBit_no [simp]:
- "setBit (number_of bin) n = number_of (bin_sc n 1 bin) "
+ "setBit (number_of bin) n = word_of_int (bin_sc n 1 (number_of bin))"
by (simp add: setBit_def)
lemma clearBit_no [simp]:
- "clearBit (number_of bin) n = number_of (bin_sc n 0 bin)"
+ "clearBit (number_of bin) n = word_of_int (bin_sc n 0 (number_of bin))"
by (simp add: clearBit_def)
lemma to_bl_n1:
@@ -2529,11 +2527,11 @@
apply (case_tac "nat")
apply clarsimp
apply (case_tac "n")
- apply (clarsimp simp add : word_1_wi [symmetric])
- apply (clarsimp simp add : word_0_wi [symmetric] BIT_simps)
+ apply clarsimp
+ apply clarsimp
apply (drule word_gt_0 [THEN iffD1])
apply (safe intro!: word_eqI bin_nth_lem ext)
- apply (auto simp add: test_bit_2p nth_2p_bin word_test_bit_def [symmetric] BIT_simps)
+ apply (auto simp add: test_bit_2p nth_2p_bin word_test_bit_def [symmetric])
done
lemma word_of_int_2p: "(word_of_int (2 ^ n) :: 'a :: len word) = 2 ^ n"
@@ -2545,7 +2543,7 @@
apply (rule box_equals)
apply (rule_tac [2] bintr_ariths (1))+
apply (clarsimp simp add : number_of_is_id)
- apply (simp add: BIT_simps)
+ apply simp
done
lemma bang_is_le: "x !! m \<Longrightarrow> 2 ^ m <= (x :: 'a :: len word)"
@@ -2577,37 +2575,35 @@
subsection {* Shifting, Rotating, and Splitting Words *}
-lemma shiftl1_number [simp] :
- "shiftl1 (number_of w) = number_of (w BIT 0)"
- apply (unfold shiftl1_def word_number_of_def)
- apply (simp add: word_ubin.norm_eq_iff [symmetric] word_ubin.eq_norm
- del: BIT_simps)
+lemma shiftl1_wi [simp]: "shiftl1 (word_of_int w) = word_of_int (w BIT 0)"
+ unfolding shiftl1_def
+ apply (simp only: word_ubin.norm_eq_iff [symmetric] word_ubin.eq_norm)
apply (subst refl [THEN bintrunc_BIT_I, symmetric])
apply (subst bintrunc_bintrunc_min)
apply simp
done
+lemma shiftl1_number [simp] :
+ "shiftl1 (number_of w) = number_of (Int.Bit0 w)"
+ unfolding word_number_of_alt shiftl1_wi by simp
+
lemma shiftl1_0 [simp] : "shiftl1 0 = 0"
- unfolding word_0_no shiftl1_number by (auto simp: BIT_simps)
-
-lemma shiftl1_def_u: "shiftl1 w = number_of (uint w BIT 0)"
- by (simp only: word_number_of_def shiftl1_def)
-
-lemma shiftl1_def_s: "shiftl1 w = number_of (sint w BIT 0)"
- by (rule trans [OF _ shiftl1_number]) simp
-
-lemma shiftr1_0 [simp] : "shiftr1 0 = 0"
- unfolding shiftr1_def
- by simp (simp add: word_0_wi)
-
-lemma sshiftr1_0 [simp] : "sshiftr1 0 = 0"
- apply (unfold sshiftr1_def)
- apply simp
- apply (simp add : word_0_wi)
- done
+ unfolding shiftl1_def by simp
+
+lemma shiftl1_def_u: "shiftl1 w = word_of_int (uint w BIT 0)"
+ by (simp only: shiftl1_def) (* FIXME: duplicate *)
+
+lemma shiftl1_def_s: "shiftl1 w = word_of_int (sint w BIT 0)"
+ unfolding shiftl1_def Bit_B0 wi_hom_syms by simp
+
+lemma shiftr1_0 [simp]: "shiftr1 0 = 0"
+ unfolding shiftr1_def by simp
+
+lemma sshiftr1_0 [simp]: "sshiftr1 0 = 0"
+ unfolding sshiftr1_def by simp
lemma sshiftr1_n1 [simp] : "sshiftr1 -1 = -1"
- unfolding sshiftr1_def by auto
+ unfolding sshiftr1_def by simp
lemma shiftl_0 [simp] : "(0::'a::len0 word) << n = 0"
unfolding shiftl_def by (induct n) auto
@@ -2745,8 +2741,7 @@
unfolding bshiftr1_def by (rule word_bl.Abs_inverse) simp
lemma shiftl1_of_bl: "shiftl1 (of_bl bl) = of_bl (bl @ [False])"
- unfolding uint_bl of_bl_no
- by (simp add: bl_to_bin_aux_append bl_to_bin_def)
+ by (simp add: of_bl_def bl_to_bin_append)
lemma shiftl1_bl: "shiftl1 (w::'a::len0 word) = of_bl (to_bl w @ [False])"
proof -
@@ -2910,16 +2905,10 @@
(* note - the following results use 'a :: len word < number_ring *)
lemma shiftl1_2t: "shiftl1 (w :: 'a :: len word) = 2 * w"
- apply (simp add: shiftl1_def_u BIT_simps)
- apply (simp only: double_number_of_Bit0 [symmetric])
- apply simp
- done
+ by (simp add: shiftl1_def Bit_def wi_hom_mult [symmetric])
lemma shiftl1_p: "shiftl1 (w :: 'a :: len word) = w + w"
- apply (simp add: shiftl1_def_u BIT_simps)
- apply (simp only: double_number_of_Bit0 [symmetric])
- apply simp
- done
+ by (simp add: shiftl1_2t)
lemma shiftl_t2n: "shiftl (w :: 'a :: len word) n = 2 ^ n * w"
unfolding shiftl_def
@@ -3056,7 +3045,7 @@
lemma mask_bin: "mask n = number_of (bintrunc n Int.Min)"
by (auto simp add: nth_bintr word_size intro: word_eqI)
-lemma and_mask_bintr: "w AND mask n = number_of (bintrunc n (uint w))"
+lemma and_mask_bintr: "w AND mask n = word_of_int (bintrunc n (uint w))"
apply (rule word_eqI)
apply (simp add: nth_bintr word_size word_ops_nth_size)
apply (auto simp add: test_bit_bin)
@@ -3080,10 +3069,11 @@
done
lemma and_mask_mod_2p: "w AND mask n = word_of_int (uint w mod 2 ^ n)"
- by (fact and_mask_bintr [unfolded word_number_of_alt no_bintr_alt])
+ by (simp only: and_mask_bintr bintrunc_mod2p)
lemma and_mask_lt_2p: "uint (w AND mask n) < 2 ^ n"
- apply (simp add : and_mask_bintr no_bintr_alt)
+ apply (simp add: and_mask_bintr word_ubin.eq_norm)
+ apply (simp add: bintrunc_mod2p)
apply (rule xtr8)
prefer 2
apply (rule pos_mod_bound)
@@ -3102,7 +3092,8 @@
lemma and_mask_dvd: "2 ^ n dvd uint w = (w AND mask n = 0)"
apply (simp add: dvd_eq_mod_eq_0 and_mask_mod_2p)
- apply (simp add: word_uint.norm_eq_iff [symmetric] word_of_int_homs)
+ apply (simp add: word_uint.norm_eq_iff [symmetric] word_of_int_homs
+ del: word_of_int_0)
apply (subst word_uint.norm_Rep [symmetric])
apply (simp only: bintrunc_bintrunc_min bintrunc_mod2p [symmetric] min_def)
apply auto
@@ -3499,7 +3490,7 @@
apply (unfold word_size)
apply (cases "len_of TYPE('a) >= len_of TYPE('b)")
defer
- apply (simp add: word_0_wi_Pls)
+ apply simp
apply (simp add : of_bl_def to_bl_def)
apply (subst bin_split_take1 [symmetric])
prefer 2
@@ -4279,7 +4270,7 @@
lemma shiftr1_1 [simp]:
"shiftr1 (1::'a::len word) = 0"
- by (simp add: shiftr1_def word_0_wi)
+ unfolding shiftr1_def by simp
lemma shiftr_1[simp]:
"(1::'a::len word) >> n = (if n = 0 then 1 else 0)"
@@ -4589,7 +4580,4 @@
setup {* SMT_Word.setup *}
-text {* Legacy simp rules *}
-declare BIT_simps [simp]
-
end