--- 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 \<open>The Simplifier \label{sec:simplifier}\<close>
-text \<open>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 \<open>
+ 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.
\<close>
@@ -288,69 +287,63 @@
'cong' (() | 'add' | 'del')) ':' @{syntax thmrefs}
\<close>}
- \<^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 \<open>(simp add: facts)\<close>.
- 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 \<open>(simp add: facts)\<close>. 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 \<open>add\<close>/\<open>del\<close> 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 \<open>add\<close>/\<open>del\<close> 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 \<open>only\<close> modifier first removes all other rewrite
- rules, looper tactics (including split rules), congruence rules, and
- then behaves like \<open>add\<close>. Implicit solvers remain, which means
- that trivial rules like reflexivity or introduction of \<open>True\<close> 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 \<open>only\<close> modifier first removes all other rewrite rules, looper tactics
+ (including split rules), congruence rules, and then behaves like \<open>add\<close>.
+ Implicit solvers remain, which means that trivial rules like reflexivity or
+ introduction of \<open>True\<close> 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 \<open>split\<close> 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 \<open>split\<close> 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
- \<open>(split thms)\<close> can be imitated by ``\<open>(simp only:
- split: thms)\<close>''.
+ single-step case splitting. The effect of repeatedly applying \<open>(split thms)\<close>
+ can be imitated by ``\<open>(simp only: split: thms)\<close>''.
\<^medskip>
- The \<open>cong\<close> modifiers add or delete Simplifier
- congruence rules (see also \secref{sec:simp-rules}); the default is
- to add.
+ The \<open>cong\<close> 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>\<open>The order is irrelevant for goals without
- schematic variables, so simplification might actually be performed
- in parallel here.\<close>
+ \<^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>\<open>The
+ order is irrelevant for goals without schematic variables, so simplification
+ might actually be performed in parallel here.\<close>
- 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>\<open>Unlike the corresponding Isar proof methods, the
- ML tactics do not insist in changing the goal state.\<close>
+ 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>\<open>Unlike the corresponding Isar proof
+ methods, the ML tactics do not insist in changing the goal state.\<close>
\begin{center}
\small
@@ -358,24 +351,21 @@
\hline
Isar method & ML tactic & behavior \\\hline
- \<open>(simp (no_asm))\<close> & @{ML simp_tac} & assumptions are ignored
- completely \\\hline
+ \<open>(simp (no_asm))\<close> & @{ML simp_tac} & assumptions are ignored completely
+ \\\hline
- \<open>(simp (no_asm_simp))\<close> & @{ML asm_simp_tac} & assumptions
- are used in the simplification of the conclusion but are not
- themselves simplified \\\hline
+ \<open>(simp (no_asm_simp))\<close> & @{ML asm_simp_tac} & assumptions are used in the
+ simplification of the conclusion but are not themselves simplified \\\hline
- \<open>(simp (no_asm_use))\<close> & @{ML full_simp_tac} & assumptions
- are simplified but are not used in the simplification of each other
- or the conclusion \\\hline
+ \<open>(simp (no_asm_use))\<close> & @{ML full_simp_tac} & assumptions are simplified but
+ are not used in the simplification of each other or the conclusion \\\hline
- \<open>(simp)\<close> & @{ML asm_full_simp_tac} & assumptions are used in
- the simplification of the conclusion and to simplify other
- assumptions \\\hline
+ \<open>(simp)\<close> & @{ML asm_full_simp_tac} & assumptions are used in the
+ simplification of the conclusion and to simplify other assumptions \\\hline
- \<open>(simp (asm_lr))\<close> & @{ML asm_lr_simp_tac} & compatibility
- mode: an assumption is only used for simplifying assumptions which
- are to the right of it \\\hline
+ \<open>(simp (asm_lr))\<close> & @{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 \<open>Examples\<close>
-text \<open>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 \<open>
+ 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}:
\<close>
lemma "0 + (x + 0) = x + 0 + 0" apply simp? oops
-text \<open>The above attempt \<^emph>\<open>fails\<close>, 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:\<close>
+text \<open>
+ The above attempt \<^emph>\<open>fails\<close>, 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:\<close>
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 \<open>
\<^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:
\<close>
lemma fixes x :: nat shows "x = 0 \<Longrightarrow> 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 \<open>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 \<open>
+ 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 "\<And>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 \<open>f
- ?x \<equiv> g (f (g ?x))\<close> 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 "\<And>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 \<open>f ?x \<equiv> g (f (g ?x))\<close> 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:
\<close>
lemma "(\<And>x::nat. f x = g (f (g x))) \<Longrightarrow> f 0 = f 0 + 0"
by (simp (no_asm))
-text \<open>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 \<open>
+ 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:
\<close>
@@ -451,26 +441,26 @@
text \<open>
\<^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) \<Longrightarrow> y = x \<Longrightarrow> f x = f y
- \<Longrightarrow> 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) \<Longrightarrow> y = x \<Longrightarrow> f x = f y \<Longrightarrow> Q"} gives rise to the infinite
+ reduction sequence
\[
\<open>P (f x)\<close> \stackrel{\<open>f x \<equiv> f y\<close>}{\longmapsto}
\<open>P (f y)\<close> \stackrel{\<open>y \<equiv> x\<close>}{\longmapsto}
\<open>P (f x)\<close> \stackrel{\<open>f x \<equiv> f y\<close>}{\longmapsto} \cdots
\]
- whereas applying the same to @{prop "y = x \<Longrightarrow> f x = f y \<Longrightarrow> P (f x) \<Longrightarrow>
- Q"} terminates (without solving the goal):
+ whereas applying the same to @{prop "y = x \<Longrightarrow> f x = f y \<Longrightarrow> P (f x) \<Longrightarrow> Q"}
+ terminates (without solving the goal):
\<close>
lemma "y = x \<Longrightarrow> f x = f y \<Longrightarrow> P (f x) \<Longrightarrow> Q"
apply simp
oops
-text \<open>See also \secref{sec:simp-trace} for options to enable
- Simplifier trace mode, which often helps to diagnose problems with
- rewrite systems.
+text \<open>
+ See also \secref{sec:simp-trace} for options to enable Simplifier trace
+ mode, which often helps to diagnose problems with rewrite systems.
\<close>
@@ -491,200 +481,191 @@
@@{command print_simpset} ('!'?)
\<close>}
- \<^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:
\<open>Suc ?m + ?n = ?m + Suc ?n\<close> \\
\<open>?P \<and> ?P \<longleftrightarrow> ?P\<close> \\
\<open>?A \<union> ?B \<equiv> {x. x \<in> ?A \<or> x \<in> ?B}\<close>
\<^medskip>
- Conditional rewrites such as \<open>?m < ?n \<Longrightarrow> ?m div ?n = 0\<close> are
- also permitted; the conditions can be arbitrary formulas.
+ Conditional rewrites such as \<open>?m < ?n \<Longrightarrow> ?m div ?n = 0\<close> are also permitted;
+ the conditions can be arbitrary formulas.
\<^medskip>
- Internally, all rewrite rules are translated into Pure
- equalities, theorems with conclusion \<open>lhs \<equiv> rhs\<close>. The
- simpset contains a function for extracting equalities from arbitrary
- theorems, which is usually installed when the object-logic is
- configured initially. For example, \<open>\<not> ?x \<in> {}\<close> could be
- turned into \<open>?x \<in> {} \<equiv> False\<close>. 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 \<open>lhs \<equiv> rhs\<close>. The simpset contains a function for extracting
+ equalities from arbitrary theorems, which is usually installed when the
+ object-logic is configured initially. For example, \<open>\<not> ?x \<in> {}\<close> could be
+ turned into \<open>?x \<in> {} \<equiv> False\<close>. 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 \<open>lhs\<close>
- term:
+ The Simplifier accepts the following formats for the \<open>lhs\<close> term:
- \<^enum> First-order patterns, considering the sublanguage of
- application of constant operators to variable operands, without
- \<open>\<lambda>\<close>-abstractions or functional variables.
- For example:
+ \<^enum> First-order patterns, considering the sublanguage of application of
+ constant operators to variable operands, without \<open>\<lambda>\<close>-abstractions or
+ functional variables. For example:
\<open>(?x + ?y) + ?z \<equiv> ?x + (?y + ?z)\<close> \\
\<open>f (f ?x ?y) ?z \<equiv> f ?x (f ?y ?z)\<close>
- \<^enum> Higher-order patterns in the sense of @{cite "nipkow-patterns"}.
- These are terms in \<open>\<beta>\<close>-normal form (this will always be the
- case unless you have done something strange) where each occurrence
- of an unknown is of the form \<open>?F x\<^sub>1 \<dots> x\<^sub>n\<close>, where the
- \<open>x\<^sub>i\<close> are distinct bound variables.
+ \<^enum> Higher-order patterns in the sense of @{cite "nipkow-patterns"}. These
+ are terms in \<open>\<beta>\<close>-normal form (this will always be the case unless you have
+ done something strange) where each occurrence of an unknown is of the form
+ \<open>?F x\<^sub>1 \<dots> x\<^sub>n\<close>, where the \<open>x\<^sub>i\<close> are distinct bound variables.
- For example, \<open>(\<forall>x. ?P x \<and> ?Q x) \<equiv> (\<forall>x. ?P x) \<and> (\<forall>x. ?Q x)\<close>
- or its symmetric form, since the \<open>rhs\<close> is also a
- higher-order pattern.
+ For example, \<open>(\<forall>x. ?P x \<and> ?Q x) \<equiv> (\<forall>x. ?P x) \<and> (\<forall>x. ?Q x)\<close> or its
+ symmetric form, since the \<open>rhs\<close> is also a higher-order pattern.
- \<^enum> Physical first-order patterns over raw \<open>\<lambda>\<close>-term
- structure without \<open>\<alpha>\<beta>\<eta>\<close>-equality; abstractions and bound
- variables are treated like quasi-constant term material.
+ \<^enum> Physical first-order patterns over raw \<open>\<lambda>\<close>-term structure without
+ \<open>\<alpha>\<beta>\<eta>\<close>-equality; abstractions and bound variables are treated like
+ quasi-constant term material.
- For example, the rule \<open>?f ?x \<in> range ?f = True\<close> rewrites the
- term \<open>g a \<in> range g\<close> to \<open>True\<close>, but will fail to
- match \<open>g (h b) \<in> range (\<lambda>x. g (h x))\<close>. However, offending
- subterms (in our case \<open>?f ?x\<close>, which is not a pattern) can
- be replaced by adding new variables and conditions like this: \<open>?y = ?f ?x \<Longrightarrow> ?y \<in> range ?f = True\<close> is acceptable as a conditional
- rewrite rule of the second category since conditions can be
- arbitrary terms.
+ For example, the rule \<open>?f ?x \<in> range ?f = True\<close> rewrites the term \<open>g a \<in>
+ range g\<close> to \<open>True\<close>, but will fail to match \<open>g (h b) \<in> range (\<lambda>x. g (h
+ x))\<close>. However, offending subterms (in our case \<open>?f ?x\<close>, which is not a
+ pattern) can be replaced by adding new variables and conditions like this:
+ \<open>?y = ?f ?x \<Longrightarrow> ?y \<in> range ?f = True\<close> 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]
"\<dots> \<Longrightarrow> f ?x\<^sub>1 \<dots> ?x\<^sub>n = f ?y\<^sub>1 \<dots> ?y\<^sub>n"}
- This controls the simplification of the arguments of \<open>f\<close>. For
- example, some arguments can be simplified under additional
- assumptions: @{text [display] "?P\<^sub>1 \<longleftrightarrow> ?Q\<^sub>1 \<Longrightarrow> (?Q\<^sub>1 \<Longrightarrow> ?P\<^sub>2 \<longleftrightarrow> ?Q\<^sub>2) \<Longrightarrow>
- (?P\<^sub>1 \<longrightarrow> ?P\<^sub>2) \<longleftrightarrow> (?Q\<^sub>1 \<longrightarrow> ?Q\<^sub>2)"}
+ This controls the simplification of the arguments of \<open>f\<close>. For example, some
+ arguments can be simplified under additional assumptions:
+ @{text [display]
+ "?P\<^sub>1 \<longleftrightarrow> ?Q\<^sub>1 \<Longrightarrow>
+ (?Q\<^sub>1 \<Longrightarrow> ?P\<^sub>2 \<longleftrightarrow> ?Q\<^sub>2) \<Longrightarrow>
+ (?P\<^sub>1 \<longrightarrow> ?P\<^sub>2) \<longleftrightarrow> (?Q\<^sub>1 \<longrightarrow> ?Q\<^sub>2)"}
- Given this rule, the Simplifier assumes \<open>?Q\<^sub>1\<close> and extracts
- rewrite rules from it when simplifying \<open>?P\<^sub>2\<close>. Such local
- assumptions are effective for rewriting formulae such as \<open>x =
- 0 \<longrightarrow> y + x = y\<close>.
+ Given this rule, the Simplifier assumes \<open>?Q\<^sub>1\<close> and extracts rewrite rules
+ from it when simplifying \<open>?P\<^sub>2\<close>. Such local assumptions are effective for
+ rewriting formulae such as \<open>x = 0 \<longrightarrow> y + x = y\<close>.
%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) \<Longrightarrow> (\<And>x. x \<in> ?B \<Longrightarrow> ?P x \<longleftrightarrow> ?Q x) \<Longrightarrow>
+ The following congruence rule for bounded quantifiers also supplies
+ contextual information --- about the bound variable: @{text [display]
+ "(?A = ?B) \<Longrightarrow>
+ (\<And>x. x \<in> ?B \<Longrightarrow> ?P x \<longleftrightarrow> ?Q x) \<Longrightarrow>
(\<forall>x \<in> ?A. ?P x) \<longleftrightarrow> (\<forall>x \<in> ?B. ?Q x)"}
\<^medskip>
- This congruence rule for conditional expressions can
- supply contextual information for simplifying the arms:
- @{text [display] "?p = ?q \<Longrightarrow> (?q \<Longrightarrow> ?a = ?c) \<Longrightarrow> (\<not> ?q \<Longrightarrow> ?b = ?d) \<Longrightarrow>
+ This congruence rule for conditional expressions can supply contextual
+ information for simplifying the arms: @{text [display]
+ "?p = ?q \<Longrightarrow>
+ (?q \<Longrightarrow> ?a = ?c) \<Longrightarrow>
+ (\<not> ?q \<Longrightarrow> ?b = ?d) \<Longrightarrow>
(if ?p then ?a else ?b) = (if ?q then ?c else ?d)"}
- A congruence rule can also \<^emph>\<open>prevent\<close> simplification of some
- arguments. Here is an alternative congruence rule for conditional
- expressions that conforms to non-strict functional evaluation:
- @{text [display] "?p = ?q \<Longrightarrow> (if ?p then ?a else ?b) = (if ?q then ?a else ?b)"}
+ A congruence rule can also \<^emph>\<open>prevent\<close> simplification of some arguments. Here
+ is an alternative congruence rule for conditional expressions that conforms
+ to non-strict functional evaluation: @{text [display]
+ "?p = ?q \<Longrightarrow>
+ (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 \<open>?q\<close> 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 \<open>?q\<close> 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
- ``\<open>!\<close>'' 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 ``\<open>!\<close>''
+ 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>\<open>not\<close> 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>\<open>not\<close> 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 \<open>?n + 0 \<equiv> ?n\<close> 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 \<open>?n + 0 \<equiv> ?n\<close> 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}
\<close>
subsection \<open>Ordered rewriting with permutative rules\<close>
-text \<open>A rewrite rule is \<^emph>\<open>permutative\<close> if the left-hand side and
- right-hand side are the equal up to renaming of variables. The most
- common permutative rule is commutativity: \<open>?x + ?y = ?y +
- ?x\<close>. Other examples include \<open>(?x - ?y) - ?z = (?x - ?z) -
- ?y\<close> in arithmetic and \<open>insert ?x (insert ?y ?A) = insert ?y
- (insert ?x ?A)\<close> for sets. Such rules are common enough to merit
- special attention.
+text \<open>
+ A rewrite rule is \<^emph>\<open>permutative\<close> if the left-hand side and right-hand side
+ are the equal up to renaming of variables. The most common permutative rule
+ is commutativity: \<open>?x + ?y = ?y + ?x\<close>. Other examples include \<open>(?x - ?y) -
+ ?z = (?x - ?z) - ?y\<close> in arithmetic and \<open>insert ?x (insert ?y ?A) = insert ?y
+ (insert ?x ?A)\<close> 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>\<open>ordered rewriting\<close>.
- Permutative rules are detected and only applied if the rewriting
- step decreases the redex wrt.\ a given term ordering. For example,
- commutativity rewrites \<open>b + a\<close> to \<open>a + b\<close>, 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>\<open>ordered rewriting\<close>. Permutative rules are
+ detected and only applied if the rewriting step decreases the redex wrt.\ a
+ given term ordering. For example, commutativity rewrites \<open>b + a\<close> to \<open>a + b\<close>,
+ 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.\<close>
+ 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.
+\<close>
subsubsection \<open>Rewriting with AC operators\<close>
-text \<open>Ordered rewriting is particularly effective in the case of
- associative-commutative operators. (Associativity by itself is not
- permutative.) When dealing with an AC-operator \<open>f\<close>, keep
- the following points in mind:
+text \<open>
+ Ordered rewriting is particularly effective in the case of
+ associative-commutative operators. (Associativity by itself is not
+ permutative.) When dealing with an AC-operator \<open>f\<close>, keep the following
+ points in mind:
- \<^item> The associative law must always be oriented from left to
- right, namely \<open>f (f x y) z = f x (f y z)\<close>. 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
+ \<open>f (f x y) z = f x (f y z)\<close>. 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>\<open>left-commutativity\<close> (LC): \<open>f x (f y z) = f y (f x z)\<close>.
-
+ \<^item> To complete your set of rewrite rules, you must add not just
+ associativity (A) and commutativity (C) but also a derived rule
+ \<^emph>\<open>left-commutativity\<close> (LC): \<open>f x (f y z) = f y (f x z)\<close>.
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 \<open>Thus the Simplifier is able to establish equalities with
- arbitrary permutations of subterms, by normalizing to a common
- standard form. For example:\<close>
+text \<open>
+ Thus the Simplifier is able to establish equalities with arbitrary
+ permutations of subterms, by normalizing to a common standard form. For
+ example:
+\<close>
lemma "(b \<bullet> c) \<bullet> a = xxx"
apply (simp only: AC_rules)
@@ -719,10 +702,11 @@
end
-text \<open>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 \<open>
+ 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.
\<close>
@@ -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 \<open>Simplification procedures \label{sec:simproc}\<close>
-text \<open>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 \<open>
+ 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 \<open>t \<equiv> u\<close> 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>\<open>internal form\<close>, bypassing the
- automatic preprocessing of object-level equivalences.
+ Any successful result needs to be a (possibly conditional) rewrite rule \<open>t \<equiv>
+ u\<close> 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>\<open>internal form\<close>,
+ bypassing the automatic preprocessing of object-level equivalences.
\begin{matharray}{rcl}
@{command_def "simproc_setup"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
@@ -829,40 +811,39 @@
@@{attribute simproc} (('add' ':')? | 'del' ':') (@{syntax name}+)
\<close>}
- \<^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 \<open>r\<close> and the result is
- supposed to be some proven rewrite rule \<open>r \<equiv> r'\<close> (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 \<open>r\<close> and the result is supposed
+ to be some proven rewrite rule \<open>r \<equiv> r'\<close> (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> \<open>simproc add: name\<close> and \<open>simproc del: name\<close>
- 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> \<open>simproc add: name\<close> and \<open>simproc del: name\<close> 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.
\<close>
subsubsection \<open>Example\<close>
-text \<open>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.\<close>
+text \<open>
+ 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.
+\<close>
(*<*)experiment begin(*>*)
simproc_setup unit ("x::unit") =
@@ -871,20 +852,20 @@
else SOME (mk_meta_eq @{thm unit_eq})\<close>
(*<*)end(*>*)
-text \<open>Since the Simplifier applies simplification procedures
- frequently, it is important to make the failure check in ML
- reasonably fast.\<close>
+text \<open>
+ Since the Simplifier applies simplification procedures frequently, it is
+ important to make the failure check in ML reasonably fast.\<close>
subsection \<open>Configurable Simplifier strategies \label{sec:simp-strategies}\<close>
-text \<open>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.\<close>
+text \<open>
+ 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.\<close>
subsubsection \<open>The subgoaler\<close>
@@ -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 \<open>Suc ?m < ?n \<Longrightarrow>
- ?m < ?n\<close>, 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 \<open>Suc ?m < ?n \<Longrightarrow> ?m < ?n\<close>, the default strategy could
+ loop. % FIXME !??
- \<^descr> @{ML Simplifier.set_subgoaler}~\<open>tac ctxt\<close> sets the
- subgoaler of the context to \<open>tac\<close>. The tactic will
- be applied to the context of the running Simplifier instance.
+ \<^descr> @{ML Simplifier.set_subgoaler}~\<open>tac ctxt\<close> sets the subgoaler of the
+ context to \<open>tac\<close>. The tactic will be applied to the context of the running
+ Simplifier instance.
- \<^descr> @{ML Simplifier.prems_of}~\<open>ctxt\<close> 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}~\<open>ctxt\<close> 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:
\<close>
@@ -923,9 +903,9 @@
asm_simp_tac ctxt
\<close>
-text \<open>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.\<close>
+text \<open>
+ 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.\<close>
subsubsection \<open>The solver\<close>
@@ -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 \<open>t = t\<close>, 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 \<open>t = t\<close>, 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 \<open>a \<in> ?A\<close> since this requires
- instantiating \<open>?A\<close>. 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 \<open>a \<in> ?A\<close> since this requires instantiating \<open>?A\<close>. 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}~\<open>name tac\<close> turns \<open>tac\<close> into a solver; the \<open>name\<close> 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> \<open>ctxt setSSolver solver\<close> installs \<open>solver\<close> as
- the safe solver of \<open>ctxt\<close>.
+ \<^descr> @{ML Simplifier.mk_solver}~\<open>name tac\<close> turns \<open>tac\<close> into a solver; the
+ \<open>name\<close> is only attached as a comment and has no further significance.
- \<^descr> \<open>ctxt addSSolver solver\<close> adds \<open>solver\<close> as an
- additional safe solver; it will be tried after the solvers which had
- already been present in \<open>ctxt\<close>.
+ \<^descr> \<open>ctxt setSSolver solver\<close> installs \<open>solver\<close> as the safe solver of \<open>ctxt\<close>.
- \<^descr> \<open>ctxt setSolver solver\<close> installs \<open>solver\<close> as the
- unsafe solver of \<open>ctxt\<close>.
+ \<^descr> \<open>ctxt addSSolver solver\<close> adds \<open>solver\<close> as an additional safe solver; it
+ will be tried after the solvers which had already been present in \<open>ctxt\<close>.
- \<^descr> \<open>ctxt addSolver solver\<close> adds \<open>solver\<close> as an
- additional unsafe solver; it will be tried after the solvers which
- had already been present in \<open>ctxt\<close>.
+ \<^descr> \<open>ctxt setSolver solver\<close> installs \<open>solver\<close> as the unsafe solver of \<open>ctxt\<close>.
+
+ \<^descr> \<open>ctxt addSolver solver\<close> adds \<open>solver\<close> as an additional unsafe solver; it
+ will be tried after the solvers which had already been present in \<open>ctxt\<close>.
\<^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
- \<open>s = ?x\<close>, where \<open>s\<close> needs to be simplified and
- \<open>?x\<close> 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 \<open>s = ?x\<close>, where \<open>s\<close> needs to
+ be simplified and \<open>?x\<close> 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 \<open>t = ?x\<close>, 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 \<open>t = ?x\<close>, 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, \<open>False \<longleftrightarrow> ?Q\<close> could be
- rewritten to \<open>\<not> ?Q\<close>. To cover this case, the solver could
- try resolving with the theorem \<open>\<not> False\<close> of the
+ It may even happen that due to simplification the subgoal is no longer an
+ equality. For example, \<open>False \<longleftrightarrow> ?Q\<close> could be rewritten to \<open>\<not> ?Q\<close>. To cover
+ this case, the solver could try resolving with the theorem \<open>\<not> False\<close> 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>\<open>conditional\<close> --- that is, contains premises not of the form
- \<open>t = ?x\<close>. 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>\<open>conditional\<close> --- that is,
+ contains premises not of the form \<open>t = ?x\<close>. Otherwise it indicates that some
+ congruence rule, or possibly the subgoaler or solver, is faulty.
\end{warn}
\<close>
@@ -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>\<open>case splitting\<close>: 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>\<open>case splitting\<close>: the expansion of a conditional.
+ Another possibility is to apply an elimination rule on the assumptions. More
+ adventurous loopers could start an induction.
- \<^descr> \<open>ctxt setloop tac\<close> installs \<open>tac\<close> as the only
- looper tactic of \<open>ctxt\<close>.
+ \<^descr> \<open>ctxt setloop tac\<close> installs \<open>tac\<close> as the only looper tactic of \<open>ctxt\<close>.
- \<^descr> \<open>ctxt addloop (name, tac)\<close> adds \<open>tac\<close> as an
- additional looper tactic with name \<open>name\<close>, which is
- significant for managing the collection of loopers. The tactic will
- be tried after the looper tactics that had already been present in
- \<open>ctxt\<close>.
+ \<^descr> \<open>ctxt addloop (name, tac)\<close> adds \<open>tac\<close> as an additional looper tactic
+ with name \<open>name\<close>, which is significant for managing the collection of
+ loopers. The tactic will be tried after the looper tactics that had
+ already been present in \<open>ctxt\<close>.
- \<^descr> \<open>ctxt delloop name\<close> deletes the looper tactic that was
- associated with \<open>name\<close> from \<open>ctxt\<close>.
+ \<^descr> \<open>ctxt delloop name\<close> deletes the looper tactic that was associated with
+ \<open>name\<close> from \<open>ctxt\<close>.
- \<^descr> @{ML Splitter.add_split}~\<open>thm ctxt\<close> adds split tactics
- for \<open>thm\<close> as additional looper tactics of \<open>ctxt\<close>.
+ \<^descr> @{ML Splitter.add_split}~\<open>thm ctxt\<close> adds split tactics for \<open>thm\<close> as
+ additional looper tactics of \<open>ctxt\<close>.
- \<^descr> @{ML Splitter.del_split}~\<open>thm ctxt\<close> deletes the split
- tactic corresponding to \<open>thm\<close> from the looper tactics of
- \<open>ctxt\<close>.
+ \<^descr> @{ML Splitter.del_split}~\<open>thm ctxt\<close> deletes the split tactic
+ corresponding to \<open>thm\<close> from the looper tactics of \<open>ctxt\<close>.
-
- 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) \<longleftrightarrow> (?Q \<longrightarrow> ?P ?x) \<and> (\<not> ?Q \<longrightarrow> ?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) \<longleftrightarrow> (\<forall>a b. ?p = (a, b) \<longrightarrow> ?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 \<open>split\<close> 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 \<open>split\<close> 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}
\<close>
@@ -1123,18 +1083,17 @@
opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use') ')'
\<close>}
- \<^descr> @{attribute simplified}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> causes a theorem to
- be simplified, either by exactly the specified rules \<open>a\<^sub>1, \<dots>,
- a\<^sub>n\<close>, or the implicit Simplifier context if no arguments are given.
- The result is fully simplified by default, including assumptions and
- conclusion; the options \<open>no_asm\<close> etc.\ tune the Simplifier in
- the same way as the for the \<open>simp\<close> method.
+ \<^descr> @{attribute simplified}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> causes a theorem to be simplified,
+ either by exactly the specified rules \<open>a\<^sub>1, \<dots>, a\<^sub>n\<close>, or the implicit
+ Simplifier context if no arguments are given. The result is fully simplified
+ by default, including assumptions and conclusion; the options \<open>no_asm\<close> etc.\
+ tune the Simplifier in the same way as the for the \<open>simp\<close> 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>\<open>not\<close> 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>\<open>not\<close> involved here. The @{attribute
+ simplified} attribute should be only rarely required under normal
+ circumstances.
\<close>