src/HOL/Library/List_Cset.thy
changeset 43971 892030194015
parent 43307 1a32a953cef1
child 43979 9f27d2bf4087
     1.1 --- a/src/HOL/Library/List_Cset.thy	Mon Jul 25 14:10:12 2011 +0200
     1.2 +++ b/src/HOL/Library/List_Cset.thy	Mon Jul 25 16:55:48 2011 +0200
     1.3 @@ -8,15 +8,7 @@
     1.4  begin
     1.5  
     1.6  declare mem_def [simp]
     1.7 -
     1.8 -definition set :: "'a list \<Rightarrow> 'a Cset.set" where
     1.9 -  "set xs = Set (List.set xs)"
    1.10 -hide_const (open) set
    1.11 -
    1.12 -lemma member_set [simp]:
    1.13 -  "member (List_Cset.set xs) = set xs"
    1.14 -  by (simp add: set_def)
    1.15 -hide_fact (open) member_set
    1.16 +declare Cset.set_code [code del]
    1.17  
    1.18  definition coset :: "'a list \<Rightarrow> 'a Cset.set" where
    1.19    "coset xs = Set (- set xs)"
    1.20 @@ -27,10 +19,10 @@
    1.21    by (simp add: coset_def)
    1.22  hide_fact (open) member_coset
    1.23  
    1.24 -code_datatype List_Cset.set List_Cset.coset
    1.25 +code_datatype Cset.set List_Cset.coset
    1.26  
    1.27  lemma member_code [code]:
    1.28 -  "member (List_Cset.set xs) = List.member xs"
    1.29 +  "member (Cset.set xs) = List.member xs"
    1.30    "member (List_Cset.coset xs) = Not \<circ> List.member xs"
    1.31    by (simp_all add: fun_eq_iff member_def fun_Compl_def bool_Compl_def)
    1.32  
    1.33 @@ -48,7 +40,7 @@
    1.34  definition (in term_syntax)
    1.35    setify :: "'a\<Colon>typerep list \<times> (unit \<Rightarrow> Code_Evaluation.term)
    1.36      \<Rightarrow> 'a Cset.set \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
    1.37 -  [code_unfold]: "setify xs = Code_Evaluation.valtermify List_Cset.set {\<cdot>} xs"
    1.38 +  [code_unfold]: "setify xs = Code_Evaluation.valtermify Cset.set {\<cdot>} xs"
    1.39  
    1.40  notation fcomp (infixl "\<circ>>" 60)
    1.41  notation scomp (infixl "\<circ>\<rightarrow>" 60)
    1.42 @@ -69,12 +61,12 @@
    1.43  subsection {* Basic operations *}
    1.44  
    1.45  lemma is_empty_set [code]:
    1.46 -  "Cset.is_empty (List_Cset.set xs) \<longleftrightarrow> List.null xs"
    1.47 +  "Cset.is_empty (Cset.set xs) \<longleftrightarrow> List.null xs"
    1.48    by (simp add: is_empty_set null_def)
    1.49  hide_fact (open) is_empty_set
    1.50  
    1.51  lemma empty_set [code]:
    1.52 -  "bot = List_Cset.set []"
    1.53 +  "Cset.empty = Cset.set []"
    1.54    by (simp add: set_def)
    1.55  hide_fact (open) empty_set
    1.56  
    1.57 @@ -84,63 +76,87 @@
    1.58  hide_fact (open) UNIV_set
    1.59  
    1.60  lemma remove_set [code]:
    1.61 -  "Cset.remove x (List_Cset.set xs) = List_Cset.set (removeAll x xs)"
    1.62 +  "Cset.remove x (Cset.set xs) = Cset.set (removeAll x xs)"
    1.63    "Cset.remove x (List_Cset.coset xs) = List_Cset.coset (List.insert x xs)"
    1.64 -by (simp_all add: set_def coset_def)
    1.65 +by (simp_all add: Cset.set_def coset_def)
    1.66    (metis List.set_insert More_Set.remove_def remove_set_compl)
    1.67  
    1.68  lemma insert_set [code]:
    1.69 -  "Cset.insert x (List_Cset.set xs) = List_Cset.set (List.insert x xs)"
    1.70 +  "Cset.insert x (Cset.set xs) = Cset.set (List.insert x xs)"
    1.71    "Cset.insert x (List_Cset.coset xs) = List_Cset.coset (removeAll x xs)"
    1.72 -  by (simp_all add: set_def coset_def)
    1.73 +  by (simp_all add: Cset.set_def coset_def)
    1.74  
    1.75  lemma map_set [code]:
    1.76 -  "Cset.map f (List_Cset.set xs) = List_Cset.set (remdups (List.map f xs))"
    1.77 -  by (simp add: set_def)
    1.78 +  "Cset.map f (Cset.set xs) = Cset.set (remdups (List.map f xs))"
    1.79 +  by (simp add: Cset.set_def)
    1.80    
    1.81  lemma filter_set [code]:
    1.82 -  "Cset.filter P (List_Cset.set xs) = List_Cset.set (List.filter P xs)"
    1.83 -  by (simp add: set_def project_set)
    1.84 +  "Cset.filter P (Cset.set xs) = Cset.set (List.filter P xs)"
    1.85 +  by (simp add: Cset.set_def project_set)
    1.86  
    1.87  lemma forall_set [code]:
    1.88 -  "Cset.forall P (List_Cset.set xs) \<longleftrightarrow> list_all P xs"
    1.89 -  by (simp add: set_def list_all_iff)
    1.90 +  "Cset.forall P (Cset.set xs) \<longleftrightarrow> list_all P xs"
    1.91 +  by (simp add: Cset.set_def list_all_iff)
    1.92  
    1.93  lemma exists_set [code]:
    1.94 -  "Cset.exists P (List_Cset.set xs) \<longleftrightarrow> list_ex P xs"
    1.95 -  by (simp add: set_def list_ex_iff)
    1.96 +  "Cset.exists P (Cset.set xs) \<longleftrightarrow> list_ex P xs"
    1.97 +  by (simp add: Cset.set_def list_ex_iff)
    1.98  
    1.99  lemma card_set [code]:
   1.100 -  "Cset.card (List_Cset.set xs) = length (remdups xs)"
   1.101 +  "Cset.card (Cset.set xs) = length (remdups xs)"
   1.102  proof -
   1.103    have "Finite_Set.card (set (remdups xs)) = length (remdups xs)"
   1.104      by (rule distinct_card) simp
   1.105 -  then show ?thesis by (simp add: set_def)
   1.106 +  then show ?thesis by (simp add: Cset.set_def)
   1.107  qed
   1.108  
   1.109  lemma compl_set [simp, code]:
   1.110 -  "- List_Cset.set xs = List_Cset.coset xs"
   1.111 -  by (simp add: set_def coset_def)
   1.112 +  "- Cset.set xs = List_Cset.coset xs"
   1.113 +  by (simp add: Cset.set_def coset_def)
   1.114  
   1.115  lemma compl_coset [simp, code]:
   1.116 -  "- List_Cset.coset xs = List_Cset.set xs"
   1.117 -  by (simp add: set_def coset_def)
   1.118 +  "- List_Cset.coset xs = Cset.set xs"
   1.119 +  by (simp add: Cset.set_def coset_def)
   1.120  
   1.121  context complete_lattice
   1.122  begin
   1.123  
   1.124  lemma Infimum_inf [code]:
   1.125 -  "Infimum (List_Cset.set As) = foldr inf As top"
   1.126 +  "Infimum (Cset.set As) = foldr inf As top"
   1.127    "Infimum (List_Cset.coset []) = bot"
   1.128    by (simp_all add: Inf_set_foldr Inf_UNIV)
   1.129  
   1.130  lemma Supremum_sup [code]:
   1.131 -  "Supremum (List_Cset.set As) = foldr sup As bot"
   1.132 +  "Supremum (Cset.set As) = foldr sup As bot"
   1.133    "Supremum (List_Cset.coset []) = top"
   1.134    by (simp_all add: Sup_set_foldr Sup_UNIV)
   1.135  
   1.136  end
   1.137  
   1.138 +declare single_code [code del]
   1.139 +lemma single_set [code]:
   1.140 +  "Cset.single a = Cset.set [a]"
   1.141 +by(simp add: Cset.single_code)
   1.142 +hide_fact (open) single_set
   1.143 +
   1.144 +lemma bind_set [code]:
   1.145 +  "Cset.bind (Cset.set xs) f = foldl (\<lambda>A x. sup A (f x)) (Cset.set []) xs"
   1.146 +proof(rule sym)
   1.147 +  show "foldl (\<lambda>A x. sup A (f x)) (Cset.set []) xs = Cset.bind (Cset.set xs) f"
   1.148 +    by(induct xs rule: rev_induct)(auto simp add: Cset.bind_def Cset.set_def)
   1.149 +qed
   1.150 +hide_fact (open) bind_set
   1.151 +
   1.152 +lemma pred_of_cset_set [code]:
   1.153 +  "pred_of_cset (Cset.set xs) = foldr sup (map Predicate.single xs) bot"
   1.154 +proof -
   1.155 +  have "pred_of_cset (Cset.set xs) = Predicate.Pred (\<lambda>x. x \<in> set xs)"
   1.156 +    by(auto simp add: Cset.pred_of_cset_def mem_def)
   1.157 +  moreover have "foldr sup (map Predicate.single xs) bot = \<dots>"
   1.158 +    by(induct xs)(auto simp add: bot_pred_def simp del: mem_def intro: pred_eqI, simp)
   1.159 +  ultimately show ?thesis by(simp)
   1.160 +qed
   1.161 +hide_fact (open) pred_of_cset_set
   1.162  
   1.163  subsection {* Derived operations *}
   1.164  
   1.165 @@ -171,11 +187,11 @@
   1.166  subsection {* Functorial operations *}
   1.167  
   1.168  lemma inter_project [code]:
   1.169 -  "inf A (List_Cset.set xs) = List_Cset.set (List.filter (Cset.member A) xs)"
   1.170 +  "inf A (Cset.set xs) = Cset.set (List.filter (Cset.member A) xs)"
   1.171    "inf A (List_Cset.coset xs) = foldr Cset.remove xs A"
   1.172  proof -
   1.173 -  show "inf A (List_Cset.set xs) = List_Cset.set (List.filter (member A) xs)"
   1.174 -    by (simp add: inter project_def set_def)
   1.175 +  show "inf A (Cset.set xs) = Cset.set (List.filter (member A) xs)"
   1.176 +    by (simp add: inter project_def Cset.set_def)
   1.177    have *: "\<And>x::'a. Cset.remove = (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member)"
   1.178      by (simp add: fun_eq_iff More_Set.remove_def)
   1.179    have "member \<circ> fold (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member) xs =
   1.180 @@ -193,12 +209,12 @@
   1.181  qed
   1.182  
   1.183  lemma subtract_remove [code]:
   1.184 -  "A - List_Cset.set xs = foldr Cset.remove xs A"
   1.185 -  "A - List_Cset.coset xs = List_Cset.set (List.filter (member A) xs)"
   1.186 +  "A - Cset.set xs = foldr Cset.remove xs A"
   1.187 +  "A - List_Cset.coset xs = Cset.set (List.filter (member A) xs)"
   1.188    by (simp_all only: diff_eq compl_set compl_coset inter_project)
   1.189  
   1.190  lemma union_insert [code]:
   1.191 -  "sup (List_Cset.set xs) A = foldr Cset.insert xs A"
   1.192 +  "sup (Cset.set xs) A = foldr Cset.insert xs A"
   1.193    "sup (List_Cset.coset xs) A = List_Cset.coset (List.filter (Not \<circ> member A) xs)"
   1.194  proof -
   1.195    have *: "\<And>x::'a. Cset.insert = (\<lambda>x. Set \<circ> Set.insert x \<circ> member)"
   1.196 @@ -209,11 +225,11 @@
   1.197    then have "fold Set.insert xs (member A) =
   1.198      member (fold (\<lambda>x. Set \<circ> Set.insert x \<circ> member) xs A)"
   1.199      by (simp add: fun_eq_iff)
   1.200 -  then have "sup (List_Cset.set xs) A = fold Cset.insert xs A"
   1.201 +  then have "sup (Cset.set xs) A = fold Cset.insert xs A"
   1.202      by (simp add: union_set *)
   1.203    moreover have "\<And>x y :: 'a. Cset.insert y \<circ> Cset.insert x = Cset.insert x \<circ> Cset.insert y"
   1.204      by (auto simp add: * intro: ext)
   1.205 -  ultimately show "sup (List_Cset.set xs) A = foldr Cset.insert xs A"
   1.206 +  ultimately show "sup (Cset.set xs) A = foldr Cset.insert xs A"
   1.207      by (simp add: foldr_fold)
   1.208    show "sup (List_Cset.coset xs) A = List_Cset.coset (List.filter (Not \<circ> member A) xs)"
   1.209      by (auto simp add: coset_def)