# HG changeset patch
# User nipkow
# Date 968946360 -7200
# Node ID 67f2920862c77739888149e4ca1f9c9b113797c8
# Parent  78822f2d921f2603773404098cd82bbd2a7c9434
*** empty log message ***

diff -r 78822f2d921f -r 67f2920862c7 doc-src/TutorialI/Advanced/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Advanced/ROOT.ML	Thu Sep 14 17:46:00 2000 +0200
@@ -0,0 +1,2 @@
+use "../settings.ML";
+use_thy "simp";
diff -r 78822f2d921f -r 67f2920862c7 doc-src/TutorialI/Advanced/advanced.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Advanced/advanced.tex	Thu Sep 14 17:46:00 2000 +0200
@@ -0,0 +1,26 @@
+\chapter{Advanced Simplification, Recursion, and Induction}
+\markboth{}{CHAPTER 4: ADVANCED}
+
+Although we have already learned a lot about simplification, recursion and
+induction, there are some advanced proof techniques that we have not covered
+yet and which are worth knowing about if you intend to beome a serious
+(human) theorem prover. The three sections of this chapter are almost
+independent of each other and can be read in any order. Only the notion of
+\emph{congruence rules}, introduced in the section on simplification, is
+required for parts of the section on recursion.
+
+\input{document/simp.tex}
+
+\section{Advanced forms of recursion}
+\label{sec:advanced-recdef}
+\index{*recdef|(}
+\input{../Recdef/document/Nested0.tex}
+\input{../Recdef/document/Nested1.tex}
+\input{../Recdef/document/Nested2.tex}
+\index{*recdef|)}
+
+\section{Advanced induction techniques}
+\label{sec:advanced-ind}
+\index{induction|(}
+\input{../Misc/document/AdvancedInd.tex}
+\index{induction|)}
diff -r 78822f2d921f -r 67f2920862c7 doc-src/TutorialI/Advanced/simp.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Advanced/simp.thy	Thu Sep 14 17:46:00 2000 +0200
@@ -0,0 +1,131 @@
+(*<*)
+theory simp = Main:
+(*>*)
+
+section{*Simplification*}
+
+text{*\label{sec:simplification-II}\index{simplification|(}
+This section discusses some additional nifty features not covered so far and
+gives a short introduction to the simplification process itself. The latter
+is helpful to understand why a particular rule does or does not apply in some
+situation.
+*}
+
+subsection{*Advanced features*}
+
+subsubsection{*Congruence rules*}
+
+text{*\label{sec:simp-cong}
+It is hardwired into the simplifier that while simplifying the conclusion $Q$
+of $P \isasymImp Q$ it is legal to make uses of the assumptions $P$. This
+kind of contextual information can also be made available for other
+operators. For example, @{prop"xs = [] --> xs@xs = xs"} simplifies to @{term
+True} because we may use @{prop"xs = []"} when simplifying @{prop"xs@xs =
+xs"}. The generation of contextual information during simplification is
+controlled by so-called \bfindex{congruence rules}. This is the one for
+@{text"\<longrightarrow>"}:
+@{thm[display]imp_cong[no_vars]}
+It should be read as follows:
+In order to simplify @{prop"P-->Q"} to @{prop"P'-->Q'"},
+simplify @{prop P} to @{prop P'}
+and assume @{prop"P'"} when simplifying @{prop Q} to @{prop"Q'"}.
+
+Here are some more examples.  The congruence rules for bounded
+quantifiers supply contextual information about the bound variable:
+@{thm[display,eta_contract=false,margin=60]ball_cong[no_vars]}
+The congruence rule for conditional expressions supply contextual
+information for simplifying the arms:
+@{thm[display]if_cong[no_vars]}
+A congruence rule can also \emph{prevent} simplification of some arguments.
+Here is an alternative congruence rule for conditional expressions:
+@{thm[display]if_weak_cong[no_vars]}
+Only the first argument is simplified; the others remain unchanged.
+This makes simplification much faster and is faithful to the evaluation
+strategy in programming languages, which is why this is the default
+congruence rule for @{text if}. Analogous rules control the evaluaton of
+@{text case} expressions.
+
+You can delare your own congruence rules with the attribute @{text cong},
+either globally, in the usual manner,
+\begin{quote}
+\isacommand{declare} \textit{theorem-name} @{text"[cong]"}
+\end{quote}
+or locally in a @{text"simp"} call by adding the modifier
+\begin{quote}
+@{text"cong:"} \textit{list of theorem names}
+\end{quote}
+The effect is reversed by @{text"cong del"} instead of @{text cong}.
+
+\begin{warn}
+The congruence rule @{thm[source]conj_cong}
+@{thm[display]conj_cong[no_vars]}
+is occasionally useful but not a default rule; you have to use it explicitly.
+\end{warn}
+*}
+
+subsubsection{*Permutative rewrite rules*}
+
+text{*
+\index{rewrite rule!permutative|bold}
+\index{rewriting!ordered|bold}
+\index{ordered rewriting|bold}
+\index{simplification!ordered|bold}
+An equation is a \bfindex{permutative rewrite rule} if the left-hand
+side and right-hand side are the same up to renaming of variables.  The most
+common permutative rule is commutativity: @{prop"x+y = y+x"}.  Other examples
+include @{prop"(x-y)-z = (x-z)-y"} in arithmetic and @{prop"insert x (insert
+y A) = insert y (insert x A)"} for sets. Such rules are problematic because
+once they apply, they can be used forever. The simplifier is aware of this
+danger and treats permutative rules by means of a special strategy, called
+\bfindex{ordered rewriting}: a permutative rewrite
+rule is only applied if the term becomes ``smaller'' (w.r.t.\ some fixed
+lexicographic ordering on terms). For example, commutativity rewrites
+@{term"b+a"} to @{term"a+b"}, but then stops because @{term"a+b"} is strictly
+smaller than @{term"b+a"}.  Permutative rewrite rules can be turned into
+simplification rules in the usual manner via the @{text simp} attribute; the
+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
+following points in mind:
+\begin{itemize}\index{associative-commutative operators}
+  
+\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
+  used with commutativity, can lead to nontermination.
+
+\item To complete your set of rewrite rules, you must add not just
+  associativity~(A) and commutativity~(C) but also a derived rule, {\bf
+    left-com\-mut\-ativ\-ity} (LC): $f(x,f(y,z)) = f(y,f(x,z))$.
+\end{itemize}
+Ordered rewriting with the combination of A, C, and LC sorts a term
+lexicographically:
+\[\def\maps#1{~\stackrel{#1}{\leadsto}~}
+ f(f(b,c),a) \maps{A} f(b,f(c,a)) \maps{C} f(b,f(a,c)) \maps{LC} f(a,f(b,c)) \]
+
+Note that ordered rewriting for @{text"+"} and @{text"*"} on numbers is rarely
+necessary because the builtin arithmetic capabilities often take care of
+this.
+*}
+
+subsection{*How it works*}
+
+text{*\label{sec:SimpHow}
+Roughly speaking, the simplifier proceeds bottom-up (subterms are simplified
+first) and a conditional equation is only applied if its condition could be
+proved (again by simplification). Below we explain some special 
+*}
+
+subsubsection{*Higher-order patterns*}
+
+subsubsection{*Local assumptions*}
+
+subsubsection{*The preprocessor*}
+
+text{*
+\index{simplification|)}
+*}
+(*<*)
+end
+(*>*)
diff -r 78822f2d921f -r 67f2920862c7 doc-src/TutorialI/CTL/CTL.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/CTL/CTL.thy	Thu Sep 14 17:46:00 2000 +0200
@@ -0,0 +1,234 @@
+theory CTL = Main:
+
+typedecl atom;
+types state = "atom set";
+
+datatype ctl_form = Atom atom
+                  | NOT ctl_form
+                  | And ctl_form ctl_form
+                  | AX ctl_form
+                  | EF ctl_form
+                  | AF ctl_form;
+
+consts valid :: "state \<Rightarrow> ctl_form \<Rightarrow> bool" ("(_ \<Turnstile> _)" [80,80] 80)
+       M :: "(state \<times> state)set";
+
+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)}";
+
+primrec
+"s \<Turnstile> Atom a  =  (a\<in>s)"
+"s \<Turnstile> NOT f   = (~(s \<Turnstile> f))"
+"s \<Turnstile> And f g = (s \<Turnstile> f \<and> s \<Turnstile> g)"
+"s \<Turnstile> AX f    = (\<forall>t. (s,t) \<in> M \<longrightarrow> t \<Turnstile> f)"
+"s \<Turnstile> EF f    = (\<exists>t. (s,t) \<in> M^* \<and> t \<Turnstile> f)"
+"s \<Turnstile> AF f    = (\<forall>p \<in> Paths s. \<exists>i. p i \<Turnstile> f)";
+
+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}";
+
+lemma mono_af: "mono(af A)";
+by(force simp add: af_def intro:monoI);
+
+consts mc :: "ctl_form \<Rightarrow> state set";
+primrec
+"mc(Atom a)  = {s. a\<in>s}"
+"mc(NOT f)   = -mc f"
+"mc(And f g) = mc f \<inter> mc g"
+"mc(AX f)    = {s. \<forall>t. (s,t) \<in> M  \<longrightarrow> t \<in> mc f}"
+"mc(EF f)    = lfp(\<lambda>T. mc f \<union> {s. \<exists>t. (s,t)\<in>M \<and> t\<in>T})"
+"mc(AF f)    = lfp(af(mc f))";
+
+lemma mono_ef: "mono(\<lambda>T. A \<union> {s. \<exists>t. (s,t)\<in>M \<and> t\<in>T})";
+apply(rule monoI);
+by(blast);
+
+lemma lfp_conv_EF:
+"lfp(\<lambda>T. A \<union> {s. \<exists>t. (s,t)\<in>M \<and> t\<in>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(blast intro: r_into_rtrancl rtrancl_trans);
+apply(rule subsetI);
+apply(simp);
+apply(erule exE);
+apply(erule conjE);
+apply(erule_tac P = "t\<in>A" in rev_mp);
+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);
+
+theorem lfp_subset_AF:
+"lfp(af A) \<subseteq> {s. \<forall> p \<in> Paths s. \<exists> i. p i \<in> A}";
+apply(rule subsetI);
+apply(erule Lfp.induct[OF _ mono_af]);
+apply(simp add: af_def Paths_def);
+apply(erule disjE);
+ apply(blast);
+apply(clarify);
+apply(erule_tac x = "p 1" in allE);
+apply(clarsimp);
+apply(erule_tac x = "\<lambda>i. p(i+1)" in allE);
+apply(simp);
+by(blast);
+
+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
+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
+@{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
+@{term A}-avoiding path. Let us formalize this sketch.
+
+The one-step argument in the above sketch
+*};
+
+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 swap);
+apply(rule ssubst[OF lfp_Tarski[OF mono_af]]);
+by(simp add:af_def);
+
+text{*\noindent
+is proved by a variant of contraposition (@{thm[source]swap}:
+@{thm swap[no_vars]}), i.e.\ assuming the negation of the conclusion
+and proving @{term"s : lfp(af A)"}. Unfolding @{term lfp} once and
+simplifying with the definition of @{term af} finishes the proof.
+
+Now we iterate this process. The following construction of the desired
+path is parameterized by a predicate @{term P} that should hold along the path:
+*};
+
+consts path :: "state \<Rightarrow> (state \<Rightarrow> bool) \<Rightarrow> (nat \<Rightarrow> state)";
+primrec
+"path s P 0 = s"
+"path s P (Suc n) = (SOME t. (path s P n,t) \<in> M \<and> P t)";
+
+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
+concern to us since we will only use @{term path} in such cases where a
+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.
+*};
+
+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)";
+
+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:
+*};
+
+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
+*};
+
+ apply(simp add:Paths_def, blast);
+apply(rule_tac x = "path s P" in exI);
+apply(simp);
+apply(intro strip);
+apply(induct_tac i);
+ apply(simp);
+ apply(fast intro:selectI2EX);
+apply(simp);
+apply(rule selectI2EX);
+ apply(blast);
+apply(rule selectI2EX);
+ apply(blast);
+by(blast);
+
+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)";
+apply(subgoal_tac
+ "\<exists> p. s = p 0 \<and> (\<forall> i. (p i,p(Suc i))\<in>M \<and> P(p i))");
+ apply(simp add:Paths_def);
+ apply(blast);
+apply(rule_tac x = "nat_rec s (\<lambda>n t. SOME u. (t,u)\<in>M \<and> P u)" in exI);
+apply(simp);
+apply(intro strip);
+apply(induct_tac i);
+ apply(simp);
+ apply(fast intro:selectI2EX);
+apply(simp);
+apply(rule selectI2EX);
+ apply(blast);
+apply(rule selectI2EX);
+ apply(blast);
+by(blast);
+
+theorem AF_subset_lfp:
+"{s. \<forall> p \<in> Paths s. \<exists> i. p i \<in> A} \<subseteq> lfp(af A)";
+apply(rule subsetI);
+apply(erule contrapos2);
+apply simp;
+apply(drule seq_lemma);
+by(auto dest:not_in_lfp_afD);
+
+
+(*
+Second proof of opposite direction, directly by wellfounded induction
+on the initial segment of M that avoids A.
+
+Avoid s A = the set of successors of s that can be reached by a finite A-avoiding path
+*)
+
+consts Avoid :: "state \<Rightarrow> state set \<Rightarrow> state set";
+inductive "Avoid s A"
+intros "s \<in> Avoid s A"
+       "\<lbrakk> t \<in> Avoid s A; t \<notin> A; (t,u) \<in> M \<rbrakk> \<Longrightarrow> u \<in> Avoid s A";
+
+(* For any infinite A-avoiding path (f) in Avoid s A,
+   there is some infinite A-avoiding path (p) in Avoid s A that starts with s.
+*)
+lemma ex_infinite_path[rule_format]:
+"t \<in> Avoid s A  \<Longrightarrow>
+ \<forall>f. t = f 0 \<longrightarrow> (\<forall>i. (f i, f (Suc i)) \<in> M \<and> f i \<in> Avoid s A \<and> f i \<notin> A)
+                \<longrightarrow> (\<exists> p\<in>Paths s. \<forall>i. p i \<notin> A)";
+apply(simp add:Paths_def);
+apply(erule Avoid.induct);
+ apply(blast);
+apply(rule allI);
+apply(erule_tac x = "\<lambda>i. case i of 0 \<Rightarrow> t | Suc i \<Rightarrow> f i" in allE);
+by(force split:nat.split);
+
+lemma Avoid_in_lfp[rule_format(no_asm)]:
+"\<forall>p\<in>Paths s. \<exists>i. p i \<in> A \<Longrightarrow> t \<in> Avoid s A \<longrightarrow> t \<in> lfp(af A)";
+apply(subgoal_tac "wf{(y,x). (x,y)\<in>M \<and> x \<in> Avoid s A \<and> y \<in> Avoid s A \<and> x \<notin> A}");
+ apply(erule_tac a = t in wf_induct);
+ apply(clarsimp);
+ apply(rule ssubst [OF lfp_Tarski[OF mono_af]]);
+ apply(unfold af_def);
+ apply(blast intro:Avoid.intros);
+apply(erule contrapos2);
+apply(simp add:wf_iff_no_infinite_down_chain);
+apply(erule exE);
+apply(rule ex_infinite_path);
+by(auto);
+
+theorem AF_subset_lfp:
+"{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: lfp_conv_EF equalityI[OF lfp_subset_AF AF_subset_lfp]);
+
+end;
diff -r 78822f2d921f -r 67f2920862c7 doc-src/TutorialI/CTL/PDL.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/CTL/PDL.thy	Thu Sep 14 17:46:00 2000 +0200
@@ -0,0 +1,58 @@
+theory PDL = Main:;
+
+typedecl atom;
+types state = "atom set";
+
+datatype ctl_form = Atom atom
+                  | NOT ctl_form
+                  | And ctl_form ctl_form
+                  | AX ctl_form
+                  | EF ctl_form;
+
+consts valid :: "state \<Rightarrow> ctl_form \<Rightarrow> bool" ("(_ \<Turnstile> _)" [80,80] 80)
+       M :: "(state \<times> state)set";
+
+primrec
+"s \<Turnstile> Atom a  = (a\<in>s)"
+"s \<Turnstile> NOT f   = (\<not>(s \<Turnstile> f))"
+"s \<Turnstile> And f g = (s \<Turnstile> f \<and> s \<Turnstile> g)"
+"s \<Turnstile> AX f    = (\<forall>t. (s,t) \<in> M \<longrightarrow> t \<Turnstile> f)"
+"s \<Turnstile> EF f    = (\<exists>t. (s,t) \<in> M^* \<and> t \<Turnstile> f)";
+
+consts mc :: "ctl_form \<Rightarrow> state set";
+primrec
+"mc(Atom a)  = {s. a\<in>s}"
+"mc(NOT f)   = -mc f"
+"mc(And f g) = mc f Int mc g"
+"mc(AX f)    = {s. \<forall>t. (s,t) \<in> M  \<longrightarrow> t \<in> mc f}"
+"mc(EF f)    = lfp(\<lambda>T. mc f \<union> {s. \<exists>t. (s,t)\<in>M \<and> t\<in>T})";
+
+lemma mono_lemma: "mono(\<lambda>T. A \<union> {s. \<exists>t. (s,t)\<in>M \<and> t\<in>T})";
+apply(rule monoI);
+by(blast);
+
+lemma lfp_conv_EF:
+"lfp(\<lambda>T. A \<union> {s. \<exists>t. (s,t)\<in>M \<and> t\<in>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_lemma);
+ apply(simp);
+ apply(blast intro: r_into_rtrancl rtrancl_trans);
+apply(rule subsetI);
+apply(simp);
+apply(erule exE);
+apply(erule conjE);
+apply(erule_tac P = "t\<in>A" in rev_mp);
+apply(erule converse_rtrancl_induct);
+ apply(rule ssubst[OF lfp_Tarski[OF mono_lemma]]);
+ apply(blast);
+apply(rule ssubst[OF lfp_Tarski[OF mono_lemma]]);
+by(blast);
+
+theorem "mc f = {s. s \<Turnstile> f}";
+apply(induct_tac f);
+by(auto simp add:lfp_conv_EF);
+
+end;
diff -r 78822f2d921f -r 67f2920862c7 doc-src/TutorialI/CTL/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/CTL/ROOT.ML	Thu Sep 14 17:46:00 2000 +0200
@@ -0,0 +1,3 @@
+use "../settings.ML";
+use_thy "PDL";
+use_thy "CTL";
diff -r 78822f2d921f -r 67f2920862c7 doc-src/TutorialI/IsaMakefile
--- a/doc-src/TutorialI/IsaMakefile	Thu Sep 14 17:46:00 2000 +0200
+++ b/doc-src/TutorialI/IsaMakefile	Thu Sep 14 17:46:00 2000 +0200
@@ -4,7 +4,7 @@
 
 ## targets
 
-default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Recdef HOL-Advanced HOL-Misc styles
+default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Recdef HOL-Advanced HOL-CTL HOL-Misc styles
 images:
 test:
 all: default
@@ -101,6 +101,14 @@
 	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Advanced
 	@rm -f tutorial.dvi
 
+## HOL-CTL
+
+HOL-CTL: HOL $(LOG)/HOL-CTL.gz
+
+$(LOG)/HOL-CTL.gz: $(OUT)/HOL CTL/PDL.thy CTL/CTL.thy CTL/ROOT.ML
+	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL CTL
+	@rm -f tutorial.dvi
+
 ## HOL-Misc
 
 HOL-Misc: HOL $(LOG)/HOL-Misc.gz
@@ -117,4 +125,4 @@
 ## clean
 
 clean:
-	@rm -f tutorial.dvi $(LOG)/HOL-Ifexpr.gz $(LOG)/HOL-CodeGen.gz $(LOG)/HOL-Misc.gz $(LOG)/HOL-ToyList.gz $(LOG)/HOL-ToyList2.gz $(LOG)/HOL-Trie.gz $(LOG)/HOL-Datatype.gz $(LOG)/HOL-Recdef.gz $(LOG)/HOL-Advanced.gz 
+	@rm -f tutorial.dvi $(LOG)/HOL-Ifexpr.gz $(LOG)/HOL-CodeGen.gz $(LOG)/HOL-Misc.gz $(LOG)/HOL-ToyList.gz $(LOG)/HOL-ToyList2.gz $(LOG)/HOL-Trie.gz $(LOG)/HOL-Datatype.gz $(LOG)/HOL-Recdef.gz $(LOG)/HOL-Advanced.gz $(LOG)/HOL-CTL.gz 
diff -r 78822f2d921f -r 67f2920862c7 doc-src/TutorialI/Misc/document/AdvancedInd.tex
--- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Thu Sep 14 17:46:00 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Thu Sep 14 17:46:00 2000 +0200
@@ -86,16 +86,16 @@
 \begin{isamarkuptext}%
 \noindent
 or the wholesale stripping of \isa{{\isasymforall}} and
-\isa{{\isasymlongrightarrow}} in the conclusion via \isa{rulified}%
+\isa{{\isasymlongrightarrow}} in the conclusion via \isa{rule{\isacharunderscore}format}%
 \end{isamarkuptext}%
-\isacommand{lemmas}\ myrule\ {\isacharequal}\ simple{\isacharbrackleft}rulified{\isacharbrackright}%
+\isacommand{lemmas}\ myrule\ {\isacharequal}\ simple{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}%
 \begin{isamarkuptext}%
 \noindent
 yielding \isa{{\isasymlbrakk}A\ y{\isacharsemicolon}\ B\ y{\isasymrbrakk}\ {\isasymLongrightarrow}\ B\ y\ {\isasymand}\ A\ y}.
 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}rulified{\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\ {\isacharampersand}\ A\ y{\isachardoublequote}%
 \begin{isamarkuptext}%
 \bigskip
 
@@ -185,13 +185,13 @@
 
 We can now derive the desired \isa{i\ {\isasymle}\ f\ i} from \isa{f{\isacharunderscore}incr}:%
 \end{isamarkuptext}%
-\isacommand{lemmas}\ f{\isacharunderscore}incr\ {\isacharequal}\ f{\isacharunderscore}incr{\isacharunderscore}lem{\isacharbrackleft}rulified{\isacharcomma}\ OF\ refl{\isacharbrackright}%
+\isacommand{lemmas}\ f{\isacharunderscore}incr\ {\isacharequal}\ f{\isacharunderscore}incr{\isacharunderscore}lem{\isacharbrackleft}rule{\isacharunderscore}format{\isacharcomma}\ OF\ refl{\isacharbrackright}%
 \begin{isamarkuptext}%
 \noindent
 The final \isa{refl} gets rid of the premise \isa{{\isacharquery}k\ {\isacharequal}\ f\ {\isacharquery}i}. Again,
 we could have included this derivation in the original statement of the lemma:%
 \end{isamarkuptext}%
-\isacommand{lemma}\ f{\isacharunderscore}incr{\isacharbrackleft}rulified{\isacharcomma}\ OF\ refl{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i{\isachardot}\ k\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isachardoublequote}%
+\isacommand{lemma}\ f{\isacharunderscore}incr{\isacharbrackleft}rule{\isacharunderscore}format{\isacharcomma}\ OF\ refl{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i{\isachardot}\ k\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isachardoublequote}%
 \begin{isamarkuptext}%
 \begin{exercise}
 From the above axiom and lemma for \isa{f} show that \isa{f} is the
diff -r 78822f2d921f -r 67f2920862c7 doc-src/TutorialI/tricks.tex
--- a/doc-src/TutorialI/tricks.tex	Thu Sep 14 17:46:00 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,27 +0,0 @@
-%\chapter{The Tricks of the Trade}
-\chapter{Advanced Simplification, Recursion, and Induction}
-\markboth{}{CHAPTER 4: ADVANCED}
-
-Although we have already learned a lot about simplification, recursion and
-induction, there are some advanced proof techniques that we have not covered
-yet and which are worth knowing about if you intend to beome a serious
-(human) theorem prover. The three sections of this chapter are almost
-independent of each other and can be read in any order. Only the notion of
-\emph{congruence rules}, introduced in the section on simplification, is
-required for parts of the section on recursion.
-
-\input{Advanced/document/simp.tex}
-
-\section{Advanced forms of recursion}
-\label{sec:advanced-recdef}
-\index{*recdef|(}
-\input{Recdef/document/Nested0.tex}
-\input{Recdef/document/Nested1.tex}
-\input{Recdef/document/Nested2.tex}
-\index{*recdef|)}
-
-\section{Advanced induction techniques}
-\label{sec:advanced-ind}
-\index{induction|(}
-\input{Misc/document/AdvancedInd.tex}
-\index{induction|)}
diff -r 78822f2d921f -r 67f2920862c7 doc-src/TutorialI/tutorial.tex
--- a/doc-src/TutorialI/tutorial.tex	Thu Sep 14 17:46:00 2000 +0200
+++ b/doc-src/TutorialI/tutorial.tex	Thu Sep 14 17:46:00 2000 +0200
@@ -65,7 +65,8 @@
 
 \input{basics}
 \input{fp}
-\input{tricks}
+\input{Advanced/advanced}
+%\chapter{The Tricks of the Trade}
 \input{appendix}
 
 \bibliographystyle{plain}