theory a1 
imports Main 
begin


lemma p_a: "(A\<and>B)\<longrightarrow> (\<not>(C\<and>\<not>A))\<and>(C\<longrightarrow>B)"
apply (rule impI)
apply (erule conjE)
apply (rule conjI)
 apply (rule notI)
 apply (erule conjE)
 apply (erule notE) 
 apply assumption
apply (rule impI)
apply assumption
done


lemma p_b: "(\<not> (a\<longrightarrow>b))=(a \<and> \<not> b)"
apply (rule iffI)
 apply (rule conjI)
  apply (case_tac a)
   apply (assumption)
  apply (erule notE)
  apply (rule impI)
  apply (erule notE)
  apply assumption
 apply (rule notI)
 apply (erule notE)
 apply (rule impI)
 apply assumption
apply (rule notI)
apply (erule conjE)
apply (erule impE)
 apply assumption
apply (erule notE)
apply assumption
done

lemma p_c: " \<lbrakk>((\<not> a) = b)\<rbrakk> \<Longrightarrow> (a= (\<not> b)) "
apply (rule iffI)
 apply (erule iffE)
 apply (rule notI)
 apply (erule_tac P=b in impE)
  apply assumption
 apply (erule notE)
 apply assumption
apply (erule iffE)
apply (case_tac a)
 apply assumption
apply (erule impE)
 apply assumption
apply (erule notE)
apply assumption
done

lemma p_d: "(((f\<longrightarrow>g)\<longrightarrow>(h\<longrightarrow>f))\<longrightarrow>g) = ((f\<longrightarrow>g) \<and> (g\<or>h))"
apply (rule iffI)
 apply (rule conjI)
  apply (rule impI)
  apply (erule impE)
   apply (rule impI)
   apply (rule impI)
   apply assumption
  apply assumption
 apply (case_tac h)
  apply (rule disjI2)
  apply assumption
 apply (rule disjI1)
 apply (erule impE)
  apply (rule impI)
  apply (rule impI)
  apply (erule notE)
  apply assumption
 apply assumption
apply (erule conjE)
apply (rule impI)
apply (erule disjE)
 apply assumption
apply (erule impE)
 apply (case_tac f)
  apply assumption
 apply(erule impE)
  apply (rule impI)
  apply (erule notE)
  apply assumption
 apply (erule impE)
  apply assumption
 apply (erule notE)
 apply assumption
apply assumption
done


lemma p_e: "(a\<longrightarrow>b)=(\<not> (a \<and> \<not> b))"
apply (rule iffI)
 apply (rule notI)
 apply (erule conjE)
 apply (erule impE)
  apply assumption
 apply (erule notE)
 apply assumption
apply (rule impI)
 apply (case_tac b)
 apply assumption
apply (erule notE)
apply (rule conjI)
 apply assumption
apply assumption
done


lemma p_f: "(a\<longrightarrow>b)=(\<not> (a \<and> \<not> b))"
apply (rule p_c) 
apply (rule p_b)
done

end