equal
deleted
inserted
replaced
1 (* Title: HOL/Tools/Function/auto_term.ML |
|
2 Author: Alexander Krauss, TU Muenchen |
|
3 |
|
4 A package for general recursive function definitions. |
|
5 Method "relation" to commence a termination proof using a user-specified relation. |
|
6 *) |
|
7 |
|
8 signature FUNDEF_RELATION = |
|
9 sig |
|
10 val relation_tac: Proof.context -> term -> int -> tactic |
|
11 val setup: theory -> theory |
|
12 end |
|
13 |
|
14 structure FundefRelation : FUNDEF_RELATION = |
|
15 struct |
|
16 |
|
17 fun inst_thm ctxt rel st = |
|
18 let |
|
19 val cert = Thm.cterm_of (ProofContext.theory_of ctxt) |
|
20 val rel' = cert (singleton (Variable.polymorphic ctxt) rel) |
|
21 val st' = Thm.incr_indexes (#maxidx (Thm.rep_cterm rel') + 1) st |
|
22 val Rvar = cert (Var (the_single (Term.add_vars (prop_of st') []))) |
|
23 in |
|
24 Drule.cterm_instantiate [(Rvar, rel')] st' |
|
25 end |
|
26 |
|
27 fun relation_tac ctxt rel i = |
|
28 TRY (FundefCommon.apply_termination_rule ctxt i) |
|
29 THEN PRIMITIVE (inst_thm ctxt rel) |
|
30 |
|
31 val setup = |
|
32 Method.setup @{binding relation} |
|
33 (Args.term >> (fn rel => fn ctxt => SIMPLE_METHOD' (relation_tac ctxt rel))) |
|
34 "proves termination using a user-specified wellfounded relation" |
|
35 |
|
36 end |
|