src/HOL/CTL/CTL.thy

 theory CTL = Main:
 
 section {* CTL formulae *}
 
 text {*
-  \tweakskip By using the common technique of ``shallow embedding'', a
-  CTL formula is identified with the corresponding set of states where
-  it holds.  Consequently, CTL operations such as negation,
-  conjunction, disjunction simply become complement, intersection,
-  union of sets.  We only require a separate operation for
-  implication, as point-wise inclusion is usually not encountered in
-  plain set-theory.
+  \tweakskip We formalize basic concepts of Computational Tree Logic
+  (CTL) \cite{McMillan-PhDThesis,McMillan-LectureNotes} within the
+  simply-typed set theory of HOL.
+
+  By using the common technique of ``shallow embedding'', a CTL
+  formula is identified with the corresponding set of states where it
+  holds.  Consequently, CTL operations such as negation, conjunction,
+  disjunction simply become complement, intersection, union of sets.
+  We only require a separate operation for implication, as point-wise
+  inclusion is usually not encountered in plain set-theory.
 *}
 
 lemmas [intro!] = Int_greatest Un_upper2 Un_upper1 Int_lower1 Int_lower2
 
 types 'a ctl = "'a set"

 lemma [intro!]: "p \<inter> p \<rightarrow> q \<subseteq> q" by (unfold imp_def) auto
 lemma [intro!]: "p \<subseteq> (q \<rightarrow> p)" by (unfold imp_def) rule
 
 
 text {*
-  \smallskip The CTL path operators are more interesting; they are 
-  based on an arbitrary, but fixed model @{text \<M>}, which is simply 
-  a transition relation over states @{typ "'a"}. 
+  \smallskip The CTL path operators are more interesting; they are
+  based on an arbitrary, but fixed model @{text \<M>}, which is simply
+  a transition relation over states @{typ "'a"}.
 *}
 
 consts model :: "('a \<times> 'a) set"    ("\<M>")
 
 text {*
-  The operators @{text \<EX>}, @{text \<EF>}, @{text \<EG>} are taken as
-  primitives, while @{text \<AX>}, @{text \<AF>}, @{text \<AG>} are
+  The operators @{text \<EX>}, @{text \<EF>}, @{text \<EG>} are taken
+  as primitives, while @{text \<AX>}, @{text \<AF>}, @{text \<AG>} are
   defined as derived ones.  The formula @{text "\<EX> p"} holds in a
   state @{term s}, iff there is a successor state @{term s'} (with
   respect to the model @{term \<M>}), such that @{term p} holds in
   @{term s'}.  The formula @{text "\<EF> p"} holds in a state @{term
   s}, iff there is a path in @{text \<M>}, starting from @{term s},

   EX :: "'a ctl \<Rightarrow> 'a ctl"    ("\<EX> _" [80] 90)    "\<EX> p \<equiv> {s. \<exists>s'. (s, s') \<in> \<M> \<and> s' \<in> p}"
   EF :: "'a ctl \<Rightarrow> 'a ctl"    ("\<EF> _" [80] 90)    "\<EF> p \<equiv> lfp (\<lambda>s. p \<union> \<EX> s)"
   EG :: "'a ctl \<Rightarrow> 'a ctl"    ("\<EG> _" [80] 90)    "\<EG> p \<equiv> gfp (\<lambda>s. p \<inter> \<EX> s)"
 
 text {*
-  @{text "\<AX>"}, @{text "\<AF>"} and @{text "\<AG>"} are now defined 
-  dually in terms of @{text "\<EX>"}, @{text "\<EF>"} and @{text "\<EG>"}.
+  @{text "\<AX>"}, @{text "\<AF>"} and @{text "\<AG>"} are now defined
+  dually in terms of @{text "\<EX>"}, @{text "\<EF>"} and @{text
+  "\<EG>"}.
 *}
 
 constdefs
   AX :: "'a ctl \<Rightarrow> 'a ctl"    ("\<AX> _" [80] 90)    "\<AX> p \<equiv> - \<EX> - p"
   AF :: "'a ctl \<Rightarrow> 'a ctl"    ("\<AF> _" [80] 90)    "\<AF> p \<equiv> - \<EG> - p"
   AG :: "'a ctl \<Rightarrow> 'a ctl"    ("\<AG> _" [80] 90)    "\<AG> p \<equiv> - \<EF> - p"
 
 lemmas [simp] = EX_def EG_def AX_def EF_def AF_def AG_def
 
 
-
 section {* Basic fixed point properties *}
 
 text {*
-  \tweakskip First of all, we use the de-Morgan property of fixed points
+  \tweakskip First of all, we use the de-Morgan property of fixed
+  points
 *}
 
 lemma lfp_gfp: "lfp f = - gfp (\<lambda>s . - (f (- s)))"
 proof
   show "lfp f \<subseteq> - gfp (\<lambda>s. - f (- s))"

 proof -
   have "mono (\<lambda>s. p \<inter> \<EX> s)" by rule (auto simp add: EX_def)
   then show ?thesis by (simp only: EG_def) (rule gfp_unfold)
 qed
 
-
 text {*
   From the greatest fixed point definition of @{term "\<AG> p"}, we
   derive as a consequence of the Knaster-Tarski theorem on the one
   hand that @{term "\<AG> p"} is a fixed point of the monotonic
   function @{term "\<lambda>s. p \<inter> \<AX> s"}.
 *}
 
 lemma AG_fp: "\<AG> p = p \<inter> \<AX> \<AG> p"
 proof -
-  have "mono (\<lambda>s. p \<inter> \<AX> s)" sorry (* by rule (auto simp add: AX_def EX_def) *)
-  then show ?thesis sorry (* by (simp only: AG_gfp) (rule gfp_unfold) *)
+  have "mono (\<lambda>s. p \<inter> \<AX> s)" by rule (auto simp add: AX_def EX_def)
+  then show ?thesis by (simp only: AG_gfp) (rule gfp_unfold)
 qed
 
 text {*
   This fact may be split up into two inequalities (merely using
   transitivity of @{text "\<subseteq>" }, which is an instance of the overloaded

   elementary monotonicity and distributivity rules.
 *}
 
 lemma AX_int: "\<AX> (p \<inter> q) = \<AX> p \<inter> \<AX> q" by auto 
 lemma AX_mono: "p \<subseteq> q \<Longrightarrow> \<AX> p \<subseteq> \<AX> q" by auto
-lemma AG_mono: "p \<subseteq> q \<Longrightarrow> \<AG> p \<subseteq> \<AG> q" by (simp only: AG_gfp, rule gfp_mono) auto 
+lemma AG_mono: "p \<subseteq> q \<Longrightarrow> \<AG> p \<subseteq> \<AG> q"
+  by (simp only: AG_gfp, rule gfp_mono) auto 
 
 text {*
   The formula @{term "AG p"} implies @{term "AX p"} (we use
   substitution of @{text "\<subseteq>"} with monotonicity).
 *}

     ultimately show "\<AG> p \<subseteq> \<AG> p \<inter> \<AX> \<AG> p" ..
   qed
 qed
 
 text {*
-  \smallskip We now give an alternative characterization of the
-  @{text "\<AG>"} operator, which describes the @{text "\<AG>"}
-  operator in an ``operational'' way by tree induction:
-  In a state holds @{term "AG p"} iff
-  in that state holds @{term p}, and in all reachable states @{term s}
-  follows from the fact that @{term p} holds in @{term s}, that @{term
-  p} also holds in all successor states of @{term s}.  We use the
-  co-induction principle @{thm [source] AG_I} to establish this in a
-  purely algebraic manner.
+  \smallskip We now give an alternative characterization of the @{text
+  "\<AG>"} operator, which describes the @{text "\<AG>"} operator in
+  an ``operational'' way by tree induction: In a state holds @{term
+  "AG p"} iff in that state holds @{term p}, and in all reachable
+  states @{term s} follows from the fact that @{term p} holds in
+  @{term s}, that @{term p} also holds in all successor states of
+  @{term s}.  We use the co-induction principle @{thm [source] AG_I}
+  to establish this in a purely algebraic manner.
 *}
 
 theorem AG_induct: "p \<inter> \<AG> (p \<rightarrow> \<AX> p) = \<AG> p"
 proof
   show "p \<inter> \<AG> (p \<rightarrow> \<AX> p) \<subseteq> \<AG> p"  (is "?lhs \<subseteq> _")