Hello dear friends,
I'm looking for some method or tactic (instead of some Isar statements) that can instantiate schematic variables in a goal. Is anyone ever heard that?
I think the usual approach is to either instantiate them indirectly with e.g. resolution (
rule etc.) or to make sure that you don't even get schematic variables in the first place. I don't know of a tactic.
I did once make one for existentials. One could probably do something similar for schematic variables without too much effort…
Depends on whether you want to instantiate the schematic variables with particular terms or with some freshly created variables. I don’t know proof methods for these things, but there are attributes:
where for the former,
no_vars for the latter.
Yeah, i made the method version of the
where by myself, by copying and modifying the implementation in Eisbach. Actually I just modified the final declaration of the attributes and added the declaration of methods. The attributes originally apply on theorems and now as methods they apply on the state sequent of the proof. That is all, in only 10 lines of change. So I think, maybe it would be interesting to add the
where method in Eisbach, adding 10 lines and giving good features?
Not sure. I have to say that I never missed such methods. Maybe you’re using a heavily tactics-based style, while my style is focused on Isar. With Isar, you often have to write things more explicitly, but that’s a feature: it makes the proofs more intelligible for the human reader.
Last updated: Dec 07 2023 at 20:16 UTC