Stream: General

Topic: Defining Eisbach methods with variable length arguments


view this post on Zulip Niels Mündler (Jun 27 2021 at 15:58):

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?

view this post on Zulip Manuel Eberl (Jun 27 2021 at 16:02):

I wrote a method called inst_existentials in ML back in the day (grep the distribution to find it) that does something like that.

view this post on Zulip Niels Mündler (Jun 27 2021 at 16:06):

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?

view this post on Zulip Niels Mündler (Jun 27 2021 at 16:25):

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?

view this post on Zulip Manuel Eberl (Jun 27 2021 at 16:46):

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

view this post on Zulip Manuel Eberl (Jun 27 2021 at 16:46):

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

view this post on Zulip Manuel Eberl (Jun 27 2021 at 16:47):

Applying a rule in ML is typically done with the resolve_tac tactic. That's probably the one I used as well.

view this post on Zulip Manuel Eberl (Jun 27 2021 at 16:48):

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.

view this post on Zulip Niels Mündler (Jun 27 2021 at 16:56):

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"

view this post on Zulip Manuel Eberl (Jun 27 2021 at 16:57):

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: Mar 28 2024 at 12:29 UTC