equal
deleted
inserted
replaced
20 |
20 |
21 definition zimage :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a zet \<Rightarrow> 'b zet" where |
21 definition zimage :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a zet \<Rightarrow> 'b zet" where |
22 "zimage f A == Abs_zet (image f (Rep_zet A))" |
22 "zimage f A == Abs_zet (image f (Rep_zet A))" |
23 |
23 |
24 lemma zet_def': "zet = {A :: 'a set | A f z. inj_on f A \<and> f ` A = explode z}" |
24 lemma zet_def': "zet = {A :: 'a set | A f z. inj_on f A \<and> f ` A = explode z}" |
25 apply (rule set_ext) |
25 apply (rule set_eqI) |
26 apply (auto simp add: zet_def) |
26 apply (auto simp add: zet_def) |
27 apply (rule_tac x=f in exI) |
27 apply (rule_tac x=f in exI) |
28 apply auto |
28 apply auto |
29 apply (rule_tac x="Sep z (\<lambda> y. y \<in> (f ` x))" in exI) |
29 apply (rule_tac x="Sep z (\<lambda> y. y \<in> (f ` x))" in exI) |
30 apply (auto simp add: explode_def Sep) |
30 apply (auto simp add: explode_def Sep) |
116 |
116 |
117 definition zsubset :: "'a zet \<Rightarrow> 'a zet \<Rightarrow> bool" where |
117 definition zsubset :: "'a zet \<Rightarrow> 'a zet \<Rightarrow> bool" where |
118 "zsubset a b \<equiv> ! x. zin x a \<longrightarrow> zin x b" |
118 "zsubset a b \<equiv> ! x. zin x a \<longrightarrow> zin x b" |
119 |
119 |
120 lemma explode_union: "explode (union a b) = (explode a) \<union> (explode b)" |
120 lemma explode_union: "explode (union a b) = (explode a) \<union> (explode b)" |
121 apply (rule set_ext) |
121 apply (rule set_eqI) |
122 apply (simp add: explode_def union) |
122 apply (simp add: explode_def union) |
123 done |
123 done |
124 |
124 |
125 lemma Rep_zet_zunion: "Rep_zet (zunion a b) = (Rep_zet a) \<union> (Rep_zet b)" |
125 lemma Rep_zet_zunion: "Rep_zet (zunion a b) = (Rep_zet a) \<union> (Rep_zet b)" |
126 proof - |
126 proof - |
161 |
161 |
162 lemma zimage_zexplode_eq: "zimage f (zexplode z) = zexplode (Repl z f)" |
162 lemma zimage_zexplode_eq: "zimage f (zexplode z) = zexplode (Repl z f)" |
163 by (simp add: zet_ext_eq zin_zexplode_eq Repl zimage_iff) |
163 by (simp add: zet_ext_eq zin_zexplode_eq Repl zimage_iff) |
164 |
164 |
165 lemma range_explode_eq_zet: "range explode = zet" |
165 lemma range_explode_eq_zet: "range explode = zet" |
166 apply (rule set_ext) |
166 apply (rule set_eqI) |
167 apply (auto simp add: explode_mem_zet) |
167 apply (auto simp add: explode_mem_zet) |
168 apply (drule image_zet_rep) |
168 apply (drule image_zet_rep) |
169 apply (simp add: image_def) |
169 apply (simp add: image_def) |
170 apply auto |
170 apply auto |
171 apply (rule_tac x=z in exI) |
171 apply (rule_tac x=z in exI) |