author | krauss |
Sat, 02 Jan 2010 23:18:58 +0100 | |
changeset 34232 | 36a2a3029fd3 |
parent 34229 | f66bb6536f6a |
child 34236 | 010a3206cbbe |
permissions | -rw-r--r-- |
31775 | 1 |
(* Title: HOL/Tools/Function/termination.ML |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
2 |
Author: Alexander Krauss, TU Muenchen |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
3 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
4 |
Context data for termination proofs |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
5 |
*) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
6 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
7 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
8 |
signature TERMINATION = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
9 |
sig |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
10 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
11 |
type data |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
12 |
datatype cell = Less of thm | LessEq of (thm * thm) | None of (thm * thm) | False of thm |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
13 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
14 |
val mk_sumcases : data -> typ -> term list -> term |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
15 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
16 |
val get_num_points : data -> int |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
17 |
val get_types : data -> int -> typ |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
18 |
val get_measures : data -> int -> term list |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
19 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
20 |
(* read from cache *) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
21 |
val get_chain : data -> term -> term -> thm option option |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
22 |
val get_descent : data -> term -> term -> term -> cell option |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
23 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
24 |
val dest_call : data -> term -> ((string * typ) list * int * term * int * term * term) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
25 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
26 |
val CALLS : (term list * int -> tactic) -> int -> tactic |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
27 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
28 |
(* Termination tactics. Sequential composition via continuations. (2nd argument is the error continuation) *) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
29 |
type ttac = (data -> int -> tactic) -> (data -> int -> tactic) -> data -> int -> tactic |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
30 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
31 |
val TERMINATION : Proof.context -> (data -> int -> tactic) -> int -> tactic |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
32 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
33 |
val REPEAT : ttac -> ttac |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
34 |
|
30607
c3d1590debd8
eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
wenzelm
parents:
30304
diff
changeset
|
35 |
val wf_union_tac : Proof.context -> tactic |
34228
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
36 |
|
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
37 |
val decompose_tac : Proof.context -> tactic -> ttac |
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
38 |
|
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
39 |
val derive_diag : Proof.context -> tactic -> |
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
40 |
(data -> int -> tactic) -> data -> int -> tactic |
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
41 |
|
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
42 |
val derive_all : Proof.context -> tactic -> |
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
43 |
(data -> int -> tactic) -> data -> int -> tactic |
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
44 |
|
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
45 |
end |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
46 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
47 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
48 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
49 |
structure Termination : TERMINATION = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
50 |
struct |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
51 |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
32683
diff
changeset
|
52 |
open Function_Lib |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
53 |
|
29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
29125
diff
changeset
|
54 |
val term2_ord = prod_ord TermOrd.fast_term_ord TermOrd.fast_term_ord |
31971
8c1b845ed105
renamed functor TableFun to Table, and GraphFun to Graph;
wenzelm
parents:
31775
diff
changeset
|
55 |
structure Term2tab = Table(type key = term * term val ord = term2_ord); |
8c1b845ed105
renamed functor TableFun to Table, and GraphFun to Graph;
wenzelm
parents:
31775
diff
changeset
|
56 |
structure Term3tab = Table(type key = term * (term * term) val ord = prod_ord TermOrd.fast_term_ord term2_ord); |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
57 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
58 |
(** Analyzing binary trees **) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
59 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
60 |
(* Skeleton of a tree structure *) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
61 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
62 |
datatype skel = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
63 |
SLeaf of int (* index *) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
64 |
| SBranch of (skel * skel) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
65 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
66 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
67 |
(* abstract make and dest functions *) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
68 |
fun mk_tree leaf branch = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
69 |
let fun mk (SLeaf i) = leaf i |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
70 |
| mk (SBranch (s, t)) = branch (mk s, mk t) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
71 |
in mk end |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
72 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
73 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
74 |
fun dest_tree split = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
75 |
let fun dest (SLeaf i) x = [(i, x)] |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
76 |
| dest (SBranch (s, t)) x = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
77 |
let val (l, r) = split x |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
78 |
in dest s l @ dest t r end |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
79 |
in dest end |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
80 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
81 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
82 |
(* concrete versions for sum types *) |
32602 | 83 |
fun is_inj (Const (@{const_name Sum_Type.Inl}, _) $ _) = true |
84 |
| is_inj (Const (@{const_name Sum_Type.Inr}, _) $ _) = true |
|
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
85 |
| is_inj _ = false |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
86 |
|
32602 | 87 |
fun dest_inl (Const (@{const_name Sum_Type.Inl}, _) $ t) = SOME t |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
88 |
| dest_inl _ = NONE |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
89 |
|
32602 | 90 |
fun dest_inr (Const (@{const_name Sum_Type.Inr}, _) $ t) = SOME t |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
91 |
| dest_inr _ = NONE |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
92 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
93 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
94 |
fun mk_skel ps = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
95 |
let |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
96 |
fun skel i ps = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
97 |
if forall is_inj ps andalso not (null ps) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
98 |
then let |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
99 |
val (j, s) = skel i (map_filter dest_inl ps) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
100 |
val (k, t) = skel j (map_filter dest_inr ps) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
101 |
in (k, SBranch (s, t)) end |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
102 |
else (i + 1, SLeaf i) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
103 |
in |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
104 |
snd (skel 0 ps) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
105 |
end |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
106 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
107 |
(* compute list of types for nodes *) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
108 |
fun node_types sk T = dest_tree (fn Type ("+", [LT, RT]) => (LT, RT)) sk T |> map snd |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
109 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
110 |
(* find index and raw term *) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
111 |
fun dest_inj (SLeaf i) trm = (i, trm) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
112 |
| dest_inj (SBranch (s, t)) trm = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
113 |
case dest_inl trm of |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
114 |
SOME trm' => dest_inj s trm' |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
115 |
| _ => dest_inj t (the (dest_inr trm)) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
116 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
117 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
118 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
119 |
(** Matrix cell datatype **) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
120 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
121 |
datatype cell = Less of thm | LessEq of (thm * thm) | None of (thm * thm) | False of thm; |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
122 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
123 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
124 |
type data = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
125 |
skel (* structure of the sum type encoding "program points" *) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
126 |
* (int -> typ) (* types of program points *) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
127 |
* (term list Inttab.table) (* measures for program points *) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
128 |
* (thm option Term2tab.table) (* which calls form chains? *) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
129 |
* (cell Term3tab.table) (* local descents *) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
130 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
131 |
|
34228
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
132 |
fun map_chains f (p, T, M, C, D) = (p, T, M, f C, D) |
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
133 |
fun map_descent f (p, T, M, C, D) = (p, T, M, C, f D) |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
134 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
135 |
fun note_chain c1 c2 res = map_chains (Term2tab.update ((c1, c2), res)) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
136 |
fun note_descent c m1 m2 res = map_descent (Term3tab.update ((c,(m1, m2)), res)) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
137 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
138 |
(* Build case expression *) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
139 |
fun mk_sumcases (sk, _, _, _, _) T fs = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
140 |
mk_tree (fn i => (nth fs i, domain_type (fastype_of (nth fs i)))) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
141 |
(fn ((f, fT), (g, gT)) => (SumTree.mk_sumcase fT gT T f g, SumTree.mk_sumT fT gT)) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
142 |
sk |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
143 |
|> fst |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
144 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
145 |
fun mk_sum_skel rel = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
146 |
let |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
32683
diff
changeset
|
147 |
val cs = Function_Lib.dest_binop_list @{const_name Lattices.sup} rel |
32602 | 148 |
fun collect_pats (Const (@{const_name Collect}, _) $ Abs (_, _, c)) = |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
149 |
let |
33855
cd8acf137c9c
eliminated dead code and some unused bindings, reported by polyml
krauss
parents:
33099
diff
changeset
|
150 |
val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const ("Pair", _) $ r $ l)) $ _) |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
151 |
= Term.strip_qnt_body "Ex" c |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
152 |
in cons r o cons l end |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
153 |
in |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
154 |
mk_skel (fold collect_pats cs []) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
155 |
end |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
156 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
157 |
fun create ctxt T rel = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
158 |
let |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
159 |
val sk = mk_sum_skel rel |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
160 |
val Ts = node_types sk T |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
161 |
val M = Inttab.make (map_index (apsnd (MeasureFunctions.get_measure_functions ctxt)) Ts) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
162 |
in |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
163 |
(sk, nth Ts, M, Term2tab.empty, Term3tab.empty) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
164 |
end |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
165 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
166 |
fun get_num_points (sk, _, _, _, _) = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
167 |
let |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
168 |
fun num (SLeaf i) = i + 1 |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
169 |
| num (SBranch (s, t)) = num t |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
170 |
in num sk end |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
171 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
172 |
fun get_types (_, T, _, _, _) = T |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
173 |
fun get_measures (_, _, M, _, _) = Inttab.lookup_list M |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
174 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
175 |
fun get_chain (_, _, _, C, _) c1 c2 = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
176 |
Term2tab.lookup C (c1, c2) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
177 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
178 |
fun get_descent (_, _, _, _, D) c m1 m2 = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
179 |
Term3tab.lookup D (c, (m1, m2)) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
180 |
|
32602 | 181 |
fun dest_call D (Const (@{const_name Collect}, _) $ Abs (_, _, c)) = |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
182 |
let |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
183 |
val (sk, _, _, _, _) = D |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
184 |
val vs = Term.strip_qnt_vars "Ex" c |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
185 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
186 |
(* FIXME: throw error "dest_call" for malformed terms *) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
187 |
val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const ("Pair", _) $ r $ l)) $ Gam) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
188 |
= Term.strip_qnt_body "Ex" c |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
189 |
val (p, l') = dest_inj sk l |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
190 |
val (q, r') = dest_inj sk r |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
191 |
in |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
192 |
(vs, p, l', q, r', Gam) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
193 |
end |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
194 |
| dest_call D t = error "dest_call" |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
195 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
196 |
|
34229 | 197 |
fun mk_desc thy tac vs Gam l r m1 m2 = |
198 |
let |
|
199 |
fun try rel = |
|
200 |
try_proof (cterm_of thy |
|
201 |
(Term.list_all (vs, |
|
202 |
Logic.mk_implies (HOLogic.mk_Trueprop Gam, |
|
203 |
HOLogic.mk_Trueprop (Const (rel, @{typ "nat => nat => bool"}) |
|
204 |
$ (m2 $ r) $ (m1 $ l)))))) tac |
|
205 |
in |
|
206 |
case try @{const_name HOL.less} of |
|
207 |
Solved thm => Less thm |
|
208 |
| Stuck thm => |
|
209 |
(case try @{const_name HOL.less_eq} of |
|
210 |
Solved thm2 => LessEq (thm2, thm) |
|
211 |
| Stuck thm2 => |
|
212 |
if prems_of thm2 = [HOLogic.Trueprop $ HOLogic.false_const] |
|
213 |
then False thm2 else None (thm2, thm) |
|
214 |
| _ => raise Match) (* FIXME *) |
|
215 |
| _ => raise Match |
|
216 |
end |
|
217 |
||
218 |
fun derive_descent thy tac c m1 m2 D = |
|
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
219 |
case get_descent D c m1 m2 of |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
220 |
SOME _ => D |
34229 | 221 |
| NONE => |
222 |
let |
|
223 |
val (vs, _, l, _, r, Gam) = dest_call D c |
|
224 |
in |
|
225 |
note_descent c m1 m2 (mk_desc thy tac vs Gam l r m1 m2) D |
|
226 |
end |
|
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
227 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
228 |
fun CALLS tac i st = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
229 |
if Thm.no_prems st then all_tac st |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
230 |
else case Thm.term_of (Thm.cprem_of st i) of |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
32683
diff
changeset
|
231 |
(_ $ (_ $ rel)) => tac (Function_Lib.dest_binop_list @{const_name Lattices.sup} rel, i) st |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
232 |
|_ => no_tac st |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
233 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
234 |
type ttac = (data -> int -> tactic) -> (data -> int -> tactic) -> data -> int -> tactic |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
235 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
236 |
fun TERMINATION ctxt tac = |
32602 | 237 |
SUBGOAL (fn (_ $ (Const (@{const_name wf}, wfT) $ rel), i) => |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
238 |
let |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
239 |
val (T, _) = HOLogic.dest_prodT (HOLogic.dest_setT (domain_type wfT)) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
240 |
in |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
241 |
tac (create ctxt T rel) i |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
242 |
end) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
243 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
244 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
245 |
(* A tactic to convert open to closed termination goals *) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
246 |
local |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
247 |
fun dest_term (t : term) = (* FIXME, cf. Lexicographic order *) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
248 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
249 |
val (vars, prop) = Function_Lib.dest_all_all t |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
250 |
val (prems, concl) = Logic.strip_horn prop |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
251 |
val (lhs, rhs) = concl |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
252 |
|> HOLogic.dest_Trueprop |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
253 |
|> HOLogic.dest_mem |> fst |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
254 |
|> HOLogic.dest_prod |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
255 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
256 |
(vars, prems, lhs, rhs) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
257 |
end |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
258 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
259 |
fun mk_pair_compr (T, qs, l, r, conds) = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
260 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
261 |
val pT = HOLogic.mk_prodT (T, T) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
262 |
val n = length qs |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
263 |
val peq = HOLogic.eq_const pT $ Bound n $ (HOLogic.pair_const T T $ l $ r) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
264 |
val conds' = if null conds then [HOLogic.true_const] else conds |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
265 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
266 |
HOLogic.Collect_const pT $ |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
267 |
Abs ("uu_", pT, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
268 |
(foldr1 HOLogic.mk_conj (peq :: conds') |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
269 |
|> fold_rev (fn v => fn t => HOLogic.exists_const (fastype_of v) $ lambda v t) qs)) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
270 |
end |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
271 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
272 |
in |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
273 |
|
30607
c3d1590debd8
eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
wenzelm
parents:
30304
diff
changeset
|
274 |
fun wf_union_tac ctxt st = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
275 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
276 |
val thy = ProofContext.theory_of ctxt |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
277 |
val cert = cterm_of (theory_of_thm st) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
278 |
val ((_ $ (_ $ rel)) :: ineqs) = prems_of st |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
279 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
280 |
fun mk_compr ineq = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
281 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
282 |
val (vars, prems, lhs, rhs) = dest_term ineq |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
283 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
284 |
mk_pair_compr (fastype_of lhs, vars, lhs, rhs, map (ObjectLogic.atomize_term thy) prems) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
285 |
end |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
286 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
287 |
val relation = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
288 |
if null ineqs |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
289 |
then Const (@{const_name Set.empty}, fastype_of rel) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
290 |
else map mk_compr ineqs |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
291 |
|> foldr1 (HOLogic.mk_binop @{const_name Lattices.sup}) |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
292 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
293 |
fun solve_membership_tac i = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
294 |
(EVERY' (replicate (i - 2) (rtac @{thm UnI2})) (* pick the right component of the union *) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
295 |
THEN' (fn j => TRY (rtac @{thm UnI1} j)) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
296 |
THEN' (rtac @{thm CollectI}) (* unfold comprehension *) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
297 |
THEN' (fn i => REPEAT (rtac @{thm exI} i)) (* Turn existentials into schematic Vars *) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
298 |
THEN' ((rtac @{thm refl}) (* unification instantiates all Vars *) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
299 |
ORELSE' ((rtac @{thm conjI}) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
300 |
THEN' (rtac @{thm refl}) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
301 |
THEN' (blast_tac (claset_of ctxt)))) (* Solve rest of context... not very elegant *) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
302 |
) i |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
303 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
304 |
((PRIMITIVE (Drule.cterm_instantiate [(cert rel, cert relation)]) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
305 |
THEN ALLGOALS (fn i => if i = 1 then all_tac else solve_membership_tac i))) st |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
306 |
end |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
307 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
308 |
end |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
309 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
310 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
311 |
(* continuation passing repeat combinator *) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
312 |
fun REPEAT ttac cont err_cont = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
313 |
ttac (fn D => fn i => (REPEAT ttac cont cont D i)) err_cont |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
314 |
|
34228
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
315 |
(*** DEPENDENCY GRAPHS ***) |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
316 |
|
34228
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
317 |
structure TermGraph = Graph(type key = term val ord = TermOrd.fast_term_ord); |
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
318 |
|
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
319 |
|
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
320 |
fun prove_chain thy chain_tac c1 c2 = |
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
321 |
let |
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
322 |
val goal = |
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
323 |
HOLogic.mk_eq (HOLogic.mk_binop @{const_name Relation.rel_comp} (c1, c2), |
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
324 |
Const (@{const_name Set.empty}, fastype_of c1)) |
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
325 |
|> HOLogic.mk_Trueprop (* "C1 O C2 = {}" *) |
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
326 |
in |
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
327 |
case Function_Lib.try_proof (cterm_of thy goal) chain_tac of |
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
328 |
Function_Lib.Solved thm => SOME thm |
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
329 |
| _ => NONE |
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
330 |
end |
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
331 |
|
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
332 |
fun derive_chains ctxt chain_tac cont D = CALLS (fn (cs, i) => |
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
333 |
let |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
334 |
val thy = ProofContext.theory_of ctxt |
34228
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
335 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
336 |
fun derive_chain c1 c2 D = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
337 |
if is_some (get_chain D c1 c2) then D else |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
338 |
note_chain c1 c2 (prove_chain thy chain_tac c1 c2) D |
34228
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
339 |
in |
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
340 |
cont (fold_product derive_chain cs cs D) i |
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
341 |
end) |
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
342 |
|
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
343 |
|
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
344 |
fun mk_dgraph D cs = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
345 |
TermGraph.empty |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
346 |
|> fold (fn c => TermGraph.new_node (c,())) cs |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
347 |
|> fold_product (fn c1 => fn c2 => |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
348 |
if is_none (get_chain D c1 c2 |> the_default NONE) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
349 |
then TermGraph.add_edge (c1, c2) else I) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
350 |
cs cs |
34228
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
351 |
|
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
352 |
fun ucomp_empty_tac T = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
353 |
REPEAT_ALL_NEW (rtac @{thm union_comp_emptyR} |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
354 |
ORELSE' rtac @{thm union_comp_emptyL} |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
355 |
ORELSE' SUBGOAL (fn (_ $ (_ $ (_ $ c1 $ c2) $ _), i) => rtac (T c1 c2) i)) |
34228
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
356 |
|
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
357 |
fun regroup_calls_tac cs = CALLS (fn (cs', i) => |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
358 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
359 |
val is = map (fn c => find_index (curry op aconv c) cs') cs |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
360 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
361 |
CONVERSION (Conv.arg_conv (Conv.arg_conv |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
362 |
(Function_Lib.regroup_union_conv is))) i |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
363 |
end) |
34228
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
364 |
|
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
365 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
366 |
fun solve_trivial_tac D = CALLS (fn ([c], i) => |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
367 |
(case get_chain D c c of |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
368 |
SOME (SOME thm) => rtac @{thm wf_no_loop} i |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
369 |
THEN rtac thm i |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
370 |
| _ => no_tac) |
34228
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
371 |
| _ => no_tac) |
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
372 |
|
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
373 |
fun decompose_tac' cont err_cont D = CALLS (fn (cs, i) => |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
374 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
375 |
val G = mk_dgraph D cs |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
376 |
val sccs = TermGraph.strong_conn G |
34228
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
377 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
378 |
fun split [SCC] i = (solve_trivial_tac D i ORELSE cont D i) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
379 |
| split (SCC::rest) i = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
380 |
regroup_calls_tac SCC i |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
381 |
THEN rtac @{thm wf_union_compatible} i |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
382 |
THEN rtac @{thm less_by_empty} (i + 2) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
383 |
THEN ucomp_empty_tac (the o the oo get_chain D) (i + 2) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
384 |
THEN split rest (i + 1) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
385 |
THEN (solve_trivial_tac D i ORELSE cont D i) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
386 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
387 |
if length sccs > 1 then split sccs i |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
388 |
else solve_trivial_tac D i ORELSE err_cont D i |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
389 |
end) |
34228
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
390 |
|
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
391 |
fun decompose_tac ctxt chain_tac cont err_cont = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
392 |
derive_chains ctxt chain_tac (decompose_tac' cont err_cont) |
34228
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
393 |
|
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
394 |
|
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
395 |
(*** Local Descent Proofs ***) |
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
396 |
|
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
397 |
fun gen_descent diag ctxt tac cont D = CALLS (fn (cs, i) => |
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
398 |
let |
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
399 |
val thy = ProofContext.theory_of ctxt |
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
400 |
val measures_of = get_measures D |
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
401 |
|
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
402 |
fun derive c D = |
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
403 |
let |
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
404 |
val (_, p, _, q, _, _) = dest_call D c |
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
405 |
in |
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
406 |
if diag andalso p = q |
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
407 |
then fold (fn m => derive_descent thy tac c m m) (measures_of p) D |
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
408 |
else fold_product (derive_descent thy tac c) |
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
409 |
(measures_of p) (measures_of q) D |
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
410 |
end |
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
411 |
in |
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
412 |
cont (Function_Common.PROFILE "deriving descents" (fold derive cs) D) i |
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
413 |
end) |
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
414 |
|
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
415 |
val derive_diag = gen_descent true |
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
416 |
val derive_all = gen_descent false |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
417 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
418 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
419 |
end |