# HG changeset patch # User haftmann # Date 1207309225 -7200 # Node ID 7fcc10088e727533714e906d529b9fe88856cb94 # Parent 9e7f95903b245d4e335c1f299f8e1b54983362e4 renamed app2 to map2 diff -r 9e7f95903b24 -r 7fcc10088e72 src/HOL/Word/BinOperations.thy --- 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 (\w b s. s BIT (NOT b))" definition - int_and_def: "bitAND = bin_rec (\x. Int.Pls) (\y. y) + int_and_def [code func del]: "bitAND = bin_rec (\x. Int.Pls) (\y. y) (\w b s y. s (bin_rest y) BIT (b AND bin_last y))" definition - int_or_def: "bitOR = bin_rec (\x. x) (\y. Int.Min) + int_or_def [code func del]: "bitOR = bin_rec (\x. x) (\y. Int.Min) (\w b s y. s (bin_rest y) BIT (b OR bin_last y))" definition - int_xor_def: "bitXOR = bin_rec (\x. x) bitNOT + int_xor_def [code func del]: "bitXOR = bin_rec (\x. x) bitNOT (\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 \ int \ 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 \ 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 \ int \ bool list \ 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 \ int \ 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 \ (nat \ bool) \ 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 \ nat \ 'a list \ '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 \ 'b \ 'c) \ 'a list \ 'b list \ '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 \ int list \ int" where + "bin_rcat n = foldl (%u v. bin_cat u n v) Int.Pls" + +function bin_rsplit_aux :: "nat \ nat \ int \ int list \ 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 \ nat \ int \ int list" where + "bin_rsplit n w = bin_rsplit_aux n (fst w) (snd w) []" + +function bin_rsplitl_aux :: "nat \ nat \ int \ int list \ 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 \ nat \ int \ 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] diff -r 9e7f95903b24 -r 7fcc10088e72 src/HOL/Word/WordBitwise.thy --- 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]) diff -r 9e7f95903b24 -r 7fcc10088e72 src/HOL/Word/WordGenLib.thy --- 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 & \ (to_bl (mask n::'a::len word)) = + have "map2 op & \ (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 . diff -r 9e7f95903b24 -r 7fcc10088e72 src/HOL/Word/WordShift.thy --- 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"