# HG changeset patch
# User nipkow
# Date 1363001251 -3600
# Node ID 1dff81cf425bdd17499e4e98dc510a2b96528426
# Parent  8a9f0503b1c01d956bc3da13fea4cde1bd8e5649
more factorisation of Step & Co

diff -r 8a9f0503b1c0 -r 1dff81cf425b src/HOL/IMP/Abs_Int0.thy
--- a/src/HOL/IMP/Abs_Int0.thy	Sun Mar 10 18:29:10 2013 +0100
+++ b/src/HOL/IMP/Abs_Int0.thy	Mon Mar 11 12:27:31 2013 +0100
@@ -9,33 +9,9 @@
 declare order_trans[trans]
 
 class semilattice = semilattice_sup + top
-(* +
-assumes join_ge1 [simp]: "x \<le> x \<squnion> y"
-and join_ge2 [simp]: "y \<le> x \<squnion> y"
-and join_least: "x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> x \<squnion> y \<le> z"
-begin
-
-lemma join_le_iff[simp]: "x \<squnion> y \<le> z \<longleftrightarrow> x \<le> z \<and> y \<le> z"
-by (metis join_ge1 join_ge2 join_least order_trans)
-*)
-
-lemma le_join_disj: "x \<le> y \<or> x \<le> z \<Longrightarrow> x \<le> y \<squnion> (z::'a::semilattice_sup)"
-by (metis sup_ge1 sup_ge2 order_trans)
 
 
 instance "fun" :: (type, semilattice) semilattice ..
-(*
-definition top_fun where "top_fun = (\<lambda>x. \<top>)"
-
-lemma join_apply[simp]: "(f \<squnion> g) x = f x \<squnion> g x"
-by (simp add: join_fun_def)
-
-instance
-proof
-qed (simp_all add: le_fun_def)
-
-end
-*)
 
 instantiation option :: (order)order
 begin
@@ -97,6 +73,9 @@
 
 end
 
+lemma [simp]: "(Some x < Some y) = (x < y)"
+by(auto simp: less_le)
+
 instantiation option :: (order)bot
 begin
 
@@ -178,34 +157,14 @@
 "aval' (V x) S = S x" |
 "aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
 
-(* Interpretation would be nicer but is impossible *)
-definition "step' = Step.Step
+definition "step' = Step
   (\<lambda>x e S. case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(S(x := aval' e S)))
   (\<lambda>b S. S)"
 
-lemma [simp]: "step' S (SKIP {P}) = (SKIP {S})"
-by(simp add: step'_def Step.Step.simps)
-lemma [simp]: "step' S (x ::= e {P}) =
-  x ::= e {case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(S(x := aval' e S))}"
-by(simp add: step'_def Step.Step.simps)
-lemma [simp]: "step' S (C1; C2) = step' S C1; step' (post C1) C2"
-by(simp add: step'_def Step.Step.simps)
-lemma [simp]: "step' S (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) =
-   IF b THEN {S} step' P1 C1 ELSE {S} step' P2 C2
-   {post C1 \<squnion> post C2}"
-by(simp add: step'_def Step.Step.simps)
-lemma [simp]: "step' S ({I} WHILE b DO {P} C {Q}) =
-  {S \<squnion> post C} WHILE b DO {I} step' P C {I}"
-by(simp add: step'_def Step.Step.simps)
-
 definition AI :: "com \<Rightarrow> 'av st option acom option" where
 "AI c = pfp (step' \<top>) (bot c)"
 
 
-lemma strip_step'[simp]: "strip(step' S C) = strip C"
-by(induct C arbitrary: S) (simp_all add: Let_def)
-
-
 abbreviation \<gamma>\<^isub>s :: "'av st \<Rightarrow> state set"
 where "\<gamma>\<^isub>s == \<gamma>_fun \<gamma>"
 
@@ -236,23 +195,18 @@
 lemma aval'_sound: "s : \<gamma>\<^isub>s S \<Longrightarrow> aval a s : \<gamma>(aval' a S)"
 by (induct a) (auto simp: gamma_num' gamma_plus' \<gamma>_fun_def)
 
-lemma in_gamma_update:
-  "\<lbrakk> s : \<gamma>\<^isub>s S; i : \<gamma> a \<rbrakk> \<Longrightarrow> s(x := i) : \<gamma>\<^isub>s(S(x := a))"
+lemma in_gamma_update: "\<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 gamma_Step_subcomm:
+  assumes "!!x e S. f1 x e (\<gamma>\<^isub>o S) \<subseteq> \<gamma>\<^isub>o (f2 x e S)"  "!!b S. g1 b (\<gamma>\<^isub>o S) \<subseteq> \<gamma>\<^isub>o (g2 b S)"
+  shows "Step f1 g1 (\<gamma>\<^isub>o S) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c (Step f2 g2 S C)"
+proof(induction C arbitrary: S)
+qed  (auto simp: mono_gamma_o assms)
+
 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 intro: aval'_sound in_gamma_update split: option.splits)
-next
-  case Seq thus ?case by auto
-next
-  case If thus ?case by (auto simp: mono_gamma_o)
-next
-  case While thus ?case by (auto simp: mono_gamma_o)
-qed
+unfolding step_def step'_def
+by(rule gamma_Step_subcomm) (auto simp: aval'_sound in_gamma_update split: option.splits)
 
 lemma AI_sound: "AI c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C"
 proof(simp add: CS_def AI_def)
@@ -263,7 +217,7 @@
     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
-  have 3: "strip (\<gamma>\<^isub>c C) = c" by(simp add: strip_pfp[OF _ 1])
+  have 3: "strip (\<gamma>\<^isub>c C) = c" by(simp add: strip_pfp[OF _ 1] step'_def)
   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
@@ -288,10 +242,8 @@
 by(simp add: le_fun_def)
 
 lemma mono_step': "S1 \<le> S2 \<Longrightarrow> C1 \<le> C2 \<Longrightarrow> step' S1 C1 \<le> step' S2 C2"
-apply(induction C1 C2 arbitrary: S1 S2 rule: less_eq_acom.induct)
-apply (auto simp: Let_def mono_update mono_aval' mono_post le_join_disj
-            split: option.split)
-done
+unfolding step'_def
+by(rule mono2_Step) (auto simp: mono_update mono_aval' split: option.split)
 
 end
 
diff -r 8a9f0503b1c0 -r 1dff81cf425b src/HOL/IMP/Abs_Int1.thy
--- a/src/HOL/IMP/Abs_Int1.thy	Sun Mar 10 18:29:10 2013 +0100
+++ b/src/HOL/IMP/Abs_Int1.thy	Mon Mar 11 12:27:31 2013 +0100
@@ -37,8 +37,7 @@
 
 subsection "Computable Abstract Interpretation"
 
-text{* Abstract interpretation over type @{text st} instead of
-functions. *}
+text{* Abstract interpretation over type @{text st} instead of functions. *}
 
 context Gamma
 begin
@@ -51,8 +50,29 @@
 lemma aval'_sound: "s : \<gamma>\<^isub>s S \<Longrightarrow> vars a \<subseteq> dom S \<Longrightarrow> aval a s : \<gamma>(aval' a S)"
 by (induction a) (auto simp: gamma_num' gamma_plus' \<gamma>_st_def)
 
+lemma gamma_Step_subcomm: fixes C1 C2 :: "'a::semilattice_sup acom"
+  assumes "!!x e S. x : X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow> S \<in> L X \<Longrightarrow> f1 x e (\<gamma>\<^isub>o S) \<subseteq> \<gamma>\<^isub>o (f2 x e S)"
+          "!!b S. S \<in> L X \<Longrightarrow> vars b \<subseteq> X \<Longrightarrow> g1 b (\<gamma>\<^isub>o S) \<subseteq> \<gamma>\<^isub>o (g2 b S)"
+  shows "C \<in> L X \<Longrightarrow> S \<in> L X \<Longrightarrow> Step f1 g1 (\<gamma>\<^isub>o S) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c (Step f2 g2 S C)"
+proof(induction C arbitrary: S)
+qed (auto simp: assms intro!: mono_gamma_o post_in_L sup_ge1 sup_ge2)
+
+lemma in_gamma_update: "\<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)
+
 end
 
+
+lemma Step_in_L: fixes C :: "'a::semilatticeL acom"
+assumes "!!x e S. \<lbrakk>S \<in> L X; x \<in> X; vars e \<subseteq> X\<rbrakk> \<Longrightarrow> f x e S \<in> L X"
+        "!!b S. S \<in> L X \<Longrightarrow> vars b \<subseteq> X \<Longrightarrow> g b S \<in> L X"
+shows"\<lbrakk> C \<in> L X; S \<in> L X \<rbrakk> \<Longrightarrow> Step f g S C \<in> L X"
+proof(induction C arbitrary: S)
+  case Assign thus ?case
+    by(auto simp: L_st_def assms split: option.splits)
+qed (auto simp: assms)
+
+
 text{* The for-clause (here and elsewhere) only serves the purpose of fixing
 the name of the type parameter @{typ 'av} which would otherwise be renamed to
 @{typ 'a}. *}
@@ -60,63 +80,28 @@
 locale Abs_Int = Gamma where \<gamma>=\<gamma> for \<gamma> :: "'av::semilattice \<Rightarrow> val set"
 begin
 
-(* Interpretation would be nicer but is impossible *)
-definition "step' = Step.Step
+definition "step' = Step
   (\<lambda>x e S. case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(update S x (aval' e S)))
   (\<lambda>b S. S)"
 
-lemma [code,simp]: "step' S (SKIP {P}) = (SKIP {S})"
-by(simp add: step'_def Step.Step.simps)
-lemma [code,simp]: "step' S (x ::= e {P}) =
-  x ::= e {case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(update S x (aval' e S))}"
-by(simp add: step'_def Step.Step.simps)
-lemma [code,simp]: "step' S (C1; C2) = step' S C1; step' (post C1) C2"
-by(simp add: step'_def Step.Step.simps)
-lemma [code,simp]: "step' S (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) =
-   IF b THEN {S} step' P1 C1 ELSE {S} step' P2 C2
-   {post C1 \<squnion> post C2}"
-by(simp add: step'_def Step.Step.simps)
-lemma [code,simp]: "step' S ({I} WHILE b DO {P} C {Q}) =
-  {S \<squnion> post C} WHILE b DO {I} step' P C {I}"
-by(simp add: step'_def Step.Step.simps)
-
 definition AI :: "com \<Rightarrow> 'av st option acom option" where
 "AI c = pfp (step' (Top(vars c))) (bot c)"
 
 
 lemma strip_step'[simp]: "strip(step' S C) = strip C"
-by(induct C arbitrary: S) (simp_all add: Let_def)
+by(simp add: step'_def)
 
 
 text{* Soundness: *}
 
-lemma in_gamma_update:
-  "\<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)
+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)"
+unfolding step_def step'_def
+by(rule gamma_Step_subcomm)
+  (auto simp: L_st_def intro!: aval'_sound in_gamma_update split: option.splits)
 
-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: L_st_def intro: aval'_sound in_gamma_update split: option.splits)
-next
-  case Seq thus ?case by auto
-next
-  case (If b p1 C1 p2 C2 P)
-  hence "post C1 \<le> post C1 \<squnion> post C2 \<and> post C2 \<le> post C1 \<squnion> post C2"
-    by(simp, metis post_in_L sup_ge1 sup_ge2)
-  thus ?case using If by (auto simp: mono_gamma_o)
-next
-  case While thus ?case by (auto simp: mono_gamma_o)
-qed
-
-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(auto simp: L_st_def split: option.splits)
-qed auto
+lemma step'_in_L[simp]: "\<lbrakk> C \<in> L X; S \<in> L X \<rbrakk> \<Longrightarrow> step' S C \<in> L X"
+unfolding step'_def
+by(rule Step_in_L)(auto simp: L_st_def step'_def split: option.splits)
 
 lemma AI_sound: "AI c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C"
 proof(simp add: CS_def AI_def)
@@ -132,7 +117,7 @@
     show "\<gamma>\<^isub>c (step' (Top(vars c)) C) \<le> \<gamma>\<^isub>c C"
       by(rule mono_gamma_c[OF pfp'])
   qed
-  have 3: "strip (\<gamma>\<^isub>c C) = c" by(simp add: strip_pfp[OF _ 1])
+  have 3: "strip (\<gamma>\<^isub>c C) = c" by(simp add: strip_pfp[OF _ 1] step'_def)
   have "lfp c (step (\<gamma>\<^isub>o(Top(vars c)))) \<le> \<gamma>\<^isub>c C"
     by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o(Top(vars c)))", OF 3 2])
   thus "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C" by simp
@@ -147,6 +132,15 @@
   x \<le> y \<or> x \<le> z \<Longrightarrow> x \<le> y \<squnion> z"
 by (metis sup_ge1 sup_ge2 order_trans)
 
+theorem mono2_Step: fixes C1 :: "'a::semilatticeL acom"
+  assumes "!!x e S1 S2. \<lbrakk>S1 \<in> L X; S2 \<in> L X; x \<in> X; vars e \<subseteq> X; S1 \<le> S2\<rbrakk> \<Longrightarrow> f x e S1 \<le> f x e S2"
+          "!!b S1 S2. S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> vars b \<subseteq> X \<Longrightarrow> S1 \<le> S2 \<Longrightarrow> g b S1 \<le> g b S2"
+  shows "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> C1 \<in> L X \<Longrightarrow> C2 \<in> L X \<Longrightarrow>
+  S1 \<le> S2 \<Longrightarrow> C1 \<le> C2 \<Longrightarrow> Step f g S1 C1 \<le> Step f g S2 C2"
+by(induction C1 C2 arbitrary: S1 S2 rule: less_eq_acom.induct)
+  (auto simp: mono_post assms le_sup_disj le_sup_disj[OF  post_in_L post_in_L])
+
+
 locale Abs_Int_mono = Abs_Int +
 assumes mono_plus': "a1 \<le> b1 \<Longrightarrow> a2 \<le> b2 \<Longrightarrow> plus' a1 a2 \<le> plus' b1 b2"
 begin
@@ -157,11 +151,8 @@
 
 theorem mono_step': "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> C1 \<in> L X \<Longrightarrow> C2 \<in> L X \<Longrightarrow>
   S1 \<le> S2 \<Longrightarrow> C1 \<le> C2 \<Longrightarrow> step' S1 C1 \<le> step' S2 C2"
-apply(induction C1 C2 arbitrary: S1 S2 rule: less_eq_acom.induct)
-apply (auto simp: Let_def mono_aval' mono_post
-  le_sup_disj le_sup_disj[OF  post_in_L post_in_L]
-            split: option.split)
-done
+unfolding step'_def
+by(rule mono2_Step) (auto simp: mono_aval' split: option.split)
 
 lemma mono_step'_top: "C \<in> L X \<Longrightarrow> C' \<in> L X \<Longrightarrow>
   C \<le> C' \<Longrightarrow> step' (Top X) C \<le> step' (Top X) C'"
@@ -173,14 +164,14 @@
 and "\<forall>C. C \<in> L(vars c)\<inter>{C. strip C = c} \<longrightarrow> f C \<in> L(vars c)\<inter>{C. strip C = c}"
 and "f C' \<le> C'" "strip C' = c" "C' \<in> L(vars c)" "pfp f (bot c) = Some C"
 shows "C \<le> C'"
-apply(rule while_least[OF assms(1,2) _ _ assms(3) _ assms(6)[unfolded pfp_def]])
-by (simp_all add: assms(4,5) bot_least)
+by(rule while_least[OF assms(1,2) _ _ assms(3) _ assms(6)[unfolded pfp_def]])
+  (simp_all add: assms(4,5) bot_least)
 
 lemma AI_least_pfp: assumes "AI c = Some C"
 and "step' (Top(vars c)) C' \<le> C'" "strip C' = c" "C' \<in> L(vars c)"
 shows "C \<le> C'"
-apply(rule pfp_bot_least[OF _ _ assms(2-4) assms(1)[unfolded AI_def]])
-by (simp_all add: mono_step'_top)
+by(rule pfp_bot_least[OF _ _ assms(2-4) assms(1)[unfolded AI_def]])
+  (simp_all add: mono_step'_top)
 
 end
 
diff -r 8a9f0503b1c0 -r 1dff81cf425b src/HOL/IMP/Abs_Int2.thy
--- a/src/HOL/IMP/Abs_Int2.thy	Sun Mar 10 18:29:10 2013 +0100
+++ b/src/HOL/IMP/Abs_Int2.thy	Mon Mar 11 12:27:31 2013 +0100
@@ -30,16 +30,16 @@
 
 locale Val_abs1_gamma =
   Gamma where \<gamma> = \<gamma> for \<gamma> :: "'av::lattice \<Rightarrow> val set" +
-assumes inter_gamma_subset_gamma_meet:
+assumes inter_gamma_subset_gamma_inf:
   "\<gamma> a1 \<inter> \<gamma> a2 \<subseteq> \<gamma>(a1 \<sqinter> a2)"
 and gamma_bot[simp]: "\<gamma> \<bottom> = {}"
 begin
 
-lemma in_gamma_meet: "x : \<gamma> a1 \<Longrightarrow> x : \<gamma> a2 \<Longrightarrow> x : \<gamma>(a1 \<sqinter> a2)"
-by (metis IntI inter_gamma_subset_gamma_meet set_mp)
+lemma in_gamma_inf: "x : \<gamma> a1 \<Longrightarrow> x : \<gamma> a2 \<Longrightarrow> x : \<gamma>(a1 \<sqinter> a2)"
+by (metis IntI inter_gamma_subset_gamma_inf set_mp)
 
-lemma gamma_meet[simp]: "\<gamma>(a1 \<sqinter> a2) = \<gamma> a1 \<inter> \<gamma> a2"
-by(rule equalityI[OF _ inter_gamma_subset_gamma_meet])
+lemma gamma_inf[simp]: "\<gamma>(a1 \<sqinter> a2) = \<gamma> a1 \<inter> \<gamma> a2"
+by(rule equalityI[OF _ inter_gamma_subset_gamma_inf])
   (metis inf_le1 inf_le2 le_inf_iff mono_gamma)
 
 end
@@ -121,7 +121,7 @@
   moreover have "s x : \<gamma> a" using V by simp
   ultimately show ?case using V(3)
     by(simp add: Let_def \<gamma>_st_def)
-      (metis mono_gamma emptyE in_gamma_meet gamma_bot subset_empty)
+      (metis mono_gamma emptyE in_gamma_inf gamma_bot subset_empty)
 next
   case (Plus e1 e2) thus ?case
     using filter_plus'[OF _ aval''_sound[OF Plus.prems(3)] aval''_sound[OF Plus.prems(3)]]
@@ -146,69 +146,27 @@
       (metis (lifting) afilter_in_L afilter_sound aval''_sound filter_less')
 qed
 
-(* Interpretation would be nicer but is impossible *)
-definition "step' = Step.Step
+definition "step' = Step
   (\<lambda>x e S. case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(update S x (aval' e S)))
   (\<lambda>b S. bfilter b True S)"
 
-lemma [code,simp]: "step' S (SKIP {P}) = (SKIP {S})"
-by(simp add: step'_def Step.Step.simps)
-lemma [code,simp]: "step' S (x ::= e {P}) =
-  x ::= e {case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(update S x (aval' e S))}"
-by(simp add: step'_def Step.Step.simps)
-lemma [code,simp]: "step' S (C1; C2) = step' S C1; step' (post C1) C2"
-by(simp add: step'_def Step.Step.simps)
-lemma [code,simp]: "step' S (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) =
-  (let P1' = bfilter b True S; C1' = step' P1 C1;
-       P2' = bfilter b False S; C2' = step' P2 C2
-   in IF b THEN {P1'} C1' ELSE {P2'} C2' {post C1 \<squnion> post C2})"
-by(simp add: step'_def Step.Step.simps)
-lemma [code,simp]: "step' S ({I} WHILE b DO {p} C {Q}) =
-   {S \<squnion> post C}
-   WHILE b DO {bfilter b True I} step' p C
-   {bfilter b False I}"
-by(simp add: step'_def Step.Step.simps)
-
 definition AI :: "com \<Rightarrow> 'av st option acom option" where
 "AI c = pfp (step' \<top>\<^bsub>vars c\<^esub>) (bot c)"
 
 lemma strip_step'[simp]: "strip(step' S c) = strip c"
-by(induct c arbitrary: S) (simp_all add: Let_def)
+by(simp add: step'_def)
 
 
 subsubsection "Soundness"
 
-lemma in_gamma_update:
-  "\<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)
-
 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: L_st_def intro: aval'_sound in_gamma_update split: option.splits)
-next
-  case Seq thus ?case by auto
-next
-  case (If b _ C1 _ C2)
-  hence 0: "post C1 \<le> post C1 \<squnion> post C2 \<and> post C2 \<le> post C1 \<squnion> post C2"
-    by(simp, metis post_in_L sup_ge1 sup_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)
-  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
+unfolding step_def step'_def
+by(rule gamma_Step_subcomm)
+  (auto simp: L_st_def intro!: aval'_sound bfilter_sound in_gamma_update split: option.splits)
 
 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(auto simp add: L_option_def L_st_def split: option.splits)
-qed (auto simp add: bfilter_in_L)
+unfolding step'_def
+by(rule Step_in_L)(auto simp: bfilter_in_L L_st_def step'_def split: option.splits)
 
 lemma AI_sound: "AI c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C"
 proof(simp add: CS_def AI_def)
@@ -258,31 +216,28 @@
 lemma mono_afilter: "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow>
   r1 \<le> r2 \<Longrightarrow> S1 \<le> S2 \<Longrightarrow> afilter e r1 S1 \<le> afilter e r2 S2"
 apply(induction e arbitrary: r1 r2 S1 S2)
-apply(auto simp: test_num' Let_def inf_mono split: option.splits prod.splits)
-apply (metis mono_gamma subsetD)
-apply (metis inf_mono le_bot mono_fun_L)
-apply (metis inf_mono mono_fun_L mono_update)
+   apply(auto simp: test_num' Let_def inf_mono split: option.splits prod.splits)
+   apply (metis mono_gamma subsetD)
+  apply (metis inf_mono le_bot mono_fun_L)
+ apply (metis inf_mono mono_fun_L mono_update)
 apply(metis mono_aval'' mono_filter_plus'[simplified less_eq_prod_def] fst_conv snd_conv afilter_in_L)
 done
 
 lemma mono_bfilter: "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> vars b \<subseteq> X \<Longrightarrow>
   S1 \<le> S2 \<Longrightarrow> bfilter b bv S1 \<le> bfilter b bv S2"
 apply(induction b arbitrary: bv S1 S2)
-apply(simp)
-apply(simp)
-apply simp
-apply(metis sup_least order_trans[OF _ sup_ge1] order_trans[OF _ sup_ge2] bfilter_in_L)
+   apply(simp)
+  apply(simp)
+ apply simp
+ apply(metis sup_least order_trans[OF _ sup_ge1] order_trans[OF _ sup_ge2] bfilter_in_L)
 apply (simp split: prod.splits)
 apply(metis mono_aval'' mono_afilter mono_filter_less'[simplified less_eq_prod_def] fst_conv snd_conv afilter_in_L)
 done
 
 theorem mono_step': "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> C1 \<in> L X \<Longrightarrow> C2 \<in> L X \<Longrightarrow>
   S1 \<le> S2 \<Longrightarrow> C1 \<le> C2 \<Longrightarrow> step' S1 C1 \<le> step' S2 C2"
-apply(induction C1 C2 arbitrary: S1 S2 rule: less_eq_acom.induct)
-apply (auto simp: Let_def mono_bfilter mono_aval' mono_post
-  le_sup_disj le_sup_disj[OF  post_in_L post_in_L] bfilter_in_L
-            split: option.split)
-done
+unfolding step'_def
+by(rule mono2_Step) (auto simp: mono_aval' mono_bfilter split: option.split)
 
 lemma mono_step'_top: "C1 \<in> L X \<Longrightarrow> C2 \<in> L X \<Longrightarrow>
   C1 \<le> C2 \<Longrightarrow> step' (Top X) C1 \<le> step' (Top X) C2"
diff -r 8a9f0503b1c0 -r 1dff81cf425b src/HOL/IMP/Abs_Int2_ivl.thy
--- a/src/HOL/IMP/Abs_Int2_ivl.thy	Sun Mar 10 18:29:10 2013 +0100
+++ b/src/HOL/IMP/Abs_Int2_ivl.thy	Mon Mar 11 12:27:31 2013 +0100
@@ -1,9 +1,7 @@
 (* Author: Tobias Nipkow *)
 
 theory Abs_Int2_ivl
-imports "~~/src/HOL/Library/Quotient_List"
-        "~~/src/HOL/Library/Extended"
-        Abs_Int2
+imports Abs_Int2
 begin
 
 subsection "Interval Analysis"
diff -r 8a9f0503b1c0 -r 1dff81cf425b src/HOL/IMP/Abs_Int3.thy
--- a/src/HOL/IMP/Abs_Int3.thy	Sun Mar 10 18:29:10 2013 +0100
+++ b/src/HOL/IMP/Abs_Int3.thy	Mon Mar 11 12:27:31 2013 +0100
@@ -350,7 +350,7 @@
 lemma strip_pfp_wn:
   "\<lbrakk> \<forall>C. strip(f C) = strip C; pfp_wn f C = Some C' \<rbrakk> \<Longrightarrow> strip C' = strip C"
 by(auto simp add: pfp_wn_def iter_narrow_def split: option.splits)
-  (metis (no_types) narrow_acom_def strip_iter_widen strip_map2_acom strip_while)
+  (metis (mono_tags) strip_iter_widen strip_narrow_acom strip_while)
 
 
 locale Abs_Int2 = Abs_Int1_mono
@@ -478,17 +478,17 @@
   "C1 \<in> Lc c \<Longrightarrow> C2 \<in> Lc c \<Longrightarrow> \<not> C2 \<le> C1 \<Longrightarrow> m_c (C1 \<nabla> C2) < m_c C1"
 apply(auto simp: Lc_acom_def m_c_def Let_def widen_acom_def)
 apply(subgoal_tac "length(annos C2) = length(annos C1)")
-prefer 2 apply (simp add: size_annos_same2)
+ prefer 2 apply (simp add: size_annos_same2)
 apply (auto)
 apply(rule setsum_strict_mono_ex1)
-apply simp
-apply (clarsimp)
-apply(simp add: m_o_anti_mono finite_cvars widen1[where c = "strip C2"])
+  apply simp
+ apply (clarsimp)
+ apply(simp add: m_o_anti_mono finite_cvars widen1[where c = "strip C2"])
 apply(auto simp: le_iff_le_annos listrel_iff_nth)
 apply(rule_tac x=i in bexI)
-prefer 2 apply simp
+ prefer 2 apply simp
 apply(rule m_o_widen)
-apply (simp add: finite_cvars)+
+   apply (simp add: finite_cvars)+
 done
 
 
@@ -525,10 +525,6 @@
 definition n_o :: "'av st option \<Rightarrow> nat" ("n\<^isub>o") where
 "n\<^isub>o opt = (case opt of None \<Rightarrow> 0 | Some S \<Rightarrow> n\<^isub>s S + 1)"
 
-(* FIXME mv *)
-lemma [simp]: "(Some x < Some y) = (x < y)"
-by(auto simp: less_le)
-
 lemma n_o_narrow:
   "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> finite X
   \<Longrightarrow> S2 \<le> S1 \<Longrightarrow> S1 \<triangle> S2 < S1 \<Longrightarrow> n\<^isub>o (S1 \<triangle> S2) < n\<^isub>o S1"
@@ -689,7 +685,7 @@
 apply(erule iter_widen_pfp)
 done
 
-(*unused_thms Abs_Int_init -*)
+(*unused_thms Abs_Int_init - *)
 
 subsubsection "Counterexamples"
 
diff -r 8a9f0503b1c0 -r 1dff81cf425b src/HOL/IMP/Abs_Int_init.thy
--- a/src/HOL/IMP/Abs_Int_init.thy	Sun Mar 10 18:29:10 2013 +0100
+++ b/src/HOL/IMP/Abs_Int_init.thy	Mon Mar 11 12:27:31 2013 +0100
@@ -1,8 +1,10 @@
 theory Abs_Int_init
 imports "~~/src/HOL/Library/While_Combinator"
+        "~~/src/HOL/Library/Quotient_List"
+        "~~/src/HOL/Library/Extended"
         Vars Collecting Abs_Int_Tests
 begin
 
-hide_const (open) top bot dom --"to avoid qualified names"
+hide_const (open) top bot dom  --"to avoid qualified names"
 
 end
diff -r 8a9f0503b1c0 -r 1dff81cf425b src/HOL/IMP/Collecting.thy
--- a/src/HOL/IMP/Collecting.thy	Sun Mar 10 18:29:10 2013 +0100
+++ b/src/HOL/IMP/Collecting.thy	Mon Mar 11 12:27:31 2013 +0100
@@ -11,23 +11,26 @@
   bot ("\<bottom>") and
   top ("\<top>")
 
-locale Step =
-fixes step_assign :: "vname \<Rightarrow> aexp \<Rightarrow> 'a \<Rightarrow> 'a::sup"
-and step_cond :: "bexp \<Rightarrow> 'a \<Rightarrow> 'a"
-begin
+fun Step :: "(vname \<Rightarrow> aexp \<Rightarrow> 'a \<Rightarrow> 'a::sup) \<Rightarrow> (bexp \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a acom \<Rightarrow> 'a acom" where
+"Step f g S (SKIP {Q}) = (SKIP {S})" |
+"Step f g S (x ::= e {Q}) =
+  x ::= e {f x e S}" |
+"Step f g S (C1; C2) = Step f g S C1; Step f g (post C1) C2" |
+"Step f g S (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) =
+  IF b THEN {g b S} Step f g P1 C1 ELSE {g (Not b) S} Step f g P2 C2
+  {post C1 \<squnion> post C2}" |
+"Step f g S ({I} WHILE b DO {P} C {Q}) =
+  {S \<squnion> post C} WHILE b DO {g b I} Step f g P C {g (Not b) I}"
 
-fun Step :: "'a \<Rightarrow> 'a acom \<Rightarrow> 'a acom" where
-"Step S (SKIP {Q}) = (SKIP {S})" |
-"Step S (x ::= e {Q}) =
-  x ::= e {step_assign x e S}" |
-"Step S (C1; C2) = Step S C1; Step (post C1) C2" |
-"Step S (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) =
-  IF b THEN {step_cond b S} Step P1 C1 ELSE {step_cond (Not b) S} Step P2 C2
-  {post C1 \<squnion> post C2}" |
-"Step S ({I} WHILE b DO {P} C {Q}) =
-  {S \<squnion> post C} WHILE b DO {step_cond b I} Step P C {step_cond (Not b) I}"
+(* Could hide f and g like this:
+consts fa :: "vname \<Rightarrow> aexp \<Rightarrow> 'a \<Rightarrow> 'a::sup"
+       fb :: "bexp \<Rightarrow> 'a \<Rightarrow> 'a::sup"
+abbreviation "STEP == Step fa fb"
+thm Step.simps[where f = fa and g = fb]
+*)
 
-end
+lemma strip_Step[simp]: "strip(Step f g S C) = strip C"
+by(induct C arbitrary: S) auto
 
 
 subsection "Collecting Semantics of Commands"
@@ -169,31 +172,35 @@
 
 subsubsection "Collecting semantics"
 
-interpretation Step
-where step_assign = "\<lambda>x e S. {s(x := aval e s) |s. s : S}"
-and step_cond = "\<lambda>b S. {s:S. bval b s}"
-defines step is Step
-.
+definition "step = Step (\<lambda>x e S. {s(x := aval e s) |s. s : S}) (\<lambda>b S. {s:S. bval b s})"
 
 definition CS :: "com \<Rightarrow> state set acom" where
 "CS c = lfp c (step UNIV)"
 
-lemma mono2_step: "c1 \<le> c2 \<Longrightarrow> S1 \<subseteq> S2 \<Longrightarrow> step S1 c1 \<le> step S2 c2"
-proof(induction c1 c2 arbitrary: S1 S2 rule: less_eq_acom.induct)
-  case 2 thus ?case by fastforce
+lemma mono2_Step: fixes C1 C2 :: "'a::semilattice_sup acom"
+  assumes "!!x e S1 S2. S1 \<le> S2 \<Longrightarrow> f x e S1 \<le> f x e S2"
+          "!!b S1 S2. S1 \<le> S2 \<Longrightarrow> g b S1 \<le> g b S2"
+  shows "C1 \<le> C2 \<Longrightarrow> S1 \<le> S2 \<Longrightarrow> Step f g S1 C1 \<le> Step f g S2 C2"
+proof(induction C1 C2 arbitrary: S1 S2 rule: less_eq_acom.induct)
+  case 2 thus ?case by (fastforce simp: assms(1))
 next
   case 3 thus ?case by(simp add: le_post)
 next
-  case 4 thus ?case by(simp add: subset_iff)(metis le_post set_mp)+
+  case 4 thus ?case
+    by(simp add: subset_iff assms(2)) (metis le_post le_supI1 le_supI2)
 next
-  case 5 thus ?case by(simp add: subset_iff) (metis le_post set_mp)
+  case 5 thus ?case
+    by(simp add: subset_iff assms(2)) (metis le_post le_supI1 le_supI2)
 qed auto
 
+lemma mono2_step: "C1 \<le> C2 \<Longrightarrow> S1 \<subseteq> S2 \<Longrightarrow> step S1 C1 \<le> step S2 C2"
+unfolding step_def by(rule mono2_Step) auto
+
 lemma mono_step: "mono (step S)"
 by(blast intro: monoI mono2_step)
 
 lemma strip_step: "strip(step S C) = strip C"
-by (induction C arbitrary: S) auto
+by (induction C arbitrary: S) (auto simp: step_def)
 
 lemma lfp_cs_unfold: "lfp c (step S) = step S (lfp c (step S))"
 apply(rule lfp_unfold[OF _  mono_step])
@@ -224,23 +231,24 @@
 lemma big_step_post_step:
   "\<lbrakk> (c, s) \<Rightarrow> t;  strip C = c;  s \<in> S;  step S C \<le> C \<rbrakk> \<Longrightarrow> t \<in> post C"
 proof(induction arbitrary: C S rule: big_step_induct)
-  case Skip thus ?case by(auto simp: strip_eq_SKIP)
+  case Skip thus ?case by(auto simp: strip_eq_SKIP step_def)
 next
-  case Assign thus ?case by(fastforce simp: strip_eq_Assign)
+  case Assign thus ?case by(fastforce simp: strip_eq_Assign step_def)
 next
-  case Seq thus ?case by(fastforce simp: strip_eq_Seq)
+  case Seq thus ?case by(fastforce simp: strip_eq_Seq step_def)
 next
-  case IfTrue thus ?case apply(auto simp: strip_eq_If)
-    by (metis (lifting) mem_Collect_eq set_mp)
+  case IfTrue thus ?case apply(auto simp: strip_eq_If step_def)
+    by (metis (lifting,full_types) mem_Collect_eq set_mp)
 next
-  case IfFalse thus ?case apply(auto simp: strip_eq_If)
-    by (metis (lifting) mem_Collect_eq set_mp)
+  case IfFalse thus ?case apply(auto simp: strip_eq_If step_def)
+    by (metis (lifting,full_types) mem_Collect_eq set_mp)
 next
   case (WhileTrue b s1 c' s2 s3)
   from WhileTrue.prems(1) obtain I P C' Q where "C = {I} WHILE b DO {P} C' {Q}" "strip C' = c'"
     by(auto simp: strip_eq_While)
   from WhileTrue.prems(3) `C = _`
-  have "step P C' \<le> C'"  "{s \<in> I. bval b s} \<le> P"  "S \<le> I"  "step (post C') C \<le> C"  by auto
+  have "step P C' \<le> C'"  "{s \<in> I. bval b s} \<le> P"  "S \<le> I"  "step (post C') C \<le> C"
+    by (auto simp: step_def)
   have "step {s \<in> I. bval b s} C' \<le> C'"
     by (rule order_trans[OF mono2_step[OF order_refl `{s \<in> I. bval b s} \<le> P`] `step P C' \<le> C'`])
   have "s1: {s:I. bval b s}" using `s1 \<in> S` `S \<subseteq> I` `bval b s1` by auto
@@ -248,7 +256,7 @@
   from WhileTrue.IH(2)[OF WhileTrue.prems(1) s2_in_post_C' `step (post C') C \<le> C`]
   show ?case .
 next
-  case (WhileFalse b s1 c') thus ?case by (force simp: strip_eq_While)
+  case (WhileFalse b s1 c') thus ?case by (force simp: strip_eq_While step_def)
 qed
 
 lemma big_step_lfp: "\<lbrakk> (c,s) \<Rightarrow> t;  s \<in> S \<rbrakk> \<Longrightarrow> t \<in> post(lfp c (step S))"