47 |
47 |
48 lemma eq_imp_rel: |
48 lemma eq_imp_rel: |
49 shows "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b" |
49 shows "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b" |
50 by (simp add: equivp_reflp) |
50 by (simp add: equivp_reflp) |
51 |
51 |
|
52 lemma identity_equivp: |
|
53 shows "equivp (op =)" |
|
54 unfolding equivp_def |
|
55 by auto |
|
56 |
|
57 |
52 text {* Partial equivalences: not yet used anywhere *} |
58 text {* Partial equivalences: not yet used anywhere *} |
53 definition |
59 definition |
54 "part_equivp E \<equiv> (\<exists>x. E x x) \<and> (\<forall>x y. E x y = (E x x \<and> E y y \<and> (E x = E y)))" |
60 "part_equivp E \<equiv> (\<exists>x. E x x) \<and> (\<forall>x y. E x y = (E x x \<and> E y y \<and> (E x = E y)))" |
55 |
61 |
56 lemma equivp_IMP_part_equivp: |
62 lemma equivp_implies_part_equivp: |
57 assumes a: "equivp E" |
63 assumes a: "equivp E" |
58 shows "part_equivp E" |
64 shows "part_equivp E" |
59 using a |
65 using a |
60 unfolding equivp_def part_equivp_def |
66 unfolding equivp_def part_equivp_def |
61 by auto |
67 by auto |
63 text {* Composition of Relations *} |
69 text {* Composition of Relations *} |
64 abbreviation |
70 abbreviation |
65 rel_conj (infixr "OOO" 75) |
71 rel_conj (infixr "OOO" 75) |
66 where |
72 where |
67 "r1 OOO r2 \<equiv> r1 OO r2 OO r1" |
73 "r1 OOO r2 \<equiv> r1 OO r2 OO r1" |
|
74 |
|
75 lemma eq_comp_r: "op = OO R OO op = \<equiv> R" |
|
76 apply (rule eq_reflection) |
|
77 apply (rule ext)+ |
|
78 apply auto |
|
79 done |
|
80 |
|
81 section {* Respects predicate *} |
|
82 |
|
83 definition |
|
84 Respects |
|
85 where |
|
86 "Respects R x \<equiv> (R x x)" |
|
87 |
|
88 lemma in_respects: |
|
89 shows "(x \<in> Respects R) = R x x" |
|
90 unfolding mem_def Respects_def |
|
91 by simp |
|
92 |
|
93 section {* Function map and function relation *} |
|
94 |
|
95 definition |
|
96 fun_map (infixr "--->" 55) |
|
97 where |
|
98 [simp]: "fun_map f g h x = g (h (f x))" |
|
99 |
|
100 definition |
|
101 fun_rel (infixr "===>" 55) |
|
102 where |
|
103 [simp]: "fun_rel E1 E2 f g = (\<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))" |
|
104 |
|
105 |
|
106 lemma fun_map_id: |
|
107 shows "(id ---> id) = id" |
|
108 by (simp add: expand_fun_eq id_def) |
|
109 |
|
110 lemma fun_rel_eq: |
|
111 shows "(op =) ===> (op =) \<equiv> (op =)" |
|
112 by (rule eq_reflection) (simp add: expand_fun_eq) |
|
113 |
|
114 lemma fun_rel_id: |
|
115 assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)" |
|
116 shows "(R1 ===> R2) f g" |
|
117 using a by simp |
|
118 |
|
119 lemma fun_rel_id_asm: |
|
120 assumes a: "\<And>x y. R1 x y \<Longrightarrow> (A \<longrightarrow> R2 (f x) (g y))" |
|
121 shows "A \<longrightarrow> (R1 ===> R2) f g" |
|
122 using a by auto |
|
123 |
68 |
124 |
69 section {* Quotient Predicate *} |
125 section {* Quotient Predicate *} |
70 |
126 |
71 definition |
127 definition |
72 "Quotient E Abs Rep \<equiv> |
128 "Quotient E Abs Rep \<equiv> |
123 assumes a: "Quotient E Abs Rep" |
179 assumes a: "Quotient E Abs Rep" |
124 shows "transp E" |
180 shows "transp E" |
125 using a unfolding Quotient_def transp_def |
181 using a unfolding Quotient_def transp_def |
126 by metis |
182 by metis |
127 |
183 |
128 section {* Lemmas about (op =) *} |
|
129 |
|
130 lemma identity_equivp: |
|
131 shows "equivp (op =)" |
|
132 unfolding equivp_def |
|
133 by auto |
|
134 |
|
135 lemma identity_quotient: |
184 lemma identity_quotient: |
136 shows "Quotient (op =) id id" |
185 shows "Quotient (op =) id id" |
137 unfolding Quotient_def id_def |
186 unfolding Quotient_def id_def |
138 by blast |
187 by blast |
139 |
|
140 section {* Function map and function relation *} |
|
141 |
|
142 definition |
|
143 fun_map (infixr "--->" 55) |
|
144 where |
|
145 [simp]: "fun_map f g h x = g (h (f x))" |
|
146 |
|
147 definition |
|
148 fun_rel (infixr "===>" 55) |
|
149 where |
|
150 [simp]: "fun_rel E1 E2 f g = (\<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))" |
|
151 |
|
152 |
|
153 lemma fun_map_id: |
|
154 shows "(id ---> id) = id" |
|
155 by (simp add: expand_fun_eq id_def) |
|
156 |
|
157 lemma fun_rel_eq: |
|
158 shows "(op =) ===> (op =) \<equiv> (op =)" |
|
159 by (rule eq_reflection) (simp add: expand_fun_eq) |
|
160 |
188 |
161 lemma fun_quotient: |
189 lemma fun_quotient: |
162 assumes q1: "Quotient R1 abs1 rep1" |
190 assumes q1: "Quotient R1 abs1 rep1" |
163 and q2: "Quotient R2 abs2 rep2" |
191 and q2: "Quotient R2 abs2 rep2" |
164 shows "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)" |
192 shows "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)" |
190 ultimately |
218 ultimately |
191 show "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)" |
219 show "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)" |
192 unfolding Quotient_def by blast |
220 unfolding Quotient_def by blast |
193 qed |
221 qed |
194 |
222 |
195 section {* Respects predicate *} |
223 lemma abs_o_rep: |
196 |
224 assumes a: "Quotient R Abs Rep" |
197 definition |
225 shows "Abs o Rep = id" |
198 Respects |
226 apply(rule ext) |
199 where |
227 apply(simp add: Quotient_abs_rep[OF a]) |
200 "Respects R x \<equiv> (R x x)" |
228 done |
201 |
|
202 lemma in_respects: |
|
203 shows "(x \<in> Respects R) = R x x" |
|
204 unfolding mem_def Respects_def by simp |
|
205 |
229 |
206 lemma equals_rsp: |
230 lemma equals_rsp: |
207 assumes q: "Quotient R Abs Rep" |
231 assumes q: "Quotient R Abs Rep" |
208 and a: "R xa xb" "R ya yb" |
232 and a: "R xa xb" "R ya yb" |
209 shows "R xa ya = R xb yb" |
233 shows "R xa ya = R xb yb" |
228 |
252 |
229 lemma rep_abs_rsp: |
253 lemma rep_abs_rsp: |
230 assumes q: "Quotient R Abs Rep" |
254 assumes q: "Quotient R Abs Rep" |
231 and a: "R x1 x2" |
255 and a: "R x1 x2" |
232 shows "R x1 (Rep (Abs x2))" |
256 shows "R x1 (Rep (Abs x2))" |
233 using q a by (metis Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q]) |
257 using a |
|
258 by (metis Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q]) |
234 |
259 |
235 lemma rep_abs_rsp_left: |
260 lemma rep_abs_rsp_left: |
236 assumes q: "Quotient R Abs Rep" |
261 assumes q: "Quotient R Abs Rep" |
237 and a: "R x1 x2" |
262 and a: "R x1 x2" |
238 shows "R (Rep (Abs x1)) x2" |
263 shows "R (Rep (Abs x1)) x2" |
239 using q a by (metis Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q]) |
264 using a |
|
265 by (metis Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q]) |
240 |
266 |
241 (* In the following theorem R1 can be instantiated with anything, |
267 (* In the following theorem R1 can be instantiated with anything, |
242 but we know some of the types of the Rep and Abs functions; |
268 but we know some of the types of the Rep and Abs functions; |
243 so by solving Quotient assumptions we can get a unique R1 that |
269 so by solving Quotient assumptions we can get a unique R1 that |
244 will be provable; which is why we need to use apply_rsp and |
270 will be provable; which is why we need to use apply_rsp and |
253 lemma apply_rsp': |
279 lemma apply_rsp': |
254 assumes a: "(R1 ===> R2) f g" "R1 x y" |
280 assumes a: "(R1 ===> R2) f g" "R1 x y" |
255 shows "R2 (f x) (g y)" |
281 shows "R2 (f x) (g y)" |
256 using a by simp |
282 using a by simp |
257 |
283 |
258 (* Set of lemmas for regularisation of ball and bex *) |
284 section {* lemmas for regularisation of ball and bex *} |
259 |
285 |
260 lemma ball_reg_eqv: |
286 lemma ball_reg_eqv: |
261 fixes P :: "'a \<Rightarrow> bool" |
287 fixes P :: "'a \<Rightarrow> bool" |
262 assumes a: "equivp R" |
288 assumes a: "equivp R" |
263 shows "Ball (Respects R) P = (All P)" |
289 shows "Ball (Respects R) P = (All P)" |
347 |
373 |
348 lemma bex_ex_comm: |
374 lemma bex_ex_comm: |
349 "((\<exists>y. \<exists>x. A x y) \<longrightarrow> (\<exists>y. \<exists>x\<in>P. B x y)) \<Longrightarrow> ((\<exists>x. \<exists>y. A x y) \<longrightarrow> (\<exists>x\<in>P. \<exists>y. B x y))" |
375 "((\<exists>y. \<exists>x. A x y) \<longrightarrow> (\<exists>y. \<exists>x\<in>P. B x y)) \<Longrightarrow> ((\<exists>x. \<exists>y. A x y) \<longrightarrow> (\<exists>x\<in>P. \<exists>y. B x y))" |
350 by auto |
376 by auto |
351 |
377 |
352 (* Bounded abstraction *) |
378 section {* Bounded abstraction *} |
|
379 |
353 definition |
380 definition |
354 Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" |
381 Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" |
355 where |
382 where |
356 "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)" |
383 "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)" |
357 |
384 |
358 definition |
385 lemma babs_rsp: |
359 Bexeq :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" |
386 assumes q: "Quotient R1 Abs1 Rep1" |
360 where |
387 and a: "(R1 ===> R2) f g" |
361 "Bexeq R P \<equiv> (\<exists>x \<in> Respects R. P x) \<and> (\<forall>x \<in> Respects R. \<forall>y \<in> Respects R. ((P x \<and> P y) \<longrightarrow> (R x y)))" |
388 shows "(R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)" |
|
389 apply (auto simp add: Babs_def) |
|
390 apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1") |
|
391 using a apply (simp add: Babs_def) |
|
392 apply (simp add: in_respects) |
|
393 using Quotient_rel[OF q] |
|
394 by metis |
|
395 |
|
396 lemma babs_prs: |
|
397 assumes q1: "Quotient R1 Abs1 Rep1" |
|
398 and q2: "Quotient R2 Abs2 Rep2" |
|
399 shows "(Rep1 ---> Abs2) (Babs (Respects R1) ((Abs1 ---> Rep2) f)) \<equiv> f" |
|
400 apply(rule eq_reflection) |
|
401 apply(rule ext) |
|
402 apply simp |
|
403 apply (subgoal_tac "Rep1 x \<in> Respects R1") |
|
404 apply (simp add: Babs_def Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) |
|
405 apply (simp add: in_respects Quotient_rel_rep[OF q1]) |
|
406 done |
|
407 |
|
408 lemma babs_simp: |
|
409 assumes q: "Quotient R1 Abs Rep" |
|
410 shows "((R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)) = ((R1 ===> R2) f g)" |
|
411 apply(rule iffI) |
|
412 apply(simp_all only: babs_rsp[OF q]) |
|
413 apply(auto simp add: Babs_def) |
|
414 apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1") |
|
415 apply(metis Babs_def) |
|
416 apply (simp add: in_respects) |
|
417 using Quotient_rel[OF q] |
|
418 by metis |
|
419 |
|
420 (* If a user proves that a particular functional relation |
|
421 is an equivalence this may be useful in regularising *) |
|
422 lemma babs_reg_eqv: |
|
423 shows "equivp R \<Longrightarrow> Babs (Respects R) P = P" |
|
424 by (simp add: expand_fun_eq Babs_def in_respects equivp_reflp) |
|
425 |
362 |
426 |
363 (* 3 lemmas needed for proving repabs_inj *) |
427 (* 3 lemmas needed for proving repabs_inj *) |
364 lemma ball_rsp: |
428 lemma ball_rsp: |
365 assumes a: "(R ===> (op =)) f g" |
429 assumes a: "(R ===> (op =)) f g" |
366 shows "Ball (Respects R) f = Ball (Respects R) g" |
430 shows "Ball (Respects R) f = Ball (Respects R) g" |
375 assumes a: "(R ===> (op =)) f g" |
439 assumes a: "(R ===> (op =)) f g" |
376 shows "(Bex1 (Respects R) f = Bex1 (Respects R) g)" |
440 shows "(Bex1 (Respects R) f = Bex1 (Respects R) g)" |
377 using a |
441 using a |
378 by (simp add: Ex1_def Bex1_def in_respects) auto |
442 by (simp add: Ex1_def Bex1_def in_respects) auto |
379 |
443 |
|
444 (* 3 lemmas needed for cleaning of quantifiers *) |
|
445 lemma all_prs: |
|
446 assumes a: "Quotient R absf repf" |
|
447 shows "Ball (Respects R) ((absf ---> id) f) = All f" |
|
448 using a unfolding Quotient_def Ball_def in_respects fun_map_def id_apply |
|
449 by metis |
|
450 |
|
451 lemma ex_prs: |
|
452 assumes a: "Quotient R absf repf" |
|
453 shows "Bex (Respects R) ((absf ---> id) f) = Ex f" |
|
454 using a unfolding Quotient_def Bex_def in_respects fun_map_def id_apply |
|
455 by metis |
|
456 |
|
457 section {* Bexeq quantifier *} |
|
458 |
|
459 definition |
|
460 Bexeq :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" |
|
461 where |
|
462 "Bexeq R P \<equiv> (\<exists>x \<in> Respects R. P x) \<and> (\<forall>x \<in> Respects R. \<forall>y \<in> Respects R. ((P x \<and> P y) \<longrightarrow> (R x y)))" |
|
463 |
380 (* TODO/FIXME: simplify the repetitions in this proof *) |
464 (* TODO/FIXME: simplify the repetitions in this proof *) |
381 lemma bexeq_rsp: |
465 lemma bexeq_rsp: |
382 assumes a: "Quotient R absf repf" |
466 assumes a: "Quotient R absf repf" |
383 shows "((R ===> op =) ===> op =) (Bexeq R) (Bexeq R)" |
467 shows "((R ===> op =) ===> op =) (Bexeq R) (Bexeq R)" |
384 apply simp |
468 apply simp |
385 unfolding Bexeq_def |
469 unfolding Bexeq_def |
386 apply rule |
470 apply rule |
387 apply rule |
471 apply rule |
388 apply rule |
472 apply rule |
414 apply (erule_tac x="ya" in ballE) |
498 apply (erule_tac x="ya" in ballE) |
415 prefer 2 |
499 prefer 2 |
416 apply (metis) |
500 apply (metis) |
417 apply (metis in_respects) |
501 apply (metis in_respects) |
418 done |
502 done |
419 |
|
420 lemma babs_rsp: |
|
421 assumes q: "Quotient R1 Abs1 Rep1" |
|
422 and a: "(R1 ===> R2) f g" |
|
423 shows "(R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)" |
|
424 apply (auto simp add: Babs_def) |
|
425 apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1") |
|
426 using a apply (simp add: Babs_def) |
|
427 apply (simp add: in_respects) |
|
428 using Quotient_rel[OF q] |
|
429 by metis |
|
430 |
|
431 lemma babs_prs: |
|
432 assumes q1: "Quotient R1 Abs1 Rep1" |
|
433 and q2: "Quotient R2 Abs2 Rep2" |
|
434 shows "(Rep1 ---> Abs2) (Babs (Respects R1) ((Abs1 ---> Rep2) f)) \<equiv> f" |
|
435 apply(rule eq_reflection) |
|
436 apply(rule ext) |
|
437 apply simp |
|
438 apply (subgoal_tac "Rep1 x \<in> Respects R1") |
|
439 apply (simp add: Babs_def Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) |
|
440 apply (simp add: in_respects Quotient_rel_rep[OF q1]) |
|
441 done |
|
442 |
|
443 lemma babs_simp: |
|
444 assumes q: "Quotient R1 Abs Rep" |
|
445 shows "((R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)) = ((R1 ===> R2) f g)" |
|
446 apply(rule iffI) |
|
447 apply(simp_all only: babs_rsp[OF q]) |
|
448 apply(auto simp add: Babs_def) |
|
449 apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1") |
|
450 apply(metis Babs_def) |
|
451 apply (simp add: in_respects) |
|
452 using Quotient_rel[OF q] |
|
453 by metis |
|
454 |
|
455 (* If a user proves that a particular functional relation |
|
456 is an equivalence this may be useful in regularising *) |
|
457 lemma babs_reg_eqv: |
|
458 shows "equivp R \<Longrightarrow> Babs (Respects R) P = P" |
|
459 by (simp add: expand_fun_eq Babs_def in_respects equivp_reflp) |
|
460 |
|
461 (* 3 lemmas needed for cleaning of quantifiers *) |
|
462 lemma all_prs: |
|
463 assumes a: "Quotient R absf repf" |
|
464 shows "Ball (Respects R) ((absf ---> id) f) = All f" |
|
465 using a unfolding Quotient_def Ball_def in_respects fun_map_def id_apply |
|
466 by metis |
|
467 |
|
468 lemma ex_prs: |
|
469 assumes a: "Quotient R absf repf" |
|
470 shows "Bex (Respects R) ((absf ---> id) f) = Ex f" |
|
471 using a unfolding Quotient_def Bex_def in_respects fun_map_def id_apply |
|
472 by metis |
|
473 |
503 |
474 lemma ex1_prs: |
504 lemma ex1_prs: |
475 assumes a: "Quotient R absf repf" |
505 assumes a: "Quotient R absf repf" |
476 shows "((absf ---> id) ---> id) (Bexeq R) f = Ex1 f" |
506 shows "((absf ---> id) ---> id) (Bexeq R) f = Ex1 f" |
477 apply simp |
507 apply simp |
506 apply rule+ |
536 apply rule+ |
507 using a unfolding Quotient_def in_respects |
537 using a unfolding Quotient_def in_respects |
508 apply metis |
538 apply metis |
509 done |
539 done |
510 |
540 |
511 lemma fun_rel_id: |
541 section {* Various respects and preserve lemmas *} |
512 assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)" |
|
513 shows "(R1 ===> R2) f g" |
|
514 using a by simp |
|
515 |
|
516 lemma fun_rel_id_asm: |
|
517 assumes a: "\<And>x y. R1 x y \<Longrightarrow> (A \<longrightarrow> R2 (f x) (g y))" |
|
518 shows "A \<longrightarrow> (R1 ===> R2) f g" |
|
519 using a by auto |
|
520 |
542 |
521 lemma quot_rel_rsp: |
543 lemma quot_rel_rsp: |
522 assumes a: "Quotient R Abs Rep" |
544 assumes a: "Quotient R Abs Rep" |
523 shows "(R ===> R ===> op =) R R" |
545 shows "(R ===> R ===> op =) R R" |
524 apply(rule fun_rel_id)+ |
546 apply(rule fun_rel_id)+ |
573 and a2: "R1 x y" |
595 and a2: "R1 x y" |
574 shows "R2 ((Let x f)::'c) ((Let y g)::'c)" |
596 shows "R2 ((Let x f)::'c) ((Let y g)::'c)" |
575 using apply_rsp[OF q1 a1] a2 by auto |
597 using apply_rsp[OF q1 a1] a2 by auto |
576 |
598 |
577 |
599 |
578 |
|
579 |
|
580 (******************************************) |
600 (******************************************) |
581 (* REST OF THE FILE IS UNUSED (until now) *) |
601 (* REST OF THE FILE IS UNUSED (until now) *) |
582 (******************************************) |
602 (******************************************) |
583 |
603 |
|
604 text {* |
584 lemma in_fun: |
605 lemma in_fun: |
585 shows "x \<in> ((f ---> g) s) = g (f x \<in> s)" |
606 shows "x \<in> ((f ---> g) s) = g (f x \<in> s)" |
586 by (simp add: mem_def) |
607 by (simp add: mem_def) |
587 |
608 |
588 lemma respects_thm: |
609 lemma respects_thm: |
589 shows "Respects (R1 ===> R2) f = (\<forall>x y. R1 x y \<longrightarrow> R2 (f x) (f y))" |
610 shows "Respects (R1 ===> R2) f = (\<forall>x y. R1 x y \<longrightarrow> R2 (f x) (f y))" |
590 unfolding Respects_def |
611 unfolding Respects_def |
591 by (simp add: expand_fun_eq) |
612 by (simp add: expand_fun_eq) |
592 |
613 |
609 assumes a: "Respects (R2 ===> R3) f" |
630 assumes a: "Respects (R2 ===> R3) f" |
610 and b: "Respects (R1 ===> R2) g" |
631 and b: "Respects (R1 ===> R2) g" |
611 shows "Respects (R1 ===> R3) (f o g)" |
632 shows "Respects (R1 ===> R3) (f o g)" |
612 using a b unfolding Respects_def |
633 using a b unfolding Respects_def |
613 by simp |
634 by simp |
614 |
|
615 lemma abs_o_rep: |
|
616 assumes a: "Quotient r absf repf" |
|
617 shows "absf o repf = id" |
|
618 apply(rule ext) |
|
619 apply(simp add: Quotient_abs_rep[OF a]) |
|
620 done |
|
621 |
|
622 lemma eq_comp_r: "op = OO R OO op = \<equiv> R" |
|
623 apply (rule eq_reflection) |
|
624 apply (rule ext)+ |
|
625 apply auto |
|
626 done |
|
627 |
635 |
628 lemma fun_rel_eq_rel: |
636 lemma fun_rel_eq_rel: |
629 assumes q1: "Quotient R1 Abs1 Rep1" |
637 assumes q1: "Quotient R1 Abs1 Rep1" |
630 and q2: "Quotient R2 Abs2 Rep2" |
638 and q2: "Quotient R2 Abs2 Rep2" |
631 shows "(R1 ===> R2) f g = ((Respects (R1 ===> R2) f) \<and> (Respects (R1 ===> R2) g) |
639 shows "(R1 ===> R2) f g = ((Respects (R1 ===> R2) f) \<and> (Respects (R1 ===> R2) g) |