# HG changeset patch # User paulson # Date 1107363985 -3600 # Node ID 7c638a46dcbbcd7d99ee1ade7cf9d88a54baa846 # Parent 55497029b25517964bd1e7a1b10c7cd2f4cd1b33 tidying of some subst/simplesubst proofs diff -r 55497029b255 -r 7c638a46dcbb doc-src/TutorialI/CTL/document/CTL.tex --- a/doc-src/TutorialI/CTL/document/CTL.tex Wed Feb 02 18:06:00 2005 +0100 +++ b/doc-src/TutorialI/CTL/document/CTL.tex Wed Feb 02 18:06:25 2005 +0100 @@ -67,11 +67,9 @@ \isamarkuptrue% \isacommand{lemma}\ mono{\isacharunderscore}af{\isacharcolon}\ {\isachardoublequote}mono{\isacharparenleft}af\ A{\isacharparenright}{\isachardoublequote}\isanewline \isamarkupfalse% -\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ mono{\isacharunderscore}def\ af{\isacharunderscore}def{\isacharparenright}\isanewline +\isamarkupfalse% \isamarkupfalse% -\isacommand{apply}\ blast\isanewline \isamarkupfalse% -\isacommand{done}\isamarkupfalse% \isamarkupfalse% \isamarkupfalse% \isamarkupfalse% @@ -100,42 +98,13 @@ \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% -% -\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% -\isacommand{apply}{\isacharparenleft}rule\ lfp{\isacharunderscore}lowerbound{\isacharparenright}\isanewline +\isamarkupfalse% \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% \isamarkupfalse% -\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline \isamarkupfalse% -\isacommand{done}\isamarkupfalse% % \begin{isamarkuptext}% The opposite inclusion is proved by contradiction: if some state @@ -153,13 +122,10 @@ \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% -\isacommand{done}\isamarkupfalse% +\isamarkupfalse% % \begin{isamarkuptext}% \noindent @@ -193,100 +159,26 @@ \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% -% -\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% \isamarkuptrue% -\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}% +\isamarkupfalse% \isamarkuptrue% -\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}% +\isamarkupfalse% \isamarkuptrue% -\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}% +\isamarkupfalse% +\isamarkupfalse% +\isamarkuptrue% +\isamarkupfalse% \isamarkuptrue% -\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline +\isamarkupfalse% \isamarkupfalse% -\isacommand{apply}{\isacharparenleft}rule\ someI{\isadigit{2}}{\isacharunderscore}ex{\isacharparenright}\isanewline -\ \isamarkupfalse% -\isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline +\isamarkupfalse% \isamarkupfalse% -\isacommand{apply}{\isacharparenleft}rule\ someI{\isadigit{2}}{\isacharunderscore}ex{\isacharparenright}\isanewline -\ \isamarkupfalse% -\isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline +\isamarkupfalse% \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. @@ -323,40 +215,15 @@ \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% -% -\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% \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% +\isamarkupfalse% \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% -\isacommand{done}\isamarkupfalse% +\isamarkupfalse% % \begin{isamarkuptext}% If you find these proofs too complicated, we recommend that you read @@ -370,11 +237,9 @@ \isamarkuptrue% \isacommand{theorem}\ {\isachardoublequote}mc\ f\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ f{\isacharbraceright}{\isachardoublequote}\isanewline \isamarkupfalse% -\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ f{\isacharparenright}\isanewline +\isamarkupfalse% \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 diff -r 55497029b255 -r 7c638a46dcbb doc-src/TutorialI/CTL/document/CTLind.tex --- a/doc-src/TutorialI/CTL/document/CTLind.tex Wed Feb 02 18:06:00 2005 +0100 +++ b/doc-src/TutorialI/CTL/document/CTLind.tex Wed Feb 02 18:06:25 2005 +0100 @@ -50,17 +50,12 @@ \ \ {\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% -\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% \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 @@ -81,84 +76,22 @@ \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% -\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% +\isamarkupfalse% +\isamarkupfalse% +\isamarkuptrue% +\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}% +\isamarkupfalse% \isamarkuptrue% -\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% \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 @@ -178,7 +111,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 \isanewline \isamarkupfalse% \isamarkupfalse% diff -r 55497029b255 -r 7c638a46dcbb doc-src/TutorialI/CTL/document/PDL.tex --- a/doc-src/TutorialI/CTL/document/PDL.tex Wed Feb 02 18:06:00 2005 +0100 +++ b/doc-src/TutorialI/CTL/document/PDL.tex Wed Feb 02 18:06:25 2005 +0100 @@ -87,11 +87,9 @@ \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% -\isacommand{apply}{\isacharparenleft}rule\ monoI{\isacharparenright}\isanewline +\isamarkupfalse% \isamarkupfalse% -\isacommand{apply}\ blast\isanewline \isamarkupfalse% -\isacommand{done}\isamarkupfalse% % \begin{isamarkuptext}% \noindent @@ -101,112 +99,30 @@ \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% -% -\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% -\isacommand{apply}{\isacharparenleft}rule\ equalityI{\isacharparenright}\isanewline -\ \isamarkupfalse% -\isacommand{apply}{\isacharparenleft}rule\ subsetI{\isacharparenright}\isanewline -\ \isamarkupfalse% -\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isamarkupfalse% +\isamarkupfalse% +\isamarkupfalse% +\isamarkupfalse% \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% -\isacommand{apply}{\isacharparenleft}rule\ subsetI{\isacharparenright}\isanewline +\isamarkupfalse% +\isamarkupfalse% +\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% +\isamarkupfalse% +\isamarkuptrue% +\isamarkupfalse% \isamarkuptrue% -\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}% +\isamarkupfalse% +\isamarkuptrue% +\isamarkupfalse% \isamarkuptrue% -\isacommand{apply}{\isacharparenleft}subst\ lfp{\isacharunderscore}unfold{\isacharbrackleft}OF\ mono{\isacharunderscore}ef{\isacharbrackright}{\isacharparenright}\isanewline +\isamarkupfalse% \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 @@ -215,11 +131,9 @@ \isamarkuptrue% \isacommand{theorem}\ {\isachardoublequote}mc\ f\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ f{\isacharbraceright}{\isachardoublequote}\isanewline \isamarkupfalse% -\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ f{\isacharparenright}\isanewline +\isamarkupfalse% \isamarkupfalse% -\isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ EF{\isacharunderscore}lemma{\isacharparenright}\isanewline \isamarkupfalse% -\isacommand{done}\isamarkupfalse% % \begin{isamarkuptext}% \begin{exercise} diff -r 55497029b255 -r 7c638a46dcbb src/HOL/Library/Word.thy --- a/src/HOL/Library/Word.thy Wed Feb 02 18:06:00 2005 +0100 +++ b/src/HOL/Library/Word.thy Wed Feb 02 18:06:25 2005 +0100 @@ -2425,7 +2425,7 @@ from ki ij jl lw show ?thesis - apply (simplesubst bv_sliceI [where ?j = i and ?i = j and ?w = w and ?w1.0 = "w1 @ w2" and ?w2.0 = w3 and ?w3.0 = "w4 @ w5"]) + apply (subst bv_sliceI [where ?j = i and ?i = j and ?w = w and ?w1.0 = "w1 @ w2" and ?w2.0 = w3 and ?w3.0 = "w4 @ w5"]) apply simp_all apply (rule w_def) apply (simp add: w_defs min_def) diff -r 55497029b255 -r 7c638a46dcbb src/HOL/Matrix/MatrixGeneral.thy --- a/src/HOL/Matrix/MatrixGeneral.thy Wed Feb 02 18:06:00 2005 +0100 +++ b/src/HOL/Matrix/MatrixGeneral.thy Wed Feb 02 18:06:25 2005 +0100 @@ -698,11 +698,11 @@ let ?mx = "max (ncols a) (max (nrows u) (nrows v))" from prems show "mult_matrix_n (max (ncols a) (nrows (combine_matrix fadd u v))) fmul fadd a (combine_matrix fadd u v) = combine_matrix fadd (mult_matrix_n (max (ncols a) (nrows u)) fmul fadd a u) (mult_matrix_n (max (ncols a) (nrows v)) fmul fadd a v)" - apply (simplesubst mult_matrix_nm[of _ _ _ ?mx fadd fmul]) + apply (subst mult_matrix_nm[of _ _ _ ?mx fadd fmul]) apply (simp add: max1 max2 combine_nrows combine_ncols)+ - apply (simplesubst mult_matrix_nm[of _ _ _ ?mx fadd fmul]) + apply (subst mult_matrix_nm[of _ _ v ?mx fadd fmul]) apply (simp add: max1 max2 combine_nrows combine_ncols)+ - apply (simplesubst mult_matrix_nm[of _ _ _ ?mx fadd fmul]) + apply (subst mult_matrix_nm[of _ _ u ?mx fadd fmul]) apply (simp add: max1 max2 combine_nrows combine_ncols)+ apply (simp add: mult_matrix_n_def r_distributive_def foldseq_distr[of fadd]) apply (simp add: combine_matrix_def combine_infmatrix_def) @@ -738,9 +738,9 @@ let ?mx = "max (nrows a) (max (ncols u) (ncols v))" from prems show "mult_matrix_n (max (ncols (combine_matrix fadd u v)) (nrows a)) fmul fadd (combine_matrix fadd u v) a = combine_matrix fadd (mult_matrix_n (max (ncols u) (nrows a)) fmul fadd u a) (mult_matrix_n (max (ncols v) (nrows a)) fmul fadd v a)" - apply (simplesubst mult_matrix_nm[of _ _ _ ?mx fadd fmul]) + apply (subst mult_matrix_nm[of v _ _ ?mx fadd fmul]) apply (simp add: max1 max2 combine_nrows combine_ncols)+ - apply (simplesubst mult_matrix_nm[of _ _ _ ?mx fadd fmul]) + apply (subst mult_matrix_nm[of u _ _ ?mx fadd fmul]) apply (simp add: max1 max2 combine_nrows combine_ncols)+ apply (subst mult_matrix_nm[of _ _ _ ?mx fadd fmul]) apply (simp add: max1 max2 combine_nrows combine_ncols)+ @@ -1227,7 +1227,7 @@ have "!! a b c d. fadd (fadd a b) (fadd c d) = fadd (fadd a c) (fadd b d)" by (simp! add: associative_def commutative_def) then show ?concl - apply (simplesubst mult_matrix_assoc) + apply (subst mult_matrix_assoc) apply (simp_all!) by (simp add: associative_def distributive_def l_distributive_def r_distributive_def)+ qed diff -r 55497029b255 -r 7c638a46dcbb src/HOL/ex/set.thy --- a/src/HOL/ex/set.thy Wed Feb 02 18:06:00 2005 +0100 +++ b/src/HOL/ex/set.thy Wed Feb 02 18:06:25 2005 +0100 @@ -103,21 +103,18 @@ theorem Schroeder_Bernstein: "inj (f :: 'a \ 'b) \ inj (g :: 'b \ 'a) \ \h:: 'a \ 'b. inj h \ surj h" - apply (rule decomposition [THEN exE]) - apply (rule exI) + apply (rule decomposition [where f=f and g=g, THEN exE]) + apply (rule_tac x = "(\z. if z \ x then f z else inv g z)" in exI) + --{*The term above can be synthesized by a sufficiently detailed proof.*} apply (rule bij_if_then_else) apply (rule_tac [4] refl) apply (rule_tac [2] inj_on_inv) apply (erule subset_inj_on [OF _ subset_UNIV]) - txt {* Tricky variable instantiations! *} - apply (erule ssubst, simplesubst double_complement) - apply (rule subsetI, erule imageE, erule ssubst, rule rangeI) - apply (erule ssubst, simplesubst double_complement, erule inv_image_comp [symmetric]) + apply blast + apply (erule ssubst, subst double_complement, erule inv_image_comp [symmetric]) done -subsection {* Set variable instantiation examples *} - text {* From W. W. Bledsoe and Guohui Feng, SET-VAR. JAR 11 (3), 1993, pages 293-314.