equal
deleted
inserted
replaced
28 unfolding lab_def sub_def by simp |
28 unfolding lab_def sub_def by simp |
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_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.coiter treeFIBNF_map_def by simp |
34 unfolding lab_def pair_fun_def treeFI.unf_coiter treeFIBNF_map_def by simp |
35 |
35 |
36 lemma coiter_pair_fun_sub: "sub (treeFI_coiter (f \<odot> g) t) = listF_map (treeFI_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.coiter treeFIBNF_map_def by simp |
37 unfolding sub_def pair_fun_def treeFI.unf_coiter treeFIBNF_map_def by simp |
38 |
38 |
39 (* Tree reverse:*) |
39 (* Tree reverse:*) |
40 definition "trev \<equiv> treeFI_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" |
43 unfolding trev_def by (simp add: coiter_pair_fun_lab) |
43 unfolding trev_def by (simp add: coiter_pair_fun_lab) |
44 |
44 |
45 lemma trev_simps2[simp]: "sub (trev t) = listF_map trev (lrev (sub t))" |
45 lemma trev_simps2[simp]: "sub (trev t) = listF_map trev (lrev (sub t))" |