51174
|
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 |
|