src/HOL/ex/CTL.thy
 author hoelzl Thu Jan 31 11:31:27 2013 +0100 (2013-01-31) changeset 50999 3de230ed0547 parent 46685 866a798d051c child 58622 aa99568f56de permissions -rw-r--r--
introduce order topology
     1 (*  Title:      HOL/ex/CTL.thy

     2     Author:     Gertrud Bauer

     3 *)

     4

     5 header {* CTL formulae *}

     6

     7 theory CTL

     8 imports Main

     9 begin

    10

    11 text {*

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

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

    14   simply-typed set theory of HOL.

    15

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

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

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

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

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

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

    22 *}

    23

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

    25

    26 type_synonym 'a ctl = "'a set"

    27

    28 definition

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

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

    31

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

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

    34

    35

    36 text {*

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

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

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

    40 *}

    41

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

    43

    44 text {*

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

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

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

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

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

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

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

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

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

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

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

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

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

    58   \cite{McMillan-PhDThesis}.

    59 *}

    60

    61 definition

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

    63 definition

    64   EF ("\<EF> _" [80] 90)  where "\<EF> p = lfp (\<lambda>s. p \<union> \<EX> s)"

    65 definition

    66   EG ("\<EG> _" [80] 90)  where "\<EG> p = gfp (\<lambda>s. p \<inter> \<EX> s)"

    67

    68 text {*

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

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

    71   "\<EG>"}.

    72 *}

    73

    74 definition

    75   AX  ("\<AX> _" [80] 90) where "\<AX> p = - \<EX> - p"

    76 definition

    77   AF  ("\<AF> _" [80] 90) where "\<AF> p = - \<EG> - p"

    78 definition

    79   AG  ("\<AG> _" [80] 90) where "\<AG> p = - \<EF> - p"

    80

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

    82

    83

    84 subsection {* Basic fixed point properties *}

    85

    86 text {*

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

    88 *}

    89

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

    91 proof

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

    93   proof

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

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

    96     proof

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

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

    99         by (auto simp add: gfp_def)

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

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

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

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

   104     qed

   105   qed

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

   107   proof (rule lfp_greatest)

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

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

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

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

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

   113   qed

   114 qed

   115

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

   117   by (simp add: lfp_gfp)

   118

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

   120   by (simp add: lfp_gfp)

   121

   122 text {*

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

   124   and @{term "AG p"}:

   125 *}

   126

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

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

   129

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

   131 proof -

   132   have "mono (\<lambda>s. p \<union> \<EX> s)" by rule auto

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

   134 qed

   135

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

   137 proof -

   138   have "mono (\<lambda>s. p \<union> \<AX> s)" by rule auto

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

   140 qed

   141

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

   143 proof -

   144   have "mono (\<lambda>s. p \<inter> \<EX> s)" by rule auto

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

   146 qed

   147

   148 text {*

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

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

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

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

   153 *}

   154

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

   156 proof -

   157   have "mono (\<lambda>s. p \<inter> \<AX> s)" by rule auto

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

   159 qed

   160

   161 text {*

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

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

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

   165 *}

   166

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

   168 proof -

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

   170   finally show ?thesis .

   171 qed

   172

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

   174 proof -

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

   176   finally show ?thesis .

   177 qed

   178

   179 text {*

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

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

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

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

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

   185 *}

   186

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

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

   189

   190

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

   192

   193 text {*

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

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

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

   197   monotonicity and distributivity rules.

   198 *}

   199

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

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

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

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

   204

   205 text {*

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

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

   208 *}

   209

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

   211 proof -

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

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

   214   finally show ?thesis .

   215 qed

   216

   217 text {*

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

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

   220   used to feed a single rule step.

   221 *}

   222

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

   224 proof

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

   226 next

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

   228   proof (rule AG_I)

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

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

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

   232   qed

   233 qed

   234

   235 text {*

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

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

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

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

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

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

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

   243   to establish this in a purely algebraic manner.

   244 *}

   245

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

   247 proof

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

   249   proof (rule AG_I)

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

   251     proof

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

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

   254       proof -

   255         {

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

   257           also have "p \<inter> p \<rightarrow> \<AX> p \<subseteq> \<AX> p" ..

   258           finally have "?lhs \<subseteq> \<AX> p" by auto

   259         }

   260         moreover

   261         {

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

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

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

   265         }

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

   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