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

author | wenzelm |

Sat, 03 Nov 2012 21:31:40 +0100 | |

changeset 50063 | 7e491da6bcbd |

parent 50062 | e038198f7d08 |

child 50064 | e08cc8b20564 |

more on the Simplifier, based on old material;

src/Doc/IsarRef/Generic.thy | file | annotate | diff | comparison | revisions | |

src/Doc/Ref/document/simplifier.tex | file | annotate | diff | comparison | revisions |

--- a/src/Doc/IsarRef/Generic.thy Sat Nov 03 19:07:07 2012 +0100 +++ b/src/Doc/IsarRef/Generic.thy Sat Nov 03 21:31:40 2012 +0100 @@ -377,7 +377,22 @@ section {* The Simplifier \label{sec:simplifier} *} -subsection {* Simplification methods *} +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 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. *} + + +subsection {* Simplification methods \label{sec:simp-meth} *} text {* \begin{matharray}{rcl} @@ -391,21 +406,34 @@ opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use' | 'asm_lr' ) ')' ; - @{syntax_def simpmod}: ('add' | 'del' | 'only' | 'cong' (() | 'add' | 'del') | - 'split' (() | 'add' | 'del')) ':' @{syntax thmrefs} + @{syntax_def simpmod}: ('add' | 'del' | 'only' | 'split' (() | 'add' | 'del') | + 'cong' (() | 'add' | 'del')) ':' @{syntax thmrefs} "} \begin{description} - \item @{method simp} invokes the Simplifier, after declaring - additional rules according to the arguments given. Note that the - @{text only} modifier first removes all other rewrite rules, - congruences, and looper tactics (including splits), and then behaves - like @{text add}. + \item @{method simp} invokes the Simplifier on the first subgoal, + after inserting chained facts as additional goal premises; further + rule declarations may be included via @{text "(simp add: facts)"}. + The proof method fails if the subgoal remains unchanged after + simplification. - \medskip The @{text cong} modifiers add or delete Simplifier - congruence rules (see also \secref{sec:simp-cong}), the default is - to add. + Note that the original goal premises and chained facts are subject + to simplification themselves, while declarations via @{text + "add"}/@{text "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 @{text only} modifier first removes all other rewrite + rules, looper tactics (including split rules), congruence rules, and + then behaves like @{text add}. Implicit solvers remain, which means + that trivial rules like reflexivity or introduction of @{text + "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 @{text split} modifiers add or delete rules for the Splitter (see also \cite{isabelle-ref}), the default is to add. @@ -413,36 +441,60 @@ include the Splitter (all major object logics such HOL, HOLCF, FOL, ZF do this already). + \medskip The @{text cong} modifiers add or delete Simplifier + congruence rules (see also \secref{sec:simp-rules}); the default is + to add. + \item @{method simp_all} is similar to @{method simp}, but acts on - all goals (backwards from the last to the first one). + 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}. + + The proof method fails if all subgoals remain unchanged after + simplification. \end{description} - By default the Simplifier methods take local assumptions fully into - account, using equational assumptions in the subsequent - normalization process, or simplifying assumptions themselves (cf.\ - @{ML asm_full_simp_tac} in \cite{isabelle-ref}). In structured - proofs this is usually quite well behaved in practice: just the - local premises of the actual goal are involved, additional facts may - be inserted via explicit forward-chaining (via @{command "then"}, - @{command "from"}, @{command "using"} etc.). + 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 + \begin{tabular}{|l|l|p{0.3\textwidth}|} + \hline + Isar method & ML tactic & behavior \\\hline + + @{text "(simp (no_asm))"} & @{ML simp_tac} & assumptions are ignored + completely \\\hline - Additional Simplifier options may be specified to tune the behavior - further (mostly for unstructured scripts with many accidental local - facts): ``@{text "(no_asm)"}'' means assumptions are ignored - completely (cf.\ @{ML simp_tac}), ``@{text "(no_asm_simp)"}'' means - assumptions are used in the simplification of the conclusion but are - not themselves simplified (cf.\ @{ML asm_simp_tac}), and ``@{text - "(no_asm_use)"}'' means assumptions are simplified but are not used - in the simplification of each other or the conclusion (cf.\ @{ML - full_simp_tac}). For compatibility reasons, there is also an option - ``@{text "(asm_lr)"}'', which means that an assumption is only used - for simplifying assumptions which are to the right of it (cf.\ @{ML - asm_lr_simp_tac}). + @{text "(simp (no_asm_simp))"} & @{ML asm_simp_tac} & assumptions + are used in the simplification of the conclusion but are not + themselves simplified \\\hline + + @{text "(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 - The configuration option @{text "depth_limit"} limits the number of - recursive invocations of the simplifier during conditional - rewriting. + @{text "(simp)"} & @{ML asm_full_simp_tac} & assumptions are used in + the simplification of the conclusion and to simplify other + assumptions \\\hline + + @{text "(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} \medskip The Splitter package is usually configured to work as part of the Simplifier. The effect of repeatedly applying @{ML @@ -452,51 +504,45 @@ *} -subsection {* Declaring rules *} +subsection {* Declaring rules \label{sec:simp-rules} *} text {* \begin{matharray}{rcl} @{command_def "print_simpset"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ @{attribute_def simp} & : & @{text attribute} \\ @{attribute_def split} & : & @{text attribute} \\ + @{attribute_def cong} & : & @{text attribute} \\ \end{matharray} @{rail " - (@@{attribute simp} | @@{attribute split}) (() | 'add' | 'del') + (@@{attribute simp} | @@{attribute split} | @@{attribute cong}) + (() | 'add' | 'del') "} \begin{description} \item @{command "print_simpset"} prints the collection of rules declared to the Simplifier, which is also known as ``simpset'' - internally \cite{isabelle-ref}. + internally. + + 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. \item @{attribute simp} declares simplification rules. \item @{attribute split} declares case split rules. - \end{description} -*} - - -subsection {* Congruence rules\label{sec:simp-cong} *} - -text {* - \begin{matharray}{rcl} - @{attribute_def cong} & : & @{text attribute} \\ - \end{matharray} - - @{rail " - @@{attribute cong} (() | 'add' | 'del') - "} - - \begin{description} - \item @{attribute cong} declares congruence rules to the Simplifier context. - \end{description} - 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"} @@ -532,10 +578,47 @@ 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 @{text "?q"} to prove the goal. + + \end{description} *} -subsection {* Simplification procedures *} +subsection {* Configuration options \label{sec:simp-config} *} + +text {* + \begin{tabular}{rcll} + @{attribute_def simp_depth_limit} & : & @{text attribute} & default @{text 100} \\ + @{attribute_def simp_trace} & : & @{text attribute} & default @{text false} \\ + @{attribute_def simp_trace_depth_limit} & : & @{text attribute} & default @{text 1} \\ + @{attribute_def simp_debug} & : & @{text attribute} & default @{text false} \\ + \end{tabular} + \medskip + + These configurations options control further aspects of the Simplifier. + See also \secref{sec:config}. + + \begin{description} + + \item @{attribute simp_depth_limit} limits the number of recursive + invocations of the Simplifier during conditional rewriting. + + \item @{attribute simp_trace} makes the Simplifier output internal + operations. This includes rewrite steps, but also bookkeeping like + modifications of the simpset. + + \item @{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). + + \item @{attribute simp_debug} makes the Simplifier output some extra + information about internal operations. This includes any attempted + invocation of simplification procedures. + + \end{description} +*} + + +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 @@ -616,7 +699,7 @@ reasonably fast. *} -subsection {* Forward simplification *} +subsection {* Forward simplification \label{sec:simp-forward} *} text {* \begin{matharray}{rcl}

--- a/src/Doc/Ref/document/simplifier.tex Sat Nov 03 19:07:07 2012 +0100 +++ b/src/Doc/Ref/document/simplifier.tex Sat Nov 03 21:31:40 2012 +0100 @@ -3,42 +3,16 @@ \label{chap:simplification} \index{simplification|(} -This chapter describes Isabelle's generic simplification package. It performs -conditional and unconditional rewriting and uses contextual information -(`local assumptions'). It provides several general hooks, which can provide -automatic case splits during rewriting, for example. The simplifier is -already set up for many of Isabelle's logics: FOL, ZF, HOL, HOLCF. - -The first section is a quick introduction to the simplifier that -should be sufficient to get started. The later sections explain more -advanced features. - \section{Simplification for dummies} \label{sec:simp-for-dummies} -Basic use of the simplifier is particularly easy because each theory -is equipped with sensible default information controlling the rewrite -process --- namely the implicit {\em current - simpset}\index{simpset!current}. A suite of simple commands is -provided that refer to the implicit simpset of the current theory -context. - -\begin{warn} - Make sure that you are working within the correct theory context. - Executing proofs interactively, or loading them from ML files - without associated theories may require setting the current theory - manually via the \ttindex{context} command. -\end{warn} - \subsection{Simplification tactics} \label{sec:simp-for-dummies-tacs} \begin{ttbox} Simp_tac : int -> tactic Asm_simp_tac : int -> tactic Full_simp_tac : int -> tactic Asm_full_simp_tac : int -> tactic -trace_simp : bool ref \hfill{\bf initially false} -debug_simp : bool ref \hfill{\bf initially false} \end{ttbox} \begin{ttdescription} @@ -60,12 +34,6 @@ \footnote{\texttt{Asm_full_simp_tac} used to process the assumptions from left to right. For backwards compatibilty reasons only there is now \texttt{Asm_lr_simp_tac} that behaves like the old \texttt{Asm_full_simp_tac}.} -\item[set \ttindexbold{trace_simp};] makes the simplifier output internal - operations. This includes rewrite steps, but also bookkeeping like - modifications of the simpset. -\item[set \ttindexbold{debug_simp};] makes the simplifier output some extra - information about internal operations. This includes any attempted - invocation of simplification procedures. \end{ttdescription} \medskip @@ -122,14 +90,6 @@ \end{ttbox} terminates. -\medskip - -Using the simplifier effectively may take a bit of experimentation. -Set the \verb$trace_simp$\index{tracing!of simplification} flag to get -a better idea of what is going on. The resulting output can be -enormous, especially since invocations of the simplifier are often -nested (e.g.\ when solving conditions of rewrite rules). - \subsection{Modifying the current simpset} \begin{ttbox}