# HG changeset patch
# User nipkow
# Date 1325967593 -3600
# Node ID 7e4a18db738492d082313e41a9cb45e6142aa74e
# Parent  793cecd4ffc0628db0fa5da04004f25513bb0728
tuned

diff -r 793cecd4ffc0 -r 7e4a18db7384 src/HOL/IMP/Abs_Int0.thy
--- 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
diff -r 793cecd4ffc0 -r 7e4a18db7384 src/HOL/IMP/Abs_Int0_fun.thy
--- 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
diff -r 793cecd4ffc0 -r 7e4a18db7384 src/HOL/IMP/Abs_Int1.thy
--- 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
 
diff -r 793cecd4ffc0 -r 7e4a18db7384 src/HOL/IMP/Abs_Int2.thy
--- 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')"