--- a/src/HOL/Word/BinBoolList.thy Wed Jun 30 16:41:03 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1174 +0,0 @@
-(*
- Author: Jeremy Dawson, NICTA
-
- contains theorems to do with integers, expressed using Pls, Min, BIT,
- theorems linking them to lists of booleans, and repeated splitting
- and concatenation.
-*)
-
-header "Bool lists and integers"
-
-theory BinBoolList
-imports BinOperations
-begin
-
-subsection {* Operations on lists of booleans *}
-
-primrec bl_to_bin_aux :: "bool list \<Rightarrow> int \<Rightarrow> int" where
- Nil: "bl_to_bin_aux [] w = w"
- | Cons: "bl_to_bin_aux (b # bs) w =
- 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"
-
-primrec bin_to_bl_aux :: "nat \<Rightarrow> int \<Rightarrow> bool list \<Rightarrow> bool list" where
- Z: "bin_to_bl_aux 0 w bl = bl"
- | Suc: "bin_to_bl_aux (Suc n) w bl =
- bin_to_bl_aux n (bin_rest w) ((bin_last w = 1) # bl)"
-
-definition bin_to_bl :: "nat \<Rightarrow> int \<Rightarrow> bool list" where
- bin_to_bl_def : "bin_to_bl n w = bin_to_bl_aux n w []"
-
-primrec bl_of_nth :: "nat \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool list" where
- Suc: "bl_of_nth (Suc n) f = f n # bl_of_nth n f"
- | Z: "bl_of_nth 0 f = []"
-
-primrec takefill :: "'a \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
- Z: "takefill fill 0 xs = []"
- | Suc: "takefill fill (Suc n) xs = (
- case xs of [] => fill # takefill fill n xs
- | y # ys => y # takefill fill n ys)"
-
-definition map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list" where
- "map2 f as bs = map (split f) (zip as bs)"
-
-lemma map2_Nil [simp]: "map2 f [] ys = []"
- unfolding map2_def by auto
-
-lemma map2_Nil2 [simp]: "map2 f xs [] = []"
- unfolding map2_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
-
-
-subsection "Arithmetic in terms of bool lists"
-
-(* arithmetic operations in terms of the reversed bool list,
- assuming input list(s) the same length, and don't extend them *)
-
-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)"
-
-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 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 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 butlast_power:
- "(butlast ^^ n) bl = take (length bl - n) bl"
- by (induct n) (auto simp: butlast_take)
-
-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)"
- by (cases n) auto
-
-lemma bin_to_bl_aux_Min_minus_simp [simp]:
- "0 < n ==> bin_to_bl_aux n Int.Min bl =
- bin_to_bl_aux (n - 1) Int.Min (True # bl)"
- by (cases n) auto
-
-lemma bin_to_bl_aux_Bit_minus_simp [simp]:
- "0 < n ==> bin_to_bl_aux n (w BIT b) bl =
- bin_to_bl_aux (n - 1) w ((b = 1) # bl)"
- by (cases n) auto
-
-lemma bin_to_bl_aux_Bit0_minus_simp [simp]:
- "0 < n ==> bin_to_bl_aux n (Int.Bit0 w) bl =
- bin_to_bl_aux (n - 1) w (False # bl)"
- by (cases n) auto
-
-lemma bin_to_bl_aux_Bit1_minus_simp [simp]:
- "0 < n ==> bin_to_bl_aux n (Int.Bit1 w) bl =
- bin_to_bl_aux (n - 1) w (True # bl)"
- by (cases n) auto
-
-(** link between bin and bool list **)
-
-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:
- "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 cs (bl_to_bin bs)"
- unfolding bl_to_bin_def by (rule bl_to_bin_aux_append)
-
-lemma bin_to_bl_aux_alt:
- "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 = []"
- 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"
- unfolding bin_to_bl_def by (simp add : size_bin_to_bl_aux)
-
-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':
- "bin_to_bl (n + length bs) (bl_to_bin_aux bs w) =
- bin_to_bl_aux n w bs"
- apply (induct bs arbitrary: w n)
- apply auto
- apply (simp_all only : add_Suc [symmetric])
- apply (auto simp add : bin_to_bl_def)
- done
-
-lemma bl_bin_bl: "bin_to_bl (length bs) (bl_to_bin bs) = bs"
- unfolding bl_to_bin_def
- apply (rule box_equals)
- apply (rule bl_bin_bl')
- prefer 2
- apply (rule bin_to_bl_aux.Z)
- 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)
- defer
- apply (rule bl_bin_bl)
- apply (rule bl_bin_bl)
- apply simp
- done
-
-lemma bl_to_bin_False: "bl_to_bin (False # bl) = bl_to_bin bl"
- unfolding bl_to_bin_def by auto
-
-lemma bl_to_bin_Nil: "bl_to_bin [] = Int.Pls"
- unfolding bl_to_bin_def by auto
-
-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)
-
-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: "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: bl_to_bin_def)
- done
-
-lemma bin_to_bl_trunc:
- "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 =
- replicate (n - m) False @ bin_to_bl_aux (min n m) bin bl"
- apply (induct n)
- apply clarsimp
- apply clarsimp
- apply (case_tac "m")
- apply (clarsimp simp: bin_to_bl_Pls_aux)
- apply (erule thin_rl)
- apply (induct_tac n)
- apply auto
- done
-
-lemmas bin_to_bl_bintr =
- bin_to_bl_aux_bintr [where bl = "[]", folded bin_to_bl_def]
-
-lemma bl_to_bin_rep_False: "bl_to_bin (replicate n False) = Int.Pls"
- 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':
- "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:
- "hd (bin_to_bl_aux (Suc n) w bs) =
- (bin_sign (sbintrunc n w) = Int.Min)"
- apply (induct n arbitrary: w bs)
- apply clarsimp
- apply (cases w rule: bin_exhaust)
- apply (simp split add : bit.split)
- apply clarsimp
- done
-
-lemma bl_sbin_sign:
- "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 =
- (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 auto
- done
-
-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)
- apply clarsimp
- apply (case_tac m, clarsimp)
- apply (clarsimp simp: bin_to_bl_def)
- apply (simp add: bin_to_bl_aux_alt)
- apply clarsimp
- apply (case_tac m, clarsimp)
- apply (clarsimp simp: bin_to_bl_def)
- 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")
- 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 arith
- done
-
-lemmas nth_rev_alt = nth_rev [where xs = "rev ys", simplified, standard]
-
-lemma nth_bin_to_bl_aux [rule_format] :
- "ALL w n bl. n < m + length bl --> (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 clarsimp
- apply clarsimp
- apply (case_tac w rule: bin_exhaust)
- apply clarsimp
- apply (case_tac "n - m")
- apply arith
- apply simp
- apply (rule_tac f = "%n. bl ! n" in arg_cong)
- apply arith
- 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)
- apply clarsimp
- apply clarsimp
- apply safe
- apply (erule allE, erule xtr8 [rotated],
- simp add: numeral_simps algebra_simps cong add : number_of_False_cong)+
- done
-
-lemma bl_to_bin_lt2p: "bl_to_bin bs < (2 ^ length bs)"
- apply (unfold bl_to_bin_def)
- apply (rule xtr1)
- prefer 2
- apply (rule bl_to_bin_lt2p_aux)
- 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)
- apply clarsimp
- apply clarsimp
- apply safe
- apply (erule allE, erule preorder_class.order_trans [rotated],
- simp add: numeral_simps algebra_simps cong add : number_of_False_cong)+
- done
-
-lemma bl_to_bin_ge0: "bl_to_bin bs >= 0"
- apply (unfold bl_to_bin_def)
- apply (rule xtr4)
- apply (rule bl_to_bin_ge2p_aux)
- apply simp
- done
-
-lemma butlast_rest_bin:
- "butlast (bin_to_bl n w) = bin_to_bl (n - 1) (bin_rest w)"
- apply (unfold bin_to_bl_def)
- apply (cases w rule: bin_exhaust)
- apply (cases n, clarsimp)
- apply clarsimp
- apply (auto simp add: bin_to_bl_aux_alt)
- done
-
-lemmas butlast_bin_rest = butlast_rest_bin
- [where w="bl_to_bin bl" and n="length bl", simplified, standard]
-
-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)"
- apply (unfold bl_to_bin_def)
- apply (cases bl)
- 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) =
- bl_to_bin_aux (drop (length bl - m) bl) (bintrunc (m - length bl) w)"
- apply (induct_tac bl)
- apply clarsimp
- apply clarsimp
- apply safe
- 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 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 list (Int.Bit0 (bintrunc nat w))"
- in arg_cong)
- apply simp
- done
-
-lemma trunc_bl2bin:
- "bintrunc m (bl_to_bin bl) = bl_to_bin (drop (length bl - m) bl)"
- unfolding bl_to_bin_def by (simp add : trunc_bl2bin_aux)
-
-lemmas trunc_bl2bin_len [simp] =
- trunc_bl2bin [of "length bl" bl, simplified, standard]
-
-lemma bl2bin_drop:
- "bl_to_bin (drop k bl) = bintrunc (length bl - k) (bl_to_bin bl)"
- apply (rule trans)
- prefer 2
- apply (rule trunc_bl2bin [symmetric])
- apply (cases "k <= length bl")
- 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)
- apply clarsimp
- apply (simp only: bin_nth.Suc [symmetric] add_Suc)
- done
-
-lemma take_rest_power_bin:
- "m <= n ==> take m (bin_to_bl n w) = bin_to_bl m ((bin_rest ^^ (n - m)) w)"
- apply (rule nth_equalityI)
- apply simp
- apply (clarsimp simp add: nth_bin_to_bl nth_rest_power_bin)
- done
-
-lemma hd_butlast: "size xs > 1 ==> hd (butlast xs) = hd xs"
- by (cases xs) auto
-
-lemma last_bin_last':
- "size xs > 0 \<Longrightarrow> last xs = (bin_last (bl_to_bin_aux xs w) = 1)"
- by (induct xs arbitrary: w) auto
-
-lemma last_bin_last:
- "size xs > 0 ==> last xs = (bin_last (bl_to_bin xs) = 1)"
- unfolding bl_to_bin_def by (erule last_bin_last')
-
-lemma bin_last_last:
- "bin_last w = (if last (bin_to_bl (Suc n) w) then 1 else 0)"
- apply (unfold bin_to_bl_def)
- apply simp
- apply (auto simp add: bin_to_bl_aux_alt)
- done
-
-(** 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) =
- bin_to_bl_aux n (v XOR w) (map2 (%x y. x ~= y) 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_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) =
- bin_to_bl_aux n (v AND 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_not_aux_bin [rule_format] :
- "ALL w cs. map Not (bin_to_bl_aux n w cs) =
- bin_to_bl_aux n (NOT w) (map Not cs)"
- apply (induct n)
- apply clarsimp
- apply clarsimp
- apply (case_tac w rule: bin_exhaust)
- apply (case_tac b)
- apply auto
- done
-
-lemmas bl_not_bin = bl_not_aux_bin
- [where cs = "[]", unfolded bin_to_bl_def [symmetric] map.simps]
-
-lemmas bl_and_bin = bl_and_aux_bin [where bs="[]" and cs="[]",
- unfolded map2_Nil, folded bin_to_bl_def]
-
-lemmas bl_or_bin = bl_or_aux_bin [where bs="[]" and cs="[]",
- unfolded map2_Nil, folded bin_to_bl_def]
-
-lemmas bl_xor_bin = bl_xor_aux_bin [where bs="[]" and cs="[]",
- 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) =
- bin_to_bl_aux (n - m) bin (drop (m - n) bs)"
- apply (induct n, clarsimp)
- apply clarsimp
- apply (case_tac bin rule: bin_exhaust)
- apply (case_tac "m <= n", simp)
- apply (case_tac "m - n", simp)
- apply simp
- apply (rule_tac f = "%nat. drop nat bs" in arg_cong)
- apply simp
- done
-
-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)
- 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) =
- take m (bin_to_bl (m + n) w)"
- apply (induct n)
- apply clarify
- 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) -->
- bin_to_bl m a = take m (bin_to_bl (m + n) c)"
- apply (induct n)
- apply clarsimp
- apply (clarsimp simp: Let_def split: ls_splits)
- apply (simp add: bin_to_bl_def)
- apply (simp add: take_bin2bl_lem)
- done
-
-lemma bin_split_take1:
- "k = m + n ==> bin_split n c = (a, b) ==>
- 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 -->
- takefill fill n l ! m = (if m < length l then l ! m else fill)"
- apply (induct n, 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_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 length_takefill [simp]: "length (takefill fill n l) = n"
- by (simp add : takefill_alt)
-
-lemma take_takefill':
- "!!w n. n = k + m ==> take k (takefill fill n w) = takefill fill k w"
- by (induct k) (auto split add : list.split)
-
-lemma drop_takefill:
- "!!w. drop k (takefill fill (m + k) w) = takefill fill m (drop k w)"
- by (induct k) (auto split add : list.split)
-
-lemma takefill_le [simp]:
- "m \<le> n \<Longrightarrow> takefill x m (takefill x n l) = takefill x m l"
- by (auto simp: le_iff_add takefill_le')
-
-lemma take_takefill [simp]:
- "m \<le> n \<Longrightarrow> take m (takefill fill n w) = takefill fill m w"
- by (auto simp: le_iff_add take_takefill')
-
-lemma takefill_append:
- "takefill fill (m + length xs) (xs @ w) = xs @ (takefill fill m w)"
- by (induct xs) auto
-
-lemma takefill_same':
- "l = length xs ==> takefill fill l xs = xs"
- by clarify (induct xs, auto)
-
-lemmas takefill_same [simp] = takefill_same' [OF refl]
-
-lemma takefill_bintrunc:
- "takefill False n bl = rev (bin_to_bl n (bl_to_bin (rev bl)))"
- apply (rule nth_equalityI)
- apply simp
- apply (clarsimp simp: nth_takefill nth_rev nth_bin_to_bl bin_nth_of_bl)
- done
-
-lemma bl_bin_bl_rtf:
- "bin_to_bl n (bl_to_bin bl) = rev (takefill False n (rev bl))"
- by (simp add : takefill_bintrunc)
-
-lemmas bl_bin_bl_rep_drop =
- bl_bin_bl_rtf [simplified takefill_alt,
- simplified, simplified rev_take, simplified]
-
-lemma tf_rev:
- "n + k = m + length bl ==> takefill x m (rev (takefill y n bl)) =
- rev (takefill y m (rev (takefill x k (rev bl))))"
- apply (rule nth_equalityI)
- apply (auto simp add: nth_takefill nth_rev)
- apply (rule_tac f = "%n. bl ! n" in arg_cong)
- apply arith
- done
-
-lemma takefill_minus:
- "0 < n ==> takefill fill (Suc (n - 1)) w = takefill fill n w"
- by auto
-
-lemmas takefill_Suc_cases =
- list.cases [THEN takefill.Suc [THEN trans], standard]
-
-lemmas takefill_Suc_Nil = takefill_Suc_cases (1)
-lemmas takefill_Suc_Cons = takefill_Suc_cases (2)
-
-lemmas takefill_minus_simps = takefill_Suc_cases [THEN [2]
- takefill_minus [symmetric, THEN trans], standard]
-
-lemmas takefill_pred_simps [simp] =
- takefill_minus_simps [where n="number_of bin", simplified nobm1, standard]
-
-(* links with function bl_to_bin *)
-
-lemma bl_to_bin_aux_cat:
- "!!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)
- done
-
-lemma bin_to_bl_aux_cat:
- "!!w bs. bin_to_bl_aux (nv + nw) (bin_cat v nw w) bs =
- bin_to_bl_aux nv v (bin_to_bl_aux nw w bs)"
- by (induct nw) auto
-
-lemmas bl_to_bin_aux_alt =
- bl_to_bin_aux_cat [where nv = "0" and v = "Int.Pls",
- simplified bl_to_bin_def [symmetric], simplified]
-
-lemmas bin_to_bl_cat =
- bin_to_bl_aux_cat [where bs = "[]", folded bin_to_bl_def]
-
-lemmas bl_to_bin_aux_app_cat =
- trans [OF bl_to_bin_aux_append bl_to_bin_aux_alt]
-
-lemmas bin_to_bl_aux_cat_app =
- trans [OF bin_to_bl_aux_cat bin_to_bl_aux_alt]
-
-lemmas bl_to_bin_app_cat = bl_to_bin_aux_app_cat
- [where w = "Int.Pls", folded bl_to_bin_def]
-
-lemmas bin_to_bl_cat_app = bin_to_bl_aux_cat_app
- [where bs = "[]", folded bin_to_bl_def]
-
-(* bl_to_bin_app_cat_alt and bl_to_bin_app_cat are easily interderivable *)
-lemma bl_to_bin_app_cat_alt:
- "bin_cat (bl_to_bin cs) n w = bl_to_bin (cs @ bin_to_bl n w)"
- by (simp add : bl_to_bin_app_cat)
-
-lemma mask_lem: "(bl_to_bin (True # replicate n False)) =
- Int.succ (bl_to_bin (replicate n True))"
- apply (unfold bl_to_bin_def)
- apply (induct n)
- apply simp
- apply (simp only: Suc_eq_plus1 replicate_add
- append_Cons [symmetric] bl_to_bin_aux_append)
- apply simp
- done
-
-(* function bl_of_nth *)
-lemma length_bl_of_nth [simp]: "length (bl_of_nth n f) = n"
- by (induct n) auto
-
-lemma nth_bl_of_nth [simp]:
- "m < n \<Longrightarrow> rev (bl_of_nth n f) ! m = f m"
- apply (induct n)
- apply simp
- apply (clarsimp simp add : nth_append)
- apply (rule_tac f = "f" in arg_cong)
- apply simp
- done
-
-lemma bl_of_nth_inj:
- "(!!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)
- apply clarsimp
- apply (rule trans [OF _ hd_Cons_tl])
- apply (frule Suc_le_lessD)
- apply (simp add: nth_rev trans [OF drop_Suc drop_tl, symmetric])
- apply (subst hd_drop_conv_nth)
- apply force
- apply simp_all
- apply (rule_tac f = "%n. drop n xs" in arg_cong)
- apply simp
- done
-
-lemmas bl_of_nth_nth [simp] = order_refl [THEN bl_of_nth_nth_le, simplified]
-
-lemma size_rbl_pred: "length (rbl_pred bl) = length bl"
- by (induct bl) auto
-
-lemma size_rbl_succ: "length (rbl_succ bl) = length bl"
- by (induct bl) auto
-
-lemma size_rbl_add:
- "!!cl. length (rbl_add bl cl) = length bl"
- by (induct bl) (auto simp: Let_def size_rbl_succ)
-
-lemma size_rbl_mult:
- "!!cl. length (rbl_mult bl cl) = length bl"
- by (induct bl) (auto simp add : Let_def size_rbl_add)
-
-lemmas rbl_sizes [simp] =
- size_rbl_pred size_rbl_succ size_rbl_add size_rbl_mult
-
-lemmas rbl_Nils =
- rbl_pred.Nil rbl_succ.Nil rbl_add.Nil rbl_mult.Nil
-
-lemma rbl_pred:
- "!!bin. rbl_pred (rev (bin_to_bl n bin)) = rev (bin_to_bl n (Int.pred bin))"
- apply (induct n, simp)
- apply (unfold bin_to_bl_def)
- apply clarsimp
- apply (case_tac bin rule: bin_exhaust)
- apply (case_tac b)
- apply (clarsimp simp: bin_to_bl_aux_alt)+
- done
-
-lemma rbl_succ:
- "!!bin. rbl_succ (rev (bin_to_bl n bin)) = rev (bin_to_bl n (Int.succ bin))"
- apply (induct n, simp)
- apply (unfold bin_to_bl_def)
- apply clarsimp
- apply (case_tac bin rule: bin_exhaust)
- apply (case_tac b)
- apply (clarsimp simp: bin_to_bl_aux_alt)+
- done
-
-lemma rbl_add:
- "!!bina binb. rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) =
- rev (bin_to_bl n (bina + binb))"
- apply (induct n, simp)
- apply (unfold bin_to_bl_def)
- apply clarsimp
- apply (case_tac bina rule: bin_exhaust)
- apply (case_tac binb rule: bin_exhaust)
- apply (case_tac b)
- apply (case_tac [!] "ba")
- apply (auto simp: rbl_succ succ_def bin_to_bl_aux_alt Let_def add_ac)
- done
-
-lemma rbl_add_app2:
- "!!blb. length blb >= length bla ==>
- rbl_add bla (blb @ blc) = rbl_add bla blb"
- apply (induct bla, simp)
- apply clarsimp
- apply (case_tac blb, clarsimp)
- apply (clarsimp simp: Let_def)
- done
-
-lemma rbl_add_take2:
- "!!blb. length blb >= length bla ==>
- rbl_add bla (take (length bla) blb) = rbl_add bla blb"
- apply (induct bla, simp)
- apply clarsimp
- apply (case_tac blb, clarsimp)
- apply (clarsimp simp: Let_def)
- done
-
-lemma rbl_add_long:
- "m >= n ==> rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl m binb)) =
- rev (bin_to_bl n (bina + binb))"
- apply (rule box_equals [OF _ rbl_add_take2 rbl_add])
- apply (rule_tac f = "rbl_add (rev (bin_to_bl n bina))" in arg_cong)
- apply (rule rev_swap [THEN iffD1])
- apply (simp add: rev_take drop_bin2bl)
- apply simp
- done
-
-lemma rbl_mult_app2:
- "!!blb. length blb >= length bla ==>
- rbl_mult bla (blb @ blc) = rbl_mult bla blb"
- apply (induct bla, simp)
- apply clarsimp
- apply (case_tac blb, clarsimp)
- apply (clarsimp simp: Let_def rbl_add_app2)
- done
-
-lemma rbl_mult_take2:
- "length blb >= length bla ==>
- rbl_mult bla (take (length bla) blb) = rbl_mult bla blb"
- apply (rule trans)
- apply (rule rbl_mult_app2 [symmetric])
- apply simp
- apply (rule_tac f = "rbl_mult bla" in arg_cong)
- apply (rule append_take_drop_id)
- done
-
-lemma rbl_mult_gt1:
- "m >= length bl ==> rbl_mult bl (rev (bin_to_bl m binb)) =
- rbl_mult bl (rev (bin_to_bl (length bl) binb))"
- apply (rule trans)
- apply (rule rbl_mult_take2 [symmetric])
- apply simp_all
- apply (rule_tac f = "rbl_mult bl" in arg_cong)
- apply (rule rev_swap [THEN iffD1])
- apply (simp add: rev_take drop_bin2bl)
- done
-
-lemma rbl_mult_gt:
- "m > n ==> rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl m binb)) =
- rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb))"
- by (auto intro: trans [OF rbl_mult_gt1])
-
-lemmas rbl_mult_Suc = lessI [THEN rbl_mult_gt]
-
-lemma rbbl_Cons:
- "b # rev (bin_to_bl n x) = rev (bin_to_bl (Suc n) (x BIT If b 1 0))"
- apply (unfold bin_to_bl_def)
- apply simp
- apply (simp add: bin_to_bl_aux_alt)
- done
-
-lemma rbl_mult: "!!bina binb.
- rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) =
- rev (bin_to_bl n (bina * binb))"
- apply (induct n)
- apply simp
- apply (unfold bin_to_bl_def)
- apply clarsimp
- apply (case_tac bina rule: bin_exhaust)
- apply (case_tac binb rule: bin_exhaust)
- apply (case_tac b)
- apply (case_tac [!] "ba")
- apply (auto simp: bin_to_bl_aux_alt Let_def)
- apply (auto simp: rbbl_Cons rbl_mult_Suc rbl_add)
- done
-
-lemma rbl_add_split:
- "P (rbl_add (y # ys) (x # xs)) =
- (ALL ws. length ws = length ys --> ws = rbl_add ys xs -->
- (y --> ((x --> P (False # rbl_succ ws)) & (~ x --> P (True # ws)))) &
- (~ y --> P (x # ws)))"
- apply (auto simp add: Let_def)
- apply (case_tac [!] "y")
- apply auto
- done
-
-lemma rbl_mult_split:
- "P (rbl_mult (y # ys) xs) =
- (ALL ws. length ws = Suc (length ys) --> ws = False # rbl_mult ys xs -->
- (y --> P (rbl_add ws xs)) & (~ y --> P ws))"
- by (clarsimp simp add : Let_def)
-
-lemma and_len: "xs = ys ==> xs = ys & length xs = length ys"
- by auto
-
-lemma size_if: "size (if p then xs else ys) = (if p then size xs else size ys)"
- by auto
-
-lemma tl_if: "tl (if p then xs else ys) = (if p then tl xs else tl ys)"
- by auto
-
-lemma hd_if: "hd (if p then xs else ys) = (if p then hd xs else hd ys)"
- by auto
-
-lemma if_Not_x: "(if p then ~ x else x) = (p = (~ x))"
- by auto
-
-lemma if_x_Not: "(if p then x else ~ x) = (p = x)"
- by auto
-
-lemma if_same_and: "(If p x y & If p u v) = (if p then x & u else y & v)"
- by auto
-
-lemma if_same_eq: "(If p x y = (If p u v)) = (if p then x = (u) else y = (v))"
- by auto
-
-lemma if_same_eq_not:
- "(If p x y = (~ If p u v)) = (if p then x = (~u) else y = (~v))"
- by auto
-
-(* note - if_Cons can cause blowup in the size, if p is complex,
- so make a simproc *)
-lemma if_Cons: "(if p then x # xs else y # ys) = If p x y # If p xs ys"
- by auto
-
-lemma if_single:
- "(if xc then [xab] else [an]) = [if xc then xab else an]"
- by auto
-
-lemma if_bool_simps:
- "If p True y = (p | y) & If p False y = (~p & y) &
- If p y True = (p --> y) & If p y False = (p & y)"
- by auto
-
-lemmas if_simps = if_x_Not if_Not_x if_cancel if_True if_False if_bool_simps
-
-lemmas seqr = eq_reflection [where x = "size w", standard]
-
-lemmas tl_Nil = tl.simps (1)
-lemmas tl_Cons = tl.simps (2)
-
-
-subsection "Repeated splitting or concatenation"
-
-lemma sclem:
- "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 =
- bin_cat x (size xs * n) (foldl (%u. bin_cat u n) y xs)"
- apply (induct xs)
- apply simp
- apply clarify
- apply (simp (no_asm))
- apply (frule asm_rl)
- apply (drule spec)
- apply (erule trans)
- apply (drule_tac x = "bin_cat y n a" in spec)
- apply (simp add : bin_cat_assoc_sym min_max.inf_absorb2)
- done
-
-lemma bin_rcat_bl:
- "(bin_rcat n wl) = bl_to_bin (concat (map (bin_to_bl n) wl))"
- apply (unfold bin_rcat_def)
- apply (rule sym)
- apply (induct wl)
- apply (auto simp add : bl_to_bin_append)
- apply (simp add : bl_to_bin_aux_alt sclem)
- apply (simp add : bin_cat_foldl_lem [symmetric])
- done
-
-lemmas bin_rsplit_aux_simps = bin_rsplit_aux.simps bin_rsplitl_aux.simps
-lemmas rsplit_aux_simps = bin_rsplit_aux_simps
-
-lemmas th_if_simp1 = split_if [where P = "op = l",
- THEN iffD1, THEN conjunct1, THEN mp, standard]
-lemmas th_if_simp2 = split_if [where P = "op = l",
- THEN iffD1, THEN conjunct2, THEN mp, standard]
-
-lemmas rsplit_aux_simp1s = rsplit_aux_simps [THEN th_if_simp1]
-
-lemmas rsplit_aux_simp2ls = rsplit_aux_simps [THEN th_if_simp2]
-(* these safe to [simp add] as require calculating m - n *)
-lemmas bin_rsplit_aux_simp2s [simp] = rsplit_aux_simp2ls [unfolded Let_def]
-lemmas rbscl = bin_rsplit_aux_simp2s (2)
-
-lemmas rsplit_aux_0_simps [simp] =
- rsplit_aux_simp1s [OF disjI1] rsplit_aux_simp1s [OF disjI2]
-
-lemma bin_rsplit_aux_append:
- "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 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 = "[]"] =
- bin_rsplit_aux_append bin_rsplitl_aux_append
-
-lemmas rsplit_def_auxs = bin_rsplit_def bin_rsplitl_def
-
-lemmas rsplit_aux_alts = rsplit_aux_apps
- [unfolded append_Nil rsplit_def_auxs [symmetric]]
-
-lemma bin_split_minus: "0 < n ==> bin_split (Suc (n - 1)) w = bin_split n w"
- by auto
-
-lemmas bin_split_minus_simp =
- bin_split.Suc [THEN [2] bin_split_minus [symmetric, THEN trans], standard]
-
-lemma bin_split_pred_simp [simp]:
- "(0::nat) < number_of bin \<Longrightarrow>
- bin_split (number_of bin) w =
- (let (w1, w2) = bin_split (number_of (Int.pred bin)) (bin_rest w)
- 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
- then bs
- else let (a, b) = bin_split n c in bin_rsplit n (m - n, a) @ b # bs)"
- 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
- bin_rsplit_aux_simp_alt, standard]
-
-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)
- 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
-
-lemmas bin_rsplit_size_sign = bin_rsplit_size_sign' [OF asm_rl
- rev_rev_ident [THEN trans] set_rev [THEN equalityD2 [THEN subsetD]],
- standard]
-
-lemma bin_nth_rsplit [rule_format] :
- "n > 0 ==> m < n ==> (ALL w k nw. rev sw = bin_rsplit n (nw, w) -->
- k < size sw --> bin_nth (sw ! k) m = bin_nth w (k * n + m))"
- apply (induct sw)
- apply clarsimp
- apply clarsimp
- apply (drule bthrs)
- apply (simp (no_asm_use) add: Let_def split: ls_splits)
- apply clarify
- apply (erule allE, erule impE, erule exI)
- apply (case_tac k)
- apply clarsimp
- prefer 2
- apply clarsimp
- apply (erule allE)
- apply (erule (1) impE)
- apply (drule bin_nth_split, erule conjE, erule allE,
- erule trans, simp add : add_ac)+
- done
-
-lemma bin_rsplit_all:
- "0 < nw ==> nw <= n ==> bin_rsplit n (nw, w) = [bintrunc n w]"
- unfolding bin_rsplit_def
- by (clarsimp dest!: split_bintrunc simp: rsplit_aux_simp2ls split: ls_splits)
-
-lemma bin_rsplit_l [rule_format] :
- "ALL bin. bin_rsplitl n (m, bin) = bin_rsplit n (m, bintrunc m bin)"
- apply (rule_tac a = "m" in wf_less_than [THEN wf_induct])
- apply (simp (no_asm) add : bin_rsplitl_def bin_rsplit_def)
- apply (rule allI)
- apply (subst bin_rsplitl_aux.simps)
- apply (subst bin_rsplit_aux.simps)
- apply (clarsimp simp: Let_def split: ls_splits)
- apply (drule bin_split_trunc)
- apply (drule sym [THEN trans], assumption)
- 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 (subst rsplit_aux_alts)
- unfolding bin_split_cat
- apply simp
- done
-
-lemma bin_rsplit_aux_len_le [rule_format] :
- "\<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)
- done
-
-lemma bin_rsplit_len_le:
- "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) =
- (nw + n - 1) div n + length cs"
- 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)
- apply (case_tac m)
- apply simp
- apply (case_tac "m <= n")
- apply auto
- done
-
-lemma bin_rsplit_len:
- "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:
- "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 using `length bs = length cs` 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
-
-end
--- a/src/HOL/Word/BinGeneral.thy Wed Jun 30 16:41:03 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,938 +0,0 @@
-(*
- Author: Jeremy Dawson, NICTA
-
- contains basic definition to do with integers
- expressed using Pls, Min, BIT and important resulting theorems,
- in particular, bin_rec and related work
-*)
-
-header {* Basic Definitions for Binary Integers *}
-
-theory BinGeneral
-imports Misc_Numeric Bit
-begin
-
-subsection {* Further properties of numerals *}
-
-definition Bit :: "int \<Rightarrow> bit \<Rightarrow> int" (infixl "BIT" 90) where
- "k BIT b = bit_case 0 1 b + k + k"
-
-lemma BIT_B0_eq_Bit0 [simp]: "w BIT 0 = Int.Bit0 w"
- unfolding Bit_def Bit0_def by simp
-
-lemma BIT_B1_eq_Bit1 [simp]: "w BIT 1 = Int.Bit1 w"
- unfolding Bit_def Bit1_def by simp
-
-lemmas BIT_simps = BIT_B0_eq_Bit0 BIT_B1_eq_Bit1
-
-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 **)
-
-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 = (0::bit) & c = (1::bit))"
- unfolding Bit_def by (auto split: bit.split)
-
-lemma le_Bits:
- "(v BIT b <= w BIT c) = (v < w | v <= w & (b ~= (1::bit) | c ~= (0::bit)))"
- 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 (0::bit) = k + k"
- by (unfold Bit_def) simp
-
-lemma Bit_B1:
- "k BIT (1::bit) = k + k + 1"
- by (unfold Bit_def) simp
-
-lemma Bit_B0_2t: "k BIT (0::bit) = 2 * k"
- by (rule trans, rule Bit_B0) simp
-
-lemma Bit_B1_2t: "k BIT (1::bit) = 2 * k + 1"
- by (rule trans, rule Bit_B1) simp
-
-lemma B_mod_2':
- "X = 2 ==> (w BIT (1::bit)) mod X = 1 & (w BIT (0::bit)) mod X = 0"
- apply (simp (no_asm) only: Bit_B0 Bit_B1)
- apply (simp add: z1pmod2)
- done
-
-lemma B1_mod_2 [simp]: "(Int.Bit1 w) mod 2 = 1"
- unfolding numeral_simps number_of_is_id by (simp add: z1pmod2)
-
-lemma B0_mod_2 [simp]: "(Int.Bit0 w) mod 2 = 0"
- unfolding numeral_simps number_of_is_id by simp
-
-lemma neB1E [elim!]:
- assumes ne: "y \<noteq> (1::bit)"
- assumes y: "y = (0::bit) \<Longrightarrow> P"
- shows "P"
- apply (rule y)
- apply (cases y rule: bit.exhaust, simp)
- apply (simp add: ne)
- done
-
-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_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
-
-
-subsection {* Destructors for binary integers *}
-
-definition bin_last :: "int \<Rightarrow> bit" where
- "bin_last w = (if w mod 2 = 0 then (0::bit) else (1::bit))"
-
-definition bin_rest :: "int \<Rightarrow> int" where
- "bin_rest w = w div 2"
-
-definition bin_rl :: "int \<Rightarrow> int \<times> bit" where
- "bin_rl w = (bin_rest w, bin_last w)"
-
-lemma bin_rl_char: "bin_rl w = (r, l) \<longleftrightarrow> r BIT l = w"
- apply (cases l)
- apply (auto simp add: bin_rl_def bin_last_def bin_rest_def)
- unfolding Pls_def Min_def Bit0_def Bit1_def number_of_is_id
- apply arith+
- done
-
-primrec bin_nth where
- Z: "bin_nth w 0 = (bin_last w = (1::bit))"
- | Suc: "bin_nth w (Suc n) = bin_nth (bin_rest w) n"
-
-lemma bin_rl_simps [simp]:
- "bin_rl Int.Pls = (Int.Pls, (0::bit))"
- "bin_rl Int.Min = (Int.Min, (1::bit))"
- "bin_rl (Int.Bit0 r) = (r, (0::bit))"
- "bin_rl (Int.Bit1 r) = (r, (1::bit))"
- "bin_rl (r BIT b) = (r, b)"
- unfolding bin_rl_char by simp_all
-
-lemma bin_rl_simp [simp]:
- "bin_rest w BIT bin_last w = w"
- by (simp add: iffD1 [OF bin_rl_char bin_rl_def])
-
-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"
- "bin_rest (Int.Bit0 w) = w"
- "bin_rest (Int.Bit1 w) = w"
- "bin_rest (w BIT b) = w"
- using bin_rl_simps bin_rl_def by auto
-
-lemma bin_last_simps [simp]:
- "bin_last Int.Pls = (0::bit)"
- "bin_last Int.Min = (1::bit)"
- "bin_last (Int.Bit0 w) = (0::bit)"
- "bin_last (Int.Bit1 w) = (1::bit)"
- "bin_last (w BIT b) = b"
- using bin_rl_simps bin_rl_def by auto
-
-lemma bin_r_l_extras [simp]:
- "bin_last 0 = (0::bit)"
- "bin_last (- 1) = (1::bit)"
- "bin_last -1 = (1::bit)"
- "bin_last 1 = (1::bit)"
- "bin_rest 1 = 0"
- "bin_rest 0 = 0"
- "bin_rest (- 1) = - 1"
- "bin_rest -1 = -1"
- by (simp_all add: bin_last_def bin_rest_def)
-
-lemma bin_last_mod:
- "bin_last w = (if w mod 2 = 0 then (0::bit) else (1::bit))"
- apply (case_tac w rule: bin_exhaust)
- apply (case_tac b)
- apply auto
- done
-
-lemma bin_rest_div:
- "bin_rest w = w div 2"
- apply (case_tac w rule: bin_exhaust)
- apply (rule trans)
- apply clarsimp
- apply (rule refl)
- apply (drule trans)
- apply (rule Bit_def)
- apply (simp add: z1pdiv2 split: bit.split)
- done
-
-lemma Bit_div2 [simp]: "(w BIT b) div 2 = w"
- unfolding bin_rest_div [symmetric] by auto
-
-lemma Bit0_div2 [simp]: "(Int.Bit0 w) div 2 = w"
- using Bit_div2 [where b="(0::bit)"] by simp
-
-lemma Bit1_div2 [simp]: "(Int.Bit1 w) div 2 = w"
- using Bit_div2 [where b="(1::bit)"] by simp
-
-lemma bin_nth_lem [rule_format]:
- "ALL y. bin_nth x = bin_nth y --> x = y"
- apply (induct x rule: bin_induct)
- apply safe
- apply (erule rev_mp)
- apply (induct_tac y rule: bin_induct)
- apply (safe del: subset_antisym)
- apply (drule_tac x=0 in fun_cong, force)
- apply (erule notE, rule ext,
- drule_tac x="Suc x" in fun_cong, force)
- apply (drule_tac x=0 in fun_cong, force)
- apply (erule rev_mp)
- apply (induct_tac y rule: bin_induct)
- apply (safe del: subset_antisym)
- apply (drule_tac x=0 in fun_cong, force)
- apply (erule notE, rule ext,
- drule_tac x="Suc x" in fun_cong, force)
- apply (drule_tac x=0 in fun_cong, force)
- apply (case_tac y rule: bin_exhaust)
- apply clarify
- apply (erule allE)
- apply (erule impE)
- prefer 2
- apply (erule BIT_eqI)
- apply (drule_tac x=0 in fun_cong, force)
- apply (rule ext)
- apply (drule_tac x="Suc ?x" in fun_cong, force)
- done
-
-lemma bin_nth_eq_iff: "(bin_nth x = bin_nth y) = (x = y)"
- by (auto elim: bin_nth_lem)
-
-lemmas bin_eqI = ext [THEN bin_nth_eq_iff [THEN iffD1], standard]
-
-lemma bin_nth_Pls [simp]: "~ bin_nth Int.Pls n"
- by (induct n) auto
-
-lemma bin_nth_Min [simp]: "bin_nth Int.Min n"
- by (induct n) auto
-
-lemma bin_nth_0_BIT: "bin_nth (w BIT b) 0 = (b = (1::bit))"
- by auto
-
-lemma bin_nth_Suc_BIT: "bin_nth (w BIT b) (Suc n) = bin_nth w n"
- by auto
-
-lemma bin_nth_minus [simp]: "0 < n ==> bin_nth (w BIT b) n = bin_nth w (n - 1)"
- by (cases n) auto
-
-lemma bin_nth_minus_Bit0 [simp]:
- "0 < n ==> bin_nth (Int.Bit0 w) n = bin_nth w (n - 1)"
- using bin_nth_minus [where b="(0::bit)"] by simp
-
-lemma bin_nth_minus_Bit1 [simp]:
- "0 < n ==> bin_nth (Int.Bit1 w) n = bin_nth w (n - 1)"
- using bin_nth_minus [where b="(1::bit)"] by simp
-
-lemmas bin_nth_0 = bin_nth.simps(1)
-lemmas bin_nth_Suc = bin_nth.simps(2)
-
-lemmas bin_nth_simps =
- 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 (auto simp add: bin_rl_def bin_last_def bin_rest_def)
- unfolding Pls_def Min_def Bit0_def Bit1_def number_of_is_id
- 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 (0::bit) f1 = f1 \<Longrightarrow>
- bin_rec f1 f2 f3 (Int.Bit0 w) = f3 w (0::bit) (bin_rec f1 f2 f3 w)"
- by (simp add: bin_rec_Pls bin_rec.simps [of _ _ _ "Int.Bit0 w"])
-
-lemma bin_rec_Bit1:
- "f3 Int.Min (1::bit) f2 = f2 \<Longrightarrow>
- bin_rec f1 f2 f3 (Int.Bit1 w) = f3 w (1::bit) (bin_rec f1 f2 f3 w)"
- by (simp add: bin_rec_Min bin_rec.simps [of _ _ _ "Int.Bit1 w"])
-
-lemma bin_rec_Bit:
- "f = bin_rec f1 f2 f3 ==> f3 Int.Pls (0::bit) f1 = f1 ==>
- f3 Int.Min (1::bit) 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 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]
-
-lemma bin_sign_rest [simp]:
- "bin_sign (bin_rest w) = (bin_sign w)"
- by (cases w rule: bin_exhaust) auto
-
-consts
- bintrunc :: "nat => int => int"
-primrec
- Z : "bintrunc 0 bin = Int.Pls"
- Suc : "bintrunc (Suc n) bin = bintrunc n (bin_rest bin) BIT (bin_last bin)"
-
-consts
- sbintrunc :: "nat => int => int"
-primrec
- Z : "sbintrunc 0 bin =
- (case bin_last bin of (1::bit) => Int.Min | (0::bit) => Int.Pls)"
- Suc : "sbintrunc (Suc n) bin = sbintrunc n (bin_rest bin) BIT (bin_last bin)"
-
-lemma sign_bintr:
- "!!w. bin_sign (bintrunc n w) = Int.Pls"
- by (induct n) auto
-
-lemma bintrunc_mod2p:
- "!!w. bintrunc n w = (w mod 2 ^ n :: int)"
- apply (induct n, clarsimp)
- apply (simp add: bin_last_mod bin_rest_div Bit_def zmod_zmult2_eq
- cong: number_of_False_cong)
- done
-
-lemma sbintrunc_mod2p:
- "!!w. sbintrunc n w = ((w + 2 ^ n) mod 2 ^ (Suc n) - 2 ^ n :: int)"
- apply (induct n)
- apply clarsimp
- apply (subst mod_add_left_eq)
- apply (simp add: bin_last_mod)
- apply (simp add: number_of_eq)
- apply clarsimp
- apply (simp add: bin_last_mod bin_rest_div Bit_def
- cong: number_of_False_cong)
- apply (clarsimp simp: mod_mult_mult1 [symmetric]
- zmod_zdiv_equality [THEN diff_eq_eq [THEN iffD2 [THEN sym]]])
- apply (rule trans [symmetric, OF _ emep1])
- apply auto
- apply (auto simp: even_def)
- done
-
-subsection "Simplifications for (s)bintrunc"
-
-lemma bit_bool:
- "(b = (b' = (1::bit))) = (b' = (if b then (1::bit) else (0::bit)))"
- by (cases b') auto
-
-lemmas bit_bool1 [simp] = refl [THEN bit_bool [THEN iffD1], symmetric]
-
-lemma bin_sign_lem:
- "!!bin. (bin_sign (sbintrunc n bin) = Int.Min) = bin_nth bin n"
- apply (induct n)
- apply (case_tac bin rule: bin_exhaust, case_tac b, auto)+
- done
-
-lemma nth_bintr:
- "!!w m. bin_nth (bintrunc m w) n = (n < m & bin_nth w n)"
- apply (induct n)
- apply (case_tac m, auto)[1]
- apply (case_tac m, auto)[1]
- done
-
-lemma nth_sbintr:
- "!!w m. bin_nth (sbintrunc m w) n =
- (if n < m then bin_nth w n else bin_nth w m)"
- apply (induct n)
- apply (case_tac m, simp_all split: bit.splits)[1]
- apply (case_tac m, simp_all split: bit.splits)[1]
- done
-
-lemma bin_nth_Bit:
- "bin_nth (w BIT b) n = (n = 0 & b = (1::bit) | (EX m. n = Suc m & bin_nth w m))"
- by (cases n) auto
-
-lemma bin_nth_Bit0:
- "bin_nth (Int.Bit0 w) n = (EX m. n = Suc m & bin_nth w m)"
- using bin_nth_Bit [where b="(0::bit)"] by simp
-
-lemma bin_nth_Bit1:
- "bin_nth (Int.Bit1 w) n = (n = 0 | (EX m. n = Suc m & bin_nth w m))"
- using bin_nth_Bit [where b="(1::bit)"] by simp
-
-lemma bintrunc_bintrunc_l:
- "n <= m ==> (bintrunc m (bintrunc n w) = bintrunc n w)"
- by (rule bin_eqI) (auto simp add : nth_bintr)
-
-lemma sbintrunc_sbintrunc_l:
- "n <= m ==> (sbintrunc m (sbintrunc n w) = sbintrunc n w)"
- by (rule bin_eqI) (auto simp: nth_sbintr)
-
-lemma bintrunc_bintrunc_ge:
- "n <= m ==> (bintrunc n (bintrunc m w) = bintrunc n w)"
- by (rule bin_eqI) (auto simp: nth_bintr)
-
-lemma bintrunc_bintrunc_min [simp]:
- "bintrunc m (bintrunc n w) = bintrunc (min m n) w"
- apply (rule bin_eqI)
- apply (auto simp: nth_bintr)
- done
-
-lemma sbintrunc_sbintrunc_min [simp]:
- "sbintrunc m (sbintrunc n w) = sbintrunc (min m n) w"
- apply (rule bin_eqI)
- apply (auto simp: nth_sbintr min_max.inf_absorb1 min_max.inf_absorb2)
- done
-
-lemmas bintrunc_Pls =
- bintrunc.Suc [where bin="Int.Pls", simplified bin_last_simps bin_rest_simps, standard]
-
-lemmas bintrunc_Min [simp] =
- bintrunc.Suc [where bin="Int.Min", simplified bin_last_simps bin_rest_simps, standard]
-
-lemmas bintrunc_BIT [simp] =
- bintrunc.Suc [where bin="w BIT b", simplified bin_last_simps bin_rest_simps, standard]
-
-lemma bintrunc_Bit0 [simp]:
- "bintrunc (Suc n) (Int.Bit0 w) = Int.Bit0 (bintrunc n w)"
- using bintrunc_BIT [where b="(0::bit)"] by simp
-
-lemma bintrunc_Bit1 [simp]:
- "bintrunc (Suc n) (Int.Bit1 w) = Int.Bit1 (bintrunc n w)"
- using bintrunc_BIT [where b="(1::bit)"] by simp
-
-lemmas bintrunc_Sucs = bintrunc_Pls bintrunc_Min bintrunc_BIT
- bintrunc_Bit0 bintrunc_Bit1
-
-lemmas sbintrunc_Suc_Pls =
- sbintrunc.Suc [where bin="Int.Pls", simplified bin_last_simps bin_rest_simps, standard]
-
-lemmas sbintrunc_Suc_Min =
- sbintrunc.Suc [where bin="Int.Min", simplified bin_last_simps bin_rest_simps, standard]
-
-lemmas sbintrunc_Suc_BIT [simp] =
- sbintrunc.Suc [where bin="w BIT b", simplified bin_last_simps bin_rest_simps, standard]
-
-lemma sbintrunc_Suc_Bit0 [simp]:
- "sbintrunc (Suc n) (Int.Bit0 w) = Int.Bit0 (sbintrunc n w)"
- using sbintrunc_Suc_BIT [where b="(0::bit)"] by simp
-
-lemma sbintrunc_Suc_Bit1 [simp]:
- "sbintrunc (Suc n) (Int.Bit1 w) = Int.Bit1 (sbintrunc n w)"
- using sbintrunc_Suc_BIT [where b="(1::bit)"] by simp
-
-lemmas sbintrunc_Sucs = sbintrunc_Suc_Pls sbintrunc_Suc_Min sbintrunc_Suc_BIT
- sbintrunc_Suc_Bit0 sbintrunc_Suc_Bit1
-
-lemmas sbintrunc_Pls =
- sbintrunc.Z [where bin="Int.Pls",
- simplified bin_last_simps bin_rest_simps bit.simps, standard]
-
-lemmas sbintrunc_Min =
- sbintrunc.Z [where bin="Int.Min",
- simplified bin_last_simps bin_rest_simps bit.simps, standard]
-
-lemmas sbintrunc_0_BIT_B0 [simp] =
- sbintrunc.Z [where bin="w BIT (0::bit)",
- simplified bin_last_simps bin_rest_simps bit.simps, standard]
-
-lemmas sbintrunc_0_BIT_B1 [simp] =
- sbintrunc.Z [where bin="w BIT (1::bit)",
- simplified bin_last_simps bin_rest_simps bit.simps, standard]
-
-lemma sbintrunc_0_Bit0 [simp]: "sbintrunc 0 (Int.Bit0 w) = Int.Pls"
- using sbintrunc_0_BIT_B0 by simp
-
-lemma sbintrunc_0_Bit1 [simp]: "sbintrunc 0 (Int.Bit1 w) = Int.Min"
- using sbintrunc_0_BIT_B1 by simp
-
-lemmas sbintrunc_0_simps =
- sbintrunc_Pls sbintrunc_Min sbintrunc_0_BIT_B0 sbintrunc_0_BIT_B1
- sbintrunc_0_Bit0 sbintrunc_0_Bit1
-
-lemmas bintrunc_simps = bintrunc.Z bintrunc_Sucs
-lemmas sbintrunc_simps = sbintrunc_0_simps sbintrunc_Sucs
-
-lemma bintrunc_minus:
- "0 < n ==> bintrunc (Suc (n - 1)) w = bintrunc n w"
- by auto
-
-lemma sbintrunc_minus:
- "0 < n ==> sbintrunc (Suc (n - 1)) w = sbintrunc n w"
- by auto
-
-lemmas bintrunc_minus_simps =
- bintrunc_Sucs [THEN [2] bintrunc_minus [symmetric, THEN trans], standard]
-lemmas sbintrunc_minus_simps =
- sbintrunc_Sucs [THEN [2] sbintrunc_minus [symmetric, THEN trans], standard]
-
-lemma bintrunc_n_Pls [simp]:
- "bintrunc n Int.Pls = Int.Pls"
- by (induct n) auto
-
-lemma sbintrunc_n_PM [simp]:
- "sbintrunc n Int.Pls = Int.Pls"
- "sbintrunc n Int.Min = Int.Min"
- by (induct n) auto
-
-lemmas thobini1 = arg_cong [where f = "%w. w BIT b", standard]
-
-lemmas bintrunc_BIT_I = trans [OF bintrunc_BIT thobini1]
-lemmas bintrunc_Min_I = trans [OF bintrunc_Min thobini1]
-
-lemmas bmsts = bintrunc_minus_simps(1-3) [THEN thobini1 [THEN [2] trans], standard]
-lemmas bintrunc_Pls_minus_I = bmsts(1)
-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 auto
-lemma bintrunc_0_BIT: "bintrunc 0 (w BIT b) = Int.Pls"
- by auto
-
-lemma bintrunc_Suc_lem:
- "bintrunc (Suc n) x = y ==> m = Suc n ==> bintrunc m x = y"
- by auto
-
-lemmas bintrunc_Suc_Ialts =
- bintrunc_Min_I [THEN bintrunc_Suc_lem, standard]
- bintrunc_BIT_I [THEN bintrunc_Suc_lem, standard]
-
-lemmas sbintrunc_BIT_I = trans [OF sbintrunc_Suc_BIT thobini1]
-
-lemmas sbintrunc_Suc_Is =
- sbintrunc_Sucs(1-3) [THEN thobini1 [THEN [2] trans], standard]
-
-lemmas sbintrunc_Suc_minus_Is =
- sbintrunc_minus_simps(1-3) [THEN thobini1 [THEN [2] trans], standard]
-
-lemma sbintrunc_Suc_lem:
- "sbintrunc (Suc n) x = y ==> m = Suc n ==> sbintrunc m x = y"
- by auto
-
-lemmas sbintrunc_Suc_Ialts =
- sbintrunc_Suc_Is [THEN sbintrunc_Suc_lem, standard]
-
-lemma sbintrunc_bintrunc_lt:
- "m > n ==> sbintrunc n (bintrunc m w) = sbintrunc n w"
- by (rule bin_eqI) (auto simp: nth_sbintr nth_bintr)
-
-lemma bintrunc_sbintrunc_le:
- "m <= Suc n ==> bintrunc m (sbintrunc n w) = bintrunc m w"
- apply (rule bin_eqI)
- apply (auto simp: nth_sbintr nth_bintr)
- apply (subgoal_tac "x=n", safe, arith+)[1]
- apply (subgoal_tac "x=n", safe, arith+)[1]
- done
-
-lemmas bintrunc_sbintrunc [simp] = order_refl [THEN bintrunc_sbintrunc_le]
-lemmas sbintrunc_bintrunc [simp] = lessI [THEN sbintrunc_bintrunc_lt]
-lemmas bintrunc_bintrunc [simp] = order_refl [THEN bintrunc_bintrunc_l]
-lemmas sbintrunc_sbintrunc [simp] = order_refl [THEN sbintrunc_sbintrunc_l]
-
-lemma bintrunc_sbintrunc' [simp]:
- "0 < n \<Longrightarrow> bintrunc n (sbintrunc (n - 1) w) = bintrunc n w"
- by (cases n) (auto simp del: bintrunc.Suc)
-
-lemma sbintrunc_bintrunc' [simp]:
- "0 < n \<Longrightarrow> sbintrunc (n - 1) (bintrunc n w) = sbintrunc (n - 1) w"
- by (cases n) (auto simp del: bintrunc.Suc)
-
-lemma bin_sbin_eq_iff:
- "bintrunc (Suc n) x = bintrunc (Suc n) y <->
- sbintrunc n x = sbintrunc n y"
- apply (rule iffI)
- apply (rule box_equals [OF _ sbintrunc_bintrunc sbintrunc_bintrunc])
- apply simp
- apply (rule box_equals [OF _ bintrunc_sbintrunc bintrunc_sbintrunc])
- apply simp
- done
-
-lemma bin_sbin_eq_iff':
- "0 < n \<Longrightarrow> bintrunc n x = bintrunc n y <->
- sbintrunc (n - 1) x = sbintrunc (n - 1) y"
- by (cases n) (simp_all add: bin_sbin_eq_iff del: bintrunc.Suc)
-
-lemmas bintrunc_sbintruncS0 [simp] = bintrunc_sbintrunc' [unfolded One_nat_def]
-lemmas sbintrunc_bintruncS0 [simp] = sbintrunc_bintrunc' [unfolded One_nat_def]
-
-lemmas bintrunc_bintrunc_l' = le_add1 [THEN bintrunc_bintrunc_l]
-lemmas sbintrunc_sbintrunc_l' = le_add1 [THEN sbintrunc_sbintrunc_l]
-
-(* although bintrunc_minus_simps, if added to default simpset,
- tends to get applied where it's not wanted in developing the theories,
- we get a version for when the word length is given literally *)
-
-lemmas nat_non0_gr =
- trans [OF iszero_def [THEN Not_eq_iff [THEN iffD2]] refl, standard]
-
-lemmas bintrunc_pred_simps [simp] =
- bintrunc_minus_simps [of "number_of bin", simplified nobm1, standard]
-
-lemmas sbintrunc_pred_simps [simp] =
- sbintrunc_minus_simps [of "number_of bin", simplified nobm1, standard]
-
-lemma no_bintr_alt:
- "number_of (bintrunc n w) = w mod 2 ^ n"
- by (simp add: number_of_eq bintrunc_mod2p)
-
-lemma no_bintr_alt1: "bintrunc n = (%w. w mod 2 ^ n :: int)"
- by (rule ext) (rule bintrunc_mod2p)
-
-lemma range_bintrunc: "range (bintrunc n) = {i. 0 <= i & i < 2 ^ n}"
- apply (unfold no_bintr_alt1)
- apply (auto simp add: image_iff)
- apply (rule exI)
- apply (auto intro: int_mod_lem [THEN iffD1, symmetric])
- done
-
-lemma no_bintr:
- "number_of (bintrunc n w) = (number_of w mod 2 ^ n :: int)"
- by (simp add : bintrunc_mod2p number_of_eq)
-
-lemma no_sbintr_alt2:
- "sbintrunc n = (%w. (w + 2 ^ n) mod 2 ^ Suc n - 2 ^ n :: int)"
- by (rule ext) (simp add : sbintrunc_mod2p)
-
-lemma no_sbintr:
- "number_of (sbintrunc n w) =
- ((number_of w + 2 ^ n) mod 2 ^ Suc n - 2 ^ n :: int)"
- by (simp add : no_sbintr_alt2 number_of_eq)
-
-lemma range_sbintrunc:
- "range (sbintrunc n) = {i. - (2 ^ n) <= i & i < 2 ^ n}"
- apply (unfold no_sbintr_alt2)
- apply (auto simp add: image_iff eq_diff_eq)
- apply (rule exI)
- apply (auto intro: int_mod_lem [THEN iffD1, symmetric])
- done
-
-lemma sb_inc_lem:
- "(a::int) + 2^k < 0 \<Longrightarrow> a + 2^k + 2^(Suc k) <= (a + 2^k) mod 2^(Suc k)"
- apply (erule int_mod_ge' [where n = "2 ^ (Suc k)" and b = "a + 2 ^ k", simplified zless2p])
- apply (rule TrueI)
- done
-
-lemma sb_inc_lem':
- "(a::int) < - (2^k) \<Longrightarrow> a + 2^k + 2^(Suc k) <= (a + 2^k) mod 2^(Suc k)"
- by (rule sb_inc_lem) simp
-
-lemma sbintrunc_inc:
- "x < - (2^n) ==> x + 2^(Suc n) <= sbintrunc n x"
- unfolding no_sbintr_alt2 by (drule sb_inc_lem') simp
-
-lemma sb_dec_lem:
- "(0::int) <= - (2^k) + a ==> (a + 2^k) mod (2 * 2 ^ k) <= - (2 ^ k) + a"
- by (rule int_mod_le' [where n = "2 ^ (Suc k)" and b = "a + 2 ^ k",
- simplified zless2p, OF _ TrueI, simplified])
-
-lemma sb_dec_lem':
- "(2::int) ^ k <= a ==> (a + 2 ^ k) mod (2 * 2 ^ k) <= - (2 ^ k) + a"
- by (rule iffD1 [OF diff_le_eq', THEN sb_dec_lem, simplified])
-
-lemma sbintrunc_dec:
- "x >= (2 ^ n) ==> x - 2 ^ (Suc n) >= sbintrunc n x"
- unfolding no_sbintr_alt2 by (drule sb_dec_lem') simp
-
-lemmas zmod_uminus' = zmod_uminus [where b="c", standard]
-lemmas zpower_zmod' = zpower_zmod [where m="c" and y="k", standard]
-
-lemmas brdmod1s' [symmetric] =
- mod_add_left_eq mod_add_right_eq
- zmod_zsub_left_eq zmod_zsub_right_eq
- zmod_zmult1_eq zmod_zmult1_eq_rev
-
-lemmas brdmods' [symmetric] =
- zpower_zmod' [symmetric]
- trans [OF mod_add_left_eq mod_add_right_eq]
- trans [OF zmod_zsub_left_eq zmod_zsub_right_eq]
- trans [OF zmod_zmult1_eq zmod_zmult1_eq_rev]
- zmod_uminus' [symmetric]
- mod_add_left_eq [where b = "1::int"]
- zmod_zsub_left_eq [where b = "1"]
-
-lemmas bintr_arith1s =
- brdmod1s' [where c="2^n::int", folded pred_def succ_def bintrunc_mod2p, standard]
-lemmas bintr_ariths =
- brdmods' [where c="2^n::int", folded pred_def succ_def bintrunc_mod2p, standard]
-
-lemmas m2pths = pos_mod_sign pos_mod_bound [OF zless2p, standard]
-
-lemma bintr_ge0: "(0 :: int) <= number_of (bintrunc n w)"
- by (simp add : no_bintr m2pths)
-
-lemma bintr_lt2p: "number_of (bintrunc n w) < (2 ^ n :: int)"
- by (simp add : no_bintr m2pths)
-
-lemma bintr_Min:
- "number_of (bintrunc n Int.Min) = (2 ^ n :: int) - 1"
- by (simp add : no_bintr m1mod2k)
-
-lemma sbintr_ge: "(- (2 ^ n) :: int) <= number_of (sbintrunc n w)"
- by (simp add : no_sbintr m2pths)
-
-lemma sbintr_lt: "number_of (sbintrunc n w) < (2 ^ n :: int)"
- by (simp add : no_sbintr m2pths)
-
-lemma bintrunc_Suc:
- "bintrunc (Suc n) bin = bintrunc n (bin_rest bin) BIT bin_last bin"
- by (case_tac bin rule: bin_exhaust) auto
-
-lemma sign_Pls_ge_0:
- "(bin_sign bin = Int.Pls) = (number_of bin >= (0 :: int))"
- by (induct bin rule: numeral_induct) auto
-
-lemma sign_Min_lt_0:
- "(bin_sign bin = Int.Min) = (number_of bin < (0 :: int))"
- by (induct bin rule: numeral_induct) auto
-
-lemmas sign_Min_neg = trans [OF sign_Min_lt_0 neg_def [symmetric]]
-
-lemma bin_rest_trunc:
- "!!bin. (bin_rest (bintrunc n bin)) = bintrunc (n - 1) (bin_rest bin)"
- by (induct n) auto
-
-lemma bin_rest_power_trunc [rule_format] :
- "(bin_rest ^^ k) (bintrunc n bin) =
- bintrunc (n - k) ((bin_rest ^^ k) bin)"
- by (induct k) (auto simp: bin_rest_trunc)
-
-lemma bin_rest_trunc_i:
- "bintrunc n (bin_rest bin) = bin_rest (bintrunc (Suc n) bin)"
- by auto
-
-lemma bin_rest_strunc:
- "!!bin. bin_rest (sbintrunc (Suc n) bin) = sbintrunc n (bin_rest bin)"
- by (induct n) auto
-
-lemma bintrunc_rest [simp]:
- "!!bin. bintrunc n (bin_rest (bintrunc n bin)) = bin_rest (bintrunc n bin)"
- apply (induct n, simp)
- apply (case_tac bin rule: bin_exhaust)
- apply (auto simp: bintrunc_bintrunc_l)
- done
-
-lemma sbintrunc_rest [simp]:
- "!!bin. sbintrunc n (bin_rest (sbintrunc n bin)) = bin_rest (sbintrunc n bin)"
- apply (induct n, simp)
- apply (case_tac bin rule: bin_exhaust)
- apply (auto simp: bintrunc_bintrunc_l split: bit.splits)
- done
-
-lemma bintrunc_rest':
- "bintrunc n o bin_rest o bintrunc n = bin_rest o bintrunc n"
- by (rule ext) auto
-
-lemma sbintrunc_rest' :
- "sbintrunc n o bin_rest o sbintrunc n = bin_rest o sbintrunc n"
- by (rule ext) auto
-
-lemma rco_lem:
- "f o g o f = g o f ==> f o (g o f) ^^ n = g ^^ n o f"
- apply (rule ext)
- apply (induct_tac n)
- apply (simp_all (no_asm))
- apply (drule fun_cong)
- apply (unfold o_def)
- apply (erule trans)
- apply simp
- done
-
-lemma rco_alt: "(f o g) ^^ n o f = f o (g o f) ^^ n"
- apply (rule ext)
- apply (induct n)
- apply (simp_all add: o_def)
- done
-
-lemmas rco_bintr = bintrunc_rest'
- [THEN rco_lem [THEN fun_cong], unfolded o_def]
-lemmas rco_sbintr = sbintrunc_rest'
- [THEN rco_lem [THEN fun_cong], unfolded o_def]
-
-subsection {* Splitting and concatenation *}
-
-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))"
-
-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 *}
-
-lemma funpow_minus_simp:
- "0 < n \<Longrightarrow> f ^^ n = f \<circ> f ^^ (n - 1)"
- by (cases n) simp_all
-
-lemmas funpow_pred_simp [simp] =
- funpow_minus_simp [of "number_of bin", simplified nobm1, standard]
-
-lemmas replicate_minus_simp =
- trans [OF gen_minus [where f = "%n. replicate n x"] replicate.replicate_Suc,
- standard]
-
-lemmas replicate_pred_simp [simp] =
- replicate_minus_simp [of "number_of bin", simplified nobm1, standard]
-
-lemmas power_Suc_no [simp] = power_Suc [of "number_of a", standard]
-
-lemmas power_minus_simp =
- trans [OF gen_minus [where f = "power f"] power_Suc, standard]
-
-lemmas power_pred_simp =
- power_minus_simp [of "number_of bin", simplified nobm1, standard]
-lemmas power_pred_simp_no [simp] = power_pred_simp [where f= "number_of f", standard]
-
-lemma list_exhaust_size_gt0:
- assumes y: "\<And>a list. y = a # list \<Longrightarrow> P"
- shows "0 < length y \<Longrightarrow> P"
- apply (cases y, simp)
- apply (rule y)
- apply fastsimp
- done
-
-lemma list_exhaust_size_eq0:
- assumes y: "y = [] \<Longrightarrow> P"
- shows "length y = 0 \<Longrightarrow> P"
- apply (cases y)
- apply (rule y, simp)
- apply simp
- done
-
-lemma size_Cons_lem_eq:
- "y = xa # list ==> size y = Suc k ==> size list = k"
- by auto
-
-lemma size_Cons_lem_eq_bin:
- "y = xa # list ==> size y = number_of (Int.succ k) ==>
- size list = number_of k"
- by (auto simp: pred_def succ_def split add : split_if_asm)
-
-lemmas ls_splits =
- prod.split split_split prod.split_asm split_split_asm split_if_asm
-
-lemma not_B1_is_B0: "y \<noteq> (1::bit) \<Longrightarrow> y = (0::bit)"
- by (cases y) auto
-
-lemma B1_ass_B0:
- assumes y: "y = (0::bit) \<Longrightarrow> y = (1::bit)"
- shows "y = (1::bit)"
- apply (rule classical)
- apply (drule not_B1_is_B0)
- apply (erule y)
- done
-
--- "simplifications for specific word lengths"
-lemmas n2s_ths [THEN eq_reflection] = add_2_eq_Suc add_2_eq_Suc'
-
-lemmas s2n_ths = n2s_ths [symmetric]
-
-end
--- a/src/HOL/Word/BinOperations.thy Wed Jun 30 16:41:03 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,638 +0,0 @@
-(*
- Author: Jeremy Dawson and Gerwin Klein, NICTA
-
- definition and basic theorems for bit-wise logical operations
- for integers expressed using Pls, Min, BIT,
- and converting them to and from lists of bools
-*)
-
-header {* Bitwise Operations on Binary Integers *}
-
-theory BinOperations
-imports Bit_Operations BinGeneral
-begin
-
-subsection {* Logical operations *}
-
-text "bit-wise logical operations on the int type"
-
-instantiation int :: bit
-begin
-
-definition
- int_not_def [code del]: "bitNOT = bin_rec Int.Min Int.Pls
- (\<lambda>w b s. s BIT (NOT b))"
-
-definition
- int_and_def [code del]: "bitAND = bin_rec (\<lambda>x. Int.Pls) (\<lambda>y. y)
- (\<lambda>w b s y. s (bin_rest y) BIT (b AND bin_last y))"
-
-definition
- int_or_def [code del]: "bitOR = bin_rec (\<lambda>x. x) (\<lambda>y. Int.Min)
- (\<lambda>w b s y. s (bin_rest y) BIT (b OR bin_last y))"
-
-definition
- int_xor_def [code del]: "bitXOR = bin_rec (\<lambda>x. x) bitNOT
- (\<lambda>w b s y. s (bin_rest y) BIT (b XOR bin_last y))"
-
-instance ..
-
-end
-
-lemma int_not_simps [simp]:
- "NOT Int.Pls = Int.Min"
- "NOT Int.Min = Int.Pls"
- "NOT (Int.Bit0 w) = Int.Bit1 (NOT w)"
- "NOT (Int.Bit1 w) = Int.Bit0 (NOT w)"
- "NOT (w BIT b) = (NOT w) BIT (NOT b)"
- unfolding int_not_def by (simp_all add: bin_rec_simps)
-
-declare int_not_simps(1-4) [code]
-
-lemma int_xor_Pls [simp, code]:
- "Int.Pls XOR x = x"
- unfolding int_xor_def by (simp add: bin_rec_PM)
-
-lemma int_xor_Min [simp, code]:
- "Int.Min XOR x = NOT x"
- unfolding int_xor_def by (simp add: bin_rec_PM)
-
-lemma int_xor_Bits [simp]:
- "(x BIT b) XOR (y BIT c) = (x XOR y) BIT (b XOR c)"
- apply (unfold int_xor_def)
- apply (rule bin_rec_simps (1) [THEN fun_cong, THEN trans])
- apply (rule ext, simp)
- prefer 2
- apply simp
- apply (rule ext)
- apply (simp add: int_not_simps [symmetric])
- done
-
-lemma int_xor_Bits2 [simp, code]:
- "(Int.Bit0 x) XOR (Int.Bit0 y) = Int.Bit0 (x XOR y)"
- "(Int.Bit0 x) XOR (Int.Bit1 y) = Int.Bit1 (x XOR y)"
- "(Int.Bit1 x) XOR (Int.Bit0 y) = Int.Bit1 (x XOR y)"
- "(Int.Bit1 x) XOR (Int.Bit1 y) = Int.Bit0 (x XOR y)"
- unfolding BIT_simps [symmetric] int_xor_Bits by simp_all
-
-lemma int_xor_x_simps':
- "w XOR (Int.Pls BIT 0) = w"
- "w XOR (Int.Min BIT 1) = NOT w"
- apply (induct w rule: bin_induct)
- apply simp_all[4]
- apply (unfold int_xor_Bits)
- apply clarsimp+
- done
-
-lemma int_xor_extra_simps [simp, code]:
- "w XOR Int.Pls = w"
- "w XOR Int.Min = NOT w"
- using int_xor_x_simps' by simp_all
-
-lemma int_or_Pls [simp, code]:
- "Int.Pls OR x = x"
- by (unfold int_or_def) (simp add: bin_rec_PM)
-
-lemma int_or_Min [simp, code]:
- "Int.Min OR x = Int.Min"
- by (unfold int_or_def) (simp add: bin_rec_PM)
-
-lemma int_or_Bits [simp]:
- "(x BIT b) OR (y BIT c) = (x OR y) BIT (b OR c)"
- unfolding int_or_def by (simp add: bin_rec_simps)
-
-lemma int_or_Bits2 [simp, code]:
- "(Int.Bit0 x) OR (Int.Bit0 y) = Int.Bit0 (x OR y)"
- "(Int.Bit0 x) OR (Int.Bit1 y) = Int.Bit1 (x OR y)"
- "(Int.Bit1 x) OR (Int.Bit0 y) = Int.Bit1 (x OR y)"
- "(Int.Bit1 x) OR (Int.Bit1 y) = Int.Bit1 (x OR y)"
- unfolding BIT_simps [symmetric] int_or_Bits by simp_all
-
-lemma int_or_x_simps':
- "w OR (Int.Pls BIT 0) = w"
- "w OR (Int.Min BIT 1) = Int.Min"
- apply (induct w rule: bin_induct)
- apply simp_all[4]
- apply (unfold int_or_Bits)
- apply clarsimp+
- done
-
-lemma int_or_extra_simps [simp, code]:
- "w OR Int.Pls = w"
- "w OR Int.Min = Int.Min"
- using int_or_x_simps' by simp_all
-
-lemma int_and_Pls [simp, code]:
- "Int.Pls AND x = Int.Pls"
- unfolding int_and_def by (simp add: bin_rec_PM)
-
-lemma int_and_Min [simp, code]:
- "Int.Min AND x = x"
- unfolding int_and_def by (simp add: bin_rec_PM)
-
-lemma int_and_Bits [simp]:
- "(x BIT b) AND (y BIT c) = (x AND y) BIT (b AND c)"
- unfolding int_and_def by (simp add: bin_rec_simps)
-
-lemma int_and_Bits2 [simp, code]:
- "(Int.Bit0 x) AND (Int.Bit0 y) = Int.Bit0 (x AND y)"
- "(Int.Bit0 x) AND (Int.Bit1 y) = Int.Bit0 (x AND y)"
- "(Int.Bit1 x) AND (Int.Bit0 y) = Int.Bit0 (x AND y)"
- "(Int.Bit1 x) AND (Int.Bit1 y) = Int.Bit1 (x AND y)"
- unfolding BIT_simps [symmetric] int_and_Bits by simp_all
-
-lemma int_and_x_simps':
- "w AND (Int.Pls BIT 0) = Int.Pls"
- "w AND (Int.Min BIT 1) = w"
- apply (induct w rule: bin_induct)
- apply simp_all[4]
- apply (unfold int_and_Bits)
- apply clarsimp+
- done
-
-lemma int_and_extra_simps [simp, code]:
- "w AND Int.Pls = Int.Pls"
- "w AND Int.Min = w"
- using int_and_x_simps' by simp_all
-
-(* commutativity of the above *)
-lemma bin_ops_comm:
- shows
- int_and_comm: "!!y::int. x AND y = y AND x" and
- int_or_comm: "!!y::int. x OR y = y OR x" and
- int_xor_comm: "!!y::int. x XOR y = y XOR x"
- apply (induct x rule: bin_induct)
- apply simp_all[6]
- apply (case_tac y rule: bin_exhaust, simp add: bit_ops_comm)+
- done
-
-lemma bin_ops_same [simp]:
- "(x::int) AND x = x"
- "(x::int) OR x = x"
- "(x::int) XOR x = Int.Pls"
- by (induct x rule: bin_induct) auto
-
-lemma int_not_not [simp]: "NOT (NOT (x::int)) = x"
- by (induct x rule: bin_induct) auto
-
-lemmas bin_log_esimps =
- int_and_extra_simps int_or_extra_simps int_xor_extra_simps
- int_and_Pls int_and_Min int_or_Pls int_or_Min int_xor_Pls int_xor_Min
-
-(* basic properties of logical (bit-wise) operations *)
-
-lemma bbw_ao_absorb:
- "!!y::int. x AND (y OR x) = x & x OR (y AND x) = x"
- apply (induct x rule: bin_induct)
- apply auto
- apply (case_tac [!] y rule: bin_exhaust)
- apply auto
- apply (case_tac [!] bit)
- apply auto
- done
-
-lemma bbw_ao_absorbs_other:
- "x AND (x OR y) = x \<and> (y AND x) OR x = (x::int)"
- "(y OR x) AND x = x \<and> x OR (x AND y) = (x::int)"
- "(x OR y) AND x = x \<and> (x AND y) OR x = (x::int)"
- apply (auto simp: bbw_ao_absorb int_or_comm)
- apply (subst int_or_comm)
- apply (simp add: bbw_ao_absorb)
- apply (subst int_and_comm)
- apply (subst int_or_comm)
- apply (simp add: bbw_ao_absorb)
- apply (subst int_and_comm)
- apply (simp add: bbw_ao_absorb)
- done
-
-lemmas bbw_ao_absorbs [simp] = bbw_ao_absorb bbw_ao_absorbs_other
-
-lemma int_xor_not:
- "!!y::int. (NOT x) XOR y = NOT (x XOR y) &
- x XOR (NOT y) = NOT (x XOR y)"
- apply (induct x rule: bin_induct)
- apply auto
- apply (case_tac y rule: bin_exhaust, auto,
- case_tac b, auto)+
- done
-
-lemma bbw_assocs':
- "!!y z::int. (x AND y) AND z = x AND (y AND z) &
- (x OR y) OR z = x OR (y OR z) &
- (x XOR y) XOR z = x XOR (y XOR z)"
- apply (induct x rule: bin_induct)
- apply (auto simp: int_xor_not)
- apply (case_tac [!] y rule: bin_exhaust)
- apply (case_tac [!] z rule: bin_exhaust)
- apply (case_tac [!] bit)
- apply (case_tac [!] b)
- apply (auto simp del: BIT_simps)
- done
-
-lemma int_and_assoc:
- "(x AND y) AND (z::int) = x AND (y AND z)"
- by (simp add: bbw_assocs')
-
-lemma int_or_assoc:
- "(x OR y) OR (z::int) = x OR (y OR z)"
- by (simp add: bbw_assocs')
-
-lemma int_xor_assoc:
- "(x XOR y) XOR (z::int) = x XOR (y XOR z)"
- by (simp add: bbw_assocs')
-
-lemmas bbw_assocs = int_and_assoc int_or_assoc int_xor_assoc
-
-lemma bbw_lcs [simp]:
- "(y::int) AND (x AND z) = x AND (y AND z)"
- "(y::int) OR (x OR z) = x OR (y OR z)"
- "(y::int) XOR (x XOR z) = x XOR (y XOR z)"
- apply (auto simp: bbw_assocs [symmetric])
- apply (auto simp: bin_ops_comm)
- done
-
-lemma bbw_not_dist:
- "!!y::int. NOT (x OR y) = (NOT x) AND (NOT y)"
- "!!y::int. NOT (x AND y) = (NOT x) OR (NOT y)"
- apply (induct x rule: bin_induct)
- apply auto
- apply (case_tac [!] y rule: bin_exhaust)
- apply (case_tac [!] bit, auto simp del: BIT_simps)
- done
-
-lemma bbw_oa_dist:
- "!!y z::int. (x AND y) OR z =
- (x OR z) AND (y OR z)"
- apply (induct x rule: bin_induct)
- apply auto
- apply (case_tac y rule: bin_exhaust)
- apply (case_tac z rule: bin_exhaust)
- apply (case_tac ba, auto simp del: BIT_simps)
- done
-
-lemma bbw_ao_dist:
- "!!y z::int. (x OR y) AND z =
- (x AND z) OR (y AND z)"
- apply (induct x rule: bin_induct)
- apply auto
- apply (case_tac y rule: bin_exhaust)
- apply (case_tac z rule: bin_exhaust)
- apply (case_tac ba, auto simp del: BIT_simps)
- done
-
-(*
-Why were these declared simp???
-declare bin_ops_comm [simp] bbw_assocs [simp]
-*)
-
-lemma plus_and_or [rule_format]:
- "ALL y::int. (x AND y) + (x OR y) = x + y"
- apply (induct x rule: bin_induct)
- apply clarsimp
- apply clarsimp
- apply clarsimp
- apply (case_tac y rule: bin_exhaust)
- apply clarsimp
- apply (unfold Bit_def)
- apply clarsimp
- apply (erule_tac x = "x" in allE)
- apply (simp split: bit.split)
- done
-
-lemma le_int_or:
- "!!x. bin_sign y = Int.Pls ==> x <= x OR y"
- apply (induct y rule: bin_induct)
- apply clarsimp
- apply clarsimp
- apply (case_tac x rule: bin_exhaust)
- apply (case_tac b)
- apply (case_tac [!] bit)
- apply (auto simp: less_eq_int_code)
- done
-
-lemmas int_and_le =
- xtr3 [OF bbw_ao_absorbs (2) [THEN conjunct2, symmetric] le_int_or] ;
-
-lemma bin_nth_ops:
- "!!x y. bin_nth (x AND y) n = (bin_nth x n & bin_nth y n)"
- "!!x y. bin_nth (x OR y) n = (bin_nth x n | bin_nth y n)"
- "!!x y. bin_nth (x XOR y) n = (bin_nth x n ~= bin_nth y n)"
- "!!x. bin_nth (NOT x) n = (~ bin_nth x n)"
- apply (induct n)
- apply safe
- apply (case_tac [!] x rule: bin_exhaust)
- apply (simp_all del: BIT_simps)
- apply (case_tac [!] y rule: bin_exhaust)
- apply (simp_all del: BIT_simps)
- apply (auto dest: not_B1_is_B0 intro: B1_ass_B0)
- done
-
-(* interaction between bit-wise and arithmetic *)
-(* good example of bin_induction *)
-lemma bin_add_not: "x + NOT x = Int.Min"
- apply (induct x rule: bin_induct)
- apply clarsimp
- apply clarsimp
- apply (case_tac bit, auto)
- done
-
-(* truncating results of bit-wise operations *)
-lemma bin_trunc_ao:
- "!!x y. (bintrunc n x) AND (bintrunc n y) = bintrunc n (x AND y)"
- "!!x y. (bintrunc n x) OR (bintrunc n y) = bintrunc n (x OR y)"
- apply (induct n)
- apply auto
- apply (case_tac [!] x rule: bin_exhaust)
- apply (case_tac [!] y rule: bin_exhaust)
- apply auto
- done
-
-lemma bin_trunc_xor:
- "!!x y. bintrunc n (bintrunc n x XOR bintrunc n y) =
- bintrunc n (x XOR y)"
- apply (induct n)
- apply auto
- apply (case_tac [!] x rule: bin_exhaust)
- apply (case_tac [!] y rule: bin_exhaust)
- apply auto
- done
-
-lemma bin_trunc_not:
- "!!x. bintrunc n (NOT (bintrunc n x)) = bintrunc n (NOT x)"
- apply (induct n)
- apply auto
- apply (case_tac [!] x rule: bin_exhaust)
- apply auto
- done
-
-(* want theorems of the form of bin_trunc_xor *)
-lemma bintr_bintr_i:
- "x = bintrunc n y ==> bintrunc n x = bintrunc n y"
- by auto
-
-lemmas bin_trunc_and = bin_trunc_ao(1) [THEN bintr_bintr_i]
-lemmas bin_trunc_or = bin_trunc_ao(2) [THEN bintr_bintr_i]
-
-subsection {* Setting and clearing bits *}
-
-primrec
- bin_sc :: "nat => bit => int => int"
-where
- Z: "bin_sc 0 b w = bin_rest w BIT b"
- | Suc: "bin_sc (Suc n) b w = bin_sc n b (bin_rest w) BIT bin_last w"
-
-(** nth bit, set/clear **)
-
-lemma bin_nth_sc [simp]:
- "!!w. bin_nth (bin_sc n b w) n = (b = 1)"
- by (induct n) auto
-
-lemma bin_sc_sc_same [simp]:
- "!!w. bin_sc n c (bin_sc n b w) = bin_sc n c w"
- by (induct n) auto
-
-lemma bin_sc_sc_diff:
- "!!w m. m ~= n ==>
- bin_sc m c (bin_sc n b w) = bin_sc n b (bin_sc m c w)"
- apply (induct n)
- apply (case_tac [!] m)
- apply auto
- done
-
-lemma bin_nth_sc_gen:
- "!!w m. bin_nth (bin_sc n b w) m = (if m = n then b = 1 else bin_nth w m)"
- by (induct n) (case_tac [!] m, auto)
-
-lemma bin_sc_nth [simp]:
- "!!w. (bin_sc n (If (bin_nth w n) 1 0) w) = w"
- by (induct n) auto
-
-lemma bin_sign_sc [simp]:
- "!!w. bin_sign (bin_sc n b w) = bin_sign w"
- by (induct n) auto
-
-lemma bin_sc_bintr [simp]:
- "!!w m. bintrunc m (bin_sc n x (bintrunc m (w))) = bintrunc m (bin_sc n x w)"
- apply (induct n)
- apply (case_tac [!] w rule: bin_exhaust)
- apply (case_tac [!] m, auto)
- done
-
-lemma bin_clr_le:
- "!!w. bin_sc n 0 w <= w"
- apply (induct n)
- apply (case_tac [!] w rule: bin_exhaust)
- apply (auto simp del: BIT_simps)
- apply (unfold Bit_def)
- apply (simp_all split: bit.split)
- done
-
-lemma bin_set_ge:
- "!!w. bin_sc n 1 w >= w"
- apply (induct n)
- apply (case_tac [!] w rule: bin_exhaust)
- apply (auto simp del: BIT_simps)
- apply (unfold Bit_def)
- apply (simp_all split: bit.split)
- done
-
-lemma bintr_bin_clr_le:
- "!!w m. bintrunc n (bin_sc m 0 w) <= bintrunc n w"
- apply (induct n)
- apply simp
- apply (case_tac w rule: bin_exhaust)
- apply (case_tac m)
- apply (auto simp del: BIT_simps)
- apply (unfold Bit_def)
- apply (simp_all split: bit.split)
- done
-
-lemma bintr_bin_set_ge:
- "!!w m. bintrunc n (bin_sc m 1 w) >= bintrunc n w"
- apply (induct n)
- apply simp
- apply (case_tac w rule: bin_exhaust)
- apply (case_tac m)
- apply (auto simp del: BIT_simps)
- apply (unfold Bit_def)
- apply (simp_all split: bit.split)
- done
-
-lemma bin_sc_FP [simp]: "bin_sc n 0 Int.Pls = Int.Pls"
- by (induct n) auto
-
-lemma bin_sc_TM [simp]: "bin_sc n 1 Int.Min = Int.Min"
- by (induct n) auto
-
-lemmas bin_sc_simps = bin_sc.Z bin_sc.Suc bin_sc_TM bin_sc_FP
-
-lemma bin_sc_minus:
- "0 < n ==> bin_sc (Suc (n - 1)) b w = bin_sc n b w"
- by auto
-
-lemmas bin_sc_Suc_minus =
- trans [OF bin_sc_minus [symmetric] bin_sc.Suc, standard]
-
-lemmas bin_sc_Suc_pred [simp] =
- bin_sc_Suc_minus [of "number_of bin", simplified nobm1, standard]
-
-
-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"
-
-fun bin_rsplit_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" where
- "bin_rsplit_aux n m c bs =
- (if m = 0 | n = 0 then bs else
- let (a, b) = bin_split n c
- in bin_rsplit_aux n (m - n) a (b # bs))"
-
-definition bin_rsplit :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list" where
- "bin_rsplit n w = bin_rsplit_aux n (fst w) (snd w) []"
-
-fun bin_rsplitl_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" where
- "bin_rsplitl_aux n m c bs =
- (if m = 0 | n = 0 then bs else
- let (a, b) = bin_split (min m n) c
- in bin_rsplitl_aux n (m - n) a (b # bs))"
-
-definition bin_rsplitl :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list" where
- "bin_rsplitl n w = bin_rsplitl_aux n (fst w) (snd w) []"
-
-declare bin_rsplit_aux.simps [simp del]
-declare bin_rsplitl_aux.simps [simp del]
-
-lemma bin_sign_cat:
- "!!y. bin_sign (bin_cat x n y) = bin_sign x"
- by (induct n) auto
-
-lemma bin_cat_Suc_Bit:
- "bin_cat w (Suc n) (v BIT b) = bin_cat w n v BIT b"
- by auto
-
-lemma bin_nth_cat:
- "!!n y. bin_nth (bin_cat x k y) n =
- (if n < k then bin_nth y n else bin_nth x (n - k))"
- apply (induct k)
- apply clarsimp
- apply (case_tac n, auto)
- done
-
-lemma bin_nth_split:
- "!!b c. bin_split n c = (a, b) ==>
- (ALL k. bin_nth a k = bin_nth c (n + k)) &
- (ALL k. bin_nth b k = (k < n & bin_nth c k))"
- apply (induct n)
- apply clarsimp
- apply (clarsimp simp: Let_def split: ls_splits)
- apply (case_tac k)
- apply auto
- done
-
-lemma bin_cat_assoc:
- "!!z. bin_cat (bin_cat x m y) n z = bin_cat x (m + n) (bin_cat y n z)"
- by (induct n) auto
-
-lemma bin_cat_assoc_sym: "!!z m.
- bin_cat x m (bin_cat y n z) = bin_cat (bin_cat x (m - n) y) (min m n) z"
- apply (induct n, clarsimp)
- apply (case_tac m, auto)
- done
-
-lemma bin_cat_Pls [simp]:
- "!!w. bin_cat Int.Pls n w = bintrunc n w"
- by (induct n) auto
-
-lemma bintr_cat1:
- "!!b. bintrunc (k + n) (bin_cat a n b) = bin_cat (bintrunc k a) n b"
- by (induct n) auto
-
-lemma bintr_cat: "bintrunc m (bin_cat a n b) =
- bin_cat (bintrunc (m - n) a) n (bintrunc (min m n) b)"
- by (rule bin_eqI) (auto simp: bin_nth_cat nth_bintr)
-
-lemma bintr_cat_same [simp]:
- "bintrunc n (bin_cat a n b) = bintrunc n b"
- by (auto simp add : bintr_cat)
-
-lemma cat_bintr [simp]:
- "!!b. bin_cat a n (bintrunc n b) = bin_cat a n b"
- by (induct n) auto
-
-lemma split_bintrunc:
- "!!b c. bin_split n c = (a, b) ==> b = bintrunc n c"
- by (induct n) (auto simp: Let_def split: ls_splits)
-
-lemma bin_cat_split:
- "!!v w. bin_split n w = (u, v) ==> w = bin_cat u n v"
- by (induct n) (auto simp: Let_def split: ls_splits)
-
-lemma bin_split_cat:
- "!!w. bin_split n (bin_cat v n w) = (v, bintrunc n w)"
- by (induct n) auto
-
-lemma bin_split_Pls [simp]:
- "bin_split n Int.Pls = (Int.Pls, Int.Pls)"
- by (induct n) (auto simp: Let_def split: ls_splits)
-
-lemma bin_split_Min [simp]:
- "bin_split n Int.Min = (Int.Min, bintrunc n Int.Min)"
- by (induct n) (auto simp: Let_def split: ls_splits)
-
-lemma bin_split_trunc:
- "!!m b c. bin_split (min m n) c = (a, b) ==>
- bin_split n (bintrunc m c) = (bintrunc (m - n) a, b)"
- apply (induct n, clarsimp)
- apply (simp add: bin_rest_trunc Let_def split: ls_splits)
- apply (case_tac m)
- apply (auto simp: Let_def split: ls_splits)
- done
-
-lemma bin_split_trunc1:
- "!!m b c. bin_split n c = (a, b) ==>
- bin_split n (bintrunc m c) = (bintrunc (m - n) a, bintrunc m b)"
- apply (induct n, clarsimp)
- apply (simp add: bin_rest_trunc Let_def split: ls_splits)
- apply (case_tac m)
- apply (auto simp: Let_def split: ls_splits)
- done
-
-lemma bin_cat_num:
- "!!b. bin_cat a n b = a * 2 ^ n + bintrunc n b"
- apply (induct n, clarsimp)
- apply (simp add: Bit_def cong: number_of_False_cong)
- done
-
-lemma bin_split_num:
- "!!b. bin_split n b = (b div 2 ^ n, b mod 2 ^ n)"
- apply (induct n, clarsimp)
- apply (simp add: bin_rest_div zdiv_zmult2_eq)
- apply (case_tac b rule: bin_exhaust)
- apply simp
- apply (simp add: Bit_def mod_mult_mult1 p1mod22k
- split: bit.split
- cong: number_of_False_cong)
- done
-
-subsection {* Miscellaneous lemmas *}
-
-lemma nth_2p_bin:
- "!!m. bin_nth (2 ^ n) m = (m = n)"
- apply (induct n)
- apply clarsimp
- apply safe
- apply (case_tac m)
- apply (auto simp: trans [OF numeral_1_eq_1 [symmetric] number_of_eq])
- apply (case_tac m)
- apply (auto simp: Bit_B0_2t [symmetric])
- done
-
-(* for use when simplifying with bin_nth_Bit *)
-
-lemma ex_eq_or:
- "(EX m. n = Suc m & (m = k | P m)) = (n = Suc k | (EX m. n = Suc m & P m))"
- by auto
-
-end
-
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Word/Bit_Int.thy Wed Jun 30 16:45:47 2010 +0200
@@ -0,0 +1,638 @@
+(*
+ Author: Jeremy Dawson and Gerwin Klein, NICTA
+
+ definition and basic theorems for bit-wise logical operations
+ for integers expressed using Pls, Min, BIT,
+ and converting them to and from lists of bools
+*)
+
+header {* Bitwise Operations on Binary Integers *}
+
+theory Bit_Int
+imports Bit_Representation Bit_Operations
+begin
+
+subsection {* Logical operations *}
+
+text "bit-wise logical operations on the int type"
+
+instantiation int :: bit
+begin
+
+definition
+ int_not_def [code del]: "bitNOT = bin_rec Int.Min Int.Pls
+ (\<lambda>w b s. s BIT (NOT b))"
+
+definition
+ int_and_def [code del]: "bitAND = bin_rec (\<lambda>x. Int.Pls) (\<lambda>y. y)
+ (\<lambda>w b s y. s (bin_rest y) BIT (b AND bin_last y))"
+
+definition
+ int_or_def [code del]: "bitOR = bin_rec (\<lambda>x. x) (\<lambda>y. Int.Min)
+ (\<lambda>w b s y. s (bin_rest y) BIT (b OR bin_last y))"
+
+definition
+ int_xor_def [code del]: "bitXOR = bin_rec (\<lambda>x. x) bitNOT
+ (\<lambda>w b s y. s (bin_rest y) BIT (b XOR bin_last y))"
+
+instance ..
+
+end
+
+lemma int_not_simps [simp]:
+ "NOT Int.Pls = Int.Min"
+ "NOT Int.Min = Int.Pls"
+ "NOT (Int.Bit0 w) = Int.Bit1 (NOT w)"
+ "NOT (Int.Bit1 w) = Int.Bit0 (NOT w)"
+ "NOT (w BIT b) = (NOT w) BIT (NOT b)"
+ unfolding int_not_def by (simp_all add: bin_rec_simps)
+
+declare int_not_simps(1-4) [code]
+
+lemma int_xor_Pls [simp, code]:
+ "Int.Pls XOR x = x"
+ unfolding int_xor_def by (simp add: bin_rec_PM)
+
+lemma int_xor_Min [simp, code]:
+ "Int.Min XOR x = NOT x"
+ unfolding int_xor_def by (simp add: bin_rec_PM)
+
+lemma int_xor_Bits [simp]:
+ "(x BIT b) XOR (y BIT c) = (x XOR y) BIT (b XOR c)"
+ apply (unfold int_xor_def)
+ apply (rule bin_rec_simps (1) [THEN fun_cong, THEN trans])
+ apply (rule ext, simp)
+ prefer 2
+ apply simp
+ apply (rule ext)
+ apply (simp add: int_not_simps [symmetric])
+ done
+
+lemma int_xor_Bits2 [simp, code]:
+ "(Int.Bit0 x) XOR (Int.Bit0 y) = Int.Bit0 (x XOR y)"
+ "(Int.Bit0 x) XOR (Int.Bit1 y) = Int.Bit1 (x XOR y)"
+ "(Int.Bit1 x) XOR (Int.Bit0 y) = Int.Bit1 (x XOR y)"
+ "(Int.Bit1 x) XOR (Int.Bit1 y) = Int.Bit0 (x XOR y)"
+ unfolding BIT_simps [symmetric] int_xor_Bits by simp_all
+
+lemma int_xor_x_simps':
+ "w XOR (Int.Pls BIT 0) = w"
+ "w XOR (Int.Min BIT 1) = NOT w"
+ apply (induct w rule: bin_induct)
+ apply simp_all[4]
+ apply (unfold int_xor_Bits)
+ apply clarsimp+
+ done
+
+lemma int_xor_extra_simps [simp, code]:
+ "w XOR Int.Pls = w"
+ "w XOR Int.Min = NOT w"
+ using int_xor_x_simps' by simp_all
+
+lemma int_or_Pls [simp, code]:
+ "Int.Pls OR x = x"
+ by (unfold int_or_def) (simp add: bin_rec_PM)
+
+lemma int_or_Min [simp, code]:
+ "Int.Min OR x = Int.Min"
+ by (unfold int_or_def) (simp add: bin_rec_PM)
+
+lemma int_or_Bits [simp]:
+ "(x BIT b) OR (y BIT c) = (x OR y) BIT (b OR c)"
+ unfolding int_or_def by (simp add: bin_rec_simps)
+
+lemma int_or_Bits2 [simp, code]:
+ "(Int.Bit0 x) OR (Int.Bit0 y) = Int.Bit0 (x OR y)"
+ "(Int.Bit0 x) OR (Int.Bit1 y) = Int.Bit1 (x OR y)"
+ "(Int.Bit1 x) OR (Int.Bit0 y) = Int.Bit1 (x OR y)"
+ "(Int.Bit1 x) OR (Int.Bit1 y) = Int.Bit1 (x OR y)"
+ unfolding BIT_simps [symmetric] int_or_Bits by simp_all
+
+lemma int_or_x_simps':
+ "w OR (Int.Pls BIT 0) = w"
+ "w OR (Int.Min BIT 1) = Int.Min"
+ apply (induct w rule: bin_induct)
+ apply simp_all[4]
+ apply (unfold int_or_Bits)
+ apply clarsimp+
+ done
+
+lemma int_or_extra_simps [simp, code]:
+ "w OR Int.Pls = w"
+ "w OR Int.Min = Int.Min"
+ using int_or_x_simps' by simp_all
+
+lemma int_and_Pls [simp, code]:
+ "Int.Pls AND x = Int.Pls"
+ unfolding int_and_def by (simp add: bin_rec_PM)
+
+lemma int_and_Min [simp, code]:
+ "Int.Min AND x = x"
+ unfolding int_and_def by (simp add: bin_rec_PM)
+
+lemma int_and_Bits [simp]:
+ "(x BIT b) AND (y BIT c) = (x AND y) BIT (b AND c)"
+ unfolding int_and_def by (simp add: bin_rec_simps)
+
+lemma int_and_Bits2 [simp, code]:
+ "(Int.Bit0 x) AND (Int.Bit0 y) = Int.Bit0 (x AND y)"
+ "(Int.Bit0 x) AND (Int.Bit1 y) = Int.Bit0 (x AND y)"
+ "(Int.Bit1 x) AND (Int.Bit0 y) = Int.Bit0 (x AND y)"
+ "(Int.Bit1 x) AND (Int.Bit1 y) = Int.Bit1 (x AND y)"
+ unfolding BIT_simps [symmetric] int_and_Bits by simp_all
+
+lemma int_and_x_simps':
+ "w AND (Int.Pls BIT 0) = Int.Pls"
+ "w AND (Int.Min BIT 1) = w"
+ apply (induct w rule: bin_induct)
+ apply simp_all[4]
+ apply (unfold int_and_Bits)
+ apply clarsimp+
+ done
+
+lemma int_and_extra_simps [simp, code]:
+ "w AND Int.Pls = Int.Pls"
+ "w AND Int.Min = w"
+ using int_and_x_simps' by simp_all
+
+(* commutativity of the above *)
+lemma bin_ops_comm:
+ shows
+ int_and_comm: "!!y::int. x AND y = y AND x" and
+ int_or_comm: "!!y::int. x OR y = y OR x" and
+ int_xor_comm: "!!y::int. x XOR y = y XOR x"
+ apply (induct x rule: bin_induct)
+ apply simp_all[6]
+ apply (case_tac y rule: bin_exhaust, simp add: bit_ops_comm)+
+ done
+
+lemma bin_ops_same [simp]:
+ "(x::int) AND x = x"
+ "(x::int) OR x = x"
+ "(x::int) XOR x = Int.Pls"
+ by (induct x rule: bin_induct) auto
+
+lemma int_not_not [simp]: "NOT (NOT (x::int)) = x"
+ by (induct x rule: bin_induct) auto
+
+lemmas bin_log_esimps =
+ int_and_extra_simps int_or_extra_simps int_xor_extra_simps
+ int_and_Pls int_and_Min int_or_Pls int_or_Min int_xor_Pls int_xor_Min
+
+(* basic properties of logical (bit-wise) operations *)
+
+lemma bbw_ao_absorb:
+ "!!y::int. x AND (y OR x) = x & x OR (y AND x) = x"
+ apply (induct x rule: bin_induct)
+ apply auto
+ apply (case_tac [!] y rule: bin_exhaust)
+ apply auto
+ apply (case_tac [!] bit)
+ apply auto
+ done
+
+lemma bbw_ao_absorbs_other:
+ "x AND (x OR y) = x \<and> (y AND x) OR x = (x::int)"
+ "(y OR x) AND x = x \<and> x OR (x AND y) = (x::int)"
+ "(x OR y) AND x = x \<and> (x AND y) OR x = (x::int)"
+ apply (auto simp: bbw_ao_absorb int_or_comm)
+ apply (subst int_or_comm)
+ apply (simp add: bbw_ao_absorb)
+ apply (subst int_and_comm)
+ apply (subst int_or_comm)
+ apply (simp add: bbw_ao_absorb)
+ apply (subst int_and_comm)
+ apply (simp add: bbw_ao_absorb)
+ done
+
+lemmas bbw_ao_absorbs [simp] = bbw_ao_absorb bbw_ao_absorbs_other
+
+lemma int_xor_not:
+ "!!y::int. (NOT x) XOR y = NOT (x XOR y) &
+ x XOR (NOT y) = NOT (x XOR y)"
+ apply (induct x rule: bin_induct)
+ apply auto
+ apply (case_tac y rule: bin_exhaust, auto,
+ case_tac b, auto)+
+ done
+
+lemma bbw_assocs':
+ "!!y z::int. (x AND y) AND z = x AND (y AND z) &
+ (x OR y) OR z = x OR (y OR z) &
+ (x XOR y) XOR z = x XOR (y XOR z)"
+ apply (induct x rule: bin_induct)
+ apply (auto simp: int_xor_not)
+ apply (case_tac [!] y rule: bin_exhaust)
+ apply (case_tac [!] z rule: bin_exhaust)
+ apply (case_tac [!] bit)
+ apply (case_tac [!] b)
+ apply (auto simp del: BIT_simps)
+ done
+
+lemma int_and_assoc:
+ "(x AND y) AND (z::int) = x AND (y AND z)"
+ by (simp add: bbw_assocs')
+
+lemma int_or_assoc:
+ "(x OR y) OR (z::int) = x OR (y OR z)"
+ by (simp add: bbw_assocs')
+
+lemma int_xor_assoc:
+ "(x XOR y) XOR (z::int) = x XOR (y XOR z)"
+ by (simp add: bbw_assocs')
+
+lemmas bbw_assocs = int_and_assoc int_or_assoc int_xor_assoc
+
+lemma bbw_lcs [simp]:
+ "(y::int) AND (x AND z) = x AND (y AND z)"
+ "(y::int) OR (x OR z) = x OR (y OR z)"
+ "(y::int) XOR (x XOR z) = x XOR (y XOR z)"
+ apply (auto simp: bbw_assocs [symmetric])
+ apply (auto simp: bin_ops_comm)
+ done
+
+lemma bbw_not_dist:
+ "!!y::int. NOT (x OR y) = (NOT x) AND (NOT y)"
+ "!!y::int. NOT (x AND y) = (NOT x) OR (NOT y)"
+ apply (induct x rule: bin_induct)
+ apply auto
+ apply (case_tac [!] y rule: bin_exhaust)
+ apply (case_tac [!] bit, auto simp del: BIT_simps)
+ done
+
+lemma bbw_oa_dist:
+ "!!y z::int. (x AND y) OR z =
+ (x OR z) AND (y OR z)"
+ apply (induct x rule: bin_induct)
+ apply auto
+ apply (case_tac y rule: bin_exhaust)
+ apply (case_tac z rule: bin_exhaust)
+ apply (case_tac ba, auto simp del: BIT_simps)
+ done
+
+lemma bbw_ao_dist:
+ "!!y z::int. (x OR y) AND z =
+ (x AND z) OR (y AND z)"
+ apply (induct x rule: bin_induct)
+ apply auto
+ apply (case_tac y rule: bin_exhaust)
+ apply (case_tac z rule: bin_exhaust)
+ apply (case_tac ba, auto simp del: BIT_simps)
+ done
+
+(*
+Why were these declared simp???
+declare bin_ops_comm [simp] bbw_assocs [simp]
+*)
+
+lemma plus_and_or [rule_format]:
+ "ALL y::int. (x AND y) + (x OR y) = x + y"
+ apply (induct x rule: bin_induct)
+ apply clarsimp
+ apply clarsimp
+ apply clarsimp
+ apply (case_tac y rule: bin_exhaust)
+ apply clarsimp
+ apply (unfold Bit_def)
+ apply clarsimp
+ apply (erule_tac x = "x" in allE)
+ apply (simp split: bit.split)
+ done
+
+lemma le_int_or:
+ "!!x. bin_sign y = Int.Pls ==> x <= x OR y"
+ apply (induct y rule: bin_induct)
+ apply clarsimp
+ apply clarsimp
+ apply (case_tac x rule: bin_exhaust)
+ apply (case_tac b)
+ apply (case_tac [!] bit)
+ apply (auto simp: less_eq_int_code)
+ done
+
+lemmas int_and_le =
+ xtr3 [OF bbw_ao_absorbs (2) [THEN conjunct2, symmetric] le_int_or] ;
+
+lemma bin_nth_ops:
+ "!!x y. bin_nth (x AND y) n = (bin_nth x n & bin_nth y n)"
+ "!!x y. bin_nth (x OR y) n = (bin_nth x n | bin_nth y n)"
+ "!!x y. bin_nth (x XOR y) n = (bin_nth x n ~= bin_nth y n)"
+ "!!x. bin_nth (NOT x) n = (~ bin_nth x n)"
+ apply (induct n)
+ apply safe
+ apply (case_tac [!] x rule: bin_exhaust)
+ apply (simp_all del: BIT_simps)
+ apply (case_tac [!] y rule: bin_exhaust)
+ apply (simp_all del: BIT_simps)
+ apply (auto dest: not_B1_is_B0 intro: B1_ass_B0)
+ done
+
+(* interaction between bit-wise and arithmetic *)
+(* good example of bin_induction *)
+lemma bin_add_not: "x + NOT x = Int.Min"
+ apply (induct x rule: bin_induct)
+ apply clarsimp
+ apply clarsimp
+ apply (case_tac bit, auto)
+ done
+
+(* truncating results of bit-wise operations *)
+lemma bin_trunc_ao:
+ "!!x y. (bintrunc n x) AND (bintrunc n y) = bintrunc n (x AND y)"
+ "!!x y. (bintrunc n x) OR (bintrunc n y) = bintrunc n (x OR y)"
+ apply (induct n)
+ apply auto
+ apply (case_tac [!] x rule: bin_exhaust)
+ apply (case_tac [!] y rule: bin_exhaust)
+ apply auto
+ done
+
+lemma bin_trunc_xor:
+ "!!x y. bintrunc n (bintrunc n x XOR bintrunc n y) =
+ bintrunc n (x XOR y)"
+ apply (induct n)
+ apply auto
+ apply (case_tac [!] x rule: bin_exhaust)
+ apply (case_tac [!] y rule: bin_exhaust)
+ apply auto
+ done
+
+lemma bin_trunc_not:
+ "!!x. bintrunc n (NOT (bintrunc n x)) = bintrunc n (NOT x)"
+ apply (induct n)
+ apply auto
+ apply (case_tac [!] x rule: bin_exhaust)
+ apply auto
+ done
+
+(* want theorems of the form of bin_trunc_xor *)
+lemma bintr_bintr_i:
+ "x = bintrunc n y ==> bintrunc n x = bintrunc n y"
+ by auto
+
+lemmas bin_trunc_and = bin_trunc_ao(1) [THEN bintr_bintr_i]
+lemmas bin_trunc_or = bin_trunc_ao(2) [THEN bintr_bintr_i]
+
+subsection {* Setting and clearing bits *}
+
+primrec
+ bin_sc :: "nat => bit => int => int"
+where
+ Z: "bin_sc 0 b w = bin_rest w BIT b"
+ | Suc: "bin_sc (Suc n) b w = bin_sc n b (bin_rest w) BIT bin_last w"
+
+(** nth bit, set/clear **)
+
+lemma bin_nth_sc [simp]:
+ "!!w. bin_nth (bin_sc n b w) n = (b = 1)"
+ by (induct n) auto
+
+lemma bin_sc_sc_same [simp]:
+ "!!w. bin_sc n c (bin_sc n b w) = bin_sc n c w"
+ by (induct n) auto
+
+lemma bin_sc_sc_diff:
+ "!!w m. m ~= n ==>
+ bin_sc m c (bin_sc n b w) = bin_sc n b (bin_sc m c w)"
+ apply (induct n)
+ apply (case_tac [!] m)
+ apply auto
+ done
+
+lemma bin_nth_sc_gen:
+ "!!w m. bin_nth (bin_sc n b w) m = (if m = n then b = 1 else bin_nth w m)"
+ by (induct n) (case_tac [!] m, auto)
+
+lemma bin_sc_nth [simp]:
+ "!!w. (bin_sc n (If (bin_nth w n) 1 0) w) = w"
+ by (induct n) auto
+
+lemma bin_sign_sc [simp]:
+ "!!w. bin_sign (bin_sc n b w) = bin_sign w"
+ by (induct n) auto
+
+lemma bin_sc_bintr [simp]:
+ "!!w m. bintrunc m (bin_sc n x (bintrunc m (w))) = bintrunc m (bin_sc n x w)"
+ apply (induct n)
+ apply (case_tac [!] w rule: bin_exhaust)
+ apply (case_tac [!] m, auto)
+ done
+
+lemma bin_clr_le:
+ "!!w. bin_sc n 0 w <= w"
+ apply (induct n)
+ apply (case_tac [!] w rule: bin_exhaust)
+ apply (auto simp del: BIT_simps)
+ apply (unfold Bit_def)
+ apply (simp_all split: bit.split)
+ done
+
+lemma bin_set_ge:
+ "!!w. bin_sc n 1 w >= w"
+ apply (induct n)
+ apply (case_tac [!] w rule: bin_exhaust)
+ apply (auto simp del: BIT_simps)
+ apply (unfold Bit_def)
+ apply (simp_all split: bit.split)
+ done
+
+lemma bintr_bin_clr_le:
+ "!!w m. bintrunc n (bin_sc m 0 w) <= bintrunc n w"
+ apply (induct n)
+ apply simp
+ apply (case_tac w rule: bin_exhaust)
+ apply (case_tac m)
+ apply (auto simp del: BIT_simps)
+ apply (unfold Bit_def)
+ apply (simp_all split: bit.split)
+ done
+
+lemma bintr_bin_set_ge:
+ "!!w m. bintrunc n (bin_sc m 1 w) >= bintrunc n w"
+ apply (induct n)
+ apply simp
+ apply (case_tac w rule: bin_exhaust)
+ apply (case_tac m)
+ apply (auto simp del: BIT_simps)
+ apply (unfold Bit_def)
+ apply (simp_all split: bit.split)
+ done
+
+lemma bin_sc_FP [simp]: "bin_sc n 0 Int.Pls = Int.Pls"
+ by (induct n) auto
+
+lemma bin_sc_TM [simp]: "bin_sc n 1 Int.Min = Int.Min"
+ by (induct n) auto
+
+lemmas bin_sc_simps = bin_sc.Z bin_sc.Suc bin_sc_TM bin_sc_FP
+
+lemma bin_sc_minus:
+ "0 < n ==> bin_sc (Suc (n - 1)) b w = bin_sc n b w"
+ by auto
+
+lemmas bin_sc_Suc_minus =
+ trans [OF bin_sc_minus [symmetric] bin_sc.Suc, standard]
+
+lemmas bin_sc_Suc_pred [simp] =
+ bin_sc_Suc_minus [of "number_of bin", simplified nobm1, standard]
+
+
+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"
+
+fun bin_rsplit_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" where
+ "bin_rsplit_aux n m c bs =
+ (if m = 0 | n = 0 then bs else
+ let (a, b) = bin_split n c
+ in bin_rsplit_aux n (m - n) a (b # bs))"
+
+definition bin_rsplit :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list" where
+ "bin_rsplit n w = bin_rsplit_aux n (fst w) (snd w) []"
+
+fun bin_rsplitl_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" where
+ "bin_rsplitl_aux n m c bs =
+ (if m = 0 | n = 0 then bs else
+ let (a, b) = bin_split (min m n) c
+ in bin_rsplitl_aux n (m - n) a (b # bs))"
+
+definition bin_rsplitl :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list" where
+ "bin_rsplitl n w = bin_rsplitl_aux n (fst w) (snd w) []"
+
+declare bin_rsplit_aux.simps [simp del]
+declare bin_rsplitl_aux.simps [simp del]
+
+lemma bin_sign_cat:
+ "!!y. bin_sign (bin_cat x n y) = bin_sign x"
+ by (induct n) auto
+
+lemma bin_cat_Suc_Bit:
+ "bin_cat w (Suc n) (v BIT b) = bin_cat w n v BIT b"
+ by auto
+
+lemma bin_nth_cat:
+ "!!n y. bin_nth (bin_cat x k y) n =
+ (if n < k then bin_nth y n else bin_nth x (n - k))"
+ apply (induct k)
+ apply clarsimp
+ apply (case_tac n, auto)
+ done
+
+lemma bin_nth_split:
+ "!!b c. bin_split n c = (a, b) ==>
+ (ALL k. bin_nth a k = bin_nth c (n + k)) &
+ (ALL k. bin_nth b k = (k < n & bin_nth c k))"
+ apply (induct n)
+ apply clarsimp
+ apply (clarsimp simp: Let_def split: ls_splits)
+ apply (case_tac k)
+ apply auto
+ done
+
+lemma bin_cat_assoc:
+ "!!z. bin_cat (bin_cat x m y) n z = bin_cat x (m + n) (bin_cat y n z)"
+ by (induct n) auto
+
+lemma bin_cat_assoc_sym: "!!z m.
+ bin_cat x m (bin_cat y n z) = bin_cat (bin_cat x (m - n) y) (min m n) z"
+ apply (induct n, clarsimp)
+ apply (case_tac m, auto)
+ done
+
+lemma bin_cat_Pls [simp]:
+ "!!w. bin_cat Int.Pls n w = bintrunc n w"
+ by (induct n) auto
+
+lemma bintr_cat1:
+ "!!b. bintrunc (k + n) (bin_cat a n b) = bin_cat (bintrunc k a) n b"
+ by (induct n) auto
+
+lemma bintr_cat: "bintrunc m (bin_cat a n b) =
+ bin_cat (bintrunc (m - n) a) n (bintrunc (min m n) b)"
+ by (rule bin_eqI) (auto simp: bin_nth_cat nth_bintr)
+
+lemma bintr_cat_same [simp]:
+ "bintrunc n (bin_cat a n b) = bintrunc n b"
+ by (auto simp add : bintr_cat)
+
+lemma cat_bintr [simp]:
+ "!!b. bin_cat a n (bintrunc n b) = bin_cat a n b"
+ by (induct n) auto
+
+lemma split_bintrunc:
+ "!!b c. bin_split n c = (a, b) ==> b = bintrunc n c"
+ by (induct n) (auto simp: Let_def split: ls_splits)
+
+lemma bin_cat_split:
+ "!!v w. bin_split n w = (u, v) ==> w = bin_cat u n v"
+ by (induct n) (auto simp: Let_def split: ls_splits)
+
+lemma bin_split_cat:
+ "!!w. bin_split n (bin_cat v n w) = (v, bintrunc n w)"
+ by (induct n) auto
+
+lemma bin_split_Pls [simp]:
+ "bin_split n Int.Pls = (Int.Pls, Int.Pls)"
+ by (induct n) (auto simp: Let_def split: ls_splits)
+
+lemma bin_split_Min [simp]:
+ "bin_split n Int.Min = (Int.Min, bintrunc n Int.Min)"
+ by (induct n) (auto simp: Let_def split: ls_splits)
+
+lemma bin_split_trunc:
+ "!!m b c. bin_split (min m n) c = (a, b) ==>
+ bin_split n (bintrunc m c) = (bintrunc (m - n) a, b)"
+ apply (induct n, clarsimp)
+ apply (simp add: bin_rest_trunc Let_def split: ls_splits)
+ apply (case_tac m)
+ apply (auto simp: Let_def split: ls_splits)
+ done
+
+lemma bin_split_trunc1:
+ "!!m b c. bin_split n c = (a, b) ==>
+ bin_split n (bintrunc m c) = (bintrunc (m - n) a, bintrunc m b)"
+ apply (induct n, clarsimp)
+ apply (simp add: bin_rest_trunc Let_def split: ls_splits)
+ apply (case_tac m)
+ apply (auto simp: Let_def split: ls_splits)
+ done
+
+lemma bin_cat_num:
+ "!!b. bin_cat a n b = a * 2 ^ n + bintrunc n b"
+ apply (induct n, clarsimp)
+ apply (simp add: Bit_def cong: number_of_False_cong)
+ done
+
+lemma bin_split_num:
+ "!!b. bin_split n b = (b div 2 ^ n, b mod 2 ^ n)"
+ apply (induct n, clarsimp)
+ apply (simp add: bin_rest_div zdiv_zmult2_eq)
+ apply (case_tac b rule: bin_exhaust)
+ apply simp
+ apply (simp add: Bit_def mod_mult_mult1 p1mod22k
+ split: bit.split
+ cong: number_of_False_cong)
+ done
+
+subsection {* Miscellaneous lemmas *}
+
+lemma nth_2p_bin:
+ "!!m. bin_nth (2 ^ n) m = (m = n)"
+ apply (induct n)
+ apply clarsimp
+ apply safe
+ apply (case_tac m)
+ apply (auto simp: trans [OF numeral_1_eq_1 [symmetric] number_of_eq])
+ apply (case_tac m)
+ apply (auto simp: Bit_B0_2t [symmetric])
+ done
+
+(* for use when simplifying with bin_nth_Bit *)
+
+lemma ex_eq_or:
+ "(EX m. n = Suc m & (m = k | P m)) = (n = Suc k | (EX m. n = Suc m & P m))"
+ by auto
+
+end
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Word/Bit_Representation.thy Wed Jun 30 16:45:47 2010 +0200
@@ -0,0 +1,938 @@
+(*
+ Author: Jeremy Dawson, NICTA
+
+ contains basic definition to do with integers
+ expressed using Pls, Min, BIT and important resulting theorems,
+ in particular, bin_rec and related work
+*)
+
+header {* Basic Definitions for Binary Integers *}
+
+theory Bit_Representation
+imports Misc_Numeric Bit
+begin
+
+subsection {* Further properties of numerals *}
+
+definition Bit :: "int \<Rightarrow> bit \<Rightarrow> int" (infixl "BIT" 90) where
+ "k BIT b = bit_case 0 1 b + k + k"
+
+lemma BIT_B0_eq_Bit0 [simp]: "w BIT 0 = Int.Bit0 w"
+ unfolding Bit_def Bit0_def by simp
+
+lemma BIT_B1_eq_Bit1 [simp]: "w BIT 1 = Int.Bit1 w"
+ unfolding Bit_def Bit1_def by simp
+
+lemmas BIT_simps = BIT_B0_eq_Bit0 BIT_B1_eq_Bit1
+
+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 **)
+
+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 = (0::bit) & c = (1::bit))"
+ unfolding Bit_def by (auto split: bit.split)
+
+lemma le_Bits:
+ "(v BIT b <= w BIT c) = (v < w | v <= w & (b ~= (1::bit) | c ~= (0::bit)))"
+ 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 (0::bit) = k + k"
+ by (unfold Bit_def) simp
+
+lemma Bit_B1:
+ "k BIT (1::bit) = k + k + 1"
+ by (unfold Bit_def) simp
+
+lemma Bit_B0_2t: "k BIT (0::bit) = 2 * k"
+ by (rule trans, rule Bit_B0) simp
+
+lemma Bit_B1_2t: "k BIT (1::bit) = 2 * k + 1"
+ by (rule trans, rule Bit_B1) simp
+
+lemma B_mod_2':
+ "X = 2 ==> (w BIT (1::bit)) mod X = 1 & (w BIT (0::bit)) mod X = 0"
+ apply (simp (no_asm) only: Bit_B0 Bit_B1)
+ apply (simp add: z1pmod2)
+ done
+
+lemma B1_mod_2 [simp]: "(Int.Bit1 w) mod 2 = 1"
+ unfolding numeral_simps number_of_is_id by (simp add: z1pmod2)
+
+lemma B0_mod_2 [simp]: "(Int.Bit0 w) mod 2 = 0"
+ unfolding numeral_simps number_of_is_id by simp
+
+lemma neB1E [elim!]:
+ assumes ne: "y \<noteq> (1::bit)"
+ assumes y: "y = (0::bit) \<Longrightarrow> P"
+ shows "P"
+ apply (rule y)
+ apply (cases y rule: bit.exhaust, simp)
+ apply (simp add: ne)
+ done
+
+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_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
+
+
+subsection {* Destructors for binary integers *}
+
+definition bin_last :: "int \<Rightarrow> bit" where
+ "bin_last w = (if w mod 2 = 0 then (0::bit) else (1::bit))"
+
+definition bin_rest :: "int \<Rightarrow> int" where
+ "bin_rest w = w div 2"
+
+definition bin_rl :: "int \<Rightarrow> int \<times> bit" where
+ "bin_rl w = (bin_rest w, bin_last w)"
+
+lemma bin_rl_char: "bin_rl w = (r, l) \<longleftrightarrow> r BIT l = w"
+ apply (cases l)
+ apply (auto simp add: bin_rl_def bin_last_def bin_rest_def)
+ unfolding Pls_def Min_def Bit0_def Bit1_def number_of_is_id
+ apply arith+
+ done
+
+primrec bin_nth where
+ Z: "bin_nth w 0 = (bin_last w = (1::bit))"
+ | Suc: "bin_nth w (Suc n) = bin_nth (bin_rest w) n"
+
+lemma bin_rl_simps [simp]:
+ "bin_rl Int.Pls = (Int.Pls, (0::bit))"
+ "bin_rl Int.Min = (Int.Min, (1::bit))"
+ "bin_rl (Int.Bit0 r) = (r, (0::bit))"
+ "bin_rl (Int.Bit1 r) = (r, (1::bit))"
+ "bin_rl (r BIT b) = (r, b)"
+ unfolding bin_rl_char by simp_all
+
+lemma bin_rl_simp [simp]:
+ "bin_rest w BIT bin_last w = w"
+ by (simp add: iffD1 [OF bin_rl_char bin_rl_def])
+
+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"
+ "bin_rest (Int.Bit0 w) = w"
+ "bin_rest (Int.Bit1 w) = w"
+ "bin_rest (w BIT b) = w"
+ using bin_rl_simps bin_rl_def by auto
+
+lemma bin_last_simps [simp]:
+ "bin_last Int.Pls = (0::bit)"
+ "bin_last Int.Min = (1::bit)"
+ "bin_last (Int.Bit0 w) = (0::bit)"
+ "bin_last (Int.Bit1 w) = (1::bit)"
+ "bin_last (w BIT b) = b"
+ using bin_rl_simps bin_rl_def by auto
+
+lemma bin_r_l_extras [simp]:
+ "bin_last 0 = (0::bit)"
+ "bin_last (- 1) = (1::bit)"
+ "bin_last -1 = (1::bit)"
+ "bin_last 1 = (1::bit)"
+ "bin_rest 1 = 0"
+ "bin_rest 0 = 0"
+ "bin_rest (- 1) = - 1"
+ "bin_rest -1 = -1"
+ by (simp_all add: bin_last_def bin_rest_def)
+
+lemma bin_last_mod:
+ "bin_last w = (if w mod 2 = 0 then (0::bit) else (1::bit))"
+ apply (case_tac w rule: bin_exhaust)
+ apply (case_tac b)
+ apply auto
+ done
+
+lemma bin_rest_div:
+ "bin_rest w = w div 2"
+ apply (case_tac w rule: bin_exhaust)
+ apply (rule trans)
+ apply clarsimp
+ apply (rule refl)
+ apply (drule trans)
+ apply (rule Bit_def)
+ apply (simp add: z1pdiv2 split: bit.split)
+ done
+
+lemma Bit_div2 [simp]: "(w BIT b) div 2 = w"
+ unfolding bin_rest_div [symmetric] by auto
+
+lemma Bit0_div2 [simp]: "(Int.Bit0 w) div 2 = w"
+ using Bit_div2 [where b="(0::bit)"] by simp
+
+lemma Bit1_div2 [simp]: "(Int.Bit1 w) div 2 = w"
+ using Bit_div2 [where b="(1::bit)"] by simp
+
+lemma bin_nth_lem [rule_format]:
+ "ALL y. bin_nth x = bin_nth y --> x = y"
+ apply (induct x rule: bin_induct)
+ apply safe
+ apply (erule rev_mp)
+ apply (induct_tac y rule: bin_induct)
+ apply (safe del: subset_antisym)
+ apply (drule_tac x=0 in fun_cong, force)
+ apply (erule notE, rule ext,
+ drule_tac x="Suc x" in fun_cong, force)
+ apply (drule_tac x=0 in fun_cong, force)
+ apply (erule rev_mp)
+ apply (induct_tac y rule: bin_induct)
+ apply (safe del: subset_antisym)
+ apply (drule_tac x=0 in fun_cong, force)
+ apply (erule notE, rule ext,
+ drule_tac x="Suc x" in fun_cong, force)
+ apply (drule_tac x=0 in fun_cong, force)
+ apply (case_tac y rule: bin_exhaust)
+ apply clarify
+ apply (erule allE)
+ apply (erule impE)
+ prefer 2
+ apply (erule BIT_eqI)
+ apply (drule_tac x=0 in fun_cong, force)
+ apply (rule ext)
+ apply (drule_tac x="Suc ?x" in fun_cong, force)
+ done
+
+lemma bin_nth_eq_iff: "(bin_nth x = bin_nth y) = (x = y)"
+ by (auto elim: bin_nth_lem)
+
+lemmas bin_eqI = ext [THEN bin_nth_eq_iff [THEN iffD1], standard]
+
+lemma bin_nth_Pls [simp]: "~ bin_nth Int.Pls n"
+ by (induct n) auto
+
+lemma bin_nth_Min [simp]: "bin_nth Int.Min n"
+ by (induct n) auto
+
+lemma bin_nth_0_BIT: "bin_nth (w BIT b) 0 = (b = (1::bit))"
+ by auto
+
+lemma bin_nth_Suc_BIT: "bin_nth (w BIT b) (Suc n) = bin_nth w n"
+ by auto
+
+lemma bin_nth_minus [simp]: "0 < n ==> bin_nth (w BIT b) n = bin_nth w (n - 1)"
+ by (cases n) auto
+
+lemma bin_nth_minus_Bit0 [simp]:
+ "0 < n ==> bin_nth (Int.Bit0 w) n = bin_nth w (n - 1)"
+ using bin_nth_minus [where b="(0::bit)"] by simp
+
+lemma bin_nth_minus_Bit1 [simp]:
+ "0 < n ==> bin_nth (Int.Bit1 w) n = bin_nth w (n - 1)"
+ using bin_nth_minus [where b="(1::bit)"] by simp
+
+lemmas bin_nth_0 = bin_nth.simps(1)
+lemmas bin_nth_Suc = bin_nth.simps(2)
+
+lemmas bin_nth_simps =
+ 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 (auto simp add: bin_rl_def bin_last_def bin_rest_def)
+ unfolding Pls_def Min_def Bit0_def Bit1_def number_of_is_id
+ 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 (0::bit) f1 = f1 \<Longrightarrow>
+ bin_rec f1 f2 f3 (Int.Bit0 w) = f3 w (0::bit) (bin_rec f1 f2 f3 w)"
+ by (simp add: bin_rec_Pls bin_rec.simps [of _ _ _ "Int.Bit0 w"])
+
+lemma bin_rec_Bit1:
+ "f3 Int.Min (1::bit) f2 = f2 \<Longrightarrow>
+ bin_rec f1 f2 f3 (Int.Bit1 w) = f3 w (1::bit) (bin_rec f1 f2 f3 w)"
+ by (simp add: bin_rec_Min bin_rec.simps [of _ _ _ "Int.Bit1 w"])
+
+lemma bin_rec_Bit:
+ "f = bin_rec f1 f2 f3 ==> f3 Int.Pls (0::bit) f1 = f1 ==>
+ f3 Int.Min (1::bit) 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 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]
+
+lemma bin_sign_rest [simp]:
+ "bin_sign (bin_rest w) = (bin_sign w)"
+ by (cases w rule: bin_exhaust) auto
+
+consts
+ bintrunc :: "nat => int => int"
+primrec
+ Z : "bintrunc 0 bin = Int.Pls"
+ Suc : "bintrunc (Suc n) bin = bintrunc n (bin_rest bin) BIT (bin_last bin)"
+
+consts
+ sbintrunc :: "nat => int => int"
+primrec
+ Z : "sbintrunc 0 bin =
+ (case bin_last bin of (1::bit) => Int.Min | (0::bit) => Int.Pls)"
+ Suc : "sbintrunc (Suc n) bin = sbintrunc n (bin_rest bin) BIT (bin_last bin)"
+
+lemma sign_bintr:
+ "!!w. bin_sign (bintrunc n w) = Int.Pls"
+ by (induct n) auto
+
+lemma bintrunc_mod2p:
+ "!!w. bintrunc n w = (w mod 2 ^ n :: int)"
+ apply (induct n, clarsimp)
+ apply (simp add: bin_last_mod bin_rest_div Bit_def zmod_zmult2_eq
+ cong: number_of_False_cong)
+ done
+
+lemma sbintrunc_mod2p:
+ "!!w. sbintrunc n w = ((w + 2 ^ n) mod 2 ^ (Suc n) - 2 ^ n :: int)"
+ apply (induct n)
+ apply clarsimp
+ apply (subst mod_add_left_eq)
+ apply (simp add: bin_last_mod)
+ apply (simp add: number_of_eq)
+ apply clarsimp
+ apply (simp add: bin_last_mod bin_rest_div Bit_def
+ cong: number_of_False_cong)
+ apply (clarsimp simp: mod_mult_mult1 [symmetric]
+ zmod_zdiv_equality [THEN diff_eq_eq [THEN iffD2 [THEN sym]]])
+ apply (rule trans [symmetric, OF _ emep1])
+ apply auto
+ apply (auto simp: even_def)
+ done
+
+subsection "Simplifications for (s)bintrunc"
+
+lemma bit_bool:
+ "(b = (b' = (1::bit))) = (b' = (if b then (1::bit) else (0::bit)))"
+ by (cases b') auto
+
+lemmas bit_bool1 [simp] = refl [THEN bit_bool [THEN iffD1], symmetric]
+
+lemma bin_sign_lem:
+ "!!bin. (bin_sign (sbintrunc n bin) = Int.Min) = bin_nth bin n"
+ apply (induct n)
+ apply (case_tac bin rule: bin_exhaust, case_tac b, auto)+
+ done
+
+lemma nth_bintr:
+ "!!w m. bin_nth (bintrunc m w) n = (n < m & bin_nth w n)"
+ apply (induct n)
+ apply (case_tac m, auto)[1]
+ apply (case_tac m, auto)[1]
+ done
+
+lemma nth_sbintr:
+ "!!w m. bin_nth (sbintrunc m w) n =
+ (if n < m then bin_nth w n else bin_nth w m)"
+ apply (induct n)
+ apply (case_tac m, simp_all split: bit.splits)[1]
+ apply (case_tac m, simp_all split: bit.splits)[1]
+ done
+
+lemma bin_nth_Bit:
+ "bin_nth (w BIT b) n = (n = 0 & b = (1::bit) | (EX m. n = Suc m & bin_nth w m))"
+ by (cases n) auto
+
+lemma bin_nth_Bit0:
+ "bin_nth (Int.Bit0 w) n = (EX m. n = Suc m & bin_nth w m)"
+ using bin_nth_Bit [where b="(0::bit)"] by simp
+
+lemma bin_nth_Bit1:
+ "bin_nth (Int.Bit1 w) n = (n = 0 | (EX m. n = Suc m & bin_nth w m))"
+ using bin_nth_Bit [where b="(1::bit)"] by simp
+
+lemma bintrunc_bintrunc_l:
+ "n <= m ==> (bintrunc m (bintrunc n w) = bintrunc n w)"
+ by (rule bin_eqI) (auto simp add : nth_bintr)
+
+lemma sbintrunc_sbintrunc_l:
+ "n <= m ==> (sbintrunc m (sbintrunc n w) = sbintrunc n w)"
+ by (rule bin_eqI) (auto simp: nth_sbintr)
+
+lemma bintrunc_bintrunc_ge:
+ "n <= m ==> (bintrunc n (bintrunc m w) = bintrunc n w)"
+ by (rule bin_eqI) (auto simp: nth_bintr)
+
+lemma bintrunc_bintrunc_min [simp]:
+ "bintrunc m (bintrunc n w) = bintrunc (min m n) w"
+ apply (rule bin_eqI)
+ apply (auto simp: nth_bintr)
+ done
+
+lemma sbintrunc_sbintrunc_min [simp]:
+ "sbintrunc m (sbintrunc n w) = sbintrunc (min m n) w"
+ apply (rule bin_eqI)
+ apply (auto simp: nth_sbintr min_max.inf_absorb1 min_max.inf_absorb2)
+ done
+
+lemmas bintrunc_Pls =
+ bintrunc.Suc [where bin="Int.Pls", simplified bin_last_simps bin_rest_simps, standard]
+
+lemmas bintrunc_Min [simp] =
+ bintrunc.Suc [where bin="Int.Min", simplified bin_last_simps bin_rest_simps, standard]
+
+lemmas bintrunc_BIT [simp] =
+ bintrunc.Suc [where bin="w BIT b", simplified bin_last_simps bin_rest_simps, standard]
+
+lemma bintrunc_Bit0 [simp]:
+ "bintrunc (Suc n) (Int.Bit0 w) = Int.Bit0 (bintrunc n w)"
+ using bintrunc_BIT [where b="(0::bit)"] by simp
+
+lemma bintrunc_Bit1 [simp]:
+ "bintrunc (Suc n) (Int.Bit1 w) = Int.Bit1 (bintrunc n w)"
+ using bintrunc_BIT [where b="(1::bit)"] by simp
+
+lemmas bintrunc_Sucs = bintrunc_Pls bintrunc_Min bintrunc_BIT
+ bintrunc_Bit0 bintrunc_Bit1
+
+lemmas sbintrunc_Suc_Pls =
+ sbintrunc.Suc [where bin="Int.Pls", simplified bin_last_simps bin_rest_simps, standard]
+
+lemmas sbintrunc_Suc_Min =
+ sbintrunc.Suc [where bin="Int.Min", simplified bin_last_simps bin_rest_simps, standard]
+
+lemmas sbintrunc_Suc_BIT [simp] =
+ sbintrunc.Suc [where bin="w BIT b", simplified bin_last_simps bin_rest_simps, standard]
+
+lemma sbintrunc_Suc_Bit0 [simp]:
+ "sbintrunc (Suc n) (Int.Bit0 w) = Int.Bit0 (sbintrunc n w)"
+ using sbintrunc_Suc_BIT [where b="(0::bit)"] by simp
+
+lemma sbintrunc_Suc_Bit1 [simp]:
+ "sbintrunc (Suc n) (Int.Bit1 w) = Int.Bit1 (sbintrunc n w)"
+ using sbintrunc_Suc_BIT [where b="(1::bit)"] by simp
+
+lemmas sbintrunc_Sucs = sbintrunc_Suc_Pls sbintrunc_Suc_Min sbintrunc_Suc_BIT
+ sbintrunc_Suc_Bit0 sbintrunc_Suc_Bit1
+
+lemmas sbintrunc_Pls =
+ sbintrunc.Z [where bin="Int.Pls",
+ simplified bin_last_simps bin_rest_simps bit.simps, standard]
+
+lemmas sbintrunc_Min =
+ sbintrunc.Z [where bin="Int.Min",
+ simplified bin_last_simps bin_rest_simps bit.simps, standard]
+
+lemmas sbintrunc_0_BIT_B0 [simp] =
+ sbintrunc.Z [where bin="w BIT (0::bit)",
+ simplified bin_last_simps bin_rest_simps bit.simps, standard]
+
+lemmas sbintrunc_0_BIT_B1 [simp] =
+ sbintrunc.Z [where bin="w BIT (1::bit)",
+ simplified bin_last_simps bin_rest_simps bit.simps, standard]
+
+lemma sbintrunc_0_Bit0 [simp]: "sbintrunc 0 (Int.Bit0 w) = Int.Pls"
+ using sbintrunc_0_BIT_B0 by simp
+
+lemma sbintrunc_0_Bit1 [simp]: "sbintrunc 0 (Int.Bit1 w) = Int.Min"
+ using sbintrunc_0_BIT_B1 by simp
+
+lemmas sbintrunc_0_simps =
+ sbintrunc_Pls sbintrunc_Min sbintrunc_0_BIT_B0 sbintrunc_0_BIT_B1
+ sbintrunc_0_Bit0 sbintrunc_0_Bit1
+
+lemmas bintrunc_simps = bintrunc.Z bintrunc_Sucs
+lemmas sbintrunc_simps = sbintrunc_0_simps sbintrunc_Sucs
+
+lemma bintrunc_minus:
+ "0 < n ==> bintrunc (Suc (n - 1)) w = bintrunc n w"
+ by auto
+
+lemma sbintrunc_minus:
+ "0 < n ==> sbintrunc (Suc (n - 1)) w = sbintrunc n w"
+ by auto
+
+lemmas bintrunc_minus_simps =
+ bintrunc_Sucs [THEN [2] bintrunc_minus [symmetric, THEN trans], standard]
+lemmas sbintrunc_minus_simps =
+ sbintrunc_Sucs [THEN [2] sbintrunc_minus [symmetric, THEN trans], standard]
+
+lemma bintrunc_n_Pls [simp]:
+ "bintrunc n Int.Pls = Int.Pls"
+ by (induct n) auto
+
+lemma sbintrunc_n_PM [simp]:
+ "sbintrunc n Int.Pls = Int.Pls"
+ "sbintrunc n Int.Min = Int.Min"
+ by (induct n) auto
+
+lemmas thobini1 = arg_cong [where f = "%w. w BIT b", standard]
+
+lemmas bintrunc_BIT_I = trans [OF bintrunc_BIT thobini1]
+lemmas bintrunc_Min_I = trans [OF bintrunc_Min thobini1]
+
+lemmas bmsts = bintrunc_minus_simps(1-3) [THEN thobini1 [THEN [2] trans], standard]
+lemmas bintrunc_Pls_minus_I = bmsts(1)
+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 auto
+lemma bintrunc_0_BIT: "bintrunc 0 (w BIT b) = Int.Pls"
+ by auto
+
+lemma bintrunc_Suc_lem:
+ "bintrunc (Suc n) x = y ==> m = Suc n ==> bintrunc m x = y"
+ by auto
+
+lemmas bintrunc_Suc_Ialts =
+ bintrunc_Min_I [THEN bintrunc_Suc_lem, standard]
+ bintrunc_BIT_I [THEN bintrunc_Suc_lem, standard]
+
+lemmas sbintrunc_BIT_I = trans [OF sbintrunc_Suc_BIT thobini1]
+
+lemmas sbintrunc_Suc_Is =
+ sbintrunc_Sucs(1-3) [THEN thobini1 [THEN [2] trans], standard]
+
+lemmas sbintrunc_Suc_minus_Is =
+ sbintrunc_minus_simps(1-3) [THEN thobini1 [THEN [2] trans], standard]
+
+lemma sbintrunc_Suc_lem:
+ "sbintrunc (Suc n) x = y ==> m = Suc n ==> sbintrunc m x = y"
+ by auto
+
+lemmas sbintrunc_Suc_Ialts =
+ sbintrunc_Suc_Is [THEN sbintrunc_Suc_lem, standard]
+
+lemma sbintrunc_bintrunc_lt:
+ "m > n ==> sbintrunc n (bintrunc m w) = sbintrunc n w"
+ by (rule bin_eqI) (auto simp: nth_sbintr nth_bintr)
+
+lemma bintrunc_sbintrunc_le:
+ "m <= Suc n ==> bintrunc m (sbintrunc n w) = bintrunc m w"
+ apply (rule bin_eqI)
+ apply (auto simp: nth_sbintr nth_bintr)
+ apply (subgoal_tac "x=n", safe, arith+)[1]
+ apply (subgoal_tac "x=n", safe, arith+)[1]
+ done
+
+lemmas bintrunc_sbintrunc [simp] = order_refl [THEN bintrunc_sbintrunc_le]
+lemmas sbintrunc_bintrunc [simp] = lessI [THEN sbintrunc_bintrunc_lt]
+lemmas bintrunc_bintrunc [simp] = order_refl [THEN bintrunc_bintrunc_l]
+lemmas sbintrunc_sbintrunc [simp] = order_refl [THEN sbintrunc_sbintrunc_l]
+
+lemma bintrunc_sbintrunc' [simp]:
+ "0 < n \<Longrightarrow> bintrunc n (sbintrunc (n - 1) w) = bintrunc n w"
+ by (cases n) (auto simp del: bintrunc.Suc)
+
+lemma sbintrunc_bintrunc' [simp]:
+ "0 < n \<Longrightarrow> sbintrunc (n - 1) (bintrunc n w) = sbintrunc (n - 1) w"
+ by (cases n) (auto simp del: bintrunc.Suc)
+
+lemma bin_sbin_eq_iff:
+ "bintrunc (Suc n) x = bintrunc (Suc n) y <->
+ sbintrunc n x = sbintrunc n y"
+ apply (rule iffI)
+ apply (rule box_equals [OF _ sbintrunc_bintrunc sbintrunc_bintrunc])
+ apply simp
+ apply (rule box_equals [OF _ bintrunc_sbintrunc bintrunc_sbintrunc])
+ apply simp
+ done
+
+lemma bin_sbin_eq_iff':
+ "0 < n \<Longrightarrow> bintrunc n x = bintrunc n y <->
+ sbintrunc (n - 1) x = sbintrunc (n - 1) y"
+ by (cases n) (simp_all add: bin_sbin_eq_iff del: bintrunc.Suc)
+
+lemmas bintrunc_sbintruncS0 [simp] = bintrunc_sbintrunc' [unfolded One_nat_def]
+lemmas sbintrunc_bintruncS0 [simp] = sbintrunc_bintrunc' [unfolded One_nat_def]
+
+lemmas bintrunc_bintrunc_l' = le_add1 [THEN bintrunc_bintrunc_l]
+lemmas sbintrunc_sbintrunc_l' = le_add1 [THEN sbintrunc_sbintrunc_l]
+
+(* although bintrunc_minus_simps, if added to default simpset,
+ tends to get applied where it's not wanted in developing the theories,
+ we get a version for when the word length is given literally *)
+
+lemmas nat_non0_gr =
+ trans [OF iszero_def [THEN Not_eq_iff [THEN iffD2]] refl, standard]
+
+lemmas bintrunc_pred_simps [simp] =
+ bintrunc_minus_simps [of "number_of bin", simplified nobm1, standard]
+
+lemmas sbintrunc_pred_simps [simp] =
+ sbintrunc_minus_simps [of "number_of bin", simplified nobm1, standard]
+
+lemma no_bintr_alt:
+ "number_of (bintrunc n w) = w mod 2 ^ n"
+ by (simp add: number_of_eq bintrunc_mod2p)
+
+lemma no_bintr_alt1: "bintrunc n = (%w. w mod 2 ^ n :: int)"
+ by (rule ext) (rule bintrunc_mod2p)
+
+lemma range_bintrunc: "range (bintrunc n) = {i. 0 <= i & i < 2 ^ n}"
+ apply (unfold no_bintr_alt1)
+ apply (auto simp add: image_iff)
+ apply (rule exI)
+ apply (auto intro: int_mod_lem [THEN iffD1, symmetric])
+ done
+
+lemma no_bintr:
+ "number_of (bintrunc n w) = (number_of w mod 2 ^ n :: int)"
+ by (simp add : bintrunc_mod2p number_of_eq)
+
+lemma no_sbintr_alt2:
+ "sbintrunc n = (%w. (w + 2 ^ n) mod 2 ^ Suc n - 2 ^ n :: int)"
+ by (rule ext) (simp add : sbintrunc_mod2p)
+
+lemma no_sbintr:
+ "number_of (sbintrunc n w) =
+ ((number_of w + 2 ^ n) mod 2 ^ Suc n - 2 ^ n :: int)"
+ by (simp add : no_sbintr_alt2 number_of_eq)
+
+lemma range_sbintrunc:
+ "range (sbintrunc n) = {i. - (2 ^ n) <= i & i < 2 ^ n}"
+ apply (unfold no_sbintr_alt2)
+ apply (auto simp add: image_iff eq_diff_eq)
+ apply (rule exI)
+ apply (auto intro: int_mod_lem [THEN iffD1, symmetric])
+ done
+
+lemma sb_inc_lem:
+ "(a::int) + 2^k < 0 \<Longrightarrow> a + 2^k + 2^(Suc k) <= (a + 2^k) mod 2^(Suc k)"
+ apply (erule int_mod_ge' [where n = "2 ^ (Suc k)" and b = "a + 2 ^ k", simplified zless2p])
+ apply (rule TrueI)
+ done
+
+lemma sb_inc_lem':
+ "(a::int) < - (2^k) \<Longrightarrow> a + 2^k + 2^(Suc k) <= (a + 2^k) mod 2^(Suc k)"
+ by (rule sb_inc_lem) simp
+
+lemma sbintrunc_inc:
+ "x < - (2^n) ==> x + 2^(Suc n) <= sbintrunc n x"
+ unfolding no_sbintr_alt2 by (drule sb_inc_lem') simp
+
+lemma sb_dec_lem:
+ "(0::int) <= - (2^k) + a ==> (a + 2^k) mod (2 * 2 ^ k) <= - (2 ^ k) + a"
+ by (rule int_mod_le' [where n = "2 ^ (Suc k)" and b = "a + 2 ^ k",
+ simplified zless2p, OF _ TrueI, simplified])
+
+lemma sb_dec_lem':
+ "(2::int) ^ k <= a ==> (a + 2 ^ k) mod (2 * 2 ^ k) <= - (2 ^ k) + a"
+ by (rule iffD1 [OF diff_le_eq', THEN sb_dec_lem, simplified])
+
+lemma sbintrunc_dec:
+ "x >= (2 ^ n) ==> x - 2 ^ (Suc n) >= sbintrunc n x"
+ unfolding no_sbintr_alt2 by (drule sb_dec_lem') simp
+
+lemmas zmod_uminus' = zmod_uminus [where b="c", standard]
+lemmas zpower_zmod' = zpower_zmod [where m="c" and y="k", standard]
+
+lemmas brdmod1s' [symmetric] =
+ mod_add_left_eq mod_add_right_eq
+ zmod_zsub_left_eq zmod_zsub_right_eq
+ zmod_zmult1_eq zmod_zmult1_eq_rev
+
+lemmas brdmods' [symmetric] =
+ zpower_zmod' [symmetric]
+ trans [OF mod_add_left_eq mod_add_right_eq]
+ trans [OF zmod_zsub_left_eq zmod_zsub_right_eq]
+ trans [OF zmod_zmult1_eq zmod_zmult1_eq_rev]
+ zmod_uminus' [symmetric]
+ mod_add_left_eq [where b = "1::int"]
+ zmod_zsub_left_eq [where b = "1"]
+
+lemmas bintr_arith1s =
+ brdmod1s' [where c="2^n::int", folded pred_def succ_def bintrunc_mod2p, standard]
+lemmas bintr_ariths =
+ brdmods' [where c="2^n::int", folded pred_def succ_def bintrunc_mod2p, standard]
+
+lemmas m2pths = pos_mod_sign pos_mod_bound [OF zless2p, standard]
+
+lemma bintr_ge0: "(0 :: int) <= number_of (bintrunc n w)"
+ by (simp add : no_bintr m2pths)
+
+lemma bintr_lt2p: "number_of (bintrunc n w) < (2 ^ n :: int)"
+ by (simp add : no_bintr m2pths)
+
+lemma bintr_Min:
+ "number_of (bintrunc n Int.Min) = (2 ^ n :: int) - 1"
+ by (simp add : no_bintr m1mod2k)
+
+lemma sbintr_ge: "(- (2 ^ n) :: int) <= number_of (sbintrunc n w)"
+ by (simp add : no_sbintr m2pths)
+
+lemma sbintr_lt: "number_of (sbintrunc n w) < (2 ^ n :: int)"
+ by (simp add : no_sbintr m2pths)
+
+lemma bintrunc_Suc:
+ "bintrunc (Suc n) bin = bintrunc n (bin_rest bin) BIT bin_last bin"
+ by (case_tac bin rule: bin_exhaust) auto
+
+lemma sign_Pls_ge_0:
+ "(bin_sign bin = Int.Pls) = (number_of bin >= (0 :: int))"
+ by (induct bin rule: numeral_induct) auto
+
+lemma sign_Min_lt_0:
+ "(bin_sign bin = Int.Min) = (number_of bin < (0 :: int))"
+ by (induct bin rule: numeral_induct) auto
+
+lemmas sign_Min_neg = trans [OF sign_Min_lt_0 neg_def [symmetric]]
+
+lemma bin_rest_trunc:
+ "!!bin. (bin_rest (bintrunc n bin)) = bintrunc (n - 1) (bin_rest bin)"
+ by (induct n) auto
+
+lemma bin_rest_power_trunc [rule_format] :
+ "(bin_rest ^^ k) (bintrunc n bin) =
+ bintrunc (n - k) ((bin_rest ^^ k) bin)"
+ by (induct k) (auto simp: bin_rest_trunc)
+
+lemma bin_rest_trunc_i:
+ "bintrunc n (bin_rest bin) = bin_rest (bintrunc (Suc n) bin)"
+ by auto
+
+lemma bin_rest_strunc:
+ "!!bin. bin_rest (sbintrunc (Suc n) bin) = sbintrunc n (bin_rest bin)"
+ by (induct n) auto
+
+lemma bintrunc_rest [simp]:
+ "!!bin. bintrunc n (bin_rest (bintrunc n bin)) = bin_rest (bintrunc n bin)"
+ apply (induct n, simp)
+ apply (case_tac bin rule: bin_exhaust)
+ apply (auto simp: bintrunc_bintrunc_l)
+ done
+
+lemma sbintrunc_rest [simp]:
+ "!!bin. sbintrunc n (bin_rest (sbintrunc n bin)) = bin_rest (sbintrunc n bin)"
+ apply (induct n, simp)
+ apply (case_tac bin rule: bin_exhaust)
+ apply (auto simp: bintrunc_bintrunc_l split: bit.splits)
+ done
+
+lemma bintrunc_rest':
+ "bintrunc n o bin_rest o bintrunc n = bin_rest o bintrunc n"
+ by (rule ext) auto
+
+lemma sbintrunc_rest' :
+ "sbintrunc n o bin_rest o sbintrunc n = bin_rest o sbintrunc n"
+ by (rule ext) auto
+
+lemma rco_lem:
+ "f o g o f = g o f ==> f o (g o f) ^^ n = g ^^ n o f"
+ apply (rule ext)
+ apply (induct_tac n)
+ apply (simp_all (no_asm))
+ apply (drule fun_cong)
+ apply (unfold o_def)
+ apply (erule trans)
+ apply simp
+ done
+
+lemma rco_alt: "(f o g) ^^ n o f = f o (g o f) ^^ n"
+ apply (rule ext)
+ apply (induct n)
+ apply (simp_all add: o_def)
+ done
+
+lemmas rco_bintr = bintrunc_rest'
+ [THEN rco_lem [THEN fun_cong], unfolded o_def]
+lemmas rco_sbintr = sbintrunc_rest'
+ [THEN rco_lem [THEN fun_cong], unfolded o_def]
+
+subsection {* Splitting and concatenation *}
+
+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))"
+
+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 *}
+
+lemma funpow_minus_simp:
+ "0 < n \<Longrightarrow> f ^^ n = f \<circ> f ^^ (n - 1)"
+ by (cases n) simp_all
+
+lemmas funpow_pred_simp [simp] =
+ funpow_minus_simp [of "number_of bin", simplified nobm1, standard]
+
+lemmas replicate_minus_simp =
+ trans [OF gen_minus [where f = "%n. replicate n x"] replicate.replicate_Suc,
+ standard]
+
+lemmas replicate_pred_simp [simp] =
+ replicate_minus_simp [of "number_of bin", simplified nobm1, standard]
+
+lemmas power_Suc_no [simp] = power_Suc [of "number_of a", standard]
+
+lemmas power_minus_simp =
+ trans [OF gen_minus [where f = "power f"] power_Suc, standard]
+
+lemmas power_pred_simp =
+ power_minus_simp [of "number_of bin", simplified nobm1, standard]
+lemmas power_pred_simp_no [simp] = power_pred_simp [where f= "number_of f", standard]
+
+lemma list_exhaust_size_gt0:
+ assumes y: "\<And>a list. y = a # list \<Longrightarrow> P"
+ shows "0 < length y \<Longrightarrow> P"
+ apply (cases y, simp)
+ apply (rule y)
+ apply fastsimp
+ done
+
+lemma list_exhaust_size_eq0:
+ assumes y: "y = [] \<Longrightarrow> P"
+ shows "length y = 0 \<Longrightarrow> P"
+ apply (cases y)
+ apply (rule y, simp)
+ apply simp
+ done
+
+lemma size_Cons_lem_eq:
+ "y = xa # list ==> size y = Suc k ==> size list = k"
+ by auto
+
+lemma size_Cons_lem_eq_bin:
+ "y = xa # list ==> size y = number_of (Int.succ k) ==>
+ size list = number_of k"
+ by (auto simp: pred_def succ_def split add : split_if_asm)
+
+lemmas ls_splits =
+ prod.split split_split prod.split_asm split_split_asm split_if_asm
+
+lemma not_B1_is_B0: "y \<noteq> (1::bit) \<Longrightarrow> y = (0::bit)"
+ by (cases y) auto
+
+lemma B1_ass_B0:
+ assumes y: "y = (0::bit) \<Longrightarrow> y = (1::bit)"
+ shows "y = (1::bit)"
+ apply (rule classical)
+ apply (drule not_B1_is_B0)
+ apply (erule y)
+ done
+
+-- "simplifications for specific word lengths"
+lemmas n2s_ths [THEN eq_reflection] = add_2_eq_Suc add_2_eq_Suc'
+
+lemmas s2n_ths = n2s_ths [symmetric]
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Word/Bool_List_Representation.thy Wed Jun 30 16:45:47 2010 +0200
@@ -0,0 +1,1174 @@
+(*
+ Author: Jeremy Dawson, NICTA
+
+ contains theorems to do with integers, expressed using Pls, Min, BIT,
+ theorems linking them to lists of booleans, and repeated splitting
+ and concatenation.
+*)
+
+header "Bool lists and integers"
+
+theory Bool_List_Representation
+imports Bit_Int
+begin
+
+subsection {* Operations on lists of booleans *}
+
+primrec bl_to_bin_aux :: "bool list \<Rightarrow> int \<Rightarrow> int" where
+ Nil: "bl_to_bin_aux [] w = w"
+ | Cons: "bl_to_bin_aux (b # bs) w =
+ 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"
+
+primrec bin_to_bl_aux :: "nat \<Rightarrow> int \<Rightarrow> bool list \<Rightarrow> bool list" where
+ Z: "bin_to_bl_aux 0 w bl = bl"
+ | Suc: "bin_to_bl_aux (Suc n) w bl =
+ bin_to_bl_aux n (bin_rest w) ((bin_last w = 1) # bl)"
+
+definition bin_to_bl :: "nat \<Rightarrow> int \<Rightarrow> bool list" where
+ bin_to_bl_def : "bin_to_bl n w = bin_to_bl_aux n w []"
+
+primrec bl_of_nth :: "nat \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool list" where
+ Suc: "bl_of_nth (Suc n) f = f n # bl_of_nth n f"
+ | Z: "bl_of_nth 0 f = []"
+
+primrec takefill :: "'a \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+ Z: "takefill fill 0 xs = []"
+ | Suc: "takefill fill (Suc n) xs = (
+ case xs of [] => fill # takefill fill n xs
+ | y # ys => y # takefill fill n ys)"
+
+definition map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list" where
+ "map2 f as bs = map (split f) (zip as bs)"
+
+lemma map2_Nil [simp]: "map2 f [] ys = []"
+ unfolding map2_def by auto
+
+lemma map2_Nil2 [simp]: "map2 f xs [] = []"
+ unfolding map2_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
+
+
+subsection "Arithmetic in terms of bool lists"
+
+(* arithmetic operations in terms of the reversed bool list,
+ assuming input list(s) the same length, and don't extend them *)
+
+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)"
+
+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 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 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 butlast_power:
+ "(butlast ^^ n) bl = take (length bl - n) bl"
+ by (induct n) (auto simp: butlast_take)
+
+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)"
+ by (cases n) auto
+
+lemma bin_to_bl_aux_Min_minus_simp [simp]:
+ "0 < n ==> bin_to_bl_aux n Int.Min bl =
+ bin_to_bl_aux (n - 1) Int.Min (True # bl)"
+ by (cases n) auto
+
+lemma bin_to_bl_aux_Bit_minus_simp [simp]:
+ "0 < n ==> bin_to_bl_aux n (w BIT b) bl =
+ bin_to_bl_aux (n - 1) w ((b = 1) # bl)"
+ by (cases n) auto
+
+lemma bin_to_bl_aux_Bit0_minus_simp [simp]:
+ "0 < n ==> bin_to_bl_aux n (Int.Bit0 w) bl =
+ bin_to_bl_aux (n - 1) w (False # bl)"
+ by (cases n) auto
+
+lemma bin_to_bl_aux_Bit1_minus_simp [simp]:
+ "0 < n ==> bin_to_bl_aux n (Int.Bit1 w) bl =
+ bin_to_bl_aux (n - 1) w (True # bl)"
+ by (cases n) auto
+
+(** link between bin and bool list **)
+
+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:
+ "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 cs (bl_to_bin bs)"
+ unfolding bl_to_bin_def by (rule bl_to_bin_aux_append)
+
+lemma bin_to_bl_aux_alt:
+ "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 = []"
+ 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"
+ unfolding bin_to_bl_def by (simp add : size_bin_to_bl_aux)
+
+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':
+ "bin_to_bl (n + length bs) (bl_to_bin_aux bs w) =
+ bin_to_bl_aux n w bs"
+ apply (induct bs arbitrary: w n)
+ apply auto
+ apply (simp_all only : add_Suc [symmetric])
+ apply (auto simp add : bin_to_bl_def)
+ done
+
+lemma bl_bin_bl: "bin_to_bl (length bs) (bl_to_bin bs) = bs"
+ unfolding bl_to_bin_def
+ apply (rule box_equals)
+ apply (rule bl_bin_bl')
+ prefer 2
+ apply (rule bin_to_bl_aux.Z)
+ 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)
+ defer
+ apply (rule bl_bin_bl)
+ apply (rule bl_bin_bl)
+ apply simp
+ done
+
+lemma bl_to_bin_False: "bl_to_bin (False # bl) = bl_to_bin bl"
+ unfolding bl_to_bin_def by auto
+
+lemma bl_to_bin_Nil: "bl_to_bin [] = Int.Pls"
+ unfolding bl_to_bin_def by auto
+
+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)
+
+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: "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: bl_to_bin_def)
+ done
+
+lemma bin_to_bl_trunc:
+ "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 =
+ replicate (n - m) False @ bin_to_bl_aux (min n m) bin bl"
+ apply (induct n)
+ apply clarsimp
+ apply clarsimp
+ apply (case_tac "m")
+ apply (clarsimp simp: bin_to_bl_Pls_aux)
+ apply (erule thin_rl)
+ apply (induct_tac n)
+ apply auto
+ done
+
+lemmas bin_to_bl_bintr =
+ bin_to_bl_aux_bintr [where bl = "[]", folded bin_to_bl_def]
+
+lemma bl_to_bin_rep_False: "bl_to_bin (replicate n False) = Int.Pls"
+ 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':
+ "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:
+ "hd (bin_to_bl_aux (Suc n) w bs) =
+ (bin_sign (sbintrunc n w) = Int.Min)"
+ apply (induct n arbitrary: w bs)
+ apply clarsimp
+ apply (cases w rule: bin_exhaust)
+ apply (simp split add : bit.split)
+ apply clarsimp
+ done
+
+lemma bl_sbin_sign:
+ "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 =
+ (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 auto
+ done
+
+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)
+ apply clarsimp
+ apply (case_tac m, clarsimp)
+ apply (clarsimp simp: bin_to_bl_def)
+ apply (simp add: bin_to_bl_aux_alt)
+ apply clarsimp
+ apply (case_tac m, clarsimp)
+ apply (clarsimp simp: bin_to_bl_def)
+ 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")
+ 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 arith
+ done
+
+lemmas nth_rev_alt = nth_rev [where xs = "rev ys", simplified, standard]
+
+lemma nth_bin_to_bl_aux [rule_format] :
+ "ALL w n bl. n < m + length bl --> (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 clarsimp
+ apply clarsimp
+ apply (case_tac w rule: bin_exhaust)
+ apply clarsimp
+ apply (case_tac "n - m")
+ apply arith
+ apply simp
+ apply (rule_tac f = "%n. bl ! n" in arg_cong)
+ apply arith
+ 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)
+ apply clarsimp
+ apply clarsimp
+ apply safe
+ apply (erule allE, erule xtr8 [rotated],
+ simp add: numeral_simps algebra_simps cong add : number_of_False_cong)+
+ done
+
+lemma bl_to_bin_lt2p: "bl_to_bin bs < (2 ^ length bs)"
+ apply (unfold bl_to_bin_def)
+ apply (rule xtr1)
+ prefer 2
+ apply (rule bl_to_bin_lt2p_aux)
+ 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)
+ apply clarsimp
+ apply clarsimp
+ apply safe
+ apply (erule allE, erule preorder_class.order_trans [rotated],
+ simp add: numeral_simps algebra_simps cong add : number_of_False_cong)+
+ done
+
+lemma bl_to_bin_ge0: "bl_to_bin bs >= 0"
+ apply (unfold bl_to_bin_def)
+ apply (rule xtr4)
+ apply (rule bl_to_bin_ge2p_aux)
+ apply simp
+ done
+
+lemma butlast_rest_bin:
+ "butlast (bin_to_bl n w) = bin_to_bl (n - 1) (bin_rest w)"
+ apply (unfold bin_to_bl_def)
+ apply (cases w rule: bin_exhaust)
+ apply (cases n, clarsimp)
+ apply clarsimp
+ apply (auto simp add: bin_to_bl_aux_alt)
+ done
+
+lemmas butlast_bin_rest = butlast_rest_bin
+ [where w="bl_to_bin bl" and n="length bl", simplified, standard]
+
+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)"
+ apply (unfold bl_to_bin_def)
+ apply (cases bl)
+ 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) =
+ bl_to_bin_aux (drop (length bl - m) bl) (bintrunc (m - length bl) w)"
+ apply (induct_tac bl)
+ apply clarsimp
+ apply clarsimp
+ apply safe
+ 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 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 list (Int.Bit0 (bintrunc nat w))"
+ in arg_cong)
+ apply simp
+ done
+
+lemma trunc_bl2bin:
+ "bintrunc m (bl_to_bin bl) = bl_to_bin (drop (length bl - m) bl)"
+ unfolding bl_to_bin_def by (simp add : trunc_bl2bin_aux)
+
+lemmas trunc_bl2bin_len [simp] =
+ trunc_bl2bin [of "length bl" bl, simplified, standard]
+
+lemma bl2bin_drop:
+ "bl_to_bin (drop k bl) = bintrunc (length bl - k) (bl_to_bin bl)"
+ apply (rule trans)
+ prefer 2
+ apply (rule trunc_bl2bin [symmetric])
+ apply (cases "k <= length bl")
+ 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)
+ apply clarsimp
+ apply (simp only: bin_nth.Suc [symmetric] add_Suc)
+ done
+
+lemma take_rest_power_bin:
+ "m <= n ==> take m (bin_to_bl n w) = bin_to_bl m ((bin_rest ^^ (n - m)) w)"
+ apply (rule nth_equalityI)
+ apply simp
+ apply (clarsimp simp add: nth_bin_to_bl nth_rest_power_bin)
+ done
+
+lemma hd_butlast: "size xs > 1 ==> hd (butlast xs) = hd xs"
+ by (cases xs) auto
+
+lemma last_bin_last':
+ "size xs > 0 \<Longrightarrow> last xs = (bin_last (bl_to_bin_aux xs w) = 1)"
+ by (induct xs arbitrary: w) auto
+
+lemma last_bin_last:
+ "size xs > 0 ==> last xs = (bin_last (bl_to_bin xs) = 1)"
+ unfolding bl_to_bin_def by (erule last_bin_last')
+
+lemma bin_last_last:
+ "bin_last w = (if last (bin_to_bl (Suc n) w) then 1 else 0)"
+ apply (unfold bin_to_bl_def)
+ apply simp
+ apply (auto simp add: bin_to_bl_aux_alt)
+ done
+
+(** 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) =
+ bin_to_bl_aux n (v XOR w) (map2 (%x y. x ~= y) 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_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) =
+ bin_to_bl_aux n (v AND 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_not_aux_bin [rule_format] :
+ "ALL w cs. map Not (bin_to_bl_aux n w cs) =
+ bin_to_bl_aux n (NOT w) (map Not cs)"
+ apply (induct n)
+ apply clarsimp
+ apply clarsimp
+ apply (case_tac w rule: bin_exhaust)
+ apply (case_tac b)
+ apply auto
+ done
+
+lemmas bl_not_bin = bl_not_aux_bin
+ [where cs = "[]", unfolded bin_to_bl_def [symmetric] map.simps]
+
+lemmas bl_and_bin = bl_and_aux_bin [where bs="[]" and cs="[]",
+ unfolded map2_Nil, folded bin_to_bl_def]
+
+lemmas bl_or_bin = bl_or_aux_bin [where bs="[]" and cs="[]",
+ unfolded map2_Nil, folded bin_to_bl_def]
+
+lemmas bl_xor_bin = bl_xor_aux_bin [where bs="[]" and cs="[]",
+ 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) =
+ bin_to_bl_aux (n - m) bin (drop (m - n) bs)"
+ apply (induct n, clarsimp)
+ apply clarsimp
+ apply (case_tac bin rule: bin_exhaust)
+ apply (case_tac "m <= n", simp)
+ apply (case_tac "m - n", simp)
+ apply simp
+ apply (rule_tac f = "%nat. drop nat bs" in arg_cong)
+ apply simp
+ done
+
+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)
+ 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) =
+ take m (bin_to_bl (m + n) w)"
+ apply (induct n)
+ apply clarify
+ 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) -->
+ bin_to_bl m a = take m (bin_to_bl (m + n) c)"
+ apply (induct n)
+ apply clarsimp
+ apply (clarsimp simp: Let_def split: ls_splits)
+ apply (simp add: bin_to_bl_def)
+ apply (simp add: take_bin2bl_lem)
+ done
+
+lemma bin_split_take1:
+ "k = m + n ==> bin_split n c = (a, b) ==>
+ 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 -->
+ takefill fill n l ! m = (if m < length l then l ! m else fill)"
+ apply (induct n, 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_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 length_takefill [simp]: "length (takefill fill n l) = n"
+ by (simp add : takefill_alt)
+
+lemma take_takefill':
+ "!!w n. n = k + m ==> take k (takefill fill n w) = takefill fill k w"
+ by (induct k) (auto split add : list.split)
+
+lemma drop_takefill:
+ "!!w. drop k (takefill fill (m + k) w) = takefill fill m (drop k w)"
+ by (induct k) (auto split add : list.split)
+
+lemma takefill_le [simp]:
+ "m \<le> n \<Longrightarrow> takefill x m (takefill x n l) = takefill x m l"
+ by (auto simp: le_iff_add takefill_le')
+
+lemma take_takefill [simp]:
+ "m \<le> n \<Longrightarrow> take m (takefill fill n w) = takefill fill m w"
+ by (auto simp: le_iff_add take_takefill')
+
+lemma takefill_append:
+ "takefill fill (m + length xs) (xs @ w) = xs @ (takefill fill m w)"
+ by (induct xs) auto
+
+lemma takefill_same':
+ "l = length xs ==> takefill fill l xs = xs"
+ by clarify (induct xs, auto)
+
+lemmas takefill_same [simp] = takefill_same' [OF refl]
+
+lemma takefill_bintrunc:
+ "takefill False n bl = rev (bin_to_bl n (bl_to_bin (rev bl)))"
+ apply (rule nth_equalityI)
+ apply simp
+ apply (clarsimp simp: nth_takefill nth_rev nth_bin_to_bl bin_nth_of_bl)
+ done
+
+lemma bl_bin_bl_rtf:
+ "bin_to_bl n (bl_to_bin bl) = rev (takefill False n (rev bl))"
+ by (simp add : takefill_bintrunc)
+
+lemmas bl_bin_bl_rep_drop =
+ bl_bin_bl_rtf [simplified takefill_alt,
+ simplified, simplified rev_take, simplified]
+
+lemma tf_rev:
+ "n + k = m + length bl ==> takefill x m (rev (takefill y n bl)) =
+ rev (takefill y m (rev (takefill x k (rev bl))))"
+ apply (rule nth_equalityI)
+ apply (auto simp add: nth_takefill nth_rev)
+ apply (rule_tac f = "%n. bl ! n" in arg_cong)
+ apply arith
+ done
+
+lemma takefill_minus:
+ "0 < n ==> takefill fill (Suc (n - 1)) w = takefill fill n w"
+ by auto
+
+lemmas takefill_Suc_cases =
+ list.cases [THEN takefill.Suc [THEN trans], standard]
+
+lemmas takefill_Suc_Nil = takefill_Suc_cases (1)
+lemmas takefill_Suc_Cons = takefill_Suc_cases (2)
+
+lemmas takefill_minus_simps = takefill_Suc_cases [THEN [2]
+ takefill_minus [symmetric, THEN trans], standard]
+
+lemmas takefill_pred_simps [simp] =
+ takefill_minus_simps [where n="number_of bin", simplified nobm1, standard]
+
+(* links with function bl_to_bin *)
+
+lemma bl_to_bin_aux_cat:
+ "!!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)
+ done
+
+lemma bin_to_bl_aux_cat:
+ "!!w bs. bin_to_bl_aux (nv + nw) (bin_cat v nw w) bs =
+ bin_to_bl_aux nv v (bin_to_bl_aux nw w bs)"
+ by (induct nw) auto
+
+lemmas bl_to_bin_aux_alt =
+ bl_to_bin_aux_cat [where nv = "0" and v = "Int.Pls",
+ simplified bl_to_bin_def [symmetric], simplified]
+
+lemmas bin_to_bl_cat =
+ bin_to_bl_aux_cat [where bs = "[]", folded bin_to_bl_def]
+
+lemmas bl_to_bin_aux_app_cat =
+ trans [OF bl_to_bin_aux_append bl_to_bin_aux_alt]
+
+lemmas bin_to_bl_aux_cat_app =
+ trans [OF bin_to_bl_aux_cat bin_to_bl_aux_alt]
+
+lemmas bl_to_bin_app_cat = bl_to_bin_aux_app_cat
+ [where w = "Int.Pls", folded bl_to_bin_def]
+
+lemmas bin_to_bl_cat_app = bin_to_bl_aux_cat_app
+ [where bs = "[]", folded bin_to_bl_def]
+
+(* bl_to_bin_app_cat_alt and bl_to_bin_app_cat are easily interderivable *)
+lemma bl_to_bin_app_cat_alt:
+ "bin_cat (bl_to_bin cs) n w = bl_to_bin (cs @ bin_to_bl n w)"
+ by (simp add : bl_to_bin_app_cat)
+
+lemma mask_lem: "(bl_to_bin (True # replicate n False)) =
+ Int.succ (bl_to_bin (replicate n True))"
+ apply (unfold bl_to_bin_def)
+ apply (induct n)
+ apply simp
+ apply (simp only: Suc_eq_plus1 replicate_add
+ append_Cons [symmetric] bl_to_bin_aux_append)
+ apply simp
+ done
+
+(* function bl_of_nth *)
+lemma length_bl_of_nth [simp]: "length (bl_of_nth n f) = n"
+ by (induct n) auto
+
+lemma nth_bl_of_nth [simp]:
+ "m < n \<Longrightarrow> rev (bl_of_nth n f) ! m = f m"
+ apply (induct n)
+ apply simp
+ apply (clarsimp simp add : nth_append)
+ apply (rule_tac f = "f" in arg_cong)
+ apply simp
+ done
+
+lemma bl_of_nth_inj:
+ "(!!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)
+ apply clarsimp
+ apply (rule trans [OF _ hd_Cons_tl])
+ apply (frule Suc_le_lessD)
+ apply (simp add: nth_rev trans [OF drop_Suc drop_tl, symmetric])
+ apply (subst hd_drop_conv_nth)
+ apply force
+ apply simp_all
+ apply (rule_tac f = "%n. drop n xs" in arg_cong)
+ apply simp
+ done
+
+lemmas bl_of_nth_nth [simp] = order_refl [THEN bl_of_nth_nth_le, simplified]
+
+lemma size_rbl_pred: "length (rbl_pred bl) = length bl"
+ by (induct bl) auto
+
+lemma size_rbl_succ: "length (rbl_succ bl) = length bl"
+ by (induct bl) auto
+
+lemma size_rbl_add:
+ "!!cl. length (rbl_add bl cl) = length bl"
+ by (induct bl) (auto simp: Let_def size_rbl_succ)
+
+lemma size_rbl_mult:
+ "!!cl. length (rbl_mult bl cl) = length bl"
+ by (induct bl) (auto simp add : Let_def size_rbl_add)
+
+lemmas rbl_sizes [simp] =
+ size_rbl_pred size_rbl_succ size_rbl_add size_rbl_mult
+
+lemmas rbl_Nils =
+ rbl_pred.Nil rbl_succ.Nil rbl_add.Nil rbl_mult.Nil
+
+lemma rbl_pred:
+ "!!bin. rbl_pred (rev (bin_to_bl n bin)) = rev (bin_to_bl n (Int.pred bin))"
+ apply (induct n, simp)
+ apply (unfold bin_to_bl_def)
+ apply clarsimp
+ apply (case_tac bin rule: bin_exhaust)
+ apply (case_tac b)
+ apply (clarsimp simp: bin_to_bl_aux_alt)+
+ done
+
+lemma rbl_succ:
+ "!!bin. rbl_succ (rev (bin_to_bl n bin)) = rev (bin_to_bl n (Int.succ bin))"
+ apply (induct n, simp)
+ apply (unfold bin_to_bl_def)
+ apply clarsimp
+ apply (case_tac bin rule: bin_exhaust)
+ apply (case_tac b)
+ apply (clarsimp simp: bin_to_bl_aux_alt)+
+ done
+
+lemma rbl_add:
+ "!!bina binb. rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) =
+ rev (bin_to_bl n (bina + binb))"
+ apply (induct n, simp)
+ apply (unfold bin_to_bl_def)
+ apply clarsimp
+ apply (case_tac bina rule: bin_exhaust)
+ apply (case_tac binb rule: bin_exhaust)
+ apply (case_tac b)
+ apply (case_tac [!] "ba")
+ apply (auto simp: rbl_succ succ_def bin_to_bl_aux_alt Let_def add_ac)
+ done
+
+lemma rbl_add_app2:
+ "!!blb. length blb >= length bla ==>
+ rbl_add bla (blb @ blc) = rbl_add bla blb"
+ apply (induct bla, simp)
+ apply clarsimp
+ apply (case_tac blb, clarsimp)
+ apply (clarsimp simp: Let_def)
+ done
+
+lemma rbl_add_take2:
+ "!!blb. length blb >= length bla ==>
+ rbl_add bla (take (length bla) blb) = rbl_add bla blb"
+ apply (induct bla, simp)
+ apply clarsimp
+ apply (case_tac blb, clarsimp)
+ apply (clarsimp simp: Let_def)
+ done
+
+lemma rbl_add_long:
+ "m >= n ==> rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl m binb)) =
+ rev (bin_to_bl n (bina + binb))"
+ apply (rule box_equals [OF _ rbl_add_take2 rbl_add])
+ apply (rule_tac f = "rbl_add (rev (bin_to_bl n bina))" in arg_cong)
+ apply (rule rev_swap [THEN iffD1])
+ apply (simp add: rev_take drop_bin2bl)
+ apply simp
+ done
+
+lemma rbl_mult_app2:
+ "!!blb. length blb >= length bla ==>
+ rbl_mult bla (blb @ blc) = rbl_mult bla blb"
+ apply (induct bla, simp)
+ apply clarsimp
+ apply (case_tac blb, clarsimp)
+ apply (clarsimp simp: Let_def rbl_add_app2)
+ done
+
+lemma rbl_mult_take2:
+ "length blb >= length bla ==>
+ rbl_mult bla (take (length bla) blb) = rbl_mult bla blb"
+ apply (rule trans)
+ apply (rule rbl_mult_app2 [symmetric])
+ apply simp
+ apply (rule_tac f = "rbl_mult bla" in arg_cong)
+ apply (rule append_take_drop_id)
+ done
+
+lemma rbl_mult_gt1:
+ "m >= length bl ==> rbl_mult bl (rev (bin_to_bl m binb)) =
+ rbl_mult bl (rev (bin_to_bl (length bl) binb))"
+ apply (rule trans)
+ apply (rule rbl_mult_take2 [symmetric])
+ apply simp_all
+ apply (rule_tac f = "rbl_mult bl" in arg_cong)
+ apply (rule rev_swap [THEN iffD1])
+ apply (simp add: rev_take drop_bin2bl)
+ done
+
+lemma rbl_mult_gt:
+ "m > n ==> rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl m binb)) =
+ rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb))"
+ by (auto intro: trans [OF rbl_mult_gt1])
+
+lemmas rbl_mult_Suc = lessI [THEN rbl_mult_gt]
+
+lemma rbbl_Cons:
+ "b # rev (bin_to_bl n x) = rev (bin_to_bl (Suc n) (x BIT If b 1 0))"
+ apply (unfold bin_to_bl_def)
+ apply simp
+ apply (simp add: bin_to_bl_aux_alt)
+ done
+
+lemma rbl_mult: "!!bina binb.
+ rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) =
+ rev (bin_to_bl n (bina * binb))"
+ apply (induct n)
+ apply simp
+ apply (unfold bin_to_bl_def)
+ apply clarsimp
+ apply (case_tac bina rule: bin_exhaust)
+ apply (case_tac binb rule: bin_exhaust)
+ apply (case_tac b)
+ apply (case_tac [!] "ba")
+ apply (auto simp: bin_to_bl_aux_alt Let_def)
+ apply (auto simp: rbbl_Cons rbl_mult_Suc rbl_add)
+ done
+
+lemma rbl_add_split:
+ "P (rbl_add (y # ys) (x # xs)) =
+ (ALL ws. length ws = length ys --> ws = rbl_add ys xs -->
+ (y --> ((x --> P (False # rbl_succ ws)) & (~ x --> P (True # ws)))) &
+ (~ y --> P (x # ws)))"
+ apply (auto simp add: Let_def)
+ apply (case_tac [!] "y")
+ apply auto
+ done
+
+lemma rbl_mult_split:
+ "P (rbl_mult (y # ys) xs) =
+ (ALL ws. length ws = Suc (length ys) --> ws = False # rbl_mult ys xs -->
+ (y --> P (rbl_add ws xs)) & (~ y --> P ws))"
+ by (clarsimp simp add : Let_def)
+
+lemma and_len: "xs = ys ==> xs = ys & length xs = length ys"
+ by auto
+
+lemma size_if: "size (if p then xs else ys) = (if p then size xs else size ys)"
+ by auto
+
+lemma tl_if: "tl (if p then xs else ys) = (if p then tl xs else tl ys)"
+ by auto
+
+lemma hd_if: "hd (if p then xs else ys) = (if p then hd xs else hd ys)"
+ by auto
+
+lemma if_Not_x: "(if p then ~ x else x) = (p = (~ x))"
+ by auto
+
+lemma if_x_Not: "(if p then x else ~ x) = (p = x)"
+ by auto
+
+lemma if_same_and: "(If p x y & If p u v) = (if p then x & u else y & v)"
+ by auto
+
+lemma if_same_eq: "(If p x y = (If p u v)) = (if p then x = (u) else y = (v))"
+ by auto
+
+lemma if_same_eq_not:
+ "(If p x y = (~ If p u v)) = (if p then x = (~u) else y = (~v))"
+ by auto
+
+(* note - if_Cons can cause blowup in the size, if p is complex,
+ so make a simproc *)
+lemma if_Cons: "(if p then x # xs else y # ys) = If p x y # If p xs ys"
+ by auto
+
+lemma if_single:
+ "(if xc then [xab] else [an]) = [if xc then xab else an]"
+ by auto
+
+lemma if_bool_simps:
+ "If p True y = (p | y) & If p False y = (~p & y) &
+ If p y True = (p --> y) & If p y False = (p & y)"
+ by auto
+
+lemmas if_simps = if_x_Not if_Not_x if_cancel if_True if_False if_bool_simps
+
+lemmas seqr = eq_reflection [where x = "size w", standard]
+
+lemmas tl_Nil = tl.simps (1)
+lemmas tl_Cons = tl.simps (2)
+
+
+subsection "Repeated splitting or concatenation"
+
+lemma sclem:
+ "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 =
+ bin_cat x (size xs * n) (foldl (%u. bin_cat u n) y xs)"
+ apply (induct xs)
+ apply simp
+ apply clarify
+ apply (simp (no_asm))
+ apply (frule asm_rl)
+ apply (drule spec)
+ apply (erule trans)
+ apply (drule_tac x = "bin_cat y n a" in spec)
+ apply (simp add : bin_cat_assoc_sym min_max.inf_absorb2)
+ done
+
+lemma bin_rcat_bl:
+ "(bin_rcat n wl) = bl_to_bin (concat (map (bin_to_bl n) wl))"
+ apply (unfold bin_rcat_def)
+ apply (rule sym)
+ apply (induct wl)
+ apply (auto simp add : bl_to_bin_append)
+ apply (simp add : bl_to_bin_aux_alt sclem)
+ apply (simp add : bin_cat_foldl_lem [symmetric])
+ done
+
+lemmas bin_rsplit_aux_simps = bin_rsplit_aux.simps bin_rsplitl_aux.simps
+lemmas rsplit_aux_simps = bin_rsplit_aux_simps
+
+lemmas th_if_simp1 = split_if [where P = "op = l",
+ THEN iffD1, THEN conjunct1, THEN mp, standard]
+lemmas th_if_simp2 = split_if [where P = "op = l",
+ THEN iffD1, THEN conjunct2, THEN mp, standard]
+
+lemmas rsplit_aux_simp1s = rsplit_aux_simps [THEN th_if_simp1]
+
+lemmas rsplit_aux_simp2ls = rsplit_aux_simps [THEN th_if_simp2]
+(* these safe to [simp add] as require calculating m - n *)
+lemmas bin_rsplit_aux_simp2s [simp] = rsplit_aux_simp2ls [unfolded Let_def]
+lemmas rbscl = bin_rsplit_aux_simp2s (2)
+
+lemmas rsplit_aux_0_simps [simp] =
+ rsplit_aux_simp1s [OF disjI1] rsplit_aux_simp1s [OF disjI2]
+
+lemma bin_rsplit_aux_append:
+ "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 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 = "[]"] =
+ bin_rsplit_aux_append bin_rsplitl_aux_append
+
+lemmas rsplit_def_auxs = bin_rsplit_def bin_rsplitl_def
+
+lemmas rsplit_aux_alts = rsplit_aux_apps
+ [unfolded append_Nil rsplit_def_auxs [symmetric]]
+
+lemma bin_split_minus: "0 < n ==> bin_split (Suc (n - 1)) w = bin_split n w"
+ by auto
+
+lemmas bin_split_minus_simp =
+ bin_split.Suc [THEN [2] bin_split_minus [symmetric, THEN trans], standard]
+
+lemma bin_split_pred_simp [simp]:
+ "(0::nat) < number_of bin \<Longrightarrow>
+ bin_split (number_of bin) w =
+ (let (w1, w2) = bin_split (number_of (Int.pred bin)) (bin_rest w)
+ 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
+ then bs
+ else let (a, b) = bin_split n c in bin_rsplit n (m - n, a) @ b # bs)"
+ 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
+ bin_rsplit_aux_simp_alt, standard]
+
+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)
+ 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
+
+lemmas bin_rsplit_size_sign = bin_rsplit_size_sign' [OF asm_rl
+ rev_rev_ident [THEN trans] set_rev [THEN equalityD2 [THEN subsetD]],
+ standard]
+
+lemma bin_nth_rsplit [rule_format] :
+ "n > 0 ==> m < n ==> (ALL w k nw. rev sw = bin_rsplit n (nw, w) -->
+ k < size sw --> bin_nth (sw ! k) m = bin_nth w (k * n + m))"
+ apply (induct sw)
+ apply clarsimp
+ apply clarsimp
+ apply (drule bthrs)
+ apply (simp (no_asm_use) add: Let_def split: ls_splits)
+ apply clarify
+ apply (erule allE, erule impE, erule exI)
+ apply (case_tac k)
+ apply clarsimp
+ prefer 2
+ apply clarsimp
+ apply (erule allE)
+ apply (erule (1) impE)
+ apply (drule bin_nth_split, erule conjE, erule allE,
+ erule trans, simp add : add_ac)+
+ done
+
+lemma bin_rsplit_all:
+ "0 < nw ==> nw <= n ==> bin_rsplit n (nw, w) = [bintrunc n w]"
+ unfolding bin_rsplit_def
+ by (clarsimp dest!: split_bintrunc simp: rsplit_aux_simp2ls split: ls_splits)
+
+lemma bin_rsplit_l [rule_format] :
+ "ALL bin. bin_rsplitl n (m, bin) = bin_rsplit n (m, bintrunc m bin)"
+ apply (rule_tac a = "m" in wf_less_than [THEN wf_induct])
+ apply (simp (no_asm) add : bin_rsplitl_def bin_rsplit_def)
+ apply (rule allI)
+ apply (subst bin_rsplitl_aux.simps)
+ apply (subst bin_rsplit_aux.simps)
+ apply (clarsimp simp: Let_def split: ls_splits)
+ apply (drule bin_split_trunc)
+ apply (drule sym [THEN trans], assumption)
+ 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 (subst rsplit_aux_alts)
+ unfolding bin_split_cat
+ apply simp
+ done
+
+lemma bin_rsplit_aux_len_le [rule_format] :
+ "\<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)
+ done
+
+lemma bin_rsplit_len_le:
+ "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) =
+ (nw + n - 1) div n + length cs"
+ 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)
+ apply (case_tac m)
+ apply simp
+ apply (case_tac "m <= n")
+ apply auto
+ done
+
+lemma bin_rsplit_len:
+ "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:
+ "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 using `length bs = length cs` 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
+
+end
--- a/src/HOL/Word/WordDefinition.thy Wed Jun 30 16:41:03 2010 +0200
+++ b/src/HOL/Word/WordDefinition.thy Wed Jun 30 16:45:47 2010 +0200
@@ -8,7 +8,7 @@
header {* Definition of Word Type *}
theory WordDefinition
-imports Type_Length Misc_Typedef BinBoolList
+imports Type_Length Misc_Typedef Bool_List_Representation
begin
subsection {* Type definition *}