--- a/src/HOL/Tools/meson.ML Tue May 11 10:47:15 2004 +0200
+++ b/src/HOL/Tools/meson.ML Tue May 11 10:48:00 2004 +0200
@@ -148,8 +148,8 @@
(*Must check for negative literal first!*)
val clause_rules = [disj_assoc, make_neg_rule, make_pos_rule];
- (*For Plaisted's postive refinement. [currently unused] *)
- val refined_clause_rules = [disj_assoc, make_refined_neg_rule, make_pos_rule];
+ (*For ordinary resolution. *)
+ val resolution_clause_rules = [disj_assoc, make_neg_rule', make_pos_rule'];
(*Create a goal or support clause, conclusing False*)
fun make_goal th = (*Must check for negative literal first!*)
@@ -268,6 +268,13 @@
name_thms "Horn#"
(gen_distinct Drule.eq_thm_prop (foldr (add_contras clause_rules) (ths,[])));
+(*Convert a list of clauses to meta-level clauses, with no contrapositives,
+ for ordinary resolution.*)
+fun make_meta_clauses ths =
+ name_thms "MClause#"
+ (gen_distinct Drule.eq_thm_prop
+ (map (make_horn resolution_clause_rules) ths));
+
(*Could simply use nprems_of, which would count remaining subgoals -- no
discrimination as to their size! With BEST_FIRST, fails for problem 41.*)
--- a/src/HOL/meson_lemmas.ML Tue May 11 10:47:15 2004 +0200
+++ b/src/HOL/meson_lemmas.ML Tue May 11 10:48:00 2004 +0200
@@ -8,7 +8,9 @@
(* Generation of contrapositives *)
-(*Inserts negated disjunct after removing the negation; P is a literal*)
+(*Inserts negated disjunct after removing the negation; P is a literal.
+ Model elimination requires assuming the negation of every attempted subgoal,
+ hence the negated disjuncts.*)
val [major,minor] = Goal "~P|Q ==> ((~P==>P) ==> Q)";
by (rtac (major RS disjE) 1);
by (rtac notE 1);
@@ -29,6 +31,14 @@
by (ALLGOALS assume_tac);
qed "make_pos_rule";
+(** Versions of make_neg_rule and make_pos_rule that don't insert new
+ assumptions, for ordinary resolution. **)
+
+val make_neg_rule' = make_refined_neg_rule;
+
+Goal "[|P|Q; ~P|] ==> Q";
+by (Blast_tac 1);
+qed "make_pos_rule'";
(* Generation of a goal clause -- put away the final literal *)