--- a/src/HOL/IMP/Abs_Int0.thy Sat Jan 07 12:39:46 2012 +0100
+++ b/src/HOL/IMP/Abs_Int0.thy Sat Jan 07 21:19:53 2012 +0100
@@ -124,9 +124,10 @@
lemma mono_update: "a \<sqsubseteq> a' \<Longrightarrow> S \<sqsubseteq> S' \<Longrightarrow> update S x a \<sqsubseteq> update S' x a'"
by(auto simp add: le_st_def lookup_def update_def)
-lemma step'_mono: "S \<sqsubseteq> S' \<Longrightarrow> step' S c \<sqsubseteq> step' S' c"
-apply(induction c arbitrary: S S')
-apply (auto simp: Let_def mono_update mono_aval' le_join_disj split: option.split)
+lemma mono_step': "S \<sqsubseteq> S' \<Longrightarrow> c \<sqsubseteq> c' \<Longrightarrow> step' S c \<sqsubseteq> step' S' c'"
+apply(induction c c' arbitrary: S S' rule: le_acom.induct)
+apply (auto simp: Let_def mono_update mono_aval' mono_post le_join_disj
+ split: option.split)
done
end
--- a/src/HOL/IMP/Abs_Int0_fun.thy Sat Jan 07 12:39:46 2012 +0100
+++ b/src/HOL/IMP/Abs_Int0_fun.thy Sat Jan 07 21:19:53 2012 +0100
@@ -372,6 +372,9 @@
subsubsection "Monotonicity"
+lemma mono_post: "c \<sqsubseteq> c' \<Longrightarrow> post c \<sqsubseteq> post c'"
+by(induction c c' rule: le_acom.induct) (auto)
+
locale Abs_Int_Fun_mono = Abs_Int_Fun +
assumes mono_plus': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow> plus' a1 a2 \<sqsubseteq> plus' b1 b2"
begin
@@ -382,9 +385,10 @@
lemma mono_update: "a \<sqsubseteq> a' \<Longrightarrow> S \<sqsubseteq> S' \<Longrightarrow> S(x := a) \<sqsubseteq> S'(x := a')"
by(simp add: le_fun_def)
-lemma step'_mono: "S \<sqsubseteq> S' \<Longrightarrow> step' S c \<sqsubseteq> step' S' c"
-apply(induction c arbitrary: S S')
-apply (auto simp: Let_def mono_update mono_aval' le_join_disj split: option.split)
+lemma mono_step': "S \<sqsubseteq> S' \<Longrightarrow> c \<sqsubseteq> c' \<Longrightarrow> step' S c \<sqsubseteq> step' S' c'"
+apply(induction c c' arbitrary: S S' rule: le_acom.induct)
+apply (auto simp: Let_def mono_update mono_aval' mono_post le_join_disj
+ split: option.split)
done
end
--- a/src/HOL/IMP/Abs_Int1.thy Sat Jan 07 12:39:46 2012 +0100
+++ b/src/HOL/IMP/Abs_Int1.thy Sat Jan 07 21:19:53 2012 +0100
@@ -260,18 +260,14 @@
apply(metis mono_aval'' mono_afilter mono_filter_less'[simplified le_prod_def] fst_conv snd_conv)
done
-
-lemma post_le_post: "c \<sqsubseteq> c' \<Longrightarrow> post c \<sqsubseteq> post c'"
-by (induction c c' rule: le_acom.induct) simp_all
-
-lemma mono_step'_aux: "S \<sqsubseteq> S' \<Longrightarrow> c \<sqsubseteq> c' \<Longrightarrow> step' S c \<sqsubseteq> step' S' c'"
+lemma mono_step': "S \<sqsubseteq> S' \<Longrightarrow> c \<sqsubseteq> c' \<Longrightarrow> step' S c \<sqsubseteq> step' S' c'"
apply(induction c c' arbitrary: S S' rule: le_acom.induct)
-apply (auto simp: post_le_post Let_def mono_bfilter mono_update mono_aval' le_join_disj
+apply (auto simp: mono_post mono_bfilter mono_update mono_aval' Let_def le_join_disj
split: option.split)
done
-lemma mono_step': "mono (step' S)"
-by(simp add: mono_def mono_step'_aux[OF le_refl])
+lemma mono_step'2: "mono (step' S)"
+by(simp add: mono_def mono_step'[OF le_refl])
end
--- a/src/HOL/IMP/Abs_Int2.thy Sat Jan 07 12:39:46 2012 +0100
+++ b/src/HOL/IMP/Abs_Int2.thy Sat Jan 07 21:19:53 2012 +0100
@@ -190,7 +190,7 @@
lemma AI_WN_sound: "AI_WN c = Some c' \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c c'"
proof(simp add: CS_def AI_WN_def)
assume 1: "pfp_WN (step' \<top>) c = Some c'"
- from pfp_WN_pfp[OF allI[OF strip_step'] mono_step' 1]
+ from pfp_WN_pfp[OF allI[OF strip_step'] 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')"