# HG changeset patch
# User blanchet
# Date 1402478926 -7200
# Node ID 9daec42f67842245189cd50f9c96753afe311db5
# Parent  f25dad3d6144f5b4703a4e7698f562b5776ce143
fixed unsoundness in SMT(2) as oracle: don't register typedef Abs_x as constructor unless it is known to be injective

diff -r f25dad3d6144 -r 9daec42f6784 src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Wed Jun 11 11:28:46 2014 +0200
+++ b/src/HOL/SMT.thy	Wed Jun 11 11:28:46 2014 +0200
@@ -419,7 +419,6 @@
   "(if P then Q else \<not>R) \<or> P \<or> R"
   by auto
 
-
 hide_type (open) pattern
 hide_const fun_app term_true term_false z3div z3mod
 hide_const (open) trigger pat nopat weight
diff -r f25dad3d6144 -r 9daec42f6784 src/HOL/Tools/SMT/smt_datatypes.ML
--- a/src/HOL/Tools/SMT/smt_datatypes.ML	Wed Jun 11 11:28:46 2014 +0200
+++ b/src/HOL/Tools/SMT/smt_datatypes.ML	Wed Jun 11 11:28:46 2014 +0200
@@ -71,16 +71,18 @@
 
 (* typedef declarations *)
 
-fun get_typedef_decl (info : Typedef.info) T Ts =
-  let
-    val ({Abs_name, Rep_name, abs_type, rep_type, ...}, _) = info
+fun get_typedef_decl (({Abs_name, Rep_name, abs_type, rep_type, ...}, {Abs_inverse, ...})
+    : Typedef.info) T Ts =
+  if can (curry (op RS) @{thm UNIV_I}) Abs_inverse then
+    let
+      val env = snd (Term.dest_Type abs_type) ~~ Ts
+      val instT = Term.map_atyps (perhaps (AList.lookup (op =) env))
 
-    val env = snd (Term.dest_Type abs_type) ~~ Ts
-    val instT = Term.map_atyps (perhaps (AList.lookup (op =) env))
-
-    val constr = Const (Abs_name, instT (rep_type --> abs_type))
-    val select = Const (Rep_name, instT (abs_type --> rep_type))
-  in (T, [(constr, [select])]) end
+      val constr = Const (Abs_name, instT (rep_type --> abs_type))
+      val select = Const (Rep_name, instT (abs_type --> rep_type))
+    in [(T, [(constr, [select])])] end
+  else
+    []
 
 
 (* collection of declarations *)
@@ -99,7 +101,7 @@
         | NONE =>
             (case Typedef.get_info ctxt n of
               [] => ([], ctxt)
-            | info :: _ => ([get_typedef_decl info T Ts], ctxt))))
+            | info :: _ => (get_typedef_decl info T Ts, ctxt))))
   end
 
 fun add_decls T (declss, ctxt) =
diff -r f25dad3d6144 -r 9daec42f6784 src/HOL/Tools/SMT2/smt2_datatypes.ML
--- a/src/HOL/Tools/SMT2/smt2_datatypes.ML	Wed Jun 11 11:28:46 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_datatypes.ML	Wed Jun 11 11:28:46 2014 +0200
@@ -19,8 +19,7 @@
 
 fun mk_selectors T Ts ctxt =
   let
-    val (sels, ctxt') =
-      Variable.variant_fixes (replicate (length Ts) "select") ctxt
+    val (sels, ctxt') = Variable.variant_fixes (replicate (length Ts) "select") ctxt
   in (map2 (fn n => fn U => Free (n, T --> U)) sels Ts, ctxt') end
 
 
@@ -71,16 +70,18 @@
 
 (* typedef declarations *)
 
-fun get_typedef_decl (info : Typedef.info) T Ts =
-  let
-    val ({Abs_name, Rep_name, abs_type, rep_type, ...}, _) = info
+fun get_typedef_decl (({Abs_name, Rep_name, abs_type, rep_type, ...}, {Abs_inverse, ...})
+    : Typedef.info) T Ts =
+  if can (curry (op RS) @{thm UNIV_I}) Abs_inverse then
+    let
+      val env = snd (Term.dest_Type abs_type) ~~ Ts
+      val instT = Term.map_atyps (perhaps (AList.lookup (op =) env))
 
-    val env = snd (Term.dest_Type abs_type) ~~ Ts
-    val instT = Term.map_atyps (perhaps (AList.lookup (op =) env))
-
-    val constr = Const (Abs_name, instT (rep_type --> abs_type))
-    val select = Const (Rep_name, instT (abs_type --> rep_type))
-  in (T, [(constr, [select])]) end
+      val constr = Const (Abs_name, instT (rep_type --> abs_type))
+      val select = Const (Rep_name, instT (abs_type --> rep_type))
+    in [(T, [(constr, [select])])] end
+  else
+    []
 
 
 (* collection of declarations *)
@@ -99,7 +100,7 @@
         | NONE =>
             (case Typedef.get_info ctxt n of
               [] => ([], ctxt)
-            | info :: _ => ([get_typedef_decl info T Ts], ctxt))))
+            | info :: _ => (get_typedef_decl info T Ts, ctxt))))
   end
 
 fun add_decls T (declss, ctxt) =