doc-src/IsarRef/Thy/Synopsis.thy
author wenzelm
Wed Jun 01 13:06:45 2011 +0200 (2011-06-01)
changeset 42920 8c0a49d72857
parent 42919 6e83c2f73240
child 42921 ec270c6cb942
permissions -rw-r--r--
some material on "Structured Natural Deduction";
tuned;
wenzelm@42917
     1
theory Synopsis
wenzelm@42917
     2
imports Base Main
wenzelm@42917
     3
begin
wenzelm@42917
     4
wenzelm@42917
     5
chapter {* Synopsis *}
wenzelm@42917
     6
wenzelm@42917
     7
section {* Notepad *}
wenzelm@42917
     8
wenzelm@42917
     9
text {*
wenzelm@42917
    10
  An Isar proof body serves as mathematical notepad to compose logical
wenzelm@42918
    11
  content, consisting of types, terms, facts.
wenzelm@42917
    12
*}
wenzelm@42917
    13
wenzelm@42917
    14
wenzelm@42918
    15
subsection {* Types and terms *}
wenzelm@42918
    16
wenzelm@42918
    17
notepad
wenzelm@42918
    18
begin
wenzelm@42918
    19
  txt {* Locally fixed entities: *}
wenzelm@42918
    20
  fix x   -- {* local constant, without any type information yet *}
wenzelm@42918
    21
  fix x :: 'a  -- {* variant with explicit type-constraint for subsequent use*}
wenzelm@42918
    22
wenzelm@42918
    23
  fix a b
wenzelm@42918
    24
  assume "a = b"  -- {* type assignment at first occurrence in concrete term *}
wenzelm@42918
    25
wenzelm@42918
    26
  txt {* Definitions (non-polymorphic): *}
wenzelm@42918
    27
  def x \<equiv> "t::'a"
wenzelm@42918
    28
wenzelm@42918
    29
  txt {* Abbreviations (polymorphic): *}
wenzelm@42918
    30
  let ?f = "\<lambda>x. x"
wenzelm@42918
    31
  term "?f ?f"
wenzelm@42918
    32
wenzelm@42918
    33
  txt {* Notation: *}
wenzelm@42918
    34
  write x  ("***")
wenzelm@42918
    35
end
wenzelm@42918
    36
wenzelm@42918
    37
wenzelm@42917
    38
subsection {* Facts *}
wenzelm@42917
    39
wenzelm@42917
    40
text {*
wenzelm@42917
    41
  A fact is a simultaneous list of theorems.
wenzelm@42917
    42
*}
wenzelm@42917
    43
wenzelm@42917
    44
wenzelm@42917
    45
subsubsection {* Producing facts *}
wenzelm@42917
    46
wenzelm@42917
    47
notepad
wenzelm@42917
    48
begin
wenzelm@42917
    49
wenzelm@42917
    50
  txt {* Via assumption (``lambda''): *}
wenzelm@42917
    51
  assume a: A
wenzelm@42917
    52
wenzelm@42917
    53
  txt {* Via proof (``let''): *}
wenzelm@42917
    54
  have b: B sorry
wenzelm@42917
    55
wenzelm@42917
    56
  txt {* Via abbreviation (``let''): *}
wenzelm@42917
    57
  note c = a b
wenzelm@42917
    58
wenzelm@42917
    59
end
wenzelm@42917
    60
wenzelm@42917
    61
wenzelm@42917
    62
subsubsection {* Referencing facts *}
wenzelm@42917
    63
wenzelm@42917
    64
notepad
wenzelm@42917
    65
begin
wenzelm@42917
    66
  txt {* Via explicit name: *}
wenzelm@42917
    67
  assume a: A
wenzelm@42917
    68
  note a
wenzelm@42917
    69
wenzelm@42917
    70
  txt {* Via implicit name: *}
wenzelm@42917
    71
  assume A
wenzelm@42917
    72
  note this
wenzelm@42917
    73
wenzelm@42917
    74
  txt {* Via literal proposition (unification with results from the proof text): *}
wenzelm@42917
    75
  assume A
wenzelm@42917
    76
  note `A`
wenzelm@42917
    77
wenzelm@42917
    78
  assume "\<And>x. B x"
wenzelm@42917
    79
  note `B a`
wenzelm@42917
    80
  note `B b`
wenzelm@42917
    81
end
wenzelm@42917
    82
wenzelm@42917
    83
wenzelm@42917
    84
subsubsection {* Manipulating facts *}
wenzelm@42917
    85
wenzelm@42917
    86
notepad
wenzelm@42917
    87
begin
wenzelm@42917
    88
  txt {* Instantiation: *}
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@42917
    94
  txt {* Backchaining: *}
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@42917
   100
  txt {* Symmetric results: *}
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@42917
   107
  txt {* Adhoc-simplication (take care!): *}
wenzelm@42917
   108
  assume "P ([] @ xs)"
wenzelm@42917
   109
  note this [simplified]
wenzelm@42917
   110
end
wenzelm@42917
   111
wenzelm@42917
   112
wenzelm@42917
   113
subsubsection {* Projections *}
wenzelm@42917
   114
wenzelm@42917
   115
text {*
wenzelm@42917
   116
  Isar facts consist of multiple theorems.  There is notation to project
wenzelm@42917
   117
  interval ranges.
wenzelm@42917
   118
*}
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@42917
   129
subsubsection {* Naming conventions *}
wenzelm@42917
   130
wenzelm@42917
   131
text {*
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@42917
   149
*}
wenzelm@42917
   150
wenzelm@42917
   151
wenzelm@42917
   152
subsection {* Block structure *}
wenzelm@42917
   153
wenzelm@42917
   154
text {*
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@42917
   157
*}
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@42917
   167
  note `A`
wenzelm@42917
   168
  note `B`
wenzelm@42917
   169
end
wenzelm@42917
   170
wenzelm@42917
   171
text {* 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@42917
   174
  to ``jump'' between these sub-blocks. *}
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@42917
   192
  txt {* Alternative version with explicit parentheses everywhere: *}
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@42919
   217
section {* Calculational reasoning *}
wenzelm@42919
   218
wenzelm@42919
   219
text {*
wenzelm@42919
   220
  For example, see @{file "~~/src/HOL/Isar_Examples/Group.thy"}.
wenzelm@42919
   221
*}
wenzelm@42919
   222
wenzelm@42919
   223
wenzelm@42919
   224
subsection {* Special names in Isar proofs *}
wenzelm@42919
   225
wenzelm@42919
   226
text {*
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@42919
   238
*}
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@42919
   246
    term ?thesis  -- {* static! *}
wenzelm@42919
   247
  qed
wenzelm@42919
   248
  term "\<dots>"
wenzelm@42919
   249
  thm this
wenzelm@42919
   250
end
wenzelm@42919
   251
wenzelm@42919
   252
text {* 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@42919
   255
  calculation}. *}
wenzelm@42919
   256
wenzelm@42919
   257
wenzelm@42919
   258
subsection {* Transitive chains *}
wenzelm@42919
   259
wenzelm@42919
   260
text {* The Idea is to combine @{text this} and @{text calculation}
wenzelm@42919
   261
  via typical @{text trans} rules (see also @{command
wenzelm@42919
   262
  print_trans_rules}): *}
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@42919
   270
  txt {* Plain bottom-up calculation: *}
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@42919
   279
  txt {* Variant using the @{text "\<dots>"} abbreviation: *}
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@42919
   288
  txt {* Top-down version with explicit claim at the head: *}
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@42919
   300
  txt {* Mixed inequalities (require suitable base type): *}
wenzelm@42919
   301
  fix a b c d :: nat
wenzelm@42919
   302
wenzelm@42919
   303
  have "a < b" sorry
wenzelm@42919
   304
  also
wenzelm@42919
   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@42919
   313
subsubsection {* Notes *}
wenzelm@42919
   314
wenzelm@42919
   315
text {*
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
wenzelm@42919
   321
  \item User applications may declare there 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@42919
   325
*}
wenzelm@42919
   326
wenzelm@42919
   327
wenzelm@42919
   328
subsection {* Degenerate calculations and bigstep reasoning *}
wenzelm@42919
   329
wenzelm@42919
   330
text {* The Idea is to append @{text this} to @{text calculation},
wenzelm@42919
   331
  without rule composition.  *}
wenzelm@42919
   332
wenzelm@42919
   333
notepad
wenzelm@42919
   334
begin
wenzelm@42920
   335
  txt {* A vacuous proof: *}
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@42919
   344
  txt {* Slightly more content (trivial bigstep reasoning): *}
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@42920
   353
  txt {* More ambitious bigstep reasoning involving structured results: *}
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@42919
   362
  have R by blast  -- {* ``big-bang integration'' of proof blocks (occasionally fragile) *}
wenzelm@42919
   363
end
wenzelm@42919
   364
wenzelm@42920
   365
wenzelm@42920
   366
section {* Structured Natural Deduction *}
wenzelm@42920
   367
wenzelm@42920
   368
subsection {* Rule statements *}
wenzelm@42920
   369
wenzelm@42920
   370
text {*
wenzelm@42920
   371
  Isabelle/Pure ``theorems'' are always natural deduction rules,
wenzelm@42920
   372
  which sometimes happen to consist of a conclusion only.
wenzelm@42920
   373
wenzelm@42920
   374
  The framework connectives @{text "\<And>"} and @{text "\<Longrightarrow>"} indicate the
wenzelm@42920
   375
  rule structure declaratively.  For example: *}
wenzelm@42920
   376
wenzelm@42920
   377
thm conjI
wenzelm@42920
   378
thm impI
wenzelm@42920
   379
thm nat.induct
wenzelm@42920
   380
wenzelm@42920
   381
text {*
wenzelm@42920
   382
  The object-logic is embedded into the Pure framework via an implicit
wenzelm@42920
   383
  derivability judgment @{term "Trueprop :: bool \<Rightarrow> prop"}.
wenzelm@42920
   384
wenzelm@42920
   385
  Thus any HOL formulae appears atomic to the Pure framework, while
wenzelm@42920
   386
  the rule structure outlines the corresponding proof pattern.
wenzelm@42920
   387
wenzelm@42920
   388
  This can be made explicit as follows:
wenzelm@42920
   389
*}
wenzelm@42920
   390
wenzelm@42920
   391
notepad
wenzelm@42920
   392
begin
wenzelm@42920
   393
  write Trueprop  ("Tr")
wenzelm@42920
   394
wenzelm@42920
   395
  thm conjI
wenzelm@42920
   396
  thm impI
wenzelm@42920
   397
  thm nat.induct
wenzelm@42920
   398
end
wenzelm@42920
   399
wenzelm@42920
   400
text {*
wenzelm@42920
   401
  Isar provides first-class notation for rule statements as follows.
wenzelm@42920
   402
*}
wenzelm@42920
   403
wenzelm@42920
   404
print_statement conjI
wenzelm@42920
   405
print_statement impI
wenzelm@42920
   406
print_statement nat.induct
wenzelm@42920
   407
wenzelm@42920
   408
wenzelm@42920
   409
subsubsection {* Examples *}
wenzelm@42920
   410
wenzelm@42920
   411
text {*
wenzelm@42920
   412
  Introductions and eliminations of some standard connectives of
wenzelm@42920
   413
  the object-logic can be written as rule statements as follows.  (The
wenzelm@42920
   414
  proof ``@{command "by"}~@{method blast}'' serves as sanity check.)
wenzelm@42920
   415
*}
wenzelm@42920
   416
wenzelm@42920
   417
lemma "(P \<Longrightarrow> False) \<Longrightarrow> \<not> P" by blast
wenzelm@42920
   418
lemma "\<not> P \<Longrightarrow> P \<Longrightarrow> Q" by blast
wenzelm@42920
   419
wenzelm@42920
   420
lemma "P \<Longrightarrow> Q \<Longrightarrow> P \<and> Q" by blast
wenzelm@42920
   421
lemma "P \<and> Q \<Longrightarrow> (P \<Longrightarrow> Q \<Longrightarrow> R) \<Longrightarrow> R" by blast
wenzelm@42920
   422
wenzelm@42920
   423
lemma "P \<Longrightarrow> P \<or> Q" by blast
wenzelm@42920
   424
lemma "Q \<Longrightarrow> P \<or> Q" by blast
wenzelm@42920
   425
lemma "P \<or> Q \<Longrightarrow> (P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R" by blast
wenzelm@42920
   426
wenzelm@42920
   427
lemma "(\<And>x. P x) \<Longrightarrow> (\<forall>x. P x)" by blast
wenzelm@42920
   428
lemma "(\<forall>x. P x) \<Longrightarrow> P x" by blast
wenzelm@42920
   429
wenzelm@42920
   430
lemma "P x \<Longrightarrow> (\<exists>x. P x)" by blast
wenzelm@42920
   431
lemma "(\<exists>x. P x) \<Longrightarrow> (\<And>x. P x \<Longrightarrow> R) \<Longrightarrow> R" by blast
wenzelm@42920
   432
wenzelm@42920
   433
lemma "x \<in> A \<Longrightarrow> x \<in> B \<Longrightarrow> x \<in> A \<inter> B" by blast
wenzelm@42920
   434
lemma "x \<in> A \<inter> B \<Longrightarrow> (x \<in> A \<Longrightarrow> x \<in> B \<Longrightarrow> R) \<Longrightarrow> R" by blast
wenzelm@42920
   435
wenzelm@42920
   436
lemma "x \<in> A \<Longrightarrow> x \<in> A \<union> B" by blast
wenzelm@42920
   437
lemma "x \<in> B \<Longrightarrow> x \<in> A \<union> B" by blast
wenzelm@42920
   438
lemma "x \<in> A \<union> B \<Longrightarrow> (x \<in> A \<Longrightarrow> R) \<Longrightarrow> (x \<in> B \<Longrightarrow> R) \<Longrightarrow> R" by blast
wenzelm@42920
   439
wenzelm@42920
   440
wenzelm@42920
   441
subsection {* Isar context elements *}
wenzelm@42920
   442
wenzelm@42920
   443
text {* We derive some results out of the blue, using Isar context
wenzelm@42920
   444
  elements and some explicit blocks.  This illustrates their meaning
wenzelm@42920
   445
  wrt.\ Pure connectives, without goal states getting in the way.  *}
wenzelm@42920
   446
wenzelm@42920
   447
notepad
wenzelm@42920
   448
begin
wenzelm@42920
   449
  {
wenzelm@42920
   450
    fix x
wenzelm@42920
   451
    have "B x" sorry
wenzelm@42920
   452
  }
wenzelm@42920
   453
  have "\<And>x. B x" by fact
wenzelm@42920
   454
wenzelm@42920
   455
next
wenzelm@42920
   456
wenzelm@42920
   457
  {
wenzelm@42920
   458
    assume A
wenzelm@42920
   459
    have B sorry
wenzelm@42920
   460
  }
wenzelm@42920
   461
  have "A \<Longrightarrow> B" by fact
wenzelm@42920
   462
wenzelm@42920
   463
next
wenzelm@42920
   464
wenzelm@42920
   465
  {
wenzelm@42920
   466
    def x \<equiv> t
wenzelm@42920
   467
    have "B x" sorry
wenzelm@42920
   468
  }
wenzelm@42920
   469
  have "B t" by fact
wenzelm@42920
   470
wenzelm@42920
   471
next
wenzelm@42920
   472
wenzelm@42920
   473
  {
wenzelm@42920
   474
    obtain x :: 'a where "B x" sorry
wenzelm@42920
   475
    have C sorry
wenzelm@42920
   476
  }
wenzelm@42920
   477
  have C by fact
wenzelm@42920
   478
wenzelm@42920
   479
end
wenzelm@42920
   480
wenzelm@42920
   481
wenzelm@42920
   482
subsection {* Pure rule composition *}
wenzelm@42920
   483
wenzelm@42920
   484
text {*
wenzelm@42920
   485
  The Pure framework provides means for:
wenzelm@42920
   486
wenzelm@42920
   487
  \begin{itemize}
wenzelm@42920
   488
wenzelm@42920
   489
    \item backward-chaining of rules by @{inference resolution}
wenzelm@42920
   490
wenzelm@42920
   491
    \item closing of branches by @{inference assumption}
wenzelm@42920
   492
wenzelm@42920
   493
  \end{itemize}
wenzelm@42920
   494
wenzelm@42920
   495
  Both principles involve higher-order unification of @{text \<lambda>}-terms
wenzelm@42920
   496
  modulo @{text "\<alpha>\<beta>\<eta>"}-equivalence (cf.\ Huet and Miller).  *}
wenzelm@42920
   497
wenzelm@42920
   498
notepad
wenzelm@42920
   499
begin
wenzelm@42920
   500
  assume a: A and b: B
wenzelm@42920
   501
  thm conjI
wenzelm@42920
   502
  thm conjI [of A B]  -- "instantiation"
wenzelm@42920
   503
  thm conjI [of A B, OF a b]  -- "instantiation and composition"
wenzelm@42920
   504
  thm conjI [OF a b]  -- "composition via unification (trivial)"
wenzelm@42920
   505
  thm conjI [OF `A` `B`]
wenzelm@42920
   506
wenzelm@42920
   507
  thm conjI [OF disjI1]
wenzelm@42920
   508
end
wenzelm@42920
   509
wenzelm@42920
   510
text {* Note: Low-level rule composition is tedious and leads to
wenzelm@42920
   511
  unreadable~/ unmaintainable expressions in the text.  *}
wenzelm@42920
   512
wenzelm@42920
   513
wenzelm@42920
   514
subsection {* Structured backward reasoning *}
wenzelm@42920
   515
wenzelm@42920
   516
text {* Idea: Canonical proof decomposition via @{command fix}~/
wenzelm@42920
   517
  @{command assume}~/ @{command show}, where the body produces a
wenzelm@42920
   518
  natural deduction rule to refine some goal.  *}
wenzelm@42920
   519
wenzelm@42920
   520
notepad
wenzelm@42920
   521
begin
wenzelm@42920
   522
  fix A B :: "'a \<Rightarrow> bool"
wenzelm@42920
   523
wenzelm@42920
   524
  have "\<And>x. A x \<Longrightarrow> B x"
wenzelm@42920
   525
  proof -
wenzelm@42920
   526
    fix x
wenzelm@42920
   527
    assume "A x"
wenzelm@42920
   528
    show "B x" sorry
wenzelm@42920
   529
  qed
wenzelm@42920
   530
wenzelm@42920
   531
  have "\<And>x. A x \<Longrightarrow> B x"
wenzelm@42920
   532
  proof -
wenzelm@42920
   533
    {
wenzelm@42920
   534
      fix x
wenzelm@42920
   535
      assume "A x"
wenzelm@42920
   536
      show "B x" sorry
wenzelm@42920
   537
    } -- "implicit block structure made explicit"
wenzelm@42920
   538
    note `\<And>x. A x \<Longrightarrow> B x`
wenzelm@42920
   539
      -- "side exit for the resulting rule"
wenzelm@42920
   540
  qed
wenzelm@42920
   541
end
wenzelm@42920
   542
wenzelm@42920
   543
wenzelm@42920
   544
subsection {* Structured rule application *}
wenzelm@42920
   545
wenzelm@42920
   546
text {*
wenzelm@42920
   547
  Idea: Previous facts and new claims are composed with a rule from
wenzelm@42920
   548
  the context (or background library).
wenzelm@42920
   549
*}
wenzelm@42920
   550
wenzelm@42920
   551
notepad
wenzelm@42920
   552
begin
wenzelm@42920
   553
  assume r1: "A \<Longrightarrow> B \<Longrightarrow> C"  -- {* simple rule (Horn clause) *}
wenzelm@42920
   554
wenzelm@42920
   555
  have A sorry  -- "prefix of facts via outer sub-proof"
wenzelm@42920
   556
  then have C
wenzelm@42920
   557
  proof (rule r1)
wenzelm@42920
   558
    show B sorry  -- "remaining rule premises via inner sub-proof"
wenzelm@42920
   559
  qed
wenzelm@42920
   560
wenzelm@42920
   561
  have C
wenzelm@42920
   562
  proof (rule r1)
wenzelm@42920
   563
    show A sorry
wenzelm@42920
   564
    show B sorry
wenzelm@42920
   565
  qed
wenzelm@42920
   566
wenzelm@42920
   567
  have A and B sorry
wenzelm@42920
   568
  then have C
wenzelm@42920
   569
  proof (rule r1)
wenzelm@42920
   570
  qed
wenzelm@42920
   571
wenzelm@42920
   572
  have A and B sorry
wenzelm@42920
   573
  then have C by (rule r1)
wenzelm@42920
   574
wenzelm@42920
   575
next
wenzelm@42920
   576
wenzelm@42920
   577
  assume r2: "A \<Longrightarrow> (\<And>x. B1 x \<Longrightarrow> B2 x) \<Longrightarrow> C"  -- {* nested rule *}
wenzelm@42920
   578
wenzelm@42920
   579
  have A sorry
wenzelm@42920
   580
  then have C
wenzelm@42920
   581
  proof (rule r2)
wenzelm@42920
   582
    fix x
wenzelm@42920
   583
    assume "B1 x"
wenzelm@42920
   584
    show "B2 x" sorry
wenzelm@42920
   585
  qed
wenzelm@42920
   586
wenzelm@42920
   587
  txt {* The compound rule premise @{prop "\<And>x. B1 x \<Longrightarrow> B2 x"} is better
wenzelm@42920
   588
    addressed via @{command fix}~/ @{command assume}~/ @{command show}
wenzelm@42920
   589
    in the nested proof body.  *}
wenzelm@42920
   590
end
wenzelm@42920
   591
wenzelm@42920
   592
wenzelm@42920
   593
subsection {* Example: predicate logic *}
wenzelm@42920
   594
wenzelm@42920
   595
text {*
wenzelm@42920
   596
  Using the above principles, standard introduction and elimination proofs
wenzelm@42920
   597
  of predicate logic connectives of HOL work as follows.
wenzelm@42920
   598
*}
wenzelm@42920
   599
wenzelm@42920
   600
notepad
wenzelm@42920
   601
begin
wenzelm@42920
   602
  have "A \<longrightarrow> B" and A sorry
wenzelm@42920
   603
  then have B ..
wenzelm@42920
   604
wenzelm@42920
   605
  have A sorry
wenzelm@42920
   606
  then have "A \<or> B" ..
wenzelm@42920
   607
wenzelm@42920
   608
  have B sorry
wenzelm@42920
   609
  then have "A \<or> B" ..
wenzelm@42920
   610
wenzelm@42920
   611
  have "A \<or> B" sorry
wenzelm@42920
   612
  then have C
wenzelm@42920
   613
  proof
wenzelm@42920
   614
    assume A
wenzelm@42920
   615
    then show C sorry
wenzelm@42920
   616
  next
wenzelm@42920
   617
    assume B
wenzelm@42920
   618
    then show C sorry
wenzelm@42920
   619
  qed
wenzelm@42920
   620
wenzelm@42920
   621
  have A and B sorry
wenzelm@42920
   622
  then have "A \<and> B" ..
wenzelm@42920
   623
wenzelm@42920
   624
  have "A \<and> B" sorry
wenzelm@42920
   625
  then have A ..
wenzelm@42920
   626
wenzelm@42920
   627
  have "A \<and> B" sorry
wenzelm@42920
   628
  then have B ..
wenzelm@42920
   629
wenzelm@42920
   630
  have False sorry
wenzelm@42920
   631
  then have A ..
wenzelm@42920
   632
wenzelm@42920
   633
  have True ..
wenzelm@42920
   634
wenzelm@42920
   635
  have "\<not> A"
wenzelm@42920
   636
  proof
wenzelm@42920
   637
    assume A
wenzelm@42920
   638
    then show False sorry
wenzelm@42920
   639
  qed
wenzelm@42920
   640
wenzelm@42920
   641
  have "\<not> A" and A sorry
wenzelm@42920
   642
  then have B ..
wenzelm@42920
   643
wenzelm@42920
   644
  have "\<forall>x. P x"
wenzelm@42920
   645
  proof
wenzelm@42920
   646
    fix x
wenzelm@42920
   647
    show "P x" sorry
wenzelm@42920
   648
  qed
wenzelm@42920
   649
wenzelm@42920
   650
  have "\<forall>x. P x" sorry
wenzelm@42920
   651
  then have "P a" ..
wenzelm@42920
   652
wenzelm@42920
   653
  have "\<exists>x. P x"
wenzelm@42920
   654
  proof
wenzelm@42920
   655
    show "P a" sorry
wenzelm@42920
   656
  qed
wenzelm@42920
   657
wenzelm@42920
   658
  have "\<exists>x. P x" sorry
wenzelm@42920
   659
  then have C
wenzelm@42920
   660
  proof
wenzelm@42920
   661
    fix a
wenzelm@42920
   662
    assume "P a"
wenzelm@42920
   663
    show C sorry
wenzelm@42920
   664
  qed
wenzelm@42920
   665
wenzelm@42920
   666
  txt {* Less awkward version using @{command obtain}: *}
wenzelm@42920
   667
  have "\<exists>x. P x" sorry
wenzelm@42920
   668
  then obtain a where "P a" ..
wenzelm@42920
   669
end
wenzelm@42920
   670
wenzelm@42920
   671
text {* Further variations to illustrate Isar sub-proofs involving
wenzelm@42920
   672
  @{command show}: *}
wenzelm@42920
   673
wenzelm@42920
   674
notepad
wenzelm@42920
   675
begin
wenzelm@42920
   676
  have "A \<and> B"
wenzelm@42920
   677
  proof  -- {* two strictly isolated subproofs *}
wenzelm@42920
   678
    show A sorry
wenzelm@42920
   679
  next
wenzelm@42920
   680
    show B sorry
wenzelm@42920
   681
  qed
wenzelm@42920
   682
wenzelm@42920
   683
  have "A \<and> B"
wenzelm@42920
   684
  proof  -- {* one simultaneous sub-proof *}
wenzelm@42920
   685
    show A and B sorry
wenzelm@42920
   686
  qed
wenzelm@42920
   687
wenzelm@42920
   688
  have "A \<and> B"
wenzelm@42920
   689
  proof  -- {* two subproofs in the same context *}
wenzelm@42920
   690
    show A sorry
wenzelm@42920
   691
    show B sorry
wenzelm@42920
   692
  qed
wenzelm@42920
   693
wenzelm@42920
   694
  have "A \<and> B"
wenzelm@42920
   695
  proof  -- {* swapped order *}
wenzelm@42920
   696
    show B sorry
wenzelm@42920
   697
    show A sorry
wenzelm@42920
   698
  qed
wenzelm@42920
   699
wenzelm@42920
   700
  have "A \<and> B"
wenzelm@42920
   701
  proof  -- {* sequential subproofs *}
wenzelm@42920
   702
    show A sorry
wenzelm@42920
   703
    show B using `A` sorry
wenzelm@42920
   704
  qed
wenzelm@42920
   705
end
wenzelm@42920
   706
wenzelm@42920
   707
wenzelm@42920
   708
subsubsection {* Example: set-theoretic operators *}
wenzelm@42920
   709
wenzelm@42920
   710
text {* There is nothing special about logical connectives (@{text
wenzelm@42920
   711
  "\<and>"}, @{text "\<or>"}, @{text "\<forall>"}, @{text "\<exists>"} etc.).  Operators from
wenzelm@42920
   712
  set-theory or lattice-theory for analogously.  It is only a matter
wenzelm@42920
   713
  of rule declarations in the library; rules can be also specified
wenzelm@42920
   714
  explicitly.
wenzelm@42920
   715
*}
wenzelm@42920
   716
wenzelm@42920
   717
notepad
wenzelm@42920
   718
begin
wenzelm@42920
   719
  have "x \<in> A" and "x \<in> B" sorry
wenzelm@42920
   720
  then have "x \<in> A \<inter> B" ..
wenzelm@42920
   721
wenzelm@42920
   722
  have "x \<in> A" sorry
wenzelm@42920
   723
  then have "x \<in> A \<union> B" ..
wenzelm@42920
   724
wenzelm@42920
   725
  have "x \<in> B" sorry
wenzelm@42920
   726
  then have "x \<in> A \<union> B" ..
wenzelm@42920
   727
wenzelm@42920
   728
  have "x \<in> A \<union> B" sorry
wenzelm@42920
   729
  then have C
wenzelm@42920
   730
  proof
wenzelm@42920
   731
    assume "x \<in> A"
wenzelm@42920
   732
    then show C sorry
wenzelm@42920
   733
  next
wenzelm@42920
   734
    assume "x \<in> B"
wenzelm@42920
   735
    then show C sorry
wenzelm@42920
   736
  qed
wenzelm@42920
   737
wenzelm@42920
   738
next
wenzelm@42920
   739
  have "x \<in> \<Inter>A"
wenzelm@42920
   740
  proof
wenzelm@42920
   741
    fix a
wenzelm@42920
   742
    assume "a \<in> A"
wenzelm@42920
   743
    show "x \<in> a" sorry
wenzelm@42920
   744
  qed
wenzelm@42920
   745
wenzelm@42920
   746
  have "x \<in> \<Inter>A" sorry
wenzelm@42920
   747
  then have "x \<in> a"
wenzelm@42920
   748
  proof
wenzelm@42920
   749
    show "a \<in> A" sorry
wenzelm@42920
   750
  qed
wenzelm@42920
   751
wenzelm@42920
   752
  have "a \<in> A" and "x \<in> a" sorry
wenzelm@42920
   753
  then have "x \<in> \<Union>A" ..
wenzelm@42920
   754
wenzelm@42920
   755
  have "x \<in> \<Union>A" sorry
wenzelm@42920
   756
  then obtain a where "a \<in> A" and "x \<in> a" ..
wenzelm@42920
   757
end
wenzelm@42920
   758
wenzelm@42917
   759
end