equal
deleted
inserted
replaced
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 =) ===> set_eq) Inf Inf" |
44 "((set_eq ===> op =) ===> set_eq) Sup Sup" |
44 "((set_eq ===> op =) ===> set_eq) 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 by (auto simp: fun_rel_eq) |
47 by (auto simp: fun_rel_eq) |
47 |
48 |
48 quotient_definition "member :: 'a => 'a Cset.set => bool" |
49 quotient_definition "member :: 'a => 'a Cset.set => bool" |
49 is "op \<in>" |
50 is "op \<in>" |
50 quotient_definition "Set :: ('a => bool) => 'a Cset.set" |
51 quotient_definition "Set :: ('a => bool) => 'a Cset.set" |
85 is "(op -) :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" |
86 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 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 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 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 is "Sup_class.Sup :: 'a set set \<Rightarrow> 'a 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" |
90 |
93 |
91 |
94 |
92 context complete_lattice |
95 context complete_lattice |
93 begin |
96 begin |
94 |
97 |
107 [simp]: "Supremum A = Sup (\<lambda>x. member x A)" |
110 [simp]: "Supremum A = Sup (\<lambda>x. member x A)" |
108 |
111 |
109 end |
112 end |
110 |
113 |
111 hide_const (open) is_empty insert remove map filter forall exists card |
114 hide_const (open) is_empty insert remove map filter forall exists card |
112 set subset psubset inter union empty UNIV uminus minus Inf Sup |
115 set subset psubset inter union empty UNIV uminus minus Inf Sup UNION |
113 |
116 |
114 hide_fact (open) is_empty_def insert_def remove_def map_def filter_def |
117 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 |
118 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 |
119 inter_def union_def empty_def UNIV_def uminus_def minus_def Inf_def Sup_def |
|
120 UNION_def |
117 |
121 |
118 |
122 |
119 end |
123 end |