14 |
14 |
15 hide_const (open) Sublist.sub |
15 hide_const (open) Sublist.sub |
16 |
16 |
17 codata_raw treeFI: 'tree = "'a \<times> 'tree listF" |
17 codata_raw treeFI: 'tree = "'a \<times> 'tree listF" |
18 |
18 |
19 lemma treeFIBNF_listF_set[simp]: "treeFIBNF_set2 (i, xs) = listF_set xs" |
19 lemma pre_treeFI_listF_set[simp]: "pre_treeFI_set2 (i, xs) = listF_set xs" |
20 unfolding treeFIBNF_set2_def collect_def[abs_def] prod_set_defs |
20 unfolding pre_treeFI_set2_def collect_def[abs_def] prod_set_defs |
21 by (auto simp add: listF.set_natural') |
21 by (auto simp add: listF.set_natural') |
22 |
22 |
23 (* selectors for trees *) |
23 (* selectors for trees *) |
24 definition "lab tr \<equiv> fst (treeFI_unf tr)" |
24 definition "lab tr \<equiv> fst (treeFI_unf tr)" |
25 definition "sub tr \<equiv> snd (treeFI_unf tr)" |
25 definition "sub tr \<equiv> snd (treeFI_unf tr)" |
29 |
29 |
30 definition pair_fun (infixr "\<odot>" 50) where |
30 definition pair_fun (infixr "\<odot>" 50) where |
31 "f \<odot> g \<equiv> \<lambda>x. (f x, g x)" |
31 "f \<odot> g \<equiv> \<lambda>x. (f x, g x)" |
32 |
32 |
33 lemma coiter_pair_fun_lab: "lab (treeFI_unf_coiter (f \<odot> g) t) = f t" |
33 lemma coiter_pair_fun_lab: "lab (treeFI_unf_coiter (f \<odot> g) t) = f t" |
34 unfolding lab_def pair_fun_def treeFI.unf_coiter treeFIBNF_map_def by simp |
34 unfolding lab_def pair_fun_def treeFI.unf_coiter pre_treeFI_map_def by simp |
35 |
35 |
36 lemma coiter_pair_fun_sub: "sub (treeFI_unf_coiter (f \<odot> g) t) = listF_map (treeFI_unf_coiter (f \<odot> g)) (g t)" |
36 lemma coiter_pair_fun_sub: "sub (treeFI_unf_coiter (f \<odot> g) t) = listF_map (treeFI_unf_coiter (f \<odot> g)) (g t)" |
37 unfolding sub_def pair_fun_def treeFI.unf_coiter treeFIBNF_map_def by simp |
37 unfolding sub_def pair_fun_def treeFI.unf_coiter pre_treeFI_map_def by simp |
38 |
38 |
39 (* Tree reverse:*) |
39 (* Tree reverse:*) |
40 definition "trev \<equiv> treeFI_unf_coiter (lab \<odot> lrev o sub)" |
40 definition "trev \<equiv> treeFI_unf_coiter (lab \<odot> lrev o sub)" |
41 |
41 |
42 lemma trev_simps1[simp]: "lab (trev t) = lab t" |
42 lemma trev_simps1[simp]: "lab (trev t) = lab t" |
57 let ?zs = "zipp (sub a) (sub b)" |
57 let ?zs = "zipp (sub a) (sub b)" |
58 let ?z = "(lab a, ?zs)" |
58 let ?z = "(lab a, ?zs)" |
59 assume "phi a b" |
59 assume "phi a b" |
60 with step have step': "lab a = lab b" "lengthh (sub a) = lengthh (sub b)" |
60 with step have step': "lab a = lab b" "lengthh (sub a) = lengthh (sub b)" |
61 "\<forall>i < lengthh (sub a). phi (nthh (sub a) i) (nthh (sub b) i)" by auto |
61 "\<forall>i < lengthh (sub a). phi (nthh (sub a) i) (nthh (sub b) i)" by auto |
62 hence "treeFIBNF_map id fst ?z = treeFI_unf a" "treeFIBNF_map id snd ?z = treeFI_unf b" |
62 hence "pre_treeFI_map id fst ?z = treeFI_unf a" "pre_treeFI_map id snd ?z = treeFI_unf b" |
63 unfolding treeFIBNF_map_def by auto |
63 unfolding pre_treeFI_map_def by auto |
64 moreover have "\<forall>(x, y) \<in> treeFIBNF_set2 ?z. phi x y" |
64 moreover have "\<forall>(x, y) \<in> pre_treeFI_set2 ?z. phi x y" |
65 proof safe |
65 proof safe |
66 fix z1 z2 |
66 fix z1 z2 |
67 assume "(z1, z2) \<in> treeFIBNF_set2 ?z" |
67 assume "(z1, z2) \<in> pre_treeFI_set2 ?z" |
68 hence "(z1, z2) \<in> listF_set ?zs" by auto |
68 hence "(z1, z2) \<in> listF_set ?zs" by auto |
69 hence "\<exists>i < lengthh ?zs. nthh ?zs i = (z1, z2)" by auto |
69 hence "\<exists>i < lengthh ?zs. nthh ?zs i = (z1, z2)" by auto |
70 with step'(2) obtain i where "i < lengthh (sub a)" |
70 with step'(2) obtain i where "i < lengthh (sub a)" |
71 "nthh (sub a) i = z1" "nthh (sub b) i = z2" by auto |
71 "nthh (sub a) i = z1" "nthh (sub b) i = z2" by auto |
72 with step'(3) show "phi z1 z2" by auto |
72 with step'(3) show "phi z1 z2" by auto |
73 qed |
73 qed |
74 ultimately show "\<exists>z. |
74 ultimately show "\<exists>z. |
75 (treeFIBNF_map id fst z = treeFI_unf a \<and> |
75 (pre_treeFI_map id fst z = treeFI_unf a \<and> |
76 treeFIBNF_map id snd z = treeFI_unf b) \<and> |
76 pre_treeFI_map id snd z = treeFI_unf b) \<and> |
77 (\<forall>x y. (x, y) \<in> treeFIBNF_set2 z \<longrightarrow> phi x y)" by blast |
77 (\<forall>x y. (x, y) \<in> pre_treeFI_set2 z \<longrightarrow> phi x y)" by blast |
78 qed |
78 qed |
79 |
79 |
80 lemma trev_trev: "trev (trev tr) = tr" |
80 lemma trev_trev: "trev (trev tr) = tr" |
81 by (rule treeFI_coinduct[of "%a b. trev (trev b) = a"]) auto |
81 by (rule treeFI_coinduct[of "%a b. trev (trev b) = a"]) auto |
82 |
82 |