src/HOL/ex/CTL.thy
 author bauerg Thu Apr 28 17:08:08 2005 +0200 (2005-04-28) changeset 15871 e524119dbf19 child 16417 9bc16273c2d4 permissions -rw-r--r--
*** empty log message ***
     1

     2 (*  Title:      HOL/ex/CTL.thy

     3     ID:         $Id$

     4     Author:     Gertrud Bauer

     5 *)

     6

     7 header {* CTL formulae *}

     8

     9 theory CTL = Main:

    10

    11

    12

    13 text {*

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

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

    16   simply-typed set theory of HOL.

    17

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

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

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

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

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

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

    24 *}

    25

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

    27

    28 types 'a ctl = "'a set"

    29 constdefs

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

    31   "p \<rightarrow> q \<equiv> - p \<union> q"

    32

    33 lemma [intro!]: "p \<inter> p \<rightarrow> q \<subseteq> q" by (unfold imp_def) auto

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

    35

    36

    37 text {*

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

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

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

    41 *}

    42

    43 consts model :: "('a \<times> 'a) set"    ("\<M>")

    44

    45 text {*

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

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

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

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

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

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

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

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

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

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

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

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

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

    59   \cite{McMillan-PhDThesis}.

    60 *}

    61

    62 constdefs

    63   EX :: "'a ctl \<Rightarrow> 'a ctl"    ("\<EX> _" [80] 90)    "\<EX> p \<equiv> {s. \<exists>s'. (s, s') \<in> \<M> \<and> s' \<in> p}"

    64   EF :: "'a ctl \<Rightarrow> 'a ctl"    ("\<EF> _" [80] 90)    "\<EF> p \<equiv> lfp (\<lambda>s. p \<union> \<EX> s)"

    65   EG :: "'a ctl \<Rightarrow> 'a ctl"    ("\<EG> _" [80] 90)    "\<EG> p \<equiv> 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 constdefs

    74   AX :: "'a ctl \<Rightarrow> 'a ctl"    ("\<AX> _" [80] 90)    "\<AX> p \<equiv> - \<EX> - p"

    75   AF :: "'a ctl \<Rightarrow> 'a ctl"    ("\<AF> _" [80] 90)    "\<AF> p \<equiv> - \<EG> - p"

    76   AG :: "'a ctl \<Rightarrow> 'a ctl"    ("\<AG> _" [80] 90)    "\<AG> p \<equiv> - \<EF> - p"

    77

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

    79

    80

    81 section {* Basic fixed point properties *}

    82

    83 text {*

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

    85 *}

    86

    87 lemma lfp_gfp: "lfp f = - gfp (\<lambda>s . - (f (- s)))"

    88 proof

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

    90   proof

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

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

    93     proof

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

    95       then obtain u where "x \<in> u" and "u \<subseteq> - f (- u)" by (unfold gfp_def) auto

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

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

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

    99       then show False by contradiction

   100     qed

   101   qed

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

   103   proof (rule lfp_greatest)

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

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

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

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

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

   109   qed

   110 qed

   111

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

   113   by (simp add: lfp_gfp)

   114

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

   116   by (simp add: lfp_gfp)

   117

   118 text {*

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

   120   and @{term "AG p"}:

   121 *}

   122

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

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

   125

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

   127 proof -

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

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

   130 qed

   131

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

   133 proof -

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

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

   136 qed

   137

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

   139 proof -

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

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

   142 qed

   143

   144 text {*

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

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

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

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

   149 *}

   150

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

   152 proof -

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

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

   155 qed

   156

   157 text {*

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

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

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

   161 *}

   162

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

   164 proof -

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

   166   finally show ?thesis .

   167 qed

   168

   169 text {**}

   170

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

   172 proof -

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

   174   finally show ?thesis .

   175 qed

   176

   177 text {*

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

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

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

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

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

   183 *}

   184

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

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

   187

   188

   189 section {* The tree induction principle \label{sec:calc-ctl-tree-induct} *}

   190

   191 text {*

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

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

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

   195   monotonicity and distributivity rules.

   196 *}

   197

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

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

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

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

   202

   203 text {*

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

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

   206 *}

   207

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

   209 proof -

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

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

   212   finally show ?thesis .

   213 qed

   214

   215 text {*

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

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

   218   used to feed a single rule step.

   219 *}

   220

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

   222 proof

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

   224 next

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

   226   proof (rule AG_I)

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

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

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

   230   qed

   231 qed

   232

   233 text {*

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

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

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

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

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

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

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

   241   to establish this in a purely algebraic manner.

   242 *}

   243

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

   245 proof

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

   247   proof (rule AG_I)

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

   249     proof

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

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

   252       proof -

   253 	{

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

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

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

   257 	}

   258 	moreover

   259 	{

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

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

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

   263 	}

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

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

   266 	finally show ?thesis .

   267       qed

   268     qed

   269   qed

   270 next

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

   272   proof

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

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

   275     proof -

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

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

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

   279       finally show ?thesis .

   280     qed

   281   qed

   282 qed

   283

   284

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

   286

   287 text {*

   288   Further interesting properties of CTL expressions may be

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

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

   291 *}

   292

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

   294 proof -

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

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

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

   298   proof

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

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

   301     also note Int_mono AG_mono

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

   303   next

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

   305     moreover

   306     {

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

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

   309       also note AG_mono

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

   311     }

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

   313   qed

   314   finally show ?thesis .

   315 qed

   316

   317 end