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 ML {* |
595 ML {* |
596 fun unlam_def t = |
596 fun unlam_def orig_ctxt ctxt t = |
597 let |
597 let |
598 val (v, rest) = Thm.dest_abs NONE (Thm.rhs_of t) |
598 val (v, rest) = Thm.dest_abs NONE (Thm.rhs_of t) |
599 val t2 = Drule.fun_cong_rule t v |
599 val (vname, vt) = Term.dest_Free (Thm.term_of v) |
|
600 val ([vnname], ctxt) = Variable.variant_fixes [vname] ctxt |
|
601 val nv = Free(vnname, vt) |
|
602 val t2 = Drule.fun_cong_rule t (Thm.cterm_of @{theory} nv) |
600 val tnorm = equal_elim (Drule.beta_eta_conversion (Thm.cprop_of t2)) t2 |
603 val tnorm = equal_elim (Drule.beta_eta_conversion (Thm.cprop_of t2)) t2 |
601 in unlam_def tnorm end |
604 in unlam_def orig_ctxt ctxt tnorm end |
602 handle CTERM _ => t |
605 handle CTERM _ => singleton (ProofContext.export ctxt orig_ctxt) t |
603 *} |
606 *} |
604 |
607 |
605 local_setup {* |
608 local_setup {* |
606 make_const_def "IN" @{term "membship"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
609 make_const_def "IN" @{term "membship"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
607 *} |
|
608 |
|
609 ML {* |
|
610 val IN_def = unlam_def @{thm IN_def} |
|
611 *} |
610 *} |
612 |
611 |
613 term membship |
612 term membship |
614 term IN |
613 term IN |
615 thm IN_def |
614 thm IN_def |
692 apply (rule QUOT_TYPE_fset_i.thm10) |
691 apply (rule QUOT_TYPE_fset_i.thm10) |
693 done |
692 done |
694 |
693 |
695 ML {* |
694 ML {* |
696 fun mk_rep_abs x = @{term REP_fset} $ (@{term ABS_fset} $ x) |
695 fun mk_rep_abs x = @{term REP_fset} $ (@{term ABS_fset} $ x) |
697 val consts = [@{const_name "Nil"}] |
696 val consts = [@{const_name "Nil"}, @{const_name "append"}, @{const_name "Cons"}] |
698 *} |
697 *} |
699 |
698 |
700 ML {* |
699 ML {* |
701 fun build_goal thm constructors mk_rep_abs = |
700 fun build_goal thm constructors mk_rep_abs = |
702 let |
701 let |
703 fun is_const (Const (x, t)) = x mem constructors |
702 fun is_const (Const (x, t)) = x mem constructors |
704 | is_const _ = false |
703 | is_const _ = false |
705 fun build_aux (Abs (s, t, tr)) = (Abs (s, t, build_aux tr)) |
704 fun build_aux (Abs (s, t, tr)) = (Abs (s, t, build_aux tr)) |
706 | build_aux (f $ a) = |
705 | build_aux (f $ a) = |
707 (if is_const f then mk_rep_abs (f $ (build_aux a)) |
706 let |
708 else ((build_aux f) $ (build_aux a))) |
707 val (f,args) = strip_comb (f $ a) |
|
708 in |
|
709 (if is_const f then mk_rep_abs (list_comb (f, (map mk_rep_abs (map build_aux args)))) |
|
710 else list_comb ((build_aux f), (map build_aux args))) |
|
711 end |
709 | build_aux x = |
712 | build_aux x = |
710 if is_const x then mk_rep_abs x else x |
713 if is_const x then mk_rep_abs x else x |
711 val concl = HOLogic.dest_Trueprop (Thm.concl_of thm) |
714 val concl = HOLogic.dest_Trueprop (Thm.concl_of thm) |
712 in |
715 in |
713 HOLogic.mk_eq ((build_aux concl), concl) |
716 HOLogic.mk_eq ((build_aux concl), concl) |
728 *} |
731 *} |
729 |
732 |
730 ML {* val emptyt = symmetric @{thm EMPTY_def} *} |
733 ML {* val emptyt = symmetric @{thm EMPTY_def} *} |
731 ML {* val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false [emptyt] cgoal) *} |
734 ML {* val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false [emptyt] cgoal) *} |
732 |
735 |
733 ML {* val in_t = (symmetric IN_def) *} |
736 ML {* val in_t = (symmetric (unlam_def @{context} @{context} @{thm IN_def})) *} |
734 ML {* val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite false [in_t] (cgoal2)) *} |
737 ML {* val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite false [in_t] (cgoal2)) *} |
735 |
738 |
736 (*theorem "(IN x EMPTY = False) = (x memb [] = False)"*) |
739 (*theorem "(IN x EMPTY = False) = (x memb [] = False)"*) |
737 |
740 |
738 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal3) *} |
741 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal3) *} |
740 unfolding IN_def EMPTY_def |
743 unfolding IN_def EMPTY_def |
741 apply (rule_tac mem_respects) |
744 apply (rule_tac mem_respects) |
742 apply (simp only: QUOT_TYPE_fset_i.REP_ABS_rsp) |
745 apply (simp only: QUOT_TYPE_fset_i.REP_ABS_rsp) |
743 apply (simp_all) |
746 apply (simp_all) |
744 apply (rule list_eq_sym) |
747 apply (rule list_eq_sym) |
|
748 done |
|
749 |
|
750 thm length_append (* Not true but worth checking that the goal is correct *) |
|
751 ML {* |
|
752 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm length_append})) |
|
753 val goal = build_goal m1_novars consts mk_rep_abs |
|
754 val cgoal = cterm_of @{theory} goal |
|
755 *} |
|
756 ML {* val uniont = symmetric (unlam_def @{context} @{context} @{thm UNION_def}) *} |
|
757 ML {* val cardt = symmetric (unlam_def @{context} @{context} @{thm CARD_def}) *} |
|
758 ML {* val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true [cardt] cgoal) *} |
|
759 ML {* val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true [uniont] cgoal2) *} |