Theory Abs_Int3
section "Widening and Narrowing"
theory Abs_Int3
imports Abs_Int2_ivl
begin
class WN = SL_top +
fixes widen :: "'a ⇒ 'a ⇒ 'a" (infix "∇" 65)
assumes widen1: "x ⊑ x ∇ y"
assumes widen2: "y ⊑ x ∇ y"
fixes narrow :: "'a ⇒ 'a ⇒ 'a" (infix "△" 65)
assumes narrow1: "y ⊑ x ⟹ y ⊑ x △ y"
assumes narrow2: "y ⊑ x ⟹ x △ y ⊑ x"
subsection "Intervals"
instantiation ivl :: WN
begin
definition "widen_ivl ivl1 ivl2 =
(
case (ivl1,ivl2) of (I l1 h1, I l2 h2) ⇒
I (if le_option False l2 l1 ∧ l2 ≠ l1 then None else l1)
(if le_option True h1 h2 ∧ h1 ≠ h2 then None else h1))"
definition "narrow_ivl ivl1 ivl2 =
(
case (ivl1,ivl2) of (I l1 h1, I l2 h2) ⇒
I (if l1 = None then l2 else l1)
(if h1 = None then h2 else h1))"
instance
proof qed
(auto simp add: widen_ivl_def narrow_ivl_def le_option_def le_ivl_def empty_def split: ivl.split option.split if_splits)
end
subsection "Abstract State"
instantiation st :: (WN)WN
begin
definition "widen_st F1 F2 =
FunDom (λx. fun F1 x ∇ fun F2 x) (inter_list (dom F1) (dom F2))"
definition "narrow_st F1 F2 =
FunDom (λx. fun F1 x △ fun F2 x) (inter_list (dom F1) (dom F2))"
instance
proof (standard, goal_cases)
case 1 thus ?case
by(simp add: widen_st_def le_st_def lookup_def widen1)
next
case 2 thus ?case
by(simp add: widen_st_def le_st_def lookup_def widen2)
next
case 3 thus ?case
by(auto simp: narrow_st_def le_st_def lookup_def narrow1)
next
case 4 thus ?case
by(auto simp: narrow_st_def le_st_def lookup_def narrow2)
qed
end
subsection "Option"
instantiation option :: (WN)WN
begin
fun widen_option where
"None ∇ x = x" |
"x ∇ None = x" |
"(Some x) ∇ (Some y) = Some(x ∇ y)"
fun narrow_option where
"None △ x = None" |
"x △ None = None" |
"(Some x) △ (Some y) = Some(x △ y)"
instance
proof (standard, goal_cases)
case (1 x y) show ?case
by(induct x y rule: widen_option.induct) (simp_all add: widen1)
next
case (2 x y) show ?case
by(induct x y rule: widen_option.induct) (simp_all add: widen2)
next
case (3 x y) thus ?case
by(induct x y rule: narrow_option.induct) (simp_all add: narrow1)
next
case (4 y x) thus ?case
by(induct x y rule: narrow_option.induct) (simp_all add: narrow2)
qed
end
subsection "Annotated commands"
fun map2_acom :: "('a ⇒ 'a ⇒ 'a) ⇒ 'a acom ⇒ 'a acom ⇒ 'a acom" where
"map2_acom f (SKIP {a1}) (SKIP {a2}) = (SKIP {f a1 a2})" |
"map2_acom f (x ::= e {a1}) (x' ::= e' {a2}) = (x ::= e {f a1 a2})" |
"map2_acom f (c1;;c2) (c1';;c2') = (map2_acom f c1 c1';; map2_acom f c2 c2')" |
"map2_acom f (IF b THEN c1 ELSE c2 {a1}) (IF b' THEN c1' ELSE c2' {a2}) =
(IF b THEN map2_acom f c1 c1' ELSE map2_acom f c2 c2' {f a1 a2})" |
"map2_acom f ({a1} WHILE b DO c {a2}) ({a3} WHILE b' DO c' {a4}) =
({f a1 a3} WHILE b DO map2_acom f c c' {f a2 a4})"
abbreviation widen_acom :: "('a::WN)acom ⇒ 'a acom ⇒ 'a acom" (infix "∇⇩c" 65)
where "widen_acom == map2_acom (∇)"
abbreviation narrow_acom :: "('a::WN)acom ⇒ 'a acom ⇒ 'a acom" (infix "△⇩c" 65)
where "narrow_acom == map2_acom (△)"
lemma widen1_acom: "strip c = strip c' ⟹ c ⊑ c ∇⇩c c'"
by(induct c c' rule: le_acom.induct)(simp_all add: widen1)
lemma widen2_acom: "strip c = strip c' ⟹ c' ⊑ c ∇⇩c c'"
by(induct c c' rule: le_acom.induct)(simp_all add: widen2)
lemma narrow1_acom: "y ⊑ x ⟹ y ⊑ x △⇩c y"
by(induct y x rule: le_acom.induct) (simp_all add: narrow1)
lemma narrow2_acom: "y ⊑ x ⟹ x △⇩c y ⊑ x"
by(induct y x rule: le_acom.induct) (simp_all add: narrow2)
subsection "Post-fixed point computation"
definition iter_widen :: "('a acom ⇒ 'a acom) ⇒ 'a acom ⇒ ('a::WN)acom option"
where "iter_widen f = while_option (λc. ¬ f c ⊑ c) (λc. c ∇⇩c f c)"
definition iter_narrow :: "('a acom ⇒ 'a acom) ⇒ 'a acom ⇒ 'a::WN acom option"
where "iter_narrow f = while_option (λc. ¬ c ⊑ c △⇩c f c) (λc. c △⇩c f c)"
definition pfp_wn ::
"(('a::WN)option acom ⇒ 'a option acom) ⇒ com ⇒ 'a option acom option"
where "pfp_wn f c = (case iter_widen f (⊥⇩c c) of None ⇒ None
| Some c' ⇒ iter_narrow f c')"
lemma strip_map2_acom:
"strip c1 = strip c2 ⟹ strip(map2_acom f c1 c2) = strip c1"
by(induct f c1 c2 rule: map2_acom.induct) simp_all
lemma iter_widen_pfp: "iter_widen f c = Some c' ⟹ f c' ⊑ c'"
by(auto simp add: iter_widen_def dest: while_option_stop)
lemma strip_while: fixes f :: "'a acom ⇒ 'a acom"
assumes "∀c. strip (f c) = strip c" and "while_option P f c = Some c'"
shows "strip c' = strip c"
using while_option_rule[where P = "λc'. strip c' = strip c", OF _ assms(2)]
by (metis assms(1))
lemma strip_iter_widen: fixes f :: "'a::WN acom ⇒ 'a acom"
assumes "∀c. strip (f c) = strip c" and "iter_widen f c = Some c'"
shows "strip c' = strip c"
proof-
have "∀c. strip(c ∇⇩c f c) = strip c" by (metis assms(1) strip_map2_acom)
from strip_while[OF this] assms(2) show ?thesis by(simp add: iter_widen_def)
qed
lemma iter_narrow_pfp: assumes "mono f" and "f c0 ⊑ c0"
and "iter_narrow f c0 = Some c"
shows "f c ⊑ c ∧ c ⊑ c0" (is "?P c")
proof-
{ fix c assume "?P c"
note 1 = conjunct1[OF this] and 2 = conjunct2[OF this]
let ?c' = "c △⇩c f c"
have "?P ?c'"
proof
have "f ?c' ⊑ f c" by(rule monoD[OF ‹mono f› narrow2_acom[OF 1]])
also have "… ⊑ ?c'" by(rule narrow1_acom[OF 1])
finally show "f ?c' ⊑ ?c'" .
have "?c' ⊑ c" by (rule narrow2_acom[OF 1])
also have "c ⊑ c0" by(rule 2)
finally show "?c' ⊑ c0" .
qed
}
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:
"⟦ mono f; pfp_wn f c = Some c' ⟧ ⟹ f c' ⊑ c'"
unfolding pfp_wn_def
by (auto dest: iter_widen_pfp iter_narrow_pfp split: option.splits)
lemma strip_pfp_wn:
"⟦ ∀c. strip(f c) = strip c; pfp_wn f c = Some c' ⟧ ⟹ strip c' = c"
apply(auto simp add: pfp_wn_def iter_narrow_def split: option.splits)
by (metis (mono_tags) strip_map2_acom strip_while strip_bot_acom strip_iter_widen)
locale Abs_Int2 = Abs_Int1_mono
where γ=γ for γ :: "'av::{WN,L_top_bot} ⇒ val set"
begin
definition AI_wn :: "com ⇒ 'av st option acom option" where
"AI_wn = pfp_wn (step' ⊤)"
lemma AI_wn_sound: "AI_wn c = Some c' ⟹ CS c ≤ γ⇩c c'"
proof(simp add: CS_def AI_wn_def)
assume 1: "pfp_wn (step' ⊤) c = Some c'"
from pfp_wn_pfp[OF mono_step'2 1]
have 2: "step' ⊤ c' ⊑ c'" .
have 3: "strip (γ⇩c (step' ⊤ c')) = c" by(simp add: strip_pfp_wn[OF _ 1])
have "lfp (step UNIV) c ≤ γ⇩c (step' ⊤ c')"
proof(rule lfp_lowerbound[simplified,OF 3])
show "step UNIV (γ⇩c (step' ⊤ c')) ≤ γ⇩c (step' ⊤ c')"
proof(rule step_preserves_le[OF _ _])
show "UNIV ⊆ γ⇩o ⊤" by simp
show "γ⇩c (step' ⊤ c') ≤ γ⇩c c'" by(rule mono_gamma_c[OF 2])
qed
qed
from this 2 show "lfp (step UNIV) c ≤ γ⇩c c'"
by (blast intro: mono_gamma_c order_trans)
qed
end
global_interpretation Abs_Int2
where γ = γ_ivl and num' = num_ivl and plus' = plus_ivl
and test_num' = in_ivl
and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
defines AI_ivl' = AI_wn
..
subsection "Tests"
definition "step_up_ivl n = ((λc. c ∇⇩c step_ivl ⊤ c)^^n)"
definition "step_down_ivl n = ((λc. c △⇩c step_ivl ⊤ c)^^n)"
text‹For @{const test3_ivl}, @{const AI_ivl} needed as many iterations as
the loop took to execute. In contrast, @{const AI_ivl'} converges in a
constant number of steps:›
value "show_acom (step_up_ivl 1 (⊥⇩c test3_ivl))"
value "show_acom (step_up_ivl 2 (⊥⇩c test3_ivl))"
value "show_acom (step_up_ivl 3 (⊥⇩c test3_ivl))"
value "show_acom (step_up_ivl 4 (⊥⇩c test3_ivl))"
value "show_acom (step_up_ivl 5 (⊥⇩c test3_ivl))"
value "show_acom (step_down_ivl 1 (step_up_ivl 5 (⊥⇩c test3_ivl)))"
value "show_acom (step_down_ivl 2 (step_up_ivl 5 (⊥⇩c test3_ivl)))"
value "show_acom (step_down_ivl 3 (step_up_ivl 5 (⊥⇩c test3_ivl)))"
text‹Now all the analyses terminate:›
value "show_acom_opt (AI_ivl' test4_ivl)"
value "show_acom_opt (AI_ivl' test5_ivl)"
value "show_acom_opt (AI_ivl' test6_ivl)"
subsection "Termination: Intervals"
definition m_ivl :: "ivl ⇒ nat" where
"m_ivl ivl = (case ivl of I l h ⇒
(case l of None ⇒ 0 | Some _ ⇒ 1) + (case h of None ⇒ 0 | Some _ ⇒ 1))"
lemma m_ivl_height: "m_ivl ivl ≤ 2"
by(simp add: m_ivl_def split: ivl.split option.split)
lemma m_ivl_anti_mono: "(y::ivl) ⊑ x ⟹ m_ivl x ≤ m_ivl y"
by(auto simp: m_ivl_def le_option_def le_ivl_def
split: ivl.split option.split if_splits)
lemma m_ivl_widen:
"~ y ⊑ x ⟹ m_ivl(x ∇ 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)
lemma Top_less_ivl: "⊤ ⊑ x ⟹ m_ivl x = 0"
by(auto simp: m_ivl_def le_option_def le_ivl_def empty_def Top_ivl_def
split: ivl.split option.split if_splits)
definition n_ivl :: "ivl ⇒ nat" where
"n_ivl ivl = 2 - m_ivl ivl"
lemma n_ivl_mono: "(x::ivl) ⊑ y ⟹ n_ivl x ≤ n_ivl y"
unfolding n_ivl_def by (metis diff_le_mono2 m_ivl_anti_mono)
lemma n_ivl_narrow:
"~ x ⊑ x △ y ⟹ n_ivl(x △ 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)
subsection "Termination: Abstract State"
definition "m_st m st = (∑x∈set(dom st). m(fun st x))"
lemma m_st_height: assumes "finite X" and "set (dom S) ⊆ X"
shows "m_st m_ivl S ≤ 2 * card X"
proof(auto simp: m_st_def)
have "(∑x∈set(dom S). m_ivl (fun S x)) ≤ (∑x∈set(dom S). 2)" (is "?L ≤ _")
by(rule sum_mono)(simp add:m_ivl_height)
also have "… ≤ (∑x∈X. 2)"
by(rule sum_mono2[OF assms]) simp
also have "… = 2 * card X" by(simp)
finally show "?L ≤ …" .
qed
lemma m_st_anti_mono:
"S1 ⊑ S2 ⟹ m_st m_ivl S2 ≤ m_st m_ivl S1"
proof(auto simp: m_st_def le_st_def lookup_def split: if_splits)
let ?X = "set(dom S1)" let ?Y = "set(dom S2)"
let ?f = "fun S1" let ?g = "fun S2"
assume asm: "∀x∈?Y. (x ∈ ?X ⟶ ?f x ⊑ ?g x) ∧ (x ∈ ?X ∨ ⊤ ⊑ ?g x)"
hence 1: "∀y∈?Y∩?X. m_ivl(?g y) ≤ m_ivl(?f y)" by(simp add: m_ivl_anti_mono)
have 0: "∀x∈?Y-?X. m_ivl(?g x) = 0" using asm by (auto simp: Top_less_ivl)
have "(∑y∈?Y. m_ivl(?g y)) = (∑y∈(?Y-?X) ∪ (?Y∩?X). m_ivl(?g y))"
by (metis Un_Diff_Int)
also have "… = (∑y∈?Y-?X. m_ivl(?g y)) + (∑y∈?Y∩?X. m_ivl(?g y))"
by(subst sum.union_disjoint) auto
also have "(∑y∈?Y-?X. m_ivl(?g y)) = 0" using 0 by simp
also have "0 + (∑y∈?Y∩?X. m_ivl(?g y)) = (∑y∈?Y∩?X. m_ivl(?g y))" by simp
also have "… ≤ (∑y∈?Y∩?X. m_ivl(?f y))"
by(rule sum_mono)(simp add: 1)
also have "… ≤ (∑y∈?X. m_ivl(?f y))"
by(simp add: sum_mono2[of "?X" "?Y Int ?X", OF _ Int_lower2])
finally show "(∑y∈?Y. m_ivl(?g y)) ≤ (∑x∈?X. m_ivl(?f x))" .
qed
lemma m_st_widen:
assumes "¬ S2 ⊑ S1" shows "m_st m_ivl (S1 ∇ S2) < m_st m_ivl S1"
proof-
{ let ?X = "set(dom S1)" let ?Y = "set(dom S2)"
let ?f = "fun S1" let ?g = "fun S2"
fix x assume "x ∈ ?X" "¬ lookup S2 x ⊑ ?f x"
have "(∑x∈?X∩?Y. m_ivl(?f x ∇ ?g x)) < (∑x∈?X. m_ivl(?f x))" (is "?L < ?R")
proof cases
assume "x : ?Y"
have "?L < (∑x∈?X∩?Y. m_ivl(?f x))"
proof(rule sum_strict_mono_ex1, simp)
show "∀x∈?X∩?Y. m_ivl(?f x ∇ ?g x) ≤ m_ivl (?f x)"
by (metis m_ivl_anti_mono widen1)
next
show "∃x∈?X∩?Y. m_ivl(?f x ∇ ?g x) < m_ivl(?f x)"
using ‹x:?X› ‹x:?Y› ‹¬ lookup S2 x ⊑ ?f x›
by (metis IntI m_ivl_widen lookup_def)
qed
also have "… ≤ ?R" by(simp add: sum_mono2[OF _ Int_lower1])
finally show ?thesis .
next
assume "x ~: ?Y"
have "?L ≤ (∑x∈?X∩?Y. m_ivl(?f x))"
proof(rule sum_mono, simp)
fix x assume "x:?X ∧ x:?Y" show "m_ivl(?f x ∇ ?g x) ≤ m_ivl (?f x)"
by (metis m_ivl_anti_mono widen1)
qed
also have "… < m_ivl(?f x) + …"
using m_ivl_widen[OF ‹¬ lookup S2 x ⊑ ?f x›]
by (metis Nat.le_refl add_strict_increasing gr0I not_less0)
also have "… = (∑y∈insert x (?X∩?Y). m_ivl(?f y))"
using ‹x ~: ?Y› by simp
also have "… ≤ (∑x∈?X. m_ivl(?f x))"
by(rule sum_mono2)(insert ‹x:?X›, auto)
finally show ?thesis .
qed
} with assms show ?thesis
by(auto simp: le_st_def widen_st_def m_st_def Int_def)
qed
definition "n_st m X st = (∑x∈X. m(lookup st x))"
lemma n_st_mono: assumes "set(dom S1) ⊆ X" "set(dom S2) ⊆ X" "S1 ⊑ S2"
shows "n_st n_ivl X S1 ≤ n_st n_ivl X S2"
proof-
have "(∑x∈X. n_ivl(lookup S1 x)) ≤ (∑x∈X. n_ivl(lookup S2 x))"
apply(rule sum_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) ⊆ X" "set(dom S2) ⊆ X"
and "S2 ⊑ S1" "¬ S1 ⊑ S1 △ S2"
shows "n_st n_ivl X (S1 △ S2) < n_st n_ivl X S1"
proof-
have 1: "∀x∈X. n_ivl (lookup (S1 △ S2) x) ≤ 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: "∃x∈X. n_ivl (lookup (S1 △ 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 "(∑x∈X. n_ivl(lookup (S1 △ S2) x)) < (∑x∈X. n_ivl(lookup S1 x))"
apply(rule sum_strict_mono_ex1[OF ‹finite X›]) using 1 2 by blast+
thus ?thesis by(simp add: n_st_def)
qed
subsection "Termination: Option"
definition "m_o m n opt = (case opt of None ⇒ n+1 | Some x ⇒ m x)"
lemma m_o_anti_mono: "finite X ⟹ domo S2 ⊆ X ⟹ S1 ⊑ S2 ⟹
m_o (m_st m_ivl) (2 * card X) S2 ≤ m_o (m_st m_ivl) (2 * card X) S1"
apply(induction S1 S2 rule: le_option.induct)
apply(auto simp: domo_def m_o_def m_st_anti_mono le_SucI m_st_height
split: option.splits)
done
lemma m_o_widen: "⟦ finite X; domo S2 ⊆ X; ¬ S2 ⊑ S1 ⟧ ⟹
m_o (m_st m_ivl) (2 * card X) (S1 ∇ 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 m_st_widen
split: option.split)
definition "n_o n opt = (case opt of None ⇒ 0 | Some x ⇒ n x + 1)"
lemma n_o_mono: "domo S1 ⊆ X ⟹ domo S2 ⊆ X ⟹ S1 ⊑ S2 ⟹
n_o (n_st n_ivl X) S1 ≤ 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:
"⟦ finite X; domo S1 ⊆ X; domo S2 ⊆ X; S2 ⊑ S1; ¬ S1 ⊑ S1 △ S2 ⟧
⟹ n_o (n_st n_ivl X) (S1 △ 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 ∇ S2) ⊆ domo S1 ∪ 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 △ S2) ⊆ domo S1 ∪ domo S2"
apply(induction S1 S2 rule: narrow_option.induct)
apply (auto simp: domo_def narrow_st_def)
done
subsection "Termination: Commands"
lemma strip_widen_acom[simp]:
"strip c' = strip (c::'a::WN acom) ⟹ strip (c ∇⇩c c') = strip c"
by(induction "widen::'a⇒'a⇒'a" c c' rule: map2_acom.induct) simp_all
lemma strip_narrow_acom[simp]:
"strip c' = strip (c::'a::WN acom) ⟹ strip (c △⇩c c') = strip c"
by(induction "narrow::'a⇒'a⇒'a" c c' rule: map2_acom.induct) simp_all
lemma annos_widen_acom[simp]: "strip c1 = strip (c2::'a::WN acom) ⟹
annos(c1 ∇⇩c c2) = map (%(x,y).x∇y) (zip (annos c1) (annos(c2::'a::WN acom)))"
by(induction "widen::'a⇒'a⇒'a" c1 c2 rule: map2_acom.induct)
(simp_all add: size_annos_same2)
lemma annos_narrow_acom[simp]: "strip c1 = strip (c2::'a::WN acom) ⟹
annos(c1 △⇩c c2) = map (%(x,y).x△y) (zip (annos c1) (annos(c2::'a::WN acom)))"
by(induction "narrow::'a⇒'a⇒'a" c1 c2 rule: map2_acom.induct)
(simp_all add: size_annos_same2)
lemma widen_acom_Com[simp]: "strip c2 = strip c1 ⟹
c1 : Com X ⟹ c2 : Com X ⟹ (c1 ∇⇩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: widen_st_def)
done
lemma narrow_acom_Com[simp]: "strip c2 = strip c1 ⟹
c1 : Com X ⟹ c2 : Com X ⟹ (c1 △⇩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 ∑i=0..<size as. m(as!i))"
lemma measure_m_c: "finite X ⟹ {(c, c ∇⇩c c') |c c'::ivl st option acom.
strip c' = strip c ∧ c : Com X ∧ c' : Com X ∧ ¬ c' ⊑ c}¯
⊆ measure(m_c(m_o (m_st m_ivl) (2*card(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 sum_strict_mono_ex1)
apply simp
apply (clarsimp)
apply(erule m_o_anti_mono)
apply(rule subset_trans[OF domo_widen_subset])
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 m_o_widen)
apply (simp)+
done
lemma measure_n_c: "finite X ⟹ {(c, c △⇩c c') |c c'.
strip c = strip c' ∧ c ∈ Com X ∧ c' ∈ Com X ∧ c' ⊑ c ∧ ¬ c ⊑ c △⇩c c'}¯
⊆ 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 sum_strict_mono_ex1)
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)
apply(rule_tac x=n in bexI)
prefer 2 apply simp
apply(erule n_o_narrow)
apply (simp)+
done
subsection "Termination: Post-Fixed Point Iterations"
lemma iter_widen_termination:
fixes c0 :: "'a::WN acom"
assumes P_f: "⋀c. P c ⟹ P(f c)"
assumes P_widen: "⋀c c'. P c ⟹ P c' ⟹ P(c ∇⇩c c')"
and "wf({(c::'a acom,c ∇⇩c c')|c c'. P c ∧ P c' ∧ ~ c' ⊑ c}^-1)"
and "P c0" and "c0 ⊑ f c0" shows "∃c. iter_widen f c0 = Some c"
proof(simp add: iter_widen_def, rule wf_while_option_Some[where P = "P"])
show "wf {(cc', c). (P c ∧ ¬ f c ⊑ c) ∧ cc' = c ∇⇩c f c}"
apply(rule wf_subset[OF assms(3)]) by(blast intro: P_f)
next
show "P c0" by(rule ‹P c0›)
next
fix c assume "P c" thus "P (c ∇⇩c f c)" by(simp add: P_f P_widen)
qed
lemma iter_narrow_termination:
assumes P_f: "⋀c. P c ⟹ P(c △⇩c f c)"
and wf: "wf({(c, c △⇩c f c)|c c'. P c ∧ ~ c ⊑ c △⇩c f c}^-1)"
and "P c0" shows "∃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 ∧ ¬ c ⊑ c △⇩c f c) ∧ c' = c △⇩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 △⇩c f c)" by(simp add: P_f)
qed
lemma iter_winden_step_ivl_termination:
"∃c. iter_widen (step_ivl ⊤) (⊥⇩c c0) = Some c"
apply(rule iter_widen_termination[where
P = "%c. strip c = c0 ∧ c : Com(vars c0)"])
apply (simp_all add: step'_Com bot_acom)
apply(rule wf_subset)
apply(rule wf_measure)
apply(rule subset_trans)
prefer 2
apply(rule measure_m_c[where X = "vars c0", OF finite_cvars])
apply blast
done
lemma iter_narrow_step_ivl_termination:
"c0 ∈ Com (vars(strip c0)) ⟹ step_ivl ⊤ c0 ⊑ c0 ⟹
∃c. iter_narrow (step_ivl ⊤) c0 = Some c"
apply(rule iter_narrow_termination[where
P = "%c. strip c = strip c0 ∧ c : Com(vars(strip c0)) ∧ step_ivl ⊤ c ⊑ 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')
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 "∀c::'a st option acom. c : Com(X) ⟶ vars(strip c) ⊆ X ⟶ f c : Com(X)"
and "c : Com(X)" and "vars(strip c) ⊆ X" shows "c' : Com(X)"
using while_option_rule[where P = "λc'. c' : Com(X) ∧ vars(strip c') ⊆ X", OF _ assms(1)]
by(simp add: assms(2-))
lemma iter_widen_Com: fixes f :: "'a::WN st option acom ⇒ 'a st option acom"
assumes "iter_widen f c = Some c'"
and "∀c. c : Com(X) ⟶ vars(strip c) ⊆ X ⟶ f c : Com(X)"
and "!!c. strip(f c) = strip c"
and "c : Com(X)" and "vars (strip c) ⊆ X" shows "c' : Com(X)"
proof-
have "∀c. c : Com(X) ⟶ vars(strip c) ⊆ X ⟶ c ∇⇩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
context Abs_Int2
begin
lemma iter_widen_step'_Com:
"iter_widen (step' ⊤) c = Some c' ⟹ vars(strip c) ⊆ X ⟹ c : Com(X)
⟹ 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
end
theorem AI_ivl'_termination:
"∃c'. AI_ivl' c = 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