# HG changeset patch
# User bulwahn
# Date 1328426678 -3600
# Node ID 1a68fcb80b62c002971cf23f7ce65bdcee2e70b4
# Parent  5f5665a0b9737f816906b4a10fe65d18aa8b3eb6
beautifying definitions of check_all and adding instance for finite_4

diff -r 5f5665a0b973 -r 1a68fcb80b62 src/HOL/Quickcheck_Exhaustive.thy
--- a/src/HOL/Quickcheck_Exhaustive.thy	Sun Feb 05 07:05:34 2012 +0100
+++ b/src/HOL/Quickcheck_Exhaustive.thy	Sun Feb 05 08:24:38 2012 +0100
@@ -425,7 +425,8 @@
 begin
 
 definition
-  "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))"
+  "check_all f = (f (Code_Evaluation.valtermify Enum.finite_2.a\<^isub>1)
+    orelse f (Code_Evaluation.valtermify Enum.finite_2.a\<^isub>2))"
 
 definition enum_term_of_finite_2 :: "Enum.finite_2 itself => unit => term list"
 where
@@ -439,7 +440,9 @@
 begin
 
 definition
-  "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)))"
+  "check_all f = (f (Code_Evaluation.valtermify Enum.finite_3.a\<^isub>1)
+    orelse f (Code_Evaluation.valtermify Enum.finite_3.a\<^isub>2)
+    orelse f (Code_Evaluation.valtermify Enum.finite_3.a\<^isub>3))"
 
 definition enum_term_of_finite_3 :: "Enum.finite_3 itself => unit => term list"
 where
@@ -449,6 +452,23 @@
 
 end
 
+instantiation Enum.finite_4 :: check_all
+begin
+
+definition
+  "check_all f = (f (Code_Evaluation.valtermify Enum.finite_4.a\<^isub>1)
+    orelse f (Code_Evaluation.valtermify Enum.finite_4.a\<^isub>2)
+    orelse f (Code_Evaluation.valtermify Enum.finite_4.a\<^isub>3)
+    orelse f (Code_Evaluation.valtermify Enum.finite_4.a\<^isub>4))"
+
+definition enum_term_of_finite_4 :: "Enum.finite_4 itself => unit => term list"
+where
+  "enum_term_of_finite_4 = (%_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_4 list))"
+
+instance ..
+
+end
+
 subsection {* Bounded universal quantifiers *}
 
 class bounded_forall =