author bauerg Thu Apr 28 17:08:08 2005 +0200 (2005-04-28) changeset 15871 e524119dbf19 parent 15870 4320bce5873f child 15872 8336ff711d80
*** empty log message ***
 src/HOL/CTL/CTL.thy file | annotate | diff | revisions src/HOL/CTL/ROOT.ML file | annotate | diff | revisions src/HOL/CTL/document/root.bib file | annotate | diff | revisions src/HOL/CTL/document/root.tex file | annotate | diff | revisions src/HOL/IsaMakefile file | annotate | diff | revisions src/HOL/ex/CTL.thy file | annotate | diff | revisions src/HOL/ex/ROOT.ML file | annotate | diff | revisions src/HOL/ex/document/root.bib file | annotate | diff | revisions src/HOL/ex/document/root.tex file | annotate | diff | revisions
     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> _"  90)    "\<EX> p \<equiv> {s. \<exists>s'. (s, s') \<in> \<M> \<and> s' \<in> p}"
1.60 -  EF :: "'a ctl \<Rightarrow> 'a ctl"    ("\<EF> _"  90)    "\<EF> p \<equiv> lfp (\<lambda>s. p \<union> \<EX> s)"
1.61 -  EG :: "'a ctl \<Rightarrow> 'a ctl"    ("\<EG> _"  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> _"  90)    "\<AX> p \<equiv> - \<EX> - p"
1.71 -  AF :: "'a ctl \<Rightarrow> 'a ctl"    ("\<AF> _"  90)    "\<AF> p \<equiv> - \<EG> - p"
1.72 -  AG :: "'a ctl \<Rightarrow> 'a ctl"    ("\<AG> _"  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> _"  90)    "\<EX> p \<equiv> {s. \<exists>s'. (s, s') \<in> \<M> \<and> s' \<in> p}"
6.67 +  EF :: "'a ctl \<Rightarrow> 'a ctl"    ("\<EF> _"  90)    "\<EF> p \<equiv> lfp (\<lambda>s. p \<union> \<EX> s)"
6.68 +  EG :: "'a ctl \<Rightarrow> 'a ctl"    ("\<EG> _"  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> _"  90)    "\<AX> p \<equiv> - \<EX> - p"
6.78 +  AF :: "'a ctl \<Rightarrow> 'a ctl"    ("\<AF> _"  90)    "\<AF> p \<equiv> - \<EG> - p"
6.79 +  AG :: "'a ctl \<Rightarrow> 'a ctl"    ("\<AG> _"  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}