*** empty log message ***

--- a/doc-src/TutorialI/Advanced/document/simp.tex	Thu Oct 19 21:25:15 2000 +0200
+++ b/doc-src/TutorialI/Advanced/document/simp.tex	Fri Oct 20 08:46:41 2000 +0200
@@ -97,10 +97,10 @@
 simplifier recognizes their special status automatically.
 
 Permutative rewrite rules are most effective in the case of
-associative-commutative operators.  (Associativity by itself is not
-permutative.)  When dealing with an AC-operator~$f$, keep the
+associative-commutative functions.  (Associativity by itself is not
+permutative.)  When dealing with an AC-function~$f$, keep the
 following points in mind:
-\begin{itemize}\index{associative-commutative operators}
+\begin{itemize}\index{associative-commutative function}
   
 \item The associative law must always be oriented from left to right,
   namely $f(f(x,y),z) = f(x,f(y,z))$.  The opposite orientation, if

--- a/doc-src/TutorialI/Advanced/simp.thy	Thu Oct 19 21:25:15 2000 +0200
+++ b/doc-src/TutorialI/Advanced/simp.thy	Fri Oct 20 08:46:41 2000 +0200
@@ -86,10 +86,10 @@
 simplifier recognizes their special status automatically.
 
 Permutative rewrite rules are most effective in the case of
-associative-commutative operators.  (Associativity by itself is not
-permutative.)  When dealing with an AC-operator~$f$, keep the
+associative-commutative functions.  (Associativity by itself is not
+permutative.)  When dealing with an AC-function~$f$, keep the
 following points in mind:
-\begin{itemize}\index{associative-commutative operators}
+\begin{itemize}\index{associative-commutative function}
   
 \item The associative law must always be oriented from left to right,
   namely $f(f(x,y),z) = f(x,f(y,z))$.  The opposite orientation, if

--- a/doc-src/TutorialI/CTL/Base.thy	Thu Oct 19 21:25:15 2000 +0200
+++ b/doc-src/TutorialI/CTL/Base.thy	Fri Oct 20 08:46:41 2000 +0200
@@ -1,6 +1,6 @@
 (*<*)theory Base = Main:(*>*)
 
-section{*Case study: Verified model checkers*}
+section{*Case study: Verified model checking*}
 
 text{*
 Model checking is a very popular technique for the verification of finite
@@ -50,18 +50,20 @@
 which is false.
 
 Abstracting from this concrete example, we assume there is some type of
-states
+states:
 *}
 
 typedecl state
 
 text{*\noindent
-which we merely declare rather than define because it is an implicit
-parameter of our model.  Of course it would have been more generic to make
-@{typ state} a type parameter of everything but fixing @{typ state} as above
-reduces clutter.
-Similarly we declare an arbitrary but fixed transition system, i.e.\
-relation between states:
+Command \isacommand{typedecl} merely declares a new type but without
+defining it (see also \S\ref{sec:typedecl}). Thus we know nothing
+about the type other than its existence. That is exactly what we need
+because @{typ state} really is an implicit parameter of our model.  Of
+course it would have been more generic to make @{typ state} a type
+parameter of everything but declaring @{typ state} globally as above
+reduces clutter.  Similarly we declare an arbitrary but fixed
+transition system, i.e.\ relation between states:
 *}
 
 consts M :: "(state \<times> state)set";

--- a/doc-src/TutorialI/CTL/CTL.thy	Thu Oct 19 21:25:15 2000 +0200
+++ b/doc-src/TutorialI/CTL/CTL.thy	Fri Oct 20 08:46:41 2000 +0200
@@ -87,7 +87,7 @@
  apply(erule lfp_induct);
   apply(rule mono_ef);
  apply(simp);
- apply(blast intro: r_into_rtrancl rtrancl_trans);
+ apply(blast intro: rtrancl_trans);
 apply(rule subsetI);
 apply(simp, clarify);
 apply(erule converse_rtrancl_induct);
@@ -112,10 +112,9 @@
 @{thm[source]lfp_lowerbound}:
 @{thm[display]lfp_lowerbound[of _ "S",no_vars]}
 The instance of the premise @{prop"f S \<subseteq> S"} is proved pointwise,
-starting with simplification and clarification:
+a decision that clarification takes for us:
 *};
 apply(rule lfp_lowerbound);
-apply(rule subsetI);
 apply(clarsimp simp add: af_def Paths_def);
 (*ML"Pretty.setmargin 70";
 pr(latex xsymbols symbols);*)
@@ -380,24 +379,116 @@
 done
 
 text{*
+
 The above language is not quite CTL. The latter also includes an
-until-operator, which is the subject of the following exercise.
-It is not definable in terms of the other operators!
+until-operator @{term"EU f g"} with semantics ``there exist a path
+where @{term f} is true until @{term g} becomes true''. With the help
+of an auxiliary function
+*}
+
+consts until:: "state set \<Rightarrow> state set \<Rightarrow> state \<Rightarrow> state list \<Rightarrow> bool"
+primrec
+"until A B s []    = (s \<in> B)"
+"until A B s (t#p) = (s \<in> A \<and> (s,t) \<in> M \<and> until A B t p)"
+(*<*)constdefs
+ eusem :: "state set \<Rightarrow> state set \<Rightarrow> state set"
+"eusem A B \<equiv> {s. \<exists>p. until A B s p}"(*>*)
+
+text{*\noindent
+the semantics of @{term EU} is straightforward:
+@{text[display]"s \<Turnstile> EU f g = (\<exists>p. until A B s p)"}
+Note that @{term EU} is not definable in terms of the other operators!
+
+Model checking @{term EU} is again a least fixed point construction:
+@{text[display]"mc(EU f g) = lfp(\<lambda>T. mc g \<union> mc f \<inter> (M^-1 ^^ T))"}
+
 \begin{exercise}
-Extend the datatype of formulae by the binary until operator @{term"EU f g"} with semantics
-``there exist a path where @{term f} is true until @{term g} becomes true''
-@{text[display]"s \<Turnstile> EU f g = (\<exists>p\<in>Paths s. \<exists>j. p j \<Turnstile> g \<and> (\<exists>i < j. p i \<Turnstile> f))"}
-and model checking algorithm
-@{text[display]"mc(EU f g) = lfp(\<lambda>T. mc g \<union> mc f \<inter> (M^-1 ^^ T))"}
-Prove the equivalence between semantics and model checking, i.e.\ that
+Extend the datatype of formulae by the above until operator
+and prove the equivalence between semantics and model checking, i.e.\ that
 @{prop[display]"mc(EU f g) = {s. s \<Turnstile> EU f g}"}
 %For readability you may want to annotate {term EU} with its customary syntax
 %{text[display]"| EU formula formula    E[_ U _]"}
 %which enables you to read and write {text"E[f U g]"} instead of {term"EU f g"}.
 \end{exercise}
-For more CTL exercises see, for example \cite{Huth-Ryan-book}.
-\bigskip
+For more CTL exercises see, for example, \cite{Huth-Ryan-book}.
+*}
+
+(*<*)
+constdefs
+ eufix :: "state set \<Rightarrow> state set \<Rightarrow> state set \<Rightarrow> state set"
+"eufix A B T \<equiv> B \<union> A \<inter> (M^-1 ^^ T)"
+
+lemma "lfp(eufix A B) \<subseteq> eusem A B"
+apply(rule lfp_lowerbound)
+apply(clarsimp simp add:eusem_def eufix_def);
+apply(erule disjE);
+ apply(rule_tac x = "[]" in exI);
+ apply simp
+apply(clarsimp);
+apply(rule_tac x = "y#xc" in exI);
+apply simp;
+done
+
+lemma mono_eufix: "mono(eufix A B)";
+apply(simp add: mono_def eufix_def);
+apply blast;
+done
+
+lemma "eusem A B \<subseteq> lfp(eufix A B)";
+apply(clarsimp simp add:eusem_def);
+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(simp add:eufix_def);
+apply(clarsimp);
+apply(rule ssubst[OF lfp_unfold[OF mono_eufix]]);
+apply(simp add:eufix_def);
+apply blast;
+done
 
+(*
+constdefs
+ eusem :: "state set \<Rightarrow> state set \<Rightarrow> state set"
+"eusem A B \<equiv> {s. \<exists>p\<in>Paths s. \<exists>j. p j \<in> B \<and> (\<forall>i < j. p i \<in> A)}"
+
+axioms
+M_total: "\<exists>t. (s,t) \<in> M"
+
+consts apath :: "state \<Rightarrow> (nat \<Rightarrow> state)"
+primrec
+"apath s 0 = s"
+"apath s (Suc i) = (SOME t. (apath s i,t) \<in> M)"
+
+lemma [iff]: "apath s \<in> Paths s";
+apply(simp add:Paths_def);
+apply(blast intro: M_total[THEN someI_ex])
+done
+
+constdefs
+ pcons :: "state \<Rightarrow> (nat \<Rightarrow> state) \<Rightarrow> (nat \<Rightarrow> state)"
+"pcons s p == \<lambda>i. case i of 0 \<Rightarrow> s | Suc j \<Rightarrow> p j"
+
+lemma pcons_PathI: "[| (s,t) : M; p \<in> Paths t |] ==> pcons s p \<in> Paths s";
+by(simp add:Paths_def pcons_def split:nat.split);
+
+lemma "lfp(eufix A B) \<subseteq> eusem A B"
+apply(rule lfp_lowerbound)
+apply(clarsimp simp add:eusem_def eufix_def);
+apply(erule disjE);
+ apply(rule_tac x = "apath x" in bexI);
+  apply(rule_tac x = 0 in exI);
+  apply simp;
+ apply simp;
+apply(clarify);
+apply(rule_tac x = "pcons xb p" in bexI);
+ apply(rule_tac x = "j+1" in exI);
+ apply (simp add:pcons_def split:nat.split);
+apply (simp add:pcons_PathI)
+done
+*)
+(*>*)
+text{*
 Let us close this section with a few words about the executability of our model checkers.
 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.

--- a/doc-src/TutorialI/CTL/CTLind.thy	Thu Oct 19 21:25:15 2000 +0200
+++ b/doc-src/TutorialI/CTL/CTLind.thy	Fri Oct 20 08:46:41 2000 +0200
@@ -3,12 +3,15 @@
 subsection{*CTL revisited*}
 
 text{*\label{sec:CTL-revisited}
+The purpose of this section is twofold: we want to demonstrate
+some of the induction principles and heuristics discussed above and we want to
+show how inductive definitions can simplify proofs.
 In \S\ref{sec:CTL} we gave a fairly involved proof of the correctness of a
 model checker for CTL. In particular the proof of the
 @{thm[source]infinity_lemma} on the way to @{thm[source]AF_lemma2} is not as
 simple as one might intuitively expect, due to the @{text SOME} operator
-involved. The purpose of this section is to show how an inductive definition
-can help to simplify the proof of @{thm[source]AF_lemma2}.
+involved. Below we give a simpler proof of @{thm[source]AF_lemma2}
+based on an auxiliary inductive definition.
 
 Let us call a (finite or infinite) path \emph{@{term A}-avoiding} if it does
 not touch any node in the set @{term A}. Then @{thm[source]AF_lemma2} says

--- a/doc-src/TutorialI/CTL/document/Base.tex	Thu Oct 19 21:25:15 2000 +0200
+++ b/doc-src/TutorialI/CTL/document/Base.tex	Fri Oct 20 08:46:41 2000 +0200
@@ -2,7 +2,7 @@
 \begin{isabellebody}%
 \def\isabellecontext{Base}%
 %
-\isamarkupsection{Case study: Verified model checkers}
+\isamarkupsection{Case study: Verified model checking}
 %
 \begin{isamarkuptext}%
 Model checking is a very popular technique for the verification of finite
@@ -52,17 +52,19 @@
 which is false.
 
 Abstracting from this concrete example, we assume there is some type of
-states%
+states:%
 \end{isamarkuptext}%
 \isacommand{typedecl}\ state%
 \begin{isamarkuptext}%
 \noindent
-which we merely declare rather than define because it is an implicit
-parameter of our model.  Of course it would have been more generic to make
-\isa{state} a type parameter of everything but fixing \isa{state} as above
-reduces clutter.
-Similarly we declare an arbitrary but fixed transition system, i.e.\
-relation between states:%
+Command \isacommand{typedecl} merely declares a new type but without
+defining it (see also \S\ref{sec:typedecl}). Thus we know nothing
+about the type other than its existence. That is exactly what we need
+because \isa{state} really is an implicit parameter of our model.  Of
+course it would have been more generic to make \isa{state} a type
+parameter of everything but declaring \isa{state} globally as above
+reduces clutter.  Similarly we declare an arbitrary but fixed
+transition system, i.e.\ relation between states:%
 \end{isamarkuptext}%
 \isacommand{consts}\ M\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}state\ {\isasymtimes}\ state{\isacharparenright}set{\isachardoublequote}%
 \begin{isamarkuptext}%

--- a/doc-src/TutorialI/CTL/document/CTL.tex	Thu Oct 19 21:25:15 2000 +0200
+++ b/doc-src/TutorialI/CTL/document/CTL.tex	Fri Oct 20 08:46:41 2000 +0200
@@ -66,10 +66,9 @@
 \ \ \ \ \ f\ S\ {\isasymsubseteq}\ S\ {\isasymLongrightarrow}\ lfp\ f\ {\isasymsubseteq}\ S%
 \end{isabelle}
 The instance of the premise \isa{f\ S\ {\isasymsubseteq}\ S} is proved pointwise,
-starting with simplification and clarification:%
+a decision that clarification takes for us:%
 \end{isamarkuptxt}%
 \isacommand{apply}{\isacharparenleft}rule\ lfp{\isacharunderscore}lowerbound{\isacharparenright}\isanewline
-\isacommand{apply}{\isacharparenleft}rule\ subsetI{\isacharparenright}\isanewline
 \isacommand{apply}{\isacharparenleft}clarsimp\ simp\ add{\isacharcolon}\ af{\isacharunderscore}def\ Paths{\isacharunderscore}def{\isacharparenright}%
 \begin{isamarkuptxt}%
 \begin{isabelle}
@@ -282,19 +281,30 @@
 \isacommand{done}%
 \begin{isamarkuptext}%
 The above language is not quite CTL. The latter also includes an
-until-operator, which is the subject of the following exercise.
-It is not definable in terms of the other operators!
-\begin{exercise}
-Extend the datatype of formulae by the binary until operator \isa{EU\ f\ g} with semantics
-``there exist a path where \isa{f} is true until \isa{g} becomes true''
+until-operator \isa{EU\ f\ g} with semantics ``there exist a path
+where \isa{f} is true until \isa{g} becomes true''. With the help
+of an auxiliary function%
+\end{isamarkuptext}%
+\isacommand{consts}\ until{\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ set\ {\isasymRightarrow}\ state\ set\ {\isasymRightarrow}\ state\ {\isasymRightarrow}\ state\ list\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline
+\isacommand{primrec}\isanewline
+{\isachardoublequote}until\ A\ B\ s\ {\isacharbrackleft}{\isacharbrackright}\ \ \ \ {\isacharequal}\ {\isacharparenleft}s\ {\isasymin}\ B{\isacharparenright}{\isachardoublequote}\isanewline
+{\isachardoublequote}until\ A\ B\ s\ {\isacharparenleft}t{\isacharhash}p{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}s\ {\isasymin}\ A\ {\isasymand}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ until\ A\ B\ t\ p{\isacharparenright}{\isachardoublequote}%
+\begin{isamarkuptext}%
+\noindent
+the semantics of \isa{EU} is straightforward:
 \begin{isabelle}%
-\ \ \ \ \ s\ {\isasymTurnstile}\ EU\ f\ g\ {\isacharequal}\ {\isacharparenleft}{\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}j{\isachardot}\ p\ j\ {\isasymTurnstile}\ g\ {\isasymand}\ {\isacharparenleft}{\isasymexists}i\ {\isacharless}\ j{\isachardot}\ p\ i\ {\isasymTurnstile}\ f{\isacharparenright}{\isacharparenright}%
+\ \ \ \ \ s\ {\isasymTurnstile}\ EU\ f\ g\ {\isacharequal}\ {\isacharparenleft}{\isasymexists}p{\isachardot}\ until\ A\ B\ s\ p{\isacharparenright}%
 \end{isabelle}
-and model checking algorithm
+Note that \isa{EU} is not definable in terms of the other operators!
+
+Model checking \isa{EU} is again a least fixed point construction:
 \begin{isabelle}%
 \ \ \ \ \ mc{\isacharparenleft}EU\ f\ g{\isacharparenright}\ {\isacharequal}\ lfp{\isacharparenleft}{\isasymlambda}T{\isachardot}\ mc\ g\ {\isasymunion}\ mc\ f\ {\isasyminter}\ {\isacharparenleft}M{\isacharcircum}{\isacharminus}{\isadigit{1}}\ {\isacharcircum}{\isacharcircum}\ T{\isacharparenright}{\isacharparenright}%
 \end{isabelle}
-Prove the equivalence between semantics and model checking, i.e.\ that
+
+\begin{exercise}
+Extend the datatype of formulae by the above until operator
+and prove the equivalence between semantics and model checking, i.e.\ that
 \begin{isabelle}%
 \ \ \ \ \ mc\ {\isacharparenleft}EU\ f\ g{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ EU\ f\ g{\isacharbraceright}%
 \end{isabelle}
@@ -302,9 +312,10 @@
 %{text[display]"| EU formula formula    E[_ U _]"}
 %which enables you to read and write {text"E[f U g]"} instead of {term"EU f g"}.
 \end{exercise}
-For more CTL exercises see, for example \cite{Huth-Ryan-book}.
-\bigskip
-
+For more CTL exercises see, for example, \cite{Huth-Ryan-book}.%
+\end{isamarkuptext}%
+%
+\begin{isamarkuptext}%
 Let us close this section with a few words about the executability of our model checkers.
 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.

--- a/doc-src/TutorialI/Misc/AdvancedInd.thy	Thu Oct 19 21:25:15 2000 +0200
+++ b/doc-src/TutorialI/Misc/AdvancedInd.thy	Fri Oct 20 08:46:41 2000 +0200
@@ -6,7 +6,8 @@
 Now that we have learned about rules and logic, we take another look at the
 finer points of induction. The two questions we answer are: what to do if the
 proposition to be proved is not directly amenable to induction, and how to
-utilize and even derive new induction schemas.
+utilize and even derive new induction schemas. We conclude with some slightly subtle
+examples of induction.
 *};
 
 subsection{*Massaging the proposition*};
@@ -82,7 +83,7 @@
 Here is a simple example (which is proved by @{text"blast"}):
 *};
 
-lemma simple: "\<forall>y. A y \<longrightarrow> B y \<longrightarrow> B y & A y";
+lemma simple: "\<forall>y. A y \<longrightarrow> B y \<longrightarrow> B y \<and> A y";
 (*<*)by blast;(*>*)
 
 text{*\noindent
@@ -105,7 +106,7 @@
 statement of your original lemma, thus avoiding the intermediate step:
 *};
 
-lemma myrule[rule_format]:  "\<forall>y. A y \<longrightarrow> B y \<longrightarrow> B y & A y";
+lemma myrule[rule_format]:  "\<forall>y. A y \<longrightarrow> B y \<longrightarrow> B y \<and> A y";
 (*<*)
 by blast;
 (*>*)
@@ -129,6 +130,9 @@
 replace it with $(x@1,\dots,x@k) \in R$, and rephrase the conclusion $C$ as
 \[ \forall y@1 \dots y@n.~ (x@1,\dots,x@k) = t \longrightarrow C \]
 For an example see \S\ref{sec:CTL-revisited} below.
+
+Of course, all premises that share free variables with $t$ need to be pulled into
+the conclusion as well, under the @{text"\<forall>"}, again using @{text"\<longrightarrow>"} as shown above.
 *};
 
 subsection{*Beyond structural and recursion induction*};
@@ -149,7 +153,7 @@
 Here is an example of its application.
 *};
 
-consts f :: "nat => nat";
+consts f :: "nat \<Rightarrow> nat";
 axioms f_ax: "f(f(n)) < f(Suc(n))";
 
 text{*\noindent
@@ -289,7 +293,6 @@
 by(insert induct_lem, blast);
 
 text{*
-
 Finally we should mention that HOL already provides the mother of all
 inductions, \textbf{well-founded
 induction}\indexbold{induction!well-founded}\index{well-founded

--- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Thu Oct 19 21:25:15 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Fri Oct 20 08:46:41 2000 +0200
@@ -7,7 +7,8 @@
 Now that we have learned about rules and logic, we take another look at the
 finer points of induction. The two questions we answer are: what to do if the
 proposition to be proved is not directly amenable to induction, and how to
-utilize and even derive new induction schemas.%
+utilize and even derive new induction schemas. We conclude with some slightly subtle
+examples of induction.%
 \end{isamarkuptext}%
 %
 \isamarkupsubsection{Massaging the proposition}
@@ -77,7 +78,7 @@
 which can yield a fairly complex conclusion.
 Here is a simple example (which is proved by \isa{blast}):%
 \end{isamarkuptext}%
-\isacommand{lemma}\ simple{\isacharcolon}\ {\isachardoublequote}{\isasymforall}y{\isachardot}\ A\ y\ {\isasymlongrightarrow}\ B\ y\ {\isasymlongrightarrow}\ B\ y\ {\isacharampersand}\ A\ y{\isachardoublequote}%
+\isacommand{lemma}\ simple{\isacharcolon}\ {\isachardoublequote}{\isasymforall}y{\isachardot}\ A\ y\ {\isasymlongrightarrow}\ B\ y\ {\isasymlongrightarrow}\ B\ y\ {\isasymand}\ A\ y{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent
 You can get the desired lemma by explicit
@@ -96,7 +97,7 @@
 You can go one step further and include these derivations already in the
 statement of your original lemma, thus avoiding the intermediate step:%
 \end{isamarkuptext}%
-\isacommand{lemma}\ myrule{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\ \ {\isachardoublequote}{\isasymforall}y{\isachardot}\ A\ y\ {\isasymlongrightarrow}\ B\ y\ {\isasymlongrightarrow}\ B\ y\ {\isacharampersand}\ A\ y{\isachardoublequote}%
+\isacommand{lemma}\ myrule{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\ \ {\isachardoublequote}{\isasymforall}y{\isachardot}\ A\ y\ {\isasymlongrightarrow}\ B\ y\ {\isasymlongrightarrow}\ B\ y\ {\isasymand}\ A\ y{\isachardoublequote}%
 \begin{isamarkuptext}%
 \bigskip
 
@@ -115,7 +116,10 @@
 a premise $t \in R$, where $t$ is not just an $n$-tuple of variables, we
 replace it with $(x@1,\dots,x@k) \in R$, and rephrase the conclusion $C$ as
 \[ \forall y@1 \dots y@n.~ (x@1,\dots,x@k) = t \longrightarrow C \]
-For an example see \S\ref{sec:CTL-revisited} below.%
+For an example see \S\ref{sec:CTL-revisited} below.
+
+Of course, all premises that share free variables with $t$ need to be pulled into
+the conclusion as well, under the \isa{{\isasymforall}}, again using \isa{{\isasymlongrightarrow}} as shown above.%
 \end{isamarkuptext}%
 %
 \isamarkupsubsection{Beyond structural and recursion induction}
@@ -138,7 +142,7 @@
 \end{isabelle}
 Here is an example of its application.%
 \end{isamarkuptext}%
-\isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isacharequal}{\isachargreater}\ nat{\isachardoublequote}\isanewline
+\isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
 \isacommand{axioms}\ f{\isacharunderscore}ax{\isacharcolon}\ {\isachardoublequote}f{\isacharparenleft}f{\isacharparenleft}n{\isacharparenright}{\isacharparenright}\ {\isacharless}\ f{\isacharparenleft}Suc{\isacharparenleft}n{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent

--- a/doc-src/TutorialI/todo.tobias	Thu Oct 19 21:25:15 2000 +0200
+++ b/doc-src/TutorialI/todo.tobias	Fri Oct 20 08:46:41 2000 +0200
@@ -1,27 +1,21 @@
-General questions
-=================
-
-Here is an initial list:
-clarify, clarsimp, hyp_subst_tac, rename_tac, rotate_tac, split
-single step tactics: (e/d/f)rule, insert
-with instantiation: (e/d/f)rule_tac, insert_tac
+Implementation
+==============
 
 Hide global names like Node.
 Why is comp needed in addition to op O?
 Explain in syntax section!
 
-Implementation
-==============
+defs with = and pattern matching
 
-swap in classical.ML has ugly name Pa in it. Rename.
+replace "simp only split" by "split_tac".
 
-Induction rules for int: int_le/ge_induct?
-Needed for ifak example. But is that example worth it?
+arithmetic: allow mixed nat/int formulae
+-> simplify proof of part1 in Inductive/AB.thy
 
 Add map_cong?? (upto 10% slower)
-But we should install UN_cong and INT_cong too.
 
-defs with = and pattern matching
+Recdef: Get rid of function name in header.
+Support mutual recursion (Konrad?)
 
 use arith_tac in recdef to solve termination conditions?
 -> new example in Recdef/termination
@@ -34,15 +28,18 @@
 
 it would be nice if one could get id to the enclosing quotes in the [source] option.
 
-arithmetic: allow mixed nat/int formulae
--> simplify proof of part1 in Inductive/AB.thy
+More predefined functions for datatypes: map?
+
+Induction rules for int: int_le/ge_induct?
+Needed for ifak example. But is that example worth it?
+
 
 Minor fixes in the tutorial
 ===========================
 
-replace simp only split by split_tac.
+explanation of absence of contrapos_pn in Rules?
 
-get rid of use_thy?
+get rid of use_thy in tutorial?
 
 Explain typographic conventions?
 
@@ -62,27 +59,19 @@
 
 Syntax section: syntax annotations nor just for consts but also for constdefs and datatype.
 
-Prove EU exercise in CTL.
-
 
 Minor additions to the tutorial, unclear where
 ==============================================
 
 Tacticals: , ? +
 
-"typedecl" is used in CTL/Base, but where is it introduced?
-In More Types chapter? Rephrase the CTL bit accordingly.
-
-print_simpset (-> print_simps?)
-(Another subsection Useful theorems, methods, and commands?)
-
 Mention that simp etc (big step tactics) insist on change?
 
 Rules: Introduce "by" (as a kind of shorthand for apply+done, except that it
 does more.)
 
 A list of further useful commands (rules? tricks?)
-prefer, defer
+prefer, defer, print_simpset (-> print_simps?)
 
 An overview of the automatic methods: simp, auto, fast, blast, force,
 clarify, clarsimp (intro, elim?)
@@ -134,12 +123,8 @@
 
 Sets via ordered list of intervals. (Isa/Interval(2))
 
-Sets: PDL and CTL
-
-Ind. defs: Grammar (for same number of as and bs),
 propositional logic (soundness and completeness?),
 predicate logic (soundness?),
-CTL proof.
 
 Tautology checker. Based on Ifexpr or prop.logic?
 Include forward reference in relevant section.
@@ -159,33 +144,18 @@
 Additional topics
 =================
 
-Beef up recdef (see below).
-Nested recursion? Mutual recursion?
-
-Nested inductive datatypes: better recursion and induction
-(see below)
+Recdef with nested recursion?
 
 Extensionality: applications in
 - boolean expressions: valif o bool2if = value
 - Advanced datatypes exercise subst (f o g) = subst f o subst g
 
 A look at the library?
-Functions. Relations. Lfp/Gfp. Map.
+Map.
 If WF is discussed, make a link to it from AdvancedInd.
 
 Prototyping?
 
-
-Isabelle
-========
-
-Get rid of function name in recdef header
-
-More predefined functions for datatypes: map?
-
-1 and 2 on nat?
-
-
 ==============================================================
 Recdef: