--- a/src/HOL/IsaMakefile Fri Mar 30 17:25:34 2012 +0200
+++ b/src/HOL/IsaMakefile Fri Mar 30 18:56:02 2012 +0200
@@ -448,20 +448,20 @@
Library/Efficient_Nat.thy Library/Code_Prolog.thy \
Library/Code_Real_Approx_By_Float.thy \
Tools/Predicate_Compile/code_prolog.ML Library/ContNotDenum.thy \
- Library/Cset.thy Library/Cset_Monad.thy Library/Continuity.thy \
+ Library/Continuity.thy \
Library/Convex.thy Library/Countable.thy \
- Library/Dlist.thy Library/Dlist_Cset.thy Library/Eval_Witness.thy \
- Library/DAList.thy Library/Dlist.thy Library/Dlist_Cset.thy \
+ Library/Dlist.thy Library/Eval_Witness.thy \
+ Library/DAList.thy Library/Dlist.thy \
Library/Eval_Witness.thy \
Library/Extended_Real.thy Library/Extended_Nat.thy Library/Float.thy \
Library/Formal_Power_Series.thy Library/Fraction_Field.thy \
- Library/FrechetDeriv.thy Library/Cset.thy Library/FuncSet.thy \
+ Library/FrechetDeriv.thy Library/FuncSet.thy \
Library/Function_Algebras.thy Library/Fundamental_Theorem_Algebra.thy \
Library/Glbs.thy Library/Indicator_Function.thy \
Library/Infinite_Set.thy Library/Inner_Product.thy \
Library/Kleene_Algebra.thy Library/LaTeXsugar.thy \
Library/Lattice_Algebras.thy Library/Lattice_Syntax.thy \
- Library/Library.thy Library/List_Cset.thy Library/List_Prefix.thy \
+ Library/Library.thy Library/List_Prefix.thy \
Library/List_lexord.thy Library/Mapping.thy Library/Monad_Syntax.thy \
Library/Multiset.thy Library/Nat_Bijection.thy \
Library/Numeral_Type.thy Library/Old_Recdef.thy \
@@ -1274,7 +1274,7 @@
$(OUT)/HOL-Multivariate_Analysis: $(OUT)/HOL \
Multivariate_Analysis/Brouwer_Fixpoint.thy \
- Multivariate_Analysis/Cartesian_Euclidean_Space.thy \
+ Multivariate_Analysis/Cartesian_Euclidean_Space.thy \
Multivariate_Analysis/Convex_Euclidean_Space.thy \
Multivariate_Analysis/Derivative.thy \
Multivariate_Analysis/Determinants.thy \
@@ -1313,7 +1313,7 @@
Probability/ex/Dining_Cryptographers.thy \
Probability/ex/Koepf_Duermuth_Countermeasure.thy \
Probability/Finite_Product_Measure.thy \
- Probability/Independent_Family.thy \
+ Probability/Independent_Family.thy \
Probability/Infinite_Product_Measure.thy Probability/Information.thy \
Probability/Lebesgue_Integration.thy Probability/Lebesgue_Measure.thy \
Probability/Measure.thy Probability/Probability_Measure.thy \
@@ -1617,8 +1617,8 @@
HOL-Quotient_Examples: HOL $(LOG)/HOL-Quotient_Examples.gz
$(LOG)/HOL-Quotient_Examples.gz: $(OUT)/HOL \
- Quotient_Examples/DList.thy Quotient_Examples/Quotient_Cset.thy \
- Quotient_Examples/FSet.thy Quotient_Examples/List_Quotient_Cset.thy \
+ Quotient_Examples/DList.thy \
+ Quotient_Examples/FSet.thy \
Quotient_Examples/Quotient_Int.thy Quotient_Examples/Quotient_Message.thy \
Quotient_Examples/Lift_Set.thy Quotient_Examples/Lift_RBT.thy \
Quotient_Examples/Lift_Fun.thy
--- a/src/HOL/Library/Cset.thy Fri Mar 30 17:25:34 2012 +0200
+++ b/src/HOL/Library/Cset.thy Fri Mar 30 18:56:02 2012 +0200
@@ -1,398 +0,0 @@
-
-(* Author: Florian Haftmann, TU Muenchen *)
-
-header {* A dedicated set type which is executable on its finite part *}
-
-theory Cset
-imports Main
-begin
-
-subsection {* Lifting *}
-
-typedef (open) 'a set = "UNIV :: 'a set set"
- morphisms set_of Set by rule+
-hide_type (open) set
-
-lemma set_of_Set [simp]:
- "set_of (Set A) = A"
- by (rule Set_inverse) rule
-
-lemma Set_set_of [simp]:
- "Set (set_of A) = A"
- by (fact set_of_inverse)
-
-definition member :: "'a Cset.set \<Rightarrow> 'a \<Rightarrow> bool" where
- "member A x \<longleftrightarrow> x \<in> set_of A"
-
-lemma member_Set [simp]:
- "member (Set A) x \<longleftrightarrow> x \<in> A"
- by (simp add: member_def)
-
-lemma Set_inject [simp]:
- "Set A = Set B \<longleftrightarrow> A = B"
- by (simp add: Set_inject)
-
-lemma set_eq_iff:
- "A = B \<longleftrightarrow> member A = member B"
- by (auto simp add: fun_eq_iff set_of_inject [symmetric] member_def)
-hide_fact (open) set_eq_iff
-
-lemma set_eqI:
- "member A = member B \<Longrightarrow> A = B"
- by (simp add: Cset.set_eq_iff)
-hide_fact (open) set_eqI
-
-subsection {* Lattice instantiation *}
-
-instantiation Cset.set :: (type) boolean_algebra
-begin
-
-definition less_eq_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
- [simp]: "A \<le> B \<longleftrightarrow> set_of A \<subseteq> set_of B"
-
-definition less_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
- [simp]: "A < B \<longleftrightarrow> set_of A \<subset> set_of B"
-
-definition inf_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
- [simp]: "inf A B = Set (set_of A \<inter> set_of B)"
-
-definition sup_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
- [simp]: "sup A B = Set (set_of A \<union> set_of B)"
-
-definition bot_set :: "'a Cset.set" where
- [simp]: "bot = Set {}"
-
-definition top_set :: "'a Cset.set" where
- [simp]: "top = Set UNIV"
-
-definition uminus_set :: "'a Cset.set \<Rightarrow> 'a Cset.set" where
- [simp]: "- A = Set (- (set_of A))"
-
-definition minus_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
- [simp]: "A - B = Set (set_of A - set_of B)"
-
-instance proof
-qed (auto intro!: Cset.set_eqI simp add: member_def)
-
-end
-
-instantiation Cset.set :: (type) complete_lattice
-begin
-
-definition Inf_set :: "'a Cset.set set \<Rightarrow> 'a Cset.set" where
- [simp]: "Inf_set As = Set (Inf (image set_of As))"
-
-definition Sup_set :: "'a Cset.set set \<Rightarrow> 'a Cset.set" where
- [simp]: "Sup_set As = Set (Sup (image set_of As))"
-
-instance proof
-qed (auto simp add: le_fun_def)
-
-end
-
-instance Cset.set :: (type) complete_boolean_algebra proof
-qed (unfold INF_def SUP_def, auto)
-
-
-subsection {* Basic operations *}
-
-abbreviation empty :: "'a Cset.set" where "empty \<equiv> bot"
-hide_const (open) empty
-
-abbreviation UNIV :: "'a Cset.set" where "UNIV \<equiv> top"
-hide_const (open) UNIV
-
-definition is_empty :: "'a Cset.set \<Rightarrow> bool" where
- [simp]: "is_empty A \<longleftrightarrow> Set.is_empty (set_of A)"
-
-definition insert :: "'a \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
- [simp]: "insert x A = Set (Set.insert x (set_of A))"
-
-definition remove :: "'a \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
- [simp]: "remove x A = Set (Set.remove x (set_of A))"
-
-definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a Cset.set \<Rightarrow> 'b Cset.set" where
- [simp]: "map f A = Set (image f (set_of A))"
-
-enriched_type map: map
- by (simp_all add: fun_eq_iff image_compose)
-
-definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
- [simp]: "filter P A = Set (Set.project P (set_of A))"
-
-definition forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
- [simp]: "forall P A \<longleftrightarrow> Ball (set_of A) P"
-
-definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
- [simp]: "exists P A \<longleftrightarrow> Bex (set_of A) P"
-
-definition card :: "'a Cset.set \<Rightarrow> nat" where
- [simp]: "card A = Finite_Set.card (set_of A)"
-
-context complete_lattice
-begin
-
-definition Infimum :: "'a Cset.set \<Rightarrow> 'a" where
- [simp]: "Infimum A = Inf (set_of A)"
-
-definition Supremum :: "'a Cset.set \<Rightarrow> 'a" where
- [simp]: "Supremum A = Sup (set_of A)"
-
-end
-
-subsection {* More operations *}
-
-text {* conversion from @{typ "'a list"} *}
-
-definition set :: "'a list \<Rightarrow> 'a Cset.set" where
- "set xs = Set (List.set xs)"
-hide_const (open) set
-
-definition coset :: "'a list \<Rightarrow> 'a Cset.set" where
- "coset xs = Set (- List.set xs)"
-hide_const (open) coset
-
-text {* conversion from @{typ "'a Predicate.pred"} *}
-
-definition pred_of_cset :: "'a Cset.set \<Rightarrow> 'a Predicate.pred" where
- [code del]: "pred_of_cset = Predicate.Pred \<circ> Cset.member"
-
-definition of_pred :: "'a Predicate.pred \<Rightarrow> 'a Cset.set" where
- "of_pred = Cset.Set \<circ> Collect \<circ> Predicate.eval"
-
-definition of_seq :: "'a Predicate.seq \<Rightarrow> 'a Cset.set" where
- "of_seq = of_pred \<circ> Predicate.pred_of_seq"
-
-text {* monad operations *}
-
-definition single :: "'a \<Rightarrow> 'a Cset.set" where
- "single a = Set {a}"
-
-definition bind :: "'a Cset.set \<Rightarrow> ('a \<Rightarrow> 'b Cset.set) \<Rightarrow> 'b Cset.set" (infixl "\<guillemotright>=" 70) where
- "A \<guillemotright>= f = (SUP x : set_of A. f x)"
-
-
-subsection {* Simplified simprules *}
-
-lemma empty_simp [simp]: "member Cset.empty = bot"
- by (simp add: fun_eq_iff)
-
-lemma UNIV_simp [simp]: "member Cset.UNIV = top"
- by (simp add: fun_eq_iff)
-
-lemma is_empty_simp [simp]:
- "is_empty A \<longleftrightarrow> set_of A = {}"
- by (simp add: Set.is_empty_def)
-declare is_empty_def [simp del]
-
-lemma remove_simp [simp]:
- "remove x A = Set (set_of A - {x})"
- by (simp add: Set.remove_def)
-declare remove_def [simp del]
-
-lemma filter_simp [simp]:
- "filter P A = Set {x \<in> set_of A. P x}"
- by (simp add: Set.project_def)
-declare filter_def [simp del]
-
-lemma set_of_set [simp]:
- "set_of (Cset.set xs) = set xs"
- by (simp add: set_def)
-hide_fact (open) set_def
-
-lemma member_set [simp]:
- "member (Cset.set xs) = (\<lambda>x. x \<in> set xs)"
- by (simp add: fun_eq_iff member_def)
-hide_fact (open) member_set
-
-lemma set_of_coset [simp]:
- "set_of (Cset.coset xs) = - set xs"
- by (simp add: coset_def)
-hide_fact (open) coset_def
-
-lemma member_coset [simp]:
- "member (Cset.coset xs) = (\<lambda>x. x \<in> - set xs)"
- by (simp add: fun_eq_iff member_def)
-hide_fact (open) member_coset
-
-lemma set_simps [simp]:
- "Cset.set [] = Cset.empty"
- "Cset.set (x # xs) = insert x (Cset.set xs)"
-by(simp_all add: Cset.set_def)
-
-lemma member_SUP [simp]:
- "member (SUPR A f) = SUPR A (member \<circ> f)"
- by (auto simp add: fun_eq_iff member_def, unfold SUP_def, auto)
-
-lemma member_bind [simp]:
- "member (P \<guillemotright>= f) = SUPR (set_of P) (member \<circ> f)"
- by (simp add: bind_def Cset.set_eq_iff)
-
-lemma member_single [simp]:
- "member (single a) = (\<lambda>x. x \<in> {a})"
- by (simp add: single_def fun_eq_iff)
-
-lemma single_sup_simps [simp]:
- shows single_sup: "sup (single a) A = insert a A"
- and sup_single: "sup A (single a) = insert a A"
- by (auto simp add: Cset.set_eq_iff single_def)
-
-lemma single_bind [simp]:
- "single a \<guillemotright>= B = B a"
- by (simp add: Cset.set_eq_iff SUP_insert single_def)
-
-lemma bind_bind:
- "(A \<guillemotright>= B) \<guillemotright>= C = A \<guillemotright>= (\<lambda>x. B x \<guillemotright>= C)"
- by (simp add: bind_def, simp only: SUP_def image_image, simp)
-
-lemma bind_single [simp]:
- "A \<guillemotright>= single = A"
- by (simp add: Cset.set_eq_iff fun_eq_iff single_def member_def)
-
-lemma bind_const: "A \<guillemotright>= (\<lambda>_. B) = (if Cset.is_empty A then Cset.empty else B)"
- by (auto simp add: Cset.set_eq_iff fun_eq_iff)
-
-lemma empty_bind [simp]:
- "Cset.empty \<guillemotright>= f = Cset.empty"
- by (simp add: Cset.set_eq_iff fun_eq_iff )
-
-lemma member_of_pred [simp]:
- "member (of_pred P) = (\<lambda>x. x \<in> {x. Predicate.eval P x})"
- by (simp add: of_pred_def fun_eq_iff)
-
-lemma member_of_seq [simp]:
- "member (of_seq xq) = (\<lambda>x. x \<in> {x. Predicate.member xq x})"
- by (simp add: of_seq_def eval_member)
-
-lemma eval_pred_of_cset [simp]:
- "Predicate.eval (pred_of_cset A) = Cset.member A"
- by (simp add: pred_of_cset_def)
-
-subsection {* Default implementations *}
-
-lemma set_code [code]:
- "Cset.set = (\<lambda>xs. fold insert xs Cset.empty)"
-proof (rule ext, rule Cset.set_eqI)
- fix xs :: "'a list"
- show "member (Cset.set xs) = member (fold insert xs Cset.empty)"
- by (simp add: fold_commute_apply [symmetric, where ?h = Set and ?g = Set.insert]
- fun_eq_iff Cset.set_def union_set_fold [symmetric])
-qed
-
-lemma single_code [code]:
- "single a = insert a Cset.empty"
- by (simp add: Cset.single_def)
-
-lemma compl_set [simp]:
- "- Cset.set xs = Cset.coset xs"
- by (simp add: Cset.set_def Cset.coset_def)
-
-lemma compl_coset [simp]:
- "- Cset.coset xs = Cset.set xs"
- by (simp add: Cset.set_def Cset.coset_def)
-
-lemma inter_project:
- "inf A (Cset.set xs) = Cset.set (List.filter (Cset.member A) xs)"
- "inf A (Cset.coset xs) = foldr Cset.remove xs A"
-proof -
- show "inf A (Cset.set xs) = Cset.set (List.filter (member A) xs)"
- by (simp add: project_def Cset.set_def member_def) auto
- have *: "\<And>x::'a. Cset.remove = (\<lambda>x. Set \<circ> Set.remove x \<circ> set_of)"
- by (simp add: fun_eq_iff Set.remove_def)
- have "set_of \<circ> fold (\<lambda>x. Set \<circ> Set.remove x \<circ> set_of) xs =
- fold Set.remove xs \<circ> set_of"
- by (rule fold_commute) (simp add: fun_eq_iff)
- then have "fold Set.remove xs (set_of A) =
- set_of (fold (\<lambda>x. Set \<circ> Set.remove x \<circ> set_of) xs A)"
- by (simp add: fun_eq_iff)
- then have "inf A (Cset.coset xs) = fold Cset.remove xs A"
- by (simp add: Diff_eq [symmetric] minus_set_fold *)
- moreover have "\<And>x y :: 'a. Cset.remove y \<circ> Cset.remove x = Cset.remove x \<circ> Cset.remove y"
- by (auto simp add: Set.remove_def *)
- ultimately show "inf A (Cset.coset xs) = foldr Cset.remove xs A"
- by (simp add: foldr_fold)
-qed
-
-lemma union_insert:
- "sup (Cset.set xs) A = foldr Cset.insert xs A"
- "sup (Cset.coset xs) A = Cset.coset (List.filter (Not \<circ> member A) xs)"
-proof -
- have *: "\<And>x::'a. Cset.insert = (\<lambda>x. Set \<circ> Set.insert x \<circ> set_of)"
- by (simp add: fun_eq_iff)
- have "set_of \<circ> fold (\<lambda>x. Set \<circ> Set.insert x \<circ> set_of) xs =
- fold Set.insert xs \<circ> set_of"
- by (rule fold_commute) (simp add: fun_eq_iff)
- then have "fold Set.insert xs (set_of A) =
- set_of (fold (\<lambda>x. Set \<circ> Set.insert x \<circ> set_of) xs A)"
- by (simp add: fun_eq_iff)
- then have "sup (Cset.set xs) A = fold Cset.insert xs A"
- by (simp add: union_set_fold *)
- moreover have "\<And>x y :: 'a. Cset.insert y \<circ> Cset.insert x = Cset.insert x \<circ> Cset.insert y"
- by (auto simp add: *)
- ultimately show "sup (Cset.set xs) A = foldr Cset.insert xs A"
- by (simp add: foldr_fold)
- show "sup (Cset.coset xs) A = Cset.coset (List.filter (Not \<circ> member A) xs)"
- by (auto simp add: Cset.coset_def Cset.member_def)
-qed
-
-lemma subtract_remove:
- "A - Cset.set xs = foldr Cset.remove xs A"
- "A - Cset.coset xs = Cset.set (List.filter (member A) xs)"
- by (simp_all only: diff_eq compl_set compl_coset inter_project)
-
-context complete_lattice
-begin
-
-lemma Infimum_inf:
- "Infimum (Cset.set As) = foldr inf As top"
- "Infimum (Cset.coset []) = bot"
- by (simp_all add: Inf_set_foldr)
-
-lemma Supremum_sup:
- "Supremum (Cset.set As) = foldr sup As bot"
- "Supremum (Cset.coset []) = top"
- by (simp_all add: Sup_set_foldr)
-
-end
-
-lemma of_pred_code [code]:
- "of_pred (Predicate.Seq f) = (case f () of
- Predicate.Empty \<Rightarrow> Cset.empty
- | Predicate.Insert x P \<Rightarrow> Cset.insert x (of_pred P)
- | Predicate.Join P xq \<Rightarrow> sup (of_pred P) (of_seq xq))"
- by (auto split: seq.split simp add: Predicate.Seq_def of_pred_def Cset.set_eq_iff eval_member [symmetric] member_def [symmetric])
-
-lemma of_seq_code [code]:
- "of_seq Predicate.Empty = Cset.empty"
- "of_seq (Predicate.Insert x P) = Cset.insert x (of_pred P)"
- "of_seq (Predicate.Join P xq) = sup (of_pred P) (of_seq xq)"
- by (auto simp add: of_seq_def of_pred_def Cset.set_eq_iff)
-
-lemma bind_set:
- "Cset.bind (Cset.set xs) f = fold (sup \<circ> f) xs (Cset.set [])"
- by (simp add: Cset.bind_def SUP_set_fold)
-hide_fact (open) bind_set
-
-lemma pred_of_cset_set:
- "pred_of_cset (Cset.set xs) = foldr sup (List.map Predicate.single xs) bot"
-proof -
- have "pred_of_cset (Cset.set xs) = Predicate.Pred (\<lambda>x. x \<in> set xs)"
- by (simp add: Cset.pred_of_cset_def)
- moreover have "foldr sup (List.map Predicate.single xs) bot = \<dots>"
- by (induct xs) (auto simp add: bot_pred_def intro: pred_eqI)
- ultimately show ?thesis by simp
-qed
-hide_fact (open) pred_of_cset_set
-
-no_notation bind (infixl "\<guillemotright>=" 70)
-
-hide_const (open) is_empty insert remove map filter forall exists card
- Inter Union bind single of_pred of_seq
-
-hide_fact (open) set_def pred_of_cset_def of_pred_def of_seq_def single_def
- bind_def empty_simp UNIV_simp set_simps member_bind
- member_single single_sup_simps single_sup sup_single single_bind
- bind_bind bind_single bind_const empty_bind member_of_pred member_of_seq
- eval_pred_of_cset set_code single_code of_pred_code of_seq_code
-
-end
--- a/src/HOL/Library/Cset_Monad.thy Fri Mar 30 17:25:34 2012 +0200
+++ b/src/HOL/Library/Cset_Monad.thy Fri Mar 30 18:56:02 2012 +0200
@@ -1,15 +0,0 @@
-(* Title: HOL/Library/Cset_Monad.thy
- Author: Andreas Lochbihler, Karlsruhe Institute of Technology
-*)
-
-header {* Monad notation for computable sets (cset) *}
-
-theory Cset_Monad
-imports Cset Monad_Syntax
-begin
-
-setup {*
- Adhoc_Overloading.add_variant @{const_name bind} @{const_name Cset.bind}
-*}
-
-end
\ No newline at end of file
--- a/src/HOL/Library/Dlist_Cset.thy Fri Mar 30 17:25:34 2012 +0200
+++ b/src/HOL/Library/Dlist_Cset.thy Fri Mar 30 18:56:02 2012 +0200
@@ -1,133 +0,0 @@
-(* Author: Florian Haftmann, TU Muenchen *)
-
-header {* Canonical implementation of sets by distinct lists *}
-
-theory Dlist_Cset
-imports Dlist Cset
-begin
-
-definition Set :: "'a dlist \<Rightarrow> 'a Cset.set" where
- "Set dxs = Cset.set (list_of_dlist dxs)"
-
-definition Coset :: "'a dlist \<Rightarrow> 'a Cset.set" where
- "Coset dxs = Cset.coset (list_of_dlist dxs)"
-
-code_datatype Set Coset
-
-lemma Set_Dlist [simp]:
- "Set (Dlist xs) = Cset.set xs"
- by (rule Cset.set_eqI) (simp add: Set_def)
-
-lemma Coset_Dlist [simp]:
- "Coset (Dlist xs) = Cset.coset xs"
- by (rule Cset.set_eqI) (simp add: Coset_def)
-
-lemma member_Set [simp]:
- "Cset.member (Set dxs) = List.member (list_of_dlist dxs)"
- by (simp add: Set_def fun_eq_iff List.member_def)
-
-lemma member_Coset [simp]:
- "Cset.member (Coset dxs) = Not \<circ> List.member (list_of_dlist dxs)"
- by (simp add: Coset_def fun_eq_iff List.member_def)
-
-lemma Set_dlist_of_list [code]:
- "Cset.set xs = Set (dlist_of_list xs)"
- by (rule Cset.set_eqI) simp
-
-lemma Coset_dlist_of_list [code]:
- "Cset.coset xs = Coset (dlist_of_list xs)"
- by (rule Cset.set_eqI) simp
-
-lemma is_empty_Set [code]:
- "Cset.is_empty (Set dxs) \<longleftrightarrow> Dlist.null dxs"
- by (simp add: Dlist.null_def List.null_def Set_def)
-
-lemma bot_code [code]:
- "bot = Set Dlist.empty"
- by (simp add: empty_def)
-
-lemma top_code [code]:
- "top = Coset Dlist.empty"
- by (simp add: empty_def Cset.coset_def)
-
-lemma insert_code [code]:
- "Cset.insert x (Set dxs) = Set (Dlist.insert x dxs)"
- "Cset.insert x (Coset dxs) = Coset (Dlist.remove x dxs)"
- by (simp_all add: Dlist.insert_def Dlist.remove_def Cset.set_def Cset.coset_def Set_def Coset_def)
-
-lemma remove_code [code]:
- "Cset.remove x (Set dxs) = Set (Dlist.remove x dxs)"
- "Cset.remove x (Coset dxs) = Coset (Dlist.insert x dxs)"
- by (simp_all add: Dlist.insert_def Dlist.remove_def Cset.set_def Cset.coset_def Set_def Coset_def Compl_insert)
-
-lemma member_code [code]:
- "Cset.member (Set dxs) = Dlist.member dxs"
- "Cset.member (Coset dxs) = Not \<circ> Dlist.member dxs"
- by (simp_all add: List.member_def member_def fun_eq_iff Dlist.member_def)
-
-lemma compl_code [code]:
- "- Set dxs = Coset dxs"
- "- Coset dxs = Set dxs"
- by (rule Cset.set_eqI, simp add: fun_eq_iff List.member_def Set_def Coset_def)+
-
-lemma map_code [code]:
- "Cset.map f (Set dxs) = Set (Dlist.map f dxs)"
- by (rule Cset.set_eqI) (simp add: fun_eq_iff List.member_def Set_def)
-
-lemma filter_code [code]:
- "Cset.filter f (Set dxs) = Set (Dlist.filter f dxs)"
- by (rule Cset.set_eqI) (simp add: fun_eq_iff List.member_def Set_def)
-
-lemma forall_Set [code]:
- "Cset.forall P (Set xs) \<longleftrightarrow> list_all P (list_of_dlist xs)"
- by (simp add: Set_def list_all_iff)
-
-lemma exists_Set [code]:
- "Cset.exists P (Set xs) \<longleftrightarrow> list_ex P (list_of_dlist xs)"
- by (simp add: Set_def list_ex_iff)
-
-lemma card_code [code]:
- "Cset.card (Set dxs) = Dlist.length dxs"
- by (simp add: length_def Set_def distinct_card)
-
-lemma inter_code [code]:
- "inf A (Set xs) = Set (Dlist.filter (Cset.member A) xs)"
- "inf A (Coset xs) = Dlist.foldr Cset.remove xs A"
- by (simp_all only: Set_def Coset_def foldr_def inter_project list_of_dlist_filter)
-
-lemma subtract_code [code]:
- "A - Set xs = Dlist.foldr Cset.remove xs A"
- "A - Coset xs = Set (Dlist.filter (Cset.member A) xs)"
- by (simp_all only: Set_def Coset_def foldr_def subtract_remove list_of_dlist_filter)
-
-lemma union_code [code]:
- "sup (Set xs) A = Dlist.foldr Cset.insert xs A"
- "sup (Coset xs) A = Coset (Dlist.filter (Not \<circ> Cset.member A) xs)"
- by (simp_all only: Set_def Coset_def foldr_def union_insert list_of_dlist_filter)
-
-context complete_lattice
-begin
-
-lemma Infimum_code [code]:
- "Infimum (Set As) = Dlist.foldr inf As top"
- by (simp only: Set_def Infimum_inf foldr_def inf.commute)
-
-lemma Supremum_code [code]:
- "Supremum (Set As) = Dlist.foldr sup As bot"
- by (simp only: Set_def Supremum_sup foldr_def sup.commute)
-
-end
-
-declare Cset.single_code [code]
-
-lemma bind_set [code]:
- "Cset.bind (Dlist_Cset.Set xs) f = fold (sup \<circ> f) (list_of_dlist xs) Cset.empty"
- by (simp add: Cset.bind_set Set_def)
-hide_fact (open) bind_set
-
-lemma pred_of_cset_set [code]:
- "pred_of_cset (Dlist_Cset.Set xs) = foldr sup (map Predicate.single (list_of_dlist xs)) bot"
- by (simp add: Cset.pred_of_cset_set Dlist_Cset.Set_def)
-hide_fact (open) pred_of_cset_set
-
-end
--- a/src/HOL/Library/Library.thy Fri Mar 30 17:25:34 2012 +0200
+++ b/src/HOL/Library/Library.thy Fri Mar 30 18:56:02 2012 +0200
@@ -12,15 +12,12 @@
ContNotDenum
Convex
Countable
- Cset_Monad
- Dlist_Cset
Eval_Witness
Extended_Nat
Float
Formal_Power_Series
Fraction_Field
FrechetDeriv
- Cset
FuncSet
Function_Algebras
Fundamental_Theorem_Algebra
--- a/src/HOL/Library/List_Cset.thy Fri Mar 30 17:25:34 2012 +0200
+++ b/src/HOL/Library/List_Cset.thy Fri Mar 30 18:56:02 2012 +0200
@@ -1,142 +0,0 @@
-
-(* Author: Florian Haftmann, TU Muenchen *)
-
-header {* implementation of Cset.sets based on lists *}
-
-theory List_Cset
-imports Cset
-begin
-
-code_datatype Cset.set Cset.coset
-
-lemma member_code [code]:
- "member (Cset.set xs) = List.member xs"
- "member (Cset.coset xs) = Not \<circ> List.member xs"
- by (simp_all add: fun_eq_iff List.member_def)
-
-definition (in term_syntax)
- csetify :: "'a\<Colon>typerep list \<times> (unit \<Rightarrow> Code_Evaluation.term)
- \<Rightarrow> 'a Cset.set \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
- [code_unfold]: "csetify 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 (csetify 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 (simp add: is_empty_set null_def)
-hide_fact (open) is_empty_set
-
-lemma empty_set [code]:
- "Cset.empty = Cset.set []"
- by simp
-hide_fact (open) empty_set
-
-lemma UNIV_set [code]:
- "top = Cset.coset []"
- by (simp add: Cset.coset_def)
-hide_fact (open) UNIV_set
-
-lemma remove_set [code]:
- "Cset.remove x (Cset.set xs) = Cset.set (removeAll x xs)"
- "Cset.remove x (Cset.coset xs) = Cset.coset (List.insert x xs)"
- by (simp_all add: Cset.set_def Cset.coset_def Compl_insert)
-
-lemma insert_set [code]:
- "Cset.insert x (Cset.set xs) = Cset.set (List.insert x xs)"
- "Cset.insert x (Cset.coset xs) = Cset.coset (removeAll x xs)"
- by (simp_all add: Cset.set_def Cset.coset_def)
-
-declare compl_set [code]
-declare compl_coset [code]
-declare subtract_remove [code]
-
-lemma map_set [code]:
- "Cset.map f (Cset.set xs) = Cset.set (remdups (List.map f xs))"
- by (simp add: Cset.set_def)
-
-lemma filter_set [code]:
- "Cset.filter P (Cset.set xs) = Cset.set (List.filter P xs)"
- by (simp add: Cset.set_def)
-
-lemma forall_set [code]:
- "Cset.forall P (Cset.set xs) \<longleftrightarrow> list_all P xs"
- by (simp add: Cset.set_def list_all_iff)
-
-lemma exists_set [code]:
- "Cset.exists P (Cset.set xs) \<longleftrightarrow> list_ex P xs"
- by (simp add: Cset.set_def list_ex_iff)
-
-lemma card_set [code]:
- "Cset.card (Cset.set xs) = length (remdups xs)"
-proof -
- have "Finite_Set.card (set (remdups xs)) = length (remdups xs)"
- by (rule distinct_card) simp
- then show ?thesis by (simp add: Cset.set_def)
-qed
-
-context complete_lattice
-begin
-
-declare Infimum_inf [code]
-declare Supremum_sup [code]
-
-end
-
-declare Cset.single_code [code del]
-lemma single_set [code]:
- "Cset.single a = Cset.set [a]"
-by(simp add: Cset.single_code)
-hide_fact (open) single_set
-
-declare Cset.bind_set [code]
-declare Cset.pred_of_cset_set [code]
-
-
-subsection {* Derived operations *}
-
-lemma subset_eq_forall [code]:
- "A \<le> B \<longleftrightarrow> Cset.forall (member B) A"
- by (simp add: subset_eq member_def)
-
-lemma subset_subset_eq [code]:
- "A < B \<longleftrightarrow> A \<le> B \<and> \<not> B \<le> (A :: 'a Cset.set)"
- by (fact less_le_not_le)
-
-instantiation Cset.set :: (type) equal
-begin
-
-definition [code]:
- "HOL.equal A B \<longleftrightarrow> A \<le> B \<and> B \<le> (A :: 'a Cset.set)"
-
-instance proof
-qed (auto simp add: equal_set_def Cset.set_eq_iff Cset.member_def fun_eq_iff)
-
-end
-
-lemma [code nbe]:
- "HOL.equal (A :: 'a Cset.set) A \<longleftrightarrow> True"
- by (fact equal_refl)
-
-
-subsection {* Functorial operations *}
-
-declare inter_project [code]
-declare union_insert [code]
-
-end
--- a/src/HOL/Library/ROOT.ML Fri Mar 30 17:25:34 2012 +0200
+++ b/src/HOL/Library/ROOT.ML Fri Mar 30 18:56:02 2012 +0200
@@ -1,7 +1,7 @@
(* Classical Higher-order Logic -- batteries included *)
-use_thys ["Library", "List_Cset", "List_Prefix", "List_lexord", "Sublist_Order",
+use_thys ["Library", "List_Prefix", "List_lexord", "Sublist_Order",
"Product_Lattice",
"Code_Char_chr", "Code_Char_ord", "Code_Integer", "Efficient_Nat"(*, "Code_Prolog"*),
"Code_Real_Approx_By_Float", "Target_Numeral"];
--- a/src/HOL/Quotient_Examples/List_Quotient_Cset.thy Fri Mar 30 17:25:34 2012 +0200
+++ b/src/HOL/Quotient_Examples/List_Quotient_Cset.thy Fri Mar 30 18:56:02 2012 +0200
@@ -1,191 +0,0 @@
-(* Title: HOL/Quotient_Examples/List_Quotient_Cset.thy
- Author: Florian Haftmann, Alexander Krauss, TU Muenchen
-*)
-
-header {* Implementation of type Quotient_Cset.set based on lists. Code equations obtained via quotient lifting. *}
-
-theory List_Quotient_Cset
-imports Quotient_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 Quotient_Cset.set" where
- "coset xs = Quotient_Cset.uminus (Quotient_Cset.set xs)"
-
-code_datatype Quotient_Cset.set List_Quotient_Cset.coset
-
-lemma member_code [code]:
- "member x (Quotient_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)
- csetify :: "'a\<Colon>typerep list \<times> (unit \<Rightarrow> Code_Evaluation.term)
- \<Rightarrow> 'a Quotient_Cset.set \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
- [code_unfold]: "csetify xs = Code_Evaluation.valtermify Quotient_Cset.set {\<cdot>} xs"
-
-notation fcomp (infixl "\<circ>>" 60)
-notation scomp (infixl "\<circ>\<rightarrow>" 60)
-
-instantiation Quotient_Cset.set :: (random) random
-begin
-
-definition
- "Quickcheck.random i = Quickcheck.random i \<circ>\<rightarrow> (\<lambda>xs. Pair (csetify xs))"
-
-instance ..
-
-end
-
-no_notation fcomp (infixl "\<circ>>" 60)
-no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
-
-subsection {* Basic operations *}
-
-lemma is_empty_set [code]:
- "Quotient_Cset.is_empty (Quotient_Cset.set xs) \<longleftrightarrow> List.null xs"
- by (lifting is_empty_set)
-hide_fact (open) is_empty_set
-
-lemma empty_set [code]:
- "Quotient_Cset.empty = Quotient_Cset.set []"
- by (lifting set.simps(1)[symmetric])
-hide_fact (open) empty_set
-
-lemma UNIV_set [code]:
- "Quotient_Cset.UNIV = coset []"
- unfolding coset_def by descending simp
-hide_fact (open) UNIV_set
-
-lemma remove_set [code]:
- "Quotient_Cset.remove x (Quotient_Cset.set xs) = Quotient_Cset.set (removeAll x xs)"
- "Quotient_Cset.remove x (coset xs) = coset (List.insert x xs)"
-unfolding coset_def
-apply descending
-apply (simp add: Set.remove_def)
-apply descending
-by (auto simp add: set_eq_iff)
-
-lemma insert_set [code]:
- "Quotient_Cset.insert x (Quotient_Cset.set xs) = Quotient_Cset.set (List.insert x xs)"
- "Quotient_Cset.insert x (coset xs) = coset (removeAll x xs)"
-unfolding coset_def
-apply (lifting set_insert[symmetric])
-by descending simp
-
-lemma map_set [code]:
- "Quotient_Cset.map f (Quotient_Cset.set xs) = Quotient_Cset.set (remdups (List.map f xs))"
-by descending simp
-
-lemma filter_set [code]:
- "Quotient_Cset.filter P (Quotient_Cset.set xs) = Quotient_Cset.set (List.filter P xs)"
-by descending (simp add: set_eq_iff)
-
-lemma forall_set [code]:
- "Quotient_Cset.forall (Quotient_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]:
- "Quotient_Cset.exists (Quotient_Cset.set xs) P \<longleftrightarrow> list_ex P xs"
-by descending (fact Bex_set_list_ex)
-
-lemma card_set [code]:
- "Quotient_Cset.card (Quotient_Cset.set xs) = length (remdups xs)"
-by (lifting length_remdups_card_conv[symmetric])
-
-lemma compl_set [simp, code]:
- "Quotient_Cset.uminus (Quotient_Cset.set xs) = coset xs"
-unfolding coset_def by descending simp
-
-lemma compl_coset [simp, code]:
- "Quotient_Cset.uminus (coset xs) = Quotient_Cset.set xs"
-unfolding coset_def by descending simp
-
-lemma Inf_inf [code]:
- "Quotient_Cset.Inf (Quotient_Cset.set (xs\<Colon>'a\<Colon>complete_lattice list)) = foldr inf xs top"
- "Quotient_Cset.Inf (coset ([]\<Colon>'a\<Colon>complete_lattice list)) = bot"
- unfolding List_Quotient_Cset.UNIV_set[symmetric]
- by (lifting Inf_set_foldr Inf_UNIV)
-
-lemma Sup_sup [code]:
- "Quotient_Cset.Sup (Quotient_Cset.set (xs\<Colon>'a\<Colon>complete_lattice list)) = foldr sup xs bot"
- "Quotient_Cset.Sup (coset ([]\<Colon>'a\<Colon>complete_lattice list)) = top"
- unfolding List_Quotient_Cset.UNIV_set[symmetric]
- by (lifting Sup_set_foldr Sup_UNIV)
-
-subsection {* Derived operations *}
-
-lemma subset_eq_forall [code]:
- "Quotient_Cset.subset A B \<longleftrightarrow> Quotient_Cset.forall A (\<lambda>x. member x B)"
-by descending blast
-
-lemma subset_subset_eq [code]:
- "Quotient_Cset.psubset A B \<longleftrightarrow> Quotient_Cset.subset A B \<and> \<not> Quotient_Cset.subset B A"
-by descending blast
-
-instantiation Quotient_Cset.set :: (type) equal
-begin
-
-definition [code]:
- "HOL.equal A B \<longleftrightarrow> Quotient_Cset.subset A B \<and> Quotient_Cset.subset B A"
-
-instance
-apply intro_classes
-unfolding equal_set_def
-by descending auto
-
-end
-
-lemma [code nbe]:
- "HOL.equal (A :: 'a Quotient_Cset.set) A \<longleftrightarrow> True"
- by (fact equal_refl)
-
-
-subsection {* Functorial operations *}
-
-lemma inter_project [code]:
- "Quotient_Cset.inter A (Quotient_Cset.set xs) = Quotient_Cset.set (List.filter (\<lambda>x. Quotient_Cset.member x A) xs)"
- "Quotient_Cset.inter A (coset xs) = foldr Quotient_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]:
- "Quotient_Cset.minus A (Quotient_Cset.set xs) = foldr Quotient_Cset.remove xs A"
- "Quotient_Cset.minus A (coset xs) = Quotient_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]:
- "Quotient_Cset.union (Quotient_Cset.set xs) A = foldr Quotient_Cset.insert xs A"
- "Quotient_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
-
-lemma UNION_code [code]:
- "Quotient_Cset.UNION (Quotient_Cset.set []) f = Quotient_Cset.set []"
- "Quotient_Cset.UNION (Quotient_Cset.set (x#xs)) f =
- Quotient_Cset.union (f x) (Quotient_Cset.UNION (Quotient_Cset.set xs) f)"
- by (descending, simp)+
-
-
-end
--- a/src/HOL/Quotient_Examples/Quotient_Cset.thy Fri Mar 30 17:25:34 2012 +0200
+++ b/src/HOL/Quotient_Examples/Quotient_Cset.thy Fri Mar 30 18:56:02 2012 +0200
@@ -1,77 +0,0 @@
-(* Title: HOL/Quotient_Examples/Quotient_Cset.thy
- Author: Florian Haftmann, Alexander Krauss, TU Muenchen
-*)
-
-header {* A variant of theory Cset from Library, defined as a quotient *}
-
-theory Quotient_Cset
-imports Main "~~/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 *}
-
-quotient_definition "member :: 'a => 'a Quotient_Cset.set => bool"
-is "op \<in>" by simp
-quotient_definition "Set :: ('a => bool) => 'a Quotient_Cset.set"
-is Collect done
-quotient_definition is_empty where "is_empty :: 'a Quotient_Cset.set \<Rightarrow> bool"
-is Set.is_empty by simp
-quotient_definition insert where "insert :: 'a \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set"
-is Set.insert by simp
-quotient_definition remove where "remove :: 'a \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set"
-is Set.remove by simp
-quotient_definition map where "map :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'b Quotient_Cset.set"
-is image by simp
-quotient_definition filter where "filter :: ('a \<Rightarrow> bool) \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set"
-is Set.project by simp
-quotient_definition "forall :: 'a Quotient_Cset.set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
-is Ball by simp
-quotient_definition "exists :: 'a Quotient_Cset.set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
-is Bex by simp
-quotient_definition card where "card :: 'a Quotient_Cset.set \<Rightarrow> nat"
-is Finite_Set.card by simp
-quotient_definition set where "set :: 'a list => 'a Quotient_Cset.set"
-is List.set done
-quotient_definition subset where "subset :: 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> bool"
-is "op \<subseteq> :: 'a set \<Rightarrow> 'a set \<Rightarrow> bool" by simp
-quotient_definition psubset where "psubset :: 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> bool"
-is "op \<subset> :: 'a set \<Rightarrow> 'a set \<Rightarrow> bool" by simp
-quotient_definition inter where "inter :: 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set"
-is "op \<inter> :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" by simp
-quotient_definition union where "union :: 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set"
-is "op \<union> :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" by simp
-quotient_definition empty where "empty :: 'a Quotient_Cset.set"
-is "{} :: 'a set" done
-quotient_definition UNIV where "UNIV :: 'a Quotient_Cset.set"
-is "Set.UNIV :: 'a set" done
-quotient_definition uminus where "uminus :: 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set"
-is "uminus_class.uminus :: 'a set \<Rightarrow> 'a set" by simp
-quotient_definition minus where "minus :: 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set"
-is "(op -) :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" by simp
-quotient_definition Inf where "Inf :: ('a :: Inf) Quotient_Cset.set \<Rightarrow> 'a"
-is "Inf_class.Inf :: ('a :: Inf) set \<Rightarrow> 'a" by simp
-quotient_definition Sup where "Sup :: ('a :: Sup) Quotient_Cset.set \<Rightarrow> 'a"
-is "Sup_class.Sup :: ('a :: Sup) set \<Rightarrow> 'a" by simp
-quotient_definition UNION where "UNION :: 'a Quotient_Cset.set \<Rightarrow> ('a \<Rightarrow> 'b Quotient_Cset.set) \<Rightarrow> 'b Quotient_Cset.set"
-is "Complete_Lattices.UNION :: 'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" by simp
-
-hide_const (open) is_empty insert remove map filter forall exists card
- set subset psubset inter union empty UNIV uminus minus Inf Sup UNION
-
-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
- UNION_eq
-
-end
--- a/src/HOL/Quotient_Examples/ROOT.ML Fri Mar 30 17:25:34 2012 +0200
+++ b/src/HOL/Quotient_Examples/ROOT.ML Fri Mar 30 18:56:02 2012 +0200
@@ -4,6 +4,6 @@
Testing the quotient package.
*)
-use_thys ["DList", "FSet", "Quotient_Int", "Quotient_Message", "Quotient_Cset",
- "List_Quotient_Cset", "Lift_Set", "Lift_RBT", "Lift_Fun", "Quotient_Rat"];
+use_thys ["DList", "FSet", "Quotient_Int", "Quotient_Message",
+ "Lift_Set", "Lift_RBT", "Lift_Fun", "Quotient_Rat"];