--- a/src/HOL/Option.thy Mon Jan 20 23:07:23 2014 +0100
+++ b/src/HOL/Option.thy Mon Jan 20 23:34:26 2014 +0100
@@ -5,7 +5,7 @@
header {* Datatype option *}
theory Option
-imports Datatype
+imports Datatype Finite_Set
begin
datatype 'a option = None | Some 'a
@@ -175,6 +175,16 @@
hide_fact (open) map_cong bind_cong
+subsubsection {* Interaction with finite sets *}
+
+lemma finite_option_UNIV [simp]:
+ "finite (UNIV :: 'a option set) = finite (UNIV :: 'a set)"
+ by (auto simp add: UNIV_option_conv elim: finite_imageD intro: inj_Some)
+
+instance option :: (finite) finite
+ by default (simp add: UNIV_option_conv)
+
+
subsubsection {* Code generator setup *}
definition is_none :: "'a option \<Rightarrow> bool" where