sets and cosets
authorhaftmann
Tue Oct 06 15:59:12 2009 +0200 (2009-10-06)
changeset 32880b8bee63c7202
parent 32878 f8d995b5dd60
child 32881 13b153243ed4
sets and cosets
src/HOL/Library/Fset.thy
src/HOL/Library/List_Set.thy
     1.1 --- a/src/HOL/Library/Fset.thy	Mon Oct 05 17:28:59 2009 +0100
     1.2 +++ b/src/HOL/Library/Fset.thy	Tue Oct 06 15:59:12 2009 +0200
     1.3 @@ -9,7 +9,6 @@
     1.4  
     1.5  declare mem_def [simp]
     1.6  
     1.7 -
     1.8  subsection {* Lifting *}
     1.9  
    1.10  datatype 'a fset = Fset "'a set"
    1.11 @@ -28,7 +27,30 @@
    1.12    "member (Set xs) = set xs"
    1.13    by (simp add: Set_def)
    1.14  
    1.15 -code_datatype Set
    1.16 +definition Coset :: "'a list \<Rightarrow> 'a fset" where
    1.17 +  "Coset xs = Fset (- set xs)"
    1.18 +
    1.19 +lemma member_Coset [simp]:
    1.20 +  "member (Coset xs) = - set xs"
    1.21 +  by (simp add: Coset_def)
    1.22 +
    1.23 +code_datatype Set Coset
    1.24 +
    1.25 +lemma member_code [code]:
    1.26 +  "member (Set xs) y \<longleftrightarrow> List.member y xs"
    1.27 +  "member (Coset xs) y \<longleftrightarrow> \<not> List.member y xs"
    1.28 +  by (simp_all add: mem_iff fun_Compl_def bool_Compl_def)
    1.29 +
    1.30 +lemma member_image_UNIV [simp]:
    1.31 +  "member ` UNIV = UNIV"
    1.32 +proof -
    1.33 +  have "\<And>A \<Colon> 'a set. \<exists>B \<Colon> 'a fset. A = member B"
    1.34 +  proof
    1.35 +    fix A :: "'a set"
    1.36 +    show "A = member (Fset A)" by simp
    1.37 +  qed
    1.38 +  then show ?thesis by (simp add: image_def)
    1.39 +qed
    1.40  
    1.41  
    1.42  subsection {* Basic operations *}
    1.43 @@ -52,14 +74,16 @@
    1.44  
    1.45  lemma insert_Set [code]:
    1.46    "insert x (Set xs) = Set (List_Set.insert x xs)"
    1.47 -  by (simp add: Set_def insert_set)
    1.48 +  "insert x (Coset xs) = Coset (remove_all x xs)"
    1.49 +  by (simp_all add: Set_def Coset_def insert_set insert_set_compl)
    1.50  
    1.51  definition remove :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
    1.52    [simp]: "remove x A = Fset (List_Set.remove x (member A))"
    1.53  
    1.54  lemma remove_Set [code]:
    1.55    "remove x (Set xs) = Set (remove_all x xs)"
    1.56 -  by (simp add: Set_def remove_set)
    1.57 +  "remove x (Coset xs) = Coset (List_Set.insert x xs)"
    1.58 +  by (simp_all add: Set_def Coset_def remove_set remove_set_compl)
    1.59  
    1.60  definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" where
    1.61    [simp]: "map f A = Fset (image f (member A))"
    1.62 @@ -103,15 +127,11 @@
    1.63  
    1.64  subsection {* Derived operations *}
    1.65  
    1.66 -lemma member_exists [code]:
    1.67 -  "member A y \<longleftrightarrow> exists (\<lambda>x. y = x) A"
    1.68 -  by simp
    1.69 -
    1.70  definition subfset_eq :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where
    1.71    [simp]: "subfset_eq A B \<longleftrightarrow> member A \<subseteq> member B"
    1.72  
    1.73  lemma subfset_eq_forall [code]:
    1.74 -  "subfset_eq A B \<longleftrightarrow> forall (\<lambda>x. member B x) A"
    1.75 +  "subfset_eq A B \<longleftrightarrow> forall (member B) A"
    1.76    by (simp add: subset_eq)
    1.77  
    1.78  definition subfset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where
    1.79 @@ -125,26 +145,23 @@
    1.80    "eq_class.eq A B \<longleftrightarrow> subfset_eq A B \<and> subfset_eq B A"
    1.81    by (cases A, cases B) (simp add: eq set_eq)
    1.82  
    1.83 -definition inter :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
    1.84 -  [simp]: "inter A B = Fset (project (member A) (member B))"
    1.85 -
    1.86 -lemma inter_project [code]:
    1.87 -  "inter A B = filter (member A) B"
    1.88 -  by (simp add: inter)
    1.89 -
    1.90  
    1.91  subsection {* Functorial operations *}
    1.92  
    1.93 -definition union :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
    1.94 -  [simp]: "union A B = Fset (member A \<union> member B)"
    1.95 +definition inter :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
    1.96 +  [simp]: "inter A B = Fset (member A \<inter> member B)"
    1.97  
    1.98 -lemma union_insert [code]:
    1.99 -  "union (Set xs) A = foldl (\<lambda>A x. insert x A) A xs"
   1.100 +lemma inter_project [code]:
   1.101 +  "inter A (Set xs) = Set (List.filter (member A) xs)"
   1.102 +  "inter A (Coset xs) = foldl (\<lambda>A x. remove x A) A xs"
   1.103  proof -
   1.104 -  have "foldl (\<lambda>A x. Set.insert x A) (member A) xs =
   1.105 -    member (foldl (\<lambda>A x. Fset (Set.insert x (member A))) A xs)"
   1.106 +  show "inter A (Set xs) = Set (List.filter (member A) xs)"
   1.107 +    by (simp add: inter project_def Set_def)
   1.108 +  have "foldl (\<lambda>A x. List_Set.remove x A) (member A) xs =
   1.109 +    member (foldl (\<lambda>A x. Fset (List_Set.remove x (member A))) A xs)"
   1.110      by (rule foldl_apply_inv) simp
   1.111 -  then show ?thesis by (simp add: union_set)
   1.112 +  then show "inter A (Coset xs) = foldl (\<lambda>A x. remove x A) A xs"
   1.113 +    by (simp add: Diff_eq [symmetric] minus_set)
   1.114  qed
   1.115  
   1.116  definition subtract :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
   1.117 @@ -152,25 +169,50 @@
   1.118  
   1.119  lemma subtract_remove [code]:
   1.120    "subtract (Set xs) A = foldl (\<lambda>A x. remove x A) A xs"
   1.121 +  "subtract (Coset xs) A = Set (List.filter (member A) xs)"
   1.122  proof -
   1.123    have "foldl (\<lambda>A x. List_Set.remove x A) (member A) xs =
   1.124      member (foldl (\<lambda>A x. Fset (List_Set.remove x (member A))) A xs)"
   1.125      by (rule foldl_apply_inv) simp
   1.126 -  then show ?thesis by (simp add: minus_set)
   1.127 +  then show "subtract (Set xs) A = foldl (\<lambda>A x. remove x A) A xs"
   1.128 +    by (simp add: minus_set)
   1.129 +  show "subtract (Coset xs) A = Set (List.filter (member A) xs)"
   1.130 +    by (auto simp add: Coset_def Set_def)
   1.131 +qed
   1.132 +
   1.133 +definition union :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
   1.134 +  [simp]: "union A B = Fset (member A \<union> member B)"
   1.135 +
   1.136 +lemma union_insert [code]:
   1.137 +  "union (Set xs) A = foldl (\<lambda>A x. insert x A) A xs"
   1.138 +  "union (Coset xs) A = Coset (List.filter (Not \<circ> member A) xs)"
   1.139 +proof -
   1.140 +  have "foldl (\<lambda>A x. Set.insert x A) (member A) xs =
   1.141 +    member (foldl (\<lambda>A x. Fset (Set.insert x (member A))) A xs)"
   1.142 +    by (rule foldl_apply_inv) simp
   1.143 +  then show "union (Set xs) A = foldl (\<lambda>A x. insert x A) A xs"
   1.144 +    by (simp add: union_set)
   1.145 +  show "union (Coset xs) A = Coset (List.filter (Not \<circ> member A) xs)"
   1.146 +    by (auto simp add: Coset_def)
   1.147  qed
   1.148  
   1.149  definition Inter :: "'a fset fset \<Rightarrow> 'a fset" where
   1.150    [simp]: "Inter A = Fset (Complete_Lattice.Inter (member ` member A))"
   1.151  
   1.152  lemma Inter_inter [code]:
   1.153 -  "Inter (Set (A # As)) = foldl inter A As"
   1.154 +  "Inter (Set As) = foldl inter (Coset []) As"
   1.155 +  "Inter (Coset []) = empty"
   1.156  proof -
   1.157 +  have [simp]: "Coset [] = Fset UNIV"
   1.158 +    by (simp add: Coset_def)
   1.159    note Inter_image_eq [simp del] set_map [simp del] set.simps [simp del]
   1.160 -  have "foldl (op \<inter>) (member A) (List.map member As) = 
   1.161 -    member (foldl (\<lambda>B A. Fset (member B \<inter> A)) A (List.map member As))"
   1.162 +  have "foldl (op \<inter>) (member (Coset [])) (List.map member As) = 
   1.163 +    member (foldl (\<lambda>B A. Fset (member B \<inter> A)) (Coset []) (List.map member As))"
   1.164      by (rule foldl_apply_inv) simp
   1.165 -  then show ?thesis
   1.166 -    by (simp add: Inter_set image_set inter_def_raw inter foldl_map)
   1.167 +  then show "Inter (Set As) = foldl inter (Coset []) As"
   1.168 +    by (simp add: Inter_set image_set inter inter_def_raw foldl_map)
   1.169 +  show "Inter (Coset []) = empty"
   1.170 +    by simp
   1.171  qed
   1.172  
   1.173  definition Union :: "'a fset fset \<Rightarrow> 'a fset" where
   1.174 @@ -178,13 +220,18 @@
   1.175  
   1.176  lemma Union_union [code]:
   1.177    "Union (Set As) = foldl union empty As"
   1.178 +  "Union (Coset []) = Coset []"
   1.179  proof -
   1.180 +  have [simp]: "Coset [] = Fset UNIV"
   1.181 +    by (simp add: Coset_def)
   1.182    note Union_image_eq [simp del] set_map [simp del]
   1.183    have "foldl (op \<union>) (member empty) (List.map member As) = 
   1.184      member (foldl (\<lambda>B A. Fset (member B \<union> A)) empty (List.map member As))"
   1.185      by (rule foldl_apply_inv) simp
   1.186 -  then show ?thesis
   1.187 +  then show "Union (Set As) = foldl union empty As"
   1.188      by (simp add: Union_set image_set union_def_raw foldl_map)
   1.189 +  show "Union (Coset []) = Coset []"
   1.190 +    by simp
   1.191  qed
   1.192  
   1.193  
   1.194 @@ -221,11 +268,6 @@
   1.195    by (simp add: List_Set.project_def)
   1.196  declare filter_def [simp del]
   1.197  
   1.198 -lemma inter_simp [simp]:
   1.199 -  "inter A B = Fset (member A \<inter> member B)"
   1.200 -  by (simp add: inter)
   1.201 -declare inter_def [simp del]
   1.202 -
   1.203  declare mem_def [simp del]
   1.204  
   1.205  
     2.1 --- a/src/HOL/Library/List_Set.thy	Mon Oct 05 17:28:59 2009 +0100
     2.2 +++ b/src/HOL/Library/List_Set.thy	Tue Oct 06 15:59:12 2009 +0200
     2.3 @@ -65,10 +65,18 @@
     2.4    "Set.insert x (set xs) = set (insert x xs)"
     2.5    by (auto simp add: insert_def)
     2.6  
     2.7 +lemma insert_set_compl:
     2.8 +  "Set.insert x (- set xs) = - set (List_Set.remove_all x xs)"
     2.9 +  by (auto simp del: mem_def simp add: remove_all_def)
    2.10 +
    2.11  lemma remove_set:
    2.12    "remove x (set xs) = set (remove_all x xs)"
    2.13    by (auto simp add: remove_def remove_all_def)
    2.14  
    2.15 +lemma remove_set_compl:
    2.16 +  "List_Set.remove x (- set xs) = - set (List_Set.insert x xs)"
    2.17 +  by (auto simp del: mem_def simp add: remove_def List_Set.insert_def)
    2.18 +
    2.19  lemma image_set:
    2.20    "image f (set xs) = set (map f xs)"
    2.21    by simp
    2.22 @@ -98,14 +106,12 @@
    2.23  qed
    2.24  
    2.25  lemma Inter_set:
    2.26 -  "Inter (set (A # As)) = foldl (op \<inter>) A As"
    2.27 +  "Inter (set As) = foldl (op \<inter>) UNIV As"
    2.28  proof -
    2.29 -  have "finite (set (A # As))" by simp
    2.30 -  moreover have "fold (op \<inter>) UNIV (set (A # As)) = foldl (\<lambda>y x. x \<inter> y) UNIV (A # As)"
    2.31 +  have "fold (op \<inter>) UNIV (set As) = foldl (\<lambda>y x. x \<inter> y) UNIV As"
    2.32      by (rule fun_left_comm_idem.fold_set, unfold_locales, auto)
    2.33 -  ultimately have "Inter (set (A # As)) = foldl (op \<inter>) UNIV (A # As)"
    2.34 -    by (simp only: Inter_fold_inter Int_commute)
    2.35 -  then show ?thesis by simp
    2.36 +  then show ?thesis
    2.37 +    by (simp only: Inter_fold_inter finite_set Int_commute)
    2.38  qed
    2.39  
    2.40  lemma Union_set:
    2.41 @@ -118,14 +124,12 @@
    2.42  qed
    2.43  
    2.44  lemma INTER_set:
    2.45 -  "INTER (set (A # As)) f = foldl (\<lambda>B A. f A \<inter> B) (f A) As"
    2.46 +  "INTER (set As) f = foldl (\<lambda>B A. f A \<inter> B) UNIV As"
    2.47  proof -
    2.48 -  have "finite (set (A # As))" by simp
    2.49 -  moreover have "fold (\<lambda>A. op \<inter> (f A)) UNIV (set (A # As)) = foldl (\<lambda>B A. f A \<inter> B) UNIV (A # As)"
    2.50 +  have "fold (\<lambda>A. op \<inter> (f A)) UNIV (set As) = foldl (\<lambda>B A. f A \<inter> B) UNIV As"
    2.51      by (rule fun_left_comm_idem.fold_set, unfold_locales, auto)
    2.52 -  ultimately have "INTER (set (A # As)) f = foldl (\<lambda>B A. f A \<inter> B) UNIV (A # As)"
    2.53 -    by (simp only: INTER_fold_inter) 
    2.54 -  then show ?thesis by simp
    2.55 +  then show ?thesis
    2.56 +    by (simp only: INTER_fold_inter finite_set)
    2.57  qed
    2.58  
    2.59  lemma UNION_set: