equal
deleted
inserted
replaced
26 |
26 |
27 lemma dtor[simp]: "treeFsetI_dtor t = (lab t, sub t)" |
27 lemma dtor[simp]: "treeFsetI_dtor t = (lab t, sub t)" |
28 unfolding lab_def sub_def by simp |
28 unfolding lab_def sub_def by simp |
29 |
29 |
30 lemma unfold_pair_fun_lab: "lab (treeFsetI_dtor_unfold (f \<odot> g) t) = f t" |
30 lemma unfold_pair_fun_lab: "lab (treeFsetI_dtor_unfold (f \<odot> g) t) = f t" |
31 unfolding lab_def pair_fun_def treeFsetI.dtor_unfolds pre_treeFsetI_map_def by simp |
31 unfolding lab_def pair_fun_def treeFsetI.dtor_unfold pre_treeFsetI_map_def by simp |
32 |
32 |
33 lemma unfold_pair_fun_sub: "sub (treeFsetI_dtor_unfold (f \<odot> g) t) = map_fset (treeFsetI_dtor_unfold (f \<odot> g)) (g t)" |
33 lemma unfold_pair_fun_sub: "sub (treeFsetI_dtor_unfold (f \<odot> g) t) = map_fset (treeFsetI_dtor_unfold (f \<odot> g)) (g t)" |
34 unfolding sub_def pair_fun_def treeFsetI.dtor_unfolds pre_treeFsetI_map_def by simp |
34 unfolding sub_def pair_fun_def treeFsetI.dtor_unfold pre_treeFsetI_map_def by simp |
35 |
35 |
36 (* tree map (contrived example): *) |
36 (* tree map (contrived example): *) |
37 definition "tmap f \<equiv> treeFsetI_dtor_unfold (f o lab \<odot> sub)" |
37 definition "tmap f \<equiv> treeFsetI_dtor_unfold (f o lab \<odot> sub)" |
38 |
38 |
39 lemma tmap_simps1[simp]: "lab (tmap f t) = f (lab t)" |
39 lemma tmap_simps1[simp]: "lab (tmap f t) = f (lab t)" |