744 ML {* val in_t = (symmetric (unlam_def @{context} @{context} @{thm IN_def})) *} |
744 ML {* val in_t = (symmetric (unlam_def @{context} @{context} @{thm IN_def})) *} |
745 ML {* val uniont = symmetric (unlam_def @{context} @{context} @{thm UNION_def}) *} |
745 ML {* val uniont = symmetric (unlam_def @{context} @{context} @{thm UNION_def}) *} |
746 ML {* val cardt = symmetric (unlam_def @{context} @{context} @{thm CARD_def}) *} |
746 ML {* val cardt = symmetric (unlam_def @{context} @{context} @{thm CARD_def}) *} |
747 ML {* val insertt = symmetric (unlam_def @{context} @{context} @{thm INSERT_def}) *} |
747 ML {* val insertt = symmetric (unlam_def @{context} @{context} @{thm INSERT_def}) *} |
748 |
748 |
749 thm m1 |
|
750 |
|
751 ML {* |
|
752 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m1})) |
|
753 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
|
754 val cgoal = cterm_of @{theory} goal |
|
755 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false [emptyt, in_t] cgoal) |
|
756 *} |
|
757 |
|
758 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *} |
|
759 apply(rule_tac f="(op =)" in arg_cong2) |
|
760 unfolding IN_def EMPTY_def |
|
761 apply (rule_tac mem_respects) |
|
762 apply (simp only: QUOT_TYPE_I_fset.REP_ABS_rsp) |
|
763 apply (simp_all) |
|
764 apply (rule list_eq_sym) |
|
765 done |
|
766 |
|
767 thm length_append (* Not true but worth checking that the goal is correct *) |
|
768 ML {* |
|
769 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm length_append})) |
|
770 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
|
771 val cgoal = cterm_of @{theory} goal |
|
772 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false [emptyt, in_t, cardt, uniont] cgoal) |
|
773 *} |
|
774 (*prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *} |
|
775 unfolding CARD_def UNION_def |
|
776 apply(rule_tac f="(op =)" in arg_cong2)*) |
|
777 |
|
778 thm m2 |
|
779 ML {* |
|
780 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m2})) |
|
781 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
|
782 val cgoal = cterm_of @{theory} goal |
|
783 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false [emptyt, in_t, cardt, uniont, insertt] cgoal) |
|
784 *} |
|
785 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *} |
|
786 apply(rule_tac f="(op =)" in arg_cong2) |
|
787 unfolding IN_def |
|
788 apply (rule_tac mem_respects) |
|
789 unfolding INSERT_def |
|
790 apply (simp only: QUOT_TYPE_I_fset.REP_ABS_rsp) |
|
791 apply (rule cons_preserves) |
|
792 apply (simp only: QUOT_TYPE_I_fset.REP_ABS_rsp) |
|
793 apply (rule list_eq_sym) |
|
794 apply (rule_tac f="(op \<or>)" in arg_cong2) |
|
795 apply (simp) |
|
796 apply (rule_tac mem_respects) |
|
797 apply (simp only: QUOT_TYPE_I_fset.REP_ABS_rsp) |
|
798 apply (rule list_eq_sym) |
|
799 done |
|
800 |
|
801 notation ( output) "prop" ("#_" [1000] 1000) |
749 notation ( output) "prop" ("#_" [1000] 1000) |
802 |
750 |
803 ML {* @{thm arg_cong2} *} |
751 ML {* @{thm arg_cong2} *} |
804 ML {* rtac *} |
752 ML {* rtac *} |
805 ML {* Term.dest_Const @{term "op ="} *} |
753 ML {* Term.dest_Const @{term "op ="} *} |
870 foo_tac, |
819 foo_tac, |
871 simp_tac (@{simpset} addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp}) |
820 simp_tac (@{simpset} addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp}) |
872 ] |
821 ] |
873 *} |
822 *} |
874 |
823 |
875 ML {* Thm.assume @{cprop "0 = 0"} *} |
824 thm m1 |
876 |
825 |
877 ML simp_tac |
826 ML {* |
878 |
827 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m1})) |
|
828 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
|
829 val cgoal = cterm_of @{theory} goal |
|
830 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false [emptyt, in_t] cgoal) |
|
831 *} |
|
832 |
|
833 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *} |
|
834 apply (tactic {* foo_tac' 1 *}) |
|
835 unfolding IN_def EMPTY_def |
|
836 apply (tactic {* foo_tac' 1 *}) |
|
837 apply (tactic {* foo_tac' 1 *}) |
|
838 apply (tactic {* foo_tac' 1 *}) |
|
839 apply (tactic {* foo_tac' 1 *}) |
|
840 done |
|
841 |
|
842 |
|
843 thm length_append (* Not true but worth checking that the goal is correct *) |
|
844 ML {* |
|
845 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm length_append})) |
|
846 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
|
847 val cgoal = cterm_of @{theory} goal |
|
848 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false [emptyt, in_t, cardt, uniont] cgoal) |
|
849 *} |
|
850 (* prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *} |
|
851 apply (tactic {* foo_tac' 1 *}) |
|
852 apply (tactic {* foo_tac' 2 *}) |
|
853 apply (tactic {* foo_tac' 2 *}) |
|
854 apply (tactic {* foo_tac' 2 *}) |
|
855 unfolding CARD_def UNION_def |
|
856 apply (tactic {* foo_tac' 1 *}) *) |
|
857 |
|
858 thm m2 |
|
859 ML {* |
|
860 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m2})) |
|
861 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
|
862 val cgoal = cterm_of @{theory} goal |
|
863 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false [emptyt, in_t, cardt, uniont, insertt] cgoal) |
|
864 *} |
879 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *} |
865 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *} |
880 apply (tactic {* foo_tac' 1 *}) |
866 apply (tactic {* foo_tac' 1 *}) |
881 unfolding IN_def INSERT_def |
867 unfolding IN_def INSERT_def |
882 apply (tactic {* foo_tac' 1 *}) |
868 apply (tactic {* foo_tac' 1 *}) |
883 apply (tactic {* foo_tac' 1 *}) |
869 apply (tactic {* foo_tac' 1 *}) |