11 imports Prelim |
11 imports Prelim |
12 begin |
12 begin |
13 |
13 |
14 hide_fact (open) Quotient_Product.prod_rel_def |
14 hide_fact (open) Quotient_Product.prod_rel_def |
15 |
15 |
16 typedecl N typedecl T |
16 typedecl N |
|
17 typedecl T |
17 |
18 |
18 codata_raw Tree: 'Tree = "N \<times> (T + 'Tree) fset" |
19 codata Tree = NNode (root: N) (ccont: "(T + Tree) fset") |
19 |
20 |
20 |
21 |
21 section {* Sugar notations for Tree *} |
22 section {* Sugar notations for Tree *} |
22 |
|
23 subsection{* Setup for map, set, rel *} |
|
24 |
|
25 (* These should be eventually inferred from compositionality *) |
|
26 |
|
27 lemma pre_Tree_map: |
|
28 "pre_Tree_map f (n, as) = (n, map_fset (id \<oplus> f) as)" |
|
29 unfolding pre_Tree_map_def id_apply |
|
30 sum_map_def by simp |
|
31 |
|
32 lemma pre_Tree_map': |
|
33 "pre_Tree_map f n_as = (fst n_as, map_fset (id \<oplus> f) (snd n_as))" |
|
34 using pre_Tree_map by(cases n_as, simp) |
|
35 |
|
36 |
23 |
37 definition |
24 definition |
38 "llift2 \<phi> as1 as2 \<longleftrightarrow> |
25 "llift2 \<phi> as1 as2 \<longleftrightarrow> |
39 (\<forall> n. Inl n \<in> fset as1 \<longleftrightarrow> Inl n \<in> fset as2) \<and> |
26 (\<forall> n. Inl n \<in> fset as1 \<longleftrightarrow> Inl n \<in> fset as2) \<and> |
40 (\<forall> tr1. Inr tr1 \<in> fset as1 \<longrightarrow> (\<exists> tr2. Inr tr2 \<in> fset as2 \<and> \<phi> tr1 tr2)) \<and> |
27 (\<forall> tr1. Inr tr1 \<in> fset as1 \<longrightarrow> (\<exists> tr2. Inr tr2 \<in> fset as2 \<and> \<phi> tr1 tr2)) \<and> |
50 apply (metis sumE sum.simps(1,2,4)) |
37 apply (metis sumE sum.simps(1,2,4)) |
51 apply (metis sumE sum.simps(1,2,4)) |
38 apply (metis sumE sum.simps(1,2,4)) |
52 done |
39 done |
53 |
40 |
54 |
41 |
55 subsection{* Constructors *} |
|
56 |
|
57 definition NNode :: "N \<Rightarrow> (T + Tree)fset \<Rightarrow> Tree" |
|
58 where "NNode n as \<equiv> Tree_ctor (n,as)" |
|
59 |
|
60 lemmas ctor_defs = NNode_def |
|
61 |
|
62 |
|
63 subsection {* Pre-selectors *} |
|
64 |
|
65 (* These are mere auxiliaries *) |
|
66 |
|
67 definition "asNNode tr \<equiv> SOME n_as. NNode (fst n_as) (snd n_as) = tr" |
|
68 lemmas pre_sel_defs = asNNode_def |
|
69 |
|
70 |
|
71 subsection {* Selectors *} |
|
72 |
|
73 (* One for each pair (constructor, constructor argument) *) |
|
74 |
|
75 (* For NNode: *) |
|
76 definition root :: "Tree \<Rightarrow> N" where "root tr = fst (asNNode tr)" |
|
77 definition ccont :: "Tree \<Rightarrow> (T + Tree)fset" where "ccont tr = snd (asNNode tr)" |
|
78 |
|
79 lemmas sel_defs = root_def ccont_def |
|
80 |
|
81 |
|
82 subsection {* Basic properties *} |
|
83 |
|
84 (* Constructors versus selectors *) |
|
85 lemma NNode_surj: "\<exists> n as. NNode n as = tr" |
|
86 unfolding NNode_def |
|
87 by (metis Tree.ctor_dtor pair_collapse) |
|
88 |
|
89 lemma NNode_asNNode: |
|
90 "NNode (fst (asNNode tr)) (snd (asNNode tr)) = tr" |
|
91 proof- |
|
92 obtain n as where "NNode n as = tr" using NNode_surj[of tr] by blast |
|
93 hence "NNode (fst (n,as)) (snd (n,as)) = tr" by simp |
|
94 thus ?thesis unfolding asNNode_def by(rule someI) |
|
95 qed |
|
96 |
|
97 theorem NNode_root_ccont[simp]: |
|
98 "NNode (root tr) (ccont tr) = tr" |
|
99 using NNode_asNNode unfolding root_def ccont_def . |
|
100 |
|
101 (* Constructors *) |
|
102 theorem TTree_simps[simp]: |
|
103 "NNode n as = NNode n' as' \<longleftrightarrow> n = n' \<and> as = as'" |
|
104 unfolding ctor_defs Tree.ctor_inject by auto |
|
105 |
|
106 theorem TTree_cases[elim, case_names NNode Choice]: |
|
107 assumes NNode: "\<And> n as. tr = NNode n as \<Longrightarrow> phi" |
|
108 shows phi |
|
109 proof(cases rule: Tree.ctor_exhaust[of tr]) |
|
110 fix x assume "tr = Tree_ctor x" |
|
111 thus ?thesis |
|
112 apply(cases x) |
|
113 using NNode unfolding ctor_defs apply blast |
|
114 done |
|
115 qed |
|
116 |
|
117 (* Constructors versus selectors *) |
|
118 theorem TTree_sel_ctor[simp]: |
|
119 "root (NNode n as) = n" |
|
120 "ccont (NNode n as) = as" |
|
121 unfolding root_def ccont_def |
|
122 by (metis (no_types) NNode_asNNode TTree_simps)+ |
|
123 |
|
124 |
|
125 subsection{* Coinduction *} |
42 subsection{* Coinduction *} |
126 |
43 |
127 theorem TTree_coind_Node[elim, consumes 1, case_names NNode, induct pred: "HOL.eq"]: |
44 theorem Tree_coind_NNode[elim, consumes 1, case_names NNode, induct pred: "HOL.eq"]: |
128 assumes phi: "\<phi> tr1 tr2" and |
45 assumes phi: "\<phi> tr1 tr2" and |
129 NNode: "\<And> n1 n2 as1 as2. |
46 NNode: "\<And> n1 n2 as1 as2. |
130 \<lbrakk>\<phi> (NNode n1 as1) (NNode n2 as2)\<rbrakk> \<Longrightarrow> |
47 \<lbrakk>\<phi> (NNode n1 as1) (NNode n2 as2)\<rbrakk> \<Longrightarrow> |
131 n1 = n2 \<and> llift2 \<phi> as1 as2" |
48 n1 = n2 \<and> llift2 \<phi> as1 as2" |
132 shows "tr1 = tr2" |
49 shows "tr1 = tr2" |
139 unfolding pre_Tree_rel apply(rule NNode) using \<phi> unfolding NNode_def by simp |
56 unfolding pre_Tree_rel apply(rule NNode) using \<phi> unfolding NNode_def by simp |
140 qed |
57 qed |
141 |
58 |
142 theorem TTree_coind[elim, consumes 1, case_names LLift]: |
59 theorem TTree_coind[elim, consumes 1, case_names LLift]: |
143 assumes phi: "\<phi> tr1 tr2" and |
60 assumes phi: "\<phi> tr1 tr2" and |
144 LLift: "\<And> tr1 tr2. \<phi> tr1 tr2 \<Longrightarrow> |
61 LLift: "\<And> tr1 tr2. \<phi> tr1 tr2 \<Longrightarrow> root tr1 = root tr2 \<and> llift2 \<phi> (ccont tr1) (ccont tr2)" |
145 root tr1 = root tr2 \<and> llift2 \<phi> (ccont tr1) (ccont tr2)" |
|
146 shows "tr1 = tr2" |
62 shows "tr1 = tr2" |
147 using phi apply(induct rule: TTree_coind_Node) |
63 using phi apply(induct rule: Tree_coind_NNode) |
148 using LLift by (metis TTree_sel_ctor) |
64 using LLift by (metis Tree.sels) |
149 |
|
150 |
|
151 |
|
152 subsection {* Coiteration *} |
|
153 |
|
154 (* Preliminaries: *) |
|
155 declare Tree.dtor_ctor[simp] |
|
156 declare Tree.ctor_dtor[simp] |
|
157 |
|
158 lemma Tree_dtor_NNode[simp]: |
|
159 "Tree_dtor (NNode n as) = (n,as)" |
|
160 unfolding NNode_def Tree.dtor_ctor .. |
|
161 |
|
162 lemma Tree_dtor_root_ccont: |
|
163 "Tree_dtor tr = (root tr, ccont tr)" |
|
164 unfolding root_def ccont_def |
|
165 by (metis (lifting) NNode_asNNode Tree_dtor_NNode) |
|
166 |
|
167 (* Coiteration *) |
|
168 definition TTree_unfold :: |
|
169 "('b \<Rightarrow> N) \<Rightarrow> ('b \<Rightarrow> (T + 'b) fset) \<Rightarrow> 'b \<Rightarrow> Tree" |
|
170 where "TTree_unfold rt ct \<equiv> Tree_dtor_unfold <rt,ct>" |
|
171 |
|
172 lemma Tree_unfold_unfold: |
|
173 "Tree_dtor_unfold s = TTree_unfold (fst o s) (snd o s)" |
|
174 apply(rule ext) |
|
175 unfolding TTree_unfold_def by simp |
|
176 |
|
177 theorem TTree_unfold: |
|
178 "root (TTree_unfold rt ct b) = rt b" |
|
179 "ccont (TTree_unfold rt ct b) = map_fset (id \<oplus> TTree_unfold rt ct) (ct b)" |
|
180 using Tree.dtor_unfold[of "<rt,ct>" b] unfolding Tree_unfold_unfold fst_convol snd_convol |
|
181 unfolding pre_Tree_map' fst_convol' snd_convol' |
|
182 unfolding Tree_dtor_root_ccont by simp_all |
|
183 |
|
184 (* Corecursion, stronger than coiteration (unfold) *) |
|
185 definition TTree_corec :: |
|
186 "('b \<Rightarrow> N) \<Rightarrow> ('b \<Rightarrow> (T + (Tree + 'b)) fset) \<Rightarrow> 'b \<Rightarrow> Tree" |
|
187 where "TTree_corec rt ct \<equiv> Tree_dtor_corec <rt,ct>" |
|
188 |
|
189 lemma Tree_dtor_corec_corec: |
|
190 "Tree_dtor_corec s = TTree_corec (fst o s) (snd o s)" |
|
191 apply(rule ext) |
|
192 unfolding TTree_corec_def by simp |
|
193 |
|
194 theorem TTree_corec: |
|
195 "root (TTree_corec rt ct b) = rt b" |
|
196 "ccont (TTree_corec rt ct b) = map_fset (id \<oplus> ([[id, TTree_corec rt ct]]) ) (ct b)" |
|
197 using Tree.dtor_corec[of "<rt,ct>" b] unfolding Tree_dtor_corec_corec fst_convol snd_convol |
|
198 unfolding pre_Tree_map' fst_convol' snd_convol' |
|
199 unfolding Tree_dtor_root_ccont by simp_all |
|
200 |
65 |
201 |
66 |
202 subsection{* The characteristic theorems transported from fset to set *} |
67 subsection{* The characteristic theorems transported from fset to set *} |
203 |
68 |
204 definition "Node n as \<equiv> NNode n (the_inv fset as)" |
69 definition "Node n as \<equiv> NNode n (the_inv fset as)" |
205 definition "cont \<equiv> fset o ccont" |
70 definition "cont \<equiv> fset o ccont" |
206 definition "unfold rt ct \<equiv> TTree_unfold rt (the_inv fset o ct)" |
71 definition "unfold rt ct \<equiv> Tree_unfold rt (the_inv fset o ct)" |
207 definition "corec rt ct \<equiv> TTree_corec rt (the_inv fset o ct)" |
72 definition "corec rt ct \<equiv> Tree_corec rt (the_inv fset o ct)" |
208 |
73 |
209 definition lift ("_ ^#" 200) where |
74 definition lift ("_ ^#" 200) where |
210 "lift \<phi> as \<longleftrightarrow> (\<forall> tr. Inr tr \<in> as \<longrightarrow> \<phi> tr)" |
75 "lift \<phi> as \<longleftrightarrow> (\<forall> tr. Inr tr \<in> as \<longrightarrow> \<phi> tr)" |
211 |
76 |
212 definition lift2 ("_ ^#2" 200) where |
77 definition lift2 ("_ ^#2" 200) where |
257 lemma finite_cont[simp]: "finite (cont tr)" |
122 lemma finite_cont[simp]: "finite (cont tr)" |
258 unfolding cont_def by auto |
123 unfolding cont_def by auto |
259 |
124 |
260 theorem Node_root_cont[simp]: |
125 theorem Node_root_cont[simp]: |
261 "Node (root tr) (cont tr) = tr" |
126 "Node (root tr) (cont tr) = tr" |
262 using NNode_root_ccont unfolding Node_def cont_def |
127 using Tree.collapse unfolding Node_def cont_def |
263 by (metis cont_def finite_cont fset_cong fset_to_fset o_def) |
128 by (metis cont_def finite_cont fset_cong fset_to_fset o_def) |
264 |
129 |
265 theorem Tree_simps[simp]: |
130 theorem Tree_simps[simp]: |
266 assumes "finite as" and "finite as'" |
131 assumes "finite as" and "finite as'" |
267 shows "Node n as = Node n' as' \<longleftrightarrow> n = n' \<and> as = as'" |
132 shows "Node n as = Node n' as' \<longleftrightarrow> n = n' \<and> as = as'" |
268 using assms TTree_simps unfolding Node_def |
133 using assms Tree.inject unfolding Node_def |
269 by (metis fset_to_fset) |
134 by (metis fset_to_fset) |
270 |
135 |
271 theorem Tree_cases[elim, case_names Node Choice]: |
136 theorem Tree_cases[elim, case_names Node Choice]: |
272 assumes Node: "\<And> n as. \<lbrakk>finite as; tr = Node n as\<rbrakk> \<Longrightarrow> phi" |
137 assumes Node: "\<And> n as. \<lbrakk>finite as; tr = Node n as\<rbrakk> \<Longrightarrow> phi" |
273 shows phi |
138 shows phi |
274 apply(cases rule: TTree_cases[of tr]) |
139 apply(cases rule: Tree.exhaust[of tr]) |
275 using Node unfolding Node_def |
140 using Node unfolding Node_def |
276 by (metis Node Node_root_cont finite_cont) |
141 by (metis Node Node_root_cont finite_cont) |
277 |
142 |
278 theorem Tree_sel_ctor[simp]: |
143 theorem Tree_sel_ctor[simp]: |
279 "root (Node n as) = n" |
144 "root (Node n as) = n" |
288 Node: |
153 Node: |
289 "\<And> n1 n2 as1 as2. |
154 "\<And> n1 n2 as1 as2. |
290 \<lbrakk>finite as1; finite as2; \<phi> (Node n1 as1) (Node n2 as2)\<rbrakk> |
155 \<lbrakk>finite as1; finite as2; \<phi> (Node n1 as1) (Node n2 as2)\<rbrakk> |
291 \<Longrightarrow> n1 = n2 \<and> (\<phi>^#2) as1 as2" |
156 \<Longrightarrow> n1 = n2 \<and> (\<phi>^#2) as1 as2" |
292 shows "tr1 = tr2" |
157 shows "tr1 = tr2" |
293 using phi apply(induct rule: TTree_coind_Node) |
158 using phi apply(induct rule: Tree_coind_NNode) |
294 unfolding llift2_lift2 apply(rule Node) |
159 unfolding llift2_lift2 apply(rule Node) |
295 unfolding Node_def |
160 unfolding Node_def |
296 apply (metis finite_fset) |
161 apply (metis finite_fset) |
297 apply (metis finite_fset) |
162 apply (metis finite_fset) |
298 by (metis finite_fset fset_cong fset_to_fset) |
163 by (metis finite_fset fset_cong fset_to_fset) |
306 unfolding llift2_lift2 apply(rule Lift[unfolded cont_def comp_def]) . |
171 unfolding llift2_lift2 apply(rule Lift[unfolded cont_def comp_def]) . |
307 |
172 |
308 theorem unfold: |
173 theorem unfold: |
309 "root (unfold rt ct b) = rt b" |
174 "root (unfold rt ct b) = rt b" |
310 "finite (ct b) \<Longrightarrow> cont (unfold rt ct b) = image (id \<oplus> unfold rt ct) (ct b)" |
175 "finite (ct b) \<Longrightarrow> cont (unfold rt ct b) = image (id \<oplus> unfold rt ct) (ct b)" |
311 using TTree_unfold[of rt "the_inv fset \<circ> ct" b] unfolding unfold_def |
176 using Tree.sel_unfold[of rt "the_inv fset \<circ> ct" b] unfolding unfold_def |
312 apply - apply metis |
177 apply - apply metis |
313 unfolding cont_def comp_def |
178 unfolding cont_def comp_def |
314 by (metis (no_types) fset_to_fset map_fset_image) |
179 by (metis (no_types) fset_to_fset map_fset_image) |
315 |
180 |
316 |
|
317 theorem corec: |
181 theorem corec: |
318 "root (corec rt ct b) = rt b" |
182 "root (corec rt ct b) = rt b" |
319 "finite (ct b) \<Longrightarrow> cont (corec rt ct b) = image (id \<oplus> ([[id, corec rt ct]])) (ct b)" |
183 "finite (ct b) \<Longrightarrow> cont (corec rt ct b) = image (id \<oplus> ([[id, corec rt ct]])) (ct b)" |
320 using TTree_corec[of rt "the_inv fset \<circ> ct" b] unfolding corec_def |
184 using Tree.sel_corec[of rt "the_inv fset \<circ> ct" b] unfolding corec_def |
321 apply - apply metis |
185 apply - |
322 unfolding cont_def comp_def |
186 apply simp |
|
187 unfolding cont_def comp_def id_def |
323 by (metis (no_types) fset_to_fset map_fset_image) |
188 by (metis (no_types) fset_to_fset map_fset_image) |
324 |
189 |
325 |
|
326 end |
190 end |