--- 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