theory week02A_demo imports Main begin

section\<open>Propositional logic\<close>

subsection\<open>Basic rules\<close>

text\<open>\<and>\<close>
thm conjI 

thm conjunct2
thm conjE 

text\<open>\<or>\<close>
thm disjI1 
thm disjI2 
thm disjE

text\<open>\<longrightarrow>\<close>
thm impI impE


subsection\<open>Examples\<close>

text\<open>a simple backward step:\<close>
lemma "A \<and> B" thm conjI
apply(rule conjI)
oops

text\<open>a simple backward proof:\<close>
lemma "B \<and> A \<longrightarrow> A \<and> B" 
(*TODO*)
sorry


lemma "(A \<or> B) \<longrightarrow> (B \<or> A)"
(*TODO*)
sorry

lemma "\<lbrakk> B \<longrightarrow> C; A \<longrightarrow> B \<rbrakk> \<Longrightarrow> A \<longrightarrow> C"
sorry

thm notI notE 

lemma "\<not>A \<or> \<not>B \<Longrightarrow> \<not>(A \<and> B)"
(*TODO*)
sorry


text \<open>Case distinctions\<close>

lemma "P \<or> \<not>P"
  apply (case_tac "P")
  oops
  

thm FalseE

lemma "(\<not>P \<longrightarrow> False) \<longrightarrow> P"
oops 


text\<open>Explicit backtracking:\<close>

lemma "\<lbrakk> P \<and> Q; A \<and> B \<rbrakk> \<Longrightarrow> A"
apply(erule conjE)
back
apply(assumption)
done
text \<open>UGLY! EVIL! AVOID!\<close>


text\<open>Implicit backtracking: chaining with ,\<close>

lemma "\<lbrakk> P \<and> Q; A \<and> B \<rbrakk> \<Longrightarrow> A"
apply (erule conjE, assumption)
done

text\<open>OR: use rule_tac or erule_tac to instantiate the schematic variables of the rule\<close>

lemma "\<lbrakk> P \<and> Q; A \<and> B \<rbrakk> \<Longrightarrow> A"
apply (erule_tac P=A and Q=B in conjE)
apply assumption
done

text \<open>more rules\<close>
text\<open>\<and>\<close>
thm conjunct1 conjunct2

text\<open>\<or>\<close>
thm disjCI  

lemma our_own_disjCI: "(\<not>Q \<longrightarrow> P) \<Longrightarrow> P \<or> Q"
(*TODO (with case_tac) *)
sorry

text\<open>\<longrightarrow>\<close>
thm mp

text\<open>= (iff)\<close>
thm iffI iffE iffD1 iffD2


text\<open>Equality\<close>
thm refl sym trans

text\<open>\<not>\<close>
thm notI notE

text\<open>Contradictions\<close>
thm FalseE ccontr classical excluded_middle

\<comment> \<open>more rules\<close>

text \<open>defer and prefer\<close>
lemma "(A \<or> A) = (A \<and> A)"
  apply (rule iffI)
  prefer 2 
  defer
  sorry

text\<open>classical propositional logic:\<close>
lemma Pierce: "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"
  apply (rule impI)
  apply (rule classical)
  apply (erule impE)
   apply (rule impI)
   apply (erule notE)
   apply assumption
  apply assumption
  done


text \<open>Exercises\<close>


lemma "A \<and> B \<longrightarrow> A \<longrightarrow> B"
  oops

lemma "A \<longrightarrow> (B \<or> C) \<longrightarrow> (\<not> A \<or> \<not> B) \<longrightarrow> C"
  oops

lemma"((A \<longrightarrow> B) \<and> (B \<longrightarrow> A)) = (A = B)"
  oops 

lemma "(A \<longrightarrow> (B \<and> C)) \<longrightarrow> (A \<longrightarrow> C)"
  oops

end