# HG changeset patch
# User blanchet
# Date 1366015263 -7200
# Node ID 0a4b4735d8bdb0f64743fa82997e43b3b8d67916
# Parent  3d213f39d83c85ba2a61d59632f7ccd33a924d7d
not all Nitpick 'constructors' are injective -- careful

diff -r 3d213f39d83c -r 0a4b4735d8bd src/HOL/Nitpick_Examples/Typedef_Nits.thy
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Sun Apr 14 21:54:45 2013 +1000
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Mon Apr 15 10:41:03 2013 +0200
@@ -183,4 +183,14 @@
 nitpick [card = 1, expect = none]
 by (rule Rep_rat_inverse)
 
+typedef check = "{x\<Colon>nat. x < 2}" by (rule exI[of _ 0], auto)
+
+lemma "Rep_check (Abs_check n) = n \<Longrightarrow> n < 2"
+nitpick [card = 1\<emdash>3, expect = none]
+using Rep_check[of "Abs_check n"] by auto
+
+lemma "Rep_check (Abs_check n) = n \<Longrightarrow> n < 1"
+nitpick [card = 1\<emdash>3, expect = genuine]
+oops
+
 end
diff -r 3d213f39d83c -r 0a4b4735d8bd src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sun Apr 14 21:54:45 2013 +1000
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Apr 15 10:41:03 2013 +0200
@@ -130,6 +130,7 @@
   val is_quot_rep_fun : Proof.context -> styp -> bool
   val mate_of_rep_fun : Proof.context -> styp -> styp
   val is_constr_like : Proof.context -> styp -> bool
+  val is_constr_like_injective : Proof.context -> styp -> bool
   val is_constr : Proof.context -> (typ option * bool) list -> styp -> bool
   val is_sel : string -> bool
   val is_sel_like_and_no_discr : string -> bool
@@ -803,6 +804,11 @@
     (is_abs_fun ctxt x andalso is_pure_typedef ctxt (range_type T)) orelse
     is_coconstr ctxt x
   end
+fun is_constr_like_injective ctxt (s, T) =
+  is_constr_like ctxt (s, T) andalso
+  let val (x as (_, T)) = (s, unarize_unbox_etc_type T) in
+    not (is_abs_fun ctxt x) orelse is_univ_typedef ctxt (range_type T)
+  end
 fun is_stale_constr ctxt (x as (s, T)) =
   is_registered_type ctxt (body_type T) andalso is_constr_like ctxt x andalso
   not (s = @{const_name Nitpick.Abs_Frac} orelse is_coconstr ctxt x)
@@ -1186,9 +1192,12 @@
   let val thy = Proof_Context.theory_of ctxt in
     (case strip_comb t of
        (Const x', args) =>
-       if x = x' then nth args n
-       else if is_constr_like ctxt x' then Const (@{const_name unknown}, res_T)
-       else raise SAME ()
+       if x = x' then
+          if is_constr_like_injective ctxt x then nth args n else raise SAME ()
+       else if is_constr_like ctxt x' then
+         Const (@{const_name unknown}, res_T)
+       else
+         raise SAME ()
      | _ => raise SAME())
     handle SAME () =>
            s_betapply [] (nth_arg_sel_term_for_constr thy stds x n, t)
diff -r 3d213f39d83c -r 0a4b4735d8bd src/HOL/Tools/Nitpick/nitpick_preproc.ML
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Sun Apr 14 21:54:45 2013 +1000
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon Apr 15 10:41:03 2013 +0200
@@ -1086,7 +1086,7 @@
           else if is_sel_like_and_no_discr s then
             case strip_comb (hd args) of
               (Const (x' as (s', T')), ts') =>
-              if is_constr_like ctxt x' andalso
+              if is_constr_like_injective ctxt x' andalso
                  constr_name_for_sel_like s = s' andalso
                  not (exists is_pair_type (binder_types T')) then
                 list_comb (nth ts' (sel_no_from_name s), tl args)