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