Как мне отобразить, какие классы типов созданы для nat, int и т. Д.?

Я сделал grep для папки src / HOL с instance+[ ]nat и instantiation+[ ]nat, и, возможно, я нашел все классы типов, которые были созданы для nat.

Поскольку важно, чтобы я также смотрел, как были созданы экземпляры int, rat и real, было бы удобно, если бы для этого существовала команда, например print_dependencies, которая покажет зависимости для класса типа.

Ниже я показываю все команды печати и визуализации, которые я нашел, просто глядя на раскрывающийся список завершения команд, когда я набираю print_.

Я также показываю экземпляры для nat, которые я нашел в файлах корневой папки src / HOL, где главы соответствуют документу HOL.

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
*)

Визуализировать и распечатать команды:

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     *)

isabelle
person Community    schedule 16.02.2014    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Команда print_classes в Isabelle также перечисляет все определенные классы и типы, экземпляры которых были созданы в классе. Копирование вывода в файл и запуск его с помощью команды grep:

grep -F 'nat ::'

дает список классов, в которые были созданы экземпляры nat, который представляет собой довольно длинный список:

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

Как требуется.

person davidg    schedule 16.02.2014
comment
Спасибо. Определенно по запросу. Я пока не могу проголосовать, иначе проголосовал бы за. - person ; 17.02.2014
comment
Панель вывода Isabelle / jEdit пока не имеет собственного средства поиска, но jEdit имеет. Итак, если вы просто скопируете и вставите текст в обычный текстовый буфер и используете, например, Hypersearch по нему, вы получите больше удобства, чем grep из командной строки в старом стиле. - person Makarius; 02.03.2014