(*
    ex.thy,v 1.1 2016/09/29 17:37:37 jdf Exp
    Original Author: Tjark Weber
    Updated to Isabelle 2016 by Jacques Fleuriot
*)

section {* Predicate Logic *}

 theory ex imports Main begin 

text {*
We are again talking about proofs in the calculus of Natural Deduction.  In
addition to the rules given in the exercise "Propositional Logic", you may
now also use

exI: ?P ?x \<Longrightarrow> \<exists>x. ?P x
exE:\<lbrakk>\<exists>x. ?P x; \<And>x. ?P x \<Longrightarrow> ?Q\<rbrakk> \<Longrightarrow> ?Q
allI: (\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x
allE: \<lbrakk>\<forall>x. ?P x; ?P ?x \<Longrightarrow> ?R\<rbrakk> \<Longrightarrow> ?R

Give a proof of the following propositions or an argument why the formula is
not valid:
*}
 
  
lemma "(\<exists>x. \<forall>y. P x y) \<longrightarrow> (\<forall>y. \<exists>x. P x y)"
 oops 

lemma "(\<forall>x. P x \<longrightarrow> Q) = ((\<exists>x. P x) \<longrightarrow> Q)"
 oops 

lemma "((\<forall> x. P x) \<and> (\<forall> x. Q x)) = (\<forall> x. (P x \<and> Q x))"
 oops 

lemma "((\<forall> x. P x) \<or> (\<forall> x. Q x)) = (\<forall> x. (P x \<or> Q x))"
 oops 

lemma "((\<exists> x. P x) \<or> (\<exists> x. Q x)) = (\<exists> x. (P x \<or> Q x))"
 oops 

lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>y. \<forall>x. P x y)"
 oops 

lemma "(\<not> (\<forall> x. P x)) = (\<exists> x. \<not> P x)"
 oops 

 end