--- a/src/HOL/Word/Bit_Int.thy Mon Dec 23 14:24:20 2013 +0100
+++ b/src/HOL/Word/Bit_Int.thy Mon Dec 23 14:24:21 2013 +0100
@@ -482,25 +482,30 @@
subsection {* Splitting and concatenation *}
-definition bin_rcat :: "nat \<Rightarrow> int list \<Rightarrow> int" where
+definition bin_rcat :: "nat \<Rightarrow> int list \<Rightarrow> int"
+where
"bin_rcat n = foldl (\<lambda>u v. bin_cat u n v) 0"
-fun bin_rsplit_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" where
+fun bin_rsplit_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list"
+where
"bin_rsplit_aux n m c bs =
(if m = 0 | n = 0 then bs else
let (a, b) = bin_split n c
in bin_rsplit_aux n (m - n) a (b # bs))"
-definition bin_rsplit :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list" where
+definition bin_rsplit :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list"
+where
"bin_rsplit n w = bin_rsplit_aux n (fst w) (snd w) []"
-fun bin_rsplitl_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" where
+fun bin_rsplitl_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list"
+where
"bin_rsplitl_aux n m c bs =
(if m = 0 | n = 0 then bs else
let (a, b) = bin_split (min m n) c
in bin_rsplitl_aux n (m - n) a (b # bs))"
-definition bin_rsplitl :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list" where
+definition bin_rsplitl :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list"
+where
"bin_rsplitl n w = bin_rsplitl_aux n (fst w) (snd w) []"
declare bin_rsplit_aux.simps [simp del]
--- a/src/HOL/Word/Bit_Representation.thy Mon Dec 23 14:24:20 2013 +0100
+++ b/src/HOL/Word/Bit_Representation.thy Mon Dec 23 14:24:21 2013 +0100
@@ -10,7 +10,8 @@
subsection {* Constructors and destructors for binary integers *}
-definition Bit :: "int \<Rightarrow> bool \<Rightarrow> int" (infixl "BIT" 90) where
+definition Bit :: "int \<Rightarrow> bool \<Rightarrow> int" (infixl "BIT" 90)
+where
"k BIT b = (if b then 1 else 0) + k + k"
lemma Bit_B0:
@@ -27,14 +28,16 @@
lemma Bit_B1_2t: "k BIT True = 2 * k + 1"
by (rule trans, rule Bit_B1) simp
-definition bin_last :: "int \<Rightarrow> bool" where
+definition bin_last :: "int \<Rightarrow> bool"
+where
"bin_last w \<longleftrightarrow> w mod 2 = 1"
lemma bin_last_odd:
"bin_last = odd"
by (rule ext) (simp add: bin_last_def even_def)
-definition bin_rest :: "int \<Rightarrow> int" where
+definition bin_rest :: "int \<Rightarrow> int"
+where
"bin_rest w = w div 2"
lemma bin_rl_simp [simp]:
@@ -271,7 +274,8 @@
subsection {* Truncating binary integers *}
-definition bin_sign :: "int \<Rightarrow> int" where
+definition bin_sign :: "int \<Rightarrow> int"
+where
bin_sign_def: "bin_sign k = (if k \<ge> 0 then 0 else - 1)"
lemma bin_sign_simps [simp]:
--- a/src/HOL/Word/Bool_List_Representation.thy Mon Dec 23 14:24:20 2013 +0100
+++ b/src/HOL/Word/Bool_List_Representation.thy Mon Dec 23 14:24:21 2013 +0100
@@ -31,27 +31,33 @@
subsection {* Operations on lists of booleans *}
-primrec bl_to_bin_aux :: "bool list \<Rightarrow> int \<Rightarrow> int" where
+primrec bl_to_bin_aux :: "bool list \<Rightarrow> int \<Rightarrow> int"
+where
Nil: "bl_to_bin_aux [] w = w"
| Cons: "bl_to_bin_aux (b # bs) w =
bl_to_bin_aux bs (w BIT b)"
-definition bl_to_bin :: "bool list \<Rightarrow> int" where
+definition bl_to_bin :: "bool list \<Rightarrow> int"
+where
bl_to_bin_def: "bl_to_bin bs = bl_to_bin_aux bs 0"
-primrec bin_to_bl_aux :: "nat \<Rightarrow> int \<Rightarrow> bool list \<Rightarrow> bool list" where
+primrec bin_to_bl_aux :: "nat \<Rightarrow> int \<Rightarrow> bool list \<Rightarrow> bool list"
+where
Z: "bin_to_bl_aux 0 w bl = bl"
| Suc: "bin_to_bl_aux (Suc n) w bl =
bin_to_bl_aux n (bin_rest w) ((bin_last w) # bl)"
-definition bin_to_bl :: "nat \<Rightarrow> int \<Rightarrow> bool list" where
+definition bin_to_bl :: "nat \<Rightarrow> int \<Rightarrow> bool list"
+where
bin_to_bl_def : "bin_to_bl n w = bin_to_bl_aux n w []"
-primrec bl_of_nth :: "nat \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool list" where
+primrec bl_of_nth :: "nat \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool list"
+where
Suc: "bl_of_nth (Suc n) f = f n # bl_of_nth n f"
| Z: "bl_of_nth 0 f = []"
-primrec takefill :: "'a \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+primrec takefill :: "'a \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
+where
Z: "takefill fill 0 xs = []"
| Suc: "takefill fill (Suc n) xs = (
case xs of [] => fill # takefill fill n xs
@@ -65,21 +71,25 @@
assuming input list(s) the same length, and don't extend them.
*}
-primrec rbl_succ :: "bool list => bool list" where
+primrec rbl_succ :: "bool list => bool list"
+where
Nil: "rbl_succ Nil = Nil"
| Cons: "rbl_succ (x # xs) = (if x then False # rbl_succ xs else True # xs)"
-primrec rbl_pred :: "bool list => bool list" where
+primrec rbl_pred :: "bool list => bool list"
+where
Nil: "rbl_pred Nil = Nil"
| Cons: "rbl_pred (x # xs) = (if x then False # xs else True # rbl_pred xs)"
-primrec rbl_add :: "bool list => bool list => bool list" where
+primrec rbl_add :: "bool list => bool list => bool list"
+where
-- "result is length of first arg, second arg may be longer"
Nil: "rbl_add Nil x = Nil"
| Cons: "rbl_add (y # ys) x = (let ws = rbl_add ys (tl x) in
(y ~= hd x) # (if hd x & y then rbl_succ ws else ws))"
-primrec rbl_mult :: "bool list => bool list => bool list" where
+primrec rbl_mult :: "bool list => bool list => bool list"
+where
-- "result is length of first arg, second arg may be longer"
Nil: "rbl_mult Nil x = Nil"
| Cons: "rbl_mult (y # ys) x = (let ws = False # rbl_mult ys x in
--- a/src/HOL/Word/Word.thy Mon Dec 23 14:24:20 2013 +0100
+++ b/src/HOL/Word/Word.thy Mon Dec 23 14:24:21 2013 +0100
@@ -35,7 +35,8 @@
shows "uint w mod 2 ^ len_of TYPE('a) = uint w"
using uint_nonnegative uint_bounded by (rule mod_pos_pos_trivial)
-definition word_of_int :: "int \<Rightarrow> 'a\<Colon>len0 word" where
+definition word_of_int :: "int \<Rightarrow> 'a\<Colon>len0 word"
+where
-- {* representation of words using unsigned or signed bins,
only difference in these is the type class *}
"word_of_int k = Abs_word (k mod 2 ^ len_of TYPE('a))"
@@ -72,7 +73,8 @@
instantiation word :: (len0) equal
begin
-definition equal_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool" where
+definition equal_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool"
+where
"equal_word k l \<longleftrightarrow> HOL.equal (uint k) (uint l)"
instance proof
@@ -101,31 +103,39 @@
subsection {* Type conversions and casting *}
-definition sint :: "'a :: len word => int" where
+definition sint :: "'a :: len word => int"
+where
-- {* treats the most-significant-bit as a sign bit *}
sint_uint: "sint w = sbintrunc (len_of TYPE ('a) - 1) (uint w)"
-definition unat :: "'a :: len0 word => nat" where
+definition unat :: "'a :: len0 word => nat"
+where
"unat w = nat (uint w)"
-definition uints :: "nat => int set" where
+definition uints :: "nat => int set"
+where
-- "the sets of integers representing the words"
"uints n = range (bintrunc n)"
-definition sints :: "nat => int set" where
+definition sints :: "nat => int set"
+where
"sints n = range (sbintrunc (n - 1))"
-definition unats :: "nat => nat set" where
+definition unats :: "nat => nat set"
+where
"unats n = {i. i < 2 ^ n}"
-definition norm_sint :: "nat => int => int" where
+definition norm_sint :: "nat => int => int"
+where
"norm_sint n w = (w + 2 ^ (n - 1)) mod 2 ^ n - 2 ^ (n - 1)"
-definition scast :: "'a :: len word => 'b :: len word" where
+definition scast :: "'a :: len word => 'b :: len word"
+where
-- "cast a word to a different length"
"scast w = word_of_int (sint w)"
-definition ucast :: "'a :: len0 word => 'b :: len0 word" where
+definition ucast :: "'a :: len0 word => 'b :: len0 word"
+where
"ucast w = word_of_int (uint w)"
instantiation word :: (len0) size
@@ -138,29 +148,37 @@
end
-definition source_size :: "('a :: len0 word => 'b) => nat" where
+definition source_size :: "('a :: len0 word => 'b) => nat"
+where
-- "whether a cast (or other) function is to a longer or shorter length"
"source_size c = (let arb = undefined ; x = c arb in size arb)"
-definition target_size :: "('a => 'b :: len0 word) => nat" where
+definition target_size :: "('a => 'b :: len0 word) => nat"
+where
"target_size c = size (c undefined)"
-definition is_up :: "('a :: len0 word => 'b :: len0 word) => bool" where
+definition is_up :: "('a :: len0 word => 'b :: len0 word) => bool"
+where
"is_up c \<longleftrightarrow> source_size c <= target_size c"
-definition is_down :: "('a :: len0 word => 'b :: len0 word) => bool" where
+definition is_down :: "('a :: len0 word => 'b :: len0 word) => bool"
+where
"is_down c \<longleftrightarrow> target_size c <= source_size c"
-definition of_bl :: "bool list => 'a :: len0 word" where
+definition of_bl :: "bool list => 'a :: len0 word"
+where
"of_bl bl = word_of_int (bl_to_bin bl)"
-definition to_bl :: "'a :: len0 word => bool list" where
+definition to_bl :: "'a :: len0 word => bool list"
+where
"to_bl w = bin_to_bl (len_of TYPE ('a)) (uint w)"
-definition word_reverse :: "'a :: len0 word => 'a word" where
+definition word_reverse :: "'a :: len0 word => 'a word"
+where
"word_reverse w = of_bl (rev (to_bl w))"
-definition word_int_case :: "(int => 'b) => ('a :: len0 word) => 'b" where
+definition word_int_case :: "(int => 'b) => ('a :: len0 word) => 'b"
+where
"word_int_case f w = f (uint w)"
translations
@@ -232,7 +250,8 @@
subsection {* Correspondence relation for theorem transfer *}
definition cr_word :: "int \<Rightarrow> 'a::len0 word \<Rightarrow> bool"
- where "cr_word \<equiv> (\<lambda>x y. word_of_int x = y)"
+where
+ "cr_word = (\<lambda>x y. word_of_int x = y)"
lemma Quotient_word:
"Quotient (\<lambda>x y. bintrunc (len_of TYPE('a)) x = bintrunc (len_of TYPE('a)) y)
@@ -341,7 +360,8 @@
apply (simp add: word_of_nat wi_hom_sub)
done
-definition udvd :: "'a::len word => 'a::len word => bool" (infixl "udvd" 50) where
+definition udvd :: "'a::len word => 'a::len word => bool" (infixl "udvd" 50)
+where
"a udvd b = (EX n>=0. uint b = n * uint a)"
@@ -361,10 +381,12 @@
end
-definition word_sle :: "'a :: len word => 'a word => bool" ("(_/ <=s _)" [50, 51] 50) where
+definition word_sle :: "'a :: len word => 'a word => bool" ("(_/ <=s _)" [50, 51] 50)
+where
"a <=s b = (sint a <= sint b)"
-definition word_sless :: "'a :: len word => 'a word => bool" ("(_/ <s _)" [50, 51] 50) where
+definition word_sless :: "'a :: len word => 'a word => bool" ("(_/ <s _)" [50, 51] 50)
+where
"(x <s y) = (x <=s y & x ~= y)"
@@ -398,10 +420,12 @@
definition
word_lsb_def: "lsb a \<longleftrightarrow> bin_last (uint a)"
-definition shiftl1 :: "'a word \<Rightarrow> 'a word" where
+definition shiftl1 :: "'a word \<Rightarrow> 'a word"
+where
"shiftl1 w = word_of_int (uint w BIT False)"
-definition shiftr1 :: "'a word \<Rightarrow> 'a word" where
+definition shiftr1 :: "'a word \<Rightarrow> 'a word"
+where
-- "shift right as unsigned or as signed, ie logical or arithmetic"
"shiftr1 w = word_of_int (bin_rest (uint w))"
@@ -434,76 +458,95 @@
end
-definition setBit :: "'a :: len0 word => nat => 'a word" where
+definition setBit :: "'a :: len0 word => nat => 'a word"
+where
"setBit w n = set_bit w n True"
-definition clearBit :: "'a :: len0 word => nat => 'a word" where
+definition clearBit :: "'a :: len0 word => nat => 'a word"
+where
"clearBit w n = set_bit w n False"
subsection "Shift operations"
-definition sshiftr1 :: "'a :: len word => 'a word" where
+definition sshiftr1 :: "'a :: len word => 'a word"
+where
"sshiftr1 w = word_of_int (bin_rest (sint w))"
-definition bshiftr1 :: "bool => 'a :: len word => 'a word" where
+definition bshiftr1 :: "bool => 'a :: len word => 'a word"
+where
"bshiftr1 b w = of_bl (b # butlast (to_bl w))"
-definition sshiftr :: "'a :: len word => nat => 'a word" (infixl ">>>" 55) where
+definition sshiftr :: "'a :: len word => nat => 'a word" (infixl ">>>" 55)
+where
"w >>> n = (sshiftr1 ^^ n) w"
-definition mask :: "nat => 'a::len word" where
+definition mask :: "nat => 'a::len word"
+where
"mask n = (1 << n) - 1"
-definition revcast :: "'a :: len0 word => 'b :: len0 word" where
+definition revcast :: "'a :: len0 word => 'b :: len0 word"
+where
"revcast w = of_bl (takefill False (len_of TYPE('b)) (to_bl w))"
-definition slice1 :: "nat => 'a :: len0 word => 'b :: len0 word" where
+definition slice1 :: "nat => 'a :: len0 word => 'b :: len0 word"
+where
"slice1 n w = of_bl (takefill False n (to_bl w))"
-definition slice :: "nat => 'a :: len0 word => 'b :: len0 word" where
+definition slice :: "nat => 'a :: len0 word => 'b :: len0 word"
+where
"slice n w = slice1 (size w - n) w"
subsection "Rotation"
-definition rotater1 :: "'a list => 'a list" where
+definition rotater1 :: "'a list => 'a list"
+where
"rotater1 ys =
(case ys of [] => [] | x # xs => last ys # butlast ys)"
-definition rotater :: "nat => 'a list => 'a list" where
+definition rotater :: "nat => 'a list => 'a list"
+where
"rotater n = rotater1 ^^ n"
-definition word_rotr :: "nat => 'a :: len0 word => 'a :: len0 word" where
+definition word_rotr :: "nat => 'a :: len0 word => 'a :: len0 word"
+where
"word_rotr n w = of_bl (rotater n (to_bl w))"
-definition word_rotl :: "nat => 'a :: len0 word => 'a :: len0 word" where
+definition word_rotl :: "nat => 'a :: len0 word => 'a :: len0 word"
+where
"word_rotl n w = of_bl (rotate n (to_bl w))"
-definition word_roti :: "int => 'a :: len0 word => 'a :: len0 word" where
+definition word_roti :: "int => 'a :: len0 word => 'a :: len0 word"
+where
"word_roti i w = (if i >= 0 then word_rotr (nat i) w
else word_rotl (nat (- i)) w)"
subsection "Split and cat operations"
-definition word_cat :: "'a :: len0 word => 'b :: len0 word => 'c :: len0 word" where
+definition word_cat :: "'a :: len0 word => 'b :: len0 word => 'c :: len0 word"
+where
"word_cat a b = word_of_int (bin_cat (uint a) (len_of TYPE ('b)) (uint b))"
-definition word_split :: "'a :: len0 word => ('b :: len0 word) * ('c :: len0 word)" where
+definition word_split :: "'a :: len0 word => ('b :: len0 word) * ('c :: len0 word)"
+where
"word_split a =
(case bin_split (len_of TYPE ('c)) (uint a) of
(u, v) => (word_of_int u, word_of_int v))"
-definition word_rcat :: "'a :: len0 word list => 'b :: len0 word" where
+definition word_rcat :: "'a :: len0 word list => 'b :: len0 word"
+where
"word_rcat ws =
word_of_int (bin_rcat (len_of TYPE ('a)) (map uint ws))"
-definition word_rsplit :: "'a :: len0 word => 'b :: len word list" where
+definition word_rsplit :: "'a :: len0 word => 'b :: len word list"
+where
"word_rsplit w =
map word_of_int (bin_rsplit (len_of TYPE ('b)) (len_of TYPE ('a), uint w))"
-definition max_word :: "'a::len word" -- "Largest representable machine integer." where
+definition max_word :: "'a::len word" -- "Largest representable machine integer."
+where
"max_word = word_of_int (2 ^ len_of TYPE('a) - 1)"
(* FIXME: only provide one theorem name *)
@@ -4536,7 +4579,8 @@
subsection {* Recursion combinator for words *}
-definition word_rec :: "'a \<Rightarrow> ('b::len word \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b word \<Rightarrow> 'a" where
+definition word_rec :: "'a \<Rightarrow> ('b::len word \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b word \<Rightarrow> 'a"
+where
"word_rec forZero forSuc n = nat_rec forZero (forSuc \<circ> of_nat) (unat n)"
lemma word_rec_0: "word_rec z s 0 = z"