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