Theory Arith_Thms

(*
  File: Arith_Thms.thy
  Author: Bohua Zhan

  Setup for proof steps related to arithmetic, mostly on natural numbers.
*)

section ‹Setup for arithmetic›

theory Arith_Thms
  imports Order_Thms HOL.Binomial
begin

(* Reducing inequality on natural numbers. *)
theorem reduce_le_plus_consts: "(x::nat) + n1  y + n2  x  y + (n2-n1)" by simp
theorem reduce_le_plus_consts': "n1  n2  (x::nat) + n1  y + n2  x + (n1-n2)  y" by simp
theorem reduce_less_plus_consts: "(x::nat) + n1 < y + n2  x < y + (n2-n1)" by simp
theorem reduce_less_plus_consts': "n1  n2  (x::nat) + n1 < y + n2  x + (n1-n2) < y" by simp

(* To normal form. *)
theorem norm_less_lminus: "(x::nat) - n < y  x  y + (n-1)" by simp
theorem norm_less_lplus:  "(x::nat) + n < y  x + (n+1)  y" by simp
theorem norm_less_rminus: "(x::nat) < y - n  x + (n+1)  y" by simp
theorem norm_less_rplus:  "(x::nat) < y + n  x  y + (n-1)" by simp
theorem norm_less:        "(x::nat) < y      x + 1  y"     by simp
theorem norm_le_lminus: "(x::nat) - n  y  x  y + n"  by simp
theorem norm_le_rminus: "(x::nat)  y - n  x  y + 0"  by simp
theorem norm_le: "(x::nat)  y  x  y + 0" by simp
theorem norm_le_lplus0: "(x::nat) + 0  y  x  y + 0" by simp

(* Transitive resolve. *)
theorem trans_resolve1: "n1 > 0  (x::nat) + n1  y  (y::nat) + n2  x  False" by simp
theorem trans_resolve2: "n1 > n2  (x::nat) + n1  y  (y::nat)  x + n2  False" by simp

(* Transitive. *)
theorem trans1: "(x::nat) + n1  y  y + n2  z  x + (n1+n2)  z" by simp
theorem trans2: "(x::nat)  y + n1  y  z + n2  x  z + (n1+n2)" by simp
theorem trans3: "(x::nat) + n1  y  y  z + n2  x  z + (n2-n1)" by simp
theorem trans4: "n1 > n2  (x::nat) + n1  y  y  z + n2  x + (n1-n2)  z" by simp
theorem trans5: "(x::nat)  y + n1  y + n2  z  x  z + (n1-n2)" by simp
theorem trans6: "n2 > n1  (x::nat)  y + n1  y + n2  z  x + (n2-n1)  z" by simp

(* Resolve. *)
theorem single_resolve: "n > 0  (x::nat) + n  x  False" by simp
theorem single_resolve_const: "n > 0  (x::nat) + n  0  False" by simp

(* Comparison with constants. *)
theorem cv_const1: "(x::nat) + n  y  0 + (x+n)  y" by simp  (* x is const *)
theorem cv_const2: "(x::nat) + n  y  x  0 + (y-n)" by simp  (* y is const *)
theorem cv_const3: "y < n  (x::nat) + n  y  x + (n-y)  0" by simp  (* y is const (contradiction with 0 ≤ x) *)
theorem cv_const4: "(x::nat)  y + n  0 + (x-n)  y" by simp  (* x is const *)
theorem cv_const5: "(x::nat)  y + n  0  y + (n-x)" by simp  (* x is const (trivial) *)
theorem cv_const6: "(x::nat)  y + n  x  0 + (y+n)" by simp  (* y is const *)

(* Misc *)
theorem nat_eq_to_ineqs: "(x::nat) = y + n  x  y + n  x  y + n" by simp
theorem nat_ineq_impl_not_eq: "(x::nat) + n  y  n > 0  x  y" by simp
theorem eq_to_ineqs: "(x::nat)  y  x  y  y  x" by simp
theorem ineq_to_eqs1: "(x::nat)  y + 0  y  x + 0  x = y" by simp

ML_file ‹arith.ML›
ML_file ‹order.ML›
ML_file ‹order_test.ML›

setup register_wellform_data ("(a::nat) - b", ["a ≥ b"])
setup add_prfstep_check_req ("(a::nat) - b", "(a::nat) ≥ b")

(* Normalize any expression to "a - b" form. *)
lemma nat_sub_norm:
  "(a::nat) = a - 0  a  0" by simp

(* Adding and subtracting two normalized expressions. *)
lemma nat_sub1:
  "(a::nat)  b  c  d  (a - b) + (c - d) = (a + c) - (b + d)  a + c  b + d" by simp

lemma nat_sub2:
  "(a::nat)  b  c  d  a - b  c - d  (a - b) - (c - d) = (a + d) - (b + c)  a + d  b + c" by simp

lemma nat_sub3:
  "(a::nat)  b  c  d  (a - b) * (c - d) = (a * c + b * d) - (a * d + b * c)  a * c + b * d  a * d + b * c"
  by (smt (verit) diff_mult_distrib mult.commute mult_le_mono1 nat_sub2)

(* Cancel identical terms on two sides, yielding a normalized expression. *)
lemma nat_sub_combine:
  "(a::nat) + b  c + b  (a + b) - (c + b) = a - c  a  c" by simp

lemma nat_sub_combine2:
  "n  m  (a::nat) + b * n  c + b * m  (a + b * n) - (c + b * m) = (a + b * (n - m)) - c  a + b * (n - m)  c  n  m"
  by (simp add: add.commute right_diff_distrib')

lemma nat_sub_combine3:
  "n  m  (a::nat) + b * n  c + b * m  (a + b * n) - (c + b * m) = a - (c + b * (m - n))  a  c + b * (m - n)  m  n"
  by (smt (verit) add.commute mult.commute nat_diff_add_eq2 nat_le_add_iff1)

ML_file ‹nat_sub.ML›
ML_file ‹nat_sub_test.ML›

(* Ordering on Nats. *)
lemma le_neq_implies_less' [forward]: "(m::nat)  n  m  n  m < n" by simp
lemma le_zero_to_equal_zero [forward]: "(n::nat)  0  n = 0" by simp
lemma less_one_to_equal_zero [forward]: "(n::nat) < 1  n = 0" by simp
setup add_backward_prfstep_cond @{thm Nat.mult_le_mono1} [with_cond "?k ≠ 1"]
setup add_resolve_prfstep @{thm Nat.not_add_less1}
lemma not_minus_less [resolve]: "¬(i::nat) < (i - j)" by simp
lemma nat_le_prod_with_same [backward]: "m  0  (n::nat)  m * n" by simp
lemma nat_le_prod_with_le [backward1]: "k  0  (n::nat)  m  (n::nat)  k * m"
  using le_trans nat_le_prod_with_same by blast
lemma nat_plus_le_to_less [backward1]: "b  0  (a::nat) + b  c  a < c" by simp
lemma nat_plus_le_to_less2 [backward1]: "a  0  (a::nat) + b  c  b < c" by simp
setup add_forward_prfstep @{thm add_right_imp_eq}
setup add_forward_prfstep @{thm add_left_imp_eq}

setup add_rewrite_rule_cond @{thm Nat.le_diff_conv2} [with_term "?i + ?k"]
lemma nat_less_diff_conv: "(i::nat) < j - k  i + k < j" by simp
setup add_forward_prfstep_cond @{thm nat_less_diff_conv} [with_cond "?k ≠ ?NUMC", with_term "?i + ?k"]
lemma Nat_le_diff_conv2_same [forward]: "i  j  (i::nat)  i - j  j = 0" by simp
lemma nat_gt_zero [forward]: "b - a > 0  b > (a::nat)" by simp
lemma n_minus_1_less_n: "(n::nat)  1  n - 1 < n" by simp
setup add_forward_prfstep_cond @{thm n_minus_1_less_n} [with_term "?n - 1"]

(* Monotonicity of ordering *)
setup add_backward_prfstep @{thm Nat.diff_le_mono}
setup add_backward2_prfstep @{thm Nat.diff_less_mono}
setup add_backward_prfstep @{thm Nat.mult_le_mono2}
setup add_resolve_prfstep @{thm Nat.le_add1}
setup add_resolve_prfstep @{thm Nat.le_add2}
setup add_backward_prfstep @{thm add_left_mono}
setup add_backward_prfstep @{thm add_right_mono}
lemma add_mono_neutr [backward]: "(0::'a::linordered_ring)  b  a  a + b" by simp
lemma add_mono_neutl [backward]: "(0::'a::linordered_ring)  b  a  b + a" by simp
setup add_forward_prfstep @{thm add_less_imp_less_left}
lemma sum_le_zero1 [forward]: "(a::'a::linordered_ring) + b < 0  a  0  b < 0" by (meson add_less_same_cancel1 less_le_trans)
lemma less_sum1 [backward]: "b > 0  a < a + (b::nat)" by auto
setup add_backward_prfstep @{thm Nat.trans_less_add2}
setup add_backward_prfstep @{thm Nat.add_less_mono1}
setup add_backward1_prfstep @{thm Nat.add_less_mono}
setup add_backward1_prfstep @{thm Nat.add_le_mono}
setup add_backward1_prfstep @{thm add_increasing2}
setup add_backward1_prfstep @{thm add_mono}
setup add_backward_prfstep @{thm add_strict_left_mono}
setup add_backward1_prfstep @{thm Nat.mult_le_mono}

(* Addition. *)
theorem nat_add_eq_self_zero [forward]: "(m::nat) = m + n  n = 0" by simp
theorem nat_add_eq_self_zero' [forward]: "(m::nat) = n + m  n = 0" by simp
theorem nat_mult_2: "(a::nat) + a = 2 * a" by simp
setup add_rewrite_rule_cond @{thm nat_mult_2} [with_cond "?a ≠ 0"]
theorem plus_one_non_zero [resolve]: "¬(n::nat) + 1 = 0" by simp

(* Diff. *)
lemma nat_same_minus_ge [forward]: "(c::nat) - a  c - b  a  c  a  b" by arith
lemma diff_eq_zero [forward]: "(k::nat)  j  j - k = 0  j = k" by simp
lemma diff_eq_zero' [forward]: "(k::nat)  j  j - k + i = j  k = i" by simp

(* Divides. *)
theorem dvd_defD1 [resolve]: "(a::nat) dvd b  k. b = a * k" using dvdE by blast
theorem dvd_defD2 [resolve]: "(a::nat) dvd b  k. b = k * a" by (metis dvd_mult_div_cancel mult.commute)
setup add_forward_prfstep @{thm Nat.dvd_imp_le}
theorem dvd_ineq2 [forward]: "(k::nat) dvd n  n > 0  k  1" by (simp add: Suc_leI dvd_pos_nat)

setup add_forward_prfstep_cond @{thm dvd_trans} (with_conds ["?a ≠ ?b", "?b ≠ ?c", "?a ≠ ?c"])
setup add_forward_prfstep_cond @{thm Nat.dvd_antisym} [with_cond "?m ≠ ?n"]
theorem dvd_cancel [backward1]: "c > 0  (a::nat) * c dvd b * c  a dvd b" by simp
setup add_forward_prfstep (equiv_forward_th @{thm dvd_add_right_iff})

(* Divisibility: existence. *)
setup add_resolve_prfstep @{thm dvd_refl}
theorem exists_n_dvd_n [backward]: "P (n::nat)  k. k dvd n  P k" using dvd_refl by blast
setup add_resolve_prfstep @{thm one_dvd}

theorem any_n_dvd_0 [forward]: "¬ ( k. k dvd (0::nat)  P k)  ¬ ( k. P k)" by simp

theorem n_dvd_one: "(n::nat) dvd 1  n = 1" by simp
setup add_forward_prfstep_cond @{thm n_dvd_one} [with_cond "?n ≠ 1"]

(* Products. *)
setup add_rewrite_rule @{thm mult_zero_left}
lemma prod_ineqs1 [forward]: "(m::nat) * k > 0  m > 0  k > 0" by simp
lemma prod_ineqs2 [backward]: "(k::nat) > 0  m  m * k" by simp

theorem prod_cancel: "(a::nat) * b = a * c  a > 0  b = c" by auto
setup add_forward_prfstep_cond @{thm prod_cancel} [with_cond "?b ≠ ?c"]

theorem mult_n1n: "(n::nat) = m * n  n > 0  m = 1" by auto
setup add_forward_prfstep_cond @{thm mult_n1n} [with_cond "?m ≠ 1"]

theorem prod_is_one [forward]: "(x::nat) * y = 1  x = 1" by simp

theorem prod_dvd_intro [backward]: "(k::nat) dvd m  k dvd n  k dvd m * n"
  using dvd_mult dvd_mult2 by blast

(* Definition of gcd. *)
setup add_forward_prfstep_cond @{thm gcd_dvd1} [with_term "gcd ?a ?b"]
setup add_forward_prfstep_cond @{thm gcd_dvd2} [with_term "gcd ?a ?b"]

(* Coprimality. *)
setup add_rewrite_rule_bidir @{thm coprime_iff_gcd_eq_1}
lemma coprime_exp [backward]: "coprime d a  coprime (d::nat) (a ^ n)" by simp
setup add_backward_prfstep @{thm coprime_exp}
setup add_rewrite_rule @{thm gcd.commute}
lemma coprime_dvd_mult [backward1]: "coprime (a::nat) b  a dvd c * b  a dvd c"
  by (metis coprime_dvd_mult_left_iff)
lemma coprime_dvd_mult' [backward1]: "coprime (a::nat) b  a dvd b * c  a dvd c"
  by (metis coprime_dvd_mult_right_iff)

theorem coprime_dvd [forward]:
  "coprime (a::nat) b  p dvd a  p > 1  ¬ p dvd b"
  using coprime_common_divisor_nat by blast

(* Powers. *)
setup add_rewrite_rule @{thm power_0}
theorem power_ge_0 [rewrite]: "m  0  p ^ m = p * (p ^ (m - 1))" by (simp add: power_eq_if)
setup add_rewrite_rule_cond @{thm power_one} [with_cond "?n ≠ 0"]
setup add_rewrite_rule_cond @{thm power_one_right} [with_cond "?a ≠ 1"]
setup add_gen_prfstep ("power_case_intro",
  [WithTerm @{term_pat "?p ^ (?FREE::nat)"}, CreateCase @{term_pat "(?FREE::nat) = 0"}])

lemma one_is_power_of_any [resolve]: "i. (1::nat) = a ^ i" by (metis power.simps(1))

setup add_rewrite_rule @{thm power_Suc}

theorem power_dvd [forward]: "(p::nat)^n dvd a  n  0  p dvd a" using dvd_power dvd_trans by blast

theorem power_eq_one: "(b::nat) ^ n = 1  b = 1  n = 0"
  by (metis One_nat_def Suc_lessI nat_zero_less_power_iff power_0 power_inject_exp)
setup add_forward_prfstep_cond @{thm power_eq_one} (with_conds ["?b ≠ 1", "?n ≠ 0"])

(* Factorial. *)
theorem fact_ge_1_nat: "fact (n::nat)  (1::nat)" by simp
setup add_forward_prfstep_cond @{thm fact_ge_1_nat} [with_term "fact ?n"]
setup add_backward1_prfstep @{thm dvd_fact}

(* Successor function. *)
setup add_rewrite_rule @{thm Nat.Suc_eq_plus1}
setup add_backward_prfstep @{thm Nat.gr0_implies_Suc}

(* Cases *)
setup fold add_rewrite_rule @{thms Nat.nat.case}

(* Induction. *)
lemma nat_cases: "P 0  (n. P (Suc n))  P n" using nat_induct by auto

(* div *)
declare times_div_less_eq_dividend [resolve]

setup add_var_induct_rule @{thm nat_induct} #>
  add_strong_induct_rule @{thm nat_less_induct} #>
  add_cases_rule @{thm nat_cases}

end