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

author | wenzelm |

Fri, 15 Oct 1999 16:44:37 +0200 | |

changeset 7874 | 180364256231 |

parent 7873 | 5d1200c7a671 |

child 7875 | 1baf422ec16a |

improved presentation;

--- a/src/HOL/Isar_examples/BasicLogic.thy Fri Oct 15 16:43:05 1999 +0200 +++ b/src/HOL/Isar_examples/BasicLogic.thy Fri Oct 15 16:44:37 1999 +0200 @@ -54,7 +54,7 @@ text {* Isar provides several ways to fine-tune the reasoning, avoiding - irrelevant detail. Several abbreviated language elements are + excessive detail. Several abbreviated language elements are available, enabling the writer to express proofs in a more concise way, even without referring to any automated proof tools yet. @@ -70,9 +70,9 @@ text {* In fact, concluding any (sub-)proof already involves solving any remaining goals by assumption\footnote{This is not a completely - trivial operation. As usual in Isabelle, proof by assumption - involves full higher-order unification.}. Thus we may skip the - rather vacuous body of the above proof as well. + trivial operation, as proof by assumption involves full higher-order + unification.}. Thus we may skip the rather vacuous body of the above + proof as well. *}; lemma "A --> A"; @@ -91,7 +91,7 @@ by rule; text {* - Proof by a single rule may be abbreviated as a double dot. + Proof by a single rule may be abbreviated as double-dot. *}; lemma "A --> A"; ..; @@ -103,7 +103,7 @@ *}; text {* - Let us also reconsider $K$. It's statement is composed of iterated + Let us also reconsider $K$. Its statement is composed of iterated connectives. Basic decomposition is by a single rule at a time, which is why our first version above was by nesting two proofs. @@ -135,10 +135,10 @@ \isacommand{proof}~($\idt{intro}$~\name{impI}~\name{allI}) to strip implications and universal quantifiers. - Such well-tuned iterated decomposition of certain structure is the - prime application of $\idt{intro}$ and $\idt{elim}$. In general, - terminal steps that solve a goal completely are typically performed - by actual automated proof methods (such as + Such well-tuned iterated decomposition of certain structures is the + prime application of $\idt{intro}$ and $\idt{elim}$. In contrast, + terminal steps that solve a goal completely are usually performed by + actual automated proof methods (such as \isacommand{by}~$\idt{blast}$). *}; @@ -206,8 +206,9 @@ qed; text {* - Subsequently, only the outermost decomposition step is left backward, - all the rest is forward. + In the subsequent version we flatten the structure of the main body + by doing forward reasoning all the time. Only the outermost + decomposition step is left as backward. *}; lemma "A & B --> B & A"; @@ -247,9 +248,9 @@ decomposition, and bottom-up forward composition. In practice, there is no single best way to arrange some pieces of formal reasoning, of course. Depending on the actual applications, the intended audience - etc., certain aspects such as rules~/ methods vs.\ facts have to be - emphasized in an appropriate way. This requires the proof writer to - develop good taste, and some practice, of course. + etc., rules (and methods) on the one hand vs.\ facts on the other + hand have to be emphasized in an appropriate way. This requires the + proof writer to develop good taste, and some practice, of course. *}; text {* @@ -321,8 +322,8 @@ case. \medskip In our example the situation is even simpler, since the two - ``cases'' actually coincide. Consequently the proof may be rephrased - as follows. + cases actually coincide. Consequently the proof may be rephrased as + follows. *}; lemma "P | P --> P";

--- a/src/HOL/Isar_examples/Cantor.thy Fri Oct 15 16:43:05 1999 +0200 +++ b/src/HOL/Isar_examples/Cantor.thy Fri Oct 15 16:44:37 1999 +0200 @@ -14,16 +14,17 @@ elements. It has become a favorite basic example in pure higher-order logic since it is so easily expressed: \[\all{f::\alpha \To \alpha \To \idt{bool}} \ex{S::\alpha \To \idt{bool}} - \all{x::\alpha}. f \ap x \not= S\] + \all{x::\alpha} f \ap x \not= S\] Viewing types as sets, $\alpha \To \idt{bool}$ represents the powerset of $\alpha$. This version of the theorem states that for every function from $\alpha$ to its powerset, some subset is outside its range. The Isabelle/Isar proofs below uses HOL's set theory, - with the type $\alpha \ap \idt{set}$ and the operator $\idt{range}$. + with the type $\alpha \ap \idt{set}$ and the operator + $\idt{range}::(\alpha \To \beta) \To \beta \ap \idt{set}$. \bigskip We first consider a slightly awkward version of the proof, - with the reasoning expressed quite naively. + with the innermost reasoning expressed quite naively. *}; theorem "EX S. S ~: range(f :: 'a => 'a set)"; @@ -58,11 +59,11 @@ change the order of assumptions introduced in the two cases of rule \name{equalityCE}, streamlining the flow of intermediate facts and avoiding explicit naming.\footnote{In general, neither the order of - assumptions as introduced \isacommand{assume}, nor the order of goals - as solved by \isacommand{show} matters. The basic logical structure - has to be left intact, though. In particular, assumptions - ``belonging'' to some goal have to be introduced \emph{before} its - corresponding \isacommand{show}.} + assumptions as introduced by \isacommand{assume}, nor the order of + goals as solved by \isacommand{show} is of any significance. The + basic logical structure has to be left intact, though. In + particular, assumptions ``belonging'' to some goal have to be + introduced \emph{before} its corresponding \isacommand{show}.} *}; theorem "EX S. S ~: range(f :: 'a => 'a set)"; @@ -91,10 +92,10 @@ text {* How much creativity is required? As it happens, Isabelle can prove - this theorem automatically. The default context of the classical - proof tools contains rules for most of the constructs of HOL's set - theory. We must augment it with \name{equalityCE} to break up set - equalities, and then apply best-first search. Depth-first search + this theorem automatically. The default context of the Isabelle's + classical prover contains rules for most of the constructs of HOL's + set theory. We must augment it with \name{equalityCE} to break up + set equalities, and then apply best-first search. Depth-first search would diverge, but best-first search successfully navigates through the large search space. *}; @@ -106,8 +107,8 @@ While this establishes the same theorem internally, we do not get any idea of how the proof actually works. There is currently no way to transform internal system-level representations of Isabelle proofs - back into Isar documents. Writing proof documents really is a - creative process, after all. + back into Isar documents. Writing intelligible proof documents + really is a creative process, after all. *}; end;

--- a/src/HOL/Isar_examples/ExprCompiler.thy Fri Oct 15 16:43:05 1999 +0200 +++ b/src/HOL/Isar_examples/ExprCompiler.thy Fri Oct 15 16:44:37 1999 +0200 @@ -10,9 +10,9 @@ theory ExprCompiler = Main:; text {* - This is a (quite trivial) example of program verification. We model - a compiler translating expressions to stack machine instructions, and - prove its correctness wrt.\ evaluation semantics. + This is a (rather trivial) example of program verification. We model + a compiler for translating expressions to stack machine instructions, + and prove its correctness wrt.\ some evaluation semantics. *}; @@ -21,7 +21,7 @@ text {* Binary operations are just functions over some type of values. This is both for syntax and semantics, i.e.\ we use a ``shallow - embedding''. + embedding'' here. *}; types @@ -42,8 +42,8 @@ Binop "'val binop" "('adr, 'val) expr" "('adr, 'val) expr"; text {* - Evaluation (wrt.\ an environment) is defined by primitive recursion - over the structure of expressions. + Evaluation (wrt.\ some environment of variable assignments) is + defined by primitive recursion over the structure of expressions. *}; consts

--- a/src/HOL/Isar_examples/Group.thy Fri Oct 15 16:43:05 1999 +0200 +++ b/src/HOL/Isar_examples/Group.thy Fri Oct 15 16:44:37 1999 +0200 @@ -7,12 +7,13 @@ theory Group = Main:; -subsection {* Groups *}; +subsection {* Groups and calculational reasoning *}; text {* - We define an axiomatic type class of general groups over signature - $({\times} :: \alpha \To \alpha \To \alpha, \idt{one} :: \alpha, - \idt{inv} :: \alpha \To \alpha)$. + We define an axiomatic type class of groups over signature $({\times} + :: \alpha \To \alpha \To \alpha, \idt{one} :: \alpha, \idt{inv} :: + \alpha \To \alpha)$. Note that the parent class $\idt{times}$ is + provided by the basic HOL theory. *}; consts @@ -27,9 +28,7 @@ text {* The group axioms only state the properties of left unit and inverse, - the right versions are derivable as follows. The calculational proof - style below closely follows typical presentations given in any basic - course on algebra. + the right versions may be derived as follows. *}; theorem group_right_inverse: "x * inv x = (one::'a::group)"; @@ -55,7 +54,7 @@ text {* With \name{group-right-inverse} already at our disposal, - \name{group-right-unit} is now obtained much easier as follows. + \name{group-right-unit} is now obtained much easier. *}; theorem group_right_unit: "x * one = (x::'a::group)"; @@ -72,18 +71,27 @@ qed; text {* - \bigskip There are only two Isar language elements for calculational - proofs: \isakeyword{also} for initial or intermediate calculational - steps, and \isakeyword{finally} for building the result of a - calculation. These constructs are not hardwired into Isabelle/Isar, - but defined on top of the basic Isar/VM interpreter. Expanding the - \isakeyword{also} and \isakeyword{finally} derived language elements, - calculations may be simulated as demonstrated below. + \medskip The calculational proof style above follows typical + presentations given in any introductory course on algebra. The basic + technique is to form a transitive chain of equations, which in turn + are established by simplifying with appropriate rules. The low-level + logical parts of equational reasoning are left implicit. - Note that ``$\dots$'' is just a special term binding that happens to - be bound automatically to the argument of the last fact established - by assume or any local goal. In contrast to $\var{thesis}$, the - ``$\dots$'' variable is bound \emph{after} the proof is finished. + Note that ``$\dots$'' is just a special term variable that happens to + be bound automatically to the argument\footnote{The argument of a + curried infix expression happens to be its right-hand side.} of the + last fact achieved by any local assumption or proven statement. In + contrast to $\var{thesis}$, the ``$\dots$'' variable is bound + \emph{after} the proof is finished. + + There are only two separate Isar language elements for calculational + proofs: ``\isakeyword{also}'' for initial or intermediate + calculational steps, and ``\isakeyword{finally}'' for exhibiting the + result of a calculation. These constructs are not hardwired into + Isabelle/Isar, but defined on top of the basic Isar/VM interpreter. + Expanding the \isakeyword{also} and \isakeyword{finally} derived + language elements, calculations may be simulated as demonstrated + below. *}; theorem "x * one = (x::'a::group)"; @@ -112,16 +120,26 @@ note calculation = trans [OF calculation this] -- {* final calculational step: compose with transitivity rule ... *}; from calculation - -- {* ... and pick up final result *}; + -- {* ... and pick up the final result *}; show ?thesis; .; qed; +text {* + Note that this scheme of calculations is not restricted to plain + transitivity. Rules like anti-symmetry, or even forward and backward + substitution work as well. For the actual \isacommand{also} and + \isacommand{finally} commands, Isabelle/Isar maintains separate + context information of ``transitivity'' rules. Rule selection takes + place automatically by higher-order unification. +*}; + subsection {* Groups as monoids *}; text {* - Monoids are usually defined like this. + Monoids over signature $({\times} :: \alpha \To \alpha \To \alpha, + \idt{one} :: \alpha)$ are defined like this. *}; axclass monoid < times @@ -144,4 +162,13 @@ rule group_left_unit, rule group_right_unit); +text {* + The \isacommand{instance} command actually is a version of + \isacommand{theorem}, setting up a goal that reflects the intended + class relation (or type constructor arity). Thus any Isar proof + language element may be involved to establish this statement. When + concluding the proof, the result is transformed into the original + type signature extension behind the scenes. +*}; + end;

--- a/src/HOL/Isar_examples/KnasterTarski.thy Fri Oct 15 16:43:05 1999 +0200 +++ b/src/HOL/Isar_examples/KnasterTarski.thy Fri Oct 15 16:44:37 1999 +0200 @@ -13,10 +13,9 @@ subsection {* Prose version *}; text {* - According to the book ``Introduction to Lattices and Order'' - \cite[pages 93--94]{davey-priestley}, the Knaster-Tarski fixpoint - theorem is as follows.\footnote{We have dualized the argument, and - tuned the notation a little bit.} + According to the textbook \cite[pages 93--94]{davey-priestley}, the + Knaster-Tarski fixpoint theorem is as follows.\footnote{We have + dualized the argument, and tuned the notation a little bit.} \medskip \textbf{The Knaster-Tarski Fixpoint Theorem.} Let $L$ be a complete lattice and $f \colon L \to L$ an order-preserving map. @@ -51,10 +50,10 @@ proof -; {{; fix x; - assume mem: "x : ?H"; + assume H: "x : ?H"; hence "?a <= x"; by (rule Inter_lower); with mono; have "f ?a <= f x"; ..; - also; from mem; have "... <= x"; ..; + also; from H; have "... <= x"; ..; finally; have "f ?a <= x"; .; }}; hence ge: "f ?a <= ?a"; by (rule Inter_greatest); @@ -77,7 +76,7 @@ changed to achieve structured top-down decomposition of the problem at the outer level, while the small inner steps of reasoning or done in a forward manner. Note that this requires only the most basic - features of the Isar language. + features of the Isar language, we are certainly more at ease here. *}; theorem KnasterTarski': "mono f ==> EX a::'a set. f a = a"; @@ -91,10 +90,10 @@ show ge: "f ?a <= ?a"; proof (rule Inter_greatest); fix x; - assume mem: "x : ?H"; + assume H: "x : ?H"; hence "?a <= x"; by (rule Inter_lower); with mono; have "f ?a <= f x"; ..; - also; from mem; have "... <= x"; ..; + also; from H; have "... <= x"; ..; finally; show "f ?a <= x"; .; qed; show "?a <= f ?a";

--- a/src/HOL/Isar_examples/MultisetOrder.thy Fri Oct 15 16:43:05 1999 +0200 +++ b/src/HOL/Isar_examples/MultisetOrder.thy Fri Oct 15 16:44:37 1999 +0200 @@ -29,7 +29,8 @@ M0 + {#a#} = M0' + {#a'#} & N = M0' + K & ?r K a'"; by simp; thus "?case1 | ?case2"; proof (elim exE conjE); - fix a' M0' K; assume N: "N = M0' + K" and r: "?r K a'"; + fix a' M0' K; + assume N: "N = M0' + K" and r: "?r K a'"; assume "M0 + {#a#} = M0' + {#a'#}"; hence "M0 = M0' & a = a' | (EX K'. M0 = K' + {#a'#} & M0' = K' + {#a#})"; @@ -66,7 +67,8 @@ and acc_hyp: "ALL M. (M, M0) : ?R --> M + {#a#} : ?W"; have "M0 + {#a#} : ?W"; proof (rule accI [of "M0 + {#a#}"]); - fix N; assume "(N, M0 + {#a#}) : ?R"; + fix N; + assume "(N, M0 + {#a#}) : ?R"; hence "((EX M. (M, M0) : ?R & N = M + {#a#}) | (EX K. (ALL b. elem K b --> (b, a) : r) & N = M0 + K))"; by (rule less_add);

--- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy Fri Oct 15 16:43:05 1999 +0200 +++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy Fri Oct 15 16:44:37 1999 +0200 @@ -54,7 +54,7 @@ qed; -subsection {* Basic properties of below *}; +subsection {* Basic properties of ``below'' *}; constdefs below :: "nat => nat set" @@ -77,7 +77,7 @@ lemmas Sigma_Suc = Sigma_Suc1 Sigma_Suc2; -subsection {* Basic properties of evnodd *}; +subsection {* Basic properties of ``evnodd'' *}; constdefs evnodd :: "(nat * nat) set => nat => (nat * nat) set" @@ -223,7 +223,7 @@ thus "?thesis b"; proof (elim exE); have "?e (a Un t) b = ?e a b Un ?e t b"; by (rule evnodd_Un); - also; fix i j; assume e: "?e a b = {(i, j)}"; + also; fix i j; assume "?e a b = {(i, j)}"; also; have "... Un ?e t b = insert (i, j) (?e t b)"; by simp; also; have "card ... = Suc (card (?e t b))"; proof (rule card_insert_disjoint); @@ -292,7 +292,7 @@ also; have "?e ?t 1 = ?e ?t'' 1"; by simp; also; from t''; have "card ... = card (?e ?t'' 0)"; by (rule tiling_domino_01 [RS sym]); - finally; show False; ..; + finally; have "... < ..."; .; thus False; ..; qed; qed;

--- a/src/HOL/Isar_examples/Peirce.thy Fri Oct 15 16:43:05 1999 +0200 +++ b/src/HOL/Isar_examples/Peirce.thy Fri Oct 15 16:44:37 1999 +0200 @@ -13,11 +13,10 @@ certainly involve some form of classical contradiction. The first proof is again a well-balanced combination of plain - backward and forward reasoning. The actual classical reasoning step - is where the negated goal is introduced as additional assumption. - This eventually leads to a contradiction.\footnote{The rule involved - here is negation elimination; it holds in intuitionistic logic as - well.} + backward and forward reasoning. The actual classical step is where + the negated goal may be introduced as additional assumption. This + eventually leads to a contradiction.\footnote{The rule involved there + is negation elimination; it holds in intuitionistic logic as well.} *}; theorem "((A --> B) --> A) --> A"; @@ -36,12 +35,13 @@ qed; text {* - The subsequent version rearranges the reasoning by means of ``weak - assumptions'' (as introduced by \isacommand{presume}). Before + In the subsequent version the reasoning is rearranged by means of + ``weak assumptions'' (as introduced by \isacommand{presume}). Before assuming the negated goal $\neg A$, its intended consequence $A \impl B$ is put into place in order to solve the main problem. Nevertheless, we do not get anything for free, but have to establish - $A \impl B$ later on. The overall effect is that of a \emph{cut}. + $A \impl B$ later on. The overall effect is that of a logical + \emph{cut}. Technically speaking, whenever some goal is solved by \isacommand{show} in the context of weak assumptions then the latter @@ -58,11 +58,11 @@ presume "A --> B"; with aba; show A; ..; next; - assume not_a: "~ A"; + assume "~ A"; show "A --> B"; proof; assume A; - with not_a; show B; ..; + thus B; by contradiction; qed; qed; qed; @@ -70,9 +70,9 @@ text {* Note that the goals stemming from weak assumptions may be even left until qed time, where they get eventually solved ``by assumption'' as - well. In that case there is really no big difference between the two - kinds of assumptions, apart from the order of reducing the individual - parts of the proof configuration. + well. In that case there is really no fundamental difference between + the two kinds of assumptions, apart from the order of reducing the + individual parts of the proof configuration. Nevertheless, the ``strong'' mode of plain assumptions is quite important in practice to achieve robustness of proof document

--- a/src/HOL/Isar_examples/document/root.tex Fri Oct 15 16:43:05 1999 +0200 +++ b/src/HOL/Isar_examples/document/root.tex Fri Oct 15 16:44:37 1999 +0200 @@ -10,10 +10,10 @@ \maketitle \begin{abstract} - Isar offers a high-level proof (and theory) language interface to Isabelle. - We give various examples of Isabelle/Isar proof developments, ranging from - simple demonstrations of certain language features to more advanced - applications. + Isar offers a high-level proof (and theory) language for Isabelle. + We give various examples of Isabelle/Isar proof developments, + ranging from simple demonstrations of certain language features to + more advanced applications. \end{abstract} \tableofcontents

--- a/src/HOL/Isar_examples/document/style.tex Fri Oct 15 16:43:05 1999 +0200 +++ b/src/HOL/Isar_examples/document/style.tex Fri Oct 15 16:44:37 1999 +0200 @@ -9,7 +9,7 @@ \newcommand{\name}[1]{\textsl{#1}} \newcommand{\idt}[1]{{\mathord{\mathit{#1}}}} -\newcommand{\var}[1]{{?\!#1}} +\newcommand{\var}[1]{{?\!\idt{#1}}} \DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D} \newcommand{\dsh}{\dshsym}