# HG changeset patch
# User krauss
# Date 1204716292 -3600
# Node ID 0a0c2752561e1cea86fce6f4caab055eb6028250
# Parent  8292f8723e99b7e03530926f64221b880d219aaf
Use conversions instead of simplifier. tuned

diff -r 8292f8723e99 -r 0a0c2752561e src/HOL/Tools/function_package/context_tree.ML
--- a/src/HOL/Tools/function_package/context_tree.ML	Tue Mar 04 13:35:45 2008 +0100
+++ b/src/HOL/Tools/function_package/context_tree.ML	Wed Mar 05 12:24:52 2008 +0100
@@ -104,8 +104,9 @@
 fun mk_branch ctx t = 
     let
       val (ctx', fixes, impl) = dest_all_all_ctx ctx t
+      val assms = Logic.strip_imp_prems impl
     in
-      (ctx', fixes, Logic.strip_imp_prems impl, rhs_of (Logic.strip_imp_concl impl))
+      (ctx', fixes, assms, rhs_of (Logic.strip_imp_concl impl))
     end
     
 fun find_cong_rule ctx fvar h ((r,dep)::rs) t =
@@ -231,40 +232,37 @@
       snd o traverse_help ([], []) tr []
     end
 
-val is_refl = op aconv o Logic.dest_equals o prop_of
-
 fun rewrite_by_tree thy h ih x tr =
     let
-      fun rewrite_help fix f_as h_as x (Leaf t) = (reflexive (cterm_of thy t), x)
-        | rewrite_help fix f_as h_as x (RCall (_ $ arg, st)) =
+      fun rewrite_help _ _ x (Leaf t) = (reflexive (cterm_of thy t), x)
+        | rewrite_help fix h_as x (RCall (_ $ arg, st)) =
           let
-            val (inner, (lRi,ha)::x') = rewrite_help fix f_as h_as x st
+            val (inner, (lRi,ha)::x') = rewrite_help fix h_as x st (* "a' = a" *)
                                                      
-             (* Need not use the simplifier here. Can use primitive steps! *)
-            val rew_ha = if is_refl inner then I else simplify (HOL_basic_ss addsimps [inner])
-           
-            val h_a_eq_h_a' = combination (reflexive (cterm_of thy h)) inner
             val iha = import_thm thy (fix, h_as) ha (* (a', h a') : G *)
-                                 |> rew_ha
-                      
+                 |> Conv.fconv_rule (Conv.arg_conv (Conv.comb_conv (Conv.arg_conv (K inner))))
+                                                    (* (a, h a) : G   *)
             val inst_ih = instantiate' [] [SOME (cterm_of thy arg)] ih
-            val eq = implies_elim (implies_elim inst_ih lRi) iha
+            val eq = implies_elim (implies_elim inst_ih lRi) iha (* h a = f a *)
                      
-            val h_a'_eq_f_a' = eq RS eq_reflection
-            val result = transitive h_a_eq_h_a' h_a'_eq_f_a'
+            val h_a'_eq_h_a = combination (reflexive (cterm_of thy h)) inner
+            val h_a_eq_f_a = eq RS eq_reflection
+            val result = transitive h_a'_eq_h_a h_a_eq_f_a
           in
             (result, x')
           end
-        | rewrite_help fix f_as h_as x (Cong (crule, deps, branches)) =
+        | rewrite_help fix h_as x (Cong (crule, deps, branches)) =
           let
             fun sub_step lu i x =
                 let
                   val ((fixes, assumes), st) = nth branches i
-                  val used = fold_rev (cons o lu) (IntGraph.imm_succs deps i) []
-                  val used_rev = map (fn u_eq => (u_eq RS sym) RS eq_reflection) used
-                  val assumes' = map (simplify (HOL_basic_ss addsimps (filter_out is_refl used_rev))) assumes
+                  val used = map lu (IntGraph.imm_succs deps i)
+                             |> map (fn u_eq => (u_eq RS sym) RS eq_reflection)
+                             |> filter_out Thm.is_reflexive
+
+                  val assumes' = map (simplify (HOL_basic_ss addsimps used)) assumes
                                  
-                  val (subeq, x') = rewrite_help (fix @ fixes) (f_as @ assumes) (h_as @ assumes') x st
+                  val (subeq, x') = rewrite_help (fix @ fixes) (h_as @ assumes') x st
                   val subeq_exp = export_thm thy (fixes, assumes) (subeq RS meta_eq_to_obj_eq)
                 in
                   (subeq_exp, x')
@@ -275,7 +273,7 @@
             (fold_rev (curry op COMP) subthms crule, x')
           end
     in
-      rewrite_help [] [] [] x tr
+      rewrite_help [] [] x tr
     end
     
 end
diff -r 8292f8723e99 -r 0a0c2752561e src/HOL/Tools/function_package/fundef_core.ML
--- a/src/HOL/Tools/function_package/fundef_core.ML	Tue Mar 04 13:35:45 2008 +0100
+++ b/src/HOL/Tools/function_package/fundef_core.ML	Wed Mar 05 12:24:52 2008 +0100
@@ -295,15 +295,16 @@
 fun mk_replacement_lemma thy h ih_elim clause =
     let
         val ClauseInfo {cdata=ClauseContext {qs, lhs, rhs, cqs, ags, case_hyp, ...}, RCs, tree, ...} = clause
+        local open Conv in
+        val ih_conv = arg1_conv o arg_conv o arg_conv
+        end
 
-        val ih_elim_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_elim
+        val ih_elim_case = Conv.fconv_rule (ih_conv (K (case_hyp RS eq_reflection))) ih_elim
 
         val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs
         val h_assums = map (fn RCInfo {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qs, h_assum)))) RCs
 
-        val ih_elim_case_inst = instantiate' [] [NONE, SOME (cterm_of thy h)] ih_elim_case (* Should be done globally *)
-
-        val (eql, _) = FundefCtxTree.rewrite_by_tree thy h ih_elim_case_inst (Ris ~~ h_assums) tree
+        val (eql, _) = FundefCtxTree.rewrite_by_tree thy h ih_elim_case (Ris ~~ h_assums) tree
 
         val replace_lemma = (eql RS meta_eq_to_obj_eq)
                                 |> implies_intr (cprop_of case_hyp)
@@ -418,6 +419,7 @@
         val ihyp_thm = assume ihyp |> forall_elim_vars 0
         val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex)
         val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un)
+                        |> instantiate' [] [NONE, SOME (cterm_of thy h)]
 
         val _ = Output.debug (K "Proving Replacement lemmas...")
         val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses
@@ -575,6 +577,9 @@
 
 val acc_subset_induct = @{thm Orderings.predicate1I} RS @{thm Accessible_Part.accp_subset_induct}
 
+
+val binder_conv = Conv.arg_conv oo Conv.abs_conv
+
 fun mk_partial_induct_rule thy globals R complete_thm clauses =
     let
       val Globals {domT, x, z, a, P, D, ...} = globals
@@ -603,12 +608,14 @@
 
   fun prove_case clause =
       let
-    val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, gs, lhs, case_hyp, ...}, RCs, 
+    val ClauseInfo {cdata = ClauseContext {ctxt, qs, cqs, ags, gs, lhs, case_hyp, ...}, RCs, 
                     qglr = (oqs, _, _, _), ...} = clause
                        
-    val replace_x_ss = HOL_basic_ss addsimps [case_hyp]
-    val lhs_D = simplify replace_x_ss x_D (* lhs : D *)
-    val sih = full_simplify replace_x_ss aihyp
+    val case_hyp_conv = K (case_hyp RS eq_reflection)
+    local open Conv in 
+    val lhs_D = fconv_rule (arg_conv (arg_conv (case_hyp_conv))) x_D
+    val sih = fconv_rule (binder_conv (K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt) aihyp
+    end
           
     fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) =
         sih |> forall_elim (cterm_of thy rcarg)
@@ -632,7 +639,7 @@
            |> fold Thm.elim_implies P_recs
           
     val res = cterm_of thy (HOLogic.mk_Trueprop (P $ x))
-           |> Simplifier.rewrite replace_x_ss
+           |> Conv.arg_conv (Conv.arg_conv case_hyp_conv)
            |> symmetric (* P lhs == P x *)
            |> (fn eql => equal_elim eql P_lhs) (* "P x" *)
            |> implies_intr (cprop_of case_hyp)
@@ -720,7 +727,7 @@
             val used = map (fn (ctx,thm) => FundefCtxTree.export_thm thy ctx thm) (u @ sub)
                        
             val hyp = HOLogic.mk_Trueprop (R' $ arg $ lhs)
-                      |> fold_rev (curry Logic.mk_implies o prop_of) used
+                      |> fold_rev (curry Logic.mk_implies o prop_of) used (* additional hyps *)
                       |> FundefCtxTree.export_term (fixes, assumes) 
                       |> fold_rev (curry Logic.mk_implies o prop_of) ags
                       |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
@@ -729,25 +736,18 @@
             val thm = assume hyp
                       |> fold forall_elim cqs
                       |> fold Thm.elim_implies ags
-                      |> FundefCtxTree.import_thm thy (fixes, assumes) (*  "(arg, lhs) : R'"  *)
-                      |> fold Thm.elim_implies used
-                      
-            val acc = thm COMP ih_case
+                      |> FundefCtxTree.import_thm thy (fixes, assumes)
+                      |> fold Thm.elim_implies used (*  "(arg, lhs) : R'"  *)
                       
-            val z_eq_arg = cterm_of thy (HOLogic.mk_Trueprop (HOLogic.mk_eq (z, arg)))
-                           
-            val arg_eq_z = (assume z_eq_arg) RS sym
-                           
-            val z_acc = simplify (HOL_basic_ss addsimps [arg_eq_z]) acc (* fragile, slow... *)
-                        |> implies_intr (cprop_of case_hyp)
-                        |> implies_intr z_eq_arg
+            val z_eq_arg = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (z, arg))))
 
-            val z_eq_arg = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (z, arg))))
-            val x_eq_lhs = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (x, lhs))))
-                           
-            val ethm = (z_acc OF [z_eq_arg, x_eq_lhs])
+            val acc = thm COMP ih_case
+            val z_acc_local = acc
+            |> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv (K (symmetric (z_eq_arg RS eq_reflection)))))
+
+            val ethm = z_acc_local
                          |> FundefCtxTree.export_thm thy (fixes, 
-                                                          z_eq_arg :: x_eq_lhs :: ags @ assumes)
+                                                          z_eq_arg :: case_hyp :: ags @ assumes)
                          |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
 
             val sub' = sub @ [(([],[]), acc)]
diff -r 8292f8723e99 -r 0a0c2752561e src/HOL/Tools/function_package/mutual.ML
--- a/src/HOL/Tools/function_package/mutual.ML	Tue Mar 04 13:35:45 2008 +0100
+++ b/src/HOL/Tools/function_package/mutual.ML	Wed Mar 05 12:24:52 2008 +0100
@@ -168,8 +168,6 @@
     end
 
 
-fun beta_reduce thm = Thm.equal_elim (Thm.beta_conversion true (cprop_of thm)) thm
-                      
 fun in_context ctxt (f, pre_qs, pre_gs, pre_args, pre_rhs) F =
     let
       val thy = ProofContext.theory_of ctxt
@@ -222,7 +220,7 @@
       val xs = map_index (fn (i,T) => cterm_of thy (Free ("x" ^ string_of_int i, T))) caTs (* FIXME: Bind xs properly *)
     in
       fold (fn x => fn thm => combination thm (reflexive x)) xs thm
-           |> beta_reduce
+           |> Conv.fconv_rule (Thm.beta_conversion true)
            |> fold_rev forall_intr xs
            |> forall_elim_vars 0
     end