1.1 --- a/src/HOL/Finite_Set.thy	Sun Sep 04 09:28:15 2011 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Mon Sep 05 07:49:31 2011 +0200
     1.3 @@ -486,22 +486,9 @@
     1.4  
     1.5  end
     1.6  
     1.7 -instance unit :: finite proof
     1.8 -qed (simp add: UNIV_unit)
     1.9 -
    1.10 -instance bool :: finite proof
    1.11 -qed (simp add: UNIV_bool)
    1.12 -
    1.13  instance prod :: (finite, finite) finite proof
    1.14  qed (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite)
    1.15  
    1.16 -lemma finite_option_UNIV [simp]:
    1.17 -  "finite (UNIV :: 'a option set) = finite (UNIV :: 'a set)"
    1.18 -  by (auto simp add: UNIV_option_conv elim: finite_imageD intro: inj_Some)
    1.19 -
    1.20 -instance option :: (finite) finite proof
    1.21 -qed (simp add: UNIV_option_conv)
    1.22 -
    1.23  lemma inj_graph: "inj (%f. {(x, y). y = f x})"
    1.24    by (rule inj_onI, auto simp add: set_eq_iff fun_eq_iff)
    1.25  
    1.26 @@ -519,9 +506,22 @@
    1.27    qed
    1.28  qed
    1.29  
    1.30 +instance bool :: finite proof
    1.31 +qed (simp add: UNIV_bool)
    1.32 +
    1.33 +instance unit :: finite proof
    1.34 +qed (simp add: UNIV_unit)
    1.35 +
    1.36  instance sum :: (finite, finite) finite proof
    1.37  qed (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite)
    1.38  
    1.39 +lemma finite_option_UNIV [simp]:
    1.40 +  "finite (UNIV :: 'a option set) = finite (UNIV :: 'a set)"
    1.41 +  by (auto simp add: UNIV_option_conv elim: finite_imageD intro: inj_Some)
    1.42 +
    1.43 +instance option :: (finite) finite proof
    1.44 +qed (simp add: UNIV_option_conv)
    1.45 +
    1.46  
    1.47  subsection {* A basic fold functional for finite sets *}
    1.48