--- a/src/HOL/IsaMakefile Tue Aug 28 19:45:45 2007 +0200
+++ b/src/HOL/IsaMakefile Tue Aug 28 20:13:47 2007 +0200
@@ -814,7 +814,7 @@
Library/Boolean_Algebra.thy Library/Numeral_Type.thy \
Word/Num_Lemmas.thy \
Word/TdThs.thy \
- Word/BinInduct.thy \
+ Word/Size.thy \
Word/BinGeneral.thy \
Word/BinOperations.thy \
Word/BinBoolList.thy \
@@ -824,7 +824,6 @@
Word/WordBitwise.thy \
Word/WordShift.thy \
Word/WordGenLib.thy \
- Word/WordBoolList.thy \
Word/WordMain.thy \
Word/document/root.tex
@cd Word; $(ISATOOL) usedir -b -g true $(OUT)/HOL HOL-Word
--- a/src/HOL/Word/BinBoolList.thy Tue Aug 28 19:45:45 2007 +0200
+++ b/src/HOL/Word/BinBoolList.thy Tue Aug 28 20:13:47 2007 +0200
@@ -11,7 +11,32 @@
theory BinBoolList imports BinOperations begin
-subsection "Lemmas about standard list operations"
+subsection "Arithmetic in terms of bool lists"
+
+consts (* arithmetic operations in terms of the reversed bool list,
+ assuming input list(s) the same length, and don't extend them *)
+ rbl_succ :: "bool list => bool list"
+ rbl_pred :: "bool list => bool list"
+ rbl_add :: "bool list => bool list => bool list"
+ rbl_mult :: "bool list => bool list => bool list"
+
+primrec
+ Nil: "rbl_succ Nil = Nil"
+ Cons: "rbl_succ (x # xs) = (if x then False # rbl_succ xs else True # xs)"
+
+primrec
+ Nil : "rbl_pred Nil = Nil"
+ Cons : "rbl_pred (x # xs) = (if x then False # xs else True # rbl_pred xs)"
+
+primrec (* result is length of first arg, second arg may be longer *)
+ Nil : "rbl_add Nil x = Nil"
+ Cons : "rbl_add (y # ys) x = (let ws = rbl_add ys (tl x) in
+ (y ~= hd x) # (if hd x & y then rbl_succ ws else ws))"
+
+primrec (* result is length of first arg, second arg may be longer *)
+ Nil : "rbl_mult Nil x = Nil"
+ Cons : "rbl_mult (y # ys) x = (let ws = False # rbl_mult ys x in
+ if y then rbl_add ws x else ws)"
lemma tl_take: "tl (take n l) = take (n - 1) (tl l)"
apply (cases n, clarsimp)
@@ -50,34 +75,6 @@
"(butlast ^ n) bl = take (length bl - n) bl"
by (induct n) (auto simp: butlast_take)
-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]
-
-lemma hd_butlast: "size xs > 1 ==> hd (butlast xs) = hd xs"
- by (cases xs) auto
-
-subsection "From integers to bool lists"
-
-consts
- bin_to_bl :: "nat => int => bool list"
- bin_to_bl_aux :: "nat => int => bool list => bool list"
-
-primrec
- 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 = bit.B1) # bl)"
-
-defs
- bin_to_bl_def : "bin_to_bl n w == bin_to_bl_aux n w []"
-
lemma bin_to_bl_aux_Pls_minus_simp:
"0 < n ==> bin_to_bl_aux n Numeral.Pls bl =
bin_to_bl_aux (n - 1) Numeral.Pls (False # bl)"
@@ -97,24 +94,81 @@
bin_to_bl_aux_Min_minus_simp [simp]
bin_to_bl_aux_Bit_minus_simp [simp]
+(** link between bin and bool list **)
+
+lemma bl_to_bin_aux_append [rule_format] :
+ "ALL w. bl_to_bin_aux w (bs @ cs) = bl_to_bin_aux (bl_to_bin_aux w bs) cs"
+ by (induct bs) auto
+
lemma bin_to_bl_aux_append [rule_format] :
"ALL w bs. bin_to_bl_aux n w bs @ cs = bin_to_bl_aux n w (bs @ cs)"
by (induct n) auto
+lemma bl_to_bin_append:
+ "bl_to_bin (bs @ cs) = bl_to_bin_aux (bl_to_bin bs) cs"
+ 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 [simp]: "bin_to_bl 0 bs = []"
+lemma bin_to_bl_0: "bin_to_bl 0 bs = []"
unfolding bin_to_bl_def by auto
lemma size_bin_to_bl_aux [rule_format] :
"ALL w bs. size (bin_to_bl_aux n w bs) = n + length bs"
by (induct n) auto
-lemma size_bin_to_bl [simp]: "size (bin_to_bl n w) = n"
+lemma size_bin_to_bl: "size (bin_to_bl n w) = n"
unfolding bin_to_bl_def by (simp add : size_bin_to_bl_aux)
+lemma bin_bl_bin' [rule_format] :
+ "ALL w bs. bl_to_bin (bin_to_bl_aux n w bs) =
+ bl_to_bin_aux (bintrunc n w) bs"
+ by (induct n) (auto simp add : bl_to_bin_def)
+
+lemma bin_bl_bin: "bl_to_bin (bin_to_bl n w) = bintrunc n w"
+ unfolding bin_to_bl_def bin_bl_bin' by auto
+
+lemma bl_bin_bl' [rule_format] :
+ "ALL w n. bin_to_bl (n + length bs) (bl_to_bin_aux w bs) =
+ bin_to_bl_aux n w bs"
+ apply (induct "bs")
+ 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 [] = Numeral.Pls"
+ unfolding bl_to_bin_def by auto
+
lemma bin_to_bl_Pls_aux [rule_format] :
"ALL bl. bin_to_bl_aux n Numeral.Pls bl = replicate n False @ bl"
by (induct n) (auto simp: replicate_app_Cons_same)
@@ -129,6 +183,21 @@
lemma bin_to_bl_Min: "bin_to_bl n Numeral.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"
@@ -145,95 +214,16 @@
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) = Numeral.Pls"
+ by (induct n) auto
+
lemma len_bin_to_bl_aux [rule_format] :
"ALL w bs. length (bin_to_bl_aux n w bs) = n + length bs"
by (induct "n") auto
lemma len_bin_to_bl [simp]: "length (bin_to_bl n w) = n"
unfolding bin_to_bl_def len_bin_to_bl_aux by auto
-
-
-subsection "From bool lists to integers"
-
-consts
- bl_to_bin :: "bool list => int"
- bl_to_bin_aux :: "int => bool list => int"
-
-primrec
- Nil : "bl_to_bin_aux w [] = w"
- Cons : "bl_to_bin_aux w (b # bs) =
- bl_to_bin_aux (w BIT (if b then bit.B1 else bit.B0)) bs"
-
-defs
- bl_to_bin_def : "bl_to_bin bs == bl_to_bin_aux Numeral.Pls bs"
-
-(** link between bin and bool list **)
-
-lemma bl_to_bin_aux_append [rule_format] :
- "ALL w. bl_to_bin_aux w (bs @ cs) = bl_to_bin_aux (bl_to_bin_aux w bs) cs"
- by (induct bs) auto
-
-lemma bl_to_bin_append:
- "bl_to_bin (bs @ cs) = bl_to_bin_aux (bl_to_bin bs) cs"
- unfolding bl_to_bin_def by (rule bl_to_bin_aux_append)
-
-lemma bl_to_bin_False [simp]: "bl_to_bin (False # bl) = bl_to_bin bl"
- unfolding bl_to_bin_def by auto
-lemma bl_to_bin_Nil [simp]: "bl_to_bin [] = Numeral.Pls"
- unfolding bl_to_bin_def by auto
-
-lemma bl_to_bin_rep_F:
- "bl_to_bin (replicate n False @ bl) = bl_to_bin bl"
- by (induct n) auto
-
-lemma bl_to_bin_rep_False: "bl_to_bin (replicate n False) = Numeral.Pls"
- by (induct n) auto
-
-
-subsection "Converting between bool lists and integers"
-
-lemma bin_bl_bin' [rule_format] :
- "ALL w bs. bl_to_bin (bin_to_bl_aux n w bs) =
- bl_to_bin_aux (bintrunc n w) bs"
- by (induct n) (auto simp add : bl_to_bin_def)
-
-lemma bin_bl_bin [simp]: "bl_to_bin (bin_to_bl n w) = bintrunc n w"
- unfolding bin_to_bl_def bin_bl_bin' by auto
-
-lemma bl_bin_bl' [rule_format] :
- "ALL w n. bin_to_bl (n + length bs) (bl_to_bin_aux w bs) =
- bin_to_bl_aux n w bs"
- apply (induct "bs")
- apply auto
- apply (simp_all only : add_Suc [symmetric])
- apply (auto simp add : bin_to_bl_def)
- done
-
-lemma bl_bin_bl [simp]: "bin_to_bl (length bs) (bl_to_bin bs) = bs"
- unfolding bl_to_bin_def
- apply (rule box_equals)
- apply (rule bl_bin_bl')
- prefer 2
- apply (rule bin_to_bl_aux.Z)
- apply simp
- done
-
-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 bin_to_bl_trunc [simp]:
- "n <= m ==> bin_to_bl n (bintrunc m w) = bin_to_bl n w"
- by (auto intro: bl_to_bin_inj)
-
-subsection "@{term bin_sign} with bool list operations"
-
lemma sign_bl_bin' [rule_format] :
"ALL w. bin_sign (bl_to_bin_aux w bs) = bin_sign w"
by (induct bs) auto
@@ -255,8 +245,6 @@
"hd (bin_to_bl (Suc n) w) = (bin_sign (sbintrunc n w) = Numeral.Min)"
unfolding bin_to_bl_def by (rule bl_sbin_sign_aux)
-subsection "@{term bin_nth} with bool list operations"
-
lemma bin_nth_of_bl_aux [rule_format] :
"ALL w. bin_nth (bl_to_bin_aux w bl) n =
(n < size bl & rev bl ! n | n >= length bl & bin_nth w (n - size bl))"
@@ -284,6 +272,17 @@
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]
+
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))"
@@ -302,8 +301,6 @@
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)
-subsection "Ordering with bool list operations"
-
lemma bl_to_bin_lt2p_aux [rule_format] :
"ALL w. bl_to_bin_aux w bs < (w + 1) * (2 ^ length bs)"
apply (induct "bs")
@@ -339,8 +336,6 @@
apply simp
done
-subsection "@{term butlast} with bool list operations"
-
lemma butlast_rest_bin:
"butlast (bin_to_bl n w) = bin_to_bl (n - 1) (bin_rest w)"
apply (unfold bin_to_bl_def)
@@ -365,8 +360,6 @@
apply (auto simp add: butlast_rest_bl2bin_aux)
done
-subsection "Truncation"
-
lemma trunc_bl2bin_aux [rule_format] :
"ALL w. bintrunc m (bl_to_bin_aux w bl) =
bl_to_bin_aux (bintrunc (m - length bl) w) (drop (length bl - m) bl)"
@@ -404,7 +397,6 @@
apply auto
done
-(* TODO: This is not related to bool lists; should be moved *)
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)
@@ -419,7 +411,8 @@
apply (clarsimp simp add: nth_bin_to_bl nth_rest_power_bin)
done
-subsection "@{term last} with bool list operations"
+lemma hd_butlast: "size xs > 1 ==> hd (butlast xs) = hd xs"
+ by (cases xs) auto
lemma last_bin_last' [rule_format] :
"ALL w. size xs > 0 --> last xs = (bin_last (bl_to_bin_aux w xs) = bit.B1)"
@@ -436,14 +429,8 @@
apply (auto simp add: bin_to_bl_aux_alt)
done
-subsection "Bit-wise operations on bool lists"
-
-consts
- app2 :: "('a => 'b => 'c) => 'a list => 'b list => 'c list"
-
-defs
- app2_def : "app2 f as bs == map (split f) (zip as bs)"
-
+(** links between bit-wise operations and operations on bool lists **)
+
lemma app2_Nil [simp]: "app2 f [] ys = []"
unfolding app2_def by auto
@@ -513,8 +500,6 @@
lemmas bl_xor_bin = bl_xor_aux_bin [where bs="[]" and cs="[]",
unfolded app2_Nil, folded bin_to_bl_def]
-subsection "@{term drop} with bool list operations"
-
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)"
@@ -549,8 +534,6 @@
apply simp
done
-subsection "@{term bin_split} with bool list operations"
-
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)"
@@ -566,19 +549,6 @@
bin_to_bl m a = take m (bin_to_bl k c)"
by (auto elim: bin_split_take)
-subsection "@{term takefill}"
-
-consts
- takefill :: "'a => nat => 'a list => 'a list"
-
--- "takefill - like take but if argument list too short,"
--- "extends result to get requested length"
-primrec
- 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)"
-
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)
@@ -672,8 +642,6 @@
lemmas takefill_pred_simps [simp] =
takefill_minus_simps [where n="number_of bin", simplified nobm1, standard]
-subsection "@{term bin_cat} with bool list operations"
-
(* links with function bl_to_bin *)
lemma bl_to_bin_aux_cat:
@@ -723,15 +691,7 @@
apply simp
done
-subsection "function @{term bl_of_nth}"
-
-consts
- bl_of_nth :: "nat => (nat => bool) => bool list"
-
-primrec
- Suc : "bl_of_nth (Suc n) f = f n # bl_of_nth n f"
- Z : "bl_of_nth 0 f = []"
-
+(* function bl_of_nth *)
lemma length_bl_of_nth [simp]: "length (bl_of_nth n f) = n"
by (induct n) auto
@@ -764,33 +724,6 @@
lemmas bl_of_nth_nth [simp] = order_refl [THEN bl_of_nth_nth_le, simplified]
-subsection "Arithmetic in terms of bool lists"
-
-consts (* arithmetic operations in terms of the reversed bool list,
- assuming input list(s) the same length, and don't extend them *)
- rbl_succ :: "bool list => bool list"
- rbl_pred :: "bool list => bool list"
- rbl_add :: "bool list => bool list => bool list"
- rbl_mult :: "bool list => bool list => bool list"
-
-primrec
- Nil: "rbl_succ Nil = Nil"
- Cons: "rbl_succ (x # xs) = (if x then False # rbl_succ xs else True # xs)"
-
-primrec
- Nil : "rbl_pred Nil = Nil"
- Cons : "rbl_pred (x # xs) = (if x then False # xs else True # rbl_pred xs)"
-
-primrec (* result is length of first arg, second arg may be longer *)
- Nil : "rbl_add Nil x = Nil"
- Cons : "rbl_add (y # ys) x = (let ws = rbl_add ys (tl x) in
- (y ~= hd x) # (if hd x & y then rbl_succ ws else ws))"
-
-primrec (* result is length of first arg, second arg may be longer *)
- Nil : "rbl_mult Nil x = Nil"
- Cons : "rbl_mult (y # ys) x = (let ws = False # rbl_mult ys x in
- if y then rbl_add ws x else ws)"
-
lemma size_rbl_pred: "length (rbl_pred bl) = length bl"
by (induct bl) auto
@@ -947,8 +880,6 @@
(y --> P (rbl_add ws xs)) & (~ y --> P ws))"
by (clarsimp simp add : Let_def)
-subsection "Miscellaneous lemmas"
-
lemma and_len: "xs = ys ==> xs = ys & length xs = length ys"
by auto
@@ -961,6 +892,12 @@
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
@@ -980,6 +917,13 @@
"(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"]
lemmas tl_Nil = tl.simps (1)
@@ -1071,6 +1015,8 @@
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, bs, m, c) =
(if m = 0 \<or> n = 0
--- a/src/HOL/Word/BinGeneral.thy Tue Aug 28 19:45:45 2007 +0200
+++ b/src/HOL/Word/BinGeneral.thy Tue Aug 28 20:13:47 2007 +0200
@@ -9,53 +9,48 @@
header {* Basic Definitions for Binary Integers *}
-theory BinGeneral imports BinInduct Num_Lemmas
+theory BinGeneral imports Num_Lemmas
begin
-subsection {* BIT as a datatype constructor *}
-
-(** ways in which type Bin resembles a datatype **)
-
-lemmas BIT_eqI = conjI [THEN BIT_eq_iff [THEN iffD2]]
+subsection {* Recursion combinator for binary integers *}
-lemma neB1E [elim!]:
- assumes ne: "y \<noteq> bit.B1"
- assumes y: "y = bit.B0 \<Longrightarrow> P"
- shows "P"
- apply (rule y)
- apply (cases y rule: bit.exhaust, simp)
- apply (simp add: ne)
- done
-
-lemma bin_exhaust:
- assumes Q: "\<And>x b. bin = x BIT b \<Longrightarrow> Q"
- shows "Q"
- by (rule BIT_cases, rule Q)
-
-subsection {* Recursion combinator for binary integers *}
+lemma brlem: "(bin = Numeral.Min) = (- bin + Numeral.pred 0 = 0)"
+ unfolding Min_def pred_def by arith
function
bin_rec' :: "int * 'a * 'a * (int => bit => 'a => 'a) => 'a"
where
"bin_rec' (bin, f1, f2, f3) = (if bin = Numeral.Pls then f1
else if bin = Numeral.Min then f2
- else f3 (bin_rest bin) (bin_last bin)
- (bin_rec' (bin_rest bin, f1, f2, f3)))"
+ else case bin_rl bin of (w, b) => f3 w b (bin_rec' (w, f1, f2, f3)))"
by pat_completeness auto
termination
- by (relation "measure (size o fst)") simp_all
+ apply (relation "measure (nat o abs o fst)")
+ apply simp
+ apply (simp add: Pls_def brlem)
+ apply (clarsimp simp: bin_rl_char pred_def)
+ apply (frule thin_rl [THEN refl [THEN bin_abs_lem [rule_format]]])
+ apply (unfold Pls_def Min_def number_of_eq)
+ prefer 2
+ apply (erule asm_rl)
+ apply auto
+ done
constdefs
bin_rec :: "'a => 'a => (int => bit => 'a => 'a) => int => 'a"
"bin_rec f1 f2 f3 bin == bin_rec' (bin, f1, f2, f3)"
-lemma bin_rec_Pls: "bin_rec f1 f2 f3 Numeral.Pls = f1"
- unfolding bin_rec_def by simp
+lemma bin_rec_PM:
+ "f = bin_rec f1 f2 f3 ==> f Numeral.Pls = f1 & f Numeral.Min = f2"
+ apply safe
+ apply (unfold bin_rec_def)
+ apply (auto intro: bin_rec'.simps [THEN trans])
+ done
-lemma bin_rec_Min: "bin_rec f1 f2 f3 Numeral.Min = f2"
- unfolding bin_rec_def by simp
+lemmas bin_rec_Pls = refl [THEN bin_rec_PM, THEN conjunct1, standard]
+lemmas bin_rec_Min = refl [THEN bin_rec_PM, THEN conjunct2, standard]
lemma bin_rec_Bit:
"f = bin_rec f1 f2 f3 ==> f3 Numeral.Pls bit.B0 f1 = f1 ==>
@@ -64,23 +59,46 @@
apply (unfold bin_rec_def)
apply (rule bin_rec'.simps [THEN trans])
apply auto
+ apply (unfold Pls_def Min_def Bit_def)
+ apply (cases b, auto)+
done
lemmas bin_rec_simps = refl [THEN bin_rec_Bit] bin_rec_Pls bin_rec_Min
-subsection {* Sign of binary integers *}
+subsection {* Destructors for binary integers *}
consts
+ -- "corresponding operations analysing bins"
+ bin_last :: "int => bit"
+ bin_rest :: "int => int"
bin_sign :: "int => int"
+ bin_nth :: "int => nat => bool"
+
+primrec
+ Z : "bin_nth w 0 = (bin_last w = bit.B1)"
+ Suc : "bin_nth w (Suc n) = bin_nth (bin_rest w) n"
defs
+ bin_rest_def : "bin_rest w == fst (bin_rl w)"
+ bin_last_def : "bin_last w == snd (bin_rl w)"
bin_sign_def : "bin_sign == bin_rec Numeral.Pls Numeral.Min (%w b s. s)"
-lemmas bin_rest_simps =
- bin_rest_Pls bin_rest_Min bin_rest_BIT
+lemma bin_rl: "bin_rl w = (bin_rest w, bin_last w)"
+ unfolding bin_rest_def bin_last_def by auto
+
+lemmas bin_rl_simp [simp] = iffD1 [OF bin_rl_char bin_rl]
-lemmas bin_last_simps =
- bin_last_Pls bin_last_Min bin_last_BIT
+lemma bin_rest_simps [simp]:
+ "bin_rest Numeral.Pls = Numeral.Pls"
+ "bin_rest Numeral.Min = Numeral.Min"
+ "bin_rest (w BIT b) = w"
+ unfolding bin_rest_def by auto
+
+lemma bin_last_simps [simp]:
+ "bin_last Numeral.Pls = bit.B0"
+ "bin_last Numeral.Min = bit.B1"
+ "bin_last (w BIT b) = b"
+ unfolding bin_last_def by auto
lemma bin_sign_simps [simp]:
"bin_sign Numeral.Pls = Numeral.Pls"
@@ -105,31 +123,25 @@
lemma bin_last_mod:
"bin_last w = (if w mod 2 = 0 then bit.B0 else bit.B1)"
- apply (subgoal_tac "bin_last w =
- (if number_of w mod 2 = (0::int) then bit.B0 else bit.B1)")
- apply (simp only: number_of_is_id)
- apply (induct w rule: int_bin_induct, simp_all)
+ 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 (subgoal_tac "number_of (bin_rest w) = number_of w div (2::int)")
- apply (simp only: number_of_is_id)
- apply (induct w rule: int_bin_induct, simp_all)
+ 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
-subsection {* Testing bit positions *}
-
-consts
- bin_nth :: "int => nat => bool"
-
-primrec
- Z : "bin_nth w 0 = (bin_last w = bit.B1)"
- Suc : "bin_nth w (Suc n) = bin_nth (bin_rest w) n"
-
lemma bin_nth_lem [rule_format]:
"ALL y. bin_nth x = bin_nth y --> x = y"
apply (induct x rule: bin_induct)
@@ -232,7 +244,13 @@
apply (auto simp: even_def)
done
-text "Simplifications for (s)bintrunc"
+subsection "Simplifications for (s)bintrunc"
+
+lemma bit_bool:
+ "(b = (b' = bit.B1)) = (b' = (if b then bit.B1 else bit.B0))"
+ 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) = Numeral.Min) = bin_nth bin n"
--- a/src/HOL/Word/BinInduct.thy Tue Aug 28 19:45:45 2007 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,171 +0,0 @@
-(*
- ID: $Id$
- Author: Brian Huffman
-*)
-
-header {* Binary Integers as an Inductive Datatype *}
-
-theory BinInduct imports Main begin
-
-subsection {* Injectivity and distinctness of constructors *}
-
-lemma BIT_eq: "x BIT a = y BIT b \<Longrightarrow> x = y \<and> a = b"
- by (simp add: eq_number_of_BIT_BIT [unfolded number_of_is_id])
-
-lemma BIT_eq_iff: "(x BIT a = y BIT b) = (x = y \<and> a = b)"
- by (safe dest!: BIT_eq)
-
-lemma BIT_eq_Pls: "(w BIT b = Numeral.Pls) = (w = Numeral.Pls \<and> b = bit.B0)"
- by (subst Pls_0_eq [symmetric], simp only: BIT_eq_iff)
-
-lemma BIT_eq_Min: "(w BIT b = Numeral.Min) = (w = Numeral.Min \<and> b = bit.B1)"
- by (subst Min_1_eq [symmetric], simp only: BIT_eq_iff)
-
-lemma Pls_eq_BIT: "(Numeral.Pls = w BIT b) = (w = Numeral.Pls \<and> b = bit.B0)"
- by (subst eq_commute, rule BIT_eq_Pls)
-
-lemma Min_eq_BIT: "(Numeral.Min = w BIT b) = (w = Numeral.Min \<and> b = bit.B1)"
- by (subst eq_commute, rule BIT_eq_Min)
-
-lemma Min_neq_Pls: "Numeral.Min \<noteq> Numeral.Pls"
- unfolding Min_def Pls_def by simp
-
-lemma Pls_neq_Min: "Numeral.Pls \<noteq> Numeral.Min"
- unfolding Min_def Pls_def by simp
-
-lemmas bin_injects [simp] =
- BIT_eq_iff BIT_eq_Pls BIT_eq_Min
- Pls_eq_BIT Min_eq_BIT Min_neq_Pls Pls_neq_Min
-
-
-subsection {* Induction and case analysis *}
-
-inductive
- is_numeral :: "int \<Rightarrow> bool"
-where
- Pls: "is_numeral Numeral.Pls"
-| Min: "is_numeral Numeral.Min"
-| B0: "is_numeral z \<Longrightarrow> is_numeral (z BIT bit.B0)"
-| B1: "is_numeral z \<Longrightarrow> is_numeral (z BIT bit.B1)"
-
-lemma is_numeral_succ: "is_numeral z \<Longrightarrow> is_numeral (Numeral.succ z)"
- by (erule is_numeral.induct, simp_all add: is_numeral.intros)
-
-lemma is_numeral_pred: "is_numeral z \<Longrightarrow> is_numeral (Numeral.pred z)"
- by (erule is_numeral.induct, simp_all add: is_numeral.intros)
-
-lemma is_numeral_uminus: "is_numeral z \<Longrightarrow> is_numeral (uminus z)"
- by (erule is_numeral.induct, simp_all add: is_numeral.intros is_numeral_pred)
-
-lemma is_numeral_int: "is_numeral (int n)"
- apply (induct "n")
- apply (simp add: is_numeral.Pls [unfolded Numeral.Pls_def])
- apply (drule is_numeral_succ [unfolded Numeral.succ_def])
- apply (simp add: add_commute)
- done
-
-lemma is_numeral: "is_numeral z"
- by (induct "z") (simp_all only: is_numeral_int is_numeral_uminus)
-
-lemma int_bin_induct [case_names Pls Min B0 B1]:
- assumes Pls: "P Numeral.Pls"
- assumes Min: "P Numeral.Min"
- assumes B0: "\<And>x. \<lbrakk>P x; x \<noteq> Numeral.Pls\<rbrakk> \<Longrightarrow> P (x BIT bit.B0)"
- assumes B1: "\<And>x. \<lbrakk>P x; x \<noteq> Numeral.Min\<rbrakk> \<Longrightarrow> P (x BIT bit.B1)"
- shows "P x"
-proof (induct x rule: is_numeral.induct [OF is_numeral])
- from Pls show "P Numeral.Pls" .
- from Min show "P Numeral.Min" .
- fix z
- show "P z \<Longrightarrow> P (z BIT bit.B0)"
- by (cases "z = Numeral.Pls", auto intro: Pls B0)
- show "P z \<Longrightarrow> P (z BIT bit.B1)"
- by (cases "z = Numeral.Min", auto intro: Min B1)
-qed
-
-lemma bin_induct [case_names Pls Min Bit]:
- assumes Pls: "P Numeral.Pls"
- assumes Min: "P Numeral.Min"
- assumes Bit: "\<And>bin bit. P bin \<Longrightarrow> P (bin BIT bit)"
- shows "P x"
- by (induct x rule: int_bin_induct) (auto intro: assms)
-
-lemma BIT_exhausts: "\<exists>w b. x = w BIT b"
- by (induct x rule: bin_induct)
- (fast intro: Pls_0_eq [symmetric] Min_1_eq [symmetric])+
-
-lemma BIT_cases: "(\<And>w b. x = w BIT b \<Longrightarrow> Q) \<Longrightarrow> Q"
- by (insert BIT_exhausts [of x], auto)
-
-
-subsection {* Destructors for BIT *}
-
-definition
- bin_rest :: "int \<Rightarrow> int" where
- "bin_rest x = (THE w. \<exists>b. x = w BIT b)"
-
-definition
- bin_last :: "int \<Rightarrow> bit" where
- "bin_last x = (THE b. \<exists>w. x = w BIT b)"
-
-lemma bin_rest_BIT [simp]: "bin_rest (w BIT b) = w"
- by (unfold bin_rest_def, rule the_equality, fast, simp)
-
-lemma bin_rest_Pls [simp]: "bin_rest Numeral.Pls = Numeral.Pls"
- by (subst Pls_0_eq [symmetric], rule bin_rest_BIT)
-
-lemma bin_rest_Min [simp]: "bin_rest Numeral.Min = Numeral.Min"
- by (subst Min_1_eq [symmetric], rule bin_rest_BIT)
-
-lemma bin_last_BIT [simp]: "bin_last (w BIT b) = b"
- by (unfold bin_last_def, rule the_equality, fast, simp)
-
-lemma bin_last_Pls [simp]: "bin_last Numeral.Pls = bit.B0"
- by (subst Pls_0_eq [symmetric], rule bin_last_BIT)
-
-lemma bin_last_Min [simp]: "bin_last Numeral.Min = bit.B1"
- by (subst Min_1_eq [symmetric], rule bin_last_BIT)
-
-lemma bin_rest_BIT_bin_last [simp]: "(bin_rest x) BIT (bin_last x) = x"
- by (cases x rule: BIT_cases) simp
-
-lemma wf_bin_rest:
- "wf {(bin_rest w, w) |w. w \<noteq> Numeral.Pls \<and> w \<noteq> Numeral.Min}"
- apply (rule wfUNIVI, simp (no_asm_use))
- apply (rename_tac "z", induct_tac "z" rule: bin_induct)
- apply (drule spec, erule mp, simp)+
- done
-
-subsection {* Size function *}
-
-function
- binsize :: "int \<Rightarrow> nat"
-where
- "binsize z = (if z = Numeral.Pls \<or> z = Numeral.Min
- then 0 else Suc (binsize (bin_rest z)))"
- by pat_completeness simp
-
-termination binsize
- apply (relation "{(bin_rest w, w) |w. w \<noteq> Numeral.Pls \<and> w \<noteq> Numeral.Min}")
- apply (rule wf_bin_rest)
- apply simp
- done
-
-instance int :: size
- int_size_def: "size \<equiv> binsize" ..
-
-lemma int_size_simps [simp]:
- "size Numeral.Pls = 0"
- "size Numeral.Min = 0"
- "size (w BIT bit.B0) = (if w = Numeral.Pls then 0 else Suc (size w))"
- "size (w BIT bit.B1) = (if w = Numeral.Min then 0 else Suc (size w))"
- unfolding int_size_def by simp_all
-
-lemma size_bin_rest [simp]: "size (bin_rest w) = size w - 1"
- by (induct w rule: int_bin_induct) simp_all
-
-lemma int_size_gt_zero_iff [simp]:
- "(0 < size w) = (w \<noteq> Numeral.Pls \<and> w \<noteq> Numeral.Min)"
- by (induct w rule: int_bin_induct) simp_all
-
-end
--- a/src/HOL/Word/BinOperations.thy Tue Aug 28 19:45:45 2007 +0200
+++ b/src/HOL/Word/BinOperations.thy Tue Aug 28 20:13:47 2007 +0200
@@ -36,11 +36,11 @@
lemma int_xor_Pls [simp]:
"Numeral.Pls XOR x = x"
- unfolding int_xor_def by (simp add: bin_rec_Pls)
+ unfolding int_xor_def by (simp add: bin_rec_PM)
lemma int_xor_Min [simp]:
"Numeral.Min XOR x = NOT x"
- unfolding int_xor_def by (simp add: bin_rec_Min)
+ 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)"
@@ -66,11 +66,11 @@
lemma int_or_Pls [simp]:
"Numeral.Pls OR x = x"
- by (unfold int_or_def) (simp add: bin_rec_Pls)
+ by (unfold int_or_def) (simp add: bin_rec_PM)
lemma int_or_Min [simp]:
"Numeral.Min OR x = Numeral.Min"
- by (unfold int_or_def) (simp add: bin_rec_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)"
@@ -90,11 +90,11 @@
lemma int_and_Pls [simp]:
"Numeral.Pls AND x = Numeral.Pls"
- unfolding int_and_def by (simp add: bin_rec_Pls)
+ unfolding int_and_def by (simp add: bin_rec_PM)
lemma int_and_Min [simp]:
"Numeral.Min AND x = x"
- unfolding int_and_def by (simp add: bin_rec_Min)
+ 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)"
@@ -361,13 +361,10 @@
lemma bin_nth_sc_gen:
"!!w m. bin_nth (bin_sc n b w) m = (if m = n then b = bit.B1 else bin_nth w m)"
by (induct n) (case_tac [!] m, auto)
-
-lemma bit_bool1: "(if s = bit.B1 then bit.B1 else bit.B0) = s"
- by auto
lemma bin_sc_nth [simp]:
"!!w. (bin_sc n (If (bin_nth w n) bit.B1 bit.B0) w) = w"
- by (induct n) (auto simp add: bit_bool1)
+ by (induct n) auto
lemma bin_sign_sc [simp]:
"!!w. bin_sign (bin_sc n b w) = bin_sign w"
@@ -438,6 +435,49 @@
lemmas bin_sc_Suc_pred [simp] =
bin_sc_Suc_minus [of "number_of bin", simplified nobm1, standard]
+subsection {* Operations on lists of booleans *}
+
+consts
+ bin_to_bl :: "nat => int => bool list"
+ bin_to_bl_aux :: "nat => int => bool list => bool list"
+ bl_to_bin :: "bool list => int"
+ bl_to_bin_aux :: "int => bool list => int"
+
+ bl_of_nth :: "nat => (nat => bool) => bool list"
+
+primrec
+ Nil : "bl_to_bin_aux w [] = w"
+ Cons : "bl_to_bin_aux w (b # bs) =
+ bl_to_bin_aux (w BIT (if b then bit.B1 else bit.B0)) bs"
+
+primrec
+ 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 = bit.B1) # bl)"
+
+defs
+ bin_to_bl_def : "bin_to_bl n w == bin_to_bl_aux n w []"
+ bl_to_bin_def : "bl_to_bin bs == bl_to_bin_aux Numeral.Pls bs"
+
+primrec
+ Suc : "bl_of_nth (Suc n) f = f n # bl_of_nth n f"
+ Z : "bl_of_nth 0 f = []"
+
+consts
+ takefill :: "'a => nat => 'a list => 'a list"
+ app2 :: "('a => 'b => 'c) => 'a list => 'b list => 'c list"
+
+-- "takefill - like take but if argument list too short,"
+-- "extends result to get requested length"
+primrec
+ 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)"
+
+defs
+ app2_def : "app2 f as bs == map (split f) (zip as bs)"
+
subsection {* Splitting and concatenation *}
-- "rcat and rsplit"
--- a/src/HOL/Word/Examples/WordExamples.thy Tue Aug 28 19:45:45 2007 +0200
+++ b/src/HOL/Word/Examples/WordExamples.thy Tue Aug 28 20:13:47 2007 +0200
@@ -21,12 +21,12 @@
-- "number ring simps"
lemma
- "27 + 11 = (38::'a::finite word)"
+ "27 + 11 = (38::'a::len word)"
"27 + 11 = (6::5 word)"
- "7 * 3 = (21::'a::finite word)"
- "11 - 27 = (-16::'a::finite word)"
- "- -11 = (11::'a::finite word)"
- "-40 + 1 = (-39::'a::finite word)"
+ "7 * 3 = (21::'a::len word)"
+ "11 - 27 = (-16::'a::len word)"
+ "- -11 = (11::'a::len word)"
+ "-40 + 1 = (-39::'a::len word)"
by simp_all
lemma "word_pred 2 = 1" by simp
@@ -56,12 +56,12 @@
lemma "scast (0b1010 :: 4 word) = (0b111010 :: 6 word)" by simp
-- "reducing goals to nat or int and arith:"
-lemma "i < x ==> i < (i + 1 :: 'a :: finite word)" by unat_arith
-lemma "i < x ==> i < (i + 1 :: 'a :: finite word)" by uint_arith
+lemma "i < x ==> i < (i + 1 :: 'a :: len word)" by unat_arith
+lemma "i < x ==> i < (i + 1 :: 'a :: len word)" by uint_arith
-- "bool lists"
-lemma "of_bl [True, False, True, True] = (0b1011::'a::finite word)" by simp
+lemma "of_bl [True, False, True, True] = (0b1011::'a::len word)" by simp
lemma "to_bl (0b110::4 word) = [False, True, True, False]" by simp
@@ -92,21 +92,21 @@
lemma "(0b11000 :: 10 word) !! n = (n = 4 \<or> n = 3)"
by (auto simp add: bin_nth_Bit)
-lemma "set_bit 55 7 True = (183::'a word)" by simp
-lemma "set_bit 0b0010 7 True = (0b10000010::'a word)" by simp
-lemma "set_bit 0b0010 1 False = (0::'a word)" by simp
+lemma "set_bit 55 7 True = (183::'a::len0 word)" by simp
+lemma "set_bit 0b0010 7 True = (0b10000010::'a::len0 word)" by simp
+lemma "set_bit 0b0010 1 False = (0::'a::len0 word)" by simp
-lemma "lsb (0b0101::'a::finite word)" by simp
-lemma "\<not> lsb (0b1000::'a::finite word)" by simp
+lemma "lsb (0b0101::'a::len word)" by simp
+lemma "\<not> lsb (0b1000::'a::len word)" by simp
lemma "\<not> msb (0b0101::4 word)" by simp
lemma "msb (0b1000::4 word)" by simp
-lemma "word_cat (27::4 word) (27::8 word) = (2843::'a::finite word)" by simp
+lemma "word_cat (27::4 word) (27::8 word) = (2843::'a::len word)" by simp
lemma "word_cat (0b0011::4 word) (0b1111::6word) = (0b0011001111 :: 10 word)"
by simp
-lemma "0b1011 << 2 = (0b101100::'a word)" by simp
+lemma "0b1011 << 2 = (0b101100::'a::len0 word)" by simp
lemma "0b1011 >> 2 = (0b10::8 word)" by simp
lemma "0b1011 >>> 2 = (0b10::8 word)" by simp
--- a/src/HOL/Word/Num_Lemmas.thy Tue Aug 28 19:45:45 2007 +0200
+++ b/src/HOL/Word/Num_Lemmas.thy Tue Aug 28 20:13:47 2007 +0200
@@ -7,12 +7,37 @@
theory Num_Lemmas imports Parity begin
-(* lemmas funpow_0 = funpow.simps(1) *)
+lemma contentsI: "y = {x} ==> contents y = x"
+ unfolding contents_def by auto
+
+lemma prod_case_split: "prod_case = split"
+ by (rule ext)+ auto
+
+lemmas split_split = prod.split [unfolded prod_case_split]
+lemmas split_split_asm = prod.split_asm [unfolded prod_case_split]
+lemmas "split.splits" = split_split split_split_asm
+
+lemmas funpow_0 = funpow.simps(1)
lemmas funpow_Suc = funpow.simps(2)
-(* used by BinGeneral.funpow_minus_simp *)
+
+lemma nonemptyE: "S ~= {} ==> (!!x. x : S ==> R) ==> R"
+ apply (erule contrapos_np)
+ apply (rule equals0I)
+ apply auto
+ done
lemma gt_or_eq_0: "0 < y \<or> 0 = (y::nat)" by auto
+constdefs
+ mod_alt :: "'a => 'a => 'a :: Divides.div"
+ "mod_alt n m == n mod m"
+
+ -- "alternative way of defining @{text bin_last}, @{text bin_rest}"
+ bin_rl :: "int => int * bit"
+ "bin_rl w == SOME (r, l). w = r BIT l"
+
+declare iszero_0 [iff]
+
lemmas xtr1 = xtrans(1)
lemmas xtr2 = xtrans(2)
lemmas xtr3 = xtrans(3)
@@ -22,7 +47,13 @@
lemmas xtr7 = xtrans(7)
lemmas xtr8 = xtrans(8)
-lemmas PlsMin_defs (*[intro!]*) =
+lemma Min_ne_Pls [iff]:
+ "Numeral.Min ~= Numeral.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]
@@ -31,19 +62,36 @@
"False ==> number_of x = number_of y"
by auto
+lemmas nat_simps = diff_add_inverse2 diff_add_inverse
+lemmas nat_iffs = le_add1 le_add2
+
+lemma sum_imp_diff: "j = k + i ==> j - i = (k :: nat)"
+ by (clarsimp simp add: nat_simps)
+
lemma nobm1:
"0 < (number_of w :: nat) ==>
number_of w - (1 :: nat) = number_of (Numeral.pred w)"
apply (unfold nat_number_of_def One_nat_def nat_1 [symmetric] pred_def)
apply (simp add: number_of_eq nat_diff_distrib [symmetric])
done
-(* used in BinGeneral, BinOperations, BinBoolList *)
+
+lemma of_int_power:
+ "of_int (a ^ n) = (of_int a ^ n :: 'a :: {recpower, comm_ring_1})"
+ by (induct n) (auto simp add: power_Suc)
lemma zless2: "0 < (2 :: int)"
by auto
-lemmas zless2p [simp] = zless2 [THEN zero_less_power] (* keep *)
-lemmas zle2p [simp] = zless2p [THEN order_less_imp_le] (* keep *)
+lemmas zless2p [simp] = zless2 [THEN zero_less_power]
+lemmas zle2p [simp] = zless2p [THEN order_less_imp_le]
+
+lemmas pos_mod_sign2 = zless2 [THEN pos_mod_sign [where b = "2::int"]]
+lemmas pos_mod_bound2 = zless2 [THEN pos_mod_bound [where b = "2::int"]]
+
+-- "the inverse(s) of @{text number_of}"
+lemma nmod2: "n mod (2::int) = 0 | n mod 2 = 1"
+ using pos_mod_sign2 [of n] pos_mod_bound2 [of n]
+ unfolding mod_alt_def [symmetric] by auto
lemma emep1:
"even n ==> even d ==> 0 <= d ==> (n + 1) mod (d :: int) = (n mod d) + 1"
@@ -56,53 +104,192 @@
lemmas eme1p = emep1 [simplified add_commute]
+lemma le_diff_eq': "(a \<le> c - b) = (b + a \<le> (c::int))"
+ by (simp add: le_diff_eq add_commute)
+
+lemma less_diff_eq': "(a < c - b) = (b + a < (c::int))"
+ by (simp add: less_diff_eq add_commute)
+
lemma diff_le_eq': "(a - b \<le> c) = (a \<le> b + (c::int))"
by (simp add: diff_le_eq add_commute)
-(* used by BinGeneral.sb_dec_lem' *)
+
+lemma diff_less_eq': "(a - b < c) = (a < b + (c::int))"
+ by (simp add: diff_less_eq add_commute)
+
lemmas m1mod2k = zless2p [THEN zmod_minus1]
-(* used in WordArith *)
-
+lemmas m1mod22k = mult_pos_pos [OF zless2 zless2p, THEN zmod_minus1]
lemmas p1mod22k' = zless2p [THEN order_less_imp_le, THEN pos_zmod_mult_2]
+lemmas z1pmod2' = zero_le_one [THEN pos_zmod_mult_2, simplified]
+lemmas z1pdiv2' = zero_le_one [THEN pos_zdiv_mult_2, simplified]
lemma p1mod22k:
"(2 * b + 1) mod (2 * 2 ^ n) = 2 * (b mod 2 ^ n) + (1::int)"
by (simp add: p1mod22k' add_commute)
-(* used in BinOperations *)
+
+lemma z1pmod2:
+ "(2 * b + 1) mod 2 = (1::int)"
+ by (simp add: z1pmod2' add_commute)
+
+lemma z1pdiv2:
+ "(2 * b + 1) div 2 = (b::int)"
+ by (simp add: z1pdiv2' add_commute)
lemmas zdiv_le_dividend = xtr3 [OF zdiv_1 [symmetric] zdiv_mono2,
simplified int_one_le_iff_zero_less, simplified, standard]
-(* used in WordShift *)
+
+(** 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 = bit.B0 & c = bit.B1)"
+ unfolding Bit_def by (auto split: bit.split)
+
+lemma le_Bits:
+ "(v BIT b <= w BIT c) = (v < w | v <= w & (b ~= bit.B1 | c ~= bit.B0))"
+ unfolding Bit_def by (auto split: bit.split)
+
+lemma neB1E [elim!]:
+ assumes ne: "y \<noteq> bit.B1"
+ assumes y: "y = bit.B0 \<Longrightarrow> P"
+ shows "P"
+ apply (rule y)
+ apply (cases y rule: bit.exhaust, simp)
+ apply (simp add: ne)
+ done
+
+lemma bin_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
+
+lemma bin_rl_char: "(bin_rl w = (r, l)) = (r BIT l = w)"
+ apply (unfold bin_rl_def)
+ apply safe
+ apply (cases w rule: bin_exhaust)
+ apply auto
+ done
+
+lemmas bin_rl_simps [THEN bin_rl_char [THEN iffD2], standard, simp] =
+ Pls_0_eq Min_1_eq refl
+
+lemma bin_abs_lem:
+ "bin = (w BIT b) ==> ~ bin = Numeral.Min --> ~ bin = Numeral.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 Numeral.Pls"
+ and PMin: "P Numeral.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 no_no [simp]: "number_of (number_of i) = i"
+ unfolding number_of_eq by simp
lemma Bit_B0:
"k BIT bit.B0 = k + k"
by (unfold Bit_def) simp
+lemma Bit_B1:
+ "k BIT bit.B1 = k + k + 1"
+ by (unfold Bit_def) simp
+
lemma Bit_B0_2t: "k BIT bit.B0 = 2 * k"
by (rule trans, rule Bit_B0) simp
-(* used in BinOperations *)
+
+lemma Bit_B1_2t: "k BIT bit.B1 = 2 * k + 1"
+ by (rule trans, rule Bit_B1) simp
+
+lemma B_mod_2':
+ "X = 2 ==> (w BIT bit.B1) mod X = 1 & (w BIT bit.B0) mod X = 0"
+ apply (simp (no_asm) only: Bit_B0 Bit_B1)
+ apply (simp add: z1pmod2)
+ done
+
+lemmas B1_mod_2 [simp] = B_mod_2' [OF refl, THEN conjunct1, standard]
+lemmas B0_mod_2 [simp] = B_mod_2' [OF refl, THEN conjunct2, standard]
+
+lemma axxbyy:
+ "a + m + m = b + n + n ==> (a = 0 | a = 1) ==> (b = 0 | b = 1) ==>
+ a = b & m = (n :: int)"
+ apply auto
+ apply (drule_tac f="%n. n mod 2" in arg_cong)
+ apply (clarsimp simp: z1pmod2)
+ apply (drule_tac f="%n. n mod 2" in arg_cong)
+ apply (clarsimp simp: z1pmod2)
+ done
+
+lemma axxmod2:
+ "(1 + x + x) mod 2 = (1 :: int) & (0 + x + x) mod 2 = (0 :: int)"
+ by simp (rule z1pmod2)
+
+lemma axxdiv2:
+ "(1 + x + x) div 2 = (x :: int) & (0 + x + x) div 2 = (x :: int)"
+ by simp (rule z1pdiv2)
+
+lemmas iszero_minus = trans [THEN trans,
+ OF iszero_def neg_equal_0_iff_equal iszero_def [symmetric], standard]
lemmas zadd_diff_inverse = trans [OF diff_add_cancel [symmetric] add_commute,
standard]
-(* used in WordArith *)
lemmas add_diff_cancel2 = add_commute [THEN diff_eq_eq [THEN iffD2], standard]
-(* used in WordShift *)
lemma zmod_uminus: "- ((a :: int) mod b) mod b = -a mod b"
by (simp add : zmod_zminus1_eq_if)
-(* used in BinGeneral *)
+
+lemma zmod_zsub_distrib: "((a::int) - b) mod c = (a mod c - b mod c) mod c"
+ apply (unfold diff_int_def)
+ apply (rule trans [OF _ zmod_zadd1_eq [symmetric]])
+ apply (simp add: zmod_uminus zmod_zadd1_eq [symmetric])
+ done
lemma zmod_zsub_right_eq: "((a::int) - b) mod c = (a - b mod c) mod c"
apply (unfold diff_int_def)
apply (rule trans [OF _ zmod_zadd_right_eq [symmetric]])
apply (simp add : zmod_uminus zmod_zadd_right_eq [symmetric])
done
-(* used in BinGeneral, WordGenLib *)
lemmas zmod_zsub_left_eq =
zmod_zadd_left_eq [where b = "- ?b", simplified diff_int_def [symmetric]]
-(* used in BinGeneral, WordGenLib *)
lemma zmod_zsub_self [simp]:
"((b :: int) - a) mod a = b mod a"
@@ -114,12 +301,10 @@
apply (subst zmod_zmult1_eq)
apply simp
done
-(* used in BinGeneral *)
lemmas rdmods [symmetric] = zmod_uminus [symmetric]
zmod_zsub_left_eq zmod_zsub_right_eq zmod_zadd_left_eq
zmod_zadd_right_eq zmod_zmult1_eq zmod_zmult1_eq_rev
-(* used in WordArith, WordShift *)
lemma mod_plus_right:
"((a + x) mod m = (b + x) mod m) = (a mod m = b mod (m :: nat))"
@@ -128,12 +313,27 @@
apply arith
done
+lemma nat_minus_mod: "(n - n mod m) mod m = (0 :: nat)"
+ by (induct n) (simp_all add : mod_Suc)
+
+lemmas nat_minus_mod_plus_right = trans [OF nat_minus_mod mod_0 [symmetric],
+ THEN mod_plus_right [THEN iffD2], standard, simplified]
+
+lemmas push_mods' = zmod_zadd1_eq [standard]
+ zmod_zmult_distrib [standard] zmod_zsub_distrib [standard]
+ zmod_uminus [symmetric, standard]
+
+lemmas push_mods = push_mods' [THEN eq_reflection, standard]
+lemmas pull_mods = push_mods [symmetric] rdmods [THEN eq_reflection, standard]
+lemmas mod_simps =
+ zmod_zmult_self1 [THEN eq_reflection] zmod_zmult_self2 [THEN eq_reflection]
+ mod_mod_trivial [THEN eq_reflection]
+
lemma nat_mod_eq:
"!!b. b < n ==> a mod n = b mod n ==> a mod n = (b :: nat)"
by (induct a) auto
lemmas nat_mod_eq' = refl [THEN [2] nat_mod_eq]
-(* used in WordArith, WordGenLib *)
lemma nat_mod_lem:
"(0 :: nat) < n ==> b < n = (b mod n = b)"
@@ -142,7 +342,6 @@
apply (erule subst)
apply (erule mod_less_divisor)
done
-(* used in WordArith *)
lemma mod_nat_add:
"(x :: nat) < z ==> y < z ==>
@@ -155,7 +354,10 @@
apply (rule nat_mod_eq')
apply arith
done
-(* used in WordArith, WordGenLib *)
+
+lemma mod_nat_sub:
+ "(x :: nat) < z ==> (x - y) mod z = x - y"
+ by (rule nat_mod_eq') arith
lemma int_mod_lem:
"(0 :: int) < n ==> (0 <= b & b < n) = (b mod n = b)"
@@ -164,14 +366,12 @@
apply (erule_tac [!] subst)
apply auto
done
-(* used in WordDefinition, WordArith, WordShift *)
lemma int_mod_eq:
"(0 :: int) <= b ==> b < n ==> a mod n = b mod n ==> a mod n = b"
by clarsimp (rule mod_pos_pos_trivial)
lemmas int_mod_eq' = refl [THEN [3] int_mod_eq]
-(* used in WordDefinition, WordArith, WordShift, WordGenLib *)
lemma int_mod_le: "0 <= a ==> 0 < (n :: int) ==> a mod n <= a"
apply (cases "a < n")
@@ -195,15 +395,88 @@
"(x :: int) < z ==> y < z ==> 0 <= y ==> 0 <= x ==> 0 <= z ==>
(x + y) mod z = (if x + y < z then x + y else x + y - z)"
by (auto intro: int_mod_eq)
-(* used in WordArith, WordGenLib *)
lemma mod_sub_if_z:
"(x :: int) < z ==> y < z ==> 0 <= y ==> 0 <= x ==> 0 <= z ==>
(x - y) mod z = (if y <= x then x - y else x - y + z)"
by (auto intro: int_mod_eq)
-(* used in WordArith, WordGenLib *)
+
+lemmas zmde = zmod_zdiv_equality [THEN diff_eq_eq [THEN iffD2], symmetric]
+lemmas mcl = mult_cancel_left [THEN iffD1, THEN make_pos_rule]
+
+(* already have this for naturals, div_mult_self1/2, but not for ints *)
+lemma zdiv_mult_self: "m ~= (0 :: int) ==> (a + m * n) div m = a div m + n"
+ apply (rule mcl)
+ prefer 2
+ apply (erule asm_rl)
+ apply (simp add: zmde ring_distribs)
+ apply (simp add: push_mods)
+ done
+
+(** Rep_Integ **)
+lemma eqne: "equiv A r ==> X : A // r ==> X ~= {}"
+ unfolding equiv_def refl_def quotient_def Image_def by auto
+
+lemmas Rep_Integ_ne = Integ.Rep_Integ
+ [THEN equiv_intrel [THEN eqne, simplified Integ_def [symmetric]], standard]
+
+lemmas riq = Integ.Rep_Integ [simplified Integ_def]
+lemmas intrel_refl = refl [THEN equiv_intrel_iff [THEN iffD1], standard]
+lemmas Rep_Integ_equiv = quotient_eq_iff
+ [OF equiv_intrel riq riq, simplified Integ.Rep_Integ_inject, standard]
+lemmas Rep_Integ_same =
+ Rep_Integ_equiv [THEN intrel_refl [THEN rev_iffD2], standard]
+
+lemma RI_int: "(a, 0) : Rep_Integ (int a)"
+ unfolding int_def by auto
+
+lemmas RI_intrel [simp] = UNIV_I [THEN quotientI,
+ THEN Integ.Abs_Integ_inverse [simplified Integ_def], standard]
+
+lemma RI_minus: "(a, b) : Rep_Integ x ==> (b, a) : Rep_Integ (- x)"
+ apply (rule_tac z=x in eq_Abs_Integ)
+ apply (clarsimp simp: minus)
+ done
-lemmas mcl = mult_cancel_left [THEN iffD1, THEN make_pos_rule]
+lemma RI_add:
+ "(a, b) : Rep_Integ x ==> (c, d) : Rep_Integ y ==>
+ (a + c, b + d) : Rep_Integ (x + y)"
+ apply (rule_tac z=x in eq_Abs_Integ)
+ apply (rule_tac z=y in eq_Abs_Integ)
+ apply (clarsimp simp: add)
+ done
+
+lemma mem_same: "a : S ==> a = b ==> b : S"
+ by fast
+
+(* two alternative proofs of this *)
+lemma RI_eq_diff': "(a, b) : Rep_Integ (int a - int b)"
+ apply (unfold diff_def)
+ apply (rule mem_same)
+ apply (rule RI_minus RI_add RI_int)+
+ apply simp
+ done
+
+lemma RI_eq_diff: "((a, b) : Rep_Integ x) = (int a - int b = x)"
+ apply safe
+ apply (rule Rep_Integ_same)
+ prefer 2
+ apply (erule asm_rl)
+ apply (rule RI_eq_diff')+
+ done
+
+lemma mod_power_lem:
+ "a > 1 ==> a ^ n mod a ^ m = (if m <= n then 0 else (a :: int) ^ n)"
+ apply clarsimp
+ apply safe
+ apply (simp add: zdvd_iff_zmod_eq_0 [symmetric])
+ apply (drule le_iff_add [THEN iffD1])
+ apply (force simp: zpower_zadd_distrib)
+ apply (rule mod_pos_pos_trivial)
+ apply (simp add: zero_le_power)
+ apply (rule power_strict_increasing)
+ apply auto
+ done
lemma min_pm [simp]: "min a b + (a - b) = (a :: nat)"
by arith
@@ -215,14 +488,40 @@
lemmas rev_min_pm1 [simp] = trans [OF add_commute rev_min_pm]
+lemma pl_pl_rels:
+ "a + b = c + d ==>
+ a >= c & b <= d | a <= c & b >= (d :: nat)"
+ apply (cut_tac n=a and m=c in nat_le_linear)
+ apply (safe dest!: le_iff_add [THEN iffD1])
+ apply arith+
+ done
+
+lemmas pl_pl_rels' = add_commute [THEN [2] trans, THEN pl_pl_rels]
+
+lemma minus_eq: "(m - k = m) = (k = 0 | m = (0 :: nat))"
+ by arith
+
+lemma pl_pl_mm: "(a :: nat) + b = c + d ==> a - c = d - b"
+ by arith
+
+lemmas pl_pl_mm' = add_commute [THEN [2] trans, THEN pl_pl_mm]
+
lemma min_minus [simp] : "min m (m - k) = (m - k :: nat)"
by arith
lemmas min_minus' [simp] = trans [OF min_max.inf_commute min_minus]
+lemma nat_no_eq_iff:
+ "(number_of b :: int) >= 0 ==> (number_of c :: int) >= 0 ==>
+ (number_of b = (number_of c :: nat)) = (b = c)"
+ apply (unfold nat_number_of_def)
+ apply safe
+ apply (drule (2) eq_nat_nat_iff [THEN iffD1])
+ apply (simp add: number_of_eq)
+ done
+
lemmas dme = box_equals [OF div_mod_equality add_0_right add_0_right]
lemmas dtle = xtr3 [OF dme [symmetric] le_add1]
-(* used in WordShift *)
lemmas th2 = order_trans [OF order_refl [THEN [2] mult_le_mono] dtle]
lemma td_gal:
@@ -233,7 +532,6 @@
done
lemmas td_gal_lt = td_gal [simplified le_def, simplified]
-(* used in WordShift *)
lemma div_mult_le: "(a :: nat) div b * b <= a"
apply (cases b)
@@ -241,7 +539,6 @@
apply (rule order_refl [THEN th2])
apply auto
done
-(* used in WordArith *)
lemmas sdl = split_div_lemma [THEN iffD1, symmetric]
@@ -256,8 +553,22 @@
apply (rule_tac f="%n. n div f" in arg_cong)
apply (simp add : mult_ac)
done
-(* used in WordShift *)
+lemma diff_mod_le: "(a::nat) < d ==> b dvd d ==> a - a mod b <= d - b"
+ apply (unfold dvd_def)
+ apply clarify
+ apply (case_tac k)
+ apply clarsimp
+ apply clarify
+ apply (cases "b > 0")
+ apply (drule mult_commute [THEN xtr1])
+ apply (frule (1) td_gal_lt [THEN iffD1])
+ apply (clarsimp simp: le_simps)
+ apply (rule mult_div_cancel [THEN [2] xtr4])
+ apply (rule mult_mono)
+ apply auto
+ done
+
lemma less_le_mult':
"w * c < b * c ==> 0 \<le> c ==> (w + 1) * c \<le> b * (c::int)"
apply (rule mult_right_mono)
@@ -267,7 +578,9 @@
done
lemmas less_le_mult = less_le_mult' [simplified left_distrib, simplified]
-(* used in WordArith *)
+
+lemmas less_le_mult_minus = iffD2 [OF le_diff_eq less_le_mult,
+ simplified left_diff_distrib, standard]
lemma lrlem':
assumes d: "(i::nat) \<le> j \<or> m < j'"
@@ -290,33 +603,20 @@
apply arith
apply simp
done
-(* used in BinBoolList *)
lemma gen_minus: "0 < n ==> f n = f (Suc (n - 1))"
by auto
-(* used in BinGeneral *)
lemma mpl_lem: "j <= (i :: nat) ==> k < j ==> i - j + k < i"
apply (induct i, clarsimp)
apply (cases j, clarsimp)
apply arith
done
-(* used in WordShift *)
-subsection "if simps"
-
-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_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
-(* used in WordBitwise *)
+lemma nonneg_mod_div:
+ "0 <= a ==> 0 <= b ==> 0 <= (a mod b :: int) & 0 <= a div b"
+ apply (cases "b = 0", clarsimp)
+ apply (auto intro: pos_imp_zdiv_nonneg_iff [THEN iffD2])
+ done
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Word/Size.thy Tue Aug 28 20:13:47 2007 +0200
@@ -0,0 +1,54 @@
+(*
+ ID: $Id$
+ Author: John Matthews, Galois Connections, Inc., copyright 2006
+
+ A typeclass for parameterizing types by size.
+ Used primarily to parameterize machine word sizes.
+*)
+theory Size
+imports Numeral_Type
+begin
+
+text {*
+ The aim of this is to allow any type as index type, but to provide a
+ default instantiation for numeral types. This independence requires
+ some duplication with the definitions in Numeral\_Type.
+*}
+axclass len0 < type
+
+consts
+ len_of :: "('a :: len0 itself) => nat"
+
+text {*
+ Some theorems are only true on words with length greater 0.
+*}
+axclass len < len0
+ len_gt_0 [iff]: "0 < len_of TYPE ('a :: len0)"
+
+instance num0 :: len0 ..
+instance num1 :: len0 ..
+instance bit0 :: (len0) len0 ..
+instance bit1 :: (len0) len0 ..
+
+defs (overloaded)
+ len_num0: "len_of (x::num0 itself) == 0"
+ len_num1: "len_of (x::num1 itself) == 1"
+ len_bit0: "len_of (x::'a::len0 bit0 itself) == 2 * len_of TYPE ('a)"
+ len_bit1: "len_of (x::'a::len0 bit1 itself) == 2 * len_of TYPE ('a) + 1"
+
+lemmas len_of_numeral_defs [simp] = len_num0 len_num1 len_bit0 len_bit1
+
+instance num1 :: len by (intro_classes) simp
+instance bit0 :: (len) len by (intro_classes) simp
+instance bit1 :: (len0) len by (intro_classes) simp
+
+-- "Examples:"
+lemma "len_of TYPE(17) = 17" by simp
+lemma "len_of TYPE(0) = 0" by simp
+
+-- "not simplified:"
+lemma "len_of TYPE('a::len0) = x"
+ oops
+
+end
+
--- a/src/HOL/Word/WordArith.thy Tue Aug 28 19:45:45 2007 +0200
+++ b/src/HOL/Word/WordArith.thy Tue Aug 28 20:13:47 2007 +0200
@@ -11,10 +11,46 @@
theory WordArith imports WordDefinition begin
+
+lemma word_less_alt: "(a < b) = (uint a < uint b)"
+ unfolding word_less_def word_le_def
+ by (auto simp del: word_uint.Rep_inject
+ simp: word_uint.Rep_inject [symmetric])
+
+lemma signed_linorder: "linorder word_sle word_sless"
+ apply unfold_locales
+ apply (unfold word_sle_def word_sless_def)
+ by auto
+
+interpretation signed: linorder ["word_sle" "word_sless"]
+ by (rule signed_linorder)
+
lemmas word_arith_wis [THEN meta_eq_to_obj_eq] =
word_add_def word_mult_def word_minus_def
word_succ_def word_pred_def word_0_wi word_1_wi
+lemma udvdI:
+ "0 \<le> n ==> uint b = n * uint a ==> a udvd b"
+ by (auto simp: udvd_def)
+
+lemmas word_div_no [simp] =
+ word_div_def [of "number_of ?a" "number_of ?b"]
+
+lemmas word_mod_no [simp] =
+ word_mod_def [of "number_of ?a" "number_of ?b"]
+
+lemmas word_less_no [simp] =
+ word_less_def [of "number_of ?a" "number_of ?b"]
+
+lemmas word_le_no [simp] =
+ word_le_def [of "number_of ?a" "number_of ?b"]
+
+lemmas word_sless_no [simp] =
+ word_sless_def [of "number_of ?a" "number_of ?b"]
+
+lemmas word_sle_no [simp] =
+ word_sle_def [of "number_of ?a" "number_of ?b"]
+
(* following two are available in class number_ring,
but convenient to have them here here;
note - the number_ring versions, numeral_0_eq_0 and numeral_1_eq_1
@@ -29,7 +65,7 @@
unfolding Pls_def Bit_def by auto
lemma word_1_no:
- "(1 :: 'a word) == number_of (Numeral.Pls BIT bit.B1)"
+ "(1 :: 'a :: len0 word) == number_of (Numeral.Pls BIT bit.B1)"
unfolding word_1_wi word_number_of_def int_one_bin by auto
lemma word_m1_wi: "-1 == word_of_int -1"
@@ -38,10 +74,25 @@
lemma word_m1_wi_Min: "-1 = word_of_int Numeral.Min"
by (simp add: word_m1_wi number_of_eq)
+lemma word_0_bl: "of_bl [] = 0"
+ unfolding word_0_wi of_bl_def by (simp add : Pls_def)
+
+lemma word_1_bl: "of_bl [True] = 1"
+ unfolding word_1_wi of_bl_def
+ by (simp add : bl_to_bin_def Bit_def Pls_def)
+
lemma uint_0 [simp] : "(uint 0 = 0)"
unfolding word_0_wi
by (simp add: word_ubin.eq_norm Pls_def [symmetric])
+lemma of_bl_0 [simp] : "of_bl (replicate n False) = 0"
+ by (simp add : word_0_wi of_bl_def bl_to_bin_rep_False Pls_def)
+
+lemma to_bl_0:
+ "to_bl (0::'a::len0 word) = replicate (len_of TYPE('a)) False"
+ unfolding uint_bl
+ by (simp add : word_size bin_to_bl_Pls Pls_def [symmetric])
+
lemma uint_0_iff: "(uint x = 0) = (x = 0)"
by (auto intro!: word_uint.Rep_eqD)
@@ -51,7 +102,7 @@
lemma unat_0 [simp]: "unat 0 = 0"
unfolding unat_def by auto
-lemma size_0_same': "size w = 0 ==> w = (v :: 'a word)"
+lemma size_0_same': "size w = 0 ==> w = (v :: 'a :: len0 word)"
apply (unfold word_size)
apply (rule box_equals)
defer
@@ -95,14 +146,14 @@
apply (rule refl)
done
-lemma uint_1 [simp] : "uint (1 :: 'a :: finite word) = 1"
+lemma uint_1 [simp] : "uint (1 :: 'a :: len word) = 1"
unfolding word_1_wi
by (simp add: word_ubin.eq_norm int_one_bin bintrunc_minus_simps)
-lemma unat_1 [simp] : "unat (1 :: 'a :: finite word) = 1"
+lemma unat_1 [simp] : "unat (1 :: 'a :: len word) = 1"
by (unfold unat_def uint_1) auto
-lemma ucast_1 [simp] : "ucast (1 :: 'a :: finite word) = 1"
+lemma ucast_1 [simp] : "ucast (1 :: 'a :: len word) = 1"
unfolding ucast_def word_1_wi
by (simp add: word_ubin.eq_norm int_one_bin bintrunc_minus_simps)
@@ -124,8 +175,9 @@
lemmas wi_hom_syms = wi_homs [symmetric]
-lemma word_sub_def: "a - b == a + - (b :: 'a word)"
- by (rule diff_def)
+lemma word_sub_def: "a - b == a + - (b :: 'a :: len0 word)"
+ unfolding word_sub_wi diff_def
+ by (simp only : word_uint.Rep_inverse wi_hom_syms)
lemmas word_diff_minus = word_sub_def [THEN meta_eq_to_obj_eq, standard]
@@ -192,7 +244,12 @@
lemmas sint_word_ariths = uint_word_arith_bintrs
[THEN uint_sint [symmetric, THEN trans],
unfolded uint_sint bintr_arith1s bintr_ariths
- zero_less_card_finite [THEN bin_sbin_eq_iff'] word_sbin.norm_Rep, standard]
+ len_gt_0 [THEN bin_sbin_eq_iff'] word_sbin.norm_Rep, standard]
+
+lemmas uint_div_alt = word_div_def
+ [THEN meta_eq_to_obj_eq [THEN trans [OF uint_cong int_word_uint]], standard]
+lemmas uint_mod_alt = word_mod_def
+ [THEN meta_eq_to_obj_eq [THEN trans [OF uint_cong int_word_uint]], standard]
lemma word_pred_0_n1: "word_pred 0 = word_of_int -1"
unfolding word_pred_def number_of_eq
@@ -218,65 +275,70 @@
"\<exists>y. x = word_of_int y"
by (rule_tac x="uint x" in exI) simp
+lemma word_arith_eqs:
+ fixes a :: "'a::len0 word"
+ fixes b :: "'a::len0 word"
+ shows
+ word_add_0: "0 + a = a" and
+ word_add_0_right: "a + 0 = a" and
+ word_mult_1: "1 * a = a" and
+ word_mult_1_right: "a * 1 = a" and
+ word_add_commute: "a + b = b + a" and
+ word_add_assoc: "a + b + c = a + (b + c)" and
+ word_add_left_commute: "a + (b + c) = b + (a + c)" and
+ word_mult_commute: "a * b = b * a" and
+ word_mult_assoc: "a * b * c = a * (b * c)" and
+ word_mult_left_commute: "a * (b * c) = b * (a * c)" and
+ word_left_distrib: "(a + b) * c = a * c + b * c" and
+ word_right_distrib: "a * (b + c) = a * b + a * c" and
+ word_left_minus: "- a + a = 0" and
+ word_diff_0_right: "a - 0 = a" and
+ word_diff_self: "a - a = 0"
+ using word_of_int_Ex [of a]
+ word_of_int_Ex [of b]
+ word_of_int_Ex [of c]
+ by (auto simp: word_of_int_hom_syms [symmetric]
+ zadd_0_right add_commute add_assoc add_left_commute
+ mult_commute mult_assoc mult_left_commute
+ plus_times.left_distrib plus_times.right_distrib)
+
+lemmas word_add_ac = word_add_commute word_add_assoc word_add_left_commute
+lemmas word_mult_ac = word_mult_commute word_mult_assoc word_mult_left_commute
+
+lemmas word_plus_ac0 = word_add_0 word_add_0_right word_add_ac
+lemmas word_times_ac1 = word_mult_1 word_mult_1_right word_mult_ac
+
+
subsection "Order on fixed-length words"
-instance word :: (type) ord
- word_le_def: "a <= b == uint a <= uint b"
- word_less_def: "x < y == x <= y & x ~= y"
- ..
-
-constdefs
- word_sle :: "'a :: finite word => 'a word => bool" ("(_/ <=s _)" [50, 51] 50)
- "a <=s b == sint a <= sint b"
-
- word_sless :: "'a :: finite word => 'a word => bool" ("(_/ <s _)" [50, 51] 50)
- "(x <s y) == (x <=s y & x ~= y)"
-
-lemma word_less_alt: "(a < b) = (uint a < uint b)"
- unfolding word_less_def word_le_def
- by (auto simp del: word_uint.Rep_inject
- simp: word_uint.Rep_inject [symmetric])
-
-lemma signed_linorder: "linorder word_sle word_sless"
- apply unfold_locales
- apply (unfold word_sle_def word_sless_def)
- by auto
-
-interpretation signed: linorder ["word_sle" "word_sless"]
- by (rule signed_linorder)
-
-lemmas word_less_no [simp] =
- word_less_def [of "number_of ?a" "number_of ?b"]
-
-lemmas word_le_no [simp] =
- word_le_def [of "number_of ?a" "number_of ?b"]
-
-lemmas word_sless_no [simp] =
- word_sless_def [of "number_of ?a" "number_of ?b"]
-
-lemmas word_sle_no [simp] =
- word_sle_def [of "number_of ?a" "number_of ?b"]
-
-lemma word_order_trans: "x <= y ==> y <= z ==> x <= (z :: 'a word)"
+lemma word_order_trans: "x <= y ==> y <= z ==> x <= (z :: 'a :: len0 word)"
unfolding word_le_def by auto
-lemma word_order_refl: "z <= (z :: 'a word)"
+lemma word_order_refl: "z <= (z :: 'a :: len0 word)"
unfolding word_le_def by auto
-lemma word_order_antisym: "x <= y ==> y <= x ==> x = (y :: 'a word)"
+lemma word_order_antisym: "x <= y ==> y <= x ==> x = (y :: 'a :: len0 word)"
unfolding word_le_def by (auto intro!: word_uint.Rep_eqD)
lemma word_order_linear:
- "y <= x | x <= (y :: 'a word)"
+ "y <= x | x <= (y :: 'a :: len0 word)"
unfolding word_le_def by auto
lemma word_zero_le [simp] :
- "0 <= (y :: 'a word)"
+ "0 <= (y :: 'a :: len0 word)"
unfolding word_le_def by auto
+
+instance word :: (len0) semigroup_add
+ by intro_classes (simp add: word_add_assoc)
-instance word :: (type) linorder
+instance word :: (len0) linorder
by intro_classes (auto simp: word_less_def word_le_def)
+instance word :: (len0) ring
+ by intro_classes
+ (auto simp: word_arith_eqs word_diff_minus
+ word_diff_self [unfolded word_diff_minus])
+
lemma word_m1_ge [simp] : "word_pred 0 >= y"
unfolding word_le_def
by (simp only : word_pred_0_n1 word_uint.eq_norm m1mod2k) auto
@@ -286,7 +348,7 @@
lemmas word_not_simps [simp] =
word_zero_le [THEN leD] word_m1_ge [THEN leD] word_n1_ge [THEN leD]
-lemma word_gt_0: "0 < y = (0 ~= (y :: 'a word))"
+lemma word_gt_0: "0 < y = (0 ~= (y :: 'a :: len0 word))"
unfolding word_less_def by auto
lemmas word_gt_0_no [simp] = word_gt_0 [of "number_of ?y"]
@@ -304,28 +366,15 @@
by (rule nat_less_eq_zless [symmetric]) simp
lemma wi_less:
- "(word_of_int n < (word_of_int m :: 'a word)) =
- (n mod 2 ^ CARD('a) < m mod 2 ^ CARD('a))"
+ "(word_of_int n < (word_of_int m :: 'a :: len0 word)) =
+ (n mod 2 ^ len_of TYPE('a) < m mod 2 ^ len_of TYPE('a))"
unfolding word_less_alt by (simp add: word_uint.eq_norm)
lemma wi_le:
- "(word_of_int n <= (word_of_int m :: 'a word)) =
- (n mod 2 ^ CARD('a) <= m mod 2 ^ CARD('a))"
+ "(word_of_int n <= (word_of_int m :: 'a :: len0 word)) =
+ (n mod 2 ^ len_of TYPE('a) <= m mod 2 ^ len_of TYPE('a))"
unfolding word_le_def by (simp add: word_uint.eq_norm)
-lemmas unat_mono = word_less_nat_alt [THEN iffD1, standard]
-
-
-subsection "Divisibility"
-
-definition
- udvd :: "'a::finite word \<Rightarrow> 'a word \<Rightarrow> bool" (infixl "udvd" 50) where
- "a udvd b \<equiv> \<exists>n\<ge>0. uint b = n * uint a"
-
-lemma udvdI:
- "0 \<le> n ==> uint b = n * uint a ==> a udvd b"
- by (auto simp: udvd_def)
-
lemma udvd_nat_alt: "a udvd b = (EX n>=0. unat b = n * unat a)"
apply (unfold udvd_def)
apply safe
@@ -342,31 +391,13 @@
lemma udvd_iff_dvd: "x udvd y <-> unat x dvd unat y"
unfolding dvd_def udvd_nat_alt by force
-
-subsection "Division with remainder"
-
-instance word :: (type) Divides.div
- word_div_def: "a div b == word_of_int (uint a div uint b)"
- word_mod_def: "a mod b == word_of_int (uint a mod uint b)"
- ..
-
-lemmas word_div_no [simp] =
- word_div_def [of "number_of ?a" "number_of ?b"]
+lemmas unat_mono = word_less_nat_alt [THEN iffD1, standard]
-lemmas word_mod_no [simp] =
- word_mod_def [of "number_of ?a" "number_of ?b"]
-
-lemmas uint_div_alt = word_div_def
- [THEN meta_eq_to_obj_eq [THEN trans [OF uint_cong int_word_uint]], standard]
-lemmas uint_mod_alt = word_mod_def
- [THEN meta_eq_to_obj_eq [THEN trans [OF uint_cong int_word_uint]], standard]
-
-
-lemma word_zero_neq_one: "0 < CARD('a) ==> (0 :: 'a word) ~= 1";
+lemma word_zero_neq_one: "0 < len_of TYPE ('a :: len0) ==> (0 :: 'a word) ~= 1";
unfolding word_arith_wis
by (auto simp add: word_ubin.norm_eq_iff [symmetric] gr0_conv_Suc)
-lemmas lenw1_zero_neq_one = zero_less_card_finite [THEN word_zero_neq_one]
+lemmas lenw1_zero_neq_one = len_gt_0 [THEN word_zero_neq_one]
lemma no_no [simp] : "number_of (number_of b) = number_of b"
by (simp add: number_of_eq)
@@ -402,21 +433,21 @@
mult_nonneg_nonneg [OF uint_ge_0 uint_ge_0, standard]
lemma uint_sub_lt2p [simp]:
- "uint (x :: 'a word) - uint (y :: 'b word) <
- 2 ^ CARD('a)"
+ "uint (x :: 'a :: len0 word) - uint (y :: 'b :: len0 word) <
+ 2 ^ len_of TYPE('a)"
using uint_ge_0 [of y] uint_lt2p [of x] by arith
subsection "Conditions for the addition (etc) of two words to overflow"
lemma uint_add_lem:
- "(uint x + uint y < 2 ^ CARD('a)) =
- (uint (x + y :: 'a word) = uint x + uint y)"
+ "(uint x + uint y < 2 ^ len_of TYPE('a)) =
+ (uint (x + y :: 'a :: len0 word) = uint x + uint y)"
by (unfold uint_word_ariths) (auto intro!: trans [OF _ int_mod_lem])
lemma uint_mult_lem:
- "(uint x * uint y < 2 ^ CARD('a)) =
- (uint (x * y :: 'a word) = uint x * uint y)"
+ "(uint x * uint y < 2 ^ len_of TYPE('a)) =
+ (uint (x * y :: 'a :: len0 word) = uint x * uint y)"
by (unfold uint_word_ariths) (auto intro!: trans [OF _ int_mod_lem])
lemma uint_sub_lem:
@@ -438,25 +469,25 @@
subsection {* Definition of uint\_arith *}
lemma word_of_int_inverse:
- "word_of_int r = a ==> 0 <= r ==> r < 2 ^ CARD('a) ==>
- uint (a::'a word) = r"
+ "word_of_int r = a ==> 0 <= r ==> r < 2 ^ len_of TYPE('a) ==>
+ uint (a::'a::len0 word) = r"
apply (erule word_uint.Abs_inverse' [rotated])
apply (simp add: uints_num)
done
lemma uint_split:
- fixes x::"'a word"
+ fixes x::"'a::len0 word"
shows "P (uint x) =
- (ALL i. word_of_int i = x & 0 <= i & i < 2^CARD('a) --> P i)"
+ (ALL i. word_of_int i = x & 0 <= i & i < 2^len_of TYPE('a) --> P i)"
apply (fold word_int_case_def)
apply (auto dest!: word_of_int_inverse simp: int_word_uint int_mod_eq'
split: word_int_split)
done
lemma uint_split_asm:
- fixes x::"'a word"
+ fixes x::"'a::len0 word"
shows "P (uint x) =
- (~(EX i. word_of_int i = x & 0 <= i & i < 2^CARD('a) & ~ P i))"
+ (~(EX i. word_of_int i = x & 0 <= i & i < 2^len_of TYPE('a) & ~ P i))"
by (auto dest!: word_of_int_inverse
simp: int_word_uint int_mod_eq'
split: uint_split)
@@ -468,7 +499,7 @@
word_uint.Rep_inject [symmetric]
uint_sub_if' uint_plus_if'
-(* use this to stop, eg, 2 ^ CARD(32) being simplified *)
+(* use this to stop, eg, 2 ^ len_of TYPE (32) being simplified *)
lemma power_False_cong: "False ==> a ^ b = c ^ d"
by auto
@@ -507,18 +538,18 @@
subsection "More on overflows and monotonicity"
lemma no_plus_overflow_uint_size:
- "((x :: 'a word) <= x + y) = (uint x + uint y < 2 ^ size x)"
+ "((x :: 'a :: len0 word) <= x + y) = (uint x + uint y < 2 ^ size x)"
unfolding word_size by uint_arith
lemmas no_olen_add = no_plus_overflow_uint_size [unfolded word_size]
-lemma no_ulen_sub: "((x :: 'a word) >= x - y) = (uint y <= uint x)"
+lemma no_ulen_sub: "((x :: 'a :: len0 word) >= x - y) = (uint y <= uint x)"
by uint_arith
lemma no_olen_add':
- fixes x :: "'a word"
- shows "(x \<le> y + x) = (uint y + uint x < 2 ^ CARD('a))"
- by (simp add: add_ac no_olen_add)
+ fixes x :: "'a::len0 word"
+ shows "(x \<le> y + x) = (uint y + uint x < 2 ^ len_of TYPE('a))"
+ by (simp add: word_add_ac add_ac no_olen_add)
lemmas olen_add_eqv = trans [OF no_olen_add no_olen_add' [symmetric], standard]
@@ -530,35 +561,35 @@
lemmas word_sub_le = word_sub_le_iff [THEN iffD2, standard]
lemma word_less_sub1:
- "(x :: 'a :: finite word) ~= 0 ==> (1 < x) = (0 < x - 1)"
+ "(x :: 'a :: len word) ~= 0 ==> (1 < x) = (0 < x - 1)"
by uint_arith
lemma word_le_sub1:
- "(x :: 'a :: finite word) ~= 0 ==> (1 <= x) = (0 <= x - 1)"
+ "(x :: 'a :: len word) ~= 0 ==> (1 <= x) = (0 <= x - 1)"
by uint_arith
lemma sub_wrap_lt:
- "((x :: 'a word) < x - z) = (x < z)"
+ "((x :: 'a :: len0 word) < x - z) = (x < z)"
by uint_arith
lemma sub_wrap:
- "((x :: 'a word) <= x - z) = (z = 0 | x < z)"
+ "((x :: 'a :: len0 word) <= x - z) = (z = 0 | x < z)"
by uint_arith
lemma plus_minus_not_NULL_ab:
- "(x :: 'a word) <= ab - c ==> c <= ab ==> c ~= 0 ==> x + c ~= 0"
+ "(x :: 'a :: len0 word) <= ab - c ==> c <= ab ==> c ~= 0 ==> x + c ~= 0"
by uint_arith
lemma plus_minus_no_overflow_ab:
- "(x :: 'a word) <= ab - c ==> c <= ab ==> x <= x + c"
+ "(x :: 'a :: len0 word) <= ab - c ==> c <= ab ==> x <= x + c"
by uint_arith
lemma le_minus':
- "(a :: 'a word) + c <= b ==> a <= a + c ==> c <= b - a"
+ "(a :: 'a :: len0 word) + c <= b ==> a <= a + c ==> c <= b - a"
by uint_arith
lemma le_plus':
- "(a :: 'a word) <= b ==> c <= b - a ==> a + c <= b"
+ "(a :: 'a :: len0 word) <= b ==> c <= b - a ==> a + c <= b"
by uint_arith
lemmas le_plus = le_plus' [rotated]
@@ -566,69 +597,69 @@
lemmas le_minus = leD [THEN thin_rl, THEN le_minus', standard]
lemma word_plus_mono_right:
- "(y :: 'a word) <= z ==> x <= x + z ==> x + y <= x + z"
+ "(y :: 'a :: len0 word) <= z ==> x <= x + z ==> x + y <= x + z"
by uint_arith
lemma word_less_minus_cancel:
- "y - x < z - x ==> x <= z ==> (y :: 'a word) < z"
+ "y - x < z - x ==> x <= z ==> (y :: 'a :: len0 word) < z"
by uint_arith
lemma word_less_minus_mono_left:
- "(y :: 'a word) < z ==> x <= y ==> y - x < z - x"
+ "(y :: 'a :: len0 word) < z ==> x <= y ==> y - x < z - x"
by uint_arith
lemma word_less_minus_mono:
"a < c ==> d < b ==> a - b < a ==> c - d < c
- ==> a - b < c - (d::'a::finite word)"
+ ==> a - b < c - (d::'a::len word)"
by uint_arith
lemma word_le_minus_cancel:
- "y - x <= z - x ==> x <= z ==> (y :: 'a word) <= z"
+ "y - x <= z - x ==> x <= z ==> (y :: 'a :: len0 word) <= z"
by uint_arith
lemma word_le_minus_mono_left:
- "(y :: 'a word) <= z ==> x <= y ==> y - x <= z - x"
+ "(y :: 'a :: len0 word) <= z ==> x <= y ==> y - x <= z - x"
by uint_arith
lemma word_le_minus_mono:
"a <= c ==> d <= b ==> a - b <= a ==> c - d <= c
- ==> a - b <= c - (d::'a::finite word)"
+ ==> a - b <= c - (d::'a::len word)"
by uint_arith
lemma plus_le_left_cancel_wrap:
- "(x :: 'a word) + y' < x ==> x + y < x ==> (x + y' < x + y) = (y' < y)"
+ "(x :: 'a :: len0 word) + y' < x ==> x + y < x ==> (x + y' < x + y) = (y' < y)"
by uint_arith
lemma plus_le_left_cancel_nowrap:
- "(x :: 'a word) <= x + y' ==> x <= x + y ==>
+ "(x :: 'a :: len0 word) <= x + y' ==> x <= x + y ==>
(x + y' < x + y) = (y' < y)"
by uint_arith
lemma word_plus_mono_right2:
- "(a :: 'a word) <= a + b ==> c <= b ==> a <= a + c"
+ "(a :: 'a :: len0 word) <= a + b ==> c <= b ==> a <= a + c"
by uint_arith
lemma word_less_add_right:
- "(x :: 'a word) < y - z ==> z <= y ==> x + z < y"
+ "(x :: 'a :: len0 word) < y - z ==> z <= y ==> x + z < y"
by uint_arith
lemma word_less_sub_right:
- "(x :: 'a word) < y + z ==> y <= x ==> x - y < z"
+ "(x :: 'a :: len0 word) < y + z ==> y <= x ==> x - y < z"
by uint_arith
lemma word_le_plus_either:
- "(x :: 'a word) <= y | x <= z ==> y <= y + z ==> x <= y + z"
+ "(x :: 'a :: len0 word) <= y | x <= z ==> y <= y + z ==> x <= y + z"
by uint_arith
lemma word_less_nowrapI:
- "(x :: 'a word) < z - k ==> k <= z ==> 0 < k ==> x < x + k"
+ "(x :: 'a :: len0 word) < z - k ==> k <= z ==> 0 < k ==> x < x + k"
by uint_arith
-lemma inc_le: "(i :: 'a :: finite word) < m ==> i + 1 <= m"
+lemma inc_le: "(i :: 'a :: len word) < m ==> i + 1 <= m"
by uint_arith
lemma inc_i:
- "(1 :: 'a :: finite word) <= i ==> i < m ==> 1 <= (i + 1) & i + 1 <= m"
+ "(1 :: 'a :: len word) <= i ==> i < m ==> 1 <= (i + 1) & i + 1 <= m"
by uint_arith
lemma udvd_incr_lem:
@@ -684,13 +715,89 @@
apply simp
done
+(* links with rbl operations *)
+lemma word_succ_rbl:
+ "to_bl w = bl ==> to_bl (word_succ w) = (rev (rbl_succ (rev bl)))"
+ apply (unfold word_succ_def)
+ apply clarify
+ apply (simp add: to_bl_of_bin)
+ apply (simp add: to_bl_def rbl_succ)
+ done
+
+lemma word_pred_rbl:
+ "to_bl w = bl ==> to_bl (word_pred w) = (rev (rbl_pred (rev bl)))"
+ apply (unfold word_pred_def)
+ apply clarify
+ apply (simp add: to_bl_of_bin)
+ apply (simp add: to_bl_def rbl_pred)
+ done
+
+lemma word_add_rbl:
+ "to_bl v = vbl ==> to_bl w = wbl ==>
+ to_bl (v + w) = (rev (rbl_add (rev vbl) (rev wbl)))"
+ apply (unfold word_add_def)
+ apply clarify
+ apply (simp add: to_bl_of_bin)
+ apply (simp add: to_bl_def rbl_add)
+ done
+
+lemma word_mult_rbl:
+ "to_bl v = vbl ==> to_bl w = wbl ==>
+ to_bl (v * w) = (rev (rbl_mult (rev vbl) (rev wbl)))"
+ apply (unfold word_mult_def)
+ apply clarify
+ apply (simp add: to_bl_of_bin)
+ apply (simp add: to_bl_def rbl_mult)
+ done
+
+lemma rtb_rbl_ariths:
+ "rev (to_bl w) = ys \<Longrightarrow> rev (to_bl (word_succ w)) = rbl_succ ys"
+
+ "rev (to_bl w) = ys \<Longrightarrow> rev (to_bl (word_pred w)) = rbl_pred ys"
+
+ "[| rev (to_bl v) = ys; rev (to_bl w) = xs |]
+ ==> rev (to_bl (v * w)) = rbl_mult ys xs"
+
+ "[| rev (to_bl v) = ys; rev (to_bl w) = xs |]
+ ==> rev (to_bl (v + w)) = rbl_add ys xs"
+ by (auto simp: rev_swap [symmetric] word_succ_rbl
+ word_pred_rbl word_mult_rbl word_add_rbl)
+
+
subsection "Arithmetic type class instantiations"
+instance word :: (len0) comm_monoid_add ..
+
+instance word :: (len0) comm_monoid_mult
+ apply (intro_classes)
+ apply (simp add: word_mult_commute)
+ apply (simp add: word_mult_1)
+ done
+
+instance word :: (len0) comm_semiring
+ by (intro_classes) (simp add : word_left_distrib)
+
+instance word :: (len0) ab_group_add ..
+
+instance word :: (len0) comm_ring ..
+
+instance word :: (len) comm_semiring_1
+ by (intro_classes) (simp add: lenw1_zero_neq_one)
+
+instance word :: (len) comm_ring_1 ..
+
+instance word :: (len0) comm_semiring_0 ..
+
+instance word :: (len0) order ..
+
+instance word :: (len) recpower
+ by (intro_classes) (simp_all add: word_pow)
+
(* note that iszero_def is only for class comm_semiring_1_cancel,
- which requires word length >= 1, ie 'a :: finite word *)
+ which requires word length >= 1, ie 'a :: len word *)
lemma zero_bintrunc:
- "iszero (number_of x :: 'a :: finite word) =
- (bintrunc CARD('a) x = Numeral.Pls)"
+ "iszero (number_of x :: 'a :: len word) =
+ (bintrunc (len_of TYPE('a)) x = Numeral.Pls)"
apply (unfold iszero_def word_0_wi word_no_wi)
apply (rule word_ubin.norm_eq_iff [symmetric, THEN trans])
apply (simp add : Pls_def [symmetric])
@@ -704,7 +811,16 @@
lemma word_of_int: "of_int = word_of_int"
apply (rule ext)
- apply (simp add: word_of_int Abs_word'_eq)
+ apply (unfold of_int_def)
+ apply (rule contentsI)
+ apply safe
+ apply (simp_all add: word_of_nat word_of_int_homs)
+ defer
+ apply (rule Rep_Integ_ne [THEN nonemptyE])
+ apply (rule bexI)
+ prefer 2
+ apply assumption
+ apply (auto simp add: RI_eq_diff)
done
lemma word_of_int_nat:
@@ -712,15 +828,15 @@
by (simp add: of_nat_nat word_of_int)
lemma word_number_of_eq:
- "number_of w = (of_int w :: 'a :: finite word)"
+ "number_of w = (of_int w :: 'a :: len word)"
unfolding word_number_of_def word_of_int by auto
-instance word :: (finite) number_ring
+instance word :: (len) number_ring
by (intro_classes) (simp add : word_number_of_eq)
lemma iszero_word_no [simp] :
- "iszero (number_of bin :: 'a :: finite word) =
- iszero (number_of (bintrunc CARD('a) bin) :: int)"
+ "iszero (number_of bin :: 'a :: len word) =
+ iszero (number_of (bintrunc (len_of TYPE('a)) bin) :: int)"
apply (simp add: zero_bintrunc number_of_is_id)
apply (unfold iszero_def Pls_def)
apply (rule refl)
@@ -730,7 +846,7 @@
subsection "Word and nat"
lemma td_ext_unat':
- "n = CARD('a :: finite) ==>
+ "n = len_of TYPE ('a :: len) ==>
td_ext (unat :: 'a word => nat) of_nat
(unats n) (%i. i mod 2 ^ n)"
apply (unfold td_ext_def' unat_def word_of_nat unats_uints)
@@ -743,24 +859,24 @@
lemmas unat_of_nat = td_ext_unat [THEN td_ext.eq_norm, standard]
interpretation word_unat:
- td_ext ["unat::'a::finite word => nat"
+ td_ext ["unat::'a::len word => nat"
of_nat
- "unats CARD('a::finite)"
- "%i. i mod 2 ^ CARD('a::finite)"]
+ "unats (len_of TYPE('a::len))"
+ "%i. i mod 2 ^ len_of TYPE('a::len)"]
by (rule td_ext_unat)
lemmas td_unat = word_unat.td_thm
lemmas unat_lt2p [iff] = word_unat.Rep [unfolded unats_def mem_Collect_eq]
-lemma unat_le: "y <= unat (z :: 'a :: finite word) ==> y : unats CARD('a)"
+lemma unat_le: "y <= unat (z :: 'a :: len word) ==> y : unats (len_of TYPE ('a))"
apply (unfold unats_def)
apply clarsimp
apply (rule xtrans, rule unat_lt2p, assumption)
done
lemma word_nchotomy:
- "ALL w. EX n. (w :: 'a :: finite word) = of_nat n & n < 2 ^ CARD('a)"
+ "ALL w. EX n. (w :: 'a :: len word) = of_nat n & n < 2 ^ len_of TYPE ('a)"
apply (rule allI)
apply (rule word_unat.Abs_cases)
apply (unfold unats_def)
@@ -768,8 +884,8 @@
done
lemma of_nat_eq:
- fixes w :: "'a::finite word"
- shows "(of_nat n = w) = (\<exists>q. n = unat w + q * 2 ^ CARD('a))"
+ fixes w :: "'a::len word"
+ shows "(of_nat n = w) = (\<exists>q. n = unat w + q * 2 ^ len_of TYPE('a))"
apply (rule trans)
apply (rule word_unat.inverse_norm)
apply (rule iffI)
@@ -783,7 +899,7 @@
unfolding word_size by (rule of_nat_eq)
lemma of_nat_0:
- "(of_nat m = (0::'a::finite word)) = (\<exists>q. m = q * 2 ^ CARD('a))"
+ "(of_nat m = (0::'a::len word)) = (\<exists>q. m = q * 2 ^ len_of TYPE('a))"
by (simp add: of_nat_eq)
lemmas of_nat_2p = mult_1 [symmetric, THEN iffD2 [OF of_nat_0 exI]]
@@ -792,7 +908,7 @@
by (cases k) auto
lemma of_nat_neq_0:
- "0 < k ==> k < 2 ^ CARD('a :: finite) ==> of_nat k ~= (0 :: 'a word)"
+ "0 < k ==> k < 2 ^ len_of TYPE ('a :: len) ==> of_nat k ~= (0 :: 'a word)"
by (clarsimp simp add : of_nat_0)
lemma Abs_fnat_hom_add:
@@ -800,17 +916,17 @@
by simp
lemma Abs_fnat_hom_mult:
- "of_nat a * of_nat b = (of_nat (a * b) :: 'a :: finite word)"
+ "of_nat a * of_nat b = (of_nat (a * b) :: 'a :: len word)"
by (simp add: word_of_nat word_of_int_mult_hom zmult_int)
lemma Abs_fnat_hom_Suc:
"word_succ (of_nat a) = of_nat (Suc a)"
by (simp add: word_of_nat word_of_int_succ_hom add_ac)
-lemma Abs_fnat_hom_0: "(0::'a::finite word) = of_nat 0"
+lemma Abs_fnat_hom_0: "(0::'a::len word) = of_nat 0"
by (simp add: word_of_nat word_0_wi)
-lemma Abs_fnat_hom_1: "(1::'a::finite word) = of_nat (Suc 0)"
+lemma Abs_fnat_hom_1: "(1::'a::len word) = of_nat (Suc 0)"
by (simp add: word_of_nat word_1_wi)
lemmas Abs_fnat_homs =
@@ -852,14 +968,14 @@
[simplified linorder_not_less [symmetric], simplified]
lemma unat_add_lem:
- "(unat x + unat y < 2 ^ CARD('a)) =
- (unat (x + y :: 'a :: finite word) = unat x + unat y)"
+ "(unat x + unat y < 2 ^ len_of TYPE('a)) =
+ (unat (x + y :: 'a :: len word) = unat x + unat y)"
unfolding unat_word_ariths
by (auto intro!: trans [OF _ nat_mod_lem])
lemma unat_mult_lem:
- "(unat x * unat y < 2 ^ CARD('a)) =
- (unat (x * y :: 'a :: finite word) = unat x * unat y)"
+ "(unat x * unat y < 2 ^ len_of TYPE('a)) =
+ (unat (x * y :: 'a :: len word) = unat x * unat y)"
unfolding unat_word_ariths
by (auto intro!: trans [OF _ nat_mod_lem])
@@ -867,7 +983,7 @@
trans [OF unat_word_ariths(1) mod_nat_add, simplified, standard]
lemma le_no_overflow:
- "x <= b ==> a <= a + b ==> x <= a + (b :: 'a word)"
+ "x <= b ==> a <= a + b ==> x <= a + (b :: 'a :: len0 word)"
apply (erule order_trans)
apply (erule olen_add_eqv [THEN iffD1])
done
@@ -898,13 +1014,13 @@
lemmas unat_sub_if' = unat_sub_if_size [unfolded word_size]
-lemma unat_div: "unat ((x :: 'a :: finite word) div y) = unat x div unat y"
+lemma unat_div: "unat ((x :: 'a :: len word) div y) = unat x div unat y"
apply (simp add : unat_word_ariths)
apply (rule unat_lt2p [THEN xtr7, THEN nat_mod_eq'])
apply (rule div_le_dividend)
done
-lemma unat_mod: "unat ((x :: 'a :: finite word) mod y) = unat x mod unat y"
+lemma unat_mod: "unat ((x :: 'a :: len word) mod y) = unat x mod unat y"
apply (clarsimp simp add : unat_word_ariths)
apply (cases "unat y")
prefer 2
@@ -913,25 +1029,25 @@
apply auto
done
-lemma uint_div: "uint ((x :: 'a :: finite word) div y) = uint x div uint y"
+lemma uint_div: "uint ((x :: 'a :: len word) div y) = uint x div uint y"
unfolding uint_nat by (simp add : unat_div zdiv_int)
-lemma uint_mod: "uint ((x :: 'a :: finite word) mod y) = uint x mod uint y"
+lemma uint_mod: "uint ((x :: 'a :: len word) mod y) = uint x mod uint y"
unfolding uint_nat by (simp add : unat_mod zmod_int)
subsection {* Definition of unat\_arith tactic *}
lemma unat_split:
- fixes x::"'a::finite word"
+ fixes x::"'a::len word"
shows "P (unat x) =
- (ALL n. of_nat n = x & n < 2^CARD('a) --> P n)"
+ (ALL n. of_nat n = x & n < 2^len_of TYPE('a) --> P n)"
by (auto simp: unat_of_nat)
lemma unat_split_asm:
- fixes x::"'a::finite word"
+ fixes x::"'a::len word"
shows "P (unat x) =
- (~(EX n. of_nat n = x & n < 2^CARD('a) & ~ P n))"
+ (~(EX n. of_nat n = x & n < 2^len_of TYPE('a) & ~ P n))"
by (auto simp: unat_of_nat)
lemmas of_nat_inverse =
@@ -975,10 +1091,10 @@
"solving word arithmetic via natural numbers and arith"
lemma no_plus_overflow_unat_size:
- "((x :: 'a :: finite word) <= x + y) = (unat x + unat y < 2 ^ size x)"
+ "((x :: 'a :: len word) <= x + y) = (unat x + unat y < 2 ^ size x)"
unfolding word_size by unat_arith
-lemma unat_sub: "b <= a ==> unat (a - b) = unat a - unat (b :: 'a :: finite word)"
+lemma unat_sub: "b <= a ==> unat (a - b) = unat a - unat (b :: 'a :: len word)"
by unat_arith
lemmas no_olen_add_nat = no_plus_overflow_unat_size [unfolded word_size]
@@ -986,7 +1102,7 @@
lemmas unat_plus_simple = trans [OF no_olen_add_nat unat_add_lem, standard]
lemma word_div_mult:
- "(0 :: 'a :: finite word) < y ==> unat x * unat y < 2 ^ CARD('a) ==>
+ "(0 :: 'a :: len word) < y ==> unat x * unat y < 2 ^ len_of TYPE('a) ==>
x * y div y = x"
apply unat_arith
apply clarsimp
@@ -994,8 +1110,8 @@
apply auto
done
-lemma div_lt': "(i :: 'a :: finite word) <= k div x ==>
- unat i * unat x < 2 ^ CARD('a)"
+lemma div_lt': "(i :: 'a :: len word) <= k div x ==>
+ unat i * unat x < 2 ^ len_of TYPE('a)"
apply unat_arith
apply clarsimp
apply (drule mult_le_mono1)
@@ -1005,7 +1121,7 @@
lemmas div_lt'' = order_less_imp_le [THEN div_lt']
-lemma div_lt_mult: "(i :: 'a :: finite word) < k div x ==> 0 < x ==> i * x < k"
+lemma div_lt_mult: "(i :: 'a :: len word) < k div x ==> 0 < x ==> i * x < k"
apply (frule div_lt'' [THEN unat_mult_lem [THEN iffD1]])
apply (simp add: unat_arith_simps)
apply (drule (1) mult_less_mono1)
@@ -1014,7 +1130,7 @@
done
lemma div_le_mult:
- "(i :: 'a :: finite word) <= k div x ==> 0 < x ==> i * x <= k"
+ "(i :: 'a :: len word) <= k div x ==> 0 < x ==> i * x <= k"
apply (frule div_lt' [THEN unat_mult_lem [THEN iffD1]])
apply (simp add: unat_arith_simps)
apply (drule mult_le_mono1)
@@ -1023,7 +1139,7 @@
done
lemma div_lt_uint':
- "(i :: 'a :: finite word) <= k div x ==> uint i * uint x < 2 ^ CARD('a)"
+ "(i :: 'a :: len word) <= k div x ==> uint i * uint x < 2 ^ len_of TYPE('a)"
apply (unfold uint_nat)
apply (drule div_lt')
apply (simp add: zmult_int zless_nat_eq_int_zless [symmetric]
@@ -1033,8 +1149,8 @@
lemmas div_lt_uint'' = order_less_imp_le [THEN div_lt_uint']
lemma word_le_exists':
- "(x :: 'a word) <= y ==>
- (EX z. y = x + z & uint x + uint z < 2 ^ CARD('a))"
+ "(x :: 'a :: len0 word) <= y ==>
+ (EX z. y = x + z & uint x + uint z < 2 ^ len_of TYPE('a))"
apply (rule exI)
apply (rule conjI)
apply (rule zadd_diff_inverse)
@@ -1070,7 +1186,7 @@
mod_le_divisor div_le_dividend thd1
lemma word_mod_div_equality:
- "(n div b) * b + (n mod b) = (n :: 'a :: finite word)"
+ "(n div b) * b + (n mod b) = (n :: 'a :: len word)"
apply (unfold word_less_nat_alt word_arith_nat_defs)
apply (cut_tac y="unat b" in gt_or_eq_0)
apply (erule disjE)
@@ -1078,7 +1194,7 @@
apply simp
done
-lemma word_div_mult_le: "a div b * b <= (a::'a::finite word)"
+lemma word_div_mult_le: "a div b * b <= (a::'a::len word)"
apply (unfold word_le_nat_alt word_arith_nat_defs)
apply (cut_tac y="unat b" in gt_or_eq_0)
apply (erule disjE)
@@ -1086,19 +1202,35 @@
apply simp
done
-lemma word_mod_less_divisor: "0 < n ==> m mod n < (n :: 'a :: finite word)"
+lemma word_mod_less_divisor: "0 < n ==> m mod n < (n :: 'a :: len word)"
apply (simp only: word_less_nat_alt word_arith_nat_defs)
apply (clarsimp simp add : uno_simps)
done
lemma word_of_int_power_hom:
- "word_of_int a ^ n = (word_of_int (a ^ n) :: 'a :: finite word)"
+ "word_of_int a ^ n = (word_of_int (a ^ n) :: 'a :: len word)"
by (induct n) (simp_all add : word_of_int_hom_syms power_Suc)
lemma word_arith_power_alt:
- "a ^ n = (word_of_int (uint a ^ n) :: 'a :: finite word)"
+ "a ^ n = (word_of_int (uint a ^ n) :: 'a :: len word)"
by (simp add : word_of_int_power_hom [symmetric])
+lemma of_bl_length_less:
+ "length x = k ==> k < len_of TYPE('a) ==> (of_bl x :: 'a :: len word) < 2 ^ k"
+ apply (unfold of_bl_no [unfolded word_number_of_def]
+ word_less_alt word_number_of_alt)
+ apply safe
+ apply (simp (no_asm) add: word_of_int_power_hom word_uint.eq_norm
+ del: word_of_int_bin)
+ apply (simp add: mod_pos_pos_trivial)
+ apply (subst mod_pos_pos_trivial)
+ apply (rule bl_to_bin_ge0)
+ apply (rule order_less_trans)
+ apply (rule bl_to_bin_lt2p)
+ apply simp
+ apply (rule bl_to_bin_lt2p)
+ done
+
subsection "Cardinality, finiteness of set of words"
@@ -1109,7 +1241,7 @@
lemmas card_word = trans [OF card_eq card_lessThan', standard]
-lemma finite_word_UNIV: "finite (UNIV :: 'a :: finite word set)"
+lemma finite_word_UNIV: "finite (UNIV :: 'a :: len word set)"
apply (rule contrapos_np)
prefer 2
apply (erule card_infinite)
@@ -1117,7 +1249,7 @@
done
lemma card_word_size:
- "card (UNIV :: 'a :: finite word set) = (2 ^ size (x :: 'a word))"
+ "card (UNIV :: 'a :: len word set) = (2 ^ size (x :: 'a word))"
unfolding word_size by (rule card_word)
end
--- a/src/HOL/Word/WordBitwise.thy Tue Aug 28 19:45:45 2007 +0200
+++ b/src/HOL/Word/WordBitwise.thy Tue Aug 28 20:13:47 2007 +0200
@@ -38,7 +38,7 @@
bin_trunc_ao(1) [symmetric])
lemma word_ops_nth_size:
- "n < size (x::'a word) ==>
+ "n < size (x::'a::len0 word) ==>
(x OR y) !! n = (x !! n | y !! n) &
(x AND y) !! n = (x !! n & y !! n) &
(x XOR y) !! n = (x !! n ~= y !! n) &
@@ -47,7 +47,7 @@
by (clarsimp simp add : word_ubin.eq_norm nth_bintr bin_nth_ops)
lemma word_ao_nth:
- fixes x :: "'a word"
+ fixes x :: "'a::len0 word"
shows "(x OR y) !! n = (x !! n | y !! n) &
(x AND y) !! n = (x !! n & y !! n)"
apply (cases "n < size x")
@@ -66,7 +66,7 @@
word_wi_log_defs
lemma word_bw_assocs:
- fixes x :: "'a word"
+ fixes x :: "'a::len0 word"
shows
"(x AND y) AND z = x AND y AND z"
"(x OR y) OR z = x OR y OR z"
@@ -77,7 +77,7 @@
by (auto simp: bwsimps bbw_assocs)
lemma word_bw_comms:
- fixes x :: "'a word"
+ fixes x :: "'a::len0 word"
shows
"x AND y = y AND x"
"x OR y = y OR x"
@@ -87,7 +87,7 @@
by (auto simp: bwsimps bin_ops_comm)
lemma word_bw_lcs:
- fixes x :: "'a word"
+ fixes x :: "'a::len0 word"
shows
"y AND x AND z = x AND y AND z"
"y OR x OR z = x OR y OR z"
@@ -98,7 +98,7 @@
by (auto simp: bwsimps)
lemma word_log_esimps [simp]:
- fixes x :: "'a word"
+ fixes x :: "'a::len0 word"
shows
"x AND 0 = 0"
"x AND -1 = x"
@@ -116,7 +116,7 @@
by (auto simp: bwsimps)
lemma word_not_dist:
- fixes x :: "'a word"
+ fixes x :: "'a::len0 word"
shows
"NOT (x OR y) = NOT x AND NOT y"
"NOT (x AND y) = NOT x OR NOT y"
@@ -125,7 +125,7 @@
by (auto simp: bwsimps bbw_not_dist)
lemma word_bw_same:
- fixes x :: "'a word"
+ fixes x :: "'a::len0 word"
shows
"x AND x = x"
"x OR x = x"
@@ -134,7 +134,7 @@
by (auto simp: bwsimps)
lemma word_ao_absorbs [simp]:
- fixes x :: "'a word"
+ fixes x :: "'a::len0 word"
shows
"x AND (y OR x) = x"
"x OR y AND x = x"
@@ -149,12 +149,12 @@
by (auto simp: bwsimps)
lemma word_not_not [simp]:
- "NOT NOT (x::'a word) = x"
+ "NOT NOT (x::'a::len0 word) = x"
using word_of_int_Ex [where x=x]
by (auto simp: bwsimps)
lemma word_ao_dist:
- fixes x :: "'a word"
+ fixes x :: "'a::len0 word"
shows "(x OR y) AND z = x AND z OR y AND z"
using word_of_int_Ex [where x=x]
word_of_int_Ex [where x=y]
@@ -162,7 +162,7 @@
by (auto simp: bwsimps bbw_ao_dist simp del: bin_ops_comm)
lemma word_oa_dist:
- fixes x :: "'a word"
+ fixes x :: "'a::len0 word"
shows "x AND y OR z = (x OR z) AND (y OR z)"
using word_of_int_Ex [where x=x]
word_of_int_Ex [where x=y]
@@ -170,28 +170,28 @@
by (auto simp: bwsimps bbw_oa_dist simp del: bin_ops_comm)
lemma word_add_not [simp]:
- fixes x :: "'a word"
+ fixes x :: "'a::len0 word"
shows "x + NOT x = -1"
using word_of_int_Ex [where x=x]
by (auto simp: bwsimps bin_add_not)
lemma word_plus_and_or [simp]:
- fixes x :: "'a word"
+ fixes x :: "'a::len0 word"
shows "(x AND y) + (x OR y) = x + y"
using word_of_int_Ex [where x=x]
word_of_int_Ex [where x=y]
by (auto simp: bwsimps plus_and_or)
lemma leoa:
- fixes x :: "'a word"
+ fixes x :: "'a::len0 word"
shows "(w = (x OR y)) ==> (y = (w AND y))" by auto
lemma leao:
- fixes x' :: "'a word"
+ fixes x' :: "'a::len0 word"
shows "(w' = (x' AND y')) ==> (x' = (x' OR w'))" by auto
lemmas word_ao_equiv = leao [COMP leoa [COMP iffI]]
-lemma le_word_or2: "x <= x OR (y::'a word)"
+lemma le_word_or2: "x <= x OR (y::'a::len0 word)"
unfolding word_le_def uint_or
by (auto intro: le_int_or)
@@ -201,12 +201,36 @@
lemmas word_and_le2 =
xtr3 [OF word_ao_absorbs (8) [symmetric] le_word_or2, standard]
-lemma word_lsb_alt: "lsb (w::'a word) = test_bit w 0"
+lemma bl_word_not: "to_bl (NOT w) = map Not (to_bl w)"
+ unfolding to_bl_def word_log_defs
+ by (simp add: bl_not_bin number_of_is_id word_no_wi [symmetric])
+
+lemma bl_word_xor: "to_bl (v XOR w) = app2 op ~= (to_bl v) (to_bl w)"
+ unfolding to_bl_def word_log_defs bl_xor_bin
+ by (simp add: number_of_is_id word_no_wi [symmetric])
+
+lemma bl_word_or: "to_bl (v OR w) = app2 op | (to_bl v) (to_bl w)"
+ unfolding to_bl_def word_log_defs
+ by (simp add: bl_or_bin number_of_is_id word_no_wi [symmetric])
+
+lemma bl_word_and: "to_bl (v AND w) = app2 op & (to_bl v) (to_bl w)"
+ unfolding to_bl_def word_log_defs
+ by (simp add: bl_and_bin number_of_is_id word_no_wi [symmetric])
+
+lemma word_lsb_alt: "lsb (w::'a::len0 word) = test_bit w 0"
by (auto simp: word_test_bit_def word_lsb_def)
-lemma word_lsb_1_0: "lsb (1::'a::finite word) & ~ lsb (0::'b word)"
+lemma word_lsb_1_0: "lsb (1::'a::len word) & ~ lsb (0::'b::len0 word)"
unfolding word_lsb_def word_1_no word_0_no by auto
+lemma word_lsb_last: "lsb (w::'a::len word) = last (to_bl w)"
+ apply (unfold word_lsb_def uint_bl bin_to_bl_def)
+ apply (rule_tac bin="uint w" in bin_exhaust)
+ apply (cases "size w")
+ apply auto
+ apply (auto simp add: bin_to_bl_aux_alt)
+ done
+
lemma word_lsb_int: "lsb w = (uint w mod 2 = 1)"
unfolding word_lsb_def bin_last_mod by auto
@@ -215,13 +239,13 @@
by (simp add : sign_Min_lt_0 number_of_is_id)
lemma word_msb_no':
- "w = number_of bin ==> msb (w::'a::finite word) = bin_nth bin (size w - 1)"
+ "w = number_of bin ==> msb (w::'a::len word) = bin_nth bin (size w - 1)"
unfolding word_msb_def word_number_of_def
by (clarsimp simp add: word_sbin.eq_norm word_size bin_sign_lem)
lemmas word_msb_no = refl [THEN word_msb_no', unfolded word_size]
-lemma word_msb_nth': "msb (w::'a::finite word) = bin_nth (uint w) (size w - 1)"
+lemma word_msb_nth': "msb (w::'a::len word) = bin_nth (uint w) (size w - 1)"
apply (unfold word_size)
apply (rule trans [OF _ word_msb_no])
apply (simp add : word_number_of_def)
@@ -229,18 +253,48 @@
lemmas word_msb_nth = word_msb_nth' [unfolded word_size]
+lemma word_msb_alt: "msb (w::'a::len word) = hd (to_bl w)"
+ apply (unfold word_msb_nth uint_bl)
+ apply (subst hd_conv_nth)
+ apply (rule length_greater_0_conv [THEN iffD1])
+ apply simp
+ apply (simp add : nth_bin_to_bl word_size)
+ done
+
lemma word_set_nth:
- "set_bit w n (test_bit w n) = (w::'a word)"
+ "set_bit w n (test_bit w n) = (w::'a::len0 word)"
unfolding word_test_bit_def word_set_bit_def by auto
+lemma bin_nth_uint':
+ "bin_nth (uint w) n = (rev (bin_to_bl (size w) (uint w)) ! n & n < size w)"
+ apply (unfold word_size)
+ apply (safe elim!: bin_nth_uint_imp)
+ apply (frule bin_nth_uint_imp)
+ apply (fast dest!: bin_nth_bl)+
+ done
+
+lemmas bin_nth_uint = bin_nth_uint' [unfolded word_size]
+
+lemma test_bit_bl: "w !! n = (rev (to_bl w) ! n & n < size w)"
+ unfolding to_bl_def word_test_bit_def word_size
+ by (rule bin_nth_uint)
+
+lemma to_bl_nth: "n < size w ==> to_bl w ! n = w !! (size w - Suc n)"
+ apply (unfold test_bit_bl)
+ apply clarsimp
+ apply (rule trans)
+ apply (rule nth_rev_alt)
+ apply (auto simp add: word_size)
+ done
+
lemma test_bit_set:
- fixes w :: "'a word"
+ fixes w :: "'a::len0 word"
shows "(set_bit w n x) !! n = (n < size w & x)"
unfolding word_size word_test_bit_def word_set_bit_def
by (clarsimp simp add : word_ubin.eq_norm nth_bintr)
lemma test_bit_set_gen:
- fixes w :: "'a word"
+ fixes w :: "'a::len0 word"
shows "test_bit (set_bit w n x) m =
(if m = n then n < size w & x else test_bit w m)"
apply (unfold word_size word_test_bit_def word_set_bit_def)
@@ -249,34 +303,70 @@
simp add: word_test_bit_def [symmetric])
done
+lemma of_bl_rep_False: "of_bl (replicate n False @ bs) = of_bl bs"
+ unfolding of_bl_def bl_to_bin_rep_F by auto
+
lemma msb_nth':
- fixes w :: "'a::finite word"
+ fixes w :: "'a::len word"
shows "msb w = w !! (size w - 1)"
unfolding word_msb_nth' word_test_bit_def by simp
lemmas msb_nth = msb_nth' [unfolded word_size]
-lemmas msb0 = zero_less_card_finite [THEN diff_Suc_less, THEN
+lemmas msb0 = len_gt_0 [THEN diff_Suc_less, THEN
word_ops_nth_size [unfolded word_size], standard]
lemmas msb1 = msb0 [where i = 0]
lemmas word_ops_msb = msb1 [unfolded msb_nth [symmetric, unfolded One_nat_def]]
-lemmas lsb0 = zero_less_card_finite [THEN word_ops_nth_size [unfolded word_size], standard]
+lemmas lsb0 = len_gt_0 [THEN word_ops_nth_size [unfolded word_size], standard]
lemmas word_ops_lsb = lsb0 [unfolded word_lsb_alt]
+lemma td_ext_nth':
+ "n = size (w::'a::len0 word) ==> ofn = set_bits ==> [w, ofn g] = l ==>
+ td_ext test_bit ofn {f. ALL i. f i --> i < n} (%h i. h i & i < n)"
+ apply (unfold word_size td_ext_def')
+ apply safe
+ apply (rule_tac [3] ext)
+ apply (rule_tac [4] ext)
+ apply (unfold word_size of_nth_def test_bit_bl)
+ apply safe
+ defer
+ apply (clarsimp simp: word_bl.Abs_inverse)+
+ apply (rule word_bl.Rep_inverse')
+ apply (rule sym [THEN trans])
+ apply (rule bl_of_nth_nth)
+ apply simp
+ apply (rule bl_of_nth_inj)
+ apply (clarsimp simp add : test_bit_bl word_size)
+ done
+
+lemmas td_ext_nth = td_ext_nth' [OF refl refl refl, unfolded word_size]
+
+interpretation test_bit:
+ td_ext ["op !! :: 'a::len0 word => nat => bool"
+ set_bits
+ "{f. \<forall>i. f i \<longrightarrow> i < len_of TYPE('a::len0)}"
+ "(\<lambda>h i. h i \<and> i < len_of TYPE('a::len0))"]
+ by (rule td_ext_nth)
+
+declare test_bit.Rep' [simp del]
+declare test_bit.Rep' [rule del]
+
+lemmas td_nth = test_bit.td_thm
+
lemma word_set_set_same:
- fixes w :: "'a word"
+ fixes w :: "'a::len0 word"
shows "set_bit (set_bit w n x) n y = set_bit w n y"
by (rule word_eqI) (simp add : test_bit_set_gen word_size)
lemma word_set_set_diff:
- fixes w :: "'a word"
+ fixes w :: "'a::len0 word"
assumes "m ~= n"
shows "set_bit (set_bit w m x) n y = set_bit (set_bit w n y) m x"
by (rule word_eqI) (clarsimp simp add : test_bit_set_gen word_size prems)
lemma test_bit_no':
- fixes w :: "'a word"
+ fixes w :: "'a::len0 word"
shows "w = number_of bin ==> test_bit w n = (n < size w & bin_nth bin n)"
unfolding word_test_bit_def word_number_of_def word_size
by (simp add : nth_bintr [symmetric] word_ubin.eq_norm)
@@ -284,22 +374,22 @@
lemmas test_bit_no =
refl [THEN test_bit_no', unfolded word_size, THEN eq_reflection, standard]
-lemma nth_0: "~ (0::'a word) !! n"
+lemma nth_0: "~ (0::'a::len0 word) !! n"
unfolding test_bit_no word_0_no by auto
lemma nth_sint:
- fixes w :: "'a::finite word"
- defines "l \<equiv> CARD('a)"
+ fixes w :: "'a::len word"
+ defines "l \<equiv> len_of TYPE ('a)"
shows "bin_nth (sint w) n = (if n < l - 1 then w !! n else w !! (l - 1))"
unfolding sint_uint l_def
by (clarsimp simp add: nth_sbintr word_test_bit_def [symmetric])
lemma word_lsb_no:
- "lsb (number_of bin :: 'a :: finite word) = (bin_last bin = bit.B1)"
+ "lsb (number_of bin :: 'a :: len word) = (bin_last bin = bit.B1)"
unfolding word_lsb_alt test_bit_no by auto
lemma word_set_no:
- "set_bit (number_of bin::'a word) n b =
+ "set_bit (number_of bin::'a::len0 word) n b =
number_of (bin_sc n (if b then bit.B1 else bit.B0) bin)"
apply (unfold word_set_bit_def word_number_of_def [symmetric])
apply (rule word_eqI)
@@ -312,9 +402,17 @@
lemmas clearBit_no = clearBit_def [THEN trans [OF meta_eq_to_obj_eq word_set_no],
simplified if_simps, THEN eq_reflection, standard]
-lemma word_msb_n1: "msb (-1::'a::finite word)"
- unfolding word_msb_def sint_sbintrunc number_of_is_id bin_sign_lem
- by (rule bin_nth_Min)
+lemma to_bl_n1:
+ "to_bl (-1::'a::len0 word) = replicate (len_of TYPE ('a)) True"
+ apply (rule word_bl.Abs_inverse')
+ apply simp
+ apply (rule word_eqI)
+ apply (clarsimp simp add: word_size test_bit_no)
+ apply (auto simp add: word_bl.Abs_inverse test_bit_bl word_size)
+ done
+
+lemma word_msb_n1: "msb (-1::'a::len word)"
+ unfolding word_msb_alt word_msb_alt to_bl_n1 by simp
declare word_set_set_same [simp] word_set_nth [simp]
test_bit_no [simp] word_set_no [simp] nth_0 [simp]
@@ -322,7 +420,7 @@
word_lsb_no [simp] word_msb_no [simp] word_msb_n1 [simp] word_lsb_1_0 [simp]
lemma word_set_nth_iff:
- "(set_bit w n b = w) = (w !! n = b | n >= size (w::'a word))"
+ "(set_bit w n b = w) = (w !! n = b | n >= size (w::'a::len0 word))"
apply (rule iffI)
apply (rule disjCI)
apply (drule word_eqD)
@@ -338,7 +436,7 @@
lemma test_bit_2p':
"w = word_of_int (2 ^ n) ==>
- w !! m = (m = n & m < size (w :: 'a :: finite word))"
+ w !! m = (m = n & m < size (w :: 'a :: len word))"
unfolding word_test_bit_def word_size
by (auto simp add: word_ubin.eq_norm nth_bintr nth_2p_bin)
@@ -348,9 +446,9 @@
word_of_int [symmetric] of_int_power]
lemma uint_2p:
- "(0::'a::finite word) < 2 ^ n ==> uint (2 ^ n::'a::finite word) = 2 ^ n"
+ "(0::'a::len word) < 2 ^ n ==> uint (2 ^ n::'a::len word) = 2 ^ n"
apply (unfold word_arith_power_alt)
- apply (case_tac "CARD('a)")
+ apply (case_tac "len_of TYPE ('a)")
apply clarsimp
apply (case_tac "nat")
apply clarsimp
@@ -362,9 +460,9 @@
apply (auto simp add: test_bit_2p nth_2p_bin word_test_bit_def [symmetric])
done
-lemma word_of_int_2p: "(word_of_int (2 ^ n) :: 'a :: finite word) = 2 ^ n"
+lemma word_of_int_2p: "(word_of_int (2 ^ n) :: 'a :: len word) = 2 ^ n"
apply (unfold word_arith_power_alt)
- apply (case_tac "CARD('a)")
+ apply (case_tac "len_of TYPE ('a)")
apply clarsimp
apply (case_tac "nat")
apply (rule word_ubin.norm_eq_iff [THEN iffD1])
@@ -374,7 +472,7 @@
apply simp
done
-lemma bang_is_le: "x !! m ==> 2 ^ m <= (x :: 'a :: finite word)"
+lemma bang_is_le: "x !! m ==> 2 ^ m <= (x :: 'a :: len word)"
apply (rule xtr3)
apply (rule_tac [2] y = "x" in le_word_or2)
apply (rule word_eqI)
@@ -382,7 +480,7 @@
done
lemma word_clr_le:
- fixes w :: "'a word"
+ fixes w :: "'a::len0 word"
shows "w >= set_bit w n False"
apply (unfold word_set_bit_def word_le_def word_ubin.eq_norm)
apply simp
@@ -392,7 +490,7 @@
done
lemma word_set_ge:
- fixes w :: "'a::finite word"
+ fixes w :: "'a::len word"
shows "w <= set_bit w n True"
apply (unfold word_set_bit_def word_le_def word_ubin.eq_norm)
apply simp
--- a/src/HOL/Word/WordBoolList.thy Tue Aug 28 19:45:45 2007 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,362 +0,0 @@
-(*
- ID: $Id$
- Author: Jeremy Dawson and Gerwin Klein, NICTA
-*)
-
-header {* Bool Lists and Words *}
-
-theory WordBoolList imports BinBoolList WordBitwise begin
-
-constdefs
- of_bl :: "bool list => 'a word"
- "of_bl bl == word_of_int (bl_to_bin bl)"
- to_bl :: "'a word => bool list"
- "to_bl w ==
- bin_to_bl CARD('a) (uint w)"
-
- word_reverse :: "'a word => 'a word"
- "word_reverse w == of_bl (rev (to_bl w))"
-
-defs (overloaded)
- word_set_bits_def:
- "(BITS n. f n)::'a word == of_bl (bl_of_nth CARD('a) f)"
-
-lemmas of_nth_def = word_set_bits_def
-
-lemma to_bl_def':
- "(to_bl :: 'a word => bool list) =
- bin_to_bl CARD('a) o uint"
- by (auto simp: to_bl_def intro: ext)
-
-lemmas word_reverse_no_def [simp] = word_reverse_def [of "number_of ?w"]
-
-(* type definitions theorem for in terms of equivalent bool list *)
-lemma td_bl:
- "type_definition (to_bl :: 'a word => bool list)
- of_bl
- {bl. length bl = CARD('a)}"
- apply (unfold type_definition_def of_bl_def to_bl_def)
- apply (simp add: word_ubin.eq_norm)
- apply safe
- apply (drule sym)
- apply simp
- done
-
-interpretation word_bl:
- type_definition ["to_bl :: 'a word => bool list"
- of_bl
- "{bl. length bl = CARD('a)}"]
- by (rule td_bl)
-
-lemma word_size_bl: "size w == size (to_bl w)"
- unfolding word_size by auto
-
-lemma to_bl_use_of_bl:
- "(to_bl w = bl) = (w = of_bl bl \<and> length bl = length (to_bl w))"
- by (fastsimp elim!: word_bl.Abs_inverse [simplified])
-
-lemma to_bl_word_rev: "to_bl (word_reverse w) = rev (to_bl w)"
- unfolding word_reverse_def by (simp add: word_bl.Abs_inverse)
-
-lemma word_rev_rev [simp] : "word_reverse (word_reverse w) = w"
- unfolding word_reverse_def by (simp add : word_bl.Abs_inverse)
-
-lemma word_rev_gal: "word_reverse w = u ==> word_reverse u = w"
- by auto
-
-lemmas word_rev_gal' = sym [THEN word_rev_gal, symmetric, standard]
-
-lemmas length_bl_gt_0 [iff] = xtr1 [OF word_bl.Rep' zero_less_card_finite, standard]
-lemmas bl_not_Nil [iff] =
- length_bl_gt_0 [THEN length_greater_0_conv [THEN iffD1], standard]
-lemmas length_bl_neq_0 [iff] = length_bl_gt_0 [THEN gr_implies_not0]
-
-lemma hd_bl_sign_sint: "hd (to_bl w) = (bin_sign (sint w) = Numeral.Min)"
- apply (unfold to_bl_def sint_uint)
- apply (rule trans [OF _ bl_sbin_sign])
- apply simp
- done
-
-lemma of_bl_drop':
- "lend = length bl - CARD('a) ==>
- of_bl (drop lend bl) = (of_bl bl :: 'a word)"
- apply (unfold of_bl_def)
- apply (clarsimp simp add : trunc_bl2bin [symmetric])
- done
-
-lemmas of_bl_no = of_bl_def [folded word_number_of_def]
-
-lemma test_bit_of_bl:
- "(of_bl bl::'a word) !! n = (rev bl ! n \<and> n < CARD('a) \<and> n < length bl)"
- apply (unfold of_bl_def word_test_bit_def)
- apply (auto simp add: word_size word_ubin.eq_norm nth_bintr bin_nth_of_bl)
- done
-
-lemma no_of_bl:
- "(number_of bin ::'a word) = of_bl (bin_to_bl CARD('a) bin)"
- unfolding word_size of_bl_no by (simp add : word_number_of_def)
-
-lemma uint_bl: "to_bl w == bin_to_bl (size w) (uint w)"
- unfolding word_size to_bl_def by auto
-
-lemma to_bl_bin: "bl_to_bin (to_bl w) = uint w"
- unfolding uint_bl by (simp add : word_size)
-
-lemma to_bl_of_bin:
- "to_bl (word_of_int bin::'a word) = bin_to_bl CARD('a) bin"
- unfolding uint_bl by (clarsimp simp add: word_ubin.eq_norm word_size)
-
-lemmas to_bl_no_bin [simp] = to_bl_of_bin [folded word_number_of_def]
-
-lemma to_bl_to_bin [simp] : "bl_to_bin (to_bl w) = uint w"
- unfolding uint_bl by (simp add : word_size)
-
-lemmas uint_bl_bin [simp] = trans [OF bin_bl_bin word_ubin.norm_Rep, standard]
-
-lemma word_rev_tf':
- "r = to_bl (of_bl bl) ==> r = rev (takefill False (length r) (rev bl))"
- unfolding of_bl_def uint_bl
- by (clarsimp simp add: bl_bin_bl_rtf word_ubin.eq_norm word_size)
-
-lemmas word_rev_tf = refl [THEN word_rev_tf', unfolded word_bl.Rep', standard]
-
-lemmas word_rep_drop = word_rev_tf [simplified takefill_alt,
- simplified, simplified rev_take, simplified]
-
-lemma of_bl_append_same: "of_bl (X @ to_bl w) = w"
- by (rule word_bl.Rep_eqD) (simp add: word_rep_drop)
-
-lemma ucast_bl: "ucast w == of_bl (to_bl w)"
- unfolding ucast_def of_bl_def uint_bl
- by (auto simp add : word_size)
-
-lemma to_bl_ucast:
- "to_bl (ucast (w::'b word) ::'a word) =
- replicate (CARD('a) - CARD('b)) False @
- drop (CARD('b) - CARD('a)) (to_bl w)"
- apply (unfold ucast_bl)
- apply (rule trans)
- apply (rule word_rep_drop)
- apply simp
- done
-
-lemma ucast_up_app':
- "uc = ucast ==> source_size uc + n = target_size uc ==>
- to_bl (uc w) = replicate n False @ (to_bl w)"
- apply (auto simp add : source_size target_size to_bl_ucast)
- apply (rule_tac f = "%n. replicate n False" in arg_cong)
- apply simp
- done
-
-lemma ucast_down_drop':
- "uc = ucast ==> source_size uc = target_size uc + n ==>
- to_bl (uc w) = drop n (to_bl w)"
- by (auto simp add : source_size target_size to_bl_ucast)
-
-lemma scast_down_drop':
- "sc = scast ==> source_size sc = target_size sc + n ==>
- to_bl (sc w) = drop n (to_bl w)"
- apply (subgoal_tac "sc = ucast")
- apply safe
- apply simp
- apply (erule refl [THEN ucast_down_drop'])
- apply (rule refl [THEN down_cast_same', symmetric])
- apply (simp add : source_size target_size is_down)
- done
-
-lemmas ucast_up_app = refl [THEN ucast_up_app']
-lemmas ucast_down_drop = refl [THEN ucast_down_drop']
-lemmas scast_down_drop = refl [THEN scast_down_drop']
-
-lemma ucast_of_bl_up':
- "w = of_bl bl ==> size bl <= size w ==> ucast w = of_bl bl"
- by (auto simp add : nth_ucast word_size test_bit_of_bl intro!: word_eqI)
-
-lemmas ucast_of_bl_up = refl [THEN ucast_of_bl_up']
-
-lemma ucast_down_bl': "uc = ucast ==> is_down uc ==> uc (of_bl bl) = of_bl bl"
- unfolding of_bl_no by clarify (erule ucast_down_no)
-
-lemmas ucast_down_bl = ucast_down_bl' [OF refl]
-
-lemma word_0_bl: "of_bl [] = 0"
- unfolding word_0_wi of_bl_def by (simp add : Pls_def)
-
-lemma word_1_bl: "of_bl [True] = 1"
- unfolding word_1_wi of_bl_def
- by (simp add : bl_to_bin_def Bit_def Pls_def)
-
-lemma of_bl_0 [simp] : "of_bl (replicate n False) = 0"
- by (simp add : word_0_wi of_bl_def bl_to_bin_rep_False Pls_def)
-
-lemma to_bl_0:
- "to_bl (0::'a word) = replicate CARD('a) False"
- unfolding uint_bl
- by (simp add : word_size bin_to_bl_Pls Pls_def [symmetric])
-
-(* links with rbl operations *)
-lemma word_succ_rbl:
- "to_bl w = bl ==> to_bl (word_succ w) = (rev (rbl_succ (rev bl)))"
- apply (unfold word_succ_def)
- apply clarify
- apply (simp add: to_bl_of_bin)
- apply (simp add: to_bl_def rbl_succ)
- done
-
-lemma word_pred_rbl:
- "to_bl w = bl ==> to_bl (word_pred w) = (rev (rbl_pred (rev bl)))"
- apply (unfold word_pred_def)
- apply clarify
- apply (simp add: to_bl_of_bin)
- apply (simp add: to_bl_def rbl_pred)
- done
-
-lemma word_add_rbl:
- "to_bl v = vbl ==> to_bl w = wbl ==>
- to_bl (v + w) = (rev (rbl_add (rev vbl) (rev wbl)))"
- apply (unfold word_add_def)
- apply clarify
- apply (simp add: to_bl_of_bin)
- apply (simp add: to_bl_def rbl_add)
- done
-
-lemma word_mult_rbl:
- "to_bl v = vbl ==> to_bl w = wbl ==>
- to_bl (v * w) = (rev (rbl_mult (rev vbl) (rev wbl)))"
- apply (unfold word_mult_def)
- apply clarify
- apply (simp add: to_bl_of_bin)
- apply (simp add: to_bl_def rbl_mult)
- done
-
-lemma rtb_rbl_ariths:
- "rev (to_bl w) = ys \<Longrightarrow> rev (to_bl (word_succ w)) = rbl_succ ys"
-
- "rev (to_bl w) = ys \<Longrightarrow> rev (to_bl (word_pred w)) = rbl_pred ys"
-
- "[| rev (to_bl v) = ys; rev (to_bl w) = xs |]
- ==> rev (to_bl (v * w)) = rbl_mult ys xs"
-
- "[| rev (to_bl v) = ys; rev (to_bl w) = xs |]
- ==> rev (to_bl (v + w)) = rbl_add ys xs"
- by (auto simp: rev_swap [symmetric] word_succ_rbl
- word_pred_rbl word_mult_rbl word_add_rbl)
-
-lemma of_bl_length_less:
- "length x = k ==> k < CARD('a) ==> (of_bl x :: 'a :: finite word) < 2 ^ k"
- apply (unfold of_bl_no [unfolded word_number_of_def]
- word_less_alt word_number_of_alt)
- apply safe
- apply (simp (no_asm) add: word_of_int_power_hom word_uint.eq_norm
- del: word_of_int_bin)
- apply (simp add: mod_pos_pos_trivial)
- apply (subst mod_pos_pos_trivial)
- apply (rule bl_to_bin_ge0)
- apply (rule order_less_trans)
- apply (rule bl_to_bin_lt2p)
- apply simp
- apply (rule bl_to_bin_lt2p)
- done
-
-subsection "Bitwise operations on bool lists"
-
-lemma bl_word_not: "to_bl (NOT w) = map Not (to_bl w)"
- unfolding to_bl_def word_log_defs
- by (simp add: bl_not_bin number_of_is_id word_no_wi [symmetric])
-
-lemma bl_word_xor: "to_bl (v XOR w) = app2 op ~= (to_bl v) (to_bl w)"
- unfolding to_bl_def word_log_defs bl_xor_bin
- by (simp add: number_of_is_id word_no_wi [symmetric])
-
-lemma bl_word_or: "to_bl (v OR w) = app2 op | (to_bl v) (to_bl w)"
- unfolding to_bl_def word_log_defs
- by (simp add: bl_or_bin number_of_is_id word_no_wi [symmetric])
-
-lemma bl_word_and: "to_bl (v AND w) = app2 op & (to_bl v) (to_bl w)"
- unfolding to_bl_def word_log_defs
- by (simp add: bl_and_bin number_of_is_id word_no_wi [symmetric])
-
-lemma word_lsb_last: "lsb (w::'a::finite word) = last (to_bl w)"
- apply (unfold word_lsb_def uint_bl bin_to_bl_def)
- apply (rule_tac bin="uint w" in bin_exhaust)
- apply (cases "size w")
- apply auto
- apply (auto simp add: bin_to_bl_aux_alt)
- done
-
-lemma word_msb_alt: "msb (w::'a::finite word) = hd (to_bl w)"
- apply (unfold word_msb_nth uint_bl)
- apply (subst hd_conv_nth)
- apply (rule length_greater_0_conv [THEN iffD1])
- apply simp
- apply (simp add : nth_bin_to_bl word_size)
- done
-
-lemma bin_nth_uint':
- "bin_nth (uint w) n = (rev (bin_to_bl (size w) (uint w)) ! n & n < size w)"
- apply (unfold word_size)
- apply (safe elim!: bin_nth_uint_imp)
- apply (frule bin_nth_uint_imp)
- apply (fast dest!: bin_nth_bl)+
- done
-
-lemmas bin_nth_uint = bin_nth_uint' [unfolded word_size]
-
-lemma test_bit_bl: "w !! n = (rev (to_bl w) ! n & n < size w)"
- unfolding to_bl_def word_test_bit_def word_size
- by (rule bin_nth_uint)
-
-lemma to_bl_nth: "n < size w ==> to_bl w ! n = w !! (size w - Suc n)"
- apply (unfold test_bit_bl)
- apply clarsimp
- apply (rule trans)
- apply (rule nth_rev_alt)
- apply (auto simp add: word_size)
- done
-
-lemma of_bl_rep_False: "of_bl (replicate n False @ bs) = of_bl bs"
- unfolding of_bl_def bl_to_bin_rep_F by auto
-
-lemma td_ext_nth':
- "n = size (w::'a word) ==> ofn = set_bits ==> [w, ofn g] = l ==>
- td_ext test_bit ofn {f. ALL i. f i --> i < n} (%h i. h i & i < n)"
- apply (unfold word_size td_ext_def')
- apply safe
- apply (rule_tac [3] ext)
- apply (rule_tac [4] ext)
- apply (unfold word_size of_nth_def test_bit_bl)
- apply safe
- defer
- apply (clarsimp simp: word_bl.Abs_inverse)+
- apply (rule word_bl.Rep_inverse')
- apply (rule sym [THEN trans])
- apply (rule bl_of_nth_nth)
- apply simp
- apply (rule bl_of_nth_inj)
- apply (clarsimp simp add : test_bit_bl word_size)
- done
-
-lemmas td_ext_nth = td_ext_nth' [OF refl refl refl, unfolded word_size]
-
-interpretation test_bit:
- td_ext ["op !! :: 'a word => nat => bool"
- set_bits
- "{f. \<forall>i. f i \<longrightarrow> i < CARD('a)}"
- "(\<lambda>h i. h i \<and> i < CARD('a))"]
- by (rule td_ext_nth)
-
-declare test_bit.Rep' [simp del]
-declare test_bit.Rep' [rule del]
-
-lemmas td_nth = test_bit.td_thm
-
-lemma to_bl_n1:
- "to_bl (-1::'a word) = replicate CARD('a) True"
- apply (rule word_bl.Abs_inverse')
- apply simp
- apply (rule word_eqI)
- apply (clarsimp simp add: word_size test_bit_no)
- apply (auto simp add: word_bl.Abs_inverse test_bit_bl word_size)
- done
-
-end
\ No newline at end of file
--- a/src/HOL/Word/WordDefinition.thy Tue Aug 28 19:45:45 2007 +0200
+++ b/src/HOL/Word/WordDefinition.thy Tue Aug 28 20:13:47 2007 +0200
@@ -8,98 +8,41 @@
header {* Definition of Word Type *}
-theory WordDefinition
-imports Numeral_Type BinOperations TdThs begin
+theory WordDefinition imports Size BinBoolList TdThs begin
typedef (open word) 'a word
- = "{(0::int) ..< 2^CARD('a)}" by auto
+ = "{(0::int) ..< 2^len_of TYPE('a::len0)}" by auto
-instance word :: (type) number ..
+instance word :: (len0) number ..
+instance word :: (type) minus ..
+instance word :: (type) plus ..
+instance word :: (type) one ..
+instance word :: (type) zero ..
+instance word :: (type) times ..
+instance word :: (type) Divides.div ..
+instance word :: (type) power ..
+instance word :: (type) ord ..
instance word :: (type) size ..
instance word :: (type) inverse ..
instance word :: (type) bit ..
-subsection {* Basic arithmetic *}
-
-definition
- Abs_word' :: "int \<Rightarrow> 'a word"
- where "Abs_word' x = Abs_word (x mod 2^CARD('a))"
-
-lemma Rep_word_mod: "Rep_word (x::'a word) mod 2^CARD('a) = Rep_word x"
- by (simp only: mod_pos_pos_trivial Rep_word [simplified])
-
-lemma Rep_word_inverse': "Abs_word' (Rep_word x) = x"
- unfolding Abs_word'_def Rep_word_mod
- by (rule Rep_word_inverse)
-
-lemma Abs_word'_inverse: "Rep_word (Abs_word' z::'a word) = z mod 2^CARD('a)"
- unfolding Abs_word'_def
- by (simp add: Abs_word_inverse)
-
-lemmas Rep_word_simps =
- Rep_word_inject [symmetric]
- Rep_word_mod
- Rep_word_inverse'
- Abs_word'_inverse
-
-instance word :: (type) "{zero,one,plus,minus,times,power}"
- word_zero_def: "0 \<equiv> Abs_word' 0"
- word_one_def: "1 \<equiv> Abs_word' 1"
- word_add_def: "x + y \<equiv> Abs_word' (Rep_word x + Rep_word y)"
- word_mult_def: "x * y \<equiv> Abs_word' (Rep_word x * Rep_word y)"
- word_diff_def: "x - y \<equiv> Abs_word' (Rep_word x - Rep_word y)"
- word_minus_def: "- x \<equiv> Abs_word' (- Rep_word x)"
- word_power_def: "x ^ n \<equiv> Abs_word' (Rep_word x ^ n)"
- ..
-
-lemmas word_arith_defs =
- word_zero_def
- word_one_def
- word_add_def
- word_mult_def
- word_diff_def
- word_minus_def
- word_power_def
-
-instance word :: (type) "{comm_ring,comm_monoid_mult,recpower}"
- apply (intro_classes, unfold word_arith_defs)
- apply (simp_all add: Rep_word_simps zmod_simps ring_simps
- mod_pos_pos_trivial)
- done
-
-instance word :: (finite) comm_ring_1
- apply (intro_classes, unfold word_arith_defs)
- apply (simp_all add: Rep_word_simps zmod_simps ring_simps
- mod_pos_pos_trivial one_less_power)
- done
-
-lemma word_of_nat: "of_nat n = Abs_word' (int n)"
- apply (induct n)
- apply (simp add: word_zero_def)
- apply (simp add: Rep_word_simps word_arith_defs zmod_simps)
- done
-
-lemma word_of_int: "of_int z = Abs_word' z"
- apply (cases z rule: int_diff_cases)
- apply (simp add: Rep_word_simps word_diff_def word_of_nat zmod_simps)
- done
subsection "Type conversions and casting"
constdefs
-- {* representation of words using unsigned or signed bins,
only difference in these is the type class *}
- word_of_int :: "int => 'a word"
- "word_of_int w == Abs_word (bintrunc CARD('a) w)"
+ word_of_int :: "int => 'a :: len0 word"
+ "word_of_int w == Abs_word (bintrunc (len_of TYPE ('a)) w)"
-- {* uint and sint cast a word to an integer,
uint treats the word as unsigned,
sint treats the most-significant-bit as a sign bit *}
- uint :: "'a word => int"
+ uint :: "'a :: len0 word => int"
"uint w == Rep_word w"
- sint :: "'a :: finite word => int"
- sint_uint: "sint w == sbintrunc (CARD('a) - 1) (uint w)"
- unat :: "'a word => nat"
+ sint :: "'a :: len word => int"
+ sint_uint: "sint w == sbintrunc (len_of TYPE ('a) - 1) (uint w)"
+ unat :: "'a :: len0 word => nat"
"unat w == nat (uint w)"
-- "the sets of integers representing the words"
@@ -112,12 +55,38 @@
norm_sint :: "nat => int => int"
"norm_sint n w == (w + 2 ^ (n - 1)) mod 2 ^ n - 2 ^ (n - 1)"
+ -- "cast a word to a different length"
+ scast :: "'a :: len word => 'b :: len word"
+ "scast w == word_of_int (sint w)"
+ ucast :: "'a :: len0 word => 'b :: len0 word"
+ "ucast w == word_of_int (uint w)"
+
+ -- "whether a cast (or other) function is to a longer or shorter length"
+ source_size :: "('a :: len0 word => 'b) => nat"
+ "source_size c == let arb = arbitrary ; x = c arb in size arb"
+ target_size :: "('a => 'b :: len0 word) => nat"
+ "target_size c == size (c arbitrary)"
+ is_up :: "('a :: len0 word => 'b :: len0 word) => bool"
+ "is_up c == source_size c <= target_size c"
+ is_down :: "('a :: len0 word => 'b :: len0 word) => bool"
+ "is_down c == target_size c <= source_size c"
+
+constdefs
+ of_bl :: "bool list => 'a :: len0 word"
+ "of_bl bl == word_of_int (bl_to_bin bl)"
+ to_bl :: "'a :: len0 word => bool list"
+ "to_bl w ==
+ bin_to_bl (len_of TYPE ('a)) (uint w)"
+
+ word_reverse :: "'a :: len0 word => 'a word"
+ "word_reverse w == of_bl (rev (to_bl w))"
+
defs (overloaded)
- word_size: "size (w :: 'a word) == CARD('a)"
+ word_size: "size (w :: 'a :: len0 word) == len_of TYPE('a)"
word_number_of_def: "number_of w == word_of_int w"
constdefs
- word_int_case :: "(int => 'b) => ('a word) => 'b"
+ word_int_case :: "(int => 'b) => ('a :: len0 word) => 'b"
"word_int_case f w == f (uint w)"
syntax
@@ -128,98 +97,180 @@
subsection "Arithmetic operations"
-lemma Abs_word'_eq: "Abs_word' = word_of_int"
- unfolding expand_fun_eq Abs_word'_def word_of_int_def
- by (simp add: bintrunc_mod2p)
+defs (overloaded)
+ word_1_wi: "(1 :: ('a :: len0) word) == word_of_int 1"
+ word_0_wi: "(0 :: ('a :: len0) word) == word_of_int 0"
-lemma word_1_wi: "(1 :: ('a) word) == word_of_int 1"
- by (simp only: word_arith_defs Abs_word'_eq)
-
-lemma word_0_wi: "(0 :: ('a) word) == word_of_int 0"
- by (simp only: word_arith_defs Abs_word'_eq)
+ word_le_def: "a <= b == uint a <= uint b"
+ word_less_def: "x < y == x <= y & x ~= (y :: 'a :: len0 word)"
constdefs
- word_succ :: "'a word => 'a word"
+ word_succ :: "'a :: len0 word => 'a word"
"word_succ a == word_of_int (Numeral.succ (uint a))"
- word_pred :: "'a word => 'a word"
+ word_pred :: "'a :: len0 word => 'a word"
"word_pred a == word_of_int (Numeral.pred (uint a))"
+ udvd :: "'a::len word => 'a::len word => bool" (infixl "udvd" 50)
+ "a udvd b == EX n>=0. uint b = n * uint a"
+
+ word_sle :: "'a :: len word => 'a word => bool" ("(_/ <=s _)" [50, 51] 50)
+ "a <=s b == sint a <= sint b"
+
+ word_sless :: "'a :: len word => 'a word => bool" ("(_/ <s _)" [50, 51] 50)
+ "(x <s y) == (x <=s y & x ~= y)"
+
consts
- word_power :: "'a word => nat => 'a word"
+ word_power :: "'a :: len0 word => nat => 'a word"
primrec
"word_power a 0 = 1"
"word_power a (Suc n) = a * word_power a n"
-lemma
+defs (overloaded)
word_pow: "power == word_power"
- apply (rule eq_reflection, rule ext, rule ext)
- apply (rename_tac n, induct_tac n, simp_all add: power_Suc)
- done
-
-lemma
word_add_def: "a + b == word_of_int (uint a + uint b)"
-and
word_sub_wi: "a - b == word_of_int (uint a - uint b)"
-and
word_minus_def: "- a == word_of_int (- uint a)"
-and
word_mult_def: "a * b == word_of_int (uint a * uint b)"
- by (simp_all only: word_arith_defs Abs_word'_eq uint_def)
+ word_div_def: "a div b == word_of_int (uint a div uint b)"
+ word_mod_def: "a mod b == word_of_int (uint a mod uint b)"
+
subsection "Bit-wise operations"
defs (overloaded)
word_and_def:
- "(a::'a word) AND b == word_of_int (uint a AND uint b)"
+ "(a::'a::len0 word) AND b == word_of_int (uint a AND uint b)"
word_or_def:
- "(a::'a word) OR b == word_of_int (uint a OR uint b)"
+ "(a::'a::len0 word) OR b == word_of_int (uint a OR uint b)"
word_xor_def:
- "(a::'a word) XOR b == word_of_int (uint a XOR uint b)"
+ "(a::'a::len0 word) XOR b == word_of_int (uint a XOR uint b)"
word_not_def:
- "NOT (a::'a word) == word_of_int (NOT (uint a))"
+ "NOT (a::'a::len0 word) == word_of_int (NOT (uint a))"
word_test_bit_def:
- "test_bit (a::'a word) == bin_nth (uint a)"
+ "test_bit (a::'a::len0 word) == bin_nth (uint a)"
word_set_bit_def:
- "set_bit (a::'a word) n x ==
+ "set_bit (a::'a::len0 word) n x ==
word_of_int (bin_sc n (If x bit.B1 bit.B0) (uint a))"
+ word_set_bits_def:
+ "(BITS n. f n)::'a::len0 word == of_bl (bl_of_nth (len_of TYPE ('a)) f)"
+
word_lsb_def:
- "lsb (a::'a word) == bin_last (uint a) = bit.B1"
+ "lsb (a::'a::len0 word) == bin_last (uint a) = bit.B1"
word_msb_def:
- "msb (a::'a::finite word) == bin_sign (sint a) = Numeral.Min"
+ "msb (a::'a::len word) == bin_sign (sint a) = Numeral.Min"
constdefs
- setBit :: "'a word => nat => 'a word"
+ setBit :: "'a :: len0 word => nat => 'a word"
"setBit w n == set_bit w n True"
- clearBit :: "'a word => nat => 'a word"
+ clearBit :: "'a :: len0 word => nat => 'a word"
"clearBit w n == set_bit w n False"
+subsection "Shift operations"
+
+constdefs
+ shiftl1 :: "'a :: len0 word => 'a word"
+ "shiftl1 w == word_of_int (uint w BIT bit.B0)"
+
+ -- "shift right as unsigned or as signed, ie logical or arithmetic"
+ shiftr1 :: "'a :: len0 word => 'a word"
+ "shiftr1 w == word_of_int (bin_rest (uint w))"
+
+ sshiftr1 :: "'a :: len word => 'a word"
+ "sshiftr1 w == word_of_int (bin_rest (sint w))"
+
+ bshiftr1 :: "bool => 'a :: len word => 'a word"
+ "bshiftr1 b w == of_bl (b # butlast (to_bl w))"
+
+ sshiftr :: "'a :: len word => nat => 'a word" (infixl ">>>" 55)
+ "w >>> n == (sshiftr1 ^ n) w"
+
+ mask :: "nat => 'a::len word"
+ "mask n == (1 << n) - 1"
+
+ revcast :: "'a :: len0 word => 'b :: len0 word"
+ "revcast w == of_bl (takefill False (len_of TYPE('b)) (to_bl w))"
+
+ slice1 :: "nat => 'a :: len0 word => 'b :: len0 word"
+ "slice1 n w == of_bl (takefill False n (to_bl w))"
+
+ slice :: "nat => 'a :: len0 word => 'b :: len0 word"
+ "slice n w == slice1 (size w - n) w"
+
+
+defs (overloaded)
+ shiftl_def: "(w::'a::len0 word) << n == (shiftl1 ^ n) w"
+ shiftr_def: "(w::'a::len0 word) >> n == (shiftr1 ^ n) w"
+
+
+subsection "Rotation"
+
+constdefs
+ rotater1 :: "'a list => 'a list"
+ "rotater1 ys ==
+ case ys of [] => [] | x # xs => last ys # butlast ys"
+
+ rotater :: "nat => 'a list => 'a list"
+ "rotater n == rotater1 ^ n"
+
+ word_rotr :: "nat => 'a :: len0 word => 'a :: len0 word"
+ "word_rotr n w == of_bl (rotater n (to_bl w))"
+
+ word_rotl :: "nat => 'a :: len0 word => 'a :: len0 word"
+ "word_rotl n w == of_bl (rotate n (to_bl w))"
+
+ word_roti :: "int => 'a :: len0 word => 'a :: len0 word"
+ "word_roti i w == if i >= 0 then word_rotr (nat i) w
+ else word_rotl (nat (- i)) w"
+
+
+subsection "Split and cat operations"
+
+constdefs
+ word_cat :: "'a :: len0 word => 'b :: len0 word => 'c :: len0 word"
+ "word_cat a b == word_of_int (bin_cat (uint a) (len_of TYPE ('b)) (uint b))"
+
+ word_split :: "'a :: len0 word => ('b :: len0 word) * ('c :: len0 word)"
+ "word_split a ==
+ case bin_split (len_of TYPE ('c)) (uint a) of
+ (u, v) => (word_of_int u, word_of_int v)"
+
+ word_rcat :: "'a :: len0 word list => 'b :: len0 word"
+ "word_rcat ws ==
+ word_of_int (bin_rcat (len_of TYPE ('a)) (map uint ws))"
+
+ word_rsplit :: "'a :: len0 word => 'b :: len word list"
+ "word_rsplit w ==
+ map word_of_int (bin_rsplit (len_of TYPE ('b)) (len_of TYPE ('a), uint w))"
+
constdefs
-- "Largest representable machine integer."
- max_word :: "'a::finite word"
- "max_word \<equiv> word_of_int (2^CARD('a) - 1)"
+ max_word :: "'a::len word"
+ "max_word \<equiv> word_of_int (2^len_of TYPE('a) - 1)"
consts
- of_bool :: "bool \<Rightarrow> 'a::finite word"
+ of_bool :: "bool \<Rightarrow> 'a::len word"
primrec
"of_bool False = 0"
"of_bool True = 1"
+lemmas of_nth_def = word_set_bits_def
+
lemmas word_size_gt_0 [iff] =
- xtr1 [OF word_size [THEN meta_eq_to_obj_eq] zero_less_card_finite, standard]
-lemmas lens_gt_0 = word_size_gt_0 zero_less_card_finite
+ xtr1 [OF word_size [THEN meta_eq_to_obj_eq] len_gt_0, standard]
+lemmas lens_gt_0 = word_size_gt_0 len_gt_0
lemmas lens_not_0 [iff] = lens_gt_0 [THEN gr_implies_not0, standard]
lemma uints_num: "uints n = {i. 0 \<le> i \<and> i < 2 ^ n}"
@@ -236,16 +287,16 @@
lemma
Rep_word_0:"0 <= Rep_word x" and
- Rep_word_lt: "Rep_word (x::'a word) < 2 ^ CARD('a)"
+ Rep_word_lt: "Rep_word (x::'a::len0 word) < 2 ^ len_of TYPE('a)"
by (auto simp: Rep_word [simplified])
lemma Rep_word_mod_same:
- "Rep_word x mod 2 ^ CARD('a) = Rep_word (x::'a word)"
+ "Rep_word x mod 2 ^ len_of TYPE('a) = Rep_word (x::'a::len0 word)"
by (simp add: int_mod_eq Rep_word_lt Rep_word_0)
lemma td_ext_uint:
- "td_ext (uint :: 'a word => int) word_of_int (uints CARD('a))
- (%w::int. w mod 2 ^ CARD('a))"
+ "td_ext (uint :: 'a word => int) word_of_int (uints (len_of TYPE('a::len0)))
+ (%w::int. w mod 2 ^ len_of TYPE('a))"
apply (unfold td_ext_def')
apply (simp add: uints_num uint_def word_of_int_def bintrunc_mod2p)
apply (simp add: Rep_word_mod_same Rep_word_0 Rep_word_lt
@@ -255,34 +306,33 @@
lemmas int_word_uint = td_ext_uint [THEN td_ext.eq_norm, standard]
interpretation word_uint:
- td_ext ["uint::'a word \<Rightarrow> int"
+ td_ext ["uint::'a::len0 word \<Rightarrow> int"
word_of_int
- "uints CARD('a)"
- "\<lambda>w. w mod 2 ^ CARD('a)"]
+ "uints (len_of TYPE('a::len0))"
+ "\<lambda>w. w mod 2 ^ len_of TYPE('a::len0)"]
by (rule td_ext_uint)
lemmas td_uint = word_uint.td_thm
lemmas td_ext_ubin = td_ext_uint
- [simplified zero_less_card_finite no_bintr_alt1 [symmetric]]
+ [simplified len_gt_0 no_bintr_alt1 [symmetric]]
interpretation word_ubin:
- td_ext ["uint::'a word \<Rightarrow> int"
+ td_ext ["uint::'a::len0 word \<Rightarrow> int"
word_of_int
- "uints CARD('a)"
- "bintrunc CARD('a)"]
+ "uints (len_of TYPE('a::len0))"
+ "bintrunc (len_of TYPE('a::len0))"]
by (rule td_ext_ubin)
lemma sint_sbintrunc':
"sint (word_of_int bin :: 'a word) =
- (sbintrunc (CARD('a :: finite) - 1) bin)"
+ (sbintrunc (len_of TYPE ('a :: len) - 1) bin)"
unfolding sint_uint
by (auto simp: word_ubin.eq_norm sbintrunc_bintrunc_lt)
lemma uint_sint:
- "uint w = bintrunc CARD('a) (sint (w :: 'a :: finite word))"
+ "uint w = bintrunc (len_of TYPE('a)) (sint (w :: 'a :: len word))"
unfolding sint_uint by (auto simp: bintrunc_sbintrunc_le)
-
lemma bintr_uint':
"n >= size w ==> bintrunc n (uint w) = uint w"
@@ -302,11 +352,11 @@
lemmas wi_bintr = wi_bintr' [unfolded word_size]
lemma td_ext_sbin:
- "td_ext (sint :: 'a word => int) word_of_int (sints CARD('a::finite))
- (sbintrunc (CARD('a) - 1))"
+ "td_ext (sint :: 'a word => int) word_of_int (sints (len_of TYPE('a::len)))
+ (sbintrunc (len_of TYPE('a) - 1))"
apply (unfold td_ext_def' sint_uint)
apply (simp add : word_ubin.eq_norm)
- apply (cases "CARD('a)")
+ apply (cases "len_of TYPE('a)")
apply (auto simp add : sints_def)
apply (rule sym [THEN trans])
apply (rule word_ubin.Abs_norm)
@@ -316,25 +366,25 @@
done
lemmas td_ext_sint = td_ext_sbin
- [simplified zero_less_card_finite no_sbintr_alt2 Suc_pred' [symmetric]]
+ [simplified len_gt_0 no_sbintr_alt2 Suc_pred' [symmetric]]
(* We do sint before sbin, before sint is the user version
and interpretations do not produce thm duplicates. I.e.
we get the name word_sint.Rep_eqD, but not word_sbin.Req_eqD,
because the latter is the same thm as the former *)
interpretation word_sint:
- td_ext ["sint ::'a::finite word => int"
+ td_ext ["sint ::'a::len word => int"
word_of_int
- "sints CARD('a::finite)"
- "%w. (w + 2^(CARD('a::finite) - 1)) mod 2^CARD('a::finite) -
- 2 ^ (CARD('a::finite) - 1)"]
+ "sints (len_of TYPE('a::len))"
+ "%w. (w + 2^(len_of TYPE('a::len) - 1)) mod 2^len_of TYPE('a::len) -
+ 2 ^ (len_of TYPE('a::len) - 1)"]
by (rule td_ext_sint)
interpretation word_sbin:
- td_ext ["sint ::'a::finite word => int"
+ td_ext ["sint ::'a::len word => int"
word_of_int
- "sints CARD('a::finite)"
- "sbintrunc (CARD('a::finite) - 1)"]
+ "sints (len_of TYPE('a::len))"
+ "sbintrunc (len_of TYPE('a::len) - 1)"]
by (rule td_ext_sbin)
lemmas int_word_sint = td_ext_sint [THEN td_ext.eq_norm, standard]
@@ -347,21 +397,28 @@
lemma word_no_wi: "number_of = word_of_int"
by (auto simp: word_number_of_def intro: ext)
+lemma to_bl_def':
+ "(to_bl :: 'a :: len0 word => bool list) =
+ bin_to_bl (len_of TYPE('a)) o uint"
+ by (auto simp: to_bl_def intro: ext)
+
+lemmas word_reverse_no_def [simp] = word_reverse_def [of "number_of ?w"]
+
lemmas uints_mod = uints_def [unfolded no_bintr_alt1]
lemma uint_bintrunc: "uint (number_of bin :: 'a word) =
- number_of (bintrunc CARD('a) bin)"
+ number_of (bintrunc (len_of TYPE ('a :: len0)) bin)"
unfolding word_number_of_def number_of_eq
by (auto intro: word_ubin.eq_norm)
lemma sint_sbintrunc: "sint (number_of bin :: 'a word) =
- number_of (sbintrunc (CARD('a :: finite) - 1) bin)"
+ number_of (sbintrunc (len_of TYPE ('a :: len) - 1) bin)"
unfolding word_number_of_def number_of_eq
by (auto intro!: word_sbin.eq_norm simp del: one_is_Suc_zero)
lemma unat_bintrunc:
- "unat (number_of bin :: 'a word) =
- number_of (bintrunc CARD('a) bin)"
+ "unat (number_of bin :: 'a :: len0 word) =
+ number_of (bintrunc (len_of TYPE('a)) bin)"
unfolding unat_def nat_number_of_def
by (simp only: uint_bintrunc)
@@ -371,7 +428,7 @@
sint_sbintrunc [simp]
unat_bintrunc [simp]
-lemma size_0_eq: "size (w :: 'a word) = 0 ==> v = w"
+lemma size_0_eq: "size (w :: 'a :: len0 word) = 0 ==> v = w"
apply (unfold word_size)
apply (rule word_uint.Rep_eqD)
apply (rule box_equals)
@@ -396,7 +453,7 @@
iffD2 [OF linorder_not_le uint_m2p_neg, standard]
lemma lt2p_lem:
- "CARD('a) <= n ==> uint (w :: 'a word) < 2 ^ n"
+ "len_of TYPE('a) <= n ==> uint (w :: 'a :: len0 word) < 2 ^ n"
by (rule xtr8 [OF _ uint_lt2p]) simp
lemmas uint_le_0_iff [simp] =
@@ -406,13 +463,13 @@
unfolding unat_def by auto
lemma uint_number_of:
- "uint (number_of b :: 'a word) = number_of b mod 2 ^ CARD('a)"
+ "uint (number_of b :: 'a :: len0 word) = number_of b mod 2 ^ len_of TYPE('a)"
unfolding word_number_of_alt
by (simp only: int_word_uint)
lemma unat_number_of:
"bin_sign b = Numeral.Pls ==>
- unat (number_of b::'a word) = number_of b mod 2 ^ CARD('a)"
+ unat (number_of b::'a::len0 word) = number_of b mod 2 ^ len_of TYPE ('a)"
apply (unfold unat_def)
apply (clarsimp simp only: uint_number_of)
apply (rule nat_mod_distrib [THEN trans])
@@ -420,31 +477,31 @@
apply (simp_all add: nat_power_eq)
done
-lemma sint_number_of: "sint (number_of b :: 'a :: finite word) = (number_of b +
- 2 ^ (CARD('a) - 1)) mod 2 ^ CARD('a) -
- 2 ^ (CARD('a) - 1)"
+lemma sint_number_of: "sint (number_of b :: 'a :: len word) = (number_of b +
+ 2 ^ (len_of TYPE('a) - 1)) mod 2 ^ len_of TYPE('a) -
+ 2 ^ (len_of TYPE('a) - 1)"
unfolding word_number_of_alt by (rule int_word_sint)
lemma word_of_int_bin [simp] :
- "(word_of_int (number_of bin) :: 'a word) = (number_of bin)"
+ "(word_of_int (number_of bin) :: 'a :: len0 word) = (number_of bin)"
unfolding word_number_of_alt by auto
lemma word_int_case_wi:
"word_int_case f (word_of_int i :: 'b word) =
- f (i mod 2 ^ CARD('b))"
+ f (i mod 2 ^ len_of TYPE('b::len0))"
unfolding word_int_case_def by (simp add: word_uint.eq_norm)
lemma word_int_split:
"P (word_int_case f x) =
- (ALL i. x = (word_of_int i :: 'b word) &
- 0 <= i & i < 2 ^ CARD('b) --> P (f i))"
+ (ALL i. x = (word_of_int i :: 'b :: len0 word) &
+ 0 <= i & i < 2 ^ len_of TYPE('b) --> P (f i))"
unfolding word_int_case_def
by (auto simp: word_uint.eq_norm int_mod_eq')
lemma word_int_split_asm:
"P (word_int_case f x) =
- (~ (EX n. x = (word_of_int n :: 'b word) &
- 0 <= n & n < 2 ^ CARD('b) & ~ P (f n)))"
+ (~ (EX n. x = (word_of_int n :: 'b::len0 word) &
+ 0 <= n & n < 2 ^ len_of TYPE('b::len0) & ~ P (f n)))"
unfolding word_int_case_def
by (auto simp: word_uint.eq_norm int_mod_eq')
@@ -466,10 +523,10 @@
lemmas sint_below_size = sint_range_size
[THEN conjunct1, THEN [2] order_trans, folded One_nat_def, standard]
-lemma test_bit_eq_iff: "(test_bit (u::'a word) = test_bit v) = (u = v)"
+lemma test_bit_eq_iff: "(test_bit (u::'a::len0 word) = test_bit v) = (u = v)"
unfolding word_test_bit_def by (simp add: bin_nth_eq_iff)
-lemma test_bit_size [rule_format] : "(w::'a word) !! n --> n < size w"
+lemma test_bit_size [rule_format] : "(w::'a::len0 word) !! n --> n < size w"
apply (unfold word_test_bit_def)
apply (subst word_ubin.norm_Rep [symmetric])
apply (simp only: nth_bintr word_size)
@@ -477,7 +534,7 @@
done
lemma word_eqI [rule_format] :
- fixes u :: "'a word"
+ fixes u :: "'a::len0 word"
shows "(ALL n. n < size u --> u !! n = v !! n) ==> u = v"
apply (rule test_bit_eq_iff [THEN iffD1])
apply (rule ext)
@@ -515,6 +572,88 @@
lemmas bin_nth_uint_imp = bin_nth_uint_imp' [rule_format, unfolded word_size]
lemmas bin_nth_sint = bin_nth_sint' [rule_format, unfolded word_size]
+(* type definitions theorem for in terms of equivalent bool list *)
+lemma td_bl:
+ "type_definition (to_bl :: 'a::len0 word => bool list)
+ of_bl
+ {bl. length bl = len_of TYPE('a)}"
+ apply (unfold type_definition_def of_bl_def to_bl_def)
+ apply (simp add: word_ubin.eq_norm)
+ apply safe
+ apply (drule sym)
+ apply simp
+ done
+
+interpretation word_bl:
+ type_definition ["to_bl :: 'a::len0 word => bool list"
+ of_bl
+ "{bl. length bl = len_of TYPE('a::len0)}"]
+ by (rule td_bl)
+
+lemma word_size_bl: "size w == size (to_bl w)"
+ unfolding word_size by auto
+
+lemma to_bl_use_of_bl:
+ "(to_bl w = bl) = (w = of_bl bl \<and> length bl = length (to_bl w))"
+ by (fastsimp elim!: word_bl.Abs_inverse [simplified])
+
+lemma to_bl_word_rev: "to_bl (word_reverse w) = rev (to_bl w)"
+ unfolding word_reverse_def by (simp add: word_bl.Abs_inverse)
+
+lemma word_rev_rev [simp] : "word_reverse (word_reverse w) = w"
+ unfolding word_reverse_def by (simp add : word_bl.Abs_inverse)
+
+lemma word_rev_gal: "word_reverse w = u ==> word_reverse u = w"
+ by auto
+
+lemmas word_rev_gal' = sym [THEN word_rev_gal, symmetric, standard]
+
+lemmas length_bl_gt_0 [iff] = xtr1 [OF word_bl.Rep' len_gt_0, standard]
+lemmas bl_not_Nil [iff] =
+ length_bl_gt_0 [THEN length_greater_0_conv [THEN iffD1], standard]
+lemmas length_bl_neq_0 [iff] = length_bl_gt_0 [THEN gr_implies_not0]
+
+lemma hd_bl_sign_sint: "hd (to_bl w) = (bin_sign (sint w) = Numeral.Min)"
+ apply (unfold to_bl_def sint_uint)
+ apply (rule trans [OF _ bl_sbin_sign])
+ apply simp
+ done
+
+lemma of_bl_drop':
+ "lend = length bl - len_of TYPE ('a :: len0) ==>
+ of_bl (drop lend bl) = (of_bl bl :: 'a word)"
+ apply (unfold of_bl_def)
+ apply (clarsimp simp add : trunc_bl2bin [symmetric])
+ done
+
+lemmas of_bl_no = of_bl_def [folded word_number_of_def]
+
+lemma test_bit_of_bl:
+ "(of_bl bl::'a::len0 word) !! n = (rev bl ! n \<and> n < len_of TYPE('a) \<and> n < length bl)"
+ apply (unfold of_bl_def word_test_bit_def)
+ apply (auto simp add: word_size word_ubin.eq_norm nth_bintr bin_nth_of_bl)
+ done
+
+lemma no_of_bl:
+ "(number_of bin ::'a::len0 word) = of_bl (bin_to_bl (len_of TYPE ('a)) bin)"
+ unfolding word_size of_bl_no by (simp add : word_number_of_def)
+
+lemma uint_bl: "to_bl w == bin_to_bl (size w) (uint w)"
+ unfolding word_size to_bl_def by auto
+
+lemma to_bl_bin: "bl_to_bin (to_bl w) = uint w"
+ unfolding uint_bl by (simp add : word_size)
+
+lemma to_bl_of_bin:
+ "to_bl (word_of_int bin::'a::len0 word) = bin_to_bl (len_of TYPE('a)) bin"
+ unfolding uint_bl by (clarsimp simp add: word_ubin.eq_norm word_size)
+
+lemmas to_bl_no_bin [simp] = to_bl_of_bin [folded word_number_of_def]
+
+lemma to_bl_to_bin [simp] : "bl_to_bin (to_bl w) = uint w"
+ unfolding uint_bl by (simp add : word_size)
+
+lemmas uint_bl_bin [simp] = trans [OF bin_bl_bin word_ubin.norm_Rep, standard]
lemmas num_AB_u [simp] = word_uint.Rep_inverse
[unfolded o_def word_number_of_def [symmetric], standard]
@@ -549,14 +688,14 @@
may want these in reverse, but loop as simp rules, so use following *)
lemma num_of_bintr':
- "bintrunc CARD('a) a = b ==>
+ "bintrunc (len_of TYPE('a :: len0)) a = b ==>
number_of a = (number_of b :: 'a word)"
apply safe
apply (rule_tac num_of_bintr [symmetric])
done
lemma num_of_sbintr':
- "sbintrunc (CARD('a :: finite) - 1) a = b ==>
+ "sbintrunc (len_of TYPE('a :: len) - 1) a = b ==>
number_of a = (number_of b :: 'a word)"
apply safe
apply (rule_tac num_of_sbintr [symmetric])
@@ -566,32 +705,7 @@
OF num_of_bintr word_number_of_def [THEN meta_eq_to_obj_eq], standard]
lemmas num_abs_sbintr = sym [THEN trans,
OF num_of_sbintr word_number_of_def [THEN meta_eq_to_obj_eq], standard]
-
-lemmas test_bit_def' = word_test_bit_def [THEN meta_eq_to_obj_eq, THEN fun_cong]
-
-lemmas word_log_defs = word_and_def word_or_def word_xor_def word_not_def
-lemmas word_log_bin_defs = word_log_defs
-
-
-subsection {* Casting words to different lengths *}
-
-constdefs
- -- "cast a word to a different length"
- scast :: "'a :: finite word => 'b :: finite word"
- "scast w == word_of_int (sint w)"
- ucast :: "'a word => 'b word"
- "ucast w == word_of_int (uint w)"
-
- -- "whether a cast (or other) function is to a longer or shorter length"
- source_size :: "('a word => 'b) => nat"
- "source_size c == let arb = arbitrary ; x = c arb in size arb"
- target_size :: "('a => 'b word) => nat"
- "target_size c == size (c arbitrary)"
- is_up :: "('a word => 'b word) => bool"
- "is_up c == source_size c <= target_size c"
- is_down :: "('a word => 'b word) => bool"
- "is_down c == target_size c <= source_size c"
-
+
(** cast - note, no arg for new length, as it's determined by type of result,
thus in "cast w = w, the type means cast to length of w! **)
@@ -601,8 +715,12 @@
lemma scast_id: "scast w = w"
unfolding scast_def by auto
+lemma ucast_bl: "ucast w == of_bl (to_bl w)"
+ unfolding ucast_def of_bl_def uint_bl
+ by (auto simp add : word_size)
+
lemma nth_ucast:
- "(ucast w::'a word) !! n = (w !! n & n < CARD('a))"
+ "(ucast w::'a::len0 word) !! n = (w !! n & n < len_of TYPE('a))"
apply (unfold ucast_def test_bit_bin)
apply (simp add: word_ubin.eq_norm nth_bintr word_size)
apply (fast elim!: bin_nth_uint_imp)
@@ -611,13 +729,13 @@
(* for literal u(s)cast *)
lemma ucast_bintr [simp]:
- "ucast (number_of w ::'a word) =
- number_of (bintrunc CARD('a) w)"
+ "ucast (number_of w ::'a::len0 word) =
+ number_of (bintrunc (len_of TYPE('a)) w)"
unfolding ucast_def by simp
lemma scast_sbintr [simp]:
- "scast (number_of w ::'a::finite word) =
- number_of (sbintrunc (CARD('a) - Suc 0) w)"
+ "scast (number_of w ::'a::len word) =
+ number_of (sbintrunc (len_of TYPE('a) - Suc 0) w)"
unfolding scast_def by simp
lemmas source_size = source_size_def [unfolded Let_def word_size]
@@ -639,6 +757,50 @@
apply simp
done
+lemma word_rev_tf':
+ "r = to_bl (of_bl bl) ==> r = rev (takefill False (length r) (rev bl))"
+ unfolding of_bl_def uint_bl
+ by (clarsimp simp add: bl_bin_bl_rtf word_ubin.eq_norm word_size)
+
+lemmas word_rev_tf = refl [THEN word_rev_tf', unfolded word_bl.Rep', standard]
+
+lemmas word_rep_drop = word_rev_tf [simplified takefill_alt,
+ simplified, simplified rev_take, simplified]
+
+lemma to_bl_ucast:
+ "to_bl (ucast (w::'b::len0 word) ::'a::len0 word) =
+ replicate (len_of TYPE('a) - len_of TYPE('b)) False @
+ drop (len_of TYPE('b) - len_of TYPE('a)) (to_bl w)"
+ apply (unfold ucast_bl)
+ apply (rule trans)
+ apply (rule word_rep_drop)
+ apply simp
+ done
+
+lemma ucast_up_app':
+ "uc = ucast ==> source_size uc + n = target_size uc ==>
+ to_bl (uc w) = replicate n False @ (to_bl w)"
+ apply (auto simp add : source_size target_size to_bl_ucast)
+ apply (rule_tac f = "%n. replicate n False" in arg_cong)
+ apply simp
+ done
+
+lemma ucast_down_drop':
+ "uc = ucast ==> source_size uc = target_size uc + n ==>
+ to_bl (uc w) = drop n (to_bl w)"
+ by (auto simp add : source_size target_size to_bl_ucast)
+
+lemma scast_down_drop':
+ "sc = scast ==> source_size sc = target_size sc + n ==>
+ to_bl (sc w) = drop n (to_bl w)"
+ apply (subgoal_tac "sc = ucast")
+ apply safe
+ apply simp
+ apply (erule refl [THEN ucast_down_drop'])
+ apply (rule refl [THEN down_cast_same', symmetric])
+ apply (simp add : source_size target_size is_down)
+ done
+
lemma sint_up_scast':
"sc = scast ==> is_up sc ==> sint (sc w) = sint w"
apply (unfold is_up)
@@ -665,6 +827,9 @@
done
lemmas down_cast_same = refl [THEN down_cast_same']
+lemmas ucast_up_app = refl [THEN ucast_up_app']
+lemmas ucast_down_drop = refl [THEN ucast_down_drop']
+lemmas scast_down_drop = refl [THEN scast_down_drop']
lemmas uint_up_ucast = refl [THEN uint_up_ucast']
lemmas sint_up_scast = refl [THEN sint_up_scast']
@@ -678,8 +843,13 @@
apply (clarsimp simp add: sint_up_scast)
done
+lemma ucast_of_bl_up':
+ "w = of_bl bl ==> size bl <= size w ==> ucast w = of_bl bl"
+ by (auto simp add : nth_ucast word_size test_bit_of_bl intro!: word_eqI)
+
lemmas ucast_up_ucast = refl [THEN ucast_up_ucast']
lemmas scast_up_scast = refl [THEN scast_up_scast']
+lemmas ucast_of_bl_up = refl [THEN ucast_of_bl_up']
lemmas ucast_up_ucast_id = trans [OF ucast_up_ucast ucast_id]
lemmas scast_up_scast_id = trans [OF scast_up_scast scast_id]
@@ -690,25 +860,27 @@
lemmas scast_down_scast_id = isdus [THEN ucast_up_ucast_id]
lemma up_ucast_surj:
- "is_up (ucast :: 'b word => 'a word) ==>
+ "is_up (ucast :: 'b::len0 word => 'a::len0 word) ==>
surj (ucast :: 'a word => 'b word)"
by (rule surjI, erule ucast_up_ucast_id)
lemma up_scast_surj:
- "is_up (scast :: 'b::finite word => 'a::finite word) ==>
+ "is_up (scast :: 'b::len word => 'a::len word) ==>
surj (scast :: 'a word => 'b word)"
by (rule surjI, erule scast_up_scast_id)
lemma down_scast_inj:
- "is_down (scast :: 'b::finite word => 'a::finite word) ==>
+ "is_down (scast :: 'b::len word => 'a::len word) ==>
inj_on (ucast :: 'a word => 'b word) A"
by (rule inj_on_inverseI, erule scast_down_scast_id)
lemma down_ucast_inj:
- "is_down (ucast :: 'b word => 'a word) ==>
+ "is_down (ucast :: 'b::len0 word => 'a::len0 word) ==>
inj_on (ucast :: 'a word => 'b word) A"
by (rule inj_on_inverseI, erule ucast_down_ucast_id)
+lemma of_bl_append_same: "of_bl (X @ to_bl w) = w"
+ by (rule word_bl.Rep_eqD) (simp add: word_rep_drop)
lemma ucast_down_no':
"uc = ucast ==> is_down uc ==> uc (number_of bin) = number_of bin"
@@ -720,4 +892,15 @@
lemmas ucast_down_no = ucast_down_no' [OF refl]
+lemma ucast_down_bl': "uc = ucast ==> is_down uc ==> uc (of_bl bl) = of_bl bl"
+ unfolding of_bl_no by clarify (erule ucast_down_no)
+
+lemmas ucast_down_bl = ucast_down_bl' [OF refl]
+
+lemmas slice_def' = slice_def [unfolded word_size]
+lemmas test_bit_def' = word_test_bit_def [THEN meta_eq_to_obj_eq, THEN fun_cong]
+
+lemmas word_log_defs = word_and_def word_or_def word_xor_def word_not_def
+lemmas word_log_bin_defs = word_log_defs
+
end
--- a/src/HOL/Word/WordGenLib.thy Tue Aug 28 19:45:45 2007 +0200
+++ b/src/HOL/Word/WordGenLib.thy Tue Aug 28 20:13:47 2007 +0200
@@ -14,17 +14,17 @@
declare of_nat_2p [simp]
lemma word_int_cases:
- "\<lbrakk>\<And>n. \<lbrakk>(x ::'a word) = word_of_int n; 0 \<le> n; n < 2^CARD('a)\<rbrakk> \<Longrightarrow> P\<rbrakk>
+ "\<lbrakk>\<And>n. \<lbrakk>(x ::'a::len0 word) = word_of_int n; 0 \<le> n; n < 2^len_of TYPE('a)\<rbrakk> \<Longrightarrow> P\<rbrakk>
\<Longrightarrow> P"
by (cases x rule: word_uint.Abs_cases) (simp add: uints_num)
lemma word_nat_cases [cases type: word]:
- "\<lbrakk>\<And>n. \<lbrakk>(x ::'a::finite word) = of_nat n; n < 2^CARD('a)\<rbrakk> \<Longrightarrow> P\<rbrakk>
+ "\<lbrakk>\<And>n. \<lbrakk>(x ::'a::len word) = of_nat n; n < 2^len_of TYPE('a)\<rbrakk> \<Longrightarrow> P\<rbrakk>
\<Longrightarrow> P"
by (cases x rule: word_unat.Abs_cases) (simp add: unats_def)
lemma max_word_eq:
- "(max_word::'a::finite word) = 2^CARD('a) - 1"
+ "(max_word::'a::len word) = 2^len_of TYPE('a) - 1"
by (simp add: max_word_def word_of_int_hom_syms word_of_int_2p)
lemma max_word_max [simp,intro!]:
@@ -33,14 +33,14 @@
(simp add: max_word_def word_le_def int_word_uint int_mod_eq')
lemma word_of_int_2p_len:
- "word_of_int (2 ^ CARD('a)) = (0::'a word)"
+ "word_of_int (2 ^ len_of TYPE('a)) = (0::'a::len0 word)"
by (subst word_uint.Abs_norm [symmetric])
(simp add: word_of_int_hom_syms)
lemma word_pow_0:
- "(2::'a::finite word) ^ CARD('a) = 0"
+ "(2::'a::len word) ^ len_of TYPE('a) = 0"
proof -
- have "word_of_int (2 ^ CARD('a)) = (0::'a word)"
+ have "word_of_int (2 ^ len_of TYPE('a)) = (0::'a word)"
by (rule word_of_int_2p_len)
thus ?thesis by (simp add: word_of_int_2p)
qed
@@ -53,18 +53,18 @@
done
lemma max_word_minus:
- "max_word = (-1::'a::finite word)"
+ "max_word = (-1::'a::len word)"
proof -
have "-1 + 1 = (0::'a word)" by simp
thus ?thesis by (rule max_word_wrap [symmetric])
qed
lemma max_word_bl [simp]:
- "to_bl (max_word::'a::finite word) = replicate CARD('a) True"
+ "to_bl (max_word::'a::len word) = replicate (len_of TYPE('a)) True"
by (subst max_word_minus to_bl_n1)+ simp
lemma max_test_bit [simp]:
- "(max_word::'a::finite word) !! n = (n < CARD('a))"
+ "(max_word::'a::len word) !! n = (n < len_of TYPE('a))"
by (auto simp add: test_bit_bl word_size)
lemma word_and_max [simp]:
@@ -76,15 +76,15 @@
by (rule word_eqI) (simp add: word_ops_nth_size word_size)
lemma word_ao_dist2:
- "x AND (y OR z) = x AND y OR x AND (z::'a word)"
+ "x AND (y OR z) = x AND y OR x AND (z::'a::len0 word)"
by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
lemma word_oa_dist2:
- "x OR y AND z = (x OR y) AND (x OR (z::'a word))"
+ "x OR y AND z = (x OR y) AND (x OR (z::'a::len0 word))"
by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
lemma word_and_not [simp]:
- "x AND NOT x = (0::'a word)"
+ "x AND NOT x = (0::'a::len0 word)"
by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
lemma word_or_not [simp]:
@@ -111,7 +111,7 @@
by (rule word_boolean)
lemma word_xor_and_or:
- "x XOR y = x AND NOT y OR NOT x AND (y::'a word)"
+ "x XOR y = x AND NOT y OR NOT x AND (y::'a::len0 word)"
by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
interpretation word_bool_alg:
@@ -123,15 +123,15 @@
done
lemma shiftr_0 [iff]:
- "(x::'a word) >> 0 = x"
+ "(x::'a::len0 word) >> 0 = x"
by (simp add: shiftr_bl)
lemma shiftl_0 [simp]:
- "(x :: 'a :: finite word) << 0 = x"
+ "(x :: 'a :: len word) << 0 = x"
by (simp add: shiftl_t2n)
lemma shiftl_1 [simp]:
- "(1::'a::finite word) << n = 2^n"
+ "(1::'a::len word) << n = 2^n"
by (simp add: shiftl_t2n)
lemma uint_lt_0 [simp]:
@@ -139,21 +139,21 @@
by (simp add: linorder_not_less)
lemma shiftr1_1 [simp]:
- "shiftr1 (1::'a::finite word) = 0"
+ "shiftr1 (1::'a::len word) = 0"
by (simp add: shiftr1_def word_0_alt)
lemma shiftr_1[simp]:
- "(1::'a::finite word) >> n = (if n = 0 then 1 else 0)"
+ "(1::'a::len word) >> n = (if n = 0 then 1 else 0)"
by (induct n) (auto simp: shiftr_def)
lemma word_less_1 [simp]:
- "((x::'a::finite word) < 1) = (x = 0)"
+ "((x::'a::len word) < 1) = (x = 0)"
by (simp add: word_less_nat_alt unat_0_iff)
lemma to_bl_mask:
- "to_bl (mask n :: 'a::finite word) =
- replicate (CARD('a) - n) False @
- replicate (min CARD('a) n) True"
+ "to_bl (mask n :: 'a::len word) =
+ replicate (len_of TYPE('a) - n) False @
+ replicate (min (len_of TYPE('a)) n) True"
by (simp add: mask_bl word_rep_drop min_def)
lemma map_replicate_True:
@@ -167,19 +167,19 @@
by (induct xs arbitrary: n) auto
lemma bl_and_mask:
- fixes w :: "'a::finite word"
+ fixes w :: "'a::len word"
fixes n
- defines "n' \<equiv> CARD('a) - n"
+ defines "n' \<equiv> len_of TYPE('a) - n"
shows "to_bl (w AND mask n) = replicate n' False @ drop n' (to_bl w)"
proof -
note [simp] = map_replicate_True map_replicate_False
have "to_bl (w AND mask n) =
- app2 op & (to_bl w) (to_bl (mask n::'a::finite word))"
+ app2 op & (to_bl w) (to_bl (mask n::'a::len word))"
by (simp add: bl_word_and)
also
have "to_bl w = take n' (to_bl w) @ drop n' (to_bl w)" by simp
also
- have "app2 op & \<dots> (to_bl (mask n::'a::finite word)) =
+ have "app2 op & \<dots> (to_bl (mask n::'a::len word)) =
replicate n' False @ drop n' (to_bl w)"
unfolding to_bl_mask n'_def app2_def
by (subst zip_append) auto
@@ -193,7 +193,7 @@
by (simp add: takefill_alt rev_take)
lemma map_nth_0 [simp]:
- "map (op !! (0::'a word)) xs = replicate (length xs) False"
+ "map (op !! (0::'a::len0 word)) xs = replicate (length xs) False"
by (induct xs) auto
lemma uint_plus_if_size:
@@ -206,7 +206,7 @@
word_size)
lemma unat_plus_if_size:
- "unat (x + (y::'a::finite word)) =
+ "unat (x + (y::'a::len word)) =
(if unat x + unat y < 2^size x then
unat x + unat y
else
@@ -217,7 +217,7 @@
done
lemma word_neq_0_conv [simp]:
- fixes w :: "'a :: finite word"
+ fixes w :: "'a :: len word"
shows "(w \<noteq> 0) = (0 < w)"
proof -
have "0 \<le> w" by (rule word_zero_le)
@@ -225,7 +225,7 @@
qed
lemma max_lt:
- "unat (max a b div c) = unat (max a b) div unat (c:: 'a :: finite word)"
+ "unat (max a b div c) = unat (max a b) div unat (c:: 'a :: len word)"
apply (subst word_arith_nat_defs)
apply (subst word_unat.eq_norm)
apply (subst mod_if)
@@ -253,12 +253,12 @@
lemmas unat_sub = unat_sub_simple
lemma word_less_sub1:
- fixes x :: "'a :: finite word"
+ fixes x :: "'a :: len word"
shows "x \<noteq> 0 ==> 1 < x = (0 < x - 1)"
by (simp add: unat_sub_if_size word_less_nat_alt)
lemma word_le_sub1:
- fixes x :: "'a :: finite word"
+ fixes x :: "'a :: len word"
shows "x \<noteq> 0 ==> 1 \<le> x = (0 \<le> x - 1)"
by (simp add: unat_sub_if_size order_le_less word_less_nat_alt)
@@ -268,9 +268,9 @@
word_le_sub1 [of "number_of ?w"]
lemma word_of_int_minus:
- "word_of_int (2^CARD('a) - i) = (word_of_int (-i)::'a::finite word)"
+ "word_of_int (2^len_of TYPE('a) - i) = (word_of_int (-i)::'a::len word)"
proof -
- have x: "2^CARD('a) - i = -i + 2^CARD('a)" by simp
+ have x: "2^len_of TYPE('a) - i = -i + 2^len_of TYPE('a)" by simp
show ?thesis
apply (subst x)
apply (subst word_uint.Abs_norm [symmetric], subst zmod_zadd_self2)
@@ -282,7 +282,7 @@
word_uint.Abs_inject [unfolded uints_num, simplified]
lemma word_le_less_eq:
- "(x ::'z::finite word) \<le> y = (x = y \<or> x < y)"
+ "(x ::'z::len word) \<le> y = (x = y \<or> x < y)"
by (auto simp add: word_less_def)
lemma mod_plus_cong:
@@ -312,7 +312,7 @@
done
lemma word_induct_less:
- "\<lbrakk>P (0::'a::finite word); \<And>n. \<lbrakk>n < m; P n\<rbrakk> \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P m"
+ "\<lbrakk>P (0::'a::len word); \<And>n. \<lbrakk>n < m; P n\<rbrakk> \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P m"
apply (cases m)
apply atomize
apply (erule rev_mp)+
@@ -335,24 +335,24 @@
done
lemma word_induct:
- "\<lbrakk>P (0::'a::finite word); \<And>n. P n \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P m"
+ "\<lbrakk>P (0::'a::len word); \<And>n. P n \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P m"
by (erule word_induct_less, simp)
lemma word_induct2 [induct type]:
- "\<lbrakk>P 0; \<And>n. \<lbrakk>1 + n \<noteq> 0; P n\<rbrakk> \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P (n::'b::finite word)"
+ "\<lbrakk>P 0; \<And>n. \<lbrakk>1 + n \<noteq> 0; P n\<rbrakk> \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P (n::'b::len word)"
apply (rule word_induct, simp)
apply (case_tac "1+n = 0", auto)
done
constdefs
- word_rec :: "'a \<Rightarrow> ('b::finite word \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b word \<Rightarrow> 'a"
+ word_rec :: "'a \<Rightarrow> ('b::len word \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b word \<Rightarrow> 'a"
"word_rec forZero forSuc n \<equiv> nat_rec forZero (forSuc \<circ> of_nat) (unat n)"
lemma word_rec_0: "word_rec z s 0 = z"
by (simp add: word_rec_def)
lemma word_rec_Suc:
- "1 + n \<noteq> (0::'a::finite word) \<Longrightarrow> word_rec z s (1 + n) = s n (word_rec z s n)"
+ "1 + n \<noteq> (0::'a::len word) \<Longrightarrow> word_rec z s (1 + n) = s n (word_rec z s n)"
apply (simp add: word_rec_def unat_word_ariths)
apply (subst nat_mod_eq')
apply (cut_tac x=n in unat_lt2p)
@@ -448,7 +448,7 @@
done
lemma unatSuc:
- "1 + n \<noteq> (0::'a::finite word) \<Longrightarrow> unat (1 + n) = Suc (unat n)"
+ "1 + n \<noteq> (0::'a::len word) \<Longrightarrow> unat (1 + n) = Suc (unat n)"
by unat_arith
end
--- a/src/HOL/Word/WordShift.thy Tue Aug 28 19:45:45 2007 +0200
+++ b/src/HOL/Word/WordShift.thy Tue Aug 28 20:13:47 2007 +0200
@@ -6,28 +6,11 @@
*)
header {* Shifting, Rotating, and Splitting Words *}
-theory WordShift imports WordBitwise WordBoolList begin
+
+theory WordShift imports WordBitwise begin
subsection "Bit shifting"
-constdefs
- shiftl1 :: "'a word => 'a word"
- "shiftl1 w == word_of_int (uint w BIT bit.B0)"
-
- -- "shift right as unsigned or as signed, ie logical or arithmetic"
- shiftr1 :: "'a word => 'a word"
- "shiftr1 w == word_of_int (bin_rest (uint w))"
-
- sshiftr1 :: "'a :: finite word => 'a word"
- "sshiftr1 w == word_of_int (bin_rest (sint w))"
-
- sshiftr :: "'a :: finite word => nat => 'a word" (infixl ">>>" 55)
- "w >>> n == (sshiftr1 ^ n) w"
-
-defs (overloaded)
- shiftl_def: "(w::'a word) << n == (shiftl1 ^ n) w"
- shiftr_def: "(w::'a word) >> n == (shiftr1 ^ n) w"
-
lemma shiftl1_number [simp] :
"shiftl1 (number_of w) = number_of (w BIT bit.B0)"
apply (unfold shiftl1_def word_number_of_def)
@@ -58,10 +41,10 @@
lemma sshiftr1_n1 [simp] : "sshiftr1 -1 = -1"
unfolding sshiftr1_def by auto
-lemma shiftl_0 [simp] : "(0::'a word) << n = 0"
+lemma shiftl_0 [simp] : "(0::'a::len0 word) << n = 0"
unfolding shiftl_def by (induct n) auto
-lemma shiftr_0 [simp] : "(0::'a word) >> n = 0"
+lemma shiftr_0 [simp] : "(0::'a::len0 word) >> n = 0"
unfolding shiftr_def by (induct n) auto
lemma sshiftr_0 [simp] : "0 >>> n = 0"
@@ -78,7 +61,7 @@
done
lemma nth_shiftl' [rule_format]:
- "ALL n. ((w::'a word) << m) !! n = (n < size w & n >= m & w !! (n - m))"
+ "ALL n. ((w::'a::len0 word) << m) !! n = (n < size w & n >= m & w !! (n - m))"
apply (unfold shiftl_def)
apply (induct "m")
apply (force elim!: test_bit_size)
@@ -97,7 +80,7 @@
done
lemma nth_shiftr:
- "\<And>n. ((w::'a word) >> m) !! n = w !! (n + m)"
+ "\<And>n. ((w::'a::len0 word) >> m) !! n = w !! (n + m)"
apply (unfold shiftr_def)
apply (induct "m")
apply (auto simp add : nth_shiftr1)
@@ -187,10 +170,6 @@
subsubsection "shift functions in terms of lists of bools"
-definition
- bshiftr1 :: "bool => 'a :: finite word => 'a word" where
- "bshiftr1 b w == of_bl (b # butlast (to_bl w))"
-
lemmas bshiftr1_no_bin [simp] =
bshiftr1_def [where w="number_of ?w", unfolded to_bl_no_bin]
@@ -202,11 +181,13 @@
by (simp add: bl_to_bin_aux_append bl_to_bin_def)
lemmas shiftl1_bl = shiftl1_of_bl
- [where bl = "to_bl (?w :: ?'a word)", simplified]
+ [where bl = "to_bl (?w :: ?'a :: len0 word)", simplified]
lemma bl_shiftl1:
- "to_bl (shiftl1 (w :: 'a :: finite word)) = tl (to_bl w) @ [False]"
- by (simp add: shiftl1_bl word_rep_drop drop_Suc drop_Cons')
+ "to_bl (shiftl1 (w :: 'a :: len word)) = tl (to_bl w) @ [False]"
+ apply (simp add: shiftl1_bl word_rep_drop drop_Suc drop_Cons')
+ apply (fast intro!: Suc_leI)
+ done
lemma shiftr1_bl: "shiftr1 w = of_bl (butlast (to_bl w))"
apply (unfold shiftr1_def uint_bl of_bl_def)
@@ -215,15 +196,15 @@
done
lemma bl_shiftr1:
- "to_bl (shiftr1 (w :: 'a :: finite word)) = False # butlast (to_bl w)"
+ "to_bl (shiftr1 (w :: 'a :: len word)) = False # butlast (to_bl w)"
unfolding shiftr1_bl
- by (simp add : word_rep_drop zero_less_card_finite [THEN Suc_leI])
+ by (simp add : word_rep_drop len_gt_0 [THEN Suc_leI])
-(* relate the two above : TODO - remove the :: finite restriction on
+(* relate the two above : TODO - remove the :: len restriction on
this theorem and others depending on it *)
lemma shiftl1_rev:
- "shiftl1 (w :: 'a :: finite word) = word_reverse (shiftr1 (word_reverse w))"
+ "shiftl1 (w :: 'a :: len word) = word_reverse (shiftr1 (word_reverse w))"
apply (unfold word_reverse_def)
apply (rule word_bl.Rep_inverse' [symmetric])
apply (simp add: bl_shiftl1 bl_shiftr1 word_bl.Abs_inverse)
@@ -232,7 +213,7 @@
done
lemma shiftl_rev:
- "shiftl (w :: 'a :: finite word) n = word_reverse (shiftr (word_reverse w) n)"
+ "shiftl (w :: 'a :: len word) n = word_reverse (shiftr (word_reverse w) n)"
apply (unfold shiftl_def shiftr_def)
apply (induct "n")
apply (auto simp add : shiftl1_rev)
@@ -245,7 +226,7 @@
lemmas rev_shiftr = shiftl_rev [THEN word_rev_gal', standard]
lemma bl_sshiftr1:
- "to_bl (sshiftr1 (w :: 'a :: finite word)) = hd (to_bl w) # butlast (to_bl w)"
+ "to_bl (sshiftr1 (w :: 'a :: len word)) = hd (to_bl w) # butlast (to_bl w)"
apply (unfold sshiftr1_def uint_bl word_size)
apply (simp add: butlast_rest_bin word_ubin.eq_norm)
apply (simp add: sint_uint)
@@ -257,13 +238,14 @@
nth_bin_to_bl bin_nth.Suc [symmetric]
nth_sbintr
del: bin_nth.Suc)
+ apply force
apply (rule impI)
apply (rule_tac f = "bin_nth (uint w)" in arg_cong)
apply simp
done
lemma drop_shiftr:
- "drop n (to_bl ((w :: 'a :: finite word) >> n)) = take (size w - n) (to_bl w)"
+ "drop n (to_bl ((w :: 'a :: len word) >> n)) = take (size w - n) (to_bl w)"
apply (unfold shiftr_def)
apply (induct n)
prefer 2
@@ -273,7 +255,7 @@
done
lemma drop_sshiftr:
- "drop n (to_bl ((w :: 'a :: finite word) >>> n)) = take (size w - n) (to_bl w)"
+ "drop n (to_bl ((w :: 'a :: len word) >>> n)) = take (size w - n) (to_bl w)"
apply (unfold sshiftr_def)
apply (induct n)
prefer 2
@@ -283,7 +265,7 @@
done
lemma take_shiftr [rule_format] :
- "n <= size (w :: 'a :: finite word) --> take n (to_bl (w >> n)) =
+ "n <= size (w :: 'a :: len word) --> take n (to_bl (w >> n)) =
replicate n False"
apply (unfold shiftr_def)
apply (induct n)
@@ -295,7 +277,7 @@
done
lemma take_sshiftr' [rule_format] :
- "n <= size (w :: 'a :: finite word) --> hd (to_bl (w >>> n)) = hd (to_bl w) &
+ "n <= size (w :: 'a :: len word) --> hd (to_bl (w >>> n)) = hd (to_bl w) &
take n (to_bl (w >>> n)) = replicate n (hd (to_bl w))"
apply (unfold sshiftr_def)
apply (induct n)
@@ -320,7 +302,7 @@
by (induct n) (auto simp: shiftl1_of_bl replicate_app_Cons_same)
lemmas shiftl_bl =
- shiftl_of_bl [where bl = "to_bl (?w :: ?'a word)", simplified]
+ shiftl_of_bl [where bl = "to_bl (?w :: ?'a :: len0 word)", simplified]
lemmas shiftl_number [simp] = shiftl_def [where w="number_of ?w"]
@@ -329,46 +311,46 @@
by (simp add: shiftl_bl word_rep_drop word_size min_def)
lemma shiftl_zero_size:
- fixes x :: "'a word"
+ fixes x :: "'a::len0 word"
shows "size x <= n ==> x << n = 0"
apply (unfold word_size)
apply (rule word_eqI)
apply (clarsimp simp add: shiftl_bl word_size test_bit_of_bl nth_append)
done
-(* note - the following results use 'a :: finite word < number_ring *)
+(* note - the following results use 'a :: len word < number_ring *)
-lemma shiftl1_2t: "shiftl1 (w :: 'a :: finite word) = 2 * w"
+lemma shiftl1_2t: "shiftl1 (w :: 'a :: len word) = 2 * w"
apply (simp add: shiftl1_def_u)
apply (simp only: double_number_of_BIT [symmetric])
apply simp
done
-lemma shiftl1_p: "shiftl1 (w :: 'a :: finite word) = w + w"
+lemma shiftl1_p: "shiftl1 (w :: 'a :: len word) = w + w"
apply (simp add: shiftl1_def_u)
apply (simp only: double_number_of_BIT [symmetric])
apply simp
done
-lemma shiftl_t2n: "shiftl (w :: 'a :: finite word) n = 2 ^ n * w"
+lemma shiftl_t2n: "shiftl (w :: 'a :: len word) n = 2 ^ n * w"
unfolding shiftl_def
by (induct n) (auto simp: shiftl1_2t power_Suc)
lemma shiftr1_bintr [simp]:
- "(shiftr1 (number_of w) :: 'a word) =
- number_of (bin_rest (bintrunc CARD('a) w))"
+ "(shiftr1 (number_of w) :: 'a :: len0 word) =
+ number_of (bin_rest (bintrunc (len_of TYPE ('a)) w))"
unfolding shiftr1_def word_number_of_def
by (simp add : word_ubin.eq_norm)
lemma sshiftr1_sbintr [simp] :
- "(sshiftr1 (number_of w) :: 'a :: finite word) =
- number_of (bin_rest (sbintrunc (CARD('a) - 1) w))"
+ "(sshiftr1 (number_of w) :: 'a :: len word) =
+ number_of (bin_rest (sbintrunc (len_of TYPE ('a) - 1) w))"
unfolding sshiftr1_def word_number_of_def
by (simp add : word_sbin.eq_norm)
lemma shiftr_no':
"w = number_of bin ==>
- (w::'a word) >> n = number_of ((bin_rest ^ n) (bintrunc (size w) bin))"
+ (w::'a::len0 word) >> n = number_of ((bin_rest ^ n) (bintrunc (size w) bin))"
apply clarsimp
apply (rule word_eqI)
apply (auto simp: nth_shiftr nth_rest_power_bin nth_bintr word_size)
@@ -380,7 +362,7 @@
apply clarsimp
apply (rule word_eqI)
apply (auto simp: nth_sshiftr nth_rest_power_bin nth_sbintr word_size)
- apply (subgoal_tac "na + n = CARD('a) - Suc 0", simp, simp)+
+ apply (subgoal_tac "na + n = len_of TYPE('a) - Suc 0", simp, simp)+
done
lemmas sshiftr_no [simp] =
@@ -416,7 +398,7 @@
lemmas shiftr_bl = word_bl.Rep' [THEN eq_imp_le, THEN shiftr_bl_of,
simplified word_size, simplified, THEN eq_reflection, standard]
-lemma msb_shift': "msb (w::'a::finite word) <-> (w >> (size w - 1)) ~= 0"
+lemma msb_shift': "msb (w::'a::len word) <-> (w >> (size w - 1)) ~= 0"
apply (unfold shiftr_bl word_msb_alt)
apply (simp add: word_size Suc_le_eq take_Suc)
apply (cases "hd (to_bl w)")
@@ -476,10 +458,6 @@
subsubsection "Mask"
-definition
- mask :: "nat => 'a::finite word" where
- "mask n == (1 << n) - 1"
-
lemma nth_mask': "m = mask n ==> test_bit m i = (i < n & i < size m)"
apply (unfold mask_def test_bit_bl)
apply (simp only: word_1_bl [symmetric] shiftl_of_bl)
@@ -511,9 +489,9 @@
lemmas and_mask_wi = and_mask_no [unfolded word_number_of_def]
lemma bl_and_mask:
- "to_bl (w AND mask n :: 'a :: finite word) =
- replicate (CARD('a) - n) False @
- drop (CARD('a) - n) (to_bl w)"
+ "to_bl (w AND mask n :: 'a :: len word) =
+ replicate (len_of TYPE('a) - n) False @
+ drop (len_of TYPE('a) - n) (to_bl w)"
apply (rule nth_equalityI)
apply simp
apply (clarsimp simp add: to_bl_nth word_size)
@@ -560,14 +538,14 @@
done
lemma word_2p_lem:
- "n < size w ==> w < 2 ^ n = (uint (w :: 'a :: finite word) < 2 ^ n)"
+ "n < size w ==> w < 2 ^ n = (uint (w :: 'a :: len word) < 2 ^ n)"
apply (unfold word_size word_less_alt word_number_of_alt)
apply (clarsimp simp add: word_of_int_power_hom word_uint.eq_norm
int_mod_eq'
simp del: word_of_int_bin)
done
-lemma less_mask_eq: "x < 2 ^ n ==> x AND mask n = (x :: 'a :: finite word)"
+lemma less_mask_eq: "x < 2 ^ n ==> x AND mask n = (x :: 'a :: len word)"
apply (unfold word_less_alt word_number_of_alt)
apply (clarsimp simp add: and_mask_mod_2p word_of_int_power_hom
word_uint.eq_norm
@@ -587,7 +565,7 @@
unfolding word_size by (erule and_mask_less')
lemma word_mod_2p_is_mask':
- "c = 2 ^ n ==> c > 0 ==> x mod c = (x :: 'a :: finite word) AND mask n"
+ "c = 2 ^ n ==> c > 0 ==> x mod c = (x :: 'a :: len word) AND mask n"
by (clarsimp simp add: word_mod_def uint_2p and_mask_mod_2p)
lemmas word_mod_2p_is_mask = refl [THEN word_mod_2p_is_mask']
@@ -616,18 +594,14 @@
subsubsection "Revcast"
-definition
- revcast :: "'a word => 'b word" where
- "revcast w == of_bl (takefill False CARD('b) (to_bl w))"
-
lemmas revcast_def' = revcast_def [simplified]
lemmas revcast_def'' = revcast_def' [simplified word_size]
lemmas revcast_no_def [simp] =
revcast_def' [where w="number_of ?w", unfolded word_size]
lemma to_bl_revcast:
- "to_bl (revcast w :: 'a word) =
- takefill False CARD('a) (to_bl w)"
+ "to_bl (revcast w :: 'a :: len0 word) =
+ takefill False (len_of TYPE ('a)) (to_bl w)"
apply (unfold revcast_def' word_size)
apply (rule word_bl.Abs_inverse)
apply simp
@@ -656,7 +630,7 @@
lemma revcast_down_uu':
"rc = revcast ==> source_size rc = target_size rc + n ==>
- rc (w :: 'a :: finite word) = ucast (w >> n)"
+ rc (w :: 'a :: len word) = ucast (w >> n)"
apply (simp add: revcast_def')
apply (rule word_bl.Rep_inverse')
apply (rule trans, rule ucast_down_drop)
@@ -667,7 +641,7 @@
lemma revcast_down_us':
"rc = revcast ==> source_size rc = target_size rc + n ==>
- rc (w :: 'a :: finite word) = ucast (w >>> n)"
+ rc (w :: 'a :: len word) = ucast (w >>> n)"
apply (simp add: revcast_def')
apply (rule word_bl.Rep_inverse')
apply (rule trans, rule ucast_down_drop)
@@ -678,7 +652,7 @@
lemma revcast_down_su':
"rc = revcast ==> source_size rc = target_size rc + n ==>
- rc (w :: 'a :: finite word) = scast (w >> n)"
+ rc (w :: 'a :: len word) = scast (w >> n)"
apply (simp add: revcast_def')
apply (rule word_bl.Rep_inverse')
apply (rule trans, rule scast_down_drop)
@@ -689,7 +663,7 @@
lemma revcast_down_ss':
"rc = revcast ==> source_size rc = target_size rc + n ==>
- rc (w :: 'a :: finite word) = scast (w >>> n)"
+ rc (w :: 'a :: len word) = scast (w >>> n)"
apply (simp add: revcast_def')
apply (rule word_bl.Rep_inverse')
apply (rule trans, rule scast_down_drop)
@@ -705,7 +679,7 @@
lemma cast_down_rev:
"uc = ucast ==> source_size uc = target_size uc + n ==>
- uc w = revcast ((w :: 'a :: finite word) << n)"
+ uc w = revcast ((w :: 'a :: len word) << n)"
apply (unfold shiftl_rev)
apply clarify
apply (simp add: revcast_rev_ucast)
@@ -717,7 +691,7 @@
lemma revcast_up':
"rc = revcast ==> source_size rc + n = target_size rc ==>
- rc w = (ucast w :: 'a :: finite word) << n"
+ rc w = (ucast w :: 'a :: len word) << n"
apply (simp add: revcast_def')
apply (rule word_bl.Rep_inverse')
apply (simp add: takefill_alt)
@@ -743,16 +717,6 @@
subsubsection "Slices"
-definition
- slice1 :: "nat => 'a word => 'b word" where
- "slice1 n w == of_bl (takefill False n (to_bl w))"
-
-definition
- slice :: "nat => 'a word => 'b word" where
- "slice n w == slice1 (size w - n) w"
-
-lemmas slice_def' = slice_def [unfolded word_size]
-
lemmas slice1_no_bin [simp] =
slice1_def [where w="number_of ?w", unfolded to_bl_no_bin]
@@ -785,8 +749,8 @@
done
lemma nth_slice:
- "(slice n w :: 'a word) !! m =
- (w !! (m + n) & m < CARD('a))"
+ "(slice n w :: 'a :: len0 word) !! m =
+ (w !! (m + n) & m < len_of TYPE ('a))"
unfolding slice_shiftr
by (simp add : nth_ucast nth_shiftr)
@@ -802,8 +766,8 @@
apply (unfold slice1_def word_size of_bl_def uint_bl)
apply (clarsimp simp: word_ubin.eq_norm bl_bin_bl_rep_drop
takefill_append [symmetric])
- apply (rule_tac f = "%k. takefill False CARD('a)
- (replicate k False @ bin_to_bl CARD('b) (uint w))" in arg_cong)
+ apply (rule_tac f = "%k. takefill False (len_of TYPE('a))
+ (replicate k False @ bin_to_bl (len_of TYPE('b)) (uint w))" in arg_cong)
apply arith
done
@@ -830,17 +794,17 @@
lemmas revcast_slice1 = refl [THEN revcast_slice1']
lemma slice1_tf_tf':
- "to_bl (slice1 n w :: 'a word) =
- rev (takefill False CARD('a) (rev (takefill False n (to_bl w))))"
+ "to_bl (slice1 n w :: 'a :: len0 word) =
+ rev (takefill False (len_of TYPE('a)) (rev (takefill False n (to_bl w))))"
unfolding slice1_def by (rule word_rev_tf)
lemmas slice1_tf_tf = slice1_tf_tf'
[THEN word_bl.Rep_inverse', symmetric, standard]
lemma rev_slice1:
- "n + k = CARD('a) + CARD('b) \<Longrightarrow>
- slice1 n (word_reverse w :: 'b word) =
- word_reverse (slice1 k w :: 'a word)"
+ "n + k = len_of TYPE('a) + len_of TYPE('b) \<Longrightarrow>
+ slice1 n (word_reverse w :: 'b :: len0 word) =
+ word_reverse (slice1 k w :: 'a :: len0 word)"
apply (unfold word_reverse_def slice1_tf_tf)
apply (rule word_bl.Rep_inverse')
apply (rule rev_swap [THEN iffD1])
@@ -868,10 +832,10 @@
criterion for overflow of addition of signed integers *}
lemma sofl_test:
- "(sint (x :: 'a :: finite word) + sint y = sint (x + y)) =
+ "(sint (x :: 'a :: len word) + sint y = sint (x + y)) =
((((x+y) XOR x) AND ((x+y) XOR y)) >> (size x - 1) = 0)"
apply (unfold word_size)
- apply (cases "CARD('a)", simp)
+ apply (cases "len_of TYPE('a)", simp)
apply (subst msb_shift [THEN sym_notr])
apply (simp add: word_ops_msb)
apply (simp add: word_msb_sint)
@@ -898,30 +862,13 @@
subsection "Split and cat"
-constdefs
- word_cat :: "'a word => 'b word => 'c word"
- "word_cat a b == word_of_int (bin_cat (uint a) CARD('b) (uint b))"
-
- word_split :: "'a word => ('b word) * ('c word)"
- "word_split a ==
- case bin_split CARD('c) (uint a) of
- (u, v) => (word_of_int u, word_of_int v)"
-
- word_rcat :: "'a word list => 'b word"
- "word_rcat ws ==
- word_of_int (bin_rcat CARD('a) (map uint ws))"
-
- word_rsplit :: "'a word => 'b :: finite word list"
- "word_rsplit w ==
- map word_of_int (bin_rsplit CARD('b) (CARD('a), uint w))"
-
lemmas word_split_bin' = word_split_def [THEN meta_eq_to_obj_eq, standard]
lemmas word_cat_bin' = word_cat_def [THEN meta_eq_to_obj_eq, standard]
lemma word_rsplit_no:
- "(word_rsplit (number_of bin :: 'b word) :: 'a word list) =
- map number_of (bin_rsplit CARD('a :: finite)
- (CARD('b), bintrunc CARD('b) bin))"
+ "(word_rsplit (number_of bin :: 'b :: len0 word) :: 'a word list) =
+ map number_of (bin_rsplit (len_of TYPE('a :: len))
+ (len_of TYPE('b), bintrunc (len_of TYPE('b)) bin))"
apply (unfold word_rsplit_def word_no_wi)
apply (simp add: word_ubin.eq_norm)
done
@@ -943,7 +890,7 @@
done
lemma of_bl_append:
- "(of_bl (xs @ ys) :: 'a :: finite word) = of_bl xs * 2^(length ys) + of_bl ys"
+ "(of_bl (xs @ ys) :: 'a :: len word) = of_bl xs * 2^(length ys) + of_bl ys"
apply (unfold of_bl_def)
apply (simp add: bl_to_bin_app_cat bin_cat_num)
apply (simp add: word_of_int_power_hom [symmetric] new_word_of_int_hom_syms)
@@ -955,7 +902,7 @@
(auto simp add: test_bit_of_bl nth_append)
lemma of_bl_True:
- "(of_bl (True#xs)::'a::finite word) = 2^length xs + of_bl xs"
+ "(of_bl (True#xs)::'a::len word) = 2^length xs + of_bl xs"
by (subst of_bl_append [where xs="[True]", simplified])
(simp add: word_1_bl)
@@ -963,8 +910,8 @@
"of_bl (x#xs) = of_bool x * 2^length xs + of_bl xs"
by (cases x) (simp_all add: of_bl_True)
-lemma split_uint_lem: "bin_split n (uint (w :: 'a word)) = (a, b) ==>
- a = bintrunc (CARD('a) - n) a & b = bintrunc CARD('a) b"
+lemma split_uint_lem: "bin_split n (uint (w :: 'a :: len0 word)) = (a, b) ==>
+ a = bintrunc (len_of TYPE('a) - n) a & b = bintrunc (len_of TYPE('a)) b"
apply (frule word_ubin.norm_Rep [THEN ssubst])
apply (drule bin_split_trunc1)
apply (drule sym [THEN trans])
@@ -986,7 +933,7 @@
apply (clarsimp split: prod.splits)
apply (frule split_uint_lem [THEN conjunct1])
apply (unfold word_size)
- apply (cases "CARD('a) >= CARD('b)")
+ apply (cases "len_of TYPE('a) >= len_of TYPE('b)")
defer
apply (simp add: word_0_bl word_0_wi_Pls)
apply (simp add : of_bl_def to_bl_def)
@@ -1012,9 +959,9 @@
done
lemma word_split_bl_eq:
- "(word_split (c::'a::finite word) :: ('c word * 'd word)) =
- (of_bl (take (CARD('a::finite) - CARD('d)) (to_bl c)),
- of_bl (drop (CARD('a) - CARD('d)) (to_bl c)))"
+ "(word_split (c::'a::len word) :: ('c :: len0 word * 'd :: len0 word)) =
+ (of_bl (take (len_of TYPE('a::len) - len_of TYPE('d::len0)) (to_bl c)),
+ of_bl (drop (len_of TYPE('a) - len_of TYPE('d)) (to_bl c)))"
apply (rule word_split_bl [THEN iffD1])
apply (unfold word_size)
apply (rule refl conjI)+
@@ -1057,13 +1004,14 @@
-- "limited hom result"
lemma word_cat_hom:
- "CARD('a) <= CARD('b) + CARD('c)
+ "len_of TYPE('a::len0) <= len_of TYPE('b::len0) + len_of TYPE ('c::len0)
==>
(word_cat (word_of_int w :: 'b word) (b :: 'c word) :: 'a word) =
word_of_int (bin_cat w (size b) (uint b))"
apply (unfold word_cat_def word_size)
apply (clarsimp simp add : word_ubin.norm_eq_iff [symmetric]
word_ubin.eq_norm bintr_cat min_def)
+ apply arith
done
lemma word_cat_split_alt:
@@ -1138,7 +1086,7 @@
by (simp add: bin_rsplit_aux_simp_alt Let_def split: split_split)
lemma test_bit_rsplit:
- "sw = word_rsplit w ==> m < size (hd sw :: 'a :: finite word) ==>
+ "sw = word_rsplit w ==> m < size (hd sw :: 'a :: len word) ==>
k < length sw ==> (rev sw ! k) !! m = (w !! (k * size (hd sw) + m))"
apply (unfold word_rsplit_def word_test_bit_def)
apply (rule trans)
@@ -1153,7 +1101,7 @@
apply (rule map_ident [THEN fun_cong])
apply (rule refl [THEN map_cong])
apply (simp add : word_ubin.eq_norm)
- apply (erule bin_rsplit_size_sign [OF zero_less_card_finite refl])
+ apply (erule bin_rsplit_size_sign [OF len_gt_0 refl])
done
lemma word_rcat_bl: "word_rcat wl == of_bl (concat (map to_bl wl))"
@@ -1166,10 +1114,10 @@
lemmas size_rcat_lem = size_rcat_lem' [unfolded word_size]
-lemmas td_gal_lt_len = zero_less_card_finite [THEN td_gal_lt, standard]
+lemmas td_gal_lt_len = len_gt_0 [THEN td_gal_lt, standard]
lemma nth_rcat_lem' [rule_format] :
- "sw = size (hd wl :: 'a :: finite word) ==> (ALL n. n < size wl * sw -->
+ "sw = size (hd wl :: 'a :: len word) ==> (ALL n. n < size wl * sw -->
rev (concat (map to_bl wl)) ! n =
rev (to_bl (rev wl ! (n div sw))) ! (n mod sw))"
apply (unfold word_size)
@@ -1184,7 +1132,7 @@
lemmas nth_rcat_lem = refl [THEN nth_rcat_lem', unfolded word_size]
lemma test_bit_rcat:
- "sw = size (hd wl :: 'a :: finite word) ==> rc = word_rcat wl ==> rc !! n =
+ "sw = size (hd wl :: 'a :: len word) ==> rc = word_rcat wl ==> rc !! n =
(n < size rc & n div sw < size wl & (rev wl) ! (n div sw) !! (n mod sw))"
apply (unfold word_rcat_bl word_size)
apply (clarsimp simp add :
@@ -1215,7 +1163,7 @@
lemmas word_rsplit_len_indep = word_rsplit_len_indep' [OF refl refl refl refl]
lemma length_word_rsplit_size:
- "n = CARD('a :: finite) ==>
+ "n = len_of TYPE ('a :: len) ==>
(length (word_rsplit w :: 'a word list) <= m) = (size w <= m * n)"
apply (unfold word_rsplit_def word_size)
apply (clarsimp simp add : bin_rsplit_len_le)
@@ -1225,12 +1173,12 @@
length_word_rsplit_size [unfolded Not_eq_iff linorder_not_less [symmetric]]
lemma length_word_rsplit_exp_size:
- "n = CARD('a :: finite) ==>
+ "n = len_of TYPE ('a :: len) ==>
length (word_rsplit w :: 'a word list) = (size w + n - 1) div n"
unfolding word_rsplit_def by (clarsimp simp add : word_size bin_rsplit_len)
lemma length_word_rsplit_even_size:
- "n = CARD('a :: finite) ==> size w = m * n ==>
+ "n = len_of TYPE ('a :: len) ==> size w = m * n ==>
length (word_rsplit w :: 'a word list) = m"
by (clarsimp simp add : length_word_rsplit_exp_size given_quot_alt)
@@ -1247,15 +1195,15 @@
apply (simp_all add: word_size
refl [THEN length_word_rsplit_size [simplified le_def, simplified]])
apply safe
- apply (erule xtr7, rule zero_less_card_finite [THEN dtle])+
+ apply (erule xtr7, rule len_gt_0 [THEN dtle])+
done
lemma size_word_rsplit_rcat_size':
- "word_rcat (ws :: 'a :: finite word list) = frcw ==>
- size frcw = length ws * CARD('a) ==>
+ "word_rcat (ws :: 'a :: len word list) = frcw ==>
+ size frcw = length ws * len_of TYPE ('a) ==>
size (hd [word_rsplit frcw, ws]) = size ws"
apply (clarsimp simp add : word_size length_word_rsplit_exp_size')
- apply (fast intro: given_quot_alt zero_less_card_finite)
+ apply (fast intro: given_quot_alt)
done
lemmas size_word_rsplit_rcat_size =
@@ -1268,8 +1216,8 @@
by (auto simp: add_commute)
lemma word_rsplit_rcat_size':
- "word_rcat (ws :: 'a :: finite word list) = frcw ==>
- size frcw = length ws * CARD('a) ==> word_rsplit frcw = ws"
+ "word_rcat (ws :: 'a :: len word list) = frcw ==>
+ size frcw = length ws * len_of TYPE ('a) ==> word_rsplit frcw = ws"
apply (frule size_word_rsplit_rcat_size, assumption)
apply (clarsimp simp add : word_size)
apply (rule nth_equalityI, assumption)
@@ -1296,24 +1244,6 @@
subsection "Rotation"
-constdefs
- rotater1 :: "'a list => 'a list"
- "rotater1 ys ==
- case ys of [] => [] | x # xs => last ys # butlast ys"
-
- rotater :: "nat => 'a list => 'a list"
- "rotater n == rotater1 ^ n"
-
- word_rotr :: "nat => 'a word => 'a word"
- "word_rotr n w == of_bl (rotater n (to_bl w))"
-
- word_rotl :: "nat => 'a word => 'a word"
- "word_rotl n w == of_bl (rotate n (to_bl w))"
-
- word_roti :: "int => 'a word => 'a word"
- "word_roti i w == if i >= 0 then word_rotr (nat i) w
- else word_rotl (nat (- i)) w"
-
lemmas rotater_0' [simp] = rotater_def [where n = "0", simplified]
lemmas word_rot_defs = word_roti_def word_rotr_def word_rotl_def
@@ -1628,7 +1558,7 @@
simplified word_bl.Rep', standard]
lemma bl_word_roti_dt':
- "n = nat ((- i) mod int (size (w :: 'a :: finite word))) ==>
+ "n = nat ((- i) mod int (size (w :: 'a :: len word))) ==>
to_bl (word_roti i w) = drop n (to_bl w) @ take n (to_bl w)"
apply (unfold word_roti_def)
apply (simp add: bl_word_rotl_dt bl_word_rotr_dt word_size)