324 definition |
324 definition |
325 "rec_ex2 f = CN rec_sign [rec_sigma2 f]" |
325 "rec_ex2 f = CN rec_sign [rec_sigma2 f]" |
326 |
326 |
327 text {* Dvd, Quotient, Modulo *} |
327 text {* Dvd, Quotient, Modulo *} |
328 |
328 |
|
329 (* FIXME: probably all not needed *) |
329 definition |
330 definition |
330 "rec_dvd = |
331 "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 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 |
333 definition |
334 definition |
347 |
348 |
348 fun Iter where |
349 fun Iter where |
349 "Iter f 0 = id" |
350 "Iter f 0 = id" |
350 | "Iter f (Suc n) = f \<circ> (Iter f n)" |
351 | "Iter f (Suc n) = f \<circ> (Iter f n)" |
351 |
352 |
352 lemma iter_comm: |
353 lemma Iter_comm: |
353 "(Iter f n) (f x) = f ((Iter f n) x)" |
354 "(Iter f n) (f x) = f ((Iter f n) x)" |
354 by (induct n) (simp_all) |
355 by (induct n) (simp_all) |
355 |
356 |
356 lemma iter_lemma [simp]: |
357 lemma iter_lemma [simp]: |
357 "rec_eval (rec_iter f) [n, x] = Iter (\<lambda>x. rec_eval f [x]) n x" |
358 "rec_eval (rec_iter f) [n, x] = Iter (\<lambda>x. rec_eval f [x]) n x" |
695 |
696 |
696 lemma penc_lemma [simp]: |
697 lemma penc_lemma [simp]: |
697 "rec_eval rec_penc [m, n] = penc m n" |
698 "rec_eval rec_penc [m, n] = penc m n" |
698 by (simp add: rec_penc_def prod_encode_def) |
699 by (simp add: rec_penc_def prod_encode_def) |
699 |
700 |
|
701 text {* encoding and decoding of lists of natural numbers *} |
|
702 |
700 fun |
703 fun |
701 lenc :: "nat list \<Rightarrow> nat" |
704 lenc :: "nat list \<Rightarrow> nat" |
702 where |
705 where |
703 "lenc [] = 0" |
706 "lenc [] = 0" |
704 | "lenc (x # xs) = penc (Suc x) (lenc xs)" |
707 | "lenc (x # xs) = penc (Suc x) (lenc xs)" |
712 lemma pdec_zero_simps [simp]: |
715 lemma pdec_zero_simps [simp]: |
713 "pdec1 0 = 0" |
716 "pdec1 0 = 0" |
714 "pdec2 0 = 0" |
717 "pdec2 0 = 0" |
715 by (simp_all add: prod_decode_def prod_decode_aux.simps) |
718 by (simp_all add: prod_decode_def prod_decode_aux.simps) |
716 |
719 |
717 lemma w: |
720 lemma ldec_zero: |
718 "ldec 0 n = 0" |
721 "ldec 0 n = 0" |
719 by (induct n) (simp_all add: prod_decode_def prod_decode_aux.simps) |
722 by (induct n) (simp_all add: prod_decode_def prod_decode_aux.simps) |
720 |
723 |
721 lemma list_encode_inverse: |
724 lemma list_encode_inverse: |
722 "ldec (lenc xs) n = (if n < length xs then xs ! n else 0)" |
725 "ldec (lenc xs) n = (if n < length xs then xs ! n else 0)" |
723 apply(induct xs arbitrary: n rule: lenc.induct) |
726 by (induct xs arbitrary: n rule: lenc.induct) |
724 apply(simp_all add: w) |
727 (auto simp add: ldec_zero nth_Cons split: nat.splits) |
725 apply(case_tac n) |
728 |
726 apply(simp_all) |
|
727 done |
|
728 |
729 |
729 lemma lenc_length_le: |
730 lemma lenc_length_le: |
730 "length xs \<le> lenc xs" |
731 "length xs \<le> lenc xs" |
731 by (induct xs) (simp_all add: prod_encode_def) |
732 by (induct xs) (simp_all add: prod_encode_def) |
732 |
733 |
764 |
765 |
765 lemma enclen_zero [simp]: |
766 lemma enclen_zero [simp]: |
766 "enclen 0 = 0" |
767 "enclen 0 = 0" |
767 by (simp add: enclen_def) |
768 by (simp add: enclen_def) |
768 |
769 |
|
770 fun |
|
771 rec_lenc :: "recf list \<Rightarrow> recf" |
|
772 where |
|
773 "rec_lenc [] = Z" |
|
774 | "rec_lenc (f # fs) = CN rec_penc [CN S [f], rec_lenc fs]" |
769 |
775 |
770 definition |
776 definition |
771 "rec_ldec = CN rec_pred [CN rec_pdec1 [rec_swap (rec_iter rec_pdec2)]]" |
777 "rec_ldec = CN rec_pred [CN rec_pdec1 [rec_swap (rec_iter rec_pdec2)]]" |
|
778 |
|
779 definition |
|
780 "rec_within = CN rec_less [Z, rec_swap (rec_iter rec_pdec2)]" |
|
781 |
|
782 definition |
|
783 "rec_enclen = CN (rec_max1 (CN rec_not [CN rec_within [Id 2 1, CN rec_pred [Id 2 0]]])) [Id 1 0, Id 1 0]" |
772 |
784 |
773 lemma ldec_iter: |
785 lemma ldec_iter: |
774 "ldec z n = pdec1 ((Iter pdec2 n) z) - 1" |
786 "ldec z n = pdec1 ((Iter pdec2 n) z) - 1" |
775 apply(induct n arbitrary: z) |
787 by (induct n arbitrary: z) (simp | subst Iter_comm)+ |
776 apply(simp_all) |
788 |
777 apply(subst iter_comm) |
789 lemma within_iter: |
778 apply(simp) |
790 "within z n = (0 < (Iter pdec2 n) z)" |
779 done |
791 by (induct n arbitrary: z) (simp | subst Iter_comm)+ |
|
792 |
|
793 lemma lenc_lemma [simp]: |
|
794 "rec_eval (rec_lenc fs) xs = lenc (map (\<lambda>f. rec_eval f xs) fs)" |
|
795 by (induct fs) (simp_all) |
780 |
796 |
781 lemma ldec_lemma [simp]: |
797 lemma ldec_lemma [simp]: |
782 "rec_eval rec_ldec [z, n] = ldec z n" |
798 "rec_eval rec_ldec [z, n] = ldec z n" |
783 by (simp add: ldec_iter rec_ldec_def) |
799 by (simp add: ldec_iter rec_ldec_def) |
784 |
800 |
|
801 lemma within_lemma [simp]: |
|
802 "rec_eval rec_within [z, n] = (if within z n then 1 else 0)" |
|
803 by (simp add: within_iter rec_within_def) |
|
804 |
|
805 lemma enclen_lemma [simp]: |
|
806 "rec_eval rec_enclen [z] = enclen z" |
|
807 by (simp add: rec_enclen_def enclen_def) |
|
808 |
|
809 |
785 end |
810 end |
786 |
811 |