equal
deleted
inserted
replaced
135 where |
135 where |
136 "E1 ===> E2 \<equiv> FUN_REL E1 E2" |
136 "E1 ===> E2 \<equiv> FUN_REL E1 E2" |
137 |
137 |
138 lemma FUN_REL_EQ: |
138 lemma FUN_REL_EQ: |
139 "(op =) ===> (op =) \<equiv> (op =)" |
139 "(op =) ===> (op =) \<equiv> (op =)" |
140 by (simp add: expand_fun_eq) |
140 by (rule eq_reflection) (simp add: expand_fun_eq) |
141 |
141 |
142 lemma FUN_QUOTIENT: |
142 lemma FUN_QUOTIENT: |
143 assumes q1: "QUOTIENT R1 abs1 rep1" |
143 assumes q1: "QUOTIENT R1 abs1 rep1" |
144 and q2: "QUOTIENT R2 abs2 rep2" |
144 and q2: "QUOTIENT R2 abs2 rep2" |
145 shows "QUOTIENT (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)" |
145 shows "QUOTIENT (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)" |