6598 |
6598 |
6599 lemma set_list_bind: "set (List.bind xs f) = (\<Union>x\<in>set xs. set (f x))" |
6599 lemma set_list_bind: "set (List.bind xs f) = (\<Union>x\<in>set xs. set (f x))" |
6600 by (induction xs) simp_all |
6600 by (induction xs) simp_all |
6601 |
6601 |
6602 |
6602 |
6603 subsection \<open>Transfer\<close> |
|
6604 |
|
6605 definition embed_list :: "nat list \<Rightarrow> int list" where |
|
6606 "embed_list l = map int l" |
|
6607 |
|
6608 definition nat_list :: "int list \<Rightarrow> bool" where |
|
6609 "nat_list l = nat_set (set l)" |
|
6610 |
|
6611 definition return_list :: "int list \<Rightarrow> nat list" where |
|
6612 "return_list l = map nat l" |
|
6613 |
|
6614 lemma transfer_nat_int_list_return_embed: "nat_list l \<longrightarrow> |
|
6615 embed_list (return_list l) = l" |
|
6616 unfolding embed_list_def return_list_def nat_list_def nat_set_def |
|
6617 apply (induct l) |
|
6618 apply auto |
|
6619 done |
|
6620 |
|
6621 lemma transfer_nat_int_list_functions: |
|
6622 "l @ m = return_list (embed_list l @ embed_list m)" |
|
6623 "[] = return_list []" |
|
6624 unfolding return_list_def embed_list_def |
|
6625 apply auto |
|
6626 apply (induct l, auto) |
|
6627 apply (induct m, auto) |
|
6628 done |
|
6629 |
|
6630 (* |
|
6631 lemma transfer_nat_int_fold1: "fold f l x = |
|
6632 fold (%x. f (nat x)) (embed_list l) x"; |
|
6633 *) |
|
6634 |
|
6635 |
|
6636 subsection \<open>Code generation\<close> |
6603 subsection \<open>Code generation\<close> |
6637 |
6604 |
6638 text\<open>Optional tail recursive version of @{const map}. Can avoid |
6605 text\<open>Optional tail recursive version of @{const map}. Can avoid |
6639 stack overflow in some target languages.\<close> |
6606 stack overflow in some target languages.\<close> |
6640 |
6607 |