src/HOL/Library/Discrete.thy
 author Manuel Eberl Thu Sep 01 11:53:07 2016 +0200 (2016-09-01) changeset 63766 695d60817cb1 parent 63540 f8652d0534fa child 64449 8c44dfb4ca8a permissions -rw-r--r--
Some facts about factorial and binomial coefficients
 wenzelm@59349 ` 1` ```(* Author: Florian Haftmann, TU Muenchen *) ``` haftmann@51174 ` 2` wenzelm@60500 ` 3` ```section \Common discrete functions\ ``` haftmann@51174 ` 4` haftmann@51174 ` 5` ```theory Discrete ``` haftmann@51174 ` 6` ```imports Main ``` haftmann@51174 ` 7` ```begin ``` haftmann@51174 ` 8` wenzelm@60500 ` 9` ```subsection \Discrete logarithm\ ``` haftmann@51174 ` 10` wenzelm@61115 ` 11` ```context ``` wenzelm@61115 ` 12` ```begin ``` wenzelm@61115 ` 13` wenzelm@61115 ` 14` ```qualified fun log :: "nat \ nat" ``` wenzelm@59349 ` 15` ``` where [simp del]: "log n = (if n < 2 then 0 else Suc (log (n div 2)))" ``` haftmann@51174 ` 16` haftmann@61831 ` 17` ```lemma log_induct [consumes 1, case_names one double]: ``` haftmann@61831 ` 18` ``` fixes n :: nat ``` haftmann@61831 ` 19` ``` assumes "n > 0" ``` haftmann@61831 ` 20` ``` assumes one: "P 1" ``` haftmann@61831 ` 21` ``` assumes double: "\n. n \ 2 \ P (n div 2) \ P n" ``` haftmann@61831 ` 22` ``` shows "P n" ``` wenzelm@61975 ` 23` ```using \n > 0\ proof (induct n rule: log.induct) ``` haftmann@61831 ` 24` ``` fix n ``` haftmann@61831 ` 25` ``` assume "\ n < 2 \ ``` haftmann@61831 ` 26` ``` 0 < n div 2 \ P (n div 2)" ``` haftmann@61831 ` 27` ``` then have *: "n \ 2 \ P (n div 2)" by simp ``` haftmann@61831 ` 28` ``` assume "n > 0" ``` haftmann@61831 ` 29` ``` show "P n" ``` haftmann@61831 ` 30` ``` proof (cases "n = 1") ``` wenzelm@63540 ` 31` ``` case True ``` wenzelm@63540 ` 32` ``` with one show ?thesis by simp ``` haftmann@61831 ` 33` ``` next ``` wenzelm@63540 ` 34` ``` case False ``` wenzelm@63540 ` 35` ``` with \n > 0\ have "n \ 2" by auto ``` wenzelm@63540 ` 36` ``` with * have "P (n div 2)" . ``` wenzelm@63540 ` 37` ``` with \n \ 2\ show ?thesis by (rule double) ``` haftmann@61831 ` 38` ``` qed ``` haftmann@61831 ` 39` ```qed ``` haftmann@61831 ` 40` ``` ``` wenzelm@59349 ` 41` ```lemma log_zero [simp]: "log 0 = 0" ``` haftmann@51174 ` 42` ``` by (simp add: log.simps) ``` haftmann@51174 ` 43` wenzelm@59349 ` 44` ```lemma log_one [simp]: "log 1 = 0" ``` haftmann@51174 ` 45` ``` by (simp add: log.simps) ``` haftmann@51174 ` 46` wenzelm@59349 ` 47` ```lemma log_Suc_zero [simp]: "log (Suc 0) = 0" ``` haftmann@51174 ` 48` ``` using log_one by simp ``` haftmann@51174 ` 49` wenzelm@59349 ` 50` ```lemma log_rec: "n \ 2 \ log n = Suc (log (n div 2))" ``` haftmann@51174 ` 51` ``` by (simp add: log.simps) ``` haftmann@51174 ` 52` wenzelm@59349 ` 53` ```lemma log_twice [simp]: "n \ 0 \ log (2 * n) = Suc (log n)" ``` haftmann@51174 ` 54` ``` by (simp add: log_rec) ``` haftmann@51174 ` 55` wenzelm@59349 ` 56` ```lemma log_half [simp]: "log (n div 2) = log n - 1" ``` haftmann@51174 ` 57` ```proof (cases "n < 2") ``` haftmann@51174 ` 58` ``` case True ``` haftmann@51174 ` 59` ``` then have "n = 0 \ n = 1" by arith ``` haftmann@51174 ` 60` ``` then show ?thesis by (auto simp del: One_nat_def) ``` haftmann@51174 ` 61` ```next ``` wenzelm@59349 ` 62` ``` case False ``` wenzelm@59349 ` 63` ``` then show ?thesis by (simp add: log_rec) ``` haftmann@51174 ` 64` ```qed ``` haftmann@51174 ` 65` wenzelm@59349 ` 66` ```lemma log_exp [simp]: "log (2 ^ n) = n" ``` haftmann@51174 ` 67` ``` by (induct n) simp_all ``` haftmann@51174 ` 68` wenzelm@59349 ` 69` ```lemma log_mono: "mono log" ``` haftmann@51174 ` 70` ```proof ``` haftmann@51174 ` 71` ``` fix m n :: nat ``` haftmann@51174 ` 72` ``` assume "m \ n" ``` haftmann@51174 ` 73` ``` then show "log m \ log n" ``` haftmann@51174 ` 74` ``` proof (induct m arbitrary: n rule: log.induct) ``` haftmann@51174 ` 75` ``` case (1 m) ``` haftmann@51174 ` 76` ``` then have mn2: "m div 2 \ n div 2" by arith ``` haftmann@51174 ` 77` ``` show "log m \ log n" ``` haftmann@61831 ` 78` ``` proof (cases "m \ 2") ``` haftmann@61831 ` 79` ``` case False ``` haftmann@51174 ` 80` ``` then have "m = 0 \ m = 1" by arith ``` haftmann@51174 ` 81` ``` then show ?thesis by (auto simp del: One_nat_def) ``` haftmann@51174 ` 82` ``` next ``` haftmann@61831 ` 83` ``` case True then have "\ m < 2" by simp ``` haftmann@61831 ` 84` ``` with mn2 have "n \ 2" by arith ``` haftmann@61831 ` 85` ``` from True have m2_0: "m div 2 \ 0" by arith ``` haftmann@51174 ` 86` ``` with mn2 have n2_0: "n div 2 \ 0" by arith ``` wenzelm@61975 ` 87` ``` from \\ m < 2\ "1.hyps" mn2 have "log (m div 2) \ log (n div 2)" by blast ``` haftmann@51174 ` 88` ``` with m2_0 n2_0 have "log (2 * (m div 2)) \ log (2 * (n div 2))" by simp ``` wenzelm@60500 ` 89` ``` with m2_0 n2_0 \m \ 2\ \n \ 2\ show ?thesis by (simp only: log_rec [of m] log_rec [of n]) simp ``` haftmann@51174 ` 90` ``` qed ``` haftmann@51174 ` 91` ``` qed ``` haftmann@51174 ` 92` ```qed ``` haftmann@51174 ` 93` haftmann@61831 ` 94` ```lemma log_exp2_le: ``` haftmann@61831 ` 95` ``` assumes "n > 0" ``` haftmann@61831 ` 96` ``` shows "2 ^ log n \ n" ``` wenzelm@63516 ` 97` ``` using assms ``` wenzelm@63516 ` 98` ```proof (induct n rule: log_induct) ``` wenzelm@63516 ` 99` ``` case one ``` wenzelm@63516 ` 100` ``` then show ?case by simp ``` haftmann@61831 ` 101` ```next ``` wenzelm@63516 ` 102` ``` case (double n) ``` haftmann@61831 ` 103` ``` with log_mono have "log n \ Suc 0" ``` haftmann@61831 ` 104` ``` by (simp add: log.simps) ``` haftmann@61831 ` 105` ``` assume "2 ^ log (n div 2) \ n div 2" ``` wenzelm@61975 ` 106` ``` with \n \ 2\ have "2 ^ (log n - Suc 0) \ n div 2" by simp ``` haftmann@61831 ` 107` ``` then have "2 ^ (log n - Suc 0) * 2 ^ 1 \ n div 2 * 2" by simp ``` wenzelm@61975 ` 108` ``` with \log n \ Suc 0\ have "2 ^ log n \ n div 2 * 2" ``` haftmann@61831 ` 109` ``` unfolding power_add [symmetric] by simp ``` haftmann@61831 ` 110` ``` also have "n div 2 * 2 \ n" by (cases "even n") simp_all ``` wenzelm@63516 ` 111` ``` finally show ?case . ``` haftmann@61831 ` 112` ```qed ``` haftmann@61831 ` 113` haftmann@51174 ` 114` wenzelm@60500 ` 115` ```subsection \Discrete square root\ ``` haftmann@51174 ` 116` wenzelm@61115 ` 117` ```qualified definition sqrt :: "nat \ nat" ``` wenzelm@59349 ` 118` ``` where "sqrt n = Max {m. m\<^sup>2 \ n}" ``` haftmann@51263 ` 119` haftmann@51263 ` 120` ```lemma sqrt_aux: ``` haftmann@51263 ` 121` ``` fixes n :: nat ``` wenzelm@53015 ` 122` ``` shows "finite {m. m\<^sup>2 \ n}" and "{m. m\<^sup>2 \ n} \ {}" ``` haftmann@51263 ` 123` ```proof - ``` haftmann@51263 ` 124` ``` { fix m ``` wenzelm@53015 ` 125` ``` assume "m\<^sup>2 \ n" ``` haftmann@51263 ` 126` ``` then have "m \ n" ``` haftmann@51263 ` 127` ``` by (cases m) (simp_all add: power2_eq_square) ``` haftmann@51263 ` 128` ``` } note ** = this ``` wenzelm@53015 ` 129` ``` then have "{m. m\<^sup>2 \ n} \ {m. m \ n}" by auto ``` wenzelm@53015 ` 130` ``` then show "finite {m. m\<^sup>2 \ n}" by (rule finite_subset) rule ``` wenzelm@53015 ` 131` ``` have "0\<^sup>2 \ n" by simp ``` wenzelm@53015 ` 132` ``` then show *: "{m. m\<^sup>2 \ n} \ {}" by blast ``` haftmann@51263 ` 133` ```qed ``` haftmann@51263 ` 134` eberlm@63766 ` 135` ```lemma sqrt_unique: ``` eberlm@63766 ` 136` ``` assumes "m^2 \ n" "n < (Suc m)^2" ``` eberlm@63766 ` 137` ``` shows "Discrete.sqrt n = m" ``` eberlm@63766 ` 138` ```proof - ``` eberlm@63766 ` 139` ``` have "m' \ m" if "m'^2 \ n" for m' ``` eberlm@63766 ` 140` ``` proof - ``` eberlm@63766 ` 141` ``` note that ``` eberlm@63766 ` 142` ``` also note assms(2) ``` eberlm@63766 ` 143` ``` finally have "m' < Suc m" by (rule power_less_imp_less_base) simp_all ``` eberlm@63766 ` 144` ``` thus "m' \ m" by simp ``` eberlm@63766 ` 145` ``` qed ``` eberlm@63766 ` 146` ``` with \m^2 \ n\ sqrt_aux[of n] show ?thesis unfolding Discrete.sqrt_def ``` eberlm@63766 ` 147` ``` by (intro antisym Max.boundedI Max.coboundedI) simp_all ``` eberlm@63766 ` 148` ```qed ``` eberlm@63766 ` 149` eberlm@63766 ` 150` eberlm@63766 ` 151` ```lemma sqrt_code[code]: "sqrt n = Max (Set.filter (\m. m\<^sup>2 \ n) {0..n})" ``` haftmann@51263 ` 152` ```proof - ``` wenzelm@53015 ` 153` ``` from power2_nat_le_imp_le [of _ n] have "{m. m \ n \ m\<^sup>2 \ n} = {m. m\<^sup>2 \ n}" by auto ``` haftmann@51263 ` 154` ``` then show ?thesis by (simp add: sqrt_def Set.filter_def) ``` haftmann@51263 ` 155` ```qed ``` haftmann@51174 ` 156` wenzelm@59349 ` 157` ```lemma sqrt_inverse_power2 [simp]: "sqrt (n\<^sup>2) = n" ``` haftmann@51174 ` 158` ```proof - ``` haftmann@51174 ` 159` ``` have "{m. m \ n} \ {}" by auto ``` haftmann@51174 ` 160` ``` then have "Max {m. m \ n} \ n" by auto ``` haftmann@51174 ` 161` ``` then show ?thesis ``` haftmann@51174 ` 162` ``` by (auto simp add: sqrt_def power2_nat_le_eq_le intro: antisym) ``` haftmann@51174 ` 163` ```qed ``` haftmann@51174 ` 164` wenzelm@59349 ` 165` ```lemma sqrt_zero [simp]: "sqrt 0 = 0" ``` haftmann@58787 ` 166` ``` using sqrt_inverse_power2 [of 0] by simp ``` haftmann@58787 ` 167` wenzelm@59349 ` 168` ```lemma sqrt_one [simp]: "sqrt 1 = 1" ``` haftmann@58787 ` 169` ``` using sqrt_inverse_power2 [of 1] by simp ``` haftmann@58787 ` 170` wenzelm@59349 ` 171` ```lemma mono_sqrt: "mono sqrt" ``` haftmann@51263 ` 172` ```proof ``` haftmann@51263 ` 173` ``` fix m n :: nat ``` haftmann@51263 ` 174` ``` have *: "0 * 0 \ m" by simp ``` haftmann@51263 ` 175` ``` assume "m \ n" ``` haftmann@51263 ` 176` ``` then show "sqrt m \ sqrt n" ``` wenzelm@60500 ` 177` ``` by (auto intro!: Max_mono \0 * 0 \ m\ finite_less_ub simp add: power2_eq_square sqrt_def) ``` haftmann@51263 ` 178` ```qed ``` haftmann@51263 ` 179` eberlm@63766 ` 180` ```lemma mono_sqrt': "m \ n \ Discrete.sqrt m \ Discrete.sqrt n" ``` eberlm@63766 ` 181` ``` using mono_sqrt unfolding mono_def by auto ``` eberlm@63766 ` 182` wenzelm@59349 ` 183` ```lemma sqrt_greater_zero_iff [simp]: "sqrt n > 0 \ n > 0" ``` haftmann@51174 ` 184` ```proof - ``` wenzelm@53015 ` 185` ``` have *: "0 < Max {m. m\<^sup>2 \ n} \ (\a\{m. m\<^sup>2 \ n}. 0 < a)" ``` haftmann@51263 ` 186` ``` by (rule Max_gr_iff) (fact sqrt_aux)+ ``` haftmann@51263 ` 187` ``` show ?thesis ``` haftmann@51263 ` 188` ``` proof ``` haftmann@51263 ` 189` ``` assume "0 < sqrt n" ``` wenzelm@53015 ` 190` ``` then have "0 < Max {m. m\<^sup>2 \ n}" by (simp add: sqrt_def) ``` haftmann@51263 ` 191` ``` with * show "0 < n" by (auto dest: power2_nat_le_imp_le) ``` haftmann@51263 ` 192` ``` next ``` haftmann@51263 ` 193` ``` assume "0 < n" ``` wenzelm@53015 ` 194` ``` then have "1\<^sup>2 \ n \ 0 < (1::nat)" by simp ``` wenzelm@53015 ` 195` ``` then have "\q. q\<^sup>2 \ n \ 0 < q" .. ``` wenzelm@53015 ` 196` ``` with * have "0 < Max {m. m\<^sup>2 \ n}" by blast ``` haftmann@51263 ` 197` ``` then show "0 < sqrt n" by (simp add: sqrt_def) ``` haftmann@51263 ` 198` ``` qed ``` haftmann@51263 ` 199` ```qed ``` haftmann@51263 ` 200` wenzelm@59349 ` 201` ```lemma sqrt_power2_le [simp]: "(sqrt n)\<^sup>2 \ n" (* FIXME tune proof *) ``` haftmann@51263 ` 202` ```proof (cases "n > 0") ``` haftmann@58787 ` 203` ``` case False then show ?thesis by simp ``` haftmann@51263 ` 204` ```next ``` haftmann@51263 ` 205` ``` case True then have "sqrt n > 0" by simp ``` wenzelm@53015 ` 206` ``` then have "mono (times (Max {m. m\<^sup>2 \ n}))" by (auto intro: mono_times_nat simp add: sqrt_def) ``` wenzelm@53015 ` 207` ``` then have *: "Max {m. m\<^sup>2 \ n} * Max {m. m\<^sup>2 \ n} = Max (times (Max {m. m\<^sup>2 \ n}) ` {m. m\<^sup>2 \ n})" ``` haftmann@51263 ` 208` ``` using sqrt_aux [of n] by (rule mono_Max_commute) ``` haftmann@51263 ` 209` ``` have "Max (op * (Max {m. m * m \ n}) ` {m. m * m \ n}) \ n" ``` haftmann@51263 ` 210` ``` apply (subst Max_le_iff) ``` haftmann@51263 ` 211` ``` apply (metis (mono_tags) finite_imageI finite_less_ub le_square) ``` haftmann@51263 ` 212` ``` apply simp ``` haftmann@51263 ` 213` ``` apply (metis le0 mult_0_right) ``` haftmann@51263 ` 214` ``` apply auto ``` haftmann@51263 ` 215` ``` proof - ``` haftmann@51263 ` 216` ``` fix q ``` haftmann@51263 ` 217` ``` assume "q * q \ n" ``` haftmann@51263 ` 218` ``` show "Max {m. m * m \ n} * q \ n" ``` haftmann@51263 ` 219` ``` proof (cases "q > 0") ``` haftmann@51263 ` 220` ``` case False then show ?thesis by simp ``` haftmann@51263 ` 221` ``` next ``` haftmann@51263 ` 222` ``` case True then have "mono (times q)" by (rule mono_times_nat) ``` haftmann@51263 ` 223` ``` then have "q * Max {m. m * m \ n} = Max (times q ` {m. m * m \ n})" ``` haftmann@51263 ` 224` ``` using sqrt_aux [of n] by (auto simp add: power2_eq_square intro: mono_Max_commute) ``` haftmann@57514 ` 225` ``` then have "Max {m. m * m \ n} * q = Max (times q ` {m. m * m \ n})" by (simp add: ac_simps) ``` wenzelm@59349 ` 226` ``` then show ?thesis ``` wenzelm@59349 ` 227` ``` apply simp ``` haftmann@51263 ` 228` ``` apply (subst Max_le_iff) ``` haftmann@51263 ` 229` ``` apply auto ``` haftmann@51263 ` 230` ``` apply (metis (mono_tags) finite_imageI finite_less_ub le_square) ``` wenzelm@60500 ` 231` ``` apply (metis \q * q \ n\) ``` wenzelm@60500 ` 232` ``` apply (metis \q * q \ n\ le_cases mult_le_mono1 mult_le_mono2 order_trans) ``` wenzelm@59349 ` 233` ``` done ``` haftmann@51263 ` 234` ``` qed ``` haftmann@51263 ` 235` ``` qed ``` haftmann@51263 ` 236` ``` with * show ?thesis by (simp add: sqrt_def power2_eq_square) ``` haftmann@51174 ` 237` ```qed ``` haftmann@51174 ` 238` wenzelm@59349 ` 239` ```lemma sqrt_le: "sqrt n \ n" ``` haftmann@51263 ` 240` ``` using sqrt_aux [of n] by (auto simp add: sqrt_def intro: power2_nat_le_imp_le) ``` haftmann@51174 ` 241` haftmann@51174 ` 242` ```end ``` haftmann@51174 ` 243` nipkow@62390 ` 244` ```end ```