src/HOL/Library/Discrete.thy
 author wenzelm Wed Mar 08 10:50:59 2017 +0100 (2017-03-08) changeset 65151 a7394aa4d21c parent 64919 7e0c8924dfda child 67399 eab6ce8368fa permissions -rw-r--r--
tuned proofs;
```     1 (* Author: Florian Haftmann, TU Muenchen *)
```
```     2
```
```     3 section \<open>Common discrete functions\<close>
```
```     4
```
```     5 theory Discrete
```
```     6 imports Complex_Main
```
```     7 begin
```
```     8
```
```     9 subsection \<open>Discrete logarithm\<close>
```
```    10
```
```    11 context
```
```    12 begin
```
```    13
```
```    14 qualified fun log :: "nat \<Rightarrow> nat"
```
```    15   where [simp del]: "log n = (if n < 2 then 0 else Suc (log (n div 2)))"
```
```    16
```
```    17 lemma log_induct [consumes 1, case_names one double]:
```
```    18   fixes n :: nat
```
```    19   assumes "n > 0"
```
```    20   assumes one: "P 1"
```
```    21   assumes double: "\<And>n. n \<ge> 2 \<Longrightarrow> P (n div 2) \<Longrightarrow> P n"
```
```    22   shows "P n"
```
```    23 using \<open>n > 0\<close> proof (induct n rule: log.induct)
```
```    24   fix n
```
```    25   assume "\<not> n < 2 \<Longrightarrow>
```
```    26           0 < n div 2 \<Longrightarrow> P (n div 2)"
```
```    27   then have *: "n \<ge> 2 \<Longrightarrow> P (n div 2)" by simp
```
```    28   assume "n > 0"
```
```    29   show "P n"
```
```    30   proof (cases "n = 1")
```
```    31     case True
```
```    32     with one show ?thesis by simp
```
```    33   next
```
```    34     case False
```
```    35     with \<open>n > 0\<close> have "n \<ge> 2" by auto
```
```    36     with * have "P (n div 2)" .
```
```    37     with \<open>n \<ge> 2\<close> show ?thesis by (rule double)
```
```    38   qed
```
```    39 qed
```
```    40
```
```    41 lemma log_zero [simp]: "log 0 = 0"
```
```    42   by (simp add: log.simps)
```
```    43
```
```    44 lemma log_one [simp]: "log 1 = 0"
```
```    45   by (simp add: log.simps)
```
```    46
```
```    47 lemma log_Suc_zero [simp]: "log (Suc 0) = 0"
```
```    48   using log_one by simp
```
```    49
```
```    50 lemma log_rec: "n \<ge> 2 \<Longrightarrow> log n = Suc (log (n div 2))"
```
```    51   by (simp add: log.simps)
```
```    52
```
```    53 lemma log_twice [simp]: "n \<noteq> 0 \<Longrightarrow> log (2 * n) = Suc (log n)"
```
```    54   by (simp add: log_rec)
```
```    55
```
```    56 lemma log_half [simp]: "log (n div 2) = log n - 1"
```
```    57 proof (cases "n < 2")
```
```    58   case True
```
```    59   then have "n = 0 \<or> n = 1" by arith
```
```    60   then show ?thesis by (auto simp del: One_nat_def)
```
```    61 next
```
```    62   case False
```
```    63   then show ?thesis by (simp add: log_rec)
```
```    64 qed
```
```    65
```
```    66 lemma log_exp [simp]: "log (2 ^ n) = n"
```
```    67   by (induct n) simp_all
```
```    68
```
```    69 lemma log_mono: "mono log"
```
```    70 proof
```
```    71   fix m n :: nat
```
```    72   assume "m \<le> n"
```
```    73   then show "log m \<le> log n"
```
```    74   proof (induct m arbitrary: n rule: log.induct)
```
```    75     case (1 m)
```
```    76     then have mn2: "m div 2 \<le> n div 2" by arith
```
```    77     show "log m \<le> log n"
```
```    78     proof (cases "m \<ge> 2")
```
```    79       case False
```
```    80       then have "m = 0 \<or> m = 1" by arith
```
```    81       then show ?thesis by (auto simp del: One_nat_def)
```
```    82     next
```
```    83       case True then have "\<not> m < 2" by simp
```
```    84       with mn2 have "n \<ge> 2" by arith
```
```    85       from True have m2_0: "m div 2 \<noteq> 0" by arith
```
```    86       with mn2 have n2_0: "n div 2 \<noteq> 0" by arith
```
```    87       from \<open>\<not> m < 2\<close> "1.hyps" mn2 have "log (m div 2) \<le> log (n div 2)" by blast
```
```    88       with m2_0 n2_0 have "log (2 * (m div 2)) \<le> log (2 * (n div 2))" by simp
```
```    89       with m2_0 n2_0 \<open>m \<ge> 2\<close> \<open>n \<ge> 2\<close> show ?thesis by (simp only: log_rec [of m] log_rec [of n]) simp
```
```    90     qed
```
```    91   qed
```
```    92 qed
```
```    93
```
```    94 lemma log_exp2_le:
```
```    95   assumes "n > 0"
```
```    96   shows "2 ^ log n \<le> n"
```
```    97   using assms
```
```    98 proof (induct n rule: log_induct)
```
```    99   case one
```
```   100   then show ?case by simp
```
```   101 next
```
```   102   case (double n)
```
```   103   with log_mono have "log n \<ge> Suc 0"
```
```   104     by (simp add: log.simps)
```
```   105   assume "2 ^ log (n div 2) \<le> n div 2"
```
```   106   with \<open>n \<ge> 2\<close> have "2 ^ (log n - Suc 0) \<le> n div 2" by simp
```
```   107   then have "2 ^ (log n - Suc 0) * 2 ^ 1 \<le> n div 2 * 2" by simp
```
```   108   with \<open>log n \<ge> Suc 0\<close> have "2 ^ log n \<le> n div 2 * 2"
```
```   109     unfolding power_add [symmetric] by simp
```
```   110   also have "n div 2 * 2 \<le> n" by (cases "even n") simp_all
```
```   111   finally show ?case .
```
```   112 qed
```
```   113
```
```   114 lemma log_exp2_gt: "2 * 2 ^ log n > n"
```
```   115 proof (cases "n > 0")
```
```   116   case True
```
```   117   thus ?thesis
```
```   118   proof (induct n rule: log_induct)
```
```   119     case (double n)
```
```   120     thus ?case
```
```   121       by (cases "even n") (auto elim!: evenE oddE simp: field_simps log.simps)
```
```   122   qed simp_all
```
```   123 qed simp_all
```
```   124
```
```   125 lemma log_exp2_ge: "2 * 2 ^ log n \<ge> n"
```
```   126   using log_exp2_gt[of n] by simp
```
```   127
```
```   128 lemma log_le_iff: "m \<le> n \<Longrightarrow> log m \<le> log n"
```
```   129   by (rule monoD [OF log_mono])
```
```   130
```
```   131 lemma log_eqI:
```
```   132   assumes "n > 0" "2^k \<le> n" "n < 2 * 2^k"
```
```   133   shows   "log n = k"
```
```   134 proof (rule antisym)
```
```   135   from \<open>n > 0\<close> have "2 ^ log n \<le> n" by (rule log_exp2_le)
```
```   136   also have "\<dots> < 2 ^ Suc k" using assms by simp
```
```   137   finally have "log n < Suc k" by (subst (asm) power_strict_increasing_iff) simp_all
```
```   138   thus "log n \<le> k" by simp
```
```   139 next
```
```   140   have "2^k \<le> n" by fact
```
```   141   also have "\<dots> < 2^(Suc (log n))" by (simp add: log_exp2_gt)
```
```   142   finally have "k < Suc (log n)" by (subst (asm) power_strict_increasing_iff) simp_all
```
```   143   thus "k \<le> log n" by simp
```
```   144 qed
```
```   145
```
```   146 lemma log_altdef: "log n = (if n = 0 then 0 else nat \<lfloor>Transcendental.log 2 (real_of_nat n)\<rfloor>)"
```
```   147 proof (cases "n = 0")
```
```   148   case False
```
```   149   have "\<lfloor>Transcendental.log 2 (real_of_nat n)\<rfloor> = int (log n)"
```
```   150   proof (rule floor_unique)
```
```   151     from False have "2 powr (real (log n)) \<le> real n"
```
```   152       by (simp add: powr_realpow log_exp2_le)
```
```   153     hence "Transcendental.log 2 (2 powr (real (log n))) \<le> Transcendental.log 2 (real n)"
```
```   154       using False by (subst Transcendental.log_le_cancel_iff) simp_all
```
```   155     also have "Transcendental.log 2 (2 powr (real (log n))) = real (log n)" by simp
```
```   156     finally show "real_of_int (int (log n)) \<le> Transcendental.log 2 (real n)" by simp
```
```   157   next
```
```   158     have "real n < real (2 * 2 ^ log n)"
```
```   159       by (subst of_nat_less_iff) (rule log_exp2_gt)
```
```   160     also have "\<dots> = 2 powr (real (log n) + 1)"
```
```   161       by (simp add: powr_add powr_realpow)
```
```   162     finally have "Transcendental.log 2 (real n) < Transcendental.log 2 \<dots>"
```
```   163       using False by (subst Transcendental.log_less_cancel_iff) simp_all
```
```   164     also have "\<dots> = real (log n) + 1" by simp
```
```   165     finally show "Transcendental.log 2 (real n) < real_of_int (int (log n)) + 1" by simp
```
```   166   qed
```
```   167   thus ?thesis by simp
```
```   168 qed simp_all
```
```   169
```
```   170
```
```   171 subsection \<open>Discrete square root\<close>
```
```   172
```
```   173 qualified definition sqrt :: "nat \<Rightarrow> nat"
```
```   174   where "sqrt n = Max {m. m\<^sup>2 \<le> n}"
```
```   175
```
```   176 lemma sqrt_aux:
```
```   177   fixes n :: nat
```
```   178   shows "finite {m. m\<^sup>2 \<le> n}" and "{m. m\<^sup>2 \<le> n} \<noteq> {}"
```
```   179 proof -
```
```   180   { fix m
```
```   181     assume "m\<^sup>2 \<le> n"
```
```   182     then have "m \<le> n"
```
```   183       by (cases m) (simp_all add: power2_eq_square)
```
```   184   } note ** = this
```
```   185   then have "{m. m\<^sup>2 \<le> n} \<subseteq> {m. m \<le> n}" by auto
```
```   186   then show "finite {m. m\<^sup>2 \<le> n}" by (rule finite_subset) rule
```
```   187   have "0\<^sup>2 \<le> n" by simp
```
```   188   then show *: "{m. m\<^sup>2 \<le> n} \<noteq> {}" by blast
```
```   189 qed
```
```   190
```
```   191 lemma sqrt_unique:
```
```   192   assumes "m^2 \<le> n" "n < (Suc m)^2"
```
```   193   shows   "Discrete.sqrt n = m"
```
```   194 proof -
```
```   195   have "m' \<le> m" if "m'^2 \<le> n" for m'
```
```   196   proof -
```
```   197     note that
```
```   198     also note assms(2)
```
```   199     finally have "m' < Suc m" by (rule power_less_imp_less_base) simp_all
```
```   200     thus "m' \<le> m" by simp
```
```   201   qed
```
```   202   with \<open>m^2 \<le> n\<close> sqrt_aux[of n] show ?thesis unfolding Discrete.sqrt_def
```
```   203     by (intro antisym Max.boundedI Max.coboundedI) simp_all
```
```   204 qed
```
```   205
```
```   206
```
```   207 lemma sqrt_code[code]: "sqrt n = Max (Set.filter (\<lambda>m. m\<^sup>2 \<le> n) {0..n})"
```
```   208 proof -
```
```   209   from power2_nat_le_imp_le [of _ n] have "{m. m \<le> n \<and> m\<^sup>2 \<le> n} = {m. m\<^sup>2 \<le> n}" by auto
```
```   210   then show ?thesis by (simp add: sqrt_def Set.filter_def)
```
```   211 qed
```
```   212
```
```   213 lemma sqrt_inverse_power2 [simp]: "sqrt (n\<^sup>2) = n"
```
```   214 proof -
```
```   215   have "{m. m \<le> n} \<noteq> {}" by auto
```
```   216   then have "Max {m. m \<le> n} \<le> n" by auto
```
```   217   then show ?thesis
```
```   218     by (auto simp add: sqrt_def power2_nat_le_eq_le intro: antisym)
```
```   219 qed
```
```   220
```
```   221 lemma sqrt_zero [simp]: "sqrt 0 = 0"
```
```   222   using sqrt_inverse_power2 [of 0] by simp
```
```   223
```
```   224 lemma sqrt_one [simp]: "sqrt 1 = 1"
```
```   225   using sqrt_inverse_power2 [of 1] by simp
```
```   226
```
```   227 lemma mono_sqrt: "mono sqrt"
```
```   228 proof
```
```   229   fix m n :: nat
```
```   230   have *: "0 * 0 \<le> m" by simp
```
```   231   assume "m \<le> n"
```
```   232   then show "sqrt m \<le> sqrt n"
```
```   233     by (auto intro!: Max_mono \<open>0 * 0 \<le> m\<close> finite_less_ub simp add: power2_eq_square sqrt_def)
```
```   234 qed
```
```   235
```
```   236 lemma mono_sqrt': "m \<le> n \<Longrightarrow> Discrete.sqrt m \<le> Discrete.sqrt n"
```
```   237   using mono_sqrt unfolding mono_def by auto
```
```   238
```
```   239 lemma sqrt_greater_zero_iff [simp]: "sqrt n > 0 \<longleftrightarrow> n > 0"
```
```   240 proof -
```
```   241   have *: "0 < Max {m. m\<^sup>2 \<le> n} \<longleftrightarrow> (\<exists>a\<in>{m. m\<^sup>2 \<le> n}. 0 < a)"
```
```   242     by (rule Max_gr_iff) (fact sqrt_aux)+
```
```   243   show ?thesis
```
```   244   proof
```
```   245     assume "0 < sqrt n"
```
```   246     then have "0 < Max {m. m\<^sup>2 \<le> n}" by (simp add: sqrt_def)
```
```   247     with * show "0 < n" by (auto dest: power2_nat_le_imp_le)
```
```   248   next
```
```   249     assume "0 < n"
```
```   250     then have "1\<^sup>2 \<le> n \<and> 0 < (1::nat)" by simp
```
```   251     then have "\<exists>q. q\<^sup>2 \<le> n \<and> 0 < q" ..
```
```   252     with * have "0 < Max {m. m\<^sup>2 \<le> n}" by blast
```
```   253     then show "0 < sqrt n" by  (simp add: sqrt_def)
```
```   254   qed
```
```   255 qed
```
```   256
```
```   257 lemma sqrt_power2_le [simp]: "(sqrt n)\<^sup>2 \<le> n" (* FIXME tune proof *)
```
```   258 proof (cases "n > 0")
```
```   259   case False then show ?thesis by simp
```
```   260 next
```
```   261   case True then have "sqrt n > 0" by simp
```
```   262   then have "mono (times (Max {m. m\<^sup>2 \<le> n}))" by (auto intro: mono_times_nat simp add: sqrt_def)
```
```   263   then have *: "Max {m. m\<^sup>2 \<le> n} * Max {m. m\<^sup>2 \<le> n} = Max (times (Max {m. m\<^sup>2 \<le> n}) ` {m. m\<^sup>2 \<le> n})"
```
```   264     using sqrt_aux [of n] by (rule mono_Max_commute)
```
```   265   have "\<And>a. a * a \<le> n \<Longrightarrow> Max {m. m * m \<le> n} * a \<le> n"
```
```   266   proof -
```
```   267     fix q
```
```   268     assume "q * q \<le> n"
```
```   269     show "Max {m. m * m \<le> n} * q \<le> n"
```
```   270     proof (cases "q > 0")
```
```   271       case False then show ?thesis by simp
```
```   272     next
```
```   273       case True then have "mono (times q)" by (rule mono_times_nat)
```
```   274       then have "q * Max {m. m * m \<le> n} = Max (times q ` {m. m * m \<le> n})"
```
```   275         using sqrt_aux [of n] by (auto simp add: power2_eq_square intro: mono_Max_commute)
```
```   276       then have "Max {m. m * m \<le> n} * q = Max (times q ` {m. m * m \<le> n})" by (simp add: ac_simps)
```
```   277       moreover have "finite (op * q ` {m. m * m \<le> n})"
```
```   278         by (metis (mono_tags) finite_imageI finite_less_ub le_square)
```
```   279       moreover have "\<exists>x. x * x \<le> n"
```
```   280         by (metis \<open>q * q \<le> n\<close>)
```
```   281       ultimately show ?thesis
```
```   282         by simp (metis \<open>q * q \<le> n\<close> le_cases mult_le_mono1 mult_le_mono2 order_trans)
```
```   283     qed
```
```   284   qed
```
```   285   then have "Max (op * (Max {m. m * m \<le> n}) ` {m. m * m \<le> n}) \<le> n"
```
```   286     apply (subst Max_le_iff)
```
```   287       apply (metis (mono_tags) finite_imageI finite_less_ub le_square)
```
```   288      apply auto
```
```   289     apply (metis le0 mult_0_right)
```
```   290     done
```
```   291   with * show ?thesis by (simp add: sqrt_def power2_eq_square)
```
```   292 qed
```
```   293
```
```   294 lemma sqrt_le: "sqrt n \<le> n"
```
```   295   using sqrt_aux [of n] by (auto simp add: sqrt_def intro: power2_nat_le_imp_le)
```
```   296
```
```   297 text \<open>Additional facts about the discrete square root, thanks to Julian Biendarra, Manuel Eberl\<close>
```
```   298
```
```   299 lemma Suc_sqrt_power2_gt: "n < (Suc (Discrete.sqrt n))^2"
```
```   300   using Max_ge[OF Discrete.sqrt_aux(1), of "Discrete.sqrt n + 1" n]
```
```   301   by (cases "n < (Suc (Discrete.sqrt n))^2") (simp_all add: Discrete.sqrt_def)
```
```   302
```
```   303 lemma le_sqrt_iff: "x \<le> Discrete.sqrt y \<longleftrightarrow> x^2 \<le> y"
```
```   304 proof -
```
```   305   have "x \<le> Discrete.sqrt y \<longleftrightarrow> (\<exists>z. z\<^sup>2 \<le> y \<and> x \<le> z)"
```
```   306     using Max_ge_iff[OF Discrete.sqrt_aux, of x y] by (simp add: Discrete.sqrt_def)
```
```   307   also have "\<dots> \<longleftrightarrow> x^2 \<le> y"
```
```   308   proof safe
```
```   309     fix z assume "x \<le> z" "z ^ 2 \<le> y"
```
```   310     thus "x^2 \<le> y" by (intro le_trans[of "x^2" "z^2" y]) (simp_all add: power2_nat_le_eq_le)
```
```   311   qed auto
```
```   312   finally show ?thesis .
```
```   313 qed
```
```   314
```
```   315 lemma le_sqrtI: "x^2 \<le> y \<Longrightarrow> x \<le> Discrete.sqrt y"
```
```   316   by (simp add: le_sqrt_iff)
```
```   317
```
```   318 lemma sqrt_le_iff: "Discrete.sqrt y \<le> x \<longleftrightarrow> (\<forall>z. z^2 \<le> y \<longrightarrow> z \<le> x)"
```
```   319   using Max.bounded_iff[OF Discrete.sqrt_aux] by (simp add: Discrete.sqrt_def)
```
```   320
```
```   321 lemma sqrt_leI:
```
```   322   "(\<And>z. z^2 \<le> y \<Longrightarrow> z \<le> x) \<Longrightarrow> Discrete.sqrt y \<le> x"
```
```   323   by (simp add: sqrt_le_iff)
```
```   324
```
```   325 lemma sqrt_Suc:
```
```   326   "Discrete.sqrt (Suc n) = (if \<exists>m. Suc n = m^2 then Suc (Discrete.sqrt n) else Discrete.sqrt n)"
```
```   327 proof cases
```
```   328   assume "\<exists> m. Suc n = m^2"
```
```   329   then obtain m where m_def: "Suc n = m^2" by blast
```
```   330   then have lhs: "Discrete.sqrt (Suc n) = m" by simp
```
```   331   from m_def sqrt_power2_le[of n]
```
```   332     have "(Discrete.sqrt n)^2 < m^2" by linarith
```
```   333   with power2_less_imp_less have lt_m: "Discrete.sqrt n < m" by blast
```
```   334   from m_def Suc_sqrt_power2_gt[of "n"]
```
```   335     have "m^2 \<le> (Suc(Discrete.sqrt n))^2" by simp
```
```   336   with power2_nat_le_eq_le have "m \<le> Suc (Discrete.sqrt n)" by blast
```
```   337   with lt_m have "m = Suc (Discrete.sqrt n)" by simp
```
```   338   with lhs m_def show ?thesis by fastforce
```
```   339 next
```
```   340   assume asm: "\<not> (\<exists> m. Suc n = m^2)"
```
```   341   hence "Suc n \<noteq> (Discrete.sqrt (Suc n))^2" by simp
```
```   342   with sqrt_power2_le[of "Suc n"]
```
```   343     have "Discrete.sqrt (Suc n) \<le> Discrete.sqrt n" by (intro le_sqrtI) linarith
```
```   344   moreover have "Discrete.sqrt (Suc n) \<ge> Discrete.sqrt n"
```
```   345     by (intro monoD[OF mono_sqrt]) simp_all
```
```   346   ultimately show ?thesis using asm by simp
```
```   347 qed
```
```   348
```
```   349 end
```
```   350
```
```   351 end
```