fixed unsoundness in SMT(2) as oracle: don't register typedef Abs_x as constructor unless it is known to be injective
authorblanchet
Wed Jun 11 11:28:46 2014 +0200 (2014-06-11)
changeset 572139daec42f6784
parent 57212 f25dad3d6144
child 57214 c4986877deea
fixed unsoundness in SMT(2) as oracle: don't register typedef Abs_x as constructor unless it is known to be injective
src/HOL/SMT.thy
src/HOL/Tools/SMT/smt_datatypes.ML
src/HOL/Tools/SMT2/smt2_datatypes.ML
     1.1 --- a/src/HOL/SMT.thy	Wed Jun 11 11:28:46 2014 +0200
     1.2 +++ b/src/HOL/SMT.thy	Wed Jun 11 11:28:46 2014 +0200
     1.3 @@ -419,7 +419,6 @@
     1.4    "(if P then Q else \<not>R) \<or> P \<or> R"
     1.5    by auto
     1.6  
     1.7 -
     1.8  hide_type (open) pattern
     1.9  hide_const fun_app term_true term_false z3div z3mod
    1.10  hide_const (open) trigger pat nopat weight
     2.1 --- a/src/HOL/Tools/SMT/smt_datatypes.ML	Wed Jun 11 11:28:46 2014 +0200
     2.2 +++ b/src/HOL/Tools/SMT/smt_datatypes.ML	Wed Jun 11 11:28:46 2014 +0200
     2.3 @@ -71,16 +71,18 @@
     2.4  
     2.5  (* typedef declarations *)
     2.6  
     2.7 -fun get_typedef_decl (info : Typedef.info) T Ts =
     2.8 -  let
     2.9 -    val ({Abs_name, Rep_name, abs_type, rep_type, ...}, _) = info
    2.10 +fun get_typedef_decl (({Abs_name, Rep_name, abs_type, rep_type, ...}, {Abs_inverse, ...})
    2.11 +    : Typedef.info) T Ts =
    2.12 +  if can (curry (op RS) @{thm UNIV_I}) Abs_inverse then
    2.13 +    let
    2.14 +      val env = snd (Term.dest_Type abs_type) ~~ Ts
    2.15 +      val instT = Term.map_atyps (perhaps (AList.lookup (op =) env))
    2.16  
    2.17 -    val env = snd (Term.dest_Type abs_type) ~~ Ts
    2.18 -    val instT = Term.map_atyps (perhaps (AList.lookup (op =) env))
    2.19 -
    2.20 -    val constr = Const (Abs_name, instT (rep_type --> abs_type))
    2.21 -    val select = Const (Rep_name, instT (abs_type --> rep_type))
    2.22 -  in (T, [(constr, [select])]) end
    2.23 +      val constr = Const (Abs_name, instT (rep_type --> abs_type))
    2.24 +      val select = Const (Rep_name, instT (abs_type --> rep_type))
    2.25 +    in [(T, [(constr, [select])])] end
    2.26 +  else
    2.27 +    []
    2.28  
    2.29  
    2.30  (* collection of declarations *)
    2.31 @@ -99,7 +101,7 @@
    2.32          | NONE =>
    2.33              (case Typedef.get_info ctxt n of
    2.34                [] => ([], ctxt)
    2.35 -            | info :: _ => ([get_typedef_decl info T Ts], ctxt))))
    2.36 +            | info :: _ => (get_typedef_decl info T Ts, ctxt))))
    2.37    end
    2.38  
    2.39  fun add_decls T (declss, ctxt) =
     3.1 --- a/src/HOL/Tools/SMT2/smt2_datatypes.ML	Wed Jun 11 11:28:46 2014 +0200
     3.2 +++ b/src/HOL/Tools/SMT2/smt2_datatypes.ML	Wed Jun 11 11:28:46 2014 +0200
     3.3 @@ -19,8 +19,7 @@
     3.4  
     3.5  fun mk_selectors T Ts ctxt =
     3.6    let
     3.7 -    val (sels, ctxt') =
     3.8 -      Variable.variant_fixes (replicate (length Ts) "select") ctxt
     3.9 +    val (sels, ctxt') = Variable.variant_fixes (replicate (length Ts) "select") ctxt
    3.10    in (map2 (fn n => fn U => Free (n, T --> U)) sels Ts, ctxt') end
    3.11  
    3.12  
    3.13 @@ -71,16 +70,18 @@
    3.14  
    3.15  (* typedef declarations *)
    3.16  
    3.17 -fun get_typedef_decl (info : Typedef.info) T Ts =
    3.18 -  let
    3.19 -    val ({Abs_name, Rep_name, abs_type, rep_type, ...}, _) = info
    3.20 +fun get_typedef_decl (({Abs_name, Rep_name, abs_type, rep_type, ...}, {Abs_inverse, ...})
    3.21 +    : Typedef.info) T Ts =
    3.22 +  if can (curry (op RS) @{thm UNIV_I}) Abs_inverse then
    3.23 +    let
    3.24 +      val env = snd (Term.dest_Type abs_type) ~~ Ts
    3.25 +      val instT = Term.map_atyps (perhaps (AList.lookup (op =) env))
    3.26  
    3.27 -    val env = snd (Term.dest_Type abs_type) ~~ Ts
    3.28 -    val instT = Term.map_atyps (perhaps (AList.lookup (op =) env))
    3.29 -
    3.30 -    val constr = Const (Abs_name, instT (rep_type --> abs_type))
    3.31 -    val select = Const (Rep_name, instT (abs_type --> rep_type))
    3.32 -  in (T, [(constr, [select])]) end
    3.33 +      val constr = Const (Abs_name, instT (rep_type --> abs_type))
    3.34 +      val select = Const (Rep_name, instT (abs_type --> rep_type))
    3.35 +    in [(T, [(constr, [select])])] end
    3.36 +  else
    3.37 +    []
    3.38  
    3.39  
    3.40  (* collection of declarations *)
    3.41 @@ -99,7 +100,7 @@
    3.42          | NONE =>
    3.43              (case Typedef.get_info ctxt n of
    3.44                [] => ([], ctxt)
    3.45 -            | info :: _ => ([get_typedef_decl info T Ts], ctxt))))
    3.46 +            | info :: _ => (get_typedef_decl info T Ts, ctxt))))
    3.47    end
    3.48  
    3.49  fun add_decls T (declss, ctxt) =