src/HOL/ex/CTL.thy
 author obua Mon Apr 10 16:00:34 2006 +0200 (2006-04-10) changeset 19404 9bf2cdc9e8e8 parent 17388 495c799df31d child 20807 bd3b60f9a343 permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
     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 constdefs

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

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

    29

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

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

    32

    33

    34 text {*

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

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

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

    38 *}

    39

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

    41

    42 text {*

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

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

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

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

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

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

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

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

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

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

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

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

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

    56   \cite{McMillan-PhDThesis}.

    57 *}

    58

    59 constdefs

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

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

    62   EG :: "'a ctl \<Rightarrow> 'a ctl"    ("\<EG> _"  90)    "\<EG> p \<equiv> gfp (\<lambda>s. p \<inter> \<EX> s)"

    63

    64 text {*

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

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

    67   "\<EG>"}.

    68 *}

    69

    70 constdefs

    71   AX :: "'a ctl \<Rightarrow> 'a ctl"    ("\<AX> _"  90)    "\<AX> p \<equiv> - \<EX> - p"

    72   AF :: "'a ctl \<Rightarrow> 'a ctl"    ("\<AF> _"  90)    "\<AF> p \<equiv> - \<EG> - p"

    73   AG :: "'a ctl \<Rightarrow> 'a ctl"    ("\<AG> _"  90)    "\<AG> p \<equiv> - \<EF> - p"

    74

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

    76

    77

    78 section {* Basic fixed point properties *}

    79

    80 text {*

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

    82 *}

    83

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

    85 proof

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

    87   proof

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

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

    90     proof

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

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

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

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

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

    96       then show False by contradiction

    97     qed

    98   qed

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

   100   proof (rule lfp_greatest)

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

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

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

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

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

   106   qed

   107 qed

   108

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

   110   by (simp add: lfp_gfp)

   111

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

   113   by (simp add: lfp_gfp)

   114

   115 text {*

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

   117   and @{term "AG p"}:

   118 *}

   119

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

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

   122

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

   124 proof -

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

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

   127 qed

   128

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

   130 proof -

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

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

   133 qed

   134

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

   136 proof -

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

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

   139 qed

   140

   141 text {*

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

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

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

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

   146 *}

   147

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

   149 proof -

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

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

   152 qed

   153

   154 text {*

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

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

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

   158 *}

   159

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

   161 proof -

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

   163   finally show ?thesis .

   164 qed

   165

   166 text {**}

   167

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

   169 proof -

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

   171   finally show ?thesis .

   172 qed

   173

   174 text {*

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

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

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

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

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

   180 *}

   181

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

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

   184

   185

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

   187

   188 text {*

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

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

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

   192   monotonicity and distributivity rules.

   193 *}

   194

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

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

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

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

   199

   200 text {*

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

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

   203 *}

   204

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

   206 proof -

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

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

   209   finally show ?thesis .

   210 qed

   211

   212 text {*

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

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

   215   used to feed a single rule step.

   216 *}

   217

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

   219 proof

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

   221 next

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

   223   proof (rule AG_I)

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

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

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

   227   qed

   228 qed

   229

   230 text {*

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

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

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

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

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

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

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

   238   to establish this in a purely algebraic manner.

   239 *}

   240

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

   242 proof

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

   244   proof (rule AG_I)

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

   246     proof

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

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

   249       proof -

   250 	{

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

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

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

   254 	}

   255 	moreover

   256 	{

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

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

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

   260 	}

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

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

   263 	finally show ?thesis .

   264       qed

   265     qed

   266   qed

   267 next

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

   269   proof

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

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

   272     proof -

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

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

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

   276       finally show ?thesis .

   277     qed

   278   qed

   279 qed

   280

   281

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

   283

   284 text {*

   285   Further interesting properties of CTL expressions may be

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

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

   288 *}

   289

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

   291 proof -

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

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

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

   295   proof

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

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

   298     also note Int_mono AG_mono

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

   300   next

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

   302     moreover

   303     {

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

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

   306       also note AG_mono

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

   308     }

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

   310   qed

   311   finally show ?thesis .

   312 qed

   313

   314 end