author | wenzelm |
Thu, 23 Jul 2009 18:44:09 +0200 | |
changeset 32149 | ef59550a55d3 |
parent 32135 | f645b51e8e54 |
child 32602 | f2b741473860 |
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 note_measure : int -> term -> data -> data |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
17 |
val note_chain : term -> term -> thm option -> data -> data |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
18 |
val note_descent : term -> term -> term -> cell -> data -> data |
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 |
val get_num_points : data -> int |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
21 |
val get_types : data -> int -> typ |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
22 |
val get_measures : data -> int -> term list |
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 |
(* read from cache *) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
25 |
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
|
26 |
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
|
27 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
28 |
(* writes *) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
29 |
val derive_descent : theory -> tactic -> term -> term -> term -> data -> data |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
30 |
val derive_descents : theory -> tactic -> term -> data -> data |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
31 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
32 |
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
|
33 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
34 |
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
|
35 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
36 |
(* 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
|
37 |
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
|
38 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
39 |
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
|
40 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
41 |
val REPEAT : ttac -> ttac |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
42 |
|
30607
c3d1590debd8
eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
wenzelm
parents:
30304
diff
changeset
|
43 |
val wf_union_tac : Proof.context -> tactic |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
44 |
end |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
45 |
|
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 |
structure Termination : TERMINATION = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
49 |
struct |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
50 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
51 |
open FundefLib |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
52 |
|
29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
29125
diff
changeset
|
53 |
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
|
54 |
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
|
55 |
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
|
56 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
57 |
(** Analyzing binary trees **) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
58 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
59 |
(* Skeleton of a tree structure *) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
60 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
61 |
datatype skel = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
62 |
SLeaf of int (* index *) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
63 |
| SBranch of (skel * skel) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
64 |
|
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 |
(* abstract make and dest functions *) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
67 |
fun mk_tree leaf branch = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
68 |
let fun mk (SLeaf i) = leaf i |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
69 |
| 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
|
70 |
in mk end |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
71 |
|
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 |
fun dest_tree split = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
74 |
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
|
75 |
| dest (SBranch (s, t)) x = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
76 |
let val (l, r) = split x |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
77 |
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
|
78 |
in dest end |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
79 |
|
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 |
(* concrete versions for sum types *) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
82 |
fun is_inj (Const ("Sum_Type.Inl", _) $ _) = true |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
83 |
| is_inj (Const ("Sum_Type.Inr", _) $ _) = true |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
84 |
| is_inj _ = false |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
85 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
86 |
fun dest_inl (Const ("Sum_Type.Inl", _) $ t) = SOME t |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
87 |
| dest_inl _ = NONE |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
88 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
89 |
fun dest_inr (Const ("Sum_Type.Inr", _) $ t) = SOME t |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
90 |
| dest_inr _ = NONE |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
91 |
|
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 |
fun mk_skel ps = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
94 |
let |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
95 |
fun skel i ps = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
96 |
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
|
97 |
then let |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
98 |
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
|
99 |
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
|
100 |
in (k, SBranch (s, t)) end |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
101 |
else (i + 1, SLeaf i) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
102 |
in |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
103 |
snd (skel 0 ps) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
104 |
end |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
105 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
106 |
(* compute list of types for nodes *) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
107 |
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
|
108 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
109 |
(* find index and raw term *) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
110 |
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
|
111 |
| dest_inj (SBranch (s, t)) trm = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
112 |
case dest_inl trm of |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
113 |
SOME trm' => dest_inj s trm' |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
114 |
| _ => dest_inj t (the (dest_inr trm)) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
115 |
|
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 |
(** Matrix cell datatype **) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
119 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
120 |
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
|
121 |
|
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 |
type data = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
124 |
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
|
125 |
* (int -> typ) (* types of program points *) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
126 |
* (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
|
127 |
* (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
|
128 |
* (cell Term3tab.table) (* local descents *) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
129 |
|
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 |
fun map_measures f (p, T, M, C, D) = (p, T, f M, C, D) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
132 |
fun map_chains f (p, T, M, C, D) = (p, T, M, f C, D) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
133 |
fun map_descent f (p, T, M, C, D) = (p, T, M, C, f D) |
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_measure p m = map_measures (Inttab.insert_list (op aconv) (p, m)) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
136 |
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
|
137 |
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
|
138 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
139 |
(* Build case expression *) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
140 |
fun mk_sumcases (sk, _, _, _, _) T fs = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
141 |
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
|
142 |
(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
|
143 |
sk |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
144 |
|> fst |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
145 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
146 |
fun mk_sum_skel rel = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
147 |
let |
32135
f645b51e8e54
set intersection and union now named inter and union; closer connection between set and lattice operations; factored out complete lattice
haftmann
parents:
31971
diff
changeset
|
148 |
val cs = FundefLib.dest_binop_list @{const_name union} rel |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
149 |
fun collect_pats (Const ("Collect", _) $ Abs (_, _, c)) = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
150 |
let |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
151 |
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
|
152 |
= Term.strip_qnt_body "Ex" c |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
153 |
in cons r o cons l end |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
154 |
in |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
155 |
mk_skel (fold collect_pats cs []) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
156 |
end |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
157 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
158 |
fun create ctxt T rel = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
159 |
let |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
160 |
val sk = mk_sum_skel rel |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
161 |
val Ts = node_types sk T |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
162 |
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
|
163 |
in |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
164 |
(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
|
165 |
end |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
166 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
167 |
fun get_num_points (sk, _, _, _, _) = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
168 |
let |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
169 |
fun num (SLeaf i) = i + 1 |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
170 |
| num (SBranch (s, t)) = num t |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
171 |
in num sk end |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
172 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
173 |
fun get_types (_, T, _, _, _) = T |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
174 |
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
|
175 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
176 |
fun get_chain (_, _, _, C, _) c1 c2 = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
177 |
Term2tab.lookup C (c1, c2) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
178 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
179 |
fun get_descent (_, _, _, _, D) c m1 m2 = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
180 |
Term3tab.lookup D (c, (m1, m2)) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
181 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
182 |
fun dest_call D (Const ("Collect", _) $ Abs (_, _, c)) = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
183 |
let |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
184 |
val n = get_num_points D |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
185 |
val (sk, _, _, _, _) = D |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
186 |
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
|
187 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
188 |
(* 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
|
189 |
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
|
190 |
= Term.strip_qnt_body "Ex" c |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
191 |
val (p, l') = dest_inj sk l |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
192 |
val (q, r') = dest_inj sk r |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
193 |
in |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
194 |
(vs, p, l', q, r', Gam) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
195 |
end |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
196 |
| dest_call D t = error "dest_call" |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
197 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
198 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
199 |
fun derive_desc_aux thy tac c (vs, p, l', q, r', Gam) m1 m2 D = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
200 |
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
|
201 |
SOME _ => D |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
202 |
| NONE => let |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
203 |
fun cgoal rel = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
204 |
Term.list_all (vs, |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
205 |
Logic.mk_implies (HOLogic.mk_Trueprop Gam, |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
206 |
HOLogic.mk_Trueprop (Const (rel, @{typ "nat => nat => bool"}) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
207 |
$ (m2 $ r') $ (m1 $ l')))) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
208 |
|> cterm_of thy |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
209 |
in |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
210 |
note_descent c m1 m2 |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
211 |
(case try_proof (cgoal @{const_name HOL.less}) tac of |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
212 |
Solved thm => Less thm |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
213 |
| Stuck thm => |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
214 |
(case try_proof (cgoal @{const_name HOL.less_eq}) tac of |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
215 |
Solved thm2 => LessEq (thm2, thm) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
216 |
| Stuck thm2 => |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
217 |
if prems_of thm2 = [HOLogic.Trueprop $ HOLogic.false_const] |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
218 |
then False thm2 else None (thm2, thm) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
219 |
| _ => raise Match) (* FIXME *) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
220 |
| _ => raise Match) D |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
221 |
end |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
222 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
223 |
fun derive_descent thy tac c m1 m2 D = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
224 |
derive_desc_aux thy tac c (dest_call D c) m1 m2 D |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
225 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
226 |
(* all descents in one go *) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
227 |
fun derive_descents thy tac c D = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
228 |
let val cdesc as (vs, p, l', q, r', Gam) = dest_call D c |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
229 |
in fold_product (derive_desc_aux thy tac c cdesc) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
230 |
(get_measures D p) (get_measures D q) D |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
231 |
end |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
232 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
233 |
fun CALLS tac i st = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
234 |
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
|
235 |
else case Thm.term_of (Thm.cprem_of st i) of |
32135
f645b51e8e54
set intersection and union now named inter and union; closer connection between set and lattice operations; factored out complete lattice
haftmann
parents:
31971
diff
changeset
|
236 |
(_ $ (_ $ rel)) => tac (FundefLib.dest_binop_list @{const_name union} rel, i) st |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
237 |
|_ => no_tac st |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
238 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
239 |
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
|
240 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
241 |
fun TERMINATION ctxt tac = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
242 |
SUBGOAL (fn (_ $ (Const (@{const_name "wf"}, wfT) $ rel), i) => |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
243 |
let |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
244 |
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
|
245 |
in |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
246 |
tac (create ctxt T rel) i |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
247 |
end) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
248 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
249 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
250 |
(* 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
|
251 |
local |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
252 |
fun dest_term (t : term) = (* FIXME, cf. Lexicographic order *) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
253 |
let |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
254 |
val (vars, prop) = FundefLib.dest_all_all t |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
255 |
val (prems, concl) = Logic.strip_horn prop |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
256 |
val (lhs, rhs) = concl |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
257 |
|> HOLogic.dest_Trueprop |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
258 |
|> HOLogic.dest_mem |> fst |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
259 |
|> HOLogic.dest_prod |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
260 |
in |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
261 |
(vars, prems, lhs, rhs) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
262 |
end |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
263 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
264 |
fun mk_pair_compr (T, qs, l, r, conds) = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
265 |
let |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
266 |
val pT = HOLogic.mk_prodT (T, T) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
267 |
val n = length qs |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
268 |
val peq = HOLogic.eq_const pT $ Bound n $ (HOLogic.pair_const T T $ l $ r) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
269 |
val conds' = if null conds then [HOLogic.true_const] else conds |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
270 |
in |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
271 |
HOLogic.Collect_const pT $ |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
272 |
Abs ("uu_", pT, |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
273 |
(foldr1 HOLogic.mk_conj (peq :: conds') |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
274 |
|> fold_rev (fn v => fn t => HOLogic.exists_const (fastype_of v) $ lambda v t) qs)) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
275 |
end |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
276 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
277 |
in |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
278 |
|
30607
c3d1590debd8
eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
wenzelm
parents:
30304
diff
changeset
|
279 |
fun wf_union_tac ctxt st = |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
280 |
let |
30607
c3d1590debd8
eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
wenzelm
parents:
30304
diff
changeset
|
281 |
val thy = ProofContext.theory_of ctxt |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
282 |
val cert = cterm_of (theory_of_thm st) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
283 |
val ((trueprop $ (wf $ rel)) :: ineqs) = prems_of st |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
284 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
285 |
fun mk_compr ineq = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
286 |
let |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
287 |
val (vars, prems, lhs, rhs) = dest_term ineq |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
288 |
in |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
289 |
mk_pair_compr (fastype_of lhs, vars, lhs, rhs, map (ObjectLogic.atomize_term thy) prems) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
290 |
end |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
291 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
292 |
val relation = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
293 |
if null ineqs then |
30304
d8e4cd2ac2a1
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
haftmann
parents:
29269
diff
changeset
|
294 |
Const (@{const_name Set.empty}, fastype_of rel) |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
295 |
else |
32135
f645b51e8e54
set intersection and union now named inter and union; closer connection between set and lattice operations; factored out complete lattice
haftmann
parents:
31971
diff
changeset
|
296 |
foldr1 (HOLogic.mk_binop @{const_name union}) (map mk_compr ineqs) |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
297 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
298 |
fun solve_membership_tac i = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
299 |
(EVERY' (replicate (i - 2) (rtac @{thm UnI2})) (* pick the right component of the union *) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
300 |
THEN' (fn j => TRY (rtac @{thm UnI1} j)) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
301 |
THEN' (rtac @{thm CollectI}) (* unfold comprehension *) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
302 |
THEN' (fn i => REPEAT (rtac @{thm exI} i)) (* Turn existentials into schematic Vars *) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
303 |
THEN' ((rtac @{thm refl}) (* unification instantiates all Vars *) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
304 |
ORELSE' ((rtac @{thm conjI}) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
305 |
THEN' (rtac @{thm refl}) |
32149
ef59550a55d3
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
wenzelm
parents:
32135
diff
changeset
|
306 |
THEN' (blast_tac (claset_of ctxt)))) (* Solve rest of context... not very elegant *) |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
307 |
) i |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
308 |
in |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
309 |
((PRIMITIVE (Drule.cterm_instantiate [(cert rel, cert relation)]) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
310 |
THEN ALLGOALS (fn i => if i = 1 then all_tac else solve_membership_tac i))) st |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
311 |
end |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
312 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
313 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
314 |
end |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
315 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
316 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
317 |
(* continuation passing repeat combinator *) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
318 |
fun REPEAT ttac cont err_cont = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
319 |
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
|
320 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
321 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
322 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
323 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
324 |
end |