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