*** empty log message ***
authornipkow
Thu Sep 14 17:46:00 2000 +0200 (2000-09-14)
changeset 995867f2920862c7
parent 9957 78822f2d921f
child 9959 4a2ae974043d
*** empty log message ***
doc-src/TutorialI/Advanced/ROOT.ML
doc-src/TutorialI/Advanced/advanced.tex
doc-src/TutorialI/Advanced/simp.thy
doc-src/TutorialI/CTL/CTL.thy
doc-src/TutorialI/CTL/PDL.thy
doc-src/TutorialI/CTL/ROOT.ML
doc-src/TutorialI/IsaMakefile
doc-src/TutorialI/Misc/document/AdvancedInd.tex
doc-src/TutorialI/tricks.tex
doc-src/TutorialI/tutorial.tex
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/TutorialI/Advanced/ROOT.ML	Thu Sep 14 17:46:00 2000 +0200
     1.3 @@ -0,0 +1,2 @@
     1.4 +use "../settings.ML";
     1.5 +use_thy "simp";
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/doc-src/TutorialI/Advanced/advanced.tex	Thu Sep 14 17:46:00 2000 +0200
     2.3 @@ -0,0 +1,26 @@
     2.4 +\chapter{Advanced Simplification, Recursion, and Induction}
     2.5 +\markboth{}{CHAPTER 4: ADVANCED}
     2.6 +
     2.7 +Although we have already learned a lot about simplification, recursion and
     2.8 +induction, there are some advanced proof techniques that we have not covered
     2.9 +yet and which are worth knowing about if you intend to beome a serious
    2.10 +(human) theorem prover. The three sections of this chapter are almost
    2.11 +independent of each other and can be read in any order. Only the notion of
    2.12 +\emph{congruence rules}, introduced in the section on simplification, is
    2.13 +required for parts of the section on recursion.
    2.14 +
    2.15 +\input{document/simp.tex}
    2.16 +
    2.17 +\section{Advanced forms of recursion}
    2.18 +\label{sec:advanced-recdef}
    2.19 +\index{*recdef|(}
    2.20 +\input{../Recdef/document/Nested0.tex}
    2.21 +\input{../Recdef/document/Nested1.tex}
    2.22 +\input{../Recdef/document/Nested2.tex}
    2.23 +\index{*recdef|)}
    2.24 +
    2.25 +\section{Advanced induction techniques}
    2.26 +\label{sec:advanced-ind}
    2.27 +\index{induction|(}
    2.28 +\input{../Misc/document/AdvancedInd.tex}
    2.29 +\index{induction|)}
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/doc-src/TutorialI/Advanced/simp.thy	Thu Sep 14 17:46:00 2000 +0200
     3.3 @@ -0,0 +1,131 @@
     3.4 +(*<*)
     3.5 +theory simp = Main:
     3.6 +(*>*)
     3.7 +
     3.8 +section{*Simplification*}
     3.9 +
    3.10 +text{*\label{sec:simplification-II}\index{simplification|(}
    3.11 +This section discusses some additional nifty features not covered so far and
    3.12 +gives a short introduction to the simplification process itself. The latter
    3.13 +is helpful to understand why a particular rule does or does not apply in some
    3.14 +situation.
    3.15 +*}
    3.16 +
    3.17 +subsection{*Advanced features*}
    3.18 +
    3.19 +subsubsection{*Congruence rules*}
    3.20 +
    3.21 +text{*\label{sec:simp-cong}
    3.22 +It is hardwired into the simplifier that while simplifying the conclusion $Q$
    3.23 +of $P \isasymImp Q$ it is legal to make uses of the assumptions $P$. This
    3.24 +kind of contextual information can also be made available for other
    3.25 +operators. For example, @{prop"xs = [] --> xs@xs = xs"} simplifies to @{term
    3.26 +True} because we may use @{prop"xs = []"} when simplifying @{prop"xs@xs =
    3.27 +xs"}. The generation of contextual information during simplification is
    3.28 +controlled by so-called \bfindex{congruence rules}. This is the one for
    3.29 +@{text"\<longrightarrow>"}:
    3.30 +@{thm[display]imp_cong[no_vars]}
    3.31 +It should be read as follows:
    3.32 +In order to simplify @{prop"P-->Q"} to @{prop"P'-->Q'"},
    3.33 +simplify @{prop P} to @{prop P'}
    3.34 +and assume @{prop"P'"} when simplifying @{prop Q} to @{prop"Q'"}.
    3.35 +
    3.36 +Here are some more examples.  The congruence rules for bounded
    3.37 +quantifiers supply contextual information about the bound variable:
    3.38 +@{thm[display,eta_contract=false,margin=60]ball_cong[no_vars]}
    3.39 +The congruence rule for conditional expressions supply contextual
    3.40 +information for simplifying the arms:
    3.41 +@{thm[display]if_cong[no_vars]}
    3.42 +A congruence rule can also \emph{prevent} simplification of some arguments.
    3.43 +Here is an alternative congruence rule for conditional expressions:
    3.44 +@{thm[display]if_weak_cong[no_vars]}
    3.45 +Only the first argument is simplified; the others remain unchanged.
    3.46 +This makes simplification much faster and is faithful to the evaluation
    3.47 +strategy in programming languages, which is why this is the default
    3.48 +congruence rule for @{text if}. Analogous rules control the evaluaton of
    3.49 +@{text case} expressions.
    3.50 +
    3.51 +You can delare your own congruence rules with the attribute @{text cong},
    3.52 +either globally, in the usual manner,
    3.53 +\begin{quote}
    3.54 +\isacommand{declare} \textit{theorem-name} @{text"[cong]"}
    3.55 +\end{quote}
    3.56 +or locally in a @{text"simp"} call by adding the modifier
    3.57 +\begin{quote}
    3.58 +@{text"cong:"} \textit{list of theorem names}
    3.59 +\end{quote}
    3.60 +The effect is reversed by @{text"cong del"} instead of @{text cong}.
    3.61 +
    3.62 +\begin{warn}
    3.63 +The congruence rule @{thm[source]conj_cong}
    3.64 +@{thm[display]conj_cong[no_vars]}
    3.65 +is occasionally useful but not a default rule; you have to use it explicitly.
    3.66 +\end{warn}
    3.67 +*}
    3.68 +
    3.69 +subsubsection{*Permutative rewrite rules*}
    3.70 +
    3.71 +text{*
    3.72 +\index{rewrite rule!permutative|bold}
    3.73 +\index{rewriting!ordered|bold}
    3.74 +\index{ordered rewriting|bold}
    3.75 +\index{simplification!ordered|bold}
    3.76 +An equation is a \bfindex{permutative rewrite rule} if the left-hand
    3.77 +side and right-hand side are the same up to renaming of variables.  The most
    3.78 +common permutative rule is commutativity: @{prop"x+y = y+x"}.  Other examples
    3.79 +include @{prop"(x-y)-z = (x-z)-y"} in arithmetic and @{prop"insert x (insert
    3.80 +y A) = insert y (insert x A)"} for sets. Such rules are problematic because
    3.81 +once they apply, they can be used forever. The simplifier is aware of this
    3.82 +danger and treats permutative rules by means of a special strategy, called
    3.83 +\bfindex{ordered rewriting}: a permutative rewrite
    3.84 +rule is only applied if the term becomes ``smaller'' (w.r.t.\ some fixed
    3.85 +lexicographic ordering on terms). For example, commutativity rewrites
    3.86 +@{term"b+a"} to @{term"a+b"}, but then stops because @{term"a+b"} is strictly
    3.87 +smaller than @{term"b+a"}.  Permutative rewrite rules can be turned into
    3.88 +simplification rules in the usual manner via the @{text simp} attribute; the
    3.89 +simplifier recognizes their special status automatically.
    3.90 +
    3.91 +Permutative rewrite rules are most effective in the case of
    3.92 +associative-commutative operators.  (Associativity by itself is not
    3.93 +permutative.)  When dealing with an AC-operator~$f$, keep the
    3.94 +following points in mind:
    3.95 +\begin{itemize}\index{associative-commutative operators}
    3.96 +  
    3.97 +\item The associative law must always be oriented from left to right,
    3.98 +  namely $f(f(x,y),z) = f(x,f(y,z))$.  The opposite orientation, if
    3.99 +  used with commutativity, can lead to nontermination.
   3.100 +
   3.101 +\item To complete your set of rewrite rules, you must add not just
   3.102 +  associativity~(A) and commutativity~(C) but also a derived rule, {\bf
   3.103 +    left-com\-mut\-ativ\-ity} (LC): $f(x,f(y,z)) = f(y,f(x,z))$.
   3.104 +\end{itemize}
   3.105 +Ordered rewriting with the combination of A, C, and LC sorts a term
   3.106 +lexicographically:
   3.107 +\[\def\maps#1{~\stackrel{#1}{\leadsto}~}
   3.108 + 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)) \]
   3.109 +
   3.110 +Note that ordered rewriting for @{text"+"} and @{text"*"} on numbers is rarely
   3.111 +necessary because the builtin arithmetic capabilities often take care of
   3.112 +this.
   3.113 +*}
   3.114 +
   3.115 +subsection{*How it works*}
   3.116 +
   3.117 +text{*\label{sec:SimpHow}
   3.118 +Roughly speaking, the simplifier proceeds bottom-up (subterms are simplified
   3.119 +first) and a conditional equation is only applied if its condition could be
   3.120 +proved (again by simplification). Below we explain some special 
   3.121 +*}
   3.122 +
   3.123 +subsubsection{*Higher-order patterns*}
   3.124 +
   3.125 +subsubsection{*Local assumptions*}
   3.126 +
   3.127 +subsubsection{*The preprocessor*}
   3.128 +
   3.129 +text{*
   3.130 +\index{simplification|)}
   3.131 +*}
   3.132 +(*<*)
   3.133 +end
   3.134 +(*>*)
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/doc-src/TutorialI/CTL/CTL.thy	Thu Sep 14 17:46:00 2000 +0200
     4.3 @@ -0,0 +1,234 @@
     4.4 +theory CTL = Main:
     4.5 +
     4.6 +typedecl atom;
     4.7 +types state = "atom set";
     4.8 +
     4.9 +datatype ctl_form = Atom atom
    4.10 +                  | NOT ctl_form
    4.11 +                  | And ctl_form ctl_form
    4.12 +                  | AX ctl_form
    4.13 +                  | EF ctl_form
    4.14 +                  | AF ctl_form;
    4.15 +
    4.16 +consts valid :: "state \<Rightarrow> ctl_form \<Rightarrow> bool" ("(_ \<Turnstile> _)" [80,80] 80)
    4.17 +       M :: "(state \<times> state)set";
    4.18 +
    4.19 +constdefs Paths :: "state \<Rightarrow> (nat \<Rightarrow> state)set"
    4.20 +"Paths s \<equiv> {p. s = p 0 \<and> (\<forall>i. (p i, p(i+1)) \<in> M)}";
    4.21 +
    4.22 +primrec
    4.23 +"s \<Turnstile> Atom a  =  (a\<in>s)"
    4.24 +"s \<Turnstile> NOT f   = (~(s \<Turnstile> f))"
    4.25 +"s \<Turnstile> And f g = (s \<Turnstile> f \<and> s \<Turnstile> g)"
    4.26 +"s \<Turnstile> AX f    = (\<forall>t. (s,t) \<in> M \<longrightarrow> t \<Turnstile> f)"
    4.27 +"s \<Turnstile> EF f    = (\<exists>t. (s,t) \<in> M^* \<and> t \<Turnstile> f)"
    4.28 +"s \<Turnstile> AF f    = (\<forall>p \<in> Paths s. \<exists>i. p i \<Turnstile> f)";
    4.29 +
    4.30 +constdefs af :: "state set \<Rightarrow> state set \<Rightarrow> state set"
    4.31 +"af A T \<equiv> A \<union> {s. \<forall>t. (s, t) \<in> M \<longrightarrow> t \<in> T}";
    4.32 +
    4.33 +lemma mono_af: "mono(af A)";
    4.34 +by(force simp add: af_def intro:monoI);
    4.35 +
    4.36 +consts mc :: "ctl_form \<Rightarrow> state set";
    4.37 +primrec
    4.38 +"mc(Atom a)  = {s. a\<in>s}"
    4.39 +"mc(NOT f)   = -mc f"
    4.40 +"mc(And f g) = mc f \<inter> mc g"
    4.41 +"mc(AX f)    = {s. \<forall>t. (s,t) \<in> M  \<longrightarrow> t \<in> mc f}"
    4.42 +"mc(EF f)    = lfp(\<lambda>T. mc f \<union> {s. \<exists>t. (s,t)\<in>M \<and> t\<in>T})"
    4.43 +"mc(AF f)    = lfp(af(mc f))";
    4.44 +
    4.45 +lemma mono_ef: "mono(\<lambda>T. A \<union> {s. \<exists>t. (s,t)\<in>M \<and> t\<in>T})";
    4.46 +apply(rule monoI);
    4.47 +by(blast);
    4.48 +
    4.49 +lemma lfp_conv_EF:
    4.50 +"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}";
    4.51 +apply(rule equalityI);
    4.52 + apply(rule subsetI);
    4.53 + apply(simp);
    4.54 + apply(erule Lfp.induct);
    4.55 +  apply(rule mono_ef);
    4.56 + apply(simp);
    4.57 + apply(blast intro: r_into_rtrancl rtrancl_trans);
    4.58 +apply(rule subsetI);
    4.59 +apply(simp);
    4.60 +apply(erule exE);
    4.61 +apply(erule conjE);
    4.62 +apply(erule_tac P = "t\<in>A" in rev_mp);
    4.63 +apply(erule converse_rtrancl_induct);
    4.64 + apply(rule ssubst [OF lfp_Tarski[OF mono_ef]]);
    4.65 + apply(blast);
    4.66 +apply(rule ssubst [OF lfp_Tarski[OF mono_ef]]);
    4.67 +by(blast);
    4.68 +
    4.69 +theorem lfp_subset_AF:
    4.70 +"lfp(af A) \<subseteq> {s. \<forall> p \<in> Paths s. \<exists> i. p i \<in> A}";
    4.71 +apply(rule subsetI);
    4.72 +apply(erule Lfp.induct[OF _ mono_af]);
    4.73 +apply(simp add: af_def Paths_def);
    4.74 +apply(erule disjE);
    4.75 + apply(blast);
    4.76 +apply(clarify);
    4.77 +apply(erule_tac x = "p 1" in allE);
    4.78 +apply(clarsimp);
    4.79 +apply(erule_tac x = "\<lambda>i. p(i+1)" in allE);
    4.80 +apply(simp);
    4.81 +by(blast);
    4.82 +
    4.83 +text{*
    4.84 +The opposite direction is proved by contradiction: if some state
    4.85 +{term s} is not in @{term"lfp(af A)"}, then we can construct an
    4.86 +infinite @{term A}-avoiding path starting from @{term s}. The reason is
    4.87 +that by unfolding @{term"lfp"} we find that if @{term s} is not in
    4.88 +@{term"lfp(af A)"}, then @{term s} is not in @{term A} and there is a
    4.89 +direct successor of @{term s} that is again not in @{term"lfp(af
    4.90 +A)"}. Iterating this argument yields the promised infinite
    4.91 +@{term A}-avoiding path. Let us formalize this sketch.
    4.92 +
    4.93 +The one-step argument in the above sketch
    4.94 +*};
    4.95 +
    4.96 +lemma not_in_lfp_afD:
    4.97 + "s \<notin> lfp(af A) \<Longrightarrow> s \<notin> A \<and> (\<exists> t. (s,t)\<in>M \<and> t \<notin> lfp(af A))";
    4.98 +apply(erule swap);
    4.99 +apply(rule ssubst[OF lfp_Tarski[OF mono_af]]);
   4.100 +by(simp add:af_def);
   4.101 +
   4.102 +text{*\noindent
   4.103 +is proved by a variant of contraposition (@{thm[source]swap}:
   4.104 +@{thm swap[no_vars]}), i.e.\ assuming the negation of the conclusion
   4.105 +and proving @{term"s : lfp(af A)"}. Unfolding @{term lfp} once and
   4.106 +simplifying with the definition of @{term af} finishes the proof.
   4.107 +
   4.108 +Now we iterate this process. The following construction of the desired
   4.109 +path is parameterized by a predicate @{term P} that should hold along the path:
   4.110 +*};
   4.111 +
   4.112 +consts path :: "state \<Rightarrow> (state \<Rightarrow> bool) \<Rightarrow> (nat \<Rightarrow> state)";
   4.113 +primrec
   4.114 +"path s P 0 = s"
   4.115 +"path s P (Suc n) = (SOME t. (path s P n,t) \<in> M \<and> P t)";
   4.116 +
   4.117 +text{*\noindent
   4.118 +Element @{term"n+1"} on this path is some arbitrary successor
   4.119 +@{term"t"} of element @{term"n"} such that @{term"P t"} holds.  Of
   4.120 +course, such a @{term"t"} may in general not exist, but that is of no
   4.121 +concern to us since we will only use @{term path} in such cases where a
   4.122 +suitable @{term"t"} does exist.
   4.123 +
   4.124 +Now we prove that if each state @{term"s"} that satisfies @{term"P"}
   4.125 +has a successor that again satisfies @{term"P"}, then there exists an infinite @{term"P"}-path.
   4.126 +*};
   4.127 +
   4.128 +lemma seq_lemma:
   4.129 +"\<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)";
   4.130 +
   4.131 +txt{*\noindent
   4.132 +First we rephrase the conclusion slightly because we need to prove both the path property
   4.133 +and the fact that @{term"P"} holds simultaneously:
   4.134 +*};
   4.135 +
   4.136 +apply(subgoal_tac "\<exists> p. s = p 0 \<and> (\<forall> i. (p i,p(i+1)) \<in> M \<and> P(p i))");
   4.137 +
   4.138 +txt{*\noindent
   4.139 +From this proposition the original goal follows easily
   4.140 +*};
   4.141 +
   4.142 + apply(simp add:Paths_def, blast);
   4.143 +apply(rule_tac x = "path s P" in exI);
   4.144 +apply(simp);
   4.145 +apply(intro strip);
   4.146 +apply(induct_tac i);
   4.147 + apply(simp);
   4.148 + apply(fast intro:selectI2EX);
   4.149 +apply(simp);
   4.150 +apply(rule selectI2EX);
   4.151 + apply(blast);
   4.152 +apply(rule selectI2EX);
   4.153 + apply(blast);
   4.154 +by(blast);
   4.155 +
   4.156 +lemma seq_lemma:
   4.157 +"\<lbrakk> P s; \<forall> s. P s \<longrightarrow> (\<exists> t. (s,t)\<in>M \<and> P t) \<rbrakk> \<Longrightarrow>
   4.158 + \<exists> p\<in>Paths s. \<forall> i. P(p i)";
   4.159 +apply(subgoal_tac
   4.160 + "\<exists> p. s = p 0 \<and> (\<forall> i. (p i,p(Suc i))\<in>M \<and> P(p i))");
   4.161 + apply(simp add:Paths_def);
   4.162 + apply(blast);
   4.163 +apply(rule_tac x = "nat_rec s (\<lambda>n t. SOME u. (t,u)\<in>M \<and> P u)" in exI);
   4.164 +apply(simp);
   4.165 +apply(intro strip);
   4.166 +apply(induct_tac i);
   4.167 + apply(simp);
   4.168 + apply(fast intro:selectI2EX);
   4.169 +apply(simp);
   4.170 +apply(rule selectI2EX);
   4.171 + apply(blast);
   4.172 +apply(rule selectI2EX);
   4.173 + apply(blast);
   4.174 +by(blast);
   4.175 +
   4.176 +theorem AF_subset_lfp:
   4.177 +"{s. \<forall> p \<in> Paths s. \<exists> i. p i \<in> A} \<subseteq> lfp(af A)";
   4.178 +apply(rule subsetI);
   4.179 +apply(erule contrapos2);
   4.180 +apply simp;
   4.181 +apply(drule seq_lemma);
   4.182 +by(auto dest:not_in_lfp_afD);
   4.183 +
   4.184 +
   4.185 +(*
   4.186 +Second proof of opposite direction, directly by wellfounded induction
   4.187 +on the initial segment of M that avoids A.
   4.188 +
   4.189 +Avoid s A = the set of successors of s that can be reached by a finite A-avoiding path
   4.190 +*)
   4.191 +
   4.192 +consts Avoid :: "state \<Rightarrow> state set \<Rightarrow> state set";
   4.193 +inductive "Avoid s A"
   4.194 +intros "s \<in> Avoid s A"
   4.195 +       "\<lbrakk> t \<in> Avoid s A; t \<notin> A; (t,u) \<in> M \<rbrakk> \<Longrightarrow> u \<in> Avoid s A";
   4.196 +
   4.197 +(* For any infinite A-avoiding path (f) in Avoid s A,
   4.198 +   there is some infinite A-avoiding path (p) in Avoid s A that starts with s.
   4.199 +*)
   4.200 +lemma ex_infinite_path[rule_format]:
   4.201 +"t \<in> Avoid s A  \<Longrightarrow>
   4.202 + \<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)
   4.203 +                \<longrightarrow> (\<exists> p\<in>Paths s. \<forall>i. p i \<notin> A)";
   4.204 +apply(simp add:Paths_def);
   4.205 +apply(erule Avoid.induct);
   4.206 + apply(blast);
   4.207 +apply(rule allI);
   4.208 +apply(erule_tac x = "\<lambda>i. case i of 0 \<Rightarrow> t | Suc i \<Rightarrow> f i" in allE);
   4.209 +by(force split:nat.split);
   4.210 +
   4.211 +lemma Avoid_in_lfp[rule_format(no_asm)]:
   4.212 +"\<forall>p\<in>Paths s. \<exists>i. p i \<in> A \<Longrightarrow> t \<in> Avoid s A \<longrightarrow> t \<in> lfp(af A)";
   4.213 +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}");
   4.214 + apply(erule_tac a = t in wf_induct);
   4.215 + apply(clarsimp);
   4.216 + apply(rule ssubst [OF lfp_Tarski[OF mono_af]]);
   4.217 + apply(unfold af_def);
   4.218 + apply(blast intro:Avoid.intros);
   4.219 +apply(erule contrapos2);
   4.220 +apply(simp add:wf_iff_no_infinite_down_chain);
   4.221 +apply(erule exE);
   4.222 +apply(rule ex_infinite_path);
   4.223 +by(auto);
   4.224 +
   4.225 +theorem AF_subset_lfp:
   4.226 +"{s. \<forall>p \<in> Paths s. \<exists> i. p i \<in> A} \<subseteq> lfp(af A)";
   4.227 +apply(rule subsetI);
   4.228 +apply(simp);
   4.229 +apply(erule Avoid_in_lfp);
   4.230 +by(rule Avoid.intros);
   4.231 +
   4.232 +
   4.233 +theorem "mc f = {s. s \<Turnstile> f}";
   4.234 +apply(induct_tac f);
   4.235 +by(auto simp add: lfp_conv_EF equalityI[OF lfp_subset_AF AF_subset_lfp]);
   4.236 +
   4.237 +end;
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/doc-src/TutorialI/CTL/PDL.thy	Thu Sep 14 17:46:00 2000 +0200
     5.3 @@ -0,0 +1,58 @@
     5.4 +theory PDL = Main:;
     5.5 +
     5.6 +typedecl atom;
     5.7 +types state = "atom set";
     5.8 +
     5.9 +datatype ctl_form = Atom atom
    5.10 +                  | NOT ctl_form
    5.11 +                  | And ctl_form ctl_form
    5.12 +                  | AX ctl_form
    5.13 +                  | EF ctl_form;
    5.14 +
    5.15 +consts valid :: "state \<Rightarrow> ctl_form \<Rightarrow> bool" ("(_ \<Turnstile> _)" [80,80] 80)
    5.16 +       M :: "(state \<times> state)set";
    5.17 +
    5.18 +primrec
    5.19 +"s \<Turnstile> Atom a  = (a\<in>s)"
    5.20 +"s \<Turnstile> NOT f   = (\<not>(s \<Turnstile> f))"
    5.21 +"s \<Turnstile> And f g = (s \<Turnstile> f \<and> s \<Turnstile> g)"
    5.22 +"s \<Turnstile> AX f    = (\<forall>t. (s,t) \<in> M \<longrightarrow> t \<Turnstile> f)"
    5.23 +"s \<Turnstile> EF f    = (\<exists>t. (s,t) \<in> M^* \<and> t \<Turnstile> f)";
    5.24 +
    5.25 +consts mc :: "ctl_form \<Rightarrow> state set";
    5.26 +primrec
    5.27 +"mc(Atom a)  = {s. a\<in>s}"
    5.28 +"mc(NOT f)   = -mc f"
    5.29 +"mc(And f g) = mc f Int mc g"
    5.30 +"mc(AX f)    = {s. \<forall>t. (s,t) \<in> M  \<longrightarrow> t \<in> mc f}"
    5.31 +"mc(EF f)    = lfp(\<lambda>T. mc f \<union> {s. \<exists>t. (s,t)\<in>M \<and> t\<in>T})";
    5.32 +
    5.33 +lemma mono_lemma: "mono(\<lambda>T. A \<union> {s. \<exists>t. (s,t)\<in>M \<and> t\<in>T})";
    5.34 +apply(rule monoI);
    5.35 +by(blast);
    5.36 +
    5.37 +lemma lfp_conv_EF:
    5.38 +"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}";
    5.39 +apply(rule equalityI);
    5.40 + apply(rule subsetI);
    5.41 + apply(simp);
    5.42 + apply(erule Lfp.induct);
    5.43 +  apply(rule mono_lemma);
    5.44 + apply(simp);
    5.45 + apply(blast intro: r_into_rtrancl rtrancl_trans);
    5.46 +apply(rule subsetI);
    5.47 +apply(simp);
    5.48 +apply(erule exE);
    5.49 +apply(erule conjE);
    5.50 +apply(erule_tac P = "t\<in>A" in rev_mp);
    5.51 +apply(erule converse_rtrancl_induct);
    5.52 + apply(rule ssubst[OF lfp_Tarski[OF mono_lemma]]);
    5.53 + apply(blast);
    5.54 +apply(rule ssubst[OF lfp_Tarski[OF mono_lemma]]);
    5.55 +by(blast);
    5.56 +
    5.57 +theorem "mc f = {s. s \<Turnstile> f}";
    5.58 +apply(induct_tac f);
    5.59 +by(auto simp add:lfp_conv_EF);
    5.60 +
    5.61 +end;
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/doc-src/TutorialI/CTL/ROOT.ML	Thu Sep 14 17:46:00 2000 +0200
     6.3 @@ -0,0 +1,3 @@
     6.4 +use "../settings.ML";
     6.5 +use_thy "PDL";
     6.6 +use_thy "CTL";
     7.1 --- a/doc-src/TutorialI/IsaMakefile	Thu Sep 14 17:46:00 2000 +0200
     7.2 +++ b/doc-src/TutorialI/IsaMakefile	Thu Sep 14 17:46:00 2000 +0200
     7.3 @@ -4,7 +4,7 @@
     7.4  
     7.5  ## targets
     7.6  
     7.7 -default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Recdef HOL-Advanced HOL-Misc styles
     7.8 +default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Recdef HOL-Advanced HOL-CTL HOL-Misc styles
     7.9  images:
    7.10  test:
    7.11  all: default
    7.12 @@ -101,6 +101,14 @@
    7.13  	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Advanced
    7.14  	@rm -f tutorial.dvi
    7.15  
    7.16 +## HOL-CTL
    7.17 +
    7.18 +HOL-CTL: HOL $(LOG)/HOL-CTL.gz
    7.19 +
    7.20 +$(LOG)/HOL-CTL.gz: $(OUT)/HOL CTL/PDL.thy CTL/CTL.thy CTL/ROOT.ML
    7.21 +	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL CTL
    7.22 +	@rm -f tutorial.dvi
    7.23 +
    7.24  ## HOL-Misc
    7.25  
    7.26  HOL-Misc: HOL $(LOG)/HOL-Misc.gz
    7.27 @@ -117,4 +125,4 @@
    7.28  ## clean
    7.29  
    7.30  clean:
    7.31 -	@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 
    7.32 +	@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 
     8.1 --- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Thu Sep 14 17:46:00 2000 +0200
     8.2 +++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Thu Sep 14 17:46:00 2000 +0200
     8.3 @@ -86,16 +86,16 @@
     8.4  \begin{isamarkuptext}%
     8.5  \noindent
     8.6  or the wholesale stripping of \isa{{\isasymforall}} and
     8.7 -\isa{{\isasymlongrightarrow}} in the conclusion via \isa{rulified}%
     8.8 +\isa{{\isasymlongrightarrow}} in the conclusion via \isa{rule{\isacharunderscore}format}%
     8.9  \end{isamarkuptext}%
    8.10 -\isacommand{lemmas}\ myrule\ {\isacharequal}\ simple{\isacharbrackleft}rulified{\isacharbrackright}%
    8.11 +\isacommand{lemmas}\ myrule\ {\isacharequal}\ simple{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}%
    8.12  \begin{isamarkuptext}%
    8.13  \noindent
    8.14  yielding \isa{{\isasymlbrakk}A\ y{\isacharsemicolon}\ B\ y{\isasymrbrakk}\ {\isasymLongrightarrow}\ B\ y\ {\isasymand}\ A\ y}.
    8.15  You can go one step further and include these derivations already in the
    8.16  statement of your original lemma, thus avoiding the intermediate step:%
    8.17  \end{isamarkuptext}%
    8.18 -\isacommand{lemma}\ myrule{\isacharbrackleft}rulified{\isacharbrackright}{\isacharcolon}\ \ {\isachardoublequote}{\isasymforall}y{\isachardot}\ A\ y\ {\isasymlongrightarrow}\ B\ y\ {\isasymlongrightarrow}\ B\ y\ {\isacharampersand}\ A\ y{\isachardoublequote}%
    8.19 +\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}%
    8.20  \begin{isamarkuptext}%
    8.21  \bigskip
    8.22  
    8.23 @@ -185,13 +185,13 @@
    8.24  
    8.25  We can now derive the desired \isa{i\ {\isasymle}\ f\ i} from \isa{f{\isacharunderscore}incr}:%
    8.26  \end{isamarkuptext}%
    8.27 -\isacommand{lemmas}\ f{\isacharunderscore}incr\ {\isacharequal}\ f{\isacharunderscore}incr{\isacharunderscore}lem{\isacharbrackleft}rulified{\isacharcomma}\ OF\ refl{\isacharbrackright}%
    8.28 +\isacommand{lemmas}\ f{\isacharunderscore}incr\ {\isacharequal}\ f{\isacharunderscore}incr{\isacharunderscore}lem{\isacharbrackleft}rule{\isacharunderscore}format{\isacharcomma}\ OF\ refl{\isacharbrackright}%
    8.29  \begin{isamarkuptext}%
    8.30  \noindent
    8.31  The final \isa{refl} gets rid of the premise \isa{{\isacharquery}k\ {\isacharequal}\ f\ {\isacharquery}i}. Again,
    8.32  we could have included this derivation in the original statement of the lemma:%
    8.33  \end{isamarkuptext}%
    8.34 -\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}%
    8.35 +\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}%
    8.36  \begin{isamarkuptext}%
    8.37  \begin{exercise}
    8.38  From the above axiom and lemma for \isa{f} show that \isa{f} is the
     9.1 --- a/doc-src/TutorialI/tricks.tex	Thu Sep 14 17:46:00 2000 +0200
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,27 +0,0 @@
     9.4 -%\chapter{The Tricks of the Trade}
     9.5 -\chapter{Advanced Simplification, Recursion, and Induction}
     9.6 -\markboth{}{CHAPTER 4: ADVANCED}
     9.7 -
     9.8 -Although we have already learned a lot about simplification, recursion and
     9.9 -induction, there are some advanced proof techniques that we have not covered
    9.10 -yet and which are worth knowing about if you intend to beome a serious
    9.11 -(human) theorem prover. The three sections of this chapter are almost
    9.12 -independent of each other and can be read in any order. Only the notion of
    9.13 -\emph{congruence rules}, introduced in the section on simplification, is
    9.14 -required for parts of the section on recursion.
    9.15 -
    9.16 -\input{Advanced/document/simp.tex}
    9.17 -
    9.18 -\section{Advanced forms of recursion}
    9.19 -\label{sec:advanced-recdef}
    9.20 -\index{*recdef|(}
    9.21 -\input{Recdef/document/Nested0.tex}
    9.22 -\input{Recdef/document/Nested1.tex}
    9.23 -\input{Recdef/document/Nested2.tex}
    9.24 -\index{*recdef|)}
    9.25 -
    9.26 -\section{Advanced induction techniques}
    9.27 -\label{sec:advanced-ind}
    9.28 -\index{induction|(}
    9.29 -\input{Misc/document/AdvancedInd.tex}
    9.30 -\index{induction|)}
    10.1 --- a/doc-src/TutorialI/tutorial.tex	Thu Sep 14 17:46:00 2000 +0200
    10.2 +++ b/doc-src/TutorialI/tutorial.tex	Thu Sep 14 17:46:00 2000 +0200
    10.3 @@ -65,7 +65,8 @@
    10.4  
    10.5  \input{basics}
    10.6  \input{fp}
    10.7 -\input{tricks}
    10.8 +\input{Advanced/advanced}
    10.9 +%\chapter{The Tricks of the Trade}
   10.10  \input{appendix}
   10.11  
   10.12  \bibliographystyle{plain}