equal
deleted
inserted
replaced
717 apply (metis QuotMain.m1 list_eq_refl) |
717 apply (metis QuotMain.m1 list_eq_refl) |
718 apply (metis QUOT_TYPE_I_fset.R_sym QUOT_TYPE_I_fset.thm11 list_eq_refl mem_cons) |
718 apply (metis QUOT_TYPE_I_fset.R_sym QUOT_TYPE_I_fset.thm11 list_eq_refl mem_cons) |
719 done |
719 done |
720 |
720 |
721 text {* |
721 text {* |
722 Unlam_def converts a definition given as |
722 Unabs_def converts a definition given as |
723 |
723 |
724 c \<equiv> %x. %y. f x y |
724 c \<equiv> %x. %y. f x y |
725 |
725 |
726 to a theorem of the form |
726 to a theorem of the form |
727 |
727 |
730 This function is needed to rewrite the right-hand |
730 This function is needed to rewrite the right-hand |
731 side to the left-hand side. |
731 side to the left-hand side. |
732 *} |
732 *} |
733 |
733 |
734 ML {* |
734 ML {* |
735 fun unlam_def ctxt def = |
735 fun unabs_def ctxt def = |
736 let |
736 let |
737 val (lhs, rhs) = Thm.dest_equals (cprop_of def) |
737 val (lhs, rhs) = Thm.dest_equals (cprop_of def) |
738 val xs = strip_abs_vars (term_of rhs) |
738 val xs = strip_abs_vars (term_of rhs) |
739 val (_, ctxt') = Variable.add_fixes (map fst xs) ctxt |
739 val (_, ctxt') = Variable.add_fixes (map fst xs) ctxt |
740 |
740 |
756 |
756 |
757 term membship |
757 term membship |
758 term IN |
758 term IN |
759 thm IN_def |
759 thm IN_def |
760 |
760 |
761 (* unlam_def tests *) |
761 (* unabs_def tests *) |
762 ML {* (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"} *} |
763 ML {* MetaSimplifier.rewrite_rule @{thms IN_def} @{thm IN_def}*} |
763 ML {* MetaSimplifier.rewrite_rule @{thms IN_def} @{thm IN_def}*} |
764 ML {* @{thm IN_def}; unlam_def @{context} @{thm IN_def} *} |
764 ML {* @{thm IN_def}; unabs_def @{context} @{thm IN_def} *} |
765 |
765 |
766 lemmas a = QUOT_TYPE.ABS_def[OF QUOT_TYPE_fset] |
766 lemmas a = QUOT_TYPE.ABS_def[OF QUOT_TYPE_fset] |
767 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] |
768 |
768 |
769 lemma yy: |
769 lemma yy: |
930 |> writeln |
930 |> writeln |
931 *} |
931 *} |
932 |
932 |
933 |
933 |
934 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} *} |
935 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 (unabs_def @{context} t)) fset_defs *} |
936 |
936 |
937 ML {* |
937 ML {* |
938 fun dest_cbinop t = |
938 fun dest_cbinop t = |
939 let |
939 let |
940 val (t2, rhs) = Thm.dest_comb t; |
940 val (t2, rhs) = Thm.dest_comb t; |