# HG changeset patch
# User paulson
# Date 1088414113 -7200
# Node ID 5abd18710a1fa5ea13b9e5995bf7a757167ff4a0
# Parent  0628f38bcbcf0ba9fa0de9cc52fc107fde944010
new method for explicit classical resolution

diff -r 0628f38bcbcf -r 5abd18710a1f src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Fri Jun 25 15:03:05 2004 +0200
+++ b/src/HOL/Tools/meson.ML	Mon Jun 28 11:15:13 2004 +0200
@@ -285,7 +285,7 @@
 fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls));
 
 
-fun skolemize_tac prems =
+fun skolemize_prems_tac prems =
     cut_facts_tac (map (skolemize o make_nnf) prems)  THEN'
     REPEAT o (etac exE);
 
@@ -293,7 +293,7 @@
 fun MESON cltac = SELECT_GOAL
  (EVERY1 [rtac ccontr,
           METAHYPS (fn negs =>
-                    EVERY1 [skolemize_tac negs,
+                    EVERY1 [skolemize_prems_tac negs,
                             METAHYPS (cltac o make_clauses)])]);
 
 (** Best-first search versions **)
@@ -347,8 +347,8 @@
 
 (**** Code to support ordinary resolution, rather than Model Elimination ****)
 
-(*Convert a list of clauses to meta-level clauses, with no contrapositives,
-  for ordinary resolution.*)
+(*Convert a list of clauses (disjunctions) 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'
@@ -398,6 +398,19 @@
 	  REPEAT_DETERM_N (length ts) o (etac thin_rl)]
      end);
 
+(*Top-level conversion to clauses (disjunctions). Each clause has  
+  leading !!-bound universal variables, to express generality.*)
+val make_clauses_tac = 
+  SUBGOAL
+    (fn (prop,_) =>
+     let val ts = Logic.strip_assums_hyp prop
+     in EVERY1 
+	 [METAHYPS
+	    (fn hyps => 
+              (cut_rules_tac (map forall_intr_vars (make_clauses hyps)) 1)),
+	  REPEAT_DETERM_N (length ts) o (etac thin_rl)]
+     end);
+
 
 
 (** proof method setup **)
@@ -412,6 +425,10 @@
   Method.SIMPLE_METHOD' HEADGOAL
     (CHANGED_PROP o skolemize_tac);
 
+val make_clauses_meth =
+  Method.SIMPLE_METHOD' HEADGOAL
+    (CHANGED_PROP o make_clauses_tac);
+
 in
 
 val meson_setup =
@@ -419,7 +436,9 @@
   [("meson", Method.ctxt_args meson_meth, 
     "The MESON resolution proof procedure"),
    ("skolemize", Method.no_args skolemize_meth, 
-    "Skolemization into existential quantifiers")]];
+    "Skolemization into existential quantifiers"),
+   ("make_clauses", Method.no_args make_clauses_meth, 
+    "Conversion to !!-quantified disjunctions")]];
 
 end;
 
diff -r 0628f38bcbcf -r 5abd18710a1f src/HOL/ex/Classical.thy
--- a/src/HOL/ex/Classical.thy	Fri Jun 25 15:03:05 2004 +0200
+++ b/src/HOL/ex/Classical.thy	Mon Jun 28 11:15:13 2004 +0200
@@ -781,4 +781,21 @@
             (~ p a | ~ p(f x) | p(f(f x))))"
 by meson
 
+
+text{*A manual resolution proof of problem 19.*}
+lemma "\<exists>x. \<forall>y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))"
+proof (rule ccontr, skolemize, make_clauses)
+  fix f g
+  assume P: "\<And>U. P U" 
+     and Q: "\<And>U. \<not> Q U"
+     and PQ: "\<And>U. \<not> P (f U) \<or> Q (g U)"
+  from PQ [of a]
+  show False
+  proof
+    assume "\<not> P (f a)" thus False by (rule notE [OF _ P])
+  next
+    assume "Q (g a)" thus False by (rule notE [OF Q])
+  qed
+qed
+
 end