# HG changeset patch # User huffman # Date 1188324827 -7200 # Node ID 70f0214b3ecce812b4167e477762747486a6217d # Parent 58d24cbe5fa6c7468754b1bf37a1baa8cc8a88f4 revert to Word library version from 2007/08/20 diff -r 58d24cbe5fa6 -r 70f0214b3ecc src/HOL/IsaMakefile --- 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 diff -r 58d24cbe5fa6 -r 70f0214b3ecc src/HOL/Word/BinBoolList.thy --- 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 \ n = 0 diff -r 58d24cbe5fa6 -r 70f0214b3ecc src/HOL/Word/BinGeneral.thy --- 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 \ bit.B1" - assumes y: "y = bit.B0 \ P" - shows "P" - apply (rule y) - apply (cases y rule: bit.exhaust, simp) - apply (simp add: ne) - done - -lemma bin_exhaust: - assumes Q: "\x b. bin = x BIT b \ 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" diff -r 58d24cbe5fa6 -r 70f0214b3ecc src/HOL/Word/BinInduct.thy --- 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 \ x = y \ 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 \ a = b)" - by (safe dest!: BIT_eq) - -lemma BIT_eq_Pls: "(w BIT b = Numeral.Pls) = (w = Numeral.Pls \ 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 \ 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 \ b = bit.B0)" - by (subst eq_commute, rule BIT_eq_Pls) - -lemma Min_eq_BIT: "(Numeral.Min = w BIT b) = (w = Numeral.Min \ b = bit.B1)" - by (subst eq_commute, rule BIT_eq_Min) - -lemma Min_neq_Pls: "Numeral.Min \ Numeral.Pls" - unfolding Min_def Pls_def by simp - -lemma Pls_neq_Min: "Numeral.Pls \ 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 \ bool" -where - Pls: "is_numeral Numeral.Pls" -| Min: "is_numeral Numeral.Min" -| B0: "is_numeral z \ is_numeral (z BIT bit.B0)" -| B1: "is_numeral z \ is_numeral (z BIT bit.B1)" - -lemma is_numeral_succ: "is_numeral z \ is_numeral (Numeral.succ z)" - by (erule is_numeral.induct, simp_all add: is_numeral.intros) - -lemma is_numeral_pred: "is_numeral z \ is_numeral (Numeral.pred z)" - by (erule is_numeral.induct, simp_all add: is_numeral.intros) - -lemma is_numeral_uminus: "is_numeral z \ 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: "\x. \P x; x \ Numeral.Pls\ \ P (x BIT bit.B0)" - assumes B1: "\x. \P x; x \ Numeral.Min\ \ 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 \ P (z BIT bit.B0)" - by (cases "z = Numeral.Pls", auto intro: Pls B0) - show "P z \ 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: "\bin bit. P bin \ P (bin BIT bit)" - shows "P x" - by (induct x rule: int_bin_induct) (auto intro: assms) - -lemma BIT_exhausts: "\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: "(\w b. x = w BIT b \ Q) \ Q" - by (insert BIT_exhausts [of x], auto) - - -subsection {* Destructors for BIT *} - -definition - bin_rest :: "int \ int" where - "bin_rest x = (THE w. \b. x = w BIT b)" - -definition - bin_last :: "int \ bit" where - "bin_last x = (THE b. \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 \ Numeral.Pls \ w \ 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 \ nat" -where - "binsize z = (if z = Numeral.Pls \ 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 \ Numeral.Pls \ w \ Numeral.Min}") - apply (rule wf_bin_rest) - apply simp - done - -instance int :: size - int_size_def: "size \ 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 \ Numeral.Pls \ w \ Numeral.Min)" - by (induct w rule: int_bin_induct) simp_all - -end diff -r 58d24cbe5fa6 -r 70f0214b3ecc src/HOL/Word/BinOperations.thy --- 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" diff -r 58d24cbe5fa6 -r 70f0214b3ecc src/HOL/Word/Examples/WordExamples.thy --- 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 \ 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 "\ lsb (0b1000::'a::finite word)" by simp +lemma "lsb (0b0101::'a::len word)" by simp +lemma "\ lsb (0b1000::'a::len word)" by simp lemma "\ 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 diff -r 58d24cbe5fa6 -r 70f0214b3ecc src/HOL/Word/Num_Lemmas.thy --- 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 \ 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 \ c - b) = (b + a \ (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 \ c) = (a \ 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 \ 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 \ bit.B1" + assumes y: "y = bit.B0 \ 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: "\x b. bin = x BIT b \ 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 \ c ==> (w + 1) * c \ 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) \ j \ 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 diff -r 58d24cbe5fa6 -r 70f0214b3ecc src/HOL/Word/Size.thy --- /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 + diff -r 58d24cbe5fa6 -r 70f0214b3ecc src/HOL/Word/WordArith.thy --- 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 \ 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 @@ "\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" ("(_/ 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 \ 'a word \ bool" (infixl "udvd" 50) where - "a udvd b \ \n\0. uint b = n * uint a" - -lemma udvdI: - "0 \ 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 \ y + x) = (uint y + uint x < 2 ^ CARD('a))" - by (simp add: add_ac no_olen_add) + fixes x :: "'a::len0 word" + shows "(x \ 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 \ rev (to_bl (word_succ w)) = rbl_succ ys" + + "rev (to_bl w) = ys \ 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) = (\q. n = unat w + q * 2 ^ CARD('a))" + fixes w :: "'a::len word" + shows "(of_nat n = w) = (\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)) = (\q. m = q * 2 ^ CARD('a))" + "(of_nat m = (0::'a::len word)) = (\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 diff -r 58d24cbe5fa6 -r 70f0214b3ecc src/HOL/Word/WordBitwise.thy --- 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. \i. f i \ i < len_of TYPE('a::len0)}" + "(\h i. h i \ 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 \ CARD('a)" + fixes w :: "'a::len word" + defines "l \ 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 diff -r 58d24cbe5fa6 -r 70f0214b3ecc src/HOL/Word/WordBoolList.thy --- 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 \ 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 \ n < CARD('a) \ 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 \ rev (to_bl (word_succ w)) = rbl_succ ys" - - "rev (to_bl w) = ys \ 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. \i. f i \ i < CARD('a)}" - "(\h i. h i \ 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 diff -r 58d24cbe5fa6 -r 70f0214b3ecc src/HOL/Word/WordDefinition.thy --- 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 \ '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 \ Abs_word' 0" - word_one_def: "1 \ Abs_word' 1" - word_add_def: "x + y \ Abs_word' (Rep_word x + Rep_word y)" - word_mult_def: "x * y \ Abs_word' (Rep_word x * Rep_word y)" - word_diff_def: "x - y \ Abs_word' (Rep_word x - Rep_word y)" - word_minus_def: "- x \ Abs_word' (- Rep_word x)" - word_power_def: "x ^ n \ 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" ("(_/ 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 \ word_of_int (2^CARD('a) - 1)" + max_word :: "'a::len word" + "max_word \ word_of_int (2^len_of TYPE('a) - 1)" consts - of_bool :: "bool \ 'a::finite word" + of_bool :: "bool \ '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 \ i \ 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 \ int" + td_ext ["uint::'a::len0 word \ int" word_of_int - "uints CARD('a)" - "\w. w mod 2 ^ CARD('a)"] + "uints (len_of TYPE('a::len0))" + "\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 \ int" + td_ext ["uint::'a::len0 word \ 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 \ 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 \ n < len_of TYPE('a) \ 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 diff -r 58d24cbe5fa6 -r 70f0214b3ecc src/HOL/Word/WordGenLib.thy --- 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: - "\\n. \(x ::'a word) = word_of_int n; 0 \ n; n < 2^CARD('a)\ \ P\ + "\\n. \(x ::'a::len0 word) = word_of_int n; 0 \ n; n < 2^len_of TYPE('a)\ \ P\ \ P" by (cases x rule: word_uint.Abs_cases) (simp add: uints_num) lemma word_nat_cases [cases type: word]: - "\\n. \(x ::'a::finite word) = of_nat n; n < 2^CARD('a)\ \ P\ + "\\n. \(x ::'a::len word) = of_nat n; n < 2^len_of TYPE('a)\ \ P\ \ 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' \ CARD('a) - n" + defines "n' \ 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 & \ (to_bl (mask n::'a::finite word)) = + have "app2 op & \ (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 \ 0) = (0 < w)" proof - have "0 \ 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 \ 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 \ 0 ==> 1 \ x = (0 \ 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) \ y = (x = y \ x < y)" + "(x ::'z::len word) \ y = (x = y \ x < y)" by (auto simp add: word_less_def) lemma mod_plus_cong: @@ -312,7 +312,7 @@ done lemma word_induct_less: - "\P (0::'a::finite word); \n. \n < m; P n\ \ P (1 + n)\ \ P m" + "\P (0::'a::len word); \n. \n < m; P n\ \ P (1 + n)\ \ P m" apply (cases m) apply atomize apply (erule rev_mp)+ @@ -335,24 +335,24 @@ done lemma word_induct: - "\P (0::'a::finite word); \n. P n \ P (1 + n)\ \ P m" + "\P (0::'a::len word); \n. P n \ P (1 + n)\ \ P m" by (erule word_induct_less, simp) lemma word_induct2 [induct type]: - "\P 0; \n. \1 + n \ 0; P n\ \ P (1 + n)\ \ P (n::'b::finite word)" + "\P 0; \n. \1 + n \ 0; P n\ \ P (1 + n)\ \ P (n::'b::len word)" apply (rule word_induct, simp) apply (case_tac "1+n = 0", auto) done constdefs - word_rec :: "'a \ ('b::finite word \ 'a \ 'a) \ 'b word \ 'a" + word_rec :: "'a \ ('b::len word \ 'a \ 'a) \ 'b word \ 'a" "word_rec forZero forSuc n \ nat_rec forZero (forSuc \ 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 \ (0::'a::finite word) \ word_rec z s (1 + n) = s n (word_rec z s n)" + "1 + n \ (0::'a::len word) \ 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 \ (0::'a::finite word) \ unat (1 + n) = Suc (unat n)" + "1 + n \ (0::'a::len word) \ unat (1 + n) = Suc (unat n)" by unat_arith end diff -r 58d24cbe5fa6 -r 70f0214b3ecc src/HOL/Word/WordShift.thy --- 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: - "\n. ((w::'a word) >> m) !! n = w !! (n + m)" + "\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) \ - slice1 n (word_reverse w :: 'b word) = - word_reverse (slice1 k w :: 'a word)" + "n + k = len_of TYPE('a) + len_of TYPE('b) \ + 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)