Hey, is there some way to apply a rule/fact such that terms not matching by unification will be spit out as a new subgoal? For example, consider this:

definition "myProp s ≡ s = {}" (* some proof *) lemma myProof: "myProp {}" unfolding myProp_def by safe (* some very similar proof that only needs to rewrite {} ∪ {} to {} *) (* this is the best I could come up with *) lemma myProof': "myProp ({} ∪ {})" proof - have 1: "{} ∪ {} = {}" by safe show ?thesis by (subst 1, fact myProof) qed (* The next thing is what I would like to have *) lemma myProof'': "myProp ({} ∪ {})" proof (fact myProof) show "{} ∪ {} = {}" by safe qed

I'm not aware of such a method, which I think generally runs into the usual problem of multiple possible unifiers.

But if you're happy with a basic heuristic, try this: Unify.thy

I hacked it together as an exercise and I'll probably need something like it soon myself, so I'd appreciate knowing if you find places where it breaks.

Cool thanks! I'll give it a go on the actual example leading to that question later

(deleted, accidental post)

if anyone is curious, Josh and I applied above linked tactic to the problem I was facing, but it needs more tuning

Last updated: Dec 07 2023 at 08:19 UTC