equal
deleted
inserted
replaced
742 val cxs = map (cterm_of thy o Free) xs |
742 val cxs = map (cterm_of thy o Free) xs |
743 val new_lhs = Drule.list_comb (lhs, cxs) |
743 val new_lhs = Drule.list_comb (lhs, cxs) |
744 |
744 |
745 fun get_conv [] = Conv.rewr_conv def |
745 fun get_conv [] = Conv.rewr_conv def |
746 | get_conv (x::xs) = Conv.fun_conv (get_conv xs) |
746 | get_conv (x::xs) = Conv.fun_conv (get_conv xs) |
747 |
|
748 in |
747 in |
749 get_conv xs new_lhs |> |
748 get_conv xs new_lhs |> |
750 singleton (ProofContext.export ctxt' ctxt) |
749 singleton (ProofContext.export ctxt' ctxt) |
751 end |
750 end |
752 *} |
751 *} |
757 |
756 |
758 term membship |
757 term membship |
759 term IN |
758 term IN |
760 thm IN_def |
759 thm IN_def |
761 |
760 |
762 ML {* |
761 (* unlam_def tests *) |
763 (Conv.fun_conv (Conv.fun_conv (Conv.rewr_conv @{thm IN_def}))) @{cterm "IN x y"} |
762 ML {* (Conv.fun_conv (Conv.fun_conv (Conv.rewr_conv @{thm IN_def}))) @{cterm "IN x y"} *} |
764 *} |
|
765 |
|
766 ML {* MetaSimplifier.rewrite_rule @{thms IN_def} @{thm IN_def}*} |
763 ML {* MetaSimplifier.rewrite_rule @{thms IN_def} @{thm IN_def}*} |
767 |
|
768 ML {* @{thm IN_def}; unlam_def @{context} @{thm IN_def} *} |
764 ML {* @{thm IN_def}; unlam_def @{context} @{thm IN_def} *} |
769 |
765 |
770 lemmas a = QUOT_TYPE.ABS_def[OF QUOT_TYPE_fset] |
766 lemmas a = QUOT_TYPE.ABS_def[OF QUOT_TYPE_fset] |
771 thm QUOT_TYPE.thm11[OF QUOT_TYPE_fset, THEN iffD1, simplified a] |
767 thm QUOT_TYPE.thm11[OF QUOT_TYPE_fset, THEN iffD1, simplified a] |
772 |
768 |
854 *} |
850 *} |
855 |
851 |
856 ML {* val qty = @{typ "'a fset"} *} |
852 ML {* val qty = @{typ "'a fset"} *} |
857 ML {* val tt = Type ("fun", [Type ("fun", [qty, @{typ "prop"}]), @{typ "prop"}]) *} |
853 ML {* val tt = Type ("fun", [Type ("fun", [qty, @{typ "prop"}]), @{typ "prop"}]) *} |
858 ML {* val fall = Const(@{const_name all}, dummyT) *} |
854 ML {* val fall = Const(@{const_name all}, dummyT) *} |
859 |
|
860 ML {* Syntax.check_term *} |
|
861 |
855 |
862 ML {* |
856 ML {* |
863 fun build_goal_term ctxt thm constructors rty qty mk_rep mk_abs = |
857 fun build_goal_term ctxt thm constructors rty qty mk_rep mk_abs = |
864 let |
858 let |
865 fun mk_rep_abs x = mk_rep (mk_abs x); |
859 fun mk_rep_abs x = mk_rep (mk_abs x); |
921 ML {* |
915 ML {* |
922 fun build_goal ctxt thm cons rty qty mk_rep mk_abs = |
916 fun build_goal ctxt thm cons rty qty mk_rep mk_abs = |
923 Logic.mk_equals ((build_goal_term ctxt thm cons rty qty mk_rep mk_abs), (Thm.prop_of thm)) |
917 Logic.mk_equals ((build_goal_term ctxt thm cons rty qty mk_rep mk_abs), (Thm.prop_of thm)) |
924 *} |
918 *} |
925 |
919 |
|
920 ML {* |
|
921 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m1})) |
|
922 *} |
|
923 |
|
924 ML {* |
|
925 m1_novars |> prop_of |
|
926 |> Syntax.string_of_term @{context} |
|
927 |> writeln; |
|
928 build_goal_term @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs |
|
929 |> Syntax.string_of_term @{context} |
|
930 |> writeln |
|
931 *} |
|
932 |
926 |
933 |
927 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *} |
934 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *} |
928 ML {* val fset_defs_sym = map (fn t => symmetric (unlam_def @{context} t)) fset_defs *} |
935 ML {* val fset_defs_sym = map (fn t => symmetric (unlam_def @{context} t)) fset_defs *} |
929 |
936 |
930 ML {* |
937 ML {* |