theory Unify imports Main begin lemma back_ssubst: "\P a; a' = a\ \ P a'" by (erule ssubst) method_setup unify = \ let fun dest_Trueprop (Const (\<^const_name>\Trueprop\, _) $ t) = t | dest_Trueprop t = t fun replace i xs y = take (i-1) xs @ cons y (drop i xs) fun splice xs ys = let fun splice' i = (take i xs @ drop i ys, i) in map splice' (1 upto length xs) end fun mk_pred context hd (args, i) = let val x = Free (#1 (Name.variant "x" context), dummyT) in lambda x (list_comb (hd, replace i args x)) end in Attrib.thm >> (fn th => fn ctxt => SIMPLE_METHOD' (SUBGOAL (fn (goal, i) => let val (hd, concl_args) = strip_comb (dest_Trueprop (Logic.strip_imp_concl goal)) val (_, rule_args) = strip_comb (dest_Trueprop (Thm.concl_of th)) val rule_args' = map (map_types (K dummyT)) rule_args val concl_args' = map (map_types (K dummyT)) concl_args val cpreds = splice rule_args' concl_args' |> map (mk_pred (Variable.names_of ctxt) hd) |> Type_Infer_Context.infer_types ctxt |> map (Thm.cterm_of ctxt) val resolutions = cpreds |> map (fn c => Drule.infer_instantiate' ctxt [SOME c] @{thm back_ssubst}) |> map (fn th => resolve_tac ctxt [th]) in ((foldl1 (op THEN') resolutions) THEN' resolve_tac ctxt [th]) i end))) end \ section \Examples\ definition "myProp s \ s = {}" lemma myProof: "myProp {}" unfolding myProp_def by safe lemma myProof': "myProp ({} \ {})" proof (unify myProof) show "{} \ {} = {}" by safe qed text \More general:\ axiomatization P where ax: "P {} {}" lemma "P ({} \ {}) ({} \ {} \ {})" apply (unify ax) apply safe oops axiomatization Q a b c x y z where axQ: "Q a b c" and axQ': "Q x y z" lemma "myProp p \ myProp q \ Q c b a \ Q d e f" apply (unify axQ) oops end