src/HOL/Library/List_Cset.thy
changeset 44558 cc878a312673
parent 44556 c0fd385a41f4
child 44560 1711be44e76a
     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