# HG changeset patch
# User haftmann
# Date 1172910418 -3600
# Node ID dfe146d65b14c8f4d434013b59e6f5cd4b454e19
# Parent  ec7ecf70695599de3bd017081ff33a5eaf318ccc
moved instance option :: finite here

diff -r ec7ecf706955 -r dfe146d65b14 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Sat Mar 03 00:16:09 2007 +0100
+++ b/src/HOL/Finite_Set.thy	Sat Mar 03 09:26:58 2007 +0100
@@ -7,7 +7,7 @@
 header {* Finite sets *}
 
 theory Finite_Set
-imports Power Divides Inductive Lattices
+imports Divides
 begin
 
 subsection {* Definition and basic properties *}
@@ -1639,7 +1639,6 @@
 apply (auto simp add: ring_distrib add_ac)
 done
 
-
 lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::{recpower, comm_monoid_mult})) = y^(card A)"
   apply (erule finite_induct)
   apply (auto simp add: power_Suc)
@@ -2588,6 +2587,22 @@
   "UNIV = (UNIV \<Colon> 'a\<Colon>finite set) <+> (UNIV \<Colon> 'b\<Colon>finite set)"
   unfolding UNIV_Plus_UNIV ..
 
+lemma insert_None_conv_UNIV: "insert None (range Some) = UNIV"
+  by (rule set_ext, case_tac x, auto)
+
+instance option :: (finite) finite
+proof
+  have "finite (UNIV :: 'a set)" by (rule finite)
+  hence "finite (insert None (Some ` (UNIV :: 'a set)))" by simp
+  also have "insert None (Some ` (UNIV :: 'a set)) = UNIV"
+    by (rule insert_None_conv_UNIV)
+  finally show "finite (UNIV :: 'a option set)" .
+qed
+
+lemma univ_option [code func]:
+  "UNIV = insert (None \<Colon> 'a\<Colon>finite option) (image Some UNIV)"
+  unfolding insert_None_conv_UNIV ..
+
 instance set :: (finite) finite
 proof
   have "finite (UNIV :: 'a set)" by (rule finite)