1 (* Title: HOL/Tools/function_package/termination.ML |
|
2 ID: $Id$ |
|
3 Author: Alexander Krauss, TU Muenchen |
|
4 |
|
5 A package for general recursive function definitions. |
|
6 Termination goals... |
|
7 *) |
|
8 |
|
9 |
|
10 signature FUNDEF_TERMINATION = |
|
11 sig |
|
12 val mk_total_termination_goal : term -> term |
|
13 (* val mk_partial_termination_goal : theory -> FundefCommon.result_with_names -> string -> term * term*) |
|
14 end |
|
15 |
|
16 structure FundefTermination : FUNDEF_TERMINATION = |
|
17 struct |
|
18 |
|
19 |
|
20 open FundefLib |
|
21 open FundefCommon |
|
22 open FundefAbbrev |
|
23 |
|
24 fun mk_total_termination_goal R = |
|
25 let |
|
26 val domT = domain_type (fastype_of R) |
|
27 val x = Free ("x", domT) |
|
28 in |
|
29 mk_forall x (Trueprop (mk_acc domT R $ x)) |
|
30 end |
|
31 |
|
32 (* |
|
33 fun mk_partial_termination_goal thy (FundefMResult {R, f, ... }, _, _) dom = |
|
34 let |
|
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 |
|
50 |
|
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 |
|
56 in |
|
57 (subs, dcl) |
|
58 end |
|
59 *) |
|
60 end |
|
61 |
|
62 |
|
63 |
|
64 |
|