# HG changeset patch
# User nipkow
# Date 1368663222 -7200
# Node ID db08e493cf441fd11cdb7e864d7517b058365a01
# Parent  4ea9a385ec8369dc43cc9eb895fde5816fb3cfbf# Parent  a4cbca8f7342e599dc4fb1fbe88791433cde9de1
merged

diff -r 4ea9a385ec83 -r db08e493cf44 src/HOL/IMP/ACom.thy
--- a/src/HOL/IMP/ACom.thy	Wed May 15 23:00:17 2013 +0200
+++ b/src/HOL/IMP/ACom.thy	Thu May 16 02:13:42 2013 +0200
@@ -15,15 +15,6 @@
   While 'a bexp 'a "('a acom)" 'a
     ("({_}//WHILE _//DO ({_}//_)//{_})"  [0, 0, 0, 61, 0] 61)
 
-text_raw{*\snip{postdef}{2}{1}{% *}
-fun post :: "'a acom \<Rightarrow>'a" where
-"post (SKIP {P}) = P" |
-"post (x ::= e {P}) = P" |
-"post (C\<^isub>1; C\<^isub>2) = post C\<^isub>2" |
-"post (IF b THEN {P\<^isub>1} C\<^isub>1 ELSE {P\<^isub>2} C\<^isub>2 {Q}) = Q" |
-"post ({I} WHILE b DO {P} C {Q}) = Q"
-text_raw{*}%endsnip*}
-
 text_raw{*\snip{stripdef}{1}{1}{% *}
 fun strip :: "'a acom \<Rightarrow> com" where
 "strip (SKIP {P}) = com.SKIP" |
@@ -34,15 +25,29 @@
 "strip ({I} WHILE b DO {P} C {Q}) = WHILE b DO strip C"
 text_raw{*}%endsnip*}
 
-text_raw{*\snip{annodef}{1}{1}{% *}
-fun anno :: "'a \<Rightarrow> com \<Rightarrow> 'a acom" where
-"anno A com.SKIP = SKIP {A}" |
-"anno A (x ::= e) = x ::= e {A}" |
-"anno A (c\<^isub>1;c\<^isub>2) = anno A c\<^isub>1; anno A c\<^isub>2" |
-"anno A (IF b THEN c\<^isub>1 ELSE c\<^isub>2) =
-  IF b THEN {A} anno A c\<^isub>1 ELSE {A} anno A c\<^isub>2 {A}" |
-"anno A (WHILE b DO c) =
-  {A} WHILE b DO {A} anno A c {A}"
+text_raw{*\snip{asizedef}{1}{1}{% *}
+fun asize :: "com \<Rightarrow> nat" where
+"asize com.SKIP = 1" |
+"asize (x ::= e) = 1" |
+"asize (C\<^isub>1;C\<^isub>2) = asize C\<^isub>1 + asize C\<^isub>2" |
+"asize (IF b THEN C\<^isub>1 ELSE C\<^isub>2) = asize C\<^isub>1 + asize C\<^isub>2 + 3" |
+"asize (WHILE b DO C) = asize C + 3"
+text_raw{*}%endsnip*}
+
+text_raw{*\snip{annotatedef}{1}{1}{% *}
+definition shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a" where
+"shift f n = (\<lambda>p. f(p+n))"
+
+fun annotate :: "(nat \<Rightarrow> 'a) \<Rightarrow> com \<Rightarrow> 'a acom" where
+"annotate f com.SKIP = SKIP {f 0}" |
+"annotate f (x ::= e) = x ::= e {f 0}" |
+"annotate f (c\<^isub>1;c\<^isub>2) = annotate f c\<^isub>1; annotate (shift f (asize c\<^isub>1)) c\<^isub>2" |
+"annotate f (IF b THEN c\<^isub>1 ELSE c\<^isub>2) =
+  IF b THEN {f 0} annotate (shift f 1) c\<^isub>1
+  ELSE {f(asize c\<^isub>1 + 1)} annotate (shift f (asize c\<^isub>1 + 2)) c\<^isub>2
+  {f(asize c\<^isub>1 + asize c\<^isub>2 + 2)}" |
+"annotate f (WHILE b DO c) =
+  {f 0} WHILE b DO {f 1} annotate (shift f 2) c {f(asize c + 2)}"
 text_raw{*}%endsnip*}
 
 text_raw{*\snip{annosdef}{1}{1}{% *}
@@ -51,10 +56,16 @@
 "annos (x ::= e {P}) = [P]" |
 "annos (C\<^isub>1;C\<^isub>2) = annos C\<^isub>1 @ annos C\<^isub>2" |
 "annos (IF b THEN {P\<^isub>1} C\<^isub>1 ELSE {P\<^isub>2} C\<^isub>2 {Q}) =
-  P\<^isub>1 # P\<^isub>2 # Q # annos C\<^isub>1 @ annos C\<^isub>2" |
-"annos ({I} WHILE b DO {P} C {Q}) = I # P # Q # annos C"
+  P\<^isub>1 # annos C\<^isub>1 @  P\<^isub>2 # annos C\<^isub>2 @ [Q]" |
+"annos ({I} WHILE b DO {P} C {Q}) = I # P # annos C @ [Q]"
 text_raw{*}%endsnip*}
 
+definition anno :: "'a acom \<Rightarrow> nat \<Rightarrow> 'a" where
+"anno C p = annos C ! p"
+
+definition post :: "'a acom \<Rightarrow>'a" where
+"post C = last(annos C)"
+
 text_raw{*\snip{mapacomdef}{1}{2}{% *}
 fun map_acom :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a acom \<Rightarrow> 'b acom" where
 "map_acom f (SKIP {P}) = SKIP {f P}" |
@@ -68,39 +79,56 @@
 text_raw{*}%endsnip*}
 
 
+lemma annos_ne: "annos C \<noteq> []"
+by(induction C) auto
+
+lemma strip_annotate[simp]: "strip(annotate f c) = c"
+by(induction c arbitrary: f) auto
+
+lemma length_annos_annotate[simp]: "length (annos (annotate f c)) = asize c"
+by(induction c arbitrary: f) auto
+
+lemma size_annos: "size(annos C) = asize(strip C)"
+by(induction C)(auto)
+
+lemma size_annos_same: "strip C1 = strip C2 \<Longrightarrow> size(annos C1) = size(annos C2)"
+apply(induct C2 arbitrary: C1)
+apply(case_tac C1, simp_all)+
+done
+
+lemmas size_annos_same2 = eqTrueI[OF size_annos_same]
+
+lemma anno_annotate[simp]: "p < asize c \<Longrightarrow> anno (annotate f c) p = f p"
+apply(induction c arbitrary: f p)
+apply (auto simp: anno_def nth_append nth_Cons numeral_eq_Suc shift_def
+            split: nat.split)
+  apply (metis add_Suc_right add_diff_inverse nat_add_commute)
+ apply(rule_tac f=f in arg_cong)
+ apply arith
+apply (metis less_Suc_eq)
+done
+
+lemma eq_acom_iff_strip_annos:
+  "C1 = C2 \<longleftrightarrow> strip C1 = strip C2 \<and> annos C1 = annos C2"
+apply(induction C1 arbitrary: C2)
+apply(case_tac C2, auto simp: size_annos_same2)+
+done
+
+lemma eq_acom_iff_strip_anno:
+  "C1=C2 \<longleftrightarrow> strip C1 = strip C2 \<and> (\<forall>p<size(annos C1). anno C1 p = anno C2 p)"
+by(auto simp add: eq_acom_iff_strip_annos anno_def
+     list_eq_iff_nth_eq size_annos_same2)
+
 lemma post_map_acom[simp]: "post(map_acom f C) = f(post C)"
-by (induction C) simp_all
+by (induction C) (auto simp: post_def last_append annos_ne)
 
-lemma strip_acom[simp]: "strip (map_acom f C) = strip C"
+lemma strip_map_acom[simp]: "strip (map_acom f C) = strip C"
 by (induction C) auto
 
-lemma map_acom_SKIP:
- "map_acom f C = SKIP {S'} \<longleftrightarrow> (\<exists>S. C = SKIP {S} \<and> S' = f S)"
-by (cases C) auto
-
-lemma map_acom_Assign:
- "map_acom f C = x ::= e {S'} \<longleftrightarrow> (\<exists>S. C = x::=e {S} \<and> S' = f S)"
-by (cases C) auto
-
-lemma map_acom_Seq:
- "map_acom f C = C1';C2' \<longleftrightarrow>
- (\<exists>C1 C2. C = C1;C2 \<and> map_acom f C1 = C1' \<and> map_acom f C2 = C2')"
-by (cases C) auto
-
-lemma map_acom_If:
- "map_acom f C = IF b THEN {P1'} C1' ELSE {P2'} C2' {Q'} \<longleftrightarrow>
- (\<exists>P1 P2 C1 C2 Q. C = IF b THEN {P1} C1 ELSE {P2} C2 {Q} \<and>
-     map_acom f C1 = C1' \<and> map_acom f C2 = C2' \<and> P1' = f P1 \<and> P2' = f P2 \<and> Q' = f Q)"
-by (cases C) auto
-
-lemma map_acom_While:
- "map_acom f w = {I'} WHILE b DO {p'} C' {P'} \<longleftrightarrow>
- (\<exists>I p P C. w = {I} WHILE b DO {p} C {P} \<and> map_acom f C = C' \<and> I' = f I \<and> p' = f p \<and> P' = f P)"
-by (cases w) auto
-
-
-lemma strip_anno[simp]: "strip (anno a c) = c"
-by(induct c) simp_all
+lemma anno_map_acom: "p < size(annos C) \<Longrightarrow> anno (map_acom f C) p = f(anno C p)"
+apply(induction C arbitrary: p)
+apply(auto simp: anno_def nth_append nth_Cons' size_annos)
+done
 
 lemma strip_eq_SKIP:
   "strip C = com.SKIP \<longleftrightarrow> (EX P. C = SKIP {P})"
@@ -124,17 +152,16 @@
   (EX I P C1 Q. C = {I} WHILE b DO {P} C1 {Q} & strip C1 = c1)"
 by (cases C) simp_all
 
-lemma set_annos_anno[simp]: "set (annos (anno a c)) = {a}"
-by(induction c)(auto)
+lemma [simp]: "shift (\<lambda>p. a) n = (\<lambda>p. a)"
+by(simp add:shift_def)
 
-lemma size_annos_same: "strip C1 = strip C2 \<Longrightarrow> size(annos C1) = size(annos C2)"
-apply(induct C2 arbitrary: C1)
-apply (auto simp: strip_eq_SKIP strip_eq_Assign strip_eq_Seq strip_eq_If strip_eq_While)
-done
-
-lemmas size_annos_same2 = eqTrueI[OF size_annos_same]
+lemma set_annos_anno[simp]: "set (annos (annotate (\<lambda>p. a) c)) = {a}"
+by(induction c) simp_all
 
 lemma post_in_annos: "post C \<in> set(annos C)"
-by(induction C) auto
+by(auto simp: post_def annos_ne)
+
+lemma post_anno_asize: "post C = anno C (size(annos C) - 1)"
+by(simp add: post_def last_conv_nth[OF annos_ne] anno_def)
 
 end
diff -r 4ea9a385ec83 -r db08e493cf44 src/HOL/IMP/Abs_Int0.thy
--- a/src/HOL/IMP/Abs_Int0.thy	Wed May 15 23:00:17 2013 +0200
+++ b/src/HOL/IMP/Abs_Int0.thy	Thu May 16 02:13:42 2013 +0200
@@ -93,10 +93,10 @@
 
 
 definition bot :: "com \<Rightarrow> 'a option acom" where
-"bot c = anno None c"
+"bot c = annotate (\<lambda>p. None) c"
 
 lemma bot_least: "strip C = c \<Longrightarrow> bot c \<le> C"
-by(induct C arbitrary: c)(auto simp: bot_def)
+by(auto simp: bot_def less_eq_acom_def)
 
 lemma strip_bot[simp]: "strip(bot c) = c"
 by(simp add: bot_def)
@@ -206,7 +206,7 @@
 by(induction S1 S2 rule: less_eq_option.induct)(simp_all add: mono_gamma_s)
 
 lemma mono_gamma_c: "C1 \<le> C2 \<Longrightarrow> \<gamma>\<^isub>c C1 \<le> \<gamma>\<^isub>c C2"
-by (induction C1 C2 rule: less_eq_acom.induct) (simp_all add:mono_gamma_o)
+by (simp add: less_eq_acom_def mono_gamma_o size_annos anno_map_acom size_annos_same[of C1 C2])
 
 text{* Correctness: *}
 
@@ -247,9 +247,6 @@
 
 subsubsection "Monotonicity"
 
-lemma mono_post: "C1 \<le> C2 \<Longrightarrow> post C1 \<le> post C2"
-by(induction C1 C2 rule: less_eq_acom.induct) (auto)
-
 locale Abs_Int_fun_mono = Abs_Int_fun +
 assumes mono_plus': "a1 \<le> b1 \<Longrightarrow> a2 \<le> b2 \<Longrightarrow> plus' a1 a2 \<le> plus' b1 b2"
 begin
@@ -307,6 +304,9 @@
     by (blast intro: I mono)
 qed
 
+lemma le_iff_le_annos: "C1 \<le> C2 \<longleftrightarrow>
+  strip C1 = strip C2 \<and> (\<forall> i<size(annos C1). annos C1 ! i \<le> annos C2 ! i)"
+by(simp add: less_eq_acom_def anno_def)
 
 locale Measure1_fun =
 fixes m :: "'av::top \<Rightarrow> nat"
@@ -345,15 +345,6 @@
 end
 
 
-lemma le_iff_le_annos_zip: "C1 \<le> C2 \<longleftrightarrow>
- (\<forall> (a1,a2) \<in> set(zip (annos C1) (annos C2)). a1 \<le> a2) \<and> strip C1 = strip C2"
-by(induct C1 C2 rule: less_eq_acom.induct) (auto simp: size_annos_same2)
-
-lemma le_iff_le_annos: "C1 \<le> C2 \<longleftrightarrow>
-  strip C1 = strip C2 \<and> (\<forall> i<size(annos C1). annos C1 ! i \<le> annos C2 ! i)"
-by(auto simp add: le_iff_le_annos_zip set_zip) (metis size_annos_same2)
-
-
 locale Measure_fun = Measure1_fun where m=m
   for m :: "'av::semilattice_sup_top \<Rightarrow> nat" +
 assumes m2: "x < y \<Longrightarrow> m x > m y"
diff -r 4ea9a385ec83 -r db08e493cf44 src/HOL/IMP/Abs_Int3.thy
--- a/src/HOL/IMP/Abs_Int3.thy	Wed May 15 23:00:17 2013 +0200
+++ b/src/HOL/IMP/Abs_Int3.thy	Thu May 16 02:13:42 2013 +0200
@@ -110,6 +110,11 @@
 
 end
 
+definition map2_acom :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a acom \<Rightarrow> 'a acom \<Rightarrow> 'a acom"
+where
+"map2_acom f C1 C2 = annotate (\<lambda>p. f (anno C1 p) (anno C2 p)) (strip C1)"
+
+(*
 text_raw{*\snip{maptwoacomdef}{2}{2}{% *}
 fun map2_acom :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a acom \<Rightarrow> 'a acom \<Rightarrow> 'a acom"
 where
@@ -125,11 +130,11 @@
   ({a\<^isub>3} WHILE b' DO {q} D {a\<^isub>4})
   = ({f a\<^isub>1 a\<^isub>3} WHILE b DO {f p q} map2_acom f C D {f a\<^isub>2 a\<^isub>4})"
 text_raw{*}%endsnip*}
-
+*)(*
 lemma annos_map2_acom[simp]: "strip C2 = strip C1 \<Longrightarrow>
   annos(map2_acom f C1 C2) = map (%(x,y).f x y) (zip (annos C1) (annos C2))"
 by(induction f C1 C2 rule: map2_acom.induct)(simp_all add: size_annos_same2)
-
+*)
 instantiation acom :: (widen)widen
 begin
 definition "widen_acom = map2_acom (op \<nabla>)"
@@ -144,7 +149,8 @@
 
 lemma strip_map2_acom[simp]:
  "strip C1 = strip C2 \<Longrightarrow> strip(map2_acom f C1 C2) = strip C1"
-by(induct f C1 C2 rule: map2_acom.induct) simp_all
+by(simp add: map2_acom_def)
+(*by(induct f C1 C2 rule: map2_acom.induct) simp_all*)
 
 lemma strip_widen_acom[simp]:
   "strip C1 = strip C2 \<Longrightarrow> strip(C1 \<nabla> C2) = strip C1"
@@ -155,13 +161,13 @@
 by(simp add: narrow_acom_def)
 
 lemma narrow1_acom: "C2 \<le> C1 \<Longrightarrow> C2 \<le> C1 \<triangle> (C2::'a::WN acom)"
-by(induct C1 C2 rule: less_eq_acom.induct)(simp_all add: narrow_acom_def narrow1)
+by(simp add: narrow_acom_def narrow1 map2_acom_def less_eq_acom_def size_annos)
 
 lemma narrow2_acom: "C2 \<le> C1 \<Longrightarrow> C1 \<triangle> (C2::'a::WN acom) \<le> C1"
-by(induct C1 C2 rule: less_eq_acom.induct)(simp_all add: narrow_acom_def narrow2)
+by(simp add: narrow_acom_def narrow2 map2_acom_def less_eq_acom_def size_annos)
 
 
-subsubsection "Post-fixed point computation"
+subsubsection "Pre-fixpoint computation"
 
 definition iter_widen :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> ('a::{order,widen})option"
 where "iter_widen f = while_option (\<lambda>x. \<not> f x \<le> x) (\<lambda>x. x \<nabla> f x)"
@@ -327,6 +333,11 @@
 apply (auto)
 by transfer simp
 
+(* FIXME mk anno abbrv *)
+lemma annos_map2_acom[simp]: "strip C2 = strip C1 \<Longrightarrow>
+  annos(map2_acom f C1 C2) = map (%(x,y).f x y) (zip (annos C1) (annos C2))"
+by(simp add: map2_acom_def list_eq_iff_nth_eq size_annos anno_def[symmetric] size_annos_same[of C1 C2])
+
 lemma top_on_acom_widen:
   "\<lbrakk>top_on_acom C1 X; strip C1 = strip C2; top_on_acom C2 X\<rbrakk>
   \<Longrightarrow> top_on_acom (C1 \<nabla> C2 :: _ st option acom) X"
@@ -403,13 +414,13 @@
 lemma m_c_widen:
   "strip C1 = strip C2  \<Longrightarrow> top_on_acom C1 (-vars C1) \<Longrightarrow> top_on_acom C2 (-vars C2)
    \<Longrightarrow> \<not> C2 \<le> C1 \<Longrightarrow> m_c (C1 \<nabla> C2) < m_c C1"
-apply(auto simp: m_c_def widen_acom_def listsum_setsum_nth)
+apply(auto simp: m_c_def widen_acom_def map2_acom_def size_annos[symmetric] anno_def[symmetric]listsum_setsum_nth)
 apply(subgoal_tac "length(annos C2) = length(annos C1)")
  prefer 2 apply (simp add: size_annos_same2)
 apply (auto)
 apply(rule setsum_strict_mono_ex1)
- apply(auto simp add: m_o_anti_mono vars_acom_def top_on_acom_def top_on_opt_widen widen1 le_iff_le_annos listrel_iff_nth)
-apply(rule_tac x=i in bexI)
+ apply(auto simp add: m_o_anti_mono vars_acom_def anno_def top_on_acom_def top_on_opt_widen widen1 less_eq_acom_def listrel_iff_nth)
+apply(rule_tac x=p in bexI)
  apply (auto simp: vars_acom_def m_o_widen top_on_acom_def)
 done
 
diff -r 4ea9a385ec83 -r db08e493cf44 src/HOL/IMP/Abs_State.thy
--- a/src/HOL/IMP/Abs_State.thy	Wed May 15 23:00:17 2013 +0200
+++ b/src/HOL/IMP/Abs_State.thy	Thu May 16 02:13:42 2013 +0200
@@ -155,7 +155,7 @@
 by(induction S1 S2 rule: less_eq_option.induct)(simp_all add: mono_gamma_s)
 
 lemma mono_gamma_c: "C1 \<le> C2 \<Longrightarrow> \<gamma>\<^isub>c C1 \<le> \<gamma>\<^isub>c C2"
-by (induction C1 C2 rule: less_eq_acom.induct) (simp_all add:mono_gamma_o)
+by (simp add: less_eq_acom_def mono_gamma_o size_annos anno_map_acom size_annos_same[of C1 C2])
 
 lemma in_gamma_option_iff:
   "x : \<gamma>_option r u \<longleftrightarrow> (\<exists>u'. u = Some u' \<and> x : r u')"
diff -r 4ea9a385ec83 -r db08e493cf44 src/HOL/IMP/Collecting.thy
--- a/src/HOL/IMP/Collecting.thy	Wed May 15 23:00:17 2013 +0200
+++ b/src/HOL/IMP/Collecting.thy	Thu May 16 02:13:42 2013 +0200
@@ -11,16 +11,21 @@
   bot ("\<bottom>") and
   top ("\<top>")
 
-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}) =
+context
+  fixes f :: "vname \<Rightarrow> aexp \<Rightarrow> 'a \<Rightarrow> 'a::sup"
+  fixes g :: "bexp \<Rightarrow> 'a \<Rightarrow> 'a"
+begin
+fun Step :: "'a \<Rightarrow> 'a acom \<Rightarrow> 'a acom" where
+"Step S (SKIP {Q}) = (SKIP {S})" |
+"Step 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
+"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 {g b S} Step P1 C1 ELSE {g (Not b) S} Step 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}"
+"Step S ({I} WHILE b DO {P} C {Q}) =
+  {S \<squnion> post C} WHILE b DO {g b I} Step P C {g (Not b) I}"
+end
 
 lemma strip_Step[simp]: "strip(Step f g S C) = strip C"
 by(induct C arbitrary: S) auto
@@ -33,33 +38,8 @@
 instantiation acom :: (order) order
 begin
 
-fun less_eq_acom :: "('a::order)acom \<Rightarrow> 'a acom \<Rightarrow> bool" where
-"(SKIP {P}) \<le> (SKIP {P'}) = (P \<le> P')" |
-"(x ::= e {P}) \<le> (x' ::= e' {P'}) = (x=x' \<and> e=e' \<and> P \<le> P')" |
-"(C1;C2) \<le> (C1';C2') = (C1 \<le> C1' \<and> C2 \<le> C2')" |
-"(IF b THEN {P1} C1 ELSE {P2} C2 {Q}) \<le> (IF b' THEN {P1'} C1' ELSE {P2'} C2' {Q'}) =
-  (b=b' \<and> P1 \<le> P1' \<and> C1 \<le> C1' \<and> P2 \<le> P2' \<and> C2 \<le> C2' \<and> Q \<le> Q')" |
-"({I} WHILE b DO {P} C {Q}) \<le> ({I'} WHILE b' DO {P'} C' {Q'}) =
-  (b=b' \<and> C \<le> C' \<and> I \<le> I' \<and> P \<le> P' \<and> Q \<le> Q')" |
-"less_eq_acom _ _ = False"
-
-lemma SKIP_le: "SKIP {S} \<le> c \<longleftrightarrow> (\<exists>S'. c = SKIP {S'} \<and> S \<le> S')"
-by (cases c) auto
-
-lemma Assign_le: "x ::= e {S} \<le> c \<longleftrightarrow> (\<exists>S'. c = x ::= e {S'} \<and> S \<le> S')"
-by (cases c) auto
-
-lemma Seq_le: "C1;C2 \<le> C \<longleftrightarrow> (\<exists>C1' C2'. C = C1';C2' \<and> C1 \<le> C1' \<and> C2 \<le> C2')"
-by (cases C) auto
-
-lemma If_le: "IF b THEN {p1} C1 ELSE {p2} C2 {S} \<le> C \<longleftrightarrow>
-  (\<exists>p1' p2' C1' C2' S'. C = IF b THEN {p1'} C1' ELSE {p2'} C2' {S'} \<and>
-     p1 \<le> p1' \<and> p2 \<le> p2' \<and> C1 \<le> C1' \<and> C2 \<le> C2' \<and> S \<le> S')"
-by (cases C) auto
-
-lemma While_le: "{I} WHILE b DO {p} C {P} \<le> W \<longleftrightarrow>
-  (\<exists>I' p' C' P'. W = {I'} WHILE b DO {p'} C' {P'} \<and> C \<le> C' \<and> p \<le> p' \<and> I \<le> I' \<and> P \<le> P')"
-by (cases W) auto
+definition less_eq_acom :: "('a::order)acom \<Rightarrow> 'a acom \<Rightarrow> bool" where
+"C1 \<le> C2 \<longleftrightarrow> strip C1 = strip C2 \<and> (\<forall>p<size(annos C1). anno C1 p \<le> anno C2 p)"
 
 definition less_acom :: "'a acom \<Rightarrow> 'a acom \<Rightarrow> bool" where
 "less_acom x y = (x \<le> y \<and> \<not> y \<le> x)"
@@ -68,102 +48,65 @@
 proof
   case goal1 show ?case by(simp add: less_acom_def)
 next
-  case goal2 thus ?case by (induct x) auto
+  case goal2 thus ?case by(auto simp: less_eq_acom_def)
 next
-  case goal3 thus ?case
-  apply(induct x y arbitrary: z rule: less_eq_acom.induct)
-  apply (auto intro: le_trans simp: SKIP_le Assign_le Seq_le If_le While_le)
-  done
+  case goal3 thus ?case by(fastforce simp: less_eq_acom_def size_annos)
 next
   case goal4 thus ?case
-  apply(induct x y rule: less_eq_acom.induct)
-  apply (auto intro: le_antisym)
-  done
+    by(fastforce simp: le_antisym less_eq_acom_def size_annos
+         eq_acom_iff_strip_anno)
 qed
 
 end
 
-text_raw{*\snip{subadef}{2}{1}{% *}
-fun sub\<^isub>1 :: "'a acom \<Rightarrow> 'a acom" where
-"sub\<^isub>1(C\<^isub>1;C\<^isub>2) = C\<^isub>1" |
-"sub\<^isub>1(IF b THEN {P\<^isub>1} C\<^isub>1 ELSE {P\<^isub>2} C\<^isub>2 {Q}) = C\<^isub>1" |
-"sub\<^isub>1({I} WHILE b DO {P} C {Q}) = C"
-text_raw{*}%endsnip*}
+lemma less_eq_acom_annos:
+  "C1 \<le> C2 \<longleftrightarrow> strip C1 = strip C2 \<and> list_all2 (op \<le>) (annos C1) (annos C2)"
+by(auto simp add: less_eq_acom_def anno_def list_all2_conv_all_nth size_annos_same2)
+
+lemma SKIP_le[simp]: "SKIP {S} \<le> c \<longleftrightarrow> (\<exists>S'. c = SKIP {S'} \<and> S \<le> S')"
+by (cases c) (auto simp:less_eq_acom_def anno_def)
 
-text_raw{*\snip{subbdef}{1}{1}{% *}
-fun sub\<^isub>2 :: "'a acom \<Rightarrow> 'a acom" where
-"sub\<^isub>2(C\<^isub>1;C\<^isub>2) = C\<^isub>2" |
-"sub\<^isub>2(IF b THEN {P\<^isub>1} C\<^isub>1 ELSE {P\<^isub>2} C\<^isub>2 {Q}) = C\<^isub>2"
-text_raw{*}%endsnip*}
+lemma Assign_le[simp]: "x ::= e {S} \<le> c \<longleftrightarrow> (\<exists>S'. c = x ::= e {S'} \<and> S \<le> S')"
+by (cases c) (auto simp:less_eq_acom_def anno_def)
 
-text_raw{*\snip{annoadef}{1}{1}{% *}
-fun anno\<^isub>1 :: "'a acom \<Rightarrow> 'a" where
-"anno\<^isub>1(IF b THEN {P\<^isub>1} C\<^isub>1 ELSE {P\<^isub>2} C\<^isub>2 {Q}) = P\<^isub>1" |
-"anno\<^isub>1({I} WHILE b DO {P} C {Q}) = I"
-text_raw{*}%endsnip*}
+lemma Seq_le[simp]: "C1;C2 \<le> C \<longleftrightarrow> (\<exists>C1' C2'. C = C1';C2' \<and> C1 \<le> C1' \<and> C2 \<le> C2')"
+apply (cases C)
+apply(auto simp: less_eq_acom_annos list_all2_append size_annos_same2)
+done
 
-text_raw{*\snip{annobdef}{1}{2}{% *}
-fun anno\<^isub>2 :: "'a acom \<Rightarrow> 'a" where
-"anno\<^isub>2(IF b THEN {P\<^isub>1} C\<^isub>1 ELSE {P\<^isub>2} C\<^isub>2 {Q}) = P\<^isub>2" |
-"anno\<^isub>2({I} WHILE b DO {P} C {Q}) = P"
-text_raw{*}%endsnip*}
+lemma If_le[simp]: "IF b THEN {p1} C1 ELSE {p2} C2 {S} \<le> C \<longleftrightarrow>
+  (\<exists>p1' p2' C1' C2' S'. C = IF b THEN {p1'} C1' ELSE {p2'} C2' {S'} \<and>
+     p1 \<le> p1' \<and> p2 \<le> p2' \<and> C1 \<le> C1' \<and> C2 \<le> C2' \<and> S \<le> S')"
+apply (cases C)
+apply(auto simp: less_eq_acom_annos list_all2_append size_annos_same2)
+done
 
-fun merge :: "com \<Rightarrow> 'a acom set \<Rightarrow> 'a set acom" where
-"merge com.SKIP M = (SKIP {post ` M})" |
-"merge (x ::= a) M = (x ::= a {post ` M})" |
-"merge (c1;c2) M =
-  merge c1 (sub\<^isub>1 ` M); merge c2 (sub\<^isub>2 ` M)" |
-"merge (IF b THEN c1 ELSE c2) M =
-  IF b THEN {anno\<^isub>1 ` M} merge c1 (sub\<^isub>1 ` M) ELSE {anno\<^isub>2 ` M} merge c2 (sub\<^isub>2 ` M)
-  {post ` M}" |
-"merge (WHILE b DO c) M =
- {anno\<^isub>1 ` M}
- WHILE b DO {anno\<^isub>2 ` M} merge c (sub\<^isub>1 ` M)
- {post ` M}"
+lemma While_le[simp]: "{I} WHILE b DO {p} C {P} \<le> W \<longleftrightarrow>
+  (\<exists>I' p' C' P'. W = {I'} WHILE b DO {p'} C' {P'} \<and> C \<le> C' \<and> p \<le> p' \<and> I \<le> I' \<and> P \<le> P')"
+apply (cases W)
+apply(auto simp: less_eq_acom_annos list_all2_append size_annos_same2)
+done
+
+lemma mono_post: "C \<le> C' \<Longrightarrow> post C \<le> post C'"
+using annos_ne[of C']
+by(auto simp: post_def less_eq_acom_def last_conv_nth[OF annos_ne] anno_def
+     dest: size_annos_same)
+
+definition Inf_acom :: "com \<Rightarrow> 'a::complete_lattice acom set \<Rightarrow> 'a acom" where
+"Inf_acom c M = annotate (\<lambda>p. INF C:M. anno C p) c"
 
 interpretation
-  Complete_Lattice "{C. strip C = c}" "map_acom Inter o (merge c)" for c
+  Complete_Lattice "{C. strip C = c}" "Inf_acom c" for c
 proof
-  case goal1
-  have "a:A \<Longrightarrow> map_acom Inter (merge (strip a) A) \<le> a"
-  proof(induction a arbitrary: A)
-    case Seq from Seq.prems show ?case by(force intro!: Seq.IH)
-  next
-    case If from If.prems show ?case by(force intro!: If.IH)
-  next
-    case While from While.prems show ?case by(force intro!: While.IH)
-  qed force+
-  with goal1 show ?case by auto
+  case goal1 thus ?case
+    by(auto simp: Inf_acom_def less_eq_acom_def size_annos intro:INF_lower)
 next
-  case goal2
-  thus ?case
-  proof(simp, induction b arbitrary: c A)
-    case SKIP thus ?case by (force simp:SKIP_le)
-  next
-    case Assign thus ?case by (force simp:Assign_le)
-  next
-    case Seq from Seq.prems show ?case by(force intro!: Seq.IH simp:Seq_le)
-  next
-    case If from If.prems show ?case by (force simp: If_le intro!: If.IH)
-  next
-    case While from While.prems show ?case by(fastforce simp: While_le intro: While.IH)
-  qed
+  case goal2 thus ?case
+    by(auto simp: Inf_acom_def less_eq_acom_def size_annos intro:INF_greatest)
 next
-  case goal3
-  have "strip(merge c A) = c"
-  proof(induction c arbitrary: A)
-    case Seq from Seq.prems show ?case by (fastforce simp: strip_eq_Seq subset_iff intro!: Seq.IH)
-  next
-    case If from If.prems show ?case by (fastforce intro!: If.IH simp: strip_eq_If)
-  next
-    case While from While.prems show ?case by(fastforce intro: While.IH simp: strip_eq_While)
-  qed auto
-  thus ?case by auto
+  case goal3 thus ?case by(auto simp: Inf_acom_def)
 qed
 
-lemma le_post: "c \<le> d \<Longrightarrow> post c \<le> post d"
-by(induction c d rule: less_eq_acom.induct) auto
-
 
 subsubsection "Collecting semantics"
 
@@ -176,17 +119,21 @@
   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))
+proof(induction S1 C1 arbitrary: C2 S2 rule: Step.induct)
+  case 1 thus ?case by(auto)
 next
-  case 3 thus ?case by(simp add: le_post)
+  case 2 thus ?case by (auto simp: assms(1))
+next
+  case 3 thus ?case by(auto simp: mono_post)
 next
   case 4 thus ?case
-    by(simp add: subset_iff assms(2)) (metis le_post le_supI1 le_supI2)
+    by(auto simp: subset_iff assms(2))
+      (metis mono_post le_supI1 le_supI2)+
 next
   case 5 thus ?case
-    by(simp add: subset_iff assms(2)) (metis le_post le_supI1 le_supI2)
-qed auto
+    by(auto simp: subset_iff assms(2))
+      (metis mono_post le_supI1 le_supI2)+
+qed
 
 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
@@ -211,31 +158,34 @@
 
 subsubsection "Relation to big-step semantics"
 
-lemma post_merge: "\<forall> c' \<in> M. strip c' = c \<Longrightarrow> post (merge c M) = post ` M"
-proof(induction c arbitrary: M)
-  case (Seq c1 c2)
-  have "post ` M = post ` sub\<^isub>2 ` M" using Seq.prems by (force simp: strip_eq_Seq)
-  moreover have "\<forall> c' \<in> sub\<^isub>2 ` M. strip c' = c2" using Seq.prems by (auto simp: strip_eq_Seq)
-  ultimately show ?case using Seq.IH(2)[of "sub\<^isub>2 ` M"] by simp
-qed simp_all
+lemma asize_nz: "asize(c::com) \<noteq> 0"
+by (metis length_0_conv length_annos_annotate annos_ne)
 
+lemma post_Inf_acom:
+  "\<forall>C\<in>M. strip C = c \<Longrightarrow> post (Inf_acom c M) = \<Inter>(post ` M)"
+apply(subgoal_tac "\<forall>C\<in>M. size(annos C) = asize c")
+ apply(simp add: post_anno_asize Inf_acom_def asize_nz neq0_conv[symmetric])
+apply(simp add: size_annos)
+done
 
 lemma post_lfp: "post(lfp c f) = (\<Inter>{post C|C. strip C = c \<and> f C \<le> C})"
-by(auto simp add: lfp_def post_merge)
+by(auto simp add: lfp_def post_Inf_acom)
 
 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 step_def)
+  case Skip thus ?case by(auto simp: strip_eq_SKIP step_def post_def)
 next
-  case Assign thus ?case by(fastforce simp: strip_eq_Assign step_def)
+  case Assign thus ?case
+    by(fastforce simp: strip_eq_Assign step_def post_def)
 next
-  case Seq thus ?case by(fastforce simp: strip_eq_Seq step_def)
+  case Seq thus ?case
+    by(fastforce simp: strip_eq_Seq step_def post_def last_append annos_ne)
 next
-  case IfTrue thus ?case apply(auto simp: strip_eq_If step_def)
+  case IfTrue thus ?case apply(auto simp: strip_eq_If step_def post_def)
     by (metis (lifting,full_types) mem_Collect_eq set_mp)
 next
-  case IfFalse thus ?case apply(auto simp: strip_eq_If step_def)
+  case IfFalse thus ?case apply(auto simp: strip_eq_If step_def post_def)
     by (metis (lifting,full_types) mem_Collect_eq set_mp)
 next
   case (WhileTrue b s1 c' s2 s3)
@@ -243,7 +193,7 @@
     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 simp: step_def)
+    by (auto simp: step_def post_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
@@ -251,7 +201,8 @@
   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 step_def)
+  case (WhileFalse b s1 c') thus ?case
+    by (force simp: strip_eq_While step_def post_def)
 qed
 
 lemma big_step_lfp: "\<lbrakk> (c,s) \<Rightarrow> t;  s \<in> S \<rbrakk> \<Longrightarrow> t \<in> post(lfp c (step S))"
diff -r 4ea9a385ec83 -r db08e493cf44 src/HOL/IMP/Collecting1.thy
--- a/src/HOL/IMP/Collecting1.thy	Wed May 15 23:00:17 2013 +0200
+++ b/src/HOL/IMP/Collecting1.thy	Thu May 16 02:13:42 2013 +0200
@@ -25,12 +25,12 @@
 
 
 definition steps :: "state \<Rightarrow> com \<Rightarrow> nat \<Rightarrow> state set acom" where
-"steps s c n = ((step {})^^n) (step {s} (anno {} c))"
+"steps s c n = ((step {})^^n) (step {s} (annotate (\<lambda>p. {}) c))"
 
 lemma steps_approx_fix_step: assumes "step S cs = cs" and "s:S"
 shows "steps s (strip cs) n \<le> cs"
 proof-
-  let ?bot = "anno {} (strip cs)"
+  let ?bot = "annotate (\<lambda>p. {}) (strip cs)"
   have "?bot \<le> cs" by(induction cs) auto
   from step_preserves_le[OF assms(1)_ this, of "{s}"] `s:S`
   have 1: "step {s} ?bot \<le> cs" by simp
diff -r 4ea9a385ec83 -r db08e493cf44 src/HOL/IMP/Collecting_Examples.thy
--- a/src/HOL/IMP/Collecting_Examples.thy	Wed May 15 23:00:17 2013 +0200
+++ b/src/HOL/IMP/Collecting_Examples.thy	Thu May 16 02:13:42 2013 +0200
@@ -22,16 +22,16 @@
 translated into a printable format as sets of variable-state pairs, for the
 variables in the command: *}
 
-definition show_acom ::
-  "state set acom \<Rightarrow> (vname*val)set set acom" where
-"show_acom C = map_acom (\<lambda>S. (\<lambda>s. (\<lambda>x. (x, s x)) ` (vars_acom C)) ` S) C"
+definition show_acom :: "state set acom \<Rightarrow> (vname*val)set set acom" where
+"show_acom C =
+   annotate (\<lambda>p. (\<lambda>s. (\<lambda>x. (x, s x)) ` (vars_acom C)) ` anno C p) (strip C)"
 
 
 subsection "Examples"
 
 definition "c0 = WHILE Less (V ''x'') (N 3)
                 DO ''x'' ::= Plus (V ''x'') (N 2)"
-definition C0 :: "state set acom" where "C0 = anno {} c0"
+definition C0 :: "state set acom" where "C0 = annotate (%p. {}) c0"
 
 text{* Collecting semantics: *}