author | wenzelm |
Fri, 13 Mar 2009 19:58:26 +0100 | |
changeset 30510 | 4120fc59dd85 |
parent 25545 | 21cd20c1ce98 |
child 30515 | bca05b17b618 |
permissions | -rw-r--r-- |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
1 |
(* Title: HOL/Tools/function_package/auto_term.ML |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
2 |
ID: $Id$ |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
3 |
Author: Alexander Krauss, TU Muenchen |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
4 |
|
20873 | 5 |
A package for general recursive function definitions. |
21319
cf814e36f788
replaced "auto_term" by the simpler method "relation", which does not try
krauss
parents:
21104
diff
changeset
|
6 |
Method "relation" to commence a termination proof using a user-specified relation. |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
7 |
*) |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
8 |
|
21319
cf814e36f788
replaced "auto_term" by the simpler method "relation", which does not try
krauss
parents:
21104
diff
changeset
|
9 |
signature FUNDEF_RELATION = |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
10 |
sig |
21588 | 11 |
val relation_tac: Proof.context -> term -> int -> tactic |
20873 | 12 |
val setup: theory -> theory |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
13 |
end |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
14 |
|
21319
cf814e36f788
replaced "auto_term" by the simpler method "relation", which does not try
krauss
parents:
21104
diff
changeset
|
15 |
structure FundefRelation : FUNDEF_RELATION = |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
16 |
struct |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
17 |
|
22733
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22496
diff
changeset
|
18 |
fun inst_thm ctxt rel st = |
21319
cf814e36f788
replaced "auto_term" by the simpler method "relation", which does not try
krauss
parents:
21104
diff
changeset
|
19 |
let |
cf814e36f788
replaced "auto_term" by the simpler method "relation", which does not try
krauss
parents:
21104
diff
changeset
|
20 |
val cert = Thm.cterm_of (ProofContext.theory_of ctxt) |
cf814e36f788
replaced "auto_term" by the simpler method "relation", which does not try
krauss
parents:
21104
diff
changeset
|
21 |
val rel' = cert (singleton (Variable.polymorphic ctxt) rel) |
22733
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22496
diff
changeset
|
22 |
val st' = Thm.incr_indexes (#maxidx (Thm.rep_cterm rel') + 1) st |
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22496
diff
changeset
|
23 |
val Rvar = cert (Var (the_single (Term.add_vars (prop_of st') []))) |
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22496
diff
changeset
|
24 |
in |
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22496
diff
changeset
|
25 |
Drule.cterm_instantiate [(Rvar, rel')] st' |
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22496
diff
changeset
|
26 |
end |
21588 | 27 |
|
22733
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22496
diff
changeset
|
28 |
fun relation_tac ctxt rel i = |
25545
21cd20c1ce98
methods "relation" and "lexicographic_order" do not insist on applying the "f.termination" rule of a function.
krauss
parents:
22733
diff
changeset
|
29 |
TRY (FundefCommon.apply_termination_rule ctxt i) |
22733
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22496
diff
changeset
|
30 |
THEN PRIMITIVE (inst_thm ctxt rel) |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
31 |
|
20295 | 32 |
val setup = Method.add_methods |
30510
4120fc59dd85
unified type Proof.method and pervasive METHOD combinators;
wenzelm
parents:
25545
diff
changeset
|
33 |
[("relation", (SIMPLE_METHOD' o (fn (rel, ctxt) => relation_tac ctxt rel)) oo (Method.syntax Args.term), |
21319
cf814e36f788
replaced "auto_term" by the simpler method "relation", which does not try
krauss
parents:
21104
diff
changeset
|
34 |
"proves termination using a user-specified wellfounded relation")] |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
35 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
36 |
end |