src/HOL/Library/Discrete.thy
author wenzelm
Sun Jan 11 13:44:25 2015 +0100 (2015-01-11)
changeset 59349 3bde948f439c
parent 58881 b9556a055632
child 60500 903bb1495239
permissions -rw-r--r--
tuned -- more Sidekick-friendly layout;
     1 (* Author: Florian Haftmann, TU Muenchen *)
     2 
     3 section {* Common discrete functions *}
     4 
     5 theory Discrete
     6 imports Main
     7 begin
     8 
     9 subsection {* Discrete logarithm *}
    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 `m \<ge> 2` `n \<ge> 2` show ?thesis by (simp only: log_rec [of m] log_rec [of n]) simp
    63     qed
    64   qed
    65 qed
    66 
    67 
    68 subsection {* Discrete square root *}
    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 `0 * 0 \<le> m` 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 `q * q \<le> n`)
   166           apply (metis `q * q \<le> n` 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