691 apply (rule QUOT_TYPE_fset_i.thm10) |
699 apply (rule QUOT_TYPE_fset_i.thm10) |
692 done |
700 done |
693 |
701 |
694 ML {* |
702 ML {* |
695 fun mk_rep_abs x = @{term REP_fset} $ (@{term ABS_fset} $ x) |
703 fun mk_rep_abs x = @{term REP_fset} $ (@{term ABS_fset} $ x) |
696 val consts = [@{const_name "Nil"}, @{const_name "append"}, @{const_name "Cons"}] |
704 val consts = [@{const_name "Nil"}, @{const_name "append"}, @{const_name "Cons"}, @{const_name "membship"}] |
697 *} |
705 *} |
698 |
706 |
699 ML {* |
707 ML {* |
700 fun build_goal thm constructors mk_rep_abs = |
708 fun build_goal thm constructors lifted_type mk_rep_abs = |
701 let |
709 let |
702 fun is_const (Const (x, t)) = x mem constructors |
710 fun is_const (Const (x, t)) = x mem constructors |
703 | is_const _ = false |
711 | is_const _ = false |
|
712 fun maybe_mk_rep_abs t = |
|
713 let |
|
714 val _ = writeln ("Maybe: " ^ Syntax.string_of_term @{context} t) |
|
715 in |
|
716 if type_of t = lifted_type then mk_rep_abs t else t |
|
717 end |
704 fun build_aux (Abs (s, t, tr)) = (Abs (s, t, build_aux tr)) |
718 fun build_aux (Abs (s, t, tr)) = (Abs (s, t, build_aux tr)) |
705 | build_aux (f $ a) = |
719 | build_aux (f $ a) = |
706 let |
720 let |
707 val (f,args) = strip_comb (f $ a) |
721 val (f,args) = strip_comb (f $ a) |
|
722 val _ = writeln (Syntax.string_of_term @{context} f) |
708 in |
723 in |
709 (if is_const f then mk_rep_abs (list_comb (f, (map mk_rep_abs (map build_aux args)))) |
724 (if is_const f then maybe_mk_rep_abs (list_comb (f, (map maybe_mk_rep_abs (map build_aux args)))) |
710 else list_comb ((build_aux f), (map build_aux args))) |
725 else list_comb ((build_aux f), (map build_aux args))) |
711 end |
726 end |
712 | build_aux x = |
727 | build_aux x = |
713 if is_const x then mk_rep_abs x else x |
728 if is_const x then maybe_mk_rep_abs x else x |
714 val concl = HOLogic.dest_Trueprop (Thm.concl_of thm) |
729 val concl = HOLogic.dest_Trueprop (Thm.concl_of thm) |
715 in |
730 in |
716 HOLogic.mk_eq ((build_aux concl), concl) |
731 HOLogic.mk_eq ((build_aux concl), concl) |
717 end *} |
732 end *} |
718 |
733 |
724 in th' end); |
739 in th' end); |
725 *} |
740 *} |
726 |
741 |
727 ML {* |
742 ML {* |
728 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m1})) |
743 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m1})) |
729 val goal = build_goal m1_novars consts mk_rep_abs |
744 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
730 val cgoal = cterm_of @{theory} goal |
745 val cgoal = cterm_of @{theory} goal |
731 *} |
746 *} |
732 |
747 |
733 ML {* val emptyt = symmetric @{thm EMPTY_def} *} |
748 ML {* val emptyt = symmetric @{thm EMPTY_def} *} |
734 ML {* val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false [emptyt] cgoal) *} |
749 ML {* val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false [emptyt] cgoal) *} |
748 done |
763 done |
749 |
764 |
750 thm length_append (* Not true but worth checking that the goal is correct *) |
765 thm length_append (* Not true but worth checking that the goal is correct *) |
751 ML {* |
766 ML {* |
752 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm length_append})) |
767 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm length_append})) |
753 val goal = build_goal m1_novars consts mk_rep_abs |
768 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
754 val cgoal = cterm_of @{theory} goal |
769 val cgoal = cterm_of @{theory} goal |
755 *} |
770 *} |
756 ML {* val uniont = symmetric (unlam_def @{context} @{context} @{thm UNION_def}) *} |
771 ML {* val uniont = symmetric (unlam_def @{context} @{context} @{thm UNION_def}) *} |
757 ML {* val cardt = symmetric (unlam_def @{context} @{context} @{thm CARD_def}) *} |
772 ML {* val cardt = symmetric (unlam_def @{context} @{context} @{thm CARD_def}) *} |
|
773 ML {* val insertt = symmetric (unlam_def @{context} @{context} @{thm INSERT_def}) *} |
758 ML {* val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true [cardt] cgoal) *} |
774 ML {* val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true [cardt] cgoal) *} |
759 ML {* val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true [uniont] cgoal2) *} |
775 ML {* val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true [uniont] cgoal2) *} |
|
776 |
|
777 thm m2 |
|
778 ML {* |
|
779 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m2})) |
|
780 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
|
781 val cgoal = cterm_of @{theory} goal |
|
782 *} |
|
783 ML {* val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true [in_t] cgoal) *} |
|
784 ML {* val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true [insertt] cgoal2) *} |
|
785 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal3) *} |
|
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_fset_i.REP_ABS_rsp) |
|
791 apply (rule cons_preserves) |
|
792 apply (simp only: QUOT_TYPE_fset_i.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_fset_i.REP_ABS_rsp) |
|
798 apply (rule list_eq_sym) |
|
799 done |