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