equal
deleted
inserted
replaced
885 val concl2 = term_of (#prop (crep_thm thm)) |
885 val concl2 = term_of (#prop (crep_thm thm)) |
886 in |
886 in |
887 Logic.mk_equals ((build_aux concl2), concl2) |
887 Logic.mk_equals ((build_aux concl2), concl2) |
888 end *} |
888 end *} |
889 |
889 |
890 ML {* val emptyt = (symmetric (unlam_def @{context} @{thm EMPTY_def})) *} |
|
891 ML {* val in_t = (symmetric (unlam_def @{context} @{thm IN_def})) *} |
|
892 ML {* val uniont = symmetric (unlam_def @{context} @{thm UNION_def}) *} |
|
893 ML {* val cardt = symmetric (unlam_def @{context} @{thm card_def}) *} |
|
894 ML {* val insertt = symmetric (unlam_def @{context} @{thm INSERT_def}) *} |
|
895 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *} |
890 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *} |
896 ML {* val fset_defs_sym = [emptyt, in_t, uniont, cardt, insertt] *} |
891 ML {* val fset_defs_sym = map (fn t => symmetric (unlam_def @{context} t)) fset_defs *} |
897 |
892 |
898 ML {* |
893 ML {* |
899 fun dest_cbinop t = |
894 fun dest_cbinop t = |
900 let |
895 let |
901 val (t2, rhs) = Thm.dest_comb t; |
896 val (t2, rhs) = Thm.dest_comb t; |
960 REPEAT_ALL_NEW (FIRST' [ |
955 REPEAT_ALL_NEW (FIRST' [ |
961 rtac @{thm trueprop_cong}, |
956 rtac @{thm trueprop_cong}, |
962 rtac @{thm list_eq_sym}, |
957 rtac @{thm list_eq_sym}, |
963 rtac @{thm cons_preserves}, |
958 rtac @{thm cons_preserves}, |
964 rtac @{thm mem_respects}, |
959 rtac @{thm mem_respects}, |
|
960 rtac @{thm card1_rsp}, |
965 rtac @{thm QUOT_TYPE_I_fset.R_trans2}, |
961 rtac @{thm QUOT_TYPE_I_fset.R_trans2}, |
966 CHANGED o (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})), |
962 CHANGED o (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})), |
967 foo_tac, |
963 foo_tac, |
968 CHANGED o (ObjectLogic.full_atomize_tac) |
964 CHANGED o (ObjectLogic.full_atomize_tac) |
969 ]) |
965 ]) |
1060 Toplevel.program (fn () => |
1056 Toplevel.program (fn () => |
1061 cterm_of @{theory} goal |
1057 cterm_of @{theory} goal |
1062 ) |
1058 ) |
1063 *} |
1059 *} |
1064 ML {* |
1060 ML {* |
1065 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
1061 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal) |
1066 *} |
1062 *} |
1067 prove {* Thm.term_of cgoal2 *} |
1063 prove {* Thm.term_of cgoal2 *} |
1068 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1064 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1069 apply (tactic {* foo_tac' @{context} 1 *}) |
1065 apply (tactic {* foo_tac' @{context} 1 *}) |
1070 done |
1066 done |
1081 build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
1077 build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
1082 ) |
1078 ) |
1083 *} |
1079 *} |
1084 ML {* |
1080 ML {* |
1085 val cgoal = cterm_of @{theory} goal |
1081 val cgoal = cterm_of @{theory} goal |
1086 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
1082 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal) |
1087 *} |
1083 *} |
1088 ML fset_defs_sym |
1084 ML fset_defs_sym |
1089 prove {* (Thm.term_of cgoal2) *} |
1085 prove {* (Thm.term_of cgoal2) *} |
1090 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1086 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1091 apply (atomize(full)) |
1087 apply (tactic {* foo_tac' @{context} 1 *}) |
1092 apply (rule_tac trueprop_cong) |
|
1093 apply (atomize(full)) |
|
1094 apply (tactic {* foo_tac' @{context} 1 *}) |
|
1095 apply (rule_tac f = "P" in arg_cong) |
1088 apply (rule_tac f = "P" in arg_cong) |
1096 sorry |
1089 sorry |
1097 |
1090 |
1098 thm card1_suc |
1091 thm card1_suc |
1099 |
1092 |
1103 ML {* |
1096 ML {* |
1104 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
1097 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
1105 *} |
1098 *} |
1106 ML {* |
1099 ML {* |
1107 val cgoal = cterm_of @{theory} goal |
1100 val cgoal = cterm_of @{theory} goal |
1108 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
1101 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal) |
1109 *} |
1102 *} |
1110 prove {* (Thm.term_of cgoal2) *} |
1103 prove {* (Thm.term_of cgoal2) *} |
1111 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1104 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
|
1105 apply (tactic {* foo_tac' @{context} 1 *}) |
1112 |
1106 |
1113 |
1107 |
1114 |
1108 |
1115 (* |
1109 (* |
1116 datatype obj1 = |
1110 datatype obj1 = |