# HG changeset patch
# User nipkow
# Date 1358625905 -3600
# Node ID c54ea7f5418f01bd40ea4407446fb9696b9b6df9
# Parent  23bb011a5832fa56f938e3755317de9befcb74c2
simplified proofs

diff -r 23bb011a5832 -r c54ea7f5418f src/HOL/IMP/ACom.thy
--- a/src/HOL/IMP/ACom.thy	Sat Jan 19 17:42:12 2013 +0100
+++ b/src/HOL/IMP/ACom.thy	Sat Jan 19 21:05:05 2013 +0100
@@ -4,9 +4,6 @@
 imports Com
 begin
 
-(* is there a better place? *)
-definition "show_state xs s = [(x,s x). x \<leftarrow> xs]"
-
 subsection "Annotated Commands"
 
 datatype 'a acom =
diff -r 23bb011a5832 -r c54ea7f5418f src/HOL/IMP/Abs_Int0.thy
--- a/src/HOL/IMP/Abs_Int0.thy	Sat Jan 19 17:42:12 2013 +0100
+++ b/src/HOL/IMP/Abs_Int0.thy	Sat Jan 19 21:05:05 2013 +0100
@@ -311,57 +311,33 @@
   "\<lbrakk> s : \<gamma>\<^isub>s S; i : \<gamma> a \<rbrakk> \<Longrightarrow> s(x := i) : \<gamma>\<^isub>s(S(x := a))"
 by(simp add: \<gamma>_fun_def)
 
-lemma step_preserves_le:
-  "\<lbrakk> S \<subseteq> \<gamma>\<^isub>o S'; C \<le> \<gamma>\<^isub>c C' \<rbrakk> \<Longrightarrow> step S C \<le> \<gamma>\<^isub>c (step' S' C')"
-proof(induction C arbitrary: C' S S')
-  case SKIP thus ?case by(auto simp:SKIP_le map_acom_SKIP)
+lemma step_step': "step (\<gamma>\<^isub>o S) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c (step' S C)"
+proof(induction C arbitrary: S)
+  case SKIP thus ?case by auto
 next
   case Assign thus ?case
-    by (fastforce simp: Assign_le  map_acom_Assign intro: aval'_sound in_gamma_update
-      split: option.splits del:subsetD)
+    by (fastforce intro: aval'_sound in_gamma_update split: option.splits)
 next
-  case Seq thus ?case apply (auto simp: Seq_le map_acom_Seq)
-    by (metis le_post post_map_acom)
+  case Seq thus ?case by auto
 next
-  case (If b p1 C1 p2 C2 P)
-  then obtain q1 q2 D1 D2 P' where
-      "C' = IF b THEN {q1} D1 ELSE {q2} D2 {P'}"
-      "p1 \<subseteq> \<gamma>\<^isub>o q1" "p2 \<subseteq> \<gamma>\<^isub>o q2" "P \<subseteq> \<gamma>\<^isub>o P'" "C1 \<le> \<gamma>\<^isub>c D1" "C2 \<le> \<gamma>\<^isub>c D2"
-    by (fastforce simp: If_le map_acom_If)
-  moreover have "post C1 \<subseteq> \<gamma>\<^isub>o(post D1 \<squnion> post D2)"
-    by (metis (no_types) `C1 \<le> \<gamma>\<^isub>c D1` join_ge1 le_post mono_gamma_o order_trans post_map_acom)
-  moreover have "post C2 \<subseteq> \<gamma>\<^isub>o(post D1 \<squnion> post D2)"
-    by (metis (no_types) `C2 \<le> \<gamma>\<^isub>c D2` join_ge2 le_post mono_gamma_o order_trans post_map_acom)
-  ultimately show ?case using `S \<subseteq> \<gamma>\<^isub>o S'` by (simp add: If.IH subset_iff)
+  case If thus ?case by (auto simp: mono_gamma_o)
 next
-  case (While I b p1 C1 P)
-  then obtain D1 I' p1' P' where
-    "C' = {I'} WHILE b DO {p1'} D1 {P'}"
-    "I \<subseteq> \<gamma>\<^isub>o I'" "p1 \<subseteq> \<gamma>\<^isub>o p1'" "P \<subseteq> \<gamma>\<^isub>o P'" "C1 \<le> \<gamma>\<^isub>c D1"
-    by (fastforce simp: map_acom_While While_le)
-  moreover have "S \<union> post C1 \<subseteq> \<gamma>\<^isub>o (S' \<squnion> post D1)"
-    using `S \<subseteq> \<gamma>\<^isub>o S'` le_post[OF `C1 \<le> \<gamma>\<^isub>c D1`, simplified]
-    by (metis (no_types) join_ge1 join_ge2 le_sup_iff mono_gamma_o order_trans)
-  ultimately show ?case by (simp add: While.IH subset_iff)
-
+  case While thus ?case by (auto simp: mono_gamma_o)
 qed
 
 lemma AI_sound: "AI c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C"
 proof(simp add: CS_def AI_def)
   assume 1: "pfp (step' \<top>) (bot c) = Some C"
-  have 2: "step' \<top> C \<sqsubseteq> C" by(rule pfp_pfp[OF 1])
-  have 3: "strip (\<gamma>\<^isub>c (step' \<top> C)) = c"
-    by(simp add: strip_pfp[OF _ 1])
-  have "lfp c (step UNIV) \<le> \<gamma>\<^isub>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)"
-    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])
-    qed
+  have pfp': "step' \<top> C \<sqsubseteq> C" by(rule pfp_pfp[OF 1])
+  have 2: "step (\<gamma>\<^isub>o \<top>) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C"  --"transfer the pfp'"
+  proof(rule order_trans)
+    show "step (\<gamma>\<^isub>o \<top>) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c (step' \<top> C)" by(rule step_step')
+    show "... \<le> \<gamma>\<^isub>c C" by (metis mono_gamma_c[OF pfp'])
   qed
-  with 2 show "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C"
-    by (blast intro: mono_gamma_c order_trans)
+  have 3: "strip (\<gamma>\<^isub>c C) = c" by(simp add: strip_pfp[OF _ 1])
+  have "lfp c (step (\<gamma>\<^isub>o \<top>)) \<le> \<gamma>\<^isub>c C"
+    by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o \<top>)", OF 3 2])
+  thus "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C" by simp
 qed
 
 end
diff -r 23bb011a5832 -r c54ea7f5418f src/HOL/IMP/Abs_Int1.thy
--- a/src/HOL/IMP/Abs_Int1.thy	Sat Jan 19 17:42:12 2013 +0100
+++ b/src/HOL/IMP/Abs_Int1.thy	Sat Jan 19 21:05:05 2013 +0100
@@ -84,44 +84,21 @@
   "\<lbrakk> s : \<gamma>\<^isub>s S; i : \<gamma> a \<rbrakk> \<Longrightarrow> s(x := i) : \<gamma>\<^isub>s(update S x a)"
 by(simp add: \<gamma>_st_def)
 
-theorem step_preserves_le:
-  "\<lbrakk> S \<subseteq> \<gamma>\<^isub>o S'; C \<le> \<gamma>\<^isub>c C';  C' \<in> L X; S' \<in> L X \<rbrakk> \<Longrightarrow> step S C \<le> \<gamma>\<^isub>c (step' S' C')"
-proof(induction C arbitrary: C' S S')
-  case SKIP thus ?case by(auto simp:SKIP_le map_acom_SKIP)
+lemma step_step': "C \<in> L X \<Longrightarrow> S \<in> L X \<Longrightarrow> step (\<gamma>\<^isub>o S) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c (step' S C)"
+proof(induction C arbitrary: S)
+  case SKIP thus ?case by auto
 next
   case Assign thus ?case
-    by(fastforce simp: Assign_le map_acom_Assign L_st_def
-        intro: aval'_sound in_gamma_update split: option.splits)
+    by (fastforce simp: L_st_def intro: aval'_sound in_gamma_update split: option.splits)
 next
-  case Seq thus ?case apply (auto simp: Seq_le map_acom_Seq)
-    by (metis le_post post_map_acom post_in_L)
+  case Seq thus ?case by auto
 next
-  case (If b P1 C1 P2 C2 Q)
-  then obtain P1' P2' C1' C2' Q' where
-      "C' = IF b THEN {P1'} C1' ELSE {P2'} C2' {Q'}"
-      "P1 \<subseteq> \<gamma>\<^isub>o P1'" "P2 \<subseteq> \<gamma>\<^isub>o P2'" "Q \<subseteq> \<gamma>\<^isub>o Q'" "C1 \<le> \<gamma>\<^isub>c C1'" "C2 \<le> \<gamma>\<^isub>c C2'"
-    by (fastforce simp: If_le map_acom_If)
-  moreover from this(1) `C' \<in> L X`
-  have L: "C1' \<in> L X" "C2' \<in> L X" "P1' \<in> L X" "P2' \<in> L X" by simp_all
-  moreover have "post C1 \<subseteq> \<gamma>\<^isub>o(post C1' \<squnion> post C2')"
-    by (metis (no_types) `C1 \<le> \<gamma>\<^isub>c C1'` join_ge1 le_post mono_gamma_o order_trans post_map_acom L post_in_L)
-  moreover have "post C2 \<subseteq> \<gamma>\<^isub>o(post C1' \<squnion> post C2')"
-    by (metis (no_types) `C2 \<le> \<gamma>\<^isub>c C2'` join_ge2 le_post mono_gamma_o order_trans post_map_acom L post_in_L)
-  ultimately show ?case using `S \<subseteq> \<gamma>\<^isub>o S'` `S' \<in> L X`
-    by (simp add: If.IH subset_iff)
+  case (If b p1 C1 p2 C2 P)
+  hence "post C1 \<sqsubseteq> post C1 \<squnion> post C2 \<and> post C2 \<sqsubseteq> post C1 \<squnion> post C2"
+    by(simp, metis post_in_L join_ge1 join_ge2)
+  thus ?case using If by (auto simp: mono_gamma_o)
 next
-  case (While I b P1 C1 Q)
-  then obtain C1' I' P1' Q' where
-    "C' = {I'} WHILE b DO {P1'} C1' {Q'}"
-    "I \<subseteq> \<gamma>\<^isub>o I'" "P1 \<subseteq> \<gamma>\<^isub>o P1'" "C1 \<le> \<gamma>\<^isub>c C1'" "Q \<subseteq> \<gamma>\<^isub>o Q'" 
-    by (fastforce simp: map_acom_While While_le)
-  moreover from this(1) `C' \<in> L X`
-  have L: "C1' \<in> L X" "I' \<in> L X" "P1' \<in> L X" by simp_all
-  moreover note compat = `S' \<in> L X` post_in_L[OF L(1)]
-  moreover have "S \<union> post C1 \<subseteq> \<gamma>\<^isub>o (S' \<squnion> post C1')"
-    using `S \<subseteq> \<gamma>\<^isub>o S'` le_post[OF `C1 \<le> \<gamma>\<^isub>c C1'`, simplified]
-    by (metis (no_types) join_ge1[OF compat] join_ge2[OF compat] le_sup_iff mono_gamma_o order_trans)
-  ultimately show ?case by (simp add: While.IH subset_iff)
+  case While thus ?case by (auto simp: mono_gamma_o)
 qed
 
 lemma step'_in_L[simp]:
@@ -131,25 +108,24 @@
     by(auto simp: L_st_def update_def split: option.splits)
 qed auto
 
-theorem AI_sound: "AI c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C"
+lemma AI_sound: "AI c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C"
 proof(simp add: CS_def AI_def)
   assume 1: "pfp (step' (top c)) (bot c) = Some C"
   have "C \<in> L(vars c)"
     by(rule pfp_inv[where P = "%C. C \<in> L(vars c)", OF 1 _ bot_in_L])
       (erule step'_in_L[OF _ top_in_L])
-  have 2: "step' (top c) C \<sqsubseteq> C" by(rule pfp_pfp[OF 1])
-  have 3: "strip (\<gamma>\<^isub>c (step' (top c) C)) = c"
-    by(simp add: strip_pfp[OF _ 1])
-  have "lfp c (step UNIV) \<le> \<gamma>\<^isub>c (step' (top c) C)"
-  proof(rule lfp_lowerbound[simplified,OF 3])
-    show "step UNIV (\<gamma>\<^isub>c (step' (top c) C)) \<le> \<gamma>\<^isub>c (step' (top c) C)"
-    proof(rule step_preserves_le[OF _ _ `C \<in> L(vars c)` top_in_L])
-      show "UNIV \<subseteq> \<gamma>\<^isub>o (top c)" by simp
-      show "\<gamma>\<^isub>c (step' (top c) C) \<le> \<gamma>\<^isub>c C" by(rule mono_gamma_c[OF 2])
-    qed
+  have pfp': "step' (top c) C \<sqsubseteq> C" by(rule pfp_pfp[OF 1])
+  have 2: "step (\<gamma>\<^isub>o(top c)) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C"
+  proof(rule order_trans)
+    show "step (\<gamma>\<^isub>o (top c)) (\<gamma>\<^isub>c C) \<le>  \<gamma>\<^isub>c (step' (top c) C)"
+      by(rule step_step'[OF `C \<in> L(vars c)` top_in_L])
+    show "\<gamma>\<^isub>c (step' (top c) C) \<le> \<gamma>\<^isub>c C"
+      by(rule mono_gamma_c[OF pfp'])
   qed
-  from this 2 show "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C"
-    by (blast intro: mono_gamma_c order_trans)
+  have 3: "strip (\<gamma>\<^isub>c C) = c" by(simp add: strip_pfp[OF _ 1])
+  have "lfp c (step (\<gamma>\<^isub>o(top c))) \<le> \<gamma>\<^isub>c C"
+    by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o(top c))", OF 3 2])
+  thus "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C" by simp
 qed
 
 end
diff -r 23bb011a5832 -r c54ea7f5418f src/HOL/IMP/Abs_Int2.thy
--- a/src/HOL/IMP/Abs_Int2.thy	Sat Jan 19 17:42:12 2013 +0100
+++ b/src/HOL/IMP/Abs_Int2.thy	Sat Jan 19 21:05:05 2013 +0100
@@ -179,75 +179,52 @@
   "\<lbrakk> s : \<gamma>\<^isub>s S; i : \<gamma> a \<rbrakk> \<Longrightarrow> s(x := i) : \<gamma>\<^isub>s(update S x a)"
 by(simp add: \<gamma>_st_def)
 
-theorem step_preserves_le:
-  "\<lbrakk> S \<subseteq> \<gamma>\<^isub>o S'; C \<le> \<gamma>\<^isub>c C'; C' \<in> L X; S' \<in> L X \<rbrakk> \<Longrightarrow> step S C \<le> \<gamma>\<^isub>c (step' S' C')"
-proof(induction C arbitrary: C' S S')
-  case SKIP thus ?case by(auto simp:SKIP_le map_acom_SKIP)
+lemma step_step': "C \<in> L X \<Longrightarrow> S \<in> L X \<Longrightarrow> step (\<gamma>\<^isub>o S) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c (step' S C)"
+proof(induction C arbitrary: S)
+  case SKIP thus ?case by auto
 next
   case Assign thus ?case
-    by (fastforce simp: Assign_le map_acom_Assign L_option_def L_st_def
-        intro: aval'_sound in_gamma_update  split: option.splits del:subsetD)
+    by (fastforce simp: L_st_def intro: aval'_sound in_gamma_update split: option.splits)
 next
-  case Seq thus ?case apply (auto simp: Seq_le map_acom_Seq)
-    by (metis le_post post_map_acom post_in_L)
+  case Seq thus ?case by auto
 next
-  case (If b P1 C1 P2 C2 Q)
-  then obtain P1' C1' P2' C2' Q' where
-      "C' = IF b THEN {P1'} C1' ELSE {P2'} C2' {Q'}"
-      "P1 \<subseteq> \<gamma>\<^isub>o P1'" "P2 \<subseteq> \<gamma>\<^isub>o P2'"  "C1 \<le> \<gamma>\<^isub>c C1'" "C2 \<le> \<gamma>\<^isub>c C2'" "Q \<subseteq> \<gamma>\<^isub>o Q'" 
-    by (fastforce simp: If_le map_acom_If)
-  moreover from this(1) `C' \<in> L X`
-  have L: "C1' \<in> L X" "C2' \<in> L X" "P1' \<in> L X" "P2' \<in> L X" and "vars b \<subseteq> X"
-    by simp_all
-  moreover have "post C1 \<subseteq> \<gamma>\<^isub>o(post C1' \<squnion> post C2')"
-    by (metis (no_types) `C1 \<le> \<gamma>\<^isub>c C1'` join_ge1 le_post mono_gamma_o order_trans post_map_acom post_in_L L)
-  moreover have "post C2 \<subseteq> \<gamma>\<^isub>o(post C1' \<squnion> post C2')"
-    by (metis (no_types) `C2 \<le> \<gamma>\<^isub>c C2'` join_ge2 le_post mono_gamma_o order_trans post_map_acom post_in_L L)
-  moreover note vars = `S' \<in> L X` `vars b \<subseteq> X`
-  ultimately show ?case using `S \<subseteq> \<gamma>\<^isub>o S'`
-    by (simp add: If.IH subset_iff bfilter_sound[OF vars] bfilter_in_L[OF vars])
+  case (If b _ C1 _ C2)
+  hence 0: "post C1 \<sqsubseteq> post C1 \<squnion> post C2 \<and> post C2 \<sqsubseteq> post C1 \<squnion> post C2"
+    by(simp, metis post_in_L join_ge1 join_ge2)
+  have "vars b \<subseteq> X" using If.prems by simp
+  note vars = `S \<in> L X` `vars b \<subseteq> X`
+  show ?case using If 0
+    by (auto simp: mono_gamma_o bfilter_sound[OF vars] bfilter_in_L[OF vars])
 next
-  case (While I b P C1 Q)
-  then obtain C1' I' P' Q' where
-    "C' = {I'} WHILE b DO {P'} C1' {Q'}"
-    "I \<subseteq> \<gamma>\<^isub>o I'" "P \<subseteq> \<gamma>\<^isub>o P'" "Q \<subseteq> \<gamma>\<^isub>o Q'" "C1 \<le> \<gamma>\<^isub>c C1'"
-    by (fastforce simp: map_acom_While While_le)
-  moreover from this(1) `C' \<in> L X`
-  have L: "C1' \<in> L X" "I' \<in> L X" "P' \<in> L X" and "vars b \<subseteq> X" by simp_all
-  moreover note compat = `S' \<in> L X` post_in_L[OF L(1)]
-  moreover note vars = `I' \<in> L X` `vars b \<subseteq> X`
-  moreover have "S \<union> post C1 \<subseteq> \<gamma>\<^isub>o (S' \<squnion> post C1')"
-    using `S \<subseteq> \<gamma>\<^isub>o S'` le_post[OF `C1 \<le> \<gamma>\<^isub>c C1'`, simplified]
-    by (metis (no_types) join_ge1[OF compat] join_ge2[OF compat] le_sup_iff mono_gamma_o order_trans)
-  ultimately show ?case
-    by (simp add: While.IH subset_iff bfilter_sound[OF vars] bfilter_in_L[OF vars])
+  case (While I b)
+  hence vars: "I \<in> L X" "vars b \<subseteq> X" by simp_all
+  thus ?case using While
+    by (auto simp: mono_gamma_o bfilter_sound[OF vars] bfilter_in_L[OF vars])
 qed
 
-lemma step'_in_L[simp]:
-  "\<lbrakk> C \<in> L X; S \<in> L X \<rbrakk> \<Longrightarrow> step' S C \<in> L X"
+lemma step'_in_L[simp]: "\<lbrakk> C \<in> L X; S \<in> L X \<rbrakk> \<Longrightarrow> step' S C \<in> L X"
 proof(induction C arbitrary: S)
   case Assign thus ?case by(simp add: L_option_def L_st_def update_def split: option.splits)
 qed (auto simp add: bfilter_in_L)
 
-theorem AI_sound: "AI c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C"
+lemma AI_sound: "AI c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C"
 proof(simp add: CS_def AI_def)
   assume 1: "pfp (step' (top c)) (bot c) = Some C"
   have "C \<in> L(vars c)"
     by(rule pfp_inv[where P = "%C. C \<in> L(vars c)", OF 1 _ bot_in_L])
       (erule step'_in_L[OF _ top_in_L])
-  have 2: "step' (top c) C \<sqsubseteq> C" by(rule pfp_pfp[OF 1])
-  have 3: "strip (\<gamma>\<^isub>c (step' (top c) C)) = c"
-    by(simp add: strip_pfp[OF _ 1])
-  have "lfp c (step UNIV) \<le> \<gamma>\<^isub>c (step' (top c) C)"
-  proof(rule lfp_lowerbound[simplified,OF 3])
-    show "step UNIV (\<gamma>\<^isub>c (step' (top c) C)) \<le> \<gamma>\<^isub>c (step' (top c) C)"
-    proof(rule step_preserves_le[OF _ _ `C \<in> L(vars c)` top_in_L])
-      show "UNIV \<subseteq> \<gamma>\<^isub>o (top c)" by simp
-      show "\<gamma>\<^isub>c (step' (top c) C) \<le> \<gamma>\<^isub>c C" by(rule mono_gamma_c[OF 2])
-    qed
+  have pfp': "step' (top c) C \<sqsubseteq> C" by(rule pfp_pfp[OF 1])
+  have 2: "step (\<gamma>\<^isub>o(top c)) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C"
+  proof(rule order_trans)
+    show "step (\<gamma>\<^isub>o (top c)) (\<gamma>\<^isub>c C) \<le>  \<gamma>\<^isub>c (step' (top c) C)"
+      by(rule step_step'[OF `C \<in> L(vars c)` top_in_L])
+    show "\<gamma>\<^isub>c (step' (top c) C) \<le> \<gamma>\<^isub>c C"
+      by(rule mono_gamma_c[OF pfp'])
   qed
-  from this 2 show "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C"
-    by (blast intro: mono_gamma_c order_trans)
+  have 3: "strip (\<gamma>\<^isub>c C) = c" by(simp add: strip_pfp[OF _ 1])
+  have "lfp c (step (\<gamma>\<^isub>o(top c))) \<le> \<gamma>\<^isub>c C"
+    by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o(top c))", OF 3 2])
+  thus "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C" by simp
 qed
 
 end
diff -r 23bb011a5832 -r c54ea7f5418f src/HOL/IMP/Abs_Int3.thy
--- a/src/HOL/IMP/Abs_Int3.thy	Sat Jan 19 17:42:12 2013 +0100
+++ b/src/HOL/IMP/Abs_Int3.thy	Sat Jan 19 21:05:05 2013 +0100
@@ -366,18 +366,17 @@
   have 2: "(strip C = c & C \<in> L(vars c)) \<and> step' \<top>\<^bsub>c\<^esub> C \<sqsubseteq> C"
     by(rule pfp_wn_pfp[where x="bot c"])
       (simp_all add: 1 mono_step'_top widen_c_in_L narrow_c_in_L)
-  have 3: "strip (\<gamma>\<^isub>c (step' \<top>\<^bsub>c\<^esub> C)) = c" by(simp add: strip_pfp_wn[OF _ 1])
-  have "lfp c (step UNIV) \<le> \<gamma>\<^isub>c (step' \<top>\<^bsub>c\<^esub> C)"
-  proof(rule lfp_lowerbound[simplified,OF 3])
-    show "step UNIV (\<gamma>\<^isub>c (step' \<top>\<^bsub>c\<^esub> C)) \<le> \<gamma>\<^isub>c (step' \<top>\<^bsub>c\<^esub> C)"
-    proof(rule step_preserves_le[OF _ _ _ top_in_L])
-      show "UNIV \<subseteq> \<gamma>\<^isub>o \<top>\<^bsub>c\<^esub>" by simp
-      show "\<gamma>\<^isub>c (step' \<top>\<^bsub>c\<^esub> C) \<le> \<gamma>\<^isub>c C" by(rule mono_gamma_c[OF conjunct2[OF 2]])
-      show "C \<in> L(vars c)" using 2 by blast
-    qed
+  have pfp: "step (\<gamma>\<^isub>o(top c)) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C"
+  proof(rule order_trans)
+    show "step (\<gamma>\<^isub>o (top c)) (\<gamma>\<^isub>c C) \<le>  \<gamma>\<^isub>c (step' (top c) C)"
+      by(rule step_step'[OF conjunct2[OF conjunct1[OF 2]] top_in_L])
+    show "... \<le> \<gamma>\<^isub>c C"
+      by(rule mono_gamma_c[OF conjunct2[OF 2]])
   qed
-  from this 2 show "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C"
-    by (blast intro: mono_gamma_c order_trans)
+  have 3: "strip (\<gamma>\<^isub>c C) = c" by(simp add: strip_pfp_wn[OF _ 1])
+  have "lfp c (step (\<gamma>\<^isub>o (top c))) \<le> \<gamma>\<^isub>c C"
+    by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o(top c))", OF 3 pfp])
+  thus "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C" by simp
 qed
 
 end
diff -r 23bb011a5832 -r c54ea7f5418f src/HOL/IMP/Abs_Int_ITP/ACom_ITP.thy
--- a/src/HOL/IMP/Abs_Int_ITP/ACom_ITP.thy	Sat Jan 19 17:42:12 2013 +0100
+++ b/src/HOL/IMP/Abs_Int_ITP/ACom_ITP.thy	Sat Jan 19 21:05:05 2013 +0100
@@ -4,9 +4,6 @@
 imports "../Com"
 begin
 
-(* is there a better place? *)
-definition "show_state xs s = [(x,s x). x \<leftarrow> xs]"
-
 subsection "Annotated Commands"
 
 datatype 'a acom =
diff -r 23bb011a5832 -r c54ea7f5418f src/HOL/IMP/Collecting_Examples.thy
--- a/src/HOL/IMP/Collecting_Examples.thy	Sat Jan 19 17:42:12 2013 +0100
+++ b/src/HOL/IMP/Collecting_Examples.thy	Sat Jan 19 21:05:05 2013 +0100
@@ -12,7 +12,7 @@
                 DO ''x'' ::= Plus (V ''x'') (N 2)"
 definition C0 :: "state set acom" where "C0 = anno {} c"
 
-definition "show_acom xs = map_acom (\<lambda>S. show_state xs ` S)"
+definition "show_acom xs = map_acom (\<lambda>S. (\<lambda>s. [(x,s x). x \<leftarrow> xs]) ` S)"
 
 text{* Collecting semantics: *}
 
diff -r 23bb011a5832 -r c54ea7f5418f src/HOL/IMP/Hoare_Examples.thy
--- a/src/HOL/IMP/Hoare_Examples.thy	Sat Jan 19 17:42:12 2013 +0100
+++ b/src/HOL/IMP/Hoare_Examples.thy	Sat Jan 19 21:05:05 2013 +0100
@@ -5,7 +5,7 @@
 subsection{* Example: Sums *}
 
 text{* Summing up the first @{text n} natural numbers. The sum is accumulated
-in variable @{text 0}, the loop counter is variable @{text 1}. *}
+in variable @{text x}, the loop counter is variable @{text y}. *}
 
 abbreviation "w n ==
   WHILE Less (V ''y'') (N n)