# 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 \ a' \ S \ S' \ update S x a \ update S' x a'" by(auto simp add: le_st_def lookup_def update_def) -lemma step'_mono: "S \ S' \ step' S c \ 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 \ S' \ c \ c' \ step' S c \ 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 \ c' \ post c \ post c'" +by(induction c c' rule: le_acom.induct) (auto) + locale Abs_Int_Fun_mono = Abs_Int_Fun + assumes mono_plus': "a1 \ b1 \ a2 \ b2 \ plus' a1 a2 \ plus' b1 b2" begin @@ -382,9 +385,10 @@ lemma mono_update: "a \ a' \ S \ S' \ S(x := a) \ S'(x := a')" by(simp add: le_fun_def) -lemma step'_mono: "S \ S' \ step' S c \ 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 \ S' \ c \ c' \ step' S c \ 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 \ c' \ post c \ post c'" -by (induction c c' rule: le_acom.induct) simp_all - -lemma mono_step'_aux: "S \ S' \ c \ c' \ step' S c \ step' S' c'" +lemma mono_step': "S \ S' \ c \ c' \ step' S c \ 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' \ CS c \ \\<^isub>c c'" proof(simp add: CS_def AI_WN_def) assume 1: "pfp_WN (step' \) 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' \ c' \ c'" . have 3: "strip (\\<^isub>c (step' \ c')) = c" by(simp add: strip_pfp_WN[OF _ 1]) have "lfp (step UNIV) c \ \\<^isub>c (step' \ c')"