nat, int 등 어떤 유형 클래스가 인스턴스화되었는지 표시하려면 어떻게해야합니까?

Question

instance+[ ]nat 및 instantiation+[ ]nat과 함께 src/HOL 폴더에 grep을 작성했는데 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  *) 

Answer 1

이사벨의 print_classes 명령은 정의 된 모든 클래스를 나열하고 어떤 종류의 클래스로 인스턴스화되고있다. 파일로 출력을 복사하고 grep 명령을 통해 그것을 실행 :

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 

로 :

grep -F 'nat ::' 

은 다소 긴 목록입니다 nat가로 인스턴스화 된 클래스의 목록을 제공합니다 필수.