--- a/simpdata.ML Thu Jan 27 17:01:10 1994 +0100
+++ b/simpdata.ML Thu Feb 03 09:55:47 1994 +0100
@@ -52,6 +52,7 @@
val simp_thms = map prover
[ "(x=x) = True",
"(~True) = False", "(~False) = True", "(~ ~ P) = P",
+ "(~P) ~= P", "P ~= (~P)", "(P ~= Q) = (P = (~Q))",
"(True=P) = P", "(P=True) = P",
"(True --> P) = P", "(False --> P) = True",
"(P --> True) = True", "(P --> P) = True",
@@ -101,6 +102,17 @@
fun split_tac splits =
mk_case_split_tac (meta_obj_reflection RS iffD2) (map mk_eq splits);
+(* eliminiation of existential quantifiers in assumptions *)
+
+val ex_all_equiv =
+ let val lemma1 = prove_goal HOL.thy
+ "(? x. P(x) ==> PROP Q) ==> (!!x. P(x) ==> PROP Q)"
+ (fn prems => [resolve_tac prems 1, etac exI 1]);
+ val lemma2 = prove_goalw HOL.thy [Ex_def RS eq_reflection]
+ "(!!x. P(x) ==> PROP Q) ==> (? x. P(x) ==> PROP Q)"
+ (fn prems => [REPEAT(resolve_tac prems 1)])
+ in equal_intr lemma1 lemma2 end;
+
(** '&' congruence rule: not included by default! *)
val conj_cong = impI RSN