rational and real instances for new compilation scheme for exhaustive quickcheck
authorbulwahn
Fri Apr 08 16:31:14 2011 +0200 (2011-04-08)
changeset 42311eb32a8474a57
parent 42310 c664cc5cc5e9
child 42312 5bf3b9612e43
rational and real instances for new compilation scheme for exhaustive quickcheck
src/HOL/Rat.thy
src/HOL/RealDef.thy
     1.1 --- a/src/HOL/Rat.thy	Fri Apr 08 16:31:14 2011 +0200
     1.2 +++ b/src/HOL/Rat.thy	Fri Apr 08 16:31:14 2011 +0200
     1.3 @@ -1136,7 +1136,17 @@
     1.4  begin
     1.5  
     1.6  definition
     1.7 -  "exhaustive f d = exhaustive (%(k, kt). exhaustive (%(l, lt).
     1.8 +  "exhaustive f d = exhaustive (%k. exhaustive (%l. f (Fract (Code_Numeral.int_of k) (Code_Numeral.int_of l))) d) d"
     1.9 +
    1.10 +instance ..
    1.11 +
    1.12 +end
    1.13 +
    1.14 +instantiation rat :: full_exhaustive
    1.15 +begin
    1.16 +
    1.17 +definition
    1.18 +  "full_exhaustive f d = full_exhaustive (%(k, kt). full_exhaustive (%(l, lt).
    1.19       f (valterm_fract (Code_Numeral.int_of k, %_. Code_Evaluation.term_of (Code_Numeral.int_of k)) (Code_Numeral.int_of l, %_. Code_Evaluation.term_of (Code_Numeral.int_of l)))) d) d"
    1.20  
    1.21  instance ..
     2.1 --- a/src/HOL/RealDef.thy	Fri Apr 08 16:31:14 2011 +0200
     2.2 +++ b/src/HOL/RealDef.thy	Fri Apr 08 16:31:14 2011 +0200
     2.3 @@ -1772,7 +1772,17 @@
     2.4  begin
     2.5  
     2.6  definition
     2.7 -  "exhaustive f d = exhaustive (%r. f (valterm_ratreal r)) d"
     2.8 +  "exhaustive f d = exhaustive (%r. f (Ratreal r)) d"
     2.9 +
    2.10 +instance ..
    2.11 +
    2.12 +end
    2.13 +
    2.14 +instantiation real :: full_exhaustive
    2.15 +begin
    2.16 +
    2.17 +definition
    2.18 +  "full_exhaustive f d = full_exhaustive (%r. f (valterm_ratreal r)) d"
    2.19  
    2.20  instance ..
    2.21