|
1 theory Recs |
|
2 imports Main Fact "~~/src/HOL/Number_Theory/Primes" |
|
3 begin |
|
4 |
|
5 lemma if_zero_one [simp]: |
|
6 "(if P then 1 else 0) = (0::nat) \<longleftrightarrow> \<not> P" |
|
7 "(if P then 0 else 1) = (0::nat) \<longleftrightarrow> P" |
|
8 "(0::nat) < (if P then 1 else 0) = P" |
|
9 by (simp_all) |
|
10 |
|
11 lemma nth: |
|
12 "(x # xs) ! 0 = x" |
|
13 "(x # y # xs) ! 1 = y" |
|
14 "(x # y # z # xs) ! 2 = z" |
|
15 "(x # y # z # u # xs) ! 3 = u" |
|
16 by (simp_all) |
|
17 |
|
18 lemma setprod_atMost_Suc[simp]: "(\<Prod>i \<le> Suc n. f i) = (\<Prod>i \<le> n. f i) * f(Suc n)" |
|
19 by(simp add:atMost_Suc mult_ac) |
|
20 |
|
21 lemma setprod_lessThan_Suc[simp]: "(\<Prod>i < Suc n. f i) = (\<Prod>i < n. f i) * f n" |
|
22 by (simp add:lessThan_Suc mult_ac) |
|
23 |
|
24 lemma setsum_add_nat_ivl2: "n \<le> p \<Longrightarrow> |
|
25 setsum f {..<n} + setsum f {n..p} = setsum f {..p::nat}" |
|
26 apply(subst setsum_Un_disjoint[symmetric]) |
|
27 apply(auto simp add: ivl_disj_un_one) |
|
28 done |
|
29 |
|
30 |
|
31 lemma setsum_eq_zero [simp]: |
|
32 fixes n::nat |
|
33 shows "(\<Sum>i < n. f i) = (0::nat) \<longleftrightarrow> (\<forall>i < n. f i = 0)" |
|
34 "(\<Sum>i \<le> n. f i) = (0::nat) \<longleftrightarrow> (\<forall>i \<le> n. f i = 0)" |
|
35 by (auto) |
|
36 |
|
37 lemma setprod_eq_zero [simp]: |
|
38 fixes n::nat |
|
39 shows "(\<Prod>i < n. f i) = (0::nat) \<longleftrightarrow> (\<exists>i < n. f i = 0)" |
|
40 "(\<Prod>i \<le> n. f i) = (0::nat) \<longleftrightarrow> (\<exists>i \<le> n. f i = 0)" |
|
41 by (auto) |
|
42 |
|
43 lemma setsum_one_less: |
|
44 fixes n::nat |
|
45 assumes "\<forall>i < n. f i \<le> 1" |
|
46 shows "(\<Sum>i < n. f i) \<le> n" |
|
47 using assms |
|
48 by (induct n) (auto) |
|
49 |
|
50 lemma setsum_least_eq: |
|
51 fixes n p::nat |
|
52 assumes h0: "p \<le> n" |
|
53 assumes h1: "\<forall>i \<in> {..<p}. f i = 1" |
|
54 assumes h2: "\<forall>i \<in> {p..n}. f i = 0" |
|
55 shows "(\<Sum>i \<le> n. f i) = p" |
|
56 proof - |
|
57 have eq_p: "(\<Sum>i \<in> {..<p}. f i) = p" |
|
58 using h1 by (induct p) (simp_all) |
|
59 have eq_zero: "(\<Sum>i \<in> {p..n}. f i) = 0" |
|
60 using h2 by auto |
|
61 have "(\<Sum>i \<le> n. f i) = (\<Sum>i \<in> {..<p}. f i) + (\<Sum>i \<in> {p..n}. f i)" |
|
62 using h0 by (simp add: setsum_add_nat_ivl2) |
|
63 also have "... = (\<Sum>i \<in> {..<p}. f i)" using eq_zero by simp |
|
64 finally show "(\<Sum>i \<le> n. f i) = p" using eq_p by simp |
|
65 qed |
|
66 |
|
67 lemma setprod_one_le: |
|
68 fixes n::nat |
|
69 assumes "\<forall>i \<le> n. f i \<le> (1::nat)" |
|
70 shows "(\<Prod>i \<le> n. f i) \<le> 1" |
|
71 using assms |
|
72 apply(induct n) |
|
73 apply(auto) |
|
74 by (metis One_nat_def eq_iff le_0_eq le_SucE mult_0 nat_mult_1) |
|
75 |
|
76 lemma setprod_greater_zero: |
|
77 fixes n::nat |
|
78 assumes "\<forall>i \<le> n. f i \<ge> (0::nat)" |
|
79 shows "(\<Prod>i \<le> n. f i) \<ge> 0" |
|
80 using assms |
|
81 by (induct n) (auto) |
|
82 |
|
83 lemma setprod_eq_one: |
|
84 fixes n::nat |
|
85 assumes "\<forall>i \<le> n. f i = Suc 0" |
|
86 shows "(\<Prod>i \<le> n. f i) = Suc 0" |
|
87 using assms |
|
88 by (induct n) (auto) |
|
89 |
|
90 lemma setsum_cut_off_less: |
|
91 fixes n::nat |
|
92 assumes h1: "m \<le> n" |
|
93 and h2: "\<forall>i \<in> {m..<n}. f i = 0" |
|
94 shows "(\<Sum>i < n. f i) = (\<Sum>i < m. f i)" |
|
95 proof - |
|
96 have eq_zero: "(\<Sum>i \<in> {m..<n}. f i) = 0" |
|
97 using h2 by auto |
|
98 have "(\<Sum>i < n. f i) = (\<Sum>i \<in> {..<m}. f i) + (\<Sum>i \<in> {m..<n}. f i)" |
|
99 using h1 by (metis atLeast0LessThan le0 setsum_add_nat_ivl) |
|
100 also have "... = (\<Sum>i \<in> {..<m}. f i)" using eq_zero by simp |
|
101 finally show "(\<Sum>i < n. f i) = (\<Sum>i < m. f i)" by simp |
|
102 qed |
|
103 |
|
104 lemma setsum_cut_off_le: |
|
105 fixes n::nat |
|
106 assumes h1: "m \<le> n" |
|
107 and h2: "\<forall>i \<in> {m..n}. f i = 0" |
|
108 shows "(\<Sum>i \<le> n. f i) = (\<Sum>i < m. f i)" |
|
109 proof - |
|
110 have eq_zero: "(\<Sum>i \<in> {m..n}. f i) = 0" |
|
111 using h2 by auto |
|
112 have "(\<Sum>i \<le> n. f i) = (\<Sum>i \<in> {..<m}. f i) + (\<Sum>i \<in> {m..n}. f i)" |
|
113 using h1 by (simp add: setsum_add_nat_ivl2) |
|
114 also have "... = (\<Sum>i \<in> {..<m}. f i)" using eq_zero by simp |
|
115 finally show "(\<Sum>i \<le> n. f i) = (\<Sum>i < m. f i)" by simp |
|
116 qed |
|
117 |
|
118 lemma setprod_one [simp]: |
|
119 fixes n::nat |
|
120 shows "(\<Prod>i < n. Suc 0) = Suc 0" |
|
121 "(\<Prod>i \<le> n. Suc 0) = Suc 0" |
|
122 by (induct n) (simp_all) |
|
123 |
|
124 |
|
125 datatype recf = z |
|
126 | s |
|
127 | id nat nat |
|
128 | Cn nat recf "recf list" |
|
129 | Pr nat recf recf |
|
130 | Mn nat recf |
|
131 |
|
132 fun arity :: "recf \<Rightarrow> nat" |
|
133 where |
|
134 "arity z = 1" |
|
135 | "arity s = 1" |
|
136 | "arity (id m n) = m" |
|
137 | "arity (Cn n f gs) = n" |
|
138 | "arity (Pr n f g) = Suc n" |
|
139 | "arity (Mn n f) = n" |
|
140 |
|
141 abbreviation |
|
142 "CN f gs \<equiv> Cn (arity (hd gs)) f gs" |
|
143 |
|
144 abbreviation |
|
145 "PR f g \<equiv> Pr (arity f) f g" |
|
146 |
|
147 fun rec_eval :: "recf \<Rightarrow> nat list \<Rightarrow> nat" |
|
148 where |
|
149 "rec_eval z xs = 0" |
|
150 | "rec_eval s xs = Suc (xs ! 0)" |
|
151 | "rec_eval (id m n) xs = xs ! n" |
|
152 | "rec_eval (Cn n f gs) xs = rec_eval f (map (\<lambda>x. rec_eval x xs) gs)" |
|
153 | "rec_eval (Pr n f g) (0 # xs) = rec_eval f xs" |
|
154 | "rec_eval (Pr n f g) (Suc x # xs) = |
|
155 rec_eval g (x # (rec_eval (Pr n f g) (x # xs)) # xs)" |
|
156 | "rec_eval (Mn n f) xs = (LEAST x. rec_eval f (x # xs) = 0)" |
|
157 |
|
158 inductive |
|
159 terminates :: "recf \<Rightarrow> nat list \<Rightarrow> bool" |
|
160 where |
|
161 termi_z: "terminates z [n]" |
|
162 | termi_s: "terminates s [n]" |
|
163 | termi_id: "\<lbrakk>n < m; length xs = m\<rbrakk> \<Longrightarrow> terminates (id m n) xs" |
|
164 | termi_cn: "\<lbrakk>terminates f (map (\<lambda>g. rec_eval g xs) gs); |
|
165 \<forall>g \<in> set gs. terminates g xs; length xs = n\<rbrakk> \<Longrightarrow> terminates (Cn n f gs) xs" |
|
166 | termi_pr: "\<lbrakk>\<forall> y < x. terminates g (y # (rec_eval (Pr n f g) (y # xs) # xs)); |
|
167 terminates f xs; |
|
168 length xs = n\<rbrakk> |
|
169 \<Longrightarrow> terminates (Pr n f g) (xs @ [x])" |
|
170 | termi_mn: "\<lbrakk>length xs = n; terminates f (r # xs); |
|
171 rec_eval f (r # xs) = 0; |
|
172 \<forall> i < r. terminates f (i # xs) \<and> rec_eval f (i # xs) > 0\<rbrakk> \<Longrightarrow> terminates (Mn n f) xs" |
|
173 |
|
174 |
|
175 section {* Recursive Function Definitions *} |
|
176 |
|
177 text {* |
|
178 @{text "constn n"} is the recursive function which computes |
|
179 natural number @{text "n"}. |
|
180 *} |
|
181 fun constn :: "nat \<Rightarrow> recf" |
|
182 where |
|
183 "constn 0 = z" | |
|
184 "constn (Suc n) = CN s [constn n]" |
|
185 |
|
186 definition |
|
187 "rec_swap f = CN f [id 2 1, id 2 0]" |
|
188 |
|
189 definition |
|
190 "rec_add = PR (id 1 0) (CN s [id 3 1])" |
|
191 |
|
192 definition |
|
193 "rec_mult = PR z (CN rec_add [id 3 1, id 3 2])" |
|
194 |
|
195 definition |
|
196 "rec_power_swap = PR (constn 1) (CN rec_mult [id 3 1, id 3 2])" |
|
197 |
|
198 definition |
|
199 "rec_power = rec_swap rec_power_swap" |
|
200 |
|
201 definition |
|
202 "rec_fact = PR (constn 1) (CN rec_mult [CN s [id 3 0], id 3 1])" |
|
203 |
|
204 definition |
|
205 "rec_pred = CN (PR z (id 3 0)) [id 1 0, id 1 0]" |
|
206 |
|
207 definition |
|
208 "rec_minus_swap = (PR (id 1 0) (CN rec_pred [id 3 1]))" |
|
209 |
|
210 definition |
|
211 "rec_minus = rec_swap rec_minus_swap" |
|
212 |
|
213 text {* Sign function returning 1 when the input argument is greater than @{text "0"}. *} |
|
214 definition |
|
215 "rec_sign = CN rec_minus [constn 1, CN rec_minus [constn 1, id 1 0]]" |
|
216 |
|
217 definition |
|
218 "rec_not = CN rec_minus [constn 1, id 1 0]" |
|
219 |
|
220 text {* |
|
221 @{text "rec_eq"} compares two arguments: returns @{text "1"} |
|
222 if they are equal; @{text "0"} otherwise. *} |
|
223 definition |
|
224 "rec_eq = CN rec_minus |
|
225 [CN (constn 1) [id 2 0], |
|
226 CN rec_add [rec_minus, rec_swap rec_minus]]" |
|
227 |
|
228 definition |
|
229 "rec_noteq = CN rec_not [rec_eq]" |
|
230 |
|
231 definition |
|
232 "rec_conj = CN rec_sign [rec_mult]" |
|
233 |
|
234 definition |
|
235 "rec_disj = CN rec_sign [rec_add]" |
|
236 |
|
237 definition |
|
238 "rec_imp = CN rec_disj [CN rec_not [id 2 0], id 2 1]" |
|
239 |
|
240 text {* |
|
241 @{text "rec_less"} compares two arguments and returns @{text "1"} if |
|
242 the first is less than the second; otherwise returns @{text "0"}. *} |
|
243 definition |
|
244 "rec_less = CN rec_sign [rec_swap rec_minus]" |
|
245 |
|
246 definition |
|
247 "rec_le = CN rec_disj [rec_less, rec_eq]" |
|
248 |
|
249 text {* Sigma and Accum for function with one and two arguments *} |
|
250 |
|
251 definition |
|
252 "rec_sigma1 f = PR (CN f [z, id 1 0]) (CN rec_add [id 3 1, CN f [s, id 3 2]])" |
|
253 |
|
254 definition |
|
255 "rec_sigma2 f = PR (CN f [z, id 2 0, id 2 1]) (CN rec_add [id 4 1, CN f [s, id 4 2, id 4 3]])" |
|
256 |
|
257 definition |
|
258 "rec_accum1 f = PR (CN f [z, id 1 0]) (CN rec_mult [id 3 1, CN f [s, id 3 2]])" |
|
259 |
|
260 definition |
|
261 "rec_accum2 f = PR (CN f [z, id 2 0, id 2 1]) (CN rec_mult [id 4 1, CN f [s, id 4 2, id 4 3]])" |
|
262 |
|
263 text {* Bounded quantifiers for one and two arguments *} |
|
264 |
|
265 definition |
|
266 "rec_all1 f = CN rec_sign [rec_accum1 f]" |
|
267 |
|
268 definition |
|
269 "rec_all2 f = CN rec_sign [rec_accum2 f]" |
|
270 |
|
271 definition |
|
272 "rec_ex1 f = CN rec_sign [rec_sigma1 f]" |
|
273 |
|
274 definition |
|
275 "rec_ex2 f = CN rec_sign [rec_sigma2 f]" |
|
276 |
|
277 text {* Dvd *} |
|
278 |
|
279 definition |
|
280 "rec_dvd_swap = CN (rec_ex2 (CN rec_eq [id 3 2, CN rec_mult [id 3 1, id 3 0]])) [id 2 0, id 2 1, id 2 0]" |
|
281 |
|
282 definition |
|
283 "rec_dvd = rec_swap rec_dvd_swap" |
|
284 |
|
285 section {* Correctness of Recursive Functions *} |
|
286 |
|
287 lemma constn_lemma [simp]: |
|
288 "rec_eval (constn n) xs = n" |
|
289 by (induct n) (simp_all) |
|
290 |
|
291 lemma swap_lemma [simp]: |
|
292 "rec_eval (rec_swap f) [x, y] = rec_eval f [y, x]" |
|
293 by (simp add: rec_swap_def) |
|
294 |
|
295 lemma add_lemma [simp]: |
|
296 "rec_eval rec_add [x, y] = x + y" |
|
297 by (induct x) (simp_all add: rec_add_def) |
|
298 |
|
299 lemma mult_lemma [simp]: |
|
300 "rec_eval rec_mult [x, y] = x * y" |
|
301 by (induct x) (simp_all add: rec_mult_def) |
|
302 |
|
303 lemma power_swap_lemma [simp]: |
|
304 "rec_eval rec_power_swap [y, x] = x ^ y" |
|
305 by (induct y) (simp_all add: rec_power_swap_def) |
|
306 |
|
307 lemma power_lemma [simp]: |
|
308 "rec_eval rec_power [x, y] = x ^ y" |
|
309 by (simp add: rec_power_def) |
|
310 |
|
311 lemma fact_lemma [simp]: |
|
312 "rec_eval rec_fact [x] = fact x" |
|
313 by (induct x) (simp_all add: rec_fact_def) |
|
314 |
|
315 lemma pred_lemma [simp]: |
|
316 "rec_eval rec_pred [x] = x - 1" |
|
317 by (induct x) (simp_all add: rec_pred_def) |
|
318 |
|
319 lemma minus_swap_lemma [simp]: |
|
320 "rec_eval rec_minus_swap [x, y] = y - x" |
|
321 by (induct x) (simp_all add: rec_minus_swap_def) |
|
322 |
|
323 lemma minus_lemma [simp]: |
|
324 "rec_eval rec_minus [x, y] = x - y" |
|
325 by (simp add: rec_minus_def) |
|
326 |
|
327 lemma sign_lemma [simp]: |
|
328 "rec_eval rec_sign [x] = (if x = 0 then 0 else 1)" |
|
329 by (simp add: rec_sign_def) |
|
330 |
|
331 lemma not_lemma [simp]: |
|
332 "rec_eval rec_not [x] = (if x = 0 then 1 else 0)" |
|
333 by (simp add: rec_not_def) |
|
334 |
|
335 lemma eq_lemma [simp]: |
|
336 "rec_eval rec_eq [x, y] = (if x = y then 1 else 0)" |
|
337 by (simp add: rec_eq_def) |
|
338 |
|
339 lemma noteq_lemma [simp]: |
|
340 "rec_eval rec_noteq [x, y] = (if x \<noteq> y then 1 else 0)" |
|
341 by (simp add: rec_noteq_def) |
|
342 |
|
343 lemma conj_lemma [simp]: |
|
344 "rec_eval rec_conj [x, y] = (if x = 0 \<or> y = 0 then 0 else 1)" |
|
345 by (simp add: rec_conj_def) |
|
346 |
|
347 lemma disj_lemma [simp]: |
|
348 "rec_eval rec_disj [x, y] = (if x = 0 \<and> y = 0 then 0 else 1)" |
|
349 by (simp add: rec_disj_def) |
|
350 |
|
351 lemma imp_lemma [simp]: |
|
352 "rec_eval rec_imp [x, y] = (if 0 < x \<and> y = 0 then 0 else 1)" |
|
353 by (simp add: rec_imp_def) |
|
354 |
|
355 lemma less_lemma [simp]: |
|
356 "rec_eval rec_less [x, y] = (if x < y then 1 else 0)" |
|
357 by (simp add: rec_less_def) |
|
358 |
|
359 lemma le_lemma [simp]: |
|
360 "rec_eval rec_le [x, y] = (if (x \<le> y) then 1 else 0)" |
|
361 by(simp add: rec_le_def) |
|
362 |
|
363 |
|
364 lemma sigma1_lemma [simp]: |
|
365 shows "rec_eval (rec_sigma1 f) [x, y] = (\<Sum> z \<le> x. (rec_eval f) [z, y])" |
|
366 by (induct x) (simp_all add: rec_sigma1_def) |
|
367 |
|
368 lemma sigma2_lemma [simp]: |
|
369 shows "rec_eval (rec_sigma2 f) [x, y1, y2] = (\<Sum> z \<le> x. (rec_eval f) [z, y1, y2])" |
|
370 by (induct x) (simp_all add: rec_sigma2_def) |
|
371 |
|
372 lemma accum1_lemma [simp]: |
|
373 shows "rec_eval (rec_accum1 f) [x, y] = (\<Prod> z \<le> x. (rec_eval f) [z, y])" |
|
374 by (induct x) (simp_all add: rec_accum1_def) |
|
375 |
|
376 lemma accum2_lemma [simp]: |
|
377 shows "rec_eval (rec_accum2 f) [x, y1, y2] = (\<Prod> z \<le> x. (rec_eval f) [z, y1, y2])" |
|
378 by (induct x) (simp_all add: rec_accum2_def) |
|
379 |
|
380 lemma ex1_lemma [simp]: |
|
381 "rec_eval (rec_ex1 f) [x, y] = (if (\<exists>z \<le> x. 0 < rec_eval f [z, y]) then 1 else 0)" |
|
382 by (simp add: rec_ex1_def) |
|
383 |
|
384 lemma ex2_lemma [simp]: |
|
385 "rec_eval (rec_ex2 f) [x, y1, y2] = (if (\<exists>z \<le> x. 0 < rec_eval f [z, y1, y2]) then 1 else 0)" |
|
386 by (simp add: rec_ex2_def) |
|
387 |
|
388 lemma all1_lemma [simp]: |
|
389 "rec_eval (rec_all1 f) [x, y] = (if (\<forall>z \<le> x. 0 < rec_eval f [z, y]) then 1 else 0)" |
|
390 by (simp add: rec_all1_def) |
|
391 |
|
392 lemma all2_lemma [simp]: |
|
393 "rec_eval (rec_all2 f) [x, y1, y2] = (if (\<forall>z \<le> x. 0 < rec_eval f [z, y1, y2]) then 1 else 0)" |
|
394 by (simp add: rec_all2_def) |
|
395 |
|
396 |
|
397 lemma dvd_alt_def: |
|
398 "(x dvd y) = (\<exists>k\<le>y. y = x * (k::nat))" |
|
399 apply(auto simp add: dvd_def) |
|
400 apply(case_tac x) |
|
401 apply(auto) |
|
402 done |
|
403 |
|
404 lemma dvd_swap_lemma [simp]: |
|
405 "rec_eval rec_dvd_swap [x, y] = (if y dvd x then 1 else 0)" |
|
406 unfolding dvd_alt_def |
|
407 by (auto simp add: rec_dvd_swap_def) |
|
408 |
|
409 lemma dvd_lemma [simp]: |
|
410 "rec_eval rec_dvd [x, y] = (if x dvd y then 1 else 0)" |
|
411 by (simp add: rec_dvd_def) |
|
412 |
|
413 definition |
|
414 "rec_prime = |
|
415 (let conj1 = CN rec_less [constn 1, id 1 0] in |
|
416 let disj = CN rec_disj [CN rec_eq [id 2 0, constn 1], rec_eq] in |
|
417 let imp = CN rec_imp [rec_dvd, disj] in |
|
418 let conj2 = CN (rec_all1 imp) [id 1 0, id 1 0] in |
|
419 CN rec_conj [conj1, conj2])" |
|
420 |
|
421 lemma prime_alt_def: |
|
422 fixes p::nat |
|
423 shows "prime p = (1 < p \<and> (\<forall>m \<le> p. m dvd p \<longrightarrow> m = 1 \<or> m = p))" |
|
424 apply(auto simp add: prime_nat_def dvd_def) |
|
425 by (metis One_nat_def le_neq_implies_less less_SucI less_Suc_eq_0_disj less_Suc_eq_le mult_is_0 n_less_n_mult_m not_less_eq_eq) |
|
426 |
|
427 lemma prime_lemma [simp]: |
|
428 "rec_eval rec_prime [x] = (if prime x then 1 else 0)" |
|
429 by (simp add: rec_prime_def Let_def prime_alt_def) |
|
430 |
|
431 |
|
432 fun Minr :: "(nat list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" |
|
433 where "Minr R x y = (let setx = {z | z. z \<le> x \<and> R [z, y]} in |
|
434 if (setx = {}) then (Suc x) else (Min setx))" |
|
435 |
|
436 definition |
|
437 "rec_minr f = rec_sigma (rec_accum (CN rec_not [f]))" |
|
438 |
|
439 lemma minr_lemma [simp]: |
|
440 shows "rec_eval (rec_minr f) [x, y] = Minr (\<lambda>xs. (0 < rec_eval f xs)) x y" |
|
441 apply(simp only: rec_minr_def) |
|
442 apply(simp only: sigma_lemma) |
|
443 apply(simp only: accum_lemma) |
|
444 apply(subst rec_eval.simps) |
|
445 apply(simp only: map.simps nth) |
|
446 apply(simp only: Minr.simps Let_def) |
|
447 apply(auto simp del: not_lemma) |
|
448 apply(simp) |
|
449 apply(simp only: not_lemma sign_lemma) |
|
450 apply(rule sym) |
|
451 apply(rule Min_eqI) |
|
452 apply(auto)[1] |
|
453 apply(simp) |
|
454 apply(subst setsum_cut_off_le[where m="ya"]) |
|
455 apply(simp) |
|
456 apply(simp) |
|
457 apply(metis Icc_subset_Ici_iff atLeast_def in_mono le_refl mem_Collect_eq) |
|
458 apply(rule setsum_one_less) |
|
459 apply(default) |
|
460 apply(rule impI) |
|
461 apply(rule setprod_one_le) |
|
462 apply(auto split: if_splits)[1] |
|
463 apply(simp) |
|
464 apply(rule conjI) |
|
465 apply(subst setsum_cut_off_le[where m="xa"]) |
|
466 apply(simp) |
|
467 apply(simp) |
|
468 apply (metis Icc_subset_Ici_iff atLeast_def in_mono le_refl mem_Collect_eq) |
|
469 apply(rule le_trans) |
|
470 apply(rule setsum_one_less) |
|
471 apply(default) |
|
472 apply(rule impI) |
|
473 apply(rule setprod_one_le) |
|
474 apply(auto split: if_splits)[1] |
|
475 apply(simp) |
|
476 apply(subgoal_tac "\<exists>l. l = (LEAST z. 0 < rec_eval f [z, y])") |
|
477 defer |
|
478 apply metis |
|
479 apply(erule exE) |
|
480 apply(subgoal_tac "l \<le> x") |
|
481 defer |
|
482 apply (metis not_leE not_less_Least order_trans) |
|
483 apply(subst setsum_least_eq) |
|
484 apply(rotate_tac 3) |
|
485 apply(assumption) |
|
486 prefer 3 |
|
487 apply (metis LeastI_ex) |
|
488 apply(auto)[1] |
|
489 apply(subgoal_tac "a < (LEAST z. 0 < rec_eval f [z, y])") |
|
490 prefer 2 |
|
491 apply(auto)[1] |
|
492 apply(rotate_tac 5) |
|
493 apply(drule not_less_Least) |
|
494 apply(auto)[1] |
|
495 apply(auto) |
|
496 by (metis (mono_tags) LeastI_ex) |
|
497 |
|
498 (* |
|
499 lemma prime_alt_iff: |
|
500 fixes x::nat |
|
501 shows "prime x \<longleftrightarrow> 1 < x \<and> (\<forall>u < x. \<forall>v < x. x \<noteq> u * v)" |
|
502 unfolding prime_nat_simp dvd_def |
|
503 apply(auto) |
|
504 by (smt n_less_m_mult_n nat_mult_commute) |
|
505 |
|
506 lemma prime_alt2_iff: |
|
507 fixes x::nat |
|
508 shows "prime x \<longleftrightarrow> 1 < x \<and> (\<forall>u \<le> x - 1. \<forall>v \<le> x - 1. x \<noteq> u * v)" |
|
509 unfolding prime_alt_iff |
|
510 sorry |
|
511 *) |
|
512 |
|
513 definition |
|
514 "rec_prime = CN rec_conj |
|
515 [CN rec_less [constn 1, id 1 0], |
|
516 CN (rec_all (CN (rec_all2 (CN rec_noteq [id 3 2, CN rec_mult [id 3 1, id 3 0]])) |
|
517 [CN rec_pred [id 2 1], id 2 0, id 2 1])) |
|
518 [CN rec_pred [id 1 0], id 1 0]]" |
|
519 |
|
520 lemma prime_lemma [simp]: |
|
521 "rec_eval rec_prime [x] = (if prime x then 1 else 0)" |
|
522 apply(rule trans) |
|
523 apply(simp add: rec_prime_def) |
|
524 apply(simp only: prime_nat_def dvd_def) |
|
525 apply(auto) |
|
526 apply(drule_tac x="m" in spec) |
|
527 apply(auto) |
|
528 apply(case_tac m) |
|
529 apply(auto) |
|
530 apply(case_tac nat) |
|
531 apply(auto) |
|
532 apply(case_tac k) |
|
533 apply(auto) |
|
534 apply(case_tac nat) |
|
535 apply(auto) |
|
536 done |
|
537 |
|
538 lemma if_zero [simp]: |
|
539 "(0::nat) < (if P then 1 else 0) = P" |
|
540 by (simp) |
|
541 |
|
542 lemma if_cong: |
|
543 "P = Q \<Longrightarrow> (if P then 1 else (0::nat)) = (if Q then 1 else 0)" |
|
544 by simp |
|
545 |
|
546 |
|
547 |
|
548 |
|
549 end |