--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy Tue Aug 13 14:20:22 2013 +0200
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy Tue Aug 13 16:25:47 2013 +0200
@@ -205,21 +205,21 @@
definition AI_wn :: "com \<Rightarrow> 'av st option acom option" where
"AI_wn = pfp_wn (step' \<top>)"
-lemma AI_wn_sound: "AI_wn c = Some c' \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c c'"
+lemma AI_wn_sound: "AI_wn c = Some c' \<Longrightarrow> CS c \<le> \<gamma>\<^sub>c c'"
proof(simp add: CS_def AI_wn_def)
assume 1: "pfp_wn (step' \<top>) c = Some c'"
from pfp_wn_pfp[OF mono_step'2 1]
have 2: "step' \<top> c' \<sqsubseteq> c'" .
- have 3: "strip (\<gamma>\<^isub>c (step' \<top> c')) = c" by(simp add: strip_pfp_wn[OF _ 1])
- have "lfp (step UNIV) c \<le> \<gamma>\<^isub>c (step' \<top> c')"
+ have 3: "strip (\<gamma>\<^sub>c (step' \<top> c')) = c" by(simp add: strip_pfp_wn[OF _ 1])
+ have "lfp (step UNIV) c \<le> \<gamma>\<^sub>c (step' \<top> c')"
proof(rule lfp_lowerbound[simplified,OF 3])
- show "step UNIV (\<gamma>\<^isub>c (step' \<top> c')) \<le> \<gamma>\<^isub>c (step' \<top> c')"
+ show "step UNIV (\<gamma>\<^sub>c (step' \<top> c')) \<le> \<gamma>\<^sub>c (step' \<top> c')"
proof(rule step_preserves_le[OF _ _])
- show "UNIV \<subseteq> \<gamma>\<^isub>o \<top>" by simp
- show "\<gamma>\<^isub>c (step' \<top> c') \<le> \<gamma>\<^isub>c c'" by(rule mono_gamma_c[OF 2])
+ show "UNIV \<subseteq> \<gamma>\<^sub>o \<top>" by simp
+ show "\<gamma>\<^sub>c (step' \<top> c') \<le> \<gamma>\<^sub>c c'" by(rule mono_gamma_c[OF 2])
qed
qed
- from this 2 show "lfp (step UNIV) c \<le> \<gamma>\<^isub>c c'"
+ from this 2 show "lfp (step UNIV) c \<le> \<gamma>\<^sub>c c'"
by (blast intro: mono_gamma_c order_trans)
qed