src/HOL/ex/Higher_Order_Logic.thy
author wenzelm
Tue Jul 17 13:19:17 2007 +0200 (2007-07-17)
changeset 23822 bfb3b1e1d766
parent 23373 ead82c82da9e
child 26957 e3f04fdd994d
permissions -rw-r--r--
tuned specifications;
     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 axiomatization
    37   imp :: "o \<Rightarrow> o \<Rightarrow> o"    (infixr "\<longrightarrow>" 25) and
    38   All :: "('a \<Rightarrow> o) \<Rightarrow> o"    (binder "\<forall>" 10)
    39 where
    40   impI [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B" and
    41   impE [dest, trans]: "A \<longrightarrow> B \<Longrightarrow> A \<Longrightarrow> B" and
    42   allI [intro]: "(\<And>x. P x) \<Longrightarrow> \<forall>x. P x" and
    43   allE [dest]: "\<forall>x. P x \<Longrightarrow> P a"
    44 
    45 
    46 subsubsection {* Extensional equality *}
    47 
    48 axiomatization
    49   equal :: "'a \<Rightarrow> 'a \<Rightarrow> o"   (infixl "=" 50)
    50 where
    51   refl [intro]: "x = x" and
    52   subst: "x = y \<Longrightarrow> P x \<Longrightarrow> P y"
    53 
    54 axiomatization where
    55   ext [intro]: "(\<And>x. f x = g x) \<Longrightarrow> f = g" and
    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   then show "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>") where
    84   "\<bottom> \<equiv> \<forall>A. A"
    85 
    86 definition
    87   true :: o  ("\<top>") where
    88   "\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>"
    89 
    90 definition
    91   not :: "o \<Rightarrow> o"  ("\<not> _" [40] 40) where
    92   "not \<equiv> \<lambda>A. A \<longrightarrow> \<bottom>"
    93 
    94 definition
    95   conj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<and>" 35) where
    96   "conj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
    97 
    98 definition
    99   disj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<or>" 30) where
   100   "disj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
   101 
   102 definition
   103   Ex :: "('a \<Rightarrow> o) \<Rightarrow> o"  (binder "\<exists>" 10) where
   104   "\<exists>x. P x \<equiv> \<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
   105 
   106 abbreviation
   107   not_equal :: "'a \<Rightarrow> 'a \<Rightarrow> o"  (infixl "\<noteq>" 50) where
   108   "x \<noteq> y \<equiv> \<not> (x = y)"
   109 
   110 theorem falseE [elim]: "\<bottom> \<Longrightarrow> A"
   111 proof (unfold false_def)
   112   assume "\<forall>A. A"
   113   then show A ..
   114 qed
   115 
   116 theorem trueI [intro]: \<top>
   117 proof (unfold true_def)
   118   show "\<bottom> \<longrightarrow> \<bottom>" ..
   119 qed
   120 
   121 theorem notI [intro]: "(A \<Longrightarrow> \<bottom>) \<Longrightarrow> \<not> A"
   122 proof (unfold not_def)
   123   assume "A \<Longrightarrow> \<bottom>"
   124   then show "A \<longrightarrow> \<bottom>" ..
   125 qed
   126 
   127 theorem notE [elim]: "\<not> A \<Longrightarrow> A \<Longrightarrow> B"
   128 proof (unfold not_def)
   129   assume "A \<longrightarrow> \<bottom>"
   130   also assume A
   131   finally have \<bottom> ..
   132   then show B ..
   133 qed
   134 
   135 lemma notE': "A \<Longrightarrow> \<not> A \<Longrightarrow> B"
   136   by (rule notE)
   137 
   138 lemmas contradiction = notE notE'  -- {* proof by contradiction in any order *}
   139 
   140 theorem conjI [intro]: "A \<Longrightarrow> B \<Longrightarrow> A \<and> B"
   141 proof (unfold conj_def)
   142   assume A and B
   143   show "\<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
   144   proof
   145     fix C show "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
   146     proof
   147       assume "A \<longrightarrow> B \<longrightarrow> C"
   148       also note `A`
   149       also note `B`
   150       finally show C .
   151     qed
   152   qed
   153 qed
   154 
   155 theorem conjE [elim]: "A \<and> B \<Longrightarrow> (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C"
   156 proof (unfold conj_def)
   157   assume c: "\<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
   158   assume "A \<Longrightarrow> B \<Longrightarrow> C"
   159   moreover {
   160     from c have "(A \<longrightarrow> B \<longrightarrow> A) \<longrightarrow> A" ..
   161     also have "A \<longrightarrow> B \<longrightarrow> A"
   162     proof
   163       assume A
   164       then show "B \<longrightarrow> A" ..
   165     qed
   166     finally have A .
   167   } moreover {
   168     from c have "(A \<longrightarrow> B \<longrightarrow> B) \<longrightarrow> B" ..
   169     also have "A \<longrightarrow> B \<longrightarrow> B"
   170     proof
   171       show "B \<longrightarrow> B" ..
   172     qed
   173     finally have B .
   174   } ultimately show C .
   175 qed
   176 
   177 theorem disjI1 [intro]: "A \<Longrightarrow> A \<or> B"
   178 proof (unfold disj_def)
   179   assume A
   180   show "\<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
   181   proof
   182     fix C show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
   183     proof
   184       assume "A \<longrightarrow> C"
   185       also note `A`
   186       finally have C .
   187       then show "(B \<longrightarrow> C) \<longrightarrow> C" ..
   188     qed
   189   qed
   190 qed
   191 
   192 theorem disjI2 [intro]: "B \<Longrightarrow> A \<or> B"
   193 proof (unfold disj_def)
   194   assume B
   195   show "\<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
   196   proof
   197     fix C show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
   198     proof
   199       show "(B \<longrightarrow> C) \<longrightarrow> C"
   200       proof
   201         assume "B \<longrightarrow> C"
   202         also note `B`
   203         finally show C .
   204       qed
   205     qed
   206   qed
   207 qed
   208 
   209 theorem disjE [elim]: "A \<or> B \<Longrightarrow> (A \<Longrightarrow> C) \<Longrightarrow> (B \<Longrightarrow> C) \<Longrightarrow> C"
   210 proof (unfold disj_def)
   211   assume c: "\<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
   212   assume r1: "A \<Longrightarrow> C" and r2: "B \<Longrightarrow> C"
   213   from c have "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C" ..
   214   also have "A \<longrightarrow> C"
   215   proof
   216     assume A then show C by (rule r1)
   217   qed
   218   also have "B \<longrightarrow> C"
   219   proof
   220     assume B then show C by (rule r2)
   221   qed
   222   finally show C .
   223 qed
   224 
   225 theorem exI [intro]: "P a \<Longrightarrow> \<exists>x. P x"
   226 proof (unfold Ex_def)
   227   assume "P a"
   228   show "\<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
   229   proof
   230     fix C show "(\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
   231     proof
   232       assume "\<forall>x. P x \<longrightarrow> C"
   233       then have "P a \<longrightarrow> C" ..
   234       also note `P a`
   235       finally show C .
   236     qed
   237   qed
   238 qed
   239 
   240 theorem exE [elim]: "\<exists>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> C) \<Longrightarrow> C"
   241 proof (unfold Ex_def)
   242   assume c: "\<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
   243   assume r: "\<And>x. P x \<Longrightarrow> C"
   244   from c have "(\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C" ..
   245   also have "\<forall>x. P x \<longrightarrow> C"
   246   proof
   247     fix x show "P x \<longrightarrow> C"
   248     proof
   249       assume "P x"
   250       then show C by (rule r)
   251     qed
   252   qed
   253   finally show C .
   254 qed
   255 
   256 
   257 subsection {* Classical logic *}
   258 
   259 locale classical =
   260   assumes classical: "(\<not> A \<Longrightarrow> A) \<Longrightarrow> A"
   261 
   262 theorem (in classical)
   263   Peirce's_Law: "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"
   264 proof
   265   assume a: "(A \<longrightarrow> B) \<longrightarrow> A"
   266   show A
   267   proof (rule classical)
   268     assume "\<not> A"
   269     have "A \<longrightarrow> B"
   270     proof
   271       assume A
   272       with `\<not> A` show B by (rule contradiction)
   273     qed
   274     with a show A ..
   275   qed
   276 qed
   277 
   278 theorem (in classical)
   279   double_negation: "\<not> \<not> A \<Longrightarrow> A"
   280 proof -
   281   assume "\<not> \<not> A"
   282   show A
   283   proof (rule classical)
   284     assume "\<not> A"
   285     with `\<not> \<not> A` show ?thesis by (rule contradiction)
   286   qed
   287 qed
   288 
   289 theorem (in classical)
   290   tertium_non_datur: "A \<or> \<not> A"
   291 proof (rule double_negation)
   292   show "\<not> \<not> (A \<or> \<not> A)"
   293   proof
   294     assume "\<not> (A \<or> \<not> A)"
   295     have "\<not> A"
   296     proof
   297       assume A then have "A \<or> \<not> A" ..
   298       with `\<not> (A \<or> \<not> A)` show \<bottom> by (rule contradiction)
   299     qed
   300     then have "A \<or> \<not> A" ..
   301     with `\<not> (A \<or> \<not> A)` show \<bottom> by (rule contradiction)
   302   qed
   303 qed
   304 
   305 theorem (in classical)
   306   classical_cases: "(A \<Longrightarrow> C) \<Longrightarrow> (\<not> A \<Longrightarrow> C) \<Longrightarrow> C"
   307 proof -
   308   assume r1: "A \<Longrightarrow> C" and r2: "\<not> A \<Longrightarrow> C"
   309   from tertium_non_datur show C
   310   proof
   311     assume A
   312     then show ?thesis by (rule r1)
   313   next
   314     assume "\<not> A"
   315     then show ?thesis by (rule r2)
   316   qed
   317 qed
   318 
   319 lemma (in classical) "(\<not> A \<Longrightarrow> A) \<Longrightarrow> A"  (* FIXME *)
   320 proof -
   321   assume r: "\<not> A \<Longrightarrow> A"
   322   show A
   323   proof (rule classical_cases)
   324     assume A then show A .
   325   next
   326     assume "\<not> A" then show A by (rule r)
   327   qed
   328 qed
   329 
   330 end