# HG changeset patch # User haftmann # Date 1492071009 -7200 # Node ID 721feefce9c6e8b40560732b9183898e75ded306 # Parent b11b7ad226841dfa79836574972bdee0b3e5f0cb early abort on depth limit diff -r b11b7ad22684 -r 721feefce9c6 src/HOL/Quickcheck_Narrowing.thy --- a/src/HOL/Quickcheck_Narrowing.thy Thu Apr 13 10:10:08 2017 +0200 +++ b/src/HOL/Quickcheck_Narrowing.thy Thu Apr 13 10:10:09 2017 +0200 @@ -99,13 +99,14 @@ definition "apply" :: "('a => 'b) narrowing => 'a narrowing => 'b narrowing" where - "apply f a d = + "apply f a d = (if d > 0 then (case f d of Narrowing_cons (Narrowing_sum_of_products ps) cfs \ case a (d - 1) of Narrowing_cons ta cas \ let - shallow = d > 0 \ non_empty ta; + shallow = non_empty ta; cs = [(\(x # xs) \ cf xs (conv cas x)). shallow, cf \ cfs] - in Narrowing_cons (Narrowing_sum_of_products [ta # p. shallow, p \ ps]) cs)" + in Narrowing_cons (Narrowing_sum_of_products [ta # p. shallow, p \ ps]) cs) + else Narrowing_cons (Narrowing_sum_of_products []) [])" definition sum :: "'a narrowing => 'a narrowing => 'a narrowing" where