equal
deleted
inserted
replaced
70 abbreviation |
70 abbreviation |
71 rel_conj (infixr "OOO" 75) |
71 rel_conj (infixr "OOO" 75) |
72 where |
72 where |
73 "r1 OOO r2 \<equiv> r1 OO r2 OO r1" |
73 "r1 OOO r2 \<equiv> r1 OO r2 OO r1" |
74 |
74 |
75 lemma eq_comp_r: "op = OO R OO op = \<equiv> R" |
75 lemma eq_comp_r: |
76 apply (rule eq_reflection) |
76 shows "((op =) OOO R) = R" |
77 apply (rule ext)+ |
77 by (auto simp add: expand_fun_eq) |
78 apply auto |
|
79 done |
|
80 |
78 |
81 section {* Respects predicate *} |
79 section {* Respects predicate *} |
82 |
80 |
83 definition |
81 definition |
84 Respects |
82 Respects |
106 lemma fun_map_id: |
104 lemma fun_map_id: |
107 shows "(id ---> id) = id" |
105 shows "(id ---> id) = id" |
108 by (simp add: expand_fun_eq id_def) |
106 by (simp add: expand_fun_eq id_def) |
109 |
107 |
110 lemma fun_rel_eq: |
108 lemma fun_rel_eq: |
111 shows "(op =) ===> (op =) \<equiv> (op =)" |
109 shows "((op =) ===> (op =)) = (op =)" |
112 by (rule eq_reflection) (simp add: expand_fun_eq) |
110 by (simp add: expand_fun_eq) |
113 |
111 |
114 lemma fun_rel_id: |
112 lemma fun_rel_id: |
115 assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)" |
113 assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)" |
116 shows "(R1 ===> R2) f g" |
114 shows "(R1 ===> R2) f g" |
117 using a by simp |
115 using a by simp |
394 by metis |
392 by metis |
395 |
393 |
396 lemma babs_prs: |
394 lemma babs_prs: |
397 assumes q1: "Quotient R1 Abs1 Rep1" |
395 assumes q1: "Quotient R1 Abs1 Rep1" |
398 and q2: "Quotient R2 Abs2 Rep2" |
396 and q2: "Quotient R2 Abs2 Rep2" |
399 shows "(Rep1 ---> Abs2) (Babs (Respects R1) ((Abs1 ---> Rep2) f)) \<equiv> f" |
397 shows "((Rep1 ---> Abs2) (Babs (Respects R1) ((Abs1 ---> Rep2) f))) = f" |
400 apply(rule eq_reflection) |
398 apply (rule ext) |
401 apply(rule ext) |
399 apply (simp) |
402 apply simp |
|
403 apply (subgoal_tac "Rep1 x \<in> Respects R1") |
400 apply (subgoal_tac "Rep1 x \<in> Respects R1") |
404 apply (simp add: Babs_def Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) |
401 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]) |
402 apply (simp add: in_respects Quotient_rel_rep[OF q1]) |
406 done |
403 done |
407 |
404 |