changing iteration scheme of functions to use minimal number of function updates for exhaustive testing
authorbulwahn
Fri Mar 25 16:03:49 2011 +0100 (2011-03-25)
changeset 42117306713ec55c3
parent 42112 9cb122742f5c
child 42118 a51761c262d1
changing iteration scheme of functions to use minimal number of function updates for exhaustive testing
src/HOL/Quickcheck_Exhaustive.thy
     1.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Fri Mar 25 15:22:09 2011 +0100
     1.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Fri Mar 25 16:03:49 2011 +0100
     1.3 @@ -91,19 +91,17 @@
     1.4  
     1.5  fun exhaustive_fun' :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
     1.6  where
     1.7 -  "exhaustive_fun' f i d = (if i > 1 then
     1.8 -    exhaustive (%(a, at). exhaustive (%(b, bt).
     1.9 -      exhaustive_fun' (%(g, gt). f (g(a := b),
    1.10 -        (%_. let T1 = (Typerep.typerep (TYPE('a)));
    1.11 -                 T2 = (Typerep.typerep (TYPE('b)))
    1.12 -             in
    1.13 -               Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App
    1.14 -                 (Code_Evaluation.Const (STR ''Fun.fun_upd'')
    1.15 -                    (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''fun'') [T1, T2],
    1.16 -                       Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''fun'') [T1, T2]]]]))
    1.17 -               (gt ())) (at ())) (bt ())))) (i - 1) d) d) d
    1.18 -  else (if i > 0 then
    1.19 -    exhaustive (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d else None))"
    1.20 +  "exhaustive_fun' f i d = (exhaustive (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d)
    1.21 +   orelse (if i > 1 then
    1.22 +     exhaustive_fun' (%(g, gt). exhaustive (%(a, at). exhaustive (%(b, bt).
    1.23 +       f (g(a := b),
    1.24 +         (%_. let A = (Typerep.typerep (TYPE('a)));
    1.25 +                  B = (Typerep.typerep (TYPE('b)));
    1.26 +                  fun = (%T U. Typerep.Typerep (STR ''fun'') [T, U])
    1.27 +              in
    1.28 +                Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App
    1.29 +                  (Code_Evaluation.Const (STR ''Fun.fun_upd'') (fun (fun A B) (fun A (fun B (fun A B)))))
    1.30 +                (gt ())) (at ())) (bt ())))) d) d) (i - 1) d else None)"
    1.31  
    1.32  definition exhaustive_fun :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => term list option"
    1.33  where