749 \ 1.\ \isasymlbrakk P\ x\ y\ z;\ Suc\ x\ <\ y\isasymrbrakk \ \isasymLongrightarrow \ f\ z\ =\ x\ *\ y% |
749 \ 1.\ \isasymlbrakk P\ x\ y\ z;\ Suc\ x\ <\ y\isasymrbrakk \ \isasymLongrightarrow \ f\ z\ =\ x\ *\ y% |
750 \end{isabelle} |
750 \end{isabelle} |
751 Now we wish to apply a commutative law: |
751 Now we wish to apply a commutative law: |
752 \begin{isabelle} |
752 \begin{isabelle} |
753 ?m\ *\ ?n\ =\ ?n\ *\ ?m% |
753 ?m\ *\ ?n\ =\ ?n\ *\ ?m% |
754 \rulename{mult_commute} |
754 \rulename{mult.commute} |
755 \end{isabelle} |
755 \end{isabelle} |
756 Isabelle rejects our first attempt: |
756 Isabelle rejects our first attempt: |
757 \begin{isabelle} |
757 \begin{isabelle} |
758 apply (simp add: mult_commute) |
758 apply (simp add: mult.commute) |
759 \end{isabelle} |
759 \end{isabelle} |
760 The simplifier notices the danger of looping and refuses to apply the |
760 The simplifier notices the danger of looping and refuses to apply the |
761 rule.% |
761 rule.% |
762 \footnote{More precisely, it only applies such a rule if the new term is |
762 \footnote{More precisely, it only applies such a rule if the new term is |
763 smaller under a specified ordering; here, \isa{x\ *\ y} |
763 smaller under a specified ordering; here, \isa{x\ *\ y} |
764 is already smaller than |
764 is already smaller than |
765 \isa{y\ *\ x}.} |
765 \isa{y\ *\ x}.} |
766 % |
766 % |
767 The \isa{subst} method applies \isa{mult_commute} exactly once. |
767 The \isa{subst} method applies \isa{mult.commute} exactly once. |
768 \begin{isabelle} |
768 \begin{isabelle} |
769 \isacommand{apply}\ (subst\ mult_commute)\isanewline |
769 \isacommand{apply}\ (subst\ mult.commute)\isanewline |
770 \ 1.\ \isasymlbrakk P\ x\ y\ z;\ Suc\ x\ <\ y\isasymrbrakk \ |
770 \ 1.\ \isasymlbrakk P\ x\ y\ z;\ Suc\ x\ <\ y\isasymrbrakk \ |
771 \isasymLongrightarrow \ f\ z\ =\ y\ *\ x% |
771 \isasymLongrightarrow \ f\ z\ =\ y\ *\ x% |
772 \end{isabelle} |
772 \end{isabelle} |
773 As we wanted, \isa{x\ *\ y} has become \isa{y\ *\ x}. |
773 As we wanted, \isa{x\ *\ y} has become \isa{y\ *\ x}. |
774 |
774 |
775 \medskip |
775 \medskip |
776 This use of the \methdx{subst} method has the same effect as the command |
776 This use of the \methdx{subst} method has the same effect as the command |
777 \begin{isabelle} |
777 \begin{isabelle} |
778 \isacommand{apply}\ (rule\ mult_commute [THEN ssubst]) |
778 \isacommand{apply}\ (rule\ mult.commute [THEN ssubst]) |
779 \end{isabelle} |
779 \end{isabelle} |
780 The attribute \isa{THEN}, which combines two rules, is described in |
780 The attribute \isa{THEN}, which combines two rules, is described in |
781 {\S}\ref{sec:THEN} below. The \methdx{subst} method is more powerful than |
781 {\S}\ref{sec:THEN} below. The \methdx{subst} method is more powerful than |
782 applying the substitution rule. It can perform substitutions in a subgoal's |
782 applying the substitution rule. It can perform substitutions in a subgoal's |
783 assumptions. Moreover, if the subgoal contains more than one occurrence of |
783 assumptions. Moreover, if the subgoal contains more than one occurrence of |
1984 |
1984 |
1985 %Answer is now included in that section! Is a modified version of this |
1985 %Answer is now included in that section! Is a modified version of this |
1986 % exercise worth including? E.g. find a difference between the two ways |
1986 % exercise worth including? E.g. find a difference between the two ways |
1987 % of substituting. |
1987 % of substituting. |
1988 %\begin{exercise} |
1988 %\begin{exercise} |
1989 %In {\S}\ref{sec:subst} the method \isa{subst\ mult_commute} was applied. How |
1989 %In {\S}\ref{sec:subst} the method \isa{subst\ mult.commute} was applied. How |
1990 %can we achieve the same effect using \isa{THEN} with the rule \isa{ssubst}? |
1990 %can we achieve the same effect using \isa{THEN} with the rule \isa{ssubst}? |
1991 %% answer rule (mult_commute [THEN ssubst]) |
1991 %% answer rule (mult.commute [THEN ssubst]) |
1992 %\end{exercise} |
1992 %\end{exercise} |
1993 |
1993 |
1994 \subsection{Modifying a Theorem using {\tt\slshape OF}} |
1994 \subsection{Modifying a Theorem using {\tt\slshape OF}} |
1995 |
1995 |
1996 \index{*OF (attribute)|(}% |
1996 \index{*OF (attribute)|(}% |