From The Isabelle Cookbook, pages 11 and 12, I found some beginning information related to what I'm trying to do.
Representative of what I'm trying to do is this ML statement:
val syntax_str = Syntax.string_of_term @{context} (prop_of @{thm conjI});
I want to save the theorem conjI to a file as an ASCII string, and have it look like this:
P \<Longrightarrow> Q \<Longrightarrow> P \<and> Q
Below, I show some of the ML commands I experimented with from src/Pure/General/pretty.ML and src/Pure/Syntax/syntax.ML.
I can get a string, but it's not good for saving to a file. I don't know how to get the string as what's saved to a THY file.
ML‹Syntax.pretty_term›
ML‹Syntax.pretty_term @{context} (prop_of @{thm conjI})›
ML‹Pretty.writeln (Syntax.pretty_term @{context} (prop_of @{thm conjI}))›
ML‹Pretty.string_of (Syntax.pretty_term @{context} (prop_of @{thm conjI}))›
ML‹Pretty.symbolic_output (Syntax.pretty_term @{context} (prop_of @{thm conjI}))›
ML‹Pretty.symbolic_string_of (Syntax.pretty_term @{context} (prop_of @{thm conjI}))›
ML‹Pretty.str_of (Syntax.pretty_term @{context} (prop_of @{thm conjI}))›
ML‹
val syntax_str = Syntax.string_of_term @{context} (prop_of @{thm conjI});
writeln syntax_str;
File.write (Path.explode (
File.platform_path(Resources.master_directory @{theory}) ^
"/syntax_str.txt")) syntax_str;
›
ML‹
val pretty_str = Pretty.str_of (
Syntax.pretty_term @{context} (prop_of @{thm conjI}));
writeln pretty_str;
File.write (Path.explode (
File.platform_path(Resources.master_directory @{theory}) ^
"/pretty_str.txt")) pretty_str;
›
Thanks.
I am not sure if this is the best way, but you could try:
fun render_thm ctxt thm =
Print_Mode.setmp ["xsymbols"]
(fn _ => Display.pretty_thm ctxt thm
|> Pretty.str_of
|> YXML.parse_body
|> XML.content_of) ()
Now, if you run:
ML {* render_thm @{context} @{thm iffI} *}
you will get a string that displays in Isabelle/jEdit as:
⟦?P ⟹ ?Q; ?Q ⟹ ?P⟧ ⟹ ?P = ?Q
but internally is actually:
\<lbrakk>?P \<Longrightarrow> ?Q; ?Q \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P = ?Q
This latter version is what you will get if you save the string to a file using File.write.
Collected from the Internet
Please contact [email protected] to delete if infringement.
Comments