Coq has tactic language Ltac with match facilities and so on. Does Isabelle/HOL have some programming language for tactics with the services for parsing, pattern matching and so on? I skimmed through Isabelle's Isar reference manual and the old Pawlson tutorial but I have found cues for that.
0
votes
I am not serious Isabelle/HOL user, so take it with grain of salt. There is a tactic language called Eisbach. You can see more in the paper A Proof Method Language for Isabelle. ts.data61.csiro.au/publications/nicta_full_text/8465.pdf
– keep_learning
That comment should just be the answer.
– Joachim Breitner
@JoachimBreitner I thought it was not significant, that is why I added it as a comment.
– keep_learning
It is also possible to write tactics/methods directly in Isabelle/ML (arguably this methodology provides more flexibility than Eisbach, but, from my own experience, this flexibility is rarely needed in practice). For this, the primary reference is the "Implementation manual" of Isabelle and one of the secondary references could be the "Isabelle/ML cookbook". There was a post on this subject on SO a while ago, but keep in mind that it is quite old: stackoverflow.com/questions/15217009/….
– user9716869
1 Answers
3
votes
I am not serious Isabelle/HOL user, so take it with grain of salt. There is a tactic language called Eisbach. You can see more in the paper A Proof Method Language for Isabelle. ts.data61.csiro.au/publications/nicta_full_text/8465.pdf
