src/FOL/IFOL.ML
changeset 12 f17d542276b6
parent 0 a5a9c433f639
child 779 4ab9176b45b7
     1.1 --- a/src/FOL/IFOL.ML	Fri Sep 24 10:52:55 1993 +0200
     1.2 +++ b/src/FOL/IFOL.ML	Fri Sep 24 11:13:55 1993 +0200
     1.3 @@ -24,6 +24,7 @@
     1.4    val eq_cong: thm
     1.5    val eq_mp_tac: int -> tactic
     1.6    val ex1I: thm
     1.7 +  val ex_ex1I: thm
     1.8    val ex1E: thm
     1.9    val ex1_equalsE: thm
    1.10    val ex1_cong: thm
    1.11 @@ -180,6 +181,12 @@
    1.12      "[| P(a);  !!x. P(x) ==> x=a |] ==> EX! x. P(x)"
    1.13   (fn prems => [ (REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)) ]);
    1.14  
    1.15 +(*Sometimes easier to use: the premises have no shared variables*)
    1.16 +val ex_ex1I = prove_goal IFOL.thy
    1.17 +    "[| EX x.P(x);  !!x y. [| P(x); P(y) |] ==> x=y |] ==> EX! x. P(x)"
    1.18 + (fn [ex,eq] => [ (rtac (ex RS exE) 1),
    1.19 +		  (REPEAT (ares_tac [ex1I,eq] 1)) ]);
    1.20 +
    1.21  val ex1E = prove_goalw IFOL.thy [ex1_def]
    1.22      "[| EX! x.P(x);  !!x. [| P(x);  ALL y. P(y) --> y=x |] ==> R |] ==> R"
    1.23   (fn prems =>