author blanchet Mon Jan 20 23:34:26 2014 +0100 (2014-01-20) changeset 55089 181751ad852f parent 55088 57c82e01022b child 55090 9475b16e520b
swapped dependencies of 'Finite_Set' and 'Option' (to move BNF up)
 src/HOL/Finite_Set.thy file | annotate | diff | revisions src/HOL/Lattices_Big.thy file | annotate | diff | revisions src/HOL/Lifting_Option.thy file | annotate | diff | revisions src/HOL/Option.thy file | annotate | diff | revisions
```     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
```