--- 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 \<notin> lfp(af A) \<Longrightarrow> s \<notin> A \<and> (\<exists> t. (s,t) \<in> M \<and> t \<notin> 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
--- 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 \<Turnstile> EF f) = (s \<Turnstile> f | s \<Turnstile> 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
--- 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}%
--- 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}%
--- 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
--- 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 \<Rightarrow> '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
(*>*)