--- a/src/HOL/Word/BinBoolList.thy Fri Apr 04 13:40:23 2008 +0200
+++ b/src/HOL/Word/BinBoolList.thy Fri Apr 04 13:40:24 2008 +0200
@@ -9,33 +9,33 @@
header "Bool lists and integers"
-theory BinBoolList imports BinOperations begin
+theory BinBoolList
+imports BinOperations
+begin
subsection "Arithmetic in terms of bool lists"
-consts (* arithmetic operations in terms of the reversed bool list,
+(* arithmetic operations in terms of the reversed bool list,
assuming input list(s) the same length, and don't extend them *)
- rbl_succ :: "bool list => bool list"
- rbl_pred :: "bool list => bool list"
- rbl_add :: "bool list => bool list => bool list"
- rbl_mult :: "bool list => bool list => bool list"
-primrec
+primrec rbl_succ :: "bool list => bool list" where
Nil: "rbl_succ Nil = Nil"
- Cons: "rbl_succ (x # xs) = (if x then False # rbl_succ xs else True # xs)"
+ | Cons: "rbl_succ (x # xs) = (if x then False # rbl_succ xs else True # xs)"
-primrec
- Nil : "rbl_pred Nil = Nil"
- Cons : "rbl_pred (x # xs) = (if x then False # xs else True # rbl_pred xs)"
+primrec rbl_pred :: "bool list => bool list" where
+ Nil: "rbl_pred Nil = Nil"
+ | Cons: "rbl_pred (x # xs) = (if x then False # xs else True # rbl_pred xs)"
-primrec (* result is length of first arg, second arg may be longer *)
- Nil : "rbl_add Nil x = Nil"
- Cons : "rbl_add (y # ys) x = (let ws = rbl_add ys (tl x) in
+primrec rbl_add :: "bool list => bool list => bool list" where
+ (* result is length of first arg, second arg may be longer *)
+ Nil: "rbl_add Nil x = Nil"
+ | Cons: "rbl_add (y # ys) x = (let ws = rbl_add ys (tl x) in
(y ~= hd x) # (if hd x & y then rbl_succ ws else ws))"
-primrec (* result is length of first arg, second arg may be longer *)
- Nil : "rbl_mult Nil x = Nil"
- Cons : "rbl_mult (y # ys) x = (let ws = False # rbl_mult ys x in
+primrec rbl_mult :: "bool list => bool list => bool list" where
+ (* result is length of first arg, second arg may be longer *)
+ Nil: "rbl_mult Nil x = Nil"
+ | Cons: "rbl_mult (y # ys) x = (let ws = False # rbl_mult ys x in
if y then rbl_add ws x else ws)"
lemma tl_take: "tl (take n l) = take (n - 1) (tl l)"
@@ -102,16 +102,16 @@
(** link between bin and bool list **)
-lemma bl_to_bin_aux_append [rule_format] :
- "ALL w. bl_to_bin_aux w (bs @ cs) = bl_to_bin_aux (bl_to_bin_aux w bs) cs"
- by (induct bs) auto
+lemma bl_to_bin_aux_append:
+ "bl_to_bin_aux (bs @ cs) w = bl_to_bin_aux cs (bl_to_bin_aux bs w)"
+ by (induct bs arbitrary: w) auto
-lemma bin_to_bl_aux_append [rule_format] :
- "ALL w bs. bin_to_bl_aux n w bs @ cs = bin_to_bl_aux n w (bs @ cs)"
- by (induct n) auto
+lemma bin_to_bl_aux_append:
+ "bin_to_bl_aux n w bs @ cs = bin_to_bl_aux n w (bs @ cs)"
+ by (induct n arbitrary: w bs) auto
lemma bl_to_bin_append:
- "bl_to_bin (bs @ cs) = bl_to_bin_aux (bl_to_bin bs) cs"
+ "bl_to_bin (bs @ cs) = bl_to_bin_aux cs (bl_to_bin bs)"
unfolding bl_to_bin_def by (rule bl_to_bin_aux_append)
lemma bin_to_bl_aux_alt:
@@ -121,25 +121,25 @@
lemma bin_to_bl_0: "bin_to_bl 0 bs = []"
unfolding bin_to_bl_def by auto
-lemma size_bin_to_bl_aux [rule_format] :
- "ALL w bs. size (bin_to_bl_aux n w bs) = n + length bs"
- by (induct n) 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"
unfolding bin_to_bl_def by (simp add : size_bin_to_bl_aux)
-lemma bin_bl_bin' [rule_format] :
- "ALL w bs. bl_to_bin (bin_to_bl_aux n w bs) =
- bl_to_bin_aux (bintrunc n w) bs"
- by (induct n) (auto simp add : bl_to_bin_def)
+lemma bin_bl_bin':
+ "bl_to_bin (bin_to_bl_aux n w bs) =
+ 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"
unfolding bin_to_bl_def bin_bl_bin' by auto
-lemma bl_bin_bl' [rule_format] :
- "ALL w n. bin_to_bl (n + length bs) (bl_to_bin_aux w bs) =
+lemma bl_bin_bl':
+ "bin_to_bl (n + length bs) (bl_to_bin_aux bs w) =
bin_to_bl_aux n w bs"
- apply (induct "bs")
+ apply (induct bs arbitrary: w n)
apply auto
apply (simp_all only : add_Suc [symmetric])
apply (auto simp add : bin_to_bl_def)
@@ -175,9 +175,9 @@
lemma bl_to_bin_Nil: "bl_to_bin [] = Int.Pls"
unfolding bl_to_bin_def by auto
-lemma bin_to_bl_Pls_aux [rule_format] :
- "ALL bl. bin_to_bl_aux n Int.Pls bl = replicate n False @ bl"
- by (induct n) (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)
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)
@@ -223,26 +223,26 @@
lemma bl_to_bin_rep_False: "bl_to_bin (replicate n False) = Int.Pls"
by (induct n) auto
-lemma len_bin_to_bl_aux [rule_format] :
- "ALL w bs. length (bin_to_bl_aux n w bs) = n + length bs"
- by (induct "n") auto
+lemma len_bin_to_bl_aux:
+ "length (bin_to_bl_aux n w bs) = n + length bs"
+ by (induct n arbitrary: w bs) auto
lemma len_bin_to_bl [simp]: "length (bin_to_bl n w) = n"
unfolding bin_to_bl_def len_bin_to_bl_aux by auto
-lemma sign_bl_bin' [rule_format] :
- "ALL w. bin_sign (bl_to_bin_aux w bs) = bin_sign w"
- by (induct bs) auto
+lemma sign_bl_bin':
+ "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"
unfolding bl_to_bin_def by (simp add : sign_bl_bin')
-lemma bl_sbin_sign_aux [rule_format] :
- "ALL w bs. hd (bin_to_bl_aux (Suc n) w bs) =
+lemma bl_sbin_sign_aux:
+ "hd (bin_to_bl_aux (Suc n) w bs) =
(bin_sign (sbintrunc n w) = Int.Min)"
- apply (induct "n")
+ apply (induct n arbitrary: w bs)
apply clarsimp
- apply (case_tac w rule: bin_exhaust)
+ apply (cases w rule: bin_exhaust)
apply (simp split add : bit.split)
apply clarsimp
done
@@ -251,15 +251,15 @@
"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] :
- "ALL w. bin_nth (bl_to_bin_aux w bl) n =
+lemma bin_nth_of_bl_aux [rule_format]:
+ "\<forall>w. 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 clarsimp
apply clarsimp
apply (cut_tac x=n and y="size list" in linorder_less_linear)
apply (erule disjE, simp add: nth_append)+
- apply (simp add: nth_append)
+ apply auto
done
lemma bin_nth_of_bl: "bin_nth (bl_to_bin bl) n = (n < length bl & rev bl ! n)";
@@ -307,14 +307,14 @@
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] :
- "ALL w. bl_to_bin_aux w bs < (w + 1) * (2 ^ length bs)"
- apply (induct "bs")
+lemma bl_to_bin_lt2p_aux [rule_format]:
+ "\<forall>w. bl_to_bin_aux bs w < (w + 1) * (2 ^ length bs)"
+ apply (induct bs)
apply clarsimp
apply clarsimp
apply safe
- apply (erule allE, erule xtr8 [rotated],
- simp add: numeral_simps ring_simps cong add : number_of_False_cong)+
+ apply (erule allE, erule xtr8 [rotated],
+ simp add: numeral_simps ring_simps cong add : number_of_False_cong)+
done
lemma bl_to_bin_lt2p: "bl_to_bin bs < (2 ^ length bs)"
@@ -326,7 +326,7 @@
done
lemma bl_to_bin_ge2p_aux [rule_format] :
- "ALL w. bl_to_bin_aux w bs >= w * (2 ^ length bs)"
+ "\<forall>w. bl_to_bin_aux bs w >= w * (2 ^ length bs)"
apply (induct bs)
apply clarsimp
apply clarsimp
@@ -354,10 +354,10 @@
lemmas butlast_bin_rest = butlast_rest_bin
[where w="bl_to_bin bl" and n="length bl", simplified, standard]
-lemma butlast_rest_bl2bin_aux [rule_format] :
- "ALL w. bl ~= [] -->
- bl_to_bin_aux w (butlast bl) = bin_rest (bl_to_bin_aux w bl)"
- by (induct bl) auto
+lemma butlast_rest_bl2bin_aux:
+ "bl ~= [] \<Longrightarrow>
+ bl_to_bin_aux (butlast bl) w = bin_rest (bl_to_bin_aux bl w)"
+ by (induct bl arbitrary: w) auto
lemma butlast_rest_bl2bin:
"bl_to_bin (butlast bl) = bin_rest (bl_to_bin bl)"
@@ -366,9 +366,9 @@
apply (auto simp add: butlast_rest_bl2bin_aux)
done
-lemma trunc_bl2bin_aux [rule_format] :
- "ALL w. bintrunc m (bl_to_bin_aux w bl) =
- bl_to_bin_aux (bintrunc (m - length bl) w) (drop (length bl - m) bl)"
+lemma trunc_bl2bin_aux [rule_format]:
+ "ALL w. 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 clarsimp
apply clarsimp
@@ -376,13 +376,13 @@
apply (case_tac "m - size list")
apply (simp add : diff_is_0_eq [THEN iffD1, THEN Suc_diff_le])
apply simp
- apply (rule_tac f = "%nat. bl_to_bin_aux (Int.Bit1 (bintrunc nat w)) list"
+ apply (rule_tac f = "%nat. bl_to_bin_aux list (Int.Bit1 (bintrunc nat w))"
in arg_cong)
apply simp
apply (case_tac "m - size list")
apply (simp add: diff_is_0_eq [THEN iffD1, THEN Suc_diff_le])
apply simp
- apply (rule_tac f = "%nat. bl_to_bin_aux (Int.Bit0 (bintrunc nat w)) list"
+ apply (rule_tac f = "%nat. bl_to_bin_aux list (Int.Bit0 (bintrunc nat w))"
in arg_cong)
apply simp
done
@@ -420,9 +420,9 @@
lemma hd_butlast: "size xs > 1 ==> hd (butlast xs) = hd xs"
by (cases xs) auto
-lemma last_bin_last' [rule_format] :
- "ALL w. size xs > 0 --> last xs = (bin_last (bl_to_bin_aux w xs) = bit.B1)"
- by (induct xs) auto
+lemma last_bin_last':
+ "size xs > 0 \<Longrightarrow> last xs = (bin_last (bl_to_bin_aux xs w) = bit.B1)"
+ by (induct xs arbitrary: w) auto
lemma last_bin_last:
"size xs > 0 ==> last xs = (bin_last (bl_to_bin xs) = bit.B1)"
@@ -437,16 +437,16 @@
(** links between bit-wise operations and operations on bool lists **)
-lemma app2_Nil [simp]: "app2 f [] ys = []"
- unfolding app2_def by auto
+lemma map2_Nil [simp]: "map2 f [] ys = []"
+ unfolding map2_def by auto
-lemma app2_Cons [simp]:
- "app2 f (x # xs) (y # ys) = f x y # app2 f xs ys"
- unfolding app2_def by auto
+lemma map2_Cons [simp]:
+ "map2 f (x # xs) (y # ys) = f x y # map2 f xs ys"
+ unfolding map2_def by auto
lemma bl_xor_aux_bin [rule_format] : "ALL v w bs cs.
- app2 (%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) (app2 (%x y. x ~= y) bs cs)"
+ 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 simp
@@ -458,8 +458,8 @@
done
lemma bl_or_aux_bin [rule_format] : "ALL v w bs cs.
- app2 (op | ) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
- bin_to_bl_aux n (v OR w) (app2 (op | ) 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
@@ -471,8 +471,8 @@
done
lemma bl_and_aux_bin [rule_format] : "ALL v w bs cs.
- app2 (op & ) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
- bin_to_bl_aux n (v AND w) (app2 (op & ) bs cs)"
+ 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 simp
@@ -498,13 +498,13 @@
[where cs = "[]", unfolded bin_to_bl_def [symmetric] map.simps]
lemmas bl_and_bin = bl_and_aux_bin [where bs="[]" and cs="[]",
- unfolded app2_Nil, folded bin_to_bl_def]
+ unfolded map2_Nil, folded bin_to_bl_def]
lemmas bl_or_bin = bl_or_aux_bin [where bs="[]" and cs="[]",
- unfolded app2_Nil, folded bin_to_bl_def]
+ unfolded map2_Nil, folded bin_to_bl_def]
lemmas bl_xor_bin = bl_xor_aux_bin [where bs="[]" and cs="[]",
- unfolded app2_Nil, folded bin_to_bl_def]
+ unfolded map2_Nil, folded bin_to_bl_def]
lemma drop_bin2bl_aux [rule_format] :
"ALL m bin bs. drop m (bin_to_bl_aux n bin bs) =
@@ -651,8 +651,8 @@
(* links with function bl_to_bin *)
lemma bl_to_bin_aux_cat:
- "!!nv v. bl_to_bin_aux (bin_cat w nv v) bs =
- bin_cat w (nv + length bs) (bl_to_bin_aux v bs)"
+ "!!nv v. bl_to_bin_aux bs (bin_cat w nv v) =
+ bin_cat w (nv + length bs) (bl_to_bin_aux bs v)"
apply (induct bs)
apply simp
apply (simp add: bin_cat_Suc_Bit [symmetric] del: bin_cat.simps)
@@ -985,19 +985,21 @@
rsplit_aux_simp1s [OF disjI1] rsplit_aux_simp1s [OF disjI2]
lemma bin_rsplit_aux_append:
- "bin_rsplit_aux (n, bs @ cs, m, c) = bin_rsplit_aux (n, bs, m, c) @ cs"
- apply (rule_tac u=n and v=bs and w=m and x=c in bin_rsplit_aux.induct)
+ "bin_rsplit_aux n m c (bs @ cs) = bin_rsplit_aux n m c bs @ cs"
+ apply (induct n m c bs rule: bin_rsplit_aux.induct)
apply (subst bin_rsplit_aux.simps)
apply (subst bin_rsplit_aux.simps)
apply (clarsimp split: ls_splits)
+ apply auto
done
lemma bin_rsplitl_aux_append:
- "bin_rsplitl_aux (n, bs @ cs, m, c) = bin_rsplitl_aux (n, bs, m, c) @ cs"
- apply (rule_tac u=n and v=bs and w=m and x=c in bin_rsplitl_aux.induct)
+ "bin_rsplitl_aux n m c (bs @ cs) = bin_rsplitl_aux n m c bs @ cs"
+ apply (induct n m c bs rule: bin_rsplitl_aux.induct)
apply (subst bin_rsplitl_aux.simps)
apply (subst bin_rsplitl_aux.simps)
apply (clarsimp split: ls_splits)
+ apply auto
done
lemmas rsplit_aux_apps [where bs = "[]"] =
@@ -1024,17 +1026,18 @@
declare bin_split_pred_simp [simp]
lemma bin_rsplit_aux_simp_alt:
- "bin_rsplit_aux (n, bs, m, c) =
+ "bin_rsplit_aux n m c bs =
(if m = 0 \<or> n = 0
then bs
else let (a, b) = bin_split n c in bin_rsplit n (m - n, a) @ b # bs)"
- apply (rule trans)
- apply (subst bin_rsplit_aux.simps, rule refl)
- apply (simp add: rsplit_aux_alts)
+ unfolding bin_rsplit_aux.simps [of n m c bs]
+ apply simp
+ apply (subst rsplit_aux_alts)
+ apply (simp add: bin_rsplit_def)
done
lemmas bin_rsplit_simp_alt =
- trans [OF bin_rsplit_def [THEN meta_eq_to_obj_eq]
+ trans [OF bin_rsplit_def
bin_rsplit_aux_simp_alt, standard]
lemmas bthrs = bin_rsplit_simp_alt [THEN [2] trans]
@@ -1089,27 +1092,33 @@
apply (rule allI)
apply (subst bin_rsplitl_aux.simps)
apply (subst bin_rsplit_aux.simps)
- apply (clarsimp simp: rsplit_aux_alts Let_def split: ls_splits)
+ apply (clarsimp simp: Let_def split: ls_splits)
apply (drule bin_split_trunc)
apply (drule sym [THEN trans], assumption)
- apply fast
+ apply (subst rsplit_aux_alts(1))
+ apply (subst rsplit_aux_alts(2))
+ apply clarsimp
+ unfolding bin_rsplit_def bin_rsplitl_def
+ apply simp
done
-
+
lemma bin_rsplit_rcat [rule_format] :
"n > 0 --> bin_rsplit n (n * size ws, bin_rcat n ws) = map (bintrunc n) ws"
apply (unfold bin_rsplit_def bin_rcat_def)
apply (rule_tac xs = "ws" in rev_induct)
apply clarsimp
apply clarsimp
- apply (clarsimp simp add: bin_split_cat rsplit_aux_alts)
+ apply (subst rsplit_aux_alts)
+ unfolding bin_split_cat
+ apply simp
done
lemma bin_rsplit_aux_len_le [rule_format] :
- "ALL ws m. n \<noteq> 0 --> ws = bin_rsplit_aux (n, bs, nw, w) -->
- (length ws <= m) = (nw + length bs * n <= m * n)"
- apply (rule_tac u=n and v=bs and w=nw and x=w in bin_rsplit_aux.induct)
+ "\<forall>ws m. n \<noteq> 0 \<longrightarrow> ws = bin_rsplit_aux n nw w bs \<longrightarrow>
+ length ws \<le> m \<longleftrightarrow> nw + length bs * n \<le> m * n"
+ apply (induct n nw w bs rule: bin_rsplit_aux.induct)
apply (subst bin_rsplit_aux.simps)
- apply (simp add:lrlem Let_def split: ls_splits )
+ apply (simp add: lrlem Let_def split: ls_splits)
done
lemma bin_rsplit_len_le:
@@ -1117,9 +1126,9 @@
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, cs, nw, w)) =
+ "n\<noteq>0 --> length (bin_rsplit_aux n nw w cs) =
(nw + n - 1) div n + length cs"
- apply (rule_tac u=n and v=cs and w=nw and x=w in bin_rsplit_aux.induct)
+ apply (induct n nw w cs rule: bin_rsplit_aux.induct)
apply (subst bin_rsplit_aux.simps)
apply (clarsimp simp: Let_def split: ls_splits)
apply (erule thin_rl)
@@ -1134,27 +1143,30 @@
"n\<noteq>0 ==> length (bin_rsplit n (nw, w)) = (nw + n - 1) div n"
unfolding bin_rsplit_def by (clarsimp simp add : bin_rsplit_aux_len)
-lemma bin_rsplit_aux_len_indep [rule_format] :
- "n\<noteq>0 ==> (ALL v bs. length bs = length cs -->
- length (bin_rsplit_aux (n, bs, nw, v)) =
- length (bin_rsplit_aux (n, cs, nw, w)))"
- apply (rule_tac u=n and v=cs and w=nw and x=w in bin_rsplit_aux.induct)
- apply clarsimp
- apply (simp (no_asm_simp) add: bin_rsplit_aux_simp_alt Let_def
- split: ls_splits)
- apply clarify
- apply (erule allE)+
- apply (erule impE)
- apply (fast elim!: sym)
- apply (simp (no_asm_use) add: rsplit_aux_alts)
- apply (erule impE)
- apply (rule_tac x="ba # bs" in exI)
- apply auto
- done
+lemma bin_rsplit_aux_len_indep:
+ "n \<noteq> 0 \<Longrightarrow> length bs = length cs \<Longrightarrow>
+ length (bin_rsplit_aux n nw v bs) =
+ length (bin_rsplit_aux n nw w cs)"
+proof (induct n nw w cs arbitrary: v bs rule: bin_rsplit_aux.induct)
+ case (1 n m w cs v bs) show ?case
+ proof (cases "m = 0")
+ case True then show ?thesis by simp
+ next
+ case False
+ from "1.hyps" `m \<noteq> 0` `n \<noteq> 0` have hyp: "\<And>v bs. length bs = Suc (length cs) \<Longrightarrow>
+ length (bin_rsplit_aux n (m - n) v bs) =
+ length (bin_rsplit_aux n (m - n) (fst (bin_split n w)) (snd (bin_split n w) # cs))"
+ by auto
+ show ?thesis using `length bs = length cs` `n \<noteq> 0`
+ by (auto simp add: bin_rsplit_aux_simp_alt Let_def bin_rsplit_len
+ split: ls_splits)
+ qed
+qed
lemma bin_rsplit_len_indep:
"n\<noteq>0 ==> length (bin_rsplit n (nw, v)) = length (bin_rsplit n (nw, w))"
apply (unfold bin_rsplit_def)
+ apply (simp (no_asm))
apply (erule bin_rsplit_aux_len_indep)
apply (rule refl)
done
--- a/src/HOL/Word/BinGeneral.thy Fri Apr 04 13:40:23 2008 +0200
+++ b/src/HOL/Word/BinGeneral.thy Fri Apr 04 13:40:24 2008 +0200
@@ -9,98 +9,201 @@
header {* Basic Definitions for Binary Integers *}
-theory BinGeneral imports Num_Lemmas
-
+theory BinGeneral
+imports Num_Lemmas
begin
-subsection {* Recursion combinator for binary integers *}
+subsection {* Further properties of numerals *}
+
+datatype bit = B0 | B1
+
+definition
+ Bit :: "int \<Rightarrow> bit \<Rightarrow> int" (infixl "BIT" 90) where
+ "k BIT b = (case b of B0 \<Rightarrow> 0 | B1 \<Rightarrow> 1) + k + k"
+
+lemma BIT_B0_eq_Bit0 [simp]: "w BIT B0 = Int.Bit0 w"
+ unfolding Bit_def Bit0_def by simp
+
+lemma BIT_B1_eq_Bit1 [simp]: "w BIT B1 = Int.Bit1 w"
+ unfolding Bit_def Bit1_def by simp
+
+lemmas BIT_simps = BIT_B0_eq_Bit0 BIT_B1_eq_Bit1
-lemma brlem: "(bin = Int.Min) = (- bin + Int.pred 0 = 0)"
- unfolding Min_def pred_def by arith
+hide (open) const B0 B1
+
+lemma Min_ne_Pls [iff]:
+ "Int.Min ~= Int.Pls"
+ unfolding Min_def Pls_def by auto
+
+lemmas Pls_ne_Min [iff] = Min_ne_Pls [symmetric]
+
+lemmas PlsMin_defs [intro!] =
+ Pls_def Min_def Pls_def [symmetric] Min_def [symmetric]
+
+lemmas PlsMin_simps [simp] = PlsMin_defs [THEN Eq_TrueI]
+
+lemma number_of_False_cong:
+ "False \<Longrightarrow> number_of x = number_of y"
+ by (rule FalseE)
+
+(** ways in which type Bin resembles a datatype **)
-function
- bin_rec :: "'a \<Rightarrow> 'a \<Rightarrow> (int \<Rightarrow> bit \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> int \<Rightarrow> 'a"
-where
- "bin_rec f1 f2 f3 bin = (if bin = Int.Pls then f1
- else if bin = Int.Min then f2
- else case bin_rl bin of (w, b) => f3 w b (bin_rec f1 f2 f3 w))"
- by pat_completeness auto
+lemma BIT_eq: "u BIT b = v BIT c ==> u = v & b = c"
+ apply (unfold Bit_def)
+ apply (simp (no_asm_use) split: bit.split_asm)
+ apply simp_all
+ apply (drule_tac f=even in arg_cong, clarsimp)+
+ done
+
+lemmas BIT_eqE [elim!] = BIT_eq [THEN conjE, standard]
+
+lemma BIT_eq_iff [simp]:
+ "(u BIT b = v BIT c) = (u = v \<and> b = c)"
+ by (rule iffI) auto
+
+lemmas BIT_eqI [intro!] = conjI [THEN BIT_eq_iff [THEN iffD2]]
+
+lemma less_Bits:
+ "(v BIT b < w BIT c) = (v < w | v <= w & b = bit.B0 & c = bit.B1)"
+ unfolding Bit_def by (auto split: bit.split)
-termination
- apply (relation "measure (nat o abs o snd o snd o snd)")
- apply simp
- apply (simp add: Pls_def brlem)
- apply (clarsimp simp: bin_rl_char pred_def)
- apply (frule thin_rl [THEN refl [THEN bin_abs_lem [rule_format]]])
- apply (unfold Pls_def Min_def number_of_eq)
- prefer 2
- apply (erule asm_rl)
- apply auto
+lemma le_Bits:
+ "(v BIT b <= w BIT c) = (v < w | v <= w & (b ~= bit.B1 | c ~= bit.B0))"
+ unfolding Bit_def by (auto split: bit.split)
+
+lemma no_no [simp]: "number_of (number_of i) = i"
+ unfolding number_of_eq by simp
+
+lemma Bit_B0:
+ "k BIT bit.B0 = k + k"
+ by (unfold Bit_def) simp
+
+lemma Bit_B1:
+ "k BIT bit.B1 = k + k + 1"
+ by (unfold Bit_def) simp
+
+lemma Bit_B0_2t: "k BIT bit.B0 = 2 * k"
+ by (rule trans, rule Bit_B0) simp
+
+lemma Bit_B1_2t: "k BIT bit.B1 = 2 * k + 1"
+ by (rule trans, rule Bit_B1) simp
+
+lemma B_mod_2':
+ "X = 2 ==> (w BIT bit.B1) mod X = 1 & (w BIT bit.B0) mod X = 0"
+ apply (simp (no_asm) only: Bit_B0 Bit_B1)
+ apply (simp add: z1pmod2)
done
-declare bin_rec.simps [simp del]
+lemma B1_mod_2 [simp]: "(Int.Bit1 w) mod 2 = 1"
+ unfolding numeral_simps number_of_is_id by (simp add: z1pmod2)
-lemma bin_rec_PM:
- "f = bin_rec f1 f2 f3 ==> f Int.Pls = f1 & f Int.Min = f2"
- by (auto simp add: bin_rec.simps)
-
-lemma bin_rec_Pls: "bin_rec f1 f2 f3 Int.Pls = f1"
- by (simp add: bin_rec.simps)
+lemma B0_mod_2 [simp]: "(Int.Bit0 w) mod 2 = 0"
+ unfolding numeral_simps number_of_is_id by simp
-lemma bin_rec_Min: "bin_rec f1 f2 f3 Int.Min = f2"
- by (simp add: bin_rec.simps)
+lemma neB1E [elim!]:
+ assumes ne: "y \<noteq> bit.B1"
+ assumes y: "y = bit.B0 \<Longrightarrow> P"
+ shows "P"
+ apply (rule y)
+ apply (cases y rule: bit.exhaust, simp)
+ apply (simp add: ne)
+ done
-lemma bin_rec_Bit0:
- "f3 Int.Pls bit.B0 f1 = f1 \<Longrightarrow>
- bin_rec f1 f2 f3 (Int.Bit0 w) = f3 w bit.B0 (bin_rec f1 f2 f3 w)"
- apply (simp add: bin_rec_Pls bin_rec.simps [of _ _ _ "Int.Bit0 w"])
- unfolding Pls_def Min_def Bit0_def
- apply auto
- apply presburger
- apply (simp add: bin_rec.simps)
+lemma bin_ex_rl: "EX w b. w BIT b = bin"
+ apply (unfold Bit_def)
+ apply (cases "even bin")
+ apply (clarsimp simp: even_equiv_def)
+ apply (auto simp: odd_equiv_def split: bit.split)
done
-lemma bin_rec_Bit1:
- "f3 Int.Min bit.B1 f2 = f2 \<Longrightarrow>
- bin_rec f1 f2 f3 (Int.Bit1 w) = f3 w bit.B1 (bin_rec f1 f2 f3 w)"
- apply (simp add: bin_rec.simps [of _ _ _ "Int.Bit1 w"])
- unfolding Pls_def Min_def Bit1_def
- apply auto
- apply (cases w)
- apply auto
- apply (simp add: bin_rec.simps)
- unfolding Min_def Pls_def number_of_is_id apply auto
- unfolding Bit0_def apply presburger
+lemma bin_exhaust:
+ assumes Q: "\<And>x b. bin = x BIT b \<Longrightarrow> Q"
+ shows "Q"
+ apply (insert bin_ex_rl [of bin])
+ apply (erule exE)+
+ apply (rule Q)
+ apply force
done
-
-lemma bin_rec_Bit:
- "f = bin_rec f1 f2 f3 ==> f3 Int.Pls bit.B0 f1 = f1 ==>
- f3 Int.Min bit.B1 f2 = f2 ==> f (w BIT b) = f3 w b (f w)"
- by (cases b, simp add: bin_rec_Bit0, simp add: bin_rec_Bit1)
-lemmas bin_rec_simps = refl [THEN bin_rec_Bit] bin_rec_Pls bin_rec_Min
- bin_rec_Bit0 bin_rec_Bit1
subsection {* Destructors for binary integers *}
+definition bin_rl :: "int \<Rightarrow> int \<times> bit" where
+ [code func del]: "bin_rl w = (THE (r, l). w = r BIT l)"
+
+lemma bin_rl_char: "(bin_rl w = (r, l)) = (r BIT l = w)"
+ apply (unfold bin_rl_def)
+ apply safe
+ apply (cases w rule: bin_exhaust)
+ apply auto
+ done
+
definition
bin_rest_def [code func del]: "bin_rest w = fst (bin_rl w)"
definition
bin_last_def [code func del] : "bin_last w = snd (bin_rl w)"
-definition
- bin_sign_def [code func del] : "bin_sign = bin_rec Int.Pls Int.Min (%w b s. s)"
-
primrec bin_nth where
- "bin_nth.Z" : "bin_nth w 0 = (bin_last w = bit.B1)"
- | "bin_nth.Suc" : "bin_nth w (Suc n) = bin_nth (bin_rest w) n"
+ Z: "bin_nth w 0 = (bin_last w = bit.B1)"
+ | Suc: "bin_nth w (Suc n) = bin_nth (bin_rest w) n"
lemma bin_rl: "bin_rl w = (bin_rest w, bin_last w)"
unfolding bin_rest_def bin_last_def by auto
+lemma bin_rl_simps [simp]:
+ "bin_rl Int.Pls = (Int.Pls, bit.B0)"
+ "bin_rl Int.Min = (Int.Min, bit.B1)"
+ "bin_rl (Int.Bit0 r) = (r, bit.B0)"
+ "bin_rl (Int.Bit1 r) = (r, bit.B1)"
+ "bin_rl (r BIT b) = (r, b)"
+ unfolding bin_rl_char by simp_all
+
+declare bin_rl_simps(1-4) [code func]
+
lemmas bin_rl_simp [simp] = iffD1 [OF bin_rl_char bin_rl]
+lemma bin_abs_lem:
+ "bin = (w BIT b) ==> ~ bin = Int.Min --> ~ bin = Int.Pls -->
+ nat (abs w) < nat (abs bin)"
+ apply (clarsimp simp add: bin_rl_char)
+ apply (unfold Pls_def Min_def Bit_def)
+ apply (cases b)
+ apply (clarsimp, arith)
+ apply (clarsimp, arith)
+ done
+
+lemma bin_induct:
+ assumes PPls: "P Int.Pls"
+ and PMin: "P Int.Min"
+ and PBit: "!!bin bit. P bin ==> P (bin BIT bit)"
+ shows "P bin"
+ apply (rule_tac P=P and a=bin and f1="nat o abs"
+ in wf_measure [THEN wf_induct])
+ apply (simp add: measure_def inv_image_def)
+ apply (case_tac x rule: bin_exhaust)
+ apply (frule bin_abs_lem)
+ apply (auto simp add : PPls PMin PBit)
+ done
+
+lemma numeral_induct:
+ assumes Pls: "P Int.Pls"
+ assumes Min: "P Int.Min"
+ assumes Bit0: "\<And>w. \<lbrakk>P w; w \<noteq> Int.Pls\<rbrakk> \<Longrightarrow> P (Int.Bit0 w)"
+ assumes Bit1: "\<And>w. \<lbrakk>P w; w \<noteq> Int.Min\<rbrakk> \<Longrightarrow> P (Int.Bit1 w)"
+ shows "P x"
+ apply (induct x rule: bin_induct)
+ apply (rule Pls)
+ apply (rule Min)
+ apply (case_tac bit)
+ apply (case_tac "bin = Int.Pls")
+ apply simp
+ apply (simp add: Bit0)
+ apply (case_tac "bin = Int.Min")
+ apply simp
+ apply (simp add: Bit1)
+ done
+
lemma bin_rest_simps [simp]:
"bin_rest Int.Pls = Int.Pls"
"bin_rest Int.Min = Int.Min"
@@ -121,16 +224,6 @@
declare bin_last_simps(1-4) [code func]
-lemma bin_sign_simps [simp]:
- "bin_sign Int.Pls = Int.Pls"
- "bin_sign Int.Min = Int.Min"
- "bin_sign (Int.Bit0 w) = bin_sign w"
- "bin_sign (Int.Bit1 w) = bin_sign w"
- "bin_sign (w BIT b) = bin_sign w"
- unfolding bin_sign_def by (auto simp: bin_rec_simps)
-
-declare bin_sign_simps(1-4) [code func]
-
lemma bin_r_l_extras [simp]:
"bin_last 0 = bit.B0"
"bin_last (- 1) = bit.B1"
@@ -237,11 +330,94 @@
bin_nth_0 bin_nth_Suc bin_nth_Pls bin_nth_Min bin_nth_minus
bin_nth_minus_Bit0 bin_nth_minus_Bit1
+
+subsection {* Recursion combinator for binary integers *}
+
+lemma brlem: "(bin = Int.Min) = (- bin + Int.pred 0 = 0)"
+ unfolding Min_def pred_def by arith
+
+function
+ bin_rec :: "'a \<Rightarrow> 'a \<Rightarrow> (int \<Rightarrow> bit \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> int \<Rightarrow> 'a"
+where
+ "bin_rec f1 f2 f3 bin = (if bin = Int.Pls then f1
+ else if bin = Int.Min then f2
+ else case bin_rl bin of (w, b) => f3 w b (bin_rec f1 f2 f3 w))"
+ by pat_completeness auto
+
+termination
+ apply (relation "measure (nat o abs o snd o snd o snd)")
+ apply simp
+ apply (simp add: Pls_def brlem)
+ apply (clarsimp simp: bin_rl_char pred_def)
+ apply (frule thin_rl [THEN refl [THEN bin_abs_lem [rule_format]]])
+ apply (unfold Pls_def Min_def number_of_eq)
+ prefer 2
+ apply (erule asm_rl)
+ apply auto
+ done
+
+declare bin_rec.simps [simp del]
+
+lemma bin_rec_PM:
+ "f = bin_rec f1 f2 f3 ==> f Int.Pls = f1 & f Int.Min = f2"
+ by (auto simp add: bin_rec.simps)
+
+lemma bin_rec_Pls: "bin_rec f1 f2 f3 Int.Pls = f1"
+ by (simp add: bin_rec.simps)
+
+lemma bin_rec_Min: "bin_rec f1 f2 f3 Int.Min = f2"
+ by (simp add: bin_rec.simps)
+
+lemma bin_rec_Bit0:
+ "f3 Int.Pls bit.B0 f1 = f1 \<Longrightarrow>
+ bin_rec f1 f2 f3 (Int.Bit0 w) = f3 w bit.B0 (bin_rec f1 f2 f3 w)"
+ apply (simp add: bin_rec_Pls bin_rec.simps [of _ _ _ "Int.Bit0 w"])
+ unfolding Pls_def Min_def Bit0_def
+ apply auto
+ apply presburger
+ apply (simp add: bin_rec.simps)
+ done
+
+lemma bin_rec_Bit1:
+ "f3 Int.Min bit.B1 f2 = f2 \<Longrightarrow>
+ bin_rec f1 f2 f3 (Int.Bit1 w) = f3 w bit.B1 (bin_rec f1 f2 f3 w)"
+ apply (simp add: bin_rec.simps [of _ _ _ "Int.Bit1 w"])
+ unfolding Pls_def Min_def Bit1_def
+ apply auto
+ apply (cases w)
+ apply auto
+ apply (simp add: bin_rec.simps)
+ unfolding Min_def Pls_def number_of_is_id apply auto
+ unfolding Bit0_def apply presburger
+ done
+
+lemma bin_rec_Bit:
+ "f = bin_rec f1 f2 f3 ==> f3 Int.Pls bit.B0 f1 = f1 ==>
+ f3 Int.Min bit.B1 f2 = f2 ==> f (w BIT b) = f3 w b (f w)"
+ by (cases b, simp add: bin_rec_Bit0, simp add: bin_rec_Bit1)
+
+lemmas bin_rec_simps = refl [THEN bin_rec_Bit] bin_rec_Pls bin_rec_Min
+ bin_rec_Bit0 bin_rec_Bit1
+
+
+subsection {* Truncating binary integers *}
+
+definition
+ bin_sign_def [code func del] : "bin_sign = bin_rec Int.Pls Int.Min (%w b s. s)"
+
+lemma bin_sign_simps [simp]:
+ "bin_sign Int.Pls = Int.Pls"
+ "bin_sign Int.Min = Int.Min"
+ "bin_sign (Int.Bit0 w) = bin_sign w"
+ "bin_sign (Int.Bit1 w) = bin_sign w"
+ "bin_sign (w BIT b) = bin_sign w"
+ unfolding bin_sign_def by (auto simp: bin_rec_simps)
+
+declare bin_sign_simps(1-4) [code func]
+
lemma bin_sign_rest [simp]:
"bin_sign (bin_rest w) = (bin_sign w)"
- by (case_tac w rule: bin_exhaust) auto
-
-subsection {* Truncating binary integers *}
+ by (cases w rule: bin_exhaust) auto
consts
bintrunc :: "nat => int => int"
@@ -718,18 +894,14 @@
subsection {* Splitting and concatenation *}
-consts
- bin_split :: "nat => int => int * int"
-primrec
- Z : "bin_split 0 w = (w, Int.Pls)"
- Suc : "bin_split (Suc n) w = (let (w1, w2) = bin_split n (bin_rest w)
- in (w1, w2 BIT bin_last w))"
+primrec bin_split :: "nat \<Rightarrow> int \<Rightarrow> int \<times> int" where
+ Z: "bin_split 0 w = (w, Int.Pls)"
+ | Suc: "bin_split (Suc n) w = (let (w1, w2) = bin_split n (bin_rest w)
+ in (w1, w2 BIT bin_last w))"
-consts
- bin_cat :: "int => nat => int => int"
-primrec
- Z : "bin_cat w 0 v = w"
- Suc : "bin_cat w (Suc n) v = bin_cat w n (bin_rest v) BIT bin_last v"
+primrec bin_cat :: "int \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int" where
+ Z: "bin_cat w 0 v = w"
+ | Suc: "bin_cat w (Suc n) v = bin_cat w n (bin_rest v) BIT bin_last v"
subsection {* Miscellaneous lemmas *}