# HG changeset patch
# User blanchet
# Date 1393884330 -3600
# Node ID aed17a173d169f7edbcf18cc7ad935e6bd2a2c9d
# Parent  6fba7f6c532a0425282099a0127946484efb60d4
fixed handling of 'case_prod' and other 'case' functions for interpreted types

diff -r 6fba7f6c532a -r aed17a173d16 src/HOL/Nitpick_Examples/Core_Nits.thy
--- a/src/HOL/Nitpick_Examples/Core_Nits.thy	Mon Mar 03 22:33:22 2014 +0100
+++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Mon Mar 03 23:05:30 2014 +0100
@@ -11,29 +11,29 @@
 imports Main
 begin
 
-nitpick_params [verbose, card = 1\<emdash>6, unary_ints, max_potential = 0,
+nitpick_params [verbose, card = 1-6, unary_ints, max_potential = 0,
                 sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
 
 subsection {* Curry in a Hurry *}
 
 lemma "(\<lambda>f x y. (curry o split) f x y) = (\<lambda>f x y. (\<lambda>x. x) f x y)"
-nitpick [card = 1\<emdash>12, expect = none]
+nitpick [card = 1-12, expect = none]
 by auto
 
 lemma "(\<lambda>f p. (split o curry) f p) = (\<lambda>f p. (\<lambda>x. x) f p)"
-nitpick [card = 1\<emdash>12, expect = none]
+nitpick [card = 1-12, expect = none]
 by auto
 
 lemma "split (curry f) = f"
-nitpick [card = 1\<emdash>12, expect = none]
+nitpick [card = 1-12, expect = none]
 by auto
 
 lemma "curry (split f) = f"
-nitpick [card = 1\<emdash>12, expect = none]
+nitpick [card = 1-12, expect = none]
 by auto
 
 lemma "split (\<lambda>x y. f (x, y)) = f"
-nitpick [card = 1\<emdash>12, expect = none]
+nitpick [card = 1-12, expect = none]
 by auto
 
 subsection {* Representations *}
@@ -44,7 +44,7 @@
 
 lemma "(\<exists>g. \<forall>x. g (f x) = x) \<longrightarrow> (\<forall>y. \<exists>x. y = f x)"
 nitpick [card 'a = 25, card 'b = 24, expect = genuine]
-nitpick [card = 1\<emdash>10, mono, expect = none]
+nitpick [card = 1-10, mono, expect = none]
 oops
 
 lemma "\<exists>f. f = (\<lambda>x. x) \<and> f y \<noteq> y"
@@ -56,39 +56,39 @@
 oops
 
 lemma "{(a\<Colon>'a\<times>'a, b\<Colon>'b)}^-1 = {(b, a)}"
-nitpick [card = 1\<emdash>12, expect = none]
+nitpick [card = 1-12, expect = none]
 by auto
 
 lemma "fst (a, b) = a"
-nitpick [card = 1\<emdash>20, expect = none]
+nitpick [card = 1-20, expect = none]
 by auto
 
 lemma "\<exists>P. P = Id"
-nitpick [card = 1\<emdash>20, expect = none]
+nitpick [card = 1-20, expect = none]
 by auto
 
 lemma "(a\<Colon>'a\<Rightarrow>'b, a) \<in> Id\<^sup>*"
-nitpick [card = 1\<emdash>2, expect = none]
+nitpick [card = 1-2, expect = none]
 by auto
 
 lemma "(a\<Colon>'a\<times>'a, a) \<in> Id\<^sup>* \<union> {(a, b)}\<^sup>*"
-nitpick [card = 1\<emdash>4, expect = none]
+nitpick [card = 1-4, expect = none]
 by auto
 
 lemma "(a, a) \<in> Id"
-nitpick [card = 1\<emdash>50, expect = none]
+nitpick [card = 1-50, expect = none]
 by (auto simp: Id_def)
 
 lemma "((a\<Colon>'a, b\<Colon>'a), (a, b)) \<in> Id"
-nitpick [card = 1\<emdash>10, expect = none]
+nitpick [card = 1-10, expect = none]
 by (auto simp: Id_def)
 
 lemma "(x\<Colon>'a\<times>'a) \<in> UNIV"
-nitpick [card = 1\<emdash>50, expect = none]
+nitpick [card = 1-50, expect = none]
 sorry
 
 lemma "{} = A - A"
-nitpick [card = 1\<emdash>100, expect = none]
+nitpick [card = 1-100, expect = none]
 by auto
 
 lemma "g = Let (A \<or> B)"
@@ -132,7 +132,7 @@
 oops
 
 lemma "(x\<Colon>'a) = (\<lambda>a. \<lambda>b. \<lambda>c. if c then a else b) x x True"
-nitpick [card = 1\<emdash>10, expect = none]
+nitpick [card = 1-10, expect = none]
 by auto
 
 lemma "\<exists>F. F a b = G a b"
@@ -149,7 +149,7 @@
 
 lemma "(A, B) \<in> R \<or> (\<exists>C. (A, C) \<in> R \<and> (C, B) \<in> R) \<Longrightarrow>
        A = B \<or> (A, B) \<in> R \<or> (\<exists>C. (A, C) \<in> R \<and> (C, B) \<in> R)"
-nitpick [card = 1\<emdash>25, expect = none]
+nitpick [card = 1-25, expect = none]
 by auto
 
 lemma "f = (\<lambda>x\<Colon>'a\<times>'b. x)"
@@ -174,19 +174,19 @@
 oops
 
 lemma "\<exists>x\<Colon>'a \<Rightarrow> bool. x = y"
-nitpick [card 'a = 1\<emdash>15, expect = none]
+nitpick [card 'a = 1-15, expect = none]
 by auto
 
 lemma "\<exists>x y\<Colon>'a \<Rightarrow> bool. x = y"
-nitpick [card = 1\<emdash>15, expect = none]
+nitpick [card = 1-15, expect = none]
 by auto
 
 lemma "\<forall>x. \<exists>y. f x y = f x (g x)"
-nitpick [card = 1\<emdash>4, expect = none]
+nitpick [card = 1-4, expect = none]
 by auto
 
 lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. f u v w x = f u (g u) w (h u w)"
-nitpick [card = 1\<emdash>4, expect = none]
+nitpick [card = 1-4, expect = none]
 by auto
 
 lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. f u v w x = f u (g u w) w (h u)"
@@ -195,42 +195,42 @@
 
 lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. \<forall>y. \<exists>z.
        f u v w x y z = f u (g u) w (h u w) y (k u w y)"
-nitpick [card = 1\<emdash>2, expect = none]
+nitpick [card = 1-2, expect = none]
 sorry
 
 lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. \<forall>y. \<exists>z.
        f u v w x y z = f u (g u) w (h u w y) y (k u w y)"
-nitpick [card = 1\<emdash>2, expect = genuine]
+nitpick [card = 1-2, expect = genuine]
 oops
 
 lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. \<forall>y. \<exists>z.
        f u v w x y z = f u (g u w) w (h u w) y (k u w y)"
-nitpick [card = 1\<emdash>2, expect = genuine]
+nitpick [card = 1-2, expect = genuine]
 oops
 
 lemma "\<forall>u\<Colon>'a \<times> 'b. \<exists>v\<Colon>'c. \<forall>w\<Colon>'d. \<exists>x\<Colon>'e \<times> 'f.
        f u v w x = f u (g u) w (h u w)"
-nitpick [card = 1\<emdash>2, expect = none]
+nitpick [card = 1-2, expect = none]
 sorry
 
 lemma "\<forall>u\<Colon>'a \<times> 'b. \<exists>v\<Colon>'c. \<forall>w\<Colon>'d. \<exists>x\<Colon>'e \<times> 'f.
        f u v w x = f u (g u w) w (h u)"
-nitpick [card = 1\<emdash>2, dont_box, expect = genuine]
+nitpick [card = 1-2, dont_box, expect = genuine]
 oops
 
 lemma "\<forall>u\<Colon>'a \<Rightarrow> 'b. \<exists>v\<Colon>'c. \<forall>w\<Colon>'d. \<exists>x\<Colon>'e \<Rightarrow> 'f.
        f u v w x = f u (g u) w (h u w)"
-nitpick [card = 1\<emdash>2, dont_box, expect = none]
+nitpick [card = 1-2, dont_box, expect = none]
 sorry
 
 lemma "\<forall>u\<Colon>'a \<Rightarrow> 'b. \<exists>v\<Colon>'c. \<forall>w\<Colon>'d. \<exists>x\<Colon>'e \<Rightarrow> 'f.
        f u v w x = f u (g u w) w (h u)"
-nitpick [card = 1\<emdash>2, dont_box, expect = genuine]
+nitpick [card = 1-2, dont_box, expect = genuine]
 oops
 
 lemma "\<forall>x. if (\<forall>y. x = y) then False else True"
 nitpick [card = 1, expect = genuine]
-nitpick [card = 2\<emdash>5, expect = none]
+nitpick [card = 2-5, expect = none]
 oops
 
 lemma "\<forall>x\<Colon>'a\<times>'b. if (\<forall>y. x = y) then False else True"
@@ -323,15 +323,15 @@
 oops
 
 lemma "P x \<equiv> P x"
-nitpick [card = 1\<emdash>10, expect = none]
+nitpick [card = 1-10, expect = none]
 by auto
 
 lemma "P x \<equiv> Q x \<Longrightarrow> P x = Q x"
-nitpick [card = 1\<emdash>10, expect = none]
+nitpick [card = 1-10, expect = none]
 by auto
 
 lemma "P x = Q x \<Longrightarrow> P x \<equiv> Q x"
-nitpick [card = 1\<emdash>10, expect = none]
+nitpick [card = 1-10, expect = none]
 by auto
 
 lemma "x \<equiv> (op \<Longrightarrow>) \<Longrightarrow> False"
@@ -343,7 +343,7 @@
 by auto
 
 lemma "P x \<Longrightarrow> P x"
-nitpick [card = 1\<emdash>10, expect = none]
+nitpick [card = 1-10, expect = none]
 by auto
 
 lemma "True \<Longrightarrow> True" "False \<Longrightarrow> True" "False \<Longrightarrow> False"
@@ -594,11 +594,11 @@
 by simp
 
 lemma "I = (\<lambda>x. x) \<Longrightarrow> trancl = (\<lambda>x. trancl (I x))"
-nitpick [card = 1\<emdash>2, expect = none]
+nitpick [card = 1-2, expect = none]
 by auto
 
 lemma "rtrancl = (\<lambda>x. rtrancl x \<union> {(y, y)})"
-nitpick [card = 1\<emdash>3, expect = none]
+nitpick [card = 1-3, expect = none]
 apply (rule ext)
 by auto
 
@@ -607,11 +607,11 @@
 by auto
 
 lemma "((x, x), (x, x)) \<in> rtrancl {}"
-nitpick [card = 1\<emdash>5, expect = none]
+nitpick [card = 1-5, expect = none]
 by auto
 
 lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<union> = (\<lambda>x. op \<union> (I x))"
-nitpick [card = 1\<emdash>5, expect = none]
+nitpick [card = 1-5, expect = none]
 by auto
 
 lemma "a \<in> A \<Longrightarrow> a \<in> (A \<union> B)" "b \<in> B \<Longrightarrow> b \<in> (A \<union> B)"
@@ -619,27 +619,27 @@
 by auto
 
 lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<inter> = (\<lambda>x. op \<inter> (I x))"
-nitpick [card = 1\<emdash>5, expect = none]
+nitpick [card = 1-5, expect = none]
 by auto
 
 lemma "a \<notin> A \<Longrightarrow> a \<notin> (A \<inter> B)" "b \<notin> B \<Longrightarrow> b \<notin> (A \<inter> B)"
-nitpick [card = 1\<emdash>5, expect = none]
+nitpick [card = 1-5, expect = none]
 by auto
 
 lemma "x \<in> ((A\<Colon>'a set) - B) \<longleftrightarrow> x \<in> A \<and> x \<notin> B"
-nitpick [card = 1\<emdash>5, expect = none]
+nitpick [card = 1-5, expect = none]
 by auto
 
 lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<subset> = (\<lambda>x. op \<subset> (I x))"
-nitpick [card = 1\<emdash>5, expect = none]
+nitpick [card = 1-5, expect = none]
 by auto
 
 lemma "A \<subset> B \<Longrightarrow> (\<forall>a \<in> A. a \<in> B) \<and> (\<exists>b \<in> B. b \<notin> A)"
-nitpick [card = 1\<emdash>5, expect = none]
+nitpick [card = 1-5, expect = none]
 by auto
 
 lemma "A \<subseteq> B \<Longrightarrow> \<forall>a \<in> A. a \<in> B"
-nitpick [card = 1\<emdash>5, expect = none]
+nitpick [card = 1-5, expect = none]
 by auto
 
 lemma "A \<subseteq> B \<Longrightarrow> A \<subset> B"
@@ -651,7 +651,7 @@
 by auto
 
 lemma "I = (\<lambda>x\<Colon>'a set. x) \<Longrightarrow> uminus = (\<lambda>x. uminus (I x))"
-nitpick [card = 1\<emdash>7, expect = none]
+nitpick [card = 1-7, expect = none]
 by auto
 
 lemma "A \<union> - A = UNIV"
@@ -685,7 +685,7 @@
 oops
 
 lemma "\<exists>x. x = The"
-nitpick [card = 1\<emdash>3]
+nitpick [card = 1-3]
 by auto
 
 lemma "P x \<and> (\<forall>y. P y \<longrightarrow> y = x) \<longrightarrow> The P = x"
@@ -698,11 +698,11 @@
 
 lemma "P x \<and> P y \<and> x \<noteq> y \<longrightarrow> The P = x \<or> The P = y"
 nitpick [card = 2, expect = none]
-nitpick [card = 3\<emdash>5, expect = genuine]
+nitpick [card = 3-5, expect = genuine]
 oops
 
 lemma "P x \<Longrightarrow> P (The P)"
-nitpick [card = 1\<emdash>2, expect = none]
+nitpick [card = 1-2, expect = none]
 nitpick [card = 8, expect = genuine]
 oops
 
@@ -711,7 +711,7 @@
 oops
 
 lemma "I = (\<lambda>x. x) \<Longrightarrow> The = (\<lambda>x. The (I x))"
-nitpick [card = 1\<emdash>5, expect = none]
+nitpick [card = 1-5, expect = none]
 by auto
 
 lemma "x = Eps"
@@ -719,7 +719,7 @@
 oops
 
 lemma "\<exists>x. x = Eps"
-nitpick [card = 1\<emdash>3, expect = none]
+nitpick [card = 1-3, expect = none]
 by auto
 
 lemma "P x \<and> (\<forall>y. P y \<longrightarrow> y = x) \<longrightarrow> Eps P = x"
@@ -732,7 +732,7 @@
 oops
 
 lemma "P x \<Longrightarrow> P (Eps P)"
-nitpick [card = 1\<emdash>8, expect = none]
+nitpick [card = 1-8, expect = none]
 by (metis exE_some)
 
 lemma "\<forall>x. \<not> P x \<longrightarrow> Eps P = y"
diff -r 6fba7f6c532a -r aed17a173d16 src/HOL/Nitpick_Examples/Datatype_Nits.thy
--- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Mon Mar 03 22:33:22 2014 +0100
+++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Mon Mar 03 23:05:30 2014 +0100
@@ -11,7 +11,7 @@
 imports Main
 begin
 
-nitpick_params [verbose, card = 1\<emdash>8, max_potential = 0,
+nitpick_params [verbose, card = 1-8, max_potential = 0,
                 sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
 
 primrec rot where
@@ -23,7 +23,7 @@
 "rot NibbleF = Nibble0"
 
 lemma "rot n \<noteq> n"
-nitpick [card = 1\<emdash>8,16, verbose, expect = none]
+nitpick [card = 1-8,16, verbose, expect = none]
 sorry
 
 lemma "rot Nibble2 \<noteq> Nibble3"
diff -r 6fba7f6c532a -r aed17a173d16 src/HOL/Nitpick_Examples/Induct_Nits.thy
--- a/src/HOL/Nitpick_Examples/Induct_Nits.thy	Mon Mar 03 22:33:22 2014 +0100
+++ b/src/HOL/Nitpick_Examples/Induct_Nits.thy	Mon Mar 03 23:05:30 2014 +0100
@@ -11,7 +11,7 @@
 imports Main
 begin
 
-nitpick_params [verbose, card = 1\<emdash>8, unary_ints,
+nitpick_params [verbose, card = 1-8, unary_ints,
                 sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
 
 inductive p1 :: "nat \<Rightarrow> bool" where
diff -r 6fba7f6c532a -r aed17a173d16 src/HOL/Nitpick_Examples/Integer_Nits.thy
--- a/src/HOL/Nitpick_Examples/Integer_Nits.thy	Mon Mar 03 22:33:22 2014 +0100
+++ b/src/HOL/Nitpick_Examples/Integer_Nits.thy	Mon Mar 03 23:05:30 2014 +0100
@@ -11,7 +11,7 @@
 imports Main
 begin
 
-nitpick_params [verbose, card = 1\<emdash>5, bits = 1,2,3,4,6,
+nitpick_params [verbose, card = 1-5, bits = 1,2,3,4,6,
                 sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
 
 lemma "Suc x = x + 1"
@@ -187,7 +187,7 @@
 
 lemma "y \<noteq> 0 \<Longrightarrow> x * y div y = (x::int)"
 nitpick [unary_ints, expect = none]
-nitpick [binary_ints, card = 1\<emdash>4, bits = 1\<emdash>4, expect = none]
+nitpick [binary_ints, card = 1-4, bits = 1-4, expect = none]
 sorry
 
 lemma "(x * y < 0) \<longleftrightarrow> (x > 0 \<and> y < 0) \<or> (x < 0 \<and> y > (0::int))"
diff -r 6fba7f6c532a -r aed17a173d16 src/HOL/Nitpick_Examples/Manual_Nits.thy
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Mon Mar 03 22:33:22 2014 +0100
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Mon Mar 03 23:05:30 2014 +0100
@@ -12,9 +12,21 @@
    suite. *)
 
 theory Manual_Nits
-imports Main Real "~~/src/HOL/Library/Quotient_Product"
+imports Real "~~/src/HOL/Library/Quotient_Product"
 begin
 
+declaration {*
+  Nitpick_HOL.register_frac_type @{type_name real}
+   [(@{const_name zero_real_inst.zero_real}, @{const_name Nitpick.zero_frac}),
+    (@{const_name one_real_inst.one_real}, @{const_name Nitpick.one_frac}),
+    (@{const_name plus_real_inst.plus_real}, @{const_name Nitpick.plus_frac}),
+    (@{const_name times_real_inst.times_real}, @{const_name Nitpick.times_frac}),
+    (@{const_name uminus_real_inst.uminus_real}, @{const_name Nitpick.uminus_frac}),
+    (@{const_name inverse_real_inst.inverse_real}, @{const_name Nitpick.inverse_frac}),
+    (@{const_name ord_real_inst.less_real}, @{const_name Nitpick.less_frac}),
+    (@{const_name ord_real_inst.less_eq_real}, @{const_name Nitpick.less_eq_frac})]
+*}
+(*###*)
 
 section {* 2. First Steps *}
 
@@ -47,7 +59,7 @@
 
 lemma "\<exists>!x. x \<in> A \<Longrightarrow> (THE y. y \<in> A) \<in> A"
 nitpick [expect = none]
-nitpick [card 'a = 1\<emdash>50, expect = none]
+nitpick [card 'a = 1-50, expect = none]
 (* sledgehammer *)
 by (metis the_equality)
 
@@ -218,7 +230,7 @@
 
 lemma "\<lbrakk>xs = LCons a xs; ys = LCons a ys\<rbrakk> \<Longrightarrow> xs = ys"
 nitpick [bisim_depth = -1, show_types, expect = quasi_genuine]
-nitpick [card = 1\<emdash>5, expect = none]
+nitpick [card = 1-5, expect = none]
 sorry
 
 
@@ -255,7 +267,7 @@
 "subst\<^sub>2 \<sigma> (App t u) = App (subst\<^sub>2 \<sigma> t) (subst\<^sub>2 \<sigma> u)"
 
 lemma "\<not> loose t 0 \<Longrightarrow> subst\<^sub>2 \<sigma> t = t"
-nitpick [card = 1\<emdash>5, expect = none]
+nitpick [card = 1-5, expect = none]
 sorry
 
 
@@ -282,7 +294,7 @@
 (* nitpick *)
 apply (induct set: reach)
   apply auto
- nitpick [card = 1\<emdash>4, bits = 1\<emdash>4, expect = none]
+ nitpick [card = 1-4, bits = 1-4, expect = none]
  apply (thin_tac "n \<in> reach")
  nitpick [expect = genuine]
 oops
@@ -291,7 +303,7 @@
 (* nitpick *)
 apply (induct set: reach)
   apply auto
- nitpick [card = 1\<emdash>4, bits = 1\<emdash>4, expect = none]
+ nitpick [card = 1-4, bits = 1-4, expect = none]
  apply (thin_tac "n \<in> reach")
  nitpick [expect = genuine]
 oops
@@ -345,7 +357,7 @@
 
 theorem S\<^sub>3_sound:
 "w \<in> S\<^sub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
-nitpick [card = 1\<emdash>5, expect = none]
+nitpick [card = 1-5, expect = none]
 sorry
 
 theorem S\<^sub>3_complete:
@@ -364,19 +376,19 @@
 
 theorem S\<^sub>4_sound:
 "w \<in> S\<^sub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
-nitpick [card = 1\<emdash>5, expect = none]
+nitpick [card = 1-5, expect = none]
 sorry
 
 theorem S\<^sub>4_complete:
 "length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^sub>4"
-nitpick [card = 1\<emdash>5, expect = none]
+nitpick [card = 1-5, expect = none]
 sorry
 
 theorem S\<^sub>4_A\<^sub>4_B\<^sub>4_sound_and_complete:
 "w \<in> S\<^sub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
 "w \<in> A\<^sub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] + 1"
 "w \<in> B\<^sub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = b] = length [x \<leftarrow> w. x = a] + 1"
-nitpick [card = 1\<emdash>5, expect = none]
+nitpick [card = 1-5, expect = none]
 sorry
 
 
@@ -431,13 +443,13 @@
 theorem dataset_skew_split:
 "dataset (skew t) = dataset t"
 "dataset (split t) = dataset t"
-nitpick [card = 1\<emdash>5, expect = none]
+nitpick [card = 1-5, expect = none]
 sorry
 
 theorem wf_skew_split:
 "wf t \<Longrightarrow> skew t = t"
 "wf t \<Longrightarrow> split t = t"
-nitpick [card = 1\<emdash>5, expect = none]
+nitpick [card = 1-5, expect = none]
 sorry
 
 primrec insort\<^sub>1 where
@@ -461,11 +473,11 @@
                        (if x > y then insort\<^sub>2 u x else u))"
 
 theorem wf_insort\<^sub>2: "wf t \<Longrightarrow> wf (insort\<^sub>2 t x)"
-nitpick [card = 1\<emdash>5, expect = none]
+nitpick [card = 1-5, expect = none]
 sorry
 
 theorem dataset_insort\<^sub>2: "dataset (insort\<^sub>2 t x) = {x} \<union> dataset t"
-nitpick [card = 1\<emdash>5, expect = none]
+nitpick [card = 1-5, expect = none]
 sorry
 
 end
diff -r 6fba7f6c532a -r aed17a173d16 src/HOL/Nitpick_Examples/Record_Nits.thy
--- a/src/HOL/Nitpick_Examples/Record_Nits.thy	Mon Mar 03 22:33:22 2014 +0100
+++ b/src/HOL/Nitpick_Examples/Record_Nits.thy	Mon Mar 03 23:05:30 2014 +0100
@@ -11,7 +11,7 @@
 imports Main
 begin
 
-nitpick_params [verbose, card = 1\<emdash>6, max_potential = 0,
+nitpick_params [verbose, card = 1-6, max_potential = 0,
                 sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
 
 record point2d =
diff -r 6fba7f6c532a -r aed17a173d16 src/HOL/Nitpick_Examples/Refute_Nits.thy
--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy	Mon Mar 03 22:33:22 2014 +0100
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy	Mon Mar 03 23:05:30 2014 +0100
@@ -11,7 +11,7 @@
 imports Main
 begin
 
-nitpick_params [verbose, card = 1\<emdash>6, max_potential = 0,
+nitpick_params [verbose, card = 1-6, max_potential = 0,
                 sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
 
 lemma "P \<and> Q"
@@ -283,7 +283,7 @@
 text {* ``Every point is a fixed point of some function.'' *}
 
 lemma "\<exists>f. f x = x"
-nitpick [card = 1\<emdash>7, expect = none]
+nitpick [card = 1-7, expect = none]
 apply (rule_tac x = "\<lambda>x. x" in exI)
 apply simp
 done
@@ -700,7 +700,7 @@
 oops
 
 lemma "rec_T3 e (E x) = e x"
-nitpick [card = 1\<emdash>4, expect = none]
+nitpick [card = 1-4, expect = none]
 apply simp
 done
 
@@ -729,7 +729,7 @@
 oops
 
 lemma "P Suc"
-nitpick [card = 1\<emdash>7, expect = none]
+nitpick [card = 1-7, expect = none]
 oops
 
 lemma "rec_nat zero suc 0 = zero"
@@ -765,12 +765,12 @@
 oops
 
 lemma "rec_list nil cons [] = nil"
-nitpick [card = 1\<emdash>5, expect = none]
+nitpick [card = 1-5, expect = none]
 apply simp
 done
 
 lemma "rec_list nil cons (x#xs) = cons x xs (rec_list nil cons xs)"
-nitpick [card = 1\<emdash>5, expect = none]
+nitpick [card = 1-5, expect = none]
 apply simp
 done
 
@@ -843,7 +843,7 @@
 done
 
 lemma "rec_BinTree l n (Node x y) = n x y (rec_BinTree l n x) (rec_BinTree l n y)"
-nitpick [card = 1\<emdash>5, expect = none]
+nitpick [card = 1-5, expect = none]
 apply simp
 done
 
@@ -881,12 +881,12 @@
 oops
 
 lemma "rec_aexp_bexp_1 number ite equal (Number x) = number x"
-nitpick [card = 1\<emdash>3, expect = none]
+nitpick [card = 1-3, expect = none]
 apply simp
 done
 
 lemma "rec_aexp_bexp_1 number ite equal (ITE x y z) = ite x y z (rec_aexp_bexp_2 number ite equal x) (rec_aexp_bexp_1 number ite equal y) (rec_aexp_bexp_1 number ite equal z)"
-nitpick [card = 1\<emdash>3, expect = none]
+nitpick [card = 1-3, expect = none]
 apply simp
 done
 
@@ -899,7 +899,7 @@
 oops
 
 lemma "rec_aexp_bexp_2 number ite equal (Equal x y) = equal x y (rec_aexp_bexp_1 number ite equal x) (rec_aexp_bexp_1 number ite equal y)"
-nitpick [card = 1\<emdash>3, expect = none]
+nitpick [card = 1-3, expect = none]
 apply simp
 done
 
@@ -959,32 +959,32 @@
 oops
 
 lemma "rec_X_Y_1 a b c d e f A = a"
-nitpick [card = 1\<emdash>5, expect = none]
+nitpick [card = 1-5, expect = none]
 apply simp
 done
 
 lemma "rec_X_Y_1 a b c d e f (B x) = b x (rec_X_Y_1 a b c d e f x)"
-nitpick [card = 1\<emdash>5, expect = none]
+nitpick [card = 1-5, expect = none]
 apply simp
 done
 
 lemma "rec_X_Y_1 a b c d e f (C y) = c y (rec_X_Y_2 a b c d e f y)"
-nitpick [card = 1\<emdash>5, expect = none]
+nitpick [card = 1-5, expect = none]
 apply simp
 done
 
 lemma "rec_X_Y_2 a b c d e f (D x) = d x (rec_X_Y_1 a b c d e f x)"
-nitpick [card = 1\<emdash>5, expect = none]
+nitpick [card = 1-5, expect = none]
 apply simp
 done
 
 lemma "rec_X_Y_2 a b c d e f (E y) = e y (rec_X_Y_2 a b c d e f y)"
-nitpick [card = 1\<emdash>5, expect = none]
+nitpick [card = 1-5, expect = none]
 apply simp
 done
 
 lemma "rec_X_Y_2 a b c d e f F = f"
-nitpick [card = 1\<emdash>5, expect = none]
+nitpick [card = 1-5, expect = none]
 apply simp
 done
 
@@ -1015,32 +1015,32 @@
 oops
 
 lemma "rec_XOpt_1 cx dx n1 s1 n2 s2 (CX x) = cx x (rec_XOpt_2 cx dx n1 s1 n2 s2 x)"
-nitpick [card = 1\<emdash>5, expect = none]
+nitpick [card = 1-5, expect = none]
 apply simp
 done
 
 lemma "rec_XOpt_1 cx dx n1 s1 n2 s2 (DX x) = dx x (\<lambda>b. rec_XOpt_3 cx dx n1 s1 n2 s2 (x b))"
-nitpick [card = 1\<emdash>3, expect = none]
+nitpick [card = 1-3, expect = none]
 apply simp
 done
 
 lemma "rec_XOpt_2 cx dx n1 s1 n2 s2 None = n1"
-nitpick [card = 1\<emdash>4, expect = none]
+nitpick [card = 1-4, expect = none]
 apply simp
 done
 
 lemma "rec_XOpt_2 cx dx n1 s1 n2 s2 (Some x) = s1 x (rec_XOpt_1 cx dx n1 s1 n2 s2 x)"
-nitpick [card = 1\<emdash>4, expect = none]
+nitpick [card = 1-4, expect = none]
 apply simp
 done
 
 lemma "rec_XOpt_3 cx dx n1 s1 n2 s2 None = n2"
-nitpick [card = 1\<emdash>4, expect = none]
+nitpick [card = 1-4, expect = none]
 apply simp
 done
 
 lemma "rec_XOpt_3 cx dx n1 s1 n2 s2 (Some x) = s2 x (rec_XOpt_1 cx dx n1 s1 n2 s2 x)"
-nitpick [card = 1\<emdash>4, expect = none]
+nitpick [card = 1-4, expect = none]
 apply simp
 done
 
@@ -1071,17 +1071,17 @@
 oops
 
 lemma "rec_YOpt_1 cy n s (CY x) = cy x (rec_YOpt_2 cy n s x)"
-nitpick [card = 1\<emdash>2, expect = none]
+nitpick [card = 1-2, expect = none]
 apply simp
 done
 
 lemma "rec_YOpt_2 cy n s None = n"
-nitpick [card = 1\<emdash>2, expect = none]
+nitpick [card = 1-2, expect = none]
 apply simp
 done
 
 lemma "rec_YOpt_2 cy n s (Some x) = s x (\<lambda>a. rec_YOpt_1 cy n s (x a))"
-nitpick [card = 1\<emdash>2, expect = none]
+nitpick [card = 1-2, expect = none]
 apply simp
 done
 
@@ -1108,17 +1108,17 @@
 oops
 
 lemma "rec_Trie_1 tr nil cons (TR x) = tr x (rec_Trie_2 tr nil cons x)"
-nitpick [card = 1\<emdash>4, expect = none]
+nitpick [card = 1-4, expect = none]
 apply simp
 done
 
 lemma "rec_Trie_2 tr nil cons [] = nil"
-nitpick [card = 1\<emdash>4, expect = none]
+nitpick [card = 1-4, expect = none]
 apply simp
 done
 
 lemma "rec_Trie_2 tr nil cons (x#xs) = cons x xs (rec_Trie_1 tr nil cons x) (rec_Trie_2 tr nil cons xs)"
-nitpick [card = 1\<emdash>4, expect = none]
+nitpick [card = 1-4, expect = none]
 apply simp
 done
 
@@ -1145,12 +1145,12 @@
 oops
 
 lemma "rec_InfTree leaf node Leaf = leaf"
-nitpick [card = 1\<emdash>3, expect = none]
+nitpick [card = 1-3, expect = none]
 apply simp
 done
 
 lemma "rec_InfTree leaf node (Node x) = node x (\<lambda>n. rec_InfTree leaf node (x n))"
-nitpick [card = 1\<emdash>3, expect = none]
+nitpick [card = 1-3, expect = none]
 apply simp
 done
 
@@ -1169,22 +1169,22 @@
 oops
 
 lemma "P (Lam (\<lambda>a. Var a))"
-nitpick [card = 1\<emdash>5, expect = none]
+nitpick [card = 1-5, expect = none]
 nitpick [card 'a = 4, card "'a lambda" = 5, expect = genuine]
 oops
 
 lemma "rec_lambda var app lam (Var x) = var x"
-nitpick [card = 1\<emdash>3, expect = none]
+nitpick [card = 1-3, expect = none]
 apply simp
 done
 
 lemma "rec_lambda var app lam (App x y) = app x y (rec_lambda var app lam x) (rec_lambda var app lam y)"
-nitpick [card = 1\<emdash>3, expect = none]
+nitpick [card = 1-3, expect = none]
 apply simp
 done
 
 lemma "rec_lambda var app lam (Lam x) = lam x (\<lambda>a. rec_lambda var app lam (x a))"
-nitpick [card = 1\<emdash>3, expect = none]
+nitpick [card = 1-3, expect = none]
 apply simp
 done
 
@@ -1210,27 +1210,27 @@
 oops
 
 lemma "rec_U_1 e c d nil cons (E x) = e x (rec_U_2 e c d nil cons x)"
-nitpick [card = 1\<emdash>3, expect = none]
+nitpick [card = 1-3, expect = none]
 apply simp
 done
 
 lemma "rec_U_2 e c d nil cons (C x) = c x"
-nitpick [card = 1\<emdash>3, expect = none]
+nitpick [card = 1-3, expect = none]
 apply simp
 done
 
 lemma "rec_U_2 e c d nil cons (D x) = d x (rec_U_3 e c d nil cons x)"
-nitpick [card = 1\<emdash>3, expect = none]
+nitpick [card = 1-3, expect = none]
 apply simp
 done
 
 lemma "rec_U_3 e c d nil cons [] = nil"
-nitpick [card = 1\<emdash>3, expect = none]
+nitpick [card = 1-3, expect = none]
 apply simp
 done
 
 lemma "rec_U_3 e c d nil cons (x#xs) = cons x xs (rec_U_1 e c d nil cons x) (rec_U_3 e c d nil cons xs)"
-nitpick [card = 1\<emdash>3, expect = none]
+nitpick [card = 1-3, expect = none]
 apply simp
 done
 
diff -r 6fba7f6c532a -r aed17a173d16 src/HOL/Nitpick_Examples/Typedef_Nits.thy
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Mon Mar 03 22:33:22 2014 +0100
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Mon Mar 03 23:05:30 2014 +0100
@@ -11,7 +11,7 @@
 imports Complex_Main
 begin
 
-nitpick_params [verbose, card = 1\<emdash>4, sat_solver = MiniSat_JNI, max_threads = 1,
+nitpick_params [verbose, card = 1-4, sat_solver = MiniSat_JNI, max_threads = 1,
                 timeout = 240]
 
 definition "three = {0\<Colon>nat, 1, 2}"
@@ -73,7 +73,7 @@
 sorry
 
 lemma "x \<noteq> (y\<Colon>(bool \<times> bool) bounded) \<Longrightarrow> z = x \<or> z = y"
-nitpick [card = 1\<emdash>5, expect = genuine]
+nitpick [card = 1-5, expect = genuine]
 oops
 
 lemma "True \<equiv> ((\<lambda>x\<Colon>bool. x) = (\<lambda>x. x))"
@@ -101,11 +101,11 @@
 oops
 
 lemma "Pair a b = Abs_prod (Pair_Rep a b)"
-nitpick [card = 1\<emdash>2, expect = none]
+nitpick [card = 1-2, expect = none]
 by (rule Pair_def)
 
 lemma "Pair a b = Abs_prod (Pair_Rep b a)"
-nitpick [card = 1\<emdash>2, expect = none]
+nitpick [card = 1-2, expect = none]
 nitpick [dont_box, expect = genuine]
 oops
 
@@ -114,7 +114,7 @@
 by (simp add: Pair_def [THEN sym])
 
 lemma "fst (Abs_prod (Pair_Rep a b)) = b"
-nitpick [card = 1\<emdash>2, expect = none]
+nitpick [card = 1-2, expect = none]
 nitpick [dont_box, expect = genuine]
 oops
 
@@ -164,7 +164,7 @@
 by (rule Rep_Nat_inverse)
 
 lemma "Abs_list (Rep_list a) = a"
-(* nitpick [card = 1\<emdash>2, expect = none] FIXME *)
+(* nitpick [card = 1-2, expect = none] FIXME *)
 by (rule Rep_list_inverse)
 
 record point =
@@ -186,11 +186,11 @@
 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]
+nitpick [card = 1-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]
+nitpick [card = 1-3, expect = genuine]
 oops
 
 end
diff -r 6fba7f6c532a -r aed17a173d16 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Mar 03 22:33:22 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Mar 03 23:05:30 2014 +0100
@@ -160,10 +160,8 @@
   val unregister_codatatype :
     typ -> morphism -> Context.generic -> Context.generic
   val unregister_codatatype_global : typ -> theory -> theory
-  val data_type_constrs : hol_context -> typ -> (string * typ) list
   val binarized_and_boxed_data_type_constrs :
     hol_context -> bool -> typ -> (string * typ) list
-  val num_data_type_constrs : hol_context -> typ -> int
   val constr_name_for_sel_like : string -> string
   val binarized_and_boxed_constr_for_sel : hol_context -> bool ->
     string * typ -> string * typ
@@ -991,41 +989,42 @@
 fun suc_const T = Const (@{const_name Suc}, T --> T)
 
 fun uncached_data_type_constrs ({thy, ctxt, ...} : hol_context)
-                               (T as Type (s, Ts)) =
-    (case AList.lookup (op =) (#codatatypes (Data.get (Context.Proof ctxt)))
-                       s of
-       SOME (_, xs' as (_ :: _)) => map (apsnd (repair_constr_type T)) xs'
-     | _ =>
-       if is_frac_type ctxt T then
-         case typedef_info ctxt s of
-           SOME {abs_type, rep_type, Abs_name, ...} =>
-           [(Abs_name,
-             varify_and_instantiate_type ctxt abs_type T rep_type --> T)]
-         | NONE => [] (* impossible *)
-       else if is_data_type ctxt T then
-         case Ctr_Sugar.ctr_sugar_of ctxt s of
-           SOME {ctrs, ...} =>
-           map (apsnd (repair_constr_type T) o dest_Const) ctrs
-         | NONE =>
-           if is_record_type T then
-             let
-               val s' = unsuffix Record.ext_typeN s ^ Record.extN
-               val T' = (Record.get_extT_fields thy T
-                        |> apsnd single |> uncurry append |> map snd) ---> T
-             in [(s', T')] end
-           else if is_raw_quot_type ctxt T then
-             [(@{const_name Quot}, rep_type_for_quot_type ctxt T --> T)]
-           else case typedef_info ctxt s of
+                               (T as Type (s, _)) =
+    if is_interpreted_type s then
+      []
+    else
+      (case AList.lookup (op =) (#codatatypes (Data.get (Context.Proof ctxt)))
+                         s of
+         SOME (_, xs' as (_ :: _)) => map (apsnd (repair_constr_type T)) xs'
+       | _ =>
+         if is_frac_type ctxt T then
+           case typedef_info ctxt s of
              SOME {abs_type, rep_type, Abs_name, ...} =>
              [(Abs_name,
                varify_and_instantiate_type ctxt abs_type T rep_type --> T)]
+           | NONE => [] (* impossible *)
+         else
+           case Ctr_Sugar.ctr_sugar_of ctxt s of
+             SOME {ctrs, ...} =>
+             map (apsnd (repair_constr_type T) o dest_Const) ctrs
            | NONE =>
-             if T = @{typ ind} then
-               [dest_Const @{const Zero_Rep}, dest_Const @{const Suc_Rep}]
-             else
-               []
-       else
-         [])
+             if is_record_type T then
+               let
+                 val s' = unsuffix Record.ext_typeN s ^ Record.extN
+                 val T' = (Record.get_extT_fields thy T
+                          |> apsnd single |> uncurry append |> map snd) ---> T
+               in [(s', T')] end
+             else if is_raw_quot_type ctxt T then
+               [(@{const_name Quot}, rep_type_for_quot_type ctxt T --> T)]
+             else case typedef_info ctxt s of
+               SOME {abs_type, rep_type, Abs_name, ...} =>
+               [(Abs_name,
+                 varify_and_instantiate_type ctxt abs_type T rep_type --> T)]
+             | NONE =>
+               if T = @{typ ind} then
+                 [dest_Const @{const Zero_Rep}, dest_Const @{const Suc_Rep}]
+               else
+                 [])
   | uncached_data_type_constrs _ _ = []
 
 fun data_type_constrs (hol_ctxt as {constr_cache, ...}) T =
@@ -1039,7 +1038,6 @@
 fun binarized_and_boxed_data_type_constrs hol_ctxt binarize =
   map (apsnd ((binarize ? binarize_nat_and_int_in_type)
               o box_type hol_ctxt InConstr)) o data_type_constrs hol_ctxt
-val num_data_type_constrs = length oo data_type_constrs
 
 fun constr_name_for_sel_like @{const_name fst} = @{const_name Pair}
   | constr_name_for_sel_like @{const_name snd} = @{const_name Pair}
@@ -1222,7 +1220,7 @@
     if s = @{const_name Suc} then
       Abs (Name.uu, dataT,
            @{const Not} $ HOLogic.mk_eq (zero_const dataT, Bound 0))
-    else if num_data_type_constrs hol_ctxt dataT >= 2 then
+    else if length (data_type_constrs hol_ctxt dataT) >= 2 then
       Const (discr_for_constr x)
     else
       Abs (Name.uu, dataT, @{const True})
@@ -1505,8 +1503,12 @@
                | t => t)
 
 fun case_const_names ctxt =
-  map_filter (fn {casex, ...} => SOME (apsnd (fn T => num_binder_types T - 1) (dest_Const casex)))
-      (Ctr_Sugar.ctr_sugars_of ctxt) @
+  map_filter (fn {casex = Const (s, T), ...} =>
+      let val Ts = binder_types T in
+        if is_data_type ctxt (List.last Ts) then SOME (s, length Ts - 1)
+        else NONE
+      end)
+    (Ctr_Sugar.ctr_sugars_of ctxt) @
   map (apsnd length o snd) (#codatatypes (Data.get (Context.Proof ctxt)))
 
 fun fixpoint_kind_of_const thy table x =