equal
deleted
inserted
replaced
590 using a |
590 using a |
591 apply(induct) |
591 apply(induct) |
592 apply(auto) |
592 apply(auto) |
593 done |
593 done |
594 |
594 |
595 |
595 ML {* |
596 definition "IN x xa \<equiv> x memb REP_fset xa" |
596 fun unlam_def t = |
597 |
597 let |
598 (*local_setup {* |
598 val (v, rest) = Thm.dest_abs NONE (Thm.rhs_of t) |
|
599 val t2 = Drule.fun_cong_rule t v |
|
600 val tnorm = equal_elim (Drule.beta_eta_conversion (Thm.cprop_of t2)) t2 |
|
601 in unlam_def tnorm end |
|
602 handle CTERM _ => t |
|
603 *} |
|
604 |
|
605 local_setup {* |
599 make_const_def "IN" @{term "membship"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
606 make_const_def "IN" @{term "membship"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
600 *}*) |
607 *} |
|
608 |
|
609 ML {* |
|
610 val IN_def = unlam_def @{thm IN_def} |
|
611 *} |
601 |
612 |
602 term membship |
613 term membship |
603 term IN |
614 term IN |
604 thm IN_def |
615 thm IN_def |
605 |
616 |
717 *} |
728 *} |
718 |
729 |
719 ML {* val emptyt = symmetric @{thm EMPTY_def} *} |
730 ML {* val emptyt = symmetric @{thm EMPTY_def} *} |
720 ML {* val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false [emptyt] cgoal) *} |
731 ML {* val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false [emptyt] cgoal) *} |
721 |
732 |
722 ML {* val in_t = (symmetric @{thm IN_def}) *} |
733 ML {* val in_t = (symmetric IN_def) *} |
723 ML {* val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite false [in_t] (cgoal2)) *} |
734 ML {* val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite false [in_t] (cgoal2)) *} |
724 |
735 |
725 (*theorem "(IN x EMPTY = False) = (x memb [] = False)"*) |
736 (*theorem "(IN x EMPTY = False) = (x memb [] = False)"*) |
726 |
737 |
727 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal3) *} |
738 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal3) *} |
728 apply(rule_tac f="(op =)" in arg_cong2) |
739 apply(rule_tac f="(op =)" in arg_cong2) |
729 unfolding IN_def EMPTY_def |
740 unfolding IN_def EMPTY_def |
730 apply (rule_tac mem_respects) |
741 apply (rule_tac mem_respects) |
731 apply (simp only: QUOT_TYPE_fset_i.REP_ABS_rsp) |
742 apply (simp only: QUOT_TYPE_fset_i.REP_ABS_rsp) |
732 |
743 apply (simp_all) |
733 |
744 apply (rule list_eq_sym) |