Jonathan Julian Huerta y Munive (Apr 13 2024 at 09:51): Jonathan Julian Huerta y Munive (Apr 13 2024 at 09:51):I have defined the following function to send the proof obligation to Output in its XML format:
(* thm -> thm Seq.seq *)
fun print_goal_as_xml_to_output thm =
let
val ctxt = \<^context>;
val goal = Thm.prop_of thm;
val xml_goal = YXML.parse (Syntax.string_of_term ctxt goal);
val str_from_pretty_goal = Pretty.string_of (XML.pretty 10 xml_goal);
val list_goal = map Pretty.str (space_explode "" str_from_pretty_goal);
val to_print = Pretty.blk (3, Pretty.breaks list_goal)
val _ = writeln (Pretty.string_of to_print);
in Seq.single thm end
I can see the corresponding proof obligation via
apply (tactic ‹print_goal_as_xml_to_output›)
However, I would like a more direct way without the thm parameter (without using apply(tactic ...)). That is, I want a function xml_goal: Proof.context -> string so that I can do ML_prf ‹ writeln (xml_goal \<^context>)›. My suspicion is that this would require creating the function directly in Goal.ML and probably would violate an Isabelle design principle. Is there such a function (or something similar e.g. goal: Proof.context -> thm)? Or is my suspicion correct?
Hanno Becker (May 02 2024 at 04:31):I don't think Proof.context contains the given proof goal, you'd need Proof.state for that. I'm unaware of this being exposed in ML_prf, though.
You can define a custom proof script command though (like apply) which would have access, if that helps.
Jonathan Julian Huerta y Munive (May 02 2024 at 08:17):Thanks for the suggestion @Hanno Becker , I will think about your comments and report back.
Jonathan Julian Huerta y Munive (May 02 2024 at 17:26):Exploring your suggestions, I discovered that a combination of ML_val with my function suffices for my current purposes. Thanks!
Yutaka Nagashima (May 02 2024 at 22:30):Hi @Jonathan Julian Huerta y Munive ,
I also think Proof.state is more relevant for your objective.
These functions might help you:
If you build a new custom proof script command similar to apply, you can achieve the objective you've described without violating Isabelle's design principles, I believe.
However, for that, you might need to use Toplevel.state, which can be confusing at first. I did something similar when developing try_hard, as seen here:
Jonathan Julian Huerta y Munive (May 03 2024 at 08:21):Hi @Yutaka Nagashima, you are right. Indeed, I wrote a similar function to that at L440 yesterday. Thanks for the pointers! They will be inspiring. BTW, I heard good news about you yesterday, congrats!
Last updated: May 04 2024 at 20:16 UTC