# HG changeset patch
# User bulwahn
# Date 1291362046 -3600
# Node ID ef6fde932f4cab2f5bf363ca71ea46383b989411
# Parent  882e860a1e830539cf2be5087d95667e8c5ff370
improving readability of Smallcheck theory; adding constant orelse to improve performance of the function package

diff -r 882e860a1e83 -r ef6fde932f4c src/HOL/Smallcheck.thy
--- a/src/HOL/Smallcheck.thy	Fri Dec 03 08:40:46 2010 +0100
+++ b/src/HOL/Smallcheck.thy	Fri Dec 03 08:40:46 2010 +0100
@@ -48,7 +48,7 @@
 
 end
 
-section {* full small value generator type classes *}
+subsection {* full small value generator type classes *}
 
 class full_small = term_of +
 fixes full_small :: "('a * (unit => term) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
@@ -80,7 +80,7 @@
 
 instantiation prod :: (full_small, full_small) full_small
 begin
-ML {* @{const_name "Pair"} *}
+
 definition
   "full_small f d = full_small (%(x, t1). full_small (%(y, t2). f ((x, y),
     %u. Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.term_of (Pair :: 'a => 'b => ('a * 'b))) (t1 ())) (t2 ()))) d) d"
@@ -97,14 +97,16 @@
   "full_small_fun' f i d = (if i > 1 then
     full_small (%(a, at). full_small (%(b, bt).
       full_small_fun' (%(g, gt). f (g(a := b),
-        (%_. let T1 = (Typerep.typerep (TYPE('a))); T2 = (Typerep.typerep (TYPE('b))) in Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App
-         
-(Code_Evaluation.Const (STR ''Fun.fun_upd'')
-
-(Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''fun'') [T1, T2], Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''fun'') [T1, T2]]]]))
-
- (gt ())) (at ())) (bt ())))) (i - 1) d) d) d else (if i > 0 then
-  full_small (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d else None))"
+        (%_. let T1 = (Typerep.typerep (TYPE('a)));
+                 T2 = (Typerep.typerep (TYPE('b)))
+             in
+               Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App
+                 (Code_Evaluation.Const (STR ''Fun.fun_upd'')
+                    (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''fun'') [T1, T2],
+                       Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''fun'') [T1, T2]]]]))
+               (gt ())) (at ())) (bt ())))) (i - 1) d) d) d
+  else (if i > 0 then
+    full_small (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d else None))"
 
 definition full_small_fun :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => term list option"
 where
@@ -117,6 +119,11 @@
 
 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)"
@@ -130,7 +137,7 @@
 setup {* Smallvalue_Generators.setup *}
 *)
 
-hide_fact catch_match_def
-hide_const (open) catch_match
+hide_fact orelse_def catch_match_def
+hide_const (open) orelse catch_match
 
 end
\ No newline at end of file
diff -r 882e860a1e83 -r ef6fde932f4c src/HOL/Tools/smallvalue_generators.ML
--- a/src/HOL/Tools/smallvalue_generators.ML	Fri Dec 03 08:40:46 2010 +0100
+++ b/src/HOL/Tools/smallvalue_generators.ML	Fri Dec 03 08:40:46 2010 +0100
@@ -50,8 +50,8 @@
   let
     val (T as Type(@{type_name "option"}, [T'])) = fastype_of x
   in
-    Const (@{const_name Option.option_case}, T --> (T' --> T) --> T --> T)
-      $ y $ Const (@{const_name Some}, T' --> T) $ x
+    Const (@{const_name "Smallcheck.orelse"}, T --> T --> T)
+      $ x $ y
   end
 
 (** datatypes **)