Email Gateway (Aug 17 2022 at 13:27): Email Gateway (Aug 17 2022 at 13:27):From: Sean McLaughlin <seanmcl@cmu.edu>
Hello,
I'd like a way to extract the theorem dependencies of a theorem.
I know Isabelle has a great facility for plotting these deps with
"thm_deps", but is there a way to just extract a tree of dependencies
(that could be topologically sorted, say).
Same question for entire theories: there is the command
ML {* print_theory (theory "Set") *}
which prints the theorems in alphabetical order. Is there a way
to print them, say, in the order of definition?
I looked in theory.ML, but the type theory doesn't have
any reference to type term.thm.
Thanks, for this an my previous questions!
Sean
Email Gateway (Aug 17 2022 at 13:27):From: John Matthews <matthews@galois.com>
I am also interested in this question. Similarly, how to I extract the
list of external oracles used in the proof of a tagged theorem, when
theorem dependencies are turned off?
Thanks,
-john
Email Gateway (Aug 17 2022 at 13:27):From: Makarius <makarius@sketis.net>
On Tue, 25 Oct 2005, John Matthews wrote:
Similarly, how to I extract the list of external oracles used in the
proof of a tagged theorem, when theorem dependencies are turned off?
See Pure/proofterm.ML for some operations on proof terms as stored within
the "der" field of a thm.
On Oct 24, 2005, at 5:52 PM, Sean McLaughlin wrote:
I'd like a way to extract the theorem dependencies of a theorem. I
know Isabelle has a great facility for plotting these deps with
"thm_deps", but is there a way to just extract a tree of dependencies
(that could be topologically sorted, say).
See Pure/Thy/thm_deps.ML. You may build a Graph.T (cf.
Pure/General/graph.ML) and get a toplogically sorted list of entries like
this:
fn G => Graph.all_succs G (Graph.minimals G)
Makarius
Email Gateway (Aug 17 2022 at 13:27):From: John Matthews <matthews@galois.com>
Thanks, Makarius. Here is the SML code I wrote to extract the list of
external oracle tags used in the proof of a theorem. Am I using any
deprecated functions?
text {* Extract the abstract syntax of a theorem's oracle tags. *}
ML {*
fun oracle_terms_of_thm thm
= Proofterm.oracles_of_proof [] (proof_of thm)
*}
text {* This will let us view the tagged oracles using surface syntax.
*}
ML {*
fun oracle_strings_of_thm thm
= let val thy = theory_of_thm thm
in map (fn (oracle,formula) => (oracle, Sign.string_of_term thy
formula))
(oracles_of_thm thm)
end
*}
-john
Email Gateway (Aug 17 2022 at 13:27):From: Makarius <makarius@sketis.net>
On Tue, 25 Oct 2005, John Matthews wrote:
Here is the SML code I wrote to extract the list of external oracle tags
used in the proof of a theorem. Am I using any deprecated functions?
This looks fine.
text {* This will let us view the tagged oracles using surface syntax.
*}
in map (fn (oracle,formula) => (oracle, Sign.string_of_term thy
Just a minor point concerning ``surface syntax'': using the theory context
of a theorem is a fair approximation if this is just for diagnostics.
For realistic output of formal entities one should usually use the static
proof context of the invoking command, with ProofContext.string_of_term
etc. There is also an abstract Pretty.pp concept for passing aroung
syntactic context for pretty printing output.
Makarius
Last updated: May 03 2024 at 12:27 UTC