diff -r c40ce2de2020 -r be5c23ebe1eb src/HOL/Tools/function_package/fundef_package.ML --- a/src/HOL/Tools/function_package/fundef_package.ML Mon Jun 05 14:22:58 2006 +0200 +++ b/src/HOL/Tools/function_package/fundef_package.ML Mon Jun 05 14:26:07 2006 +0200 @@ -9,12 +9,13 @@ signature FUNDEF_PACKAGE = sig - val add_fundef : ((bstring * Attrib.src list) * string) list -> theory -> Proof.state (* Need an _i variant *) + val add_fundef : ((bstring * Attrib.src list) * string) list list -> theory -> Proof.state (* Need an _i variant *) val cong_add: attribute val cong_del: attribute val setup : theory -> theory + val get_congs : theory -> thm list end @@ -26,46 +27,73 @@ val True_implies = thm "True_implies" +fun add_simps label moreatts (MutualPart {f_name, ...}, psimps) (names, attss) thy = + let + val thy = thy |> Theory.add_path f_name + + val thy = thy |> Theory.add_path label + val spsimps = map standard psimps + val add_list = (names ~~ spsimps) ~~ attss + val (_, thy) = PureThy.add_thms add_list thy + val thy = thy |> Theory.parent_path + + val (_, thy) = PureThy.add_thmss [((label, spsimps), Simplifier.simp_add :: moreatts)] thy + val thy = thy |> Theory.parent_path + in + thy + end + + + + + + fun fundef_afterqed congs curry_info name data names atts thmss thy = let val (complete_thm :: compat_thms) = map hd thmss - val fundef_data = FundefProof.mk_partial_rules_curried thy congs curry_info data (freezeT complete_thm) (map freezeT compat_thms) - val FundefResult {psimps, subset_pinduct, simple_pinduct, total_intro, dom_intros, ...} = fundef_data - + val fundef_data = FundefMutual.mk_partial_rules_mutual thy congs curry_info data (freezeT complete_thm) (map freezeT compat_thms) + val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, ...} = fundef_data + val Mutual {parts, ...} = curry_info val Prep {names = Names {acc_R=accR, ...}, ...} = data val dom_abbrev = Logic.mk_equals (Free (name ^ "_dom", fastype_of accR), accR) val (_, thy) = LocalTheory.mapping NONE (Specification.abbreviation_i ("", false) [(NONE, dom_abbrev)]) thy - val thy = thy |> Theory.add_path name - - val thy = thy |> Theory.add_path "psimps" - val (_, thy) = PureThy.add_thms ((names ~~ psimps) ~~ atts) thy; - val thy = thy |> Theory.parent_path + val thy = fold2 (add_simps "psimps" []) (parts ~~ psimps) (names ~~ atts) thy - val (_, thy) = PureThy.add_thms [(("cases", complete_thm), [RuleCases.case_names names])] thy - val (_, thy) = PureThy.add_thmss [(("domintros", dom_intros), [])] thy - val (_, thy) = PureThy.add_thms [(("termination", total_intro), [])] thy - val (_,thy) = PureThy.add_thms [(("pinduct", simple_pinduct), [RuleCases.case_names names, InductAttrib.induct_set ""])] thy - val (_, thy) = PureThy.add_thmss [(("psimps", psimps), [Simplifier.simp_add])] thy + val thy = thy |> Theory.add_path name + val (_, thy) = PureThy.add_thms [(("cases", complete_thm), [RuleCases.case_names (flat names)])] thy + val (_, thy) = PureThy.add_thmss [(("domintros", domintros), [])] thy + val (_, thy) = PureThy.add_thms [(("termination", termination), [])] thy + val (_,thy) = PureThy.add_thmss [(("pinduct", map standard simple_pinducts), [RuleCases.case_names (flat names), InductAttrib.induct_set ""])] thy val thy = thy |> Theory.parent_path in - add_fundef_data name fundef_data thy + add_fundef_data name (fundef_data, curry_info, names, atts) thy end -fun gen_add_fundef prep_att eqns_atts thy = +fun gen_add_fundef prep_att eqns_attss thy = let - val (natts, eqns) = split_list eqns_atts - val (names, raw_atts) = split_list natts + fun split eqns_atts = + let + val (natts, eqns) = split_list eqns_atts + val (names, raw_atts) = split_list natts + val atts = map (map (prep_att thy)) raw_atts + in + ((names, atts), eqns) + end - val atts = map (map (prep_att thy)) raw_atts + + val (natts, eqns) = split_list (map split_list eqns_attss) + val (names, raw_atts) = split_list (map split_list natts) + + val atts = map (map (map (prep_att thy))) raw_atts val congs = get_fundef_congs (Context.Theory thy) - val t_eqns = map (Sign.read_prop thy) eqns - |> map (term_of o cterm_of thy) (* HACK to prevent strange things from happening with abbreviations *) + val t_eqns = map (map (Sign.read_prop thy)) eqns + |> map (map (term_of o cterm_of thy)) (* HACK to prevent strange things from happening with abbreviations *) - val (curry_info, name, (data, thy)) = FundefPrep.prepare_fundef_curried congs t_eqns thy + val (curry_info, name, (data, thy)) = FundefMutual.prepare_fundef_mutual congs t_eqns thy val Prep {complete, compat, ...} = data val props = (complete :: compat) (*(complete :: fst (chop 110 compat))*) @@ -76,27 +104,23 @@ end -fun total_termination_afterqed name thmss thy = +fun total_termination_afterqed name (Mutual {parts, ...}) thmss thy = let val totality = hd (hd thmss) - val FundefResult {psimps, simple_pinduct, ... } + val (FundefMResult {psimps, simple_pinducts, ... }, Mutual {parts, ...}, names, atts) = the (get_fundef_data name thy) val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies]) - val tsimps = map remove_domain_condition psimps - val tinduct = remove_domain_condition simple_pinduct + val tsimps = map (map remove_domain_condition) psimps + val tinduct = map remove_domain_condition simple_pinducts + + val thy = fold2 (add_simps "simps" [RecfunCodegen.add NONE]) (parts ~~ tsimps) (names ~~ atts) thy val thy = Theory.add_path name thy - (* Need the names and attributes. Apply the attributes again? *) -(* val thy = thy |> Theory.add_path "simps" - val (_, thy) = PureThy.add_thms ((names ~~ tsimps) ~~ atts) thy; - val thy = thy |> Theory.parent_path*) - - val (_, thy) = PureThy.add_thms [(("induct", tinduct), [])] thy - val (_, thy) = PureThy.add_thmss [(("simps", tsimps), [Simplifier.simp_add, RecfunCodegen.add NONE])] thy + val (_, thy) = PureThy.add_thmss [(("induct", map standard tinduct), [])] thy val thy = Theory.parent_path thy in thy @@ -135,13 +159,13 @@ val name = if name = "" then get_last_fundef thy else name val data = the (get_fundef_data name thy) - val FundefResult {total_intro, ...} = data + val (res as FundefMResult {termination, ...}, mutual, _, _) = data val goal = FundefTermination.mk_total_termination_goal data in thy |> ProofContext.init - |> ProofContext.note_thmss_i [(("termination_intro", - [ContextRules.intro_query NONE]), [([total_intro], [])])] |> snd - |> Proof.theorem_i PureThy.internalK NONE (total_termination_afterqed name) NONE ("", []) + |> ProofContext.note_thmss_i [(("termination", + [ContextRules.intro_query NONE]), [([termination], [])])] |> snd + |> Proof.theorem_i PureThy.internalK NONE (total_termination_afterqed name mutual) NONE ("", []) [(("", []), [(goal, [])])] end | fundef_setup_termination_proof name (SOME (dom_name, dom)) thy = @@ -173,6 +197,9 @@ [("fundef_cong", Attrib.add_del_args cong_add cong_del, "declaration of congruence rule for function definitions")] +val get_congs = FundefCommon.get_fundef_congs o Context.Theory + + (* outer syntax *) local structure P = OuterParse and K = OuterKeyword in @@ -182,8 +209,8 @@ val functionP = OuterSyntax.command "function" "define general recursive functions" K.thy_goal - (function_decl >> (fn eqns => - Toplevel.print o Toplevel.theory_to_proof (add_fundef eqns))); + (P.and_list1 function_decl >> (fn eqnss => + Toplevel.print o Toplevel.theory_to_proof (add_fundef eqnss))); val terminationP = OuterSyntax.command "termination" "prove termination of a recursive function" K.thy_goal