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