Niels Mündler (Jun 27 2021 at 15:58): 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?
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.
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?
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?
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.
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.
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.
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.
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"
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: Dec 21 2024 at 12:33 UTC