# HG changeset patch # User wenzelm # Date 1444680204 -7200 # Node ID e0825405d398d3e115bc0959eec75373b313500c # Parent ee42cba50933cabe49c69e154c50460003824f49 more symbols; diff -r ee42cba50933 -r e0825405d398 src/Doc/Isar_Ref/Document_Preparation.thy --- a/src/Doc/Isar_Ref/Document_Preparation.thy Mon Oct 12 21:42:14 2015 +0200 +++ b/src/Doc/Isar_Ref/Document_Preparation.thy Mon Oct 12 22:03:24 2015 +0200 @@ -75,7 +75,8 @@ antiquotations}, see also \secref{sec:antiq}. These are interpreted in the present theory or proof context. - \medskip The proof markup commands closely resemble those for theory + \<^medskip> + The proof markup commands closely resemble those for theory specifications, but have a different formal status and produce different {\LaTeX} macros. \ @@ -426,14 +427,15 @@ Some tags are pre-declared for certain classes of commands, serving as default markup if no tags are given in the text: - \medskip + \<^medskip> \begin{tabular}{ll} @{text "theory"} & theory begin/end \\ @{text "proof"} & all proof commands \\ @{text "ML"} & all commands involving ML code \\ \end{tabular} + \<^medskip> - \medskip The Isabelle document preparation system + The Isabelle document preparation system @{cite "isabelle-system"} allows tagged command regions to be presented specifically, e.g.\ to fold proof texts, or drop parts of the text completely. @@ -451,7 +453,8 @@ sub-proof to be typeset as @{text visible} (unless some of its parts are tagged differently). - \medskip Command tags merely produce certain markup environments for + \<^medskip> + Command tags merely produce certain markup environments for type-setting. The meaning of these is determined by {\LaTeX} macros, as defined in @{file "~~/lib/texinputs/isabelle.sty"} or by the document author. The Isabelle document preparation tools @@ -513,62 +516,62 @@ \begin{itemize} - \item Empty @{verbatim "()"} + \<^item> Empty @{verbatim "()"} @{rail \()\} - \item Nonterminal @{verbatim "A"} + \<^item> Nonterminal @{verbatim "A"} @{rail \A\} - \item Nonterminal via Isabelle antiquotation + \<^item> Nonterminal via Isabelle antiquotation @{verbatim "@{syntax method}"} @{rail \@{syntax method}\} - \item Terminal @{verbatim "'xyz'"} + \<^item> Terminal @{verbatim "'xyz'"} @{rail \'xyz'\} - \item Terminal in keyword style @{verbatim "@'xyz'"} + \<^item> Terminal in keyword style @{verbatim "@'xyz'"} @{rail \@'xyz'\} - \item Terminal via Isabelle antiquotation + \<^item> Terminal via Isabelle antiquotation @{verbatim "@@{method rule}"} @{rail \@@{method rule}\} - \item Concatenation @{verbatim "A B C"} + \<^item> Concatenation @{verbatim "A B C"} @{rail \A B C\} - \item Newline inside concatenation + \<^item> Newline inside concatenation @{verbatim "A B C \ D E F"} @{rail \A B C \ D E F\} - \item Variants @{verbatim "A | B | C"} + \<^item> Variants @{verbatim "A | B | C"} @{rail \A | B | C\} - \item Option @{verbatim "A ?"} + \<^item> Option @{verbatim "A ?"} @{rail \A ?\} - \item Repetition @{verbatim "A *"} + \<^item> Repetition @{verbatim "A *"} @{rail \A *\} - \item Repetition with separator @{verbatim "A * sep"} + \<^item> Repetition with separator @{verbatim "A * sep"} @{rail \A * sep\} - \item Strict repetition @{verbatim "A +"} + \<^item> Strict repetition @{verbatim "A +"} @{rail \A +\} - \item Strict repetition with separator @{verbatim "A + sep"} + \<^item> Strict repetition with separator @{verbatim "A + sep"} @{rail \A + sep\} diff -r ee42cba50933 -r e0825405d398 src/Doc/Isar_Ref/First_Order_Logic.thy --- a/src/Doc/Isar_Ref/First_Order_Logic.thy Mon Oct 12 21:42:14 2015 +0200 +++ b/src/Doc/Isar_Ref/First_Order_Logic.thy Mon Oct 12 22:03:24 2015 +0200 @@ -231,7 +231,8 @@ ``@{text "\ A \ B \ A \ B"}'' coincides with the original axiomatization of @{thm disjE}. - \medskip We continue propositional logic by introducing absurdity + \<^medskip> + We continue propositional logic by introducing absurdity with its characteristic elimination. Plain truth may then be defined as a proposition that is trivially true. \ @@ -248,8 +249,8 @@ unfolding true_def .. text \ - \medskip Now negation represents an implication towards - absurdity: + \<^medskip> + Now negation represents an implication towards absurdity: \ definition @@ -374,7 +375,7 @@ can now be summarized as follows, using the native Isar statement format of \secref{sec:framework-stmt}. - \medskip + \<^medskip> \begin{tabular}{l} @{text "impI: \ A \ B \ A \ B"} \\ @{text "impD: \ A \ B \ A \ B"} \\[1ex] @@ -398,7 +399,7 @@ @{text "exI: \ B a \ \x. B x"} \\ @{text "exE: \ \x. B x \ a \ B a"} \end{tabular} - \medskip + \<^medskip> This essentially provides a declarative reading of Pure rules as Isar reasoning patterns: the rule statements tells how a @@ -511,7 +512,8 @@ (*>*) text \ - \bigskip Of course, these proofs are merely examples. As + \<^bigskip> + Of course, these proofs are merely examples. As sketched in \secref{sec:framework-subproof}, there is a fair amount of flexibility in expressing Pure deductions in Isar. Here the user is asked to express himself adequately, aiming at proof texts of diff -r ee42cba50933 -r e0825405d398 src/Doc/Isar_Ref/Framework.thy --- a/src/Doc/Isar_Ref/Framework.thy Mon Oct 12 21:42:14 2015 +0200 +++ b/src/Doc/Isar_Ref/Framework.thy Mon Oct 12 22:03:24 2015 +0200 @@ -52,7 +52,8 @@ @{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 + \<^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 @@ -69,7 +70,8 @@ examples shall refer to set-theory, to minimize the danger of understanding connectives of predicate logic as something special. - \medskip The following deduction performs @{text "\"}-introduction, + \<^medskip> + The following deduction performs @{text "\"}-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 @@ -97,7 +99,8 @@ text_raw \\end{minipage}\ text \ - \medskip Note that @{command assume} augments the proof + \<^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 @@ -152,7 +155,8 @@ text_raw \\end{minipage}\ text \ - \medskip This Isar reasoning pattern again refers to the + \<^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}~@{text "(rule InterI)"}''. Note @@ -166,7 +170,8 @@ refinement of the enclosing claim, using the rule derived from the proof body. - \medskip The next example involves @{term "\\"}, which can be + \<^medskip> + The next example involves @{term "\\"}, which can be characterized as the set of all @{term "x"} such that @{prop "\A. x \ A \ A \ \"}. The elimination rule for @{prop "x \ \\"} does not mention @{text "\"} and @{text "\"} at all, but admits to obtain @@ -201,7 +206,8 @@ text_raw \\end{minipage}\ text \ - \medskip Although the Isar proof follows the natural + \<^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 @@ -236,13 +242,13 @@ parlance, there are three levels of @{text "\"}-calculus with corresponding arrows @{text "\"}/@{text "\"}/@{text "\"}: - \medskip + \<^medskip> \begin{tabular}{ll} @{text "\ \ \"} & syntactic function space (terms depending on terms) \\ @{text "\x. B(x)"} & universal quantification (proofs depending on terms) \\ @{text "A \ B"} & implication (proofs depending on proofs) \\ \end{tabular} - \medskip + \<^medskip> Here only the types of syntactic terms, and the propositions of proof terms have been shown. The @{text @@ -298,7 +304,8 @@ prop"} with axioms for reflexivity, substitution, extensionality, and @{text "\\\"}-conversion on @{text "\"}-terms. - \medskip An object-logic introduces another layer on top of Pure, + \<^medskip> + An object-logic introduces another layer on top of Pure, e.g.\ with types @{text "i"} for individuals and @{text "o"} for propositions, term constants @{text "Trueprop :: o \ prop"} as (implicit) derivability judgment and connectives like @{text "\ :: o @@ -348,7 +355,8 @@ @{text "InterI:"}~@{prop "(\A. A \ \ \ x \ A) \ x \ \\"} \] - \medskip Goals are also represented as rules: @{text "A\<^sub>1 \ + \<^medskip> + Goals are also represented as rules: @{text "A\<^sub>1 \ \ A\<^sub>n \ C"} states that the sub-goals @{text "A\<^sub>1, \, A\<^sub>n"} entail the result @{text "C"}; for @{text "n = 0"} the goal is finished. To allow @{text "C"} being a rule statement @@ -384,7 +392,7 @@ \end{tabular}} \] - \medskip + \<^medskip> \[ \infer[(@{inference_def assumption})]{@{text "C\"}} @@ -399,7 +407,7 @@ Isabelle/Pure: {\footnotesize - \medskip + \<^medskip> \begin{tabular}{r@ {\quad}l} @{text "(A \ B \ B \ A) \ #(A \ B \ B \ A)"} & @{text "(init)"} \\ @{text "(A \ B \ B) \ (A \ B \ A) \ #\"} & @{text "(resolution B \ A \ B \ A)"} \\ @@ -409,7 +417,7 @@ @{text "#\"} & @{text "(assumption)"} \\ @{text "A \ B \ B \ A"} & @{text "(finish)"} \\ \end{tabular} - \medskip + \<^medskip> } Compositions of @{inference assumption} after @{inference @@ -464,7 +472,7 @@ \secref{sec:framework-stmt} for the separate category @{text "statement"}. - \medskip + \<^medskip> \begin{tabular}{rcl} @{text "theory\stmt"} & = & @{command "theorem"}~@{text "statement proof |"}~~@{command "definition"}~@{text "\ | \"} \\[1ex] @@ -484,15 +492,18 @@ & @{text "|"} & @{command "show"}~@{text "name: props proof"} \\ \end{tabular} - \medskip Simultaneous propositions or facts may be separated by the + \<^medskip> + Simultaneous propositions or facts may be separated by the @{keyword "and"} keyword. - \medskip The syntax for terms and propositions is inherited from + \<^medskip> + The syntax for terms and propositions is inherited from Pure (and the object-logic). A @{text "pattern"} is a @{text "term"} with schematic variables, to be bound by higher-order matching. - \medskip Facts may be referenced by name or proposition. For + \<^medskip> + Facts may be referenced by name or proposition. For example, the result of ``@{command have}~@{text "a: A \proof\"}'' becomes available both as @{text "a"} and \isacharbackquoteopen@{text "A"}\isacharbackquoteclose. Moreover, @@ -509,12 +520,12 @@ frequently together with @{command then} we provide some abbreviations: - \medskip + \<^medskip> \begin{tabular}{rcl} @{command from}~@{text a} & @{text "\"} & @{command note}~@{text a}~@{command then} \\ @{command with}~@{text a} & @{text "\"} & @{command from}~@{text "a \ this"} \\ \end{tabular} - \medskip + \<^medskip> The @{text "method"} category is essentially a parameter and may be populated later. Methods use the facts indicated by @{command @@ -541,7 +552,8 @@ "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 + \<^medskip> + Block structure can be indicated explicitly by ``@{command "{"}~@{text "\"}~@{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 @@ -580,12 +592,12 @@ @{inference discharge} as given below. The additional variants @{command presume} and @{command def} are defined as follows: - \medskip + \<^medskip> \begin{tabular}{rcl} @{command presume}~@{text A} & @{text "\"} & @{command assume}~@{text "\weak\discharge\ A"} \\ @{command def}~@{text "x \ a"} & @{text "\"} & @{command fix}~@{text x}~@{command assume}~@{text "\expansion\ x \ a"} \\ \end{tabular} - \medskip + \<^medskip> \[ \infer[(@{inference_def discharge})]{@{text "\\ - A \ #A \ B"}}{@{text "\\ \ B"}} @@ -597,7 +609,8 @@ \infer[(@{inference_def expansion})]{@{text "\\ - (x \ a) \ B a"}}{@{text "\\ \ B x"}} \] - \medskip Note that @{inference discharge} and @{inference + \<^medskip> + Note that @{inference discharge} and @{inference "weak\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, @@ -611,7 +624,7 @@ with a proof of a case rule stating that this extension is conservative (i.e.\ may be removed from closed results later on): - \medskip + \<^medskip> \begin{tabular}{l} @{text "\facts\"}~~@{command obtain}~@{text "\<^vec>x \ \<^vec>A \<^vec>x \proof\ \"} \\[0.5ex] \quad @{command have}~@{text "case: \thesis. (\\<^vec>x. \<^vec>A \<^vec>x \ thesis) \ thesis\"} \\ @@ -622,7 +635,7 @@ \quad @{command qed} \\ \quad @{command fix}~@{text "\<^vec>x"}~@{command assume}~@{text "\elimination case\ \<^vec>A \<^vec>x"} \\ \end{tabular} - \medskip + \<^medskip> \[ \infer[(@{inference elimination})]{@{text "\ \ B"}}{ @@ -644,7 +657,8 @@ is similar to ``@{command have}~@{text "A \ B"}'', but the latter involves multiple sub-goals. - \medskip The subsequent Isar proof texts explain all context + \<^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}. @@ -684,17 +698,19 @@ (*>*) text \ - \bigskip This illustrates the meaning of Isar context + \<^bigskip> + This illustrates the meaning of Isar context elements without goals getting in between. \ + subsection \Structured statements \label{sec:framework-stmt}\ text \ The category @{text "statement"} of top-level theorem specifications is defined as follows: - \medskip + \<^medskip> \begin{tabular}{rcl} @{text "statement"} & @{text "\"} & @{text "name: props \ \"} \\ & @{text "|"} & @{text "context\<^sup>* conclusion"} \\[0.5ex] @@ -707,7 +723,8 @@ & & \quad @{text "\ \"} \\ \end{tabular} - \medskip A simple @{text "statement"} consists of named + \<^medskip> + A simple @{text "statement"} consists of named propositions. The full form admits local context elements followed by the actual conclusions, such as ``@{keyword "fixes"}~@{text x}~@{keyword "assumes"}~@{text "A x"}~@{keyword "shows"}~@{text "B @@ -721,14 +738,14 @@ parameters (@{text "vars"}) and several premises (@{text "props"}). This specifies multi-branch elimination rules. - \medskip + \<^medskip> \begin{tabular}{l} @{text "\ \<^vec>x \ \<^vec>A \<^vec>x \ \ \"} \\[0.5ex] \quad @{text "\ thesis"} \\ \quad @{text "\ [intro]: \\<^vec>x. \<^vec>A \<^vec>x \ thesis \ \"} \\ \quad @{text "\ thesis"} \\ \end{tabular} - \medskip + \<^medskip> Presenting structured statements in such an ``open'' format usually simplifies the subsequent proof, because the outer structure of the @@ -761,7 +778,8 @@ text_raw \\end{minipage}\ text \ - \medskip Here local facts \isacharbackquoteopen@{text "A + \<^medskip> + Here local facts \isacharbackquoteopen@{text "A x"}\isacharbackquoteclose\ and \isacharbackquoteopen@{text "B y"}\isacharbackquoteclose\ are referenced immediately; there is no need to decompose the logical rule structure again. In the second @@ -789,7 +807,8 @@ 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 + \<^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 @@ -927,12 +946,14 @@ text_raw \\end{minipage}\ text \ - \medskip Such ``peephole optimizations'' of Isar texts are + \<^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. - \medskip This illustrates the basic idea of structured proof + \<^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 @@ -1005,7 +1026,8 @@ the calculational chain, but the exact correspondence is dependent on the transitivity rules being involved. - \medskip Symmetry rules such as @{prop "x = y \ y = x"} are like + \<^medskip> + Symmetry rules such as @{prop "x = y \ 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 ``@{text "a [symmetric]"}'', or single-step diff -r ee42cba50933 -r e0825405d398 src/Doc/Isar_Ref/Generic.thy --- a/src/Doc/Isar_Ref/Generic.thy Mon Oct 12 21:42:14 2015 +0200 +++ b/src/Doc/Isar_Ref/Generic.thy Mon Oct 12 22:03:24 2015 +0200 @@ -293,7 +293,7 @@ @{method_def simp_all} & : & @{text method} \\ @{attribute_def simp_depth_limit} & : & @{text attribute} & default @{text 100} \\ \end{tabular} - \medskip + \<^medskip> @{rail \ (@@{method simp} | @@{method simp_all}) opt? (@{syntax simpmod} * ) @@ -321,7 +321,8 @@ either case, which might be required precisely like that in some boundary situations to perform the intended simplification step! - \medskip The @{text only} modifier first removes all other rewrite + \<^medskip> + The @{text only} modifier first removes all other rewrite rules, looper tactics (including split rules), congruence rules, and then behaves like @{text add}. Implicit solvers remain, which means that trivial rules like reflexivity or introduction of @{text @@ -330,7 +331,8 @@ lead to some surprise of the meaning of ``only'' in Isabelle/HOL compared to English! - \medskip The @{text split} modifiers add or delete rules for the + \<^medskip> + The @{text split} modifiers add or delete rules for the Splitter (see also \secref{sec:simp-strategies} on the looper). This works only if the Simplifier method has been properly setup to include the Splitter (all major object logics such HOL, HOLCF, FOL, @@ -341,7 +343,8 @@ @{text "(split thms)"} can be imitated by ``@{text "(simp only: split: thms)"}''. - \medskip The @{text cong} modifiers add or delete Simplifier + \<^medskip> + The @{text cong} modifiers add or delete Simplifier congruence rules (see also \secref{sec:simp-rules}); the default is to add. @@ -421,7 +424,8 @@ lemma fixes x :: "'a :: monoid_add" shows "0 + (x + 0) = x + 0 + 0" by simp text \ - \medskip In many cases, assumptions of a subgoal are also needed in + \<^medskip> + In many cases, assumptions of a subgoal are also needed in the simplification process. For example: \ @@ -467,7 +471,9 @@ have "f 0 = f 0 + 0" by simp end -text \\medskip Because assumptions may simplify each other, there +text \ + \<^medskip> + Because assumptions may simplify each other, there can be very subtle cases of nontermination. For example, the regular @{method simp} method applied to @{prop "P (f x) \ y = x \ f x = f y \ Q"} gives rise to the infinite reduction sequence @@ -518,11 +524,12 @@ @{text "?P \ ?P \ ?P"} \\ @{text "?A \ ?B \ {x. x \ ?A \ x \ ?B}"} - \smallskip + \<^medskip> Conditional rewrites such as @{text "?m < ?n \ ?m div ?n = 0"} are also permitted; the conditions can be arbitrary formulas. - \medskip Internally, all rewrite rules are translated into Pure + \<^medskip> + Internally, all rewrite rules are translated into Pure equalities, theorems with conclusion @{text "lhs \ rhs"}. The simpset contains a function for extracting equalities from arbitrary theorems, which is usually installed when the object-logic is @@ -536,7 +543,7 @@ \begin{enumerate} - \item First-order patterns, considering the sublanguage of + \<^enum> First-order patterns, considering the sublanguage of application of constant operators to variable operands, without @{text "\"}-abstractions or functional variables. For example: @@ -544,7 +551,7 @@ @{text "(?x + ?y) + ?z \ ?x + (?y + ?z)"} \\ @{text "f (f ?x ?y) ?z \ f ?x (f ?y ?z)"} - \item Higher-order patterns in the sense of @{cite "nipkow-patterns"}. + \<^enum> Higher-order patterns in the sense of @{cite "nipkow-patterns"}. These are terms in @{text "\"}-normal form (this will always be the case unless you have done something strange) where each occurrence of an unknown is of the form @{text "?F x\<^sub>1 \ x\<^sub>n"}, where the @@ -554,7 +561,7 @@ or its symmetric form, since the @{text "rhs"} is also a higher-order pattern. - \item Physical first-order patterns over raw @{text "\"}-term + \<^enum> Physical first-order patterns over raw @{text "\"}-term structure without @{text "\\\"}-equality; abstractions and bound variables are treated like quasi-constant term material. @@ -591,12 +598,14 @@ %The local assumptions are also provided as theorems to the solver; %see \secref{sec:simp-solver} below. - \medskip The following congruence rule for bounded quantifiers also + \<^medskip> + The following congruence rule for bounded quantifiers also supplies contextual information --- about the bound variable: @{text [display] "(?A = ?B) \ (\x. x \ ?B \ ?P x \ ?Q x) \ (\x \ ?A. ?P x) \ (\x \ ?B. ?Q x)"} - \medskip This congruence rule for conditional expressions can + \<^medskip> + This congruence rule for conditional expressions can supply contextual information for simplifying the arms: @{text [display] "?p = ?q \ (?q \ ?a = ?c) \ (\ ?q \ ?b = ?d) \ (if ?p then ?a else ?b) = (if ?q then ?c else ?d)"} @@ -636,7 +645,8 @@ @{command "definition"} is an exception in \emph{not} declaring anything. - \medskip It is up the user to manipulate the current simpset further + \<^medskip> + It is up the user to manipulate the current simpset further by explicitly adding or deleting theorems as simplification rules, or installing other tools via simplification procedures (\secref{sec:simproc}). Good simpsets are hard to design. Rules @@ -682,7 +692,8 @@ could be also changed locally for special applications via @{index_ML Simplifier.set_termless} in Isabelle/ML. - \medskip Permutative rewrite rules are declared to the Simplifier + \<^medskip> + Permutative rewrite rules are declared to the Simplifier just like other rewrite rules. Their special status is recognized automatically, and their application is guarded by the term ordering accordingly.\ @@ -697,12 +708,12 @@ \begin{itemize} - \item The associative law must always be oriented from left to + \<^item> The associative law must always be oriented from left to right, namely @{text "f (f x y) z = f x (f y z)"}. The opposite orientation, if used with commutativity, leads to looping in conjunction with the standard term order. - \item To complete your set of rewrite rules, you must add not just + \<^item> To complete your set of rewrite rules, you must add not just associativity (A) and commutativity (C) but also a derived rule \emph{left-commutativity} (LC): @{text "f x (f y z) = f y (f x z)"}. @@ -769,7 +780,7 @@ @{attribute_def simp_trace_new} & : & @{text attribute} \\ @{attribute_def simp_break} & : & @{text attribute} \\ \end{tabular} - \medskip + \<^medskip> @{rail \ @@{attribute simp_trace_new} ('interactive')? \ @@ -983,7 +994,8 @@ Solvers are packaged up in abstract type @{ML_type solver}, with @{ML Simplifier.mk_solver} as the only operation to create a solver. - \medskip Rewriting does not instantiate unknowns. For example, + \<^medskip> + Rewriting does not instantiate unknowns. For example, rewriting alone cannot prove @{text "a \ ?A"} since this requires instantiating @{text "?A"}. The solver, however, is an arbitrary tactic and may instantiate unknowns as it pleases. This is the only @@ -1024,7 +1036,8 @@ \end{description} - \medskip The solver tactic is invoked with the context of the + \<^medskip> + The solver tactic is invoked with the context of the running Simplifier. Further operations may be used to retrieve relevant information, such as the list of local Simplifier premises via @{ML Simplifier.prems_of} --- this @@ -1035,7 +1048,8 @@ assume_tac}), even if the Simplifier proper happens to ignore local premises at the moment. - \medskip As explained before, the subgoaler is also used to solve + \<^medskip> + As explained before, the subgoaler is also used to solve the premises of congruence rules. These are usually of the form @{text "s = ?x"}, where @{text "s"} needs to be simplified and @{text "?x"} needs to be instantiated with the result. Typically, @@ -1051,8 +1065,7 @@ try resolving with the theorem @{text "\ False"} of the object-logic. - \medskip - + \<^medskip> \begin{warn} If a premise of a congruence rule cannot be proved, then the congruence is ignored. This should only happen if the rule is @@ -1563,21 +1576,21 @@ \begin{itemize} - \item It does not use the classical wrapper tacticals, such as the + \<^item> It does not use the classical wrapper tacticals, such as the integration with the Simplifier of @{method fastforce}. - \item It does not perform higher-order unification, as needed by the + \<^item> It does not perform higher-order unification, as needed by the rule @{thm [source=false] rangeI} in HOL. There are often alternatives to such rules, for example @{thm [source=false] range_eqI}. - \item Function variables may only be applied to parameters of the + \<^item> Function variables may only be applied to parameters of the subgoal. (This restriction arises because the prover does not use higher-order unification.) If other function variables are present then the prover will fail with the message @{verbatim [display] \Function unknown's argument not a bound variable\} - \item Its proof strategy is more general than @{method fast} but can + \<^item> Its proof strategy is more general than @{method fast} but can be slower. If @{method blast} fails or seems to be running forever, try @{method fast} and the other proof tools described below. @@ -1909,7 +1922,7 @@ @{attribute_def unify_trace_bound} & : & @{text "attribute"} & default @{text "50"} \\ @{attribute_def unify_search_bound} & : & @{text "attribute"} & default @{text "60"} \\ \end{tabular} - \medskip + \<^medskip> Higher-order unification works well in most practical situations, but sometimes needs extra care to identify problems. These tracing diff -r ee42cba50933 -r e0825405d398 src/Doc/Isar_Ref/HOL_Specific.thy --- a/src/Doc/Isar_Ref/HOL_Specific.thy Mon Oct 12 21:42:14 2015 +0200 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy Mon Oct 12 22:03:24 2015 +0200 @@ -35,7 +35,8 @@ mathematics, but for most applications this does not matter. If you prefer ML to Lisp, you will probably prefer HOL to ZF. - \medskip The syntax of HOL follows @{text "\"}-calculus and + \<^medskip> + The syntax of HOL follows @{text "\"}-calculus and functional programming. Function application is curried. To apply the function @{text f} of type @{text "\\<^sub>1 \ \\<^sub>2 \ \\<^sub>3"} to the arguments @{text a} and @{text b} in HOL, you simply write @{text "f @@ -47,7 +48,8 @@ be avoided by currying functions by default. Explicit tuples are as infrequent in HOL formalizations as in good ML or Haskell programs. - \medskip Isabelle/HOL has a distinct feel, compared to other + \<^medskip> + Isabelle/HOL has a distinct feel, compared to other object-logics like Isabelle/ZF. It identifies object-level types with meta-level types, taking advantage of the default type-inference mechanism of Isabelle/Pure. HOL fully identifies @@ -192,25 +194,25 @@ \begin{itemize} - \item Theorems of the form @{text "A \ B \ \ A \ \ B"}, for proving + \<^item> Theorems of the form @{text "A \ B \ \ A \ \ B"}, for proving monotonicity of inductive definitions whose introduction rules have premises involving terms such as @{text "\ R t"}. - \item Monotonicity theorems for logical operators, which are of the + \<^item> Monotonicity theorems for logical operators, which are of the general form @{text "(\ \ \) \ \ (\ \ \) \ \ \ \"}. For example, in the case of the operator @{text "\"}, the corresponding theorem is \[ \infer{@{text "P\<^sub>1 \ P\<^sub>2 \ Q\<^sub>1 \ Q\<^sub>2"}}{@{text "P\<^sub>1 \ Q\<^sub>1"} & @{text "P\<^sub>2 \ Q\<^sub>2"}} \] - \item De Morgan style equations for reasoning about the ``polarity'' + \<^item> De Morgan style equations for reasoning about the ``polarity'' of expressions, e.g. \[ @{prop "\ \ P \ P"} \qquad\qquad @{prop "\ (P \ Q) \ \ P \ \ Q"} \] - \item Equations for reducing complex operators to more primitive + \<^item> Equations for reducing complex operators to more primitive ones whose monotonicity can easily be proved, e.g. \[ @{prop "(P \ Q) \ \ P \ Q"} \qquad\qquad @@ -395,8 +397,7 @@ | And "'a bexp" "'a bexp" | Neg "'a bexp" - -text \\medskip Evaluation of arithmetic and boolean expressions\ +text \\<^medskip> Evaluation of arithmetic and boolean expressions\ primrec evala :: "('a \ nat) \ 'a aexp \ nat" and evalb :: "('a \ nat) \ 'a bexp \ bool" @@ -415,7 +416,8 @@ additional parameter, an \emph{environment} that maps variables to their values. - \medskip Substitution on expressions can be defined similarly. The mapping + \<^medskip> + Substitution on expressions can be defined similarly. The mapping @{text f} of type @{typ "'a \ 'a aexp"} given as a parameter is lifted canonically on the types @{typ "'a aexp"} and @{typ "'a bexp"}, respectively. @@ -501,7 +503,8 @@ be applied to an argument. In particular, @{term "map_tree f \ ts"} is not allowed here. - \medskip Here is a simple composition lemma for @{term map_tree}: + \<^medskip> + Here is a simple composition lemma for @{term map_tree}: \ lemma "map_tree g (map_tree f t) = map_tree (g \ f) t" @@ -683,7 +686,8 @@ \end{description} - \medskip Hints for @{command (HOL) "recdef"} may be also declared + \<^medskip> + Hints for @{command (HOL) "recdef"} may be also declared globally, using the following attributes. \begin{matharray}{rcl} @@ -708,8 +712,7 @@ @{attribute_def "show_variants"} & : & @{text "attribute"} & default @{text false} \\ \end{tabular} - \medskip - + \<^medskip> Adhoc overloading allows to overload a constant depending on its type. Typically this involves the introduction of an uninterpreted constant (used for input and output) and the addition @@ -899,20 +902,22 @@ element. In fact, @{text "\x = a, y = b\"} is just an abbreviation for @{text "\x = a, y = b, \ = ()\"}. - \medskip Two key observations make extensible records in a simply + \<^medskip> + Two key observations make extensible records in a simply typed language like HOL work out: \begin{enumerate} - \item the more part is internalized, as a free term or type + \<^enum> the more part is internalized, as a free term or type variable, - \item field names are externalized, they cannot be accessed within + \<^enum> field names are externalized, they cannot be accessed within the logic as first-class values. \end{enumerate} - \medskip In Isabelle/HOL record types have to be defined explicitly, + \<^medskip> + In Isabelle/HOL record types have to be defined explicitly, fixing their field names and types, and their (optional) parent record. Afterwards, records may be formed using above syntax, while obeying the canonical order of fields as given by their declaration. @@ -980,7 +985,8 @@ assume for now that @{text "(\\<^sub>1, \, \\<^sub>m) t"} is a root record with fields @{text "c\<^sub>1 :: \\<^sub>1, \, c\<^sub>n :: \\<^sub>n"}. - \medskip \textbf{Selectors} and \textbf{updates} are available for any + \<^medskip> + \textbf{Selectors} and \textbf{updates} are available for any field (including ``@{text more}''): \begin{matharray}{lll} @@ -998,14 +1004,16 @@ equality is concerned. Thus commutativity of independent updates can be proven within the logic for any two fields, but not as a general theorem. - \medskip The \textbf{make} operation provides a cumulative record + \<^medskip> + The \textbf{make} operation provides a cumulative record constructor function: \begin{matharray}{lll} @{text "t.make"} & @{text "::"} & @{text "\\<^sub>1 \ \ \\<^sub>n \ \\<^vec>c :: \<^vec>\\"} \\ \end{matharray} - \medskip We now reconsider the case of non-root records, which are derived + \<^medskip> + We now reconsider the case of non-root records, which are derived of some parent. In general, the latter may depend on another parent as well, resulting in a list of \emph{ancestor records}. Appending the lists of fields of all ancestors results in a certain field prefix. The record @@ -1014,7 +1022,7 @@ ancestor fields @{text "b\<^sub>1 :: \\<^sub>1, \, b\<^sub>k :: \\<^sub>k"}, the above record operations will get the following types: - \medskip + \<^medskip> \begin{tabular}{lll} @{text "c\<^sub>i"} & @{text "::"} & @{text "\\<^vec>b :: \<^vec>\, \<^vec>c :: \<^vec>\, \ :: \\ \ \\<^sub>i"} \\ @{text "c\<^sub>i_update"} & @{text "::"} & @{text "\\<^sub>i \ @@ -1023,7 +1031,7 @@ @{text "t.make"} & @{text "::"} & @{text "\\<^sub>1 \ \ \\<^sub>k \ \\<^sub>1 \ \ \\<^sub>n \ \\<^vec>b :: \<^vec>\, \<^vec>c :: \<^vec>\\"} \\ \end{tabular} - \medskip + \<^medskip> Some further operations address the extension aspect of a derived record scheme specifically: @{text "t.fields"} produces a record @@ -1032,14 +1040,14 @@ record and adds a given more part; @{text "t.truncate"} restricts a record scheme to a fixed record. - \medskip + \<^medskip> \begin{tabular}{lll} @{text "t.fields"} & @{text "::"} & @{text "\\<^sub>1 \ \ \\<^sub>n \ \\<^vec>c :: \<^vec>\\"} \\ @{text "t.extend"} & @{text "::"} & @{text "\\<^vec>b :: \<^vec>\, \<^vec>c :: \<^vec>\\ \ \ \ \\<^vec>b :: \<^vec>\, \<^vec>c :: \<^vec>\, \ :: \\"} \\ @{text "t.truncate"} & @{text "::"} & @{text "\\<^vec>b :: \<^vec>\, \<^vec>c :: \<^vec>\, \ :: \\ \ \\<^vec>b :: \<^vec>\, \<^vec>c :: \<^vec>\\"} \\ \end{tabular} - \medskip + \<^medskip> Note that @{text "t.make"} and @{text "t.fields"} coincide for root records. @@ -1056,26 +1064,26 @@ \begin{enumerate} - \item Standard conversions for selectors or updates applied to record + \<^enum> Standard conversions for selectors or updates applied to record constructor terms are made part of the default Simplifier context; thus proofs by reduction of basic operations merely require the @{method simp} method without further arguments. These rules are available as @{text "t.simps"}, too. - \item Selectors applied to updated records are automatically reduced by an + \<^enum> Selectors applied to updated records are automatically reduced by an internal simplification procedure, which is also part of the standard Simplifier setup. - \item Inject equations of a form analogous to @{prop "(x, y) = (x', y') \ + \<^enum> Inject equations of a form analogous to @{prop "(x, y) = (x', y') \ x = x' \ y = y'"} are declared to the Simplifier and Classical Reasoner as @{attribute iff} rules. These rules are available as @{text "t.iffs"}. - \item The introduction rule for record equality analogous to @{text "x r = + \<^enum> The introduction rule for record equality analogous to @{text "x r = x r' \ y r = y r' \ \ r = r'"} is declared to the Simplifier, and as the basic rule context as ``@{attribute intro}@{text "?"}''. The rule is called @{text "t.equality"}. - \item Representations of arbitrary record expressions as canonical + \<^enum> Representations of arbitrary record expressions as canonical constructor terms are provided both in @{method cases} and @{method induct} format (cf.\ the generic proof methods of the same name, \secref{sec:cases-induct}). Several variations are available, for fixed @@ -1086,7 +1094,7 @@ need to apply something like ``@{text "(cases r)"}'' to a certain proof problem. - \item The derived record operations @{text "t.make"}, @{text "t.fields"}, + \<^enum> The derived record operations @{text "t.make"}, @{text "t.fields"}, @{text "t.extend"}, @{text "t.truncate"} are \emph{not} treated automatically, but usually need to be expanded by hand, using the collective fact @{text "t.defs"}. @@ -1135,7 +1143,8 @@ virtues'' of this relatively simple family of logics. STT has only ground types, without polymorphism and without type definitions. - \medskip M. Gordon @{cite "Gordon:1985:HOL"} augmented Church's STT by + \<^medskip> + M. Gordon @{cite "Gordon:1985:HOL"} augmented Church's STT by adding schematic polymorphism (type variables and type constructors) and a facility to introduce new types as semantic subtypes from existing types. This genuine extension of the logic was explained semantically by A. Pitts @@ -1145,7 +1154,8 @@ interpretations is closed by forming subsets (via predicates taken from the logic). - \medskip Isabelle/HOL goes beyond Gordon-style HOL by admitting overloaded + \<^medskip> + Isabelle/HOL goes beyond Gordon-style HOL by admitting overloaded constant definitions @{cite "Wenzel:1997:TPHOL" and "Haftmann-Wenzel:2006:classes"}, which are actually a concept of Isabelle/Pure and do not depend on particular set-theoretic semantics of @@ -1402,7 +1412,7 @@ \begin{enumerate} - \item The first one is a low-level mode when the user must provide as a + \<^enum> The first one is a low-level mode when the user must provide as a first argument of @{command (HOL) "setup_lifting"} a quotient theorem @{term "Quotient R Abs Rep T"}. The package configures a transfer rule for equality, a domain transfer rules and sets up the @{command_def (HOL) @@ -1416,7 +1426,7 @@ Users generally will not prove the @{text Quotient} theorem manually for new types, as special commands exist to automate the process. - \item When a new subtype is defined by @{command (HOL) typedef}, @{command + \<^enum> When a new subtype is defined by @{command (HOL) typedef}, @{command (HOL) "lift_definition"} can be used in its second mode, where only the @{term type_definition} theorem @{term "type_definition Rep Abs A"} is used as an argument of the command. The command internally proves the @@ -1430,7 +1440,8 @@ the corresponding Quotient theorem is proved and registered by @{command (HOL) setup_lifting}. - \medskip The command @{command (HOL) "setup_lifting"} also sets up the + \<^medskip> + The command @{command (HOL) "setup_lifting"} also sets up the code generator for the new type. Later on, when a new constant is defined by @{command (HOL) "lift_definition"}, the Lifting package proves and registers a code equation (if there is one) for the new constant. @@ -1463,7 +1474,8 @@ unconditional for total quotients. The equation defines @{text f} using the abstraction function. - \medskip Integration with [@{attribute code} abstract]: For subtypes + \<^medskip> + Integration with [@{attribute code} abstract]: For subtypes (e.g.\ corresponding to a datatype invariant, such as @{typ "'a dlist"}), @{command (HOL) "lift_definition"} uses a code certificate theorem @{text f.rep_eq} as a code equation. Because of the limitation of the code @@ -2292,7 +2304,7 @@ \begin{enumerate} - \item Universal problems over multivariate polynomials in a + \<^enum> Universal problems over multivariate polynomials in a (semi)-ring/field/idom; the capabilities of the method are augmented according to properties of these structures. For this problem class the method is only complete for algebraically closed fields, since @@ -2302,7 +2314,7 @@ The problems can contain equations @{text "p = 0"} or inequations @{text "q \ 0"} anywhere within a universal problem statement. - \item All-exists problems of the following restricted (but useful) + \<^enum> All-exists problems of the following restricted (but useful) form: @{text [display] "\x\<^sub>1 \ x\<^sub>n. diff -r ee42cba50933 -r e0825405d398 src/Doc/Isar_Ref/Inner_Syntax.thy --- a/src/Doc/Isar_Ref/Inner_Syntax.thy Mon Oct 12 21:42:14 2015 +0200 +++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Mon Oct 12 22:03:24 2015 +0200 @@ -138,7 +138,7 @@ @{attribute_def show_tags} & : & @{text attribute} & default @{text false} \\ @{attribute_def show_question_marks} & : & @{text attribute} & default @{text true} \\ \end{tabular} - \medskip + \<^medskip> These configuration options control the detail of information that is displayed for types, terms, theorems, goals etc. See also @@ -273,7 +273,8 @@ \end{description} - \medskip The pretty printer for inner syntax maintains alternative + \<^medskip> + The pretty printer for inner syntax maintains alternative mixfix productions for any print mode name invented by the user, say in commands like @{command notation} or @{command abbreviation}. Mode names can be arbitrary, but the following ones have a specific @@ -281,24 +282,24 @@ \begin{itemize} - \item @{verbatim \""\} (the empty string): default mode; + \<^item> @{verbatim \""\} (the empty string): default mode; implicitly active as last element in the list of modes. - \item @{verbatim input}: dummy print mode that is never active; may + \<^item> @{verbatim input}: dummy print mode that is never active; may be used to specify notation that is only available for input. - \item @{verbatim internal} dummy print mode that is never active; + \<^item> @{verbatim internal} dummy print mode that is never active; used internally in Isabelle/Pure. - \item @{verbatim xsymbols}: enable proper mathematical symbols + \<^item> @{verbatim xsymbols}: enable proper mathematical symbols instead of ASCII art.\footnote{This traditional mode name stems from the ``X-Symbol'' package for classic Proof~General with XEmacs.} - \item @{verbatim HTML}: additional mode that is active in HTML + \<^item> @{verbatim HTML}: additional mode that is active in HTML presentation of Isabelle theory sources; allows to provide alternative output notation. - \item @{verbatim latex}: additional mode that is active in {\LaTeX} + \<^item> @{verbatim latex}: additional mode that is active in {\LaTeX} document preparation of Isabelle theory sources; allows to provide alternative output notation. @@ -370,7 +371,8 @@ instead. If a term has fewer arguments than specified in the mixfix template, the concrete syntax is ignored. - \medskip A mixfix template may also contain additional directives + \<^medskip> + A mixfix template may also contain additional directives for pretty printing, notably spaces, blocks, and breaks. The general template format is a sequence over any of the following entities. @@ -380,7 +382,7 @@ \item @{text "d"} is a delimiter, namely a non-empty sequence of characters other than the following special characters: - \smallskip + \<^medskip> \begin{tabular}{ll} @{verbatim "'"} & single quote \\ @{verbatim "_"} & underscore \\ @@ -389,7 +391,7 @@ @{verbatim ")"} & close parenthesis \\ @{verbatim "/"} & slash \\ \end{tabular} - \medskip + \<^medskip> \item @{verbatim "'"} escapes the special meaning of these meta-characters, producing a literal version of the following @@ -565,11 +567,11 @@ \begin{enumerate} - \item \emph{delimiters} --- the literal tokens occurring in + \<^enum> \emph{delimiters} --- the literal tokens occurring in productions of the given priority grammar (cf.\ \secref{sec:priority-grammar}); - \item \emph{named tokens} --- various categories of identifiers etc. + \<^enum> \emph{named tokens} --- various categories of identifiers etc. \end{enumerate} @@ -578,7 +580,8 @@ alternative ways to refer to the same entity, potentially via qualified names. - \medskip The categories for named tokens are defined once and for + \<^medskip> + The categories for named tokens are defined once and for all as follows, reusing some categories of the outer token syntax (\secref{sec:outer-lex}). @@ -628,13 +631,15 @@ priority grammar can be translated into a normal context-free grammar by introducing new nonterminals and productions. - \medskip Formally, a set of context free productions @{text G} + \<^medskip> + Formally, a set of context free productions @{text G} induces a derivation relation @{text "\\<^sub>G"} as follows. Let @{text \} and @{text \} denote strings of terminal or nonterminal symbols. Then @{text "\ A\<^sup>(\<^sup>p\<^sup>) \ \\<^sub>G \ \ \"} holds if and only if @{text G} contains some production @{text "A\<^sup>(\<^sup>q\<^sup>) = \"} for @{text "p \ q"}. - \medskip The following grammar for arithmetic expressions + \<^medskip> + The following grammar for arithmetic expressions demonstrates how binding power and associativity of operators can be enforced by priorities. @@ -652,21 +657,22 @@ "+"}. Furthermore @{verbatim "+"} associates to the left and @{verbatim "*"} to the right. - \medskip For clarity, grammars obey these conventions: + \<^medskip> + For clarity, grammars obey these conventions: \begin{itemize} - \item All priorities must lie between 0 and 1000. + \<^item> All priorities must lie between 0 and 1000. - \item Priority 0 on the right-hand side and priority 1000 on the + \<^item> Priority 0 on the right-hand side and priority 1000 on the left-hand side may be omitted. - \item The production @{text "A\<^sup>(\<^sup>p\<^sup>) = \"} is written as @{text "A = \ + \<^item> The production @{text "A\<^sup>(\<^sup>p\<^sup>) = \"} is written as @{text "A = \ (p)"}, i.e.\ the priority of the left-hand side actually appears in a column on the far right. - \item Alternatives are separated by @{text "|"}. + \<^item> Alternatives are separated by @{text "|"}. - \item Repetition is indicated by dots @{text "(\)"} in an informal + \<^item> Repetition is indicated by dots @{text "(\)"} in an informal but obvious way. \end{itemize} @@ -759,7 +765,8 @@ \end{supertabular} \end{center} - \medskip Here literal terminals are printed @{verbatim "verbatim"}; + \<^medskip> + Here literal terminals are printed @{verbatim "verbatim"}; see also \secref{sec:inner-lex} for further token categories of the inner syntax. The meaning of the nonterminals defined by the above grammar is as follows: @@ -823,23 +830,23 @@ \begin{itemize} - \item In @{syntax (inner) idts}, note that @{text "x :: nat y"} is + \<^item> In @{syntax (inner) idts}, note that @{text "x :: nat y"} is parsed as @{text "x :: (nat y)"}, treating @{text y} like a type constructor applied to @{text nat}. To avoid this interpretation, write @{text "(x :: nat) y"} with explicit parentheses. - \item Similarly, @{text "x :: nat y :: nat"} is parsed as @{text "x :: + \<^item> Similarly, @{text "x :: nat y :: nat"} is parsed as @{text "x :: (nat y :: nat)"}. The correct form is @{text "(x :: nat) (y :: nat)"}, or @{text "(x :: nat) y :: nat"} if @{text y} is last in the sequence of identifiers. - \item Type constraints for terms bind very weakly. For example, + \<^item> Type constraints for terms bind very weakly. For example, @{text "x < y :: nat"} is normally parsed as @{text "(x < y) :: nat"}, unless @{text "<"} has a very low priority, in which case the input is likely to be ambiguous. The correct form is @{text "x < (y :: nat)"}. - \item Dummy variables (written as underscore) may occur in different + \<^item> Dummy variables (written as underscore) may occur in different roles. \begin{description} @@ -1053,7 +1060,8 @@ @{verbatim "()"} and @{verbatim "(x)"} are excluded as ASTs, because they have too few subtrees. - \medskip AST application is merely a pro-forma mechanism to indicate + \<^medskip> + AST application is merely a pro-forma mechanism to indicate certain syntactic structures. Thus @{verbatim "(c a b)"} could mean either term application or type application, depending on the syntactic context. @@ -1090,7 +1098,8 @@ variables (free or schematic) into @{ML Ast.Variable}. This information is precise when printing fully formal @{text "\"}-terms. - \medskip AST translation patterns (\secref{sec:syn-trans}) that + \<^medskip> + AST translation patterns (\secref{sec:syn-trans}) that represent terms cannot distinguish constants and variables syntactically. Explicit indication of @{text "CONST c"} inside the term language is required, unless @{text "c"} is known as special @@ -1126,16 +1135,16 @@ \begin{itemize} - \item Input of term constants (or fixed variables) that are + \<^item> Input of term constants (or fixed variables) that are introduced by concrete syntax via @{command notation}: the correspondence of a particular grammar production to some known term entity is preserved. - \item Input of type constants (constructors) and type classes --- + \<^item> Input of type constants (constructors) and type classes --- thanks to explicit syntactic distinction independently on the context. - \item Output of term constants, type constants, type classes --- + \<^item> Output of term constants, type constants, type classes --- this information is already available from the internal term to be printed. @@ -1159,8 +1168,7 @@ @{attribute_def syntax_ast_trace} & : & @{text attribute} & default @{text false} \\ @{attribute_def syntax_ast_stats} & : & @{text attribute} & default @{text false} \\ \end{tabular} - - \medskip + \<^medskip> Unlike mixfix notation for existing formal entities (\secref{sec:notation}), raw syntax declarations provide full access @@ -1207,14 +1215,14 @@ follows: \begin{itemize} - \item @{text "prop"} if @{text "\\<^sub>i = prop"} + \<^item> @{text "prop"} if @{text "\\<^sub>i = prop"} - \item @{text "logic"} if @{text "\\<^sub>i = (\)\"} for logical type + \<^item> @{text "logic"} if @{text "\\<^sub>i = (\)\"} for logical type constructor @{text "\ \ prop"} - \item @{text any} if @{text "\\<^sub>i = \"} for type variables + \<^item> @{text any} if @{text "\\<^sub>i = \"} for type variables - \item @{text "\"} if @{text "\\<^sub>i = \"} for nonterminal @{text "\"} + \<^item> @{text "\"} if @{text "\\<^sub>i = \"} for nonterminal @{text "\"} (syntactic type constructor) \end{itemize} @@ -1225,7 +1233,8 @@ The resulting nonterminal of the production is determined similarly from type @{text "\"}, with priority @{text "q"} and default 1000. - \medskip Parsing via this production produces parse trees @{text + \<^medskip> + Parsing via this production produces parse trees @{text "t\<^sub>1, \, t\<^sub>n"} for the argument slots. The resulting parse tree is composed as @{text "c t\<^sub>1 \ t\<^sub>n"}, by using the syntax constant @{text "c"} of the syntax declaration. @@ -1236,7 +1245,8 @@ "_foobar"}). Names should be chosen with care, to avoid clashes with other syntax declarations. - \medskip The special case of copy production is specified by @{text + \<^medskip> + The special case of copy production is specified by @{text "c = "}@{verbatim \""\} (empty string). It means that the resulting parse tree @{text "t"} is copied directly, without any further decoration. @@ -1281,13 +1291,13 @@ \begin{itemize} - \item Rules must be left linear: @{text "lhs"} must not contain + \<^item> Rules must be left linear: @{text "lhs"} must not contain repeated variables.\footnote{The deeper reason for this is that AST equality is not well-defined: different occurrences of the ``same'' AST could be decorated differently by accidental type-constraints or source position information, for example.} - \item Every variable in @{text "rhs"} must also occur in @{text + \<^item> Every variable in @{text "rhs"} must also occur in @{text "lhs"}. \end{itemize} @@ -1312,11 +1322,11 @@ \begin{itemize} - \item Iterated replacement via recursive @{command translations}. + \<^item> Iterated replacement via recursive @{command translations}. For example, consider list enumeration @{term "[a, b, c, d]"} as defined in theory @{theory List} in Isabelle/HOL. - \item Change of binding status of variables: anything beyond the + \<^item> Change of binding status of variables: anything beyond the built-in @{keyword "binder"} mixfix annotation requires explicit syntax translations. For example, consider list filter comprehension @{term "[x \ xs . P]"} as defined in theory @{theory @@ -1348,21 +1358,21 @@ \begin{itemize} - \item Objects of the form @{ML Ast.Variable}~@{text "x"} or @{ML + \<^item> Objects of the form @{ML Ast.Variable}~@{text "x"} or @{ML Ast.Constant}~@{text "x"} are matched by pattern @{ML Ast.Constant}~@{text "x"}. Thus all atomic ASTs in the object are treated as (potential) constants, and a successful match makes them actual constants even before name space resolution (see also \secref{sec:ast}). - \item Object @{text "u"} is matched by pattern @{ML + \<^item> Object @{text "u"} is matched by pattern @{ML Ast.Variable}~@{text "x"}, binding @{text "x"} to @{text "u"}. - \item Object @{ML Ast.Appl}~@{text "us"} is matched by @{ML + \<^item> Object @{ML Ast.Appl}~@{text "us"} is matched by @{ML Ast.Appl}~@{text "ts"} if @{text "us"} and @{text "ts"} have the same length and each corresponding subtree matches. - \item In every other case, matching fails. + \<^item> In every other case, matching fails. \end{itemize} @@ -1436,7 +1446,7 @@ @{syntax text} argument that refers to an ML expression of appropriate type as follows: - \medskip + \<^medskip> {\footnotesize \begin{tabular}{l} @{command parse_ast_translation} : \\ @@ -1450,7 +1460,7 @@ @{command print_ast_translation} : \\ \quad @{ML_type "(string * (Proof.context -> Ast.ast list -> Ast.ast)) list"} \\ \end{tabular}} - \medskip + \<^medskip> The argument list consists of @{text "(c, tr)"} pairs, where @{text "c"} is the syntax name of the formal entity involved, and @{text @@ -1627,7 +1637,8 @@ finally pretty-printed. The built-in print AST translations reverse the corresponding parse AST translations. - \medskip For the actual printing process, the priority grammar + \<^medskip> + For the actual printing process, the priority grammar (\secref{sec:priority-grammar}) plays a vital role: productions are used as templates for pretty printing, with argument slots stemming from nonterminals, and syntactic sugar stemming from literal tokens. @@ -1655,7 +1666,8 @@ in order of appearance within the grammar. An occurrence of some AST variable @{text "x"} is printed as @{text "x"} outright. - \medskip White space is \emph{not} inserted automatically. If + \<^medskip> + White space is \emph{not} inserted automatically. If blanks (or breaks) are required to separate tokens, they need to be specified in the mixfix declaration (\secref{sec:mixfix}). \ diff -r ee42cba50933 -r e0825405d398 src/Doc/Isar_Ref/Outer_Syntax.thy --- a/src/Doc/Isar_Ref/Outer_Syntax.thy Mon Oct 12 21:42:14 2015 +0200 +++ b/src/Doc/Isar_Ref/Outer_Syntax.thy Mon Oct 12 22:03:24 2015 +0200 @@ -15,7 +15,8 @@ Concrete theory and proof language elements will be introduced later on. - \medskip In order to get started with writing well-formed + \<^medskip> + In order to get started with writing well-formed Isabelle/Isar documents, the most important aspect to be noted is the difference of \emph{inner} versus \emph{outer} syntax. Inner syntax is that of Isabelle types and terms of the logic, while outer @@ -74,13 +75,13 @@ \begin{enumerate} - \item \emph{major keywords} --- the command names that are available + \<^enum> \emph{major keywords} --- the command names that are available in the present logic session; - \item \emph{minor keywords} --- additional literal tokens required + \<^enum> \emph{minor keywords} --- additional literal tokens required by the syntax of commands; - \item \emph{named tokens} --- various categories of identifiers etc. + \<^enum> \emph{named tokens} --- various categories of identifiers etc. \end{enumerate} @@ -102,8 +103,8 @@ tabs, newlines and formfeeds between tokens serve as explicit separators. - \medskip The categories for named tokens are defined once and for - all as follows. + \<^medskip> + The categories for named tokens are defined once and for all as follows. \begin{center} \begin{supertabular}{rcl} @@ -341,7 +342,8 @@ @{syntax_def prop_pat}: '(' (@'is' @{syntax prop} +) ')' \} - \medskip Declarations of local variables @{text "x :: \"} and + \<^medskip> + Declarations of local variables @{text "x :: \"} and logical propositions @{text "a : \"} represent different views on the same principle of introducing a local scope. In practice, one may usually omit the typing of @{syntax vars} (due to @@ -412,11 +414,11 @@ There are three forms of theorem references: \begin{enumerate} - \item named facts @{text "a"}, + \<^enum> named facts @{text "a"}, - \item selections from named facts @{text "a(i)"} or @{text "a(j - k)"}, + \<^enum> selections from named facts @{text "a(i)"} or @{text "a(j - k)"}, - \item literal fact propositions using token syntax @{syntax_ref altstring} + \<^enum> literal fact propositions using token syntax @{syntax_ref altstring} @{verbatim "`"}@{text "\"}@{verbatim "`"} or @{syntax_ref cartouche} @{text "\\\"} (see also method @{method_ref fact}). diff -r ee42cba50933 -r e0825405d398 src/Doc/Isar_Ref/Preface.thy --- a/src/Doc/Isar_Ref/Preface.thy Mon Oct 12 21:42:14 2015 +0200 +++ b/src/Doc/Isar_Ref/Preface.thy Mon Oct 12 22:03:24 2015 +0200 @@ -26,7 +26,8 @@ Isabelle/jEdit Prover IDE @{cite "Wenzel:2012"} emphasizes the document-oriented approach of Isabelle/Isar again more explicitly. - \medskip Apart from the technical advances over bare-bones ML + \<^medskip> + Apart from the technical advances over bare-bones ML programming, the main purpose of the Isar language is to provide a conceptually different view on machine-checked proofs @{cite "Wenzel:1999:TPHOL" and "Wenzel-PhD"}. \emph{Isar} stands for @@ -49,7 +50,8 @@ structured proofs. Isabelle/Isar supports a broad range of proof styles, both readable and unreadable ones. - \medskip The generic Isabelle/Isar framework (see + \<^medskip> + The generic Isabelle/Isar framework (see \chref{ch:isar-framework}) works reasonably well for any Isabelle object-logic that conforms to the natural deduction view of the Isabelle/Pure framework. Specific language elements introduced by @@ -58,7 +60,8 @@ framework, examples given in the generic parts will usually refer to Isabelle/HOL. - \medskip Isar commands may be either \emph{proper} document + \<^medskip> + Isar commands may be either \emph{proper} document constructors, or \emph{improper commands}. Some proof methods and attributes introduced later are classified as improper as well. Improper Isar language elements, which are marked by ``@{text diff -r ee42cba50933 -r e0825405d398 src/Doc/Isar_Ref/Proof.thy --- a/src/Doc/Isar_Ref/Proof.thy Mon Oct 12 21:42:14 2015 +0200 +++ b/src/Doc/Isar_Ref/Proof.thy Mon Oct 12 22:03:24 2015 +0200 @@ -247,7 +247,8 @@ incremental type-inference, as the user proceeds to build up the Isar proof text from left to right. - \medskip Term abbreviations are quite different from local + \<^medskip> + Term abbreviations are quite different from local definitions as introduced via @{command "def"} (see \secref{sec:proof-context}). The latter are visible within the logic as actual equations, while abbreviations disappear during the @@ -554,7 +555,8 @@ calculations, there is no separate \emph{begin-calculation} command required. - \medskip The Isar calculation proof commands may be defined as + \<^medskip> + The Isar calculation proof commands may be defined as follows:\footnote{We suppress internal bookkeeping such as proper handling of block-structure.} @@ -651,7 +653,8 @@ the subsequent mechanisms allow to imitate the effect of subgoal addressing that is known from ML tactics. - \medskip Goal \emph{restriction} means the proof state is wrapped-up in a + \<^medskip> + Goal \emph{restriction} means the proof state is wrapped-up in a way that certain subgoals are exposed, and other subgoals are ``parked'' elsewhere. Thus a proof method has no other chance than to operate on the subgoals that are presently exposed. @@ -671,7 +674,8 @@ "(rule r, simp_all)[]"}'' simplifies all new goals that emerge from applying rule @{text "r"} to the originally first one. - \medskip Improper methods, notably tactic emulations, offer low-level goal + \<^medskip> + Improper methods, notably tactic emulations, offer low-level goal addressing as explicit argument to the individual tactic being involved. Here ``@{text "[!]"}'' refers to all goals, and ``@{text "[n-]"}'' to all goals starting from @{text "n"}. @@ -702,13 +706,13 @@ \begin{enumerate} - \item An \emph{initial} refinement step @{command_ref + \<^enum> An \emph{initial} refinement step @{command_ref "proof"}~@{text "m\<^sub>1"} reduces a newly stated goal to a number of sub-goals that are to be solved later. Facts are passed to @{text "m\<^sub>1"} for forward chaining, if so indicated by @{text "proof(chain)"} mode. - \item A \emph{terminal} conclusion step @{command_ref "qed"}~@{text + \<^enum> A \emph{terminal} conclusion step @{command_ref "qed"}~@{text "m\<^sub>2"} is intended to solve remaining goals. No facts are passed to @{text "m\<^sub>2"}. @@ -720,7 +724,8 @@ problem of unstructured tactic scripts that consist of numerous consecutive goal transformations, with invisible effects. - \medskip As a general rule of thumb for good proof style, initial + \<^medskip> + As a general rule of thumb for good proof style, initial proof methods should either solve the goal completely, or constitute some well-understood reduction to new sub-goals. Arbitrary automatic proof tools that are prone leave a large number of badly @@ -1053,7 +1058,8 @@ y\<^sub>1 \ y\<^sub>m)"}'' instead, the proof author is able to chose local names that fit nicely into the current context. - \medskip It is important to note that proper use of @{command + \<^medskip> + It is important to note that proper use of @{command "case"} does not provide means to peek at the current goal state, which is not directly observable in Isar! Nonetheless, goal refinement commands do provide named cases @{text "goal\<^sub>i"} @@ -1068,7 +1074,8 @@ previous theory specifications in a canonical way (say from @{command "inductive"} definitions). - \medskip Proper cases are only available if both the proof method + \<^medskip> + Proper cases are only available if both the proof method and the rules involved support this. By using appropriate attributes, case names, conclusions, and parameters may be also declared by hand. Thus variant versions of rules that have been @@ -1217,7 +1224,7 @@ The rule is determined as follows, according to the facts and arguments passed to the @{method cases} method: - \medskip + \<^medskip> \begin{tabular}{llll} facts & & arguments & rule \\\hline @{text "\ R"} & @{method cases} & & implicit rule @{text R} \\ @@ -1226,7 +1233,7 @@ @{text "\ A t"} & @{method cases} & @{text "\"} & inductive predicate/set elimination (of @{text A}) \\ @{text "\"} & @{method cases} & @{text "\ rule: R"} & explicit rule @{text R} \\ \end{tabular} - \medskip + \<^medskip> Several instantiations may be given, referring to the \emph{suffix} of premises of the case rule; within each premise, the \emph{prefix} @@ -1241,14 +1248,14 @@ @{method cases} method, but refer to induction rules, which are determined as follows: - \medskip + \<^medskip> \begin{tabular}{llll} facts & & arguments & rule \\\hline & @{method induct} & @{text "P x"} & datatype induction (type of @{text x}) \\ @{text "\ A x"} & @{method induct} & @{text "\"} & predicate/set induction (of @{text A}) \\ @{text "\"} & @{method induct} & @{text "\ rule: R"} & explicit rule @{text R} \\ \end{tabular} - \medskip + \<^medskip> Several instantiations may be given, each referring to some part of a mutual inductive definition or datatype --- only related partial @@ -1297,13 +1304,14 @@ @{method induct} method, but refers to coinduction rules, which are determined as follows: - \medskip + \<^medskip> \begin{tabular}{llll} goal & & arguments & rule \\\hline & @{method coinduct} & @{text x} & type coinduction (type of @{text x}) \\ @{text "A x"} & @{method coinduct} & @{text "\"} & predicate/set coinduction (of @{text A}) \\ @{text "\"} & @{method coinduct} & @{text "\ rule: R"} & explicit rule @{text R} \\ \end{tabular} + \<^medskip> Coinduction is the dual of induction. Induction essentially eliminates @{text "A x"} towards a generic result @{text "P x"}, @@ -1333,7 +1341,8 @@ The @{command "print_cases"} command prints all named cases present in the current proof state. - \medskip Despite the additional infrastructure, both @{method cases} + \<^medskip> + Despite the additional infrastructure, both @{method cases} and @{method coinduct} merely apply a certain rule, after instantiation, while conforming due to the usual way of monotonic natural deduction: the context of a structured statement @{text @@ -1363,7 +1372,8 @@ @{text c.IH}, @{text c.hyps} and @{text c.prems}, as above. - \medskip Facts presented to either method are consumed according to + \<^medskip> + Facts presented to either method are consumed according to the number of ``major premises'' of the rule involved, which is usually 0 for plain cases and induction rules of datatypes etc.\ and 1 for rules of inductive predicates or sets and the like. The @@ -1438,13 +1448,13 @@ soundness of this temporary context extension. As representative examples, one may think of standard rules from Isabelle/HOL like this: - \medskip + \<^medskip> \begin{tabular}{ll} @{text "\x. B x \ (\x. B x \ thesis) \ thesis"} \\ @{text "A \ B \ (A \ B \ thesis) \ thesis"} \\ @{text "A \ B \ (A \ thesis) \ (B \ thesis) \ thesis"} \\ \end{tabular} - \medskip + \<^medskip> In general, these particular rules and connectives need to get involved at all: this concept works directly in Isabelle/Pure via Isar commands @@ -1474,7 +1484,8 @@ the rule this is a fact name, in the resulting rule it is used as annotation with the @{attribute_ref case_names} attribute. - \medskip Formally, the command @{command consider} is defined as derived + \<^medskip> + Formally, the command @{command consider} is defined as derived Isar language element as follows: \begin{matharray}{l} @@ -1503,7 +1514,8 @@ export will fail! This restriction conforms to the usual manner of existential reasoning in Natural Deduction. - \medskip Formally, the command @{command obtain} is defined as derived + \<^medskip> + Formally, the command @{command obtain} is defined as derived Isar language element as follows, using an instrumented variant of @{command assume}: diff -r ee42cba50933 -r e0825405d398 src/Doc/Isar_Ref/Quick_Reference.thy --- a/src/Doc/Isar_Ref/Quick_Reference.thy Mon Oct 12 21:42:14 2015 +0200 +++ b/src/Doc/Isar_Ref/Quick_Reference.thy Mon Oct 12 22:03:24 2015 +0200 @@ -25,7 +25,7 @@ @{command "write"}~@{text "c (mx)"} & declare local mixfix syntax \\ \end{tabular} - \medskip + \<^medskip> \begin{tabular}{rcl} @{text "proof"} & = & @{text "prfx\<^sup>*"}~@{command "proof"}~@{text "method\<^sup>? stmt\<^sup>*"}~@{command "qed"}~@{text "method\<^sup>?"} \\ diff -r ee42cba50933 -r e0825405d398 src/Doc/Isar_Ref/Spec.thy --- a/src/Doc/Isar_Ref/Spec.thy Mon Oct 12 21:42:14 2015 +0200 +++ b/src/Doc/Isar_Ref/Spec.thy Mon Oct 12 22:03:24 2015 +0200 @@ -45,7 +45,8 @@ refer to local parameters and assumptions that are discharged later. See \secref{sec:target} for more details. - \medskip A theory is commenced by the @{command "theory"} command, which + \<^medskip> + A theory is commenced by the @{command "theory"} command, which indicates imports of previous theories, according to an acyclic foundational order. Before the initial @{command "theory"} command, there may be optional document header material (like @{command section} or @@ -199,7 +200,8 @@ "("}@{keyword "in"}~@{text "c)"}, but individual syntax diagrams omit that aspect for clarity. - \medskip The exact meaning of results produced within a local theory + \<^medskip> + The exact meaning of results produced within a local theory context depends on the underlying target infrastructure (locale, type class etc.). The general idea is as follows, considering a context named @{text c} with parameter @{text x} and assumption @{text "A[x]"}. @@ -628,7 +630,8 @@ \secref{sec:goals}, term bindings may be included as expected, though. - \medskip Locale specifications are ``closed up'' by + \<^medskip> + Locale specifications are ``closed up'' by turning the given text into a predicate definition @{text loc_axioms} and deriving the original assumptions as local lemmas (modulo local definitions). The predicate statement covers only the @@ -847,9 +850,13 @@ of @{command "interpretation"} and @{command "sublocale"}. It is available by importing theory @{file "~~/src/Tools/Permanent_Interpretation.thy"} and provides + \begin{enumerate} - \item a unified view on arbitrary suitable local theories as interpretation target; - \item rewrite morphisms by means of \emph{rewrite definitions}. + + \<^enum> a unified view on arbitrary suitable local theories as interpretation target; + + \<^enum> rewrite morphisms by means of \emph{rewrite definitions}. + \end{enumerate} \begin{matharray}{rcl} @@ -860,7 +867,6 @@ @@{command permanent_interpretation} @{syntax locale_expr} \ definitions? equations? ; - definitions: @'defining' (@{syntax thmdecl}? @{syntax name} \ @{syntax mixfix}? @'=' @{syntax term} + @'and'); equations: @'where' (@{syntax thmdecl}? @{syntax prop} + @'and') @@ -894,11 +900,11 @@ \begin{itemize} - \item produces a corresponding definition in - the local theory's underlying target \emph{and} - - \item augments the rewrite morphism with the equation - stemming from the symmetric of the corresponding definition. + \<^item> produces a corresponding definition in + the local theory's underlying target \emph{and} + + \<^item> augments the rewrite morphism with the equation + stemming from the symmetric of the corresponding definition. \end{itemize} @@ -907,11 +913,11 @@ \begin{itemize} - \item Definitions are parsed in the syntactic interpretation - context, just like equations. - - \item The proof needs not consider the equations stemming from - definitions -- they are proved implicitly by construction. + \<^item> Definitions are parsed in the syntactic interpretation + context, just like equations. + + \<^item> The proof needs not consider the equations stemming from + definitions -- they are proved implicitly by construction. \end{itemize} @@ -1054,14 +1060,14 @@ \begin{itemize} - \item Local constant declarations @{text "g[\]"} referring to the + \<^item> Local constant declarations @{text "g[\]"} referring to the local type parameter @{text \} and local parameters @{text "f[\]"} are accompanied by theory-level constants @{text "g[?\ :: c]"} referring to theory-level class operations @{text "f[?\ :: c]"}. - \item Local theorem bindings are lifted as are assumptions. + \<^item> Local theorem bindings are lifted as are assumptions. - \item Local syntax refers to local operations @{text "g[\]"} and + \<^item> Local syntax refers to local operations @{text "g[\]"} and global operations @{text "g[?\ :: c]"} uniformly. Type inference resolves ambiguities. In rare cases, manual type annotations are needed. @@ -1076,7 +1082,8 @@ type-constructor arities must obey the principle of \emph{co-regularity} as defined below. - \medskip For the subsequent formulation of co-regularity we assume + \<^medskip> + For the subsequent formulation of co-regularity we assume that the class relation is closed by transitivity and reflexivity. Moreover the collection of arities @{text "t :: (\<^vec>s)c"} is completed such that @{text "t :: (\<^vec>s)c"} and @{text "c \ c'"} @@ -1092,7 +1099,8 @@ This relation on sorts is further extended to tuples of sorts (of the same length) in the component-wise way. - \smallskip Co-regularity of the class relation together with the + \<^medskip> + Co-regularity of the class relation together with the arities relation means: \[ @{text "t :: (\<^vec>s\<^sub>1)c\<^sub>1 \ t :: (\<^vec>s\<^sub>2)c\<^sub>2 \ c\<^sub>1 \ c\<^sub>2 \ \<^vec>s\<^sub>1 \ \<^vec>s\<^sub>2"} @@ -1101,7 +1109,8 @@ classes of some type-constructor arities are related, then the argument sorts need to be related in the same way. - \medskip Co-regularity is a very fundamental property of the + \<^medskip> + Co-regularity is a very fundamental property of the order-sorted algebra of types. For example, it entails principle types and most general unifiers, e.g.\ see @{cite "nipkow-prehofer"}. \ @@ -1376,21 +1385,22 @@ definitions may be weakened by adding arbitrary pre-conditions: @{text "A \ c x y \ t"}. - \medskip The built-in well-formedness conditions for definitional + \<^medskip> + The built-in well-formedness conditions for definitional specifications are: \begin{itemize} - \item Arguments (on the left-hand side) must be distinct variables. + \<^item> Arguments (on the left-hand side) must be distinct variables. - \item All variables on the right-hand side must also appear on the + \<^item> All variables on the right-hand side must also appear on the left-hand side. - \item All type variables on the right-hand side must also appear on + \<^item> All type variables on the right-hand side must also appear on the left-hand side; this prohibits @{text "0 :: nat \ length ([] :: \ list)"} for example. - \item The definition must not be recursive. Most object-logics + \<^item> The definition must not be recursive. Most object-logics provide definitional principles that can be used to express recursion safely. diff -r ee42cba50933 -r e0825405d398 src/Doc/Isar_Ref/Synopsis.thy --- a/src/Doc/Isar_Ref/Synopsis.thy Mon Oct 12 21:42:14 2015 +0200 +++ b/src/Doc/Isar_Ref/Synopsis.thy Mon Oct 12 22:03:24 2015 +0200 @@ -131,18 +131,18 @@ text \ \begin{itemize} - \item Lower-case identifiers are usually preferred. + \<^item> Lower-case identifiers are usually preferred. - \item Facts can be named after the main term within the proposition. + \<^item> Facts can be named after the main term within the proposition. - \item Facts should \emph{not} be named after the command that + \<^item> Facts should \emph{not} be named after the command that introduced them (@{command "assume"}, @{command "have"}). This is misleading and hard to maintain. - \item Natural numbers can be used as ``meaningless'' names (more + \<^item> Natural numbers can be used as ``meaningless'' names (more appropriate than @{text "a1"}, @{text "a2"} etc.) - \item Symbolic identifiers are supported (e.g. @{text "*"}, @{text + \<^item> Symbolic identifiers are supported (e.g. @{text "*"}, @{text "**"}, @{text "***"}). \end{itemize} @@ -226,13 +226,13 @@ text \ \begin{itemize} - \item term @{text "?thesis"} --- the main conclusion of the + \<^item> term @{text "?thesis"} --- the main conclusion of the innermost pending claim - \item term @{text "\"} --- the argument of the last explicitly - stated result (for infix application this is the right-hand side) + \<^item> term @{text "\"} --- the argument of the last explicitly + stated result (for infix application this is the right-hand side) - \item fact @{text "this"} --- the last result produced in the text + \<^item> fact @{text "this"} --- the last result produced in the text \end{itemize} \ @@ -315,10 +315,10 @@ text \ \begin{itemize} - \item The notion of @{text trans} rule is very general due to the + \<^item> The notion of @{text trans} rule is very general due to the flexibility of Isabelle/Pure rule composition. - \item User applications may declare their own rules, with some care + \<^item> User applications may declare their own rules, with some care about the operational details of higher-order unification. \end{itemize} @@ -393,12 +393,12 @@ The proof method @{method induct} provides: \begin{itemize} - \item implicit rule selection and robust instantiation + \<^item> implicit rule selection and robust instantiation - \item context elements via symbolic case names + \<^item> context elements via symbolic case names - \item support for rule-structured induction statements, with local - parameters, premises, etc. + \<^item> support for rule-structured induction statements, with local + parameters, premises, etc. \end{itemize} \ @@ -423,13 +423,13 @@ The subsequent example combines the following proof patterns: \begin{itemize} - \item outermost induction (over the datatype structure of natural + \<^item> outermost induction (over the datatype structure of natural numbers), to decompose the proof problem in top-down manner - \item calculational reasoning (\secref{sec:calculations-synopsis}) + \<^item> calculational reasoning (\secref{sec:calculations-synopsis}) to compose the result in each case - \item solving local claims within the calculation by simplification + \<^item> solving local claims within the calculation by simplification \end{itemize} \ @@ -684,9 +684,9 @@ \begin{itemize} - \item backward-chaining of rules by @{inference resolution} + \<^item> backward-chaining of rules by @{inference resolution} - \item closing of branches by @{inference assumption} + \<^item> closing of branches by @{inference assumption} \end{itemize} @@ -974,10 +974,10 @@ \begin{itemize} - \item prefix of assumptions (or ``major premises'') + \<^item> prefix of assumptions (or ``major premises'') - \item one or more cases that enable to establish the main conclusion - in an augmented context + \<^item> one or more cases that enable to establish the main conclusion + in an augmented context \end{itemize} \ @@ -1017,11 +1017,11 @@ \begin{itemize} - \item native language elements to state eliminations + \<^item> native language elements to state eliminations - \item symbolic case names + \<^item> symbolic case names - \item method @{method cases} to recover this structure in a + \<^item> method @{method cases} to recover this structure in a sub-proof \end{itemize}