# HG changeset patch # User krauss # Date 1149510367 -7200 # Node ID be5c23ebe1eb663ef5418f74d37a294fd911f98b # Parent c40ce2de20209af3a01ccc44c329c3f3b12680b3 HOL/Tools/function_package: Added support for mutual recursive definitions. diff -r c40ce2de2020 -r be5c23ebe1eb src/HOL/Datatype.thy --- a/src/HOL/Datatype.thy Mon Jun 05 14:22:58 2006 +0200 +++ b/src/HOL/Datatype.thy Mon Jun 05 14:26:07 2006 +0200 @@ -6,8 +6,7 @@ header {* Datatypes *} theory Datatype -imports Datatype_Universe FunDef -uses ("Tools/function_package/fundef_datatype.ML") +imports Datatype_Universe begin subsection {* Representing primitive types *} @@ -316,8 +315,6 @@ haskell (target_atom "Just") -use "Tools/function_package/fundef_datatype.ML" -setup FundefDatatype.setup end diff -r c40ce2de2020 -r be5c23ebe1eb src/HOL/FunDef.thy --- a/src/HOL/FunDef.thy Mon Jun 05 14:22:58 2006 +0200 +++ b/src/HOL/FunDef.thy Mon Jun 05 14:26:07 2006 +0200 @@ -1,13 +1,17 @@ theory FunDef -imports Accessible_Part +imports Accessible_Part Datatype Recdef uses +("Tools/function_package/sum_tools.ML") ("Tools/function_package/fundef_common.ML") ("Tools/function_package/fundef_lib.ML") ("Tools/function_package/context_tree.ML") ("Tools/function_package/fundef_prep.ML") ("Tools/function_package/fundef_proof.ML") ("Tools/function_package/termination.ML") +("Tools/function_package/mutual.ML") ("Tools/function_package/fundef_package.ML") +("Tools/function_package/fundef_datatype.ML") +("Tools/function_package/auto_term.ML") begin lemma fundef_ex1_existence: @@ -34,16 +38,52 @@ by simp +subsection {* Projections *} +consts + lpg::"(('a + 'b) * 'a) set" + rpg::"(('a + 'b) * 'b) set" + +inductive lpg +intros + "(Inl x, x) : lpg" +inductive rpg +intros + "(Inr y, y) : rpg" +definition + "lproj x = (THE y. (x,y) : lpg)" + "rproj x = (THE y. (x,y) : rpg)" + +lemma lproj_inl: + "lproj (Inl x) = x" + by (auto simp:lproj_def intro: the_equality lpg.intros elim: lpg.cases) +lemma rproj_inr: + "rproj (Inr x) = x" + by (auto simp:rproj_def intro: the_equality rpg.intros elim: rpg.cases) + + + + +use "Tools/function_package/sum_tools.ML" use "Tools/function_package/fundef_common.ML" use "Tools/function_package/fundef_lib.ML" use "Tools/function_package/context_tree.ML" use "Tools/function_package/fundef_prep.ML" use "Tools/function_package/fundef_proof.ML" use "Tools/function_package/termination.ML" +use "Tools/function_package/mutual.ML" use "Tools/function_package/fundef_package.ML" setup FundefPackage.setup +use "Tools/function_package/fundef_datatype.ML" +setup FundefDatatype.setup + +use "Tools/function_package/auto_term.ML" +setup FundefAutoTerm.setup + + +lemmas [fundef_cong] = + let_cong if_cong image_cong INT_cong UN_cong bex_cong ball_cong imp_cong end diff -r c40ce2de2020 -r be5c23ebe1eb src/HOL/List.thy --- a/src/HOL/List.thy Mon Jun 05 14:22:58 2006 +0200 +++ b/src/HOL/List.thy Mon Jun 05 14:26:07 2006 +0200 @@ -6,7 +6,7 @@ header {* The datatype of finite lists *} theory List -imports PreList +imports PreList FunDef begin datatype 'a list = @@ -498,7 +498,7 @@ lemma map_eq_conv[simp]: "(map f xs = map g xs) = (!x : set xs. f x = g x)" by (induct xs) auto -lemma map_cong [recdef_cong]: +lemma map_cong [fundef_cong, recdef_cong]: "xs = ys ==> (!!x. x : set ys ==> f x = g x) ==> map f xs = map g ys" -- {* a congruence rule for @{text map} *} by simp @@ -863,7 +863,7 @@ (\us vs. ys = us @ x # vs \ (\u\set us. \ P u) \ P x \ xs = filter P vs)" by(auto dest:Cons_eq_filterD) -lemma filter_cong[recdef_cong]: +lemma filter_cong[fundef_cong, recdef_cong]: "xs = ys \ (\x. x \ set ys \ P x = Q x) \ filter P xs = filter Q ys" apply simp apply(erule thin_rl) @@ -1363,12 +1363,12 @@ apply(auto) done -lemma takeWhile_cong [recdef_cong]: +lemma takeWhile_cong [fundef_cong, recdef_cong]: "[| l = k; !!x. x : set l ==> P x = Q x |] ==> takeWhile P l = takeWhile Q k" by (induct k fixing: l, simp_all) -lemma dropWhile_cong [recdef_cong]: +lemma dropWhile_cong [fundef_cong, recdef_cong]: "[| l = k; !!x. x : set l ==> P x = Q x |] ==> dropWhile P l = dropWhile Q k" by (induct k fixing: l, simp_all) @@ -1613,12 +1613,12 @@ lemma foldr_append[simp]: "foldr f (xs @ ys) a = foldr f xs (foldr f ys a)" by (induct xs) auto -lemma foldl_cong [recdef_cong]: +lemma foldl_cong [fundef_cong, recdef_cong]: "[| a = b; l = k; !!a x. x : set l ==> f a x = g a x |] ==> foldl f a l = foldl g b k" by (induct k fixing: a b l, simp_all) -lemma foldr_cong [recdef_cong]: +lemma foldr_cong [fundef_cong, recdef_cong]: "[| a = b; l = k; !!a x. x : set l ==> f x a = g x a |] ==> foldr f l a = foldr g k b" by (induct k fixing: a b l, simp_all) diff -r c40ce2de2020 -r be5c23ebe1eb src/HOL/Recdef.thy --- a/src/HOL/Recdef.thy Mon Jun 05 14:22:58 2006 +0200 +++ b/src/HOL/Recdef.thy Mon Jun 05 14:26:07 2006 +0200 @@ -6,7 +6,7 @@ header {* TFL: recursive function definitions *} theory Recdef -imports Wellfounded_Relations Datatype +imports Wellfounded_Relations uses ("../TFL/casesplit.ML") ("../TFL/utils.ML") @@ -18,7 +18,6 @@ ("../TFL/tfl.ML") ("../TFL/post.ML") ("Tools/recdef_package.ML") - ("Tools/function_package/auto_term.ML") begin lemma tfl_eq_True: "(x = True) --> x" @@ -97,7 +96,4 @@ qed -use "Tools/function_package/auto_term.ML" -setup FundefAutoTerm.setup - end diff -r c40ce2de2020 -r be5c23ebe1eb src/HOL/Tools/function_package/auto_term.ML --- a/src/HOL/Tools/function_package/auto_term.ML Mon Jun 05 14:22:58 2006 +0200 +++ b/src/HOL/Tools/function_package/auto_term.ML Mon Jun 05 14:26:07 2006 +0200 @@ -32,7 +32,7 @@ val {simps, congs, wfs} = RecdefPackage.get_local_hints ctxt val ss = local_simpset_of ctxt addsimps simps - val intro_rule = ProofContext.get_thm ctxt (Name "termination_intro") + val intro_rule = ProofContext.get_thm ctxt (Name "termination") in Method.RAW_METHOD (K (auto_term_tac intro_rule diff -r c40ce2de2020 -r be5c23ebe1eb src/HOL/Tools/function_package/fundef_common.ML --- a/src/HOL/Tools/function_package/fundef_common.ML Mon Jun 05 14:22:58 2006 +0200 +++ b/src/HOL/Tools/function_package/fundef_common.ML Mon Jun 05 14:26:07 2006 +0200 @@ -22,6 +22,7 @@ | Cong of (term * thm * depgraph * ((string * typ) list * thm list * ctx_tree) list) | RCall of (term * ctx_tree) +type glrs = (term list * term list * term * term) list (* A record containing all the relevant symbols and types needed during the proof. @@ -39,8 +40,18 @@ datatype rec_call_info = - RCInfo of {RI: thm, RIvs: (string * typ) list, lRI: thm, lRIq: thm, Gh: thm, Gh': thm} - + RCInfo + of { + RI: thm, + RIvs: (string * typ) list, + lRI: thm, + lRIq: thm, + Gh: thm, + Gh': thm, + GmAs: term list, + rcarg: term +} + datatype clause_info = ClauseInfo of { @@ -73,6 +84,36 @@ datatype curry_info = Curry of { argTs: typ list, curry_ss: simpset } +type inj_proj = ((term -> term) * (term -> term)) + +type qgar = (string * typ) list * term list * term list * term + +datatype mutual_part = + MutualPart of + { + f_name: string, + const: string * typ, + cargTs: typ list, + pthA: SumTools.sum_path, + pthR: SumTools.sum_path, + qgars: qgar list, + f_def: thm + } + + +datatype mutual_info = + Mutual of + { + name: string, + sum_const: string * typ, + ST: typ, + RST: typ, + streeA: SumTools.sum_tree, + streeR: SumTools.sum_tree, + parts: mutual_part list, + qglrss: (term list * term list * term * term) list list + } + datatype prep_result = Prep of @@ -99,11 +140,28 @@ dom_intros : thm list } +datatype fundef_mresult = + FundefMResult of + { + f: term, + G : term, + R : term, + + psimps : thm list list, + subset_pinducts : thm list, + simple_pinducts : thm list, + cases : thm, + termination : thm, + domintros : thm list + } + + +type result_with_names = fundef_mresult * mutual_info * string list list * attribute list list list structure FundefData = TheoryDataFun (struct val name = "HOL/function_def/data"; - type T = string * fundef_result Symtab.table + type T = string * result_with_names Symtab.table val empty = ("", Symtab.empty); val copy = I; diff -r c40ce2de2020 -r be5c23ebe1eb src/HOL/Tools/function_package/fundef_datatype.ML --- a/src/HOL/Tools/function_package/fundef_datatype.ML Mon Jun 05 14:22:58 2006 +0200 +++ b/src/HOL/Tools/function_package/fundef_datatype.ML Mon Jun 05 14:26:07 2006 +0200 @@ -18,6 +18,7 @@ structure FundefDatatype : FUNDEF_DATATYPE = struct + fun mk_argvar i T = Free ("_av" ^ (string_of_int i), T) fun mk_patvar i T = Free ("_pv" ^ (string_of_int i), T) diff -r c40ce2de2020 -r be5c23ebe1eb src/HOL/Tools/function_package/fundef_lib.ML --- a/src/HOL/Tools/function_package/fundef_lib.ML Mon Jun 05 14:22:58 2006 +0200 +++ b/src/HOL/Tools/function_package/fundef_lib.ML Mon Jun 05 14:26:07 2006 +0200 @@ -62,3 +62,6 @@ fun upairs [] = [] | upairs (x::xs) = map (pair x) (x::xs) @ upairs xs + +fun the_single [x] = x + | the_single _ = sys_error "the_single" \ No newline at end of file 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 diff -r c40ce2de2020 -r be5c23ebe1eb src/HOL/Tools/function_package/fundef_prep.ML --- a/src/HOL/Tools/function_package/fundef_prep.ML Mon Jun 05 14:22:58 2006 +0200 +++ b/src/HOL/Tools/function_package/fundef_prep.ML Mon Jun 05 14:26:07 2006 +0200 @@ -11,6 +11,11 @@ sig val prepare_fundef_curried : thm list -> term list -> theory -> FundefCommon.curry_info option * xstring * (FundefCommon.prep_result * theory) + + val prepare_fundef_new : theory -> thm list -> string -> term -> FundefCommon.glrs -> string list + -> FundefCommon.prep_result * theory + + end @@ -125,12 +130,17 @@ val RI = freezeT RI val lRI = localize RI val lRIq = fold_rev (forall_intr o cterm_of thy o mk_var0) RIvs lRI + val plRI = prop_of lRI + val GmAs = Logic.strip_imp_prems plRI + val rcarg = case Logic.strip_imp_concl plRI of + trueprop $ (memb $ (pair $ rcarg $ _) $ R) => rcarg + | _ => raise Match val Gh_term = Pattern.rewrite_term thy [rw_RI_to_h_assum, rw_f_to_h] [] (prop_of lRIq) val Gh = assume (cterm_of thy Gh_term) val Gh' = assume (cterm_of thy (rename_vars Gh_term)) in - RCInfo {RI=RI, RIvs=RIvs, lRI=lRI, lRIq=lRIq, Gh=Gh, Gh'=Gh'} + RCInfo {RI=RI, RIvs=RIvs, lRI=lRI, lRIq=lRIq, Gh=Gh, Gh'=Gh', GmAs=GmAs, rcarg=rcarg} end val case_hyp = assume (cterm_of thy (Trueprop (mk_eq (x, lhs)))) @@ -151,7 +161,7 @@ (* Chooses fresh free names, declares G and R, defines f and returns a record with all the information *) -fun setup_context (f, glrs, used) fname congs thy = +fun setup_context (f, glrs, used) defname congs thy = let val trees = map (build_tree thy f congs) glrs val allused = fold FundefCtxTree.add_context_varnames trees used @@ -175,8 +185,8 @@ val GT = mk_relT (domT, ranT) val RT = mk_relT (domT, domT) - val G_name = fname ^ "_graph" - val R_name = fname ^ "_rel" + val G_name = defname ^ "_graph" + val R_name = defname ^ "_rel" val glrs' = mk_primed_vars thy glrs @@ -292,9 +302,9 @@ * Defines the function, the graph and the termination relation, synthesizes completeness * and comatibility conditions and returns everything. *) -fun prepare_fundef congs eqs fname thy = +fun prepare_fundef congs eqs defname thy = let - val (names, thy) = setup_context (analyze_eqs eqs) fname congs thy + val (names, thy) = setup_context (analyze_eqs eqs) defname congs thy val Names {G, R, glrs, trees, ...} = names val {G_intros, vRiss, R_intross, complete, compat} = extract_conditions thy names trees congs @@ -310,6 +320,28 @@ end +fun prepare_fundef_new thy congs defname f glrs used = + let + val (names, thy) = setup_context (f, glrs, used) defname congs thy + val Names {G, R, glrs, trees, ...} = names + + val {G_intros, vRiss, R_intross, complete, compat} = extract_conditions thy names trees congs + + val (G_intro_thms, (thy, _)) = inductive_def G_intros (thy, G) + val (R_intro_thmss, (thy, _)) = fold_burrow inductive_def R_intross (thy, R) + + val n = length glrs + val clauses = map3 (mk_clause_info thy names) ((1 upto n) ~~ glrs) (G_intro_thms ~~ trees) (map2 (curry op ~~) vRiss R_intro_thmss) + in + (Prep {names = names, complete=complete, compat=compat, clauses = clauses}, + thy) + end + + + + + + fun prepare_fundef_curried congs eqs thy = diff -r c40ce2de2020 -r be5c23ebe1eb src/HOL/Tools/function_package/fundef_proof.ML --- a/src/HOL/Tools/function_package/fundef_proof.ML Mon Jun 05 14:22:58 2006 +0200 +++ b/src/HOL/Tools/function_package/fundef_proof.ML Mon Jun 05 14:26:07 2006 +0200 @@ -10,6 +10,9 @@ signature FUNDEF_PROOF = sig + val mk_partial_rules : theory -> thm list -> FundefCommon.prep_result + -> thm -> thm list -> FundefCommon.fundef_result + val mk_partial_rules_curried : theory -> thm list -> FundefCommon.curry_info option -> FundefCommon.prep_result -> thm -> thm list -> FundefCommon.fundef_result end @@ -42,7 +45,7 @@ -fun mk_simp thy names f_iff graph_is_function clause valthm = +fun mk_psimp thy names f_iff graph_is_function clause valthm = let val Names {R, acc_R, domT, z, ...} = names val ClauseInfo {qs, cqs, gs, lhs, rhs, ...} = clause @@ -56,10 +59,10 @@ |> (fn it => it COMP valthm) |> implies_intr lhs_acc |> asm_simplify (HOL_basic_ss addsimps [f_iff]) - |> fold forall_intr cqs +(* |> fold forall_intr cqs |> forall_elim_vars 0 |> varifyT - |> Drule.close_derivation + |> Drule.close_derivation*) end @@ -143,20 +146,23 @@ |> implies_intr a_D |> implies_intr D_dcl |> implies_intr D_subset - |> forall_intr_frees - |> forall_elim_vars 0 + + val subset_induct_all = fold_rev (forall_intr o cterm_of thy) [P, a, D] subset_induct_rule val simple_induct_rule = subset_induct_rule - |> instantiate' [] [SOME (cterm_of thy acc_R)] + |> forall_intr (cterm_of thy D) + |> forall_elim (cterm_of thy acc_R) |> (curry op COMP) subset_refl |> (curry op COMP) (acc_downward |> (instantiate' [SOME (ctyp_of thy domT)] (map (SOME o cterm_of thy) [x, R, z])) |> forall_intr (cterm_of thy z) |> forall_intr (cterm_of thy x)) + |> forall_intr (cterm_of thy a) + |> forall_intr (cterm_of thy P) in - (varifyT subset_induct_rule, varifyT simple_induct_rule) + (subset_induct_all, simple_induct_rule) end @@ -344,25 +350,13 @@ let val Names {z, R, acc_R, ...} = names val ClauseInfo {qs, gs, lhs, rhs, ...} = clause - - val z_lhs = cterm_of thy (HOLogic.mk_prod (z,lhs)) - val z_acc = cterm_of thy (HOLogic.mk_mem (z,acc_R)) - - val icases = R_cases - |> instantiate' [] [SOME z_lhs, SOME z_acc] - |> forall_intr_frees - |> forall_elim_vars 0 - val goal = cterm_of thy (HOLogic.mk_Trueprop (HOLogic.mk_mem (lhs,acc_R))) in Goal.init goal - |> SINGLE (resolve_tac [accI] 1) |> the - |> SINGLE (eresolve_tac [icases] 1) |> the - |> SINGLE (CLASIMPSET auto_tac) |> the + |> (SINGLE (resolve_tac [accI] 1)) |> print |> the + |> (SINGLE (eresolve_tac [R_cases] 1)) |> print |> the + |> (SINGLE (CLASIMPSET auto_tac)) |> print |> the |> Goal.conclude - |> forall_intr_frees - |> forall_elim_vars 0 - |> varifyT end @@ -530,7 +524,7 @@ val f_iff = (graph_is_function RS inst_ex1_iff) val _ = Output.debug "Proving simplification rules" - val psimps = map2 (mk_simp thy names f_iff graph_is_function) clauses values + val psimps = map2 (mk_psimp thy names f_iff graph_is_function) clauses values val _ = Output.debug "Proving partial induction rule" val (subset_pinduct, simple_pinduct) = mk_partial_induct_rule thy names complete_thm clauses diff -r c40ce2de2020 -r be5c23ebe1eb src/HOL/Tools/function_package/mutual.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/function_package/mutual.ML Mon Jun 05 14:26:07 2006 +0200 @@ -0,0 +1,264 @@ +(* Title: HOL/Tools/function_package/mutual.ML + ID: $Id$ + Author: Alexander Krauss, TU Muenchen + +A package for general recursive function definitions. +Tools for mutual recursive definitions. + +*) + +signature FUNDEF_MUTUAL = +sig + + val prepare_fundef_mutual : thm list -> term list list -> theory -> + (FundefCommon.mutual_info * string * (FundefCommon.prep_result * theory)) + + + val mk_partial_rules_mutual : theory -> thm list -> FundefCommon.mutual_info -> FundefCommon.prep_result -> thm -> thm list -> + FundefCommon.fundef_mresult +end + + +structure FundefMutual: FUNDEF_MUTUAL = +struct + +open FundefCommon + + + +fun check_const (Const C) = C + | check_const _ = raise ERROR "Head symbol of every left hand side must be a constant." (* FIXME: Output the equation here *) + + + + + +fun split_def geq = + let + val gs = Logic.strip_imp_prems geq + val eq = Logic.strip_imp_concl geq + val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq) + val (fc, args) = strip_comb f_args + val f = check_const fc + + val qs = fold_rev Term.add_frees args [] + + val rhs_new_vars = (Term.add_frees rhs []) \\ qs + val _ = if null rhs_new_vars then () + else raise ERROR "Variables occur on right hand side only: " (* FIXME: Output vars here *) + in + ((f, length args), (qs, gs, args, rhs)) + end + + +fun analyze_eqs thy eqss = + let + fun all_equal ((x as ((n:string,T), k:int))::xs) = if forall (fn ((n',_),k') => n = n' andalso k = k') xs then x + else raise ERROR ("All equations in a block must describe the same " + ^ "constant and have the same number of arguments.") + + val def_infoss = map (split_list o map split_def) eqss + val (consts, qgarss) = split_list (map (fn (Cis, eqs) => (all_equal Cis, eqs)) def_infoss) + + val cnames = map (fst o fst) consts + val check_rcs = exists_Const (fn (n,_) => if n mem cnames + then raise ERROR "Recursive Calls not allowed in premises." else false) + val _ = forall (forall (fn (_, gs, _, _) => forall check_rcs gs)) qgarss + + fun curried_types ((_,T), k) = + let + val (caTs, uaTs) = chop k (binder_types T) + in + (caTs, uaTs ---> body_type T) + end + + val (caTss, resultTs) = split_list (map curried_types consts) + val argTs = map (foldr1 HOLogic.mk_prodT) caTss + + val (RST,streeR, pthsR) = SumTools.mk_tree resultTs + val (ST, streeA, pthsA) = SumTools.mk_tree argTs + + val def_name = foldr1 (fn (a,b) => a ^ "_" ^ b) (map Sign.base_name cnames) + val sfun_xname = def_name ^ "_sum" + val sfun_type = ST --> RST + + val thy = Sign.add_consts_i [(sfun_xname, sfun_type, NoSyn)] thy (* Add the sum function *) + val sfun = Const (Sign.intern_const thy sfun_xname, sfun_type) + + fun define (((((n, T), _), caTs), (pthA, pthR)), qgars) (thy, rews) = + let + val fxname = Sign.extern_const thy n + val f = Const (n, T) + val vars = map_index (fn (i,T) => Free ("x" ^ string_of_int i, T)) caTs + + val f_exp = SumTools.mk_proj streeR pthR (sfun $ SumTools.mk_inj streeA pthA (foldr1 HOLogic.mk_prod vars)) + val def = Logic.mk_equals (list_comb (f, vars), f_exp) + + val ([f_def], thy) = PureThy.add_defs_i false [((fxname ^ "_def", def), [])] thy + val rews' = (f, fold_rev lambda vars f_exp) :: rews + in + (MutualPart {f_name=fxname, const=(n, T),cargTs=caTs,pthA=pthA,pthR=pthR,qgars=qgars,f_def=f_def}, (thy, rews')) + end + + val _ = print pthsA + val _ = print pthsR + + val (parts, (thy, rews)) = fold_map define (((consts ~~ caTss)~~ (pthsA ~~ pthsR)) ~~ qgarss) (thy, []) + + fun mk_qglrss (MutualPart {qgars, pthA, pthR, ...}) = + let + fun convert_eqs (qs, gs, args, rhs) = + (map Free qs, gs, SumTools.mk_inj streeA pthA (foldr1 HOLogic.mk_prod args), + SumTools.mk_inj streeR pthR (Pattern.rewrite_term thy rews [] rhs)) + in + map convert_eqs qgars + end + + val qglrss = map mk_qglrss parts + in + (Mutual {name=def_name,sum_const=dest_Const sfun, ST=ST, RST=RST, streeA=streeA, streeR=streeR, parts=parts, qglrss=qglrss}, thy) + end + + + + +fun prepare_fundef_mutual congs eqss thy = + let + val (mutual, thy) = analyze_eqs thy eqss + val Mutual {name, sum_const, qglrss, ...} = mutual + val global_glrs = flat qglrss + val used = fold (fn (qs, _, _, _) => fold (curry op ins_string o fst o dest_Free) qs) global_glrs [] + in + (mutual, name, FundefPrep.prepare_fundef_new thy congs name (Const sum_const) global_glrs used) + end + + +(* Beta-reduce both sides of a meta-equality *) +fun beta_norm_eq thm = + let + val (lhs, rhs) = dest_equals (cprop_of thm) + val lhs_conv = beta_conversion false lhs + val rhs_conv = beta_conversion false rhs + in + transitive (symmetric lhs_conv) (transitive thm rhs_conv) + end + + + + +fun map_mutual2 f (Mutual {parts, ...}) = + map2 (fn (p as MutualPart {qgars, ...}) => map2 (f p) qgars) parts + + + +fun recover_mutual_psimp thy RST streeR all_f_defs (MutualPart {f_def, pthR, ...}) (_,_,args,_) sum_psimp = + let + val [accCond] = cprems_of sum_psimp + val plain_eq = implies_elim sum_psimp (assume accCond) + val x = Free ("x", RST) + + val f_def_inst = instantiate' [] (map (SOME o cterm_of thy) args) f_def + in + reflexive (cterm_of thy (lambda x (SumTools.mk_proj streeR pthR x))) (* PR(x) == PR(x) *) + |> (fn it => combination it (plain_eq 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) + |> implies_intr accCond + end + + + + + +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) + + +val sum_case_rules = thms "Datatype.sum.cases" +val split_apply = thm "Product_Type.split" + + +fun mutual_induct_rules thy induct all_f_defs (Mutual {qglrss, RST, parts, streeA, ...}) = + let + fun mk_P (MutualPart {cargTs, ...}) Pname = + let + val avars = map_index (fn (i,T) => Var (("a", i), T)) cargTs + val atup = foldr1 HOLogic.mk_prod avars + in + tupled_lambda atup (list_comb (Free (Pname, cargTs ---> HOLogic.boolT), avars)) + end + + val Ps = map2 mk_P parts (mutual_induct_Pnames (length parts)) + val case_exp = SumTools.mk_sumcases streeA HOLogic.boolT Ps + + val induct_inst = + forall_elim (cterm_of thy case_exp) induct + |> full_simplify (HOL_basic_ss addsimps (split_apply :: sum_case_rules)) + |> full_simplify (HOL_basic_ss addsimps all_f_defs) + + fun mk_proj rule (MutualPart {cargTs, pthA, ...}) = + let + val afs = map_index (fn (i,T) => Free ("a" ^ string_of_int i, T)) cargTs + val inj = SumTools.mk_inj streeA pthA (foldr1 HOLogic.mk_prod afs) + in + rule + |> forall_elim (cterm_of thy inj) + |> full_simplify (HOL_basic_ss addsimps (split_apply :: sum_case_rules)) + end + + in + map (mk_proj induct_inst) parts + end + + + + + +fun mk_partial_rules_mutual thy congs (m as Mutual {qglrss, RST, parts, streeR, ...}) data complete_thm compat_thms = + let + val result = FundefProof.mk_partial_rules thy congs data complete_thm compat_thms + val FundefResult {f, G, R, compatibility, completeness, psimps, subset_pinduct,simple_pinduct,total_intro,dom_intros} = result + + val sum_psimps = Library.unflat qglrss psimps + + val all_f_defs = map (fn MutualPart {f_def, ...} => symmetric f_def) parts + val mpsimps = map_mutual2 (recover_mutual_psimp thy RST streeR all_f_defs) m sum_psimps + val minducts = mutual_induct_rules thy simple_pinduct all_f_defs m + val termination = full_simplify (HOL_basic_ss addsimps all_f_defs) total_intro + in + FundefMResult { f=f, G=G, R=R, + psimps=mpsimps, subset_pinducts=[subset_pinduct], simple_pinducts=minducts, + cases=completeness, termination=termination, domintros=dom_intros} + end + + +end + + + + + + + + + + + + + + + + + + + + + + + + + diff -r c40ce2de2020 -r be5c23ebe1eb src/HOL/Tools/function_package/sum_tools.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/function_package/sum_tools.ML Mon Jun 05 14:26:07 2006 +0200 @@ -0,0 +1,109 @@ +(* Title: HOL/Tools/function_package/sum_tools.ML + ID: $Id$ + Author: Alexander Krauss, TU Muenchen + +A package for general recursive function definitions. +Tools for mutual recursive definitions. This could actually be useful for other packages, too, but needs +some cleanup first... + +*) + +signature SUM_TOOLS = +sig + type sum_tree + type sum_path + + val projl_inl: thm + val projr_inr: thm + + val mk_tree : typ list -> typ * sum_tree * sum_path list + + val mk_proj: sum_tree -> sum_path -> term -> term + val mk_inj: sum_tree -> sum_path -> term -> term + + val mk_sumcases: sum_tree -> typ -> term list -> term +end + + +structure SumTools: SUM_TOOLS = +struct + +val inlN = "Sum_Type.Inl" +val inrN = "Sum_Type.Inr" +val sumcaseN = "Datatype.sum.sum_case" + +val projlN = "FunDef.lproj" +val projrN = "FunDef.rproj" +val projl_inl = thm "FunDef.lproj_inl" +val projr_inr = thm "FunDef.rproj_inr" + + + +fun mk_sumT LT RT = Type ("+", [LT, RT]) +fun mk_sumcase TL TR T l r = Const (sumcaseN, (TL --> T) --> (TR --> T) --> mk_sumT TL TR --> T) $ l $ r + + +datatype sum_tree + = Leaf of typ + | Branch of (typ * (typ * sum_tree) * (typ * sum_tree)) + +type sum_path = bool list (* true: left, false: right *) + +fun sum_type_of (Leaf T) = T + | sum_type_of (Branch (ST,(LT,_),(RT,_))) = ST + + +fun mk_tree Ts = + let + fun mk_tree' 1 [T] = (T, Leaf T, [[]]) + | mk_tree' n Ts = + let + val n2 = n div 2 + val (lTs, rTs) = chop n2 Ts + val (TL, ltree, lpaths) = mk_tree' n2 lTs + val (TR, rtree, rpaths) = mk_tree' (n - n2) rTs + val T = mk_sumT TL TR + val pths = map (cons true) lpaths @ map (cons false) rpaths + in + (T, Branch (T, (TL, ltree), (TR, rtree)), pths) + end + in + mk_tree' (length Ts) Ts + end + + +fun mk_inj (Leaf _) [] t = t + | mk_inj (Branch (ST, (LT, tr), _)) (true::pth) t = + Const (inlN, LT --> ST) $ mk_inj tr pth t + | mk_inj (Branch (ST, _, (RT, tr))) (false::pth) t = + Const (inrN, RT --> ST) $ mk_inj tr pth t + | mk_inj _ _ _ = sys_error "mk_inj" + +fun mk_proj (Leaf _) [] t = t + | mk_proj (Branch (ST, (LT, tr), _)) (true::pth) t = + mk_proj tr pth (Const (projlN, ST --> LT) $ t) + | mk_proj (Branch (ST, _, (RT, tr))) (false::pth) t = + mk_proj tr pth (Const (projrN, ST --> RT) $ t) + | mk_proj _ _ _ = sys_error "mk_proj" + + +fun mk_sumcases tree T ts = + let + fun mk_sumcases' (Leaf _) (t::ts) = (t,ts) + | mk_sumcases' (Branch (ST, (LT, ltr), (RT, rtr))) ts = + let + val (lcase, ts') = mk_sumcases' ltr ts + val (rcase, ts'') = mk_sumcases' rtr ts' + in + (mk_sumcase LT RT T lcase rcase, ts'') + end + | mk_sumcases' _ [] = sys_error "mk_sumcases" + in + fst (mk_sumcases' tree ts) + end + +end + + + + diff -r c40ce2de2020 -r be5c23ebe1eb src/HOL/Tools/function_package/termination.ML --- a/src/HOL/Tools/function_package/termination.ML Mon Jun 05 14:22:58 2006 +0200 +++ b/src/HOL/Tools/function_package/termination.ML Mon Jun 05 14:26:07 2006 +0200 @@ -9,8 +9,8 @@ signature FUNDEF_TERMINATION = sig - val mk_total_termination_goal : FundefCommon.fundef_result -> term - val mk_partial_termination_goal : theory -> FundefCommon.fundef_result -> string -> term * term + val mk_total_termination_goal : FundefCommon.result_with_names -> term + val mk_partial_termination_goal : theory -> FundefCommon.result_with_names -> string -> term * term end structure FundefTermination : FUNDEF_TERMINATION = @@ -20,20 +20,16 @@ open FundefCommon open FundefAbbrev -fun mk_total_termination_goal data = +fun mk_total_termination_goal (FundefMResult {R, f, ... }, _, _, _) = let - val FundefResult {R, f, ... } = data - val domT = domain_type (fastype_of f) val x = Free ("x", domT) in Trueprop (mk_mem (x, Const (acc_const_name, fastype_of R --> HOLogic.mk_setT domT) $ R)) end -fun mk_partial_termination_goal thy data dom = +fun mk_partial_termination_goal thy (FundefMResult {R, f, ... }, _, _, _) dom = let - val FundefResult {R, f, ... } = data - val domT = domain_type (fastype_of f) val D = Sign.simple_read_term thy (Type.varifyT (HOLogic.mk_setT domT)) dom val DT = type_of D diff -r c40ce2de2020 -r be5c23ebe1eb src/HOL/Tools/recdef_package.ML --- a/src/HOL/Tools/recdef_package.ML Mon Jun 05 14:22:58 2006 +0200 +++ b/src/HOL/Tools/recdef_package.ML Mon Jun 05 14:26:07 2006 +0200 @@ -300,7 +300,7 @@ LocalRecdefData.init #> Attrib.add_attributes [(recdef_simpN, Attrib.add_del_args simp_add simp_del, "declaration of recdef simp rule"), - (recdef_congN, Attrib.add_del_args (FundefPackage.cong_add o cong_add) (FundefPackage.cong_del o cong_del), "declaration of recdef cong rule"), + (recdef_congN, Attrib.add_del_args cong_add cong_del, "declaration of recdef cong rule"), (recdef_wfN, Attrib.add_del_args wf_add wf_del, "declaration of recdef wf rule")]; diff -r c40ce2de2020 -r be5c23ebe1eb src/HOL/ex/Fundefs.thy --- a/src/HOL/ex/Fundefs.thy Mon Jun 05 14:22:58 2006 +0200 +++ b/src/HOL/ex/Fundefs.thy Mon Jun 05 14:26:07 2006 +0200 @@ -5,11 +5,10 @@ Examples of function definitions using the new "function" package. *) -theory Fundefs +theory Fundefs imports Main begin - section {* Very basic *} consts fib :: "nat \ nat" @@ -22,7 +21,7 @@ text {* we get partial simp and induction rules: *} thm fib.psimps -thm fib.pinduct +thm pinduct text {* There is also a cases rule to distinguish cases along the definition *} thm fib.cases @@ -41,6 +40,8 @@ function "add 0 y = y" "add (Suc x) y = Suc (add x y)" +thm add_rel.cases + by pat_completeness auto termination by (auto_term "measure fst") @@ -50,7 +51,6 @@ section {* Nested recursion *} - consts nz :: "nat \ nat" function "nz 0 = 0" @@ -61,7 +61,9 @@ assumes trm: "x \ nz_dom" shows "nz x = 0" using trm -by induct auto +apply induct +apply auto +done termination nz apply (auto_term "less_than") -- {* Oops, it left us something to prove *} @@ -70,6 +72,36 @@ thm nz.simps thm nz.induct +text {* Here comes McCarthy's 91-function *} + +consts f91 :: "nat => nat" +function + "f91 n = (if 100 < n then n - 10 else f91 (f91 (n + 11)))" +by pat_completeness auto + +(* Prove a lemma before attempting a termination proof *) +lemma f91_estimate: + assumes trm: "n : f91_dom" + shows "n < f91 n + 11" +using trm by induct auto + +(* Now go for termination *) +termination +proof + let ?R = "measure (%x. 101 - x)" + show "wf ?R" .. + + fix n::nat assume "~ 100 < n" (* Inner call *) + thus "(n + 11, n) : ?R" + by simp arith + + assume inner_trm: "n + 11 : f91_dom" (* Outer call *) + with f91_estimate have "n + 11 < f91 (n + 11) + 11" . + with `~ 100 < n` show "(f91 (n + 11), n) : ?R" + by simp arith +qed + + section {* More general patterns *} @@ -84,7 +116,8 @@ "gcd2 (Suc x) (Suc y) = (if x < y then gcd2 (Suc x) (y - x) else gcd2 (x - y) (Suc y))" by pat_completeness auto -termination by (auto_term "measure (\(x,y). x + y)") +termination + by (auto_term "measure (\(x,y). x + y)") thm gcd2.simps thm gcd2.induct @@ -117,4 +150,34 @@ thm ev.induct thm ev.cases + +section {* Mutual Recursion *} + + +consts + evn :: "nat \ bool" + od :: "nat \ bool" + +function + "evn 0 = True" + "evn (Suc n) = od n" +and + "od 0 = False" + "od (Suc n) = evn n" + by pat_completeness auto + +thm evn.psimps +thm od.psimps + +thm evn_od.pinduct +thm evn_od.termination +thm evn_od.domintros + +termination + by (auto_term "measure (sum_case (%n. n) (%n. n))") + +thm evn.simps +thm od.simps + + end