# HG changeset patch # User nipkow # Date 1117004664 -7200 # Node ID 3f2a9f40016837edbeacc466b9fc7d744c1f0a20 # Parent 0e7b145c3a89c1f5313e61c3e48343bb46ca5378 *** empty log message *** diff -r 0e7b145c3a89 -r 3f2a9f400168 doc-src/TutorialI/Advanced/document/Partial.tex --- a/doc-src/TutorialI/Advanced/document/Partial.tex Wed May 25 09:03:53 2005 +0200 +++ b/doc-src/TutorialI/Advanced/document/Partial.tex Wed May 25 09:04:24 2005 +0200 @@ -150,7 +150,7 @@ \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline \ \ {\isachardoublequote}wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\ {\isasymLongrightarrow}\ find{\isacharparenleft}f{\isacharcomma}x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ f\ x\ {\isacharequal}\ x\ then\ x\ else\ find{\isacharparenleft}f{\isacharcomma}\ f\ x{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{by}\ simp\isamarkupfalse% % \begin{isamarkuptext}% \noindent Then you should disable the original recursion equation:% @@ -165,9 +165,11 @@ \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\ {\isasymlongrightarrow}\ f{\isacharparenleft}find{\isacharparenleft}f{\isacharcomma}x{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ find{\isacharparenleft}f{\isacharcomma}x{\isacharparenright}{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ f\ x\ rule{\isacharcolon}\ find{\isachardot}induct{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{apply}\ simp\isanewline \isamarkupfalse% +\isacommand{done}\isamarkupfalse% % \isamarkupsubsubsection{The {\tt\slshape while} Combinator% } @@ -229,10 +231,14 @@ \ \ {\isasymexists}y{\isachardot}\ while\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}x{\isacharprime}{\isacharparenright}{\isachardot}\ x{\isacharprime}\ {\isasymnoteq}\ x{\isacharparenright}\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}x{\isacharprime}{\isacharparenright}{\isachardot}\ {\isacharparenleft}x{\isacharprime}{\isacharcomma}f\ x{\isacharprime}{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}x{\isacharcomma}f\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}y{\isacharparenright}\ {\isasymand}\isanewline \ \ \ \ \ \ \ f\ y\ {\isacharequal}\ y{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ P\ {\isacharequal}\ {\isachardoublequote}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}x{\isacharprime}{\isacharparenright}{\isachardot}\ x{\isacharprime}\ {\isacharequal}\ f\ x{\isachardoublequote}\ \isakeyword{and}\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ r\ {\isacharequal}\ {\isachardoublequote}inv{\isacharunderscore}image\ {\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\ fst{\isachardoublequote}\ \isakeyword{in}\ while{\isacharunderscore}rule{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{apply}\ auto\isanewline \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ inv{\isacharunderscore}image{\isacharunderscore}def\ step{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{done}\isamarkupfalse% % \begin{isamarkuptext}% The theorem itself is a simple consequence of this lemma:% @@ -240,9 +246,11 @@ \isamarkuptrue% \isacommand{theorem}\ {\isachardoublequote}wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\ {\isasymLongrightarrow}\ f{\isacharparenleft}find{\isadigit{2}}\ f\ x{\isacharparenright}\ {\isacharequal}\ find{\isadigit{2}}\ f\ x{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}drule{\isacharunderscore}tac\ x\ {\isacharequal}\ x\ \isakeyword{in}\ lem{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ find{\isadigit{2}}{\isacharunderscore}def{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{done}\isamarkupfalse% % \begin{isamarkuptext}% Let us conclude this section on partial functions by a diff -r 0e7b145c3a89 -r 3f2a9f400168 doc-src/TutorialI/Advanced/document/WFrec.tex --- a/doc-src/TutorialI/Advanced/document/WFrec.tex Wed May 25 09:03:53 2005 +0200 +++ b/doc-src/TutorialI/Advanced/document/WFrec.tex Wed May 25 09:04:24 2005 +0200 @@ -85,12 +85,37 @@ \end{isamarkuptext}% \isamarkuptrue% \isacommand{lemma}\ wf{\isacharunderscore}greater{\isacharcolon}\ {\isachardoublequote}wf\ {\isacharbraceleft}{\isacharparenleft}i{\isacharcomma}j{\isacharparenright}{\isachardot}\ j{\isacharless}i\ {\isasymand}\ i\ {\isasymle}\ {\isacharparenleft}N{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharbraceright}{\isachardoublequote}\isamarkupfalse% -\isamarkuptrue% -\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +The proof is by showing that our relation is a subset of another well-founded +relation: one given by a measure function.\index{*wf_subset (theorem)}% +\end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% +\isacommand{apply}\ {\isacharparenleft}rule\ wf{\isacharunderscore}subset\ {\isacharbrackleft}of\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}k{\isacharcolon}{\isacharcolon}nat{\isachardot}\ N{\isacharminus}k{\isacharparenright}{\isachardoublequote}{\isacharbrackright}{\isacharcomma}\ blast{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isacharbraceleft}{\isacharparenleft}i{\isacharcomma}\ j{\isacharparenright}{\isachardot}\ j\ {\isacharless}\ i\ {\isasymand}\ i\ {\isasymle}\ N{\isacharbraceright}\ {\isasymsubseteq}\ measure\ {\isacharparenleft}op\ {\isacharminus}\ N{\isacharparenright}% +\end{isabelle} + +\noindent +The inclusion remains to be proved. After unfolding some definitions, +we are left with simple arithmetic:% +\end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% +\isacommand{apply}\ {\isacharparenleft}clarify{\isacharcomma}\ simp\ add{\isacharcolon}\ measure{\isacharunderscore}def\ inv{\isacharunderscore}image{\isacharunderscore}def{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ b{\isachardot}\ {\isasymlbrakk}b\ {\isacharless}\ a{\isacharsemicolon}\ a\ {\isasymle}\ N{\isasymrbrakk}\ {\isasymLongrightarrow}\ N\ {\isacharminus}\ a\ {\isacharless}\ N\ {\isacharminus}\ b% +\end{isabelle} + +\noindent +And that is dispatched automatically:% +\end{isamarkuptxt}% +\isamarkuptrue% +\isacommand{by}\ arith\isamarkupfalse% % \begin{isamarkuptext}% \noindent diff -r 0e7b145c3a89 -r 3f2a9f400168 doc-src/TutorialI/CTL/CTL.thy --- a/doc-src/TutorialI/CTL/CTL.thy Wed May 25 09:03:53 2005 +0200 +++ b/doc-src/TutorialI/CTL/CTL.thy Wed May 25 09:04:24 2005 +0200 @@ -244,7 +244,7 @@ automatically. This is what happens in the step case. The induction step is similar, but more involved, because now we face nested -occurrences of @{const SOME}. As a result, @{text fast} is no longer able to +occurrences of @{text SOME}. As a result, @{text fast} is no longer able to solve the subgoal and we apply @{thm[source]someI2_ex} by hand. We merely show the proof commands but do not describe the details: *}; diff -r 0e7b145c3a89 -r 3f2a9f400168 doc-src/TutorialI/CTL/document/CTL.tex --- a/doc-src/TutorialI/CTL/document/CTL.tex Wed May 25 09:03:53 2005 +0200 +++ b/doc-src/TutorialI/CTL/document/CTL.tex Wed May 25 09:04:24 2005 +0200 @@ -67,13 +67,14 @@ \isamarkuptrue% \isacommand{lemma}\ mono{\isacharunderscore}af{\isacharcolon}\ {\isachardoublequote}mono{\isacharparenleft}af\ A{\isacharparenright}{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ mono{\isacharunderscore}def\ af{\isacharunderscore}def{\isacharparenright}\isanewline \isamarkupfalse% -\isanewline +\isacommand{apply}\ blast\isanewline +\isamarkupfalse% +\isacommand{done}\isamarkupfalse% \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% -\isanewline \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% @@ -89,8 +90,6 @@ \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% -\isanewline -\isamarkupfalse% % \begin{isamarkuptext}% All we need to prove now is \isa{mc\ {\isacharparenleft}AF\ f{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ AF\ f{\isacharbraceright}}, which states @@ -101,13 +100,42 @@ \isamarkuptrue% \isacommand{theorem}\ AF{\isacharunderscore}lemma{\isadigit{1}}{\isacharcolon}\isanewline \ \ {\isachardoublequote}lfp{\isacharparenleft}af\ A{\isacharparenright}\ {\isasymsubseteq}\ {\isacharbraceleft}s{\isachardot}\ {\isasymforall}p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharbraceright}{\isachardoublequote}\isamarkupfalse% -\isamarkuptrue% -\isamarkupfalse% -\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +In contrast to the analogous proof for \isa{EF}, and just +for a change, we do not use fixed point induction. Park-induction, +named after David Park, is weaker but sufficient for this proof: +\begin{center} +\isa{f\ S\ {\isasymsubseteq}\ S\ {\isasymLongrightarrow}\ lfp\ f\ {\isasymsubseteq}\ S} \hfill (\isa{lfp{\isacharunderscore}lowerbound}) +\end{center} +The instance of the premise \isa{f\ S\ {\isasymsubseteq}\ S} is proved pointwise, +a decision that \isa{auto} takes for us:% +\end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}rule\ lfp{\isacharunderscore}lowerbound{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ af{\isacharunderscore}def\ Paths{\isacharunderscore}def{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}{\isasymforall}t{\isachardot}\ {\isacharparenleft}p\ {\isadigit{0}}{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymlongrightarrow}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}{\isasymforall}t{\isachardot}\ }{\isacharparenleft}{\isasymforall}p{\isachardot}\ t\ {\isacharequal}\ p\ {\isadigit{0}}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}\ {\isasymlongrightarrow}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}{\isasymforall}t{\isachardot}\ {\isacharparenleft}{\isasymforall}p{\isachardot}\ }{\isacharparenleft}{\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ \ }{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isasymrbrakk}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ }{\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A% +\end{isabelle} +In this remaining case, we set \isa{t} to \isa{p\ {\isadigit{1}}}. +The rest is automatic, which is surprising because it involves +finding the instantiation \isa{{\isasymlambda}i{\isachardot}\ p\ {\isacharparenleft}i\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}} +for \isa{{\isasymforall}p}.% +\end{isamarkuptxt}% +\isamarkuptrue% +\isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}p\ {\isadigit{1}}{\isachardoublequote}\ \isakeyword{in}\ allE{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline +\isamarkupfalse% +\isacommand{done}\isamarkupfalse% % \begin{isamarkuptext}% The opposite inclusion is proved by contradiction: if some state @@ -125,10 +153,13 @@ \isacommand{lemma}\ not{\isacharunderscore}in{\isacharunderscore}lfp{\isacharunderscore}afD{\isacharcolon}\isanewline \ {\isachardoublequote}s\ {\isasymnotin}\ lfp{\isacharparenleft}af\ A{\isacharparenright}\ {\isasymLongrightarrow}\ s\ {\isasymnotin}\ A\ {\isasymand}\ {\isacharparenleft}{\isasymexists}\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ t\ {\isasymnotin}\ lfp{\isacharparenleft}af\ A{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}erule\ contrapos{\isacharunderscore}np{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}subst\ lfp{\isacharunderscore}unfold{\isacharbrackleft}OF\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ af{\isacharunderscore}def{\isacharparenright}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{done}\isamarkupfalse% % \begin{isamarkuptext}% \noindent @@ -162,26 +193,100 @@ \isacommand{lemma}\ infinity{\isacharunderscore}lemma{\isacharcolon}\isanewline \ \ {\isachardoublequote}{\isasymlbrakk}\ Q\ s{\isacharsemicolon}\ {\isasymforall}s{\isachardot}\ Q\ s\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q\ t{\isacharparenright}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\isanewline \ \ \ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ Q{\isacharparenleft}p\ i{\isacharparenright}{\isachardoublequote}\isamarkupfalse% -\isamarkuptrue% -\isamarkupfalse% -\isamarkuptrue% -\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +First we rephrase the conclusion slightly because we need to prove simultaneously +both the path property and the fact that \isa{Q} holds:% +\end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}subgoal{\isacharunderscore}tac\isanewline +\ \ {\isachardoublequote}{\isasymexists}p{\isachardot}\ s\ {\isacharequal}\ p\ {\isadigit{0}}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isacharcolon}{\isacharcolon}nat{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p{\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q{\isacharparenleft}p\ i{\isacharparenright}{\isacharparenright}{\isachardoublequote}{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +From this proposition the original goal follows easily:% +\end{isamarkuptxt}% +\ \isamarkuptrue% +\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ Paths{\isacharunderscore}def{\isacharcomma}\ blast{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +The new subgoal is proved by providing the witness \isa{path\ s\ Q} for \isa{p}:% +\end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}path\ s\ Q{\isachardoublequote}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +After simplification and clarification, the subgoal has the following form: +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}i{\isachardot}\ {\isasymlbrakk}Q\ s{\isacharsemicolon}\ {\isasymforall}s{\isachardot}\ Q\ s\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q\ t{\isacharparenright}{\isasymrbrakk}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}i{\isachardot}\ }{\isasymLongrightarrow}\ {\isacharparenleft}path\ s\ Q\ i{\isacharcomma}\ SOME\ t{\isachardot}\ {\isacharparenleft}path\ s\ Q\ i{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}i{\isachardot}\ {\isasymLongrightarrow}\ }Q\ {\isacharparenleft}path\ s\ Q\ i{\isacharparenright}% +\end{isabelle} +It invites a proof by induction on \isa{i}:% +\end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ i{\isacharparenright}\isanewline +\ \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +After simplification, the base case boils down to +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isasymlbrakk}Q\ s{\isacharsemicolon}\ {\isasymforall}s{\isachardot}\ Q\ s\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q\ t{\isacharparenright}{\isasymrbrakk}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ }{\isasymLongrightarrow}\ {\isacharparenleft}s{\isacharcomma}\ SOME\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q\ t{\isacharparenright}\ {\isasymin}\ M% +\end{isabelle} +The conclusion looks exceedingly trivial: after all, \isa{t} is chosen such that \isa{{\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M} +holds. However, we first have to show that such a \isa{t} actually exists! This reasoning +is embodied in the theorem \isa{someI{\isadigit{2}}{\isacharunderscore}ex}: +\begin{isabelle}% +\ \ \ \ \ {\isasymlbrakk}{\isasymexists}a{\isachardot}\ {\isacharquery}P\ a{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ {\isacharquery}P\ x\ {\isasymLongrightarrow}\ {\isacharquery}Q\ x{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}Q\ {\isacharparenleft}SOME\ x{\isachardot}\ {\isacharquery}P\ x{\isacharparenright}% +\end{isabelle} +When we apply this theorem as an introduction rule, \isa{{\isacharquery}P\ x} becomes +\isa{{\isacharparenleft}s{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q\ x} and \isa{{\isacharquery}Q\ x} becomes \isa{{\isacharparenleft}s{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ M} and we have to prove +two subgoals: \isa{{\isasymexists}a{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ a{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q\ a}, which follows from the assumptions, and +\isa{{\isacharparenleft}s{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q\ x\ {\isasymLongrightarrow}\ {\isacharparenleft}s{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ M}, which is trivial. Thus it is not surprising that +\isa{fast} can prove the base case quickly:% +\end{isamarkuptxt}% +\ \isamarkuptrue% +\isacommand{apply}{\isacharparenleft}fast\ intro{\isacharcolon}\ someI{\isadigit{2}}{\isacharunderscore}ex{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +What is worth noting here is that we have used \methdx{fast} rather than +\isa{blast}. The reason is that \isa{blast} would fail because it cannot +cope with \isa{someI{\isadigit{2}}{\isacharunderscore}ex}: unifying its conclusion with the current +subgoal is non-trivial because of the nested schematic variables. For +efficiency reasons \isa{blast} does not even attempt such unifications. +Although \isa{fast} can in principle cope with complicated unification +problems, in practice the number of unifiers arising is often prohibitive and +the offending rule may need to be applied explicitly rather than +automatically. This is what happens in the step case. + +The induction step is similar, but more involved, because now we face nested +occurrences of \isa{SOME}. As a result, \isa{fast} is no longer able to +solve the subgoal and we apply \isa{someI{\isadigit{2}}{\isacharunderscore}ex} by hand. We merely +show the proof commands but do not describe the details:% +\end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}rule\ someI{\isadigit{2}}{\isacharunderscore}ex{\isacharparenright}\isanewline +\ \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}rule\ someI{\isadigit{2}}{\isacharunderscore}ex{\isacharparenright}\isanewline +\ \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{done}\isamarkupfalse% % \begin{isamarkuptext}% Function \isa{path} has fulfilled its purpose now and can be forgotten. @@ -211,7 +316,6 @@ \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% -\isanewline \isamarkupfalse% % \begin{isamarkuptext}% @@ -219,15 +323,40 @@ \end{isamarkuptext}% \isamarkuptrue% \isacommand{theorem}\ AF{\isacharunderscore}lemma{\isadigit{2}}{\isacharcolon}\ {\isachardoublequote}{\isacharbraceleft}s{\isachardot}\ {\isasymforall}p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharbraceright}\ {\isasymsubseteq}\ lfp{\isacharparenleft}af\ A{\isacharparenright}{\isachardoublequote}\isamarkupfalse% -\isamarkuptrue% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +The proof is again pointwise and then by contraposition:% +\end{isamarkuptxt}% \isamarkuptrue% +\isacommand{apply}{\isacharparenleft}rule\ subsetI{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}erule\ contrapos{\isacharunderscore}pp{\isacharparenright}\isanewline +\isamarkupfalse% +\isacommand{apply}\ simp\isamarkupfalse% +% +\begin{isamarkuptxt}% +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymnotin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymexists}p{\isasymin}Paths\ x{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ A% +\end{isabelle} +Applying the \isa{infinity{\isacharunderscore}lemma} as a destruction rule leaves two subgoals, the second +premise of \isa{infinity{\isacharunderscore}lemma} and the original subgoal:% +\end{isamarkuptxt}% \isamarkuptrue% +\isacommand{apply}{\isacharparenleft}drule\ infinity{\isacharunderscore}lemma{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ {\isasymforall}s{\isachardot}\ s\ {\isasymnotin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ t\ {\isasymnotin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}{\isacharparenright}\isanewline +\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ {\isasymexists}p{\isasymin}Paths\ x{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\ {\isasymLongrightarrow}\isanewline +\isaindent{\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ }{\isasymexists}p{\isasymin}Paths\ x{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ A% +\end{isabelle} +Both are solved automatically:% +\end{isamarkuptxt}% +\ \isamarkuptrue% +\isacommand{apply}{\isacharparenleft}auto\ dest{\isacharcolon}\ not{\isacharunderscore}in{\isacharunderscore}lfp{\isacharunderscore}afD{\isacharparenright}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{done}\isamarkupfalse% % \begin{isamarkuptext}% If you find these proofs too complicated, we recommend that you read @@ -241,9 +370,11 @@ \isamarkuptrue% \isacommand{theorem}\ {\isachardoublequote}mc\ f\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ f{\isacharbraceright}{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ f{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ EF{\isacharunderscore}lemma\ equalityI{\isacharbrackleft}OF\ AF{\isacharunderscore}lemma{\isadigit{1}}\ AF{\isacharunderscore}lemma{\isadigit{2}}{\isacharbrackright}{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{done}\isamarkupfalse% % \begin{isamarkuptext}% The language defined above is not quite CTL\@. The latter also includes an @@ -293,12 +424,6 @@ \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% -\isanewline -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isanewline \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% @@ -311,8 +436,10 @@ \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% -\isanewline -\isanewline +\isamarkupfalse% +\isamarkupfalse% +\isamarkupfalse% +\isamarkupfalse% \isamarkupfalse% % \begin{isamarkuptext}% diff -r 0e7b145c3a89 -r 3f2a9f400168 doc-src/TutorialI/CTL/document/CTLind.tex --- a/doc-src/TutorialI/CTL/document/CTLind.tex Wed May 25 09:03:53 2005 +0200 +++ b/doc-src/TutorialI/CTL/document/CTLind.tex Wed May 25 09:04:24 2005 +0200 @@ -50,12 +50,17 @@ \ \ {\isachardoublequote}t\ {\isasymin}\ Avoid\ s\ A\ \ {\isasymLongrightarrow}\isanewline \ \ \ {\isasymforall}f{\isasymin}Paths\ t{\isachardot}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ f\ i\ {\isasymnotin}\ A{\isacharparenright}\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ A{\isacharparenright}{\isachardoublequote}\isanewline \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}erule\ Avoid{\isachardot}induct{\isacharparenright}\isanewline +\ \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}drule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}{\isasymlambda}i{\isachardot}\ case\ i\ of\ {\isadigit{0}}\ {\isasymRightarrow}\ t\ {\isacharbar}\ Suc\ i\ {\isasymRightarrow}\ f\ i{\isachardoublequote}\ \isakeyword{in}\ bspec{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ Paths{\isacharunderscore}def\ split{\isacharcolon}\ nat{\isachardot}split{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{done}\isamarkupfalse% % \begin{isamarkuptext}% \noindent @@ -76,22 +81,84 @@ \isamarkuptrue% \isacommand{lemma}\ Avoid{\isacharunderscore}in{\isacharunderscore}lfp{\isacharbrackleft}rule{\isacharunderscore}format{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isacharbrackright}{\isacharcolon}\isanewline \ \ {\isachardoublequote}{\isasymforall}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A\ {\isasymLongrightarrow}\ t\ {\isasymin}\ Avoid\ s\ A\ {\isasymlongrightarrow}\ t\ {\isasymin}\ lfp{\isacharparenleft}af\ A{\isacharparenright}{\isachardoublequote}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +The proof is by induction on the ``distance'' between \isa{t} and \isa{A}. Remember that \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}\ {\isacharequal}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. +If \isa{t} is already in \isa{A}, then \isa{t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}} is +trivial. If \isa{t} is not in \isa{A} but all successors are in +\isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}} (induction hypothesis), then \isa{t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}} is +again trivial. + +The formal counterpart of this proof sketch is a well-founded induction +on~\isa{M} restricted to \isa{Avoid\ s\ A\ {\isacharminus}\ A}, roughly speaking: +\begin{isabelle}% +\ \ \ \ \ {\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ x\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ x\ {\isasymnotin}\ A{\isacharbraceright}% +\end{isabelle} +As we shall see presently, the absence of infinite \isa{A}-avoiding paths +starting from \isa{s} implies well-foundedness of this relation. For the +moment we assume this and proceed with the induction:% +\end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkuptrue% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}subgoal{\isacharunderscore}tac\ {\isachardoublequote}wf{\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}x{\isacharparenright}{\isachardot}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ x\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ x\ {\isasymnotin}\ A{\isacharbraceright}{\isachardoublequote}{\isacharparenright}\isanewline +\ \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ a\ {\isacharequal}\ t\ \isakeyword{in}\ wf{\isacharunderscore}induct{\isacharparenright}\isanewline +\ \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}\isamarkupfalse% \isamarkupfalse% -\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ {\isasymlbrakk}{\isasymforall}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharsemicolon}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ \ }{\isasymforall}y{\isachardot}\ {\isacharparenleft}t{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ t\ {\isasymnotin}\ A\ {\isasymlongrightarrow}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ \ {\isasymforall}y{\isachardot}\ }y\ {\isasymin}\ Avoid\ s\ A\ {\isasymlongrightarrow}\ y\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}{\isacharsemicolon}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ \ }t\ {\isasymin}\ Avoid\ s\ A{\isasymrbrakk}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ }{\isasymLongrightarrow}\ t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\isanewline +\ {\isadigit{2}}{\isachardot}\ {\isasymforall}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A\ {\isasymLongrightarrow}\isanewline +\isaindent{\ {\isadigit{2}}{\isachardot}\ }wf\ {\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ x\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ x\ {\isasymnotin}\ A{\isacharbraceright}% +\end{isabelle} +Now the induction hypothesis states that if \isa{t\ {\isasymnotin}\ A} +then all successors of \isa{t} that are in \isa{Avoid\ s\ A} are in +\isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. Unfolding \isa{lfp} in the conclusion of the first +subgoal once, we have to prove that \isa{t} is in \isa{A} or all successors +of \isa{t} are in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. But if \isa{t} is not in \isa{A}, +the second +\isa{Avoid}-rule implies that all successors of \isa{t} are in +\isa{Avoid\ s\ A}, because we also assume \isa{t\ {\isasymin}\ Avoid\ s\ A}. +Hence, by the induction hypothesis, all successors of \isa{t} are indeed in +\isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. Mechanically:% +\end{isamarkuptxt}% +\ \isamarkuptrue% +\isacommand{apply}{\isacharparenleft}subst\ lfp{\isacharunderscore}unfold{\isacharbrackleft}OF\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharparenright}\isanewline +\ \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}simp\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}\ add{\isacharcolon}\ af{\isacharunderscore}def{\isacharparenright}\isanewline +\ \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ Avoid{\isachardot}intros{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +Having proved the main goal, we return to the proof obligation that the +relation used above is indeed well-founded. This is proved by contradiction: if +the relation is not well-founded then there exists an infinite \isa{A}-avoiding path all in \isa{Avoid\ s\ A}, by theorem +\isa{wf{\isacharunderscore}iff{\isacharunderscore}no{\isacharunderscore}infinite{\isacharunderscore}down{\isacharunderscore}chain}: +\begin{isabelle}% +\ \ \ \ \ wf\ r\ {\isacharequal}\ {\isacharparenleft}{\isasymnot}\ {\isacharparenleft}{\isasymexists}f{\isachardot}\ {\isasymforall}i{\isachardot}\ {\isacharparenleft}f\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharcomma}\ f\ i{\isacharparenright}\ {\isasymin}\ r{\isacharparenright}{\isacharparenright}% +\end{isabelle} +From lemma \isa{ex{\isacharunderscore}infinite{\isacharunderscore}path} the existence of an infinite +\isa{A}-avoiding path starting in \isa{s} follows, contradiction.% +\end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}erule\ contrapos{\isacharunderscore}pp{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ wf{\isacharunderscore}iff{\isacharunderscore}no{\isacharunderscore}infinite{\isacharunderscore}down{\isacharunderscore}chain{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}erule\ exE{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}rule\ ex{\isacharunderscore}infinite{\isacharunderscore}path{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ Paths{\isacharunderscore}def{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{done}\isamarkupfalse% % \begin{isamarkuptext}% The \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}} modifier of the \isa{rule{\isacharunderscore}format} directive in the @@ -111,6 +178,7 @@ \isamarkuptrue% \isacommand{theorem}\ AF{\isacharunderscore}lemma{\isadigit{2}}{\isacharcolon}\ \ {\isachardoublequote}{\isacharbraceleft}s{\isachardot}\ {\isasymforall}p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}\ i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharbraceright}\ {\isasymsubseteq}\ lfp{\isacharparenleft}af\ A{\isacharparenright}{\isachardoublequote}\isanewline \isamarkupfalse% +\isacommand{by}{\isacharparenleft}auto\ elim{\isacharcolon}\ Avoid{\isacharunderscore}in{\isacharunderscore}lfp\ intro{\isacharcolon}\ Avoid{\isachardot}intros{\isacharparenright}\isanewline \isanewline \isamarkupfalse% \isamarkupfalse% diff -r 0e7b145c3a89 -r 3f2a9f400168 doc-src/TutorialI/CTL/document/PDL.tex --- a/doc-src/TutorialI/CTL/document/PDL.tex Wed May 25 09:03:53 2005 +0200 +++ b/doc-src/TutorialI/CTL/document/PDL.tex Wed May 25 09:04:24 2005 +0200 @@ -87,9 +87,11 @@ \isamarkuptrue% \isacommand{lemma}\ mono{\isacharunderscore}ef{\isacharcolon}\ {\isachardoublequote}mono{\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ {\isacharparenleft}M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}rule\ monoI{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{apply}\ blast\isanewline \isamarkupfalse% +\isacommand{done}\isamarkupfalse% % \begin{isamarkuptext}% \noindent @@ -99,30 +101,112 @@ \isamarkuptrue% \isacommand{lemma}\ EF{\isacharunderscore}lemma{\isacharcolon}\isanewline \ \ {\isachardoublequote}lfp{\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ {\isacharparenleft}M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A{\isacharbraceright}{\isachardoublequote}\isamarkupfalse% -\isamarkuptrue% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +The equality is proved in the canonical fashion by proving that each set +includes the other; the inclusion is shown pointwise:% +\end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}rule\ equalityI{\isacharparenright}\isanewline +\ \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}rule\ subsetI{\isacharparenright}\isanewline +\ \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isamarkupfalse% \isamarkupfalse% -\isamarkuptrue% -\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +Simplification leaves us with the following first subgoal +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}s{\isachardot}\ s\ {\isasymin}\ lfp\ {\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A% +\end{isabelle} +which is proved by \isa{lfp}-induction:% +\end{isamarkuptxt}% +\ \isamarkuptrue% +\isacommand{apply}{\isacharparenleft}erule\ lfp{\isacharunderscore}induct{\isacharparenright}\isanewline +\ \ \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}rule\ mono{\isacharunderscore}ef{\isacharparenright}\isanewline +\ \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +Having disposed of the monotonicity subgoal, +simplification leaves us with the following goal: +\begin{isabelle} +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ A\ {\isasymor}\isanewline +\ \ \ \ \ \ \ \ \ x\ {\isasymin}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ {\isacharparenleft}lfp\ {\isacharparenleft}\dots{\isacharparenright}\ {\isasyminter}\ {\isacharbraceleft}x{\isachardot}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A{\isacharbraceright}{\isacharparenright}\isanewline +\ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A +\end{isabelle} +It is proved by \isa{blast}, using the transitivity of +\isa{M\isactrlsup {\isacharasterisk}}.% +\end{isamarkuptxt}% +\ \isamarkuptrue% +\isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtrancl{\isacharunderscore}trans{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +We now return to the second set inclusion subgoal, which is again proved +pointwise:% +\end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% -\isamarkupfalse% -\isamarkuptrue% -\isamarkupfalse% -\isamarkuptrue% +\isacommand{apply}{\isacharparenleft}rule\ subsetI{\isacharparenright}\isanewline \isamarkupfalse% -\isamarkuptrue% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}simp{\isacharcomma}\ clarify{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +After simplification and clarification we are left with +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ t{\isachardot}\ {\isasymlbrakk}{\isacharparenleft}x{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}{\isacharsemicolon}\ t\ {\isasymin}\ A{\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isasymin}\ lfp\ {\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}% +\end{isabelle} +This goal is proved by induction on \isa{{\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}}. But since the model +checker works backwards (from \isa{t} to \isa{s}), we cannot use the +induction theorem \isa{rtrancl{\isacharunderscore}induct}: it works in the +forward direction. Fortunately the converse induction theorem +\isa{converse{\isacharunderscore}rtrancl{\isacharunderscore}induct} already exists: +\begin{isabelle}% +\ \ \ \ \ {\isasymlbrakk}{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r\isactrlsup {\isacharasterisk}{\isacharsemicolon}\ P\ b{\isacharsemicolon}\isanewline +\isaindent{\ \ \ \ \ \ }{\isasymAnd}y\ z{\isachardot}\ {\isasymlbrakk}{\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharsemicolon}\ {\isacharparenleft}z{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r\isactrlsup {\isacharasterisk}{\isacharsemicolon}\ P\ z{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ y{\isasymrbrakk}\isanewline +\isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ P\ a% +\end{isabelle} +It says that if \isa{{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r\isactrlsup {\isacharasterisk}} and we know \isa{P\ b} then we can infer +\isa{P\ a} provided each step backwards from a predecessor \isa{z} of +\isa{b} preserves \isa{P}.% +\end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}erule\ converse{\isacharunderscore}rtrancl{\isacharunderscore}induct{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +The base case +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ t{\isachardot}\ t\ {\isasymin}\ A\ {\isasymLongrightarrow}\ t\ {\isasymin}\ lfp\ {\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}% +\end{isabelle} +is solved by unrolling \isa{lfp} once% +\end{isamarkuptxt}% +\ \isamarkuptrue% +\isacommand{apply}{\isacharparenleft}subst\ lfp{\isacharunderscore}unfold{\isacharbrackleft}OF\ mono{\isacharunderscore}ef{\isacharbrackright}{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ t{\isachardot}\ t\ {\isasymin}\ A\ {\isasymLongrightarrow}\ t\ {\isasymin}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ lfp\ {\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}% +\end{isabelle} +and disposing of the resulting trivial subgoal automatically:% +\end{isamarkuptxt}% +\ \isamarkuptrue% +\isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +The proof of the induction step is identical to the one for the base case:% +\end{isamarkuptxt}% +\isamarkuptrue% +\isacommand{apply}{\isacharparenleft}subst\ lfp{\isacharunderscore}unfold{\isacharbrackleft}OF\ mono{\isacharunderscore}ef{\isacharbrackright}{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{done}\isamarkupfalse% % \begin{isamarkuptext}% The main theorem is proved in the familiar manner: induction followed by @@ -131,9 +215,11 @@ \isamarkuptrue% \isacommand{theorem}\ {\isachardoublequote}mc\ f\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ f{\isacharbraceright}{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ f{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ EF{\isacharunderscore}lemma{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{done}\isamarkupfalse% % \begin{isamarkuptext}% \begin{exercise} @@ -158,17 +244,14 @@ \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% -\isanewline -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isanewline \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% -\isanewline +\isamarkupfalse% +\isamarkupfalse% +\isamarkupfalse% \isamarkupfalse% \isamarkupfalse% \end{isabellebody}% diff -r 0e7b145c3a89 -r 3f2a9f400168 doc-src/TutorialI/CodeGen/document/CodeGen.tex --- a/doc-src/TutorialI/CodeGen/document/CodeGen.tex Wed May 25 09:03:53 2005 +0200 +++ b/doc-src/TutorialI/CodeGen/document/CodeGen.tex Wed May 25 09:04:24 2005 +0200 @@ -105,12 +105,27 @@ \end{isamarkuptext}% \isamarkuptrue% \isacommand{theorem}\ {\isachardoublequote}{\isasymforall}vs{\isachardot}\ exec\ {\isacharparenleft}comp\ e{\isacharparenright}\ s\ vs\ {\isacharequal}\ {\isacharparenleft}value\ e\ s{\isacharparenright}\ {\isacharhash}\ vs{\isachardoublequote}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +It will be proved by induction on \isa{e} followed by simplification. +First, we must prove a lemma about executing the concatenation of two +instruction sequences:% +\end{isamarkuptxt}% \isamarkuptrue% \isamarkupfalse% \isacommand{lemma}\ exec{\isacharunderscore}app{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline \ \ {\isachardoublequote}{\isasymforall}vs{\isachardot}\ exec\ {\isacharparenleft}xs{\isacharat}ys{\isacharparenright}\ s\ vs\ {\isacharequal}\ exec\ ys\ s\ {\isacharparenleft}exec\ xs\ s\ vs{\isacharparenright}{\isachardoublequote}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +This requires induction on \isa{xs} and ordinary simplification for the +base cases. In the induction step, simplification leaves us with a formula +that contains two \isa{case}-expressions over instructions. Thus we add +automatic case splitting, which finishes the proof:% +\end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharcomma}\ simp\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}\isamarkupfalse% \isamarkupfalse% % \begin{isamarkuptext}% @@ -122,7 +137,7 @@ \isamarkuptrue% \isamarkupfalse% \isamarkupfalse% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharunderscore}all\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}\isamarkupfalse% \isamarkupfalse% % \begin{isamarkuptext}% @@ -137,7 +152,6 @@ \end{isamarkuptext}% \isamarkuptrue% \isamarkupfalse% -\isanewline \isamarkupfalse% \isamarkupfalse% \end{isabellebody}% diff -r 0e7b145c3a89 -r 3f2a9f400168 doc-src/TutorialI/Datatype/document/ABexpr.tex --- a/doc-src/TutorialI/Datatype/document/ABexpr.tex Wed May 25 09:03:53 2005 +0200 +++ b/doc-src/TutorialI/Datatype/document/ABexpr.tex Wed May 25 09:04:24 2005 +0200 @@ -103,9 +103,14 @@ \isacommand{lemma}\ {\isachardoublequote}evala\ {\isacharparenleft}substa\ s\ a{\isacharparenright}\ env\ {\isacharequal}\ evala\ a\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ evala\ {\isacharparenleft}s\ x{\isacharparenright}\ env{\isacharparenright}\ {\isasymand}\isanewline \ \ \ \ \ \ \ \ evalb\ {\isacharparenleft}substb\ s\ b{\isacharparenright}\ env\ {\isacharequal}\ evalb\ b\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ evala\ {\isacharparenleft}s\ x{\isacharparenright}\ env{\isacharparenright}{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ a\ \isakeyword{and}\ b{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +The resulting 8 goals (one for each constructor) are proved in one fell swoop:% +\end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% +\isacommand{apply}\ simp{\isacharunderscore}all\isamarkupfalse% \isamarkupfalse% % \begin{isamarkuptext}% @@ -135,14 +140,12 @@ \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% -\isanewline \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% -\isanewline \isamarkupfalse% \isamarkupfalse% \end{isabellebody}% diff -r 0e7b145c3a89 -r 3f2a9f400168 doc-src/TutorialI/Datatype/document/Fundata.tex --- a/doc-src/TutorialI/Datatype/document/Fundata.tex Wed May 25 09:03:53 2005 +0200 +++ b/doc-src/TutorialI/Datatype/document/Fundata.tex Wed May 25 09:04:24 2005 +0200 @@ -43,12 +43,23 @@ \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}map{\isacharunderscore}bt\ {\isacharparenleft}g\ o\ f{\isacharparenright}\ T\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ T{\isacharparenright}{\isachardoublequote}\isanewline \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ T{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{done}\isamarkupfalse% \isamarkupfalse% \isamarkupfalse% -\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +Because of the function type, the proof state after induction looks unusual. +Notice the quantified induction hypothesis: +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ map{\isacharunderscore}bt\ {\isacharparenleft}g\ {\isasymcirc}\ f{\isacharparenright}\ Tip\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ Tip{\isacharparenright}\isanewline +\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}a\ F{\isachardot}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ map{\isacharunderscore}bt\ {\isacharparenleft}g\ {\isasymcirc}\ f{\isacharparenright}\ {\isacharparenleft}F\ x{\isacharparenright}\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ {\isacharparenleft}F\ x{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\isanewline +\isaindent{\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}a\ F{\isachardot}\ }map{\isacharunderscore}bt\ {\isacharparenleft}g\ {\isasymcirc}\ f{\isacharparenright}\ {\isacharparenleft}Br\ a\ F{\isacharparenright}\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ {\isacharparenleft}Br\ a\ F{\isacharparenright}{\isacharparenright}% +\end{isabelle}% +\end{isamarkuptxt}% \isamarkuptrue% -\isanewline \isamarkupfalse% \isamarkupfalse% \end{isabellebody}% diff -r 0e7b145c3a89 -r 3f2a9f400168 doc-src/TutorialI/Datatype/document/Nested.tex --- a/doc-src/TutorialI/Datatype/document/Nested.tex Wed May 25 09:03:53 2005 +0200 +++ b/doc-src/TutorialI/Datatype/document/Nested.tex Wed May 25 09:04:24 2005 +0200 @@ -73,8 +73,9 @@ \isacommand{lemma}\ subst{\isacharunderscore}id{\isacharcolon}\ {\isachardoublequote}subst\ \ Var\ t\ \ {\isacharequal}\ {\isacharparenleft}t\ {\isacharcolon}{\isacharcolon}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isacharparenright}\ \ {\isasymand}\isanewline \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ substs\ Var\ ts\ {\isacharequal}\ {\isacharparenleft}ts{\isacharcolon}{\isacharcolon}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term\ list{\isacharparenright}{\isachardoublequote}\isanewline \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ t\ \isakeyword{and}\ ts{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{done}\isamarkupfalse% % \begin{isamarkuptext}% \noindent @@ -116,9 +117,9 @@ \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% -\isanewline -\isanewline -\isanewline +\isamarkupfalse% +\isamarkupfalse% +\isamarkupfalse% \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% @@ -126,14 +127,11 @@ \isamarkupfalse% \isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isanewline -\isamarkupfalse% \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}subst\ s\ {\isacharparenleft}App\ f\ ts{\isacharparenright}\ {\isacharequal}\ App\ f\ {\isacharparenleft}map\ {\isacharparenleft}subst\ s{\isacharparenright}\ ts{\isacharparenright}{\isachardoublequote}\isanewline \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ ts{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{done}\isamarkupfalse% % \begin{isamarkuptext}% \noindent diff -r 0e7b145c3a89 -r 3f2a9f400168 doc-src/TutorialI/Documents/document/Documents.tex --- a/doc-src/TutorialI/Documents/document/Documents.tex Wed May 25 09:03:53 2005 +0200 +++ b/doc-src/TutorialI/Documents/document/Documents.tex Wed May 25 09:04:24 2005 +0200 @@ -587,6 +587,9 @@ } \isanewline \ \ \isamarkupfalse% +\isacommand{by}\ {\isacharparenleft}rule\ impI{\isacharparenright}\ % +\isamarkupcmt{implicit assumption step involved here% +} \isamarkupfalse% % \begin{isamarkuptext}% @@ -812,7 +815,7 @@ \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}x\ {\isasymnoteq}\ {\isacharparenleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}int{\isacharparenright}\ {\isasymLongrightarrow}\ {\isadigit{0}}\ {\isacharless}\ x\ {\isacharasterisk}\ x{\isachardoublequote}\isanewline \ \ \isamarkupfalse% -\isamarkupfalse% +\isacommand{by}\ {\isacharparenleft}auto{\isacharparenright}\isamarkupfalse% % \begin{isamarkuptext}% \noindent Here the real source of the proof has been as follows: diff -r 0e7b145c3a89 -r 3f2a9f400168 doc-src/TutorialI/Ifexpr/document/Ifexpr.tex --- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Wed May 25 09:03:53 2005 +0200 +++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Wed May 25 09:04:24 2005 +0200 @@ -100,10 +100,17 @@ \end{isamarkuptext}% \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}valif\ {\isacharparenleft}bool{\isadigit{2}}if\ b{\isacharparenright}\ env\ {\isacharequal}\ value\ b\ env{\isachardoublequote}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +The proof is canonical:% +\end{isamarkuptxt}% \isamarkuptrue% +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ b{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{done}\isamarkupfalse% % \begin{isamarkuptext}% \noindent @@ -152,11 +159,9 @@ \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline \ \ {\isachardoublequote}{\isasymforall}t\ e{\isachardot}\ valif\ {\isacharparenleft}normif\ b\ t\ e{\isacharparenright}\ env\ {\isacharequal}\ valif\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ env{\isachardoublequote}\isamarkupfalse% \isamarkupfalse% -\isanewline \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% -\isanewline \isamarkupfalse% % \begin{isamarkuptext}% @@ -184,11 +189,9 @@ \isamarkuptrue% \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}t\ e{\isachardot}\ normal{\isacharparenleft}normif\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}normal\ t\ {\isasymand}\ normal\ e{\isacharparenright}{\isachardoublequote}\isamarkupfalse% \isamarkupfalse% -\isanewline \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% -\isanewline \isamarkupfalse% % \begin{isamarkuptext}% @@ -217,21 +220,17 @@ \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% -\isanewline +\isamarkupfalse% +\isamarkupfalse% \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% -\isanewline \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% -\isanewline \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% -\isanewline -\isamarkupfalse% -\isamarkupfalse% \end{isabellebody}% %%% Local Variables: %%% mode: latex diff -r 0e7b145c3a89 -r 3f2a9f400168 doc-src/TutorialI/Inductive/document/AB.tex --- a/doc-src/TutorialI/Inductive/document/AB.tex Wed May 25 09:03:53 2005 +0200 +++ b/doc-src/TutorialI/Inductive/document/AB.tex Wed May 25 09:04:24 2005 +0200 @@ -38,7 +38,7 @@ \isamarkuptrue% \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymnoteq}\ a{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ b{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}x\ {\isasymnoteq}\ b{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ a{\isacharparenright}{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{by}\ {\isacharparenleft}case{\isacharunderscore}tac\ x{\isacharcomma}\ auto{\isacharparenright}\isamarkupfalse% % \begin{isamarkuptext}% \noindent @@ -80,8 +80,16 @@ \ \ {\isachardoublequote}{\isacharparenleft}w\ {\isasymin}\ S\ {\isasymlongrightarrow}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}{\isacharparenright}\ \ \ \ \ {\isasymand}\isanewline \ \ \ {\isacharparenleft}w\ {\isasymin}\ A\ {\isasymlongrightarrow}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isasymand}\isanewline \ \ \ {\isacharparenleft}w\ {\isasymin}\ B\ {\isasymlongrightarrow}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +These propositions are expressed with the help of the predefined \isa{filter} function on lists, which has the convenient syntax \isa{{\isacharbrackleft}x{\isasymin}xs{\isachardot}\ P\ x{\isacharbrackright}}, the list of all elements \isa{x} in \isa{xs} such that \isa{P\ x} +holds. Remember that on lists \isa{size} and \isa{length} are synonymous. + +The proof itself is by rule induction and afterwards automatic:% +\end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% +\isacommand{by}\ {\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}induct{\isacharcomma}\ auto{\isacharparenright}\isamarkupfalse% % \begin{isamarkuptext}% \noindent @@ -120,10 +128,26 @@ \isacommand{lemma}\ step{\isadigit{1}}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i\ {\isacharless}\ size\ w{\isachardot}\isanewline \ \ {\isasymbar}{\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ P\ x{\isacharbrackright}{\isacharparenright}{\isacharminus}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}\isanewline \ \ \ {\isacharminus}\ {\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ P\ x{\isacharbrackright}{\isacharparenright}{\isacharminus}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isasymbar}\ {\isasymle}\ {\isadigit{1}}{\isachardoublequote}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +The lemma is a bit hard to read because of the coercion function +\isa{int\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ int}. It is required because \isa{size} returns +a natural number, but subtraction on type~\isa{nat} will do the wrong thing. +Function \isa{take} is predefined and \isa{take\ i\ xs} is the prefix of +length \isa{i} of \isa{xs}; below we also need \isa{drop\ i\ xs}, which +is what remains after that prefix has been dropped from \isa{xs}. + +The proof is by induction on \isa{w}, with a trivial base case, and a not +so trivial induction step. Since it is essentially just arithmetic, we do not +discuss it.% +\end{isamarkuptxt}% \isamarkuptrue% +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ w{\isacharparenright}\isanewline +\ \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{by}{\isacharparenleft}force\ simp\ add{\isacharcolon}\ zabs{\isacharunderscore}def\ take{\isacharunderscore}Cons\ split{\isacharcolon}\ nat{\isachardot}split\ if{\isacharunderscore}splits{\isacharparenright}\isamarkupfalse% % \begin{isamarkuptext}% Finally we come to the above-mentioned lemma about cutting in half a word with two more elements of one sort than of the other sort:% @@ -132,9 +156,17 @@ \isacommand{lemma}\ part{\isadigit{1}}{\isacharcolon}\isanewline \ {\isachardoublequote}size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{2}}\ {\isasymLongrightarrow}\isanewline \ \ {\isasymexists}i{\isasymle}size\ w{\isachardot}\ size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{1}}{\isachardoublequote}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +This is proved by \isa{force} with the help of the intermediate value theorem, +instantiated appropriately and with its first premise disposed of by lemma +\isa{step{\isadigit{1}}}:% +\end{isamarkuptxt}% \isamarkuptrue% +\isacommand{apply}{\isacharparenleft}insert\ nat{\isadigit{0}}{\isacharunderscore}intermed{\isacharunderscore}int{\isacharunderscore}val{\isacharbrackleft}OF\ step{\isadigit{1}}{\isacharcomma}\ of\ {\isachardoublequote}P{\isachardoublequote}\ {\isachardoublequote}w{\isachardoublequote}\ {\isachardoublequote}{\isadigit{1}}{\isachardoublequote}{\isacharbrackright}{\isacharparenright}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{by}\ force\isamarkupfalse% % \begin{isamarkuptext}% \noindent @@ -149,7 +181,7 @@ \ \ \ \ size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{1}}{\isasymrbrakk}\isanewline \ \ \ {\isasymLongrightarrow}\ size{\isacharbrackleft}x{\isasymin}drop\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}drop\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{1}}{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{by}{\isacharparenleft}simp\ del{\isacharcolon}\ append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharparenright}\isamarkupfalse% % \begin{isamarkuptext}% \noindent @@ -182,38 +214,119 @@ \ \ {\isachardoublequote}{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ \ \ \ \ {\isasymlongrightarrow}\ w\ {\isasymin}\ S{\isacharparenright}\ {\isasymand}\isanewline \ \ \ {\isacharparenleft}size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}\ {\isasymlongrightarrow}\ w\ {\isasymin}\ A{\isacharparenright}\ {\isasymand}\isanewline \ \ \ {\isacharparenleft}size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}\ {\isasymlongrightarrow}\ w\ {\isasymin}\ B{\isacharparenright}{\isachardoublequote}\isamarkupfalse% -\isamarkuptrue% -\isamarkupfalse% -\isamarkupfalse% -\isamarkuptrue% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +The proof is by induction on \isa{w}. Structural induction would fail here +because, as we can see from the grammar, we need to make bigger steps than +merely appending a single letter at the front. Hence we induct on the length +of \isa{w}, using the induction rule \isa{length{\isacharunderscore}induct}:% +\end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ w\ rule{\isacharcolon}\ length{\isacharunderscore}induct{\isacharparenright}\isamarkupfalse% \isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +The \isa{rule} parameter tells \isa{induct{\isacharunderscore}tac} explicitly which induction +rule to use. For details see \S\ref{sec:complete-ind} below. +In this case the result is that we may assume the lemma already +holds for all words shorter than \isa{w}. + +The proof continues with a case distinction on \isa{w}, +on whether \isa{w} is empty or not.% +\end{isamarkuptxt}% \isamarkuptrue% +\isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ w{\isacharparenright}\isanewline +\ \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all{\isacharparenright}\isamarkupfalse% \isamarkupfalse% -\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +Simplification disposes of the base case and leaves only a conjunction +of two step cases to be proved: +if \isa{w\ {\isacharequal}\ a\ {\isacharhash}\ v} and \begin{isabelle}% +\ \ \ \ \ length\ {\isacharbrackleft}x{\isasymin}v\ {\isachardot}\ x\ {\isacharequal}\ a{\isacharbrackright}\ {\isacharequal}\ length\ {\isacharbrackleft}x{\isasymin}v\ {\isachardot}\ x\ {\isacharequal}\ b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{2}}% +\end{isabelle} then +\isa{b\ {\isacharhash}\ v\ {\isasymin}\ A}, and similarly for \isa{w\ {\isacharequal}\ b\ {\isacharhash}\ v}. +We only consider the first case in detail. + +After breaking the conjunction up into two cases, we can apply +\isa{part{\isadigit{1}}} to the assumption that \isa{w} contains two more \isa{a}'s than \isa{b}'s.% +\end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% -\isamarkuptrue% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}rule\ conjI{\isacharparenright}\isanewline +\ \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline +\ \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}frule\ part{\isadigit{1}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}a{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline +\ \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +This yields an index \isa{i\ {\isasymle}\ length\ v} such that +\begin{isabelle}% +\ \ \ \ \ length\ {\isacharbrackleft}x{\isasymin}take\ i\ v\ {\isachardot}\ x\ {\isacharequal}\ a{\isacharbrackright}\ {\isacharequal}\ length\ {\isacharbrackleft}x{\isasymin}take\ i\ v\ {\isachardot}\ x\ {\isacharequal}\ b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}% +\end{isabelle} +With the help of \isa{part{\isadigit{2}}} it follows that +\begin{isabelle}% +\ \ \ \ \ length\ {\isacharbrackleft}x{\isasymin}drop\ i\ v\ {\isachardot}\ x\ {\isacharequal}\ a{\isacharbrackright}\ {\isacharequal}\ length\ {\isacharbrackleft}x{\isasymin}drop\ i\ v\ {\isachardot}\ x\ {\isacharequal}\ b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}% +\end{isabelle}% +\end{isamarkuptxt}% +\ \isamarkuptrue% +\isacommand{apply}{\isacharparenleft}drule\ part{\isadigit{2}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}a{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline +\ \ \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}assumption{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +Now it is time to decompose \isa{v} in the conclusion \isa{b\ {\isacharhash}\ v\ {\isasymin}\ A} +into \isa{take\ i\ v\ {\isacharat}\ drop\ i\ v},% +\end{isamarkuptxt}% +\ \isamarkuptrue% +\isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ n{\isadigit{1}}{\isacharequal}i\ \isakeyword{and}\ t{\isacharequal}v\ \isakeyword{in}\ subst{\isacharbrackleft}OF\ append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharbrackright}{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +(the variables \isa{n{\isadigit{1}}} and \isa{t} are the result of composing the +theorems \isa{subst} and \isa{append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id}) +after which the appropriate rule of the grammar reduces the goal +to the two subgoals \isa{take\ i\ v\ {\isasymin}\ A} and \isa{drop\ i\ v\ {\isasymin}\ A}:% +\end{isamarkuptxt}% +\ \isamarkuptrue% +\isacommand{apply}{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +Both subgoals follow from the induction hypothesis because both \isa{take\ i\ v} and \isa{drop\ i\ v} are shorter than \isa{w}:% +\end{isamarkuptxt}% +\ \ \isamarkuptrue% +\isacommand{apply}{\isacharparenleft}force\ simp\ add{\isacharcolon}\ min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj{\isacharparenright}\isanewline +\ \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}force\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +The case \isa{w\ {\isacharequal}\ b\ {\isacharhash}\ v} is proved analogously:% +\end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% -\isamarkupfalse% -\isamarkuptrue% +\isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}frule\ part{\isadigit{1}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}b{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}drule\ part{\isadigit{2}}{\isacharbrackleft}of\ {\isachardoublequote}{\isasymlambda}x{\isachardot}\ x{\isacharequal}b{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline +\ \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}assumption{\isacharparenright}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ n{\isadigit{1}}{\isacharequal}i\ \isakeyword{and}\ t{\isacharequal}v\ \isakeyword{in}\ subst{\isacharbrackleft}OF\ append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharbrackright}{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharparenright}\isanewline +\ \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}force\ simp\ add{\isacharcolon}\ min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj{\isacharparenright}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{by}{\isacharparenleft}force\ simp\ add{\isacharcolon}\ min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}\isamarkupfalse% % \begin{isamarkuptext}% We conclude this section with a comparison of our proof with diff -r 0e7b145c3a89 -r 3f2a9f400168 doc-src/TutorialI/Inductive/document/Advanced.tex --- a/doc-src/TutorialI/Inductive/document/Advanced.tex Wed May 25 09:03:53 2005 +0200 +++ b/doc-src/TutorialI/Inductive/document/Advanced.tex Wed May 25 09:04:24 2005 +0200 @@ -22,11 +22,21 @@ \isamarkupfalse% \isacommand{lemma}\ gterms{\isacharunderscore}mono{\isacharcolon}\ {\isachardoublequote}F{\isasymsubseteq}G\ {\isasymLongrightarrow}\ gterms\ F\ {\isasymsubseteq}\ gterms\ G{\isachardoublequote}\isanewline \isamarkupfalse% +\isacommand{apply}\ clarify\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{apply}\ {\isacharparenleft}erule\ gterms{\isachardot}induct{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ args\ f{\isachardot}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}F\ {\isasymsubseteq}\ G{\isacharsemicolon}\ {\isasymforall}t{\isasymin}set\ args{\isachardot}\ t\ {\isasymin}\ gterms\ F\ {\isasymand}\ t\ {\isasymin}\ gterms\ G{\isacharsemicolon}\ f\ {\isasymin}\ F{\isasymrbrakk}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ gterms\ G% +\end{isabelle}% +\end{isamarkuptxt}% \isamarkuptrue% +\isacommand{apply}\ blast\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{done}\isamarkupfalse% % \begin{isamarkuptext}% \begin{isabelle}% @@ -57,7 +67,9 @@ \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}Suc{\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even\ {\isasymLongrightarrow}\ P\ n{\isachardoublequote}\isanewline \isamarkupfalse% +\isacommand{apply}\ {\isacharparenleft}ind{\isacharunderscore}cases\ {\isachardoublequote}Suc{\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even{\isachardoublequote}{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{oops}\isanewline \isanewline \isamarkupfalse% \isacommand{inductive{\isacharunderscore}cases}\ gterm{\isacharunderscore}Apply{\isacharunderscore}elim\ {\isacharbrackleft}elim{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}Apply\ f\ args\ {\isasymin}\ gterms\ F{\isachardoublequote}\isamarkupfalse% @@ -74,10 +86,22 @@ \isacommand{lemma}\ gterms{\isacharunderscore}IntI\ {\isacharbrackleft}rule{\isacharunderscore}format{\isacharcomma}\ intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\isanewline \ \ \ \ \ {\isachardoublequote}t\ {\isasymin}\ gterms\ F\ {\isasymLongrightarrow}\ t\ {\isasymin}\ gterms\ G\ {\isasymlongrightarrow}\ t\ {\isasymin}\ gterms\ {\isacharparenleft}F{\isasyminter}G{\isacharparenright}{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{apply}\ {\isacharparenleft}erule\ gterms{\isachardot}induct{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}args\ f{\isachardot}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}{\isasymforall}t{\isasymin}set\ args{\isachardot}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}\ \ \ }t\ {\isasymin}\ gterms\ F\ {\isasymand}\ {\isacharparenleft}t\ {\isasymin}\ gterms\ G\ {\isasymlongrightarrow}\ t\ {\isasymin}\ gterms\ {\isacharparenleft}F\ {\isasyminter}\ G{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }f\ {\isasymin}\ F{\isasymrbrakk}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ gterms\ G\ {\isasymlongrightarrow}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymLongrightarrow}\ }Apply\ f\ args\ {\isasymin}\ gterms\ {\isacharparenleft}F\ {\isasyminter}\ G{\isacharparenright}% +\end{isabelle}% +\end{isamarkuptxt}% \isamarkuptrue% +\isacommand{apply}\ blast\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{done}\isamarkupfalse% % \begin{isamarkuptext}% \begin{isabelle}% @@ -89,7 +113,7 @@ \isacommand{lemma}\ gterms{\isacharunderscore}Int{\isacharunderscore}eq\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline \ \ \ \ \ {\isachardoublequote}gterms\ {\isacharparenleft}F{\isasyminter}G{\isacharparenright}\ {\isacharequal}\ gterms\ F\ {\isasyminter}\ gterms\ G{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{by}\ {\isacharparenleft}blast\ intro{\isacharbang}{\isacharcolon}\ mono{\isacharunderscore}Int\ monoI\ gterms{\isacharunderscore}mono{\isacharparenright}\isamarkupfalse% % \begin{isamarkuptext}% the following declaration isn't actually used% @@ -125,23 +149,67 @@ \isamarkupfalse% \isacommand{lemma}\ {\isachardoublequote}well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity\ {\isasymsubseteq}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{apply}\ clarify\isamarkupfalse% +% +\begin{isamarkuptxt}% +The situation after clarify +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity\ {\isasymLongrightarrow}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ }x\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity% +\end{isabelle}% +\end{isamarkuptxt}% \isamarkuptrue% +\isacommand{apply}\ {\isacharparenleft}erule\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isachardot}induct{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +note the induction hypothesis! +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ args\ f{\isachardot}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}{\isasymforall}t{\isasymin}set\ args{\isachardot}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}\ \ \ }t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity\ {\isasymand}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}\ \ \ }t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isacharsemicolon}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity% +\end{isabelle}% +\end{isamarkuptxt}% +\isamarkuptrue% +\isacommand{apply}\ auto\isanewline \isamarkupfalse% -\isamarkuptrue% -\isamarkupfalse% +\isacommand{done}\isanewline \isanewline \isanewline \isanewline \isamarkupfalse% \isacommand{lemma}\ {\isachardoublequote}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity\ {\isasymsubseteq}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{apply}\ clarify\isamarkupfalse% +% +\begin{isamarkuptxt}% +The situation after clarify +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity\ {\isasymLongrightarrow}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ }x\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity% +\end{isabelle}% +\end{isamarkuptxt}% \isamarkuptrue% +\isacommand{apply}\ {\isacharparenleft}erule\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}{\isachardot}induct{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +note the induction hypothesis! +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ args\ f{\isachardot}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}args\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}}{\isasymin}\ lists\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}{\isasymin}\ \ }{\isacharparenleft}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity\ {\isasyminter}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}{\isasymin}\ \ {\isacharparenleft}}{\isacharbraceleft}x{\isachardot}\ x\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isacharbraceright}{\isacharparenright}{\isacharsemicolon}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity% +\end{isabelle}% +\end{isamarkuptxt}% +\isamarkuptrue% +\isacommand{apply}\ auto\isanewline \isamarkupfalse% -\isamarkuptrue% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{done}\isamarkupfalse% % \begin{isamarkuptext}% \begin{isabelle}% @@ -190,16 +258,24 @@ \isamarkupfalse% \isacommand{lemma}\ {\isachardoublequote}well{\isacharunderscore}typed{\isacharunderscore}gterm\ sig\ {\isasymsubseteq}\ well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}\ sig{\isachardoublequote}\isanewline \isamarkupfalse% +\isacommand{apply}\ clarify\isanewline \isamarkupfalse% +\isacommand{apply}\ {\isacharparenleft}erule\ well{\isacharunderscore}typed{\isacharunderscore}gterm{\isachardot}induct{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{apply}\ auto\isanewline \isamarkupfalse% +\isacommand{done}\isanewline \isanewline \isamarkupfalse% \isacommand{lemma}\ {\isachardoublequote}well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}\ sig\ {\isasymsubseteq}\ well{\isacharunderscore}typed{\isacharunderscore}gterm\ sig{\isachardoublequote}\isanewline \isamarkupfalse% +\isacommand{apply}\ clarify\isanewline \isamarkupfalse% +\isacommand{apply}\ {\isacharparenleft}erule\ well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}{\isachardot}induct{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{apply}\ auto\isanewline \isamarkupfalse% +\isacommand{done}\isanewline \isanewline \isanewline \isamarkupfalse% diff -r 0e7b145c3a89 -r 3f2a9f400168 doc-src/TutorialI/Inductive/document/Even.tex --- a/doc-src/TutorialI/Inductive/document/Even.tex Wed May 25 09:03:53 2005 +0200 +++ b/doc-src/TutorialI/Inductive/document/Even.tex Wed May 25 09:04:24 2005 +0200 @@ -35,10 +35,22 @@ \isamarkuptrue% \isacommand{lemma}\ two{\isacharunderscore}times{\isacharunderscore}even{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isadigit{2}}{\isacharasterisk}k\ {\isasymin}\ even{\isachardoublequote}\isanewline \isamarkupfalse% +\isacommand{apply}\ {\isacharparenleft}induct{\isacharunderscore}tac\ k{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +The first step is induction on the natural number \isa{k}, which leaves +two subgoals: +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isadigit{2}}\ {\isacharasterisk}\ {\isadigit{0}}\ {\isasymin}\ Even{\isachardot}even\isanewline +\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isadigit{2}}\ {\isacharasterisk}\ n\ {\isasymin}\ Even{\isachardot}even\ {\isasymLongrightarrow}\ {\isadigit{2}}\ {\isacharasterisk}\ Suc\ n\ {\isasymin}\ Even{\isachardot}even% +\end{isabelle} +Here \isa{auto} simplifies both subgoals so that they match the introduction +rules, which then are applied automatically.% +\end{isamarkuptxt}% +\ \isamarkuptrue% +\isacommand{apply}\ auto\isanewline \isamarkupfalse% -\isamarkuptrue% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{done}\isamarkupfalse% % \begin{isamarkuptext}% Our goal is to prove the equivalence between the traditional definition @@ -49,7 +61,7 @@ \isamarkuptrue% \isacommand{lemma}\ dvd{\isacharunderscore}imp{\isacharunderscore}even{\isacharcolon}\ {\isachardoublequote}{\isadigit{2}}\ dvd\ n\ {\isasymLongrightarrow}\ n\ {\isasymin}\ even{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{by}\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ dvd{\isacharunderscore}def{\isacharparenright}\isamarkupfalse% % \begin{isamarkuptext}% our first rule induction!% @@ -57,14 +69,34 @@ \isamarkuptrue% \isacommand{lemma}\ even{\isacharunderscore}imp{\isacharunderscore}dvd{\isacharcolon}\ {\isachardoublequote}n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isadigit{2}}\ dvd\ n{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkuptrue% -\isamarkupfalse% +\isacommand{apply}\ {\isacharparenleft}erule\ even{\isachardot}induct{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isadigit{2}}\ dvd\ {\isadigit{0}}\isanewline +\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ Even{\isachardot}even{\isacharsemicolon}\ {\isadigit{2}}\ dvd\ n{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isadigit{2}}\ dvd\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}% +\end{isabelle}% +\end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% +\isacommand{apply}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ dvd{\isacharunderscore}def{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ Even{\isachardot}even{\isacharsemicolon}\ {\isasymexists}k{\isachardot}\ n\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ k{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isasymexists}k{\isachardot}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ k% +\end{isabelle}% +\end{isamarkuptxt}% \isamarkuptrue% +\isacommand{apply}\ clarify\isamarkupfalse% +% +\begin{isamarkuptxt}% +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n\ k{\isachardot}\ {\isadigit{2}}\ {\isacharasterisk}\ k\ {\isasymin}\ Even{\isachardot}even\ {\isasymLongrightarrow}\ {\isasymexists}ka{\isachardot}\ Suc\ {\isacharparenleft}Suc\ {\isacharparenleft}{\isadigit{2}}\ {\isacharasterisk}\ k{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ ka% +\end{isabelle}% +\end{isamarkuptxt}% +\isamarkuptrue% +\isacommand{apply}\ {\isacharparenleft}rule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}Suc\ k{\isachardoublequote}\ \isakeyword{in}\ exI{\isacharcomma}\ simp{\isacharparenright}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{done}\isamarkupfalse% % \begin{isamarkuptext}% no iff-attribute because we don't always want to use it% @@ -72,7 +104,7 @@ \isamarkuptrue% \isacommand{theorem}\ even{\isacharunderscore}iff{\isacharunderscore}dvd{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}n\ {\isasymin}\ even{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{2}}\ dvd\ n{\isacharparenright}{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{by}\ {\isacharparenleft}blast\ intro{\isacharcolon}\ dvd{\isacharunderscore}imp{\isacharunderscore}even\ even{\isacharunderscore}imp{\isacharunderscore}dvd{\isacharparenright}\isamarkupfalse% % \begin{isamarkuptext}% this result ISN'T inductive...% @@ -80,9 +112,16 @@ \isamarkuptrue% \isacommand{lemma}\ Suc{\isacharunderscore}Suc{\isacharunderscore}even{\isacharunderscore}imp{\isacharunderscore}even{\isacharcolon}\ {\isachardoublequote}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even\ {\isasymLongrightarrow}\ n\ {\isasymin}\ even{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{apply}\ {\isacharparenleft}erule\ even{\isachardot}induct{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ n\ {\isasymin}\ Even{\isachardot}even\isanewline +\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}na{\isachardot}\ {\isasymlbrakk}na\ {\isasymin}\ Even{\isachardot}even{\isacharsemicolon}\ n\ {\isasymin}\ Even{\isachardot}even{\isasymrbrakk}\ {\isasymLongrightarrow}\ n\ {\isasymin}\ Even{\isachardot}even% +\end{isabelle}% +\end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% +\isacommand{oops}\isamarkupfalse% % \begin{isamarkuptext}% ...so we need an inductive lemma...% @@ -90,10 +129,19 @@ \isamarkuptrue% \isacommand{lemma}\ even{\isacharunderscore}imp{\isacharunderscore}even{\isacharunderscore}minus{\isacharunderscore}{\isadigit{2}}{\isacharcolon}\ {\isachardoublequote}n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ n\ {\isacharminus}\ {\isadigit{2}}\ {\isasymin}\ even{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{apply}\ {\isacharparenleft}erule\ even{\isachardot}induct{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isadigit{0}}\ {\isacharminus}\ {\isadigit{2}}\ {\isasymin}\ Even{\isachardot}even\isanewline +\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ Even{\isachardot}even{\isacharsemicolon}\ n\ {\isacharminus}\ {\isadigit{2}}\ {\isasymin}\ Even{\isachardot}even{\isasymrbrakk}\isanewline +\isaindent{\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ }{\isasymLongrightarrow}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharminus}\ {\isadigit{2}}\ {\isasymin}\ Even{\isachardot}even% +\end{isabelle}% +\end{isamarkuptxt}% \isamarkuptrue% +\isacommand{apply}\ auto\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{done}\isamarkupfalse% % \begin{isamarkuptext}% ...and prove it in a separate step% @@ -101,11 +149,13 @@ \isamarkuptrue% \isacommand{lemma}\ Suc{\isacharunderscore}Suc{\isacharunderscore}even{\isacharunderscore}imp{\isacharunderscore}even{\isacharcolon}\ {\isachardoublequote}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even\ {\isasymLongrightarrow}\ n\ {\isasymin}\ even{\isachardoublequote}\isanewline \isamarkupfalse% +\isacommand{by}\ {\isacharparenleft}drule\ even{\isacharunderscore}imp{\isacharunderscore}even{\isacharunderscore}minus{\isacharunderscore}{\isadigit{2}}{\isacharcomma}\ simp{\isacharparenright}\isanewline \isanewline \isanewline \isamarkupfalse% \isacommand{lemma}\ {\isacharbrackleft}iff{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}\ {\isasymin}\ even{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}n\ {\isasymin}\ even{\isacharparenright}{\isachardoublequote}\isanewline \isamarkupfalse% +\isacommand{by}\ {\isacharparenleft}blast\ dest{\isacharcolon}\ Suc{\isacharunderscore}Suc{\isacharunderscore}even{\isacharunderscore}imp{\isacharunderscore}even{\isacharparenright}\isanewline \isanewline \isamarkupfalse% \isacommand{end}\isanewline diff -r 0e7b145c3a89 -r 3f2a9f400168 doc-src/TutorialI/Inductive/document/Mutual.tex --- a/doc-src/TutorialI/Inductive/document/Mutual.tex Wed May 25 09:03:53 2005 +0200 +++ b/doc-src/TutorialI/Inductive/document/Mutual.tex Wed May 25 09:04:24 2005 +0200 @@ -39,8 +39,27 @@ \end{isamarkuptext}% \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}m\ {\isasymin}\ even\ {\isasymlongrightarrow}\ {\isadigit{2}}\ dvd\ m{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}n\ {\isasymin}\ odd\ {\isasymlongrightarrow}\ {\isadigit{2}}\ dvd\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +The proof is by rule induction. Because of the form of the induction theorem, +it is applied by \isa{rule} rather than \isa{erule} as for ordinary +inductive definitions:% +\end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}rule\ even{\isacharunderscore}odd{\isachardot}induct{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isadigit{2}}\ dvd\ {\isadigit{0}}\isanewline +\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ odd{\isacharsemicolon}\ {\isadigit{2}}\ dvd\ Suc\ n{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isadigit{2}}\ dvd\ Suc\ n\isanewline +\ {\isadigit{3}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ Mutual{\isachardot}even{\isacharsemicolon}\ {\isadigit{2}}\ dvd\ n{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isadigit{2}}\ dvd\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}% +\end{isabelle} +The first two subgoals are proved by simplification and the final one can be +proved in the same manner as in \S\ref{sec:rule-induction} +where the same subgoal was encountered before. +We do not show the proof script.% +\end{isamarkuptxt}% \isamarkuptrue% \isamarkupfalse% \isamarkupfalse% @@ -48,7 +67,6 @@ \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% -\isanewline \isamarkupfalse% \isamarkupfalse% \end{isabellebody}% diff -r 0e7b145c3a89 -r 3f2a9f400168 doc-src/TutorialI/Inductive/document/Star.tex --- a/doc-src/TutorialI/Inductive/document/Star.tex Wed May 25 09:03:53 2005 +0200 +++ b/doc-src/TutorialI/Inductive/document/Star.tex Wed May 25 09:04:24 2005 +0200 @@ -47,7 +47,7 @@ \isamarkuptrue% \isacommand{lemma}\ {\isacharbrackleft}intro{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{by}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isacharunderscore}step{\isacharparenright}\isamarkupfalse% % \begin{isamarkuptext}% \noindent @@ -76,17 +76,69 @@ \isamarkuptrue% \isacommand{lemma}\ rtc{\isacharunderscore}trans{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}erule\ rtc{\isachardot}induct{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +Unfortunately, even the base case is a problem: +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ {\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}% +\end{isabelle} +We have to abandon this proof attempt. +To understand what is going on, let us look again at \isa{rtc{\isachardot}induct}. +In the above application of \isa{erule}, the first premise of +\isa{rtc{\isachardot}induct} is unified with the first suitable assumption, which +is \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}} rather than \isa{{\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}}. Although that +is what we want, it is merely due to the order in which the assumptions occur +in the subgoal, which it is not good practice to rely on. As a result, +\isa{{\isacharquery}xb} becomes \isa{x}, \isa{{\isacharquery}xa} becomes +\isa{y} and \isa{{\isacharquery}P} becomes \isa{{\isasymlambda}u\ v{\isachardot}\ {\isacharparenleft}u{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}}, thus +yielding the above subgoal. So what went wrong? + +When looking at the instantiation of \isa{{\isacharquery}P} we see that it does not +depend on its second parameter at all. The reason is that in our original +goal, of the pair \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}} only \isa{x} appears also in the +conclusion, but not \isa{y}. Thus our induction statement is too +weak. Fortunately, it can easily be strengthened: +transfer the additional premise \isa{{\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}} into the conclusion:% +\end{isamarkuptxt}% \isamarkuptrue% \isamarkupfalse% \isacommand{lemma}\ rtc{\isacharunderscore}trans{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\isanewline \ \ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isamarkupfalse% -\isamarkuptrue% -\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +This is not an obscure trick but a generally applicable heuristic: +\begin{quote}\em +When proving a statement by rule induction on $(x@1,\dots,x@n) \in R$, +pull all other premises containing any of the $x@i$ into the conclusion +using $\longrightarrow$. +\end{quote} +A similar heuristic for other kinds of inductions is formulated in +\S\ref{sec:ind-var-in-prems}. The \isa{rule{\isacharunderscore}format} directive turns +\isa{{\isasymlongrightarrow}} back into \isa{{\isasymLongrightarrow}}: in the end we obtain the original +statement of our lemma.% +\end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}erule\ rtc{\isachardot}induct{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +Now induction produces two subgoals which are both proved automatically: +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\isanewline +\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}x\ y\ za{\isachardot}\isanewline +\isaindent{\ {\isadigit{2}}{\isachardot}\ \ \ \ }{\isasymlbrakk}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ r{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}\ za{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isacharsemicolon}\ {\isacharparenleft}za{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isasymrbrakk}\isanewline +\isaindent{\ {\isadigit{2}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ {\isacharparenleft}za{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}% +\end{isabelle}% +\end{isamarkuptxt}% +\ \isamarkuptrue% +\isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isacharunderscore}step{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{done}\isamarkupfalse% % \begin{isamarkuptext}% Let us now prove that \isa{r{\isacharasterisk}} is really the reflexive transitive closure @@ -110,18 +162,26 @@ \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}erule\ rtc{\isadigit{2}}{\isachardot}induct{\isacharparenright}\isanewline +\ \ \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline +\ \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isacharunderscore}trans{\isacharparenright}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{done}\isanewline \isanewline \isamarkupfalse% \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}erule\ rtc{\isachardot}induct{\isacharparenright}\isanewline +\ \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isadigit{2}}{\isachardot}intros{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isadigit{2}}{\isachardot}intros{\isacharparenright}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{done}\isamarkupfalse% % \begin{isamarkuptext}% So why did we start with the first definition? Because it is simpler. It @@ -149,7 +209,6 @@ \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% -\isanewline \isamarkupfalse% \isamarkupfalse% \end{isabellebody}% diff -r 0e7b145c3a89 -r 3f2a9f400168 doc-src/TutorialI/IsaMakefile --- a/doc-src/TutorialI/IsaMakefile Wed May 25 09:03:53 2005 +0200 +++ b/doc-src/TutorialI/IsaMakefile Wed May 25 09:04:24 2005 +0200 @@ -17,7 +17,7 @@ SRC = $(ISABELLE_HOME)/src OUT = $(ISABELLE_OUTPUT) LOG = $(OUT)/log -OPTIONS = -m brackets -i true -d "" -D document +OPTIONS = -H false -m brackets -i true -d "" -D document USEDIR = @$(ISATOOL) usedir $(OPTIONS) $(OUT)/HOL REALUSEDIR = @$(ISATOOL) usedir $(OPTIONS) $(OUT)/HOL-Complex diff -r 0e7b145c3a89 -r 3f2a9f400168 doc-src/TutorialI/Misc/document/AdvancedInd.tex --- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex Wed May 25 09:03:53 2005 +0200 +++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex Wed May 25 09:04:24 2005 +0200 @@ -29,11 +29,99 @@ \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ last\ xs{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +But induction produces the warning +\begin{quote}\tt +Induction variable occurs also among premises! +\end{quote} +and leads to the base case +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd\ {\isacharparenleft}rev\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ last\ {\isacharbrackleft}{\isacharbrackright}% +\end{isabelle} +Simplification reduces the base case to this: +\begin{isabelle} +\ 1.\ xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd\ []\ =\ last\ [] +\end{isabelle} +We cannot prove this equality because we do not know what \isa{hd} and +\isa{last} return when applied to \isa{{\isacharbrackleft}{\isacharbrackright}}. + +We should not have ignored the warning. Because the induction +formula is only the conclusion, induction does not affect the occurrence of \isa{xs} in the premises. +Thus the case that should have been trivial +becomes unprovable. Fortunately, the solution is easy:\footnote{A similar +heuristic applies to rule inductions; see \S\ref{sec:rtc}.} +\begin{quote} +\emph{Pull all occurrences of the induction variable into the conclusion +using \isa{{\isasymlongrightarrow}}.} +\end{quote} +Thus we should state the lemma as an ordinary +implication~(\isa{{\isasymlongrightarrow}}), letting +\attrdx{rule_format} (\S\ref{sec:forward}) convert the +result to the usual \isa{{\isasymLongrightarrow}} form:% +\end{isamarkuptxt}% \isamarkuptrue% \isamarkupfalse% \isacommand{lemma}\ hd{\isacharunderscore}rev\ {\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ last\ xs{\isachardoublequote}\isamarkupfalse% \isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +This time, induction leaves us with a trivial base case: +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ hd\ {\isacharparenleft}rev\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ last\ {\isacharbrackleft}{\isacharbrackright}% +\end{isabelle} +And \isa{auto} completes the proof. + +If there are multiple premises $A@1$, \dots, $A@n$ containing the +induction variable, you should turn the conclusion $C$ into +\[ A@1 \longrightarrow \cdots A@n \longrightarrow C. \] +Additionally, you may also have to universally quantify some other variables, +which can yield a fairly complex conclusion. However, \isa{rule{\isacharunderscore}format} +can remove any number of occurrences of \isa{{\isasymforall}} and +\isa{{\isasymlongrightarrow}}. + +\index{induction!on a term}% +A second reason why your proposition may not be amenable to induction is that +you want to induct on a complex term, rather than a variable. In +general, induction on a term~$t$ requires rephrasing the conclusion~$C$ +as +\begin{equation}\label{eqn:ind-over-term} +\forall y@1 \dots y@n.~ x = t \longrightarrow C. +\end{equation} +where $y@1 \dots y@n$ are the free variables in $t$ and $x$ is a new variable. +Now you can perform induction on~$x$. An example appears in +\S\ref{sec:complete-ind} below. + +The very same problem may occur in connection with rule induction. Remember +that it requires a premise of the form $(x@1,\dots,x@k) \in R$, where $R$ is +some inductively defined set and the $x@i$ are variables. If instead we have +a premise $t \in R$, where $t$ is not just an $n$-tuple of variables, we +replace it with $(x@1,\dots,x@k) \in R$, and rephrase the conclusion $C$ as +\[ \forall y@1 \dots y@n.~ (x@1,\dots,x@k) = t \longrightarrow C. \] +For an example see \S\ref{sec:CTL-revisited} below. + +Of course, all premises that share free variables with $t$ need to be pulled into +the conclusion as well, under the \isa{{\isasymforall}}, again using \isa{{\isasymlongrightarrow}} as shown above. + +Readers who are puzzled by the form of statement +(\ref{eqn:ind-over-term}) above should remember that the +transformation is only performed to permit induction. Once induction +has been applied, the statement can be transformed back into something quite +intuitive. For example, applying wellfounded induction on $x$ (w.r.t.\ +$\prec$) to (\ref{eqn:ind-over-term}) and transforming the result a +little leads to the goal +\[ \bigwedge\overline{y}.\ + \forall \overline{z}.\ t\,\overline{z} \prec t\,\overline{y}\ \longrightarrow\ C\,\overline{z} + \ \Longrightarrow\ C\,\overline{y} \] +where $\overline{y}$ stands for $y@1 \dots y@n$ and the dependence of $t$ and +$C$ on the free variables of $t$ has been made explicit. +Unfortunately, this induction schema cannot be expressed as a +single theorem because it depends on the number of free variables in $t$ --- +the notation $\overline{y}$ is merely an informal device.% +\end{isamarkuptxt}% \isamarkuptrue% \isamarkupfalse% % @@ -82,14 +170,41 @@ \end{isamarkuptext}% \isamarkuptrue% \isacommand{lemma}\ f{\isacharunderscore}incr{\isacharunderscore}lem{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i{\isachardot}\ k\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isachardoublequote}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +To perform induction on \isa{k} using \isa{nat{\isacharunderscore}less{\isacharunderscore}induct}, we use +the same general induction method as for recursion induction (see +\S\ref{sec:recdef-induction}):% +\end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ k\ rule{\isacharcolon}\ nat{\isacharunderscore}less{\isacharunderscore}induct{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +We get the following proof state: +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymforall}m{\isacharless}n{\isachardot}\ {\isasymforall}i{\isachardot}\ m\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i\ {\isasymLongrightarrow}\ {\isasymforall}i{\isachardot}\ n\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i% +\end{isabelle} +After stripping the \isa{{\isasymforall}i}, the proof continues with a case +distinction on \isa{i}. The case \isa{i\ {\isacharequal}\ {\isadigit{0}}} is trivial and we focus on +the other case:% +\end{isamarkuptxt}% \isamarkuptrue% +\isacommand{apply}{\isacharparenleft}rule\ allI{\isacharparenright}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ i{\isacharparenright}\isanewline +\ \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n\ i\ nat{\isachardot}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}{\isasymforall}m{\isacharless}n{\isachardot}\ {\isasymforall}i{\isachardot}\ m\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isacharsemicolon}\ i\ {\isacharequal}\ Suc\ nat{\isasymrbrakk}\ {\isasymLongrightarrow}\ n\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i% +\end{isabelle}% +\end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% +\isacommand{by}{\isacharparenleft}blast\ intro{\isacharbang}{\isacharcolon}\ f{\isacharunderscore}ax\ Suc{\isacharunderscore}leI\ intro{\isacharcolon}\ le{\isacharunderscore}less{\isacharunderscore}trans{\isacharparenright}\isamarkupfalse% % \begin{isamarkuptext}% \noindent @@ -180,10 +295,18 @@ \isamarkuptrue% \isacommand{lemma}\ induct{\isacharunderscore}lem{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isasymAnd}n{\isacharcolon}{\isacharcolon}nat{\isachardot}\ {\isasymforall}m{\isacharless}n{\isachardot}\ P\ m\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymforall}m{\isacharless}n{\isachardot}\ P\ m{\isachardoublequote}\isanewline \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ n{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +The base case is vacuously true. For the induction step (\isa{m\ {\isacharless}\ Suc\ n}) we distinguish two cases: case \isa{m\ {\isacharless}\ n} is true by induction +hypothesis and case \isa{m\ {\isacharequal}\ n} follows from the assumption, again using +the induction hypothesis:% +\end{isamarkuptxt}% +\ \isamarkuptrue% +\isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline \isamarkupfalse% -\isamarkuptrue% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{by}{\isacharparenleft}blast\ elim{\isacharcolon}\ less{\isacharunderscore}SucE{\isacharparenright}\isamarkupfalse% % \begin{isamarkuptext}% \noindent @@ -202,7 +325,7 @@ \isamarkuptrue% \isacommand{theorem}\ nat{\isacharunderscore}less{\isacharunderscore}induct{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isasymAnd}n{\isacharcolon}{\isacharcolon}nat{\isachardot}\ {\isasymforall}m{\isacharless}n{\isachardot}\ P\ m\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}\ {\isasymLongrightarrow}\ P\ n{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{by}{\isacharparenleft}insert\ induct{\isacharunderscore}lem{\isacharcomma}\ blast{\isacharparenright}\isamarkupfalse% % \begin{isamarkuptext}% HOL already provides the mother of diff -r 0e7b145c3a89 -r 3f2a9f400168 doc-src/TutorialI/Misc/document/Itrev.tex --- a/doc-src/TutorialI/Misc/document/Itrev.tex Wed May 25 09:03:53 2005 +0200 +++ b/doc-src/TutorialI/Misc/document/Itrev.tex Wed May 25 09:04:24 2005 +0200 @@ -65,16 +65,61 @@ \end{isamarkuptext}% \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}itrev\ xs\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ rev\ xs{\isachardoublequote}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +There is no choice as to the induction variable, and we immediately simplify:% +\end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +Unfortunately, this attempt does not prove +the induction step: +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }itrev\ list\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ rev\ list\ {\isasymLongrightarrow}\ itrev\ list\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharequal}\ rev\ list\ {\isacharat}\ {\isacharbrackleft}a{\isacharbrackright}% +\end{isabelle} +The induction hypothesis is too weak. The fixed +argument,~\isa{{\isacharbrackleft}{\isacharbrackright}}, prevents it from rewriting the conclusion. +This example suggests a heuristic: +\begin{quote}\index{generalizing induction formulae}% +\emph{Generalize goals for induction by replacing constants by variables.} +\end{quote} +Of course one cannot do this na\"{\i}vely: \isa{itrev\ xs\ ys\ {\isacharequal}\ rev\ xs} is +just not true. The correct generalization is% +\end{isamarkuptxt}% \isamarkuptrue% \isamarkupfalse% \isacommand{lemma}\ {\isachardoublequote}itrev\ xs\ ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ ys{\isachardoublequote}\isamarkupfalse% \isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +If \isa{ys} is replaced by \isa{{\isacharbrackleft}{\isacharbrackright}}, the right-hand side simplifies to +\isa{rev\ xs}, as required. + +In this instance it was easy to guess the right generalization. +Other situations can require a good deal of creativity. + +Although we now have two variables, only \isa{xs} is suitable for +induction, and we repeat our proof attempt. Unfortunately, we are still +not there: +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }itrev\ list\ ys\ {\isacharequal}\ rev\ list\ {\isacharat}\ ys\ {\isasymLongrightarrow}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }itrev\ list\ {\isacharparenleft}a\ {\isacharhash}\ ys{\isacharparenright}\ {\isacharequal}\ rev\ list\ {\isacharat}\ a\ {\isacharhash}\ ys% +\end{isabelle} +The induction hypothesis is still too weak, but this time it takes no +intuition to generalize: the problem is that \isa{ys} is fixed throughout +the subgoal, but the induction hypothesis needs to be applied with +\isa{a\ {\isacharhash}\ ys} instead of \isa{ys}. Hence we prove the theorem +for all \isa{ys} instead of a fixed one:% +\end{isamarkuptxt}% \isamarkuptrue% \isamarkupfalse% \isacommand{lemma}\ {\isachardoublequote}{\isasymforall}ys{\isachardot}\ itrev\ xs\ ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ ys{\isachardoublequote}\isamarkupfalse% -\isanewline \isamarkupfalse% % \begin{isamarkuptext}% diff -r 0e7b145c3a89 -r 3f2a9f400168 doc-src/TutorialI/Misc/document/Plus.tex --- a/doc-src/TutorialI/Misc/document/Plus.tex Wed May 25 09:03:53 2005 +0200 +++ b/doc-src/TutorialI/Misc/document/Plus.tex Wed May 25 09:04:24 2005 +0200 @@ -19,10 +19,8 @@ \isamarkuptrue% \isamarkupfalse% \isamarkupfalse% -\isanewline \isamarkupfalse% \isacommand{lemma}\ {\isachardoublequote}plus\ m\ n\ {\isacharequal}\ m{\isacharplus}n{\isachardoublequote}\isamarkupfalse% -\isanewline \isamarkupfalse% \isamarkupfalse% \end{isabellebody}% diff -r 0e7b145c3a89 -r 3f2a9f400168 doc-src/TutorialI/Misc/document/Tree.tex --- a/doc-src/TutorialI/Misc/document/Tree.tex Wed May 25 09:03:53 2005 +0200 +++ b/doc-src/TutorialI/Misc/document/Tree.tex Wed May 25 09:04:24 2005 +0200 @@ -20,7 +20,6 @@ \isamarkuptrue% \isacommand{lemma}\ mirror{\isacharunderscore}mirror{\isacharcolon}\ {\isachardoublequote}mirror{\isacharparenleft}mirror\ t{\isacharparenright}\ {\isacharequal}\ t{\isachardoublequote}\isamarkupfalse% \isamarkupfalse% -\isanewline \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% @@ -33,7 +32,6 @@ \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}flatten{\isacharparenleft}mirror\ t{\isacharparenright}\ {\isacharequal}\ rev{\isacharparenleft}flatten\ t{\isacharparenright}{\isachardoublequote}\isamarkupfalse% \isamarkupfalse% -\isanewline \isamarkupfalse% \isamarkupfalse% \end{isabellebody}% diff -r 0e7b145c3a89 -r 3f2a9f400168 doc-src/TutorialI/Misc/document/Tree2.tex --- a/doc-src/TutorialI/Misc/document/Tree2.tex Wed May 25 09:03:53 2005 +0200 +++ b/doc-src/TutorialI/Misc/document/Tree2.tex Wed May 25 09:04:24 2005 +0200 @@ -20,10 +20,8 @@ \isamarkuptrue% \isamarkupfalse% \isamarkupfalse% -\isanewline \isamarkupfalse% \isacommand{lemma}\ {\isachardoublequote}flatten{\isadigit{2}}\ t\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ flatten\ t{\isachardoublequote}\isamarkupfalse% -\isanewline \isamarkupfalse% \isamarkupfalse% \end{isabellebody}% diff -r 0e7b145c3a89 -r 3f2a9f400168 doc-src/TutorialI/Misc/document/case_exprs.tex --- a/doc-src/TutorialI/Misc/document/case_exprs.tex Wed May 25 09:03:53 2005 +0200 +++ b/doc-src/TutorialI/Misc/document/case_exprs.tex Wed May 25 09:04:24 2005 +0200 @@ -67,9 +67,20 @@ \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbar}\ y{\isacharhash}ys\ {\isasymRightarrow}\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ xs{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +results in the proof state +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ {\isacharparenleft}case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbar}\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ xs{\isacharparenright}\ {\isacharequal}\ xs\isanewline +\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline +\isaindent{\ {\isadigit{2}}{\isachardot}\ \ \ \ }xs\ {\isacharequal}\ a\ {\isacharhash}\ list\ {\isasymLongrightarrow}\ {\isacharparenleft}case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbar}\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ xs{\isacharparenright}\ {\isacharequal}\ xs% +\end{isabelle} +which is solved automatically:% +\end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isamarkupfalse% \isamarkupfalse% % \begin{isamarkuptext}% diff -r 0e7b145c3a89 -r 3f2a9f400168 doc-src/TutorialI/Misc/document/natsum.tex --- a/doc-src/TutorialI/Misc/document/natsum.tex Wed May 25 09:03:53 2005 +0200 +++ b/doc-src/TutorialI/Misc/document/natsum.tex Wed May 25 09:04:24 2005 +0200 @@ -24,9 +24,11 @@ \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}sum\ n\ {\isacharplus}\ sum\ n\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}Suc\ n{\isacharparenright}{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ n{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{done}\isamarkupfalse% % \begin{isamarkuptext}% \newcommand{\mystar}{*% @@ -107,7 +109,7 @@ \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}min\ i\ {\isacharparenleft}max\ j\ {\isacharparenleft}k{\isacharasterisk}k{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ max\ {\isacharparenleft}min\ {\isacharparenleft}k{\isacharasterisk}k{\isacharparenright}\ i{\isacharparenright}\ {\isacharparenleft}min\ i\ {\isacharparenleft}j{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}arith{\isacharparenright}\isamarkupfalse% \isamarkupfalse% % \begin{isamarkuptext}% diff -r 0e7b145c3a89 -r 3f2a9f400168 doc-src/TutorialI/Misc/document/simp.tex --- a/doc-src/TutorialI/Misc/document/simp.tex Wed May 25 09:03:53 2005 +0200 +++ b/doc-src/TutorialI/Misc/document/simp.tex Wed May 25 09:04:24 2005 +0200 @@ -114,8 +114,9 @@ \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}{\isasymlbrakk}\ xs\ {\isacharat}\ zs\ {\isacharequal}\ ys\ {\isacharat}\ xs{\isacharsemicolon}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ ys\ {\isacharequal}\ zs{\isachardoublequote}\isanewline \isamarkupfalse% +\isacommand{apply}\ simp\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{done}\isamarkupfalse% % \begin{isamarkuptext}% \noindent @@ -127,9 +128,19 @@ \end{isamarkuptext}% \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}{\isasymforall}x{\isachardot}\ f\ x\ {\isacharequal}\ g\ {\isacharparenleft}f\ {\isacharparenleft}g\ x{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ f\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ f\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +An unmodified application of \isa{simp} loops. The culprit is the +simplification rule \isa{f\ x\ {\isacharequal}\ g\ {\isacharparenleft}f\ {\isacharparenleft}g\ x{\isacharparenright}{\isacharparenright}}, which is extracted from +the assumption. (Isabelle notices certain simple forms of +nontermination but not this one.) The problem can be circumvented by +telling the simplifier to ignore the assumptions:% +\end{isamarkuptxt}% \isamarkuptrue% +\isacommand{apply}{\isacharparenleft}simp\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isacharparenright}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{done}\isamarkupfalse% % \begin{isamarkuptext}% \noindent @@ -187,12 +198,27 @@ \end{isamarkuptext}% \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}xor\ A\ {\isacharparenleft}{\isasymnot}A{\isacharparenright}{\isachardoublequote}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +Typically, we begin by unfolding some definitions: +\indexbold{definitions!unfolding}% +\end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ xor{\isacharunderscore}def{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +In this particular case, the resulting goal +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ A\ {\isasymand}\ {\isasymnot}\ {\isasymnot}\ A\ {\isasymor}\ {\isasymnot}\ A\ {\isasymand}\ {\isasymnot}\ A% +\end{isabelle} +can be proved by simplification. Thus we could have proved the lemma outright by% +\end{isamarkuptxt}% \isamarkuptrue% \isamarkupfalse% \isamarkupfalse% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ xor{\isacharunderscore}def{\isacharparenright}\isamarkupfalse% \isamarkupfalse% % \begin{isamarkuptext}% @@ -229,8 +255,9 @@ \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}let\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ in\ xs{\isacharat}ys{\isacharat}xs{\isacharparenright}\ {\isacharequal}\ ys{\isachardoublequote}\isanewline \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ Let{\isacharunderscore}def{\isacharparenright}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{done}\isamarkupfalse% % \begin{isamarkuptext}% If, in a particular context, there is no danger of a combinatorial explosion @@ -252,8 +279,9 @@ \isamarkuptrue% \isacommand{lemma}\ hd{\isacharunderscore}Cons{\isacharunderscore}tl{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ \ {\isasymLongrightarrow}\ \ hd\ xs\ {\isacharhash}\ tl\ xs\ {\isacharequal}\ xs{\isachardoublequote}\isanewline \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharcomma}\ simp{\isacharparenright}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{done}\isamarkupfalse% % \begin{isamarkuptext}% \noindent @@ -265,7 +293,6 @@ \end{isamarkuptext}% \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharhash}\ tl{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ rev\ xs{\isachardoublequote}\isamarkupfalse% -\isanewline \isamarkupfalse% % \begin{isamarkuptext}% @@ -290,18 +317,51 @@ \end{isamarkuptext}% \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}{\isasymforall}xs{\isachardot}\ if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ rev\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ else\ rev\ xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +The goal can be split by a special method, \methdx{split}:% +\end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}split\ split{\isacharunderscore}if{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isasymforall}xs{\isachardot}\ {\isacharparenleft}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ rev\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ rev\ xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}% +\end{isabelle} +where \tdx{split_if} is a theorem that expresses splitting of +\isa{if}s. Because +splitting the \isa{if}s is usually the right proof strategy, the +simplifier does it automatically. Try \isacommand{apply}\isa{{\isacharparenleft}simp{\isacharparenright}} +on the initial goal above. + +This splitting idea generalizes from \isa{if} to \sdx{case}. +Let us simplify a case analysis over lists:\index{*list.split (theorem)}% +\end{isamarkuptxt}% \isamarkuptrue% \isamarkupfalse% \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ zs\ {\isacharbar}\ y{\isacharhash}ys\ {\isasymRightarrow}\ y{\isacharhash}{\isacharparenleft}ys{\isacharat}zs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ xs{\isacharat}zs{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}split\ list{\isachardot}split{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isacharparenleft}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ zs\ {\isacharequal}\ xs\ {\isacharat}\ zs{\isacharparenright}\ {\isasymand}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ }{\isacharparenleft}{\isasymforall}a\ list{\isachardot}\ xs\ {\isacharequal}\ a\ {\isacharhash}\ list\ {\isasymlongrightarrow}\ a\ {\isacharhash}\ list\ {\isacharat}\ zs\ {\isacharequal}\ xs\ {\isacharat}\ zs{\isacharparenright}% +\end{isabelle} +The simplifier does not split +\isa{case}-expressions, as it does \isa{if}-expressions, +because with recursive datatypes it could lead to nontermination. +Instead, the simplifier has a modifier +\isa{split}\index{*split (modifier)} +for adding splitting rules explicitly. The +lemma above can be proved in one step by% +\end{isamarkuptxt}% \isamarkuptrue% -\isanewline \isamarkupfalse% \isamarkupfalse% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}simp\ split{\isacharcolon}\ list{\isachardot}split{\isacharparenright}\isamarkupfalse% \isamarkupfalse% % \begin{isamarkuptext}% @@ -322,8 +382,7 @@ \end{isamarkuptext}% \isamarkuptrue% \isamarkupfalse% -\isamarkupfalse% -\isanewline +\isacommand{apply}{\isacharparenleft}simp\ split\ del{\isacharcolon}\ split{\isacharunderscore}if{\isacharparenright}\isamarkupfalse% \isamarkupfalse% % \begin{isamarkuptext}% @@ -348,9 +407,31 @@ \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ ys\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ else\ ys\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ xs\ {\isacharat}\ ys\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}split\ split{\isacharunderscore}if{\isacharunderscore}asm{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +Unlike splitting the conclusion, this step creates two +separate subgoals, which here can be solved by \isa{simp{\isacharunderscore}all}: +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isasymlbrakk}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\ ys\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ xs\ {\isacharat}\ ys\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\isanewline +\ {\isadigit{2}}{\isachardot}\ {\isasymlbrakk}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\ ys\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ xs\ {\isacharat}\ ys\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}% +\end{isabelle} +If you need to split both in the assumptions and the conclusion, +use $t$\isa{{\isachardot}splits} which subsumes $t$\isa{{\isachardot}split} and +$t$\isa{{\isachardot}split{\isacharunderscore}asm}. Analogously, there is \isa{if{\isacharunderscore}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}% +\end{isamarkuptxt}% \isamarkuptrue% -\isanewline \isamarkupfalse% % \isamarkupsubsection{Tracing% @@ -365,10 +446,11 @@ on:% \end{isamarkuptext}% \isamarkuptrue% +\isacommand{ML}\ {\isachardoublequote}set\ trace{\isacharunderscore}simp{\isachardoublequote}\isanewline \isamarkupfalse% \isacommand{lemma}\ {\isachardoublequote}rev\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isamarkupfalse% \isamarkupfalse% % \begin{isamarkuptext}% @@ -405,6 +487,7 @@ rules. Thus it is advisable to reset it:% \end{isamarkuptext}% \isamarkuptrue% +\isacommand{ML}\ {\isachardoublequote}reset\ trace{\isacharunderscore}simp{\isachardoublequote}\isanewline \isamarkupfalse% \isamarkupfalse% \end{isabellebody}% diff -r 0e7b145c3a89 -r 3f2a9f400168 doc-src/TutorialI/Recdef/document/Induction.tex --- a/doc-src/TutorialI/Recdef/document/Induction.tex Wed May 25 09:03:53 2005 +0200 +++ b/doc-src/TutorialI/Recdef/document/Induction.tex Wed May 25 09:04:24 2005 +0200 @@ -21,11 +21,33 @@ \end{isamarkuptext}% \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}map\ f\ {\isacharparenleft}sep{\isacharparenleft}x{\isacharcomma}xs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sep{\isacharparenleft}f\ x{\isacharcomma}\ map\ f\ xs{\isacharparenright}{\isachardoublequote}\isamarkupfalse% -\isamarkuptrue% -\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +Note that \isa{map\ f\ xs} +is the result of applying \isa{f} to all elements of \isa{xs}. We prove +this lemma by recursion induction over \isa{sep}:% +\end{isamarkuptxt}% \isamarkuptrue% +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ x\ xs\ rule{\isacharcolon}\ sep{\isachardot}induct{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +The resulting proof state has three subgoals corresponding to the three +clauses for \isa{sep}: +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a{\isachardot}\ map\ f\ {\isacharparenleft}sep\ {\isacharparenleft}a{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sep\ {\isacharparenleft}f\ a{\isacharcomma}\ map\ f\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline +\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}a\ x{\isachardot}\ map\ f\ {\isacharparenleft}sep\ {\isacharparenleft}a{\isacharcomma}\ {\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sep\ {\isacharparenleft}f\ a{\isacharcomma}\ map\ f\ {\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}\isanewline +\ {\isadigit{3}}{\isachardot}\ {\isasymAnd}a\ x\ y\ zs{\isachardot}\isanewline +\isaindent{\ {\isadigit{3}}{\isachardot}\ \ \ \ }map\ f\ {\isacharparenleft}sep\ {\isacharparenleft}a{\isacharcomma}\ y\ {\isacharhash}\ zs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sep\ {\isacharparenleft}f\ a{\isacharcomma}\ map\ f\ {\isacharparenleft}y\ {\isacharhash}\ zs{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\isanewline +\isaindent{\ {\isadigit{3}}{\isachardot}\ \ \ \ }map\ f\ {\isacharparenleft}sep\ {\isacharparenleft}a{\isacharcomma}\ x\ {\isacharhash}\ y\ {\isacharhash}\ zs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sep\ {\isacharparenleft}f\ a{\isacharcomma}\ map\ f\ {\isacharparenleft}x\ {\isacharhash}\ y\ {\isacharhash}\ zs{\isacharparenright}{\isacharparenright}% +\end{isabelle} +The rest is pure simplification:% +\end{isamarkuptxt}% +\isamarkuptrue% +\isacommand{apply}\ simp{\isacharunderscore}all\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{done}\isamarkupfalse% % \begin{isamarkuptext}% Try proving the above lemma by structural induction, and you find that you diff -r 0e7b145c3a89 -r 3f2a9f400168 doc-src/TutorialI/Recdef/document/Nested2.tex --- a/doc-src/TutorialI/Recdef/document/Nested2.tex Wed May 25 09:03:53 2005 +0200 +++ b/doc-src/TutorialI/Recdef/document/Nested2.tex Wed May 25 09:04:24 2005 +0200 @@ -5,8 +5,7 @@ \isamarkupfalse% \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}t\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ size\ t\ {\isacharless}\ Suc{\isacharparenleft}term{\isacharunderscore}list{\isacharunderscore}size\ ts{\isacharparenright}{\isachardoublequote}\isanewline \isamarkupfalse% -\isanewline -\isamarkupfalse% +\isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ ts{\isacharcomma}\ auto{\isacharparenright}\isamarkupfalse% \isamarkupfalse% % \begin{isamarkuptext}% @@ -21,9 +20,19 @@ \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}trev{\isacharparenleft}trev\ t{\isacharparenright}\ {\isacharequal}\ t{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ t\ rule{\isacharcolon}\ trev{\isachardot}induct{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ trev\ {\isacharparenleft}trev\ {\isacharparenleft}Var\ x{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ Var\ x\isanewline +\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}f\ ts{\isachardot}\isanewline +\isaindent{\ {\isadigit{2}}{\isachardot}\ \ \ \ }{\isasymforall}x{\isachardot}\ x\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ trev\ {\isacharparenleft}trev\ x{\isacharparenright}\ {\isacharequal}\ x\ {\isasymLongrightarrow}\isanewline +\isaindent{\ {\isadigit{2}}{\isachardot}\ \ \ \ }trev\ {\isacharparenleft}trev\ {\isacharparenleft}App\ f\ ts{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ App\ f\ ts% +\end{isabelle} +Both the base case and the induction step fall to simplification:% +\end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% +\isacommand{by}{\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ rev{\isacharunderscore}map\ sym{\isacharbrackleft}OF\ map{\isacharunderscore}compose{\isacharbrackright}\ cong{\isacharcolon}\ map{\isacharunderscore}cong{\isacharparenright}\isamarkupfalse% % \begin{isamarkuptext}% \noindent diff -r 0e7b145c3a89 -r 3f2a9f400168 doc-src/TutorialI/Recdef/document/simplification.tex --- a/doc-src/TutorialI/Recdef/document/simplification.tex Wed May 25 09:03:53 2005 +0200 +++ b/doc-src/TutorialI/Recdef/document/simplification.tex Wed May 25 09:04:24 2005 +0200 @@ -94,13 +94,16 @@ \isamarkuptrue% \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}gcd\ {\isacharparenleft}m{\isacharcomma}\ {\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ m{\isachardoublequote}\isanewline \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{done}\isanewline \isanewline \isamarkupfalse% \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}n\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ gcd{\isacharparenleft}m{\isacharcomma}\ n{\isacharparenright}\ {\isacharequal}\ gcd{\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}{\isachardoublequote}\isanewline \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{done}\isamarkupfalse% % \begin{isamarkuptext}% \noindent diff -r 0e7b145c3a89 -r 3f2a9f400168 doc-src/TutorialI/Recdef/document/termination.tex --- a/doc-src/TutorialI/Recdef/document/termination.tex Wed May 25 09:03:53 2005 +0200 +++ b/doc-src/TutorialI/Recdef/document/termination.tex Wed May 25 09:04:24 2005 +0200 @@ -65,8 +65,9 @@ \isamarkuptrue% \isacommand{theorem}\ {\isachardoublequote}qs{\isacharbrackleft}{\isadigit{2}}{\isacharcomma}{\isadigit{3}}{\isacharcomma}{\isadigit{0}}{\isacharbrackright}\ {\isacharequal}\ qs{\isacharbrackleft}{\isadigit{3}}{\isacharcomma}{\isadigit{0}}{\isacharcomma}{\isadigit{2}}{\isacharbrackright}{\isachardoublequote}\isanewline \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{done}\isamarkupfalse% % \begin{isamarkuptext}% \noindent diff -r 0e7b145c3a89 -r 3f2a9f400168 doc-src/TutorialI/ToyList/document/ToyList.tex --- a/doc-src/TutorialI/ToyList/document/ToyList.tex Wed May 25 09:03:53 2005 +0200 +++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Wed May 25 09:04:24 2005 +0200 @@ -136,12 +136,99 @@ \end{isamarkuptext}% \isamarkuptrue% \isacommand{theorem}\ rev{\isacharunderscore}rev\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}\isamarkupfalse% -\isamarkuptrue% -\isamarkupfalse% +% +\begin{isamarkuptxt}% +\index{theorem@\isacommand {theorem} (command)|bold}% +\noindent +This \isacommand{theorem} command does several things: +\begin{itemize} +\item +It establishes a new theorem to be proved, namely \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs}. +\item +It gives that theorem the name \isa{rev{\isacharunderscore}rev}, for later reference. +\item +It tells Isabelle (via the bracketed attribute \attrdx{simp}) to take the eventual theorem as a simplification rule: future proofs involving +simplification will replace occurrences of \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}} by +\isa{xs}. +\end{itemize} +The name and the simplification attribute are optional. +Isabelle's response is to print the initial proof state consisting +of some header information (like how many subgoals there are) followed by +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs% +\end{isabelle} +For compactness reasons we omit the header in this tutorial. +Until we have finished a proof, the \rmindex{proof state} proper +always looks like this: +\begin{isabelle} +~1.~$G\sb{1}$\isanewline +~~\vdots~~\isanewline +~$n$.~$G\sb{n}$ +\end{isabelle} +The numbered lines contain the subgoals $G\sb{1}$, \dots, $G\sb{n}$ +that we need to prove to establish the main goal.\index{subgoals} +Initially there is only one subgoal, which is identical with the +main goal. (If you always want to see the main goal as well, +set the flag \isa{Proof.show_main_goal}\index{*show_main_goal (flag)} +--- this flag used to be set by default.) + +Let us now get back to \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs}. Properties of recursively +defined functions are best established by induction. In this case there is +nothing obvious except induction on \isa{xs}:% +\end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent\index{*induct_tac (method)}% +This tells Isabelle to perform induction on variable \isa{xs}. The suffix +\isa{tac} stands for \textbf{tactic},\index{tactics} +a synonym for ``theorem proving function''. +By default, induction acts on the first subgoal. The new proof state contains +two subgoals, namely the base case (\isa{Nil}) and the induction step +(\isa{Cons}): +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ rev\ {\isacharparenleft}rev\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\isanewline +\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline +\isaindent{\ {\isadigit{2}}{\isachardot}\ \ \ \ }rev\ {\isacharparenleft}rev\ list{\isacharparenright}\ {\isacharequal}\ list\ {\isasymLongrightarrow}\ rev\ {\isacharparenleft}rev\ {\isacharparenleft}a\ {\isacharhash}\ list{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ a\ {\isacharhash}\ list% +\end{isabelle} + +The induction step is an example of the general format of a subgoal:\index{subgoals} +\begin{isabelle} +~$i$.~{\isasymAnd}$x\sb{1}$~\dots$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion} +\end{isabelle}\index{$IsaAnd@\isasymAnd|bold} +The prefix of bound variables \isasymAnd$x\sb{1}$~\dots~$x\sb{n}$ can be +ignored most of the time, or simply treated as a list of variables local to +this subgoal. Their deeper significance is explained in Chapter~\ref{chap:rules}. +The {\it assumptions}\index{assumptions!of subgoal} +are the local assumptions for this subgoal and {\it + conclusion}\index{conclusion!of subgoal} is the actual proposition to be proved. +Typical proof steps +that add new assumptions are induction and case distinction. In our example +the only assumption is the induction hypothesis \isa{rev\ {\isacharparenleft}rev\ list{\isacharparenright}\ {\isacharequal}\ list}, where \isa{list} is a variable name chosen by Isabelle. If there +are multiple assumptions, they are enclosed in the bracket pair +\indexboldpos{\isasymlbrakk}{$Isabrl} and +\indexboldpos{\isasymrbrakk}{$Isabrr} and separated by semicolons. + +Let us try to solve both goals automatically:% +\end{isamarkuptxt}% \isamarkuptrue% -\isanewline +\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +This command tells Isabelle to apply a proof strategy called +\isa{auto} to all subgoals. Essentially, \isa{auto} tries to +simplify the subgoals. In our case, subgoal~1 is solved completely (thanks +to the equation \isa{rev\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}}) and disappears; the simplified version +of subgoal~2 becomes the new subgoal~1: +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }rev\ {\isacharparenleft}rev\ list{\isacharparenright}\ {\isacharequal}\ list\ {\isasymLongrightarrow}\ rev\ {\isacharparenleft}rev\ list\ {\isacharat}\ a\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ a\ {\isacharhash}\ list% +\end{isabelle} +In order to simplify this subgoal further, a lemma suggests itself.% +\end{isamarkuptxt}% +\isamarkuptrue% \isamarkupfalse% % \isamarkupsubsubsection{First Lemma% @@ -155,12 +242,36 @@ \end{isamarkuptext}% \isamarkuptrue% \isacommand{lemma}\ rev{\isacharunderscore}app\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}rev\ ys{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isachardoublequote}\isamarkupfalse% -\isamarkuptrue% -\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent The keywords \commdx{theorem} and +\commdx{lemma} are interchangeable and merely indicate +the importance we attach to a proposition. Therefore we use the words +\emph{theorem} and \emph{lemma} pretty much interchangeably, too. + +There are two variables that we could induct on: \isa{xs} and +\isa{ys}. Because \isa{{\isacharat}} is defined by recursion on +the first argument, \isa{xs} is the correct one:% +\end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +This time not even the base case is solved automatically:% +\end{isamarkuptxt}% \isamarkuptrue% -\isanewline +\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ rev\ ys\ {\isacharequal}\ rev\ ys\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}% +\end{isabelle} +Again, we need to abandon this proof attempt and prove another simple lemma +first. In the future the step of abandoning an incomplete proof before +embarking on the proof of a lemma usually remains implicit.% +\end{isamarkuptxt}% +\isamarkuptrue% \isamarkupfalse% % \isamarkupsubsubsection{Second Lemma% @@ -173,10 +284,21 @@ \isamarkuptrue% \isacommand{lemma}\ app{\isacharunderscore}Nil{\isadigit{2}}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +It works, yielding the desired message \isa{No\ subgoals{\isacharbang}}: +\begin{isabelle}% +xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs\isanewline +No\ subgoals{\isacharbang}% +\end{isabelle} +We still need to confirm that the proof is now finished:% +\end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% +\isacommand{done}\isamarkupfalse% % \begin{isamarkuptext}% \noindent @@ -196,8 +318,27 @@ \isamarkuptrue% \isacommand{lemma}\ rev{\isacharunderscore}app\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}rev\ ys{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isachardoublequote}\isanewline \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +we find that this time \isa{auto} solves the base case, but the +induction step merely simplifies to +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }rev\ {\isacharparenleft}list\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ rev\ ys\ {\isacharat}\ rev\ list\ {\isasymLongrightarrow}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isacharparenleft}rev\ ys\ {\isacharat}\ rev\ list{\isacharparenright}\ {\isacharat}\ a\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ rev\ ys\ {\isacharat}\ rev\ list\ {\isacharat}\ a\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}% +\end{isabelle} +Now we need to remember that \isa{{\isacharat}} associates to the right, and that +\isa{{\isacharhash}} and \isa{{\isacharat}} have the same priority (namely the \isa{{\isadigit{6}}{\isadigit{5}}} +in their \isacommand{infixr} annotation). Thus the conclusion really is +\begin{isabelle} +~~~~~(rev~ys~@~rev~list)~@~(a~\#~[])~=~rev~ys~@~(rev~list~@~(a~\#~[])) +\end{isabelle} +and the missing lemma is associativity of \isa{{\isacharat}}.% +\end{isamarkuptxt}% \isamarkuptrue% \isamarkupfalse% % @@ -212,9 +353,11 @@ \isamarkuptrue% \isacommand{lemma}\ app{\isacharunderscore}assoc\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharat}\ zs\ {\isacharequal}\ xs\ {\isacharat}\ {\isacharparenleft}ys\ {\isacharat}\ zs{\isacharparenright}{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{done}\isamarkupfalse% % \begin{isamarkuptext}% \noindent @@ -223,9 +366,11 @@ \isamarkuptrue% \isacommand{lemma}\ rev{\isacharunderscore}app\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}rev\ ys{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{done}\isamarkupfalse% % \begin{isamarkuptext}% \noindent @@ -234,9 +379,11 @@ \isamarkuptrue% \isacommand{theorem}\ rev{\isacharunderscore}rev\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline \isamarkupfalse% +\isacommand{done}\isamarkupfalse% % \begin{isamarkuptext}% \noindent diff -r 0e7b145c3a89 -r 3f2a9f400168 doc-src/TutorialI/Trie/document/Trie.tex --- a/doc-src/TutorialI/Trie/document/Trie.tex Wed May 25 09:03:53 2005 +0200 +++ b/doc-src/TutorialI/Trie/document/Trie.tex Wed May 25 09:04:24 2005 +0200 @@ -63,8 +63,9 @@ \isamarkuptrue% \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}lookup\ {\isacharparenleft}Trie\ None\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ as\ {\isacharequal}\ None{\isachardoublequote}\isanewline \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ as{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{done}\isamarkupfalse% % \begin{isamarkuptext}% Things begin to get interesting with the definition of an update function @@ -109,11 +110,36 @@ \isamarkuptrue% \isacommand{theorem}\ {\isachardoublequote}{\isasymforall}t\ v\ bs{\isachardot}\ lookup\ {\isacharparenleft}update\ t\ as\ v{\isacharparenright}\ bs\ {\isacharequal}\isanewline \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}if\ as{\isacharequal}bs\ then\ Some\ v\ else\ lookup\ t\ bs{\isacharparenright}{\isachardoublequote}\isamarkupfalse% -\isamarkuptrue% -\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +Our plan is to induct on \isa{as}; hence the remaining variables are +quantified. From the definitions it is clear that induction on either +\isa{as} or \isa{bs} is required. The choice of \isa{as} is +guided by the intuition that simplification of \isa{lookup} might be easier +if \isa{update} has already been simplified, which can only happen if +\isa{as} is instantiated. +The start of the proof is conventional:% +\end{isamarkuptxt}% \isamarkuptrue% +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ as{\isacharcomma}\ auto{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\noindent +Unfortunately, this time we are left with three intimidating looking subgoals: +\begin{isabelle} +~1.~\dots~{\isasymLongrightarrow}~lookup~\dots~bs~=~lookup~t~bs\isanewline +~2.~\dots~{\isasymLongrightarrow}~lookup~\dots~bs~=~lookup~t~bs\isanewline +~3.~\dots~{\isasymLongrightarrow}~lookup~\dots~bs~=~lookup~t~bs +\end{isabelle} +Clearly, if we want to make headway we have to instantiate \isa{bs} as +well now. It turns out that instead of induction, case distinction +suffices:% +\end{isamarkuptxt}% +\isamarkuptrue% +\isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac{\isacharbrackleft}{\isacharbang}{\isacharbrackright}\ bs{\isacharcomma}\ auto{\isacharparenright}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{done}\isamarkupfalse% % \begin{isamarkuptext}% \noindent @@ -158,28 +184,16 @@ \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% -\isanewline -\isanewline -\isanewline -\isanewline \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% -\isanewline -\isamarkupfalse% -\isamarkupfalse% \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% -\isanewline -\isanewline -\isanewline -\isamarkupfalse% -\isamarkupfalse% \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% @@ -188,14 +202,16 @@ \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% -\isanewline \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% -\isanewline +\isamarkupfalse% +\isamarkupfalse% +\isamarkupfalse% +\isamarkupfalse% \isamarkupfalse% \isamarkupfalse% \end{isabellebody}%