# HG changeset patch
# User krauss
# Date 1174567016 -3600
# Node ID 1fe951654cee2ee4c04d7c6138466b5930b663d3
# Parent  1f428200fd9c5d0f152a532b6ed61beec70a91f7
fixed problem with the construction of mutual simp rules

diff -r 1f428200fd9c -r 1fe951654cee src/HOL/Tools/function_package/mutual.ML
--- a/src/HOL/Tools/function_package/mutual.ML	Thu Mar 22 13:36:55 2007 +0100
+++ b/src/HOL/Tools/function_package/mutual.ML	Thu Mar 22 13:36:56 2007 +0100
@@ -68,12 +68,6 @@
     fsum : term option
    }
 
-
-
-
-
-
-
 fun mutual_induct_Pnames n =
     if n < 5 then fst (chop n ["P","Q","R","S"])
     else map (fn i => "P" ^ string_of_int i) (1 upto n)
@@ -82,8 +76,6 @@
 fun open_all_all (Const ("all", _) $ Abs (n, T, b)) = apfst (cons (n, T)) (open_all_all b)
   | open_all_all t = ([], t)
 
-
-
 (* Builds a curried clause description in abstracted form *)
 fun split_def ctxt fnames geq arities =
     let
@@ -252,34 +244,26 @@
       val export = fold_rev (implies_intr o cprop_of) ags
                    #> fold_rev forall_intr_rename (oqnames ~~ cqs)
     in
-      F (f, qs, gs, args, rhs) import export
+      F ctxt (f, qs, gs, args, rhs) import export
     end
 
-
-fun recover_mutual_psimp thy RST streeR all_f_defs parts (f, _, _, args, _) import (export : thm -> thm) sum_psimp_eq =
+fun recover_mutual_psimp all_orig_fdefs parts ctxt (fname, _, _, args, rhs) import (export : thm -> thm) sum_psimp_eq =
     let
-      val (MutualPart {f_defthm=SOME f_def, pthR, ...}) = get_part f parts
-          
+      val (MutualPart {f=SOME f, f_defthm=SOME f_def, pthR, ...}) = get_part fname parts
+
       val psimp = import sum_psimp_eq
       val (simp, restore_cond) = case cprems_of psimp of
                                    [] => (psimp, I)
                                  | [cond] => (implies_elim psimp (assume cond), implies_intr cond)
                                  | _ => sys_error "Too many conditions"
-
-      val x = Free ("x", RST)
-
-      val f_def_inst = fold (fn arg => fn thm => combination thm (reflexive (cterm_of thy arg))) args (Thm.freezeT f_def) (* FIXME *)
-                            |> beta_reduce
     in
-      reflexive (cterm_of thy (lambda x (SumTools.mk_proj streeR pthR x)))  (*  PR(x) == PR(x) *)
-                |> (fn it => combination it (simp RS eq_reflection))
-                |> beta_norm_eq (*  PR(S(I(as))) == PR(IR(...)) *)
-                |> transitive f_def_inst (*  f ... == PR(IR(...)) *)
-                |> simplify (HOL_basic_ss addsimps [SumTools.projl_inl, SumTools.projr_inr]) (*  f ... == ... *)
-                |> simplify (HOL_basic_ss addsimps all_f_defs) (*  f ... == ... *)
-                |> (fn it => it RS meta_eq_to_obj_eq)
-                |> restore_cond
-                |> export
+      Goal.prove ctxt [] [] 
+                 (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs))
+                 (fn _ => SIMPSET (unfold_tac all_orig_fdefs)
+                          THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1
+                          THEN SIMPSET' simp_tac 1)
+        |> restore_cond 
+        |> export
     end
 
 
@@ -353,9 +337,11 @@
       val all_f_defs = map (fn MutualPart {f_defthm = SOME f_def, cargTs, ...} =>
                                mk_applied_form lthy cargTs (symmetric (Thm.freezeT f_def)))
                            parts
+
+      val all_orig_fdefs = map (fn MutualPart {f_defthm = SOME f_def, ...} => f_def) parts
                            
       fun mk_mpsimp fqgar sum_psimp =
-          in_context lthy fqgar (recover_mutual_psimp thy RST streeR all_f_defs parts) sum_psimp
+          in_context lthy fqgar (recover_mutual_psimp all_orig_fdefs parts) sum_psimp
           
       val mpsimps = map2 mk_mpsimp fqgars psimps
       val mtrsimps = map_option (map2 mk_mpsimp fqgars) trsimps