derived axiom iffI as a lemma (thanks to Alexander Maletzky)
authornipkow
Sun Oct 22 09:10:10 2017 +0200 (19 months ago)
changeset 66893ced164fe3bbd
parent 66892 d67d28254ff2
child 66894 c08d7349774e
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
CONTRIBUTORS
src/HOL/HOL.thy
src/HOL/document/root.bib
     1.1 --- a/CONTRIBUTORS	Sat Oct 21 18:19:11 2017 +0200
     1.2 +++ b/CONTRIBUTORS	Sun Oct 22 09:10:10 2017 +0200
     1.3 @@ -6,6 +6,8 @@
     1.4  Contributions to this Isabelle version
     1.5  --------------------------------------
     1.6  
     1.7 +* October 2017: Alexander Maletzky
     1.8 +  Derivation of axiom "iff" in HOL.thy from the other axioms.
     1.9  
    1.10  Contributions to Isabelle2017
    1.11  -----------------------------
     2.1 --- a/src/HOL/HOL.thy	Sat Oct 21 18:19:11 2017 +0200
     2.2 +++ b/src/HOL/HOL.thy	Sun Oct 22 09:10:10 2017 +0200
     2.3 @@ -55,6 +55,15 @@
     2.4  
     2.5  subsection \<open>Primitive logic\<close>
     2.6  
     2.7 +text \<open>
     2.8 +The definition of the logic is based on Mike Gordon's technical report \cite{Gordon-TR68} that
     2.9 +describes the first implementation of HOL. However, there are a number of differences.
    2.10 +In particular, we start with the definite description operator and introduce Hilbert's \<open>\<epsilon>\<close> operator
    2.11 +only much later. Moreover, axiom \<open>(P \<longrightarrow> Q) \<longrightarrow> (Q \<longrightarrow> P) \<longrightarrow> (P = Q)\<close> is derived from the other
    2.12 +axioms. The fact that this axiom is derivable was first noticed by Bruno Barras (for Mike Gordon's
    2.13 +line of HOL systems) and later independently by Alexander Maletzky (for Isabelle/HOL).
    2.14 +\<close>
    2.15 +
    2.16  subsubsection \<open>Core syntax\<close>
    2.17  
    2.18  setup \<open>Axclass.class_axiomatization (@{binding type}, [])\<close>
    2.19 @@ -195,7 +204,6 @@
    2.20    impI: "(P \<Longrightarrow> Q) \<Longrightarrow> P \<longrightarrow> Q" and
    2.21    mp: "\<lbrakk>P \<longrightarrow> Q; P\<rbrakk> \<Longrightarrow> Q" and
    2.22  
    2.23 -  iff: "(P \<longrightarrow> Q) \<longrightarrow> (Q \<longrightarrow> P) \<longrightarrow> (P = Q)" and
    2.24    True_or_False: "(P = True) \<or> (P = False)"
    2.25  
    2.26  definition If :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" ("(if (_)/ then (_)/ else (_))" [0, 0, 10] 10)
    2.27 @@ -283,9 +291,6 @@
    2.28  
    2.29  subsubsection \<open>Equality of booleans -- iff\<close>
    2.30  
    2.31 -lemma iffI: assumes "P \<Longrightarrow> Q" and "Q \<Longrightarrow> P" shows "P = Q"
    2.32 -  by (iprover intro: iff [THEN mp, THEN mp] impI assms)
    2.33 -
    2.34  lemma iffD2: "\<lbrakk>P = Q; Q\<rbrakk> \<Longrightarrow> P"
    2.35    by (erule ssubst)
    2.36  
    2.37 @@ -305,24 +310,16 @@
    2.38    by (iprover intro: minor impI major [THEN iffD2] major [THEN iffD1])
    2.39  
    2.40  
    2.41 -subsubsection \<open>True\<close>
    2.42 +subsubsection \<open>True (1)\<close>
    2.43  
    2.44  lemma TrueI: True
    2.45    unfolding True_def by (rule refl)
    2.46  
    2.47 -lemma eqTrueI: "P \<Longrightarrow> P = True"
    2.48 -  by (iprover intro: iffI TrueI)
    2.49 -
    2.50  lemma eqTrueE: "P = True \<Longrightarrow> P"
    2.51    by (erule iffD2) (rule TrueI)
    2.52  
    2.53  
    2.54 -subsubsection \<open>Universal quantifier\<close>
    2.55 -
    2.56 -lemma allI:
    2.57 -  assumes "\<And>x::'a. P x"
    2.58 -  shows "\<forall>x. P x"
    2.59 -  unfolding All_def by (iprover intro: ext eqTrueI assms)
    2.60 +subsubsection \<open>Universal quantifier (1)\<close>
    2.61  
    2.62  lemma spec: "\<forall>x::'a. P x \<Longrightarrow> P x"
    2.63    apply (unfold All_def)
    2.64 @@ -420,6 +417,70 @@
    2.65    by (erule subst, erule ssubst, assumption)
    2.66  
    2.67  
    2.68 +subsubsection \<open>Disjunction (1)\<close>
    2.69 +
    2.70 +lemma disjE:
    2.71 +  assumes major: "P \<or> Q"
    2.72 +    and minorP: "P \<Longrightarrow> R"
    2.73 +    and minorQ: "Q \<Longrightarrow> R"
    2.74 +  shows R
    2.75 +  by (iprover intro: minorP minorQ impI
    2.76 +      major [unfolded or_def, THEN spec, THEN mp, THEN mp])
    2.77 +
    2.78 +
    2.79 +subsubsection \<open>Derivation of \<open>iffI\<close>\<close>
    2.80 +
    2.81 +text \<open>In an intuitionistic version of HOL \<open>iffI\<close> needs to be an axiom.\<close>
    2.82 +
    2.83 +lemma iffI:
    2.84 +  assumes "P \<Longrightarrow> Q" and "Q \<Longrightarrow> P"
    2.85 +  shows "P = Q"
    2.86 +proof (rule disjE[OF True_or_False[of P]])
    2.87 +  assume 1: "P = True"
    2.88 +  note Q = assms(1)[OF eqTrueE[OF this]]
    2.89 +  from 1 show ?thesis
    2.90 +  proof (rule ssubst)
    2.91 +    from True_or_False[of Q] show "True = Q"
    2.92 +    proof (rule disjE)
    2.93 +      assume "Q = True"
    2.94 +      thus ?thesis by(rule sym)
    2.95 +    next
    2.96 +      assume "Q = False"
    2.97 +      with Q have False by (rule rev_iffD1)
    2.98 +      thus ?thesis by (rule FalseE)
    2.99 +    qed
   2.100 +  qed
   2.101 +next
   2.102 +  assume 2: "P = False"
   2.103 +  thus ?thesis
   2.104 +  proof (rule ssubst)
   2.105 +    from True_or_False[of Q] show "False = Q"
   2.106 +    proof (rule disjE)
   2.107 +      assume "Q = True"
   2.108 +      from 2 assms(2)[OF eqTrueE[OF this]] have False by (rule iffD1)
   2.109 +      thus ?thesis by (rule FalseE)
   2.110 +    next
   2.111 +      assume "Q = False"
   2.112 +      thus ?thesis by(rule sym)
   2.113 +    qed
   2.114 +  qed
   2.115 +qed
   2.116 +
   2.117 +
   2.118 +subsubsection \<open>True (2)\<close>
   2.119 +
   2.120 +lemma eqTrueI: "P \<Longrightarrow> P = True"
   2.121 +  by (iprover intro: iffI TrueI)
   2.122 +
   2.123 +
   2.124 +subsubsection \<open>Universal quantifier (2)\<close>
   2.125 +
   2.126 +lemma allI:
   2.127 +  assumes "\<And>x::'a. P x"
   2.128 +  shows "\<forall>x. P x"
   2.129 +  unfolding All_def by (iprover intro: ext eqTrueI assms)
   2.130 +
   2.131 +
   2.132  subsubsection \<open>Existential quantifier\<close>
   2.133  
   2.134  lemma exI: "P x \<Longrightarrow> \<exists>x::'a. P x"
   2.135 @@ -458,7 +519,7 @@
   2.136    by (iprover intro: conjI assms)
   2.137  
   2.138  
   2.139 -subsubsection \<open>Disjunction\<close>
   2.140 +subsubsection \<open>Disjunction (2)\<close>
   2.141  
   2.142  lemma disjI1: "P \<Longrightarrow> P \<or> Q"
   2.143    unfolding or_def by (iprover intro: allI impI mp)
   2.144 @@ -466,14 +527,6 @@
   2.145  lemma disjI2: "Q \<Longrightarrow> P \<or> Q"
   2.146    unfolding or_def by (iprover intro: allI impI mp)
   2.147  
   2.148 -lemma disjE:
   2.149 -  assumes major: "P \<or> Q"
   2.150 -    and minorP: "P \<Longrightarrow> R"
   2.151 -    and minorQ: "Q \<Longrightarrow> R"
   2.152 -  shows R
   2.153 -  by (iprover intro: minorP minorQ impI
   2.154 -      major [unfolded or_def, THEN spec, THEN mp, THEN mp])
   2.155 -
   2.156  
   2.157  subsubsection \<open>Classical logic\<close>
   2.158  
     3.1 --- a/src/HOL/document/root.bib	Sat Oct 21 18:19:11 2017 +0200
     3.2 +++ b/src/HOL/document/root.bib	Sun Oct 22 09:10:10 2017 +0200
     3.3 @@ -1,3 +1,25 @@
     3.4 +@book{Birkhoff79,
     3.5 +  author =      {Garret Birkhoff},
     3.6 +  title =       {Lattice Theory},
     3.7 +  publisher =   {American Mathematical Society},
     3.8 +  year=1979
     3.9 +}
    3.10 +
    3.11 +@Book{davenport92,
    3.12 +  author =	 {H. Davenport},
    3.13 +  title = 	 {The Higher Arithmetic},
    3.14 +  publisher = 	 {Cambridge University Press},
    3.15 +  year = 	 1992
    3.16 +}
    3.17 +
    3.18 +@techreport{Gordon-TR68,
    3.19 +  author = "Mike Gordon",
    3.20 +  title = "{HOL}: {A} Machine Oriented Formulation of Higher-Order Logic",
    3.21 +  institution = "University of Cambridge, Computer Laboratory",
    3.22 +  number = 68,
    3.23 +  year = 1985
    3.24 +}
    3.25 +
    3.26  @book{card-book,
    3.27    title = {Introduction to {C}ardinal {A}rithmetic},
    3.28    author = {M. Holz and K. Steffens and E. Weitz},
    3.29 @@ -5,11 +27,13 @@
    3.30    year = 1999,
    3.31  }
    3.32  
    3.33 -@Book{davenport92,
    3.34 -  author =	 {H. Davenport},
    3.35 -  title = 	 {The Higher Arithmetic},
    3.36 -  publisher = 	 {Cambridge University Press},
    3.37 -  year = 	 1992
    3.38 +@book{Nipkow-et-al:2002:tutorial,
    3.39 +  author =      {T. Nipkow and L. C. Paulson and M. Wenzel},
    3.40 +  title =       {{Isabelle/HOL} --- A Proof Assistant for Higher-Order Logic},
    3.41 +  series =      {LNCS},
    3.42 +  volume =      2283,
    3.43 +  year =        2002,
    3.44 +  publisher =   {Springer-Verlag}
    3.45  }
    3.46  
    3.47  @InProceedings{paulin-tlca,
    3.48 @@ -26,19 +50,3 @@
    3.49    year		= 1993,
    3.50    publisher	= {Springer},
    3.51    series	= {LNCS 664}}
    3.52 -
    3.53 -@book{Birkhoff79,
    3.54 -  author =      {Garret Birkhoff},
    3.55 -  title =       {Lattice Theory},
    3.56 -  publisher =   {American Mathematical Society},
    3.57 -  year=1979
    3.58 -}
    3.59 -
    3.60 -@book{Nipkow-et-al:2002:tutorial,
    3.61 -  author =      {T. Nipkow and L. C. Paulson and M. Wenzel},
    3.62 -  title =       {{Isabelle/HOL} --- A Proof Assistant for Higher-Order Logic},
    3.63 -  series =      {LNCS},
    3.64 -  volume =      2283,
    3.65 -  year =        2002,
    3.66 -  publisher =   {Springer-Verlag}
    3.67 -}
    3.68 \ No newline at end of file