--- 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"
--- 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')
--- 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, [])]]
--- 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"
--- 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
-
-
-
-