*** empty log message ***
authorbauerg
Thu Apr 28 17:08:08 2005 +0200 (2005-04-28)
changeset 15871e524119dbf19
parent 15870 4320bce5873f
child 15872 8336ff711d80
*** empty log message ***
src/HOL/CTL/CTL.thy
src/HOL/CTL/ROOT.ML
src/HOL/CTL/document/root.bib
src/HOL/CTL/document/root.tex
src/HOL/IsaMakefile
src/HOL/ex/CTL.thy
src/HOL/ex/ROOT.ML
src/HOL/ex/document/root.bib
src/HOL/ex/document/root.tex
     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}