theory iff_redundant
        
imports HOL
begin

text \<open>Start with the axiomatization, just as in HOL. Several constants, like \<open>The\<close>, are omitted here,
  because they are not needed for demonstrating that axiom "iff" is redundant.\<close>

axiomatization myimplies :: "[bool, bool] \<Rightarrow> bool"  (infixr "\<rightharpoonup>" 25)
  and myeq :: "['a, 'a] \<Rightarrow> bool"  (infixl "\<approx>" 50)


subsubsection \<open>Defined connectives and quantifiers\<close>

definition myTrue :: bool
  where "myTrue \<equiv> ((\<lambda>x::bool. x) \<approx> (\<lambda>x. x))"

definition myAll :: "('a \<Rightarrow> bool) \<Rightarrow> bool" (binder "\<forall>\<forall>" 10)
  where "myAll P \<equiv> (P \<approx> (\<lambda>x. myTrue))"

definition myFalse :: bool
  where "myFalse \<equiv> (\<forall>\<forall>P. P)"

definition mydisj :: "[bool, bool] \<Rightarrow> bool"  (infixr "\<nabla>" 30)
  where myor_def: "P \<nabla> Q \<equiv> \<forall>\<forall>R. (P \<rightharpoonup> R) \<rightharpoonup> (Q \<rightharpoonup> R) \<rightharpoonup> R"

subsubsection \<open>Axioms and basic definitions\<close>

axiomatization where
  myrefl: "t \<approx> (t::'a)" and
  mysubst: "s \<approx> t \<Longrightarrow> P s \<Longrightarrow> P t" and
  myext: "(\<And>x::'a. (f x ::'b) \<approx> g x) \<Longrightarrow> (\<lambda>x. f x) \<approx> (\<lambda>x. g x)"

text \<open>There is no "myiff" here:\<close>
axiomatization where
  myimpI: "(P \<Longrightarrow> Q) \<Longrightarrow> P \<rightharpoonup> Q" and
  mymp: "\<lbrakk>P \<rightharpoonup> Q; P\<rbrakk> \<Longrightarrow> Q" and
  myTrue_or_False: "(P \<approx> myTrue) \<nabla> (P \<approx> myFalse)"

subsection \<open>Fundamental rules\<close>

text \<open>The lemmas in this subsection do not depend on axiom "iff".\<close>

subsubsection \<open>Equality\<close>

lemma mysym: "s \<approx> t \<Longrightarrow> t \<approx> s"
  by (erule mysubst) (rule myrefl)

lemma myssubst: "t \<approx> s \<Longrightarrow> P s \<Longrightarrow> P t"
  by (drule mysym) (erule mysubst)

lemma myfun_cong: "(f :: 'a \<Rightarrow> 'b) \<approx> g \<Longrightarrow> f x \<approx> g x"
apply (erule mysubst)
apply (rule myrefl)
done

subsubsection \<open>Equality of booleans -- iff\<close>

lemma myiffD2: "\<lbrakk>P \<approx> Q; Q\<rbrakk> \<Longrightarrow> P"
  by (erule myssubst)

lemma myrev_iffD2: "\<lbrakk>Q; P \<approx> Q\<rbrakk> \<Longrightarrow> P"
  by (erule myiffD2)

lemma myiffD1: "Q \<approx> P \<Longrightarrow> Q \<Longrightarrow> P"
  by (drule mysym) (rule myiffD2)

lemma myrev_iffD1: "Q \<Longrightarrow> Q \<approx> P \<Longrightarrow> P"
  by (drule mysym) (rule myrev_iffD2)

lemma myiffE:
  assumes major: "P \<approx> Q"
    and minor: "\<lbrakk>P \<rightharpoonup> Q; Q \<rightharpoonup> P\<rbrakk> \<Longrightarrow> R"
  shows R
  by (iprover intro: minor myimpI major [THEN myiffD2] major [THEN myiffD1])

subsubsection \<open>True\<close>

lemma myTrueI: "myTrue"
  unfolding myTrue_def by (rule myrefl)

text \<open>"eqTrueI" has to be postponed after "myiff" is proved.\<close>

lemma myeqTrueE: "P \<approx> myTrue \<Longrightarrow> P"
  by (erule myiffD2) (rule myTrueI)

subsubsection \<open>Universal quantifier\<close>

text \<open>"allI" has to be postponed after "myiff" is proved.\<close>

lemma myspec: "\<forall>\<forall>x::'a. P x \<Longrightarrow> P x"
apply (unfold myAll_def)
apply (rule myeqTrueE)
apply (erule myfun_cong)
done

subsubsection \<open>False\<close>

lemma myFalseE: "myFalse \<Longrightarrow> P"
  apply (unfold myFalse_def)
  apply (erule myspec)
  done

subsubsection \<open>Disjunction\<close>

text \<open>"disjI1" and "disjI2" have to be postponed after "myiff" is proved.\<close>

lemma mydisjE:
  assumes major: "P \<nabla> Q"
      and minorP: "P \<Longrightarrow> R"
      and minorQ: "Q \<Longrightarrow> R"
  shows R
by (iprover intro: minorP minorQ myimpI
                 major [unfolded myor_def, THEN myspec, THEN mymp, THEN mymp])

subsection \<open>iff\<close>

text \<open>This is the new part.\<close>

lemma myiffI:
  assumes 1: "P \<Longrightarrow> Q" and 2: "Q \<Longrightarrow> P"
  shows "P \<approx> Q"
  using myTrue_or_False[of P]
proof (rule mydisjE)
  assume c1: "P \<approx> myTrue"
  hence P by (rule myeqTrueE)
  hence Q by (rule 1)
  from c1 show ?thesis
  proof (rule myssubst)
    from myTrue_or_False[of Q] show "myTrue \<approx> Q"
    proof (rule mydisjE)
      assume "Q \<approx> myTrue"
      thus ?thesis
      proof (rule myssubst)
        show "myTrue \<approx> myTrue" by (rule myrefl)
      qed
    next
      assume "Q \<approx> myFalse"
      with \<open>Q\<close> have myFalse by (rule myrev_iffD1)
      thus ?thesis by (rule myFalseE)
    qed
  qed
next
  assume c2: "P \<approx> myFalse"
  thus ?thesis
  proof (rule myssubst)
    from myTrue_or_False[of Q] show "myFalse \<approx> Q"
    proof (rule mydisjE)
      assume "Q \<approx> myTrue"
      hence Q by (rule myeqTrueE)
      hence P by (rule 2)
      with c2 have myFalse by (rule myiffD1)
      thus ?thesis by (rule myFalseE)
    next
      assume "Q \<approx> myFalse"
      thus ?thesis
      proof (rule myssubst)
        show "myFalse \<approx> myFalse" by (rule myrefl)
      qed
    qed
  qed
qed

text \<open>If needed; probably "myiffI" is sufficient anyway.\<close>

theorem myiff: "(P \<rightharpoonup> Q) \<rightharpoonup> (Q \<rightharpoonup> P) \<rightharpoonup> (P \<approx> Q)"
  by (iprover intro: myimpI myiffI mymp)

end