# HG changeset patch
# User bulwahn
# Date 1291977725 -3600
# Node ID a76ee71c3313b798b39d75fcae27933a3550b8b7
# Parent  013adf7ebd964c5f0712a89736e69084d5519f3e
adding check_all instances for a few more finite types in smallcheck

diff -r 013adf7ebd96 -r a76ee71c3313 src/HOL/Smallcheck.thy
--- a/src/HOL/Smallcheck.thy	Fri Dec 10 11:42:04 2010 +0100
+++ b/src/HOL/Smallcheck.thy	Fri Dec 10 11:42:05 2010 +0100
@@ -7,6 +7,11 @@
 uses ("Tools/smallvalue_generators.ML")
 begin
 
+subsection {* basic operations for generators *}
+
+definition orelse :: "'a option => 'a option => 'a option" (infixr "orelse" 55)
+where
+  [code_unfold]: "x orelse y = (case x of Some x' => Some x' | None => y)"
 
 subsection {* small value generator type classes *}
 
@@ -151,6 +156,18 @@
 
 end
 
+
+instantiation unit :: check_all
+begin
+
+definition
+  "check_all f = f (Code_Evaluation.valtermify ())"
+
+instance ..
+
+end
+
+
 instantiation bool :: check_all
 begin
 
@@ -161,6 +178,7 @@
 
 end
 
+
 instantiation prod :: (check_all, check_all) check_all
 begin
 
@@ -171,6 +189,67 @@
 
 end
 
+
+instantiation sum :: (check_all, check_all) check_all
+begin
+
+definition
+  "check_all f = (case check_all (%(a, t). f (Inl a, %_. Code_Evaluation.App (Code_Evaluation.term_of (Inl :: 'a => 'a + 'b)) (t ()))) of Some x' => Some x'
+             | None => check_all (%(b, t). f (Inr b, %_. Code_Evaluation.App (Code_Evaluation.term_of (Inr :: 'b => 'a + 'b)) (t ()))))"
+
+instance ..
+
+end
+
+instantiation nibble :: check_all
+begin
+
+definition
+  "check_all f =
+    f (Code_Evaluation.valtermify Nibble0) orelse
+    f (Code_Evaluation.valtermify Nibble1) orelse
+    f (Code_Evaluation.valtermify Nibble2) orelse
+    f (Code_Evaluation.valtermify Nibble3) orelse
+    f (Code_Evaluation.valtermify Nibble4) orelse
+    f (Code_Evaluation.valtermify Nibble5) orelse
+    f (Code_Evaluation.valtermify Nibble6) orelse
+    f (Code_Evaluation.valtermify Nibble7) orelse
+    f (Code_Evaluation.valtermify Nibble8) orelse
+    f (Code_Evaluation.valtermify Nibble9) orelse
+    f (Code_Evaluation.valtermify NibbleA) orelse
+    f (Code_Evaluation.valtermify NibbleB) orelse
+    f (Code_Evaluation.valtermify NibbleC) orelse
+    f (Code_Evaluation.valtermify NibbleD) orelse
+    f (Code_Evaluation.valtermify NibbleE) orelse
+    f (Code_Evaluation.valtermify NibbleF)"
+
+instance ..
+
+end
+
+
+instantiation char :: check_all
+begin
+
+definition
+  "check_all f = check_all (%(x, t1). check_all (%(y, t2). f (Char x y, %_. Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.term_of Char) (t1 ())) (t2 ()))))"
+
+instance ..
+
+end
+
+
+instantiation option :: (check_all) check_all
+begin
+
+definition
+  "check_all f = f (Code_Evaluation.valtermify (None :: 'a option)) orelse check_all (%(x, t). f (Some x, %_. Code_Evaluation.App (Code_Evaluation.term_of (Some :: 'a => 'a option)) (t ())))"
+
+instance ..
+
+end
+
+
 instantiation Enum.finite_1 :: check_all
 begin
 
@@ -205,11 +284,6 @@
 
 subsection {* Defining combinators for any first-order data type *}
 
-definition orelse :: "'a option => 'a option => 'a option"
-where
-  [code_unfold]: "orelse x y = (case x of Some x' => Some x' | None => y)"
-
-
 definition catch_match :: "term list option => term list option => term list option"
 where
   [code del]: "catch_match t1 t2 = (SOME t. t = t1 \<or> t = t2)"
@@ -224,6 +298,7 @@
 declare [[quickcheck_tester = exhaustive]]
 
 hide_fact orelse_def catch_match_def
+no_notation orelse (infixr "orelse" 55)
 hide_const (open) orelse catch_match mk_map_term check_all_n_lists
 
 end
\ No newline at end of file