(* Title: HOL/Int.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Author: Tobias Nipkow, Florian Haftmann, TU Muenchen
*)
section \The Integers as Equivalence Classes over Pairs of Natural Numbers\
theory Int
imports Equiv_Relations Power Quotient Fun_Def
begin
subsection \Definition of integers as a quotient type\
definition intrel :: "(nat \ nat) \ (nat \ nat) \ bool"
where "intrel = (\(x, y) (u, v). x + v = u + y)"
lemma intrel_iff [simp]: "intrel (x, y) (u, v) \ x + v = u + y"
by (simp add: intrel_def)
quotient_type int = "nat \ nat" / "intrel"
morphisms Rep_Integ Abs_Integ
proof (rule equivpI)
show "reflp intrel" by (auto simp: reflp_def)
show "symp intrel" by (auto simp: symp_def)
show "transp intrel" by (auto simp: transp_def)
qed
lemma eq_Abs_Integ [case_names Abs_Integ, cases type: int]:
"(\x y. z = Abs_Integ (x, y) \ P) \ P"
by (induct z) auto
subsection \Integers form a commutative ring\
instantiation int :: comm_ring_1
begin
lift_definition zero_int :: "int" is "(0, 0)" .
lift_definition one_int :: "int" is "(1, 0)" .
lift_definition plus_int :: "int \ int \ int"
is "\(x, y) (u, v). (x + u, y + v)"
by clarsimp
lift_definition uminus_int :: "int \ int"
is "\(x, y). (y, x)"
by clarsimp
lift_definition minus_int :: "int \ int \ int"
is "\(x, y) (u, v). (x + v, y + u)"
by clarsimp
lift_definition times_int :: "int \ int \ int"
is "\(x, y) (u, v). (x*u + y*v, x*v + y*u)"
proof (clarsimp)
fix s t u v w x y z :: nat
assume "s + v = u + t" and "w + z = y + x"
then have "(s + v) * w + (u + t) * x + u * (w + z) + v * (y + x) =
(u + t) * w + (s + v) * x + u * (y + x) + v * (w + z)"
by simp
then show "(s * w + t * x) + (u * z + v * y) = (u * y + v * z) + (s * x + t * w)"
by (simp add: algebra_simps)
qed
instance
by standard (transfer; clarsimp simp: algebra_simps)+
end
abbreviation int :: "nat \ int"
where "int \ of_nat"
lemma int_def: "int n = Abs_Integ (n, 0)"
by (induct n) (simp add: zero_int.abs_eq, simp add: one_int.abs_eq plus_int.abs_eq)
lemma int_transfer [transfer_rule]: "(rel_fun (op =) pcr_int) (\n. (n, 0)) int"
by (simp add: rel_fun_def int.pcr_cr_eq cr_int_def int_def)
lemma int_diff_cases: obtains (diff) m n where "z = int m - int n"
by transfer clarsimp
subsection \Integers are totally ordered\
instantiation int :: linorder
begin
lift_definition less_eq_int :: "int \ int \ bool"
is "\(x, y) (u, v). x + v \ u + y"
by auto
lift_definition less_int :: "int \ int \ bool"
is "\(x, y) (u, v). x + v < u + y"
by auto
instance
by standard (transfer, force)+
end
instantiation int :: distrib_lattice
begin
definition "(inf :: int \ int \ int) = min"
definition "(sup :: int \ int \ int) = max"
instance
by standard (auto simp add: inf_int_def sup_int_def max_min_distrib2)
end
subsection \Ordering properties of arithmetic operations\
instance int :: ordered_cancel_ab_semigroup_add
proof
fix i j k :: int
show "i \ j \ k + i \ k + j"
by transfer clarsimp
qed
text \Strict Monotonicity of Multiplication.\
text \Strict, in 1st argument; proof is by induction on \k > 0\.\
lemma zmult_zless_mono2_lemma: "i < j \ 0 < k \ int k * i < int k * j"
for i j :: int
proof (induct k)
case 0
then show ?case by simp
next
case (Suc k)
then show ?case
by (cases "k = 0") (simp_all add: distrib_right add_strict_mono)
qed
lemma zero_le_imp_eq_int: "0 \ k \ \n. k = int n"
for k :: int
apply transfer
apply clarsimp
apply (rule_tac x="a - b" in exI)
apply simp
done
lemma zero_less_imp_eq_int: "0 < k \ \n>0. k = int n"
for k :: int
apply transfer
apply clarsimp
apply (rule_tac x="a - b" in exI)
apply simp
done
lemma zmult_zless_mono2: "i < j \ 0 < k \ k * i < k * j"
for i j k :: int
by (drule zero_less_imp_eq_int) (auto simp add: zmult_zless_mono2_lemma)
text \The integers form an ordered integral domain.\
instantiation int :: linordered_idom
begin
definition zabs_def: "\i::int\ = (if i < 0 then - i else i)"
definition zsgn_def: "sgn (i::int) = (if i = 0 then 0 else if 0 < i then 1 else - 1)"
instance
proof
fix i j k :: int
show "i < j \ 0 < k \ k * i < k * j"
by (rule zmult_zless_mono2)
show "\i\ = (if i < 0 then -i else i)"
by (simp only: zabs_def)
show "sgn (i::int) = (if i=0 then 0 else if 0* w + 1 \ z"
for w z :: int
by transfer clarsimp
lemma zless_iff_Suc_zadd: "w < z \ (\n. z = w + int (Suc n))"
for w z :: int
apply transfer
apply auto
apply (rename_tac a b c d)
apply (rule_tac x="c+b - Suc(a+d)" in exI)
apply arith
done
lemma zabs_less_one_iff [simp]: "\z\ < 1 \ z = 0" (is "?lhs \ ?rhs")
for z :: int
proof
assume ?rhs
then show ?lhs by simp
next
assume ?lhs
with zless_imp_add1_zle [of "\z\" 1] have "\z\ + 1 \ 1" by simp
then have "\z\ \ 0" by simp
then show ?rhs by simp
qed
lemmas int_distrib =
distrib_right [of z1 z2 w]
distrib_left [of w z1 z2]
left_diff_distrib [of z1 z2 w]
right_diff_distrib [of w z1 z2]
for z1 z2 w :: int
subsection \Embedding of the Integers into any \ring_1\: \of_int\\
context ring_1
begin
lift_definition of_int :: "int \ 'a"
is "\(i, j). of_nat i - of_nat j"
by (clarsimp simp add: diff_eq_eq eq_diff_eq diff_add_eq
of_nat_add [symmetric] simp del: of_nat_add)
lemma of_int_0 [simp]: "of_int 0 = 0"
by transfer simp
lemma of_int_1 [simp]: "of_int 1 = 1"
by transfer simp
lemma of_int_add [simp]: "of_int (w + z) = of_int w + of_int z"
by transfer (clarsimp simp add: algebra_simps)
lemma of_int_minus [simp]: "of_int (- z) = - (of_int z)"
by (transfer fixing: uminus) clarsimp
lemma of_int_diff [simp]: "of_int (w - z) = of_int w - of_int z"
using of_int_add [of w "- z"] by simp
lemma of_int_mult [simp]: "of_int (w*z) = of_int w * of_int z"
by (transfer fixing: times) (clarsimp simp add: algebra_simps)
lemma mult_of_int_commute: "of_int x * y = y * of_int x"
by (transfer fixing: times) (auto simp: algebra_simps mult_of_nat_commute)
text \Collapse nested embeddings.\
lemma of_int_of_nat_eq [simp]: "of_int (int n) = of_nat n"
by (induct n) auto
lemma of_int_numeral [simp, code_post]: "of_int (numeral k) = numeral k"
by (simp add: of_nat_numeral [symmetric] of_int_of_nat_eq [symmetric])
lemma of_int_neg_numeral [code_post]: "of_int (- numeral k) = - numeral k"
by simp
lemma of_int_power [simp]: "of_int (z ^ n) = of_int z ^ n"
by (induct n) simp_all
lemma of_int_of_bool [simp]:
"of_int (of_bool P) = of_bool P"
by auto
end
context ring_char_0
begin
lemma of_int_eq_iff [simp]: "of_int w = of_int z \ w = z"
by transfer (clarsimp simp add: algebra_simps of_nat_add [symmetric] simp del: of_nat_add)
text \Special cases where either operand is zero.\
lemma of_int_eq_0_iff [simp]: "of_int z = 0 \ z = 0"
using of_int_eq_iff [of z 0] by simp
lemma of_int_0_eq_iff [simp]: "0 = of_int z \ z = 0"
using of_int_eq_iff [of 0 z] by simp
lemma of_int_eq_1_iff [iff]: "of_int z = 1 \ z = 1"
using of_int_eq_iff [of z 1] by simp
end
context linordered_idom
begin
text \Every \linordered_idom\ has characteristic zero.\
subclass ring_char_0 ..
lemma of_int_le_iff [simp]: "of_int w \ of_int z \ w \ z"
by (transfer fixing: less_eq)
(clarsimp simp add: algebra_simps of_nat_add [symmetric] simp del: of_nat_add)
lemma of_int_less_iff [simp]: "of_int w < of_int z \ w < z"
by (simp add: less_le order_less_le)
lemma of_int_0_le_iff [simp]: "0 \ of_int z \ 0 \ z"
using of_int_le_iff [of 0 z] by simp
lemma of_int_le_0_iff [simp]: "of_int z \ 0 \ z \ 0"
using of_int_le_iff [of z 0] by simp
lemma of_int_0_less_iff [simp]: "0 < of_int z \ 0 < z"
using of_int_less_iff [of 0 z] by simp
lemma of_int_less_0_iff [simp]: "of_int z < 0 \ z < 0"
using of_int_less_iff [of z 0] by simp
lemma of_int_1_le_iff [simp]: "1 \ of_int z \ 1 \ z"
using of_int_le_iff [of 1 z] by simp
lemma of_int_le_1_iff [simp]: "of_int z \ 1 \ z \ 1"
using of_int_le_iff [of z 1] by simp
lemma of_int_1_less_iff [simp]: "1 < of_int z \ 1 < z"
using of_int_less_iff [of 1 z] by simp
lemma of_int_less_1_iff [simp]: "of_int z < 1 \ z < 1"
using of_int_less_iff [of z 1] by simp
lemma of_int_pos: "z > 0 \ of_int z > 0"
by simp
lemma of_int_nonneg: "z \ 0 \ of_int z \ 0"
by simp
lemma of_int_abs [simp]: "of_int \x\ = \of_int x\"
by (auto simp add: abs_if)
lemma of_int_lessD:
assumes "\of_int n\ < x"
shows "n = 0 \ x > 1"
proof (cases "n = 0")
case True
then show ?thesis by simp
next
case False
then have "\n\ \ 0" by simp
then have "\n\ > 0" by simp
then have "\n\ \ 1"
using zless_imp_add1_zle [of 0 "\n\"] by simp
then have "\of_int n\ \ 1"
unfolding of_int_1_le_iff [of "\n\", symmetric] by simp
then have "1 < x" using assms by (rule le_less_trans)
then show ?thesis ..
qed
lemma of_int_leD:
assumes "\of_int n\ \ x"
shows "n = 0 \ 1 \ x"
proof (cases "n = 0")
case True
then show ?thesis by simp
next
case False
then have "\n\ \ 0" by simp
then have "\n\ > 0" by simp
then have "\n\ \ 1"
using zless_imp_add1_zle [of 0 "\n\"] by simp
then have "\of_int n\ \ 1"
unfolding of_int_1_le_iff [of "\n\", symmetric] by simp
then have "1 \ x" using assms by (rule order_trans)
then show ?thesis ..
qed
end
text \Comparisons involving @{term of_int}.\
lemma of_int_eq_numeral_iff [iff]: "of_int z = (numeral n :: 'a::ring_char_0) \ z = numeral n"
using of_int_eq_iff by fastforce
lemma of_int_le_numeral_iff [simp]:
"of_int z \ (numeral n :: 'a::linordered_idom) \ z \ numeral n"
using of_int_le_iff [of z "numeral n"] by simp
lemma of_int_numeral_le_iff [simp]:
"(numeral n :: 'a::linordered_idom) \ of_int z \ numeral n \ z"
using of_int_le_iff [of "numeral n"] by simp
lemma of_int_less_numeral_iff [simp]:
"of_int z < (numeral n :: 'a::linordered_idom) \ z < numeral n"
using of_int_less_iff [of z "numeral n"] by simp
lemma of_int_numeral_less_iff [simp]:
"(numeral n :: 'a::linordered_idom) < of_int z \ numeral n < z"
using of_int_less_iff [of "numeral n" z] by simp
lemma of_nat_less_of_int_iff: "(of_nat n::'a::linordered_idom) < of_int x \ int n < x"
by (metis of_int_of_nat_eq of_int_less_iff)
lemma of_int_eq_id [simp]: "of_int = id"
proof
show "of_int z = id z" for z
by (cases z rule: int_diff_cases) simp
qed
instance int :: no_top
apply standard
apply (rule_tac x="x + 1" in exI)
apply simp
done
instance int :: no_bot
apply standard
apply (rule_tac x="x - 1" in exI)
apply simp
done
subsection \Magnitude of an Integer, as a Natural Number: \nat\\
lift_definition nat :: "int \ nat" is "\(x, y). x - y"
by auto
lemma nat_int [simp]: "nat (int n) = n"
by transfer simp
lemma int_nat_eq [simp]: "int (nat z) = (if 0 \ z then z else 0)"
by transfer clarsimp
lemma nat_0_le: "0 \ z \ int (nat z) = z"
by simp
lemma nat_le_0 [simp]: "z \ 0 \ nat z = 0"
by transfer clarsimp
lemma nat_le_eq_zle: "0 < w \ 0 \ z \ nat w \ nat z \ w \ z"
by transfer (clarsimp, arith)
text \An alternative condition is @{term "0 \ w"}.\
lemma nat_mono_iff: "0 < z \ nat w < nat z \ w < z"
by (simp add: nat_le_eq_zle linorder_not_le [symmetric])
lemma nat_less_eq_zless: "0 \ w \ nat w < nat z \ w < z"
by (simp add: nat_le_eq_zle linorder_not_le [symmetric])
lemma zless_nat_conj [simp]: "nat w < nat z \ 0 < z \ w < z"
by transfer (clarsimp, arith)
lemma nonneg_int_cases:
assumes "0 \ k"
obtains n where "k = int n"
proof -
from assms have "k = int (nat k)"
by simp
then show thesis
by (rule that)
qed
lemma pos_int_cases:
assumes "0 < k"
obtains n where "k = int n" and "n > 0"
proof -
from assms have "0 \ k"
by simp
then obtain n where "k = int n"
by (rule nonneg_int_cases)
moreover have "n > 0"
using \k = int n\ assms by simp
ultimately show thesis
by (rule that)
qed
lemma nonpos_int_cases:
assumes "k \ 0"
obtains n where "k = - int n"
proof -
from assms have "- k \ 0"
by simp
then obtain n where "- k = int n"
by (rule nonneg_int_cases)
then have "k = - int n"
by simp
then show thesis
by (rule that)
qed
lemma neg_int_cases:
assumes "k < 0"
obtains n where "k = - int n" and "n > 0"
proof -
from assms have "- k > 0"
by simp
then obtain n where "- k = int n" and "- k > 0"
by (blast elim: pos_int_cases)
then have "k = - int n" and "n > 0"
by simp_all
then show thesis
by (rule that)
qed
lemma nat_eq_iff: "nat w = m \ (if 0 \ w then w = int m else m = 0)"
by transfer (clarsimp simp add: le_imp_diff_is_add)
lemma nat_eq_iff2: "m = nat w \ (if 0 \ w then w = int m else m = 0)"
using nat_eq_iff [of w m] by auto
lemma nat_0 [simp]: "nat 0 = 0"
by (simp add: nat_eq_iff)
lemma nat_1 [simp]: "nat 1 = Suc 0"
by (simp add: nat_eq_iff)
lemma nat_numeral [simp]: "nat (numeral k) = numeral k"
by (simp add: nat_eq_iff)
lemma nat_neg_numeral [simp]: "nat (- numeral k) = 0"
by simp
lemma nat_2: "nat 2 = Suc (Suc 0)"
by simp
lemma nat_less_iff: "0 \ w \ nat w < m \ w < of_nat m"
by transfer (clarsimp, arith)
lemma nat_le_iff: "nat x \ n \ x \ int n"
by transfer (clarsimp simp add: le_diff_conv)
lemma nat_mono: "x \ y \ nat x \ nat y"
by transfer auto
lemma nat_0_iff[simp]: "nat i = 0 \ i \ 0"
for i :: int
by transfer clarsimp
lemma int_eq_iff: "of_nat m = z \ m = nat z \ 0 \ z"
by (auto simp add: nat_eq_iff2)
lemma zero_less_nat_eq [simp]: "0 < nat z \ 0 < z"
using zless_nat_conj [of 0] by auto
lemma nat_add_distrib: "0 \ z \ 0 \ z' \ nat (z + z') = nat z + nat z'"
by transfer clarsimp
lemma nat_diff_distrib': "0 \ x \ 0 \ y \ nat (x - y) = nat x - nat y"
by transfer clarsimp
lemma nat_diff_distrib: "0 \ z' \ z' \ z \ nat (z - z') = nat z - nat z'"
by (rule nat_diff_distrib') auto
lemma nat_zminus_int [simp]: "nat (- int n) = 0"
by transfer simp
lemma le_nat_iff: "k \ 0 \ n \ nat k \ int n \ k"
by transfer auto
lemma zless_nat_eq_int_zless: "m < nat z \*