src/HOL/HOL.thy
changeset 66893 ced164fe3bbd
parent 66836 4eb431c3f974
child 67091 1393c2340eec
     1.1 --- a/src/HOL/HOL.thy	Sat Oct 21 18:19:11 2017 +0200
     1.2 +++ b/src/HOL/HOL.thy	Sun Oct 22 09:10:10 2017 +0200
     1.3 @@ -55,6 +55,15 @@
     1.4  
     1.5  subsection \<open>Primitive logic\<close>
     1.6  
     1.7 +text \<open>
     1.8 +The definition of the logic is based on Mike Gordon's technical report \cite{Gordon-TR68} that
     1.9 +describes the first implementation of HOL. However, there are a number of differences.
    1.10 +In particular, we start with the definite description operator and introduce Hilbert's \<open>\<epsilon>\<close> operator
    1.11 +only much later. Moreover, axiom \<open>(P \<longrightarrow> Q) \<longrightarrow> (Q \<longrightarrow> P) \<longrightarrow> (P = Q)\<close> is derived from the other
    1.12 +axioms. The fact that this axiom is derivable was first noticed by Bruno Barras (for Mike Gordon's
    1.13 +line of HOL systems) and later independently by Alexander Maletzky (for Isabelle/HOL).
    1.14 +\<close>
    1.15 +
    1.16  subsubsection \<open>Core syntax\<close>
    1.17  
    1.18  setup \<open>Axclass.class_axiomatization (@{binding type}, [])\<close>
    1.19 @@ -195,7 +204,6 @@
    1.20    impI: "(P \<Longrightarrow> Q) \<Longrightarrow> P \<longrightarrow> Q" and
    1.21    mp: "\<lbrakk>P \<longrightarrow> Q; P\<rbrakk> \<Longrightarrow> Q" and
    1.22  
    1.23 -  iff: "(P \<longrightarrow> Q) \<longrightarrow> (Q \<longrightarrow> P) \<longrightarrow> (P = Q)" and
    1.24    True_or_False: "(P = True) \<or> (P = False)"
    1.25  
    1.26  definition If :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" ("(if (_)/ then (_)/ else (_))" [0, 0, 10] 10)
    1.27 @@ -283,9 +291,6 @@
    1.28  
    1.29  subsubsection \<open>Equality of booleans -- iff\<close>
    1.30  
    1.31 -lemma iffI: assumes "P \<Longrightarrow> Q" and "Q \<Longrightarrow> P" shows "P = Q"
    1.32 -  by (iprover intro: iff [THEN mp, THEN mp] impI assms)
    1.33 -
    1.34  lemma iffD2: "\<lbrakk>P = Q; Q\<rbrakk> \<Longrightarrow> P"
    1.35    by (erule ssubst)
    1.36  
    1.37 @@ -305,24 +310,16 @@
    1.38    by (iprover intro: minor impI major [THEN iffD2] major [THEN iffD1])
    1.39  
    1.40  
    1.41 -subsubsection \<open>True\<close>
    1.42 +subsubsection \<open>True (1)\<close>
    1.43  
    1.44  lemma TrueI: True
    1.45    unfolding True_def by (rule refl)
    1.46  
    1.47 -lemma eqTrueI: "P \<Longrightarrow> P = True"
    1.48 -  by (iprover intro: iffI TrueI)
    1.49 -
    1.50  lemma eqTrueE: "P = True \<Longrightarrow> P"
    1.51    by (erule iffD2) (rule TrueI)
    1.52  
    1.53  
    1.54 -subsubsection \<open>Universal quantifier\<close>
    1.55 -
    1.56 -lemma allI:
    1.57 -  assumes "\<And>x::'a. P x"
    1.58 -  shows "\<forall>x. P x"
    1.59 -  unfolding All_def by (iprover intro: ext eqTrueI assms)
    1.60 +subsubsection \<open>Universal quantifier (1)\<close>
    1.61  
    1.62  lemma spec: "\<forall>x::'a. P x \<Longrightarrow> P x"
    1.63    apply (unfold All_def)
    1.64 @@ -420,6 +417,70 @@
    1.65    by (erule subst, erule ssubst, assumption)
    1.66  
    1.67  
    1.68 +subsubsection \<open>Disjunction (1)\<close>
    1.69 +
    1.70 +lemma disjE:
    1.71 +  assumes major: "P \<or> Q"
    1.72 +    and minorP: "P \<Longrightarrow> R"
    1.73 +    and minorQ: "Q \<Longrightarrow> R"
    1.74 +  shows R
    1.75 +  by (iprover intro: minorP minorQ impI
    1.76 +      major [unfolded or_def, THEN spec, THEN mp, THEN mp])
    1.77 +
    1.78 +
    1.79 +subsubsection \<open>Derivation of \<open>iffI\<close>\<close>
    1.80 +
    1.81 +text \<open>In an intuitionistic version of HOL \<open>iffI\<close> needs to be an axiom.\<close>
    1.82 +
    1.83 +lemma iffI:
    1.84 +  assumes "P \<Longrightarrow> Q" and "Q \<Longrightarrow> P"
    1.85 +  shows "P = Q"
    1.86 +proof (rule disjE[OF True_or_False[of P]])
    1.87 +  assume 1: "P = True"
    1.88 +  note Q = assms(1)[OF eqTrueE[OF this]]
    1.89 +  from 1 show ?thesis
    1.90 +  proof (rule ssubst)
    1.91 +    from True_or_False[of Q] show "True = Q"
    1.92 +    proof (rule disjE)
    1.93 +      assume "Q = True"
    1.94 +      thus ?thesis by(rule sym)
    1.95 +    next
    1.96 +      assume "Q = False"
    1.97 +      with Q have False by (rule rev_iffD1)
    1.98 +      thus ?thesis by (rule FalseE)
    1.99 +    qed
   1.100 +  qed
   1.101 +next
   1.102 +  assume 2: "P = False"
   1.103 +  thus ?thesis
   1.104 +  proof (rule ssubst)
   1.105 +    from True_or_False[of Q] show "False = Q"
   1.106 +    proof (rule disjE)
   1.107 +      assume "Q = True"
   1.108 +      from 2 assms(2)[OF eqTrueE[OF this]] have False by (rule iffD1)
   1.109 +      thus ?thesis by (rule FalseE)
   1.110 +    next
   1.111 +      assume "Q = False"
   1.112 +      thus ?thesis by(rule sym)
   1.113 +    qed
   1.114 +  qed
   1.115 +qed
   1.116 +
   1.117 +
   1.118 +subsubsection \<open>True (2)\<close>
   1.119 +
   1.120 +lemma eqTrueI: "P \<Longrightarrow> P = True"
   1.121 +  by (iprover intro: iffI TrueI)
   1.122 +
   1.123 +
   1.124 +subsubsection \<open>Universal quantifier (2)\<close>
   1.125 +
   1.126 +lemma allI:
   1.127 +  assumes "\<And>x::'a. P x"
   1.128 +  shows "\<forall>x. P x"
   1.129 +  unfolding All_def by (iprover intro: ext eqTrueI assms)
   1.130 +
   1.131 +
   1.132  subsubsection \<open>Existential quantifier\<close>
   1.133  
   1.134  lemma exI: "P x \<Longrightarrow> \<exists>x::'a. P x"
   1.135 @@ -458,7 +519,7 @@
   1.136    by (iprover intro: conjI assms)
   1.137  
   1.138  
   1.139 -subsubsection \<open>Disjunction\<close>
   1.140 +subsubsection \<open>Disjunction (2)\<close>
   1.141  
   1.142  lemma disjI1: "P \<Longrightarrow> P \<or> Q"
   1.143    unfolding or_def by (iprover intro: allI impI mp)
   1.144 @@ -466,14 +527,6 @@
   1.145  lemma disjI2: "Q \<Longrightarrow> P \<or> Q"
   1.146    unfolding or_def by (iprover intro: allI impI mp)
   1.147  
   1.148 -lemma disjE:
   1.149 -  assumes major: "P \<or> Q"
   1.150 -    and minorP: "P \<Longrightarrow> R"
   1.151 -    and minorQ: "Q \<Longrightarrow> R"
   1.152 -  shows R
   1.153 -  by (iprover intro: minorP minorQ impI
   1.154 -      major [unfolded or_def, THEN spec, THEN mp, THEN mp])
   1.155 -
   1.156  
   1.157  subsubsection \<open>Classical logic\<close>
   1.158