Theory Quotient_Int

```(*  Title:      HOL/Quotient_Examples/Quotient_Int.thy
Author:     Cezary Kaliszyk
Author:     Christian Urban

Integers based on Quotients, based on an older version by Larry
Paulson.
*)

theory Quotient_Int
imports "HOL-Library.Quotient_Product"
begin

fun
intrel :: "(nat × nat) ⇒ (nat × nat) ⇒ bool" (infix "≈" 50)
where
"intrel (x, y) (u, v) = (x + v = u + y)"

quotient_type int = "nat × nat" / intrel
by (auto simp add: equivp_def fun_eq_iff)

instantiation int :: "{zero, one, plus, uminus, minus, times, ord, abs, sgn}"
begin

quotient_definition
"0 :: int" is "(0::nat, 0::nat)" done

quotient_definition
"1 :: int" is "(1::nat, 0::nat)" done

fun
plus_int_raw :: "(nat × nat) ⇒ (nat × nat) ⇒ (nat × nat)"
where
"plus_int_raw (x, y) (u, v) = (x + u, y + v)"

quotient_definition
"(+) :: (int ⇒ int ⇒ int)" is "plus_int_raw" by auto

fun
uminus_int_raw :: "(nat × nat) ⇒ (nat × nat)"
where
"uminus_int_raw (x, y) = (y, x)"

quotient_definition
"(uminus :: (int ⇒ int))" is "uminus_int_raw" by auto

definition
minus_int_def:  "z - w = z + (-w::int)"

fun
times_int_raw :: "(nat × nat) ⇒ (nat × nat) ⇒ (nat × nat)"
where
"times_int_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)"

lemma times_int_raw_fst:
assumes a: "x ≈ z"
shows "times_int_raw x y ≈ times_int_raw z y"
using a
apply(cases x, cases y, cases z)
apply(hypsubst_thin)
apply(rename_tac u v w x y z)
apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")
done

lemma times_int_raw_snd:
assumes a: "x ≈ z"
shows "times_int_raw y x ≈ times_int_raw y z"
using a
apply(cases x, cases y, cases z)
apply(hypsubst_thin)
apply(rename_tac u v w x y z)
apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")
done

quotient_definition
"((*)) :: (int ⇒ int ⇒ int)" is "times_int_raw"
apply(rule equivp_transp[OF int_equivp])
apply(rule times_int_raw_fst)
apply(assumption)
apply(rule times_int_raw_snd)
apply(assumption)
done

fun
le_int_raw :: "(nat × nat) ⇒ (nat × nat) ⇒ bool"
where
"le_int_raw (x, y) (u, v) = (x+v ≤ u+y)"

quotient_definition
le_int_def: "(≤) :: int ⇒ int ⇒ bool" is "le_int_raw" by auto

definition
less_int_def: "(z::int) < w = (z ≤ w ∧ z ≠ w)"

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 ..

end

text‹The integers form a ‹comm_ring_1››

instance int :: comm_ring_1
proof
fix i j k :: int
show "(i + j) + k = i + (j + k)"
by (descending) (auto)
show "i + j = j + i"
by (descending) (auto)
show "0 + i = (i::int)"
by (descending) (auto)
show "- i + i = 0"
by (descending) (auto)
show "i - j = i + - j"
show "(i * j) * k = i * (j * k)"
by (descending) (auto simp add: algebra_simps)
show "i * j = j * i"
by (descending) (auto)
show "1 * i = i"
by (descending) (auto)
show "(i + j) * k = i * k + j * k"
by (descending) (auto simp add: algebra_simps)
show "0 ≠ (1::int)"
by (descending) (auto)
qed

lemma plus_int_raw_rsp_aux:
assumes a: "a ≈ b" "c ≈ d"
shows "plus_int_raw a c ≈ plus_int_raw b d"
using a
by (cases a, cases b, cases c, cases d)
(simp)

"(abs_int (x,y)) + (abs_int (u,v)) =
(abs_int (x + u, y + v))"
apply(fold plus_int_raw.simps)
apply(rule Quotient3_rel_abs[OF Quotient3_int])
apply(rule plus_int_raw_rsp_aux)
done

definition int_of_nat_raw:
"int_of_nat_raw m = (m :: nat, 0 :: nat)"

quotient_definition
"int_of_nat :: nat ⇒ int" is "int_of_nat_raw" done

lemma int_of_nat:
shows "of_nat m = int_of_nat m"
by (induct m)

instance int :: linorder
proof
fix i j k :: int
show antisym: "i ≤ j ⟹ j ≤ i ⟹ i = j"
by (descending) (auto)
show "(i < j) = (i ≤ j ∧ ¬ j ≤ i)"
by (auto simp add: less_int_def dest: antisym)
show "i ≤ i"
by (descending) (auto)
show "i ≤ j ⟹ j ≤ k ⟹ i ≤ k"
by (descending) (auto)
show "i ≤ j ∨ j ≤ i"
by (descending) (auto)
qed

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

proof
fix i j k :: int
show "i ≤ j ⟹ k + i ≤ k + j"
by (descending) (auto)
qed

abbreviation
"less_int_raw i j ≡ le_int_raw i j ∧ ¬(i ≈ j)"

lemma zmult_zless_mono2_lemma:
fixes i j::int
and   k::nat
shows "i < j ⟹ 0 < k ⟹ of_nat k * i < of_nat k * j"
apply(induct "k")
apply(simp)
apply(case_tac "k = 0")
done

lemma zero_le_imp_eq_int_raw:
fixes k::"(nat × nat)"
shows "less_int_raw (0, 0) k ⟹ (∃n > 0. k ≈ int_of_nat_raw n)"
apply(cases k)
apply(auto)
apply(rule_tac i="b" and j="a" in less_Suc_induct)
apply(auto)
done

lemma zero_le_imp_eq_int:
fixes k::int
shows "0 < k ⟹ ∃n > 0. k = of_nat n"
unfolding less_int_def int_of_nat
by (descending) (rule zero_le_imp_eq_int_raw)

lemma zmult_zless_mono2:
fixes i j k::int
assumes a: "i < j" "0 < k"
shows "k * i < k * j"
using a
by (drule_tac zero_le_imp_eq_int) (auto simp add: zmult_zless_mono2_lemma)

text‹The integers form an ordered integral domain›

instance int :: linordered_idom
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<i then 1 else - 1)"
by (simp only: zsgn_def)
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

lemma int_induct2:
assumes "P 0 0"
and     "⋀n m. P n m ⟹ P (Suc n) m"
and     "⋀n m. P n m ⟹ P n (Suc m)"
shows   "P n m"
using assms
by (induction_schema) (pat_completeness, lexicographic_order)

lemma int_induct:
fixes j :: int
assumes a: "P 0"
and     b: "⋀i::int. P i ⟹ P (i + 1)"
and     c: "⋀i::int. P i ⟹ P (i - 1)"
shows      "P j"
using a b c
unfolding minus_int_def
by (descending) (auto intro: int_induct2)

text ‹Magnitide of an Integer, as a Natural Number: \<^term>‹nat››

definition
"int_to_nat_raw ≡ λ(x, y).x - (y::nat)"

quotient_definition
"int_to_nat::int ⇒ nat"
is
"int_to_nat_raw"
unfolding int_to_nat_raw_def by auto

lemma nat_le_eq_zle:
fixes w z::"int"
shows "0 < w ∨ 0 ≤ z ⟹ (int_to_nat w ≤ int_to_nat z) = (w ≤ z)"
unfolding less_int_def
by (descending) (auto simp add: int_to_nat_raw_def)

end
```