Theory Data_Integer

section ‹Data: Integers›

theory Data_Integer
  imports
    Numeral_Cpo
    Data_Bool
begin

domain Integer = MkI (lazy int)

instance Integer :: flat
proof
  fix x y :: Integer
  assume "x ⊑ y" then show "x = ⊥ ∨ x = y"
    by (cases x; cases y) simp_all
qed

instantiation Integer :: "{plus,times,minus,uminus,zero,one}"
begin

definition "0 = MkI⋅0"
definition "1 = MkI⋅1"
definition "a + b = (Λ (MkI⋅x) (MkI⋅y). MkI⋅(x + y))⋅a⋅b"
definition "a - b = (Λ (MkI⋅x) (MkI⋅y). MkI⋅(x - y))⋅a⋅b"
definition "a * b = (Λ (MkI⋅x) (MkI⋅y). MkI⋅(x * y))⋅a⋅b"
definition "- a = (Λ (MkI⋅x). MkI⋅(uminus x))⋅a"

instance ..

end

lemma Integer_arith_strict [simp]:
  fixes x :: Integer
  shows "⊥ + x = ⊥" and "x + ⊥ = ⊥"
    and "⊥ * x = ⊥" and "x * ⊥ = ⊥"
    and "⊥ - x = ⊥" and "x - ⊥ = ⊥"
    and "- ⊥ = (⊥::Integer)"
  unfolding plus_Integer_def times_Integer_def
  unfolding minus_Integer_def uminus_Integer_def
  by (cases x, simp, simp)+

lemma Integer_arith_simps [simp]:
  "MkI⋅a + MkI⋅b = MkI⋅(a + b)"
  "MkI⋅a * MkI⋅b = MkI⋅(a * b)"
  "MkI⋅a - MkI⋅b = MkI⋅(a - b)"
  "- MkI⋅a = MkI⋅(uminus a)"
  unfolding plus_Integer_def times_Integer_def
  unfolding minus_Integer_def uminus_Integer_def
  by simp_all

lemma plus_MkI_MkI:
  "MkI⋅x + MkI⋅y = MkI⋅(x + y)"
  unfolding plus_Integer_def by simp

instance Integer :: "{plus_cpo,minus_cpo,times_cpo}"
  by standard (simp_all add: flatdom_strict2cont)

instance Integer :: comm_monoid_add
proof
  fix a b c :: Integer
  show "(a + b) + c = a + (b + c)"
    by (cases a; cases b; cases c) simp_all
  show "a + b = b + a"
    by (cases a; cases b) simp_all
  show "0 + a = a"
    unfolding zero_Integer_def
    by (cases a) simp_all
qed

instance Integer :: comm_monoid_mult
proof
  fix a b c :: Integer
  show "(a * b) * c = a * (b * c)"
    by (cases a; cases b; cases c) simp_all
  show "a * b = b * a"
    by (cases a; cases b) simp_all
  show "1 * a = a"
    unfolding one_Integer_def
    by (cases a) simp_all
qed

instance Integer :: comm_semiring
proof
  fix a b c :: Integer
  show "(a + b) * c = a * c + b * c"
    by (cases a; cases b; cases c) (simp_all add: distrib_right)
qed

instance Integer :: semiring_numeral ..

lemma Integer_add_diff_cancel [simp]:
  "b ≠ ⊥ ⟹ (a::Integer) + b - b = a"
  by (cases a; cases b) simp_all

lemma zero_Integer_neq_bottom [simp]: "(0::Integer) ≠ ⊥"
  by (simp add: zero_Integer_def)

lemma one_Integer_neq_bottom [simp]: "(1::Integer) ≠ ⊥"
  by (simp add: one_Integer_def)

lemma plus_Integer_eq_bottom_iff [simp]:
  fixes x y :: Integer shows "x + y = ⊥ ⟷ x = ⊥ ∨ y = ⊥"
  by (cases x, simp, cases y, simp, simp)

lemma diff_Integer_eq_bottom_iff [simp]:
  fixes x y :: Integer shows "x - y = ⊥ ⟷ x = ⊥ ∨ y = ⊥"
  by (cases x, simp, cases y, simp, simp)

lemma mult_Integer_eq_bottom_iff [simp]:
  fixes x y :: Integer shows "x * y = ⊥ ⟷ x = ⊥ ∨ y = ⊥"
  by (cases x, simp, cases y, simp, simp)

lemma minus_Integer_eq_bottom_iff [simp]:
  fixes x :: Integer shows "- x = ⊥ ⟷ x = ⊥"
  by (cases x, simp, simp)

lemma numeral_Integer_eq: "numeral k = MkI⋅(numeral k)"
  by (induct k, simp_all only: numeral.simps one_Integer_def plus_MkI_MkI)

lemma numeral_Integer_neq_bottom [simp]: "(numeral k::Integer) ≠ ⊥"
  unfolding numeral_Integer_eq by simp

text ‹Symmetric versions are also needed, because the reorient
  simproc does not apply to these comparisons.›

lemma bottom_neq_zero_Integer [simp]: "(⊥::Integer) ≠ 0"
  by (simp add: zero_Integer_def)

lemma bottom_neq_one_Integer [simp]: "(⊥::Integer) ≠ 1"
  by (simp add: one_Integer_def)

lemma bottom_neq_numeral_Integer [simp]: "(⊥::Integer) ≠ numeral k"
  unfolding numeral_Integer_eq by simp

instantiation Integer :: Ord_linear
begin

definition
  "eq = (Λ (MkI⋅x) (MkI⋅y). if x = y then TT else FF)"

definition
  "compare = (Λ (MkI⋅x) (MkI⋅y).
    if x < y then LT else if x > y then GT else EQ)"

instance proof
  fix x y z :: Integer
  show "compare⋅⊥⋅y = ⊥"
    unfolding compare_Integer_def by simp
  show "compare⋅x⋅⊥ = ⊥"
    unfolding compare_Integer_def by (cases x, simp_all)
  show "oppOrdering⋅(compare⋅x⋅y) = compare⋅y⋅x"
    unfolding compare_Integer_def
    by (cases x, cases y, simp, simp,
        cases y, simp, simp add: not_less less_imp_le)
  show "x = y" if "compare⋅x⋅y = EQ"
    using that
    unfolding compare_Integer_def
    by (cases x, cases y, simp, simp,
        cases y, simp, simp split: if_splits)
  show "compare⋅x⋅z = LT" if "compare⋅x⋅y = LT" and "compare⋅y⋅z = LT"
    using that
    unfolding compare_Integer_def
    by (cases x, simp, cases y, simp, cases z, simp,
        auto split: if_splits)
  show "eq⋅x⋅y = is_EQ⋅(compare⋅x⋅y)"
    unfolding eq_Integer_def compare_Integer_def
    by (cases x, simp, cases y, simp, auto)
  show "compare⋅x⋅x ⊑ EQ"
    unfolding compare_Integer_def
    by (cases x, simp_all)
qed

end

lemma eq_MkI_MkI [simp]:
  "eq⋅(MkI⋅m)⋅(MkI⋅n) = (if m = n then TT else FF)"
  by (simp add: eq_Integer_def)

lemma compare_MkI_MkI [simp]:
  "compare⋅(MkI⋅x)⋅(MkI⋅y) = (if x < y then LT else if x > y then GT else EQ)"
  unfolding compare_Integer_def by simp

lemma lt_MkI_MkI [simp]:
  "lt⋅(MkI⋅x)⋅(MkI⋅y) = (if x < y then TT else FF)"
  unfolding lt_def by simp

lemma le_MkI_MkI [simp]:
  "le⋅(MkI⋅x)⋅(MkI⋅y) = (if x ≤ y then TT else FF)"
  unfolding le_def by simp

lemma eq_Integer_bottom_iff [simp]:
  fixes x y :: Integer shows "eq⋅x⋅y = ⊥ ⟷ x = ⊥ ∨ y = ⊥"
  by (cases x, simp, cases y, simp, simp)

lemma compare_Integer_bottom_iff [simp]:
  fixes x y :: Integer shows "compare⋅x⋅y = ⊥ ⟷ x = ⊥ ∨ y = ⊥"
  by (cases x, simp, cases y, simp, simp)

lemma lt_Integer_bottom_iff [simp]:
  fixes x y :: Integer shows "lt⋅x⋅y = ⊥ ⟷ x = ⊥ ∨ y = ⊥"
  by (cases x, simp, cases y, simp, simp)

lemma le_Integer_bottom_iff [simp]:
  fixes x y :: Integer shows "le⋅x⋅y = ⊥ ⟷ x = ⊥ ∨ y = ⊥"
  by (cases x, simp, cases y, simp, simp)

lemma compare_refl_Integer [simp]:
  "(x::Integer) ≠ ⊥ ⟹ compare⋅x⋅x = EQ"
  by (cases x) simp_all

lemma eq_refl_Integer [simp]:
  "(x::Integer) ≠ ⊥ ⟹ eq⋅x⋅x = TT"
  by (cases x) simp_all

lemma lt_refl_Integer [simp]:
  "(x::Integer) ≠ ⊥ ⟹ lt⋅x⋅x = FF"
  by (cases x) simp_all

lemma le_refl_Integer [simp]:
  "(x::Integer) ≠ ⊥ ⟹ le⋅x⋅x = TT"
  by (cases x) simp_all

lemma eq_Integer_numeral_simps [simp]:
  "eq⋅(0::Integer)⋅0 = TT"
  "eq⋅(0::Integer)⋅1 = FF"
  "eq⋅(1::Integer)⋅0 = FF"
  "eq⋅(1::Integer)⋅1 = TT"
  "eq⋅(0::Integer)⋅(numeral k) = FF"
  "eq⋅(numeral k)⋅(0::Integer) = FF"
  "k ≠ Num.One ⟹ eq⋅(1::Integer)⋅(numeral k) = FF"
  "k ≠ Num.One ⟹ eq⋅(numeral k)⋅(1::Integer) = FF"
  "eq⋅(numeral k::Integer)⋅(numeral l) = (if k = l then TT else FF)"
  unfolding zero_Integer_def one_Integer_def numeral_Integer_eq
  by simp_all

lemma compare_Integer_numeral_simps [simp]:
  "compare⋅(0::Integer)⋅0 = EQ"
  "compare⋅(0::Integer)⋅1 = LT"
  "compare⋅(1::Integer)⋅0 = GT"
  "compare⋅(1::Integer)⋅1 = EQ"
  "compare⋅(0::Integer)⋅(numeral k) = LT"
  "compare⋅(numeral k)⋅(0::Integer) = GT"
  "Num.One < k ⟹ compare⋅(1::Integer)⋅(numeral k) = LT"
  "Num.One < k ⟹ compare⋅(numeral k)⋅(1::Integer) = GT"
  "compare⋅(numeral k::Integer)⋅(numeral l) =
    (if k < l then LT else if k > l then GT else EQ)"
  unfolding zero_Integer_def one_Integer_def numeral_Integer_eq
  by simp_all

lemma lt_Integer_numeral_simps [simp]:
  "lt⋅(0::Integer)⋅0 = FF"
  "lt⋅(0::Integer)⋅1 = TT"
  "lt⋅(1::Integer)⋅0 = FF"
  "lt⋅(1::Integer)⋅1 = FF"
  "lt⋅(0::Integer)⋅(numeral k) = TT"
  "lt⋅(numeral k)⋅(0::Integer) = FF"
  "Num.One < k ⟹ lt⋅(1::Integer)⋅(numeral k) = TT"
  "lt⋅(numeral k)⋅(1::Integer) = FF"
  "lt⋅(numeral k::Integer)⋅(numeral l) = (if k < l then TT else FF)"
  unfolding zero_Integer_def one_Integer_def numeral_Integer_eq
  by simp_all

lemma le_Integer_numeral_simps [simp]:
  "le⋅(0::Integer)⋅0 = TT"
  "le⋅(0::Integer)⋅1 = TT"
  "le⋅(1::Integer)⋅0 = FF"
  "le⋅(1::Integer)⋅1 = TT"
  "le⋅(0::Integer)⋅(numeral k) = TT"
  "le⋅(numeral k)⋅(0::Integer) = FF"
  "le⋅(1::Integer)⋅(numeral k) = TT"
  "Num.One < k ⟹ le⋅(numeral k)⋅(1::Integer) = FF"
  "le⋅(numeral k::Integer)⋅(numeral l) = (if k ≤ l then TT else FF)"
  unfolding zero_Integer_def one_Integer_def numeral_Integer_eq
  by simp_all

lemma MkI_eq_0_iff [simp]: "MkI⋅n = 0 ⟷ n = 0"
  unfolding zero_Integer_def by simp

lemma MkI_eq_1_iff [simp]: "MkI⋅n = 1 ⟷ n = 1"
  unfolding one_Integer_def by simp

lemma MkI_eq_numeral_iff [simp]: "MkI⋅n = numeral k ⟷ n = numeral k"
  unfolding numeral_Integer_eq by simp

lemma MkI_0: "MkI⋅0 = 0"
  by simp

lemma MkI_1: "MkI⋅1 = 1"
  by simp

lemma le_plus_1:
  fixes m :: "Integer"
  assumes "le⋅m⋅n = TT"
  shows "le⋅m⋅(n + 1) = TT"
proof -
  from assms have "n ≠ ⊥" by auto
  then have "le⋅n⋅(n + 1) = TT"
    by (cases n) (auto, metis le_MkI_MkI less_add_one less_le_not_le one_Integer_def plus_MkI_MkI)
  with assms show ?thesis by (auto dest: le_trans)
qed

subsection ‹Induction rules that do not break the abstraction›

lemma nonneg_Integer_induct [consumes 1, case_names 0 step]:
  fixes i :: Integer
  assumes i_nonneg: "le⋅0⋅i = TT"
    and zero: "P 0"
    and step: "⋀i. le⋅1⋅i = TT ⟹ P (i - 1) ⟹ P i"
  shows "P i"
proof (cases i)
  case bottom
  then have False using i_nonneg by simp
  then show ?thesis ..
next
  case (MkI integer)
  show ?thesis
  proof (cases integer)
    case neg
    then have False using i_nonneg MkI by (auto simp add: zero_Integer_def one_Integer_def)
    then show ?thesis ..
  next
    case (nonneg nat)
    have "P (MkI⋅(int nat))"
    proof(induct nat)
      case 0
      show ?case using zero by (simp add: zero_Integer_def)
    next
      case (Suc nat)
      have "le⋅1⋅(MkI⋅(int (Suc nat))) = TT"
        by (simp add: one_Integer_def)
      moreover
      have "P (MkI⋅(int (Suc nat)) - 1)"
        using Suc
        by (simp add: one_Integer_def)
      ultimately
      show ?case
        by (rule step)
    qed
    then show ?thesis using nonneg MkI by simp
  qed
qed

end