Parsing command tokens like "apply" in outer syntax · Isabelle/ML

I am interested in writing a command which will parse entire apply scripts. For instance, I want something like

have "True ∧ (a ∨ ¬a)"
  my_command
  apply (rule conjI[of True])
  apply auto[1]
  apply simp
  done

where my_command will be able to parse the entire apply script and e.g. do something with each tactic.

If each apply is changed to a string that is not a command, like apply', then I am able to use Parse.reserved "apply'" to parse this. However, this approach does not seem to be able to parse apply since it is already a command. I've tried other parser functions like Parse.command_name and Parse.keyword_with, but these do not seem to parse the apply commands either. Is what I am trying to do possible?

Jonathan Julian Huerta y Munive (Sep 23 2025 at 09:03):

Hi, I am afraid I do not understand your question. Do you want to parse apply commands? Have you tried Method.parse? You can see examples of parsers parsing methods and embedded keywords in ISABELLE_HOME/src/HOL/ex/Sketch_and_Explore and in ISABELLE_HOME/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML

Sage Binder (Sep 23 2025 at 23:07):

Thank you for pointing me toward the Sketch_and_Explore. I actually did not know about that, and it looks interesting.

Let me try and clarify what I want to do. I want a command which can examine an apply script and extract the list of tactics used. Currently. I can use Scan.repeat (Parse.reserved "apply2" |-- (Method.parse), which will parse a sequence of apply2 TACTIC commands into the list of applied tactics. E.g., with

have "True ∧ (a ∨ ¬a)"
  my_command
  apply2 (rule conjI[of True])
  apply2 auto[1]
  apply2 simp
  done

my_command will yield (with a little additional processing) something like ["rule conjI[of True]", "auto", "simp"]. However, to actually apply my_command to a proof script, I would have to change each apply to apply2. I'd like to make it so that I do not have to do this. E.g., given

have "True ∧ (a ∨ ¬a)"
  my_command
  apply (rule conjI[of True])
  apply auto[1]
  apply simp
  done

I would like my_command to still produce the same list ["rule conjI[of True]", "auto", "simp"]. However, simply changing Parse.reserved "apply2" to Parse.reserved "apply" does not work, I presume because apply is already a command/keyword. I also tried Parse.command, Parse.keyword_with, and Parse.embedded, but my_command just yields an empty list in all cases.

FYI, I have the keyword "my_command" :: prf_script % "proof" at the beginning of the .thy file. Maybe something different is needed for what I want to do?

irvin (Sep 24 2025 at 11:48):

Sage Binder (Sep 24 2025 at 14:28):

Strictly speaking, I need to temporarily "forget" that apply is a keyword, but maybe that is not possible either...

irvin (Sep 25 2025 at 06:08):

Yea that's want I meant by reusing a keyword. I know a project which patched isabelle for this functionality but I'm not sure how they did it

Jonathan Julian Huerta y Munive (Sep 25 2025 at 11:12):

I am not sure that what you want is stragihtforward with Isabelle/ML. The "official" solution would probably require a combination of Isabelle/Scala and Isabelle/ML. But If you are willing to change your approach a bit and do something (currently) brittle, I have written functionality (develop branch) to retrieve the "user actions" from a .thy file up to a line number. You would need to make this function dependent on the local \<^theory> and pass it as an argument.

Stream: Isabelle/ML

Topic: Parsing command tokens like "apply" in outer syntax