1.1 --- a/src/HOL/Library/List_Cset.thy Sat Aug 27 09:02:25 2011 +0200
1.2 +++ b/src/HOL/Library/List_Cset.thy Sat Aug 27 09:44:45 2011 +0200
1.3 @@ -7,28 +7,12 @@
1.4 imports Cset
1.5 begin
1.6
1.7 -declare mem_def [simp]
1.8 -declare Cset.set_code [code del]
1.9 -
1.10 -definition coset :: "'a list \<Rightarrow> 'a Cset.set" where
1.11 - "coset xs = Set (- set xs)"
1.12 -hide_const (open) coset
1.13 -
1.14 -lemma set_of_coset [simp]:
1.15 - "set_of (List_Cset.coset xs) = - set xs"
1.16 - by (simp add: coset_def)
1.17 -
1.18 -lemma member_coset [simp]:
1.19 - "member (List_Cset.coset xs) = (\<lambda>x. x \<in> - set xs)"
1.20 - by (simp add: coset_def fun_eq_iff)
1.21 -hide_fact (open) member_coset
1.22 -
1.23 -code_datatype Cset.set List_Cset.coset
1.24 +code_datatype Cset.set Cset.coset
1.25
1.26 lemma member_code [code]:
1.27 "member (Cset.set xs) = List.member xs"
1.28 - "member (List_Cset.coset xs) = Not \<circ> List.member xs"
1.29 - by (simp_all add: fun_eq_iff member_def fun_Compl_def member_set)
1.30 + "member (Cset.coset xs) = Not \<circ> List.member xs"
1.31 + by (simp_all add: fun_eq_iff List.member_def)
1.32
1.33 definition (in term_syntax)
1.34 setify :: "'a\<Colon>typerep list \<times> (unit \<Rightarrow> Code_Evaluation.term)
1.35 @@ -60,24 +44,27 @@
1.36
1.37 lemma empty_set [code]:
1.38 "Cset.empty = Cset.set []"
1.39 - by (simp add: set_def)
1.40 + by simp
1.41 hide_fact (open) empty_set
1.42
1.43 lemma UNIV_set [code]:
1.44 - "top = List_Cset.coset []"
1.45 - by (simp add: coset_def)
1.46 + "top = Cset.coset []"
1.47 + by (simp add: Cset.coset_def)
1.48 hide_fact (open) UNIV_set
1.49
1.50 lemma remove_set [code]:
1.51 "Cset.remove x (Cset.set xs) = Cset.set (removeAll x xs)"
1.52 - "Cset.remove x (List_Cset.coset xs) = List_Cset.coset (List.insert x xs)"
1.53 -by (simp_all add: Cset.set_def coset_def)
1.54 - (metis List.set_insert More_Set.remove_def remove_set_compl)
1.55 + "Cset.remove x (Cset.coset xs) = Cset.coset (List.insert x xs)"
1.56 + by (simp_all add: Cset.set_def Cset.coset_def Compl_insert)
1.57
1.58 lemma insert_set [code]:
1.59 "Cset.insert x (Cset.set xs) = Cset.set (List.insert x xs)"
1.60 - "Cset.insert x (List_Cset.coset xs) = List_Cset.coset (removeAll x xs)"
1.61 - by (simp_all add: Cset.set_def coset_def)
1.62 + "Cset.insert x (Cset.coset xs) = Cset.coset (removeAll x xs)"
1.63 + by (simp_all add: Cset.set_def Cset.coset_def)
1.64 +
1.65 +declare compl_set [code]
1.66 +declare compl_coset [code]
1.67 +declare subtract_remove [cpde]
1.68
1.69 lemma map_set [code]:
1.70 "Cset.map f (Cset.set xs) = Cset.set (remdups (List.map f xs))"
1.71 @@ -103,26 +90,11 @@
1.72 then show ?thesis by (simp add: Cset.set_def)
1.73 qed
1.74
1.75 -lemma compl_set [simp, code]:
1.76 - "- Cset.set xs = List_Cset.coset xs"
1.77 - by (simp add: Cset.set_def coset_def)
1.78 -
1.79 -lemma compl_coset [simp, code]:
1.80 - "- List_Cset.coset xs = Cset.set xs"
1.81 - by (simp add: Cset.set_def coset_def)
1.82 -
1.83 context complete_lattice
1.84 begin
1.85
1.86 -lemma Infimum_inf [code]:
1.87 - "Infimum (Cset.set As) = foldr inf As top"
1.88 - "Infimum (List_Cset.coset []) = bot"
1.89 - by (simp_all add: Inf_set_foldr)
1.90 -
1.91 -lemma Supremum_sup [code]:
1.92 - "Supremum (Cset.set As) = foldr sup As bot"
1.93 - "Supremum (List_Cset.coset []) = top"
1.94 - by (simp_all add: Sup_set_foldr)
1.95 +declare Infimum_inf [code]
1.96 +declare Supremum_sup [code]
1.97
1.98 end
1.99
1.100 @@ -132,20 +104,8 @@
1.101 by(simp add: Cset.single_code)
1.102 hide_fact (open) single_set
1.103
1.104 -lemma bind_set [code]:
1.105 - "Cset.bind (Cset.set xs) f = fold (sup \<circ> f) xs (Cset.set [])"
1.106 - by (simp add: Cset.bind_def SUPR_set_fold)
1.107 -
1.108 -lemma pred_of_cset_set [code]:
1.109 - "pred_of_cset (Cset.set xs) = foldr sup (map Predicate.single xs) bot"
1.110 -proof -
1.111 - have "pred_of_cset (Cset.set xs) = Predicate.Pred (\<lambda>x. x \<in> set xs)"
1.112 - by (simp add: Cset.pred_of_cset_def member_code member_set)
1.113 - moreover have "foldr sup (map Predicate.single xs) bot = \<dots>"
1.114 - by (induct xs) (auto simp add: bot_pred_def simp del: mem_def intro: pred_eqI, simp)
1.115 - ultimately show ?thesis by simp
1.116 -qed
1.117 -hide_fact (open) pred_of_cset_set
1.118 +declare Cset.bind_set [code]
1.119 +declare Cset.pred_of_cset_set [code]
1.120
1.121
1.122 subsection {* Derived operations *}
1.123 @@ -165,7 +125,7 @@
1.124 "HOL.equal A B \<longleftrightarrow> A \<le> B \<and> B \<le> (A :: 'a Cset.set)"
1.125
1.126 instance proof
1.127 -qed (simp add: equal_set_def set_eq [symmetric] Cset.set_eq_iff fun_eq_iff member_def)
1.128 +qed (auto simp add: equal_set_def Cset.set_eq_iff Cset.member_def fun_eq_iff mem_def)
1.129
1.130 end
1.131
1.132 @@ -176,59 +136,7 @@
1.133
1.134 subsection {* Functorial operations *}
1.135
1.136 -lemma member_cset_of:
1.137 - "member = set_of"
1.138 - by (rule ext)+ (simp add: member_def)
1.139 -
1.140 -lemma inter_project [code]:
1.141 - "inf A (Cset.set xs) = Cset.set (List.filter (Cset.member A) xs)"
1.142 - "inf A (List_Cset.coset xs) = foldr Cset.remove xs A"
1.143 -proof -
1.144 - show "inf A (Cset.set xs) = Cset.set (List.filter (member A) xs)"
1.145 - by (simp add: inter project_def Cset.set_def member_cset_of)
1.146 - have *: "\<And>x::'a. Cset.remove = (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member)"
1.147 - by (simp add: fun_eq_iff More_Set.remove_def member_cset_of)
1.148 - have "member \<circ> fold (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member) xs =
1.149 - fold More_Set.remove xs \<circ> member"
1.150 - by (rule fold_commute) (simp add: fun_eq_iff)
1.151 - then have "fold More_Set.remove xs (member A) =
1.152 - member (fold (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member) xs A)"
1.153 - by (simp add: fun_eq_iff)
1.154 - then have "inf A (List_Cset.coset xs) = fold Cset.remove xs A"
1.155 - by (simp add: Diff_eq [symmetric] minus_set * member_cset_of)
1.156 - moreover have "\<And>x y :: 'a. Cset.remove y \<circ> Cset.remove x = Cset.remove x \<circ> Cset.remove y"
1.157 - by (auto simp add: More_Set.remove_def * member_cset_of intro: ext)
1.158 - ultimately show "inf A (List_Cset.coset xs) = foldr Cset.remove xs A"
1.159 - by (simp add: foldr_fold)
1.160 -qed
1.161 -
1.162 -lemma subtract_remove [code]:
1.163 - "A - Cset.set xs = foldr Cset.remove xs A"
1.164 - "A - List_Cset.coset xs = Cset.set (List.filter (member A) xs)"
1.165 - by (simp_all only: diff_eq compl_set compl_coset inter_project)
1.166 -
1.167 -lemma union_insert [code]:
1.168 - "sup (Cset.set xs) A = foldr Cset.insert xs A"
1.169 - "sup (List_Cset.coset xs) A = List_Cset.coset (List.filter (Not \<circ> member A) xs)"
1.170 -proof -
1.171 - have *: "\<And>x::'a. Cset.insert = (\<lambda>x. Set \<circ> Set.insert x \<circ> member)"
1.172 - by (simp add: fun_eq_iff member_cset_of)
1.173 - have "member \<circ> fold (\<lambda>x. Set \<circ> Set.insert x \<circ> member) xs =
1.174 - fold Set.insert xs \<circ> member"
1.175 - by (rule fold_commute) (simp add: fun_eq_iff)
1.176 - then have "fold Set.insert xs (member A) =
1.177 - member (fold (\<lambda>x. Set \<circ> Set.insert x \<circ> member) xs A)"
1.178 - by (simp add: fun_eq_iff)
1.179 - then have "sup (Cset.set xs) A = fold Cset.insert xs A"
1.180 - by (simp add: union_set * member_cset_of)
1.181 - moreover have "\<And>x y :: 'a. Cset.insert y \<circ> Cset.insert x = Cset.insert x \<circ> Cset.insert y"
1.182 - by (auto simp add: * member_cset_of intro: ext)
1.183 - ultimately show "sup (Cset.set xs) A = foldr Cset.insert xs A"
1.184 - by (simp add: foldr_fold)
1.185 - show "sup (List_Cset.coset xs) A = List_Cset.coset (List.filter (Not \<circ> member A) xs)"
1.186 - by (auto simp add: coset_def member_cset_of)
1.187 -qed
1.188 -
1.189 -declare mem_def[simp del]
1.190 +declare inter_project [code]
1.191 +declare union_insert [code]
1.192
1.193 end