src/HOL/ex/Higher_Order_Logic.thy
author krauss
Wed Sep 13 12:05:50 2006 +0200 (2006-09-13)
changeset 20523 36a59e5d0039
parent 19736 d8d0f8f51d69
child 21404 eb85850d3eb7
permissions -rw-r--r--
Major update to function package, including new syntax and the (only theoretical)
ability to handle local contexts.
     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 imports CPure begin
     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 definition
    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 abbreviation
    97   not_equal :: "'a \<Rightarrow> 'a \<Rightarrow> o"    (infixl "\<noteq>" 50)
    98   "x \<noteq> y \<equiv> \<not> (x = y)"
    99 
   100 theorem falseE [elim]: "\<bottom> \<Longrightarrow> A"
   101 proof (unfold false_def)
   102   assume "\<forall>A. A"
   103   thus A ..
   104 qed
   105 
   106 theorem trueI [intro]: \<top>
   107 proof (unfold true_def)
   108   show "\<bottom> \<longrightarrow> \<bottom>" ..
   109 qed
   110 
   111 theorem notI [intro]: "(A \<Longrightarrow> \<bottom>) \<Longrightarrow> \<not> A"
   112 proof (unfold not_def)
   113   assume "A \<Longrightarrow> \<bottom>"
   114   thus "A \<longrightarrow> \<bottom>" ..
   115 qed
   116 
   117 theorem notE [elim]: "\<not> A \<Longrightarrow> A \<Longrightarrow> B"
   118 proof (unfold not_def)
   119   assume "A \<longrightarrow> \<bottom>"
   120   also assume A
   121   finally have \<bottom> ..
   122   thus B ..
   123 qed
   124 
   125 lemma notE': "A \<Longrightarrow> \<not> A \<Longrightarrow> B"
   126   by (rule notE)
   127 
   128 lemmas contradiction = notE notE'  -- {* proof by contradiction in any order *}
   129 
   130 theorem conjI [intro]: "A \<Longrightarrow> B \<Longrightarrow> A \<and> B"
   131 proof (unfold conj_def)
   132   assume A and B
   133   show "\<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
   134   proof
   135     fix C show "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
   136     proof
   137       assume "A \<longrightarrow> B \<longrightarrow> C"
   138       also have A .
   139       also have B .
   140       finally show C .
   141     qed
   142   qed
   143 qed
   144 
   145 theorem conjE [elim]: "A \<and> B \<Longrightarrow> (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C"
   146 proof (unfold conj_def)
   147   assume c: "\<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
   148   assume "A \<Longrightarrow> B \<Longrightarrow> C"
   149   moreover {
   150     from c have "(A \<longrightarrow> B \<longrightarrow> A) \<longrightarrow> A" ..
   151     also have "A \<longrightarrow> B \<longrightarrow> A"
   152     proof
   153       assume A
   154       thus "B \<longrightarrow> A" ..
   155     qed
   156     finally have A .
   157   } moreover {
   158     from c have "(A \<longrightarrow> B \<longrightarrow> B) \<longrightarrow> B" ..
   159     also have "A \<longrightarrow> B \<longrightarrow> B"
   160     proof
   161       show "B \<longrightarrow> B" ..
   162     qed
   163     finally have B .
   164   } ultimately show C .
   165 qed
   166 
   167 theorem disjI1 [intro]: "A \<Longrightarrow> A \<or> B"
   168 proof (unfold disj_def)
   169   assume A
   170   show "\<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
   171   proof
   172     fix C show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
   173     proof
   174       assume "A \<longrightarrow> C"
   175       also have A .
   176       finally have C .
   177       thus "(B \<longrightarrow> C) \<longrightarrow> C" ..
   178     qed
   179   qed
   180 qed
   181 
   182 theorem disjI2 [intro]: "B \<Longrightarrow> A \<or> B"
   183 proof (unfold disj_def)
   184   assume B
   185   show "\<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
   186   proof
   187     fix C show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
   188     proof
   189       show "(B \<longrightarrow> C) \<longrightarrow> C"
   190       proof
   191         assume "B \<longrightarrow> C"
   192         also have B .
   193         finally show C .
   194       qed
   195     qed
   196   qed
   197 qed
   198 
   199 theorem disjE [elim]: "A \<or> B \<Longrightarrow> (A \<Longrightarrow> C) \<Longrightarrow> (B \<Longrightarrow> C) \<Longrightarrow> C"
   200 proof (unfold disj_def)
   201   assume c: "\<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
   202   assume r1: "A \<Longrightarrow> C" and r2: "B \<Longrightarrow> C"
   203   from c have "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C" ..
   204   also have "A \<longrightarrow> C"
   205   proof
   206     assume A thus C by (rule r1)
   207   qed
   208   also have "B \<longrightarrow> C"
   209   proof
   210     assume B thus C by (rule r2)
   211   qed
   212   finally show C .
   213 qed
   214 
   215 theorem exI [intro]: "P a \<Longrightarrow> \<exists>x. P x"
   216 proof (unfold Ex_def)
   217   assume "P a"
   218   show "\<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
   219   proof
   220     fix C show "(\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
   221     proof
   222       assume "\<forall>x. P x \<longrightarrow> C"
   223       hence "P a \<longrightarrow> C" ..
   224       also have "P a" .
   225       finally show C .
   226     qed
   227   qed
   228 qed
   229 
   230 theorem exE [elim]: "\<exists>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> C) \<Longrightarrow> C"
   231 proof (unfold Ex_def)
   232   assume c: "\<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
   233   assume r: "\<And>x. P x \<Longrightarrow> C"
   234   from c have "(\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C" ..
   235   also have "\<forall>x. P x \<longrightarrow> C"
   236   proof
   237     fix x show "P x \<longrightarrow> C"
   238     proof
   239       assume "P x"
   240       thus C by (rule r)
   241     qed
   242   qed
   243   finally show C .
   244 qed
   245 
   246 
   247 subsection {* Classical logic *}
   248 
   249 locale classical =
   250   assumes classical: "(\<not> A \<Longrightarrow> A) \<Longrightarrow> A"
   251 
   252 theorem (in classical)
   253   Peirce's_Law: "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"
   254 proof
   255   assume a: "(A \<longrightarrow> B) \<longrightarrow> A"
   256   show A
   257   proof (rule classical)
   258     assume "\<not> A"
   259     have "A \<longrightarrow> B"
   260     proof
   261       assume A
   262       thus B by (rule contradiction)
   263     qed
   264     with a show A ..
   265   qed
   266 qed
   267 
   268 theorem (in classical)
   269   double_negation: "\<not> \<not> A \<Longrightarrow> A"
   270 proof -
   271   assume "\<not> \<not> A"
   272   show A
   273   proof (rule classical)
   274     assume "\<not> A"
   275     thus ?thesis by (rule contradiction)
   276   qed
   277 qed
   278 
   279 theorem (in classical)
   280   tertium_non_datur: "A \<or> \<not> A"
   281 proof (rule double_negation)
   282   show "\<not> \<not> (A \<or> \<not> A)"
   283   proof
   284     assume "\<not> (A \<or> \<not> A)"
   285     have "\<not> A"
   286     proof
   287       assume A hence "A \<or> \<not> A" ..
   288       thus \<bottom> by (rule contradiction)
   289     qed
   290     hence "A \<or> \<not> A" ..
   291     thus \<bottom> by (rule contradiction)
   292   qed
   293 qed
   294 
   295 theorem (in classical)
   296   classical_cases: "(A \<Longrightarrow> C) \<Longrightarrow> (\<not> A \<Longrightarrow> C) \<Longrightarrow> C"
   297 proof -
   298   assume r1: "A \<Longrightarrow> C" and r2: "\<not> A \<Longrightarrow> C"
   299   from tertium_non_datur show C
   300   proof
   301     assume A
   302     thus ?thesis by (rule r1)
   303   next
   304     assume "\<not> A"
   305     thus ?thesis by (rule r2)
   306   qed
   307 qed
   308 
   309 lemma (in classical) "(\<not> A \<Longrightarrow> A) \<Longrightarrow> A"  (* FIXME *)
   310 proof -
   311   assume r: "\<not> A \<Longrightarrow> A"
   312   show A
   313   proof (rule classical_cases)
   314     assume A thus A .
   315   next
   316     assume "\<not> A" thus A by (rule r)
   317   qed
   318 qed
   319 
   320 end