added operations to Cset with code equations in backing implementations
authorAndreas Lochbihler
Mon Jul 25 16:55:48 2011 +0200 (2011-07-25)
changeset 43971892030194015
parent 43966 bb11faa6a79e
child 43972 24a3ddc79a5c
added operations to Cset with code equations in backing implementations
src/HOL/Library/Cset.thy
src/HOL/Library/Dlist_Cset.thy
src/HOL/Library/List_Cset.thy
     1.1 --- a/src/HOL/Library/Cset.thy	Mon Jul 25 14:10:12 2011 +0200
     1.2 +++ b/src/HOL/Library/Cset.thy	Mon Jul 25 16:55:48 2011 +0200
     1.3 @@ -86,6 +86,12 @@
     1.4  
     1.5  subsection {* Basic operations *}
     1.6  
     1.7 +abbreviation empty :: "'a Cset.set" where "empty \<equiv> bot"
     1.8 +hide_const (open) empty
     1.9 +
    1.10 +abbreviation UNIV :: "'a Cset.set" where "UNIV \<equiv> top"
    1.11 +hide_const (open) UNIV
    1.12 +
    1.13  definition is_empty :: "'a Cset.set \<Rightarrow> bool" where
    1.14    [simp]: "is_empty A \<longleftrightarrow> More_Set.is_empty (member A)"
    1.15  
    1.16 @@ -124,9 +130,42 @@
    1.17  
    1.18  end
    1.19  
    1.20 +subsection {* More operations *}
    1.21 +
    1.22 +text {* conversion from @{typ "'a list"} *}
    1.23 +
    1.24 +definition set :: "'a list \<Rightarrow> 'a Cset.set" where
    1.25 +  "set xs = Set (List.set xs)"
    1.26 +hide_const (open) set
    1.27 +
    1.28 +text {* conversion from @{typ "'a Predicate.pred"} *}
    1.29 +
    1.30 +definition pred_of_cset :: "'a Cset.set \<Rightarrow> 'a Predicate.pred"
    1.31 +where [code del]: "pred_of_cset = Predicate.Pred \<circ> Cset.member"
    1.32 +
    1.33 +definition of_pred :: "'a Predicate.pred \<Rightarrow> 'a Cset.set"
    1.34 +where "of_pred = Cset.Set \<circ> Predicate.eval"
    1.35 +
    1.36 +definition of_seq :: "'a Predicate.seq \<Rightarrow> 'a Cset.set"
    1.37 +where "of_seq = of_pred \<circ> Predicate.pred_of_seq"
    1.38 +
    1.39 +text {* monad operations *}
    1.40 +
    1.41 +definition single :: "'a \<Rightarrow> 'a Cset.set" where
    1.42 +  "single a = Set {a}"
    1.43 +
    1.44 +definition bind :: "'a Cset.set \<Rightarrow> ('a \<Rightarrow> 'b Cset.set) \<Rightarrow> 'b Cset.set"
    1.45 +                (infixl "\<guillemotright>=" 70)
    1.46 +  where "A \<guillemotright>= f = Set (\<Union>x \<in> member A. member (f x))"
    1.47  
    1.48  subsection {* Simplified simprules *}
    1.49  
    1.50 +lemma empty_simp [simp]: "member Cset.empty = {}"
    1.51 +  by(simp)
    1.52 +
    1.53 +lemma UNIV_simp [simp]: "member Cset.UNIV = UNIV"
    1.54 +  by simp
    1.55 +
    1.56  lemma is_empty_simp [simp]:
    1.57    "is_empty A \<longleftrightarrow> member A = {}"
    1.58    by (simp add: More_Set.is_empty_def)
    1.59 @@ -142,10 +181,103 @@
    1.60    by (simp add: More_Set.project_def)
    1.61  declare filter_def [simp del]
    1.62  
    1.63 +lemma member_set [simp]:
    1.64 +  "member (Cset.set xs) = set xs"
    1.65 +  by (simp add: set_def)
    1.66 +hide_fact (open) member_set set_def
    1.67 +
    1.68 +lemma set_simps [simp]:
    1.69 +  "Cset.set [] = Cset.empty"
    1.70 +  "Cset.set (x # xs) = insert x (Cset.set xs)"
    1.71 +by(simp_all add: Cset.set_def)
    1.72 +
    1.73 +lemma member_SUPR [simp]:
    1.74 +  "member (SUPR A f) = SUPR A (member \<circ> f)"
    1.75 +unfolding SUPR_def by simp
    1.76 +
    1.77 +lemma member_bind [simp]:
    1.78 +  "member (P \<guillemotright>= f) = member (SUPR (member P) f)"
    1.79 +by (simp add: bind_def Cset.set_eq_iff)
    1.80 +
    1.81 +lemma member_single [simp]:
    1.82 +  "member (single a) = {a}"
    1.83 +by(simp add: single_def)
    1.84 +
    1.85 +lemma single_sup_simps [simp]:
    1.86 +  shows single_sup: "sup (single a) A = insert a A"
    1.87 +  and sup_single: "sup A (single a) = insert a A"
    1.88 +by(auto simp add: Cset.set_eq_iff)
    1.89 +
    1.90 +lemma single_bind [simp]:
    1.91 +  "single a \<guillemotright>= B = B a"
    1.92 +by(simp add: bind_def single_def)
    1.93 +
    1.94 +lemma bind_bind:
    1.95 +  "(A \<guillemotright>= B) \<guillemotright>= C = A \<guillemotright>= (\<lambda>x. B x \<guillemotright>= C)"
    1.96 +by(simp add: bind_def)
    1.97 +
    1.98 +lemma bind_single [simp]:
    1.99 +  "A \<guillemotright>= single = A"
   1.100 +by(simp add: bind_def single_def)
   1.101 +
   1.102 +lemma bind_const: "A \<guillemotright>= (\<lambda>_. B) = (if Cset.is_empty A then Cset.empty else B)"
   1.103 +by(auto simp add: Cset.set_eq_iff)
   1.104 +
   1.105 +lemma empty_bind [simp]:
   1.106 +  "Cset.empty \<guillemotright>= f = Cset.empty"
   1.107 +by(simp add: Cset.set_eq_iff)
   1.108 +
   1.109 +lemma member_of_pred [simp]:
   1.110 +  "member (of_pred P) = {x. Predicate.eval P x}"
   1.111 +by(simp add: of_pred_def Collect_def)
   1.112 +
   1.113 +lemma member_of_seq [simp]:
   1.114 +  "member (of_seq xq) = {x. Predicate.member xq x}"
   1.115 +by(simp add: of_seq_def eval_member)
   1.116 +
   1.117 +lemma eval_pred_of_cset [simp]: 
   1.118 +  "Predicate.eval (pred_of_cset A) = Cset.member A"
   1.119 +by(simp add: pred_of_cset_def)
   1.120 +
   1.121 +subsection {* Default implementations *}
   1.122 +
   1.123 +lemma set_code [code]:
   1.124 +  "Cset.set = foldl (\<lambda>A x. insert x A) Cset.empty"
   1.125 +proof(rule ext, rule Cset.set_eqI)
   1.126 +  fix xs
   1.127 +  show "member (Cset.set xs) = member (foldl (\<lambda>A x. insert x A) Cset.empty xs)"
   1.128 +    by(induct xs rule: rev_induct)(simp_all)
   1.129 +qed
   1.130 +
   1.131 +lemma single_code [code]:
   1.132 +  "single a = insert a Cset.empty"
   1.133 +by(simp add: Cset.single_def)
   1.134 +
   1.135 +lemma of_pred_code [code]:
   1.136 +  "of_pred (Predicate.Seq f) = (case f () of
   1.137 +     Predicate.Empty \<Rightarrow> Cset.empty
   1.138 +   | Predicate.Insert x P \<Rightarrow> Cset.insert x (of_pred P)
   1.139 +   | Predicate.Join P xq \<Rightarrow> sup (of_pred P) (of_seq xq))"
   1.140 +by(auto split: seq.split 
   1.141 +        simp add: Predicate.Seq_def of_pred_def eval_member Cset.set_eq_iff)
   1.142 +
   1.143 +lemma of_seq_code [code]:
   1.144 +  "of_seq Predicate.Empty = Cset.empty"
   1.145 +  "of_seq (Predicate.Insert x P) = Cset.insert x (of_pred P)"
   1.146 +  "of_seq (Predicate.Join P xq) = sup (of_pred P) (of_seq xq)"
   1.147 +by(auto simp add: of_seq_def of_pred_def Cset.set_eq_iff)
   1.148 +
   1.149  declare mem_def [simp del]
   1.150  
   1.151 +no_notation bind (infixl "\<guillemotright>=" 70)
   1.152  
   1.153  hide_const (open) is_empty insert remove map filter forall exists card
   1.154 -  Inter Union
   1.155 +  Inter Union bind single of_pred of_seq
   1.156 +
   1.157 +hide_fact (open) set_def pred_of_cset_def of_pred_def of_seq_def single_def 
   1.158 +  bind_def empty_simp UNIV_simp member_set set_simps member_SUPR member_bind 
   1.159 +  member_single single_sup_simps single_sup sup_single single_bind
   1.160 +  bind_bind bind_single bind_const empty_bind member_of_pred member_of_seq
   1.161 +  eval_pred_of_cset set_code single_code of_pred_code of_seq_code
   1.162  
   1.163  end
     2.1 --- a/src/HOL/Library/Dlist_Cset.thy	Mon Jul 25 14:10:12 2011 +0200
     2.2 +++ b/src/HOL/Library/Dlist_Cset.thy	Mon Jul 25 16:55:48 2011 +0200
     2.3 @@ -7,7 +7,7 @@
     2.4  begin
     2.5  
     2.6  definition Set :: "'a dlist \<Rightarrow> 'a Cset.set" where
     2.7 -  "Set dxs = List_Cset.set (list_of_dlist dxs)"
     2.8 +  "Set dxs = Cset.set (list_of_dlist dxs)"
     2.9  
    2.10  definition Coset :: "'a dlist \<Rightarrow> 'a Cset.set" where
    2.11    "Coset dxs = List_Cset.coset (list_of_dlist dxs)"
    2.12 @@ -27,6 +27,9 @@
    2.13  declare forall_set [code del]
    2.14  declare exists_set [code del]
    2.15  declare card_set [code del]
    2.16 +declare List_Cset.single_set [code del]
    2.17 +declare List_Cset.bind_set [code del]
    2.18 +declare List_Cset.pred_of_cset_set [code del]
    2.19  declare inter_project [code del]
    2.20  declare subtract_remove [code del]
    2.21  declare union_insert [code del]
    2.22 @@ -50,7 +53,7 @@
    2.23    by (simp add: Coset_def member_set not_set_compl)
    2.24  
    2.25  lemma Set_dlist_of_list [code]:
    2.26 -  "List_Cset.set xs = Set (dlist_of_list xs)"
    2.27 +  "Cset.set xs = Set (dlist_of_list xs)"
    2.28    by (rule Cset.set_eqI) simp
    2.29  
    2.30  lemma Coset_dlist_of_list [code]:
    2.31 @@ -137,4 +140,16 @@
    2.32  
    2.33  end
    2.34  
    2.35 +declare Cset.single_code[code]
    2.36 +
    2.37 +lemma bind_set [code]:
    2.38 +  "Cset.bind (Dlist_Cset.Set xs) f = foldl (\<lambda>A x. sup A (f x)) Cset.empty (list_of_dlist xs)"
    2.39 +by(simp add: List_Cset.bind_set Dlist_Cset.Set_def)
    2.40 +hide_fact (open) bind_set
    2.41 +
    2.42 +lemma pred_of_cset_set [code]:
    2.43 +  "pred_of_cset (Dlist_Cset.Set xs) = foldr sup (map Predicate.single (list_of_dlist xs)) bot"
    2.44 +by(simp add: List_Cset.pred_of_cset_set Dlist_Cset.Set_def)
    2.45 +hide_fact (open) pred_of_cset_set
    2.46 +
    2.47  end
     3.1 --- a/src/HOL/Library/List_Cset.thy	Mon Jul 25 14:10:12 2011 +0200
     3.2 +++ b/src/HOL/Library/List_Cset.thy	Mon Jul 25 16:55:48 2011 +0200
     3.3 @@ -8,15 +8,7 @@
     3.4  begin
     3.5  
     3.6  declare mem_def [simp]
     3.7 -
     3.8 -definition set :: "'a list \<Rightarrow> 'a Cset.set" where
     3.9 -  "set xs = Set (List.set xs)"
    3.10 -hide_const (open) set
    3.11 -
    3.12 -lemma member_set [simp]:
    3.13 -  "member (List_Cset.set xs) = set xs"
    3.14 -  by (simp add: set_def)
    3.15 -hide_fact (open) member_set
    3.16 +declare Cset.set_code [code del]
    3.17  
    3.18  definition coset :: "'a list \<Rightarrow> 'a Cset.set" where
    3.19    "coset xs = Set (- set xs)"
    3.20 @@ -27,10 +19,10 @@
    3.21    by (simp add: coset_def)
    3.22  hide_fact (open) member_coset
    3.23  
    3.24 -code_datatype List_Cset.set List_Cset.coset
    3.25 +code_datatype Cset.set List_Cset.coset
    3.26  
    3.27  lemma member_code [code]:
    3.28 -  "member (List_Cset.set xs) = List.member xs"
    3.29 +  "member (Cset.set xs) = List.member xs"
    3.30    "member (List_Cset.coset xs) = Not \<circ> List.member xs"
    3.31    by (simp_all add: fun_eq_iff member_def fun_Compl_def bool_Compl_def)
    3.32  
    3.33 @@ -48,7 +40,7 @@
    3.34  definition (in term_syntax)
    3.35    setify :: "'a\<Colon>typerep list \<times> (unit \<Rightarrow> Code_Evaluation.term)
    3.36      \<Rightarrow> 'a Cset.set \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
    3.37 -  [code_unfold]: "setify xs = Code_Evaluation.valtermify List_Cset.set {\<cdot>} xs"
    3.38 +  [code_unfold]: "setify xs = Code_Evaluation.valtermify Cset.set {\<cdot>} xs"
    3.39  
    3.40  notation fcomp (infixl "\<circ>>" 60)
    3.41  notation scomp (infixl "\<circ>\<rightarrow>" 60)
    3.42 @@ -69,12 +61,12 @@
    3.43  subsection {* Basic operations *}
    3.44  
    3.45  lemma is_empty_set [code]:
    3.46 -  "Cset.is_empty (List_Cset.set xs) \<longleftrightarrow> List.null xs"
    3.47 +  "Cset.is_empty (Cset.set xs) \<longleftrightarrow> List.null xs"
    3.48    by (simp add: is_empty_set null_def)
    3.49  hide_fact (open) is_empty_set
    3.50  
    3.51  lemma empty_set [code]:
    3.52 -  "bot = List_Cset.set []"
    3.53 +  "Cset.empty = Cset.set []"
    3.54    by (simp add: set_def)
    3.55  hide_fact (open) empty_set
    3.56  
    3.57 @@ -84,63 +76,87 @@
    3.58  hide_fact (open) UNIV_set
    3.59  
    3.60  lemma remove_set [code]:
    3.61 -  "Cset.remove x (List_Cset.set xs) = List_Cset.set (removeAll x xs)"
    3.62 +  "Cset.remove x (Cset.set xs) = Cset.set (removeAll x xs)"
    3.63    "Cset.remove x (List_Cset.coset xs) = List_Cset.coset (List.insert x xs)"
    3.64 -by (simp_all add: set_def coset_def)
    3.65 +by (simp_all add: Cset.set_def coset_def)
    3.66    (metis List.set_insert More_Set.remove_def remove_set_compl)
    3.67  
    3.68  lemma insert_set [code]:
    3.69 -  "Cset.insert x (List_Cset.set xs) = List_Cset.set (List.insert x xs)"
    3.70 +  "Cset.insert x (Cset.set xs) = Cset.set (List.insert x xs)"
    3.71    "Cset.insert x (List_Cset.coset xs) = List_Cset.coset (removeAll x xs)"
    3.72 -  by (simp_all add: set_def coset_def)
    3.73 +  by (simp_all add: Cset.set_def coset_def)
    3.74  
    3.75  lemma map_set [code]:
    3.76 -  "Cset.map f (List_Cset.set xs) = List_Cset.set (remdups (List.map f xs))"
    3.77 -  by (simp add: set_def)
    3.78 +  "Cset.map f (Cset.set xs) = Cset.set (remdups (List.map f xs))"
    3.79 +  by (simp add: Cset.set_def)
    3.80    
    3.81  lemma filter_set [code]:
    3.82 -  "Cset.filter P (List_Cset.set xs) = List_Cset.set (List.filter P xs)"
    3.83 -  by (simp add: set_def project_set)
    3.84 +  "Cset.filter P (Cset.set xs) = Cset.set (List.filter P xs)"
    3.85 +  by (simp add: Cset.set_def project_set)
    3.86  
    3.87  lemma forall_set [code]:
    3.88 -  "Cset.forall P (List_Cset.set xs) \<longleftrightarrow> list_all P xs"
    3.89 -  by (simp add: set_def list_all_iff)
    3.90 +  "Cset.forall P (Cset.set xs) \<longleftrightarrow> list_all P xs"
    3.91 +  by (simp add: Cset.set_def list_all_iff)
    3.92  
    3.93  lemma exists_set [code]:
    3.94 -  "Cset.exists P (List_Cset.set xs) \<longleftrightarrow> list_ex P xs"
    3.95 -  by (simp add: set_def list_ex_iff)
    3.96 +  "Cset.exists P (Cset.set xs) \<longleftrightarrow> list_ex P xs"
    3.97 +  by (simp add: Cset.set_def list_ex_iff)
    3.98  
    3.99  lemma card_set [code]:
   3.100 -  "Cset.card (List_Cset.set xs) = length (remdups xs)"
   3.101 +  "Cset.card (Cset.set xs) = length (remdups xs)"
   3.102  proof -
   3.103    have "Finite_Set.card (set (remdups xs)) = length (remdups xs)"
   3.104      by (rule distinct_card) simp
   3.105 -  then show ?thesis by (simp add: set_def)
   3.106 +  then show ?thesis by (simp add: Cset.set_def)
   3.107  qed
   3.108  
   3.109  lemma compl_set [simp, code]:
   3.110 -  "- List_Cset.set xs = List_Cset.coset xs"
   3.111 -  by (simp add: set_def coset_def)
   3.112 +  "- Cset.set xs = List_Cset.coset xs"
   3.113 +  by (simp add: Cset.set_def coset_def)
   3.114  
   3.115  lemma compl_coset [simp, code]:
   3.116 -  "- List_Cset.coset xs = List_Cset.set xs"
   3.117 -  by (simp add: set_def coset_def)
   3.118 +  "- List_Cset.coset xs = Cset.set xs"
   3.119 +  by (simp add: Cset.set_def coset_def)
   3.120  
   3.121  context complete_lattice
   3.122  begin
   3.123  
   3.124  lemma Infimum_inf [code]:
   3.125 -  "Infimum (List_Cset.set As) = foldr inf As top"
   3.126 +  "Infimum (Cset.set As) = foldr inf As top"
   3.127    "Infimum (List_Cset.coset []) = bot"
   3.128    by (simp_all add: Inf_set_foldr Inf_UNIV)
   3.129  
   3.130  lemma Supremum_sup [code]:
   3.131 -  "Supremum (List_Cset.set As) = foldr sup As bot"
   3.132 +  "Supremum (Cset.set As) = foldr sup As bot"
   3.133    "Supremum (List_Cset.coset []) = top"
   3.134    by (simp_all add: Sup_set_foldr Sup_UNIV)
   3.135  
   3.136  end
   3.137  
   3.138 +declare single_code [code del]
   3.139 +lemma single_set [code]:
   3.140 +  "Cset.single a = Cset.set [a]"
   3.141 +by(simp add: Cset.single_code)
   3.142 +hide_fact (open) single_set
   3.143 +
   3.144 +lemma bind_set [code]:
   3.145 +  "Cset.bind (Cset.set xs) f = foldl (\<lambda>A x. sup A (f x)) (Cset.set []) xs"
   3.146 +proof(rule sym)
   3.147 +  show "foldl (\<lambda>A x. sup A (f x)) (Cset.set []) xs = Cset.bind (Cset.set xs) f"
   3.148 +    by(induct xs rule: rev_induct)(auto simp add: Cset.bind_def Cset.set_def)
   3.149 +qed
   3.150 +hide_fact (open) bind_set
   3.151 +
   3.152 +lemma pred_of_cset_set [code]:
   3.153 +  "pred_of_cset (Cset.set xs) = foldr sup (map Predicate.single xs) bot"
   3.154 +proof -
   3.155 +  have "pred_of_cset (Cset.set xs) = Predicate.Pred (\<lambda>x. x \<in> set xs)"
   3.156 +    by(auto simp add: Cset.pred_of_cset_def mem_def)
   3.157 +  moreover have "foldr sup (map Predicate.single xs) bot = \<dots>"
   3.158 +    by(induct xs)(auto simp add: bot_pred_def simp del: mem_def intro: pred_eqI, simp)
   3.159 +  ultimately show ?thesis by(simp)
   3.160 +qed
   3.161 +hide_fact (open) pred_of_cset_set
   3.162  
   3.163  subsection {* Derived operations *}
   3.164  
   3.165 @@ -171,11 +187,11 @@
   3.166  subsection {* Functorial operations *}
   3.167  
   3.168  lemma inter_project [code]:
   3.169 -  "inf A (List_Cset.set xs) = List_Cset.set (List.filter (Cset.member A) xs)"
   3.170 +  "inf A (Cset.set xs) = Cset.set (List.filter (Cset.member A) xs)"
   3.171    "inf A (List_Cset.coset xs) = foldr Cset.remove xs A"
   3.172  proof -
   3.173 -  show "inf A (List_Cset.set xs) = List_Cset.set (List.filter (member A) xs)"
   3.174 -    by (simp add: inter project_def set_def)
   3.175 +  show "inf A (Cset.set xs) = Cset.set (List.filter (member A) xs)"
   3.176 +    by (simp add: inter project_def Cset.set_def)
   3.177    have *: "\<And>x::'a. Cset.remove = (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member)"
   3.178      by (simp add: fun_eq_iff More_Set.remove_def)
   3.179    have "member \<circ> fold (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member) xs =
   3.180 @@ -193,12 +209,12 @@
   3.181  qed
   3.182  
   3.183  lemma subtract_remove [code]:
   3.184 -  "A - List_Cset.set xs = foldr Cset.remove xs A"
   3.185 -  "A - List_Cset.coset xs = List_Cset.set (List.filter (member A) xs)"
   3.186 +  "A - Cset.set xs = foldr Cset.remove xs A"
   3.187 +  "A - List_Cset.coset xs = Cset.set (List.filter (member A) xs)"
   3.188    by (simp_all only: diff_eq compl_set compl_coset inter_project)
   3.189  
   3.190  lemma union_insert [code]:
   3.191 -  "sup (List_Cset.set xs) A = foldr Cset.insert xs A"
   3.192 +  "sup (Cset.set xs) A = foldr Cset.insert xs A"
   3.193    "sup (List_Cset.coset xs) A = List_Cset.coset (List.filter (Not \<circ> member A) xs)"
   3.194  proof -
   3.195    have *: "\<And>x::'a. Cset.insert = (\<lambda>x. Set \<circ> Set.insert x \<circ> member)"
   3.196 @@ -209,11 +225,11 @@
   3.197    then have "fold Set.insert xs (member A) =
   3.198      member (fold (\<lambda>x. Set \<circ> Set.insert x \<circ> member) xs A)"
   3.199      by (simp add: fun_eq_iff)
   3.200 -  then have "sup (List_Cset.set xs) A = fold Cset.insert xs A"
   3.201 +  then have "sup (Cset.set xs) A = fold Cset.insert xs A"
   3.202      by (simp add: union_set *)
   3.203    moreover have "\<And>x y :: 'a. Cset.insert y \<circ> Cset.insert x = Cset.insert x \<circ> Cset.insert y"
   3.204      by (auto simp add: * intro: ext)
   3.205 -  ultimately show "sup (List_Cset.set xs) A = foldr Cset.insert xs A"
   3.206 +  ultimately show "sup (Cset.set xs) A = foldr Cset.insert xs A"
   3.207      by (simp add: foldr_fold)
   3.208    show "sup (List_Cset.coset xs) A = List_Cset.coset (List.filter (Not \<circ> member A) xs)"
   3.209      by (auto simp add: coset_def)