Theory DG_State

theory DG_State
  imports "Voblint_Domain.State_Concretization"
begin

section ‹The value a D/G unknown carries›

text ‹An analysis chooses a flow-sensitive answer domain ‹D› and a
  flow-insensitive side-effect domain ‹G›. The framework keeps them opaque and
  stores them in separate components of ‹dg_state›; it never copies a global
  component into a local answer.

  This theory is that carrier and its order, and nothing else: no address, no
  solver tree, no transfer. Everything above it only projects and repacks the
  two components, which is what makes those constructions independent of the
  concrete domains.›


subsection ‹A lattice copy type for D-times-G unknown values›
text ‹
  The solver's single value type must order local and global halves
  componentwise. Raw pairs cannot: this repository loads
  ‹HOL-Library.Product_Lexorder›, so every ‹'l * 'g› in scope already
  carries the lexicographic order, and a componentwise instance for the same
  type would clash with it. ‹dg_state› is a distinct carrier so that both
  orders can coexist.
›

datatype ('l, 'g) dg_state = DG (dg_local: 'l) (dg_global: 'g)

instantiation dg_state :: (ord, ord) ord
begin

definition less_eq_dg_state :: "('a, 'b) dg_state ⇒ ('a, 'b) dg_state ⇒ bool" where
  "less_eq_dg_state d1 d2 = (dg_local d1 ≤ dg_local d2 ∧ dg_global d1 ≤ dg_global d2)"

definition less_dg_state :: "('a, 'b) dg_state ⇒ ('a, 'b) dg_state ⇒ bool" where
  "less_dg_state d1 d2 = (d1 ≤ d2 ∧ ¬ d2 ≤ d1)"

instance ..

end

instance dg_state :: (order, order) order
proof intro_classes
  fix x y z :: "('a, 'b) dg_state"
  show "x < y ⟷ x ≤ y ∧ ¬ y ≤ x" by (simp add: less_dg_state_def)
  show "x ≤ x" by (simp add: less_eq_dg_state_def)
  show "x ≤ y ⟹ y ≤ z ⟹ x ≤ z"
    by (auto simp: less_eq_dg_state_def intro: order_trans)
  show "x ≤ y ⟹ y ≤ x ⟹ x = y"
    by (auto simp: less_eq_dg_state_def intro: dg_state.expand antisym)
qed

instantiation dg_state :: (semilattice_sup, semilattice_sup) semilattice_sup
begin

definition sup_dg_state :: "('a, 'b) dg_state ⇒ ('a, 'b) dg_state ⇒ ('a, 'b) dg_state" where
  "sup_dg_state d1 d2 = DG (dg_local d1 ⊔ dg_local d2) (dg_global d1 ⊔ dg_global d2)"

instance
  by standard (auto simp: less_eq_dg_state_def sup_dg_state_def)

end

instantiation dg_state :: (order_bot, order_bot) order_bot
begin

definition bot_dg_state :: "('a, 'b) dg_state" where
  "bot_dg_state = DG bot bot"

instance
  by standard (simp add: less_eq_dg_state_def bot_dg_state_def)

end

instance dg_state ::
  (bounded_semilattice_sup_bot, bounded_semilattice_sup_bot) bounded_semilattice_sup_bot ..

subsection ‹Reading the two components back›

text ‹Every construction above this theory projects and repacks, so the four
  projection equations and the constructor comparison are what its proofs
  should meet instead of the instance definitions. The order itself stays
  unfolded: ‹less_eq_dg_state_def› is not a simp rule, because a bound
  between two values that are not both constructor terms reads better as one
  ‹≤› than as a conjunction of two.›

lemma dg_local_sup [simp]:
  fixes x y :: "('a::semilattice_sup, 'b::semilattice_sup) dg_state"
  shows "dg_local (x ⊔ y) = dg_local x ⊔ dg_local y"
  by (simp add: sup_dg_state_def)

lemma dg_global_sup [simp]:
  fixes x y :: "('a::semilattice_sup, 'b::semilattice_sup) dg_state"
  shows "dg_global (x ⊔ y) = dg_global x ⊔ dg_global y"
  by (simp add: sup_dg_state_def)

lemma dg_local_bot [simp]:
  "dg_local (bot :: ('a::order_bot, 'b::order_bot) dg_state) = bot"
  by (simp add: bot_dg_state_def)

lemma dg_global_bot [simp]:
  "dg_global (bot :: ('a::order_bot, 'b::order_bot) dg_state) = bot"
  by (simp add: bot_dg_state_def)

lemma DG_le_DG [simp]:
  fixes d d' :: "'a::ord" and g g' :: "'b::ord"
  shows "DG d g ≤ DG d' g' ⟷ d ≤ d' ∧ g ≤ g'"
  by (simp add: less_eq_dg_state_def)

instantiation dg_state ::
  ("{bounded_semilattice_sup_bot, warrowing}", "{bounded_semilattice_sup_bot, warrowing}") warrowing
begin

definition widen_dg_state ::
  "('a, 'b) dg_state ⇒ ('a, 'b) dg_state ⇒ ('a, 'b) dg_state"
where
  "widen_dg_state a b = DG (dg_local a ∇ dg_local b) (dg_global a ∇ dg_global b)"

definition narrow_dg_state ::
  "('a, 'b) dg_state ⇒ ('a, 'b) dg_state ⇒ ('a, 'b) dg_state"
where
  "narrow_dg_state a b = DG (dg_local a Δ (dg_local b)) (dg_global a Δ (dg_global b))"

instance
  by standard
    (simp_all add: less_eq_dg_state_def widen_dg_state_def narrow_dg_state_def
      narrowing_class.narrow_ge narrowing_class.narrow_le
      widening_class.widen_ge1 widening_class.widen_ge2)

end

end