127 lemma prod_rel_apply [simp]: |
127 lemma prod_rel_apply [simp]: |
128 "prod_rel R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d" |
128 "prod_rel R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d" |
129 by (simp add: prod_rel_def) |
129 by (simp add: prod_rel_def) |
130 |
130 |
131 bnf "'a \<times> 'b" |
131 bnf "'a \<times> 'b" |
132 map: map_pair |
132 map: map_prod |
133 sets: fsts snds |
133 sets: fsts snds |
134 bd: natLeq |
134 bd: natLeq |
135 rel: prod_rel |
135 rel: prod_rel |
136 proof (unfold prod_set_defs) |
136 proof (unfold prod_set_defs) |
137 show "map_pair id id = id" by (rule map_pair.id) |
137 show "map_prod id id = id" by (rule map_prod.id) |
138 next |
138 next |
139 fix f1 f2 g1 g2 |
139 fix f1 f2 g1 g2 |
140 show "map_pair (g1 o f1) (g2 o f2) = map_pair g1 g2 o map_pair f1 f2" |
140 show "map_prod (g1 o f1) (g2 o f2) = map_prod g1 g2 o map_prod f1 f2" |
141 by (rule map_pair.comp[symmetric]) |
141 by (rule map_prod.comp[symmetric]) |
142 next |
142 next |
143 fix x f1 f2 g1 g2 |
143 fix x f1 f2 g1 g2 |
144 assume "\<And>z. z \<in> {fst x} \<Longrightarrow> f1 z = g1 z" "\<And>z. z \<in> {snd x} \<Longrightarrow> f2 z = g2 z" |
144 assume "\<And>z. z \<in> {fst x} \<Longrightarrow> f1 z = g1 z" "\<And>z. z \<in> {snd x} \<Longrightarrow> f2 z = g2 z" |
145 thus "map_pair f1 f2 x = map_pair g1 g2 x" by (cases x) simp |
145 thus "map_prod f1 f2 x = map_prod g1 g2 x" by (cases x) simp |
146 next |
146 next |
147 fix f1 f2 |
147 fix f1 f2 |
148 show "(\<lambda>x. {fst x}) o map_pair f1 f2 = image f1 o (\<lambda>x. {fst x})" |
148 show "(\<lambda>x. {fst x}) o map_prod f1 f2 = image f1 o (\<lambda>x. {fst x})" |
149 by (rule ext, unfold o_apply) simp |
149 by (rule ext, unfold o_apply) simp |
150 next |
150 next |
151 fix f1 f2 |
151 fix f1 f2 |
152 show "(\<lambda>x. {snd x}) o map_pair f1 f2 = image f2 o (\<lambda>x. {snd x})" |
152 show "(\<lambda>x. {snd x}) o map_prod f1 f2 = image f2 o (\<lambda>x. {snd x})" |
153 by (rule ext, unfold o_apply) simp |
153 by (rule ext, unfold o_apply) simp |
154 next |
154 next |
155 show "card_order natLeq" by (rule natLeq_card_order) |
155 show "card_order natLeq" by (rule natLeq_card_order) |
156 next |
156 next |
157 show "cinfinite natLeq" by (rule natLeq_cinfinite) |
157 show "cinfinite natLeq" by (rule natLeq_cinfinite) |
167 fix R1 R2 S1 S2 |
167 fix R1 R2 S1 S2 |
168 show "prod_rel R1 R2 OO prod_rel S1 S2 \<le> prod_rel (R1 OO S1) (R2 OO S2)" by auto |
168 show "prod_rel R1 R2 OO prod_rel S1 S2 \<le> prod_rel (R1 OO S1) (R2 OO S2)" by auto |
169 next |
169 next |
170 fix R S |
170 fix R S |
171 show "prod_rel R S = |
171 show "prod_rel R S = |
172 (Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_pair fst fst))\<inverse>\<inverse> OO |
172 (Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_prod fst fst))\<inverse>\<inverse> OO |
173 Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_pair snd snd)" |
173 Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_prod snd snd)" |
174 unfolding prod_set_defs prod_rel_def Grp_def relcompp.simps conversep.simps fun_eq_iff |
174 unfolding prod_set_defs prod_rel_def Grp_def relcompp.simps conversep.simps fun_eq_iff |
175 by auto |
175 by auto |
176 qed |
176 qed |
177 |
177 |
178 bnf "'a \<Rightarrow> 'b" |
178 bnf "'a \<Rightarrow> 'b" |