1055 rtac @{thm ext}, |
1056 rtac @{thm ext}, |
1056 rtac trans_thm, |
1057 rtac trans_thm, |
1057 res_forall_rsp_tac ctxt, |
1058 res_forall_rsp_tac ctxt, |
1058 (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])), |
1059 (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])), |
1059 (instantiate_tac @{thm APPLY_RSP} ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])), |
1060 (instantiate_tac @{thm APPLY_RSP} ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])), |
1060 rtac reflex_thm, |
1061 rtac reflex_thm, |
1061 atac, |
1062 atac, |
1062 ((simp_tac ((Simplifier.context @{context} HOL_ss) addsimps @{thms FUN_REL.simps})) THEN_ALL_NEW (fn _ => no_tac)) |
1063 ( |
|
1064 (simp_tac ((Simplifier.context @{context} HOL_ss) addsimps @{thms FUN_REL.simps})) |
|
1065 THEN_ALL_NEW (fn _ => no_tac) |
|
1066 ) |
1063 ]) |
1067 ]) |
1064 *} |
1068 *} |
1065 |
1069 |
1066 ML {* |
1070 ML {* |
1067 fun r_mk_comb_tac_fset ctxt = |
1071 fun r_mk_comb_tac_fset ctxt = |
1137 done |
1141 done |
1138 |
1142 |
1139 ML {* val nthm = MetaSimplifier.rewrite_rule fset_defs_sym (snd (no_vars (Context.Theory @{theory}, @{thm list_induct_t}))) *} |
1143 ML {* val nthm = MetaSimplifier.rewrite_rule fset_defs_sym (snd (no_vars (Context.Theory @{theory}, @{thm list_induct_t}))) *} |
1140 |
1144 |
1141 thm list.recs(2) |
1145 thm list.recs(2) |
1142 |
1146 thm m2 |
1143 ML {* atomize_thm @{thm m2} *} |
1147 ML {* atomize_thm @{thm m2} *} |
1144 |
1148 |
1145 prove m2_r_p: {* |
1149 prove m2_r_p: {* |
1146 build_regularize_goal (atomize_thm @{thm m2}) @{typ "'a List.list"} @{term "op \<approx>"} @{context} *} |
1150 build_regularize_goal (atomize_thm @{thm m2}) @{typ "'a List.list"} @{term "op \<approx>"} @{context} *} |
1147 apply (simp add: equiv_res_forall[OF equiv_list_eq]) |
1151 apply (simp add: equiv_res_forall[OF equiv_list_eq]) |
1201 prove m2_t: m2_t |
1205 prove m2_t: m2_t |
1202 apply (simp only: m2_t_p[symmetric]) |
1206 apply (simp only: m2_t_p[symmetric]) |
1203 apply (tactic {* rtac m2_r 1 *}) |
1207 apply (tactic {* rtac m2_r 1 *}) |
1204 done |
1208 done |
1205 |
1209 |
|
1210 lemma id_apply2 [simp]: "id x \<equiv> x" |
|
1211 by (simp add: id_def) |
|
1212 |
|
1213 |
1206 thm LAMBDA_PRS |
1214 thm LAMBDA_PRS |
1207 ML {* |
1215 ML {* |
1208 val t = prop_of @{thm LAMBDA_PRS} |
1216 val t = prop_of @{thm LAMBDA_PRS} |
1209 val tt = Drule.instantiate' [SOME @{ctyp "'a list"}, SOME @{ctyp "'a fset"}] [] @{thm LAMBDA_PRS} |
1217 val tt = Drule.instantiate' [SOME @{ctyp "'a list"}, SOME @{ctyp "'a fset"}] [] @{thm LAMBDA_PRS} |
1210 val ttt = tt OF [@{thm QUOTIENT_fset}, @{thm IDENTITY_QUOTIENT}] |
1218 val ttt = @{thm LAMBDA_PRS} OF [@{thm QUOTIENT_fset}, @{thm IDENTITY_QUOTIENT}] |
1211 *} |
1219 val tttt = @{thm "HOL.sym"} OF [ttt] |
1212 ML {* val tttt = @{thm "HOL.sym"} OF [ttt] *} |
1220 *} |
1213 ML {* val zzzz = MetaSimplifier.rewrite_rule [tttt] @{thm m2_t} *} |
1221 ML {* |
1214 |
1222 val ttttt = MetaSimplifier.rewrite_rule [@{thm id_apply2}] tttt |
1215 |
1223 val zzz = @{thm m2_t} |
1216 thm m2_t |
1224 *} |
1217 ML {* @{thm m2_t} *} |
1225 |
|
1226 ML {* |
|
1227 fun eqsubst_thm ctxt thms thm = |
|
1228 let |
|
1229 val goalstate = Goal.init (Thm.cprop_of thm) |
|
1230 val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of |
|
1231 NONE => error "eqsubst_thm" |
|
1232 | SOME th => cprem_of th 1 |
|
1233 val tac = (EqSubst.eqsubst_tac ctxt [0] thms 1) THEN simp_tac HOL_ss 1 |
|
1234 val cgoal = cterm_of (ProofContext.theory_of ctxt) (Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a')) |
|
1235 val rt = Toplevel.program (fn () => Goal.prove_internal [] cgoal (fn _ => tac)); |
|
1236 in |
|
1237 Simplifier.rewrite_rule [rt] thm |
|
1238 end |
|
1239 *} |
|
1240 ML {* val m2_t' = eqsubst_thm @{context} [ttttt] @{thm m2_t} *} |
|
1241 ML {* val rwr = @{thm FORALL_PRS[OF QUOTIENT_fset]} *} |
|
1242 ML {* val rwrs = @{thm "HOL.sym"} OF [ObjectLogic.rulify rwr] *} |
|
1243 ML {* rwrs; m2_t' *} |
|
1244 ML {* eqsubst_thm @{context} [rwrs] m2_t' *} |
|
1245 thm INSERT_def |
|
1246 |
1218 |
1247 |
1219 ML {* val card1_suc_f = Thm.freezeT (atomize_thm @{thm card1_suc}) *} |
1248 ML {* val card1_suc_f = Thm.freezeT (atomize_thm @{thm card1_suc}) *} |
1220 |
1249 |
1221 prove card1_suc_r: {* |
1250 prove card1_suc_r: {* |
1222 Logic.mk_implies |
1251 Logic.mk_implies |