229 (fold (AList.delete (fn (((a : string), _), (b, _)) => a = b)) |
229 (fold (AList.delete (fn (((a : string), _), (b, _)) => a = b)) |
230 (map (fn n => (n, 0)) xns) tml); |
230 (map (fn n => (n, 0)) xns) tml); |
231 val substt = |
231 val substt = |
232 let |
232 let |
233 val ih = Drule.cterm_rule (Thm.instantiate (subst_ty, [])); |
233 val ih = Drule.cterm_rule (Thm.instantiate (subst_ty, [])); |
234 in map (pairself ih) (subst_ns @ subst_vs @ cts) end; |
234 in map (apply2 ih) (subst_ns @ subst_vs @ cts) end; |
235 val th = (Drule.instantiate_normalize (subst_ty, substt) eq) RS sym; |
235 val th = (Drule.instantiate_normalize (subst_ty, substt) eq) RS sym; |
236 in (hd (Variable.export ctxt'' ctxt [th]), bds) end) |
236 in (hd (Variable.export ctxt'' ctxt [th]), bds) end) |
237 handle Pattern.MATCH => tryeqs eqs (ct, ctxt) bds); |
237 handle Pattern.MATCH => tryeqs eqs (ct, ctxt) bds); |
238 |
238 |
239 (* looks for the atoms equation and instantiates it with the right number *) |
239 (* looks for the atoms equation and instantiates it with the right number *) |
277 |
277 |
278 fun conv ctxt eqs ct = |
278 fun conv ctxt eqs ct = |
279 let |
279 let |
280 val (congs, bds) = mk_congs ctxt eqs; |
280 val (congs, bds) = mk_congs ctxt eqs; |
281 val congs = rearrange congs; |
281 val congs = rearrange congs; |
282 val (th, bds') = apfst mk_eq (divide_and_conquer' (decomp_reify (mk_decompatom eqs) congs) (ct, ctxt) bds); |
282 val (th, bds') = |
|
283 apfst mk_eq (divide_and_conquer' (decomp_reify (mk_decompatom eqs) congs) (ct, ctxt) bds); |
283 fun is_list_var (Var (_, t)) = can dest_listT t |
284 fun is_list_var (Var (_, t)) = can dest_listT t |
284 | is_list_var _ = false; |
285 | is_list_var _ = false; |
285 val vars = th |> prop_of |> Logic.dest_equals |> snd |
286 val vars = th |> prop_of |> Logic.dest_equals |> snd |
286 |> strip_comb |> snd |> filter is_list_var; |
287 |> strip_comb |> snd |> filter is_list_var; |
287 val cert = cterm_of (Proof_Context.theory_of ctxt); |
288 val cert = cterm_of (Proof_Context.theory_of ctxt); |
288 val vs = map (fn v as Var (_, T) => |
289 val vs = map (fn v as Var (_, T) => |
289 (v, the (AList.lookup Type.could_unify bds' T) |> snd |> HOLogic.mk_list (dest_listT T))) vars; |
290 (v, the (AList.lookup Type.could_unify bds' T) |> snd |> HOLogic.mk_list (dest_listT T))) vars; |
290 val th' = Drule.instantiate_normalize ([], (map o pairself) cert vs) th; |
291 val th' = Drule.instantiate_normalize ([], (map o apply2) cert vs) th; |
291 val th'' = Thm.symmetric (dereify ctxt [] (Thm.lhs_of th')); |
292 val th'' = Thm.symmetric (dereify ctxt [] (Thm.lhs_of th')); |
292 in Thm.transitive th'' th' end; |
293 in Thm.transitive th'' th' end; |
293 |
294 |
294 fun tac ctxt eqs = |
295 fun tac ctxt eqs = |
295 lift_conv ctxt (conv ctxt eqs); |
296 lift_conv ctxt (conv ctxt eqs); |