# HG changeset patch
# User paulson
# Date 1084265280 -7200
# Node ID 3eda95792083ebef86e31b18b35b33ebd0bd5972
# Parent  967db86e853cb980c17ed09b4980cb20adb66282
conversion to clauses for ordinary resolution rather than ME

diff -r 967db86e853c -r 3eda95792083 src/HOL/Tools/meson.ML
--- 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.*)
 
diff -r 967db86e853c -r 3eda95792083 src/HOL/meson_lemmas.ML
--- 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 *)