author | nipkow |
Fri, 27 Mar 2020 12:28:05 +0100 | |
changeset 71593 | 71579bd59cd4 |
parent 67149 | e61557884799 |
child 79971 | 033f90dc441d |
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 |
|
41114 | 4 |
Context data for termination proofs. |
29125
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 |
signature TERMINATION = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
8 |
sig |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
9 |
type data |
39924
f4d3e70ed3a8
discontinued continuations to simplify control flow; dropped optimization in scnp
krauss
parents:
39923
diff
changeset
|
10 |
datatype cell = Less of thm | LessEq of thm * thm | None of thm * thm | False of thm |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
11 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
12 |
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
|
13 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
14 |
val get_num_points : data -> int |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
15 |
val get_types : data -> int -> typ |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
16 |
val get_measures : data -> int -> term list |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
17 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
18 |
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
|
19 |
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
|
20 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
21 |
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
|
22 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
23 |
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
|
24 |
|
39924
f4d3e70ed3a8
discontinued continuations to simplify control flow; dropped optimization in scnp
krauss
parents:
39923
diff
changeset
|
25 |
(* Termination tactics *) |
f4d3e70ed3a8
discontinued continuations to simplify control flow; dropped optimization in scnp
krauss
parents:
39923
diff
changeset
|
26 |
type ttac = data -> int -> tactic |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
27 |
|
39924
f4d3e70ed3a8
discontinued continuations to simplify control flow; dropped optimization in scnp
krauss
parents:
39923
diff
changeset
|
28 |
val TERMINATION : Proof.context -> tactic -> ttac -> int -> tactic |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
29 |
|
30607
c3d1590debd8
eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
wenzelm
parents:
30304
diff
changeset
|
30 |
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
|
31 |
|
59618 | 32 |
val decompose_tac : Proof.context -> ttac |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
33 |
end |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
34 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
35 |
structure Termination : TERMINATION = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
36 |
struct |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
37 |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
32683
diff
changeset
|
38 |
open Function_Lib |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
39 |
|
35408 | 40 |
val term2_ord = prod_ord Term_Ord.fast_term_ord Term_Ord.fast_term_ord |
31971
8c1b845ed105
renamed functor TableFun to Table, and GraphFun to Graph;
wenzelm
parents:
31775
diff
changeset
|
41 |
structure Term2tab = Table(type key = term * term val ord = term2_ord); |
35408 | 42 |
structure Term3tab = |
43 |
Table(type key = term * (term * term) val ord = prod_ord Term_Ord.fast_term_ord term2_ord); |
|
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
44 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
45 |
(** Analyzing binary trees **) |
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 |
(* Skeleton of a tree structure *) |
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 |
datatype skel = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
50 |
SLeaf of int (* index *) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
51 |
| SBranch of (skel * skel) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
52 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
53 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
54 |
(* abstract make and dest functions *) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
55 |
fun mk_tree leaf branch = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
56 |
let fun mk (SLeaf i) = leaf i |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
57 |
| 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
|
58 |
in mk end |
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 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
61 |
fun dest_tree split = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
62 |
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
|
63 |
| dest (SBranch (s, t)) x = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
64 |
let val (l, r) = split x |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
65 |
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
|
66 |
in dest end |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
67 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
68 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
69 |
(* concrete versions for sum types *) |
67149 | 70 |
fun is_inj (Const (\<^const_name>\<open>Sum_Type.Inl\<close>, _) $ _) = true |
71 |
| is_inj (Const (\<^const_name>\<open>Sum_Type.Inr\<close>, _) $ _) = true |
|
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
72 |
| is_inj _ = false |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
73 |
|
67149 | 74 |
fun dest_inl (Const (\<^const_name>\<open>Sum_Type.Inl\<close>, _) $ t) = SOME t |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
75 |
| dest_inl _ = NONE |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
76 |
|
67149 | 77 |
fun dest_inr (Const (\<^const_name>\<open>Sum_Type.Inr\<close>, _) $ t) = SOME t |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
78 |
| dest_inr _ = NONE |
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 |
fun mk_skel ps = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
82 |
let |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
83 |
fun skel i ps = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
84 |
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
|
85 |
then let |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
86 |
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
|
87 |
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
|
88 |
in (k, SBranch (s, t)) end |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
89 |
else (i + 1, SLeaf i) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
90 |
in |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
91 |
snd (skel 0 ps) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
92 |
end |
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 |
(* compute list of types for nodes *) |
67149 | 95 |
fun node_types sk T = dest_tree (fn Type (\<^type_name>\<open>Sum_Type.sum\<close>, [LT, RT]) => (LT, RT)) sk T |> map snd |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
96 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
97 |
(* find index and raw term *) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
98 |
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
|
99 |
| dest_inj (SBranch (s, t)) trm = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
100 |
case dest_inl trm of |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
101 |
SOME trm' => dest_inj s trm' |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
102 |
| _ => dest_inj t (the (dest_inr trm)) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
103 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
104 |
|
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 |
(** Matrix cell datatype **) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
107 |
|
39924
f4d3e70ed3a8
discontinued continuations to simplify control flow; dropped optimization in scnp
krauss
parents:
39923
diff
changeset
|
108 |
datatype cell = Less of thm | LessEq of thm * thm | None of thm * thm | False of thm; |
29125
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 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
111 |
type data = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
112 |
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
|
113 |
* (int -> typ) (* types of program points *) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
114 |
* (term list Inttab.table) (* measures for program points *) |
39923
0e1bd289c8ea
use Cache structure instead of passing tables around explicitly
krauss
parents:
38864
diff
changeset
|
115 |
* (term * term -> thm option) (* which calls form chains? (cached) *) |
0e1bd289c8ea
use Cache structure instead of passing tables around explicitly
krauss
parents:
38864
diff
changeset
|
116 |
* (term * (term * term) -> cell)(* local descents (cached) *) |
29125
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 |
(* Build case expression *) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
120 |
fun mk_sumcases (sk, _, _, _, _) T fs = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
121 |
mk_tree (fn i => (nth fs i, domain_type (fastype_of (nth fs i)))) |
55968 | 122 |
(fn ((f, fT), (g, gT)) => (Sum_Tree.mk_sumcase fT gT T f g, Sum_Tree.mk_sumT fT gT)) |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
123 |
sk |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
124 |
|> fst |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
125 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
126 |
fun mk_sum_skel rel = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
127 |
let |
67149 | 128 |
val cs = Function_Lib.dest_binop_list \<^const_name>\<open>Lattices.sup\<close> rel |
129 |
fun collect_pats (Const (\<^const_name>\<open>Collect\<close>, _) $ Abs (_, _, c)) = |
|
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
130 |
let |
67149 | 131 |
val (Const (\<^const_name>\<open>HOL.conj\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ (Const (\<^const_name>\<open>Pair\<close>, _) $ r $ l)) $ _) |
132 |
= Term.strip_qnt_body \<^const_name>\<open>Ex\<close> c |
|
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
133 |
in cons r o cons l end |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
134 |
in |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
135 |
mk_skel (fold collect_pats cs []) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
136 |
end |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
137 |
|
59618 | 138 |
fun prove_chain ctxt chain_tac (c1, c2) = |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
139 |
let |
39923
0e1bd289c8ea
use Cache structure instead of passing tables around explicitly
krauss
parents:
38864
diff
changeset
|
140 |
val goal = |
67149 | 141 |
HOLogic.mk_eq (HOLogic.mk_binop \<^const_name>\<open>Relation.relcomp\<close> (c1, c2), |
142 |
Const (\<^const_abbrev>\<open>Set.empty\<close>, fastype_of c1)) |
|
39923
0e1bd289c8ea
use Cache structure instead of passing tables around explicitly
krauss
parents:
38864
diff
changeset
|
143 |
|> HOLogic.mk_Trueprop (* "C1 O C2 = {}" *) |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
144 |
in |
60328 | 145 |
(case Function_Lib.try_proof ctxt (Thm.cterm_of ctxt goal) chain_tac of |
39923
0e1bd289c8ea
use Cache structure instead of passing tables around explicitly
krauss
parents:
38864
diff
changeset
|
146 |
Function_Lib.Solved thm => SOME thm |
60328 | 147 |
| _ => NONE) |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
148 |
end |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
149 |
|
39923
0e1bd289c8ea
use Cache structure instead of passing tables around explicitly
krauss
parents:
38864
diff
changeset
|
150 |
|
67149 | 151 |
fun dest_call' sk (Const (\<^const_name>\<open>Collect\<close>, _) $ Abs (_, _, c)) = |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
152 |
let |
67149 | 153 |
val vs = Term.strip_qnt_vars \<^const_name>\<open>Ex\<close> c |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
154 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
155 |
(* FIXME: throw error "dest_call" for malformed terms *) |
67149 | 156 |
val (Const (\<^const_name>\<open>HOL.conj\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ (Const (\<^const_name>\<open>Pair\<close>, _) $ r $ l)) $ Gam) |
157 |
= Term.strip_qnt_body \<^const_name>\<open>Ex\<close> c |
|
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
158 |
val (p, l') = dest_inj sk l |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
159 |
val (q, r') = dest_inj sk r |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
160 |
in |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
161 |
(vs, p, l', q, r', Gam) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
162 |
end |
39923
0e1bd289c8ea
use Cache structure instead of passing tables around explicitly
krauss
parents:
38864
diff
changeset
|
163 |
| dest_call' _ _ = error "dest_call" |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
164 |
|
39923
0e1bd289c8ea
use Cache structure instead of passing tables around explicitly
krauss
parents:
38864
diff
changeset
|
165 |
fun dest_call (sk, _, _, _, _) = dest_call' sk |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
166 |
|
59618 | 167 |
fun mk_desc ctxt tac vs Gam l r m1 m2 = |
34229 | 168 |
let |
169 |
fun try rel = |
|
60328 | 170 |
try_proof ctxt (Thm.cterm_of ctxt |
46218
ecf6375e2abb
renamed Term.list_all to Logic.list_all, in accordance to HOLogic.list_all;
wenzelm
parents:
45740
diff
changeset
|
171 |
(Logic.list_all (vs, |
34229 | 172 |
Logic.mk_implies (HOLogic.mk_Trueprop Gam, |
67149 | 173 |
HOLogic.mk_Trueprop (Const (rel, \<^typ>\<open>nat \<Rightarrow> nat \<Rightarrow> bool\<close>) |
34229 | 174 |
$ (m2 $ r) $ (m1 $ l)))))) tac |
175 |
in |
|
67149 | 176 |
(case try \<^const_name>\<open>Orderings.less\<close> of |
60328 | 177 |
Solved thm => Less thm |
178 |
| Stuck thm => |
|
67149 | 179 |
(case try \<^const_name>\<open>Orderings.less_eq\<close> of |
34229 | 180 |
Solved thm2 => LessEq (thm2, thm) |
181 |
| Stuck thm2 => |
|
67149 | 182 |
if Thm.prems_of thm2 = [HOLogic.Trueprop $ \<^term>\<open>False\<close>] |
60328 | 183 |
then False thm2 else None (thm2, thm) |
34229 | 184 |
| _ => raise Match) (* FIXME *) |
60328 | 185 |
| _ => raise Match) |
34229 | 186 |
end |
187 |
||
59618 | 188 |
fun prove_descent ctxt tac sk (c, (m1, m2)) = |
39923
0e1bd289c8ea
use Cache structure instead of passing tables around explicitly
krauss
parents:
38864
diff
changeset
|
189 |
let |
0e1bd289c8ea
use Cache structure instead of passing tables around explicitly
krauss
parents:
38864
diff
changeset
|
190 |
val (vs, _, l, _, r, Gam) = dest_call' sk c |
0e1bd289c8ea
use Cache structure instead of passing tables around explicitly
krauss
parents:
38864
diff
changeset
|
191 |
in |
59618 | 192 |
mk_desc ctxt tac vs Gam l r m1 m2 |
39923
0e1bd289c8ea
use Cache structure instead of passing tables around explicitly
krauss
parents:
38864
diff
changeset
|
193 |
end |
0e1bd289c8ea
use Cache structure instead of passing tables around explicitly
krauss
parents:
38864
diff
changeset
|
194 |
|
0e1bd289c8ea
use Cache structure instead of passing tables around explicitly
krauss
parents:
38864
diff
changeset
|
195 |
fun create ctxt chain_tac descent_tac T rel = |
0e1bd289c8ea
use Cache structure instead of passing tables around explicitly
krauss
parents:
38864
diff
changeset
|
196 |
let |
0e1bd289c8ea
use Cache structure instead of passing tables around explicitly
krauss
parents:
38864
diff
changeset
|
197 |
val sk = mk_sum_skel rel |
0e1bd289c8ea
use Cache structure instead of passing tables around explicitly
krauss
parents:
38864
diff
changeset
|
198 |
val Ts = node_types sk T |
57959 | 199 |
val M = Inttab.make (map_index (apsnd (Measure_Functions.get_measure_functions ctxt)) Ts) |
59618 | 200 |
val chain_cache = |
201 |
Cache.create Term2tab.empty Term2tab.lookup Term2tab.update |
|
202 |
(prove_chain ctxt chain_tac) |
|
203 |
val descent_cache = |
|
204 |
Cache.create Term3tab.empty Term3tab.lookup Term3tab.update |
|
205 |
(prove_descent ctxt descent_tac sk) |
|
39923
0e1bd289c8ea
use Cache structure instead of passing tables around explicitly
krauss
parents:
38864
diff
changeset
|
206 |
in |
0e1bd289c8ea
use Cache structure instead of passing tables around explicitly
krauss
parents:
38864
diff
changeset
|
207 |
(sk, nth Ts, M, chain_cache, descent_cache) |
0e1bd289c8ea
use Cache structure instead of passing tables around explicitly
krauss
parents:
38864
diff
changeset
|
208 |
end |
0e1bd289c8ea
use Cache structure instead of passing tables around explicitly
krauss
parents:
38864
diff
changeset
|
209 |
|
0e1bd289c8ea
use Cache structure instead of passing tables around explicitly
krauss
parents:
38864
diff
changeset
|
210 |
fun get_num_points (sk, _, _, _, _) = |
0e1bd289c8ea
use Cache structure instead of passing tables around explicitly
krauss
parents:
38864
diff
changeset
|
211 |
let |
0e1bd289c8ea
use Cache structure instead of passing tables around explicitly
krauss
parents:
38864
diff
changeset
|
212 |
fun num (SLeaf i) = i + 1 |
0e1bd289c8ea
use Cache structure instead of passing tables around explicitly
krauss
parents:
38864
diff
changeset
|
213 |
| num (SBranch (s, t)) = num t |
0e1bd289c8ea
use Cache structure instead of passing tables around explicitly
krauss
parents:
38864
diff
changeset
|
214 |
in num sk end |
0e1bd289c8ea
use Cache structure instead of passing tables around explicitly
krauss
parents:
38864
diff
changeset
|
215 |
|
0e1bd289c8ea
use Cache structure instead of passing tables around explicitly
krauss
parents:
38864
diff
changeset
|
216 |
fun get_types (_, T, _, _, _) = T |
0e1bd289c8ea
use Cache structure instead of passing tables around explicitly
krauss
parents:
38864
diff
changeset
|
217 |
fun get_measures (_, _, M, _, _) = Inttab.lookup_list M |
0e1bd289c8ea
use Cache structure instead of passing tables around explicitly
krauss
parents:
38864
diff
changeset
|
218 |
|
0e1bd289c8ea
use Cache structure instead of passing tables around explicitly
krauss
parents:
38864
diff
changeset
|
219 |
fun get_chain (_, _, _, C, _) c1 c2 = |
0e1bd289c8ea
use Cache structure instead of passing tables around explicitly
krauss
parents:
38864
diff
changeset
|
220 |
SOME (C (c1, c2)) |
0e1bd289c8ea
use Cache structure instead of passing tables around explicitly
krauss
parents:
38864
diff
changeset
|
221 |
|
0e1bd289c8ea
use Cache structure instead of passing tables around explicitly
krauss
parents:
38864
diff
changeset
|
222 |
fun get_descent (_, _, _, _, D) c m1 m2 = |
0e1bd289c8ea
use Cache structure instead of passing tables around explicitly
krauss
parents:
38864
diff
changeset
|
223 |
SOME (D (c, (m1, m2))) |
0e1bd289c8ea
use Cache structure instead of passing tables around explicitly
krauss
parents:
38864
diff
changeset
|
224 |
|
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
225 |
fun CALLS tac i st = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
226 |
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
|
227 |
else case Thm.term_of (Thm.cprem_of st i) of |
67149 | 228 |
(_ $ (_ $ rel)) => tac (Function_Lib.dest_binop_list \<^const_name>\<open>Lattices.sup\<close> rel, i) st |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
229 |
|_ => no_tac st |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
230 |
|
39924
f4d3e70ed3a8
discontinued continuations to simplify control flow; dropped optimization in scnp
krauss
parents:
39923
diff
changeset
|
231 |
type ttac = data -> int -> tactic |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
232 |
|
39923
0e1bd289c8ea
use Cache structure instead of passing tables around explicitly
krauss
parents:
38864
diff
changeset
|
233 |
fun TERMINATION ctxt atac tac = |
67149 | 234 |
SUBGOAL (fn (_ $ (Const (\<^const_name>\<open>wf\<close>, wfT) $ rel), i) => |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
235 |
let |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
236 |
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
|
237 |
in |
39923
0e1bd289c8ea
use Cache structure instead of passing tables around explicitly
krauss
parents:
38864
diff
changeset
|
238 |
tac (create ctxt atac atac T rel) i |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
239 |
end) |
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 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
242 |
(* 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
|
243 |
local |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
244 |
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
|
245 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
246 |
val (vars, prop) = Function_Lib.dest_all_all t |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
247 |
val (prems, concl) = Logic.strip_horn prop |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
248 |
val (lhs, rhs) = concl |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
249 |
|> HOLogic.dest_Trueprop |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
250 |
|> HOLogic.dest_mem |> fst |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
251 |
|> HOLogic.dest_prod |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
252 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
253 |
(vars, prems, lhs, rhs) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
254 |
end |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
255 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
256 |
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
|
257 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
258 |
val pT = HOLogic.mk_prodT (T, T) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
259 |
val n = length qs |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
260 |
val peq = HOLogic.eq_const pT $ Bound n $ (HOLogic.pair_const T T $ l $ r) |
67149 | 261 |
val conds' = if null conds then [\<^term>\<open>True\<close>] else conds |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
262 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
263 |
HOLogic.Collect_const pT $ |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
264 |
Abs ("uu_", pT, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
265 |
(foldr1 HOLogic.mk_conj (peq :: conds') |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
266 |
|> 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
|
267 |
end |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
268 |
|
52723
2ebcc81f599c
eliminate duplicate calls when moving to closed form -- graph decomposition chokes on duplicates
krauss
parents:
47835
diff
changeset
|
269 |
val Un_aci_simps = |
2ebcc81f599c
eliminate duplicate calls when moving to closed form -- graph decomposition chokes on duplicates
krauss
parents:
47835
diff
changeset
|
270 |
map mk_meta_eq @{thms Un_ac Un_absorb} |
2ebcc81f599c
eliminate duplicate calls when moving to closed form -- graph decomposition chokes on duplicates
krauss
parents:
47835
diff
changeset
|
271 |
|
29125
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 |
|
56231
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
wenzelm
parents:
55968
diff
changeset
|
274 |
fun wf_union_tac ctxt st = SUBGOAL (fn _ => |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
275 |
let |
59582 | 276 |
val ((_ $ (_ $ rel)) :: ineqs) = Thm.prems_of st |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
277 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
278 |
fun mk_compr ineq = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
279 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
280 |
val (vars, prems, lhs, rhs) = dest_term ineq |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
281 |
in |
59970 | 282 |
mk_pair_compr (fastype_of lhs, vars, lhs, rhs, map (Object_Logic.atomize_term ctxt) prems) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
283 |
end |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
284 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
285 |
val relation = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
286 |
if null ineqs |
67149 | 287 |
then Const (\<^const_abbrev>\<open>Set.empty\<close>, fastype_of rel) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
288 |
else map mk_compr ineqs |
67149 | 289 |
|> foldr1 (HOLogic.mk_binop \<^const_name>\<open>Lattices.sup\<close>) |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
290 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
291 |
fun solve_membership_tac i = |
60752 | 292 |
(EVERY' (replicate (i - 2) (resolve_tac ctxt @{thms UnI2})) (* pick the right component of the union *) |
293 |
THEN' (fn j => TRY (resolve_tac ctxt @{thms UnI1} j)) |
|
294 |
THEN' (resolve_tac ctxt @{thms CollectI}) (* unfold comprehension *) |
|
295 |
THEN' (fn i => REPEAT (resolve_tac ctxt @{thms exI} i)) (* Turn existentials into schematic Vars *) |
|
296 |
THEN' ((resolve_tac ctxt @{thms refl}) (* unification instantiates all Vars *) |
|
297 |
ORELSE' ((resolve_tac ctxt @{thms conjI}) |
|
298 |
THEN' (resolve_tac ctxt @{thms refl}) |
|
42793 | 299 |
THEN' (blast_tac ctxt))) (* Solve rest of context... not very elegant *) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
300 |
) i |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
301 |
in |
60784 | 302 |
if is_Var rel then |
303 |
PRIMITIVE (infer_instantiate ctxt [(#1 (dest_Var rel), Thm.cterm_of ctxt relation)]) |
|
304 |
THEN ALLGOALS (fn i => if i = 1 then all_tac else solve_membership_tac i) |
|
305 |
THEN rewrite_goal_tac ctxt Un_aci_simps 1 (* eliminate duplicates *) |
|
306 |
else no_tac |
|
56231
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
wenzelm
parents:
55968
diff
changeset
|
307 |
end) 1 st |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
308 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
309 |
end |
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 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
312 |
|
34228
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
313 |
(*** DEPENDENCY GRAPHS ***) |
29125
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 |
fun mk_dgraph D cs = |
35404 | 316 |
Term_Graph.empty |
317 |
|> fold (fn c => Term_Graph.new_node (c, ())) cs |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
318 |
|> fold_product (fn c1 => fn c2 => |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
319 |
if is_none (get_chain D c1 c2 |> the_default NONE) |
47835 | 320 |
then Term_Graph.add_edge (c2, c1) else I) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
321 |
cs cs |
34228
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
322 |
|
60752 | 323 |
fun ucomp_empty_tac ctxt T = |
324 |
REPEAT_ALL_NEW (resolve_tac ctxt @{thms union_comp_emptyR} |
|
325 |
ORELSE' resolve_tac ctxt @{thms union_comp_emptyL} |
|
326 |
ORELSE' SUBGOAL (fn (_ $ (_ $ (_ $ c1 $ c2) $ _), i) => resolve_tac ctxt [T c1 c2] i)) |
|
34228
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
327 |
|
59618 | 328 |
fun regroup_calls_tac ctxt cs = CALLS (fn (cs', i) => |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
329 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
330 |
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
|
331 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
332 |
CONVERSION (Conv.arg_conv (Conv.arg_conv |
59625 | 333 |
(Function_Lib.regroup_union_conv ctxt is))) i |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
334 |
end) |
34228
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
335 |
|
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
336 |
|
60752 | 337 |
fun solve_trivial_tac ctxt D = |
338 |
CALLS (fn ([c], i) => |
|
339 |
(case get_chain D c c of |
|
340 |
SOME (SOME thm) => |
|
341 |
resolve_tac ctxt @{thms wf_no_loop} i THEN |
|
342 |
resolve_tac ctxt [thm] i |
|
343 |
| _ => no_tac) |
|
34228
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
344 |
| _ => no_tac) |
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
345 |
|
59618 | 346 |
fun decompose_tac ctxt D = CALLS (fn (cs, i) => |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
347 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
348 |
val G = mk_dgraph D cs |
35404 | 349 |
val sccs = Term_Graph.strong_conn G |
34228
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
350 |
|
60752 | 351 |
fun split [SCC] i = TRY (solve_trivial_tac ctxt D i) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
352 |
| split (SCC::rest) i = |
59618 | 353 |
regroup_calls_tac ctxt SCC i |
60752 | 354 |
THEN resolve_tac ctxt @{thms wf_union_compatible} i |
355 |
THEN resolve_tac ctxt @{thms less_by_empty} (i + 2) |
|
356 |
THEN ucomp_empty_tac ctxt (the o the oo get_chain D) (i + 2) |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
357 |
THEN split rest (i + 1) |
60752 | 358 |
THEN TRY (solve_trivial_tac ctxt D i) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
359 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
360 |
if length sccs > 1 then split sccs i |
60752 | 361 |
else solve_trivial_tac ctxt D i |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34229
diff
changeset
|
362 |
end) |
34228
bc0cea4cae52
absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents:
33855
diff
changeset
|
363 |
|
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
364 |
end |