Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] How to print the axioms of the current theory

Email Gateway (Jun 06 2022 at 14:25):

From: Miguel Pagano <miguel.pagano@unc.edu.ar>
Hi, is there some command to print only the axioms specified within an
axiomatization declaration?

I know of Theory.all_axioms_of but it lists also the axioms added by
definitions.

Having such a command (or better a document antiquotation) would permit to
show the axioms assumed by a theory.

Thanks in advance. Regards,
Miguel

Email Gateway (Jun 22 2022 at 22:28):

From: Miguel Pagano <miguel.pagano@unc.edu.ar>
I could get the axioms by filtering out the definitions:
ML\<open>
let
val axioms = Theory.all_axioms_of @{theory}
val defs = (map #2 o Defs.dest_constdefs []) (Theory.defs_of @{theory})
fun not_in_defs ax = List.exists (fn ax' => ax' = (#1 ax)) defs
val only_axioms = filter_out not_in_defs axioms
in
map (fn ax => (writeln o String.concat) [#1 ax,": ",Syntax.string_of_term
@{context} ( #2 ax)]) only_axioms
end
\<close>

Regards,
M.

Last updated: Apr 24 2024 at 08:20 UTC