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;
     1 theory Framework

     2 imports Base Main

     3 begin

     4

     5 chapter \<open>The Isabelle/Isar Framework \label{ch:isar-framework}\<close>

     6

     7 text \<open>

     8   Isabelle/Isar @{cite "Wenzel:1999:TPHOL" and "Wenzel-PhD" and

     9   "Nipkow-TYPES02" and "Wenzel-Paulson:2006" and "Wenzel:2006:Festschrift"}

    10   is intended as a generic framework for developing formal

    11   mathematical documents with full proof checking.  Definitions and

    12   proofs are organized as theories.  An assembly of theory sources may

    13   be presented as a printed document; see also

    14   \chref{ch:document-prep}.

    15

    16   The main objective of Isar is the design of a human-readable

    17   structured proof language, which is called the primary proof

    18   format'' in Isar terminology.  Such a primary proof language is

    19   somewhere in the middle between the extremes of primitive proof

    20   objects and actual natural language.  In this respect, Isar is a bit

    21   more formalistic than Mizar @{cite "Trybulec:1993:MizarFeatures" and

    22   "Rudnicki:1992:MizarOverview" and "Wiedijk:1999:Mizar"},

    23   using logical symbols for certain reasoning schemes where Mizar

    24   would prefer English words; see @{cite "Wenzel-Wiedijk:2002"} for

    25   further comparisons of these systems.

    26

    27   So Isar challenges the traditional way of recording informal proofs

    28   in mathematical prose, as well as the common tendency to see fully

    29   formal proofs directly as objects of some logical calculus (e.g.\

    30   @{text "\<lambda>"}-terms in a version of type theory).  In fact, Isar is

    31   better understood as an interpreter of a simple block-structured

    32   language for describing the data flow of local facts and goals,

    33   interspersed with occasional invocations of proof methods.

    34   Everything is reduced to logical inferences internally, but these

    35   steps are somewhat marginal compared to the overall bookkeeping of

    36   the interpretation process.  Thanks to careful design of the syntax

    37   and semantics of Isar language elements, a formal record of Isar

    38   instructions may later appear as an intelligible text to the

    39   attentive reader.

    40

    41   The Isar proof language has emerged from careful analysis of some

    42   inherent virtues of the existing logical framework of Isabelle/Pure

    43   @{cite "paulson-found" and "paulson700"}, notably composition of higher-order

    44   natural deduction rules, which is a generalization of Gentzen's

    45   original calculus @{cite "Gentzen:1935"}.  The approach of generic

    46   inference systems in Pure is continued by Isar towards actual proof

    47   texts.

    48

    49   Concrete applications require another intermediate layer: an

    50   object-logic.  Isabelle/HOL @{cite "isa-tutorial"} (simply-typed

    51   set-theory) is being used most of the time; Isabelle/ZF

    52   @{cite "isabelle-ZF"} is less extensively developed, although it would

    53   probably fit better for classical mathematics.

    54

    55   \medskip In order to illustrate natural deduction in Isar, we shall

    56   refer to the background theory and library of Isabelle/HOL.  This

    57   includes common notions of predicate logic, naive set-theory etc.\

    58   using fairly standard mathematical notation.  From the perspective

    59   of generic natural deduction there is nothing special about the

    60   logical connectives of HOL (@{text "\<and>"}, @{text "\<or>"}, @{text "\<forall>"},

    61   @{text "\<exists>"}, etc.), only the resulting reasoning principles are

    62   relevant to the user.  There are similar rules available for

    63   set-theory operators (@{text "\<inter>"}, @{text "\<union>"}, @{text "\<Inter>"}, @{text

    64   "\<Union>"}, etc.), or any other theory developed in the library (lattice

    65   theory, topology etc.).

    66

    67   Subsequently we briefly review fragments of Isar proof texts

    68   corresponding directly to such general deduction schemes.  The

    69   examples shall refer to set-theory, to minimize the danger of

    70   understanding connectives of predicate logic as something special.

    71

    72   \medskip The following deduction performs @{text "\<inter>"}-introduction,

    73   working forwards from assumptions towards the conclusion.  We give

    74   both the Isar text, and depict the primitive rule involved, as

    75   determined by unification of the problem against rules that are

    76   declared in the library context.

    77 \<close>

    78

    79 text_raw \<open>\medskip\begin{minipage}{0.6\textwidth}\<close>

    80

    81 (*<*)

    82 notepad

    83 begin

    84 (*>*)

    85     assume "x \<in> A" and "x \<in> B"

    86     then have "x \<in> A \<inter> B" ..

    87 (*<*)

    88 end

    89 (*>*)

    90

    91 text_raw \<open>\end{minipage}\begin{minipage}{0.4\textwidth}\<close>

    92

    93 text \<open>

    94   \infer{@{prop "x \<in> A \<inter> B"}}{@{prop "x \<in> A"} & @{prop "x \<in> B"}}

    95 \<close>

    96

    97 text_raw \<open>\end{minipage}\<close>

    98

    99 text \<open>

   100   \medskip\noindent Note that @{command assume} augments the proof

   101   context, @{command then} indicates that the current fact shall be

   102   used in the next step, and @{command have} states an intermediate

   103   goal.  The two dots @{command ".."}'' refer to a complete proof of

   104   this claim, using the indicated facts and a canonical rule from the

   105   context.  We could have been more explicit here by spelling out the

   106   final proof step via the @{command "by"} command:

   107 \<close>

   108

   109 (*<*)

   110 notepad

   111 begin

   112 (*>*)

   113     assume "x \<in> A" and "x \<in> B"

   114     then have "x \<in> A \<inter> B" by (rule IntI)

   115 (*<*)

   116 end

   117 (*>*)

   118

   119 text \<open>

   120   \noindent The format of the @{text "\<inter>"}-introduction rule represents

   121   the most basic inference, which proceeds from given premises to a

   122   conclusion, without any nested proof context involved.

   123

   124   The next example performs backwards introduction on @{term "\<Inter>\<A>"},

   125   the intersection of all sets within a given set.  This requires a

   126   nested proof of set membership within a local context, where @{term

   127   A} is an arbitrary-but-fixed member of the collection:

   128 \<close>

   129

   130 text_raw \<open>\medskip\begin{minipage}{0.6\textwidth}\<close>

   131

   132 (*<*)

   133 notepad

   134 begin

   135 (*>*)

   136     have "x \<in> \<Inter>\<A>"

   137     proof

   138       fix A

   139       assume "A \<in> \<A>"

   140       show "x \<in> A" sorry %noproof

   141     qed

   142 (*<*)

   143 end

   144 (*>*)

   145

   146 text_raw \<open>\end{minipage}\begin{minipage}{0.4\textwidth}\<close>

   147

   148 text \<open>

   149   \infer{@{prop "x \<in> \<Inter>\<A>"}}{\infer*{@{prop "x \<in> A"}}{@{text "[A][A \<in> \<A>]"}}}

   150 \<close>

   151

   152 text_raw \<open>\end{minipage}\<close>

   153

   154 text \<open>

   155   \medskip\noindent This Isar reasoning pattern again refers to the

   156   primitive rule depicted above.  The system determines it in the

   157   @{command proof}'' step, which could have been spelled out more

   158   explicitly as @{command proof}~@{text "(rule InterI)"}''.  Note

   159   that the rule involves both a local parameter @{term "A"} and an

   160   assumption @{prop "A \<in> \<A>"} in the nested reasoning.  This kind of

   161   compound rule typically demands a genuine sub-proof in Isar, working

   162   backwards rather than forwards as seen before.  In the proof body we

   163   encounter the @{command fix}-@{command assume}-@{command show}

   164   outline of nested sub-proofs that is typical for Isar.  The final

   165   @{command show} is like @{command have} followed by an additional

   166   refinement of the enclosing claim, using the rule derived from the

   167   proof body.

   168

   169   \medskip The next example involves @{term "\<Union>\<A>"}, which can be

   170   characterized as the set of all @{term "x"} such that @{prop "\<exists>A. x

   171   \<in> A \<and> A \<in> \<A>"}.  The elimination rule for @{prop "x \<in> \<Union>\<A>"} does

   172   not mention @{text "\<exists>"} and @{text "\<and>"} at all, but admits to obtain

   173   directly a local @{term "A"} such that @{prop "x \<in> A"} and @{prop "A

   174   \<in> \<A>"} hold.  This corresponds to the following Isar proof and

   175   inference rule, respectively:

   176 \<close>

   177

   178 text_raw \<open>\medskip\begin{minipage}{0.6\textwidth}\<close>

   179

   180 (*<*)

   181 notepad

   182 begin

   183 (*>*)

   184     assume "x \<in> \<Union>\<A>"

   185     then have C

   186     proof

   187       fix A

   188       assume "x \<in> A" and "A \<in> \<A>"

   189       show C sorry %noproof

   190     qed

   191 (*<*)

   192 end

   193 (*>*)

   194

   195 text_raw \<open>\end{minipage}\begin{minipage}{0.4\textwidth}\<close>

   196

   197 text \<open>

   198   \infer{@{prop "C"}}{@{prop "x \<in> \<Union>\<A>"} & \infer*{@{prop "C"}~}{@{text "[A][x \<in> A, A \<in> \<A>]"}}}

   199 \<close>

   200

   201 text_raw \<open>\end{minipage}\<close>

   202

   203 text \<open>

   204   \medskip\noindent Although the Isar proof follows the natural

   205   deduction rule closely, the text reads not as natural as

   206   anticipated.  There is a double occurrence of an arbitrary

   207   conclusion @{prop "C"}, which represents the final result, but is

   208   irrelevant for now.  This issue arises for any elimination rule

   209   involving local parameters.  Isar provides the derived language

   210   element @{command obtain}, which is able to perform the same

   211   elimination proof more conveniently:

   212 \<close>

   213

   214 (*<*)

   215 notepad

   216 begin

   217 (*>*)

   218     assume "x \<in> \<Union>\<A>"

   219     then obtain A where "x \<in> A" and "A \<in> \<A>" ..

   220 (*<*)

   221 end

   222 (*>*)

   223

   224 text \<open>

   225   \noindent Here we avoid to mention the final conclusion @{prop "C"}

   226   and return to plain forward reasoning.  The rule involved in the

   227   @{command ".."}'' proof is the same as before.

   228 \<close>

   229

   230

   231 section \<open>The Pure framework \label{sec:framework-pure}\<close>

   232

   233 text \<open>

   234   The Pure logic @{cite "paulson-found" and "paulson700"} is an intuitionistic

   235   fragment of higher-order logic @{cite "church40"}.  In type-theoretic

   236   parlance, there are three levels of @{text "\<lambda>"}-calculus with

   237   corresponding arrows @{text "\<Rightarrow>"}/@{text "\<And>"}/@{text "\<Longrightarrow>"}:

   238

   239   \medskip

   240   \begin{tabular}{ll}

   241   @{text "\<alpha> \<Rightarrow> \<beta>"} & syntactic function space (terms depending on terms) \\

   242   @{text "\<And>x. B(x)"} & universal quantification (proofs depending on terms) \\

   243   @{text "A \<Longrightarrow> B"} & implication (proofs depending on proofs) \\

   244   \end{tabular}

   245   \medskip

   246

   247   \noindent Here only the types of syntactic terms, and the

   248   propositions of proof terms have been shown.  The @{text

   249   "\<lambda>"}-structure of proofs can be recorded as an optional feature of

   250   the Pure inference kernel @{cite "Berghofer-Nipkow:2000:TPHOL"}, but

   251   the formal system can never depend on them due to \emph{proof

   252   irrelevance}.

   253

   254   On top of this most primitive layer of proofs, Pure implements a

   255   generic calculus for nested natural deduction rules, similar to

   256   @{cite "Schroeder-Heister:1984"}.  Here object-logic inferences are

   257   internalized as formulae over @{text "\<And>"} and @{text "\<Longrightarrow>"}.

   258   Combining such rule statements may involve higher-order unification

   259   @{cite "paulson-natural"}.

   260 \<close>

   261

   262

   263 subsection \<open>Primitive inferences\<close>

   264

   265 text \<open>

   266   Term syntax provides explicit notation for abstraction @{text "\<lambda>x ::

   267   \<alpha>. b(x)"} and application @{text "b a"}, while types are usually

   268   implicit thanks to type-inference; terms of type @{text "prop"} are

   269   called propositions.  Logical statements are composed via @{text "\<And>x

   270   :: \<alpha>. B(x)"} and @{text "A \<Longrightarrow> B"}.  Primitive reasoning operates on

   271   judgments of the form @{text "\<Gamma> \<turnstile> \<phi>"}, with standard introduction

   272   and elimination rules for @{text "\<And>"} and @{text "\<Longrightarrow>"} that refer to

   273   fixed parameters @{text "x\<^sub>1, \<dots>, x\<^sub>m"} and hypotheses

   274   @{text "A\<^sub>1, \<dots>, A\<^sub>n"} from the context @{text "\<Gamma>"};

   275   the corresponding proof terms are left implicit.  The subsequent

   276   inference rules define @{text "\<Gamma> \<turnstile> \<phi>"} inductively, relative to a

   277   collection of axioms:

   278

   279   $  280 \infer{@{text "\<turnstile> A"}}{(@{text "A"} \text{~axiom})}   281 \qquad   282 \infer{@{text "A \<turnstile> A"}}{}   283$

   284

   285   $  286 \infer{@{text "\<Gamma> \<turnstile> \<And>x. B(x)"}}{@{text "\<Gamma> \<turnstile> B(x)"} & @{text "x \<notin> \<Gamma>"}}   287 \qquad   288 \infer{@{text "\<Gamma> \<turnstile> B(a)"}}{@{text "\<Gamma> \<turnstile> \<And>x. B(x)"}}   289$

   290

   291   $  292 \infer{@{text "\<Gamma> - A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}}   293 \qquad   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"}}   295$

   296

   297   Furthermore, Pure provides a built-in equality @{text "\<equiv> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow>

   298   prop"} with axioms for reflexivity, substitution, extensionality,

   299   and @{text "\<alpha>\<beta>\<eta>"}-conversion on @{text "\<lambda>"}-terms.

   300

   301   \medskip An object-logic introduces another layer on top of Pure,

   302   e.g.\ with types @{text "i"} for individuals and @{text "o"} for

   303   propositions, term constants @{text "Trueprop :: o \<Rightarrow> prop"} as

   304   (implicit) derivability judgment and connectives like @{text "\<and> :: o

   305   \<Rightarrow> o \<Rightarrow> o"} or @{text "\<forall> :: (i \<Rightarrow> o) \<Rightarrow> o"}, and axioms for object-level

   306   rules such as @{text "conjI: A \<Longrightarrow> B \<Longrightarrow> A \<and> B"} or @{text "allI: (\<And>x. B

   307   x) \<Longrightarrow> \<forall>x. B x"}.  Derived object rules are represented as theorems of

   308   Pure.  After the initial object-logic setup, further axiomatizations

   309   are usually avoided; plain definitions and derived principles are

   310   used exclusively.

   311 \<close>

   312

   313

   314 subsection \<open>Reasoning with rules \label{sec:framework-resolution}\<close>

   315

   316 text \<open>

   317   Primitive inferences mostly serve foundational purposes.  The main

   318   reasoning mechanisms of Pure operate on nested natural deduction

   319   rules expressed as formulae, using @{text "\<And>"} to bind local

   320   parameters and @{text "\<Longrightarrow>"} to express entailment.  Multiple

   321   parameters and premises are represented by repeating these

   322   connectives in a right-associative manner.

   323

   324   Since @{text "\<And>"} and @{text "\<Longrightarrow>"} commute thanks to the theorem

   325   @{prop "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}, we may assume w.l.o.g.\

   326   that rule statements always observe the normal form where

   327   quantifiers are pulled in front of implications at each level of

   328   nesting.  This means that any Pure proposition may be presented as a

   329   \emph{Hereditary Harrop Formula} @{cite "Miller:1991"} which is of the

   330   form @{text "\<And>x\<^sub>1 \<dots> x\<^sub>m. H\<^sub>1 \<Longrightarrow> \<dots> H\<^sub>n \<Longrightarrow>

   331   A"} for @{text "m, n \<ge> 0"}, and @{text "A"} atomic, and @{text

   332   "H\<^sub>1, \<dots>, H\<^sub>n"} being recursively of the same format.

   333   Following the convention that outermost quantifiers are implicit,

   334   Horn clauses @{text "A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> A"} are a special

   335   case of this.

   336

   337   For example, @{text "\<inter>"}-introduction rule encountered before is

   338   represented as a Pure theorem as follows:

   339   $  340 @{text "IntI:"}~@{prop "x \<in> A \<Longrightarrow> x \<in> B \<Longrightarrow> x \<in> A \<inter> B"}   341$

   342

   343   \noindent This is a plain Horn clause, since no further nesting on

   344   the left is involved.  The general @{text "\<Inter>"}-introduction

   345   corresponds to a Hereditary Harrop Formula with one additional level

   346   of nesting:

   347   $  348 @{text "InterI:"}~@{prop "(\<And>A. A \<in> \<A> \<Longrightarrow> x \<in> A) \<Longrightarrow> x \<in> \<Inter>\<A>"}   349$

   350

   351   \medskip Goals are also represented as rules: @{text "A\<^sub>1 \<Longrightarrow>

   352   \<dots> A\<^sub>n \<Longrightarrow> C"} states that the sub-goals @{text "A\<^sub>1, \<dots>,

   353   A\<^sub>n"} entail the result @{text "C"}; for @{text "n = 0"} the

   354   goal is finished.  To allow @{text "C"} being a rule statement

   355   itself, we introduce the protective marker @{text "# :: prop \<Rightarrow>

   356   prop"}, which is defined as identity and hidden from the user.  We

   357   initialize and finish goal states as follows:

   358

   359   $  360 \begin{array}{c@ {\qquad}c}   361 \infer[(@{inference_def init})]{@{text "C \<Longrightarrow> #C"}}{} &   362 \infer[(@{inference_def finish})]{@{text C}}{@{text "#C"}}   363 \end{array}   364$

   365

   366   \noindent Goal states are refined in intermediate proof steps until

   367   a finished form is achieved.  Here the two main reasoning principles

   368   are @{inference resolution}, for back-chaining a rule against a

   369   sub-goal (replacing it by zero or more sub-goals), and @{inference

   370   assumption}, for solving a sub-goal (finding a short-circuit with

   371   local assumptions).  Below @{text "\<^vec>x"} stands for @{text

   372   "x\<^sub>1, \<dots>, x\<^sub>n"} (@{text "n \<ge> 0"}).

   373

   374   $  375 \infer[(@{inference_def resolution})]   376 {@{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> \<^vec>A (\<^vec>a \<^vec>x))\<vartheta> \<Longrightarrow> C\<vartheta>"}}   377 {\begin{tabular}{rl}   378 @{text "rule:"} &   379 @{text "\<^vec>A \<^vec>a \<Longrightarrow> B \<^vec>a"} \\   380 @{text "goal:"} &   381 @{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> B' \<^vec>x) \<Longrightarrow> C"} \\   382 @{text "goal unifier:"} &   383 @{text "(\<lambda>\<^vec>x. B (\<^vec>a \<^vec>x))\<vartheta> = B'\<vartheta>"} \\   384 \end{tabular}}   385$

   386

   387   \medskip

   388

   389   $  390 \infer[(@{inference_def assumption})]{@{text "C\<vartheta>"}}   391 {\begin{tabular}{rl}   392 @{text "goal:"} &   393 @{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> A \<^vec>x) \<Longrightarrow> C"} \\   394 @{text "assm unifier:"} & @{text "A\<vartheta> = H\<^sub>i\<vartheta>"}~~\text{(for some~@{text "H\<^sub>i"})} \\   395 \end{tabular}}   396$

   397

   398   The following trace illustrates goal-oriented reasoning in

   399   Isabelle/Pure:

   400

   401   {\footnotesize

   402   \medskip

   403   \begin{tabular}{r@ {\quad}l}

   404   @{text "(A \<and> B \<Longrightarrow> B \<and> A) \<Longrightarrow> #(A \<and> B \<Longrightarrow> B \<and> A)"} & @{text "(init)"} \\

   405   @{text "(A \<and> B \<Longrightarrow> B) \<Longrightarrow> (A \<and> B \<Longrightarrow> A) \<Longrightarrow> #\<dots>"} & @{text "(resolution B \<Longrightarrow> A \<Longrightarrow> B \<and> A)"} \\

   406   @{text "(A \<and> B \<Longrightarrow> A \<and> B) \<Longrightarrow> (A \<and> B \<Longrightarrow> A) \<Longrightarrow> #\<dots>"} & @{text "(resolution A \<and> B \<Longrightarrow> B)"} \\

   407   @{text "(A \<and> B \<Longrightarrow> A) \<Longrightarrow> #\<dots>"} & @{text "(assumption)"} \\

   408   @{text "(A \<and> B \<Longrightarrow> A \<and> B) \<Longrightarrow> #\<dots>"} & @{text "(resolution A \<and> B \<Longrightarrow> A)"} \\

   409   @{text "#\<dots>"} & @{text "(assumption)"} \\

   410   @{text "A \<and> B \<Longrightarrow> B \<and> A"} & @{text "(finish)"} \\

   411   \end{tabular}

   412   \medskip

   413   }

   414

   415   Compositions of @{inference assumption} after @{inference

   416   resolution} occurs quite often, typically in elimination steps.

   417   Traditional Isabelle tactics accommodate this by a combined

   418   @{inference_def elim_resolution} principle.  In contrast, Isar uses

   419   a slightly more refined combination, where the assumptions to be

   420   closed are marked explicitly, using again the protective marker

   421   @{text "#"}:

   422

   423   $  424 \infer[(@{inference refinement})]   425 {@{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> \<^vec>G' (\<^vec>a \<^vec>x))\<vartheta> \<Longrightarrow> C\<vartheta>"}}   426 {\begin{tabular}{rl}   427 @{text "sub\<hyphen>proof:"} &   428 @{text "\<^vec>G \<^vec>a \<Longrightarrow> B \<^vec>a"} \\   429 @{text "goal:"} &   430 @{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> B' \<^vec>x) \<Longrightarrow> C"} \\   431 @{text "goal unifier:"} &   432 @{text "(\<lambda>\<^vec>x. B (\<^vec>a \<^vec>x))\<vartheta> = B'\<vartheta>"} \\   433 @{text "assm unifiers:"} &   434 @{text "(\<lambda>\<^vec>x. G\<^sub>j (\<^vec>a \<^vec>x))\<vartheta> = #H\<^sub>i\<vartheta>"} \\   435 & \quad (for each marked @{text "G\<^sub>j"} some @{text "#H\<^sub>i"}) \\   436 \end{tabular}}   437$

   438

   439   \noindent Here the @{text "sub\<hyphen>proof"} rule stems from the

   440   main @{command fix}-@{command assume}-@{command show} outline of

   441   Isar (cf.\ \secref{sec:framework-subproof}): each assumption

   442   indicated in the text results in a marked premise @{text "G"} above.

   443   The marking enforces resolution against one of the sub-goal's

   444   premises.  Consequently, @{command fix}-@{command assume}-@{command

   445   show} enables to fit the result of a sub-proof quite robustly into a

   446   pending sub-goal, while maintaining a good measure of flexibility.

   447 \<close>

   448

   449

   450 section \<open>The Isar proof language \label{sec:framework-isar}\<close>

   451

   452 text \<open>

   453   Structured proofs are presented as high-level expressions for

   454   composing entities of Pure (propositions, facts, and goals).  The

   455   Isar proof language allows to organize reasoning within the

   456   underlying rule calculus of Pure, but Isar is not another logical

   457   calculus!

   458

   459   Isar is an exercise in sound minimalism.  Approximately half of the

   460   language is introduced as primitive, the rest defined as derived

   461   concepts.  The following grammar describes the core language

   462   (category @{text "proof"}), which is embedded into theory

   463   specification elements such as @{command theorem}; see also

   464   \secref{sec:framework-stmt} for the separate category @{text

   465   "statement"}.

   466

   467   \medskip

   468   \begin{tabular}{rcl}

   469     @{text "theory\<hyphen>stmt"} & = & @{command "theorem"}~@{text "statement proof  |"}~~@{command "definition"}~@{text "\<dots>  |  \<dots>"} \$1ex]   470   471 @{text "proof"} & = & @{text "prfx\<^sup>*"}~@{command "proof"}~@{text "method\<^sup>? stmt\<^sup>*"}~@{command "qed"}~@{text "method\<^sup>?"} \\[1ex]   472   473 @{text prfx} & = & @{command "using"}~@{text "facts"} \\   474 & @{text "|"} & @{command "unfolding"}~@{text "facts"} \\   475   476 @{text stmt} & = & @{command "{"}~@{text "stmt\<^sup>*"}~@{command "}"} \\   477 & @{text "|"} & @{command "next"} \\   478 & @{text "|"} & @{command "note"}~@{text "name = facts"} \\   479 & @{text "|"} & @{command "let"}~@{text "term = term"} \\   480 & @{text "|"} & @{command "fix"}~@{text "var\<^sup>+"} \\   481 & @{text "|"} & @{command assume}~@{text "\<guillemotleft>inference\<guillemotright> name: props"} \\   482 & @{text "|"} & @{command "then"}@{text "\<^sup>?"}~@{text goal} \\   483 @{text goal} & = & @{command "have"}~@{text "name: props proof"} \\   484 & @{text "|"} & @{command "show"}~@{text "name: props proof"} \\   485 \end{tabular}   486   487 \medskip Simultaneous propositions or facts may be separated by the   488 @{keyword "and"} keyword.   489   490 \medskip The syntax for terms and propositions is inherited from   491 Pure (and the object-logic). A @{text "pattern"} is a @{text   492 "term"} with schematic variables, to be bound by higher-order   493 matching.   494   495 \medskip Facts may be referenced by name or proposition. For   496 example, the result of @{command have}~@{text "a: A \<langle>proof\<rangle>"}''   497 becomes available both as @{text "a"} and   498 \isacharbackquoteopen@{text "A"}\isacharbackquoteclose. Moreover,   499 fact expressions may involve attributes that modify either the   500 theorem or the background context. For example, the expression   501 @{text "a [OF b]"}'' refers to the composition of two facts   502 according to the @{inference resolution} inference of   503 \secref{sec:framework-resolution}, while @{text "a [intro]"}''   504 declares a fact as introduction rule in the context.   505   506 The special fact called @{fact this}'' always refers to the last   507 result, as produced by @{command note}, @{command assume}, @{command   508 have}, or @{command show}. Since @{command note} occurs   509 frequently together with @{command then} we provide some   510 abbreviations:   511   512 \medskip   513 \begin{tabular}{rcl}   514 @{command from}~@{text a} & @{text "\<equiv>"} & @{command note}~@{text a}~@{command then} \\   515 @{command with}~@{text a} & @{text "\<equiv>"} & @{command from}~@{text "a \<AND> this"} \\   516 \end{tabular}   517 \medskip   518   519 The @{text "method"} category is essentially a parameter and may be   520 populated later. Methods use the facts indicated by @{command   521 "then"} or @{command using}, and then operate on the goal state.   522 Some basic methods are predefined: @{method "-"}'' leaves the goal   523 unchanged, @{method this}'' applies the facts as rules to the   524 goal, @{method (Pure) "rule"}'' applies the facts to another rule and the   525 result to the goal (both @{method this}'' and @{method (Pure) rule}''   526 refer to @{inference resolution} of   527 \secref{sec:framework-resolution}). The secondary arguments to   528 @{method (Pure) rule}'' may be specified explicitly as in @{text "(rule   529 a)"}'', or picked from the context. In the latter case, the system   530 first tries rules declared as @{attribute (Pure) elim} or   531 @{attribute (Pure) dest}, followed by those declared as @{attribute   532 (Pure) intro}.   533   534 The default method for @{command proof} is @{method (Pure) rule}''   535 (arguments picked from the context), for @{command qed} it is   536 @{method "-"}''. Further abbreviations for terminal proof steps   537 are @{command "by"}~@{text "method\<^sub>1 method\<^sub>2"}'' for   538 @{command proof}~@{text "method\<^sub>1"}~@{command qed}~@{text   539 "method\<^sub>2"}'', and @{command ".."}'' for @{command   540 "by"}~@{method (Pure) rule}, and @{command "."}'' for @{command   541 "by"}~@{method this}''. The @{command unfolding} element operates   542 directly on the current facts and goal by applying equalities.   543   544 \medskip Block structure can be indicated explicitly by @{command   545 "{"}~@{text "\<dots>"}~@{command "}"}'', although the body of a sub-proof   546 already involves implicit nesting. In any case, @{command next}   547 jumps into the next section of a block, i.e.\ it acts like closing   548 an implicit block scope and opening another one; there is no direct   549 correspondence to subgoals here.   550   551 The remaining elements @{command fix} and @{command assume} build up   552 a local context (see \secref{sec:framework-context}), while   553 @{command show} refines a pending sub-goal by the rule resulting   554 from a nested sub-proof (see \secref{sec:framework-subproof}).   555 Further derived concepts will support calculational reasoning (see   556 \secref{sec:framework-calc}).   557 \<close>   558   559   560 subsection \<open>Context elements \label{sec:framework-context}\<close>   561   562 text \<open>   563 In judgments @{text "\<Gamma> \<turnstile> \<phi>"} of the primitive framework, @{text "\<Gamma>"}   564 essentially acts like a proof context. Isar elaborates this idea   565 towards a higher-level notion, with additional information for   566 type-inference, term abbreviations, local facts, hypotheses etc.   567   568 The element @{command fix}~@{text "x :: \<alpha>"} declares a local   569 parameter, i.e.\ an arbitrary-but-fixed entity of a given type; in   570 results exported from the context, @{text "x"} may become anything.   571 The @{command assume}~@{text "\<guillemotleft>inference\<guillemotright>"} element provides a   572 general interface to hypotheses: @{command assume}~@{text   573 "\<guillemotleft>inference\<guillemotright> A"}'' produces @{text "A \<turnstile> A"} locally, while the   574 included inference tells how to discharge @{text A} from results   575 @{text "A \<turnstile> B"} later on. There is no user-syntax for @{text   576 "\<guillemotleft>inference\<guillemotright>"}, i.e.\ it may only occur internally when derived   577 commands are defined in ML.   578   579 At the user-level, the default inference for @{command assume} is   580 @{inference discharge} as given below. The additional variants   581 @{command presume} and @{command def} are defined as follows:   582   583 \medskip   584 \begin{tabular}{rcl}   585 @{command presume}~@{text A} & @{text "\<equiv>"} & @{command assume}~@{text "\<guillemotleft>weak\<hyphen>discharge\<guillemotright> A"} \\   586 @{command def}~@{text "x \<equiv> a"} & @{text "\<equiv>"} & @{command fix}~@{text x}~@{command assume}~@{text "\<guillemotleft>expansion\<guillemotright> x \<equiv> a"} \\   587 \end{tabular}   588 \medskip   589   590 \[   591 \infer[(@{inference_def discharge})]{@{text "\<strut>\<Gamma> - A \<turnstile> #A \<Longrightarrow> B"}}{@{text "\<strut>\<Gamma> \<turnstile> B"}}   592$

   593   $  594 \infer[(@{inference_def "weak\<hyphen>discharge"})]{@{text "\<strut>\<Gamma> - A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<strut>\<Gamma> \<turnstile> B"}}   595$

   596   $  597 \infer[(@{inference_def expansion})]{@{text "\<strut>\<Gamma> - (x \<equiv> a) \<turnstile> B a"}}{@{text "\<strut>\<Gamma> \<turnstile> B x"}}   598$

   599

   600   \medskip Note that @{inference discharge} and @{inference

   601   "weak\<hyphen>discharge"} differ in the marker for @{prop A}, which is

   602   relevant when the result of a @{command fix}-@{command

   603   assume}-@{command show} outline is composed with a pending goal,

   604   cf.\ \secref{sec:framework-subproof}.

   605

   606   The most interesting derived context element in Isar is @{command

   607   obtain} @{cite \<open>\S5.3\<close> "Wenzel-PhD"}, which supports generalized

   608   elimination steps in a purely forward manner.  The @{command obtain}

   609   command takes a specification of parameters @{text "\<^vec>x"} and

   610   assumptions @{text "\<^vec>A"} to be added to the context, together

   611   with a proof of a case rule stating that this extension is

   612   conservative (i.e.\ may be removed from closed results later on):

   613

   614   \medskip

   615   \begin{tabular}{l}

   616   @{text "\<langle>facts\<rangle>"}~~@{command obtain}~@{text "\<^vec>x \<WHERE> \<^vec>A \<^vec>x  \<langle>proof\<rangle> \<equiv>"} \$0.5ex]   617 \quad @{command have}~@{text "case: \<And>thesis. (\<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis) \<Longrightarrow> thesis\<rangle>"} \\   618 \quad @{command proof}~@{method "-"} \\   619 \qquad @{command fix}~@{text thesis} \\   620 \qquad @{command assume}~@{text "[intro]: \<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis"} \\   621 \qquad @{command show}~@{text thesis}~@{command using}~@{text "\<langle>facts\<rangle> \<langle>proof\<rangle>"} \\   622 \quad @{command qed} \\   623 \quad @{command fix}~@{text "\<^vec>x"}~@{command assume}~@{text "\<guillemotleft>elimination case\<guillemotright> \<^vec>A \<^vec>x"} \\   624 \end{tabular}   625 \medskip   626   627 \[   628 \infer[(@{inference elimination})]{@{text "\<Gamma> \<turnstile> B"}}{   629 \begin{tabular}{rl}   630 @{text "case:"} &   631 @{text "\<Gamma> \<turnstile> \<And>thesis. (\<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis) \<Longrightarrow> thesis"} \\[0.2ex]   632 @{text "result:"} &   633 @{text "\<Gamma> \<union> \<^vec>A \<^vec>y \<turnstile> B"} \\[0.2ex]   634 \end{tabular}}   635$

   636

   637   \noindent Here the name @{text thesis}'' is a specific convention

   638   for an arbitrary-but-fixed proposition; in the primitive natural

   639   deduction rules shown before we have occasionally used @{text C}.

   640   The whole statement of @{command obtain}~@{text x}~@{keyword

   641   "where"}~@{text "A x"}'' may be read as a claim that @{text "A x"}

   642   may be assumed for some arbitrary-but-fixed @{text "x"}.  Also note

   643   that @{command obtain}~@{text "A \<AND> B"}'' without parameters

   644   is similar to @{command have}~@{text "A \<AND> B"}'', but the

   645   latter involves multiple sub-goals.

   646

   647   \medskip The subsequent Isar proof texts explain all context

   648   elements introduced above using the formal proof language itself.

   649   After finishing a local proof within a block, we indicate the

   650   exported result via @{command note}.

   651 \<close>

   652

   653 (*<*)

   654 theorem True

   655 proof

   656 (*>*)

   657   text_raw \<open>\begin{minipage}[t]{0.45\textwidth}\<close>

   658   {

   659     fix x

   660     have "B x" sorry %noproof

   661   }

   662   note \<open>\<And>x. B x\<close>

   663   text_raw \<open>\end{minipage}\quad\begin{minipage}[t]{0.45\textwidth}\<close>(*<*)next(*>*)

   664   {

   665     assume A

   666     have B sorry %noproof

   667   }

   668   note \<open>A \<Longrightarrow> B\<close>

   669   text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.45\textwidth}\<close>(*<*)next(*>*)

   670   {

   671     def x \<equiv> a

   672     have "B x" sorry %noproof

   673   }

   674   note \<open>B a\<close>

   675   text_raw \<open>\end{minipage}\quad\begin{minipage}[t]{0.45\textwidth}\<close>(*<*)next(*>*)

   676   {

   677     obtain x where "A x" sorry %noproof

   678     have B sorry %noproof

   679   }

   680   note \<open>B\<close>

   681   text_raw \<open>\end{minipage}\<close>

   682 (*<*)

   683 qed

   684 (*>*)

   685

   686 text \<open>

   687   \bigskip\noindent This illustrates the meaning of Isar context

   688   elements without goals getting in between.

   689 \<close>

   690

   691 subsection \<open>Structured statements \label{sec:framework-stmt}\<close>

   692

   693 text \<open>

   694   The category @{text "statement"} of top-level theorem specifications

   695   is defined as follows:

   696

   697   \medskip

   698   \begin{tabular}{rcl}

   699   @{text "statement"} & @{text "\<equiv>"} & @{text "name: props \<AND> \<dots>"} \\

   700   & @{text "|"} & @{text "context\<^sup>* conclusion"} \\[0.5ex]

   701

   702   @{text "context"} & @{text "\<equiv>"} & @{text "\<FIXES> vars \<AND> \<dots>"} \\

   703   & @{text "|"} & @{text "\<ASSUMES> name: props \<AND> \<dots>"} \\

   704

   705   @{text "conclusion"} & @{text "\<equiv>"} & @{text "\<SHOWS> name: props \<AND> \<dots>"} \\

   706   & @{text "|"} & @{text "\<OBTAINS> vars \<AND> \<dots> \<WHERE> name: props \<AND> \<dots>"} \\

   707   & & \quad @{text "\<BBAR> \<dots>"} \\

   708   \end{tabular}

   709

   710   \medskip\noindent A simple @{text "statement"} consists of named

   711   propositions.  The full form admits local context elements followed

   712   by the actual conclusions, such as @{keyword "fixes"}~@{text

   713   x}~@{keyword "assumes"}~@{text "A x"}~@{keyword "shows"}~@{text "B

   714   x"}''.  The final result emerges as a Pure rule after discharging

   715   the context: @{prop "\<And>x. A x \<Longrightarrow> B x"}.

   716

   717   The @{keyword "obtains"} variant is another abbreviation defined

   718   below; unlike @{command obtain} (cf.\

   719   \secref{sec:framework-context}) there may be several cases''

   720   separated by @{text "\<BBAR>"}'', each consisting of several

   721   parameters (@{text "vars"}) and several premises (@{text "props"}).

   722   This specifies multi-branch elimination rules.

   723

   724   \medskip

   725   \begin{tabular}{l}

   726   @{text "\<OBTAINS> \<^vec>x \<WHERE> \<^vec>A \<^vec>x   \<BBAR>   \<dots>   \<equiv>"} \\[0.5ex]

   727   \quad @{text "\<FIXES> thesis"} \\

   728   \quad @{text "\<ASSUMES> [intro]: \<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis  \<AND>  \<dots>"} \\

   729   \quad @{text "\<SHOWS> thesis"} \\

   730   \end{tabular}

   731   \medskip

   732

   733   Presenting structured statements in such an open'' format usually

   734   simplifies the subsequent proof, because the outer structure of the

   735   problem is already laid out directly.  E.g.\ consider the following

   736   canonical patterns for @{text "\<SHOWS>"} and @{text "\<OBTAINS>"},

   737   respectively:

   738 \<close>

   739

   740 text_raw \<open>\begin{minipage}{0.5\textwidth}\<close>

   741

   742 theorem

   743   fixes x and y

   744   assumes "A x" and "B y"

   745   shows "C x y"

   746 proof -

   747   from \<open>A x\<close> and \<open>B y\<close>

   748   show "C x y" sorry %noproof

   749 qed

   750

   751 text_raw \<open>\end{minipage}\begin{minipage}{0.5\textwidth}\<close>

   752

   753 theorem

   754   obtains x and y

   755   where "A x" and "B y"

   756 proof -

   757   have "A a" and "B b" sorry %noproof

   758   then show thesis ..

   759 qed

   760

   761 text_raw \<open>\end{minipage}\<close>

   762

   763 text \<open>

   764   \medskip\noindent Here local facts \isacharbackquoteopen@{text "A

   765   x"}\isacharbackquoteclose\ and \isacharbackquoteopen@{text "B

   766   y"}\isacharbackquoteclose\ are referenced immediately; there is no

   767   need to decompose the logical rule structure again.  In the second

   768   proof the final @{command then}~@{command show}~@{text

   769   thesis}~@{command ".."}''  involves the local rule case @{text "\<And>x

   770   y. A x \<Longrightarrow> B y \<Longrightarrow> thesis"} for the particular instance of terms @{text

   771   "a"} and @{text "b"} produced in the body.

   772 \<close>

   773

   774

   775 subsection \<open>Structured proof refinement \label{sec:framework-subproof}\<close>

   776

   777 text \<open>

   778   By breaking up the grammar for the Isar proof language, we may

   779   understand a proof text as a linear sequence of individual proof

   780   commands.  These are interpreted as transitions of the Isar virtual

   781   machine (Isar/VM), which operates on a block-structured

   782   configuration in single steps.  This allows users to write proof

   783   texts in an incremental manner, and inspect intermediate

   784   configurations for debugging.

   785

   786   The basic idea is analogous to evaluating algebraic expressions on a

   787   stack machine: @{text "(a + b) \<cdot> c"} then corresponds to a sequence

   788   of single transitions for each symbol @{text "(, a, +, b, ), \<cdot>, c"}.

   789   In Isar the algebraic values are facts or goals, and the operations

   790   are inferences.

   791

   792   \medskip The Isar/VM state maintains a stack of nodes, each node

   793   contains the local proof context, the linguistic mode, and a pending

   794   goal (optional).  The mode determines the type of transition that

   795   may be performed next, it essentially alternates between forward and

   796   backward reasoning, with an intermediate stage for chained facts

   797   (see \figref{fig:isar-vm}).

   798

   799   \begin{figure}[htb]

   800   \begin{center}

   801   \includegraphics[width=0.8\textwidth]{isar-vm}

   802   \end{center}

   803   \caption{Isar/VM modes}\label{fig:isar-vm}

   804   \end{figure}

   805

   806   For example, in @{text "state"} mode Isar acts like a mathematical

   807   scratch-pad, accepting declarations like @{command fix}, @{command

   808   assume}, and claims like @{command have}, @{command show}.  A goal

   809   statement changes the mode to @{text "prove"}, which means that we

   810   may now refine the problem via @{command unfolding} or @{command

   811   proof}.  Then we are again in @{text "state"} mode of a proof body,

   812   which may issue @{command show} statements to solve pending

   813   sub-goals.  A concluding @{command qed} will return to the original

   814   @{text "state"} mode one level upwards.  The subsequent Isar/VM

   815   trace indicates block structure, linguistic mode, goal state, and

   816   inferences:

   817 \<close>

   818

   819 text_raw \<open>\begingroup\footnotesize\<close>

   820 (*<*)notepad begin

   821 (*>*)

   822   text_raw \<open>\begin{minipage}[t]{0.18\textwidth}\<close>

   823   have "A \<longrightarrow> B"

   824   proof

   825     assume A

   826     show B

   827       sorry %noproof

   828   qed

   829   text_raw \<open>\end{minipage}\quad

   830 \begin{minipage}[t]{0.06\textwidth}

   831 @{text "begin"} \\

   832 \\

   833 \\

   834 @{text "begin"} \\

   835 @{text "end"} \\

   836 @{text "end"} \\

   837 \end{minipage}

   838 \begin{minipage}[t]{0.08\textwidth}

   839 @{text "prove"} \\

   840 @{text "state"} \\

   841 @{text "state"} \\

   842 @{text "prove"} \\

   843 @{text "state"} \\

   844 @{text "state"} \\

   845 \end{minipage}\begin{minipage}[t]{0.35\textwidth}

   846 @{text "(A \<longrightarrow> B) \<Longrightarrow> #(A \<longrightarrow> B)"} \\

   847 @{text "(A \<Longrightarrow> B) \<Longrightarrow> #(A \<longrightarrow> B)"} \\

   848 \\

   849 \\

   850 @{text "#(A \<longrightarrow> B)"} \\

   851 @{text "A \<longrightarrow> B"} \\

   852 \end{minipage}\begin{minipage}[t]{0.4\textwidth}

   853 @{text "(init)"} \\

   854 @{text "(resolution impI)"} \\

   855 \\

   856 \\

   857 @{text "(refinement #A \<Longrightarrow> B)"} \\

   858 @{text "(finish)"} \\

   859 \end{minipage}\<close>

   860 (*<*)

   861 end

   862 (*>*)

   863 text_raw \<open>\endgroup\<close>

   864

   865 text \<open>

   866   \noindent Here the @{inference refinement} inference from

   867   \secref{sec:framework-resolution} mediates composition of Isar

   868   sub-proofs nicely.  Observe that this principle incorporates some

   869   degree of freedom in proof composition.  In particular, the proof

   870   body allows parameters and assumptions to be re-ordered, or commuted

   871   according to Hereditary Harrop Form.  Moreover, context elements

   872   that are not used in a sub-proof may be omitted altogether.  For

   873   example:

   874 \<close>

   875

   876 text_raw \<open>\begin{minipage}{0.5\textwidth}\<close>

   877

   878 (*<*)

   879 notepad

   880 begin

   881 (*>*)

   882   have "\<And>x y. A x \<Longrightarrow> B y \<Longrightarrow> C x y"

   883   proof -

   884     fix x and y

   885     assume "A x" and "B y"

   886     show "C x y" sorry %noproof

   887   qed

   888

   889 text_raw \<open>\end{minipage}\begin{minipage}{0.5\textwidth}\<close>

   890

   891 (*<*)

   892 next

   893 (*>*)

   894   have "\<And>x y. A x \<Longrightarrow> B y \<Longrightarrow> C x y"

   895   proof -

   896     fix x assume "A x"

   897     fix y assume "B y"

   898     show "C x y" sorry %noproof

   899   qed

   900

   901 text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}{0.5\textwidth}\<close>

   902

   903 (*<*)

   904 next

   905 (*>*)

   906   have "\<And>x y. A x \<Longrightarrow> B y \<Longrightarrow> C x y"

   907   proof -

   908     fix y assume "B y"

   909     fix x assume "A x"

   910     show "C x y" sorry

   911   qed

   912

   913 text_raw \<open>\end{minipage}\begin{minipage}{0.5\textwidth}\<close>

   914 (*<*)

   915 next

   916 (*>*)

   917   have "\<And>x y. A x \<Longrightarrow> B y \<Longrightarrow> C x y"

   918   proof -

   919     fix y assume "B y"

   920     fix x

   921     show "C x y" sorry

   922   qed

   923 (*<*)

   924 end

   925 (*>*)

   926

   927 text_raw \<open>\end{minipage}\<close>

   928

   929 text \<open>

   930   \medskip\noindent Such peephole optimizations'' of Isar texts are

   931   practically important to improve readability, by rearranging

   932   contexts elements according to the natural flow of reasoning in the

   933   body, while still observing the overall scoping rules.

   934

   935   \medskip This illustrates the basic idea of structured proof

   936   processing in Isar.  The main mechanisms are based on natural

   937   deduction rule composition within the Pure framework.  In

   938   particular, there are no direct operations on goal states within the

   939   proof body.  Moreover, there is no hidden automated reasoning

   940   involved, just plain unification.

   941 \<close>

   942

   943

   944 subsection \<open>Calculational reasoning \label{sec:framework-calc}\<close>

   945

   946 text \<open>

   947   The existing Isar infrastructure is sufficiently flexible to support

   948   calculational reasoning (chains of transitivity steps) as derived

   949   concept.  The generic proof elements introduced below depend on

   950   rules declared as @{attribute trans} in the context.  It is left to

   951   the object-logic to provide a suitable rule collection for mixed

   952   relations of @{text "="}, @{text "<"}, @{text "\<le>"}, @{text "\<subset>"},

   953   @{text "\<subseteq>"} etc.  Due to the flexibility of rule composition

   954   (\secref{sec:framework-resolution}), substitution of equals by

   955   equals is covered as well, even substitution of inequalities

   956   involving monotonicity conditions; see also @{cite \<open>\S6\<close> "Wenzel-PhD"}

   957   and @{cite "Bauer-Wenzel:2001"}.

   958

   959   The generic calculational mechanism is based on the observation that

   960   rules such as @{text "trans:"}~@{prop "x = y \<Longrightarrow> y = z \<Longrightarrow> x = z"}

   961   proceed from the premises towards the conclusion in a deterministic

   962   fashion.  Thus we may reason in forward mode, feeding intermediate

   963   results into rules selected from the context.  The course of

   964   reasoning is organized by maintaining a secondary fact called

   965   @{fact calculation}'', apart from the primary @{fact this}''

   966   already provided by the Isar primitives.  In the definitions below,

   967   @{attribute OF} refers to @{inference resolution}

   968   (\secref{sec:framework-resolution}) with multiple rule arguments,

   969   and @{text "trans"} represents to a suitable rule from the context:

   970

   971   \begin{matharray}{rcl}

   972     @{command "also"}@{text "\<^sub>0"} & \equiv & @{command "note"}~@{text "calculation = this"} \\

   973     @{command "also"}@{text "\<^sub>n\<^sub>+\<^sub>1"} & \equiv & @{command "note"}~@{text "calculation = trans [OF calculation this]"} \\[0.5ex]

   974     @{command "finally"} & \equiv & @{command "also"}~@{command "from"}~@{text calculation} \\

   975   \end{matharray}

   976

   977   \noindent The start of a calculation is determined implicitly in the

   978   text: here @{command also} sets @{fact calculation} to the current

   979   result; any subsequent occurrence will update @{fact calculation} by

   980   combination with the next result and a transitivity rule.  The

   981   calculational sequence is concluded via @{command finally}, where

   982   the final result is exposed for use in a concluding claim.

   983

   984   Here is a canonical proof pattern, using @{command have} to

   985   establish the intermediate results:

   986 \<close>

   987

   988 (*<*)

   989 notepad

   990 begin

   991 (*>*)

   992   have "a = b" sorry

   993   also have "\<dots> = c" sorry

   994   also have "\<dots> = d" sorry

   995   finally have "a = d" .

   996 (*<*)

   997 end

   998 (*>*)

   999

  1000 text \<open>

  1001   \noindent The term @{text "\<dots>"}'' above is a special abbreviation

  1002   provided by the Isabelle/Isar syntax layer: it statically refers to

  1003   the right-hand side argument of the previous statement given in the

  1004   text.  Thus it happens to coincide with relevant sub-expressions in

  1005   the calculational chain, but the exact correspondence is dependent

  1006   on the transitivity rules being involved.

  1007

  1008   \medskip Symmetry rules such as @{prop "x = y \<Longrightarrow> y = x"} are like

  1009   transitivities with only one premise.  Isar maintains a separate

  1010   rule collection declared via the @{attribute sym} attribute, to be

  1011   used in fact expressions @{text "a [symmetric]"}'', or single-step

  1012   proofs @{command assume}~@{text "x = y"}~@{command then}~@{command

  1013   have}~@{text "y = x"}~@{command ".."}''.

  1014 \<close>

  1015

  1016 end