added Theorem all_not_ex
authorchaieb
Sun Jun 17 13:39:22 2007 +0200 (2007-06-17)
changeset 234039e1edc15ef52
parent 23402 6472c689664f
child 23404 8659acd81f9d
added Theorem all_not_ex
src/HOL/HOL.thy
     1.1 --- a/src/HOL/HOL.thy	Sun Jun 17 08:56:13 2007 +0200
     1.2 +++ b/src/HOL/HOL.thy	Sun Jun 17 13:39:22 2007 +0200
     1.3 @@ -1061,6 +1061,7 @@
     1.4  lemma imp_all: "((! x. P x) --> Q) = (? x. P x --> Q)" by blast
     1.5  lemma not_ex: "(~ (? x. P(x))) = (! x.~P(x))" by iprover
     1.6  lemma imp_ex: "((? x. P x) --> Q) = (! x. P x --> Q)" by iprover
     1.7 +lemma all_not_ex: "(ALL x. P x) = (~ (EX x. ~ P x ))" by blast
     1.8  
     1.9  lemma ex_disj_distrib: "(? x. P(x) | Q(x)) = ((? x. P(x)) | (? x. Q(x)))" by iprover
    1.10  lemma all_conj_distrib: "(!x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))" by iprover