39 definition |
39 definition |
40 "Quotient E Abs Rep \<equiv> (\<forall>a. Abs (Rep a) = a) \<and> |
40 "Quotient E Abs Rep \<equiv> (\<forall>a. Abs (Rep a) = a) \<and> |
41 (\<forall>a. E (Rep a) (Rep a)) \<and> |
41 (\<forall>a. E (Rep a) (Rep a)) \<and> |
42 (\<forall>r s. E r s = (E r r \<and> E s s \<and> (Abs r = Abs s)))" |
42 (\<forall>r s. E r s = (E r r \<and> E s s \<and> (Abs r = Abs s)))" |
43 |
43 |
44 lemma Quotient_ABS_REP: |
44 lemma Quotient_abs_rep: |
45 assumes a: "Quotient E Abs Rep" |
45 assumes a: "Quotient E Abs Rep" |
46 shows "Abs (Rep a) = a" |
46 shows "Abs (Rep a) = a" |
47 using a unfolding Quotient_def |
47 using a unfolding Quotient_def |
48 by simp |
48 by simp |
49 |
49 |
75 assumes a: "Quotient R Abs Rep" |
75 assumes a: "Quotient R Abs Rep" |
76 shows "R (Rep a) (Rep b) = (a = b)" |
76 shows "R (Rep a) (Rep b) = (a = b)" |
77 using a unfolding Quotient_def |
77 using a unfolding Quotient_def |
78 by metis |
78 by metis |
79 |
79 |
80 lemma Quotient_REP_ABS: |
80 lemma Quotient_rep_abs: |
81 assumes a: "Quotient R Abs Rep" |
81 assumes a: "Quotient R Abs Rep" |
82 shows "R r r \<Longrightarrow> R (Rep (Abs r)) r" |
82 shows "R r r \<Longrightarrow> R (Rep (Abs r)) r" |
83 using a unfolding Quotient_def |
83 using a unfolding Quotient_def |
84 by blast |
84 by blast |
85 |
85 |
281 lemma lambda_prs: |
281 lemma lambda_prs: |
282 assumes q1: "Quotient R1 Abs1 Rep1" |
282 assumes q1: "Quotient R1 Abs1 Rep1" |
283 and q2: "Quotient R2 Abs2 Rep2" |
283 and q2: "Quotient R2 Abs2 Rep2" |
284 shows "(Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) = (\<lambda>x. f x)" |
284 shows "(Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) = (\<lambda>x. f x)" |
285 unfolding expand_fun_eq |
285 unfolding expand_fun_eq |
286 using Quotient_ABS_REP[OF q1] Quotient_ABS_REP[OF q2] |
286 using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] |
287 by simp |
287 by simp |
288 |
288 |
289 lemma lambda_prs1: |
289 lemma lambda_prs1: |
290 assumes q1: "Quotient R1 Abs1 Rep1" |
290 assumes q1: "Quotient R1 Abs1 Rep1" |
291 and q2: "Quotient R2 Abs2 Rep2" |
291 and q2: "Quotient R2 Abs2 Rep2" |
292 shows "(Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x) = (\<lambda>x. f x)" |
292 shows "(Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x) = (\<lambda>x. f x)" |
293 unfolding expand_fun_eq |
293 unfolding expand_fun_eq |
294 using Quotient_ABS_REP[OF q1] Quotient_ABS_REP[OF q2] |
294 using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] |
295 by simp |
295 by simp |
296 |
296 |
297 (* Not used since applic_prs proves a version for an arbitrary number of arguments *) |
297 (* Not used since applic_prs proves a version for an arbitrary number of arguments *) |
298 lemma APP_PRS: |
298 lemma APP_PRS: |
299 assumes q1: "Quotient R1 abs1 rep1" |
299 assumes q1: "Quotient R1 abs1 rep1" |
300 and q2: "Quotient R2 abs2 rep2" |
300 and q2: "Quotient R2 abs2 rep2" |
301 shows "abs2 ((abs1 ---> rep2) f (rep1 x)) = f x" |
301 shows "abs2 ((abs1 ---> rep2) f (rep1 x)) = f x" |
302 unfolding expand_fun_eq |
302 unfolding expand_fun_eq |
303 using Quotient_ABS_REP[OF q1] Quotient_ABS_REP[OF q2] |
303 using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] |
304 by simp |
304 by simp |
305 |
305 |
306 (* Ask Peter: assumption q1 and q2 not used and lemma is the 'identity' *) |
306 (* Ask Peter: assumption q1 and q2 not used and lemma is the 'identity' *) |
307 lemma LAMBDA_RSP: |
307 lemma LAMBDA_RSP: |
308 assumes q1: "Quotient R1 Abs1 Rep1" |
308 assumes q1: "Quotient R1 Abs1 Rep1" |
326 |
326 |
327 lemma REP_ABS_RSP: |
327 lemma REP_ABS_RSP: |
328 assumes q: "Quotient R Abs Rep" |
328 assumes q: "Quotient R Abs Rep" |
329 and a: "R x1 x2" |
329 and a: "R x1 x2" |
330 shows "R x1 (Rep (Abs x2))" |
330 shows "R x1 (Rep (Abs x2))" |
331 using q a by (metis Quotient_rel[OF q] Quotient_ABS_REP[OF q] Quotient_REP_reflp[OF q]) |
331 using q a by (metis Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_REP_reflp[OF q]) |
332 |
332 |
333 (* Not used *) |
333 (* Not used *) |
334 lemma REP_ABS_RSP_LEFT: |
334 lemma REP_ABS_RSP_LEFT: |
335 assumes q: "Quotient R Abs Rep" |
335 assumes q: "Quotient R Abs Rep" |
336 and a: "R x1 x2" |
336 and a: "R x1 x2" |
337 shows "R x1 (Rep (Abs x2))" |
337 shows "R x1 (Rep (Abs x2))" |
338 using q a by (metis Quotient_rel[OF q] Quotient_ABS_REP[OF q] Quotient_REP_reflp[OF q]) |
338 using q a by (metis Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_REP_reflp[OF q]) |
339 |
339 |
340 (* ----------------------------------------------------- *) |
340 (* ----------------------------------------------------- *) |
341 (* Quantifiers: FORALL, EXISTS, EXISTS_UNIQUE, *) |
341 (* Quantifiers: FORALL, EXISTS, EXISTS_UNIQUE, *) |
342 (* Ball, Bex, RES_EXISTS_EQUIV *) |
342 (* Ball, Bex, RES_EXISTS_EQUIV *) |
343 (* ----------------------------------------------------- *) |
343 (* ----------------------------------------------------- *) |
345 (* bool theory: COND, LET *) |
345 (* bool theory: COND, LET *) |
346 |
346 |
347 lemma IF_PRS: |
347 lemma IF_PRS: |
348 assumes q: "Quotient R Abs Rep" |
348 assumes q: "Quotient R Abs Rep" |
349 shows "If a b c = Abs (If a (Rep b) (Rep c))" |
349 shows "If a b c = Abs (If a (Rep b) (Rep c))" |
350 using Quotient_ABS_REP[OF q] by auto |
350 using Quotient_abs_rep[OF q] by auto |
351 |
351 |
352 (* ask peter: no use of q *) |
352 (* ask peter: no use of q *) |
353 lemma IF_RSP: |
353 lemma IF_RSP: |
354 assumes q: "Quotient R Abs Rep" |
354 assumes q: "Quotient R Abs Rep" |
355 and a: "a1 = a2" "R b1 b2" "R c1 c2" |
355 and a: "a1 = a2" "R b1 b2" "R c1 c2" |
358 |
358 |
359 lemma LET_PRS: |
359 lemma LET_PRS: |
360 assumes q1: "Quotient R1 Abs1 Rep1" |
360 assumes q1: "Quotient R1 Abs1 Rep1" |
361 and q2: "Quotient R2 Abs2 Rep2" |
361 and q2: "Quotient R2 Abs2 Rep2" |
362 shows "Let x f = Abs2 (Let (Rep1 x) ((Abs1 ---> Rep2) f))" |
362 shows "Let x f = Abs2 (Let (Rep1 x) ((Abs1 ---> Rep2) f))" |
363 using Quotient_ABS_REP[OF q1] Quotient_ABS_REP[OF q2] by auto |
363 using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] by auto |
364 |
364 |
365 lemma LET_RSP: |
365 lemma LET_RSP: |
366 assumes q1: "Quotient R1 Abs1 Rep1" |
366 assumes q1: "Quotient R1 Abs1 Rep1" |
367 and q2: "Quotient R2 Abs2 Rep2" |
367 and q2: "Quotient R2 Abs2 Rep2" |
368 and a1: "(R1 ===> R2) f g" |
368 and a1: "(R1 ===> R2) f g" |
382 (* Not used *) |
382 (* Not used *) |
383 lemma APPLY_PRS: |
383 lemma APPLY_PRS: |
384 assumes q1: "Quotient R1 Abs1 Rep1" |
384 assumes q1: "Quotient R1 Abs1 Rep1" |
385 and q2: "Quotient R2 Abs2 Rep2" |
385 and q2: "Quotient R2 Abs2 Rep2" |
386 shows "f x = Abs2 (((Abs1 ---> Rep2) f) (Rep1 x))" |
386 shows "f x = Abs2 (((Abs1 ---> Rep2) f) (Rep1 x))" |
387 using Quotient_ABS_REP[OF q1] Quotient_ABS_REP[OF q2] by auto |
387 using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] by auto |
388 |
388 |
389 (* In the following theorem R1 can be instantiated with anything, |
389 (* In the following theorem R1 can be instantiated with anything, |
390 but we know some of the types of the Rep and Abs functions; |
390 but we know some of the types of the Rep and Abs functions; |
391 so by solving Quotient assumptions we can get a unique R2 that |
391 so by solving Quotient assumptions we can get a unique R2 that |
392 will be provable; which is why we need to use APPLY_RSP *) |
392 will be provable; which is why we need to use APPLY_RSP *) |
406 |
406 |
407 (* We use id_simps which includes id_apply; so these 2 theorems can be removed *) |
407 (* We use id_simps which includes id_apply; so these 2 theorems can be removed *) |
408 lemma I_PRS: |
408 lemma I_PRS: |
409 assumes q: "Quotient R Abs Rep" |
409 assumes q: "Quotient R Abs Rep" |
410 shows "id e = Abs (id (Rep e))" |
410 shows "id e = Abs (id (Rep e))" |
411 using Quotient_ABS_REP[OF q] by auto |
411 using Quotient_abs_rep[OF q] by auto |
412 |
412 |
413 lemma I_RSP: |
413 lemma I_RSP: |
414 assumes q: "Quotient R Abs Rep" |
414 assumes q: "Quotient R Abs Rep" |
415 and a: "R e1 e2" |
415 and a: "R e1 e2" |
416 shows "R (id e1) (id e2)" |
416 shows "R (id e1) (id e2)" |
419 lemma o_PRS: |
419 lemma o_PRS: |
420 assumes q1: "Quotient R1 Abs1 Rep1" |
420 assumes q1: "Quotient R1 Abs1 Rep1" |
421 and q2: "Quotient R2 Abs2 Rep2" |
421 and q2: "Quotient R2 Abs2 Rep2" |
422 and q3: "Quotient R3 Abs3 Rep3" |
422 and q3: "Quotient R3 Abs3 Rep3" |
423 shows "f o g = (Rep1 ---> Abs3) (((Abs2 ---> Rep3) f) o ((Abs1 ---> Rep2) g))" |
423 shows "f o g = (Rep1 ---> Abs3) (((Abs2 ---> Rep3) f) o ((Abs1 ---> Rep2) g))" |
424 using Quotient_ABS_REP[OF q1] Quotient_ABS_REP[OF q2] Quotient_ABS_REP[OF q3] |
424 using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] Quotient_abs_rep[OF q3] |
425 unfolding o_def expand_fun_eq |
425 unfolding o_def expand_fun_eq |
426 by simp |
426 by simp |
427 |
427 |
428 lemma o_RSP: |
428 lemma o_RSP: |
429 assumes q1: "Quotient R1 Abs1 Rep1" |
429 assumes q1: "Quotient R1 Abs1 Rep1" |