# HG changeset patch
# User paulson
# Date 1084546152 -7200
# Node ID 7ccfc167e451fca1ee96a2f270b0138c1cba2803
# Parent  81001d6cb8c0696bf8182df3b9ea22353dee5439
clauses for ordinary resolution

diff -r 81001d6cb8c0 -r 7ccfc167e451 src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Fri May 14 16:48:37 2004 +0200
+++ b/src/HOL/Tools/meson.ML	Fri May 14 16:49:12 2004 +0200
@@ -268,13 +268,6 @@
     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.*)
 
@@ -348,7 +341,45 @@
 val meson_tac = CLASET' meson_claset_tac;
 
 
-(* proof method setup *)
+(** Code to support ordinary resolution, rather than Model Elimination **)
+
+(*Convert a list of clauses to meta-level clauses, with no contrapositives,
+  for ordinary resolution.*)
+
+(*Rules to convert the head literal into a negated assumption. If the head
+  literal is already negated, then using notEfalse instead of notEfalse'
+  prevents a double negation.*)
+val notEfalse = read_instantiate [("R","False")] notE;
+val notEfalse' = rotate_prems 1 notEfalse;
+
+fun negate_nead th = 
+    th RS notEfalse handle THM _ => th RS notEfalse';
+
+(*Converting one clause*)
+fun make_meta_clause th = negate_nead (make_horn resolution_clause_rules th);
+
+fun make_meta_clauses ths =
+    name_thms "MClause#"
+      (gen_distinct Drule.eq_thm_prop (map make_meta_clause ths));
+
+(*Permute a rule's premises to move the i-th premise to the last position.*)
+fun make_last i th =
+  let val n = nprems_of th 
+  in  if 1 <= i andalso i <= n 
+      then Thm.permute_prems (i-1) 1 th
+      else raise THM("make_last", i, [th])
+  end;
+
+(*Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing
+  double-negations.*)
+val negate_head = rewrite_rule [atomize_not, not_not RS eq_reflection];
+
+(*Maps the clause  [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P*)
+fun select_literal i cl = negate_head (make_last i cl);
+
+
+
+(** proof method setup **)
 
 local