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