# HG changeset patch
# User nipkow
# Date 1508656210 -7200
# Node ID ced164fe3bbd12b27d53e7230a27faa7f5196bba
# Parent  d67d28254ff2e7ecf9f8385a455172142160da0c
derived axiom iffI as a lemma (thanks to Alexander Maletzky)

diff -r d67d28254ff2 -r ced164fe3bbd CONTRIBUTORS
--- a/CONTRIBUTORS	Sat Oct 21 18:19:11 2017 +0200
+++ b/CONTRIBUTORS	Sun Oct 22 09:10:10 2017 +0200
@@ -6,6 +6,8 @@
 Contributions to this Isabelle version
 --------------------------------------
 
+* October 2017: Alexander Maletzky
+  Derivation of axiom "iff" in HOL.thy from the other axioms.
 
 Contributions to Isabelle2017
 -----------------------------
diff -r d67d28254ff2 -r ced164fe3bbd src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sat Oct 21 18:19:11 2017 +0200
+++ b/src/HOL/HOL.thy	Sun Oct 22 09:10:10 2017 +0200
@@ -55,6 +55,15 @@
 
 subsection \<open>Primitive logic\<close>
 
+text \<open>
+The definition of the logic is based on Mike Gordon's technical report \cite{Gordon-TR68} that
+describes the first implementation of HOL. However, there are a number of differences.
+In particular, we start with the definite description operator and introduce Hilbert's \<open>\<epsilon>\<close> operator
+only much later. Moreover, axiom \<open>(P \<longrightarrow> Q) \<longrightarrow> (Q \<longrightarrow> P) \<longrightarrow> (P = Q)\<close> is derived from the other
+axioms. The fact that this axiom is derivable was first noticed by Bruno Barras (for Mike Gordon's
+line of HOL systems) and later independently by Alexander Maletzky (for Isabelle/HOL).
+\<close>
+
 subsubsection \<open>Core syntax\<close>
 
 setup \<open>Axclass.class_axiomatization (@{binding type}, [])\<close>
@@ -195,7 +204,6 @@
   impI: "(P \<Longrightarrow> Q) \<Longrightarrow> P \<longrightarrow> Q" and
   mp: "\<lbrakk>P \<longrightarrow> Q; P\<rbrakk> \<Longrightarrow> Q" and
 
-  iff: "(P \<longrightarrow> Q) \<longrightarrow> (Q \<longrightarrow> P) \<longrightarrow> (P = Q)" and
   True_or_False: "(P = True) \<or> (P = False)"
 
 definition If :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" ("(if (_)/ then (_)/ else (_))" [0, 0, 10] 10)
@@ -283,9 +291,6 @@
 
 subsubsection \<open>Equality of booleans -- iff\<close>
 
-lemma iffI: assumes "P \<Longrightarrow> Q" and "Q \<Longrightarrow> P" shows "P = Q"
-  by (iprover intro: iff [THEN mp, THEN mp] impI assms)
-
 lemma iffD2: "\<lbrakk>P = Q; Q\<rbrakk> \<Longrightarrow> P"
   by (erule ssubst)
 
@@ -305,24 +310,16 @@
   by (iprover intro: minor impI major [THEN iffD2] major [THEN iffD1])
 
 
-subsubsection \<open>True\<close>
+subsubsection \<open>True (1)\<close>
 
 lemma TrueI: True
   unfolding True_def by (rule refl)
 
-lemma eqTrueI: "P \<Longrightarrow> P = True"
-  by (iprover intro: iffI TrueI)
-
 lemma eqTrueE: "P = True \<Longrightarrow> P"
   by (erule iffD2) (rule TrueI)
 
 
-subsubsection \<open>Universal quantifier\<close>
-
-lemma allI:
-  assumes "\<And>x::'a. P x"
-  shows "\<forall>x. P x"
-  unfolding All_def by (iprover intro: ext eqTrueI assms)
+subsubsection \<open>Universal quantifier (1)\<close>
 
 lemma spec: "\<forall>x::'a. P x \<Longrightarrow> P x"
   apply (unfold All_def)
@@ -420,6 +417,70 @@
   by (erule subst, erule ssubst, assumption)
 
 
+subsubsection \<open>Disjunction (1)\<close>
+
+lemma disjE:
+  assumes major: "P \<or> Q"
+    and minorP: "P \<Longrightarrow> R"
+    and minorQ: "Q \<Longrightarrow> R"
+  shows R
+  by (iprover intro: minorP minorQ impI
+      major [unfolded or_def, THEN spec, THEN mp, THEN mp])
+
+
+subsubsection \<open>Derivation of \<open>iffI\<close>\<close>
+
+text \<open>In an intuitionistic version of HOL \<open>iffI\<close> needs to be an axiom.\<close>
+
+lemma iffI:
+  assumes "P \<Longrightarrow> Q" and "Q \<Longrightarrow> P"
+  shows "P = Q"
+proof (rule disjE[OF True_or_False[of P]])
+  assume 1: "P = True"
+  note Q = assms(1)[OF eqTrueE[OF this]]
+  from 1 show ?thesis
+  proof (rule ssubst)
+    from True_or_False[of Q] show "True = Q"
+    proof (rule disjE)
+      assume "Q = True"
+      thus ?thesis by(rule sym)
+    next
+      assume "Q = False"
+      with Q have False by (rule rev_iffD1)
+      thus ?thesis by (rule FalseE)
+    qed
+  qed
+next
+  assume 2: "P = False"
+  thus ?thesis
+  proof (rule ssubst)
+    from True_or_False[of Q] show "False = Q"
+    proof (rule disjE)
+      assume "Q = True"
+      from 2 assms(2)[OF eqTrueE[OF this]] have False by (rule iffD1)
+      thus ?thesis by (rule FalseE)
+    next
+      assume "Q = False"
+      thus ?thesis by(rule sym)
+    qed
+  qed
+qed
+
+
+subsubsection \<open>True (2)\<close>
+
+lemma eqTrueI: "P \<Longrightarrow> P = True"
+  by (iprover intro: iffI TrueI)
+
+
+subsubsection \<open>Universal quantifier (2)\<close>
+
+lemma allI:
+  assumes "\<And>x::'a. P x"
+  shows "\<forall>x. P x"
+  unfolding All_def by (iprover intro: ext eqTrueI assms)
+
+
 subsubsection \<open>Existential quantifier\<close>
 
 lemma exI: "P x \<Longrightarrow> \<exists>x::'a. P x"
@@ -458,7 +519,7 @@
   by (iprover intro: conjI assms)
 
 
-subsubsection \<open>Disjunction\<close>
+subsubsection \<open>Disjunction (2)\<close>
 
 lemma disjI1: "P \<Longrightarrow> P \<or> Q"
   unfolding or_def by (iprover intro: allI impI mp)
@@ -466,14 +527,6 @@
 lemma disjI2: "Q \<Longrightarrow> P \<or> Q"
   unfolding or_def by (iprover intro: allI impI mp)
 
-lemma disjE:
-  assumes major: "P \<or> Q"
-    and minorP: "P \<Longrightarrow> R"
-    and minorQ: "Q \<Longrightarrow> R"
-  shows R
-  by (iprover intro: minorP minorQ impI
-      major [unfolded or_def, THEN spec, THEN mp, THEN mp])
-
 
 subsubsection \<open>Classical logic\<close>
 
diff -r d67d28254ff2 -r ced164fe3bbd src/HOL/document/root.bib
--- a/src/HOL/document/root.bib	Sat Oct 21 18:19:11 2017 +0200
+++ b/src/HOL/document/root.bib	Sun Oct 22 09:10:10 2017 +0200
@@ -1,3 +1,25 @@
+@book{Birkhoff79,
+  author =      {Garret Birkhoff},
+  title =       {Lattice Theory},
+  publisher =   {American Mathematical Society},
+  year=1979
+}
+
+@Book{davenport92,
+  author =	 {H. Davenport},
+  title = 	 {The Higher Arithmetic},
+  publisher = 	 {Cambridge University Press},
+  year = 	 1992
+}
+
+@techreport{Gordon-TR68,
+  author = "Mike Gordon",
+  title = "{HOL}: {A} Machine Oriented Formulation of Higher-Order Logic",
+  institution = "University of Cambridge, Computer Laboratory",
+  number = 68,
+  year = 1985
+}
+
 @book{card-book,
   title = {Introduction to {C}ardinal {A}rithmetic},
   author = {M. Holz and K. Steffens and E. Weitz},
@@ -5,11 +27,13 @@
   year = 1999,
 }
 
-@Book{davenport92,
-  author =	 {H. Davenport},
-  title = 	 {The Higher Arithmetic},
-  publisher = 	 {Cambridge University Press},
-  year = 	 1992
+@book{Nipkow-et-al:2002:tutorial,
+  author =      {T. Nipkow and L. C. Paulson and M. Wenzel},
+  title =       {{Isabelle/HOL} --- A Proof Assistant for Higher-Order Logic},
+  series =      {LNCS},
+  volume =      2283,
+  year =        2002,
+  publisher =   {Springer-Verlag}
 }
 
 @InProceedings{paulin-tlca,
@@ -26,19 +50,3 @@
   year		= 1993,
   publisher	= {Springer},
   series	= {LNCS 664}}
-
-@book{Birkhoff79,
-  author =      {Garret Birkhoff},
-  title =       {Lattice Theory},
-  publisher =   {American Mathematical Society},
-  year=1979
-}
-
-@book{Nipkow-et-al:2002:tutorial,
-  author =      {T. Nipkow and L. C. Paulson and M. Wenzel},
-  title =       {{Isabelle/HOL} --- A Proof Assistant for Higher-Order Logic},
-  series =      {LNCS},
-  volume =      2283,
-  year =        2002,
-  publisher =   {Springer-Verlag}
-}
\ No newline at end of file