Theory Abs_Int3
subsection "Widening and Narrowing"
theory Abs_Int3
imports Abs_Int2_ivl
begin
class widen =
fixes widen :: "'a ⇒ 'a ⇒ 'a" (infix "∇" 65)
class narrow =
fixes narrow :: "'a ⇒ 'a ⇒ 'a" (infix "△" 65)
class wn = widen + narrow + order +
assumes widen1: "x ≤ x ∇ y"
assumes widen2: "y ≤ x ∇ y"
assumes narrow1: "y ≤ x ⟹ y ≤ x △ y"
assumes narrow2: "y ≤ x ⟹ x △ y ≤ x"
begin
lemma narrowid[simp]: "x △ x = x"
by (rule order.antisym) (simp_all add: narrow1 narrow2)
end
lemma top_widen_top[simp]: "⊤ ∇ ⊤ = (⊤::_::{wn,order_top})"
by (metis eq_iff top_greatest widen2)
instantiation ivl :: wn
begin
definition "widen_rep p1 p2 =
(if is_empty_rep p1 then p2 else if is_empty_rep p2 then p1 else
let (l1,h1) = p1; (l2,h2) = p2
in (if l2 < l1 then Minf else l1, if h1 < h2 then Pinf else h1))"
lift_definition widen_ivl :: "ivl ⇒ ivl ⇒ ivl" is widen_rep
by(auto simp: widen_rep_def eq_ivl_iff)
definition "narrow_rep p1 p2 =
(if is_empty_rep p1 ∨ is_empty_rep p2 then empty_rep else
let (l1,h1) = p1; (l2,h2) = p2
in (if l1 = Minf then l2 else l1, if h1 = Pinf then h2 else h1))"
lift_definition narrow_ivl :: "ivl ⇒ ivl ⇒ ivl" is narrow_rep
by(auto simp: narrow_rep_def eq_ivl_iff)
instance
proof
qed (transfer, auto simp: widen_rep_def narrow_rep_def le_iff_subset γ_rep_def subset_eq is_empty_rep_def empty_rep_def eq_ivl_def split: if_splits extended.splits)+
end
instantiation st :: ("{order_top,wn}")wn
begin
lift_definition widen_st :: "'a st ⇒ 'a st ⇒ 'a st" is "map2_st_rep (∇)"
by(auto simp: eq_st_def)
lift_definition narrow_st :: "'a st ⇒ 'a st ⇒ 'a st" is "map2_st_rep (△)"
by(auto simp: eq_st_def)
instance
proof (standard, goal_cases)
case 1 thus ?case by transfer (simp add: less_eq_st_rep_iff widen1)
next
case 2 thus ?case by transfer (simp add: less_eq_st_rep_iff widen2)
next
case 3 thus ?case by transfer (simp add: less_eq_st_rep_iff narrow1)
next
case 4 thus ?case by transfer (simp add: less_eq_st_rep_iff narrow2)
qed
end
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) thus ?case
by(induct x y rule: widen_option.induct)(simp_all add: widen1)
next
case (2 x y) thus ?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
definition map2_acom :: "('a ⇒ 'a ⇒ 'a) ⇒ 'a acom ⇒ 'a acom ⇒ 'a acom"
where
"map2_acom f C1 C2 = annotate (λp. f (anno C1 p) (anno C2 p)) (strip C1)"
instantiation acom :: (widen)widen
begin
definition "widen_acom = map2_acom (∇)"
instance ..
end
instantiation acom :: (narrow)narrow
begin
definition "narrow_acom = map2_acom (△)"
instance ..
end
lemma strip_map2_acom[simp]:
"strip C1 = strip C2 ⟹ strip(map2_acom f C1 C2) = strip C1"
by(simp add: map2_acom_def)
lemma strip_widen_acom[simp]:
"strip C1 = strip C2 ⟹ strip(C1 ∇ C2) = strip C1"
by(simp add: widen_acom_def)
lemma strip_narrow_acom[simp]:
"strip C1 = strip C2 ⟹ strip(C1 △ C2) = strip C1"
by(simp add: narrow_acom_def)
lemma narrow1_acom: "C2 ≤ C1 ⟹ C2 ≤ C1 △ (C2::'a::wn acom)"
by(simp add: narrow_acom_def narrow1 map2_acom_def less_eq_acom_def size_annos)
lemma narrow2_acom: "C2 ≤ C1 ⟹ C1 △ (C2::'a::wn acom) ≤ C1"
by(simp add: narrow_acom_def narrow2 map2_acom_def less_eq_acom_def size_annos)
subsubsection "Pre-fixpoint computation"
definition iter_widen :: "('a ⇒ 'a) ⇒ 'a ⇒ ('a::{order,widen})option"
where "iter_widen f = while_option (λx. ¬ f x ≤ x) (λx. x ∇ f x)"
definition iter_narrow :: "('a ⇒ 'a) ⇒ 'a ⇒ ('a::{order,narrow})option"
where "iter_narrow f = while_option (λx. x △ f x < x) (λx. x △ f x)"
definition pfp_wn :: "('a::{order,widen,narrow} ⇒ 'a) ⇒ 'a ⇒ 'a option"
where "pfp_wn f x =
(case iter_widen f x of None ⇒ None | Some p ⇒ iter_narrow f p)"
lemma iter_widen_pfp: "iter_widen f x = Some p ⟹ f p ≤ p"
by(auto simp add: iter_widen_def dest: while_option_stop)
lemma iter_widen_inv:
assumes "!!x. P x ⟹ P(f x)" "!!x1 x2. P x1 ⟹ P x2 ⟹ P(x1 ∇ x2)" and "P x"
and "iter_widen f x = Some y" shows "P y"
using while_option_rule[where P = "P", OF _ assms(4)[unfolded iter_widen_def]]
by (blast intro: assms(1-3))
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::{order,widen} 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 ∇ f C) = strip C"
by (metis assms(1) strip_map2_acom widen_acom_def)
from strip_while[OF this] assms(2) show ?thesis by(simp add: iter_widen_def)
qed
lemma iter_narrow_pfp:
assumes mono: "!!x1 x2::_::wn acom. P x1 ⟹ P x2 ⟹ x1 ≤ x2 ⟹ f x1 ≤ f x2"
and Pinv: "!!x. P x ⟹ P(f x)" "!!x1 x2. P x1 ⟹ P x2 ⟹ P(x1 △ x2)"
and "P p0" and "f p0 ≤ p0" and "iter_narrow f p0 = Some p"
shows "P p ∧ f p ≤ p"
proof-
let ?Q = "%p. P p ∧ f p ≤ p ∧ p ≤ p0"
have "?Q (p △ f p)" if Q: "?Q p" for p
proof auto
note P = conjunct1[OF Q] and 12 = conjunct2[OF Q]
note 1 = conjunct1[OF 12] and 2 = conjunct2[OF 12]
let ?p' = "p △ f p"
show "P ?p'" by (blast intro: P Pinv)
have "f ?p' ≤ f p" by(rule mono[OF ‹P (p △ f p)› P narrow2_acom[OF 1]])
also have "… ≤ ?p'" by(rule narrow1_acom[OF 1])
finally show "f ?p' ≤ ?p'" .
have "?p' ≤ p" by (rule narrow2_acom[OF 1])
also have "p ≤ p0" by(rule 2)
finally show "?p' ≤ p0" .
qed
thus ?thesis
using while_option_rule[where P = ?Q, OF _ assms(6)[simplified iter_narrow_def]]
by (blast intro: assms(4,5) le_refl)
qed
lemma pfp_wn_pfp:
assumes mono: "!!x1 x2::_::wn acom. P x1 ⟹ P x2 ⟹ x1 ≤ x2 ⟹ f x1 ≤ f x2"
and Pinv: "P x" "!!x. P x ⟹ P(f x)"
"!!x1 x2. P x1 ⟹ P x2 ⟹ P(x1 ∇ x2)"
"!!x1 x2. P x1 ⟹ P x2 ⟹ P(x1 △ x2)"
and pfp_wn: "pfp_wn f x = Some p" shows "P p ∧ f p ≤ p"
proof-
from pfp_wn obtain p0
where its: "iter_widen f x = Some p0" "iter_narrow f p0 = Some p"
by(auto simp: pfp_wn_def split: option.splits)
have "P p0" by (blast intro: iter_widen_inv[where P="P"] its(1) Pinv(1-3))
thus ?thesis
by - (assumption |
rule iter_narrow_pfp[where P=P] mono Pinv(2,4) iter_widen_pfp its)+
qed
lemma strip_pfp_wn:
"⟦ ∀C. strip(f C) = strip C; pfp_wn f C = Some C' ⟧ ⟹ strip C' = strip C"
by(auto simp add: pfp_wn_def iter_narrow_def split: option.splits)
(metis (mono_tags) strip_iter_widen strip_narrow_acom strip_while)
locale Abs_Int_wn = Abs_Int_inv_mono where γ=γ
for γ :: "'av::{wn,bounded_lattice} ⇒ val set"
begin
definition AI_wn :: "com ⇒ 'av st option acom option" where
"AI_wn c = pfp_wn (step' ⊤) (bot c)"
lemma AI_wn_correct: "AI_wn c = Some C ⟹ CS c ≤ γ⇩c C"
proof(simp add: CS_def AI_wn_def)
assume 1: "pfp_wn (step' ⊤) (bot c) = Some C"
have 2: "strip C = c ∧ step' ⊤ C ≤ C"
by(rule pfp_wn_pfp[where x="bot c"]) (simp_all add: 1 mono_step'_top)
have pfp: "step (γ⇩o ⊤) (γ⇩c C) ≤ γ⇩c C"
proof(rule order_trans)
show "step (γ⇩o ⊤) (γ⇩c C) ≤ γ⇩c (step' ⊤ C)"
by(rule step_step')
show "... ≤ γ⇩c C"
by(rule mono_gamma_c[OF conjunct2[OF 2]])
qed
have 3: "strip (γ⇩c C) = c" by(simp add: strip_pfp_wn[OF _ 1])
have "lfp c (step (γ⇩o ⊤)) ≤ γ⇩c C"
by(rule lfp_lowerbound[simplified,where f="step (γ⇩o ⊤)", OF 3 pfp])
thus "lfp c (step UNIV) ≤ γ⇩c C" by simp
qed
end
global_interpretation Abs_Int_wn
where γ = γ_ivl and num' = num_ivl and plus' = "(+)"
and test_num' = in_ivl
and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
defines AI_wn_ivl = AI_wn
..
subsubsection "Tests"
definition "step_up_ivl n = ((λC. C ∇ step_ivl ⊤ C)^^n)"
definition "step_down_ivl n = ((λ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_wn_ivl› converges in a
constant number of steps:›
value "show_acom (step_up_ivl 1 (bot test3_ivl))"
value "show_acom (step_up_ivl 2 (bot test3_ivl))"
value "show_acom (step_up_ivl 3 (bot test3_ivl))"
value "show_acom (step_up_ivl 4 (bot test3_ivl))"
value "show_acom (step_up_ivl 5 (bot test3_ivl))"
value "show_acom (step_up_ivl 6 (bot test3_ivl))"
value "show_acom (step_up_ivl 7 (bot test3_ivl))"
value "show_acom (step_up_ivl 8 (bot test3_ivl))"
value "show_acom (step_down_ivl 1 (step_up_ivl 8 (bot test3_ivl)))"
value "show_acom (step_down_ivl 2 (step_up_ivl 8 (bot test3_ivl)))"
value "show_acom (step_down_ivl 3 (step_up_ivl 8 (bot test3_ivl)))"
value "show_acom (step_down_ivl 4 (step_up_ivl 8 (bot test3_ivl)))"
value "show_acom_opt (AI_wn_ivl test3_ivl)"
text‹Now all the analyses terminate:›
value "show_acom_opt (AI_wn_ivl test4_ivl)"
value "show_acom_opt (AI_wn_ivl test5_ivl)"
value "show_acom_opt (AI_wn_ivl test6_ivl)"
subsubsection "Generic Termination Proof"
lemma top_on_opt_widen:
"top_on_opt o1 X ⟹ top_on_opt o2 X ⟹ top_on_opt (o1 ∇ o2 :: _ st option) X"
apply(induct o1 o2 rule: widen_option.induct)
apply (auto)
by transfer simp
lemma top_on_opt_narrow:
"top_on_opt o1 X ⟹ top_on_opt o2 X ⟹ top_on_opt (o1 △ o2 :: _ st option) X"
apply(induct o1 o2 rule: narrow_option.induct)
apply (auto)
by transfer simp
lemma annos_map2_acom[simp]: "strip C2 = strip C1 ⟹
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:
"⟦top_on_acom C1 X; strip C1 = strip C2; top_on_acom C2 X⟧
⟹ top_on_acom (C1 ∇ C2 :: _ st option acom) X"
by(auto simp add: widen_acom_def top_on_acom_def)(metis top_on_opt_widen in_set_zipE)
lemma top_on_acom_narrow:
"⟦top_on_acom C1 X; strip C1 = strip C2; top_on_acom C2 X⟧
⟹ top_on_acom (C1 △ C2 :: _ st option acom) X"
by(auto simp add: narrow_acom_def top_on_acom_def)(metis top_on_opt_narrow in_set_zipE)
text‹The assumptions for widening and narrowing differ because during
narrowing we have the invariant \<^prop>‹y ≤ x› (where ‹y› is the next
iterate), but during widening there is no such invariant, there we only have
that not yet \<^prop>‹y ≤ x›. This complicates the termination proof for
widening.›
locale Measure_wn = Measure1 where m=m
for m :: "'av::{order_top,wn} ⇒ nat" +
fixes n :: "'av ⇒ nat"
assumes m_anti_mono: "x ≤ y ⟹ m x ≥ m y"
assumes m_widen: "~ y ≤ x ⟹ m(x ∇ y) < m x"
assumes n_narrow: "y ≤ x ⟹ x △ y < x ⟹ n(x △ y) < n x"
begin
lemma m_s_anti_mono_rep: assumes "∀x. S1 x ≤ S2 x"
shows "(∑x∈X. m (S2 x)) ≤ (∑x∈X. m (S1 x))"
proof-
from assms have "∀x. m(S1 x) ≥ m(S2 x)" by (metis m_anti_mono)
thus "(∑x∈X. m (S2 x)) ≤ (∑x∈X. m (S1 x))" by (metis sum_mono)
qed
lemma m_s_anti_mono: "S1 ≤ S2 ⟹ m_s S1 X ≥ m_s S2 X"
unfolding m_s_def
apply (transfer fixing: m)
apply(simp add: less_eq_st_rep_iff eq_st_def m_s_anti_mono_rep)
done
lemma m_s_widen_rep: assumes "finite X" "S1 = S2 on -X" "¬ S2 x ≤ S1 x"
shows "(∑x∈X. m (S1 x ∇ S2 x)) < (∑x∈X. m (S1 x))"
proof-
have 1: "∀x∈X. m(S1 x) ≥ m(S1 x ∇ S2 x)"
by (metis m_anti_mono wn_class.widen1)
have "x ∈ X" using assms(2,3)
by(auto simp add: Ball_def)
hence 2: "∃x∈X. m(S1 x) > m(S1 x ∇ S2 x)"
using assms(3) m_widen by blast
from sum_strict_mono_ex1[OF ‹finite X› 1 2]
show ?thesis .
qed
lemma m_s_widen: "finite X ⟹ fun S1 = fun S2 on -X ==>
~ S2 ≤ S1 ⟹ m_s (S1 ∇ S2) X < m_s S1 X"
apply(auto simp add: less_st_def m_s_def)
apply (transfer fixing: m)
apply(auto simp add: less_eq_st_rep_iff m_s_widen_rep)
done
lemma m_o_anti_mono: "finite X ⟹ top_on_opt o1 (-X) ⟹ top_on_opt o2 (-X) ⟹
o1 ≤ o2 ⟹ m_o o1 X ≥ m_o o2 X"
proof(induction o1 o2 rule: less_eq_option.induct)
case 1 thus ?case by (simp add: m_o_def)(metis m_s_anti_mono)
next
case 2 thus ?case
by(simp add: m_o_def le_SucI m_s_h split: option.splits)
next
case 3 thus ?case by simp
qed
lemma m_o_widen: "⟦ finite X; top_on_opt S1 (-X); top_on_opt S2 (-X); ¬ S2 ≤ S1 ⟧ ⟹
m_o (S1 ∇ S2) X < m_o S1 X"
by(auto simp: m_o_def m_s_h less_Suc_eq_le m_s_widen split: option.split)
lemma m_c_widen:
"strip C1 = strip C2 ⟹ top_on_acom C1 (-vars C1) ⟹ top_on_acom C2 (-vars C2)
⟹ ¬ C2 ≤ C1 ⟹ m_c (C1 ∇ C2) < m_c C1"
apply(auto simp: m_c_def widen_acom_def map2_acom_def size_annos[symmetric] anno_def[symmetric]sum_list_sum_nth)
apply(subgoal_tac "length(annos C2) = length(annos C1)")
prefer 2 apply (simp add: size_annos_same2)
apply (auto)
apply(rule sum_strict_mono_ex1)
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
definition n_s :: "'av st ⇒ vname set ⇒ nat" ("n⇩s") where
"n⇩s S X = (∑x∈X. n(fun S x))"
lemma n_s_narrow_rep:
assumes "finite X" "S1 = S2 on -X" "∀x. S2 x ≤ S1 x" "∀x. S1 x △ S2 x ≤ S1 x"
"S1 x ≠ S1 x △ S2 x"
shows "(∑x∈X. n (S1 x △ S2 x)) < (∑x∈X. n (S1 x))"
proof-
have 1: "∀x. n(S1 x △ S2 x) ≤ n(S1 x)"
by (metis assms(3) assms(4) eq_iff less_le_not_le n_narrow)
have "x ∈ X" by (metis Compl_iff assms(2) assms(5) narrowid)
hence 2: "∃x∈X. n(S1 x △ S2 x) < n(S1 x)"
by (metis assms(3-5) eq_iff less_le_not_le n_narrow)
show ?thesis
apply(rule sum_strict_mono_ex1[OF ‹finite X›]) using 1 2 by blast+
qed
lemma n_s_narrow: "finite X ⟹ fun S1 = fun S2 on -X ⟹ S2 ≤ S1 ⟹ S1 △ S2 < S1
⟹ n⇩s (S1 △ S2) X < n⇩s S1 X"
apply(auto simp add: less_st_def n_s_def)
apply (transfer fixing: n)
apply(auto simp add: less_eq_st_rep_iff eq_st_def fun_eq_iff n_s_narrow_rep)
done
definition n_o :: "'av st option ⇒ vname set ⇒ nat" ("n⇩o") where
"n⇩o opt X = (case opt of None ⇒ 0 | Some S ⇒ n⇩s S X + 1)"
lemma n_o_narrow:
"top_on_opt S1 (-X) ⟹ top_on_opt S2 (-X) ⟹ finite X
⟹ S2 ≤ S1 ⟹ S1 △ S2 < S1 ⟹ n⇩o (S1 △ S2) X < n⇩o S1 X"
apply(induction S1 S2 rule: narrow_option.induct)
apply(auto simp: n_o_def n_s_narrow)
done
definition n_c :: "'av st option acom ⇒ nat" ("n⇩c") where
"n⇩c C = sum_list (map (λa. n⇩o a (vars C)) (annos C))"
lemma less_annos_iff: "(C1 < C2) = (C1 ≤ C2 ∧
(∃i<length (annos C1). annos C1 ! i < annos C2 ! i))"
by(metis (opaque_lifting, no_types) less_le_not_le le_iff_le_annos size_annos_same2)
lemma n_c_narrow: "strip C1 = strip C2
⟹ top_on_acom C1 (- vars C1) ⟹ top_on_acom C2 (- vars C2)
⟹ C2 ≤ C1 ⟹ C1 △ C2 < C1 ⟹ n⇩c (C1 △ C2) < n⇩c C1"
apply(auto simp: n_c_def narrow_acom_def sum_list_sum_nth)
apply(subgoal_tac "length(annos C2) = length(annos C1)")
prefer 2 apply (simp add: size_annos_same2)
apply (auto)
apply(simp add: less_annos_iff le_iff_le_annos)
apply(rule sum_strict_mono_ex1)
apply (auto simp: vars_acom_def top_on_acom_def)
apply (metis n_o_narrow nth_mem finite_cvars less_imp_le le_less order_refl)
apply(rule_tac x=i in bexI)
prefer 2 apply simp
apply(rule n_o_narrow[where X = "vars(strip C2)"])
apply (simp_all)
done
end
lemma iter_widen_termination:
fixes m :: "'a::wn acom ⇒ nat"
assumes P_f: "⋀C. P C ⟹ P(f C)"
and P_widen: "⋀C1 C2. P C1 ⟹ P C2 ⟹ P(C1 ∇ C2)"
and m_widen: "⋀C1 C2. P C1 ⟹ P C2 ⟹ ~ C2 ≤ C1 ⟹ m(C1 ∇ C2) < m C1"
and "P C" shows "∃C'. iter_widen f C = Some C'"
proof(simp add: iter_widen_def,
rule measure_while_option_Some[where P = P and f=m])
show "P C" by(rule ‹P C›)
next
fix C assume "P C" "¬ f C ≤ C" thus "P (C ∇ f C) ∧ m (C ∇ f C) < m C"
by(simp add: P_f P_widen m_widen)
qed
lemma iter_narrow_termination:
fixes n :: "'a::wn acom ⇒ nat"
assumes P_f: "⋀C. P C ⟹ P(f C)"
and P_narrow: "⋀C1 C2. P C1 ⟹ P C2 ⟹ P(C1 △ C2)"
and mono: "⋀C1 C2. P C1 ⟹ P C2 ⟹ C1 ≤ C2 ⟹ f C1 ≤ f C2"
and n_narrow: "⋀C1 C2. P C1 ⟹ P C2 ⟹ C2 ≤ C1 ⟹ C1 △ C2 < C1 ⟹ n(C1 △ C2) < n C1"
and init: "P C" "f C ≤ C" shows "∃C'. iter_narrow f C = Some C'"
proof(simp add: iter_narrow_def,
rule measure_while_option_Some[where f=n and P = "%C. P C ∧ f C ≤ C"])
show "P C ∧ f C ≤ C" using init by blast
next
fix C assume 1: "P C ∧ f C ≤ C" and 2: "C △ f C < C"
hence "P (C △ f C)" by(simp add: P_f P_narrow)
moreover then have "f (C △ f C) ≤ C △ f C"
by (metis narrow1_acom narrow2_acom 1 mono order_trans)
moreover have "n (C △ f C) < n C" using 1 2 by(simp add: n_narrow P_f)
ultimately show "(P (C △ f C) ∧ f (C △ f C) ≤ C △ f C) ∧ n(C △ f C) < n C"
by blast
qed
locale Abs_Int_wn_measure = Abs_Int_wn where γ=γ + Measure_wn where m=m
for γ :: "'av::{wn,bounded_lattice} ⇒ val set" and m :: "'av ⇒ nat"
subsubsection "Termination: Intervals"
definition m_rep :: "eint2 ⇒ nat" where
"m_rep p = (if is_empty_rep p then 3 else
let (l,h) = p in (case l of Minf ⇒ 0 | _ ⇒ 1) + (case h of Pinf ⇒ 0 | _ ⇒ 1))"
lift_definition m_ivl :: "ivl ⇒ nat" is m_rep
by(auto simp: m_rep_def eq_ivl_iff)
lemma m_ivl_nice: "m_ivl[l,h] = (if [l,h] = ⊥ then 3 else
(if l = Minf then 0 else 1) + (if h = Pinf then 0 else 1))"
unfolding bot_ivl_def
by transfer (auto simp: m_rep_def eq_ivl_empty split: extended.split)
lemma m_ivl_height: "m_ivl iv ≤ 3"
by transfer (simp add: m_rep_def split: prod.split extended.split)
lemma m_ivl_anti_mono: "y ≤ x ⟹ m_ivl x ≤ m_ivl y"
by transfer
(auto simp: m_rep_def is_empty_rep_def γ_rep_cases le_iff_subset
split: prod.split extended.splits if_splits)
lemma m_ivl_widen:
"~ y ≤ x ⟹ m_ivl(x ∇ y) < m_ivl x"
by transfer
(auto simp: m_rep_def widen_rep_def is_empty_rep_def γ_rep_cases le_iff_subset
split: prod.split extended.splits if_splits)
definition n_ivl :: "ivl ⇒ nat" where
"n_ivl iv = 3 - m_ivl iv"
lemma n_ivl_narrow:
"x △ y < x ⟹ n_ivl(x △ y) < n_ivl x"
unfolding n_ivl_def
apply(subst (asm) less_le_not_le)
apply transfer
by(auto simp add: m_rep_def narrow_rep_def is_empty_rep_def empty_rep_def γ_rep_cases le_iff_subset
split: prod.splits if_splits extended.split)
global_interpretation Abs_Int_wn_measure
where γ = γ_ivl and num' = num_ivl and plus' = "(+)"
and test_num' = in_ivl
and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
and m = m_ivl and n = n_ivl and h = 3
proof (standard, goal_cases)
case 2 thus ?case by(rule m_ivl_anti_mono)
next
case 1 thus ?case by(rule m_ivl_height)
next
case 3 thus ?case by(rule m_ivl_widen)
next
case 4 from 4(2) show ?case by(rule n_ivl_narrow)
qed
lemma iter_winden_step_ivl_termination:
"∃C. iter_widen (step_ivl ⊤) (bot c) = Some C"
apply(rule iter_widen_termination[where m = "m_c" and P = "%C. strip C = c ∧ top_on_acom C (- vars C)"])
apply (auto simp add: m_c_widen top_on_bot top_on_step'[simplified comp_def vars_acom_def]
vars_acom_def top_on_acom_widen)
done
lemma iter_narrow_step_ivl_termination:
"top_on_acom C (- vars C) ⟹ step_ivl ⊤ C ≤ C ⟹
∃C'. iter_narrow (step_ivl ⊤) C = Some C'"
apply(rule iter_narrow_termination[where n = "n_c" and P = "%C'. strip C = strip C' ∧ top_on_acom C' (-vars C')"])
apply(auto simp: top_on_step'[simplified comp_def vars_acom_def]
mono_step'_top n_c_narrow vars_acom_def top_on_acom_narrow)
done
theorem AI_wn_ivl_termination:
"∃C. AI_wn_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(rule conjunct2)
apply(rule iter_widen_inv[where f = "step' ⊤" and P = "%C. c = strip C & top_on_acom C (- vars C)"])
apply(auto simp: top_on_acom_widen top_on_step'[simplified comp_def vars_acom_def]
iter_widen_pfp top_on_bot vars_acom_def)
done
subsubsection "Counterexamples"
text‹Widening is increasing by assumption, but \<^prop>‹x ≤ f x› is not an invariant of widening.
It can already be lost after the first step:›
lemma assumes "!!x y::'a::wn. x ≤ y ⟹ f x ≤ f y"
and "x ≤ f x" and "¬ f x ≤ x" shows "x ∇ f x ≤ f(x ∇ f x)"
nitpick[card = 3, expect = genuine, show_consts, timeout = 120]
oops
text‹Widening terminates but may converge more slowly than Kleene iteration.
In the following model, Kleene iteration goes from 0 to the least pfp
in one step but widening takes 2 steps to reach a strictly larger pfp:›
lemma assumes "!!x y::'a::wn. x ≤ y ⟹ f x ≤ f y"
and "x ≤ f x" and "¬ f x ≤ x" and "f(f x) ≤ f x"
shows "f(x ∇ f x) ≤ x ∇ f x"
nitpick[card = 4, expect = genuine, show_consts, timeout = 120]
oops
end