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}