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