doc-src/TutorialI/CTL/PDL.thy
author nipkow
Thu Sep 14 17:46:00 2000 +0200 (2000-09-14)
changeset 9958 67f2920862c7
child 10122 194c7349b6c0
permissions -rw-r--r--
*** empty log message ***
     1 theory PDL = Main:;
     2 
     3 typedecl atom;
     4 types state = "atom set";
     5 
     6 datatype ctl_form = Atom atom
     7                   | NOT ctl_form
     8                   | And ctl_form ctl_form
     9                   | AX ctl_form
    10                   | EF ctl_form;
    11 
    12 consts valid :: "state \<Rightarrow> ctl_form \<Rightarrow> bool" ("(_ \<Turnstile> _)" [80,80] 80)
    13        M :: "(state \<times> state)set";
    14 
    15 primrec
    16 "s \<Turnstile> Atom a  = (a\<in>s)"
    17 "s \<Turnstile> NOT f   = (\<not>(s \<Turnstile> f))"
    18 "s \<Turnstile> And f g = (s \<Turnstile> f \<and> s \<Turnstile> g)"
    19 "s \<Turnstile> AX f    = (\<forall>t. (s,t) \<in> M \<longrightarrow> t \<Turnstile> f)"
    20 "s \<Turnstile> EF f    = (\<exists>t. (s,t) \<in> M^* \<and> t \<Turnstile> f)";
    21 
    22 consts mc :: "ctl_form \<Rightarrow> state set";
    23 primrec
    24 "mc(Atom a)  = {s. a\<in>s}"
    25 "mc(NOT f)   = -mc f"
    26 "mc(And f g) = mc f Int mc g"
    27 "mc(AX f)    = {s. \<forall>t. (s,t) \<in> M  \<longrightarrow> t \<in> mc f}"
    28 "mc(EF f)    = lfp(\<lambda>T. mc f \<union> {s. \<exists>t. (s,t)\<in>M \<and> t\<in>T})";
    29 
    30 lemma mono_lemma: "mono(\<lambda>T. A \<union> {s. \<exists>t. (s,t)\<in>M \<and> t\<in>T})";
    31 apply(rule monoI);
    32 by(blast);
    33 
    34 lemma lfp_conv_EF:
    35 "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}";
    36 apply(rule equalityI);
    37  apply(rule subsetI);
    38  apply(simp);
    39  apply(erule Lfp.induct);
    40   apply(rule mono_lemma);
    41  apply(simp);
    42  apply(blast intro: r_into_rtrancl rtrancl_trans);
    43 apply(rule subsetI);
    44 apply(simp);
    45 apply(erule exE);
    46 apply(erule conjE);
    47 apply(erule_tac P = "t\<in>A" in rev_mp);
    48 apply(erule converse_rtrancl_induct);
    49  apply(rule ssubst[OF lfp_Tarski[OF mono_lemma]]);
    50  apply(blast);
    51 apply(rule ssubst[OF lfp_Tarski[OF mono_lemma]]);
    52 by(blast);
    53 
    54 theorem "mc f = {s. s \<Turnstile> f}";
    55 apply(induct_tac f);
    56 by(auto simp add:lfp_conv_EF);
    57 
    58 end;