Theory Util_NatInf

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

header {* Results for natural arithmetics with infinity *}

theory Util_NatInf
imports "$ISABELLE_HOME/src/HOL/Library/Nat_Infinity"
begin



subsection {* Arithmetic operations with @{typ inat} *} 

subsubsection {* Additional definitions *}


thm one_inat_def
thm plus_inat_def
thm times_inat_def

instantiation inat :: "{minus, Divides.div}"
begin

definition
  diff_inat_def [code del]: "
  a - b ≡ (case a of 
    (Fin x) => (case b of (Fin y) => Fin (x - y) | ∞ => 0) | 
    ∞ => ∞)"

definition
  div_inat_def [code del]: "
  a div b ≡ (case a of 
    (Fin x) => (case b of (Fin y) => Fin (x div y) | ∞ => 0) | 
    ∞ => (case b of (Fin y) => ((case y of 0 => 0 | Suc n => ∞)) | ∞ => ∞ ))"
definition
  mod_inat_def [code del]: "
  a mod b ≡ (case a of 
    (Fin x) => (case b of (Fin y) => Fin (x mod y) | ∞ => a) | 
    ∞ => ∞)"

instance ..

end

(*instance inat :: "{ord, zero, one, plus, minus, times, Divides.div}" ..*)





lemmas inat_arith_defs = 
  zero_inat_def one_inat_def
  plus_inat_def diff_inat_def times_inat_def div_inat_def mod_inat_def
declare zero_inat_def[simp]

primrec the_Fin :: "inat => nat" where
  "the_Fin (Fin n) = n"

lemma Fin_the_Fin: "n ≠ ∞ ==> Fin (the_Fin n) = n" by fastsimp

subsubsection {* Results for comparison operators *}

lemma Fin_ile_mono: "(Fin m ≤ Fin n) = (m ≤ n)" by simp
lemma Fin_iless_mono: "(Fin m < Fin n) = (m < n)" by simp
lemma Infty_ub: "n ≤ ∞" by simp

thm less_not_sym
lemma iless_not_sym: "(x::inat) < y ==> ¬ y < x" by simp
thm less_not_refl
lemma iless_not_refl: "¬ (n::inat) < n" by simp
thm le_refl
lemma ile_refl: "(n::inat) ≤ n" by simp
lemma eq_imp_ile: "(m::inat) = n ==> m ≤ n" by simp

lemma not_Infty_iless: "¬ ∞ < n" by simp
lemma Fin_iless_Infty: "Fin n < ∞" by simp
lemma not_Infty_ile_Fin: "¬ ∞ ≤ Fin n" by simp
(*lemma Fin_ile_Infty: "Fin n ≤ ∞"*)
lemmas Fin_ile_Infty = Infty_ub


(*lemma neq_Infty_Fin_conv: "(n ≠ ∞) = (∃k. n = Fin k)" *)
lemmas neq_Infty_Fin_conv = not_Infty_eq

lemma Infty_le_eq: "(∞ ≤ n) = (n = ∞)" by simp

lemma ile_trans: "[| (i::inat) ≤ j; j ≤ k |] ==> i ≤ k" by simp
lemma ile_anti_sym: "[| (m::inat) ≤ n; n ≤ m |] ==> m = n" by simp
lemma iless_ile: "((m::inat) < n) = (m ≤ n ∧ m ≠ n)" by (safe, simp_all)
lemma ile_linear: "(m::inat) ≤ n ∨ n ≤ m" by (safe, simp_all)

(*
instance inat :: order ..
instance inat :: linorder ..
instance inat :: wellorder ..
*)




thm neq0_conv
lemma ineq0_conv: "(n ≠ (0::inat)) = (0 < n)"
by (case_tac n, simp_all)
lemmas ineq0_conv_Fin[simp] = ineq0_conv[unfolded zero_inat_def]

(*lemma not_iless0: "¬ n < (0::inat)"*)
lemmas not_iless0 = not_ilessi0
lemma iless_iSuc0: "(n < iSuc 0) = (n = 0)"
by (case_tac n, simp_all)
lemmas iless_iSuc0_Fin[simp] = iless_iSuc0[unfolded zero_inat_def]

(*lemma ile_0_eq: "(n ≤ (0::inat)) = (n = 0)"*)
lemmas ile_0_eq = i0_neq

lemma neq_Infty_imp_ex_Fin: "n ≠ ∞ ==> ∃nat. n = Fin nat"
by (case_tac n, simp_all)
corollary less_Infty_imp_ex_Fin: "n < ∞ ==> ∃nat. n = Fin nat"
thm neq_Infty_imp_ex_Fin[OF less_imp_neq]
by (rule neq_Infty_imp_ex_Fin[OF less_imp_neq])





subsubsection {* Addition and difference *}


lemma iadd_Fin_Fin: "Fin a + Fin b = Fin (a + b)" by simp
lemma iadd_Infty: "∞ + n = ∞" by simp
lemma iadd_Infty_right: "n + ∞ = ∞" by simp

lemma idiff_Fin_Fin[simp,code]: "Fin a - Fin b = Fin (a - b)"
unfolding diff_inat_def by simp
lemma idiff_Infty[simp,code]: "∞ - n = ∞"
unfolding diff_inat_def by simp
lemma idiff_Infty_right[simp,code]: "Fin a - ∞ = 0"
unfolding diff_inat_def by simp

lemma idiff_0: "(n::inat) - 0 = n"
by (case_tac n, simp_all)
lemmas idiff_0_Fin[simp,code] = idiff_0[unfolded zero_inat_def]
lemma idiff_0_eq_0: "(0::inat) - n = 0"
by (case_tac n, simp_all)
lemmas idiff_0_eq_0_Fin[simp,code] = idiff_0_eq_0[unfolded zero_inat_def]

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::inat)) = 
  (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_Fin = idiff_eq_conv[unfolded zero_inat_def]

lemma idiff_self_eq_0: "n ≠ ∞ ==> (n::inat) - n = 0" 
by fastsimp
lemmas idiff_self_eq_0_Fin = idiff_self_eq_0[unfolded zero_inat_def]

lemma less_eq_idiff_eq_sum: "y ≤ (x::inat) ==> (z ≤ x - y) = (z + y ≤ x)"
by (case_tac x, case_tac y, case_tac z, fastsimp+)


lemma iSuc_pred: "0 < n ==> iSuc (n - iSuc 0) = n"
apply (case_tac n)
apply (simp add: iSuc_Fin)+
done
lemmas iSuc_pred_Fin = iSuc_pred[unfolded zero_inat_def]
lemma iadd_0: "(0::inat) + n = n" 
by (rule monoid_add_class.add_0_left)
lemmas iadd_0_Fin[simp, code] = iadd_0[unfolded zero_inat_def]
lemma iadd_0_right: "n + (0::inat) = n" 
by (rule monoid_add_class.add_0_right)
lemmas iadd_0_right_Fin[simp, code] = iadd_0_right[unfolded zero_inat_def]

lemma iadd_commute: "(a::inat) + b = b + a" 
by (rule ab_semigroup_add_class.add_commute)
thm add_assoc
lemma iadd_assoc: "(a::inat) + b + c = a + (b + c)"
by (rule semigroup_add_class.add.assoc)


thm add_Suc
lemma iadd_Suc: "iSuc m + n = iSuc (m + n)"
apply (case_tac m, case_tac n)
apply (simp add: iSuc_Fin)+
done

thm add_Suc_right
lemma iadd_Suc_right: "m + iSuc n = iSuc (m + n)"
by (simp only: iadd_commute[of m] iadd_Suc)

lemma mono_iSuc: "mono iSuc"
unfolding mono_def by simp

thm add_is_0[no_vars]
lemma iadd_is_0: "(m + n = (0::inat)) = (m = 0 ∧ n = 0)"
by (case_tac m, case_tac n, simp_all)
lemmas iadd_is_0_Fin = iadd_is_0[unfolded zero_inat_def]

lemma ile_add1: "(n::inat) ≤ n + m"
by (case_tac m, case_tac n, simp_all)
lemma ile_add2: "(n::inat) ≤ m + n"
by (simp only: iadd_commute[of m] ile_add1)

lemma iadd_ile_mono: "[| (i::inat) ≤ j; k ≤ l |] ==> i + k ≤ j + l"
by (rule add_mono)
lemma iadd_ile_mono1: "(i::inat) ≤ j ==> i + k ≤ j + k"
by (rule add_right_mono)
lemma iadd_ile_mono2: "(i::inat) ≤ j ==> k + i ≤ k + j"
by (rule add_left_mono)

lemma iadd_iless_mono: "[| (i::inat) < 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::inat) ==> i ≤ j + m" 
by (rule order_trans[OF _ ile_add1])
lemma trans_ile_iadd2: "i ≤ (j::inat) ==> i ≤ m + j"
by (rule order_trans[OF _ ile_add2])

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

thm add_leD1[no_vars]
lemma iadd_ileD1: "m + k ≤ (n::inat) ==> m ≤ n"
by (case_tac m, case_tac n, case_tac k, simp_all)
lemma iadd_ileD2: "m + k ≤ (n::inat) ==> k ≤ n"
by (rule iadd_ileD1, simp only: iadd_commute[of m])



thm diff_le_mono
lemma idiff_ile_mono: "m ≤ (n::inat) ==> m - l ≤ n - l"
by (case_tac m, case_tac n, case_tac l, simp_all)
thm diff_le_mono2
lemma idiff_ile_mono2: "m ≤ (n::inat) ==> l - n ≤ l - m"
by (case_tac m, case_tac n, case_tac l, simp_all, case_tac l, simp_all)

thm diff_less_mono
lemma idiff_iless_mono: "[| m < (n::inat); l ≤ m |] ==> m - l < n - l"
by (case_tac m, case_tac n, case_tac l, simp_all, case_tac l, simp_all)
thm diff_less_mono2
lemma idiff_iless_mono2: "[| m < (n::inat); 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 *}

lemma imult_Fin_Fin: "Fin a * Fin b = Fin (a * b)" by simp
lemma imult_Infty: "(0::inat) < n ==> ∞ * n = ∞" 
by (case_tac n, simp_all)
lemmas imult_Infty_Fin[simp] = imult_Infty[unfolded zero_inat_def]
lemma imult_Infty_right: "(0::inat) < n ==> n * ∞ = ∞"
by (case_tac n, simp_all)
lemmas imult_Infty_right_Fin[simp] = imult_Infty_right[unfolded zero_inat_def]

lemma idiv_Fin_Fin[simp, code]: "Fin a div Fin b = Fin (a div b)"
unfolding div_inat_def by simp
lemma idiv_Infty: "0 < n ==> ∞ div n = ∞"
unfolding div_inat_def
apply (case_tac n, simp_all)
apply (rename_tac n1, case_tac n1, simp_all)
done
lemmas idiv_Infty_Fin[simp] = idiv_Infty[unfolded zero_inat_def]

lemma idiv_Infty_right[simp]: "n ≠ ∞ ==> n div ∞ = 0"
unfolding div_inat_def by (case_tac n, simp_all)

lemma idiv_Infty_if: "n div ∞ = (if n = ∞ then ∞ else 0)"
unfolding div_inat_def
by (case_tac n, simp_all)

lemmas idiv_Infty_if_Fin = idiv_Infty_if[unfolded zero_inat_def]

lemma imult_0: "0 * (m::inat) = 0" 
by (case_tac m, simp_all)
lemmas imult_0_Fin[simp, code] = imult_0[unfolded zero_inat_def]
lemma imult_0_right: "(m::inat) * 0 = 0"
by (case_tac m, simp_all)
lemmas imult_0_right_Fin[simp, code] = imult_0_right[unfolded zero_inat_def]

lemma imult_is_0: "((m::inat) * n = 0) = (m = 0 ∨ n = 0)"
apply (case_tac m, case_tac n, simp_all)
apply (case_tac n, simp_all)
done
lemma inat_0_less_mult_iff: "(0 < (m::inat) * n) = (0 < m ∧ 0 < n)"
by (simp only: ineq0_conv[symmetric] imult_is_0, simp)
lemmas imult_is_0_Fin = imult_is_0[unfolded zero_inat_def]
lemmas inat_0_less_mult_iff_Fin = inat_0_less_mult_iff[unfolded zero_inat_def]

lemma imult_commute: "(a::inat) * b = b * a"
by (rule ab_semigroup_mult_class.mult_commute)


lemma imult_Infty_if: "∞ * n = (if n = 0 then 0 else ∞)"
by (case_tac n, simp_all)
lemma imult_Infty_right_if: "n * ∞ = (if n = 0 then 0 else ∞)"
by (case_tac n, simp_all)
lemmas imult_Infty_if_Fin = imult_Infty_if[unfolded zero_inat_def]
lemmas imult_Infty_right_if_Fin = imult_Infty_right_if[unfolded zero_inat_def]

lemma imult_is_Infty: "((a::inat) * b = ∞) = (a = ∞ ∧ b ≠ 0 ∨ b = ∞ ∧ a ≠ 0)"
apply (case_tac a, case_tac b, simp_all)
apply (case_tac b, simp_all)
done
lemmas imult_is_Infty_Fin = imult_is_Infty[unfolded zero_inat_def]

lemma imult_assoc: "(a::inat) * b * c = a * (b * c)"
by (rule semigroup_mult_class.mult.assoc)

lemma idiv_by_0: "(a::inat) div 0 = 0"
unfolding div_inat_def by (case_tac a, simp_all)
lemmas idiv_by_0_Fin[simp, code] = idiv_by_0[unfolded zero_inat_def]

lemma idiv_0: "0 div (a::inat) = 0"
unfolding div_inat_def by (case_tac a, simp_all)
lemmas idiv_0_Fin[simp, code] = idiv_0[unfolded zero_inat_def]

thm mod_by_0
lemma imod_by_0: "(a::inat) mod 0 = a"
unfolding mod_inat_def by (case_tac a, simp_all)
lemmas imod_by_0_Fin[simp, code] = imod_by_0[unfolded zero_inat_def]

lemma imod_0: "0 mod (a::inat) = 0"
unfolding mod_inat_def by (case_tac a, simp_all)
lemmas imod_0_Fin[simp, code] = imod_0[unfolded zero_inat_def]

lemma imod_Fin_Fin[simp, code]: "Fin a mod Fin b = Fin (a mod b)"
unfolding mod_inat_def by simp
lemma imod_Infty[simp, code]: "∞ mod n = ∞"
unfolding mod_inat_def by simp
lemma imod_Infty_right[simp, code]: "n mod ∞ = n"
unfolding mod_inat_def by (case_tac n) simp_all

(*<*)
thm mult_Suc
(*lemma imult_Suc: "iSuc m * n = n + m * n"*)
(*lemmas imult_Suc = mult_iSuc*)

thm mult_Suc_right
(*lemma imult_Suc_right: "m * iSuc n = m + m * n"*)
(*lemmas imult_Suc_right mult_iSuc_right*)
(*>*)

lemma idiv_self: "[| 0 < (n::inat); n ≠ ∞ |] ==> n div n = 1"
by (case_tac n, simp_all add: one_inat_def)
lemma imod_self: "n ≠ ∞ ==> (n::inat) mod n = 0"
by (case_tac n, simp_all)

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

lemma imod_iless_divisor: "[| 0 < (n::inat); m ≠ ∞ |]  ==> m mod n < n"
by (case_tac m, simp_all) (case_tac n, simp_all)
lemma imod_ile_dividend: "(m::inat) mod n ≤ m"
by (case_tac m, simp_all) (case_tac n, simp_all)
lemma idiv_ile_dividend: "(m::inat) div n ≤ m"
by (case_tac m, simp_all) (case_tac n, simp_all)

thm div_mult2_eq
lemma idiv_imult2_eq: "(a::inat) div (b * c) = a div b div c"
apply (case_tac a, case_tac b, case_tac c, simp add: div_mult2_eq)
apply (simp add: imult_Infty_right_if idiv_Infty_right)
apply (simp add: imult_Infty_if idiv_Infty_right idiv_0[unfolded zero_inat_def])
apply (case_tac "b = 0", simp)
apply (case_tac "c = 0", simp)
thm idiv_Infty
thm idiv_Infty[OF inat_0_less_mult_iff[THEN iffD2]]
apply (simp add: idiv_Infty[OF inat_0_less_mult_iff[THEN iffD2]])
done


thm add_mult_distrib
lemma iadd_imult_distrib: "((m::inat) + n) * k = m * k + n * k"
by (rule left_distrib)

thm add_mult_distrib2
lemma iadd_imult_distrib2: "k * ((m::inat) + n) = k * m + k * n"
by (simp only: imult_commute[of k] iadd_imult_distrib)



thm mult_le_mono
lemma imult_ile_mono: "[| (i::inat) ≤ 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::inat) ≤ j ==> i * k ≤ j * k"
by (rule imult_ile_mono[OF _ ile_refl])
thm mult_le_mono2
lemma imult_ile_mono2: "(i::inat) ≤ j ==> k * i ≤ k * j"
by (rule imult_ile_mono[OF ile_refl])

lemma imult_iless_mono1: "[| (i::inat) < 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::inat) < j; 0 < k; k ≠ ∞ |] ==> k * i ≤ k * j"
by (simp only: imult_commute[of k], rule imult_iless_mono1)

lemma imod_1: "(Fin m) mod iSuc 0 = 0"
by (simp add: iSuc_Fin)
lemmas imod_1_Fin[simp, code] = imod_1[unfolded zero_inat_def]

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

lemma imod_iadd_self1: "(Fin n + m) mod (Fin n) = m mod (Fin n)"
by (simp only: iadd_commute[of _ m] imod_iadd_self2)

lemma idiv_imod_equality: "(m::inat) 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::inat) div n * n + m mod n = m"
by (insert idiv_imod_equality[of m n 0], simp)

lemma idiv_ile_mono: "m ≤ (n::inat) ==> 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_Infty)
apply (simp add: i0_lb[unfolded zero_inat_def])
done
lemma idiv_ile_mono2: "[| 0 < m; m ≤ (n::inat) |] ==> 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