## Stream: General

### Topic: applying rules/facts up to unification

#### Kevin Kappelmann (Mar 18 2020 at 12:52):

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
```

#### Josh Chen (Mar 20 2020 at 01:45):

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.

#### Kevin Kappelmann (Mar 20 2020 at 09:32):

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

#### Josh Chen (Mar 23 2020 at 12:54):

(deleted, accidental post)

#### Kevin Kappelmann (Mar 23 2020 at 13:52):

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