Theory Util_NatInf

(*  Title:      Util_NatInf.thy
    Date:       Oct 2006
    Author:     David Trachtenherz
*)

section ‹Results for natural arithmetics with infinity›

theory Util_NatInf
imports "HOL-Library.Extended_Nat"
begin

subsection ‹Arithmetic operations with @{typ enat}›

subsubsection ‹Additional definitions›

instantiation enat :: modulo
begin

definition
  div_enat_def [code del]: "
  a div b ≡ (case a of
    (enat x) ⇒ (case b of (enat y) ⇒ enat (x div y) | ∞ ⇒ 0) |
    ∞ ⇒ (case b of (enat y) ⇒ ((case y of 0 ⇒ 0 | Suc n ⇒ ∞)) | ∞ ⇒ ∞ ))"
definition
  mod_enat_def [code del]: "
  a mod b ≡ (case a of
    (enat x) ⇒ (case b of (enat y) ⇒ enat (x mod y) | ∞ ⇒ a) |
    ∞ ⇒ ∞)"

instance ..

end


lemmas enat_arith_defs =
  zero_enat_def one_enat_def
  plus_enat_def diff_enat_def times_enat_def div_enat_def mod_enat_def
declare zero_enat_def[simp]


lemmas ineq0_conv_enat[simp] = i0_less[symmetric, unfolded zero_enat_def]

lemmas iless_eSuc0_enat[simp] = iless_eSuc0[unfolded zero_enat_def]


subsubsection ‹Addition, difference, order›

lemma diff_eq_conv_nat: "(x - y = (z::nat)) = (if y < x then x = y + z else z = 0)"
by auto
lemma idiff_eq_conv: "
  (x - y = (z::enat)) =
  (if y < x then x = y + z else if x ≠ ∞ then z = 0 else z = ∞)"
by (case_tac x, case_tac y, case_tac z, auto, case_tac z, auto)
lemmas idiff_eq_conv_enat = idiff_eq_conv[unfolded zero_enat_def]

lemma less_eq_idiff_eq_sum: "y ≤ (x::enat) ⟹ (z ≤ x - y) = (z + y ≤ x)"
by (case_tac x, case_tac y, case_tac z, fastforce+)


lemma eSuc_pred: "0 < n ⟹ eSuc (n - eSuc 0) = n"
apply (case_tac n)
apply (simp add: eSuc_enat)+
done
lemmas eSuc_pred_enat = eSuc_pred[unfolded zero_enat_def]
lemmas iadd_0_enat[simp] = add_0_left[where 'a = enat, unfolded zero_enat_def]
lemmas iadd_0_right_enat[simp] = add_0_right[where 'a=enat, unfolded zero_enat_def]

lemma ile_add1: "(n::enat) ≤ n + m"
by (case_tac m, case_tac n, simp_all)
lemma ile_add2: "(n::enat) ≤ m + n"
by (simp only: add.commute[of m] ile_add1)

lemma iadd_iless_mono: "⟦ (i::enat) < j; k < l ⟧ ⟹ i + k < j + l"
by (case_tac i, case_tac k, case_tac j, case_tac l, simp_all)

lemma trans_ile_iadd1: "i ≤ (j::enat) ⟹ i ≤ j + m"
by (rule order_trans[OF _ ile_add1])
lemma trans_ile_iadd2: "i ≤ (j::enat) ⟹ i ≤ m + j"
by (rule order_trans[OF _ ile_add2])

lemma trans_iless_iadd1: "i < (j::enat) ⟹ i < j + m"
by (rule order_less_le_trans[OF _ ile_add1])
lemma trans_iless_iadd2: "i < (j::enat) ⟹ i < m + j"
by (rule order_less_le_trans[OF _ ile_add2])

lemma iadd_ileD1: "m + k ≤ (n::enat) ⟹ m ≤ n"
by (case_tac m, case_tac n, case_tac k, simp_all)

lemma iadd_ileD2: "m + k ≤ (n::enat) ⟹ k ≤ n"
by (rule iadd_ileD1, simp only: add.commute[of m])


lemma idiff_ile_mono: "m ≤ (n::enat) ⟹ m - l ≤ n - l"
by (case_tac m, case_tac n, case_tac l, simp_all)

lemma idiff_ile_mono2: "m ≤ (n::enat) ⟹ l - n ≤ l - m"
by (case_tac m, case_tac n, case_tac l, simp_all, case_tac l, simp_all)

lemma idiff_iless_mono: "⟦ m < (n::enat); l ≤ m ⟧ ⟹ m - l < n - l"
by (case_tac m, case_tac n, case_tac l, simp_all, case_tac l, simp_all)

lemma idiff_iless_mono2: "⟦ m < (n::enat); m < l ⟧ ⟹ l - n ≤ l - m"
by (case_tac m, case_tac n, case_tac l, simp_all, case_tac l, simp_all)


subsubsection ‹Multiplication and division›

lemmas imult_infinity_enat[simp] = imult_infinity[unfolded zero_enat_def]
lemmas imult_infinity_right_enat[simp] = imult_infinity_right[unfolded zero_enat_def]

lemma idiv_enat_enat[simp, code]: "enat a div enat b = enat (a div b)"
unfolding div_enat_def by simp

lemma idiv_infinity: "0 < n ⟹ (∞::enat) div n = ∞"
unfolding div_enat_def
apply (case_tac n, simp_all)
apply (rename_tac n1, case_tac n1, simp_all)
done

lemmas idiv_infinity_enat[simp] = idiv_infinity[unfolded zero_enat_def]

lemma idiv_infinity_right[simp]: "n ≠ ∞ ⟹ n div (∞::enat) = 0"
unfolding div_enat_def by (case_tac n, simp_all)

lemma idiv_infinity_if: "n div ∞ = (if n = ∞ then ∞ else 0::enat)"
unfolding div_enat_def
by (case_tac n, simp_all)

lemmas idiv_infinity_if_enat = idiv_infinity_if[unfolded zero_enat_def]

lemmas imult_0_enat[simp] = mult_zero_left[where 'a=enat,unfolded zero_enat_def]
lemmas imult_0_right_enat[simp] = mult_zero_right[where 'a=enat,unfolded zero_enat_def]

lemmas imult_is_0_enat = imult_is_0[unfolded zero_enat_def]
lemmas enat_0_less_mult_iff_enat = enat_0_less_mult_iff[unfolded zero_enat_def]

lemma imult_infinity_if: "∞ * n = (if n = 0 then 0 else ∞::enat)"
by (case_tac n, simp_all)
lemma imult_infinity_right_if: "n * ∞ = (if n = 0 then 0 else ∞::enat)"
by (case_tac n, simp_all)
lemmas imult_infinity_if_enat = imult_infinity_if[unfolded zero_enat_def]
lemmas imult_infinity_right_if_enat = imult_infinity_right_if[unfolded zero_enat_def]

lemmas imult_is_infinity_enat = imult_is_infinity[unfolded zero_enat_def]

lemma idiv_by_0: "(a::enat) div 0 = 0"
unfolding div_enat_def by (case_tac a, simp_all)
lemmas idiv_by_0_enat[simp, code] = idiv_by_0[unfolded zero_enat_def]

lemma idiv_0: "0 div (a::enat) = 0"
unfolding div_enat_def by (case_tac a, simp_all)
lemmas idiv_0_enat[simp, code] = idiv_0[unfolded zero_enat_def]

lemma imod_by_0: "(a::enat) mod 0 = a"
unfolding mod_enat_def by (case_tac a, simp_all)
lemmas imod_by_0_enat[simp, code] = imod_by_0[unfolded zero_enat_def]

lemma imod_0: "0 mod (a::enat) = 0"
unfolding mod_enat_def by (case_tac a, simp_all)
lemmas imod_0_enat[simp, code] = imod_0[unfolded zero_enat_def]

lemma imod_enat_enat[simp, code]: "enat a mod enat b = enat (a mod b)"
unfolding mod_enat_def by simp
lemma imod_infinity[simp, code]: "∞ mod n = (∞::enat)"
unfolding mod_enat_def by simp
lemma imod_infinity_right[simp, code]: "n mod (∞::enat) = n"
unfolding mod_enat_def by (case_tac n) simp_all

lemma idiv_self: "⟦ 0 < (n::enat); n ≠ ∞ ⟧ ⟹ n div n = 1"
by (case_tac n, simp_all add: one_enat_def)
lemma imod_self: "n ≠ ∞ ⟹ (n::enat) mod n = 0"
by (case_tac n, simp_all)

lemma idiv_iless: "m < (n::enat) ⟹ m div n = 0"
by (case_tac m, simp_all) (case_tac n, simp_all)
lemma imod_iless: "m < (n::enat) ⟹ m mod n = m"
by (case_tac m, simp_all) (case_tac n, simp_all)

lemma imod_iless_divisor: "⟦ 0 < (n::enat); m ≠ ∞ ⟧  ⟹ m mod n < n"
by (case_tac m, simp_all) (case_tac n, simp_all)
lemma imod_ile_dividend: "(m::enat) mod n ≤ m"
by (case_tac m, simp_all) (case_tac n, simp_all)
lemma idiv_ile_dividend: "(m::enat) div n ≤ m"
by (case_tac m, simp_all) (case_tac n, simp_all)

lemma idiv_imult2_eq: "(a::enat) div (b * c) = a div b div c"
apply (case_tac a, case_tac b, case_tac c, simp_all add: div_mult2_eq)
apply (simp add: imult_infinity_if)
apply (case_tac "b = 0", simp)
apply (case_tac "c = 0", simp)
apply (simp add: idiv_infinity[OF enat_0_less_mult_iff[THEN iffD2]])
done

lemma imult_ile_mono: "⟦ (i::enat) ≤ j; k ≤ l ⟧ ⟹ i * k ≤ j * l"
apply (case_tac i, case_tac j, case_tac k, case_tac l, simp_all add: mult_le_mono)
apply (case_tac k, case_tac l, simp_all)
apply (case_tac k, case_tac l, simp_all)
done

lemma imult_ile_mono1: "(i::enat) ≤ j ⟹ i * k ≤ j * k"
by (rule imult_ile_mono[OF _ order_refl])

lemma imult_ile_mono2: "(i::enat) ≤ j ⟹ k * i ≤ k * j"
by (rule imult_ile_mono[OF order_refl])

lemma imult_iless_mono1: "⟦ (i::enat) < j; 0 < k; k ≠ ∞ ⟧ ⟹ i * k ≤ j * k"
by (case_tac i, case_tac j, case_tac k, simp_all)
lemma imult_iless_mono2: "⟦ (i::enat) < j; 0 < k; k ≠ ∞ ⟧ ⟹ k * i ≤ k * j"
by (simp only: mult.commute[of k], rule imult_iless_mono1)

lemma imod_1: "(enat m) mod eSuc 0 = 0"
by (simp add: eSuc_enat)
lemmas imod_1_enat[simp, code] = imod_1[unfolded zero_enat_def]

lemma imod_iadd_self2: "(m + enat n) mod (enat n) = m mod (enat n)"
by (case_tac m, simp_all)

lemma imod_iadd_self1: "(enat n + m) mod (enat n) = m mod (enat n)"
by (simp only: add.commute[of _ m] imod_iadd_self2)

lemma idiv_imod_equality: "(m::enat) div n * n + m mod n + k = m + k"
by (case_tac m, simp_all) (case_tac n, simp_all)
lemma imod_idiv_equality: "(m::enat) div n * n + m mod n = m"
by (insert idiv_imod_equality[of m n 0], simp)

lemma idiv_ile_mono: "m ≤ (n::enat) ⟹ m div k ≤ n div k"
apply (case_tac "k = 0", simp)
apply (case_tac m, case_tac k, simp_all)
apply (case_tac n)
 apply (simp add: div_le_mono)
apply (simp add: idiv_infinity)
apply (simp add: i0_lb[unfolded zero_enat_def])
done
lemma idiv_ile_mono2: "⟦ 0 < m; m ≤ (n::enat) ⟧ ⟹ k div n ≤ k div m"
apply (case_tac "n = 0", simp)
apply (case_tac m, case_tac k, simp_all)
apply (case_tac n)
 apply (simp add: div_le_mono2)
apply simp
done

end