src/HOL/Quickcheck_Exhaustive.thy
changeset 46417 1a68fcb80b62
parent 46311 56fae81902ce
child 46950 d0181abdbdac
     1.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Sun Feb 05 07:05:34 2012 +0100
     1.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Sun Feb 05 08:24:38 2012 +0100
     1.3 @@ -425,7 +425,8 @@
     1.4  begin
     1.5  
     1.6  definition
     1.7 -  "check_all f = (case f (Code_Evaluation.valtermify Enum.finite_2.a\<^isub>1) of Some x' \<Rightarrow> Some x' | None \<Rightarrow> f (Code_Evaluation.valtermify Enum.finite_2.a\<^isub>2))"
     1.8 +  "check_all f = (f (Code_Evaluation.valtermify Enum.finite_2.a\<^isub>1)
     1.9 +    orelse f (Code_Evaluation.valtermify Enum.finite_2.a\<^isub>2))"
    1.10  
    1.11  definition enum_term_of_finite_2 :: "Enum.finite_2 itself => unit => term list"
    1.12  where
    1.13 @@ -439,7 +440,9 @@
    1.14  begin
    1.15  
    1.16  definition
    1.17 -  "check_all f = (case f (Code_Evaluation.valtermify Enum.finite_3.a\<^isub>1) of Some x' \<Rightarrow> Some x' | None \<Rightarrow> (case f (Code_Evaluation.valtermify Enum.finite_3.a\<^isub>2) of Some x' \<Rightarrow> Some x' | None \<Rightarrow> f (Code_Evaluation.valtermify Enum.finite_3.a\<^isub>3)))"
    1.18 +  "check_all f = (f (Code_Evaluation.valtermify Enum.finite_3.a\<^isub>1)
    1.19 +    orelse f (Code_Evaluation.valtermify Enum.finite_3.a\<^isub>2)
    1.20 +    orelse f (Code_Evaluation.valtermify Enum.finite_3.a\<^isub>3))"
    1.21  
    1.22  definition enum_term_of_finite_3 :: "Enum.finite_3 itself => unit => term list"
    1.23  where
    1.24 @@ -449,6 +452,23 @@
    1.25  
    1.26  end
    1.27  
    1.28 +instantiation Enum.finite_4 :: check_all
    1.29 +begin
    1.30 +
    1.31 +definition
    1.32 +  "check_all f = (f (Code_Evaluation.valtermify Enum.finite_4.a\<^isub>1)
    1.33 +    orelse f (Code_Evaluation.valtermify Enum.finite_4.a\<^isub>2)
    1.34 +    orelse f (Code_Evaluation.valtermify Enum.finite_4.a\<^isub>3)
    1.35 +    orelse f (Code_Evaluation.valtermify Enum.finite_4.a\<^isub>4))"
    1.36 +
    1.37 +definition enum_term_of_finite_4 :: "Enum.finite_4 itself => unit => term list"
    1.38 +where
    1.39 +  "enum_term_of_finite_4 = (%_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_4 list))"
    1.40 +
    1.41 +instance ..
    1.42 +
    1.43 +end
    1.44 +
    1.45  subsection {* Bounded universal quantifiers *}
    1.46  
    1.47  class bounded_forall =