src/HOL/ex/Higher_Order_Logic.thy
author haftmann
Fri Oct 10 19:55:32 2014 +0200 (2014-10-10)
changeset 58646 cd63a4b12a33
parent 58622 aa99568f56de
child 58889 5b7a9633cfa8
permissions -rw-r--r--
specialized specification: avoid trivial instances
     1 (*  Title:      HOL/ex/Higher_Order_Logic.thy
     2     Author:     Gertrud Bauer and Markus Wenzel, TU Muenchen
     3 *)
     4 
     5 header {* Foundations of HOL *}
     6 
     7 theory Higher_Order_Logic imports Pure begin
     8 
     9 text {*
    10   The following theory development demonstrates Higher-Order Logic
    11   itself, represented directly within the Pure framework of Isabelle.
    12   The ``HOL'' logic given here is essentially that of Gordon
    13   @{cite "Gordon:1985:HOL"}, although we prefer to present basic concepts
    14   in a slightly more conventional manner oriented towards plain
    15   Natural Deduction.
    16 *}
    17 
    18 
    19 subsection {* Pure Logic *}
    20 
    21 class type
    22 default_sort type
    23 
    24 typedecl o
    25 instance o :: type ..
    26 instance "fun" :: (type, type) type ..
    27 
    28 
    29 subsubsection {* Basic logical connectives *}
    30 
    31 judgment
    32   Trueprop :: "o \<Rightarrow> prop"    ("_" 5)
    33 
    34 axiomatization
    35   imp :: "o \<Rightarrow> o \<Rightarrow> o"    (infixr "\<longrightarrow>" 25) and
    36   All :: "('a \<Rightarrow> o) \<Rightarrow> o"    (binder "\<forall>" 10)
    37 where
    38   impI [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B" and
    39   impE [dest, trans]: "A \<longrightarrow> B \<Longrightarrow> A \<Longrightarrow> B" and
    40   allI [intro]: "(\<And>x. P x) \<Longrightarrow> \<forall>x. P x" and
    41   allE [dest]: "\<forall>x. P x \<Longrightarrow> P a"
    42 
    43 
    44 subsubsection {* Extensional equality *}
    45 
    46 axiomatization
    47   equal :: "'a \<Rightarrow> 'a \<Rightarrow> o"   (infixl "=" 50)
    48 where
    49   refl [intro]: "x = x" and
    50   subst: "x = y \<Longrightarrow> P x \<Longrightarrow> P y"
    51 
    52 axiomatization where
    53   ext [intro]: "(\<And>x. f x = g x) \<Longrightarrow> f = g" and
    54   iff [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A = B"
    55 
    56 theorem sym [sym]: "x = y \<Longrightarrow> y = x"
    57 proof -
    58   assume "x = y"
    59   then show "y = x" by (rule subst) (rule refl)
    60 qed
    61 
    62 lemma [trans]: "x = y \<Longrightarrow> P y \<Longrightarrow> P x"
    63   by (rule subst) (rule sym)
    64 
    65 lemma [trans]: "P x \<Longrightarrow> x = y \<Longrightarrow> P y"
    66   by (rule subst)
    67 
    68 theorem trans [trans]: "x = y \<Longrightarrow> y = z \<Longrightarrow> x = z"
    69   by (rule subst)
    70 
    71 theorem iff1 [elim]: "A = B \<Longrightarrow> A \<Longrightarrow> B"
    72   by (rule subst)
    73 
    74 theorem iff2 [elim]: "A = B \<Longrightarrow> B \<Longrightarrow> A"
    75   by (rule subst) (rule sym)
    76 
    77 
    78 subsubsection {* Derived connectives *}
    79 
    80 definition
    81   false :: o  ("\<bottom>") where
    82   "\<bottom> \<equiv> \<forall>A. A"
    83 
    84 definition
    85   true :: o  ("\<top>") where
    86   "\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>"
    87 
    88 definition
    89   not :: "o \<Rightarrow> o"  ("\<not> _" [40] 40) where
    90   "not \<equiv> \<lambda>A. A \<longrightarrow> \<bottom>"
    91 
    92 definition
    93   conj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<and>" 35) where
    94   "conj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
    95 
    96 definition
    97   disj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<or>" 30) where
    98   "disj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
    99 
   100 definition
   101   Ex :: "('a \<Rightarrow> o) \<Rightarrow> o"  (binder "\<exists>" 10) where
   102   "\<exists>x. P x \<equiv> \<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
   103 
   104 abbreviation
   105   not_equal :: "'a \<Rightarrow> 'a \<Rightarrow> o"  (infixl "\<noteq>" 50) where
   106   "x \<noteq> y \<equiv> \<not> (x = y)"
   107 
   108 theorem falseE [elim]: "\<bottom> \<Longrightarrow> A"
   109 proof (unfold false_def)
   110   assume "\<forall>A. A"
   111   then show A ..
   112 qed
   113 
   114 theorem trueI [intro]: \<top>
   115 proof (unfold true_def)
   116   show "\<bottom> \<longrightarrow> \<bottom>" ..
   117 qed
   118 
   119 theorem notI [intro]: "(A \<Longrightarrow> \<bottom>) \<Longrightarrow> \<not> A"
   120 proof (unfold not_def)
   121   assume "A \<Longrightarrow> \<bottom>"
   122   then show "A \<longrightarrow> \<bottom>" ..
   123 qed
   124 
   125 theorem notE [elim]: "\<not> A \<Longrightarrow> A \<Longrightarrow> B"
   126 proof (unfold not_def)
   127   assume "A \<longrightarrow> \<bottom>"
   128   also assume A
   129   finally have \<bottom> ..
   130   then show B ..
   131 qed
   132 
   133 lemma notE': "A \<Longrightarrow> \<not> A \<Longrightarrow> B"
   134   by (rule notE)
   135 
   136 lemmas contradiction = notE notE'  -- {* proof by contradiction in any order *}
   137 
   138 theorem conjI [intro]: "A \<Longrightarrow> B \<Longrightarrow> A \<and> B"
   139 proof (unfold conj_def)
   140   assume A and B
   141   show "\<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
   142   proof
   143     fix C show "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
   144     proof
   145       assume "A \<longrightarrow> B \<longrightarrow> C"
   146       also note `A`
   147       also note `B`
   148       finally show C .
   149     qed
   150   qed
   151 qed
   152 
   153 theorem conjE [elim]: "A \<and> B \<Longrightarrow> (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C"
   154 proof (unfold conj_def)
   155   assume c: "\<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
   156   assume "A \<Longrightarrow> B \<Longrightarrow> C"
   157   moreover {
   158     from c have "(A \<longrightarrow> B \<longrightarrow> A) \<longrightarrow> A" ..
   159     also have "A \<longrightarrow> B \<longrightarrow> A"
   160     proof
   161       assume A
   162       then show "B \<longrightarrow> A" ..
   163     qed
   164     finally have A .
   165   } moreover {
   166     from c have "(A \<longrightarrow> B \<longrightarrow> B) \<longrightarrow> B" ..
   167     also have "A \<longrightarrow> B \<longrightarrow> B"
   168     proof
   169       show "B \<longrightarrow> B" ..
   170     qed
   171     finally have B .
   172   } ultimately show C .
   173 qed
   174 
   175 theorem disjI1 [intro]: "A \<Longrightarrow> A \<or> B"
   176 proof (unfold disj_def)
   177   assume A
   178   show "\<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
   179   proof
   180     fix C show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
   181     proof
   182       assume "A \<longrightarrow> C"
   183       also note `A`
   184       finally have C .
   185       then show "(B \<longrightarrow> C) \<longrightarrow> C" ..
   186     qed
   187   qed
   188 qed
   189 
   190 theorem disjI2 [intro]: "B \<Longrightarrow> A \<or> B"
   191 proof (unfold disj_def)
   192   assume B
   193   show "\<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
   194   proof
   195     fix C show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
   196     proof
   197       show "(B \<longrightarrow> C) \<longrightarrow> C"
   198       proof
   199         assume "B \<longrightarrow> C"
   200         also note `B`
   201         finally show C .
   202       qed
   203     qed
   204   qed
   205 qed
   206 
   207 theorem disjE [elim]: "A \<or> B \<Longrightarrow> (A \<Longrightarrow> C) \<Longrightarrow> (B \<Longrightarrow> C) \<Longrightarrow> C"
   208 proof (unfold disj_def)
   209   assume c: "\<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
   210   assume r1: "A \<Longrightarrow> C" and r2: "B \<Longrightarrow> C"
   211   from c have "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C" ..
   212   also have "A \<longrightarrow> C"
   213   proof
   214     assume A then show C by (rule r1)
   215   qed
   216   also have "B \<longrightarrow> C"
   217   proof
   218     assume B then show C by (rule r2)
   219   qed
   220   finally show C .
   221 qed
   222 
   223 theorem exI [intro]: "P a \<Longrightarrow> \<exists>x. P x"
   224 proof (unfold Ex_def)
   225   assume "P a"
   226   show "\<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
   227   proof
   228     fix C show "(\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
   229     proof
   230       assume "\<forall>x. P x \<longrightarrow> C"
   231       then have "P a \<longrightarrow> C" ..
   232       also note `P a`
   233       finally show C .
   234     qed
   235   qed
   236 qed
   237 
   238 theorem exE [elim]: "\<exists>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> C) \<Longrightarrow> C"
   239 proof (unfold Ex_def)
   240   assume c: "\<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
   241   assume r: "\<And>x. P x \<Longrightarrow> C"
   242   from c have "(\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C" ..
   243   also have "\<forall>x. P x \<longrightarrow> C"
   244   proof
   245     fix x show "P x \<longrightarrow> C"
   246     proof
   247       assume "P x"
   248       then show C by (rule r)
   249     qed
   250   qed
   251   finally show C .
   252 qed
   253 
   254 
   255 subsection {* Classical logic *}
   256 
   257 locale classical =
   258   assumes classical: "(\<not> A \<Longrightarrow> A) \<Longrightarrow> A"
   259 
   260 theorem (in classical)
   261   Peirce's_Law: "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"
   262 proof
   263   assume a: "(A \<longrightarrow> B) \<longrightarrow> A"
   264   show A
   265   proof (rule classical)
   266     assume "\<not> A"
   267     have "A \<longrightarrow> B"
   268     proof
   269       assume A
   270       with `\<not> A` show B by (rule contradiction)
   271     qed
   272     with a show A ..
   273   qed
   274 qed
   275 
   276 theorem (in classical)
   277   double_negation: "\<not> \<not> A \<Longrightarrow> A"
   278 proof -
   279   assume "\<not> \<not> A"
   280   show A
   281   proof (rule classical)
   282     assume "\<not> A"
   283     with `\<not> \<not> A` show ?thesis by (rule contradiction)
   284   qed
   285 qed
   286 
   287 theorem (in classical)
   288   tertium_non_datur: "A \<or> \<not> A"
   289 proof (rule double_negation)
   290   show "\<not> \<not> (A \<or> \<not> A)"
   291   proof
   292     assume "\<not> (A \<or> \<not> A)"
   293     have "\<not> A"
   294     proof
   295       assume A then have "A \<or> \<not> A" ..
   296       with `\<not> (A \<or> \<not> A)` show \<bottom> by (rule contradiction)
   297     qed
   298     then have "A \<or> \<not> A" ..
   299     with `\<not> (A \<or> \<not> A)` show \<bottom> by (rule contradiction)
   300   qed
   301 qed
   302 
   303 theorem (in classical)
   304   classical_cases: "(A \<Longrightarrow> C) \<Longrightarrow> (\<not> A \<Longrightarrow> C) \<Longrightarrow> C"
   305 proof -
   306   assume r1: "A \<Longrightarrow> C" and r2: "\<not> A \<Longrightarrow> C"
   307   from tertium_non_datur show C
   308   proof
   309     assume A
   310     then show ?thesis by (rule r1)
   311   next
   312     assume "\<not> A"
   313     then show ?thesis by (rule r2)
   314   qed
   315 qed
   316 
   317 lemma (in classical) "(\<not> A \<Longrightarrow> A) \<Longrightarrow> A"  (* FIXME *)
   318 proof -
   319   assume r: "\<not> A \<Longrightarrow> A"
   320   show A
   321   proof (rule classical_cases)
   322     assume A then show A .
   323   next
   324     assume "\<not> A" then show A by (rule r)
   325   qed
   326 qed
   327 
   328 end