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 local |
14 signature BASIC_MESON = |
15 |
15 sig |
16 val not_conjD = thm "meson_not_conjD"; |
16 val size_of_subgoals : thm -> int |
17 val not_disjD = thm "meson_not_disjD"; |
17 val make_nnf : thm -> thm |
18 val not_notD = thm "meson_not_notD"; |
18 val skolemize : thm -> thm |
19 val not_allD = thm "meson_not_allD"; |
19 val make_clauses : thm list -> thm list |
20 val not_exD = thm "meson_not_exD"; |
20 val make_horns : thm list -> thm list |
21 val imp_to_disjD = thm "meson_imp_to_disjD"; |
21 val best_prolog_tac : (thm -> int) -> thm list -> tactic |
22 val not_impD = thm "meson_not_impD"; |
22 val depth_prolog_tac : thm list -> tactic |
23 val iff_to_disjD = thm "meson_iff_to_disjD"; |
23 val gocls : thm list -> thm list |
24 val not_iffD = thm "meson_not_iffD"; |
24 val skolemize_prems_tac : thm list -> int -> tactic |
25 val conj_exD1 = thm "meson_conj_exD1"; |
25 val MESON : (thm list -> tactic) -> int -> tactic |
26 val conj_exD2 = thm "meson_conj_exD2"; |
26 val best_meson_tac : (thm -> int) -> int -> tactic |
27 val disj_exD = thm "meson_disj_exD"; |
27 val safe_best_meson_tac : int -> tactic |
28 val disj_exD1 = thm "meson_disj_exD1"; |
28 val depth_meson_tac : int -> tactic |
29 val disj_exD2 = thm "meson_disj_exD2"; |
29 val prolog_step_tac' : thm list -> int -> tactic |
30 val disj_assoc = thm "meson_disj_assoc"; |
30 val iter_deepen_prolog_tac : thm list -> tactic |
31 val disj_comm = thm "meson_disj_comm"; |
31 val iter_deepen_meson_tac : int -> tactic |
32 val disj_FalseD1 = thm "meson_disj_FalseD1"; |
32 val meson_tac : int -> tactic |
33 val disj_FalseD2 = thm "meson_disj_FalseD2"; |
33 val negate_head : thm -> thm |
34 |
34 val select_literal : int -> thm -> thm |
35 |
35 val skolemize_tac : int -> tactic |
36 (**** Operators for forward proof ****) |
36 val make_clauses_tac : int -> tactic |
37 |
37 val meson_setup : (theory -> theory) list |
38 (*raises exception if no rules apply -- unlike RL*) |
38 end |
39 fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls)) |
39 |
40 | tryres (th, []) = raise THM("tryres", 0, [th]); |
40 |
41 |
41 structure Meson = |
42 val prop_of = #prop o rep_thm; |
42 struct |
43 |
43 |
44 (*Permits forward proof from rules that discharge assumptions*) |
44 val not_conjD = thm "meson_not_conjD"; |
45 fun forward_res nf st = |
45 val not_disjD = thm "meson_not_disjD"; |
46 case Seq.pull (ALLGOALS (METAHYPS (fn [prem] => rtac (nf prem) 1)) st) |
46 val not_notD = thm "meson_not_notD"; |
47 of SOME(th,_) => th |
47 val not_allD = thm "meson_not_allD"; |
48 | NONE => raise THM("forward_res", 0, [st]); |
48 val not_exD = thm "meson_not_exD"; |
49 |
49 val imp_to_disjD = thm "meson_imp_to_disjD"; |
50 |
50 val not_impD = thm "meson_not_impD"; |
51 (*Are any of the constants in "bs" present in the term?*) |
51 val iff_to_disjD = thm "meson_iff_to_disjD"; |
52 fun has_consts bs = |
52 val not_iffD = thm "meson_not_iffD"; |
53 let fun has (Const(a,_)) = a mem bs |
53 val conj_exD1 = thm "meson_conj_exD1"; |
54 | has (Const ("Hilbert_Choice.Eps",_) $ _) = false |
54 val conj_exD2 = thm "meson_conj_exD2"; |
55 (*ignore constants within @-terms*) |
55 val disj_exD = thm "meson_disj_exD"; |
56 | has (f$u) = has f orelse has u |
56 val disj_exD1 = thm "meson_disj_exD1"; |
57 | has (Abs(_,_,t)) = has t |
57 val disj_exD2 = thm "meson_disj_exD2"; |
58 | has _ = false |
58 val disj_assoc = thm "meson_disj_assoc"; |
59 in has end; |
59 val disj_comm = thm "meson_disj_comm"; |
60 |
60 val disj_FalseD1 = thm "meson_disj_FalseD1"; |
61 |
61 val disj_FalseD2 = thm "meson_disj_FalseD2"; |
62 (**** Clause handling ****) |
62 |
63 |
63 |
64 fun literals (Const("Trueprop",_) $ P) = literals P |
64 (**** Operators for forward proof ****) |
65 | literals (Const("op |",_) $ P $ Q) = literals P @ literals Q |
65 |
66 | literals (Const("Not",_) $ P) = [(false,P)] |
66 (*raises exception if no rules apply -- unlike RL*) |
67 | literals P = [(true,P)]; |
67 fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls)) |
68 |
68 | tryres (th, []) = raise THM("tryres", 0, [th]); |
69 (*number of literals in a term*) |
69 |
70 val nliterals = length o literals; |
70 val prop_of = #prop o rep_thm; |
71 |
71 |
72 (*to detect, and remove, tautologous clauses*) |
72 (*Permits forward proof from rules that discharge assumptions*) |
73 fun taut_lits [] = false |
73 fun forward_res nf st = |
74 | taut_lits ((flg,t)::ts) = (not flg,t) mem ts orelse taut_lits ts; |
74 case Seq.pull (ALLGOALS (METAHYPS (fn [prem] => rtac (nf prem) 1)) st) |
75 |
75 of SOME(th,_) => th |
76 (*Include False as a literal: an occurrence of ~False is a tautology*) |
76 | NONE => raise THM("forward_res", 0, [st]); |
77 fun is_taut th = taut_lits ((true, HOLogic.false_const) :: |
77 |
78 literals (prop_of th)); |
78 |
79 |
79 (*Are any of the constants in "bs" present in the term?*) |
80 (*Generation of unique names -- maxidx cannot be relied upon to increase! |
80 fun has_consts bs = |
81 Cannot rely on "variant", since variables might coincide when literals |
81 let fun has (Const(a,_)) = a mem bs |
82 are joined to make a clause... |
82 | has (Const ("Hilbert_Choice.Eps",_) $ _) = false |
83 19 chooses "U" as the first variable name*) |
83 (*ignore constants within @-terms*) |
84 val name_ref = ref 19; |
84 | has (f$u) = has f orelse has u |
85 |
85 | has (Abs(_,_,t)) = has t |
86 (*Replaces universally quantified variables by FREE variables -- because |
86 | has _ = false |
87 assumptions may not contain scheme variables. Later, call "generalize". *) |
87 in has end; |
88 fun freeze_spec th = |
88 |
89 let val sth = th RS spec |
89 |
90 val newname = (name_ref := !name_ref + 1; |
90 (**** Clause handling ****) |
91 radixstring(26, "A", !name_ref)) |
91 |
92 in read_instantiate [("x", newname)] sth end; |
92 fun literals (Const("Trueprop",_) $ P) = literals P |
93 |
93 | literals (Const("op |",_) $ P $ Q) = literals P @ literals Q |
94 fun resop nf [prem] = resolve_tac (nf prem) 1; |
94 | literals (Const("Not",_) $ P) = [(false,P)] |
95 |
95 | literals P = [(true,P)]; |
96 (*Conjunctive normal form, detecting tautologies early. |
96 |
97 Strips universal quantifiers and breaks up conjunctions. *) |
97 (*number of literals in a term*) |
98 fun cnf_aux seen (th,ths) = |
98 val nliterals = length o literals; |
99 if taut_lits (literals(prop_of th) @ seen) |
99 |
100 then ths (*tautology ignored*) |
100 (*to detect, and remove, tautologous clauses*) |
101 else if not (has_consts ["All","op &"] (prop_of th)) |
101 fun taut_lits [] = false |
102 then th::ths (*no work to do, terminate*) |
102 | taut_lits ((flg,t)::ts) = (not flg,t) mem ts orelse taut_lits ts; |
103 else (*conjunction?*) |
103 |
104 cnf_aux seen (th RS conjunct1, |
104 (*Include False as a literal: an occurrence of ~False is a tautology*) |
105 cnf_aux seen (th RS conjunct2, ths)) |
105 fun is_taut th = taut_lits ((true, HOLogic.false_const) :: |
106 handle THM _ => (*universal quant?*) |
106 literals (prop_of th)); |
107 cnf_aux seen (freeze_spec th, ths) |
107 |
108 handle THM _ => (*disjunction?*) |
108 (*Generation of unique names -- maxidx cannot be relied upon to increase! |
109 let val tac = |
109 Cannot rely on "variant", since variables might coincide when literals |
110 (METAHYPS (resop (cnf_nil seen)) 1) THEN |
110 are joined to make a clause... |
111 (fn st' => st' |> |
111 19 chooses "U" as the first variable name*) |
112 METAHYPS (resop (cnf_nil (literals (concl_of st') @ seen))) 1) |
112 val name_ref = ref 19; |
113 in Seq.list_of (tac (th RS disj_forward)) @ ths end |
113 |
114 and cnf_nil seen th = cnf_aux seen (th,[]); |
114 (*Replaces universally quantified variables by FREE variables -- because |
115 |
115 assumptions may not contain scheme variables. Later, call "generalize". *) |
116 (*Top-level call to cnf -- it's safe to reset name_ref*) |
116 fun freeze_spec th = |
117 fun cnf (th,ths) = |
117 let val sth = th RS spec |
118 (name_ref := 19; cnf (th RS conjunct1, cnf (th RS conjunct2, ths)) |
118 val newname = (name_ref := !name_ref + 1; |
119 handle THM _ => (*not a conjunction*) cnf_aux [] (th, ths)); |
119 radixstring(26, "A", !name_ref)) |
120 |
120 in read_instantiate [("x", newname)] sth end; |
121 (**** Removal of duplicate literals ****) |
121 |
122 |
122 fun resop nf [prem] = resolve_tac (nf prem) 1; |
123 (*Forward proof, passing extra assumptions as theorems to the tactic*) |
123 |
124 fun forward_res2 nf hyps st = |
124 (*Conjunctive normal form, detecting tautologies early. |
125 case Seq.pull |
125 Strips universal quantifiers and breaks up conjunctions. *) |
126 (REPEAT |
126 fun cnf_aux seen (th,ths) = |
127 (METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1) |
127 if taut_lits (literals(prop_of th) @ seen) |
128 st) |
128 then ths (*tautology ignored*) |
129 of SOME(th,_) => th |
129 else if not (has_consts ["All","op &"] (prop_of th)) |
130 | NONE => raise THM("forward_res2", 0, [st]); |
130 then th::ths (*no work to do, terminate*) |
131 |
131 else (*conjunction?*) |
132 (*Remove duplicates in P|Q by assuming ~P in Q |
132 cnf_aux seen (th RS conjunct1, |
133 rls (initially []) accumulates assumptions of the form P==>False*) |
133 cnf_aux seen (th RS conjunct2, ths)) |
134 fun nodups_aux rls th = nodups_aux rls (th RS disj_assoc) |
134 handle THM _ => (*universal quant?*) |
135 handle THM _ => tryres(th,rls) |
135 cnf_aux seen (freeze_spec th, ths) |
136 handle THM _ => tryres(forward_res2 nodups_aux rls (th RS disj_forward2), |
136 handle THM _ => (*disjunction?*) |
137 [disj_FalseD1, disj_FalseD2, asm_rl]) |
137 let val tac = |
138 handle THM _ => th; |
138 (METAHYPS (resop (cnf_nil seen)) 1) THEN |
139 |
139 (fn st' => st' |> |
140 (*Remove duplicate literals, if there are any*) |
140 METAHYPS (resop (cnf_nil (literals (concl_of st') @ seen))) 1) |
141 fun nodups th = |
141 in Seq.list_of (tac (th RS disj_forward)) @ ths end |
142 if null(findrep(literals(prop_of th))) then th |
142 and cnf_nil seen th = cnf_aux seen (th,[]); |
143 else nodups_aux [] th; |
143 |
144 |
144 (*Top-level call to cnf -- it's safe to reset name_ref*) |
145 |
145 fun cnf (th,ths) = |
146 (**** Generation of contrapositives ****) |
146 (name_ref := 19; cnf (th RS conjunct1, cnf (th RS conjunct2, ths)) |
147 |
147 handle THM _ => (*not a conjunction*) cnf_aux [] (th, ths)); |
148 (*Associate disjuctions to right -- make leftmost disjunct a LITERAL*) |
148 |
149 fun assoc_right th = assoc_right (th RS disj_assoc) |
149 (**** Removal of duplicate literals ****) |
150 handle THM _ => th; |
150 |
151 |
151 (*Forward proof, passing extra assumptions as theorems to the tactic*) |
152 (*Must check for negative literal first!*) |
152 fun forward_res2 nf hyps st = |
153 val clause_rules = [disj_assoc, make_neg_rule, make_pos_rule]; |
153 case Seq.pull |
154 |
154 (REPEAT |
155 (*For ordinary resolution. *) |
155 (METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1) |
156 val resolution_clause_rules = [disj_assoc, make_neg_rule', make_pos_rule']; |
156 st) |
157 |
157 of SOME(th,_) => th |
158 (*Create a goal or support clause, conclusing False*) |
158 | NONE => raise THM("forward_res2", 0, [st]); |
159 fun make_goal th = (*Must check for negative literal first!*) |
159 |
160 make_goal (tryres(th, clause_rules)) |
160 (*Remove duplicates in P|Q by assuming ~P in Q |
161 handle THM _ => tryres(th, [make_neg_goal, make_pos_goal]); |
161 rls (initially []) accumulates assumptions of the form P==>False*) |
162 |
162 fun nodups_aux rls th = nodups_aux rls (th RS disj_assoc) |
163 (*Sort clauses by number of literals*) |
163 handle THM _ => tryres(th,rls) |
164 fun fewerlits(th1,th2) = nliterals(prop_of th1) < nliterals(prop_of th2); |
164 handle THM _ => tryres(forward_res2 nodups_aux rls (th RS disj_forward2), |
165 |
165 [disj_FalseD1, disj_FalseD2, asm_rl]) |
166 (*TAUTOLOGY CHECK SHOULD NOT BE NECESSARY!*) |
166 handle THM _ => th; |
167 fun sort_clauses ths = sort (make_ord fewerlits) (List.filter (not o is_taut) ths); |
167 |
168 |
168 (*Remove duplicate literals, if there are any*) |
169 (*Convert all suitable free variables to schematic variables*) |
169 fun nodups th = |
170 fun generalize th = forall_elim_vars 0 (forall_intr_frees th); |
170 if null(findrep(literals(prop_of th))) then th |
171 |
171 else nodups_aux [] th; |
172 (*Create a meta-level Horn clause*) |
172 |
173 fun make_horn crules th = make_horn crules (tryres(th,crules)) |
173 |
174 handle THM _ => th; |
174 (**** Generation of contrapositives ****) |
175 |
175 |
176 (*Generate Horn clauses for all contrapositives of a clause*) |
176 (*Associate disjuctions to right -- make leftmost disjunct a LITERAL*) |
177 fun add_contras crules (th,hcs) = |
177 fun assoc_right th = assoc_right (th RS disj_assoc) |
178 let fun rots (0,th) = hcs |
178 handle THM _ => th; |
179 | rots (k,th) = zero_var_indexes (make_horn crules th) :: |
179 |
180 rots(k-1, assoc_right (th RS disj_comm)) |
180 (*Must check for negative literal first!*) |
181 in case nliterals(prop_of th) of |
181 val clause_rules = [disj_assoc, make_neg_rule, make_pos_rule]; |
182 1 => th::hcs |
182 |
183 | n => rots(n, assoc_right th) |
183 (*For ordinary resolution. *) |
184 end; |
184 val resolution_clause_rules = [disj_assoc, make_neg_rule', make_pos_rule']; |
185 |
185 |
186 (*Use "theorem naming" to label the clauses*) |
186 (*Create a goal or support clause, conclusing False*) |
187 fun name_thms label = |
187 fun make_goal th = (*Must check for negative literal first!*) |
188 let fun name1 (th, (k,ths)) = |
188 make_goal (tryres(th, clause_rules)) |
189 (k-1, Thm.name_thm (label ^ string_of_int k, th) :: ths) |
189 handle THM _ => tryres(th, [make_neg_goal, make_pos_goal]); |
190 |
190 |
191 in fn ths => #2 (foldr name1 (length ths, []) ths) end; |
191 (*Sort clauses by number of literals*) |
192 |
192 fun fewerlits(th1,th2) = nliterals(prop_of th1) < nliterals(prop_of th2); |
193 (*Find an all-negative support clause*) |
193 |
194 fun is_negative th = forall (not o #1) (literals (prop_of th)); |
194 (*TAUTOLOGY CHECK SHOULD NOT BE NECESSARY!*) |
195 |
195 fun sort_clauses ths = sort (make_ord fewerlits) (List.filter (not o is_taut) ths); |
196 val neg_clauses = List.filter is_negative; |
196 |
197 |
197 (*Convert all suitable free variables to schematic variables*) |
198 |
198 fun generalize th = forall_elim_vars 0 (forall_intr_frees th); |
199 (***** MESON PROOF PROCEDURE *****) |
199 |
200 |
200 (*Create a meta-level Horn clause*) |
201 fun rhyps (Const("==>",_) $ (Const("Trueprop",_) $ A) $ phi, |
201 fun make_horn crules th = make_horn crules (tryres(th,crules)) |
202 As) = rhyps(phi, A::As) |
202 handle THM _ => th; |
203 | rhyps (_, As) = As; |
203 |
204 |
204 (*Generate Horn clauses for all contrapositives of a clause*) |
205 (** Detecting repeated assumptions in a subgoal **) |
205 fun add_contras crules (th,hcs) = |
206 |
206 let fun rots (0,th) = hcs |
207 (*The stringtree detects repeated assumptions.*) |
207 | rots (k,th) = zero_var_indexes (make_horn crules th) :: |
208 fun ins_term (net,t) = Net.insert_term((t,t), net, op aconv); |
208 rots(k-1, assoc_right (th RS disj_comm)) |
209 |
209 in case nliterals(prop_of th) of |
210 (*detects repetitions in a list of terms*) |
210 1 => th::hcs |
211 fun has_reps [] = false |
211 | n => rots(n, assoc_right th) |
212 | has_reps [_] = false |
212 end; |
213 | has_reps [t,u] = (t aconv u) |
213 |
214 | has_reps ts = (Library.foldl ins_term (Net.empty, ts); false) |
214 (*Use "theorem naming" to label the clauses*) |
215 handle INSERT => true; |
215 fun name_thms label = |
216 |
216 let fun name1 (th, (k,ths)) = |
217 (*Like TRYALL eq_assume_tac, but avoids expensive THEN calls*) |
217 (k-1, Thm.name_thm (label ^ string_of_int k, th) :: ths) |
218 fun TRYALL_eq_assume_tac 0 st = Seq.single st |
218 |
219 | TRYALL_eq_assume_tac i st = |
219 in fn ths => #2 (foldr name1 (length ths, []) ths) end; |
220 TRYALL_eq_assume_tac (i-1) (eq_assumption i st) |
220 |
221 handle THM _ => TRYALL_eq_assume_tac (i-1) st; |
221 (*Find an all-negative support clause*) |
222 |
222 fun is_negative th = forall (not o #1) (literals (prop_of th)); |
223 (*Loop checking: FAIL if trying to prove the same thing twice |
223 |
224 -- if *ANY* subgoal has repeated literals*) |
224 val neg_clauses = List.filter is_negative; |
225 fun check_tac st = |
225 |
226 if exists (fn prem => has_reps (rhyps(prem,[]))) (prems_of st) |
226 |
227 then Seq.empty else Seq.single st; |
227 (***** MESON PROOF PROCEDURE *****) |
228 |
228 |
229 |
229 fun rhyps (Const("==>",_) $ (Const("Trueprop",_) $ A) $ phi, |
230 (* net_resolve_tac actually made it slower... *) |
230 As) = rhyps(phi, A::As) |
231 fun prolog_step_tac horns i = |
231 | rhyps (_, As) = As; |
232 (assume_tac i APPEND resolve_tac horns i) THEN check_tac THEN |
232 |
233 TRYALL eq_assume_tac; |
233 (** Detecting repeated assumptions in a subgoal **) |
234 |
234 |
235 |
235 (*The stringtree detects repeated assumptions.*) |
236 in |
236 fun ins_term (net,t) = Net.insert_term((t,t), net, op aconv); |
|
237 |
|
238 (*detects repetitions in a list of terms*) |
|
239 fun has_reps [] = false |
|
240 | has_reps [_] = false |
|
241 | has_reps [t,u] = (t aconv u) |
|
242 | has_reps ts = (Library.foldl ins_term (Net.empty, ts); false) |
|
243 handle INSERT => true; |
|
244 |
|
245 (*Like TRYALL eq_assume_tac, but avoids expensive THEN calls*) |
|
246 fun TRYALL_eq_assume_tac 0 st = Seq.single st |
|
247 | TRYALL_eq_assume_tac i st = |
|
248 TRYALL_eq_assume_tac (i-1) (eq_assumption i st) |
|
249 handle THM _ => TRYALL_eq_assume_tac (i-1) st; |
|
250 |
|
251 (*Loop checking: FAIL if trying to prove the same thing twice |
|
252 -- if *ANY* subgoal has repeated literals*) |
|
253 fun check_tac st = |
|
254 if exists (fn prem => has_reps (rhyps(prem,[]))) (prems_of st) |
|
255 then Seq.empty else Seq.single st; |
|
256 |
|
257 |
|
258 (* net_resolve_tac actually made it slower... *) |
|
259 fun prolog_step_tac horns i = |
|
260 (assume_tac i APPEND resolve_tac horns i) THEN check_tac THEN |
|
261 TRYALL eq_assume_tac; |
|
262 |
|
263 |
|
264 |
237 |
265 |
238 |
266 |
239 (*Sums the sizes of the subgoals, ignoring hypotheses (ancestors)*) |
267 (*Sums the sizes of the subgoals, ignoring hypotheses (ancestors)*) |
240 local fun addconcl(prem,sz) = size_of_term(Logic.strip_assums_concl prem) + sz |
268 fun addconcl(prem,sz) = size_of_term(Logic.strip_assums_concl prem) + sz |
241 in |
269 |
242 fun size_of_subgoals st = foldr addconcl 0 (prems_of st) |
270 fun size_of_subgoals st = foldr addconcl 0 (prems_of st); |
243 end; |
271 |
244 |
272 |
245 (*Negation Normal Form*) |
273 (*Negation Normal Form*) |
246 val nnf_rls = [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD, |
274 val nnf_rls = [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD, |
247 not_impD, not_iffD, not_allD, not_exD, not_notD]; |
275 not_impD, not_iffD, not_allD, not_exD, not_notD]; |
248 fun make_nnf th = make_nnf (tryres(th, nnf_rls)) |
276 fun make_nnf th = make_nnf (tryres(th, nnf_rls)) |