src/HOL/Library/Cset.thy
changeset 40672 abd4e7358847
parent 40604 c0770657c8de
child 40968 a6fcd305f7dc
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Cset.thy	Mon Nov 22 17:46:51 2010 +0100
     1.3 @@ -0,0 +1,357 @@
     1.4 +
     1.5 +(* Author: Florian Haftmann, TU Muenchen *)
     1.6 +
     1.7 +header {* A dedicated set type which is executable on its finite part *}
     1.8 +
     1.9 +theory Cset
    1.10 +imports More_Set More_List
    1.11 +begin
    1.12 +
    1.13 +subsection {* Lifting *}
    1.14 +
    1.15 +typedef (open) 'a set = "UNIV :: 'a set set"
    1.16 +  morphisms member Set by rule+
    1.17 +hide_type (open) set
    1.18 +
    1.19 +lemma member_Set [simp]:
    1.20 +  "member (Set A) = A"
    1.21 +  by (rule Set_inverse) rule
    1.22 +
    1.23 +lemma Set_member [simp]:
    1.24 +  "Set (member A) = A"
    1.25 +  by (fact member_inverse)
    1.26 +
    1.27 +lemma Set_inject [simp]:
    1.28 +  "Set A = Set B \<longleftrightarrow> A = B"
    1.29 +  by (simp add: Set_inject)
    1.30 +
    1.31 +lemma set_eq_iff:
    1.32 +  "A = B \<longleftrightarrow> member A = member B"
    1.33 +  by (simp add: member_inject)
    1.34 +hide_fact (open) set_eq_iff
    1.35 +
    1.36 +lemma set_eqI:
    1.37 +  "member A = member B \<Longrightarrow> A = B"
    1.38 +  by (simp add: Cset.set_eq_iff)
    1.39 +hide_fact (open) set_eqI
    1.40 +
    1.41 +declare mem_def [simp]
    1.42 +
    1.43 +definition set :: "'a list \<Rightarrow> 'a Cset.set" where
    1.44 +  "set xs = Set (List.set xs)"
    1.45 +hide_const (open) set
    1.46 +
    1.47 +lemma member_set [simp]:
    1.48 +  "member (Cset.set xs) = set xs"
    1.49 +  by (simp add: set_def)
    1.50 +hide_fact (open) member_set
    1.51 +
    1.52 +definition coset :: "'a list \<Rightarrow> 'a Cset.set" where
    1.53 +  "coset xs = Set (- set xs)"
    1.54 +hide_const (open) coset
    1.55 +
    1.56 +lemma member_coset [simp]:
    1.57 +  "member (Cset.coset xs) = - set xs"
    1.58 +  by (simp add: coset_def)
    1.59 +hide_fact (open) member_coset
    1.60 +
    1.61 +code_datatype Cset.set Cset.coset
    1.62 +
    1.63 +lemma member_code [code]:
    1.64 +  "member (Cset.set xs) = List.member xs"
    1.65 +  "member (Cset.coset xs) = Not \<circ> List.member xs"
    1.66 +  by (simp_all add: fun_eq_iff member_def fun_Compl_def bool_Compl_def)
    1.67 +
    1.68 +lemma member_image_UNIV [simp]:
    1.69 +  "member ` UNIV = UNIV"
    1.70 +proof -
    1.71 +  have "\<And>A \<Colon> 'a set. \<exists>B \<Colon> 'a Cset.set. A = member B"
    1.72 +  proof
    1.73 +    fix A :: "'a set"
    1.74 +    show "A = member (Set A)" by simp
    1.75 +  qed
    1.76 +  then show ?thesis by (simp add: image_def)
    1.77 +qed
    1.78 +
    1.79 +definition (in term_syntax)
    1.80 +  setify :: "'a\<Colon>typerep list \<times> (unit \<Rightarrow> Code_Evaluation.term)
    1.81 +    \<Rightarrow> 'a Cset.set \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
    1.82 +  [code_unfold]: "setify xs = Code_Evaluation.valtermify Cset.set {\<cdot>} xs"
    1.83 +
    1.84 +notation fcomp (infixl "\<circ>>" 60)
    1.85 +notation scomp (infixl "\<circ>\<rightarrow>" 60)
    1.86 +
    1.87 +instantiation Cset.set :: (random) random
    1.88 +begin
    1.89 +
    1.90 +definition
    1.91 +  "Quickcheck.random i = Quickcheck.random i \<circ>\<rightarrow> (\<lambda>xs. Pair (setify xs))"
    1.92 +
    1.93 +instance ..
    1.94 +
    1.95 +end
    1.96 +
    1.97 +no_notation fcomp (infixl "\<circ>>" 60)
    1.98 +no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
    1.99 +
   1.100 +
   1.101 +subsection {* Lattice instantiation *}
   1.102 +
   1.103 +instantiation Cset.set :: (type) boolean_algebra
   1.104 +begin
   1.105 +
   1.106 +definition less_eq_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
   1.107 +  [simp]: "A \<le> B \<longleftrightarrow> member A \<subseteq> member B"
   1.108 +
   1.109 +definition less_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
   1.110 +  [simp]: "A < B \<longleftrightarrow> member A \<subset> member B"
   1.111 +
   1.112 +definition inf_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
   1.113 +  [simp]: "inf A B = Set (member A \<inter> member B)"
   1.114 +
   1.115 +definition sup_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
   1.116 +  [simp]: "sup A B = Set (member A \<union> member B)"
   1.117 +
   1.118 +definition bot_set :: "'a Cset.set" where
   1.119 +  [simp]: "bot = Set {}"
   1.120 +
   1.121 +definition top_set :: "'a Cset.set" where
   1.122 +  [simp]: "top = Set UNIV"
   1.123 +
   1.124 +definition uminus_set :: "'a Cset.set \<Rightarrow> 'a Cset.set" where
   1.125 +  [simp]: "- A = Set (- (member A))"
   1.126 +
   1.127 +definition minus_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
   1.128 +  [simp]: "A - B = Set (member A - member B)"
   1.129 +
   1.130 +instance proof
   1.131 +qed (auto intro: Cset.set_eqI)
   1.132 +
   1.133 +end
   1.134 +
   1.135 +instantiation Cset.set :: (type) complete_lattice
   1.136 +begin
   1.137 +
   1.138 +definition Inf_set :: "'a Cset.set set \<Rightarrow> 'a Cset.set" where
   1.139 +  [simp]: "Inf_set As = Set (Inf (image member As))"
   1.140 +
   1.141 +definition Sup_set :: "'a Cset.set set \<Rightarrow> 'a Cset.set" where
   1.142 +  [simp]: "Sup_set As = Set (Sup (image member As))"
   1.143 +
   1.144 +instance proof
   1.145 +qed (auto simp add: le_fun_def le_bool_def)
   1.146 +
   1.147 +end
   1.148 +
   1.149 +
   1.150 +subsection {* Basic operations *}
   1.151 +
   1.152 +definition is_empty :: "'a Cset.set \<Rightarrow> bool" where
   1.153 +  [simp]: "is_empty A \<longleftrightarrow> More_Set.is_empty (member A)"
   1.154 +
   1.155 +lemma is_empty_set [code]:
   1.156 +  "is_empty (Cset.set xs) \<longleftrightarrow> List.null xs"
   1.157 +  by (simp add: is_empty_set)
   1.158 +hide_fact (open) is_empty_set
   1.159 +
   1.160 +lemma empty_set [code]:
   1.161 +  "bot = Cset.set []"
   1.162 +  by (simp add: set_def)
   1.163 +hide_fact (open) empty_set
   1.164 +
   1.165 +lemma UNIV_set [code]:
   1.166 +  "top = Cset.coset []"
   1.167 +  by (simp add: coset_def)
   1.168 +hide_fact (open) UNIV_set
   1.169 +
   1.170 +definition insert :: "'a \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
   1.171 +  [simp]: "insert x A = Set (Set.insert x (member A))"
   1.172 +
   1.173 +lemma insert_set [code]:
   1.174 +  "insert x (Cset.set xs) = Cset.set (List.insert x xs)"
   1.175 +  "insert x (Cset.coset xs) = Cset.coset (removeAll x xs)"
   1.176 +  by (simp_all add: set_def coset_def)
   1.177 +
   1.178 +definition remove :: "'a \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
   1.179 +  [simp]: "remove x A = Set (More_Set.remove x (member A))"
   1.180 +
   1.181 +lemma remove_set [code]:
   1.182 +  "remove x (Cset.set xs) = Cset.set (removeAll x xs)"
   1.183 +  "remove x (Cset.coset xs) = Cset.coset (List.insert x xs)"
   1.184 +  by (simp_all add: set_def coset_def remove_set_compl)
   1.185 +    (simp add: More_Set.remove_def)
   1.186 +
   1.187 +definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a Cset.set \<Rightarrow> 'b Cset.set" where
   1.188 +  [simp]: "map f A = Set (image f (member A))"
   1.189 +
   1.190 +lemma map_set [code]:
   1.191 +  "map f (Cset.set xs) = Cset.set (remdups (List.map f xs))"
   1.192 +  by (simp add: set_def)
   1.193 +
   1.194 +type_mapper map
   1.195 +  by (simp_all add: image_image)
   1.196 +
   1.197 +definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
   1.198 +  [simp]: "filter P A = Set (More_Set.project P (member A))"
   1.199 +
   1.200 +lemma filter_set [code]:
   1.201 +  "filter P (Cset.set xs) = Cset.set (List.filter P xs)"
   1.202 +  by (simp add: set_def project_set)
   1.203 +
   1.204 +definition forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
   1.205 +  [simp]: "forall P A \<longleftrightarrow> Ball (member A) P"
   1.206 +
   1.207 +lemma forall_set [code]:
   1.208 +  "forall P (Cset.set xs) \<longleftrightarrow> list_all P xs"
   1.209 +  by (simp add: set_def list_all_iff)
   1.210 +
   1.211 +definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
   1.212 +  [simp]: "exists P A \<longleftrightarrow> Bex (member A) P"
   1.213 +
   1.214 +lemma exists_set [code]:
   1.215 +  "exists P (Cset.set xs) \<longleftrightarrow> list_ex P xs"
   1.216 +  by (simp add: set_def list_ex_iff)
   1.217 +
   1.218 +definition card :: "'a Cset.set \<Rightarrow> nat" where
   1.219 +  [simp]: "card A = Finite_Set.card (member A)"
   1.220 +
   1.221 +lemma card_set [code]:
   1.222 +  "card (Cset.set xs) = length (remdups xs)"
   1.223 +proof -
   1.224 +  have "Finite_Set.card (set (remdups xs)) = length (remdups xs)"
   1.225 +    by (rule distinct_card) simp
   1.226 +  then show ?thesis by (simp add: set_def)
   1.227 +qed
   1.228 +
   1.229 +lemma compl_set [simp, code]:
   1.230 +  "- Cset.set xs = Cset.coset xs"
   1.231 +  by (simp add: set_def coset_def)
   1.232 +
   1.233 +lemma compl_coset [simp, code]:
   1.234 +  "- Cset.coset xs = Cset.set xs"
   1.235 +  by (simp add: set_def coset_def)
   1.236 +
   1.237 +
   1.238 +subsection {* Derived operations *}
   1.239 +
   1.240 +lemma subset_eq_forall [code]:
   1.241 +  "A \<le> B \<longleftrightarrow> forall (member B) A"
   1.242 +  by (simp add: subset_eq)
   1.243 +
   1.244 +lemma subset_subset_eq [code]:
   1.245 +  "A < B \<longleftrightarrow> A \<le> B \<and> \<not> B \<le> (A :: 'a Cset.set)"
   1.246 +  by (fact less_le_not_le)
   1.247 +
   1.248 +instantiation Cset.set :: (type) equal
   1.249 +begin
   1.250 +
   1.251 +definition [code]:
   1.252 +  "HOL.equal A B \<longleftrightarrow> A \<le> B \<and> B \<le> (A :: 'a Cset.set)"
   1.253 +
   1.254 +instance proof
   1.255 +qed (simp add: equal_set_def set_eq [symmetric] Cset.set_eq_iff)
   1.256 +
   1.257 +end
   1.258 +
   1.259 +lemma [code nbe]:
   1.260 +  "HOL.equal (A :: 'a Cset.set) A \<longleftrightarrow> True"
   1.261 +  by (fact equal_refl)
   1.262 +
   1.263 +
   1.264 +subsection {* Functorial operations *}
   1.265 +
   1.266 +lemma inter_project [code]:
   1.267 +  "inf A (Cset.set xs) = Cset.set (List.filter (member A) xs)"
   1.268 +  "inf A (Cset.coset xs) = foldr remove xs A"
   1.269 +proof -
   1.270 +  show "inf A (Cset.set xs) = Cset.set (List.filter (member A) xs)"
   1.271 +    by (simp add: inter project_def set_def)
   1.272 +  have *: "\<And>x::'a. remove = (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member)"
   1.273 +    by (simp add: fun_eq_iff)
   1.274 +  have "member \<circ> fold (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member) xs =
   1.275 +    fold More_Set.remove xs \<circ> member"
   1.276 +    by (rule fold_commute) (simp add: fun_eq_iff)
   1.277 +  then have "fold More_Set.remove xs (member A) = 
   1.278 +    member (fold (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member) xs A)"
   1.279 +    by (simp add: fun_eq_iff)
   1.280 +  then have "inf A (Cset.coset xs) = fold remove xs A"
   1.281 +    by (simp add: Diff_eq [symmetric] minus_set *)
   1.282 +  moreover have "\<And>x y :: 'a. Cset.remove y \<circ> Cset.remove x = Cset.remove x \<circ> Cset.remove y"
   1.283 +    by (auto simp add: More_Set.remove_def * intro: ext)
   1.284 +  ultimately show "inf A (Cset.coset xs) = foldr remove xs A"
   1.285 +    by (simp add: foldr_fold)
   1.286 +qed
   1.287 +
   1.288 +lemma subtract_remove [code]:
   1.289 +  "A - Cset.set xs = foldr remove xs A"
   1.290 +  "A - Cset.coset xs = Cset.set (List.filter (member A) xs)"
   1.291 +  by (simp_all only: diff_eq compl_set compl_coset inter_project)
   1.292 +
   1.293 +lemma union_insert [code]:
   1.294 +  "sup (Cset.set xs) A = foldr insert xs A"
   1.295 +  "sup (Cset.coset xs) A = Cset.coset (List.filter (Not \<circ> member A) xs)"
   1.296 +proof -
   1.297 +  have *: "\<And>x::'a. insert = (\<lambda>x. Set \<circ> Set.insert x \<circ> member)"
   1.298 +    by (simp add: fun_eq_iff)
   1.299 +  have "member \<circ> fold (\<lambda>x. Set \<circ> Set.insert x \<circ> member) xs =
   1.300 +    fold Set.insert xs \<circ> member"
   1.301 +    by (rule fold_commute) (simp add: fun_eq_iff)
   1.302 +  then have "fold Set.insert xs (member A) =
   1.303 +    member (fold (\<lambda>x. Set \<circ> Set.insert x \<circ> member) xs A)"
   1.304 +    by (simp add: fun_eq_iff)
   1.305 +  then have "sup (Cset.set xs) A = fold insert xs A"
   1.306 +    by (simp add: union_set *)
   1.307 +  moreover have "\<And>x y :: 'a. Cset.insert y \<circ> Cset.insert x = Cset.insert x \<circ> Cset.insert y"
   1.308 +    by (auto simp add: * intro: ext)
   1.309 +  ultimately show "sup (Cset.set xs) A = foldr insert xs A"
   1.310 +    by (simp add: foldr_fold)
   1.311 +  show "sup (Cset.coset xs) A = Cset.coset (List.filter (Not \<circ> member A) xs)"
   1.312 +    by (auto simp add: coset_def)
   1.313 +qed
   1.314 +
   1.315 +context complete_lattice
   1.316 +begin
   1.317 +
   1.318 +definition Infimum :: "'a Cset.set \<Rightarrow> 'a" where
   1.319 +  [simp]: "Infimum A = Inf (member A)"
   1.320 +
   1.321 +lemma Infimum_inf [code]:
   1.322 +  "Infimum (Cset.set As) = foldr inf As top"
   1.323 +  "Infimum (Cset.coset []) = bot"
   1.324 +  by (simp_all add: Inf_set_foldr Inf_UNIV)
   1.325 +
   1.326 +definition Supremum :: "'a Cset.set \<Rightarrow> 'a" where
   1.327 +  [simp]: "Supremum A = Sup (member A)"
   1.328 +
   1.329 +lemma Supremum_sup [code]:
   1.330 +  "Supremum (Cset.set As) = foldr sup As bot"
   1.331 +  "Supremum (Cset.coset []) = top"
   1.332 +  by (simp_all add: Sup_set_foldr Sup_UNIV)
   1.333 +
   1.334 +end
   1.335 +
   1.336 +
   1.337 +subsection {* Simplified simprules *}
   1.338 +
   1.339 +lemma is_empty_simp [simp]:
   1.340 +  "is_empty A \<longleftrightarrow> member A = {}"
   1.341 +  by (simp add: More_Set.is_empty_def)
   1.342 +declare is_empty_def [simp del]
   1.343 +
   1.344 +lemma remove_simp [simp]:
   1.345 +  "remove x A = Set (member A - {x})"
   1.346 +  by (simp add: More_Set.remove_def)
   1.347 +declare remove_def [simp del]
   1.348 +
   1.349 +lemma filter_simp [simp]:
   1.350 +  "filter P A = Set {x \<in> member A. P x}"
   1.351 +  by (simp add: More_Set.project_def)
   1.352 +declare filter_def [simp del]
   1.353 +
   1.354 +declare mem_def [simp del]
   1.355 +
   1.356 +
   1.357 +hide_const (open) setify is_empty insert remove map filter forall exists card
   1.358 +  Inter Union
   1.359 +
   1.360 +end