# 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