Theory Backward_Domain_Mono
theory Backward_Domain_Mono
imports Backward_Domain
begin
section ‹Monotone and reductive backward filtering›
text ‹
Split out of @{theory Voblint_Domain.Backward_Domain}: this theory proves the
filters of ‹sound_refinement› reductive, from its reductive intersection, and
adds ‹mono_refinement› for monotone operations on top of it.
›
subsection ‹Pairwise order for reductive/monotone inverse operators›
text ‹
A minimal componentwise order on ‹'a * 'a›, used only to state each inverse
operator's monotonicity and reductiveness as a single fact about its returned
pair rather than as two separately-assumed projections. Deliberately not
‹'a * 'a›'s own ‹≤›: some already-transitively-imported theory instantiates
‹('a,'b) prod :: order› here with a non-componentwise (order-with-a-‹<›-disjunct)
definition, so relying on the ambient ‹≤› would silently pick up the wrong
relation. This local, self-contained ‹≤_pair› avoids that entirely.
›
abbreviation le_pair :: "'a::order × 'a ⇒ 'a × 'a ⇒ bool" where
"le_pair p q ≡ fst p ≤ fst q ∧ snd p ≤ snd q"
lemma le_pair_fst: "le_pair p q ⟹ fst p ≤ fst q"
by simp
lemma le_pair_snd: "le_pair p q ⟹ snd p ≤ snd q"
by simp
subsection ‹Refined backward-analysis locale›
text ‹
Extends @{locale sound_refinement} with two orthogonal strengthenings of the
domain-author operators, bundled into one locale so a concrete domain proves
both against a single interpretation rather than reproving @{locale
sound_refinement}'s base soundness once per strengthening:
- Monotonicity: the generic @{term afilter} / @{term bfilter} are then
monotone in the abstract state (and target value) by the same induction
that proves their soundness.
- Reductiveness: ‹intersect›'s result is below both input operands --
refinement narrows, never enlarges. This is the only reductiveness this
locale assumes: ‹afilter_reductive›/‹bfilter_reductive› need it solely at
@{term afilter}'s ‹V› case, where ‹intersect› is the sole narrowing step;
the ‹inv_*› operators have no reductiveness assumption of their own,
because none of the reductiveness proofs need one -- each recursive
‹afilter›/‹bfilter› step is bounded by its own induction hypothesis, not
by a per-operator shrink fact.
Each ‹inv_*› operator's monotonicity contract is one @{const le_pair} fact
about its returned pair rather than two separately-assumed ‹fst›/‹snd›
projections; the componentwise facts ‹afilter_mono›/‹bfilter_mono›'s own
induction needs are derived from these once, inside this locale.
›
text ‹
Reductiveness is part of every backward domain, and monotonicity is a
separate locale because a domain can be reductive without being monotone,
and the executable lifted filtering needs only reductiveness. Int's
‹Refine_Fixpoint› mode is exactly that case: ‹refine› is reductive at every
mode but monotone only off ‹Refine_Fixpoint› (‹Int_Arithmetic›'s
‹refine_nonfixpoint_mono›), so it interprets ‹sound_refinement› and gets the
precise, dead-arm-eliminating filtering, while ‹branch_mono› and the rest
of the monotonicity layer stay out of its reach.
›
context sound_refinement
begin
text ‹
Reductiveness of the whole recursion, not just its individual ‹intersect›
steps: \<^term>‹afilter e a d›/\<^term>‹bfilter b res d› are always ‹≤› their
input state, so a compound expression's re-narrowing of an already-settled
location never revives it -- once a location is \<^const>‹is_empty› it stays
\<^const>‹is_empty› through every later step (@{thm is_empty_state_antimono}).
Neither proof needs any monotonicity: ‹afilter›'s ‹V› case is bounded by
‹intersect_reductive2›, every compound case by its own induction hypothesis.
›
lemma afilter_Plus_unfold:
"afilter (Plus e1 e2) a d =
afilter e1 (fst (inv_plus a (⟦e1⟧⇧♯ d) (⟦e2⟧⇧♯ d)))
(afilter e2 (snd (inv_plus a (⟦e1⟧⇧♯ d) (⟦e2⟧⇧♯ d))) d)"
by (simp add: Let_def case_prod_beta)
lemma afilter_Minus_unfold:
"afilter (Minus e1 e2) a d =
afilter e1 (fst (inv_minus a (⟦e1⟧⇧♯ d) (⟦e2⟧⇧♯ d)))
(afilter e2 (snd (inv_minus a (⟦e1⟧⇧♯ d) (⟦e2⟧⇧♯ d))) d)"
by (simp add: Let_def case_prod_beta)
lemma afilter_Times_unfold:
"afilter (Times e1 e2) a d =
afilter e1 (fst (inv_times a (⟦e1⟧⇧♯ d) (⟦e2⟧⇧♯ d)))
(afilter e2 (snd (inv_times a (⟦e1⟧⇧♯ d) (⟦e2⟧⇧♯ d))) d)"
by (simp add: Let_def case_prod_beta)
lemma bfilter_Less_unfold:
"bfilter (Less e1 e2) res d =
afilter e1 (fst (inv_less res (⟦e1⟧⇧♯ d) (⟦e2⟧⇧♯ d)))
(afilter e2 (snd (inv_less res (⟦e1⟧⇧♯ d) (⟦e2⟧⇧♯ d))) d)"
by (simp add: Let_def case_prod_beta)
lemma bfilter_GreaterEq_unfold:
"bfilter (GreaterEq e1 e2) res d =
afilter e1 (fst (inv_less (¬ res) (⟦e1⟧⇧♯ d) (⟦e2⟧⇧♯ d)))
(afilter e2 (snd (inv_less (¬ res) (⟦e1⟧⇧♯ d) (⟦e2⟧⇧♯ d))) d)"
by (simp add: Let_def case_prod_beta)
lemma bfilter_Greater_unfold:
"bfilter (Greater e1 e2) res d =
afilter e2 (fst (inv_less res (⟦e2⟧⇧♯ d) (⟦e1⟧⇧♯ d)))
(afilter e1 (snd (inv_less res (⟦e2⟧⇧♯ d) (⟦e1⟧⇧♯ d))) d)"
by (simp add: Let_def case_prod_beta)
lemma bfilter_LessEq_unfold:
"bfilter (LessEq e1 e2) res d =
afilter e2 (fst (inv_less (¬ res) (⟦e2⟧⇧♯ d) (⟦e1⟧⇧♯ d)))
(afilter e1 (snd (inv_less (¬ res) (⟦e2⟧⇧♯ d) (⟦e1⟧⇧♯ d))) d)"
by (simp add: Let_def case_prod_beta)
lemma bfilter_Eq_unfold:
"bfilter (Eq e1 e2) res d =
afilter e1 (fst (inv_eq res (⟦e1⟧⇧♯ d) (⟦e2⟧⇧♯ d)))
(afilter e2 (snd (inv_eq res (⟦e1⟧⇧♯ d) (⟦e2⟧⇧♯ d))) d)"
by (simp add: Let_def case_prod_beta)
lemma bfilter_NotEq_unfold:
"bfilter (NotEq e1 e2) res d =
afilter e1 (fst (inv_eq (¬ res) (⟦e1⟧⇧♯ d) (⟦e2⟧⇧♯ d)))
(afilter e2 (snd (inv_eq (¬ res) (⟦e1⟧⇧♯ d) (⟦e2⟧⇧♯ d))) d)"
by (simp add: Let_def case_prod_beta)
lemma afilter_reductive: "afilter e a d ≤ d"
proof (induction e arbitrary: a d)
case (V x) then show ?case by (auto simp: le_fun_def)
next
case (Plus e1 e2) then show ?case
unfolding afilter_Plus_unfold split_beta by (blast intro: order_trans)
next
case (Minus e1 e2) then show ?case
unfolding afilter_Minus_unfold split_beta by (blast intro: order_trans)
next
case (Times e1 e2) then show ?case
unfolding afilter_Times_unfold split_beta by (blast intro: order_trans)
qed simp_all
lemma bfilter_reductive: "bfilter b res d ≤ d"
proof (induction b arbitrary: res d)
case (Not b)
show ?case unfolding bfilter.simps by (rule Not.IH)
next
case (And b1 b2)
show ?case
proof (cases res)
case True
have "bfilter b1 True (bfilter b2 True d) ≤ d"
by (rule order_trans[OF And.IH(1) And.IH(2)])
then show ?thesis using True by simp
next
case False
then have res: "res = False" by simp
show ?thesis unfolding res bfilter.simps
by (intro sup_least) (simp_all add: And.IH)
qed
next
case (Or b1 b2)
show ?case
proof (cases res)
case True
then have res: "res = True" by simp
show ?thesis unfolding res bfilter.simps
by (intro sup_least) (simp_all add: Or.IH)
next
case False
have "bfilter b1 False (bfilter b2 False d) ≤ d"
by (rule order_trans[OF Or.IH(1) Or.IH(2)])
then show ?thesis using False by simp
qed
qed (simp_all only: bfilter.simps Let_def split_beta afilter_reductive
order_trans[OF afilter_reductive afilter_reductive])
text ‹
A witness-bottom incoming state forces ‹bfilter_lifted› to ‹Bot›
regardless of what ‹feasible› answers: narrowing (‹bfilter_reductive›) can
only shrink a location, never repopulate one already empty, so whichever
location witnessed ‹sigma›'s emptiness survives every leaf update and every
join arm untouched. This is what lets an executable caller skip
‹bfilter_st_lift›'s ‹live_default_st› precondition entirely on a dead
state: the answer is ‹Bot› either way, forward-gate false positive or not.
›
lemma bfilter_lifted_witness_bottom:
assumes "is_empty_state sigma"
shows "bfilter_lifted e pol sigma = Bot"
using assms proof (induction e arbitrary: pol)
case (And b1 b2) then show ?case by (cases pol) simp_all
next
case (Or b1 b2) then show ?case by (cases pol) simp_all
qed (simp_all add: is_empty_state_antimono[OF bfilter_reductive] del: bfilter.simps)
lemma branch_lifted_witness_bottom:
assumes "is_empty_state sigma"
shows "branch_lifted e pol sigma = Bot"
unfolding branch_lifted_def using bfilter_lifted_witness_bottom[OF assms] by simp
lemma branch_witness_bottom:
assumes "is_empty_state sigma"
shows "branch e pol sigma = bot"
unfolding branch_def using branch_lifted_witness_bottom[OF assms] by simp
end
text ‹The monotonicity half of the strengthening. Each inverse operator is assumed monotone
in every argument, which is what carries ‹bfilter› and ‹branch› through their structural
induction. ‹tobool_mono› is the one assumption that does not read that way: a definite
truth value found at the coarser value must survive at the sharper one, and only a
non-empty sharper value can be asked -- an empty one decides everything vacuously.›
locale mono_refinement =
sound_refinement + mono_intersection intersect
+ mono_evaluator gamma_state aval_abs + mono_truth_test tobool +
assumes inv_less_mono:
"x1 ≤ x2 ⟹ y1 ≤ y2 ⟹ le_pair (inv_less res x1 y1) (inv_less res x2 y2)"
and inv_eq_mono:
"x1 ≤ x2 ⟹ y1 ≤ y2 ⟹ le_pair (inv_eq res x1 y1) (inv_eq res x2 y2)"
and inv_plus_mono:
"r1 ≤ r2 ⟹ x1 ≤ x2 ⟹ y1 ≤ y2 ⟹ le_pair (inv_plus r1 x1 y1) (inv_plus r2 x2 y2)"
and inv_minus_mono:
"r1 ≤ r2 ⟹ x1 ≤ x2 ⟹ y1 ≤ y2 ⟹ le_pair (inv_minus r1 x1 y1) (inv_minus r2 x2 y2)"
and inv_times_mono:
"r1 ≤ r2 ⟹ x1 ≤ x2 ⟹ y1 ≤ y2 ⟹ le_pair (inv_times r1 x1 y1) (inv_times r2 x2 y2)"
begin
lemmas inv_less_mono_fst [intro] = inv_less_mono[THEN le_pair_fst]
lemmas inv_less_mono_snd [intro] = inv_less_mono[THEN le_pair_snd]
lemmas inv_eq_mono_fst [intro] = inv_eq_mono[THEN le_pair_fst]
lemmas inv_eq_mono_snd [intro] = inv_eq_mono[THEN le_pair_snd]
lemmas inv_plus_mono_fst [intro] = inv_plus_mono[THEN le_pair_fst]
lemmas inv_plus_mono_snd [intro] = inv_plus_mono[THEN le_pair_snd]
lemmas inv_minus_mono_fst [intro] = inv_minus_mono[THEN le_pair_fst]
lemmas inv_minus_mono_snd [intro] = inv_minus_mono[THEN le_pair_snd]
lemmas inv_times_mono_fst [intro] = inv_times_mono[THEN le_pair_fst]
lemmas inv_times_mono_snd [intro] = inv_times_mono[THEN le_pair_snd]
lemma afilter_mono:
"a1 ≤ a2 ⟹ d1 ≤ d2 ⟹ afilter e a1 d1 ≤ afilter e a2 d2"
proof (induction e arbitrary: a1 a2 d1 d2)
case (N n)
then show ?case by simp
next
case (V x)
show ?case
unfolding afilter.simps
proof (rule le_funI)
fix y
show "(d1(x := intersect a1 (d1 x))) y ≤ (d2(x := intersect a2 (d2 x))) y"
proof (cases "y = x")
case True
thus ?thesis using intersect_mono[OF V.prems(1) le_funD[OF V.prems(2)]] by simp
next
case False thus ?thesis using le_funD[OF V.prems(2)] by simp
qed
qed
next
case (Plus e1 e2)
have v1: "⟦e1⟧⇧♯ d1 ≤ ⟦e1⟧⇧♯ d2" and v2: "⟦e2⟧⇧♯ d1 ≤ ⟦e2⟧⇧♯ d2"
using aval_abs_mono[OF Plus.prems(2)] by simp_all
show ?case unfolding afilter_Plus_unfold
using v1 v2 Plus.prems
by (blast intro: Plus.IH)
next
case (Minus e1 e2)
have v1: "⟦e1⟧⇧♯ d1 ≤ ⟦e1⟧⇧♯ d2" and v2: "⟦e2⟧⇧♯ d1 ≤ ⟦e2⟧⇧♯ d2"
using aval_abs_mono[OF Minus.prems(2)] by simp_all
show ?case unfolding afilter_Minus_unfold
using v1 v2 Minus.prems
by (blast intro: Minus.IH)
next
case (Times e1 e2)
have v1: "⟦e1⟧⇧♯ d1 ≤ ⟦e1⟧⇧♯ d2" and v2: "⟦e2⟧⇧♯ d1 ≤ ⟦e2⟧⇧♯ d2"
using aval_abs_mono[OF Times.prems(2)] by simp_all
show ?case unfolding afilter_Times_unfold
using v1 v2 Times.prems
by (blast intro: Times.IH)
next
case (Less e1 e2) then show ?case by simp
next
case (Div e1 e2) then show ?case by simp
next
case (Mod e1 e2) then show ?case by simp
next
case (GreaterEq e1 e2) then show ?case by simp
next
case (Greater e1 e2) then show ?case by simp
next
case (LessEq e1 e2) then show ?case by simp
next
case (Eq e1 e2) then show ?case by simp
next
case (NotEq e1 e2) then show ?case by simp
next
case (Not e) then show ?case by simp
next
case (And e1 e2) then show ?case by simp
next
case (Or e1 e2) then show ?case by simp
qed
text ‹
Monotonicity companion to ‹afilter_pair_sound›: the same two-operand
filtering step, once ‹inv_less›/‹inv_eq›/‹inv_plus›/... has narrowed the
operand pair monotonically, is itself monotone in both the narrowed pair
and the incoming state. Stated generically here from the completed
‹afilter_mono›, so it cannot help ‹afilter_mono›'s own Plus/Minus/Times
cases -- ‹afilter_mono› is still mid-induction when they run -- but lets
later clients such as ‹bfilter_mono›'s Less/Eq cases apply it directly
instead of repeating this chaining.
›
lemma afilter_pair_mono [intro]:
assumes fst: "fst p1 ≤ fst p2" and snd: "snd p1 ≤ snd p2" and st: "d1 ≤ d2"
shows "afilter e1 (fst p1) (afilter e2 (snd p1) d1)
≤ afilter e1 (fst p2) (afilter e2 (snd p2) d2)"
proof -
have inner: "afilter e2 (snd p1) d1 ≤ afilter e2 (snd p2) d2"
by (rule afilter_mono[OF snd st])
show ?thesis by (rule afilter_mono[OF fst inner])
qed
text ‹
Monotonicity companion to ‹bfilter_default_sound›: the same ‹inv_eq›-
against-‹0› reduction is monotone in ‹d›, following directly from
‹aval_abs_mono›, ‹inv_eq_mono›, and ‹afilter_mono›.
›
lemma bfilter_default_mono:
assumes "d1 ≤ d2"
shows "afilter e (fst (inv_eq (¬ res) (⟦e⟧⇧♯ d1) (⟦N 0⟧⇧♯ d1))) d1
≤ afilter e (fst (inv_eq (¬ res) (⟦e⟧⇧♯ d2) (⟦N 0⟧⇧♯ d2))) d2"
proof -
have v1: "⟦e⟧⇧♯ d1 ≤ ⟦e⟧⇧♯ d2" by (rule aval_abs_mono[OF assms])
have v0: "⟦N 0⟧⇧♯ d1 ≤ ⟦N 0⟧⇧♯ d2" by (rule aval_abs_mono[OF assms])
have iv: "fst (inv_eq (¬ res) (⟦e⟧⇧♯ d1) (⟦N 0⟧⇧♯ d1))
≤ fst (inv_eq (¬ res) (⟦e⟧⇧♯ d2) (⟦N 0⟧⇧♯ d2))"
using inv_eq_mono[OF v1 v0] by simp
show ?thesis by (rule afilter_mono[OF iv assms])
qed
text ‹
The forward gate is monotone in the direction its call sites need: a state
whose forward value already rules the selected polarity out cannot become
feasible by shrinking. ‹is_empty_antimono› settles the bottom case and
‹tobool_mono› the definite-answer case. ‹tobool_mono› explicitly excludes
bottom operands -- an author's ‹tobool› may answer arbitrarily there, since
‹gamma bot = {}› makes every answer vacuously sound -- which is why
‹feasible› tests ‹is_empty› first rather than relying on ‹tobool› to agree
across a bottom/non-bottom pair.
›
lemma feasible_mono:
assumes "sigma1 ≤ sigma2" and "feasible e pol sigma1"
shows "feasible e pol sigma2"
proof -
have v: "⟦e⟧⇧♯ sigma1 ≤ ⟦e⟧⇧♯ sigma2" by (rule aval_abs_mono[OF assms(1)])
have nb1: "¬ is_empty (⟦e⟧⇧♯ sigma1)" using assms(2) by (simp add: feasible_def)
have nb2: "¬ is_empty (⟦e⟧⇧♯ sigma2)" using nb1 is_empty_antimono[OF v] by blast
have "tobool (⟦e⟧⇧♯ sigma2) ≠ Some (¬ pol)"
proof
assume "tobool (⟦e⟧⇧♯ sigma2) = Some (¬ pol)"
then have "tobool (⟦e⟧⇧♯ sigma1) = Some (¬ pol)"
using tobool_mono[OF nb1 v] by simp
then show False using assms(2) by (simp add: feasible_def)
qed
with nb2 show ?thesis by (simp add: feasible_def)
qed
text ‹
‹bfilter›'s two join cases test ‹feasible› and fall back to ‹bot› on
failure; ‹bfilter_lifted›'s corresponding cases do the same against
‹Bot›. Both reduce to this one order fact, generic in the carrier: a
monotone guard together with a monotone payload keeps the whole
if-then-else monotone.
›
lemma if_bot_mono:
fixes x y :: "'b::order_bot"
assumes pq: "p ⟹ q"
and xy: "x ≤ y"
shows "(if p then x else bot) ≤ (if q then y else bot)"
using assms by auto
text ‹
Monotonicity of the feasibility-gated join ‹bfilter›'s two join cases
compute. An infeasible disjunct contributes ‹bot›, which is below
everything; a feasible one stays feasible in the larger state, and the
recursive monotonicity fact carries through unchanged.
›
lemma gated_join_mono:
assumes "sigma1 ≤ sigma2"
and "bfilter b1 pol sigma1 ≤ bfilter b1 pol sigma2"
and "bfilter b2 pol sigma1 ≤ bfilter b2 pol sigma2"
shows "(if feasible b1 pol sigma1 then bfilter b1 pol sigma1 else bot)
⊔ (if feasible b2 pol sigma1 then bfilter b2 pol sigma1 else bot)
≤ (if feasible b1 pol sigma2 then bfilter b1 pol sigma2 else bot)
⊔ (if feasible b2 pol sigma2 then bfilter b2 pol sigma2 else bot)"
by (intro sup_mono if_bot_mono feasible_mono[OF assms(1)] assms(2,3))
lemma bfilter_mono:
"d1 ≤ d2 ⟹ bfilter b res d1 ≤ bfilter b res d2"
proof (induction b arbitrary: res d1 d2)
case (Not b) show ?case unfolding bfilter.simps by (rule Not.IH[OF Not.prems])
next
case (And b1 b2)
show ?case
proof (cases res)
case True
have c: "bfilter b2 True d1 ≤ bfilter b2 True d2" by (rule And.IH(2)[OF And.prems])
have "bfilter b1 True (bfilter b2 True d1) ≤ bfilter b1 True (bfilter b2 True d2)"
by (rule And.IH(1)[OF c])
thus ?thesis using True by simp
next
case False
then have res: "res = False" by simp
show ?thesis
unfolding res bfilter.simps
by (rule gated_join_mono[OF And.prems And.IH[OF And.prems]])
qed
next
case (Or b1 b2)
show ?case
proof (cases res)
case True
then have res: "res = True" by simp
show ?thesis
unfolding res bfilter.simps
by (rule gated_join_mono[OF Or.prems Or.IH[OF Or.prems]])
next
case False
have c: "bfilter b2 False d1 ≤ bfilter b2 False d2" by (rule Or.IH(2)[OF Or.prems])
have "bfilter b1 False (bfilter b2 False d1) ≤ bfilter b1 False (bfilter b2 False d2)"
by (rule Or.IH(1)[OF c])
thus ?thesis using False by simp
qed
next
case (Less e1 e2)
have v1: "⟦e1⟧⇧♯ d1 ≤ ⟦e1⟧⇧♯ d2" and v2: "⟦e2⟧⇧♯ d1 ≤ ⟦e2⟧⇧♯ d2"
using aval_abs_mono[OF Less.prems] by simp_all
show ?case unfolding bfilter_Less_unfold
by (rule afilter_pair_mono[OF inv_less_mono_fst[OF v1 v2] inv_less_mono_snd[OF v1 v2]
Less.prems])
next
case (GreaterEq e1 e2)
have v1: "⟦e1⟧⇧♯ d1 ≤ ⟦e1⟧⇧♯ d2" and v2: "⟦e2⟧⇧♯ d1 ≤ ⟦e2⟧⇧♯ d2"
using aval_abs_mono[OF GreaterEq.prems] by simp_all
show ?case unfolding bfilter_GreaterEq_unfold
by (rule afilter_pair_mono[OF inv_less_mono_fst[OF v1 v2] inv_less_mono_snd[OF v1 v2]
GreaterEq.prems])
next
case (Greater e1 e2)
have v1: "⟦e1⟧⇧♯ d1 ≤ ⟦e1⟧⇧♯ d2" and v2: "⟦e2⟧⇧♯ d1 ≤ ⟦e2⟧⇧♯ d2"
using aval_abs_mono[OF Greater.prems] by simp_all
show ?case unfolding bfilter_Greater_unfold
by (rule afilter_pair_mono[OF inv_less_mono_fst[OF v2 v1] inv_less_mono_snd[OF v2 v1]
Greater.prems])
next
case (LessEq e1 e2)
have v1: "⟦e1⟧⇧♯ d1 ≤ ⟦e1⟧⇧♯ d2" and v2: "⟦e2⟧⇧♯ d1 ≤ ⟦e2⟧⇧♯ d2"
using aval_abs_mono[OF LessEq.prems] by simp_all
show ?case unfolding bfilter_LessEq_unfold
by (rule afilter_pair_mono[OF inv_less_mono_fst[OF v2 v1] inv_less_mono_snd[OF v2 v1]
LessEq.prems])
next
case (Eq e1 e2)
have v1: "⟦e1⟧⇧♯ d1 ≤ ⟦e1⟧⇧♯ d2" and v2: "⟦e2⟧⇧♯ d1 ≤ ⟦e2⟧⇧♯ d2"
using aval_abs_mono[OF Eq.prems] by simp_all
show ?case unfolding bfilter_Eq_unfold
by (rule afilter_pair_mono[OF inv_eq_mono_fst[OF v1 v2] inv_eq_mono_snd[OF v1 v2] Eq.prems])
next
case (NotEq e1 e2)
have v1: "⟦e1⟧⇧♯ d1 ≤ ⟦e1⟧⇧♯ d2" and v2: "⟦e2⟧⇧♯ d1 ≤ ⟦e2⟧⇧♯ d2"
using aval_abs_mono[OF NotEq.prems] by simp_all
show ?case unfolding bfilter_NotEq_unfold
by (rule afilter_pair_mono[OF inv_eq_mono_fst[OF v1 v2] inv_eq_mono_snd[OF v1 v2] NotEq.prems])
qed (simp_all only: bfilter.simps Let_def case_prod_beta bfilter_default_mono)
text ‹
‹bfilter_lifted›'s atomic shapes reduce to ‹bfilter_mono› lifted
through \<^const>‹normalize_lift›; the sequential ‹And›/‹Or› cases lift
@{const bind_lift}'s own premise (case ‹Bot› is trivial, case ‹Lifted› is
the head recursion's own monotonicity fact), and the join cases are
‹gated_join_mono› restated against \<^const>‹Bot›.
›
lemma gated_join_lifted_mono:
assumes "sigma1 ≤ sigma2"
and "bfilter_lifted b1 pol sigma1 ≤ bfilter_lifted b1 pol sigma2"
and "bfilter_lifted b2 pol sigma1 ≤ bfilter_lifted b2 pol sigma2"
shows "(if feasible b1 pol sigma1 then bfilter_lifted b1 pol sigma1 else Bot)
⊔ (if feasible b2 pol sigma1 then bfilter_lifted b2 pol sigma1 else Bot)
≤ (if feasible b1 pol sigma2 then bfilter_lifted b1 pol sigma2 else Bot)
⊔ (if feasible b2 pol sigma2 then bfilter_lifted b2 pol sigma2 else Bot)"
unfolding bot_lifted_eq[symmetric]
by (intro sup_mono if_bot_mono feasible_mono[OF assms(1)] assms(2,3))
lemma bfilter_lifted_mono:
"sigma1 ≤ sigma2 ⟹ bfilter_lifted e pol sigma1 ≤ bfilter_lifted e pol sigma2"
proof (induction e arbitrary: pol sigma1 sigma2)
case (And b1 b2)
show ?case
proof (cases pol)
case True
have step: "bfilter_lifted b2 True sigma1 ≤ bfilter_lifted b2 True sigma2"
by (rule And.IH(2)[OF And.prems])
have ih1: "⋀a b. a ≤ b ⟹ bfilter_lifted b1 True a ≤ bfilter_lifted b1 True b"
using And.IH(1) by simp
show ?thesis using True by (simp add: bind_lift_mono2[OF step ih1])
next
case False
then have pol: "pol = False" by simp
show ?thesis
unfolding pol bfilter_lifted.simps
by (rule gated_join_lifted_mono[OF And.prems And.IH[OF And.prems]])
qed
next
case (Or b1 b2)
show ?case
proof (cases pol)
case True
then have pol: "pol = True" by simp
show ?thesis
unfolding pol bfilter_lifted.simps
by (rule gated_join_lifted_mono[OF Or.prems Or.IH[OF Or.prems]])
next
case False
have step: "bfilter_lifted b2 False sigma1 ≤ bfilter_lifted b2 False sigma2"
by (rule Or.IH(2)[OF Or.prems])
have ih1: "⋀a b. a ≤ b ⟹ bfilter_lifted b1 False a ≤ bfilter_lifted b1 False b"
using Or.IH(1) by simp
show ?thesis using False by (simp add: bind_lift_mono2[OF step ih1])
qed
qed (simp_all only: bfilter_lifted.simps normalize_state_lift_mono bfilter_mono)
lemma branch_lifted_mono:
assumes "sigma1 ≤ sigma2"
shows "branch_lifted e pol sigma1 ≤ branch_lifted e pol sigma2"
proof (cases "feasible e pol sigma1")
case True
have "feasible e pol sigma2" by (rule feasible_mono[OF assms True])
with True assms show ?thesis
unfolding branch_lifted_def by (simp add: bfilter_lifted_mono)
next
case False
then show ?thesis unfolding branch_lifted_def by simp
qed
lemma branch_mono:
assumes "sigma1 ≤ sigma2"
shows "branch e pol sigma1 ≤ branch e pol sigma2"
unfolding branch_def
by (rule collapse_lift_mono[OF branch_lifted_mono[OF assms]])
text ‹
‹bfilter_lifted› only ever narrows further than raw ‹bfilter›: each leaf
either falls through to ‹bfilter› unchanged or short-circuits to ‹Bot›,
and every ‹And›/‹Or› recursion step preserves that ordering by
‹bfilter_lifted_mono›. ‹branch_le_bfilter› transports this to the
collapsed carrier: callers that only need an upper bound on ‹branch›'s
result -- e.g. post-fixpoint checks -- can reuse their existing
‹bfilter›-level reasoning through it instead of re-deriving one against
‹branch›'s definition.
›
lemma gated_join_lifted_le_raw:
fixes y1 y2 :: "'a abs_state"
assumes "x1 ≤ Lifted y1" and "x2 ≤ Lifted y2"
shows "(if p1 then x1 else Bot) ⊔ (if p2 then x2 else Bot)
≤ Lifted ((if p1 then y1 else bot) ⊔ (if p2 then y2 else bot))"
using assms sup_mono[OF assms] by (cases p1; cases p2) simp_all
lemma bfilter_lifted_le_raw: "bfilter_lifted e pol sigma ≤ Lifted (bfilter e pol sigma)"
proof (induction e arbitrary: pol sigma)
case (And b1 b2)
show ?case
proof (cases pol)
case True
show ?thesis
proof (cases "bfilter_lifted b2 True sigma")
case Bot
then show ?thesis using True by simp
next
case (Lifted t)
have le_t: "t ≤ bfilter b2 True sigma"
using And.IH(2)[of True sigma] Lifted by simp
have "bfilter_lifted b1 True t ≤ bfilter_lifted b1 True (bfilter b2 True sigma)"
by (rule bfilter_lifted_mono[OF le_t])
also have "… ≤ Lifted (bfilter b1 True (bfilter b2 True sigma))"
using And.IH(1)[of True "bfilter b2 True sigma"] by simp
finally show ?thesis using True Lifted by simp
qed
next
case False
then have pol: "pol = False" by simp
show ?thesis
unfolding pol bfilter_lifted.simps bfilter.simps
by (rule gated_join_lifted_le_raw[OF And.IH])
qed
next
case (Or b1 b2)
show ?case
proof (cases pol)
case True
then have pol: "pol = True" by simp
show ?thesis
unfolding pol bfilter_lifted.simps bfilter.simps
by (rule gated_join_lifted_le_raw[OF Or.IH])
next
case False
show ?thesis
proof (cases "bfilter_lifted b2 False sigma")
case Bot
then show ?thesis using False by simp
next
case (Lifted t)
have le_t: "t ≤ bfilter b2 False sigma"
using Or.IH(2)[of False sigma] Lifted by simp
have "bfilter_lifted b1 False t ≤ bfilter_lifted b1 False (bfilter b2 False sigma)"
by (rule bfilter_lifted_mono[OF le_t])
also have "… ≤ Lifted (bfilter b1 False (bfilter b2 False sigma))"
using Or.IH(1)[of False "bfilter b2 False sigma"] by simp
finally show ?thesis using False Lifted by simp
qed
qed
qed (simp_all add: normalize_lift_def)
lemma branch_lifted_le_raw: "branch_lifted e pol sigma ≤ Lifted (bfilter e pol sigma)"
unfolding branch_lifted_def
by (cases "feasible e pol sigma") (simp_all add: bfilter_lifted_le_raw)
lemma branch_le_bfilter: "branch e pol sigma ≤ bfilter e pol sigma"
unfolding branch_def
using collapse_lift_mono[OF branch_lifted_le_raw] by simp
end
end