# HG changeset patch
# User nipkow
# Date 1326963102 -3600
# Node ID 8fbcbcf4380e76638311da76cdd9030e096af389
# Parent  75dc4beb43b37ffe4413edde3d9aca612081ce89
added termination of narrowing

diff -r 75dc4beb43b3 -r 8fbcbcf4380e src/HOL/IMP/Abs_Int1.thy
--- a/src/HOL/IMP/Abs_Int1.thy	Wed Jan 18 22:06:31 2012 +0100
+++ b/src/HOL/IMP/Abs_Int1.thy	Thu Jan 19 09:51:42 2012 +0100
@@ -258,7 +258,7 @@
 lemma domo_Top[simp]: "domo \<top> = {}"
 by(simp add: domo_def Top_st_def Top_option_def)
 
-lemma bot_acom_Dom[simp]: "\<bottom>\<^sub>c c \<in> Com X"
+lemma bot_acom_Com[simp]: "\<bottom>\<^sub>c c \<in> Com X"
 by(simp add: bot_acom_def Com_def domo_def set_annos_anno)
 
 lemma post_in_annos: "post c : set(annos c)"
diff -r 75dc4beb43b3 -r 8fbcbcf4380e src/HOL/IMP/Abs_Int2.thy
--- a/src/HOL/IMP/Abs_Int2.thy	Wed Jan 18 22:06:31 2012 +0100
+++ b/src/HOL/IMP/Abs_Int2.thy	Thu Jan 19 09:51:42 2012 +0100
@@ -131,31 +131,19 @@
 lemma narrow2_acom: "y \<sqsubseteq> x \<Longrightarrow> x \<triangle>\<^sub>c y \<sqsubseteq> x"
 by(induct y x rule: le_acom.induct) (simp_all add: narrow2)
 
-(*
-lemma strip_widen_acom:
-  "strip c' = strip (c::'a::WN acom) \<Longrightarrow>  strip (c \<nabla>\<^sub>c c') = strip c"
-by(induction "widen::'a\<Rightarrow>'a\<Rightarrow>'a" c c' rule: map2_acom.induct) simp_all
-
-lemma annos_widen_acom[simp]: "strip c1 = strip (c2::'a::WN acom) \<Longrightarrow>
-  annos(c1 \<nabla>\<^sub>c c2) = map (%(x,y).x\<nabla>y) (zip (annos c1) (annos(c2::'a::WN acom)))"
-by(induction "widen::'a\<Rightarrow>'a\<Rightarrow>'a" c1 c2 rule: map2_acom.induct)
-  (simp_all add: size_annos_same2)
-*)
 
 subsubsection "Post-fixed point computation"
 
 definition iter_widen :: "('a acom \<Rightarrow> 'a acom) \<Rightarrow> 'a acom \<Rightarrow> ('a::WN)acom option"
 where "iter_widen f = while_option (\<lambda>c. \<not> f c \<sqsubseteq> c) (\<lambda>c. c \<nabla>\<^sub>c f c)"
 
-definition
-  prefp :: "(('a::preord) \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a option" where
-"prefp f = while_option (\<lambda>x. \<not> x \<sqsubseteq> f x) f"
-
+definition iter_narrow :: "('a acom \<Rightarrow> 'a acom) \<Rightarrow> 'a acom \<Rightarrow> 'a::WN acom option"
+where "iter_narrow f = while_option (\<lambda>c. \<not> c \<sqsubseteq> c \<triangle>\<^sub>c f c) (\<lambda>c. c \<triangle>\<^sub>c f c)"
 
-definition
-  pfp_WN :: "(('a::WN)option acom \<Rightarrow> 'a option acom) \<Rightarrow> com \<Rightarrow> 'a option acom option"
-where "pfp_WN f c = (case iter_widen f (\<bottom>\<^sub>c c) of None \<Rightarrow> None
-                     | Some c' \<Rightarrow> prefp (\<lambda>c. c \<triangle>\<^sub>c f c) c')"
+definition pfp_wn ::
+  "(('a::WN)option acom \<Rightarrow> 'a option acom) \<Rightarrow> com \<Rightarrow> 'a option acom option"
+where "pfp_wn f c = (case iter_widen f (\<bottom>\<^sub>c c) of None \<Rightarrow> None
+                     | Some c' \<Rightarrow> iter_narrow f c')"
 
 lemma strip_map2_acom:
  "strip c1 = strip c2 \<Longrightarrow> strip(map2_acom f c1 c2) = strip c1"
@@ -178,51 +166,51 @@
   from strip_while[OF this] assms(2) show ?thesis by(simp add: iter_widen_def)
 qed
 
-lemma iter_down_pfp: assumes "mono f" and "f x0 \<sqsubseteq> x0" 
-and "prefp (\<lambda>c. c \<triangle>\<^sub>c f c) x0 = Some x"
-shows "f x \<sqsubseteq> x \<and> x \<sqsubseteq> x0" (is "?P x")
+lemma iter_narrow_pfp: assumes "mono f" and "f c0 \<sqsubseteq> c0"
+and "iter_narrow f c0 = Some c"
+shows "f c \<sqsubseteq> c \<and> c \<sqsubseteq> c0" (is "?P c")
 proof-
-  { fix x assume "?P x"
+  { fix c assume "?P c"
     note 1 = conjunct1[OF this] and 2 = conjunct2[OF this]
-    let ?x' = "x \<triangle>\<^sub>c f x"
-    have "?P ?x'"
+    let ?c' = "c \<triangle>\<^sub>c f c"
+    have "?P ?c'"
     proof
-      have "f ?x' \<sqsubseteq> f x"  by(rule monoD[OF `mono f` narrow2_acom[OF 1]])
-      also have "\<dots> \<sqsubseteq> ?x'" by(rule narrow1_acom[OF 1])
-      finally show "f ?x' \<sqsubseteq> ?x'" .
-      have "?x' \<sqsubseteq> x" by (rule narrow2_acom[OF 1])
-      also have "x \<sqsubseteq> x0" by(rule 2)
-      finally show "?x' \<sqsubseteq> x0" .
+      have "f ?c' \<sqsubseteq> f c"  by(rule monoD[OF `mono f` narrow2_acom[OF 1]])
+      also have "\<dots> \<sqsubseteq> ?c'" by(rule narrow1_acom[OF 1])
+      finally show "f ?c' \<sqsubseteq> ?c'" .
+      have "?c' \<sqsubseteq> c" by (rule narrow2_acom[OF 1])
+      also have "c \<sqsubseteq> c0" by(rule 2)
+      finally show "?c' \<sqsubseteq> c0" .
     qed
   }
-  with while_option_rule[where P = ?P, OF _ assms(3)[simplified prefp_def]]
+  with while_option_rule[where P = ?P, OF _ assms(3)[simplified iter_narrow_def]]
     assms(2) le_refl
   show ?thesis by blast
 qed
 
-lemma pfp_WN_pfp:
-  "\<lbrakk> mono f;  pfp_WN f c = Some c' \<rbrakk> \<Longrightarrow> f c' \<sqsubseteq> c'"
-unfolding pfp_WN_def
-by (auto dest: iter_down_pfp iter_widen_pfp split: option.splits)
+lemma pfp_wn_pfp:
+  "\<lbrakk> mono f;  pfp_wn f c = Some c' \<rbrakk> \<Longrightarrow> f c' \<sqsubseteq> c'"
+unfolding pfp_wn_def
+by (auto dest: iter_widen_pfp iter_narrow_pfp split: option.splits)
 
-lemma strip_pfp_WN:
-  "\<lbrakk> \<forall>c. strip(f c) = strip c; pfp_WN f c = Some c' \<rbrakk> \<Longrightarrow> strip c' = c"
-apply(auto simp add: pfp_WN_def prefp_def split: option.splits)
+lemma strip_pfp_wn:
+  "\<lbrakk> \<forall>c. strip(f c) = strip c; pfp_wn f c = Some c' \<rbrakk> \<Longrightarrow> strip c' = c"
+apply(auto simp add: pfp_wn_def iter_narrow_def split: option.splits)
 by (metis (no_types) strip_map2_acom strip_while strip_bot_acom strip_iter_widen)
 
 locale Abs_Int2 = Abs_Int1_mono
 where \<gamma>=\<gamma> for \<gamma> :: "'av::{WN,L_top_bot} \<Rightarrow> val set"
 begin
 
-definition AI_WN :: "com \<Rightarrow> 'av st option acom option" where
-"AI_WN = pfp_WN (step' \<top>)"
+definition AI_wn :: "com \<Rightarrow> 'av st option acom option" where
+"AI_wn = pfp_wn (step' \<top>)"
 
-lemma AI_WN_sound: "AI_WN c = Some c' \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c c'"
-proof(simp add: CS_def AI_WN_def)
-  assume 1: "pfp_WN (step' \<top>) c = Some c'"
-  from pfp_WN_pfp[OF mono_step'2 1]
+lemma AI_wn_sound: "AI_wn c = Some c' \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c c'"
+proof(simp add: CS_def AI_wn_def)
+  assume 1: "pfp_wn (step' \<top>) c = Some c'"
+  from pfp_wn_pfp[OF mono_step'2 1]
   have 2: "step' \<top> c' \<sqsubseteq> c'" .
-  have 3: "strip (\<gamma>\<^isub>c (step' \<top> c')) = c" by(simp add: strip_pfp_WN[OF _ 1])
+  have 3: "strip (\<gamma>\<^isub>c (step' \<top> c')) = c" by(simp add: strip_pfp_wn[OF _ 1])
   have "lfp (step UNIV) c \<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')"
@@ -240,7 +228,7 @@
 interpretation Abs_Int2
 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
 and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
-defines AI_ivl' is AI_WN
+defines AI_ivl' is AI_wn
 proof qed
 
 
@@ -271,40 +259,6 @@
 
 subsubsection "Termination: Intervals"
 
-(* interesting(?) relic
-lemma widen_assoc:
-  "~ (y::ivl) \<sqsubseteq> x \<Longrightarrow> ~ z \<sqsubseteq> x \<nabla> y \<Longrightarrow> ((x::ivl) \<nabla> y) \<nabla> z = x \<nabla> (y \<nabla> z)"
-apply(cases x)
-apply(cases y)
-apply(cases z)
-apply(rename_tac x1 x2 y1 y2 z1 z2)
-apply(simp add: le_ivl_def)
-apply(case_tac x1)
-apply(case_tac x2)
-apply(simp add:le_option_def widen_ivl_def split: if_splits option.splits)
-apply(simp add:le_option_def widen_ivl_def split: if_splits option.splits)
-apply(case_tac x2)
-apply(simp add:le_option_def widen_ivl_def split: if_splits option.splits)
-apply(case_tac y1)
-apply(case_tac y2)
-apply(simp add:le_option_def widen_ivl_def split: if_splits option.splits)
-apply(case_tac z1)
-apply(auto simp add:le_option_def widen_ivl_def split: if_splits option.splits ivl.splits)[1]
-apply(auto simp add:le_option_def widen_ivl_def split: if_splits option.splits ivl.splits)[1]
-apply(case_tac y2)
-apply(auto simp add:le_option_def widen_ivl_def split: if_splits option.splits ivl.splits)[1]
-apply(case_tac z1)
-apply(auto simp add:le_option_def widen_ivl_def split: if_splits ivl.splits option.splits)[1]
-apply(case_tac z2)
-apply(auto simp add:le_option_def widen_ivl_def split: if_splits option.splits)[1]
-apply(auto simp add:le_option_def widen_ivl_def split: if_splits option.splits)[1]
-done
-
-lemma widen_step_trans:
-  "~ (y::ivl) \<sqsubseteq> x \<Longrightarrow> ~ z \<sqsubseteq> x \<nabla> y \<Longrightarrow> EX u. (x \<nabla> y) \<nabla> z = x \<nabla> u \<and> ~ u \<sqsubseteq> x"
-by (metis widen_assoc preord_class.le_trans widen1)
-*)
-
 definition m_ivl :: "ivl \<Rightarrow> nat" where
 "m_ivl ivl = (case ivl of I l h \<Rightarrow>
      (case l of None \<Rightarrow> 0 | Some _ \<Rightarrow> 1) + (case h of None \<Rightarrow> 0 | Some _ \<Rightarrow> 1))"
@@ -316,7 +270,7 @@
 by(auto simp: m_ivl_def le_option_def le_ivl_def
         split: ivl.split option.split if_splits)
 
-lemma less_m_ivl_widen:
+lemma m_ivl_widen:
   "~ y \<sqsubseteq> x \<Longrightarrow> m_ivl(x \<nabla> y) < m_ivl x"
 by(auto simp: m_ivl_def widen_ivl_def le_option_def le_ivl_def
         split: ivl.splits option.splits if_splits)
@@ -326,6 +280,18 @@
         split: ivl.split option.split if_splits)
 
 
+definition n_ivl :: "ivl \<Rightarrow> nat" where
+"n_ivl ivl = 2 - m_ivl ivl"
+
+lemma n_ivl_mono: "(x::ivl) \<sqsubseteq> y \<Longrightarrow> n_ivl x \<le> n_ivl y"
+unfolding n_ivl_def by (metis diff_le_mono2 m_ivl_anti_mono)
+
+lemma n_ivl_narrow:
+  "~ x \<sqsubseteq> x \<triangle> y \<Longrightarrow> n_ivl(x \<triangle> y) < n_ivl x"
+by(auto simp: n_ivl_def m_ivl_def narrow_ivl_def le_option_def le_ivl_def
+        split: ivl.splits option.splits if_splits)
+
+
 subsubsection "Termination: Abstract State"
 
 definition "m_st m st = (\<Sum>x\<in>set(dom st). m(fun st x))"
@@ -363,7 +329,7 @@
     by (metis add_less_cancel_left)
 qed
 
-lemma less_m_st_widen:
+lemma m_st_widen:
 assumes "\<not> S2 \<sqsubseteq> S1" shows "m_st m_ivl (S1 \<nabla> S2) < m_st m_ivl S1"
 proof-
   { let ?X = "set(dom S1)" let ?Y = "set(dom S2)"
@@ -379,7 +345,7 @@
       next
         show "\<exists>x\<in>?X\<inter>?Y. m_ivl(?f x \<nabla> ?g x) < m_ivl(?f x)"
           using `x:?X` `x:?Y` `\<not> lookup S2 x \<sqsubseteq> ?f x`
-          by (metis IntI less_m_ivl_widen lookup_def)
+          by (metis IntI m_ivl_widen lookup_def)
       qed
       also have "\<dots> \<le> ?R" by(simp add: setsum_mono3[OF _ Int_lower1])
       finally show ?thesis .
@@ -391,7 +357,7 @@
           by (metis m_ivl_anti_mono widen1)
       qed
       also have "\<dots> < m_ivl(?f x) + \<dots>"
-        using less_m_ivl_widen[OF `\<not> lookup S2 x \<sqsubseteq> ?f x`]
+        using m_ivl_widen[OF `\<not> lookup S2 x \<sqsubseteq> ?f x`]
         by (metis Nat.le_refl add_strict_increasing gr0I not_less0)
       also have "\<dots> = (\<Sum>y\<in>insert x (?X\<inter>?Y). m_ivl(?f y))"
         using `x ~: ?Y` by simp
@@ -403,6 +369,35 @@
     by(auto simp: le_st_def widen_st_def m_st_def Int_def)
 qed
 
+definition "n_st m X st = (\<Sum>x\<in>X. m(lookup st x))"
+
+lemma n_st_mono: assumes "set(dom S1) \<subseteq> X" "set(dom S2) \<subseteq> X" "S1 \<sqsubseteq> S2"
+shows "n_st n_ivl X S1 \<le> n_st n_ivl X S2"
+proof-
+  have "(\<Sum>x\<in>X. n_ivl(lookup S1 x)) \<le> (\<Sum>x\<in>X. n_ivl(lookup S2 x))"
+    apply(rule setsum_mono) using assms
+    by(auto simp: le_st_def lookup_def n_ivl_mono split: if_splits)
+  thus ?thesis by(simp add: n_st_def)
+qed
+
+lemma n_st_narrow:
+assumes "finite X" and "set(dom S1) \<subseteq> X" "set(dom S2) \<subseteq> X"
+and "S2 \<sqsubseteq> S1" "\<not> S1 \<sqsubseteq> S1 \<triangle> S2"
+shows "n_st n_ivl X (S1 \<triangle> S2) < n_st n_ivl X S1"
+proof-
+  have 1: "\<forall>x\<in>X. n_ivl (lookup (S1 \<triangle> S2) x) \<le> n_ivl (lookup S1 x)"
+    using assms(2-4)
+    by(auto simp: le_st_def narrow_st_def lookup_def n_ivl_mono narrow2
+            split: if_splits)
+  have 2: "\<exists>x\<in>X. n_ivl (lookup (S1 \<triangle> S2) x) < n_ivl (lookup S1 x)"
+    using assms(2-5)
+    by(auto simp: le_st_def narrow_st_def lookup_def intro: n_ivl_narrow
+            split: if_splits)
+  have "(\<Sum>x\<in>X. n_ivl(lookup (S1 \<triangle> S2) x)) < (\<Sum>x\<in>X. n_ivl(lookup S1 x))"
+    apply(rule setsum_strict_mono1[OF `finite X`]) using 1 2 by blast+
+  thus ?thesis by(simp add: n_st_def)
+qed
+
 
 subsubsection "Termination: Option"
 
@@ -415,35 +410,63 @@
            split: option.splits)
 done
 
-lemma less_m_o_widen: "\<lbrakk> finite X; domo S2 \<subseteq> X; \<not> S2 \<sqsubseteq> S1 \<rbrakk> \<Longrightarrow>
+lemma m_o_widen: "\<lbrakk> finite X; domo S2 \<subseteq> X; \<not> S2 \<sqsubseteq> S1 \<rbrakk> \<Longrightarrow>
   m_o (m_st m_ivl) (2 * card X) (S1 \<nabla> S2) < m_o (m_st m_ivl) (2 * card X) S1"
-by(auto simp: m_o_def domo_def m_st_height less_Suc_eq_le less_m_st_widen
+by(auto simp: m_o_def domo_def m_st_height less_Suc_eq_le m_st_widen
         split: option.split)
 
+definition "n_o n opt = (case opt of None \<Rightarrow> 0 | Some x \<Rightarrow> n x + 1)"
+
+lemma n_o_mono: "domo S1 \<subseteq> X \<Longrightarrow> domo S2 \<subseteq> X \<Longrightarrow> S1 \<sqsubseteq> S2 \<Longrightarrow>
+  n_o (n_st n_ivl X) S1 \<le> n_o (n_st n_ivl X) S2"
+apply(induction S1 S2 rule: le_option.induct)
+apply(auto simp: domo_def n_o_def n_st_mono
+           split: option.splits)
+done
+
+lemma n_o_narrow:
+  "\<lbrakk> finite X; domo S1 \<subseteq> X; domo S2 \<subseteq> X; S2 \<sqsubseteq> S1; \<not> S1 \<sqsubseteq> S1 \<triangle> S2 \<rbrakk>
+  \<Longrightarrow> n_o (n_st n_ivl X) (S1 \<triangle> S2) < n_o (n_st n_ivl X) S1"
+apply(induction S1 S2 rule: narrow_option.induct)
+apply(auto simp: n_o_def domo_def n_st_narrow)
+done
 
 lemma domo_widen_subset: "domo (S1 \<nabla> S2) \<subseteq> domo S1 \<union> domo S2"
 apply(induction S1 S2 rule: widen_option.induct)
 apply (auto simp: domo_def widen_st_def)
 done
 
+lemma domo_narrow_subset: "domo (S1 \<triangle> S2) \<subseteq> domo S1 \<union> domo S2"
+apply(induction S1 S2 rule: narrow_option.induct)
+apply (auto simp: domo_def narrow_st_def)
+done
+
 subsubsection "Termination: Commands"
 
-lemma strip_widen_acom:
+lemma strip_widen_acom[simp]:
   "strip c' = strip (c::'a::WN acom) \<Longrightarrow>  strip (c \<nabla>\<^sub>c c') = strip c"
 by(induction "widen::'a\<Rightarrow>'a\<Rightarrow>'a" c c' rule: map2_acom.induct) simp_all
 
+lemma strip_narrow_acom[simp]:
+  "strip c' = strip (c::'a::WN acom) \<Longrightarrow>  strip (c \<triangle>\<^sub>c c') = strip c"
+by(induction "narrow::'a\<Rightarrow>'a\<Rightarrow>'a" c c' rule: map2_acom.induct) simp_all
+
 lemma annos_widen_acom[simp]: "strip c1 = strip (c2::'a::WN acom) \<Longrightarrow>
   annos(c1 \<nabla>\<^sub>c c2) = map (%(x,y).x\<nabla>y) (zip (annos c1) (annos(c2::'a::WN acom)))"
 by(induction "widen::'a\<Rightarrow>'a\<Rightarrow>'a" c1 c2 rule: map2_acom.induct)
   (simp_all add: size_annos_same2)
 
-lemma Com_widen_acom: "strip c2 = strip c1 \<Longrightarrow>
+lemma annos_narrow_acom[simp]: "strip c1 = strip (c2::'a::WN acom) \<Longrightarrow>
+  annos(c1 \<triangle>\<^sub>c c2) = map (%(x,y).x\<triangle>y) (zip (annos c1) (annos(c2::'a::WN acom)))"
+by(induction "narrow::'a\<Rightarrow>'a\<Rightarrow>'a" c1 c2 rule: map2_acom.induct)
+  (simp_all add: size_annos_same2)
+
+lemma widen_acom_Com[simp]: "strip c2 = strip c1 \<Longrightarrow>
   c1 : Com X \<Longrightarrow> c2 : Com X \<Longrightarrow> (c1 \<nabla>\<^sub>c c2) : Com X"
-apply(auto simp add: Com_def split: option.splits)
+apply(auto simp add: Com_def)
 apply(rename_tac S S' x)
 apply(erule in_set_zipE)
-apply(simp add: domo_def)
-apply (auto split: option.splits)
+apply(auto simp: domo_def split: option.splits)
 apply(case_tac S)
 apply(case_tac S')
 apply simp
@@ -453,6 +476,21 @@
 apply (fastforce simp: widen_st_def)
 done
 
+lemma narrow_acom_Com[simp]: "strip c2 = strip c1 \<Longrightarrow>
+  c1 : Com X \<Longrightarrow> c2 : Com X \<Longrightarrow> (c1 \<triangle>\<^sub>c c2) : Com X"
+apply(auto simp add: Com_def)
+apply(rename_tac S S' x)
+apply(erule in_set_zipE)
+apply(auto simp: domo_def split: option.splits)
+apply(case_tac S)
+apply(case_tac S')
+apply simp
+apply fastforce
+apply(case_tac S')
+apply fastforce
+apply (fastforce simp: narrow_st_def)
+done
+
 definition "m_c m c = (let as = annos c in \<Sum>i=0..<size as. m(as!i))"
 
 lemma measure_m_c: "finite X \<Longrightarrow> {(c, c \<nabla>\<^sub>c c') |c c'\<Colon>ivl st option acom.
@@ -467,12 +505,34 @@
 apply (clarsimp)
 apply(erule m_o_anti_mono)
 apply(rule subset_trans[OF domo_widen_subset])
-apply fastsimp
+apply fastforce
 apply(rule widen1)
 apply(auto simp: le_iff_le_annos listrel_iff_nth)
 apply(rule_tac x=n in bexI)
 prefer 2 apply simp
-apply(erule less_m_o_widen)
+apply(erule m_o_widen)
+apply (simp)+
+done
+
+lemma measure_n_c: "finite X \<Longrightarrow> {(c, c \<triangle>\<^sub>c c') |c c'.
+  strip c = strip c' \<and> c \<in> Com X \<and> c' \<in> Com X \<and> c' \<sqsubseteq> c \<and> \<not> c \<sqsubseteq> c \<triangle>\<^sub>c c'}\<inverse>
+  \<subseteq> measure(m_c(n_o (n_st n_ivl X)))"
+apply(auto simp: m_c_def Let_def Com_def)
+apply(subgoal_tac "length(annos c') = length(annos c)")
+prefer 2 apply (simp add: size_annos_same2)
+apply (auto)
+apply(rule setsum_strict_mono1)
+apply simp
+apply (clarsimp)
+apply(rule n_o_mono)
+using domo_narrow_subset apply fastforce
+apply fastforce
+apply(rule narrow2)
+apply(fastforce simp: le_iff_le_annos listrel_iff_nth)
+apply(auto simp: le_iff_le_annos listrel_iff_nth strip_narrow_acom)
+apply(rule_tac x=n in bexI)
+prefer 2 apply simp
+apply(erule n_o_narrow)
 apply (simp)+
 done
 
@@ -494,11 +554,24 @@
   fix c assume "P c" thus "P (c \<nabla>\<^sub>c f c)" by(simp add: P_f P_widen)
 qed
 
-lemma
-  "EX c::ivl st option acom. iter_widen (step_ivl \<top>) (\<bottom>\<^sub>c c0) = Some c"
+lemma iter_narrow_termination:
+assumes P_f: "\<And>c. P c \<Longrightarrow> P(c \<triangle>\<^sub>c f c)"
+and wf: "wf({(c, c \<triangle>\<^sub>c f c)|c c'. P c \<and> ~ c \<sqsubseteq> c \<triangle>\<^sub>c f c}^-1)"
+and "P c0" shows "EX c. iter_narrow f c0 = Some c"
+proof(simp add: iter_narrow_def, rule wf_while_option_Some[where P = "P"])
+  show "wf {(c', c). (P c \<and> \<not> c \<sqsubseteq> c \<triangle>\<^sub>c f c) \<and> c' = c \<triangle>\<^sub>c f c}"
+    apply(rule wf_subset[OF wf]) by(blast intro: P_f)
+next
+  show "P c0" by(rule `P c0`)
+next
+  fix c assume "P c" thus "P (c \<triangle>\<^sub>c f c)" by(simp add: P_f)
+qed
+
+lemma iter_winden_step_ivl_termination:
+  "EX c. iter_widen (step_ivl \<top>) (\<bottom>\<^sub>c c0) = Some c"
 apply(rule iter_widen_termination[where
   P = "%c. strip c = c0 \<and> c : Com(vars c0)"])
-apply (simp_all add: strip_step' step'_Com Com_widen_acom strip_widen_acom bot_acom domo_Top)
+apply (simp_all add: step'_Com bot_acom)
 apply(rule wf_subset)
 apply(rule wf_measure)
 apply(rule subset_trans)
@@ -507,4 +580,98 @@
 apply blast
 done
 
+lemma iter_narrow_step_ivl_termination:
+  "c0 \<in> Com (vars(strip c0)) \<Longrightarrow> step_ivl \<top> c0 \<sqsubseteq> c0 \<Longrightarrow>
+  EX c. iter_narrow (step_ivl \<top>) c0 = Some c"
+apply(rule iter_narrow_termination[where
+  P = "%c. strip c = strip c0 \<and> c : Com(vars(strip c0)) \<and> step_ivl \<top> c \<sqsubseteq> c"])
+apply (simp_all add: step'_Com)
+apply(clarify)
+apply(frule narrow2_acom, drule mono_step'[OF le_refl], erule le_trans[OF _ narrow1_acom])
+apply assumption
+apply(rule wf_subset)
+apply(rule wf_measure)
+apply(rule subset_trans)
+prefer 2
+apply(rule measure_n_c[where X = "vars(strip c0)", OF finite_cvars])
+apply auto
+by (metis bot_least domo_Top order_refl step'_Com strip_step')
+
+(* FIXME: simplify type system: Combine Com(X) and vars <= X?? *)
+lemma while_Com:
+fixes c :: "'a st option acom"
+assumes "while_option P f c = Some c'"
+and "!!c. strip(f c) = strip c"
+and "\<forall>c::'a st option acom. c : Com(X) \<longrightarrow> vars(strip c) \<subseteq> X \<longrightarrow> f c : Com(X)"
+and "c : Com(X)" and "vars(strip c) \<subseteq> X" shows "c' : Com(X)"
+using while_option_rule[where P = "\<lambda>c'. c' : Com(X) \<and> vars(strip c') \<subseteq> X", OF _ assms(1)]
+by(simp add: assms(2-))
+
+lemma iter_widen_Com: fixes f :: "'a::WN st option acom \<Rightarrow> 'a st option acom"
+assumes "iter_widen f c = Some c'"
+and "\<forall>c. c : Com(X) \<longrightarrow> vars(strip c) \<subseteq> X \<longrightarrow> f c : Com(X)"
+and "!!c. strip(f c) = strip c"
+and "c : Com(X)" and "vars (strip c) \<subseteq> X" shows "c' : Com(X)"
+proof-
+  have "\<forall>c. c : Com(X) \<longrightarrow> vars(strip c) \<subseteq> X \<longrightarrow> c \<nabla>\<^sub>c f c : Com(X)"
+    by (metis (full_types) widen_acom_Com assms(2,3))
+  from while_Com[OF assms(1)[simplified iter_widen_def] _ this assms(4,5)]
+  show ?thesis using assms(3) by(simp)
+qed
+
+(* step' = step_ivl! mv into locale*)
+lemma iter_widen_step'_Com:
+  "iter_widen (step' \<top>) c = Some c' \<Longrightarrow> vars(strip c) \<subseteq> X \<Longrightarrow> c : Com(X)
+   \<Longrightarrow> c' : Com(X)"
+apply(subgoal_tac "strip c'= strip c")
+prefer 2 apply (metis strip_iter_widen strip_step')
+apply(drule iter_widen_Com)
+prefer 3 apply assumption
+prefer 3 apply assumption
+apply (auto simp: step'_Com)
+done
+
+theorem step_ivl_termination:
+  "EX c. AI_ivl' c0 = Some c"
+apply(auto simp: AI_wn_def pfp_wn_def iter_winden_step_ivl_termination split: option.split)
+apply(rule iter_narrow_step_ivl_termination)
+apply (metis bot_acom_Com iter_widen_step'_Com[OF _ subset_refl] strip_iter_widen strip_step')
+apply(erule iter_widen_pfp)
+done
+
 end
+
+
+(* interesting(?) relic
+lemma widen_assoc:
+  "~ (y::ivl) \<sqsubseteq> x \<Longrightarrow> ~ z \<sqsubseteq> x \<nabla> y \<Longrightarrow> ((x::ivl) \<nabla> y) \<nabla> z = x \<nabla> (y \<nabla> z)"
+apply(cases x)
+apply(cases y)
+apply(cases z)
+apply(rename_tac x1 x2 y1 y2 z1 z2)
+apply(simp add: le_ivl_def)
+apply(case_tac x1)
+apply(case_tac x2)
+apply(simp add:le_option_def widen_ivl_def split: if_splits option.splits)
+apply(simp add:le_option_def widen_ivl_def split: if_splits option.splits)
+apply(case_tac x2)
+apply(simp add:le_option_def widen_ivl_def split: if_splits option.splits)
+apply(case_tac y1)
+apply(case_tac y2)
+apply(simp add:le_option_def widen_ivl_def split: if_splits option.splits)
+apply(case_tac z1)
+apply(auto simp add:le_option_def widen_ivl_def split: if_splits option.splits ivl.splits)[1]
+apply(auto simp add:le_option_def widen_ivl_def split: if_splits option.splits ivl.splits)[1]
+apply(case_tac y2)
+apply(auto simp add:le_option_def widen_ivl_def split: if_splits option.splits ivl.splits)[1]
+apply(case_tac z1)
+apply(auto simp add:le_option_def widen_ivl_def split: if_splits ivl.splits option.splits)[1]
+apply(case_tac z2)
+apply(auto simp add:le_option_def widen_ivl_def split: if_splits option.splits)[1]
+apply(auto simp add:le_option_def widen_ivl_def split: if_splits option.splits)[1]
+done
+
+lemma widen_step_trans:
+  "~ (y::ivl) \<sqsubseteq> x \<Longrightarrow> ~ z \<sqsubseteq> x \<nabla> y \<Longrightarrow> EX u. (x \<nabla> y) \<nabla> z = x \<nabla> u \<and> ~ u \<sqsubseteq> x"
+by (metis widen_assoc preord_class.le_trans widen1)
+*)