1 (* Title: HOL/Tools/function_package/auto_term.ML |
1 (* Title: HOL/Tools/function_package/auto_term.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Alexander Krauss, TU Muenchen |
3 Author: Alexander Krauss, TU Muenchen |
4 |
4 |
5 A package for general recursive function definitions. |
5 A package for general recursive function definitions. |
6 The auto_term method. |
6 The auto_term method. |
7 *) |
7 *) |
8 |
8 |
9 |
9 |
10 signature FUNDEF_AUTO_TERM = |
10 signature FUNDEF_AUTO_TERM = |
11 sig |
11 sig |
12 val setup : theory -> theory |
12 val setup: theory -> theory |
13 end |
13 end |
14 |
14 |
15 structure FundefAutoTerm : FUNDEF_AUTO_TERM = |
15 structure FundefAutoTerm : FUNDEF_AUTO_TERM = |
16 struct |
16 struct |
17 |
17 |
18 open FundefCommon |
18 open FundefCommon |
19 open FundefAbbrev |
19 open FundefAbbrev |
20 |
20 |
21 |
21 |
|
22 fun auto_term_tac ctxt rule rel wf_rules ss = |
|
23 let |
|
24 val cert = Thm.cterm_of (ProofContext.theory_of ctxt) |
22 |
25 |
23 fun auto_term_tac tc_intro_rule relstr wf_rules ss = |
26 val rel' = cert (singleton (Variable.polymorphic ctxt) rel) |
24 (resolve_tac [tc_intro_rule] 1) (* produce the usual goals *) |
27 val rule' = rule |> Thm.incr_indexes (#maxidx (Thm.rep_cterm rel') + 1) |
25 THEN (instantiate_tac [("R", relstr)]) (* instantiate with the given relation *) |
28 val prem = #1 (Logic.dest_implies (Thm.prop_of rule')) |
26 THEN (ALLGOALS |
29 val R' = cert (Var (the_single (Term.add_vars prem []))) |
27 (fn 1 => REPEAT (ares_tac wf_rules 1) (* Solve wellfoundedness *) |
30 in |
28 | i => asm_simp_tac ss i)) (* Simplify termination conditions *) |
31 resolve_tac [Drule.cterm_instantiate [(R', rel')] rule'] 1 (* produce the usual goals *) |
29 |
32 THEN (ALLGOALS |
30 fun mk_termination_meth relstr ctxt = |
33 (fn 1 => REPEAT (ares_tac wf_rules 1) (* Solve wellfoundedness *) |
31 let |
34 | i => asm_simp_tac ss i)) (* Simplify termination conditions *) |
32 val {simps, congs, wfs} = RecdefPackage.get_hints (Context.Proof ctxt) |
35 end |
33 val ss = local_simpset_of ctxt addsimps simps |
|
34 |
|
35 val intro_rule = ProofContext.get_thm ctxt (Name "termination") |
|
36 (* FIXME avoid internal name lookup -- dynamic scoping! *) |
|
37 in |
|
38 Method.RAW_METHOD (K (auto_term_tac |
|
39 intro_rule |
|
40 relstr |
|
41 wfs |
|
42 ss)) |
|
43 end |
|
44 |
36 |
45 |
37 |
|
38 fun termination_meth src = Method.syntax Args.term src #> (fn (ctxt, rel) => |
|
39 let |
|
40 val {simps, congs, wfs} = RecdefPackage.get_hints (Context.Proof ctxt) |
|
41 val ss = local_simpset_of ctxt addsimps simps |
|
42 |
|
43 val intro_rule = ProofContext.get_thm ctxt (Name "termination") |
|
44 (* FIXME avoid internal name lookup -- dynamic scoping! *) |
|
45 in Method.RAW_METHOD (K (auto_term_tac ctxt intro_rule rel wfs ss)) end) |
46 |
46 |
47 val setup = Method.add_methods |
47 val setup = Method.add_methods |
48 [("auto_term", Method.simple_args Args.name mk_termination_meth, |
48 [("auto_term", termination_meth, "termination prover for recdef compatibility")] |
49 "termination prover for recdef compatibility")] |
|
50 |
49 |
51 end |
50 end |