# HG changeset patch # User krauss # Date 1177056371 -7200 # Node ID 0b14bb35be90f94ad39cda79710b646331bb6944 # Parent 5bd1a2a94e1b535b3fa73ea535967e0f9ba2656a definition lookup via terms, not names. Methods "relation" and "lexicographic_order" do not depend on "termination" setup. diff -r 5bd1a2a94e1b -r 0b14bb35be90 src/HOL/Tools/function_package/auto_term.ML --- a/src/HOL/Tools/function_package/auto_term.ML Fri Apr 20 00:28:07 2007 +0200 +++ b/src/HOL/Tools/function_package/auto_term.ML Fri Apr 20 10:06:11 2007 +0200 @@ -15,18 +15,19 @@ structure FundefRelation : FUNDEF_RELATION = struct -fun relation_tac ctxt rel = +fun inst_thm ctxt rel st = let val cert = Thm.cterm_of (ProofContext.theory_of ctxt) - val rel' = cert (singleton (Variable.polymorphic ctxt) rel) - val rule = FundefCommon.get_termination_rule ctxt |> the - |> Thm.incr_indexes (#maxidx (Thm.rep_cterm rel') + 1) + val st' = Thm.incr_indexes (#maxidx (Thm.rep_cterm rel') + 1) st + val Rvar = cert (Var (the_single (Term.add_vars (prop_of st') []))) + in + Drule.cterm_instantiate [(Rvar, rel')] st' + end - val _ $ premise $ _ = Thm.prop_of rule - val Rvar = cert (Var (the_single (Term.add_vars premise []))) - in rtac (Drule.cterm_instantiate [(Rvar, rel')] rule) end - +fun relation_tac ctxt rel i = + FundefCommon.apply_termination_rule ctxt i + THEN PRIMITIVE (inst_thm ctxt rel) val setup = Method.add_methods [("relation", (Method.SIMPLE_METHOD' o (fn (rel, ctxt) => relation_tac ctxt rel)) oo (Method.syntax Args.term), diff -r 5bd1a2a94e1b -r 0b14bb35be90 src/HOL/Tools/function_package/fundef_common.ML --- a/src/HOL/Tools/function_package/fundef_common.ML Fri Apr 20 00:28:07 2007 +0200 +++ b/src/HOL/Tools/function_package/fundef_common.ML Fri Apr 20 10:06:11 2007 +0200 @@ -17,7 +17,7 @@ val acc_const_name = "Accessible_Part.acc" fun mk_acc domT R = - Const (acc_const_name, (fastype_of R) --> domT --> HOLogic.boolT) $ R + Const (acc_const_name, (domT --> domT --> HOLogic.boolT) --> domT --> HOLogic.boolT) $ R val function_name = suffix "C" val graph_name = suffix "_graph" @@ -36,7 +36,7 @@ datatype fundef_result = FundefResult of { - f: term, + fs: term list, G: term, R: term, @@ -50,12 +50,15 @@ domintros : thm list option } + datatype fundef_context_data = FundefCtxData of { + defname : string, + add_simps : string -> Attrib.src list -> thm list -> local_theory -> thm list * local_theory, - f : term, + fs : term list, R : term, psimps: thm list, @@ -63,27 +66,26 @@ termination: thm } -fun morph_fundef_data phi (FundefCtxData {add_simps, f, R, psimps, pinducts, termination}) = +fun morph_fundef_data phi (FundefCtxData {add_simps, fs, R, psimps, pinducts, termination, defname}) = let - val term = Morphism.term phi - val thm = Morphism.thm phi - val fact = Morphism.fact phi + val term = Morphism.term phi val thm = Morphism.thm phi val fact = Morphism.fact phi + val name = Morphism.name phi in - FundefCtxData { add_simps=add_simps (*FIXME ???*), - f = term f, R = term R, psimps = fact psimps, - pinducts = fact pinducts, termination = thm termination } + FundefCtxData { add_simps = add_simps (* contains no logical entities *), + fs = map term fs, R = term R, psimps = fact psimps, + pinducts = fact pinducts, termination = thm termination, + defname = name defname } end - structure FundefData = GenericDataFun (struct val name = "HOL/function_def/data"; - type T = string * fundef_context_data Symtab.table + type T = (term * fundef_context_data) NetRules.T - val empty = ("", Symtab.empty); + val empty = NetRules.init (op aconv o pairself fst) fst; val copy = I; val extend = I; - fun merge _ ((l1,tab1),(l2,tab2)) = (l1, Symtab.merge (K true) (tab1, tab2)) + fun merge _ (tab1, tab2) = NetRules.merge (tab1, tab2) fun print _ _ = (); end); @@ -100,30 +102,61 @@ end); -fun add_fundef_data name fundef_data = - FundefData.map (fn (last,tab) => (name, Symtab.update_new (name, fundef_data) tab)) +(* Generally useful?? *) +fun lift_morphism thy f = + let + val term = Drule.term_rule thy f + in + Morphism.thm_morphism f $> Morphism.term_morphism term $> Morphism.typ_morphism (Logic.type_map term) + end + +fun import_fundef_data t ctxt = + let + val thy = Context.theory_of ctxt + val ct = cterm_of thy t + val inst_morph = lift_morphism thy o Thm.instantiate -fun get_fundef_data name thy = Symtab.lookup (snd (FundefData.get thy)) name + fun match data = + SOME (morph_fundef_data (inst_morph (Thm.cterm_match (cterm_of thy (fst data), ct))) (snd data)) + handle Pattern.MATCH => NONE + in + get_first match (NetRules.retrieve (FundefData.get ctxt) t) + end -fun set_last_fundef name = FundefData.map (apfst (K name)) -fun get_last_fundef thy = fst (FundefData.get thy) +fun import_last_fundef ctxt = + case NetRules.rules (FundefData.get ctxt) of + [] => NONE + | (t, data) :: _ => + let + val ([t'], ctxt') = Variable.import_terms true [t] (Context.proof_of ctxt) + in + import_fundef_data t' (Context.Proof ctxt') + end +val all_fundef_data = NetRules.rules o FundefData.get val map_fundef_congs = FundefCongs.map val get_fundef_congs = FundefCongs.get -structure TerminationRule = ProofDataFun +structure TerminationRule = GenericDataFun (struct val name = "HOL/function_def/termination" - type T = thm option - fun init _ = NONE + type T = thm list + val empty = [] + val extend = I + fun merge _ = Drule.merge_rules fun print _ _ = () end); -val get_termination_rule = TerminationRule.get -val set_termination_rule = TerminationRule.map o K o SOME +val get_termination_rules = TerminationRule.get +val store_termination_rule = TerminationRule.map o cons +val apply_termination_rule = resolve_tac o get_termination_rules o Context.Proof + +fun add_fundef_data (data as FundefCtxData {fs, termination, ...}) = + FundefData.map (fold (fn f => NetRules.insert (f, data)) fs) + #> store_termination_rule termination diff -r 5bd1a2a94e1b -r 0b14bb35be90 src/HOL/Tools/function_package/fundef_core.ML --- a/src/HOL/Tools/function_package/fundef_core.ML Fri Apr 20 00:28:07 2007 +0200 +++ b/src/HOL/Tools/function_package/fundef_core.ML Fri Apr 20 10:06:11 2007 +0200 @@ -941,7 +941,7 @@ val trsimps = if tailrec then SOME (mk_trsimps psimps) else NONE in - FundefResult {f=f, G=G, R=R, cases=complete_thm, + FundefResult {fs=[f], G=G, R=R, cases=complete_thm, psimps=psimps, subset_pinducts=[subset_pinduct], simple_pinducts=[simple_pinduct], termination=total_intro, trsimps=trsimps, domintros=dom_intros} diff -r 5bd1a2a94e1b -r 0b14bb35be90 src/HOL/Tools/function_package/fundef_datatype.ML --- a/src/HOL/Tools/function_package/fundef_datatype.ML Fri Apr 20 00:28:07 2007 +0200 +++ b/src/HOL/Tools/function_package/fundef_datatype.ML Fri Apr 20 10:06:11 2007 +0200 @@ -168,8 +168,8 @@ (Method.Basic (K pat_completeness), SOME (Method.Source_i (Args.src (("HOL.simp_all", []), Position.none)))) -fun termination_by_lexicographic_order name = - FundefPackage.setup_termination_proof (SOME name) +val termination_by_lexicographic_order = + FundefPackage.setup_termination_proof NONE #> Proof.global_terminal_proof (Method.Basic LexicographicOrder.lexicographic_order, NONE) val setup = @@ -184,8 +184,8 @@ fun fun_cmd config fixes statements lthy = lthy |> FundefPackage.add_fundef fixes statements config - ||> by_pat_completeness_simp - |-> termination_by_lexicographic_order + |> by_pat_completeness_simp + |> termination_by_lexicographic_order val funP = diff -r 5bd1a2a94e1b -r 0b14bb35be90 src/HOL/Tools/function_package/fundef_package.ML --- a/src/HOL/Tools/function_package/fundef_package.ML Fri Apr 20 00:28:07 2007 +0200 +++ b/src/HOL/Tools/function_package/fundef_package.ML Fri Apr 20 10:06:11 2007 +0200 @@ -13,13 +13,13 @@ -> ((bstring * Attrib.src list) * (string * bool)) list -> FundefCommon.fundef_config -> local_theory - -> string * Proof.state + -> Proof.state val add_fundef_i: (string * typ option * mixfix) list -> ((bstring * Attrib.src list) * (term * bool)) list -> FundefCommon.fundef_config -> local_theory - -> string * Proof.state + -> Proof.state val setup_termination_proof : string option -> local_theory -> Proof.state @@ -70,7 +70,7 @@ 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, ...} = + val FundefResult {fs, R, psimps, trsimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = cont (Goal.close_result proof) val qualify = NameSpace.qualified defname @@ -87,12 +87,12 @@ ||> fold_option (snd oo curry note_theorem (qualify "domintros", [])) domintros val cdata = FundefCtxData { add_simps=addsmps, psimps=psimps', - pinducts=snd pinducts', termination=termination', f=f, R=R } + pinducts=snd pinducts', termination=termination', fs=fs, R=R, defname=defname } val cdata' = cdata |> morph_fundef_data (LocalTheory.target_morphism lthy); (* FIXME !? *) in lthy - |> LocalTheory.declaration (fn phi => add_fundef_data defname (morph_fundef_data phi cdata)) (* save in target *) - |> Context.proof_map (add_fundef_data defname cdata') (* also save in local context *) + |> LocalTheory.declaration (fn phi => add_fundef_data (morph_fundef_data phi cdata)) (* save in target *) + |> Context.proof_map (add_fundef_data cdata') (* also save in local context *) end (* FIXME: Add cases for induct and cases thm *) @@ -129,18 +129,17 @@ val afterqed = fundef_afterqed config fixes spec defname cont sort_cont in - (defname, lthy - |> Proof.theorem_i NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]] - |> Proof.refine (Method.primitive_text (fn _ => goalstate)) |> Seq.hd) + lthy + |> Proof.theorem_i NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]] + |> Proof.refine (Method.primitive_text (fn _ => goalstate)) |> Seq.hd end -fun total_termination_afterqed defname data [[totality]] lthy = +fun total_termination_afterqed data [[totality]] lthy = let - val FundefCtxData { add_simps, psimps, pinducts, ... } = data + val FundefCtxData { add_simps, psimps, pinducts, defname, ... } = data val totality = Goal.close_result totality - |> Thm.varifyT (* FIXME ! *) val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals]) @@ -159,16 +158,16 @@ end -fun setup_termination_proof name_opt lthy = +fun setup_termination_proof term_opt lthy = let - val defname = the_default (get_last_fundef (Context.Proof lthy)) name_opt - val data = the (get_fundef_data defname (Context.Proof lthy)) - handle Option.Option => raise ERROR ("No such function definition: " ^ defname) + val data = the (case term_opt of + SOME t => import_fundef_data (ProofContext.read_term lthy t) (Context.Proof lthy) + | NONE => import_last_fundef (Context.Proof lthy)) + handle Option.Option => raise ERROR ("Not a function: " ^ quote (the_default "" term_opt)) val FundefCtxData {termination, R, ...} = data val domT = domain_type (fastype_of R) val goal = HOLogic.mk_Trueprop (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT))) - |> Type.freeze (* FIXME ! *) in lthy |> ProofContext.note_thmss_i "" [(("", [ContextRules.rule_del]), [([allI], [])])] |> snd @@ -176,8 +175,7 @@ |> ProofContext.note_thmss_i "" [(("termination", [ContextRules.intro_bang (SOME 0)]), [([Goal.norm_result termination], [])])] |> snd - |> set_termination_rule termination - |> Proof.theorem_i NONE (total_termination_afterqed defname data) [[(goal, [])]] + |> Proof.theorem_i NONE (total_termination_afterqed data) [[(goal, [])]] end @@ -230,12 +228,12 @@ OuterSyntax.command "function" "define general recursive functions" K.thy_goal (fundef_parser default_config >> (fn ((config, fixes), statements) => - Toplevel.local_theory_to_proof (target_of config) (add_fundef fixes statements config #> snd) + Toplevel.local_theory_to_proof (target_of config) (add_fundef fixes statements config) #> Toplevel.print)); val terminationP = OuterSyntax.command "termination" "prove termination of a recursive function" K.thy_goal - (P.opt_target -- Scan.option P.name + (P.opt_target -- Scan.option P.term >> (fn (target, name) => Toplevel.print o Toplevel.local_theory_to_proof target (setup_termination_proof name))); diff -r 5bd1a2a94e1b -r 0b14bb35be90 src/HOL/Tools/function_package/lexicographic_order.ML --- a/src/HOL/Tools/function_package/lexicographic_order.ML Fri Apr 20 00:28:07 2007 +0200 +++ b/src/HOL/Tools/function_package/lexicographic_order.ML Fri Apr 20 10:06:11 2007 +0200 @@ -260,13 +260,11 @@ end (* the main function: create table, search table, create relation, - and prove the subgoals *) (* FIXME proper goal addressing -- do not hardwire 1 *) + and prove the subgoals *) fun lexicographic_order_tac ctxt (st: thm) = let val thy = theory_of_thm st - val termination_thm = the (FundefCommon.get_termination_rule ctxt) - val next_st = SINGLE (rtac termination_thm 1) st |> the - val premlist = prems_of next_st + val premlist = prems_of st in case premlist of [] => error "invalid number of subgoals for this tactic - expecting at least 1 subgoal" @@ -292,7 +290,7 @@ val _ = writeln ("Instantiating R with " ^ (string_of_cterm crelterm)) val _ = writeln "Proving subgoals" in - next_st |> cterm_instantiate [(crel, crelterm)] + st |> cterm_instantiate [(crel, crelterm)] |> SINGLE (rtac wf_measures 1) |> the |> fold prove_row clean_table |> Seq.single @@ -300,7 +298,9 @@ end end -val lexicographic_order = Method.SIMPLE_METHOD o lexicographic_order_tac +(* FIXME goal addressing ?? *) +val lexicographic_order = Method.SIMPLE_METHOD o (fn ctxt => FundefCommon.apply_termination_rule ctxt 1 + THEN lexicographic_order_tac ctxt) val setup = Method.add_methods [("lexicographic_order", Method.ctxt_args lexicographic_order, "termination prover for lexicographic orderings")] diff -r 5bd1a2a94e1b -r 0b14bb35be90 src/HOL/Tools/function_package/mutual.ML --- a/src/HOL/Tools/function_package/mutual.ML Fri Apr 20 00:28:07 2007 +0200 +++ b/src/HOL/Tools/function_package/mutual.ML Fri Apr 20 10:06:11 2007 +0200 @@ -312,12 +312,13 @@ fun mk_partial_rules_mutual lthy inner_cont (m as Mutual {parts, fqgars, ...}) proof = let val result = inner_cont proof - val FundefResult {f, G, R, cases, psimps, trsimps, subset_pinducts=[subset_pinduct],simple_pinducts=[simple_pinduct], + val FundefResult {fs=[f], G, R, cases, psimps, trsimps, subset_pinducts=[subset_pinduct],simple_pinducts=[simple_pinduct], termination,domintros} = result - val all_f_defs = map (fn MutualPart {f_defthm = SOME f_def, cargTs, ...} => - mk_applied_form lthy cargTs (symmetric f_def)) - parts + val (all_f_defs, fs) = map (fn MutualPart {f_defthm = SOME f_def, f = SOME f, cargTs, ...} => + (mk_applied_form lthy cargTs (symmetric f_def), f)) + parts + |> split_list val all_orig_fdefs = map (fn MutualPart {f_defthm = SOME f_def, ...} => f_def) parts @@ -329,7 +330,7 @@ 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=f, G=G, R=R, + FundefResult { fs=fs, G=G, R=R, psimps=mpsimps, subset_pinducts=[subset_pinduct], simple_pinducts=minducts, cases=cases, termination=mtermination, domintros=domintros,