542 \<and> (!u v w. ((f u (f v w) = f (f u v) w)))) |
542 \<and> (!u v w. ((f u (f v w) = f (f u v) w)))) |
543 then ( |
543 then ( |
544 if (a memb A) then (fold1 f g z A) else (f (g a) (fold1 f g z A)) |
544 if (a memb A) then (fold1 f g z A) else (f (g a) (fold1 f g z A)) |
545 ) else z)" |
545 ) else z)" |
546 |
546 |
|
547 (* fold1_def is not usable, but: *) |
547 thm fold1.simps |
548 thm fold1.simps |
548 |
549 |
549 lemma cons_preserves: |
550 lemma cons_preserves: |
550 fixes z |
551 fixes z |
551 assumes a: "xs \<approx> ys" |
552 assumes a: "xs \<approx> ys" |
558 apply (induct X) |
559 apply (induct X) |
559 apply (simp) |
560 apply (simp) |
560 apply (metis QUOT_TYPE_I_fset.thm11 list_eq_refl mem_cons QuotMain.m1) |
561 apply (metis QUOT_TYPE_I_fset.thm11 list_eq_refl mem_cons QuotMain.m1) |
561 done |
562 done |
562 |
563 |
563 |
|
564 text {* |
|
565 Unabs_def converts a definition given as |
|
566 |
|
567 c \<equiv> %x. %y. f x y |
|
568 |
|
569 to a theorem of the form |
|
570 |
|
571 c x y \<equiv> f x y |
|
572 |
|
573 This function is needed to rewrite the right-hand |
|
574 side to the left-hand side. |
|
575 *} |
|
576 |
|
577 ML {* |
|
578 fun unabs_def ctxt def = |
|
579 let |
|
580 val (lhs, rhs) = Thm.dest_equals (cprop_of def) |
|
581 val xs = strip_abs_vars (term_of rhs) |
|
582 val (_, ctxt') = Variable.add_fixes (map fst xs) ctxt |
|
583 |
|
584 val thy = ProofContext.theory_of ctxt' |
|
585 val cxs = map (cterm_of thy o Free) xs |
|
586 val new_lhs = Drule.list_comb (lhs, cxs) |
|
587 |
|
588 fun get_conv [] = Conv.rewr_conv def |
|
589 | get_conv (x::xs) = Conv.fun_conv (get_conv xs) |
|
590 in |
|
591 get_conv xs new_lhs |> |
|
592 singleton (ProofContext.export ctxt' ctxt) |
|
593 end |
|
594 *} |
|
595 |
|
596 local_setup {* |
564 local_setup {* |
597 make_const_def @{binding IN} @{term "membship"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
565 make_const_def @{binding IN} @{term "membship"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
598 *} |
566 *} |
599 |
567 |
600 term membship |
568 term membship |
601 term IN |
569 term IN |
602 thm IN_def |
570 thm IN_def |
603 |
|
604 (* unabs_def tests *) |
|
605 ML {* (Conv.fun_conv (Conv.fun_conv (Conv.rewr_conv @{thm IN_def}))) @{cterm "IN x y"} *} |
|
606 ML {* MetaSimplifier.rewrite_rule @{thms IN_def} @{thm IN_def}*} |
|
607 ML {* @{thm IN_def}; unabs_def @{context} @{thm IN_def} *} |
|
608 |
571 |
609 lemmas a = QUOT_TYPE.ABS_def[OF QUOT_TYPE_fset] |
572 lemmas a = QUOT_TYPE.ABS_def[OF QUOT_TYPE_fset] |
610 thm QUOT_TYPE.thm11[OF QUOT_TYPE_fset, THEN iffD1, simplified a] |
573 thm QUOT_TYPE.thm11[OF QUOT_TYPE_fset, THEN iffD1, simplified a] |
611 |
574 |
612 lemma yy: |
575 lemma yy: |
771 build_goal_term @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs |
734 build_goal_term @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs |
772 |> Syntax.string_of_term @{context} |
735 |> Syntax.string_of_term @{context} |
773 |> writeln |
736 |> writeln |
774 *} |
737 *} |
775 |
738 |
|
739 |
|
740 text {* |
|
741 Unabs_def converts a definition given as |
|
742 |
|
743 c \<equiv> %x. %y. f x y |
|
744 |
|
745 to a theorem of the form |
|
746 |
|
747 c x y \<equiv> f x y |
|
748 |
|
749 This function is needed to rewrite the right-hand |
|
750 side to the left-hand side. |
|
751 *} |
|
752 |
|
753 ML {* |
|
754 fun unabs_def ctxt def = |
|
755 let |
|
756 val (lhs, rhs) = Thm.dest_equals (cprop_of def) |
|
757 val xs = strip_abs_vars (term_of rhs) |
|
758 val (_, ctxt') = Variable.add_fixes (map fst xs) ctxt |
|
759 |
|
760 val thy = ProofContext.theory_of ctxt' |
|
761 val cxs = map (cterm_of thy o Free) xs |
|
762 val new_lhs = Drule.list_comb (lhs, cxs) |
|
763 |
|
764 fun get_conv [] = Conv.rewr_conv def |
|
765 | get_conv (x::xs) = Conv.fun_conv (get_conv xs) |
|
766 in |
|
767 get_conv xs new_lhs |> |
|
768 singleton (ProofContext.export ctxt' ctxt) |
|
769 end |
|
770 *} |
|
771 |
|
772 ML {* (* Test: *) @{thm IN_def}; unabs_def @{context} @{thm IN_def} *} |
776 |
773 |
777 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *} |
774 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *} |
778 ML {* val fset_defs_sym = map (fn t => symmetric (unabs_def @{context} t)) fset_defs *} |
775 ML {* val fset_defs_sym = map (fn t => symmetric (unabs_def @{context} t)) fset_defs *} |
779 |
776 |
780 ML {* |
777 ML {* |