Theory Extended_Int


section ‹Extended integers (i.e. with infinity)›

text‹
  This section formalizes the extended integers, which serve as the codomain for the $p$-adic 
  valuation. The element $\infty$ is added to the integers to serve as a maximxal element in the 
  order, which is the valuation of $0$.
›

theory Extended_Int
imports Main "HOL-Library.Countable" "HOL-Library.Order_Continuity" "HOL-Library.Extended_Nat"
begin

text‹
  The following is based very closely on the theory theoryHOL-Library.Extended_Nat from the 
  standard Isabelle distribution, with adaptations made to formalize the integers extended with
  an element for infinity. This is the standard range for the valuation function on a discretely
  valued ring such as the field of $p$-adic numbers, such as in cite"engler2005valued".
›

context
  fixes f :: "nat  'a::{canonically_ordered_monoid_add, linorder_topology, complete_linorder}"
begin

lemma sums_SUP[simp, intro]: "f sums (SUP n. i<n. f i)"
  unfolding sums_def by (intro LIMSEQ_SUP monoI sum_mono2 zero_le) auto

lemma suminf_eq_SUP: "suminf f = (SUP n. i<n. f i)"
  using sums_SUP by (rule sums_unique[symmetric])

end

subsection ‹Type definition›

text ‹
  We extend the standard natural numbers by a special value indicating
  infinity.
›

typedef eint = "UNIV :: int option set" ..


definition eint :: "int  eint" where
  "eint n = Abs_eint (Some n)"

instantiation eint :: infinity
begin

definition " = Abs_eint None"
instance ..

end

fun int_option_enumeration :: "int option  nat" where
"int_option_enumeration (Some n) = (if n  0 then nat (2*(n + 1)) else  nat (2*(-n) + 1))"|
"int_option_enumeration None = (0::nat)"

lemma int_option_enumeration_inj:
"inj int_option_enumeration"
proof 
  have pos_even: "n::int. n  0  even (int_option_enumeration (Some n))  (int_option_enumeration (Some n))> 0"
  proof-
    fix n::int assume "n 0" then have "(int_option_enumeration (Some n)) = nat (2*(n + 1))"
      by simp
    then show "even (int_option_enumeration (Some n))  0 < int_option_enumeration (Some n)"
      using 0  n even_nat_iff by force
  qed
  have neg_odd: "n::int. n < 0  odd (int_option_enumeration (Some n))"
    by (simp add: even_nat_iff)
  fix x y assume A: "x  UNIV" "y  UNIV" "int_option_enumeration x = int_option_enumeration y"
  show "x = y"
    apply(cases "x = None")
      using A pos_even neg_odd 
      apply (metis dvd_0_right int_option_enumeration.elims int_option_enumeration.simps(2) not_gr0 not_le)
    proof-
      assume "x None"
      then obtain n where n_def: "x = Some n"
        by auto 
      then have y_not_None: "y  None"
        using A 
        by (metis thesis. (n. x = Some n  thesis)  thesis
              add_cancel_right_right even_add int_option_enumeration.simps(2) 
              linorder_not_less neg_odd neq0_conv pos_even) 
      then obtain m where m_def: "y = Some m"
        by blast
      show ?thesis 
      proof(cases "n 0")
        case True
        then show ?thesis
          using n_def A neg_odd pos_even m_def int_option_enumeration.simps
          by (smt (verit) eq_nat_nat_iff)
      next
        case False
        then show ?thesis 
          using n_def A neg_odd pos_even m_def int_option_enumeration.simps(1)
          by (smt (verit) eq_nat_nat_iff)
      qed
  qed
qed

definition eint_enumeration where
"eint_enumeration = int_option_enumeration  Rep_eint"

lemma eint_enumeration_inj:
"inj eint_enumeration"
  unfolding eint_enumeration_def 
  using int_option_enumeration_inj Rep_eint_inject
  by (metis (mono_tags, lifting) comp_apply injD inj_on_def)
    
instance eint :: countable
proof
  show "to_int::eint  nat. inj to_int"
    using eint_enumeration_inj by blast 
qed

old_rep_datatype eint " :: eint"
proof -
  fix P i assume "j. P (eint j)" "P "
  then show "P i"
  proof induct
    case (Abs_eint y) then show ?case
      by (cases y rule: option.exhaust)
         (auto simp: eint_def infinity_eint_def)
  qed
qed (auto simp add: eint_def infinity_eint_def Abs_eint_inject)

declare [[coercion "eint::inteint"]]

lemmas eint2_cases = eint.exhaust[case_product eint.exhaust]
lemmas eint3_cases = eint.exhaust[case_product eint.exhaust eint.exhaust]

lemma not_infinity_eq [iff]: "(x  ) = (i. x = eint i)"
  by (cases x) auto

lemma not_eint_eq [iff]: "(y. x  eint y) = (x = )"
  by (cases x) auto

lemma eint_ex_split: "(c::eint. P c)  P   (c::int. P c)"
  by (metis eint.exhaust)

primrec the_eint :: "eint  int"
  where "the_eint (eint n) = n"


subsection ‹Constructors and numbers›

instantiation eint :: zero_neq_one
begin

definition
  "0 = eint 0"

definition
  "1 = eint 1"

instance
  proof qed (simp add: zero_eint_def one_eint_def)

end


lemma eint_0 [code_post]: "eint 0 = 0"
  by (simp add: zero_eint_def)

lemma eint_1 [code_post]: "eint 1 = 1"
  by (simp add: one_eint_def)

lemma eint_0_iff: "eint x = 0  x = 0" "0 = eint x  x = 0"
  by (auto simp add: zero_eint_def)

lemma eint_1_iff: "eint x = 1  x = 1" "1 = eint x  x = 1"
  by (auto simp add: one_eint_def)

lemma infinity_ne_i0 [simp]: "(::eint)  0"
  by (simp add: zero_eint_def)

lemma i0_ne_infinity [simp]: "0  (::eint)"
  by (simp add: zero_eint_def)

lemma zero_one_eint_neq:
  "¬ 0 = (1::eint)"
  "¬ 1 = (0::eint)"
  unfolding zero_eint_def one_eint_def by simp_all

lemma infinity_ne_i1 [simp]: "(::eint)  1"
  by (simp add: one_eint_def)

lemma i1_ne_infinity [simp]: "1  (::eint)"
  by (simp add: one_eint_def)
 
subsection ‹Addition›

instantiation eint :: comm_monoid_add
begin

definition [nitpick_simp]:
  "m + n = (case m of    | eint m  (case n of    | eint n  eint (m + n)))"

lemma plus_eint_simps [simp, code]:
  fixes q :: eint
  shows "eint m + eint n = eint (m + n)"
    and " + q = "
    and "q +  = "
  by (simp_all add: plus_eint_def split: eint.splits)

instance
proof
  fix n m q :: eint
  show "n + m + q = n + (m + q)"
    by (cases n m q rule: eint3_cases) auto
  show "n + m = m + n"
    by (cases n m rule: eint2_cases) auto
  show "0 + n = n"
    by (cases n) (simp_all add: zero_eint_def)
qed

end

lemma eSuc_eint: "(eint n) + 1 = eint (n + 1)"
  by (simp add: one_eint_def)

lemma eSuc_infinity [simp]: "  + (1::eint) = "
  unfolding plus_eint_def 
  by auto 

lemma eSuc_inject [simp]: " m + (1::eint)=  n + 1  m = n"
  unfolding plus_eint_def 
  apply(cases "m = ")
  apply (metis (no_types, lifting) eSuc_eint 
    eint.distinct(2) eint.exhaust eint.simps(4) eint.simps(5) plus_eint_def)
  apply(cases "n = ")
  using eSuc_eint plus_eint_def apply auto[1]
  unfolding one_eint_def 
  using add.commute eSuc_eint 
  by auto
     
lemma eSuc_eint_iff: "x + 1 = eint y  (n. y = n + 1  x = eint n)"
  apply(cases "x = ")
  apply simp
  unfolding plus_eint_def one_eint_def 
  using eSuc_eint 
  by auto

lemma enat_eSuc_iff: "eint y = x + 1  (n. y = n + 1  eint n = x)"
  using eSuc_eint_iff 
  by metis

lemma iadd_Suc: "((m::eint) + 1) + n = (m + n) + 1"
  by (metis ab_semigroup_add_class.add_ac(1) add.assoc add.commute)
  

lemma iadd_Suc_right: "(m::eint) + (n + 1) = (m + n) + 1"
  using add.assoc[of m n 1] by auto 

subsection ‹Multiplication›

instantiation eint :: "{comm_semiring}"
begin

definition times_eint_def [nitpick_simp]:
  "m * n = (case m of     | eint m 
    (case n of    | eint n  eint (m * n)))"

lemma times_eint_simps [simp, code]:
  "eint m * eint n = eint (m * n)"
  " *  = (::eint)"
  " * eint n = "
  "eint m *  = "
  unfolding times_eint_def zero_eint_def
  by (simp_all split: eint.split)

lemma sum_infinity_imp_summand_infinity:
  assumes "a + b = (::eint)"
  shows "a =   b = "
  using assms 
  by (metis  not_eint_eq plus_eint_simps(1))

lemma sum_finite_imp_summands_finite:
  assumes "a + b  (::eint)"
  shows "a  " "b  "
  using assms eint.simps(5) apply fastforce
  using assms eint.simps(5) by fastforce


instance
proof
  fix a b c :: eint
  show "(a * b) * c = a * (b * c)"
    unfolding times_eint_def zero_eint_def
    by (simp split: eint.split)
  show comm: "a * b = b * a"
    unfolding times_eint_def zero_eint_def
    by (simp split: eint.split)
  show distr: "(a + b) * c = a * c + b * c"
    unfolding times_eint_def plus_eint_def 
    apply(cases "a + b = ")
    apply(cases "a = ")
    apply simp
    using sum_infinity_imp_summand_infinity[of a b] 
    apply (metis eint.simps(5) plus_eint_def plus_eint_simps(3))
    apply(cases "c = ")
     apply (metis eint.exhaust plus_eint_def plus_eint_simps(3) times_eint_def times_eint_simps(4))
    using sum_finite_imp_summands_finite[of a b] 
    apply auto 
    by (simp add: semiring_normalization_rules(1))
qed    


end

lemma mult_one_right[simp]:
"(n::eint)*1 = n"
  apply(cases "n = ")
  apply (simp add: one_eint_def)
  by (metis eint2_cases mult_cancel_left2 one_eint_def times_eint_simps(1))

lemma mult_one_left[simp]:
"1*(n::eint) = n"
  by (metis mult.commute mult_one_right)

lemma mult_eSuc: "((m::eint) + 1) * n = m * n + n"
  by (simp add: distrib_right)
 
lemma mult_eSuc': "((m::eint) + 1) * n = n + m * n"
  using mult_eSuc add.commute by simp 

lemma mult_eSuc_right: "(m::eint) * (n + 1) =  m * n +  m "
  by(simp add: distrib_left)

lemma mult_eSuc_right': "(m::eint) * (n + 1) =  m + m * n  "
  using mult_eSuc_right add.commute by simp 


subsection ‹Numerals›

lemma numeral_eq_eint:
  "numeral k = eint (numeral k)"
  by simp

lemma eint_numeral [code_abbrev]:
  "eint (numeral k) = numeral k"
  using numeral_eq_eint ..

lemma infinity_ne_numeral [simp]: "(::eint)  numeral k"
  by auto

lemma numeral_ne_infinity [simp]: "numeral k  (::eint)"
  by simp
  
subsection ‹Subtraction›

instantiation eint :: minus
begin

definition diff_eint_def:
"a - b = (case a of (eint x)  (case b of (eint y)  eint (x - y) |   )
          |   )"

instance ..

end




lemma idiff_eint_eint [simp, code]: "eint a - eint b = eint (a - b)"
  by (simp add: diff_eint_def)

lemma idiff_infinity [simp, code]: " - n = (::eint)"
  by (simp add: diff_eint_def)

lemma idiff_infinity_right [simp, code]: "eint a -  = "
  by (simp add: diff_eint_def)

lemma idiff_0 [simp]: "(0::eint) - n = -n"
  by (cases n, simp_all add: zero_eint_def)

lemmas idiff_eint_0 [simp] = idiff_0 [unfolded zero_eint_def]

lemma idiff_0_right [simp]: "(n::eint) - 0 = n"
  by (cases n) (simp_all add: zero_eint_def)

lemmas idiff_eint_0_right [simp] = idiff_0_right [unfolded zero_eint_def]

lemma idiff_self [simp]: "n    (n::eint) - n = 0"
  by (auto simp: zero_eint_def)


lemma eSuc_minus_eSuc [simp]: "((n::eint) + 1) - (m + 1) = n - m"
  apply(cases "n = ")
  apply simp 
  apply(cases "m = ")
  apply (metis eSuc_infinity eint.exhaust idiff_infinity_right infinity_ne_i1 sum_infinity_imp_summand_infinity)
proof-
  assume A: "n " "m  "
  obtain a where a_def: "n = eint a"
    using A 
    by auto
  obtain b where b_def: "m = eint b"
    using A 
    by auto 
  show ?thesis 
    using  idiff_eint_eint[of "a + 1" "b + 1"]
           idiff_eint_eint[of a b]
  by (simp add: a_def b_def eSuc_eint)
qed
  
lemma eSuc_minus_1 [simp]: "((n::eint)+ 1) - 1 = n"
  using eSuc_minus_eSuc[of n 0]
  by auto 


(*lemmas idiff_self_eq_0_eint = idiff_self_eq_0[unfolded zero_eint_def]*)

subsection ‹Ordering›

instantiation eint :: linordered_ab_semigroup_add
begin

definition [nitpick_simp]:
  "m  n = (case n of eint n1  (case m of eint m1  m1  n1 |   False)
    |   True)"

definition [nitpick_simp]:
  "m < n = (case m of eint m1  (case n of eint n1  m1 < n1 |   True)
    |   False)"

lemma eint_ord_simps [simp]:
  "eint m  eint n  m  n"
  "eint m < eint n  m < n"
  "q  (::eint)"
  "q < (::eint)  q  "
  "(::eint)  q  q = "
  "(::eint) < q  False"
  by (simp_all add: less_eq_eint_def less_eint_def split: eint.splits)

lemma numeral_le_eint_iff[simp]:
  shows "numeral m  eint n  numeral m  n"
  by auto

lemma numeral_less_eint_iff[simp]:
  shows "numeral m < eint n  numeral m < n"
  by simp

lemma eint_ord_code [code]:
  "eint m  eint n  m  n"
  "eint m < eint n  m < n"
  "q  (::eint)  True"
  "eint m <   True"
  "  eint n  False"
  "(::eint) < q  False"
  by simp_all

lemma eint_ord_plus_one[simp]:
  assumes "eint n  x"
  assumes "x < y"
  shows "eint (n + 1)  y"
proof-
  obtain m where "x = eint m"
    using assms(2) 
    by fastforce
  show ?thesis apply(cases "y = ")
  apply simp
    using x = eint m assms(1) assms(2) 
    by force
qed

instance
  by standard (auto simp add: less_eq_eint_def less_eint_def plus_eint_def split: eint.splits)

end

instance eint :: "{strict_ordered_comm_monoid_add}"
proof
  show "a < b  c < d  a + c < b + d" for a b c d :: eint
    by (cases a b c d rule: eint2_cases[case_product eint2_cases]) auto
qed 

(* BH: These equations are already proven generally for any type in
class linordered_semidom. However, eint is not in that class because
it does not have the cancellation property. Would it be worthwhile to
a generalize linordered_semidom to a new class that includes eint? *)

lemma add_diff_assoc_eint: "z  y  x + (y - z) = x + y - (z::eint)"
by(cases x)(auto simp add: diff_eint_def split: eint.split)

lemma eint_ord_number [simp]:
  "(numeral m :: eint)  numeral n  (numeral m :: nat)  numeral n"
  "(numeral m :: eint) < numeral n  (numeral m :: nat) < numeral n"
  apply simp 
  by simp

lemma infinity_ileE [elim!]: "  eint m  R"
  by simp  

lemma infinity_ilessE [elim!]: " < eint m  R"
  by simp

lemma imult_infinity: "(0::eint) < n   * n = "
  by (simp add: zero_eint_def less_eint_def split: eint.splits)

lemma imult_infinity_right: "(0::eint) < n  n *  = "
  by (simp add: zero_eint_def less_eint_def split: eint.splits)

lemma min_eint_simps [simp]:
  "min (eint m) (eint n) = eint (min m n)"
  "min q (::eint) = q"
  "min (::eint) q = q"
  by (auto simp add: min_def)

lemma max_eint_simps [simp]:
  "max (eint m) (eint n) = eint (max m n)"
  "max q  = (::eint)"
  "max  q = (::eint)"
  by (simp_all add: max_def)

lemma eint_ile: "n  eint m  k. n = eint k"
  by (cases n) simp_all

lemma eint_iless: "n < eint m  k. n = eint k"
  by (cases n) simp_all

lemma iadd_le_eint_iff:
  "x + y  eint n  (y' x'. x = eint x'  y = eint y'  x' + y'  n)"
by(cases x y rule: eint.exhaust[case_product eint.exhaust]) simp_all

lemma chain_incr: "i. j. Y i < Y j  j. eint k < Y j"
proof-
  assume A: "i. j. Y i < Y j"
  then have "i. n::int. Y i = eint n"
    by (metis eint.exhaust eint_ord_simps(6))
  then obtain i n where in_def: "Y (i::'a) = eint n"
    by blast 
  show "j. eint k < Y j"
  proof(rule ccontr)
    assume C: "¬(j. eint k < Y j)"
    then have C':"j. Y j  eint k"
      using le_less_linear 
      by blast
    then have "Y (i::'a)  eint k"
      by simp     
    have "m::nat. j::'a. Y j  eint (n + int m)"
    proof- fix m
      show "j::'a. Y j  eint (n + int m)"
        apply(induction m)
         apply (metis in_def int_ops(1) order_refl plus_int_code(1))
      proof- fix m
        assume "j. eint (n + int m)  Y j"
        then obtain j where j_def: "eint (n + int m)  Y j"
          by blast 
        obtain j' where j'_def: "Y j < Y j'"
          using A by blast 
        have "eint (n + int (Suc m)) = eint (n + m + 1)"
          by auto
        then have "eint (n + int (Suc m))  Y j'"
          using j_def j'_def  eint_ord_plus_one[of "n + m" "Y j" "Y j'"]
          by presburger
        then show "j. eint (n + int (Suc m))  Y j" 
          by blast 
      qed
    qed
    then show False 
      by (metis A C Y i  eint k   eint_ord_simps(1) in_def 
          order.not_eq_order_implies_strict zle_iff_zadd)
  qed
qed

lemma eint_ord_Suc:
  assumes "(x::eint) < y"
  shows "x + 1 < y + 1"
  apply(cases "y = ")
  using assms i1_ne_infinity sum_infinity_imp_summand_infinity 
   apply fastforce
  by (metis add_mono_thms_linordered_semiring(3) assms eSuc_inject order_less_le)

lemma eSuc_ile_mono [simp]: "(n::eint) + 1  m+ 1  n  m"
  by (meson add_mono_thms_linordered_semiring(3) eint_ord_Suc linorder_not_le)

lemma eSuc_mono [simp]: "(n::eint) + 1 < m+ 1  n < m"
  by (meson add_mono_thms_linordered_semiring(3) eint_ord_Suc linorder_not_le)

lemma ile_eSuc [simp]: "(n::eint)  n + 1"
  by (metis add.right_neutral add_left_mono eint_1_iff(2) eint_ord_code(1) linear not_one_le_zero zero_eint_def)

lemma ileI1: "(m::eint) < n  m + 1  n"
  by (metis eSuc_eint eint.exhaust eint_ex_split eint_iless eint_ord_Suc eint_ord_code(6) 
      eint_ord_plus_one eint_ord_simps(3) less_le_trans linear )
 
lemma Suc_ile_eq: "eint (m +1)  n  eint m < n"
  by (cases n) auto

lemma iless_Suc_eq [simp]: "eint m < n + 1  eint m  n"
  by (metis Suc_ile_eq eSuc_eint eSuc_ile_mono)

lemma eSuc_max: "(max (x::eint) y) + 1 = max (x+1) (y+1)"
  by (simp add: max_def)

lemma eSuc_Max:
  assumes "finite A" "A  ({}::eint set)"
  shows " (Max A) + 1 = Max ((+)1 ` A)"
using assms proof induction
  case (insert x A)
  thus ?case 
    using Max_insert[of A x] Max_singleton[of x] add.commute[of 1] eSuc_max finite_imageI 
          image_insert image_is_empty
  by (simp add: add.commute hom_Max_commute)
qed simp

instantiation eint :: "{order_top}"
begin

definition top_eint :: eint where "top_eint = "

instance
  by standard (simp add: top_eint_def)

end

lemma finite_eint_bounded:
  assumes le_fin: "y. y  A  eint m  y  y  eint n"
  shows "finite A"
proof (rule finite_subset)
  show "finite (eint ` {m..n})" by blast
  have "A  {eint m..eint n}" using le_fin by fastforce
  also have "  eint ` {m..n}"
    apply (rule subsetI)
    subgoal for x by (cases x) auto
    done
  finally show "A  eint ` {m..n}" .
qed


subsection ‹Cancellation simprocs›

lemma add_diff_cancel_eint[simp]: "x    x + y - x = (y::eint)"
by (metis add.commute add.right_neutral add_diff_assoc_eint idiff_self order_refl)

lemma eint_add_left_cancel: "a + b = a + c  a = (::eint)  b = c"
  unfolding plus_eint_def by (simp split: eint.split)

lemma eint_add_left_cancel_le: "a + b  a + c  a = (::eint)  b  c"
  unfolding plus_eint_def by (simp split: eint.split)

lemma eint_add_left_cancel_less: "a + b < a + c  a  (::eint)  b < c"
  unfolding plus_eint_def by (simp split: eint.split)

lemma plus_eq_infty_iff_eint: "(m::eint) + n =   m=  n="
using eint_add_left_cancel by fastforce

ML structure Cancel_Enat_Common =
struct
  (* copied from src/HOL/Tools/nat_numeral_simprocs.ML *)
  fun find_first_t _    _ []         = raise TERM("find_first_t", [])
    | find_first_t past u (t::terms) =
          if u aconv t then (rev past @ terms)
          else find_first_t (t::past) u terms

  fun dest_summing (Const (const_nameGroups.plus, _) $ t $ u, ts) =
        dest_summing (t, dest_summing (u, ts))
    | dest_summing (t, ts) = t :: ts

  val mk_sum = Arith_Data.long_mk_sum
  fun dest_sum t = dest_summing (t, [])
  val find_first = find_first_t []
  val trans_tac = Numeral_Simprocs.trans_tac
  val norm_ss =
    simpset_of (put_simpset HOL_basic_ss context
      addsimps @{thms ac_simps add_0_left add_0_right})
  fun norm_tac ctxt = ALLGOALS (simp_tac (put_simpset norm_ss ctxt))
  fun simplify_meta_eq ctxt cancel_th th =
    Arith_Data.simplify_meta_eq [] ctxt
      ([th, cancel_th] MRS trans)
  fun mk_eq (a, b) = HOLogic.mk_Trueprop (HOLogic.mk_eq (a, b))
end

structure Eq_Enat_Cancel = ExtractCommonTermFun
(open Cancel_Enat_Common
  val mk_bal = HOLogic.mk_eq
  val dest_bal = HOLogic.dest_bin const_nameHOL.eq typeint
  fun simp_conv _ _ = SOME @{thm eint_add_left_cancel}
)

structure Le_Enat_Cancel = ExtractCommonTermFun
(open Cancel_Enat_Common
  val mk_bal = HOLogic.mk_binrel const_nameOrderings.less_eq
  val dest_bal = HOLogic.dest_bin const_nameOrderings.less_eq typeint
  fun simp_conv _ _ = SOME @{thm eint_add_left_cancel_le}
)

structure Less_Enat_Cancel = ExtractCommonTermFun
(open Cancel_Enat_Common
  val mk_bal = HOLogic.mk_binrel const_nameOrderings.less
  val dest_bal = HOLogic.dest_bin const_nameOrderings.less typeint
  fun simp_conv _ _ = SOME @{thm eint_add_left_cancel_less}
)

simproc_setup eint_eq_cancel
  ("(l::eint) + m = n" | "(l::eint) = m + n") =
  fn phi => fn ctxt => fn ct => Eq_Enat_Cancel.proc ctxt (Thm.term_of ct)

simproc_setup eint_le_cancel
  ("(l::eint) + m  n" | "(l::eint)  m + n") =
  fn phi => fn ctxt => fn ct => Le_Enat_Cancel.proc ctxt (Thm.term_of ct)

simproc_setup eint_less_cancel
  ("(l::eint) + m < n" | "(l::eint) < m + n") =
  fn phi => fn ctxt => fn ct => Less_Enat_Cancel.proc ctxt (Thm.term_of ct)

text ‹TODO: add regression tests for these simprocs›

text ‹TODO: add simprocs for combining and cancelling numerals›

subsection ‹Well-ordering›

lemma less_eintE:
  "[| n < eint m; !!k. n = eint k ==> k < m ==> P |] ==> P"
by (induct n) auto

lemma less_infinityE:
  "[| n < ; !!k. n = eint k ==> P |] ==> P"
by (induct n) auto


subsection ‹Traditional theorem names›

lemmas eint_defs = zero_eint_def one_eint_def 
  plus_eint_def less_eq_eint_def less_eint_def

instantiation eint :: uminus
begin

definition 
"- b = (case b of    | eint m  eint (-m))"

lemma eint_uminus_eq:
"(a::eint) + (-a) = a - a"
  apply(induction a)
  apply (simp add: uminus_eint_def)
  by simp




instance..
end

section‹Additional Lemmas (Useful for the Proof of Hensel's Lemma)›

lemma eint_mult_mono:
  assumes "(c::eint) > 0  c  "
  assumes "k > n"
  shows "k*c > n*c"  
  using assms apply(induction k, induction n, induction c)
  by(auto simp add: zero_eint_def)

lemma eint_mult_mono':
  assumes "(c::eint)  0  c  "
  assumes "k > n"
  shows "k*c  n*c"  
  apply(cases "c = 0")
   apply (metis add.right_neutral assms(2) eint_add_left_cancel eint_ord_code(3) 
         eint_ord_simps(4) eq_iff less_le_trans mult.commute mult_eSuc_right' 
         mult_one_right not_less times_eint_simps(4) zero_eint_def)
    using assms eint_mult_mono 
    by (simp add: le_less)

lemma eint_minus_le:
  assumes "(b::eint) < c"
  shows "c - b > 0"
  using assms apply(induction b, induction c) 
  by (auto simp add: zero_eint_def)  

lemma eint_nat_times:
  assumes "(c::eint) > 0"
  shows "(Suc n)*(c::eint) > 0"
  using assms  apply(induction c)
  apply (simp add: zero_eint_def)
  by simp

lemma eint_pos_times_is_pos:
  assumes "(c::eint) > 0"
  assumes "b > 0"
  shows "b*c > 0"
  using assms apply(induction c, induction b)
  by(auto simp add: zero_eint_def imult_infinity_right)

lemma eint_nat_is_pos:
"eint (Suc n) > 0"
  by (simp add: zero_eint_def)

lemma eint_pow_int_is_pos:
  assumes "n > 0"
  shows "eint n > 0"
  using assms by (simp add: zero_eint_def)

lemma eint_nat_times':
  assumes "(c::eint)  0"
  shows "(Suc n)*c  0"  
  using assms zero_eint_def by fastforce

lemma eint_pos_int_times_ge:
  assumes "(c::eint)  0"
  assumes "n > 0"
  shows "eint n * c  c"
  using assms apply(induction c)
   apply (metis Extended_Int.ileI1 Groups.mult_ac(2) add_0_left eint_mult_mono' eint_pow_int_is_pos
      mult_one_right nless_le not_less times_eint_simps(4))
  apply simp
  done

lemma eint_pos_int_times_gt:
  assumes "(c::eint) > 0"
  assumes "c "
  assumes "n > 1"
  shows "eint n * c > c"
  using assms eint_mult_mono[of c 1 "eint n"]
  by (metis eint_ord_simps(2) mult_one_left one_eint_def)

lemma eint_add_cancel_fact[simp]:
  assumes "(c::eint)  "
  shows "c + (b - c) = b"
  using assms apply(induction c, induction b)
  by auto 

lemma nat_mult_not_infty[simp]:
  assumes "c  "
  shows "(eint n) * c  "
  using assms by auto

lemma eint_minus_distl:
  assumes "(b::eint)  d"
  shows "b*c - d*c = (b-d)*c"
  using assms apply(induction c, induction b, induction d)
  apply (metis add_diff_cancel_eint distrib_right eint.distinct(2) eint_add_cancel_fact nat_mult_not_infty)
    apply simp
      apply simp
        by (simp add: mult.commute times_eint_def)    

lemma eint_minus_distr:
  assumes "(b::eint)  d"
  shows "c*(b - d) = c*b - c*d"
  by (metis assms eint_minus_distl mult.commute)  

lemma eint_int_minus_distr:
"(eint n)*c - (eint m)*c = eint (n - m) * c"
  by (metis add.right_neutral distrib_right eint_add_left_cancel eint_minus_distl idiff_eint_eint
      idiff_infinity idiff_self infinity_ne_i0 nat_mult_not_infty not_eint_eq times_eint_simps(4))

lemma eint_2_minus_1_mult[simp]:
"2*(b::eint) - b = b"
proof -
  have "e. (::eint) * e = "
  by (simp add: times_eint_def)
  then show ?thesis
    by (metis add_diff_cancel_eint idiff_infinity mult.commute mult_eSuc_right' mult_one_right one_add_one one_eint_def plus_eint_simps(1))
qed

lemma eint_minus_comm:
"(d::eint) + b - c = d - c + b"
apply(induction c )
  apply (metis add.assoc add_diff_cancel_eint eint.distinct(2) eint_add_cancel_fact)
    apply(induction d)
    apply (metis distrib_left eint2_cases eint_minus_distl i1_ne_infinity idiff_infinity_right 
           mult_one_left plus_eq_infty_iff_eint sum_infinity_imp_summand_infinity times_eint_simps(3))
      apply(induction b)
        apply simp
          by simp

lemma ge_plus_pos_imp_gt:
  assumes "(c::eint) "
  assumes "(b::eint) > 0"
  assumes "d  c + b"
  shows "d > c"
  using assms apply(induction d, induction c)
  apply (metis add.comm_neutral assms(2) eint_add_left_cancel_less less_le_trans)
   apply blast
    by simp

lemma eint_minus_ineq:
  assumes "(c::eint) "
  assumes "b  d"
  shows "b - c  d - c"
  by (metis add_left_mono antisym assms(1) assms(2) eint_add_cancel_fact linear)

lemma eint_minus_ineq':
  assumes "(c::eint) "
  assumes "b  d"
  assumes "(e::eint) > 0"
  assumes "e  "
  shows "e*(b - c)  e*(d - c)"
  using assms eint_minus_ineq 
  by (metis eint_mult_mono' eq_iff less_le mult.commute)

lemma eint_minus_ineq'':
  assumes "(c::eint) "
  assumes "b  d"
  assumes "(e::eint) > 0"
  assumes "e  "
  shows "e*(b - c)  e*d - e*c"
  using assms eint_minus_ineq' 
  proof -
    have "e. (0::eint) + e = e"
      by simp
    then have f1: "e * 0 = 0"
      by (metis add_diff_cancel_eint assms(4) idiff_self mult_eSuc_right' mult_one_right)
    have "  c * e"
      using assms(1) assms(4) eint_pos_times_is_pos by auto
    then show ?thesis
      using f1 by (metis assms(1) assms(2) assms(3) assms(4) eint_minus_distl eint_minus_ineq' idiff_self mult.commute)
  qed

lemma eint_min_ineq:
  assumes "(b::eint)  min c d"
  assumes "c > e"
  assumes "d > e"
  shows "b > e"
  by (meson assms(1) assms(2) assms(3) less_le_trans min_le_iff_disj)

lemma eint_plus_times:
  assumes "(d::eint)  0"
  assumes "(b::eint)  c + (eint k)*d"
  assumes "k  l"
  shows "b  c + l*d" 
proof-
  have "k*d  l*d"
    by (smt (verit) assms(1) assms(3) eint_mult_mono' eint_ord_simps(2) eq_iff times_eint_simps(4))
  thus ?thesis 
    by (meson add_mono_thms_linordered_semiring(2) assms(2) order_subst2)
qed
end