16 |
16 |
17 definition "NilF = listF_ctor (Inl ())" |
17 definition "NilF = listF_ctor (Inl ())" |
18 definition "Conss a as \<equiv> listF_ctor (Inr (a, as))" |
18 definition "Conss a as \<equiv> listF_ctor (Inr (a, as))" |
19 |
19 |
20 lemma listF_map_NilF[simp]: "listF_map f NilF = NilF" |
20 lemma listF_map_NilF[simp]: "listF_map f NilF = NilF" |
21 unfolding listF_map_def pre_listF_map_def NilF_def listF.ctor_folds by simp |
21 unfolding listF_map_def pre_listF_map_def NilF_def listF.ctor_fold by simp |
22 |
22 |
23 lemma listF_map_Conss[simp]: |
23 lemma listF_map_Conss[simp]: |
24 "listF_map f (Conss x xs) = Conss (f x) (listF_map f xs)" |
24 "listF_map f (Conss x xs) = Conss (f x) (listF_map f xs)" |
25 unfolding listF_map_def pre_listF_map_def Conss_def listF.ctor_folds by simp |
25 unfolding listF_map_def pre_listF_map_def Conss_def listF.ctor_fold by simp |
26 |
26 |
27 lemma listF_set_NilF[simp]: "listF_set NilF = {}" |
27 lemma listF_set_NilF[simp]: "listF_set NilF = {}" |
28 unfolding listF_set_def NilF_def listF.ctor_folds pre_listF_set1_def pre_listF_set2_def |
28 unfolding listF_set_def NilF_def listF.ctor_fold pre_listF_set1_def pre_listF_set2_def |
29 sum_set_defs pre_listF_map_def collect_def[abs_def] by simp |
29 sum_set_defs pre_listF_map_def collect_def[abs_def] by simp |
30 |
30 |
31 lemma listF_set_Conss[simp]: "listF_set (Conss x xs) = {x} \<union> listF_set xs" |
31 lemma listF_set_Conss[simp]: "listF_set (Conss x xs) = {x} \<union> listF_set xs" |
32 unfolding listF_set_def Conss_def listF.ctor_folds pre_listF_set1_def pre_listF_set2_def |
32 unfolding listF_set_def Conss_def listF.ctor_fold pre_listF_set1_def pre_listF_set2_def |
33 sum_set_defs prod_set_defs pre_listF_map_def collect_def[abs_def] by simp |
33 sum_set_defs prod_set_defs pre_listF_map_def collect_def[abs_def] by simp |
34 |
34 |
35 lemma fold_sum_case_NilF: "listF_ctor_fold (sum_case f g) NilF = f ()" |
35 lemma fold_sum_case_NilF: "listF_ctor_fold (sum_case f g) NilF = f ()" |
36 unfolding NilF_def listF.ctor_folds pre_listF_map_def by simp |
36 unfolding NilF_def listF.ctor_fold pre_listF_map_def by simp |
37 |
37 |
38 |
38 |
39 lemma fold_sum_case_Conss: |
39 lemma fold_sum_case_Conss: |
40 "listF_ctor_fold (sum_case f g) (Conss y ys) = g (y, listF_ctor_fold (sum_case f g) ys)" |
40 "listF_ctor_fold (sum_case f g) (Conss y ys) = g (y, listF_ctor_fold (sum_case f g) ys)" |
41 unfolding Conss_def listF.ctor_folds pre_listF_map_def by simp |
41 unfolding Conss_def listF.ctor_fold pre_listF_map_def by simp |
42 |
42 |
43 (* familiar induction principle *) |
43 (* familiar induction principle *) |
44 lemma listF_induct: |
44 lemma listF_induct: |
45 fixes xs :: "'a listF" |
45 fixes xs :: "'a listF" |
46 assumes IB: "P NilF" and IH: "\<And>x xs. P xs \<Longrightarrow> P (Conss x xs)" |
46 assumes IB: "P NilF" and IH: "\<And>x xs. P xs \<Longrightarrow> P (Conss x xs)" |