fixed soundness bug in Nitpick's handling of typedefs
authorblanchet
Mon Nov 23 17:59:22 2009 +0100 (2009-11-23)
changeset 3387662bcf6a52493
parent 33865 8f335b40b550
child 33877 e779bea3d337
fixed soundness bug in Nitpick's handling of typedefs
src/HOL/Tools/Nitpick/HISTORY
src/HOL/Tools/Nitpick/nitpick_hol.ML
     1.1 --- a/src/HOL/Tools/Nitpick/HISTORY	Mon Nov 23 17:27:43 2009 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/HISTORY	Mon Nov 23 17:59:22 2009 +0100
     1.3 @@ -10,8 +10,8 @@
     1.4    * Optimized Kodkod encoding of datatypes whose constructors don't appear in
     1.5      the formula to falsify
     1.6    * Added support for codatatype view of datatypes
     1.7 -  * Fixed soundness bugs related to sets, sets of sets, and (co)inductive
     1.8 -    predicates
     1.9 +  * Fixed soundness bugs related to sets, sets of sets, (co)inductive
    1.10 +    predicates, and typedefs
    1.11    * Fixed monotonicity check
    1.12    * Fixed error when processing definitions
    1.13    * Fixed error in "star_linear_preds" optimization
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Nov 23 17:27:43 2009 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Nov 23 17:59:22 2009 +0100
     2.3 @@ -496,7 +496,7 @@
     2.4  type typedef_info =
     2.5    {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string,
     2.6     set_def: thm option, prop_of_Rep: thm, set_name: string,
     2.7 -   Rep_inverse: thm option}
     2.8 +   Abs_inverse: thm option, Rep_inverse: thm option}
     2.9  
    2.10  (* theory -> string -> typedef_info *)
    2.11  fun typedef_info thy s =
    2.12 @@ -505,13 +505,14 @@
    2.13            Abs_name = @{const_name Abs_Frac}, Rep_name = @{const_name Rep_Frac},
    2.14            set_def = NONE, prop_of_Rep = @{prop "Rep_Frac x \<in> Frac"}
    2.15                            |> Logic.varify,
    2.16 -          set_name = @{const_name Frac}, Rep_inverse = NONE}
    2.17 +          set_name = @{const_name Frac}, Abs_inverse = NONE, Rep_inverse = NONE}
    2.18    else case Typedef.get_info thy s of
    2.19 -    SOME {abs_type, rep_type, Abs_name, Rep_name, set_def, Rep, Rep_inverse,
    2.20 -          ...} =>
    2.21 +    SOME {abs_type, rep_type, Abs_name, Rep_name, set_def, Rep, Abs_inverse,
    2.22 +          Rep_inverse, ...} =>
    2.23      SOME {abs_type = abs_type, rep_type = rep_type, Abs_name = Abs_name,
    2.24            Rep_name = Rep_name, set_def = set_def, prop_of_Rep = prop_of Rep,
    2.25 -          set_name = set_prefix ^ s, Rep_inverse = SOME Rep_inverse}
    2.26 +          set_name = set_prefix ^ s, Abs_inverse = SOME Abs_inverse,
    2.27 +          Rep_inverse = SOME Rep_inverse}
    2.28    | NONE => NONE
    2.29  
    2.30  (* FIXME: use antiquotation for "code_numeral" below or detect "rep_datatype",
    2.31 @@ -1288,11 +1289,13 @@
    2.32        end
    2.33      | NONE => []
    2.34    end
    2.35 -(* theory -> styp -> term *)
    2.36 -fun inverse_axiom_for_rep_fun thy (x as (_, T)) =
    2.37 +(* theory -> styp -> term list *)
    2.38 +fun inverse_axioms_for_rep_fun thy (x as (_, T)) =
    2.39    let val abs_T = domain_type T in
    2.40 -    typedef_info thy (fst (dest_Type abs_T)) |> the |> #Rep_inverse |> the
    2.41 -    |> prop_of |> Refute.specialize_type thy x
    2.42 +    typedef_info thy (fst (dest_Type abs_T)) |> the
    2.43 +    |> pairf #Abs_inverse #Rep_inverse
    2.44 +    |> pairself (Refute.specialize_type thy x o prop_of o the)
    2.45 +    ||> single |> op ::
    2.46    end
    2.47  
    2.48  (* theory -> int * styp -> term *)
    2.49 @@ -3063,8 +3066,8 @@
    2.50                                                      (extra_table def_table s) x)
    2.51                       |> add_axioms_for_term depth
    2.52                                              (Const (mate_of_rep_fun thy x))
    2.53 -                     |> add_maybe_def_axiom depth
    2.54 -                                            (inverse_axiom_for_rep_fun thy x)
    2.55 +                     |> fold (add_def_axiom depth)
    2.56 +                             (inverse_axioms_for_rep_fun thy x)
    2.57               else
    2.58                 accum |> user_axioms <> SOME false
    2.59                          ? fold (add_nondef_axiom depth)