equal
deleted
inserted
replaced
|
1 (* Title: HOL/Tools/function_package/auto_term.ML |
|
2 ID: $Id$ |
|
3 Author: Alexander Krauss, TU Muenchen |
|
4 |
|
5 A package for general recursive function definitions. |
|
6 The auto_term method. |
|
7 *) |
|
8 |
|
9 |
|
10 signature FUNDEF_AUTO_TERM = |
|
11 sig |
|
12 val setup : theory -> theory |
|
13 end |
|
14 |
|
15 structure FundefAutoTerm : FUNDEF_AUTO_TERM = |
|
16 struct |
|
17 |
|
18 open FundefCommon |
|
19 open FundefAbbrev |
|
20 |
|
21 |
|
22 |
|
23 fun auto_term_tac tc_intro_rule relstr wf_rules ss = |
|
24 (resolve_tac [tc_intro_rule] 1) (* produce the usual goals *) |
|
25 THEN (instantiate_tac [("R", relstr)]) (* instantiate with the given relation *) |
|
26 THEN (ALLGOALS |
|
27 (fn 1 => ares_tac wf_rules 1 (* Solve wellfoundedness *) |
|
28 | i => asm_simp_tac ss i)) (* Simplify termination conditions *) |
|
29 |
|
30 fun mk_termination_meth relstr ctxt = |
|
31 let |
|
32 val {simps, congs, wfs} = RecdefPackage.get_local_hints ctxt |
|
33 val ss = local_simpset_of ctxt addsimps simps |
|
34 |
|
35 val intro_rule = ProofContext.get_thm ctxt (Name "termination_intro") |
|
36 in |
|
37 Method.RAW_METHOD (K (auto_term_tac |
|
38 intro_rule |
|
39 relstr |
|
40 wfs |
|
41 ss)) |
|
42 end |
|
43 |
|
44 |
|
45 |
|
46 val setup = Method.add_methods [("auto_term", Method.simple_args Args.name mk_termination_meth, "termination prover for recdef compatibility")] |
|
47 |
|
48 end |
|
49 |
|
50 |
|
51 |
|
52 |