--- a/src/HOL/Word/Bit_Int.thy Fri Sep 06 20:55:14 2013 +0200
+++ b/src/HOL/Word/Bit_Int.thy Fri Sep 06 20:59:36 2013 +0200
@@ -67,12 +67,6 @@
lemma int_and_m1 [simp]: "(-1::int) AND x = x"
by (simp add: bitAND_int.simps)
-lemma Bit_eq_0_iff: "w BIT b = 0 \<longleftrightarrow> w = 0 \<and> b = 0"
- by (subst BIT_eq_iff [symmetric], simp)
-
-lemma Bit_eq_m1_iff: "w BIT b = -1 \<longleftrightarrow> w = -1 \<and> b = 1"
- by (subst BIT_eq_iff [symmetric], simp)
-
lemma int_and_Bits [simp]:
"(x BIT b) AND (y BIT c) = (x AND y) BIT (b AND c)"
by (subst bitAND_int.simps, simp add: Bit_eq_0_iff Bit_eq_m1_iff)
@@ -83,9 +77,6 @@
lemma int_or_minus1 [simp]: "(-1::int) OR x = -1"
unfolding int_or_def by simp
-lemma bit_or_def: "(b::bit) OR c = NOT (NOT b AND NOT c)"
- by (induct b, simp_all) (* TODO: move *)
-
lemma int_or_Bits [simp]:
"(x BIT b) OR (y BIT c) = (x OR y) BIT (b OR c)"
unfolding int_or_def bit_or_def by simp
@@ -93,9 +84,6 @@
lemma int_xor_zero [simp]: "(0::int) XOR x = x"
unfolding int_xor_def by simp
-lemma bit_xor_def: "(b::bit) XOR c = (b AND NOT c) OR (NOT b AND c)"
- by (induct b, simp_all) (* TODO: move *)
-
lemma int_xor_Bits [simp]:
"(x BIT b) XOR (y BIT c) = (x XOR y) BIT (b XOR c)"
unfolding int_xor_def bit_xor_def by simp
@@ -126,12 +114,6 @@
lemma bin_last_XOR [simp]: "bin_last (x XOR y) = bin_last x XOR bin_last y"
by (cases x rule: bin_exhaust, cases y rule: bin_exhaust, simp)
-lemma bit_NOT_eq_1_iff [simp]: "NOT (b::bit) = 1 \<longleftrightarrow> b = 0"
- by (induct b, simp_all)
-
-lemma bit_AND_eq_1_iff [simp]: "(a::bit) AND b = 1 \<longleftrightarrow> a = 1 \<and> b = 1"
- by (induct a, simp_all)
-
lemma bin_nth_ops:
"!!x y. bin_nth (x AND y) n = (bin_nth x n & bin_nth y n)"
"!!x y. bin_nth (x OR y) n = (bin_nth x n | bin_nth y n)"
@@ -367,13 +349,6 @@
lemmas int_and_le =
xtrans(3) [OF bbw_ao_absorbs (2) [THEN conjunct2, symmetric] le_int_or]
-lemma add_BIT_simps [simp]: (* FIXME: move *)
- "x BIT 0 + y BIT 0 = (x + y) BIT 0"
- "x BIT 0 + y BIT 1 = (x + y) BIT 1"
- "x BIT 1 + y BIT 0 = (x + y) BIT 1"
- "x BIT 1 + y BIT 1 = (x + y + 1) BIT 0"
- by (simp_all add: Bit_B0_2t Bit_B1_2t)
-
(* interaction between bit-wise and arithmetic *)
(* good example of bin_induction *)
lemma bin_add_not: "x + NOT x = (-1::int)"
--- a/src/HOL/Word/Bit_Operations.thy Fri Sep 06 20:55:14 2013 +0200
+++ b/src/HOL/Word/Bit_Operations.thy Fri Sep 06 20:59:36 2013 +0200
@@ -90,4 +90,16 @@
lemma bit_not_not [simp]: "NOT (NOT (x::bit)) = x"
by (cases x) auto
+lemma bit_or_def: "(b::bit) OR c = NOT (NOT b AND NOT c)"
+ by (induct b, simp_all)
+
+lemma bit_xor_def: "(b::bit) XOR c = (b AND NOT c) OR (NOT b AND c)"
+ by (induct b, simp_all)
+
+lemma bit_NOT_eq_1_iff [simp]: "NOT (b::bit) = 1 \<longleftrightarrow> b = 0"
+ by (induct b, simp_all)
+
+lemma bit_AND_eq_1_iff [simp]: "(a::bit) AND b = 1 \<longleftrightarrow> a = 1 \<and> b = 1"
+ by (induct a, simp_all)
+
end
--- a/src/HOL/Word/Bit_Representation.thy Fri Sep 06 20:55:14 2013 +0200
+++ b/src/HOL/Word/Bit_Representation.thy Fri Sep 06 20:59:36 2013 +0200
@@ -71,6 +71,12 @@
shows "0 BIT 0 = 0" and "0 BIT 1 = 1" and "1 BIT 0 = 2" and "1 BIT 1 = 3"
unfolding Bit_def by simp_all
+lemma Bit_eq_0_iff: "w BIT b = 0 \<longleftrightarrow> w = 0 \<and> b = 0"
+ by (subst BIT_eq_iff [symmetric], simp)
+
+lemma Bit_eq_m1_iff: "w BIT b = -1 \<longleftrightarrow> w = -1 \<and> b = 1"
+ by (subst BIT_eq_iff [symmetric], simp)
+
lemma BitM_inc: "Num.BitM (Num.inc w) = Num.Bit1 w"
by (induct w, simp_all)
--- a/src/HOL/Word/Bool_List_Representation.thy Fri Sep 06 20:55:14 2013 +0200
+++ b/src/HOL/Word/Bool_List_Representation.thy Fri Sep 06 20:59:36 2013 +0200
@@ -374,23 +374,18 @@
lemma trunc_bl2bin_aux:
"bintrunc m (bl_to_bin_aux bl w) =
bl_to_bin_aux (drop (length bl - m) bl) (bintrunc (m - length bl) w)"
- apply (induct bl arbitrary: w)
- apply clarsimp
- apply clarsimp
- apply safe
- apply (case_tac "m - size bl")
- apply (simp add : diff_is_0_eq [THEN iffD1, THEN Suc_diff_le])
- apply simp
- apply (rule_tac f = "%nat. bl_to_bin_aux bl (bintrunc nat w BIT 1)"
- in arg_cong)
- apply simp
- apply (case_tac "m - size bl")
- apply (simp add: diff_is_0_eq [THEN iffD1, THEN Suc_diff_le])
- apply simp
- apply (rule_tac f = "%nat. bl_to_bin_aux bl (bintrunc nat w BIT 0)"
- in arg_cong)
- apply simp
- done
+proof (induct bl arbitrary: w)
+ case Nil show ?case by simp
+next
+ case (Cons b bl) show ?case
+ proof (cases "m - length bl")
+ case 0 then have "Suc (length bl) - m = Suc (length bl - m)" by simp
+ with Cons show ?thesis by simp
+ next
+ case (Suc n) then have *: "m - Suc (length bl) = n" by simp
+ with Suc Cons show ?thesis by simp
+ qed
+qed
lemma trunc_bl2bin:
"bintrunc m (bl_to_bin bl) = bl_to_bin (drop (length bl - m) bl)"