src/HOL/ex/CTL.thy
 author nipkow Fri Mar 06 17:38:47 2009 +0100 (2009-03-06) changeset 30313 b2441b0c8d38 parent 26813 6a4d5ca6d2e5 child 32587 caa5ada96a00 permissions -rw-r--r--
     1 (*  Title:      HOL/ex/CTL.thy

     2     ID:         $Id$

     3     Author:     Gertrud Bauer

     4 *)

     5

     6 header {* CTL formulae *}

     7

     8 theory CTL imports Main begin

     9

    10 text {*

    11   We formalize basic concepts of Computational Tree Logic (CTL)

    12   \cite{McMillan-PhDThesis,McMillan-LectureNotes} within the

    13   simply-typed set theory of HOL.

    14

    15   By using the common technique of shallow embedding'', a CTL

    16   formula is identified with the corresponding set of states where it

    17   holds.  Consequently, CTL operations such as negation, conjunction,

    18   disjunction simply become complement, intersection, union of sets.

    19   We only require a separate operation for implication, as point-wise

    20   inclusion is usually not encountered in plain set-theory.

    21 *}

    22

    23 lemmas [intro!] = Int_greatest Un_upper2 Un_upper1 Int_lower1 Int_lower2

    24

    25 types 'a ctl = "'a set"

    26

    27 definition

    28   imp :: "'a ctl \<Rightarrow> 'a ctl \<Rightarrow> 'a ctl"    (infixr "\<rightarrow>" 75) where

    29   "p \<rightarrow> q = - p \<union> q"

    30

    31 lemma [intro!]: "p \<inter> p \<rightarrow> q \<subseteq> q" unfolding imp_def by auto

    32 lemma [intro!]: "p \<subseteq> (q \<rightarrow> p)" unfolding imp_def by rule

    33

    34

    35 text {*

    36   \smallskip The CTL path operators are more interesting; they are

    37   based on an arbitrary, but fixed model @{text \<M>}, which is simply

    38   a transition relation over states @{typ "'a"}.

    39 *}

    40

    41 axiomatization \<M> :: "('a \<times> 'a) set"

    42

    43 text {*

    44   The operators @{text \<EX>}, @{text \<EF>}, @{text \<EG>} are taken

    45   as primitives, while @{text \<AX>}, @{text \<AF>}, @{text \<AG>} are

    46   defined as derived ones.  The formula @{text "\<EX> p"} holds in a

    47   state @{term s}, iff there is a successor state @{term s'} (with

    48   respect to the model @{term \<M>}), such that @{term p} holds in

    49   @{term s'}.  The formula @{text "\<EF> p"} holds in a state @{term

    50   s}, iff there is a path in @{text \<M>}, starting from @{term s},

    51   such that there exists a state @{term s'} on the path, such that

    52   @{term p} holds in @{term s'}.  The formula @{text "\<EG> p"} holds

    53   in a state @{term s}, iff there is a path, starting from @{term s},

    54   such that for all states @{term s'} on the path, @{term p} holds in

    55   @{term s'}.  It is easy to see that @{text "\<EF> p"} and @{text

    56   "\<EG> p"} may be expressed using least and greatest fixed points

    57   \cite{McMillan-PhDThesis}.

    58 *}

    59

    60 definition

    61   EX  ("\<EX> _"  90) where "\<EX> p = {s. \<exists>s'. (s, s') \<in> \<M> \<and> s' \<in> p}"

    62 definition

    63   EF ("\<EF> _"  90)  where "\<EF> p = lfp (\<lambda>s. p \<union> \<EX> s)"

    64 definition

    65   EG ("\<EG> _"  90)  where "\<EG> p = gfp (\<lambda>s. p \<inter> \<EX> s)"

    66

    67 text {*

    68   @{text "\<AX>"}, @{text "\<AF>"} and @{text "\<AG>"} are now defined

    69   dually in terms of @{text "\<EX>"}, @{text "\<EF>"} and @{text

    70   "\<EG>"}.

    71 *}

    72

    73 definition

    74   AX  ("\<AX> _"  90) where "\<AX> p = - \<EX> - p"

    75 definition

    76   AF  ("\<AF> _"  90) where "\<AF> p = - \<EG> - p"

    77 definition

    78   AG  ("\<AG> _"  90) where "\<AG> p = - \<EF> - p"

    79

    80 lemmas [simp] = EX_def EG_def AX_def EF_def AF_def AG_def

    81

    82

    83 subsection {* Basic fixed point properties *}

    84

    85 text {*

    86   First of all, we use the de-Morgan property of fixed points

    87 *}

    88

    89 lemma lfp_gfp: "lfp f = - gfp (\<lambda>s::'a set. - (f (- s)))"

    90 proof

    91   show "lfp f \<subseteq> - gfp (\<lambda>s. - f (- s))"

    92   proof

    93     fix x assume l: "x \<in> lfp f"

    94     show "x \<in> - gfp (\<lambda>s. - f (- s))"

    95     proof

    96       assume "x \<in> gfp (\<lambda>s. - f (- s))"

    97       then obtain u where "x \<in> u" and "u \<subseteq> - f (- u)"

    98 	by (auto simp add: gfp_def Sup_set_eq)

    99       then have "f (- u) \<subseteq> - u" by auto

   100       then have "lfp f \<subseteq> - u" by (rule lfp_lowerbound)

   101       from l and this have "x \<notin> u" by auto

   102       with x \<in> u show False by contradiction

   103     qed

   104   qed

   105   show "- gfp (\<lambda>s. - f (- s)) \<subseteq> lfp f"

   106   proof (rule lfp_greatest)

   107     fix u assume "f u \<subseteq> u"

   108     then have "- u \<subseteq> - f u" by auto

   109     then have "- u \<subseteq> - f (- (- u))" by simp

   110     then have "- u \<subseteq> gfp (\<lambda>s. - f (- s))" by (rule gfp_upperbound)

   111     then show "- gfp (\<lambda>s. - f (- s)) \<subseteq> u" by auto

   112   qed

   113 qed

   114

   115 lemma lfp_gfp': "- lfp f = gfp (\<lambda>s::'a set. - (f (- s)))"

   116   by (simp add: lfp_gfp)

   117

   118 lemma gfp_lfp': "- gfp f = lfp (\<lambda>s::'a set. - (f (- s)))"

   119   by (simp add: lfp_gfp)

   120

   121 text {*

   122   in order to give dual fixed point representations of @{term "AF p"}

   123   and @{term "AG p"}:

   124 *}

   125

   126 lemma AF_lfp: "\<AF> p = lfp (\<lambda>s. p \<union> \<AX> s)" by (simp add: lfp_gfp)

   127 lemma AG_gfp: "\<AG> p = gfp (\<lambda>s. p \<inter> \<AX> s)" by (simp add: lfp_gfp)

   128

   129 lemma EF_fp: "\<EF> p = p \<union> \<EX> \<EF> p"

   130 proof -

   131   have "mono (\<lambda>s. p \<union> \<EX> s)" by rule (auto simp add: EX_def)

   132   then show ?thesis by (simp only: EF_def) (rule lfp_unfold)

   133 qed

   134

   135 lemma AF_fp: "\<AF> p = p \<union> \<AX> \<AF> p"

   136 proof -

   137   have "mono (\<lambda>s. p \<union> \<AX> s)" by rule (auto simp add: AX_def EX_def)

   138   then show ?thesis by (simp only: AF_lfp) (rule lfp_unfold)

   139 qed

   140

   141 lemma EG_fp: "\<EG> p = p \<inter> \<EX> \<EG> p"

   142 proof -

   143   have "mono (\<lambda>s. p \<inter> \<EX> s)" by rule (auto simp add: EX_def)

   144   then show ?thesis by (simp only: EG_def) (rule gfp_unfold)

   145 qed

   146

   147 text {*

   148   From the greatest fixed point definition of @{term "\<AG> p"}, we

   149   derive as a consequence of the Knaster-Tarski theorem on the one

   150   hand that @{term "\<AG> p"} is a fixed point of the monotonic

   151   function @{term "\<lambda>s. p \<inter> \<AX> s"}.

   152 *}

   153

   154 lemma AG_fp: "\<AG> p = p \<inter> \<AX> \<AG> p"

   155 proof -

   156   have "mono (\<lambda>s. p \<inter> \<AX> s)" by rule (auto simp add: AX_def EX_def)

   157   then show ?thesis by (simp only: AG_gfp) (rule gfp_unfold)

   158 qed

   159

   160 text {*

   161   This fact may be split up into two inequalities (merely using

   162   transitivity of @{text "\<subseteq>" }, which is an instance of the overloaded

   163   @{text "\<le>"} in Isabelle/HOL).

   164 *}

   165

   166 lemma AG_fp_1: "\<AG> p \<subseteq> p"

   167 proof -

   168   note AG_fp also have "p \<inter> \<AX> \<AG> p \<subseteq> p" by auto

   169   finally show ?thesis .

   170 qed

   171

   172 lemma AG_fp_2: "\<AG> p \<subseteq> \<AX> \<AG> p"

   173 proof -

   174   note AG_fp also have "p \<inter> \<AX> \<AG> p \<subseteq> \<AX> \<AG> p" by auto

   175   finally show ?thesis .

   176 qed

   177

   178 text {*

   179   On the other hand, we have from the Knaster-Tarski fixed point

   180   theorem that any other post-fixed point of @{term "\<lambda>s. p \<inter> AX s"} is

   181   smaller than @{term "AG p"}.  A post-fixed point is a set of states

   182   @{term q} such that @{term "q \<subseteq> p \<inter> AX q"}.  This leads to the

   183   following co-induction principle for @{term "AG p"}.

   184 *}

   185

   186 lemma AG_I: "q \<subseteq> p \<inter> \<AX> q \<Longrightarrow> q \<subseteq> \<AG> p"

   187   by (simp only: AG_gfp) (rule gfp_upperbound)

   188

   189

   190 subsection {* The tree induction principle \label{sec:calc-ctl-tree-induct} *}

   191

   192 text {*

   193   With the most basic facts available, we are now able to establish a

   194   few more interesting results, leading to the \emph{tree induction}

   195   principle for @{text AG} (see below).  We will use some elementary

   196   monotonicity and distributivity rules.

   197 *}

   198

   199 lemma AX_int: "\<AX> (p \<inter> q) = \<AX> p \<inter> \<AX> q" by auto

   200 lemma AX_mono: "p \<subseteq> q \<Longrightarrow> \<AX> p \<subseteq> \<AX> q" by auto

   201 lemma AG_mono: "p \<subseteq> q \<Longrightarrow> \<AG> p \<subseteq> \<AG> q"

   202   by (simp only: AG_gfp, rule gfp_mono) auto

   203

   204 text {*

   205   The formula @{term "AG p"} implies @{term "AX p"} (we use

   206   substitution of @{text "\<subseteq>"} with monotonicity).

   207 *}

   208

   209 lemma AG_AX: "\<AG> p \<subseteq> \<AX> p"

   210 proof -

   211   have "\<AG> p \<subseteq> \<AX> \<AG> p" by (rule AG_fp_2)

   212   also have "\<AG> p \<subseteq> p" by (rule AG_fp_1) moreover note AX_mono

   213   finally show ?thesis .

   214 qed

   215

   216 text {*

   217   Furthermore we show idempotency of the @{text "\<AG>"} operator.

   218   The proof is a good example of how accumulated facts may get

   219   used to feed a single rule step.

   220 *}

   221

   222 lemma AG_AG: "\<AG> \<AG> p = \<AG> p"

   223 proof

   224   show "\<AG> \<AG> p \<subseteq> \<AG> p" by (rule AG_fp_1)

   225 next

   226   show "\<AG> p \<subseteq> \<AG> \<AG> p"

   227   proof (rule AG_I)

   228     have "\<AG> p \<subseteq> \<AG> p" ..

   229     moreover have "\<AG> p \<subseteq> \<AX> \<AG> p" by (rule AG_fp_2)

   230     ultimately show "\<AG> p \<subseteq> \<AG> p \<inter> \<AX> \<AG> p" ..

   231   qed

   232 qed

   233

   234 text {*

   235   \smallskip We now give an alternative characterization of the @{text

   236   "\<AG>"} operator, which describes the @{text "\<AG>"} operator in

   237   an operational'' way by tree induction: In a state holds @{term

   238   "AG p"} iff in that state holds @{term p}, and in all reachable

   239   states @{term s} follows from the fact that @{term p} holds in

   240   @{term s}, that @{term p} also holds in all successor states of

   241   @{term s}.  We use the co-induction principle @{thm [source] AG_I}

   242   to establish this in a purely algebraic manner.

   243 *}

   244

   245 theorem AG_induct: "p \<inter> \<AG> (p \<rightarrow> \<AX> p) = \<AG> p"

   246 proof

   247   show "p \<inter> \<AG> (p \<rightarrow> \<AX> p) \<subseteq> \<AG> p"  (is "?lhs \<subseteq> _")

   248   proof (rule AG_I)

   249     show "?lhs \<subseteq> p \<inter> \<AX> ?lhs"

   250     proof

   251       show "?lhs \<subseteq> p" ..

   252       show "?lhs \<subseteq> \<AX> ?lhs"

   253       proof -

   254 	{

   255 	  have "\<AG> (p \<rightarrow> \<AX> p) \<subseteq> p \<rightarrow> \<AX> p" by (rule AG_fp_1)

   256           moreover have "p \<inter> p \<rightarrow> \<AX> p \<subseteq> \<AX> p" ..

   257           ultimately have "?lhs \<subseteq> \<AX> p" by auto

   258 	}

   259 	moreover

   260 	{

   261 	  have "p \<inter> \<AG> (p \<rightarrow> \<AX> p) \<subseteq> \<AG> (p \<rightarrow> \<AX> p)" ..

   262           also have "\<dots> \<subseteq> \<AX> \<dots>" by (rule AG_fp_2)

   263           finally have "?lhs \<subseteq> \<AX> \<AG> (p \<rightarrow> \<AX> p)" .

   264 	}

   265 	ultimately have "?lhs \<subseteq> \<AX> p \<inter> \<AX> \<AG> (p \<rightarrow> \<AX> p)"

   266 	  by (rule Int_greatest)

   267 	also have "\<dots> = \<AX> ?lhs" by (simp only: AX_int)

   268 	finally show ?thesis .

   269       qed

   270     qed

   271   qed

   272 next

   273   show "\<AG> p \<subseteq> p \<inter> \<AG> (p \<rightarrow> \<AX> p)"

   274   proof

   275     show "\<AG> p \<subseteq> p" by (rule AG_fp_1)

   276     show "\<AG> p \<subseteq> \<AG> (p \<rightarrow> \<AX> p)"

   277     proof -

   278       have "\<AG> p = \<AG> \<AG> p" by (simp only: AG_AG)

   279       also have "\<AG> p \<subseteq> \<AX> p" by (rule AG_AX) moreover note AG_mono

   280       also have "\<AX> p \<subseteq> (p \<rightarrow> \<AX> p)" .. moreover note AG_mono

   281       finally show ?thesis .

   282     qed

   283   qed

   284 qed

   285

   286

   287 subsection {* An application of tree induction \label{sec:calc-ctl-commute} *}

   288

   289 text {*

   290   Further interesting properties of CTL expressions may be

   291   demonstrated with the help of tree induction; here we show that

   292   @{text \<AX>} and @{text \<AG>} commute.

   293 *}

   294

   295 theorem AG_AX_commute: "\<AG> \<AX> p = \<AX> \<AG> p"

   296 proof -

   297   have "\<AG> \<AX> p = \<AX> p \<inter> \<AX> \<AG> \<AX> p" by (rule AG_fp)

   298   also have "\<dots> = \<AX> (p \<inter> \<AG> \<AX> p)" by (simp only: AX_int)

   299   also have "p \<inter> \<AG> \<AX> p = \<AG> p"  (is "?lhs = _")

   300   proof

   301     have "\<AX> p \<subseteq> p \<rightarrow> \<AX> p" ..

   302     also have "p \<inter> \<AG> (p \<rightarrow> \<AX> p) = \<AG> p" by (rule AG_induct)

   303     also note Int_mono AG_mono

   304     ultimately show "?lhs \<subseteq> \<AG> p" by fast

   305   next

   306     have "\<AG> p \<subseteq> p" by (rule AG_fp_1)

   307     moreover

   308     {

   309       have "\<AG> p = \<AG> \<AG> p" by (simp only: AG_AG)

   310       also have "\<AG> p \<subseteq> \<AX> p" by (rule AG_AX)

   311       also note AG_mono

   312       ultimately have "\<AG> p \<subseteq> \<AG> \<AX> p" .

   313     }

   314     ultimately show "\<AG> p \<subseteq> ?lhs" ..

   315   qed

   316   finally show ?thesis .

   317 qed

   318

   319 end