563 | "xs \<approx> ys \<Longrightarrow> ys \<approx> xs" |
563 | "xs \<approx> ys \<Longrightarrow> ys \<approx> xs" |
564 | "a#a#xs \<approx> a#xs" |
564 | "a#a#xs \<approx> a#xs" |
565 | "xs \<approx> ys \<Longrightarrow> a#xs \<approx> a#ys" |
565 | "xs \<approx> ys \<Longrightarrow> a#xs \<approx> a#ys" |
566 | "\<lbrakk>xs1 \<approx> xs2; xs2 \<approx> xs3\<rbrakk> \<Longrightarrow> xs1 \<approx> xs3" |
566 | "\<lbrakk>xs1 \<approx> xs2; xs2 \<approx> xs3\<rbrakk> \<Longrightarrow> xs1 \<approx> xs3" |
567 |
567 |
568 lemma list_eq_sym: |
568 lemma list_eq_refl: |
569 shows "xs \<approx> xs" |
569 shows "xs \<approx> xs" |
570 apply (induct xs) |
570 apply (induct xs) |
571 apply (auto intro: list_eq.intros) |
571 apply (auto intro: list_eq.intros) |
572 done |
572 done |
573 |
573 |
574 lemma equiv_list_eq: |
574 lemma equiv_list_eq: |
575 shows "EQUIV list_eq" |
575 shows "EQUIV list_eq" |
576 unfolding EQUIV_REFL_SYM_TRANS REFL_def SYM_def TRANS_def |
576 unfolding EQUIV_REFL_SYM_TRANS REFL_def SYM_def TRANS_def |
577 apply(auto intro: list_eq.intros list_eq_sym) |
577 apply(auto intro: list_eq.intros list_eq_refl) |
578 done |
578 done |
579 |
579 |
580 local_setup {* |
580 local_setup {* |
581 typedef_main (@{binding "fset"}, @{term "list_eq"}, @{typ "'a list"}, @{thm "equiv_list_eq"}) #> snd |
581 typedef_main (@{binding "fset"}, @{term "list_eq"}, @{typ "'a list"}, @{thm "equiv_list_eq"}) #> snd |
582 *} |
582 *} |
691 assumes c: "card1 xs = Suc n" |
691 assumes c: "card1 xs = Suc n" |
692 shows "\<exists>a ys. ~(a memb ys) \<and> xs \<approx> (a # ys)" |
692 shows "\<exists>a ys. ~(a memb ys) \<and> xs \<approx> (a # ys)" |
693 using c |
693 using c |
694 apply(induct xs) |
694 apply(induct xs) |
695 apply (metis Suc_neq_Zero card1_0) |
695 apply (metis Suc_neq_Zero card1_0) |
696 apply (metis QUOT_TYPE_I_fset.R_trans QuotMain.card1_cons list_eq_sym mem_cons) |
696 apply (metis QUOT_TYPE_I_fset.R_trans QuotMain.card1_cons list_eq_refl mem_cons) |
697 done |
697 done |
698 |
698 |
699 lemma cons_preserves: |
699 lemma cons_preserves: |
700 fixes z |
700 fixes z |
701 assumes a: "xs \<approx> ys" |
701 assumes a: "xs \<approx> ys" |
771 apply(rule_tac f="(op =) (x memb REP_fset xs)" in arg_cong) |
771 apply(rule_tac f="(op =) (x memb REP_fset xs)" in arg_cong) |
772 apply(rule mem_respects) |
772 apply(rule mem_respects) |
773 apply(rule list_eq.intros(3)) |
773 apply(rule list_eq.intros(3)) |
774 apply(unfold REP_fset_def ABS_fset_def) |
774 apply(unfold REP_fset_def ABS_fset_def) |
775 apply(simp only: QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset]) |
775 apply(simp only: QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset]) |
776 apply(rule list_eq_sym) |
776 apply(rule list_eq_refl) |
777 done |
777 done |
778 |
778 |
779 lemma append_respects_fst: |
779 lemma append_respects_fst: |
780 assumes a : "list_eq l1 l2" |
780 assumes a : "list_eq l1 l2" |
781 shows "list_eq (l1 @ s) (l2 @ s)" |
781 shows "list_eq (l1 @ s) (l2 @ s)" |
782 using a |
782 using a |
783 apply(induct) |
783 apply(induct) |
784 apply(auto intro: list_eq.intros) |
784 apply(auto intro: list_eq.intros) |
785 apply(simp add: list_eq_sym) |
785 apply(simp add: list_eq_refl) |
786 done |
786 done |
787 |
787 |
788 lemma yyy: |
788 lemma yyy: |
789 shows " |
789 shows " |
790 ( |
790 ( |
798 apply(rule_tac f="(op &)" in arg_cong2) |
798 apply(rule_tac f="(op &)" in arg_cong2) |
799 apply(rule_tac f="(op =)" in arg_cong2) |
799 apply(rule_tac f="(op =)" in arg_cong2) |
800 apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric]) |
800 apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric]) |
801 apply(rule append_respects_fst) |
801 apply(rule append_respects_fst) |
802 apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp) |
802 apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp) |
803 apply(rule list_eq_sym) |
803 apply(rule list_eq_refl) |
804 apply(simp) |
804 apply(simp) |
805 apply(rule_tac f="(op =)" in arg_cong2) |
805 apply(rule_tac f="(op =)" in arg_cong2) |
806 apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric]) |
806 apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric]) |
807 apply(rule append_respects_fst) |
807 apply(rule append_respects_fst) |
808 apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp) |
808 apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp) |
809 apply(rule list_eq_sym) |
809 apply(rule list_eq_refl) |
810 apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric]) |
810 apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric]) |
811 apply(rule list_eq.intros(5)) |
811 apply(rule list_eq.intros(5)) |
812 apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp) |
812 apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp) |
813 apply(rule list_eq_sym) |
813 apply(rule list_eq_refl) |
814 done |
814 done |
815 |
815 |
816 lemma |
816 lemma |
817 shows " |
817 shows " |
818 (UNION EMPTY s = s) & |
818 (UNION EMPTY s = s) & |
933 |
933 |
934 ML {* |
934 ML {* |
935 fun foo_tac' ctxt = |
935 fun foo_tac' ctxt = |
936 REPEAT_ALL_NEW (FIRST' [ |
936 REPEAT_ALL_NEW (FIRST' [ |
937 rtac @{thm trueprop_cong}, |
937 rtac @{thm trueprop_cong}, |
938 rtac @{thm list_eq_sym}, |
938 rtac @{thm list_eq_refl}, |
939 rtac @{thm cons_preserves}, |
939 rtac @{thm cons_preserves}, |
940 rtac @{thm mem_respects}, |
940 rtac @{thm mem_respects}, |
941 rtac @{thm QUOT_TYPE_I_fset.R_trans2}, |
941 rtac @{thm QUOT_TYPE_I_fset.R_trans2}, |
942 CHANGED o (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})), |
942 CHANGED o (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})), |
943 foo_tac, |
943 foo_tac, |