Theory Parity_Warrowing

theory Parity_Warrowing
  imports "Voblint_Domain.Parity_Lattice"
begin

section ‹Parity warrowing and domain instance›

text ‹
  Parity is finite, so widening is join and narrowing keeps the left argument.
›

instantiation parity :: warrowing begin
  definition "((a :: parity) ∇ b) = join_parity a b"
  definition "((a :: parity) Δ b) = a"
instance proof
  fix a b :: parity
  show "a ≤ (a ∇ b)" unfolding less_eq_parity_def widen_parity_def by (rule join_parity_ub1)
  show "b ≤ (a ∇ b)" unfolding less_eq_parity_def widen_parity_def by (rule join_parity_ub2)
  show "b ≤ a ⟹ b ≤ (a Δ b)" unfolding narrow_parity_def by simp
  show "b ≤ a ⟹ (a Δ b) ≤ a"
    unfolding narrow_parity_def by (simp add: less_eq_parity_def)
qed
end

instantiation parity :: numeric_domain begin
definition gamma_abs_parity [simp]: "numeric_domain_class.gamma (a :: parity) = gamma_parity a"
definition is_empty_parity [simp]: "is_empty (a :: parity) = is_bottom_parity a"
definition to_string_parity [simp]:
  "to_string (a :: parity) = (if is_top_parity a then sym_top else string_of_parity a)"
instance proof
  show "numeric_domain_class.gamma (bot :: parity) = {}" unfolding bot_parity_def by simp
next
  show "numeric_domain_class.gamma (top :: parity) = UNIV" by (simp add: gamma_parity_top)
next
  fix a b :: parity
  assume H: "a ≤ b"
  have "gamma_parity a ⊆ gamma_parity b"
    using H unfolding less_eq_parity_def by (rule gamma_parity_mono)
  then show "numeric_domain_class.gamma a ⊆ numeric_domain_class.gamma b" by simp
next
  fix a :: parity
  show "is_empty a ⟷ numeric_domain_class.gamma a = {}"
    by (simp add: is_bottom_parity_correct)
qed
end

end