1(*  Title:      HOL/ex/CTL.thy
2    Author:     Gertrud Bauer
3*)
4
5section \<open>CTL formulae\<close>
6
7theory CTL
8imports Main
9begin
10
11text \<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
24lemmas [intro!] = Int_greatest Un_upper2 Un_upper1 Int_lower1 Int_lower2
25
26type_synonym 'a ctl = "'a set"
27
28definition imp :: "'a ctl \<Rightarrow> 'a ctl \<Rightarrow> 'a ctl"  (infixr "\<rightarrow>" 75)
29  where "p \<rightarrow> q = - p \<union> q"
30
31lemma [intro!]: "p \<inter> p \<rightarrow> q \<subseteq> q" unfolding imp_def by auto
32lemma [intro!]: "p \<subseteq> (q \<rightarrow> p)" unfolding imp_def by rule
33
34
35text \<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>\<open>'a\<close>.
40\<close>
41
42axiomatization \<M> :: "('a \<times> 'a) set"
43
44text \<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
57definition EX  ("\<^bold>E\<^bold>X _" [80] 90)
58  where [simp]: "\<^bold>E\<^bold>X p = {s. \<exists>s'. (s, s') \<in> \<M> \<and> s' \<in> p}"
59
60definition EF ("\<^bold>E\<^bold>F _" [80] 90)
61  where [simp]: "\<^bold>E\<^bold>F p = lfp (\<lambda>s. p \<union> \<^bold>E\<^bold>X s)"
62
63definition EG ("\<^bold>E\<^bold>G _" [80] 90)
64  where [simp]: "\<^bold>E\<^bold>G p = gfp (\<lambda>s. p \<inter> \<^bold>E\<^bold>X s)"
65
66text \<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
71definition AX  ("\<^bold>A\<^bold>X _" [80] 90)
72  where [simp]: "\<^bold>A\<^bold>X p = - \<^bold>E\<^bold>X - p"
73definition AF  ("\<^bold>A\<^bold>F _" [80] 90)
74  where [simp]: "\<^bold>A\<^bold>F p = - \<^bold>E\<^bold>G - p"
75definition AG  ("\<^bold>A\<^bold>G _" [80] 90)
76  where [simp]: "\<^bold>A\<^bold>G p = - \<^bold>E\<^bold>F - p"
77
78
79subsection \<open>Basic fixed point properties\<close>
80
81text \<open>
82  First of all, we use the de-Morgan property of fixed points.
83\<close>
84
85lemma lfp_gfp: "lfp f = - gfp (\<lambda>s::'a set. - (f (- s)))"
86proof
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
109qed
110
111lemma lfp_gfp': "- lfp f = gfp (\<lambda>s::'a set. - (f (- s)))"
112  by (simp add: lfp_gfp)
113
114lemma gfp_lfp': "- gfp f = lfp (\<lambda>s::'a set. - (f (- s)))"
115  by (simp add: lfp_gfp)
116
117text \<open>
118  In order to give dual fixed point representations of \<^term>\<open>\<^bold>A\<^bold>F p\<close> and
119  \<^term>\<open>\<^bold>A\<^bold>G p\<close>:
120\<close>
121
122lemma AF_lfp: "\<^bold>A\<^bold>F p = lfp (\<lambda>s. p \<union> \<^bold>A\<^bold>X s)"
123  by (simp add: lfp_gfp)
124
125lemma AG_gfp: "\<^bold>A\<^bold>G p = gfp (\<lambda>s. p \<inter> \<^bold>A\<^bold>X s)"
126  by (simp add: lfp_gfp)
127
128lemma EF_fp: "\<^bold>E\<^bold>F p = p \<union> \<^bold>E\<^bold>X \<^bold>E\<^bold>F p"
129proof -
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)
132qed
133
134lemma AF_fp: "\<^bold>A\<^bold>F p = p \<union> \<^bold>A\<^bold>X \<^bold>A\<^bold>F p"
135proof -
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)
138qed
139
140lemma EG_fp: "\<^bold>E\<^bold>G p = p \<inter> \<^bold>E\<^bold>X \<^bold>E\<^bold>G p"
141proof -
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)
144qed
145
146text \<open>
147  From the greatest fixed point definition of \<^term>\<open>\<^bold>A\<^bold>G p\<close>, we derive as
148  a consequence of the Knaster-Tarski theorem on the one hand that \<^term>\<open>\<^bold>A\<^bold>G p\<close> is a fixed point of the monotonic function
149  \<^term>\<open>\<lambda>s. p \<inter> \<^bold>A\<^bold>X s\<close>.
150\<close>
151
152lemma AG_fp: "\<^bold>A\<^bold>G p = p \<inter> \<^bold>A\<^bold>X \<^bold>A\<^bold>G p"
153proof -
154  have "mono (\<lambda>s. p \<inter> \<^bold>A\<^bold>X s)" by rule auto
155  then show ?thesis by (simp only: AG_gfp) (rule gfp_unfold)
156qed
157
158text \<open>
159  This fact may be split up into two inequalities (merely using transitivity
160  of \<open>\<subseteq>\<close>, which is an instance of the overloaded \<open>\<le>\<close> in Isabelle/HOL).
161\<close>
162
163lemma AG_fp_1: "\<^bold>A\<^bold>G p \<subseteq> p"
164proof -
165  note AG_fp also have "p \<inter> \<^bold>A\<^bold>X \<^bold>A\<^bold>G p \<subseteq> p" by auto
166  finally show ?thesis .
167qed
168
169lemma AG_fp_2: "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>X \<^bold>A\<^bold>G p"
170proof -
171  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
172  finally show ?thesis .
173qed
174
175text \<open>
176  On the other hand, we have from the Knaster-Tarski fixed point theorem that
177  any other post-fixed point of \<^term>\<open>\<lambda>s. p \<inter> \<^bold>A\<^bold>X s\<close> is smaller than
178  \<^term>\<open>\<^bold>A\<^bold>G p\<close>. A post-fixed point is a set of states \<open>q\<close> such that \<^term>\<open>q \<subseteq> p \<inter> \<^bold>A\<^bold>X q\<close>. This leads to the following co-induction principle for
179  \<^term>\<open>\<^bold>A\<^bold>G p\<close>.
180\<close>
181
182lemma AG_I: "q \<subseteq> p \<inter> \<^bold>A\<^bold>X q \<Longrightarrow> q \<subseteq> \<^bold>A\<^bold>G p"
183  by (simp only: AG_gfp) (rule gfp_upperbound)
184
185
186subsection \<open>The tree induction principle \label{sec:calc-ctl-tree-induct}\<close>
187
188text \<open>
189  With the most basic facts available, we are now able to establish a few more
190  interesting results, leading to the \<^emph>\<open>tree induction\<close> principle for \<open>\<^bold>A\<^bold>G\<close>
191  (see below). We will use some elementary monotonicity and distributivity
192  rules.
193\<close>
194
195lemma AX_int: "\<^bold>A\<^bold>X (p \<inter> q) = \<^bold>A\<^bold>X p \<inter> \<^bold>A\<^bold>X q" by auto
196lemma AX_mono: "p \<subseteq> q \<Longrightarrow> \<^bold>A\<^bold>X p \<subseteq> \<^bold>A\<^bold>X q" by auto
197lemma AG_mono: "p \<subseteq> q \<Longrightarrow> \<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>G q"
198  by (simp only: AG_gfp, rule gfp_mono) auto
199
200text \<open>
201  The formula \<^term>\<open>AG p\<close> implies \<^term>\<open>AX p\<close> (we use substitution of
202  \<open>\<subseteq>\<close> with monotonicity).
203\<close>
204
205lemma AG_AX: "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>X p"
206proof -
207  have "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>X \<^bold>A\<^bold>G p" by (rule AG_fp_2)
208  also have "\<^bold>A\<^bold>G p \<subseteq> p" by (rule AG_fp_1)
209  moreover note AX_mono
210  finally show ?thesis .
211qed
212
213text \<open>
214  Furthermore we show idempotency of the \<open>\<^bold>A\<^bold>G\<close> operator. The proof is a good
215  example of how accumulated facts may get used to feed a single rule step.
216\<close>
217
218lemma AG_AG: "\<^bold>A\<^bold>G \<^bold>A\<^bold>G p = \<^bold>A\<^bold>G p"
219proof
220  show "\<^bold>A\<^bold>G \<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>G p" by (rule AG_fp_1)
221next
222  show "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>G \<^bold>A\<^bold>G p"
223  proof (rule AG_I)
224    have "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>G p" ..
225    moreover have "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>X \<^bold>A\<^bold>G p" by (rule AG_fp_2)
226    ultimately show "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>G p \<inter> \<^bold>A\<^bold>X \<^bold>A\<^bold>G p" ..
227  qed
228qed
229
230text \<open>
231  \<^smallskip>
232  We now give an alternative characterization of the \<open>\<^bold>A\<^bold>G\<close> operator, which
233  describes the \<open>\<^bold>A\<^bold>G\<close> operator in an ``operational'' way by tree induction:
234  In a state holds \<^term>\<open>AG p\<close> iff in that state holds \<open>p\<close>, and in all
235  reachable states \<open>s\<close> follows from the fact that \<open>p\<close> holds in \<open>s\<close>, that \<open>p\<close>
236  also holds in all successor states of \<open>s\<close>. We use the co-induction principle
237  @{thm [source] AG_I} to establish this in a purely algebraic manner.
238\<close>
239
240theorem AG_induct: "p \<inter> \<^bold>A\<^bold>G (p \<rightarrow> \<^bold>A\<^bold>X p) = \<^bold>A\<^bold>G p"
241proof
242  show "p \<inter> \<^bold>A\<^bold>G (p \<rightarrow> \<^bold>A\<^bold>X p) \<subseteq> \<^bold>A\<^bold>G p"  (is "?lhs \<subseteq> _")
243  proof (rule AG_I)
244    show "?lhs \<subseteq> p \<inter> \<^bold>A\<^bold>X ?lhs"
245    proof
246      show "?lhs \<subseteq> p" ..
247      show "?lhs \<subseteq> \<^bold>A\<^bold>X ?lhs"
248      proof -
249        {
250          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)
251          also have "p \<inter> p \<rightarrow> \<^bold>A\<^bold>X p \<subseteq> \<^bold>A\<^bold>X p" ..
252          finally have "?lhs \<subseteq> \<^bold>A\<^bold>X p" by auto
253        }
254        moreover
255        {
256          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)" ..
257          also have "\<dots> \<subseteq> \<^bold>A\<^bold>X \<dots>" by (rule AG_fp_2)
258          finally have "?lhs \<subseteq> \<^bold>A\<^bold>X \<^bold>A\<^bold>G (p \<rightarrow> \<^bold>A\<^bold>X p)" .
259        }
260        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)" ..
261        also have "\<dots> = \<^bold>A\<^bold>X ?lhs" by (simp only: AX_int)
262        finally show ?thesis .
263      qed
264    qed
265  qed
266next
267  show "\<^bold>A\<^bold>G p \<subseteq> p \<inter> \<^bold>A\<^bold>G (p \<rightarrow> \<^bold>A\<^bold>X p)"
268  proof
269    show "\<^bold>A\<^bold>G p \<subseteq> p" by (rule AG_fp_1)
270    show "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>G (p \<rightarrow> \<^bold>A\<^bold>X p)"
271    proof -
272      have "\<^bold>A\<^bold>G p = \<^bold>A\<^bold>G \<^bold>A\<^bold>G p" by (simp only: AG_AG)
273      also have "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>X p" by (rule AG_AX) moreover note AG_mono
274      also have "\<^bold>A\<^bold>X p \<subseteq> (p \<rightarrow> \<^bold>A\<^bold>X p)" .. moreover note AG_mono
275      finally show ?thesis .
276    qed
277  qed
278qed
279
280
281subsection \<open>An application of tree induction \label{sec:calc-ctl-commute}\<close>
282
283text \<open>
284  Further interesting properties of CTL expressions may be demonstrated with
285  the help of tree induction; here we show that \<open>\<^bold>A\<^bold>X\<close> and \<open>\<^bold>A\<^bold>G\<close> commute.
286\<close>
287
288theorem AG_AX_commute: "\<^bold>A\<^bold>G \<^bold>A\<^bold>X p = \<^bold>A\<^bold>X \<^bold>A\<^bold>G p"
289proof -
290  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)
291  also have "\<dots> = \<^bold>A\<^bold>X (p \<inter> \<^bold>A\<^bold>G \<^bold>A\<^bold>X p)" by (simp only: AX_int)
292  also have "p \<inter> \<^bold>A\<^bold>G \<^bold>A\<^bold>X p = \<^bold>A\<^bold>G p"  (is "?lhs = _")
293  proof
294    have "\<^bold>A\<^bold>X p \<subseteq> p \<rightarrow> \<^bold>A\<^bold>X p" ..
295    also have "p \<inter> \<^bold>A\<^bold>G (p \<rightarrow> \<^bold>A\<^bold>X p) = \<^bold>A\<^bold>G p" by (rule AG_induct)
296    also note Int_mono AG_mono
297    ultimately show "?lhs \<subseteq> \<^bold>A\<^bold>G p" by fast
298  next
299    have "\<^bold>A\<^bold>G p \<subseteq> p" by (rule AG_fp_1)
300    moreover
301    {
302      have "\<^bold>A\<^bold>G p = \<^bold>A\<^bold>G \<^bold>A\<^bold>G p" by (simp only: AG_AG)
303      also have "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>X p" by (rule AG_AX)
304      also note AG_mono
305      ultimately have "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>G \<^bold>A\<^bold>X p" .
306    }
307    ultimately show "\<^bold>A\<^bold>G p \<subseteq> ?lhs" ..
308  qed
309  finally show ?thesis .
310qed
311
312end
313