1148 in |
1148 in |
1149 (ths, snd (Local_Theory.note ((Binding.empty, [add_eqvt]), ths) ctxt)) |
1149 (ths, snd (Local_Theory.note ((Binding.empty, [add_eqvt]), ths) ctxt)) |
1150 end |
1150 end |
1151 *} |
1151 *} |
1152 |
1152 |
1153 end |
1153 ML {* |
|
1154 fun prove_by_alpha_induct alphas build_goal ind utac inputs ctxt = |
|
1155 let |
|
1156 val tys = map (domain_type o fastype_of) alphas; |
|
1157 val names = Datatype_Prop.make_tnames tys; |
|
1158 val (namesl, ctxt') = Variable.variant_fixes names ctxt; |
|
1159 val (namesr, ctxt'') = Variable.variant_fixes names ctxt'; |
|
1160 val freesl = map Free (namesl ~~ tys); |
|
1161 val freesr = map Free (namesr ~~ tys); |
|
1162 val (gls_lists, ctxt'') = fold_map (build_goal (tys ~~ (freesl ~~ freesr))) inputs ctxt''; |
|
1163 val gls = flat gls_lists; |
|
1164 fun trm_gls_map t = filter (exists_subterm (fn s => s = t)) gls; |
|
1165 val trm_gl_lists = map trm_gls_map freesl; |
|
1166 val trm_gls = map mk_conjl trm_gl_lists; |
|
1167 val pgls = map |
|
1168 (fn ((alpha, gl), (l, r)) => HOLogic.mk_imp (alpha $ l $ r, gl)) |
|
1169 ((alphas ~~ trm_gls) ~~ (freesl ~~ freesr)) |
|
1170 val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj pgls); |
|
1171 (* val _ = tracing (PolyML.makestring gl); *) |
|
1172 fun tac {context,...} = (ind_tac ind THEN_ALL_NEW split_conjs THEN_ALL_NEW utac) 1 |
|
1173 val th_loc = Goal.prove ctxt'' [] [] gl tac |
|
1174 val ths_loc = HOLogic.conj_elims th_loc |
|
1175 val ths = Variable.export ctxt'' ctxt ths_loc |
|
1176 in |
|
1177 filter (fn x => not (prop_of x = prop_of @{thm TrueI})) ths |
|
1178 end |
|
1179 *} |
|
1180 |
|
1181 ML {* |
|
1182 fun build_rsp_gl alphas fnctn ctxt = |
|
1183 let |
|
1184 val typ = domain_type (fastype_of fnctn); |
|
1185 val (argl, argr) = the (AList.lookup (op=) alphas typ); |
|
1186 in |
|
1187 ([HOLogic.mk_eq (fnctn $ argl, fnctn $ argr)], ctxt) |
|
1188 end |
|
1189 *} |
|
1190 |
|
1191 ML {* |
|
1192 fun fvbv_rsp_tac' simps ctxt = |
|
1193 asm_full_simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW |
|
1194 asm_full_simp_tac (HOL_ss addsimps (@{thm alpha_gen} :: simps)) THEN_ALL_NEW |
|
1195 REPEAT o eresolve_tac [conjE, exE] THEN_ALL_NEW |
|
1196 asm_full_simp_tac (HOL_ss addsimps simps) THEN_ALL_NEW |
|
1197 TRY o blast_tac (claset_of ctxt) |
|
1198 *} |
|
1199 |
|
1200 ML {* |
|
1201 fun build_fvbv_rsps alphas ind simps fnctns ctxt = |
|
1202 prove_by_alpha_induct alphas build_rsp_gl ind (fvbv_rsp_tac' simps ctxt) fnctns ctxt |
|
1203 *} |
|
1204 |
|
1205 end |