1.1 --- a/src/HOL/Library/Cset.thy Mon Jul 25 14:10:12 2011 +0200
1.2 +++ b/src/HOL/Library/Cset.thy Mon Jul 25 16:55:48 2011 +0200
1.3 @@ -86,6 +86,12 @@
1.4
1.5 subsection {* Basic operations *}
1.6
1.7 +abbreviation empty :: "'a Cset.set" where "empty \<equiv> bot"
1.8 +hide_const (open) empty
1.9 +
1.10 +abbreviation UNIV :: "'a Cset.set" where "UNIV \<equiv> top"
1.11 +hide_const (open) UNIV
1.12 +
1.13 definition is_empty :: "'a Cset.set \<Rightarrow> bool" where
1.14 [simp]: "is_empty A \<longleftrightarrow> More_Set.is_empty (member A)"
1.15
1.16 @@ -124,9 +130,42 @@
1.17
1.18 end
1.19
1.20 +subsection {* More operations *}
1.21 +
1.22 +text {* conversion from @{typ "'a list"} *}
1.23 +
1.24 +definition set :: "'a list \<Rightarrow> 'a Cset.set" where
1.25 + "set xs = Set (List.set xs)"
1.26 +hide_const (open) set
1.27 +
1.28 +text {* conversion from @{typ "'a Predicate.pred"} *}
1.29 +
1.30 +definition pred_of_cset :: "'a Cset.set \<Rightarrow> 'a Predicate.pred"
1.31 +where [code del]: "pred_of_cset = Predicate.Pred \<circ> Cset.member"
1.32 +
1.33 +definition of_pred :: "'a Predicate.pred \<Rightarrow> 'a Cset.set"
1.34 +where "of_pred = Cset.Set \<circ> Predicate.eval"
1.35 +
1.36 +definition of_seq :: "'a Predicate.seq \<Rightarrow> 'a Cset.set"
1.37 +where "of_seq = of_pred \<circ> Predicate.pred_of_seq"
1.38 +
1.39 +text {* monad operations *}
1.40 +
1.41 +definition single :: "'a \<Rightarrow> 'a Cset.set" where
1.42 + "single a = Set {a}"
1.43 +
1.44 +definition bind :: "'a Cset.set \<Rightarrow> ('a \<Rightarrow> 'b Cset.set) \<Rightarrow> 'b Cset.set"
1.45 + (infixl "\<guillemotright>=" 70)
1.46 + where "A \<guillemotright>= f = Set (\<Union>x \<in> member A. member (f x))"
1.47
1.48 subsection {* Simplified simprules *}
1.49
1.50 +lemma empty_simp [simp]: "member Cset.empty = {}"
1.51 + by(simp)
1.52 +
1.53 +lemma UNIV_simp [simp]: "member Cset.UNIV = UNIV"
1.54 + by simp
1.55 +
1.56 lemma is_empty_simp [simp]:
1.57 "is_empty A \<longleftrightarrow> member A = {}"
1.58 by (simp add: More_Set.is_empty_def)
1.59 @@ -142,10 +181,103 @@
1.60 by (simp add: More_Set.project_def)
1.61 declare filter_def [simp del]
1.62
1.63 +lemma member_set [simp]:
1.64 + "member (Cset.set xs) = set xs"
1.65 + by (simp add: set_def)
1.66 +hide_fact (open) member_set set_def
1.67 +
1.68 +lemma set_simps [simp]:
1.69 + "Cset.set [] = Cset.empty"
1.70 + "Cset.set (x # xs) = insert x (Cset.set xs)"
1.71 +by(simp_all add: Cset.set_def)
1.72 +
1.73 +lemma member_SUPR [simp]:
1.74 + "member (SUPR A f) = SUPR A (member \<circ> f)"
1.75 +unfolding SUPR_def by simp
1.76 +
1.77 +lemma member_bind [simp]:
1.78 + "member (P \<guillemotright>= f) = member (SUPR (member P) f)"
1.79 +by (simp add: bind_def Cset.set_eq_iff)
1.80 +
1.81 +lemma member_single [simp]:
1.82 + "member (single a) = {a}"
1.83 +by(simp add: single_def)
1.84 +
1.85 +lemma single_sup_simps [simp]:
1.86 + shows single_sup: "sup (single a) A = insert a A"
1.87 + and sup_single: "sup A (single a) = insert a A"
1.88 +by(auto simp add: Cset.set_eq_iff)
1.89 +
1.90 +lemma single_bind [simp]:
1.91 + "single a \<guillemotright>= B = B a"
1.92 +by(simp add: bind_def single_def)
1.93 +
1.94 +lemma bind_bind:
1.95 + "(A \<guillemotright>= B) \<guillemotright>= C = A \<guillemotright>= (\<lambda>x. B x \<guillemotright>= C)"
1.96 +by(simp add: bind_def)
1.97 +
1.98 +lemma bind_single [simp]:
1.99 + "A \<guillemotright>= single = A"
1.100 +by(simp add: bind_def single_def)
1.101 +
1.102 +lemma bind_const: "A \<guillemotright>= (\<lambda>_. B) = (if Cset.is_empty A then Cset.empty else B)"
1.103 +by(auto simp add: Cset.set_eq_iff)
1.104 +
1.105 +lemma empty_bind [simp]:
1.106 + "Cset.empty \<guillemotright>= f = Cset.empty"
1.107 +by(simp add: Cset.set_eq_iff)
1.108 +
1.109 +lemma member_of_pred [simp]:
1.110 + "member (of_pred P) = {x. Predicate.eval P x}"
1.111 +by(simp add: of_pred_def Collect_def)
1.112 +
1.113 +lemma member_of_seq [simp]:
1.114 + "member (of_seq xq) = {x. Predicate.member xq x}"
1.115 +by(simp add: of_seq_def eval_member)
1.116 +
1.117 +lemma eval_pred_of_cset [simp]:
1.118 + "Predicate.eval (pred_of_cset A) = Cset.member A"
1.119 +by(simp add: pred_of_cset_def)
1.120 +
1.121 +subsection {* Default implementations *}
1.122 +
1.123 +lemma set_code [code]:
1.124 + "Cset.set = foldl (\<lambda>A x. insert x A) Cset.empty"
1.125 +proof(rule ext, rule Cset.set_eqI)
1.126 + fix xs
1.127 + show "member (Cset.set xs) = member (foldl (\<lambda>A x. insert x A) Cset.empty xs)"
1.128 + by(induct xs rule: rev_induct)(simp_all)
1.129 +qed
1.130 +
1.131 +lemma single_code [code]:
1.132 + "single a = insert a Cset.empty"
1.133 +by(simp add: Cset.single_def)
1.134 +
1.135 +lemma of_pred_code [code]:
1.136 + "of_pred (Predicate.Seq f) = (case f () of
1.137 + Predicate.Empty \<Rightarrow> Cset.empty
1.138 + | Predicate.Insert x P \<Rightarrow> Cset.insert x (of_pred P)
1.139 + | Predicate.Join P xq \<Rightarrow> sup (of_pred P) (of_seq xq))"
1.140 +by(auto split: seq.split
1.141 + simp add: Predicate.Seq_def of_pred_def eval_member Cset.set_eq_iff)
1.142 +
1.143 +lemma of_seq_code [code]:
1.144 + "of_seq Predicate.Empty = Cset.empty"
1.145 + "of_seq (Predicate.Insert x P) = Cset.insert x (of_pred P)"
1.146 + "of_seq (Predicate.Join P xq) = sup (of_pred P) (of_seq xq)"
1.147 +by(auto simp add: of_seq_def of_pred_def Cset.set_eq_iff)
1.148 +
1.149 declare mem_def [simp del]
1.150
1.151 +no_notation bind (infixl "\<guillemotright>=" 70)
1.152
1.153 hide_const (open) is_empty insert remove map filter forall exists card
1.154 - Inter Union
1.155 + Inter Union bind single of_pred of_seq
1.156 +
1.157 +hide_fact (open) set_def pred_of_cset_def of_pred_def of_seq_def single_def
1.158 + bind_def empty_simp UNIV_simp member_set set_simps member_SUPR member_bind
1.159 + member_single single_sup_simps single_sup sup_single single_bind
1.160 + bind_bind bind_single bind_const empty_bind member_of_pred member_of_seq
1.161 + eval_pred_of_cset set_code single_code of_pred_code of_seq_code
1.162
1.163 end
2.1 --- a/src/HOL/Library/Dlist_Cset.thy Mon Jul 25 14:10:12 2011 +0200
2.2 +++ b/src/HOL/Library/Dlist_Cset.thy Mon Jul 25 16:55:48 2011 +0200
2.3 @@ -7,7 +7,7 @@
2.4 begin
2.5
2.6 definition Set :: "'a dlist \<Rightarrow> 'a Cset.set" where
2.7 - "Set dxs = List_Cset.set (list_of_dlist dxs)"
2.8 + "Set dxs = Cset.set (list_of_dlist dxs)"
2.9
2.10 definition Coset :: "'a dlist \<Rightarrow> 'a Cset.set" where
2.11 "Coset dxs = List_Cset.coset (list_of_dlist dxs)"
2.12 @@ -27,6 +27,9 @@
2.13 declare forall_set [code del]
2.14 declare exists_set [code del]
2.15 declare card_set [code del]
2.16 +declare List_Cset.single_set [code del]
2.17 +declare List_Cset.bind_set [code del]
2.18 +declare List_Cset.pred_of_cset_set [code del]
2.19 declare inter_project [code del]
2.20 declare subtract_remove [code del]
2.21 declare union_insert [code del]
2.22 @@ -50,7 +53,7 @@
2.23 by (simp add: Coset_def member_set not_set_compl)
2.24
2.25 lemma Set_dlist_of_list [code]:
2.26 - "List_Cset.set xs = Set (dlist_of_list xs)"
2.27 + "Cset.set xs = Set (dlist_of_list xs)"
2.28 by (rule Cset.set_eqI) simp
2.29
2.30 lemma Coset_dlist_of_list [code]:
2.31 @@ -137,4 +140,16 @@
2.32
2.33 end
2.34
2.35 +declare Cset.single_code[code]
2.36 +
2.37 +lemma bind_set [code]:
2.38 + "Cset.bind (Dlist_Cset.Set xs) f = foldl (\<lambda>A x. sup A (f x)) Cset.empty (list_of_dlist xs)"
2.39 +by(simp add: List_Cset.bind_set Dlist_Cset.Set_def)
2.40 +hide_fact (open) bind_set
2.41 +
2.42 +lemma pred_of_cset_set [code]:
2.43 + "pred_of_cset (Dlist_Cset.Set xs) = foldr sup (map Predicate.single (list_of_dlist xs)) bot"
2.44 +by(simp add: List_Cset.pred_of_cset_set Dlist_Cset.Set_def)
2.45 +hide_fact (open) pred_of_cset_set
2.46 +
2.47 end
3.1 --- a/src/HOL/Library/List_Cset.thy Mon Jul 25 14:10:12 2011 +0200
3.2 +++ b/src/HOL/Library/List_Cset.thy Mon Jul 25 16:55:48 2011 +0200
3.3 @@ -8,15 +8,7 @@
3.4 begin
3.5
3.6 declare mem_def [simp]
3.7 -
3.8 -definition set :: "'a list \<Rightarrow> 'a Cset.set" where
3.9 - "set xs = Set (List.set xs)"
3.10 -hide_const (open) set
3.11 -
3.12 -lemma member_set [simp]:
3.13 - "member (List_Cset.set xs) = set xs"
3.14 - by (simp add: set_def)
3.15 -hide_fact (open) member_set
3.16 +declare Cset.set_code [code del]
3.17
3.18 definition coset :: "'a list \<Rightarrow> 'a Cset.set" where
3.19 "coset xs = Set (- set xs)"
3.20 @@ -27,10 +19,10 @@
3.21 by (simp add: coset_def)
3.22 hide_fact (open) member_coset
3.23
3.24 -code_datatype List_Cset.set List_Cset.coset
3.25 +code_datatype Cset.set List_Cset.coset
3.26
3.27 lemma member_code [code]:
3.28 - "member (List_Cset.set xs) = List.member xs"
3.29 + "member (Cset.set xs) = List.member xs"
3.30 "member (List_Cset.coset xs) = Not \<circ> List.member xs"
3.31 by (simp_all add: fun_eq_iff member_def fun_Compl_def bool_Compl_def)
3.32
3.33 @@ -48,7 +40,7 @@
3.34 definition (in term_syntax)
3.35 setify :: "'a\<Colon>typerep list \<times> (unit \<Rightarrow> Code_Evaluation.term)
3.36 \<Rightarrow> 'a Cset.set \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
3.37 - [code_unfold]: "setify xs = Code_Evaluation.valtermify List_Cset.set {\<cdot>} xs"
3.38 + [code_unfold]: "setify xs = Code_Evaluation.valtermify Cset.set {\<cdot>} xs"
3.39
3.40 notation fcomp (infixl "\<circ>>" 60)
3.41 notation scomp (infixl "\<circ>\<rightarrow>" 60)
3.42 @@ -69,12 +61,12 @@
3.43 subsection {* Basic operations *}
3.44
3.45 lemma is_empty_set [code]:
3.46 - "Cset.is_empty (List_Cset.set xs) \<longleftrightarrow> List.null xs"
3.47 + "Cset.is_empty (Cset.set xs) \<longleftrightarrow> List.null xs"
3.48 by (simp add: is_empty_set null_def)
3.49 hide_fact (open) is_empty_set
3.50
3.51 lemma empty_set [code]:
3.52 - "bot = List_Cset.set []"
3.53 + "Cset.empty = Cset.set []"
3.54 by (simp add: set_def)
3.55 hide_fact (open) empty_set
3.56
3.57 @@ -84,63 +76,87 @@
3.58 hide_fact (open) UNIV_set
3.59
3.60 lemma remove_set [code]:
3.61 - "Cset.remove x (List_Cset.set xs) = List_Cset.set (removeAll x xs)"
3.62 + "Cset.remove x (Cset.set xs) = Cset.set (removeAll x xs)"
3.63 "Cset.remove x (List_Cset.coset xs) = List_Cset.coset (List.insert x xs)"
3.64 -by (simp_all add: set_def coset_def)
3.65 +by (simp_all add: Cset.set_def coset_def)
3.66 (metis List.set_insert More_Set.remove_def remove_set_compl)
3.67
3.68 lemma insert_set [code]:
3.69 - "Cset.insert x (List_Cset.set xs) = List_Cset.set (List.insert x xs)"
3.70 + "Cset.insert x (Cset.set xs) = Cset.set (List.insert x xs)"
3.71 "Cset.insert x (List_Cset.coset xs) = List_Cset.coset (removeAll x xs)"
3.72 - by (simp_all add: set_def coset_def)
3.73 + by (simp_all add: Cset.set_def coset_def)
3.74
3.75 lemma map_set [code]:
3.76 - "Cset.map f (List_Cset.set xs) = List_Cset.set (remdups (List.map f xs))"
3.77 - by (simp add: set_def)
3.78 + "Cset.map f (Cset.set xs) = Cset.set (remdups (List.map f xs))"
3.79 + by (simp add: Cset.set_def)
3.80
3.81 lemma filter_set [code]:
3.82 - "Cset.filter P (List_Cset.set xs) = List_Cset.set (List.filter P xs)"
3.83 - by (simp add: set_def project_set)
3.84 + "Cset.filter P (Cset.set xs) = Cset.set (List.filter P xs)"
3.85 + by (simp add: Cset.set_def project_set)
3.86
3.87 lemma forall_set [code]:
3.88 - "Cset.forall P (List_Cset.set xs) \<longleftrightarrow> list_all P xs"
3.89 - by (simp add: set_def list_all_iff)
3.90 + "Cset.forall P (Cset.set xs) \<longleftrightarrow> list_all P xs"
3.91 + by (simp add: Cset.set_def list_all_iff)
3.92
3.93 lemma exists_set [code]:
3.94 - "Cset.exists P (List_Cset.set xs) \<longleftrightarrow> list_ex P xs"
3.95 - by (simp add: set_def list_ex_iff)
3.96 + "Cset.exists P (Cset.set xs) \<longleftrightarrow> list_ex P xs"
3.97 + by (simp add: Cset.set_def list_ex_iff)
3.98
3.99 lemma card_set [code]:
3.100 - "Cset.card (List_Cset.set xs) = length (remdups xs)"
3.101 + "Cset.card (Cset.set xs) = length (remdups xs)"
3.102 proof -
3.103 have "Finite_Set.card (set (remdups xs)) = length (remdups xs)"
3.104 by (rule distinct_card) simp
3.105 - then show ?thesis by (simp add: set_def)
3.106 + then show ?thesis by (simp add: Cset.set_def)
3.107 qed
3.108
3.109 lemma compl_set [simp, code]:
3.110 - "- List_Cset.set xs = List_Cset.coset xs"
3.111 - by (simp add: set_def coset_def)
3.112 + "- Cset.set xs = List_Cset.coset xs"
3.113 + by (simp add: Cset.set_def coset_def)
3.114
3.115 lemma compl_coset [simp, code]:
3.116 - "- List_Cset.coset xs = List_Cset.set xs"
3.117 - by (simp add: set_def coset_def)
3.118 + "- List_Cset.coset xs = Cset.set xs"
3.119 + by (simp add: Cset.set_def coset_def)
3.120
3.121 context complete_lattice
3.122 begin
3.123
3.124 lemma Infimum_inf [code]:
3.125 - "Infimum (List_Cset.set As) = foldr inf As top"
3.126 + "Infimum (Cset.set As) = foldr inf As top"
3.127 "Infimum (List_Cset.coset []) = bot"
3.128 by (simp_all add: Inf_set_foldr Inf_UNIV)
3.129
3.130 lemma Supremum_sup [code]:
3.131 - "Supremum (List_Cset.set As) = foldr sup As bot"
3.132 + "Supremum (Cset.set As) = foldr sup As bot"
3.133 "Supremum (List_Cset.coset []) = top"
3.134 by (simp_all add: Sup_set_foldr Sup_UNIV)
3.135
3.136 end
3.137
3.138 +declare single_code [code del]
3.139 +lemma single_set [code]:
3.140 + "Cset.single a = Cset.set [a]"
3.141 +by(simp add: Cset.single_code)
3.142 +hide_fact (open) single_set
3.143 +
3.144 +lemma bind_set [code]:
3.145 + "Cset.bind (Cset.set xs) f = foldl (\<lambda>A x. sup A (f x)) (Cset.set []) xs"
3.146 +proof(rule sym)
3.147 + show "foldl (\<lambda>A x. sup A (f x)) (Cset.set []) xs = Cset.bind (Cset.set xs) f"
3.148 + by(induct xs rule: rev_induct)(auto simp add: Cset.bind_def Cset.set_def)
3.149 +qed
3.150 +hide_fact (open) bind_set
3.151 +
3.152 +lemma pred_of_cset_set [code]:
3.153 + "pred_of_cset (Cset.set xs) = foldr sup (map Predicate.single xs) bot"
3.154 +proof -
3.155 + have "pred_of_cset (Cset.set xs) = Predicate.Pred (\<lambda>x. x \<in> set xs)"
3.156 + by(auto simp add: Cset.pred_of_cset_def mem_def)
3.157 + moreover have "foldr sup (map Predicate.single xs) bot = \<dots>"
3.158 + by(induct xs)(auto simp add: bot_pred_def simp del: mem_def intro: pred_eqI, simp)
3.159 + ultimately show ?thesis by(simp)
3.160 +qed
3.161 +hide_fact (open) pred_of_cset_set
3.162
3.163 subsection {* Derived operations *}
3.164
3.165 @@ -171,11 +187,11 @@
3.166 subsection {* Functorial operations *}
3.167
3.168 lemma inter_project [code]:
3.169 - "inf A (List_Cset.set xs) = List_Cset.set (List.filter (Cset.member A) xs)"
3.170 + "inf A (Cset.set xs) = Cset.set (List.filter (Cset.member A) xs)"
3.171 "inf A (List_Cset.coset xs) = foldr Cset.remove xs A"
3.172 proof -
3.173 - show "inf A (List_Cset.set xs) = List_Cset.set (List.filter (member A) xs)"
3.174 - by (simp add: inter project_def set_def)
3.175 + show "inf A (Cset.set xs) = Cset.set (List.filter (member A) xs)"
3.176 + by (simp add: inter project_def Cset.set_def)
3.177 have *: "\<And>x::'a. Cset.remove = (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member)"
3.178 by (simp add: fun_eq_iff More_Set.remove_def)
3.179 have "member \<circ> fold (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member) xs =
3.180 @@ -193,12 +209,12 @@
3.181 qed
3.182
3.183 lemma subtract_remove [code]:
3.184 - "A - List_Cset.set xs = foldr Cset.remove xs A"
3.185 - "A - List_Cset.coset xs = List_Cset.set (List.filter (member A) xs)"
3.186 + "A - Cset.set xs = foldr Cset.remove xs A"
3.187 + "A - List_Cset.coset xs = Cset.set (List.filter (member A) xs)"
3.188 by (simp_all only: diff_eq compl_set compl_coset inter_project)
3.189
3.190 lemma union_insert [code]:
3.191 - "sup (List_Cset.set xs) A = foldr Cset.insert xs A"
3.192 + "sup (Cset.set xs) A = foldr Cset.insert xs A"
3.193 "sup (List_Cset.coset xs) A = List_Cset.coset (List.filter (Not \<circ> member A) xs)"
3.194 proof -
3.195 have *: "\<And>x::'a. Cset.insert = (\<lambda>x. Set \<circ> Set.insert x \<circ> member)"
3.196 @@ -209,11 +225,11 @@
3.197 then have "fold Set.insert xs (member A) =
3.198 member (fold (\<lambda>x. Set \<circ> Set.insert x \<circ> member) xs A)"
3.199 by (simp add: fun_eq_iff)
3.200 - then have "sup (List_Cset.set xs) A = fold Cset.insert xs A"
3.201 + then have "sup (Cset.set xs) A = fold Cset.insert xs A"
3.202 by (simp add: union_set *)
3.203 moreover have "\<And>x y :: 'a. Cset.insert y \<circ> Cset.insert x = Cset.insert x \<circ> Cset.insert y"
3.204 by (auto simp add: * intro: ext)
3.205 - ultimately show "sup (List_Cset.set xs) A = foldr Cset.insert xs A"
3.206 + ultimately show "sup (Cset.set xs) A = foldr Cset.insert xs A"
3.207 by (simp add: foldr_fold)
3.208 show "sup (List_Cset.coset xs) A = List_Cset.coset (List.filter (Not \<circ> member A) xs)"
3.209 by (auto simp add: coset_def)