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