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