|
33100
|
1 |
(* Title: HOL/Tools/Function/relation.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 FUNCTION_RELATION =
|
|
|
9 |
sig
|
|
|
10 |
val relation_tac: Proof.context -> term -> int -> tactic
|
|
|
11 |
val setup: theory -> theory
|
|
|
12 |
end
|
|
|
13 |
|
|
|
14 |
structure Function_Relation : FUNCTION_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 (Function_Common.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
|