src/HOL/Quotient_Examples/Quotient_Cset.thy
 author haftmann Mon Dec 26 22:17:10 2011 +0100 (2011-12-26) changeset 45990 b7b905b23b2a parent 45986 c9e50153e5ae child 47092 fa3538d6004b permissions -rw-r--r--
incorporated More_Set and More_List into the Main body -- to be consolidated later
1 (*  Title:      HOL/Quotient_Examples/Quotient_Cset.thy
2     Author:     Florian Haftmann, Alexander Krauss, TU Muenchen
3 *)
5 header {* A variant of theory Cset from Library, defined as a quotient *}
7 theory Quotient_Cset
8 imports Main "~~/src/HOL/Library/Quotient_Syntax"
9 begin
11 subsection {* Lifting *}
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 ="
17 quotient_type 'a set = "'a Set.set" / "set_eq"
20 hide_type (open) set
22 subsection {* Operations *}
24 lemma [quot_respect]:
25   "(op = ===> set_eq ===> op =) (op \<in>) (op \<in>)"
26   "(op = ===> set_eq) Collect Collect"
27   "(set_eq ===> op =) Set.is_empty Set.is_empty"
28   "(op = ===> set_eq ===> set_eq) Set.insert Set.insert"
29   "(op = ===> set_eq ===> set_eq) Set.remove Set.remove"
30   "(op = ===> set_eq ===> set_eq) image image"
31   "(op = ===> set_eq ===> set_eq) Set.project 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 =) Inf Inf"
44   "(set_eq ===> op =) Sup Sup"
45   "(op = ===> set_eq) List.set List.set"
46   "(set_eq ===> (op = ===> set_eq) ===> set_eq) UNION UNION"
47 by (auto simp: fun_rel_eq)
49 quotient_definition "member :: 'a => 'a Quotient_Cset.set => bool"
50 is "op \<in>"
51 quotient_definition "Set :: ('a => bool) => 'a Quotient_Cset.set"
52 is Collect
53 quotient_definition is_empty where "is_empty :: 'a Quotient_Cset.set \<Rightarrow> bool"
54 is Set.is_empty
55 quotient_definition insert where "insert :: 'a \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set"
56 is Set.insert
57 quotient_definition remove where "remove :: 'a \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set"
58 is Set.remove
59 quotient_definition map where "map :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'b Quotient_Cset.set"
60 is image
61 quotient_definition filter where "filter :: ('a \<Rightarrow> bool) \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set"
62 is Set.project
63 quotient_definition "forall :: 'a Quotient_Cset.set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
64 is Ball
65 quotient_definition "exists :: 'a Quotient_Cset.set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
66 is Bex
67 quotient_definition card where "card :: 'a Quotient_Cset.set \<Rightarrow> nat"
68 is Finite_Set.card
69 quotient_definition set where "set :: 'a list => 'a Quotient_Cset.set"
70 is List.set
71 quotient_definition subset where "subset :: 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> bool"
72 is "op \<subseteq> :: 'a set \<Rightarrow> 'a set \<Rightarrow> bool"
73 quotient_definition psubset where "psubset :: 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> bool"
74 is "op \<subset> :: 'a set \<Rightarrow> 'a set \<Rightarrow> bool"
75 quotient_definition inter where "inter :: 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set"
76 is "op \<inter> :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
77 quotient_definition union where "union :: 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set"
78 is "op \<union> :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
79 quotient_definition empty where "empty :: 'a Quotient_Cset.set"
80 is "{} :: 'a set"
81 quotient_definition UNIV where "UNIV :: 'a Quotient_Cset.set"
82 is "Set.UNIV :: 'a set"
83 quotient_definition uminus where "uminus :: 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set"
84 is "uminus_class.uminus :: 'a set \<Rightarrow> 'a set"
85 quotient_definition minus where "minus :: 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set"
86 is "(op -) :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
87 quotient_definition Inf where "Inf :: ('a :: Inf) Quotient_Cset.set \<Rightarrow> 'a"
88 is "Inf_class.Inf :: ('a :: Inf) set \<Rightarrow> 'a"
89 quotient_definition Sup where "Sup :: ('a :: Sup) Quotient_Cset.set \<Rightarrow> 'a"
90 is "Sup_class.Sup :: ('a :: Sup) set \<Rightarrow> 'a"
91 quotient_definition UNION where "UNION :: 'a Quotient_Cset.set \<Rightarrow> ('a \<Rightarrow> 'b Quotient_Cset.set) \<Rightarrow> 'b Quotient_Cset.set"
92 is "Complete_Lattices.UNION :: 'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"
94 hide_const (open) is_empty insert remove map filter forall exists card
95   set subset psubset inter union empty UNIV uminus minus Inf Sup UNION
97 hide_fact (open) is_empty_def insert_def remove_def map_def filter_def
98   forall_def exists_def card_def set_def subset_def psubset_def
99   inter_def union_def empty_def UNIV_def uminus_def minus_def Inf_def Sup_def
100   UNION_eq
102 end