79 |
74 |
80 subsection {* Discrete square root *} |
75 subsection {* Discrete square root *} |
81 |
76 |
82 definition sqrt :: "nat \<Rightarrow> nat" |
77 definition sqrt :: "nat \<Rightarrow> nat" |
83 where |
78 where |
84 "sqrt n = Max {m. m ^ 2 \<le> n}" |
79 "sqrt n = Max {m. m\<twosuperior> \<le> n}" |
|
80 |
|
81 lemma sqrt_aux: |
|
82 fixes n :: nat |
|
83 shows "finite {m. m\<twosuperior> \<le> n}" and "{m. m\<twosuperior> \<le> n} \<noteq> {}" |
|
84 proof - |
|
85 { fix m |
|
86 assume "m\<twosuperior> \<le> n" |
|
87 then have "m \<le> n" |
|
88 by (cases m) (simp_all add: power2_eq_square) |
|
89 } note ** = this |
|
90 then have "{m. m\<twosuperior> \<le> n} \<subseteq> {m. m \<le> n}" by auto |
|
91 then show "finite {m. m\<twosuperior> \<le> n}" by (rule finite_subset) rule |
|
92 have "0\<twosuperior> \<le> n" by simp |
|
93 then show *: "{m. m\<twosuperior> \<le> n} \<noteq> {}" by blast |
|
94 qed |
|
95 |
|
96 lemma [code]: |
|
97 "sqrt n = Max (Set.filter (\<lambda>m. m\<twosuperior> \<le> n) {0..n})" |
|
98 proof - |
|
99 from power2_nat_le_imp_le [of _ n] have "{m. m \<le> n \<and> m\<twosuperior> \<le> n} = {m. m\<twosuperior> \<le> n}" by auto |
|
100 then show ?thesis by (simp add: sqrt_def Set.filter_def) |
|
101 qed |
85 |
102 |
86 lemma sqrt_inverse_power2 [simp]: |
103 lemma sqrt_inverse_power2 [simp]: |
87 "sqrt (n ^ 2) = n" |
104 "sqrt (n\<twosuperior>) = n" |
88 proof - |
105 proof - |
89 have "{m. m \<le> n} \<noteq> {}" by auto |
106 have "{m. m \<le> n} \<noteq> {}" by auto |
90 then have "Max {m. m \<le> n} \<le> n" by auto |
107 then have "Max {m. m \<le> n} \<le> n" by auto |
91 then show ?thesis |
108 then show ?thesis |
92 by (auto simp add: sqrt_def power2_nat_le_eq_le intro: antisym) |
109 by (auto simp add: sqrt_def power2_nat_le_eq_le intro: antisym) |
93 qed |
110 qed |
94 |
111 |
95 lemma [code]: |
112 lemma mono_sqrt: "mono sqrt" |
96 "sqrt n = Max (Set.filter (\<lambda>m. m ^ 2 \<le> n) {0..n})" |
113 proof |
|
114 fix m n :: nat |
|
115 have *: "0 * 0 \<le> m" by simp |
|
116 assume "m \<le> n" |
|
117 then show "sqrt m \<le> sqrt n" |
|
118 by (auto intro!: Max_mono `0 * 0 \<le> m` finite_less_ub simp add: power2_eq_square sqrt_def) |
|
119 qed |
|
120 |
|
121 lemma sqrt_greater_zero_iff [simp]: |
|
122 "sqrt n > 0 \<longleftrightarrow> n > 0" |
97 proof - |
123 proof - |
98 { fix m |
124 have *: "0 < Max {m. m\<twosuperior> \<le> n} \<longleftrightarrow> (\<exists>a\<in>{m. m\<twosuperior> \<le> n}. 0 < a)" |
99 assume "m\<twosuperior> \<le> n" |
125 by (rule Max_gr_iff) (fact sqrt_aux)+ |
100 then have "m \<le> n" |
126 show ?thesis |
101 by (cases m) (simp_all add: power2_eq_square) |
127 proof |
102 } |
128 assume "0 < sqrt n" |
103 then have "{m. m \<le> n \<and> m\<twosuperior> \<le> n} = {m. m\<twosuperior> \<le> n}" by auto |
129 then have "0 < Max {m. m\<twosuperior> \<le> n}" by (simp add: sqrt_def) |
104 then show ?thesis by (simp add: sqrt_def Set.filter_def) |
130 with * show "0 < n" by (auto dest: power2_nat_le_imp_le) |
|
131 next |
|
132 assume "0 < n" |
|
133 then have "1\<twosuperior> \<le> n \<and> 0 < (1::nat)" by simp |
|
134 then have "\<exists>q. q\<twosuperior> \<le> n \<and> 0 < q" .. |
|
135 with * have "0 < Max {m. m\<twosuperior> \<le> n}" by blast |
|
136 then show "0 < sqrt n" by (simp add: sqrt_def) |
|
137 qed |
|
138 qed |
|
139 |
|
140 lemma sqrt_power2_le [simp]: (* FIXME tune proof *) |
|
141 "(sqrt n)\<twosuperior> \<le> n" |
|
142 proof (cases "n > 0") |
|
143 case False then show ?thesis by (simp add: sqrt_def) |
|
144 next |
|
145 case True then have "sqrt n > 0" by simp |
|
146 then have "mono (times (Max {m. m\<twosuperior> \<le> n}))" by (auto intro: mono_times_nat simp add: sqrt_def) |
|
147 then have *: "Max {m. m\<twosuperior> \<le> n} * Max {m. m\<twosuperior> \<le> n} = Max (times (Max {m. m\<twosuperior> \<le> n}) ` {m. m\<twosuperior> \<le> n})" |
|
148 using sqrt_aux [of n] by (rule mono_Max_commute) |
|
149 have "Max (op * (Max {m. m * m \<le> n}) ` {m. m * m \<le> n}) \<le> n" |
|
150 apply (subst Max_le_iff) |
|
151 apply (metis (mono_tags) finite_imageI finite_less_ub le_square) |
|
152 apply simp |
|
153 apply (metis le0 mult_0_right) |
|
154 apply auto |
|
155 proof - |
|
156 fix q |
|
157 assume "q * q \<le> n" |
|
158 show "Max {m. m * m \<le> n} * q \<le> n" |
|
159 proof (cases "q > 0") |
|
160 case False then show ?thesis by simp |
|
161 next |
|
162 case True then have "mono (times q)" by (rule mono_times_nat) |
|
163 then have "q * Max {m. m * m \<le> n} = Max (times q ` {m. m * m \<le> n})" |
|
164 using sqrt_aux [of n] by (auto simp add: power2_eq_square intro: mono_Max_commute) |
|
165 then have "Max {m. m * m \<le> n} * q = Max (times q ` {m. m * m \<le> n})" by (simp add: mult_ac) |
|
166 then show ?thesis apply simp |
|
167 apply (subst Max_le_iff) |
|
168 apply auto |
|
169 apply (metis (mono_tags) finite_imageI finite_less_ub le_square) |
|
170 apply (metis `q * q \<le> n`) |
|
171 using `q * q \<le> n` by (metis le_cases mult_le_mono1 mult_le_mono2 order_trans) |
|
172 qed |
|
173 qed |
|
174 with * show ?thesis by (simp add: sqrt_def power2_eq_square) |
105 qed |
175 qed |
106 |
176 |
107 lemma sqrt_le: |
177 lemma sqrt_le: |
108 "sqrt n \<le> n" |
178 "sqrt n \<le> n" |
109 proof - |
179 using sqrt_aux [of n] by (auto simp add: sqrt_def intro: power2_nat_le_imp_le) |
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 |
180 |
122 hide_const (open) log sqrt |
181 hide_const (open) log sqrt |
123 |
182 |
124 end |
183 end |
125 |
184 |