124 assumes a: "Quotient E Abs Rep" |
124 assumes a: "Quotient E Abs Rep" |
125 shows "transp E" |
125 shows "transp E" |
126 using a unfolding Quotient_def transp_def |
126 using a unfolding Quotient_def transp_def |
127 by metis |
127 by metis |
128 |
128 |
129 fun |
129 definition |
130 fun_map |
130 fun_map (infixr "--->" 55) |
131 where |
131 where |
132 "fun_map f g h x = g (h (f x))" |
132 [simp]: "fun_map f g h x = g (h (f x))" |
133 |
|
134 abbreviation |
|
135 fun_map_syn (infixr "--->" 55) |
|
136 where |
|
137 "f ---> g \<equiv> fun_map f g" |
|
138 |
133 |
139 lemma fun_map_id: |
134 lemma fun_map_id: |
140 shows "(id ---> id) = id" |
135 shows "(id ---> id) = id" |
141 by (simp add: expand_fun_eq id_def) |
136 by (simp add: expand_fun_eq id_def) |
142 |
137 |
143 |
138 definition |
144 fun |
139 fun_rel (infixr "===>" 55) |
145 fun_rel |
|
146 where |
140 where |
147 "fun_rel E1 E2 f g = (\<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))" |
141 [simp]: "fun_rel E1 E2 f g = (\<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))" |
148 |
|
149 abbreviation |
|
150 fun_rel_syn (infixr "===>" 55) |
|
151 where |
|
152 "E1 ===> E2 \<equiv> fun_rel E1 E2" |
|
153 |
142 |
154 lemma fun_rel_eq: |
143 lemma fun_rel_eq: |
155 "(op =) ===> (op =) \<equiv> (op =)" |
144 "(op =) ===> (op =) \<equiv> (op =)" |
156 by (rule eq_reflection) (simp add: expand_fun_eq) |
145 by (rule eq_reflection) (simp add: expand_fun_eq) |
157 |
146 |
451 is an equivalence this may be useful in regularising *) |
440 is an equivalence this may be useful in regularising *) |
452 lemma babs_reg_eqv: |
441 lemma babs_reg_eqv: |
453 shows "equivp R \<Longrightarrow> Babs (Respects R) P = P" |
442 shows "equivp R \<Longrightarrow> Babs (Respects R) P = P" |
454 by (simp add: expand_fun_eq Babs_def in_respects equivp_reflp) |
443 by (simp add: expand_fun_eq Babs_def in_respects equivp_reflp) |
455 |
444 |
456 (* 2 lemmas needed for cleaning of quantifiers *) |
445 (* 3 lemmas needed for cleaning of quantifiers *) |
457 lemma all_prs: |
446 lemma all_prs: |
458 assumes a: "Quotient R absf repf" |
447 assumes a: "Quotient R absf repf" |
459 shows "Ball (Respects R) ((absf ---> id) f) = All f" |
448 shows "Ball (Respects R) ((absf ---> id) f) = All f" |
460 using a unfolding Quotient_def |
449 using a unfolding Quotient_def Ball_def in_respects fun_map_def id_apply |
461 by (metis in_respects fun_map.simps id_apply) |
450 by metis |
462 |
451 |
463 lemma ex_prs: |
452 lemma ex_prs: |
464 assumes a: "Quotient R absf repf" |
453 assumes a: "Quotient R absf repf" |
465 shows "Bex (Respects R) ((absf ---> id) f) = Ex f" |
454 shows "Bex (Respects R) ((absf ---> id) f) = Ex f" |
466 using a unfolding Quotient_def |
455 using a unfolding Quotient_def Bex_def in_respects fun_map_def id_apply |
467 by (metis COMBC_def Collect_def Collect_mem_eq in_respects fun_map.simps id_apply) |
456 by metis |
468 |
457 |
469 lemma ex1_prs: |
458 lemma ex1_prs: |
470 assumes a: "Quotient R absf repf" |
459 assumes a: "Quotient R absf repf" |
471 shows "((absf ---> id) ---> id) (Bexeq R) f = Ex1 f" |
460 shows "((absf ---> id) ---> id) (Bexeq R) f = Ex1 f" |
472 apply simp |
461 apply simp |
637 and q2: "Quotient R2 Abs2 Rep2" |
626 and q2: "Quotient R2 Abs2 Rep2" |
638 and r1: "Respects (R1 ===> R2) f" |
627 and r1: "Respects (R1 ===> R2) f" |
639 and r2: "Respects (R1 ===> R2) g" |
628 and r2: "Respects (R1 ===> R2) g" |
640 shows "((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g) = (\<forall>x y. R1 x y \<longrightarrow> R2 (f x) (g y))" |
629 shows "((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g) = (\<forall>x y. R1 x y \<longrightarrow> R2 (f x) (g y))" |
641 apply(rule_tac iffI) |
630 apply(rule_tac iffI) |
|
631 apply(rule)+ |
|
632 apply (rule apply_rsp'[of "R1" "R2"]) |
|
633 apply(subst Quotient_rel[OF fun_quotient[OF q1 q2]]) |
|
634 apply auto |
642 using fun_quotient[OF q1 q2] r1 r2 unfolding Quotient_def Respects_def |
635 using fun_quotient[OF q1 q2] r1 r2 unfolding Quotient_def Respects_def |
643 apply(metis apply_rsp') |
636 apply (metis let_rsp q1) |
|
637 apply (metis fun_rel_eq_rel let_rsp q1 q2 r2) |
644 using r1 unfolding Respects_def expand_fun_eq |
638 using r1 unfolding Respects_def expand_fun_eq |
645 apply(simp (no_asm_use)) |
639 apply(simp (no_asm_use)) |
646 apply(metis Quotient_rel[OF q2] Quotient_rel_rep[OF q1]) |
640 apply(metis Quotient_rel[OF q2] Quotient_rel_rep[OF q1]) |
647 done |
641 done |
648 |
642 |