src/Doc/Isar_Ref/Framework.thy
 author wenzelm Mon Oct 09 21:12:22 2017 +0200 (23 months ago) changeset 66822 4642cf4a7ebb parent 64510 488cb71eeb83 child 67399 eab6ce8368fa permissions -rw-r--r--
tuned signature;
     1 (*:maxLineLen=78:*)

     2

     3 theory Framework

     4   imports Main Base

     5 begin

     6

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

     8

     9 text \<open>

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

    11   "Nipkow-TYPES02" and "Wiedijk:1999:Mizar" and "Wenzel-Paulson:2006" and

    12   "Wenzel:2006:Festschrift"} is a generic framework for developing formal

    13   mathematical documents with full proof checking. Definitions, statements and

    14   proofs are organized as theories. A collection of theories sources may be

    15   presented as a printed document; see also \chref{ch:document-prep}.

    16

    17   The main concern of Isar is the design of a human-readable structured proof

    18   language, which is called the primary proof format'' in Isar terminology.

    19   Such a primary proof language is somewhere in the middle between the

    20   extremes of primitive proof objects and actual natural language.

    21

    22   Thus Isar challenges the traditional way of recording informal proofs in

    23   mathematical prose, as well as the common tendency to see fully formal

    24   proofs directly as objects of some logical calculus (e.g.\ \<open>\<lambda>\<close>-terms in a

    25   version of type theory). Technically, Isar is an interpreter of a simple

    26   block-structured language for describing the data flow of local facts and

    27   goals, interspersed with occasional invocations of proof methods. Everything

    28   is reduced to logical inferences internally, but these steps are somewhat

    29   marginal compared to the overall bookkeeping of the interpretation process.

    30   Thanks to careful design of the syntax and semantics of Isar language

    31   elements, a formal record of Isar commands may later appear as an

    32   intelligible text to the human reader.

    33

    34   The Isar proof language has emerged from careful analysis of some inherent

    35   virtues of the logical framework Isabelle/Pure @{cite "paulson-found" and

    36   "paulson700"}, notably composition of higher-order natural deduction rules,

    37   which is a generalization of Gentzen's original calculus @{cite

    38   "Gentzen:1935"}. The approach of generic inference systems in Pure is

    39   continued by Isar towards actual proof texts. See also

    40   \figref{fig:natural-deduction}

    41

    42   \begin{figure}[htb]

    43

    44   \begin{center}

    45   \begin{minipage}[t]{0.9\textwidth}

    46

    47   \textbf{Inferences:}

    48   \begin{center}

    49   \begin{tabular}{l@ {\qquad}l}

    50   \infer{\<open>B\<close>}{\<open>A \<longrightarrow> B\<close> & \<open>A\<close>} &

    51   \infer{\<open>A \<longrightarrow> B\<close>}{\infer*{\<open>B\<close>}{\<open>[A]\<close>}} \\

    52   \end{tabular}

    53   \end{center}

    54

    55   \textbf{Isabelle/Pure:}

    56   \begin{center}

    57   \begin{tabular}{l@ {\qquad}l}

    58   \<open>(A \<longrightarrow> B) \<Longrightarrow> A \<Longrightarrow> B\<close> &

    59   \<open>(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B\<close>

    60   \end{tabular}

    61   \end{center}

    62

    63   \textbf{Isabelle/Isar:}

    64   \begin{center}

    65   \begin{minipage}[t]{0.4\textwidth}

    66   @{theory_text [display, indent = 2]

    67     \<open>have "A \<longrightarrow> B" \<proof>

    68 also have A \<proof>

    69 finally have B .\<close>}

    70   \end{minipage}

    71   \begin{minipage}[t]{0.4\textwidth}

    72   @{theory_text [display, indent = 2]

    73     \<open>have "A \<longrightarrow> B"

    74 proof

    75   assume A

    76   then show B \<proof>

    77 qed\<close>}

    78   \end{minipage}

    79   \end{center}

    80

    81   \end{minipage}

    82   \end{center}

    83

    84   \caption{Natural Deduction via inferences according to Gentzen, rules in

    85   Isabelle/Pure, and proofs in Isabelle/Isar}\label{fig:natural-deduction}

    86

    87   \end{figure}

    88

    89   \<^medskip>

    90   Concrete applications require another intermediate layer: an object-logic.

    91   Isabelle/HOL @{cite "isa-tutorial"} (simply-typed set-theory) is most

    92   commonly used; elementary examples are given in the directory

    93   \<^dir>\<open>~~/src/HOL/Isar_Examples\<close>. Some examples demonstrate how to start a fresh

    94   object-logic from Isabelle/Pure, and use Isar proofs from the very start,

    95   despite the lack of advanced proof tools at such an early stage (e.g.\ see

    96   \<^file>\<open>~~/src/HOL/Isar_Examples/Higher_Order_Logic.thy\<close>). Isabelle/FOL @{cite

    97   "isabelle-logics"} and Isabelle/ZF @{cite "isabelle-ZF"} also work, but are

    98   much less developed.

    99

   100   In order to illustrate natural deduction in Isar, we shall subsequently

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

   102   common notions of predicate logic, naive set-theory etc.\ using fairly

   103   standard mathematical notation. From the perspective of generic natural

   104   deduction there is nothing special about the logical connectives of HOL

   105   (\<open>\<and>\<close>, \<open>\<or>\<close>, \<open>\<forall>\<close>, \<open>\<exists>\<close>, etc.), only the resulting reasoning principles are

   106   relevant to the user. There are similar rules available for set-theory

   107   operators (\<open>\<inter>\<close>, \<open>\<union>\<close>, \<open>\<Inter>\<close>, \<open>\<Union>\<close>, etc.), or any other theory developed in the

   108   library (lattice theory, topology etc.).

   109

   110   Subsequently we briefly review fragments of Isar proof texts corresponding

   111   directly to such general deduction schemes. The examples shall refer to

   112   set-theory, to minimize the danger of understanding connectives of predicate

   113   logic as something special.

   114

   115   \<^medskip>

   116   The following deduction performs \<open>\<inter>\<close>-introduction, working forwards from

   117   assumptions towards the conclusion. We give both the Isar text, and depict

   118   the primitive rule involved, as determined by unification of fact and goal

   119   statements against rules that are declared in the library context.

   120 \<close>

   121

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

   123

   124 (*<*)

   125 notepad

   126 begin

   127     fix x :: 'a and A B

   128 (*>*)

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

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

   131 (*<*)

   132 end

   133 (*>*)

   134

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

   136

   137 text \<open>

   138   \infer{\<open>x \<in> A \<inter> B\<close>}{\<open>x \<in> A\<close> & \<open>x \<in> B\<close>}

   139 \<close>

   140

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

   142

   143 text \<open>

   144   \<^medskip>

   145   Note that \<^theory_text>\<open>assume\<close> augments the proof context, \<^theory_text>\<open>then\<close> indicates that the

   146   current fact shall be used in the next step, and \<^theory_text>\<open>have\<close> states an

   147   intermediate goal. The two dots \<^theory_text>\<open>..\<close>'' refer to a complete proof of this

   148   claim, using the indicated facts and a canonical rule from the context. We

   149   could have been more explicit here by spelling out the final proof step via

   150   the \<^theory_text>\<open>by\<close> command:

   151 \<close>

   152

   153 (*<*)

   154 notepad

   155 begin

   156     fix x :: 'a and A B

   157 (*>*)

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

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

   160 (*<*)

   161 end

   162 (*>*)

   163

   164 text \<open>

   165   The format of the \<open>\<inter>\<close>-introduction rule represents the most basic inference,

   166   which proceeds from given premises to a conclusion, without any nested proof

   167   context involved.

   168

   169   The next example performs backwards introduction of \<open>\<Inter>\<A>\<close>, the intersection

   170   of all sets within a given set. This requires a nested proof of set

   171   membership within a local context, where \<open>A\<close> is an arbitrary-but-fixed

   172   member of the collection:

   173 \<close>

   174

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

   176

   177 (*<*)

   178 notepad

   179 begin

   180     fix x :: 'a and \<A>

   181 (*>*)

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

   183     proof

   184       fix A

   185       assume "A \<in> \<A>"

   186       show "x \<in> A" \<proof>

   187     qed

   188 (*<*)

   189 end

   190 (*>*)

   191

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

   193

   194 text \<open>

   195   \infer{\<open>x \<in> \<Inter>\<A>\<close>}{\infer*{\<open>x \<in> A\<close>}{\<open>[A][A \<in> \<A>]\<close>}}

   196 \<close>

   197

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

   199

   200 text \<open>

   201   \<^medskip>

   202   This Isar reasoning pattern again refers to the primitive rule depicted

   203   above. The system determines it in the \<^theory_text>\<open>proof\<close>'' step, which could have

   204   been spelled out more explicitly as \<^theory_text>\<open>proof (rule InterI)\<close>''. Note that

   205   the rule involves both a local parameter \<open>A\<close> and an assumption \<open>A \<in> \<A>\<close> in

   206   the nested reasoning. Such compound rules typically demands a genuine

   207   subproof in Isar, working backwards rather than forwards as seen before. In

   208   the proof body we encounter the \<^theory_text>\<open>fix\<close>-\<^theory_text>\<open>assume\<close>-\<^theory_text>\<open>show\<close> outline of nested

   209   subproofs that is typical for Isar. The final \<^theory_text>\<open>show\<close> is like \<^theory_text>\<open>have\<close>

   210   followed by an additional refinement of the enclosing claim, using the rule

   211   derived from the proof body.

   212

   213   \<^medskip>

   214   The next example involves \<open>\<Union>\<A>\<close>, which can be characterized as the set of

   215   all \<open>x\<close> such that \<open>\<exists>A. x \<in> A \<and> A \<in> \<A>\<close>. The elimination rule for \<open>x \<in> \<Union>\<A>\<close>

   216   does not mention \<open>\<exists>\<close> and \<open>\<and>\<close> at all, but admits to obtain directly a local

   217   \<open>A\<close> such that \<open>x \<in> A\<close> and \<open>A \<in> \<A>\<close> hold. This corresponds to the following

   218   Isar proof and inference rule, respectively:

   219 \<close>

   220

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

   222

   223 (*<*)

   224 notepad

   225 begin

   226     fix x :: 'a and \<A> C

   227 (*>*)

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

   229     then have C

   230     proof

   231       fix A

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

   233       show C \<proof>

   234     qed

   235 (*<*)

   236 end

   237 (*>*)

   238

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

   240

   241 text \<open>

   242   \infer{\<open>C\<close>}{\<open>x \<in> \<Union>\<A>\<close> & \infer*{\<open>C\<close>~}{\<open>[A][x \<in> A, A \<in> \<A>]\<close>}}

   243 \<close>

   244

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

   246

   247 text \<open>

   248   \<^medskip>

   249   Although the Isar proof follows the natural deduction rule closely, the text

   250   reads not as natural as anticipated. There is a double occurrence of an

   251   arbitrary conclusion \<open>C\<close>, which represents the final result, but is

   252   irrelevant for now. This issue arises for any elimination rule involving

   253   local parameters. Isar provides the derived language element \<^theory_text>\<open>obtain\<close>,

   254   which is able to perform the same elimination proof more conveniently:

   255 \<close>

   256

   257 (*<*)

   258 notepad

   259 begin

   260     fix x :: 'a and \<A>

   261 (*>*)

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

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

   264 (*<*)

   265 end

   266 (*>*)

   267

   268 text \<open>

   269   Here we avoid to mention the final conclusion \<open>C\<close> and return to plain

   270   forward reasoning. The rule involved in the \<^theory_text>\<open>..\<close>'' proof is the same as

   271   before.

   272 \<close>

   273

   274

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

   276

   277 text \<open>

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

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

   280   parlance, there are three levels of \<open>\<lambda>\<close>-calculus with corresponding arrows

   281   \<open>\<Rightarrow>\<close>/\<open>\<And>\<close>/\<open>\<Longrightarrow>\<close>:

   282

   283   \<^medskip>

   284   \begin{tabular}{ll}

   285   \<open>\<alpha> \<Rightarrow> \<beta>\<close> & syntactic function space (terms depending on terms) \\

   286   \<open>\<And>x. B(x)\<close> & universal quantification (proofs depending on terms) \\

   287   \<open>A \<Longrightarrow> B\<close> & implication (proofs depending on proofs) \\

   288   \end{tabular}

   289   \<^medskip>

   290

   291   Here only the types of syntactic terms, and the propositions of proof terms

   292   have been shown. The \<open>\<lambda>\<close>-structure of proofs can be recorded as an optional

   293   feature of the Pure inference kernel @{cite "Berghofer-Nipkow:2000:TPHOL"},

   294   but the formal system can never depend on them due to \<^emph>\<open>proof irrelevance\<close>.

   295

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

   297   calculus for nested natural deduction rules, similar to @{cite

   298   "Schroeder-Heister:1984"}. Here object-logic inferences are internalized as

   299   formulae over \<open>\<And>\<close> and \<open>\<Longrightarrow>\<close>. Combining such rule statements may involve

   300   higher-order unification @{cite "paulson-natural"}.

   301 \<close>

   302

   303

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

   305

   306 text \<open>

   307   Term syntax provides explicit notation for abstraction \<open>\<lambda>x :: \<alpha>. b(x)\<close> and

   308   application \<open>b a\<close>, while types are usually implicit thanks to

   309   type-inference; terms of type \<open>prop\<close> are called propositions. Logical

   310   statements are composed via \<open>\<And>x :: \<alpha>. B(x)\<close> and \<open>A \<Longrightarrow> B\<close>. Primitive reasoning

   311   operates on judgments of the form \<open>\<Gamma> \<turnstile> \<phi>\<close>, with standard introduction and

   312   elimination rules for \<open>\<And>\<close> and \<open>\<Longrightarrow>\<close> that refer to fixed parameters \<open>x\<^sub>1, \<dots>,

   313   x\<^sub>m\<close> and hypotheses \<open>A\<^sub>1, \<dots>, A\<^sub>n\<close> from the context \<open>\<Gamma>\<close>; the corresponding

   314   proof terms are left implicit. The subsequent inference rules define \<open>\<Gamma> \<turnstile> \<phi>\<close>

   315   inductively, relative to a collection of axioms from the implicit background

   316   theory:

   317

   318   $  319 \infer{\<open>\<turnstile> A\<close>}{\<open>A\<close> \mbox{~is axiom}}   320 \qquad   321 \infer{\<open>A \<turnstile> A\<close>}{}   322$

   323

   324   $  325 \infer{\<open>\<Gamma> \<turnstile> \<And>x. B(x)\<close>}{\<open>\<Gamma> \<turnstile> B(x)\<close> & \<open>x \<notin> \<Gamma>\<close>}   326 \qquad   327 \infer{\<open>\<Gamma> \<turnstile> B(a)\<close>}{\<open>\<Gamma> \<turnstile> \<And>x. B(x)\<close>}   328$

   329

   330   $  331 \infer{\<open>\<Gamma> - A \<turnstile> A \<Longrightarrow> B\<close>}{\<open>\<Gamma> \<turnstile> B\<close>}   332 \qquad   333 \infer{\<open>\<Gamma>\<^sub>1 \<union> \<Gamma>\<^sub>2 \<turnstile> B\<close>}{\<open>\<Gamma>\<^sub>1 \<turnstile> A \<Longrightarrow> B\<close> & \<open>\<Gamma>\<^sub>2 \<turnstile> A\<close>}   334$

   335

   336   Furthermore, Pure provides a built-in equality \<open>\<equiv> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> prop\<close> with

   337   axioms for reflexivity, substitution, extensionality, and \<open>\<alpha>\<beta>\<eta>\<close>-conversion

   338   on \<open>\<lambda>\<close>-terms.

   339

   340   \<^medskip>

   341

   342   An object-logic introduces another layer on top of Pure, e.g.\ with types

   343   \<open>i\<close> for individuals and \<open>o\<close> for propositions, term constants \<open>Trueprop :: o

   344   \<Rightarrow> prop\<close> as (implicit) derivability judgment and connectives like \<open>\<and> :: o \<Rightarrow> o

   345   \<Rightarrow> o\<close> or \<open>\<forall> :: (i \<Rightarrow> o) \<Rightarrow> o\<close>, and axioms for object-level rules such as

   346   \<open>conjI: A \<Longrightarrow> B \<Longrightarrow> A \<and> B\<close> or \<open>allI: (\<And>x. B x) \<Longrightarrow> \<forall>x. B x\<close>. Derived object rules

   347   are represented as theorems of Pure. After the initial object-logic setup,

   348   further axiomatizations are usually avoided: definitional principles are

   349   used instead (e.g.\ \<^theory_text>\<open>definition\<close>, \<^theory_text>\<open>inductive\<close>, \<^theory_text>\<open>fun\<close>, \<^theory_text>\<open>function\<close>).

   350 \<close>

   351

   352

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

   354

   355 text \<open>

   356   Primitive inferences mostly serve foundational purposes. The main reasoning

   357   mechanisms of Pure operate on nested natural deduction rules expressed as

   358   formulae, using \<open>\<And>\<close> to bind local parameters and \<open>\<Longrightarrow>\<close> to express entailment.

   359   Multiple parameters and premises are represented by repeating these

   360   connectives in a right-associative manner.

   361

   362   Thanks to the Pure theorem @{prop "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"} the

   363   connectives \<open>\<And>\<close> and \<open>\<Longrightarrow>\<close> commute. So we may assume w.l.o.g.\ that rule

   364   statements always observe the normal form where quantifiers are pulled in

   365   front of implications at each level of nesting. This means that any Pure

   366   proposition may be presented as a \<^emph>\<open>Hereditary Harrop Formula\<close> @{cite

   367   "Miller:1991"} which is of the form \<open>\<And>x\<^sub>1 \<dots> x\<^sub>m. H\<^sub>1 \<Longrightarrow> \<dots> H\<^sub>n \<Longrightarrow> A\<close> for \<open>m, n

   368   \<ge> 0\<close>, and \<open>A\<close> atomic, and \<open>H\<^sub>1, \<dots>, H\<^sub>n\<close> being recursively of the same

   369   format. Following the convention that outermost quantifiers are implicit,

   370   Horn clauses \<open>A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> A\<close> are a special case of this.

   371

   372   For example, the \<open>\<inter>\<close>-introduction rule encountered before is represented as

   373   a Pure theorem as follows:

   374   $  375 \<open>IntI:\<close>~@{prop "x \<in> A \<Longrightarrow> x \<in> B \<Longrightarrow> x \<in> A \<inter> B"}   376$

   377

   378   This is a plain Horn clause, since no further nesting on the left is

   379   involved. The general \<open>\<Inter>\<close>-introduction corresponds to a Hereditary Harrop

   380   Formula with one additional level of nesting:

   381   $  382 \<open>InterI:\<close>~@{prop "(\<And>A. A \<in> \<A> \<Longrightarrow> x \<in> A) \<Longrightarrow> x \<in> \<Inter>\<A>"}   383$

   384

   385   \<^medskip>

   386   Goals are also represented as rules: \<open>A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> C\<close> states that the

   387   subgoals \<open>A\<^sub>1, \<dots>, A\<^sub>n\<close> entail the result \<open>C\<close>; for \<open>n = 0\<close> the goal is

   388   finished. To allow \<open>C\<close> being a rule statement itself, there is an internal

   389   protective marker \<open># :: prop \<Rightarrow> prop\<close>, which is defined as identity and

   390   hidden from the user. We initialize and finish goal states as follows:

   391

   392   $  393 \begin{array}{c@ {\qquad}c}   394 \infer[(@{inference_def init})]{\<open>C \<Longrightarrow> #C\<close>}{} &   395 \infer[(@{inference_def finish})]{\<open>C\<close>}{\<open>#C\<close>}   396 \end{array}   397$

   398

   399   Goal states are refined in intermediate proof steps until a finished form is

   400   achieved. Here the two main reasoning principles are @{inference

   401   resolution}, for back-chaining a rule against a subgoal (replacing it by

   402   zero or more subgoals), and @{inference assumption}, for solving a subgoal

   403   (finding a short-circuit with local assumptions). Below \<open>\<^vec>x\<close> stands

   404   for \<open>x\<^sub>1, \<dots>, x\<^sub>n\<close> (for \<open>n \<ge> 0\<close>).

   405

   406   $  407 \infer[(@{inference_def resolution})]   408 {\<open>(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> \<^vec>A (\<^vec>a \<^vec>x))\<vartheta> \<Longrightarrow> C\<vartheta>\<close>}   409 {\begin{tabular}{rl}   410 \<open>rule:\<close> &   411 \<open>\<^vec>A \<^vec>a \<Longrightarrow> B \<^vec>a\<close> \\   412 \<open>goal:\<close> &   413 \<open>(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> B' \<^vec>x) \<Longrightarrow> C\<close> \\   414 \<open>goal unifier:\<close> &   415 \<open>(\<lambda>\<^vec>x. B (\<^vec>a \<^vec>x))\<vartheta> = B'\<vartheta>\<close> \\   416 \end{tabular}}   417$

   418

   419   \<^medskip>

   420

   421   $  422 \infer[(@{inference_def assumption})]{\<open>C\<vartheta>\<close>}   423 {\begin{tabular}{rl}   424 \<open>goal:\<close> &   425 \<open>(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> A \<^vec>x) \<Longrightarrow> C\<close> \\   426 \<open>assm unifier:\<close> & \<open>A\<vartheta> = H\<^sub>i\<vartheta>\<close>~~\mbox{for some~\<open>H\<^sub>i\<close>} \\   427 \end{tabular}}   428$

   429

   430   The following trace illustrates goal-oriented reasoning in

   431   Isabelle/Pure:

   432

   433   {\footnotesize

   434   \<^medskip>

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

   436   \<open>(A \<and> B \<Longrightarrow> B \<and> A) \<Longrightarrow> #(A \<and> B \<Longrightarrow> B \<and> A)\<close> & \<open>(init)\<close> \\

   437   \<open>(A \<and> B \<Longrightarrow> B) \<Longrightarrow> (A \<and> B \<Longrightarrow> A) \<Longrightarrow> #\<dots>\<close> & \<open>(resolution B \<Longrightarrow> A \<Longrightarrow> B \<and> A)\<close> \\

   438   \<open>(A \<and> B \<Longrightarrow> A \<and> B) \<Longrightarrow> (A \<and> B \<Longrightarrow> A) \<Longrightarrow> #\<dots>\<close> & \<open>(resolution A \<and> B \<Longrightarrow> B)\<close> \\

   439   \<open>(A \<and> B \<Longrightarrow> A) \<Longrightarrow> #\<dots>\<close> & \<open>(assumption)\<close> \\

   440   \<open>(A \<and> B \<Longrightarrow> A \<and> B) \<Longrightarrow> #\<dots>\<close> & \<open>(resolution A \<and> B \<Longrightarrow> A)\<close> \\

   441   \<open>#\<dots>\<close> & \<open>(assumption)\<close> \\

   442   \<open>A \<and> B \<Longrightarrow> B \<and> A\<close> & \<open>(finish)\<close> \\

   443   \end{tabular}

   444   \<^medskip>

   445   }

   446

   447   Compositions of @{inference assumption} after @{inference resolution} occurs

   448   quite often, typically in elimination steps. Traditional Isabelle tactics

   449   accommodate this by a combined @{inference_def elim_resolution} principle.

   450   In contrast, Isar uses a combined refinement rule as follows:\footnote{For

   451   simplicity and clarity, the presentation ignores \<^emph>\<open>weak premises\<close> as

   452   introduced via \<^theory_text>\<open>presume\<close> or \<^theory_text>\<open>show \<dots> when\<close>.}

   453

   454   {\small

   455   $  456 \infer[(@{inference refinement})]   457 {\<open>C\<vartheta>\<close>}   458 {\begin{tabular}{rl}   459 \<open>subgoal:\<close> &   460 \<open>(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> B' \<^vec>x) \<Longrightarrow> C\<close> \\   461 \<open>subproof:\<close> &   462 \<open>\<^vec>G \<^vec>a \<Longrightarrow> B \<^vec>a\<close> \quad for schematic \<open>\<^vec>a\<close> \\   463 \<open>concl unifier:\<close> &   464 \<open>(\<lambda>\<^vec>x. B (\<^vec>a \<^vec>x))\<vartheta> = B'\<vartheta>\<close> \\   465 \<open>assm unifiers:\<close> &   466 \<open>(\<lambda>\<^vec>x. G\<^sub>j (\<^vec>a \<^vec>x))\<vartheta> = H\<^sub>i\<vartheta>\<close> \quad for each \<open>G\<^sub>j\<close> some \<open>H\<^sub>i\<close> \\   467 \end{tabular}}   468$}

   469

   470   Here the \<open>subproof\<close> rule stems from the main \<^theory_text>\<open>fix\<close>-\<^theory_text>\<open>assume\<close>-\<^theory_text>\<open>show\<close>

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

   472   indicated in the text results in a marked premise \<open>G\<close> above. Consequently,

   473   \<^theory_text>\<open>fix\<close>-\<^theory_text>\<open>assume\<close>-\<^theory_text>\<open>show\<close> enables to fit the result of a subproof quite

   474   robustly into a pending subgoal, while maintaining a good measure of

   475   flexibility: the subproof only needs to fit modulo unification, and its

   476   assumptions may be a proper subset of the subgoal premises (see

   477   \secref{sec:framework-subproof}).

   478 \<close>

   479

   480

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

   482

   483 text \<open>

   484   Structured proofs are presented as high-level expressions for composing

   485   entities of Pure (propositions, facts, and goals). The Isar proof language

   486   allows to organize reasoning within the underlying rule calculus of Pure,

   487   but Isar is not another logical calculus. Isar merely imposes certain

   488   structure and policies on Pure inferences. The main grammar of the Isar

   489   proof language is given in \figref{fig:isar-syntax}.

   490

   491   \begin{figure}[htb]

   492   \begin{center}

   493   \begin{tabular}{rcl}

   494     \<open>main\<close> & \<open>=\<close> & \<^theory_text>\<open>notepad begin "statement\<^sup>*" end\<close> \\

   495     & \<open>|\<close> & \<^theory_text>\<open>theorem name: props if name: props for vars\<close> \\

   496     & \<open>|\<close> & \<^theory_text>\<open>theorem name:\<close> \\

   497     & & \quad\<^theory_text>\<open>fixes vars\<close> \\

   498     & & \quad\<^theory_text>\<open>assumes name: props\<close> \\

   499     & & \quad\<^theory_text>\<open>shows name: props "proof"\<close> \\

   500     & \<open>|\<close> & \<^theory_text>\<open>theorem name:\<close> \\

   501     & & \quad\<^theory_text>\<open>fixes vars\<close> \\

   502     & & \quad\<^theory_text>\<open>assumes name: props\<close> \\

   503     & & \quad\<^theory_text>\<open>obtains (name) clause "\<^bold>|" \<dots> "proof"\<close> \\

   504     \<open>proof\<close> & \<open>=\<close> & \<^theory_text>\<open>"refinement\<^sup>* proper_proof"\<close> \\

   505     \<open>refinement\<close> & \<open>=\<close> &  \<^theory_text>\<open>apply method\<close> \\

   506     & \<open>|\<close> & \<^theory_text>\<open>supply name = thms\<close> \\

   507     & \<open>|\<close> & \<^theory_text>\<open>subgoal premises name for vars "proof"\<close> \\

   508     & \<open>|\<close> & \<^theory_text>\<open>using thms\<close> \\

   509     & \<open>|\<close> & \<^theory_text>\<open>unfolding thms\<close> \\

   510     \<open>proper_proof\<close> & \<open>=\<close> & \<^theory_text>\<open>proof "method\<^sup>?" "statement\<^sup>*" qed "method\<^sup>?"\<close> \\

   511     & \<open>|\<close> & \<^theory_text>\<open>by method method\<close>~~~\<open>|\<close>~~~\<^theory_text>\<open>..\<close>~~~\<open>|\<close>~~~\<^theory_text>\<open>.\<close>~~~\<open>|\<close>~~~\<^theory_text>\<open>sorry\<close>~~~\<open>|\<close>~~~\<^theory_text>\<open>done\<close> \\

   512     \<open>statement\<close> & \<open>=\<close> & \<^theory_text>\<open>{ "statement\<^sup>*" }\<close>~~~\<open>|\<close>~~~\<^theory_text>\<open>next\<close> \\

   513     & \<open>|\<close> & \<^theory_text>\<open>note name = thms\<close> \\

   514     & \<open>|\<close> & \<^theory_text>\<open>let "term" = "term"\<close> \\

   515     & \<open>|\<close> & \<^theory_text>\<open>write name  (mixfix)\<close> \\

   516     & \<open>|\<close> & \<^theory_text>\<open>fix vars\<close> \\

   517     & \<open>|\<close> & \<^theory_text>\<open>assume name: props if props for vars\<close> \\

   518     & \<open>|\<close> & \<^theory_text>\<open>presume name: props if props for vars\<close> \\

   519     & \<open>|\<close> & \<^theory_text>\<open>define clause\<close> \\

   520     & \<open>|\<close> & \<^theory_text>\<open>case name: "case"\<close> \\

   521     & \<open>|\<close> & \<^theory_text>\<open>then"\<^sup>?" goal\<close> \\

   522     & \<open>|\<close> & \<^theory_text>\<open>from thms goal\<close> \\

   523     & \<open>|\<close> & \<^theory_text>\<open>with thms goal\<close> \\

   524     & \<open>|\<close> & \<^theory_text>\<open>also\<close>~~~\<open>|\<close>~~~\<^theory_text>\<open>finally goal\<close> \\

   525     & \<open>|\<close> & \<^theory_text>\<open>moreover\<close>~~~\<open>|\<close>~~~\<^theory_text>\<open>ultimately goal\<close> \\

   526     \<open>goal\<close> & \<open>=\<close> & \<^theory_text>\<open>have name: props if name: props for vars "proof"\<close> \\

   527     & \<open>|\<close> & \<^theory_text>\<open>show name: props if name: props for vars "proof"\<close> \\

   528     & \<open>|\<close> & \<^theory_text>\<open>show name: props when name: props for vars "proof"\<close> \\

   529     & \<open>|\<close> & \<^theory_text>\<open>consider (name) clause "\<^bold>|" \<dots> "proof"\<close> \\

   530     & \<open>|\<close> & \<^theory_text>\<open>obtain (name) clause "proof"\<close> \\

   531     \<open>clause\<close> & \<open>=\<close> & \<^theory_text>\<open>vars where name: props if props for vars\<close> \\

   532   \end{tabular}

   533   \end{center}

   534   \caption{Main grammar of the Isar proof language}\label{fig:isar-syntax}

   535   \end{figure}

   536

   537   The construction of the Isar proof language proceeds in a bottom-up fashion,

   538   as an exercise in purity and minimalism. The grammar in

   539   \appref{ap:main-grammar} describes the primitive parts of the core language

   540   (category \<open>proof\<close>), which is embedded into the main outer theory syntax via

   541   elements that require a proof (e.g.\ \<^theory_text>\<open>theorem\<close>, \<^theory_text>\<open>lemma\<close>, \<^theory_text>\<open>function\<close>,

   542   \<^theory_text>\<open>termination\<close>).

   543

   544   The syntax for terms and propositions is inherited from Pure (and the

   545   object-logic). A \<open>pattern\<close> is a \<open>term\<close> with schematic variables, to be bound

   546   by higher-order matching. Simultaneous propositions or facts may be

   547   separated by the \<^theory_text>\<open>and\<close> keyword.

   548

   549   \<^medskip>

   550   Facts may be referenced by name or proposition. For example, the result of

   551   \<^theory_text>\<open>have a: A \<proof>\<close>'' becomes accessible both via the name \<open>a\<close> and the

   552   literal proposition \<open>\<open>A\<close>\<close>. Moreover, fact expressions may involve attributes

   553   that modify either the theorem or the background context. For example, the

   554   expression \<open>a [OF b]\<close>'' refers to the composition of two facts according

   555   to the @{inference resolution} inference of

   556   \secref{sec:framework-resolution}, while \<open>a [intro]\<close>'' declares a fact as

   557   introduction rule in the context.

   558

   559   The special fact called @{fact this}'' always refers to the last result,

   560   as produced by \<^theory_text>\<open>note\<close>, \<^theory_text>\<open>assume\<close>, \<^theory_text>\<open>have\<close>, or \<^theory_text>\<open>show\<close>. Since \<^theory_text>\<open>note\<close> occurs

   561   frequently together with \<^theory_text>\<open>then\<close>, there are some abbreviations:

   562

   563   \<^medskip>

   564   \begin{tabular}{rcl}

   565     \<^theory_text>\<open>from a\<close> & \<open>\<equiv>\<close> & \<^theory_text>\<open>note a then\<close> \\

   566     \<^theory_text>\<open>with a\<close> & \<open>\<equiv>\<close> & \<^theory_text>\<open>from a and this\<close> \\

   567   \end{tabular}

   568   \<^medskip>

   569

   570   The \<open>method\<close> category is essentially a parameter of the Isar language and

   571   may be populated later. The command \<^theory_text>\<open>method_setup\<close> allows to define proof

   572   methods semantically in Isabelle/ML. The Eisbach language allows to define

   573   proof methods symbolically, as recursive expressions over existing methods

   574   @{cite "Matichuk-et-al:2014"}; see also \<^dir>\<open>~~/src/HOL/Eisbach\<close>.

   575

   576   Methods use the facts indicated by \<^theory_text>\<open>then\<close> or \<^theory_text>\<open>using\<close>, and then operate on

   577   the goal state. Some basic methods are predefined in Pure: @{method "-"}''

   578   leaves the goal unchanged, @{method this}'' applies the facts as rules to

   579   the goal, @{method (Pure) "rule"}'' applies the facts to another rule and

   580   the result to the goal (both @{method this}'' and @{method (Pure)

   581   rule}'' refer to @{inference resolution} of

   582   \secref{sec:framework-resolution}). The secondary arguments to @{method

   583   (Pure) rule}'' may be specified explicitly as in \<open>(rule a)\<close>'', or picked

   584   from the context. In the latter case, the system first tries rules declared

   585   as @{attribute (Pure) elim} or @{attribute (Pure) dest}, followed by those

   586   declared as @{attribute (Pure) intro}.

   587

   588   The default method for \<^theory_text>\<open>proof\<close> is @{method standard}'' (which subsumes

   589   @{method rule} with arguments picked from the context), for \<^theory_text>\<open>qed\<close> it is

   590   @{method "succeed"}''. Further abbreviations for terminal proof steps are

   591   \<^theory_text>\<open>by method\<^sub>1 method\<^sub>2\<close>'' for \<^theory_text>\<open>proof method\<^sub>1 qed method\<^sub>2\<close>'', and

   592   \<^theory_text>\<open>..\<close>'' for \<^theory_text>\<open>by standard\<close>, and \<^theory_text>\<open>.\<close>'' for \<^theory_text>\<open>by this\<close>''. The command

   593   \<^theory_text>\<open>unfolding facts\<close>'' operates directly on the goal by applying equalities.

   594

   595   \<^medskip>

   596   Block structure can be indicated explicitly by \<^theory_text>\<open>{ \<dots> }\<close>'', although the

   597   body of a subproof \<^theory_text>\<open>proof \<dots> qed\<close>'' already provides implicit nesting. In

   598   both situations, \<^theory_text>\<open>next\<close> jumps into the next section of a block, i.e.\ it

   599   acts like closing an implicit block scope and opening another one. There is

   600   no direct connection to subgoals here!

   601

   602   The commands \<^theory_text>\<open>fix\<close> and \<^theory_text>\<open>assume\<close> build up a local context (see

   603   \secref{sec:framework-context}), while \<^theory_text>\<open>show\<close> refines a pending subgoal by

   604   the rule resulting from a nested subproof (see

   605   \secref{sec:framework-subproof}). Further derived concepts will support

   606   calculational reasoning (see \secref{sec:framework-calc}).

   607 \<close>

   608

   609

   610 subsection \<open>Context elements \label{sec:framework-context}\<close>

   611

   612 text \<open>

   613   In judgments \<open>\<Gamma> \<turnstile> \<phi>\<close> of the primitive framework, \<open>\<Gamma>\<close> essentially acts like a

   614   proof context. Isar elaborates this idea towards a more advanced concept,

   615   with additional information for type-inference, term abbreviations, local

   616   facts, hypotheses etc.

   617

   618   The element \<^theory_text>\<open>fix x :: \<alpha>\<close> declares a local parameter, i.e.\ an

   619   arbitrary-but-fixed entity of a given type; in results exported from the

   620   context, \<open>x\<close> may become anything. The \<^theory_text>\<open>assume \<guillemotleft>inference\<guillemotright>\<close> element provides

   621   a general interface to hypotheses: \<^theory_text>\<open>assume \<guillemotleft>inference\<guillemotright> A\<close> produces \<open>A \<turnstile> A\<close>

   622   locally, while the included inference tells how to discharge \<open>A\<close> from

   623   results \<open>A \<turnstile> B\<close> later on. There is no surface syntax for \<open>\<guillemotleft>inference\<guillemotright>\<close>,

   624   i.e.\ it may only occur internally when derived commands are defined in ML.

   625

   626   The default inference for \<^theory_text>\<open>assume\<close> is @{inference export} as given below.

   627   The derived element \<^theory_text>\<open>define x where "x \<equiv> a"\<close> is defined as \<^theory_text>\<open>fix x assume

   628   \<guillemotleft>expand\<guillemotright> x \<equiv> a\<close>, with the subsequent inference @{inference expand}.

   629

   630   $  631 \infer[(@{inference_def export})]{\<open>\<strut>\<Gamma> - A \<turnstile> A \<Longrightarrow> B\<close>}{\<open>\<strut>\<Gamma> \<turnstile> B\<close>}   632 \qquad   633 \infer[(@{inference_def expand})]{\<open>\<strut>\<Gamma> - (x \<equiv> a) \<turnstile> B a\<close>}{\<open>\<strut>\<Gamma> \<turnstile> B x\<close>}   634$

   635

   636   \<^medskip>

   637   The most interesting derived context element in Isar is \<^theory_text>\<open>obtain\<close> @{cite

   638   \<open>\S5.3\<close> "Wenzel-PhD"}, which supports generalized elimination steps in a

   639   purely forward manner. The \<^theory_text>\<open>obtain\<close> command takes a specification of

   640   parameters \<open>\<^vec>x\<close> and assumptions \<open>\<^vec>A\<close> to be added to the context,

   641   together with a proof of a case rule stating that this extension is

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

   643

   644   \<^medskip>

   645   \begin{tabular}{l}

   646   \<^theory_text>\<open>\<langle>facts\<rangle> obtain "\<^vec>x" where "\<^vec>A" "\<^vec>x" \<proof> \<equiv>\<close> \$0.5ex]   647 \quad \<^theory_text>\<open>have "case": "\<And>thesis. (\<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis) \<Longrightarrow> thesis"\<close> \\   648 \quad \<^theory_text>\<open>proof -\<close> \\   649 \qquad \<^theory_text>\<open>fix thesis\<close> \\   650 \qquad \<^theory_text>\<open>assume [intro]: "\<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis"\<close> \\   651 \qquad \<^theory_text>\<open>show thesis using \<langle>facts\<rangle> \<proof>\<close> \\   652 \quad \<^theory_text>\<open>qed\<close> \\   653 \quad \<^theory_text>\<open>fix "\<^vec>x" assume \<guillemotleft>elimination "case"\<guillemotright> "\<^vec>A \<^vec>x"\<close> \\   654 \end{tabular}   655 \<^medskip>   656   657 \[   658 \infer[(@{inference elimination})]{\<open>\<Gamma> \<turnstile> B\<close>}{   659 \begin{tabular}{rl}   660 \<open>case:\<close> &   661 \<open>\<Gamma> \<turnstile> \<And>thesis. (\<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis) \<Longrightarrow> thesis\<close> \\[0.2ex]   662 \<open>result:\<close> &   663 \<open>\<Gamma> \<union> \<^vec>A \<^vec>y \<turnstile> B\<close> \\[0.2ex]   664 \end{tabular}}   665$

   666

   667   Here the name \<open>thesis\<close>'' is a specific convention for an

   668   arbitrary-but-fixed proposition; in the primitive natural deduction rules

   669   shown before we have occasionally used \<open>C\<close>. The whole statement of

   670   \<^theory_text>\<open>obtain x where A x\<close>'' can be read as a claim that \<open>A x\<close> may be assumed

   671   for some arbitrary-but-fixed \<open>x\<close>. Also note that \<^theory_text>\<open>obtain A and B\<close>''

   672   without parameters is similar to \<^theory_text>\<open>have A and B\<close>'', but the latter

   673   involves multiple subgoals that need to be proven separately.

   674

   675   \<^medskip>

   676   The subsequent Isar proof texts explain all context elements introduced

   677   above using the formal proof language itself. After finishing a local proof

   678   within a block, the exported result is indicated via \<^theory_text>\<open>note\<close>.

   679 \<close>

   680

   681 (*<*)

   682 theorem True

   683 proof

   684 (*>*)

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

   686   {

   687     fix x

   688     have "B x" \<proof>

   689   }

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

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

   692   {

   693     assume A

   694     have B \<proof>

   695   }

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

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

   698   {

   699     define x where "x \<equiv> a"

   700     have "B x" \<proof>

   701   }

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

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

   704   {

   705     obtain x where "A x" \<proof>

   706     have B \<proof>

   707   }

   708   note \<open>B\<close>

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

   710 (*<*)

   711 qed

   712 (*>*)

   713

   714 text \<open>

   715   \<^bigskip>

   716   This explains the meaning of Isar context elements without, without goal

   717   states getting in the way.

   718 \<close>

   719

   720

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

   722

   723 text \<open>

   724   The syntax of top-level theorem statements is defined as follows:

   725

   726   \<^medskip>

   727   \begin{tabular}{rcl}

   728   \<open>statement\<close> & \<open>\<equiv>\<close> & \<^theory_text>\<open>name: props and \<dots>\<close> \\

   729   & \<open>|\<close> & \<open>context\<^sup>* conclusion\<close> \\[0.5ex]

   730

   731   \<open>context\<close> & \<open>\<equiv>\<close> & \<^theory_text>\<open>fixes vars and \<dots>\<close> \\

   732   & \<open>|\<close> & \<^theory_text>\<open>assumes name: props and \<dots>\<close> \\

   733

   734   \<open>conclusion\<close> & \<open>\<equiv>\<close> & \<^theory_text>\<open>shows name: props and \<dots>\<close> \\

   735   & \<open>|\<close> & \<^theory_text>\<open>obtains vars and \<dots> where name: props and \<dots>\<close> \\

   736   & & \quad \<open>\<BBAR> \<dots>\<close> \\

   737   \end{tabular}

   738

   739   \<^medskip>

   740   A simple statement consists of named propositions. The full form admits

   741   local context elements followed by the actual conclusions, such as \<^theory_text>\<open>fixes

   742   x assumes A x shows B x\<close>''. The final result emerges as a Pure rule after

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

   744

   745   The \<^theory_text>\<open>obtains\<close> variant is another abbreviation defined below; unlike

   746   \<^theory_text>\<open>obtain\<close> (cf.\ \secref{sec:framework-context}) there may be several

   747   cases'' separated by \<open>\<BBAR>\<close>'', each consisting of several parameters

   748   (\<open>vars\<close>) and several premises (\<open>props\<close>). This specifies multi-branch

   749   elimination rules.

   750

   751   \<^medskip>

   752   \begin{tabular}{l}

   753   \<^theory_text>\<open>obtains "\<^vec>x" where "\<^vec>A" "\<^vec>x"  "\<BBAR>"  \<dots>  \<equiv>\<close> \\[0.5ex]

   754   \quad \<^theory_text>\<open>fixes thesis\<close> \\

   755   \quad \<^theory_text>\<open>assumes [intro]: "\<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis"  and  \<dots>\<close> \\

   756   \quad \<^theory_text>\<open>shows thesis\<close> \\

   757   \end{tabular}

   758   \<^medskip>

   759

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

   761   simplifies the subsequent proof, because the outer structure of the problem

   762   is already laid out directly. E.g.\ consider the following canonical

   763   patterns for \<^theory_text>\<open>shows\<close> and \<^theory_text>\<open>obtains\<close>, respectively:

   764 \<close>

   765

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

   767

   768   theorem

   769     fixes x and y

   770     assumes "A x" and "B y"

   771     shows "C x y"

   772   proof -

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

   774     show "C x y" \<proof>

   775   qed

   776

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

   778

   779   theorem

   780     obtains x and y

   781     where "A x" and "B y"

   782   proof -

   783     have "A a" and "B b" \<proof>

   784     then show thesis ..

   785   qed

   786

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

   788

   789 text \<open>

   790   \<^medskip>

   791   Here local facts \<open>\<open>A x\<close>\<close> and \<open>\<open>B y\<close>\<close> are referenced immediately; there is no

   792   need to decompose the logical rule structure again. In the second proof the

   793   final \<^theory_text>\<open>then show thesis ..\<close>'' involves the local rule case \<open>\<And>x y. A x \<Longrightarrow> B

   794   y \<Longrightarrow> thesis\<close> for the particular instance of terms \<open>a\<close> and \<open>b\<close> produced in the

   795   body.

   796 \<close>

   797

   798

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

   800

   801 text \<open>

   802   By breaking up the grammar for the Isar proof language, we may understand a

   803   proof text as a linear sequence of individual proof commands. These are

   804   interpreted as transitions of the Isar virtual machine (Isar/VM), which

   805   operates on a block-structured configuration in single steps. This allows

   806   users to write proof texts in an incremental manner, and inspect

   807   intermediate configurations for debugging.

   808

   809   The basic idea is analogous to evaluating algebraic expressions on a stack

   810   machine: \<open>(a + b) \<cdot> c\<close> then corresponds to a sequence of single transitions

   811   for each symbol \<open>(, a, +, b, ), \<cdot>, c\<close>. In Isar the algebraic values are

   812   facts or goals, and the operations are inferences.

   813

   814   \<^medskip>

   815   The Isar/VM state maintains a stack of nodes, each node contains the local

   816   proof context, the linguistic mode, and a pending goal (optional). The mode

   817   determines the type of transition that may be performed next, it essentially

   818   alternates between forward and backward reasoning, with an intermediate

   819   stage for chained facts (see \figref{fig:isar-vm}).

   820

   821   \begin{figure}[htb]

   822   \begin{center}

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

   824   \end{center}

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

   826   \end{figure}

   827

   828   For example, in \<open>state\<close> mode Isar acts like a mathematical scratch-pad,

   829   accepting declarations like \<^theory_text>\<open>fix\<close>, \<^theory_text>\<open>assume\<close>, and claims like \<^theory_text>\<open>have\<close>,

   830   \<^theory_text>\<open>show\<close>. A goal statement changes the mode to \<open>prove\<close>, which means that we

   831   may now refine the problem via \<^theory_text>\<open>unfolding\<close> or \<^theory_text>\<open>proof\<close>. Then we are again

   832   in \<open>state\<close> mode of a proof body, which may issue \<^theory_text>\<open>show\<close> statements to solve

   833   pending subgoals. A concluding \<^theory_text>\<open>qed\<close> will return to the original \<open>state\<close>

   834   mode one level upwards. The subsequent Isar/VM trace indicates block

   835   structure, linguistic mode, goal state, and inferences:

   836 \<close>

   837

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

   839 (*<*)notepad begin

   840 (*>*)

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

   842   have "A \<longrightarrow> B"

   843   proof

   844     assume A

   845     show B

   846       \<proof>

   847   qed

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

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

   850 \<open>begin\<close> \\

   851 \\

   852 \\

   853 \<open>begin\<close> \\

   854 \<open>end\<close> \\

   855 \<open>end\<close> \\

   856 \end{minipage}

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

   858 \<open>prove\<close> \\

   859 \<open>state\<close> \\

   860 \<open>state\<close> \\

   861 \<open>prove\<close> \\

   862 \<open>state\<close> \\

   863 \<open>state\<close> \\

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

   865 \<open>(A \<longrightarrow> B) \<Longrightarrow> #(A \<longrightarrow> B)\<close> \\

   866 \<open>(A \<Longrightarrow> B) \<Longrightarrow> #(A \<longrightarrow> B)\<close> \\

   867 \\

   868 \\

   869 \<open>#(A \<longrightarrow> B)\<close> \\

   870 \<open>A \<longrightarrow> B\<close> \\

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

   872 \<open>(init)\<close> \\

   873 \<open>(resolution impI)\<close> \\

   874 \\

   875 \\

   876 \<open>(refinement #A \<Longrightarrow> B)\<close> \\

   877 \<open>(finish)\<close> \\

   878 \end{minipage}\<close>

   879 (*<*)

   880 end

   881 (*>*)

   882 text_raw \<open>\endgroup\<close>

   883

   884 text \<open>

   885   Here the @{inference refinement} inference from

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

   887   nicely. Observe that this principle incorporates some degree of freedom in

   888   proof composition. In particular, the proof body allows parameters and

   889   assumptions to be re-ordered, or commuted according to Hereditary Harrop

   890   Form. Moreover, context elements that are not used in a subproof may be

   891   omitted altogether. For example:

   892 \<close>

   893

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

   895

   896 (*<*)

   897 notepad

   898 begin

   899 (*>*)

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

   901   proof -

   902     fix x and y

   903     assume "A x" and "B y"

   904     show "C x y" \<proof>

   905   qed

   906

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

   908

   909 (*<*)

   910 next

   911 (*>*)

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

   913   proof -

   914     fix x assume "A x"

   915     fix y assume "B y"

   916     show "C x y" \<proof>

   917   qed

   918

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

   920

   921 (*<*)

   922 next

   923 (*>*)

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

   925   proof -

   926     fix y assume "B y"

   927     fix x assume "A x"

   928     show "C x y" \<proof>

   929   qed

   930

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

   932 (*<*)

   933 next

   934 (*>*)

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

   936   proof -

   937     fix y assume "B y"

   938     fix x

   939     show "C x y" \<proof>

   940   qed

   941 (*<*)

   942 end

   943 (*>*)

   944

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

   946

   947 text \<open>

   948   \<^medskip>

   949   Such fine-tuning of Isar text is practically important to improve

   950   readability. Contexts elements are rearranged according to the natural flow

   951   of reasoning in the body, while still observing the overall scoping rules.

   952

   953   \<^medskip>

   954   This illustrates the basic idea of structured proof processing in Isar. The

   955   main mechanisms are based on natural deduction rule composition within the

   956   Pure framework. In particular, there are no direct operations on goal states

   957   within the proof body. Moreover, there is no hidden automated reasoning

   958   involved, just plain unification.

   959 \<close>

   960

   961

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

   963

   964 text \<open>

   965   The existing Isar infrastructure is sufficiently flexible to support

   966   calculational reasoning (chains of transitivity steps) as derived concept.

   967   The generic proof elements introduced below depend on rules declared as

   968   @{attribute trans} in the context. It is left to the object-logic to provide

   969   a suitable rule collection for mixed relations of \<open>=\<close>, \<open><\<close>, \<open>\<le>\<close>, \<open>\<subset>\<close>, \<open>\<subseteq>\<close>

   970   etc. Due to the flexibility of rule composition

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

   972   covered as well, even substitution of inequalities involving monotonicity

   973   conditions; see also @{cite \<open>\S6\<close> "Wenzel-PhD"} and @{cite

   974   "Bauer-Wenzel:2001"}.

   975

   976   The generic calculational mechanism is based on the observation that rules

   977   such as \<open>trans:\<close>~@{prop "x = y \<Longrightarrow> y = z \<Longrightarrow> x = z"} proceed from the premises

   978   towards the conclusion in a deterministic fashion. Thus we may reason in

   979   forward mode, feeding intermediate results into rules selected from the

   980   context. The course of reasoning is organized by maintaining a secondary

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

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

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

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

   985   \<open>trans\<close> represents to a suitable rule from the context:

   986

   987   \begin{matharray}{rcl}

   988     \<^theory_text>\<open>also"\<^sub>0"\<close> & \equiv & \<^theory_text>\<open>note calculation = this\<close> \\

   989     \<^theory_text>\<open>also"\<^sub>n\<^sub>+\<^sub>1"\<close> & \equiv & \<^theory_text>\<open>note calculation = trans [OF calculation this]\<close> \\[0.5ex]

   990     \<^theory_text>\<open>finally\<close> & \equiv & \<^theory_text>\<open>also from calculation\<close> \\

   991   \end{matharray}

   992

   993   The start of a calculation is determined implicitly in the text: here

   994   \<^theory_text>\<open>also\<close> sets @{fact calculation} to the current result; any subsequent

   995   occurrence will update @{fact calculation} by combination with the next

   996   result and a transitivity rule. The calculational sequence is concluded via

   997   \<^theory_text>\<open>finally\<close>, where the final result is exposed for use in a concluding claim.

   998

   999   Here is a canonical proof pattern, using \<^theory_text>\<open>have\<close> to establish the

  1000   intermediate results:

  1001 \<close>

  1002

  1003 (*<*)

  1004 notepad

  1005 begin

  1006   fix a b c d :: 'a

  1007 (*>*)

  1008   have "a = b" \<proof>

  1009   also have "\<dots> = c" \<proof>

  1010   also have "\<dots> = d" \<proof>

  1011   finally have "a = d" .

  1012 (*<*)

  1013 end

  1014 (*>*)

  1015

  1016 text \<open>

  1017   The term \<open>\<dots>\<close>'' (literal ellipsis) is a special abbreviation provided by

  1018   the Isabelle/Isar term syntax: it statically refers to the right-hand side

  1019   argument of the previous statement given in the text. Thus it happens to

  1020   coincide with relevant sub-expressions in the calculational chain, but the

  1021   exact correspondence is dependent on the transitivity rules being involved.

  1022

  1023   \<^medskip>

  1024   Symmetry rules such as @{prop "x = y \<Longrightarrow> y = x"} are like transitivities with

  1025   only one premise. Isar maintains a separate rule collection declared via the

  1026   @{attribute sym} attribute, to be used in fact expressions \<open>a

  1027   [symmetric]\<close>'', or single-step proofs \<^theory_text>\<open>assume "x = y" then have "y = x"

  1028   ..\<close>''.

  1029 \<close>

  1030

  1031 end