src/HOL/Library/Discrete.thy
 author haftmann Tue Feb 19 19:44:10 2013 +0100 (2013-02-19) changeset 51188 9b5bf1a9a710 parent 51174 071674018df9 child 51263 31e786e0e6a7 permissions -rw-r--r--
dropped spurious left-over from 0a2371e7ced3
```     1 (* Author: Florian Haftmann, TU Muenchen *)
```
```     2
```
```     3 header {* Common discrete functions *}
```
```     4
```
```     5 theory Discrete
```
```     6 imports Main
```
```     7 begin
```
```     8
```
```     9 lemma power2_nat_le_eq_le:
```
```    10   fixes m n :: nat
```
```    11   shows "m ^ 2 \<le> n ^ 2 \<longleftrightarrow> m \<le> n"
```
```    12   by (auto intro: power2_le_imp_le power_mono)
```
```    13
```
```    14 subsection {* Discrete logarithm *}
```
```    15
```
```    16 fun log :: "nat \<Rightarrow> nat" where
```
```    17   [simp del]: "log n = (if n < 2 then 0 else Suc (log (n div 2)))"
```
```    18
```
```    19 lemma log_zero [simp]:
```
```    20   "log 0 = 0"
```
```    21   by (simp add: log.simps)
```
```    22
```
```    23 lemma log_one [simp]:
```
```    24   "log 1 = 0"
```
```    25   by (simp add: log.simps)
```
```    26
```
```    27 lemma log_Suc_zero [simp]:
```
```    28   "log (Suc 0) = 0"
```
```    29   using log_one by simp
```
```    30
```
```    31 lemma log_rec:
```
```    32   "n \<ge> 2 \<Longrightarrow> log n = Suc (log (n div 2))"
```
```    33   by (simp add: log.simps)
```
```    34
```
```    35 lemma log_twice [simp]:
```
```    36   "n \<noteq> 0 \<Longrightarrow> log (2 * n) = Suc (log n)"
```
```    37   by (simp add: log_rec)
```
```    38
```
```    39 lemma log_half [simp]:
```
```    40   "log (n div 2) = log n - 1"
```
```    41 proof (cases "n < 2")
```
```    42   case True
```
```    43   then have "n = 0 \<or> n = 1" by arith
```
```    44   then show ?thesis by (auto simp del: One_nat_def)
```
```    45 next
```
```    46   case False then show ?thesis by (simp add: log_rec)
```
```    47 qed
```
```    48
```
```    49 lemma log_exp [simp]:
```
```    50   "log (2 ^ n) = n"
```
```    51   by (induct n) simp_all
```
```    52
```
```    53 lemma log_mono:
```
```    54   "mono log"
```
```    55 proof
```
```    56   fix m n :: nat
```
```    57   assume "m \<le> n"
```
```    58   then show "log m \<le> log n"
```
```    59   proof (induct m arbitrary: n rule: log.induct)
```
```    60     case (1 m)
```
```    61     then have mn2: "m div 2 \<le> n div 2" by arith
```
```    62     show "log m \<le> log n"
```
```    63     proof (cases "m < 2")
```
```    64       case True
```
```    65       then have "m = 0 \<or> m = 1" by arith
```
```    66       then show ?thesis by (auto simp del: One_nat_def)
```
```    67     next
```
```    68       case False
```
```    69       with mn2 have "m \<ge> 2" and "n \<ge> 2" by auto arith
```
```    70       from False have m2_0: "m div 2 \<noteq> 0" by arith
```
```    71       with mn2 have n2_0: "n div 2 \<noteq> 0" by arith
```
```    72       from False "1.hyps" mn2 have "log (m div 2) \<le> log (n div 2)" by blast
```
```    73       with m2_0 n2_0 have "log (2 * (m div 2)) \<le> log (2 * (n div 2))" by simp
```
```    74       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
```
```    75     qed
```
```    76   qed
```
```    77 qed
```
```    78
```
```    79
```
```    80 subsection {* Discrete square root *}
```
```    81
```
```    82 definition sqrt :: "nat \<Rightarrow> nat"
```
```    83 where
```
```    84   "sqrt n = Max {m. m ^ 2 \<le> n}"
```
```    85
```
```    86 lemma sqrt_inverse_power2 [simp]:
```
```    87   "sqrt (n ^ 2) = n"
```
```    88 proof -
```
```    89   have "{m. m \<le> n} \<noteq> {}" by auto
```
```    90   then have "Max {m. m \<le> n} \<le> n" by auto
```
```    91   then show ?thesis
```
```    92     by (auto simp add: sqrt_def power2_nat_le_eq_le intro: antisym)
```
```    93 qed
```
```    94
```
```    95 lemma [code]:
```
```    96   "sqrt n = Max (Set.filter (\<lambda>m. m ^ 2 \<le> n) {0..n})"
```
```    97 proof -
```
```    98   { fix m
```
```    99     assume "m\<twosuperior> \<le> n"
```
```   100     then have "m \<le> n"
```
```   101       by (cases m) (simp_all add: power2_eq_square)
```
```   102   }
```
```   103   then have "{m. m \<le> n \<and> m\<twosuperior> \<le> n} = {m. m\<twosuperior> \<le> n}" by auto
```
```   104   then show ?thesis by (simp add: sqrt_def Set.filter_def)
```
```   105 qed
```
```   106
```
```   107 lemma sqrt_le:
```
```   108   "sqrt n \<le> n"
```
```   109 proof -
```
```   110   have "0\<twosuperior> \<le> n" by simp
```
```   111   then have *: "{m. m\<twosuperior> \<le> n} \<noteq> {}" by blast
```
```   112   { fix m
```
```   113     assume "m\<twosuperior> \<le> n"
```
```   114     then have "m \<le> n"
```
```   115       by (cases m) (simp_all add: power2_eq_square)
```
```   116   } note ** = this
```
```   117   then have "{m. m\<twosuperior> \<le> n} \<subseteq> {m. m \<le> n}" by auto
```
```   118   then have "finite {m. m\<twosuperior> \<le> n}" by (rule finite_subset) rule
```
```   119   with * show ?thesis by (auto simp add: sqrt_def intro: **)
```
```   120 qed
```
```   121
```
```   122 hide_const (open) log sqrt
```
```   123
```
```   124 end
```
```   125
```