src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 33864 232daf7eafaf
parent 33851 ab6ecae44033
child 33876 62bcf6a52493
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Nov 23 14:34:05 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Nov 23 17:26:32 2009 +0100
@@ -514,10 +514,12 @@
           set_name = set_prefix ^ s, Rep_inverse = SOME Rep_inverse}
   | NONE => NONE
 
+(* FIXME: use antiquotation for "code_numeral" below or detect "rep_datatype",
+   e.g., by adding a field to "DatatypeAux.info". *)
 (* string -> bool *)
 fun is_basic_datatype s =
     s mem [@{type_name "*"}, @{type_name bool}, @{type_name unit},
-           @{type_name nat}, @{type_name int}]
+           @{type_name nat}, @{type_name int}, "Code_Numeral.code_numeral"]
 (* theory -> string -> bool *)
 val is_typedef = is_some oo typedef_info
 val is_real_datatype = is_some oo Datatype.get_info
@@ -539,7 +541,7 @@
           try (fst o dest_Const o snd o Logic.dest_equals o prop_of) thm
         | NONE =>
           try (fst o dest_Const o snd o HOLogic.dest_mem
-               o HOLogic.dest_Trueprop) prop_of_Rep) = SOME @{const_name UNIV}
+               o HOLogic.dest_Trueprop) prop_of_Rep) = SOME @{const_name top}
      | NONE => false)
   | is_univ_typedef _ _ = false
 fun is_datatype thy (T as Type (s, _)) =
@@ -1288,8 +1290,10 @@
   end
 (* theory -> styp -> term *)
 fun inverse_axiom_for_rep_fun thy (x as (_, T)) =
-  typedef_info thy (fst (dest_Type (domain_type T)))
-  |> the |> #Rep_inverse |> the |> prop_of |> Refute.specialize_type thy x
+  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
+  end
 
 (* theory -> int * styp -> term *)
 fun constr_case_body thy (j, (x as (_, T))) =
@@ -1404,6 +1408,7 @@
   | _ => NONE
 (* theory -> term -> bool *)
 fun is_constr_pattern _ (Bound _) = true
+  | is_constr_pattern _ (Var _) = true
   | is_constr_pattern thy t =
     case strip_comb t of
       (Const (x as (s, _)), args) =>
@@ -1445,7 +1450,7 @@
           else
             raise SAME ())
          handle SAME () => betapply (do_term depth Ts t0, do_term depth Ts t1))
-      | Const (@{const_name refl_on}, T) $ Const (@{const_name UNIV}, _) $ t2 =>
+      | Const (@{const_name refl_on}, T) $ Const (@{const_name top}, _) $ t2 =>
         do_const depth Ts t (@{const_name refl'}, range_type T) [t2]
       | (t0 as Const (x as (@{const_name Sigma}, T))) $ t1
         $ (t2 as Abs (_, _, t2')) =>
@@ -1492,7 +1497,7 @@
                 if is_finite_type ext_ctxt (domain_type T) then
                   (Abs ("A", domain_type T, @{const True}), ts)
                 else case ts of
-                  [Const (@{const_name UNIV}, _)] => (@{const False}, [])
+                  [Const (@{const_name top}, _)] => (@{const False}, [])
                 | _ => (Const x, ts)
               else
                 (Const x, ts)
@@ -3004,10 +3009,14 @@
           end
       end
     (* int -> term -> accumulator -> accumulator *)
+    and add_def_axiom depth = add_axiom fst apfst depth
     and add_nondef_axiom depth = add_axiom snd apsnd depth
-    and add_def_axiom depth t =
-      (if head_of t = @{const "==>"} then add_nondef_axiom
-       else add_axiom fst apfst) depth t
+    and add_maybe_def_axiom depth t =
+      (if head_of t <> @{const "==>"} then add_def_axiom
+       else add_nondef_axiom) depth t
+    and add_eq_axiom depth t =
+      (if is_constr_pattern_formula thy t then add_def_axiom
+       else add_nondef_axiom) depth t
     (* int -> term -> accumulator -> accumulator *)
     and add_axioms_for_term depth t (accum as (xs, axs)) =
       case t of
@@ -3029,29 +3038,33 @@
                  val ax1 = try (Refute.specialize_type thy x) of_class
                  val ax2 = Option.map (Refute.specialize_type thy x o snd)
                                       (Refute.get_classdef thy class)
-               in fold (add_def_axiom depth) (map_filter I [ax1, ax2]) accum end
+               in
+                 fold (add_maybe_def_axiom depth) (map_filter I [ax1, ax2])
+                      accum
+               end
              else if is_constr thy x then
                accum
              else if is_equational_fun ext_ctxt x then
-               fold (add_def_axiom depth) (equational_fun_axioms ext_ctxt x)
+               fold (add_eq_axiom depth) (equational_fun_axioms ext_ctxt x)
                     accum
              else if is_abs_fun thy x then
                accum |> fold (add_nondef_axiom depth)
                              (nondef_props_for_const thy false nondef_table x)
                      |> is_funky_typedef thy (range_type T)
-                        ? fold (add_def_axiom depth)
+                        ? fold (add_maybe_def_axiom depth)
                                (nondef_props_for_const thy true
                                                     (extra_table def_table s) x)
              else if is_rep_fun thy x then
                accum |> fold (add_nondef_axiom depth)
                              (nondef_props_for_const thy false nondef_table x)
                      |> is_funky_typedef thy (range_type T)
-                        ? fold (add_def_axiom depth)
+                        ? fold (add_maybe_def_axiom depth)
                                (nondef_props_for_const thy true
                                                     (extra_table def_table s) x)
                      |> add_axioms_for_term depth
                                             (Const (mate_of_rep_fun thy x))
-                     |> add_def_axiom depth (inverse_axiom_for_rep_fun thy x)
+                     |> add_maybe_def_axiom depth
+                                            (inverse_axiom_for_rep_fun thy x)
              else
                accum |> user_axioms <> SOME false
                         ? fold (add_nondef_axiom depth)
@@ -3076,9 +3089,10 @@
       | Type (z as (_, Ts)) =>
         fold (add_axioms_for_type depth) Ts
         #> (if is_pure_typedef thy T then
-              fold (add_def_axiom depth) (optimized_typedef_axioms thy z)
+              fold (add_maybe_def_axiom depth) (optimized_typedef_axioms thy z)
             else if max_bisim_depth >= 0 andalso is_codatatype thy T then
-              fold (add_def_axiom depth) (codatatype_bisim_axioms ext_ctxt T)
+              fold (add_maybe_def_axiom depth)
+                   (codatatype_bisim_axioms ext_ctxt T)
             else
               I)
     (* int -> typ -> sort -> accumulator -> accumulator *)