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