src/HOL/Library/Discrete.thy
author Andreas Lochbihler
Fri Sep 20 10:09:16 2013 +0200 (2013-09-20)
changeset 53745 788730ab7da4
parent 53015 a1119cf551e8
child 57514 bdc2c6b40bf2
permissions -rw-r--r--
prefer Code.abort over code_abort
     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: mult_ac)
   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