tidying of some subst/simplesubst proofs
authorpaulson
Wed Feb 02 18:06:25 2005 +0100 (2005-02-02)
changeset 154887c638a46dcbb
parent 15487 55497029b255
child 15489 d136af442665
tidying of some subst/simplesubst proofs
doc-src/TutorialI/CTL/document/CTL.tex
doc-src/TutorialI/CTL/document/CTLind.tex
doc-src/TutorialI/CTL/document/PDL.tex
src/HOL/Library/Word.thy
src/HOL/Matrix/MatrixGeneral.thy
src/HOL/ex/set.thy
     1.1 --- a/doc-src/TutorialI/CTL/document/CTL.tex	Wed Feb 02 18:06:00 2005 +0100
     1.2 +++ b/doc-src/TutorialI/CTL/document/CTL.tex	Wed Feb 02 18:06:25 2005 +0100
     1.3 @@ -67,11 +67,9 @@
     1.4  \isamarkuptrue%
     1.5  \isacommand{lemma}\ mono{\isacharunderscore}af{\isacharcolon}\ {\isachardoublequote}mono{\isacharparenleft}af\ A{\isacharparenright}{\isachardoublequote}\isanewline
     1.6  \isamarkupfalse%
     1.7 -\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ mono{\isacharunderscore}def\ af{\isacharunderscore}def{\isacharparenright}\isanewline
     1.8 +\isamarkupfalse%
     1.9  \isamarkupfalse%
    1.10 -\isacommand{apply}\ blast\isanewline
    1.11  \isamarkupfalse%
    1.12 -\isacommand{done}\isamarkupfalse%
    1.13  \isamarkupfalse%
    1.14  \isamarkupfalse%
    1.15  \isamarkupfalse%
    1.16 @@ -100,42 +98,13 @@
    1.17  \isamarkuptrue%
    1.18  \isacommand{theorem}\ AF{\isacharunderscore}lemma{\isadigit{1}}{\isacharcolon}\isanewline
    1.19  \ \ {\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%
    1.20 -%
    1.21 -\begin{isamarkuptxt}%
    1.22 -\noindent
    1.23 -In contrast to the analogous proof for \isa{EF}, and just
    1.24 -for a change, we do not use fixed point induction.  Park-induction,
    1.25 -named after David Park, is weaker but sufficient for this proof:
    1.26 -\begin{center}
    1.27 -\isa{f\ S\ {\isasymsubseteq}\ S\ {\isasymLongrightarrow}\ lfp\ f\ {\isasymsubseteq}\ S} \hfill (\isa{lfp{\isacharunderscore}lowerbound})
    1.28 -\end{center}
    1.29 -The instance of the premise \isa{f\ S\ {\isasymsubseteq}\ S} is proved pointwise,
    1.30 -a decision that \isa{auto} takes for us:%
    1.31 -\end{isamarkuptxt}%
    1.32  \isamarkuptrue%
    1.33 -\isacommand{apply}{\isacharparenleft}rule\ lfp{\isacharunderscore}lowerbound{\isacharparenright}\isanewline
    1.34 +\isamarkupfalse%
    1.35  \isamarkupfalse%
    1.36 -\isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ af{\isacharunderscore}def\ Paths{\isacharunderscore}def{\isacharparenright}\isamarkupfalse%
    1.37 -%
    1.38 -\begin{isamarkuptxt}%
    1.39 -\begin{isabelle}%
    1.40 -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}{\isasymforall}t{\isachardot}\ {\isacharparenleft}p\ {\isadigit{0}}{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymlongrightarrow}\isanewline
    1.41 -\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
    1.42 -\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
    1.43 -\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ \ }{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isasymrbrakk}\isanewline
    1.44 -\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ }{\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A%
    1.45 -\end{isabelle}
    1.46 -In this remaining case, we set \isa{t} to \isa{p\ {\isadigit{1}}}.
    1.47 -The rest is automatic, which is surprising because it involves
    1.48 -finding the instantiation \isa{{\isasymlambda}i{\isachardot}\ p\ {\isacharparenleft}i\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}}
    1.49 -for \isa{{\isasymforall}p}.%
    1.50 -\end{isamarkuptxt}%
    1.51  \isamarkuptrue%
    1.52 -\isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}p\ {\isadigit{1}}{\isachardoublequote}\ \isakeyword{in}\ allE{\isacharparenright}\isanewline
    1.53 +\isamarkupfalse%
    1.54  \isamarkupfalse%
    1.55 -\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline
    1.56  \isamarkupfalse%
    1.57 -\isacommand{done}\isamarkupfalse%
    1.58  %
    1.59  \begin{isamarkuptext}%
    1.60  The opposite inclusion is proved by contradiction: if some state
    1.61 @@ -153,13 +122,10 @@
    1.62  \isacommand{lemma}\ not{\isacharunderscore}in{\isacharunderscore}lfp{\isacharunderscore}afD{\isacharcolon}\isanewline
    1.63  \ {\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
    1.64  \isamarkupfalse%
    1.65 -\isacommand{apply}{\isacharparenleft}erule\ contrapos{\isacharunderscore}np{\isacharparenright}\isanewline
    1.66  \isamarkupfalse%
    1.67 -\isacommand{apply}{\isacharparenleft}subst\ lfp{\isacharunderscore}unfold{\isacharbrackleft}OF\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharparenright}\isanewline
    1.68  \isamarkupfalse%
    1.69 -\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ af{\isacharunderscore}def{\isacharparenright}\isanewline
    1.70  \isamarkupfalse%
    1.71 -\isacommand{done}\isamarkupfalse%
    1.72 +\isamarkupfalse%
    1.73  %
    1.74  \begin{isamarkuptext}%
    1.75  \noindent
    1.76 @@ -193,100 +159,26 @@
    1.77  \isacommand{lemma}\ infinity{\isacharunderscore}lemma{\isacharcolon}\isanewline
    1.78  \ \ {\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
    1.79  \ \ \ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ Q{\isacharparenleft}p\ i{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
    1.80 -%
    1.81 -\begin{isamarkuptxt}%
    1.82 -\noindent
    1.83 -First we rephrase the conclusion slightly because we need to prove simultaneously
    1.84 -both the path property and the fact that \isa{Q} holds:%
    1.85 -\end{isamarkuptxt}%
    1.86 +\isamarkuptrue%
    1.87 +\isamarkupfalse%
    1.88  \isamarkuptrue%
    1.89 -\isacommand{apply}{\isacharparenleft}subgoal{\isacharunderscore}tac\isanewline
    1.90 -\ \ {\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%
    1.91 -%
    1.92 -\begin{isamarkuptxt}%
    1.93 -\noindent
    1.94 -From this proposition the original goal follows easily:%
    1.95 -\end{isamarkuptxt}%
    1.96 -\ \isamarkuptrue%
    1.97 -\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ Paths{\isacharunderscore}def{\isacharcomma}\ blast{\isacharparenright}\isamarkupfalse%
    1.98 -%
    1.99 -\begin{isamarkuptxt}%
   1.100 -\noindent
   1.101 -The new subgoal is proved by providing the witness \isa{path\ s\ Q} for \isa{p}:%
   1.102 -\end{isamarkuptxt}%
   1.103 +\isamarkupfalse%
   1.104  \isamarkuptrue%
   1.105 -\isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}path\ s\ Q{\isachardoublequote}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline
   1.106  \isamarkupfalse%
   1.107 -\isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}\isamarkupfalse%
   1.108 -%
   1.109 -\begin{isamarkuptxt}%
   1.110 -\noindent
   1.111 -After simplification and clarification, the subgoal has the following form:
   1.112 -\begin{isabelle}%
   1.113 -\ {\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
   1.114 -\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
   1.115 -\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}i{\isachardot}\ {\isasymLongrightarrow}\ }Q\ {\isacharparenleft}path\ s\ Q\ i{\isacharparenright}%
   1.116 -\end{isabelle}
   1.117 -It invites a proof by induction on \isa{i}:%
   1.118 -\end{isamarkuptxt}%
   1.119 +\isamarkupfalse%
   1.120  \isamarkuptrue%
   1.121 -\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ i{\isacharparenright}\isanewline
   1.122 -\ \isamarkupfalse%
   1.123 -\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isamarkupfalse%
   1.124 -%
   1.125 -\begin{isamarkuptxt}%
   1.126 -\noindent
   1.127 -After simplification, the base case boils down to
   1.128 -\begin{isabelle}%
   1.129 -\ {\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
   1.130 -\isaindent{\ {\isadigit{1}}{\isachardot}\ }{\isasymLongrightarrow}\ {\isacharparenleft}s{\isacharcomma}\ SOME\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q\ t{\isacharparenright}\ {\isasymin}\ M%
   1.131 -\end{isabelle}
   1.132 -The conclusion looks exceedingly trivial: after all, \isa{t} is chosen such that \isa{{\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M}
   1.133 -holds. However, we first have to show that such a \isa{t} actually exists! This reasoning
   1.134 -is embodied in the theorem \isa{someI{\isadigit{2}}{\isacharunderscore}ex}:
   1.135 -\begin{isabelle}%
   1.136 -\ \ \ \ \ {\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}%
   1.137 -\end{isabelle}
   1.138 -When we apply this theorem as an introduction rule, \isa{{\isacharquery}P\ x} becomes
   1.139 -\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
   1.140 -two subgoals: \isa{{\isasymexists}a{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ a{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q\ a}, which follows from the assumptions, and
   1.141 -\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
   1.142 -\isa{fast} can prove the base case quickly:%
   1.143 -\end{isamarkuptxt}%
   1.144 -\ \isamarkuptrue%
   1.145 -\isacommand{apply}{\isacharparenleft}fast\ intro{\isacharcolon}\ someI{\isadigit{2}}{\isacharunderscore}ex{\isacharparenright}\isamarkupfalse%
   1.146 -%
   1.147 -\begin{isamarkuptxt}%
   1.148 -\noindent
   1.149 -What is worth noting here is that we have used \methdx{fast} rather than
   1.150 -\isa{blast}.  The reason is that \isa{blast} would fail because it cannot
   1.151 -cope with \isa{someI{\isadigit{2}}{\isacharunderscore}ex}: unifying its conclusion with the current
   1.152 -subgoal is non-trivial because of the nested schematic variables. For
   1.153 -efficiency reasons \isa{blast} does not even attempt such unifications.
   1.154 -Although \isa{fast} can in principle cope with complicated unification
   1.155 -problems, in practice the number of unifiers arising is often prohibitive and
   1.156 -the offending rule may need to be applied explicitly rather than
   1.157 -automatically. This is what happens in the step case.
   1.158 -
   1.159 -The induction step is similar, but more involved, because now we face nested
   1.160 -occurrences of \isa{SOME}. As a result, \isa{fast} is no longer able to
   1.161 -solve the subgoal and we apply \isa{someI{\isadigit{2}}{\isacharunderscore}ex} by hand.  We merely
   1.162 -show the proof commands but do not describe the details:%
   1.163 -\end{isamarkuptxt}%
   1.164 +\isamarkupfalse%
   1.165 +\isamarkupfalse%
   1.166 +\isamarkuptrue%
   1.167 +\isamarkupfalse%
   1.168  \isamarkuptrue%
   1.169 -\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
   1.170 +\isamarkupfalse%
   1.171  \isamarkupfalse%
   1.172 -\isacommand{apply}{\isacharparenleft}rule\ someI{\isadigit{2}}{\isacharunderscore}ex{\isacharparenright}\isanewline
   1.173 -\ \isamarkupfalse%
   1.174 -\isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
   1.175 +\isamarkupfalse%
   1.176  \isamarkupfalse%
   1.177 -\isacommand{apply}{\isacharparenleft}rule\ someI{\isadigit{2}}{\isacharunderscore}ex{\isacharparenright}\isanewline
   1.178 -\ \isamarkupfalse%
   1.179 -\isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
   1.180 +\isamarkupfalse%
   1.181  \isamarkupfalse%
   1.182 -\isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
   1.183  \isamarkupfalse%
   1.184 -\isacommand{done}\isamarkupfalse%
   1.185  %
   1.186  \begin{isamarkuptext}%
   1.187  Function \isa{path} has fulfilled its purpose now and can be forgotten.
   1.188 @@ -323,40 +215,15 @@
   1.189  \end{isamarkuptext}%
   1.190  \isamarkuptrue%
   1.191  \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%
   1.192 -%
   1.193 -\begin{isamarkuptxt}%
   1.194 -\noindent
   1.195 -The proof is again pointwise and then by contraposition:%
   1.196 -\end{isamarkuptxt}%
   1.197  \isamarkuptrue%
   1.198 -\isacommand{apply}{\isacharparenleft}rule\ subsetI{\isacharparenright}\isanewline
   1.199  \isamarkupfalse%
   1.200 -\isacommand{apply}{\isacharparenleft}erule\ contrapos{\isacharunderscore}pp{\isacharparenright}\isanewline
   1.201 +\isamarkupfalse%
   1.202  \isamarkupfalse%
   1.203 -\isacommand{apply}\ simp\isamarkupfalse%
   1.204 -%
   1.205 -\begin{isamarkuptxt}%
   1.206 -\begin{isabelle}%
   1.207 -\ {\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%
   1.208 -\end{isabelle}
   1.209 -Applying the \isa{infinity{\isacharunderscore}lemma} as a destruction rule leaves two subgoals, the second
   1.210 -premise of \isa{infinity{\isacharunderscore}lemma} and the original subgoal:%
   1.211 -\end{isamarkuptxt}%
   1.212 +\isamarkuptrue%
   1.213 +\isamarkupfalse%
   1.214  \isamarkuptrue%
   1.215 -\isacommand{apply}{\isacharparenleft}drule\ infinity{\isacharunderscore}lemma{\isacharparenright}\isamarkupfalse%
   1.216 -%
   1.217 -\begin{isamarkuptxt}%
   1.218 -\begin{isabelle}%
   1.219 -\ {\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
   1.220 -\ {\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
   1.221 -\isaindent{\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ }{\isasymexists}p{\isasymin}Paths\ x{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ A%
   1.222 -\end{isabelle}
   1.223 -Both are solved automatically:%
   1.224 -\end{isamarkuptxt}%
   1.225 -\ \isamarkuptrue%
   1.226 -\isacommand{apply}{\isacharparenleft}auto\ dest{\isacharcolon}\ not{\isacharunderscore}in{\isacharunderscore}lfp{\isacharunderscore}afD{\isacharparenright}\isanewline
   1.227  \isamarkupfalse%
   1.228 -\isacommand{done}\isamarkupfalse%
   1.229 +\isamarkupfalse%
   1.230  %
   1.231  \begin{isamarkuptext}%
   1.232  If you find these proofs too complicated, we recommend that you read
   1.233 @@ -370,11 +237,9 @@
   1.234  \isamarkuptrue%
   1.235  \isacommand{theorem}\ {\isachardoublequote}mc\ f\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ f{\isacharbraceright}{\isachardoublequote}\isanewline
   1.236  \isamarkupfalse%
   1.237 -\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ f{\isacharparenright}\isanewline
   1.238 +\isamarkupfalse%
   1.239  \isamarkupfalse%
   1.240 -\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
   1.241  \isamarkupfalse%
   1.242 -\isacommand{done}\isamarkupfalse%
   1.243  %
   1.244  \begin{isamarkuptext}%
   1.245  The language defined above is not quite CTL\@. The latter also includes an
     2.1 --- a/doc-src/TutorialI/CTL/document/CTLind.tex	Wed Feb 02 18:06:00 2005 +0100
     2.2 +++ b/doc-src/TutorialI/CTL/document/CTLind.tex	Wed Feb 02 18:06:25 2005 +0100
     2.3 @@ -50,17 +50,12 @@
     2.4  \ \ {\isachardoublequote}t\ {\isasymin}\ Avoid\ s\ A\ \ {\isasymLongrightarrow}\isanewline
     2.5  \ \ \ {\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
     2.6  \isamarkupfalse%
     2.7 -\isacommand{apply}{\isacharparenleft}erule\ Avoid{\isachardot}induct{\isacharparenright}\isanewline
     2.8 -\ \isamarkupfalse%
     2.9 -\isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
    2.10  \isamarkupfalse%
    2.11 -\isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline
    2.12 +\isamarkupfalse%
    2.13  \isamarkupfalse%
    2.14 -\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
    2.15 +\isamarkupfalse%
    2.16  \isamarkupfalse%
    2.17 -\isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ Paths{\isacharunderscore}def\ split{\isacharcolon}\ nat{\isachardot}split{\isacharparenright}\isanewline
    2.18  \isamarkupfalse%
    2.19 -\isacommand{done}\isamarkupfalse%
    2.20  %
    2.21  \begin{isamarkuptext}%
    2.22  \noindent
    2.23 @@ -81,84 +76,22 @@
    2.24  \isamarkuptrue%
    2.25  \isacommand{lemma}\ Avoid{\isacharunderscore}in{\isacharunderscore}lfp{\isacharbrackleft}rule{\isacharunderscore}format{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isacharbrackright}{\isacharcolon}\isanewline
    2.26  \ \ {\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%
    2.27 -%
    2.28 -\begin{isamarkuptxt}%
    2.29 -\noindent
    2.30 -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}}.
    2.31 -If \isa{t} is already in \isa{A}, then \isa{t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}} is
    2.32 -trivial. If \isa{t} is not in \isa{A} but all successors are in
    2.33 -\isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}} (induction hypothesis), then \isa{t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}} is
    2.34 -again trivial.
    2.35 -
    2.36 -The formal counterpart of this proof sketch is a well-founded induction
    2.37 -on~\isa{M} restricted to \isa{Avoid\ s\ A\ {\isacharminus}\ A}, roughly speaking:
    2.38 -\begin{isabelle}%
    2.39 -\ \ \ \ \ {\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}%
    2.40 -\end{isabelle}
    2.41 -As we shall see presently, the absence of infinite \isa{A}-avoiding paths
    2.42 -starting from \isa{s} implies well-foundedness of this relation. For the
    2.43 -moment we assume this and proceed with the induction:%
    2.44 -\end{isamarkuptxt}%
    2.45  \isamarkuptrue%
    2.46 -\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
    2.47 -\ \isamarkupfalse%
    2.48 -\isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ a\ {\isacharequal}\ t\ \isakeyword{in}\ wf{\isacharunderscore}induct{\isacharparenright}\isanewline
    2.49 -\ \isamarkupfalse%
    2.50 -\isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}\isamarkupfalse%
    2.51 +\isamarkupfalse%
    2.52 +\isamarkupfalse%
    2.53 +\isamarkupfalse%
    2.54 +\isamarkupfalse%
    2.55 +\isamarkuptrue%
    2.56 +\isamarkupfalse%
    2.57  \isamarkupfalse%
    2.58 -%
    2.59 -\begin{isamarkuptxt}%
    2.60 -\noindent
    2.61 -\begin{isabelle}%
    2.62 -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ {\isasymlbrakk}{\isasymforall}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharsemicolon}\isanewline
    2.63 -\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ \ }{\isasymforall}y{\isachardot}\ {\isacharparenleft}t{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ t\ {\isasymnotin}\ A\ {\isasymlongrightarrow}\isanewline
    2.64 -\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
    2.65 -\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ \ }t\ {\isasymin}\ Avoid\ s\ A{\isasymrbrakk}\isanewline
    2.66 -\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ }{\isasymLongrightarrow}\ t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\isanewline
    2.67 -\ {\isadigit{2}}{\isachardot}\ {\isasymforall}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A\ {\isasymLongrightarrow}\isanewline
    2.68 -\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}%
    2.69 -\end{isabelle}
    2.70 -Now the induction hypothesis states that if \isa{t\ {\isasymnotin}\ A}
    2.71 -then all successors of \isa{t} that are in \isa{Avoid\ s\ A} are in
    2.72 -\isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. Unfolding \isa{lfp} in the conclusion of the first
    2.73 -subgoal once, we have to prove that \isa{t} is in \isa{A} or all successors
    2.74 -of \isa{t} are in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}.  But if \isa{t} is not in \isa{A},
    2.75 -the second 
    2.76 -\isa{Avoid}-rule implies that all successors of \isa{t} are in
    2.77 -\isa{Avoid\ s\ A}, because we also assume \isa{t\ {\isasymin}\ Avoid\ s\ A}.
    2.78 -Hence, by the induction hypothesis, all successors of \isa{t} are indeed in
    2.79 -\isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. Mechanically:%
    2.80 -\end{isamarkuptxt}%
    2.81 -\ \isamarkuptrue%
    2.82 -\isacommand{apply}{\isacharparenleft}subst\ lfp{\isacharunderscore}unfold{\isacharbrackleft}OF\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharparenright}\isanewline
    2.83 -\ \isamarkupfalse%
    2.84 -\isacommand{apply}{\isacharparenleft}simp\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}\ add{\isacharcolon}\ af{\isacharunderscore}def{\isacharparenright}\isanewline
    2.85 -\ \isamarkupfalse%
    2.86 -\isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ Avoid{\isachardot}intros{\isacharparenright}\isamarkupfalse%
    2.87 -%
    2.88 -\begin{isamarkuptxt}%
    2.89 -Having proved the main goal, we return to the proof obligation that the 
    2.90 -relation used above is indeed well-founded. This is proved by contradiction: if
    2.91 -the relation is not well-founded then there exists an infinite \isa{A}-avoiding path all in \isa{Avoid\ s\ A}, by theorem
    2.92 -\isa{wf{\isacharunderscore}iff{\isacharunderscore}no{\isacharunderscore}infinite{\isacharunderscore}down{\isacharunderscore}chain}:
    2.93 -\begin{isabelle}%
    2.94 -\ \ \ \ \ 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}%
    2.95 -\end{isabelle}
    2.96 -From lemma \isa{ex{\isacharunderscore}infinite{\isacharunderscore}path} the existence of an infinite
    2.97 -\isa{A}-avoiding path starting in \isa{s} follows, contradiction.%
    2.98 -\end{isamarkuptxt}%
    2.99 +\isamarkupfalse%
   2.100  \isamarkuptrue%
   2.101 -\isacommand{apply}{\isacharparenleft}erule\ contrapos{\isacharunderscore}pp{\isacharparenright}\isanewline
   2.102  \isamarkupfalse%
   2.103 -\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ wf{\isacharunderscore}iff{\isacharunderscore}no{\isacharunderscore}infinite{\isacharunderscore}down{\isacharunderscore}chain{\isacharparenright}\isanewline
   2.104  \isamarkupfalse%
   2.105 -\isacommand{apply}{\isacharparenleft}erule\ exE{\isacharparenright}\isanewline
   2.106  \isamarkupfalse%
   2.107 -\isacommand{apply}{\isacharparenleft}rule\ ex{\isacharunderscore}infinite{\isacharunderscore}path{\isacharparenright}\isanewline
   2.108 +\isamarkupfalse%
   2.109  \isamarkupfalse%
   2.110 -\isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ Paths{\isacharunderscore}def{\isacharparenright}\isanewline
   2.111  \isamarkupfalse%
   2.112 -\isacommand{done}\isamarkupfalse%
   2.113  %
   2.114  \begin{isamarkuptext}%
   2.115  The \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}} modifier of the \isa{rule{\isacharunderscore}format} directive in the
   2.116 @@ -178,7 +111,7 @@
   2.117  \isamarkuptrue%
   2.118  \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
   2.119  \isamarkupfalse%
   2.120 -\isacommand{by}{\isacharparenleft}auto\ elim{\isacharcolon}\ Avoid{\isacharunderscore}in{\isacharunderscore}lfp\ intro{\isacharcolon}\ Avoid{\isachardot}intros{\isacharparenright}\isanewline
   2.121 +\isanewline
   2.122  \isanewline
   2.123  \isamarkupfalse%
   2.124  \isamarkupfalse%
     3.1 --- a/doc-src/TutorialI/CTL/document/PDL.tex	Wed Feb 02 18:06:00 2005 +0100
     3.2 +++ b/doc-src/TutorialI/CTL/document/PDL.tex	Wed Feb 02 18:06:25 2005 +0100
     3.3 @@ -87,11 +87,9 @@
     3.4  \isamarkuptrue%
     3.5  \isacommand{lemma}\ mono{\isacharunderscore}ef{\isacharcolon}\ {\isachardoublequote}mono{\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ {\isacharparenleft}M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
     3.6  \isamarkupfalse%
     3.7 -\isacommand{apply}{\isacharparenleft}rule\ monoI{\isacharparenright}\isanewline
     3.8 +\isamarkupfalse%
     3.9  \isamarkupfalse%
    3.10 -\isacommand{apply}\ blast\isanewline
    3.11  \isamarkupfalse%
    3.12 -\isacommand{done}\isamarkupfalse%
    3.13  %
    3.14  \begin{isamarkuptext}%
    3.15  \noindent
    3.16 @@ -101,112 +99,30 @@
    3.17  \isamarkuptrue%
    3.18  \isacommand{lemma}\ EF{\isacharunderscore}lemma{\isacharcolon}\isanewline
    3.19  \ \ {\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%
    3.20 -%
    3.21 -\begin{isamarkuptxt}%
    3.22 -\noindent
    3.23 -The equality is proved in the canonical fashion by proving that each set
    3.24 -includes the other; the inclusion is shown pointwise:%
    3.25 -\end{isamarkuptxt}%
    3.26  \isamarkuptrue%
    3.27 -\isacommand{apply}{\isacharparenleft}rule\ equalityI{\isacharparenright}\isanewline
    3.28 -\ \isamarkupfalse%
    3.29 -\isacommand{apply}{\isacharparenleft}rule\ subsetI{\isacharparenright}\isanewline
    3.30 -\ \isamarkupfalse%
    3.31 -\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isamarkupfalse%
    3.32 +\isamarkupfalse%
    3.33 +\isamarkupfalse%
    3.34 +\isamarkupfalse%
    3.35  \isamarkupfalse%
    3.36 -%
    3.37 -\begin{isamarkuptxt}%
    3.38 -\noindent
    3.39 -Simplification leaves us with the following first subgoal
    3.40 -\begin{isabelle}%
    3.41 -\ {\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%
    3.42 -\end{isabelle}
    3.43 -which is proved by \isa{lfp}-induction:%
    3.44 -\end{isamarkuptxt}%
    3.45 -\ \isamarkuptrue%
    3.46 -\isacommand{apply}{\isacharparenleft}erule\ lfp{\isacharunderscore}induct{\isacharparenright}\isanewline
    3.47 -\ \ \isamarkupfalse%
    3.48 -\isacommand{apply}{\isacharparenleft}rule\ mono{\isacharunderscore}ef{\isacharparenright}\isanewline
    3.49 -\ \isamarkupfalse%
    3.50 -\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isamarkupfalse%
    3.51 -%
    3.52 -\begin{isamarkuptxt}%
    3.53 -\noindent
    3.54 -Having disposed of the monotonicity subgoal,
    3.55 -simplification leaves us with the following goal:
    3.56 -\begin{isabelle}
    3.57 -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ A\ {\isasymor}\isanewline
    3.58 -\ \ \ \ \ \ \ \ \ 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
    3.59 -\ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A
    3.60 -\end{isabelle}
    3.61 -It is proved by \isa{blast}, using the transitivity of 
    3.62 -\isa{M\isactrlsup {\isacharasterisk}}.%
    3.63 -\end{isamarkuptxt}%
    3.64 -\ \isamarkuptrue%
    3.65 -\isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtrancl{\isacharunderscore}trans{\isacharparenright}\isamarkupfalse%
    3.66 -%
    3.67 -\begin{isamarkuptxt}%
    3.68 -We now return to the second set inclusion subgoal, which is again proved
    3.69 -pointwise:%
    3.70 -\end{isamarkuptxt}%
    3.71  \isamarkuptrue%
    3.72 -\isacommand{apply}{\isacharparenleft}rule\ subsetI{\isacharparenright}\isanewline
    3.73 +\isamarkupfalse%
    3.74 +\isamarkupfalse%
    3.75 +\isamarkupfalse%
    3.76 +\isamarkuptrue%
    3.77  \isamarkupfalse%
    3.78 -\isacommand{apply}{\isacharparenleft}simp{\isacharcomma}\ clarify{\isacharparenright}\isamarkupfalse%
    3.79 -%
    3.80 -\begin{isamarkuptxt}%
    3.81 -\noindent
    3.82 -After simplification and clarification we are left with
    3.83 -\begin{isabelle}%
    3.84 -\ {\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}%
    3.85 -\end{isabelle}
    3.86 -This goal is proved by induction on \isa{{\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}}. But since the model
    3.87 -checker works backwards (from \isa{t} to \isa{s}), we cannot use the
    3.88 -induction theorem \isa{rtrancl{\isacharunderscore}induct}: it works in the
    3.89 -forward direction. Fortunately the converse induction theorem
    3.90 -\isa{converse{\isacharunderscore}rtrancl{\isacharunderscore}induct} already exists:
    3.91 -\begin{isabelle}%
    3.92 -\ \ \ \ \ {\isasymlbrakk}{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r\isactrlsup {\isacharasterisk}{\isacharsemicolon}\ P\ b{\isacharsemicolon}\isanewline
    3.93 -\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
    3.94 -\isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ P\ a%
    3.95 -\end{isabelle}
    3.96 -It says that if \isa{{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r\isactrlsup {\isacharasterisk}} and we know \isa{P\ b} then we can infer
    3.97 -\isa{P\ a} provided each step backwards from a predecessor \isa{z} of
    3.98 -\isa{b} preserves \isa{P}.%
    3.99 -\end{isamarkuptxt}%
   3.100 +\isamarkuptrue%
   3.101 +\isamarkupfalse%
   3.102 +\isamarkupfalse%
   3.103 +\isamarkuptrue%
   3.104 +\isamarkupfalse%
   3.105  \isamarkuptrue%
   3.106 -\isacommand{apply}{\isacharparenleft}erule\ converse{\isacharunderscore}rtrancl{\isacharunderscore}induct{\isacharparenright}\isamarkupfalse%
   3.107 -%
   3.108 -\begin{isamarkuptxt}%
   3.109 -\noindent
   3.110 -The base case
   3.111 -\begin{isabelle}%
   3.112 -\ {\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}%
   3.113 -\end{isabelle}
   3.114 -is solved by unrolling \isa{lfp} once%
   3.115 -\end{isamarkuptxt}%
   3.116 -\ \isamarkuptrue%
   3.117 -\isacommand{apply}{\isacharparenleft}subst\ lfp{\isacharunderscore}unfold{\isacharbrackleft}OF\ mono{\isacharunderscore}ef{\isacharbrackright}{\isacharparenright}\isamarkupfalse%
   3.118 -%
   3.119 -\begin{isamarkuptxt}%
   3.120 -\begin{isabelle}%
   3.121 -\ {\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}%
   3.122 -\end{isabelle}
   3.123 -and disposing of the resulting trivial subgoal automatically:%
   3.124 -\end{isamarkuptxt}%
   3.125 -\ \isamarkuptrue%
   3.126 -\isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isamarkupfalse%
   3.127 -%
   3.128 -\begin{isamarkuptxt}%
   3.129 -\noindent
   3.130 -The proof of the induction step is identical to the one for the base case:%
   3.131 -\end{isamarkuptxt}%
   3.132 +\isamarkupfalse%
   3.133 +\isamarkuptrue%
   3.134 +\isamarkupfalse%
   3.135  \isamarkuptrue%
   3.136 -\isacommand{apply}{\isacharparenleft}subst\ lfp{\isacharunderscore}unfold{\isacharbrackleft}OF\ mono{\isacharunderscore}ef{\isacharbrackright}{\isacharparenright}\isanewline
   3.137 +\isamarkupfalse%
   3.138  \isamarkupfalse%
   3.139 -\isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
   3.140  \isamarkupfalse%
   3.141 -\isacommand{done}\isamarkupfalse%
   3.142  %
   3.143  \begin{isamarkuptext}%
   3.144  The main theorem is proved in the familiar manner: induction followed by
   3.145 @@ -215,11 +131,9 @@
   3.146  \isamarkuptrue%
   3.147  \isacommand{theorem}\ {\isachardoublequote}mc\ f\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ f{\isacharbraceright}{\isachardoublequote}\isanewline
   3.148  \isamarkupfalse%
   3.149 -\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ f{\isacharparenright}\isanewline
   3.150 +\isamarkupfalse%
   3.151  \isamarkupfalse%
   3.152 -\isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ EF{\isacharunderscore}lemma{\isacharparenright}\isanewline
   3.153  \isamarkupfalse%
   3.154 -\isacommand{done}\isamarkupfalse%
   3.155  %
   3.156  \begin{isamarkuptext}%
   3.157  \begin{exercise}
     4.1 --- a/src/HOL/Library/Word.thy	Wed Feb 02 18:06:00 2005 +0100
     4.2 +++ b/src/HOL/Library/Word.thy	Wed Feb 02 18:06:25 2005 +0100
     4.3 @@ -2425,7 +2425,7 @@
     4.4  
     4.5    from ki ij jl lw
     4.6    show ?thesis
     4.7 -    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"])
     4.8 +    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"])
     4.9      apply simp_all
    4.10      apply (rule w_def)
    4.11      apply (simp add: w_defs min_def)
     5.1 --- a/src/HOL/Matrix/MatrixGeneral.thy	Wed Feb 02 18:06:00 2005 +0100
     5.2 +++ b/src/HOL/Matrix/MatrixGeneral.thy	Wed Feb 02 18:06:25 2005 +0100
     5.3 @@ -698,11 +698,11 @@
     5.4        let ?mx = "max (ncols a) (max (nrows u) (nrows v))"
     5.5        from prems show "mult_matrix_n (max (ncols a) (nrows (combine_matrix fadd u v))) fmul fadd a (combine_matrix fadd u v) =
     5.6          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)"
     5.7 -        apply (simplesubst mult_matrix_nm[of _ _ _ ?mx fadd fmul])
     5.8 +        apply (subst mult_matrix_nm[of _ _ _ ?mx fadd fmul])
     5.9          apply (simp add: max1 max2 combine_nrows combine_ncols)+
    5.10 -        apply (simplesubst mult_matrix_nm[of _ _ _ ?mx fadd fmul])
    5.11 +        apply (subst mult_matrix_nm[of _ _ v ?mx fadd fmul])
    5.12          apply (simp add: max1 max2 combine_nrows combine_ncols)+
    5.13 -        apply (simplesubst mult_matrix_nm[of _ _ _ ?mx fadd fmul])
    5.14 +        apply (subst mult_matrix_nm[of _ _ u ?mx fadd fmul])
    5.15          apply (simp add: max1 max2 combine_nrows combine_ncols)+
    5.16          apply (simp add: mult_matrix_n_def r_distributive_def foldseq_distr[of fadd])
    5.17          apply (simp add: combine_matrix_def combine_infmatrix_def)
    5.18 @@ -738,9 +738,9 @@
    5.19        let ?mx = "max (nrows a) (max (ncols u) (ncols v))"
    5.20        from prems show "mult_matrix_n (max (ncols (combine_matrix fadd u v)) (nrows a)) fmul fadd (combine_matrix fadd u v) a =
    5.21                 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)"
    5.22 -        apply (simplesubst mult_matrix_nm[of _ _ _ ?mx fadd fmul])
    5.23 +        apply (subst mult_matrix_nm[of v _ _ ?mx fadd fmul])
    5.24          apply (simp add: max1 max2 combine_nrows combine_ncols)+
    5.25 -        apply (simplesubst mult_matrix_nm[of _ _ _ ?mx fadd fmul])
    5.26 +        apply (subst mult_matrix_nm[of u _ _ ?mx fadd fmul])
    5.27          apply (simp add: max1 max2 combine_nrows combine_ncols)+
    5.28          apply (subst mult_matrix_nm[of _ _ _ ?mx fadd fmul])
    5.29          apply (simp add: max1 max2 combine_nrows combine_ncols)+
    5.30 @@ -1227,7 +1227,7 @@
    5.31    have "!! a b c d. fadd (fadd a b) (fadd c d) = fadd (fadd a c) (fadd b d)"
    5.32      by (simp! add: associative_def commutative_def)
    5.33    then show ?concl
    5.34 -    apply (simplesubst mult_matrix_assoc)
    5.35 +    apply (subst mult_matrix_assoc)
    5.36      apply (simp_all!)
    5.37      by (simp add: associative_def distributive_def l_distributive_def r_distributive_def)+
    5.38  qed
     6.1 --- a/src/HOL/ex/set.thy	Wed Feb 02 18:06:00 2005 +0100
     6.2 +++ b/src/HOL/ex/set.thy	Wed Feb 02 18:06:25 2005 +0100
     6.3 @@ -103,21 +103,18 @@
     6.4  theorem Schroeder_Bernstein:
     6.5    "inj (f :: 'a \<Rightarrow> 'b) \<Longrightarrow> inj (g :: 'b \<Rightarrow> 'a)
     6.6      \<Longrightarrow> \<exists>h:: 'a \<Rightarrow> 'b. inj h \<and> surj h"
     6.7 -  apply (rule decomposition [THEN exE])
     6.8 -  apply (rule exI)
     6.9 +  apply (rule decomposition [where f=f and g=g, THEN exE])
    6.10 +  apply (rule_tac x = "(\<lambda>z. if z \<in> x then f z else inv g z)" in exI) 
    6.11 +    --{*The term above can be synthesized by a sufficiently detailed proof.*}
    6.12    apply (rule bij_if_then_else)
    6.13       apply (rule_tac [4] refl)
    6.14      apply (rule_tac [2] inj_on_inv)
    6.15      apply (erule subset_inj_on [OF _ subset_UNIV])
    6.16 -   txt {* Tricky variable instantiations! *}
    6.17 -   apply (erule ssubst, simplesubst double_complement)
    6.18 -   apply (rule subsetI, erule imageE, erule ssubst, rule rangeI)
    6.19 -  apply (erule ssubst, simplesubst double_complement, erule inv_image_comp [symmetric])
    6.20 +   apply blast
    6.21 +  apply (erule ssubst, subst double_complement, erule inv_image_comp [symmetric])
    6.22    done
    6.23  
    6.24  
    6.25 -subsection {* Set variable instantiation examples *}
    6.26 -
    6.27  text {*
    6.28    From W. W. Bledsoe and Guohui Feng, SET-VAR. JAR 11 (3), 1993, pages
    6.29    293-314.