# HG changeset patch
# User krauss
# Date 1176221398 -7200
# Node ID 5fcee5b319a205e148c739fa8a91be9e9433c95f
# Parent  25693088396b39390c82002b0bdc0acbee6366d8
proper handling of morphisms

diff -r 25693088396b -r 5fcee5b319a2 src/HOL/Tools/function_package/fundef_common.ML
--- a/src/HOL/Tools/function_package/fundef_common.ML	Tue Apr 10 14:11:01 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_common.ML	Tue Apr 10 18:09:58 2007 +0200
@@ -63,6 +63,17 @@
       termination: thm
      }
 
+fun morph_fundef_data phi (FundefCtxData {add_simps, f, R, psimps, pinducts, termination}) =
+    let
+      val term = Morphism.term phi
+      val thm = Morphism.thm phi
+      val fact = Morphism.fact phi
+    in
+      FundefCtxData { add_simps=add_simps (*FIXME ???*), 
+                      f = term f, R = term R, psimps = fact psimps, 
+                      pinducts = fact pinducts, termination = thm termination }
+    end
+
 
 structure FundefData = GenericDataFun
 (struct
diff -r 25693088396b -r 5fcee5b319a2 src/HOL/Tools/function_package/fundef_package.ML
--- a/src/HOL/Tools/function_package/fundef_package.ML	Tue Apr 10 14:11:01 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Tue Apr 10 18:09:58 2007 +0200
@@ -69,6 +69,8 @@
     end
 
 
+fun pr_ctxdata (x: fundef_context_data) = (Output.debug (K (PolyML.makestring x)); x)
+
 fun fundef_afterqed config fixes spec defname cont sort_cont [[proof]] lthy =
     let
       val FundefResult {f, R, psimps, trsimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = 
@@ -89,9 +91,10 @@
 
       val cdata = FundefCtxData { add_simps=addsmps, psimps=psimps',
                                   pinducts=snd pinducts', termination=termination', f=f, R=R }
+            |> morph_fundef_data (LocalTheory.target_morphism lthy)
     in
-      lthy  (* FIXME proper handling of morphism *)
-        |> LocalTheory.declaration (fn phi => add_fundef_data defname cdata) (* save in target *)
+      lthy 
+        |> LocalTheory.declaration (fn phi => add_fundef_data defname (pr_ctxdata (morph_fundef_data phi cdata))) (* save in target *)
         |> Context.proof_map (add_fundef_data defname cdata) (* also save in local context *)
     end (* FIXME: Add cases for induct and cases thm *)
 
diff -r 25693088396b -r 5fcee5b319a2 src/HOL/Tools/function_package/mutual.ML
--- a/src/HOL/Tools/function_package/mutual.ML	Tue Apr 10 14:11:01 2007 +0200
+++ b/src/HOL/Tools/function_package/mutual.ML	Tue Apr 10 18:09:58 2007 +0200
@@ -269,8 +269,9 @@
     end
     
 
-fun mutual_induct_rules thy induct all_f_defs (Mutual {RST, parts, streeA, ...}) =
+fun mutual_induct_rules lthy induct all_f_defs (Mutual {RST, parts, streeA, ...}) =
     let
+      val cert = cterm_of (ProofContext.theory_of lthy)
       val newPs = map2 (fn Pname => fn MutualPart {cargTs, ...} => 
                                        Free (Pname, cargTs ---> HOLogic.boolT))
                        (mutual_induct_Pnames (length parts))
@@ -288,7 +289,7 @@
       val case_exp = SumTools.mk_sumcases streeA HOLogic.boolT Ps
                      
       val induct_inst =
-          forall_elim (cterm_of thy case_exp) induct
+          forall_elim (cert case_exp) induct
                       |> full_simplify (HOL_basic_ss addsimps (split_apply :: sum_case_rules))
                       |> full_simplify (HOL_basic_ss addsimps all_f_defs)
           
@@ -298,9 +299,9 @@
             val inj = SumTools.mk_inj streeA pthA (foldr1 HOLogic.mk_prod afs)
           in
             rule
-              |> forall_elim (cterm_of thy inj)
+              |> forall_elim (cert inj)
               |> full_simplify (HOL_basic_ss addsimps (split_apply :: sum_case_rules))
-              |> fold_rev (forall_intr o cterm_of thy) (afs @ newPs)
+              |> fold_rev (forall_intr o cert) (afs @ newPs)
           end
           
     in
@@ -308,17 +309,8 @@
     end
     
 
-
-
-
-fun mk_partial_rules_mutual lthy inner_cont (m as Mutual {RST, parts, streeR, fqgars, ...}) proof =
+fun mk_partial_rules_mutual lthy inner_cont (m as Mutual {parts, fqgars, ...}) proof =
     let
-      val thy = ProofContext.theory_of lthy
-                                       
-      (* FIXME !? *)
-      val expand = Assumption.export false lthy (LocalTheory.target_of lthy)
-      val expand_term = Drule.term_rule thy expand
-                        
       val result = inner_cont proof
       val FundefResult {f, G, R, cases, psimps, trsimps, subset_pinducts=[subset_pinduct],simple_pinducts=[simple_pinduct],
                         termination,domintros} = result
@@ -334,14 +326,14 @@
           
       val mpsimps = map2 mk_mpsimp fqgars psimps
       val mtrsimps = map_option (map2 mk_mpsimp fqgars) trsimps
-      val minducts = mutual_induct_rules thy simple_pinduct all_f_defs m
+      val minducts = mutual_induct_rules lthy simple_pinduct all_f_defs m
       val mtermination = full_simplify (HOL_basic_ss addsimps all_f_defs) termination
     in
-      FundefResult { f=expand_term f, G=expand_term G, R=expand_term R,
-                     psimps=map expand mpsimps, subset_pinducts=[expand subset_pinduct], simple_pinducts=map expand minducts,
-                     cases=expand cases, termination=expand mtermination,
-                     domintros=map_option (map expand) domintros,
-                     trsimps=map_option (map expand) mtrsimps}
+      FundefResult { f=f, G=G, R=R,
+                     psimps=mpsimps, subset_pinducts=[subset_pinduct], simple_pinducts=minducts,
+                     cases=cases, termination=mtermination,
+                     domintros=domintros,
+                     trsimps=mtrsimps}
     end