author  krauss 
Wed, 05 Dec 2007 14:36:58 +0100  
changeset 25545  21cd20c1ce98 
parent 22733  0b14bb35be90 
child 30510  4120fc59dd85 
permissions  rwrr 
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 userspecified 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 
21879  33 
[("relation", (Method.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 userspecified 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 