author | wenzelm |
Wed, 15 Nov 2006 20:50:22 +0100 | |
changeset 21391 | a8809f46bd7f |
parent 21255 | 617fdb08abe9 |
child 22166 | 0a50d4db234a |
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/termination.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 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
5 |
A package for general recursive function definitions. |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
6 |
Termination goals... |
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 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
9 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
10 |
signature FUNDEF_TERMINATION = |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
11 |
sig |
21255
617fdb08abe9
added profiling code, improved handling of proof terms, generation of domain
krauss
parents:
21237
diff
changeset
|
12 |
val mk_total_termination_goal : term -> term -> term |
617fdb08abe9
added profiling code, improved handling of proof terms, generation of domain
krauss
parents:
21237
diff
changeset
|
13 |
(* val mk_partial_termination_goal : theory -> FundefCommon.result_with_names -> string -> term * term*) |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
14 |
end |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
15 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
16 |
structure FundefTermination : FUNDEF_TERMINATION = |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
17 |
struct |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
18 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
19 |
|
21051
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20523
diff
changeset
|
20 |
open FundefLib |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
21 |
open FundefCommon |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
22 |
open FundefAbbrev |
21237 | 23 |
|
21255
617fdb08abe9
added profiling code, improved handling of proof terms, generation of domain
krauss
parents:
21237
diff
changeset
|
24 |
fun mk_total_termination_goal f R = |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
25 |
let |
21237 | 26 |
val domT = domain_type (fastype_of f) |
27 |
val x = Free ("x", domT) |
|
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
28 |
in |
21104 | 29 |
mk_forall x (Trueprop (mk_acc domT R $ x)) |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
30 |
end |
21237 | 31 |
|
21255
617fdb08abe9
added profiling code, improved handling of proof terms, generation of domain
krauss
parents:
21237
diff
changeset
|
32 |
(* |
20270
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19806
diff
changeset
|
33 |
fun mk_partial_termination_goal thy (FundefMResult {R, f, ... }, _, _) dom = |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
34 |
let |
21237 | 35 |
val domT = domain_type (fastype_of f) |
36 |
val D = Sign.simple_read_term thy (Logic.varifyT (HOLogic.mk_setT domT)) dom |
|
37 |
val DT = type_of D |
|
38 |
val idomT = HOLogic.dest_setT DT |
|
39 |
||
40 |
val x = Free ("x", idomT) |
|
41 |
val z = Free ("z", idomT) |
|
42 |
val Rname = fst (dest_Const R) |
|
43 |
val iRT = mk_relT (idomT, idomT) |
|
44 |
val iR = Const (Rname, iRT) |
|
45 |
||
46 |
val subs = HOLogic.mk_Trueprop |
|
47 |
(Const ("Orderings.less_eq", DT --> DT --> boolT) $ D $ |
|
48 |
(Const (acc_const_name, iRT --> DT) $ iR)) |
|
49 |
|> Type.freeze |
|
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
50 |
|
21237 | 51 |
val dcl = mk_forall x |
52 |
(mk_forall z (Logic.mk_implies (Trueprop (HOLogic.mk_mem (x, D)), |
|
53 |
Logic.mk_implies (mk_relmem (z, x) iR, |
|
54 |
Trueprop (mk_mem (z, D)))))) |
|
55 |
|> Type.freeze |
|
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
56 |
in |
21237 | 57 |
(subs, dcl) |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
58 |
end |
21255
617fdb08abe9
added profiling code, improved handling of proof terms, generation of domain
krauss
parents:
21237
diff
changeset
|
59 |
*) |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
60 |
end |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
61 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
62 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
63 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
64 |