# HG changeset patch
# User blanchet
# Date 1258995562 -3600
# Node ID 62bcf6a52493205cb0607ba9321ea9190f9c2b65
# Parent  8f335b40b550698681db1df37de9934f64e54eaf
fixed soundness bug in Nitpick's handling of typedefs

diff -r 8f335b40b550 -r 62bcf6a52493 src/HOL/Tools/Nitpick/HISTORY
--- a/src/HOL/Tools/Nitpick/HISTORY	Mon Nov 23 17:27:43 2009 +0100
+++ b/src/HOL/Tools/Nitpick/HISTORY	Mon Nov 23 17:59:22 2009 +0100
@@ -10,8 +10,8 @@
   * Optimized Kodkod encoding of datatypes whose constructors don't appear in
     the formula to falsify
   * Added support for codatatype view of datatypes
-  * Fixed soundness bugs related to sets, sets of sets, and (co)inductive
-    predicates
+  * Fixed soundness bugs related to sets, sets of sets, (co)inductive
+    predicates, and typedefs
   * Fixed monotonicity check
   * Fixed error when processing definitions
   * Fixed error in "star_linear_preds" optimization
diff -r 8f335b40b550 -r 62bcf6a52493 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Nov 23 17:27:43 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Nov 23 17:59:22 2009 +0100
@@ -496,7 +496,7 @@
 type typedef_info =
   {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string,
    set_def: thm option, prop_of_Rep: thm, set_name: string,
-   Rep_inverse: thm option}
+   Abs_inverse: thm option, Rep_inverse: thm option}
 
 (* theory -> string -> typedef_info *)
 fun typedef_info thy s =
@@ -505,13 +505,14 @@
           Abs_name = @{const_name Abs_Frac}, Rep_name = @{const_name Rep_Frac},
           set_def = NONE, prop_of_Rep = @{prop "Rep_Frac x \<in> Frac"}
                           |> Logic.varify,
-          set_name = @{const_name Frac}, Rep_inverse = NONE}
+          set_name = @{const_name Frac}, Abs_inverse = NONE, Rep_inverse = NONE}
   else case Typedef.get_info thy s of
-    SOME {abs_type, rep_type, Abs_name, Rep_name, set_def, Rep, Rep_inverse,
-          ...} =>
+    SOME {abs_type, rep_type, Abs_name, Rep_name, set_def, Rep, Abs_inverse,
+          Rep_inverse, ...} =>
     SOME {abs_type = abs_type, rep_type = rep_type, Abs_name = Abs_name,
           Rep_name = Rep_name, set_def = set_def, prop_of_Rep = prop_of Rep,
-          set_name = set_prefix ^ s, Rep_inverse = SOME Rep_inverse}
+          set_name = set_prefix ^ s, Abs_inverse = SOME Abs_inverse,
+          Rep_inverse = SOME Rep_inverse}
   | NONE => NONE
 
 (* FIXME: use antiquotation for "code_numeral" below or detect "rep_datatype",
@@ -1288,11 +1289,13 @@
       end
     | NONE => []
   end
-(* theory -> styp -> term *)
-fun inverse_axiom_for_rep_fun thy (x as (_, T)) =
+(* theory -> styp -> term list *)
+fun inverse_axioms_for_rep_fun thy (x as (_, T)) =
   let val abs_T = domain_type T in
-    typedef_info thy (fst (dest_Type abs_T)) |> the |> #Rep_inverse |> the
-    |> prop_of |> Refute.specialize_type thy x
+    typedef_info thy (fst (dest_Type abs_T)) |> the
+    |> pairf #Abs_inverse #Rep_inverse
+    |> pairself (Refute.specialize_type thy x o prop_of o the)
+    ||> single |> op ::
   end
 
 (* theory -> int * styp -> term *)
@@ -3063,8 +3066,8 @@
                                                     (extra_table def_table s) x)
                      |> add_axioms_for_term depth
                                             (Const (mate_of_rep_fun thy x))
-                     |> add_maybe_def_axiom depth
-                                            (inverse_axiom_for_rep_fun thy x)
+                     |> fold (add_def_axiom depth)
+                             (inverse_axioms_for_rep_fun thy x)
              else
                accum |> user_axioms <> SOME false
                         ? fold (add_nondef_axiom depth)