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