58 theorem thm11: |
58 theorem thm11: |
59 shows "R r r' = (ABS r = ABS r')" |
59 shows "R r r' = (ABS r = ABS r')" |
60 unfolding ABS_def |
60 unfolding ABS_def |
61 by (simp only: equiv[simplified EQUIV_def] lem7) |
61 by (simp only: equiv[simplified EQUIV_def] lem7) |
62 |
62 |
|
63 |
63 lemma REP_ABS_rsp: |
64 lemma REP_ABS_rsp: |
64 shows "R f g \<Longrightarrow> R f (REP (ABS g))" |
65 shows "R f (REP (ABS g)) = R f g" |
|
66 and "R (REP (ABS g)) f = R g f" |
|
67 apply(subst thm11) |
|
68 apply(simp add: thm10 thm11) |
|
69 apply(subst thm11) |
|
70 apply(simp add: thm10 thm11) |
|
71 done |
|
72 |
|
73 lemma REP_ABS_rsp: |
|
74 shows "R g g \<Longrightarrow> (REP (ABS g) = g" |
65 apply(subst thm11) |
75 apply(subst thm11) |
66 apply(simp add: thm10 thm11) |
76 apply(simp add: thm10 thm11) |
67 done |
77 done |
68 |
78 |
69 lemma QUOTIENT: |
79 lemma QUOTIENT: |
555 lemma yy: |
565 lemma yy: |
556 shows "(False = x memb []) = (False = IN (x::nat) EMPTY)" |
566 shows "(False = x memb []) = (False = IN (x::nat) EMPTY)" |
557 unfolding IN_def EMPTY_def |
567 unfolding IN_def EMPTY_def |
558 apply(rule_tac f="(op =) False" in arg_cong) |
568 apply(rule_tac f="(op =) False" in arg_cong) |
559 apply(rule mem_respects) |
569 apply(rule mem_respects) |
560 apply(unfold REP_fset_def ABS_fset_def) |
570 apply(rule QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset, |
561 apply(rule QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset]) |
571 simplified REP_fset_def[symmetric] ABS_fset_def[symmetric]]) |
562 apply(rule list_eq.intros) |
572 apply(rule list_eq.intros) |
563 done |
573 done |
564 |
574 |
565 lemma |
575 lemma |
566 shows "IN (x::nat) EMPTY = False" |
576 shows "IN (x::nat) EMPTY = False" |
582 apply(rule QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset]) |
592 apply(rule QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset]) |
583 apply(rule list_eq_sym) |
593 apply(rule list_eq_sym) |
584 done |
594 done |
585 |
595 |
586 lemma helper: |
596 lemma helper: |
587 assumes a : "list_eq l1 r1" |
597 assumes a : "list_eq l1 l2" |
588 shows "list_eq (l1 @ l) (r1 @ l)" |
598 shows "list_eq (l1 @ s) (l2 @ s)" |
589 using a |
599 using a |
590 apply(induct) |
600 apply(induct) |
591 apply(simp add:list_eq.intros) |
601 apply(auto intro: list_eq.intros) |
592 apply(simp add:list_eq_sym) |
602 apply(simp add: list_eq_sym) |
593 apply(simp add:list_eq.intros(3)) |
603 done |
594 apply(simp add:list_eq.intros(4)) |
604 |
595 apply(simp add:list_eq.intros(5)) |
605 thm list_eq.intros |
596 apply(rule_tac list_eq.intros(6)) |
|
597 apply(assumption) |
|
598 apply(assumption) |
|
599 done |
|
600 |
606 |
601 lemma yyy : |
607 lemma yyy : |
602 shows " |
608 shows " |
603 ( |
609 ( |
604 (UNION EMPTY s = s) & |
610 (UNION EMPTY s = s) & |
608 ((ABS_fset ((e # (REP_fset s1)) @ REP_fset s2)) = ABS_fset (e # (REP_fset s1 @ REP_fset s2))) |
614 ((ABS_fset ((e # (REP_fset s1)) @ REP_fset s2)) = ABS_fset (e # (REP_fset s1 @ REP_fset s2))) |
609 )" |
615 )" |
610 unfolding UNION_def EMPTY_def INSERT_def |
616 unfolding UNION_def EMPTY_def INSERT_def |
611 apply(rule_tac f="(op &)" in arg_cong2) |
617 apply(rule_tac f="(op &)" in arg_cong2) |
612 apply(rule_tac f="(op =)" in arg_cong2) |
618 apply(rule_tac f="(op =)" in arg_cong2) |
613 apply (unfold REP_fset_def ABS_fset_def) |
619 apply(simp only: QUOT_TYPE.thm11[OF QUOT_TYPE_fset, |
614 apply(simp only: QUOT_TYPE.thm11[OF QUOT_TYPE_fset,symmetric]) |
620 simplified REP_fset_def[symmetric] ABS_fset_def[symmetric], symmetric]) |
615 apply(rule helper) |
621 apply(rule helper) |
616 apply(rule list_eq.intros(3)) |
622 apply(rule list_eq.intros(3)) |
617 apply(rule QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset]) |
623 apply(rule QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset, |
|
624 simplified REP_fset_def[symmetric] ABS_fset_def[symmetric]]) |
618 apply(rule list_eq_sym) |
625 apply(rule list_eq_sym) |
619 apply(simp) |
626 apply(simp) |
620 apply(rule_tac f="(op =)" in arg_cong2) |
627 apply(rule_tac f="(op =)" in arg_cong2) |
621 apply(simp only: QUOT_TYPE.thm11[OF QUOT_TYPE_fset,symmetric]) |
628 apply(simp only: QUOT_TYPE.thm11[OF QUOT_TYPE_fset, |
|
629 simplified REP_fset_def[symmetric] ABS_fset_def[symmetric], symmetric]) |
622 apply(rule helper) |
630 apply(rule helper) |
623 apply(rule list_eq.intros(3)) |
631 apply(rule list_eq.intros(3)) |
624 apply(rule QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset]) |
632 apply(rule QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset, |
|
633 simplified REP_fset_def[symmetric] ABS_fset_def[symmetric]]) |
625 apply(rule list_eq_sym) |
634 apply(rule list_eq_sym) |
626 apply(simp only: QUOT_TYPE.thm11[OF QUOT_TYPE_fset,symmetric]) |
635 apply(simp only: QUOT_TYPE.thm11[OF QUOT_TYPE_fset, |
627 apply(fold REP_fset_def ABS_fset_def) |
636 simplified REP_fset_def[symmetric] ABS_fset_def[symmetric], symmetric]) |
628 apply(rule list_eq.intros(5)) |
637 apply(rule list_eq.intros(5)) |
629 apply(rule list_eq.intros(3)) |
638 apply(rule list_eq.intros(3)) |
630 apply (unfold REP_fset_def ABS_fset_def) |
639 apply(rule QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset, |
631 apply(rule QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset]) |
640 simplified REP_fset_def[symmetric] ABS_fset_def[symmetric]]) |
632 apply(rule list_eq_sym) |
641 apply(rule list_eq_sym) |
633 done |
642 done |
634 |
643 |
635 lemma |
644 lemma |
636 shows " |
645 shows " |