13 end |
13 end |
14 |
14 |
15 structure FundefRelation : FUNDEF_RELATION = |
15 structure FundefRelation : FUNDEF_RELATION = |
16 struct |
16 struct |
17 |
17 |
18 fun relation_tac ctxt rel = |
18 fun inst_thm ctxt rel st = |
19 let |
19 let |
20 val cert = Thm.cterm_of (ProofContext.theory_of ctxt) |
20 val cert = Thm.cterm_of (ProofContext.theory_of ctxt) |
|
21 val rel' = cert (singleton (Variable.polymorphic ctxt) rel) |
|
22 val st' = Thm.incr_indexes (#maxidx (Thm.rep_cterm rel') + 1) st |
|
23 val Rvar = cert (Var (the_single (Term.add_vars (prop_of st') []))) |
|
24 in |
|
25 Drule.cterm_instantiate [(Rvar, rel')] st' |
|
26 end |
21 |
27 |
22 val rel' = cert (singleton (Variable.polymorphic ctxt) rel) |
28 fun relation_tac ctxt rel i = |
23 val rule = FundefCommon.get_termination_rule ctxt |> the |
29 FundefCommon.apply_termination_rule ctxt i |
24 |> Thm.incr_indexes (#maxidx (Thm.rep_cterm rel') + 1) |
30 THEN PRIMITIVE (inst_thm ctxt rel) |
25 |
|
26 val _ $ premise $ _ = Thm.prop_of rule |
|
27 val Rvar = cert (Var (the_single (Term.add_vars premise []))) |
|
28 in rtac (Drule.cterm_instantiate [(Rvar, rel')] rule) end |
|
29 |
|
30 |
31 |
31 val setup = Method.add_methods |
32 val setup = Method.add_methods |
32 [("relation", (Method.SIMPLE_METHOD' o (fn (rel, ctxt) => relation_tac ctxt rel)) oo (Method.syntax Args.term), |
33 [("relation", (Method.SIMPLE_METHOD' o (fn (rel, ctxt) => relation_tac ctxt rel)) oo (Method.syntax Args.term), |
33 "proves termination using a user-specified wellfounded relation")] |
34 "proves termination using a user-specified wellfounded relation")] |
34 |
35 |