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