*** empty log message ***

--- a/doc-src/TutorialI/CTL/CTL.thy	Fri Oct 06 01:21:17 2000 +0200
+++ b/doc-src/TutorialI/CTL/CTL.thy	Fri Oct 06 12:31:53 2000 +0200
@@ -1,38 +1,38 @@
-(*<*)theory CTL = Base:(*>*)
+(*<*)theory CTL = Base:;(*>*)
 
-subsection{*Computation tree logic---CTL*}
+subsection{*Computation tree logic---CTL*};
 
 text{*
 The semantics of PDL only needs transitive reflexive closure.
 Let us now be a bit more adventurous and introduce a new temporal operator
 that goes beyond transitive reflexive closure. We extend the datatype
 @{text formula} by a new constructor
-*}
+*};
 (*<*)
 datatype formula = Atom atom
                   | Neg formula
                   | And formula formula
                   | AX formula
                   | EF formula(*>*)
-                  | AF formula
+                  | AF formula;
 
 text{*\noindent
 which stands for "always in the future":
-on all paths, at some point the formula holds. 
-Introducing the notion of paths (in @{term M})
-*}
+on all paths, at some point the formula holds. Formalizing the notion of an infinite path is easy
+in HOL: it is simply a function from @{typ nat} to @{typ state}.
+*};
 
 constdefs Paths :: "state \<Rightarrow> (nat \<Rightarrow> state)set"
          "Paths s \<equiv> {p. s = p 0 \<and> (\<forall>i. (p i, p(i+1)) \<in> M)}";
 
 text{*\noindent
-allows a very succinct definition of the semantics of @{term AF}:
+This definition allows a very succinct statement of the semantics of @{term AF}:
 \footnote{Do not be mislead: neither datatypes nor recursive functions can be
 extended by new constructors or equations. This is just a trick of the
 presentation. In reality one has to define a new datatype and a new function.}
-*}
+*};
 (*<*)
-consts valid :: "state \<Rightarrow> formula \<Rightarrow> bool" ("(_ \<Turnstile> _)" [80,80] 80)
+consts valid :: "state \<Rightarrow> formula \<Rightarrow> bool" ("(_ \<Turnstile> _)" [80,80] 80);
 
 primrec
 "s \<Turnstile> Atom a  =  (a \<in> L s)"
@@ -45,25 +45,16 @@
 
 text{*\noindent
 Model checking @{term AF} involves a function which
-is just large enough to warrant a separate definition:
-*}
+is just complicated enough to warrant a separate definition:
+*};
 
 constdefs af :: "state set \<Rightarrow> state set \<Rightarrow> state set"
          "af A T \<equiv> A \<union> {s. \<forall>t. (s, t) \<in> M \<longrightarrow> t \<in> T}";
 
 text{*\noindent
-This function is monotone in its second argument (and also its first, but
-that is irrelevant), and hence @{term"af A"} has a least fixpoint.
-*}
-
-lemma mono_af: "mono(af A)";
-apply(simp add: mono_def af_def)
-by(blast);
-
-text{*\noindent
-Now we can define @{term "mc(AF f)"} as the least set @{term T} that contains
+Now we define @{term "mc(AF f)"} as the least set @{term T} that contains
 @{term"mc f"} and all states all of whose direct successors are in @{term T}:
-*}
+*};
 (*<*)
 consts mc :: "formula \<Rightarrow> state set";
 primrec
@@ -73,48 +64,107 @@
 "mc(AX f)    = {s. \<forall>t. (s,t) \<in> M  \<longrightarrow> t \<in> mc f}"
 "mc(EF f)    = lfp(\<lambda>T. mc f \<union> M^-1 ^^ T)"(*>*)
 "mc(AF f)    = lfp(af(mc f))";
+
+text{*\noindent
+Because @{term af} is monotone in its second argument (and also its first, but
+that is irrelevant) @{term"af A"} has a least fixpoint:
+*};
+
+lemma mono_af: "mono(af A)";
+apply(simp add: mono_def af_def);
+apply blast;
+done
 (*<*)
-lemma mono_ef: "mono(\<lambda>T. A \<union> M^-1 ^^ T)"
-apply(rule monoI)
-by(blast)
+lemma mono_ef: "mono(\<lambda>T. A \<union> M^-1 ^^ T)";
+apply(rule monoI);
+by(blast);
 
 lemma EF_lemma:
-  "lfp(\<lambda>T. A \<union> M^-1 ^^ T) = {s. \<exists>t. (s,t) \<in> M^* \<and> t \<in> A}"
+  "lfp(\<lambda>T. A \<union> M^-1 ^^ T) = {s. \<exists>t. (s,t) \<in> M^* \<and> t \<in> A}";
 apply(rule equalityI);
  apply(rule subsetI);
- apply(simp)
- apply(erule Lfp.induct)
-  apply(rule mono_ef)
- apply(simp)
+ apply(simp);
+ apply(erule Lfp.induct);
+  apply(rule mono_ef);
+ apply(simp);
  apply(blast intro: r_into_rtrancl rtrancl_trans);
-apply(rule subsetI)
-apply(simp, clarify)
-apply(erule converse_rtrancl_induct)
- apply(rule ssubst[OF lfp_Tarski[OF mono_ef]])
- apply(blast)
-apply(rule ssubst[OF lfp_Tarski[OF mono_ef]])
-by(blast)
+apply(rule subsetI);
+apply(simp, clarify);
+apply(erule converse_rtrancl_induct);
+ apply(rule ssubst[OF lfp_Tarski[OF mono_ef]]);
+ apply(blast);
+apply(rule ssubst[OF lfp_Tarski[OF mono_ef]]);
+by(blast);
 (*>*)
+text{*
+All we need to prove now is that @{term mc} and @{text"\<Turnstile>"}
+agree for @{term AF}, i.e.\ that @{prop"mc(AF f) = {s. s \<Turnstile>
+AF f}"}. This time we prove the two containments separately, starting
+with the easy one:
+*};
 
-theorem lfp_subset_AF:
-"lfp(af A) \<subseteq> {s. \<forall> p \<in> Paths s. \<exists> i. p i \<in> A}";
+theorem AF_lemma1:
+  "lfp(af A) \<subseteq> {s. \<forall> p \<in> Paths s. \<exists> i. p i \<in> A}";
+
+txt{*\noindent
+The proof is again pointwise. Fixpoint induction on the premise @{prop"s \<in> lfp(af A)"} followed
+by simplification and clarification
+*};
+
 apply(rule subsetI);
 apply(erule Lfp.induct[OF _ mono_af]);
-apply(simp add: af_def Paths_def);
+apply(clarsimp simp add: af_def Paths_def);
+(*ML"Pretty.setmargin 70";
+pr(latex xsymbols symbols);*)
+txt{*\noindent
+FIXME OF/of with undescore?
+
+leads to the following somewhat involved proof state
+\begin{isabelle}
+\ \isadigit{1}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}p\ \isadigit{0}\ {\isasymin}\ A\ {\isasymor}\isanewline
+\ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymforall}t{\isachardot}\ {\isacharparenleft}p\ \isadigit{0}{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymlongrightarrow}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\ {\isasymand}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\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
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ {\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isasymrbrakk}\isanewline
+\ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A
+\end{isabelle}
+Now we eliminate the disjunction. The case @{prop"p 0 \<in> A"} is trivial:
+*};
+
 apply(erule disjE);
  apply(blast);
-apply(clarify);
+
+txt{*\noindent
+In the other case we set @{term t} to @{term"p 1"} and simplify matters:
+*};
+
 apply(erule_tac x = "p 1" in allE);
 apply(clarsimp);
+(*ML"Pretty.setmargin 70";
+pr(latex xsymbols symbols);*)
+
+txt{*
+\begin{isabelle}
+\ \isadigit{1}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharsemicolon}\ p\ \isadigit{1}\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}{\isacharsemicolon}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ {\isasymforall}pa{\isachardot}\ p\ \isadigit{1}\ {\isacharequal}\ pa\ \isadigit{0}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}pa\ i{\isacharcomma}\ pa\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}\ {\isasymlongrightarrow}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymexists}i{\isachardot}\ pa\ i\ {\isasymin}\ A{\isacharparenright}{\isasymrbrakk}\isanewline
+\ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A
+\end{isabelle}
+It merely remains to set @{term pa} to @{term"\<lambda>i. p(i+1)"}, i.e.\ @{term p} without its
+first element. The rest is practically automatic:
+*};
+
 apply(erule_tac x = "\<lambda>i. p(i+1)" in allE);
-apply(simp);
-by(blast);
+apply simp;
+apply blast;
+done;
 
 text{*
-The opposite direction is proved by contradiction: if some state
-{term s} is not in @{term"lfp(af A)"}, then we can construct an
+The opposite containment is proved by contradiction: if some state
+@{term s} is not in @{term"lfp(af A)"}, then we can construct an
 infinite @{term A}-avoiding path starting from @{term s}. The reason is
-that by unfolding @{term"lfp"} we find that if @{term s} is not in
+that by unfolding @{term lfp} we find that if @{term s} is not in
 @{term"lfp(af A)"}, then @{term s} is not in @{term A} and there is a
 direct successor of @{term s} that is again not in @{term"lfp(af
 A)"}. Iterating this argument yields the promised infinite
@@ -127,7 +177,8 @@
  "s \<notin> lfp(af A) \<Longrightarrow> s \<notin> A \<and> (\<exists> t. (s,t)\<in>M \<and> t \<notin> lfp(af A))";
 apply(erule swap);
 apply(rule ssubst[OF lfp_Tarski[OF mono_af]]);
-by(simp add:af_def);
+apply(simp add:af_def);
+done;
 
 text{*\noindent
 is proved by a variant of contraposition (@{thm[source]swap}:
@@ -146,44 +197,109 @@
 
 text{*\noindent
 Element @{term"n+1"} on this path is some arbitrary successor
-@{term"t"} of element @{term"n"} such that @{term"P t"} holds.  Of
-course, such a @{term"t"} may in general not exist, but that is of no
+@{term t} of element @{term n} such that @{term"P t"} holds.  Remember that @{text"SOME t. R t"}
+is some arbitrary but fixed @{term t} such that @{prop"R t"} holds (see \S\ref{sec-SOME}). Of
+course, such a @{term t} may in general not exist, but that is of no
 concern to us since we will only use @{term path} in such cases where a
-suitable @{term"t"} does exist.
+suitable @{term t} does exist.
 
-Now we prove that if each state @{term"s"} that satisfies @{term"P"}
-has a successor that again satisfies @{term"P"}, then there exists an infinite @{term"P"}-path.
+Let us show that if each state @{term s} that satisfies @{term P}
+has a successor that again satisfies @{term P}, then there exists an infinite @{term P}-path:
 *};
 
-lemma seq_lemma:
-"\<lbrakk> P s; \<forall>s. P s \<longrightarrow> (\<exists> t. (s,t)\<in>M \<and> P t) \<rbrakk> \<Longrightarrow> \<exists>p\<in>Paths s. \<forall>i. P(p i)";
+lemma infinity_lemma:
+  "\<lbrakk> P s; \<forall>s. P s \<longrightarrow> (\<exists> t. (s,t) \<in> M \<and> P t) \<rbrakk> \<Longrightarrow>
+   \<exists>p\<in>Paths s. \<forall>i. P(p i)";
 
 txt{*\noindent
 First we rephrase the conclusion slightly because we need to prove both the path property
-and the fact that @{term"P"} holds simultaneously:
+and the fact that @{term P} holds simultaneously:
 *};
 
-apply(subgoal_tac "\<exists> p. s = p 0 \<and> (\<forall> i. (p i,p(i+1)) \<in> M \<and> P(p i))");
+apply(subgoal_tac "\<exists>p. s = p 0 \<and> (\<forall>i. (p i,p(i+1)) \<in> M \<and> P(p i))");
 
 txt{*\noindent
-From this proposition the original goal follows easily
+From this proposition the original goal follows easily:
 *};
 
  apply(simp add:Paths_def, blast);
+
+txt{*\noindent
+The new subgoal is proved by providing the witness @{term "path s P"} for @{term p}:
+*};
+
 apply(rule_tac x = "path s P" in exI);
-apply(simp);
-apply(intro strip);
+apply(clarsimp);
+(*ML"Pretty.setmargin 70";
+pr(latex xsymbols symbols);*)
+
+txt{*\noindent
+After simplification and clarification the subgoal has the following compact form
+\begin{isabelle}
+\ \isadigit{1}{\isachardot}\ {\isasymAnd}i{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ {\isasymforall}s{\isachardot}\ P\ s\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}{\isasymrbrakk}\isanewline
+\ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}path\ s\ P\ i{\isacharcomma}\ SOME\ t{\isachardot}\ {\isacharparenleft}path\ s\ P\ i{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ P\ {\isacharparenleft}path\ s\ P\ i{\isacharparenright}
+\end{isabelle}
+and invites a proof by induction on @{term i}:
+*};
+
 apply(induct_tac i);
  apply(simp);
+(*ML"Pretty.setmargin 70";
+pr(latex xsymbols symbols);*)
+
+txt{*\noindent
+After simplification the base case boils down to
+\begin{isabelle}
+\ \isadigit{1}{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ {\isasymforall}s{\isachardot}\ P\ s\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}{\isasymrbrakk}\isanewline
+\ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}s{\isacharcomma}\ SOME\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}\ {\isasymin}\ M
+\end{isabelle}
+The conclusion looks exceedingly trivial: after all, @{term t} is chosen such that @{prop"(s,t):M"}
+holds. However, we first have to show that such a @{term t} actually exists! This reasoning
+is embodied in the theorem @{thm[source]someI2_ex}:
+@{thm[display,eta_contract=false]someI2_ex}
+When we apply this theorem as an introduction rule, @{text"?P x"} becomes
+@{prop"(s, x) : M & P x"} and @{text"?Q x"} becomes @{prop"(s,x) : M"} and we have to prove
+two subgoals: @{prop"EX a. (s, a) : M & P a"}, which follows from the assumptions, and
+@{prop"(s, x) : M & P x ==> (s,x) : M"}, which is trivial. Thus it is not surprising that
+@{text fast} can prove the base case quickly:
+*};
+
  apply(fast intro:someI2_ex);
+
+txt{*\noindent
+What is worth noting here is that we have used @{text fast} rather than @{text blast}.
+The reason is that @{text blast} would fail because it cannot cope with @{thm[source]someI2_ex}:
+unifying its conclusion with the current subgoal is nontrivial because of the nested schematic
+variables. For efficiency reasons @{text blast} does not even attempt such unifications.
+Although @{text 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.
+
+The induction step is similar, but more involved, because now we face nested occurrences of
+@{text SOME}. We merely show the proof commands but do not describe th details:
+*};
+
 apply(simp);
 apply(rule someI2_ex);
  apply(blast);
 apply(rule someI2_ex);
  apply(blast);
-by(blast);
+apply(blast);
+done;
 
-lemma seq_lemma:
+text{*
+Function @{term path} has fulfilled its purpose now and can be forgotten
+about. It was merely defined to provide the witness in the proof of the
+@{thm[source]infinity_lemma}. Afficionados of minimal proofs might like to know
+that we could have given the witness without having to define a new function:
+the term
+@{term[display]"nat_rec s (\<lambda>n t. SOME u. (t,u)\<in>M \<and> P u)"}
+where @{term nat_rec} is the predefined primitive recursor on @{typ nat}, whose defining
+equations we omit, is extensionally equal to @{term"path s P"}.
+*};
+(*<*)
+lemma infinity_lemma:
 "\<lbrakk> P s; \<forall> s. P s \<longrightarrow> (\<exists> t. (s,t)\<in>M \<and> P t) \<rbrakk> \<Longrightarrow>
  \<exists> p\<in>Paths s. \<forall> i. P(p i)";
 apply(subgoal_tac
@@ -202,16 +318,70 @@
 apply(rule someI2_ex);
  apply(blast);
 by(blast);
+(*>*)
 
-theorem AF_subset_lfp:
+text{*
+At last we can prove the opposite direction of @{thm[source]AF_lemma1}:
+*};
+
+theorem AF_lemma2:
 "{s. \<forall> p \<in> Paths s. \<exists> i. p i \<in> A} \<subseteq> lfp(af A)";
+
+txt{*\noindent
+The proof is again pointwise and then by contraposition (@{thm[source]contrapos2} is the rule
+@{thm contrapos2}):
+*};
+
 apply(rule subsetI);
 apply(erule contrapos2);
 apply simp;
-apply(drule seq_lemma);
-by(auto dest:not_in_lfp_afD);
+(*pr(latex xsymbols symbols);*)
+
+txt{*
+\begin{isabelle}
+\ \isadigit{1}{\isachardot}\ {\isasymAnd}s{\isachardot}\ s\ {\isasymnotin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ A
+\end{isabelle}
+Applying the @{thm[source]infinity_lemma} as a destruction rule leaves two subgoals, the second
+premise of @{thm[source]infinity_lemma} and the original subgoal:
+*};
+
+apply(drule infinity_lemma);
+(*pr(latex xsymbols symbols);*)
+
+txt{*
+\begin{isabelle}
+\ \isadigit{1}{\isachardot}\ {\isasymAnd}s{\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}s{\isachardot}\ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\isanewline
+\ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ A
+\end{isabelle}
+Both are solved automatically:
+*};
 
+ apply(auto dest:not_in_lfp_afD);
+done;
 
+text{*
+The main theorem is proved as for PDL, except that we also derive the necessary equality
+@{text"lfp(af A) = ..."} by combining @{thm[source]AF_lemma1} and @{thm[source]AF_lemma2}
+on the spot:
+*}
+
+theorem "mc f = {s. s \<Turnstile> f}";
+apply(induct_tac f);
+apply(auto simp add: EF_lemma equalityI[OF AF_lemma1 AF_lemma2]);
+done
+
+text{*
+Let us close this section with a few words about the executability of @{term mc}.
+It is clear that if all sets are finite, they can be represented as lists and the usual
+set operations are easily implemented. Only @{term lfp} requires a little thought.
+Fortunately the HOL library proves that in the case of finite sets and a monotone @{term F},
+@{term"lfp F"} can be computed by iterated application of @{term F} to @{term"{}"} until
+a fixpoint is reached. It is possible to generate executable functional programs
+from HOL definitions, but that is beyond the scope of the tutorial.
+*}
+
+(*<*)
 (*
 Second proof of opposite direction, directly by wellfounded induction
 on the initial segment of M that avoids A.
@@ -252,16 +422,11 @@
 apply(rule ex_infinite_path);
 by(auto);
 
-theorem AF_subset_lfp:
+theorem AF_lemma2:
 "{s. \<forall>p \<in> Paths s. \<exists> i. p i \<in> A} \<subseteq> lfp(af A)";
 apply(rule subsetI);
 apply(simp);
 apply(erule Avoid_in_lfp);
 by(rule Avoid.intros);
 
-
-theorem "mc f = {s. s \<Turnstile> f}";
-apply(induct_tac f);
-by(auto simp add: EF_lemma equalityI[OF lfp_subset_AF AF_subset_lfp]);
-
-(*<*)end(*>*)
+end(*>*)

--- a/doc-src/TutorialI/CTL/PDL.thy	Fri Oct 06 01:21:17 2000 +0200
+++ b/doc-src/TutorialI/CTL/PDL.thy	Fri Oct 06 12:31:53 2000 +0200
@@ -77,7 +77,8 @@
 
 lemma mono_ef: "mono(\<lambda>T. A \<union> M^-1 ^^ T)"
 apply(rule monoI)
-by(blast)
+apply blast
+done
 
 text{*\noindent
 in order to make sure it really has a least fixpoint.
@@ -174,7 +175,8 @@
 *}
 
 apply(rule ssubst[OF lfp_Tarski[OF mono_ef]])
-by(blast)
+apply(blast)
+done
 
 text{*
 The main theorem is proved in the familiar manner: induction followed by
@@ -183,5 +185,6 @@
 
 theorem "mc f = {s. s \<Turnstile> f}";
 apply(induct_tac f);
-by(auto simp add:EF_lemma);
+apply(auto simp add:EF_lemma);
+done;
 (*<*)end(*>*)

--- a/doc-src/TutorialI/CTL/document/CTL.tex	Fri Oct 06 01:21:17 2000 +0200
+++ b/doc-src/TutorialI/CTL/document/CTL.tex	Fri Oct 06 12:31:53 2000 +0200
@@ -14,14 +14,14 @@
 \begin{isamarkuptext}%
 \noindent
 which stands for "always in the future":
-on all paths, at some point the formula holds. 
-Introducing the notion of paths (in \isa{M})%
+on all paths, at some point the formula holds. Formalizing the notion of an infinite path is easy
+in HOL: it is simply a function from \isa{nat} to \isa{state}.%
 \end{isamarkuptext}%
 \isacommand{constdefs}\ Paths\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ state{\isacharparenright}set{\isachardoublequote}\isanewline
 \ \ \ \ \ \ \ \ \ {\isachardoublequote}Paths\ s\ {\isasymequiv}\ {\isacharbraceleft}p{\isachardot}\ s\ {\isacharequal}\ p\ \isadigit{0}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p{\isacharparenleft}i{\isacharplus}\isadigit{1}{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}{\isacharbraceright}{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent
-allows a very succinct definition of the semantics of \isa{AF}:
+This definition allows a very succinct statement of the semantics of \isa{AF}:
 \footnote{Do not be mislead: neither datatypes nor recursive functions can be
 extended by new constructors or equations. This is just a trick of the
 presentation. In reality one has to define a new datatype and a new function.}%
@@ -30,40 +30,81 @@
 \begin{isamarkuptext}%
 \noindent
 Model checking \isa{AF} involves a function which
-is just large enough to warrant a separate definition:%
+is just complicated enough to warrant a separate definition:%
 \end{isamarkuptext}%
 \isacommand{constdefs}\ af\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ set\ {\isasymRightarrow}\ state\ set\ {\isasymRightarrow}\ state\ set{\isachardoublequote}\isanewline
 \ \ \ \ \ \ \ \ \ {\isachardoublequote}af\ A\ T\ {\isasymequiv}\ A\ {\isasymunion}\ {\isacharbraceleft}s{\isachardot}\ {\isasymforall}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymlongrightarrow}\ t\ {\isasymin}\ T{\isacharbraceright}{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent
-This function is monotone in its second argument (and also its first, but
-that is irrelevant), and hence \isa{af\ A} has a least fixpoint.%
+Now we define \isa{mc\ {\isacharparenleft}AF\ f{\isacharparenright}} as the least set \isa{T} that contains
+\isa{mc\ f} and all states all of whose direct successors are in \isa{T}:%
+\end{isamarkuptext}%
+{\isachardoublequote}mc{\isacharparenleft}AF\ f{\isacharparenright}\ \ \ \ {\isacharequal}\ lfp{\isacharparenleft}af{\isacharparenleft}mc\ f{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
+\begin{isamarkuptext}%
+\noindent
+Because \isa{af} is monotone in its second argument (and also its first, but
+that is irrelevant) \isa{af\ A} has a least fixpoint:%
 \end{isamarkuptext}%
 \isacommand{lemma}\ mono{\isacharunderscore}af{\isacharcolon}\ {\isachardoublequote}mono{\isacharparenleft}af\ A{\isacharparenright}{\isachardoublequote}\isanewline
 \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ mono{\isacharunderscore}def\ af{\isacharunderscore}def{\isacharparenright}\isanewline
-\isacommand{by}{\isacharparenleft}blast{\isacharparenright}%
+\isacommand{apply}\ blast\isanewline
+\isacommand{done}%
 \begin{isamarkuptext}%
+All we need to prove now is that \isa{mc} and \isa{{\isasymTurnstile}}
+agree for \isa{AF}, i.e.\ that \isa{mc\ {\isacharparenleft}AF\ f{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ AF\ f{\isacharbraceright}}. This time we prove the two containments separately, starting
+with the easy one:%
+\end{isamarkuptext}%
+\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}%
+\begin{isamarkuptxt}%
 \noindent
-Now we can define \isa{mc\ {\isacharparenleft}AF\ f{\isacharparenright}} as the least set \isa{T} that contains
-\isa{mc\ f} and all states all of whose direct successors are in \isa{T}:%
-\end{isamarkuptext}%
-{\isachardoublequote}mc{\isacharparenleft}AF\ f{\isacharparenright}\ \ \ \ {\isacharequal}\ lfp{\isacharparenleft}af{\isacharparenleft}mc\ f{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
-\isacommand{theorem}\ lfp{\isacharunderscore}subset{\isacharunderscore}AF{\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}\isanewline
+The proof is again pointwise. Fixpoint induction on the premise \isa{s\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}} followed
+by simplification and clarification%
+\end{isamarkuptxt}%
 \isacommand{apply}{\isacharparenleft}rule\ subsetI{\isacharparenright}\isanewline
 \isacommand{apply}{\isacharparenleft}erule\ Lfp{\isachardot}induct{\isacharbrackleft}OF\ {\isacharunderscore}\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharparenright}\isanewline
-\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ af{\isacharunderscore}def\ Paths{\isacharunderscore}def{\isacharparenright}\isanewline
+\isacommand{apply}{\isacharparenleft}clarsimp\ simp\ add{\isacharcolon}\ af{\isacharunderscore}def\ Paths{\isacharunderscore}def{\isacharparenright}%
+\begin{isamarkuptxt}%
+\noindent
+FIXME OF/of with undescore?
+
+leads to the following somewhat involved proof state
+\begin{isabelle}
+\ \isadigit{1}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}p\ \isadigit{0}\ {\isasymin}\ A\ {\isasymor}\isanewline
+\ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymforall}t{\isachardot}\ {\isacharparenleft}p\ \isadigit{0}{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymlongrightarrow}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\ {\isasymand}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\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
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ {\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isasymrbrakk}\isanewline
+\ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A
+\end{isabelle}
+Now we eliminate the disjunction. The case \isa{p\ \isadigit{0}\ {\isasymin}\ A} is trivial:%
+\end{isamarkuptxt}%
 \isacommand{apply}{\isacharparenleft}erule\ disjE{\isacharparenright}\isanewline
-\ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
-\isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline
+\ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}%
+\begin{isamarkuptxt}%
+\noindent
+In the other case we set \isa{t} to \isa{p\ \isadigit{1}} and simplify matters:%
+\end{isamarkuptxt}%
 \isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}p\ \isadigit{1}{\isachardoublequote}\ \isakeyword{in}\ allE{\isacharparenright}\isanewline
-\isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}\isanewline
+\isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}%
+\begin{isamarkuptxt}%
+\begin{isabelle}
+\ \isadigit{1}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharsemicolon}\ p\ \isadigit{1}\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}{\isacharsemicolon}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ {\isasymforall}pa{\isachardot}\ p\ \isadigit{1}\ {\isacharequal}\ pa\ \isadigit{0}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}pa\ i{\isacharcomma}\ pa\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}\ {\isasymlongrightarrow}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymexists}i{\isachardot}\ pa\ i\ {\isasymin}\ A{\isacharparenright}{\isasymrbrakk}\isanewline
+\ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A
+\end{isabelle}
+It merely remains to set \isa{pa} to \isa{{\isasymlambda}i{\isachardot}\ p\ {\isacharparenleft}i\ {\isacharplus}\ \isadigit{1}{\isacharparenright}}, i.e.\ \isa{p} without its
+first element. The rest is practically automatic:%
+\end{isamarkuptxt}%
 \isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}{\isasymlambda}i{\isachardot}\ p{\isacharparenleft}i{\isacharplus}\isadigit{1}{\isacharparenright}{\isachardoublequote}\ \isakeyword{in}\ allE{\isacharparenright}\isanewline
-\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
-\isacommand{by}{\isacharparenleft}blast{\isacharparenright}%
+\isacommand{apply}\ simp\isanewline
+\isacommand{apply}\ blast\isanewline
+\isacommand{done}%
 \begin{isamarkuptext}%
-The opposite direction is proved by contradiction: if some state
-{term s} is not in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}, then we can construct an
+The opposite containment is proved by contradiction: if some state
+\isa{s} is not in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}, then we can construct an
 infinite \isa{A}-avoiding path starting from \isa{s}. The reason is
 that by unfolding \isa{lfp} we find that if \isa{s} is not in
 \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}, then \isa{s} is not in \isa{A} and there is a
@@ -76,7 +117,8 @@
 \ {\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\ swap{\isacharparenright}\isanewline
 \isacommand{apply}{\isacharparenleft}rule\ ssubst{\isacharbrackleft}OF\ lfp{\isacharunderscore}Tarski{\isacharbrackleft}OF\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharbrackright}{\isacharparenright}\isanewline
-\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}af{\isacharunderscore}def{\isacharparenright}%
+\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}af{\isacharunderscore}def{\isacharparenright}\isanewline
+\isacommand{done}%
 \begin{isamarkuptext}%
 \noindent
 is proved by a variant of contraposition (\isa{swap}:
@@ -94,113 +136,149 @@
 \begin{isamarkuptext}%
 \noindent
 Element \isa{n\ {\isacharplus}\ \isadigit{1}} on this path is some arbitrary successor
-\isa{t} of element \isa{n} such that \isa{P\ t} holds.  Of
+\isa{t} of element \isa{n} such that \isa{P\ t} holds.  Remember that \isa{SOME\ t{\isachardot}\ R\ t}
+is some arbitrary but fixed \isa{t} such that \isa{R\ t} holds (see \S\ref{sec-SOME}). Of
 course, such a \isa{t} may in general not exist, but that is of no
 concern to us since we will only use \isa{path} in such cases where a
 suitable \isa{t} does exist.
 
-Now we prove that if each state \isa{s} that satisfies \isa{P}
-has a successor that again satisfies \isa{P}, then there exists an infinite \isa{P}-path.%
+Let us show that if each state \isa{s} that satisfies \isa{P}
+has a successor that again satisfies \isa{P}, then there exists an infinite \isa{P}-path:%
 \end{isamarkuptext}%
-\isacommand{lemma}\ seq{\isacharunderscore}lemma{\isacharcolon}\isanewline
-{\isachardoublequote}{\isasymlbrakk}\ P\ s{\isacharsemicolon}\ {\isasymforall}s{\isachardot}\ P\ s\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}{\isasymin}M\ {\isasymand}\ P\ t{\isacharparenright}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ P{\isacharparenleft}p\ i{\isacharparenright}{\isachardoublequote}%
+\isacommand{lemma}\ infinity{\isacharunderscore}lemma{\isacharcolon}\isanewline
+\ \ {\isachardoublequote}{\isasymlbrakk}\ P\ s{\isacharsemicolon}\ {\isasymforall}s{\isachardot}\ P\ s\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\isanewline
+\ \ \ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ P{\isacharparenleft}p\ i{\isacharparenright}{\isachardoublequote}%
 \begin{isamarkuptxt}%
 \noindent
 First we rephrase the conclusion slightly because we need to prove both the path property
 and the fact that \isa{P} holds simultaneously:%
 \end{isamarkuptxt}%
-\isacommand{apply}{\isacharparenleft}subgoal{\isacharunderscore}tac\ {\isachardoublequote}{\isasymexists}\ p{\isachardot}\ s\ {\isacharequal}\ p\ \isadigit{0}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}\ i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}p{\isacharparenleft}i{\isacharplus}\isadigit{1}{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P{\isacharparenleft}p\ i{\isacharparenright}{\isacharparenright}{\isachardoublequote}{\isacharparenright}%
+\isacommand{apply}{\isacharparenleft}subgoal{\isacharunderscore}tac\ {\isachardoublequote}{\isasymexists}p{\isachardot}\ s\ {\isacharequal}\ p\ \isadigit{0}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}p{\isacharparenleft}i{\isacharplus}\isadigit{1}{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P{\isacharparenleft}p\ i{\isacharparenright}{\isacharparenright}{\isachardoublequote}{\isacharparenright}%
+\begin{isamarkuptxt}%
+\noindent
+From this proposition the original goal follows easily:%
+\end{isamarkuptxt}%
+\ \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}Paths{\isacharunderscore}def{\isacharcomma}\ blast{\isacharparenright}%
+\begin{isamarkuptxt}%
+\noindent
+The new subgoal is proved by providing the witness \isa{path\ s\ P} for \isa{p}:%
+\end{isamarkuptxt}%
+\isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}path\ s\ P{\isachardoublequote}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline
+\isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}%
+\begin{isamarkuptxt}%
+\noindent
+After simplification and clarification the subgoal has the following compact form
+\begin{isabelle}
+\ \isadigit{1}{\isachardot}\ {\isasymAnd}i{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ {\isasymforall}s{\isachardot}\ P\ s\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}{\isasymrbrakk}\isanewline
+\ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}path\ s\ P\ i{\isacharcomma}\ SOME\ t{\isachardot}\ {\isacharparenleft}path\ s\ P\ i{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ P\ {\isacharparenleft}path\ s\ P\ i{\isacharparenright}
+\end{isabelle}
+and invites a proof by induction on \isa{i}:%
+\end{isamarkuptxt}%
+\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ i{\isacharparenright}\isanewline
+\ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}%
 \begin{isamarkuptxt}%
 \noindent
-From this proposition the original goal follows easily%
+After simplification the base case boils down to
+\begin{isabelle}
+\ \isadigit{1}{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ {\isasymforall}s{\isachardot}\ P\ s\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}{\isasymrbrakk}\isanewline
+\ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}s{\isacharcomma}\ SOME\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ 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}Eps\ {\isacharquery}P{\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}\ P\ 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}\ P\ a}, which follows from the assumptions, and
+\isa{{\isacharparenleft}s{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ 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}%
-\ \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}Paths{\isacharunderscore}def{\isacharcomma}\ blast{\isacharparenright}\isanewline
-\isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}path\ s\ P{\isachardoublequote}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline
-\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
-\isacommand{apply}{\isacharparenleft}intro\ strip{\isacharparenright}\isanewline
-\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ i{\isacharparenright}\isanewline
-\ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
-\ \isacommand{apply}{\isacharparenleft}fast\ intro{\isacharcolon}someI\isadigit{2}{\isacharunderscore}ex{\isacharparenright}\isanewline
-\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
-\isacommand{apply}{\isacharparenleft}rule\ someI\isadigit{2}{\isacharunderscore}ex{\isacharparenright}\isanewline
-\ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
-\isacommand{apply}{\isacharparenleft}rule\ someI\isadigit{2}{\isacharunderscore}ex{\isacharparenright}\isanewline
-\ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
-\isacommand{by}{\isacharparenleft}blast{\isacharparenright}\isanewline
-\isanewline
-\isacommand{lemma}\ seq{\isacharunderscore}lemma{\isacharcolon}\isanewline
-{\isachardoublequote}{\isasymlbrakk}\ P\ s{\isacharsemicolon}\ {\isasymforall}\ s{\isachardot}\ P\ s\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}{\isasymin}M\ {\isasymand}\ P\ t{\isacharparenright}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\isanewline
-\ {\isasymexists}\ p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}\ i{\isachardot}\ P{\isacharparenleft}p\ i{\isacharparenright}{\isachardoublequote}\isanewline
-\isacommand{apply}{\isacharparenleft}subgoal{\isacharunderscore}tac\isanewline
-\ {\isachardoublequote}{\isasymexists}\ p{\isachardot}\ s\ {\isacharequal}\ p\ \isadigit{0}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}\ i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}p{\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}{\isasymin}M\ {\isasymand}\ P{\isacharparenleft}p\ i{\isacharparenright}{\isacharparenright}{\isachardoublequote}{\isacharparenright}\isanewline
-\ \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}Paths{\isacharunderscore}def{\isacharparenright}\isanewline
-\ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
-\isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}nat{\isacharunderscore}rec\ s\ {\isacharparenleft}{\isasymlambda}n\ t{\isachardot}\ SOME\ u{\isachardot}\ {\isacharparenleft}t{\isacharcomma}u{\isacharparenright}{\isasymin}M\ {\isasymand}\ P\ u{\isacharparenright}{\isachardoublequote}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline
-\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
-\isacommand{apply}{\isacharparenleft}intro\ strip{\isacharparenright}\isanewline
-\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ i{\isacharparenright}\isanewline
-\ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
-\ \isacommand{apply}{\isacharparenleft}fast\ intro{\isacharcolon}someI\isadigit{2}{\isacharunderscore}ex{\isacharparenright}\isanewline
+\ \isacommand{apply}{\isacharparenleft}fast\ intro{\isacharcolon}someI\isadigit{2}{\isacharunderscore}ex{\isacharparenright}%
+\begin{isamarkuptxt}%
+\noindent
+What is worth noting here is that we have used \isa{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 nontrivial 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.
+
+The induction step is similar, but more involved, because now we face nested occurrences of
+\isa{SOME}. We merely show the proof commands but do not describe th details:%
+\end{isamarkuptxt}%
 \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
 \isacommand{apply}{\isacharparenleft}rule\ someI\isadigit{2}{\isacharunderscore}ex{\isacharparenright}\isanewline
 \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
 \isacommand{apply}{\isacharparenleft}rule\ someI\isadigit{2}{\isacharunderscore}ex{\isacharparenright}\isanewline
 \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
-\isacommand{by}{\isacharparenleft}blast{\isacharparenright}\isanewline
-\isanewline
-\isacommand{theorem}\ AF{\isacharunderscore}subset{\isacharunderscore}lfp{\isacharcolon}\isanewline
-{\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
+\isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
+\isacommand{done}%
+\begin{isamarkuptext}%
+Function \isa{path} has fulfilled its purpose now and can be forgotten
+about. It was merely defined to provide the witness in the proof of the
+\isa{infinity{\isacharunderscore}lemma}. Afficionados of minimal proofs might like to know
+that we could have given the witness without having to define a new function:
+the term
+\begin{isabelle}%
+\ \ \ \ \ nat{\isacharunderscore}rec\ s\ {\isacharparenleft}{\isasymlambda}n\ t{\isachardot}\ SOME\ u{\isachardot}\ {\isacharparenleft}t{\isacharcomma}\ u{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ u{\isacharparenright}%
+\end{isabelle}
+where \isa{nat{\isacharunderscore}rec} is the predefined primitive recursor on \isa{nat}, whose defining
+equations we omit, is extensionally equal to \isa{path\ s\ P}.%
+\end{isamarkuptext}%
+%
+\begin{isamarkuptext}%
+At last we can prove the opposite direction of \isa{AF{\isacharunderscore}lemma\isadigit{1}}:%
+\end{isamarkuptext}%
+\isacommand{theorem}\ AF{\isacharunderscore}lemma\isadigit{2}{\isacharcolon}\isanewline
+{\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}%
+\begin{isamarkuptxt}%
+\noindent
+The proof is again pointwise and then by contraposition (\isa{contrapos\isadigit{2}} is the rule
+\isa{{\isasymlbrakk}{\isacharquery}Q{\isacharsemicolon}\ {\isasymnot}\ {\isacharquery}P\ {\isasymLongrightarrow}\ {\isasymnot}\ {\isacharquery}Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}P}):%
+\end{isamarkuptxt}%
 \isacommand{apply}{\isacharparenleft}rule\ subsetI{\isacharparenright}\isanewline
 \isacommand{apply}{\isacharparenleft}erule\ contrapos\isadigit{2}{\isacharparenright}\isanewline
-\isacommand{apply}\ simp\isanewline
-\isacommand{apply}{\isacharparenleft}drule\ seq{\isacharunderscore}lemma{\isacharparenright}\isanewline
-\isacommand{by}{\isacharparenleft}auto\ dest{\isacharcolon}not{\isacharunderscore}in{\isacharunderscore}lfp{\isacharunderscore}afD{\isacharparenright}\isanewline
-\isanewline
-\isanewline
-\isanewline
-\isanewline
-\isacommand{consts}\ Avoid\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ state\ set\ {\isasymRightarrow}\ state\ set{\isachardoublequote}\isanewline
-\isacommand{inductive}\ {\isachardoublequote}Avoid\ s\ A{\isachardoublequote}\isanewline
-\isakeyword{intros}\ {\isachardoublequote}s\ {\isasymin}\ Avoid\ s\ A{\isachardoublequote}\isanewline
-\ \ \ \ \ \ \ {\isachardoublequote}{\isasymlbrakk}\ t\ {\isasymin}\ Avoid\ s\ A{\isacharsemicolon}\ t\ {\isasymnotin}\ A{\isacharsemicolon}\ {\isacharparenleft}t{\isacharcomma}u{\isacharparenright}\ {\isasymin}\ M\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ u\ {\isasymin}\ Avoid\ s\ A{\isachardoublequote}\isanewline
-\isanewline
-\isanewline
-\isacommand{lemma}\ ex{\isacharunderscore}infinite{\isacharunderscore}path{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\isanewline
-{\isachardoublequote}t\ {\isasymin}\ Avoid\ s\ A\ \ {\isasymLongrightarrow}\isanewline
-\ {\isasymforall}f{\isachardot}\ t\ {\isacharequal}\ f\ \isadigit{0}\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}f\ i{\isacharcomma}\ f\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ f\ i\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ f\ i\ {\isasymnotin}\ A{\isacharparenright}\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}\ p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ A{\isacharparenright}{\isachardoublequote}\isanewline
-\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}Paths{\isacharunderscore}def{\isacharparenright}\isanewline
-\isacommand{apply}{\isacharparenleft}erule\ Avoid{\isachardot}induct{\isacharparenright}\isanewline
-\ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
-\isacommand{apply}{\isacharparenleft}rule\ allI{\isacharparenright}\isanewline
-\isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}{\isasymlambda}i{\isachardot}\ case\ i\ of\ \isadigit{0}\ {\isasymRightarrow}\ t\ {\isacharbar}\ Suc\ i\ {\isasymRightarrow}\ f\ i{\isachardoublequote}\ \isakeyword{in}\ allE{\isacharparenright}\isanewline
-\isacommand{by}{\isacharparenleft}force\ split{\isacharcolon}nat{\isachardot}split{\isacharparenright}\isanewline
-\isanewline
-\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}\isanewline
-\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}\ y\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ x\ {\isasymnotin}\ A{\isacharbraceright}{\isachardoublequote}{\isacharparenright}\isanewline
-\ \isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ a\ {\isacharequal}\ t\ \isakeyword{in}\ wf{\isacharunderscore}induct{\isacharparenright}\isanewline
-\ \isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}\isanewline
-\ \isacommand{apply}{\isacharparenleft}rule\ ssubst\ {\isacharbrackleft}OF\ lfp{\isacharunderscore}Tarski{\isacharbrackleft}OF\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharbrackright}{\isacharparenright}\isanewline
-\ \isacommand{apply}{\isacharparenleft}unfold\ af{\isacharunderscore}def{\isacharparenright}\isanewline
-\ \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}Avoid{\isachardot}intros{\isacharparenright}\isanewline
-\isacommand{apply}{\isacharparenleft}erule\ contrapos\isadigit{2}{\isacharparenright}\isanewline
-\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}wf{\isacharunderscore}iff{\isacharunderscore}no{\isacharunderscore}infinite{\isacharunderscore}down{\isacharunderscore}chain{\isacharparenright}\isanewline
-\isacommand{apply}{\isacharparenleft}erule\ exE{\isacharparenright}\isanewline
-\isacommand{apply}{\isacharparenleft}rule\ ex{\isacharunderscore}infinite{\isacharunderscore}path{\isacharparenright}\isanewline
-\isacommand{by}{\isacharparenleft}auto{\isacharparenright}\isanewline
-\isanewline
-\isacommand{theorem}\ AF{\isacharunderscore}subset{\isacharunderscore}lfp{\isacharcolon}\isanewline
-{\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
-\isacommand{apply}{\isacharparenleft}rule\ subsetI{\isacharparenright}\isanewline
-\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
-\isacommand{apply}{\isacharparenleft}erule\ Avoid{\isacharunderscore}in{\isacharunderscore}lfp{\isacharparenright}\isanewline
-\isacommand{by}{\isacharparenleft}rule\ Avoid{\isachardot}intros{\isacharparenright}\isanewline
-\isanewline
-\isanewline
+\isacommand{apply}\ simp%
+\begin{isamarkuptxt}%
+\begin{isabelle}
+\ \isadigit{1}{\isachardot}\ {\isasymAnd}s{\isachardot}\ s\ {\isasymnotin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymexists}p{\isasymin}Paths\ s{\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}%
+\isacommand{apply}{\isacharparenleft}drule\ infinity{\isacharunderscore}lemma{\isacharparenright}%
+\begin{isamarkuptxt}%
+\begin{isabelle}
+\ \isadigit{1}{\isachardot}\ {\isasymAnd}s{\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}s{\isachardot}\ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\isanewline
+\ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ A
+\end{isabelle}
+Both are solved automatically:%
+\end{isamarkuptxt}%
+\ \isacommand{apply}{\isacharparenleft}auto\ dest{\isacharcolon}not{\isacharunderscore}in{\isacharunderscore}lfp{\isacharunderscore}afD{\isacharparenright}\isanewline
+\isacommand{done}%
+\begin{isamarkuptext}%
+The main theorem is proved as for PDL, except that we also derive the necessary equality
+\isa{lfp{\isacharparenleft}af\ A{\isacharparenright}\ {\isacharequal}\ {\isachardot}{\isachardot}{\isachardot}} by combining \isa{AF{\isacharunderscore}lemma\isadigit{1}} and \isa{AF{\isacharunderscore}lemma\isadigit{2}}
+on the spot:%
+\end{isamarkuptext}%
 \isacommand{theorem}\ {\isachardoublequote}mc\ f\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ f{\isacharbraceright}{\isachardoublequote}\isanewline
 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ f{\isacharparenright}\isanewline
-\isacommand{by}{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ EF{\isacharunderscore}lemma\ equalityI{\isacharbrackleft}OF\ lfp{\isacharunderscore}subset{\isacharunderscore}AF\ AF{\isacharunderscore}subset{\isacharunderscore}lfp{\isacharbrackright}{\isacharparenright}\isanewline
+\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
+\isacommand{done}%
+\begin{isamarkuptext}%
+Let us close this section with a few words about the executability of \isa{mc}.
+It is clear that if all sets are finite, they can be represented as lists and the usual
+set operations are easily implemented. Only \isa{lfp} requires a little thought.
+Fortunately the HOL library proves that in the case of finite sets and a monotone \isa{F},
+\isa{lfp\ F} can be computed by iterated application of \isa{F} to \isa{{\isacharbraceleft}{\isacharbraceright}} until
+a fixpoint is reached. It is possible to generate executable functional programs
+from HOL definitions, but that is beyond the scope of the tutorial.%
+\end{isamarkuptext}%
 \end{isabellebody}%
 %%% Local Variables:
 %%% mode: latex

--- a/doc-src/TutorialI/CTL/document/PDL.tex	Fri Oct 06 01:21:17 2000 +0200
+++ b/doc-src/TutorialI/CTL/document/PDL.tex	Fri Oct 06 12:31:53 2000 +0200
@@ -73,7 +73,8 @@
 \end{isamarkuptext}%
 \isacommand{lemma}\ mono{\isacharunderscore}ef{\isacharcolon}\ {\isachardoublequote}mono{\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isacharcircum}{\isacharminus}\isadigit{1}\ {\isacharcircum}{\isacharcircum}\ T{\isacharparenright}{\isachardoublequote}\isanewline
 \isacommand{apply}{\isacharparenleft}rule\ monoI{\isacharparenright}\isanewline
-\isacommand{by}{\isacharparenleft}blast{\isacharparenright}%
+\isacommand{apply}\ blast\isanewline
+\isacommand{done}%
 \begin{isamarkuptext}%
 \noindent
 in order to make sure it really has a least fixpoint.
@@ -163,14 +164,16 @@
 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}Tarski{\isacharbrackleft}OF\ mono{\isacharunderscore}ef{\isacharbrackright}{\isacharbrackright}{\isacharparenright}\isanewline
-\isacommand{by}{\isacharparenleft}blast{\isacharparenright}%
+\isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
+\isacommand{done}%
 \begin{isamarkuptext}%
 The main theorem is proved in the familiar manner: induction followed by
 \isa{auto} augmented with the lemma as a simplification rule.%
 \end{isamarkuptext}%
 \isacommand{theorem}\ {\isachardoublequote}mc\ f\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ f{\isacharbraceright}{\isachardoublequote}\isanewline
 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ f{\isacharparenright}\isanewline
-\isacommand{by}{\isacharparenleft}auto\ simp\ add{\isacharcolon}EF{\isacharunderscore}lemma{\isacharparenright}\end{isabellebody}%
+\isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}EF{\isacharunderscore}lemma{\isacharparenright}\isanewline
+\isacommand{done}\end{isabellebody}%
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "root"