renamed auto_term.ML -> relation.ML
authorkrauss
Fri Oct 23 16:37:56 2009 +0200 (2009-10-23)
changeset 33100acc2bd3934ba
parent 33099 b8cdd3d73022
child 33101 8846318b52d0
renamed auto_term.ML -> relation.ML
src/HOL/FunDef.thy
src/HOL/IsaMakefile
src/HOL/Tools/Function/auto_term.ML
src/HOL/Tools/Function/relation.ML
     1.1 --- a/src/HOL/FunDef.thy	Fri Oct 23 16:22:10 2009 +0200
     1.2 +++ b/src/HOL/FunDef.thy	Fri Oct 23 16:37:56 2009 +0200
     1.3 @@ -18,7 +18,7 @@
     1.4    ("Tools/Function/mutual.ML")
     1.5    ("Tools/Function/pattern_split.ML")
     1.6    ("Tools/Function/function.ML")
     1.7 -  ("Tools/Function/auto_term.ML")
     1.8 +  ("Tools/Function/relation.ML")
     1.9    ("Tools/Function/measure_functions.ML")
    1.10    ("Tools/Function/lexicographic_order.ML")
    1.11    ("Tools/Function/pat_completeness.ML")
    1.12 @@ -112,7 +112,7 @@
    1.13  use "Tools/Function/sum_tree.ML"
    1.14  use "Tools/Function/mutual.ML"
    1.15  use "Tools/Function/pattern_split.ML"
    1.16 -use "Tools/Function/auto_term.ML"
    1.17 +use "Tools/Function/relation.ML"
    1.18  use "Tools/Function/function.ML"
    1.19  use "Tools/Function/pat_completeness.ML"
    1.20  use "Tools/Function/fun.ML"
     2.1 --- a/src/HOL/IsaMakefile	Fri Oct 23 16:22:10 2009 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Fri Oct 23 16:37:56 2009 +0200
     2.3 @@ -156,7 +156,6 @@
     2.4    Tools/Datatype/datatype_realizer.ML \
     2.5    Tools/Datatype/datatype_rep_proofs.ML \
     2.6    Tools/dseq.ML \
     2.7 -  Tools/Function/auto_term.ML \
     2.8    Tools/Function/context_tree.ML \
     2.9    Tools/Function/decompose.ML \
    2.10    Tools/Function/descent.ML \
    2.11 @@ -172,6 +171,7 @@
    2.12    Tools/Function/mutual.ML \
    2.13    Tools/Function/pat_completeness.ML \
    2.14    Tools/Function/pattern_split.ML \
    2.15 +  Tools/Function/relation.ML \
    2.16    Tools/Function/scnp_reconstruct.ML \
    2.17    Tools/Function/scnp_solve.ML \
    2.18    Tools/Function/size.ML \
     3.1 --- a/src/HOL/Tools/Function/auto_term.ML	Fri Oct 23 16:22:10 2009 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,36 +0,0 @@
     3.4 -(*  Title:      HOL/Tools/Function/auto_term.ML
     3.5 -    Author:     Alexander Krauss, TU Muenchen
     3.6 -
     3.7 -A package for general recursive function definitions.
     3.8 -Method "relation" to commence a termination proof using a user-specified relation.
     3.9 -*)
    3.10 -
    3.11 -signature FUNCTION_RELATION =
    3.12 -sig
    3.13 -  val relation_tac: Proof.context -> term -> int -> tactic
    3.14 -  val setup: theory -> theory
    3.15 -end
    3.16 -
    3.17 -structure Function_Relation : FUNCTION_RELATION =
    3.18 -struct
    3.19 -
    3.20 -fun inst_thm ctxt rel st =
    3.21 -    let
    3.22 -      val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
    3.23 -      val rel' = cert (singleton (Variable.polymorphic ctxt) rel)
    3.24 -      val st' = Thm.incr_indexes (#maxidx (Thm.rep_cterm rel') + 1) st
    3.25 -      val Rvar = cert (Var (the_single (Term.add_vars (prop_of st') [])))
    3.26 -    in 
    3.27 -      Drule.cterm_instantiate [(Rvar, rel')] st' 
    3.28 -    end
    3.29 -
    3.30 -fun relation_tac ctxt rel i = 
    3.31 -    TRY (Function_Common.apply_termination_rule ctxt i)
    3.32 -    THEN PRIMITIVE (inst_thm ctxt rel)
    3.33 -
    3.34 -val setup =
    3.35 -  Method.setup @{binding relation}
    3.36 -    (Args.term >> (fn rel => fn ctxt => SIMPLE_METHOD' (relation_tac ctxt rel)))
    3.37 -    "proves termination using a user-specified wellfounded relation"
    3.38 -
    3.39 -end
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Tools/Function/relation.ML	Fri Oct 23 16:37:56 2009 +0200
     4.3 @@ -0,0 +1,36 @@
     4.4 +(*  Title:      HOL/Tools/Function/relation.ML
     4.5 +    Author:     Alexander Krauss, TU Muenchen
     4.6 +
     4.7 +A package for general recursive function definitions.
     4.8 +Method "relation" to commence a termination proof using a user-specified relation.
     4.9 +*)
    4.10 +
    4.11 +signature FUNCTION_RELATION =
    4.12 +sig
    4.13 +  val relation_tac: Proof.context -> term -> int -> tactic
    4.14 +  val setup: theory -> theory
    4.15 +end
    4.16 +
    4.17 +structure Function_Relation : FUNCTION_RELATION =
    4.18 +struct
    4.19 +
    4.20 +fun inst_thm ctxt rel st =
    4.21 +    let
    4.22 +      val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
    4.23 +      val rel' = cert (singleton (Variable.polymorphic ctxt) rel)
    4.24 +      val st' = Thm.incr_indexes (#maxidx (Thm.rep_cterm rel') + 1) st
    4.25 +      val Rvar = cert (Var (the_single (Term.add_vars (prop_of st') [])))
    4.26 +    in 
    4.27 +      Drule.cterm_instantiate [(Rvar, rel')] st' 
    4.28 +    end
    4.29 +
    4.30 +fun relation_tac ctxt rel i = 
    4.31 +    TRY (Function_Common.apply_termination_rule ctxt i)
    4.32 +    THEN PRIMITIVE (inst_thm ctxt rel)
    4.33 +
    4.34 +val setup =
    4.35 +  Method.setup @{binding relation}
    4.36 +    (Args.term >> (fn rel => fn ctxt => SIMPLE_METHOD' (relation_tac ctxt rel)))
    4.37 +    "proves termination using a user-specified wellfounded relation"
    4.38 +
    4.39 +end