12 imports "../Codatatype" |
12 imports "../Codatatype" |
13 begin |
13 begin |
14 |
14 |
15 data_raw listF: 'list = "unit + 'a \<times> 'list" |
15 data_raw listF: 'list = "unit + 'a \<times> 'list" |
16 |
16 |
17 definition "NilF = listF_fld (Inl ())" |
17 definition "NilF = listF_ctor (Inl ())" |
18 definition "Conss a as \<equiv> listF_fld (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.fld_iters by simp |
21 unfolding listF_map_def pre_listF_map_def NilF_def listF.ctor_folds 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.fld_iters by simp |
25 unfolding listF_map_def pre_listF_map_def Conss_def listF.ctor_folds 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.fld_iters pre_listF_set1_def pre_listF_set2_def |
28 unfolding listF_set_def NilF_def listF.ctor_folds 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.fld_iters pre_listF_set1_def pre_listF_set2_def |
32 unfolding listF_set_def Conss_def listF.ctor_folds 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 iter_sum_case_NilF: "listF_fld_iter (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.fld_iters pre_listF_map_def by simp |
36 unfolding NilF_def listF.ctor_folds pre_listF_map_def by simp |
37 |
37 |
38 |
38 |
39 lemma iter_sum_case_Conss: |
39 lemma fold_sum_case_Conss: |
40 "listF_fld_iter (sum_case f g) (Conss y ys) = g (y, listF_fld_iter (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.fld_iters pre_listF_map_def by simp |
41 unfolding Conss_def listF.ctor_folds 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)" |
47 shows "P xs" |
47 shows "P xs" |
48 proof (rule listF.fld_induct) |
48 proof (rule listF.ctor_induct) |
49 fix xs :: "unit + 'a \<times> 'a listF" |
49 fix xs :: "unit + 'a \<times> 'a listF" |
50 assume raw_IH: "\<And>a. a \<in> pre_listF_set2 xs \<Longrightarrow> P a" |
50 assume raw_IH: "\<And>a. a \<in> pre_listF_set2 xs \<Longrightarrow> P a" |
51 show "P (listF_fld xs)" |
51 show "P (listF_ctor xs)" |
52 proof (cases xs) |
52 proof (cases xs) |
53 case (Inl a) with IB show ?thesis unfolding NilF_def by simp |
53 case (Inl a) with IB show ?thesis unfolding NilF_def by simp |
54 next |
54 next |
55 case (Inr b) |
55 case (Inr b) |
56 then obtain y ys where yys: "listF_fld xs = Conss y ys" |
56 then obtain y ys where yys: "listF_ctor xs = Conss y ys" |
57 unfolding Conss_def listF.fld_inject by (blast intro: prod.exhaust) |
57 unfolding Conss_def listF.ctor_inject by (blast intro: prod.exhaust) |
58 hence "ys \<in> pre_listF_set2 xs" |
58 hence "ys \<in> pre_listF_set2 xs" |
59 unfolding pre_listF_set2_def Conss_def listF.fld_inject sum_set_defs prod_set_defs |
59 unfolding pre_listF_set2_def Conss_def listF.ctor_inject sum_set_defs prod_set_defs |
60 collect_def[abs_def] by simp |
60 collect_def[abs_def] by simp |
61 with raw_IH have "P ys" by blast |
61 with raw_IH have "P ys" by blast |
62 with IH have "P (Conss y ys)" by blast |
62 with IH have "P (Conss y ys)" by blast |
63 with yys show ?thesis by simp |
63 with yys show ?thesis by simp |
64 qed |
64 qed |
65 qed |
65 qed |
66 |
66 |
67 rep_datatype NilF Conss |
67 rep_datatype NilF Conss |
68 by (blast intro: listF_induct) (auto simp add: NilF_def Conss_def listF.fld_inject) |
68 by (blast intro: listF_induct) (auto simp add: NilF_def Conss_def listF.ctor_inject) |
69 |
69 |
70 definition Singll ("[[_]]") where |
70 definition Singll ("[[_]]") where |
71 [simp]: "Singll a \<equiv> Conss a NilF" |
71 [simp]: "Singll a \<equiv> Conss a NilF" |
72 |
72 |
73 definition appendd (infixr "@@" 65) where |
73 definition appendd (infixr "@@" 65) where |
74 "appendd \<equiv> listF_fld_iter (sum_case (\<lambda> _. id) (\<lambda> (a,f) bs. Conss a (f bs)))" |
74 "appendd \<equiv> listF_ctor_fold (sum_case (\<lambda> _. id) (\<lambda> (a,f) bs. Conss a (f bs)))" |
75 |
75 |
76 definition "lrev \<equiv> listF_fld_iter (sum_case (\<lambda> _. NilF) (\<lambda> (b,bs). bs @@ [[b]]))" |
76 definition "lrev \<equiv> listF_ctor_fold (sum_case (\<lambda> _. NilF) (\<lambda> (b,bs). bs @@ [[b]]))" |
77 |
77 |
78 lemma lrev_NilF[simp]: "lrev NilF = NilF" |
78 lemma lrev_NilF[simp]: "lrev NilF = NilF" |
79 unfolding lrev_def by (simp add: iter_sum_case_NilF) |
79 unfolding lrev_def by (simp add: fold_sum_case_NilF) |
80 |
80 |
81 lemma lrev_Conss[simp]: "lrev (Conss y ys) = lrev ys @@ [[y]]" |
81 lemma lrev_Conss[simp]: "lrev (Conss y ys) = lrev ys @@ [[y]]" |
82 unfolding lrev_def by (simp add: iter_sum_case_Conss) |
82 unfolding lrev_def by (simp add: fold_sum_case_Conss) |
83 |
83 |
84 lemma NilF_appendd[simp]: "NilF @@ ys = ys" |
84 lemma NilF_appendd[simp]: "NilF @@ ys = ys" |
85 unfolding appendd_def by (simp add: iter_sum_case_NilF) |
85 unfolding appendd_def by (simp add: fold_sum_case_NilF) |
86 |
86 |
87 lemma Conss_append[simp]: "Conss x xs @@ ys = Conss x (xs @@ ys)" |
87 lemma Conss_append[simp]: "Conss x xs @@ ys = Conss x (xs @@ ys)" |
88 unfolding appendd_def by (simp add: iter_sum_case_Conss) |
88 unfolding appendd_def by (simp add: fold_sum_case_Conss) |
89 |
89 |
90 lemma appendd_NilF[simp]: "xs @@ NilF = xs" |
90 lemma appendd_NilF[simp]: "xs @@ NilF = xs" |
91 by (rule listF_induct) auto |
91 by (rule listF_induct) auto |
92 |
92 |
93 lemma appendd_assoc[simp]: "(xs @@ ys) @@ zs = xs @@ ys @@ zs" |
93 lemma appendd_assoc[simp]: "(xs @@ ys) @@ zs = xs @@ ys @@ zs" |