diff -r 90b02960c8ce -r 9e7f95903b24 src/HOL/Word/BinGeneral.thy
--- a/src/HOL/Word/BinGeneral.thy	Fri Apr 04 13:40:23 2008 +0200
+++ b/src/HOL/Word/BinGeneral.thy	Fri Apr 04 13:40:24 2008 +0200
@@ -9,98 +9,201 @@
 
 header {* Basic Definitions for Binary Integers *}
 
-theory BinGeneral imports Num_Lemmas
-
+theory BinGeneral
+imports Num_Lemmas
 begin
 
-subsection {* Recursion combinator for binary integers *}
+subsection {* Further properties of numerals *}
+
+datatype bit = B0 | B1
+
+definition
+  Bit :: "int \<Rightarrow> bit \<Rightarrow> int" (infixl "BIT" 90) where
+  "k BIT b = (case b of B0 \<Rightarrow> 0 | B1 \<Rightarrow> 1) + k + k"
+
+lemma BIT_B0_eq_Bit0 [simp]: "w BIT B0 = Int.Bit0 w"
+  unfolding Bit_def Bit0_def by simp
+
+lemma BIT_B1_eq_Bit1 [simp]: "w BIT B1 = Int.Bit1 w"
+  unfolding Bit_def Bit1_def by simp
+
+lemmas BIT_simps = BIT_B0_eq_Bit0 BIT_B1_eq_Bit1
 
-lemma brlem: "(bin = Int.Min) = (- bin + Int.pred 0 = 0)"
-  unfolding Min_def pred_def by arith
+hide (open) const B0 B1
+
+lemma Min_ne_Pls [iff]:  
+  "Int.Min ~= Int.Pls"
+  unfolding Min_def Pls_def by auto
+
+lemmas Pls_ne_Min [iff] = Min_ne_Pls [symmetric]
+
+lemmas PlsMin_defs [intro!] = 
+  Pls_def Min_def Pls_def [symmetric] Min_def [symmetric]
+
+lemmas PlsMin_simps [simp] = PlsMin_defs [THEN Eq_TrueI]
+
+lemma number_of_False_cong: 
+  "False \<Longrightarrow> number_of x = number_of y"
+  by (rule FalseE)
+
+(** ways in which type Bin resembles a datatype **)
 
-function
-  bin_rec :: "'a \<Rightarrow> 'a \<Rightarrow> (int \<Rightarrow> bit \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> int \<Rightarrow> 'a"  
-where 
-  "bin_rec f1 f2 f3 bin = (if bin = Int.Pls then f1 
-    else if bin = Int.Min then f2
-    else case bin_rl bin of (w, b) => f3 w b (bin_rec f1 f2 f3 w))"
-  by pat_completeness auto
+lemma BIT_eq: "u BIT b = v BIT c ==> u = v & b = c"
+  apply (unfold Bit_def)
+  apply (simp (no_asm_use) split: bit.split_asm)
+     apply simp_all
+   apply (drule_tac f=even in arg_cong, clarsimp)+
+  done
+     
+lemmas BIT_eqE [elim!] = BIT_eq [THEN conjE, standard]
+
+lemma BIT_eq_iff [simp]: 
+  "(u BIT b = v BIT c) = (u = v \<and> b = c)"
+  by (rule iffI) auto
+
+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)"
+  unfolding Bit_def by (auto split: bit.split)
 
-termination 
-  apply (relation "measure (nat o abs o snd o snd o snd)")
-   apply simp
-  apply (simp add: Pls_def brlem)
-  apply (clarsimp simp: bin_rl_char pred_def)
-  apply (frule thin_rl [THEN refl [THEN bin_abs_lem [rule_format]]]) 
-    apply (unfold Pls_def Min_def number_of_eq)
-    prefer 2
-    apply (erule asm_rl)
-   apply auto
+lemma le_Bits: 
+  "(v BIT b <= w BIT c) = (v < w | v <= w & (b ~= bit.B1 | c ~= bit.B0))" 
+  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"
+   by (unfold Bit_def) simp
+
+lemma Bit_B1:
+  "k BIT bit.B1 = k + k + 1"
+   by (unfold Bit_def) simp
+  
+lemma Bit_B0_2t: "k BIT bit.B0 = 2 * k"
+  by (rule trans, rule Bit_B0) simp
+
+lemma Bit_B1_2t: "k BIT bit.B1 = 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"
+  apply (simp (no_asm) only: Bit_B0 Bit_B1)
+  apply (simp add: z1pmod2)
   done
 
-declare bin_rec.simps [simp del]
+lemma B1_mod_2 [simp]: "(Int.Bit1 w) mod 2 = 1"
+  unfolding numeral_simps number_of_is_id by (simp add: z1pmod2)
 
-lemma bin_rec_PM:
-  "f = bin_rec f1 f2 f3 ==> f Int.Pls = f1 & f Int.Min = f2"
-  by (auto simp add: bin_rec.simps)
-
-lemma bin_rec_Pls: "bin_rec f1 f2 f3 Int.Pls = f1"
-  by (simp add: bin_rec.simps)
+lemma B0_mod_2 [simp]: "(Int.Bit0 w) mod 2 = 0"
+  unfolding numeral_simps number_of_is_id by simp
 
-lemma bin_rec_Min: "bin_rec f1 f2 f3 Int.Min = f2"
-  by (simp add: bin_rec.simps)
+lemma neB1E [elim!]:
+  assumes ne: "y \<noteq> bit.B1"
+  assumes y: "y = bit.B0 \<Longrightarrow> P"
+  shows "P"
+  apply (rule y)
+  apply (cases y rule: bit.exhaust, simp)
+  apply (simp add: ne)
+  done
 
-lemma bin_rec_Bit0:
-  "f3 Int.Pls bit.B0 f1 = f1 \<Longrightarrow>
-    bin_rec f1 f2 f3 (Int.Bit0 w) = f3 w bit.B0 (bin_rec f1 f2 f3 w)"
-  apply (simp add: bin_rec_Pls bin_rec.simps [of _ _ _ "Int.Bit0 w"])
-  unfolding Pls_def Min_def Bit0_def
-  apply auto
-  apply presburger
-  apply (simp add: bin_rec.simps)
+lemma bin_ex_rl: "EX w b. w BIT b = bin"
+  apply (unfold Bit_def)
+  apply (cases "even bin")
+   apply (clarsimp simp: even_equiv_def)
+   apply (auto simp: odd_equiv_def split: bit.split)
   done
 
-lemma bin_rec_Bit1:
-  "f3 Int.Min bit.B1 f2 = f2 \<Longrightarrow>
-    bin_rec f1 f2 f3 (Int.Bit1 w) = f3 w bit.B1 (bin_rec f1 f2 f3 w)"
-  apply (simp add: bin_rec.simps [of _ _ _ "Int.Bit1 w"])
-  unfolding Pls_def Min_def Bit1_def
-  apply auto
-  apply (cases w)
-  apply auto
-  apply (simp add: bin_rec.simps)
-    unfolding Min_def Pls_def number_of_is_id apply auto
-  unfolding Bit0_def apply presburger
+lemma bin_exhaust:
+  assumes Q: "\<And>x b. bin = x BIT b \<Longrightarrow> Q"
+  shows "Q"
+  apply (insert bin_ex_rl [of bin])  
+  apply (erule exE)+
+  apply (rule Q)
+  apply force
   done
-  
-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)"
-  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
-  bin_rec_Bit0 bin_rec_Bit1
 
 subsection {* Destructors for binary integers *}
 
+definition bin_rl :: "int \<Rightarrow> int \<times> bit" where 
+  [code func del]: "bin_rl w = (THE (r, l). w = r BIT l)"
+
+lemma bin_rl_char: "(bin_rl w = (r, l)) = (r BIT l = w)"
+  apply (unfold bin_rl_def)
+  apply safe
+   apply (cases w rule: bin_exhaust)
+   apply auto
+  done
+
 definition
   bin_rest_def [code func del]: "bin_rest w = fst (bin_rl w)"
 
 definition
   bin_last_def [code func del] : "bin_last w = snd (bin_rl w)"
 
-definition
-  bin_sign_def [code func del] : "bin_sign = bin_rec Int.Pls Int.Min (%w b s. s)"
-
 primrec bin_nth where
-  "bin_nth.Z" : "bin_nth w 0 = (bin_last w = bit.B1)"
-  | "bin_nth.Suc" : "bin_nth w (Suc n) = bin_nth (bin_rest w) n"
+  Z: "bin_nth w 0 = (bin_last w = bit.B1)"
+  | Suc: "bin_nth w (Suc n) = bin_nth (bin_rest w) n"
 
 lemma bin_rl: "bin_rl w = (bin_rest w, bin_last w)"
   unfolding bin_rest_def bin_last_def by auto
 
+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 (r BIT b) = (r, b)"
+  unfolding bin_rl_char by simp_all
+
+declare bin_rl_simps(1-4) [code func]
+
 lemmas bin_rl_simp [simp] = iffD1 [OF bin_rl_char bin_rl]
 
+lemma bin_abs_lem:
+  "bin = (w BIT b) ==> ~ bin = Int.Min --> ~ bin = Int.Pls -->
+    nat (abs w) < nat (abs bin)"
+  apply (clarsimp simp add: bin_rl_char)
+  apply (unfold Pls_def Min_def Bit_def)
+  apply (cases b)
+   apply (clarsimp, arith)
+  apply (clarsimp, arith)
+  done
+
+lemma bin_induct:
+  assumes PPls: "P Int.Pls"
+    and PMin: "P Int.Min"
+    and PBit: "!!bin bit. P bin ==> P (bin BIT bit)"
+  shows "P bin"
+  apply (rule_tac P=P and a=bin and f1="nat o abs" 
+                  in wf_measure [THEN wf_induct])
+  apply (simp add: measure_def inv_image_def)
+  apply (case_tac x rule: bin_exhaust)
+  apply (frule bin_abs_lem)
+  apply (auto simp add : PPls PMin PBit)
+  done
+
+lemma numeral_induct:
+  assumes Pls: "P Int.Pls"
+  assumes Min: "P Int.Min"
+  assumes Bit0: "\<And>w. \<lbrakk>P w; w \<noteq> Int.Pls\<rbrakk> \<Longrightarrow> P (Int.Bit0 w)"
+  assumes Bit1: "\<And>w. \<lbrakk>P w; w \<noteq> Int.Min\<rbrakk> \<Longrightarrow> P (Int.Bit1 w)"
+  shows "P x"
+  apply (induct x rule: bin_induct)
+    apply (rule Pls)
+   apply (rule Min)
+  apply (case_tac bit)
+   apply (case_tac "bin = Int.Pls")
+    apply simp
+   apply (simp add: Bit0)
+  apply (case_tac "bin = Int.Min")
+   apply simp
+  apply (simp add: Bit1)
+  done
+
 lemma bin_rest_simps [simp]: 
   "bin_rest Int.Pls = Int.Pls"
   "bin_rest Int.Min = Int.Min"
@@ -121,16 +224,6 @@
 
 declare bin_last_simps(1-4) [code func]
 
-lemma bin_sign_simps [simp]:
-  "bin_sign Int.Pls = Int.Pls"
-  "bin_sign Int.Min = Int.Min"
-  "bin_sign (Int.Bit0 w) = bin_sign w"
-  "bin_sign (Int.Bit1 w) = bin_sign w"
-  "bin_sign (w BIT b) = bin_sign w"
-  unfolding bin_sign_def by (auto simp: bin_rec_simps)
-
-declare bin_sign_simps(1-4) [code func]
-
 lemma bin_r_l_extras [simp]:
   "bin_last 0 = bit.B0"
   "bin_last (- 1) = bit.B1"
@@ -237,11 +330,94 @@
   bin_nth_0 bin_nth_Suc bin_nth_Pls bin_nth_Min bin_nth_minus
   bin_nth_minus_Bit0 bin_nth_minus_Bit1
 
+
+subsection {* Recursion combinator for binary integers *}
+
+lemma brlem: "(bin = Int.Min) = (- bin + Int.pred 0 = 0)"
+  unfolding Min_def pred_def by arith
+
+function
+  bin_rec :: "'a \<Rightarrow> 'a \<Rightarrow> (int \<Rightarrow> bit \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> int \<Rightarrow> 'a"  
+where 
+  "bin_rec f1 f2 f3 bin = (if bin = Int.Pls then f1 
+    else if bin = Int.Min then f2
+    else case bin_rl bin of (w, b) => f3 w b (bin_rec f1 f2 f3 w))"
+  by pat_completeness auto
+
+termination 
+  apply (relation "measure (nat o abs o snd o snd o snd)")
+   apply simp
+  apply (simp add: Pls_def brlem)
+  apply (clarsimp simp: bin_rl_char pred_def)
+  apply (frule thin_rl [THEN refl [THEN bin_abs_lem [rule_format]]]) 
+    apply (unfold Pls_def Min_def number_of_eq)
+    prefer 2
+    apply (erule asm_rl)
+   apply auto
+  done
+
+declare bin_rec.simps [simp del]
+
+lemma bin_rec_PM:
+  "f = bin_rec f1 f2 f3 ==> f Int.Pls = f1 & f Int.Min = f2"
+  by (auto simp add: bin_rec.simps)
+
+lemma bin_rec_Pls: "bin_rec f1 f2 f3 Int.Pls = f1"
+  by (simp add: bin_rec.simps)
+
+lemma bin_rec_Min: "bin_rec f1 f2 f3 Int.Min = f2"
+  by (simp add: bin_rec.simps)
+
+lemma bin_rec_Bit0:
+  "f3 Int.Pls bit.B0 f1 = f1 \<Longrightarrow>
+    bin_rec f1 f2 f3 (Int.Bit0 w) = f3 w bit.B0 (bin_rec f1 f2 f3 w)"
+  apply (simp add: bin_rec_Pls bin_rec.simps [of _ _ _ "Int.Bit0 w"])
+  unfolding Pls_def Min_def Bit0_def
+  apply auto
+  apply presburger
+  apply (simp add: bin_rec.simps)
+  done
+
+lemma bin_rec_Bit1:
+  "f3 Int.Min bit.B1 f2 = f2 \<Longrightarrow>
+    bin_rec f1 f2 f3 (Int.Bit1 w) = f3 w bit.B1 (bin_rec f1 f2 f3 w)"
+  apply (simp add: bin_rec.simps [of _ _ _ "Int.Bit1 w"])
+  unfolding Pls_def Min_def Bit1_def
+  apply auto
+  apply (cases w)
+  apply auto
+  apply (simp add: bin_rec.simps)
+    unfolding Min_def Pls_def number_of_is_id apply auto
+  unfolding Bit0_def apply presburger
+  done
+  
+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)"
+  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
+  bin_rec_Bit0 bin_rec_Bit1
+
+
+subsection {* Truncating binary integers *}
+
+definition
+  bin_sign_def [code func del] : "bin_sign = bin_rec Int.Pls Int.Min (%w b s. s)"
+
+lemma bin_sign_simps [simp]:
+  "bin_sign Int.Pls = Int.Pls"
+  "bin_sign Int.Min = Int.Min"
+  "bin_sign (Int.Bit0 w) = bin_sign w"
+  "bin_sign (Int.Bit1 w) = bin_sign w"
+  "bin_sign (w BIT b) = bin_sign w"
+  unfolding bin_sign_def by (auto simp: bin_rec_simps)
+
+declare bin_sign_simps(1-4) [code func]
+
 lemma bin_sign_rest [simp]: 
   "bin_sign (bin_rest w) = (bin_sign w)"
-  by (case_tac w rule: bin_exhaust) auto
-
-subsection {* Truncating binary integers *}
+  by (cases w rule: bin_exhaust) auto
 
 consts
   bintrunc :: "nat => int => int"
@@ -718,18 +894,14 @@
 
 subsection {* Splitting and concatenation *}
 
-consts
-  bin_split :: "nat => int => int * int"
-primrec
-  Z : "bin_split 0 w = (w, Int.Pls)"
-  Suc : "bin_split (Suc n) w = (let (w1, w2) = bin_split n (bin_rest w)
-    in (w1, w2 BIT bin_last w))"
+primrec bin_split :: "nat \<Rightarrow> int \<Rightarrow> int \<times> int" where
+  Z: "bin_split 0 w = (w, Int.Pls)"
+  | Suc: "bin_split (Suc n) w = (let (w1, w2) = bin_split n (bin_rest w)
+        in (w1, w2 BIT bin_last w))"
 
-consts
-  bin_cat :: "int => nat => int => int"
-primrec
-  Z : "bin_cat w 0 v = w"
-  Suc : "bin_cat w (Suc n) v = bin_cat w n (bin_rest v) BIT bin_last v"
+primrec bin_cat :: "int \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int" where
+  Z: "bin_cat w 0 v = w"
+  | Suc: "bin_cat w (Suc n) v = bin_cat w n (bin_rest v) BIT bin_last v"
 
 subsection {* Miscellaneous lemmas *}