definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
do not depend on "termination" setup.
--- 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),
--- 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
--- 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}
--- 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 =
--- 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)));
--- 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")]
--- 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,