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 \<^theory>‹HOL-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::int⇒eint"]]
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
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
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
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_name>‹Groups.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_name>‹HOL.eq› \<^typ>‹eint›
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_name>‹Orderings.less_eq›
val dest_bal = HOLogic.dest_bin \<^const_name>‹Orderings.less_eq› \<^typ>‹eint›
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_name>‹Orderings.less›
val dest_bal = HOLogic.dest_bin \<^const_name>‹Orderings.less› \<^typ>‹eint›
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