# HG changeset patch # User krauss # Date 1171557319 -3600 # Node ID be61bd159a999c00eda6fdd99dfa92753b8adf04 # Parent c95319d143322b39c1011eb64f45677bc5edb442 changed termination goal to use object quantifier diff -r c95319d14332 -r be61bd159a99 src/HOL/FunDef.thy --- a/src/HOL/FunDef.thy Thu Feb 15 12:14:34 2007 +0100 +++ b/src/HOL/FunDef.thy Thu Feb 15 17:35:19 2007 +0100 @@ -14,7 +14,6 @@ ("Tools/function_package/inductive_wrap.ML") ("Tools/function_package/context_tree.ML") ("Tools/function_package/fundef_core.ML") -("Tools/function_package/termination.ML") ("Tools/function_package/mutual.ML") ("Tools/function_package/pattern_split.ML") ("Tools/function_package/fundef_package.ML") @@ -109,7 +108,6 @@ use "Tools/function_package/inductive_wrap.ML" use "Tools/function_package/context_tree.ML" use "Tools/function_package/fundef_core.ML" -use "Tools/function_package/termination.ML" use "Tools/function_package/mutual.ML" use "Tools/function_package/pattern_split.ML" use "Tools/function_package/auto_term.ML" diff -r c95319d14332 -r be61bd159a99 src/HOL/Tools/function_package/fundef_core.ML --- a/src/HOL/Tools/function_package/fundef_core.ML Thu Feb 15 12:14:34 2007 +0100 +++ b/src/HOL/Tools/function_package/fundef_core.ML Thu Feb 15 17:35:19 2007 +0100 @@ -758,8 +758,8 @@ in FundefCtxTree.traverse_tree step tree end - - + + fun mk_nest_term_rule thy globals R R_cases clauses = let val Globals { domT, x, z, ... } = globals @@ -797,6 +797,8 @@ |> forall_intr (cterm_of thy x) |> (fn it => Drule.compose_single(it,2,wf_induct_rule)) |> curry op RS (assume wfR') + |> forall_intr_vars + |> (fn it => it COMP allI) |> fold implies_intr hyps |> implies_intr wfR' |> forall_intr (cterm_of thy R') diff -r c95319d14332 -r be61bd159a99 src/HOL/Tools/function_package/fundef_package.ML --- a/src/HOL/Tools/function_package/fundef_package.ML Thu Feb 15 12:14:34 2007 +0100 +++ b/src/HOL/Tools/function_package/fundef_package.ML Thu Feb 15 17:35:19 2007 +0100 @@ -166,11 +166,14 @@ handle Option.Option => raise ERROR ("No such function definition: " ^ defname) val FundefCtxData {termination, R, ...} = data - val goal = FundefTermination.mk_total_termination_goal R + val domT = domain_type (fastype_of R) + val goal = HOLogic.mk_Trueprop (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT))) in lthy + |> ProofContext.note_thmss_i "" [(("", [ContextRules.rule_del]), [([allI], [])])] |> snd + |> ProofContext.note_thmss_i "" [(("", [ContextRules.intro_bang (SOME 1)]), [([allI], [])])] |> snd |> ProofContext.note_thmss_i "" - [(("termination", [ContextRules.intro_query NONE]), + [(("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, [])]] diff -r c95319d14332 -r be61bd159a99 src/HOL/Tools/function_package/lexicographic_order.ML --- a/src/HOL/Tools/function_package/lexicographic_order.ML Thu Feb 15 12:14:34 2007 +0100 +++ b/src/HOL/Tools/function_package/lexicographic_order.ML Thu Feb 15 17:35:19 2007 +0100 @@ -270,11 +270,11 @@ in case premlist of [] => error "invalid number of subgoals for this tactic - expecting at least 1 subgoal" - | (wf::tl) => let - val (var, prop) = FundefLib.dest_all wf - val rel = HOLogic.dest_Trueprop prop |> dest_wf |> head_of + | (wfR::tl) => let + val trueprop $ (wf $ rel) = wfR val crel = cterm_of thy rel - val measure_funs = mk_all_measure_funs (fastype_of var) + val (domT, _) = HOLogic.dest_prodT (HOLogic.dest_setT (fastype_of rel)) + val measure_funs = mk_all_measure_funs domT val _ = writeln "Creating table" val table = map (mk_row thy measure_funs) tl val _ = writeln "Searching for lexicographic order" @@ -286,8 +286,8 @@ | SOME order => let val clean_table = map (fn x => map (nth x) order) table val funs = map (nth measure_funs) order - val list = HOLogic.mk_list (fastype_of var --> HOLogic.natT) funs - val relterm = Abs ("x", fastype_of var, Const(measures, (fastype_of list) --> (range_type (fastype_of rel))) $ list) + val list = HOLogic.mk_list (domT --> HOLogic.natT) funs + val relterm = Const(measures, (fastype_of list) --> (fastype_of rel)) $ list val crelterm = cterm_of thy relterm val _ = writeln ("Instantiating R with " ^ (string_of_cterm crelterm)) val _ = writeln "Proving subgoals" diff -r c95319d14332 -r be61bd159a99 src/HOL/Tools/function_package/termination.ML --- a/src/HOL/Tools/function_package/termination.ML Thu Feb 15 12:14:34 2007 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,64 +0,0 @@ -(* Title: HOL/Tools/function_package/termination.ML - ID: $Id$ - Author: Alexander Krauss, TU Muenchen - -A package for general recursive function definitions. -Termination goals... -*) - - -signature FUNDEF_TERMINATION = -sig - val mk_total_termination_goal : term -> term -(* val mk_partial_termination_goal : theory -> FundefCommon.result_with_names -> string -> term * term*) -end - -structure FundefTermination : FUNDEF_TERMINATION = -struct - - -open FundefLib -open FundefCommon -open FundefAbbrev - -fun mk_total_termination_goal R = - let - val domT = domain_type (fastype_of R) - val x = Free ("x", domT) - in - mk_forall x (Trueprop (mk_acc domT R $ x)) - end - -(* -fun mk_partial_termination_goal thy (FundefMResult {R, f, ... }, _, _) dom = - let - val domT = domain_type (fastype_of f) - val D = Sign.simple_read_term thy (Logic.varifyT (HOLogic.mk_setT domT)) dom - val DT = type_of D - val idomT = HOLogic.dest_setT DT - - val x = Free ("x", idomT) - val z = Free ("z", idomT) - val Rname = fst (dest_Const R) - val iRT = mk_relT (idomT, idomT) - val iR = Const (Rname, iRT) - - val subs = HOLogic.mk_Trueprop - (Const ("Orderings.less_eq", DT --> DT --> boolT) $ D $ - (Const (acc_const_name, iRT --> DT) $ iR)) - |> Type.freeze - - val dcl = mk_forall x - (mk_forall z (Logic.mk_implies (Trueprop (HOLogic.mk_mem (x, D)), - Logic.mk_implies (mk_relmem (z, x) iR, - Trueprop (mk_mem (z, D)))))) - |> Type.freeze - in - (subs, dcl) - end -*) -end - - - -