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;