348 definition |
348 definition |
349 Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" |
349 Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" |
350 where |
350 where |
351 "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)" |
351 "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)" |
352 |
352 |
|
353 definition |
|
354 Bexeq :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" |
|
355 where |
|
356 "Bexeq R P \<equiv> (\<exists>x \<in> Respects R. P x) \<and> (\<forall>x \<in> Respects R. \<forall>y \<in> Respects R. ((P x \<and> P y) \<longrightarrow> (R x y)))" |
|
357 |
353 (* 3 lemmas needed for proving repabs_inj *) |
358 (* 3 lemmas needed for proving repabs_inj *) |
354 lemma ball_rsp: |
359 lemma ball_rsp: |
355 assumes a: "(R ===> (op =)) f g" |
360 assumes a: "(R ===> (op =)) f g" |
356 shows "Ball (Respects R) f = Ball (Respects R) g" |
361 shows "Ball (Respects R) f = Ball (Respects R) g" |
357 using a by (simp add: Ball_def in_respects) |
362 using a by (simp add: Ball_def in_respects) |
358 |
363 |
359 lemma bex_rsp: |
364 lemma bex_rsp: |
360 assumes a: "(R ===> (op =)) f g" |
365 assumes a: "(R ===> (op =)) f g" |
361 shows "(Bex (Respects R) f = Bex (Respects R) g)" |
366 shows "(Bex (Respects R) f = Bex (Respects R) g)" |
362 using a by (simp add: Bex_def in_respects) |
367 using a by (simp add: Bex_def in_respects) |
|
368 |
|
369 lemma bex1_rsp: |
|
370 assumes a: "(R ===> (op =)) f g" |
|
371 shows "(Bex1 (Respects R) f = Bex1 (Respects R) g)" |
|
372 using a |
|
373 by (simp add: Ex1_def Bex1_def in_respects) auto |
363 |
374 |
364 lemma babs_rsp: |
375 lemma babs_rsp: |
365 assumes q: "Quotient R1 Abs1 Rep1" |
376 assumes q: "Quotient R1 Abs1 Rep1" |
366 and a: "(R1 ===> R2) f g" |
377 and a: "(R1 ===> R2) f g" |
367 shows "(R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)" |
378 shows "(R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)" |
413 assumes a: "Quotient R absf repf" |
424 assumes a: "Quotient R absf repf" |
414 shows "Bex (Respects R) ((absf ---> id) f) = Ex f" |
425 shows "Bex (Respects R) ((absf ---> id) f) = Ex f" |
415 using a unfolding Quotient_def |
426 using a unfolding Quotient_def |
416 by (metis COMBC_def Collect_def Collect_mem_eq in_respects fun_map.simps id_apply) |
427 by (metis COMBC_def Collect_def Collect_mem_eq in_respects fun_map.simps id_apply) |
417 |
428 |
|
429 lemma ex1_prs: |
|
430 assumes a: "Quotient R absf repf" |
|
431 shows "Bexeq R ((absf ---> id) f) = Ex1 f" |
|
432 apply (subst Bexeq_def) |
|
433 apply (subst Bex_def) |
|
434 apply (subst Ex1_def) |
|
435 apply simp |
|
436 apply rule |
|
437 apply (erule conjE)+ |
|
438 apply (erule_tac exE) |
|
439 apply (erule conjE) |
|
440 apply (subgoal_tac "\<forall>y. R y y \<longrightarrow> f (absf y) \<longrightarrow> R x y") |
|
441 apply (rule_tac x="absf x" in exI) |
|
442 apply (thin_tac "\<forall>x\<in>Respects R. \<forall>y\<in>Respects R. f (absf x) \<and> f (absf y) \<longrightarrow> R x y") |
|
443 apply (simp) |
|
444 apply rule+ |
|
445 using a unfolding Quotient_def |
|
446 apply metis |
|
447 apply rule+ |
|
448 apply (erule_tac x="x" in ballE) |
|
449 apply (erule_tac x="y" in ballE) |
|
450 apply simp |
|
451 apply (simp add: in_respects) |
|
452 apply (simp add: in_respects) |
|
453 apply (erule_tac exE) |
|
454 apply rule |
|
455 apply (rule_tac x="repf x" in exI) |
|
456 apply (simp only: in_respects) |
|
457 apply rule |
|
458 apply (metis Quotient_rel_rep[OF a]) |
|
459 using a unfolding Quotient_def apply (simp) |
|
460 apply rule+ |
|
461 using a unfolding Quotient_def in_respects |
|
462 apply metis |
|
463 done |
|
464 |
418 lemma fun_rel_id: |
465 lemma fun_rel_id: |
419 assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)" |
466 assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)" |
420 shows "(R1 ===> R2) f g" |
467 shows "(R1 ===> R2) f g" |
421 using a by simp |
468 using a by simp |
422 |
469 |