src/HOL/Smallcheck.thy
```     1.1 --- a/src/HOL/Smallcheck.thy	Mon Nov 22 10:41:57 2010 +0100
1.2 +++ b/src/HOL/Smallcheck.thy	Mon Nov 22 10:41:58 2010 +0100
1.3 @@ -16,7 +16,7 @@
1.4  instantiation unit :: small
1.5  begin
1.6
1.7 -definition "find_first f d = f ()"
1.8 +definition "small f d = f ()"
1.9
1.10  instance ..
1.11
1.12 @@ -48,6 +48,73 @@
1.13
1.14  end
1.15
1.16 +section {* full small value generator type classes *}
1.17 +
1.18 +class full_small = term_of +
1.19 +fixes full_small :: "('a * (unit => term) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
1.20 +
1.21 +instantiation unit :: full_small
1.22 +begin
1.23 +
1.24 +definition "full_small f d = f (Code_Evaluation.valtermify ())"
1.25 +
1.26 +instance ..
1.27 +
1.28 +end
1.29 +
1.30 +instantiation int :: full_small
1.31 +begin
1.32 +
1.33 +function full_small' :: "(int * (unit => term) => term list option) => int => int => term list option"
1.34 +  where "full_small' f d i = (if d < i then None else (case f (i, %_. Code_Evaluation.term_of i) of Some t => Some t | None => full_small' f d (i + 1)))"
1.35 +by pat_completeness auto
1.36 +
1.37 +termination
1.38 +  by (relation "measure (%(_, d, i). nat (d + 1 - i))") auto
1.39 +
1.40 +definition "full_small f d = full_small' f (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
1.41 +
1.42 +instance ..
1.43 +
1.44 +end
1.45 +
1.46 +instantiation prod :: (full_small, full_small) full_small
1.47 +begin
1.48 +ML {* @{const_name "Pair"} *}
1.49 +definition
1.50 +  "full_small f d = full_small (%(x, t1). full_small (%(y, t2). f ((x, y),
1.51 +    %u. Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.term_of (Pair :: 'a => 'b => ('a * 'b))) (t1 ())) (t2 ()))) d) d"
1.52 +
1.53 +instance ..
1.54 +
1.55 +end
1.56 +
1.57 +instantiation "fun" :: ("{equal, full_small}", full_small) full_small
1.58 +begin
1.59 +
1.60 +fun full_small_fun' :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
1.61 +where
1.62 +  "full_small_fun' f i d = (if i > 1 then
1.63 +    full_small (%(a, at). full_small (%(b, bt).
1.64 +      full_small_fun' (%(g, gt). f (g(a := b),
1.65 +        (%_. let T1 = (Typerep.typerep (TYPE('a))); T2 = (Typerep.typerep (TYPE('b))) in Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App
1.66 +
1.67 +(Code_Evaluation.Const (STR ''Fun.fun_upd'')
1.68 +
1.69 +(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]]]]))
1.70 +
1.71 + (gt ())) (at ())) (bt ())))) (i - 1) d) d) d else (if i > 0 then
1.72 +  full_small (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d else None))"
1.73 +
1.74 +definition full_small_fun :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => term list option"
1.75 +where
1.76 +  "full_small_fun f d = full_small_fun' f d d"
1.77 +
1.78 +
1.79 +instance ..
1.80 +
1.81 +end
1.82 +
1.83  subsection {* Defining combinators for any first-order data type *}
1.84
1.85  definition catch_match :: "term list option => term list option => term list option"
1.86 @@ -59,7 +126,7 @@
1.87
1.88  use "Tools/smallvalue_generators.ML"
1.89
1.90 -(* We do not activate smallcheck yet.
1.91 +(* We do not activate smallcheck yet.
1.92  setup {* Smallvalue_Generators.setup *}
1.93  *)
1.94
```