equal
deleted
inserted
replaced
35 lemma image_zet_rep: "A \<in> zet \<Longrightarrow> ? z . g ` A = explode z" |
35 lemma image_zet_rep: "A \<in> zet \<Longrightarrow> ? z . g ` A = explode z" |
36 apply (auto simp add: zet_def') |
36 apply (auto simp add: zet_def') |
37 apply (rule_tac x="Repl z (g o (inv_into A f))" in exI) |
37 apply (rule_tac x="Repl z (g o (inv_into A f))" in exI) |
38 apply (simp add: explode_Repl_eq) |
38 apply (simp add: explode_Repl_eq) |
39 apply (subgoal_tac "explode z = f ` A") |
39 apply (subgoal_tac "explode z = f ` A") |
40 apply (simp_all add: image_compose) |
40 apply (simp_all add: image_comp [symmetric]) |
41 done |
41 done |
42 |
42 |
43 lemma zet_image_mem: |
43 lemma zet_image_mem: |
44 assumes Azet: "A \<in> zet" |
44 assumes Azet: "A \<in> zet" |
45 shows "g ` A \<in> zet" |
45 shows "g ` A \<in> zet" |
56 apply (rule comp_inj_on) |
56 apply (rule comp_inj_on) |
57 apply (rule subset_inj_on[where B=A]) |
57 apply (rule subset_inj_on[where B=A]) |
58 apply (auto simp add: subset injf) |
58 apply (auto simp add: subset injf) |
59 done |
59 done |
60 show ?thesis |
60 show ?thesis |
61 apply (simp add: zet_def' image_compose[symmetric]) |
61 apply (simp add: zet_def' image_comp) |
62 apply (rule exI[where x="?w"]) |
62 apply (rule exI[where x="?w"]) |
63 apply (simp add: injw image_zet_rep Azet) |
63 apply (simp add: injw image_zet_rep Azet) |
64 done |
64 done |
65 qed |
65 qed |
66 |
66 |
108 done |
108 done |
109 |
109 |
110 lemma comp_zimage_eq: "zimage g (zimage f A) = zimage (g o f) A" |
110 lemma comp_zimage_eq: "zimage g (zimage f A) = zimage (g o f) A" |
111 apply (simp add: zimage_def) |
111 apply (simp add: zimage_def) |
112 apply (subst Abs_zet_inverse) |
112 apply (subst Abs_zet_inverse) |
113 apply (simp_all add: image_compose zet_image_mem Rep_zet) |
113 apply (simp_all add: image_comp zet_image_mem Rep_zet) |
114 done |
114 done |
115 |
115 |
116 definition zunion :: "'a zet \<Rightarrow> 'a zet \<Rightarrow> 'a zet" where |
116 definition zunion :: "'a zet \<Rightarrow> 'a zet \<Rightarrow> 'a zet" where |
117 "zunion a b \<equiv> Abs_zet ((Rep_zet a) \<union> (Rep_zet b))" |
117 "zunion a b \<equiv> Abs_zet ((Rep_zet a) \<union> (Rep_zet b))" |
118 |
118 |