# HG changeset patch
# User krauss
# Date 1310565045 -7200
# Node ID 9959c8732edf7333206efc0352363d4b4b443a79
# Parent  a72661ba72390816e0233d32a86bc2e9142400ad
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package

diff -r a72661ba7239 -r 9959c8732edf src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Jul 13 04:00:32 2011 +0900
+++ b/src/HOL/IsaMakefile	Wed Jul 13 15:50:45 2011 +0200
@@ -1457,8 +1457,9 @@
 HOL-Quotient_Examples: HOL $(LOG)/HOL-Quotient_Examples.gz
 
 $(LOG)/HOL-Quotient_Examples.gz: $(OUT)/HOL				\
-  Quotient_Examples/FSet.thy Quotient_Examples/Quotient_Int.thy		\
-  Quotient_Examples/Quotient_Message.thy
+  Quotient_Examples/DList.thy Quotient_Examples/Cset.thy \
+  Quotient_Examples/FSet.thy Quotient_Examples/List_Cset.thy \
+  Quotient_Examples/Quotient_Int.thy Quotient_Examples/Quotient_Message.thy
 	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Quotient_Examples
 
 
diff -r a72661ba7239 -r 9959c8732edf src/HOL/Quotient_Examples/Cset.thy
--- /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
diff -r a72661ba7239 -r 9959c8732edf src/HOL/Quotient_Examples/List_Cset.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quotient_Examples/List_Cset.thy	Wed Jul 13 15:50:45 2011 +0200
@@ -0,0 +1,197 @@
+(*  Title:      HOL/Quotient_Examples/List_Cset.thy
+    Author:     Florian Haftmann, Alexander Krauss, TU Muenchen
+*)
+
+header {* Implementation of type Cset.set based on lists. Code equations obtained via quotient lifting. *}
+
+theory List_Cset
+imports Cset
+begin
+
+lemma [quot_respect]: "((op = ===> set_eq ===> set_eq) ===> op = ===> set_eq ===> set_eq)
+  foldr foldr"
+by (simp add: fun_rel_eq)
+
+lemma [quot_preserve]: "((id ---> abs_set ---> rep_set) ---> id ---> rep_set ---> abs_set) foldr = foldr"
+apply (rule ext)+
+by (induct_tac xa) (auto simp: Quotient_abs_rep[OF Quotient_set])
+
+
+subsection {* Relationship to lists *}
+
+(*FIXME: maybe define on sets first and then lift -> more canonical*)
+definition coset :: "'a list \<Rightarrow> 'a Cset.set" where
+  "coset xs = Cset.uminus (Cset.set xs)"
+
+code_datatype Cset.set List_Cset.coset
+
+lemma member_code [code]:
+  "member x (Cset.set xs) \<longleftrightarrow> List.member xs x"
+  "member x (coset xs) \<longleftrightarrow> \<not> List.member xs x"
+unfolding coset_def
+apply (lifting in_set_member)
+by descending (simp add: in_set_member)
+
+definition (in term_syntax)
+  setify :: "'a\<Colon>typerep list \<times> (unit \<Rightarrow> Code_Evaluation.term)
+    \<Rightarrow> 'a Cset.set \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
+  [code_unfold]: "setify xs = Code_Evaluation.valtermify Cset.set {\<cdot>} xs"
+
+notation fcomp (infixl "\<circ>>" 60)
+notation scomp (infixl "\<circ>\<rightarrow>" 60)
+
+instantiation Cset.set :: (random) random
+begin
+
+definition
+  "Quickcheck.random i = Quickcheck.random i \<circ>\<rightarrow> (\<lambda>xs. Pair (setify xs))"
+
+instance ..
+
+end
+
+no_notation fcomp (infixl "\<circ>>" 60)
+no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
+
+subsection {* Basic operations *}
+
+lemma is_empty_set [code]:
+  "Cset.is_empty (Cset.set xs) \<longleftrightarrow> List.null xs"
+  by (lifting is_empty_set)
+hide_fact (open) is_empty_set
+
+lemma empty_set [code]:
+  "Cset.empty = Cset.set []"
+  by (lifting set.simps(1)[symmetric])
+hide_fact (open) empty_set
+
+lemma UNIV_set [code]:
+  "Cset.UNIV = coset []"
+  unfolding coset_def by descending simp
+hide_fact (open) UNIV_set
+
+lemma remove_set [code]:
+  "Cset.remove x (Cset.set xs) = Cset.set (removeAll x xs)"
+  "Cset.remove x (coset xs) = coset (List.insert x xs)"
+unfolding coset_def
+apply descending
+apply (simp add: More_Set.remove_def)
+apply descending
+by (simp add: remove_set_compl)
+
+lemma insert_set [code]:
+  "Cset.insert x (Cset.set xs) = Cset.set (List.insert x xs)"
+  "Cset.insert x (coset xs) = coset (removeAll x xs)"
+unfolding coset_def
+apply (lifting set_insert[symmetric])
+by descending simp
+
+lemma map_set [code]:
+  "Cset.map f (Cset.set xs) = Cset.set (remdups (List.map f xs))"
+by descending simp
+  
+lemma filter_set [code]:
+  "Cset.filter P (Cset.set xs) = Cset.set (List.filter P xs)"
+by descending (simp add: project_set)
+
+lemma forall_set [code]:
+  "Cset.forall (Cset.set xs) P \<longleftrightarrow> list_all P xs"
+(* FIXME: why does (lifting Ball_set_list_all) fail? *)
+by descending (fact Ball_set_list_all)
+
+lemma exists_set [code]:
+  "Cset.exists (Cset.set xs) P \<longleftrightarrow> list_ex P xs"
+by descending (fact Bex_set_list_ex)
+
+lemma card_set [code]:
+  "Cset.card (Cset.set xs) = length (remdups xs)"
+by (lifting length_remdups_card_conv[symmetric])
+
+lemma compl_set [simp, code]:
+  "Cset.uminus (Cset.set xs) = coset xs"
+unfolding coset_def by descending simp
+
+lemma compl_coset [simp, code]:
+  "Cset.uminus (coset xs) = Cset.set xs"
+unfolding coset_def by descending simp
+
+context complete_lattice
+begin
+
+(* FIXME: automated lifting fails, since @{term inf} and @{term top}
+  are variables (???) *)
+lemma Infimum_inf [code]:
+  "Infimum (Cset.set As) = foldr inf As top"
+  "Infimum (coset []) = bot"
+unfolding Infimum_def member_code List.member_def
+apply (simp add: mem_def Inf_set_foldr)
+apply (simp add: Inf_UNIV[unfolded UNIV_def Collect_def])
+done
+
+lemma Supremum_sup [code]:
+  "Supremum (Cset.set As) = foldr sup As bot"
+  "Supremum (coset []) = top"
+unfolding Supremum_def member_code List.member_def
+apply (simp add: mem_def Sup_set_foldr)
+apply (simp add: Sup_UNIV[unfolded UNIV_def Collect_def])
+done
+
+end
+
+
+
+subsection {* Derived operations *}
+
+lemma subset_eq_forall [code]:
+  "Cset.subset A B \<longleftrightarrow> Cset.forall A (\<lambda>x. member x B)"
+by descending blast
+
+lemma subset_subset_eq [code]:
+  "Cset.psubset A B \<longleftrightarrow> Cset.subset A B \<and> \<not> Cset.subset B A"
+by descending blast
+
+instantiation Cset.set :: (type) equal
+begin
+
+definition [code]:
+  "HOL.equal A B \<longleftrightarrow> Cset.subset A B \<and> Cset.subset B A"
+
+instance
+apply intro_classes
+unfolding equal_set_def
+by descending auto
+
+end
+
+lemma [code nbe]:
+  "HOL.equal (A :: 'a Cset.set) A \<longleftrightarrow> True"
+  by (fact equal_refl)
+
+
+subsection {* Functorial operations *}
+
+lemma inter_project [code]:
+  "Cset.inter A (Cset.set xs) = Cset.set (List.filter (\<lambda>x. Cset.member x A) xs)"
+  "Cset.inter A (coset xs) = foldr Cset.remove xs A"
+apply descending
+apply auto
+unfolding coset_def
+apply descending
+apply simp
+by (metis diff_eq minus_set_foldr)
+
+lemma subtract_remove [code]:
+  "Cset.minus A (Cset.set xs) = foldr Cset.remove xs A"
+  "Cset.minus A (coset xs) = Cset.set (List.filter (\<lambda>x. member x A) xs)"
+unfolding coset_def
+apply (lifting minus_set_foldr)
+by descending auto
+
+lemma union_insert [code]:
+  "Cset.union (Cset.set xs) A = foldr Cset.insert xs A"
+  "Cset.union (coset xs) A = coset (List.filter (\<lambda>x. \<not> member x A) xs)"
+unfolding coset_def
+apply (lifting union_set_foldr)
+by descending auto
+
+end
\ No newline at end of file
diff -r a72661ba7239 -r 9959c8732edf src/HOL/Quotient_Examples/ROOT.ML
--- a/src/HOL/Quotient_Examples/ROOT.ML	Wed Jul 13 04:00:32 2011 +0900
+++ b/src/HOL/Quotient_Examples/ROOT.ML	Wed Jul 13 15:50:45 2011 +0200
@@ -4,5 +4,5 @@
 Testing the quotient package.
 *)
 
-use_thys ["DList", "FSet", "Quotient_Int", "Quotient_Message"];
+use_thys ["DList", "FSet", "Quotient_Int", "Quotient_Message", "Cset", "List_Cset"];