# HG changeset patch
# User lcp
# Date 748862035 -7200
# Node ID f17d542276b6c4e1bf122c7ae32c45c2009b03fe
# Parent  d0e17c42dbb4f32adf216e8364ab133f7e9b736f
Added ex_ex1I: new introduction rule for the EX! quantifier.

diff -r d0e17c42dbb4 -r f17d542276b6 src/FOL/IFOL.ML
--- a/src/FOL/IFOL.ML	Fri Sep 24 10:52:55 1993 +0200
+++ b/src/FOL/IFOL.ML	Fri Sep 24 11:13:55 1993 +0200
@@ -24,6 +24,7 @@
   val eq_cong: thm
   val eq_mp_tac: int -> tactic
   val ex1I: thm
+  val ex_ex1I: thm
   val ex1E: thm
   val ex1_equalsE: thm
   val ex1_cong: thm
@@ -180,6 +181,12 @@
     "[| P(a);  !!x. P(x) ==> x=a |] ==> EX! x. P(x)"
  (fn prems => [ (REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)) ]);
 
+(*Sometimes easier to use: the premises have no shared variables*)
+val ex_ex1I = prove_goal IFOL.thy
+    "[| EX x.P(x);  !!x y. [| P(x); P(y) |] ==> x=y |] ==> EX! x. P(x)"
+ (fn [ex,eq] => [ (rtac (ex RS exE) 1),
+		  (REPEAT (ares_tac [ex1I,eq] 1)) ]);
+
 val ex1E = prove_goalw IFOL.thy [ex1_def]
     "[| EX! x.P(x);  !!x. [| P(x);  ALL y. P(y) --> y=x |] ==> R |] ==> R"
  (fn prems =>
diff -r d0e17c42dbb4 -r f17d542276b6 src/FOL/ifol.ML
--- a/src/FOL/ifol.ML	Fri Sep 24 10:52:55 1993 +0200
+++ b/src/FOL/ifol.ML	Fri Sep 24 11:13:55 1993 +0200
@@ -24,6 +24,7 @@
   val eq_cong: thm
   val eq_mp_tac: int -> tactic
   val ex1I: thm
+  val ex_ex1I: thm
   val ex1E: thm
   val ex1_equalsE: thm
   val ex1_cong: thm
@@ -180,6 +181,12 @@
     "[| P(a);  !!x. P(x) ==> x=a |] ==> EX! x. P(x)"
  (fn prems => [ (REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)) ]);
 
+(*Sometimes easier to use: the premises have no shared variables*)
+val ex_ex1I = prove_goal IFOL.thy
+    "[| EX x.P(x);  !!x y. [| P(x); P(y) |] ==> x=y |] ==> EX! x. P(x)"
+ (fn [ex,eq] => [ (rtac (ex RS exE) 1),
+		  (REPEAT (ares_tac [ex1I,eq] 1)) ]);
+
 val ex1E = prove_goalw IFOL.thy [ex1_def]
     "[| EX! x.P(x);  !!x. [| P(x);  ALL y. P(y) --> y=x |] ==> R |] ==> R"
  (fn prems =>