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.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.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.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.22  definition enum_term_of_finite_3 :: "Enum.finite_3 itself => unit => term list"
1.23  where
1.24 @@ -449,6 +452,23 @@
1.26  end
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.47  class bounded_forall =