author blanchet Wed, 15 Aug 2012 11:04:56 +0200 changeset 48812 9509fc5485b2 parent 48811 d1688612668d child 48813 b0c39fd53c0e child 48817 01d1734f779d child 48819 6cf7a9d8bbaf
fixed handling of "int" in the wake of its port to the quotient package
```--- a/src/HOL/Nitpick_Examples/Integer_Nits.thy	Wed Aug 15 11:04:55 2012 +0200
+++ b/src/HOL/Nitpick_Examples/Integer_Nits.thy	Wed Aug 15 11:04:56 2012 +0200
@@ -1,6 +1,6 @@
(*  Title:      HOL/Nitpick_Examples/Integer_Nits.thy
Author:     Jasmin Blanchette, TU Muenchen

Examples featuring Nitpick applied to natural numbers and integers.
*)
@@ -95,9 +95,6 @@
nitpick [binary_ints, bits = 9, expect = genuine]
oops

-(* FIXME
-*** Invalid intermediate term ("Nitpick_Nut.the_name"): (ConstName Nitpick.sel0\$Nitpick.Quot int \<Rightarrow> nat X).
-
lemma "nat (of_nat n) = n"
nitpick [unary_ints, expect = none]
nitpick [binary_ints, expect = none]
@@ -208,7 +205,6 @@
nitpick [unary_ints, expect = none]
nitpick [binary_ints, expect = none]
sorry
-*)

datatype tree = Null | Node nat tree tree

@@ -218,7 +214,6 @@

lemma "labels (Node x t u) \<noteq> labels (Node y v w)"
nitpick [expect = potential] (* unfortunate *)
-nitpick [dont_finitize, expect = potential]
oops

lemma "labels (Node x t u) \<noteq> {}"
@@ -227,22 +222,18 @@

lemma "card (labels t) > 0"
nitpick [expect = potential] (* unfortunate *)
-nitpick [dont_finitize, expect = potential]
oops

lemma "(\<Sum>n \<in> labels t. n + 2) \<ge> 2"
nitpick [expect = potential] (* unfortunate *)
-nitpick [dont_finitize, expect = potential]
oops

lemma "t \<noteq> Null \<Longrightarrow> (\<Sum>n \<in> labels t. n + 2) \<ge> 2"
nitpick [expect = potential] (* unfortunate *)
-nitpick [dont_finitize, expect = potential]
sorry

lemma "(\<Sum>i \<in> labels (Node x t u). f i\<Colon>nat) = f x + (\<Sum>i \<in> labels t. f i) + (\<Sum>i \<in> labels u. f i)"
nitpick [expect = potential] (* unfortunate *)
-nitpick [dont_finitize, expect = potential]
oops

end```
```--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Wed Aug 15 11:04:55 2012 +0200
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Wed Aug 15 11:04:56 2012 +0200
@@ -64,10 +64,8 @@
subsection {* 2.5. Natural Numbers and Integers *}

lemma "\<lbrakk>i \<le> j; n \<le> (m\<Colon>int)\<rbrakk> \<Longrightarrow> i * n + j * m \<le> i * m + j * n"
-(* FIXME
nitpick [expect = genuine]
nitpick [binary_ints, bits = 16, expect = genuine]
-*)
oops

lemma "\<forall>n. Suc n \<noteq> n \<Longrightarrow> P"
@@ -143,15 +141,11 @@
Ycoord :: int

lemma "Xcoord (p\<Colon>point) = Xcoord (q\<Colon>point)"
-(* FIXME: Invalid intermediate term
nitpick [show_datatypes, expect = genuine]
-*)
oops

lemma "4 * x + 3 * (y\<Colon>real) \<noteq> 1 / 2"
-(* FIXME: Invalid intermediate term
nitpick [show_datatypes, expect = genuine]
-*)
oops

subsection {* 2.8. Inductive and Coinductive Predicates *}```
```--- a/src/HOL/Nitpick_Examples/Record_Nits.thy	Wed Aug 15 11:04:55 2012 +0200
+++ b/src/HOL/Nitpick_Examples/Record_Nits.thy	Wed Aug 15 11:04:56 2012 +0200
@@ -18,7 +18,6 @@
xc :: int
yc :: int

-(* FIXME: Invalid intermediate term
lemma "\<lparr>xc = x, yc = y\<rparr> = p\<lparr>xc := x, yc := y\<rparr>"
nitpick [expect = none]
sorry
@@ -84,6 +83,5 @@
lemma "p\<lparr>xc := x, yc := y, zc := z, wc := w\<rparr> = p"
nitpick [expect = genuine]
oops
-*)

end```
```--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Wed Aug 15 11:04:55 2012 +0200
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Wed Aug 15 11:04:56 2012 +0200
@@ -171,7 +171,6 @@
Xcoord :: int
Ycoord :: int

-(* FIXME: Invalid intermediate term
lemma "Abs_point_ext (Rep_point_ext a) = a"
nitpick [expect = none]
by (fact Rep_point_ext_inverse)
@@ -183,6 +182,5 @@
lemma "Abs_rat (Rep_rat a) = a"
nitpick [card = 1, expect = none]
by (rule Rep_rat_inverse)
-*)

end```
```--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Aug 15 11:04:55 2012 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Aug 15 11:04:56 2012 +0200
@@ -670,7 +670,8 @@
is_some (Quotient_Info.lookup_quotients ctxt s)
| is_real_quot_type _ _ = false
fun is_quot_type ctxt T =
-  is_real_quot_type ctxt T andalso not (is_registered_type ctxt T)
+  is_real_quot_type ctxt T andalso not (is_registered_type ctxt T) andalso
+  T <> @{typ int}
fun is_pure_typedef ctxt (T as Type (s, _)) =
let val thy = Proof_Context.theory_of ctxt in
is_frac_type ctxt T orelse```