theory a1 imports Main begin

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

lemma "(A \<or> A) = (A \<and> A)" 
apply (rule iffI)
 apply (rule conjI)
  apply (erule disjE)
   apply assumption
  apply assumption
 apply (erule disjE)
  apply assumption
 apply assumption
apply (erule conjE)
apply (rule disjI1)
apply assumption
done
 

lemma "(A \<longrightarrow> B \<longrightarrow> C) = (A \<and> B \<longrightarrow> C)"
apply (rule iffI)
 apply (rule impI)
 apply (erule conjE)
 apply (erule impE)
  apply assumption
 apply (erule impE)
  apply assumption
 apply assumption
apply (rule impI)
apply (rule impI)
apply (erule impE)
 apply (rule conjI)
  apply assumption
 apply assumption
apply assumption
done


lemma S: "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> (A \<longrightarrow> B) \<longrightarrow> A \<longrightarrow> C"
apply (rule impI)
apply (rule impI)
apply (rule impI)
apply (erule impE)
 apply assumption
apply (erule impE)
 apply assumption
apply (erule impE)
 apply assumption
apply assumption
done


lemma "(A \<longrightarrow> \<not> B) = (B \<longrightarrow> \<not> A)"
apply (rule iffI)
 apply (rule impI)
 apply (rule notI)
 apply (erule impE)
  apply assumption
 apply (erule notE)
 apply assumption
apply (rule impI)
apply (rule notI)
apply (erule impE)
 apply assumption
apply (erule notE)
apply assumption
done


lemma "((A \<and> \<not> B) \<or> (B \<and> \<not> A)) = (A = (\<not> B))" 
apply (rule iffI)
 apply (rule iffI)
  apply (erule disjE)
   apply (erule conjE)
   apply assumption
  apply (erule conjE)
  apply (erule notE)
  apply assumption
 apply (erule disjE)
  apply (erule conjE)
  apply assumption
 apply (erule conjE)
 apply (erule notE)
 apply assumption
apply (erule iffE)
apply (case_tac A)
 apply (rule disjI1)
 apply (rule conjI)
  apply assumption
 apply (erule impE)
  apply assumption
 apply assumption
apply (rule disjI2)
apply (rule conjI) 
 apply (rule classical)
 apply (erule impE, assumption)
 apply (erule notE)
 apply assumption
apply assumption
done

lemma "\<not>(A \<and> B) \<longrightarrow> \<not> A \<or> \<not> B"
apply (rule impI)
apply (rule disjCI)
apply (rule notI)
apply (erule notE)
apply (rule conjI)
 apply assumption
apply (rule classical)
apply (erule notE)
apply assumption
done

end