summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Wed, 10 Feb 2016 09:32:16 +0100 | |

changeset 62275 | 374d1b6c473d |

parent 62274 | 199f4d6dab0a |

child 62276 | bed456ada96e |

tuned whitespace;

--- a/src/Doc/Isar_Ref/Framework.thy Sun Feb 07 21:39:10 2016 +0100 +++ b/src/Doc/Isar_Ref/Framework.thy Wed Feb 10 09:32:16 2016 +0100 @@ -8,75 +8,67 @@ text \<open> Isabelle/Isar @{cite "Wenzel:1999:TPHOL" and "Wenzel-PhD" and - "Nipkow-TYPES02" and "Wenzel-Paulson:2006" and "Wenzel:2006:Festschrift"} - is intended as a generic framework for developing formal - mathematical documents with full proof checking. Definitions and - proofs are organized as theories. An assembly of theory sources may - be presented as a printed document; see also - \chref{ch:document-prep}. + "Nipkow-TYPES02" and "Wenzel-Paulson:2006" and "Wenzel:2006:Festschrift"} is + intended as a generic framework for developing formal mathematical documents + with full proof checking. Definitions and proofs are organized as theories. + An assembly of theory sources may be presented as a printed document; see + also \chref{ch:document-prep}. - The main objective of Isar is the design of a human-readable - structured proof language, which is called the ``primary proof - format'' in Isar terminology. Such a primary proof language is - somewhere in the middle between the extremes of primitive proof - objects and actual natural language. In this respect, Isar is a bit - more formalistic than Mizar @{cite "Trybulec:1993:MizarFeatures" and - "Rudnicki:1992:MizarOverview" and "Wiedijk:1999:Mizar"}, - using logical symbols for certain reasoning schemes where Mizar - would prefer English words; see @{cite "Wenzel-Wiedijk:2002"} for - further comparisons of these systems. + The main objective of Isar is the design of a human-readable structured + proof language, which is called the ``primary proof format'' in Isar + terminology. Such a primary proof language is somewhere in the middle + between the extremes of primitive proof objects and actual natural language. + In this respect, Isar is a bit more formalistic than Mizar @{cite + "Trybulec:1993:MizarFeatures" and "Rudnicki:1992:MizarOverview" and + "Wiedijk:1999:Mizar"}, using logical symbols for certain reasoning schemes + where Mizar would prefer English words; see @{cite "Wenzel-Wiedijk:2002"} + for further comparisons of these systems. - So Isar challenges the traditional way of recording informal proofs - in mathematical prose, as well as the common tendency to see fully - formal proofs directly as objects of some logical calculus (e.g.\ - \<open>\<lambda>\<close>-terms in a version of type theory). In fact, Isar is - better understood as an interpreter of a simple block-structured - language for describing the data flow of local facts and goals, - interspersed with occasional invocations of proof methods. - Everything is reduced to logical inferences internally, but these - steps are somewhat marginal compared to the overall bookkeeping of - the interpretation process. Thanks to careful design of the syntax - and semantics of Isar language elements, a formal record of Isar - instructions may later appear as an intelligible text to the - attentive reader. + So Isar challenges the traditional way of recording informal proofs in + mathematical prose, as well as the common tendency to see fully formal + proofs directly as objects of some logical calculus (e.g.\ \<open>\<lambda>\<close>-terms in a + version of type theory). In fact, Isar is better understood as an + interpreter of a simple block-structured language for describing the data + flow of local facts and goals, interspersed with occasional invocations of + proof methods. Everything is reduced to logical inferences internally, but + these steps are somewhat marginal compared to the overall bookkeeping of the + interpretation process. Thanks to careful design of the syntax and semantics + of Isar language elements, a formal record of Isar instructions may later + appear as an intelligible text to the attentive reader. - The Isar proof language has emerged from careful analysis of some - inherent virtues of the existing logical framework of Isabelle/Pure - @{cite "paulson-found" and "paulson700"}, notably composition of higher-order - natural deduction rules, which is a generalization of Gentzen's - original calculus @{cite "Gentzen:1935"}. The approach of generic - inference systems in Pure is continued by Isar towards actual proof - texts. + The Isar proof language has emerged from careful analysis of some inherent + virtues of the existing logical framework of Isabelle/Pure @{cite + "paulson-found" and "paulson700"}, notably composition of higher-order + natural deduction rules, which is a generalization of Gentzen's original + calculus @{cite "Gentzen:1935"}. The approach of generic inference systems + in Pure is continued by Isar towards actual proof texts. - Concrete applications require another intermediate layer: an - object-logic. Isabelle/HOL @{cite "isa-tutorial"} (simply-typed - set-theory) is being used most of the time; Isabelle/ZF - @{cite "isabelle-ZF"} is less extensively developed, although it would - probably fit better for classical mathematics. + Concrete applications require another intermediate layer: an object-logic. + Isabelle/HOL @{cite "isa-tutorial"} (simply-typed set-theory) is being used + most of the time; Isabelle/ZF @{cite "isabelle-ZF"} is less extensively + developed, although it would probably fit better for classical mathematics. \<^medskip> - In order to illustrate natural deduction in Isar, we shall - refer to the background theory and library of Isabelle/HOL. This - includes common notions of predicate logic, naive set-theory etc.\ - using fairly standard mathematical notation. From the perspective - of generic natural deduction there is nothing special about the - logical connectives of HOL (\<open>\<and>\<close>, \<open>\<or>\<close>, \<open>\<forall>\<close>, - \<open>\<exists>\<close>, etc.), only the resulting reasoning principles are - relevant to the user. There are similar rules available for - set-theory operators (\<open>\<inter>\<close>, \<open>\<union>\<close>, \<open>\<Inter>\<close>, \<open>\<Union>\<close>, etc.), or any other theory developed in the library (lattice + In order to illustrate natural deduction in Isar, we shall refer to the + background theory and library of Isabelle/HOL. This includes common notions + of predicate logic, naive set-theory etc.\ using fairly standard + mathematical notation. From the perspective of generic natural deduction + there is nothing special about the logical connectives of HOL (\<open>\<and>\<close>, \<open>\<or>\<close>, + \<open>\<forall>\<close>, \<open>\<exists>\<close>, etc.), only the resulting reasoning principles are relevant to the + user. There are similar rules available for set-theory operators (\<open>\<inter>\<close>, \<open>\<union>\<close>, + \<open>\<Inter>\<close>, \<open>\<Union>\<close>, etc.), or any other theory developed in the library (lattice theory, topology etc.). - Subsequently we briefly review fragments of Isar proof texts - corresponding directly to such general deduction schemes. The - examples shall refer to set-theory, to minimize the danger of - understanding connectives of predicate logic as something special. + Subsequently we briefly review fragments of Isar proof texts corresponding + directly to such general deduction schemes. The examples shall refer to + set-theory, to minimize the danger of understanding connectives of predicate + logic as something special. \<^medskip> - The following deduction performs \<open>\<inter>\<close>-introduction, - working forwards from assumptions towards the conclusion. We give - both the Isar text, and depict the primitive rule involved, as - determined by unification of the problem against rules that are - declared in the library context. + The following deduction performs \<open>\<inter>\<close>-introduction, working forwards from + assumptions towards the conclusion. We give both the Isar text, and depict + the primitive rule involved, as determined by unification of the problem + against rules that are declared in the library context. \<close> text_raw \<open>\medskip\begin{minipage}{0.6\textwidth}\<close> @@ -101,13 +93,12 @@ text \<open> \<^medskip> - Note that @{command assume} augments the proof - context, @{command then} indicates that the current fact shall be - used in the next step, and @{command have} states an intermediate - goal. The two dots ``@{command ".."}'' refer to a complete proof of - this claim, using the indicated facts and a canonical rule from the - context. We could have been more explicit here by spelling out the - final proof step via the @{command "by"} command: + Note that @{command assume} augments the proof context, @{command then} + indicates that the current fact shall be used in the next step, and + @{command have} states an intermediate goal. The two dots ``@{command + ".."}'' refer to a complete proof of this claim, using the indicated facts + and a canonical rule from the context. We could have been more explicit here + by spelling out the final proof step via the @{command "by"} command: \<close> (*<*) @@ -121,14 +112,14 @@ (*>*) text \<open> - The format of the \<open>\<inter>\<close>-introduction rule represents - the most basic inference, which proceeds from given premises to a - conclusion, without any nested proof context involved. + The format of the \<open>\<inter>\<close>-introduction rule represents the most basic inference, + which proceeds from given premises to a conclusion, without any nested proof + context involved. - The next example performs backwards introduction on @{term "\<Inter>\<A>"}, - the intersection of all sets within a given set. This requires a - nested proof of set membership within a local context, where @{term - A} is an arbitrary-but-fixed member of the collection: + The next example performs backwards introduction on @{term "\<Inter>\<A>"}, the + intersection of all sets within a given set. This requires a nested proof of + set membership within a local context, where @{term A} is an + arbitrary-but-fixed member of the collection: \<close> text_raw \<open>\medskip\begin{minipage}{0.6\textwidth}\<close> @@ -157,27 +148,24 @@ text \<open> \<^medskip> - This Isar reasoning pattern again refers to the - primitive rule depicted above. The system determines it in the - ``@{command proof}'' step, which could have been spelled out more - explicitly as ``@{command proof}~\<open>(rule InterI)\<close>''. Note - that the rule involves both a local parameter @{term "A"} and an - assumption @{prop "A \<in> \<A>"} in the nested reasoning. This kind of + This Isar reasoning pattern again refers to the primitive rule depicted + above. The system determines it in the ``@{command proof}'' step, which + could have been spelled out more explicitly as ``@{command proof}~\<open>(rule + InterI)\<close>''. Note that the rule involves both a local parameter @{term "A"} + and an assumption @{prop "A \<in> \<A>"} in the nested reasoning. This kind of compound rule typically demands a genuine sub-proof in Isar, working - backwards rather than forwards as seen before. In the proof body we - encounter the @{command fix}-@{command assume}-@{command show} - outline of nested sub-proofs that is typical for Isar. The final - @{command show} is like @{command have} followed by an additional - refinement of the enclosing claim, using the rule derived from the - proof body. + backwards rather than forwards as seen before. In the proof body we + encounter the @{command fix}-@{command assume}-@{command show} outline of + nested sub-proofs that is typical for Isar. The final @{command show} is + like @{command have} followed by an additional refinement of the enclosing + claim, using the rule derived from the proof body. \<^medskip> - The next example involves @{term "\<Union>\<A>"}, which can be - characterized as the set of all @{term "x"} such that @{prop "\<exists>A. x - \<in> A \<and> A \<in> \<A>"}. The elimination rule for @{prop "x \<in> \<Union>\<A>"} does - not mention \<open>\<exists>\<close> and \<open>\<and>\<close> at all, but admits to obtain - directly a local @{term "A"} such that @{prop "x \<in> A"} and @{prop "A - \<in> \<A>"} hold. This corresponds to the following Isar proof and + The next example involves @{term "\<Union>\<A>"}, which can be characterized as the + set of all @{term "x"} such that @{prop "\<exists>A. x \<in> A \<and> A \<in> \<A>"}. The + elimination rule for @{prop "x \<in> \<Union>\<A>"} does not mention \<open>\<exists>\<close> and \<open>\<and>\<close> at all, + but admits to obtain directly a local @{term "A"} such that @{prop "x \<in> A"} + and @{prop "A \<in> \<A>"} hold. This corresponds to the following Isar proof and inference rule, respectively: \<close> @@ -208,14 +196,13 @@ text \<open> \<^medskip> - Although the Isar proof follows the natural - deduction rule closely, the text reads not as natural as - anticipated. There is a double occurrence of an arbitrary - conclusion @{prop "C"}, which represents the final result, but is - irrelevant for now. This issue arises for any elimination rule - involving local parameters. Isar provides the derived language - element @{command obtain}, which is able to perform the same - elimination proof more conveniently: + Although the Isar proof follows the natural deduction rule closely, the text + reads not as natural as anticipated. There is a double occurrence of an + arbitrary conclusion @{prop "C"}, which represents the final result, but is + irrelevant for now. This issue arises for any elimination rule involving + local parameters. Isar provides the derived language element @{command + obtain}, which is able to perform the same elimination proof more + conveniently: \<close> (*<*) @@ -229,9 +216,9 @@ (*>*) text \<open> - Here we avoid to mention the final conclusion @{prop "C"} - and return to plain forward reasoning. The rule involved in the - ``@{command ".."}'' proof is the same as before. + Here we avoid to mention the final conclusion @{prop "C"} and return to + plain forward reasoning. The rule involved in the ``@{command ".."}'' proof + is the same as before. \<close> @@ -239,9 +226,9 @@ text \<open> The Pure logic @{cite "paulson-found" and "paulson700"} is an intuitionistic - fragment of higher-order logic @{cite "church40"}. In type-theoretic - parlance, there are three levels of \<open>\<lambda>\<close>-calculus with - corresponding arrows \<open>\<Rightarrow>\<close>/\<open>\<And>\<close>/\<open>\<Longrightarrow>\<close>: + fragment of higher-order logic @{cite "church40"}. In type-theoretic + parlance, there are three levels of \<open>\<lambda>\<close>-calculus with corresponding arrows + \<open>\<Rightarrow>\<close>/\<open>\<And>\<close>/\<open>\<Longrightarrow>\<close>: \<^medskip> \begin{tabular}{ll} @@ -251,36 +238,31 @@ \end{tabular} \<^medskip> - Here only the types of syntactic terms, and the - propositions of proof terms have been shown. The \<open>\<lambda>\<close>-structure of proofs can be recorded as an optional feature of - the Pure inference kernel @{cite "Berghofer-Nipkow:2000:TPHOL"}, but - the formal system can never depend on them due to \<^emph>\<open>proof - irrelevance\<close>. + Here only the types of syntactic terms, and the propositions of proof terms + have been shown. The \<open>\<lambda>\<close>-structure of proofs can be recorded as an optional + feature of the Pure inference kernel @{cite "Berghofer-Nipkow:2000:TPHOL"}, + but the formal system can never depend on them due to \<^emph>\<open>proof irrelevance\<close>. - On top of this most primitive layer of proofs, Pure implements a - generic calculus for nested natural deduction rules, similar to - @{cite "Schroeder-Heister:1984"}. Here object-logic inferences are - internalized as formulae over \<open>\<And>\<close> and \<open>\<Longrightarrow>\<close>. - Combining such rule statements may involve higher-order unification - @{cite "paulson-natural"}. + On top of this most primitive layer of proofs, Pure implements a generic + calculus for nested natural deduction rules, similar to @{cite + "Schroeder-Heister:1984"}. Here object-logic inferences are internalized as + formulae over \<open>\<And>\<close> and \<open>\<Longrightarrow>\<close>. Combining such rule statements may involve + higher-order unification @{cite "paulson-natural"}. \<close> subsection \<open>Primitive inferences\<close> text \<open> - Term syntax provides explicit notation for abstraction \<open>\<lambda>x :: - \<alpha>. b(x)\<close> and application \<open>b a\<close>, while types are usually - implicit thanks to type-inference; terms of type \<open>prop\<close> are - called propositions. Logical statements are composed via \<open>\<And>x - :: \<alpha>. B(x)\<close> and \<open>A \<Longrightarrow> B\<close>. Primitive reasoning operates on - judgments of the form \<open>\<Gamma> \<turnstile> \<phi>\<close>, with standard introduction - and elimination rules for \<open>\<And>\<close> and \<open>\<Longrightarrow>\<close> that refer to - fixed parameters \<open>x\<^sub>1, \<dots>, x\<^sub>m\<close> and hypotheses - \<open>A\<^sub>1, \<dots>, A\<^sub>n\<close> from the context \<open>\<Gamma>\<close>; - the corresponding proof terms are left implicit. The subsequent - inference rules define \<open>\<Gamma> \<turnstile> \<phi>\<close> inductively, relative to a - collection of axioms: + Term syntax provides explicit notation for abstraction \<open>\<lambda>x :: \<alpha>. b(x)\<close> and + application \<open>b a\<close>, while types are usually implicit thanks to + type-inference; terms of type \<open>prop\<close> are called propositions. Logical + statements are composed via \<open>\<And>x :: \<alpha>. B(x)\<close> and \<open>A \<Longrightarrow> B\<close>. Primitive reasoning + operates on judgments of the form \<open>\<Gamma> \<turnstile> \<phi>\<close>, with standard introduction and + elimination rules for \<open>\<And>\<close> and \<open>\<Longrightarrow>\<close> that refer to fixed parameters \<open>x\<^sub>1, \<dots>, + x\<^sub>m\<close> and hypotheses \<open>A\<^sub>1, \<dots>, A\<^sub>n\<close> from the context \<open>\<Gamma>\<close>; the corresponding + proof terms are left implicit. The subsequent inference rules define \<open>\<Gamma> \<turnstile> \<phi>\<close> + inductively, relative to a collection of axioms: \[ \infer{\<open>\<turnstile> A\<close>}{(\<open>A\<close> \mbox{~axiom})} @@ -300,68 +282,60 @@ \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>} \] - Furthermore, Pure provides a built-in equality \<open>\<equiv> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> - prop\<close> with axioms for reflexivity, substitution, extensionality, - and \<open>\<alpha>\<beta>\<eta>\<close>-conversion on \<open>\<lambda>\<close>-terms. + Furthermore, Pure provides a built-in equality \<open>\<equiv> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> prop\<close> with + axioms for reflexivity, substitution, extensionality, and \<open>\<alpha>\<beta>\<eta>\<close>-conversion + on \<open>\<lambda>\<close>-terms. \<^medskip> - An object-logic introduces another layer on top of Pure, - e.g.\ with types \<open>i\<close> for individuals and \<open>o\<close> for - propositions, term constants \<open>Trueprop :: o \<Rightarrow> prop\<close> as - (implicit) derivability judgment and connectives like \<open>\<and> :: o - \<Rightarrow> o \<Rightarrow> o\<close> or \<open>\<forall> :: (i \<Rightarrow> o) \<Rightarrow> o\<close>, and axioms for object-level - rules such as \<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 are represented as theorems of - Pure. After the initial object-logic setup, further axiomatizations - are usually avoided; plain definitions and derived principles are - used exclusively. + An object-logic introduces another layer on top of Pure, e.g.\ with types + \<open>i\<close> for individuals and \<open>o\<close> for propositions, term constants \<open>Trueprop :: o + \<Rightarrow> prop\<close> as (implicit) derivability judgment and connectives like \<open>\<and> :: o \<Rightarrow> o + \<Rightarrow> o\<close> or \<open>\<forall> :: (i \<Rightarrow> o) \<Rightarrow> o\<close>, and axioms for object-level rules such as + \<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 + are represented as theorems of Pure. After the initial object-logic setup, + further axiomatizations are usually avoided; plain definitions and derived + principles are used exclusively. \<close> subsection \<open>Reasoning with rules \label{sec:framework-resolution}\<close> text \<open> - Primitive inferences mostly serve foundational purposes. The main - reasoning mechanisms of Pure operate on nested natural deduction - rules expressed as formulae, using \<open>\<And>\<close> to bind local - parameters and \<open>\<Longrightarrow>\<close> to express entailment. Multiple - parameters and premises are represented by repeating these + Primitive inferences mostly serve foundational purposes. The main reasoning + mechanisms of Pure operate on nested natural deduction rules expressed as + formulae, using \<open>\<And>\<close> to bind local parameters and \<open>\<Longrightarrow>\<close> to express entailment. + Multiple parameters and premises are represented by repeating these connectives in a right-associative manner. - Since \<open>\<And>\<close> and \<open>\<Longrightarrow>\<close> commute thanks to the theorem - @{prop "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}, we may assume w.l.o.g.\ - that rule statements always observe the normal form where - quantifiers are pulled in front of implications at each level of - nesting. This means that any Pure proposition may be presented as a - \<^emph>\<open>Hereditary Harrop Formula\<close> @{cite "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 \<ge> 0\<close>, and \<open>A\<close> atomic, and \<open>H\<^sub>1, \<dots>, H\<^sub>n\<close> being recursively of the same format. - Following the convention that outermost quantifiers are implicit, - Horn clauses \<open>A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> A\<close> are a special - case of this. + Since \<open>\<And>\<close> and \<open>\<Longrightarrow>\<close> commute thanks to the theorem @{prop "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> + (\<And>x. A \<Longrightarrow> B x)"}, we may assume w.l.o.g.\ that rule statements always observe + the normal form where quantifiers are pulled in front of implications at + each level of nesting. This means that any Pure proposition may be presented + as a \<^emph>\<open>Hereditary Harrop Formula\<close> @{cite "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 \<ge> 0\<close>, and \<open>A\<close> atomic, and \<open>H\<^sub>1, \<dots>, + H\<^sub>n\<close> being recursively of the same format. Following the convention that + outermost quantifiers are implicit, Horn clauses \<open>A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> A\<close> are a + special case of this. - For example, \<open>\<inter>\<close>-introduction rule encountered before is - represented as a Pure theorem as follows: + For example, \<open>\<inter>\<close>-introduction rule encountered before is represented as a + Pure theorem as follows: \[ \<open>IntI:\<close>~@{prop "x \<in> A \<Longrightarrow> x \<in> B \<Longrightarrow> x \<in> A \<inter> B"} \] - This is a plain Horn clause, since no further nesting on - the left is involved. The general \<open>\<Inter>\<close>-introduction - corresponds to a Hereditary Harrop Formula with one additional level - of nesting: + This is a plain Horn clause, since no further nesting on the left is + involved. The general \<open>\<Inter>\<close>-introduction corresponds to a Hereditary Harrop + Formula with one additional level of nesting: \[ \<open>InterI:\<close>~@{prop "(\<And>A. A \<in> \<A> \<Longrightarrow> x \<in> A) \<Longrightarrow> x \<in> \<Inter>\<A>"} \] \<^medskip> - Goals are also represented as rules: \<open>A\<^sub>1 \<Longrightarrow> - \<dots> A\<^sub>n \<Longrightarrow> C\<close> states that the sub-goals \<open>A\<^sub>1, \<dots>, - A\<^sub>n\<close> entail the result \<open>C\<close>; for \<open>n = 0\<close> the - goal is finished. To allow \<open>C\<close> being a rule statement - itself, we introduce the protective marker \<open># :: prop \<Rightarrow> - prop\<close>, which is defined as identity and hidden from the user. We - initialize and finish goal states as follows: + Goals are also represented as rules: \<open>A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> C\<close> states that the + sub-goals \<open>A\<^sub>1, \<dots>, A\<^sub>n\<close> entail the result \<open>C\<close>; for \<open>n = 0\<close> the goal is + finished. To allow \<open>C\<close> being a rule statement itself, we introduce the + protective marker \<open># :: prop \<Rightarrow> prop\<close>, which is defined as identity and + hidden from the user. We initialize and finish goal states as follows: \[ \begin{array}{c@ {\qquad}c} @@ -370,12 +344,12 @@ \end{array} \] - Goal states are refined in intermediate proof steps until - a finished form is achieved. Here the two main reasoning principles - are @{inference resolution}, for back-chaining a rule against a - sub-goal (replacing it by zero or more sub-goals), and @{inference - assumption}, for solving a sub-goal (finding a short-circuit with - local assumptions). Below \<open>\<^vec>x\<close> stands for \<open>x\<^sub>1, \<dots>, x\<^sub>n\<close> (\<open>n \<ge> 0\<close>). + Goal states are refined in intermediate proof steps until a finished form is + achieved. Here the two main reasoning principles are @{inference + resolution}, for back-chaining a rule against a sub-goal (replacing it by + zero or more sub-goals), and @{inference assumption}, for solving a sub-goal + (finding a short-circuit with local assumptions). Below \<open>\<^vec>x\<close> stands + for \<open>x\<^sub>1, \<dots>, x\<^sub>n\<close> (\<open>n \<ge> 0\<close>). \[ \infer[(@{inference_def resolution})] @@ -418,13 +392,12 @@ \<^medskip> } - Compositions of @{inference assumption} after @{inference - resolution} occurs quite often, typically in elimination steps. - Traditional Isabelle tactics accommodate this by a combined - @{inference_def elim_resolution} principle. In contrast, Isar uses - a slightly more refined combination, where the assumptions to be - closed are marked explicitly, using again the protective marker - \<open>#\<close>: + Compositions of @{inference assumption} after @{inference resolution} occurs + quite often, typically in elimination steps. Traditional Isabelle tactics + accommodate this by a combined @{inference_def elim_resolution} principle. + In contrast, Isar uses a slightly more refined combination, where the + assumptions to be closed are marked explicitly, using again the protective + marker \<open>#\<close>: \[ \infer[(@{inference refinement})] @@ -442,32 +415,30 @@ \end{tabular}} \] - Here the \<open>sub\<hyphen>proof\<close> rule stems from the - main @{command fix}-@{command assume}-@{command show} outline of - Isar (cf.\ \secref{sec:framework-subproof}): each assumption - indicated in the text results in a marked premise \<open>G\<close> above. - The marking enforces resolution against one of the sub-goal's - premises. Consequently, @{command fix}-@{command assume}-@{command - show} enables to fit the result of a sub-proof quite robustly into a - pending sub-goal, while maintaining a good measure of flexibility. + Here the \<open>sub\<hyphen>proof\<close> rule stems from the main @{command fix}-@{command + assume}-@{command show} outline of Isar (cf.\ + \secref{sec:framework-subproof}): each assumption indicated in the text + results in a marked premise \<open>G\<close> above. The marking enforces resolution + against one of the sub-goal's premises. Consequently, @{command + fix}-@{command assume}-@{command show} enables to fit the result of a + sub-proof quite robustly into a pending sub-goal, while maintaining a good + measure of flexibility. \<close> section \<open>The Isar proof language \label{sec:framework-isar}\<close> text \<open> - Structured proofs are presented as high-level expressions for - composing entities of Pure (propositions, facts, and goals). The - Isar proof language allows to organize reasoning within the - underlying rule calculus of Pure, but Isar is not another logical - calculus! + Structured proofs are presented as high-level expressions for composing + entities of Pure (propositions, facts, and goals). The Isar proof language + allows to organize reasoning within the underlying rule calculus of Pure, + but Isar is not another logical calculus! - Isar is an exercise in sound minimalism. Approximately half of the - language is introduced as primitive, the rest defined as derived - concepts. The following grammar describes the core language - (category \<open>proof\<close>), which is embedded into theory - specification elements such as @{command theorem}; see also - \secref{sec:framework-stmt} for the separate category \<open>statement\<close>. + Isar is an exercise in sound minimalism. Approximately half of the language + is introduced as primitive, the rest defined as derived concepts. The + following grammar describes the core language (category \<open>proof\<close>), which is + embedded into theory specification elements such as @{command theorem}; see + also \secref{sec:framework-stmt} for the separate category \<open>statement\<close>. \<^medskip> \begin{tabular}{rcl} @@ -490,31 +461,28 @@ \end{tabular} \<^medskip> - Simultaneous propositions or facts may be separated by the - @{keyword "and"} keyword. + Simultaneous propositions or facts may be separated by the @{keyword "and"} + keyword. \<^medskip> - The syntax for terms and propositions is inherited from - Pure (and the object-logic). A \<open>pattern\<close> is a \<open>term\<close> with schematic variables, to be bound by higher-order - matching. + The syntax for terms and propositions is inherited from Pure (and the + object-logic). A \<open>pattern\<close> is a \<open>term\<close> with schematic variables, to be bound + by higher-order matching. \<^medskip> - Facts may be referenced by name or proposition. For - example, the result of ``@{command have}~\<open>a: A \<langle>proof\<rangle>\<close>'' - becomes available both as \<open>a\<close> and - \isacharbackquoteopen\<open>A\<close>\isacharbackquoteclose. Moreover, - fact expressions may involve attributes that modify either the - theorem or the background context. For example, the expression - ``\<open>a [OF b]\<close>'' refers to the composition of two facts - according to the @{inference resolution} inference of - \secref{sec:framework-resolution}, while ``\<open>a [intro]\<close>'' - declares a fact as introduction rule in the context. + Facts may be referenced by name or proposition. For example, the result of + ``@{command have}~\<open>a: A \<langle>proof\<rangle>\<close>'' becomes available both as \<open>a\<close> and + \isacharbackquoteopen\<open>A\<close>\isacharbackquoteclose. Moreover, fact expressions + may involve attributes that modify either the theorem or the background + context. For example, the expression ``\<open>a [OF b]\<close>'' refers to the + composition of two facts according to the @{inference resolution} inference + of \secref{sec:framework-resolution}, while ``\<open>a [intro]\<close>'' declares a fact + as introduction rule in the context. - The special fact called ``@{fact this}'' always refers to the last - result, as produced by @{command note}, @{command assume}, @{command - have}, or @{command show}. Since @{command note} occurs - frequently together with @{command then} we provide some - abbreviations: + The special fact called ``@{fact this}'' always refers to the last result, + as produced by @{command note}, @{command assume}, @{command have}, or + @{command show}. Since @{command note} occurs frequently together with + @{command then} we provide some abbreviations: \<^medskip> \begin{tabular}{rcl} @@ -523,67 +491,63 @@ \end{tabular} \<^medskip> - The \<open>method\<close> category is essentially a parameter and may be - populated later. Methods use the facts indicated by @{command - "then"} or @{command using}, and then operate on the goal state. - Some basic methods are predefined: ``@{method "-"}'' leaves the goal - unchanged, ``@{method this}'' applies the facts as rules to the - goal, ``@{method (Pure) "rule"}'' applies the facts to another rule and the - result to the goal (both ``@{method this}'' and ``@{method (Pure) rule}'' - refer to @{inference resolution} of - \secref{sec:framework-resolution}). The secondary arguments to - ``@{method (Pure) rule}'' may be specified explicitly as in ``\<open>(rule - a)\<close>'', or picked from the context. In the latter case, the system - first tries rules declared as @{attribute (Pure) elim} or - @{attribute (Pure) dest}, followed by those declared as @{attribute - (Pure) intro}. + The \<open>method\<close> category is essentially a parameter and may be populated later. + Methods use the facts indicated by @{command "then"} or @{command using}, + and then operate on the goal state. Some basic methods are predefined: + ``@{method "-"}'' leaves the goal unchanged, ``@{method this}'' applies the + facts as rules to the goal, ``@{method (Pure) "rule"}'' applies the facts to + another rule and the result to the goal (both ``@{method this}'' and + ``@{method (Pure) rule}'' refer to @{inference resolution} of + \secref{sec:framework-resolution}). The secondary arguments to ``@{method + (Pure) rule}'' may be specified explicitly as in ``\<open>(rule a)\<close>'', or picked + from the context. In the latter case, the system first tries rules declared + as @{attribute (Pure) elim} or @{attribute (Pure) dest}, followed by those + declared as @{attribute (Pure) intro}. - The default method for @{command proof} is ``@{method standard}'' - (arguments picked from the context), for @{command qed} it is - ``@{method "succeed"}''. Further abbreviations for terminal proof steps - are ``@{command "by"}~\<open>method\<^sub>1 method\<^sub>2\<close>'' for - ``@{command proof}~\<open>method\<^sub>1\<close>~@{command qed}~\<open>method\<^sub>2\<close>'', and ``@{command ".."}'' for ``@{command - "by"}~@{method standard}, and ``@{command "."}'' for ``@{command - "by"}~@{method this}''. The @{command unfolding} element operates - directly on the current facts and goal by applying equalities. + The default method for @{command proof} is ``@{method standard}'' (arguments + picked from the context), for @{command qed} it is ``@{method "succeed"}''. + Further abbreviations for terminal proof steps are ``@{command + "by"}~\<open>method\<^sub>1 method\<^sub>2\<close>'' for ``@{command proof}~\<open>method\<^sub>1\<close>~@{command + qed}~\<open>method\<^sub>2\<close>'', and ``@{command ".."}'' for ``@{command "by"}~@{method + standard}, and ``@{command "."}'' for ``@{command "by"}~@{method this}''. + The @{command unfolding} element operates directly on the current facts and + goal by applying equalities. \<^medskip> Block structure can be indicated explicitly by ``@{command - "{"}~\<open>\<dots>\<close>~@{command "}"}'', although the body of a sub-proof - already involves implicit nesting. In any case, @{command next} - jumps into the next section of a block, i.e.\ it acts like closing - an implicit block scope and opening another one; there is no direct - correspondence to subgoals here. + "{"}~\<open>\<dots>\<close>~@{command "}"}'', although the body of a sub-proof already involves + implicit nesting. In any case, @{command next} jumps into the next section + of a block, i.e.\ it acts like closing an implicit block scope and opening + another one; there is no direct correspondence to subgoals here. - The remaining elements @{command fix} and @{command assume} build up - a local context (see \secref{sec:framework-context}), while - @{command show} refines a pending sub-goal by the rule resulting - from a nested sub-proof (see \secref{sec:framework-subproof}). - Further derived concepts will support calculational reasoning (see - \secref{sec:framework-calc}). + The remaining elements @{command fix} and @{command assume} build up a local + context (see \secref{sec:framework-context}), while @{command show} refines + a pending sub-goal by the rule resulting from a nested sub-proof (see + \secref{sec:framework-subproof}). Further derived concepts will support + calculational reasoning (see \secref{sec:framework-calc}). \<close> subsection \<open>Context elements \label{sec:framework-context}\<close> text \<open> - In judgments \<open>\<Gamma> \<turnstile> \<phi>\<close> of the primitive framework, \<open>\<Gamma>\<close> - essentially acts like a proof context. Isar elaborates this idea - towards a higher-level notion, with additional information for - type-inference, term abbreviations, local facts, hypotheses etc. + In judgments \<open>\<Gamma> \<turnstile> \<phi>\<close> of the primitive framework, \<open>\<Gamma>\<close> essentially acts like a + proof context. Isar elaborates this idea towards a higher-level notion, with + additional information for type-inference, term abbreviations, local facts, + hypotheses etc. - The element @{command fix}~\<open>x :: \<alpha>\<close> declares a local - parameter, i.e.\ an arbitrary-but-fixed entity of a given type; in - results exported from the context, \<open>x\<close> may become anything. - The @{command assume}~\<open>\<guillemotleft>inference\<guillemotright>\<close> element provides a - general interface to hypotheses: ``@{command assume}~\<open>\<guillemotleft>inference\<guillemotright> A\<close>'' produces \<open>A \<turnstile> A\<close> locally, while the - included inference tells how to discharge \<open>A\<close> from results - \<open>A \<turnstile> B\<close> later on. There is no user-syntax for \<open>\<guillemotleft>inference\<guillemotright>\<close>, i.e.\ it may only occur internally when derived - commands are defined in ML. + The element @{command fix}~\<open>x :: \<alpha>\<close> declares a local parameter, i.e.\ an + arbitrary-but-fixed entity of a given type; in results exported from the + context, \<open>x\<close> may become anything. The @{command assume}~\<open>\<guillemotleft>inference\<guillemotright>\<close> + element provides a general interface to hypotheses: ``@{command + assume}~\<open>\<guillemotleft>inference\<guillemotright> A\<close>'' produces \<open>A \<turnstile> A\<close> locally, while the included + inference tells how to discharge \<open>A\<close> from results \<open>A \<turnstile> B\<close> later on. There is + no user-syntax for \<open>\<guillemotleft>inference\<guillemotright>\<close>, i.e.\ it may only occur internally when + derived commands are defined in ML. At the user-level, the default inference for @{command assume} is - @{inference discharge} as given below. The additional variants - @{command presume} and @{command def} are defined as follows: + @{inference discharge} as given below. The additional variants @{command + presume} and @{command def} are defined as follows: \<^medskip> \begin{tabular}{rcl} @@ -603,19 +567,18 @@ \] \<^medskip> - Note that @{inference discharge} and @{inference - "weak\<hyphen>discharge"} differ in the marker for @{prop A}, which is - relevant when the result of a @{command fix}-@{command - assume}-@{command show} outline is composed with a pending goal, - cf.\ \secref{sec:framework-subproof}. + Note that @{inference discharge} and @{inference "weak\<hyphen>discharge"} differ in + the marker for @{prop A}, which is relevant when the result of a @{command + fix}-@{command assume}-@{command show} outline is composed with a pending + goal, cf.\ \secref{sec:framework-subproof}. - The most interesting derived context element in Isar is @{command - obtain} @{cite \<open>\S5.3\<close> "Wenzel-PhD"}, which supports generalized - elimination steps in a purely forward manner. The @{command obtain} - command takes a specification of parameters \<open>\<^vec>x\<close> and - assumptions \<open>\<^vec>A\<close> to be added to the context, together - with a proof of a case rule stating that this extension is - conservative (i.e.\ may be removed from closed results later on): + The most interesting derived context element in Isar is @{command obtain} + @{cite \<open>\S5.3\<close> "Wenzel-PhD"}, which supports generalized elimination steps + in a purely forward manner. The @{command obtain} command takes a + specification of parameters \<open>\<^vec>x\<close> and assumptions \<open>\<^vec>A\<close> to be + added to the context, together with a proof of a case rule stating that this + extension is conservative (i.e.\ may be removed from closed results later + on): \<^medskip> \begin{tabular}{l} @@ -640,21 +603,19 @@ \end{tabular}} \] - Here the name ``\<open>thesis\<close>'' is a specific convention - for an arbitrary-but-fixed proposition; in the primitive natural - deduction rules shown before we have occasionally used \<open>C\<close>. - The whole statement of ``@{command obtain}~\<open>x\<close>~@{keyword - "where"}~\<open>A x\<close>'' may be read as a claim that \<open>A x\<close> - may be assumed for some arbitrary-but-fixed \<open>x\<close>. Also note - that ``@{command obtain}~\<open>A \<AND> B\<close>'' without parameters - is similar to ``@{command have}~\<open>A \<AND> B\<close>'', but the - latter involves multiple sub-goals. + Here the name ``\<open>thesis\<close>'' is a specific convention for an + arbitrary-but-fixed proposition; in the primitive natural deduction rules + shown before we have occasionally used \<open>C\<close>. The whole statement of + ``@{command obtain}~\<open>x\<close>~@{keyword "where"}~\<open>A x\<close>'' may be read as a claim + that \<open>A x\<close> may be assumed for some arbitrary-but-fixed \<open>x\<close>. Also note that + ``@{command obtain}~\<open>A \<AND> B\<close>'' without parameters is similar to + ``@{command have}~\<open>A \<AND> B\<close>'', but the latter involves multiple + sub-goals. \<^medskip> - The subsequent Isar proof texts explain all context - elements introduced above using the formal proof language itself. - After finishing a local proof within a block, we indicate the - exported result via @{command note}. + The subsequent Isar proof texts explain all context elements introduced + above using the formal proof language itself. After finishing a local proof + within a block, we indicate the exported result via @{command note}. \<close> (*<*) @@ -692,8 +653,8 @@ text \<open> \<^bigskip> - This illustrates the meaning of Isar context - elements without goals getting in between. + This illustrates the meaning of Isar context elements without goals getting + in between. \<close> @@ -717,18 +678,17 @@ \end{tabular} \<^medskip> - A simple \<open>statement\<close> consists of named - propositions. The full form admits local context elements followed - by the actual conclusions, such as ``@{keyword "fixes"}~\<open>x\<close>~@{keyword "assumes"}~\<open>A x\<close>~@{keyword "shows"}~\<open>B - x\<close>''. The final result emerges as a Pure rule after discharging - the context: @{prop "\<And>x. A x \<Longrightarrow> B x"}. + A simple \<open>statement\<close> consists of named propositions. The full form admits + local context elements followed by the actual conclusions, such as + ``@{keyword "fixes"}~\<open>x\<close>~@{keyword "assumes"}~\<open>A x\<close>~@{keyword "shows"}~\<open>B + x\<close>''. The final result emerges as a Pure rule after discharging the context: + @{prop "\<And>x. A x \<Longrightarrow> B x"}. - The @{keyword "obtains"} variant is another abbreviation defined - below; unlike @{command obtain} (cf.\ - \secref{sec:framework-context}) there may be several ``cases'' - separated by ``\<open>\<BBAR>\<close>'', each consisting of several - parameters (\<open>vars\<close>) and several premises (\<open>props\<close>). - This specifies multi-branch elimination rules. + The @{keyword "obtains"} variant is another abbreviation defined below; + unlike @{command obtain} (cf.\ \secref{sec:framework-context}) there may be + several ``cases'' separated by ``\<open>\<BBAR>\<close>'', each consisting of several + parameters (\<open>vars\<close>) and several premises (\<open>props\<close>). This specifies + multi-branch elimination rules. \<^medskip> \begin{tabular}{l} @@ -740,10 +700,9 @@ \<^medskip> Presenting structured statements in such an ``open'' format usually - simplifies the subsequent proof, because the outer structure of the - problem is already laid out directly. E.g.\ consider the following - canonical patterns for \<open>\<SHOWS>\<close> and \<open>\<OBTAINS>\<close>, - respectively: + simplifies the subsequent proof, because the outer structure of the problem + is already laid out directly. E.g.\ consider the following canonical + patterns for \<open>\<SHOWS>\<close> and \<open>\<OBTAINS>\<close>, respectively: \<close> text_raw \<open>\begin{minipage}{0.5\textwidth}\<close> @@ -771,39 +730,36 @@ text \<open> \<^medskip> - Here local facts \isacharbackquoteopen\<open>A - x\<close>\isacharbackquoteclose\ and \isacharbackquoteopen\<open>B - y\<close>\isacharbackquoteclose\ are referenced immediately; there is no - need to decompose the logical rule structure again. In the second - proof the final ``@{command then}~@{command show}~\<open>thesis\<close>~@{command ".."}'' involves the local rule case \<open>\<And>x - y. A x \<Longrightarrow> B y \<Longrightarrow> thesis\<close> for the particular instance of terms \<open>a\<close> and \<open>b\<close> produced in the body. -\<close> + Here local facts \isacharbackquoteopen\<open>A x\<close>\isacharbackquoteclose\ and + \isacharbackquoteopen\<open>B y\<close>\isacharbackquoteclose\ are referenced + immediately; there is no need to decompose the logical rule structure again. + In the second proof the final ``@{command then}~@{command + show}~\<open>thesis\<close>~@{command ".."}'' involves the local rule case \<open>\<And>x y. A x \<Longrightarrow> B + y \<Longrightarrow> thesis\<close> for the particular instance of terms \<open>a\<close> and \<open>b\<close> produced in the + body. \<close> subsection \<open>Structured proof refinement \label{sec:framework-subproof}\<close> text \<open> - By breaking up the grammar for the Isar proof language, we may - understand a proof text as a linear sequence of individual proof - commands. These are interpreted as transitions of the Isar virtual - machine (Isar/VM), which operates on a block-structured - configuration in single steps. This allows users to write proof - texts in an incremental manner, and inspect intermediate - configurations for debugging. + By breaking up the grammar for the Isar proof language, we may understand a + proof text as a linear sequence of individual proof commands. These are + interpreted as transitions of the Isar virtual machine (Isar/VM), which + operates on a block-structured configuration in single steps. This allows + users to write proof texts in an incremental manner, and inspect + intermediate configurations for debugging. - The basic idea is analogous to evaluating algebraic expressions on a - stack machine: \<open>(a + b) \<cdot> c\<close> then corresponds to a sequence - of single transitions for each symbol \<open>(, a, +, b, ), \<cdot>, c\<close>. - In Isar the algebraic values are facts or goals, and the operations - are inferences. + The basic idea is analogous to evaluating algebraic expressions on a stack + machine: \<open>(a + b) \<cdot> c\<close> then corresponds to a sequence of single transitions + for each symbol \<open>(, a, +, b, ), \<cdot>, c\<close>. In Isar the algebraic values are + facts or goals, and the operations are inferences. \<^medskip> - The Isar/VM state maintains a stack of nodes, each node - contains the local proof context, the linguistic mode, and a pending - goal (optional). The mode determines the type of transition that - may be performed next, it essentially alternates between forward and - backward reasoning, with an intermediate stage for chained facts - (see \figref{fig:isar-vm}). + The Isar/VM state maintains a stack of nodes, each node contains the local + proof context, the linguistic mode, and a pending goal (optional). The mode + determines the type of transition that may be performed next, it essentially + alternates between forward and backward reasoning, with an intermediate + stage for chained facts (see \figref{fig:isar-vm}). \begin{figure}[htb] \begin{center} @@ -812,17 +768,15 @@ \caption{Isar/VM modes}\label{fig:isar-vm} \end{figure} - For example, in \<open>state\<close> mode Isar acts like a mathematical - scratch-pad, accepting declarations like @{command fix}, @{command - assume}, and claims like @{command have}, @{command show}. A goal - statement changes the mode to \<open>prove\<close>, which means that we - may now refine the problem via @{command unfolding} or @{command - proof}. Then we are again in \<open>state\<close> mode of a proof body, - which may issue @{command show} statements to solve pending - sub-goals. A concluding @{command qed} will return to the original - \<open>state\<close> mode one level upwards. The subsequent Isar/VM - trace indicates block structure, linguistic mode, goal state, and - inferences: + For example, in \<open>state\<close> mode Isar acts like a mathematical scratch-pad, + accepting declarations like @{command fix}, @{command assume}, and claims + like @{command have}, @{command show}. A goal statement changes the mode to + \<open>prove\<close>, which means that we may now refine the problem via @{command + unfolding} or @{command proof}. Then we are again in \<open>state\<close> mode of a proof + body, which may issue @{command show} statements to solve pending sub-goals. + A concluding @{command qed} will return to the original \<open>state\<close> mode one + level upwards. The subsequent Isar/VM trace indicates block structure, + linguistic mode, goal state, and inferences: \<close> text_raw \<open>\begingroup\footnotesize\<close> @@ -873,13 +827,12 @@ text \<open> Here the @{inference refinement} inference from - \secref{sec:framework-resolution} mediates composition of Isar - sub-proofs nicely. Observe that this principle incorporates some - degree of freedom in proof composition. In particular, the proof - body allows parameters and assumptions to be re-ordered, or commuted - according to Hereditary Harrop Form. Moreover, context elements - that are not used in a sub-proof may be omitted altogether. For - example: + \secref{sec:framework-resolution} mediates composition of Isar sub-proofs + nicely. Observe that this principle incorporates some degree of freedom in + proof composition. In particular, the proof body allows parameters and + assumptions to be re-ordered, or commuted according to Hereditary Harrop + Form. Moreover, context elements that are not used in a sub-proof may be + omitted altogether. For example: \<close> text_raw \<open>\begin{minipage}{0.5\textwidth}\<close> @@ -937,17 +890,16 @@ text \<open> \<^medskip> - Such ``peephole optimizations'' of Isar texts are - practically important to improve readability, by rearranging - contexts elements according to the natural flow of reasoning in the - body, while still observing the overall scoping rules. + Such ``peephole optimizations'' of Isar texts are practically important to + improve readability, by rearranging contexts elements according to the + natural flow of reasoning in the body, while still observing the overall + scoping rules. \<^medskip> - This illustrates the basic idea of structured proof - processing in Isar. The main mechanisms are based on natural - deduction rule composition within the Pure framework. In - particular, there are no direct operations on goal states within the - proof body. Moreover, there is no hidden automated reasoning + This illustrates the basic idea of structured proof processing in Isar. The + main mechanisms are based on natural deduction rule composition within the + Pure framework. In particular, there are no direct operations on goal states + within the proof body. Moreover, there is no hidden automated reasoning involved, just plain unification. \<close> @@ -956,28 +908,26 @@ text \<open> The existing Isar infrastructure is sufficiently flexible to support - calculational reasoning (chains of transitivity steps) as derived - concept. The generic proof elements introduced below depend on - rules declared as @{attribute trans} in the context. It is left to - the object-logic to provide a suitable rule collection for mixed - relations of \<open>=\<close>, \<open><\<close>, \<open>\<le>\<close>, \<open>\<subset>\<close>, - \<open>\<subseteq>\<close> etc. Due to the flexibility of rule composition - (\secref{sec:framework-resolution}), substitution of equals by - equals is covered as well, even substitution of inequalities - involving monotonicity conditions; see also @{cite \<open>\S6\<close> "Wenzel-PhD"} - and @{cite "Bauer-Wenzel:2001"}. + calculational reasoning (chains of transitivity steps) as derived concept. + The generic proof elements introduced below depend on rules declared as + @{attribute trans} in the context. It is left to the object-logic to provide + a suitable rule collection for mixed relations of \<open>=\<close>, \<open><\<close>, \<open>\<le>\<close>, \<open>\<subset>\<close>, \<open>\<subseteq>\<close> + etc. Due to the flexibility of rule composition + (\secref{sec:framework-resolution}), substitution of equals by equals is + covered as well, even substitution of inequalities involving monotonicity + conditions; see also @{cite \<open>\S6\<close> "Wenzel-PhD"} and @{cite + "Bauer-Wenzel:2001"}. - The generic calculational mechanism is based on the observation that - rules such as \<open>trans:\<close>~@{prop "x = y \<Longrightarrow> y = z \<Longrightarrow> x = z"} - proceed from the premises towards the conclusion in a deterministic - fashion. Thus we may reason in forward mode, feeding intermediate - results into rules selected from the context. The course of - reasoning is organized by maintaining a secondary fact called - ``@{fact calculation}'', apart from the primary ``@{fact this}'' - already provided by the Isar primitives. In the definitions below, + The generic calculational mechanism is based on the observation that rules + such as \<open>trans:\<close>~@{prop "x = y \<Longrightarrow> y = z \<Longrightarrow> x = z"} proceed from the premises + towards the conclusion in a deterministic fashion. Thus we may reason in + forward mode, feeding intermediate results into rules selected from the + context. The course of reasoning is organized by maintaining a secondary + fact called ``@{fact calculation}'', apart from the primary ``@{fact this}'' + already provided by the Isar primitives. In the definitions below, @{attribute OF} refers to @{inference resolution} - (\secref{sec:framework-resolution}) with multiple rule arguments, - and \<open>trans\<close> represents to a suitable rule from the context: + (\secref{sec:framework-resolution}) with multiple rule arguments, and + \<open>trans\<close> represents to a suitable rule from the context: \begin{matharray}{rcl} @{command "also"}\<open>\<^sub>0\<close> & \equiv & @{command "note"}~\<open>calculation = this\<close> \\ @@ -985,15 +935,15 @@ @{command "finally"} & \equiv & @{command "also"}~@{command "from"}~\<open>calculation\<close> \\ \end{matharray} - The start of a calculation is determined implicitly in the - text: here @{command also} sets @{fact calculation} to the current - result; any subsequent occurrence will update @{fact calculation} by - combination with the next result and a transitivity rule. The - calculational sequence is concluded via @{command finally}, where - the final result is exposed for use in a concluding claim. + The start of a calculation is determined implicitly in the text: here + @{command also} sets @{fact calculation} to the current result; any + subsequent occurrence will update @{fact calculation} by combination with + the next result and a transitivity rule. The calculational sequence is + concluded via @{command finally}, where the final result is exposed for use + in a concluding claim. - Here is a canonical proof pattern, using @{command have} to - establish the intermediate results: + Here is a canonical proof pattern, using @{command have} to establish the + intermediate results: \<close> (*<*) @@ -1009,20 +959,18 @@ (*>*) text \<open> - The term ``\<open>\<dots>\<close>'' above is a special abbreviation - provided by the Isabelle/Isar syntax layer: it statically refers to - the right-hand side argument of the previous statement given in the - text. Thus it happens to coincide with relevant sub-expressions in - the calculational chain, but the exact correspondence is dependent - on the transitivity rules being involved. + The term ``\<open>\<dots>\<close>'' above is a special abbreviation provided by the + Isabelle/Isar syntax layer: it statically refers to the right-hand side + argument of the previous statement given in the text. Thus it happens to + coincide with relevant sub-expressions in the calculational chain, but the + exact correspondence is dependent on the transitivity rules being involved. \<^medskip> - Symmetry rules such as @{prop "x = y \<Longrightarrow> y = x"} are like - transitivities with only one premise. Isar maintains a separate - rule collection declared via the @{attribute sym} attribute, to be - used in fact expressions ``\<open>a [symmetric]\<close>'', or single-step - proofs ``@{command assume}~\<open>x = y\<close>~@{command then}~@{command - have}~\<open>y = x\<close>~@{command ".."}''. + Symmetry rules such as @{prop "x = y \<Longrightarrow> y = x"} are like transitivities with + only one premise. Isar maintains a separate rule collection declared via the + @{attribute sym} attribute, to be used in fact expressions ``\<open>a + [symmetric]\<close>'', or single-step proofs ``@{command assume}~\<open>x = y\<close>~@{command + then}~@{command have}~\<open>y = x\<close>~@{command ".."}''. \<close> end \ No newline at end of file