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