83 val proxy_table : (string * (string * (thm * (string * string)))) list |
83 val proxy_table : (string * (string * (thm * (string * string)))) list |
84 val proxify_const : string -> (string * string) option |
84 val proxify_const : string -> (string * string) option |
85 val invert_const : string -> string |
85 val invert_const : string -> string |
86 val unproxify_const : string -> string |
86 val unproxify_const : string -> string |
87 val new_skolem_var_name_from_const : string -> string |
87 val new_skolem_var_name_from_const : string -> string |
|
88 val atp_logical_consts : string list |
88 val atp_irrelevant_consts : string list |
89 val atp_irrelevant_consts : string list |
89 val atp_widely_irrelevant_consts : string list |
|
90 val atp_schematic_consts_of : term -> typ list Symtab.table |
90 val atp_schematic_consts_of : term -> typ list Symtab.table |
91 val is_type_enc_higher_order : type_enc -> bool |
91 val is_type_enc_higher_order : type_enc -> bool |
92 val is_type_enc_polymorphic : type_enc -> bool |
92 val is_type_enc_polymorphic : type_enc -> bool |
93 val level_of_type_enc : type_enc -> type_level |
93 val level_of_type_enc : type_enc -> type_level |
94 val is_type_enc_sound : type_enc -> bool |
94 val is_type_enc_sound : type_enc -> bool |
388 fun new_skolem_var_name_from_const s = |
388 fun new_skolem_var_name_from_const s = |
389 let val ss = s |> space_explode Long_Name.separator in |
389 let val ss = s |> space_explode Long_Name.separator in |
390 nth ss (length ss - 2) |
390 nth ss (length ss - 2) |
391 end |
391 end |
392 |
392 |
|
393 (* These are ignored anyway by the relevance filter (unless they appear in |
|
394 higher-order places) but not by the monomorphizer. *) |
|
395 val atp_logical_consts = |
|
396 [@{const_name all}, @{const_name "==>"}, @{const_name "=="}, |
|
397 @{const_name Trueprop}, @{const_name All}, @{const_name Ex}, |
|
398 @{const_name Ex1}, @{const_name Ball}, @{const_name Bex}] |
|
399 |
393 (* These are either simplified away by "Meson.presimplify" (most of the time) or |
400 (* These are either simplified away by "Meson.presimplify" (most of the time) or |
394 handled specially via "fFalse", "fTrue", ..., "fequal". *) |
401 handled specially via "fFalse", "fTrue", ..., "fequal". *) |
395 val atp_irrelevant_consts = |
402 val atp_irrelevant_consts = |
396 [@{const_name False}, @{const_name True}, @{const_name Not}, |
403 [@{const_name False}, @{const_name True}, @{const_name Not}, |
397 @{const_name conj}, @{const_name disj}, @{const_name implies}, |
404 @{const_name conj}, @{const_name disj}, @{const_name implies}, |
398 @{const_name HOL.eq}, @{const_name If}, @{const_name Let}] |
405 @{const_name HOL.eq}, @{const_name If}, @{const_name Let}] |
399 |
406 |
400 val atp_widely_irrelevant_consts = |
407 val atp_widely_irrelevant_consts = atp_logical_consts @ atp_irrelevant_consts |
401 atp_irrelevant_consts @ |
|
402 (* These are ignored anyway by the relevance filter (unless they appear in |
|
403 higher-order places) but not by the monomorphizer. *) |
|
404 [@{const_name all}, @{const_name "==>"}, @{const_name "=="}, |
|
405 @{const_name Trueprop}, @{const_name All}, @{const_name Ex}, |
|
406 @{const_name Ex1}, @{const_name Ball}, @{const_name Bex}] |
|
407 |
408 |
408 fun add_schematic_const (x as (_, T)) = |
409 fun add_schematic_const (x as (_, T)) = |
409 Monomorph.typ_has_tvars T ? Symtab.insert_list (op =) x |
410 Monomorph.typ_has_tvars T ? Symtab.insert_list (op =) x |
410 val add_schematic_consts_of = |
411 val add_schematic_consts_of = |
411 Term.fold_aterms (fn Const (x as (s, _)) => |
412 Term.fold_aterms (fn Const (x as (s, _)) => |