src/HOL/Datatype.thy
changeset 24728 e2b3a1065676
parent 24699 c6674504103f
child 24845 abcd15369ffa
     1.1 --- a/src/HOL/Datatype.thy	Wed Sep 26 19:19:38 2007 +0200
     1.2 +++ b/src/HOL/Datatype.thy	Wed Sep 26 20:27:55 2007 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  header {* Analogues of the Cartesian Product and Disjoint Sum for Datatypes *}
     1.5  
     1.6  theory Datatype
     1.7 -imports Nat
     1.8 +imports Finite_Set
     1.9  begin
    1.10  
    1.11  typedef (Node)
    1.12 @@ -613,6 +613,22 @@
    1.13    | (Some) y where "x = Some y" and "Q y"
    1.14    using c by (cases x) simp_all
    1.15  
    1.16 +lemma insert_None_conv_UNIV: "insert None (range Some) = UNIV"
    1.17 +  by (rule set_ext, case_tac x) auto
    1.18 +
    1.19 +instance option :: (finite) finite
    1.20 +proof
    1.21 +  have "finite (UNIV :: 'a set)" by (rule finite)
    1.22 +  hence "finite (insert None (Some ` (UNIV :: 'a set)))" by simp
    1.23 +  also have "insert None (Some ` (UNIV :: 'a set)) = UNIV"
    1.24 +    by (rule insert_None_conv_UNIV)
    1.25 +  finally show "finite (UNIV :: 'a option set)" .
    1.26 +qed
    1.27 +
    1.28 +lemma univ_option [noatp, code func]:
    1.29 +  "UNIV = insert (None \<Colon> 'a\<Colon>finite option) (image Some UNIV)"
    1.30 +  unfolding insert_None_conv_UNIV ..
    1.31 +
    1.32  
    1.33  subsubsection {* Operations *}
    1.34  
    1.35 @@ -638,7 +654,6 @@
    1.36  lemma o2s_empty_eq [simp]: "(o2s xo = {}) = (xo = None)"
    1.37    by (cases xo) auto
    1.38  
    1.39 -
    1.40  constdefs
    1.41    option_map :: "('a => 'b) => ('a option => 'b option)"
    1.42    "option_map == %f y. case y of None => None | Some x => Some (f x)"