1 theory Recs |
|
2 imports Main Fact |
|
3 "~~/src/HOL/Number_Theory/Primes" |
|
4 "~~/src/HOL/Library/Nat_Bijection" |
|
5 "~~/src/HOL/Library/Discrete" |
|
6 begin |
|
7 |
|
8 declare One_nat_def[simp del] |
|
9 |
|
10 (* |
|
11 some definitions from |
|
12 |
|
13 A Course in Formal Languages, Automata and Groups |
|
14 I M Chiswell |
|
15 |
|
16 and |
|
17 |
|
18 Lecture on undecidability |
|
19 Michael M. Wolf |
|
20 *) |
|
21 |
|
22 lemma if_zero_one [simp]: |
|
23 "(if P then 1 else 0) = (0::nat) \<longleftrightarrow> \<not> P" |
|
24 "(0::nat) < (if P then 1 else 0) = P" |
|
25 "(if P then 0 else 1) = (if \<not>P then 1 else (0::nat))" |
|
26 by (simp_all) |
|
27 |
|
28 lemma nth: |
|
29 "(x # xs) ! 0 = x" |
|
30 "(x # y # xs) ! 1 = y" |
|
31 "(x # y # z # xs) ! 2 = z" |
|
32 "(x # y # z # u # xs) ! 3 = u" |
|
33 by (simp_all) |
|
34 |
|
35 |
|
36 section {* Some auxiliary lemmas about @{text "\<Sum>"} and @{text "\<Prod>"} *} |
|
37 |
|
38 lemma setprod_atMost_Suc[simp]: |
|
39 "(\<Prod>i \<le> Suc n. f i) = (\<Prod>i \<le> n. f i) * f(Suc n)" |
|
40 by(simp add:atMost_Suc mult_ac) |
|
41 |
|
42 lemma setprod_lessThan_Suc[simp]: |
|
43 "(\<Prod>i < Suc n. f i) = (\<Prod>i < n. f i) * f n" |
|
44 by (simp add:lessThan_Suc mult_ac) |
|
45 |
|
46 lemma setsum_add_nat_ivl2: "n \<le> p \<Longrightarrow> |
|
47 setsum f {..<n} + setsum f {n..p} = setsum f {..p::nat}" |
|
48 apply(subst setsum_Un_disjoint[symmetric]) |
|
49 apply(auto simp add: ivl_disj_un_one) |
|
50 done |
|
51 |
|
52 lemma setsum_eq_zero [simp]: |
|
53 fixes f::"nat \<Rightarrow> nat" |
|
54 shows "(\<Sum>i < n. f i) = 0 \<longleftrightarrow> (\<forall>i < n. f i = 0)" |
|
55 "(\<Sum>i \<le> n. f i) = 0 \<longleftrightarrow> (\<forall>i \<le> n. f i = 0)" |
|
56 by (auto) |
|
57 |
|
58 lemma setprod_eq_zero [simp]: |
|
59 fixes f::"nat \<Rightarrow> nat" |
|
60 shows "(\<Prod>i < n. f i) = 0 \<longleftrightarrow> (\<exists>i < n. f i = 0)" |
|
61 "(\<Prod>i \<le> n. f i) = 0 \<longleftrightarrow> (\<exists>i \<le> n. f i = 0)" |
|
62 by (auto) |
|
63 |
|
64 lemma setsum_one_less: |
|
65 fixes n::nat |
|
66 assumes "\<forall>i < n. f i \<le> 1" |
|
67 shows "(\<Sum>i < n. f i) \<le> n" |
|
68 using assms |
|
69 by (induct n) (auto) |
|
70 |
|
71 lemma setsum_one_le: |
|
72 fixes n::nat |
|
73 assumes "\<forall>i \<le> n. f i \<le> 1" |
|
74 shows "(\<Sum>i \<le> n. f i) \<le> Suc n" |
|
75 using assms |
|
76 by (induct n) (auto) |
|
77 |
|
78 lemma setsum_eq_one_le: |
|
79 fixes n::nat |
|
80 assumes "\<forall>i \<le> n. f i = 1" |
|
81 shows "(\<Sum>i \<le> n. f i) = Suc n" |
|
82 using assms |
|
83 by (induct n) (auto) |
|
84 |
|
85 lemma setsum_least_eq: |
|
86 fixes f::"nat \<Rightarrow> nat" |
|
87 assumes h0: "p \<le> n" |
|
88 assumes h1: "\<forall>i \<in> {..<p}. f i = 1" |
|
89 assumes h2: "\<forall>i \<in> {p..n}. f i = 0" |
|
90 shows "(\<Sum>i \<le> n. f i) = p" |
|
91 proof - |
|
92 have eq_p: "(\<Sum>i \<in> {..<p}. f i) = p" |
|
93 using h1 by (induct p) (simp_all) |
|
94 have eq_zero: "(\<Sum>i \<in> {p..n}. f i) = 0" |
|
95 using h2 by auto |
|
96 have "(\<Sum>i \<le> n. f i) = (\<Sum>i \<in> {..<p}. f i) + (\<Sum>i \<in> {p..n}. f i)" |
|
97 using h0 by (simp add: setsum_add_nat_ivl2) |
|
98 also have "... = (\<Sum>i \<in> {..<p}. f i)" using eq_zero by simp |
|
99 finally show "(\<Sum>i \<le> n. f i) = p" using eq_p by simp |
|
100 qed |
|
101 |
|
102 lemma nat_mult_le_one: |
|
103 fixes m n::nat |
|
104 assumes "m \<le> 1" "n \<le> 1" |
|
105 shows "m * n \<le> 1" |
|
106 using assms by (induct n) (auto) |
|
107 |
|
108 lemma setprod_one_le: |
|
109 fixes f::"nat \<Rightarrow> nat" |
|
110 assumes "\<forall>i \<le> n. f i \<le> 1" |
|
111 shows "(\<Prod>i \<le> n. f i) \<le> 1" |
|
112 using assms |
|
113 by (induct n) (auto intro: nat_mult_le_one) |
|
114 |
|
115 lemma setprod_greater_zero: |
|
116 fixes f::"nat \<Rightarrow> nat" |
|
117 assumes "\<forall>i \<le> n. f i \<ge> 0" |
|
118 shows "(\<Prod>i \<le> n. f i) \<ge> 0" |
|
119 using assms by (induct n) (auto) |
|
120 |
|
121 lemma setprod_eq_one: |
|
122 fixes f::"nat \<Rightarrow> nat" |
|
123 assumes "\<forall>i \<le> n. f i = Suc 0" |
|
124 shows "(\<Prod>i \<le> n. f i) = Suc 0" |
|
125 using assms by (induct n) (auto) |
|
126 |
|
127 lemma setsum_cut_off_less: |
|
128 fixes f::"nat \<Rightarrow> nat" |
|
129 assumes h1: "m \<le> n" |
|
130 and h2: "\<forall>i \<in> {m..<n}. f i = 0" |
|
131 shows "(\<Sum>i < n. f i) = (\<Sum>i < m. f i)" |
|
132 proof - |
|
133 have eq_zero: "(\<Sum>i \<in> {m..<n}. f i) = 0" |
|
134 using h2 by auto |
|
135 have "(\<Sum>i < n. f i) = (\<Sum>i \<in> {..<m}. f i) + (\<Sum>i \<in> {m..<n}. f i)" |
|
136 using h1 by (metis atLeast0LessThan le0 setsum_add_nat_ivl) |
|
137 also have "... = (\<Sum>i \<in> {..<m}. f i)" using eq_zero by simp |
|
138 finally show "(\<Sum>i < n. f i) = (\<Sum>i < m. f i)" by simp |
|
139 qed |
|
140 |
|
141 lemma setsum_cut_off_le: |
|
142 fixes f::"nat \<Rightarrow> nat" |
|
143 assumes h1: "m \<le> n" |
|
144 and h2: "\<forall>i \<in> {m..n}. f i = 0" |
|
145 shows "(\<Sum>i \<le> n. f i) = (\<Sum>i < m. f i)" |
|
146 proof - |
|
147 have eq_zero: "(\<Sum>i \<in> {m..n}. f i) = 0" |
|
148 using h2 by auto |
|
149 have "(\<Sum>i \<le> n. f i) = (\<Sum>i \<in> {..<m}. f i) + (\<Sum>i \<in> {m..n}. f i)" |
|
150 using h1 by (simp add: setsum_add_nat_ivl2) |
|
151 also have "... = (\<Sum>i \<in> {..<m}. f i)" using eq_zero by simp |
|
152 finally show "(\<Sum>i \<le> n. f i) = (\<Sum>i < m. f i)" by simp |
|
153 qed |
|
154 |
|
155 lemma setprod_one [simp]: |
|
156 fixes n::nat |
|
157 shows "(\<Prod>i < n. Suc 0) = Suc 0" |
|
158 "(\<Prod>i \<le> n. Suc 0) = Suc 0" |
|
159 by (induct n) (simp_all) |
|
160 |
|
161 |
|
162 |
|
163 section {* Recursive Functions *} |
|
164 |
|
165 datatype recf = Z |
|
166 | S |
|
167 | Id nat nat |
|
168 | Cn nat recf "recf list" |
|
169 | Pr nat recf recf |
|
170 | Mn nat recf |
|
171 |
|
172 fun arity :: "recf \<Rightarrow> nat" |
|
173 where |
|
174 "arity Z = 1" |
|
175 | "arity S = 1" |
|
176 | "arity (Id m n) = m" |
|
177 | "arity (Cn n f gs) = n" |
|
178 | "arity (Pr n f g) = Suc n" |
|
179 | "arity (Mn n f) = n" |
|
180 |
|
181 abbreviation |
|
182 "CN f gs \<equiv> Cn (arity (hd gs)) f gs" |
|
183 |
|
184 abbreviation |
|
185 "PR f g \<equiv> Pr (arity f) f g" |
|
186 |
|
187 abbreviation |
|
188 "MN f \<equiv> Mn (arity f - 1) f" |
|
189 |
|
190 fun rec_eval :: "recf \<Rightarrow> nat list \<Rightarrow> nat" |
|
191 where |
|
192 "rec_eval Z xs = 0" |
|
193 | "rec_eval S xs = Suc (xs ! 0)" |
|
194 | "rec_eval (Id m n) xs = xs ! n" |
|
195 | "rec_eval (Cn n f gs) xs = rec_eval f (map (\<lambda>x. rec_eval x xs) gs)" |
|
196 | "rec_eval (Pr n f g) (0 # xs) = rec_eval f xs" |
|
197 | "rec_eval (Pr n f g) (Suc x # xs) = |
|
198 rec_eval g (x # (rec_eval (Pr n f g) (x # xs)) # xs)" |
|
199 | "rec_eval (Mn n f) xs = (LEAST x. rec_eval f (x # xs) = 0)" |
|
200 |
|
201 inductive |
|
202 terminates :: "recf \<Rightarrow> nat list \<Rightarrow> bool" |
|
203 where |
|
204 termi_z: "terminates Z [n]" |
|
205 | termi_s: "terminates S [n]" |
|
206 | termi_id: "\<lbrakk>n < m; length xs = m\<rbrakk> \<Longrightarrow> terminates (Id m n) xs" |
|
207 | termi_cn: "\<lbrakk>terminates f (map (\<lambda>g. rec_eval g xs) gs); |
|
208 \<forall>g \<in> set gs. terminates g xs; length xs = n\<rbrakk> \<Longrightarrow> terminates (Cn n f gs) xs" |
|
209 | termi_pr: "\<lbrakk>\<forall> y < x. terminates g (y # (rec_eval (Pr n f g) (y # xs) # xs)); |
|
210 terminates f xs; |
|
211 length xs = n\<rbrakk> |
|
212 \<Longrightarrow> terminates (Pr n f g) (xs @ [x])" |
|
213 | termi_mn: "\<lbrakk>length xs = n; terminates f (r # xs); |
|
214 rec_eval f (r # xs) = 0; |
|
215 \<forall> i < r. terminates f (i # xs) \<and> rec_eval f (i # xs) > 0\<rbrakk> \<Longrightarrow> terminates (Mn n f) xs" |
|
216 |
|
217 |
|
218 section {* Recursive Function Definitions *} |
|
219 |
|
220 text {* |
|
221 @{text "constn n"} is the recursive function which computes |
|
222 natural number @{text "n"}. |
|
223 *} |
|
224 fun constn :: "nat \<Rightarrow> recf" |
|
225 where |
|
226 "constn 0 = Z" | |
|
227 "constn (Suc n) = CN S [constn n]" |
|
228 |
|
229 definition |
|
230 "rec_swap f = CN f [Id 2 1, Id 2 0]" |
|
231 |
|
232 definition |
|
233 "rec_add = PR (Id 1 0) (CN S [Id 3 1])" |
|
234 |
|
235 definition |
|
236 "rec_mult = PR Z (CN rec_add [Id 3 1, Id 3 2])" |
|
237 |
|
238 definition |
|
239 "rec_power = rec_swap (PR (constn 1) (CN rec_mult [Id 3 1, Id 3 2]))" |
|
240 |
|
241 definition |
|
242 "rec_fact = PR (constn 1) (CN rec_mult [CN S [Id 3 0], Id 3 1])" |
|
243 |
|
244 definition |
|
245 "rec_pred = CN (PR Z (Id 3 0)) [Id 1 0, Id 1 0]" |
|
246 |
|
247 definition |
|
248 "rec_minus = rec_swap (PR (Id 1 0) (CN rec_pred [Id 3 1]))" |
|
249 |
|
250 |
|
251 text {* |
|
252 The @{text "sign"} function returns 1 when the input argument |
|
253 is greater than @{text "0"}. *} |
|
254 |
|
255 definition |
|
256 "rec_sign = CN rec_minus [constn 1, CN rec_minus [constn 1, Id 1 0]]" |
|
257 |
|
258 definition |
|
259 "rec_not = CN rec_minus [constn 1, Id 1 0]" |
|
260 |
|
261 text {* |
|
262 @{text "rec_eq"} compares two arguments: returns @{text "1"} |
|
263 if they are equal; @{text "0"} otherwise. *} |
|
264 definition |
|
265 "rec_eq = CN rec_minus [constn 1, CN rec_add [rec_minus, rec_swap rec_minus]]" |
|
266 |
|
267 definition |
|
268 "rec_noteq = CN rec_not [rec_eq]" |
|
269 |
|
270 definition |
|
271 "rec_conj = CN rec_sign [rec_mult]" |
|
272 |
|
273 definition |
|
274 "rec_disj = CN rec_sign [rec_add]" |
|
275 |
|
276 definition |
|
277 "rec_imp = CN rec_disj [CN rec_not [Id 2 0], Id 2 1]" |
|
278 |
|
279 text {* @{term "rec_ifz [z, x, y]"} returns x if z is zero, |
|
280 y otherwise; @{term "rec_if [z, x, y]"} returns x if z is *not* |
|
281 zero, y otherwise *} |
|
282 |
|
283 definition |
|
284 "rec_ifz = PR (Id 2 0) (Id 4 3)" |
|
285 |
|
286 definition |
|
287 "rec_if = CN rec_ifz [CN rec_not [Id 3 0], Id 3 1, Id 3 2]" |
|
288 |
|
289 text {* |
|
290 @{text "rec_less"} compares two arguments and returns @{text "1"} if |
|
291 the first is less than the second; otherwise returns @{text "0"}. *} |
|
292 |
|
293 definition |
|
294 "rec_less = CN rec_sign [rec_swap rec_minus]" |
|
295 |
|
296 definition |
|
297 "rec_le = CN rec_disj [rec_less, rec_eq]" |
|
298 |
|
299 text {* Sigma and Accum for function with one and two arguments *} |
|
300 |
|
301 definition |
|
302 "rec_sigma1 f = PR (CN f [Z, Id 1 0]) (CN rec_add [Id 3 1, CN f [S, Id 3 2]])" |
|
303 |
|
304 definition |
|
305 "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]])" |
|
306 |
|
307 definition |
|
308 "rec_accum1 f = PR (CN f [Z, Id 1 0]) (CN rec_mult [Id 3 1, CN f [S, Id 3 2]])" |
|
309 |
|
310 definition |
|
311 "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]])" |
|
312 |
|
313 text {* Bounded quantifiers for one and two arguments *} |
|
314 |
|
315 definition |
|
316 "rec_all1 f = CN rec_sign [rec_accum1 f]" |
|
317 |
|
318 definition |
|
319 "rec_all2 f = CN rec_sign [rec_accum2 f]" |
|
320 |
|
321 definition |
|
322 "rec_ex1 f = CN rec_sign [rec_sigma1 f]" |
|
323 |
|
324 definition |
|
325 "rec_ex2 f = CN rec_sign [rec_sigma2 f]" |
|
326 |
|
327 text {* Dvd, Quotient, Modulo *} |
|
328 |
|
329 definition |
|
330 "rec_dvd = |
|
331 rec_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])" |
|
332 |
|
333 definition |
|
334 "rec_quo = (let lhs = CN S [Id 3 0] in |
|
335 let rhs = CN rec_mult [Id 3 2, CN S [Id 3 1]] in |
|
336 let cond = CN rec_eq [lhs, rhs] in |
|
337 let if_stmt = CN rec_if [cond, CN S [Id 3 1], Id 3 1] |
|
338 in PR Z if_stmt)" |
|
339 |
|
340 definition |
|
341 "rec_mod = CN rec_minus [Id 2 0, CN rec_mult [Id 2 1, rec_quo]]" |
|
342 |
|
343 |
|
344 section {* Prime Numbers *} |
|
345 |
|
346 definition |
|
347 "rec_prime = |
|
348 (let conj1 = CN rec_less [constn 1, Id 1 0] in |
|
349 let disj = CN rec_disj [CN rec_eq [Id 2 0, constn 1], rec_eq] in |
|
350 let imp = CN rec_imp [rec_dvd, disj] in |
|
351 let conj2 = CN (rec_all1 imp) [Id 1 0, Id 1 0] in |
|
352 CN rec_conj [conj1, conj2])" |
|
353 |
|
354 |
|
355 section {* Correctness of Recursive Functions *} |
|
356 |
|
357 lemma constn_lemma [simp]: |
|
358 "rec_eval (constn n) xs = n" |
|
359 by (induct n) (simp_all) |
|
360 |
|
361 lemma swap_lemma [simp]: |
|
362 "rec_eval (rec_swap f) [x, y] = rec_eval f [y, x]" |
|
363 by (simp add: rec_swap_def) |
|
364 |
|
365 lemma add_lemma [simp]: |
|
366 "rec_eval rec_add [x, y] = x + y" |
|
367 by (induct x) (simp_all add: rec_add_def) |
|
368 |
|
369 lemma mult_lemma [simp]: |
|
370 "rec_eval rec_mult [x, y] = x * y" |
|
371 by (induct x) (simp_all add: rec_mult_def) |
|
372 |
|
373 lemma power_lemma [simp]: |
|
374 "rec_eval rec_power [x, y] = x ^ y" |
|
375 by (induct y) (simp_all add: rec_power_def) |
|
376 |
|
377 lemma fact_lemma [simp]: |
|
378 "rec_eval rec_fact [x] = fact x" |
|
379 by (induct x) (simp_all add: rec_fact_def) |
|
380 |
|
381 lemma pred_lemma [simp]: |
|
382 "rec_eval rec_pred [x] = x - 1" |
|
383 by (induct x) (simp_all add: rec_pred_def) |
|
384 |
|
385 lemma minus_lemma [simp]: |
|
386 "rec_eval rec_minus [x, y] = x - y" |
|
387 by (induct y) (simp_all add: rec_minus_def) |
|
388 |
|
389 lemma sign_lemma [simp]: |
|
390 "rec_eval rec_sign [x] = (if x = 0 then 0 else 1)" |
|
391 by (simp add: rec_sign_def) |
|
392 |
|
393 lemma not_lemma [simp]: |
|
394 "rec_eval rec_not [x] = (if x = 0 then 1 else 0)" |
|
395 by (simp add: rec_not_def) |
|
396 |
|
397 lemma eq_lemma [simp]: |
|
398 "rec_eval rec_eq [x, y] = (if x = y then 1 else 0)" |
|
399 by (simp add: rec_eq_def) |
|
400 |
|
401 lemma noteq_lemma [simp]: |
|
402 "rec_eval rec_noteq [x, y] = (if x \<noteq> y then 1 else 0)" |
|
403 by (simp add: rec_noteq_def) |
|
404 |
|
405 lemma conj_lemma [simp]: |
|
406 "rec_eval rec_conj [x, y] = (if x = 0 \<or> y = 0 then 0 else 1)" |
|
407 by (simp add: rec_conj_def) |
|
408 |
|
409 lemma disj_lemma [simp]: |
|
410 "rec_eval rec_disj [x, y] = (if x = 0 \<and> y = 0 then 0 else 1)" |
|
411 by (simp add: rec_disj_def) |
|
412 |
|
413 lemma imp_lemma [simp]: |
|
414 "rec_eval rec_imp [x, y] = (if 0 < x \<and> y = 0 then 0 else 1)" |
|
415 by (simp add: rec_imp_def) |
|
416 |
|
417 lemma less_lemma [simp]: |
|
418 "rec_eval rec_less [x, y] = (if x < y then 1 else 0)" |
|
419 by (simp add: rec_less_def) |
|
420 |
|
421 lemma le_lemma [simp]: |
|
422 "rec_eval rec_le [x, y] = (if (x \<le> y) then 1 else 0)" |
|
423 by(simp add: rec_le_def) |
|
424 |
|
425 lemma ifz_lemma [simp]: |
|
426 "rec_eval rec_ifz [z, x, y] = (if z = 0 then x else y)" |
|
427 by (case_tac z) (simp_all add: rec_ifz_def) |
|
428 |
|
429 lemma if_lemma [simp]: |
|
430 "rec_eval rec_if [z, x, y] = (if 0 < z then x else y)" |
|
431 by (simp add: rec_if_def) |
|
432 |
|
433 lemma sigma1_lemma [simp]: |
|
434 shows "rec_eval (rec_sigma1 f) [x, y] = (\<Sum> z \<le> x. (rec_eval f) [z, y])" |
|
435 by (induct x) (simp_all add: rec_sigma1_def) |
|
436 |
|
437 lemma sigma2_lemma [simp]: |
|
438 shows "rec_eval (rec_sigma2 f) [x, y1, y2] = (\<Sum> z \<le> x. (rec_eval f) [z, y1, y2])" |
|
439 by (induct x) (simp_all add: rec_sigma2_def) |
|
440 |
|
441 lemma accum1_lemma [simp]: |
|
442 shows "rec_eval (rec_accum1 f) [x, y] = (\<Prod> z \<le> x. (rec_eval f) [z, y])" |
|
443 by (induct x) (simp_all add: rec_accum1_def) |
|
444 |
|
445 lemma accum2_lemma [simp]: |
|
446 shows "rec_eval (rec_accum2 f) [x, y1, y2] = (\<Prod> z \<le> x. (rec_eval f) [z, y1, y2])" |
|
447 by (induct x) (simp_all add: rec_accum2_def) |
|
448 |
|
449 lemma ex1_lemma [simp]: |
|
450 "rec_eval (rec_ex1 f) [x, y] = (if (\<exists>z \<le> x. 0 < rec_eval f [z, y]) then 1 else 0)" |
|
451 by (simp add: rec_ex1_def) |
|
452 |
|
453 lemma ex2_lemma [simp]: |
|
454 "rec_eval (rec_ex2 f) [x, y1, y2] = (if (\<exists>z \<le> x. 0 < rec_eval f [z, y1, y2]) then 1 else 0)" |
|
455 by (simp add: rec_ex2_def) |
|
456 |
|
457 lemma all1_lemma [simp]: |
|
458 "rec_eval (rec_all1 f) [x, y] = (if (\<forall>z \<le> x. 0 < rec_eval f [z, y]) then 1 else 0)" |
|
459 by (simp add: rec_all1_def) |
|
460 |
|
461 lemma all2_lemma [simp]: |
|
462 "rec_eval (rec_all2 f) [x, y1, y2] = (if (\<forall>z \<le> x. 0 < rec_eval f [z, y1, y2]) then 1 else 0)" |
|
463 by (simp add: rec_all2_def) |
|
464 |
|
465 |
|
466 lemma dvd_alt_def: |
|
467 fixes x y k:: nat |
|
468 shows "(x dvd y) = (\<exists> k \<le> y. y = x * k)" |
|
469 apply(auto simp add: dvd_def) |
|
470 apply(case_tac x) |
|
471 apply(auto) |
|
472 done |
|
473 |
|
474 lemma dvd_lemma [simp]: |
|
475 "rec_eval rec_dvd [x, y] = (if x dvd y then 1 else 0)" |
|
476 unfolding dvd_alt_def |
|
477 by (auto simp add: rec_dvd_def) |
|
478 |
|
479 fun Quo where |
|
480 "Quo x 0 = 0" |
|
481 | "Quo x (Suc y) = (if (Suc y = x * (Suc (Quo x y))) then Suc (Quo x y) else Quo x y)" |
|
482 |
|
483 lemma Quo0: |
|
484 shows "Quo 0 y = 0" |
|
485 apply(induct y) |
|
486 apply(auto) |
|
487 done |
|
488 |
|
489 lemma Quo1: |
|
490 "x * (Quo x y) \<le> y" |
|
491 by (induct y) (simp_all) |
|
492 |
|
493 lemma Quo2: |
|
494 "b * (Quo b a) + a mod b = a" |
|
495 by (induct a) (auto simp add: mod_Suc) |
|
496 |
|
497 lemma Quo3: |
|
498 "n * (Quo n m) = m - m mod n" |
|
499 using Quo2[of n m] by (auto) |
|
500 |
|
501 lemma Quo4: |
|
502 assumes h: "0 < x" |
|
503 shows "y < x + x * Quo x y" |
|
504 proof - |
|
505 have "x - (y mod x) > 0" using mod_less_divisor assms by auto |
|
506 then have "y < y + (x - (y mod x))" by simp |
|
507 then have "y < x + (y - (y mod x))" by simp |
|
508 then show "y < x + x * (Quo x y)" by (simp add: Quo3) |
|
509 qed |
|
510 |
|
511 lemma Quo_div: |
|
512 shows "Quo x y = y div x" |
|
513 apply(case_tac "x = 0") |
|
514 apply(simp add: Quo0) |
|
515 apply(subst split_div_lemma[symmetric]) |
|
516 apply(auto intro: Quo1 Quo4) |
|
517 done |
|
518 |
|
519 lemma Quo_rec_quo: |
|
520 shows "rec_eval rec_quo [y, x] = Quo x y" |
|
521 by (induct y) (simp_all add: rec_quo_def) |
|
522 |
|
523 lemma quo_lemma [simp]: |
|
524 shows "rec_eval rec_quo [y, x] = y div x" |
|
525 by (simp add: Quo_div Quo_rec_quo) |
|
526 |
|
527 lemma rem_lemma [simp]: |
|
528 shows "rec_eval rec_mod [y, x] = y mod x" |
|
529 by (simp add: rec_mod_def mod_div_equality' nat_mult_commute) |
|
530 |
|
531 |
|
532 section {* Prime Numbers *} |
|
533 |
|
534 lemma prime_alt_def: |
|
535 fixes p::nat |
|
536 shows "prime p = (1 < p \<and> (\<forall>m \<le> p. m dvd p \<longrightarrow> m = 1 \<or> m = p))" |
|
537 apply(auto simp add: prime_nat_def dvd_def) |
|
538 apply(drule_tac x="k" in spec) |
|
539 apply(auto) |
|
540 done |
|
541 |
|
542 lemma prime_lemma [simp]: |
|
543 "rec_eval rec_prime [x] = (if prime x then 1 else 0)" |
|
544 by (auto simp add: rec_prime_def Let_def prime_alt_def) |
|
545 |
|
546 section {* Bounded Maximisation *} |
|
547 |
|
548 fun BMax_rec where |
|
549 "BMax_rec R 0 = 0" |
|
550 | "BMax_rec R (Suc n) = (if R (Suc n) then (Suc n) else BMax_rec R n)" |
|
551 |
|
552 definition BMax_set :: "(nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat" |
|
553 where "BMax_set R x = Max ({z. z \<le> x \<and> R z} \<union> {0})" |
|
554 |
|
555 lemma BMax_rec_eq1: |
|
556 "BMax_rec R x = (GREATEST z. (R z \<and> z \<le> x) \<or> z = 0)" |
|
557 apply(induct x) |
|
558 apply(auto intro: Greatest_equality Greatest_equality[symmetric]) |
|
559 apply(simp add: le_Suc_eq) |
|
560 by metis |
|
561 |
|
562 lemma BMax_rec_eq2: |
|
563 "BMax_rec R x = Max ({z. z \<le> x \<and> R z} \<union> {0})" |
|
564 apply(induct x) |
|
565 apply(auto intro: Max_eqI Max_eqI[symmetric]) |
|
566 apply(simp add: le_Suc_eq) |
|
567 by metis |
|
568 |
|
569 lemma BMax_rec_eq3: |
|
570 "BMax_rec R x = Max (Set.filter (\<lambda>z. R z) {..x} \<union> {0})" |
|
571 by (simp add: BMax_rec_eq2 Set.filter_def) |
|
572 |
|
573 definition |
|
574 "rec_max1 f = PR (constn 0) (CN rec_ifz [CN f [CN S [Id 3 0], Id 3 2], CN S [Id 4 0], Id 4 1])" |
|
575 |
|
576 lemma max1_lemma [simp]: |
|
577 "rec_eval (rec_max1 f) [x, y] = BMax_rec (\<lambda>u. rec_eval f [u, y] = 0) x" |
|
578 by (induct x) (simp_all add: rec_max1_def) |
|
579 |
|
580 definition |
|
581 "rec_max2 f = PR (constn 0) (CN rec_ifz [CN f [CN S [Id 4 0], Id 4 2, Id 4 3], CN S [Id 4 0], Id 4 1])" |
|
582 |
|
583 lemma max2_lemma [simp]: |
|
584 "rec_eval (rec_max2 f) [x, y1, y2] = BMax_rec (\<lambda>u. rec_eval f [u, y1, y2] = 0) x" |
|
585 by (induct x) (simp_all add: rec_max2_def) |
|
586 |
|
587 section {* Encodings using Cantor's pairing function *} |
|
588 |
|
589 text {* |
|
590 We use Cantor's pairing function from Nat_Bijection. |
|
591 However, we need to prove that the formulation of the |
|
592 decoding function there is recursive. For this we first |
|
593 prove that we can extract the maximal triangle number |
|
594 using @{term prod_decode}. |
|
595 *} |
|
596 |
|
597 abbreviation Max_triangle_aux where |
|
598 "Max_triangle_aux k z \<equiv> fst (prod_decode_aux k z) + snd (prod_decode_aux k z)" |
|
599 |
|
600 abbreviation Max_triangle where |
|
601 "Max_triangle z \<equiv> Max_triangle_aux 0 z" |
|
602 |
|
603 abbreviation |
|
604 "pdec1 z \<equiv> fst (prod_decode z)" |
|
605 |
|
606 abbreviation |
|
607 "pdec2 z \<equiv> snd (prod_decode z)" |
|
608 |
|
609 abbreviation |
|
610 "penc m n \<equiv> prod_encode (m, n)" |
|
611 |
|
612 lemma fst_prod_decode: |
|
613 "pdec1 z = z - triangle (Max_triangle z)" |
|
614 by (subst (3) prod_decode_inverse[symmetric]) |
|
615 (simp add: prod_encode_def prod_decode_def split: prod.split) |
|
616 |
|
617 lemma snd_prod_decode: |
|
618 "pdec2 z = Max_triangle z - pdec1 z" |
|
619 by (simp only: prod_decode_def) |
|
620 |
|
621 lemma le_triangle: |
|
622 "m \<le> triangle (n + m)" |
|
623 by (induct_tac m) (simp_all) |
|
624 |
|
625 lemma Max_triangle_triangle_le: |
|
626 "triangle (Max_triangle z) \<le> z" |
|
627 by (subst (9) prod_decode_inverse[symmetric]) |
|
628 (simp add: prod_decode_def prod_encode_def split: prod.split) |
|
629 |
|
630 lemma Max_triangle_le: |
|
631 "Max_triangle z \<le> z" |
|
632 proof - |
|
633 have "Max_triangle z \<le> triangle (Max_triangle z)" |
|
634 using le_triangle[of _ 0, simplified] by simp |
|
635 also have "... \<le> z" by (rule Max_triangle_triangle_le) |
|
636 finally show "Max_triangle z \<le> z" . |
|
637 qed |
|
638 |
|
639 lemma w_aux: |
|
640 "Max_triangle (triangle k + m) = Max_triangle_aux k m" |
|
641 by (simp add: prod_decode_def[symmetric] prod_decode_triangle_add) |
|
642 |
|
643 lemma y_aux: "y \<le> Max_triangle_aux y k" |
|
644 apply(induct k arbitrary: y rule: nat_less_induct) |
|
645 apply(subst (1 2) prod_decode_aux.simps) |
|
646 apply(simp) |
|
647 apply(rule impI) |
|
648 apply(drule_tac x="n - Suc y" in spec) |
|
649 apply(drule mp) |
|
650 apply(auto)[1] |
|
651 apply(drule_tac x="Suc y" in spec) |
|
652 apply(erule Suc_leD) |
|
653 done |
|
654 |
|
655 lemma Max_triangle_greatest: |
|
656 "Max_triangle z = (GREATEST k. (triangle k \<le> z \<and> k \<le> z) \<or> k = 0)" |
|
657 apply(rule Greatest_equality[symmetric]) |
|
658 apply(rule disjI1) |
|
659 apply(rule conjI) |
|
660 apply(rule Max_triangle_triangle_le) |
|
661 apply(rule Max_triangle_le) |
|
662 apply(erule disjE) |
|
663 apply(erule conjE) |
|
664 apply(subst (asm) (1) le_iff_add) |
|
665 apply(erule exE) |
|
666 apply(clarify) |
|
667 apply(simp only: w_aux) |
|
668 apply(rule y_aux) |
|
669 apply(simp) |
|
670 done |
|
671 |
|
672 definition |
|
673 "rec_triangle = CN rec_quo [CN rec_mult [Id 1 0, S], constn 2]" |
|
674 |
|
675 lemma triangle_lemma [simp]: |
|
676 "rec_eval rec_triangle [x] = triangle x" |
|
677 by (simp add: rec_triangle_def triangle_def) |
|
678 |
|
679 definition |
|
680 "rec_max_triangle = |
|
681 (let cond = CN rec_not [CN rec_le [CN rec_triangle [Id 2 0], Id 2 1]] in |
|
682 CN (rec_max1 cond) [Id 1 0, Id 1 0])" |
|
683 |
|
684 lemma max_triangle_lemma [simp]: |
|
685 "rec_eval rec_max_triangle [x] = Max_triangle x" |
|
686 by (simp add: Max_triangle_greatest rec_max_triangle_def Let_def BMax_rec_eq1) |
|
687 |
|
688 definition |
|
689 "rec_penc = CN rec_add [CN rec_triangle [CN rec_add [Id 2 0, Id 2 1]], Id 2 0]" |
|
690 |
|
691 definition |
|
692 "rec_pdec1 = CN rec_minus [Id 1 0, CN rec_triangle [CN rec_max_triangle [Id 1 0]]]" |
|
693 |
|
694 definition |
|
695 "rec_pdec2 = CN rec_minus [CN rec_max_triangle [Id 1 0], CN rec_pdec1 [Id 1 0]]" |
|
696 |
|
697 lemma pdec1_lemma [simp]: |
|
698 "rec_eval rec_pdec1 [z] = pdec1 z" |
|
699 by (simp add: rec_pdec1_def fst_prod_decode) |
|
700 |
|
701 lemma pdec2_lemma [simp]: |
|
702 "rec_eval rec_pdec2 [z] = pdec2 z" |
|
703 by (simp add: rec_pdec2_def snd_prod_decode) |
|
704 |
|
705 lemma penc_lemma [simp]: |
|
706 "rec_eval rec_penc [m, n] = penc m n" |
|
707 by (simp add: rec_penc_def prod_encode_def) |
|
708 |
|
709 fun |
|
710 lenc :: "nat list \<Rightarrow> nat" |
|
711 where |
|
712 "lenc [] = 0" |
|
713 | "lenc (x # xs) = penc (Suc x) (lenc xs)" |
|
714 |
|
715 fun |
|
716 ldec :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
|
717 where |
|
718 "ldec z 0 = (pdec1 z) - 1" |
|
719 | "ldec z (Suc n) = ldec (pdec2 z) n" |
|
720 |
|
721 lemma pdec_zero_simps [simp]: |
|
722 "pdec1 0 = 0" |
|
723 "pdec2 0 = 0" |
|
724 by (simp_all add: prod_decode_def prod_decode_aux.simps) |
|
725 |
|
726 lemma w: |
|
727 "ldec 0 n = 0" |
|
728 by (induct n) (simp_all add: prod_decode_def prod_decode_aux.simps) |
|
729 |
|
730 lemma list_encode_inverse: |
|
731 "ldec (lenc xs) n = (if n < length xs then xs ! n else 0)" |
|
732 apply(induct xs arbitrary: n rule: lenc.induct) |
|
733 apply(simp_all add: w) |
|
734 apply(case_tac n) |
|
735 apply(simp_all) |
|
736 done |
|
737 |
|
738 fun within :: "nat \<Rightarrow> nat \<Rightarrow> bool" where |
|
739 "within z 0 = (0 < z)" |
|
740 | "within z (Suc n) = within (pdec2 z) n" |
|
741 |
|
742 |
|
743 section {* Discrete Logarithms *} |
|
744 |
|
745 definition |
|
746 "rec_lg = |
|
747 (let calc = CN rec_not [CN rec_le [CN rec_power [Id 3 2, Id 3 0], Id 3 1]] in |
|
748 let max = CN (rec_max2 calc) [Id 2 0, Id 2 0, Id 2 1] in |
|
749 let cond = CN rec_conj [CN rec_less [constn 1, Id 2 0], CN rec_less [constn 1, Id 2 1]] |
|
750 in CN rec_ifz [cond, Z, max])" |
|
751 |
|
752 definition |
|
753 "Lg x y = (if 1 < x \<and> 1 < y then BMax_rec (\<lambda>u. y ^ u \<le> x) x else 0)" |
|
754 |
|
755 lemma lg_lemma [simp]: |
|
756 "rec_eval rec_lg [x, y] = Lg x y" |
|
757 by (simp add: rec_lg_def Lg_def Let_def) |
|
758 |
|
759 definition |
|
760 "Lo x y = (if 1 < x \<and> 1 < y then BMax_rec (\<lambda>u. x mod (y ^ u) = 0) x else 0)" |
|
761 |
|
762 definition |
|
763 "rec_lo = |
|
764 (let calc = CN rec_noteq [CN rec_mod [Id 3 1, CN rec_power [Id 3 2, Id 3 0]], Z] in |
|
765 let max = CN (rec_max2 calc) [Id 2 0, Id 2 0, Id 2 1] in |
|
766 let cond = CN rec_conj [CN rec_less [constn 1, Id 2 0], CN rec_less [constn 1, Id 2 1]] |
|
767 in CN rec_ifz [cond, Z, max])" |
|
768 |
|
769 lemma lo_lemma [simp]: |
|
770 "rec_eval rec_lo [x, y] = Lo x y" |
|
771 by (simp add: rec_lo_def Lo_def Let_def) |
|
772 |
|
773 section {* NextPrime number function *} |
|
774 |
|
775 text {* |
|
776 @{text "NextPrime x"} returns the first prime number after @{text "x"}; |
|
777 @{text "Pi i"} returns the i-th prime number. *} |
|
778 |
|
779 definition NextPrime ::"nat \<Rightarrow> nat" |
|
780 where |
|
781 "NextPrime x = (LEAST y. y \<le> Suc (fact x) \<and> x < y \<and> prime y)" |
|
782 |
|
783 definition rec_nextprime :: "recf" |
|
784 where |
|
785 "rec_nextprime = (let conj1 = CN rec_le [Id 2 0, CN S [CN rec_fact [Id 2 1]]] in |
|
786 let conj2 = CN rec_less [Id 2 1, Id 2 0] in |
|
787 let conj3 = CN rec_prime [Id 2 0] in |
|
788 let conjs = CN rec_conj [CN rec_conj [conj2, conj1], conj3] |
|
789 in MN (CN rec_not [conjs]))" |
|
790 |
|
791 lemma nextprime_lemma [simp]: |
|
792 "rec_eval rec_nextprime [x] = NextPrime x" |
|
793 by (simp add: rec_nextprime_def Let_def NextPrime_def) |
|
794 |
|
795 lemma NextPrime_simps [simp]: |
|
796 shows "NextPrime 2 = 3" |
|
797 and "NextPrime 3 = 5" |
|
798 apply(simp_all add: NextPrime_def) |
|
799 apply(rule Least_equality) |
|
800 apply(auto) |
|
801 apply(eval) |
|
802 apply(rule Least_equality) |
|
803 apply(auto) |
|
804 apply(eval) |
|
805 apply(case_tac "y = 4") |
|
806 apply(auto) |
|
807 done |
|
808 |
|
809 fun Pi :: "nat \<Rightarrow> nat" |
|
810 where |
|
811 "Pi 0 = 2" | |
|
812 "Pi (Suc x) = NextPrime (Pi x)" |
|
813 |
|
814 lemma Pi_simps [simp]: |
|
815 shows "Pi 1 = 3" |
|
816 and "Pi 2 = 5" |
|
817 using NextPrime_simps |
|
818 by(simp_all add: numeral_eq_Suc One_nat_def) |
|
819 |
|
820 definition |
|
821 "rec_pi = PR (constn 2) (CN rec_nextprime [Id 2 1])" |
|
822 |
|
823 lemma pi_lemma [simp]: |
|
824 "rec_eval rec_pi [x] = Pi x" |
|
825 by (induct x) (simp_all add: rec_pi_def) |
|
826 |
|
827 end |
|
828 |
|