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