--- a/src/HOL/FunDef.thy Fri Oct 23 16:22:10 2009 +0200
+++ b/src/HOL/FunDef.thy Fri Oct 23 16:37:56 2009 +0200
@@ -18,7 +18,7 @@
("Tools/Function/mutual.ML")
("Tools/Function/pattern_split.ML")
("Tools/Function/function.ML")
- ("Tools/Function/auto_term.ML")
+ ("Tools/Function/relation.ML")
("Tools/Function/measure_functions.ML")
("Tools/Function/lexicographic_order.ML")
("Tools/Function/pat_completeness.ML")
@@ -112,7 +112,7 @@
use "Tools/Function/sum_tree.ML"
use "Tools/Function/mutual.ML"
use "Tools/Function/pattern_split.ML"
-use "Tools/Function/auto_term.ML"
+use "Tools/Function/relation.ML"
use "Tools/Function/function.ML"
use "Tools/Function/pat_completeness.ML"
use "Tools/Function/fun.ML"
--- a/src/HOL/IsaMakefile Fri Oct 23 16:22:10 2009 +0200
+++ b/src/HOL/IsaMakefile Fri Oct 23 16:37:56 2009 +0200
@@ -156,7 +156,6 @@
Tools/Datatype/datatype_realizer.ML \
Tools/Datatype/datatype_rep_proofs.ML \
Tools/dseq.ML \
- Tools/Function/auto_term.ML \
Tools/Function/context_tree.ML \
Tools/Function/decompose.ML \
Tools/Function/descent.ML \
@@ -172,6 +171,7 @@
Tools/Function/mutual.ML \
Tools/Function/pat_completeness.ML \
Tools/Function/pattern_split.ML \
+ Tools/Function/relation.ML \
Tools/Function/scnp_reconstruct.ML \
Tools/Function/scnp_solve.ML \
Tools/Function/size.ML \
--- a/src/HOL/Tools/Function/auto_term.ML Fri Oct 23 16:22:10 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,36 +0,0 @@
-(* Title: HOL/Tools/Function/auto_term.ML
- Author: Alexander Krauss, TU Muenchen
-
-A package for general recursive function definitions.
-Method "relation" to commence a termination proof using a user-specified relation.
-*)
-
-signature FUNCTION_RELATION =
-sig
- val relation_tac: Proof.context -> term -> int -> tactic
- val setup: theory -> theory
-end
-
-structure Function_Relation : FUNCTION_RELATION =
-struct
-
-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 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
-
-fun relation_tac ctxt rel i =
- TRY (Function_Common.apply_termination_rule ctxt i)
- THEN PRIMITIVE (inst_thm ctxt rel)
-
-val setup =
- Method.setup @{binding relation}
- (Args.term >> (fn rel => fn ctxt => SIMPLE_METHOD' (relation_tac ctxt rel)))
- "proves termination using a user-specified wellfounded relation"
-
-end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Function/relation.ML Fri Oct 23 16:37:56 2009 +0200
@@ -0,0 +1,36 @@
+(* Title: HOL/Tools/Function/relation.ML
+ Author: Alexander Krauss, TU Muenchen
+
+A package for general recursive function definitions.
+Method "relation" to commence a termination proof using a user-specified relation.
+*)
+
+signature FUNCTION_RELATION =
+sig
+ val relation_tac: Proof.context -> term -> int -> tactic
+ val setup: theory -> theory
+end
+
+structure Function_Relation : FUNCTION_RELATION =
+struct
+
+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 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
+
+fun relation_tac ctxt rel i =
+ TRY (Function_Common.apply_termination_rule ctxt i)
+ THEN PRIMITIVE (inst_thm ctxt rel)
+
+val setup =
+ Method.setup @{binding relation}
+ (Args.term >> (fn rel => fn ctxt => SIMPLE_METHOD' (relation_tac ctxt rel)))
+ "proves termination using a user-specified wellfounded relation"
+
+end