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