1.1 --- a/src/HOL/CTL/CTL.thy Thu Apr 28 12:04:34 2005 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,310 +0,0 @@
1.4 -
1.5 -theory CTL = Main:
1.6 -
1.7 -section {* CTL formulae *}
1.8 -
1.9 -text {*
1.10 - We formalize basic concepts of Computational Tree Logic (CTL)
1.11 - \cite{McMillan-PhDThesis,McMillan-LectureNotes} within the
1.12 - simply-typed set theory of HOL.
1.13 -
1.14 - By using the common technique of ``shallow embedding'', a CTL
1.15 - formula is identified with the corresponding set of states where it
1.16 - holds. Consequently, CTL operations such as negation, conjunction,
1.17 - disjunction simply become complement, intersection, union of sets.
1.18 - We only require a separate operation for implication, as point-wise
1.19 - inclusion is usually not encountered in plain set-theory.
1.20 -*}
1.21 -
1.22 -lemmas [intro!] = Int_greatest Un_upper2 Un_upper1 Int_lower1 Int_lower2
1.23 -
1.24 -types 'a ctl = "'a set"
1.25 -constdefs
1.26 - imp :: "'a ctl \<Rightarrow> 'a ctl \<Rightarrow> 'a ctl" (infixr "\<rightarrow>" 75)
1.27 - "p \<rightarrow> q \<equiv> - p \<union> q"
1.28 -
1.29 -lemma [intro!]: "p \<inter> p \<rightarrow> q \<subseteq> q" by (unfold imp_def) auto
1.30 -lemma [intro!]: "p \<subseteq> (q \<rightarrow> p)" by (unfold imp_def) rule
1.31 -
1.32 -
1.33 -text {*
1.34 - \smallskip The CTL path operators are more interesting; they are
1.35 - based on an arbitrary, but fixed model @{text \<M>}, which is simply
1.36 - a transition relation over states @{typ "'a"}.
1.37 -*}
1.38 -
1.39 -consts model :: "('a \<times> 'a) set" ("\<M>")
1.40 -
1.41 -text {*
1.42 - The operators @{text \<EX>}, @{text \<EF>}, @{text \<EG>} are taken
1.43 - as primitives, while @{text \<AX>}, @{text \<AF>}, @{text \<AG>} are
1.44 - defined as derived ones. The formula @{text "\<EX> p"} holds in a
1.45 - state @{term s}, iff there is a successor state @{term s'} (with
1.46 - respect to the model @{term \<M>}), such that @{term p} holds in
1.47 - @{term s'}. The formula @{text "\<EF> p"} holds in a state @{term
1.48 - s}, iff there is a path in @{text \<M>}, starting from @{term s},
1.49 - such that there exists a state @{term s'} on the path, such that
1.50 - @{term p} holds in @{term s'}. The formula @{text "\<EG> p"} holds
1.51 - in a state @{term s}, iff there is a path, starting from @{term s},
1.52 - such that for all states @{term s'} on the path, @{term p} holds in
1.53 - @{term s'}. It is easy to see that @{text "\<EF> p"} and @{text
1.54 - "\<EG> p"} may be expressed using least and greatest fixed points
1.55 - \cite{McMillan-PhDThesis}.
1.56 -*}
1.57 -
1.58 -constdefs
1.59 - EX :: "'a ctl \<Rightarrow> 'a ctl" ("\<EX> _" [80] 90) "\<EX> p \<equiv> {s. \<exists>s'. (s, s') \<in> \<M> \<and> s' \<in> p}"
1.60 - EF :: "'a ctl \<Rightarrow> 'a ctl" ("\<EF> _" [80] 90) "\<EF> p \<equiv> lfp (\<lambda>s. p \<union> \<EX> s)"
1.61 - EG :: "'a ctl \<Rightarrow> 'a ctl" ("\<EG> _" [80] 90) "\<EG> p \<equiv> gfp (\<lambda>s. p \<inter> \<EX> s)"
1.62 -
1.63 -text {*
1.64 - @{text "\<AX>"}, @{text "\<AF>"} and @{text "\<AG>"} are now defined
1.65 - dually in terms of @{text "\<EX>"}, @{text "\<EF>"} and @{text
1.66 - "\<EG>"}.
1.67 -*}
1.68 -
1.69 -constdefs
1.70 - AX :: "'a ctl \<Rightarrow> 'a ctl" ("\<AX> _" [80] 90) "\<AX> p \<equiv> - \<EX> - p"
1.71 - AF :: "'a ctl \<Rightarrow> 'a ctl" ("\<AF> _" [80] 90) "\<AF> p \<equiv> - \<EG> - p"
1.72 - AG :: "'a ctl \<Rightarrow> 'a ctl" ("\<AG> _" [80] 90) "\<AG> p \<equiv> - \<EF> - p"
1.73 -
1.74 -lemmas [simp] = EX_def EG_def AX_def EF_def AF_def AG_def
1.75 -
1.76 -
1.77 -section {* Basic fixed point properties *}
1.78 -
1.79 -text {*
1.80 - First of all, we use the de-Morgan property of fixed points
1.81 -*}
1.82 -
1.83 -lemma lfp_gfp: "lfp f = - gfp (\<lambda>s . - (f (- s)))"
1.84 -proof
1.85 - show "lfp f \<subseteq> - gfp (\<lambda>s. - f (- s))"
1.86 - proof
1.87 - fix x assume l: "x \<in> lfp f"
1.88 - show "x \<in> - gfp (\<lambda>s. - f (- s))"
1.89 - proof
1.90 - assume "x \<in> gfp (\<lambda>s. - f (- s))"
1.91 - then obtain u where "x \<in> u" and "u \<subseteq> - f (- u)" by (unfold gfp_def) auto
1.92 - then have "f (- u) \<subseteq> - u" by auto
1.93 - then have "lfp f \<subseteq> - u" by (rule lfp_lowerbound)
1.94 - from l and this have "x \<notin> u" by auto
1.95 - then show False by contradiction
1.96 - qed
1.97 - qed
1.98 - show "- gfp (\<lambda>s. - f (- s)) \<subseteq> lfp f"
1.99 - proof (rule lfp_greatest)
1.100 - fix u assume "f u \<subseteq> u"
1.101 - then have "- u \<subseteq> - f u" by auto
1.102 - then have "- u \<subseteq> - f (- (- u))" by simp
1.103 - then have "- u \<subseteq> gfp (\<lambda>s. - f (- s))" by (rule gfp_upperbound)
1.104 - then show "- gfp (\<lambda>s. - f (- s)) \<subseteq> u" by auto
1.105 - qed
1.106 -qed
1.107 -
1.108 -lemma lfp_gfp': "- lfp f = gfp (\<lambda>s. - (f (- s)))"
1.109 - by (simp add: lfp_gfp)
1.110 -
1.111 -lemma gfp_lfp': "- gfp f = lfp (\<lambda>s. - (f (- s)))"
1.112 - by (simp add: lfp_gfp)
1.113 -
1.114 -text {*
1.115 - in order to give dual fixed point representations of @{term "AF p"}
1.116 - and @{term "AG p"}:
1.117 -*}
1.118 -
1.119 -lemma AF_lfp: "\<AF> p = lfp (\<lambda>s. p \<union> \<AX> s)" by (simp add: lfp_gfp)
1.120 -lemma AG_gfp: "\<AG> p = gfp (\<lambda>s. p \<inter> \<AX> s)" by (simp add: lfp_gfp)
1.121 -
1.122 -lemma EF_fp: "\<EF> p = p \<union> \<EX> \<EF> p"
1.123 -proof -
1.124 - have "mono (\<lambda>s. p \<union> \<EX> s)" by rule (auto simp add: EX_def)
1.125 - then show ?thesis by (simp only: EF_def) (rule lfp_unfold)
1.126 -qed
1.127 -
1.128 -lemma AF_fp: "\<AF> p = p \<union> \<AX> \<AF> p"
1.129 -proof -
1.130 - have "mono (\<lambda>s. p \<union> \<AX> s)" by rule (auto simp add: AX_def EX_def)
1.131 - then show ?thesis by (simp only: AF_lfp) (rule lfp_unfold)
1.132 -qed
1.133 -
1.134 -lemma EG_fp: "\<EG> p = p \<inter> \<EX> \<EG> p"
1.135 -proof -
1.136 - have "mono (\<lambda>s. p \<inter> \<EX> s)" by rule (auto simp add: EX_def)
1.137 - then show ?thesis by (simp only: EG_def) (rule gfp_unfold)
1.138 -qed
1.139 -
1.140 -text {*
1.141 - From the greatest fixed point definition of @{term "\<AG> p"}, we
1.142 - derive as a consequence of the Knaster-Tarski theorem on the one
1.143 - hand that @{term "\<AG> p"} is a fixed point of the monotonic
1.144 - function @{term "\<lambda>s. p \<inter> \<AX> s"}.
1.145 -*}
1.146 -
1.147 -lemma AG_fp: "\<AG> p = p \<inter> \<AX> \<AG> p"
1.148 -proof -
1.149 - have "mono (\<lambda>s. p \<inter> \<AX> s)" by rule (auto simp add: AX_def EX_def)
1.150 - then show ?thesis by (simp only: AG_gfp) (rule gfp_unfold)
1.151 -qed
1.152 -
1.153 -text {*
1.154 - This fact may be split up into two inequalities (merely using
1.155 - transitivity of @{text "\<subseteq>" }, which is an instance of the overloaded
1.156 - @{text "\<le>"} in Isabelle/HOL).
1.157 -*}
1.158 -
1.159 -lemma AG_fp_1: "\<AG> p \<subseteq> p"
1.160 -proof -
1.161 - note AG_fp also have "p \<inter> \<AX> \<AG> p \<subseteq> p" by auto
1.162 - finally show ?thesis .
1.163 -qed
1.164 -
1.165 -text {**}
1.166 -
1.167 -lemma AG_fp_2: "\<AG> p \<subseteq> \<AX> \<AG> p"
1.168 -proof -
1.169 - note AG_fp also have "p \<inter> \<AX> \<AG> p \<subseteq> \<AX> \<AG> p" by auto
1.170 - finally show ?thesis .
1.171 -qed
1.172 -
1.173 -text {*
1.174 - On the other hand, we have from the Knaster-Tarski fixed point
1.175 - theorem that any other post-fixed point of @{term "\<lambda>s. p \<inter> AX s"} is
1.176 - smaller than @{term "AG p"}. A post-fixed point is a set of states
1.177 - @{term q} such that @{term "q \<subseteq> p \<inter> AX q"}. This leads to the
1.178 - following co-induction principle for @{term "AG p"}.
1.179 -*}
1.180 -
1.181 -lemma AG_I: "q \<subseteq> p \<inter> \<AX> q \<Longrightarrow> q \<subseteq> \<AG> p"
1.182 - by (simp only: AG_gfp) (rule gfp_upperbound)
1.183 -
1.184 -
1.185 -section {* The tree induction principle \label{sec:calc-ctl-tree-induct} *}
1.186 -
1.187 -text {*
1.188 - With the most basic facts available, we are now able to establish a
1.189 - few more interesting results, leading to the \emph{tree induction}
1.190 - principle for @{text AG} (see below). We will use some elementary
1.191 - monotonicity and distributivity rules.
1.192 -*}
1.193 -
1.194 -lemma AX_int: "\<AX> (p \<inter> q) = \<AX> p \<inter> \<AX> q" by auto
1.195 -lemma AX_mono: "p \<subseteq> q \<Longrightarrow> \<AX> p \<subseteq> \<AX> q" by auto
1.196 -lemma AG_mono: "p \<subseteq> q \<Longrightarrow> \<AG> p \<subseteq> \<AG> q"
1.197 - by (simp only: AG_gfp, rule gfp_mono) auto
1.198 -
1.199 -text {*
1.200 - The formula @{term "AG p"} implies @{term "AX p"} (we use
1.201 - substitution of @{text "\<subseteq>"} with monotonicity).
1.202 -*}
1.203 -
1.204 -lemma AG_AX: "\<AG> p \<subseteq> \<AX> p"
1.205 -proof -
1.206 - have "\<AG> p \<subseteq> \<AX> \<AG> p" by (rule AG_fp_2)
1.207 - also have "\<AG> p \<subseteq> p" by (rule AG_fp_1) moreover note AX_mono
1.208 - finally show ?thesis .
1.209 -qed
1.210 -
1.211 -text {*
1.212 - Furthermore we show idempotency of the @{text "\<AG>"} operator.
1.213 - The proof is a good example of how accumulated facts may get
1.214 - used to feed a single rule step.
1.215 -*}
1.216 -
1.217 -lemma AG_AG: "\<AG> \<AG> p = \<AG> p"
1.218 -proof
1.219 - show "\<AG> \<AG> p \<subseteq> \<AG> p" by (rule AG_fp_1)
1.220 -next
1.221 - show "\<AG> p \<subseteq> \<AG> \<AG> p"
1.222 - proof (rule AG_I)
1.223 - have "\<AG> p \<subseteq> \<AG> p" ..
1.224 - moreover have "\<AG> p \<subseteq> \<AX> \<AG> p" by (rule AG_fp_2)
1.225 - ultimately show "\<AG> p \<subseteq> \<AG> p \<inter> \<AX> \<AG> p" ..
1.226 - qed
1.227 -qed
1.228 -
1.229 -text {*
1.230 - \smallskip We now give an alternative characterization of the @{text
1.231 - "\<AG>"} operator, which describes the @{text "\<AG>"} operator in
1.232 - an ``operational'' way by tree induction: In a state holds @{term
1.233 - "AG p"} iff in that state holds @{term p}, and in all reachable
1.234 - states @{term s} follows from the fact that @{term p} holds in
1.235 - @{term s}, that @{term p} also holds in all successor states of
1.236 - @{term s}. We use the co-induction principle @{thm [source] AG_I}
1.237 - to establish this in a purely algebraic manner.
1.238 -*}
1.239 -
1.240 -theorem AG_induct: "p \<inter> \<AG> (p \<rightarrow> \<AX> p) = \<AG> p"
1.241 -proof
1.242 - show "p \<inter> \<AG> (p \<rightarrow> \<AX> p) \<subseteq> \<AG> p" (is "?lhs \<subseteq> _")
1.243 - proof (rule AG_I)
1.244 - show "?lhs \<subseteq> p \<inter> \<AX> ?lhs"
1.245 - proof
1.246 - show "?lhs \<subseteq> p" ..
1.247 - show "?lhs \<subseteq> \<AX> ?lhs"
1.248 - proof -
1.249 - {
1.250 - have "\<AG> (p \<rightarrow> \<AX> p) \<subseteq> p \<rightarrow> \<AX> p" by (rule AG_fp_1)
1.251 - also have "p \<inter> p \<rightarrow> \<AX> p \<subseteq> \<AX> p" ..
1.252 - finally have "?lhs \<subseteq> \<AX> p" by auto
1.253 - }
1.254 - moreover
1.255 - {
1.256 - have "p \<inter> \<AG> (p \<rightarrow> \<AX> p) \<subseteq> \<AG> (p \<rightarrow> \<AX> p)" ..
1.257 - also have "\<dots> \<subseteq> \<AX> \<dots>" by (rule AG_fp_2)
1.258 - finally have "?lhs \<subseteq> \<AX> \<AG> (p \<rightarrow> \<AX> p)" .
1.259 - }
1.260 - ultimately have "?lhs \<subseteq> \<AX> p \<inter> \<AX> \<AG> (p \<rightarrow> \<AX> p)" ..
1.261 - also have "\<dots> = \<AX> ?lhs" by (simp only: AX_int)
1.262 - finally show ?thesis .
1.263 - qed
1.264 - qed
1.265 - qed
1.266 -next
1.267 - show "\<AG> p \<subseteq> p \<inter> \<AG> (p \<rightarrow> \<AX> p)"
1.268 - proof
1.269 - show "\<AG> p \<subseteq> p" by (rule AG_fp_1)
1.270 - show "\<AG> p \<subseteq> \<AG> (p \<rightarrow> \<AX> p)"
1.271 - proof -
1.272 - have "\<AG> p = \<AG> \<AG> p" by (simp only: AG_AG)
1.273 - also have "\<AG> p \<subseteq> \<AX> p" by (rule AG_AX) moreover note AG_mono
1.274 - also have "\<AX> p \<subseteq> (p \<rightarrow> \<AX> p)" .. moreover note AG_mono
1.275 - finally show ?thesis .
1.276 - qed
1.277 - qed
1.278 -qed
1.279 -
1.280 -
1.281 -section {* An application of tree induction \label{sec:calc-ctl-commute} *}
1.282 -
1.283 -text {*
1.284 - Further interesting properties of CTL expressions may be
1.285 - demonstrated with the help of tree induction; here we show that
1.286 - @{text \<AX>} and @{text \<AG>} commute.
1.287 -*}
1.288 -
1.289 -theorem AG_AX_commute: "\<AG> \<AX> p = \<AX> \<AG> p"
1.290 -proof -
1.291 - have "\<AG> \<AX> p = \<AX> p \<inter> \<AX> \<AG> \<AX> p" by (rule AG_fp)
1.292 - also have "\<dots> = \<AX> (p \<inter> \<AG> \<AX> p)" by (simp only: AX_int)
1.293 - also have "p \<inter> \<AG> \<AX> p = \<AG> p" (is "?lhs = _")
1.294 - proof
1.295 - have "\<AX> p \<subseteq> p \<rightarrow> \<AX> p" ..
1.296 - also have "p \<inter> \<AG> (p \<rightarrow> \<AX> p) = \<AG> p" by (rule AG_induct)
1.297 - also note Int_mono AG_mono
1.298 - ultimately show "?lhs \<subseteq> \<AG> p" by fast
1.299 - next
1.300 - have "\<AG> p \<subseteq> p" by (rule AG_fp_1)
1.301 - moreover
1.302 - {
1.303 - have "\<AG> p = \<AG> \<AG> p" by (simp only: AG_AG)
1.304 - also have "\<AG> p \<subseteq> \<AX> p" by (rule AG_AX)
1.305 - also note AG_mono
1.306 - ultimately have "\<AG> p \<subseteq> \<AG> \<AX> p" .
1.307 - }
1.308 - ultimately show "\<AG> p \<subseteq> ?lhs" ..
1.309 - qed
1.310 - finally show ?thesis .
1.311 -qed
1.312 -
1.313 -end
2.1 --- a/src/HOL/CTL/ROOT.ML Thu Apr 28 12:04:34 2005 +0200
2.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
2.3 @@ -1,3 +0,0 @@
2.4 -
2.5 -use_thy "CTL";
2.6 -
3.1 --- a/src/HOL/CTL/document/root.bib Thu Apr 28 12:04:34 2005 +0200
3.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
3.3 @@ -1,13 +0,0 @@
3.4 -
3.5 -@Misc{McMillan-LectureNotes,
3.6 - author = {Ken McMillan},
3.7 - title = {Lecture notes on verification of digital and hybrid systems},
3.8 - note = {{NATO} summer school, \url{http://www-cad.eecs.berkeley.edu/~kenmcmil/tutorial/toc.html}}
3.9 -}
3.10 -
3.11 -@PhdThesis{McMillan-PhDThesis,
3.12 - author = {Ken McMillan},
3.13 - title = {Symbolic Model Checking: an approach to the state explosion problem},
3.14 - school = {Carnegie Mellon University},
3.15 - year = 1992
3.16 -}
4.1 --- a/src/HOL/CTL/document/root.tex Thu Apr 28 12:04:34 2005 +0200
4.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
4.3 @@ -1,32 +0,0 @@
4.4 -
4.5 -\documentclass[11pt,a4paper]{article}
4.6 -\usepackage{isabelle,isabellesym,pdfsetup}
4.7 -
4.8 -\urlstyle{rm}
4.9 -\isabellestyle{it}
4.10 -
4.11 -\newcommand{\isasymEX}{\isamath{\mathrm{EX}}}
4.12 -\newcommand{\isasymEF}{\isamath{\mathrm{EF}}}
4.13 -\newcommand{\isasymEG}{\isamath{\mathrm{EG}}}
4.14 -\newcommand{\isasymAX}{\isamath{\mathrm{AX}}}
4.15 -\newcommand{\isasymAF}{\isamath{\mathrm{AF}}}
4.16 -\newcommand{\isasymAG}{\isamath{\mathrm{AG}}}
4.17 -
4.18 -
4.19 -\begin{document}
4.20 -
4.21 -\title{Some properties of CTL}
4.22 -\author{Gertrud Bauer}
4.23 -\maketitle
4.24 -
4.25 -\tableofcontents
4.26 -\bigskip
4.27 -
4.28 -\parindent 0pt\parskip 0.5ex
4.29 -
4.30 -\input{session}
4.31 -
4.32 -\bibliographystyle{abbrv}
4.33 -\bibliography{root}
4.34 -
4.35 -\end{document}
5.1 --- a/src/HOL/IsaMakefile Thu Apr 28 12:04:34 2005 +0200
5.2 +++ b/src/HOL/IsaMakefile Thu Apr 28 17:08:08 2005 +0200
5.3 @@ -16,7 +16,6 @@
5.4 HOL-Bali \
5.5 HOL-Complex-ex \
5.6 HOL-Complex-Import \
5.7 - HOL-CTL \
5.8 HOL-Extraction \
5.9 HOL-Complex-HahnBanach \
5.10 HOL-Hoare \
5.11 @@ -534,15 +533,6 @@
5.12 @$(ISATOOL) usedir -g true $(OUT)/HOL Bali
5.13
5.14
5.15 -## HOL-CTL
5.16 -
5.17 -HOL-CTL: HOL $(LOG)/HOL-CTL.gz
5.18 -
5.19 -$(LOG)/HOL-CTL.gz: $(OUT)/HOL \
5.20 - CTL/CTL.thy CTL/ROOT.ML CTL/document/root.tex CTL/document/root.bib
5.21 - @$(ISATOOL) usedir $(OUT)/HOL CTL
5.22 -
5.23 -
5.24 ## HOL-Extraction
5.25
5.26 HOL-Extraction: HOL $(LOG)/HOL-Extraction.gz
5.27 @@ -701,7 +691,7 @@
5.28 $(LOG)/HOL-Lex.gz $(LOG)/HOL-Algebra.gz \
5.29 $(LOG)/HOL-Auth.gz $(LOG)/HOL-UNITY.gz \
5.30 $(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz \
5.31 - $(LOG)/HOL-Bali.gz $(LOG)/HOL-CTL.gz \
5.32 + $(LOG)/HOL-Bali.gz \
5.33 $(LOG)/HOL-MicroJava.gz $(LOG)/HOL-NanoJava.gz \
5.34 $(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses \
5.35 $(LOG)/HOL-Lattice \
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/src/HOL/ex/CTL.thy Thu Apr 28 17:08:08 2005 +0200
6.3 @@ -0,0 +1,317 @@
6.4 +
6.5 +(* Title: HOL/ex/CTL.thy
6.6 + ID: $Id$
6.7 + Author: Gertrud Bauer
6.8 +*)
6.9 +
6.10 +header {* CTL formulae *}
6.11 +
6.12 +theory CTL = Main:
6.13 +
6.14 +
6.15 +
6.16 +text {*
6.17 + We formalize basic concepts of Computational Tree Logic (CTL)
6.18 + \cite{McMillan-PhDThesis,McMillan-LectureNotes} within the
6.19 + simply-typed set theory of HOL.
6.20 +
6.21 + By using the common technique of ``shallow embedding'', a CTL
6.22 + formula is identified with the corresponding set of states where it
6.23 + holds. Consequently, CTL operations such as negation, conjunction,
6.24 + disjunction simply become complement, intersection, union of sets.
6.25 + We only require a separate operation for implication, as point-wise
6.26 + inclusion is usually not encountered in plain set-theory.
6.27 +*}
6.28 +
6.29 +lemmas [intro!] = Int_greatest Un_upper2 Un_upper1 Int_lower1 Int_lower2
6.30 +
6.31 +types 'a ctl = "'a set"
6.32 +constdefs
6.33 + imp :: "'a ctl \<Rightarrow> 'a ctl \<Rightarrow> 'a ctl" (infixr "\<rightarrow>" 75)
6.34 + "p \<rightarrow> q \<equiv> - p \<union> q"
6.35 +
6.36 +lemma [intro!]: "p \<inter> p \<rightarrow> q \<subseteq> q" by (unfold imp_def) auto
6.37 +lemma [intro!]: "p \<subseteq> (q \<rightarrow> p)" by (unfold imp_def) rule
6.38 +
6.39 +
6.40 +text {*
6.41 + \smallskip The CTL path operators are more interesting; they are
6.42 + based on an arbitrary, but fixed model @{text \<M>}, which is simply
6.43 + a transition relation over states @{typ "'a"}.
6.44 +*}
6.45 +
6.46 +consts model :: "('a \<times> 'a) set" ("\<M>")
6.47 +
6.48 +text {*
6.49 + The operators @{text \<EX>}, @{text \<EF>}, @{text \<EG>} are taken
6.50 + as primitives, while @{text \<AX>}, @{text \<AF>}, @{text \<AG>} are
6.51 + defined as derived ones. The formula @{text "\<EX> p"} holds in a
6.52 + state @{term s}, iff there is a successor state @{term s'} (with
6.53 + respect to the model @{term \<M>}), such that @{term p} holds in
6.54 + @{term s'}. The formula @{text "\<EF> p"} holds in a state @{term
6.55 + s}, iff there is a path in @{text \<M>}, starting from @{term s},
6.56 + such that there exists a state @{term s'} on the path, such that
6.57 + @{term p} holds in @{term s'}. The formula @{text "\<EG> p"} holds
6.58 + in a state @{term s}, iff there is a path, starting from @{term s},
6.59 + such that for all states @{term s'} on the path, @{term p} holds in
6.60 + @{term s'}. It is easy to see that @{text "\<EF> p"} and @{text
6.61 + "\<EG> p"} may be expressed using least and greatest fixed points
6.62 + \cite{McMillan-PhDThesis}.
6.63 +*}
6.64 +
6.65 +constdefs
6.66 + EX :: "'a ctl \<Rightarrow> 'a ctl" ("\<EX> _" [80] 90) "\<EX> p \<equiv> {s. \<exists>s'. (s, s') \<in> \<M> \<and> s' \<in> p}"
6.67 + EF :: "'a ctl \<Rightarrow> 'a ctl" ("\<EF> _" [80] 90) "\<EF> p \<equiv> lfp (\<lambda>s. p \<union> \<EX> s)"
6.68 + EG :: "'a ctl \<Rightarrow> 'a ctl" ("\<EG> _" [80] 90) "\<EG> p \<equiv> gfp (\<lambda>s. p \<inter> \<EX> s)"
6.69 +
6.70 +text {*
6.71 + @{text "\<AX>"}, @{text "\<AF>"} and @{text "\<AG>"} are now defined
6.72 + dually in terms of @{text "\<EX>"}, @{text "\<EF>"} and @{text
6.73 + "\<EG>"}.
6.74 +*}
6.75 +
6.76 +constdefs
6.77 + AX :: "'a ctl \<Rightarrow> 'a ctl" ("\<AX> _" [80] 90) "\<AX> p \<equiv> - \<EX> - p"
6.78 + AF :: "'a ctl \<Rightarrow> 'a ctl" ("\<AF> _" [80] 90) "\<AF> p \<equiv> - \<EG> - p"
6.79 + AG :: "'a ctl \<Rightarrow> 'a ctl" ("\<AG> _" [80] 90) "\<AG> p \<equiv> - \<EF> - p"
6.80 +
6.81 +lemmas [simp] = EX_def EG_def AX_def EF_def AF_def AG_def
6.82 +
6.83 +
6.84 +section {* Basic fixed point properties *}
6.85 +
6.86 +text {*
6.87 + First of all, we use the de-Morgan property of fixed points
6.88 +*}
6.89 +
6.90 +lemma lfp_gfp: "lfp f = - gfp (\<lambda>s . - (f (- s)))"
6.91 +proof
6.92 + show "lfp f \<subseteq> - gfp (\<lambda>s. - f (- s))"
6.93 + proof
6.94 + fix x assume l: "x \<in> lfp f"
6.95 + show "x \<in> - gfp (\<lambda>s. - f (- s))"
6.96 + proof
6.97 + assume "x \<in> gfp (\<lambda>s. - f (- s))"
6.98 + then obtain u where "x \<in> u" and "u \<subseteq> - f (- u)" by (unfold gfp_def) auto
6.99 + then have "f (- u) \<subseteq> - u" by auto
6.100 + then have "lfp f \<subseteq> - u" by (rule lfp_lowerbound)
6.101 + from l and this have "x \<notin> u" by auto
6.102 + then show False by contradiction
6.103 + qed
6.104 + qed
6.105 + show "- gfp (\<lambda>s. - f (- s)) \<subseteq> lfp f"
6.106 + proof (rule lfp_greatest)
6.107 + fix u assume "f u \<subseteq> u"
6.108 + then have "- u \<subseteq> - f u" by auto
6.109 + then have "- u \<subseteq> - f (- (- u))" by simp
6.110 + then have "- u \<subseteq> gfp (\<lambda>s. - f (- s))" by (rule gfp_upperbound)
6.111 + then show "- gfp (\<lambda>s. - f (- s)) \<subseteq> u" by auto
6.112 + qed
6.113 +qed
6.114 +
6.115 +lemma lfp_gfp': "- lfp f = gfp (\<lambda>s. - (f (- s)))"
6.116 + by (simp add: lfp_gfp)
6.117 +
6.118 +lemma gfp_lfp': "- gfp f = lfp (\<lambda>s. - (f (- s)))"
6.119 + by (simp add: lfp_gfp)
6.120 +
6.121 +text {*
6.122 + in order to give dual fixed point representations of @{term "AF p"}
6.123 + and @{term "AG p"}:
6.124 +*}
6.125 +
6.126 +lemma AF_lfp: "\<AF> p = lfp (\<lambda>s. p \<union> \<AX> s)" by (simp add: lfp_gfp)
6.127 +lemma AG_gfp: "\<AG> p = gfp (\<lambda>s. p \<inter> \<AX> s)" by (simp add: lfp_gfp)
6.128 +
6.129 +lemma EF_fp: "\<EF> p = p \<union> \<EX> \<EF> p"
6.130 +proof -
6.131 + have "mono (\<lambda>s. p \<union> \<EX> s)" by rule (auto simp add: EX_def)
6.132 + then show ?thesis by (simp only: EF_def) (rule lfp_unfold)
6.133 +qed
6.134 +
6.135 +lemma AF_fp: "\<AF> p = p \<union> \<AX> \<AF> p"
6.136 +proof -
6.137 + have "mono (\<lambda>s. p \<union> \<AX> s)" by rule (auto simp add: AX_def EX_def)
6.138 + then show ?thesis by (simp only: AF_lfp) (rule lfp_unfold)
6.139 +qed
6.140 +
6.141 +lemma EG_fp: "\<EG> p = p \<inter> \<EX> \<EG> p"
6.142 +proof -
6.143 + have "mono (\<lambda>s. p \<inter> \<EX> s)" by rule (auto simp add: EX_def)
6.144 + then show ?thesis by (simp only: EG_def) (rule gfp_unfold)
6.145 +qed
6.146 +
6.147 +text {*
6.148 + From the greatest fixed point definition of @{term "\<AG> p"}, we
6.149 + derive as a consequence of the Knaster-Tarski theorem on the one
6.150 + hand that @{term "\<AG> p"} is a fixed point of the monotonic
6.151 + function @{term "\<lambda>s. p \<inter> \<AX> s"}.
6.152 +*}
6.153 +
6.154 +lemma AG_fp: "\<AG> p = p \<inter> \<AX> \<AG> p"
6.155 +proof -
6.156 + have "mono (\<lambda>s. p \<inter> \<AX> s)" by rule (auto simp add: AX_def EX_def)
6.157 + then show ?thesis by (simp only: AG_gfp) (rule gfp_unfold)
6.158 +qed
6.159 +
6.160 +text {*
6.161 + This fact may be split up into two inequalities (merely using
6.162 + transitivity of @{text "\<subseteq>" }, which is an instance of the overloaded
6.163 + @{text "\<le>"} in Isabelle/HOL).
6.164 +*}
6.165 +
6.166 +lemma AG_fp_1: "\<AG> p \<subseteq> p"
6.167 +proof -
6.168 + note AG_fp also have "p \<inter> \<AX> \<AG> p \<subseteq> p" by auto
6.169 + finally show ?thesis .
6.170 +qed
6.171 +
6.172 +text {**}
6.173 +
6.174 +lemma AG_fp_2: "\<AG> p \<subseteq> \<AX> \<AG> p"
6.175 +proof -
6.176 + note AG_fp also have "p \<inter> \<AX> \<AG> p \<subseteq> \<AX> \<AG> p" by auto
6.177 + finally show ?thesis .
6.178 +qed
6.179 +
6.180 +text {*
6.181 + On the other hand, we have from the Knaster-Tarski fixed point
6.182 + theorem that any other post-fixed point of @{term "\<lambda>s. p \<inter> AX s"} is
6.183 + smaller than @{term "AG p"}. A post-fixed point is a set of states
6.184 + @{term q} such that @{term "q \<subseteq> p \<inter> AX q"}. This leads to the
6.185 + following co-induction principle for @{term "AG p"}.
6.186 +*}
6.187 +
6.188 +lemma AG_I: "q \<subseteq> p \<inter> \<AX> q \<Longrightarrow> q \<subseteq> \<AG> p"
6.189 + by (simp only: AG_gfp) (rule gfp_upperbound)
6.190 +
6.191 +
6.192 +section {* The tree induction principle \label{sec:calc-ctl-tree-induct} *}
6.193 +
6.194 +text {*
6.195 + With the most basic facts available, we are now able to establish a
6.196 + few more interesting results, leading to the \emph{tree induction}
6.197 + principle for @{text AG} (see below). We will use some elementary
6.198 + monotonicity and distributivity rules.
6.199 +*}
6.200 +
6.201 +lemma AX_int: "\<AX> (p \<inter> q) = \<AX> p \<inter> \<AX> q" by auto
6.202 +lemma AX_mono: "p \<subseteq> q \<Longrightarrow> \<AX> p \<subseteq> \<AX> q" by auto
6.203 +lemma AG_mono: "p \<subseteq> q \<Longrightarrow> \<AG> p \<subseteq> \<AG> q"
6.204 + by (simp only: AG_gfp, rule gfp_mono) auto
6.205 +
6.206 +text {*
6.207 + The formula @{term "AG p"} implies @{term "AX p"} (we use
6.208 + substitution of @{text "\<subseteq>"} with monotonicity).
6.209 +*}
6.210 +
6.211 +lemma AG_AX: "\<AG> p \<subseteq> \<AX> p"
6.212 +proof -
6.213 + have "\<AG> p \<subseteq> \<AX> \<AG> p" by (rule AG_fp_2)
6.214 + also have "\<AG> p \<subseteq> p" by (rule AG_fp_1) moreover note AX_mono
6.215 + finally show ?thesis .
6.216 +qed
6.217 +
6.218 +text {*
6.219 + Furthermore we show idempotency of the @{text "\<AG>"} operator.
6.220 + The proof is a good example of how accumulated facts may get
6.221 + used to feed a single rule step.
6.222 +*}
6.223 +
6.224 +lemma AG_AG: "\<AG> \<AG> p = \<AG> p"
6.225 +proof
6.226 + show "\<AG> \<AG> p \<subseteq> \<AG> p" by (rule AG_fp_1)
6.227 +next
6.228 + show "\<AG> p \<subseteq> \<AG> \<AG> p"
6.229 + proof (rule AG_I)
6.230 + have "\<AG> p \<subseteq> \<AG> p" ..
6.231 + moreover have "\<AG> p \<subseteq> \<AX> \<AG> p" by (rule AG_fp_2)
6.232 + ultimately show "\<AG> p \<subseteq> \<AG> p \<inter> \<AX> \<AG> p" ..
6.233 + qed
6.234 +qed
6.235 +
6.236 +text {*
6.237 + \smallskip We now give an alternative characterization of the @{text
6.238 + "\<AG>"} operator, which describes the @{text "\<AG>"} operator in
6.239 + an ``operational'' way by tree induction: In a state holds @{term
6.240 + "AG p"} iff in that state holds @{term p}, and in all reachable
6.241 + states @{term s} follows from the fact that @{term p} holds in
6.242 + @{term s}, that @{term p} also holds in all successor states of
6.243 + @{term s}. We use the co-induction principle @{thm [source] AG_I}
6.244 + to establish this in a purely algebraic manner.
6.245 +*}
6.246 +
6.247 +theorem AG_induct: "p \<inter> \<AG> (p \<rightarrow> \<AX> p) = \<AG> p"
6.248 +proof
6.249 + show "p \<inter> \<AG> (p \<rightarrow> \<AX> p) \<subseteq> \<AG> p" (is "?lhs \<subseteq> _")
6.250 + proof (rule AG_I)
6.251 + show "?lhs \<subseteq> p \<inter> \<AX> ?lhs"
6.252 + proof
6.253 + show "?lhs \<subseteq> p" ..
6.254 + show "?lhs \<subseteq> \<AX> ?lhs"
6.255 + proof -
6.256 + {
6.257 + have "\<AG> (p \<rightarrow> \<AX> p) \<subseteq> p \<rightarrow> \<AX> p" by (rule AG_fp_1)
6.258 + also have "p \<inter> p \<rightarrow> \<AX> p \<subseteq> \<AX> p" ..
6.259 + finally have "?lhs \<subseteq> \<AX> p" by auto
6.260 + }
6.261 + moreover
6.262 + {
6.263 + have "p \<inter> \<AG> (p \<rightarrow> \<AX> p) \<subseteq> \<AG> (p \<rightarrow> \<AX> p)" ..
6.264 + also have "\<dots> \<subseteq> \<AX> \<dots>" by (rule AG_fp_2)
6.265 + finally have "?lhs \<subseteq> \<AX> \<AG> (p \<rightarrow> \<AX> p)" .
6.266 + }
6.267 + ultimately have "?lhs \<subseteq> \<AX> p \<inter> \<AX> \<AG> (p \<rightarrow> \<AX> p)" ..
6.268 + also have "\<dots> = \<AX> ?lhs" by (simp only: AX_int)
6.269 + finally show ?thesis .
6.270 + qed
6.271 + qed
6.272 + qed
6.273 +next
6.274 + show "\<AG> p \<subseteq> p \<inter> \<AG> (p \<rightarrow> \<AX> p)"
6.275 + proof
6.276 + show "\<AG> p \<subseteq> p" by (rule AG_fp_1)
6.277 + show "\<AG> p \<subseteq> \<AG> (p \<rightarrow> \<AX> p)"
6.278 + proof -
6.279 + have "\<AG> p = \<AG> \<AG> p" by (simp only: AG_AG)
6.280 + also have "\<AG> p \<subseteq> \<AX> p" by (rule AG_AX) moreover note AG_mono
6.281 + also have "\<AX> p \<subseteq> (p \<rightarrow> \<AX> p)" .. moreover note AG_mono
6.282 + finally show ?thesis .
6.283 + qed
6.284 + qed
6.285 +qed
6.286 +
6.287 +
6.288 +section {* An application of tree induction \label{sec:calc-ctl-commute} *}
6.289 +
6.290 +text {*
6.291 + Further interesting properties of CTL expressions may be
6.292 + demonstrated with the help of tree induction; here we show that
6.293 + @{text \<AX>} and @{text \<AG>} commute.
6.294 +*}
6.295 +
6.296 +theorem AG_AX_commute: "\<AG> \<AX> p = \<AX> \<AG> p"
6.297 +proof -
6.298 + have "\<AG> \<AX> p = \<AX> p \<inter> \<AX> \<AG> \<AX> p" by (rule AG_fp)
6.299 + also have "\<dots> = \<AX> (p \<inter> \<AG> \<AX> p)" by (simp only: AX_int)
6.300 + also have "p \<inter> \<AG> \<AX> p = \<AG> p" (is "?lhs = _")
6.301 + proof
6.302 + have "\<AX> p \<subseteq> p \<rightarrow> \<AX> p" ..
6.303 + also have "p \<inter> \<AG> (p \<rightarrow> \<AX> p) = \<AG> p" by (rule AG_induct)
6.304 + also note Int_mono AG_mono
6.305 + ultimately show "?lhs \<subseteq> \<AG> p" by fast
6.306 + next
6.307 + have "\<AG> p \<subseteq> p" by (rule AG_fp_1)
6.308 + moreover
6.309 + {
6.310 + have "\<AG> p = \<AG> \<AG> p" by (simp only: AG_AG)
6.311 + also have "\<AG> p \<subseteq> \<AX> p" by (rule AG_AX)
6.312 + also note AG_mono
6.313 + ultimately have "\<AG> p \<subseteq> \<AG> \<AX> p" .
6.314 + }
6.315 + ultimately show "\<AG> p \<subseteq> ?lhs" ..
6.316 + qed
6.317 + finally show ?thesis .
6.318 +qed
6.319 +
6.320 +end
7.1 --- a/src/HOL/ex/ROOT.ML Thu Apr 28 12:04:34 2005 +0200
7.2 +++ b/src/HOL/ex/ROOT.ML Thu Apr 28 17:08:08 2005 +0200
7.3 @@ -22,6 +22,7 @@
7.4 time_use_thy "NatSum";
7.5 time_use_thy "Intuitionistic";
7.6 time_use_thy "Classical";
7.7 +time_use_thy "CTL";
7.8 time_use_thy "mesontest2";
7.9 time_use_thy "PresburgerEx";
7.10 time_use_thy "BT";
7.11 @@ -30,6 +31,7 @@
7.12 time_use_thy "MergeSort";
7.13 time_use_thy "Puzzle";
7.14
7.15 +
7.16 time_use_thy "Lagrange";
7.17
7.18 time_use_thy "set";
8.1 --- a/src/HOL/ex/document/root.bib Thu Apr 28 12:04:34 2005 +0200
8.2 +++ b/src/HOL/ex/document/root.bib Thu Apr 28 17:08:08 2005 +0200
8.3 @@ -1,3 +1,5 @@
8.4 +
8.5 +
8.6
8.7 @TechReport{Gordon:1985:HOL,
8.8 author = {M. J. C. Gordon},
8.9 @@ -105,3 +107,16 @@
8.10 publisher = {Springer},
8.11 year = 2002,
8.12 note = {LNCS 2283}}
8.13 +
8.14 +@Misc{McMillan-LectureNotes,
8.15 + author = {Ken McMillan},
8.16 + title = {Lecture notes on verification of digital and hybrid systems},
8.17 + note = {{NATO} summer school, \url{http://www-cad.eecs.berkeley.edu/~kenmcmil/tutorial/toc.html}}
8.18 +}
8.19 +
8.20 +@PhdThesis{McMillan-PhDThesis,
8.21 + author = {Ken McMillan},
8.22 + title = {Symbolic Model Checking: an approach to the state explosion problem},
8.23 + school = {Carnegie Mellon University},
8.24 + year = 1992
8.25 +}
8.26 \ No newline at end of file
9.1 --- a/src/HOL/ex/document/root.tex Thu Apr 28 12:04:34 2005 +0200
9.2 +++ b/src/HOL/ex/document/root.tex Thu Apr 28 17:08:08 2005 +0200
9.3 @@ -11,6 +11,15 @@
9.4 \urlstyle{rm}
9.5 \isabellestyle{it}
9.6
9.7 +\newcommand{\isasymEX}{\isamath{\mathrm{EX}}}
9.8 +\newcommand{\isasymEF}{\isamath{\mathrm{EF}}}
9.9 +\newcommand{\isasymEG}{\isamath{\mathrm{EG}}}
9.10 +\newcommand{\isasymAX}{\isamath{\mathrm{AX}}}
9.11 +\newcommand{\isasymAF}{\isamath{\mathrm{AF}}}
9.12 +\newcommand{\isasymAG}{\isamath{\mathrm{AG}}}
9.13 +
9.14 +
9.15 +
9.16 \begin{document}
9.17
9.18 \title{Miscellaneous HOL Examples}