1 (* Title: HOL/ex/meson |
1 (* Title: HOL/Tools/meson.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1992 University of Cambridge |
4 Copyright 1992 University of Cambridge |
5 |
5 |
6 The MESON resolution proof procedure for HOL |
6 The MESON resolution proof procedure for HOL. |
7 |
7 |
8 When making clauses, avoids using the rewriter -- instead uses RS recursively |
8 When making clauses, avoids using the rewriter -- instead uses RS recursively |
9 |
9 |
10 NEED TO SORT LITERALS BY # OF VARS, USING ==>I/E. ELIMINATES NEED FOR |
10 NEED TO SORT LITERALS BY # OF VARS, USING ==>I/E. ELIMINATES NEED FOR |
11 FUNCTION nodups -- if done to goal clauses too! |
11 FUNCTION nodups -- if done to goal clauses too! |
12 *) |
12 *) |
13 |
13 |
14 |
|
15 (**** LEMMAS : outside the "local" block ****) |
|
16 |
|
17 (** "Axiom" of Choice, proved using the description operator **) |
|
18 |
|
19 Goal "ALL x. EX y. Q x y ==> EX f. ALL x. Q x (f x)"; |
|
20 by (fast_tac (claset() addEs [selectI]) 1); |
|
21 qed "choice"; |
|
22 |
|
23 (*** Generation of contrapositives ***) |
|
24 |
|
25 (*Inserts negated disjunct after removing the negation; P is a literal*) |
|
26 val [major,minor] = Goal "~P|Q ==> ((~P==>P) ==> Q)"; |
|
27 by (rtac (major RS disjE) 1); |
|
28 by (rtac notE 1); |
|
29 by (etac minor 2); |
|
30 by (ALLGOALS assume_tac); |
|
31 qed "make_neg_rule"; |
|
32 |
|
33 (*For Plaisted's "Postive refinement" of the MESON procedure*) |
|
34 Goal "~P|Q ==> (P ==> Q)"; |
|
35 by (Blast_tac 1); |
|
36 qed "make_refined_neg_rule"; |
|
37 |
|
38 (*P should be a literal*) |
|
39 val [major,minor] = Goal "P|Q ==> ((P==>~P) ==> Q)"; |
|
40 by (rtac (major RS disjE) 1); |
|
41 by (rtac notE 1); |
|
42 by (etac minor 1); |
|
43 by (ALLGOALS assume_tac); |
|
44 qed "make_pos_rule"; |
|
45 |
|
46 (*** Generation of a goal clause -- put away the final literal ***) |
|
47 |
|
48 val [major,minor] = Goal "~P ==> ((~P==>P) ==> False)"; |
|
49 by (rtac notE 1); |
|
50 by (rtac minor 2); |
|
51 by (ALLGOALS (rtac major)); |
|
52 qed "make_neg_goal"; |
|
53 |
|
54 val [major,minor] = Goal "P ==> ((P==>~P) ==> False)"; |
|
55 by (rtac notE 1); |
|
56 by (rtac minor 1); |
|
57 by (ALLGOALS (rtac major)); |
|
58 qed "make_pos_goal"; |
|
59 |
|
60 |
|
61 (**** Lemmas for forward proof (like congruence rules) ****) |
|
62 |
|
63 (*NOTE: could handle conjunctions (faster?) by |
|
64 nf(th RS conjunct2) RS (nf(th RS conjunct1) RS conjI) *) |
|
65 val major::prems = Goal |
|
66 "[| P'&Q'; P' ==> P; Q' ==> Q |] ==> P&Q"; |
|
67 by (rtac (major RS conjE) 1); |
|
68 by (rtac conjI 1); |
|
69 by (ALLGOALS (eresolve_tac prems)); |
|
70 qed "conj_forward"; |
|
71 |
|
72 val major::prems = Goal |
|
73 "[| P'|Q'; P' ==> P; Q' ==> Q |] ==> P|Q"; |
|
74 by (rtac (major RS disjE) 1); |
|
75 by (ALLGOALS (dresolve_tac prems)); |
|
76 by (ALLGOALS (eresolve_tac [disjI1,disjI2])); |
|
77 qed "disj_forward"; |
|
78 |
|
79 (*Version for removal of duplicate literals*) |
|
80 val major::prems = Goal |
|
81 "[| P'|Q'; P' ==> P; [| Q'; P==>False |] ==> Q |] ==> P|Q"; |
|
82 by (cut_facts_tac [major] 1); |
|
83 by (blast_tac (claset() addIs prems) 1); |
|
84 qed "disj_forward2"; |
|
85 |
|
86 val major::prems = Goal |
|
87 "[| ALL x. P'(x); !!x. P'(x) ==> P(x) |] ==> ALL x. P(x)"; |
|
88 by (rtac allI 1); |
|
89 by (resolve_tac prems 1); |
|
90 by (rtac (major RS spec) 1); |
|
91 qed "all_forward"; |
|
92 |
|
93 val major::prems = Goal |
|
94 "[| EX x. P'(x); !!x. P'(x) ==> P(x) |] ==> EX x. P(x)"; |
|
95 by (rtac (major RS exE) 1); |
|
96 by (rtac exI 1); |
|
97 by (eresolve_tac prems 1); |
|
98 qed "ex_forward"; |
|
99 |
|
100 (**** END OF LEMMAS ****) |
|
101 |
|
102 local |
14 local |
103 |
15 |
104 (*Prove theorems using fast_tac*) |
16 (*Prove theorems using fast_tac*) |
105 fun prove_fun s = |
17 fun prove_fun s = |
106 prove_goal (the_context ()) s |
18 prove_goal (the_context ()) s |
107 (fn prems => [ cut_facts_tac prems 1, Fast_tac 1 ]); |
19 (fn prems => [ cut_facts_tac prems 1, Fast_tac 1 ]); |
108 |
20 |
109 (**** Negation Normal Form ****) |
21 (**** Negation Normal Form ****) |
110 |
22 |
111 (*** de Morgan laws ***) |
23 (*** de Morgan laws ***) |
112 |
24 |
195 (*to detect, and remove, tautologous clauses*) |
107 (*to detect, and remove, tautologous clauses*) |
196 fun taut_lits [] = false |
108 fun taut_lits [] = false |
197 | taut_lits ((flg,t)::ts) = (not flg,t) mem ts orelse taut_lits ts; |
109 | taut_lits ((flg,t)::ts) = (not flg,t) mem ts orelse taut_lits ts; |
198 |
110 |
199 (*Include False as a literal: an occurrence of ~False is a tautology*) |
111 (*Include False as a literal: an occurrence of ~False is a tautology*) |
200 fun is_taut th = taut_lits ((true, HOLogic.false_const) :: |
112 fun is_taut th = taut_lits ((true, HOLogic.false_const) :: |
201 literals (prop_of th)); |
113 literals (prop_of th)); |
202 |
114 |
203 (*Generation of unique names -- maxidx cannot be relied upon to increase! |
115 (*Generation of unique names -- maxidx cannot be relied upon to increase! |
204 Cannot rely on "variant", since variables might coincide when literals |
116 Cannot rely on "variant", since variables might coincide when literals |
205 are joined to make a clause... |
117 are joined to make a clause... |
206 19 chooses "U" as the first variable name*) |
118 19 chooses "U" as the first variable name*) |
207 val name_ref = ref 19; |
119 val name_ref = ref 19; |
208 |
120 |
209 (*Replaces universally quantified variables by FREE variables -- because |
121 (*Replaces universally quantified variables by FREE variables -- because |
210 assumptions may not contain scheme variables. Later, call "generalize". *) |
122 assumptions may not contain scheme variables. Later, call "generalize". *) |
211 fun freeze_spec th = |
123 fun freeze_spec th = |
212 let val sth = th RS spec |
124 let val sth = th RS spec |
213 val newname = (name_ref := !name_ref + 1; |
125 val newname = (name_ref := !name_ref + 1; |
214 radixstring(26, "A", !name_ref)) |
126 radixstring(26, "A", !name_ref)) |
215 in read_instantiate [("x", newname)] sth end; |
127 in read_instantiate [("x", newname)] sth end; |
216 |
128 |
217 fun resop nf [prem] = resolve_tac (nf prem) 1; |
129 fun resop nf [prem] = resolve_tac (nf prem) 1; |
218 |
130 |
219 (*Conjunctive normal form, detecting tautologies early. |
131 (*Conjunctive normal form, detecting tautologies early. |
220 Strips universal quantifiers and breaks up conjunctions. *) |
132 Strips universal quantifiers and breaks up conjunctions. *) |
221 fun cnf_aux seen (th,ths) = |
133 fun cnf_aux seen (th,ths) = |
222 if taut_lits (literals(prop_of th) @ seen) then ths |
134 if taut_lits (literals(prop_of th) @ seen) then ths |
223 else if not (has_consts ["All","op &"] (prop_of th)) then th::ths |
135 else if not (has_consts ["All","op &"] (prop_of th)) then th::ths |
224 else (*conjunction?*) |
136 else (*conjunction?*) |
225 cnf_aux seen (th RS conjunct1, |
137 cnf_aux seen (th RS conjunct1, |
226 cnf_aux seen (th RS conjunct2, ths)) |
138 cnf_aux seen (th RS conjunct2, ths)) |
227 handle THM _ => (*universal quant?*) |
139 handle THM _ => (*universal quant?*) |
228 cnf_aux seen (freeze_spec th, ths) |
140 cnf_aux seen (freeze_spec th, ths) |
229 handle THM _ => (*disjunction?*) |
141 handle THM _ => (*disjunction?*) |
230 let val tac = |
142 let val tac = |
231 (METAHYPS (resop (cnf_nil seen)) 1) THEN |
143 (METAHYPS (resop (cnf_nil seen)) 1) THEN |
232 (fn st' => st' |> |
144 (fn st' => st' |> |
233 METAHYPS (resop (cnf_nil (literals (concl_of st') @ seen))) 1) |
145 METAHYPS (resop (cnf_nil (literals (concl_of st') @ seen))) 1) |
234 in Seq.list_of (tac (th RS disj_forward)) @ ths end |
146 in Seq.list_of (tac (th RS disj_forward)) @ ths end |
235 and cnf_nil seen th = cnf_aux seen (th,[]); |
147 and cnf_nil seen th = cnf_aux seen (th,[]); |
236 |
148 |
237 (*Top-level call to cnf -- it's safe to reset name_ref*) |
149 (*Top-level call to cnf -- it's safe to reset name_ref*) |
238 fun cnf (th,ths) = |
150 fun cnf (th,ths) = |
239 (name_ref := 19; cnf (th RS conjunct1, cnf (th RS conjunct2, ths)) |
151 (name_ref := 19; cnf (th RS conjunct1, cnf (th RS conjunct2, ths)) |
240 handle THM _ => (*not a conjunction*) cnf_aux [] (th, ths)); |
152 handle THM _ => (*not a conjunction*) cnf_aux [] (th, ths)); |
241 |
153 |
242 (**** Removal of duplicate literals ****) |
154 (**** Removal of duplicate literals ****) |
243 |
155 |
244 (*Forward proof, passing extra assumptions as theorems to the tactic*) |
156 (*Forward proof, passing extra assumptions as theorems to the tactic*) |
245 fun forward_res2 nf hyps st = |
157 fun forward_res2 nf hyps st = |
246 case Seq.pull |
158 case Seq.pull |
247 (REPEAT |
159 (REPEAT |
248 (METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1) |
160 (METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1) |
249 st) |
161 st) |
250 of Some(th,_) => th |
162 of Some(th,_) => th |
251 | None => raise THM("forward_res2", 0, [st]); |
163 | None => raise THM("forward_res2", 0, [st]); |
252 |
164 |
253 (*Remove duplicates in P|Q by assuming ~P in Q |
165 (*Remove duplicates in P|Q by assuming ~P in Q |
254 rls (initially []) accumulates assumptions of the form P==>False*) |
166 rls (initially []) accumulates assumptions of the form P==>False*) |
255 fun nodups_aux rls th = nodups_aux rls (th RS disj_assoc) |
167 fun nodups_aux rls th = nodups_aux rls (th RS disj_assoc) |
256 handle THM _ => tryres(th,rls) |
168 handle THM _ => tryres(th,rls) |
257 handle THM _ => tryres(forward_res2 nodups_aux rls (th RS disj_forward2), |
169 handle THM _ => tryres(forward_res2 nodups_aux rls (th RS disj_forward2), |
258 [disj_FalseD1, disj_FalseD2, asm_rl]) |
170 [disj_FalseD1, disj_FalseD2, asm_rl]) |
259 handle THM _ => th; |
171 handle THM _ => th; |
260 |
172 |
261 (*Remove duplicate literals, if there are any*) |
173 (*Remove duplicate literals, if there are any*) |
262 fun nodups th = |
174 fun nodups th = |
263 if null(findrep(literals(prop_of th))) then th |
175 if null(findrep(literals(prop_of th))) then th |
266 |
178 |
267 (**** Generation of contrapositives ****) |
179 (**** Generation of contrapositives ****) |
268 |
180 |
269 (*Associate disjuctions to right -- make leftmost disjunct a LITERAL*) |
181 (*Associate disjuctions to right -- make leftmost disjunct a LITERAL*) |
270 fun assoc_right th = assoc_right (th RS disj_assoc) |
182 fun assoc_right th = assoc_right (th RS disj_assoc) |
271 handle THM _ => th; |
183 handle THM _ => th; |
272 |
184 |
273 (*Must check for negative literal first!*) |
185 (*Must check for negative literal first!*) |
274 val clause_rules = [disj_assoc, make_neg_rule, make_pos_rule]; |
186 val clause_rules = [disj_assoc, make_neg_rule, make_pos_rule]; |
275 |
187 |
276 (*For Plaisted's postive refinement. [currently unused] *) |
188 (*For Plaisted's postive refinement. [currently unused] *) |
277 val refined_clause_rules = [disj_assoc, make_refined_neg_rule, make_pos_rule]; |
189 val refined_clause_rules = [disj_assoc, make_refined_neg_rule, make_pos_rule]; |
278 |
190 |
279 (*Create a goal or support clause, conclusing False*) |
191 (*Create a goal or support clause, conclusing False*) |
280 fun make_goal th = (*Must check for negative literal first!*) |
192 fun make_goal th = (*Must check for negative literal first!*) |
281 make_goal (tryres(th, clause_rules)) |
193 make_goal (tryres(th, clause_rules)) |
282 handle THM _ => tryres(th, [make_neg_goal, make_pos_goal]); |
194 handle THM _ => tryres(th, [make_neg_goal, make_pos_goal]); |
283 |
195 |
284 (*Sort clauses by number of literals*) |
196 (*Sort clauses by number of literals*) |
285 fun fewerlits(th1,th2) = nliterals(prop_of th1) < nliterals(prop_of th2); |
197 fun fewerlits(th1,th2) = nliterals(prop_of th1) < nliterals(prop_of th2); |
286 |
198 |
289 |
201 |
290 (*Convert all suitable free variables to schematic variables*) |
202 (*Convert all suitable free variables to schematic variables*) |
291 fun generalize th = forall_elim_vars 0 (forall_intr_frees th); |
203 fun generalize th = forall_elim_vars 0 (forall_intr_frees th); |
292 |
204 |
293 (*Create a meta-level Horn clause*) |
205 (*Create a meta-level Horn clause*) |
294 fun make_horn crules th = make_horn crules (tryres(th,crules)) |
206 fun make_horn crules th = make_horn crules (tryres(th,crules)) |
295 handle THM _ => th; |
207 handle THM _ => th; |
296 |
208 |
297 (*Generate Horn clauses for all contrapositives of a clause*) |
209 (*Generate Horn clauses for all contrapositives of a clause*) |
298 fun add_contras crules (th,hcs) = |
210 fun add_contras crules (th,hcs) = |
299 let fun rots (0,th) = hcs |
211 let fun rots (0,th) = hcs |
300 | rots (k,th) = zero_var_indexes (make_horn crules th) :: |
212 | rots (k,th) = zero_var_indexes (make_horn crules th) :: |
301 rots(k-1, assoc_right (th RS disj_comm)) |
213 rots(k-1, assoc_right (th RS disj_comm)) |
302 in case nliterals(prop_of th) of |
214 in case nliterals(prop_of th) of |
303 1 => th::hcs |
215 1 => th::hcs |
304 | n => rots(n, assoc_right th) |
216 | n => rots(n, assoc_right th) |
305 end; |
217 end; |
306 |
218 |
307 (*Use "theorem naming" to label the clauses*) |
219 (*Use "theorem naming" to label the clauses*) |
308 fun name_thms label = |
220 fun name_thms label = |
309 let fun name1 (th, (k,ths)) = |
221 let fun name1 (th, (k,ths)) = |
310 (k-1, Thm.name_thm (label ^ string_of_int k, th) :: ths) |
222 (k-1, Thm.name_thm (label ^ string_of_int k, th) :: ths) |
311 |
223 |
312 in fn ths => #2 (foldr name1 (ths, (length ths, []))) end; |
224 in fn ths => #2 (foldr name1 (ths, (length ths, []))) end; |
313 |
225 |
314 (*Find an all-negative support clause*) |
226 (*Find an all-negative support clause*) |
315 fun is_negative th = forall (not o #1) (literals (prop_of th)); |
227 fun is_negative th = forall (not o #1) (literals (prop_of th)); |
331 (*detects repetitions in a list of terms*) |
243 (*detects repetitions in a list of terms*) |
332 fun has_reps [] = false |
244 fun has_reps [] = false |
333 | has_reps [_] = false |
245 | has_reps [_] = false |
334 | has_reps [t,u] = (t aconv u) |
246 | has_reps [t,u] = (t aconv u) |
335 | has_reps ts = (foldl ins_term (Net.empty, ts); false) |
247 | has_reps ts = (foldl ins_term (Net.empty, ts); false) |
336 handle INSERT => true; |
248 handle INSERT => true; |
337 |
249 |
338 (*Like TRYALL eq_assume_tac, but avoids expensive THEN calls*) |
250 (*Like TRYALL eq_assume_tac, but avoids expensive THEN calls*) |
339 fun TRYALL_eq_assume_tac 0 st = Seq.single st |
251 fun TRYALL_eq_assume_tac 0 st = Seq.single st |
340 | TRYALL_eq_assume_tac i st = |
252 | TRYALL_eq_assume_tac i st = |
341 TRYALL_eq_assume_tac (i-1) (eq_assumption i st) |
253 TRYALL_eq_assume_tac (i-1) (eq_assumption i st) |
342 handle THM _ => TRYALL_eq_assume_tac (i-1) st; |
254 handle THM _ => TRYALL_eq_assume_tac (i-1) st; |
343 |
255 |
344 (*Loop checking: FAIL if trying to prove the same thing twice |
256 (*Loop checking: FAIL if trying to prove the same thing twice |
345 -- if *ANY* subgoal has repeated literals*) |
257 -- if *ANY* subgoal has repeated literals*) |
346 fun check_tac st = |
258 fun check_tac st = |
347 if exists (fn prem => has_reps (rhyps(prem,[]))) (prems_of st) |
259 if exists (fn prem => has_reps (rhyps(prem,[]))) (prems_of st) |
348 then Seq.empty else Seq.single st; |
260 then Seq.empty else Seq.single st; |
349 |
261 |
350 |
262 |
351 (* net_resolve_tac actually made it slower... *) |
263 (* net_resolve_tac actually made it slower... *) |
352 fun prolog_step_tac horns i = |
264 fun prolog_step_tac horns i = |
353 (assume_tac i APPEND resolve_tac horns i) THEN check_tac THEN |
265 (assume_tac i APPEND resolve_tac horns i) THEN check_tac THEN |
354 TRYALL eq_assume_tac; |
266 TRYALL eq_assume_tac; |
355 |
267 |
356 |
268 |
357 in |
269 in |
363 fun size_of_subgoals st = foldr addconcl (prems_of st, 0) |
275 fun size_of_subgoals st = foldr addconcl (prems_of st, 0) |
364 end; |
276 end; |
365 |
277 |
366 (*Negation Normal Form*) |
278 (*Negation Normal Form*) |
367 val nnf_rls = [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD, |
279 val nnf_rls = [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD, |
368 not_impD, not_iffD, not_allD, not_exD, not_notD]; |
280 not_impD, not_iffD, not_allD, not_exD, not_notD]; |
369 fun make_nnf th = make_nnf (tryres(th, nnf_rls)) |
281 fun make_nnf th = make_nnf (tryres(th, nnf_rls)) |
370 handle THM _ => |
282 handle THM _ => |
371 forward_res make_nnf |
283 forward_res make_nnf |
372 (tryres(th, [conj_forward,disj_forward,all_forward,ex_forward])) |
284 (tryres(th, [conj_forward,disj_forward,all_forward,ex_forward])) |
373 handle THM _ => th; |
285 handle THM _ => th; |
374 |
286 |
375 (*Pull existential quantifiers (Skolemization)*) |
287 (*Pull existential quantifiers (Skolemization)*) |
376 fun skolemize th = |
288 fun skolemize th = |
377 if not (has_consts ["Ex"] (prop_of th)) then th |
289 if not (has_consts ["Ex"] (prop_of th)) then th |
378 else skolemize (tryres(th, [choice, conj_exD1, conj_exD2, |
290 else skolemize (tryres(th, [choice, conj_exD1, conj_exD2, |
379 disj_exD, disj_exD1, disj_exD2])) |
291 disj_exD, disj_exD1, disj_exD2])) |
380 handle THM _ => |
292 handle THM _ => |
381 skolemize (forward_res skolemize |
293 skolemize (forward_res skolemize |
382 (tryres (th, [conj_forward, disj_forward, all_forward]))) |
294 (tryres (th, [conj_forward, disj_forward, all_forward]))) |
383 handle THM _ => forward_res skolemize (th RS ex_forward); |
295 handle THM _ => forward_res skolemize (th RS ex_forward); |
384 |
296 |
385 |
297 |
386 (*Make clauses from a list of theorems, previously Skolemized and put into nnf. |
298 (*Make clauses from a list of theorems, previously Skolemized and put into nnf. |
387 The resulting clauses are HOL disjunctions.*) |
299 The resulting clauses are HOL disjunctions.*) |
388 fun make_clauses ths = |
300 fun make_clauses ths = |
389 sort_clauses (map (generalize o nodups) (foldr cnf (ths,[]))); |
301 sort_clauses (map (generalize o nodups) (foldr cnf (ths,[]))); |
390 |
302 |
391 (*Convert a list of clauses to (contrapositive) Horn clauses*) |
303 (*Convert a list of clauses to (contrapositive) Horn clauses*) |
392 fun make_horns ths = |
304 fun make_horns ths = |
393 name_thms "Horn#" |
305 name_thms "Horn#" |
394 (gen_distinct eq_thm (foldr (add_contras clause_rules) (ths,[]))); |
306 (gen_distinct eq_thm (foldr (add_contras clause_rules) (ths,[]))); |
395 |
307 |
396 (*Could simply use nprems_of, which would count remaining subgoals -- no |
308 (*Could simply use nprems_of, which would count remaining subgoals -- no |
397 discrimination as to their size! With BEST_FIRST, fails for problem 41.*) |
309 discrimination as to their size! With BEST_FIRST, fails for problem 41.*) |
398 |
310 |
399 fun best_prolog_tac sizef horns = |
311 fun best_prolog_tac sizef horns = |
400 BEST_FIRST (has_fewer_prems 1, sizef) (prolog_step_tac horns 1); |
312 BEST_FIRST (has_fewer_prems 1, sizef) (prolog_step_tac horns 1); |
401 |
313 |
402 fun depth_prolog_tac horns = |
314 fun depth_prolog_tac horns = |
403 DEPTH_FIRST (has_fewer_prems 1) (prolog_step_tac horns 1); |
315 DEPTH_FIRST (has_fewer_prems 1) (prolog_step_tac horns 1); |
404 |
316 |
405 (*Return all negative clauses, as possible goal clauses*) |
317 (*Return all negative clauses, as possible goal clauses*) |
406 fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls)); |
318 fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls)); |
407 |
319 |
408 |
320 |
409 fun skolemize_tac prems = |
321 fun skolemize_tac prems = |
410 cut_facts_tac (map (skolemize o make_nnf) prems) THEN' |
322 cut_facts_tac (map (skolemize o make_nnf) prems) THEN' |
411 REPEAT o (etac exE); |
323 REPEAT o (etac exE); |
412 |
324 |
413 (*Shell of all meson-tactics. Supplies cltac with clauses: HOL disjunctions*) |
325 (*Shell of all meson-tactics. Supplies cltac with clauses: HOL disjunctions*) |
414 fun MESON cltac = SELECT_GOAL |
326 fun MESON cltac = SELECT_GOAL |
417 EVERY1 [skolemize_tac negs, |
329 EVERY1 [skolemize_tac negs, |
418 METAHYPS (cltac o make_clauses)])]); |
330 METAHYPS (cltac o make_clauses)])]); |
419 |
331 |
420 (** Best-first search versions **) |
332 (** Best-first search versions **) |
421 |
333 |
422 fun best_meson_tac sizef = |
334 fun best_meson_tac sizef = |
423 MESON (fn cls => |
335 MESON (fn cls => |
424 THEN_BEST_FIRST (resolve_tac (gocls cls) 1) |
336 THEN_BEST_FIRST (resolve_tac (gocls cls) 1) |
425 (has_fewer_prems 1, sizef) |
337 (has_fewer_prems 1, sizef) |
426 (prolog_step_tac (make_horns cls) 1)); |
338 (prolog_step_tac (make_horns cls) 1)); |
427 |
339 |
428 (*First, breaks the goal into independent units*) |
340 (*First, breaks the goal into independent units*) |
429 val safe_best_meson_tac = |
341 val safe_best_meson_tac = |
430 SELECT_GOAL (TRY Safe_tac THEN |
342 SELECT_GOAL (TRY Safe_tac THEN |
431 TRYALL (best_meson_tac size_of_subgoals)); |
343 TRYALL (best_meson_tac size_of_subgoals)); |
432 |
344 |
433 (** Depth-first search version **) |
345 (** Depth-first search version **) |
434 |
346 |
435 val depth_meson_tac = |
347 val depth_meson_tac = |
436 MESON (fn cls => EVERY [resolve_tac (gocls cls) 1, |
348 MESON (fn cls => EVERY [resolve_tac (gocls cls) 1, |
437 depth_prolog_tac (make_horns cls)]); |
349 depth_prolog_tac (make_horns cls)]); |
438 |
350 |
439 |
351 |
440 |
352 |
441 (** Iterative deepening version **) |
353 (** Iterative deepening version **) |
442 |
354 |
443 (*This version does only one inference per call; |
355 (*This version does only one inference per call; |
444 having only one eq_assume_tac speeds it up!*) |
356 having only one eq_assume_tac speeds it up!*) |
445 fun prolog_step_tac' horns = |
357 fun prolog_step_tac' horns = |
446 let val (horn0s, hornps) = (*0 subgoals vs 1 or more*) |
358 let val (horn0s, hornps) = (*0 subgoals vs 1 or more*) |
447 take_prefix Thm.no_prems horns |
359 take_prefix Thm.no_prems horns |
448 val nrtac = net_resolve_tac horns |
360 val nrtac = net_resolve_tac horns |
449 in fn i => eq_assume_tac i ORELSE |
361 in fn i => eq_assume_tac i ORELSE |
450 match_tac horn0s i ORELSE (*no backtracking if unit MATCHES*) |
362 match_tac horn0s i ORELSE (*no backtracking if unit MATCHES*) |
451 ((assume_tac i APPEND nrtac i) THEN check_tac) |
363 ((assume_tac i APPEND nrtac i) THEN check_tac) |
452 end; |
364 end; |
453 |
365 |
454 fun iter_deepen_prolog_tac horns = |
366 fun iter_deepen_prolog_tac horns = |
455 ITER_DEEPEN (has_fewer_prems 1) (prolog_step_tac' horns); |
367 ITER_DEEPEN (has_fewer_prems 1) (prolog_step_tac' horns); |
456 |
368 |
457 val iter_deepen_meson_tac = |
369 val iter_deepen_meson_tac = |
458 MESON (fn cls => |
370 MESON (fn cls => |
459 (THEN_ITER_DEEPEN (resolve_tac (gocls cls) 1) |
371 (THEN_ITER_DEEPEN (resolve_tac (gocls cls) 1) |
460 (has_fewer_prems 1) |
372 (has_fewer_prems 1) |
461 (prolog_step_tac' (make_horns cls)))); |
373 (prolog_step_tac' (make_horns cls)))); |
462 |
374 |
463 val meson_tac = |
375 fun meson_claset_tac cs = |
464 SELECT_GOAL (TRY Safe_tac THEN |
376 SELECT_GOAL (TRY (safe_tac cs) THEN TRYALL iter_deepen_meson_tac); |
465 TRYALL (iter_deepen_meson_tac)); |
377 |
|
378 val meson_tac = CLASET' meson_claset_tac; |
|
379 |
|
380 |
|
381 (* proof method setup *) |
|
382 |
|
383 local |
|
384 |
|
385 fun meson_meth ctxt = |
|
386 Method.SIMPLE_METHOD' HEADGOAL (CHANGED o meson_claset_tac (Classical.get_local_claset ctxt)); |
|
387 |
|
388 in |
|
389 |
|
390 val meson_setup = |
|
391 [Method.add_methods |
|
392 [("meson", Method.ctxt_args meson_meth, "The MESON resolution proof procedure")]]; |
466 |
393 |
467 end; |
394 end; |
|
395 |
|
396 end; |