773 by (induct xs) (simp_all add: prod_encode_def) |
772 by (induct xs) (simp_all add: prod_encode_def) |
774 |
773 |
775 |
774 |
776 text {* Membership for the List Encoding *} |
775 text {* Membership for the List Encoding *} |
777 |
776 |
778 fun within :: "nat \<Rightarrow> nat \<Rightarrow> bool" where |
777 fun inside :: "nat \<Rightarrow> nat \<Rightarrow> bool" where |
779 "within z 0 = (0 < z)" |
778 "inside z 0 = (0 < z)" |
780 | "within z (Suc n) = within (pdec2 z) n" |
779 | "inside z (Suc n) = inside (pdec2 z) n" |
781 |
780 |
782 definition enclen :: "nat \<Rightarrow> nat" where |
781 definition enclen :: "nat \<Rightarrow> nat" where |
783 "enclen z = BMax_rec (\<lambda>x. within z (x - 1)) z" |
782 "enclen z = BMax_rec (\<lambda>x. inside z (x - 1)) z" |
784 |
783 |
785 lemma within_False [simp]: |
784 lemma inside_False [simp]: |
786 "within 0 n = False" |
785 "inside 0 n = False" |
787 by (induct n) (simp_all) |
786 by (induct n) (simp_all) |
788 |
787 |
789 lemma within_length [simp]: |
788 lemma inside_length [simp]: |
790 "within (lenc xs) s = (s < length xs)" |
789 "inside (lenc xs) s = (s < length xs)" |
791 apply(induct s arbitrary: xs) |
790 apply(induct s arbitrary: xs) |
792 apply(case_tac xs) |
791 apply(case_tac xs) |
793 apply(simp_all add: prod_encode_def) |
792 apply(simp_all add: prod_encode_def) |
794 apply(case_tac xs) |
793 apply(case_tac xs) |
795 apply(simp_all) |
794 apply(simp_all) |
824 |
823 |
825 definition |
824 definition |
826 "rec_ldec = CN rec_predi [CN rec_pdec1 [rec_swap (rec_iter rec_pdec2)]]" |
825 "rec_ldec = CN rec_predi [CN rec_pdec1 [rec_swap (rec_iter rec_pdec2)]]" |
827 |
826 |
828 definition |
827 definition |
829 "rec_within = CN rec_less [Z, rec_swap (rec_iter rec_pdec2)]" |
828 "rec_inside = CN rec_less [Z, rec_swap (rec_iter rec_pdec2)]" |
830 |
829 |
831 definition |
830 definition |
832 "rec_enclen = CN (rec_max1 (CN rec_not [CN rec_within [Id 2 1, CN rec_predi [Id 2 0]]])) [Id 1 0, Id 1 0]" |
831 "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]" |
833 |
832 |
834 lemma ldec_iter: |
833 lemma ldec_iter: |
835 "ldec z n = pdec1 (Iter pdec2 n z) - 1" |
834 "ldec z n = pdec1 (Iter pdec2 n z) - 1" |
836 by (induct n arbitrary: z) (simp | subst Iter_comm)+ |
835 by (induct n arbitrary: z) (simp | subst Iter_comm)+ |
837 |
836 |
838 lemma within_iter: |
837 lemma inside_iter: |
839 "within z n = (0 < Iter pdec2 n z)" |
838 "inside z n = (0 < Iter pdec2 n z)" |
840 by (induct n arbitrary: z) (simp | subst Iter_comm)+ |
839 by (induct n arbitrary: z) (simp | subst Iter_comm)+ |
841 |
840 |
842 lemma lenc_lemma [simp]: |
841 lemma lenc_lemma [simp]: |
843 "rec_eval (rec_lenc fs) xs = lenc (map (\<lambda>f. rec_eval f xs) fs)" |
842 "rec_eval (rec_lenc fs) xs = lenc (map (\<lambda>f. rec_eval f xs) fs)" |
844 by (induct fs) (simp_all) |
843 by (induct fs) (simp_all) |
845 |
844 |
846 lemma ldec_lemma [simp]: |
845 lemma ldec_lemma [simp]: |
847 "rec_eval rec_ldec [z, n] = ldec z n" |
846 "rec_eval rec_ldec [z, n] = ldec z n" |
848 by (simp add: ldec_iter rec_ldec_def) |
847 by (simp add: ldec_iter rec_ldec_def) |
849 |
848 |
850 lemma within_lemma [simp]: |
849 lemma inside_lemma [simp]: |
851 "rec_eval rec_within [z, n] = (if within z n then 1 else 0)" |
850 "rec_eval rec_inside [z, n] = (if inside z n then 1 else 0)" |
852 by (simp add: within_iter rec_within_def) |
851 by (simp add: inside_iter rec_inside_def) |
853 |
852 |
854 lemma enclen_lemma [simp]: |
853 lemma enclen_lemma [simp]: |
855 "rec_eval rec_enclen [z] = enclen z" |
854 "rec_eval rec_enclen [z] = enclen z" |
856 by (simp add: rec_enclen_def enclen_def) |
855 by (simp add: rec_enclen_def enclen_def) |
857 |
856 |