Quelle  simp.thy

(*<*)
theory simp imports Main begin
(*>*)

subsection‹Simplification Rules›

text‹\index{simplification rules}
  facilitate simplification,
  attribute ‹[simp]›\index{*simp (attribute)}
  theorems to be simplification rules, which the simplifier
  use automatically. In addition, \isacommand{datatype} and
 isacommand{primrec} declarations (and a few others)
  declare some simplification rules.
  definitions are \emph{not} declared as
  rules automatically!

  any theorem can become a simplification
 . The simplifier will try to transform it into an equation.
  example, the theorem
 prop‹~P› is turned into prop‹P = False›. The details
  explained in \S\ref{sec:SimpHow}.

  simplification attribute of theorems can be turned on and off:%
 index{*simp del (attribute)}
 begin{quote}
 isacommand{declare} \textit{theorem-name}‹[simp]›\\
 isacommand{declare} \textit{theorem-name}‹[simp del]›
 end{quote}
java.lang.NullPointerException: Cannot invoke "String.equals(Object)" because "macro" is null
 \isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs} and
java.lang.NullPointerException: Cannot invoke "String.equals(Object)" because "macro" is null
 \isacharequal}\ xs}, should be declared as default simplification rules.
  specific ones should only be used selectively and should
  be made default. Distributivity laws, for example, alter
  structure of terms and can produce an exponential blow-up instead of
 . A default simplification rule may
  to be disabled in certain proofs. Frequent changes in the simplification
  of a theorem may indicate an unwise use of defaults.
 begin{warn}
 Simplification can run forever, for example if both $f(x) = g(x)$ and
 $g(x) = f(x)$ are simplification rules. It is the user's responsibility not
 to include simplification rules that can lead to nontermination, either on
 their own or in combination with other simplification rules.
 end{warn}
 begin{warn}
 It is inadvisable to toggle the simplification attribute of a
 theorem from a parent theory $A$ in a child theory $B$ for good.
 The reason is that if some theory $C$ is based both on $B$ and (via a
 different path) on $A$, it is not defined what the simplification attribute
 of that theorem will be in $C$: it could be either.
 end{warn}
 ›

subsection‹The {\tt\slshape simp} Method›

text‹\index{*simp (method)|bold}
  general format of the simplification method is
 begin{quote}
 ‹simp› \textit{list of modifiers}
 end{quote}
  the list of \emph{modifiers} fine tunes the behaviour and may
  empty. Specific modifiers are discussed below. Most if not all of the
  seen so far could have been performed
  ‹simp› instead of \isa{auto}, except that ‹simp› attacks
  the first subgoal and may thus need to be repeated --- use
 methdx{simp_all} to simplify all subgoals.
  nothing changes, ‹simp› fails.
 ›

subsection‹Adding and Deleting Simplification Rules›

text‹
 index{simplification rules!adding and deleting}%
  a certain theorem is merely needed in a few proofs by simplification,
  do not need to make it a global simplification rule. Instead we can modify
  set of simplification rules used in a simplification step by adding rules
  it and/or deleting rules from it. The two modifiers for this are
 begin{quote}
 ‹add:› \textit{list of theorem names}\index{*add (modifier)}\\
 ‹del:› \textit{list of theorem names}\index{*del (modifier)}
 end{quote}
  you can use a specific list of theorems and omit all others:
 begin{quote}
 ‹only:› \textit{list of theorem names}\index{*only (modifier)}
 end{quote}
  this example, we invoke the simplifier, adding two distributive
 :
 begin{quote}
 isacommand{apply}‹(simp add: mod_mult_distrib add_mult_distrib)›
 end{quote}
 ›

subsection‹Assumptions›

text‹\index{simplification!with/of assumptions}
  default, assumptions are part of the simplification process: they are used
  simplification rules and are simplified themselves. For example:
 ›

lemma "[ xs @ zs = ys @ xs; [] @ xs = [] @ [] ] ==> ys = zs"
apply simp
done

text‹\noindent
  second assumption simplifies to term‹xs = []›, which in turn
  the first assumption to term‹zs = ys›, thus reducing the
  to term‹ys = ys› and hence to term‹True›.

  some cases, using the assumptions can lead to nontermination:
 ›

lemma "∀x. f x = g (f (g x)) ==> f [] = f [] @ []"

txt‹\noindent
  unmodified application of ‹simp› loops. The culprit is the
  rule term‹f x = g (f (g x))›, which is extracted from
  assumption. (Isabelle notices certain simple forms of
  but not this one.) The problem can be circumvented by
  the simplifier to ignore the assumptions:
 ›

apply(simp (no_asm))
done

text‹\noindent
  modifiers influence the treatment of assumptions:
 begin{description}
 item[‹(no_asm)›]\index{*no_asm (modifier)}
 means that assumptions are completely ignored.
 item[‹(no_asm_simp)›]\index{*no_asm_simp (modifier)}
 means that the assumptions are not simplified but
 are used in the simplification of the conclusion.
 item[‹(no_asm_use)›]\index{*no_asm_use (modifier)}
 means that the assumptions are simplified but are not
 used in the simplification of each other or the conclusion.
 end{description}
  one of the modifiers is allowed, and it must precede all
  modifiers.
 \begin{warn}
 Assumptions are simplified in a left-to-right fashion. If an
 assumption can help in simplifying one to the left of it, this may get
 overlooked. In such cases you have to rotate the assumptions explicitly:
 \isacommand{apply}@ {text"("}\methdx{rotate_tac}~$n$@ {text")"}
 causes a cyclic shift by $n$ positions from right to left, if $n$ is
 positive, and from left to right, if $n$ is negative.
 Beware that such rotations make proofs quite brittle.
 \end{warn}
 ›

subsection‹Rewriting with Definitions›

text‹\label{sec:Simp-with-Defs}\index{simplification!with definitions}
  definitions (\S\ref{sec:ConstDefinitions}) can be used as
  rules, but by default they are not: the simplifier does not
  them automatically. Definitions are intended for introducing abstract
  and not merely as abbreviations. Of course, we need to expand
  definition initially, but once we have proved enough abstract properties
  the new constant, we can forget its original definition. This style makes
  more robust: if the definition has to be changed,
  the proofs of the abstract properties will be affected.

  example, given›

definition xor :: "bool ==> bool ==> bool" where
"xor A B ≡ (A ∧ ¬B) ∨ (¬A ∧ B)"

text‹\noindent
  may want to prove
 ›

lemma "xor A (¬A)"

txt‹\noindent
 , we begin by unfolding some definitions:
 indexbold{definitions!unfolding}
 ›

apply(simp only: xor_def)

txt‹\noindent
  this particular case, the resulting goal
 {subgoals[display,indent=0]}
  be proved by simplification. Thus we could have proved the lemma outright by
\<close>(*<*)oops lemma "xor A (¬A)"(*>*)
apply(simp add: xor_def)
(*<*)done(*>*)
text‹\noindent
  course we can also unfold definitions in the middle of a proof.

 begin{warn}
 If you have defined $f\,x\,y~\isasymequiv~t$ then you can only unfold
 occurrences of $f$ with at least two arguments. This may be helpful for unfolding
 $f$ selectively, but it may also get in the way. Defining
 $f$~\isasymequiv~\isasymlambda$x\,y.\;t$ allows to unfold all occurrences of $f$.
 end{warn}

  is also the special method \isa{unfold}\index{*unfold (method)|bold}
  merely unfolds
  or several definitions, as in \isacommand{apply}\isa{(unfold xor_def)}.
  is can be useful in situations where \isa{simp} does too much.
 : \isa{unfold} acts on all subgoals!
 ›

subsection‹Simplifying {\tt\slshape let}-Expressions›

text‹\index{simplification!of \isa{let}-expressions}\index{*let expressions}%
  a goal containing \isa{let}-expressions almost invariably requires the
 ‹let›-con\-structs to be expanded at some point. Since
 ‹let›\ldots\isa{=}\ldots‹in›{\ldots} is just syntactic sugar for
  predefined constant term‹Let›, expanding ‹let›-constructs
  rewriting with \tdx{Let_def}:›

lemma "(let xs = [] in xs@ys@xs) = ys"
apply(simp add: Let_def)
done

text‹
 , in a particular context, there is no danger of a combinatorial explosion
  nested ‹let›s, you could even simplify with @{thm[source]Let_def} by
 :
 ›
declare Let_def [simp]

subsection‹Conditional Simplification Rules›

text‹
 index{conditional simplification rules}%
  far all examples of rewrite rules were equations. The simplifier also
  \emph{conditional} equations, for example
 ›

lemma hd_Cons_tl[simp]: "xs ≠ [] ==> hd xs # tl xs = xs"
apply(case_tac xs, simp, simp)
done

text‹\noindent
  the use of ``\ttindexboldpos{,}{$Isar}'' to string together a
  of methods. Assuming that the simplification rule
 term‹(rev xs = []) = (xs = [])›
  present as well,
  lemma below is proved by plain simplification:
 ›

lemma "xs ≠ [] ==> hd(rev xs) # tl(rev xs) = rev xs"
(*<*)
by(simp)
(*>*)
text‹\noindent
  conditional equation @{thm[source]hd_Cons_tl} above
  simplify term‹hd(rev xs) # tl(rev xs)› to term‹rev xs›
  the corresponding precondition term‹rev xs ~= []›
  to term‹xs ~= []›, which is exactly the local
  of the subgoal.
 ›


subsection‹Automatic Case Splits›

text‹\label{sec:AutoCaseSplits}\indexbold{case splits}%
  containing ‹if›-expressions\index{*if expressions!splitting of}
  usually proved by case
  on the boolean condition. Here is an example:
 ›

lemma "∀xs. if xs = [] then rev xs = [] else rev xs ≠ []"

txt‹\noindent
  goal can be split by a special method, \methdx{split}:
 ›

apply(split if_split)

txt‹\noindent
 {subgoals[display,indent=0]}
  \tdx{if_split} is a theorem that expresses splitting of
 ‹if›s. Because
  the ‹if›s is usually the right proof strategy, the
  does it automatically. Try \isacommand{apply}‹(simp)›
  the initial goal above.

  splitting idea generalizes from ‹if› to \sdx{case}.
  us simplify a case analysis over lists:\index{*list.split (theorem)}
\<close>(*<*)by simp(*>*)
lemma "(case xs of [] ==> zs | y#ys ==> y#(ys@zs)) = xs@zs"
apply(split list.split)
 
txt‹
 {subgoals[display,indent=0]}
  simplifier does not split
 ‹case›-expressions, as it does ‹if›-expressions,
  with recursive datatypes it could lead to nontermination.
 , the simplifier has a modifier
 ‹split›\index{*split (modifier)}
  adding splitting rules explicitly. The
  above can be proved in one step by
 ›
(*<*)oops
lemma "(case xs of [] ==> zs | y#ys ==> y#(ys@zs)) = xs@zs"
(*>*)
apply(simp split: list.split)
(*<*)done(*>*)
text‹\noindent
  \isacommand{apply}‹(simp)› alone will not succeed.

  datatype $t$ comes with a theorem
 t$‹.split› which can be declared to be a \bfindex{split rule} either
  as above, or by giving it the \attrdx{split} attribute globally:
 ›

declare list.split [split]

text‹\noindent
  ‹split› attribute can be removed with the ‹del› modifier,
  locally
 ›
(*<*)
lemma "dummy=dummy"
(*>*)
apply(simp split del: if_split)
(*<*)
oops
(*>*)
text‹\noindent
  globally:
 ›
declare list.split [split del]

text‹
  proofs typically perform splitting within ‹simp› rather than
  the ‹split› method. However, if a goal contains
  ‹if› and ‹case› expressions,
  ‹split› method can be
  in selectively exploring the effects of splitting.

  split rules shown above are intended to affect only the subgoal's
 . If you want to split an ‹if› or ‹case›-expression
  the assumptions, you have to apply \tdx{if_split_asm} or
 t$‹.split_asm›:›

lemma "if xs = [] then ys ≠ [] else ys = [] ==> xs @ ys ≠ []"
apply(split if_split_asm)

txt‹\noindent
  splitting the conclusion, this step creates two
  subgoals, which here can be solved by ‹simp_all›:
 {subgoals[display,indent=0]}
  you need to split both in the assumptions and the conclusion,
  $t$‹.splits› which subsumes $t$‹.split› and
 t$‹.split_asm›. Analogously, there is @{thm[source]if_splits}.

 begin{warn}
 The simplifier merely simplifies the condition of an
 \isa{if}\index{*if expressions!simplification of} but not the
 \isa{then} or \isa{else} parts. The latter are simplified only after the
 condition reduces to \isa{True} or \isa{False}, or after splitting. The
 same is true for \sdx{case}-expressions: only the selector is
 simplified at first, until either the expression reduces to one of the
 cases or it is split.
 end{warn}
 ›
(*<*)
by(simp_all)
(*>*)

subsection‹Tracing›
text‹\indexbold{tracing the simplifier}
  the simplifier effectively may take a bit of experimentation. Set the
  General flag \pgmenu{Isabelle} $>$ \pgmenu{Settings} $>$ \pgmenu{Trace Simplifier} to get a better idea of what is going on:
 ›

lemma "rev [a] = []"
apply(simp)
(*<*)oops(*>*)

text‹\noindent
  the following trace in Proof General's \pgmenu{Trace} buffer:

 begin{ttbox}\makeatother
 1]Applying instance of rewrite rule "List.rev.simps_2":
  (?x1 # ?xs1) \(\equiv\) rev ?xs1 @ [?x1]

 1]Rewriting:
  [a] \(\equiv\) rev [] @ [a]

 1]Applying instance of rewrite rule "List.rev.simps_1":
  [] \(\equiv\) []

 1]Rewriting:
  [] \(\equiv\) []

 1]Applying instance of rewrite rule "List.append.append_Nil":
 ] @ ?y \(\equiv\) ?y

 1]Rewriting:
 ] @ [a] \(\equiv\) [a]

 1]Applying instance of rewrite rule
 x2 # ?t1 = ?t1 \(\equiv\) False

 1]Rewriting:
 a] = [] \(\equiv\) False
 end{ttbox}
  trace lists each rule being applied, both in its general form and
  instance being used. The \texttt{[}$i$\texttt{]} in front (where
  $i$ is always \texttt{1}) indicates that we are inside the $i$th
  of the simplifier. Each attempt to apply a
  rule shows the rule followed by the trace of the
 recursive!) simplification of the conditions, the latter prefixed by
 texttt{[}$i+1$\texttt{]} instead of \texttt{[}$i$\texttt{]}.
  source of recursive invocations of the simplifier are
  of arithmetic formulae. By default, recursive invocations are not shown,
  must increase the trace depth via \pgmenu{Isabelle} $>$ \pgmenu{Settings} $>$ \pgmenu{Trace Simplifier Depth}.

  other hints about the simplifier's actions may appear.

  more complicated cases, the trace can be very lengthy. Thus it is
  to reset the \pgmenu{Trace Simplifier} flag after having
  the desired trace.
  this is easily forgotten (and may have the unpleasant effect of
  the interface with trace information), here is how you can switch
  trace on locally in a proof:›

(*<*)lemma "x=x"
(*>*)
using [[simp_trace=true]]
apply simp
(*<*)oops(*>*)

text‹\noindent
  the current proof, all simplifications in subsequent proof steps
  be traced, but the text reminds you to remove the \isa{using} clause
  it has done its job.›

subsection‹Finding Theorems\label{sec:find}›

text‹\indexbold{finding theorems}\indexbold{searching theorems}
 's large database of proved theorems
  a powerful search engine. Its chief limitation is
  restriction to the theories currently loaded.

 begin{pgnote}
  search engine is started by clicking on Proof General's \pgmenu{Find} icon.
  specify your search textually in the input buffer at the bottom
  the window.
 end{pgnote}

  simplest form of search finds theorems containing specified
 . A pattern can be any term (even
  single identifier). It may contain ``\texttt{\_}'', a wildcard standing
  any term. Here are some
 :
 begin{ttbox}
 
 _ # _ = _ # _"
 _ + _"
 _ * (_ - (_::nat))"
 end{ttbox}
  types, as shown in the last example,
  searches involving overloaded operators.

 begin{warn}
  use ``\texttt{\_}'' rather than variable names: searching for
 texttt{"x + y"} will usually not find any matching theorems
  they would need to contain \texttt{x} and~\texttt{y} literally.
  searching for infix operators, do not just type in the symbol,
  as~\texttt{+}, but a proper term such as \texttt{"_ + _"}.
  remark applies to more complicated syntaxes, too.
 end{warn}

  you are looking for rewrite rules (possibly conditional) that could
  some term, prefix the pattern with \texttt{simp:}.
 begin{ttbox}
 : "_ * (_ + _)"
 end{ttbox}
  finds \emph{all} equations---not just those with a \isa{simp} attribute---whose conclusion has the form
 {text[display]"_ * (_ + _) = …"}
  only finds equations that can simplify the given pattern
  the root, not somewhere inside: for example, equations of the form
 ‹_ + _ = …› do not match.

  may also search for theorems by name---you merely
  to specify a substring. For example, you could search for all
  theorems like this:
 begin{ttbox}
 : comm
 end{ttbox}
  retrieves all theorems whose name contains \texttt{comm}.

  criteria can also be negated by prefixing them with ``\texttt{-}''.
  example,
 begin{ttbox}
 name: List
 end{ttbox}
  theorems whose name does not contain \texttt{List}. You can use this
  exclude particular theories from the search: the long name of
  theorem contains the name of the theory it comes from.

 , different search criteria can be combined arbitrarily.
  effect is conjuctive: Find returns the theorems that satisfy all of
  criteria. For example,
 begin{ttbox}
 _ + _" -"_ - _" -simp: "_ * (_ + _)" name: assoc
 end{ttbox}
  for theorems containing plus but not minus, and which do not simplify
 mbox{‹_ * (_ + _)›} at the root, and whose name contains \texttt{assoc}.

  search criteria are explained in \S\ref{sec:find2}.

 begin{pgnote}
  General keeps a history of all your search expressions.
  you click on \pgmenu{Find}, you can use the arrow keys to scroll
  previous searches and just modify them. This saves you having
  type in lengthy expressions again and again.
 end{pgnote}
 ›
(*<*)
end
(*>*)