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