Theory Local_Spec_Product

theory Local_Spec_Product
  imports "Voblint_Framework.DG_Spec_Sound"
begin

section ‹The product carrier›

text ‹
  Two components run side by side on a pair of states. The pair is a datatype
  and not \<^typ>‹'a × 'b›, for the reason \<^typ>‹('l, 'g) dg_state› is: this
  repository loads ‹HOL-Library.Product_Lexorder›, so raw pairs already carry
  the lexicographic order, and the product needs the componentwise one. Every
  instance below, including the solver's widening and narrowing, is
  componentwise.
›

datatype ('a, 'b) analysis_product = Product (pleft: 'a) (pright: 'b)

instantiation analysis_product :: (ord, ord) ord
begin

definition less_eq_analysis_product ::
  "('a, 'b) analysis_product ⇒ ('a, 'b) analysis_product ⇒ bool" where
  "less_eq_analysis_product p q ⟷ pleft p ≤ pleft q ∧ pright p ≤ pright q"

definition less_analysis_product ::
  "('a, 'b) analysis_product ⇒ ('a, 'b) analysis_product ⇒ bool" where
  "less_analysis_product p q ⟷ p ≤ q ∧ ¬ q ≤ p"

instance ..

end

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

instantiation analysis_product :: (semilattice_sup, semilattice_sup) semilattice_sup
begin

definition sup_analysis_product ::
  "('a, 'b) analysis_product ⇒ ('a, 'b) analysis_product ⇒ ('a, 'b) analysis_product" where
  "sup_analysis_product p q = Product (pleft p ⊔ pleft q) (pright p ⊔ pright q)"

instance
  by standard (auto simp: less_eq_analysis_product_def sup_analysis_product_def)

end

instantiation analysis_product :: (order_bot, order_bot) order_bot
begin

definition bot_analysis_product :: "('a, 'b) analysis_product" where
  "bot_analysis_product = Product ⊥ ⊥"

instance
  by standard (simp add: less_eq_analysis_product_def bot_analysis_product_def)

end

instance analysis_product ::
  (bounded_semilattice_sup_bot, bounded_semilattice_sup_bot) bounded_semilattice_sup_bot ..

lemma Product_le_Product [simp]:
  "Product a b ≤ Product a' b' ⟷ a ≤ a' ∧ b ≤ b'"
  by (simp add: less_eq_analysis_product_def)

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

definition widen_analysis_product ::
  "('a, 'b) analysis_product ⇒ ('a, 'b) analysis_product ⇒ ('a, 'b) analysis_product"
where
  "widen_analysis_product p q = Product ((pleft p) ∇ pleft q) ((pright p) ∇ pright q)"

definition narrow_analysis_product ::
  "('a, 'b) analysis_product ⇒ ('a, 'b) analysis_product ⇒ ('a, 'b) analysis_product"
where
  "narrow_analysis_product p q =
     Product ((pleft p) Δ (pleft q)) ((pright p) Δ (pright q))"

instance
  by standard
    (simp_all add: less_eq_analysis_product_def widen_analysis_product_def
      narrow_analysis_product_def narrowing_class.narrow_ge narrowing_class.narrow_le
      widening_class.widen_ge1 widening_class.widen_ge2)

end


end