src/HOL/Isar_Examples/Basic_Logic.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 37671 fa53d267dab3
child 55640 abc140f21caa
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33026
8f35633c4922 modernized session Isar_Examples;
wenzelm
parents: 31758
diff changeset
     1
(*  Title:      HOL/Isar_Examples/Basic_Logic.thy
6444
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
     2
    Author:     Markus Wenzel, TU Muenchen
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
     3
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
     4
Basic propositional and quantifier reasoning.
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
     5
*)
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
     6
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
     7
header {* Basic logical reasoning *}
7748
5b9c45b21782 improved presentation;
wenzelm
parents: 7740
diff changeset
     8
31758
3edd5f813f01 observe standard theory naming conventions;
wenzelm
parents: 23393
diff changeset
     9
theory Basic_Logic
3edd5f813f01 observe standard theory naming conventions;
wenzelm
parents: 23393
diff changeset
    10
imports Main
3edd5f813f01 observe standard theory naming conventions;
wenzelm
parents: 23393
diff changeset
    11
begin
6444
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
    12
7761
7fab9592384f improved presentation;
wenzelm
parents: 7748
diff changeset
    13
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
    14
subsection {* Pure backward reasoning *}
7740
2fbe5ce9845f tuned comments;
wenzelm
parents: 7604
diff changeset
    15
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
    16
text {* In order to get a first idea of how Isabelle/Isar proof
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
    17
  documents may look like, we consider the propositions @{text I},
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
    18
  @{text K}, and @{text S}.  The following (rather explicit) proofs
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
    19
  should require little extra explanations. *}
7001
8121e11ed765 Deriving rules in Isabelle;
wenzelm
parents: 6892
diff changeset
    20
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
    21
lemma I: "A --> A"
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
    22
proof
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
    23
  assume A
23393
31781b2de73d tuned proofs: avoid implicit prems;
wenzelm
parents: 23373
diff changeset
    24
  show A by fact
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
    25
qed
6444
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
    26
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
    27
lemma K: "A --> B --> A"
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
    28
proof
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
    29
  assume A
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
    30
  show "B --> A"
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
    31
  proof
23393
31781b2de73d tuned proofs: avoid implicit prems;
wenzelm
parents: 23373
diff changeset
    32
    show A by fact
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
    33
  qed
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
    34
qed
6444
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
    35
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
    36
lemma S: "(A --> B --> C) --> (A --> B) --> A --> C"
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
    37
proof
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
    38
  assume "A --> B --> C"
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
    39
  show "(A --> B) --> A --> C"
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
    40
  proof
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
    41
    assume "A --> B"
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
    42
    show "A --> C"
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
    43
    proof
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
    44
      assume A
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
    45
      show C
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
    46
      proof (rule mp)
23393
31781b2de73d tuned proofs: avoid implicit prems;
wenzelm
parents: 23373
diff changeset
    47
        show "B --> C" by (rule mp) fact+
31781b2de73d tuned proofs: avoid implicit prems;
wenzelm
parents: 23373
diff changeset
    48
        show B by (rule mp) fact+
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
    49
      qed
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
    50
    qed
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
    51
  qed
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
    52
qed
6444
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
    53
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
    54
text {* Isar provides several ways to fine-tune the reasoning,
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
    55
  avoiding excessive detail.  Several abbreviated language elements
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
    56
  are available, enabling the writer to express proofs in a more
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
    57
  concise way, even without referring to any automated proof tools
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
    58
  yet.
7761
7fab9592384f improved presentation;
wenzelm
parents: 7748
diff changeset
    59
18193
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
    60
  First of all, proof by assumption may be abbreviated as a single
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
    61
  dot. *}
7820
cad7cc30fa40 more explanations;
wenzelm
parents: 7761
diff changeset
    62
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
    63
lemma "A --> A"
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
    64
proof
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
    65
  assume A
23393
31781b2de73d tuned proofs: avoid implicit prems;
wenzelm
parents: 23373
diff changeset
    66
  show A by fact+
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
    67
qed
7820
cad7cc30fa40 more explanations;
wenzelm
parents: 7761
diff changeset
    68
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
    69
text {* In fact, concluding any (sub-)proof already involves solving
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
    70
  any remaining goals by assumption\footnote{This is not a completely
18193
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
    71
  trivial operation, as proof by assumption may involve full
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
    72
  higher-order unification.}.  Thus we may skip the rather vacuous
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
    73
  body of the above proof as well. *}
7820
cad7cc30fa40 more explanations;
wenzelm
parents: 7761
diff changeset
    74
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
    75
lemma "A --> A"
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
    76
proof
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
    77
qed
7820
cad7cc30fa40 more explanations;
wenzelm
parents: 7761
diff changeset
    78
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
    79
text {* Note that the \isacommand{proof} command refers to the @{text
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
    80
  rule} method (without arguments) by default.  Thus it implicitly
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
    81
  applies a single rule, as determined from the syntactic form of the
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
    82
  statements involved.  The \isacommand{by} command abbreviates any
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
    83
  proof with empty body, so the proof may be further pruned. *}
7820
cad7cc30fa40 more explanations;
wenzelm
parents: 7761
diff changeset
    84
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
    85
lemma "A --> A"
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
    86
  by rule
7820
cad7cc30fa40 more explanations;
wenzelm
parents: 7761
diff changeset
    87
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
    88
text {* Proof by a single rule may be abbreviated as double-dot. *}
7820
cad7cc30fa40 more explanations;
wenzelm
parents: 7761
diff changeset
    89
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
    90
lemma "A --> A" ..
7820
cad7cc30fa40 more explanations;
wenzelm
parents: 7761
diff changeset
    91
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
    92
text {* Thus we have arrived at an adequate representation of the
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
    93
  proof of a tautology that holds by a single standard
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
    94
  rule.\footnote{Apparently, the rule here is implication
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
    95
  introduction.} *}
7820
cad7cc30fa40 more explanations;
wenzelm
parents: 7761
diff changeset
    96
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
    97
text {* Let us also reconsider @{text K}.  Its statement is composed
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
    98
  of iterated connectives.  Basic decomposition is by a single rule at
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
    99
  a time, which is why our first version above was by nesting two
18193
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
   100
  proofs.
7820
cad7cc30fa40 more explanations;
wenzelm
parents: 7761
diff changeset
   101
18193
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
   102
  The @{text intro} proof method repeatedly decomposes a goal's
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
   103
  conclusion.\footnote{The dual method is @{text elim}, acting on a
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   104
  goal's premises.} *}
7820
cad7cc30fa40 more explanations;
wenzelm
parents: 7761
diff changeset
   105
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   106
lemma "A --> B --> A"
12387
fe2353a8d1e8 fixed intro steps;
wenzelm
parents: 10636
diff changeset
   107
proof (intro impI)
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   108
  assume A
23393
31781b2de73d tuned proofs: avoid implicit prems;
wenzelm
parents: 23373
diff changeset
   109
  show A by fact
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   110
qed
7820
cad7cc30fa40 more explanations;
wenzelm
parents: 7761
diff changeset
   111
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   112
text {* Again, the body may be collapsed. *}
7820
cad7cc30fa40 more explanations;
wenzelm
parents: 7761
diff changeset
   113
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   114
lemma "A --> B --> A"
12387
fe2353a8d1e8 fixed intro steps;
wenzelm
parents: 10636
diff changeset
   115
  by (intro impI)
7820
cad7cc30fa40 more explanations;
wenzelm
parents: 7761
diff changeset
   116
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   117
text {* Just like @{text rule}, the @{text intro} and @{text elim}
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   118
  proof methods pick standard structural rules, in case no explicit
18193
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
   119
  arguments are given.  While implicit rules are usually just fine for
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
   120
  single rule application, this may go too far with iteration.  Thus
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
   121
  in practice, @{text intro} and @{text elim} would be typically
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
   122
  restricted to certain structures by giving a few rules only, e.g.\
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
   123
  \isacommand{proof}~@{text "(intro impI allI)"} to strip implications
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
   124
  and universal quantifiers.
7820
cad7cc30fa40 more explanations;
wenzelm
parents: 7761
diff changeset
   125
18193
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
   126
  Such well-tuned iterated decomposition of certain structures is the
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
   127
  prime application of @{text intro} and @{text elim}.  In contrast,
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
   128
  terminal steps that solve a goal completely are usually performed by
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
   129
  actual automated proof methods (such as \isacommand{by}~@{text
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   130
  blast}. *}
7820
cad7cc30fa40 more explanations;
wenzelm
parents: 7761
diff changeset
   131
cad7cc30fa40 more explanations;
wenzelm
parents: 7761
diff changeset
   132
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   133
subsection {* Variations of backward vs.\ forward reasoning *}
7820
cad7cc30fa40 more explanations;
wenzelm
parents: 7761
diff changeset
   134
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   135
text {* Certainly, any proof may be performed in backward-style only.
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   136
  On the other hand, small steps of reasoning are often more naturally
18193
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
   137
  expressed in forward-style.  Isar supports both backward and forward
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
   138
  reasoning as a first-class concept.  In order to demonstrate the
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
   139
  difference, we consider several proofs of @{text "A \<and> B \<longrightarrow> B \<and> A"}.
7820
cad7cc30fa40 more explanations;
wenzelm
parents: 7761
diff changeset
   140
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   141
  The first version is purely backward. *}
7001
8121e11ed765 Deriving rules in Isabelle;
wenzelm
parents: 6892
diff changeset
   142
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   143
lemma "A & B --> B & A"
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   144
proof
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   145
  assume "A & B"
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   146
  show "B & A"
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   147
  proof
23393
31781b2de73d tuned proofs: avoid implicit prems;
wenzelm
parents: 23373
diff changeset
   148
    show B by (rule conjunct2) fact
31781b2de73d tuned proofs: avoid implicit prems;
wenzelm
parents: 23373
diff changeset
   149
    show A by (rule conjunct1) fact
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   150
  qed
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   151
qed
6444
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
   152
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   153
text {* Above, the @{text "conjunct_1/2"} projection rules had to be
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   154
  named explicitly, since the goals @{text B} and @{text A} did not
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   155
  provide any structural clue.  This may be avoided using
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   156
  \isacommand{from} to focus on the @{text "A \<and> B"} assumption as the
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   157
  current facts, enabling the use of double-dot proofs.  Note that
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   158
  \isacommand{from} already does forward-chaining, involving the
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   159
  @{text conjE} rule here. *}
6444
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
   160
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   161
lemma "A & B --> B & A"
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   162
proof
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   163
  assume "A & B"
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   164
  show "B & A"
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   165
  proof
23373
ead82c82da9e tuned proofs: avoid implicit prems;
wenzelm
parents: 18193
diff changeset
   166
    from `A & B` show B ..
ead82c82da9e tuned proofs: avoid implicit prems;
wenzelm
parents: 18193
diff changeset
   167
    from `A & B` show A ..
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   168
  qed
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   169
qed
7604
wenzelm
parents: 7480
diff changeset
   170
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   171
text {* In the next version, we move the forward step one level
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   172
  upwards.  Forward-chaining from the most recent facts is indicated
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   173
  by the \isacommand{then} command.  Thus the proof of @{text "B \<and> A"}
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   174
  from @{text "A \<and> B"} actually becomes an elimination, rather than an
18193
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
   175
  introduction.  The resulting proof structure directly corresponds to
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
   176
  that of the @{text conjE} rule, including the repeated goal
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   177
  proposition that is abbreviated as @{text ?thesis} below. *}
7820
cad7cc30fa40 more explanations;
wenzelm
parents: 7761
diff changeset
   178
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   179
lemma "A & B --> B & A"
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   180
proof
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   181
  assume "A & B"
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   182
  then show "B & A"
18193
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
   183
  proof                    -- {* rule @{text conjE} of @{text "A \<and> B"} *}
23373
ead82c82da9e tuned proofs: avoid implicit prems;
wenzelm
parents: 18193
diff changeset
   184
    assume B A
ead82c82da9e tuned proofs: avoid implicit prems;
wenzelm
parents: 18193
diff changeset
   185
    then show ?thesis ..   -- {* rule @{text conjI} of @{text "B \<and> A"} *}
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   186
  qed
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   187
qed
7820
cad7cc30fa40 more explanations;
wenzelm
parents: 7761
diff changeset
   188
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   189
text {* In the subsequent version we flatten the structure of the main
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   190
  body by doing forward reasoning all the time.  Only the outermost
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   191
  decomposition step is left as backward. *}
7820
cad7cc30fa40 more explanations;
wenzelm
parents: 7761
diff changeset
   192
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   193
lemma "A & B --> B & A"
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   194
proof
23373
ead82c82da9e tuned proofs: avoid implicit prems;
wenzelm
parents: 18193
diff changeset
   195
  assume "A & B"
ead82c82da9e tuned proofs: avoid implicit prems;
wenzelm
parents: 18193
diff changeset
   196
  from `A & B` have A ..
ead82c82da9e tuned proofs: avoid implicit prems;
wenzelm
parents: 18193
diff changeset
   197
  from `A & B` have B ..
ead82c82da9e tuned proofs: avoid implicit prems;
wenzelm
parents: 18193
diff changeset
   198
  from `B` `A` show "B & A" ..
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   199
qed
6444
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
   200
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   201
text {* We can still push forward-reasoning a bit further, even at the
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   202
  risk of getting ridiculous.  Note that we force the initial proof
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   203
  step to do nothing here, by referring to the ``-'' proof method. *}
7820
cad7cc30fa40 more explanations;
wenzelm
parents: 7761
diff changeset
   204
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   205
lemma "A & B --> B & A"
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   206
proof -
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   207
  {
23373
ead82c82da9e tuned proofs: avoid implicit prems;
wenzelm
parents: 18193
diff changeset
   208
    assume "A & B"
ead82c82da9e tuned proofs: avoid implicit prems;
wenzelm
parents: 18193
diff changeset
   209
    from `A & B` have A ..
ead82c82da9e tuned proofs: avoid implicit prems;
wenzelm
parents: 18193
diff changeset
   210
    from `A & B` have B ..
ead82c82da9e tuned proofs: avoid implicit prems;
wenzelm
parents: 18193
diff changeset
   211
    from `B` `A` have "B & A" ..
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   212
  }
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   213
  then show ?thesis ..         -- {* rule @{text impI} *}
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   214
qed
7820
cad7cc30fa40 more explanations;
wenzelm
parents: 7761
diff changeset
   215
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   216
text {* \medskip With these examples we have shifted through a whole
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   217
  range from purely backward to purely forward reasoning.  Apparently,
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   218
  in the extreme ends we get slightly ill-structured proofs, which
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   219
  also require much explicit naming of either rules (backward) or
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   220
  local facts (forward).
7820
cad7cc30fa40 more explanations;
wenzelm
parents: 7761
diff changeset
   221
18193
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
   222
  The general lesson learned here is that good proof style would
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
   223
  achieve just the \emph{right} balance of top-down backward
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
   224
  decomposition, and bottom-up forward composition.  In general, there
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
   225
  is no single best way to arrange some pieces of formal reasoning, of
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
   226
  course.  Depending on the actual applications, the intended audience
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
   227
  etc., rules (and methods) on the one hand vs.\ facts on the other
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
   228
  hand have to be emphasized in an appropriate way.  This requires the
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   229
  proof writer to develop good taste, and some practice, of course. *}
7820
cad7cc30fa40 more explanations;
wenzelm
parents: 7761
diff changeset
   230
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   231
text {* For our example the most appropriate way of reasoning is
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   232
  probably the middle one, with conjunction introduction done after
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   233
  elimination. *}
7820
cad7cc30fa40 more explanations;
wenzelm
parents: 7761
diff changeset
   234
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   235
lemma "A & B --> B & A"
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   236
proof
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   237
  assume "A & B"
23373
ead82c82da9e tuned proofs: avoid implicit prems;
wenzelm
parents: 18193
diff changeset
   238
  then show "B & A"
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   239
  proof
23373
ead82c82da9e tuned proofs: avoid implicit prems;
wenzelm
parents: 18193
diff changeset
   240
    assume B A
ead82c82da9e tuned proofs: avoid implicit prems;
wenzelm
parents: 18193
diff changeset
   241
    then show ?thesis ..
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   242
  qed
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   243
qed
7820
cad7cc30fa40 more explanations;
wenzelm
parents: 7761
diff changeset
   244
cad7cc30fa40 more explanations;
wenzelm
parents: 7761
diff changeset
   245
6444
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
   246
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   247
subsection {* A few examples from ``Introduction to Isabelle'' *}
7001
8121e11ed765 Deriving rules in Isabelle;
wenzelm
parents: 6892
diff changeset
   248
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   249
text {* We rephrase some of the basic reasoning examples of
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   250
  \cite{isabelle-intro}, using HOL rather than FOL. *}
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   251
7820
cad7cc30fa40 more explanations;
wenzelm
parents: 7761
diff changeset
   252
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   253
subsubsection {* A propositional proof *}
7833
f5288e4b95d1 improved presentation;
wenzelm
parents: 7820
diff changeset
   254
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   255
text {* We consider the proposition @{text "P \<or> P \<longrightarrow> P"}.  The proof
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   256
  below involves forward-chaining from @{text "P \<or> P"}, followed by an
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   257
  explicit case-analysis on the two \emph{identical} cases. *}
6444
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
   258
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   259
lemma "P | P --> P"
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   260
proof
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   261
  assume "P | P"
23373
ead82c82da9e tuned proofs: avoid implicit prems;
wenzelm
parents: 18193
diff changeset
   262
  then show P
7833
f5288e4b95d1 improved presentation;
wenzelm
parents: 7820
diff changeset
   263
  proof                    -- {*
18193
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
   264
    rule @{text disjE}: \smash{$\infer{C}{A \disj B & \infer*{C}{[A]} & \infer*{C}{[B]}}$}
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   265
  *}
23393
31781b2de73d tuned proofs: avoid implicit prems;
wenzelm
parents: 23373
diff changeset
   266
    assume P show P by fact
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   267
  next
23393
31781b2de73d tuned proofs: avoid implicit prems;
wenzelm
parents: 23373
diff changeset
   268
    assume P show P by fact
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   269
  qed
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   270
qed
7833
f5288e4b95d1 improved presentation;
wenzelm
parents: 7820
diff changeset
   271
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   272
text {* Case splits are \emph{not} hardwired into the Isar language as
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   273
  a special feature.  The \isacommand{next} command used to separate
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   274
  the cases above is just a short form of managing block structure.
7833
f5288e4b95d1 improved presentation;
wenzelm
parents: 7820
diff changeset
   275
18193
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
   276
  \medskip In general, applying proof methods may split up a goal into
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
   277
  separate ``cases'', i.e.\ new subgoals with individual local
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
   278
  assumptions.  The corresponding proof text typically mimics this by
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
   279
  establishing results in appropriate contexts, separated by blocks.
7833
f5288e4b95d1 improved presentation;
wenzelm
parents: 7820
diff changeset
   280
18193
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
   281
  In order to avoid too much explicit parentheses, the Isar system
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
   282
  implicitly opens an additional block for any new goal, the
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
   283
  \isacommand{next} statement then closes one block level, opening a
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
   284
  new one.  The resulting behavior is what one would expect from
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
   285
  separating cases, only that it is more flexible.  E.g.\ an induction
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
   286
  base case (which does not introduce local assumptions) would
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
   287
  \emph{not} require \isacommand{next} to separate the subsequent step
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
   288
  case.
7833
f5288e4b95d1 improved presentation;
wenzelm
parents: 7820
diff changeset
   289
18193
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
   290
  \medskip In our example the situation is even simpler, since the two
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
   291
  cases actually coincide.  Consequently the proof may be rephrased as
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   292
  follows. *}
7833
f5288e4b95d1 improved presentation;
wenzelm
parents: 7820
diff changeset
   293
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   294
lemma "P | P --> P"
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   295
proof
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   296
  assume "P | P"
23373
ead82c82da9e tuned proofs: avoid implicit prems;
wenzelm
parents: 18193
diff changeset
   297
  then show P
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   298
  proof
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   299
    assume P
23393
31781b2de73d tuned proofs: avoid implicit prems;
wenzelm
parents: 23373
diff changeset
   300
    show P by fact
31781b2de73d tuned proofs: avoid implicit prems;
wenzelm
parents: 23373
diff changeset
   301
    show P by fact
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   302
  qed
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   303
qed
6444
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
   304
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   305
text {* Again, the rather vacuous body of the proof may be collapsed.
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   306
  Thus the case analysis degenerates into two assumption steps, which
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   307
  are implicitly performed when concluding the single rule step of the
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   308
  double-dot proof as follows. *}
7833
f5288e4b95d1 improved presentation;
wenzelm
parents: 7820
diff changeset
   309
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   310
lemma "P | P --> P"
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   311
proof
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   312
  assume "P | P"
23373
ead82c82da9e tuned proofs: avoid implicit prems;
wenzelm
parents: 18193
diff changeset
   313
  then show P ..
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   314
qed
6444
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
   315
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
   316
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   317
subsubsection {* A quantifier proof *}
7833
f5288e4b95d1 improved presentation;
wenzelm
parents: 7820
diff changeset
   318
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   319
text {* To illustrate quantifier reasoning, let us prove @{text
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   320
  "(\<exists>x. P (f x)) \<longrightarrow> (\<exists>y. P y)"}.  Informally, this holds because any
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   321
  @{text a} with @{text "P (f a)"} may be taken as a witness for the
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   322
  second existential statement.
6444
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
   323
18193
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
   324
  The first proof is rather verbose, exhibiting quite a lot of
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
   325
  (redundant) detail.  It gives explicit rules, even with some
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
   326
  instantiation.  Furthermore, we encounter two new language elements:
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
   327
  the \isacommand{fix} command augments the context by some new
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
   328
  ``arbitrary, but fixed'' element; the \isacommand{is} annotation
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   329
  binds term abbreviations by higher-order pattern matching. *}
7833
f5288e4b95d1 improved presentation;
wenzelm
parents: 7820
diff changeset
   330
10636
wenzelm
parents: 10007
diff changeset
   331
lemma "(EX x. P (f x)) --> (EX y. P y)"
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   332
proof
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   333
  assume "EX x. P (f x)"
23373
ead82c82da9e tuned proofs: avoid implicit prems;
wenzelm
parents: 18193
diff changeset
   334
  then show "EX y. P y"
7833
f5288e4b95d1 improved presentation;
wenzelm
parents: 7820
diff changeset
   335
  proof (rule exE)             -- {*
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   336
    rule @{text exE}: \smash{$\infer{B}{\ex x A(x) & \infer*{B}{[A(x)]_x}}$}
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   337
  *}
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   338
    fix a
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   339
    assume "P (f a)" (is "P ?witness")
23373
ead82c82da9e tuned proofs: avoid implicit prems;
wenzelm
parents: 18193
diff changeset
   340
    then show ?thesis by (rule exI [of P ?witness])
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   341
  qed
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   342
qed
6444
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
   343
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   344
text {* While explicit rule instantiation may occasionally improve
18193
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
   345
  readability of certain aspects of reasoning, it is usually quite
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
   346
  redundant.  Above, the basic proof outline gives already enough
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
   347
  structural clues for the system to infer both the rules and their
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
   348
  instances (by higher-order unification).  Thus we may as well prune
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   349
  the text as follows. *}
7833
f5288e4b95d1 improved presentation;
wenzelm
parents: 7820
diff changeset
   350
10636
wenzelm
parents: 10007
diff changeset
   351
lemma "(EX x. P (f x)) --> (EX y. P y)"
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   352
proof
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   353
  assume "EX x. P (f x)"
23373
ead82c82da9e tuned proofs: avoid implicit prems;
wenzelm
parents: 18193
diff changeset
   354
  then show "EX y. P y"
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   355
  proof
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   356
    fix a
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   357
    assume "P (f a)"
23373
ead82c82da9e tuned proofs: avoid implicit prems;
wenzelm
parents: 18193
diff changeset
   358
    then show ?thesis ..
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   359
  qed
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   360
qed
6444
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
   361
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   362
text {* Explicit @{text \<exists>}-elimination as seen above can become quite
18193
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
   363
  cumbersome in practice.  The derived Isar language element
54419506df9e tuned document;
wenzelm
parents: 16417
diff changeset
   364
  ``\isakeyword{obtain}'' provides a more handsome way to do
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   365
  generalized existence reasoning. *}
9477
9506127f6fbb obtain;
wenzelm
parents: 8902
diff changeset
   366
10636
wenzelm
parents: 10007
diff changeset
   367
lemma "(EX x. P (f x)) --> (EX y. P y)"
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   368
proof
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   369
  assume "EX x. P (f x)"
10636
wenzelm
parents: 10007
diff changeset
   370
  then obtain a where "P (f a)" ..
23373
ead82c82da9e tuned proofs: avoid implicit prems;
wenzelm
parents: 18193
diff changeset
   371
  then show "EX y. P y" ..
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   372
qed
9477
9506127f6fbb obtain;
wenzelm
parents: 8902
diff changeset
   373
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   374
text {* Technically, \isakeyword{obtain} is similar to
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   375
  \isakeyword{fix} and \isakeyword{assume} together with a soundness
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   376
  proof of the elimination involved.  Thus it behaves similar to any
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   377
  other forward proof element.  Also note that due to the nature of
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   378
  general existence reasoning involved here, any result exported from
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   379
  the context of an \isakeyword{obtain} statement may \emph{not} refer
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   380
  to the parameters introduced there. *}
9477
9506127f6fbb obtain;
wenzelm
parents: 8902
diff changeset
   381
6444
2ebe9e630cab Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff changeset
   382
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   383
subsubsection {* Deriving rules in Isabelle *}
7001
8121e11ed765 Deriving rules in Isabelle;
wenzelm
parents: 6892
diff changeset
   384
37671
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   385
text {* We derive the conjunction elimination rule from the
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   386
  corresponding projections.  The proof is quite straight-forward,
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   387
  since Isabelle/Isar supports non-atomic goals and assumptions fully
fa53d267dab3 misc tuning and modernization;
wenzelm
parents: 33026
diff changeset
   388
  transparently. *}
7001
8121e11ed765 Deriving rules in Isabelle;
wenzelm
parents: 6892
diff changeset
   389
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   390
theorem conjE: "A & B ==> (A ==> B ==> C) ==> C"
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   391
proof -
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   392
  assume "A & B"
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   393
  assume r: "A ==> B ==> C"
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   394
  show C
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   395
  proof (rule r)
23393
31781b2de73d tuned proofs: avoid implicit prems;
wenzelm
parents: 23373
diff changeset
   396
    show A by (rule conjunct1) fact
31781b2de73d tuned proofs: avoid implicit prems;
wenzelm
parents: 23373
diff changeset
   397
    show B by (rule conjunct2) fact
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   398
  qed
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   399
qed
7001
8121e11ed765 Deriving rules in Isabelle;
wenzelm
parents: 6892
diff changeset
   400
10007
64bf7da1994a isar-strip-terminators;
wenzelm
parents: 9659
diff changeset
   401
end