summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Sun, 22 Oct 2017 09:10:10 +0200 | |

changeset 66893 | ced164fe3bbd |

parent 66892 | d67d28254ff2 |

child 66894 | c08d7349774e |

derived axiom iffI as a lemma (thanks to Alexander Maletzky)

CONTRIBUTORS | file | annotate | diff | comparison | revisions | |

src/HOL/HOL.thy | file | annotate | diff | comparison | revisions | |

src/HOL/document/root.bib | file | annotate | diff | comparison | revisions |

--- 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 -----------------------------

--- 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>

--- 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