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