diff -r 1b237d147cc4 -r ae0ca486bd3f src/HOL/ex/CTL.thy
--- 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