591 apply(unfold REP_fset_def ABS_fset_def) |
599 apply(unfold REP_fset_def ABS_fset_def) |
592 apply(simp only: QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset]) |
600 apply(simp only: QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset]) |
593 apply(rule list_eq_sym) |
601 apply(rule list_eq_sym) |
594 done |
602 done |
595 |
603 |
596 lemma helper: |
604 lemma append_respects_fst: |
597 assumes a : "list_eq l1 l2" |
605 assumes a : "list_eq l1 l2" |
598 shows "list_eq (l1 @ s) (l2 @ s)" |
606 shows "list_eq (l1 @ s) (l2 @ s)" |
599 using a |
607 using a |
600 apply(induct) |
608 apply(induct) |
601 apply(auto intro: list_eq.intros) |
609 apply(auto intro: list_eq.intros) |
602 apply(simp add: list_eq_sym) |
610 apply(simp add: list_eq_sym) |
603 done |
611 done |
|
612 |
|
613 (* This code builds the interpretation from ML level, currently only |
|
614 for fset *) |
|
615 |
|
616 ML {* val mthd = Method.SIMPLE_METHOD (rtac @{thm QUOT_TYPE_fset} 1 THEN |
|
617 simp_tac (HOL_basic_ss addsimps @{thms REP_fset_def[symmetric]}) 1 THEN |
|
618 simp_tac (HOL_basic_ss addsimps @{thms ABS_fset_def[symmetric]}) 1) *} |
|
619 ML {* val mthdt = Method.Basic (fn _ => mthd) *} |
|
620 ML {* val bymt = Proof.global_terminal_proof (mthdt, NONE) *} |
|
621 ML {* val exp = [("QUOT_TYPE",(("QUOT_TYPE_fset_i", true), |
|
622 Expression.Named [ |
|
623 ("R","list_eq"), |
|
624 ("Abs","Abs_fset"), |
|
625 ("Rep","Rep_fset") |
|
626 ]))] *} |
|
627 ML {* val bindd = ((Binding.make ("",Position.none)),([]:Attrib.src list)) *} |
|
628 ML {* val eqn1 = (bindd, "QUOT_TYPE.ABS list_eq Abs_fset = ABS_fset") *} |
|
629 ML {* val eqn2 = (bindd, "QUOT_TYPE.REP Rep_fset = REP_fset") *} |
|
630 setup {* fn thy => ProofContext.theory_of |
|
631 (bymt (Expression.interpretation_cmd (exp, []) [eqn2,eqn1] thy)) *} |
|
632 |
|
633 (* It is eqivalent to the below: |
|
634 |
|
635 interpretation QUOT_TYPE_fset_i: QUOT_TYPE list_eq Abs_fset Rep_fset |
|
636 where "QUOT_TYPE.ABS list_eq Abs_fset = ABS_fset" |
|
637 and "QUOT_TYPE.REP Rep_fset = REP_fset" |
|
638 unfolding ABS_fset_def REP_fset_def |
|
639 apply (rule QUOT_TYPE_fset) |
|
640 apply (simp only: ABS_fset_def[symmetric]) |
|
641 apply (simp only: REP_fset_def[symmetric]) |
|
642 done |
|
643 *) |
604 |
644 |
605 lemma yyy : |
645 lemma yyy : |
606 shows " |
646 shows " |
607 ( |
647 ( |
608 (UNION EMPTY s = s) & |
648 (UNION EMPTY s = s) & |
612 ((ABS_fset ((e # (REP_fset s1)) @ REP_fset s2)) = ABS_fset (e # (REP_fset s1 @ REP_fset s2))) |
652 ((ABS_fset ((e # (REP_fset s1)) @ REP_fset s2)) = ABS_fset (e # (REP_fset s1 @ REP_fset s2))) |
613 )" |
653 )" |
614 unfolding UNION_def EMPTY_def INSERT_def |
654 unfolding UNION_def EMPTY_def INSERT_def |
615 apply(rule_tac f="(op &)" in arg_cong2) |
655 apply(rule_tac f="(op &)" in arg_cong2) |
616 apply(rule_tac f="(op =)" in arg_cong2) |
656 apply(rule_tac f="(op =)" in arg_cong2) |
617 apply(simp only: QUOT_TYPE.thm11[OF QUOT_TYPE_fset, |
657 apply(simp only: QUOT_TYPE_fset_i.thm11[symmetric]) |
618 simplified REP_fset_def[symmetric] ABS_fset_def[symmetric], symmetric]) |
658 apply(rule append_respects_fst) |
619 apply(rule helper) |
659 apply(simp only:QUOT_TYPE_fset_i.REP_ABS_rsp) |
620 apply(rule list_eq.intros(3)) |
|
621 apply(simp only:QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset, |
|
622 simplified REP_fset_def[symmetric] ABS_fset_def[symmetric]]) |
|
623 apply(rule list_eq_sym) |
660 apply(rule list_eq_sym) |
624 apply(simp) |
661 apply(simp) |
625 apply(rule_tac f="(op =)" in arg_cong2) |
662 apply(rule_tac f="(op =)" in arg_cong2) |
626 apply(simp only: QUOT_TYPE.thm11[OF QUOT_TYPE_fset, |
663 apply(simp only: QUOT_TYPE_fset_i.thm11[symmetric]) |
627 simplified REP_fset_def[symmetric] ABS_fset_def[symmetric], symmetric]) |
664 apply(rule append_respects_fst) |
628 apply(rule helper) |
665 apply(simp only: QUOT_TYPE_fset_i.REP_ABS_rsp) |
629 apply(rule list_eq.intros(3)) |
|
630 apply(simp only: QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset, |
|
631 simplified REP_fset_def[symmetric] ABS_fset_def[symmetric]]) |
|
632 apply(rule list_eq_sym) |
666 apply(rule list_eq_sym) |
633 apply(simp only: QUOT_TYPE.thm11[OF QUOT_TYPE_fset, |
667 apply(simp only: QUOT_TYPE_fset_i.thm11[symmetric]) |
634 simplified REP_fset_def[symmetric] ABS_fset_def[symmetric], symmetric]) |
|
635 apply(rule list_eq.intros(5)) |
668 apply(rule list_eq.intros(5)) |
636 apply(rule list_eq.intros(3)) |
669 apply(simp only: QUOT_TYPE_fset_i.REP_ABS_rsp) |
637 apply(simp only: QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset, |
|
638 simplified REP_fset_def[symmetric] ABS_fset_def[symmetric]]) |
|
639 apply(rule list_eq_sym) |
670 apply(rule list_eq_sym) |
640 done |
671 done |
641 |
672 |
642 lemma |
673 lemma |
643 shows " |
674 shows " |
644 ( |
|
645 (UNION EMPTY s = s) & |
675 (UNION EMPTY s = s) & |
646 ((UNION (INSERT e s1) s2) = (INSERT e (UNION s1 s2))) |
676 ((UNION (INSERT e s1) s2) = (INSERT e (UNION s1 s2)))" |
647 )" |
677 apply (simp add: yyy) |
648 apply(simp add:yyy) |
678 apply (rule QUOT_TYPE_fset_i.thm10) |
649 apply (unfold REP_fset_def ABS_fset_def) |
679 done |
650 apply (rule QUOT_TYPE.thm10[OF QUOT_TYPE_fset]) |
680 |
651 done |
|
652 |
|