src/HOL/ex/Higher_Order_Logic.thy
author wenzelm
Mon Aug 31 21:28:08 2015 +0200 (2015-08-31)
changeset 61070 b72a990adfe2
parent 60769 cf7f3465eaf1
child 61759 49353865e539
permissions -rw-r--r--
prefer symbols;
     1 (*  Title:      HOL/ex/Higher_Order_Logic.thy
     2     Author:     Gertrud Bauer and Markus Wenzel, TU Muenchen
     3 *)
     4 
     5 section \<open>Foundations of HOL\<close>
     6 
     7 theory Higher_Order_Logic
     8 imports Pure
     9 begin
    10 
    11 text \<open>
    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 \<close>
    19 
    20 
    21 subsection \<open>Pure Logic\<close>
    22 
    23 class type
    24 default_sort type
    25 
    26 typedecl o
    27 instance o :: type ..
    28 instance "fun" :: (type, type) type ..
    29 
    30 
    31 subsubsection \<open>Basic logical connectives\<close>
    32 
    33 judgment 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 \<open>Extensional equality\<close>
    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 \<open>Derived connectives\<close>
    80 
    81 definition false :: o  ("\<bottom>") where "\<bottom> \<equiv> \<forall>A. A"
    82 
    83 definition true :: o  ("\<top>") where "\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>"
    84 
    85 definition not :: "o \<Rightarrow> o"  ("\<not> _" [40] 40)
    86   where "not \<equiv> \<lambda>A. A \<longrightarrow> \<bottom>"
    87 
    88 definition conj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<and>" 35)
    89   where "conj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
    90 
    91 definition disj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<or>" 30)
    92   where "disj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
    93 
    94 definition Ex :: "('a \<Rightarrow> o) \<Rightarrow> o"  (binder "\<exists>" 10)
    95   where "\<exists>x. P x \<equiv> \<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
    96 
    97 abbreviation not_equal :: "'a \<Rightarrow> 'a \<Rightarrow> o"  (infixl "\<noteq>" 50)
    98   where "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   then show 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   then show "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>" and A
   120   then have \<bottom> ..
   121   then show B ..
   122 qed
   123 
   124 lemma notE': "A \<Longrightarrow> \<not> A \<Longrightarrow> B"
   125   by (rule notE)
   126 
   127 lemmas contradiction = notE notE'  -- \<open>proof by contradiction in any order\<close>
   128 
   129 theorem conjI [intro]: "A \<Longrightarrow> B \<Longrightarrow> A \<and> B"
   130 proof (unfold conj_def)
   131   assume A and B
   132   show "\<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
   133   proof
   134     fix C show "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
   135     proof
   136       assume "A \<longrightarrow> B \<longrightarrow> C"
   137       also note \<open>A\<close>
   138       also note \<open>B\<close>
   139       finally show C .
   140     qed
   141   qed
   142 qed
   143 
   144 theorem conjE [elim]: "A \<and> B \<Longrightarrow> (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C"
   145 proof (unfold conj_def)
   146   assume c: "\<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
   147   assume "A \<Longrightarrow> B \<Longrightarrow> C"
   148   moreover {
   149     from c have "(A \<longrightarrow> B \<longrightarrow> A) \<longrightarrow> A" ..
   150     also have "A \<longrightarrow> B \<longrightarrow> A"
   151     proof
   152       assume A
   153       then show "B \<longrightarrow> A" ..
   154     qed
   155     finally have A .
   156   } moreover {
   157     from c have "(A \<longrightarrow> B \<longrightarrow> B) \<longrightarrow> B" ..
   158     also have "A \<longrightarrow> B \<longrightarrow> B"
   159     proof
   160       show "B \<longrightarrow> B" ..
   161     qed
   162     finally have B .
   163   } ultimately show C .
   164 qed
   165 
   166 theorem disjI1 [intro]: "A \<Longrightarrow> A \<or> B"
   167 proof (unfold disj_def)
   168   assume A
   169   show "\<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
   170   proof
   171     fix C show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
   172     proof
   173       assume "A \<longrightarrow> C"
   174       also note \<open>A\<close>
   175       finally have C .
   176       then show "(B \<longrightarrow> C) \<longrightarrow> C" ..
   177     qed
   178   qed
   179 qed
   180 
   181 theorem disjI2 [intro]: "B \<Longrightarrow> A \<or> B"
   182 proof (unfold disj_def)
   183   assume B
   184   show "\<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
   185   proof
   186     fix C show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
   187     proof
   188       show "(B \<longrightarrow> C) \<longrightarrow> C"
   189       proof
   190         assume "B \<longrightarrow> C"
   191         also note \<open>B\<close>
   192         finally show C .
   193       qed
   194     qed
   195   qed
   196 qed
   197 
   198 theorem disjE [elim]: "A \<or> B \<Longrightarrow> (A \<Longrightarrow> C) \<Longrightarrow> (B \<Longrightarrow> C) \<Longrightarrow> C"
   199 proof (unfold disj_def)
   200   assume c: "\<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
   201   assume r1: "A \<Longrightarrow> C" and r2: "B \<Longrightarrow> C"
   202   from c have "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C" ..
   203   also have "A \<longrightarrow> C"
   204   proof
   205     assume A
   206     then show C by (rule r1)
   207   qed
   208   also have "B \<longrightarrow> C"
   209   proof
   210     assume B
   211     then show 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       then have "P a \<longrightarrow> C" ..
   225       also note \<open>P a\<close>
   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       then show C by (rule r)
   242     qed
   243   qed
   244   finally show C .
   245 qed
   246 
   247 
   248 subsection \<open>Classical logic\<close>
   249 
   250 locale classical =
   251   assumes classical: "(\<not> A \<Longrightarrow> A) \<Longrightarrow> A"
   252 
   253 theorem (in classical) 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       with \<open>\<not> A\<close> show B by (rule contradiction)
   263     qed
   264     with a show A ..
   265   qed
   266 qed
   267 
   268 theorem (in classical) double_negation: "\<not> \<not> A \<Longrightarrow> A"
   269 proof -
   270   assume "\<not> \<not> A"
   271   show A
   272   proof (rule classical)
   273     assume "\<not> A"
   274     with \<open>\<not> \<not> A\<close> show ?thesis by (rule contradiction)
   275   qed
   276 qed
   277 
   278 theorem (in classical) tertium_non_datur: "A \<or> \<not> A"
   279 proof (rule double_negation)
   280   show "\<not> \<not> (A \<or> \<not> A)"
   281   proof
   282     assume "\<not> (A \<or> \<not> A)"
   283     have "\<not> A"
   284     proof
   285       assume A then have "A \<or> \<not> A" ..
   286       with \<open>\<not> (A \<or> \<not> A)\<close> show \<bottom> by (rule contradiction)
   287     qed
   288     then have "A \<or> \<not> A" ..
   289     with \<open>\<not> (A \<or> \<not> A)\<close> show \<bottom> by (rule contradiction)
   290   qed
   291 qed
   292 
   293 theorem (in classical) classical_cases: "(A \<Longrightarrow> C) \<Longrightarrow> (\<not> A \<Longrightarrow> C) \<Longrightarrow> C"
   294 proof -
   295   assume r1: "A \<Longrightarrow> C" and r2: "\<not> A \<Longrightarrow> C"
   296   from tertium_non_datur show C
   297   proof
   298     assume A
   299     then show ?thesis by (rule r1)
   300   next
   301     assume "\<not> A"
   302     then show ?thesis by (rule r2)
   303   qed
   304 qed
   305 
   306 lemma (in classical) "(\<not> A \<Longrightarrow> A) \<Longrightarrow> A"  (* FIXME *)
   307 proof -
   308   assume r: "\<not> A \<Longrightarrow> A"
   309   show A
   310   proof (rule classical_cases)
   311     assume A then show A .
   312   next
   313     assume "\<not> A" then show A by (rule r)
   314   qed
   315 qed
   316 
   317 end