# HG changeset patch
# User blanchet
# Date 1390257266 -3600
# Node ID 181751ad852f41b97be18c08e9f1e52b3562c885
# Parent  57c82e01022b0805b9a741ab9b6eecc9ddc271cc
swapped dependencies of 'Finite_Set' and 'Option' (to move BNF up)

diff -r 57c82e01022b -r 181751ad852f src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Mon Jan 20 23:07:23 2014 +0100
+++ b/src/HOL/Finite_Set.thy	Mon Jan 20 23:34:26 2014 +0100
@@ -6,7 +6,7 @@
 header {* Finite sets *}
 
 theory Finite_Set
-imports Option Power
+imports Power
 begin
 
 subsection {* Predicate for finite sets *}
@@ -566,13 +566,6 @@
 instance sum :: (finite, finite) finite
   by default (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite)
 
-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)
-
 
 subsection {* A basic fold functional for finite sets *}
 
@@ -1729,4 +1722,3 @@
 hide_const (open) Finite_Set.fold
 
 end
-
diff -r 57c82e01022b -r 181751ad852f src/HOL/Lattices_Big.thy
--- a/src/HOL/Lattices_Big.thy	Mon Jan 20 23:07:23 2014 +0100
+++ b/src/HOL/Lattices_Big.thy	Mon Jan 20 23:34:26 2014 +0100
@@ -6,7 +6,7 @@
 header {* Big infimum (minimum) and supremum (maximum) over finite (non-empty) sets *}
 
 theory Lattices_Big
-imports Finite_Set
+imports Finite_Set Option
 begin
 
 subsection {* Generic lattice operations over a set *}
diff -r 57c82e01022b -r 181751ad852f src/HOL/Lifting_Option.thy
--- a/src/HOL/Lifting_Option.thy	Mon Jan 20 23:07:23 2014 +0100
+++ b/src/HOL/Lifting_Option.thy	Mon Jan 20 23:34:26 2014 +0100
@@ -5,7 +5,7 @@
 header {* Setup for Lifting/Transfer for the option type *}
 
 theory Lifting_Option
-imports Lifting
+imports Lifting Option
 begin
 
 subsection {* Relator and predicator properties *}
diff -r 57c82e01022b -r 181751ad852f src/HOL/Option.thy
--- 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