1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
|
(* Title: context_tactical.ML
Author: Joshua Chen
More context tactics, and context tactic combinators.
Contains code modified from
~~/Pure/search.ML
~~/Pure/tactical.ML
*)
infix 1 CTHEN CTHEN' CTHEN_ALL_NEW CTHEN_ALL_NEW_FWD
infix 0 CORELSE CAPPEND CORELSE' CAPPEND'
structure Context_Tactical:
sig
type context_tactic' = int -> context_tactic
val CONTEXT_TACTIC': (Proof.context -> int -> tactic) -> context_tactic'
val all_ctac: context_tactic
val no_ctac: context_tactic
val print_ctac: (Proof.context -> string) -> context_tactic
val CTHEN: context_tactic * context_tactic -> context_tactic
val CORELSE: context_tactic * context_tactic -> context_tactic
val CAPPEND: context_tactic * context_tactic -> context_tactic
val CTHEN': context_tactic' * context_tactic' -> context_tactic'
val CORELSE': context_tactic' * context_tactic' -> context_tactic'
val CAPPEND': context_tactic' * context_tactic' -> context_tactic'
val CTRY: context_tactic -> context_tactic
val CREPEAT: context_tactic -> context_tactic
val CREPEAT1: context_tactic -> context_tactic
val CREPEAT_N: int -> context_tactic -> context_tactic
val CFILTER: (context_state -> bool) -> context_tactic -> context_tactic
val CCHANGED: context_tactic -> context_tactic
val CTHEN_ALL_NEW: context_tactic' * context_tactic' -> context_tactic'
val CREPEAT_IN_RANGE: int -> int -> context_tactic' -> context_tactic
val CREPEAT_ALL_NEW: context_tactic' -> context_tactic'
val CTHEN_ALL_NEW_FWD: context_tactic' * context_tactic' -> context_tactic'
val CREPEAT_ALL_NEW_FWD: context_tactic' -> context_tactic'
val CHEADGOAL: context_tactic' -> context_tactic
val CALLGOALS: context_tactic' -> context_tactic
val CSOMEGOAL: context_tactic' -> context_tactic
val CRANGE: context_tactic' list -> context_tactic'
val CFIRST: context_tactic list -> context_tactic
val CFIRST': context_tactic' list -> context_tactic'
val CTHEN_BEST_FIRST: context_tactic -> (context_state -> bool) ->
(context_state -> int) -> context_tactic -> context_tactic
val CBEST_FIRST: (context_state -> bool) -> (context_state -> int) ->
context_tactic -> context_tactic
val CTHEN_ASTAR: context_tactic -> (context_state -> bool) ->
(int -> context_state -> int) -> context_tactic -> context_tactic
val CASTAR: (context_state -> bool) -> (int -> context_state -> int) ->
context_tactic -> context_tactic
end = struct
type context_tactic' = int -> context_tactic
fun CONTEXT_TACTIC' tac i (ctxt, st) = TACTIC_CONTEXT ctxt ((tac ctxt i) st)
val all_ctac = Seq.make_results o Seq.single
val no_ctac = K Seq.empty
fun print_ctac f (ctxt, st) = CONTEXT_TACTIC (print_tac ctxt (f ctxt)) (ctxt, st)
fun (ctac1 CTHEN ctac2) cst = Seq.maps_results ctac2 (ctac1 cst)
fun (ctac1 CORELSE ctac2) cst =
(case Seq.pull (ctac1 cst) of
NONE => ctac2 cst
| some => Seq.make (fn () => some))
fun (ctac1 CAPPEND ctac2) cst =
Seq.append (ctac1 cst) (Seq.make (fn () => Seq.pull (ctac2 cst)))
fun (ctac1 CTHEN' ctac2) x = ctac1 x CTHEN ctac2 x
fun (ctac1 CORELSE' ctac2) x = ctac1 x CORELSE ctac2 x
fun (ctac1 CAPPEND' ctac2) x = ctac1 x CAPPEND ctac2 x
fun CTRY ctac = ctac CORELSE all_ctac
fun CREPEAT ctac =
let
fun rep qs cst =
(case Seq.pull (Seq.filter_results (ctac cst)) of
NONE => SOME (cst, Seq.make (fn () => repq qs))
| SOME (cst', q) => rep (q :: qs) cst')
and repq [] = NONE
| repq (q :: qs) =
(case Seq.pull q of
NONE => repq qs
| SOME (cst, q) => rep (q :: qs) cst);
in fn cst => Seq.make_results (Seq.make (fn () => rep [] cst)) end
fun CREPEAT1 ctac = ctac CTHEN CREPEAT ctac
fun CREPEAT_N 0 _ = no_ctac
| CREPEAT_N n ctac = ctac CTHEN CREPEAT_N (n - 1) ctac
fun CFILTER pred ctac cst =
ctac cst
|> Seq.filter_results
|> Seq.filter pred
|> Seq.make_results
(*Only accept next states where the subgoals have changed*)
fun CCHANGED ctac (cst as (_, st)) =
CFILTER (fn (_, st') => not (Thm.eq_thm (st, st'))) ctac cst
local
fun op THEN (f, g) x = Seq.maps_results g (f x)
fun INTERVAL f i j x =
if i > j then Seq.make_results (Seq.single x)
else op THEN (f j, INTERVAL f i (j - 1)) x
(*By Peter Lammich: apply tactic to subgoals in interval in a forward manner,
skipping over emerging subgoals*)
fun INTERVAL_FWD ctac l u (cst as (_, st)) = cst |>
(if l > u then all_ctac
else (ctac l CTHEN (fn cst' as (_, st') =>
let val ofs = Thm.nprems_of st' - Thm.nprems_of st in
if ofs < ~1
then raise THM (
"INTERVAL_FWD: tactic solved more than one goal", ~1, [st, st'])
else INTERVAL_FWD ctac (l + 1 + ofs) (u + ofs) cst'
end)))
in
fun (ctac1 CTHEN_ALL_NEW ctac2) i (cst as (_, st)) =
cst |> (ctac1 i CTHEN (fn cst' as (_, st') =>
INTERVAL ctac2 i (i + Thm.nprems_of st' - Thm.nprems_of st) cst'))
(*By Peter Lammich: apply ctac2 to all subgoals emerging from ctac1, in forward
manner*)
fun (ctac1 CTHEN_ALL_NEW_FWD ctac2) i (cst as (_, st)) =
cst |> (ctac1 i CTHEN (fn cst' as (_, st') =>
INTERVAL_FWD ctac2 i (i + Thm.nprems_of st' - Thm.nprems_of st) cst'))
(*Repeatedly apply ctac to the i-th until the k-th-from-last subgoals
(i.e. leave the last k subgoals alone), until no more changes appear in the
goal state.*)
fun CREPEAT_IN_RANGE i k ctac =
let fun interval_ctac (cst as (_, st)) =
INTERVAL_FWD ctac i (Thm.nprems_of st - k) cst
in CREPEAT (CCHANGED interval_ctac) end
end
fun CREPEAT_ALL_NEW ctac =
ctac CTHEN_ALL_NEW (CTRY o (fn i => CREPEAT_ALL_NEW ctac i))
fun CREPEAT_ALL_NEW_FWD ctac =
ctac CTHEN_ALL_NEW_FWD (CTRY o (fn i => CREPEAT_ALL_NEW_FWD ctac i))
fun CHEADGOAL ctac = ctac 1
fun CALLGOALS ctac (cst as (_, st)) =
let
fun doall 0 = all_ctac
| doall n = ctac n CTHEN doall (n - 1);
in doall (Thm.nprems_of st) cst end
fun CSOMEGOAL ctac (cst as (_, st)) =
let
fun find 0 = no_ctac
| find n = ctac n CORELSE find (n - 1);
in find (Thm.nprems_of st) cst end
fun CRANGE [] _ = all_ctac
| CRANGE (ctac :: ctacs) i = CRANGE ctacs (i + 1) CTHEN ctac i
fun CFIRST ctacs = fold_rev (curry op CORELSE) ctacs no_ctac
(*FIRST' [tac1,...,tacn] i equals tac1 i ORELSE ... ORELSE tacn i*)
fun CFIRST' ctacs = fold_rev (curry op CORELSE') ctacs (K no_ctac)
(** Search tacticals **)
(* Best-first search *)
structure Thm_Heap = Heap (
type elem = int * thm;
val ord = prod_ord int_ord (Term_Ord.term_ord o apply2 Thm.prop_of)
)
structure Context_State_Heap = Heap (
type elem = int * context_state;
val ord = prod_ord int_ord (Term_Ord.term_ord o apply2 (Thm.prop_of o #2))
)
fun some_of_list [] = NONE
| some_of_list (x :: l) = SOME (x, Seq.make (fn () => some_of_list l))
(*Check for and delete duplicate proof states*)
fun delete_all_min (cst as (_, st)) heap =
if Context_State_Heap.is_empty heap then heap
else if Thm.eq_thm (st, #2 (#2 (Context_State_Heap.min heap)))
then delete_all_min cst (Context_State_Heap.delete_min heap)
else heap
(*Best-first search for a state that satisfies satp (incl initial state)
Function sizef estimates size of problem remaining (smaller means better).
tactic tac0 sets up the initial priority queue, while tac1 searches it. *)
fun CTHEN_BEST_FIRST ctac0 satp sizef ctac =
let
fun pairsize cst = (sizef cst, cst);
fun bfs (news, nst_heap) =
(case List.partition satp news of
([], nonsats) => next (fold_rev Context_State_Heap.insert (map pairsize nonsats) nst_heap)
| (sats, _) => some_of_list sats)
and next nst_heap =
if Context_State_Heap.is_empty nst_heap then NONE
else
let
val (n, cst) = Context_State_Heap.min nst_heap;
in
bfs (Seq.list_of (Seq.filter_results (ctac cst)), delete_all_min cst (Context_State_Heap.delete_min nst_heap))
end;
fun btac cst = bfs (Seq.list_of (Seq.filter_results (ctac0 cst)), Context_State_Heap.empty)
in fn cst => Seq.make_results (Seq.make (fn () => btac cst)) end
(*Ordinary best-first search, with no initial tactic*)
val CBEST_FIRST = CTHEN_BEST_FIRST all_ctac
(* A*-like search *)
(*Insertion into priority queue of states, marked with level*)
fun insert_with_level (lnth: int * int * context_state) [] = [lnth]
| insert_with_level (l, m, cst) ((l', n, cst') :: csts) =
if n < m then (l', n, cst') :: insert_with_level (l, m, cst) csts
else if n = m andalso Thm.eq_thm (#2 cst, #2 cst') then (l', n, cst') :: csts
else (l, m, cst) :: (l', n, cst') :: csts;
fun CTHEN_ASTAR ctac0 satp costf ctac =
let
fun bfs (news, nst, level) =
let fun cost cst = (level, costf level cst, cst) in
(case List.partition satp news of
([], nonsats) => next (fold_rev (insert_with_level o cost) nonsats nst)
| (sats, _) => some_of_list sats)
end
and next [] = NONE
| next ((level, n, cst) :: nst) =
bfs (Seq.list_of (Seq.filter_results (ctac cst)), nst, level + 1)
in fn cst => Seq.make_results
(Seq.make (fn () => bfs (Seq.list_of (Seq.filter_results (ctac0 cst)), [], 0)))
end
(*Ordinary ASTAR, with no initial tactic*)
val CASTAR = CTHEN_ASTAR all_ctac;
end
open Context_Tactical
|
