1

Say I have a lemma mylem: foo ?a = bar ?a, and I need to apply it on a goal that has two occurrences of foo, e.g. baz (foo (f p q)) (foo (g r s)), but only at one of these positions. I know of two ways of doing that without having to write out all of p,q..., which can be complex expressions.

  • Using apply (subst mylem) followed by an appropriate number (here, zero or one) of back commands.
  • Using apply (subst mylem[where a = 'foo x y', standard]), where x and y are unbound names.

The use of subst here is just for demonstration; I really do want to modify the lemma, e.g. to use it with rule when there are multiple possible matches that I’d like to disambiguate this way.

Both approaches look like bad style to me. Is there a nicer way of achieving that?

John Wickerson
  • 1,204
  • 12
  • 23
Joachim Breitner
  • 25,395
  • 6
  • 78
  • 139

1 Answers1

1

You can tell subst which occurrence it should replace: subst (i) mylem unfolds mylem at the i-th matching occurrence. This saves you the back steps. You can also list multiple positions as in subst (1 2) mylem. If you want to unfold mylem in premises, use subst (asm) (1 2) mylem.

In general, I do not know a way to achieve what you want inside an apply script. On the theory level, you can use lemmas with the for clause to generalise over locally introduced variables:

lemmas mylem' = mylem[where a="f x y"] for x y

Inside a structured proof, you can do it explicitly like this:

{ fix x y note mylem[where a="f x y"] }
note mylem' = this
Andreas Lochbihler
  • 4,998
  • 12
  • 10
  • Ok, that works for subst. But what if the I want to apply the rule with, say, `rule` and there are multiple ways to unify it with the goal? – Joachim Breitner Apr 09 '13 at 12:13
  • I didn’t know about `for` this way before. Can I use it in more positions than with `lemmas` and `interpret(ation)`? – Joachim Breitner Apr 23 '13 at 11:52
  • 1
    You can use `for` with `theorems`, which is similar to `lemmas`; with `inductive` and `inductive_set` to fix parameters; and inside locale expressions as they occur in `interpret(ation)`, `sublocale`, and `locale ... = ... for ... +`. – Andreas Lochbihler Apr 23 '13 at 15:26