Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Quotient_Examples/Cset.thy
changeset 43800 9959c8732edf
child 43926 3264fbfd87d6 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quotient_Examples/Cset.thy	Wed Jul 13 15:50:45 2011 +0200
@@ -0,0 +1,119 @@
+(*  Title:      HOL/Quotient_Examples/Cset.thy
+    Author:     Florian Haftmann, Alexander Krauss, TU Muenchen
+*)
+
+header {* A variant of theory Cset from Library, defined as a quotient *}
+
+theory Cset
+imports "~~/src/HOL/Library/More_Set" "~~/src/HOL/Library/More_List" "~~/src/HOL/Library/Quotient_Syntax"
+begin
+
+subsection {* Lifting *}
+
+(*FIXME: quotient package requires a dedicated constant*)
+definition set_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
+where [simp]: "set_eq \<equiv> op ="
+
+quotient_type 'a set = "'a Set.set" / "set_eq"
+by (simp add: identity_equivp)
+
+hide_type (open) set
+
+subsection {* Operations *}
+
+lemma [quot_respect]:
+  "(op = ===> set_eq ===> op =) (op \<in>) (op \<in>)"
+  "(op = ===> set_eq) Collect Collect"
+  "(set_eq ===> op =) More_Set.is_empty More_Set.is_empty"
+  "(op = ===> set_eq ===> set_eq) Set.insert Set.insert"
+  "(op = ===> set_eq ===> set_eq) More_Set.remove More_Set.remove"
+  "(op = ===> set_eq ===> set_eq) image image"
+  "(op = ===> set_eq ===> set_eq) More_Set.project More_Set.project"
+  "(set_eq ===> op =) Ball Ball"
+  "(set_eq ===> op =) Bex Bex"
+  "(set_eq ===> op =) Finite_Set.card Finite_Set.card"
+  "(set_eq ===> set_eq ===> op =) (op \<subseteq>) (op \<subseteq>)"
+  "(set_eq ===> set_eq ===> op =) (op \<subset>) (op \<subset>)"
+  "(set_eq ===> set_eq ===> set_eq) (op \<inter>) (op \<inter>)"
+  "(set_eq ===> set_eq ===> set_eq) (op \<union>) (op \<union>)"
+  "set_eq {} {}"
+  "set_eq UNIV UNIV"
+  "(set_eq ===> set_eq) uminus uminus"
+  "(set_eq ===> set_eq ===> set_eq) minus minus"
+  "((set_eq ===> op =) ===> set_eq) Inf Inf"
+  "((set_eq ===> op =) ===> set_eq) Sup Sup"
+  "(op = ===> set_eq) List.set List.set"
+by (auto simp: fun_rel_eq)
+
+quotient_definition "member :: 'a => 'a Cset.set => bool"
+is "op \<in>"
+quotient_definition "Set :: ('a => bool) => 'a Cset.set"
+is Collect
+quotient_definition is_empty where "is_empty :: 'a Cset.set \<Rightarrow> bool"
+is More_Set.is_empty
+quotient_definition insert where "insert :: 'a \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set"
+is Set.insert
+quotient_definition remove where "remove :: 'a \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set"
+is More_Set.remove
+quotient_definition map where "map :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a Cset.set \<Rightarrow> 'b Cset.set"
+is image
+quotient_definition filter where "filter :: ('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set"
+is More_Set.project
+quotient_definition "forall :: 'a Cset.set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
+is Ball
+quotient_definition "exists :: 'a Cset.set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
+is Bex
+quotient_definition card where "card :: 'a Cset.set \<Rightarrow> nat"
+is Finite_Set.card
+quotient_definition set where "set :: 'a list => 'a Cset.set"
+is List.set
+quotient_definition subset where "subset :: 'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> bool"
+is "op \<subseteq> :: 'a set \<Rightarrow> 'a set \<Rightarrow> bool"
+quotient_definition psubset where "psubset :: 'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> bool"
+is "op \<subset> :: 'a set \<Rightarrow> 'a set \<Rightarrow> bool"
+quotient_definition inter where "inter :: 'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set"
+is "op \<inter> :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
+quotient_definition union where "union :: 'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set"
+is "op \<union> :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
+quotient_definition empty where "empty :: 'a Cset.set"
+is "{} :: 'a set"
+quotient_definition UNIV where "UNIV :: 'a Cset.set"
+is "Set.UNIV :: 'a set"
+quotient_definition uminus where "uminus :: 'a Cset.set \<Rightarrow> 'a Cset.set"
+is "uminus_class.uminus :: 'a set \<Rightarrow> 'a set"
+quotient_definition minus where "minus :: 'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set"
+is "(op -) :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
+quotient_definition Inf where "Inf :: 'a Cset.set set \<Rightarrow> 'a Cset.set"
+is "Inf_class.Inf :: 'a set set \<Rightarrow> 'a set"
+quotient_definition Sup where "Sup :: 'a Cset.set set \<Rightarrow> 'a Cset.set"
+is "Sup_class.Sup :: 'a set set \<Rightarrow> 'a set"
+
+
+context complete_lattice
+begin
+
+(* FIXME: Would like to use 
+
+quotient_definition "Infimum :: 'a Cset.set \<Rightarrow> 'a"
+is "Inf"
+
+but it fails, presumably because @{term "Inf"} is a Free.
+*)
+
+definition Infimum :: "'a Cset.set \<Rightarrow> 'a" where
+  [simp]: "Infimum A = Inf (\<lambda>x. member x A)"
+
+definition Supremum :: "'a Cset.set \<Rightarrow> 'a" where
+  [simp]: "Supremum A = Sup (\<lambda>x. member x A)"
+
+end
+
+hide_const (open) is_empty insert remove map filter forall exists card
+  set subset psubset inter union empty UNIV uminus minus Inf Sup
+
+hide_fact (open) is_empty_def insert_def remove_def map_def filter_def
+  forall_def exists_def card_def set_def subset_def psubset_def
+  inter_def union_def empty_def UNIV_def uminus_def minus_def Inf_def Sup_def
+
+
+end
isabelle