equal
deleted
inserted
replaced
2 imports Main |
2 imports Main |
3 "~~/src/HOL/Library/Nat_Bijection" |
3 "~~/src/HOL/Library/Nat_Bijection" |
4 "~~/src/HOL/Library/Discrete" |
4 "~~/src/HOL/Library/Discrete" |
5 begin |
5 begin |
6 |
6 |
|
7 |
|
8 text{* |
|
9 A more streamlined and cleaned-up version of Recursive |
|
10 Functions following |
|
11 |
|
12 A Course in Formal Languages, Automata and Groups |
|
13 I. M. Chiswell |
|
14 |
|
15 and |
|
16 |
|
17 Lecture on Undecidability |
|
18 Michael M. Wolf |
|
19 *} |
|
20 |
7 declare One_nat_def[simp del] |
21 declare One_nat_def[simp del] |
8 |
22 |
9 (* |
|
10 some definitions from |
|
11 |
|
12 A Course in Formal Languages, Automata and Groups |
|
13 I M Chiswell |
|
14 |
|
15 and |
|
16 |
|
17 Lecture on undecidability |
|
18 Michael M. Wolf |
|
19 *) |
|
20 |
23 |
21 lemma if_zero_one [simp]: |
24 lemma if_zero_one [simp]: |
22 "(if P then 1 else 0) = (0::nat) \<longleftrightarrow> \<not> P" |
25 "(if P then 1 else 0) = (0::nat) \<longleftrightarrow> \<not> P" |
23 "(0::nat) < (if P then 1 else 0) = P" |
26 "(0::nat) < (if P then 1 else 0) = P" |
24 "(if P then 0 else 1) = (if \<not>P then 1 else (0::nat))" |
27 "(if P then 0 else 1) = (if \<not>P then 1 else (0::nat))" |
246 |
249 |
247 definition |
250 definition |
248 "rec_fact = CN rec_fact_aux [Id 1 0, Id 1 0]" |
251 "rec_fact = CN rec_fact_aux [Id 1 0, Id 1 0]" |
249 |
252 |
250 definition |
253 definition |
251 "rec_predi = CN (PR Z (Id 3 0)) [Id 1 0, Id 1 0]" |
254 "rec_predecessor = CN (PR Z (Id 3 0)) [Id 1 0, Id 1 0]" |
252 |
255 |
253 definition |
256 definition |
254 "rec_minus = rec_swap (PR (Id 1 0) (CN rec_predi [Id 3 1]))" |
257 "rec_minus = rec_swap (PR (Id 1 0) (CN rec_predecessor [Id 3 1]))" |
255 |
258 |
256 lemma constn_lemma [simp]: |
259 lemma constn_lemma [simp]: |
257 "rec_eval (constn n) xs = n" |
260 "rec_eval (constn n) xs = n" |
258 by (induct n) (simp_all) |
261 by (induct n) (simp_all) |
259 |
262 |
280 lemma fact_lemma [simp]: |
283 lemma fact_lemma [simp]: |
281 "rec_eval rec_fact [x] = fact x" |
284 "rec_eval rec_fact [x] = fact x" |
282 by (simp add: rec_fact_def) |
285 by (simp add: rec_fact_def) |
283 |
286 |
284 lemma pred_lemma [simp]: |
287 lemma pred_lemma [simp]: |
285 "rec_eval rec_predi [x] = x - 1" |
288 "rec_eval rec_predecessor [x] = x - 1" |
286 by (induct x) (simp_all add: rec_predi_def) |
289 by (induct x) (simp_all add: rec_predecessor_def) |
287 |
290 |
288 lemma minus_lemma [simp]: |
291 lemma minus_lemma [simp]: |
289 "rec_eval rec_minus [x, y] = x - y" |
292 "rec_eval rec_minus [x, y] = x - y" |
290 by (induct y) (simp_all add: rec_minus_def) |
293 by (induct y) (simp_all add: rec_minus_def) |
291 |
294 |
816 where |
819 where |
817 "rec_lenc [] = Z" |
820 "rec_lenc [] = Z" |
818 | "rec_lenc (f # fs) = CN rec_penc [CN S [f], rec_lenc fs]" |
821 | "rec_lenc (f # fs) = CN rec_penc [CN S [f], rec_lenc fs]" |
819 |
822 |
820 definition |
823 definition |
821 "rec_ldec = CN rec_predi [CN rec_pdec1 [rec_swap (rec_iter rec_pdec2)]]" |
824 "rec_ldec = CN rec_predecessor [CN rec_pdec1 [rec_swap (rec_iter rec_pdec2)]]" |
822 |
825 |
823 definition |
826 definition |
824 "rec_inside = CN rec_less [Z, rec_swap (rec_iter rec_pdec2)]" |
827 "rec_inside = CN rec_less [Z, rec_swap (rec_iter rec_pdec2)]" |
825 |
828 |
826 definition |
829 definition |
827 "rec_enclen = CN (rec_max1 (CN rec_not [CN rec_inside [Id 2 1, CN rec_predi [Id 2 0]]])) [Id 1 0, Id 1 0]" |
830 "rec_enclen = CN (rec_max1 (CN rec_not [CN rec_inside [Id 2 1, CN rec_predecessor [Id 2 0]]])) [Id 1 0, Id 1 0]" |
828 |
831 |
829 lemma ldec_iter: |
832 lemma ldec_iter: |
830 "ldec z n = pdec1 (Iter pdec2 n z) - 1" |
833 "ldec z n = pdec1 (Iter pdec2 n z) - 1" |
831 by (induct n arbitrary: z) (simp | subst Iter_comm)+ |
834 by (induct n arbitrary: z) (simp | subst Iter_comm)+ |
832 |
835 |