# HG changeset patch # User haftmann # Date 1333126562 -7200 # Node ID e2f0176149d0633438bd6c2fb887beaad7e25437 # Parent 3ff8c79a9e2f15033d78e242aea1e554bc4f0849 dropped now obsolete Cset theories diff -r 3ff8c79a9e2f -r e2f0176149d0 src/HOL/IsaMakefile --- 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 diff -r 3ff8c79a9e2f -r e2f0176149d0 src/HOL/Library/Cset.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 \ 'a \ bool" where - "member A x \ x \ set_of A" - -lemma member_Set [simp]: - "member (Set A) x \ x \ A" - by (simp add: member_def) - -lemma Set_inject [simp]: - "Set A = Set B \ A = B" - by (simp add: Set_inject) - -lemma set_eq_iff: - "A = B \ 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 \ 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 \ 'a Cset.set \ bool" where - [simp]: "A \ B \ set_of A \ set_of B" - -definition less_set :: "'a Cset.set \ 'a Cset.set \ bool" where - [simp]: "A < B \ set_of A \ set_of B" - -definition inf_set :: "'a Cset.set \ 'a Cset.set \ 'a Cset.set" where - [simp]: "inf A B = Set (set_of A \ set_of B)" - -definition sup_set :: "'a Cset.set \ 'a Cset.set \ 'a Cset.set" where - [simp]: "sup A B = Set (set_of A \ 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 \ 'a Cset.set" where - [simp]: "- A = Set (- (set_of A))" - -definition minus_set :: "'a Cset.set \ 'a Cset.set \ '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 \ 'a Cset.set" where - [simp]: "Inf_set As = Set (Inf (image set_of As))" - -definition Sup_set :: "'a Cset.set set \ '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 \ bot" -hide_const (open) empty - -abbreviation UNIV :: "'a Cset.set" where "UNIV \ top" -hide_const (open) UNIV - -definition is_empty :: "'a Cset.set \ bool" where - [simp]: "is_empty A \ Set.is_empty (set_of A)" - -definition insert :: "'a \ 'a Cset.set \ 'a Cset.set" where - [simp]: "insert x A = Set (Set.insert x (set_of A))" - -definition remove :: "'a \ 'a Cset.set \ 'a Cset.set" where - [simp]: "remove x A = Set (Set.remove x (set_of A))" - -definition map :: "('a \ 'b) \ 'a Cset.set \ '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 \ bool) \ 'a Cset.set \ 'a Cset.set" where - [simp]: "filter P A = Set (Set.project P (set_of A))" - -definition forall :: "('a \ bool) \ 'a Cset.set \ bool" where - [simp]: "forall P A \ Ball (set_of A) P" - -definition exists :: "('a \ bool) \ 'a Cset.set \ bool" where - [simp]: "exists P A \ Bex (set_of A) P" - -definition card :: "'a Cset.set \ nat" where - [simp]: "card A = Finite_Set.card (set_of A)" - -context complete_lattice -begin - -definition Infimum :: "'a Cset.set \ 'a" where - [simp]: "Infimum A = Inf (set_of A)" - -definition Supremum :: "'a Cset.set \ 'a" where - [simp]: "Supremum A = Sup (set_of A)" - -end - -subsection {* More operations *} - -text {* conversion from @{typ "'a list"} *} - -definition set :: "'a list \ 'a Cset.set" where - "set xs = Set (List.set xs)" -hide_const (open) set - -definition coset :: "'a list \ '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 \ 'a Predicate.pred" where - [code del]: "pred_of_cset = Predicate.Pred \ Cset.member" - -definition of_pred :: "'a Predicate.pred \ 'a Cset.set" where - "of_pred = Cset.Set \ Collect \ Predicate.eval" - -definition of_seq :: "'a Predicate.seq \ 'a Cset.set" where - "of_seq = of_pred \ Predicate.pred_of_seq" - -text {* monad operations *} - -definition single :: "'a \ 'a Cset.set" where - "single a = Set {a}" - -definition bind :: "'a Cset.set \ ('a \ 'b Cset.set) \ 'b Cset.set" (infixl "\=" 70) where - "A \= 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 \ 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 \ 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) = (\x. x \ 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) = (\x. x \ - 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 \ f)" - by (auto simp add: fun_eq_iff member_def, unfold SUP_def, auto) - -lemma member_bind [simp]: - "member (P \= f) = SUPR (set_of P) (member \ f)" - by (simp add: bind_def Cset.set_eq_iff) - -lemma member_single [simp]: - "member (single a) = (\x. x \ {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 \= B = B a" - by (simp add: Cset.set_eq_iff SUP_insert single_def) - -lemma bind_bind: - "(A \= B) \= C = A \= (\x. B x \= C)" - by (simp add: bind_def, simp only: SUP_def image_image, simp) - -lemma bind_single [simp]: - "A \= single = A" - by (simp add: Cset.set_eq_iff fun_eq_iff single_def member_def) - -lemma bind_const: "A \= (\_. 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 \= f = Cset.empty" - by (simp add: Cset.set_eq_iff fun_eq_iff ) - -lemma member_of_pred [simp]: - "member (of_pred P) = (\x. x \ {x. Predicate.eval P x})" - by (simp add: of_pred_def fun_eq_iff) - -lemma member_of_seq [simp]: - "member (of_seq xq) = (\x. x \ {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 = (\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 *: "\x::'a. Cset.remove = (\x. Set \ Set.remove x \ set_of)" - by (simp add: fun_eq_iff Set.remove_def) - have "set_of \ fold (\x. Set \ Set.remove x \ set_of) xs = - fold Set.remove xs \ set_of" - by (rule fold_commute) (simp add: fun_eq_iff) - then have "fold Set.remove xs (set_of A) = - set_of (fold (\x. Set \ Set.remove x \ 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 "\x y :: 'a. Cset.remove y \ Cset.remove x = Cset.remove x \ 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 \ member A) xs)" -proof - - have *: "\x::'a. Cset.insert = (\x. Set \ Set.insert x \ set_of)" - by (simp add: fun_eq_iff) - have "set_of \ fold (\x. Set \ Set.insert x \ set_of) xs = - fold Set.insert xs \ set_of" - by (rule fold_commute) (simp add: fun_eq_iff) - then have "fold Set.insert xs (set_of A) = - set_of (fold (\x. Set \ Set.insert x \ 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 "\x y :: 'a. Cset.insert y \ Cset.insert x = Cset.insert x \ 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 \ 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 \ Cset.empty - | Predicate.Insert x P \ Cset.insert x (of_pred P) - | Predicate.Join P xq \ 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 \ 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 (\x. x \ set xs)" - by (simp add: Cset.pred_of_cset_def) - moreover have "foldr sup (List.map Predicate.single xs) bot = \" - 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 "\=" 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 diff -r 3ff8c79a9e2f -r e2f0176149d0 src/HOL/Library/Cset_Monad.thy --- 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 diff -r 3ff8c79a9e2f -r e2f0176149d0 src/HOL/Library/Dlist_Cset.thy --- 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 \ 'a Cset.set" where - "Set dxs = Cset.set (list_of_dlist dxs)" - -definition Coset :: "'a dlist \ '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 \ 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) \ 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 \ 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) \ list_all P (list_of_dlist xs)" - by (simp add: Set_def list_all_iff) - -lemma exists_Set [code]: - "Cset.exists P (Set xs) \ 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 \ 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 \ 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 diff -r 3ff8c79a9e2f -r e2f0176149d0 src/HOL/Library/Library.thy --- 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 diff -r 3ff8c79a9e2f -r e2f0176149d0 src/HOL/Library/List_Cset.thy --- 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 \ List.member xs" - by (simp_all add: fun_eq_iff List.member_def) - -definition (in term_syntax) - csetify :: "'a\typerep list \ (unit \ Code_Evaluation.term) - \ 'a Cset.set \ (unit \ Code_Evaluation.term)" where - [code_unfold]: "csetify xs = Code_Evaluation.valtermify Cset.set {\} xs" - -notation fcomp (infixl "\>" 60) -notation scomp (infixl "\\" 60) - -instantiation Cset.set :: (random) random -begin - -definition - "Quickcheck.random i = Quickcheck.random i \\ (\xs. Pair (csetify xs))" - -instance .. - -end - -no_notation fcomp (infixl "\>" 60) -no_notation scomp (infixl "\\" 60) - -subsection {* Basic operations *} - -lemma is_empty_set [code]: - "Cset.is_empty (Cset.set xs) \ 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) \ list_all P xs" - by (simp add: Cset.set_def list_all_iff) - -lemma exists_set [code]: - "Cset.exists P (Cset.set xs) \ 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 \ B \ Cset.forall (member B) A" - by (simp add: subset_eq member_def) - -lemma subset_subset_eq [code]: - "A < B \ A \ B \ \ B \ (A :: 'a Cset.set)" - by (fact less_le_not_le) - -instantiation Cset.set :: (type) equal -begin - -definition [code]: - "HOL.equal A B \ A \ B \ B \ (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 \ True" - by (fact equal_refl) - - -subsection {* Functorial operations *} - -declare inter_project [code] -declare union_insert [code] - -end diff -r 3ff8c79a9e2f -r e2f0176149d0 src/HOL/Library/ROOT.ML --- 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"]; diff -r 3ff8c79a9e2f -r e2f0176149d0 src/HOL/Quotient_Examples/List_Quotient_Cset.thy --- 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 \ '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) \ List.member xs x" - "member x (coset xs) \ \ 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\typerep list \ (unit \ Code_Evaluation.term) - \ 'a Quotient_Cset.set \ (unit \ Code_Evaluation.term)" where - [code_unfold]: "csetify xs = Code_Evaluation.valtermify Quotient_Cset.set {\} xs" - -notation fcomp (infixl "\>" 60) -notation scomp (infixl "\\" 60) - -instantiation Quotient_Cset.set :: (random) random -begin - -definition - "Quickcheck.random i = Quickcheck.random i \\ (\xs. Pair (csetify xs))" - -instance .. - -end - -no_notation fcomp (infixl "\>" 60) -no_notation scomp (infixl "\\" 60) - -subsection {* Basic operations *} - -lemma is_empty_set [code]: - "Quotient_Cset.is_empty (Quotient_Cset.set xs) \ 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 \ 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 \ 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\'a\complete_lattice list)) = foldr inf xs top" - "Quotient_Cset.Inf (coset ([]\'a\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\'a\complete_lattice list)) = foldr sup xs bot" - "Quotient_Cset.Sup (coset ([]\'a\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 \ Quotient_Cset.forall A (\x. member x B)" -by descending blast - -lemma subset_subset_eq [code]: - "Quotient_Cset.psubset A B \ Quotient_Cset.subset A B \ \ Quotient_Cset.subset B A" -by descending blast - -instantiation Quotient_Cset.set :: (type) equal -begin - -definition [code]: - "HOL.equal A B \ Quotient_Cset.subset A B \ 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 \ 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 (\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 (\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 (\x. \ 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 diff -r 3ff8c79a9e2f -r e2f0176149d0 src/HOL/Quotient_Examples/Quotient_Cset.thy --- 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 \ 'a set \ bool" -where [simp]: "set_eq \ 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 \" 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 \ bool" -is Set.is_empty by simp -quotient_definition insert where "insert :: 'a \ 'a Quotient_Cset.set \ 'a Quotient_Cset.set" -is Set.insert by simp -quotient_definition remove where "remove :: 'a \ 'a Quotient_Cset.set \ 'a Quotient_Cset.set" -is Set.remove by simp -quotient_definition map where "map :: ('a \ 'b) \ 'a Quotient_Cset.set \ 'b Quotient_Cset.set" -is image by simp -quotient_definition filter where "filter :: ('a \ bool) \ 'a Quotient_Cset.set \ 'a Quotient_Cset.set" -is Set.project by simp -quotient_definition "forall :: 'a Quotient_Cset.set \ ('a \ bool) \ bool" -is Ball by simp -quotient_definition "exists :: 'a Quotient_Cset.set \ ('a \ bool) \ bool" -is Bex by simp -quotient_definition card where "card :: 'a Quotient_Cset.set \ 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 \ 'a Quotient_Cset.set \ bool" -is "op \ :: 'a set \ 'a set \ bool" by simp -quotient_definition psubset where "psubset :: 'a Quotient_Cset.set \ 'a Quotient_Cset.set \ bool" -is "op \ :: 'a set \ 'a set \ bool" by simp -quotient_definition inter where "inter :: 'a Quotient_Cset.set \ 'a Quotient_Cset.set \ 'a Quotient_Cset.set" -is "op \ :: 'a set \ 'a set \ 'a set" by simp -quotient_definition union where "union :: 'a Quotient_Cset.set \ 'a Quotient_Cset.set \ 'a Quotient_Cset.set" -is "op \ :: 'a set \ 'a set \ '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 \ 'a Quotient_Cset.set" -is "uminus_class.uminus :: 'a set \ 'a set" by simp -quotient_definition minus where "minus :: 'a Quotient_Cset.set \ 'a Quotient_Cset.set \ 'a Quotient_Cset.set" -is "(op -) :: 'a set \ 'a set \ 'a set" by simp -quotient_definition Inf where "Inf :: ('a :: Inf) Quotient_Cset.set \ 'a" -is "Inf_class.Inf :: ('a :: Inf) set \ 'a" by simp -quotient_definition Sup where "Sup :: ('a :: Sup) Quotient_Cset.set \ 'a" -is "Sup_class.Sup :: ('a :: Sup) set \ 'a" by simp -quotient_definition UNION where "UNION :: 'a Quotient_Cset.set \ ('a \ 'b Quotient_Cset.set) \ 'b Quotient_Cset.set" -is "Complete_Lattices.UNION :: 'a set \ ('a \ 'b set) \ '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 diff -r 3ff8c79a9e2f -r e2f0176149d0 src/HOL/Quotient_Examples/ROOT.ML --- 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"];