author wenzelm Tue Apr 26 11:56:06 2016 +0200 (2016-04-26 ago) changeset 63055 ae0ca486bd3f parent 63054 1b237d147cc4 child 63056 9b95ae9ec671
tuned notation;
 src/HOL/ex/CTL.thy file | annotate | diff | revisions src/HOL/ex/document/root.tex file | annotate | diff | revisions
     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.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.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