128 lemma IN_FUN: |
128 lemma IN_FUN: |
129 shows "x \<in> ((f ---> g) s) = g (f x \<in> s)" |
129 shows "x \<in> ((f ---> g) s) = g (f x \<in> s)" |
130 by (simp add: mem_def) |
130 by (simp add: mem_def) |
131 |
131 |
132 fun |
132 fun |
133 FUN_REL |
133 fun_rel |
134 where |
134 where |
135 "FUN_REL E1 E2 f g = (\<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))" |
135 "fun_rel E1 E2 f g = (\<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))" |
136 |
136 |
137 abbreviation |
137 abbreviation |
138 FUN_REL_syn (infixr "===>" 55) |
138 fun_rel_syn (infixr "===>" 55) |
139 where |
139 where |
140 "E1 ===> E2 \<equiv> FUN_REL E1 E2" |
140 "E1 ===> E2 \<equiv> fun_rel E1 E2" |
141 |
141 |
142 lemma FUN_REL_EQ: |
142 lemma fun_rel_eq: |
143 "(op =) ===> (op =) \<equiv> (op =)" |
143 "(op =) ===> (op =) \<equiv> (op =)" |
144 by (rule eq_reflection) (simp add: expand_fun_eq) |
144 by (rule eq_reflection) (simp add: expand_fun_eq) |
145 |
145 |
146 lemma FUN_Quotient: |
146 lemma FUN_Quotient: |
147 assumes q1: "Quotient R1 abs1 rep1" |
147 assumes q1: "Quotient R1 abs1 rep1" |
217 definition |
217 definition |
218 "RES_EXISTS_EQUIV R P \<equiv> (\<exists>x \<in> Respects R. P x) \<and> |
218 "RES_EXISTS_EQUIV R P \<equiv> (\<exists>x \<in> Respects R. P x) \<and> |
219 (\<forall>x\<in> Respects R. \<forall>y\<in> Respects R. P x \<and> P y \<longrightarrow> R x y)" |
219 (\<forall>x\<in> Respects R. \<forall>y\<in> Respects R. P x \<and> P y \<longrightarrow> R x y)" |
220 *) |
220 *) |
221 |
221 |
222 lemma FUN_REL_EQ_REL: |
222 lemma fun_rel_EQ_REL: |
223 assumes q1: "Quotient R1 Abs1 Rep1" |
223 assumes q1: "Quotient R1 Abs1 Rep1" |
224 and q2: "Quotient R2 Abs2 Rep2" |
224 and q2: "Quotient R2 Abs2 Rep2" |
225 shows "(R1 ===> R2) f g = ((Respects (R1 ===> R2) f) \<and> (Respects (R1 ===> R2) g) |
225 shows "(R1 ===> R2) f g = ((Respects (R1 ===> R2) f) \<and> (Respects (R1 ===> R2) g) |
226 \<and> ((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g))" |
226 \<and> ((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g))" |
227 using FUN_Quotient[OF q1 q2] unfolding Respects_def Quotient_def expand_fun_eq |
227 using FUN_Quotient[OF q1 q2] unfolding Respects_def Quotient_def expand_fun_eq |
228 by blast |
228 by blast |
229 |
229 |
230 (* TODO: it is the same as APPLY_RSP *) |
230 (* TODO: it is the same as APPLY_RSP *) |
231 (* q1 and q2 not used; see next lemma *) |
231 (* q1 and q2 not used; see next lemma *) |
232 lemma FUN_REL_MP: |
232 lemma fun_rel_MP: |
233 assumes q1: "Quotient R1 Abs1 Rep1" |
233 assumes q1: "Quotient R1 Abs1 Rep1" |
234 and q2: "Quotient R2 Abs2 Rep2" |
234 and q2: "Quotient R2 Abs2 Rep2" |
235 shows "(R1 ===> R2) f g \<Longrightarrow> R1 x y \<Longrightarrow> R2 (f x) (g y)" |
235 shows "(R1 ===> R2) f g \<Longrightarrow> R1 x y \<Longrightarrow> R2 (f x) (g y)" |
236 by simp |
236 by simp |
237 |
237 |
238 lemma FUN_REL_IMP: |
238 lemma fun_rel_IMP: |
239 shows "(R1 ===> R2) f g \<Longrightarrow> R1 x y \<Longrightarrow> R2 (f x) (g y)" |
239 shows "(R1 ===> R2) f g \<Longrightarrow> R1 x y \<Longrightarrow> R2 (f x) (g y)" |
240 by simp |
240 by simp |
241 |
241 |
242 lemma FUN_REL_EQUALS: |
242 lemma fun_rel_EQUALS: |
243 assumes q1: "Quotient R1 Abs1 Rep1" |
243 assumes q1: "Quotient R1 Abs1 Rep1" |
244 and q2: "Quotient R2 Abs2 Rep2" |
244 and q2: "Quotient R2 Abs2 Rep2" |
245 and r1: "Respects (R1 ===> R2) f" |
245 and r1: "Respects (R1 ===> R2) f" |
246 and r2: "Respects (R1 ===> R2) g" |
246 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))" |
247 shows "((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g) = (\<forall>x y. R1 x y \<longrightarrow> R2 (f x) (g y))" |
248 apply(rule_tac iffI) |
248 apply(rule_tac iffI) |
249 using FUN_Quotient[OF q1 q2] r1 r2 unfolding Quotient_def Respects_def |
249 using FUN_Quotient[OF q1 q2] r1 r2 unfolding Quotient_def Respects_def |
250 apply(metis FUN_REL_IMP) |
250 apply(metis fun_rel_IMP) |
251 using r1 unfolding Respects_def expand_fun_eq |
251 using r1 unfolding Respects_def expand_fun_eq |
252 apply(simp (no_asm_use)) |
252 apply(simp (no_asm_use)) |
253 apply(metis Quotient_REL[OF q2] Quotient_REL_REP[OF q1]) |
253 apply(metis Quotient_REL[OF q2] Quotient_REL_REP[OF q1]) |
254 done |
254 done |
255 |
255 |
256 (* ask Peter: FUN_REL_IMP used twice *) |
256 (* ask Peter: fun_rel_IMP used twice *) |
257 lemma FUN_REL_IMP2: |
257 lemma fun_rel_IMP2: |
258 assumes q1: "Quotient R1 Abs1 Rep1" |
258 assumes q1: "Quotient R1 Abs1 Rep1" |
259 and q2: "Quotient R2 Abs2 Rep2" |
259 and q2: "Quotient R2 Abs2 Rep2" |
260 and r1: "Respects (R1 ===> R2) f" |
260 and r1: "Respects (R1 ===> R2) f" |
261 and r2: "Respects (R1 ===> R2) g" |
261 and r2: "Respects (R1 ===> R2) g" |
262 and a: "(Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g" |
262 and a: "(Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g" |
263 shows "R1 x y \<Longrightarrow> R2 (f x) (g y)" |
263 shows "R1 x y \<Longrightarrow> R2 (f x) (g y)" |
264 using q1 q2 r1 r2 a |
264 using q1 q2 r1 r2 a |
265 by (simp add: FUN_REL_EQUALS) |
265 by (simp add: fun_rel_EQUALS) |
266 |
266 |
267 (* We don't use it, it is exactly the same as Quotient_REL_REP but wrong way *) |
267 (* We don't use it, it is exactly the same as Quotient_REL_REP but wrong way *) |
268 lemma EQUALS_PRS: |
268 lemma EQUALS_PRS: |
269 assumes q: "Quotient R Abs Rep" |
269 assumes q: "Quotient R Abs Rep" |
270 shows "(x = y) = R (Rep x) (Rep y)" |
270 shows "(x = y) = R (Rep x) (Rep y)" |
391 will be provable; which is why we need to use APPLY_RSP *) |
391 will be provable; which is why we need to use APPLY_RSP *) |
392 lemma apply_rsp: |
392 lemma apply_rsp: |
393 assumes q: "Quotient R1 Abs1 Rep1" |
393 assumes q: "Quotient R1 Abs1 Rep1" |
394 and a: "(R1 ===> R2) f g" "R1 x y" |
394 and a: "(R1 ===> R2) f g" "R1 x y" |
395 shows "R2 ((f::'a\<Rightarrow>'c) x) ((g::'a\<Rightarrow>'c) y)" |
395 shows "R2 ((f::'a\<Rightarrow>'c) x) ((g::'a\<Rightarrow>'c) y)" |
396 using a by (rule FUN_REL_IMP) |
396 using a by (rule fun_rel_IMP) |
397 |
397 |
398 lemma apply_rsp': |
398 lemma apply_rsp': |
399 assumes a: "(R1 ===> R2) f g" "R1 x y" |
399 assumes a: "(R1 ===> R2) f g" "R1 x y" |
400 shows "R2 (f x) (g y)" |
400 shows "R2 (f x) (g y)" |
401 using a by (rule FUN_REL_IMP) |
401 using a by (rule fun_rel_IMP) |
402 |
402 |
403 |
403 |
404 (* combinators: I, K, o, C, W *) |
404 (* combinators: I, K, o, C, W *) |
405 |
405 |
406 (* We use id_simps which includes id_apply; so these 2 theorems can be removed *) |
406 (* We use id_simps which includes id_apply; so these 2 theorems can be removed *) |