Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Instantiate schematic variable in apply-script

Email Gateway (Aug 18 2022 at 18:26):

From: Peter Lammich <lammich@in.tum.de>
Hi all,

I have a subgoal of the form
[| ... |] ==> a = ?f x

The proof is to instantiate ?f to function "foo", and then
invoke the simplifier. How to do this instantiation, i.e. is there a
method instantiate with that I can do:
apply (instantiate ?f = foo)

Best,
Peter

Email Gateway (Aug 18 2022 at 18:26):

From: Lars Noschinski <noschinl@in.tum.de>
My usual approach would be to avoid introducing ?f, i.e. sufficiently
instantiate the rule which introduced ?f (using the [of]-attribute).

Email Gateway (Aug 18 2022 at 18:27):

From: Peter Lammich <lammich@in.tum.de>
Unfortunately, this approach is no solution in my case, where ?f is
introduced by exhaustively applying a bunch of
elim - rules "apply (elim elim_rules)". The rules in "elim_rules" are a
verification condition generator, that I definitely do not
want to instantiate by hand before the actual verification conditions
are generated.

Best,
Peter

Email Gateway (Aug 18 2022 at 18:27):

From: Lawrence Paulson <lp15@cam.ac.uk>
You could always try something like this:

apply (rule asm_rl [of "a = foo x"])

Larry Paulson

Email Gateway (Aug 18 2022 at 18:28):

From: Lukas Bulwahn <bulwahn@in.tum.de>
On 09/27/2011 04:38 PM, Peter Lammich wrote:

On 09/27/2011 09:28 AM, Lars Noschinski wrote:

On 26.09.2011 19:02, Peter Lammich wrote:

Hi all,

I have a subgoal of the form
[| ... |] ==> a = ?f x

The proof is to instantiate ?f to function "foo", and then
invoke the simplifier. How to do this instantiation, i.e. is there a
method instantiate with that I can do:
apply (instantiate ?f = foo)
My usual approach would be to avoid introducing ?f, i.e. sufficiently
instantiate the rule which introduced ?f (using the [of]-attribute).
Unfortunately, this approach is no solution in my case, where ?f is
introduced by exhaustively applying a bunch of
elim - rules "apply (elim elim_rules)". The rules in "elim_rules" are a
verification condition generator, that I definitely do not
want to instantiate by hand before the actual verification conditions
are generated.

Then, I would suggest using rules trans and refl with the of attribute.
I guess in your case:

apply (rule trans)
prefer 2
apply (rule_tac t="foo x" in refl)

might work.

Lukas

Best,
Peter

Last updated: May 06 2024 at 16:21 UTC