60 |
60 |
61 primcorec sp\<^sub>\<nu>_comp (infixl "o\<^sub>\<nu>" 65) where |
61 primcorec sp\<^sub>\<nu>_comp (infixl "o\<^sub>\<nu>" 65) where |
62 "out (sp o\<^sub>\<nu> sp') = map_sp\<^sub>\<mu> id (\<lambda>(sp, sp'). sp o\<^sub>\<nu> sp') (out sp o\<^sub>\<mu> out sp')" |
62 "out (sp o\<^sub>\<nu> sp') = map_sp\<^sub>\<mu> id (\<lambda>(sp, sp'). sp o\<^sub>\<nu> sp') (out sp o\<^sub>\<mu> out sp')" |
63 |
63 |
64 lemma run\<^sub>\<nu>_sp\<^sub>\<nu>_comp: "run\<^sub>\<nu> (sp o\<^sub>\<nu> sp') = run\<^sub>\<nu> sp o run\<^sub>\<nu> sp'" |
64 lemma run\<^sub>\<nu>_sp\<^sub>\<nu>_comp: "run\<^sub>\<nu> (sp o\<^sub>\<nu> sp') = run\<^sub>\<nu> sp o run\<^sub>\<nu> sp'" |
65 proof (rule ext, unfold o_apply) |
65 proof (rule ext, unfold comp_apply) |
66 fix s |
66 fix s |
67 show "run\<^sub>\<nu> (sp o\<^sub>\<nu> sp') s = run\<^sub>\<nu> sp (run\<^sub>\<nu> sp' s)" |
67 show "run\<^sub>\<nu> (sp o\<^sub>\<nu> sp') s = run\<^sub>\<nu> sp (run\<^sub>\<nu> sp' s)" |
68 proof (coinduction arbitrary: sp sp' s) |
68 proof (coinduction arbitrary: sp sp' s) |
69 case Eq_stream |
69 case Eq_stream |
70 show ?case |
70 show ?case |
93 |
93 |
94 primcorec sp\<^sub>\<nu>_comp2 (infixl "o\<^sup>*\<^sub>\<nu>" 65) where |
94 primcorec sp\<^sub>\<nu>_comp2 (infixl "o\<^sup>*\<^sub>\<nu>" 65) where |
95 "out (sp o\<^sup>*\<^sub>\<nu> sp') = map_sp\<^sub>\<mu> id (\<lambda>(sp, sp'). sp o\<^sup>*\<^sub>\<nu> sp') (out sp o\<^sup>*\<^sub>\<mu> out sp')" |
95 "out (sp o\<^sup>*\<^sub>\<nu> sp') = map_sp\<^sub>\<mu> id (\<lambda>(sp, sp'). sp o\<^sup>*\<^sub>\<nu> sp') (out sp o\<^sup>*\<^sub>\<mu> out sp')" |
96 |
96 |
97 lemma run\<^sub>\<nu>_sp\<^sub>\<nu>_comp2: "run\<^sub>\<nu> (sp o\<^sup>*\<^sub>\<nu> sp') = run\<^sub>\<nu> sp o run\<^sub>\<nu> sp'" |
97 lemma run\<^sub>\<nu>_sp\<^sub>\<nu>_comp2: "run\<^sub>\<nu> (sp o\<^sup>*\<^sub>\<nu> sp') = run\<^sub>\<nu> sp o run\<^sub>\<nu> sp'" |
98 proof (rule ext, unfold o_apply) |
98 proof (rule ext, unfold comp_apply) |
99 fix s |
99 fix s |
100 show "run\<^sub>\<nu> (sp o\<^sup>*\<^sub>\<nu> sp') s = run\<^sub>\<nu> sp (run\<^sub>\<nu> sp' s)" |
100 show "run\<^sub>\<nu> (sp o\<^sup>*\<^sub>\<nu> sp') s = run\<^sub>\<nu> sp (run\<^sub>\<nu> sp' s)" |
101 proof (coinduction arbitrary: sp sp' s) |
101 proof (coinduction arbitrary: sp sp' s) |
102 case Eq_stream |
102 case Eq_stream |
103 show ?case |
103 show ?case |
155 definition \<theta> :: "('p,'a) F * 'b \<Rightarrow> ('p,'a * 'b) F" where |
155 definition \<theta> :: "('p,'a) F * 'b \<Rightarrow> ('p,'a * 'b) F" where |
156 "\<theta> xb = F id <id, \<lambda> a. (snd xb)> (fst xb)" |
156 "\<theta> xb = F id <id, \<lambda> a. (snd xb)> (fst xb)" |
157 |
157 |
158 (* The strength laws for \<theta>: *) |
158 (* The strength laws for \<theta>: *) |
159 lemma \<theta>_natural: "F id (map_pair f g) o \<theta> = \<theta> o map_pair (F id f) g" |
159 lemma \<theta>_natural: "F id (map_pair f g) o \<theta> = \<theta> o map_pair (F id f) g" |
160 unfolding \<theta>_def F.map_comp o_def id_apply convol_def map_pair_def split_beta fst_conv snd_conv .. |
160 unfolding \<theta>_def F.map_comp comp_def id_apply convol_def map_pair_def split_beta fst_conv snd_conv .. |
161 |
161 |
162 definition assl :: "'a * ('b * 'c) \<Rightarrow> ('a * 'b) * 'c" where |
162 definition assl :: "'a * ('b * 'c) \<Rightarrow> ('a * 'b) * 'c" where |
163 "assl abc = ((fst abc, fst (snd abc)), snd (snd abc))" |
163 "assl abc = ((fst abc, fst (snd abc)), snd (snd abc))" |
164 |
164 |
165 lemma \<theta>_rid: "F id fst o \<theta> = fst" |
165 lemma \<theta>_rid: "F id fst o \<theta> = fst" |
166 unfolding \<theta>_def F.map_comp F.map_id o_def id_apply convol_def fst_conv sym[OF id_def] .. |
166 unfolding \<theta>_def F.map_comp F.map_id comp_def id_apply convol_def fst_conv sym[OF id_def] .. |
167 |
167 |
168 lemma \<theta>_assl: "F id assl o \<theta> = \<theta> o map_pair \<theta> id o assl" |
168 lemma \<theta>_assl: "F id assl o \<theta> = \<theta> o map_pair \<theta> id o assl" |
169 unfolding assl_def \<theta>_def F.map_comp o_def id_apply convol_def map_pair_def split fst_conv snd_conv .. |
169 unfolding assl_def \<theta>_def F.map_comp comp_def id_apply convol_def map_pair_def split fst_conv snd_conv .. |
170 |
170 |
171 datatype_new ('a, 'b, 'c) spF\<^sub>\<mu> = GetF "'a \<Rightarrow> ('a, 'b, 'c) spF\<^sub>\<mu>" | PutF "('b,'c) F" |
171 datatype_new ('a, 'b, 'c) spF\<^sub>\<mu> = GetF "'a \<Rightarrow> ('a, 'b, 'c) spF\<^sub>\<mu>" | PutF "('b,'c) F" |
172 codatatype ('a, 'b) spF\<^sub>\<nu> = InF (outF: "('a, 'b, ('a, 'b) spF\<^sub>\<nu>) spF\<^sub>\<mu>") |
172 codatatype ('a, 'b) spF\<^sub>\<nu> = InF (outF: "('a, 'b, ('a, 'b) spF\<^sub>\<nu>) spF\<^sub>\<mu>") |
173 |
173 |
174 codatatype 'b JF = Ctor (dtor: "('b, 'b JF) F") |
174 codatatype 'b JF = Ctor (dtor: "('b, 'b JF) F") |