# HG changeset patch # User haftmann # Date 1277908093 -7200 # Node ID 8e33b9d04a82ddeabe12aa026e4364a8d2692dc0 # Parent 847e95ca9b0a4c48553957744e79cd36a9f5e58c use existing bit type from theory Bit diff -r 847e95ca9b0a -r 8e33b9d04a82 src/HOL/Word/BinBoolList.thy --- a/src/HOL/Word/BinBoolList.thy Wed Jun 30 16:28:13 2010 +0200 +++ b/src/HOL/Word/BinBoolList.thy Wed Jun 30 16:28:13 2010 +0200 @@ -53,7 +53,7 @@ lemma bin_to_bl_aux_Bit_minus_simp [simp]: "0 < n ==> bin_to_bl_aux n (w BIT b) bl = - bin_to_bl_aux (n - 1) w ((b = bit.B1) # bl)" + bin_to_bl_aux (n - 1) w ((b = 1) # bl)" by (cases n) auto lemma bin_to_bl_aux_Bit0_minus_simp [simp]: @@ -387,15 +387,15 @@ by (cases xs) auto lemma last_bin_last': - "size xs > 0 \ last xs = (bin_last (bl_to_bin_aux xs w) = bit.B1)" + "size xs > 0 \ last xs = (bin_last (bl_to_bin_aux xs w) = 1)" by (induct xs arbitrary: w) auto lemma last_bin_last: - "size xs > 0 ==> last xs = (bin_last (bl_to_bin xs) = bit.B1)" + "size xs > 0 ==> last xs = (bin_last (bl_to_bin xs) = 1)" unfolding bl_to_bin_def by (erule last_bin_last') lemma bin_last_last: - "bin_last w = (if last (bin_to_bl (Suc n) w) then bit.B1 else bit.B0)" + "bin_last w = (if last (bin_to_bl (Suc n) w) then 1 else 0)" apply (unfold bin_to_bl_def) apply simp apply (auto simp add: bin_to_bl_aux_alt) @@ -815,7 +815,7 @@ lemmas rbl_mult_Suc = lessI [THEN rbl_mult_gt] lemma rbbl_Cons: - "b # rev (bin_to_bl n x) = rev (bin_to_bl (Suc n) (x BIT If b bit.B1 bit.B0))" + "b # rev (bin_to_bl n x) = rev (bin_to_bl (Suc n) (x BIT If b 1 0))" apply (unfold bin_to_bl_def) apply simp apply (simp add: bin_to_bl_aux_alt) diff -r 847e95ca9b0a -r 8e33b9d04a82 src/HOL/Word/BinGeneral.thy --- a/src/HOL/Word/BinGeneral.thy Wed Jun 30 16:28:13 2010 +0200 +++ b/src/HOL/Word/BinGeneral.thy Wed Jun 30 16:28:13 2010 +0200 @@ -9,27 +9,22 @@ header {* Basic Definitions for Binary Integers *} theory BinGeneral -imports Num_Lemmas +imports Misc_Numeric Bit begin subsection {* Further properties of numerals *} -datatype bit = B0 | B1 +definition Bit :: "int \ bit \ int" (infixl "BIT" 90) where + "k BIT b = bit_case 0 1 b + k + k" -definition - Bit :: "int \ bit \ int" (infixl "BIT" 90) where - "k BIT b = (case b of B0 \ 0 | B1 \ 1) + k + k" - -lemma BIT_B0_eq_Bit0 [simp]: "w BIT B0 = Int.Bit0 w" +lemma BIT_B0_eq_Bit0 [simp]: "w BIT 0 = Int.Bit0 w" unfolding Bit_def Bit0_def by simp -lemma BIT_B1_eq_Bit1 [simp]: "w BIT B1 = Int.Bit1 w" +lemma BIT_B1_eq_Bit1 [simp]: "w BIT 1 = Int.Bit1 w" unfolding Bit_def Bit1_def by simp lemmas BIT_simps = BIT_B0_eq_Bit0 BIT_B1_eq_Bit1 -hide_const (open) B0 B1 - lemma Min_ne_Pls [iff]: "Int.Min ~= Int.Pls" unfolding Min_def Pls_def by auto @@ -63,32 +58,32 @@ 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)" + "(v BIT b < w BIT c) = (v < w | v <= w & b = (0::bit) & c = (1::bit))" 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))" + "(v BIT b <= w BIT c) = (v < w | v <= w & (b ~= (1::bit) | c ~= (0::bit)))" unfolding Bit_def by (auto split: bit.split) 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" + "k BIT (0::bit) = k + k" by (unfold Bit_def) simp lemma Bit_B1: - "k BIT bit.B1 = k + k + 1" + "k BIT (1::bit) = k + k + 1" by (unfold Bit_def) simp -lemma Bit_B0_2t: "k BIT bit.B0 = 2 * k" +lemma Bit_B0_2t: "k BIT (0::bit) = 2 * k" by (rule trans, rule Bit_B0) simp -lemma Bit_B1_2t: "k BIT bit.B1 = 2 * k + 1" +lemma Bit_B1_2t: "k BIT (1::bit) = 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" + "X = 2 ==> (w BIT (1::bit)) mod X = 1 & (w BIT (0::bit)) mod X = 0" apply (simp (no_asm) only: Bit_B0 Bit_B1) apply (simp add: z1pmod2) done @@ -100,8 +95,8 @@ unfolding numeral_simps number_of_is_id by simp lemma neB1E [elim!]: - assumes ne: "y \ bit.B1" - assumes y: "y = bit.B0 \ P" + assumes ne: "y \ (1::bit)" + assumes y: "y = (0::bit) \ P" shows "P" apply (rule y) apply (cases y rule: bit.exhaust, simp) @@ -128,7 +123,7 @@ subsection {* Destructors for binary integers *} definition bin_last :: "int \ bit" where - "bin_last w = (if w mod 2 = 0 then bit.B0 else bit.B1)" + "bin_last w = (if w mod 2 = 0 then (0::bit) else (1::bit))" definition bin_rest :: "int \ int" where "bin_rest w = w div 2" @@ -144,21 +139,17 @@ done primrec bin_nth where - Z: "bin_nth w 0 = (bin_last w = bit.B1)" + Z: "bin_nth w 0 = (bin_last w = (1::bit))" | Suc: "bin_nth w (Suc n) = bin_nth (bin_rest w) n" lemma bin_rl_simps [simp]: - "bin_rl Int.Pls = (Int.Pls, bit.B0)" - "bin_rl Int.Min = (Int.Min, bit.B1)" - "bin_rl (Int.Bit0 r) = (r, bit.B0)" - "bin_rl (Int.Bit1 r) = (r, bit.B1)" + "bin_rl Int.Pls = (Int.Pls, (0::bit))" + "bin_rl Int.Min = (Int.Min, (1::bit))" + "bin_rl (Int.Bit0 r) = (r, (0::bit))" + "bin_rl (Int.Bit1 r) = (r, (1::bit))" "bin_rl (r BIT b) = (r, b)" unfolding bin_rl_char by simp_all -declare bin_rl_simps(1-4) [code] - -thm iffD1 [OF bin_rl_char bin_rl_def] - lemma bin_rl_simp [simp]: "bin_rest w BIT bin_last w = w" by (simp add: iffD1 [OF bin_rl_char bin_rl_def]) @@ -212,35 +203,27 @@ "bin_rest (w BIT b) = w" using bin_rl_simps bin_rl_def by auto -declare bin_rest_simps(1-4) [code] - lemma bin_last_simps [simp]: - "bin_last Int.Pls = bit.B0" - "bin_last Int.Min = bit.B1" - "bin_last (Int.Bit0 w) = bit.B0" - "bin_last (Int.Bit1 w) = bit.B1" + "bin_last Int.Pls = (0::bit)" + "bin_last Int.Min = (1::bit)" + "bin_last (Int.Bit0 w) = (0::bit)" + "bin_last (Int.Bit1 w) = (1::bit)" "bin_last (w BIT b) = b" using bin_rl_simps bin_rl_def by auto -declare bin_last_simps(1-4) [code] - lemma bin_r_l_extras [simp]: - "bin_last 0 = bit.B0" - "bin_last (- 1) = bit.B1" - "bin_last -1 = bit.B1" - "bin_last 1 = bit.B1" + "bin_last 0 = (0::bit)" + "bin_last (- 1) = (1::bit)" + "bin_last -1 = (1::bit)" + "bin_last 1 = (1::bit)" "bin_rest 1 = 0" "bin_rest 0 = 0" "bin_rest (- 1) = - 1" "bin_rest -1 = -1" - apply (unfold number_of_Min) - apply (unfold Pls_def [symmetric] Min_def [symmetric]) - apply (unfold numeral_1_eq_1 [symmetric]) - apply (auto simp: number_of_eq) - done + by (simp_all add: bin_last_def bin_rest_def) lemma bin_last_mod: - "bin_last w = (if w mod 2 = 0 then bit.B0 else bit.B1)" + "bin_last w = (if w mod 2 = 0 then (0::bit) else (1::bit))" apply (case_tac w rule: bin_exhaust) apply (case_tac b) apply auto @@ -261,10 +244,10 @@ unfolding bin_rest_div [symmetric] by auto lemma Bit0_div2 [simp]: "(Int.Bit0 w) div 2 = w" - using Bit_div2 [where b=bit.B0] by simp + using Bit_div2 [where b="(0::bit)"] by simp lemma Bit1_div2 [simp]: "(Int.Bit1 w) div 2 = w" - using Bit_div2 [where b=bit.B1] by simp + using Bit_div2 [where b="(1::bit)"] by simp lemma bin_nth_lem [rule_format]: "ALL y. bin_nth x = bin_nth y --> x = y" @@ -306,7 +289,7 @@ lemma bin_nth_Min [simp]: "bin_nth Int.Min n" by (induct n) auto -lemma bin_nth_0_BIT: "bin_nth (w BIT b) 0 = (b = bit.B1)" +lemma bin_nth_0_BIT: "bin_nth (w BIT b) 0 = (b = (1::bit))" by auto lemma bin_nth_Suc_BIT: "bin_nth (w BIT b) (Suc n) = bin_nth w n" @@ -317,11 +300,11 @@ lemma bin_nth_minus_Bit0 [simp]: "0 < n ==> bin_nth (Int.Bit0 w) n = bin_nth w (n - 1)" - using bin_nth_minus [where b=bit.B0] by simp + using bin_nth_minus [where b="(0::bit)"] by simp lemma bin_nth_minus_Bit1 [simp]: "0 < n ==> bin_nth (Int.Bit1 w) n = bin_nth w (n - 1)" - using bin_nth_minus [where b=bit.B1] by simp + using bin_nth_minus [where b="(1::bit)"] by simp lemmas bin_nth_0 = bin_nth.simps(1) lemmas bin_nth_Suc = bin_nth.simps(2) @@ -364,18 +347,18 @@ by (simp add: bin_rec.simps) lemma bin_rec_Bit0: - "f3 Int.Pls bit.B0 f1 = f1 \ - bin_rec f1 f2 f3 (Int.Bit0 w) = f3 w bit.B0 (bin_rec f1 f2 f3 w)" + "f3 Int.Pls (0::bit) f1 = f1 \ + bin_rec f1 f2 f3 (Int.Bit0 w) = f3 w (0::bit) (bin_rec f1 f2 f3 w)" by (simp add: bin_rec_Pls bin_rec.simps [of _ _ _ "Int.Bit0 w"]) lemma bin_rec_Bit1: - "f3 Int.Min bit.B1 f2 = f2 \ - bin_rec f1 f2 f3 (Int.Bit1 w) = f3 w bit.B1 (bin_rec f1 f2 f3 w)" + "f3 Int.Min (1::bit) f2 = f2 \ + bin_rec f1 f2 f3 (Int.Bit1 w) = f3 w (1::bit) (bin_rec f1 f2 f3 w)" by (simp add: bin_rec_Min bin_rec.simps [of _ _ _ "Int.Bit1 w"]) lemma bin_rec_Bit: - "f = bin_rec f1 f2 f3 ==> f3 Int.Pls bit.B0 f1 = f1 ==> - f3 Int.Min bit.B1 f2 = f2 ==> f (w BIT b) = f3 w b (f w)" + "f = bin_rec f1 f2 f3 ==> f3 Int.Pls (0::bit) f1 = f1 ==> + f3 Int.Min (1::bit) f2 = f2 ==> f (w BIT b) = f3 w b (f w)" by (cases b, simp add: bin_rec_Bit0, simp add: bin_rec_Bit1) lemmas bin_rec_simps = refl [THEN bin_rec_Bit] bin_rec_Pls bin_rec_Min @@ -411,7 +394,7 @@ sbintrunc :: "nat => int => int" primrec Z : "sbintrunc 0 bin = - (case bin_last bin of bit.B1 => Int.Min | bit.B0 => Int.Pls)" + (case bin_last bin of (1::bit) => Int.Min | (0::bit) => Int.Pls)" Suc : "sbintrunc (Suc n) bin = sbintrunc n (bin_rest bin) BIT (bin_last bin)" lemma sign_bintr: @@ -445,7 +428,7 @@ subsection "Simplifications for (s)bintrunc" lemma bit_bool: - "(b = (b' = bit.B1)) = (b' = (if b then bit.B1 else bit.B0))" + "(b = (b' = (1::bit))) = (b' = (if b then (1::bit) else (0::bit)))" by (cases b') auto lemmas bit_bool1 [simp] = refl [THEN bit_bool [THEN iffD1], symmetric] @@ -472,16 +455,16 @@ done lemma bin_nth_Bit: - "bin_nth (w BIT b) n = (n = 0 & b = bit.B1 | (EX m. n = Suc m & bin_nth w m))" + "bin_nth (w BIT b) n = (n = 0 & b = (1::bit) | (EX m. n = Suc m & bin_nth w m))" by (cases n) auto lemma bin_nth_Bit0: "bin_nth (Int.Bit0 w) n = (EX m. n = Suc m & bin_nth w m)" - using bin_nth_Bit [where b=bit.B0] by simp + using bin_nth_Bit [where b="(0::bit)"] by simp lemma bin_nth_Bit1: "bin_nth (Int.Bit1 w) n = (n = 0 | (EX m. n = Suc m & bin_nth w m))" - using bin_nth_Bit [where b=bit.B1] by simp + using bin_nth_Bit [where b="(1::bit)"] by simp lemma bintrunc_bintrunc_l: "n <= m ==> (bintrunc m (bintrunc n w) = bintrunc n w)" @@ -518,11 +501,11 @@ lemma bintrunc_Bit0 [simp]: "bintrunc (Suc n) (Int.Bit0 w) = Int.Bit0 (bintrunc n w)" - using bintrunc_BIT [where b=bit.B0] by simp + using bintrunc_BIT [where b="(0::bit)"] by simp lemma bintrunc_Bit1 [simp]: "bintrunc (Suc n) (Int.Bit1 w) = Int.Bit1 (bintrunc n w)" - using bintrunc_BIT [where b=bit.B1] by simp + using bintrunc_BIT [where b="(1::bit)"] by simp lemmas bintrunc_Sucs = bintrunc_Pls bintrunc_Min bintrunc_BIT bintrunc_Bit0 bintrunc_Bit1 @@ -538,11 +521,11 @@ lemma sbintrunc_Suc_Bit0 [simp]: "sbintrunc (Suc n) (Int.Bit0 w) = Int.Bit0 (sbintrunc n w)" - using sbintrunc_Suc_BIT [where b=bit.B0] by simp + using sbintrunc_Suc_BIT [where b="(0::bit)"] by simp lemma sbintrunc_Suc_Bit1 [simp]: "sbintrunc (Suc n) (Int.Bit1 w) = Int.Bit1 (sbintrunc n w)" - using sbintrunc_Suc_BIT [where b=bit.B1] by simp + using sbintrunc_Suc_BIT [where b="(1::bit)"] by simp lemmas sbintrunc_Sucs = sbintrunc_Suc_Pls sbintrunc_Suc_Min sbintrunc_Suc_BIT sbintrunc_Suc_Bit0 sbintrunc_Suc_Bit1 @@ -556,11 +539,11 @@ simplified bin_last_simps bin_rest_simps bit.simps, standard] lemmas sbintrunc_0_BIT_B0 [simp] = - sbintrunc.Z [where bin="w BIT bit.B0", + sbintrunc.Z [where bin="w BIT (0::bit)", simplified bin_last_simps bin_rest_simps bit.simps, standard] lemmas sbintrunc_0_BIT_B1 [simp] = - sbintrunc.Z [where bin="w BIT bit.B1", + sbintrunc.Z [where bin="w BIT (1::bit)", simplified bin_last_simps bin_rest_simps bit.simps, standard] lemma sbintrunc_0_Bit0 [simp]: "sbintrunc 0 (Int.Bit0 w) = Int.Pls" @@ -936,12 +919,12 @@ lemmas ls_splits = prod.split split_split prod.split_asm split_split_asm split_if_asm -lemma not_B1_is_B0: "y \ bit.B1 \ y = bit.B0" +lemma not_B1_is_B0: "y \ (1::bit) \ y = (0::bit)" by (cases y) auto lemma B1_ass_B0: - assumes y: "y = bit.B0 \ y = bit.B1" - shows "y = bit.B1" + assumes y: "y = (0::bit) \ y = (1::bit)" + shows "y = (1::bit)" apply (rule classical) apply (drule not_B1_is_B0) apply (erule y) diff -r 847e95ca9b0a -r 8e33b9d04a82 src/HOL/Word/BinOperations.thy --- a/src/HOL/Word/BinOperations.thy Wed Jun 30 16:28:13 2010 +0200 +++ b/src/HOL/Word/BinOperations.thy Wed Jun 30 16:28:13 2010 +0200 @@ -9,7 +9,7 @@ header {* Bitwise Operations on Binary Integers *} theory BinOperations -imports BinGeneral BitSyntax +imports Bit_Operations BinGeneral begin subsection {* Logical operations *} @@ -76,8 +76,8 @@ unfolding BIT_simps [symmetric] int_xor_Bits by simp_all lemma int_xor_x_simps': - "w XOR (Int.Pls BIT bit.B0) = w" - "w XOR (Int.Min BIT bit.B1) = NOT w" + "w XOR (Int.Pls BIT 0) = w" + "w XOR (Int.Min BIT 1) = NOT w" apply (induct w rule: bin_induct) apply simp_all[4] apply (unfold int_xor_Bits) @@ -109,8 +109,8 @@ unfolding BIT_simps [symmetric] int_or_Bits by simp_all lemma int_or_x_simps': - "w OR (Int.Pls BIT bit.B0) = w" - "w OR (Int.Min BIT bit.B1) = Int.Min" + "w OR (Int.Pls BIT 0) = w" + "w OR (Int.Min BIT 1) = Int.Min" apply (induct w rule: bin_induct) apply simp_all[4] apply (unfold int_or_Bits) @@ -142,8 +142,8 @@ unfolding BIT_simps [symmetric] int_and_Bits by simp_all lemma int_and_x_simps': - "w AND (Int.Pls BIT bit.B0) = Int.Pls" - "w AND (Int.Min BIT bit.B1) = w" + "w AND (Int.Pls BIT 0) = Int.Pls" + "w AND (Int.Min BIT 1) = w" apply (induct w rule: bin_induct) apply simp_all[4] apply (unfold int_and_Bits) @@ -384,7 +384,7 @@ (** nth bit, set/clear **) lemma bin_nth_sc [simp]: - "!!w. bin_nth (bin_sc n b w) n = (b = bit.B1)" + "!!w. bin_nth (bin_sc n b w) n = (b = 1)" by (induct n) auto lemma bin_sc_sc_same [simp]: @@ -400,11 +400,11 @@ done 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)" + "!!w m. bin_nth (bin_sc n b w) m = (if m = n then b = 1 else bin_nth w m)" by (induct n) (case_tac [!] m, auto) lemma bin_sc_nth [simp]: - "!!w. (bin_sc n (If (bin_nth w n) bit.B1 bit.B0) w) = w" + "!!w. (bin_sc n (If (bin_nth w n) 1 0) w) = w" by (induct n) auto lemma bin_sign_sc [simp]: @@ -419,7 +419,7 @@ done lemma bin_clr_le: - "!!w. bin_sc n bit.B0 w <= w" + "!!w. bin_sc n 0 w <= w" apply (induct n) apply (case_tac [!] w rule: bin_exhaust) apply (auto simp del: BIT_simps) @@ -428,7 +428,7 @@ done lemma bin_set_ge: - "!!w. bin_sc n bit.B1 w >= w" + "!!w. bin_sc n 1 w >= w" apply (induct n) apply (case_tac [!] w rule: bin_exhaust) apply (auto simp del: BIT_simps) @@ -437,7 +437,7 @@ done lemma bintr_bin_clr_le: - "!!w m. bintrunc n (bin_sc m bit.B0 w) <= bintrunc n w" + "!!w m. bintrunc n (bin_sc m 0 w) <= bintrunc n w" apply (induct n) apply simp apply (case_tac w rule: bin_exhaust) @@ -448,7 +448,7 @@ done lemma bintr_bin_set_ge: - "!!w m. bintrunc n (bin_sc m bit.B1 w) >= bintrunc n w" + "!!w m. bintrunc n (bin_sc m 1 w) >= bintrunc n w" apply (induct n) apply simp apply (case_tac w rule: bin_exhaust) @@ -458,10 +458,10 @@ apply (simp_all split: bit.split) done -lemma bin_sc_FP [simp]: "bin_sc n bit.B0 Int.Pls = Int.Pls" +lemma bin_sc_FP [simp]: "bin_sc n 0 Int.Pls = Int.Pls" by (induct n) auto -lemma bin_sc_TM [simp]: "bin_sc n bit.B1 Int.Min = Int.Min" +lemma bin_sc_TM [simp]: "bin_sc n 1 Int.Min = Int.Min" by (induct n) auto lemmas bin_sc_simps = bin_sc.Z bin_sc.Suc bin_sc_TM bin_sc_FP @@ -481,7 +481,7 @@ 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))" + bl_to_bin_aux bs (w BIT (if b then 1 else 0))" definition bl_to_bin :: "bool list \ int" where bl_to_bin_def : "bl_to_bin bs = bl_to_bin_aux bs Int.Pls" @@ -489,7 +489,7 @@ 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)" + bin_to_bl_aux n (bin_rest w) ((bin_last w = 1) # bl)" definition bin_to_bl :: "nat \ int \ bool list" where bin_to_bl_def : "bin_to_bl n w = bin_to_bl_aux n w []" diff -r 847e95ca9b0a -r 8e33b9d04a82 src/HOL/Word/WordArith.thy --- a/src/HOL/Word/WordArith.thy Wed Jun 30 16:28:13 2010 +0200 +++ b/src/HOL/Word/WordArith.thy Wed Jun 30 16:28:13 2010 +0200 @@ -60,11 +60,11 @@ lemmas word_0_wi_Pls = word_0_wi [folded Pls_def] lemmas word_0_no = word_0_wi_Pls [folded word_no_wi] -lemma int_one_bin: "(1 :: int) == (Int.Pls BIT bit.B1)" +lemma int_one_bin: "(1 :: int) == (Int.Pls BIT 1)" unfolding Pls_def Bit_def by auto lemma word_1_no: - "(1 :: 'a :: len0 word) == number_of (Int.Pls BIT bit.B1)" + "(1 :: 'a :: len0 word) == number_of (Int.Pls BIT 1)" unfolding word_1_wi word_number_of_def int_one_bin by auto lemma word_m1_wi: "-1 == word_of_int -1" diff -r 847e95ca9b0a -r 8e33b9d04a82 src/HOL/Word/WordBitwise.thy --- a/src/HOL/Word/WordBitwise.thy Wed Jun 30 16:28:13 2010 +0200 +++ b/src/HOL/Word/WordBitwise.thy Wed Jun 30 16:28:13 2010 +0200 @@ -386,12 +386,12 @@ by (clarsimp simp add: nth_sbintr word_test_bit_def [symmetric]) lemma word_lsb_no: - "lsb (number_of bin :: 'a :: len word) = (bin_last bin = bit.B1)" + "lsb (number_of bin :: 'a :: len word) = (bin_last bin = 1)" unfolding word_lsb_alt test_bit_no by auto lemma word_set_no: "set_bit (number_of bin::'a::len0 word) n b = - number_of (bin_sc n (if b then bit.B1 else bit.B0) bin)" + number_of (bin_sc n (if b then 1 else 0) bin)" apply (unfold word_set_bit_def word_number_of_def [symmetric]) apply (rule word_eqI) apply (clarsimp simp: word_size bin_nth_sc_gen number_of_is_id diff -r 847e95ca9b0a -r 8e33b9d04a82 src/HOL/Word/WordDefinition.thy --- a/src/HOL/Word/WordDefinition.thy Wed Jun 30 16:28:13 2010 +0200 +++ b/src/HOL/Word/WordDefinition.thy Wed Jun 30 16:28:13 2010 +0200 @@ -8,7 +8,7 @@ header {* Definition of Word Type *} theory WordDefinition -imports Size BinBoolList TdThs +imports Type_Length Misc_Typedef BinBoolList begin subsection {* Type definition *} @@ -204,16 +204,16 @@ definition word_set_bit_def: "set_bit a n x = - word_of_int (bin_sc n (If x bit.B1 bit.B0) (uint a))" + word_of_int (bin_sc n (If x 1 0) (uint a))" definition word_set_bits_def: "(BITS n. f n) = of_bl (bl_of_nth (len_of TYPE ('a)) f)" definition - word_lsb_def: "lsb a \ bin_last (uint a) = bit.B1" + word_lsb_def: "lsb a \ bin_last (uint a) = 1" definition shiftl1 :: "'a word \ 'a word" where - "shiftl1 w = word_of_int (uint w BIT bit.B0)" + "shiftl1 w = word_of_int (uint w BIT 0)" definition shiftr1 :: "'a word \ 'a word" where -- "shift right as unsigned or as signed, ie logical or arithmetic" diff -r 847e95ca9b0a -r 8e33b9d04a82 src/HOL/Word/WordShift.thy --- a/src/HOL/Word/WordShift.thy Wed Jun 30 16:28:13 2010 +0200 +++ b/src/HOL/Word/WordShift.thy Wed Jun 30 16:28:13 2010 +0200 @@ -13,7 +13,7 @@ subsection "Bit shifting" lemma shiftl1_number [simp] : - "shiftl1 (number_of w) = number_of (w BIT bit.B0)" + "shiftl1 (number_of w) = number_of (w BIT 0)" apply (unfold shiftl1_def word_number_of_def) apply (simp add: word_ubin.norm_eq_iff [symmetric] word_ubin.eq_norm del: BIT_simps) @@ -27,7 +27,7 @@ lemmas shiftl1_def_u = shiftl1_def [folded word_number_of_def] -lemma shiftl1_def_s: "shiftl1 w = number_of (sint w BIT bit.B0)" +lemma shiftl1_def_s: "shiftl1 w = number_of (sint w BIT 0)" by (rule trans [OF _ shiftl1_number]) simp lemma shiftr1_0 [simp] : "shiftr1 0 = 0"