quickcheck setup for float, inspired by rat::{exhaustive,full_exhaustive,random}
authorimmler
Wed Nov 12 17:37:43 2014 +0100 (2014-11-12)
changeset 58987119680ebf37c
parent 58986 ec7373051a6c
child 58988 6ebf918128b9
quickcheck setup for float, inspired by rat::{exhaustive,full_exhaustive,random}
src/HOL/Library/Float.thy
     1.1 --- a/src/HOL/Library/Float.thy	Wed Nov 12 17:37:43 2014 +0100
     1.2 +++ b/src/HOL/Library/Float.thy	Wed Nov 12 17:37:43 2014 +0100
     1.3 @@ -260,6 +260,46 @@
     1.4      and float_of_neg_numeral[simp]: "- numeral k = float_of (- numeral k)"
     1.5    unfolding real_of_float_eq by simp_all
     1.6  
     1.7 +subsection {* Quickcheck *}
     1.8 +
     1.9 +instantiation float :: exhaustive
    1.10 +begin
    1.11 +
    1.12 +definition exhaustive_float where
    1.13 +  "exhaustive_float f d =
    1.14 +    Quickcheck_Exhaustive.exhaustive (%x. Quickcheck_Exhaustive.exhaustive (%y. f (Float x y)) d) d"
    1.15 +
    1.16 +instance ..
    1.17 +
    1.18 +end
    1.19 +
    1.20 +definition (in term_syntax) [code_unfold]:
    1.21 +  "valtermify_float x y = Code_Evaluation.valtermify Float {\<cdot>} x {\<cdot>} y"
    1.22 +
    1.23 +instantiation float :: full_exhaustive
    1.24 +begin
    1.25 +
    1.26 +definition full_exhaustive_float where
    1.27 +  "full_exhaustive_float f d =
    1.28 +    Quickcheck_Exhaustive.full_exhaustive
    1.29 +      (\<lambda>x. Quickcheck_Exhaustive.full_exhaustive (\<lambda>y. f (valtermify_float x y)) d) d"
    1.30 +
    1.31 +instance ..
    1.32 +
    1.33 +end
    1.34 +
    1.35 +instantiation float :: random
    1.36 +begin
    1.37 +
    1.38 +definition "Quickcheck_Random.random i =
    1.39 +  scomp (Quickcheck_Random.random (2 ^ nat_of_natural i))
    1.40 +    (\<lambda>man. scomp (Quickcheck_Random.random i) (\<lambda>exp. Pair (valtermify_float man exp)))"
    1.41 +
    1.42 +instance ..
    1.43 +
    1.44 +end
    1.45 +
    1.46 +
    1.47  subsection {* Represent floats as unique mantissa and exponent *}
    1.48  
    1.49  lemma int_induct_abs[case_names less]: