tuned notation;
authorwenzelm
Tue Apr 26 11:56:06 2016 +0200 (2016-04-26 ago)
changeset 63055ae0ca486bd3f
parent 63054 1b237d147cc4
child 63056 9b95ae9ec671
tuned notation;
src/HOL/ex/CTL.thy
src/HOL/ex/document/root.tex
     1.1 --- a/src/HOL/ex/CTL.thy	Tue Apr 26 11:38:19 2016 +0200
     1.2 +++ b/src/HOL/ex/CTL.thy	Tue Apr 26 11:56:06 2016 +0200
     1.3 @@ -42,37 +42,38 @@
     1.4  axiomatization \<M> :: "('a \<times> 'a) set"
     1.5  
     1.6  text \<open>
     1.7 -  The operators \<open>\<EX>\<close>, \<open>\<EF>\<close>, \<open>\<EG>\<close> are taken as primitives, while
     1.8 -  \<open>\<AX>\<close>, \<open>\<AF>\<close>, \<open>\<AG>\<close> are defined as derived ones. The formula \<open>\<EX> p\<close>
     1.9 -  holds in a state @{term s}, iff there is a successor state @{term s'} (with
    1.10 -  respect to the model @{term \<M>}), such that @{term p} holds in @{term s'}.
    1.11 -  The formula \<open>\<EF> p\<close> holds in a state @{term s}, iff there is a path in
    1.12 -  \<open>\<M>\<close>, starting from @{term s}, such that there exists a state @{term s'} on
    1.13 -  the path, such that @{term p} holds in @{term s'}. The formula \<open>\<EG> p\<close>
    1.14 -  holds in a state @{term s}, iff there is a path, starting from @{term s},
    1.15 -  such that for all states @{term s'} on the path, @{term p} holds in @{term
    1.16 -  s'}. It is easy to see that \<open>\<EF> p\<close> and \<open>\<EG> p\<close> may be expressed using
    1.17 -  least and greatest fixed points @{cite "McMillan-PhDThesis"}.
    1.18 +  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>,
    1.19 +  \<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
    1.20 +  state \<open>s\<close>, iff there is a successor state \<open>s'\<close> (with respect to the model
    1.21 +  \<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
    1.22 +  \<open>s\<close>, iff there is a path in \<open>\<M>\<close>, starting from \<open>s\<close>, such that there exists a
    1.23 +  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>
    1.24 +  holds in a state \<open>s\<close>, iff there is a path, starting from \<open>s\<close>, such that for
    1.25 +  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
    1.26 +  p\<close> and \<open>\<^bold>E\<^bold>G p\<close> may be expressed using least and greatest fixed points
    1.27 +  @{cite "McMillan-PhDThesis"}.
    1.28  \<close>
    1.29  
    1.30 -definition EX  ("\<EX> _" [80] 90)
    1.31 -  where [simp]: "\<EX> p = {s. \<exists>s'. (s, s') \<in> \<M> \<and> s' \<in> p}"
    1.32 -definition EF ("\<EF> _" [80] 90)
    1.33 -  where [simp]: "\<EF> p = lfp (\<lambda>s. p \<union> \<EX> s)"
    1.34 -definition EG ("\<EG> _" [80] 90)
    1.35 -  where [simp]: "\<EG> p = gfp (\<lambda>s. p \<inter> \<EX> s)"
    1.36 +definition EX  ("\<^bold>E\<^bold>X _" [80] 90)
    1.37 +  where [simp]: "\<^bold>E\<^bold>X p = {s. \<exists>s'. (s, s') \<in> \<M> \<and> s' \<in> p}"
    1.38 +
    1.39 +definition EF ("\<^bold>E\<^bold>F _" [80] 90)
    1.40 +  where [simp]: "\<^bold>E\<^bold>F p = lfp (\<lambda>s. p \<union> \<^bold>E\<^bold>X s)"
    1.41 +
    1.42 +definition EG ("\<^bold>E\<^bold>G _" [80] 90)
    1.43 +  where [simp]: "\<^bold>E\<^bold>G p = gfp (\<lambda>s. p \<inter> \<^bold>E\<^bold>X s)"
    1.44  
    1.45  text \<open>
    1.46 -  \<open>\<AX>\<close>, \<open>\<AF>\<close> and \<open>\<AG>\<close> are now defined dually in terms of \<open>\<EX>\<close>,
    1.47 -  \<open>\<EF>\<close> and \<open>\<EG>\<close>.
    1.48 +  \<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>,
    1.49 +  \<open>\<^bold>E\<^bold>F\<close> and \<open>\<^bold>E\<^bold>G\<close>.
    1.50  \<close>
    1.51  
    1.52 -definition AX  ("\<AX> _" [80] 90)
    1.53 -  where [simp]: "\<AX> p = - \<EX> - p"
    1.54 -definition AF  ("\<AF> _" [80] 90)
    1.55 -  where [simp]: "\<AF> p = - \<EG> - p"
    1.56 -definition AG  ("\<AG> _" [80] 90)
    1.57 -  where [simp]: "\<AG> p = - \<EF> - p"
    1.58 +definition AX  ("\<^bold>A\<^bold>X _" [80] 90)
    1.59 +  where [simp]: "\<^bold>A\<^bold>X p = - \<^bold>E\<^bold>X - p"
    1.60 +definition AF  ("\<^bold>A\<^bold>F _" [80] 90)
    1.61 +  where [simp]: "\<^bold>A\<^bold>F p = - \<^bold>E\<^bold>G - p"
    1.62 +definition AG  ("\<^bold>A\<^bold>G _" [80] 90)
    1.63 +  where [simp]: "\<^bold>A\<^bold>G p = - \<^bold>E\<^bold>F - p"
    1.64  
    1.65  
    1.66  subsection \<open>Basic fixed point properties\<close>
    1.67 @@ -114,43 +115,44 @@
    1.68    by (simp add: lfp_gfp)
    1.69  
    1.70  text \<open>
    1.71 -  In order to give dual fixed point representations of @{term "\<AF> p"} and
    1.72 -  @{term "\<AG> p"}:
    1.73 +  In order to give dual fixed point representations of @{term "\<^bold>A\<^bold>F p"} and
    1.74 +  @{term "\<^bold>A\<^bold>G p"}:
    1.75  \<close>
    1.76  
    1.77 -lemma AF_lfp: "\<AF> p = lfp (\<lambda>s. p \<union> \<AX> s)"
    1.78 -  by (simp add: lfp_gfp)
    1.79 -lemma AG_gfp: "\<AG> p = gfp (\<lambda>s. p \<inter> \<AX> s)"
    1.80 +lemma AF_lfp: "\<^bold>A\<^bold>F p = lfp (\<lambda>s. p \<union> \<^bold>A\<^bold>X s)"
    1.81    by (simp add: lfp_gfp)
    1.82  
    1.83 -lemma EF_fp: "\<EF> p = p \<union> \<EX> \<EF> p"
    1.84 +lemma AG_gfp: "\<^bold>A\<^bold>G p = gfp (\<lambda>s. p \<inter> \<^bold>A\<^bold>X s)"
    1.85 +  by (simp add: lfp_gfp)
    1.86 +
    1.87 +lemma EF_fp: "\<^bold>E\<^bold>F p = p \<union> \<^bold>E\<^bold>X \<^bold>E\<^bold>F p"
    1.88  proof -
    1.89 -  have "mono (\<lambda>s. p \<union> \<EX> s)" by rule auto
    1.90 +  have "mono (\<lambda>s. p \<union> \<^bold>E\<^bold>X s)" by rule auto
    1.91    then show ?thesis by (simp only: EF_def) (rule lfp_unfold)
    1.92  qed
    1.93  
    1.94 -lemma AF_fp: "\<AF> p = p \<union> \<AX> \<AF> p"
    1.95 +lemma AF_fp: "\<^bold>A\<^bold>F p = p \<union> \<^bold>A\<^bold>X \<^bold>A\<^bold>F p"
    1.96  proof -
    1.97 -  have "mono (\<lambda>s. p \<union> \<AX> s)" by rule auto
    1.98 +  have "mono (\<lambda>s. p \<union> \<^bold>A\<^bold>X s)" by rule auto
    1.99    then show ?thesis by (simp only: AF_lfp) (rule lfp_unfold)
   1.100  qed
   1.101  
   1.102 -lemma EG_fp: "\<EG> p = p \<inter> \<EX> \<EG> p"
   1.103 +lemma EG_fp: "\<^bold>E\<^bold>G p = p \<inter> \<^bold>E\<^bold>X \<^bold>E\<^bold>G p"
   1.104  proof -
   1.105 -  have "mono (\<lambda>s. p \<inter> \<EX> s)" by rule auto
   1.106 +  have "mono (\<lambda>s. p \<inter> \<^bold>E\<^bold>X s)" by rule auto
   1.107    then show ?thesis by (simp only: EG_def) (rule gfp_unfold)
   1.108  qed
   1.109  
   1.110  text \<open>
   1.111 -  From the greatest fixed point definition of @{term "\<AG> p"}, we derive as
   1.112 +  From the greatest fixed point definition of @{term "\<^bold>A\<^bold>G p"}, we derive as
   1.113    a consequence of the Knaster-Tarski theorem on the one hand that @{term
   1.114 -  "\<AG> p"} is a fixed point of the monotonic function
   1.115 -  @{term "\<lambda>s. p \<inter> \<AX> s"}.
   1.116 +  "\<^bold>A\<^bold>G p"} is a fixed point of the monotonic function
   1.117 +  @{term "\<lambda>s. p \<inter> \<^bold>A\<^bold>X s"}.
   1.118  \<close>
   1.119  
   1.120 -lemma AG_fp: "\<AG> p = p \<inter> \<AX> \<AG> p"
   1.121 +lemma AG_fp: "\<^bold>A\<^bold>G p = p \<inter> \<^bold>A\<^bold>X \<^bold>A\<^bold>G p"
   1.122  proof -
   1.123 -  have "mono (\<lambda>s. p \<inter> \<AX> s)" by rule auto
   1.124 +  have "mono (\<lambda>s. p \<inter> \<^bold>A\<^bold>X s)" by rule auto
   1.125    then show ?thesis by (simp only: AG_gfp) (rule gfp_unfold)
   1.126  qed
   1.127  
   1.128 @@ -159,27 +161,27 @@
   1.129    of \<open>\<subseteq>\<close>, which is an instance of the overloaded \<open>\<le>\<close> in Isabelle/HOL).
   1.130  \<close>
   1.131  
   1.132 -lemma AG_fp_1: "\<AG> p \<subseteq> p"
   1.133 +lemma AG_fp_1: "\<^bold>A\<^bold>G p \<subseteq> p"
   1.134  proof -
   1.135 -  note AG_fp also have "p \<inter> \<AX> \<AG> p \<subseteq> p" by auto
   1.136 +  note AG_fp also have "p \<inter> \<^bold>A\<^bold>X \<^bold>A\<^bold>G p \<subseteq> p" by auto
   1.137    finally show ?thesis .
   1.138  qed
   1.139  
   1.140 -lemma AG_fp_2: "\<AG> p \<subseteq> \<AX> \<AG> p"
   1.141 +lemma AG_fp_2: "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>X \<^bold>A\<^bold>G p"
   1.142  proof -
   1.143 -  note AG_fp also have "p \<inter> \<AX> \<AG> p \<subseteq> \<AX> \<AG> p" by auto
   1.144 +  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
   1.145    finally show ?thesis .
   1.146  qed
   1.147  
   1.148  text \<open>
   1.149    On the other hand, we have from the Knaster-Tarski fixed point theorem that
   1.150 -  any other post-fixed point of @{term "\<lambda>s. p \<inter> \<AX> s"} is smaller than
   1.151 -  @{term "\<AG> p"}. A post-fixed point is a set of states @{term q} such that
   1.152 -  @{term "q \<subseteq> p \<inter> \<AX> q"}. This leads to the following co-induction
   1.153 -  principle for @{term "\<AG> p"}.
   1.154 +  any other post-fixed point of @{term "\<lambda>s. p \<inter> \<^bold>A\<^bold>X s"} is smaller than
   1.155 +  @{term "\<^bold>A\<^bold>G p"}. A post-fixed point is a set of states \<open>q\<close> such that @{term
   1.156 +  "q \<subseteq> p \<inter> \<^bold>A\<^bold>X q"}. This leads to the following co-induction principle for
   1.157 +  @{term "\<^bold>A\<^bold>G p"}.
   1.158  \<close>
   1.159  
   1.160 -lemma AG_I: "q \<subseteq> p \<inter> \<AX> q \<Longrightarrow> q \<subseteq> \<AG> p"
   1.161 +lemma AG_I: "q \<subseteq> p \<inter> \<^bold>A\<^bold>X q \<Longrightarrow> q \<subseteq> \<^bold>A\<^bold>G p"
   1.162    by (simp only: AG_gfp) (rule gfp_upperbound)
   1.163  
   1.164  
   1.165 @@ -187,92 +189,91 @@
   1.166  
   1.167  text \<open>
   1.168    With the most basic facts available, we are now able to establish a few more
   1.169 -  interesting results, leading to the \<^emph>\<open>tree induction\<close> principle for \<open>\<AG>\<close>
   1.170 +  interesting results, leading to the \<^emph>\<open>tree induction\<close> principle for \<open>\<^bold>A\<^bold>G\<close>
   1.171    (see below). We will use some elementary monotonicity and distributivity
   1.172    rules.
   1.173  \<close>
   1.174  
   1.175 -lemma AX_int: "\<AX> (p \<inter> q) = \<AX> p \<inter> \<AX> q" by auto 
   1.176 -lemma AX_mono: "p \<subseteq> q \<Longrightarrow> \<AX> p \<subseteq> \<AX> q" by auto
   1.177 -lemma AG_mono: "p \<subseteq> q \<Longrightarrow> \<AG> p \<subseteq> \<AG> q"
   1.178 -  by (simp only: AG_gfp, rule gfp_mono) auto 
   1.179 +lemma AX_int: "\<^bold>A\<^bold>X (p \<inter> q) = \<^bold>A\<^bold>X p \<inter> \<^bold>A\<^bold>X q" by auto
   1.180 +lemma AX_mono: "p \<subseteq> q \<Longrightarrow> \<^bold>A\<^bold>X p \<subseteq> \<^bold>A\<^bold>X q" by auto
   1.181 +lemma AG_mono: "p \<subseteq> q \<Longrightarrow> \<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>G q"
   1.182 +  by (simp only: AG_gfp, rule gfp_mono) auto
   1.183  
   1.184  text \<open>
   1.185    The formula @{term "AG p"} implies @{term "AX p"} (we use substitution of
   1.186    \<open>\<subseteq>\<close> with monotonicity).
   1.187  \<close>
   1.188  
   1.189 -lemma AG_AX: "\<AG> p \<subseteq> \<AX> p"
   1.190 +lemma AG_AX: "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>X p"
   1.191  proof -
   1.192 -  have "\<AG> p \<subseteq> \<AX> \<AG> p" by (rule AG_fp_2)
   1.193 -  also have "\<AG> p \<subseteq> p" by (rule AG_fp_1)
   1.194 +  have "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>X \<^bold>A\<^bold>G p" by (rule AG_fp_2)
   1.195 +  also have "\<^bold>A\<^bold>G p \<subseteq> p" by (rule AG_fp_1)
   1.196    moreover note AX_mono
   1.197    finally show ?thesis .
   1.198  qed
   1.199  
   1.200  text \<open>
   1.201 -  Furthermore we show idempotency of the \<open>\<AG>\<close> operator. The proof is a good
   1.202 +  Furthermore we show idempotency of the \<open>\<^bold>A\<^bold>G\<close> operator. The proof is a good
   1.203    example of how accumulated facts may get used to feed a single rule step.
   1.204  \<close>
   1.205  
   1.206 -lemma AG_AG: "\<AG> \<AG> p = \<AG> p"
   1.207 +lemma AG_AG: "\<^bold>A\<^bold>G \<^bold>A\<^bold>G p = \<^bold>A\<^bold>G p"
   1.208  proof
   1.209 -  show "\<AG> \<AG> p \<subseteq> \<AG> p" by (rule AG_fp_1)
   1.210 +  show "\<^bold>A\<^bold>G \<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>G p" by (rule AG_fp_1)
   1.211  next
   1.212 -  show "\<AG> p \<subseteq> \<AG> \<AG> p"
   1.213 +  show "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>G \<^bold>A\<^bold>G p"
   1.214    proof (rule AG_I)
   1.215 -    have "\<AG> p \<subseteq> \<AG> p" ..
   1.216 -    moreover have "\<AG> p \<subseteq> \<AX> \<AG> p" by (rule AG_fp_2)
   1.217 -    ultimately show "\<AG> p \<subseteq> \<AG> p \<inter> \<AX> \<AG> p" ..
   1.218 +    have "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>G p" ..
   1.219 +    moreover have "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>X \<^bold>A\<^bold>G p" by (rule AG_fp_2)
   1.220 +    ultimately show "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>G p \<inter> \<^bold>A\<^bold>X \<^bold>A\<^bold>G p" ..
   1.221    qed
   1.222  qed
   1.223  
   1.224  text \<open>
   1.225    \<^smallskip>
   1.226 -  We now give an alternative characterization of the \<open>\<AG>\<close> operator, which
   1.227 -  describes the \<open>\<AG>\<close> operator in an ``operational'' way by tree induction:
   1.228 -  In a state holds @{term "AG p"} iff in that state holds @{term p}, and in
   1.229 -  all reachable states @{term s} follows from the fact that @{term p} holds in
   1.230 -  @{term s}, that @{term p} also holds in all successor states of @{term s}.
   1.231 -  We use the co-induction principle @{thm [source] AG_I} to establish this in
   1.232 -  a purely algebraic manner.
   1.233 +  We now give an alternative characterization of the \<open>\<^bold>A\<^bold>G\<close> operator, which
   1.234 +  describes the \<open>\<^bold>A\<^bold>G\<close> operator in an ``operational'' way by tree induction:
   1.235 +  In a state holds @{term "AG p"} iff in that state holds \<open>p\<close>, and in all
   1.236 +  reachable states \<open>s\<close> follows from the fact that \<open>p\<close> holds in \<open>s\<close>, that \<open>p\<close>
   1.237 +  also holds in all successor states of \<open>s\<close>. We use the co-induction principle
   1.238 +  @{thm [source] AG_I} to establish this in a purely algebraic manner.
   1.239  \<close>
   1.240  
   1.241 -theorem AG_induct: "p \<inter> \<AG> (p \<rightarrow> \<AX> p) = \<AG> p"
   1.242 +theorem AG_induct: "p \<inter> \<^bold>A\<^bold>G (p \<rightarrow> \<^bold>A\<^bold>X p) = \<^bold>A\<^bold>G p"
   1.243  proof
   1.244 -  show "p \<inter> \<AG> (p \<rightarrow> \<AX> p) \<subseteq> \<AG> p"  (is "?lhs \<subseteq> _")
   1.245 +  show "p \<inter> \<^bold>A\<^bold>G (p \<rightarrow> \<^bold>A\<^bold>X p) \<subseteq> \<^bold>A\<^bold>G p"  (is "?lhs \<subseteq> _")
   1.246    proof (rule AG_I)
   1.247 -    show "?lhs \<subseteq> p \<inter> \<AX> ?lhs"
   1.248 +    show "?lhs \<subseteq> p \<inter> \<^bold>A\<^bold>X ?lhs"
   1.249      proof
   1.250        show "?lhs \<subseteq> p" ..
   1.251 -      show "?lhs \<subseteq> \<AX> ?lhs"
   1.252 +      show "?lhs \<subseteq> \<^bold>A\<^bold>X ?lhs"
   1.253        proof -
   1.254          {
   1.255 -          have "\<AG> (p \<rightarrow> \<AX> p) \<subseteq> p \<rightarrow> \<AX> p" by (rule AG_fp_1)
   1.256 -          also have "p \<inter> p \<rightarrow> \<AX> p \<subseteq> \<AX> p" ..
   1.257 -          finally have "?lhs \<subseteq> \<AX> p" by auto
   1.258 -        }  
   1.259 +          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)
   1.260 +          also have "p \<inter> p \<rightarrow> \<^bold>A\<^bold>X p \<subseteq> \<^bold>A\<^bold>X p" ..
   1.261 +          finally have "?lhs \<subseteq> \<^bold>A\<^bold>X p" by auto
   1.262 +        }
   1.263          moreover
   1.264          {
   1.265 -          have "p \<inter> \<AG> (p \<rightarrow> \<AX> p) \<subseteq> \<AG> (p \<rightarrow> \<AX> p)" ..
   1.266 -          also have "\<dots> \<subseteq> \<AX> \<dots>" by (rule AG_fp_2)
   1.267 -          finally have "?lhs \<subseteq> \<AX> \<AG> (p \<rightarrow> \<AX> p)" .
   1.268 -        }  
   1.269 -        ultimately have "?lhs \<subseteq> \<AX> p \<inter> \<AX> \<AG> (p \<rightarrow> \<AX> p)" ..
   1.270 -        also have "\<dots> = \<AX> ?lhs" by (simp only: AX_int)
   1.271 +          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)" ..
   1.272 +          also have "\<dots> \<subseteq> \<^bold>A\<^bold>X \<dots>" by (rule AG_fp_2)
   1.273 +          finally have "?lhs \<subseteq> \<^bold>A\<^bold>X \<^bold>A\<^bold>G (p \<rightarrow> \<^bold>A\<^bold>X p)" .
   1.274 +        }
   1.275 +        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)" ..
   1.276 +        also have "\<dots> = \<^bold>A\<^bold>X ?lhs" by (simp only: AX_int)
   1.277          finally show ?thesis .
   1.278        qed
   1.279      qed
   1.280    qed
   1.281  next
   1.282 -  show "\<AG> p \<subseteq> p \<inter> \<AG> (p \<rightarrow> \<AX> p)"
   1.283 +  show "\<^bold>A\<^bold>G p \<subseteq> p \<inter> \<^bold>A\<^bold>G (p \<rightarrow> \<^bold>A\<^bold>X p)"
   1.284    proof
   1.285 -    show "\<AG> p \<subseteq> p" by (rule AG_fp_1)
   1.286 -    show "\<AG> p \<subseteq> \<AG> (p \<rightarrow> \<AX> p)"
   1.287 +    show "\<^bold>A\<^bold>G p \<subseteq> p" by (rule AG_fp_1)
   1.288 +    show "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>G (p \<rightarrow> \<^bold>A\<^bold>X p)"
   1.289      proof -
   1.290 -      have "\<AG> p = \<AG> \<AG> p" by (simp only: AG_AG)
   1.291 -      also have "\<AG> p \<subseteq> \<AX> p" by (rule AG_AX) moreover note AG_mono
   1.292 -      also have "\<AX> p \<subseteq> (p \<rightarrow> \<AX> p)" .. moreover note AG_mono
   1.293 +      have "\<^bold>A\<^bold>G p = \<^bold>A\<^bold>G \<^bold>A\<^bold>G p" by (simp only: AG_AG)
   1.294 +      also have "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>X p" by (rule AG_AX) moreover note AG_mono
   1.295 +      also have "\<^bold>A\<^bold>X p \<subseteq> (p \<rightarrow> \<^bold>A\<^bold>X p)" .. moreover note AG_mono
   1.296        finally show ?thesis .
   1.297      qed
   1.298    qed
   1.299 @@ -283,30 +284,30 @@
   1.300  
   1.301  text \<open>
   1.302    Further interesting properties of CTL expressions may be demonstrated with
   1.303 -  the help of tree induction; here we show that \<open>\<AX>\<close> and \<open>\<AG>\<close> commute.
   1.304 +  the help of tree induction; here we show that \<open>\<^bold>A\<^bold>X\<close> and \<open>\<^bold>A\<^bold>G\<close> commute.
   1.305  \<close>
   1.306  
   1.307 -theorem AG_AX_commute: "\<AG> \<AX> p = \<AX> \<AG> p"
   1.308 +theorem AG_AX_commute: "\<^bold>A\<^bold>G \<^bold>A\<^bold>X p = \<^bold>A\<^bold>X \<^bold>A\<^bold>G p"
   1.309  proof -
   1.310 -  have "\<AG> \<AX> p = \<AX> p \<inter> \<AX> \<AG> \<AX> p" by (rule AG_fp)
   1.311 -  also have "\<dots> = \<AX> (p \<inter> \<AG> \<AX> p)" by (simp only: AX_int)
   1.312 -  also have "p \<inter> \<AG> \<AX> p = \<AG> p"  (is "?lhs = _")
   1.313 -  proof  
   1.314 -    have "\<AX> p \<subseteq> p \<rightarrow> \<AX> p" ..
   1.315 -    also have "p \<inter> \<AG> (p \<rightarrow> \<AX> p) = \<AG> p" by (rule AG_induct)
   1.316 +  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)
   1.317 +  also have "\<dots> = \<^bold>A\<^bold>X (p \<inter> \<^bold>A\<^bold>G \<^bold>A\<^bold>X p)" by (simp only: AX_int)
   1.318 +  also have "p \<inter> \<^bold>A\<^bold>G \<^bold>A\<^bold>X p = \<^bold>A\<^bold>G p"  (is "?lhs = _")
   1.319 +  proof
   1.320 +    have "\<^bold>A\<^bold>X p \<subseteq> p \<rightarrow> \<^bold>A\<^bold>X p" ..
   1.321 +    also have "p \<inter> \<^bold>A\<^bold>G (p \<rightarrow> \<^bold>A\<^bold>X p) = \<^bold>A\<^bold>G p" by (rule AG_induct)
   1.322      also note Int_mono AG_mono
   1.323 -    ultimately show "?lhs \<subseteq> \<AG> p" by fast
   1.324 -  next  
   1.325 -    have "\<AG> p \<subseteq> p" by (rule AG_fp_1)
   1.326 -    moreover 
   1.327 +    ultimately show "?lhs \<subseteq> \<^bold>A\<^bold>G p" by fast
   1.328 +  next
   1.329 +    have "\<^bold>A\<^bold>G p \<subseteq> p" by (rule AG_fp_1)
   1.330 +    moreover
   1.331      {
   1.332 -      have "\<AG> p = \<AG> \<AG> p" by (simp only: AG_AG)
   1.333 -      also have "\<AG> p \<subseteq> \<AX> p" by (rule AG_AX)
   1.334 +      have "\<^bold>A\<^bold>G p = \<^bold>A\<^bold>G \<^bold>A\<^bold>G p" by (simp only: AG_AG)
   1.335 +      also have "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>X p" by (rule AG_AX)
   1.336        also note AG_mono
   1.337 -      ultimately have "\<AG> p \<subseteq> \<AG> \<AX> p" .
   1.338 -    } 
   1.339 -    ultimately show "\<AG> p \<subseteq> ?lhs" ..
   1.340 -  qed  
   1.341 +      ultimately have "\<^bold>A\<^bold>G p \<subseteq> \<^bold>A\<^bold>G \<^bold>A\<^bold>X p" .
   1.342 +    }
   1.343 +    ultimately show "\<^bold>A\<^bold>G p \<subseteq> ?lhs" ..
   1.344 +  qed
   1.345    finally show ?thesis .
   1.346  qed
   1.347  
     2.1 --- a/src/HOL/ex/document/root.tex	Tue Apr 26 11:38:19 2016 +0200
     2.2 +++ b/src/HOL/ex/document/root.tex	Tue Apr 26 11:56:06 2016 +0200
     2.3 @@ -10,14 +10,6 @@
     2.4  \urlstyle{rm}
     2.5  \isabellestyle{it}
     2.6  
     2.7 -\newcommand{\isasymEX}{\isamath{\mathrm{EX}}}
     2.8 -\newcommand{\isasymEF}{\isamath{\mathrm{EF}}}
     2.9 -\newcommand{\isasymEG}{\isamath{\mathrm{EG}}}
    2.10 -\newcommand{\isasymAX}{\isamath{\mathrm{AX}}}
    2.11 -\newcommand{\isasymAF}{\isamath{\mathrm{AF}}}
    2.12 -\newcommand{\isasymAG}{\isamath{\mathrm{AG}}}
    2.13 -
    2.14 -
    2.15  
    2.16  \begin{document}
    2.17