# HG changeset patch
# User blanchet
# Date 1314275106 -7200
# Node ID ba22ed224b20b6376eb56f6aeff02559bdbf9b05
# Parent  e3e8d20a6ebcc883e7c478a163babf5c20bc6ede
fixed bang encoding detection of which types to encode

diff -r e3e8d20a6ebc -r ba22ed224b20 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Thu Aug 25 14:06:34 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Thu Aug 25 14:25:06 2011 +0200
@@ -141,6 +141,7 @@
 val tfree_prefix = "t_"
 val const_prefix = "c_"
 val type_const_prefix = "tc_"
+val simple_type_prefix = "s_"
 val class_prefix = "cl_"
 
 val polymorphic_free_prefix = "poly_free"
@@ -165,11 +166,10 @@
 val untyped_helper_suffix = "_U"
 val type_tag_idempotence_helper_name = helper_prefix ^ "ti_idem"
 
-val predicator_name = "p"
-val app_op_name = "a"
-val type_guard_name = "g"
-val type_tag_name = "t"
-val simple_type_prefix = "ty_"
+val predicator_name = "pp"
+val app_op_name = "aa"
+val type_guard_name = "gg"
+val type_tag_name = "tt"
 
 val prefixed_predicator_name = const_prefix ^ predicator_name
 val prefixed_app_op_name = const_prefix ^ app_op_name
@@ -1097,17 +1097,15 @@
   | should_encode_type ctxt {maybe_finite_Ts, surely_infinite_Ts,
                              maybe_nonmono_Ts, ...}
                        (Noninf_Nonmono_Types soundness) T =
-    exists (type_instance ctxt T orf type_generalization ctxt T)
-           maybe_nonmono_Ts andalso
+    exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
     not (exists (type_instance ctxt T) surely_infinite_Ts orelse
          (not (member (type_aconv ctxt) maybe_finite_Ts T) andalso
           is_type_surely_infinite' ctxt soundness surely_infinite_Ts T))
   | should_encode_type ctxt {surely_finite_Ts, maybe_infinite_Ts,
                              maybe_nonmono_Ts, ...}
                        Fin_Nonmono_Types T =
-    exists (type_instance ctxt T orf type_generalization ctxt T)
-           maybe_nonmono_Ts andalso
-    (exists (type_instance ctxt T) surely_finite_Ts orelse
+    exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
+    (exists (type_generalization ctxt T) surely_finite_Ts orelse
      (not (member (type_aconv ctxt) maybe_infinite_Ts T) andalso
       is_type_surely_finite ctxt T))
   | should_encode_type _ _ _ _ = false
diff -r e3e8d20a6ebc -r ba22ed224b20 src/HOL/Tools/ATP/atp_util.ML
--- a/src/HOL/Tools/ATP/atp_util.ML	Thu Aug 25 14:06:34 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML	Thu Aug 25 14:25:06 2011 +0200
@@ -17,6 +17,7 @@
   val string_from_time : Time.time -> string
   val type_instance : Proof.context -> typ -> typ -> bool
   val type_generalization : Proof.context -> typ -> typ -> bool
+  val type_intersect : Proof.context -> typ -> typ -> bool
   val type_aconv : Proof.context -> typ * typ -> bool
   val varify_type : Proof.context -> typ -> typ
   val instantiate_type : theory -> typ -> typ -> typ -> typ
@@ -117,6 +118,8 @@
 fun type_instance ctxt T T' =
   Sign.typ_instance (Proof_Context.theory_of ctxt) (T, T')
 fun type_generalization ctxt T T' = type_instance ctxt T' T
+fun type_intersect ctxt T T' =
+  type_instance ctxt T T' orelse type_generalization ctxt T T'
 fun type_aconv ctxt (T, T') =
   type_instance ctxt T T' andalso type_instance ctxt T' T