src/HOL/Old_Number_Theory/Primes.thy
 author wenzelm Sun Sep 18 20:33:48 2016 +0200 (2016-09-18) changeset 63915 bab633745c7f parent 63833 4aaeb9427c96 permissions -rw-r--r--
tuned proofs;
 wenzelm@38159 ` 1` ```(* Title: HOL/Old_Number_Theory/Primes.thy ``` haftmann@27106 ` 2` ``` Author: Amine Chaieb, Christophe Tabacznyj and Lawrence C Paulson ``` paulson@11363 ` 3` ``` Copyright 1996 University of Cambridge ``` paulson@11363 ` 4` ```*) ``` paulson@11363 ` 5` wenzelm@61382 ` 6` ```section \Primality on nat\ ``` paulson@11363 ` 7` nipkow@15131 ` 8` ```theory Primes ``` huffman@31706 ` 9` ```imports Complex_Main Legacy_GCD ``` nipkow@15131 ` 10` ```begin ``` paulson@11363 ` 11` wenzelm@38159 ` 12` ```definition coprime :: "nat => nat => bool" ``` wenzelm@38159 ` 13` ``` where "coprime m n \ gcd m n = 1" ``` paulson@11363 ` 14` wenzelm@38159 ` 15` ```definition prime :: "nat \ bool" ``` wenzelm@38159 ` 16` ``` where "prime p \ (1 < p \ (\m. m dvd p --> m = 1 \ m = p))" ``` paulson@11363 ` 17` paulson@11363 ` 18` nipkow@16762 ` 19` ```lemma two_is_prime: "prime 2" ``` nipkow@16762 ` 20` ``` apply (auto simp add: prime_def) ``` nipkow@16762 ` 21` ``` apply (case_tac m) ``` nipkow@16762 ` 22` ``` apply (auto dest!: dvd_imp_le) ``` paulson@11363 ` 23` ``` done ``` paulson@11363 ` 24` haftmann@27556 ` 25` ```lemma prime_imp_relprime: "prime p ==> \ p dvd n ==> gcd p n = 1" ``` paulson@11363 ` 26` ``` apply (auto simp add: prime_def) ``` bulwahn@50037 ` 27` ``` apply (metis gcd_dvd1 gcd_dvd2) ``` paulson@11363 ` 28` ``` done ``` paulson@11363 ` 29` wenzelm@61382 ` 30` ```text \ ``` paulson@11363 ` 31` ``` This theorem leads immediately to a proof of the uniqueness of ``` paulson@11363 ` 32` ``` factorization. If @{term p} divides a product of primes then it is ``` paulson@11363 ` 33` ``` one of those primes. ``` wenzelm@61382 ` 34` ```\ ``` paulson@11363 ` 35` nipkow@16663 ` 36` ```lemma prime_dvd_mult: "prime p ==> p dvd m * n ==> p dvd m \ p dvd n" ``` wenzelm@12739 ` 37` ``` by (blast intro: relprime_dvd_mult prime_imp_relprime) ``` paulson@11363 ` 38` nipkow@16663 ` 39` ```lemma prime_dvd_square: "prime p ==> p dvd m^Suc (Suc 0) ==> p dvd m" ``` wenzelm@12739 ` 40` ``` by (auto dest: prime_dvd_mult) ``` wenzelm@12739 ` 41` wenzelm@53015 ` 42` ```lemma prime_dvd_power_two: "prime p ==> p dvd m\<^sup>2 ==> p dvd m" ``` paulson@14353 ` 43` ``` by (rule prime_dvd_square) (simp_all add: power2_eq_square) ``` wenzelm@11368 ` 44` chaieb@26125 ` 45` nipkow@30056 ` 46` ```lemma exp_eq_1:"(x::nat)^n = 1 \ x = 1 \ n = 0" ``` nipkow@30056 ` 47` ```by (induct n, auto) ``` nipkow@30056 ` 48` chaieb@26125 ` 49` ```lemma exp_mono_lt: "(x::nat) ^ (Suc n) < y ^ (Suc n) \ x < y" ``` nipkow@30056 ` 50` ```by(metis linorder_not_less not_less0 power_le_imp_le_base power_less_imp_less_base) ``` nipkow@30056 ` 51` chaieb@26125 ` 52` ```lemma exp_mono_le: "(x::nat) ^ (Suc n) \ y ^ (Suc n) \ x \ y" ``` nipkow@30056 ` 53` ```by (simp only: linorder_not_less[symmetric] exp_mono_lt) ``` chaieb@26125 ` 54` chaieb@26125 ` 55` ```lemma exp_mono_eq: "(x::nat) ^ Suc n = y ^ Suc n \ x = y" ``` chaieb@26125 ` 56` ```using power_inject_base[of x n y] by auto ``` chaieb@26125 ` 57` chaieb@26125 ` 58` wenzelm@53077 ` 59` ```lemma even_square: assumes e: "even (n::nat)" shows "\x. n\<^sup>2 = 4*x" ``` chaieb@26125 ` 60` ```proof- ``` chaieb@26125 ` 61` ``` from e have "2 dvd n" by presburger ``` chaieb@26125 ` 62` ``` then obtain k where k: "n = 2*k" using dvd_def by auto ``` wenzelm@53077 ` 63` ``` hence "n\<^sup>2 = 4 * k\<^sup>2" by (simp add: power2_eq_square) ``` chaieb@26125 ` 64` ``` thus ?thesis by blast ``` chaieb@26125 ` 65` ```qed ``` chaieb@26125 ` 66` wenzelm@53077 ` 67` ```lemma odd_square: assumes e: "odd (n::nat)" shows "\x. n\<^sup>2 = 4*x + 1" ``` chaieb@26125 ` 68` ```proof- ``` chaieb@26125 ` 69` ``` from e have np: "n > 0" by presburger ``` chaieb@26125 ` 70` ``` from e have "2 dvd (n - 1)" by presburger ``` haftmann@58740 ` 71` ``` then obtain k where "n - 1 = 2 * k" .. ``` chaieb@26125 ` 72` ``` hence k: "n = 2*k + 1" using e by presburger ``` wenzelm@53077 ` 73` ``` hence "n\<^sup>2 = 4* (k\<^sup>2 + k) + 1" by algebra ``` chaieb@26125 ` 74` ``` thus ?thesis by blast ``` chaieb@26125 ` 75` ```qed ``` chaieb@26125 ` 76` wenzelm@53077 ` 77` ```lemma diff_square: "(x::nat)\<^sup>2 - y\<^sup>2 = (x+y)*(x - y)" ``` chaieb@26125 ` 78` ```proof- ``` chaieb@26125 ` 79` ``` have "x \ y \ y \ x" by (rule nat_le_linear) ``` chaieb@26125 ` 80` ``` moreover ``` chaieb@26125 ` 81` ``` {assume le: "x \ y" ``` wenzelm@53077 ` 82` ``` hence "x\<^sup>2 \ y\<^sup>2" by (simp only: numeral_2_eq_2 exp_mono_le Let_def) ``` chaieb@26125 ` 83` ``` with le have ?thesis by simp } ``` chaieb@26125 ` 84` ``` moreover ``` chaieb@26125 ` 85` ``` {assume le: "y \ x" ``` wenzelm@53077 ` 86` ``` hence le2: "y\<^sup>2 \ x\<^sup>2" by (simp only: numeral_2_eq_2 exp_mono_le Let_def) ``` chaieb@26125 ` 87` ``` from le have "\z. y + z = x" by presburger ``` chaieb@26125 ` 88` ``` then obtain z where z: "x = y + z" by blast ``` wenzelm@53077 ` 89` ``` from le2 have "\z. x\<^sup>2 = y\<^sup>2 + z" by presburger ``` wenzelm@53077 ` 90` ``` then obtain z2 where z2: "x\<^sup>2 = y\<^sup>2 + z2" by blast ``` wenzelm@53077 ` 91` ``` from z z2 have ?thesis by simp algebra } ``` chaieb@26125 ` 92` ``` ultimately show ?thesis by blast ``` chaieb@26125 ` 93` ```qed ``` chaieb@26125 ` 94` wenzelm@61382 ` 95` ```text \Elementary theory of divisibility\ ``` chaieb@26125 ` 96` ```lemma divides_ge: "(a::nat) dvd b \ b = 0 \ a \ b" unfolding dvd_def by auto ``` chaieb@26125 ` 97` ```lemma divides_antisym: "(x::nat) dvd y \ y dvd x \ x = y" ``` nipkow@33657 ` 98` ``` using dvd_antisym[of x y] by auto ``` chaieb@26125 ` 99` chaieb@26125 ` 100` ```lemma divides_add_revr: assumes da: "(d::nat) dvd a" and dab:"d dvd (a + b)" ``` chaieb@26125 ` 101` ``` shows "d dvd b" ``` chaieb@26125 ` 102` ```proof- ``` chaieb@26125 ` 103` ``` from da obtain k where k:"a = d*k" by (auto simp add: dvd_def) ``` chaieb@26125 ` 104` ``` from dab obtain k' where k': "a + b = d*k'" by (auto simp add: dvd_def) ``` chaieb@26125 ` 105` ``` from k k' have "b = d *(k' - k)" by (simp add : diff_mult_distrib2) ``` chaieb@26125 ` 106` ``` thus ?thesis unfolding dvd_def by blast ``` chaieb@26125 ` 107` ```qed ``` chaieb@26125 ` 108` chaieb@26125 ` 109` ```declare nat_mult_dvd_cancel_disj[presburger] ``` chaieb@26125 ` 110` ```lemma nat_mult_dvd_cancel_disj'[presburger]: ``` wenzelm@61076 ` 111` ``` "(m::nat)*k dvd n*k \ k = 0 \ m dvd n" unfolding mult.commute[of m k] mult.commute[of n k] by presburger ``` chaieb@26125 ` 112` chaieb@26125 ` 113` ```lemma divides_mul_l: "(a::nat) dvd b ==> (c * a) dvd (c * b)" ``` chaieb@26125 ` 114` ``` by presburger ``` chaieb@26125 ` 115` chaieb@26125 ` 116` ```lemma divides_mul_r: "(a::nat) dvd b ==> (a * c) dvd (b * c)" by presburger ``` chaieb@26125 ` 117` ```lemma divides_cases: "(n::nat) dvd m ==> m = 0 \ m = n \ 2 * n <= m" ``` chaieb@26125 ` 118` ``` by (auto simp add: dvd_def) ``` chaieb@26125 ` 119` chaieb@26125 ` 120` ```lemma divides_div_not: "(x::nat) = (q * n) + r \ 0 < r \ r < n ==> ~(n dvd x)" ``` chaieb@26125 ` 121` ```proof(auto simp add: dvd_def) ``` chaieb@26125 ` 122` ``` fix k assume H: "0 < r" "r < n" "q * n + r = n * k" ``` haftmann@57512 ` 123` ``` from H(3) have r: "r = n* (k -q)" by(simp add: diff_mult_distrib2 mult.commute) ``` chaieb@26125 ` 124` ``` {assume "k - q = 0" with r H(1) have False by simp} ``` chaieb@26125 ` 125` ``` moreover ``` chaieb@26125 ` 126` ``` {assume "k - q \ 0" with r have "r \ n" by auto ``` chaieb@26125 ` 127` ``` with H(2) have False by simp} ``` chaieb@26125 ` 128` ``` ultimately show False by blast ``` chaieb@26125 ` 129` ```qed ``` chaieb@26125 ` 130` ```lemma divides_exp: "(x::nat) dvd y ==> x ^ n dvd y ^ n" ``` chaieb@26125 ` 131` ``` by (auto simp add: power_mult_distrib dvd_def) ``` chaieb@26125 ` 132` chaieb@26125 ` 133` ```lemma divides_exp2: "n \ 0 \ (x::nat) ^ n dvd y \ x dvd y" ``` chaieb@26125 ` 134` ``` by (induct n ,auto simp add: dvd_def) ``` chaieb@26125 ` 135` chaieb@26125 ` 136` ```fun fact :: "nat \ nat" where ``` chaieb@26125 ` 137` ``` "fact 0 = 1" ``` wenzelm@32960 ` 138` ```| "fact (Suc n) = Suc n * fact n" ``` chaieb@26125 ` 139` chaieb@26125 ` 140` ```lemma fact_lt: "0 < fact n" by(induct n, simp_all) ``` chaieb@26125 ` 141` ```lemma fact_le: "fact n \ 1" using fact_lt[of n] by simp ``` chaieb@26125 ` 142` ```lemma fact_mono: assumes le: "m \ n" shows "fact m \ fact n" ``` chaieb@26125 ` 143` ```proof- ``` chaieb@26125 ` 144` ``` from le have "\i. n = m+i" by presburger ``` chaieb@26125 ` 145` ``` then obtain i where i: "n = m+i" by blast ``` chaieb@26125 ` 146` ``` have "fact m \ fact (m + i)" ``` chaieb@26125 ` 147` ``` proof(induct m) ``` chaieb@26125 ` 148` ``` case 0 thus ?case using fact_le[of i] by simp ``` chaieb@26125 ` 149` ``` next ``` chaieb@26125 ` 150` ``` case (Suc m) ``` chaieb@26125 ` 151` ``` have "fact (Suc m) = Suc m * fact m" by simp ``` chaieb@26125 ` 152` ``` have th1: "Suc m \ Suc (m + i)" by simp ``` chaieb@26125 ` 153` ``` from mult_le_mono[of "Suc m" "Suc (m+i)" "fact m" "fact (m+i)", OF th1 Suc.hyps] ``` chaieb@26125 ` 154` ``` show ?case by simp ``` chaieb@26125 ` 155` ``` qed ``` chaieb@26125 ` 156` ``` thus ?thesis using i by simp ``` chaieb@26125 ` 157` ```qed ``` chaieb@26125 ` 158` chaieb@26125 ` 159` ```lemma divides_fact: "1 <= p \ p <= n ==> p dvd fact n" ``` chaieb@26125 ` 160` ```proof(induct n arbitrary: p) ``` chaieb@26125 ` 161` ``` case 0 thus ?case by simp ``` chaieb@26125 ` 162` ```next ``` chaieb@26125 ` 163` ``` case (Suc n p) ``` chaieb@26125 ` 164` ``` from Suc.prems have "p = Suc n \ p \ n" by presburger ``` chaieb@26125 ` 165` ``` moreover ``` chaieb@26125 ` 166` ``` {assume "p = Suc n" hence ?case by (simp only: fact.simps dvd_triv_left)} ``` chaieb@26125 ` 167` ``` moreover ``` chaieb@26125 ` 168` ``` {assume "p \ n" ``` chaieb@26125 ` 169` ``` with Suc.prems(1) Suc.hyps have th: "p dvd fact n" by simp ``` chaieb@26125 ` 170` ``` from dvd_mult[OF th] have ?case by (simp only: fact.simps) } ``` chaieb@26125 ` 171` ``` ultimately show ?case by blast ``` chaieb@26125 ` 172` ```qed ``` chaieb@26125 ` 173` chaieb@26125 ` 174` ```declare dvd_triv_left[presburger] ``` chaieb@26125 ` 175` ```declare dvd_triv_right[presburger] ``` chaieb@26125 ` 176` ```lemma divides_rexp: ``` chaieb@26125 ` 177` ``` "x dvd y \ (x::nat) dvd (y^(Suc n))" by (simp add: dvd_mult2[of x y]) ``` chaieb@26125 ` 178` wenzelm@61382 ` 179` ```text \Coprimality\ ``` chaieb@26125 ` 180` chaieb@26125 ` 181` ```lemma coprime: "coprime a b \ (\d. d dvd a \ d dvd b \ d = 1)" ``` chaieb@26125 ` 182` ```using gcd_unique[of 1 a b, simplified] by (auto simp add: coprime_def) ``` chaieb@26125 ` 183` ```lemma coprime_commute: "coprime a b \ coprime b a" by (simp add: coprime_def gcd_commute) ``` chaieb@26125 ` 184` chaieb@26125 ` 185` ```lemma coprime_bezout: "coprime a b \ (\x y. a * x - b * y = 1 \ b * x - a * y = 1)" ``` chaieb@26125 ` 186` ```using coprime_def gcd_bezout by auto ``` chaieb@26125 ` 187` chaieb@26125 ` 188` ```lemma coprime_divprod: "d dvd a * b \ coprime d a \ d dvd b" ``` haftmann@57512 ` 189` ``` using relprime_dvd_mult_iff[of d a b] by (auto simp add: coprime_def mult.commute) ``` chaieb@26125 ` 190` chaieb@26125 ` 191` ```lemma coprime_1[simp]: "coprime a 1" by (simp add: coprime_def) ``` chaieb@26125 ` 192` ```lemma coprime_1'[simp]: "coprime 1 a" by (simp add: coprime_def) ``` chaieb@26125 ` 193` ```lemma coprime_Suc0[simp]: "coprime a (Suc 0)" by (simp add: coprime_def) ``` chaieb@26125 ` 194` ```lemma coprime_Suc0'[simp]: "coprime (Suc 0) a" by (simp add: coprime_def) ``` chaieb@26125 ` 195` chaieb@26125 ` 196` ```lemma gcd_coprime: ``` haftmann@27556 ` 197` ``` assumes z: "gcd a b \ 0" and a: "a = a' * gcd a b" and b: "b = b' * gcd a b" ``` chaieb@26125 ` 198` ``` shows "coprime a' b'" ``` chaieb@26125 ` 199` ```proof- ``` haftmann@27556 ` 200` ``` let ?g = "gcd a b" ``` chaieb@26125 ` 201` ``` {assume bz: "a = 0" from b bz z a have ?thesis by (simp add: gcd_zero coprime_def)} ``` chaieb@26125 ` 202` ``` moreover ``` chaieb@26125 ` 203` ``` {assume az: "a\ 0" ``` chaieb@26125 ` 204` ``` from z have z': "?g > 0" by simp ``` chaieb@26125 ` 205` ``` from bezout_gcd_strong[OF az, of b] ``` chaieb@26125 ` 206` ``` obtain x y where xy: "a*x = b*y + ?g" by blast ``` nipkow@29667 ` 207` ``` from xy a b have "?g * a'*x = ?g * (b'*y + 1)" by (simp add: algebra_simps) ``` haftmann@57512 ` 208` ``` hence "?g * (a'*x) = ?g * (b'*y + 1)" by (simp add: mult.assoc) ``` chaieb@26125 ` 209` ``` hence "a'*x = (b'*y + 1)" ``` chaieb@26125 ` 210` ``` by (simp only: nat_mult_eq_cancel1[OF z']) ``` chaieb@26125 ` 211` ``` hence "a'*x - b'*y = 1" by simp ``` chaieb@26125 ` 212` ``` with coprime_bezout[of a' b'] have ?thesis by auto} ``` chaieb@26125 ` 213` ``` ultimately show ?thesis by blast ``` chaieb@26125 ` 214` ```qed ``` chaieb@26125 ` 215` ```lemma coprime_0: "coprime d 0 \ d = 1" by (simp add: coprime_def) ``` chaieb@26125 ` 216` ```lemma coprime_mul: assumes da: "coprime d a" and db: "coprime d b" ``` chaieb@26125 ` 217` ``` shows "coprime d (a * b)" ``` chaieb@26125 ` 218` ```proof- ``` haftmann@27556 ` 219` ``` from da have th: "gcd a d = 1" by (simp add: coprime_def gcd_commute) ``` chaieb@27567 ` 220` ``` from gcd_mult_cancel[of a d b, OF th] db[unfolded coprime_def] have "gcd d (a*b) = 1" ``` chaieb@26125 ` 221` ``` by (simp add: gcd_commute) ``` chaieb@26125 ` 222` ``` thus ?thesis unfolding coprime_def . ``` chaieb@26125 ` 223` ```qed ``` chaieb@26125 ` 224` ```lemma coprime_lmul2: assumes dab: "coprime d (a * b)" shows "coprime d b" ``` wenzelm@41541 ` 225` ```using dab unfolding coprime_bezout ``` chaieb@26125 ` 226` ```apply clarsimp ``` chaieb@26125 ` 227` ```apply (case_tac "d * x - a * b * y = Suc 0 ", simp_all) ``` chaieb@26125 ` 228` ```apply (rule_tac x="x" in exI) ``` chaieb@26125 ` 229` ```apply (rule_tac x="a*y" in exI) ``` haftmann@57514 ` 230` ```apply (simp add: ac_simps) ``` chaieb@26125 ` 231` ```apply (rule_tac x="a*x" in exI) ``` chaieb@26125 ` 232` ```apply (rule_tac x="y" in exI) ``` haftmann@57514 ` 233` ```apply (simp add: ac_simps) ``` chaieb@26125 ` 234` ```done ``` chaieb@26125 ` 235` chaieb@26125 ` 236` ```lemma coprime_rmul2: "coprime d (a * b) \ coprime d a" ``` chaieb@26125 ` 237` ```unfolding coprime_bezout ``` chaieb@26125 ` 238` ```apply clarsimp ``` chaieb@26125 ` 239` ```apply (case_tac "d * x - a * b * y = Suc 0 ", simp_all) ``` chaieb@26125 ` 240` ```apply (rule_tac x="x" in exI) ``` chaieb@26125 ` 241` ```apply (rule_tac x="b*y" in exI) ``` haftmann@57514 ` 242` ```apply (simp add: ac_simps) ``` chaieb@26125 ` 243` ```apply (rule_tac x="b*x" in exI) ``` chaieb@26125 ` 244` ```apply (rule_tac x="y" in exI) ``` haftmann@57514 ` 245` ```apply (simp add: ac_simps) ``` chaieb@26125 ` 246` ```done ``` chaieb@26125 ` 247` ```lemma coprime_mul_eq: "coprime d (a * b) \ coprime d a \ coprime d b" ``` chaieb@26125 ` 248` ``` using coprime_rmul2[of d a b] coprime_lmul2[of d a b] coprime_mul[of d a b] ``` chaieb@26125 ` 249` ``` by blast ``` chaieb@26125 ` 250` chaieb@26125 ` 251` ```lemma gcd_coprime_exists: ``` haftmann@27556 ` 252` ``` assumes nz: "gcd a b \ 0" ``` haftmann@27556 ` 253` ``` shows "\a' b'. a = a' * gcd a b \ b = b' * gcd a b \ coprime a' b'" ``` chaieb@26125 ` 254` ```proof- ``` haftmann@27556 ` 255` ``` let ?g = "gcd a b" ``` chaieb@26125 ` 256` ``` from gcd_dvd1[of a b] gcd_dvd2[of a b] ``` chaieb@26125 ` 257` ``` obtain a' b' where "a = ?g*a'" "b = ?g*b'" unfolding dvd_def by blast ``` chaieb@26125 ` 258` ``` hence ab': "a = a'*?g" "b = b'*?g" by algebra+ ``` chaieb@26125 ` 259` ``` from ab' gcd_coprime[OF nz ab'] show ?thesis by blast ``` chaieb@26125 ` 260` ```qed ``` chaieb@26125 ` 261` chaieb@26125 ` 262` ```lemma coprime_exp: "coprime d a ==> coprime d (a^n)" ``` chaieb@26125 ` 263` ``` by(induct n, simp_all add: coprime_mul) ``` chaieb@26125 ` 264` chaieb@26125 ` 265` ```lemma coprime_exp_imp: "coprime a b ==> coprime (a ^n) (b ^n)" ``` chaieb@26125 ` 266` ``` by (induct n, simp_all add: coprime_mul_eq coprime_commute coprime_exp) ``` chaieb@26125 ` 267` ```lemma coprime_refl[simp]: "coprime n n \ n = 1" by (simp add: coprime_def) ``` chaieb@26125 ` 268` ```lemma coprime_plus1[simp]: "coprime (n + 1) n" ``` chaieb@26125 ` 269` ``` apply (simp add: coprime_bezout) ``` chaieb@26125 ` 270` ``` apply (rule exI[where x=1]) ``` chaieb@26125 ` 271` ``` apply (rule exI[where x=1]) ``` chaieb@26125 ` 272` ``` apply simp ``` chaieb@26125 ` 273` ``` done ``` chaieb@26125 ` 274` ```lemma coprime_minus1: "n \ 0 ==> coprime (n - 1) n" ``` chaieb@26125 ` 275` ``` using coprime_plus1[of "n - 1"] coprime_commute[of "n - 1" n] by auto ``` chaieb@26125 ` 276` haftmann@27556 ` 277` ```lemma bezout_gcd_pow: "\x y. a ^n * x - b ^ n * y = gcd a b ^ n \ b ^ n * x - a ^ n * y = gcd a b ^ n" ``` chaieb@26125 ` 278` ```proof- ``` haftmann@27556 ` 279` ``` let ?g = "gcd a b" ``` chaieb@26125 ` 280` ``` {assume z: "?g = 0" hence ?thesis ``` chaieb@26125 ` 281` ``` apply (cases n, simp) ``` chaieb@26125 ` 282` ``` apply arith ``` chaieb@26125 ` 283` ``` apply (simp only: z power_0_Suc) ``` chaieb@26125 ` 284` ``` apply (rule exI[where x=0]) ``` chaieb@26125 ` 285` ``` apply (rule exI[where x=0]) ``` wenzelm@41541 ` 286` ``` apply simp ``` wenzelm@41541 ` 287` ``` done } ``` chaieb@26125 ` 288` ``` moreover ``` chaieb@26125 ` 289` ``` {assume z: "?g \ 0" ``` chaieb@26125 ` 290` ``` from gcd_dvd1[of a b] gcd_dvd2[of a b] obtain a' b' where ``` haftmann@57514 ` 291` ``` ab': "a = a'*?g" "b = b'*?g" unfolding dvd_def by (auto simp add: ac_simps) ``` chaieb@26125 ` 292` ``` hence ab'': "?g*a' = a" "?g * b' = b" by algebra+ ``` chaieb@26125 ` 293` ``` from coprime_exp_imp[OF gcd_coprime[OF z ab'], unfolded coprime_bezout, of n] ``` chaieb@26125 ` 294` ``` obtain x y where "a'^n * x - b'^n * y = 1 \ b'^n * x - a'^n * y = 1" by blast ``` chaieb@26125 ` 295` ``` hence "?g^n * (a'^n * x - b'^n * y) = ?g^n \ ?g^n*(b'^n * x - a'^n * y) = ?g^n" ``` chaieb@26125 ` 296` ``` using z by auto ``` chaieb@26125 ` 297` ``` then have "a^n * x - b^n * y = ?g^n \ b^n * x - a^n * y = ?g^n" ``` chaieb@26125 ` 298` ``` using z ab'' by (simp only: power_mult_distrib[symmetric] ``` haftmann@57512 ` 299` ``` diff_mult_distrib2 mult.assoc[symmetric]) ``` chaieb@26125 ` 300` ``` hence ?thesis by blast } ``` chaieb@26125 ` 301` ``` ultimately show ?thesis by blast ``` chaieb@26125 ` 302` ```qed ``` chaieb@27567 ` 303` chaieb@27567 ` 304` ```lemma gcd_exp: "gcd (a^n) (b^n) = gcd a b^n" ``` chaieb@26125 ` 305` ```proof- ``` haftmann@27556 ` 306` ``` let ?g = "gcd (a^n) (b^n)" ``` chaieb@27567 ` 307` ``` let ?gn = "gcd a b^n" ``` chaieb@26125 ` 308` ``` {fix e assume H: "e dvd a^n" "e dvd b^n" ``` chaieb@26125 ` 309` ``` from bezout_gcd_pow[of a n b] obtain x y ``` chaieb@26125 ` 310` ``` where xy: "a ^ n * x - b ^ n * y = ?gn \ b ^ n * x - a ^ n * y = ?gn" by blast ``` nipkow@31952 ` 311` ``` from dvd_diff_nat [OF dvd_mult2[OF H(1), of x] dvd_mult2[OF H(2), of y]] ``` nipkow@31952 ` 312` ``` dvd_diff_nat [OF dvd_mult2[OF H(2), of x] dvd_mult2[OF H(1), of y]] xy ``` haftmann@27556 ` 313` ``` have "e dvd ?gn" by (cases "a ^ n * x - b ^ n * y = gcd a b ^ n", simp_all)} ``` chaieb@26125 ` 314` ``` hence th: "\e. e dvd a^n \ e dvd b^n \ e dvd ?gn" by blast ``` chaieb@26125 ` 315` ``` from divides_exp[OF gcd_dvd1[of a b], of n] divides_exp[OF gcd_dvd2[of a b], of n] th ``` chaieb@26125 ` 316` ``` gcd_unique have "?gn = ?g" by blast thus ?thesis by simp ``` chaieb@26125 ` 317` ```qed ``` chaieb@26125 ` 318` chaieb@26125 ` 319` ```lemma coprime_exp2: "coprime (a ^ Suc n) (b^ Suc n) \ coprime a b" ``` chaieb@26125 ` 320` ```by (simp only: coprime_def gcd_exp exp_eq_1) simp ``` chaieb@26125 ` 321` chaieb@26125 ` 322` ```lemma division_decomp: assumes dc: "(a::nat) dvd b * c" ``` chaieb@26125 ` 323` ``` shows "\b' c'. a = b' * c' \ b' dvd b \ c' dvd c" ``` chaieb@26125 ` 324` ```proof- ``` haftmann@27556 ` 325` ``` let ?g = "gcd a b" ``` chaieb@26125 ` 326` ``` {assume "?g = 0" with dc have ?thesis apply (simp add: gcd_zero) ``` chaieb@26125 ` 327` ``` apply (rule exI[where x="0"]) ``` chaieb@26125 ` 328` ``` by (rule exI[where x="c"], simp)} ``` chaieb@26125 ` 329` ``` moreover ``` chaieb@26125 ` 330` ``` {assume z: "?g \ 0" ``` chaieb@26125 ` 331` ``` from gcd_coprime_exists[OF z] ``` chaieb@26125 ` 332` ``` obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'" by blast ``` chaieb@26125 ` 333` ``` from gcd_dvd2[of a b] have thb: "?g dvd b" . ``` chaieb@26125 ` 334` ``` from ab'(1) have "a' dvd a" unfolding dvd_def by blast ``` chaieb@26125 ` 335` ``` with dc have th0: "a' dvd b*c" using dvd_trans[of a' a "b*c"] by simp ``` chaieb@26125 ` 336` ``` from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto ``` haftmann@57512 ` 337` ``` hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult.assoc) ``` chaieb@26125 ` 338` ``` with z have th_1: "a' dvd b'*c" by simp ``` chaieb@26125 ` 339` ``` from coprime_divprod[OF th_1 ab'(3)] have thc: "a' dvd c" . ``` chaieb@26125 ` 340` ``` from ab' have "a = ?g*a'" by algebra ``` chaieb@26125 ` 341` ``` with thb thc have ?thesis by blast } ``` chaieb@26125 ` 342` ``` ultimately show ?thesis by blast ``` chaieb@26125 ` 343` ```qed ``` chaieb@26125 ` 344` chaieb@26125 ` 345` ```lemma nat_power_eq_0_iff: "(m::nat) ^ n = 0 \ n \ 0 \ m = 0" by (induct n, auto) ``` chaieb@26125 ` 346` chaieb@26125 ` 347` ```lemma divides_rev: assumes ab: "(a::nat) ^ n dvd b ^n" and n:"n \ 0" shows "a dvd b" ``` chaieb@26125 ` 348` ```proof- ``` haftmann@27556 ` 349` ``` let ?g = "gcd a b" ``` chaieb@26125 ` 350` ``` from n obtain m where m: "n = Suc m" by (cases n, simp_all) ``` chaieb@26125 ` 351` ``` {assume "?g = 0" with ab n have ?thesis by (simp add: gcd_zero)} ``` chaieb@26125 ` 352` ``` moreover ``` chaieb@26125 ` 353` ``` {assume z: "?g \ 0" ``` wenzelm@41541 ` 354` ``` hence zn: "?g ^ n \ 0" using n by simp ``` chaieb@26125 ` 355` ``` from gcd_coprime_exists[OF z] ``` chaieb@26125 ` 356` ``` obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'" by blast ``` chaieb@26125 ` 357` ``` from ab have "(a' * ?g) ^ n dvd (b' * ?g)^n" by (simp add: ab'(1,2)[symmetric]) ``` haftmann@57512 ` 358` ``` hence "?g^n*a'^n dvd ?g^n *b'^n" by (simp only: power_mult_distrib mult.commute) ``` chaieb@26125 ` 359` ``` with zn z n have th0:"a'^n dvd b'^n" by (auto simp add: nat_power_eq_0_iff) ``` chaieb@26125 ` 360` ``` have "a' dvd a'^n" by (simp add: m) ``` chaieb@26125 ` 361` ``` with th0 have "a' dvd b'^n" using dvd_trans[of a' "a'^n" "b'^n"] by simp ``` haftmann@57512 ` 362` ``` hence th1: "a' dvd b'^m * b'" by (simp add: m mult.commute) ``` chaieb@26125 ` 363` ``` from coprime_divprod[OF th1 coprime_exp[OF ab'(3), of m]] ``` chaieb@26125 ` 364` ``` have "a' dvd b'" . ``` chaieb@26125 ` 365` ``` hence "a'*?g dvd b'*?g" by simp ``` chaieb@26125 ` 366` ``` with ab'(1,2) have ?thesis by simp } ``` chaieb@26125 ` 367` ``` ultimately show ?thesis by blast ``` chaieb@26125 ` 368` ```qed ``` chaieb@26125 ` 369` chaieb@26125 ` 370` ```lemma divides_mul: assumes mr: "m dvd r" and nr: "n dvd r" and mn:"coprime m n" ``` chaieb@26125 ` 371` ``` shows "m * n dvd r" ``` chaieb@26125 ` 372` ```proof- ``` chaieb@26125 ` 373` ``` from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'" ``` chaieb@26125 ` 374` ``` unfolding dvd_def by blast ``` haftmann@57512 ` 375` ``` from mr n' have "m dvd n'*n" by (simp add: mult.commute) ``` chaieb@26125 ` 376` ``` hence "m dvd n'" using relprime_dvd_mult_iff[OF mn[unfolded coprime_def]] by simp ``` chaieb@26125 ` 377` ``` then obtain k where k: "n' = m*k" unfolding dvd_def by blast ``` chaieb@26125 ` 378` ``` from n' k show ?thesis unfolding dvd_def by auto ``` chaieb@26125 ` 379` ```qed ``` chaieb@26125 ` 380` wenzelm@26144 ` 381` wenzelm@61382 ` 382` ```text \A binary form of the Chinese Remainder Theorem.\ ``` chaieb@26125 ` 383` chaieb@26125 ` 384` ```lemma chinese_remainder: assumes ab: "coprime a b" and a:"a \ 0" and b:"b \ 0" ``` chaieb@26125 ` 385` ``` shows "\x q1 q2. x = u + q1 * a \ x = v + q2 * b" ``` chaieb@26125 ` 386` ```proof- ``` chaieb@26125 ` 387` ``` from bezout_add_strong[OF a, of b] bezout_add_strong[OF b, of a] ``` chaieb@26125 ` 388` ``` obtain d1 x1 y1 d2 x2 y2 where dxy1: "d1 dvd a" "d1 dvd b" "a * x1 = b * y1 + d1" ``` chaieb@26125 ` 389` ``` and dxy2: "d2 dvd b" "d2 dvd a" "b * x2 = a * y2 + d2" by blast ``` chaieb@26125 ` 390` ``` from gcd_unique[of 1 a b, simplified ab[unfolded coprime_def], simplified] ``` chaieb@26125 ` 391` ``` dxy1(1,2) dxy2(1,2) have d12: "d1 = 1" "d2 =1" by auto ``` chaieb@26125 ` 392` ``` let ?x = "v * a * x1 + u * b * x2" ``` chaieb@26125 ` 393` ``` let ?q1 = "v * x1 + u * y2" ``` chaieb@26125 ` 394` ``` let ?q2 = "v * y1 + u * x2" ``` chaieb@26125 ` 395` ``` from dxy2(3)[simplified d12] dxy1(3)[simplified d12] ``` chaieb@26125 ` 396` ``` have "?x = u + ?q1 * a" "?x = v + ?q2 * b" by algebra+ ``` chaieb@26125 ` 397` ``` thus ?thesis by blast ``` chaieb@26125 ` 398` ```qed ``` chaieb@26125 ` 399` wenzelm@61382 ` 400` ```text \Primality\ ``` wenzelm@26144 ` 401` wenzelm@61382 ` 402` ```text \A few useful theorems about primes\ ``` chaieb@26125 ` 403` chaieb@26125 ` 404` ```lemma prime_0[simp]: "~prime 0" by (simp add: prime_def) ``` chaieb@26125 ` 405` ```lemma prime_1[simp]: "~ prime 1" by (simp add: prime_def) ``` chaieb@26125 ` 406` ```lemma prime_Suc0[simp]: "~ prime (Suc 0)" by (simp add: prime_def) ``` chaieb@26125 ` 407` chaieb@26125 ` 408` ```lemma prime_ge_2: "prime p ==> p \ 2" by (simp add: prime_def) ``` wenzelm@63833 ` 409` wenzelm@63833 ` 410` ```lemma prime_factor: "n \ 1 \ \p. prime p \ p dvd n" ``` wenzelm@63833 ` 411` ```proof (induct n rule: nat_less_induct) ``` chaieb@26125 ` 412` ``` fix n ``` chaieb@26125 ` 413` ``` assume H: "\m 1 \ (\p. prime p \ p dvd m)" "n \ 1" ``` wenzelm@63833 ` 414` ``` show "\p. prime p \ p dvd n" ``` wenzelm@63833 ` 415` ``` proof (cases "n = 0") ``` wenzelm@63833 ` 416` ``` case True ``` wenzelm@63833 ` 417` ``` with two_is_prime show ?thesis by auto ``` wenzelm@63833 ` 418` ``` next ``` wenzelm@63833 ` 419` ``` case nz: False ``` wenzelm@63833 ` 420` ``` show ?thesis ``` wenzelm@63833 ` 421` ``` proof (cases "prime n") ``` wenzelm@63833 ` 422` ``` case True ``` wenzelm@63833 ` 423` ``` then have "prime n \ n dvd n" by simp ``` wenzelm@63833 ` 424` ``` then show ?thesis .. ``` wenzelm@63833 ` 425` ``` next ``` wenzelm@63833 ` 426` ``` case n: False ``` wenzelm@63833 ` 427` ``` with nz H(2) obtain k where k: "k dvd n" "k \ 1" "k \ n" ``` wenzelm@63833 ` 428` ``` by (auto simp: prime_def) ``` chaieb@26125 ` 429` ``` from dvd_imp_le[OF k(1)] nz k(3) have kn: "k < n" by simp ``` chaieb@26125 ` 430` ``` from H(1)[rule_format, OF kn k(2)] obtain p where p: "prime p" "p dvd k" by blast ``` wenzelm@63833 ` 431` ``` from dvd_trans[OF p(2) k(1)] p(1) show ?thesis by blast ``` wenzelm@63833 ` 432` ``` qed ``` wenzelm@63833 ` 433` ``` qed ``` chaieb@26125 ` 434` ```qed ``` chaieb@26125 ` 435` wenzelm@63833 ` 436` ```lemma prime_factor_lt: ``` wenzelm@63833 ` 437` ``` assumes p: "prime p" and n: "n \ 0" and npm:"n = p * m" ``` chaieb@26125 ` 438` ``` shows "m < n" ``` wenzelm@63833 ` 439` ```proof (cases "m = 0") ``` wenzelm@63833 ` 440` ``` case True ``` wenzelm@63833 ` 441` ``` with n show ?thesis by simp ``` wenzelm@63833 ` 442` ```next ``` wenzelm@63833 ` 443` ``` case m: False ``` wenzelm@63833 ` 444` ``` from npm have mn: "m dvd n" unfolding dvd_def by auto ``` wenzelm@63833 ` 445` ``` from npm m have "n \ m" using p by auto ``` wenzelm@63833 ` 446` ``` with dvd_imp_le[OF mn] n show ?thesis by simp ``` chaieb@26125 ` 447` ```qed ``` chaieb@26125 ` 448` chaieb@26125 ` 449` ```lemma euclid_bound: "\p. prime p \ n < p \ p <= Suc (fact n)" ``` chaieb@26125 ` 450` ```proof- ``` chaieb@26125 ` 451` ``` have f1: "fact n + 1 \ 1" using fact_le[of n] by arith ``` chaieb@26125 ` 452` ``` from prime_factor[OF f1] obtain p where p: "prime p" "p dvd fact n + 1" by blast ``` chaieb@26125 ` 453` ``` from dvd_imp_le[OF p(2)] have pfn: "p \ fact n + 1" by simp ``` chaieb@26125 ` 454` ``` {assume np: "p \ n" ``` chaieb@26125 ` 455` ``` from p(1) have p1: "p \ 1" by (cases p, simp_all) ``` chaieb@26125 ` 456` ``` from divides_fact[OF p1 np] have pfn': "p dvd fact n" . ``` chaieb@26125 ` 457` ``` from divides_add_revr[OF pfn' p(2)] p(1) have False by simp} ``` chaieb@26125 ` 458` ``` hence "n < p" by arith ``` chaieb@26125 ` 459` ``` with p(1) pfn show ?thesis by auto ``` chaieb@26125 ` 460` ```qed ``` chaieb@26125 ` 461` chaieb@26125 ` 462` ```lemma euclid: "\p. prime p \ p > n" using euclid_bound by auto ``` nipkow@31044 ` 463` chaieb@26125 ` 464` ```lemma primes_infinite: "\ (finite {p. prime p})" ``` nipkow@31044 ` 465` ```apply(simp add: finite_nat_set_iff_bounded_le) ``` nipkow@31044 ` 466` ```apply (metis euclid linorder_not_le) ``` nipkow@31044 ` 467` ```done ``` chaieb@26125 ` 468` chaieb@26125 ` 469` ```lemma coprime_prime: assumes ab: "coprime a b" ``` chaieb@26125 ` 470` ``` shows "~(prime p \ p dvd a \ p dvd b)" ``` chaieb@26125 ` 471` ```proof ``` chaieb@26125 ` 472` ``` assume "prime p \ p dvd a \ p dvd b" ``` chaieb@26125 ` 473` ``` thus False using ab gcd_greatest[of p a b] by (simp add: coprime_def) ``` chaieb@26125 ` 474` ```qed ``` chaieb@26125 ` 475` ```lemma coprime_prime_eq: "coprime a b \ (\p. ~(prime p \ p dvd a \ p dvd b))" ``` chaieb@26125 ` 476` ``` (is "?lhs = ?rhs") ``` chaieb@26125 ` 477` ```proof- ``` chaieb@26125 ` 478` ``` {assume "?lhs" with coprime_prime have ?rhs by blast} ``` chaieb@26125 ` 479` ``` moreover ``` chaieb@26125 ` 480` ``` {assume r: "?rhs" and c: "\ ?lhs" ``` chaieb@26125 ` 481` ``` then obtain g where g: "g\1" "g dvd a" "g dvd b" unfolding coprime_def by blast ``` chaieb@26125 ` 482` ``` from prime_factor[OF g(1)] obtain p where p: "prime p" "p dvd g" by blast ``` chaieb@26125 ` 483` ``` from dvd_trans [OF p(2) g(2)] dvd_trans [OF p(2) g(3)] ``` chaieb@26125 ` 484` ``` have "p dvd a" "p dvd b" . with p(1) r have False by blast} ``` chaieb@26125 ` 485` ``` ultimately show ?thesis by blast ``` chaieb@26125 ` 486` ```qed ``` chaieb@26125 ` 487` chaieb@26125 ` 488` ```lemma prime_coprime: assumes p: "prime p" ``` chaieb@26125 ` 489` ``` shows "n = 1 \ p dvd n \ coprime p n" ``` chaieb@26125 ` 490` ```using p prime_imp_relprime[of p n] by (auto simp add: coprime_def) ``` chaieb@26125 ` 491` chaieb@26125 ` 492` ```lemma prime_coprime_strong: "prime p \ p dvd n \ coprime p n" ``` chaieb@26125 ` 493` ``` using prime_coprime[of p n] by auto ``` chaieb@26125 ` 494` chaieb@26125 ` 495` ```declare coprime_0[simp] ``` chaieb@26125 ` 496` chaieb@26125 ` 497` ```lemma coprime_0'[simp]: "coprime 0 d \ d = 1" by (simp add: coprime_commute[of 0 d]) ``` chaieb@26125 ` 498` ```lemma coprime_bezout_strong: assumes ab: "coprime a b" and b: "b \ 1" ``` chaieb@26125 ` 499` ``` shows "\x y. a * x = b * y + 1" ``` chaieb@26125 ` 500` ```proof- ``` wenzelm@63833 ` 501` ``` have az: "a \ 0" by (rule ccontr) (use ab b in auto) ``` chaieb@26125 ` 502` ``` from bezout_gcd_strong[OF az, of b] ab[unfolded coprime_def] ``` chaieb@26125 ` 503` ``` show ?thesis by auto ``` chaieb@26125 ` 504` ```qed ``` chaieb@26125 ` 505` chaieb@26125 ` 506` ```lemma bezout_prime: assumes p: "prime p" and pa: "\ p dvd a" ``` chaieb@26125 ` 507` ``` shows "\x y. a*x = p*y + 1" ``` chaieb@26125 ` 508` ```proof- ``` chaieb@26125 ` 509` ``` from p have p1: "p \ 1" using prime_1 by blast ``` chaieb@26125 ` 510` ``` from prime_coprime[OF p, of a] p1 pa have ap: "coprime a p" ``` chaieb@26125 ` 511` ``` by (auto simp add: coprime_commute) ``` chaieb@26125 ` 512` ``` from coprime_bezout_strong[OF ap p1] show ?thesis . ``` chaieb@26125 ` 513` ```qed ``` chaieb@26125 ` 514` ```lemma prime_divprod: assumes p: "prime p" and pab: "p dvd a*b" ``` chaieb@26125 ` 515` ``` shows "p dvd a \ p dvd b" ``` chaieb@26125 ` 516` ```proof- ``` chaieb@26125 ` 517` ``` {assume "a=1" hence ?thesis using pab by simp } ``` chaieb@26125 ` 518` ``` moreover ``` chaieb@26125 ` 519` ``` {assume "p dvd a" hence ?thesis by blast} ``` chaieb@26125 ` 520` ``` moreover ``` chaieb@26125 ` 521` ``` {assume pa: "coprime p a" from coprime_divprod[OF pab pa] have ?thesis .. } ``` chaieb@26125 ` 522` ``` ultimately show ?thesis using prime_coprime[OF p, of a] by blast ``` chaieb@26125 ` 523` ```qed ``` chaieb@26125 ` 524` chaieb@26125 ` 525` ```lemma prime_divprod_eq: assumes p: "prime p" ``` chaieb@26125 ` 526` ``` shows "p dvd a*b \ p dvd a \ p dvd b" ``` chaieb@26125 ` 527` ```using p prime_divprod dvd_mult dvd_mult2 by auto ``` chaieb@26125 ` 528` chaieb@26125 ` 529` ```lemma prime_divexp: assumes p:"prime p" and px: "p dvd x^n" ``` chaieb@26125 ` 530` ``` shows "p dvd x" ``` chaieb@26125 ` 531` ```using px ``` chaieb@26125 ` 532` ```proof(induct n) ``` chaieb@26125 ` 533` ``` case 0 thus ?case by simp ``` chaieb@26125 ` 534` ```next ``` chaieb@26125 ` 535` ``` case (Suc n) ``` chaieb@26125 ` 536` ``` hence th: "p dvd x*x^n" by simp ``` chaieb@26125 ` 537` ``` {assume H: "p dvd x^n" ``` chaieb@26125 ` 538` ``` from Suc.hyps[OF H] have ?case .} ``` chaieb@26125 ` 539` ``` with prime_divprod[OF p th] show ?case by blast ``` chaieb@26125 ` 540` ```qed ``` chaieb@26125 ` 541` chaieb@26125 ` 542` ```lemma prime_divexp_n: "prime p \ p dvd x^n \ p^n dvd x^n" ``` chaieb@26125 ` 543` ``` using prime_divexp[of p x n] divides_exp[of p x n] by blast ``` chaieb@26125 ` 544` chaieb@26125 ` 545` ```lemma coprime_prime_dvd_ex: assumes xy: "\coprime x y" ``` chaieb@26125 ` 546` ``` shows "\p. prime p \ p dvd x \ p dvd y" ``` chaieb@26125 ` 547` ```proof- ``` chaieb@26125 ` 548` ``` from xy[unfolded coprime_def] obtain g where g: "g \ 1" "g dvd x" "g dvd y" ``` chaieb@26125 ` 549` ``` by blast ``` chaieb@26125 ` 550` ``` from prime_factor[OF g(1)] obtain p where p: "prime p" "p dvd g" by blast ``` chaieb@26125 ` 551` ``` from g(2,3) dvd_trans[OF p(2)] p(1) show ?thesis by auto ``` chaieb@26125 ` 552` ```qed ``` chaieb@26125 ` 553` ```lemma coprime_sos: assumes xy: "coprime x y" ``` wenzelm@53077 ` 554` ``` shows "coprime (x * y) (x\<^sup>2 + y\<^sup>2)" ``` chaieb@26125 ` 555` ```proof- ``` wenzelm@53077 ` 556` ``` {assume c: "\ coprime (x * y) (x\<^sup>2 + y\<^sup>2)" ``` chaieb@26125 ` 557` ``` from coprime_prime_dvd_ex[OF c] obtain p ``` wenzelm@53077 ` 558` ``` where p: "prime p" "p dvd x*y" "p dvd x\<^sup>2 + y\<^sup>2" by blast ``` chaieb@26125 ` 559` ``` {assume px: "p dvd x" ``` haftmann@27651 ` 560` ``` from dvd_mult[OF px, of x] p(3) ``` wenzelm@53077 ` 561` ``` obtain r s where "x * x = p * r" and "x\<^sup>2 + y\<^sup>2 = p * s" ``` haftmann@27651 ` 562` ``` by (auto elim!: dvdE) ``` wenzelm@53077 ` 563` ``` then have "y\<^sup>2 = p * (s - r)" ``` haftmann@27651 ` 564` ``` by (auto simp add: power2_eq_square diff_mult_distrib2) ``` wenzelm@53077 ` 565` ``` then have "p dvd y\<^sup>2" .. ``` chaieb@26125 ` 566` ``` with prime_divexp[OF p(1), of y 2] have py: "p dvd y" . ``` chaieb@26125 ` 567` ``` from p(1) px py xy[unfolded coprime, rule_format, of p] prime_1 ``` chaieb@26125 ` 568` ``` have False by simp } ``` chaieb@26125 ` 569` ``` moreover ``` chaieb@26125 ` 570` ``` {assume py: "p dvd y" ``` haftmann@27651 ` 571` ``` from dvd_mult[OF py, of y] p(3) ``` wenzelm@53077 ` 572` ``` obtain r s where "y * y = p * r" and "x\<^sup>2 + y\<^sup>2 = p * s" ``` haftmann@27651 ` 573` ``` by (auto elim!: dvdE) ``` wenzelm@53077 ` 574` ``` then have "x\<^sup>2 = p * (s - r)" ``` haftmann@27651 ` 575` ``` by (auto simp add: power2_eq_square diff_mult_distrib2) ``` wenzelm@53077 ` 576` ``` then have "p dvd x\<^sup>2" .. ``` chaieb@26125 ` 577` ``` with prime_divexp[OF p(1), of x 2] have px: "p dvd x" . ``` chaieb@26125 ` 578` ``` from p(1) px py xy[unfolded coprime, rule_format, of p] prime_1 ``` chaieb@26125 ` 579` ``` have False by simp } ``` chaieb@26125 ` 580` ``` ultimately have False using prime_divprod[OF p(1,2)] by blast} ``` chaieb@26125 ` 581` ``` thus ?thesis by blast ``` chaieb@26125 ` 582` ```qed ``` chaieb@26125 ` 583` chaieb@26125 ` 584` ```lemma distinct_prime_coprime: "prime p \ prime q \ p \ q \ coprime p q" ``` chaieb@26125 ` 585` ``` unfolding prime_def coprime_prime_eq by blast ``` chaieb@26125 ` 586` wenzelm@63833 ` 587` ```lemma prime_coprime_lt: ``` wenzelm@63833 ` 588` ``` assumes p: "prime p" and x: "0 < x" and xp: "x < p" ``` chaieb@26125 ` 589` ``` shows "coprime x p" ``` wenzelm@63833 ` 590` ```proof (rule ccontr) ``` wenzelm@63833 ` 591` ``` assume c: "\ ?thesis" ``` wenzelm@63833 ` 592` ``` then obtain g where g: "g \ 1" "g dvd x" "g dvd p" unfolding coprime_def by blast ``` chaieb@26125 ` 593` ``` from dvd_imp_le[OF g(2)] x xp have gp: "g < p" by arith ``` wenzelm@63833 ` 594` ``` have "g \ 0" by (rule ccontr) (use g(2) x in simp) ``` wenzelm@63833 ` 595` ``` with g gp p[unfolded prime_def] show False by blast ``` chaieb@26125 ` 596` ```qed ``` chaieb@26125 ` 597` chaieb@26125 ` 598` ```lemma prime_odd: "prime p \ p = 2 \ odd p" unfolding prime_def by auto ``` chaieb@26125 ` 599` wenzelm@26144 ` 600` wenzelm@61382 ` 601` ```text \One property of coprimality is easier to prove via prime factors.\ ``` chaieb@26125 ` 602` chaieb@26125 ` 603` ```lemma prime_divprod_pow: ``` chaieb@26125 ` 604` ``` assumes p: "prime p" and ab: "coprime a b" and pab: "p^n dvd a * b" ``` chaieb@26125 ` 605` ``` shows "p^n dvd a \ p^n dvd b" ``` chaieb@26125 ` 606` ```proof- ``` chaieb@26125 ` 607` ``` {assume "n = 0 \ a = 1 \ b = 1" with pab have ?thesis ``` chaieb@26125 ` 608` ``` apply (cases "n=0", simp_all) ``` chaieb@26125 ` 609` ``` apply (cases "a=1", simp_all) done} ``` chaieb@26125 ` 610` ``` moreover ``` chaieb@26125 ` 611` ``` {assume n: "n \ 0" and a: "a\1" and b: "b\1" ``` chaieb@26125 ` 612` ``` then obtain m where m: "n = Suc m" by (cases n, auto) ``` chaieb@26125 ` 613` ``` from divides_exp2[OF n pab] have pab': "p dvd a*b" . ``` chaieb@26125 ` 614` ``` from prime_divprod[OF p pab'] ``` chaieb@26125 ` 615` ``` have "p dvd a \ p dvd b" . ``` chaieb@26125 ` 616` ``` moreover ``` chaieb@26125 ` 617` ``` {assume pa: "p dvd a" ``` haftmann@57512 ` 618` ``` have pnba: "p^n dvd b*a" using pab by (simp add: mult.commute) ``` chaieb@26125 ` 619` ``` from coprime_prime[OF ab, of p] p pa have "\ p dvd b" by blast ``` chaieb@26125 ` 620` ``` with prime_coprime[OF p, of b] b ``` chaieb@26125 ` 621` ``` have cpb: "coprime b p" using coprime_commute by blast ``` chaieb@26125 ` 622` ``` from coprime_exp[OF cpb] have pnb: "coprime (p^n) b" ``` wenzelm@32960 ` 623` ``` by (simp add: coprime_commute) ``` chaieb@26125 ` 624` ``` from coprime_divprod[OF pnba pnb] have ?thesis by blast } ``` chaieb@26125 ` 625` ``` moreover ``` chaieb@26125 ` 626` ``` {assume pb: "p dvd b" ``` haftmann@57512 ` 627` ``` have pnba: "p^n dvd b*a" using pab by (simp add: mult.commute) ``` chaieb@26125 ` 628` ``` from coprime_prime[OF ab, of p] p pb have "\ p dvd a" by blast ``` chaieb@26125 ` 629` ``` with prime_coprime[OF p, of a] a ``` chaieb@26125 ` 630` ``` have cpb: "coprime a p" using coprime_commute by blast ``` chaieb@26125 ` 631` ``` from coprime_exp[OF cpb] have pnb: "coprime (p^n) a" ``` wenzelm@32960 ` 632` ``` by (simp add: coprime_commute) ``` chaieb@26125 ` 633` ``` from coprime_divprod[OF pab pnb] have ?thesis by blast } ``` chaieb@26125 ` 634` ``` ultimately have ?thesis by blast} ``` chaieb@26125 ` 635` ``` ultimately show ?thesis by blast ``` chaieb@26125 ` 636` ```qed ``` chaieb@26125 ` 637` chaieb@26125 ` 638` ```lemma nat_mult_eq_one: "(n::nat) * m = 1 \ n = 1 \ m = 1" (is "?lhs \ ?rhs") ``` chaieb@26125 ` 639` ```proof ``` chaieb@26125 ` 640` ``` assume H: "?lhs" ``` haftmann@57512 ` 641` ``` hence "n dvd 1" "m dvd 1" unfolding dvd_def by (auto simp add: mult.commute) ``` chaieb@26125 ` 642` ``` thus ?rhs by auto ``` chaieb@26125 ` 643` ```next ``` chaieb@26125 ` 644` ``` assume ?rhs then show ?lhs by auto ``` chaieb@26125 ` 645` ```qed ``` chaieb@26125 ` 646` ``` ``` wenzelm@41541 ` 647` ```lemma power_Suc0: "Suc 0 ^ n = Suc 0" ``` chaieb@26125 ` 648` ``` unfolding One_nat_def[symmetric] power_one .. ``` wenzelm@41541 ` 649` chaieb@26125 ` 650` ```lemma coprime_pow: assumes ab: "coprime a b" and abcn: "a * b = c ^n" ``` chaieb@26125 ` 651` ``` shows "\r s. a = r^n \ b = s ^n" ``` chaieb@26125 ` 652` ``` using ab abcn ``` chaieb@26125 ` 653` ```proof(induct c arbitrary: a b rule: nat_less_induct) ``` chaieb@26125 ` 654` ``` fix c a b ``` chaieb@26125 ` 655` ``` assume H: "\ma b. coprime a b \ a * b = m ^ n \ (\r s. a = r ^ n \ b = s ^ n)" "coprime a b" "a * b = c ^ n" ``` chaieb@26125 ` 656` ``` let ?ths = "\r s. a = r^n \ b = s ^n" ``` chaieb@26125 ` 657` ``` {assume n: "n = 0" ``` chaieb@26125 ` 658` ``` with H(3) power_one have "a*b = 1" by simp ``` chaieb@26125 ` 659` ``` hence "a = 1 \ b = 1" by simp ``` chaieb@26125 ` 660` ``` hence ?ths ``` chaieb@26125 ` 661` ``` apply - ``` chaieb@26125 ` 662` ``` apply (rule exI[where x=1]) ``` chaieb@26125 ` 663` ``` apply (rule exI[where x=1]) ``` chaieb@26125 ` 664` ``` using power_one[of n] ``` chaieb@26125 ` 665` ``` by simp} ``` chaieb@26125 ` 666` ``` moreover ``` chaieb@26125 ` 667` ``` {assume n: "n \ 0" then obtain m where m: "n = Suc m" by (cases n, auto) ``` chaieb@26125 ` 668` ``` {assume c: "c = 0" ``` chaieb@26125 ` 669` ``` with H(3) m H(2) have ?ths apply simp ``` wenzelm@32960 ` 670` ``` apply (cases "a=0", simp_all) ``` wenzelm@32960 ` 671` ``` apply (rule exI[where x="0"], simp) ``` wenzelm@32960 ` 672` ``` apply (rule exI[where x="0"], simp) ``` wenzelm@32960 ` 673` ``` done} ``` chaieb@26125 ` 674` ``` moreover ``` chaieb@26125 ` 675` ``` {assume "c=1" with H(3) power_one have "a*b = 1" by simp ``` wenzelm@32960 ` 676` ``` hence "a = 1 \ b = 1" by simp ``` wenzelm@32960 ` 677` ``` hence ?ths ``` chaieb@26125 ` 678` ``` apply - ``` chaieb@26125 ` 679` ``` apply (rule exI[where x=1]) ``` chaieb@26125 ` 680` ``` apply (rule exI[where x=1]) ``` chaieb@26125 ` 681` ``` using power_one[of n] ``` chaieb@26125 ` 682` ``` by simp} ``` chaieb@26125 ` 683` ``` moreover ``` chaieb@26125 ` 684` ``` {assume c: "c\1" "c \ 0" ``` chaieb@26125 ` 685` ``` from prime_factor[OF c(1)] obtain p where p: "prime p" "p dvd c" by blast ``` chaieb@26125 ` 686` ``` from prime_divprod_pow[OF p(1) H(2), unfolded H(3), OF divides_exp[OF p(2), of n]] ``` chaieb@26125 ` 687` ``` have pnab: "p ^ n dvd a \ p^n dvd b" . ``` chaieb@26125 ` 688` ``` from p(2) obtain l where l: "c = p*l" unfolding dvd_def by blast ``` wenzelm@41541 ` 689` ``` have pn0: "p^n \ 0" using n prime_ge_2 [OF p(1)] by simp ``` chaieb@26125 ` 690` ``` {assume pa: "p^n dvd a" ``` chaieb@26125 ` 691` ``` then obtain k where k: "a = p^n * k" unfolding dvd_def by blast ``` chaieb@26125 ` 692` ``` from l have "l dvd c" by auto ``` chaieb@26125 ` 693` ``` with dvd_imp_le[of l c] c have "l \ c" by auto ``` chaieb@26125 ` 694` ``` moreover {assume "l = c" with l c have "p = 1" by simp with p have False by simp} ``` chaieb@26125 ` 695` ``` ultimately have lc: "l < c" by arith ``` chaieb@26125 ` 696` ``` from coprime_lmul2 [OF H(2)[unfolded k coprime_commute[of "p^n*k" b]]] ``` chaieb@26125 ` 697` ``` have kb: "coprime k b" by (simp add: coprime_commute) ``` chaieb@26125 ` 698` ``` from H(3) l k pn0 have kbln: "k * b = l ^ n" ``` wenzelm@32960 ` 699` ``` by (auto simp add: power_mult_distrib) ``` chaieb@26125 ` 700` ``` from H(1)[rule_format, OF lc kb kbln] ``` chaieb@26125 ` 701` ``` obtain r s where rs: "k = r ^n" "b = s^n" by blast ``` chaieb@26125 ` 702` ``` from k rs(1) have "a = (p*r)^n" by (simp add: power_mult_distrib) ``` chaieb@26125 ` 703` ``` with rs(2) have ?ths by blast } ``` chaieb@26125 ` 704` ``` moreover ``` chaieb@26125 ` 705` ``` {assume pb: "p^n dvd b" ``` chaieb@26125 ` 706` ``` then obtain k where k: "b = p^n * k" unfolding dvd_def by blast ``` chaieb@26125 ` 707` ``` from l have "l dvd c" by auto ``` chaieb@26125 ` 708` ``` with dvd_imp_le[of l c] c have "l \ c" by auto ``` chaieb@26125 ` 709` ``` moreover {assume "l = c" with l c have "p = 1" by simp with p have False by simp} ``` chaieb@26125 ` 710` ``` ultimately have lc: "l < c" by arith ``` chaieb@26125 ` 711` ``` from coprime_lmul2 [OF H(2)[unfolded k coprime_commute[of "p^n*k" a]]] ``` chaieb@26125 ` 712` ``` have kb: "coprime k a" by (simp add: coprime_commute) ``` chaieb@26125 ` 713` ``` from H(3) l k pn0 n have kbln: "k * a = l ^ n" ``` haftmann@57512 ` 714` ``` by (simp add: power_mult_distrib mult.commute) ``` chaieb@26125 ` 715` ``` from H(1)[rule_format, OF lc kb kbln] ``` chaieb@26125 ` 716` ``` obtain r s where rs: "k = r ^n" "a = s^n" by blast ``` chaieb@26125 ` 717` ``` from k rs(1) have "b = (p*r)^n" by (simp add: power_mult_distrib) ``` chaieb@26125 ` 718` ``` with rs(2) have ?ths by blast } ``` chaieb@26125 ` 719` ``` ultimately have ?ths using pnab by blast} ``` chaieb@26125 ` 720` ``` ultimately have ?ths by blast} ``` chaieb@26125 ` 721` ```ultimately show ?ths by blast ``` chaieb@26125 ` 722` ```qed ``` chaieb@26125 ` 723` wenzelm@61382 ` 724` ```text \More useful lemmas.\ ``` chaieb@26125 ` 725` ```lemma prime_product: ``` haftmann@27651 ` 726` ``` assumes "prime (p * q)" ``` haftmann@27651 ` 727` ``` shows "p = 1 \ q = 1" ``` haftmann@27651 ` 728` ```proof - ``` haftmann@27651 ` 729` ``` from assms have ``` haftmann@27651 ` 730` ``` "1 < p * q" and P: "\m. m dvd p * q \ m = 1 \ m = p * q" ``` haftmann@27651 ` 731` ``` unfolding prime_def by auto ``` wenzelm@61382 ` 732` ``` from \1 < p * q\ have "p \ 0" by (cases p) auto ``` haftmann@27651 ` 733` ``` then have Q: "p = p * q \ q = 1" by auto ``` haftmann@27651 ` 734` ``` have "p dvd p * q" by simp ``` haftmann@27651 ` 735` ``` then have "p = 1 \ p = p * q" by (rule P) ``` haftmann@27651 ` 736` ``` then show ?thesis by (simp add: Q) ``` haftmann@27651 ` 737` ```qed ``` chaieb@26125 ` 738` chaieb@26125 ` 739` ```lemma prime_exp: "prime (p^n) \ prime p \ n = 1" ``` chaieb@26125 ` 740` ```proof(induct n) ``` chaieb@26125 ` 741` ``` case 0 thus ?case by simp ``` chaieb@26125 ` 742` ```next ``` chaieb@26125 ` 743` ``` case (Suc n) ``` chaieb@26125 ` 744` ``` {assume "p = 0" hence ?case by simp} ``` chaieb@26125 ` 745` ``` moreover ``` chaieb@26125 ` 746` ``` {assume "p=1" hence ?case by simp} ``` chaieb@26125 ` 747` ``` moreover ``` chaieb@26125 ` 748` ``` {assume p: "p \ 0" "p\1" ``` chaieb@26125 ` 749` ``` {assume pp: "prime (p^Suc n)" ``` chaieb@26125 ` 750` ``` hence "p = 1 \ p^n = 1" using prime_product[of p "p^n"] by simp ``` chaieb@26125 ` 751` ``` with p have n: "n = 0" ``` wenzelm@32960 ` 752` ``` by (simp only: exp_eq_1 ) simp ``` chaieb@26125 ` 753` ``` with pp have "prime p \ Suc n = 1" by simp} ``` chaieb@26125 ` 754` ``` moreover ``` chaieb@26125 ` 755` ``` {assume n: "prime p \ Suc n = 1" hence "prime (p^Suc n)" by simp} ``` chaieb@26125 ` 756` ``` ultimately have ?case by blast} ``` chaieb@26125 ` 757` ``` ultimately show ?case by blast ``` chaieb@26125 ` 758` ```qed ``` chaieb@26125 ` 759` chaieb@26125 ` 760` ```lemma prime_power_mult: ``` chaieb@26125 ` 761` ``` assumes p: "prime p" and xy: "x * y = p ^ k" ``` chaieb@26125 ` 762` ``` shows "\i j. x = p ^i \ y = p^ j" ``` chaieb@26125 ` 763` ``` using xy ``` chaieb@26125 ` 764` ```proof(induct k arbitrary: x y) ``` wenzelm@63833 ` 765` ``` case 0 ``` wenzelm@63833 ` 766` ``` thus ?case apply simp by (rule exI[where x="0"], simp) ``` chaieb@26125 ` 767` ```next ``` chaieb@26125 ` 768` ``` case (Suc k x y) ``` wenzelm@63833 ` 769` ``` have p0: "p \ 0" by (rule ccontr) (use p in simp) ``` chaieb@26125 ` 770` ``` from Suc.prems have pxy: "p dvd x*y" by auto ``` wenzelm@63833 ` 771` ``` from prime_divprod[OF p pxy] show ?case ``` wenzelm@63833 ` 772` ``` proof ``` wenzelm@63833 ` 773` ``` assume px: "p dvd x" ``` chaieb@26125 ` 774` ``` then obtain d where d: "x = p*d" unfolding dvd_def by blast ``` chaieb@26125 ` 775` ``` from Suc.prems d have "p*d*y = p^Suc k" by simp ``` chaieb@26125 ` 776` ``` hence th: "d*y = p^k" using p0 by simp ``` chaieb@26125 ` 777` ``` from Suc.hyps[OF th] obtain i j where ij: "d = p^i" "y = p^j" by blast ``` chaieb@26125 ` 778` ``` with d have "x = p^Suc i" by simp ``` wenzelm@63833 ` 779` ``` with ij(2) show ?thesis by blast ``` wenzelm@63833 ` 780` ``` next ``` wenzelm@63833 ` 781` ``` assume px: "p dvd y" ``` chaieb@26125 ` 782` ``` then obtain d where d: "y = p*d" unfolding dvd_def by blast ``` haftmann@57512 ` 783` ``` from Suc.prems d have "p*d*x = p^Suc k" by (simp add: mult.commute) ``` chaieb@26125 ` 784` ``` hence th: "d*x = p^k" using p0 by simp ``` chaieb@26125 ` 785` ``` from Suc.hyps[OF th] obtain i j where ij: "d = p^i" "x = p^j" by blast ``` chaieb@26125 ` 786` ``` with d have "y = p^Suc i" by simp ``` wenzelm@63833 ` 787` ``` with ij(2) show ?thesis by blast ``` wenzelm@63833 ` 788` ``` qed ``` chaieb@26125 ` 789` ```qed ``` chaieb@26125 ` 790` chaieb@26125 ` 791` ```lemma prime_power_exp: assumes p: "prime p" and n:"n \ 0" ``` chaieb@26125 ` 792` ``` and xn: "x^n = p^k" shows "\i. x = p^i" ``` chaieb@26125 ` 793` ``` using n xn ``` chaieb@26125 ` 794` ```proof(induct n arbitrary: k) ``` chaieb@26125 ` 795` ``` case 0 thus ?case by simp ``` chaieb@26125 ` 796` ```next ``` chaieb@26125 ` 797` ``` case (Suc n k) hence th: "x*x^n = p^k" by simp ``` wenzelm@41541 ` 798` ``` {assume "n = 0" with Suc have ?case by simp (rule exI[where x="k"], simp)} ``` chaieb@26125 ` 799` ``` moreover ``` chaieb@26125 ` 800` ``` {assume n: "n \ 0" ``` chaieb@26125 ` 801` ``` from prime_power_mult[OF p th] ``` chaieb@26125 ` 802` ``` obtain i j where ij: "x = p^i" "x^n = p^j"by blast ``` chaieb@26125 ` 803` ``` from Suc.hyps[OF n ij(2)] have ?case .} ``` chaieb@26125 ` 804` ``` ultimately show ?case by blast ``` chaieb@26125 ` 805` ```qed ``` chaieb@26125 ` 806` chaieb@26125 ` 807` ```lemma divides_primepow: assumes p: "prime p" ``` chaieb@26125 ` 808` ``` shows "d dvd p^k \ (\ i. i \ k \ d = p ^i)" ``` chaieb@26125 ` 809` ```proof ``` chaieb@26125 ` 810` ``` assume H: "d dvd p^k" then obtain e where e: "d*e = p^k" ``` haftmann@57512 ` 811` ``` unfolding dvd_def apply (auto simp add: mult.commute) by blast ``` chaieb@26125 ` 812` ``` from prime_power_mult[OF p e] obtain i j where ij: "d = p^i" "e=p^j" by blast ``` chaieb@26125 ` 813` ``` from prime_ge_2[OF p] have p1: "p > 1" by arith ``` chaieb@26125 ` 814` ``` from e ij have "p^(i + j) = p^k" by (simp add: power_add) ``` chaieb@26125 ` 815` ``` hence "i + j = k" using power_inject_exp[of p "i+j" k, OF p1] by simp ``` chaieb@26125 ` 816` ``` hence "i \ k" by arith ``` chaieb@26125 ` 817` ``` with ij(1) show "\i\k. d = p ^ i" by blast ``` chaieb@26125 ` 818` ```next ``` chaieb@26125 ` 819` ``` {fix i assume H: "i \ k" "d = p^i" ``` chaieb@26125 ` 820` ``` hence "\j. k = i + j" by arith ``` chaieb@26125 ` 821` ``` then obtain j where j: "k = i + j" by blast ``` chaieb@26125 ` 822` ``` hence "p^k = p^j*d" using H(2) by (simp add: power_add) ``` chaieb@26125 ` 823` ``` hence "d dvd p^k" unfolding dvd_def by auto} ``` chaieb@26125 ` 824` ``` thus "\i\k. d = p ^ i \ d dvd p ^ k" by blast ``` chaieb@26125 ` 825` ```qed ``` chaieb@26125 ` 826` chaieb@26125 ` 827` ```lemma coprime_divisors: "d dvd a \ e dvd b \ coprime a b \ coprime d e" ``` chaieb@26125 ` 828` ``` by (auto simp add: dvd_def coprime) ``` chaieb@26125 ` 829` nipkow@34223 ` 830` ```lemma mult_inj_if_coprime_nat: ``` haftmann@62349 ` 831` ``` "inj_on f A \ inj_on g B \ \a\A. \b\B. Primes.coprime (f a) (g b) \ ``` haftmann@62349 ` 832` ``` inj_on (\(a, b). f a * g b) (A \ B)" ``` haftmann@62349 ` 833` ```apply (auto simp add: inj_on_def) ``` haftmann@62349 ` 834` ```apply (metis coprime_def dvd_antisym dvd_triv_left relprime_dvd_mult_iff) ``` haftmann@62349 ` 835` ```apply (metis coprime_commute coprime_divprod dvd_antisym dvd_triv_right) ``` nipkow@34223 ` 836` ```done ``` nipkow@34223 ` 837` chaieb@26159 ` 838` ```declare power_Suc0[simp del] ``` haftmann@26757 ` 839` paulson@11363 ` 840` ```end ```