# HG changeset patch # User wenzelm # Date 1444676338 -7200 # Node ID b9a3324e4e62974ef47a9d87c14b712842ba555a # Parent 55e73b352287d2a2c3bb01c00dc09f97937dffc0 more symbols; diff -r 55e73b352287 -r b9a3324e4e62 src/Doc/Implementation/Isar.thy --- a/src/Doc/Implementation/Isar.thy Mon Oct 12 20:42:20 2015 +0200 +++ b/src/Doc/Implementation/Isar.thy Mon Oct 12 20:58:58 2015 +0200 @@ -10,7 +10,7 @@ \begin{enumerate} - \item Proof \emph{commands} define the primary language of + \<^enum> Proof \emph{commands} define the primary language of transactions of the underlying Isar/VM interpreter. Typical examples are @{command "fix"}, @{command "assume"}, @{command "show"}, @{command "proof"}, and @{command "qed"}. @@ -19,7 +19,7 @@ to expressions of structured proof text, such that both the machine and the human reader can give it a meaning as formal reasoning. - \item Proof \emph{methods} define a secondary language of mixed + \<^enum> Proof \emph{methods} define a secondary language of mixed forward-backward refinement steps involving facts and goals. Typical examples are @{method rule}, @{method unfold}, and @{method simp}. @@ -28,7 +28,7 @@ language, say as arguments to @{command "proof"}, @{command "qed"}, or @{command "by"}. - \item \emph{Attributes} define a tertiary language of small + \<^enum> \emph{Attributes} define a tertiary language of small annotations to theorems being defined or referenced. Attributes can modify both the context and the theorem. @@ -191,14 +191,14 @@ \begin{itemize} - \item Goal addressing is further limited either to operate + \<^item> Goal addressing is further limited either to operate uniformly on \emph{all} subgoals, or specifically on the \emph{first} subgoal. Exception: old-style tactic emulations that are embedded into the method space, e.g.\ @{method rule_tac}. - \item A non-trivial method always needs to make progress: an + \<^item> A non-trivial method always needs to make progress: an identical follow-up goal state has to be avoided.\footnote{This enables the user to write method expressions like @{text "meth\<^sup>+"} without looping, while the trivial do-nothing case can be recovered @@ -207,13 +207,14 @@ Exception: trivial stuttering steps, such as ``@{method -}'' or @{method succeed}. - \item Goal facts passed to the method must not be ignored. If there + \<^item> Goal facts passed to the method must not be ignored. If there is no sensible use of facts outside the goal state, facts should be inserted into the subgoals that are addressed by the method. \end{itemize} - \medskip Syntactically, the language of proof methods appears as + \<^medskip> + Syntactically, the language of proof methods appears as arguments to Isar commands like @{command "by"} or @{command apply}. User-space additions are reasonably easy by plugging suitable method-valued parser functions into the framework, using the @@ -223,14 +224,14 @@ following Isar proof schemes. This is the general form of structured proof text: - \medskip + \<^medskip> \begin{tabular}{l} @{command from}~@{text "facts\<^sub>1"}~@{command have}~@{text "props"}~@{command using}~@{text "facts\<^sub>2"} \\ @{command proof}~@{text "(initial_method)"} \\ \quad@{text "body"} \\ @{command qed}~@{text "(terminal_method)"} \\ \end{tabular} - \medskip + \<^medskip> The goal configuration consists of @{text "facts\<^sub>1"} and @{text "facts\<^sub>2"} appended in that order, and various @{text @@ -240,9 +241,10 @@ "terminal_method"} has another chance to finish any remaining subgoals, but it does not see the facts of the initial step. - \medskip This pattern illustrates unstructured proof scripts: + \<^medskip> + This pattern illustrates unstructured proof scripts: - \medskip + \<^medskip> \begin{tabular}{l} @{command have}~@{text "props"} \\ \quad@{command using}~@{text "facts\<^sub>1"}~@{command apply}~@{text "method\<^sub>1"} \\ @@ -250,7 +252,7 @@ \quad@{command using}~@{text "facts\<^sub>3"}~@{command apply}~@{text "method\<^sub>3"} \\ \quad@{command done} \\ \end{tabular} - \medskip + \<^medskip> The @{text "method\<^sub>1"} operates on the original claim while using @{text "facts\<^sub>1"}. Since the @{command apply} command @@ -259,12 +261,13 @@ "method\<^sub>3"} will see again a collection of @{text "facts\<^sub>3"} that has been inserted into the script explicitly. - \medskip Empirically, any Isar proof method can be categorized as + \<^medskip> + Empirically, any Isar proof method can be categorized as follows. \begin{enumerate} - \item \emph{Special method with cases} with named context additions + \<^enum> \emph{Special method with cases} with named context additions associated with the follow-up goal state. Example: @{method "induct"}, which is also a ``raw'' method since it @@ -272,18 +275,18 @@ Pure conjunction (\secref{sec:logic-aux}), instead of separate subgoals (\secref{sec:tactical-goals}). - \item \emph{Structured method} with strong emphasis on facts outside + \<^enum> \emph{Structured method} with strong emphasis on facts outside the goal state. Example: @{method "rule"}, which captures the key ideas behind structured reasoning in Isar in its purest form. - \item \emph{Simple method} with weaker emphasis on facts, which are + \<^enum> \emph{Simple method} with weaker emphasis on facts, which are inserted into subgoals to emulate old-style tactical ``premises''. Examples: @{method "simp"}, @{method "blast"}, @{method "auto"}. - \item \emph{Old-style tactic emulation} with detailed numeric goal + \<^enum> \emph{Old-style tactic emulation} with detailed numeric goal addressing and explicit references to entities of the internal goal state (which are otherwise invisible from proper Isar proof text). The naming convention @{text "foo_tac"} makes this special @@ -353,7 +356,8 @@ text %mlex \See also @{command method_setup} in @{cite "isabelle-isar-ref"} which includes some abstract examples. - \medskip The following toy examples illustrate how the goal facts + \<^medskip> + The following toy examples illustrate how the goal facts and state are passed to proof methods. The predefined proof method called ``@{method tactic}'' wraps ML source of type @{ML_type tactic} (abstracted over @{ML_text facts}). This allows immediate @@ -378,7 +382,9 @@ done end -text \\medskip The next example implements a method that simplifies +text \ + \<^medskip> + The next example implements a method that simplifies the first subgoal by rewrite rules that are given as arguments.\ method_setup my_simp = @@ -404,8 +410,8 @@ states are filtered out explicitly to make the raw tactic conform to standard Isar method behaviour. - \medskip Method @{method my_simp} can be used in Isar proofs like - this: + \<^medskip> + Method @{method my_simp} can be used in Isar proofs like this: \ notepad @@ -435,7 +441,9 @@ have "a = c" and "c = b" by (my_simp_all a b) end -text \\medskip Apart from explicit arguments, common proof methods +text \ + \<^medskip> + Apart from explicit arguments, common proof methods typically work with a default configuration provided by the context. As a shortcut to rule management we use a cheap solution via the @{command named_theorems} command to declare a dynamic fact in the context.\ @@ -458,7 +466,8 @@ "rewrite subgoal by given rules and my_simp rules from the context" text \ - \medskip Method @{method my_simp'} can be used in Isar proofs + \<^medskip> + Method @{method my_simp'} can be used in Isar proofs like this: \ @@ -470,7 +479,9 @@ have "a \ c" by my_simp' end -text \\medskip The @{method my_simp} variants defined above are +text \ + \<^medskip> + The @{method my_simp} variants defined above are ``simple'' methods, i.e.\ the goal facts are merely inserted as goal premises by the @{ML SIMPLE_METHOD'} or @{ML SIMPLE_METHOD} wrapper. For proof methods that are similar to the standard collection of @@ -485,7 +496,8 @@ "by"}~@{text "my_simp"}'' where @{text "foo"} is not used would deceive the reader. - \medskip The technical treatment of rules from the context requires + \<^medskip> + The technical treatment of rules from the context requires further attention. Above we rebuild a fresh @{ML_type simpset} from the arguments and \emph{all} rules retrieved from the context on every invocation of the method. This does not scale to really large diff -r 55e73b352287 -r b9a3324e4e62 src/Doc/Implementation/Logic.thy --- a/src/Doc/Implementation/Logic.thy Mon Oct 12 20:42:20 2015 +0200 +++ b/src/Doc/Implementation/Logic.thy Mon Oct 12 20:58:58 2015 +0200 @@ -36,7 +36,8 @@ The language of types is an uninterpreted order-sorted first-order algebra; types are qualified by ordered type classes. - \medskip A \emph{type class} is an abstract syntactic entity + \<^medskip> + A \emph{type class} is an abstract syntactic entity declared in the theory context. The \emph{subclass relation} @{text "c\<^sub>1 \ c\<^sub>2"} is specified by stating an acyclic generating relation; the transitive closure is maintained @@ -55,7 +56,8 @@ empty one! The intersection of all (finitely many) classes declared in the current theory is the least element wrt.\ the sort ordering. - \medskip A \emph{fixed type variable} is a pair of a basic name + \<^medskip> + A \emph{fixed type variable} is a pair of a basic name (starting with a @{text "'"} character) and a sort constraint, e.g.\ @{text "('a, s)"} which is usually printed as @{text "\\<^sub>s"}. A \emph{schematic type variable} is a pair of an indexname and a @@ -96,7 +98,8 @@ completed, i.e.\ @{text "\ :: (\<^vec>s)c"} entails @{text "\ :: (\<^vec>s)c'"} for any @{text "c' \ c"}. - \medskip The sort algebra is always maintained as \emph{coregular}, + \<^medskip> + The sort algebra is always maintained as \emph{coregular}, which means that type arities are consistent with the subclass relation: for any type constructor @{text "\"}, and classes @{text "c\<^sub>1 \ c\<^sub>2"}, and arities @{text "\ :: @@ -242,7 +245,8 @@ corresponding binders. In contrast, free variables and constants have an explicit name and type in each occurrence. - \medskip A \emph{bound variable} is a natural number @{text "b"}, + \<^medskip> + A \emph{bound variable} is a natural number @{text "b"}, which accounts for the number of intermediate binders between the variable occurrence in the body and its binding position. For example, the de-Bruijn term @{text "\\<^bsub>bool\<^esub>. \\<^bsub>bool\<^esub>. 1 \ 0"} would @@ -263,7 +267,8 @@ e.g.\ @{text "((x, 0), \)"} which is likewise printed as @{text "?x\<^sub>\"}. - \medskip A \emph{constant} is a pair of a basic name and a type, + \<^medskip> + A \emph{constant} is a pair of a basic name and a type, e.g.\ @{text "(c, \)"} which is usually printed as @{text "c\<^sub>\"} here. Constants are declared in the context as polymorphic families @{text "c :: \"}, meaning that all substitution instances @{text @@ -287,7 +292,8 @@ polymorphic constants that the user-level type-checker would reject due to violation of type class restrictions. - \medskip An \emph{atomic term} is either a variable or constant. + \<^medskip> + An \emph{atomic term} is either a variable or constant. The logical category \emph{term} is defined inductively over atomic terms, with abstraction and application as follows: @{text "t = b | x\<^sub>\ | ?x\<^sub>\ | c\<^sub>\ | \\<^sub>\. t | t\<^sub>1 t\<^sub>2"}. Parsing and printing takes care of @@ -320,7 +326,8 @@ name, but different types. In contrast, mixed instances of polymorphic constants occur routinely. - \medskip The \emph{hidden polymorphism} of a term @{text "t :: \"} + \<^medskip> + The \emph{hidden polymorphism} of a term @{text "t :: \"} is the set of type variables occurring in @{text "t"}, but not in its type @{text "\"}. This means that the term implicitly depends on type arguments that are not accounted in the result type, i.e.\ @@ -328,14 +335,16 @@ @{text "t\' :: \"} with the same type. This slightly pathological situation notoriously demands additional care. - \medskip A \emph{term abbreviation} is a syntactic definition @{text + \<^medskip> + A \emph{term abbreviation} is a syntactic definition @{text "c\<^sub>\ \ t"} of a closed term @{text "t"} of type @{text "\"}, without any hidden polymorphism. A term abbreviation looks like a constant in the syntax, but is expanded before entering the logical core. Abbreviations are usually reverted when printing terms, using @{text "t \ c\<^sub>\"} as rules for higher-order rewriting. - \medskip Canonical operations on @{text "\"}-terms include @{text + \<^medskip> + Canonical operations on @{text "\"}-terms include @{text "\\\"}-conversion: @{text "\"}-conversion refers to capture-free renaming of bound variables; @{text "\"}-conversion contracts an abstraction applied to an argument term, substituting the argument @@ -569,7 +578,8 @@ the PTS framework @{cite "Barendregt-Geuvers:2001"}, where hypotheses @{text "x : A"} are treated uniformly for propositions and types.} - \medskip The axiomatization of a theory is implicitly closed by + \<^medskip> + The axiomatization of a theory is implicitly closed by forming all instances of type and term variables: @{text "\ A\"} holds for any substitution instance of an axiom @{text "\ A"}. By pushing substitutions through derivations @@ -602,7 +612,8 @@ correct, but @{text "\\ \ \"} does not necessarily hold: the result belongs to a different proof context. - \medskip An \emph{oracle} is a function that produces axioms on the + \<^medskip> + An \emph{oracle} is a function that produces axioms on the fly. Logically, this is an instance of the @{text "axiom"} rule (\figref{fig:prim-rules}), but there is an operational difference. The system always records oracle invocations within derivations of @@ -1036,13 +1047,13 @@ Formulae} in the literature @{cite "Miller:1991"}. Here we give an inductive characterization as follows: - \medskip + \<^medskip> \begin{tabular}{ll} @{text "\<^bold>x"} & set of variables \\ @{text "\<^bold>A"} & set of atomic propositions \\ @{text "\<^bold>H = \\<^bold>x\<^sup>*. \<^bold>H\<^sup>* \ \<^bold>A"} & set of Hereditary Harrop Formulas \\ \end{tabular} - \medskip + \<^medskip> Thus we essentially impose nesting levels on propositions formed from @{text "\"} and @{text "\"}. At each level there is a prefix @@ -1054,17 +1065,18 @@ already marks the limit of rule complexity that is usually seen in practice. - \medskip Regular user-level inferences in Isabelle/Pure always + \<^medskip> + Regular user-level inferences in Isabelle/Pure always maintain the following canonical form of results: \begin{itemize} - \item Normalization by @{text "(A \ (\x. B x)) \ (\x. A \ B x)"}, + \<^item> Normalization by @{text "(A \ (\x. B x)) \ (\x. A \ B x)"}, which is a theorem of Pure, means that quantifiers are pushed in front of implication at each level of nesting. The normal form is a Hereditary Harrop Formula. - \item The outermost prefix of parameters is represented via + \<^item> The outermost prefix of parameters is represented via schematic variables: instead of @{text "\\<^vec>x. \<^vec>H \<^vec>x \ A \<^vec>x"} we have @{text "\<^vec>H ?\<^vec>x \ A ?\<^vec>x"}. Note that this representation looses information about the order of @@ -1225,7 +1237,8 @@ @{cite "Barendregt-Geuvers:2001"}, if some fine points like schematic polymorphism and type classes are ignored. - \medskip\emph{Proof abstractions} of the form @{text "\<^bold>\x :: \. prf"} + \<^medskip> + \emph{Proof abstractions} of the form @{text "\<^bold>\x :: \. prf"} or @{text "\<^bold>\p : A. prf"} correspond to introduction of @{text "\"}/@{text "\"}, and \emph{proof applications} of the form @{text "p \ t"} or @{text "p \ q"} correspond to elimination of @{text @@ -1233,7 +1246,8 @@ "A"}, and terms @{text "t"} might be suppressed and reconstructed from the overall proof term. - \medskip Various atomic proofs indicate special situations within + \<^medskip> + Various atomic proofs indicate special situations within the proof construction as follows. A \emph{bound proof variable} is a natural number @{text "b"} that @@ -1326,7 +1340,8 @@ using @{text "p \ TYPE(type)"} (they must appear before any other term argument of a theorem or axiom, but may be omitted altogether). - \medskip There are separate read and print operations for proof + \<^medskip> + There are separate read and print operations for proof terms, in order to avoid conflicts with the regular term language. \ @@ -1436,7 +1451,8 @@ recursively explores the graph of the proofs of all theorems being used here. - \medskip Alternatively, we may produce a proof term manually, and + \<^medskip> + Alternatively, we may produce a proof term manually, and turn it into a theorem as follows:\ ML_val \ @@ -1454,7 +1470,9 @@ |> Drule.export_without_context; \ -text \\medskip See also @{file "~~/src/HOL/Proofs/ex/XML_Data.thy"} +text \ + \<^medskip> + See also @{file "~~/src/HOL/Proofs/ex/XML_Data.thy"} for further examples, with export and import of proof terms via XML/ML data representation. \ diff -r 55e73b352287 -r b9a3324e4e62 src/Doc/Implementation/ML.thy --- a/src/Doc/Implementation/ML.thy Mon Oct 12 20:42:20 2015 +0200 +++ b/src/Doc/Implementation/ML.thy Mon Oct 12 20:58:58 2015 +0200 @@ -95,7 +95,8 @@ section headings that are adjacent to plain text, but not other headings as in the example above. - \medskip The precise wording of the prose text given in these + \<^medskip> + The precise wording of the prose text given in these headings is chosen carefully to introduce the main theme of the subsequent formal ML text. \ @@ -111,14 +112,14 @@ variants concerning upper or lower case letters, which are used for certain ML categories as follows: - \medskip + \<^medskip> \begin{tabular}{lll} variant & example & ML categories \\\hline lower-case & @{ML_text foo_bar} & values, types, record fields \\ capitalized & @{ML_text Foo_Bar} & datatype constructors, structures, functors \\ upper-case & @{ML_text FOO_BAR} & special values, exception constructors, signatures \\ \end{tabular} - \medskip + \<^medskip> For historical reasons, many capitalized names omit underscores, e.g.\ old-style @{ML_text FooBar} instead of @{ML_text Foo_Bar}. @@ -188,15 +189,15 @@ \begin{itemize} - \item A function that maps @{ML_text foo} to @{ML_text bar} is + \<^item> A function that maps @{ML_text foo} to @{ML_text bar} is called @{ML_text foo_to_bar} or @{ML_text bar_of_foo} (never @{ML_text foo2bar}, nor @{ML_text bar_from_foo}, nor @{ML_text bar_for_foo}, nor @{ML_text bar4foo}). - \item The name component @{ML_text legacy} means that the operation + \<^item> The name component @{ML_text legacy} means that the operation is about to be discontinued soon. - \item The name component @{ML_text global} means that this works + \<^item> The name component @{ML_text global} means that this works with the background theory instead of the regular local context (\secref{sec:context}), sometimes for historical reasons, sometimes due a genuine lack of locality of the concept involved, sometimes as @@ -205,21 +206,21 @@ application should be migrated to use it with a proper local context. - \item Variables of the main context types of the Isabelle/Isar + \<^item> Variables of the main context types of the Isabelle/Isar framework (\secref{sec:context} and \chref{ch:local-theory}) have firm naming conventions as follows: \begin{itemize} - \item theories are called @{ML_text thy}, rarely @{ML_text theory} + \<^item> theories are called @{ML_text thy}, rarely @{ML_text theory} (never @{ML_text thry}) - \item proof contexts are called @{ML_text ctxt}, rarely @{ML_text + \<^item> proof contexts are called @{ML_text ctxt}, rarely @{ML_text context} (never @{ML_text ctx}) - \item generic contexts are called @{ML_text context} - - \item local theories are called @{ML_text lthy}, except for local + \<^item> generic contexts are called @{ML_text context} + + \<^item> local theories are called @{ML_text lthy}, except for local theories that are treated as proof context (which is a semantic super-type) @@ -231,26 +232,26 @@ This allows to emphasize their data flow via plain regular expressions in the text editor. - \item The main logical entities (\secref{ch:logic}) have established + \<^item> The main logical entities (\secref{ch:logic}) have established naming convention as follows: \begin{itemize} - \item sorts are called @{ML_text S} - - \item types are called @{ML_text T}, @{ML_text U}, or @{ML_text + \<^item> sorts are called @{ML_text S} + + \<^item> types are called @{ML_text T}, @{ML_text U}, or @{ML_text ty} (never @{ML_text t}) - \item terms are called @{ML_text t}, @{ML_text u}, or @{ML_text + \<^item> terms are called @{ML_text t}, @{ML_text u}, or @{ML_text tm} (never @{ML_text trm}) - \item certified types are called @{ML_text cT}, rarely @{ML_text + \<^item> certified types are called @{ML_text cT}, rarely @{ML_text T}, with variants as for types - \item certified terms are called @{ML_text ct}, rarely @{ML_text + \<^item> certified terms are called @{ML_text ct}, rarely @{ML_text t}, with variants as for terms (never @{ML_text ctrm}) - \item theorems are called @{ML_text th}, or @{ML_text thm} + \<^item> theorems are called @{ML_text th}, or @{ML_text thm} \end{itemize} @@ -379,7 +380,8 @@ to changes of the initial text (working against \emph{maintainability}) etc. - \medskip For similar reasons, any kind of two-dimensional or tabular + \<^medskip> + For similar reasons, any kind of two-dimensional or tabular layouts, ASCII-art with lines or boxes of asterisks etc.\ should be avoided. @@ -447,12 +449,13 @@ but help to analyse the nesting based on character matching in the text editor. - \medskip There are two main exceptions to the overall principle of + \<^medskip> + There are two main exceptions to the overall principle of compositionality in the layout of complex expressions. \begin{enumerate} - \item @{ML_text "if"} expressions are iterated as if ML had multi-branch + \<^enum> @{ML_text "if"} expressions are iterated as if ML had multi-branch conditionals, e.g. \begin{verbatim} @@ -463,7 +466,7 @@ else e3 \end{verbatim} - \item @{ML_text fn} abstractions are often layed-out as if they + \<^enum> @{ML_text fn} abstractions are often layed-out as if they would lack any structure by themselves. This traditional form is motivated by the possibility to shift function arguments back and forth wrt.\ additional combinators. Example: @@ -515,7 +518,8 @@ ... end \end{verbatim} - \medskip In general the source layout is meant to emphasize the + \<^medskip> + In general the source layout is meant to emphasize the structure of complex language expressions, not to pretend that SML had a completely different syntax (say that of Haskell, Scala, Java). \ @@ -584,10 +588,11 @@ compilation within independent nodes of the implicit theory development graph.} - \medskip The next example shows how to embed ML into Isar proofs, using + \<^medskip> + The next example shows how to embed ML into Isar proofs, using @{command_ref "ML_prf"} instead of @{command_ref "ML"}. As illustrated below, the effect on the ML environment is local to the whole proof body, - but ignoring the block structure. \ + but ignoring the block structure.\ notepad begin @@ -603,7 +608,8 @@ manipulate corresponding entities, e.g.\ export a fact from a block context. - \medskip Two further ML commands are useful in certain situations: + \<^medskip> + Two further ML commands are useful in certain situations: @{command_ref ML_val} and @{command_ref ML_command} are \emph{diagnostic} in the sense that there is no effect on the underlying environment, and can thus be used anywhere. The examples below produce long strings of digits by @@ -681,7 +687,8 @@ Here @{syntax nameref} and @{syntax args} are outer syntax categories, as defined in @{cite "isabelle-isar-ref"}. - \medskip A regular antiquotation @{text "@{name args}"} processes + \<^medskip> + A regular antiquotation @{text "@{name args}"} processes its arguments by the usual means of the Isar source language, and produces corresponding ML source text, either as literal \emph{inline} text (e.g.\ @{text "@{term t}"}) or abstract @@ -781,7 +788,8 @@ \"} or @{text "C: (\ \ \ \ \) \ (\ \ \ \ \)"} (the latter is not present in the Isabelle/ML library). - \medskip The main idea is that arguments that vary less are moved + \<^medskip> + The main idea is that arguments that vary less are moved further to the left than those that vary more. Two particularly important categories of functions are \emph{selectors} and \emph{updates}. @@ -830,27 +838,28 @@ improved by introducing \emph{forward} versions of application and composition as follows: - \medskip + \<^medskip> \begin{tabular}{lll} @{text "x |> f"} & @{text "\"} & @{text "f x"} \\ @{text "(f #> g) x"} & @{text "\"} & @{text "x |> f |> g"} \\ \end{tabular} - \medskip + \<^medskip> This enables to write conveniently @{text "x |> f\<^sub>1 |> \ |> f\<^sub>n"} or @{text "f\<^sub>1 #> \ #> f\<^sub>n"} for its functional abstraction over @{text "x"}. - \medskip There is an additional set of combinators to accommodate + \<^medskip> + There is an additional set of combinators to accommodate multiple results (via pairs) that are passed on as multiple arguments (via currying). - \medskip + \<^medskip> \begin{tabular}{lll} @{text "(x, y) |-> f"} & @{text "\"} & @{text "f x y"} \\ @{text "(f #-> g) x"} & @{text "\"} & @{text "x |> f |-> g"} \\ \end{tabular} - \medskip + \<^medskip> \ text %mlref \ @@ -944,7 +953,8 @@ memory (``deforestation''), but it requires some practice to read and write fluently. - \medskip The next example elaborates the idea of canonical + \<^medskip> + The next example elaborates the idea of canonical iteration, demonstrating fast accumulation of tree content using a text buffer. \ @@ -1094,7 +1104,8 @@ \ text \ - \medskip An alternative is to make a paragraph of freely-floating words as + \<^medskip> + An alternative is to make a paragraph of freely-floating words as follows. \ @@ -1154,7 +1165,8 @@ ML runtime system attaches detailed source position stemming from the corresponding @{ML_text raise} keyword. - \medskip User modules can always introduce their own custom + \<^medskip> + User modules can always introduce their own custom exceptions locally, e.g.\ to organize internal failures robustly without overlapping with existing exceptions. Exceptions that are exposed in module signatures require extra care, though, and should @@ -1266,23 +1278,23 @@ \begin{enumerate} - \item a single ASCII character ``@{text "c"}'', for example + \<^enum> a single ASCII character ``@{text "c"}'', for example ``@{verbatim a}'', - \item a codepoint according to UTF-8 (non-ASCII byte sequence), - - \item a regular symbol ``@{verbatim \\\}@{verbatim "<"}@{text + \<^enum> a codepoint according to UTF-8 (non-ASCII byte sequence), + + \<^enum> a regular symbol ``@{verbatim \\\}@{verbatim "<"}@{text "ident"}@{verbatim ">"}'', for example ``@{verbatim "\"}'', - \item a control symbol ``@{verbatim \\\}@{verbatim "<^"}@{text + \<^enum> a control symbol ``@{verbatim \\\}@{verbatim "<^"}@{text "ident"}@{verbatim ">"}'', for example ``@{verbatim "\<^bold>"}'', - \item a raw symbol ``@{verbatim \\\}@{verbatim "<^raw:"}@{text + \<^enum> a raw symbol ``@{verbatim \\\}@{verbatim "<^raw:"}@{text text}@{verbatim ">"}'' where @{text text} consists of printable characters excluding ``@{verbatim "."}'' and ``@{verbatim ">"}'', for example ``@{verbatim "\<^raw:$\sum_{i = 1}^n$>"}'', - \item a numbered raw control symbol ``@{verbatim \\\}@{verbatim + \<^enum> a numbered raw control symbol ``@{verbatim \\\}@{verbatim "<^raw"}@{text n}@{verbatim ">"}, where @{text n} consists of digits, for example ``@{verbatim "\<^raw42>"}''. @@ -1303,7 +1315,8 @@ mathematical symbols, but within the core Isabelle/ML world there is no link to the standard collection of Isabelle regular symbols. - \medskip Output of Isabelle symbols depends on the print mode. For example, + \<^medskip> + Output of Isabelle symbols depends on the print mode. For example, the standard {\LaTeX} setup of the Isabelle document preparation system would present ``@{verbatim "\"}'' as @{text "\"}, and ``@{verbatim "\<^bold>\"}'' as @{text "\<^bold>\"}. On-screen rendering usually works by mapping a @@ -1415,10 +1428,10 @@ \begin{enumerate} - \item sequence of Isabelle symbols (see also \secref{sec:symbols}), + \<^enum> sequence of Isabelle symbols (see also \secref{sec:symbols}), with @{ML Symbol.explode} as key operation; - \item XML tree structure via YXML (see also @{cite "isabelle-system"}), + \<^enum> XML tree structure via YXML (see also @{cite "isabelle-system"}), with @{ML YXML.parse_body} as key operation. \end{enumerate} @@ -1710,7 +1723,8 @@ speedup-factor of 3.5 on 4 cores and 6.5 on 8 cores can be expected @{cite "Wenzel:2013:ITP"}. - \medskip ML threads lack the memory protection of separate + \<^medskip> + ML threads lack the memory protection of separate processes, and operate concurrently on shared heap memory. This has the advantage that results of independent computations are directly available to other threads: abstract values can be passed without @@ -1750,15 +1764,15 @@ \begin{itemize} - \item Global references (or arrays), i.e.\ mutable memory cells that + \<^item> Global references (or arrays), i.e.\ mutable memory cells that persist over several invocations of associated operations.\footnote{This is independent of the visibility of such mutable values in the toplevel scope.} - \item Global state of the running Isabelle/ML process, i.e.\ raw I/O + \<^item> Global state of the running Isabelle/ML process, i.e.\ raw I/O channels, environment variables, current working directory. - \item Writable resources in the file-system that are shared among + \<^item> Writable resources in the file-system that are shared among different threads or external processes. \end{itemize} @@ -1771,7 +1785,7 @@ \begin{itemize} - \item Avoid global references altogether. Isabelle/Isar maintains a + \<^item> Avoid global references altogether. Isabelle/Isar maintains a uniform context that incorporates arbitrary data declared by user programs (\secref{sec:context-data}). This context is passed as plain value and user tools can get/map their own data in a purely @@ -1779,7 +1793,7 @@ (\secref{sec:config-options}) provide simple drop-in replacements for historic reference variables. - \item Keep components with local state information re-entrant. + \<^item> Keep components with local state information re-entrant. Instead of poking initial values into (private) global references, a new state record can be created on each invocation, and passed through any auxiliary functions of the component. The state record @@ -1787,7 +1801,7 @@ synchronization, as long as each invocation gets its own copy and the tool itself is single-threaded. - \item Avoid raw output on @{text "stdout"} or @{text "stderr"}. The + \<^item> Avoid raw output on @{text "stdout"} or @{text "stderr"}. The Poly/ML library is thread-safe for each individual output operation, but the ordering of parallel invocations is arbitrary. This means raw output will appear on some system console with unpredictable @@ -1801,10 +1815,10 @@ only happen when commands use parallelism internally (and only at message boundaries). - \item Treat environment variables and the current working directory + \<^item> Treat environment variables and the current working directory of the running process as read-only. - \item Restrict writing to the file-system to unique temporary files. + \<^item> Restrict writing to the file-system to unique temporary files. Isabelle already provides a temporary directory that is unique for the running process, and there is a centralized source of unique serial numbers in Isabelle/ML. Thus temporary files that are passed @@ -1913,7 +1927,9 @@ @{assert} (a <> b); \ -text \\medskip See @{file "~~/src/Pure/Concurrent/mailbox.ML"} how +text \ + \<^medskip> + See @{file "~~/src/Pure/Concurrent/mailbox.ML"} how to implement a mailbox as synchronized variable over a purely functional list.\ @@ -1933,7 +1949,8 @@ evaluation via futures, asynchronous evaluation via promises, evaluation with time limit etc. - \medskip An \emph{unevaluated expression} is represented either as + \<^medskip> + An \emph{unevaluated expression} is represented either as unit abstraction @{verbatim "fn () => a"} of type @{verbatim "unit -> 'a"} or as regular function @{verbatim "fn a => b"} of type @{verbatim "'a -> 'b"}. Both forms @@ -1948,7 +1965,8 @@ be cascaded to modify a given function, before it is ultimately applied to some argument. - \medskip \emph{Reified results} make the disjoint sum of regular + \<^medskip> + \emph{Reified results} make the disjoint sum of regular values versions exceptional situations explicit as ML datatype: @{text "'a result = Res of 'a | Exn of exn"}. This is typically used for administrative purposes, to store the overall outcome of an @@ -2158,7 +2176,8 @@ threads that get activated in certain explicit wait conditions, after a timeout. - \medskip Each future task belongs to some \emph{task group}, which + \<^medskip> + Each future task belongs to some \emph{task group}, which represents the hierarchic structure of related tasks, together with the exception status a that point. By default, the task group of a newly created future is a new sub-group of the presently running one, but it is also @@ -2173,7 +2192,8 @@ tasks that lack regular result information, will pick up parallel exceptions from the cumulative group status. - \medskip A \emph{passive future} or \emph{promise} is a future with slightly + \<^medskip> + A \emph{passive future} or \emph{promise} is a future with slightly different evaluation policies: there is only a single-assignment variable and some expression to evaluate for the \emph{failed} case (e.g.\ to clean up resources when canceled). A regular result is produced by external means, @@ -2217,19 +2237,19 @@ \begin{itemize} - \item @{text "name : string"} (default @{ML "\"\""}) specifies a common name + \<^item> @{text "name : string"} (default @{ML "\"\""}) specifies a common name for the tasks of the forked futures, which serves diagnostic purposes. - \item @{text "group : Future.group option"} (default @{ML NONE}) specifies + \<^item> @{text "group : Future.group option"} (default @{ML NONE}) specifies an optional task group for the forked futures. @{ML NONE} means that a new sub-group of the current worker-thread task context is created. If this is not a worker thread, the group will be a new root in the group hierarchy. - \item @{text "deps : Future.task list"} (default @{ML "[]"}) specifies + \<^item> @{text "deps : Future.task list"} (default @{ML "[]"}) specifies dependencies on other future tasks, i.e.\ the adjacency relation in the global task queue. Dependencies on already finished tasks are ignored. - \item @{text "pri : int"} (default @{ML 0}) specifies a priority within the + \<^item> @{text "pri : int"} (default @{ML 0}) specifies a priority within the task queue. Typically there is only little deviation from the default priority @{ML 0}. @@ -2242,7 +2262,7 @@ priority tasks that are queued later need to wait until this (or another) worker thread becomes free again. - \item @{text "interrupts : bool"} (default @{ML true}) tells whether the + \<^item> @{text "interrupts : bool"} (default @{ML true}) tells whether the worker thread that processes the corresponding task is initially put into interruptible state. This state may change again while running, by modifying the thread attributes. diff -r 55e73b352287 -r b9a3324e4e62 src/Doc/Implementation/Prelim.thy --- a/src/Doc/Implementation/Prelim.thy Mon Oct 12 20:42:20 2015 +0200 +++ b/src/Doc/Implementation/Prelim.thy Mon Oct 12 20:58:58 2015 +0200 @@ -22,17 +22,18 @@ @{text "\ \ \"} is strictly limited to Simple Type Theory (with fixed type variables in the assumptions). - \medskip Contexts and derivations are linked by the following key + \<^medskip> + Contexts and derivations are linked by the following key principles: \begin{itemize} - \item Transfer: monotonicity of derivations admits results to be + \<^item> Transfer: monotonicity of derivations admits results to be transferred into a \emph{larger} context, i.e.\ @{text "\ \\<^sub>\ \"} implies @{text "\' \\<^sub>\\<^sub>' \"} for contexts @{text "\' \ \"} and @{text "\' \ \"}. - \item Export: discharge of hypotheses admits results to be exported + \<^item> Export: discharge of hypotheses admits results to be exported into a \emph{smaller} context, i.e.\ @{text "\' \\<^sub>\ \"} implies @{text "\ \\<^sub>\ \ \ \"} where @{text "\' \ \"} and @{text "\ = \' - \"}. Note that @{text "\"} remains unchanged here, @@ -40,7 +41,8 @@ \end{itemize} - \medskip By modeling the main characteristics of the primitive + \<^medskip> + By modeling the main characteristics of the primitive @{text "\"} and @{text "\"} above, and abstracting over any particular logical content, we arrive at the fundamental notions of \emph{theory context} and \emph{proof context} in Isabelle/Isar. @@ -60,7 +62,8 @@ standard proof steps implicitly (cf.\ the @{text "rule"} method @{cite "isabelle-isar-ref"}). - \medskip Thus Isabelle/Isar is able to bring forth more and more + \<^medskip> + Thus Isabelle/Isar is able to bring forth more and more concepts successively. In particular, an object-logic like Isabelle/HOL continues the Isabelle/Pure setup by adding specific components for automated reasoning (classical reasoner, tableau @@ -85,7 +88,8 @@ nameless incremental updates, until the final @{text "end"} operation is performed. - \medskip The example in \figref{fig:ex-theory} below shows a theory + \<^medskip> + The example in \figref{fig:ex-theory} below shows a theory graph derived from @{text "Pure"}, with theory @{text "Length"} importing @{text "Nat"} and @{text "List"}. The body of @{text "Length"} consists of a sequence of updates, resulting in locally a @@ -109,7 +113,8 @@ \end{center} \end{figure} - \medskip Derived formal entities may retain a reference to the + \<^medskip> + Derived formal entities may retain a reference to the background theory in order to indicate the formal context from which they were produced. This provides an immutable certificate of the background theory.\ @@ -303,14 +308,14 @@ \paragraph{Theory data} declarations need to implement the following ML signature: - \medskip + \<^medskip> \begin{tabular}{ll} @{text "\ T"} & representing type \\ @{text "\ empty: T"} & empty default value \\ @{text "\ extend: T \ T"} & re-initialize on import \\ @{text "\ merge: T \ T \ T"} & join on import \\ \end{tabular} - \medskip + \<^medskip> The @{text "empty"} value acts as initial default for \emph{any} theory that does not declare actual data content; @{text "extend"} @@ -329,12 +334,12 @@ \paragraph{Proof context data} declarations need to implement the following ML signature: - \medskip + \<^medskip> \begin{tabular}{ll} @{text "\ T"} & representing type \\ @{text "\ init: theory \ T"} & produce initial value \\ \end{tabular} - \medskip + \<^medskip> The @{text "init"} operation is supposed to produce a pure value from the given background theory and should be somehow @@ -352,16 +357,17 @@ predefined to select the current data value from the background theory. - \bigskip Any of the above data declarations over type @{text "T"} + \<^bigskip> + Any of the above data declarations over type @{text "T"} result in an ML structure with the following signature: - \medskip + \<^medskip> \begin{tabular}{ll} @{text "get: context \ T"} \\ @{text "put: T \ context \ context"} \\ @{text "map: (T \ T) \ context \ context"} \\ \end{tabular} - \medskip + \<^medskip> These other operations provide exclusive access for the particular kind of context (theory, proof, or generic context). This interface @@ -448,13 +454,14 @@ exponential blowup. Plain list append etc.\ must never be used for theory data merges! - \medskip Our intended invariant is achieved as follows: + \<^medskip> + Our intended invariant is achieved as follows: \begin{enumerate} - \item @{ML Wellformed_Terms.add} only admits terms that have passed + \<^enum> @{ML Wellformed_Terms.add} only admits terms that have passed the @{ML Sign.cert_term} check of the given theory at that point. - \item Wellformedness in the sense of @{ML Sign.cert_term} is + \<^enum> Wellformedness in the sense of @{ML Sign.cert_term} is monotonic wrt.\ the sub-theory relation. So our data can move upwards in the hierarchy (via extension or merges), and maintain wellformedness without further checks. @@ -610,17 +617,18 @@ e.g.\ the string ``@{verbatim \}'' encodes as a single symbol (\secref{sec:symbols}). - \medskip Subsequently, we shall introduce specific categories of + \<^medskip> + Subsequently, we shall introduce specific categories of names. Roughly speaking these correspond to logical entities as follows: \begin{itemize} - \item Basic names (\secref{sec:basic-name}): free and bound + \<^item> Basic names (\secref{sec:basic-name}): free and bound variables. - \item Indexed names (\secref{sec:indexname}): schematic variables. + \<^item> Indexed names (\secref{sec:indexname}): schematic variables. - \item Long names (\secref{sec:long-name}): constants of any kind + \<^item> Long names (\secref{sec:long-name}): constants of any kind (type constructors, term constants, other concepts defined in user space). Such entities are typically managed via name spaces (\secref{sec:name-space}). @@ -648,7 +656,8 @@ as internal, which prevents mysterious names like @{text "xaa"} to appear in human-readable text. - \medskip Manipulating binding scopes often requires on-the-fly + \<^medskip> + Manipulating binding scopes often requires on-the-fly renamings. A \emph{name context} contains a collection of already used names. The @{text "declare"} operation adds names to the context. @@ -725,8 +734,9 @@ @{assert} (list2 = ["x", "xa", "a", "aa", "'a", "'aa"]); \ -text \\medskip The same works relatively to the formal context as - follows.\ +text \ + \<^medskip> + The same works relatively to the formal context as follows.\ experiment fixes a b c :: 'a begin @@ -761,16 +771,17 @@ indexed names: then @{text "(x, -1)"} is used to encode the basic name @{text "x"}. - \medskip Isabelle syntax observes the following rules for + \<^medskip> + Isabelle syntax observes the following rules for representing an indexname @{text "(x, i)"} as a packed string: \begin{itemize} - \item @{text "?x"} if @{text "x"} does not end with a digit and @{text "i = 0"}, + \<^item> @{text "?x"} if @{text "x"} does not end with a digit and @{text "i = 0"}, - \item @{text "?xi"} if @{text "x"} does not end with a digit, + \<^item> @{text "?xi"} if @{text "x"} does not end with a digit, - \item @{text "?x.i"} otherwise. + \<^item> @{text "?x.i"} otherwise. \end{itemize} @@ -861,13 +872,15 @@ "declare"} operation augments a name space according to the accesses determined by a given binding, and a naming policy from the context. - \medskip A @{text "binding"} specifies details about the prospective + \<^medskip> + A @{text "binding"} specifies details about the prospective long name of a newly introduced formal entity. It consists of a base name, prefixes for qualification (separate ones for system infrastructure and user-space mechanisms), a slot for the original source position, and some additional flags. - \medskip A @{text "naming"} provides some additional details for + \<^medskip> + A @{text "naming"} provides some additional details for producing a long name from a binding. Normally, the naming is implicit in the theory or proof context. The @{text "full"} operation (and its variants for different context types) produces a @@ -875,12 +888,13 @@ main equation of this ``chemical reaction'' when binding new entities in a context is as follows: - \medskip + \<^medskip> \begin{tabular}{l} @{text "binding + naming \ long name + name space accesses"} \end{tabular} - \bigskip As a general principle, there is a separate name space for + \<^bigskip> + As a general principle, there is a separate name space for each kind of formal entity, e.g.\ fact, logical constant, type constructor, type class. It is usually clear from the occurrence in concrete syntax (or from the scope) which kind of entity a name @@ -897,7 +911,7 @@ qualification. This leads to the following conventions for derived names: - \medskip + \<^medskip> \begin{tabular}{ll} logical entity & fact name \\\hline constant @{text "c"} & @{text "c.intro"} \\ @@ -1041,8 +1055,9 @@ ML_val \Binding.pos_of @{binding here}\ -text \\medskip That position can be also printed in a message as - follows:\ +text \ + \<^medskip> + That position can be also printed in a message as follows:\ ML_command \writeln @@ -1053,7 +1068,8 @@ additional information for feedback given to the user (error messages etc.). - \medskip The following example refers to its source position + \<^medskip> + The following example refers to its source position directly, which is occasionally useful for experimentation and diagnostic purposes:\ diff -r 55e73b352287 -r b9a3324e4e62 src/Doc/Implementation/Proof.thy --- a/src/Doc/Implementation/Proof.thy Mon Oct 12 20:42:20 2015 +0200 +++ b/src/Doc/Implementation/Proof.thy Mon Oct 12 20:58:58 2015 +0200 @@ -30,7 +30,8 @@ @{text "\ B(?\)"} represents the idea of ``@{text "\ \\. B(\)"}'' without demanding a truly polymorphic framework. - \medskip Additional care is required to treat type variables in a + \<^medskip> + Additional care is required to treat type variables in a way that facilitates type-inference. In principle, term variables depend on type variables, which means that type variables would have to be declared first. For example, a raw type-theoretic framework @@ -237,7 +238,8 @@ A\<^sub>n \ B"} where @{text "A\<^sub>1, \, A\<^sub>n"} needs to be covered by the assumptions of the current context. - \medskip The @{text "add_assms"} operation augments the context by + \<^medskip> + The @{text "add_assms"} operation augments the context by local assumptions, which are parameterized by an arbitrary @{text "export"} rule (see below). @@ -249,7 +251,8 @@ separate flag to indicate a goal context, where the result is meant to refine an enclosing sub-goal of a structured proof state. - \medskip The most basic export rule discharges assumptions directly + \<^medskip> + The most basic export rule discharges assumptions directly by means of the @{text "\"} introduction rule: \[ \infer[(@{text "\\intro"})]{@{text "\ - A \ A \ B"}}{@{text "\ \ B"}} @@ -262,7 +265,8 @@ \infer[(@{text "#\\intro"})]{@{text "\ - A \ #A \ B"}}{@{text "\ \ B"}} \] - \medskip Alternative versions of assumptions may perform arbitrary + \<^medskip> + Alternative versions of assumptions may perform arbitrary transformations on export, as long as the corresponding portion of hypotheses is removed from the given facts. For example, a local definition works by fixing @{text "x"} and assuming @{text "x \ t"}, @@ -354,7 +358,8 @@ references to free variables or assumptions not present in the proof context. - \medskip The @{text "SUBPROOF"} combinator allows to structure a + \<^medskip> + The @{text "SUBPROOF"} combinator allows to structure a tactical proof recursively by decomposing a selected sub-goal: @{text "(\x. A(x) \ B(x)) \ \"} is turned into @{text "B(x) \ \"} after fixing @{text "x"} and assuming @{text "A(x)"}. This means @@ -482,7 +487,9 @@ sorry end -text \\medskip The next example demonstrates forward-elimination in +text \ + \<^medskip> + The next example demonstrates forward-elimination in a local context, using @{ML Obtain.result}.\ notepad diff -r 55e73b352287 -r b9a3324e4e62 src/Doc/Implementation/Syntax.thy --- a/src/Doc/Implementation/Syntax.thy Mon Oct 12 20:42:20 2015 +0200 +++ b/src/Doc/Implementation/Syntax.thy Mon Oct 12 20:58:58 2015 +0200 @@ -25,7 +25,8 @@ users. Beginners often stumble over unexpectedly general types inferred by the system.} - \medskip The main inner syntax operations are \emph{read} for + \<^medskip> + The main inner syntax operations are \emph{read} for parsing together with type-checking, and \emph{pretty} for formatted output. See also \secref{sec:read-print}. @@ -37,9 +38,9 @@ \begin{itemize} - \item @{text "read = parse; check"} + \<^item> @{text "read = parse; check"} - \item @{text "pretty = uncheck; unparse"} + \<^item> @{text "pretty = uncheck; unparse"} \end{itemize} @@ -49,7 +50,8 @@ "check"}. Note that the formal status of bound variables, versus free variables, versus constants must not be changed between these phases. - \medskip In general, @{text check} and @{text uncheck} operate + \<^medskip> + In general, @{text check} and @{text uncheck} operate simultaneously on a list of terms. This is particular important for type-checking, to reconstruct types for several terms of the same context and scope. In contrast, @{text parse} and @{text unparse} operate separately @@ -131,7 +133,8 @@ @{ML Syntax.read_term}, @{ML Syntax.read_prop}, and @{ML Syntax.string_of_term} are the most important operations in practice. - \medskip Note that the string values that are passed in and out are + \<^medskip> + Note that the string values that are passed in and out are annotated by the system, to carry further markup that is relevant for the Prover IDE @{cite "isabelle-jedit"}. User code should neither compose its own input strings, nor try to analyze the output strings. Conceptually this @@ -223,7 +226,8 @@ contracted during the @{text "uncheck"} phase, without affecting the type-assignment of the given terms. - \medskip The precise meaning of type checking depends on the context --- + \<^medskip> + The precise meaning of type checking depends on the context --- additional check/uncheck modules might be defined in user space. For example, the @{command class} command defines a context where diff -r 55e73b352287 -r b9a3324e4e62 src/Doc/Implementation/Tactic.thy --- a/src/Doc/Implementation/Tactic.thy Mon Oct 12 20:42:20 2015 +0200 +++ b/src/Doc/Implementation/Tactic.thy Mon Oct 12 20:58:58 2015 +0200 @@ -41,7 +41,8 @@ "#C"} here. This ensures that the decomposition into subgoals and main conclusion is well-defined for arbitrarily structured claims. - \medskip Basic goal management is performed via the following + \<^medskip> + Basic goal management is performed via the following Isabelle/Pure rules: \[ @@ -49,7 +50,8 @@ \infer[@{text "(finish)"}]{@{text "C"}}{@{text "#C"}} \] - \medskip The following low-level variants admit general reasoning + \<^medskip> + The following low-level variants admit general reasoning with protected propositions: \[ @@ -115,7 +117,8 @@ combinators for building proof tools that involve search systematically, see also \secref{sec:tacticals}. - \medskip As explained before, a goal state essentially consists of a + \<^medskip> + As explained before, a goal state essentially consists of a list of subgoals that imply the main goal (conclusion). Tactics may operate on all subgoals or on a particularly specified subgoal, but must not change the main conclusion (apart from instantiating @@ -143,22 +146,23 @@ index as @{text "int"} argument in full generality; a hardwired subgoal 1 is not acceptable. - \medskip The main well-formedness conditions for proper tactics are + \<^medskip> + The main well-formedness conditions for proper tactics are summarized as follows. \begin{itemize} - \item General tactic failure is indicated by an empty result, only + \<^item> General tactic failure is indicated by an empty result, only serious faults may produce an exception. - \item The main conclusion must not be changed, apart from + \<^item> The main conclusion must not be changed, apart from instantiating schematic variables. - \item A tactic operates either uniformly on all subgoals, or + \<^item> A tactic operates either uniformly on all subgoals, or specifically on a selected subgoal (without bumping into unrelated subgoals). - \item Range errors in subgoal addressing produce an empty result. + \<^item> Range errors in subgoal addressing produce an empty result. \end{itemize} @@ -251,7 +255,8 @@ Assumption tactics close a subgoal by unifying some of its premises against its conclusion. - \medskip All the tactics in this section operate on a subgoal + \<^medskip> + All the tactics in this section operate on a subgoal designated by a positive integer. Other subgoals might be affected indirectly, due to instantiation of schematic variables. @@ -261,12 +266,12 @@ \begin{enumerate} - \item selecting one of the rules given as argument to the tactic; + \<^enum> selecting one of the rules given as argument to the tactic; - \item selecting a subgoal premise to eliminate, unifying it against + \<^enum> selecting a subgoal premise to eliminate, unifying it against the first premise of the rule; - \item unifying the conclusion of the subgoal to the conclusion of + \<^enum> unifying the conclusion of the subgoal to the conclusion of the rule. \end{enumerate} @@ -366,7 +371,8 @@ "?P"}, according to the shape of the given subgoal. This is sufficiently well-behaved in most practical situations. - \medskip Isabelle provides separate versions of the standard @{text + \<^medskip> + Isabelle provides separate versions of the standard @{text "r/e/d/f"} resolution tactics that allow to provide explicit instantiations of unknowns of the given rule, wrt.\ terms that refer to the implicit context of the selected subgoal. @@ -675,15 +681,15 @@ \begin{itemize} - \item @{ML all_tac} is the identity element of the tactical @{ML_op + \<^item> @{ML all_tac} is the identity element of the tactical @{ML_op "THEN"}. - \item @{ML no_tac} is the identity element of @{ML_op "ORELSE"} and + \<^item> @{ML no_tac} is the identity element of @{ML_op "ORELSE"} and @{ML_op "APPEND"}. Also, it is a zero element for @{ML_op "THEN"}, which means that @{text "tac"}~@{ML_op THEN}~@{ML no_tac} is equivalent to @{ML no_tac}. - \item @{ML TRY} and @{ML REPEAT} can be expressed as (recursive) + \<^item> @{ML TRY} and @{ML REPEAT} can be expressed as (recursive) functions over more basic combinators (ignoring some internal implementation tricks):