# HG changeset patch
# User blanchet
# Date 1345021496 -7200
# Node ID 9509fc5485b2538a4f8557ce173fc69be33bf79a
# Parent  d1688612668dac815292af59ac74a7a857ceee71
fixed handling of "int" in the wake of its port to the quotient package

diff -r d1688612668d -r 9509fc5485b2 src/HOL/Nitpick_Examples/Integer_Nits.thy
--- 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
-    Copyright   2009-2011
+    Copyright   2009-2012
 
 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
diff -r d1688612668d -r 9509fc5485b2 src/HOL/Nitpick_Examples/Manual_Nits.thy
--- 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 *}
diff -r d1688612668d -r 9509fc5485b2 src/HOL/Nitpick_Examples/Record_Nits.thy
--- 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
diff -r d1688612668d -r 9509fc5485b2 src/HOL/Nitpick_Examples/Typedef_Nits.thy
--- 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
diff -r d1688612668d -r 9509fc5485b2 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- 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