author huffman Tue, 13 Dec 2011 11:26:10 +0100 changeset 45843 c58ce659ce2a parent 45825 ff7bdc67e8cb child 45844 6374cd925b18
reorder some definitions and proofs, in preparation for new numeral representation
```--- a/src/HOL/Word/Bit_Representation.thy	Mon Dec 12 23:06:41 2011 +0100
+++ b/src/HOL/Word/Bit_Representation.thy	Tue Dec 13 11:26:10 2011 +0100
@@ -23,6 +23,29 @@
definition Bit :: "int \<Rightarrow> bit \<Rightarrow> int" (infixl "BIT" 90) where
"k BIT b = bitval b + k + k"

+definition bin_last :: "int \<Rightarrow> bit" where
+  "bin_last w = (if w mod 2 = 0 then (0::bit) else (1::bit))"
+
+definition bin_rest :: "int \<Rightarrow> int" where
+  "bin_rest w = w div 2"
+
+lemma bin_rl_simp [simp]:
+  "bin_rest w BIT bin_last w = w"
+  unfolding bin_rest_def bin_last_def Bit_def
+  using mod_div_equality [of w 2]
+  by (cases "w mod 2 = 0", simp_all)
+
+lemma bin_rest_BIT: "bin_rest (x BIT b) = x"
+  unfolding bin_rest_def Bit_def
+  by (cases b, simp_all)
+
+lemma bin_last_BIT: "bin_last (x BIT b) = b"
+  unfolding bin_last_def Bit_def
+  by (cases b, simp_all add: z1pmod2)
+
+lemma BIT_eq: "u BIT b = v BIT c ==> u = v & b = c"
+  by (metis bin_rest_BIT bin_last_BIT)
+
lemma BIT_B0_eq_Bit0 [simp]: "w BIT 0 = Int.Bit0 w"
unfolding Bit_def Bit0_def by simp

@@ -46,14 +69,6 @@
"False \<Longrightarrow> number_of x = number_of y"
by (rule FalseE)

-(** ways in which type Bin resembles a datatype **)
-
-lemma BIT_eq: "u BIT b = v BIT c ==> u = v & b = c"
-  apply (cases b) apply (simp_all)
-  apply (cases c) apply (simp_all)
-  apply (cases c) apply (simp_all)
-  done
-
lemmas BIT_eqE [elim!] = BIT_eq [THEN conjE]

lemma BIT_eq_iff [simp]:
@@ -127,21 +142,11 @@

subsection {* Destructors for binary integers *}

-definition bin_last :: "int \<Rightarrow> bit" where
-  "bin_last w = (if w mod 2 = 0 then (0::bit) else (1::bit))"
-
-definition bin_rest :: "int \<Rightarrow> int" where
-  "bin_rest w = w div 2"
-
definition bin_rl :: "int \<Rightarrow> int \<times> bit" where
"bin_rl w = (bin_rest w, bin_last w)"

lemma bin_rl_char: "bin_rl w = (r, l) \<longleftrightarrow> r BIT l = w"
-  apply (cases l)
-  apply (auto simp add: bin_rl_def bin_last_def bin_rest_def)
-  unfolding Pls_def Min_def Bit0_def Bit1_def number_of_is_id
-  apply arith+
-  done
+  unfolding bin_rl_def by (auto simp: bin_rest_BIT bin_last_BIT)

primrec bin_nth where
Z: "bin_nth w 0 = (bin_last w = (1::bit))"
@@ -155,10 +160,6 @@
"bin_rl (r BIT b) = (r, b)"
unfolding bin_rl_char by simp_all

-lemma bin_rl_simp [simp]:
-  "bin_rest w BIT bin_last w = w"
-  by (simp add: iffD1 [OF bin_rl_char bin_rl_def])
-
lemma bin_abs_lem:
"bin = (w BIT b) ==> ~ bin = Int.Min --> ~ bin = Int.Pls -->
nat (abs w) < nat (abs bin)"```