src/HOL/Library/Discrete.thy
 author wenzelm Mon Dec 28 17:43:30 2015 +0100 (2015-12-28) changeset 61952 546958347e05 parent 61831 c43f87119d80 child 61975 b4b11391c676 permissions -rw-r--r--
prefer symbols for "Union", "Inter";
```     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 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 `n > 0` 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 with one show ?thesis by simp
```
```    32   next
```
```    33     case False with `n > 0` have "n \<ge> 2" by auto
```
```    34     moreover with * have "P (n div 2)" .
```
```    35     ultimately show ?thesis by (rule double)
```
```    36   qed
```
```    37 qed
```
```    38
```
```    39 lemma log_zero [simp]: "log 0 = 0"
```
```    40   by (simp add: log.simps)
```
```    41
```
```    42 lemma log_one [simp]: "log 1 = 0"
```
```    43   by (simp add: log.simps)
```
```    44
```
```    45 lemma log_Suc_zero [simp]: "log (Suc 0) = 0"
```
```    46   using log_one by simp
```
```    47
```
```    48 lemma log_rec: "n \<ge> 2 \<Longrightarrow> log n = Suc (log (n div 2))"
```
```    49   by (simp add: log.simps)
```
```    50
```
```    51 lemma log_twice [simp]: "n \<noteq> 0 \<Longrightarrow> log (2 * n) = Suc (log n)"
```
```    52   by (simp add: log_rec)
```
```    53
```
```    54 lemma log_half [simp]: "log (n div 2) = log n - 1"
```
```    55 proof (cases "n < 2")
```
```    56   case True
```
```    57   then have "n = 0 \<or> n = 1" by arith
```
```    58   then show ?thesis by (auto simp del: One_nat_def)
```
```    59 next
```
```    60   case False
```
```    61   then show ?thesis by (simp add: log_rec)
```
```    62 qed
```
```    63
```
```    64 lemma log_exp [simp]: "log (2 ^ n) = n"
```
```    65   by (induct n) simp_all
```
```    66
```
```    67 lemma log_mono: "mono log"
```
```    68 proof
```
```    69   fix m n :: nat
```
```    70   assume "m \<le> n"
```
```    71   then show "log m \<le> log n"
```
```    72   proof (induct m arbitrary: n rule: log.induct)
```
```    73     case (1 m)
```
```    74     then have mn2: "m div 2 \<le> n div 2" by arith
```
```    75     show "log m \<le> log n"
```
```    76     proof (cases "m \<ge> 2")
```
```    77       case False
```
```    78       then have "m = 0 \<or> m = 1" by arith
```
```    79       then show ?thesis by (auto simp del: One_nat_def)
```
```    80     next
```
```    81       case True then have "\<not> m < 2" by simp
```
```    82       with mn2 have "n \<ge> 2" by arith
```
```    83       from True have m2_0: "m div 2 \<noteq> 0" by arith
```
```    84       with mn2 have n2_0: "n div 2 \<noteq> 0" by arith
```
```    85       from `\<not> m < 2` "1.hyps" mn2 have "log (m div 2) \<le> log (n div 2)" by blast
```
```    86       with m2_0 n2_0 have "log (2 * (m div 2)) \<le> log (2 * (n div 2))" by simp
```
```    87       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
```
```    88     qed
```
```    89   qed
```
```    90 qed
```
```    91
```
```    92 lemma log_exp2_le:
```
```    93   assumes "n > 0"
```
```    94   shows "2 ^ log n \<le> n"
```
```    95 using assms proof (induct n rule: log_induct)
```
```    96   show "2 ^ log 1 \<le> (1 :: nat)" by simp
```
```    97 next
```
```    98   fix n :: nat
```
```    99   assume "n \<ge> 2"
```
```   100   with log_mono have "log n \<ge> Suc 0"
```
```   101     by (simp add: log.simps)
```
```   102   assume "2 ^ log (n div 2) \<le> n div 2"
```
```   103   with `n \<ge> 2` have "2 ^ (log n - Suc 0) \<le> n div 2" by simp
```
```   104   then have "2 ^ (log n - Suc 0) * 2 ^ 1 \<le> n div 2 * 2" by simp
```
```   105   with `log n \<ge> Suc 0` have "2 ^ log n \<le> n div 2 * 2"
```
```   106     unfolding power_add [symmetric] by simp
```
```   107   also have "n div 2 * 2 \<le> n" by (cases "even n") simp_all
```
```   108   finally show "2 ^ log n \<le> n" .
```
```   109 qed
```
```   110
```
```   111
```
```   112 subsection \<open>Discrete square root\<close>
```
```   113
```
```   114 qualified definition sqrt :: "nat \<Rightarrow> nat"
```
```   115   where "sqrt n = Max {m. m\<^sup>2 \<le> n}"
```
```   116
```
```   117 lemma sqrt_aux:
```
```   118   fixes n :: nat
```
```   119   shows "finite {m. m\<^sup>2 \<le> n}" and "{m. m\<^sup>2 \<le> n} \<noteq> {}"
```
```   120 proof -
```
```   121   { fix m
```
```   122     assume "m\<^sup>2 \<le> n"
```
```   123     then have "m \<le> n"
```
```   124       by (cases m) (simp_all add: power2_eq_square)
```
```   125   } note ** = this
```
```   126   then have "{m. m\<^sup>2 \<le> n} \<subseteq> {m. m \<le> n}" by auto
```
```   127   then show "finite {m. m\<^sup>2 \<le> n}" by (rule finite_subset) rule
```
```   128   have "0\<^sup>2 \<le> n" by simp
```
```   129   then show *: "{m. m\<^sup>2 \<le> n} \<noteq> {}" by blast
```
```   130 qed
```
```   131
```
```   132 lemma [code]: "sqrt n = Max (Set.filter (\<lambda>m. m\<^sup>2 \<le> n) {0..n})"
```
```   133 proof -
```
```   134   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
```
```   135   then show ?thesis by (simp add: sqrt_def Set.filter_def)
```
```   136 qed
```
```   137
```
```   138 lemma sqrt_inverse_power2 [simp]: "sqrt (n\<^sup>2) = n"
```
```   139 proof -
```
```   140   have "{m. m \<le> n} \<noteq> {}" by auto
```
```   141   then have "Max {m. m \<le> n} \<le> n" by auto
```
```   142   then show ?thesis
```
```   143     by (auto simp add: sqrt_def power2_nat_le_eq_le intro: antisym)
```
```   144 qed
```
```   145
```
```   146 lemma sqrt_zero [simp]: "sqrt 0 = 0"
```
```   147   using sqrt_inverse_power2 [of 0] by simp
```
```   148
```
```   149 lemma sqrt_one [simp]: "sqrt 1 = 1"
```
```   150   using sqrt_inverse_power2 [of 1] by simp
```
```   151
```
```   152 lemma mono_sqrt: "mono sqrt"
```
```   153 proof
```
```   154   fix m n :: nat
```
```   155   have *: "0 * 0 \<le> m" by simp
```
```   156   assume "m \<le> n"
```
```   157   then show "sqrt m \<le> sqrt n"
```
```   158     by (auto intro!: Max_mono \<open>0 * 0 \<le> m\<close> finite_less_ub simp add: power2_eq_square sqrt_def)
```
```   159 qed
```
```   160
```
```   161 lemma sqrt_greater_zero_iff [simp]: "sqrt n > 0 \<longleftrightarrow> n > 0"
```
```   162 proof -
```
```   163   have *: "0 < Max {m. m\<^sup>2 \<le> n} \<longleftrightarrow> (\<exists>a\<in>{m. m\<^sup>2 \<le> n}. 0 < a)"
```
```   164     by (rule Max_gr_iff) (fact sqrt_aux)+
```
```   165   show ?thesis
```
```   166   proof
```
```   167     assume "0 < sqrt n"
```
```   168     then have "0 < Max {m. m\<^sup>2 \<le> n}" by (simp add: sqrt_def)
```
```   169     with * show "0 < n" by (auto dest: power2_nat_le_imp_le)
```
```   170   next
```
```   171     assume "0 < n"
```
```   172     then have "1\<^sup>2 \<le> n \<and> 0 < (1::nat)" by simp
```
```   173     then have "\<exists>q. q\<^sup>2 \<le> n \<and> 0 < q" ..
```
```   174     with * have "0 < Max {m. m\<^sup>2 \<le> n}" by blast
```
```   175     then show "0 < sqrt n" by  (simp add: sqrt_def)
```
```   176   qed
```
```   177 qed
```
```   178
```
```   179 lemma sqrt_power2_le [simp]: "(sqrt n)\<^sup>2 \<le> n" (* FIXME tune proof *)
```
```   180 proof (cases "n > 0")
```
```   181   case False then show ?thesis by simp
```
```   182 next
```
```   183   case True then have "sqrt n > 0" by simp
```
```   184   then have "mono (times (Max {m. m\<^sup>2 \<le> n}))" by (auto intro: mono_times_nat simp add: sqrt_def)
```
```   185   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})"
```
```   186     using sqrt_aux [of n] by (rule mono_Max_commute)
```
```   187   have "Max (op * (Max {m. m * m \<le> n}) ` {m. m * m \<le> n}) \<le> n"
```
```   188     apply (subst Max_le_iff)
```
```   189     apply (metis (mono_tags) finite_imageI finite_less_ub le_square)
```
```   190     apply simp
```
```   191     apply (metis le0 mult_0_right)
```
```   192     apply auto
```
```   193     proof -
```
```   194       fix q
```
```   195       assume "q * q \<le> n"
```
```   196       show "Max {m. m * m \<le> n} * q \<le> n"
```
```   197       proof (cases "q > 0")
```
```   198         case False then show ?thesis by simp
```
```   199       next
```
```   200         case True then have "mono (times q)" by (rule mono_times_nat)
```
```   201         then have "q * Max {m. m * m \<le> n} = Max (times q ` {m. m * m \<le> n})"
```
```   202           using sqrt_aux [of n] by (auto simp add: power2_eq_square intro: mono_Max_commute)
```
```   203         then have "Max {m. m * m \<le> n} * q = Max (times q ` {m. m * m \<le> n})" by (simp add: ac_simps)
```
```   204         then show ?thesis
```
```   205           apply simp
```
```   206           apply (subst Max_le_iff)
```
```   207           apply auto
```
```   208           apply (metis (mono_tags) finite_imageI finite_less_ub le_square)
```
```   209           apply (metis \<open>q * q \<le> n\<close>)
```
```   210           apply (metis \<open>q * q \<le> n\<close> le_cases mult_le_mono1 mult_le_mono2 order_trans)
```
```   211           done
```
```   212       qed
```
```   213     qed
```
```   214   with * show ?thesis by (simp add: sqrt_def power2_eq_square)
```
```   215 qed
```
```   216
```
```   217 lemma sqrt_le: "sqrt n \<le> n"
```
```   218   using sqrt_aux [of n] by (auto simp add: sqrt_def intro: power2_nat_le_imp_le)
```
```   219
```
```   220 end
```
```   221
```
`   222 end`