src/HOL/Library/Cset.thy
changeset 43241 93b1183e43e5
parent 41505 6d19301074cf
child 43971 892030194015
     1.1 --- a/src/HOL/Library/Cset.thy	Tue Jun 07 11:11:01 2011 +0200
     1.2 +++ b/src/HOL/Library/Cset.thy	Tue Jun 07 11:12:05 2011 +0200
     1.3 @@ -35,66 +35,6 @@
     1.4    by (simp add: Cset.set_eq_iff)
     1.5  hide_fact (open) set_eqI
     1.6  
     1.7 -declare mem_def [simp]
     1.8 -
     1.9 -definition set :: "'a list \<Rightarrow> 'a Cset.set" where
    1.10 -  "set xs = Set (List.set xs)"
    1.11 -hide_const (open) set
    1.12 -
    1.13 -lemma member_set [simp]:
    1.14 -  "member (Cset.set xs) = set xs"
    1.15 -  by (simp add: set_def)
    1.16 -hide_fact (open) member_set
    1.17 -
    1.18 -definition coset :: "'a list \<Rightarrow> 'a Cset.set" where
    1.19 -  "coset xs = Set (- set xs)"
    1.20 -hide_const (open) coset
    1.21 -
    1.22 -lemma member_coset [simp]:
    1.23 -  "member (Cset.coset xs) = - set xs"
    1.24 -  by (simp add: coset_def)
    1.25 -hide_fact (open) member_coset
    1.26 -
    1.27 -code_datatype Cset.set Cset.coset
    1.28 -
    1.29 -lemma member_code [code]:
    1.30 -  "member (Cset.set xs) = List.member xs"
    1.31 -  "member (Cset.coset xs) = Not \<circ> List.member xs"
    1.32 -  by (simp_all add: fun_eq_iff member_def fun_Compl_def bool_Compl_def)
    1.33 -
    1.34 -lemma member_image_UNIV [simp]:
    1.35 -  "member ` UNIV = UNIV"
    1.36 -proof -
    1.37 -  have "\<And>A \<Colon> 'a set. \<exists>B \<Colon> 'a Cset.set. A = member B"
    1.38 -  proof
    1.39 -    fix A :: "'a set"
    1.40 -    show "A = member (Set A)" by simp
    1.41 -  qed
    1.42 -  then show ?thesis by (simp add: image_def)
    1.43 -qed
    1.44 -
    1.45 -definition (in term_syntax)
    1.46 -  setify :: "'a\<Colon>typerep list \<times> (unit \<Rightarrow> Code_Evaluation.term)
    1.47 -    \<Rightarrow> 'a Cset.set \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
    1.48 -  [code_unfold]: "setify xs = Code_Evaluation.valtermify Cset.set {\<cdot>} xs"
    1.49 -
    1.50 -notation fcomp (infixl "\<circ>>" 60)
    1.51 -notation scomp (infixl "\<circ>\<rightarrow>" 60)
    1.52 -
    1.53 -instantiation Cset.set :: (random) random
    1.54 -begin
    1.55 -
    1.56 -definition
    1.57 -  "Quickcheck.random i = Quickcheck.random i \<circ>\<rightarrow> (\<lambda>xs. Pair (setify xs))"
    1.58 -
    1.59 -instance ..
    1.60 -
    1.61 -end
    1.62 -
    1.63 -no_notation fcomp (infixl "\<circ>>" 60)
    1.64 -no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
    1.65 -
    1.66 -
    1.67  subsection {* Lattice instantiation *}
    1.68  
    1.69  instantiation Cset.set :: (type) boolean_algebra
    1.70 @@ -149,185 +89,39 @@
    1.71  definition is_empty :: "'a Cset.set \<Rightarrow> bool" where
    1.72    [simp]: "is_empty A \<longleftrightarrow> More_Set.is_empty (member A)"
    1.73  
    1.74 -lemma is_empty_set [code]:
    1.75 -  "is_empty (Cset.set xs) \<longleftrightarrow> List.null xs"
    1.76 -  by (simp add: is_empty_set)
    1.77 -hide_fact (open) is_empty_set
    1.78 -
    1.79 -lemma empty_set [code]:
    1.80 -  "bot = Cset.set []"
    1.81 -  by (simp add: set_def)
    1.82 -hide_fact (open) empty_set
    1.83 -
    1.84 -lemma UNIV_set [code]:
    1.85 -  "top = Cset.coset []"
    1.86 -  by (simp add: coset_def)
    1.87 -hide_fact (open) UNIV_set
    1.88 -
    1.89  definition insert :: "'a \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
    1.90    [simp]: "insert x A = Set (Set.insert x (member A))"
    1.91  
    1.92 -lemma insert_set [code]:
    1.93 -  "insert x (Cset.set xs) = Cset.set (List.insert x xs)"
    1.94 -  "insert x (Cset.coset xs) = Cset.coset (removeAll x xs)"
    1.95 -  by (simp_all add: set_def coset_def)
    1.96 -
    1.97  definition remove :: "'a \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
    1.98    [simp]: "remove x A = Set (More_Set.remove x (member A))"
    1.99  
   1.100 -lemma remove_set [code]:
   1.101 -  "remove x (Cset.set xs) = Cset.set (removeAll x xs)"
   1.102 -  "remove x (Cset.coset xs) = Cset.coset (List.insert x xs)"
   1.103 -  by (simp_all add: set_def coset_def remove_set_compl)
   1.104 -    (simp add: More_Set.remove_def)
   1.105 -
   1.106  definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a Cset.set \<Rightarrow> 'b Cset.set" where
   1.107    [simp]: "map f A = Set (image f (member A))"
   1.108  
   1.109 -lemma map_set [code]:
   1.110 -  "map f (Cset.set xs) = Cset.set (remdups (List.map f xs))"
   1.111 -  by (simp add: set_def)
   1.112 -
   1.113  enriched_type map: map
   1.114    by (simp_all add: fun_eq_iff image_compose)
   1.115  
   1.116  definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
   1.117    [simp]: "filter P A = Set (More_Set.project P (member A))"
   1.118  
   1.119 -lemma filter_set [code]:
   1.120 -  "filter P (Cset.set xs) = Cset.set (List.filter P xs)"
   1.121 -  by (simp add: set_def project_set)
   1.122 -
   1.123  definition forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
   1.124    [simp]: "forall P A \<longleftrightarrow> Ball (member A) P"
   1.125  
   1.126 -lemma forall_set [code]:
   1.127 -  "forall P (Cset.set xs) \<longleftrightarrow> list_all P xs"
   1.128 -  by (simp add: set_def list_all_iff)
   1.129 -
   1.130  definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
   1.131    [simp]: "exists P A \<longleftrightarrow> Bex (member A) P"
   1.132  
   1.133 -lemma exists_set [code]:
   1.134 -  "exists P (Cset.set xs) \<longleftrightarrow> list_ex P xs"
   1.135 -  by (simp add: set_def list_ex_iff)
   1.136 -
   1.137  definition card :: "'a Cset.set \<Rightarrow> nat" where
   1.138    [simp]: "card A = Finite_Set.card (member A)"
   1.139 -
   1.140 -lemma card_set [code]:
   1.141 -  "card (Cset.set xs) = length (remdups xs)"
   1.142 -proof -
   1.143 -  have "Finite_Set.card (set (remdups xs)) = length (remdups xs)"
   1.144 -    by (rule distinct_card) simp
   1.145 -  then show ?thesis by (simp add: set_def)
   1.146 -qed
   1.147 -
   1.148 -lemma compl_set [simp, code]:
   1.149 -  "- Cset.set xs = Cset.coset xs"
   1.150 -  by (simp add: set_def coset_def)
   1.151 -
   1.152 -lemma compl_coset [simp, code]:
   1.153 -  "- Cset.coset xs = Cset.set xs"
   1.154 -  by (simp add: set_def coset_def)
   1.155 -
   1.156 -
   1.157 -subsection {* Derived operations *}
   1.158 -
   1.159 -lemma subset_eq_forall [code]:
   1.160 -  "A \<le> B \<longleftrightarrow> forall (member B) A"
   1.161 -  by (simp add: subset_eq)
   1.162 -
   1.163 -lemma subset_subset_eq [code]:
   1.164 -  "A < B \<longleftrightarrow> A \<le> B \<and> \<not> B \<le> (A :: 'a Cset.set)"
   1.165 -  by (fact less_le_not_le)
   1.166 -
   1.167 -instantiation Cset.set :: (type) equal
   1.168 -begin
   1.169 -
   1.170 -definition [code]:
   1.171 -  "HOL.equal A B \<longleftrightarrow> A \<le> B \<and> B \<le> (A :: 'a Cset.set)"
   1.172 -
   1.173 -instance proof
   1.174 -qed (simp add: equal_set_def set_eq [symmetric] Cset.set_eq_iff)
   1.175 -
   1.176 -end
   1.177 -
   1.178 -lemma [code nbe]:
   1.179 -  "HOL.equal (A :: 'a Cset.set) A \<longleftrightarrow> True"
   1.180 -  by (fact equal_refl)
   1.181 -
   1.182 -
   1.183 -subsection {* Functorial operations *}
   1.184 -
   1.185 -lemma inter_project [code]:
   1.186 -  "inf A (Cset.set xs) = Cset.set (List.filter (member A) xs)"
   1.187 -  "inf A (Cset.coset xs) = foldr remove xs A"
   1.188 -proof -
   1.189 -  show "inf A (Cset.set xs) = Cset.set (List.filter (member A) xs)"
   1.190 -    by (simp add: inter project_def set_def)
   1.191 -  have *: "\<And>x::'a. remove = (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member)"
   1.192 -    by (simp add: fun_eq_iff)
   1.193 -  have "member \<circ> fold (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member) xs =
   1.194 -    fold More_Set.remove xs \<circ> member"
   1.195 -    by (rule fold_commute) (simp add: fun_eq_iff)
   1.196 -  then have "fold More_Set.remove xs (member A) = 
   1.197 -    member (fold (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member) xs A)"
   1.198 -    by (simp add: fun_eq_iff)
   1.199 -  then have "inf A (Cset.coset xs) = fold remove xs A"
   1.200 -    by (simp add: Diff_eq [symmetric] minus_set *)
   1.201 -  moreover have "\<And>x y :: 'a. Cset.remove y \<circ> Cset.remove x = Cset.remove x \<circ> Cset.remove y"
   1.202 -    by (auto simp add: More_Set.remove_def * intro: ext)
   1.203 -  ultimately show "inf A (Cset.coset xs) = foldr remove xs A"
   1.204 -    by (simp add: foldr_fold)
   1.205 -qed
   1.206 -
   1.207 -lemma subtract_remove [code]:
   1.208 -  "A - Cset.set xs = foldr remove xs A"
   1.209 -  "A - Cset.coset xs = Cset.set (List.filter (member A) xs)"
   1.210 -  by (simp_all only: diff_eq compl_set compl_coset inter_project)
   1.211 -
   1.212 -lemma union_insert [code]:
   1.213 -  "sup (Cset.set xs) A = foldr insert xs A"
   1.214 -  "sup (Cset.coset xs) A = Cset.coset (List.filter (Not \<circ> member A) xs)"
   1.215 -proof -
   1.216 -  have *: "\<And>x::'a. insert = (\<lambda>x. Set \<circ> Set.insert x \<circ> member)"
   1.217 -    by (simp add: fun_eq_iff)
   1.218 -  have "member \<circ> fold (\<lambda>x. Set \<circ> Set.insert x \<circ> member) xs =
   1.219 -    fold Set.insert xs \<circ> member"
   1.220 -    by (rule fold_commute) (simp add: fun_eq_iff)
   1.221 -  then have "fold Set.insert xs (member A) =
   1.222 -    member (fold (\<lambda>x. Set \<circ> Set.insert x \<circ> member) xs A)"
   1.223 -    by (simp add: fun_eq_iff)
   1.224 -  then have "sup (Cset.set xs) A = fold insert xs A"
   1.225 -    by (simp add: union_set *)
   1.226 -  moreover have "\<And>x y :: 'a. Cset.insert y \<circ> Cset.insert x = Cset.insert x \<circ> Cset.insert y"
   1.227 -    by (auto simp add: * intro: ext)
   1.228 -  ultimately show "sup (Cset.set xs) A = foldr insert xs A"
   1.229 -    by (simp add: foldr_fold)
   1.230 -  show "sup (Cset.coset xs) A = Cset.coset (List.filter (Not \<circ> member A) xs)"
   1.231 -    by (auto simp add: coset_def)
   1.232 -qed
   1.233 -
   1.234 +  
   1.235  context complete_lattice
   1.236  begin
   1.237  
   1.238  definition Infimum :: "'a Cset.set \<Rightarrow> 'a" where
   1.239    [simp]: "Infimum A = Inf (member A)"
   1.240  
   1.241 -lemma Infimum_inf [code]:
   1.242 -  "Infimum (Cset.set As) = foldr inf As top"
   1.243 -  "Infimum (Cset.coset []) = bot"
   1.244 -  by (simp_all add: Inf_set_foldr Inf_UNIV)
   1.245 -
   1.246  definition Supremum :: "'a Cset.set \<Rightarrow> 'a" where
   1.247    [simp]: "Supremum A = Sup (member A)"
   1.248  
   1.249 -lemma Supremum_sup [code]:
   1.250 -  "Supremum (Cset.set As) = foldr sup As bot"
   1.251 -  "Supremum (Cset.coset []) = top"
   1.252 -  by (simp_all add: Sup_set_foldr Sup_UNIV)
   1.253 -
   1.254  end
   1.255  
   1.256  
   1.257 @@ -351,7 +145,7 @@
   1.258  declare mem_def [simp del]
   1.259  
   1.260  
   1.261 -hide_const (open) setify is_empty insert remove map filter forall exists card
   1.262 +hide_const (open) is_empty insert remove map filter forall exists card
   1.263    Inter Union
   1.264  
   1.265  end