--- 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"
--- 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"
--- 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
--- 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))"
--- 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
--- 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 =
--- 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
--- 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
--- 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 =