merged

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Jun 25 12:15:24 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Jun 25 12:15:49 2010 +0200
@@ -2520,6 +2520,8 @@
   let
     val pred_intro_rule = nth (intros_of ctxt pred) (i - 1)
     val (in_ts, clause_out_ts) = split_mode mode ts;
+    val split_ss = HOL_basic_ss' addsimps [@{thm split_eta}, @{thm split_beta},
+      @{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}]
     fun prove_prems2 out_ts [] =
       print_tac options "before prove_match2 - last call:"
       THEN prove_match2 options ctxt out_ts
@@ -2530,14 +2532,12 @@
       THEN (REPEAT_DETERM (etac @{thm Pair_inject} 1))
       THEN (asm_full_simp_tac HOL_basic_ss' 1)
       THEN SOLVED (print_tac options "state before applying intro rule:"
-      THEN (rtac pred_intro_rule 1)
+      THEN (rtac pred_intro_rule
       (* How to handle equality correctly? *)
-      THEN (print_tac options "state before assumption matching")
-      THEN (REPEAT (atac 1 ORELSE 
-         (CHANGED (asm_full_simp_tac (HOL_basic_ss' addsimps
-           [@{thm split_eta}, @{thm "split_beta"}, @{thm "fst_conv"},
-             @{thm "snd_conv"}, @{thm pair_collapse}]) 1)
-          THEN print_tac options "state after simp_tac:"))))
+      THEN_ALL_NEW (K (print_tac options "state before assumption matching")
+      THEN' (fn i => REPEAT (atac i ORELSE (CHANGED (asm_full_simp_tac split_ss i)
+        THEN print_tac options "state after pre-simplification:")))
+      THEN' (K (print_tac options "state after assumption matching:")))) 1)
     | prove_prems2 out_ts ((p, deriv) :: ps) =
       let
         val mode = head_mode_of deriv

--- a/src/HOL/Word/BinGeneral.thy	Fri Jun 25 12:15:24 2010 +0200
+++ b/src/HOL/Word/BinGeneral.thy	Fri Jun 25 12:15:49 2010 +0200
@@ -127,29 +127,26 @@
 
 subsection {* Destructors for binary integers *}
 
-definition bin_rl :: "int \<Rightarrow> int \<times> bit" where 
-  [code del]: "bin_rl w = (THE (r, l). w = r BIT l)"
+definition bin_last :: "int \<Rightarrow> bit" where
+  "bin_last w = (if w mod 2 = 0 then bit.B0 else bit.B1)"
+
+definition bin_rest :: "int \<Rightarrow> int" where
+  "bin_rest w = w div 2"
 
-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
+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
 
-definition
-  bin_rest_def [code del]: "bin_rest w = fst (bin_rl w)"
-
-definition
-  bin_last_def [code del] : "bin_last w = snd (bin_rl w)"
-
 primrec bin_nth where
   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)"
@@ -160,7 +157,11 @@
 
 declare bin_rl_simps(1-4) [code]
 
-lemmas bin_rl_simp [simp] = iffD1 [OF bin_rl_char bin_rl]
+thm iffD1 [OF bin_rl_char bin_rl_def]
+
+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 -->
@@ -209,7 +210,7 @@
   "bin_rest (Int.Bit0 w) = w"
   "bin_rest (Int.Bit1 w) = w"
   "bin_rest (w BIT b) = w"
-  unfolding bin_rest_def by auto
+  using bin_rl_simps bin_rl_def by auto
 
 declare bin_rest_simps(1-4) [code]
 
@@ -219,7 +220,7 @@
   "bin_last (Int.Bit0 w) = bit.B0"
   "bin_last (Int.Bit1 w) = bit.B1"
   "bin_last (w BIT b) = b"
-  unfolding bin_last_def by auto
+  using bin_rl_simps bin_rl_def by auto
 
 declare bin_last_simps(1-4) [code]
 
@@ -345,14 +346,9 @@
 
 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
+  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 auto
   done
 
 declare bin_rec.simps [simp del]