src/HOL/Library/Discrete.thy
 author blanchet Wed Sep 24 15:45:55 2014 +0200 (2014-09-24) changeset 58425 246985c6b20b parent 57514 bdc2c6b40bf2 child 58787 af9eb5e566dd permissions -rw-r--r--
simpler proof
```     1 (* Author: Florian Haftmann, TU Muenchen *)
```
```     2
```
```     3 header {* Common discrete functions *}
```
```     4
```
```     5 theory Discrete
```
```     6 imports Main
```
```     7 begin
```
```     8
```
```     9 subsection {* Discrete logarithm *}
```
```    10
```
```    11 fun log :: "nat \<Rightarrow> nat" where
```
```    12   [simp del]: "log n = (if n < 2 then 0 else Suc (log (n div 2)))"
```
```    13
```
```    14 lemma log_zero [simp]:
```
```    15   "log 0 = 0"
```
```    16   by (simp add: log.simps)
```
```    17
```
```    18 lemma log_one [simp]:
```
```    19   "log 1 = 0"
```
```    20   by (simp add: log.simps)
```
```    21
```
```    22 lemma log_Suc_zero [simp]:
```
```    23   "log (Suc 0) = 0"
```
```    24   using log_one by simp
```
```    25
```
```    26 lemma log_rec:
```
```    27   "n \<ge> 2 \<Longrightarrow> log n = Suc (log (n div 2))"
```
```    28   by (simp add: log.simps)
```
```    29
```
```    30 lemma log_twice [simp]:
```
```    31   "n \<noteq> 0 \<Longrightarrow> log (2 * n) = Suc (log n)"
```
```    32   by (simp add: log_rec)
```
```    33
```
```    34 lemma log_half [simp]:
```
```    35   "log (n div 2) = log n - 1"
```
```    36 proof (cases "n < 2")
```
```    37   case True
```
```    38   then have "n = 0 \<or> n = 1" by arith
```
```    39   then show ?thesis by (auto simp del: One_nat_def)
```
```    40 next
```
```    41   case False then show ?thesis by (simp add: log_rec)
```
```    42 qed
```
```    43
```
```    44 lemma log_exp [simp]:
```
```    45   "log (2 ^ n) = n"
```
```    46   by (induct n) simp_all
```
```    47
```
```    48 lemma log_mono:
```
```    49   "mono log"
```
```    50 proof
```
```    51   fix m n :: nat
```
```    52   assume "m \<le> n"
```
```    53   then show "log m \<le> log n"
```
```    54   proof (induct m arbitrary: n rule: log.induct)
```
```    55     case (1 m)
```
```    56     then have mn2: "m div 2 \<le> n div 2" by arith
```
```    57     show "log m \<le> log n"
```
```    58     proof (cases "m < 2")
```
```    59       case True
```
```    60       then have "m = 0 \<or> m = 1" by arith
```
```    61       then show ?thesis by (auto simp del: One_nat_def)
```
```    62     next
```
```    63       case False
```
```    64       with mn2 have "m \<ge> 2" and "n \<ge> 2" by auto arith
```
```    65       from False have m2_0: "m div 2 \<noteq> 0" by arith
```
```    66       with mn2 have n2_0: "n div 2 \<noteq> 0" by arith
```
```    67       from False "1.hyps" mn2 have "log (m div 2) \<le> log (n div 2)" by blast
```
```    68       with m2_0 n2_0 have "log (2 * (m div 2)) \<le> log (2 * (n div 2))" by simp
```
```    69       with m2_0 n2_0 `m \<ge> 2` `n \<ge> 2` show ?thesis by (simp only: log_rec [of m] log_rec [of n]) simp
```
```    70     qed
```
```    71   qed
```
```    72 qed
```
```    73
```
```    74
```
```    75 subsection {* Discrete square root *}
```
```    76
```
```    77 definition sqrt :: "nat \<Rightarrow> nat"
```
```    78 where
```
```    79   "sqrt n = Max {m. m\<^sup>2 \<le> n}"
```
```    80
```
```    81 lemma sqrt_aux:
```
```    82   fixes n :: nat
```
```    83   shows "finite {m. m\<^sup>2 \<le> n}" and "{m. m\<^sup>2 \<le> n} \<noteq> {}"
```
```    84 proof -
```
```    85   { fix m
```
```    86     assume "m\<^sup>2 \<le> n"
```
```    87     then have "m \<le> n"
```
```    88       by (cases m) (simp_all add: power2_eq_square)
```
```    89   } note ** = this
```
```    90   then have "{m. m\<^sup>2 \<le> n} \<subseteq> {m. m \<le> n}" by auto
```
```    91   then show "finite {m. m\<^sup>2 \<le> n}" by (rule finite_subset) rule
```
```    92   have "0\<^sup>2 \<le> n" by simp
```
```    93   then show *: "{m. m\<^sup>2 \<le> n} \<noteq> {}" by blast
```
```    94 qed
```
```    95
```
```    96 lemma [code]:
```
```    97   "sqrt n = Max (Set.filter (\<lambda>m. m\<^sup>2 \<le> n) {0..n})"
```
```    98 proof -
```
```    99   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
```
```   100   then show ?thesis by (simp add: sqrt_def Set.filter_def)
```
```   101 qed
```
```   102
```
```   103 lemma sqrt_inverse_power2 [simp]:
```
```   104   "sqrt (n\<^sup>2) = n"
```
```   105 proof -
```
```   106   have "{m. m \<le> n} \<noteq> {}" by auto
```
```   107   then have "Max {m. m \<le> n} \<le> n" by auto
```
```   108   then show ?thesis
```
```   109     by (auto simp add: sqrt_def power2_nat_le_eq_le intro: antisym)
```
```   110 qed
```
```   111
```
```   112 lemma mono_sqrt: "mono sqrt"
```
```   113 proof
```
```   114   fix m n :: nat
```
```   115   have *: "0 * 0 \<le> m" by simp
```
```   116   assume "m \<le> n"
```
```   117   then show "sqrt m \<le> sqrt n"
```
```   118     by (auto intro!: Max_mono `0 * 0 \<le> m` finite_less_ub simp add: power2_eq_square sqrt_def)
```
```   119 qed
```
```   120
```
```   121 lemma sqrt_greater_zero_iff [simp]:
```
```   122   "sqrt n > 0 \<longleftrightarrow> n > 0"
```
```   123 proof -
```
```   124   have *: "0 < Max {m. m\<^sup>2 \<le> n} \<longleftrightarrow> (\<exists>a\<in>{m. m\<^sup>2 \<le> n}. 0 < a)"
```
```   125     by (rule Max_gr_iff) (fact sqrt_aux)+
```
```   126   show ?thesis
```
```   127   proof
```
```   128     assume "0 < sqrt n"
```
```   129     then have "0 < Max {m. m\<^sup>2 \<le> n}" by (simp add: sqrt_def)
```
```   130     with * show "0 < n" by (auto dest: power2_nat_le_imp_le)
```
```   131   next
```
```   132     assume "0 < n"
```
```   133     then have "1\<^sup>2 \<le> n \<and> 0 < (1::nat)" by simp
```
```   134     then have "\<exists>q. q\<^sup>2 \<le> n \<and> 0 < q" ..
```
```   135     with * have "0 < Max {m. m\<^sup>2 \<le> n}" by blast
```
```   136     then show "0 < sqrt n" by  (simp add: sqrt_def)
```
```   137   qed
```
```   138 qed
```
```   139
```
```   140 lemma sqrt_power2_le [simp]: (* FIXME tune proof *)
```
```   141   "(sqrt n)\<^sup>2 \<le> n"
```
```   142 proof (cases "n > 0")
```
```   143   case False then show ?thesis by (simp add: sqrt_def)
```
```   144 next
```
```   145   case True then have "sqrt n > 0" by simp
```
```   146   then have "mono (times (Max {m. m\<^sup>2 \<le> n}))" by (auto intro: mono_times_nat simp add: sqrt_def)
```
```   147   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})"
```
```   148     using sqrt_aux [of n] by (rule mono_Max_commute)
```
```   149   have "Max (op * (Max {m. m * m \<le> n}) ` {m. m * m \<le> n}) \<le> n"
```
```   150     apply (subst Max_le_iff)
```
```   151     apply (metis (mono_tags) finite_imageI finite_less_ub le_square)
```
```   152     apply simp
```
```   153     apply (metis le0 mult_0_right)
```
```   154     apply auto
```
```   155     proof -
```
```   156       fix q
```
```   157       assume "q * q \<le> n"
```
```   158       show "Max {m. m * m \<le> n} * q \<le> n"
```
```   159       proof (cases "q > 0")
```
```   160         case False then show ?thesis by simp
```
```   161       next
```
```   162         case True then have "mono (times q)" by (rule mono_times_nat)
```
```   163         then have "q * Max {m. m * m \<le> n} = Max (times q ` {m. m * m \<le> n})"
```
```   164           using sqrt_aux [of n] by (auto simp add: power2_eq_square intro: mono_Max_commute)
```
```   165         then have "Max {m. m * m \<le> n} * q = Max (times q ` {m. m * m \<le> n})" by (simp add: ac_simps)
```
```   166         then show ?thesis apply simp
```
```   167           apply (subst Max_le_iff)
```
```   168           apply auto
```
```   169           apply (metis (mono_tags) finite_imageI finite_less_ub le_square)
```
```   170           apply (metis `q * q \<le> n`)
```
```   171           using `q * q \<le> n` by (metis le_cases mult_le_mono1 mult_le_mono2 order_trans)
```
```   172       qed
```
```   173     qed
```
```   174   with * show ?thesis by (simp add: sqrt_def power2_eq_square)
```
```   175 qed
```
```   176
```
```   177 lemma sqrt_le:
```
```   178   "sqrt n \<le> n"
```
```   179   using sqrt_aux [of n] by (auto simp add: sqrt_def intro: power2_nat_le_imp_le)
```
```   180
```
```   181 hide_const (open) log sqrt
```
```   182
```
```   183 end
```
```   184
```