(* Title: HOL/ex/CTL.thy
Author: Gertrud Bauer
*)
section \<open>CTL formulae\<close>
theory CTL
imports Main
begin
text \<open>
We formalize basic concepts of Computational Tree Logic (CTL) @{cite
"McMillan-PhDThesis" and "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.
\<close>
lemmas [intro!] = Int_greatest Un_upper2 Un_upper1 Int_lower1 Int_lower2
type_synonym 'a ctl = "'a set"
definition
imp :: "'a ctl \<Rightarrow> 'a ctl \<Rightarrow> 'a ctl" (infixr "\<rightarrow>" 75) where
"p \<rightarrow> q = - p \<union> q"
lemma [intro!]: "p \<inter> p \<rightarrow> q \<subseteq> q" unfolding imp_def by auto
lemma [intro!]: "p \<subseteq> (q \<rightarrow> p)" unfolding imp_def by rule
text \<open>
\<^smallskip>
The CTL path operators are more interesting; they are based on an arbitrary,
but fixed model \<open>\<M>\<close>, which is simply a transition relation over states
@{typ 'a}.
\<close>
axiomatization \<M> :: "('a \<times> 'a) set"
text \<open>
The operators \<open>\<EX>\<close>, \<open>\<EF>\<close>, \<open>\<EG>\<close> are taken as primitives, while
\<open>\<AX>\<close>, \<open>\<AF>\<close>, \<open>\<AG>\<close> are defined as derived ones. The formula \<open>\<EX> p\<close>
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 \<open>\<EF> p\<close> holds in a state @{term s}, iff there is a path in
\<open>\<M>\<close>, starting from @{term s}, such that there exists a state @{term s'} on
the path, such that @{term p} holds in @{term s'}. The formula \<open>\<EG> p\<close>
holds in a state @{term s}, iff there is a path, starting from @{term s},
such that for all states @{term s'} on the path, @{term p} holds in @{term
s'}. It is easy to see that \<open>\<EF> p\<close> and \<open>\<EG> p\<close> may be expressed using
least and greatest fixed points @{cite "McMillan-PhDThesis"}.
\<close>
definition EX ("\<EX> _" [80] 90)
where [simp]: "\<EX> p = {s. \<exists>s'. (s, s') \<in> \<M> \<and> s' \<in> p}"
definition EF ("\<EF> _" [80] 90)
where [simp]: "\<EF> p = lfp (\<lambda>s. p \<union> \<EX> s)"
definition EG ("\<EG> _" [80] 90)
where [simp]: "\<EG> p = gfp (\<lambda>s. p \<inter> \<EX> s)"
text \<open>
\<open>\<AX>\<close>, \<open>\<AF>\<close> and \<open>\<AG>\<close> are now defined dually in terms of \<open>\<EX>\<close>,
\<open>\<EF>\<close> and \<open>\<EG>\<close>.
\<close>
definition AX ("\<AX> _" [80] 90)
where [simp]: "\<AX> p = - \<EX> - p"
definition AF ("\<AF> _" [80] 90)
where [simp]: "\<AF> p = - \<EG> - p"
definition AG ("\<AG> _" [80] 90)
where [simp]: "\<AG> p = - \<EF> - p"
subsection \<open>Basic fixed point properties\<close>
text \<open>
First of all, we use the de-Morgan property of fixed points.
\<close>
lemma lfp_gfp: "lfp f = - gfp (\<lambda>s::'a set. - (f (- s)))"
proof
show "lfp f \<subseteq> - gfp (\<lambda>s. - f (- s))"
proof
fix x assume l: "x \<in> lfp f"
show "x \<in> - gfp (\<lambda>s. - f (- s))"
proof
assume "x \<in> gfp (\<lambda>s. - f (- s))"
then obtain u where "x \<in> u" and "u \<subseteq> - f (- u)"
by (auto simp add: gfp_def)
then have "f (- u) \<subseteq> - u" by auto
then have "lfp f \<subseteq> - u" by (rule lfp_lowerbound)
from l and this have "x \<notin> u" by auto
with \<open>x \<in> u\<close> show False by contradiction
qed
qed
show "- gfp (\<lambda>s. - f (- s)) \<subseteq> lfp f"
proof (rule lfp_greatest)
fix u assume "f u \<subseteq> u"
then have "- u \<subseteq> - f u" by auto
then have "- u \<subseteq> - f (- (- u))" by simp
then have "- u \<subseteq> gfp (\<lambda>s. - f (- s))" by (rule gfp_upperbound)
then show "- gfp (\<lambda>s. - f (- s)) \<subseteq> u" by auto
qed
qed
lemma lfp_gfp': "- lfp f = gfp (\<lambda>s::'a set. - (f (- s)))"
by (simp add: lfp_gfp)
lemma gfp_lfp': "- gfp f = lfp (\<lambda>s::'a set. - (f (- s)))"
by (simp add: lfp_gfp)
text \<open>
In order to give dual fixed point representations of @{term "\<AF> p"} and
@{term "\<AG> p"}:
\<close>
lemma AF_lfp: "\<AF> p = lfp (\<lambda>s. p \<union> \<AX> s)"
by (simp add: lfp_gfp)
lemma AG_gfp: "\<AG> p = gfp (\<lambda>s. p \<inter> \<AX> s)"
by (simp add: lfp_gfp)
lemma EF_fp: "\<EF> p = p \<union> \<EX> \<EF> p"
proof -
have "mono (\<lambda>s. p \<union> \<EX> s)" by rule auto
then show ?thesis by (simp only: EF_def) (rule lfp_unfold)
qed
lemma AF_fp: "\<AF> p = p \<union> \<AX> \<AF> p"
proof -
have "mono (\<lambda>s. p \<union> \<AX> s)" by rule auto
then show ?thesis by (simp only: AF_lfp) (rule lfp_unfold)
qed
lemma EG_fp: "\<EG> p = p \<inter> \<EX> \<EG> p"
proof -
have "mono (\<lambda>s. p \<inter> \<EX> s)" by rule auto
then show ?thesis by (simp only: EG_def) (rule gfp_unfold)
qed
text \<open>
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"}.
\<close>
lemma AG_fp: "\<AG> p = p \<inter> \<AX> \<AG> p"
proof -
have "mono (\<lambda>s. p \<inter> \<AX> s)" by rule auto
then show ?thesis by (simp only: AG_gfp) (rule gfp_unfold)
qed
text \<open>
This fact may be split up into two inequalities (merely using transitivity
of \<open>\<subseteq>\<close>, which is an instance of the overloaded \<open>\<le>\<close> in Isabelle/HOL).
\<close>
lemma AG_fp_1: "\<AG> p \<subseteq> p"
proof -
note AG_fp also have "p \<inter> \<AX> \<AG> p \<subseteq> p" by auto
finally show ?thesis .
qed
lemma AG_fp_2: "\<AG> p \<subseteq> \<AX> \<AG> p"
proof -
note AG_fp also have "p \<inter> \<AX> \<AG> p \<subseteq> \<AX> \<AG> p" by auto
finally show ?thesis .
qed
text \<open>
On the other hand, we have from the Knaster-Tarski fixed point theorem that
any other post-fixed point of @{term "\<lambda>s. p \<inter> \<AX> s"} is smaller than
@{term "\<AG> p"}. A post-fixed point is a set of states @{term q} such that
@{term "q \<subseteq> p \<inter> \<AX> q"}. This leads to the following co-induction
principle for @{term "\<AG> p"}.
\<close>
lemma AG_I: "q \<subseteq> p \<inter> \<AX> q \<Longrightarrow> q \<subseteq> \<AG> p"
by (simp only: AG_gfp) (rule gfp_upperbound)
subsection \<open>The tree induction principle \label{sec:calc-ctl-tree-induct}\<close>
text \<open>
With the most basic facts available, we are now able to establish a few more
interesting results, leading to the \<^emph>\<open>tree induction\<close> principle for \<open>\<AG>\<close>
(see below). We will use some elementary monotonicity and distributivity
rules.
\<close>
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
text \<open>
The formula @{term "AG p"} implies @{term "AX p"} (we use substitution of
\<open>\<subseteq>\<close> with monotonicity).
\<close>
lemma AG_AX: "\<AG> p \<subseteq> \<AX> p"
proof -
have "\<AG> p \<subseteq> \<AX> \<AG> p" by (rule AG_fp_2)
also have "\<AG> p \<subseteq> p" by (rule AG_fp_1)
moreover note AX_mono
finally show ?thesis .
qed
text \<open>
Furthermore we show idempotency of the \<open>\<AG>\<close> operator. The proof is a good
example of how accumulated facts may get used to feed a single rule step.
\<close>
lemma AG_AG: "\<AG> \<AG> p = \<AG> p"
proof
show "\<AG> \<AG> p \<subseteq> \<AG> p" by (rule AG_fp_1)
next
show "\<AG> p \<subseteq> \<AG> \<AG> p"
proof (rule AG_I)
have "\<AG> p \<subseteq> \<AG> p" ..
moreover have "\<AG> p \<subseteq> \<AX> \<AG> p" by (rule AG_fp_2)
ultimately show "\<AG> p \<subseteq> \<AG> p \<inter> \<AX> \<AG> p" ..
qed
qed
text \<open>
\<^smallskip>
We now give an alternative characterization of the \<open>\<AG>\<close> operator, which
describes the \<open>\<AG>\<close> 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.
\<close>
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> _")
proof (rule AG_I)
show "?lhs \<subseteq> p \<inter> \<AX> ?lhs"
proof
show "?lhs \<subseteq> p" ..
show "?lhs \<subseteq> \<AX> ?lhs"
proof -
{
have "\<AG> (p \<rightarrow> \<AX> p) \<subseteq> p \<rightarrow> \<AX> p" by (rule AG_fp_1)
also have "p \<inter> p \<rightarrow> \<AX> p \<subseteq> \<AX> p" ..
finally have "?lhs \<subseteq> \<AX> p" by auto
}
moreover
{
have "p \<inter> \<AG> (p \<rightarrow> \<AX> p) \<subseteq> \<AG> (p \<rightarrow> \<AX> p)" ..
also have "\<dots> \<subseteq> \<AX> \<dots>" by (rule AG_fp_2)
finally have "?lhs \<subseteq> \<AX> \<AG> (p \<rightarrow> \<AX> p)" .
}
ultimately have "?lhs \<subseteq> \<AX> p \<inter> \<AX> \<AG> (p \<rightarrow> \<AX> p)" ..
also have "\<dots> = \<AX> ?lhs" by (simp only: AX_int)
finally show ?thesis .
qed
qed
qed
next
show "\<AG> p \<subseteq> p \<inter> \<AG> (p \<rightarrow> \<AX> p)"
proof
show "\<AG> p \<subseteq> p" by (rule AG_fp_1)
show "\<AG> p \<subseteq> \<AG> (p \<rightarrow> \<AX> p)"
proof -
have "\<AG> p = \<AG> \<AG> p" by (simp only: AG_AG)
also have "\<AG> p \<subseteq> \<AX> p" by (rule AG_AX) moreover note AG_mono
also have "\<AX> p \<subseteq> (p \<rightarrow> \<AX> p)" .. moreover note AG_mono
finally show ?thesis .
qed
qed
qed
subsection \<open>An application of tree induction \label{sec:calc-ctl-commute}\<close>
text \<open>
Further interesting properties of CTL expressions may be demonstrated with
the help of tree induction; here we show that \<open>\<AX>\<close> and \<open>\<AG>\<close> commute.
\<close>
theorem AG_AX_commute: "\<AG> \<AX> p = \<AX> \<AG> p"
proof -
have "\<AG> \<AX> p = \<AX> p \<inter> \<AX> \<AG> \<AX> p" by (rule AG_fp)
also have "\<dots> = \<AX> (p \<inter> \<AG> \<AX> p)" by (simp only: AX_int)
also have "p \<inter> \<AG> \<AX> p = \<AG> p" (is "?lhs = _")
proof
have "\<AX> p \<subseteq> p \<rightarrow> \<AX> p" ..
also have "p \<inter> \<AG> (p \<rightarrow> \<AX> p) = \<AG> p" by (rule AG_induct)
also note Int_mono AG_mono
ultimately show "?lhs \<subseteq> \<AG> p" by fast
next
have "\<AG> p \<subseteq> p" by (rule AG_fp_1)
moreover
{
have "\<AG> p = \<AG> \<AG> p" by (simp only: AG_AG)
also have "\<AG> p \<subseteq> \<AX> p" by (rule AG_AX)
also note AG_mono
ultimately have "\<AG> p \<subseteq> \<AG> \<AX> p" .
}
ultimately show "\<AG> p \<subseteq> ?lhs" ..
qed
finally show ?thesis .
qed
end