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