doc-src/TutorialI/CTL/PDL.thy

*** empty log message ***

(*<*)theory PDL = Base:(*>*)

subsection{*Propositional dynmic logic---PDL*}

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;