How do I display what type classes have been instantiated for nat, int, etc?

Question

I did a grep on on the src/HOL folder with instance+[ ]nat and instantiation+[ ]nat, and maybe I found all the type classes which have been instantiated for nat.

Since it's important that I also look at how int, rat, and real have instantiated, it would be convenient if there was a command for doing that, like print_dependencies, which will show the dependencies for a type class.

Below, I show all the print and visualization commands I found by just looking at the command completion drop-down box when I type print_.

I also show the instantiations for nat which I found in the files of the root folder src/HOL, where the chapters correspond with the HOL document.

subsection {* Nat class instantiations *}
(*
Ch.15 Nat
  zero
  comm_monoid_diff
  comm_semiring_1_cancel
  linorder
  order_bot
  no_top
  linordered_semidom
  no_zero_divisors
  wellorder proof
  ordered_cancel_comm_monoid_diff
  distrib_lattice
Ch.37 Int
Ch.39 Divides
  semiring_numeral_div
Ch.42 Semiring_Normalization
  comm_semiring_1_cancel_crossproduct
Ch.72 Fact
  fact
Ch.73 Parity
  even_odd
Ch.74 GCD
  gcd
  Gcd
*)

Visualize and print commands:

subsection{*Visualize and Print*}
class_deps           (*
locale_deps           *)
thm_deps              allI conjI
code_deps             If
(*--PRINTS-----*)
print_locale          ab_semigroup_add 
print_facts
print_statement       plus_nat_def times_nat_def
print_attributes
print_abbrevs
print_binds
print_context
print_state
print_coercions
print_commands
print_defn_rules
print_locales
print_methods        (*
print_rules           *)
print_antiquotations (*
print_ast_translation *)
print_bnfs
print_bundles
print_case_translations
print_cases          (*
print_claset          *)
print_classes
print_codeproc       (*
print_codesetup       *)
print_dependencies    ab_semigroup_add(*
print_induct_rules    *)
print_inductives
print_interps         ab_semigroup_add
print_options
print_orders
print_quot_maps
print_quotconsts
print_quotients
print_quotientsQ3
print_quotmapsQ3     (*
print_simpset         *)
print_syntax
print_theorems!      (*
print_theory!         *)
print_trans_rules    (*
print_translation     *)

Answer 1

The print_classes command in Isabelle also lists all defined classes, and which types have been instantiated into the class. Copying the output into a file, and running it through the grep command:

grep -F 'nat ::'

gives a listing of the classes that nat has been instantiated into, which is the rather long list:

nat :: ab_semigroup_add
nat :: ab_semigroup_mult
nat :: bot
nat :: cancel_ab_semigroup_add
nat :: cancel_comm_monoid_add
nat :: cancel_semigroup_add
nat :: card_UNIV
nat :: comm_monoid_add
nat :: comm_monoid_diff
nat :: comm_monoid_mult
nat :: comm_semiring
nat :: comm_semiring_0
nat :: comm_semiring_0_cancel
nat :: comm_semiring_1
nat :: comm_semiring_1_cancel
nat :: comm_semiring_1_cancel_crossproduct
nat :: distrib_lattice
nat :: div
nat :: dvd
nat :: enum_alt
nat :: enumeration_alt
nat :: equal
nat :: even_odd
nat :: exhaustive
nat :: finite_UNIV
nat :: full_exhaustive
nat :: inf
nat :: lattice
nat :: linorder
nat :: linordered_ab_semigroup_add
nat :: linordered_cancel_ab_semigroup_add
nat :: linordered_comm_semiring_strict
nat :: linordered_semidom
nat :: linordered_semiring
nat :: linordered_semiring_strict
nat :: minus
nat :: monoid_add
nat :: monoid_mult
nat :: mult_zero
nat :: narrowing
nat :: no_top
nat :: no_zero_divisors
nat :: numeral
nat :: one
nat :: ord
nat :: order
nat :: order_bot
nat :: ordered_ab_semigroup_add
nat :: ordered_ab_semigroup_add_imp_le
nat :: ordered_cancel_ab_semigroup_add
nat :: ordered_cancel_comm_monoid_diff
nat :: ordered_cancel_comm_semiring
nat :: ordered_cancel_semiring
nat :: ordered_comm_monoid_add
nat :: ordered_comm_semiring
nat :: ordered_semiring
nat :: partial_term_of
nat :: plus
nat :: power
nat :: preorder
nat :: random
nat :: semigroup_add
nat :: semigroup_mult
nat :: semilattice_inf
nat :: semilattice_sup
nat :: semiring
nat :: semiring_0
nat :: semiring_0_cancel
nat :: semiring_1
nat :: semiring_1_cancel
nat :: semiring_char_0
nat :: semiring_div
nat :: semiring_numeral
nat :: semiring_numeral_div
nat :: size
nat :: sup
nat :: term_of
nat :: times
nat :: type
nat :: typerep
nat :: wellorder
nat :: zero
nat :: zero_neq_one

As required.