swapped dependencies of 'Finite_Set' and 'Option' (to move BNF up)
authorblanchet
Mon Jan 20 23:34:26 2014 +0100 (2014-01-20)
changeset 55089181751ad852f
parent 55088 57c82e01022b
child 55090 9475b16e520b
swapped dependencies of 'Finite_Set' and 'Option' (to move BNF up)
src/HOL/Finite_Set.thy
src/HOL/Lattices_Big.thy
src/HOL/Lifting_Option.thy
src/HOL/Option.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Mon Jan 20 23:07:23 2014 +0100
     1.2 +++ b/src/HOL/Finite_Set.thy	Mon Jan 20 23:34:26 2014 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  header {* Finite sets *}
     1.5  
     1.6  theory Finite_Set
     1.7 -imports Option Power
     1.8 +imports Power
     1.9  begin
    1.10  
    1.11  subsection {* Predicate for finite sets *}
    1.12 @@ -566,13 +566,6 @@
    1.13  instance sum :: (finite, finite) finite
    1.14    by default (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite)
    1.15  
    1.16 -lemma finite_option_UNIV [simp]:
    1.17 -  "finite (UNIV :: 'a option set) = finite (UNIV :: 'a set)"
    1.18 -  by (auto simp add: UNIV_option_conv elim: finite_imageD intro: inj_Some)
    1.19 -
    1.20 -instance option :: (finite) finite
    1.21 -  by default (simp add: UNIV_option_conv)
    1.22 -
    1.23  
    1.24  subsection {* A basic fold functional for finite sets *}
    1.25  
    1.26 @@ -1729,4 +1722,3 @@
    1.27  hide_const (open) Finite_Set.fold
    1.28  
    1.29  end
    1.30 -
     2.1 --- a/src/HOL/Lattices_Big.thy	Mon Jan 20 23:07:23 2014 +0100
     2.2 +++ b/src/HOL/Lattices_Big.thy	Mon Jan 20 23:34:26 2014 +0100
     2.3 @@ -6,7 +6,7 @@
     2.4  header {* Big infimum (minimum) and supremum (maximum) over finite (non-empty) sets *}
     2.5  
     2.6  theory Lattices_Big
     2.7 -imports Finite_Set
     2.8 +imports Finite_Set Option
     2.9  begin
    2.10  
    2.11  subsection {* Generic lattice operations over a set *}
     3.1 --- a/src/HOL/Lifting_Option.thy	Mon Jan 20 23:07:23 2014 +0100
     3.2 +++ b/src/HOL/Lifting_Option.thy	Mon Jan 20 23:34:26 2014 +0100
     3.3 @@ -5,7 +5,7 @@
     3.4  header {* Setup for Lifting/Transfer for the option type *}
     3.5  
     3.6  theory Lifting_Option
     3.7 -imports Lifting
     3.8 +imports Lifting Option
     3.9  begin
    3.10  
    3.11  subsection {* Relator and predicator properties *}
     4.1 --- a/src/HOL/Option.thy	Mon Jan 20 23:07:23 2014 +0100
     4.2 +++ b/src/HOL/Option.thy	Mon Jan 20 23:34:26 2014 +0100
     4.3 @@ -5,7 +5,7 @@
     4.4  header {* Datatype option *}
     4.5  
     4.6  theory Option
     4.7 -imports Datatype
     4.8 +imports Datatype Finite_Set
     4.9  begin
    4.10  
    4.11  datatype 'a option = None | Some 'a
    4.12 @@ -175,6 +175,16 @@
    4.13  hide_fact (open) map_cong bind_cong
    4.14  
    4.15  
    4.16 +subsubsection {* Interaction with finite sets *}
    4.17 +
    4.18 +lemma finite_option_UNIV [simp]:
    4.19 +  "finite (UNIV :: 'a option set) = finite (UNIV :: 'a set)"
    4.20 +  by (auto simp add: UNIV_option_conv elim: finite_imageD intro: inj_Some)
    4.21 +
    4.22 +instance option :: (finite) finite
    4.23 +  by default (simp add: UNIV_option_conv)
    4.24 +
    4.25 +
    4.26  subsubsection {* Code generator setup *}
    4.27  
    4.28  definition is_none :: "'a option \<Rightarrow> bool" where