header {* Very Simple Predicate Logic *} theory VSPred imports VSPL begin typedecl i --{* Terms *} section {* Der Allquantor *} consts All :: "('a => o)=> o" (binder "ALL " 10) axioms allI: "!!x. P x ==> (ALL x. P x)" allE: "ALL x. P x ==> P t" section{* Der Existenzquantor *} constdefs Ex :: "('a => o)=> o" (binder "EX " 10) "Ex P == ~ (ALL x. (~ (P x)))" lemma exI: "P t ==> EX x. P x" apply (unfold Ex_def) apply (rule notI) apply (rule notE [where P="P t"]) apply (rule allE [where t="t"]) apply (assumption) apply (assumption) done lemma exE: "[| EX x. P x; P x ==> Q x |] ==> Q x" apply (unfold Ex_def) apply (rule Raa') apply (erule notE [where P="ALL x. ~ P x"]) apply (rule allI [where x="x"]) apply (rule notI) apply (erule notE) apply (drule impI) apply (drule impE) apply (assumption) apply (assumption) done end