1.1 --- a/src/HOL/IsaMakefile Fri Mar 30 17:25:34 2012 +0200
1.2 +++ b/src/HOL/IsaMakefile Fri Mar 30 18:56:02 2012 +0200
1.3 @@ -448,20 +448,20 @@
1.4 Library/Efficient_Nat.thy Library/Code_Prolog.thy \
1.5 Library/Code_Real_Approx_By_Float.thy \
1.6 Tools/Predicate_Compile/code_prolog.ML Library/ContNotDenum.thy \
1.7 - Library/Cset.thy Library/Cset_Monad.thy Library/Continuity.thy \
1.8 + Library/Continuity.thy \
1.9 Library/Convex.thy Library/Countable.thy \
1.10 - Library/Dlist.thy Library/Dlist_Cset.thy Library/Eval_Witness.thy \
1.11 - Library/DAList.thy Library/Dlist.thy Library/Dlist_Cset.thy \
1.12 + Library/Dlist.thy Library/Eval_Witness.thy \
1.13 + Library/DAList.thy Library/Dlist.thy \
1.14 Library/Eval_Witness.thy \
1.15 Library/Extended_Real.thy Library/Extended_Nat.thy Library/Float.thy \
1.16 Library/Formal_Power_Series.thy Library/Fraction_Field.thy \
1.17 - Library/FrechetDeriv.thy Library/Cset.thy Library/FuncSet.thy \
1.18 + Library/FrechetDeriv.thy Library/FuncSet.thy \
1.19 Library/Function_Algebras.thy Library/Fundamental_Theorem_Algebra.thy \
1.20 Library/Glbs.thy Library/Indicator_Function.thy \
1.21 Library/Infinite_Set.thy Library/Inner_Product.thy \
1.22 Library/Kleene_Algebra.thy Library/LaTeXsugar.thy \
1.23 Library/Lattice_Algebras.thy Library/Lattice_Syntax.thy \
1.24 - Library/Library.thy Library/List_Cset.thy Library/List_Prefix.thy \
1.25 + Library/Library.thy Library/List_Prefix.thy \
1.26 Library/List_lexord.thy Library/Mapping.thy Library/Monad_Syntax.thy \
1.27 Library/Multiset.thy Library/Nat_Bijection.thy \
1.28 Library/Numeral_Type.thy Library/Old_Recdef.thy \
1.29 @@ -1274,7 +1274,7 @@
1.30
1.31 $(OUT)/HOL-Multivariate_Analysis: $(OUT)/HOL \
1.32 Multivariate_Analysis/Brouwer_Fixpoint.thy \
1.33 - Multivariate_Analysis/Cartesian_Euclidean_Space.thy \
1.34 + Multivariate_Analysis/Cartesian_Euclidean_Space.thy \
1.35 Multivariate_Analysis/Convex_Euclidean_Space.thy \
1.36 Multivariate_Analysis/Derivative.thy \
1.37 Multivariate_Analysis/Determinants.thy \
1.38 @@ -1313,7 +1313,7 @@
1.39 Probability/ex/Dining_Cryptographers.thy \
1.40 Probability/ex/Koepf_Duermuth_Countermeasure.thy \
1.41 Probability/Finite_Product_Measure.thy \
1.42 - Probability/Independent_Family.thy \
1.43 + Probability/Independent_Family.thy \
1.44 Probability/Infinite_Product_Measure.thy Probability/Information.thy \
1.45 Probability/Lebesgue_Integration.thy Probability/Lebesgue_Measure.thy \
1.46 Probability/Measure.thy Probability/Probability_Measure.thy \
1.47 @@ -1617,8 +1617,8 @@
1.48 HOL-Quotient_Examples: HOL $(LOG)/HOL-Quotient_Examples.gz
1.49
1.50 $(LOG)/HOL-Quotient_Examples.gz: $(OUT)/HOL \
1.51 - Quotient_Examples/DList.thy Quotient_Examples/Quotient_Cset.thy \
1.52 - Quotient_Examples/FSet.thy Quotient_Examples/List_Quotient_Cset.thy \
1.53 + Quotient_Examples/DList.thy \
1.54 + Quotient_Examples/FSet.thy \
1.55 Quotient_Examples/Quotient_Int.thy Quotient_Examples/Quotient_Message.thy \
1.56 Quotient_Examples/Lift_Set.thy Quotient_Examples/Lift_RBT.thy \
1.57 Quotient_Examples/Lift_Fun.thy
2.1 --- a/src/HOL/Library/Cset.thy Fri Mar 30 17:25:34 2012 +0200
2.2 +++ b/src/HOL/Library/Cset.thy Fri Mar 30 18:56:02 2012 +0200
2.3 @@ -1,398 +0,0 @@
2.4 -
2.5 -(* Author: Florian Haftmann, TU Muenchen *)
2.6 -
2.7 -header {* A dedicated set type which is executable on its finite part *}
2.8 -
2.9 -theory Cset
2.10 -imports Main
2.11 -begin
2.12 -
2.13 -subsection {* Lifting *}
2.14 -
2.15 -typedef (open) 'a set = "UNIV :: 'a set set"
2.16 - morphisms set_of Set by rule+
2.17 -hide_type (open) set
2.18 -
2.19 -lemma set_of_Set [simp]:
2.20 - "set_of (Set A) = A"
2.21 - by (rule Set_inverse) rule
2.22 -
2.23 -lemma Set_set_of [simp]:
2.24 - "Set (set_of A) = A"
2.25 - by (fact set_of_inverse)
2.26 -
2.27 -definition member :: "'a Cset.set \<Rightarrow> 'a \<Rightarrow> bool" where
2.28 - "member A x \<longleftrightarrow> x \<in> set_of A"
2.29 -
2.30 -lemma member_Set [simp]:
2.31 - "member (Set A) x \<longleftrightarrow> x \<in> A"
2.32 - by (simp add: member_def)
2.33 -
2.34 -lemma Set_inject [simp]:
2.35 - "Set A = Set B \<longleftrightarrow> A = B"
2.36 - by (simp add: Set_inject)
2.37 -
2.38 -lemma set_eq_iff:
2.39 - "A = B \<longleftrightarrow> member A = member B"
2.40 - by (auto simp add: fun_eq_iff set_of_inject [symmetric] member_def)
2.41 -hide_fact (open) set_eq_iff
2.42 -
2.43 -lemma set_eqI:
2.44 - "member A = member B \<Longrightarrow> A = B"
2.45 - by (simp add: Cset.set_eq_iff)
2.46 -hide_fact (open) set_eqI
2.47 -
2.48 -subsection {* Lattice instantiation *}
2.49 -
2.50 -instantiation Cset.set :: (type) boolean_algebra
2.51 -begin
2.52 -
2.53 -definition less_eq_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
2.54 - [simp]: "A \<le> B \<longleftrightarrow> set_of A \<subseteq> set_of B"
2.55 -
2.56 -definition less_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
2.57 - [simp]: "A < B \<longleftrightarrow> set_of A \<subset> set_of B"
2.58 -
2.59 -definition inf_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
2.60 - [simp]: "inf A B = Set (set_of A \<inter> set_of B)"
2.61 -
2.62 -definition sup_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
2.63 - [simp]: "sup A B = Set (set_of A \<union> set_of B)"
2.64 -
2.65 -definition bot_set :: "'a Cset.set" where
2.66 - [simp]: "bot = Set {}"
2.67 -
2.68 -definition top_set :: "'a Cset.set" where
2.69 - [simp]: "top = Set UNIV"
2.70 -
2.71 -definition uminus_set :: "'a Cset.set \<Rightarrow> 'a Cset.set" where
2.72 - [simp]: "- A = Set (- (set_of A))"
2.73 -
2.74 -definition minus_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
2.75 - [simp]: "A - B = Set (set_of A - set_of B)"
2.76 -
2.77 -instance proof
2.78 -qed (auto intro!: Cset.set_eqI simp add: member_def)
2.79 -
2.80 -end
2.81 -
2.82 -instantiation Cset.set :: (type) complete_lattice
2.83 -begin
2.84 -
2.85 -definition Inf_set :: "'a Cset.set set \<Rightarrow> 'a Cset.set" where
2.86 - [simp]: "Inf_set As = Set (Inf (image set_of As))"
2.87 -
2.88 -definition Sup_set :: "'a Cset.set set \<Rightarrow> 'a Cset.set" where
2.89 - [simp]: "Sup_set As = Set (Sup (image set_of As))"
2.90 -
2.91 -instance proof
2.92 -qed (auto simp add: le_fun_def)
2.93 -
2.94 -end
2.95 -
2.96 -instance Cset.set :: (type) complete_boolean_algebra proof
2.97 -qed (unfold INF_def SUP_def, auto)
2.98 -
2.99 -
2.100 -subsection {* Basic operations *}
2.101 -
2.102 -abbreviation empty :: "'a Cset.set" where "empty \<equiv> bot"
2.103 -hide_const (open) empty
2.104 -
2.105 -abbreviation UNIV :: "'a Cset.set" where "UNIV \<equiv> top"
2.106 -hide_const (open) UNIV
2.107 -
2.108 -definition is_empty :: "'a Cset.set \<Rightarrow> bool" where
2.109 - [simp]: "is_empty A \<longleftrightarrow> Set.is_empty (set_of A)"
2.110 -
2.111 -definition insert :: "'a \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
2.112 - [simp]: "insert x A = Set (Set.insert x (set_of A))"
2.113 -
2.114 -definition remove :: "'a \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
2.115 - [simp]: "remove x A = Set (Set.remove x (set_of A))"
2.116 -
2.117 -definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a Cset.set \<Rightarrow> 'b Cset.set" where
2.118 - [simp]: "map f A = Set (image f (set_of A))"
2.119 -
2.120 -enriched_type map: map
2.121 - by (simp_all add: fun_eq_iff image_compose)
2.122 -
2.123 -definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
2.124 - [simp]: "filter P A = Set (Set.project P (set_of A))"
2.125 -
2.126 -definition forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
2.127 - [simp]: "forall P A \<longleftrightarrow> Ball (set_of A) P"
2.128 -
2.129 -definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
2.130 - [simp]: "exists P A \<longleftrightarrow> Bex (set_of A) P"
2.131 -
2.132 -definition card :: "'a Cset.set \<Rightarrow> nat" where
2.133 - [simp]: "card A = Finite_Set.card (set_of A)"
2.134 -
2.135 -context complete_lattice
2.136 -begin
2.137 -
2.138 -definition Infimum :: "'a Cset.set \<Rightarrow> 'a" where
2.139 - [simp]: "Infimum A = Inf (set_of A)"
2.140 -
2.141 -definition Supremum :: "'a Cset.set \<Rightarrow> 'a" where
2.142 - [simp]: "Supremum A = Sup (set_of A)"
2.143 -
2.144 -end
2.145 -
2.146 -subsection {* More operations *}
2.147 -
2.148 -text {* conversion from @{typ "'a list"} *}
2.149 -
2.150 -definition set :: "'a list \<Rightarrow> 'a Cset.set" where
2.151 - "set xs = Set (List.set xs)"
2.152 -hide_const (open) set
2.153 -
2.154 -definition coset :: "'a list \<Rightarrow> 'a Cset.set" where
2.155 - "coset xs = Set (- List.set xs)"
2.156 -hide_const (open) coset
2.157 -
2.158 -text {* conversion from @{typ "'a Predicate.pred"} *}
2.159 -
2.160 -definition pred_of_cset :: "'a Cset.set \<Rightarrow> 'a Predicate.pred" where
2.161 - [code del]: "pred_of_cset = Predicate.Pred \<circ> Cset.member"
2.162 -
2.163 -definition of_pred :: "'a Predicate.pred \<Rightarrow> 'a Cset.set" where
2.164 - "of_pred = Cset.Set \<circ> Collect \<circ> Predicate.eval"
2.165 -
2.166 -definition of_seq :: "'a Predicate.seq \<Rightarrow> 'a Cset.set" where
2.167 - "of_seq = of_pred \<circ> Predicate.pred_of_seq"
2.168 -
2.169 -text {* monad operations *}
2.170 -
2.171 -definition single :: "'a \<Rightarrow> 'a Cset.set" where
2.172 - "single a = Set {a}"
2.173 -
2.174 -definition bind :: "'a Cset.set \<Rightarrow> ('a \<Rightarrow> 'b Cset.set) \<Rightarrow> 'b Cset.set" (infixl "\<guillemotright>=" 70) where
2.175 - "A \<guillemotright>= f = (SUP x : set_of A. f x)"
2.176 -
2.177 -
2.178 -subsection {* Simplified simprules *}
2.179 -
2.180 -lemma empty_simp [simp]: "member Cset.empty = bot"
2.181 - by (simp add: fun_eq_iff)
2.182 -
2.183 -lemma UNIV_simp [simp]: "member Cset.UNIV = top"
2.184 - by (simp add: fun_eq_iff)
2.185 -
2.186 -lemma is_empty_simp [simp]:
2.187 - "is_empty A \<longleftrightarrow> set_of A = {}"
2.188 - by (simp add: Set.is_empty_def)
2.189 -declare is_empty_def [simp del]
2.190 -
2.191 -lemma remove_simp [simp]:
2.192 - "remove x A = Set (set_of A - {x})"
2.193 - by (simp add: Set.remove_def)
2.194 -declare remove_def [simp del]
2.195 -
2.196 -lemma filter_simp [simp]:
2.197 - "filter P A = Set {x \<in> set_of A. P x}"
2.198 - by (simp add: Set.project_def)
2.199 -declare filter_def [simp del]
2.200 -
2.201 -lemma set_of_set [simp]:
2.202 - "set_of (Cset.set xs) = set xs"
2.203 - by (simp add: set_def)
2.204 -hide_fact (open) set_def
2.205 -
2.206 -lemma member_set [simp]:
2.207 - "member (Cset.set xs) = (\<lambda>x. x \<in> set xs)"
2.208 - by (simp add: fun_eq_iff member_def)
2.209 -hide_fact (open) member_set
2.210 -
2.211 -lemma set_of_coset [simp]:
2.212 - "set_of (Cset.coset xs) = - set xs"
2.213 - by (simp add: coset_def)
2.214 -hide_fact (open) coset_def
2.215 -
2.216 -lemma member_coset [simp]:
2.217 - "member (Cset.coset xs) = (\<lambda>x. x \<in> - set xs)"
2.218 - by (simp add: fun_eq_iff member_def)
2.219 -hide_fact (open) member_coset
2.220 -
2.221 -lemma set_simps [simp]:
2.222 - "Cset.set [] = Cset.empty"
2.223 - "Cset.set (x # xs) = insert x (Cset.set xs)"
2.224 -by(simp_all add: Cset.set_def)
2.225 -
2.226 -lemma member_SUP [simp]:
2.227 - "member (SUPR A f) = SUPR A (member \<circ> f)"
2.228 - by (auto simp add: fun_eq_iff member_def, unfold SUP_def, auto)
2.229 -
2.230 -lemma member_bind [simp]:
2.231 - "member (P \<guillemotright>= f) = SUPR (set_of P) (member \<circ> f)"
2.232 - by (simp add: bind_def Cset.set_eq_iff)
2.233 -
2.234 -lemma member_single [simp]:
2.235 - "member (single a) = (\<lambda>x. x \<in> {a})"
2.236 - by (simp add: single_def fun_eq_iff)
2.237 -
2.238 -lemma single_sup_simps [simp]:
2.239 - shows single_sup: "sup (single a) A = insert a A"
2.240 - and sup_single: "sup A (single a) = insert a A"
2.241 - by (auto simp add: Cset.set_eq_iff single_def)
2.242 -
2.243 -lemma single_bind [simp]:
2.244 - "single a \<guillemotright>= B = B a"
2.245 - by (simp add: Cset.set_eq_iff SUP_insert single_def)
2.246 -
2.247 -lemma bind_bind:
2.248 - "(A \<guillemotright>= B) \<guillemotright>= C = A \<guillemotright>= (\<lambda>x. B x \<guillemotright>= C)"
2.249 - by (simp add: bind_def, simp only: SUP_def image_image, simp)
2.250 -
2.251 -lemma bind_single [simp]:
2.252 - "A \<guillemotright>= single = A"
2.253 - by (simp add: Cset.set_eq_iff fun_eq_iff single_def member_def)
2.254 -
2.255 -lemma bind_const: "A \<guillemotright>= (\<lambda>_. B) = (if Cset.is_empty A then Cset.empty else B)"
2.256 - by (auto simp add: Cset.set_eq_iff fun_eq_iff)
2.257 -
2.258 -lemma empty_bind [simp]:
2.259 - "Cset.empty \<guillemotright>= f = Cset.empty"
2.260 - by (simp add: Cset.set_eq_iff fun_eq_iff )
2.261 -
2.262 -lemma member_of_pred [simp]:
2.263 - "member (of_pred P) = (\<lambda>x. x \<in> {x. Predicate.eval P x})"
2.264 - by (simp add: of_pred_def fun_eq_iff)
2.265 -
2.266 -lemma member_of_seq [simp]:
2.267 - "member (of_seq xq) = (\<lambda>x. x \<in> {x. Predicate.member xq x})"
2.268 - by (simp add: of_seq_def eval_member)
2.269 -
2.270 -lemma eval_pred_of_cset [simp]:
2.271 - "Predicate.eval (pred_of_cset A) = Cset.member A"
2.272 - by (simp add: pred_of_cset_def)
2.273 -
2.274 -subsection {* Default implementations *}
2.275 -
2.276 -lemma set_code [code]:
2.277 - "Cset.set = (\<lambda>xs. fold insert xs Cset.empty)"
2.278 -proof (rule ext, rule Cset.set_eqI)
2.279 - fix xs :: "'a list"
2.280 - show "member (Cset.set xs) = member (fold insert xs Cset.empty)"
2.281 - by (simp add: fold_commute_apply [symmetric, where ?h = Set and ?g = Set.insert]
2.282 - fun_eq_iff Cset.set_def union_set_fold [symmetric])
2.283 -qed
2.284 -
2.285 -lemma single_code [code]:
2.286 - "single a = insert a Cset.empty"
2.287 - by (simp add: Cset.single_def)
2.288 -
2.289 -lemma compl_set [simp]:
2.290 - "- Cset.set xs = Cset.coset xs"
2.291 - by (simp add: Cset.set_def Cset.coset_def)
2.292 -
2.293 -lemma compl_coset [simp]:
2.294 - "- Cset.coset xs = Cset.set xs"
2.295 - by (simp add: Cset.set_def Cset.coset_def)
2.296 -
2.297 -lemma inter_project:
2.298 - "inf A (Cset.set xs) = Cset.set (List.filter (Cset.member A) xs)"
2.299 - "inf A (Cset.coset xs) = foldr Cset.remove xs A"
2.300 -proof -
2.301 - show "inf A (Cset.set xs) = Cset.set (List.filter (member A) xs)"
2.302 - by (simp add: project_def Cset.set_def member_def) auto
2.303 - have *: "\<And>x::'a. Cset.remove = (\<lambda>x. Set \<circ> Set.remove x \<circ> set_of)"
2.304 - by (simp add: fun_eq_iff Set.remove_def)
2.305 - have "set_of \<circ> fold (\<lambda>x. Set \<circ> Set.remove x \<circ> set_of) xs =
2.306 - fold Set.remove xs \<circ> set_of"
2.307 - by (rule fold_commute) (simp add: fun_eq_iff)
2.308 - then have "fold Set.remove xs (set_of A) =
2.309 - set_of (fold (\<lambda>x. Set \<circ> Set.remove x \<circ> set_of) xs A)"
2.310 - by (simp add: fun_eq_iff)
2.311 - then have "inf A (Cset.coset xs) = fold Cset.remove xs A"
2.312 - by (simp add: Diff_eq [symmetric] minus_set_fold *)
2.313 - moreover have "\<And>x y :: 'a. Cset.remove y \<circ> Cset.remove x = Cset.remove x \<circ> Cset.remove y"
2.314 - by (auto simp add: Set.remove_def *)
2.315 - ultimately show "inf A (Cset.coset xs) = foldr Cset.remove xs A"
2.316 - by (simp add: foldr_fold)
2.317 -qed
2.318 -
2.319 -lemma union_insert:
2.320 - "sup (Cset.set xs) A = foldr Cset.insert xs A"
2.321 - "sup (Cset.coset xs) A = Cset.coset (List.filter (Not \<circ> member A) xs)"
2.322 -proof -
2.323 - have *: "\<And>x::'a. Cset.insert = (\<lambda>x. Set \<circ> Set.insert x \<circ> set_of)"
2.324 - by (simp add: fun_eq_iff)
2.325 - have "set_of \<circ> fold (\<lambda>x. Set \<circ> Set.insert x \<circ> set_of) xs =
2.326 - fold Set.insert xs \<circ> set_of"
2.327 - by (rule fold_commute) (simp add: fun_eq_iff)
2.328 - then have "fold Set.insert xs (set_of A) =
2.329 - set_of (fold (\<lambda>x. Set \<circ> Set.insert x \<circ> set_of) xs A)"
2.330 - by (simp add: fun_eq_iff)
2.331 - then have "sup (Cset.set xs) A = fold Cset.insert xs A"
2.332 - by (simp add: union_set_fold *)
2.333 - moreover have "\<And>x y :: 'a. Cset.insert y \<circ> Cset.insert x = Cset.insert x \<circ> Cset.insert y"
2.334 - by (auto simp add: *)
2.335 - ultimately show "sup (Cset.set xs) A = foldr Cset.insert xs A"
2.336 - by (simp add: foldr_fold)
2.337 - show "sup (Cset.coset xs) A = Cset.coset (List.filter (Not \<circ> member A) xs)"
2.338 - by (auto simp add: Cset.coset_def Cset.member_def)
2.339 -qed
2.340 -
2.341 -lemma subtract_remove:
2.342 - "A - Cset.set xs = foldr Cset.remove xs A"
2.343 - "A - Cset.coset xs = Cset.set (List.filter (member A) xs)"
2.344 - by (simp_all only: diff_eq compl_set compl_coset inter_project)
2.345 -
2.346 -context complete_lattice
2.347 -begin
2.348 -
2.349 -lemma Infimum_inf:
2.350 - "Infimum (Cset.set As) = foldr inf As top"
2.351 - "Infimum (Cset.coset []) = bot"
2.352 - by (simp_all add: Inf_set_foldr)
2.353 -
2.354 -lemma Supremum_sup:
2.355 - "Supremum (Cset.set As) = foldr sup As bot"
2.356 - "Supremum (Cset.coset []) = top"
2.357 - by (simp_all add: Sup_set_foldr)
2.358 -
2.359 -end
2.360 -
2.361 -lemma of_pred_code [code]:
2.362 - "of_pred (Predicate.Seq f) = (case f () of
2.363 - Predicate.Empty \<Rightarrow> Cset.empty
2.364 - | Predicate.Insert x P \<Rightarrow> Cset.insert x (of_pred P)
2.365 - | Predicate.Join P xq \<Rightarrow> sup (of_pred P) (of_seq xq))"
2.366 - by (auto split: seq.split simp add: Predicate.Seq_def of_pred_def Cset.set_eq_iff eval_member [symmetric] member_def [symmetric])
2.367 -
2.368 -lemma of_seq_code [code]:
2.369 - "of_seq Predicate.Empty = Cset.empty"
2.370 - "of_seq (Predicate.Insert x P) = Cset.insert x (of_pred P)"
2.371 - "of_seq (Predicate.Join P xq) = sup (of_pred P) (of_seq xq)"
2.372 - by (auto simp add: of_seq_def of_pred_def Cset.set_eq_iff)
2.373 -
2.374 -lemma bind_set:
2.375 - "Cset.bind (Cset.set xs) f = fold (sup \<circ> f) xs (Cset.set [])"
2.376 - by (simp add: Cset.bind_def SUP_set_fold)
2.377 -hide_fact (open) bind_set
2.378 -
2.379 -lemma pred_of_cset_set:
2.380 - "pred_of_cset (Cset.set xs) = foldr sup (List.map Predicate.single xs) bot"
2.381 -proof -
2.382 - have "pred_of_cset (Cset.set xs) = Predicate.Pred (\<lambda>x. x \<in> set xs)"
2.383 - by (simp add: Cset.pred_of_cset_def)
2.384 - moreover have "foldr sup (List.map Predicate.single xs) bot = \<dots>"
2.385 - by (induct xs) (auto simp add: bot_pred_def intro: pred_eqI)
2.386 - ultimately show ?thesis by simp
2.387 -qed
2.388 -hide_fact (open) pred_of_cset_set
2.389 -
2.390 -no_notation bind (infixl "\<guillemotright>=" 70)
2.391 -
2.392 -hide_const (open) is_empty insert remove map filter forall exists card
2.393 - Inter Union bind single of_pred of_seq
2.394 -
2.395 -hide_fact (open) set_def pred_of_cset_def of_pred_def of_seq_def single_def
2.396 - bind_def empty_simp UNIV_simp set_simps member_bind
2.397 - member_single single_sup_simps single_sup sup_single single_bind
2.398 - bind_bind bind_single bind_const empty_bind member_of_pred member_of_seq
2.399 - eval_pred_of_cset set_code single_code of_pred_code of_seq_code
2.400 -
2.401 -end
3.1 --- a/src/HOL/Library/Cset_Monad.thy Fri Mar 30 17:25:34 2012 +0200
3.2 +++ b/src/HOL/Library/Cset_Monad.thy Fri Mar 30 18:56:02 2012 +0200
3.3 @@ -1,15 +0,0 @@
3.4 -(* Title: HOL/Library/Cset_Monad.thy
3.5 - Author: Andreas Lochbihler, Karlsruhe Institute of Technology
3.6 -*)
3.7 -
3.8 -header {* Monad notation for computable sets (cset) *}
3.9 -
3.10 -theory Cset_Monad
3.11 -imports Cset Monad_Syntax
3.12 -begin
3.13 -
3.14 -setup {*
3.15 - Adhoc_Overloading.add_variant @{const_name bind} @{const_name Cset.bind}
3.16 -*}
3.17 -
3.18 -end
3.19 \ No newline at end of file
4.1 --- a/src/HOL/Library/Dlist_Cset.thy Fri Mar 30 17:25:34 2012 +0200
4.2 +++ b/src/HOL/Library/Dlist_Cset.thy Fri Mar 30 18:56:02 2012 +0200
4.3 @@ -1,133 +0,0 @@
4.4 -(* Author: Florian Haftmann, TU Muenchen *)
4.5 -
4.6 -header {* Canonical implementation of sets by distinct lists *}
4.7 -
4.8 -theory Dlist_Cset
4.9 -imports Dlist Cset
4.10 -begin
4.11 -
4.12 -definition Set :: "'a dlist \<Rightarrow> 'a Cset.set" where
4.13 - "Set dxs = Cset.set (list_of_dlist dxs)"
4.14 -
4.15 -definition Coset :: "'a dlist \<Rightarrow> 'a Cset.set" where
4.16 - "Coset dxs = Cset.coset (list_of_dlist dxs)"
4.17 -
4.18 -code_datatype Set Coset
4.19 -
4.20 -lemma Set_Dlist [simp]:
4.21 - "Set (Dlist xs) = Cset.set xs"
4.22 - by (rule Cset.set_eqI) (simp add: Set_def)
4.23 -
4.24 -lemma Coset_Dlist [simp]:
4.25 - "Coset (Dlist xs) = Cset.coset xs"
4.26 - by (rule Cset.set_eqI) (simp add: Coset_def)
4.27 -
4.28 -lemma member_Set [simp]:
4.29 - "Cset.member (Set dxs) = List.member (list_of_dlist dxs)"
4.30 - by (simp add: Set_def fun_eq_iff List.member_def)
4.31 -
4.32 -lemma member_Coset [simp]:
4.33 - "Cset.member (Coset dxs) = Not \<circ> List.member (list_of_dlist dxs)"
4.34 - by (simp add: Coset_def fun_eq_iff List.member_def)
4.35 -
4.36 -lemma Set_dlist_of_list [code]:
4.37 - "Cset.set xs = Set (dlist_of_list xs)"
4.38 - by (rule Cset.set_eqI) simp
4.39 -
4.40 -lemma Coset_dlist_of_list [code]:
4.41 - "Cset.coset xs = Coset (dlist_of_list xs)"
4.42 - by (rule Cset.set_eqI) simp
4.43 -
4.44 -lemma is_empty_Set [code]:
4.45 - "Cset.is_empty (Set dxs) \<longleftrightarrow> Dlist.null dxs"
4.46 - by (simp add: Dlist.null_def List.null_def Set_def)
4.47 -
4.48 -lemma bot_code [code]:
4.49 - "bot = Set Dlist.empty"
4.50 - by (simp add: empty_def)
4.51 -
4.52 -lemma top_code [code]:
4.53 - "top = Coset Dlist.empty"
4.54 - by (simp add: empty_def Cset.coset_def)
4.55 -
4.56 -lemma insert_code [code]:
4.57 - "Cset.insert x (Set dxs) = Set (Dlist.insert x dxs)"
4.58 - "Cset.insert x (Coset dxs) = Coset (Dlist.remove x dxs)"
4.59 - by (simp_all add: Dlist.insert_def Dlist.remove_def Cset.set_def Cset.coset_def Set_def Coset_def)
4.60 -
4.61 -lemma remove_code [code]:
4.62 - "Cset.remove x (Set dxs) = Set (Dlist.remove x dxs)"
4.63 - "Cset.remove x (Coset dxs) = Coset (Dlist.insert x dxs)"
4.64 - by (simp_all add: Dlist.insert_def Dlist.remove_def Cset.set_def Cset.coset_def Set_def Coset_def Compl_insert)
4.65 -
4.66 -lemma member_code [code]:
4.67 - "Cset.member (Set dxs) = Dlist.member dxs"
4.68 - "Cset.member (Coset dxs) = Not \<circ> Dlist.member dxs"
4.69 - by (simp_all add: List.member_def member_def fun_eq_iff Dlist.member_def)
4.70 -
4.71 -lemma compl_code [code]:
4.72 - "- Set dxs = Coset dxs"
4.73 - "- Coset dxs = Set dxs"
4.74 - by (rule Cset.set_eqI, simp add: fun_eq_iff List.member_def Set_def Coset_def)+
4.75 -
4.76 -lemma map_code [code]:
4.77 - "Cset.map f (Set dxs) = Set (Dlist.map f dxs)"
4.78 - by (rule Cset.set_eqI) (simp add: fun_eq_iff List.member_def Set_def)
4.79 -
4.80 -lemma filter_code [code]:
4.81 - "Cset.filter f (Set dxs) = Set (Dlist.filter f dxs)"
4.82 - by (rule Cset.set_eqI) (simp add: fun_eq_iff List.member_def Set_def)
4.83 -
4.84 -lemma forall_Set [code]:
4.85 - "Cset.forall P (Set xs) \<longleftrightarrow> list_all P (list_of_dlist xs)"
4.86 - by (simp add: Set_def list_all_iff)
4.87 -
4.88 -lemma exists_Set [code]:
4.89 - "Cset.exists P (Set xs) \<longleftrightarrow> list_ex P (list_of_dlist xs)"
4.90 - by (simp add: Set_def list_ex_iff)
4.91 -
4.92 -lemma card_code [code]:
4.93 - "Cset.card (Set dxs) = Dlist.length dxs"
4.94 - by (simp add: length_def Set_def distinct_card)
4.95 -
4.96 -lemma inter_code [code]:
4.97 - "inf A (Set xs) = Set (Dlist.filter (Cset.member A) xs)"
4.98 - "inf A (Coset xs) = Dlist.foldr Cset.remove xs A"
4.99 - by (simp_all only: Set_def Coset_def foldr_def inter_project list_of_dlist_filter)
4.100 -
4.101 -lemma subtract_code [code]:
4.102 - "A - Set xs = Dlist.foldr Cset.remove xs A"
4.103 - "A - Coset xs = Set (Dlist.filter (Cset.member A) xs)"
4.104 - by (simp_all only: Set_def Coset_def foldr_def subtract_remove list_of_dlist_filter)
4.105 -
4.106 -lemma union_code [code]:
4.107 - "sup (Set xs) A = Dlist.foldr Cset.insert xs A"
4.108 - "sup (Coset xs) A = Coset (Dlist.filter (Not \<circ> Cset.member A) xs)"
4.109 - by (simp_all only: Set_def Coset_def foldr_def union_insert list_of_dlist_filter)
4.110 -
4.111 -context complete_lattice
4.112 -begin
4.113 -
4.114 -lemma Infimum_code [code]:
4.115 - "Infimum (Set As) = Dlist.foldr inf As top"
4.116 - by (simp only: Set_def Infimum_inf foldr_def inf.commute)
4.117 -
4.118 -lemma Supremum_code [code]:
4.119 - "Supremum (Set As) = Dlist.foldr sup As bot"
4.120 - by (simp only: Set_def Supremum_sup foldr_def sup.commute)
4.121 -
4.122 -end
4.123 -
4.124 -declare Cset.single_code [code]
4.125 -
4.126 -lemma bind_set [code]:
4.127 - "Cset.bind (Dlist_Cset.Set xs) f = fold (sup \<circ> f) (list_of_dlist xs) Cset.empty"
4.128 - by (simp add: Cset.bind_set Set_def)
4.129 -hide_fact (open) bind_set
4.130 -
4.131 -lemma pred_of_cset_set [code]:
4.132 - "pred_of_cset (Dlist_Cset.Set xs) = foldr sup (map Predicate.single (list_of_dlist xs)) bot"
4.133 - by (simp add: Cset.pred_of_cset_set Dlist_Cset.Set_def)
4.134 -hide_fact (open) pred_of_cset_set
4.135 -
4.136 -end
5.1 --- a/src/HOL/Library/Library.thy Fri Mar 30 17:25:34 2012 +0200
5.2 +++ b/src/HOL/Library/Library.thy Fri Mar 30 18:56:02 2012 +0200
5.3 @@ -12,15 +12,12 @@
5.4 ContNotDenum
5.5 Convex
5.6 Countable
5.7 - Cset_Monad
5.8 - Dlist_Cset
5.9 Eval_Witness
5.10 Extended_Nat
5.11 Float
5.12 Formal_Power_Series
5.13 Fraction_Field
5.14 FrechetDeriv
5.15 - Cset
5.16 FuncSet
5.17 Function_Algebras
5.18 Fundamental_Theorem_Algebra
6.1 --- a/src/HOL/Library/List_Cset.thy Fri Mar 30 17:25:34 2012 +0200
6.2 +++ b/src/HOL/Library/List_Cset.thy Fri Mar 30 18:56:02 2012 +0200
6.3 @@ -1,142 +0,0 @@
6.4 -
6.5 -(* Author: Florian Haftmann, TU Muenchen *)
6.6 -
6.7 -header {* implementation of Cset.sets based on lists *}
6.8 -
6.9 -theory List_Cset
6.10 -imports Cset
6.11 -begin
6.12 -
6.13 -code_datatype Cset.set Cset.coset
6.14 -
6.15 -lemma member_code [code]:
6.16 - "member (Cset.set xs) = List.member xs"
6.17 - "member (Cset.coset xs) = Not \<circ> List.member xs"
6.18 - by (simp_all add: fun_eq_iff List.member_def)
6.19 -
6.20 -definition (in term_syntax)
6.21 - csetify :: "'a\<Colon>typerep list \<times> (unit \<Rightarrow> Code_Evaluation.term)
6.22 - \<Rightarrow> 'a Cset.set \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
6.23 - [code_unfold]: "csetify xs = Code_Evaluation.valtermify Cset.set {\<cdot>} xs"
6.24 -
6.25 -notation fcomp (infixl "\<circ>>" 60)
6.26 -notation scomp (infixl "\<circ>\<rightarrow>" 60)
6.27 -
6.28 -instantiation Cset.set :: (random) random
6.29 -begin
6.30 -
6.31 -definition
6.32 - "Quickcheck.random i = Quickcheck.random i \<circ>\<rightarrow> (\<lambda>xs. Pair (csetify xs))"
6.33 -
6.34 -instance ..
6.35 -
6.36 -end
6.37 -
6.38 -no_notation fcomp (infixl "\<circ>>" 60)
6.39 -no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
6.40 -
6.41 -subsection {* Basic operations *}
6.42 -
6.43 -lemma is_empty_set [code]:
6.44 - "Cset.is_empty (Cset.set xs) \<longleftrightarrow> List.null xs"
6.45 - by (simp add: is_empty_set null_def)
6.46 -hide_fact (open) is_empty_set
6.47 -
6.48 -lemma empty_set [code]:
6.49 - "Cset.empty = Cset.set []"
6.50 - by simp
6.51 -hide_fact (open) empty_set
6.52 -
6.53 -lemma UNIV_set [code]:
6.54 - "top = Cset.coset []"
6.55 - by (simp add: Cset.coset_def)
6.56 -hide_fact (open) UNIV_set
6.57 -
6.58 -lemma remove_set [code]:
6.59 - "Cset.remove x (Cset.set xs) = Cset.set (removeAll x xs)"
6.60 - "Cset.remove x (Cset.coset xs) = Cset.coset (List.insert x xs)"
6.61 - by (simp_all add: Cset.set_def Cset.coset_def Compl_insert)
6.62 -
6.63 -lemma insert_set [code]:
6.64 - "Cset.insert x (Cset.set xs) = Cset.set (List.insert x xs)"
6.65 - "Cset.insert x (Cset.coset xs) = Cset.coset (removeAll x xs)"
6.66 - by (simp_all add: Cset.set_def Cset.coset_def)
6.67 -
6.68 -declare compl_set [code]
6.69 -declare compl_coset [code]
6.70 -declare subtract_remove [code]
6.71 -
6.72 -lemma map_set [code]:
6.73 - "Cset.map f (Cset.set xs) = Cset.set (remdups (List.map f xs))"
6.74 - by (simp add: Cset.set_def)
6.75 -
6.76 -lemma filter_set [code]:
6.77 - "Cset.filter P (Cset.set xs) = Cset.set (List.filter P xs)"
6.78 - by (simp add: Cset.set_def)
6.79 -
6.80 -lemma forall_set [code]:
6.81 - "Cset.forall P (Cset.set xs) \<longleftrightarrow> list_all P xs"
6.82 - by (simp add: Cset.set_def list_all_iff)
6.83 -
6.84 -lemma exists_set [code]:
6.85 - "Cset.exists P (Cset.set xs) \<longleftrightarrow> list_ex P xs"
6.86 - by (simp add: Cset.set_def list_ex_iff)
6.87 -
6.88 -lemma card_set [code]:
6.89 - "Cset.card (Cset.set xs) = length (remdups xs)"
6.90 -proof -
6.91 - have "Finite_Set.card (set (remdups xs)) = length (remdups xs)"
6.92 - by (rule distinct_card) simp
6.93 - then show ?thesis by (simp add: Cset.set_def)
6.94 -qed
6.95 -
6.96 -context complete_lattice
6.97 -begin
6.98 -
6.99 -declare Infimum_inf [code]
6.100 -declare Supremum_sup [code]
6.101 -
6.102 -end
6.103 -
6.104 -declare Cset.single_code [code del]
6.105 -lemma single_set [code]:
6.106 - "Cset.single a = Cset.set [a]"
6.107 -by(simp add: Cset.single_code)
6.108 -hide_fact (open) single_set
6.109 -
6.110 -declare Cset.bind_set [code]
6.111 -declare Cset.pred_of_cset_set [code]
6.112 -
6.113 -
6.114 -subsection {* Derived operations *}
6.115 -
6.116 -lemma subset_eq_forall [code]:
6.117 - "A \<le> B \<longleftrightarrow> Cset.forall (member B) A"
6.118 - by (simp add: subset_eq member_def)
6.119 -
6.120 -lemma subset_subset_eq [code]:
6.121 - "A < B \<longleftrightarrow> A \<le> B \<and> \<not> B \<le> (A :: 'a Cset.set)"
6.122 - by (fact less_le_not_le)
6.123 -
6.124 -instantiation Cset.set :: (type) equal
6.125 -begin
6.126 -
6.127 -definition [code]:
6.128 - "HOL.equal A B \<longleftrightarrow> A \<le> B \<and> B \<le> (A :: 'a Cset.set)"
6.129 -
6.130 -instance proof
6.131 -qed (auto simp add: equal_set_def Cset.set_eq_iff Cset.member_def fun_eq_iff)
6.132 -
6.133 -end
6.134 -
6.135 -lemma [code nbe]:
6.136 - "HOL.equal (A :: 'a Cset.set) A \<longleftrightarrow> True"
6.137 - by (fact equal_refl)
6.138 -
6.139 -
6.140 -subsection {* Functorial operations *}
6.141 -
6.142 -declare inter_project [code]
6.143 -declare union_insert [code]
6.144 -
6.145 -end
7.1 --- a/src/HOL/Library/ROOT.ML Fri Mar 30 17:25:34 2012 +0200
7.2 +++ b/src/HOL/Library/ROOT.ML Fri Mar 30 18:56:02 2012 +0200
7.3 @@ -1,7 +1,7 @@
7.4
7.5 (* Classical Higher-order Logic -- batteries included *)
7.6
7.7 -use_thys ["Library", "List_Cset", "List_Prefix", "List_lexord", "Sublist_Order",
7.8 +use_thys ["Library", "List_Prefix", "List_lexord", "Sublist_Order",
7.9 "Product_Lattice",
7.10 "Code_Char_chr", "Code_Char_ord", "Code_Integer", "Efficient_Nat"(*, "Code_Prolog"*),
7.11 "Code_Real_Approx_By_Float", "Target_Numeral"];
8.1 --- a/src/HOL/Quotient_Examples/List_Quotient_Cset.thy Fri Mar 30 17:25:34 2012 +0200
8.2 +++ b/src/HOL/Quotient_Examples/List_Quotient_Cset.thy Fri Mar 30 18:56:02 2012 +0200
8.3 @@ -1,191 +0,0 @@
8.4 -(* Title: HOL/Quotient_Examples/List_Quotient_Cset.thy
8.5 - Author: Florian Haftmann, Alexander Krauss, TU Muenchen
8.6 -*)
8.7 -
8.8 -header {* Implementation of type Quotient_Cset.set based on lists. Code equations obtained via quotient lifting. *}
8.9 -
8.10 -theory List_Quotient_Cset
8.11 -imports Quotient_Cset
8.12 -begin
8.13 -
8.14 -lemma [quot_respect]: "((op = ===> set_eq ===> set_eq) ===> op = ===> set_eq ===> set_eq)
8.15 - foldr foldr"
8.16 -by (simp add: fun_rel_eq)
8.17 -
8.18 -lemma [quot_preserve]: "((id ---> abs_set ---> rep_set) ---> id ---> rep_set ---> abs_set) foldr = foldr"
8.19 -apply (rule ext)+
8.20 -by (induct_tac xa) (auto simp: Quotient_abs_rep[OF Quotient_set])
8.21 -
8.22 -
8.23 -subsection {* Relationship to lists *}
8.24 -
8.25 -(*FIXME: maybe define on sets first and then lift -> more canonical*)
8.26 -definition coset :: "'a list \<Rightarrow> 'a Quotient_Cset.set" where
8.27 - "coset xs = Quotient_Cset.uminus (Quotient_Cset.set xs)"
8.28 -
8.29 -code_datatype Quotient_Cset.set List_Quotient_Cset.coset
8.30 -
8.31 -lemma member_code [code]:
8.32 - "member x (Quotient_Cset.set xs) \<longleftrightarrow> List.member xs x"
8.33 - "member x (coset xs) \<longleftrightarrow> \<not> List.member xs x"
8.34 -unfolding coset_def
8.35 -apply (lifting in_set_member)
8.36 -by descending (simp add: in_set_member)
8.37 -
8.38 -definition (in term_syntax)
8.39 - csetify :: "'a\<Colon>typerep list \<times> (unit \<Rightarrow> Code_Evaluation.term)
8.40 - \<Rightarrow> 'a Quotient_Cset.set \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
8.41 - [code_unfold]: "csetify xs = Code_Evaluation.valtermify Quotient_Cset.set {\<cdot>} xs"
8.42 -
8.43 -notation fcomp (infixl "\<circ>>" 60)
8.44 -notation scomp (infixl "\<circ>\<rightarrow>" 60)
8.45 -
8.46 -instantiation Quotient_Cset.set :: (random) random
8.47 -begin
8.48 -
8.49 -definition
8.50 - "Quickcheck.random i = Quickcheck.random i \<circ>\<rightarrow> (\<lambda>xs. Pair (csetify xs))"
8.51 -
8.52 -instance ..
8.53 -
8.54 -end
8.55 -
8.56 -no_notation fcomp (infixl "\<circ>>" 60)
8.57 -no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
8.58 -
8.59 -subsection {* Basic operations *}
8.60 -
8.61 -lemma is_empty_set [code]:
8.62 - "Quotient_Cset.is_empty (Quotient_Cset.set xs) \<longleftrightarrow> List.null xs"
8.63 - by (lifting is_empty_set)
8.64 -hide_fact (open) is_empty_set
8.65 -
8.66 -lemma empty_set [code]:
8.67 - "Quotient_Cset.empty = Quotient_Cset.set []"
8.68 - by (lifting set.simps(1)[symmetric])
8.69 -hide_fact (open) empty_set
8.70 -
8.71 -lemma UNIV_set [code]:
8.72 - "Quotient_Cset.UNIV = coset []"
8.73 - unfolding coset_def by descending simp
8.74 -hide_fact (open) UNIV_set
8.75 -
8.76 -lemma remove_set [code]:
8.77 - "Quotient_Cset.remove x (Quotient_Cset.set xs) = Quotient_Cset.set (removeAll x xs)"
8.78 - "Quotient_Cset.remove x (coset xs) = coset (List.insert x xs)"
8.79 -unfolding coset_def
8.80 -apply descending
8.81 -apply (simp add: Set.remove_def)
8.82 -apply descending
8.83 -by (auto simp add: set_eq_iff)
8.84 -
8.85 -lemma insert_set [code]:
8.86 - "Quotient_Cset.insert x (Quotient_Cset.set xs) = Quotient_Cset.set (List.insert x xs)"
8.87 - "Quotient_Cset.insert x (coset xs) = coset (removeAll x xs)"
8.88 -unfolding coset_def
8.89 -apply (lifting set_insert[symmetric])
8.90 -by descending simp
8.91 -
8.92 -lemma map_set [code]:
8.93 - "Quotient_Cset.map f (Quotient_Cset.set xs) = Quotient_Cset.set (remdups (List.map f xs))"
8.94 -by descending simp
8.95 -
8.96 -lemma filter_set [code]:
8.97 - "Quotient_Cset.filter P (Quotient_Cset.set xs) = Quotient_Cset.set (List.filter P xs)"
8.98 -by descending (simp add: set_eq_iff)
8.99 -
8.100 -lemma forall_set [code]:
8.101 - "Quotient_Cset.forall (Quotient_Cset.set xs) P \<longleftrightarrow> list_all P xs"
8.102 -(* FIXME: why does (lifting Ball_set_list_all) fail? *)
8.103 -by descending (fact Ball_set_list_all)
8.104 -
8.105 -lemma exists_set [code]:
8.106 - "Quotient_Cset.exists (Quotient_Cset.set xs) P \<longleftrightarrow> list_ex P xs"
8.107 -by descending (fact Bex_set_list_ex)
8.108 -
8.109 -lemma card_set [code]:
8.110 - "Quotient_Cset.card (Quotient_Cset.set xs) = length (remdups xs)"
8.111 -by (lifting length_remdups_card_conv[symmetric])
8.112 -
8.113 -lemma compl_set [simp, code]:
8.114 - "Quotient_Cset.uminus (Quotient_Cset.set xs) = coset xs"
8.115 -unfolding coset_def by descending simp
8.116 -
8.117 -lemma compl_coset [simp, code]:
8.118 - "Quotient_Cset.uminus (coset xs) = Quotient_Cset.set xs"
8.119 -unfolding coset_def by descending simp
8.120 -
8.121 -lemma Inf_inf [code]:
8.122 - "Quotient_Cset.Inf (Quotient_Cset.set (xs\<Colon>'a\<Colon>complete_lattice list)) = foldr inf xs top"
8.123 - "Quotient_Cset.Inf (coset ([]\<Colon>'a\<Colon>complete_lattice list)) = bot"
8.124 - unfolding List_Quotient_Cset.UNIV_set[symmetric]
8.125 - by (lifting Inf_set_foldr Inf_UNIV)
8.126 -
8.127 -lemma Sup_sup [code]:
8.128 - "Quotient_Cset.Sup (Quotient_Cset.set (xs\<Colon>'a\<Colon>complete_lattice list)) = foldr sup xs bot"
8.129 - "Quotient_Cset.Sup (coset ([]\<Colon>'a\<Colon>complete_lattice list)) = top"
8.130 - unfolding List_Quotient_Cset.UNIV_set[symmetric]
8.131 - by (lifting Sup_set_foldr Sup_UNIV)
8.132 -
8.133 -subsection {* Derived operations *}
8.134 -
8.135 -lemma subset_eq_forall [code]:
8.136 - "Quotient_Cset.subset A B \<longleftrightarrow> Quotient_Cset.forall A (\<lambda>x. member x B)"
8.137 -by descending blast
8.138 -
8.139 -lemma subset_subset_eq [code]:
8.140 - "Quotient_Cset.psubset A B \<longleftrightarrow> Quotient_Cset.subset A B \<and> \<not> Quotient_Cset.subset B A"
8.141 -by descending blast
8.142 -
8.143 -instantiation Quotient_Cset.set :: (type) equal
8.144 -begin
8.145 -
8.146 -definition [code]:
8.147 - "HOL.equal A B \<longleftrightarrow> Quotient_Cset.subset A B \<and> Quotient_Cset.subset B A"
8.148 -
8.149 -instance
8.150 -apply intro_classes
8.151 -unfolding equal_set_def
8.152 -by descending auto
8.153 -
8.154 -end
8.155 -
8.156 -lemma [code nbe]:
8.157 - "HOL.equal (A :: 'a Quotient_Cset.set) A \<longleftrightarrow> True"
8.158 - by (fact equal_refl)
8.159 -
8.160 -
8.161 -subsection {* Functorial operations *}
8.162 -
8.163 -lemma inter_project [code]:
8.164 - "Quotient_Cset.inter A (Quotient_Cset.set xs) = Quotient_Cset.set (List.filter (\<lambda>x. Quotient_Cset.member x A) xs)"
8.165 - "Quotient_Cset.inter A (coset xs) = foldr Quotient_Cset.remove xs A"
8.166 -apply descending
8.167 -apply auto
8.168 -unfolding coset_def
8.169 -apply descending
8.170 -apply simp
8.171 -by (metis diff_eq minus_set_foldr)
8.172 -
8.173 -lemma subtract_remove [code]:
8.174 - "Quotient_Cset.minus A (Quotient_Cset.set xs) = foldr Quotient_Cset.remove xs A"
8.175 - "Quotient_Cset.minus A (coset xs) = Quotient_Cset.set (List.filter (\<lambda>x. member x A) xs)"
8.176 -unfolding coset_def
8.177 -apply (lifting minus_set_foldr)
8.178 -by descending auto
8.179 -
8.180 -lemma union_insert [code]:
8.181 - "Quotient_Cset.union (Quotient_Cset.set xs) A = foldr Quotient_Cset.insert xs A"
8.182 - "Quotient_Cset.union (coset xs) A = coset (List.filter (\<lambda>x. \<not> member x A) xs)"
8.183 -unfolding coset_def
8.184 -apply (lifting union_set_foldr)
8.185 -by descending auto
8.186 -
8.187 -lemma UNION_code [code]:
8.188 - "Quotient_Cset.UNION (Quotient_Cset.set []) f = Quotient_Cset.set []"
8.189 - "Quotient_Cset.UNION (Quotient_Cset.set (x#xs)) f =
8.190 - Quotient_Cset.union (f x) (Quotient_Cset.UNION (Quotient_Cset.set xs) f)"
8.191 - by (descending, simp)+
8.192 -
8.193 -
8.194 -end
9.1 --- a/src/HOL/Quotient_Examples/Quotient_Cset.thy Fri Mar 30 17:25:34 2012 +0200
9.2 +++ b/src/HOL/Quotient_Examples/Quotient_Cset.thy Fri Mar 30 18:56:02 2012 +0200
9.3 @@ -1,77 +0,0 @@
9.4 -(* Title: HOL/Quotient_Examples/Quotient_Cset.thy
9.5 - Author: Florian Haftmann, Alexander Krauss, TU Muenchen
9.6 -*)
9.7 -
9.8 -header {* A variant of theory Cset from Library, defined as a quotient *}
9.9 -
9.10 -theory Quotient_Cset
9.11 -imports Main "~~/src/HOL/Library/Quotient_Syntax"
9.12 -begin
9.13 -
9.14 -subsection {* Lifting *}
9.15 -
9.16 -(*FIXME: quotient package requires a dedicated constant*)
9.17 -definition set_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
9.18 -where [simp]: "set_eq \<equiv> op ="
9.19 -
9.20 -quotient_type 'a set = "'a Set.set" / "set_eq"
9.21 -by (simp add: identity_equivp)
9.22 -
9.23 -hide_type (open) set
9.24 -
9.25 -subsection {* Operations *}
9.26 -
9.27 -quotient_definition "member :: 'a => 'a Quotient_Cset.set => bool"
9.28 -is "op \<in>" by simp
9.29 -quotient_definition "Set :: ('a => bool) => 'a Quotient_Cset.set"
9.30 -is Collect done
9.31 -quotient_definition is_empty where "is_empty :: 'a Quotient_Cset.set \<Rightarrow> bool"
9.32 -is Set.is_empty by simp
9.33 -quotient_definition insert where "insert :: 'a \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set"
9.34 -is Set.insert by simp
9.35 -quotient_definition remove where "remove :: 'a \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set"
9.36 -is Set.remove by simp
9.37 -quotient_definition map where "map :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'b Quotient_Cset.set"
9.38 -is image by simp
9.39 -quotient_definition filter where "filter :: ('a \<Rightarrow> bool) \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set"
9.40 -is Set.project by simp
9.41 -quotient_definition "forall :: 'a Quotient_Cset.set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
9.42 -is Ball by simp
9.43 -quotient_definition "exists :: 'a Quotient_Cset.set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
9.44 -is Bex by simp
9.45 -quotient_definition card where "card :: 'a Quotient_Cset.set \<Rightarrow> nat"
9.46 -is Finite_Set.card by simp
9.47 -quotient_definition set where "set :: 'a list => 'a Quotient_Cset.set"
9.48 -is List.set done
9.49 -quotient_definition subset where "subset :: 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> bool"
9.50 -is "op \<subseteq> :: 'a set \<Rightarrow> 'a set \<Rightarrow> bool" by simp
9.51 -quotient_definition psubset where "psubset :: 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> bool"
9.52 -is "op \<subset> :: 'a set \<Rightarrow> 'a set \<Rightarrow> bool" by simp
9.53 -quotient_definition inter where "inter :: 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set"
9.54 -is "op \<inter> :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" by simp
9.55 -quotient_definition union where "union :: 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set"
9.56 -is "op \<union> :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" by simp
9.57 -quotient_definition empty where "empty :: 'a Quotient_Cset.set"
9.58 -is "{} :: 'a set" done
9.59 -quotient_definition UNIV where "UNIV :: 'a Quotient_Cset.set"
9.60 -is "Set.UNIV :: 'a set" done
9.61 -quotient_definition uminus where "uminus :: 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set"
9.62 -is "uminus_class.uminus :: 'a set \<Rightarrow> 'a set" by simp
9.63 -quotient_definition minus where "minus :: 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set"
9.64 -is "(op -) :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" by simp
9.65 -quotient_definition Inf where "Inf :: ('a :: Inf) Quotient_Cset.set \<Rightarrow> 'a"
9.66 -is "Inf_class.Inf :: ('a :: Inf) set \<Rightarrow> 'a" by simp
9.67 -quotient_definition Sup where "Sup :: ('a :: Sup) Quotient_Cset.set \<Rightarrow> 'a"
9.68 -is "Sup_class.Sup :: ('a :: Sup) set \<Rightarrow> 'a" by simp
9.69 -quotient_definition UNION where "UNION :: 'a Quotient_Cset.set \<Rightarrow> ('a \<Rightarrow> 'b Quotient_Cset.set) \<Rightarrow> 'b Quotient_Cset.set"
9.70 -is "Complete_Lattices.UNION :: 'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" by simp
9.71 -
9.72 -hide_const (open) is_empty insert remove map filter forall exists card
9.73 - set subset psubset inter union empty UNIV uminus minus Inf Sup UNION
9.74 -
9.75 -hide_fact (open) is_empty_def insert_def remove_def map_def filter_def
9.76 - forall_def exists_def card_def set_def subset_def psubset_def
9.77 - inter_def union_def empty_def UNIV_def uminus_def minus_def Inf_def Sup_def
9.78 - UNION_eq
9.79 -
9.80 -end
10.1 --- a/src/HOL/Quotient_Examples/ROOT.ML Fri Mar 30 17:25:34 2012 +0200
10.2 +++ b/src/HOL/Quotient_Examples/ROOT.ML Fri Mar 30 18:56:02 2012 +0200
10.3 @@ -4,6 +4,6 @@
10.4 Testing the quotient package.
10.5 *)
10.6
10.7 -use_thys ["DList", "FSet", "Quotient_Int", "Quotient_Message", "Quotient_Cset",
10.8 - "List_Quotient_Cset", "Lift_Set", "Lift_RBT", "Lift_Fun", "Quotient_Rat"];
10.9 +use_thys ["DList", "FSet", "Quotient_Int", "Quotient_Message",
10.10 + "Lift_Set", "Lift_RBT", "Lift_Fun", "Quotient_Rat"];
10.11