src/HOL/Smallcheck.thy
changeset 40639 f1f0e6adca0a
parent 40620 7a9278de19ad
child 40899 ef6fde932f4c
     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