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