author | haftmann |
Mon, 26 Dec 2011 18:32:43 +0100 | |
changeset 45986 | c9e50153e5ae |
parent 45319 | 2b002c6b0f7d |
child 45990 | b7b905b23b2a |
permissions | -rw-r--r-- |
45319
2b002c6b0f7d
renaming Quotient_Set and List_Quotient_Set to Quotient_Cset and List_Quotient_Cset to avoid name clash with existing Quotient_Set (again, cf. 66823a0066db)
bulwahn
parents:
45267
diff
changeset
|
1 |
(* Title: HOL/Quotient_Examples/Quotient_Cset.thy |
43800
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
2 |
Author: Florian Haftmann, Alexander Krauss, TU Muenchen |
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
3 |
*) |
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
4 |
|
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
5 |
header {* A variant of theory Cset from Library, defined as a quotient *} |
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
6 |
|
45319
2b002c6b0f7d
renaming Quotient_Set and List_Quotient_Set to Quotient_Cset and List_Quotient_Cset to avoid name clash with existing Quotient_Set (again, cf. 66823a0066db)
bulwahn
parents:
45267
diff
changeset
|
7 |
theory Quotient_Cset |
43800
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
8 |
imports "~~/src/HOL/Library/More_Set" "~~/src/HOL/Library/More_List" "~~/src/HOL/Library/Quotient_Syntax" |
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
9 |
begin |
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
10 |
|
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
11 |
subsection {* Lifting *} |
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
12 |
|
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
13 |
(*FIXME: quotient package requires a dedicated constant*) |
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
14 |
definition set_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" |
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
15 |
where [simp]: "set_eq \<equiv> op =" |
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
16 |
|
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
17 |
quotient_type 'a set = "'a Set.set" / "set_eq" |
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
18 |
by (simp add: identity_equivp) |
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
19 |
|
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
20 |
hide_type (open) set |
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
21 |
|
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
22 |
subsection {* Operations *} |
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
23 |
|
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
24 |
lemma [quot_respect]: |
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
25 |
"(op = ===> set_eq ===> op =) (op \<in>) (op \<in>)" |
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
26 |
"(op = ===> set_eq) Collect Collect" |
45986
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45319
diff
changeset
|
27 |
"(set_eq ===> op =) Set.is_empty Set.is_empty" |
43800
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
28 |
"(op = ===> set_eq ===> set_eq) Set.insert Set.insert" |
45986
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45319
diff
changeset
|
29 |
"(op = ===> set_eq ===> set_eq) Set.remove Set.remove" |
43800
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
30 |
"(op = ===> set_eq ===> set_eq) image image" |
45986
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45319
diff
changeset
|
31 |
"(op = ===> set_eq ===> set_eq) Set.project Set.project" |
43800
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
32 |
"(set_eq ===> op =) Ball Ball" |
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
33 |
"(set_eq ===> op =) Bex Bex" |
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
34 |
"(set_eq ===> op =) Finite_Set.card Finite_Set.card" |
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
35 |
"(set_eq ===> set_eq ===> op =) (op \<subseteq>) (op \<subseteq>)" |
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
36 |
"(set_eq ===> set_eq ===> op =) (op \<subset>) (op \<subset>)" |
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
37 |
"(set_eq ===> set_eq ===> set_eq) (op \<inter>) (op \<inter>)" |
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
38 |
"(set_eq ===> set_eq ===> set_eq) (op \<union>) (op \<union>)" |
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
39 |
"set_eq {} {}" |
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
40 |
"set_eq UNIV UNIV" |
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
41 |
"(set_eq ===> set_eq) uminus uminus" |
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
42 |
"(set_eq ===> set_eq ===> set_eq) minus minus" |
44293
83c4f8ba0aa3
Quotient_Examples: Cset, List_Cset: Lift Inf and Sup directly.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
43926
diff
changeset
|
43 |
"(set_eq ===> op =) Inf Inf" |
83c4f8ba0aa3
Quotient_Examples: Cset, List_Cset: Lift Inf and Sup directly.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
43926
diff
changeset
|
44 |
"(set_eq ===> op =) Sup Sup" |
43800
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
45 |
"(op = ===> set_eq) List.set List.set" |
43926 | 46 |
"(set_eq ===> (op = ===> set_eq) ===> set_eq) UNION UNION" |
43800
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
47 |
by (auto simp: fun_rel_eq) |
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
48 |
|
45319
2b002c6b0f7d
renaming Quotient_Set and List_Quotient_Set to Quotient_Cset and List_Quotient_Cset to avoid name clash with existing Quotient_Set (again, cf. 66823a0066db)
bulwahn
parents:
45267
diff
changeset
|
49 |
quotient_definition "member :: 'a => 'a Quotient_Cset.set => bool" |
43800
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
50 |
is "op \<in>" |
45319
2b002c6b0f7d
renaming Quotient_Set and List_Quotient_Set to Quotient_Cset and List_Quotient_Cset to avoid name clash with existing Quotient_Set (again, cf. 66823a0066db)
bulwahn
parents:
45267
diff
changeset
|
51 |
quotient_definition "Set :: ('a => bool) => 'a Quotient_Cset.set" |
43800
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
52 |
is Collect |
45319
2b002c6b0f7d
renaming Quotient_Set and List_Quotient_Set to Quotient_Cset and List_Quotient_Cset to avoid name clash with existing Quotient_Set (again, cf. 66823a0066db)
bulwahn
parents:
45267
diff
changeset
|
53 |
quotient_definition is_empty where "is_empty :: 'a Quotient_Cset.set \<Rightarrow> bool" |
45986
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45319
diff
changeset
|
54 |
is Set.is_empty |
45319
2b002c6b0f7d
renaming Quotient_Set and List_Quotient_Set to Quotient_Cset and List_Quotient_Cset to avoid name clash with existing Quotient_Set (again, cf. 66823a0066db)
bulwahn
parents:
45267
diff
changeset
|
55 |
quotient_definition insert where "insert :: 'a \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set" |
43800
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
56 |
is Set.insert |
45319
2b002c6b0f7d
renaming Quotient_Set and List_Quotient_Set to Quotient_Cset and List_Quotient_Cset to avoid name clash with existing Quotient_Set (again, cf. 66823a0066db)
bulwahn
parents:
45267
diff
changeset
|
57 |
quotient_definition remove where "remove :: 'a \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set" |
45986
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45319
diff
changeset
|
58 |
is Set.remove |
45319
2b002c6b0f7d
renaming Quotient_Set and List_Quotient_Set to Quotient_Cset and List_Quotient_Cset to avoid name clash with existing Quotient_Set (again, cf. 66823a0066db)
bulwahn
parents:
45267
diff
changeset
|
59 |
quotient_definition map where "map :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'b Quotient_Cset.set" |
43800
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
60 |
is image |
45319
2b002c6b0f7d
renaming Quotient_Set and List_Quotient_Set to Quotient_Cset and List_Quotient_Cset to avoid name clash with existing Quotient_Set (again, cf. 66823a0066db)
bulwahn
parents:
45267
diff
changeset
|
61 |
quotient_definition filter where "filter :: ('a \<Rightarrow> bool) \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set" |
45986
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45319
diff
changeset
|
62 |
is Set.project |
45319
2b002c6b0f7d
renaming Quotient_Set and List_Quotient_Set to Quotient_Cset and List_Quotient_Cset to avoid name clash with existing Quotient_Set (again, cf. 66823a0066db)
bulwahn
parents:
45267
diff
changeset
|
63 |
quotient_definition "forall :: 'a Quotient_Cset.set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" |
43800
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
64 |
is Ball |
45319
2b002c6b0f7d
renaming Quotient_Set and List_Quotient_Set to Quotient_Cset and List_Quotient_Cset to avoid name clash with existing Quotient_Set (again, cf. 66823a0066db)
bulwahn
parents:
45267
diff
changeset
|
65 |
quotient_definition "exists :: 'a Quotient_Cset.set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" |
43800
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
66 |
is Bex |
45319
2b002c6b0f7d
renaming Quotient_Set and List_Quotient_Set to Quotient_Cset and List_Quotient_Cset to avoid name clash with existing Quotient_Set (again, cf. 66823a0066db)
bulwahn
parents:
45267
diff
changeset
|
67 |
quotient_definition card where "card :: 'a Quotient_Cset.set \<Rightarrow> nat" |
43800
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
68 |
is Finite_Set.card |
45319
2b002c6b0f7d
renaming Quotient_Set and List_Quotient_Set to Quotient_Cset and List_Quotient_Cset to avoid name clash with existing Quotient_Set (again, cf. 66823a0066db)
bulwahn
parents:
45267
diff
changeset
|
69 |
quotient_definition set where "set :: 'a list => 'a Quotient_Cset.set" |
43800
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
70 |
is List.set |
45319
2b002c6b0f7d
renaming Quotient_Set and List_Quotient_Set to Quotient_Cset and List_Quotient_Cset to avoid name clash with existing Quotient_Set (again, cf. 66823a0066db)
bulwahn
parents:
45267
diff
changeset
|
71 |
quotient_definition subset where "subset :: 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> bool" |
43800
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
72 |
is "op \<subseteq> :: 'a set \<Rightarrow> 'a set \<Rightarrow> bool" |
45319
2b002c6b0f7d
renaming Quotient_Set and List_Quotient_Set to Quotient_Cset and List_Quotient_Cset to avoid name clash with existing Quotient_Set (again, cf. 66823a0066db)
bulwahn
parents:
45267
diff
changeset
|
73 |
quotient_definition psubset where "psubset :: 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> bool" |
43800
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
74 |
is "op \<subset> :: 'a set \<Rightarrow> 'a set \<Rightarrow> bool" |
45319
2b002c6b0f7d
renaming Quotient_Set and List_Quotient_Set to Quotient_Cset and List_Quotient_Cset to avoid name clash with existing Quotient_Set (again, cf. 66823a0066db)
bulwahn
parents:
45267
diff
changeset
|
75 |
quotient_definition inter where "inter :: 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set" |
43800
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
76 |
is "op \<inter> :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" |
45319
2b002c6b0f7d
renaming Quotient_Set and List_Quotient_Set to Quotient_Cset and List_Quotient_Cset to avoid name clash with existing Quotient_Set (again, cf. 66823a0066db)
bulwahn
parents:
45267
diff
changeset
|
77 |
quotient_definition union where "union :: 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set" |
43800
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
78 |
is "op \<union> :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" |
45319
2b002c6b0f7d
renaming Quotient_Set and List_Quotient_Set to Quotient_Cset and List_Quotient_Cset to avoid name clash with existing Quotient_Set (again, cf. 66823a0066db)
bulwahn
parents:
45267
diff
changeset
|
79 |
quotient_definition empty where "empty :: 'a Quotient_Cset.set" |
43800
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
80 |
is "{} :: 'a set" |
45319
2b002c6b0f7d
renaming Quotient_Set and List_Quotient_Set to Quotient_Cset and List_Quotient_Cset to avoid name clash with existing Quotient_Set (again, cf. 66823a0066db)
bulwahn
parents:
45267
diff
changeset
|
81 |
quotient_definition UNIV where "UNIV :: 'a Quotient_Cset.set" |
43800
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
82 |
is "Set.UNIV :: 'a set" |
45319
2b002c6b0f7d
renaming Quotient_Set and List_Quotient_Set to Quotient_Cset and List_Quotient_Cset to avoid name clash with existing Quotient_Set (again, cf. 66823a0066db)
bulwahn
parents:
45267
diff
changeset
|
83 |
quotient_definition uminus where "uminus :: 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set" |
43800
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
84 |
is "uminus_class.uminus :: 'a set \<Rightarrow> 'a set" |
45319
2b002c6b0f7d
renaming Quotient_Set and List_Quotient_Set to Quotient_Cset and List_Quotient_Cset to avoid name clash with existing Quotient_Set (again, cf. 66823a0066db)
bulwahn
parents:
45267
diff
changeset
|
85 |
quotient_definition minus where "minus :: 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set" |
43800
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
86 |
is "(op -) :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" |
45319
2b002c6b0f7d
renaming Quotient_Set and List_Quotient_Set to Quotient_Cset and List_Quotient_Cset to avoid name clash with existing Quotient_Set (again, cf. 66823a0066db)
bulwahn
parents:
45267
diff
changeset
|
87 |
quotient_definition Inf where "Inf :: ('a :: Inf) Quotient_Cset.set \<Rightarrow> 'a" |
44293
83c4f8ba0aa3
Quotient_Examples: Cset, List_Cset: Lift Inf and Sup directly.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
43926
diff
changeset
|
88 |
is "Inf_class.Inf :: ('a :: Inf) set \<Rightarrow> 'a" |
45319
2b002c6b0f7d
renaming Quotient_Set and List_Quotient_Set to Quotient_Cset and List_Quotient_Cset to avoid name clash with existing Quotient_Set (again, cf. 66823a0066db)
bulwahn
parents:
45267
diff
changeset
|
89 |
quotient_definition Sup where "Sup :: ('a :: Sup) Quotient_Cset.set \<Rightarrow> 'a" |
44293
83c4f8ba0aa3
Quotient_Examples: Cset, List_Cset: Lift Inf and Sup directly.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
43926
diff
changeset
|
90 |
is "Sup_class.Sup :: ('a :: Sup) set \<Rightarrow> 'a" |
45319
2b002c6b0f7d
renaming Quotient_Set and List_Quotient_Set to Quotient_Cset and List_Quotient_Cset to avoid name clash with existing Quotient_Set (again, cf. 66823a0066db)
bulwahn
parents:
45267
diff
changeset
|
91 |
quotient_definition UNION where "UNION :: 'a Quotient_Cset.set \<Rightarrow> ('a \<Rightarrow> 'b Quotient_Cset.set) \<Rightarrow> 'b Quotient_Cset.set" |
44860
56101fa00193
renamed theory Complete_Lattice to Complete_Lattices, in accordance with Lattices, Orderings etc.
haftmann
parents:
44293
diff
changeset
|
92 |
is "Complete_Lattices.UNION :: 'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" |
43800
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
93 |
|
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
94 |
hide_const (open) is_empty insert remove map filter forall exists card |
43926 | 95 |
set subset psubset inter union empty UNIV uminus minus Inf Sup UNION |
43800
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
96 |
|
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
97 |
hide_fact (open) is_empty_def insert_def remove_def map_def filter_def |
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
98 |
forall_def exists_def card_def set_def subset_def psubset_def |
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
99 |
inter_def union_def empty_def UNIV_def uminus_def minus_def Inf_def Sup_def |
44928
7ef6505bde7f
renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents:
44860
diff
changeset
|
100 |
UNION_eq |
43800
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
101 |
|
9959c8732edf
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
krauss
parents:
diff
changeset
|
102 |
end |