src/Doc/Isar_Ref/Framework.thy
author wenzelm
Wed Mar 25 11:39:52 2015 +0100 (2015-03-25)
changeset 59809 87641097d0f3
parent 58999 ed09ae4ea2d8
child 60618 4c79543cc376
permissions -rw-r--r--
tuned signature;
wenzelm@29716
     1
theory Framework
wenzelm@42651
     2
imports Base Main
wenzelm@29716
     3
begin
wenzelm@29716
     4
wenzelm@58618
     5
chapter \<open>The Isabelle/Isar Framework \label{ch:isar-framework}\<close>
wenzelm@29716
     6
wenzelm@58618
     7
text \<open>
wenzelm@58552
     8
  Isabelle/Isar @{cite "Wenzel:1999:TPHOL" and "Wenzel-PhD" and
wenzelm@58552
     9
  "Nipkow-TYPES02" and "Wenzel-Paulson:2006" and "Wenzel:2006:Festschrift"}
wenzelm@29716
    10
  is intended as a generic framework for developing formal
wenzelm@29716
    11
  mathematical documents with full proof checking.  Definitions and
wenzelm@29735
    12
  proofs are organized as theories.  An assembly of theory sources may
wenzelm@29716
    13
  be presented as a printed document; see also
wenzelm@29716
    14
  \chref{ch:document-prep}.
wenzelm@29716
    15
wenzelm@29716
    16
  The main objective of Isar is the design of a human-readable
wenzelm@29716
    17
  structured proof language, which is called the ``primary proof
wenzelm@29716
    18
  format'' in Isar terminology.  Such a primary proof language is
wenzelm@29716
    19
  somewhere in the middle between the extremes of primitive proof
wenzelm@29716
    20
  objects and actual natural language.  In this respect, Isar is a bit
wenzelm@58552
    21
  more formalistic than Mizar @{cite "Trybulec:1993:MizarFeatures" and
wenzelm@58552
    22
  "Rudnicki:1992:MizarOverview" and "Wiedijk:1999:Mizar"},
wenzelm@29716
    23
  using logical symbols for certain reasoning schemes where Mizar
wenzelm@58552
    24
  would prefer English words; see @{cite "Wenzel-Wiedijk:2002"} for
wenzelm@29716
    25
  further comparisons of these systems.
wenzelm@29716
    26
wenzelm@29716
    27
  So Isar challenges the traditional way of recording informal proofs
wenzelm@29716
    28
  in mathematical prose, as well as the common tendency to see fully
wenzelm@29716
    29
  formal proofs directly as objects of some logical calculus (e.g.\
wenzelm@29716
    30
  @{text "\<lambda>"}-terms in a version of type theory).  In fact, Isar is
wenzelm@29716
    31
  better understood as an interpreter of a simple block-structured
wenzelm@29735
    32
  language for describing the data flow of local facts and goals,
wenzelm@29716
    33
  interspersed with occasional invocations of proof methods.
wenzelm@29716
    34
  Everything is reduced to logical inferences internally, but these
wenzelm@29716
    35
  steps are somewhat marginal compared to the overall bookkeeping of
wenzelm@29716
    36
  the interpretation process.  Thanks to careful design of the syntax
wenzelm@29716
    37
  and semantics of Isar language elements, a formal record of Isar
wenzelm@29716
    38
  instructions may later appear as an intelligible text to the
wenzelm@29716
    39
  attentive reader.
wenzelm@29716
    40
wenzelm@29716
    41
  The Isar proof language has emerged from careful analysis of some
wenzelm@29716
    42
  inherent virtues of the existing logical framework of Isabelle/Pure
wenzelm@58552
    43
  @{cite "paulson-found" and "paulson700"}, notably composition of higher-order
wenzelm@29716
    44
  natural deduction rules, which is a generalization of Gentzen's
wenzelm@58552
    45
  original calculus @{cite "Gentzen:1935"}.  The approach of generic
wenzelm@29716
    46
  inference systems in Pure is continued by Isar towards actual proof
wenzelm@29716
    47
  texts.
wenzelm@29716
    48
wenzelm@29716
    49
  Concrete applications require another intermediate layer: an
wenzelm@58552
    50
  object-logic.  Isabelle/HOL @{cite "isa-tutorial"} (simply-typed
wenzelm@29716
    51
  set-theory) is being used most of the time; Isabelle/ZF
wenzelm@58552
    52
  @{cite "isabelle-ZF"} is less extensively developed, although it would
wenzelm@29716
    53
  probably fit better for classical mathematics.
wenzelm@29721
    54
wenzelm@29735
    55
  \medskip In order to illustrate natural deduction in Isar, we shall
wenzelm@29735
    56
  refer to the background theory and library of Isabelle/HOL.  This
wenzelm@29735
    57
  includes common notions of predicate logic, naive set-theory etc.\
wenzelm@29735
    58
  using fairly standard mathematical notation.  From the perspective
wenzelm@29735
    59
  of generic natural deduction there is nothing special about the
wenzelm@29735
    60
  logical connectives of HOL (@{text "\<and>"}, @{text "\<or>"}, @{text "\<forall>"},
wenzelm@29735
    61
  @{text "\<exists>"}, etc.), only the resulting reasoning principles are
wenzelm@29735
    62
  relevant to the user.  There are similar rules available for
wenzelm@29735
    63
  set-theory operators (@{text "\<inter>"}, @{text "\<union>"}, @{text "\<Inter>"}, @{text
wenzelm@29735
    64
  "\<Union>"}, etc.), or any other theory developed in the library (lattice
wenzelm@29735
    65
  theory, topology etc.).
wenzelm@29721
    66
wenzelm@29721
    67
  Subsequently we briefly review fragments of Isar proof texts
wenzelm@29735
    68
  corresponding directly to such general deduction schemes.  The
wenzelm@29735
    69
  examples shall refer to set-theory, to minimize the danger of
wenzelm@29721
    70
  understanding connectives of predicate logic as something special.
wenzelm@29721
    71
wenzelm@29721
    72
  \medskip The following deduction performs @{text "\<inter>"}-introduction,
wenzelm@29721
    73
  working forwards from assumptions towards the conclusion.  We give
wenzelm@29721
    74
  both the Isar text, and depict the primitive rule involved, as
wenzelm@29735
    75
  determined by unification of the problem against rules that are
wenzelm@29735
    76
  declared in the library context.
wenzelm@58618
    77
\<close>
wenzelm@29721
    78
wenzelm@58618
    79
text_raw \<open>\medskip\begin{minipage}{0.6\textwidth}\<close>
wenzelm@29721
    80
wenzelm@29721
    81
(*<*)
wenzelm@40964
    82
notepad
wenzelm@40964
    83
begin
wenzelm@29721
    84
(*>*)
wenzelm@29721
    85
    assume "x \<in> A" and "x \<in> B"
wenzelm@29721
    86
    then have "x \<in> A \<inter> B" ..
wenzelm@29721
    87
(*<*)
wenzelm@40964
    88
end
wenzelm@29721
    89
(*>*)
wenzelm@29721
    90
wenzelm@58618
    91
text_raw \<open>\end{minipage}\begin{minipage}{0.4\textwidth}\<close>
wenzelm@29721
    92
wenzelm@58618
    93
text \<open>
wenzelm@29721
    94
  \infer{@{prop "x \<in> A \<inter> B"}}{@{prop "x \<in> A"} & @{prop "x \<in> B"}}
wenzelm@58618
    95
\<close>
wenzelm@29721
    96
wenzelm@58618
    97
text_raw \<open>\end{minipage}\<close>
wenzelm@29721
    98
wenzelm@58618
    99
text \<open>
wenzelm@29737
   100
  \medskip\noindent Note that @{command assume} augments the proof
wenzelm@29737
   101
  context, @{command then} indicates that the current fact shall be
wenzelm@29737
   102
  used in the next step, and @{command have} states an intermediate
wenzelm@29735
   103
  goal.  The two dots ``@{command ".."}'' refer to a complete proof of
wenzelm@29735
   104
  this claim, using the indicated facts and a canonical rule from the
wenzelm@29721
   105
  context.  We could have been more explicit here by spelling out the
wenzelm@29721
   106
  final proof step via the @{command "by"} command:
wenzelm@58618
   107
\<close>
wenzelm@29721
   108
wenzelm@29721
   109
(*<*)
wenzelm@40964
   110
notepad
wenzelm@40964
   111
begin
wenzelm@29721
   112
(*>*)
wenzelm@29721
   113
    assume "x \<in> A" and "x \<in> B"
wenzelm@29721
   114
    then have "x \<in> A \<inter> B" by (rule IntI)
wenzelm@29721
   115
(*<*)
wenzelm@40964
   116
end
wenzelm@29721
   117
(*>*)
wenzelm@29721
   118
wenzelm@58618
   119
text \<open>
wenzelm@29721
   120
  \noindent The format of the @{text "\<inter>"}-introduction rule represents
wenzelm@29721
   121
  the most basic inference, which proceeds from given premises to a
wenzelm@29735
   122
  conclusion, without any nested proof context involved.
wenzelm@29721
   123
wenzelm@29735
   124
  The next example performs backwards introduction on @{term "\<Inter>\<A>"},
wenzelm@29735
   125
  the intersection of all sets within a given set.  This requires a
wenzelm@29735
   126
  nested proof of set membership within a local context, where @{term
wenzelm@29735
   127
  A} is an arbitrary-but-fixed member of the collection:
wenzelm@58618
   128
\<close>
wenzelm@29721
   129
wenzelm@58618
   130
text_raw \<open>\medskip\begin{minipage}{0.6\textwidth}\<close>
wenzelm@29721
   131
wenzelm@29721
   132
(*<*)
wenzelm@40964
   133
notepad
wenzelm@40964
   134
begin
wenzelm@29721
   135
(*>*)
wenzelm@29721
   136
    have "x \<in> \<Inter>\<A>"
wenzelm@29721
   137
    proof
wenzelm@29721
   138
      fix A
wenzelm@29721
   139
      assume "A \<in> \<A>"
wenzelm@29733
   140
      show "x \<in> A" sorry %noproof
wenzelm@29721
   141
    qed
wenzelm@29721
   142
(*<*)
wenzelm@40964
   143
end
wenzelm@29721
   144
(*>*)
wenzelm@29721
   145
wenzelm@58618
   146
text_raw \<open>\end{minipage}\begin{minipage}{0.4\textwidth}\<close>
wenzelm@29721
   147
wenzelm@58618
   148
text \<open>
wenzelm@29721
   149
  \infer{@{prop "x \<in> \<Inter>\<A>"}}{\infer*{@{prop "x \<in> A"}}{@{text "[A][A \<in> \<A>]"}}}
wenzelm@58618
   150
\<close>
wenzelm@29721
   151
wenzelm@58618
   152
text_raw \<open>\end{minipage}\<close>
wenzelm@29721
   153
wenzelm@58618
   154
text \<open>
wenzelm@29721
   155
  \medskip\noindent This Isar reasoning pattern again refers to the
wenzelm@29721
   156
  primitive rule depicted above.  The system determines it in the
wenzelm@56594
   157
  ``@{command proof}'' step, which could have been spelled out more
wenzelm@29737
   158
  explicitly as ``@{command proof}~@{text "(rule InterI)"}''.  Note
wenzelm@29735
   159
  that the rule involves both a local parameter @{term "A"} and an
wenzelm@29729
   160
  assumption @{prop "A \<in> \<A>"} in the nested reasoning.  This kind of
wenzelm@29729
   161
  compound rule typically demands a genuine sub-proof in Isar, working
wenzelm@29729
   162
  backwards rather than forwards as seen before.  In the proof body we
wenzelm@29737
   163
  encounter the @{command fix}-@{command assume}-@{command show}
wenzelm@29737
   164
  outline of nested sub-proofs that is typical for Isar.  The final
wenzelm@29737
   165
  @{command show} is like @{command have} followed by an additional
wenzelm@29737
   166
  refinement of the enclosing claim, using the rule derived from the
wenzelm@29737
   167
  proof body.
wenzelm@29721
   168
wenzelm@29721
   169
  \medskip The next example involves @{term "\<Union>\<A>"}, which can be
wenzelm@29721
   170
  characterized as the set of all @{term "x"} such that @{prop "\<exists>A. x
wenzelm@29721
   171
  \<in> A \<and> A \<in> \<A>"}.  The elimination rule for @{prop "x \<in> \<Union>\<A>"} does
wenzelm@29721
   172
  not mention @{text "\<exists>"} and @{text "\<and>"} at all, but admits to obtain
wenzelm@29721
   173
  directly a local @{term "A"} such that @{prop "x \<in> A"} and @{prop "A
wenzelm@29721
   174
  \<in> \<A>"} hold.  This corresponds to the following Isar proof and
wenzelm@29721
   175
  inference rule, respectively:
wenzelm@58618
   176
\<close>
wenzelm@29721
   177
wenzelm@58618
   178
text_raw \<open>\medskip\begin{minipage}{0.6\textwidth}\<close>
wenzelm@29721
   179
wenzelm@29721
   180
(*<*)
wenzelm@40964
   181
notepad
wenzelm@40964
   182
begin
wenzelm@29721
   183
(*>*)
wenzelm@29721
   184
    assume "x \<in> \<Union>\<A>"
wenzelm@29721
   185
    then have C
wenzelm@29721
   186
    proof
wenzelm@29721
   187
      fix A
wenzelm@29721
   188
      assume "x \<in> A" and "A \<in> \<A>"
wenzelm@29733
   189
      show C sorry %noproof
wenzelm@29721
   190
    qed
wenzelm@29721
   191
(*<*)
wenzelm@40964
   192
end
wenzelm@29721
   193
(*>*)
wenzelm@29721
   194
wenzelm@58618
   195
text_raw \<open>\end{minipage}\begin{minipage}{0.4\textwidth}\<close>
wenzelm@29721
   196
wenzelm@58618
   197
text \<open>
wenzelm@29721
   198
  \infer{@{prop "C"}}{@{prop "x \<in> \<Union>\<A>"} & \infer*{@{prop "C"}~}{@{text "[A][x \<in> A, A \<in> \<A>]"}}}
wenzelm@58618
   199
\<close>
wenzelm@29721
   200
wenzelm@58618
   201
text_raw \<open>\end{minipage}\<close>
wenzelm@29721
   202
wenzelm@58618
   203
text \<open>
wenzelm@29721
   204
  \medskip\noindent Although the Isar proof follows the natural
wenzelm@29721
   205
  deduction rule closely, the text reads not as natural as
wenzelm@29721
   206
  anticipated.  There is a double occurrence of an arbitrary
wenzelm@29721
   207
  conclusion @{prop "C"}, which represents the final result, but is
wenzelm@29721
   208
  irrelevant for now.  This issue arises for any elimination rule
wenzelm@29721
   209
  involving local parameters.  Isar provides the derived language
wenzelm@29737
   210
  element @{command obtain}, which is able to perform the same
wenzelm@29721
   211
  elimination proof more conveniently:
wenzelm@58618
   212
\<close>
wenzelm@29721
   213
wenzelm@29721
   214
(*<*)
wenzelm@40964
   215
notepad
wenzelm@40964
   216
begin
wenzelm@29721
   217
(*>*)
wenzelm@29721
   218
    assume "x \<in> \<Union>\<A>"
wenzelm@29721
   219
    then obtain A where "x \<in> A" and "A \<in> \<A>" ..
wenzelm@29721
   220
(*<*)
wenzelm@40964
   221
end
wenzelm@29721
   222
(*>*)
wenzelm@29721
   223
wenzelm@58618
   224
text \<open>
wenzelm@29721
   225
  \noindent Here we avoid to mention the final conclusion @{prop "C"}
wenzelm@29721
   226
  and return to plain forward reasoning.  The rule involved in the
wenzelm@29721
   227
  ``@{command ".."}'' proof is the same as before.
wenzelm@58618
   228
\<close>
wenzelm@29716
   229
wenzelm@29729
   230
wenzelm@58618
   231
section \<open>The Pure framework \label{sec:framework-pure}\<close>
wenzelm@29729
   232
wenzelm@58618
   233
text \<open>
wenzelm@58552
   234
  The Pure logic @{cite "paulson-found" and "paulson700"} is an intuitionistic
wenzelm@58552
   235
  fragment of higher-order logic @{cite "church40"}.  In type-theoretic
wenzelm@29729
   236
  parlance, there are three levels of @{text "\<lambda>"}-calculus with
wenzelm@29735
   237
  corresponding arrows @{text "\<Rightarrow>"}/@{text "\<And>"}/@{text "\<Longrightarrow>"}:
wenzelm@29735
   238
wenzelm@29735
   239
  \medskip
wenzelm@29735
   240
  \begin{tabular}{ll}
wenzelm@29735
   241
  @{text "\<alpha> \<Rightarrow> \<beta>"} & syntactic function space (terms depending on terms) \\
wenzelm@29735
   242
  @{text "\<And>x. B(x)"} & universal quantification (proofs depending on terms) \\
wenzelm@29735
   243
  @{text "A \<Longrightarrow> B"} & implication (proofs depending on proofs) \\
wenzelm@29735
   244
  \end{tabular}
wenzelm@29735
   245
  \medskip
wenzelm@29729
   246
wenzelm@29735
   247
  \noindent Here only the types of syntactic terms, and the
wenzelm@29735
   248
  propositions of proof terms have been shown.  The @{text
wenzelm@29735
   249
  "\<lambda>"}-structure of proofs can be recorded as an optional feature of
wenzelm@58552
   250
  the Pure inference kernel @{cite "Berghofer-Nipkow:2000:TPHOL"}, but
wenzelm@29735
   251
  the formal system can never depend on them due to \emph{proof
wenzelm@29735
   252
  irrelevance}.
wenzelm@29735
   253
wenzelm@29735
   254
  On top of this most primitive layer of proofs, Pure implements a
wenzelm@29735
   255
  generic calculus for nested natural deduction rules, similar to
wenzelm@58552
   256
  @{cite "Schroeder-Heister:1984"}.  Here object-logic inferences are
wenzelm@29735
   257
  internalized as formulae over @{text "\<And>"} and @{text "\<Longrightarrow>"}.
wenzelm@29735
   258
  Combining such rule statements may involve higher-order unification
wenzelm@58552
   259
  @{cite "paulson-natural"}.
wenzelm@58618
   260
\<close>
wenzelm@29729
   261
wenzelm@29729
   262
wenzelm@58618
   263
subsection \<open>Primitive inferences\<close>
wenzelm@29729
   264
wenzelm@58618
   265
text \<open>
wenzelm@29729
   266
  Term syntax provides explicit notation for abstraction @{text "\<lambda>x ::
wenzelm@29729
   267
  \<alpha>. b(x)"} and application @{text "b a"}, while types are usually
wenzelm@29729
   268
  implicit thanks to type-inference; terms of type @{text "prop"} are
wenzelm@29729
   269
  called propositions.  Logical statements are composed via @{text "\<And>x
wenzelm@29729
   270
  :: \<alpha>. B(x)"} and @{text "A \<Longrightarrow> B"}.  Primitive reasoning operates on
wenzelm@29729
   271
  judgments of the form @{text "\<Gamma> \<turnstile> \<phi>"}, with standard introduction
wenzelm@29729
   272
  and elimination rules for @{text "\<And>"} and @{text "\<Longrightarrow>"} that refer to
wenzelm@53015
   273
  fixed parameters @{text "x\<^sub>1, \<dots>, x\<^sub>m"} and hypotheses
wenzelm@53015
   274
  @{text "A\<^sub>1, \<dots>, A\<^sub>n"} from the context @{text "\<Gamma>"};
wenzelm@29729
   275
  the corresponding proof terms are left implicit.  The subsequent
wenzelm@29729
   276
  inference rules define @{text "\<Gamma> \<turnstile> \<phi>"} inductively, relative to a
wenzelm@29729
   277
  collection of axioms:
wenzelm@29729
   278
wenzelm@29729
   279
  \[
wenzelm@29729
   280
  \infer{@{text "\<turnstile> A"}}{(@{text "A"} \text{~axiom})}
wenzelm@29729
   281
  \qquad
wenzelm@29729
   282
  \infer{@{text "A \<turnstile> A"}}{}
wenzelm@29729
   283
  \]
wenzelm@29729
   284
wenzelm@29729
   285
  \[
wenzelm@29729
   286
  \infer{@{text "\<Gamma> \<turnstile> \<And>x. B(x)"}}{@{text "\<Gamma> \<turnstile> B(x)"} & @{text "x \<notin> \<Gamma>"}}
wenzelm@29729
   287
  \qquad
wenzelm@29729
   288
  \infer{@{text "\<Gamma> \<turnstile> B(a)"}}{@{text "\<Gamma> \<turnstile> \<And>x. B(x)"}}
wenzelm@29729
   289
  \]
wenzelm@29729
   290
wenzelm@29729
   291
  \[
wenzelm@29729
   292
  \infer{@{text "\<Gamma> - A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}}
wenzelm@29729
   293
  \qquad
wenzelm@29729
   294
  \infer{@{text "\<Gamma>\<^sub>1 \<union> \<Gamma>\<^sub>2 \<turnstile> B"}}{@{text "\<Gamma>\<^sub>1 \<turnstile> A \<Longrightarrow> B"} & @{text "\<Gamma>\<^sub>2 \<turnstile> A"}}
wenzelm@29729
   295
  \]
wenzelm@29729
   296
wenzelm@29729
   297
  Furthermore, Pure provides a built-in equality @{text "\<equiv> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow>
wenzelm@29729
   298
  prop"} with axioms for reflexivity, substitution, extensionality,
wenzelm@29729
   299
  and @{text "\<alpha>\<beta>\<eta>"}-conversion on @{text "\<lambda>"}-terms.
wenzelm@29729
   300
wenzelm@29729
   301
  \medskip An object-logic introduces another layer on top of Pure,
wenzelm@29729
   302
  e.g.\ with types @{text "i"} for individuals and @{text "o"} for
wenzelm@29729
   303
  propositions, term constants @{text "Trueprop :: o \<Rightarrow> prop"} as
wenzelm@29729
   304
  (implicit) derivability judgment and connectives like @{text "\<and> :: o
wenzelm@29729
   305
  \<Rightarrow> o \<Rightarrow> o"} or @{text "\<forall> :: (i \<Rightarrow> o) \<Rightarrow> o"}, and axioms for object-level
wenzelm@29729
   306
  rules such as @{text "conjI: A \<Longrightarrow> B \<Longrightarrow> A \<and> B"} or @{text "allI: (\<And>x. B
wenzelm@29729
   307
  x) \<Longrightarrow> \<forall>x. B x"}.  Derived object rules are represented as theorems of
wenzelm@29729
   308
  Pure.  After the initial object-logic setup, further axiomatizations
wenzelm@29729
   309
  are usually avoided; plain definitions and derived principles are
wenzelm@29729
   310
  used exclusively.
wenzelm@58618
   311
\<close>
wenzelm@29729
   312
wenzelm@29729
   313
wenzelm@58618
   314
subsection \<open>Reasoning with rules \label{sec:framework-resolution}\<close>
wenzelm@29729
   315
wenzelm@58618
   316
text \<open>
wenzelm@29729
   317
  Primitive inferences mostly serve foundational purposes.  The main
wenzelm@29729
   318
  reasoning mechanisms of Pure operate on nested natural deduction
wenzelm@29729
   319
  rules expressed as formulae, using @{text "\<And>"} to bind local
wenzelm@29729
   320
  parameters and @{text "\<Longrightarrow>"} to express entailment.  Multiple
wenzelm@29729
   321
  parameters and premises are represented by repeating these
wenzelm@29735
   322
  connectives in a right-associative manner.
wenzelm@29729
   323
wenzelm@29729
   324
  Since @{text "\<And>"} and @{text "\<Longrightarrow>"} commute thanks to the theorem
wenzelm@29729
   325
  @{prop "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}, we may assume w.l.o.g.\
wenzelm@29729
   326
  that rule statements always observe the normal form where
wenzelm@29729
   327
  quantifiers are pulled in front of implications at each level of
wenzelm@29729
   328
  nesting.  This means that any Pure proposition may be presented as a
wenzelm@58552
   329
  \emph{Hereditary Harrop Formula} @{cite "Miller:1991"} which is of the
wenzelm@53015
   330
  form @{text "\<And>x\<^sub>1 \<dots> x\<^sub>m. H\<^sub>1 \<Longrightarrow> \<dots> H\<^sub>n \<Longrightarrow>
wenzelm@29735
   331
  A"} for @{text "m, n \<ge> 0"}, and @{text "A"} atomic, and @{text
wenzelm@53015
   332
  "H\<^sub>1, \<dots>, H\<^sub>n"} being recursively of the same format.
wenzelm@29729
   333
  Following the convention that outermost quantifiers are implicit,
wenzelm@53015
   334
  Horn clauses @{text "A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> A"} are a special
wenzelm@29729
   335
  case of this.
wenzelm@29729
   336
wenzelm@29735
   337
  For example, @{text "\<inter>"}-introduction rule encountered before is
wenzelm@29735
   338
  represented as a Pure theorem as follows:
wenzelm@29735
   339
  \[
wenzelm@29735
   340
  @{text "IntI:"}~@{prop "x \<in> A \<Longrightarrow> x \<in> B \<Longrightarrow> x \<in> A \<inter> B"}
wenzelm@29735
   341
  \]
wenzelm@29735
   342
wenzelm@29735
   343
  \noindent This is a plain Horn clause, since no further nesting on
wenzelm@29735
   344
  the left is involved.  The general @{text "\<Inter>"}-introduction
wenzelm@29735
   345
  corresponds to a Hereditary Harrop Formula with one additional level
wenzelm@29735
   346
  of nesting:
wenzelm@29735
   347
  \[
wenzelm@29735
   348
  @{text "InterI:"}~@{prop "(\<And>A. A \<in> \<A> \<Longrightarrow> x \<in> A) \<Longrightarrow> x \<in> \<Inter>\<A>"}
wenzelm@29735
   349
  \]
wenzelm@29735
   350
wenzelm@53015
   351
  \medskip Goals are also represented as rules: @{text "A\<^sub>1 \<Longrightarrow>
wenzelm@53015
   352
  \<dots> A\<^sub>n \<Longrightarrow> C"} states that the sub-goals @{text "A\<^sub>1, \<dots>,
wenzelm@53015
   353
  A\<^sub>n"} entail the result @{text "C"}; for @{text "n = 0"} the
wenzelm@29729
   354
  goal is finished.  To allow @{text "C"} being a rule statement
wenzelm@29729
   355
  itself, we introduce the protective marker @{text "# :: prop \<Rightarrow>
wenzelm@29729
   356
  prop"}, which is defined as identity and hidden from the user.  We
wenzelm@29729
   357
  initialize and finish goal states as follows:
wenzelm@29729
   358
wenzelm@29729
   359
  \[
wenzelm@29729
   360
  \begin{array}{c@ {\qquad}c}
wenzelm@29729
   361
  \infer[(@{inference_def init})]{@{text "C \<Longrightarrow> #C"}}{} &
wenzelm@29729
   362
  \infer[(@{inference_def finish})]{@{text C}}{@{text "#C"}}
wenzelm@29729
   363
  \end{array}
wenzelm@29729
   364
  \]
wenzelm@29729
   365
wenzelm@29735
   366
  \noindent Goal states are refined in intermediate proof steps until
wenzelm@29735
   367
  a finished form is achieved.  Here the two main reasoning principles
wenzelm@29735
   368
  are @{inference resolution}, for back-chaining a rule against a
wenzelm@29735
   369
  sub-goal (replacing it by zero or more sub-goals), and @{inference
wenzelm@29729
   370
  assumption}, for solving a sub-goal (finding a short-circuit with
wenzelm@29729
   371
  local assumptions).  Below @{text "\<^vec>x"} stands for @{text
wenzelm@53015
   372
  "x\<^sub>1, \<dots>, x\<^sub>n"} (@{text "n \<ge> 0"}).
wenzelm@29729
   373
wenzelm@29729
   374
  \[
wenzelm@29729
   375
  \infer[(@{inference_def resolution})]
wenzelm@29729
   376
  {@{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> \<^vec>A (\<^vec>a \<^vec>x))\<vartheta> \<Longrightarrow> C\<vartheta>"}}
wenzelm@29729
   377
  {\begin{tabular}{rl}
wenzelm@29729
   378
    @{text "rule:"} &
wenzelm@29729
   379
    @{text "\<^vec>A \<^vec>a \<Longrightarrow> B \<^vec>a"} \\
wenzelm@29729
   380
    @{text "goal:"} &
wenzelm@29729
   381
    @{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> B' \<^vec>x) \<Longrightarrow> C"} \\
wenzelm@29729
   382
    @{text "goal unifier:"} &
wenzelm@29729
   383
    @{text "(\<lambda>\<^vec>x. B (\<^vec>a \<^vec>x))\<vartheta> = B'\<vartheta>"} \\
wenzelm@29729
   384
   \end{tabular}}
wenzelm@29729
   385
  \]
wenzelm@29729
   386
wenzelm@29729
   387
  \medskip
wenzelm@29729
   388
wenzelm@29729
   389
  \[
wenzelm@29729
   390
  \infer[(@{inference_def assumption})]{@{text "C\<vartheta>"}}
wenzelm@29729
   391
  {\begin{tabular}{rl}
wenzelm@29729
   392
    @{text "goal:"} &
wenzelm@29729
   393
    @{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> A \<^vec>x) \<Longrightarrow> C"} \\
wenzelm@29729
   394
    @{text "assm unifier:"} & @{text "A\<vartheta> = H\<^sub>i\<vartheta>"}~~\text{(for some~@{text "H\<^sub>i"})} \\
wenzelm@29729
   395
   \end{tabular}}
wenzelm@29729
   396
  \]
wenzelm@29729
   397
wenzelm@29729
   398
  The following trace illustrates goal-oriented reasoning in
wenzelm@29729
   399
  Isabelle/Pure:
wenzelm@29729
   400
wenzelm@29735
   401
  {\footnotesize
wenzelm@29729
   402
  \medskip
wenzelm@29735
   403
  \begin{tabular}{r@ {\quad}l}
wenzelm@29729
   404
  @{text "(A \<and> B \<Longrightarrow> B \<and> A) \<Longrightarrow> #(A \<and> B \<Longrightarrow> B \<and> A)"} & @{text "(init)"} \\
wenzelm@29729
   405
  @{text "(A \<and> B \<Longrightarrow> B) \<Longrightarrow> (A \<and> B \<Longrightarrow> A) \<Longrightarrow> #\<dots>"} & @{text "(resolution B \<Longrightarrow> A \<Longrightarrow> B \<and> A)"} \\
wenzelm@29729
   406
  @{text "(A \<and> B \<Longrightarrow> A \<and> B) \<Longrightarrow> (A \<and> B \<Longrightarrow> A) \<Longrightarrow> #\<dots>"} & @{text "(resolution A \<and> B \<Longrightarrow> B)"} \\
wenzelm@29729
   407
  @{text "(A \<and> B \<Longrightarrow> A) \<Longrightarrow> #\<dots>"} & @{text "(assumption)"} \\
wenzelm@48279
   408
  @{text "(A \<and> B \<Longrightarrow> A \<and> B) \<Longrightarrow> #\<dots>"} & @{text "(resolution A \<and> B \<Longrightarrow> A)"} \\
wenzelm@29729
   409
  @{text "#\<dots>"} & @{text "(assumption)"} \\
wenzelm@29729
   410
  @{text "A \<and> B \<Longrightarrow> B \<and> A"} & @{text "(finish)"} \\
wenzelm@29729
   411
  \end{tabular}
wenzelm@29729
   412
  \medskip
wenzelm@29735
   413
  }
wenzelm@29729
   414
wenzelm@29729
   415
  Compositions of @{inference assumption} after @{inference
wenzelm@29729
   416
  resolution} occurs quite often, typically in elimination steps.
wenzelm@29729
   417
  Traditional Isabelle tactics accommodate this by a combined
wenzelm@29729
   418
  @{inference_def elim_resolution} principle.  In contrast, Isar uses
wenzelm@29729
   419
  a slightly more refined combination, where the assumptions to be
wenzelm@29729
   420
  closed are marked explicitly, using again the protective marker
wenzelm@29729
   421
  @{text "#"}:
wenzelm@29729
   422
wenzelm@29729
   423
  \[
wenzelm@29729
   424
  \infer[(@{inference refinement})]
wenzelm@29729
   425
  {@{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> \<^vec>G' (\<^vec>a \<^vec>x))\<vartheta> \<Longrightarrow> C\<vartheta>"}}
wenzelm@29729
   426
  {\begin{tabular}{rl}
wenzelm@42666
   427
    @{text "sub\<hyphen>proof:"} &
wenzelm@29729
   428
    @{text "\<^vec>G \<^vec>a \<Longrightarrow> B \<^vec>a"} \\
wenzelm@29729
   429
    @{text "goal:"} &
wenzelm@29729
   430
    @{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> B' \<^vec>x) \<Longrightarrow> C"} \\
wenzelm@29729
   431
    @{text "goal unifier:"} &
wenzelm@29729
   432
    @{text "(\<lambda>\<^vec>x. B (\<^vec>a \<^vec>x))\<vartheta> = B'\<vartheta>"} \\
wenzelm@29729
   433
    @{text "assm unifiers:"} &
wenzelm@29729
   434
    @{text "(\<lambda>\<^vec>x. G\<^sub>j (\<^vec>a \<^vec>x))\<vartheta> = #H\<^sub>i\<vartheta>"} \\
wenzelm@29729
   435
    & \quad (for each marked @{text "G\<^sub>j"} some @{text "#H\<^sub>i"}) \\
wenzelm@29729
   436
   \end{tabular}}
wenzelm@29729
   437
  \]
wenzelm@29729
   438
wenzelm@42666
   439
  \noindent Here the @{text "sub\<hyphen>proof"} rule stems from the
wenzelm@29737
   440
  main @{command fix}-@{command assume}-@{command show} outline of
wenzelm@29737
   441
  Isar (cf.\ \secref{sec:framework-subproof}): each assumption
wenzelm@29729
   442
  indicated in the text results in a marked premise @{text "G"} above.
wenzelm@29735
   443
  The marking enforces resolution against one of the sub-goal's
wenzelm@29737
   444
  premises.  Consequently, @{command fix}-@{command assume}-@{command
wenzelm@29737
   445
  show} enables to fit the result of a sub-proof quite robustly into a
wenzelm@29737
   446
  pending sub-goal, while maintaining a good measure of flexibility.
wenzelm@58618
   447
\<close>
wenzelm@29729
   448
wenzelm@29729
   449
wenzelm@58618
   450
section \<open>The Isar proof language \label{sec:framework-isar}\<close>
wenzelm@29729
   451
wenzelm@58618
   452
text \<open>
wenzelm@29729
   453
  Structured proofs are presented as high-level expressions for
wenzelm@29729
   454
  composing entities of Pure (propositions, facts, and goals).  The
wenzelm@29729
   455
  Isar proof language allows to organize reasoning within the
wenzelm@29729
   456
  underlying rule calculus of Pure, but Isar is not another logical
wenzelm@29729
   457
  calculus!
wenzelm@29729
   458
wenzelm@29729
   459
  Isar is an exercise in sound minimalism.  Approximately half of the
wenzelm@29729
   460
  language is introduced as primitive, the rest defined as derived
wenzelm@29729
   461
  concepts.  The following grammar describes the core language
wenzelm@29729
   462
  (category @{text "proof"}), which is embedded into theory
wenzelm@29729
   463
  specification elements such as @{command theorem}; see also
wenzelm@29729
   464
  \secref{sec:framework-stmt} for the separate category @{text
wenzelm@29729
   465
  "statement"}.
wenzelm@29729
   466
wenzelm@29729
   467
  \medskip
wenzelm@29729
   468
  \begin{tabular}{rcl}
wenzelm@42666
   469
    @{text "theory\<hyphen>stmt"} & = & @{command "theorem"}~@{text "statement proof  |"}~~@{command "definition"}~@{text "\<dots>  |  \<dots>"} \\[1ex]
wenzelm@29729
   470
wenzelm@29729
   471
    @{text "proof"} & = & @{text "prfx\<^sup>*"}~@{command "proof"}~@{text "method\<^sup>? stmt\<^sup>*"}~@{command "qed"}~@{text "method\<^sup>?"} \\[1ex]
wenzelm@29729
   472
wenzelm@29729
   473
    @{text prfx} & = & @{command "using"}~@{text "facts"} \\
wenzelm@29729
   474
    & @{text "|"} & @{command "unfolding"}~@{text "facts"} \\
wenzelm@29729
   475
wenzelm@29729
   476
    @{text stmt} & = & @{command "{"}~@{text "stmt\<^sup>*"}~@{command "}"} \\
wenzelm@29729
   477
    & @{text "|"} & @{command "next"} \\
wenzelm@29729
   478
    & @{text "|"} & @{command "note"}~@{text "name = facts"} \\
wenzelm@29729
   479
    & @{text "|"} & @{command "let"}~@{text "term = term"} \\
wenzelm@29729
   480
    & @{text "|"} & @{command "fix"}~@{text "var\<^sup>+"} \\
wenzelm@29737
   481
    & @{text "|"} & @{command assume}~@{text "\<guillemotleft>inference\<guillemotright> name: props"} \\
wenzelm@29729
   482
    & @{text "|"} & @{command "then"}@{text "\<^sup>?"}~@{text goal} \\
wenzelm@29729
   483
    @{text goal} & = & @{command "have"}~@{text "name: props proof"} \\
wenzelm@29729
   484
    & @{text "|"} & @{command "show"}~@{text "name: props proof"} \\
wenzelm@29729
   485
  \end{tabular}
wenzelm@29729
   486
wenzelm@29729
   487
  \medskip Simultaneous propositions or facts may be separated by the
wenzelm@29729
   488
  @{keyword "and"} keyword.
wenzelm@29729
   489
wenzelm@29729
   490
  \medskip The syntax for terms and propositions is inherited from
wenzelm@29729
   491
  Pure (and the object-logic).  A @{text "pattern"} is a @{text
wenzelm@29729
   492
  "term"} with schematic variables, to be bound by higher-order
wenzelm@29729
   493
  matching.
wenzelm@29729
   494
wenzelm@29735
   495
  \medskip Facts may be referenced by name or proposition.  For
wenzelm@29737
   496
  example, the result of ``@{command have}~@{text "a: A \<langle>proof\<rangle>"}''
wenzelm@29735
   497
  becomes available both as @{text "a"} and
wenzelm@29735
   498
  \isacharbackquoteopen@{text "A"}\isacharbackquoteclose.  Moreover,
wenzelm@29735
   499
  fact expressions may involve attributes that modify either the
wenzelm@29735
   500
  theorem or the background context.  For example, the expression
wenzelm@29735
   501
  ``@{text "a [OF b]"}'' refers to the composition of two facts
wenzelm@29735
   502
  according to the @{inference resolution} inference of
wenzelm@29735
   503
  \secref{sec:framework-resolution}, while ``@{text "a [intro]"}''
wenzelm@29735
   504
  declares a fact as introduction rule in the context.
wenzelm@29729
   505
wenzelm@29735
   506
  The special fact called ``@{fact this}'' always refers to the last
wenzelm@29737
   507
  result, as produced by @{command note}, @{command assume}, @{command
wenzelm@29737
   508
  have}, or @{command show}.  Since @{command note} occurs
wenzelm@29737
   509
  frequently together with @{command then} we provide some
wenzelm@29737
   510
  abbreviations:
wenzelm@29729
   511
wenzelm@29737
   512
  \medskip
wenzelm@29737
   513
  \begin{tabular}{rcl}
wenzelm@29737
   514
    @{command from}~@{text a} & @{text "\<equiv>"} & @{command note}~@{text a}~@{command then} \\
wenzelm@29737
   515
    @{command with}~@{text a} & @{text "\<equiv>"} & @{command from}~@{text "a \<AND> this"} \\
wenzelm@29737
   516
  \end{tabular}
wenzelm@29737
   517
  \medskip
wenzelm@29737
   518
wenzelm@29737
   519
  The @{text "method"} category is essentially a parameter and may be
wenzelm@29737
   520
  populated later.  Methods use the facts indicated by @{command
wenzelm@29737
   521
  "then"} or @{command using}, and then operate on the goal state.
wenzelm@29737
   522
  Some basic methods are predefined: ``@{method "-"}'' leaves the goal
wenzelm@29737
   523
  unchanged, ``@{method this}'' applies the facts as rules to the
wenzelm@42626
   524
  goal, ``@{method (Pure) "rule"}'' applies the facts to another rule and the
wenzelm@42626
   525
  result to the goal (both ``@{method this}'' and ``@{method (Pure) rule}''
wenzelm@29737
   526
  refer to @{inference resolution} of
wenzelm@29729
   527
  \secref{sec:framework-resolution}).  The secondary arguments to
wenzelm@42626
   528
  ``@{method (Pure) rule}'' may be specified explicitly as in ``@{text "(rule
wenzelm@29729
   529
  a)"}'', or picked from the context.  In the latter case, the system
wenzelm@29729
   530
  first tries rules declared as @{attribute (Pure) elim} or
wenzelm@29729
   531
  @{attribute (Pure) dest}, followed by those declared as @{attribute
wenzelm@29729
   532
  (Pure) intro}.
wenzelm@29729
   533
wenzelm@42626
   534
  The default method for @{command proof} is ``@{method (Pure) rule}''
wenzelm@29737
   535
  (arguments picked from the context), for @{command qed} it is
wenzelm@29729
   536
  ``@{method "-"}''.  Further abbreviations for terminal proof steps
wenzelm@29729
   537
  are ``@{command "by"}~@{text "method\<^sub>1 method\<^sub>2"}'' for
wenzelm@29737
   538
  ``@{command proof}~@{text "method\<^sub>1"}~@{command qed}~@{text
wenzelm@29737
   539
  "method\<^sub>2"}'', and ``@{command ".."}'' for ``@{command
wenzelm@42626
   540
  "by"}~@{method (Pure) rule}, and ``@{command "."}'' for ``@{command
wenzelm@29737
   541
  "by"}~@{method this}''.  The @{command unfolding} element operates
wenzelm@29737
   542
  directly on the current facts and goal by applying equalities.
wenzelm@29729
   543
wenzelm@29737
   544
  \medskip Block structure can be indicated explicitly by ``@{command
wenzelm@29737
   545
  "{"}~@{text "\<dots>"}~@{command "}"}'', although the body of a sub-proof
wenzelm@29737
   546
  already involves implicit nesting.  In any case, @{command next}
wenzelm@29737
   547
  jumps into the next section of a block, i.e.\ it acts like closing
wenzelm@29737
   548
  an implicit block scope and opening another one; there is no direct
wenzelm@29737
   549
  correspondence to subgoals here.
wenzelm@29729
   550
wenzelm@29737
   551
  The remaining elements @{command fix} and @{command assume} build up
wenzelm@29737
   552
  a local context (see \secref{sec:framework-context}), while
wenzelm@29737
   553
  @{command show} refines a pending sub-goal by the rule resulting
wenzelm@29729
   554
  from a nested sub-proof (see \secref{sec:framework-subproof}).
wenzelm@29729
   555
  Further derived concepts will support calculational reasoning (see
wenzelm@29729
   556
  \secref{sec:framework-calc}).
wenzelm@58618
   557
\<close>
wenzelm@29729
   558
wenzelm@29729
   559
wenzelm@58618
   560
subsection \<open>Context elements \label{sec:framework-context}\<close>
wenzelm@29729
   561
wenzelm@58618
   562
text \<open>
wenzelm@29729
   563
  In judgments @{text "\<Gamma> \<turnstile> \<phi>"} of the primitive framework, @{text "\<Gamma>"}
wenzelm@29729
   564
  essentially acts like a proof context.  Isar elaborates this idea
wenzelm@29735
   565
  towards a higher-level notion, with additional information for
wenzelm@29729
   566
  type-inference, term abbreviations, local facts, hypotheses etc.
wenzelm@29729
   567
wenzelm@29737
   568
  The element @{command fix}~@{text "x :: \<alpha>"} declares a local
wenzelm@29729
   569
  parameter, i.e.\ an arbitrary-but-fixed entity of a given type; in
wenzelm@29729
   570
  results exported from the context, @{text "x"} may become anything.
wenzelm@29737
   571
  The @{command assume}~@{text "\<guillemotleft>inference\<guillemotright>"} element provides a
wenzelm@29737
   572
  general interface to hypotheses: ``@{command assume}~@{text
wenzelm@29737
   573
  "\<guillemotleft>inference\<guillemotright> A"}'' produces @{text "A \<turnstile> A"} locally, while the
wenzelm@29737
   574
  included inference tells how to discharge @{text A} from results
wenzelm@29737
   575
  @{text "A \<turnstile> B"} later on.  There is no user-syntax for @{text
wenzelm@29737
   576
  "\<guillemotleft>inference\<guillemotright>"}, i.e.\ it may only occur internally when derived
wenzelm@29737
   577
  commands are defined in ML.
wenzelm@29737
   578
wenzelm@29737
   579
  At the user-level, the default inference for @{command assume} is
wenzelm@29737
   580
  @{inference discharge} as given below.  The additional variants
wenzelm@29737
   581
  @{command presume} and @{command def} are defined as follows:
wenzelm@29737
   582
wenzelm@29737
   583
  \medskip
wenzelm@29737
   584
  \begin{tabular}{rcl}
wenzelm@42666
   585
    @{command presume}~@{text A} & @{text "\<equiv>"} & @{command assume}~@{text "\<guillemotleft>weak\<hyphen>discharge\<guillemotright> A"} \\
wenzelm@29737
   586
    @{command def}~@{text "x \<equiv> a"} & @{text "\<equiv>"} & @{command fix}~@{text x}~@{command assume}~@{text "\<guillemotleft>expansion\<guillemotright> x \<equiv> a"} \\
wenzelm@29737
   587
  \end{tabular}
wenzelm@29737
   588
  \medskip
wenzelm@29729
   589
wenzelm@29729
   590
  \[
wenzelm@29737
   591
  \infer[(@{inference_def discharge})]{@{text "\<strut>\<Gamma> - A \<turnstile> #A \<Longrightarrow> B"}}{@{text "\<strut>\<Gamma> \<turnstile> B"}}
wenzelm@29737
   592
  \]
wenzelm@29737
   593
  \[
wenzelm@42666
   594
  \infer[(@{inference_def "weak\<hyphen>discharge"})]{@{text "\<strut>\<Gamma> - A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<strut>\<Gamma> \<turnstile> B"}}
wenzelm@29737
   595
  \]
wenzelm@29737
   596
  \[
wenzelm@29729
   597
  \infer[(@{inference_def expansion})]{@{text "\<strut>\<Gamma> - (x \<equiv> a) \<turnstile> B a"}}{@{text "\<strut>\<Gamma> \<turnstile> B x"}}
wenzelm@29729
   598
  \]
wenzelm@29729
   599
wenzelm@29737
   600
  \medskip Note that @{inference discharge} and @{inference
wenzelm@42666
   601
  "weak\<hyphen>discharge"} differ in the marker for @{prop A}, which is
wenzelm@29737
   602
  relevant when the result of a @{command fix}-@{command
wenzelm@29737
   603
  assume}-@{command show} outline is composed with a pending goal,
wenzelm@29737
   604
  cf.\ \secref{sec:framework-subproof}.
wenzelm@29729
   605
wenzelm@29737
   606
  The most interesting derived context element in Isar is @{command
wenzelm@58552
   607
  obtain} @{cite \<open>\S5.3\<close> "Wenzel-PhD"}, which supports generalized
wenzelm@29737
   608
  elimination steps in a purely forward manner.  The @{command obtain}
wenzelm@29739
   609
  command takes a specification of parameters @{text "\<^vec>x"} and
wenzelm@29737
   610
  assumptions @{text "\<^vec>A"} to be added to the context, together
wenzelm@29737
   611
  with a proof of a case rule stating that this extension is
wenzelm@29737
   612
  conservative (i.e.\ may be removed from closed results later on):
wenzelm@29729
   613
wenzelm@29729
   614
  \medskip
wenzelm@29729
   615
  \begin{tabular}{l}
wenzelm@29729
   616
  @{text "\<langle>facts\<rangle>"}~~@{command obtain}~@{text "\<^vec>x \<WHERE> \<^vec>A \<^vec>x  \<langle>proof\<rangle> \<equiv>"} \\[0.5ex]
wenzelm@29729
   617
  \quad @{command have}~@{text "case: \<And>thesis. (\<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis) \<Longrightarrow> thesis\<rangle>"} \\
wenzelm@29729
   618
  \quad @{command proof}~@{method "-"} \\
wenzelm@29729
   619
  \qquad @{command fix}~@{text thesis} \\
wenzelm@29729
   620
  \qquad @{command assume}~@{text "[intro]: \<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis"} \\
wenzelm@29733
   621
  \qquad @{command show}~@{text thesis}~@{command using}~@{text "\<langle>facts\<rangle> \<langle>proof\<rangle>"} \\
wenzelm@29729
   622
  \quad @{command qed} \\
wenzelm@29737
   623
  \quad @{command fix}~@{text "\<^vec>x"}~@{command assume}~@{text "\<guillemotleft>elimination case\<guillemotright> \<^vec>A \<^vec>x"} \\
wenzelm@29729
   624
  \end{tabular}
wenzelm@29729
   625
  \medskip
wenzelm@29729
   626
wenzelm@29729
   627
  \[
wenzelm@29729
   628
  \infer[(@{inference elimination})]{@{text "\<Gamma> \<turnstile> B"}}{
wenzelm@29729
   629
    \begin{tabular}{rl}
wenzelm@29729
   630
    @{text "case:"} &
wenzelm@29729
   631
    @{text "\<Gamma> \<turnstile> \<And>thesis. (\<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis) \<Longrightarrow> thesis"} \\[0.2ex]
wenzelm@29729
   632
    @{text "result:"} &
wenzelm@29729
   633
    @{text "\<Gamma> \<union> \<^vec>A \<^vec>y \<turnstile> B"} \\[0.2ex]
wenzelm@29729
   634
    \end{tabular}}
wenzelm@29729
   635
  \]
wenzelm@29729
   636
wenzelm@29729
   637
  \noindent Here the name ``@{text thesis}'' is a specific convention
wenzelm@29729
   638
  for an arbitrary-but-fixed proposition; in the primitive natural
wenzelm@29729
   639
  deduction rules shown before we have occasionally used @{text C}.
wenzelm@29737
   640
  The whole statement of ``@{command obtain}~@{text x}~@{keyword
wenzelm@29729
   641
  "where"}~@{text "A x"}'' may be read as a claim that @{text "A x"}
wenzelm@29729
   642
  may be assumed for some arbitrary-but-fixed @{text "x"}.  Also note
wenzelm@29737
   643
  that ``@{command obtain}~@{text "A \<AND> B"}'' without parameters
wenzelm@29737
   644
  is similar to ``@{command have}~@{text "A \<AND> B"}'', but the
wenzelm@29737
   645
  latter involves multiple sub-goals.
wenzelm@29729
   646
wenzelm@29729
   647
  \medskip The subsequent Isar proof texts explain all context
wenzelm@29729
   648
  elements introduced above using the formal proof language itself.
wenzelm@29729
   649
  After finishing a local proof within a block, we indicate the
wenzelm@29739
   650
  exported result via @{command note}.
wenzelm@58618
   651
\<close>
wenzelm@29729
   652
wenzelm@29729
   653
(*<*)
wenzelm@29729
   654
theorem True
wenzelm@29729
   655
proof
wenzelm@29729
   656
(*>*)
wenzelm@58999
   657
  text_raw \<open>\begin{minipage}[t]{0.45\textwidth}\<close>
wenzelm@29729
   658
  {
wenzelm@29729
   659
    fix x
wenzelm@29735
   660
    have "B x" sorry %noproof
wenzelm@29729
   661
  }
wenzelm@58618
   662
  note \<open>\<And>x. B x\<close>
wenzelm@58999
   663
  text_raw \<open>\end{minipage}\quad\begin{minipage}[t]{0.45\textwidth}\<close>(*<*)next(*>*)
wenzelm@29735
   664
  {
wenzelm@29735
   665
    assume A
wenzelm@29735
   666
    have B sorry %noproof
wenzelm@29735
   667
  }
wenzelm@58618
   668
  note \<open>A \<Longrightarrow> B\<close>
wenzelm@58999
   669
  text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.45\textwidth}\<close>(*<*)next(*>*)
wenzelm@29729
   670
  {
wenzelm@29729
   671
    def x \<equiv> a
wenzelm@29735
   672
    have "B x" sorry %noproof
wenzelm@29729
   673
  }
wenzelm@58618
   674
  note \<open>B a\<close>
wenzelm@58999
   675
  text_raw \<open>\end{minipage}\quad\begin{minipage}[t]{0.45\textwidth}\<close>(*<*)next(*>*)
wenzelm@29729
   676
  {
wenzelm@29735
   677
    obtain x where "A x" sorry %noproof
wenzelm@29733
   678
    have B sorry %noproof
wenzelm@29729
   679
  }
wenzelm@58618
   680
  note \<open>B\<close>
wenzelm@58999
   681
  text_raw \<open>\end{minipage}\<close>
wenzelm@29729
   682
(*<*)
wenzelm@29729
   683
qed
wenzelm@29729
   684
(*>*)
wenzelm@29729
   685
wenzelm@58618
   686
text \<open>
wenzelm@29739
   687
  \bigskip\noindent This illustrates the meaning of Isar context
wenzelm@29739
   688
  elements without goals getting in between.
wenzelm@58618
   689
\<close>
wenzelm@29729
   690
wenzelm@58618
   691
subsection \<open>Structured statements \label{sec:framework-stmt}\<close>
wenzelm@29729
   692
wenzelm@58618
   693
text \<open>
wenzelm@29729
   694
  The category @{text "statement"} of top-level theorem specifications
wenzelm@29729
   695
  is defined as follows:
wenzelm@29729
   696
wenzelm@29729
   697
  \medskip
wenzelm@29729
   698
  \begin{tabular}{rcl}
wenzelm@29729
   699
  @{text "statement"} & @{text "\<equiv>"} & @{text "name: props \<AND> \<dots>"} \\
wenzelm@29729
   700
  & @{text "|"} & @{text "context\<^sup>* conclusion"} \\[0.5ex]
wenzelm@29729
   701
wenzelm@29729
   702
  @{text "context"} & @{text "\<equiv>"} & @{text "\<FIXES> vars \<AND> \<dots>"} \\
wenzelm@29729
   703
  & @{text "|"} & @{text "\<ASSUMES> name: props \<AND> \<dots>"} \\
wenzelm@29729
   704
wenzelm@29729
   705
  @{text "conclusion"} & @{text "\<equiv>"} & @{text "\<SHOWS> name: props \<AND> \<dots>"} \\
wenzelm@29735
   706
  & @{text "|"} & @{text "\<OBTAINS> vars \<AND> \<dots> \<WHERE> name: props \<AND> \<dots>"} \\
wenzelm@29735
   707
  & & \quad @{text "\<BBAR> \<dots>"} \\
wenzelm@29729
   708
  \end{tabular}
wenzelm@29729
   709
wenzelm@29729
   710
  \medskip\noindent A simple @{text "statement"} consists of named
wenzelm@29729
   711
  propositions.  The full form admits local context elements followed
wenzelm@29729
   712
  by the actual conclusions, such as ``@{keyword "fixes"}~@{text
wenzelm@29729
   713
  x}~@{keyword "assumes"}~@{text "A x"}~@{keyword "shows"}~@{text "B
wenzelm@29729
   714
  x"}''.  The final result emerges as a Pure rule after discharging
wenzelm@29729
   715
  the context: @{prop "\<And>x. A x \<Longrightarrow> B x"}.
wenzelm@29729
   716
wenzelm@29729
   717
  The @{keyword "obtains"} variant is another abbreviation defined
wenzelm@29729
   718
  below; unlike @{command obtain} (cf.\
wenzelm@29729
   719
  \secref{sec:framework-context}) there may be several ``cases''
wenzelm@29729
   720
  separated by ``@{text "\<BBAR>"}'', each consisting of several
wenzelm@29729
   721
  parameters (@{text "vars"}) and several premises (@{text "props"}).
wenzelm@29729
   722
  This specifies multi-branch elimination rules.
wenzelm@29729
   723
wenzelm@29729
   724
  \medskip
wenzelm@29729
   725
  \begin{tabular}{l}
wenzelm@29729
   726
  @{text "\<OBTAINS> \<^vec>x \<WHERE> \<^vec>A \<^vec>x   \<BBAR>   \<dots>   \<equiv>"} \\[0.5ex]
wenzelm@29729
   727
  \quad @{text "\<FIXES> thesis"} \\
wenzelm@29729
   728
  \quad @{text "\<ASSUMES> [intro]: \<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis  \<AND>  \<dots>"} \\
wenzelm@29729
   729
  \quad @{text "\<SHOWS> thesis"} \\
wenzelm@29729
   730
  \end{tabular}
wenzelm@29729
   731
  \medskip
wenzelm@29729
   732
wenzelm@29729
   733
  Presenting structured statements in such an ``open'' format usually
wenzelm@29729
   734
  simplifies the subsequent proof, because the outer structure of the
wenzelm@29729
   735
  problem is already laid out directly.  E.g.\ consider the following
wenzelm@29729
   736
  canonical patterns for @{text "\<SHOWS>"} and @{text "\<OBTAINS>"},
wenzelm@29729
   737
  respectively:
wenzelm@58618
   738
\<close>
wenzelm@29729
   739
wenzelm@58618
   740
text_raw \<open>\begin{minipage}{0.5\textwidth}\<close>
wenzelm@29729
   741
wenzelm@29729
   742
theorem
wenzelm@29729
   743
  fixes x and y
wenzelm@29729
   744
  assumes "A x" and "B y"
wenzelm@29729
   745
  shows "C x y"
wenzelm@29729
   746
proof -
wenzelm@58618
   747
  from \<open>A x\<close> and \<open>B y\<close>
wenzelm@29733
   748
  show "C x y" sorry %noproof
wenzelm@29729
   749
qed
wenzelm@29729
   750
wenzelm@58618
   751
text_raw \<open>\end{minipage}\begin{minipage}{0.5\textwidth}\<close>
wenzelm@29729
   752
wenzelm@29729
   753
theorem
wenzelm@29729
   754
  obtains x and y
wenzelm@29729
   755
  where "A x" and "B y"
wenzelm@29729
   756
proof -
wenzelm@29733
   757
  have "A a" and "B b" sorry %noproof
wenzelm@29729
   758
  then show thesis ..
wenzelm@29729
   759
qed
wenzelm@29729
   760
wenzelm@58618
   761
text_raw \<open>\end{minipage}\<close>
wenzelm@29729
   762
wenzelm@58618
   763
text \<open>
wenzelm@29729
   764
  \medskip\noindent Here local facts \isacharbackquoteopen@{text "A
wenzelm@29729
   765
  x"}\isacharbackquoteclose\ and \isacharbackquoteopen@{text "B
wenzelm@29729
   766
  y"}\isacharbackquoteclose\ are referenced immediately; there is no
wenzelm@29729
   767
  need to decompose the logical rule structure again.  In the second
wenzelm@29729
   768
  proof the final ``@{command then}~@{command show}~@{text
wenzelm@29729
   769
  thesis}~@{command ".."}''  involves the local rule case @{text "\<And>x
wenzelm@29729
   770
  y. A x \<Longrightarrow> B y \<Longrightarrow> thesis"} for the particular instance of terms @{text
wenzelm@29729
   771
  "a"} and @{text "b"} produced in the body.
wenzelm@58618
   772
\<close>
wenzelm@29729
   773
wenzelm@29729
   774
wenzelm@58618
   775
subsection \<open>Structured proof refinement \label{sec:framework-subproof}\<close>
wenzelm@29729
   776
wenzelm@58618
   777
text \<open>
wenzelm@29729
   778
  By breaking up the grammar for the Isar proof language, we may
wenzelm@29729
   779
  understand a proof text as a linear sequence of individual proof
wenzelm@29729
   780
  commands.  These are interpreted as transitions of the Isar virtual
wenzelm@29729
   781
  machine (Isar/VM), which operates on a block-structured
wenzelm@29729
   782
  configuration in single steps.  This allows users to write proof
wenzelm@29729
   783
  texts in an incremental manner, and inspect intermediate
wenzelm@29729
   784
  configurations for debugging.
wenzelm@29729
   785
wenzelm@29729
   786
  The basic idea is analogous to evaluating algebraic expressions on a
wenzelm@29729
   787
  stack machine: @{text "(a + b) \<cdot> c"} then corresponds to a sequence
wenzelm@29729
   788
  of single transitions for each symbol @{text "(, a, +, b, ), \<cdot>, c"}.
wenzelm@29729
   789
  In Isar the algebraic values are facts or goals, and the operations
wenzelm@29729
   790
  are inferences.
wenzelm@29729
   791
wenzelm@29729
   792
  \medskip The Isar/VM state maintains a stack of nodes, each node
wenzelm@29729
   793
  contains the local proof context, the linguistic mode, and a pending
wenzelm@29729
   794
  goal (optional).  The mode determines the type of transition that
wenzelm@29729
   795
  may be performed next, it essentially alternates between forward and
wenzelm@29738
   796
  backward reasoning, with an intermediate stage for chained facts
wenzelm@29738
   797
  (see \figref{fig:isar-vm}).
wenzelm@29738
   798
wenzelm@29738
   799
  \begin{figure}[htb]
wenzelm@29738
   800
  \begin{center}
wenzelm@48958
   801
  \includegraphics[width=0.8\textwidth]{isar-vm}
wenzelm@29738
   802
  \end{center}
wenzelm@29738
   803
  \caption{Isar/VM modes}\label{fig:isar-vm}
wenzelm@29738
   804
  \end{figure}
wenzelm@29738
   805
wenzelm@29738
   806
  For example, in @{text "state"} mode Isar acts like a mathematical
wenzelm@29738
   807
  scratch-pad, accepting declarations like @{command fix}, @{command
wenzelm@29738
   808
  assume}, and claims like @{command have}, @{command show}.  A goal
wenzelm@29738
   809
  statement changes the mode to @{text "prove"}, which means that we
wenzelm@29738
   810
  may now refine the problem via @{command unfolding} or @{command
wenzelm@29738
   811
  proof}.  Then we are again in @{text "state"} mode of a proof body,
wenzelm@29738
   812
  which may issue @{command show} statements to solve pending
wenzelm@29738
   813
  sub-goals.  A concluding @{command qed} will return to the original
wenzelm@29738
   814
  @{text "state"} mode one level upwards.  The subsequent Isar/VM
wenzelm@29738
   815
  trace indicates block structure, linguistic mode, goal state, and
wenzelm@29738
   816
  inferences:
wenzelm@58618
   817
\<close>
wenzelm@29729
   818
wenzelm@58618
   819
text_raw \<open>\begingroup\footnotesize\<close>
wenzelm@40964
   820
(*<*)notepad begin
wenzelm@29729
   821
(*>*)
wenzelm@58999
   822
  text_raw \<open>\begin{minipage}[t]{0.18\textwidth}\<close>
wenzelm@29729
   823
  have "A \<longrightarrow> B"
wenzelm@29729
   824
  proof
wenzelm@29729
   825
    assume A
wenzelm@29729
   826
    show B
wenzelm@29733
   827
      sorry %noproof
wenzelm@29729
   828
  qed
wenzelm@58999
   829
  text_raw \<open>\end{minipage}\quad
wenzelm@29735
   830
\begin{minipage}[t]{0.06\textwidth}
wenzelm@29729
   831
@{text "begin"} \\
wenzelm@29729
   832
\\
wenzelm@29729
   833
\\
wenzelm@29729
   834
@{text "begin"} \\
wenzelm@29729
   835
@{text "end"} \\
wenzelm@29729
   836
@{text "end"} \\
wenzelm@29729
   837
\end{minipage}
wenzelm@29729
   838
\begin{minipage}[t]{0.08\textwidth}
wenzelm@29729
   839
@{text "prove"} \\
wenzelm@29729
   840
@{text "state"} \\
wenzelm@29729
   841
@{text "state"} \\
wenzelm@29729
   842
@{text "prove"} \\
wenzelm@29729
   843
@{text "state"} \\
wenzelm@29729
   844
@{text "state"} \\
wenzelm@29735
   845
\end{minipage}\begin{minipage}[t]{0.35\textwidth}
wenzelm@29729
   846
@{text "(A \<longrightarrow> B) \<Longrightarrow> #(A \<longrightarrow> B)"} \\
wenzelm@29729
   847
@{text "(A \<Longrightarrow> B) \<Longrightarrow> #(A \<longrightarrow> B)"} \\
wenzelm@29729
   848
\\
wenzelm@29729
   849
\\
wenzelm@29729
   850
@{text "#(A \<longrightarrow> B)"} \\
wenzelm@29729
   851
@{text "A \<longrightarrow> B"} \\
wenzelm@29735
   852
\end{minipage}\begin{minipage}[t]{0.4\textwidth}
wenzelm@29729
   853
@{text "(init)"} \\
wenzelm@29735
   854
@{text "(resolution impI)"} \\
wenzelm@29729
   855
\\
wenzelm@29729
   856
\\
wenzelm@29729
   857
@{text "(refinement #A \<Longrightarrow> B)"} \\
wenzelm@29729
   858
@{text "(finish)"} \\
wenzelm@58618
   859
\end{minipage}\<close>
wenzelm@29729
   860
(*<*)
wenzelm@40964
   861
end
wenzelm@29729
   862
(*>*)
wenzelm@58618
   863
text_raw \<open>\endgroup\<close>
wenzelm@29729
   864
wenzelm@58618
   865
text \<open>
wenzelm@29735
   866
  \noindent Here the @{inference refinement} inference from
wenzelm@29729
   867
  \secref{sec:framework-resolution} mediates composition of Isar
wenzelm@29729
   868
  sub-proofs nicely.  Observe that this principle incorporates some
wenzelm@29729
   869
  degree of freedom in proof composition.  In particular, the proof
wenzelm@29729
   870
  body allows parameters and assumptions to be re-ordered, or commuted
wenzelm@29729
   871
  according to Hereditary Harrop Form.  Moreover, context elements
wenzelm@29729
   872
  that are not used in a sub-proof may be omitted altogether.  For
wenzelm@29729
   873
  example:
wenzelm@58618
   874
\<close>
wenzelm@29729
   875
wenzelm@58618
   876
text_raw \<open>\begin{minipage}{0.5\textwidth}\<close>
wenzelm@29729
   877
wenzelm@29729
   878
(*<*)
wenzelm@40964
   879
notepad
wenzelm@40964
   880
begin
wenzelm@29729
   881
(*>*)
wenzelm@29729
   882
  have "\<And>x y. A x \<Longrightarrow> B y \<Longrightarrow> C x y"
wenzelm@29729
   883
  proof -
wenzelm@29729
   884
    fix x and y
wenzelm@29729
   885
    assume "A x" and "B y"
wenzelm@29733
   886
    show "C x y" sorry %noproof
wenzelm@29729
   887
  qed
wenzelm@29729
   888
wenzelm@58999
   889
text_raw \<open>\end{minipage}\begin{minipage}{0.5\textwidth}\<close>
wenzelm@29729
   890
wenzelm@29729
   891
(*<*)
wenzelm@29729
   892
next
wenzelm@29729
   893
(*>*)
wenzelm@29729
   894
  have "\<And>x y. A x \<Longrightarrow> B y \<Longrightarrow> C x y"
wenzelm@29729
   895
  proof -
wenzelm@29729
   896
    fix x assume "A x"
wenzelm@29729
   897
    fix y assume "B y"
wenzelm@29733
   898
    show "C x y" sorry %noproof
wenzelm@29729
   899
  qed
wenzelm@29729
   900
wenzelm@58999
   901
text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}{0.5\textwidth}\<close>
wenzelm@29729
   902
wenzelm@29729
   903
(*<*)
wenzelm@29729
   904
next
wenzelm@29729
   905
(*>*)
wenzelm@29729
   906
  have "\<And>x y. A x \<Longrightarrow> B y \<Longrightarrow> C x y"
wenzelm@29729
   907
  proof -
wenzelm@29729
   908
    fix y assume "B y"
wenzelm@29729
   909
    fix x assume "A x"
wenzelm@29729
   910
    show "C x y" sorry
wenzelm@29729
   911
  qed
wenzelm@29729
   912
wenzelm@58999
   913
text_raw \<open>\end{minipage}\begin{minipage}{0.5\textwidth}\<close>
wenzelm@29729
   914
(*<*)
wenzelm@29729
   915
next
wenzelm@29729
   916
(*>*)
wenzelm@29729
   917
  have "\<And>x y. A x \<Longrightarrow> B y \<Longrightarrow> C x y"
wenzelm@29729
   918
  proof -
wenzelm@29729
   919
    fix y assume "B y"
wenzelm@29729
   920
    fix x
wenzelm@29729
   921
    show "C x y" sorry
wenzelm@29729
   922
  qed
wenzelm@29729
   923
(*<*)
wenzelm@40964
   924
end
wenzelm@29729
   925
(*>*)
wenzelm@29729
   926
wenzelm@58618
   927
text_raw \<open>\end{minipage}\<close>
wenzelm@29729
   928
wenzelm@58618
   929
text \<open>
wenzelm@29735
   930
  \medskip\noindent Such ``peephole optimizations'' of Isar texts are
wenzelm@29729
   931
  practically important to improve readability, by rearranging
wenzelm@29729
   932
  contexts elements according to the natural flow of reasoning in the
wenzelm@29729
   933
  body, while still observing the overall scoping rules.
wenzelm@29729
   934
wenzelm@29729
   935
  \medskip This illustrates the basic idea of structured proof
wenzelm@29729
   936
  processing in Isar.  The main mechanisms are based on natural
wenzelm@29729
   937
  deduction rule composition within the Pure framework.  In
wenzelm@29729
   938
  particular, there are no direct operations on goal states within the
wenzelm@29729
   939
  proof body.  Moreover, there is no hidden automated reasoning
wenzelm@29729
   940
  involved, just plain unification.
wenzelm@58618
   941
\<close>
wenzelm@29729
   942
wenzelm@29729
   943
wenzelm@58618
   944
subsection \<open>Calculational reasoning \label{sec:framework-calc}\<close>
wenzelm@29729
   945
wenzelm@58618
   946
text \<open>
wenzelm@29735
   947
  The existing Isar infrastructure is sufficiently flexible to support
wenzelm@29729
   948
  calculational reasoning (chains of transitivity steps) as derived
wenzelm@29729
   949
  concept.  The generic proof elements introduced below depend on
wenzelm@29732
   950
  rules declared as @{attribute trans} in the context.  It is left to
wenzelm@29729
   951
  the object-logic to provide a suitable rule collection for mixed
wenzelm@29732
   952
  relations of @{text "="}, @{text "<"}, @{text "\<le>"}, @{text "\<subset>"},
wenzelm@29732
   953
  @{text "\<subseteq>"} etc.  Due to the flexibility of rule composition
wenzelm@29729
   954
  (\secref{sec:framework-resolution}), substitution of equals by
wenzelm@29729
   955
  equals is covered as well, even substitution of inequalities
wenzelm@58552
   956
  involving monotonicity conditions; see also @{cite \<open>\S6\<close> "Wenzel-PhD"}
wenzelm@58552
   957
  and @{cite "Bauer-Wenzel:2001"}.
wenzelm@29729
   958
wenzelm@29729
   959
  The generic calculational mechanism is based on the observation that
wenzelm@29735
   960
  rules such as @{text "trans:"}~@{prop "x = y \<Longrightarrow> y = z \<Longrightarrow> x = z"}
wenzelm@29735
   961
  proceed from the premises towards the conclusion in a deterministic
wenzelm@29735
   962
  fashion.  Thus we may reason in forward mode, feeding intermediate
wenzelm@29735
   963
  results into rules selected from the context.  The course of
wenzelm@29735
   964
  reasoning is organized by maintaining a secondary fact called
wenzelm@29735
   965
  ``@{fact calculation}'', apart from the primary ``@{fact this}''
wenzelm@29735
   966
  already provided by the Isar primitives.  In the definitions below,
wenzelm@29735
   967
  @{attribute OF} refers to @{inference resolution}
wenzelm@29735
   968
  (\secref{sec:framework-resolution}) with multiple rule arguments,
wenzelm@29735
   969
  and @{text "trans"} represents to a suitable rule from the context:
wenzelm@29729
   970
wenzelm@29729
   971
  \begin{matharray}{rcl}
wenzelm@29729
   972
    @{command "also"}@{text "\<^sub>0"} & \equiv & @{command "note"}~@{text "calculation = this"} \\
wenzelm@29729
   973
    @{command "also"}@{text "\<^sub>n\<^sub>+\<^sub>1"} & \equiv & @{command "note"}~@{text "calculation = trans [OF calculation this]"} \\[0.5ex]
wenzelm@29729
   974
    @{command "finally"} & \equiv & @{command "also"}~@{command "from"}~@{text calculation} \\
wenzelm@29729
   975
  \end{matharray}
wenzelm@29729
   976
wenzelm@29729
   977
  \noindent The start of a calculation is determined implicitly in the
wenzelm@29729
   978
  text: here @{command also} sets @{fact calculation} to the current
wenzelm@29729
   979
  result; any subsequent occurrence will update @{fact calculation} by
wenzelm@29729
   980
  combination with the next result and a transitivity rule.  The
wenzelm@29729
   981
  calculational sequence is concluded via @{command finally}, where
wenzelm@29729
   982
  the final result is exposed for use in a concluding claim.
wenzelm@29729
   983
wenzelm@29729
   984
  Here is a canonical proof pattern, using @{command have} to
wenzelm@29729
   985
  establish the intermediate results:
wenzelm@58618
   986
\<close>
wenzelm@29729
   987
wenzelm@29729
   988
(*<*)
wenzelm@40964
   989
notepad
wenzelm@40964
   990
begin
wenzelm@29729
   991
(*>*)
wenzelm@29729
   992
  have "a = b" sorry
wenzelm@29729
   993
  also have "\<dots> = c" sorry
wenzelm@29729
   994
  also have "\<dots> = d" sorry
wenzelm@29729
   995
  finally have "a = d" .
wenzelm@29729
   996
(*<*)
wenzelm@40964
   997
end
wenzelm@29729
   998
(*>*)
wenzelm@29729
   999
wenzelm@58618
  1000
text \<open>
wenzelm@29729
  1001
  \noindent The term ``@{text "\<dots>"}'' above is a special abbreviation
wenzelm@29729
  1002
  provided by the Isabelle/Isar syntax layer: it statically refers to
wenzelm@29729
  1003
  the right-hand side argument of the previous statement given in the
wenzelm@29729
  1004
  text.  Thus it happens to coincide with relevant sub-expressions in
wenzelm@29729
  1005
  the calculational chain, but the exact correspondence is dependent
wenzelm@29729
  1006
  on the transitivity rules being involved.
wenzelm@29729
  1007
wenzelm@29729
  1008
  \medskip Symmetry rules such as @{prop "x = y \<Longrightarrow> y = x"} are like
wenzelm@29729
  1009
  transitivities with only one premise.  Isar maintains a separate
wenzelm@29729
  1010
  rule collection declared via the @{attribute sym} attribute, to be
wenzelm@29729
  1011
  used in fact expressions ``@{text "a [symmetric]"}'', or single-step
wenzelm@29729
  1012
  proofs ``@{command assume}~@{text "x = y"}~@{command then}~@{command
wenzelm@29729
  1013
  have}~@{text "y = x"}~@{command ".."}''.
wenzelm@58618
  1014
\<close>
wenzelm@29729
  1015
wenzelm@29742
  1016
end