src/HOL/ex/CTL.thy
author wenzelm
Wed Jun 22 10:09:20 2016 +0200 (2016-06-22)
changeset 63343 fb5d8a50c641
parent 63055 ae0ca486bd3f
child 69597 ff784d5a5bfb
permissions -rw-r--r--
bundle lifting_syntax;
     1 (*  Title:      HOL/ex/CTL.thy
     2     Author:     Gertrud Bauer
     3 *)
     4 
     5 section \<open>CTL formulae\<close>
     6 
     7 theory CTL
     8 imports Main
     9 begin
    10 
    11 text \<open>
    12   We formalize basic concepts of Computational Tree Logic (CTL) @{cite
    13   "McMillan-PhDThesis" and "McMillan-LectureNotes"} within the simply-typed
    14   set theory of HOL.
    15 
    16   By using the common technique of ``shallow embedding'', a CTL formula is
    17   identified with the corresponding set of states where it holds.
    18   Consequently, CTL operations such as negation, conjunction, disjunction
    19   simply become complement, intersection, union of sets. We only require a
    20   separate operation for implication, as point-wise inclusion is usually not
    21   encountered in plain set-theory.
    22 \<close>
    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 imp :: "'a ctl \<Rightarrow> 'a ctl \<Rightarrow> 'a ctl"  (infixr "\<rightarrow>" 75)
    29   where "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 \<open>
    36   \<^smallskip>
    37   The CTL path operators are more interesting; they are based on an arbitrary,
    38   but fixed model \<open>\<M>\<close>, which is simply a transition relation over states
    39   @{typ 'a}.
    40 \<close>
    41 
    42 axiomatization \<M> :: "('a \<times> 'a) set"
    43 
    44 text \<open>
    45   The operators \<open>\<^bold>E\<^bold>X\<close>, \<open>\<^bold>E\<^bold>F\<close>, \<open>\<^bold>E\<^bold>G\<close> are taken as primitives, while \<open>\<^bold>A\<^bold>X\<close>,
    46   \<open>\<^bold>A\<^bold>F\<close>, \<open>\<^bold>A\<^bold>G\<close> are defined as derived ones. The formula \<open>\<^bold>E\<^bold>X p\<close> holds in a
    47   state \<open>s\<close>, iff there is a successor state \<open>s'\<close> (with respect to the model
    48   \<open>\<M>\<close>), such that \<open>p\<close> holds in \<open>s'\<close>. The formula \<open>\<^bold>E\<^bold>F p\<close> holds in a state
    49   \<open>s\<close>, iff there is a path in \<open>\<M>\<close>, starting from \<open>s\<close>, such that there exists a
    50   state \<open>s'\<close> on the path, such that \<open>p\<close> holds in \<open>s'\<close>. The formula \<open>\<^bold>E\<^bold>G p\<close>
    51   holds in a state \<open>s\<close>, iff there is a path, starting from \<open>s\<close>, such that for
    52   all states \<open>s'\<close> on the path, \<open>p\<close> holds in \<open>s'\<close>. It is easy to see that \<open>\<^bold>E\<^bold>F
    53   p\<close> and \<open>\<^bold>E\<^bold>G p\<close> may be expressed using least and greatest fixed points
    54   @{cite "McMillan-PhDThesis"}.
    55 \<close>
    56 
    57 definition EX  ("\<^bold>E\<^bold>X _" [80] 90)
    58   where [simp]: "\<^bold>E\<^bold>X p = {s. \<exists>s'. (s, s') \<in> \<M> \<and> s' \<in> p}"
    59 
    60 definition EF ("\<^bold>E\<^bold>F _" [80] 90)
    61   where [simp]: "\<^bold>E\<^bold>F p = lfp (\<lambda>s. p \<union> \<^bold>E\<^bold>X s)"
    62 
    63 definition EG ("\<^bold>E\<^bold>G _" [80] 90)
    64   where [simp]: "\<^bold>E\<^bold>G p = gfp (\<lambda>s. p \<inter> \<^bold>E\<^bold>X s)"
    65 
    66 text \<open>
    67   \<open>\<^bold>A\<^bold>X\<close>, \<open>\<^bold>A\<^bold>F\<close> and \<open>\<^bold>A\<^bold>G\<close> are now defined dually in terms of \<open>\<^bold>E\<^bold>X\<close>,
    68   \<open>\<^bold>E\<^bold>F\<close> and \<open>\<^bold>E\<^bold>G\<close>.
    69 \<close>
    70 
    71 definition AX  ("\<^bold>A\<^bold>X _" [80] 90)
    72   where [simp]: "\<^bold>A\<^bold>X p = - \<^bold>E\<^bold>X - p"
    73 definition AF  ("\<^bold>A\<^bold>F _" [80] 90)
    74   where [simp]: "\<^bold>A\<^bold>F p = - \<^bold>E\<^bold>G - p"
    75 definition AG  ("\<^bold>A\<^bold>G _" [80] 90)
    76   where [simp]: "\<^bold>A\<^bold>G p = - \<^bold>E\<^bold>F - p"
    77 
    78 
    79 subsection \<open>Basic fixed point properties\<close>
    80 
    81 text \<open>
    82   First of all, we use the de-Morgan property of fixed points.
    83 \<close>
    84 
    85 lemma lfp_gfp: "lfp f = - gfp (\<lambda>s::'a set. - (f (- s)))"
    86 proof
    87   show "lfp f \<subseteq> - gfp (\<lambda>s. - f (- s))"
    88   proof
    89     show "x \<in> - gfp (\<lambda>s. - f (- s))" if l: "x \<in> lfp f" for x
    90     proof
    91       assume "x \<in> gfp (\<lambda>s. - f (- s))"
    92       then obtain u where "x \<in> u" and "u \<subseteq> - f (- u)"
    93         by (auto simp add: gfp_def)
    94       then have "f (- u) \<subseteq> - u" by auto
    95       then have "lfp f \<subseteq> - u" by (rule lfp_lowerbound)
    96       from l and this have "x \<notin> u" by auto
    97       with \<open>x \<in> u\<close> show False by contradiction
    98     qed
    99   qed
   100   show "- gfp (\<lambda>s. - f (- s)) \<subseteq> lfp f"
   101   proof (rule lfp_greatest)
   102     fix u
   103     assume "f u \<subseteq> u"
   104     then have "- u \<subseteq> - f u" by auto
   105     then have "- u \<subseteq> - f (- (- u))" by simp
   106     then have "- u \<subseteq> gfp (\<lambda>s. - f (- s))" by (rule gfp_upperbound)
   107     then show "- gfp (\<lambda>s. - f (- s)) \<subseteq> u" by auto
   108   qed
   109 qed
   110 
   111 lemma lfp_gfp': "- lfp f = gfp (\<lambda>s::'a set. - (f (- s)))"
   112   by (simp add: lfp_gfp)
   113 
   114 lemma gfp_lfp': "- gfp f = lfp (\<lambda>s::'a set. - (f (- s)))"
   115   by (simp add: lfp_gfp)
   116 
   117 text \<open>
   118   In order to give dual fixed point representations of @{term "\<^bold>A\<^bold>F p"} and
   119   @{term "\<^bold>A\<^bold>G p"}:
   120 \<close>
   121 
   122 lemma AF_lfp: "\<^bold>A\<^bold>F p = lfp (\<lambda>s. p \<union> \<^bold>A\<^bold>X s)"
   123   by (simp add: lfp_gfp)
   124 
   125 lemma AG_gfp: "\<^bold>A\<^bold>G p = gfp (\<lambda>s. p \<inter> \<^bold>A\<^bold>X s)"
   126   by (simp add: lfp_gfp)
   127 
   128 lemma EF_fp: "\<^bold>E\<^bold>F p = p \<union> \<^bold>E\<^bold>X \<^bold>E\<^bold>F p"
   129 proof -
   130   have "mono (\<lambda>s. p \<union> \<^bold>E\<^bold>X s)" by rule auto
   131   then show ?thesis by (simp only: EF_def) (rule lfp_unfold)
   132 qed
   133 
   134 lemma AF_fp: "\<^bold>A\<^bold>F p = p \<union> \<^bold>A\<^bold>X \<^bold>A\<^bold>F p"
   135 proof -
   136   have "mono (\<lambda>s. p \<union> \<^bold>A\<^bold>X s)" by rule auto
   137   then show ?thesis by (simp only: AF_lfp) (rule lfp_unfold)
   138 qed
   139 
   140 lemma EG_fp: "\<^bold>E\<^bold>G p = p \<inter> \<^bold>E\<^bold>X \<^bold>E\<^bold>G p"
   141 proof -
   142   have "mono (\<lambda>s. p \<inter> \<^bold>E\<^bold>X s)" by rule auto
   143   then show ?thesis by (simp only: EG_def) (rule gfp_unfold)
   144 qed
   145 
   146 text \<open>
   147   From the greatest fixed point definition of @{term "\<^bold>A\<^bold>G p"}, we derive as
   148   a consequence of the Knaster-Tarski theorem on the one hand that @{term
   149   "\<^bold>A\<^bold>G p"} is a fixed point of the monotonic function
   150   @{term "\<lambda>s. p \<inter> \<^bold>A\<^bold>X s"}.
   151 \<close>
   152 
   153 lemma AG_fp: "\<^bold>A\<^bold>G p = p \<inter> \<^bold>A\<^bold>X \<^bold>A\<^bold>G p"
   154 proof -
   155   have "mono (\<lambda>s. p \<inter> \<^bold>A\<^bold>X s)" by rule auto
   156   then show ?thesis by (simp only: AG_gfp) (rule gfp_unfold)
   157 qed
   158 
   159 text \<open>
   160   This fact may be split up into two inequalities (merely using transitivity
   161   of \<open>\<subseteq>\<close>, which is an instance of the overloaded \<open>\<le>\<close> in Isabelle/HOL).
   162 \<close>
   163 
   164 lemma AG_fp_1: "\<^bold>A\<^bold>G p \<subseteq> p"
   165 proof -
   166   note AG_fp also have "p \<inter> \<^bold>A\<^bold>X \<^bold>A\<^bold>G p \<subseteq> p" by auto
   167   finally show ?thesis .
   168 qed
   169 
   170 lemma AG_fp_2: "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>X \<^bold>A\<^bold>G p"
   171 proof -
   172   note AG_fp also have "p \<inter> \<^bold>A\<^bold>X \<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>X \<^bold>A\<^bold>G p" by auto
   173   finally show ?thesis .
   174 qed
   175 
   176 text \<open>
   177   On the other hand, we have from the Knaster-Tarski fixed point theorem that
   178   any other post-fixed point of @{term "\<lambda>s. p \<inter> \<^bold>A\<^bold>X s"} is smaller than
   179   @{term "\<^bold>A\<^bold>G p"}. A post-fixed point is a set of states \<open>q\<close> such that @{term
   180   "q \<subseteq> p \<inter> \<^bold>A\<^bold>X q"}. This leads to the following co-induction principle for
   181   @{term "\<^bold>A\<^bold>G p"}.
   182 \<close>
   183 
   184 lemma AG_I: "q \<subseteq> p \<inter> \<^bold>A\<^bold>X q \<Longrightarrow> q \<subseteq> \<^bold>A\<^bold>G p"
   185   by (simp only: AG_gfp) (rule gfp_upperbound)
   186 
   187 
   188 subsection \<open>The tree induction principle \label{sec:calc-ctl-tree-induct}\<close>
   189 
   190 text \<open>
   191   With the most basic facts available, we are now able to establish a few more
   192   interesting results, leading to the \<^emph>\<open>tree induction\<close> principle for \<open>\<^bold>A\<^bold>G\<close>
   193   (see below). We will use some elementary monotonicity and distributivity
   194   rules.
   195 \<close>
   196 
   197 lemma AX_int: "\<^bold>A\<^bold>X (p \<inter> q) = \<^bold>A\<^bold>X p \<inter> \<^bold>A\<^bold>X q" by auto
   198 lemma AX_mono: "p \<subseteq> q \<Longrightarrow> \<^bold>A\<^bold>X p \<subseteq> \<^bold>A\<^bold>X q" by auto
   199 lemma AG_mono: "p \<subseteq> q \<Longrightarrow> \<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>G q"
   200   by (simp only: AG_gfp, rule gfp_mono) auto
   201 
   202 text \<open>
   203   The formula @{term "AG p"} implies @{term "AX p"} (we use substitution of
   204   \<open>\<subseteq>\<close> with monotonicity).
   205 \<close>
   206 
   207 lemma AG_AX: "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>X p"
   208 proof -
   209   have "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>X \<^bold>A\<^bold>G p" by (rule AG_fp_2)
   210   also have "\<^bold>A\<^bold>G p \<subseteq> p" by (rule AG_fp_1)
   211   moreover note AX_mono
   212   finally show ?thesis .
   213 qed
   214 
   215 text \<open>
   216   Furthermore we show idempotency of the \<open>\<^bold>A\<^bold>G\<close> operator. The proof is a good
   217   example of how accumulated facts may get used to feed a single rule step.
   218 \<close>
   219 
   220 lemma AG_AG: "\<^bold>A\<^bold>G \<^bold>A\<^bold>G p = \<^bold>A\<^bold>G p"
   221 proof
   222   show "\<^bold>A\<^bold>G \<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>G p" by (rule AG_fp_1)
   223 next
   224   show "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>G \<^bold>A\<^bold>G p"
   225   proof (rule AG_I)
   226     have "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>G p" ..
   227     moreover have "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>X \<^bold>A\<^bold>G p" by (rule AG_fp_2)
   228     ultimately show "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>G p \<inter> \<^bold>A\<^bold>X \<^bold>A\<^bold>G p" ..
   229   qed
   230 qed
   231 
   232 text \<open>
   233   \<^smallskip>
   234   We now give an alternative characterization of the \<open>\<^bold>A\<^bold>G\<close> operator, which
   235   describes the \<open>\<^bold>A\<^bold>G\<close> operator in an ``operational'' way by tree induction:
   236   In a state holds @{term "AG p"} iff in that state holds \<open>p\<close>, and in all
   237   reachable states \<open>s\<close> follows from the fact that \<open>p\<close> holds in \<open>s\<close>, that \<open>p\<close>
   238   also holds in all successor states of \<open>s\<close>. We use the co-induction principle
   239   @{thm [source] AG_I} to establish this in a purely algebraic manner.
   240 \<close>
   241 
   242 theorem AG_induct: "p \<inter> \<^bold>A\<^bold>G (p \<rightarrow> \<^bold>A\<^bold>X p) = \<^bold>A\<^bold>G p"
   243 proof
   244   show "p \<inter> \<^bold>A\<^bold>G (p \<rightarrow> \<^bold>A\<^bold>X p) \<subseteq> \<^bold>A\<^bold>G p"  (is "?lhs \<subseteq> _")
   245   proof (rule AG_I)
   246     show "?lhs \<subseteq> p \<inter> \<^bold>A\<^bold>X ?lhs"
   247     proof
   248       show "?lhs \<subseteq> p" ..
   249       show "?lhs \<subseteq> \<^bold>A\<^bold>X ?lhs"
   250       proof -
   251         {
   252           have "\<^bold>A\<^bold>G (p \<rightarrow> \<^bold>A\<^bold>X p) \<subseteq> p \<rightarrow> \<^bold>A\<^bold>X p" by (rule AG_fp_1)
   253           also have "p \<inter> p \<rightarrow> \<^bold>A\<^bold>X p \<subseteq> \<^bold>A\<^bold>X p" ..
   254           finally have "?lhs \<subseteq> \<^bold>A\<^bold>X p" by auto
   255         }
   256         moreover
   257         {
   258           have "p \<inter> \<^bold>A\<^bold>G (p \<rightarrow> \<^bold>A\<^bold>X p) \<subseteq> \<^bold>A\<^bold>G (p \<rightarrow> \<^bold>A\<^bold>X p)" ..
   259           also have "\<dots> \<subseteq> \<^bold>A\<^bold>X \<dots>" by (rule AG_fp_2)
   260           finally have "?lhs \<subseteq> \<^bold>A\<^bold>X \<^bold>A\<^bold>G (p \<rightarrow> \<^bold>A\<^bold>X p)" .
   261         }
   262         ultimately have "?lhs \<subseteq> \<^bold>A\<^bold>X p \<inter> \<^bold>A\<^bold>X \<^bold>A\<^bold>G (p \<rightarrow> \<^bold>A\<^bold>X p)" ..
   263         also have "\<dots> = \<^bold>A\<^bold>X ?lhs" by (simp only: AX_int)
   264         finally show ?thesis .
   265       qed
   266     qed
   267   qed
   268 next
   269   show "\<^bold>A\<^bold>G p \<subseteq> p \<inter> \<^bold>A\<^bold>G (p \<rightarrow> \<^bold>A\<^bold>X p)"
   270   proof
   271     show "\<^bold>A\<^bold>G p \<subseteq> p" by (rule AG_fp_1)
   272     show "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>G (p \<rightarrow> \<^bold>A\<^bold>X p)"
   273     proof -
   274       have "\<^bold>A\<^bold>G p = \<^bold>A\<^bold>G \<^bold>A\<^bold>G p" by (simp only: AG_AG)
   275       also have "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>X p" by (rule AG_AX) moreover note AG_mono
   276       also have "\<^bold>A\<^bold>X p \<subseteq> (p \<rightarrow> \<^bold>A\<^bold>X p)" .. moreover note AG_mono
   277       finally show ?thesis .
   278     qed
   279   qed
   280 qed
   281 
   282 
   283 subsection \<open>An application of tree induction \label{sec:calc-ctl-commute}\<close>
   284 
   285 text \<open>
   286   Further interesting properties of CTL expressions may be demonstrated with
   287   the help of tree induction; here we show that \<open>\<^bold>A\<^bold>X\<close> and \<open>\<^bold>A\<^bold>G\<close> commute.
   288 \<close>
   289 
   290 theorem AG_AX_commute: "\<^bold>A\<^bold>G \<^bold>A\<^bold>X p = \<^bold>A\<^bold>X \<^bold>A\<^bold>G p"
   291 proof -
   292   have "\<^bold>A\<^bold>G \<^bold>A\<^bold>X p = \<^bold>A\<^bold>X p \<inter> \<^bold>A\<^bold>X \<^bold>A\<^bold>G \<^bold>A\<^bold>X p" by (rule AG_fp)
   293   also have "\<dots> = \<^bold>A\<^bold>X (p \<inter> \<^bold>A\<^bold>G \<^bold>A\<^bold>X p)" by (simp only: AX_int)
   294   also have "p \<inter> \<^bold>A\<^bold>G \<^bold>A\<^bold>X p = \<^bold>A\<^bold>G p"  (is "?lhs = _")
   295   proof
   296     have "\<^bold>A\<^bold>X p \<subseteq> p \<rightarrow> \<^bold>A\<^bold>X p" ..
   297     also have "p \<inter> \<^bold>A\<^bold>G (p \<rightarrow> \<^bold>A\<^bold>X p) = \<^bold>A\<^bold>G p" by (rule AG_induct)
   298     also note Int_mono AG_mono
   299     ultimately show "?lhs \<subseteq> \<^bold>A\<^bold>G p" by fast
   300   next
   301     have "\<^bold>A\<^bold>G p \<subseteq> p" by (rule AG_fp_1)
   302     moreover
   303     {
   304       have "\<^bold>A\<^bold>G p = \<^bold>A\<^bold>G \<^bold>A\<^bold>G p" by (simp only: AG_AG)
   305       also have "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>X p" by (rule AG_AX)
   306       also note AG_mono
   307       ultimately have "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>G \<^bold>A\<^bold>X p" .
   308     }
   309     ultimately show "\<^bold>A\<^bold>G p \<subseteq> ?lhs" ..
   310   qed
   311   finally show ?thesis .
   312 qed
   313 
   314 end