# HG changeset patch
# User haftmann
# Date 1378493976 -7200
# Node ID 6301ed01e34dbe755007be20052b3f5178218687
# Parent  b098d53152d98f717f45b5e02c8d664b59966c00
slight cleanup of lemma locations; tuned proof

diff -r b098d53152d9 -r 6301ed01e34d src/HOL/Word/Bit_Int.thy
--- 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)"
diff -r b098d53152d9 -r 6301ed01e34d src/HOL/Word/Bit_Operations.thy
--- 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
diff -r b098d53152d9 -r 6301ed01e34d src/HOL/Word/Bit_Representation.thy
--- 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)
 
diff -r b098d53152d9 -r 6301ed01e34d src/HOL/Word/Bool_List_Representation.thy
--- 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)"