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.
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