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 21 2024 at 12:33 UTC