--- 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)"
--- 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)
+*)