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 _"  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 _"  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 _"  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 _"  90)

    72   where [simp]: "\<^bold>A\<^bold>X p = - \<^bold>E\<^bold>X - p"

    73 definition AF  ("\<^bold>A\<^bold>F _"  90)

    74   where [simp]: "\<^bold>A\<^bold>F p = - \<^bold>E\<^bold>G - p"

    75 definition AG  ("\<^bold>A\<^bold>G _"  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