fix Nitpick soundness bugs related to integration (in particular, "code_numeral")
authorblanchet
Mon Nov 23 17:26:32 2009 +0100 (2009-11-23)
changeset 33864232daf7eafaf
parent 33863 fb13147a3050
child 33865 8f335b40b550
fix Nitpick soundness bugs related to integration (in particular, "code_numeral")
src/HOL/Tools/Nitpick/nitpick_hol.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Nov 23 14:34:05 2009 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Nov 23 17:26:32 2009 +0100
     1.3 @@ -514,10 +514,12 @@
     1.4            set_name = set_prefix ^ s, Rep_inverse = SOME Rep_inverse}
     1.5    | NONE => NONE
     1.6  
     1.7 +(* FIXME: use antiquotation for "code_numeral" below or detect "rep_datatype",
     1.8 +   e.g., by adding a field to "DatatypeAux.info". *)
     1.9  (* string -> bool *)
    1.10  fun is_basic_datatype s =
    1.11      s mem [@{type_name "*"}, @{type_name bool}, @{type_name unit},
    1.12 -           @{type_name nat}, @{type_name int}]
    1.13 +           @{type_name nat}, @{type_name int}, "Code_Numeral.code_numeral"]
    1.14  (* theory -> string -> bool *)
    1.15  val is_typedef = is_some oo typedef_info
    1.16  val is_real_datatype = is_some oo Datatype.get_info
    1.17 @@ -539,7 +541,7 @@
    1.18            try (fst o dest_Const o snd o Logic.dest_equals o prop_of) thm
    1.19          | NONE =>
    1.20            try (fst o dest_Const o snd o HOLogic.dest_mem
    1.21 -               o HOLogic.dest_Trueprop) prop_of_Rep) = SOME @{const_name UNIV}
    1.22 +               o HOLogic.dest_Trueprop) prop_of_Rep) = SOME @{const_name top}
    1.23       | NONE => false)
    1.24    | is_univ_typedef _ _ = false
    1.25  fun is_datatype thy (T as Type (s, _)) =
    1.26 @@ -1288,8 +1290,10 @@
    1.27    end
    1.28  (* theory -> styp -> term *)
    1.29  fun inverse_axiom_for_rep_fun thy (x as (_, T)) =
    1.30 -  typedef_info thy (fst (dest_Type (domain_type T)))
    1.31 -  |> the |> #Rep_inverse |> the |> prop_of |> Refute.specialize_type thy x
    1.32 +  let val abs_T = domain_type T in
    1.33 +    typedef_info thy (fst (dest_Type abs_T)) |> the |> #Rep_inverse |> the
    1.34 +    |> prop_of |> Refute.specialize_type thy x
    1.35 +  end
    1.36  
    1.37  (* theory -> int * styp -> term *)
    1.38  fun constr_case_body thy (j, (x as (_, T))) =
    1.39 @@ -1404,6 +1408,7 @@
    1.40    | _ => NONE
    1.41  (* theory -> term -> bool *)
    1.42  fun is_constr_pattern _ (Bound _) = true
    1.43 +  | is_constr_pattern _ (Var _) = true
    1.44    | is_constr_pattern thy t =
    1.45      case strip_comb t of
    1.46        (Const (x as (s, _)), args) =>
    1.47 @@ -1445,7 +1450,7 @@
    1.48            else
    1.49              raise SAME ())
    1.50           handle SAME () => betapply (do_term depth Ts t0, do_term depth Ts t1))
    1.51 -      | Const (@{const_name refl_on}, T) $ Const (@{const_name UNIV}, _) $ t2 =>
    1.52 +      | Const (@{const_name refl_on}, T) $ Const (@{const_name top}, _) $ t2 =>
    1.53          do_const depth Ts t (@{const_name refl'}, range_type T) [t2]
    1.54        | (t0 as Const (x as (@{const_name Sigma}, T))) $ t1
    1.55          $ (t2 as Abs (_, _, t2')) =>
    1.56 @@ -1492,7 +1497,7 @@
    1.57                  if is_finite_type ext_ctxt (domain_type T) then
    1.58                    (Abs ("A", domain_type T, @{const True}), ts)
    1.59                  else case ts of
    1.60 -                  [Const (@{const_name UNIV}, _)] => (@{const False}, [])
    1.61 +                  [Const (@{const_name top}, _)] => (@{const False}, [])
    1.62                  | _ => (Const x, ts)
    1.63                else
    1.64                  (Const x, ts)
    1.65 @@ -3004,10 +3009,14 @@
    1.66            end
    1.67        end
    1.68      (* int -> term -> accumulator -> accumulator *)
    1.69 +    and add_def_axiom depth = add_axiom fst apfst depth
    1.70      and add_nondef_axiom depth = add_axiom snd apsnd depth
    1.71 -    and add_def_axiom depth t =
    1.72 -      (if head_of t = @{const "==>"} then add_nondef_axiom
    1.73 -       else add_axiom fst apfst) depth t
    1.74 +    and add_maybe_def_axiom depth t =
    1.75 +      (if head_of t <> @{const "==>"} then add_def_axiom
    1.76 +       else add_nondef_axiom) depth t
    1.77 +    and add_eq_axiom depth t =
    1.78 +      (if is_constr_pattern_formula thy t then add_def_axiom
    1.79 +       else add_nondef_axiom) depth t
    1.80      (* int -> term -> accumulator -> accumulator *)
    1.81      and add_axioms_for_term depth t (accum as (xs, axs)) =
    1.82        case t of
    1.83 @@ -3029,29 +3038,33 @@
    1.84                   val ax1 = try (Refute.specialize_type thy x) of_class
    1.85                   val ax2 = Option.map (Refute.specialize_type thy x o snd)
    1.86                                        (Refute.get_classdef thy class)
    1.87 -               in fold (add_def_axiom depth) (map_filter I [ax1, ax2]) accum end
    1.88 +               in
    1.89 +                 fold (add_maybe_def_axiom depth) (map_filter I [ax1, ax2])
    1.90 +                      accum
    1.91 +               end
    1.92               else if is_constr thy x then
    1.93                 accum
    1.94               else if is_equational_fun ext_ctxt x then
    1.95 -               fold (add_def_axiom depth) (equational_fun_axioms ext_ctxt x)
    1.96 +               fold (add_eq_axiom depth) (equational_fun_axioms ext_ctxt x)
    1.97                      accum
    1.98               else if is_abs_fun thy x then
    1.99                 accum |> fold (add_nondef_axiom depth)
   1.100                               (nondef_props_for_const thy false nondef_table x)
   1.101                       |> is_funky_typedef thy (range_type T)
   1.102 -                        ? fold (add_def_axiom depth)
   1.103 +                        ? fold (add_maybe_def_axiom depth)
   1.104                                 (nondef_props_for_const thy true
   1.105                                                      (extra_table def_table s) x)
   1.106               else if is_rep_fun thy x then
   1.107                 accum |> fold (add_nondef_axiom depth)
   1.108                               (nondef_props_for_const thy false nondef_table x)
   1.109                       |> is_funky_typedef thy (range_type T)
   1.110 -                        ? fold (add_def_axiom depth)
   1.111 +                        ? fold (add_maybe_def_axiom depth)
   1.112                                 (nondef_props_for_const thy true
   1.113                                                      (extra_table def_table s) x)
   1.114                       |> add_axioms_for_term depth
   1.115                                              (Const (mate_of_rep_fun thy x))
   1.116 -                     |> add_def_axiom depth (inverse_axiom_for_rep_fun thy x)
   1.117 +                     |> add_maybe_def_axiom depth
   1.118 +                                            (inverse_axiom_for_rep_fun thy x)
   1.119               else
   1.120                 accum |> user_axioms <> SOME false
   1.121                          ? fold (add_nondef_axiom depth)
   1.122 @@ -3076,9 +3089,10 @@
   1.123        | Type (z as (_, Ts)) =>
   1.124          fold (add_axioms_for_type depth) Ts
   1.125          #> (if is_pure_typedef thy T then
   1.126 -              fold (add_def_axiom depth) (optimized_typedef_axioms thy z)
   1.127 +              fold (add_maybe_def_axiom depth) (optimized_typedef_axioms thy z)
   1.128              else if max_bisim_depth >= 0 andalso is_codatatype thy T then
   1.129 -              fold (add_def_axiom depth) (codatatype_bisim_axioms ext_ctxt T)
   1.130 +              fold (add_maybe_def_axiom depth)
   1.131 +                   (codatatype_bisim_axioms ext_ctxt T)
   1.132              else
   1.133                I)
   1.134      (* int -> typ -> sort -> accumulator -> accumulator *)