doc-src/TutorialI/fp.tex
changeset 9742 98d3ca2c18f7
parent 9721 7e51c9f3d5a0
child 9754 a123a64cadeb
equal deleted inserted replaced
9741:0502f06c2d29 9742:98d3ca2c18f7
   556 is proved by simplification, whereas the only slightly more complex
   556 is proved by simplification, whereas the only slightly more complex
   557 
   557 
   558 \input{Misc/document/arith4.tex}%
   558 \input{Misc/document/arith4.tex}%
   559 is not proved by simplification and requires \isa{arith}.
   559 is not proved by simplification and requires \isa{arith}.
   560 
   560 
   561 \subsubsection{Permutative rewrite rules}
       
   562 
       
   563 A rewrite rule is \textbf{permutative} if the left-hand side and right-hand
       
   564 side are the same up to renaming of variables.  The most common permutative
       
   565 rule is commutativity: $x+y = y+x$.  Another example is $(x-y)-z = (x-z)-y$.
       
   566 Such rules are problematic because once they apply, they can be used forever.
       
   567 The simplifier is aware of this danger and treats permutative rules
       
   568 separately. For details see~\cite{isabelle-ref}.
       
   569 
       
   570 \subsubsection{Tracing}
   561 \subsubsection{Tracing}
   571 \indexbold{tracing the simplifier}
   562 \indexbold{tracing the simplifier}
   572 
   563 
   573 {\makeatother\input{Misc/document/trace_simp.tex}}
   564 {\makeatother\input{Misc/document/trace_simp.tex}}
   574 
       
   575 \subsection{How it works}
       
   576 \label{sec:SimpHow}
       
   577 
       
   578 \subsubsection{Higher-order patterns}
       
   579 
       
   580 \subsubsection{Local assumptions}
       
   581 
       
   582 \subsubsection{The preprocessor}
       
   583 
   565 
   584 \index{simplification|)}
   566 \index{simplification|)}
   585 
   567 
   586 \section{Induction heuristics}
   568 \section{Induction heuristics}
   587 \label{sec:InductionHeuristics}
   569 \label{sec:InductionHeuristics}
   798 \input{Recdef/document/Nested0.tex}
   780 \input{Recdef/document/Nested0.tex}
   799 \input{Recdef/document/Nested1.tex}
   781 \input{Recdef/document/Nested1.tex}
   800 \input{Recdef/document/Nested2.tex}
   782 \input{Recdef/document/Nested2.tex}
   801 
   783 
   802 \index{*recdef|)}
   784 \index{*recdef|)}
   803 
       
   804 \section{Advanced induction techniques}
       
   805 \label{sec:advanced-ind}
       
   806 \input{Misc/document/AdvancedInd.tex}
       
   807 
       
   808 %\input{Datatype/document/Nested2.tex}