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