71 where |
69 where |
72 "Newstat m q r = (if q \<noteq> 0 then Entry m (4 * (q - 1) + 2 * Scan r + 1) else 0)" |
70 "Newstat m q r = (if q \<noteq> 0 then Entry m (4 * (q - 1) + 2 * Scan r + 1) else 0)" |
73 |
71 |
74 fun Trpl :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" |
72 fun Trpl :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" |
75 where |
73 where |
76 "Trpl p q r = (Pi 0) ^ p * (Pi 1) ^ q * (Pi 2) ^ r" |
74 "Trpl p q r = list_encode [p, q, r]" |
77 |
75 |
78 fun Left where |
76 fun Left where |
79 "Left c = Lo c (Pi 0)" |
77 "Left c = list_decode c ! 0" |
80 |
78 |
81 fun Right where |
79 fun Right where |
82 "Right c = Lo c (Pi 2)" |
80 "Right c = list_decode c ! 1" |
83 |
81 |
84 fun Stat where |
82 fun Stat where |
85 "Stat c = Lo c (Pi 1)" |
83 "Stat c = list_decode c ! 2" |
86 |
84 |
87 lemma mod_dvd_simp: |
85 lemma mod_dvd_simp: |
88 "(x mod y = (0::nat)) = (y dvd x)" |
86 "(x mod y = (0::nat)) = (y dvd x)" |
89 by(auto simp add: dvd_def) |
87 by(auto simp add: dvd_def) |
90 |
|
91 lemma Trpl_Left [simp]: |
|
92 "Left (Trpl p q r) = p" |
|
93 apply(simp) |
|
94 apply(subst Lo_def) |
|
95 apply(subst dvd_eq_mod_eq_0[symmetric]) |
|
96 apply(simp) |
|
97 apply(auto) |
|
98 thm Lo_def |
|
99 thm mod_dvd_simp |
|
100 apply(simp add: left.simps trpl.simps lo.simps |
|
101 loR.simps mod_dvd_simp, auto simp: conf_decode1) |
|
102 apply(case_tac "Pi 0 ^ l * Pi (Suc 0) ^ st * Pi (Suc (Suc 0)) ^ r", |
|
103 auto) |
|
104 apply(erule_tac x = l in allE, auto) |
|
105 |
88 |
106 |
89 |
107 fun Inpt :: "nat \<Rightarrow> nat list \<Rightarrow> nat" |
90 fun Inpt :: "nat \<Rightarrow> nat list \<Rightarrow> nat" |
108 where |
91 where |
109 "Inpt m xs = Trpl 0 1 (Strt xs)" |
92 "Inpt m xs = Trpl 0 1 (Strt xs)" |
310 let add2 = CN S [CN rec_mult [constn 2, CN rec_scan [Id 3 2]]] in |
293 let add2 = CN S [CN rec_mult [constn 2, CN rec_scan [Id 3 2]]] in |
311 let entry = CN rec_entry [Id 3 0, CN rec_add [add1, add2]] |
294 let entry = CN rec_entry [Id 3 0, CN rec_add [add1, add2]] |
312 in CN rec_if [Id 3 1, entry, Z])" |
295 in CN rec_if [Id 3 1, entry, Z])" |
313 |
296 |
314 definition |
297 definition |
315 "rec_trpl = CN rec_mult [CN rec_mult |
298 "rec_trpl = CN rec_penc [CN rec_penc [Id 3 0, Id 3 1], Id 3 2]" |
316 [CN rec_power [constn (Pi 0), Id 3 0], |
|
317 CN rec_power [constn (Pi 1), Id 3 1]], |
|
318 CN rec_power [constn (Pi 2), Id 3 2]]" |
|
319 |
299 |
320 definition |
300 definition |
321 "rec_left = CN rec_lo [Id 1 0, constn (Pi 0)]" |
301 "rec_left = rec_pdec1" |
322 |
302 |
323 definition |
303 definition |
324 "rec_right = CN rec_lo [Id 1 0, constn (Pi 2)]" |
304 "rec_right = CN rec_pdec2 [rec_pdec1]" |
325 |
305 |
326 definition |
306 definition |
327 "rec_stat = CN rec_lo [Id 1 0, constn (Pi 1)]" |
307 "rec_stat = CN rec_pdec2 [rec_pdec2]" |
328 |
308 |
329 definition |
309 definition |
330 "rec_newconf = (let act = CN rec_actn [Id 2 0, CN rec_stat [Id 2 1], CN rec_right [Id 2 1]] in |
310 "rec_newconf = (let act = CN rec_actn [Id 2 0, CN rec_stat [Id 2 1], CN rec_right [Id 2 1]] in |
331 let left = CN rec_left [Id 2 1] in |
311 let left = CN rec_left [Id 2 1] in |
332 let right = CN rec_right [Id 2 1] in |
312 let right = CN rec_right [Id 2 1] in |
410 "rec_eval rec_newstat [m, q, r] = Newstat m q r" |
390 "rec_eval rec_newstat [m, q, r] = Newstat m q r" |
411 by (simp add: rec_newstat_def) |
391 by (simp add: rec_newstat_def) |
412 |
392 |
413 lemma trpl_lemma [simp]: |
393 lemma trpl_lemma [simp]: |
414 "rec_eval rec_trpl [p, q, r] = Trpl p q r" |
394 "rec_eval rec_trpl [p, q, r] = Trpl p q r" |
415 by (simp add: rec_trpl_def) |
395 apply(simp) |
|
396 apply (simp add: rec_trpl_def) |
416 |
397 |
417 lemma left_lemma [simp]: |
398 lemma left_lemma [simp]: |
418 "rec_eval rec_left [c] = Left c" |
399 "rec_eval rec_left [c] = Left c" |
419 by(simp add: rec_left_def) |
400 by(simp add: rec_left_def) |
420 |
401 |