src/HOL/ex/CTL.thy
 author obua Mon Apr 10 16:00:34 2006 +0200 (2006-04-10) changeset 19404 9bf2cdc9e8e8 parent 17388 495c799df31d child 20807 bd3b60f9a343 permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
1 (*  Title:      HOL/ex/CTL.thy
2     ID:         $Id$
3     Author:     Gertrud Bauer
4 *)
6 header {* CTL formulae *}
8 theory CTL imports Main begin
10 text {*
11   We formalize basic concepts of Computational Tree Logic (CTL)
12   \cite{McMillan-PhDThesis,McMillan-LectureNotes} within the
13   simply-typed set theory of HOL.
15   By using the common technique of shallow embedding'', a CTL
16   formula is identified with the corresponding set of states where it
17   holds.  Consequently, CTL operations such as negation, conjunction,
18   disjunction simply become complement, intersection, union of sets.
19   We only require a separate operation for implication, as point-wise
20   inclusion is usually not encountered in plain set-theory.
21 *}
23 lemmas [intro!] = Int_greatest Un_upper2 Un_upper1 Int_lower1 Int_lower2
25 types 'a ctl = "'a set"
26 constdefs
27   imp :: "'a ctl \<Rightarrow> 'a ctl \<Rightarrow> 'a ctl"    (infixr "\<rightarrow>" 75)
28   "p \<rightarrow> q \<equiv> - p \<union> q"
30 lemma [intro!]: "p \<inter> p \<rightarrow> q \<subseteq> q" by (unfold imp_def) auto
31 lemma [intro!]: "p \<subseteq> (q \<rightarrow> p)" by (unfold imp_def) 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 consts model :: "('a \<times> 'a) set"    ("\<M>")
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 constdefs
60   EX :: "'a ctl \<Rightarrow> 'a ctl"    ("\<EX> _" [80] 90)    "\<EX> p \<equiv> {s. \<exists>s'. (s, s') \<in> \<M> \<and> s' \<in> p}"
61   EF :: "'a ctl \<Rightarrow> 'a ctl"    ("\<EF> _" [80] 90)    "\<EF> p \<equiv> lfp (\<lambda>s. p \<union> \<EX> s)"
62   EG :: "'a ctl \<Rightarrow> 'a ctl"    ("\<EG> _" [80] 90)    "\<EG> p \<equiv> gfp (\<lambda>s. p \<inter> \<EX> s)"
64 text {*
65   @{text "\<AX>"}, @{text "\<AF>"} and @{text "\<AG>"} are now defined
66   dually in terms of @{text "\<EX>"}, @{text "\<EF>"} and @{text
67   "\<EG>"}.
68 *}
70 constdefs
71   AX :: "'a ctl \<Rightarrow> 'a ctl"    ("\<AX> _" [80] 90)    "\<AX> p \<equiv> - \<EX> - p"
72   AF :: "'a ctl \<Rightarrow> 'a ctl"    ("\<AF> _" [80] 90)    "\<AF> p \<equiv> - \<EG> - p"
73   AG :: "'a ctl \<Rightarrow> 'a ctl"    ("\<AG> _" [80] 90)    "\<AG> p \<equiv> - \<EF> - p"
75 lemmas [simp] = EX_def EG_def AX_def EF_def AF_def AG_def
78 section {* Basic fixed point properties *}
80 text {*
81   First of all, we use the de-Morgan property of fixed points
82 *}
84 lemma lfp_gfp: "lfp f = - gfp (\<lambda>s . - (f (- s)))"
85 proof
86   show "lfp f \<subseteq> - gfp (\<lambda>s. - f (- s))"
87   proof
88     fix x assume l: "x \<in> lfp f"
89     show "x \<in> - gfp (\<lambda>s. - f (- s))"
90     proof
91       assume "x \<in> gfp (\<lambda>s. - f (- s))"
92       then obtain u where "x \<in> u" and "u \<subseteq> - f (- u)" by (unfold gfp_def) auto
93       then have "f (- u) \<subseteq> - u" by auto
94       then have "lfp f \<subseteq> - u" by (rule lfp_lowerbound)
95       from l and this have "x \<notin> u" by auto
96       then show False by contradiction
97     qed
98   qed
99   show "- gfp (\<lambda>s. - f (- s)) \<subseteq> lfp f"
100   proof (rule lfp_greatest)
101     fix u assume "f u \<subseteq> u"
102     then have "- u \<subseteq> - f u" by auto
103     then have "- u \<subseteq> - f (- (- u))" by simp
104     then have "- u \<subseteq> gfp (\<lambda>s. - f (- s))" by (rule gfp_upperbound)
105     then show "- gfp (\<lambda>s. - f (- s)) \<subseteq> u" by auto
106   qed
107 qed
109 lemma lfp_gfp': "- lfp f = gfp (\<lambda>s. - (f (- s)))"
112 lemma gfp_lfp': "- gfp f = lfp (\<lambda>s. - (f (- s)))"
115 text {*
116   in order to give dual fixed point representations of @{term "AF p"}
117   and @{term "AG p"}:
118 *}
120 lemma AF_lfp: "\<AF> p = lfp (\<lambda>s. p \<union> \<AX> s)" by (simp add: lfp_gfp)
121 lemma AG_gfp: "\<AG> p = gfp (\<lambda>s. p \<inter> \<AX> s)" by (simp add: lfp_gfp)
123 lemma EF_fp: "\<EF> p = p \<union> \<EX> \<EF> p"
124 proof -
125   have "mono (\<lambda>s. p \<union> \<EX> s)" by rule (auto simp add: EX_def)
126   then show ?thesis by (simp only: EF_def) (rule lfp_unfold)
127 qed
129 lemma AF_fp: "\<AF> p = p \<union> \<AX> \<AF> p"
130 proof -
131   have "mono (\<lambda>s. p \<union> \<AX> s)" by rule (auto simp add: AX_def EX_def)
132   then show ?thesis by (simp only: AF_lfp) (rule lfp_unfold)
133 qed
135 lemma EG_fp: "\<EG> p = p \<inter> \<EX> \<EG> p"
136 proof -
137   have "mono (\<lambda>s. p \<inter> \<EX> s)" by rule (auto simp add: EX_def)
138   then show ?thesis by (simp only: EG_def) (rule gfp_unfold)
139 qed
141 text {*
142   From the greatest fixed point definition of @{term "\<AG> p"}, we
143   derive as a consequence of the Knaster-Tarski theorem on the one
144   hand that @{term "\<AG> p"} is a fixed point of the monotonic
145   function @{term "\<lambda>s. p \<inter> \<AX> s"}.
146 *}
148 lemma AG_fp: "\<AG> p = p \<inter> \<AX> \<AG> p"
149 proof -
150   have "mono (\<lambda>s. p \<inter> \<AX> s)" by rule (auto simp add: AX_def EX_def)
151   then show ?thesis by (simp only: AG_gfp) (rule gfp_unfold)
152 qed
154 text {*
155   This fact may be split up into two inequalities (merely using
156   transitivity of @{text "\<subseteq>" }, which is an instance of the overloaded
157   @{text "\<le>"} in Isabelle/HOL).
158 *}
160 lemma AG_fp_1: "\<AG> p \<subseteq> p"
161 proof -
162   note AG_fp also have "p \<inter> \<AX> \<AG> p \<subseteq> p" by auto
163   finally show ?thesis .
164 qed
166 text {**}
168 lemma AG_fp_2: "\<AG> p \<subseteq> \<AX> \<AG> p"
169 proof -
170   note AG_fp also have "p \<inter> \<AX> \<AG> p \<subseteq> \<AX> \<AG> p" by auto
171   finally show ?thesis .
172 qed
174 text {*
175   On the other hand, we have from the Knaster-Tarski fixed point
176   theorem that any other post-fixed point of @{term "\<lambda>s. p \<inter> AX s"} is
177   smaller than @{term "AG p"}.  A post-fixed point is a set of states
178   @{term q} such that @{term "q \<subseteq> p \<inter> AX q"}.  This leads to the
179   following co-induction principle for @{term "AG p"}.
180 *}
182 lemma AG_I: "q \<subseteq> p \<inter> \<AX> q \<Longrightarrow> q \<subseteq> \<AG> p"
183   by (simp only: AG_gfp) (rule gfp_upperbound)
186 section {* The tree induction principle \label{sec:calc-ctl-tree-induct} *}
188 text {*
189   With the most basic facts available, we are now able to establish a
190   few more interesting results, leading to the \emph{tree induction}
191   principle for @{text AG} (see below).  We will use some elementary
192   monotonicity and distributivity rules.
193 *}
195 lemma AX_int: "\<AX> (p \<inter> q) = \<AX> p \<inter> \<AX> q" by auto
196 lemma AX_mono: "p \<subseteq> q \<Longrightarrow> \<AX> p \<subseteq> \<AX> q" by auto
197 lemma AG_mono: "p \<subseteq> q \<Longrightarrow> \<AG> p \<subseteq> \<AG> q"
198   by (simp only: AG_gfp, rule gfp_mono) auto
200 text {*
201   The formula @{term "AG p"} implies @{term "AX p"} (we use
202   substitution of @{text "\<subseteq>"} with monotonicity).
203 *}
205 lemma AG_AX: "\<AG> p \<subseteq> \<AX> p"
206 proof -
207   have "\<AG> p \<subseteq> \<AX> \<AG> p" by (rule AG_fp_2)
208   also have "\<AG> p \<subseteq> p" by (rule AG_fp_1) moreover note AX_mono
209   finally show ?thesis .
210 qed
212 text {*
213   Furthermore we show idempotency of the @{text "\<AG>"} operator.
214   The proof is a good example of how accumulated facts may get
215   used to feed a single rule step.
216 *}
218 lemma AG_AG: "\<AG> \<AG> p = \<AG> p"
219 proof
220   show "\<AG> \<AG> p \<subseteq> \<AG> p" by (rule AG_fp_1)
221 next
222   show "\<AG> p \<subseteq> \<AG> \<AG> p"
223   proof (rule AG_I)
224     have "\<AG> p \<subseteq> \<AG> p" ..
225     moreover have "\<AG> p \<subseteq> \<AX> \<AG> p" by (rule AG_fp_2)
226     ultimately show "\<AG> p \<subseteq> \<AG> p \<inter> \<AX> \<AG> p" ..
227   qed
228 qed
230 text {*
231   \smallskip We now give an alternative characterization of the @{text
232   "\<AG>"} operator, which describes the @{text "\<AG>"} operator in
233   an operational'' way by tree induction: In a state holds @{term
234   "AG p"} iff in that state holds @{term p}, and in all reachable
235   states @{term s} follows from the fact that @{term p} holds in
236   @{term s}, that @{term p} also holds in all successor states of
237   @{term s}.  We use the co-induction principle @{thm [source] AG_I}
238   to establish this in a purely algebraic manner.
239 *}
241 theorem AG_induct: "p \<inter> \<AG> (p \<rightarrow> \<AX> p) = \<AG> p"
242 proof
243   show "p \<inter> \<AG> (p \<rightarrow> \<AX> p) \<subseteq> \<AG> p"  (is "?lhs \<subseteq> _")
244   proof (rule AG_I)
245     show "?lhs \<subseteq> p \<inter> \<AX> ?lhs"
246     proof
247       show "?lhs \<subseteq> p" ..
248       show "?lhs \<subseteq> \<AX> ?lhs"
249       proof -
250 	{
251 	  have "\<AG> (p \<rightarrow> \<AX> p) \<subseteq> p \<rightarrow> \<AX> p" by (rule AG_fp_1)
252           also have "p \<inter> p \<rightarrow> \<AX> p \<subseteq> \<AX> p" ..
253           finally have "?lhs \<subseteq> \<AX> p" by auto
254 	}
255 	moreover
256 	{
257 	  have "p \<inter> \<AG> (p \<rightarrow> \<AX> p) \<subseteq> \<AG> (p \<rightarrow> \<AX> p)" ..
258           also have "\<dots> \<subseteq> \<AX> \<dots>" by (rule AG_fp_2)
259           finally have "?lhs \<subseteq> \<AX> \<AG> (p \<rightarrow> \<AX> p)" .
260 	}
261 	ultimately have "?lhs \<subseteq> \<AX> p \<inter> \<AX> \<AG> (p \<rightarrow> \<AX> p)" ..
262 	also have "\<dots> = \<AX> ?lhs" by (simp only: AX_int)
263 	finally show ?thesis .
264       qed
265     qed
266   qed
267 next
268   show "\<AG> p \<subseteq> p \<inter> \<AG> (p \<rightarrow> \<AX> p)"
269   proof
270     show "\<AG> p \<subseteq> p" by (rule AG_fp_1)
271     show "\<AG> p \<subseteq> \<AG> (p \<rightarrow> \<AX> p)"
272     proof -
273       have "\<AG> p = \<AG> \<AG> p" by (simp only: AG_AG)
274       also have "\<AG> p \<subseteq> \<AX> p" by (rule AG_AX) moreover note AG_mono
275       also have "\<AX> p \<subseteq> (p \<rightarrow> \<AX> p)" .. moreover note AG_mono
276       finally show ?thesis .
277     qed
278   qed
279 qed
282 section {* An application of tree induction \label{sec:calc-ctl-commute} *}
284 text {*
285   Further interesting properties of CTL expressions may be
286   demonstrated with the help of tree induction; here we show that
287   @{text \<AX>} and @{text \<AG>} commute.
288 *}
290 theorem AG_AX_commute: "\<AG> \<AX> p = \<AX> \<AG> p"
291 proof -
292   have "\<AG> \<AX> p = \<AX> p \<inter> \<AX> \<AG> \<AX> p" by (rule AG_fp)
293   also have "\<dots> = \<AX> (p \<inter> \<AG> \<AX> p)" by (simp only: AX_int)
294   also have "p \<inter> \<AG> \<AX> p = \<AG> p"  (is "?lhs = _")
295   proof
296     have "\<AX> p \<subseteq> p \<rightarrow> \<AX> p" ..
297     also have "p \<inter> \<AG> (p \<rightarrow> \<AX> p) = \<AG> p" by (rule AG_induct)
298     also note Int_mono AG_mono
299     ultimately show "?lhs \<subseteq> \<AG> p" by fast
300   next
301     have "\<AG> p \<subseteq> p" by (rule AG_fp_1)
302     moreover
303     {
304       have "\<AG> p = \<AG> \<AG> p" by (simp only: AG_AG)
305       also have "\<AG> p \<subseteq> \<AX> p" by (rule AG_AX)
306       also note AG_mono
307       ultimately have "\<AG> p \<subseteq> \<AG> \<AX> p" .
308     }
309     ultimately show "\<AG> p \<subseteq> ?lhs" ..
310   qed
311   finally show ?thesis .
312 qed
314 end