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