src/HOL/Isar_Examples/Higher_Order_Logic.thy
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (23 months ago)
changeset 66695 91500c024c7f
parent 64908 f94ad67a0f6e
child 69593 3dda49e08b9d
permissions -rw-r--r--
tuned;
     1 (*  Title:      HOL/Isar_Examples/Higher_Order_Logic.thy
     2     Author:     Makarius
     3 *)
     4 
     5 section \<open>Foundations of HOL\<close>
     6 
     7 theory Higher_Order_Logic
     8   imports Pure
     9 begin
    10 
    11 text \<open>
    12   The following theory development illustrates the foundations of Higher-Order
    13   Logic. The ``HOL'' logic that is given here resembles @{cite
    14   "Gordon:1985:HOL"} and its predecessor @{cite "church40"}, but the order of
    15   axiomatizations and defined connectives has be adapted to modern
    16   presentations of \<open>\<lambda>\<close>-calculus and Constructive Type Theory. Thus it fits
    17   nicely to the underlying Natural Deduction framework of Isabelle/Pure and
    18   Isabelle/Isar.
    19 \<close>
    20 
    21 
    22 section \<open>HOL syntax within Pure\<close>
    23 
    24 class type
    25 default_sort type
    26 
    27 typedecl o
    28 instance o :: type ..
    29 instance "fun" :: (type, type) type ..
    30 
    31 judgment Trueprop :: "o \<Rightarrow> prop"  ("_" 5)
    32 
    33 
    34 section \<open>Minimal logic (axiomatization)\<close>
    35 
    36 axiomatization imp :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<longrightarrow>" 25)
    37   where impI [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B"
    38     and impE [dest, trans]: "A \<longrightarrow> B \<Longrightarrow> A \<Longrightarrow> B"
    39 
    40 axiomatization All :: "('a \<Rightarrow> o) \<Rightarrow> o"  (binder "\<forall>" 10)
    41   where allI [intro]: "(\<And>x. P x) \<Longrightarrow> \<forall>x. P x"
    42     and allE [dest]: "\<forall>x. P x \<Longrightarrow> P a"
    43 
    44 lemma atomize_imp [atomize]: "(A \<Longrightarrow> B) \<equiv> Trueprop (A \<longrightarrow> B)"
    45   by standard (fact impI, fact impE)
    46 
    47 lemma atomize_all [atomize]: "(\<And>x. P x) \<equiv> Trueprop (\<forall>x. P x)"
    48   by standard (fact allI, fact allE)
    49 
    50 
    51 subsubsection \<open>Derived connectives\<close>
    52 
    53 definition False :: o
    54   where "False \<equiv> \<forall>A. A"
    55 
    56 lemma FalseE [elim]:
    57   assumes "False"
    58   shows A
    59 proof -
    60   from \<open>False\<close> have "\<forall>A. A" by (simp only: False_def)
    61   then show A ..
    62 qed
    63 
    64 
    65 definition True :: o
    66   where "True \<equiv> False \<longrightarrow> False"
    67 
    68 lemma TrueI [intro]: True
    69   unfolding True_def ..
    70 
    71 
    72 definition not :: "o \<Rightarrow> o"  ("\<not> _" [40] 40)
    73   where "not \<equiv> \<lambda>A. A \<longrightarrow> False"
    74 
    75 lemma notI [intro]:
    76   assumes "A \<Longrightarrow> False"
    77   shows "\<not> A"
    78   using assms unfolding not_def ..
    79 
    80 lemma notE [elim]:
    81   assumes "\<not> A" and A
    82   shows B
    83 proof -
    84   from \<open>\<not> A\<close> have "A \<longrightarrow> False" by (simp only: not_def)
    85   from this and \<open>A\<close> have "False" ..
    86   then show B ..
    87 qed
    88 
    89 lemma notE': "A \<Longrightarrow> \<not> A \<Longrightarrow> B"
    90   by (rule notE)
    91 
    92 lemmas contradiction = notE notE'  \<comment> \<open>proof by contradiction in any order\<close>
    93 
    94 
    95 definition conj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<and>" 35)
    96   where "A \<and> B \<equiv> \<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
    97 
    98 lemma conjI [intro]:
    99   assumes A and B
   100   shows "A \<and> B"
   101   unfolding conj_def
   102 proof
   103   fix C
   104   show "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
   105   proof
   106     assume "A \<longrightarrow> B \<longrightarrow> C"
   107     also note \<open>A\<close>
   108     also note \<open>B\<close>
   109     finally show C .
   110   qed
   111 qed
   112 
   113 lemma conjE [elim]:
   114   assumes "A \<and> B"
   115   obtains A and B
   116 proof
   117   from \<open>A \<and> B\<close> have *: "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C" for C
   118     unfolding conj_def ..
   119   show A
   120   proof -
   121     note * [of A]
   122     also have "A \<longrightarrow> B \<longrightarrow> A"
   123     proof
   124       assume A
   125       then show "B \<longrightarrow> A" ..
   126     qed
   127     finally show ?thesis .
   128   qed
   129   show B
   130   proof -
   131     note * [of B]
   132     also have "A \<longrightarrow> B \<longrightarrow> B"
   133     proof
   134       show "B \<longrightarrow> B" ..
   135     qed
   136     finally show ?thesis .
   137   qed
   138 qed
   139 
   140 
   141 definition disj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<or>" 30)
   142   where "A \<or> B \<equiv> \<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
   143 
   144 lemma disjI1 [intro]:
   145   assumes A
   146   shows "A \<or> B"
   147   unfolding disj_def
   148 proof
   149   fix C
   150   show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
   151   proof
   152     assume "A \<longrightarrow> C"
   153     from this and \<open>A\<close> have C ..
   154     then show "(B \<longrightarrow> C) \<longrightarrow> C" ..
   155   qed
   156 qed
   157 
   158 lemma disjI2 [intro]:
   159   assumes B
   160   shows "A \<or> B"
   161   unfolding disj_def
   162 proof
   163   fix C
   164   show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
   165   proof
   166     show "(B \<longrightarrow> C) \<longrightarrow> C"
   167     proof
   168       assume "B \<longrightarrow> C"
   169       from this and \<open>B\<close> show C ..
   170     qed
   171   qed
   172 qed
   173 
   174 lemma disjE [elim]:
   175   assumes "A \<or> B"
   176   obtains (a) A | (b) B
   177 proof -
   178   from \<open>A \<or> B\<close> have "(A \<longrightarrow> thesis) \<longrightarrow> (B \<longrightarrow> thesis) \<longrightarrow> thesis"
   179     unfolding disj_def ..
   180   also have "A \<longrightarrow> thesis"
   181   proof
   182     assume A
   183     then show thesis by (rule a)
   184   qed
   185   also have "B \<longrightarrow> thesis"
   186   proof
   187     assume B
   188     then show thesis by (rule b)
   189   qed
   190   finally show thesis .
   191 qed
   192 
   193 
   194 definition Ex :: "('a \<Rightarrow> o) \<Rightarrow> o"  (binder "\<exists>" 10)
   195   where "\<exists>x. P x \<equiv> \<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
   196 
   197 lemma exI [intro]: "P a \<Longrightarrow> \<exists>x. P x"
   198   unfolding Ex_def
   199 proof
   200   fix C
   201   assume "P a"
   202   show "(\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
   203   proof
   204     assume "\<forall>x. P x \<longrightarrow> C"
   205     then have "P a \<longrightarrow> C" ..
   206     from this and \<open>P a\<close> show C ..
   207   qed
   208 qed
   209 
   210 lemma exE [elim]:
   211   assumes "\<exists>x. P x"
   212   obtains (that) x where "P x"
   213 proof -
   214   from \<open>\<exists>x. P x\<close> have "(\<forall>x. P x \<longrightarrow> thesis) \<longrightarrow> thesis"
   215     unfolding Ex_def ..
   216   also have "\<forall>x. P x \<longrightarrow> thesis"
   217   proof
   218     fix x
   219     show "P x \<longrightarrow> thesis"
   220     proof
   221       assume "P x"
   222       then show thesis by (rule that)
   223     qed
   224   qed
   225   finally show thesis .
   226 qed
   227 
   228 
   229 subsubsection \<open>Extensional equality\<close>
   230 
   231 axiomatization equal :: "'a \<Rightarrow> 'a \<Rightarrow> o"  (infixl "=" 50)
   232   where refl [intro]: "x = x"
   233     and subst: "x = y \<Longrightarrow> P x \<Longrightarrow> P y"
   234 
   235 abbreviation not_equal :: "'a \<Rightarrow> 'a \<Rightarrow> o"  (infixl "\<noteq>" 50)
   236   where "x \<noteq> y \<equiv> \<not> (x = y)"
   237 
   238 abbreviation iff :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<longleftrightarrow>" 25)
   239   where "A \<longleftrightarrow> B \<equiv> A = B"
   240 
   241 axiomatization
   242   where ext [intro]: "(\<And>x. f x = g x) \<Longrightarrow> f = g"
   243     and iff [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A \<longleftrightarrow> B"
   244 
   245 lemma sym [sym]: "y = x" if "x = y"
   246   using that by (rule subst) (rule refl)
   247 
   248 lemma [trans]: "x = y \<Longrightarrow> P y \<Longrightarrow> P x"
   249   by (rule subst) (rule sym)
   250 
   251 lemma [trans]: "P x \<Longrightarrow> x = y \<Longrightarrow> P y"
   252   by (rule subst)
   253 
   254 lemma arg_cong: "f x = f y" if "x = y"
   255   using that by (rule subst) (rule refl)
   256 
   257 lemma fun_cong: "f x = g x" if "f = g"
   258   using that by (rule subst) (rule refl)
   259 
   260 lemma trans [trans]: "x = y \<Longrightarrow> y = z \<Longrightarrow> x = z"
   261   by (rule subst)
   262 
   263 lemma iff1 [elim]: "A \<longleftrightarrow> B \<Longrightarrow> A \<Longrightarrow> B"
   264   by (rule subst)
   265 
   266 lemma iff2 [elim]: "A \<longleftrightarrow> B \<Longrightarrow> B \<Longrightarrow> A"
   267   by (rule subst) (rule sym)
   268 
   269 
   270 subsection \<open>Cantor's Theorem\<close>
   271 
   272 text \<open>
   273   Cantor's Theorem states that there is no surjection from a set to its
   274   powerset. The subsequent formulation uses elementary \<open>\<lambda>\<close>-calculus and
   275   predicate logic, with standard introduction and elimination rules.
   276 \<close>
   277 
   278 lemma iff_contradiction:
   279   assumes *: "\<not> A \<longleftrightarrow> A"
   280   shows C
   281 proof (rule notE)
   282   show "\<not> A"
   283   proof
   284     assume A
   285     with * have "\<not> A" ..
   286     from this and \<open>A\<close> show False ..
   287   qed
   288   with * show A ..
   289 qed
   290 
   291 theorem Cantor: "\<not> (\<exists>f :: 'a \<Rightarrow> 'a \<Rightarrow> o. \<forall>A. \<exists>x. A = f x)"
   292 proof
   293   assume "\<exists>f :: 'a \<Rightarrow> 'a \<Rightarrow> o. \<forall>A. \<exists>x. A = f x"
   294   then obtain f :: "'a \<Rightarrow> 'a \<Rightarrow> o" where *: "\<forall>A. \<exists>x. A = f x" ..
   295   let ?D = "\<lambda>x. \<not> f x x"
   296   from * have "\<exists>x. ?D = f x" ..
   297   then obtain a where "?D = f a" ..
   298   then have "?D a \<longleftrightarrow> f a a" using refl by (rule subst)
   299   then have "\<not> f a a \<longleftrightarrow> f a a" .
   300   then show False by (rule iff_contradiction)
   301 qed
   302 
   303 
   304 subsection \<open>Characterization of Classical Logic\<close>
   305 
   306 text \<open>
   307   The subsequent rules of classical reasoning are all equivalent.
   308 \<close>
   309 
   310 locale classical =
   311   assumes classical: "(\<not> A \<Longrightarrow> A) \<Longrightarrow> A"
   312   \<comment> \<open>predicate definition and hypothetical context\<close>
   313 begin
   314 
   315 lemma classical_contradiction:
   316   assumes "\<not> A \<Longrightarrow> False"
   317   shows A
   318 proof (rule classical)
   319   assume "\<not> A"
   320   then have False by (rule assms)
   321   then show A ..
   322 qed
   323 
   324 lemma double_negation:
   325   assumes "\<not> \<not> A"
   326   shows A
   327 proof (rule classical_contradiction)
   328   assume "\<not> A"
   329   with \<open>\<not> \<not> A\<close> show False by (rule contradiction)
   330 qed
   331 
   332 lemma tertium_non_datur: "A \<or> \<not> A"
   333 proof (rule double_negation)
   334   show "\<not> \<not> (A \<or> \<not> A)"
   335   proof
   336     assume "\<not> (A \<or> \<not> A)"
   337     have "\<not> A"
   338     proof
   339       assume A then have "A \<or> \<not> A" ..
   340       with \<open>\<not> (A \<or> \<not> A)\<close> show False by (rule contradiction)
   341     qed
   342     then have "A \<or> \<not> A" ..
   343     with \<open>\<not> (A \<or> \<not> A)\<close> show False by (rule contradiction)
   344   qed
   345 qed
   346 
   347 lemma classical_cases:
   348   obtains A | "\<not> A"
   349   using tertium_non_datur
   350 proof
   351   assume A
   352   then show thesis ..
   353 next
   354   assume "\<not> A"
   355   then show thesis ..
   356 qed
   357 
   358 end
   359 
   360 lemma classical_if_cases: classical
   361   if cases: "\<And>A C. (A \<Longrightarrow> C) \<Longrightarrow> (\<not> A \<Longrightarrow> C) \<Longrightarrow> C"
   362 proof
   363   fix A
   364   assume *: "\<not> A \<Longrightarrow> A"
   365   show A
   366   proof (rule cases)
   367     assume A
   368     then show A .
   369   next
   370     assume "\<not> A"
   371     then show A by (rule *)
   372   qed
   373 qed
   374 
   375 
   376 section \<open>Peirce's Law\<close>
   377 
   378 text \<open>
   379   Peirce's Law is another characterization of classical reasoning. Its
   380   statement only requires implication.
   381 \<close>
   382 
   383 theorem (in classical) Peirce's_Law: "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"
   384 proof
   385   assume *: "(A \<longrightarrow> B) \<longrightarrow> A"
   386   show A
   387   proof (rule classical)
   388     assume "\<not> A"
   389     have "A \<longrightarrow> B"
   390     proof
   391       assume A
   392       with \<open>\<not> A\<close> show B by (rule contradiction)
   393     qed
   394     with * show A ..
   395   qed
   396 qed
   397 
   398 
   399 section \<open>Hilbert's choice operator (axiomatization)\<close>
   400 
   401 axiomatization Eps :: "('a \<Rightarrow> o) \<Rightarrow> 'a"
   402   where someI: "P x \<Longrightarrow> P (Eps P)"
   403 
   404 syntax "_Eps" :: "pttrn \<Rightarrow> o \<Rightarrow> 'a"  ("(3SOME _./ _)" [0, 10] 10)
   405 translations "SOME x. P" \<rightleftharpoons> "CONST Eps (\<lambda>x. P)"
   406 
   407 text \<open>
   408   \<^medskip>
   409   It follows a derivation of the classical law of tertium-non-datur by
   410   means of Hilbert's choice operator (due to Berghofer, Beeson, Harrison,
   411   based on a proof by Diaconescu).
   412   \<^medskip>
   413 \<close>
   414 
   415 theorem Diaconescu: "A \<or> \<not> A"
   416 proof -
   417   let ?P = "\<lambda>x. (A \<and> x) \<or> \<not> x"
   418   let ?Q = "\<lambda>x. (A \<and> \<not> x) \<or> x"
   419 
   420   have a: "?P (Eps ?P)"
   421   proof (rule someI)
   422     have "\<not> False" ..
   423     then show "?P False" ..
   424   qed
   425   have b: "?Q (Eps ?Q)"
   426   proof (rule someI)
   427     have True ..
   428     then show "?Q True" ..
   429   qed
   430 
   431   from a show ?thesis
   432   proof
   433     assume "A \<and> Eps ?P"
   434     then have A ..
   435     then show ?thesis ..
   436   next
   437     assume "\<not> Eps ?P"
   438     from b show ?thesis
   439     proof
   440       assume "A \<and> \<not> Eps ?Q"
   441       then have A ..
   442       then show ?thesis ..
   443     next
   444       assume "Eps ?Q"
   445       have neq: "?P \<noteq> ?Q"
   446       proof
   447         assume "?P = ?Q"
   448         then have "Eps ?P \<longleftrightarrow> Eps ?Q" by (rule arg_cong)
   449         also note \<open>Eps ?Q\<close>
   450         finally have "Eps ?P" .
   451         with \<open>\<not> Eps ?P\<close> show False by (rule contradiction)
   452       qed
   453       have "\<not> A"
   454       proof
   455         assume A
   456         have "?P = ?Q"
   457         proof (rule ext)
   458           show "?P x \<longleftrightarrow> ?Q x" for x
   459           proof
   460             assume "?P x"
   461             then show "?Q x"
   462             proof
   463               assume "\<not> x"
   464               with \<open>A\<close> have "A \<and> \<not> x" ..
   465               then show ?thesis ..
   466             next
   467               assume "A \<and> x"
   468               then have x ..
   469               then show ?thesis ..
   470             qed
   471           next
   472             assume "?Q x"
   473             then show "?P x"
   474             proof
   475               assume "A \<and> \<not> x"
   476               then have "\<not> x" ..
   477               then show ?thesis ..
   478             next
   479               assume x
   480               with \<open>A\<close> have "A \<and> x" ..
   481               then show ?thesis ..
   482             qed
   483           qed
   484         qed
   485         with neq show False by (rule contradiction)
   486       qed
   487       then show ?thesis ..
   488     qed
   489   qed
   490 qed
   491 
   492 text \<open>
   493   This means, the hypothetical predicate @{const classical} always holds
   494   unconditionally (with all consequences).
   495 \<close>
   496 
   497 interpretation classical
   498 proof (rule classical_if_cases)
   499   fix A C
   500   assume *: "A \<Longrightarrow> C"
   501     and **: "\<not> A \<Longrightarrow> C"
   502   from Diaconescu [of A] show C
   503   proof
   504     assume A
   505     then show C by (rule *)
   506   next
   507     assume "\<not> A"
   508     then show C by (rule **)
   509   qed
   510 qed
   511 
   512 thm classical
   513   classical_contradiction
   514   double_negation
   515   tertium_non_datur
   516   classical_cases
   517   Peirce's_Law
   518 
   519 end