src/HOL/ex/CTL.thy
 author huffman Fri Aug 19 14:17:28 2011 -0700 (2011-08-19) changeset 44311 42c5cbf68052 parent 42463 f270e3e18be5 child 46008 c296c75f4cf4 permissions -rw-r--r--
new isCont theorems;
simplify some proofs.
     1 (*  Title:      HOL/ex/CTL.thy

     2     Author:     Gertrud Bauer

     3 *)

     4

     5 header {* CTL formulae *}

     6

     7 theory CTL imports Main begin

     8

     9 text {*

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

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

    12   simply-typed set theory of HOL.

    13

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

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

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

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

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

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

    20 *}

    21

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

    23

    24 type_synonym 'a ctl = "'a set"

    25

    26 definition

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

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

    29

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

    31 lemma [intro!]: "p \<subseteq> (q \<rightarrow> p)" unfolding imp_def by 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 axiomatization \<M> :: "('a \<times> 'a) set"

    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 definition

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

    61 definition

    62   EF ("\<EF> _"  90)  where "\<EF> p = lfp (\<lambda>s. p \<union> \<EX> s)"

    63 definition

    64   EG ("\<EG> _"  90)  where "\<EG> p = gfp (\<lambda>s. p \<inter> \<EX> s)"

    65

    66 text {*

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

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

    69   "\<EG>"}.

    70 *}

    71

    72 definition

    73   AX  ("\<AX> _"  90) where "\<AX> p = - \<EX> - p"

    74 definition

    75   AF  ("\<AF> _"  90) where "\<AF> p = - \<EG> - p"

    76 definition

    77   AG  ("\<AG> _"  90) where "\<AG> p = - \<EF> - p"

    78

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

    80

    81

    82 subsection {* Basic fixed point properties *}

    83

    84 text {*

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

    86 *}

    87

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

    89 proof

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

    91   proof

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

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

    94     proof

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

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

    97         by (auto simp add: gfp_def)

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

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

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

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

   102     qed

   103   qed

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

   105   proof (rule lfp_greatest)

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

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

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

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

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

   111   qed

   112 qed

   113

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

   115   by (simp add: lfp_gfp)

   116

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

   118   by (simp add: lfp_gfp)

   119

   120 text {*

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

   122   and @{term "AG p"}:

   123 *}

   124

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

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

   127

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

   129 proof -

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

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

   132 qed

   133

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

   135 proof -

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

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

   138 qed

   139

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

   141 proof -

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

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

   144 qed

   145

   146 text {*

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

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

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

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

   151 *}

   152

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

   154 proof -

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

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

   157 qed

   158

   159 text {*

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

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

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

   163 *}

   164

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

   166 proof -

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

   168   finally show ?thesis .

   169 qed

   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 subsection {* 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           moreover have "p \<inter> p \<rightarrow> \<AX> p \<subseteq> \<AX> p" ..

   256           ultimately 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           by (rule Int_greatest)

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

   267         finally show ?thesis .

   268       qed

   269     qed

   270   qed

   271 next

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

   273   proof

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

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

   276     proof -

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

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

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

   280       finally show ?thesis .

   281     qed

   282   qed

   283 qed

   284

   285

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

   287

   288 text {*

   289   Further interesting properties of CTL expressions may be

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

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

   292 *}

   293

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

   295 proof -

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

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

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

   299   proof

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

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

   302     also note Int_mono AG_mono

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

   304   next

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

   306     moreover

   307     {

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

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

   310       also note AG_mono

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

   312     }

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

   314   qed

   315   finally show ?thesis .

   316 qed

   317

   318 end