added finite(option) to Recdef.thy
authornipkow
Tue Aug 09 11:44:38 2005 +0200 (2005-08-09)
changeset 170406682c93b7d9f
parent 17039 78159411623f
child 17041 dee6f7047cae
added finite(option) to Recdef.thy
src/HOL/Recdef.thy
     1.1 --- a/src/HOL/Recdef.thy	Tue Aug 09 11:00:44 2005 +0200
     1.2 +++ b/src/HOL/Recdef.thy	Tue Aug 09 11:44:38 2005 +0200
     1.3 @@ -79,4 +79,19 @@
     1.4    wf_same_fst
     1.5    wf_empty
     1.6  
     1.7 +(* The following should really go into Datatype or Finite_Set, but
     1.8 +each one lacks the other theory as a parent . . . *)
     1.9 +
    1.10 +lemma insert_None_conv_UNIV: "insert None (range Some) = UNIV"
    1.11 +by (rule set_ext, case_tac x, auto)
    1.12 +
    1.13 +instance option :: (finite) finite
    1.14 +proof
    1.15 +  have "finite (UNIV :: 'a set)" by (rule finite)
    1.16 +  hence "finite (insert None (Some ` (UNIV :: 'a set)))" by simp
    1.17 +  also have "insert None (Some ` (UNIV :: 'a set)) = UNIV"
    1.18 +    by (rule insert_None_conv_UNIV)
    1.19 +  finally show "finite (UNIV :: 'a option set)" .
    1.20 +qed
    1.21 +
    1.22  end