src/HOL/Tools/ATP/atp_translate.ML
changeset 44491 ba22ed224b20
parent 44463 c471a2b48fa1
child 44493 c2602c5d4b0a
     1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Thu Aug 25 14:06:34 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Thu Aug 25 14:25:06 2011 +0200
     1.3 @@ -141,6 +141,7 @@
     1.4  val tfree_prefix = "t_"
     1.5  val const_prefix = "c_"
     1.6  val type_const_prefix = "tc_"
     1.7 +val simple_type_prefix = "s_"
     1.8  val class_prefix = "cl_"
     1.9  
    1.10  val polymorphic_free_prefix = "poly_free"
    1.11 @@ -165,11 +166,10 @@
    1.12  val untyped_helper_suffix = "_U"
    1.13  val type_tag_idempotence_helper_name = helper_prefix ^ "ti_idem"
    1.14  
    1.15 -val predicator_name = "p"
    1.16 -val app_op_name = "a"
    1.17 -val type_guard_name = "g"
    1.18 -val type_tag_name = "t"
    1.19 -val simple_type_prefix = "ty_"
    1.20 +val predicator_name = "pp"
    1.21 +val app_op_name = "aa"
    1.22 +val type_guard_name = "gg"
    1.23 +val type_tag_name = "tt"
    1.24  
    1.25  val prefixed_predicator_name = const_prefix ^ predicator_name
    1.26  val prefixed_app_op_name = const_prefix ^ app_op_name
    1.27 @@ -1097,17 +1097,15 @@
    1.28    | should_encode_type ctxt {maybe_finite_Ts, surely_infinite_Ts,
    1.29                               maybe_nonmono_Ts, ...}
    1.30                         (Noninf_Nonmono_Types soundness) T =
    1.31 -    exists (type_instance ctxt T orf type_generalization ctxt T)
    1.32 -           maybe_nonmono_Ts andalso
    1.33 +    exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
    1.34      not (exists (type_instance ctxt T) surely_infinite_Ts orelse
    1.35           (not (member (type_aconv ctxt) maybe_finite_Ts T) andalso
    1.36            is_type_surely_infinite' ctxt soundness surely_infinite_Ts T))
    1.37    | should_encode_type ctxt {surely_finite_Ts, maybe_infinite_Ts,
    1.38                               maybe_nonmono_Ts, ...}
    1.39                         Fin_Nonmono_Types T =
    1.40 -    exists (type_instance ctxt T orf type_generalization ctxt T)
    1.41 -           maybe_nonmono_Ts andalso
    1.42 -    (exists (type_instance ctxt T) surely_finite_Ts orelse
    1.43 +    exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
    1.44 +    (exists (type_generalization ctxt T) surely_finite_Ts orelse
    1.45       (not (member (type_aconv ctxt) maybe_infinite_Ts T) andalso
    1.46        is_type_surely_finite ctxt T))
    1.47    | should_encode_type _ _ _ _ = false