simplified proofs
authornipkow
Sat Jan 19 21:05:05 2013 +0100 (2013-01-19)
changeset 50986c54ea7f5418f
parent 50985 23bb011a5832
child 50987 616789281413
simplified proofs
src/HOL/IMP/ACom.thy
src/HOL/IMP/Abs_Int0.thy
src/HOL/IMP/Abs_Int1.thy
src/HOL/IMP/Abs_Int2.thy
src/HOL/IMP/Abs_Int3.thy
src/HOL/IMP/Abs_Int_ITP/ACom_ITP.thy
src/HOL/IMP/Collecting_Examples.thy
src/HOL/IMP/Hoare_Examples.thy
     1.1 --- a/src/HOL/IMP/ACom.thy	Sat Jan 19 17:42:12 2013 +0100
     1.2 +++ b/src/HOL/IMP/ACom.thy	Sat Jan 19 21:05:05 2013 +0100
     1.3 @@ -4,9 +4,6 @@
     1.4  imports Com
     1.5  begin
     1.6  
     1.7 -(* is there a better place? *)
     1.8 -definition "show_state xs s = [(x,s x). x \<leftarrow> xs]"
     1.9 -
    1.10  subsection "Annotated Commands"
    1.11  
    1.12  datatype 'a acom =
     2.1 --- a/src/HOL/IMP/Abs_Int0.thy	Sat Jan 19 17:42:12 2013 +0100
     2.2 +++ b/src/HOL/IMP/Abs_Int0.thy	Sat Jan 19 21:05:05 2013 +0100
     2.3 @@ -311,57 +311,33 @@
     2.4    "\<lbrakk> s : \<gamma>\<^isub>s S; i : \<gamma> a \<rbrakk> \<Longrightarrow> s(x := i) : \<gamma>\<^isub>s(S(x := a))"
     2.5  by(simp add: \<gamma>_fun_def)
     2.6  
     2.7 -lemma step_preserves_le:
     2.8 -  "\<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')"
     2.9 -proof(induction C arbitrary: C' S S')
    2.10 -  case SKIP thus ?case by(auto simp:SKIP_le map_acom_SKIP)
    2.11 +lemma step_step': "step (\<gamma>\<^isub>o S) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c (step' S C)"
    2.12 +proof(induction C arbitrary: S)
    2.13 +  case SKIP thus ?case by auto
    2.14  next
    2.15    case Assign thus ?case
    2.16 -    by (fastforce simp: Assign_le  map_acom_Assign intro: aval'_sound in_gamma_update
    2.17 -      split: option.splits del:subsetD)
    2.18 +    by (fastforce intro: aval'_sound in_gamma_update split: option.splits)
    2.19  next
    2.20 -  case Seq thus ?case apply (auto simp: Seq_le map_acom_Seq)
    2.21 -    by (metis le_post post_map_acom)
    2.22 +  case Seq thus ?case by auto
    2.23  next
    2.24 -  case (If b p1 C1 p2 C2 P)
    2.25 -  then obtain q1 q2 D1 D2 P' where
    2.26 -      "C' = IF b THEN {q1} D1 ELSE {q2} D2 {P'}"
    2.27 -      "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"
    2.28 -    by (fastforce simp: If_le map_acom_If)
    2.29 -  moreover have "post C1 \<subseteq> \<gamma>\<^isub>o(post D1 \<squnion> post D2)"
    2.30 -    by (metis (no_types) `C1 \<le> \<gamma>\<^isub>c D1` join_ge1 le_post mono_gamma_o order_trans post_map_acom)
    2.31 -  moreover have "post C2 \<subseteq> \<gamma>\<^isub>o(post D1 \<squnion> post D2)"
    2.32 -    by (metis (no_types) `C2 \<le> \<gamma>\<^isub>c D2` join_ge2 le_post mono_gamma_o order_trans post_map_acom)
    2.33 -  ultimately show ?case using `S \<subseteq> \<gamma>\<^isub>o S'` by (simp add: If.IH subset_iff)
    2.34 +  case If thus ?case by (auto simp: mono_gamma_o)
    2.35  next
    2.36 -  case (While I b p1 C1 P)
    2.37 -  then obtain D1 I' p1' P' where
    2.38 -    "C' = {I'} WHILE b DO {p1'} D1 {P'}"
    2.39 -    "I \<subseteq> \<gamma>\<^isub>o I'" "p1 \<subseteq> \<gamma>\<^isub>o p1'" "P \<subseteq> \<gamma>\<^isub>o P'" "C1 \<le> \<gamma>\<^isub>c D1"
    2.40 -    by (fastforce simp: map_acom_While While_le)
    2.41 -  moreover have "S \<union> post C1 \<subseteq> \<gamma>\<^isub>o (S' \<squnion> post D1)"
    2.42 -    using `S \<subseteq> \<gamma>\<^isub>o S'` le_post[OF `C1 \<le> \<gamma>\<^isub>c D1`, simplified]
    2.43 -    by (metis (no_types) join_ge1 join_ge2 le_sup_iff mono_gamma_o order_trans)
    2.44 -  ultimately show ?case by (simp add: While.IH subset_iff)
    2.45 -
    2.46 +  case While thus ?case by (auto simp: mono_gamma_o)
    2.47  qed
    2.48  
    2.49  lemma AI_sound: "AI c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C"
    2.50  proof(simp add: CS_def AI_def)
    2.51    assume 1: "pfp (step' \<top>) (bot c) = Some C"
    2.52 -  have 2: "step' \<top> C \<sqsubseteq> C" by(rule pfp_pfp[OF 1])
    2.53 -  have 3: "strip (\<gamma>\<^isub>c (step' \<top> C)) = c"
    2.54 -    by(simp add: strip_pfp[OF _ 1])
    2.55 -  have "lfp c (step UNIV) \<le> \<gamma>\<^isub>c (step' \<top> C)"
    2.56 -  proof(rule lfp_lowerbound[simplified,OF 3])
    2.57 -    show "step UNIV (\<gamma>\<^isub>c (step' \<top> C)) \<le> \<gamma>\<^isub>c (step' \<top> C)"
    2.58 -    proof(rule step_preserves_le[OF _ _])
    2.59 -      show "UNIV \<subseteq> \<gamma>\<^isub>o \<top>" by simp
    2.60 -      show "\<gamma>\<^isub>c (step' \<top> C) \<le> \<gamma>\<^isub>c C" by(rule mono_gamma_c[OF 2])
    2.61 -    qed
    2.62 +  have pfp': "step' \<top> C \<sqsubseteq> C" by(rule pfp_pfp[OF 1])
    2.63 +  have 2: "step (\<gamma>\<^isub>o \<top>) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C"  --"transfer the pfp'"
    2.64 +  proof(rule order_trans)
    2.65 +    show "step (\<gamma>\<^isub>o \<top>) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c (step' \<top> C)" by(rule step_step')
    2.66 +    show "... \<le> \<gamma>\<^isub>c C" by (metis mono_gamma_c[OF pfp'])
    2.67    qed
    2.68 -  with 2 show "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C"
    2.69 -    by (blast intro: mono_gamma_c order_trans)
    2.70 +  have 3: "strip (\<gamma>\<^isub>c C) = c" by(simp add: strip_pfp[OF _ 1])
    2.71 +  have "lfp c (step (\<gamma>\<^isub>o \<top>)) \<le> \<gamma>\<^isub>c C"
    2.72 +    by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o \<top>)", OF 3 2])
    2.73 +  thus "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C" by simp
    2.74  qed
    2.75  
    2.76  end
     3.1 --- a/src/HOL/IMP/Abs_Int1.thy	Sat Jan 19 17:42:12 2013 +0100
     3.2 +++ b/src/HOL/IMP/Abs_Int1.thy	Sat Jan 19 21:05:05 2013 +0100
     3.3 @@ -84,44 +84,21 @@
     3.4    "\<lbrakk> s : \<gamma>\<^isub>s S; i : \<gamma> a \<rbrakk> \<Longrightarrow> s(x := i) : \<gamma>\<^isub>s(update S x a)"
     3.5  by(simp add: \<gamma>_st_def)
     3.6  
     3.7 -theorem step_preserves_le:
     3.8 -  "\<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')"
     3.9 -proof(induction C arbitrary: C' S S')
    3.10 -  case SKIP thus ?case by(auto simp:SKIP_le map_acom_SKIP)
    3.11 +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)"
    3.12 +proof(induction C arbitrary: S)
    3.13 +  case SKIP thus ?case by auto
    3.14  next
    3.15    case Assign thus ?case
    3.16 -    by(fastforce simp: Assign_le map_acom_Assign L_st_def
    3.17 -        intro: aval'_sound in_gamma_update split: option.splits)
    3.18 +    by (fastforce simp: L_st_def intro: aval'_sound in_gamma_update split: option.splits)
    3.19  next
    3.20 -  case Seq thus ?case apply (auto simp: Seq_le map_acom_Seq)
    3.21 -    by (metis le_post post_map_acom post_in_L)
    3.22 +  case Seq thus ?case by auto
    3.23  next
    3.24 -  case (If b P1 C1 P2 C2 Q)
    3.25 -  then obtain P1' P2' C1' C2' Q' where
    3.26 -      "C' = IF b THEN {P1'} C1' ELSE {P2'} C2' {Q'}"
    3.27 -      "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'"
    3.28 -    by (fastforce simp: If_le map_acom_If)
    3.29 -  moreover from this(1) `C' \<in> L X`
    3.30 -  have L: "C1' \<in> L X" "C2' \<in> L X" "P1' \<in> L X" "P2' \<in> L X" by simp_all
    3.31 -  moreover have "post C1 \<subseteq> \<gamma>\<^isub>o(post C1' \<squnion> post C2')"
    3.32 -    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)
    3.33 -  moreover have "post C2 \<subseteq> \<gamma>\<^isub>o(post C1' \<squnion> post C2')"
    3.34 -    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)
    3.35 -  ultimately show ?case using `S \<subseteq> \<gamma>\<^isub>o S'` `S' \<in> L X`
    3.36 -    by (simp add: If.IH subset_iff)
    3.37 +  case (If b p1 C1 p2 C2 P)
    3.38 +  hence "post C1 \<sqsubseteq> post C1 \<squnion> post C2 \<and> post C2 \<sqsubseteq> post C1 \<squnion> post C2"
    3.39 +    by(simp, metis post_in_L join_ge1 join_ge2)
    3.40 +  thus ?case using If by (auto simp: mono_gamma_o)
    3.41  next
    3.42 -  case (While I b P1 C1 Q)
    3.43 -  then obtain C1' I' P1' Q' where
    3.44 -    "C' = {I'} WHILE b DO {P1'} C1' {Q'}"
    3.45 -    "I \<subseteq> \<gamma>\<^isub>o I'" "P1 \<subseteq> \<gamma>\<^isub>o P1'" "C1 \<le> \<gamma>\<^isub>c C1'" "Q \<subseteq> \<gamma>\<^isub>o Q'" 
    3.46 -    by (fastforce simp: map_acom_While While_le)
    3.47 -  moreover from this(1) `C' \<in> L X`
    3.48 -  have L: "C1' \<in> L X" "I' \<in> L X" "P1' \<in> L X" by simp_all
    3.49 -  moreover note compat = `S' \<in> L X` post_in_L[OF L(1)]
    3.50 -  moreover have "S \<union> post C1 \<subseteq> \<gamma>\<^isub>o (S' \<squnion> post C1')"
    3.51 -    using `S \<subseteq> \<gamma>\<^isub>o S'` le_post[OF `C1 \<le> \<gamma>\<^isub>c C1'`, simplified]
    3.52 -    by (metis (no_types) join_ge1[OF compat] join_ge2[OF compat] le_sup_iff mono_gamma_o order_trans)
    3.53 -  ultimately show ?case by (simp add: While.IH subset_iff)
    3.54 +  case While thus ?case by (auto simp: mono_gamma_o)
    3.55  qed
    3.56  
    3.57  lemma step'_in_L[simp]:
    3.58 @@ -131,25 +108,24 @@
    3.59      by(auto simp: L_st_def update_def split: option.splits)
    3.60  qed auto
    3.61  
    3.62 -theorem AI_sound: "AI c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C"
    3.63 +lemma AI_sound: "AI c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C"
    3.64  proof(simp add: CS_def AI_def)
    3.65    assume 1: "pfp (step' (top c)) (bot c) = Some C"
    3.66    have "C \<in> L(vars c)"
    3.67      by(rule pfp_inv[where P = "%C. C \<in> L(vars c)", OF 1 _ bot_in_L])
    3.68        (erule step'_in_L[OF _ top_in_L])
    3.69 -  have 2: "step' (top c) C \<sqsubseteq> C" by(rule pfp_pfp[OF 1])
    3.70 -  have 3: "strip (\<gamma>\<^isub>c (step' (top c) C)) = c"
    3.71 -    by(simp add: strip_pfp[OF _ 1])
    3.72 -  have "lfp c (step UNIV) \<le> \<gamma>\<^isub>c (step' (top c) C)"
    3.73 -  proof(rule lfp_lowerbound[simplified,OF 3])
    3.74 -    show "step UNIV (\<gamma>\<^isub>c (step' (top c) C)) \<le> \<gamma>\<^isub>c (step' (top c) C)"
    3.75 -    proof(rule step_preserves_le[OF _ _ `C \<in> L(vars c)` top_in_L])
    3.76 -      show "UNIV \<subseteq> \<gamma>\<^isub>o (top c)" by simp
    3.77 -      show "\<gamma>\<^isub>c (step' (top c) C) \<le> \<gamma>\<^isub>c C" by(rule mono_gamma_c[OF 2])
    3.78 -    qed
    3.79 +  have pfp': "step' (top c) C \<sqsubseteq> C" by(rule pfp_pfp[OF 1])
    3.80 +  have 2: "step (\<gamma>\<^isub>o(top c)) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C"
    3.81 +  proof(rule order_trans)
    3.82 +    show "step (\<gamma>\<^isub>o (top c)) (\<gamma>\<^isub>c C) \<le>  \<gamma>\<^isub>c (step' (top c) C)"
    3.83 +      by(rule step_step'[OF `C \<in> L(vars c)` top_in_L])
    3.84 +    show "\<gamma>\<^isub>c (step' (top c) C) \<le> \<gamma>\<^isub>c C"
    3.85 +      by(rule mono_gamma_c[OF pfp'])
    3.86    qed
    3.87 -  from this 2 show "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C"
    3.88 -    by (blast intro: mono_gamma_c order_trans)
    3.89 +  have 3: "strip (\<gamma>\<^isub>c C) = c" by(simp add: strip_pfp[OF _ 1])
    3.90 +  have "lfp c (step (\<gamma>\<^isub>o(top c))) \<le> \<gamma>\<^isub>c C"
    3.91 +    by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o(top c))", OF 3 2])
    3.92 +  thus "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C" by simp
    3.93  qed
    3.94  
    3.95  end
     4.1 --- a/src/HOL/IMP/Abs_Int2.thy	Sat Jan 19 17:42:12 2013 +0100
     4.2 +++ b/src/HOL/IMP/Abs_Int2.thy	Sat Jan 19 21:05:05 2013 +0100
     4.3 @@ -179,75 +179,52 @@
     4.4    "\<lbrakk> s : \<gamma>\<^isub>s S; i : \<gamma> a \<rbrakk> \<Longrightarrow> s(x := i) : \<gamma>\<^isub>s(update S x a)"
     4.5  by(simp add: \<gamma>_st_def)
     4.6  
     4.7 -theorem step_preserves_le:
     4.8 -  "\<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')"
     4.9 -proof(induction C arbitrary: C' S S')
    4.10 -  case SKIP thus ?case by(auto simp:SKIP_le map_acom_SKIP)
    4.11 +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)"
    4.12 +proof(induction C arbitrary: S)
    4.13 +  case SKIP thus ?case by auto
    4.14  next
    4.15    case Assign thus ?case
    4.16 -    by (fastforce simp: Assign_le map_acom_Assign L_option_def L_st_def
    4.17 -        intro: aval'_sound in_gamma_update  split: option.splits del:subsetD)
    4.18 +    by (fastforce simp: L_st_def intro: aval'_sound in_gamma_update split: option.splits)
    4.19  next
    4.20 -  case Seq thus ?case apply (auto simp: Seq_le map_acom_Seq)
    4.21 -    by (metis le_post post_map_acom post_in_L)
    4.22 +  case Seq thus ?case by auto
    4.23  next
    4.24 -  case (If b P1 C1 P2 C2 Q)
    4.25 -  then obtain P1' C1' P2' C2' Q' where
    4.26 -      "C' = IF b THEN {P1'} C1' ELSE {P2'} C2' {Q'}"
    4.27 -      "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'" 
    4.28 -    by (fastforce simp: If_le map_acom_If)
    4.29 -  moreover from this(1) `C' \<in> L X`
    4.30 -  have L: "C1' \<in> L X" "C2' \<in> L X" "P1' \<in> L X" "P2' \<in> L X" and "vars b \<subseteq> X"
    4.31 -    by simp_all
    4.32 -  moreover have "post C1 \<subseteq> \<gamma>\<^isub>o(post C1' \<squnion> post C2')"
    4.33 -    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)
    4.34 -  moreover have "post C2 \<subseteq> \<gamma>\<^isub>o(post C1' \<squnion> post C2')"
    4.35 -    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)
    4.36 -  moreover note vars = `S' \<in> L X` `vars b \<subseteq> X`
    4.37 -  ultimately show ?case using `S \<subseteq> \<gamma>\<^isub>o S'`
    4.38 -    by (simp add: If.IH subset_iff bfilter_sound[OF vars] bfilter_in_L[OF vars])
    4.39 +  case (If b _ C1 _ C2)
    4.40 +  hence 0: "post C1 \<sqsubseteq> post C1 \<squnion> post C2 \<and> post C2 \<sqsubseteq> post C1 \<squnion> post C2"
    4.41 +    by(simp, metis post_in_L join_ge1 join_ge2)
    4.42 +  have "vars b \<subseteq> X" using If.prems by simp
    4.43 +  note vars = `S \<in> L X` `vars b \<subseteq> X`
    4.44 +  show ?case using If 0
    4.45 +    by (auto simp: mono_gamma_o bfilter_sound[OF vars] bfilter_in_L[OF vars])
    4.46  next
    4.47 -  case (While I b P C1 Q)
    4.48 -  then obtain C1' I' P' Q' where
    4.49 -    "C' = {I'} WHILE b DO {P'} C1' {Q'}"
    4.50 -    "I \<subseteq> \<gamma>\<^isub>o I'" "P \<subseteq> \<gamma>\<^isub>o P'" "Q \<subseteq> \<gamma>\<^isub>o Q'" "C1 \<le> \<gamma>\<^isub>c C1'"
    4.51 -    by (fastforce simp: map_acom_While While_le)
    4.52 -  moreover from this(1) `C' \<in> L X`
    4.53 -  have L: "C1' \<in> L X" "I' \<in> L X" "P' \<in> L X" and "vars b \<subseteq> X" by simp_all
    4.54 -  moreover note compat = `S' \<in> L X` post_in_L[OF L(1)]
    4.55 -  moreover note vars = `I' \<in> L X` `vars b \<subseteq> X`
    4.56 -  moreover have "S \<union> post C1 \<subseteq> \<gamma>\<^isub>o (S' \<squnion> post C1')"
    4.57 -    using `S \<subseteq> \<gamma>\<^isub>o S'` le_post[OF `C1 \<le> \<gamma>\<^isub>c C1'`, simplified]
    4.58 -    by (metis (no_types) join_ge1[OF compat] join_ge2[OF compat] le_sup_iff mono_gamma_o order_trans)
    4.59 -  ultimately show ?case
    4.60 -    by (simp add: While.IH subset_iff bfilter_sound[OF vars] bfilter_in_L[OF vars])
    4.61 +  case (While I b)
    4.62 +  hence vars: "I \<in> L X" "vars b \<subseteq> X" by simp_all
    4.63 +  thus ?case using While
    4.64 +    by (auto simp: mono_gamma_o bfilter_sound[OF vars] bfilter_in_L[OF vars])
    4.65  qed
    4.66  
    4.67 -lemma step'_in_L[simp]:
    4.68 -  "\<lbrakk> C \<in> L X; S \<in> L X \<rbrakk> \<Longrightarrow> step' S C \<in> L X"
    4.69 +lemma step'_in_L[simp]: "\<lbrakk> C \<in> L X; S \<in> L X \<rbrakk> \<Longrightarrow> step' S C \<in> L X"
    4.70  proof(induction C arbitrary: S)
    4.71    case Assign thus ?case by(simp add: L_option_def L_st_def update_def split: option.splits)
    4.72  qed (auto simp add: bfilter_in_L)
    4.73  
    4.74 -theorem AI_sound: "AI c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C"
    4.75 +lemma AI_sound: "AI c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C"
    4.76  proof(simp add: CS_def AI_def)
    4.77    assume 1: "pfp (step' (top c)) (bot c) = Some C"
    4.78    have "C \<in> L(vars c)"
    4.79      by(rule pfp_inv[where P = "%C. C \<in> L(vars c)", OF 1 _ bot_in_L])
    4.80        (erule step'_in_L[OF _ top_in_L])
    4.81 -  have 2: "step' (top c) C \<sqsubseteq> C" by(rule pfp_pfp[OF 1])
    4.82 -  have 3: "strip (\<gamma>\<^isub>c (step' (top c) C)) = c"
    4.83 -    by(simp add: strip_pfp[OF _ 1])
    4.84 -  have "lfp c (step UNIV) \<le> \<gamma>\<^isub>c (step' (top c) C)"
    4.85 -  proof(rule lfp_lowerbound[simplified,OF 3])
    4.86 -    show "step UNIV (\<gamma>\<^isub>c (step' (top c) C)) \<le> \<gamma>\<^isub>c (step' (top c) C)"
    4.87 -    proof(rule step_preserves_le[OF _ _ `C \<in> L(vars c)` top_in_L])
    4.88 -      show "UNIV \<subseteq> \<gamma>\<^isub>o (top c)" by simp
    4.89 -      show "\<gamma>\<^isub>c (step' (top c) C) \<le> \<gamma>\<^isub>c C" by(rule mono_gamma_c[OF 2])
    4.90 -    qed
    4.91 +  have pfp': "step' (top c) C \<sqsubseteq> C" by(rule pfp_pfp[OF 1])
    4.92 +  have 2: "step (\<gamma>\<^isub>o(top c)) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C"
    4.93 +  proof(rule order_trans)
    4.94 +    show "step (\<gamma>\<^isub>o (top c)) (\<gamma>\<^isub>c C) \<le>  \<gamma>\<^isub>c (step' (top c) C)"
    4.95 +      by(rule step_step'[OF `C \<in> L(vars c)` top_in_L])
    4.96 +    show "\<gamma>\<^isub>c (step' (top c) C) \<le> \<gamma>\<^isub>c C"
    4.97 +      by(rule mono_gamma_c[OF pfp'])
    4.98    qed
    4.99 -  from this 2 show "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C"
   4.100 -    by (blast intro: mono_gamma_c order_trans)
   4.101 +  have 3: "strip (\<gamma>\<^isub>c C) = c" by(simp add: strip_pfp[OF _ 1])
   4.102 +  have "lfp c (step (\<gamma>\<^isub>o(top c))) \<le> \<gamma>\<^isub>c C"
   4.103 +    by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o(top c))", OF 3 2])
   4.104 +  thus "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C" by simp
   4.105  qed
   4.106  
   4.107  end
     5.1 --- a/src/HOL/IMP/Abs_Int3.thy	Sat Jan 19 17:42:12 2013 +0100
     5.2 +++ b/src/HOL/IMP/Abs_Int3.thy	Sat Jan 19 21:05:05 2013 +0100
     5.3 @@ -366,18 +366,17 @@
     5.4    have 2: "(strip C = c & C \<in> L(vars c)) \<and> step' \<top>\<^bsub>c\<^esub> C \<sqsubseteq> C"
     5.5      by(rule pfp_wn_pfp[where x="bot c"])
     5.6        (simp_all add: 1 mono_step'_top widen_c_in_L narrow_c_in_L)
     5.7 -  have 3: "strip (\<gamma>\<^isub>c (step' \<top>\<^bsub>c\<^esub> C)) = c" by(simp add: strip_pfp_wn[OF _ 1])
     5.8 -  have "lfp c (step UNIV) \<le> \<gamma>\<^isub>c (step' \<top>\<^bsub>c\<^esub> C)"
     5.9 -  proof(rule lfp_lowerbound[simplified,OF 3])
    5.10 -    show "step UNIV (\<gamma>\<^isub>c (step' \<top>\<^bsub>c\<^esub> C)) \<le> \<gamma>\<^isub>c (step' \<top>\<^bsub>c\<^esub> C)"
    5.11 -    proof(rule step_preserves_le[OF _ _ _ top_in_L])
    5.12 -      show "UNIV \<subseteq> \<gamma>\<^isub>o \<top>\<^bsub>c\<^esub>" by simp
    5.13 -      show "\<gamma>\<^isub>c (step' \<top>\<^bsub>c\<^esub> C) \<le> \<gamma>\<^isub>c C" by(rule mono_gamma_c[OF conjunct2[OF 2]])
    5.14 -      show "C \<in> L(vars c)" using 2 by blast
    5.15 -    qed
    5.16 +  have pfp: "step (\<gamma>\<^isub>o(top c)) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C"
    5.17 +  proof(rule order_trans)
    5.18 +    show "step (\<gamma>\<^isub>o (top c)) (\<gamma>\<^isub>c C) \<le>  \<gamma>\<^isub>c (step' (top c) C)"
    5.19 +      by(rule step_step'[OF conjunct2[OF conjunct1[OF 2]] top_in_L])
    5.20 +    show "... \<le> \<gamma>\<^isub>c C"
    5.21 +      by(rule mono_gamma_c[OF conjunct2[OF 2]])
    5.22    qed
    5.23 -  from this 2 show "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C"
    5.24 -    by (blast intro: mono_gamma_c order_trans)
    5.25 +  have 3: "strip (\<gamma>\<^isub>c C) = c" by(simp add: strip_pfp_wn[OF _ 1])
    5.26 +  have "lfp c (step (\<gamma>\<^isub>o (top c))) \<le> \<gamma>\<^isub>c C"
    5.27 +    by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o(top c))", OF 3 pfp])
    5.28 +  thus "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C" by simp
    5.29  qed
    5.30  
    5.31  end
     6.1 --- a/src/HOL/IMP/Abs_Int_ITP/ACom_ITP.thy	Sat Jan 19 17:42:12 2013 +0100
     6.2 +++ b/src/HOL/IMP/Abs_Int_ITP/ACom_ITP.thy	Sat Jan 19 21:05:05 2013 +0100
     6.3 @@ -4,9 +4,6 @@
     6.4  imports "../Com"
     6.5  begin
     6.6  
     6.7 -(* is there a better place? *)
     6.8 -definition "show_state xs s = [(x,s x). x \<leftarrow> xs]"
     6.9 -
    6.10  subsection "Annotated Commands"
    6.11  
    6.12  datatype 'a acom =
     7.1 --- a/src/HOL/IMP/Collecting_Examples.thy	Sat Jan 19 17:42:12 2013 +0100
     7.2 +++ b/src/HOL/IMP/Collecting_Examples.thy	Sat Jan 19 21:05:05 2013 +0100
     7.3 @@ -12,7 +12,7 @@
     7.4                  DO ''x'' ::= Plus (V ''x'') (N 2)"
     7.5  definition C0 :: "state set acom" where "C0 = anno {} c"
     7.6  
     7.7 -definition "show_acom xs = map_acom (\<lambda>S. show_state xs ` S)"
     7.8 +definition "show_acom xs = map_acom (\<lambda>S. (\<lambda>s. [(x,s x). x \<leftarrow> xs]) ` S)"
     7.9  
    7.10  text{* Collecting semantics: *}
    7.11  
     8.1 --- a/src/HOL/IMP/Hoare_Examples.thy	Sat Jan 19 17:42:12 2013 +0100
     8.2 +++ b/src/HOL/IMP/Hoare_Examples.thy	Sat Jan 19 21:05:05 2013 +0100
     8.3 @@ -5,7 +5,7 @@
     8.4  subsection{* Example: Sums *}
     8.5  
     8.6  text{* Summing up the first @{text n} natural numbers. The sum is accumulated
     8.7 -in variable @{text 0}, the loop counter is variable @{text 1}. *}
     8.8 +in variable @{text x}, the loop counter is variable @{text y}. *}
     8.9  
    8.10  abbreviation "w n ==
    8.11    WHILE Less (V ''y'') (N n)