# HG changeset patch
# User blanchet
# Date 1315608265 -7200
# Node ID 237ba63d6041137cc895d779379d34ed2cbc92bf
# Parent  d615dfa8857220f9e23a17821288f6e9af2a63a0
fixed definition of type intersection (soundness bug)

diff -r d615dfa88572 -r 237ba63d6041 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Sat Sep 10 00:44:25 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Sat Sep 10 00:44:25 2011 +0200
@@ -1257,7 +1257,7 @@
     grain = Ghost_Type_Arg_Vars orelse
     (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
+          (not (member (type_equiv ctxt) maybe_finite_Ts T) andalso
            is_type_kind_of_surely_infinite ctxt soundness surely_infinite_Ts
                                            T)))
   | should_encode_type ctxt {surely_finite_Ts, maybe_infinite_Ts,
@@ -1266,7 +1266,7 @@
     grain = Ghost_Type_Arg_Vars 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
+      (not (member (type_equiv ctxt) maybe_infinite_Ts T) andalso
        is_type_surely_finite ctxt T)))
   | should_encode_type _ _ _ _ = false
 
@@ -1978,7 +1978,7 @@
       case level of
         Noninf_Nonmono_Types (soundness, _) =>
         if exists (type_instance ctxt T) surely_infinite_Ts orelse
-           member (type_aconv ctxt) maybe_finite_Ts T then
+           member (type_equiv ctxt) maybe_finite_Ts T then
           mono
         else if is_type_kind_of_surely_infinite ctxt soundness
                                                 surely_infinite_Ts T then
@@ -1988,14 +1988,14 @@
            surely_infinite_Ts = surely_infinite_Ts |> insert_type ctxt I T,
            maybe_nonmono_Ts = maybe_nonmono_Ts}
         else
-          {maybe_finite_Ts = maybe_finite_Ts |> insert (type_aconv ctxt) T,
+          {maybe_finite_Ts = maybe_finite_Ts |> insert (type_equiv ctxt) T,
            surely_finite_Ts = surely_finite_Ts,
            maybe_infinite_Ts = maybe_infinite_Ts,
            surely_infinite_Ts = surely_infinite_Ts,
            maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type ctxt I T}
       | Fin_Nonmono_Types _ =>
         if exists (type_instance ctxt T) surely_finite_Ts orelse
-           member (type_aconv ctxt) maybe_infinite_Ts T then
+           member (type_equiv ctxt) maybe_infinite_Ts T then
           mono
         else if is_type_surely_finite ctxt T then
           {maybe_finite_Ts = maybe_finite_Ts,
@@ -2006,7 +2006,7 @@
         else
           {maybe_finite_Ts = maybe_finite_Ts,
            surely_finite_Ts = surely_finite_Ts,
-           maybe_infinite_Ts = maybe_infinite_Ts |> insert (type_aconv ctxt) T,
+           maybe_infinite_Ts = maybe_infinite_Ts |> insert (type_equiv ctxt) T,
            surely_infinite_Ts = surely_infinite_Ts,
            maybe_nonmono_Ts = maybe_nonmono_Ts}
       | _ => mono
diff -r d615dfa88572 -r 237ba63d6041 src/HOL/Tools/ATP/atp_util.ML
--- a/src/HOL/Tools/ATP/atp_util.ML	Sat Sep 10 00:44:25 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML	Sat Sep 10 00:44:25 2011 +0200
@@ -19,7 +19,7 @@
   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 type_equiv : Proof.context -> typ * typ -> bool
   val varify_type : Proof.context -> typ -> typ
   val instantiate_type : theory -> typ -> typ -> typ -> typ
   val varify_and_instantiate_type : Proof.context -> typ -> typ -> typ -> typ
@@ -123,9 +123,8 @@
   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
+  can (Sign.typ_unify (Proof_Context.theory_of ctxt) (T, T')) (Vartab.empty, 0)
+val type_equiv = Sign.typ_equiv o Proof_Context.theory_of
 
 fun varify_type ctxt T =
   Variable.polymorphic_types ctxt [Const (@{const_name undefined}, T)]
@@ -172,7 +171,7 @@
     fun aux slack avoid T =
       if member (op =) avoid T then
         0
-      else case AList.lookup (type_aconv ctxt) assigns T of
+      else case AList.lookup (type_equiv ctxt) assigns T of
         SOME k => k
       | NONE =>
         case T of