src/HOL/Datatype.thy
changeset 26146 61cb176d0385
parent 26072 f65a7fa2da6c
child 26339 7825c83c9eff
     1.1 --- a/src/HOL/Datatype.thy	Tue Feb 26 16:10:54 2008 +0100
     1.2 +++ b/src/HOL/Datatype.thy	Tue Feb 26 20:38:10 2008 +0100
     1.3 @@ -615,25 +615,8 @@
     1.4  lemma insert_None_conv_UNIV: "insert None (range Some) = UNIV"
     1.5    by (rule set_ext, case_tac x) auto
     1.6  
     1.7 -instantiation option :: (finite) finite
     1.8 -begin
     1.9 -
    1.10 -definition
    1.11 -  "Finite_Set.itself = TYPE('a option)"
    1.12 -
    1.13 -instance proof
    1.14 -  have "finite (UNIV :: 'a set)" by (rule finite)
    1.15 -  hence "finite (insert None (Some ` (UNIV :: 'a set)))" by simp
    1.16 -  also have "insert None (Some ` (UNIV :: 'a set)) = UNIV"
    1.17 -    by (rule insert_None_conv_UNIV)
    1.18 -  finally show "finite (UNIV :: 'a option set)" .
    1.19 -qed
    1.20 -
    1.21 -end
    1.22 -
    1.23 -lemma univ_option [noatp, code func]:
    1.24 -  "UNIV = insert (None \<Colon> 'a\<Colon>finite option) (image Some UNIV)"
    1.25 -  unfolding insert_None_conv_UNIV ..
    1.26 +instance option :: (finite) finite
    1.27 +  by default (simp add: insert_None_conv_UNIV [symmetric])
    1.28  
    1.29  
    1.30  subsubsection {* Operations *}