--- a/src/HOL/Word/BinOperations.thy Fri Apr 04 13:40:24 2008 +0200
+++ b/src/HOL/Word/BinOperations.thy Fri Apr 04 13:40:25 2008 +0200
@@ -9,8 +9,8 @@
header {* Bitwise Operations on Binary Integers *}
-theory BinOperations imports BinGeneral BitSyntax
-
+theory BinOperations
+imports BinGeneral BitSyntax
begin
subsection {* Logical operations *}
@@ -21,19 +21,19 @@
begin
definition
- int_not_def: "bitNOT = bin_rec Int.Min Int.Pls
+ int_not_def [code func del]: "bitNOT = bin_rec Int.Min Int.Pls
(\<lambda>w b s. s BIT (NOT b))"
definition
- int_and_def: "bitAND = bin_rec (\<lambda>x. Int.Pls) (\<lambda>y. y)
+ int_and_def [code func del]: "bitAND = bin_rec (\<lambda>x. Int.Pls) (\<lambda>y. y)
(\<lambda>w b s y. s (bin_rest y) BIT (b AND bin_last y))"
definition
- int_or_def: "bitOR = bin_rec (\<lambda>x. x) (\<lambda>y. Int.Min)
+ int_or_def [code func del]: "bitOR = bin_rec (\<lambda>x. x) (\<lambda>y. Int.Min)
(\<lambda>w b s y. s (bin_rest y) BIT (b OR bin_last y))"
definition
- int_xor_def: "bitXOR = bin_rec (\<lambda>x. x) bitNOT
+ int_xor_def [code func del]: "bitXOR = bin_rec (\<lambda>x. x) bitNOT
(\<lambda>w b s y. s (bin_rest y) BIT (b XOR bin_last y))"
instance ..
@@ -43,16 +43,18 @@
lemma int_not_simps [simp]:
"NOT Int.Pls = Int.Min"
"NOT Int.Min = Int.Pls"
- "NOT (w BIT b) = (NOT w) BIT (NOT b)"
"NOT (Int.Bit0 w) = Int.Bit1 (NOT w)"
"NOT (Int.Bit1 w) = Int.Bit0 (NOT w)"
+ "NOT (w BIT b) = (NOT w) BIT (NOT b)"
unfolding int_not_def by (simp_all add: bin_rec_simps)
-lemma int_xor_Pls [simp]:
+declare int_not_simps(1-4) [code func]
+
+lemma int_xor_Pls [simp, code func]:
"Int.Pls XOR x = x"
unfolding int_xor_def by (simp add: bin_rec_PM)
-lemma int_xor_Min [simp]:
+lemma int_xor_Min [simp, code func]:
"Int.Min XOR x = NOT x"
unfolding int_xor_def by (simp add: bin_rec_PM)
@@ -67,7 +69,7 @@
apply (simp add: int_not_simps [symmetric])
done
-lemma int_xor_Bits2 [simp]:
+lemma int_xor_Bits2 [simp, code func]:
"(Int.Bit0 x) XOR (Int.Bit0 y) = Int.Bit0 (x XOR y)"
"(Int.Bit0 x) XOR (Int.Bit1 y) = Int.Bit1 (x XOR y)"
"(Int.Bit1 x) XOR (Int.Bit0 y) = Int.Bit1 (x XOR y)"
@@ -83,16 +85,16 @@
apply clarsimp+
done
-lemma int_xor_extra_simps [simp]:
+lemma int_xor_extra_simps [simp, code func]:
"w XOR Int.Pls = w"
"w XOR Int.Min = NOT w"
using int_xor_x_simps' by simp_all
-lemma int_or_Pls [simp]:
+lemma int_or_Pls [simp, code func]:
"Int.Pls OR x = x"
by (unfold int_or_def) (simp add: bin_rec_PM)
-lemma int_or_Min [simp]:
+lemma int_or_Min [simp, code func]:
"Int.Min OR x = Int.Min"
by (unfold int_or_def) (simp add: bin_rec_PM)
@@ -100,7 +102,7 @@
"(x BIT b) OR (y BIT c) = (x OR y) BIT (b OR c)"
unfolding int_or_def by (simp add: bin_rec_simps)
-lemma int_or_Bits2 [simp]:
+lemma int_or_Bits2 [simp, code func]:
"(Int.Bit0 x) OR (Int.Bit0 y) = Int.Bit0 (x OR y)"
"(Int.Bit0 x) OR (Int.Bit1 y) = Int.Bit1 (x OR y)"
"(Int.Bit1 x) OR (Int.Bit0 y) = Int.Bit1 (x OR y)"
@@ -116,16 +118,16 @@
apply clarsimp+
done
-lemma int_or_extra_simps [simp]:
+lemma int_or_extra_simps [simp, code func]:
"w OR Int.Pls = w"
"w OR Int.Min = Int.Min"
using int_or_x_simps' by simp_all
-lemma int_and_Pls [simp]:
+lemma int_and_Pls [simp, code func]:
"Int.Pls AND x = Int.Pls"
unfolding int_and_def by (simp add: bin_rec_PM)
-lemma int_and_Min [simp]:
+lemma int_and_Min [simp, code func]:
"Int.Min AND x = x"
unfolding int_and_def by (simp add: bin_rec_PM)
@@ -133,7 +135,7 @@
"(x BIT b) AND (y BIT c) = (x AND y) BIT (b AND c)"
unfolding int_and_def by (simp add: bin_rec_simps)
-lemma int_and_Bits2 [simp]:
+lemma int_and_Bits2 [simp, code func]:
"(Int.Bit0 x) AND (Int.Bit0 y) = Int.Bit0 (x AND y)"
"(Int.Bit0 x) AND (Int.Bit1 y) = Int.Bit0 (x AND y)"
"(Int.Bit1 x) AND (Int.Bit0 y) = Int.Bit0 (x AND y)"
@@ -149,7 +151,7 @@
apply clarsimp+
done
-lemma int_and_extra_simps [simp]:
+lemma int_and_extra_simps [simp, code func]:
"w AND Int.Pls = Int.Pls"
"w AND Int.Min = w"
using int_and_x_simps' by simp_all
@@ -374,13 +376,11 @@
subsection {* Setting and clearing bits *}
-consts
+primrec
bin_sc :: "nat => bit => int => int"
-
-primrec
- Z : "bin_sc 0 b w = bin_rest w BIT b"
- Suc :
- "bin_sc (Suc n) b w = bin_sc n b (bin_rest w) BIT bin_last w"
+where
+ Z: "bin_sc 0 b w = bin_rest w BIT b"
+ | Suc: "bin_sc (Suc n) b w = bin_sc n b (bin_rest w) BIT bin_last w"
(** nth bit, set/clear **)
@@ -479,76 +479,63 @@
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 bl_to_bin_aux :: "bool list \<Rightarrow> int \<Rightarrow> int" where
+ Nil: "bl_to_bin_aux [] w = w"
+ | Cons: "bl_to_bin_aux (b # bs) w =
+ bl_to_bin_aux bs (w BIT (if b then bit.B1 else bit.B0))"
-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"
+definition bl_to_bin :: "bool list \<Rightarrow> int" where
+ bl_to_bin_def : "bl_to_bin bs = bl_to_bin_aux bs Int.Pls"
-primrec
- 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)"
+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 = 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 Int.Pls bs"
+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
- Suc : "bl_of_nth (Suc n) f = f n # bl_of_nth n f"
- Z : "bl_of_nth 0 f = []"
+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 = []"
-consts
- takefill :: "'a => nat => 'a list => 'a list"
- app2 :: "('a => 'b => 'c) => 'a list => 'b list => 'c list"
+primrec takefill :: "'a \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+ Z: "takefill fill 0 xs = []"
+ | Suc: "takefill fill (Suc n) xs = (
+ case xs of [] => fill # takefill fill n xs
+ | y # ys => y # takefill fill n ys)"
--- "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)"
+definition map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list" where
+ "map2 f as bs = map (split f) (zip as bs)"
-defs
- app2_def : "app2 f as bs == map (split f) (zip as bs)"
subsection {* Splitting and concatenation *}
--- "rcat and rsplit"
-consts
- bin_rcat :: "nat => int list => int"
- bin_rsplit_aux :: "nat * int list * nat * int => int list"
- bin_rsplit :: "nat => (nat * int) => int list"
- bin_rsplitl_aux :: "nat * int list * nat * int => int list"
- bin_rsplitl :: "nat => (nat * int) => int list"
-
-recdef bin_rsplit_aux "measure (fst o snd o snd)"
- "bin_rsplit_aux (n, bs, (m, c)) =
+definition bin_rcat :: "nat \<Rightarrow> int list \<Rightarrow> int" where
+ "bin_rcat n = foldl (%u v. bin_cat u n v) Int.Pls"
+
+function 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, b # bs, (m - n, a)))"
+ in bin_rsplit_aux n (m - n) a (b # bs))"
+by pat_completeness auto
+termination by (relation "measure (fst o snd)") simp_all
-recdef bin_rsplitl_aux "measure (fst o snd o snd)"
- "bin_rsplitl_aux (n, bs, (m, c)) =
+definition bin_rsplit :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list" where
+ "bin_rsplit n w = bin_rsplit_aux n (fst w) (snd w) []"
+
+function 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, b # bs, (m - n, a)))"
+ in bin_rsplitl_aux n (m - n) a (b # bs))"
+by pat_completeness auto
+termination by (relation "measure (fst o snd)") simp_all
-defs
- bin_rcat_def : "bin_rcat n bs == foldl (%u v. bin_cat u n v) Int.Pls bs"
- bin_rsplit_def : "bin_rsplit n w == bin_rsplit_aux (n, [], w)"
- bin_rsplitl_def : "bin_rsplitl n w == bin_rsplitl_aux (n, [], w)"
-
-
-(* potential for looping *)
+definition bin_rsplitl :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list" where
+ "bin_rsplitl n w = bin_rsplitl_aux n (fst w) (snd w) []"
+
declare bin_rsplit_aux.simps [simp del]
declare bin_rsplitl_aux.simps [simp del]
--- a/src/HOL/Word/WordBitwise.thy Fri Apr 04 13:40:24 2008 +0200
+++ b/src/HOL/Word/WordBitwise.thy Fri Apr 04 13:40:25 2008 +0200
@@ -7,7 +7,9 @@
header {* Bitwise Operations on Words *}
-theory WordBitwise imports WordArith begin
+theory WordBitwise
+imports WordArith
+begin
lemmas bin_log_bintrs = bin_trunc_not bin_trunc_xor bin_trunc_and bin_trunc_or
@@ -205,15 +207,15 @@
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)"
+lemma bl_word_xor: "to_bl (v XOR w) = map2 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)"
+lemma bl_word_or: "to_bl (v OR w) = map2 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)"
+lemma bl_word_and: "to_bl (v AND w) = map2 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])
--- a/src/HOL/Word/WordGenLib.thy Fri Apr 04 13:40:24 2008 +0200
+++ b/src/HOL/Word/WordGenLib.thy Fri Apr 04 13:40:25 2008 +0200
@@ -8,7 +8,8 @@
header {* Miscellaneous Library for Words *}
-theory WordGenLib imports WordShift Boolean_Algebra
+theory WordGenLib
+imports WordShift Boolean_Algebra
begin
declare of_nat_2p [simp]
@@ -174,14 +175,14 @@
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::len word))"
+ map2 op & (to_bl w) (to_bl (mask n::'a::len word))"
by (simp add: bl_word_and)
also
have "to_bl w = take n' (to_bl w) @ drop n' (to_bl w)" by simp
also
- have "app2 op & \<dots> (to_bl (mask n::'a::len word)) =
+ have "map2 op & \<dots> (to_bl (mask n::'a::len word)) =
replicate n' False @ drop n' (to_bl w)"
- unfolding to_bl_mask n'_def app2_def
+ unfolding to_bl_mask n'_def map2_def
by (subst zip_append) auto
finally
show ?thesis .
--- a/src/HOL/Word/WordShift.thy Fri Apr 04 13:40:24 2008 +0200
+++ b/src/HOL/Word/WordShift.thy Fri Apr 04 13:40:25 2008 +0200
@@ -7,7 +7,9 @@
header {* Shifting, Rotating, and Splitting Words *}
-theory WordShift imports WordBitwise begin
+theory WordShift
+imports WordBitwise
+begin
subsection "Bit shifting"
@@ -421,7 +423,7 @@
lemma align_lem_or [rule_format] :
"ALL x m. length x = n + m --> length y = n + m -->
drop m x = replicate n False --> take m y = replicate m False -->
- app2 op | x y = take m x @ drop m y"
+ map2 op | x y = take m x @ drop m y"
apply (induct_tac y)
apply force
apply clarsimp
@@ -435,7 +437,7 @@
lemma align_lem_and [rule_format] :
"ALL x m. length x = n + m --> length y = n + m -->
drop m x = replicate n False --> take m y = replicate m False -->
- app2 op & x y = replicate (n + m) False"
+ map2 op & x y = replicate (n + m) False"
apply (induct_tac y)
apply force
apply clarsimp
@@ -1344,7 +1346,7 @@
lemmas rotater_add = rotater_eqs (2)
-subsubsection "map, app2, commuting with rotate(r)"
+subsubsection "map, map2, commuting with rotate(r)"
lemma last_map: "xs ~= [] ==> last (map f xs) = f (last xs)"
by (induct xs) auto
@@ -1371,13 +1373,13 @@
apply ((case_tac ys, auto simp: neq_Nil_conv)[1])+
done
-lemma but_last_app2 [rule_format] :
+lemma but_last_map2 [rule_format] :
"ALL ys. length xs = length ys --> xs ~= [] -->
- last (app2 f xs ys) = f (last xs) (last ys) &
- butlast (app2 f xs ys) = app2 f (butlast xs) (butlast ys)"
+ last (map2 f xs ys) = f (last xs) (last ys) &
+ butlast (map2 f xs ys) = map2 f (butlast xs) (butlast ys)"
apply (induct "xs")
apply auto
- apply (unfold app2_def)
+ apply (unfold map2_def)
apply ((case_tac ys, auto simp: neq_Nil_conv)[1])+
done
@@ -1390,35 +1392,35 @@
apply ((case_tac ys, auto simp: neq_Nil_conv but_last_zip)[1])+
done
-lemma rotater1_app2:
+lemma rotater1_map2:
"length xs = length ys ==>
- rotater1 (app2 f xs ys) = app2 f (rotater1 xs) (rotater1 ys)"
- unfolding app2_def by (simp add: rotater1_map rotater1_zip)
+ rotater1 (map2 f xs ys) = map2 f (rotater1 xs) (rotater1 ys)"
+ unfolding map2_def by (simp add: rotater1_map rotater1_zip)
lemmas lrth =
box_equals [OF asm_rl length_rotater [symmetric]
length_rotater [symmetric],
- THEN rotater1_app2]
+ THEN rotater1_map2]
-lemma rotater_app2:
+lemma rotater_map2:
"length xs = length ys ==>
- rotater n (app2 f xs ys) = app2 f (rotater n xs) (rotater n ys)"
+ rotater n (map2 f xs ys) = map2 f (rotater n xs) (rotater n ys)"
by (induct n) (auto intro!: lrth)
-lemma rotate1_app2:
+lemma rotate1_map2:
"length xs = length ys ==>
- rotate1 (app2 f xs ys) = app2 f (rotate1 xs) (rotate1 ys)"
- apply (unfold app2_def)
+ rotate1 (map2 f xs ys) = map2 f (rotate1 xs) (rotate1 ys)"
+ apply (unfold map2_def)
apply (cases xs)
apply (cases ys, auto simp add : rotate1_def)+
done
lemmas lth = box_equals [OF asm_rl length_rotate [symmetric]
- length_rotate [symmetric], THEN rotate1_app2]
+ length_rotate [symmetric], THEN rotate1_map2]
-lemma rotate_app2:
+lemma rotate_map2:
"length xs = length ys ==>
- rotate n (app2 f xs ys) = app2 f (rotate n xs) (rotate n ys)"
+ rotate n (map2 f xs ys) = map2 f (rotate n xs) (rotate n ys)"
by (induct n) (auto intro!: lth)
@@ -1537,11 +1539,11 @@
lemmas lbl_lbl = trans [OF word_bl.Rep' word_bl.Rep' [symmetric]]
-lemmas ths_app2 [OF lbl_lbl] = rotate_app2 rotater_app2
+lemmas ths_map2 [OF lbl_lbl] = rotate_map2 rotater_map2
lemmas ths_map [where xs = "to_bl v"] = rotate_map rotater_map
-lemmas th1s [simplified word_rot_defs' [symmetric]] = ths_app2 ths_map
+lemmas th1s [simplified word_rot_defs' [symmetric]] = ths_map2 ths_map
lemma word_rot_logs:
"word_rotl n (NOT v) = NOT word_rotl n v"