--- a/src/HOL/ex/CTL.thy Tue Apr 26 11:38:19 2016 +0200
+++ b/src/HOL/ex/CTL.thy Tue Apr 26 11:56:06 2016 +0200
@@ -42,37 +42,38 @@
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"}.
+ The operators \<open>\<^bold>E\<^bold>X\<close>, \<open>\<^bold>E\<^bold>F\<close>, \<open>\<^bold>E\<^bold>G\<close> are taken as primitives, while \<open>\<^bold>A\<^bold>X\<close>,
+ \<open>\<^bold>A\<^bold>F\<close>, \<open>\<^bold>A\<^bold>G\<close> are defined as derived ones. The formula \<open>\<^bold>E\<^bold>X p\<close> holds in a
+ state \<open>s\<close>, iff there is a successor state \<open>s'\<close> (with respect to the model
+ \<open>\<M>\<close>), such that \<open>p\<close> holds in \<open>s'\<close>. The formula \<open>\<^bold>E\<^bold>F p\<close> holds in a state
+ \<open>s\<close>, iff there is a path in \<open>\<M>\<close>, starting from \<open>s\<close>, such that there exists a
+ state \<open>s'\<close> on the path, such that \<open>p\<close> holds in \<open>s'\<close>. The formula \<open>\<^bold>E\<^bold>G p\<close>
+ holds in a state \<open>s\<close>, iff there is a path, starting from \<open>s\<close>, such that for
+ all states \<open>s'\<close> on the path, \<open>p\<close> holds in \<open>s'\<close>. It is easy to see that \<open>\<^bold>E\<^bold>F
+ p\<close> and \<open>\<^bold>E\<^bold>G 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)"
+definition EX ("\<^bold>E\<^bold>X _" [80] 90)
+ where [simp]: "\<^bold>E\<^bold>X p = {s. \<exists>s'. (s, s') \<in> \<M> \<and> s' \<in> p}"
+
+definition EF ("\<^bold>E\<^bold>F _" [80] 90)
+ where [simp]: "\<^bold>E\<^bold>F p = lfp (\<lambda>s. p \<union> \<^bold>E\<^bold>X s)"
+
+definition EG ("\<^bold>E\<^bold>G _" [80] 90)
+ where [simp]: "\<^bold>E\<^bold>G p = gfp (\<lambda>s. p \<inter> \<^bold>E\<^bold>X 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>.
+ \<open>\<^bold>A\<^bold>X\<close>, \<open>\<^bold>A\<^bold>F\<close> and \<open>\<^bold>A\<^bold>G\<close> are now defined dually in terms of \<open>\<^bold>E\<^bold>X\<close>,
+ \<open>\<^bold>E\<^bold>F\<close> and \<open>\<^bold>E\<^bold>G\<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"
+definition AX ("\<^bold>A\<^bold>X _" [80] 90)
+ where [simp]: "\<^bold>A\<^bold>X p = - \<^bold>E\<^bold>X - p"
+definition AF ("\<^bold>A\<^bold>F _" [80] 90)
+ where [simp]: "\<^bold>A\<^bold>F p = - \<^bold>E\<^bold>G - p"
+definition AG ("\<^bold>A\<^bold>G _" [80] 90)
+ where [simp]: "\<^bold>A\<^bold>G p = - \<^bold>E\<^bold>F - p"
subsection \<open>Basic fixed point properties\<close>
@@ -114,43 +115,44 @@
by (simp add: lfp_gfp)
text \<open>
- In order to give dual fixed point representations of @{term "\<AF> p"} and
- @{term "\<AG> p"}:
+ In order to give dual fixed point representations of @{term "\<^bold>A\<^bold>F p"} and
+ @{term "\<^bold>A\<^bold>G 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)"
+lemma AF_lfp: "\<^bold>A\<^bold>F p = lfp (\<lambda>s. p \<union> \<^bold>A\<^bold>X s)"
by (simp add: lfp_gfp)
-lemma EF_fp: "\<EF> p = p \<union> \<EX> \<EF> p"
+lemma AG_gfp: "\<^bold>A\<^bold>G p = gfp (\<lambda>s. p \<inter> \<^bold>A\<^bold>X s)"
+ by (simp add: lfp_gfp)
+
+lemma EF_fp: "\<^bold>E\<^bold>F p = p \<union> \<^bold>E\<^bold>X \<^bold>E\<^bold>F p"
proof -
- have "mono (\<lambda>s. p \<union> \<EX> s)" by rule auto
+ have "mono (\<lambda>s. p \<union> \<^bold>E\<^bold>X 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"
+lemma AF_fp: "\<^bold>A\<^bold>F p = p \<union> \<^bold>A\<^bold>X \<^bold>A\<^bold>F p"
proof -
- have "mono (\<lambda>s. p \<union> \<AX> s)" by rule auto
+ have "mono (\<lambda>s. p \<union> \<^bold>A\<^bold>X 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"
+lemma EG_fp: "\<^bold>E\<^bold>G p = p \<inter> \<^bold>E\<^bold>X \<^bold>E\<^bold>G p"
proof -
- have "mono (\<lambda>s. p \<inter> \<EX> s)" by rule auto
+ have "mono (\<lambda>s. p \<inter> \<^bold>E\<^bold>X 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
+ From the greatest fixed point definition of @{term "\<^bold>A\<^bold>G 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"}.
+ "\<^bold>A\<^bold>G p"} is a fixed point of the monotonic function
+ @{term "\<lambda>s. p \<inter> \<^bold>A\<^bold>X s"}.
\<close>
-lemma AG_fp: "\<AG> p = p \<inter> \<AX> \<AG> p"
+lemma AG_fp: "\<^bold>A\<^bold>G p = p \<inter> \<^bold>A\<^bold>X \<^bold>A\<^bold>G p"
proof -
- have "mono (\<lambda>s. p \<inter> \<AX> s)" by rule auto
+ have "mono (\<lambda>s. p \<inter> \<^bold>A\<^bold>X s)" by rule auto
then show ?thesis by (simp only: AG_gfp) (rule gfp_unfold)
qed
@@ -159,27 +161,27 @@
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"
+lemma AG_fp_1: "\<^bold>A\<^bold>G p \<subseteq> p"
proof -
- note AG_fp also have "p \<inter> \<AX> \<AG> p \<subseteq> p" by auto
+ note AG_fp also have "p \<inter> \<^bold>A\<^bold>X \<^bold>A\<^bold>G p \<subseteq> p" by auto
finally show ?thesis .
qed
-lemma AG_fp_2: "\<AG> p \<subseteq> \<AX> \<AG> p"
+lemma AG_fp_2: "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>X \<^bold>A\<^bold>G p"
proof -
- note AG_fp also have "p \<inter> \<AX> \<AG> p \<subseteq> \<AX> \<AG> p" by auto
+ note AG_fp also have "p \<inter> \<^bold>A\<^bold>X \<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>X \<^bold>A\<^bold>G 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"}.
+ any other post-fixed point of @{term "\<lambda>s. p \<inter> \<^bold>A\<^bold>X s"} is smaller than
+ @{term "\<^bold>A\<^bold>G p"}. A post-fixed point is a set of states \<open>q\<close> such that @{term
+ "q \<subseteq> p \<inter> \<^bold>A\<^bold>X q"}. This leads to the following co-induction principle for
+ @{term "\<^bold>A\<^bold>G p"}.
\<close>
-lemma AG_I: "q \<subseteq> p \<inter> \<AX> q \<Longrightarrow> q \<subseteq> \<AG> p"
+lemma AG_I: "q \<subseteq> p \<inter> \<^bold>A\<^bold>X q \<Longrightarrow> q \<subseteq> \<^bold>A\<^bold>G p"
by (simp only: AG_gfp) (rule gfp_upperbound)
@@ -187,92 +189,91 @@
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>
+ interesting results, leading to the \<^emph>\<open>tree induction\<close> principle for \<open>\<^bold>A\<^bold>G\<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
+lemma AX_int: "\<^bold>A\<^bold>X (p \<inter> q) = \<^bold>A\<^bold>X p \<inter> \<^bold>A\<^bold>X q" by auto
+lemma AX_mono: "p \<subseteq> q \<Longrightarrow> \<^bold>A\<^bold>X p \<subseteq> \<^bold>A\<^bold>X q" by auto
+lemma AG_mono: "p \<subseteq> q \<Longrightarrow> \<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>G 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"
+lemma AG_AX: "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>X 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)
+ have "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>X \<^bold>A\<^bold>G p" by (rule AG_fp_2)
+ also have "\<^bold>A\<^bold>G 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
+ Furthermore we show idempotency of the \<open>\<^bold>A\<^bold>G\<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"
+lemma AG_AG: "\<^bold>A\<^bold>G \<^bold>A\<^bold>G p = \<^bold>A\<^bold>G p"
proof
- show "\<AG> \<AG> p \<subseteq> \<AG> p" by (rule AG_fp_1)
+ show "\<^bold>A\<^bold>G \<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>G p" by (rule AG_fp_1)
next
- show "\<AG> p \<subseteq> \<AG> \<AG> p"
+ show "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>G \<^bold>A\<^bold>G 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" ..
+ have "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>G p" ..
+ moreover have "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>X \<^bold>A\<^bold>G p" by (rule AG_fp_2)
+ ultimately show "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>G p \<inter> \<^bold>A\<^bold>X \<^bold>A\<^bold>G 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.
+ We now give an alternative characterization of the \<open>\<^bold>A\<^bold>G\<close> operator, which
+ describes the \<open>\<^bold>A\<^bold>G\<close> operator in an ``operational'' way by tree induction:
+ In a state holds @{term "AG p"} iff in that state holds \<open>p\<close>, and in all
+ reachable states \<open>s\<close> follows from the fact that \<open>p\<close> holds in \<open>s\<close>, that \<open>p\<close>
+ also holds in all successor states of \<open>s\<close>. 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"
+theorem AG_induct: "p \<inter> \<^bold>A\<^bold>G (p \<rightarrow> \<^bold>A\<^bold>X p) = \<^bold>A\<^bold>G p"
proof
- show "p \<inter> \<AG> (p \<rightarrow> \<AX> p) \<subseteq> \<AG> p" (is "?lhs \<subseteq> _")
+ show "p \<inter> \<^bold>A\<^bold>G (p \<rightarrow> \<^bold>A\<^bold>X p) \<subseteq> \<^bold>A\<^bold>G p" (is "?lhs \<subseteq> _")
proof (rule AG_I)
- show "?lhs \<subseteq> p \<inter> \<AX> ?lhs"
+ show "?lhs \<subseteq> p \<inter> \<^bold>A\<^bold>X ?lhs"
proof
show "?lhs \<subseteq> p" ..
- show "?lhs \<subseteq> \<AX> ?lhs"
+ show "?lhs \<subseteq> \<^bold>A\<^bold>X ?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
- }
+ have "\<^bold>A\<^bold>G (p \<rightarrow> \<^bold>A\<^bold>X p) \<subseteq> p \<rightarrow> \<^bold>A\<^bold>X p" by (rule AG_fp_1)
+ also have "p \<inter> p \<rightarrow> \<^bold>A\<^bold>X p \<subseteq> \<^bold>A\<^bold>X p" ..
+ finally have "?lhs \<subseteq> \<^bold>A\<^bold>X 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)
+ have "p \<inter> \<^bold>A\<^bold>G (p \<rightarrow> \<^bold>A\<^bold>X p) \<subseteq> \<^bold>A\<^bold>G (p \<rightarrow> \<^bold>A\<^bold>X p)" ..
+ also have "\<dots> \<subseteq> \<^bold>A\<^bold>X \<dots>" by (rule AG_fp_2)
+ finally have "?lhs \<subseteq> \<^bold>A\<^bold>X \<^bold>A\<^bold>G (p \<rightarrow> \<^bold>A\<^bold>X p)" .
+ }
+ ultimately have "?lhs \<subseteq> \<^bold>A\<^bold>X p \<inter> \<^bold>A\<^bold>X \<^bold>A\<^bold>G (p \<rightarrow> \<^bold>A\<^bold>X p)" ..
+ also have "\<dots> = \<^bold>A\<^bold>X ?lhs" by (simp only: AX_int)
finally show ?thesis .
qed
qed
qed
next
- show "\<AG> p \<subseteq> p \<inter> \<AG> (p \<rightarrow> \<AX> p)"
+ show "\<^bold>A\<^bold>G p \<subseteq> p \<inter> \<^bold>A\<^bold>G (p \<rightarrow> \<^bold>A\<^bold>X p)"
proof
- show "\<AG> p \<subseteq> p" by (rule AG_fp_1)
- show "\<AG> p \<subseteq> \<AG> (p \<rightarrow> \<AX> p)"
+ show "\<^bold>A\<^bold>G p \<subseteq> p" by (rule AG_fp_1)
+ show "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>G (p \<rightarrow> \<^bold>A\<^bold>X 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
+ have "\<^bold>A\<^bold>G p = \<^bold>A\<^bold>G \<^bold>A\<^bold>G p" by (simp only: AG_AG)
+ also have "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>X p" by (rule AG_AX) moreover note AG_mono
+ also have "\<^bold>A\<^bold>X p \<subseteq> (p \<rightarrow> \<^bold>A\<^bold>X p)" .. moreover note AG_mono
finally show ?thesis .
qed
qed
@@ -283,30 +284,30 @@
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.
+ the help of tree induction; here we show that \<open>\<^bold>A\<^bold>X\<close> and \<open>\<^bold>A\<^bold>G\<close> commute.
\<close>
-theorem AG_AX_commute: "\<AG> \<AX> p = \<AX> \<AG> p"
+theorem AG_AX_commute: "\<^bold>A\<^bold>G \<^bold>A\<^bold>X p = \<^bold>A\<^bold>X \<^bold>A\<^bold>G 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)
+ have "\<^bold>A\<^bold>G \<^bold>A\<^bold>X p = \<^bold>A\<^bold>X p \<inter> \<^bold>A\<^bold>X \<^bold>A\<^bold>G \<^bold>A\<^bold>X p" by (rule AG_fp)
+ also have "\<dots> = \<^bold>A\<^bold>X (p \<inter> \<^bold>A\<^bold>G \<^bold>A\<^bold>X p)" by (simp only: AX_int)
+ also have "p \<inter> \<^bold>A\<^bold>G \<^bold>A\<^bold>X p = \<^bold>A\<^bold>G p" (is "?lhs = _")
+ proof
+ have "\<^bold>A\<^bold>X p \<subseteq> p \<rightarrow> \<^bold>A\<^bold>X p" ..
+ also have "p \<inter> \<^bold>A\<^bold>G (p \<rightarrow> \<^bold>A\<^bold>X p) = \<^bold>A\<^bold>G 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
+ ultimately show "?lhs \<subseteq> \<^bold>A\<^bold>G p" by fast
+ next
+ have "\<^bold>A\<^bold>G 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)
+ have "\<^bold>A\<^bold>G p = \<^bold>A\<^bold>G \<^bold>A\<^bold>G p" by (simp only: AG_AG)
+ also have "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>X p" by (rule AG_AX)
also note AG_mono
- ultimately have "\<AG> p \<subseteq> \<AG> \<AX> p" .
- }
- ultimately show "\<AG> p \<subseteq> ?lhs" ..
- qed
+ ultimately have "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>G \<^bold>A\<^bold>X p" .
+ }
+ ultimately show "\<^bold>A\<^bold>G p \<subseteq> ?lhs" ..
+ qed
finally show ?thesis .
qed