Theory Int_Lattice

theory Int_Lattice
  imports Sign_Lattice Interval_Lattice Parity_Lattice Congruence_Lattice
begin

section ‹Integer product lattice›

text ‹
  The carrier keeps the four scalar abstractions independently. Its
  concretization is their intersection; componentwise order and join preserve
  the existing domain structures. Cross-domain reduction is separate from
  this carrier definition.
›

subsection ‹Carrier›

record int_dom =
  int_sign :: sign
  int_ivl :: ivl
  int_parity :: parity
  int_congruence :: congruence

subsection ‹Order, join and meet›

text ‹
  The record package represents a closed record through an extensible scheme.
  Giving the scheme a componentwise instance makes the closed ‹int_dom›
  abbreviation usable at every existing lattice-polymorphic boundary. The
  scheme's ‹more› field is Isabelle machinery, not a semantic extension point:
  new integer components belong in ‹int_dom› and must participate explicitly
  in its lattice, concretization, and exact bottom decision.
›

instantiation int_dom_ext :: (bounded_lattice) bounded_lattice
begin

definition less_eq_int_dom_ext ::
  "'a int_dom_scheme => 'a int_dom_scheme => bool" where
  "less_eq_int_dom_ext a b ⟷
     int_sign a <= int_sign b ∧
     int_ivl a <= int_ivl b ∧
     int_parity a <= int_parity b ∧
     int_congruence a <= int_congruence b ∧
     more a <= more b"

definition less_int_dom_ext ::
  "'a int_dom_scheme => 'a int_dom_scheme => bool" where
  "less_int_dom_ext a b ⟷ a ≤ b ∧ ¬ b ≤ a"

definition sup_int_dom_ext ::
  "'a int_dom_scheme => 'a int_dom_scheme => 'a int_dom_scheme" where
  "sup_int_dom_ext a b =
     int_dom_ext
       (sup (int_sign a) (int_sign b))
       (sup (int_ivl a) (int_ivl b))
       (sup (int_parity a) (int_parity b))
       (sup (int_congruence a) (int_congruence b))
       (sup (more a) (more b))"

definition inf_int_dom_ext ::
  "'a int_dom_scheme => 'a int_dom_scheme => 'a int_dom_scheme" where
  "inf_int_dom_ext a b =
     int_dom_ext
       (inf (int_sign a) (int_sign b))
       (inf (int_ivl a) (int_ivl b))
       (inf (int_parity a) (int_parity b))
       (inf (int_congruence a) (int_congruence b))
       (inf (more a) (more b))"

definition bot_int_dom_ext :: "'a int_dom_scheme" where
  "bot_int_dom_ext = int_dom_ext bot bot bot bot bot"

definition top_int_dom_ext :: "'a int_dom_scheme" where
  "top_int_dom_ext = int_dom_ext top top top top top"

instance
proof intro_classes
  fix x y z :: "'a int_dom_scheme"
  show "x < y ⟷ x ≤ y ∧ ¬ y ≤ x"
    by (simp add: less_int_dom_ext_def)
  show "x ≤ x"
    by (simp add: less_eq_int_dom_ext_def)
  show "x ≤ y ⟹ y ≤ z ⟹ x ≤ z"
    by (auto simp: less_eq_int_dom_ext_def intro: order_trans)
  show "x ≤ y ⟹ y ≤ x ⟹ x = y"
    by (cases x; cases y)
       (auto simp: less_eq_int_dom_ext_def intro: antisym)
  show "x ≤ sup x y"
    by (simp add: less_eq_int_dom_ext_def sup_int_dom_ext_def)
  show "y ≤ sup x y"
    by (simp add: less_eq_int_dom_ext_def sup_int_dom_ext_def)
  show "y ≤ x ⟹ z ≤ x ⟹ sup y z ≤ x"
    by (auto simp: less_eq_int_dom_ext_def sup_int_dom_ext_def)
  show "inf x y ≤ x"
    by (simp add: less_eq_int_dom_ext_def inf_int_dom_ext_def)
  show "inf x y ≤ y"
    by (simp add: less_eq_int_dom_ext_def inf_int_dom_ext_def)
  show "x ≤ y ⟹ x ≤ z ⟹ x ≤ inf y z"
    by (auto simp: less_eq_int_dom_ext_def inf_int_dom_ext_def)
  show "bot ≤ x"
    by (simp add: less_eq_int_dom_ext_def bot_int_dom_ext_def)
  show "x ≤ top"
    by (simp add: less_eq_int_dom_ext_def top_int_dom_ext_def)
qed

end

definition int_dom_sip :: "sign => ivl => parity => int_dom" where
  "int_dom_sip s i p =
     (top :: int_dom)⦇int_sign := s, int_ivl := i, int_parity := p⦈"

definition int_dom_sipc ::
  "sign => ivl => parity => congruence => int_dom" where
  "int_dom_sipc s i p c =
     (top :: int_dom)⦇
       int_sign := s,
       int_ivl := i,
       int_parity := p,
       int_congruence := c
     ⦈"

lemma int_congruence_int_dom_sip [simp]:
  "int_congruence (int_dom_sip s i p) = top"
  by (simp add: int_dom_sip_def top_int_dom_ext_def)


subsection ‹Concretization›

text ‹
  A product value denotes the integers every component admits:
  ‹gamma_int_dom› intersects the sign, interval, parity and congruence
  concretizations.
›

definition gamma_int_dom :: "'a int_dom_scheme => int set" where
  "gamma_int_dom d =
     gamma_sign (int_sign d) ∩
     gamma_ivl (int_ivl d) ∩
     gamma_parity (int_parity d) ∩
     gamma_congruence (int_congruence d)"

text ‹
  Every component meet is exact, so the product meet is too: it concretizes to
  the intersection of its operands. Query answers from several analyses are
  combined by ‹⊓›, which therefore neither loses nor invents values.
›

lemma gamma_inf_int_dom [simp]:
  "gamma_int_dom (a ⊓ b) = gamma_int_dom a ∩ gamma_int_dom b"
  by (auto simp: gamma_int_dom_def inf_int_dom_ext_def)

lemma gamma_int_dom_update_sign [simp]:
  "gamma_int_dom (d⦇int_sign := s⦈) =
   gamma_sign s ∩
   gamma_ivl (int_ivl d) ∩
   gamma_parity (int_parity d) ∩
   gamma_congruence (int_congruence d)"
  by (simp add: gamma_int_dom_def)

lemma gamma_int_dom_update_ivl [simp]:
  "gamma_int_dom (d⦇int_ivl := i⦈) =
   gamma_sign (int_sign d) ∩
   gamma_ivl i ∩
   gamma_parity (int_parity d) ∩
   gamma_congruence (int_congruence d)"
  by (simp add: gamma_int_dom_def)

lemma gamma_int_dom_update_parity [simp]:
  "gamma_int_dom (d⦇int_parity := p⦈) =
   gamma_sign (int_sign d) ∩
   gamma_ivl (int_ivl d) ∩
   gamma_parity p ∩
   gamma_congruence (int_congruence d)"
  by (simp add: gamma_int_dom_def)

lemma gamma_int_dom_update_congruence [simp]:
  "gamma_int_dom (d⦇int_congruence := c⦈) =
   gamma_sign (int_sign d) ∩
   gamma_ivl (int_ivl d) ∩
   gamma_parity (int_parity d) ∩
   gamma_congruence c"
  by (simp add: gamma_int_dom_def)

fun interval_fact_of_sign :: "sign ⇒ ivl" where
  "interval_fact_of_sign SBot = ⊥"
| "interval_fact_of_sign SNeg = Ivl MinInf (Fin (-1))"
| "interval_fact_of_sign SNonPos = Ivl MinInf (Fin 0)"
| "interval_fact_of_sign SZero = Ivl (Fin 0) (Fin 0)"
| "interval_fact_of_sign SNonNeg = Ivl (Fin 0) PlusInf"
| "interval_fact_of_sign SPos = Ivl (Fin 1) PlusInf"
| "interval_fact_of_sign STop = ⊤"

lemma gamma_interval_fact_of_sign [simp]:
  "gamma_ivl (interval_fact_of_sign s) = gamma_sign s"
  by (cases s) (auto simp: bot_ivl_def top_ivl_def ivl_top_def)

fun congruence_fact_of_parity :: "parity => congruence" where
  "congruence_fact_of_parity PBot = bot"
| "congruence_fact_of_parity PEven = mk_congruence 0 2"
| "congruence_fact_of_parity POdd = mk_congruence 1 2"
| "congruence_fact_of_parity PTop = top"

lemma gamma_congruence_fact_of_parity [simp]:
  "gamma_congruence (congruence_fact_of_parity p) = gamma_parity p"
  by (cases p)
     (auto simp: bot_congruence_def)

lemma gamma_intersect_ivl_exact:
  "gamma_ivl (intersect_ivl a b) = gamma_ivl a ∩ gamma_ivl b"
  using gamma_ivl_mono[OF intersect_ivl_le1]
        gamma_ivl_mono[OF intersect_ivl_le2]
        intersect_ivl_gamma
  by blast

subsection ‹Executable interface›

text ‹
  Deciding emptiness of the product needs more than the components' own tests,
  since each can be inhabited while their intersection is empty. Interval and
  congruence are checked jointly, after restricting the congruence by parity;
  ‹is_bottom_int_dom_correct› and ‹is_top_int_dom_correct_gamma› tie the tests to ‹gamma_int_dom›.
›

lemma inter_nonempty_iff:
  "A ∩ B ≠ {} ⟷ (∃x. x ∈ A ∧ x ∈ B)"
  by blast

lemma congruence_between_iff:
  assumes normalized: "normalized_congruence_rep (Some (c, m))"
  shows
    "(∃n::int. l ≤ n ∧ n ≤ u ∧ m dvd n - c) ⟷
     (if m = 0 then l ≤ c ∧ c ≤ u
      else l ≤ u ∧ l + ((c - l) mod m) ≤ u)"
proof (cases "m = 0")
  case True
  then show ?thesis by simp
next
  case False
  from normalized_congruence_rep_nonzero[OF normalized False]
  have modulus: "0 < m" by simp
  show ?thesis
  proof
    assume "∃n::int. l ≤ n ∧ n ≤ u ∧ m dvd n - c"
    then obtain n where n: "l ≤ n" "n ≤ u" "m dvd n - c"
      by blast
    have offset: "m dvd c - n"
      using n(3) by (metis dvd_minus_iff minus_diff_eq)
    have mod_eq: "(c - l) mod m = (n - l) mod m"
      using offset
      by (simp add:
          Euclidean_Rings.euclidean_ring_cancel_class.mod_eq_dvd_iff)
    have remainder_le: "(n - l) mod m ≤ n - l"
      by (rule Euclidean_Rings.zmod_le_nonneg_dividend) (use n(1) in linarith)
    show
      "if m = 0 then l ≤ c ∧ c ≤ u
       else l ≤ u ∧ l + ((c - l) mod m) ≤ u"
      using False mod_eq n(1,2) remainder_le
      by simp
  next
    assume rhs:
      "if m = 0 then l ≤ c ∧ c ≤ u
       else l ≤ u ∧ l + ((c - l) mod m) ≤ u"
    let ?n = "l + ((c - l) mod m)"
    have lower: "l ≤ ?n"
      using modulus by simp
    have congruent: "m dvd ?n - c"
    proof -
      have base: "m dvd (c - l) - (c - l) mod m"
        by (rule dvd_minus_mod)
      have "m dvd - ((c - l) - (c - l) mod m)"
        using base by (simp only: dvd_minus_iff)
      also have
        "- ((c - l) - (c - l) mod m) = ?n - c"
        by simp
      finally show ?thesis .
    qed
    have upper: "?n ≤ u"
      using rhs False by simp
    show "∃n::int. l ≤ n ∧ n ≤ u ∧ m dvd n - c"
      by (rule exI[of _ ?n]) (use lower upper congruent in blast)
  qed
qed

lemma congruence_class_nonempty:
  "∃n::int. m dvd n - c"
  by (rule exI[of _ c]) simp

lemma exists_congruence_le:
  assumes normalized: "normalized_congruence_rep (Some (c, m))"
      and nonzero: "m ≠ 0"
  shows "∃n::int. n ≤ u ∧ m dvd n - c"
proof -
  from normalized_congruence_rep_nonzero[OF normalized nonzero]
  have one_le: "1 ≤ m" by simp
  let ?q = "abs (c - u) + 1"
  have q_nonnegative: "0 ≤ ?q" by simp
  have difference_le_q: "c - u ≤ ?q"
    using abs_ge_self[of "c - u"] by linarith
  have scale: "?q ≤ m * ?q"
    using mult_right_mono[OF one_le q_nonnegative] by simp
  let ?n = "c - m * ?q"
  have upper: "?n ≤ u"
    using difference_le_q scale by linarith
  have congruent: "m dvd ?n - c"
    by simp
  show ?thesis
    by (rule exI[of _ ?n]) (use upper congruent in blast)
qed

lemma exists_congruence_ge:
  assumes normalized: "normalized_congruence_rep (Some (c, m))"
      and nonzero: "m ≠ 0"
  shows "∃n::int. l ≤ n ∧ m dvd n - c"
proof -
  from normalized_congruence_rep_nonzero[OF normalized nonzero]
  have one_le: "1 ≤ m" by simp
  let ?q = "abs (l - c) + 1"
  have q_nonnegative: "0 ≤ ?q" by simp
  have difference_le_q: "l - c ≤ ?q"
    using abs_ge_self[of "l - c"] by linarith
  have scale: "?q ≤ m * ?q"
    using mult_right_mono[OF one_le q_nonnegative] by simp
  let ?n = "c + m * ?q"
  have lower: "l ≤ ?n"
    using difference_le_q scale by linarith
  have congruent: "m dvd ?n - c"
    by simp
  show ?thesis
    by (rule exI[of _ ?n]) (use lower congruent in blast)
qed

fun ivl_congruence_rep_nonempty ::
  "ivl => congruence_rep => bool" where
  "ivl_congruence_rep_nonempty i None = False"
| "ivl_congruence_rep_nonempty (Ivl MinInf MinInf) (Some cm) = False"
| "ivl_congruence_rep_nonempty (Ivl MinInf (Fin u)) (Some (c, m)) =
     (if m = 0 then c ≤ u else True)"
| "ivl_congruence_rep_nonempty (Ivl MinInf PlusInf) (Some cm) = True"
| "ivl_congruence_rep_nonempty (Ivl (Fin l) MinInf) (Some cm) = False"
| "ivl_congruence_rep_nonempty (Ivl (Fin l) (Fin u)) (Some (c, m)) =
     (if m = 0 then l ≤ c ∧ c ≤ u
      else l ≤ u ∧ l + ((c - l) mod m) ≤ u)"
| "ivl_congruence_rep_nonempty (Ivl (Fin l) PlusInf) (Some (c, m)) =
     (if m = 0 then l ≤ c else True)"
| "ivl_congruence_rep_nonempty (Ivl PlusInf u) (Some cm) = False"

lemma ivl_congruence_rep_nonempty_correct:
  assumes normalized: "normalized_congruence_rep r"
  shows
    "ivl_congruence_rep_nonempty i r ⟷
     gamma_ivl i ∩ gamma_congruence_rep r ≠ {}"
proof (cases r)
  case None
  then show ?thesis by simp
next
  case (Some cm)
  obtain c m where cm: "cm = (c, m)"
    by (cases cm)
  have rep: "r = Some (c, m)"
    using Some cm by simp
  have normalized': "normalized_congruence_rep (Some (c, m))"
    using normalized unfolding rep .
  show ?thesis
  proof (cases i)
    case (Ivl l u)
    show ?thesis
      unfolding rep Ivl
      by (cases l; cases u; cases "m = 0")
         (auto simp: inter_nonempty_iff
            congruence_between_iff[OF normalized']
            congruence_class_nonempty
            exists_congruence_le[OF normalized']
            exists_congruence_ge[OF normalized'])
  qed
qed

fun parity_accepts :: "parity => int => bool" where
  "parity_accepts PBot n = False"
| "parity_accepts PEven n = even n"
| "parity_accepts POdd n = odd n"
| "parity_accepts PTop n = True"

lemma parity_accepts_gamma [simp]:
  "parity_accepts p n ⟷ n ∈ gamma_parity p"
  by (cases p) simp_all

lemma parity_accepts_difference:
  assumes concrete: "p = PEven ∨ p = POdd"
      and accepts: "parity_accepts p r"
  shows "2 dvd n - r ⟷ parity_accepts p n"
  using concrete accepts
  by (cases p) auto

lemma dvd_shift_modulus:
  fixes m n c :: int
  shows "m dvd n - (c + m) ⟷ m dvd n - c"
proof
  assume shifted: "m dvd n - (c + m)"
  have "m dvd (n - (c + m)) + m"
    by (rule dvd_add[OF shifted dvd_refl[of m]])
  then show "m dvd n - c" by simp
next
  assume original: "m dvd n - c"
  have "m dvd (n - c) - m"
    by (rule dvd_diff[OF original dvd_refl[of m]])
  also have "(n - c) - m = n - (c + m)"
    by simp
  finally show "m dvd n - (c + m)" .
qed

lemma gamma_normalized_lcm_two:
  "gamma_congruence_rep
     (normalize_congruence_rep (Some (r, lcm m 2))) =
   {n. m dvd n - r ∧ 2 dvd n - r}"
  by (simp only: gamma_normalize_congruence_rep
      gamma_congruence_rep.simps
      GCD.semiring_gcd_class.lcm_least_iff)

lemma congruent_even_modulus:
  fixes m n c :: int
  assumes modulus: "even m"
      and congruent: "m dvd n - c"
  shows "even n ⟷ even c"
proof -
  obtain k where difference: "n - c = m * k"
    using congruent unfolding dvd_def by blast
  have difference_even: "even (n - c)"
    using modulus difference by simp
  have parity_eq: "even (n - c) = even (n + c)"
    by (rule even_diff_iff)
  have sum_even: "even (n + c)"
    using parity_eq difference_even by blast
  show ?thesis
    using sum_even
    by (simp only: Parity.semiring_parity_class.even_add)
qed

lemma normalized_lcm_two_inter_parity:
  assumes concrete: "p = PEven ∨ p = POdd"
      and accepts: "parity_accepts p r"
  shows
    "gamma_congruence_rep
       (normalize_congruence_rep (Some (r, lcm m 2))) =
     gamma_parity p ∩ {n. m dvd n - r}"
proof -
  have difference:
    "⋀n. 2 dvd n - r ⟷ parity_accepts p n"
    by (rule parity_accepts_difference[OF concrete accepts])
  show ?thesis
    unfolding gamma_normalized_lcm_two
    using difference by auto
qed

lemma even_modulus_disjoint_parity:
  assumes concrete: "p = PEven ∨ p = POdd"
      and modulus: "even m"
      and rejects: "¬ parity_accepts p c"
  shows "gamma_parity p ∩ {n. m dvd n - c} = {}"
proof (rule equals0I)
  fix n
  assume member:
    "n ∈ gamma_parity p ∩ {n. m dvd n - c}"
  from member have accepts: "parity_accepts p n"
    by simp
  from member have congruent: "m dvd n - c"
    by simp
  have same: "even n ⟷ even c"
    by (rule congruent_even_modulus[OF modulus congruent])
  from concrete rejects accepts same show False
    by (cases p) auto
qed

lemma parity_accepts_add_odd:
  assumes concrete: "p = PEven ∨ p = POdd"
      and rejects: "¬ parity_accepts p c"
      and modulus: "odd m"
  shows "parity_accepts p (c + m)"
  using concrete rejects modulus by (cases p) auto

fun restrict_congruence_rep_by_parity ::
  "parity => congruence_rep => congruence_rep" where
  "restrict_congruence_rep_by_parity PBot r = None"
| "restrict_congruence_rep_by_parity PTop r = r"
| "restrict_congruence_rep_by_parity p None = None"
| "restrict_congruence_rep_by_parity p (Some (c, m)) =
     (if m = 0 then
        if parity_accepts p c then Some (c, 0) else None
      else if even m ∧ ¬ parity_accepts p c then None
      else
        normalize_congruence_rep
          (Some
            (c + (if parity_accepts p c then 0 else m),
             lcm m 2)))"

lemma normalized_restrict_congruence_rep_by_parity:
  assumes "normalized_congruence_rep r"
  shows
    "normalized_congruence_rep
       (restrict_congruence_rep_by_parity p r)"
  using assms
  by (cases p; cases r)
     (auto simp only: restrict_congruence_rep_by_parity.simps
        normalized_congruence_rep.simps
        normalized_normalize_congruence_rep
        option.simps
        split: prod.splits if_splits)

lemma restrict_concrete_parity_correct:
  assumes concrete: "p = PEven ∨ p = POdd"
  shows
    "gamma_congruence_rep
       (restrict_congruence_rep_by_parity p (Some (c, m))) =
     gamma_parity p ∩ gamma_congruence_rep (Some (c, m))"
proof (cases "m = 0")
  case True
  with concrete show ?thesis
    by (cases p) auto
next
  case nonzero: False
  show ?thesis
  proof (cases "even m")
    case modulus: True
    show ?thesis
    proof (cases "parity_accepts p c")
      case accepts: True
      have reduced:
        "restrict_congruence_rep_by_parity p (Some (c, m)) =
         normalize_congruence_rep (Some (c, lcm m 2))"
        using concrete nonzero modulus accepts
        by (cases p) simp_all
      have exact:
        "gamma_congruence_rep
           (normalize_congruence_rep (Some (c, lcm m 2))) =
         gamma_parity p ∩ {n. m dvd n - c}"
        by (rule normalized_lcm_two_inter_parity[OF concrete accepts])
      show ?thesis
        unfolding reduced
        using exact by simp
    next
      case rejects: False
      have reduced:
        "restrict_congruence_rep_by_parity p (Some (c, m)) = None"
        using concrete nonzero modulus rejects
        by (cases p) simp_all
      have disjoint:
        "gamma_parity p ∩ {n. m dvd n - c} = {}"
        by (rule even_modulus_disjoint_parity[OF concrete modulus rejects])
      show ?thesis
        unfolding reduced
        using disjoint by simp
    qed
  next
    case modulus: False
    show ?thesis
    proof (cases "parity_accepts p c")
      case accepts: True
      have reduced:
        "restrict_congruence_rep_by_parity p (Some (c, m)) =
         normalize_congruence_rep (Some (c, lcm m 2))"
        using concrete nonzero modulus accepts
        by (cases p) simp_all
      have exact:
        "gamma_congruence_rep
           (normalize_congruence_rep (Some (c, lcm m 2))) =
         gamma_parity p ∩ {n. m dvd n - c}"
        by (rule normalized_lcm_two_inter_parity[OF concrete accepts])
      show ?thesis
        unfolding reduced
        using exact by simp
    next
      case rejects: False
      have odd_modulus: "odd m"
        using modulus by simp
      have shifted_accepts: "parity_accepts p (c + m)"
        by (rule parity_accepts_add_odd[OF concrete rejects odd_modulus])
      have reduced:
        "restrict_congruence_rep_by_parity p (Some (c, m)) =
         normalize_congruence_rep (Some (c + m, lcm m 2))"
        using concrete nonzero modulus rejects
        by (cases p) simp_all
      have exact:
        "gamma_congruence_rep
           (normalize_congruence_rep (Some (c + m, lcm m 2))) =
         gamma_parity p ∩ {n. m dvd n - (c + m)}"
        by (rule normalized_lcm_two_inter_parity[
              OF concrete shifted_accepts])
      show ?thesis
        unfolding reduced
        using exact by (simp only: gamma_congruence_rep.simps
            dvd_shift_modulus)
    qed
  qed
qed

lemma restrict_congruence_rep_by_parity_correct:
  assumes normalized: "normalized_congruence_rep r"
  shows
    "gamma_congruence_rep
       (restrict_congruence_rep_by_parity p r) =
     gamma_parity p ∩ gamma_congruence_rep r"
proof (cases p)
  case PBot
  then show ?thesis by simp
next
  case PTop
  then show ?thesis by simp
next
  case destination: PEven
  show ?thesis
  proof (cases r)
    case None
    with destination show ?thesis by simp
  next
    case (Some cm)
    obtain c m where cm: "cm = (c, m)"
      by (cases cm)
    have rep: "r = Some (c, m)"
      using Some cm by simp
    show ?thesis
      unfolding destination rep
      by (rule restrict_concrete_parity_correct) simp
  qed
next
  case destination: POdd
  show ?thesis
  proof (cases r)
    case None
    with destination show ?thesis by simp
  next
    case (Some cm)
    obtain c m where cm: "cm = (c, m)"
      by (cases cm)
    have rep: "r = Some (c, m)"
      using Some cm by simp
    show ?thesis
      unfolding destination rep
      by (rule restrict_concrete_parity_correct) simp
  qed
qed


lift_definition restrict_congruence_by_parity ::
  "parity => congruence => congruence"
  is restrict_congruence_rep_by_parity
  by (rule normalized_restrict_congruence_rep_by_parity)

declare restrict_congruence_by_parity.rep_eq [simp]

lemma gamma_restrict_congruence_by_parity [simp]:
  "gamma_congruence (restrict_congruence_by_parity p c) =
   gamma_parity p ∩ gamma_congruence c"
proof -
  have normalized:
    "normalized_congruence_rep (Rep_congruence c)"
    by simp
  have raw:
    "gamma_congruence_rep
       (restrict_congruence_rep_by_parity p (Rep_congruence c)) =
     gamma_parity p ∩
     gamma_congruence_rep (Rep_congruence c)"
    by (rule restrict_congruence_rep_by_parity_correct[OF normalized])
  show ?thesis
    unfolding gamma_congruence_def
    using raw by simp
qed

definition ivl_congruence_nonempty ::
  "ivl => congruence => bool" where
  "ivl_congruence_nonempty i c =
   ivl_congruence_rep_nonempty i (Rep_congruence c)"

lemma ivl_congruence_nonempty_correct:
  "ivl_congruence_nonempty i c ⟷
   gamma_ivl i ∩ gamma_congruence c ≠ {}"
proof -
  have normalized:
    "normalized_congruence_rep (Rep_congruence c)"
    by simp
  show ?thesis
    unfolding ivl_congruence_nonempty_def gamma_congruence_def
    by (rule ivl_congruence_rep_nonempty_correct[OF normalized])
qed

definition is_bottom_int_dom :: "'a int_dom_scheme => bool" where
  "is_bottom_int_dom d =
     (¬ ivl_congruence_nonempty
       (intersect_ivl
         (interval_fact_of_sign (int_sign d))
         (int_ivl d))
       (restrict_congruence_by_parity
         (int_parity d)
         (int_congruence d)))"

lemma is_bottom_int_dom_correct:
  "is_bottom_int_dom d ⟷ gamma_int_dom d = {}"
proof -
  let ?i =
    "intersect_ivl
       (interval_fact_of_sign (int_sign d))
       (int_ivl d)"
  let ?c =
    "restrict_congruence_by_parity
       (int_parity d)
       (int_congruence d)"
  have nonempty:
    "ivl_congruence_nonempty ?i ?c ⟷
     gamma_ivl ?i ∩ gamma_congruence ?c ≠ {}"
    by (rule ivl_congruence_nonempty_correct)
  have restricted:
    "gamma_congruence ?c =
     gamma_parity (int_parity d) ∩
     gamma_congruence (int_congruence d)"
    by simp
  have interval:
    "gamma_ivl ?i =
     gamma_sign (int_sign d) ∩ gamma_ivl (int_ivl d)"
    by (simp only: gamma_intersect_ivl_exact
          gamma_interval_fact_of_sign)
  show ?thesis
    unfolding is_bottom_int_dom_def gamma_int_dom_def
    using nonempty restricted interval by blast
qed

text ‹
  Semantic fullness, symmetric to ‹is_bottom_int_dom› above: ‹d = top›
  additionally pins the record's own ‹more› extension field to its top,
  which ‹gamma_int_dom› never inspects, so it is strictly stronger than
  ‹gamma_int_dom d = UNIV› at this instance's actual, extension-polymorphic
  ‹'a int_dom_scheme› type. Testing each of the four concrete components'
  own exact fullness instead reads off ‹gamma_int_dom›'s own definition
  directly, the same move ‹is_bottom_int_dom› already makes for emptiness.
›

definition is_top_int_dom :: "'a int_dom_scheme => bool" where
  "is_top_int_dom d ⟷
     is_top_sign (int_sign d) ∧ is_top_ivl (int_ivl d) ∧
     is_top_parity (int_parity d) ∧ is_top_congruence (int_congruence d)"

lemma is_top_int_dom_correct_gamma: "is_top_int_dom d ⟷ gamma_int_dom d = UNIV"
  unfolding is_top_int_dom_def gamma_int_dom_def
  using is_top_sign_correct_gamma is_top_ivl_correct_gamma
        is_top_parity_correct_gamma is_top_congruence_correct_gamma
  by auto

lemma gamma_int_dom_mono:
  assumes ab: "a ≤ b"
  shows "gamma_int_dom a ⊆ gamma_int_dom b"
proof -
  from ab have le:
    "int_sign a ≤ int_sign b"
    "int_ivl a ≤ int_ivl b"
    "int_parity a ≤ int_parity b"
    "int_congruence a ≤ int_congruence b"
    by (simp_all add: less_eq_int_dom_ext_def)
  have S: "gamma_sign (int_sign a) ⊆ gamma_sign (int_sign b)"
    using le(1) unfolding less_eq_sign_def by (rule gamma_sign_mono)
  have I: "gamma_ivl (int_ivl a) ⊆ gamma_ivl (int_ivl b)"
    using le(2) by (rule gamma_ivl_mono)
  have P: "gamma_parity (int_parity a) ⊆ gamma_parity (int_parity b)"
    using le(3) unfolding less_eq_parity_def by (rule gamma_parity_mono)
  have C:
    "gamma_congruence (int_congruence a) ⊆
     gamma_congruence (int_congruence b)"
    using le(4)
    unfolding less_eq_congruence_iff_gamma .
  show ?thesis
    unfolding gamma_int_dom_def using S I P C by auto
qed

subsection ‹Constants and printing›

text ‹
  ‹int_dom_of_int› pins every component to one integer, so it concretizes
  to exactly that singleton; the printer follows Goblint's tuple format.
›

definition int_dom_of_int :: "int => int_dom" where
  "int_dom_of_int n =
     (top :: int_dom)⦇
       int_sign := sign_of_int n,
       int_ivl := Ivl (Fin n) (Fin n),
       int_parity := parity_of_int n,
       int_congruence := congruence_of_int n
     ⦈"

lemma gamma_int_dom_of_int [simp]:
  "gamma_int_dom (int_dom_of_int n) = {n}"
  by (auto simp: int_dom_of_int_def gamma_int_dom_def
        sign_of_int_gamma parity_of_int_gamma)


text ‹
  Goblint's integer-domain tuple prints a value one of its components pins to a
  single integer as that integer, a value no component constrains as ‹⊤›,
  and anything else as its components, each named and separated by ‹;›. The
  bottom test runs first, so a component that concretizes to one integer pins a
  live product to exactly that integer.
›

fun ivl_constant :: "ivl ⇒ int option" where
    "ivl_constant (Ivl (Fin l) (Fin u)) = (if l = u then Some l else None)"
  | "ivl_constant _ = None"

definition congruence_constant :: "congruence ⇒ int option" where
  "congruence_constant c =
     (case Rep_congruence c of
        Some (r, m) ⇒ if m = 0 then Some r else None
      | None ⇒ None)"

definition int_dom_constant :: "'a int_dom_scheme ⇒ int option" where
  "int_dom_constant d =
     (if int_sign d = SZero then Some 0
      else case ivl_constant (int_ivl d) of
        Some n ⇒ Some n
      | None ⇒ congruence_constant (int_congruence d))"

lemma gamma_ivl_constant:
  "ivl_constant i = Some n ⟹ gamma_ivl i = {n}"
  by (induction i rule: ivl_constant.induct) (auto split: if_splits)

lemma gamma_congruence_constant:
  "congruence_constant c = Some n ⟹ gamma_congruence c = {n}"
  unfolding congruence_constant_def gamma_congruence_def
  by (auto split: option.splits if_splits)

text ‹Printing a live product as the integer \<^const>‹int_dom_constant› names
  loses nothing: that integer is all the product denotes.›

lemma gamma_int_dom_constant_subset:
  "int_dom_constant d = Some n ⟹ gamma_int_dom d ⊆ {n}"
  using gamma_ivl_constant gamma_congruence_constant
  unfolding int_dom_constant_def gamma_int_dom_def
  by (auto split: if_splits option.splits)

definition string_of_int_dom :: "'a int_dom_scheme ⇒ String.literal" where
  "string_of_int_dom d =
     (if is_bottom_int_dom d then sym_bottom
      else if is_top_int_dom d then sym_top
      else case int_dom_constant d of
        Some n ⇒ string_of_int n
      | None ⇒
            STR ''signs:'' + string_of_sign (int_sign d)
          + STR ''; intervals:'' + string_of_ivl (int_ivl d)
          + STR ''; parities:'' + string_of_parity (int_parity d)
          + STR ''; congruences:'' + string_of_congruence (int_congruence d))"

end