I have defined an Eisbach method like the following

```
method inst_assn for y =
(rule ent_ex_postI[where x=y])
```

It is called via `apply(inst_assn "x")`

However, it would be nice if it could a variable amount of parameters and process them i.e.

`apply(inst_assn "x" "y")`

where the rule is simply applied for each argument given. Does anyone have an idea how to accomplish this? Or do I have to use a more complex language to express what I need?

I wrote a method called `inst_existentials`

in ML back in the day (grep the distribution to find it) that does something like that.

I know that method, it inspired me to write my own :sweat_smile: (link for your convenience https://isabelle.in.tum.de/library/HOL/HOL-Real_Asymp/Inst_Existentials.html).

However this one uses "Inst_Existentials.tac" but I want to apply a custom rule (based on a lemma) in the method. Where do I have to look (or for what) to find the corresponding tactics for applying a rule?

Okay so the Inst_Existentials method uses custom tactics written in ML. Is there any documentation on this? As I understand I should be able to re-use the code but need to reference a Theorem introduced in the AFP (my custom rule). "thm Session_name.lemma" seems not to work, any other suggestions?

Well that session needs to be imported at the point where you define the method in order for this to work.

And the instantiation of the rule might work a bit differently depending on the order of variables in the theorem statement.

Applying a rule in ML is typically done with the `resolve_tac`

tactic. That's probably the one I used as well.

If you have trouble figuring out the details feel free to send me some pointers to your precise situation tomorrow and I can see if I can sort it out.

Thanks! I found the issue: The lemma was defined in "Separation_Logic_Imperative_HOL.Assertions", which needed to be imported in the .thy file and then referred to in the ML file with "thm Assertions.ent_ex_postI"

Nice. Also note that my method applies a few more intro rules, such as `conjI`

and `allI`

. Might want to get rid of that for your case, depending on what you're trying to achieve.

Last updated: Sep 11 2024 at 16:22 UTC