equal
deleted
inserted
replaced
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 pre_treeFI_map_def by simp |
34 unfolding lab_def pair_fun_def treeFI.unf_coiters 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 pre_treeFI_map_def by simp |
37 unfolding sub_def pair_fun_def treeFI.unf_coiters 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" |