# HG changeset patch # User nipkow # Date 985861597 -7200 # Node ID 30d96882f91565a9269f7e7bbcfd4b45bcce518c # Parent 756c5034f08bbf33a41aa730ea3bda505c00c6c4 *** empty log message *** diff -r 756c5034f08b -r 30d96882f915 doc-src/TutorialI/CTL/CTL.thy --- a/doc-src/TutorialI/CTL/CTL.thy Thu Mar 29 10:44:37 2001 +0200 +++ b/doc-src/TutorialI/CTL/CTL.thy Thu Mar 29 12:26:37 2001 +0200 @@ -92,9 +92,9 @@ apply(rule subsetI); apply(simp, clarify); apply(erule converse_rtrancl_induct); - apply(rule ssubst[OF lfp_unfold[OF mono_ef]]); + apply(subst lfp_unfold[OF mono_ef]); apply(blast); -apply(rule ssubst[OF lfp_unfold[OF mono_ef]]); +apply(subst lfp_unfold[OF mono_ef]); by(blast); (*>*) text{* @@ -164,7 +164,7 @@ lemma not_in_lfp_afD: "s \ lfp(af A) \ s \ A \ (\ t. (s,t) \ M \ t \ lfp(af A))"; apply(erule contrapos_np); -apply(rule ssubst[OF lfp_unfold[OF mono_af]]); +apply(subst lfp_unfold[OF mono_af]); apply(simp add:af_def); done; @@ -406,10 +406,10 @@ apply(erule rev_mp); apply(rule_tac x = x in spec); apply(induct_tac p); - apply(rule ssubst[OF lfp_unfold[OF mono_eufix]]); + apply(subst lfp_unfold[OF mono_eufix]) apply(simp add:eufix_def); apply(clarsimp); -apply(rule ssubst[OF lfp_unfold[OF mono_eufix]]); +apply(subst lfp_unfold[OF mono_eufix]) apply(simp add:eufix_def); apply blast; done diff -r 756c5034f08b -r 30d96882f915 doc-src/TutorialI/CTL/PDL.thy --- a/doc-src/TutorialI/CTL/PDL.thy Thu Mar 29 10:44:37 2001 +0200 +++ b/doc-src/TutorialI/CTL/PDL.thy Thu Mar 29 12:26:37 2001 +0200 @@ -152,7 +152,7 @@ is solved by unrolling @{term lfp} once *} - apply(rule ssubst[OF lfp_unfold[OF mono_ef]]) + apply(subst lfp_unfold[OF mono_ef]) txt{* @{subgoals[display,indent=0,goals_limit=1]} @@ -165,7 +165,7 @@ The proof of the induction step is identical to the one for the base case: *} -apply(rule ssubst[OF lfp_unfold[OF mono_ef]]) +apply(subst lfp_unfold[OF mono_ef]) apply(blast) done @@ -205,7 +205,7 @@ lemma "(s \ EF f) = (s \ f | s \ Neg(AX(Neg(EF f))))"; apply(simp only:aux); apply(simp); -apply(rule ssubst[OF lfp_unfold[OF mono_ef]], fast); +apply(subst lfp_unfold[OF mono_ef], fast); done end diff -r 756c5034f08b -r 30d96882f915 doc-src/TutorialI/CTL/document/CTL.tex --- a/doc-src/TutorialI/CTL/document/CTL.tex Thu Mar 29 10:44:37 2001 +0200 +++ b/doc-src/TutorialI/CTL/document/CTL.tex Thu Mar 29 12:26:37 2001 +0200 @@ -121,7 +121,7 @@ \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 \isacommand{apply}{\isacharparenleft}erule\ contrapos{\isacharunderscore}np{\isacharparenright}\isanewline -\isacommand{apply}{\isacharparenleft}rule\ ssubst{\isacharbrackleft}OF\ lfp{\isacharunderscore}unfold{\isacharbrackleft}OF\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharbrackright}{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}subst\ lfp{\isacharunderscore}unfold{\isacharbrackleft}OF\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharparenright}\isanewline \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}af{\isacharunderscore}def{\isacharparenright}\isanewline \isacommand{done}% \begin{isamarkuptext}% diff -r 756c5034f08b -r 30d96882f915 doc-src/TutorialI/CTL/document/PDL.tex --- a/doc-src/TutorialI/CTL/document/PDL.tex Thu Mar 29 10:44:37 2001 +0200 +++ b/doc-src/TutorialI/CTL/document/PDL.tex Thu Mar 29 12:26:37 2001 +0200 @@ -153,7 +153,7 @@ \end{isabelle} is solved by unrolling \isa{lfp} once% \end{isamarkuptxt}% -\ \isacommand{apply}{\isacharparenleft}rule\ ssubst{\isacharbrackleft}OF\ lfp{\isacharunderscore}unfold{\isacharbrackleft}OF\ mono{\isacharunderscore}ef{\isacharbrackright}{\isacharbrackright}{\isacharparenright}% +\ \isacommand{apply}{\isacharparenleft}subst\ lfp{\isacharunderscore}unfold{\isacharbrackleft}OF\ mono{\isacharunderscore}ef{\isacharbrackright}{\isacharparenright}% \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}% @@ -165,7 +165,7 @@ \noindent The proof of the induction step is identical to the one for the base case:% \end{isamarkuptxt}% -\isacommand{apply}{\isacharparenleft}rule\ ssubst{\isacharbrackleft}OF\ lfp{\isacharunderscore}unfold{\isacharbrackleft}OF\ mono{\isacharunderscore}ef{\isacharbrackright}{\isacharbrackright}{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}subst\ lfp{\isacharunderscore}unfold{\isacharbrackleft}OF\ mono{\isacharunderscore}ef{\isacharbrackright}{\isacharparenright}\isanewline \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline \isacommand{done}% \begin{isamarkuptext}% diff -r 756c5034f08b -r 30d96882f915 doc-src/TutorialI/Recdef/document/examples.tex --- a/doc-src/TutorialI/Recdef/document/examples.tex Thu Mar 29 10:44:37 2001 +0200 +++ b/doc-src/TutorialI/Recdef/document/examples.tex Thu Mar 29 12:26:37 2001 +0200 @@ -73,17 +73,13 @@ \ \ {\isachardoublequote}sep{\isadigit{2}}\ xs\ \ \ \ \ \ \ {\isacharequal}\ {\isacharparenleft}{\isasymlambda}a{\isachardot}\ xs{\isacharparenright}{\isachardoublequote}% \begin{isamarkuptext}% Because of its pattern-matching syntax, \isacommand{recdef} is also useful -for the definition of non-recursive functions:% +for the definition of non-recursive functions, where the termination measure +degenerates to the empty set \isa{{\isacharbraceleft}{\isacharbraceright}}:% \end{isamarkuptext}% \isacommand{consts}\ swap{\isadigit{1}}{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline \isacommand{recdef}\ swap{\isadigit{1}}{\isadigit{2}}\ {\isachardoublequote}{\isacharbraceleft}{\isacharbraceright}{\isachardoublequote}\isanewline \ \ {\isachardoublequote}swap{\isadigit{1}}{\isadigit{2}}\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ y{\isacharhash}x{\isacharhash}zs{\isachardoublequote}\isanewline -\ \ {\isachardoublequote}swap{\isadigit{1}}{\isadigit{2}}\ zs\ \ \ \ \ \ \ {\isacharequal}\ zs{\isachardoublequote}% -\begin{isamarkuptext}% -\noindent -For non-recursive functions the termination measure degenerates to the empty -set \isa{{\isacharbraceleft}{\isacharbraceright}}.% -\end{isamarkuptext}% +\ \ {\isachardoublequote}swap{\isadigit{1}}{\isadigit{2}}\ zs\ \ \ \ \ \ \ {\isacharequal}\ zs{\isachardoublequote}\isanewline \end{isabellebody}% %%% Local Variables: %%% mode: latex diff -r 756c5034f08b -r 30d96882f915 doc-src/TutorialI/Recdef/examples.thy --- a/doc-src/TutorialI/Recdef/examples.thy Thu Mar 29 10:44:37 2001 +0200 +++ b/doc-src/TutorialI/Recdef/examples.thy Thu Mar 29 12:26:37 2001 +0200 @@ -79,7 +79,8 @@ text{* Because of its pattern-matching syntax, \isacommand{recdef} is also useful -for the definition of non-recursive functions: +for the definition of non-recursive functions, where the termination measure +degenerates to the empty set @{term"{}"}: *} consts swap12 :: "'a list \ 'a list"; @@ -87,11 +88,6 @@ "swap12 (x#y#zs) = y#x#zs" "swap12 zs = zs"; -text{*\noindent -For non-recursive functions the termination measure degenerates to the empty -set @{term"{}"}. -*} - (*<*) end (*>*)