fixed bang encoding detection of which types to encode
authorblanchet
Thu Aug 25 14:25:06 2011 +0200 (2011-08-25)
changeset 44491ba22ed224b20
parent 44490 e3e8d20a6ebc
child 44492 a330c0608da8
fixed bang encoding detection of which types to encode
src/HOL/Tools/ATP/atp_translate.ML
src/HOL/Tools/ATP/atp_util.ML
     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
     2.1 --- a/src/HOL/Tools/ATP/atp_util.ML	Thu Aug 25 14:06:34 2011 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_util.ML	Thu Aug 25 14:25:06 2011 +0200
     2.3 @@ -17,6 +17,7 @@
     2.4    val string_from_time : Time.time -> string
     2.5    val type_instance : Proof.context -> typ -> typ -> bool
     2.6    val type_generalization : Proof.context -> typ -> typ -> bool
     2.7 +  val type_intersect : Proof.context -> typ -> typ -> bool
     2.8    val type_aconv : Proof.context -> typ * typ -> bool
     2.9    val varify_type : Proof.context -> typ -> typ
    2.10    val instantiate_type : theory -> typ -> typ -> typ -> typ
    2.11 @@ -117,6 +118,8 @@
    2.12  fun type_instance ctxt T T' =
    2.13    Sign.typ_instance (Proof_Context.theory_of ctxt) (T, T')
    2.14  fun type_generalization ctxt T T' = type_instance ctxt T' T
    2.15 +fun type_intersect ctxt T T' =
    2.16 +  type_instance ctxt T T' orelse type_generalization ctxt T T'
    2.17  fun type_aconv ctxt (T, T') =
    2.18    type_instance ctxt T T' andalso type_instance ctxt T' T
    2.19