# HG changeset patch # User wenzelm # Date 1458205177 -3600 # Node ID 47635cd9a996a79314ce24e5ebf0696a03ed57ae # Parent 1d1d7f5c0b277b48ae33f2ceafbc3223d9bd0929 tuned whitespace; diff -r 1d1d7f5c0b27 -r 47635cd9a996 src/Doc/Isar_Ref/Generic.thy --- a/src/Doc/Isar_Ref/Generic.thy Thu Mar 17 09:41:21 2016 +0100 +++ b/src/Doc/Isar_Ref/Generic.thy Thu Mar 17 09:59:37 2016 +0100 @@ -247,24 +247,23 @@ section \The Simplifier \label{sec:simplifier}\ -text \The Simplifier performs conditional and unconditional - rewriting and uses contextual information: rule declarations in the - background theory or local proof context are taken into account, as - well as chained facts and subgoal premises (``local assumptions''). - There are several general hooks that allow to modify the - simplification strategy, or incorporate other proof tools that solve - sub-problems, produce rewrite rules on demand etc. +text \ + The Simplifier performs conditional and unconditional rewriting and uses + contextual information: rule declarations in the background theory or local + proof context are taken into account, as well as chained facts and subgoal + premises (``local assumptions''). There are several general hooks that allow + to modify the simplification strategy, or incorporate other proof tools that + solve sub-problems, produce rewrite rules on demand etc. - The rewriting strategy is always strictly bottom up, except for - congruence rules, which are applied while descending into a term. - Conditions in conditional rewrite rules are solved recursively - before the rewrite rule is applied. + The rewriting strategy is always strictly bottom up, except for congruence + rules, which are applied while descending into a term. Conditions in + conditional rewrite rules are solved recursively before the rewrite rule is + applied. - The default Simplifier setup of major object logics (HOL, HOLCF, - FOL, ZF) makes the Simplifier ready for immediate use, without - engaging into the internal structures. Thus it serves as - general-purpose proof tool with the main focus on equational - reasoning, and a bit more than that. + The default Simplifier setup of major object logics (HOL, HOLCF, FOL, ZF) + makes the Simplifier ready for immediate use, without engaging into the + internal structures. Thus it serves as general-purpose proof tool with the + main focus on equational reasoning, and a bit more than that. \ @@ -288,69 +287,63 @@ 'cong' (() | 'add' | 'del')) ':' @{syntax thmrefs} \} - \<^descr> @{method simp} invokes the Simplifier on the first subgoal, - after inserting chained facts as additional goal premises; further - rule declarations may be included via \(simp add: facts)\. - The proof method fails if the subgoal remains unchanged after - simplification. + \<^descr> @{method simp} invokes the Simplifier on the first subgoal, after + inserting chained facts as additional goal premises; further rule + declarations may be included via \(simp add: facts)\. The proof method fails + if the subgoal remains unchanged after simplification. - Note that the original goal premises and chained facts are subject - to simplification themselves, while declarations via \add\/\del\ merely follow the policies of the object-logic - to extract rewrite rules from theorems, without further - simplification. This may lead to slightly different behavior in - either case, which might be required precisely like that in some - boundary situations to perform the intended simplification step! + Note that the original goal premises and chained facts are subject to + simplification themselves, while declarations via \add\/\del\ merely follow + the policies of the object-logic to extract rewrite rules from theorems, + without further simplification. This may lead to slightly different behavior + in either case, which might be required precisely like that in some boundary + situations to perform the intended simplification step! \<^medskip> - The \only\ modifier first removes all other rewrite - rules, looper tactics (including split rules), congruence rules, and - then behaves like \add\. Implicit solvers remain, which means - that trivial rules like reflexivity or introduction of \True\ are available to solve the simplified subgoals, but also - non-trivial tools like linear arithmetic in HOL. The latter may - lead to some surprise of the meaning of ``only'' in Isabelle/HOL - compared to English! + The \only\ modifier first removes all other rewrite rules, looper tactics + (including split rules), congruence rules, and then behaves like \add\. + Implicit solvers remain, which means that trivial rules like reflexivity or + introduction of \True\ are available to solve the simplified subgoals, but + also non-trivial tools like linear arithmetic in HOL. The latter may lead to + some surprise of the meaning of ``only'' in Isabelle/HOL compared to + English! \<^medskip> - The \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, - ZF do this already). + The \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, ZF do this already). There is also a separate @{method_ref split} method available for - single-step case splitting. The effect of repeatedly applying - \(split thms)\ can be imitated by ``\(simp only: - split: thms)\''. + single-step case splitting. The effect of repeatedly applying \(split thms)\ + can be imitated by ``\(simp only: split: thms)\''. \<^medskip> - The \cong\ modifiers add or delete Simplifier - congruence rules (see also \secref{sec:simp-rules}); the default is - to add. + The \cong\ modifiers add or delete Simplifier congruence rules (see also + \secref{sec:simp-rules}); the default is to add. - \<^descr> @{method simp_all} is similar to @{method simp}, but acts on - all goals, working backwards from the last to the first one as usual - in Isabelle.\<^footnote>\The order is irrelevant for goals without - schematic variables, so simplification might actually be performed - in parallel here.\ + \<^descr> @{method simp_all} is similar to @{method simp}, but acts on all goals, + working backwards from the last to the first one as usual in Isabelle.\<^footnote>\The + order is irrelevant for goals without schematic variables, so simplification + might actually be performed in parallel here.\ - Chained facts are inserted into all subgoals, before the - simplification process starts. Further rule declarations are the - same as for @{method simp}. + Chained facts are inserted into all subgoals, before the simplification + process starts. Further rule declarations are the same as for @{method + simp}. The proof method fails if all subgoals remain unchanged after simplification. - \<^descr> @{attribute simp_depth_limit} limits the number of recursive - invocations of the Simplifier during conditional rewriting. + \<^descr> @{attribute simp_depth_limit} limits the number of recursive invocations + of the Simplifier during conditional rewriting. - By default the Simplifier methods above take local assumptions fully - into account, using equational assumptions in the subsequent - normalization process, or simplifying assumptions themselves. - Further options allow to fine-tune the behavior of the Simplifier - in this respect, corresponding to a variety of ML tactics as - follows.\<^footnote>\Unlike the corresponding Isar proof methods, the - ML tactics do not insist in changing the goal state.\ + By default the Simplifier methods above take local assumptions fully into + account, using equational assumptions in the subsequent normalization + process, or simplifying assumptions themselves. Further options allow to + fine-tune the behavior of the Simplifier in this respect, corresponding to a + variety of ML tactics as follows.\<^footnote>\Unlike the corresponding Isar proof + methods, the ML tactics do not insist in changing the goal state.\ \begin{center} \small @@ -358,24 +351,21 @@ \hline Isar method & ML tactic & behavior \\\hline - \(simp (no_asm))\ & @{ML simp_tac} & assumptions are ignored - completely \\\hline + \(simp (no_asm))\ & @{ML simp_tac} & assumptions are ignored completely + \\\hline - \(simp (no_asm_simp))\ & @{ML asm_simp_tac} & assumptions - are used in the simplification of the conclusion but are not - themselves simplified \\\hline + \(simp (no_asm_simp))\ & @{ML asm_simp_tac} & assumptions are used in the + simplification of the conclusion but are not themselves simplified \\\hline - \(simp (no_asm_use))\ & @{ML full_simp_tac} & assumptions - are simplified but are not used in the simplification of each other - or the conclusion \\\hline + \(simp (no_asm_use))\ & @{ML full_simp_tac} & assumptions are simplified but + are not used in the simplification of each other or the conclusion \\\hline - \(simp)\ & @{ML asm_full_simp_tac} & assumptions are used in - the simplification of the conclusion and to simplify other - assumptions \\\hline + \(simp)\ & @{ML asm_full_simp_tac} & assumptions are used in the + simplification of the conclusion and to simplify other assumptions \\\hline - \(simp (asm_lr))\ & @{ML asm_lr_simp_tac} & compatibility - mode: an assumption is only used for simplifying assumptions which - are to the right of it \\\hline + \(simp (asm_lr))\ & @{ML asm_lr_simp_tac} & compatibility mode: an + assumption is only used for simplifying assumptions which are to the right + of it \\\hline \end{tabular} \end{center} @@ -384,18 +374,19 @@ subsubsection \Examples\ -text \We consider basic algebraic simplifications in Isabelle/HOL. - The rather trivial goal @{prop "0 + (x + 0) = x + 0 + 0"} looks like - a good candidate to be solved by a single call of @{method simp}: +text \ + We consider basic algebraic simplifications in Isabelle/HOL. The rather + trivial goal @{prop "0 + (x + 0) = x + 0 + 0"} looks like a good candidate + to be solved by a single call of @{method simp}: \ lemma "0 + (x + 0) = x + 0 + 0" apply simp? oops -text \The above attempt \<^emph>\fails\, because @{term "0"} and @{term - "op +"} in the HOL library are declared as generic type class - operations, without stating any algebraic laws yet. More specific - types are required to get access to certain standard simplifications - of the theory context, e.g.\ like this:\ +text \ + The above attempt \<^emph>\fails\, because @{term "0"} and @{term "op +"} in the + HOL library are declared as generic type class operations, without stating + any algebraic laws yet. More specific types are required to get access to + certain standard simplifications of the theory context, e.g.\ like this:\ lemma fixes x :: nat shows "0 + (x + 0) = x + 0 + 0" by simp lemma fixes x :: int shows "0 + (x + 0) = x + 0 + 0" by simp @@ -403,39 +394,38 @@ text \ \<^medskip> - In many cases, assumptions of a subgoal are also needed in - the simplification process. For example: + In many cases, assumptions of a subgoal are also needed in the + simplification process. For example: \ lemma fixes x :: nat shows "x = 0 \ x + x = 0" by simp lemma fixes x :: nat assumes "x = 0" shows "x + x = 0" apply simp oops lemma fixes x :: nat assumes "x = 0" shows "x + x = 0" using assms by simp -text \As seen above, local assumptions that shall contribute to - simplification need to be part of the subgoal already, or indicated - explicitly for use by the subsequent method invocation. Both too - little or too much information can make simplification fail, for - different reasons. +text \ + As seen above, local assumptions that shall contribute to simplification + need to be part of the subgoal already, or indicated explicitly for use by + the subsequent method invocation. Both too little or too much information + can make simplification fail, for different reasons. - In the next example the malicious assumption @{prop "\x::nat. f x = - g (f (g x))"} does not contribute to solve the problem, but makes - the default @{method simp} method loop: the rewrite rule \f - ?x \ g (f (g ?x))\ extracted from the assumption does not - terminate. The Simplifier notices certain simple forms of - nontermination, but not this one. The problem can be solved - nonetheless, by ignoring assumptions via special options as - explained before: + In the next example the malicious assumption @{prop "\x::nat. f x = g (f (g + x))"} does not contribute to solve the problem, but makes the default + @{method simp} method loop: the rewrite rule \f ?x \ g (f (g ?x))\ extracted + from the assumption does not terminate. The Simplifier notices certain + simple forms of nontermination, but not this one. The problem can be solved + nonetheless, by ignoring assumptions via special options as explained + before: \ lemma "(\x::nat. f x = g (f (g x))) \ f 0 = f 0 + 0" by (simp (no_asm)) -text \The latter form is typical for long unstructured proof - scripts, where the control over the goal content is limited. In - structured proofs it is usually better to avoid pushing too many - facts into the goal state in the first place. Assumptions in the - Isar proof context do not intrude the reasoning if not used - explicitly. This is illustrated for a toplevel statement and a +text \ + The latter form is typical for long unstructured proof scripts, where the + control over the goal content is limited. In structured proofs it is usually + better to avoid pushing too many facts into the goal state in the first + place. Assumptions in the Isar proof context do not intrude the reasoning if + not used explicitly. This is illustrated for a toplevel statement and a local proof body as follows: \ @@ -451,26 +441,26 @@ 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 + 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 \[ \P (f x)\ \stackrel{\f x \ f y\}{\longmapsto} \P (f y)\ \stackrel{\y \ x\}{\longmapsto} \P (f x)\ \stackrel{\f x \ f y\}{\longmapsto} \cdots \] - whereas applying the same to @{prop "y = x \ f x = f y \ P (f x) \ - Q"} terminates (without solving the goal): + whereas applying the same to @{prop "y = x \ f x = f y \ P (f x) \ Q"} + terminates (without solving the goal): \ lemma "y = x \ f x = f y \ P (f x) \ Q" apply simp oops -text \See also \secref{sec:simp-trace} for options to enable - Simplifier trace mode, which often helps to diagnose problems with - rewrite systems. +text \ + See also \secref{sec:simp-trace} for options to enable Simplifier trace + mode, which often helps to diagnose problems with rewrite systems. \ @@ -491,200 +481,191 @@ @@{command print_simpset} ('!'?) \} - \<^descr> @{attribute simp} declares rewrite rules, by adding or - deleting them from the simpset within the theory or proof context. - Rewrite rules are theorems expressing some form of equality, for - example: + \<^descr> @{attribute simp} declares rewrite rules, by adding or deleting them from + the simpset within the theory or proof context. Rewrite rules are theorems + expressing some form of equality, for example: \Suc ?m + ?n = ?m + Suc ?n\ \\ \?P \ ?P \ ?P\ \\ \?A \ ?B \ {x. x \ ?A \ x \ ?B}\ \<^medskip> - Conditional rewrites such as \?m < ?n \ ?m div ?n = 0\ are - also permitted; the conditions can be arbitrary formulas. + Conditional rewrites such as \?m < ?n \ ?m div ?n = 0\ are also permitted; + the conditions can be arbitrary formulas. \<^medskip> - Internally, all rewrite rules are translated into Pure - equalities, theorems with conclusion \lhs \ rhs\. The - simpset contains a function for extracting equalities from arbitrary - theorems, which is usually installed when the object-logic is - configured initially. For example, \\ ?x \ {}\ could be - turned into \?x \ {} \ False\. Theorems that are declared as - @{attribute simp} and local assumptions within a goal are treated - uniformly in this respect. + Internally, all rewrite rules are translated into Pure equalities, theorems + with conclusion \lhs \ rhs\. The simpset contains a function for extracting + equalities from arbitrary theorems, which is usually installed when the + object-logic is configured initially. For example, \\ ?x \ {}\ could be + turned into \?x \ {} \ False\. Theorems that are declared as @{attribute + simp} and local assumptions within a goal are treated uniformly in this + respect. - The Simplifier accepts the following formats for the \lhs\ - term: + The Simplifier accepts the following formats for the \lhs\ term: - \<^enum> First-order patterns, considering the sublanguage of - application of constant operators to variable operands, without - \\\-abstractions or functional variables. - For example: + \<^enum> First-order patterns, considering the sublanguage of application of + constant operators to variable operands, without \\\-abstractions or + functional variables. For example: \(?x + ?y) + ?z \ ?x + (?y + ?z)\ \\ \f (f ?x ?y) ?z \ f ?x (f ?y ?z)\ - \<^enum> Higher-order patterns in the sense of @{cite "nipkow-patterns"}. - These are terms in \\\-normal form (this will always be the - case unless you have done something strange) where each occurrence - of an unknown is of the form \?F x\<^sub>1 \ x\<^sub>n\, where the - \x\<^sub>i\ are distinct bound variables. + \<^enum> Higher-order patterns in the sense of @{cite "nipkow-patterns"}. These + are terms in \\\-normal form (this will always be the case unless you have + done something strange) where each occurrence of an unknown is of the form + \?F x\<^sub>1 \ x\<^sub>n\, where the \x\<^sub>i\ are distinct bound variables. - For example, \(\x. ?P x \ ?Q x) \ (\x. ?P x) \ (\x. ?Q x)\ - or its symmetric form, since the \rhs\ is also a - higher-order pattern. + For example, \(\x. ?P x \ ?Q x) \ (\x. ?P x) \ (\x. ?Q x)\ or its + symmetric form, since the \rhs\ is also a higher-order pattern. - \<^enum> Physical first-order patterns over raw \\\-term - structure without \\\\\-equality; abstractions and bound - variables are treated like quasi-constant term material. + \<^enum> Physical first-order patterns over raw \\\-term structure without + \\\\\-equality; abstractions and bound variables are treated like + quasi-constant term material. - For example, the rule \?f ?x \ range ?f = True\ rewrites the - term \g a \ range g\ to \True\, but will fail to - match \g (h b) \ range (\x. g (h x))\. However, offending - subterms (in our case \?f ?x\, which is not a pattern) can - be replaced by adding new variables and conditions like this: \?y = ?f ?x \ ?y \ range ?f = True\ is acceptable as a conditional - rewrite rule of the second category since conditions can be - arbitrary terms. + For example, the rule \?f ?x \ range ?f = True\ rewrites the term \g a \ + range g\ to \True\, but will fail to match \g (h b) \ range (\x. g (h + x))\. However, offending subterms (in our case \?f ?x\, which is not a + pattern) can be replaced by adding new variables and conditions like this: + \?y = ?f ?x \ ?y \ range ?f = True\ is acceptable as a conditional rewrite + rule of the second category since conditions can be arbitrary terms. \<^descr> @{attribute split} declares case split rules. - \<^descr> @{attribute cong} declares congruence rules to the Simplifier - context. + \<^descr> @{attribute cong} declares congruence rules to the Simplifier context. Congruence rules are equalities of the form @{text [display] "\ \ f ?x\<^sub>1 \ ?x\<^sub>n = f ?y\<^sub>1 \ ?y\<^sub>n"} - This controls the simplification of the arguments of \f\. For - example, some arguments can be simplified under additional - assumptions: @{text [display] "?P\<^sub>1 \ ?Q\<^sub>1 \ (?Q\<^sub>1 \ ?P\<^sub>2 \ ?Q\<^sub>2) \ - (?P\<^sub>1 \ ?P\<^sub>2) \ (?Q\<^sub>1 \ ?Q\<^sub>2)"} + This controls the simplification of the arguments of \f\. For example, some + arguments can be simplified under additional assumptions: + @{text [display] + "?P\<^sub>1 \ ?Q\<^sub>1 \ + (?Q\<^sub>1 \ ?P\<^sub>2 \ ?Q\<^sub>2) \ + (?P\<^sub>1 \ ?P\<^sub>2) \ (?Q\<^sub>1 \ ?Q\<^sub>2)"} - Given this rule, the Simplifier assumes \?Q\<^sub>1\ and extracts - rewrite rules from it when simplifying \?P\<^sub>2\. Such local - assumptions are effective for rewriting formulae such as \x = - 0 \ y + x = y\. + Given this rule, the Simplifier assumes \?Q\<^sub>1\ and extracts rewrite rules + from it when simplifying \?P\<^sub>2\. Such local assumptions are effective for + rewriting formulae such as \x = 0 \ y + x = y\. %FIXME %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 - supplies contextual information --- about the bound variable: - @{text [display] "(?A = ?B) \ (\x. x \ ?B \ ?P x \ ?Q x) \ + 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 - supply contextual information for simplifying the arms: - @{text [display] "?p = ?q \ (?q \ ?a = ?c) \ (\ ?q \ ?b = ?d) \ + 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)"} - A congruence rule can also \<^emph>\prevent\ simplification of some - arguments. Here is an alternative congruence rule for conditional - expressions that conforms to non-strict functional evaluation: - @{text [display] "?p = ?q \ (if ?p then ?a else ?b) = (if ?q then ?a else ?b)"} + A congruence rule can also \<^emph>\prevent\ simplification of some arguments. Here + is an alternative congruence rule for conditional expressions that conforms + to non-strict functional evaluation: @{text [display] + "?p = ?q \ + (if ?p then ?a else ?b) = (if ?q then ?a else ?b)"} - Only the first argument is simplified; the others remain unchanged. - This can make simplification much faster, but may require an extra - case split over the condition \?q\ to prove the goal. + Only the first argument is simplified; the others remain unchanged. This can + make simplification much faster, but may require an extra case split over + the condition \?q\ to prove the goal. - \<^descr> @{command "print_simpset"} prints the collection of rules declared - to the Simplifier, which is also known as ``simpset'' internally; the - ``\!\'' option indicates extra verbosity. + \<^descr> @{command "print_simpset"} prints the collection of rules declared to the + Simplifier, which is also known as ``simpset'' internally; the ``\!\'' + option indicates extra verbosity. - For historical reasons, simpsets may occur independently from the - current context, but are conceptually dependent on it. When the - Simplifier is invoked via one of its main entry points in the Isar - source language (as proof method \secref{sec:simp-meth} or rule - attribute \secref{sec:simp-meth}), its simpset is derived from the - current proof context, and carries a back-reference to that for - other tools that might get invoked internally (e.g.\ simplification - procedures \secref{sec:simproc}). A mismatch of the context of the - simpset and the context of the problem being simplified may lead to - unexpected results. + For historical reasons, simpsets may occur independently from the current + context, but are conceptually dependent on it. When the Simplifier is + invoked via one of its main entry points in the Isar source language (as + proof method \secref{sec:simp-meth} or rule attribute + \secref{sec:simp-meth}), its simpset is derived from the current proof + context, and carries a back-reference to that for other tools that might get + invoked internally (e.g.\ simplification procedures \secref{sec:simproc}). A + mismatch of the context of the simpset and the context of the problem being + simplified may lead to unexpected results. - The implicit simpset of the theory context is propagated - monotonically through the theory hierarchy: forming a new theory, - the union of the simpsets of its imports are taken as starting - point. Also note that definitional packages like @{command - "datatype"}, @{command "primrec"}, @{command "fun"} routinely - declare Simplifier rules to the target context, while plain - @{command "definition"} is an exception in \<^emph>\not\ declaring + The implicit simpset of the theory context is propagated monotonically + through the theory hierarchy: forming a new theory, the union of the + simpsets of its imports are taken as starting point. Also note that + definitional packages like @{command "datatype"}, @{command "primrec"}, + @{command "fun"} routinely declare Simplifier rules to the target context, + while plain @{command "definition"} is an exception in \<^emph>\not\ declaring anything. \<^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 - that obviously simplify, like \?n + 0 \ ?n\ are good - candidates for the implicit simpset, unless a special - non-normalizing behavior of certain operations is intended. More - specific rules (such as distributive laws, which duplicate subterms) - should be added only for specific proof steps. Conversely, - sometimes a rule needs to be deleted just for some part of a proof. - The need of frequent additions or deletions may indicate a poorly - designed simpset. + 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 that obviously simplify, like \?n + 0 \ ?n\ are + good candidates for the implicit simpset, unless a special non-normalizing + behavior of certain operations is intended. More specific rules (such as + distributive laws, which duplicate subterms) should be added only for + specific proof steps. Conversely, sometimes a rule needs to be deleted just + for some part of a proof. The need of frequent additions or deletions may + indicate a poorly designed simpset. \begin{warn} - The union of simpsets from theory imports (as described above) is - not always a good starting point for the new theory. If some - ancestors have deleted simplification rules because they are no - longer wanted, while others have left those rules in, then the union - will contain the unwanted rules, and thus have to be deleted again - in the theory body. + The union of simpsets from theory imports (as described above) is not always + a good starting point for the new theory. If some ancestors have deleted + simplification rules because they are no longer wanted, while others have + left those rules in, then the union will contain the unwanted rules, and + thus have to be deleted again in the theory body. \end{warn} \ subsection \Ordered rewriting with permutative rules\ -text \A rewrite rule is \<^emph>\permutative\ if the left-hand side and - right-hand side are the equal up to renaming of variables. The most - common permutative rule is commutativity: \?x + ?y = ?y + - ?x\. Other examples include \(?x - ?y) - ?z = (?x - ?z) - - ?y\ in arithmetic and \insert ?x (insert ?y ?A) = insert ?y - (insert ?x ?A)\ for sets. Such rules are common enough to merit - special attention. +text \ + A rewrite rule is \<^emph>\permutative\ if the left-hand side and right-hand side + are the equal up to renaming of variables. The most common permutative rule + is commutativity: \?x + ?y = ?y + ?x\. Other examples include \(?x - ?y) - + ?z = (?x - ?z) - ?y\ in arithmetic and \insert ?x (insert ?y ?A) = insert ?y + (insert ?x ?A)\ for sets. Such rules are common enough to merit special + attention. - Because ordinary rewriting loops given such rules, the Simplifier - employs a special strategy, called \<^emph>\ordered rewriting\. - Permutative rules are detected and only applied if the rewriting - step decreases the redex wrt.\ a given term ordering. For example, - commutativity rewrites \b + a\ to \a + b\, but then - stops, because the redex cannot be decreased further in the sense of - the term ordering. + Because ordinary rewriting loops given such rules, the Simplifier employs a + special strategy, called \<^emph>\ordered rewriting\. Permutative rules are + detected and only applied if the rewriting step decreases the redex wrt.\ a + given term ordering. For example, commutativity rewrites \b + a\ to \a + b\, + but then stops, because the redex cannot be decreased further in the sense + of the term ordering. - The default is lexicographic ordering of term structure, but this - could be also changed locally for special applications via - @{index_ML Simplifier.set_termless} in Isabelle/ML. + The default is lexicographic ordering of term structure, but this 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 - just like other rewrite rules. Their special status is recognized - automatically, and their application is guarded by the term ordering - accordingly.\ + 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. +\ subsubsection \Rewriting with AC operators\ -text \Ordered rewriting is particularly effective in the case of - associative-commutative operators. (Associativity by itself is not - permutative.) When dealing with an AC-operator \f\, keep - the following points in mind: +text \ + Ordered rewriting is particularly effective in the case of + associative-commutative operators. (Associativity by itself is not + permutative.) When dealing with an AC-operator \f\, keep the following + points in mind: - \<^item> The associative law must always be oriented from left to - right, namely \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> The associative law must always be oriented from left to right, namely + \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 - associativity (A) and commutativity (C) but also a derived rule - \<^emph>\left-commutativity\ (LC): \f x (f y z) = f y (f x z)\. - + \<^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): \f x (f y z) = f y (f x z)\. Ordered rewriting with the combination of A, C, and LC sorts a term lexicographically --- the rewriting engine imitates bubble-sort. @@ -704,9 +685,11 @@ lemmas AC_rules = assoc commute left_commute -text \Thus the Simplifier is able to establish equalities with - arbitrary permutations of subterms, by normalizing to a common - standard form. For example:\ +text \ + Thus the Simplifier is able to establish equalities with arbitrary + permutations of subterms, by normalizing to a common standard form. For + example: +\ lemma "(b \ c) \ a = xxx" apply (simp only: AC_rules) @@ -719,10 +702,11 @@ end -text \Martin and Nipkow @{cite "martin-nipkow"} discuss the theory and - give many examples; other algebraic structures are amenable to - ordered rewriting, such as Boolean rings. The Boyer-Moore theorem - prover @{cite bm88book} also employs ordered rewriting. +text \ + Martin and Nipkow @{cite "martin-nipkow"} discuss the theory and give many + examples; other algebraic structures are amenable to ordered rewriting, such + as Boolean rings. The Boyer-Moore theorem prover @{cite bm88book} also + employs ordered rewriting. \ @@ -761,29 +745,29 @@ These attributes and configurations options control various aspects of Simplifier tracing and debugging. - \<^descr> @{attribute simp_trace} makes the Simplifier output internal - operations. This includes rewrite steps, but also bookkeeping like - modifications of the simpset. + \<^descr> @{attribute simp_trace} makes the Simplifier output internal operations. + This includes rewrite steps, but also bookkeeping like modifications of the + simpset. - \<^descr> @{attribute simp_trace_depth_limit} limits the effect of - @{attribute simp_trace} to the given depth of recursive Simplifier - invocations (when solving conditions of rewrite rules). + \<^descr> @{attribute simp_trace_depth_limit} limits the effect of @{attribute + simp_trace} to the given depth of recursive Simplifier invocations (when + solving conditions of rewrite rules). - \<^descr> @{attribute simp_debug} makes the Simplifier output some extra - information about internal operations. This includes any attempted - invocation of simplification procedures. + \<^descr> @{attribute simp_debug} makes the Simplifier output some extra information + about internal operations. This includes any attempted invocation of + simplification procedures. \<^descr> @{attribute simp_trace_new} controls Simplifier tracing within Isabelle/PIDE applications, notably Isabelle/jEdit @{cite "isabelle-jedit"}. - This provides a hierarchical representation of the rewriting steps - performed by the Simplifier. + This provides a hierarchical representation of the rewriting steps performed + by the Simplifier. Users can configure the behaviour by specifying breakpoints, verbosity and enabling or disabling the interactive mode. In normal verbosity (the - default), only rule applications matching a breakpoint will be shown to - the user. In full verbosity, all rule applications will be logged. - Interactive mode interrupts the normal flow of the Simplifier and defers - the decision how to continue to the user via some GUI dialog. + default), only rule applications matching a breakpoint will be shown to the + user. In full verbosity, all rule applications will be logged. Interactive + mode interrupts the normal flow of the Simplifier and defers the decision + how to continue to the user via some GUI dialog. \<^descr> @{attribute simp_break} declares term or theorem breakpoints for @{attribute simp_trace_new} as described above. Term breakpoints are @@ -800,21 +784,19 @@ subsection \Simplification procedures \label{sec:simproc}\ -text \Simplification procedures are ML functions that produce proven - rewrite rules on demand. They are associated with higher-order - patterns that approximate the left-hand sides of equations. The - Simplifier first matches the current redex against one of the LHS - patterns; if this succeeds, the corresponding ML function is - invoked, passing the Simplifier context and redex term. Thus rules - may be specifically fashioned for particular situations, resulting - in a more powerful mechanism than term rewriting by a fixed set of - rules. +text \ + Simplification procedures are ML functions that produce proven rewrite rules + on demand. They are associated with higher-order patterns that approximate + the left-hand sides of equations. The Simplifier first matches the current + redex against one of the LHS patterns; if this succeeds, the corresponding + ML function is invoked, passing the Simplifier context and redex term. Thus + rules may be specifically fashioned for particular situations, resulting in + a more powerful mechanism than term rewriting by a fixed set of rules. - Any successful result needs to be a (possibly conditional) rewrite - rule \t \ u\ that is applicable to the current redex. The - rule will be applied just as any ordinary rewrite rule. It is - expected to be already in \<^emph>\internal form\, bypassing the - automatic preprocessing of object-level equivalences. + Any successful result needs to be a (possibly conditional) rewrite rule \t \ + u\ that is applicable to the current redex. The rule will be applied just as + any ordinary rewrite rule. It is expected to be already in \<^emph>\internal form\, + bypassing the automatic preprocessing of object-level equivalences. \begin{matharray}{rcl} @{command_def "simproc_setup"} & : & \local_theory \ local_theory\ \\ @@ -829,40 +811,39 @@ @@{attribute simproc} (('add' ':')? | 'del' ':') (@{syntax name}+) \} - \<^descr> @{command "simproc_setup"} defines a named simplification - procedure that is invoked by the Simplifier whenever any of the - given term patterns match the current redex. The implementation, - which is provided as ML source text, needs to be of type @{ML_type - "morphism -> Proof.context -> cterm -> thm option"}, where the @{ML_type - cterm} represents the current redex \r\ and the result is - supposed to be some proven rewrite rule \r \ r'\ (or a - generalized version), or @{ML NONE} to indicate failure. The - @{ML_type Proof.context} argument holds the full context of the current - Simplifier invocation. The - @{ML_type morphism} informs about the difference of the original - compilation context wrt.\ the one of the actual application later - on. The optional @{keyword "identifier"} specifies theorems that - represent the logical content of the abstract theory of this - simproc. + \<^descr> @{command "simproc_setup"} defines a named simplification procedure that + is invoked by the Simplifier whenever any of the given term patterns match + the current redex. The implementation, which is provided as ML source text, + needs to be of type + @{ML_type "morphism -> Proof.context -> cterm -> thm option"}, where the + @{ML_type cterm} represents the current redex \r\ and the result is supposed + to be some proven rewrite rule \r \ r'\ (or a generalized version), or @{ML + NONE} to indicate failure. The @{ML_type Proof.context} argument holds the + full context of the current Simplifier invocation. The @{ML_type morphism} + informs about the difference of the original compilation context wrt.\ the + one of the actual application later on. The optional @{keyword "identifier"} + specifies theorems that represent the logical content of the abstract theory + of this simproc. - Morphisms and identifiers are only relevant for simprocs that are - defined within a local target context, e.g.\ in a locale. + Morphisms and identifiers are only relevant for simprocs that are defined + within a local target context, e.g.\ in a locale. - \<^descr> \simproc add: name\ and \simproc del: name\ - add or delete named simprocs to the current Simplifier context. The - default is to add a simproc. Note that @{command "simproc_setup"} - already adds the new simproc to the subsequent context. + \<^descr> \simproc add: name\ and \simproc del: name\ add or delete named simprocs + to the current Simplifier context. The default is to add a simproc. Note + that @{command "simproc_setup"} already adds the new simproc to the + subsequent context. \ subsubsection \Example\ -text \The following simplification procedure for @{thm - [source=false, show_types] unit_eq} in HOL performs fine-grained - control over rule application, beyond higher-order pattern matching. - Declaring @{thm unit_eq} as @{attribute simp} directly would make - the Simplifier loop! Note that a version of this simplification - procedure is already active in Isabelle/HOL.\ +text \ + The following simplification procedure for @{thm [source = false, + show_types] unit_eq} in HOL performs fine-grained control over rule + application, beyond higher-order pattern matching. Declaring @{thm unit_eq} + as @{attribute simp} directly would make the Simplifier loop! Note that a + version of this simplification procedure is already active in Isabelle/HOL. +\ (*<*)experiment begin(*>*) simproc_setup unit ("x::unit") = @@ -871,20 +852,20 @@ else SOME (mk_meta_eq @{thm unit_eq})\ (*<*)end(*>*) -text \Since the Simplifier applies simplification procedures - frequently, it is important to make the failure check in ML - reasonably fast.\ +text \ + Since the Simplifier applies simplification procedures frequently, it is + important to make the failure check in ML reasonably fast.\ subsection \Configurable Simplifier strategies \label{sec:simp-strategies}\ -text \The core term-rewriting engine of the Simplifier is normally - used in combination with some add-on components that modify the - strategy and allow to integrate other non-Simplifier proof tools. - These may be reconfigured in ML as explained below. Even if the - default strategies of object-logics like Isabelle/HOL are used - unchanged, it helps to understand how the standard Simplifier - strategies work.\ +text \ + The core term-rewriting engine of the Simplifier is normally used in + combination with some add-on components that modify the strategy and allow + to integrate other non-Simplifier proof tools. These may be reconfigured in + ML as explained below. Even if the default strategies of object-logics like + Isabelle/HOL are used unchanged, it helps to understand how the standard + Simplifier strategies work.\ subsubsection \The subgoaler\ @@ -897,21 +878,20 @@ \end{mldecls} The subgoaler is the tactic used to solve subgoals arising out of - conditional rewrite rules or congruence rules. The default should - be simplification itself. In rare situations, this strategy may - need to be changed. For example, if the premise of a conditional - rule is an instance of its conclusion, as in \Suc ?m < ?n \ - ?m < ?n\, the default strategy could loop. % FIXME !?? + conditional rewrite rules or congruence rules. The default should be + simplification itself. In rare situations, this strategy may need to be + changed. For example, if the premise of a conditional rule is an instance of + its conclusion, as in \Suc ?m < ?n \ ?m < ?n\, the default strategy could + loop. % FIXME !?? - \<^descr> @{ML Simplifier.set_subgoaler}~\tac ctxt\ sets the - subgoaler of the context to \tac\. The tactic will - be applied to the context of the running Simplifier instance. + \<^descr> @{ML Simplifier.set_subgoaler}~\tac ctxt\ sets the subgoaler of the + context to \tac\. The tactic will be applied to the context of the running + Simplifier instance. - \<^descr> @{ML Simplifier.prems_of}~\ctxt\ retrieves the current - set of premises from the context. This may be non-empty only if - the Simplifier has been told to utilize local assumptions in the - first place (cf.\ the options in \secref{sec:simp-meth}). - + \<^descr> @{ML Simplifier.prems_of}~\ctxt\ retrieves the current set of premises + from the context. This may be non-empty only if the Simplifier has been + told to utilize local assumptions in the first place (cf.\ the options in + \secref{sec:simp-meth}). As an example, consider the following alternative subgoaler: \ @@ -923,9 +903,9 @@ asm_simp_tac ctxt \ -text \This tactic first tries to solve the subgoal by assumption or - by resolving with with one of the premises, calling simplification - only if that fails.\ +text \ + This tactic first tries to solve the subgoal by assumption or by resolving + with with one of the premises, calling simplification only if that fails.\ subsubsection \The solver\ @@ -941,89 +921,76 @@ @{index_ML_op addSSolver: "Proof.context * solver -> Proof.context"} \\ \end{mldecls} - A solver is a tactic that attempts to solve a subgoal after - simplification. Its core functionality is to prove trivial subgoals - such as @{prop "True"} and \t = t\, but object-logics might - be more ambitious. For example, Isabelle/HOL performs a restricted - version of linear arithmetic here. + A solver is a tactic that attempts to solve a subgoal after simplification. + Its core functionality is to prove trivial subgoals such as @{prop "True"} + and \t = t\, but object-logics might be more ambitious. For example, + Isabelle/HOL performs a restricted version of linear arithmetic here. - Solvers are packaged up in abstract type @{ML_type solver}, with - @{ML Simplifier.mk_solver} as the only operation to create a solver. + 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, - rewriting alone cannot prove \a \ ?A\ since this requires - instantiating \?A\. The solver, however, is an arbitrary - tactic and may instantiate unknowns as it pleases. This is the only - way the Simplifier can handle a conditional rewrite rule whose - condition contains extra variables. When a simplification tactic is - to be combined with other provers, especially with the Classical - Reasoner, it is important whether it can be considered safe or not. - For this reason a simpset contains two solvers: safe and unsafe. + Rewriting does not instantiate unknowns. For example, rewriting alone cannot + prove \a \ ?A\ since this requires instantiating \?A\. The solver, however, + is an arbitrary tactic and may instantiate unknowns as it pleases. This is + the only way the Simplifier can handle a conditional rewrite rule whose + condition contains extra variables. When a simplification tactic is to be + combined with other provers, especially with the Classical Reasoner, it is + important whether it can be considered safe or not. For this reason a + simpset contains two solvers: safe and unsafe. - The standard simplification strategy solely uses the unsafe solver, - which is appropriate in most cases. For special applications where - the simplification process is not allowed to instantiate unknowns - within the goal, simplification starts with the safe solver, but may - still apply the ordinary unsafe one in nested simplifications for - conditional rules or congruences. Note that in this way the overall - tactic is not totally safe: it may instantiate unknowns that appear - also in other subgoals. - - \<^descr> @{ML Simplifier.mk_solver}~\name tac\ turns \tac\ into a solver; the \name\ is only attached as a - comment and has no further significance. + The standard simplification strategy solely uses the unsafe solver, which is + appropriate in most cases. For special applications where the simplification + process is not allowed to instantiate unknowns within the goal, + simplification starts with the safe solver, but may still apply the ordinary + unsafe one in nested simplifications for conditional rules or congruences. + Note that in this way the overall tactic is not totally safe: it may + instantiate unknowns that appear also in other subgoals. - \<^descr> \ctxt setSSolver solver\ installs \solver\ as - the safe solver of \ctxt\. + \<^descr> @{ML Simplifier.mk_solver}~\name tac\ turns \tac\ into a solver; the + \name\ is only attached as a comment and has no further significance. - \<^descr> \ctxt addSSolver solver\ adds \solver\ as an - additional safe solver; it will be tried after the solvers which had - already been present in \ctxt\. + \<^descr> \ctxt setSSolver solver\ installs \solver\ as the safe solver of \ctxt\. - \<^descr> \ctxt setSolver solver\ installs \solver\ as the - unsafe solver of \ctxt\. + \<^descr> \ctxt addSSolver solver\ adds \solver\ as an additional safe solver; it + will be tried after the solvers which had already been present in \ctxt\. - \<^descr> \ctxt addSolver solver\ adds \solver\ as an - additional unsafe solver; it will be tried after the solvers which - had already been present in \ctxt\. + \<^descr> \ctxt setSolver solver\ installs \solver\ as the unsafe solver of \ctxt\. + + \<^descr> \ctxt addSolver solver\ adds \solver\ as an additional unsafe solver; it + will be tried after the solvers which had already been present in \ctxt\. \<^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 - list may be non-empty only if the Simplifier runs in a mode that - utilizes local assumptions (see also \secref{sec:simp-meth}). The - solver is also presented the full goal including its assumptions in - any case. Thus it can use these (e.g.\ by calling @{ML - assume_tac}), even if the Simplifier proper happens to ignore local - premises at the moment. + 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 + list may be non-empty only if the Simplifier runs in a mode that utilizes + local assumptions (see also \secref{sec:simp-meth}). The solver is also + presented the full goal including its assumptions in any case. Thus it can + use these (e.g.\ by calling @{ML 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 - the premises of congruence rules. These are usually of the form - \s = ?x\, where \s\ needs to be simplified and - \?x\ needs to be instantiated with the result. Typically, + As explained before, the subgoaler is also used to solve the premises of + congruence rules. These are usually of the form \s = ?x\, where \s\ needs to + be simplified and \?x\ needs to be instantiated with the result. Typically, the subgoaler will invoke the Simplifier at some point, which will - eventually call the solver. For this reason, solver tactics must be - prepared to solve goals of the form \t = ?x\, usually by - reflexivity. In particular, reflexivity should be tried before any - of the fancy automated proof tools. + eventually call the solver. For this reason, solver tactics must be prepared + to solve goals of the form \t = ?x\, usually by reflexivity. In particular, + reflexivity should be tried before any of the fancy automated proof tools. - It may even happen that due to simplification the subgoal is no - longer an equality. For example, \False \ ?Q\ could be - rewritten to \\ ?Q\. To cover this case, the solver could - try resolving with the theorem \\ False\ of the + It may even happen that due to simplification the subgoal is no longer an + equality. For example, \False \ ?Q\ could be rewritten to \\ ?Q\. To cover + this case, the solver could try resolving with the theorem \\ False\ of the object-logic. \<^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 - \<^emph>\conditional\ --- that is, contains premises not of the form - \t = ?x\. Otherwise it indicates that some congruence rule, - or possibly the subgoaler or solver, is faulty. + If a premise of a congruence rule cannot be proved, then the congruence is + ignored. This should only happen if the rule is \<^emph>\conditional\ --- that is, + contains premises not of the form \t = ?x\. Otherwise it indicates that some + congruence rule, or possibly the subgoaler or solver, is faulty. \end{warn} \ @@ -1042,69 +1009,62 @@ @{index_ML Splitter.del_split: "thm -> Proof.context -> Proof.context"} \\ \end{mldecls} - The looper is a list of tactics that are applied after - simplification, in case the solver failed to solve the simplified - goal. If the looper succeeds, the simplification process is started - all over again. Each of the subgoals generated by the looper is - attacked in turn, in reverse order. + The looper is a list of tactics that are applied after simplification, in + case the solver failed to solve the simplified goal. If the looper succeeds, + the simplification process is started all over again. Each of the subgoals + generated by the looper is attacked in turn, in reverse order. - A typical looper is \<^emph>\case splitting\: the expansion of a - conditional. Another possibility is to apply an elimination rule on - the assumptions. More adventurous loopers could start an induction. + A typical looper is \<^emph>\case splitting\: the expansion of a conditional. + Another possibility is to apply an elimination rule on the assumptions. More + adventurous loopers could start an induction. - \<^descr> \ctxt setloop tac\ installs \tac\ as the only - looper tactic of \ctxt\. + \<^descr> \ctxt setloop tac\ installs \tac\ as the only looper tactic of \ctxt\. - \<^descr> \ctxt addloop (name, tac)\ adds \tac\ as an - additional looper tactic with name \name\, which is - significant for managing the collection of loopers. The tactic will - be tried after the looper tactics that had already been present in - \ctxt\. + \<^descr> \ctxt addloop (name, tac)\ adds \tac\ as an additional looper tactic + with name \name\, which is significant for managing the collection of + loopers. The tactic will be tried after the looper tactics that had + already been present in \ctxt\. - \<^descr> \ctxt delloop name\ deletes the looper tactic that was - associated with \name\ from \ctxt\. + \<^descr> \ctxt delloop name\ deletes the looper tactic that was associated with + \name\ from \ctxt\. - \<^descr> @{ML Splitter.add_split}~\thm ctxt\ adds split tactics - for \thm\ as additional looper tactics of \ctxt\. + \<^descr> @{ML Splitter.add_split}~\thm ctxt\ adds split tactics for \thm\ as + additional looper tactics of \ctxt\. - \<^descr> @{ML Splitter.del_split}~\thm ctxt\ deletes the split - tactic corresponding to \thm\ from the looper tactics of - \ctxt\. + \<^descr> @{ML Splitter.del_split}~\thm ctxt\ deletes the split tactic + corresponding to \thm\ from the looper tactics of \ctxt\. - - The splitter replaces applications of a given function; the - right-hand side of the replacement can be anything. For example, - here is a splitting rule for conditional expressions: + The splitter replaces applications of a given function; the right-hand side + of the replacement can be anything. For example, here is a splitting rule + for conditional expressions: @{text [display] "?P (if ?Q ?x ?y) \ (?Q \ ?P ?x) \ (\ ?Q \ ?P ?y)"} - Another example is the elimination operator for Cartesian products - (which happens to be called @{const case_prod} in Isabelle/HOL: + Another example is the elimination operator for Cartesian products (which + happens to be called @{const case_prod} in Isabelle/HOL: @{text [display] "?P (case_prod ?f ?p) \ (\a b. ?p = (a, b) \ ?P (f a b))"} - For technical reasons, there is a distinction between case splitting - in the conclusion and in the premises of a subgoal. The former is - done by @{ML Splitter.split_tac} with rules like @{thm [source] - if_split} or @{thm [source] option.split}, which do not split the - subgoal, while the latter is done by @{ML Splitter.split_asm_tac} - with rules like @{thm [source] if_split_asm} or @{thm [source] - option.split_asm}, which split the subgoal. The function @{ML - Splitter.add_split} automatically takes care of which tactic to - call, analyzing the form of the rules given as argument; it is the - same operation behind \split\ attribute or method modifier - syntax in the Isar source language. + For technical reasons, there is a distinction between case splitting in the + conclusion and in the premises of a subgoal. The former is done by @{ML + Splitter.split_tac} with rules like @{thm [source] if_split} or @{thm + [source] option.split}, which do not split the subgoal, while the latter is + done by @{ML Splitter.split_asm_tac} with rules like @{thm [source] + if_split_asm} or @{thm [source] option.split_asm}, which split the subgoal. + The function @{ML Splitter.add_split} automatically takes care of which + tactic to call, analyzing the form of the rules given as argument; it is the + same operation behind \split\ attribute or method modifier syntax in the + Isar source language. - Case splits should be allowed only when necessary; they are - expensive and hard to control. Case-splitting on if-expressions in - the conclusion is usually beneficial, so it is enabled by default in - Isabelle/HOL and Isabelle/FOL/ZF. + Case splits should be allowed only when necessary; they are expensive and + hard to control. Case-splitting on if-expressions in the conclusion is + usually beneficial, so it is enabled by default in Isabelle/HOL and + Isabelle/FOL/ZF. \begin{warn} - With @{ML Splitter.split_asm_tac} as looper component, the - Simplifier may split subgoals! This might cause unexpected problems - in tactic expressions that silently assume 0 or 1 subgoals after - simplification. + With @{ML Splitter.split_asm_tac} as looper component, the Simplifier may + split subgoals! This might cause unexpected problems in tactic expressions + that silently assume 0 or 1 subgoals after simplification. \end{warn} \ @@ -1123,18 +1083,17 @@ opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use') ')' \} - \<^descr> @{attribute simplified}~\a\<^sub>1 \ a\<^sub>n\ causes a theorem to - be simplified, either by exactly the specified rules \a\<^sub>1, \, - a\<^sub>n\, or the implicit Simplifier context if no arguments are given. - The result is fully simplified by default, including assumptions and - conclusion; the options \no_asm\ etc.\ tune the Simplifier in - the same way as the for the \simp\ method. + \<^descr> @{attribute simplified}~\a\<^sub>1 \ a\<^sub>n\ causes a theorem to be simplified, + either by exactly the specified rules \a\<^sub>1, \, a\<^sub>n\, or the implicit + Simplifier context if no arguments are given. The result is fully simplified + by default, including assumptions and conclusion; the options \no_asm\ etc.\ + tune the Simplifier in the same way as the for the \simp\ method. - Note that forward simplification restricts the Simplifier to its - most basic operation of term rewriting; solver and looper tactics - (\secref{sec:simp-strategies}) are \<^emph>\not\ involved here. The - @{attribute simplified} attribute should be only rarely required - under normal circumstances. + Note that forward simplification restricts the Simplifier to its most basic + operation of term rewriting; solver and looper tactics + (\secref{sec:simp-strategies}) are \<^emph>\not\ involved here. The @{attribute + simplified} attribute should be only rarely required under normal + circumstances. \