theory Demo3 imports Main begin

section{* Propositional logic *}

subsection{* Basic rules *}

text{* \<and> *}
thm conjI 

thm conjunct2
thm conjE 

text{* \<or> *}
thm disjI1 
thm disjI2 
thm disjE

text{* \<longrightarrow> *}
thm impI impE


subsection{* Examples *}

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

text{* a simple backward proof: *}
lemma "B \<and> A \<longrightarrow> A \<and> B" 
  apply (rule impI)
  apply (erule conjE)
  apply (rule conjI)
   apply assumption
  apply assumption
  done

lemma "A \<or> B \<longrightarrow> B \<or> A"
  apply (rule impI)
  apply (erule disjE)
   apply (rule disjI2)
   apply assumption
  apply (rule disjI1)
  apply assumption
  done

lemma "\<lbrakk> B \<longrightarrow> C; A \<longrightarrow> B \<rbrakk> \<Longrightarrow> A \<longrightarrow> C"
  apply (rule impI)
  apply (erule (1) impE)
  apply (erule (2) impE)
  done

thm notI notE 

lemma "\<not>A \<or> \<not>B \<Longrightarrow> \<not>(A \<and> B)"
  apply (rule notI)
  apply (erule conjE)
  apply (erule disjE) 
   apply (erule (1) notE)+
  done


text {* Case distinctions *}

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

thm FalseE

lemma "(\<not>P \<longrightarrow> False) \<longrightarrow> P"
  apply (rule impI)
  apply (rule classical)
  apply (erule impE)
   apply assumption
  apply (erule FalseE)
  done
  


text{* Explicit backtracking: *}

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


text{* Implict backtracking: chaining with , *}

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


text {* more rules *}
text{* \<and> *}
thm conjunct1 conjunct2

text{* \<or> *}
thm disjCI  

lemma our_own_disjCI: "(\<not>Q \<longrightarrow> P) \<Longrightarrow> P \<or> Q"
  apply (case_tac Q)
   apply (rule disjI2)
   apply assumption
  apply (erule impE)
   apply assumption
  apply (rule disjI1)
  apply assumption
  done

text{* \<longrightarrow> *}
thm mp

text{* = (iff) *}
thm iffI iffE iffD1 iffD2


text{* Equality *}
thm refl sym trans

text{* \<not> *}
thm notI notE

text{* Contradictions *}
thm FalseE ccontr classical excluded_middle

-- {* more rules *}

text{* Equality *}
thm refl sym trans

text{* = (iff) *}
thm iffI iffE iffD1 iffD2

text {* defer and prefer *}
lemma "(A \<or> A) = (A \<and> A)"
  prefer 2
  defer
  oops

text{* classical propositional logic: *}
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

end