src/HOL/Smallcheck.thy
changeset 41231 2e901158675e
parent 41178 f4d3acf0c4cc
child 41719 91c2510e19c5
     1.1 --- a/src/HOL/Smallcheck.thy	Fri Dec 17 08:37:35 2010 +0100
     1.2 +++ b/src/HOL/Smallcheck.thy	Fri Dec 17 12:14:18 2010 +0100
     1.3 @@ -67,6 +67,31 @@
     1.4  
     1.5  end
     1.6  
     1.7 +instantiation code_numeral :: full_small
     1.8 +begin
     1.9 +
    1.10 +function full_small_code_numeral' :: "(code_numeral * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
    1.11 +  where "full_small_code_numeral' 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_code_numeral' f d (i + 1)))"
    1.12 +by pat_completeness auto
    1.13 +
    1.14 +termination 
    1.15 +  by (relation "measure (%(_, d, i). Code_Numeral.nat_of (d + 1 - i))") auto
    1.16 +
    1.17 +definition "full_small f d = full_small_code_numeral' f d 0"
    1.18 +
    1.19 +instance ..
    1.20 +
    1.21 +end
    1.22 +
    1.23 +instantiation nat :: full_small
    1.24 +begin
    1.25 +
    1.26 +definition "full_small f d = full_small (%(x, xt). f (Code_Numeral.nat_of x, %_. Code_Evaluation.term_of (Code_Numeral.nat_of x))) d"
    1.27 +
    1.28 +instance ..
    1.29 +
    1.30 +end
    1.31 +
    1.32  instantiation int :: full_small
    1.33  begin
    1.34