38 "(set_eq ===> set_eq ===> set_eq) (op \<union>) (op \<union>)" |
38 "(set_eq ===> set_eq ===> set_eq) (op \<union>) (op \<union>)" |
39 "set_eq {} {}" |
39 "set_eq {} {}" |
40 "set_eq UNIV UNIV" |
40 "set_eq UNIV UNIV" |
41 "(set_eq ===> set_eq) uminus uminus" |
41 "(set_eq ===> set_eq) uminus uminus" |
42 "(set_eq ===> set_eq ===> set_eq) minus minus" |
42 "(set_eq ===> set_eq ===> set_eq) minus minus" |
43 "((set_eq ===> op =) ===> set_eq) Inf Inf" |
43 "(set_eq ===> op =) Inf Inf" |
44 "((set_eq ===> op =) ===> set_eq) Sup Sup" |
44 "(set_eq ===> op =) Sup Sup" |
45 "(op = ===> set_eq) List.set List.set" |
45 "(op = ===> set_eq) List.set List.set" |
46 "(set_eq ===> (op = ===> set_eq) ===> set_eq) UNION UNION" |
46 "(set_eq ===> (op = ===> set_eq) ===> set_eq) UNION UNION" |
47 by (auto simp: fun_rel_eq) |
47 by (auto simp: fun_rel_eq) |
48 |
48 |
49 quotient_definition "member :: 'a => 'a Cset.set => bool" |
49 quotient_definition "member :: 'a => 'a Cset.set => bool" |
82 is "Set.UNIV :: 'a set" |
82 is "Set.UNIV :: 'a set" |
83 quotient_definition uminus where "uminus :: 'a Cset.set \<Rightarrow> 'a Cset.set" |
83 quotient_definition uminus where "uminus :: 'a Cset.set \<Rightarrow> 'a Cset.set" |
84 is "uminus_class.uminus :: 'a set \<Rightarrow> 'a set" |
84 is "uminus_class.uminus :: 'a set \<Rightarrow> 'a set" |
85 quotient_definition minus where "minus :: 'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" |
85 quotient_definition minus where "minus :: 'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" |
86 is "(op -) :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" |
86 is "(op -) :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" |
87 quotient_definition Inf where "Inf :: 'a Cset.set set \<Rightarrow> 'a Cset.set" |
87 quotient_definition Inf where "Inf :: ('a :: Inf) Cset.set \<Rightarrow> 'a" |
88 is "Inf_class.Inf :: 'a set set \<Rightarrow> 'a set" |
88 is "Inf_class.Inf :: ('a :: Inf) set \<Rightarrow> 'a" |
89 quotient_definition Sup where "Sup :: 'a Cset.set set \<Rightarrow> 'a Cset.set" |
89 quotient_definition Sup where "Sup :: ('a :: Sup) Cset.set \<Rightarrow> 'a" |
90 is "Sup_class.Sup :: 'a set set \<Rightarrow> 'a set" |
90 is "Sup_class.Sup :: ('a :: Sup) set \<Rightarrow> 'a" |
91 quotient_definition UNION where "UNION :: 'a Cset.set \<Rightarrow> ('a \<Rightarrow> 'b Cset.set) \<Rightarrow> 'b Cset.set" |
91 quotient_definition UNION where "UNION :: 'a Cset.set \<Rightarrow> ('a \<Rightarrow> 'b Cset.set) \<Rightarrow> 'b Cset.set" |
92 is "Complete_Lattice.UNION :: 'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" |
92 is "Complete_Lattice.UNION :: 'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" |
93 |
|
94 |
|
95 context complete_lattice |
|
96 begin |
|
97 |
|
98 (* FIXME: Would like to use |
|
99 |
|
100 quotient_definition "Infimum :: 'a Cset.set \<Rightarrow> 'a" |
|
101 is "Inf" |
|
102 |
|
103 but it fails, presumably because @{term "Inf"} is a Free. |
|
104 *) |
|
105 |
|
106 definition Infimum :: "'a Cset.set \<Rightarrow> 'a" where |
|
107 [simp]: "Infimum A = Inf (\<lambda>x. member x A)" |
|
108 |
|
109 definition Supremum :: "'a Cset.set \<Rightarrow> 'a" where |
|
110 [simp]: "Supremum A = Sup (\<lambda>x. member x A)" |
|
111 |
|
112 end |
|
113 |
93 |
114 hide_const (open) is_empty insert remove map filter forall exists card |
94 hide_const (open) is_empty insert remove map filter forall exists card |
115 set subset psubset inter union empty UNIV uminus minus Inf Sup UNION |
95 set subset psubset inter union empty UNIV uminus minus Inf Sup UNION |
116 |
96 |
117 hide_fact (open) is_empty_def insert_def remove_def map_def filter_def |
97 hide_fact (open) is_empty_def insert_def remove_def map_def filter_def |
118 forall_def exists_def card_def set_def subset_def psubset_def |
98 forall_def exists_def card_def set_def subset_def psubset_def |
119 inter_def union_def empty_def UNIV_def uminus_def minus_def Inf_def Sup_def |
99 inter_def union_def empty_def UNIV_def uminus_def minus_def Inf_def Sup_def |
120 UNION_def |
100 UNION_def |
121 |
101 |
122 |
|
123 end |
102 end |