Theory Voblint_Domain.Reachability_Lift

theory Reachability_Lift
  imports State_Concretization "HOL-Library.Monad_Syntax"
begin

section ‹Explicit reachability over an abstract carrier›

text ‹
  The outer ‹Bot› represents an unreachable control-flow point; ‹Lifted a›
  represents a reachable point carrying ‹a›. The construction provides the
  order, joins, solver updates, concretization, and normalized transfer
  combinators independently of any particular abstract-state representation.
›

text ‹
  Mirrors Goblint's lifted-domain construction
  (@{url ‹https://github.com/goblint/analyzer/blob/master/src/framework/analyses.ml›}):
  ‹module Dom (LD: Lattice.S) = struct include Lattice.LiftConf (...) (LD) ... end›, whose
  outer ‹`Bot› means dead code and whose ‹unlift› only accepts ‹`Lifted x›. Reachability is
  carried as an explicit tag on top of the analysis-local state, not rediscovered from the
  state's own contents. ‹Bot› mirrors Goblint's lifted ‹`Bot›; ‹Lifted› mirrors ‹`Lifted›.
  Goblint's lift also carries an outer ‹`Top›, but not merely as a substitute for a missing
  payload ‹top›: ‹Lattice.LiftConf›'s ‹join›/‹widen› fall back to ‹`Top› whenever the base
  domain's own ‹join›/‹widen› raises ‹TopValue› or ‹Uncomparable›, i.e. whenever the base
  domain is partial enough that two of its values have no expressible join, and ‹unlift›
  rejects ‹`Top› exactly like ‹`Bot›. Every @{class numeric_domain} instance here is instead a
  total ‹bounded_semilattice_sup_bot› with its own ‹top›: ‹⊔› and ‹∇› always return a value,
  so a lifted operation here can never fail the way Goblint's can, and ‹Lifted top› already
  says everything an outer ‹`Top› would. This lift therefore stays two-valued. At the raw
  lifted representation, ‹Bot› is strictly below every ‹Lifted a›
  regardless of ‹a› -- including ‹Lifted bot›, which remains distinct from ‹Bot› even
  though ‹a› is itself locally bottom -- since dead-by-construction and
  reachable-but-locally-bottom are the two concepts this lift exists to keep separate. The
  normalization discipline developed below (‹normalize_lift›, ‹normalized_lift›) then
  layers a stronger, Voblint-specific invariant on top: every solver-facing payload an
  arbitrary caller-supplied predicate ‹empty_pred› classifies as bottom is additionally
  canonicalized to structural ‹Bot›, so ‹Lifted a› with an ‹empty_pred›-bottom ‹a› never
  actually escapes a value-producing step in practice, even though the raw datatype and
  order permit it. This theory does not know or assume that ‹empty_pred› means semantic
  emptiness -- ‹Nonrelational_Reachability› is where ‹empty_pred› is instantiated to
  ‹is_empty_state› and proved to coincide with an empty concretization.
›

subsection ‹The lifted order and lattice structure›

(* Disable Quickcheck's narrowing plugin because its generated narrowing
   arity collides with the vendored TD solver's class of the same name.
   This affects only Quickcheck infrastructure. *)
datatype (plugins del: quickcheck_narrowing) 'a lifted =
  Bot | Lifted 'a

text ‹
  The vendored TD solver stores values at sort ‹bounded_semilattice_sup_bot›
  (@{theory_text ‹TD_side›}'s ‹T :: ('x,'g,'d::bounded_semilattice_sup_bot) eqsT›),
  so ‹lifted› instantiates that combined structure directly in one step --
  order, bottom, and join together -- rather than building it up through the
  three separate parent classes (‹order›, ‹bot›, ‹semilattice_sup›) and
  bridging them with intermediate ‹instance› declarations. This intentionally
  gives up the weaker standalone arities that instantiating each parent
  separately would have provided (‹'a::type ⇒ 'a lifted :: bot› and
  ‹'a::order ⇒ 'a lifted :: order›), for an arbitrary or merely ordered
  payload; consequently the generic lifted lemmas below (‹gamma_lift_mono›,
  ‹map_lift_mono›, ‹normalize_lift_mono›, ‹transfer_lift_mono›,
  ‹transfer_lift2_mono›) and the standalone widening/narrowing instances are
  stated at ‹semilattice_sup› as well. A caller that only needs the weak
  standalone ‹bot› arity does not automatically satisfy this, and has to
  restate at the sort its real call sites already require.
›

instantiation lifted :: (semilattice_sup) bounded_semilattice_sup_bot
begin

fun less_eq_lifted :: "'a lifted ⇒ 'a lifted ⇒ bool" where
    "less_eq_lifted Bot _ = True"
  | "less_eq_lifted (Lifted _) Bot = False"
  | "less_eq_lifted (Lifted a) (Lifted b) = (a ≤ b)"

definition less_lifted :: "'a lifted ⇒ 'a lifted ⇒ bool" where
  "less_lifted x y = (x ≤ y ∧ ¬ y ≤ x)"

definition bot_lifted :: "'a lifted" where "bot_lifted = Bot"

fun sup_lifted :: "'a lifted ⇒ 'a lifted ⇒ 'a lifted" where
    "sup_lifted Bot y = y"
  | "sup_lifted x Bot = x"
  | "sup_lifted (Lifted a) (Lifted b) = Lifted (a ⊔ b)"

instance
proof intro_classes
  fix x y z :: "'a lifted"
  show "(x < y) = (x ≤ y ∧ ¬ y ≤ x)" unfolding less_lifted_def by (rule refl)
  show "x ≤ x" by (cases x) simp_all
  show "x ≤ y ⟹ y ≤ z ⟹ x ≤ z" by (cases x; cases y; cases z) simp_all
  show "x ≤ y ⟹ y ≤ x ⟹ x = y" by (cases x; cases y) simp_all
  show "x ≤ x ⊔ y" by (cases x; cases y) simp_all
  show "y ≤ x ⊔ y" by (cases x; cases y) simp_all
  show "y ≤ x ⟹ z ≤ x ⟹ y ⊔ z ≤ x" by (cases x; cases y; cases z) simp_all
  show "bot ≤ x" by (cases x) (simp_all add: bot_lifted_def)
qed

end

lemma bot_lifted_eq [simp]: "(bot :: 'a::semilattice_sup lifted) = Bot"
  unfolding bot_lifted_def by (rule refl)

text ‹
  The warrowing update rule needs \<^typ>‹'a lifted› itself to carry ‹widen›/‹narrow› once the
  executable trees it runs store a lifted payload. ‹Bot› keeps the same role here as in the
  ‹sup› instance above: a structural placeholder, neutral for ‹widen›/‹narrow› against a
  ‹Lifted› operand, with only the ‹Lifted›/‹Lifted› case deferring to the base domain's own
  operation. ‹quickcheck_narrowing› is disabled on the ‹lifted› datatype declaration above:
  Isabelle/HOL's own built-in ‹narrowing› class (for Quickcheck's narrowing-based counterexample
  search) collides with the vendored solver's ‹narrowing› class of the same base name, and the
  datatype package's default Quickcheck plugin registers an arity for ‹lifted› under that
  colliding name before this instantiation gets a chance to.
›

instantiation lifted :: ("{semilattice_sup,widening}") widening
begin

fun widen_lifted :: "'a lifted ⇒ 'a lifted ⇒ 'a lifted" where
  "widen_lifted Bot y = y"
| "widen_lifted x Bot = x"
| "widen_lifted (Lifted a) (Lifted b) = Lifted (a ∇ b)"

instance proof intro_classes
  fix x y :: "'a lifted"
  show "x ≤ x ∇ y" by (cases x; cases y) (simp_all add: widen_ge1)
  show "y ≤ x ∇ y" by (cases x; cases y) (simp_all add: widen_ge2)
qed

end

instantiation lifted :: ("{semilattice_sup,narrowing}") narrowing
begin

fun narrow_lifted :: "'a lifted ⇒ 'a lifted ⇒ 'a lifted" where
  "narrow_lifted Bot y = Bot"
| "narrow_lifted (Lifted a) Bot = Bot"
| "narrow_lifted (Lifted a) (Lifted b) = Lifted (a Δ b)"

instance proof intro_classes
  fix a b :: "'a lifted"
  show "b ≤ a ⟹ b ≤ a Δ b"
    by (cases a; cases b) (simp_all add: narrow_ge)
  show "b ≤ a ⟹ a Δ b ≤ a"
    by (cases a; cases b) (simp_all add: narrow_le)
qed

end


subsection ‹Generic concretization›

text ‹Reading a lifted value back: \<^term>‹Bot› denotes no state at all, so it concretizes to
  the empty set rather than to whatever the underlying domain's own bottom denotes.  That
  difference is the whole point of the lift -- an unreachable point and a point whose every
  coordinate is bottom are distinguishable here, and only the former is empty by
  construction.›
definition gamma_lift :: "('a ⇒ 'b set) ⇒ 'a lifted ⇒ 'b set" where
  "gamma_lift gam x = (case x of Bot ⇒ {} | Lifted a ⇒ gam a)"

lemma gamma_lift_Bot [simp]: "gamma_lift gam Bot = {}"
  unfolding gamma_lift_def by simp

lemma gamma_lift_Lifted [simp]: "gamma_lift gam (Lifted a) = gam a"
  unfolding gamma_lift_def by simp


lemma gamma_lift_mono:
  fixes x y :: "'a::semilattice_sup lifted"
  assumes gam_mono: "⋀a b. a ≤ b ⟹ gam a ⊆ gam b"
    and le: "x ≤ y"
  shows "gamma_lift gam x ⊆ gamma_lift gam y"
  using le by (cases x; cases y) (auto simp: gam_mono)

text ‹
  ‹gamma_liftE› recovers the ‹Lifted› payload a lifted membership witnesses:
  ‹Bot› concretizes to ‹{}›, so any ‹s ∈ gamma_lift gam x› already forces
  ‹x = Lifted a› for some ‹a› with ‹s ∈ gam a›. Named as an eliminator
  because its witness is exactly this structural case split, replacing the
  repeated manual ‹obtain ... where "... = Lifted ..." "s ∈ ..." by (cases
  ...) auto› pattern with one rule application.
›

lemma gamma_liftE [elim]:
  assumes "s ∈ gamma_lift gam x"
  obtains a where "x = Lifted a" and "s ∈ gam a"
  using assms by (cases x) auto

subsection ‹Generic reachability combinators›

text ‹
  ‹bind_lift› is the reachability monad's Kleisli bind, exactly \<^const>‹Option.bind›'s
  shape with ‹Bot› for ‹None› and ‹Lifted› for ‹Some›: ‹Bot› in, ‹Bot› out, without ever
  calling ‹f› -- matching Goblint's ‹unlift› being called before dispatch rather than inside
  each analysis's ‹assign›/‹branch›. ‹map_lift› is its functor counterpart (‹Option.map›'s
  analogue), for pushing a total, never-re-collapsing operation through the lift. Both are
  representation-independent: neither one inspects whether a ‹Lifted› payload happens to be
  semantically empty. That is a separate concern, taken up below in
  ∗‹Canonical-bottom normalization›.
›

fun bind_lift :: "'a lifted ⇒ ('a ⇒ 'b lifted) ⇒ 'b lifted" where
  "bind_lift Bot f = Bot"
| "bind_lift (Lifted a) f = f a"

lemma bind_lift_left_identity: "bind_lift (Lifted a) f = f a" by simp

lemma bind_lift_right_identity [simp]: "bind_lift x Lifted = x"
  by (cases x) simp_all

text ‹
  ‹gamma_lift_bindI› follows ‹bind_lift›'s own structure: a witness for ‹xs›
  together with a step that carries any such witness through ‹f› gives a
  witness for the bind. Targets the sequential ‹And›/‹Or› recursions that
  chain one filtering step's result into the next, replacing their manual
  ‹obtain d' where "... = Lifted d'" "s ∈ ..."› destructuring with one
  ‹cases›-driven rule.
›

lemma gamma_lift_bindI [intro]:
  assumes xs: "s ∈ gamma_lift gam xs"
      and step: "⋀a. s ∈ gam a ⟹ s ∈ gamma_lift gam' (f a)"
  shows "s ∈ gamma_lift gam' (bind_lift xs f)"
  using xs by (cases xs) (auto intro: step)

text ‹
  Registers \<^const>‹bind_lift› under \<^const>‹Monad_Syntax.bind›'s ad hoc overloading, so
  ‹x >>= f› and ‹do { a <- x; f a }› both parse to exactly ‹bind_lift x f› -- a pure
  syntax translation resolved at elaboration time, so every lemma about \<^const>‹bind_lift›
  applies unchanged to code written with ‹do› notation. Registered here, immediately after
  \<^const>‹bind_lift›'s definition, so the reachability combinators below can use ‹do›
  notation too.
›

adhoc_overloading Monad_Syntax.bind == bind_lift

definition map_lift :: "('a ⇒ 'b) ⇒ 'a lifted ⇒ 'b lifted" where
  "map_lift f x = do { a <- x; Lifted (f a) }"

lemma map_lift_Bot [simp]: "map_lift f Bot = Bot"
  unfolding map_lift_def by simp

lemma map_lift_Lifted [simp]: "map_lift f (Lifted a) = Lifted (f a)"
  unfolding map_lift_def by simp

text ‹‹map_lift› never invents or destroys the dead point, so the two carriers agree
  on the coarsest bottom test there is.›

lemma map_lift_eq_Bot_iff [simp]: "map_lift f x = Bot ⟷ x = Bot"
  by (cases x) simp_all

lemma map_lift_mono:
  fixes x y :: "'a::semilattice_sup lifted"
  assumes f_mono: "⋀a b. a ≤ b ⟹ f a ≤ (f b :: 'b::semilattice_sup)"
    and le: "x ≤ y"
  shows "map_lift f x ≤ map_lift f y"
  using le by (cases x; cases y) (auto simp: f_mono)

lemma map_lift_sup:
  fixes x y :: "'a::semilattice_sup lifted"
  assumes f_sup: "⋀a b. f (a ⊔ b) = (f a ⊔ f b :: 'b::semilattice_sup)"
  shows "map_lift f (x ⊔ y) = map_lift f x ⊔ map_lift f y"
  by (cases x; cases y) (simp_all add: f_sup)

lemma map_lift_id [simp]: "map_lift id x = x"
  by (cases x) simp_all

lemma map_lift_comp [simp]: "map_lift g (map_lift f x) = map_lift (g ∘ f) x"
  by (cases x) simp_all

subsection ‹Collapsing back to the plain, bot-carrying type›

text ‹
  ‹collapse_lift› goes the opposite direction from ‹normalize_lift›: where
  ‹normalize_lift› turns a domain-produced witness-bottom value into
  structural ‹Bot›, ‹collapse_lift› turns ‹Bot› back into the plain type's
  own ‹bot›, so a caller whose interface only has room for the plain type
  -- not the ‹lifted› wrapper -- can still receive a more precise lifted
  result. Unlike ‹normalize_lift›, no predicate is needed: ‹Bot› already
  says the value is empty, and ‹bot› is exactly the plain type's own
  representative of that.
›

fun collapse_lift :: "'a::bot lifted ⇒ 'a" where
    "collapse_lift Bot = bot"
  | "collapse_lift (Lifted a) = a"

lemma collapse_lift_mono:
  fixes x y :: "'a::bounded_semilattice_sup_bot lifted"
  assumes "x ≤ y"
  shows "collapse_lift x ≤ collapse_lift y"
  using assms by (cases x; cases y) simp_all

text ‹
  The soundness counterpart: a witness against ‹gam› through the lifted
  carrier survives collapsing, since ‹Bot› can only arise when there is no
  witness at all (‹gam bot = {}› rules that reading out).
›

lemma gamma_collapse_lift:
  assumes "s ∈ gamma_lift gam x" and "gam bot = {}"
  shows "s ∈ gam (collapse_lift x)"
  using assms by (cases x) simp_all

text ‹
  ‹collapse_lift› commutes with ‹map_lift f› whenever ‹f› itself sends
  ‹bot› to ‹bot›: both sides land on ‹Bot›'s collapse, ‹bot›, when the
  carrier is ‹Bot›, and agree trivially on ‹Lifted a›. This is what lets the
  map from an executable state to its function (‹f›) be applied either before or after
  collapsing a ‹lifted› result, so a commutation theorem proved for the
  ‹lifted› level transports to the collapsed, plain-type level for free.
›

lemma collapse_lift_map_lift:
  assumes "f bot = bot"
  shows "collapse_lift (map_lift f x) = f (collapse_lift x)"
  using assms by (cases x) simp_all

subsection ‹Canonical-bottom normalization›

text ‹
  ‹normalize_lift› is the one Voblint-specific piece on top of the generic combinators
  above: it turns a domain-produced witness-bottom raw result back into the canonical
  structural ‹Bot›, the counterpart of Goblint's transfer functions raising ‹Deadcode›
  when their own computation lands on bottom. ‹transfer_lift›/‹transfer_lift2› compose
  ‹bind_lift› with ‹normalize_lift›: the shape every generic edge/combine dispatcher
  actually calls.
›

definition normalize_lift :: "('a ⇒ bool) ⇒ 'a ⇒ 'a lifted" where
  "normalize_lift empty_pred a = (if empty_pred a then Bot else Lifted a)"

lemma normalize_lift_bot [simp]: "empty_pred a ⟹ normalize_lift empty_pred a = Bot"
  unfolding normalize_lift_def by simp

lemma normalize_lift_not_bot [simp]:
  "¬ empty_pred a ⟹ normalize_lift empty_pred a = Lifted a"
  unfolding normalize_lift_def by simp

text ‹
  When ‹empty_pred› exactly tracks ‹gam›'s own emptiness, normalizing never
  changes what a payload concretizes to: the ‹if› only chooses between
  ‹gam a› and ‹{}›, and those coincide exactly when ‹empty_pred a› does.
  This is the generic fact every ‹gamma_*_lift› correctness statement
  (‹Nonrelational_Reachability›'s ‹is_empty_state_lift_iff›) reduces to, once
  ‹empty_pred›'s own iff-correctness is in hand.
›

lemma gamma_normalize_lift:
  assumes "empty_pred a ⟷ gam a = {}"
  shows "gamma_lift gam (normalize_lift empty_pred a) = gam a"
  using assms unfolding normalize_lift_def by auto

definition transfer_lift ::
  "('b ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ 'a lifted ⇒ 'b lifted" where
  "transfer_lift empty_pred f x = do { a <- x; normalize_lift empty_pred (f a) }"

definition transfer_lift2 ::
  "('c ⇒ bool) ⇒ ('a ⇒ 'b ⇒ 'c) ⇒ 'a lifted ⇒ 'b lifted ⇒ 'c lifted" where
  "transfer_lift2 empty_pred f x y =
     do { a <- x; b <- y; normalize_lift empty_pred (f a b) }"

lemma transfer_lift_Bot [simp]: "transfer_lift empty_pred f Bot = Bot"
  unfolding transfer_lift_def by simp

lemma transfer_lift_Lifted [simp]:
  "transfer_lift empty_pred f (Lifted a) = normalize_lift empty_pred (f a)"
  unfolding transfer_lift_def by simp

lemma transfer_lift2_Bot_left [simp]: "transfer_lift2 empty_pred f Bot y = Bot"
  unfolding transfer_lift2_def by simp

lemma transfer_lift2_Bot_right [simp]: "transfer_lift2 empty_pred f (Lifted a) Bot = Bot"
  unfolding transfer_lift2_def by simp

lemma transfer_lift2_Lifted [simp]:
  "transfer_lift2 empty_pred f (Lifted a) (Lifted b) = normalize_lift empty_pred (f a b)"
  unfolding transfer_lift2_def by simp

text ‹
  ‹normalized_lift› names the discipline every solver-facing lifted value is meant to
  keep: \<^const>‹Bot› is the ∗‹sole› representation this construction lets a caller-supplied
  ‹empty_pred› classification collapse to -- a \<^const>‹Lifted› payload ‹empty_pred› still
  calls bottom is a
  representation the framework never lets escape a value-producing step, not a second,
  competing way to say the same thing. ‹normalize_lift›'s own ‹if› makes every one of
  its outputs self-normalized: the \<^const>‹Lifted› branch only fires when ‹empty_pred›
  already said no. ‹transfer_lift›/‹transfer_lift2› route every domain transfer step
  through exactly this ‹if›, so no transfer step can ever hand back a \<^const>‹Lifted›
  payload ‹empty_pred› still calls bottom, regardless of what the pre-lift inputs
  looked like.

  The lemmas below extend this from a single transfer step to every other value-producing
  primitive a solver combines lifted values with: ‹⊔› (joining several contributions at a
  program point) and ‹∇Δ› (the warrowing update rule). Both need only that ‹empty_pred›
  itself is downward closed under the payload's order (‹mono› below) -- exactly
  ‹is_empty_antimono›'s shape at \<^class>‹numeric_domain›, or ‹default_st_is_bot_for›'s own
  monotonicity once bridged through ‹default_st_to_fun_mono› -- not any fact
  specific to how ‹empty_pred› itself is computed.
›

definition normalized_lift :: "('a ⇒ bool) ⇒ 'a lifted ⇒ bool" where
  "normalized_lift empty_pred x = (case x of Bot ⇒ True | Lifted a ⇒ ¬ empty_pred a)"

lemma normalized_lift_Bot [simp]: "normalized_lift empty_pred Bot"
  unfolding normalized_lift_def by simp

lemma normalized_lift_Lifted [simp]:
  "normalized_lift empty_pred (Lifted a) ⟷ ¬ empty_pred a"
  unfolding normalized_lift_def by simp

lemma normalize_lift_normalized [simp]:
  "normalized_lift empty_pred (normalize_lift empty_pred a)"
  unfolding normalize_lift_def by (cases "empty_pred a") simp_all

lemma transfer_lift_normalized [simp]:
  "normalized_lift empty_pred (transfer_lift empty_pred f x)"
  by (cases x) (simp_all add: transfer_lift_def)

lemma transfer_lift2_normalized [simp]:
  "normalized_lift empty_pred (transfer_lift2 empty_pred f x y)"
  by (cases x; cases y) (simp_all add: transfer_lift2_def)

text ‹
  ‹canonicalize_lift› re-normalizes an already-lifted value against ‹empty_pred›: a
  \<^const>‹Lifted› payload that has since become witness-bottom (e.g. read from a
  representation that does not itself carry the ‹transfer_lift› discipline) collapses
  to \<^const>‹Bot›, exactly as if it had been produced by a transfer step in the first
  place. It is ‹transfer_lift empty_pred id›, not a new bottom test: reusing
  \<^const>‹transfer_lift› at the identity function is what makes
  ‹canonicalize_lift_normalized› immediate from ‹transfer_lift_normalized› rather than
  a second proof of the same fact.
›

definition canonicalize_lift :: "('a ⇒ bool) ⇒ 'a lifted ⇒ 'a lifted" where
  "canonicalize_lift empty_pred = transfer_lift empty_pred id"

lemma canonicalize_lift_Bot [simp]: "canonicalize_lift empty_pred Bot = Bot"
  unfolding canonicalize_lift_def by simp

lemma canonicalize_lift_Lifted [simp]:
  "canonicalize_lift empty_pred (Lifted a) = normalize_lift empty_pred a"
  unfolding canonicalize_lift_def by simp

lemma canonicalize_lift_normalized [simp]:
  "normalized_lift empty_pred (canonicalize_lift empty_pred x)"
  unfolding canonicalize_lift_def by (rule transfer_lift_normalized)

text ‹
  Canonicalization is idempotent: a value already collapsed against
  ‹empty_pred› is left unchanged by collapsing it again -- the defining
  property of a normalization operation.
›

lemma canonicalize_lift_idem [simp]:
  "canonicalize_lift empty_pred (canonicalize_lift empty_pred x)
     = canonicalize_lift empty_pred x"
  by (cases x) (auto simp: normalize_lift_def)

text ‹
  ‹⊔› preserves ‹normalized_lift› from two already-normalized operands: \<^const>‹Bot› is
  ‹⊔›'s identity on \<^typ>‹'a lifted› (‹sup_lifted.simps›), so the only case needing
  ‹mono› at all is \<^const>‹Lifted›/\<^const>‹Lifted›, where ‹sup_ge1›/‹sup_ge2› place each
  operand below the join and ‹mono›'s contrapositive carries non-bottomness upward.
›

lemma normalized_lift_sup:
  fixes x y :: "'a::semilattice_sup lifted"
  assumes mono: "⋀a b::'a. a ≤ b ⟹ empty_pred b ⟹ empty_pred a"
    and nx: "normalized_lift empty_pred x"
    and ny: "normalized_lift empty_pred y"
  shows "normalized_lift empty_pred (x ⊔ y)"
  using nx ny by (cases x; cases y) (auto dest: mono[OF sup_ge1] mono[OF sup_ge2])

text ‹
  ‹normalized_lift_bind› lifts a per-payload ‹normalized_lift› guarantee on
  ‹f› through ‹bind_lift›: ‹Bot› is already normalized, and ‹Lifted a› hands
  off to ‹f a›, which the assumption covers uniformly. Left unattributed:
  its premise is a schematic function fact, too broad a shape for automatic
  intro search.
›

lemma normalized_lift_bind:
  assumes "⋀a. normalized_lift empty_pred (f a)"
  shows "normalized_lift empty_pred (bind x f)"
  using assms by (cases x) simp_all

text ‹
  Generic monotonicity for the reachability dispatch, proved once here instead of at every
  instantiation (‹abs_state›, ‹default_st›, ...): whenever the underlying transfer is
  monotone and the bottom predicate is downward closed (as ‹is_empty_state› always is, via
  ‹is_empty_state_antimono›), ‹transfer_lift›/‹transfer_lift2› are monotone.
›

lemma normalize_lift_mono:
  fixes a b :: "'a::semilattice_sup"
  assumes f_le: "a ≤ b"
    and bot_mono: "empty_pred b ⟹ empty_pred a"
  shows "normalize_lift empty_pred a ≤ normalize_lift empty_pred b"
  unfolding normalize_lift_def using f_le bot_mono by auto

lemma transfer_lift_mono:
  fixes x1 x2 :: "'a::semilattice_sup lifted"
  assumes f_mono: "⋀a b. a ≤ b ⟹ f a ≤ f b"
    and bot_mono: "⋀a b. a ≤ b ⟹ empty_pred b ⟹ empty_pred a"
    and le: "x1 ≤ x2"
  shows "transfer_lift empty_pred f x1
           ≤ (transfer_lift empty_pred f x2 :: 'b::semilattice_sup lifted)"
  using assms by (cases x1; cases x2) (auto intro!:normalize_lift_mono)

lemma transfer_lift2_mono:
  fixes x1 x2 :: "'a::semilattice_sup lifted" and y1 y2 :: "'b::semilattice_sup lifted"
  assumes f_mono: "⋀a1 a2 b1 b2. a1 ≤ a2 ⟹ b1 ≤ b2 ⟹ f a1 b1 ≤ f a2 b2"
    and bot_mono: "⋀a b. a ≤ b ⟹ empty_pred b ⟹ empty_pred a"
    and lex: "x1 ≤ x2" and ley: "y1 ≤ y2"
  shows "transfer_lift2 empty_pred f x1 y1
           ≤ (transfer_lift2 empty_pred f x2 y2 :: 'c::semilattice_sup lifted)"
  using assms by (cases x1; cases x2; cases y1; cases y2)
     (auto intro: normalize_lift_mono f_mono bot_mono)

text ‹
  ‹bind_lift›'s own monotonicity: a monotone step function carried through
  a monotone bind argument stays monotone. Left unattributed, like
  ‹normalized_lift_bind›: its ‹f›/‹g› premise is schematic and broader than
  a typical ‹[intro]› shape, so call sites invoke it explicitly.
›

lemma bind_lift_mono2:
  fixes x y :: "'a::semilattice_sup lifted"
  assumes xy: "x ≤ y"
      and fg: "⋀a b. a ≤ b ⟹ f a ≤ (g b :: 'b::semilattice_sup lifted)"
  shows "bind x f ≤ bind y g"
  using xy by (cases x; cases y) (auto intro: fg)

subsection ‹Solver update integration›

text ‹
  The solver's update rules need ‹'d::{bounded_semilattice_sup_bot, warrowing}›.
  \<^typ>‹'a lifted› already carries ‹widening› and ‹narrowing› separately; this
  registers their combination ‹warrowing›, which Isabelle does not derive from
  the two arities by itself.
›

instance lifted :: ("{bounded_semilattice_sup_bot, warrowing}") warrowing ..

subsection ‹Transporting a lifted transfer along a representation map›

text ‹
  A representation map that commutes with the underlying operation, and
  classifies emptiness the same way on both sides, commutes with the whole
  lifted transfer. Stated for \<^const>‹transfer_lift›/\<^const>‹transfer_lift2›
  themselves, so any pair of representations of one domain --- an executable
  carrier and the mathematical one it stands for, say --- gets the fact once
  rather than once per operation that uses it.
›

lemma transfer_lift_commute:
  assumes commute: "⋀s. phi (f s) = F (phi s)"
    and exact: "⋀s. empty_pred s = empty_pred' (phi s)"
  shows "map_lift phi (transfer_lift empty_pred f d) = transfer_lift empty_pred' F (map_lift phi d)"
  by (cases d) (simp_all add: transfer_lift_def normalize_lift_def commute exact)

lemma transfer_lift2_commute:
  assumes commute: "⋀s t. phi (f s t) = F (phi s) (phi t)"
    and exact: "⋀s. empty_pred s = empty_pred' (phi s)"
  shows "map_lift phi (transfer_lift2 empty_pred f d1 d2) =
           transfer_lift2 empty_pred' F (map_lift phi d1) (map_lift phi d2)"
  by (cases d1; cases d2) (simp_all add: transfer_lift2_def normalize_lift_def commute exact)

end