doc-src/TutorialI/CTL/PDL.thy

--- a/doc-src/TutorialI/CTL/PDL.thy	Tue Oct 03 01:15:11 2000 +0200
+++ b/doc-src/TutorialI/CTL/PDL.thy	Tue Oct 03 11:26:54 2000 +0200
@@ -2,36 +2,61 @@
 
 subsection{*Propositional dynmic logic---PDL*}
 
-datatype ctl_form = Atom atom
-                  | NOT ctl_form
-                  | And ctl_form ctl_form
-                  | AX ctl_form
-                  | EF ctl_form;
+text{*
+The formulae of PDL are built up from atomic propositions via the customary
+propositional connectives of negation and conjunction and the two temporal
+connectives @{text AX} and @{text EF}. Since formulae are essentially
+(syntax) trees, they are naturally modelled as a datatype:
+*}
 
-consts valid :: "state \<Rightarrow> ctl_form \<Rightarrow> bool" ("(_ \<Turnstile> _)" [80,80] 80)
-       M :: "(state \<times> state)set";
+datatype pdl_form = Atom atom
+                  | NOT pdl_form
+                  | And pdl_form pdl_form
+                  | AX pdl_form
+                  | EF pdl_form;
+
+text{*\noindent
+The meaning of these formulae is given by saying which formula is true in
+which state:
+*}
+
+consts valid :: "state \<Rightarrow> pdl_form \<Rightarrow> bool" ("(_ \<Turnstile> _)" [80,80] 80)
 
 primrec
-"s \<Turnstile> Atom a  = (a\<in>s)"
+"s \<Turnstile> Atom a  = (a \<in> L 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";
+text{*
+Now we come to the model checker itself. It maps a formula into the set of
+states where the formula is true and is defined by recursion over the syntax:
+*}
+
+consts mc :: "pdl_form \<Rightarrow> state set";
 primrec
-"mc(Atom a)  = {s. a\<in>s}"
+"mc(Atom a)  = {s. a \<in> L s}"
 "mc(NOT f)   = -mc f"
-"mc(And f g) = mc f Int mc g"
+"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(EF f)    = lfp(\<lambda>T. mc f \<union> M^-1 ^^ T)"
+
 
-lemma mono_lemma: "mono(\<lambda>T. A \<union> {s. \<exists>t. (s,t)\<in>M \<and> t\<in>T})";
+text{*
+Only the equation for @{term EF} deserves a comment: the postfix @{text"^-1"}
+and the infix @{text"^^"} are predefined and denote the converse of a
+relation and the application of a relation to a set. Thus @{term "M^-1 ^^ T"}
+is the set of all predecessors of @{term T} and @{term"mc(EF f)"} is the least
+set @{term T} containing @{term"mc f"} and all predecessors of @{term T}.
+*}
+
+lemma mono_lemma: "mono(\<lambda>T. A \<union> M^-1 ^^ 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}";
+"lfp(\<lambda>T. A \<union> M^-1 ^^ T) = {s. \<exists>t. (s,t) \<in> M^* \<and> t \<in> A}";
 apply(rule equalityI);
  apply(rule subsetI);
  apply(simp);
@@ -53,5 +78,4 @@
 theorem "mc f = {s. s \<Turnstile> f}";
 apply(induct_tac f);
 by(auto simp add:lfp_conv_EF);
-
-end;
+(*<*)end(*>*)