--- 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 \<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))"
+ bl_to_bin_aux bs (w BIT (if b then 1 else 0))"
definition bl_to_bin :: "bool list \<Rightarrow> 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 \<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)"
+ bin_to_bl_aux n (bin_rest w) ((bin_last w = 1) # bl)"
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 []"