src/Doc/Isar_Ref/Synopsis.thy
author wenzelm
Sun Feb 07 20:20:35 2016 +0100 (2016-02-07)
changeset 62273 443256a20033
parent 62272 e6669fdfe759
child 63039 1a20fd9cf281
permissions -rw-r--r--
more on 'consider';
wenzelm@61656
     1
(*:maxLineLen=78:*)
wenzelm@61656
     2
wenzelm@42917
     3
theory Synopsis
wenzelm@42917
     4
imports Base Main
wenzelm@42917
     5
begin
wenzelm@42917
     6
wenzelm@58618
     7
chapter \<open>Synopsis\<close>
wenzelm@42917
     8
wenzelm@58618
     9
section \<open>Notepad\<close>
wenzelm@42917
    10
wenzelm@58618
    11
text \<open>
wenzelm@42917
    12
  An Isar proof body serves as mathematical notepad to compose logical
wenzelm@42918
    13
  content, consisting of types, terms, facts.
wenzelm@58618
    14
\<close>
wenzelm@42917
    15
wenzelm@42917
    16
wenzelm@58618
    17
subsection \<open>Types and terms\<close>
wenzelm@42918
    18
wenzelm@42918
    19
notepad
wenzelm@42918
    20
begin
wenzelm@58618
    21
  txt \<open>Locally fixed entities:\<close>
wenzelm@61580
    22
  fix x   \<comment> \<open>local constant, without any type information yet\<close>
wenzelm@61580
    23
  fix x :: 'a  \<comment> \<open>variant with explicit type-constraint for subsequent use\<close>
wenzelm@42918
    24
wenzelm@42918
    25
  fix a b
wenzelm@61580
    26
  assume "a = b"  \<comment> \<open>type assignment at first occurrence in concrete term\<close>
wenzelm@42918
    27
wenzelm@58618
    28
  txt \<open>Definitions (non-polymorphic):\<close>
wenzelm@42918
    29
  def x \<equiv> "t::'a"
wenzelm@42918
    30
wenzelm@58618
    31
  txt \<open>Abbreviations (polymorphic):\<close>
wenzelm@42918
    32
  let ?f = "\<lambda>x. x"
wenzelm@42918
    33
  term "?f ?f"
wenzelm@42918
    34
wenzelm@58618
    35
  txt \<open>Notation:\<close>
wenzelm@42918
    36
  write x  ("***")
wenzelm@42918
    37
end
wenzelm@42918
    38
wenzelm@42918
    39
wenzelm@58618
    40
subsection \<open>Facts\<close>
wenzelm@42917
    41
wenzelm@58618
    42
text \<open>
wenzelm@42917
    43
  A fact is a simultaneous list of theorems.
wenzelm@58618
    44
\<close>
wenzelm@42917
    45
wenzelm@42917
    46
wenzelm@58618
    47
subsubsection \<open>Producing facts\<close>
wenzelm@42917
    48
wenzelm@42917
    49
notepad
wenzelm@42917
    50
begin
wenzelm@42917
    51
wenzelm@58618
    52
  txt \<open>Via assumption (``lambda''):\<close>
wenzelm@42917
    53
  assume a: A
wenzelm@42917
    54
wenzelm@58618
    55
  txt \<open>Via proof (``let''):\<close>
wenzelm@62271
    56
  have b: B \<proof>
wenzelm@42917
    57
wenzelm@58618
    58
  txt \<open>Via abbreviation (``let''):\<close>
wenzelm@42917
    59
  note c = a b
wenzelm@42917
    60
wenzelm@42917
    61
end
wenzelm@42917
    62
wenzelm@42917
    63
wenzelm@58618
    64
subsubsection \<open>Referencing facts\<close>
wenzelm@42917
    65
wenzelm@42917
    66
notepad
wenzelm@42917
    67
begin
wenzelm@58618
    68
  txt \<open>Via explicit name:\<close>
wenzelm@42917
    69
  assume a: A
wenzelm@42917
    70
  note a
wenzelm@42917
    71
wenzelm@58618
    72
  txt \<open>Via implicit name:\<close>
wenzelm@42917
    73
  assume A
wenzelm@42917
    74
  note this
wenzelm@42917
    75
wenzelm@58618
    76
  txt \<open>Via literal proposition (unification with results from the proof text):\<close>
wenzelm@42917
    77
  assume A
wenzelm@58618
    78
  note \<open>A\<close>
wenzelm@42917
    79
wenzelm@42917
    80
  assume "\<And>x. B x"
wenzelm@58618
    81
  note \<open>B a\<close>
wenzelm@58618
    82
  note \<open>B b\<close>
wenzelm@42917
    83
end
wenzelm@42917
    84
wenzelm@42917
    85
wenzelm@58618
    86
subsubsection \<open>Manipulating facts\<close>
wenzelm@42917
    87
wenzelm@42917
    88
notepad
wenzelm@42917
    89
begin
wenzelm@58618
    90
  txt \<open>Instantiation:\<close>
wenzelm@42917
    91
  assume a: "\<And>x. B x"
wenzelm@42917
    92
  note a
wenzelm@42917
    93
  note a [of b]
wenzelm@42917
    94
  note a [where x = b]
wenzelm@42917
    95
wenzelm@58618
    96
  txt \<open>Backchaining:\<close>
wenzelm@42917
    97
  assume 1: A
wenzelm@42917
    98
  assume 2: "A \<Longrightarrow> C"
wenzelm@42917
    99
  note 2 [OF 1]
wenzelm@42917
   100
  note 1 [THEN 2]
wenzelm@42917
   101
wenzelm@58618
   102
  txt \<open>Symmetric results:\<close>
wenzelm@42917
   103
  assume "x = y"
wenzelm@42917
   104
  note this [symmetric]
wenzelm@42917
   105
wenzelm@42917
   106
  assume "x \<noteq> y"
wenzelm@42917
   107
  note this [symmetric]
wenzelm@42917
   108
wenzelm@58618
   109
  txt \<open>Adhoc-simplification (take care!):\<close>
wenzelm@42917
   110
  assume "P ([] @ xs)"
wenzelm@42917
   111
  note this [simplified]
wenzelm@42917
   112
end
wenzelm@42917
   113
wenzelm@42917
   114
wenzelm@58618
   115
subsubsection \<open>Projections\<close>
wenzelm@42917
   116
wenzelm@58618
   117
text \<open>
wenzelm@42917
   118
  Isar facts consist of multiple theorems.  There is notation to project
wenzelm@42917
   119
  interval ranges.
wenzelm@58618
   120
\<close>
wenzelm@42917
   121
wenzelm@42917
   122
notepad
wenzelm@42917
   123
begin
wenzelm@42917
   124
  assume stuff: A B C D
wenzelm@42917
   125
  note stuff(1)
wenzelm@42917
   126
  note stuff(2-3)
wenzelm@42917
   127
  note stuff(2-)
wenzelm@42917
   128
end
wenzelm@42917
   129
wenzelm@42917
   130
wenzelm@58618
   131
subsubsection \<open>Naming conventions\<close>
wenzelm@42917
   132
wenzelm@58618
   133
text \<open>
wenzelm@61421
   134
  \<^item> Lower-case identifiers are usually preferred.
wenzelm@42917
   135
wenzelm@61421
   136
  \<^item> Facts can be named after the main term within the proposition.
wenzelm@42917
   137
wenzelm@61477
   138
  \<^item> Facts should \<^emph>\<open>not\<close> be named after the command that
wenzelm@42917
   139
  introduced them (@{command "assume"}, @{command "have"}).  This is
wenzelm@42917
   140
  misleading and hard to maintain.
wenzelm@42917
   141
wenzelm@61421
   142
  \<^item> Natural numbers can be used as ``meaningless'' names (more
wenzelm@61493
   143
  appropriate than \<open>a1\<close>, \<open>a2\<close> etc.)
wenzelm@42917
   144
wenzelm@61493
   145
  \<^item> Symbolic identifiers are supported (e.g. \<open>*\<close>, \<open>**\<close>, \<open>***\<close>).
wenzelm@58618
   146
\<close>
wenzelm@42917
   147
wenzelm@42917
   148
wenzelm@58618
   149
subsection \<open>Block structure\<close>
wenzelm@42917
   150
wenzelm@58618
   151
text \<open>
wenzelm@42917
   152
  The formal notepad is block structured.  The fact produced by the last
wenzelm@42917
   153
  entry of a block is exported into the outer context.
wenzelm@58618
   154
\<close>
wenzelm@42917
   155
wenzelm@42917
   156
notepad
wenzelm@42917
   157
begin
wenzelm@42917
   158
  {
wenzelm@62271
   159
    have a: A \<proof>
wenzelm@62271
   160
    have b: B \<proof>
wenzelm@42917
   161
    note a b
wenzelm@42917
   162
  }
wenzelm@42917
   163
  note this
wenzelm@58618
   164
  note \<open>A\<close>
wenzelm@58618
   165
  note \<open>B\<close>
wenzelm@42917
   166
end
wenzelm@42917
   167
wenzelm@58618
   168
text \<open>Explicit blocks as well as implicit blocks of nested goal
wenzelm@42917
   169
  statements (e.g.\ @{command have}) automatically introduce one extra
wenzelm@42917
   170
  pair of parentheses in reserve.  The @{command next} command allows
wenzelm@58618
   171
  to ``jump'' between these sub-blocks.\<close>
wenzelm@42917
   172
wenzelm@42917
   173
notepad
wenzelm@42917
   174
begin
wenzelm@42917
   175
wenzelm@42917
   176
  {
wenzelm@62271
   177
    have a: A \<proof>
wenzelm@42917
   178
  next
wenzelm@42917
   179
    have b: B
wenzelm@42917
   180
    proof -
wenzelm@62271
   181
      show B \<proof>
wenzelm@42917
   182
    next
wenzelm@62271
   183
      have c: C \<proof>
wenzelm@42917
   184
    next
wenzelm@62271
   185
      have d: D \<proof>
wenzelm@42917
   186
    qed
wenzelm@42917
   187
  }
wenzelm@42917
   188
wenzelm@58618
   189
  txt \<open>Alternative version with explicit parentheses everywhere:\<close>
wenzelm@42917
   190
wenzelm@42917
   191
  {
wenzelm@42917
   192
    {
wenzelm@62271
   193
      have a: A \<proof>
wenzelm@42917
   194
    }
wenzelm@42917
   195
    {
wenzelm@42917
   196
      have b: B
wenzelm@42917
   197
      proof -
wenzelm@42917
   198
        {
wenzelm@62271
   199
          show B \<proof>
wenzelm@42917
   200
        }
wenzelm@42917
   201
        {
wenzelm@62271
   202
          have c: C \<proof>
wenzelm@42917
   203
        }
wenzelm@42917
   204
        {
wenzelm@62271
   205
          have d: D \<proof>
wenzelm@42917
   206
        }
wenzelm@42917
   207
      qed
wenzelm@42917
   208
    }
wenzelm@42917
   209
  }
wenzelm@42917
   210
wenzelm@42917
   211
end
wenzelm@42917
   212
wenzelm@42919
   213
wenzelm@58618
   214
section \<open>Calculational reasoning \label{sec:calculations-synopsis}\<close>
wenzelm@42919
   215
wenzelm@58618
   216
text \<open>
wenzelm@42919
   217
  For example, see @{file "~~/src/HOL/Isar_Examples/Group.thy"}.
wenzelm@58618
   218
\<close>
wenzelm@42919
   219
wenzelm@42919
   220
wenzelm@58618
   221
subsection \<open>Special names in Isar proofs\<close>
wenzelm@42919
   222
wenzelm@58618
   223
text \<open>
wenzelm@61493
   224
  \<^item> term \<open>?thesis\<close> --- the main conclusion of the
wenzelm@42919
   225
  innermost pending claim
wenzelm@42919
   226
wenzelm@61493
   227
  \<^item> term \<open>\<dots>\<close> --- the argument of the last explicitly
wenzelm@61421
   228
  stated result (for infix application this is the right-hand side)
wenzelm@42919
   229
wenzelm@61493
   230
  \<^item> fact \<open>this\<close> --- the last result produced in the text
wenzelm@58618
   231
\<close>
wenzelm@42919
   232
wenzelm@42919
   233
notepad
wenzelm@42919
   234
begin
wenzelm@42919
   235
  have "x = y"
wenzelm@42919
   236
  proof -
wenzelm@42919
   237
    term ?thesis
wenzelm@62271
   238
    show ?thesis \<proof>
wenzelm@61580
   239
    term ?thesis  \<comment> \<open>static!\<close>
wenzelm@42919
   240
  qed
wenzelm@42919
   241
  term "\<dots>"
wenzelm@42919
   242
  thm this
wenzelm@42919
   243
end
wenzelm@42919
   244
wenzelm@58618
   245
text \<open>Calculational reasoning maintains the special fact called
wenzelm@61493
   246
  ``\<open>calculation\<close>'' in the background.  Certain language
wenzelm@61493
   247
  elements combine primary \<open>this\<close> with secondary \<open>calculation\<close>.\<close>
wenzelm@42919
   248
wenzelm@42919
   249
wenzelm@58618
   250
subsection \<open>Transitive chains\<close>
wenzelm@42919
   251
wenzelm@61493
   252
text \<open>The Idea is to combine \<open>this\<close> and \<open>calculation\<close>
wenzelm@61493
   253
  via typical \<open>trans\<close> rules (see also @{command
wenzelm@58618
   254
  print_trans_rules}):\<close>
wenzelm@42919
   255
wenzelm@42919
   256
thm trans
wenzelm@42919
   257
thm less_trans
wenzelm@42919
   258
thm less_le_trans
wenzelm@42919
   259
wenzelm@42919
   260
notepad
wenzelm@42919
   261
begin
wenzelm@58618
   262
  txt \<open>Plain bottom-up calculation:\<close>
wenzelm@62271
   263
  have "a = b" \<proof>
wenzelm@42919
   264
  also
wenzelm@62271
   265
  have "b = c" \<proof>
wenzelm@42919
   266
  also
wenzelm@62271
   267
  have "c = d" \<proof>
wenzelm@42919
   268
  finally
wenzelm@42919
   269
  have "a = d" .
wenzelm@42919
   270
wenzelm@61493
   271
  txt \<open>Variant using the \<open>\<dots>\<close> abbreviation:\<close>
wenzelm@62271
   272
  have "a = b" \<proof>
wenzelm@42919
   273
  also
wenzelm@62271
   274
  have "\<dots> = c" \<proof>
wenzelm@42919
   275
  also
wenzelm@62271
   276
  have "\<dots> = d" \<proof>
wenzelm@42919
   277
  finally
wenzelm@42919
   278
  have "a = d" .
wenzelm@42919
   279
wenzelm@58618
   280
  txt \<open>Top-down version with explicit claim at the head:\<close>
wenzelm@42919
   281
  have "a = d"
wenzelm@42919
   282
  proof -
wenzelm@62271
   283
    have "a = b" \<proof>
wenzelm@42919
   284
    also
wenzelm@62271
   285
    have "\<dots> = c" \<proof>
wenzelm@42919
   286
    also
wenzelm@62271
   287
    have "\<dots> = d" \<proof>
wenzelm@42919
   288
    finally
wenzelm@42919
   289
    show ?thesis .
wenzelm@42919
   290
  qed
wenzelm@42919
   291
next
wenzelm@58618
   292
  txt \<open>Mixed inequalities (require suitable base type):\<close>
wenzelm@42919
   293
  fix a b c d :: nat
wenzelm@42919
   294
wenzelm@62271
   295
  have "a < b" \<proof>
wenzelm@42919
   296
  also
wenzelm@62271
   297
  have "b \<le> c" \<proof>
wenzelm@42919
   298
  also
wenzelm@62271
   299
  have "c = d" \<proof>
wenzelm@42919
   300
  finally
wenzelm@42919
   301
  have "a < d" .
wenzelm@42919
   302
end
wenzelm@42919
   303
wenzelm@42919
   304
wenzelm@58618
   305
subsubsection \<open>Notes\<close>
wenzelm@42919
   306
wenzelm@58618
   307
text \<open>
wenzelm@61493
   308
  \<^item> The notion of \<open>trans\<close> rule is very general due to the
wenzelm@42919
   309
  flexibility of Isabelle/Pure rule composition.
wenzelm@42919
   310
wenzelm@61421
   311
  \<^item> User applications may declare their own rules, with some care
wenzelm@42919
   312
  about the operational details of higher-order unification.
wenzelm@58618
   313
\<close>
wenzelm@42919
   314
wenzelm@42919
   315
wenzelm@62273
   316
subsection \<open>Degenerate calculations\<close>
wenzelm@42919
   317
wenzelm@62273
   318
text \<open>The Idea is to append \<open>this\<close> to \<open>calculation\<close>, without rule composition.
wenzelm@62273
   319
  This is occasionally useful to avoid naming intermediate facts.\<close>
wenzelm@42919
   320
wenzelm@42919
   321
notepad
wenzelm@42919
   322
begin
wenzelm@58618
   323
  txt \<open>A vacuous proof:\<close>
wenzelm@62271
   324
  have A \<proof>
wenzelm@42919
   325
  moreover
wenzelm@62271
   326
  have B \<proof>
wenzelm@42919
   327
  moreover
wenzelm@62271
   328
  have C \<proof>
wenzelm@42919
   329
  ultimately
wenzelm@42919
   330
  have A and B and C .
wenzelm@42919
   331
next
wenzelm@58618
   332
  txt \<open>Slightly more content (trivial bigstep reasoning):\<close>
wenzelm@62271
   333
  have A \<proof>
wenzelm@42919
   334
  moreover
wenzelm@62271
   335
  have B \<proof>
wenzelm@42919
   336
  moreover
wenzelm@62271
   337
  have C \<proof>
wenzelm@42919
   338
  ultimately
wenzelm@42919
   339
  have "A \<and> B \<and> C" by blast
wenzelm@42919
   340
end
wenzelm@42919
   341
wenzelm@62273
   342
text \<open>Note that For multi-branch case splitting, it is better to use @{command
wenzelm@62273
   343
  consider}.\<close>
wenzelm@62273
   344
wenzelm@42920
   345
wenzelm@58618
   346
section \<open>Induction\<close>
wenzelm@42921
   347
wenzelm@58618
   348
subsection \<open>Induction as Natural Deduction\<close>
wenzelm@42921
   349
wenzelm@58618
   350
text \<open>In principle, induction is just a special case of Natural
wenzelm@42921
   351
  Deduction (see also \secref{sec:natural-deduction-synopsis}).  For
wenzelm@58618
   352
  example:\<close>
wenzelm@42921
   353
wenzelm@42921
   354
thm nat.induct
wenzelm@42921
   355
print_statement nat.induct
wenzelm@42921
   356
wenzelm@42921
   357
notepad
wenzelm@42921
   358
begin
wenzelm@42921
   359
  fix n :: nat
wenzelm@42921
   360
  have "P n"
wenzelm@61580
   361
  proof (rule nat.induct)  \<comment> \<open>fragile rule application!\<close>
wenzelm@62271
   362
    show "P 0" \<proof>
wenzelm@42921
   363
  next
wenzelm@42921
   364
    fix n :: nat
wenzelm@42921
   365
    assume "P n"
wenzelm@62271
   366
    show "P (Suc n)" \<proof>
wenzelm@42921
   367
  qed
wenzelm@42921
   368
end
wenzelm@42921
   369
wenzelm@58618
   370
text \<open>
wenzelm@42921
   371
  In practice, much more proof infrastructure is required.
wenzelm@42921
   372
wenzelm@42921
   373
  The proof method @{method induct} provides:
wenzelm@42921
   374
wenzelm@61421
   375
  \<^item> implicit rule selection and robust instantiation
wenzelm@42921
   376
wenzelm@61421
   377
  \<^item> context elements via symbolic case names
wenzelm@42921
   378
wenzelm@61421
   379
  \<^item> support for rule-structured induction statements, with local
wenzelm@61421
   380
  parameters, premises, etc.
wenzelm@58618
   381
\<close>
wenzelm@42921
   382
wenzelm@42921
   383
notepad
wenzelm@42921
   384
begin
wenzelm@42921
   385
  fix n :: nat
wenzelm@42921
   386
  have "P n"
wenzelm@42921
   387
  proof (induct n)
wenzelm@42921
   388
    case 0
wenzelm@62271
   389
    show ?case \<proof>
wenzelm@42921
   390
  next
wenzelm@42921
   391
    case (Suc n)
wenzelm@62271
   392
    from Suc.hyps show ?case \<proof>
wenzelm@42921
   393
  qed
wenzelm@42921
   394
end
wenzelm@42921
   395
wenzelm@42921
   396
wenzelm@58618
   397
subsubsection \<open>Example\<close>
wenzelm@42921
   398
wenzelm@58618
   399
text \<open>
wenzelm@42921
   400
  The subsequent example combines the following proof patterns:
wenzelm@42921
   401
wenzelm@61421
   402
  \<^item> outermost induction (over the datatype structure of natural
wenzelm@42921
   403
  numbers), to decompose the proof problem in top-down manner
wenzelm@42921
   404
wenzelm@61421
   405
  \<^item> calculational reasoning (\secref{sec:calculations-synopsis})
wenzelm@42921
   406
  to compose the result in each case
wenzelm@42921
   407
wenzelm@61421
   408
  \<^item> solving local claims within the calculation by simplification
wenzelm@58618
   409
\<close>
wenzelm@42921
   410
wenzelm@42921
   411
lemma
wenzelm@42921
   412
  fixes n :: nat
wenzelm@42921
   413
  shows "(\<Sum>i=0..n. i) = n * (n + 1) div 2"
wenzelm@42921
   414
proof (induct n)
wenzelm@42921
   415
  case 0
wenzelm@42921
   416
  have "(\<Sum>i=0..0. i) = (0::nat)" by simp
wenzelm@42921
   417
  also have "\<dots> = 0 * (0 + 1) div 2" by simp
wenzelm@42921
   418
  finally show ?case .
wenzelm@42921
   419
next
wenzelm@42921
   420
  case (Suc n)
wenzelm@42921
   421
  have "(\<Sum>i=0..Suc n. i) = (\<Sum>i=0..n. i) + (n + 1)" by simp
wenzelm@42921
   422
  also have "\<dots> = n * (n + 1) div 2 + (n + 1)" by (simp add: Suc.hyps)
wenzelm@42921
   423
  also have "\<dots> = (n * (n + 1) + 2 * (n + 1)) div 2" by simp
wenzelm@42921
   424
  also have "\<dots> = (Suc n * (Suc n + 1)) div 2" by simp
wenzelm@42921
   425
  finally show ?case .
wenzelm@42921
   426
qed
wenzelm@42921
   427
wenzelm@58618
   428
text \<open>This demonstrates how induction proofs can be done without
wenzelm@58618
   429
  having to consider the raw Natural Deduction structure.\<close>
wenzelm@42921
   430
wenzelm@42921
   431
wenzelm@58618
   432
subsection \<open>Induction with local parameters and premises\<close>
wenzelm@42921
   433
wenzelm@58618
   434
text \<open>Idea: Pure rule statements are passed through the induction
wenzelm@42921
   435
  rule.  This achieves convenient proof patterns, thanks to some
wenzelm@42921
   436
  internal trickery in the @{method induct} method.
wenzelm@42921
   437
wenzelm@61493
   438
  Important: Using compact HOL formulae with \<open>\<forall>/\<longrightarrow>\<close> is a
wenzelm@42921
   439
  well-known anti-pattern! It would produce useless formal noise.
wenzelm@58618
   440
\<close>
wenzelm@42921
   441
wenzelm@42921
   442
notepad
wenzelm@42921
   443
begin
wenzelm@42921
   444
  fix n :: nat
wenzelm@42921
   445
  fix P :: "nat \<Rightarrow> bool"
wenzelm@42921
   446
  fix Q :: "'a \<Rightarrow> nat \<Rightarrow> bool"
wenzelm@42921
   447
wenzelm@42921
   448
  have "P n"
wenzelm@42921
   449
  proof (induct n)
wenzelm@42921
   450
    case 0
wenzelm@62271
   451
    show "P 0" \<proof>
wenzelm@42921
   452
  next
wenzelm@42921
   453
    case (Suc n)
wenzelm@62271
   454
    from \<open>P n\<close> show "P (Suc n)" \<proof>
wenzelm@42921
   455
  qed
wenzelm@42921
   456
wenzelm@42921
   457
  have "A n \<Longrightarrow> P n"
wenzelm@42921
   458
  proof (induct n)
wenzelm@42921
   459
    case 0
wenzelm@62271
   460
    from \<open>A 0\<close> show "P 0" \<proof>
wenzelm@42921
   461
  next
wenzelm@42921
   462
    case (Suc n)
wenzelm@58618
   463
    from \<open>A n \<Longrightarrow> P n\<close>
wenzelm@62271
   464
      and \<open>A (Suc n)\<close> show "P (Suc n)" \<proof>
wenzelm@42921
   465
  qed
wenzelm@42921
   466
wenzelm@42921
   467
  have "\<And>x. Q x n"
wenzelm@42921
   468
  proof (induct n)
wenzelm@42921
   469
    case 0
wenzelm@62271
   470
    show "Q x 0" \<proof>
wenzelm@42921
   471
  next
wenzelm@42921
   472
    case (Suc n)
wenzelm@62271
   473
    from \<open>\<And>x. Q x n\<close> show "Q x (Suc n)" \<proof>
wenzelm@58618
   474
    txt \<open>Local quantification admits arbitrary instances:\<close>
wenzelm@58618
   475
    note \<open>Q a n\<close> and \<open>Q b n\<close>
wenzelm@42921
   476
  qed
wenzelm@42921
   477
end
wenzelm@42921
   478
wenzelm@42921
   479
wenzelm@58618
   480
subsection \<open>Implicit induction context\<close>
wenzelm@42921
   481
wenzelm@58618
   482
text \<open>The @{method induct} method can isolate local parameters and
wenzelm@42921
   483
  premises directly from the given statement.  This is convenient in
wenzelm@42921
   484
  practical applications, but requires some understanding of what is
wenzelm@58618
   485
  going on internally (as explained above).\<close>
wenzelm@42921
   486
wenzelm@42921
   487
notepad
wenzelm@42921
   488
begin
wenzelm@42921
   489
  fix n :: nat
wenzelm@42921
   490
  fix Q :: "'a \<Rightarrow> nat \<Rightarrow> bool"
wenzelm@42921
   491
wenzelm@42921
   492
  fix x :: 'a
wenzelm@42921
   493
  assume "A x n"
wenzelm@42921
   494
  then have "Q x n"
wenzelm@42921
   495
  proof (induct n arbitrary: x)
wenzelm@42921
   496
    case 0
wenzelm@62271
   497
    from \<open>A x 0\<close> show "Q x 0" \<proof>
wenzelm@42921
   498
  next
wenzelm@42921
   499
    case (Suc n)
wenzelm@61580
   500
    from \<open>\<And>x. A x n \<Longrightarrow> Q x n\<close>  \<comment> \<open>arbitrary instances can be produced here\<close>
wenzelm@62271
   501
      and \<open>A x (Suc n)\<close> show "Q x (Suc n)" \<proof>
wenzelm@42921
   502
  qed
wenzelm@42921
   503
end
wenzelm@42921
   504
wenzelm@42921
   505
wenzelm@58618
   506
subsection \<open>Advanced induction with term definitions\<close>
wenzelm@42921
   507
wenzelm@58618
   508
text \<open>Induction over subexpressions of a certain shape are delicate
wenzelm@42921
   509
  to formalize.  The Isar @{method induct} method provides
wenzelm@42921
   510
  infrastructure for this.
wenzelm@42921
   511
wenzelm@42921
   512
  Idea: sub-expressions of the problem are turned into a defined
wenzelm@42921
   513
  induction variable; often accompanied with fixing of auxiliary
wenzelm@58618
   514
  parameters in the original expression.\<close>
wenzelm@42921
   515
wenzelm@42921
   516
notepad
wenzelm@42921
   517
begin
wenzelm@42921
   518
  fix a :: "'a \<Rightarrow> nat"
wenzelm@42921
   519
  fix A :: "nat \<Rightarrow> bool"
wenzelm@42921
   520
wenzelm@42921
   521
  assume "A (a x)"
wenzelm@42921
   522
  then have "P (a x)"
wenzelm@42921
   523
  proof (induct "a x" arbitrary: x)
wenzelm@42921
   524
    case 0
wenzelm@58618
   525
    note prem = \<open>A (a x)\<close>
wenzelm@58618
   526
      and defn = \<open>0 = a x\<close>
wenzelm@62271
   527
    show "P (a x)" \<proof>
wenzelm@42921
   528
  next
wenzelm@42921
   529
    case (Suc n)
wenzelm@58618
   530
    note hyp = \<open>\<And>x. n = a x \<Longrightarrow> A (a x) \<Longrightarrow> P (a x)\<close>
wenzelm@58618
   531
      and prem = \<open>A (a x)\<close>
wenzelm@58618
   532
      and defn = \<open>Suc n = a x\<close>
wenzelm@62271
   533
    show "P (a x)" \<proof>
wenzelm@42921
   534
  qed
wenzelm@42921
   535
end
wenzelm@42921
   536
wenzelm@42921
   537
wenzelm@58618
   538
section \<open>Natural Deduction \label{sec:natural-deduction-synopsis}\<close>
wenzelm@42920
   539
wenzelm@58618
   540
subsection \<open>Rule statements\<close>
wenzelm@42920
   541
wenzelm@58618
   542
text \<open>
wenzelm@42920
   543
  Isabelle/Pure ``theorems'' are always natural deduction rules,
wenzelm@42920
   544
  which sometimes happen to consist of a conclusion only.
wenzelm@42920
   545
wenzelm@61493
   546
  The framework connectives \<open>\<And>\<close> and \<open>\<Longrightarrow>\<close> indicate the
wenzelm@58618
   547
  rule structure declaratively.  For example:\<close>
wenzelm@42920
   548
wenzelm@42920
   549
thm conjI
wenzelm@42920
   550
thm impI
wenzelm@42920
   551
thm nat.induct
wenzelm@42920
   552
wenzelm@58618
   553
text \<open>
wenzelm@42920
   554
  The object-logic is embedded into the Pure framework via an implicit
wenzelm@42920
   555
  derivability judgment @{term "Trueprop :: bool \<Rightarrow> prop"}.
wenzelm@42920
   556
wenzelm@42920
   557
  Thus any HOL formulae appears atomic to the Pure framework, while
wenzelm@42920
   558
  the rule structure outlines the corresponding proof pattern.
wenzelm@42920
   559
wenzelm@42920
   560
  This can be made explicit as follows:
wenzelm@58618
   561
\<close>
wenzelm@42920
   562
wenzelm@42920
   563
notepad
wenzelm@42920
   564
begin
wenzelm@42920
   565
  write Trueprop  ("Tr")
wenzelm@42920
   566
wenzelm@42920
   567
  thm conjI
wenzelm@42920
   568
  thm impI
wenzelm@42920
   569
  thm nat.induct
wenzelm@42920
   570
end
wenzelm@42920
   571
wenzelm@58618
   572
text \<open>
wenzelm@42920
   573
  Isar provides first-class notation for rule statements as follows.
wenzelm@58618
   574
\<close>
wenzelm@42920
   575
wenzelm@42920
   576
print_statement conjI
wenzelm@42920
   577
print_statement impI
wenzelm@42920
   578
print_statement nat.induct
wenzelm@42920
   579
wenzelm@42920
   580
wenzelm@58618
   581
subsubsection \<open>Examples\<close>
wenzelm@42920
   582
wenzelm@58618
   583
text \<open>
wenzelm@42920
   584
  Introductions and eliminations of some standard connectives of
wenzelm@42920
   585
  the object-logic can be written as rule statements as follows.  (The
wenzelm@42920
   586
  proof ``@{command "by"}~@{method blast}'' serves as sanity check.)
wenzelm@58618
   587
\<close>
wenzelm@42920
   588
wenzelm@42920
   589
lemma "(P \<Longrightarrow> False) \<Longrightarrow> \<not> P" by blast
wenzelm@42920
   590
lemma "\<not> P \<Longrightarrow> P \<Longrightarrow> Q" by blast
wenzelm@42920
   591
wenzelm@42920
   592
lemma "P \<Longrightarrow> Q \<Longrightarrow> P \<and> Q" by blast
wenzelm@42920
   593
lemma "P \<and> Q \<Longrightarrow> (P \<Longrightarrow> Q \<Longrightarrow> R) \<Longrightarrow> R" by blast
wenzelm@42920
   594
wenzelm@42920
   595
lemma "P \<Longrightarrow> P \<or> Q" by blast
wenzelm@42920
   596
lemma "Q \<Longrightarrow> P \<or> Q" by blast
wenzelm@42920
   597
lemma "P \<or> Q \<Longrightarrow> (P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R" by blast
wenzelm@42920
   598
wenzelm@42920
   599
lemma "(\<And>x. P x) \<Longrightarrow> (\<forall>x. P x)" by blast
wenzelm@42920
   600
lemma "(\<forall>x. P x) \<Longrightarrow> P x" by blast
wenzelm@42920
   601
wenzelm@42920
   602
lemma "P x \<Longrightarrow> (\<exists>x. P x)" by blast
wenzelm@42920
   603
lemma "(\<exists>x. P x) \<Longrightarrow> (\<And>x. P x \<Longrightarrow> R) \<Longrightarrow> R" by blast
wenzelm@42920
   604
wenzelm@42920
   605
lemma "x \<in> A \<Longrightarrow> x \<in> B \<Longrightarrow> x \<in> A \<inter> B" by blast
wenzelm@42920
   606
lemma "x \<in> A \<inter> B \<Longrightarrow> (x \<in> A \<Longrightarrow> x \<in> B \<Longrightarrow> R) \<Longrightarrow> R" by blast
wenzelm@42920
   607
wenzelm@42920
   608
lemma "x \<in> A \<Longrightarrow> x \<in> A \<union> B" by blast
wenzelm@42920
   609
lemma "x \<in> B \<Longrightarrow> x \<in> A \<union> B" by blast
wenzelm@42920
   610
lemma "x \<in> A \<union> B \<Longrightarrow> (x \<in> A \<Longrightarrow> R) \<Longrightarrow> (x \<in> B \<Longrightarrow> R) \<Longrightarrow> R" by blast
wenzelm@42920
   611
wenzelm@42920
   612
wenzelm@58618
   613
subsection \<open>Isar context elements\<close>
wenzelm@42920
   614
wenzelm@58618
   615
text \<open>We derive some results out of the blue, using Isar context
wenzelm@42920
   616
  elements and some explicit blocks.  This illustrates their meaning
wenzelm@58618
   617
  wrt.\ Pure connectives, without goal states getting in the way.\<close>
wenzelm@42920
   618
wenzelm@42920
   619
notepad
wenzelm@42920
   620
begin
wenzelm@42920
   621
  {
wenzelm@42920
   622
    fix x
wenzelm@62271
   623
    have "B x" \<proof>
wenzelm@42920
   624
  }
wenzelm@42920
   625
  have "\<And>x. B x" by fact
wenzelm@42920
   626
wenzelm@42920
   627
next
wenzelm@42920
   628
wenzelm@42920
   629
  {
wenzelm@42920
   630
    assume A
wenzelm@62271
   631
    have B \<proof>
wenzelm@42920
   632
  }
wenzelm@42920
   633
  have "A \<Longrightarrow> B" by fact
wenzelm@42920
   634
wenzelm@42920
   635
next
wenzelm@42920
   636
wenzelm@42920
   637
  {
wenzelm@42920
   638
    def x \<equiv> t
wenzelm@62271
   639
    have "B x" \<proof>
wenzelm@42920
   640
  }
wenzelm@42920
   641
  have "B t" by fact
wenzelm@42920
   642
wenzelm@42920
   643
next
wenzelm@42920
   644
wenzelm@42920
   645
  {
wenzelm@62271
   646
    obtain x :: 'a where "B x" \<proof>
wenzelm@62271
   647
    have C \<proof>
wenzelm@42920
   648
  }
wenzelm@42920
   649
  have C by fact
wenzelm@42920
   650
wenzelm@42920
   651
end
wenzelm@42920
   652
wenzelm@42920
   653
wenzelm@58618
   654
subsection \<open>Pure rule composition\<close>
wenzelm@42920
   655
wenzelm@58618
   656
text \<open>
wenzelm@42920
   657
  The Pure framework provides means for:
wenzelm@42920
   658
wenzelm@61421
   659
  \<^item> backward-chaining of rules by @{inference resolution}
wenzelm@42920
   660
wenzelm@61421
   661
  \<^item> closing of branches by @{inference assumption}
wenzelm@42920
   662
wenzelm@42920
   663
wenzelm@61493
   664
  Both principles involve higher-order unification of \<open>\<lambda>\<close>-terms
wenzelm@61493
   665
  modulo \<open>\<alpha>\<beta>\<eta>\<close>-equivalence (cf.\ Huet and Miller).
wenzelm@61458
   666
\<close>
wenzelm@42920
   667
wenzelm@42920
   668
notepad
wenzelm@42920
   669
begin
wenzelm@42920
   670
  assume a: A and b: B
wenzelm@42920
   671
  thm conjI
wenzelm@61580
   672
  thm conjI [of A B]  \<comment> "instantiation"
wenzelm@61580
   673
  thm conjI [of A B, OF a b]  \<comment> "instantiation and composition"
wenzelm@61580
   674
  thm conjI [OF a b]  \<comment> "composition via unification (trivial)"
wenzelm@58618
   675
  thm conjI [OF \<open>A\<close> \<open>B\<close>]
wenzelm@42920
   676
wenzelm@42920
   677
  thm conjI [OF disjI1]
wenzelm@42920
   678
end
wenzelm@42920
   679
wenzelm@58618
   680
text \<open>Note: Low-level rule composition is tedious and leads to
wenzelm@58618
   681
  unreadable~/ unmaintainable expressions in the text.\<close>
wenzelm@42920
   682
wenzelm@42920
   683
wenzelm@58618
   684
subsection \<open>Structured backward reasoning\<close>
wenzelm@42920
   685
wenzelm@58618
   686
text \<open>Idea: Canonical proof decomposition via @{command fix}~/
wenzelm@42920
   687
  @{command assume}~/ @{command show}, where the body produces a
wenzelm@58618
   688
  natural deduction rule to refine some goal.\<close>
wenzelm@42920
   689
wenzelm@42920
   690
notepad
wenzelm@42920
   691
begin
wenzelm@42920
   692
  fix A B :: "'a \<Rightarrow> bool"
wenzelm@42920
   693
wenzelm@42920
   694
  have "\<And>x. A x \<Longrightarrow> B x"
wenzelm@42920
   695
  proof -
wenzelm@42920
   696
    fix x
wenzelm@42920
   697
    assume "A x"
wenzelm@62271
   698
    show "B x" \<proof>
wenzelm@42920
   699
  qed
wenzelm@42920
   700
wenzelm@42920
   701
  have "\<And>x. A x \<Longrightarrow> B x"
wenzelm@42920
   702
  proof -
wenzelm@42920
   703
    {
wenzelm@42920
   704
      fix x
wenzelm@42920
   705
      assume "A x"
wenzelm@62271
   706
      show "B x" \<proof>
wenzelm@61580
   707
    } \<comment> "implicit block structure made explicit"
wenzelm@58618
   708
    note \<open>\<And>x. A x \<Longrightarrow> B x\<close>
wenzelm@61580
   709
      \<comment> "side exit for the resulting rule"
wenzelm@42920
   710
  qed
wenzelm@42920
   711
end
wenzelm@42920
   712
wenzelm@42920
   713
wenzelm@58618
   714
subsection \<open>Structured rule application\<close>
wenzelm@42920
   715
wenzelm@58618
   716
text \<open>
wenzelm@42920
   717
  Idea: Previous facts and new claims are composed with a rule from
wenzelm@42920
   718
  the context (or background library).
wenzelm@58618
   719
\<close>
wenzelm@42920
   720
wenzelm@42920
   721
notepad
wenzelm@42920
   722
begin
wenzelm@62272
   723
  assume r\<^sub>1: "A \<Longrightarrow> B \<Longrightarrow> C"  \<comment> \<open>simple rule (Horn clause)\<close>
wenzelm@42920
   724
wenzelm@62271
   725
  have A \<proof>  \<comment> "prefix of facts via outer sub-proof"
wenzelm@42920
   726
  then have C
wenzelm@62272
   727
  proof (rule r\<^sub>1)
wenzelm@62271
   728
    show B \<proof>  \<comment> "remaining rule premises via inner sub-proof"
wenzelm@42920
   729
  qed
wenzelm@42920
   730
wenzelm@42920
   731
  have C
wenzelm@62272
   732
  proof (rule r\<^sub>1)
wenzelm@62271
   733
    show A \<proof>
wenzelm@62271
   734
    show B \<proof>
wenzelm@42920
   735
  qed
wenzelm@42920
   736
wenzelm@62271
   737
  have A and B \<proof>
wenzelm@42920
   738
  then have C
wenzelm@62272
   739
  proof (rule r\<^sub>1)
wenzelm@42920
   740
  qed
wenzelm@42920
   741
wenzelm@62271
   742
  have A and B \<proof>
wenzelm@62272
   743
  then have C by (rule r\<^sub>1)
wenzelm@42920
   744
wenzelm@42920
   745
next
wenzelm@42920
   746
wenzelm@62272
   747
  assume r\<^sub>2: "A \<Longrightarrow> (\<And>x. B\<^sub>1 x \<Longrightarrow> B\<^sub>2 x) \<Longrightarrow> C"  \<comment> \<open>nested rule\<close>
wenzelm@42920
   748
wenzelm@62271
   749
  have A \<proof>
wenzelm@42920
   750
  then have C
wenzelm@62272
   751
  proof (rule r\<^sub>2)
wenzelm@42920
   752
    fix x
wenzelm@62272
   753
    assume "B\<^sub>1 x"
wenzelm@62272
   754
    show "B\<^sub>2 x" \<proof>
wenzelm@42920
   755
  qed
wenzelm@42920
   756
wenzelm@62272
   757
  txt \<open>The compound rule premise @{prop "\<And>x. B\<^sub>1 x \<Longrightarrow> B\<^sub>2 x"} is better
wenzelm@42920
   758
    addressed via @{command fix}~/ @{command assume}~/ @{command show}
wenzelm@58618
   759
    in the nested proof body.\<close>
wenzelm@42920
   760
end
wenzelm@42920
   761
wenzelm@42920
   762
wenzelm@58618
   763
subsection \<open>Example: predicate logic\<close>
wenzelm@42920
   764
wenzelm@58618
   765
text \<open>
wenzelm@42920
   766
  Using the above principles, standard introduction and elimination proofs
wenzelm@42920
   767
  of predicate logic connectives of HOL work as follows.
wenzelm@58618
   768
\<close>
wenzelm@42920
   769
wenzelm@42920
   770
notepad
wenzelm@42920
   771
begin
wenzelm@62271
   772
  have "A \<longrightarrow> B" and A \<proof>
wenzelm@42920
   773
  then have B ..
wenzelm@42920
   774
wenzelm@62271
   775
  have A \<proof>
wenzelm@42920
   776
  then have "A \<or> B" ..
wenzelm@42920
   777
wenzelm@62271
   778
  have B \<proof>
wenzelm@42920
   779
  then have "A \<or> B" ..
wenzelm@42920
   780
wenzelm@62271
   781
  have "A \<or> B" \<proof>
wenzelm@42920
   782
  then have C
wenzelm@42920
   783
  proof
wenzelm@42920
   784
    assume A
wenzelm@62271
   785
    then show C \<proof>
wenzelm@42920
   786
  next
wenzelm@42920
   787
    assume B
wenzelm@62271
   788
    then show C \<proof>
wenzelm@42920
   789
  qed
wenzelm@42920
   790
wenzelm@62271
   791
  have A and B \<proof>
wenzelm@42920
   792
  then have "A \<and> B" ..
wenzelm@42920
   793
wenzelm@62271
   794
  have "A \<and> B" \<proof>
wenzelm@42920
   795
  then have A ..
wenzelm@42920
   796
wenzelm@62271
   797
  have "A \<and> B" \<proof>
wenzelm@42920
   798
  then have B ..
wenzelm@42920
   799
wenzelm@62271
   800
  have False \<proof>
wenzelm@42920
   801
  then have A ..
wenzelm@42920
   802
wenzelm@42920
   803
  have True ..
wenzelm@42920
   804
wenzelm@42920
   805
  have "\<not> A"
wenzelm@42920
   806
  proof
wenzelm@42920
   807
    assume A
wenzelm@62271
   808
    then show False \<proof>
wenzelm@42920
   809
  qed
wenzelm@42920
   810
wenzelm@62271
   811
  have "\<not> A" and A \<proof>
wenzelm@42920
   812
  then have B ..
wenzelm@42920
   813
wenzelm@42920
   814
  have "\<forall>x. P x"
wenzelm@42920
   815
  proof
wenzelm@42920
   816
    fix x
wenzelm@62271
   817
    show "P x" \<proof>
wenzelm@42920
   818
  qed
wenzelm@42920
   819
wenzelm@62271
   820
  have "\<forall>x. P x" \<proof>
wenzelm@42920
   821
  then have "P a" ..
wenzelm@42920
   822
wenzelm@42920
   823
  have "\<exists>x. P x"
wenzelm@42920
   824
  proof
wenzelm@62271
   825
    show "P a" \<proof>
wenzelm@42920
   826
  qed
wenzelm@42920
   827
wenzelm@62271
   828
  have "\<exists>x. P x" \<proof>
wenzelm@42920
   829
  then have C
wenzelm@42920
   830
  proof
wenzelm@42920
   831
    fix a
wenzelm@42920
   832
    assume "P a"
wenzelm@62271
   833
    show C \<proof>
wenzelm@42920
   834
  qed
wenzelm@42920
   835
wenzelm@58618
   836
  txt \<open>Less awkward version using @{command obtain}:\<close>
wenzelm@62271
   837
  have "\<exists>x. P x" \<proof>
wenzelm@42920
   838
  then obtain a where "P a" ..
wenzelm@42920
   839
end
wenzelm@42920
   840
wenzelm@58618
   841
text \<open>Further variations to illustrate Isar sub-proofs involving
wenzelm@58618
   842
  @{command show}:\<close>
wenzelm@42920
   843
wenzelm@42920
   844
notepad
wenzelm@42920
   845
begin
wenzelm@42920
   846
  have "A \<and> B"
wenzelm@61580
   847
  proof  \<comment> \<open>two strictly isolated subproofs\<close>
wenzelm@62271
   848
    show A \<proof>
wenzelm@42920
   849
  next
wenzelm@62271
   850
    show B \<proof>
wenzelm@42920
   851
  qed
wenzelm@42920
   852
wenzelm@42920
   853
  have "A \<and> B"
wenzelm@61580
   854
  proof  \<comment> \<open>one simultaneous sub-proof\<close>
wenzelm@62271
   855
    show A and B \<proof>
wenzelm@42920
   856
  qed
wenzelm@42920
   857
wenzelm@42920
   858
  have "A \<and> B"
wenzelm@61580
   859
  proof  \<comment> \<open>two subproofs in the same context\<close>
wenzelm@62271
   860
    show A \<proof>
wenzelm@62271
   861
    show B \<proof>
wenzelm@42920
   862
  qed
wenzelm@42920
   863
wenzelm@42920
   864
  have "A \<and> B"
wenzelm@61580
   865
  proof  \<comment> \<open>swapped order\<close>
wenzelm@62271
   866
    show B \<proof>
wenzelm@62271
   867
    show A \<proof>
wenzelm@42920
   868
  qed
wenzelm@42920
   869
wenzelm@42920
   870
  have "A \<and> B"
wenzelm@61580
   871
  proof  \<comment> \<open>sequential subproofs\<close>
wenzelm@62271
   872
    show A \<proof>
wenzelm@62271
   873
    show B using \<open>A\<close> \<proof>
wenzelm@42920
   874
  qed
wenzelm@42920
   875
end
wenzelm@42920
   876
wenzelm@42920
   877
wenzelm@58618
   878
subsubsection \<open>Example: set-theoretic operators\<close>
wenzelm@42920
   879
wenzelm@61493
   880
text \<open>There is nothing special about logical connectives (\<open>\<and>\<close>, \<open>\<or>\<close>, \<open>\<forall>\<close>, \<open>\<exists>\<close> etc.).  Operators from
wenzelm@45103
   881
  set-theory or lattice-theory work analogously.  It is only a matter
wenzelm@42920
   882
  of rule declarations in the library; rules can be also specified
wenzelm@42920
   883
  explicitly.
wenzelm@58618
   884
\<close>
wenzelm@42920
   885
wenzelm@42920
   886
notepad
wenzelm@42920
   887
begin
wenzelm@62271
   888
  have "x \<in> A" and "x \<in> B" \<proof>
wenzelm@42920
   889
  then have "x \<in> A \<inter> B" ..
wenzelm@42920
   890
wenzelm@62271
   891
  have "x \<in> A" \<proof>
wenzelm@42920
   892
  then have "x \<in> A \<union> B" ..
wenzelm@42920
   893
wenzelm@62271
   894
  have "x \<in> B" \<proof>
wenzelm@42920
   895
  then have "x \<in> A \<union> B" ..
wenzelm@42920
   896
wenzelm@62271
   897
  have "x \<in> A \<union> B" \<proof>
wenzelm@42920
   898
  then have C
wenzelm@42920
   899
  proof
wenzelm@42920
   900
    assume "x \<in> A"
wenzelm@62271
   901
    then show C \<proof>
wenzelm@42920
   902
  next
wenzelm@42920
   903
    assume "x \<in> B"
wenzelm@62271
   904
    then show C \<proof>
wenzelm@42920
   905
  qed
wenzelm@42920
   906
wenzelm@42920
   907
next
wenzelm@42920
   908
  have "x \<in> \<Inter>A"
wenzelm@42920
   909
  proof
wenzelm@42920
   910
    fix a
wenzelm@42920
   911
    assume "a \<in> A"
wenzelm@62271
   912
    show "x \<in> a" \<proof>
wenzelm@42920
   913
  qed
wenzelm@42920
   914
wenzelm@62271
   915
  have "x \<in> \<Inter>A" \<proof>
wenzelm@42920
   916
  then have "x \<in> a"
wenzelm@42920
   917
  proof
wenzelm@62271
   918
    show "a \<in> A" \<proof>
wenzelm@42920
   919
  qed
wenzelm@42920
   920
wenzelm@62271
   921
  have "a \<in> A" and "x \<in> a" \<proof>
wenzelm@42920
   922
  then have "x \<in> \<Union>A" ..
wenzelm@42920
   923
wenzelm@62271
   924
  have "x \<in> \<Union>A" \<proof>
wenzelm@42920
   925
  then obtain a where "a \<in> A" and "x \<in> a" ..
wenzelm@42920
   926
end
wenzelm@42920
   927
wenzelm@42922
   928
wenzelm@58618
   929
section \<open>Generalized elimination and cases\<close>
wenzelm@42922
   930
wenzelm@58618
   931
subsection \<open>General elimination rules\<close>
wenzelm@42922
   932
wenzelm@58618
   933
text \<open>
wenzelm@42922
   934
  The general format of elimination rules is illustrated by the
wenzelm@42922
   935
  following typical representatives:
wenzelm@58618
   936
\<close>
wenzelm@42922
   937
wenzelm@61580
   938
thm exE     \<comment> \<open>local parameter\<close>
wenzelm@61580
   939
thm conjE   \<comment> \<open>local premises\<close>
wenzelm@61580
   940
thm disjE   \<comment> \<open>split into cases\<close>
wenzelm@42922
   941
wenzelm@58618
   942
text \<open>
wenzelm@42922
   943
  Combining these characteristics leads to the following general scheme
wenzelm@42922
   944
  for elimination rules with cases:
wenzelm@42922
   945
wenzelm@61421
   946
  \<^item> prefix of assumptions (or ``major premises'')
wenzelm@42922
   947
wenzelm@61421
   948
  \<^item> one or more cases that enable to establish the main conclusion
wenzelm@61421
   949
  in an augmented context
wenzelm@58618
   950
\<close>
wenzelm@42922
   951
wenzelm@42922
   952
notepad
wenzelm@42922
   953
begin
wenzelm@42922
   954
  assume r:
wenzelm@62272
   955
    "A\<^sub>1 \<Longrightarrow> A\<^sub>2 \<Longrightarrow>  (* assumptions *)
wenzelm@62272
   956
      (\<And>x y. B\<^sub>1 x y \<Longrightarrow> C\<^sub>1 x y \<Longrightarrow> R) \<Longrightarrow>  (* case 1 *)
wenzelm@62272
   957
      (\<And>x y. B\<^sub>2 x y \<Longrightarrow> C\<^sub>2 x y \<Longrightarrow> R) \<Longrightarrow>  (* case 2 *)
wenzelm@42922
   958
      R  (* main conclusion *)"
wenzelm@42922
   959
wenzelm@62272
   960
  have A\<^sub>1 and A\<^sub>2 \<proof>
wenzelm@42922
   961
  then have R
wenzelm@42922
   962
  proof (rule r)
wenzelm@42922
   963
    fix x y
wenzelm@62272
   964
    assume "B\<^sub>1 x y" and "C\<^sub>1 x y"
wenzelm@62271
   965
    show ?thesis \<proof>
wenzelm@42922
   966
  next
wenzelm@42922
   967
    fix x y
wenzelm@62272
   968
    assume "B\<^sub>2 x y" and "C\<^sub>2 x y"
wenzelm@62271
   969
    show ?thesis \<proof>
wenzelm@42922
   970
  qed
wenzelm@42922
   971
end
wenzelm@42922
   972
wenzelm@61493
   973
text \<open>Here \<open>?thesis\<close> is used to refer to the unchanged goal
wenzelm@58618
   974
  statement.\<close>
wenzelm@42922
   975
wenzelm@42922
   976
wenzelm@58618
   977
subsection \<open>Rules with cases\<close>
wenzelm@42922
   978
wenzelm@58618
   979
text \<open>
wenzelm@42922
   980
  Applying an elimination rule to some goal, leaves that unchanged
wenzelm@42922
   981
  but allows to augment the context in the sub-proof of each case.
wenzelm@42922
   982
wenzelm@42922
   983
  Isar provides some infrastructure to support this:
wenzelm@42922
   984
wenzelm@61421
   985
  \<^item> native language elements to state eliminations
wenzelm@42922
   986
wenzelm@61421
   987
  \<^item> symbolic case names
wenzelm@42922
   988
wenzelm@61421
   989
  \<^item> method @{method cases} to recover this structure in a
wenzelm@42922
   990
  sub-proof
wenzelm@58618
   991
\<close>
wenzelm@42922
   992
wenzelm@42922
   993
print_statement exE
wenzelm@42922
   994
print_statement conjE
wenzelm@42922
   995
print_statement disjE
wenzelm@42922
   996
wenzelm@42922
   997
lemma
wenzelm@62272
   998
  assumes A\<^sub>1 and A\<^sub>2  \<comment> \<open>assumptions\<close>
wenzelm@42922
   999
  obtains
wenzelm@62272
  1000
    (case\<^sub>1)  x y where "B\<^sub>1 x y" and "C\<^sub>1 x y"
wenzelm@62272
  1001
  | (case\<^sub>2)  x y where "B\<^sub>2 x y" and "C\<^sub>2 x y"
wenzelm@62271
  1002
  \<proof>
wenzelm@42922
  1003
wenzelm@42922
  1004
wenzelm@58618
  1005
subsubsection \<open>Example\<close>
wenzelm@42922
  1006
wenzelm@42922
  1007
lemma tertium_non_datur:
wenzelm@42922
  1008
  obtains
wenzelm@42922
  1009
    (T)  A
wenzelm@42922
  1010
  | (F)  "\<not> A"
wenzelm@42922
  1011
  by blast
wenzelm@42922
  1012
wenzelm@42922
  1013
notepad
wenzelm@42922
  1014
begin
wenzelm@42922
  1015
  fix x y :: 'a
wenzelm@42922
  1016
  have C
wenzelm@42922
  1017
  proof (cases "x = y" rule: tertium_non_datur)
wenzelm@42922
  1018
    case T
wenzelm@62271
  1019
    from \<open>x = y\<close> show ?thesis \<proof>
wenzelm@42922
  1020
  next
wenzelm@42922
  1021
    case F
wenzelm@62271
  1022
    from \<open>x \<noteq> y\<close> show ?thesis \<proof>
wenzelm@42922
  1023
  qed
wenzelm@42922
  1024
end
wenzelm@42922
  1025
wenzelm@42922
  1026
wenzelm@58618
  1027
subsubsection \<open>Example\<close>
wenzelm@42922
  1028
wenzelm@58618
  1029
text \<open>
wenzelm@42922
  1030
  Isabelle/HOL specification mechanisms (datatype, inductive, etc.)
wenzelm@42922
  1031
  provide suitable derived cases rules.
wenzelm@58618
  1032
\<close>
wenzelm@42922
  1033
blanchet@58310
  1034
datatype foo = Foo | Bar foo
wenzelm@42922
  1035
wenzelm@42922
  1036
notepad
wenzelm@42922
  1037
begin
wenzelm@42922
  1038
  fix x :: foo
wenzelm@42922
  1039
  have C
wenzelm@42922
  1040
  proof (cases x)
wenzelm@42922
  1041
    case Foo
wenzelm@62271
  1042
    from \<open>x = Foo\<close> show ?thesis \<proof>
wenzelm@42922
  1043
  next
wenzelm@42922
  1044
    case (Bar a)
wenzelm@62271
  1045
    from \<open>x = Bar a\<close> show ?thesis \<proof>
wenzelm@42922
  1046
  qed
wenzelm@42922
  1047
end
wenzelm@42922
  1048
wenzelm@42922
  1049
wenzelm@62273
  1050
subsection \<open>Elimination statements and case-splitting\<close>
wenzelm@62273
  1051
wenzelm@62273
  1052
text \<open>
wenzelm@62273
  1053
  The @{command consider} states rules for generalized elimination and case
wenzelm@62273
  1054
  splitting. This is like a toplevel statement \<^theory_text>\<open>theorem obtains\<close> used within
wenzelm@62273
  1055
  a proof body; or like a multi-branch \<^theory_text>\<open>obtain\<close> without activation of the
wenzelm@62273
  1056
  local context elements yet.
wenzelm@62273
  1057
wenzelm@62273
  1058
  The proof method @{method cases} is able to use such rules with
wenzelm@62273
  1059
  forward-chaining (e.g.\ via \<^theory_text>\<open>then\<close>). This leads to the subsequent pattern
wenzelm@62273
  1060
  for case-splitting in a particular situation within a proof.
wenzelm@62273
  1061
\<close>
wenzelm@62273
  1062
wenzelm@62273
  1063
notepad
wenzelm@62273
  1064
begin
wenzelm@62273
  1065
  consider (a) A | (b) B | (c) C
wenzelm@62273
  1066
    \<proof>  \<comment> \<open>typically \<^theory_text>\<open>by auto\<close>, \<^theory_text>\<open>by blast\<close> etc.\<close>
wenzelm@62273
  1067
  then have something
wenzelm@62273
  1068
  proof cases
wenzelm@62273
  1069
    case a
wenzelm@62273
  1070
    then show ?thesis \<proof>
wenzelm@62273
  1071
  next
wenzelm@62273
  1072
    case b
wenzelm@62273
  1073
    then show ?thesis \<proof>
wenzelm@62273
  1074
  next
wenzelm@62273
  1075
    case c
wenzelm@62273
  1076
    then show ?thesis \<proof>
wenzelm@62273
  1077
  qed
wenzelm@62273
  1078
end
wenzelm@62273
  1079
wenzelm@58618
  1080
subsection \<open>Obtaining local contexts\<close>
wenzelm@42922
  1081
wenzelm@58618
  1082
text \<open>A single ``case'' branch may be inlined into Isar proof text
wenzelm@42922
  1083
  via @{command obtain}.  This proves @{prop "(\<And>x. B x \<Longrightarrow> thesis) \<Longrightarrow>
wenzelm@58618
  1084
  thesis"} on the spot, and augments the context afterwards.\<close>
wenzelm@42922
  1085
wenzelm@42922
  1086
notepad
wenzelm@42922
  1087
begin
wenzelm@42922
  1088
  fix B :: "'a \<Rightarrow> bool"
wenzelm@42922
  1089
wenzelm@62271
  1090
  obtain x where "B x" \<proof>
wenzelm@58618
  1091
  note \<open>B x\<close>
wenzelm@42922
  1092
wenzelm@58618
  1093
  txt \<open>Conclusions from this context may not mention @{term x} again!\<close>
wenzelm@42922
  1094
  {
wenzelm@62271
  1095
    obtain x where "B x" \<proof>
wenzelm@62271
  1096
    from \<open>B x\<close> have C \<proof>
wenzelm@42922
  1097
  }
wenzelm@58618
  1098
  note \<open>C\<close>
wenzelm@42922
  1099
end
wenzelm@42922
  1100
wenzelm@45103
  1101
end