equal
deleted
inserted
replaced
119 abbreviation |
119 abbreviation |
120 fun_map_syn (infixr "--->" 55) |
120 fun_map_syn (infixr "--->" 55) |
121 where |
121 where |
122 "f ---> g \<equiv> fun_map f g" |
122 "f ---> g \<equiv> fun_map f g" |
123 |
123 |
124 lemma FUN_MAP_I: |
124 lemma fun_map_id: |
125 shows "(id ---> id) = id" |
125 shows "(id ---> id) = id" |
126 by (simp add: expand_fun_eq id_def) |
126 by (simp add: expand_fun_eq id_def) |
127 |
127 |
128 lemma IN_FUN: |
128 (* Not used *) |
|
129 lemma in_fun: |
129 shows "x \<in> ((f ---> g) s) = g (f x \<in> s)" |
130 shows "x \<in> ((f ---> g) s) = g (f x \<in> s)" |
130 by (simp add: mem_def) |
131 by (simp add: mem_def) |
131 |
132 |
132 fun |
133 fun |
133 fun_rel |
134 fun_rel |
141 |
142 |
142 lemma fun_rel_eq: |
143 lemma fun_rel_eq: |
143 "(op =) ===> (op =) \<equiv> (op =)" |
144 "(op =) ===> (op =) \<equiv> (op =)" |
144 by (rule eq_reflection) (simp add: expand_fun_eq) |
145 by (rule eq_reflection) (simp add: expand_fun_eq) |
145 |
146 |
146 lemma FUN_Quotient: |
147 lemma fun_quotient: |
147 assumes q1: "Quotient R1 abs1 rep1" |
148 assumes q1: "Quotient R1 abs1 rep1" |
148 and q2: "Quotient R2 abs2 rep2" |
149 and q2: "Quotient R2 abs2 rep2" |
149 shows "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)" |
150 shows "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)" |
150 proof - |
151 proof - |
151 have "\<forall>a. (rep1 ---> abs2) ((abs1 ---> rep2) a) = a" |
152 have "\<forall>a. (rep1 ---> abs2) ((abs1 ---> rep2) a) = a" |
222 lemma fun_rel_EQ_REL: |
223 lemma fun_rel_EQ_REL: |
223 assumes q1: "Quotient R1 Abs1 Rep1" |
224 assumes q1: "Quotient R1 Abs1 Rep1" |
224 and q2: "Quotient R2 Abs2 Rep2" |
225 and q2: "Quotient R2 Abs2 Rep2" |
225 shows "(R1 ===> R2) f g = ((Respects (R1 ===> R2) f) \<and> (Respects (R1 ===> R2) g) |
226 shows "(R1 ===> R2) f g = ((Respects (R1 ===> R2) f) \<and> (Respects (R1 ===> R2) g) |
226 \<and> ((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g))" |
227 \<and> ((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g))" |
227 using FUN_Quotient[OF q1 q2] unfolding Respects_def Quotient_def expand_fun_eq |
228 using fun_quotient[OF q1 q2] unfolding Respects_def Quotient_def expand_fun_eq |
228 by blast |
229 by blast |
229 |
230 |
230 (* TODO: it is the same as APPLY_RSP *) |
231 (* TODO: it is the same as APPLY_RSP *) |
231 (* q1 and q2 not used; see next lemma *) |
232 (* q1 and q2 not used; see next lemma *) |
232 lemma fun_rel_MP: |
233 lemma fun_rel_MP: |
244 and q2: "Quotient R2 Abs2 Rep2" |
245 and q2: "Quotient R2 Abs2 Rep2" |
245 and r1: "Respects (R1 ===> R2) f" |
246 and r1: "Respects (R1 ===> R2) f" |
246 and r2: "Respects (R1 ===> R2) g" |
247 and r2: "Respects (R1 ===> R2) g" |
247 shows "((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g) = (\<forall>x y. R1 x y \<longrightarrow> R2 (f x) (g y))" |
248 shows "((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g) = (\<forall>x y. R1 x y \<longrightarrow> R2 (f x) (g y))" |
248 apply(rule_tac iffI) |
249 apply(rule_tac iffI) |
249 using FUN_Quotient[OF q1 q2] r1 r2 unfolding Quotient_def Respects_def |
250 using fun_quotient[OF q1 q2] r1 r2 unfolding Quotient_def Respects_def |
250 apply(metis fun_rel_IMP) |
251 apply(metis fun_rel_IMP) |
251 using r1 unfolding Respects_def expand_fun_eq |
252 using r1 unfolding Respects_def expand_fun_eq |
252 apply(simp (no_asm_use)) |
253 apply(simp (no_asm_use)) |
253 apply(metis Quotient_REL[OF q2] Quotient_REL_REP[OF q1]) |
254 apply(metis Quotient_REL[OF q2] Quotient_REL_REP[OF q1]) |
254 done |
255 done |