equal
deleted
inserted
replaced
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 |
741 val thy = ProofContext.theory_of ctxt' |
741 val thy = ProofContext.theory_of ctxt' |
742 fun get_lhs xs = |
742 val cxs = map (cterm_of thy o Free) xs |
743 let |
743 val new_lhs = Drule.list_comb (lhs, cxs) |
744 val cxs = map (cterm_of thy o Free) xs |
|
745 in |
|
746 Drule.list_comb (lhs, cxs) |
|
747 end |
|
748 |
744 |
749 fun get_conv [] = Conv.rewr_conv def |
745 fun get_conv [] = Conv.rewr_conv def |
750 | get_conv (x::xs) = Conv.fun_conv (get_conv xs) |
746 | get_conv (x::xs) = Conv.fun_conv (get_conv xs) |
751 |
747 |
752 in |
748 in |
753 get_conv xs (get_lhs xs) |> |
749 get_conv xs new_lhs |> |
754 singleton (ProofContext.export ctxt' ctxt) |
750 singleton (ProofContext.export ctxt' ctxt) |
755 end |
751 end |
756 *} |
752 *} |
757 |
753 |
758 local_setup {* |
754 local_setup {* |
760 *} |
756 *} |
761 |
757 |
762 term membship |
758 term membship |
763 term IN |
759 term IN |
764 thm IN_def |
760 thm IN_def |
765 ML {* (Conv.fun_conv (Conv.fun_conv (Conv.rewr_conv @{thm IN_def}))) @{cterm "IN x y"}*} |
761 |
|
762 ML {* |
|
763 (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}*} |
766 ML {* MetaSimplifier.rewrite_rule @{thms IN_def} @{thm IN_def}*} |
767 |
767 |
768 ML {* unlam_def @{context} @{thm IN_def} *} |
768 ML {* @{thm IN_def}; unlam_def @{context} @{thm IN_def} *} |
769 |
769 |
770 lemmas a = QUOT_TYPE.ABS_def[OF QUOT_TYPE_fset] |
770 lemmas a = QUOT_TYPE.ABS_def[OF QUOT_TYPE_fset] |
771 thm QUOT_TYPE.thm11[OF QUOT_TYPE_fset, THEN iffD1, simplified a] |
771 thm QUOT_TYPE.thm11[OF QUOT_TYPE_fset, THEN iffD1, simplified a] |
772 |
772 |
773 lemma yy: |
773 lemma yy: |