Theory DFI_square_1
theory DFI_square_1
imports DFI_square_0 Lucas_Diophantine
begin
fun rec_forte_init012::"nat ⇒ nat" where
"rec_forte_init012 0 = 0" |
"rec_forte_init012 (Suc 0) = 0" |
"rec_forte_init012 (Suc (Suc 0)) = 0" |
"rec_forte_init012 (Suc (Suc (Suc n))) = (∑i≤Suc (Suc n). rec_forte_init012 i)"
theorem strong_induct_init012 [consumes 0, case_names 0 1 2 sucsucsuc]:
"P 0 ⟹ P (Suc 0) ⟹ P (Suc (Suc 0)) ⟹ (⋀n. ( (∀i≤Suc (Suc n). P i) ⟹ P (Suc (Suc (Suc n))) ))
⟹ P (n::nat)"
using rec_forte_init012.induct by auto
lemma sun_lemma2:"⋀n k r. ψ A (k*n+r) =
(∑i≤n. int (n choose i) * (ψ A (Suc k) - A*ψ A k)^(n-i)*(ψ A k)^i*ψ A (r+i))"
proof -
have case_n1: "⋀r. ψ A (k+r)
= (∑i≤1. int (1 choose i) * (ψ A (k+1) - A*ψ A k)^(1-i)*(ψ A k)^i*ψ A (r+i))" for k
proof (induction k rule: strong_induct_init012)
case 0
then show ?case by auto
next
case 1
then show ?case by auto
next
case 2
then show ?case by auto
next
case (sucsucsuc k)
note t = this
hence IH_k: "ψ A (k+s)
= (∑i≤1. int (1 choose i) * (ψ A (k+1) - A*ψ A k)^(1-i)*(ψ A k)^i*ψ A (s+i))" for s by auto
have IH_Suck: "ψ A (Suc k+s)
= (∑i≤1. int (1 choose i) * (ψ A (Suc k+1) - A*ψ A (Suc k))^(1-i)*(ψ A (Suc k))^i*ψ A (s+i))"
for s
using t Suc_n_not_le_n nat_le_linear by blast
have IH_SucSuck: "ψ A (Suc (Suc k)+s) = (∑i≤1. int (1 choose i) * (ψ A (Suc (Suc k)+1)
- A*ψ A (Suc (Suc k)))^(1-i)*(ψ A (Suc (Suc k)))^i*ψ A (s+i))" for s
using t Suc_n_not_le_n nat_le_linear by blast
have "ψ A (Suc (Suc k)+r) = (ψ A (Suc (Suc k)+1)
- A*ψ A (Suc (Suc k)))*ψ A r + ψ A (Suc (Suc k)) * ψ A (r+1)"
using IH_SucSuck[of r] by (auto simp add: algebra_simps)
hence simp_psi_sucsuc: "ψ A (Suc (Suc k)+r)
= ψ A (Suc (Suc k)) * ψ A (r+1) - ψ A (Suc k) * ψ A r" by auto
have "ψ A (Suc k + r) = (ψ A (Suc k + 1) - A*ψ A (Suc k))*ψ A r + ψ A (Suc k) * ψ A (r+1)"
using IH_Suck[of r] by (auto simp add: algebra_simps)
hence "ψ A (Suc k + r) = ψ A (Suc k) * ψ A (r+1) - ψ A k * ψ A r" by auto
hence "ψ A (Suc (Suc (Suc k)) + r) = A*(ψ A (Suc (Suc k)) * ψ A (r+1) - ψ A (Suc k) * ψ A r)
- ψ A (Suc k) * ψ A (r+1) + ψ A k * ψ A r "
using simp_psi_sucsuc by auto
hence "ψ A (Suc (Suc (Suc k)) + r) = (A*ψ A (Suc (Suc k)) - ψ A (Suc k)) * ψ A (r+1)
- (A * ψ A (Suc k) - ψ A k)*ψ A r" by (auto simp add: algebra_simps)
hence simp_psi: "ψ A (Suc (Suc (Suc k)) + r)
= ψ A (Suc (Suc (Suc k))) * ψ A (r+1) - ψ A (Suc (Suc k))*ψ A r" by auto
have "(∑i≤1. int (1 choose i) * (ψ A (Suc (Suc (Suc k))+1)
- A*ψ A (Suc (Suc (Suc k))))^(1-i)*(ψ A (Suc (Suc (Suc k))))^i*ψ A (r+i))
= (ψ A (Suc (Suc (Suc (Suc k)))) - A*ψ A (Suc (Suc (Suc k))))*ψ A r
+ ψ A (Suc (Suc (Suc k))) *ψ A (r+1)"
by (auto simp add: algebra_simps)
hence "(∑i≤1. int (1 choose i) * (ψ A (Suc (Suc (Suc k))+1)
- A*ψ A (Suc (Suc (Suc k))))^(1-i)*(ψ A (Suc (Suc (Suc k))))^i*ψ A (r+i))
= - ψ A (Suc (Suc k)) * ψ A r + ψ A (Suc (Suc (Suc k))) * ψ A (r+1)" by simp
then show ?case using simp_psi by (auto simp add: algebra_simps)
qed
show "⋀k r. ψ A (k*n+r)
= (∑i≤n. int (n choose i) * (ψ A (Suc k) - A*ψ A k)^(n-i)*(ψ A k)^i*ψ A (r+i))" for n
proof (induction n rule: ψ_induct)
case 0
then show ?case by auto
next
case 1
then show ?case using case_n1 by auto
next
case (sucsuc n)
note t = this
have eq1: "ψ A (k*(n+2)+r)
= (∑i≤n+1. int ((n+1) choose i) * (ψ A (Suc k) - A*ψ A k)^(n+1-i)*(ψ A k)^i*ψ A (k+r+i))"
using t[of k "k+r"] by (auto simp add: algebra_simps)
have case_n1_to_ri: "ψ A (k+r+i) = (ψ A (k+1) - A*ψ A k)*ψ A (r+i) + ψ A k * ψ A (r+i+1)" for i
using case_n1[of k "r+i"] by (auto simp add: algebra_simps)
hence "(ψ A (k+1) - A*ψ A k)^(n+1-i)*(ψ A k)^i*ψ A (k+r+i)
= (ψ A (k+1) - A*ψ A k)^(n+1-i)*(ψ A k)^i*(ψ A (k+1) - A*ψ A k)*ψ A (r+i)
+ (ψ A (k+1) - A*ψ A k)^(n+1-i)*(ψ A k)^i*ψ A k*ψ A (r+i+1)" for i
using case_n1_to_ri[of i] distrib_left[of "(ψ A (k+1) - A*ψ A k)^(n+1-i)*(ψ A k)^i"
"(ψ A (k+1) - A*ψ A k)*ψ A (r+i)" "ψ A k * ψ A (r+i+1)"] by auto
hence "(ψ A (k+1) - A*ψ A k)^(n+1-i)*(ψ A k)^i*ψ A (k+r+i)
= (ψ A (k+1) - A*ψ A k)*(ψ A (k+1) - A*ψ A k)^(n+1-i)*(ψ A k)^i*ψ A (r+i)
+ (ψ A (k+1) - A*ψ A k)^(n+1-i)*ψ A k*(ψ A k)^i*ψ A (r+i+1)" for i by auto
hence "(ψ A (k+1) - A*ψ A k)^(n+1-i)*(ψ A k)^i*ψ A (k+r+i)
= (ψ A (k+1) - A*ψ A k)^(Suc (n+1-i))*(ψ A k)^i*ψ A (r+i)
+ (ψ A (k+1) - A*ψ A k)^(n+1-i)*(ψ A k)^(i+1)*ψ A (r+i+1)" for i
using power_Suc[of "ψ A (k+1) - A*ψ A k" "n+1-i"] power_Suc[of "ψ A k" i] by auto
hence "(ψ A (Suc k) - A*ψ A k)^(n+1-i)*(ψ A k)^i*ψ A (k+r+i)
= (ψ A (Suc k) - A*ψ A k)^(Suc (n+1-i))*(ψ A k)^i*ψ A (r+i)
+ (ψ A (Suc k) - A*ψ A k)^(n+1-i)*(ψ A k) ^(i+1) * ψ A (r+i+1)" for i by auto
hence "int ((n+1) choose i) * ((ψ A (Suc k) - A*ψ A k)^(n+1-i)*(ψ A k)^i*ψ A (k+r+i))
= int ((n+1) choose i) * ((ψ A (Suc k) - A*ψ A k)^(Suc (n+1-i))*(ψ A k)^i*ψ A (r+i)
+ (ψ A (Suc k) - A*ψ A k)^(n+1-i)*(ψ A k) ^(i+1) * ψ A (r+i+1))" for i by auto
hence "int ((n+1) choose i) * ((ψ A (Suc k) - A*ψ A k)^(n+1-i)*(ψ A k)^i*ψ A (k+r+i))
= int ((n+1) choose i) * ((ψ A (Suc k) - A*ψ A k)^(Suc (n+1-i))*(ψ A k)^i*ψ A (r+i))
+ int ((n+1) choose i) * ((ψ A (Suc k) - A*ψ A k)^(n+1-i)*(ψ A k) ^(i+1) * ψ A (r+i+1))" for i
by (auto simp add: algebra_simps)
hence "int ((n+1) choose i) * (ψ A (Suc k) - A*ψ A k)^(n+1-i)*(ψ A k)^i*ψ A (k+r+i)
= int ((n+1) choose i) * (ψ A (Suc k) - A*ψ A k)^(Suc (n+1-i))*(ψ A k)^i*ψ A (r+i)
+ int ((n+1) choose i) * (ψ A (Suc k) - A*ψ A k)^(n+1-i)*(ψ A k) ^(i+1) * ψ A (r+i+1)" for i
by (auto simp add: algebra_simps)
hence "ψ A (k*(n+2)+r) =
(∑i≤n+1. int ((n+1) choose i) * (ψ A (Suc k) - A*ψ A k)^(Suc (n+1-i))*(ψ A k)^i*ψ A (r+i)
+ int ((n+1) choose i) * (ψ A (Suc k) - A*ψ A k)^(n+1-i)*ψ A k ^(i+1) * ψ A (r+i+1))"
using eq1 by auto
hence eq2: "ψ A (k*(n+2)+r) =
(∑i≤n+1. int ((n+1) choose i) * (ψ A (Suc k) - A*ψ A k)^(Suc (n+1-i))*(ψ A k)^i*ψ A (r+i))
+ (∑i≤n+1. int ((n+1) choose i) * (ψ A (Suc k) - A*ψ A k)^(n+1-i)*(ψ A k)^(i+1)*ψ A (r+i+1))"
using sum.distrib[of "λi. int ((n+1) choose i)*(ψ A (Suc k) - A*ψ A k)^(Suc (n+1-i))*(ψ A k)^i*ψ A (r+i)"
"λi. int ((n+1) choose i) *(ψ A (Suc k) - A*ψ A k)^(n+1-i)*(ψ A k)^(i+1)*ψ A (r+i+1)" "{..n+1}"]
by auto
have "i ≤ n+1 ⟹ int ((n+1) choose i) * (ψ A (Suc k) - A*ψ A k)^(n+1-i)*(ψ A k)^(i+1)*ψ A (r+i+1)
= int (n+1 choose (i+1-1))*(ψ A (Suc k)- A*ψ A k) ^(n+2-(i+1))*ψ A k ^ (i+1)*ψ A (r+(i+1))" for i
by auto
hence "ψ A (k*(n+2)+r) =
(∑i≤n+1. int ((n+1) choose i) * (ψ A (Suc k) - A*ψ A k)^(Suc (n+1-i))*(ψ A k)^i*ψ A (r+i))
+ (∑i≤n + 1. int (n+1 choose (i+1-1))*(ψ A (Suc k)- A*ψ A k) ^(n+2-(i+1))
* ψ A k ^ (i+1)*ψ A (r+(i+1)))"
using eq2 by (auto simp add: algebra_simps)
hence "ψ A (k*(n+2)+r) =
(∑i=0..n+1. int ((n+1) choose i) * (ψ A (Suc k) - A*ψ A k)^(Suc (n+1-i))*(ψ A k)^i*ψ A (r+i))
+ (∑i=0..n + 1. int (n+1 choose (i+1-1))*(ψ A (Suc k)- A*ψ A k) ^(n+2-(i+1))
* ψ A k ^ (i+1)*ψ A (r+(i+1)))"
using atMost_atLeast0 by presburger
hence eq3: "ψ A (k*(n+2)+r) =
(∑i=0..n+1. int ((n+1) choose i) * (ψ A (Suc k) - A*ψ A k)^(Suc (n+1-i))*(ψ A k)^i*ψ A (r+i))
+ (∑i=1..n+2. int ((n+1) choose (i-1)) * (ψ A (Suc k) - A*ψ A k)^(n+2-i)*(ψ A k)^i*ψ A (r+i))"
using translation_var_0_to_1[of "λi. int ((n+1) choose (i-1))*(ψ A (Suc k) - A*ψ A k)^(n+2-i)*(ψ A k)^i*ψ A (r+i)" "n+1"]
by auto
have obvious: "{0}∪{1..n+1} = {0..n+1} ∧ {0}∩{1..n+1} = {} ∧ finite {0} ∧ finite {1..n+1}
∧ finite {n+2} ∧ {1..n+1}∪{n+2} = {1..n+2} ∧ {1..n+1}∩{n+2} = {}" by auto
hence "ψ A (k*(n+2)+r) =
int ((n+1) choose 0) * (ψ A (Suc k) - A*ψ A k)^(Suc (n+1-0))*(ψ A k)^0*ψ A (r+0)
+ (∑i=1..n+1. int ((n+1) choose i) * (ψ A (Suc k) - A*ψ A k)^(Suc (n+1-i))*(ψ A k)^i*ψ A (r+i))
+ (∑i=1..n+1. int ((n+1) choose (i-1)) * (ψ A (Suc k) - A*ψ A k)^(n+2-i)*(ψ A k)^i*ψ A (r+i))
+ int ((n+1) choose ((n+2)-1)) * (ψ A (Suc k) - A*ψ A k)^(n+2-(n+2))*(ψ A k)^(n+2)*ψ A (r+(n+2))"
using sum.union_disjoint[of "{0}" "{1..n+1}" "λi. int ((n+1) choose i) * (ψ A (Suc k) - A*ψ A k)^(Suc (n+1-i))*(ψ A k)^i*ψ A (r+i)"]
sum.union_disjoint[of "{1..n+1}" "{n+2}"
"λi. int ((n+1) choose (i-1)) * (ψ A (Suc k) - A*ψ A k)^(n+2-i)*(ψ A k)^i*ψ A (r+i)"]
Suc_1 add_Suc_right diff_le_self diff_self_eq_0 eq3 numeral_1_eq_Suc_0 numerals(1)
sum.atLeast_Suc_atMost sum.nat_ivl_Suc' by auto
hence "ψ A (k*(n+2)+r) =
int ((n+1) choose 0) * (ψ A (Suc k) - A*ψ A k)^(Suc (n+1-0))*(ψ A k)^0*ψ A (r+0)
+ (∑i=1..n+1. int ((n+1) choose i) * (ψ A (Suc k) - A*ψ A k)^(Suc (n+1-i))*(ψ A k)^i*ψ A (r+i)
+ int ((n+1) choose (i-1)) * (ψ A (Suc k) - A*ψ A k)^(n+2-i)*(ψ A k)^i*ψ A (r+i))
+ int ((n+1) choose ((n+2)-1)) * (ψ A (Suc k) - A*ψ A k)^(n+2-(n+2))*(ψ A k)^(n+2)*ψ A (r+(n+2))"
using sum.distrib[of "λi. int ((n+1) choose i) * (ψ A (Suc k) - A*ψ A k)^(Suc (n+1-i))*(ψ A k)^i*ψ A (r+i)"
"λi. int ((n+1) choose (i-1)) * (ψ A (Suc k) - A*ψ A k)^(n+2-i)*(ψ A k)^i*ψ A (r+i)" "{1..n+1}"]
by auto
hence eq4: "ψ A (k*(n+2)+r) =
int ((n+2) choose 0) * (ψ A (Suc k) - A*ψ A k)^(n+2-0)*(ψ A k)^0*ψ A (r+0)
+ (∑i=1..n+1. int ((n+1) choose i) * (ψ A (Suc k) - A*ψ A k)^(Suc (n+1-i))*(ψ A k)^i*ψ A (r+i)
+ int ((n+1) choose (i-1)) * (ψ A (Suc k) - A*ψ A k)^(n+2-i)*(ψ A k)^i*ψ A (r+i))
+ int ((n+2) choose (n+2)) * (ψ A (Suc k) - A*ψ A k)^(n+2-(n+2))*(ψ A k)^(n+2)*ψ A (r+(n+2))"
by (auto simp add: algebra_simps)
have "i∈{1..n+1} ⟹ int ((n+1) choose i) * (ψ A (Suc k) - A*ψ A k)^(Suc (n+1-i))*(ψ A k)^i*ψ A (r+i)
+ int ((n+1) choose (i-1)) * (ψ A (Suc k) - A*ψ A k)^(n+2-i)*(ψ A k)^i*ψ A (r+i)
= int ((n+1) choose i) * (ψ A (Suc k) - A*ψ A k)^(n+2-i)*(ψ A k)^i*ψ A (r+i)
+ int ((n+1) choose (i-1)) * (ψ A (Suc k) - A*ψ A k)^(n+2-i)*(ψ A k)^i*ψ A (r+i)" for i
by (simp add: Suc_diff_le)
hence "i∈{1..n+1} ⟹ int ((n+1) choose i)*(ψ A (Suc k)-A*ψ A k)^(Suc (n+1-i))*(ψ A k)^i*ψ A (r+i)
+ int ((n+1) choose (i-1)) * (ψ A (Suc k) - A*ψ A k)^(n+2-i)*(ψ A k)^i*ψ A (r+i)
= (int ((n+1) choose i)
+ int ((n+1) choose (i-1))) * (ψ A (Suc k) - A*ψ A k)^(n+2-i)*(ψ A k)^i*ψ A (r+i)" for i
by (auto simp add: algebra_simps)
hence "i∈{1..n+1} ⟹ int ((n+1) choose i)*(ψ A (Suc k)-A*ψ A k)^(Suc (n+1-i))*(ψ A k)^i*ψ A (r+i)
+ int ((n+1) choose (i-1)) * (ψ A (Suc k) - A*ψ A k)^(n+2-i)*(ψ A k)^i*ψ A (r+i)
= int ((n+2) choose i)* (ψ A (Suc k) - A*ψ A k)^(n+2-i)*(ψ A k)^i*ψ A (r+i)" for i
using choose_reduce_nat[of "n+2" i] by auto
hence "ψ A (k*(n+2)+r) = int ((n+2) choose 0) * (ψ A (Suc k) - A*ψ A k)^(n+2-0)*(ψ A k)^0*ψ A (r+0)
+ (∑i=1..n+1. int ((n+2) choose i) * (ψ A (Suc k) - A*ψ A k)^(n+2-i)*(ψ A k)^i*ψ A (r+i))
+ int ((n+2) choose (n+2)) * (ψ A (Suc k) - A*ψ A k)^(n+2-(n+2))*(ψ A k)^(n+2)*ψ A (r+(n+2))"
using eq4 by auto
hence "ψ A (k*(n+2)+r) = int ((n+2) choose 0) * (ψ A (Suc k) - A*ψ A k)^(n+2-0)*(ψ A k)^0*ψ A (r+0)
+ (∑i=1..n+2. int ((n+2) choose i) * (ψ A (Suc k) - A*ψ A k)^(n+2-i)*(ψ A k)^i*ψ A (r+i))"
by auto
hence "ψ A (k*(n+2)+r) =
(∑i=0..n+2. int ((n+2) choose i) * (ψ A (Suc k) - A*ψ A k)^(n+2-i)*(ψ A k)^i*ψ A (r+i))"
using obvious by (simp add: sum.atLeast_Suc_atMost)
hence "ψ A (k*(n+2)+r) =
(∑i≤n+2. int ((n+2) choose i) * (ψ A (Suc k) - A*ψ A k)^(n+2-i)*(ψ A k)^i*ψ A (r+i))"
using atMost_atLeast0 by presburger
then show ?case by simp
qed
qed
lemma lucas_consec_coprime: "coprime (ψ A k) (ψ A (Suc k))"
proof (induction k)
case 0
then show ?case by simp
next
case (Suc k)
note IH=this
have "∀c. c dvd ψ A (Suc k) ∧ c dvd ψ A (Suc (Suc k)) ⟶ is_unit c"
proof
fix c
show "c dvd ψ A (Suc k) ∧ c dvd ψ A (Suc (Suc k)) ⟶ is_unit c"
proof
assume divhyp: "c dvd ψ A (Suc k) ∧ c dvd ψ A (Suc (Suc k))"
then have "c dvd A * ψ A (Suc k) - ψ A k" by simp
then have "c dvd ψ A k" using divhyp by algebra
then show "is_unit c" using divhyp IH by fastforce
qed
qed
then show ?case unfolding coprime_def by simp
qed
lemma eq_mod_power: fixes a::int and b::int assumes "a mod n = b mod n" shows "a^k mod n = b^k mod n"
proof (induction k)
case 0
then show ?case by simp
next
case (Suc k)
note IH=this
then show "a ^ Suc k mod n = b ^ Suc k mod n" using assms mod_mult_cong[of a n b "a^k" "b^k"]
by fastforce
qed
lemma euclids_lemma: "(coprime (a::int) b) ∧ a dvd (b*c) ⟶ a dvd c"
using coprime_dvd_mult_right_iff by blast
lemma coprime_power: fixes a::int and b::int assumes "coprime a b" shows "coprime (a^k) b"
proof (induction k)
case 0
then show ?case by simp
next
case (Suc k)
note IH=this
then have "c dvd a ^ Suc k ∧ c dvd b ⟹ is_unit c" for c
proof -
assume assm: "c dvd a ^ Suc k ∧ c dvd b"
then have "coprime c a"
by (meson assms coprime_def dvd_trans)
then show "is_unit c"
using euclids_lemma[of c a "a^k"] IH assm by fastforce
qed
then show "coprime (a^(Suc k)) b"
by fastforce
qed
lemma dvd_remove_psi:
fixes A::int and k::nat and m::nat
assumes "(ψ A k) dvd (ψ A m)" and "A^2-4≥0" and "k>0"
shows "(int k) dvd (int m)"
proof -
define r where "r = m mod k"
then have "∃n. m = n * k + r"
using div_mod_decomp by blast
then obtain n where n_def: "m = n * k + r" by auto
have termszero:"∀i∈{1..n}. int(n choose i) * (ψ A (Suc k)
- A*ψ A k)^(n-i) * (ψ A k)^i * ψ A (r+i) mod (ψ A k) = 0"
by simp
have yes: "finite {0} ∧ finite {1..n} ∧ {0} ∩ {1..n} = {} ∧ {0}∪{1..n} = {0..n}" by auto
have termszero2: "(∑i∈{1..n}. (int(n choose i) * (ψ A (Suc k) - A*ψ A k)^(n-i) * (ψ A k)^i
* ψ A (r+i)) mod (ψ A k)) = 0"
using termszero sum.neutral by fast
have eq1: "ψ A m mod (ψ A k) = (∑i≤n. int(n choose i) * (ψ A (Suc k) - A*ψ A k)^(n-i)
* (ψ A k)^i * ψ A (r+i)) mod (ψ A k)"
using n_def sun_lemma2[of "A" "k" "n" "r"] by (simp add: mult.commute)
also have eq2: "... = (∑i≤n. (int(n choose i) * (ψ A (Suc k) - A*ψ A k)^(n-i) * (ψ A k)^i
* ψ A (r+i)) mod (ψ A k)) mod (ψ A k)"
by (simp add: mod_sum_eq)
have eq3: "(∑i≤n. (int(n choose i) * (ψ A (Suc k) - A*ψ A k)^(n-i) * (ψ A k)^i * ψ A (r+i)) mod (ψ A k))
= (∑i≤0. (int(n choose i) * (ψ A (Suc k) - A*ψ A k)^(n-i) * (ψ A k)^i * ψ A (r+i)) mod (ψ A k))
+ (∑i∈{1..n}. (int(n choose i) * (ψ A (Suc k) - A*ψ A k)^(n-i) * (ψ A k)^i * ψ A (r+i)) mod (ψ A k))"
using sum.union_disjoint[of "{0}" "{1..n}"
"(λi. int (n choose i) * (ψ A (Suc k) - A * ψ A k) ^ (n - i) * ψ A k ^ i * ψ A (r + i) mod ψ A k)"]
yes
by (metis atMost_0 atMost_atLeast0)
moreover have eq4: "... = (∑i≤0. (int(n choose i) * (ψ A (Suc k) - A*ψ A k)^(n-i)
* (ψ A k)^i * ψ A (r+i)) mod (ψ A k)) mod (ψ A k)"
using termszero2 by simp
moreover have eq5: "... = ((ψ A (Suc k) - A*ψ A k)^n * ψ A (r)) mod (ψ A k)"
by fastforce
have eq5': "(∑i≤n. (int(n choose i) * (ψ A (Suc k) - A*ψ A k)^(n-i) * (ψ A k)^i * ψ A (r+i)) mod (ψ A k))
= ((ψ A (Suc k) - A*ψ A k)^n * ψ A (r)) mod (ψ A k)"
using eq3 eq4 eq5 by metis
have "(ψ A (Suc k) - A*ψ A k) mod (ψ A k) = (ψ A (Suc k)) mod (ψ A k)" by algebra
then have "(ψ A (Suc k) - A*ψ A k)^n mod (ψ A k) = (ψ A (Suc k))^n mod (ψ A k)"
using eq_mod_power by fast
then have eq6: "((ψ A (Suc k) - A*ψ A k)^n * ψ A (r)) mod (ψ A k) = ((ψ A (Suc k))^n * ψ A (r)) mod (ψ A k)"
using mod_mult_cong by fast
then have eq7: "0 = ((ψ A (Suc k))^n * ψ A (r)) mod (ψ A k)"
using assms eq1 eq2 eq5' eq6 by simp
then have eq8: "(ψ A k) dvd (ψ A (Suc k))^n * ψ A r" by fastforce
have "coprime ((ψ A (Suc k))^n) (ψ A k)"
using lucas_consec_coprime[of A k] coprime_power coprime_commute by blast
then have eq9: "ψ A k dvd ψ A r"
using eq8 euclids_lemma coprime_commute by blast
have "(abs A)^2 ≥ 4" using assms by simp
then have ABe2: "abs A ≥ 2"
by (smt (verit, ccfv_SIG) abs_1 abs_square_le_1 zero_power2)
have "r<k" using r_def ‹k>0› by simp
then have "r + (k - r - 1) = k-1 ∧ Suc (k-1) = k" by simp
then have "ψ (abs A) r < ψ (abs A) k"
using ABe2 lucas_monotone2[of "abs A" r "k-r-1"] lucas_strict_monotonicity[of "abs A" "k-1"] by simp
then have "abs (ψ A r) < abs (ψ A k)" using lucas_symmetry_A_abs ABe2 by fastforce
then have psir0:"ψ A r = 0" using eq9
by (meson abs_dvd_iff dvd_abs_iff zdvd_not_zless zero_less_abs_iff)
have contr: "r>0 ⟹ abs(ψ A r) > 0"
using ABe2 lucas_strict_monotonicity[of "abs A" "r-1"] lucas_symmetry_A_abs[of A r] by simp
then have "r=0" using psir0 by auto
then have "int m = int k * int n" using n_def by simp
then show ?thesis by simp
qed
lemma sun_lemma7:
fixes A::int and k::nat and m::nat
assumes "A^2-4≥0" and "(ψ A k)^2 dvd ψ A m" and "k>0"
shows "ψ A k dvd (int m)"
proof -
have "k dvd m" using assms dvd_remove_psi[of A k m] by auto
then obtain "n" where n_def: "m = k * n" by auto
then show ?thesis
proof (cases "n=0")
case True
then show ?thesis using n_def by simp
next
case False
have "i≥2 ⟶ (ψ A k)^i = (ψ A k)^2 * (ψ A k)^(i-2)" for i
by (metis le_add_diff_inverse2 mult.commute power_add)
then have "∀i∈{2..n}. ((ψ A k)^i) mod (ψ A k)^2 = 0"
by (meson atLeastAtMost_iff dvd_imp_mod_0 le_imp_power_dvd)
then have termszero: "∀i∈{2..n}. (int (n choose i) * (ψ A (Suc k) - A*ψ A k)^(n-i)
*(ψ A k)^i*ψ A i) mod (ψ A k)^2 = 0"
by auto
have disj_sum: "finite {..(1::nat)} ∧ finite {2..n} ∧ {..1} ∩ {2..n} = {}
∧ {0..1}∪{2..n} = {0..n}"
using ‹n≠0› by auto
have "0 = (ψ A m) mod (ψ A k)^2" using assms by simp
also have "... = (∑i≤n. int (n choose i) * (ψ A (Suc k) - A*ψ A k)^(n-i)*(ψ A k)^i*ψ A i)mod (ψ A k)^2"
using n_def sun_lemma2[of A k n 0] by simp
also have "... = (∑i≤n. int (n choose i) * (ψ A (Suc k) - A*ψ A k)^(n-i)*(ψ A k)^i*ψ A i mod (ψ A k)^2) mod (ψ A k)^2"
using mod_sum_eq[of "(λi. (int (n choose i) * (ψ A (Suc k) - A*ψ A k)^(n-i)*(ψ A k)^i*ψ A i ) )" "(ψ A k)^2" "{..n}"] by simp
also have "... = ( (∑i≤1. int (n choose i) * (ψ A (Suc k) - A*ψ A k)^(n-i)*(ψ A k)^i*ψ A i mod (ψ A k)^2 )
+ (∑i∈{2..n}. int (n choose i) * (ψ A (Suc k) - A*ψ A k)^(n-i)*(ψ A k)^i*ψ A i mod (ψ A k)^2 ) )mod (ψ A k)^2"
using disj_sum sum.union_disjoint[of "{..(1::nat)}" "{2..n}"
"(λi. (int (n choose i) * (ψ A (Suc k) - A*ψ A k)^(n-i)*(ψ A k)^i*ψ A i mod (ψ A k)^2) )"]
by (metis (mono_tags, lifting) atMost_atLeast0)
also have "... = (∑i≤1. int (n choose i) * (ψ A (Suc k) - A*ψ A k)^(n-i)*(ψ A k)^i*ψ A i mod (ψ A k)^2 ) mod (ψ A k)^2"
using termszero sum.neutral by simp
finally have mod_eq1: "0 = int(n) * (ψ A (Suc k) - A*ψ A k)^(n-1)*(ψ A k) mod (ψ A k)^2"
by force
have "(abs A)^2 ≥ 4" using assms by simp
then have ABe2: "abs A ≥ 2"
by (smt (verit, ccfv_SIG) abs_1 abs_square_le_1 zero_power2)
have psiAknn: "abs(ψ A k) > 0"
using ABe2 assms lucas_strict_monotonicity[of "abs A" "k-1"] lucas_symmetry_A_abs[of A k] by simp
then have "ψ A k dvd int(n) * (ψ A (Suc k) - A*ψ A k)^(n-1)"
using mod_eq1 by (smt (z3) dvd_times_right_cancel_iff mod_0_imp_dvd power2_eq_square)
then have mod_eq2:"0 = int(n) * (ψ A (Suc k) - A*ψ A k)^(n-1) mod (ψ A k)" by simp
have "(ψ A (Suc k) - A*ψ A k) mod (ψ A k) = (ψ A (Suc k)) mod (ψ A k)" by algebra
then have "(ψ A (Suc k) - A*ψ A k)^(n-1) mod (ψ A k) = (ψ A (Suc k))^(n-1) mod (ψ A k)"
using eq_mod_power by fast
then have mod_eq3:"0 = int(n) * (ψ A (Suc k))^(n-1) mod (ψ A k)"
using mod_eq2 mod_mult_cong by metis
then have eq4:"(ψ A k) dvd int(n) * (ψ A (Suc k))^(n-1)" by fastforce
have "coprime ((ψ A (Suc k))^(n-1)) (ψ A k)"
using lucas_consec_coprime[of A k] coprime_power coprime_commute by blast
then have "ψ A k dvd int n"
using eq4 euclids_lemma coprime_commute mult.commute by metis
then show "ψ A k dvd int m" using n_def by simp
qed
qed
text ‹Introducing ‹ψ› and ‹χ› with both interger parameters. It is a broader definition but induction
is harder, that's why a lot of properties for these vesion are proved in the following lemmas›
definition ψ_int::"int ⇒ int ⇒ int" where
"ψ_int A n = (-1)^(if n ≥ 0 then 0 else 1) * ψ A (nat (abs n))"
definition χ_int::"int ⇒ int ⇒ int" where
"χ_int A n = χ A (nat (abs n))"
lemma ψ_int_eq: "ψ_int A n = (if n ≥ 0 then 1 else -1) * ψ A (nat (abs n))"
unfolding ψ_int_def by auto
lemma ψ_int_ind:
fixes A::int and n::int
shows "ψ_int A (n+2) = A*ψ_int A (n+1) - ψ_int A n"
proof -
consider (2) "n=-2" | (1) "n=-1" | (pos) "n ≥ 0" |(neg) "n ≤ -3" by linarith
then show ?thesis
proof cases
case 2
note t=this
have "ψ A 2 = A ∧ ψ A 1 = 1 ∧ ψ A 0 = 0"
by (smt (verit, ccfv_SIG) ψ.elims ψ.simps(1) ψ.simps(2) add_diff_cancel_left' diff_Suc_1
mult_cancel_left2 nat_1_add_1 numeral_1_eq_Suc_0 numeral_One zero_neq_numeral)
hence "ψ_int A (-2) = -A ∧ ψ_int A (-1) = -1 ∧ ψ_int A 0 = 0" unfolding ψ_int_def by auto
then show ?thesis using t by simp
next
case 1
note t=this
have "ψ_int A (-1) = -1 ∧ ψ_int A 0 = 0 ∧ ψ_int A 1 = 1" unfolding ψ_int_def by auto
then show ?thesis using t by simp
next
case pos
have triv_abs: "n ≥ 0 ∧ n+1 ≥ 0 ∧ n+2 ≥ 0 ∧ nat (abs (n+1)) = nat (abs n) +1
∧ nat (abs (n+2)) = nat (abs n) +2"
by (simp add: nat_add_distrib pos)
hence "ψ_int A n = ψ A (nat (abs n)) ∧ ψ_int A (n+1) = ψ A (nat (abs n) +1)
∧ ψ_int A (n+2) = ψ A (nat (abs n) +2)"
unfolding ψ_int_def by (simp add: triv_abs mult_numeral_1)
then show ?thesis by auto
next
case neg
hence triv_abs2: "n < 0 ∧ n+1 < 0 ∧ n+2 < 0 ∧ nat (abs (n+1)) = nat (abs (n+2)) +1
∧ nat (abs n) = nat (abs (n+2)) +2"
by auto
hence "ψ_int A n = -ψ A (nat (abs (n+2))+2) ∧ ψ_int A (n+1) = -ψ A (nat (abs (n+2)) +1)
∧ ψ_int A (n+2) = -ψ A (nat (abs (n+2)))"
unfolding ψ_int_def by auto
then show ?thesis by auto
qed
qed
lemma χ_int_ind:
fixes A::int and n::int
shows "χ_int A (n+2) = A*χ_int A (n+1) - χ_int A n"
proof -
consider (2) "n=-2" | (1) "n=-1" | (pos) "n ≥ 0" |(neg) "n ≤ -3" by linarith
then show ?thesis
proof cases
case 2
note t=this
have "χ A 2 = A*A-2 ∧ χ A 1 = A ∧ χ A 0 = 2"
by (metis One_nat_def Suc_1 χ.simps(1) χ.simps(2) χ.simps(3))
hence "χ_int A (-2) = A*A-2 ∧ χ_int A (-1) = A ∧ χ_int A 0 = 2" unfolding χ_int_def by auto
then show ?thesis using t by simp
next
case 1
note t=this
have "χ_int A (-1) = A ∧ χ_int A 0 = 2 ∧ χ_int A 1 = A" unfolding χ_int_def by auto
then show ?thesis using t by simp
next
case pos
have triv_abs: "n ≥ 0 ∧ n+1 ≥ 0 ∧ n+2 ≥ 0 ∧ nat (abs (n+1)) = nat (abs n) +1
∧ nat (abs (n+2)) = nat (abs n) +2"
by (simp add: nat_add_distrib pos)
hence "χ_int A n = χ A (nat (abs n)) ∧ χ_int A (n+1) = χ A (nat (abs n) +1)
∧ χ_int A (n+2) = χ A (nat (abs n) +2)"
unfolding χ_int_def by (simp add: triv_abs mult_numeral_1)
then show ?thesis by auto
next
case neg
hence triv_abs2: "n < 0 ∧ n+1 < 0 ∧ n+2 < 0 ∧ nat (abs (n+1)) = nat (abs (n+2)) +1
∧ nat (abs n) = nat (abs (n+2)) +2"
by auto
hence "χ_int A n = χ A (nat (abs (n+2))+2) ∧ χ_int A (n+1) = χ A (nat (abs (n+2)) +1)
∧ χ_int A (n+2) = χ A (nat (abs (n+2)))"
unfolding χ_int_def by auto
then show ?thesis by auto
qed
qed
lemma ψ_int_odd:
fixes A::int and n::int
shows "ψ_int A (-n) = -ψ_int A n"
unfolding ψ_int_def by auto
lemma χ_int_even:
fixes A::int and n::int
shows "χ_int A (-n) = χ_int A n"
unfolding χ_int_def by auto
lemma technical_lemma1:
fixes k::int and r::int and A::int
shows "ψ_int A (k+r) = ψ_int A r * χ_int A k + ψ_int A (k-r)"
proof -
have case_pos: "ψ_int A (int l +s) = ψ_int A s * χ_int A (int l) + ψ_int A (int l-s)"
for l::nat and s::int
proof (induction l rule: ψ_induct)
case 0
have "χ_int A (int 0) = 2 ∧ ψ_int A (int 0 - s) = - ψ_int A s"
unfolding χ_int_def ψ_int_def by auto
then show ?case by auto
next
case 1
have "χ_int A (int 1) = A ∧ ψ_int A (int 1 - s) = -ψ_int A (s - 1)"
unfolding χ_int_def using ψ_int_odd[of A "s - 1"] by auto
then show ?case using ψ_int_ind[of A " s - 1"] by auto
next
case (sucsuc l)
note t = this
have "ψ_int A (int (Suc (Suc l)) + s) = ψ_int A (int l + s +2)"
by (auto simp add: algebra_simps)
hence "ψ_int A (int (Suc (Suc l))+s) = A*ψ_int A (int (Suc l)+s) - ψ_int A (int l+s)"
using ψ_int_ind[of A "int l+s"] by (auto simp add: algebra_simps)
hence "ψ_int A (int (Suc (Suc l))+s) = ψ_int A s*(A*χ_int A (int l + 1) - χ_int A (int l))
+ A*ψ_int A (int l - s + 1) - ψ_int A (int l - s)"
using t by (auto simp add: algebra_simps)
hence "ψ_int A (int (Suc (Suc l))+s) = ψ_int A s*χ_int A (int l + 2) + ψ_int A (int l - s +2)"
using ψ_int_ind[of A "int l - s"] χ_int_ind[of A "int l"] by auto
then show ?case by (auto simp add: algebra_simps)
qed
then show ?thesis
proof (cases k)
case (nonneg k)
then show ?thesis using case_pos[of k r] by auto
next
case (neg n)
hence intnatk: "int (nat (abs k)) = - k" by auto
hence "ψ_int A (-k+r) = ψ_int A r * χ_int A (-k) + ψ_int A (-k-r)"
using case_pos[of "nat (abs k)" r] by argo
hence "-ψ_int A (k-r) = ψ_int A r * χ_int A k - ψ_int A (k+r)"
using ψ_int_odd[of A "k-r"] ψ_int_odd[of A "k+r"] χ_int_even[of A k] by auto
then show ?thesis by auto
qed
qed
text ‹It is now much easier to state the following lemma›
lemma technical_lemma2:
fixes r::int and A::int and n::int and q::int and k::int
assumes "n ≠ 0" and "χ_int A n = 2*k"
shows "ψ_int A (2*n+r) mod (χ_int A n) = (-ψ_int A r) mod (χ_int A n)"
and "ψ_int A (4*n*q+r) mod k = ψ_int A r mod k"
proof -
have "ψ_int A (2*n+s) = ψ_int A (n+s) * χ_int A n + ψ_int A (-s)" for s
using technical_lemma1[of A n "n+s"] by auto
hence "ψ_int A (2*n+s) mod (χ_int A n) = ψ_int A (-s) mod (χ_int A n)" for s
by (auto simp add: algebra_simps)
hence first_fact: "ψ_int A (2*n+s) mod (χ_int A n) = (-ψ_int A s) mod (χ_int A n)" for s
using ψ_int_odd[of A s] by auto
thus "ψ_int A (2*n+r) mod (χ_int A n) = (-ψ_int A r) mod (χ_int A n)" by auto
have dvd_mod: "a dvd b ⟹ l mod b = m mod b ⟹ l mod a = m mod a" for a::int and b and l and m
by (metis mod_mod_cancel)
have cor_modk: "ψ_int A (2*n+s) mod k = (-ψ_int A s) mod k" for s
using assms first_fact dvd_mod[of k "χ_int A n" "ψ_int A (2*n+s)" "-ψ_int A s"] by auto
have cor_modk2: "ψ_int A (-2*n+s) mod k = (-ψ_int A s) mod k" for s
using cor_modk[of "-2*n*s"] using mod_minus_cong by (smt (z3) cor_modk)
have q_identity: "⋀r. ψ_int A (4*n*int s+r) mod k = ψ_int A r mod k
∧ ψ_int A (-4*n*int s+r) mod k = ψ_int A r mod k" for s::nat
proof (induction s)
case 0
then show ?case by auto
next
case (Suc s)
note t = this
have "ψ_int A (4*n*int (Suc s)+r) = ψ_int A (4*n*int s + (4*n+r))
∧ ψ_int A (-4*n*int (Suc s)+r) = ψ_int A (-4*n*int s + (-4*n+r))"
by (auto simp add: algebra_simps)
hence "ψ_int A (4*n*int (Suc s)+r) mod k = ψ_int A (4*n+r) mod k
∧ ψ_int A (-4*n*int (Suc s)+r) mod k = ψ_int A (-4*n+r) mod k"
using t[of "4*n+r"] t[of "-4*n+r"] by auto
hence "ψ_int A (4*n*int (Suc s)+r) mod k = (-ψ_int A (2*n+r)) mod k
∧ ψ_int A (-4*n*int (Suc s)+r) mod k = (-ψ_int A (-2*n+r)) mod k"
using cor_modk[of "2*n+r"] cor_modk2[of "-2*n+r"] by auto
thus "ψ_int A (4*n*int (Suc s)+r) mod k = ψ_int A r mod k
∧ ψ_int A (-4*n*int (Suc s)+r) mod k = ψ_int A r mod k"
using cor_modk[of r] cor_modk2[of r] mod_minus_cong by (metis add.inverse_inverse)
qed
thus "ψ_int A (4*n*q+r) mod k = ψ_int A r mod k"
proof (cases q)
case (nonneg l)
then show ?thesis using q_identity[of "nat q" r] by auto
next
case (neg l)
then show ?thesis using q_identity[of "nat (-q)" r] by (auto simp add: algebra_simps)
qed
qed
lemma lucas_solves_pell:
fixes A :: int
shows "(A^2-4)*(ψ_int A m)^2 + 4 = (χ_int A m)^2"
unfolding ψ_int_def χ_int_def using lucas_pell_part3 by auto
lemma pell_yields_lucas:
fixes A Y :: int
shows "(∃k. (A^2-4)*Y^2 + 4 = k^2) = (∃m. Y = ψ_int A m)"
proof (rule iffI)
assume "∃k. (A⇧2 - 4) * Y⇧2 + 4 = k⇧2"
then obtain m :: nat where m: "Y = ψ A m ∨ Y = - ψ A m"
using lucas_pell_nat(1) by auto
show "∃m :: int. Y = ψ_int A m"
apply (rule disjE[OF m])
subgoal
apply (rule exI[of _ "int m"]) unfolding ψ_int_def by auto
subgoal
apply (rule exI[of _ "- int m"]) unfolding ψ_int_def by auto
done
next
assume "∃m. Y = ψ_int A m"
then obtain m where m: "Y = ψ_int A m" by auto
show "∃k. (A⇧2 - 4) * Y⇧2 + 4 = k⇧2"
unfolding lucas_pell_nat
apply (cases "0 ≤ m")
subgoal
apply (rule exI[of _ "nat m"])
using m unfolding ψ_int_def
by auto
subgoal
apply (rule exI[of _ "nat (- m)"])
using m unfolding ψ_int_def
by auto
done
qed
corollary technical_lemma2_part2:
fixes r::int and A::int and n::int and q::int and k::int
assumes "n ≠ 0" and "χ_int A n = 2*k"
shows "ψ_int A (4*n*q+r) mod k = ψ_int A r mod k"
using technical_lemma2 assms by auto
corollary technical_cor3:
fixes r::int and A::int and n::int and k::int
assumes "n ≠ 0" and "χ_int A n = 2*k"
shows "ψ_int A (2*n+r) mod k = (-ψ_int A r) mod k"
proof -
have "(ψ_int A (2*n+r) + ψ_int A r) mod χ_int A n = 0 mod χ_int A n"
using technical_lemma2[of n A k r] assms mod_add_cong[of "ψ_int A (2*n+r)" "χ_int A n"
"-ψ_int A r" "ψ_int A r" "ψ_int A r"] by (auto simp add: algebra_simps)
hence "χ_int A n dvd (ψ_int A (2*n+r) + ψ_int A r)" by auto
hence "k dvd (ψ_int A (2*n+r) + ψ_int A r)" using assms by auto
hence "(ψ_int A (2*n+r) + ψ_int A r) mod k = 0 mod k" by auto
thus ?thesis using mod_diff_cong[of "ψ_int A (2*n+r) + ψ_int A r" k 0 "ψ_int A r" "ψ_int A r"]
by auto
qed
end