|
1 (* Title: HOL/Quotient_Examples/Cset.thy |
|
2 Author: Florian Haftmann, Alexander Krauss, TU Muenchen |
|
3 *) |
|
4 |
|
5 header {* A variant of theory Cset from Library, defined as a quotient *} |
|
6 |
|
7 theory Cset |
|
8 imports "~~/src/HOL/Library/More_Set" "~~/src/HOL/Library/More_List" "~~/src/HOL/Library/Quotient_Syntax" |
|
9 begin |
|
10 |
|
11 subsection {* Lifting *} |
|
12 |
|
13 (*FIXME: quotient package requires a dedicated constant*) |
|
14 definition set_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" |
|
15 where [simp]: "set_eq \<equiv> op =" |
|
16 |
|
17 quotient_type 'a set = "'a Set.set" / "set_eq" |
|
18 by (simp add: identity_equivp) |
|
19 |
|
20 hide_type (open) set |
|
21 |
|
22 subsection {* Operations *} |
|
23 |
|
24 lemma [quot_respect]: |
|
25 "(op = ===> set_eq ===> op =) (op \<in>) (op \<in>)" |
|
26 "(op = ===> set_eq) Collect Collect" |
|
27 "(set_eq ===> op =) More_Set.is_empty More_Set.is_empty" |
|
28 "(op = ===> set_eq ===> set_eq) Set.insert Set.insert" |
|
29 "(op = ===> set_eq ===> set_eq) More_Set.remove More_Set.remove" |
|
30 "(op = ===> set_eq ===> set_eq) image image" |
|
31 "(op = ===> set_eq ===> set_eq) More_Set.project More_Set.project" |
|
32 "(set_eq ===> op =) Ball Ball" |
|
33 "(set_eq ===> op =) Bex Bex" |
|
34 "(set_eq ===> op =) Finite_Set.card Finite_Set.card" |
|
35 "(set_eq ===> set_eq ===> op =) (op \<subseteq>) (op \<subseteq>)" |
|
36 "(set_eq ===> set_eq ===> op =) (op \<subset>) (op \<subset>)" |
|
37 "(set_eq ===> set_eq ===> set_eq) (op \<inter>) (op \<inter>)" |
|
38 "(set_eq ===> set_eq ===> set_eq) (op \<union>) (op \<union>)" |
|
39 "set_eq {} {}" |
|
40 "set_eq UNIV UNIV" |
|
41 "(set_eq ===> set_eq) uminus uminus" |
|
42 "(set_eq ===> set_eq ===> set_eq) minus minus" |
|
43 "((set_eq ===> op =) ===> set_eq) Inf Inf" |
|
44 "((set_eq ===> op =) ===> set_eq) Sup Sup" |
|
45 "(op = ===> set_eq) List.set List.set" |
|
46 by (auto simp: fun_rel_eq) |
|
47 |
|
48 quotient_definition "member :: 'a => 'a Cset.set => bool" |
|
49 is "op \<in>" |
|
50 quotient_definition "Set :: ('a => bool) => 'a Cset.set" |
|
51 is Collect |
|
52 quotient_definition is_empty where "is_empty :: 'a Cset.set \<Rightarrow> bool" |
|
53 is More_Set.is_empty |
|
54 quotient_definition insert where "insert :: 'a \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" |
|
55 is Set.insert |
|
56 quotient_definition remove where "remove :: 'a \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" |
|
57 is More_Set.remove |
|
58 quotient_definition map where "map :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a Cset.set \<Rightarrow> 'b Cset.set" |
|
59 is image |
|
60 quotient_definition filter where "filter :: ('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" |
|
61 is More_Set.project |
|
62 quotient_definition "forall :: 'a Cset.set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" |
|
63 is Ball |
|
64 quotient_definition "exists :: 'a Cset.set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" |
|
65 is Bex |
|
66 quotient_definition card where "card :: 'a Cset.set \<Rightarrow> nat" |
|
67 is Finite_Set.card |
|
68 quotient_definition set where "set :: 'a list => 'a Cset.set" |
|
69 is List.set |
|
70 quotient_definition subset where "subset :: 'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> bool" |
|
71 is "op \<subseteq> :: 'a set \<Rightarrow> 'a set \<Rightarrow> bool" |
|
72 quotient_definition psubset where "psubset :: 'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> bool" |
|
73 is "op \<subset> :: 'a set \<Rightarrow> 'a set \<Rightarrow> bool" |
|
74 quotient_definition inter where "inter :: 'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" |
|
75 is "op \<inter> :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" |
|
76 quotient_definition union where "union :: 'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" |
|
77 is "op \<union> :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" |
|
78 quotient_definition empty where "empty :: 'a Cset.set" |
|
79 is "{} :: 'a set" |
|
80 quotient_definition UNIV where "UNIV :: 'a Cset.set" |
|
81 is "Set.UNIV :: 'a set" |
|
82 quotient_definition uminus where "uminus :: 'a Cset.set \<Rightarrow> 'a Cset.set" |
|
83 is "uminus_class.uminus :: 'a set \<Rightarrow> 'a set" |
|
84 quotient_definition minus where "minus :: 'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" |
|
85 is "(op -) :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" |
|
86 quotient_definition Inf where "Inf :: 'a Cset.set set \<Rightarrow> 'a Cset.set" |
|
87 is "Inf_class.Inf :: 'a set set \<Rightarrow> 'a set" |
|
88 quotient_definition Sup where "Sup :: 'a Cset.set set \<Rightarrow> 'a Cset.set" |
|
89 is "Sup_class.Sup :: 'a set set \<Rightarrow> 'a set" |
|
90 |
|
91 |
|
92 context complete_lattice |
|
93 begin |
|
94 |
|
95 (* FIXME: Would like to use |
|
96 |
|
97 quotient_definition "Infimum :: 'a Cset.set \<Rightarrow> 'a" |
|
98 is "Inf" |
|
99 |
|
100 but it fails, presumably because @{term "Inf"} is a Free. |
|
101 *) |
|
102 |
|
103 definition Infimum :: "'a Cset.set \<Rightarrow> 'a" where |
|
104 [simp]: "Infimum A = Inf (\<lambda>x. member x A)" |
|
105 |
|
106 definition Supremum :: "'a Cset.set \<Rightarrow> 'a" where |
|
107 [simp]: "Supremum A = Sup (\<lambda>x. member x A)" |
|
108 |
|
109 end |
|
110 |
|
111 hide_const (open) is_empty insert remove map filter forall exists card |
|
112 set subset psubset inter union empty UNIV uminus minus Inf Sup |
|
113 |
|
114 hide_fact (open) is_empty_def insert_def remove_def map_def filter_def |
|
115 forall_def exists_def card_def set_def subset_def psubset_def |
|
116 inter_def union_def empty_def UNIV_def uminus_def minus_def Inf_def Sup_def |
|
117 |
|
118 |
|
119 end |