186 unfolding prod_set_defs rel_prod_inject relcompp.simps conversep.simps fun_eq_iff |
186 unfolding prod_set_defs rel_prod_inject relcompp.simps conversep.simps fun_eq_iff |
187 by auto |
187 by auto |
188 qed auto |
188 qed auto |
189 |
189 |
190 bnf "'a \<Rightarrow> 'b" |
190 bnf "'a \<Rightarrow> 'b" |
191 map: "op \<circ>" |
191 map: "(\<circ>)" |
192 sets: range |
192 sets: range |
193 bd: "natLeq +c |UNIV :: 'a set|" |
193 bd: "natLeq +c |UNIV :: 'a set|" |
194 rel: "rel_fun op =" |
194 rel: "rel_fun (=)" |
195 pred: "pred_fun (\<lambda>_. True)" |
195 pred: "pred_fun (\<lambda>_. True)" |
196 proof |
196 proof |
197 fix f show "id \<circ> f = id f" by simp |
197 fix f show "id \<circ> f = id f" by simp |
198 next |
198 next |
199 fix f g show "op \<circ> (g \<circ> f) = op \<circ> g \<circ> op \<circ> f" |
199 fix f g show "(\<circ>) (g \<circ> f) = (\<circ>) g \<circ> (\<circ>) f" |
200 unfolding comp_def[abs_def] .. |
200 unfolding comp_def[abs_def] .. |
201 next |
201 next |
202 fix x f g |
202 fix x f g |
203 assume "\<And>z. z \<in> range x \<Longrightarrow> f z = g z" |
203 assume "\<And>z. z \<in> range x \<Longrightarrow> f z = g z" |
204 thus "f \<circ> x = g \<circ> x" by auto |
204 thus "f \<circ> x = g \<circ> x" by auto |
205 next |
205 next |
206 fix f show "range \<circ> op \<circ> f = op ` f \<circ> range" |
206 fix f show "range \<circ> (\<circ>) f = (`) f \<circ> range" |
207 by (auto simp add: fun_eq_iff) |
207 by (auto simp add: fun_eq_iff) |
208 next |
208 next |
209 show "card_order (natLeq +c |UNIV| )" (is "_ (_ +c ?U)") |
209 show "card_order (natLeq +c |UNIV| )" (is "_ (_ +c ?U)") |
210 apply (rule card_order_csum) |
210 apply (rule card_order_csum) |
211 apply (rule natLeq_card_order) |
211 apply (rule natLeq_card_order) |
220 have "|range f| \<le>o | (UNIV::'d set) |" (is "_ \<le>o ?U") by (rule card_of_image) |
220 have "|range f| \<le>o | (UNIV::'d set) |" (is "_ \<le>o ?U") by (rule card_of_image) |
221 also have "?U \<le>o natLeq +c ?U" by (rule ordLeq_csum2) (rule card_of_Card_order) |
221 also have "?U \<le>o natLeq +c ?U" by (rule ordLeq_csum2) (rule card_of_Card_order) |
222 finally show "|range f| \<le>o natLeq +c ?U" . |
222 finally show "|range f| \<le>o natLeq +c ?U" . |
223 next |
223 next |
224 fix R S |
224 fix R S |
225 show "rel_fun op = R OO rel_fun op = S \<le> rel_fun op = (R OO S)" by (auto simp: rel_fun_def) |
225 show "rel_fun (=) R OO rel_fun (=) S \<le> rel_fun (=) (R OO S)" by (auto simp: rel_fun_def) |
226 next |
226 next |
227 fix R |
227 fix R |
228 show "rel_fun op = R = (\<lambda>x y. |
228 show "rel_fun (=) R = (\<lambda>x y. |
229 \<exists>z. range z \<subseteq> {(x, y). R x y} \<and> fst \<circ> z = x \<and> snd \<circ> z = y)" |
229 \<exists>z. range z \<subseteq> {(x, y). R x y} \<and> fst \<circ> z = x \<and> snd \<circ> z = y)" |
230 unfolding rel_fun_def subset_iff by (force simp: fun_eq_iff[symmetric]) |
230 unfolding rel_fun_def subset_iff by (force simp: fun_eq_iff[symmetric]) |
231 qed (auto simp: pred_fun_def) |
231 qed (auto simp: pred_fun_def) |
232 |
232 |
233 end |
233 end |