969

1 
(* Title: HOL/ex/meson


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1992 University of Cambridge


5 


6 
The MESON resolution proof procedure for HOL


7 


8 
When making clauses, avoids using the rewriter  instead uses RS recursively


9 
*)


10 


11 
writeln"File HOL/ex/meson.";


12 


13 
(*Prove theorems using fast_tac*)


14 
fun prove_fun s =


15 
prove_goal HOL.thy s


16 
(fn prems => [ cut_facts_tac prems 1, fast_tac HOL_cs 1 ]);


17 


18 
(**** Negation Normal Form ****)


19 


20 
(*** de Morgan laws ***)


21 


22 
val not_conjD = prove_fun "~(P&Q) ==> ~P  ~Q";


23 
val not_disjD = prove_fun "~(PQ) ==> ~P & ~Q";


24 
val not_notD = prove_fun "~~P ==> P";


25 
val not_allD = prove_fun "~(! x.P(x)) ==> ? x. ~P(x)";


26 
val not_exD = prove_fun "~(? x.P(x)) ==> ! x. ~P(x)";


27 


28 


29 
(*** Removal of > and <> (positive and negative occurrences) ***)


30 


31 
val imp_to_disjD = prove_fun "P>Q ==> ~P  Q";


32 
val not_impD = prove_fun "~(P>Q) ==> P & ~Q";


33 


34 
val iff_to_disjD = prove_fun "P=Q ==> (~P  Q) & (~Q  P)";


35 


36 
(*Much more efficient than (P & ~Q)  (Q & ~P) for computing CNF*)


37 
val not_iffD = prove_fun "~(P=Q) ==> (P  Q) & (~P  ~Q)";


38 


39 


40 
(**** Pulling out the existential quantifiers ****)


41 


42 
(*** Conjunction ***)


43 


44 
val conj_exD1 = prove_fun "(? x.P(x)) & Q ==> ? x. P(x) & Q";


45 
val conj_exD2 = prove_fun "P & (? x.Q(x)) ==> ? x. P & Q(x)";


46 


47 
(*** Disjunction ***)


48 


49 
(*DO NOT USE with forallSkolemization: makes fewer schematic variables!!


50 
With exSkolemization, makes fewer Skolem constants*)


51 
val disj_exD = prove_fun "(? x.P(x))  (? x.Q(x)) ==> ? x. P(x)  Q(x)";


52 


53 
val disj_exD1 = prove_fun "(? x.P(x))  Q ==> ? x. P(x)  Q";


54 
val disj_exD2 = prove_fun "P  (? x.Q(x)) ==> ? x. P  Q(x)";


55 


56 


57 
(**** Skolemization  pulling "?" over "!" ****)


58 


59 
(*"Axiom" of Choice, proved using the description operator*)


60 
val [major] = goal HOL.thy


61 
"! x. ? y. Q x y ==> ? f. ! x. Q x (f x)";


62 
by (cut_facts_tac [major] 1);


63 
by (fast_tac (HOL_cs addEs [selectI]) 1);


64 
qed "choice";


65 


66 


67 
(***** Generating clauses for the Meson Proof Procedure *****)


68 


69 
(*** Disjunctions ***)


70 


71 
val disj_assoc = prove_fun "(PQ)R ==> P(QR)";


72 


73 
val disj_comm = prove_fun "PQ ==> QP";


74 


75 
val disj_FalseD1 = prove_fun "FalseP ==> P";


76 
val disj_FalseD2 = prove_fun "PFalse ==> P";


77 


78 
(*** Generation of contrapositives ***)


79 


80 
(*Inserts negated disjunct after removing the negation; P is a literal*)


81 
val [major,minor] = goal HOL.thy "~PQ ==> ((~P==>P) ==> Q)";


82 
by (rtac (major RS disjE) 1);


83 
by (rtac notE 1);


84 
by (etac minor 2);


85 
by (ALLGOALS assume_tac);


86 
qed "make_neg_rule";


87 


88 
(*For Plaisted's "Postive refinement" of the MESON procedure*)


89 
val [major,minor] = goal HOL.thy "~PQ ==> (P ==> Q)";


90 
by (rtac (major RS disjE) 1);


91 
by (rtac notE 1);


92 
by (rtac minor 2);


93 
by (ALLGOALS assume_tac);


94 
qed "make_refined_neg_rule";


95 


96 
(*P should be a literal*)


97 
val [major,minor] = goal HOL.thy "PQ ==> ((P==>~P) ==> Q)";


98 
by (rtac (major RS disjE) 1);


99 
by (rtac notE 1);


100 
by (etac minor 1);


101 
by (ALLGOALS assume_tac);


102 
qed "make_pos_rule";


103 


104 
(*** Generation of a goal clause  put away the final literal ***)


105 


106 
val [major,minor] = goal HOL.thy "~P ==> ((~P==>P) ==> False)";


107 
by (rtac notE 1);


108 
by (rtac minor 2);


109 
by (ALLGOALS (rtac major));


110 
qed "make_neg_goal";


111 


112 
val [major,minor] = goal HOL.thy "P ==> ((P==>~P) ==> False)";


113 
by (rtac notE 1);


114 
by (rtac minor 1);


115 
by (ALLGOALS (rtac major));


116 
qed "make_pos_goal";


117 


118 


119 
(**** Lemmas for forward proof (like congruence rules) ****)


120 


121 
(*NOTE: could handle conjunctions (faster?) by


122 
nf(th RS conjunct2) RS (nf(th RS conjunct1) RS conjI) *)


123 
val major::prems = goal HOL.thy


124 
"[ P'&Q'; P' ==> P; Q' ==> Q ] ==> P&Q";


125 
by (rtac (major RS conjE) 1);


126 
by (rtac conjI 1);


127 
by (ALLGOALS (eresolve_tac prems));


128 
qed "conj_forward";


129 


130 
val major::prems = goal HOL.thy


131 
"[ P'Q'; P' ==> P; Q' ==> Q ] ==> PQ";


132 
by (rtac (major RS disjE) 1);


133 
by (ALLGOALS (dresolve_tac prems));


134 
by (ALLGOALS (eresolve_tac [disjI1,disjI2]));


135 
qed "disj_forward";


136 


137 
val major::prems = goal HOL.thy


138 
"[ ! x. P'(x); !!x. P'(x) ==> P(x) ] ==> ! x. P(x)";


139 
by (rtac allI 1);


140 
by (resolve_tac prems 1);


141 
by (rtac (major RS spec) 1);


142 
qed "all_forward";


143 


144 
val major::prems = goal HOL.thy


145 
"[ ? x. P'(x); !!x. P'(x) ==> P(x) ] ==> ? x. P(x)";


146 
by (rtac (major RS exE) 1);


147 
by (rtac exI 1);


148 
by (eresolve_tac prems 1);


149 
qed "ex_forward";


150 


151 


152 
(**** Operators for forward proof ****)


153 


154 
(*raises exception if no rules apply  unlike RL*)


155 
fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls))


156 
 tryres (th, []) = raise THM("tryres", 0, [th]);


157 


158 
val prop_of = #prop o rep_thm;


159 


160 
(*Permits forward proof from rules that discharge assumptions*)


161 
fun forward_res nf state =


162 
case Sequence.pull


163 
(tapply(ALLGOALS (METAHYPS (fn [prem] => rtac (nf prem) 1)),


164 
state))


165 
of Some(th,_) => th


166 
 None => raise THM("forward_res", 0, [state]);


167 


168 


169 
(*Negation Normal Form*)


170 
val nnf_rls = [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD,


171 
not_impD, not_iffD, not_allD, not_exD, not_notD];


172 
fun make_nnf th = make_nnf (tryres(th, nnf_rls))


173 
handle THM _ =>


174 
forward_res make_nnf


175 
(tryres(th, [conj_forward,disj_forward,all_forward,ex_forward]))


176 
handle THM _ => th;


177 


178 


179 
(*Are any of the constants in "bs" present in the term?*)


180 
fun has_consts bs =


181 
let fun has (Const(a,_)) = a mem bs


182 
 has (f$u) = has f orelse has u


183 
 has (Abs(_,_,t)) = has t


184 
 has _ = false


185 
in has end;


186 


187 
(*Pull existential quantifiers (Skolemization)*)


188 
fun skolemize th =


189 
if not (has_consts ["Ex"] (prop_of th)) then th


190 
else skolemize (tryres(th, [choice, conj_exD1, conj_exD2,


191 
disj_exD, disj_exD1, disj_exD2]))


192 
handle THM _ =>


193 
skolemize (forward_res skolemize


194 
(tryres (th, [conj_forward, disj_forward, all_forward])))


195 
handle THM _ => forward_res skolemize (th RS ex_forward);


196 


197 


198 
(**** Clause handling ****)


199 


200 
fun literals (Const("Trueprop",_) $ P) = literals P


201 
 literals (Const("op ",_) $ P $ Q) = literals P @ literals Q


202 
 literals (Const("not",_) $ P) = [(false,P)]


203 
 literals P = [(true,P)];


204 


205 
(*number of literals in a term*)


206 
val nliterals = length o literals;


207 


208 
(*to delete tautologous clauses*)


209 
fun taut_lits [] = false


210 
 taut_lits ((flg,t)::ts) = (not flg,t) mem ts orelse taut_lits ts;


211 


212 
val is_taut = taut_lits o literals o prop_of;


213 


214 


215 
(*Generation of unique names  maxidx cannot be relied upon to increase!


216 
Cannot rely on "variant", since variables might coincide when literals


217 
are joined to make a clause...


218 
19 chooses "U" as the first variable name*)


219 
val name_ref = ref 19;


220 


221 
(*Replaces universally quantified variables by FREE variables  because


222 
assumptions may not contain scheme variables. Later, call "generalize". *)


223 
fun freeze_spec th =


224 
let val sth = th RS spec


225 
val newname = (name_ref := !name_ref + 1;


226 
radixstring(26, "A", !name_ref))


227 
in read_instantiate [("x", newname)] sth end;


228 


229 
fun resop nf [prem] = resolve_tac (nf prem) 1;


230 


231 
(*Conjunctive normal form, detecting tautologies early.


232 
Strips universal quantifiers and breaks up conjunctions. *)


233 
fun cnf_aux seen (th,ths) =


234 
if taut_lits (literals(prop_of th) @ seen) then ths


235 
else if not (has_consts ["All","op &"] (prop_of th)) then th::ths


236 
else (*conjunction?*)


237 
cnf_aux seen (th RS conjunct1,


238 
cnf_aux seen (th RS conjunct2, ths))


239 
handle THM _ => (*universal quant?*)


240 
cnf_aux seen (freeze_spec th, ths)


241 
handle THM _ => (*disjunction?*)


242 
let val tac =


243 
(METAHYPS (resop (cnf_nil seen)) 1) THEN


244 
(STATE (fn st' =>


245 
METAHYPS (resop (cnf_nil (literals (concl_of st') @ seen))) 1))


246 
in Sequence.list_of_s (tapply(tac, th RS disj_forward)) @ ths


247 
end


248 
and cnf_nil seen th = cnf_aux seen (th,[]);


249 


250 
(*Toplevel call to cnf  it's safe to reset name_ref*)


251 
fun cnf (th,ths) =


252 
(name_ref := 19; cnf (th RS conjunct1, cnf (th RS conjunct2, ths))


253 
handle THM _ => (*not a conjunction*) cnf_aux [] (th, ths));


254 


255 
(**** Removal of duplicate literals ****)


256 


257 
(*Version for removal of duplicate literals*)


258 
val major::prems = goal HOL.thy


259 
"[ P'Q'; P' ==> P; [ Q'; P==>False ] ==> Q ] ==> PQ";


260 
by (rtac (major RS disjE) 1);


261 
by (rtac disjI1 1);


262 
by (rtac (disjCI RS disj_comm) 2);


263 
by (ALLGOALS (eresolve_tac prems));


264 
by (etac notE 1);


265 
by (assume_tac 1);


266 
qed "disj_forward2";


267 


268 
(*Forward proof, passing extra assumptions as theorems to the tactic*)


269 
fun forward_res2 nf hyps state =


270 
case Sequence.pull


271 
(tapply(REPEAT


272 
(METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1),


273 
state))


274 
of Some(th,_) => th


275 
 None => raise THM("forward_res2", 0, [state]);


276 


277 
(*Remove duplicates in PQ by assuming ~P in Q


278 
rls (initially []) accumulates assumptions of the form P==>False*)


279 
fun nodups_aux rls th = nodups_aux rls (th RS disj_assoc)


280 
handle THM _ => tryres(th,rls)


281 
handle THM _ => tryres(forward_res2 nodups_aux rls (th RS disj_forward2),


282 
[disj_FalseD1, disj_FalseD2, asm_rl])


283 
handle THM _ => th;


284 


285 
(*Remove duplicate literals, if there are any*)


286 
fun nodups th =


287 
if null(findrep(literals(prop_of th))) then th


288 
else nodups_aux [] th;


289 


290 


291 
(**** Generation of contrapositives ****)


292 


293 
(*Associate disjuctions to right  make leftmost disjunct a LITERAL*)


294 
fun assoc_right th = assoc_right (th RS disj_assoc)


295 
handle THM _ => th;


296 


297 
(*Must check for negative literal first!*)


298 
val clause_rules = [disj_assoc, make_neg_rule, make_pos_rule];


299 
val refined_clause_rules = [disj_assoc, make_refined_neg_rule, make_pos_rule];


300 


301 
(*Create a goal or support clause, conclusing False*)


302 
fun make_goal th = (*Must check for negative literal first!*)


303 
make_goal (tryres(th, clause_rules))


304 
handle THM _ => tryres(th, [make_neg_goal, make_pos_goal]);


305 


306 
(*Sort clauses by number of literals*)


307 
fun fewerlits(th1,th2) = nliterals(prop_of th1) < nliterals(prop_of th2);


308 


309 
(*TAUTOLOGY CHECK SHOULD NOT BE NECESSARY!*)


310 
fun sort_clauses ths = sort fewerlits (filter (not o is_taut) ths);


311 


312 
(*Convert all suitable free variables to schematic variables*)


313 
fun generalize th = forall_elim_vars 0 (forall_intr_frees th);


314 


315 
(*make clauses from a list of theorems*)


316 
fun make_clauses ths =


317 
sort_clauses (map (generalize o nodups) (foldr cnf (ths,[])));


318 


319 
(*Create a Horn clause*)


320 
fun make_horn crules th = make_horn crules (tryres(th,crules))


321 
handle THM _ => th;


322 


323 
(*Generate Horn clauses for all contrapositives of a clause*)


324 
fun add_contras crules (th,hcs) =


325 
let fun rots (0,th) = hcs


326 
 rots (k,th) = zero_var_indexes (make_horn crules th) ::


327 
rots(k1, assoc_right (th RS disj_comm))


328 
in case nliterals(prop_of th) of


329 
1 => th::hcs


330 
 n => rots(n, assoc_right th)


331 
end;


332 


333 
(*Convert a list of clauses to (contrapositive) Horn clauses*)


334 
fun make_horns ths = foldr (add_contras clause_rules) (ths,[]);


335 


336 
(*Find an allnegative support clause*)


337 
fun is_negative th = forall (not o #1) (literals (prop_of th));


338 


339 
val neg_clauses = filter is_negative;


340 


341 


342 
(***** MESON PROOF PROCEDURE *****)


343 


344 
fun rhyps (Const("==>",_) $ (Const("Trueprop",_) $ A) $ phi,


345 
As) = rhyps(phi, A::As)


346 
 rhyps (_, As) = As;


347 


348 
(** Detecting repeated assumptions in a subgoal **)


349 


350 
(*The stringtree detects repeated assumptions.*)


351 
fun ins_term (net,t) = Net.insert_term((t,t), net, op aconv);


352 


353 
(*detects repetitions in a list of terms*)


354 
fun has_reps [] = false


355 
 has_reps [_] = false


356 
 has_reps [t,u] = (t aconv u)


357 
 has_reps ts = (foldl ins_term (Net.empty, ts); false)


358 
handle INSERT => true;


359 


360 
(*Loop checking: FAIL if trying to prove the same thing twice


361 
 repeated literals*)


362 
val check_tac = SUBGOAL (fn (prem,_) =>


363 
if has_reps (rhyps(prem,[])) then no_tac else all_tac);


364 


365 
(* net_resolve_tac actually made it slower... *)


366 
fun prolog_step_tac horns i =


367 
(assume_tac i APPEND resolve_tac horns i) THEN


368 
(ALLGOALS check_tac) THEN


369 
(TRYALL eq_assume_tac);


370 


371 


372 
(*Sums the sizes of the subgoals, ignoring hypotheses (ancestors)*)


373 
local fun addconcl(prem,sz) = size_of_term (Logic.strip_assums_concl prem) + sz


374 
in


375 
fun size_of_subgoals st = foldr addconcl (prems_of st, 0)


376 
end;


377 


378 
(*Could simply use nprems_of, which would count remaining subgoals  no


379 
discrimination as to their size! With BEST_FIRST, fails for problem 41.*)


380 


381 
fun best_prolog_tac sizef horns =


382 
BEST_FIRST (has_fewer_prems 1, sizef) (prolog_step_tac horns 1);


383 


384 
fun depth_prolog_tac horns =


385 
DEPTH_FIRST (has_fewer_prems 1) (prolog_step_tac horns 1);


386 


387 
(*Return all negative clauses, as possible goal clauses*)


388 
fun gocls cls = map make_goal (neg_clauses cls);


389 


390 


391 
fun skolemize_tac prems =


392 
cut_facts_tac (map (skolemize o make_nnf) prems) THEN'


393 
REPEAT o (etac exE);


394 


395 
fun MESON sko_tac = SELECT_GOAL


396 
(EVERY1 [rtac ccontr,


397 
METAHYPS (fn negs =>


398 
EVERY1 [skolemize_tac negs,


399 
METAHYPS (sko_tac o make_clauses)])]);


400 


401 
fun best_meson_tac sizef =


402 
MESON (fn cls =>


403 
resolve_tac (gocls cls) 1


404 
THEN_BEST_FIRST


405 
(has_fewer_prems 1, sizef,


406 
prolog_step_tac (make_horns cls) 1));


407 


408 
(*First, breaks the goal into independent units*)


409 
val safe_meson_tac =


410 
SELECT_GOAL (TRY (safe_tac HOL_cs) THEN


411 
TRYALL (best_meson_tac size_of_subgoals));


412 


413 
val depth_meson_tac =


414 
MESON (fn cls => EVERY [resolve_tac (gocls cls) 1,


415 
depth_prolog_tac (make_horns cls)]);


416 


417 
writeln"Reached end of file.";
