# HG changeset patch
# User bulwahn
# Date 1321367930 -3600
# Node ID 6975db7fd6f0f2ab056c5a661072cf92d24fa53e
# Parent  4cc83e901acf35ea5f9f587b2596f40b1df42dcf
improved generators for rational numbers to generate negative numbers;
added examples

diff -r 4cc83e901acf -r 6975db7fd6f0 src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Tue Nov 15 15:38:49 2011 +0100
+++ b/src/HOL/Rat.thy	Tue Nov 15 15:38:50 2011 +0100
@@ -1154,7 +1154,7 @@
 begin
 
 definition
-  "exhaustive f d = exhaustive (%k. exhaustive (%l. f (Fract (Code_Numeral.int_of k) (Code_Numeral.int_of l))) d) d"
+  "exhaustive f d = exhaustive (%l. exhaustive (%k. f (Fract k (Code_Numeral.int_of l + 1))) d) d"
 
 instance ..
 
@@ -1164,8 +1164,9 @@
 begin
 
 definition
-  "full_exhaustive f d = full_exhaustive (%(k, kt). full_exhaustive (%(l, lt).
-     f (valterm_fract (Code_Numeral.int_of k, %_. Code_Evaluation.term_of (Code_Numeral.int_of k)) (Code_Numeral.int_of l, %_. Code_Evaluation.term_of (Code_Numeral.int_of l)))) d) d"
+  "full_exhaustive f d = full_exhaustive (%(l, _). full_exhaustive (%k.
+     f (let j = Code_Numeral.int_of l + 1
+        in valterm_fract k (j, %_. Code_Evaluation.term_of j))) d) d"
 
 instance ..
 
@@ -1181,16 +1182,17 @@
 lemma [code]:
   "partial_term_of (ty :: rat itself) (Quickcheck_Narrowing.Var p tt) == Code_Evaluation.Free (STR ''_'') (Typerep.Typerep (STR ''Rat.rat'') [])"
   "partial_term_of (ty :: rat itself) (Quickcheck_Narrowing.Ctr 0 [l, k]) ==
-     Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.Const (STR ''Rat.Fract'')
-     (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''Int.int'') [], Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''Int.int'') [],
-        Typerep.Typerep (STR ''Rat.rat'') []]])) (partial_term_of (TYPE(int)) l)) (partial_term_of (TYPE(int)) k)" 
+     Code_Evaluation.App (Code_Evaluation.Const (STR ''Rat.Frct'')
+     (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''Product_Type.prod'') [Typerep.Typerep (STR ''Int.int'') [], Typerep.Typerep (STR ''Int.int'') []],
+        Typerep.Typerep (STR ''Rat.rat'') []])) (Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.Const (STR ''Product_Type.Pair'') (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''Int.int'') [], Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''Int.int'') [], Typerep.Typerep (STR ''Product_Type.prod'') [Typerep.Typerep (STR ''Int.int'') [], Typerep.Typerep (STR ''Int.int'') []]]])) (partial_term_of (TYPE(int)) l)) (partial_term_of (TYPE(int)) k))"
 by (rule partial_term_of_anything)+
 
 instantiation rat :: narrowing
 begin
 
 definition
-  "narrowing = Quickcheck_Narrowing.apply (Quickcheck_Narrowing.apply (Quickcheck_Narrowing.cons Fract) narrowing) narrowing"
+  "narrowing = Quickcheck_Narrowing.apply (Quickcheck_Narrowing.apply
+    (Quickcheck_Narrowing.cons (%nom denom. Fract nom denom)) narrowing) narrowing"
 
 instance ..
 
diff -r 4cc83e901acf -r 6975db7fd6f0 src/HOL/ex/Quickcheck_Examples.thy
--- a/src/HOL/ex/Quickcheck_Examples.thy	Tue Nov 15 15:38:49 2011 +0100
+++ b/src/HOL/ex/Quickcheck_Examples.thy	Tue Nov 15 15:38:50 2011 +0100
@@ -304,12 +304,22 @@
 quickcheck[random, size = 10]
 oops
 
+lemma "(x :: rat) >= 0"
+quickcheck[random, expect = counterexample]
+quickcheck[exhaustive, expect = counterexample]
+oops
+
 lemma
   "(x :: real) > 0 ==> y > 0 ==> z > 0 ==> x * x + y * y \<noteq> z * z"
 quickcheck[exhaustive, size = 10, expect = counterexample]
 quickcheck[random, size = 10]
 oops
 
+lemma "(x :: real) >= 0"
+quickcheck[random, expect = counterexample]
+quickcheck[exhaustive, expect = counterexample]
+oops
+
 subsubsection {* floor and ceiling functions *}
 
 lemma