equal
deleted
inserted
replaced
94 lemma QUOTIENT_TRANS: |
94 lemma QUOTIENT_TRANS: |
95 assumes a: "QUOTIENT E Abs Rep" |
95 assumes a: "QUOTIENT E Abs Rep" |
96 shows "TRANS E" |
96 shows "TRANS E" |
97 using a unfolding QUOTIENT_def TRANS_def |
97 using a unfolding QUOTIENT_def TRANS_def |
98 by metis |
98 by metis |
|
99 |
|
100 fun |
|
101 prod_rel |
|
102 where |
|
103 "prod_rel r1 r2 = (\<lambda>(a,b) (c,d). r1 a c \<and> r2 b d)" |
99 |
104 |
100 fun |
105 fun |
101 fun_map |
106 fun_map |
102 where |
107 where |
103 "fun_map f g h x = g (h (f x))" |
108 "fun_map f g h x = g (h (f x))" |
396 and a2: "(R1 ===> R2) g1 g2" |
401 and a2: "(R1 ===> R2) g1 g2" |
397 shows "(R1 ===> R3) (f1 o g1) (f2 o g2)" |
402 shows "(R1 ===> R3) (f1 o g1) (f2 o g2)" |
398 using a1 a2 unfolding o_def expand_fun_eq |
403 using a1 a2 unfolding o_def expand_fun_eq |
399 by (auto) |
404 by (auto) |
400 |
405 |
|
406 lemma equiv_res_forall: |
|
407 fixes P :: "'a \<Rightarrow> bool" |
|
408 assumes a: "EQUIV E" |
|
409 shows "Ball (Respects E) P = (All P)" |
|
410 using a by (metis EQUIV_def IN_RESPECTS a) |
|
411 |
|
412 lemma equiv_res_exists: |
|
413 fixes P :: "'a \<Rightarrow> bool" |
|
414 assumes a: "EQUIV E" |
|
415 shows "Bex (Respects E) P = (Ex P)" |
|
416 using a by (metis EQUIV_def IN_RESPECTS a) |
|
417 |
401 end |
418 end |