565 lemma yy: |
559 lemma yy: |
566 shows "(False = x memb []) = (False = IN (x::nat) EMPTY)" |
560 shows "(False = x memb []) = (False = IN (x::nat) EMPTY)" |
567 unfolding IN_def EMPTY_def |
561 unfolding IN_def EMPTY_def |
568 apply(rule_tac f="(op =) False" in arg_cong) |
562 apply(rule_tac f="(op =) False" in arg_cong) |
569 apply(rule mem_respects) |
563 apply(rule mem_respects) |
570 apply(rule QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset, |
564 apply(simp only: QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset, |
571 simplified REP_fset_def[symmetric] ABS_fset_def[symmetric]]) |
565 simplified REP_fset_def[symmetric] ABS_fset_def[symmetric]]) |
572 apply(rule list_eq.intros) |
566 apply(rule list_eq.intros) |
573 done |
567 done |
574 |
568 |
575 lemma |
569 lemma |
587 apply(rule_tac f="(op \<or>) (x=y)" in arg_cong) |
581 apply(rule_tac f="(op \<or>) (x=y)" in arg_cong) |
588 apply(rule_tac f="(op =) (x memb REP_fset xs)" in arg_cong) |
582 apply(rule_tac f="(op =) (x memb REP_fset xs)" in arg_cong) |
589 apply(rule mem_respects) |
583 apply(rule mem_respects) |
590 apply(rule list_eq.intros(3)) |
584 apply(rule list_eq.intros(3)) |
591 apply(unfold REP_fset_def ABS_fset_def) |
585 apply(unfold REP_fset_def ABS_fset_def) |
592 apply(rule QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset]) |
586 apply(simp only: QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset]) |
593 apply(rule list_eq_sym) |
587 apply(rule list_eq_sym) |
594 done |
588 done |
595 |
589 |
596 lemma helper: |
590 lemma helper: |
597 assumes a : "list_eq l1 l2" |
591 assumes a : "list_eq l1 l2" |
618 apply(rule_tac f="(op =)" in arg_cong2) |
610 apply(rule_tac f="(op =)" in arg_cong2) |
619 apply(simp only: QUOT_TYPE.thm11[OF QUOT_TYPE_fset, |
611 apply(simp only: QUOT_TYPE.thm11[OF QUOT_TYPE_fset, |
620 simplified REP_fset_def[symmetric] ABS_fset_def[symmetric], symmetric]) |
612 simplified REP_fset_def[symmetric] ABS_fset_def[symmetric], symmetric]) |
621 apply(rule helper) |
613 apply(rule helper) |
622 apply(rule list_eq.intros(3)) |
614 apply(rule list_eq.intros(3)) |
623 apply(rule QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset, |
615 apply(simp only:QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset, |
624 simplified REP_fset_def[symmetric] ABS_fset_def[symmetric]]) |
616 simplified REP_fset_def[symmetric] ABS_fset_def[symmetric]]) |
625 apply(rule list_eq_sym) |
617 apply(rule list_eq_sym) |
626 apply(simp) |
618 apply(simp) |
627 apply(rule_tac f="(op =)" in arg_cong2) |
619 apply(rule_tac f="(op =)" in arg_cong2) |
628 apply(simp only: QUOT_TYPE.thm11[OF QUOT_TYPE_fset, |
620 apply(simp only: QUOT_TYPE.thm11[OF QUOT_TYPE_fset, |
629 simplified REP_fset_def[symmetric] ABS_fset_def[symmetric], symmetric]) |
621 simplified REP_fset_def[symmetric] ABS_fset_def[symmetric], symmetric]) |
630 apply(rule helper) |
622 apply(rule helper) |
631 apply(rule list_eq.intros(3)) |
623 apply(rule list_eq.intros(3)) |
632 apply(rule QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset, |
624 apply(simp only: QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset, |
633 simplified REP_fset_def[symmetric] ABS_fset_def[symmetric]]) |
625 simplified REP_fset_def[symmetric] ABS_fset_def[symmetric]]) |
634 apply(rule list_eq_sym) |
626 apply(rule list_eq_sym) |
635 apply(simp only: QUOT_TYPE.thm11[OF QUOT_TYPE_fset, |
627 apply(simp only: QUOT_TYPE.thm11[OF QUOT_TYPE_fset, |
636 simplified REP_fset_def[symmetric] ABS_fset_def[symmetric], symmetric]) |
628 simplified REP_fset_def[symmetric] ABS_fset_def[symmetric], symmetric]) |
637 apply(rule list_eq.intros(5)) |
629 apply(rule list_eq.intros(5)) |
638 apply(rule list_eq.intros(3)) |
630 apply(rule list_eq.intros(3)) |
639 apply(rule QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset, |
631 apply(simp only: QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset, |
640 simplified REP_fset_def[symmetric] ABS_fset_def[symmetric]]) |
632 simplified REP_fset_def[symmetric] ABS_fset_def[symmetric]]) |
641 apply(rule list_eq_sym) |
633 apply(rule list_eq_sym) |
642 done |
634 done |
643 |
635 |
644 lemma |
636 lemma |