2014-02-16 2 views
1

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

Поскольку это важно, что я смотрю на то, как 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  *) 

ответ

2

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 

Как обязательный.

+0

Спасибо. Определенно, как просили. Я еще не могу голосовать, или я проголосую. –

+0

Панель вывода Isabelle/jEdit еще не имеет собственного средства поиска, но jEdit делает. Поэтому, если вы просто скопируете текст в текстовый буфер и используете, например, гиперссылки на него, вы получаете больше удобства, чем командная строка grep старого стиля. – Makarius