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