summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Library/Executable_Set.thy

changeset 37023 | efc202e1677e |

parent 36176 | 3fe7e97ccca8 |

child 37024 | e938a0b5286e |

1.1 --- a/src/HOL/Library/Executable_Set.thy Thu May 20 16:35:53 2010 +0200 1.2 +++ b/src/HOL/Library/Executable_Set.thy Thu May 20 16:35:54 2010 +0200 1.3 @@ -50,8 +50,8 @@ 1.4 by simp 1.5 1.6 lemma [code]: 1.7 - "x \<in> Set xs \<longleftrightarrow> member x xs" 1.8 - "x \<in> Coset xs \<longleftrightarrow> \<not> member x xs" 1.9 + "x \<in> Set xs \<longleftrightarrow> member xs x" 1.10 + "x \<in> Coset xs \<longleftrightarrow> \<not> member xs x" 1.11 by (simp_all add: mem_iff) 1.12 1.13 definition is_empty :: "'a set \<Rightarrow> bool" where 1.14 @@ -232,36 +232,36 @@ 1.15 1.16 lemma inter_project [code]: 1.17 "inter A (Set xs) = Set (List.filter (\<lambda>x. x \<in> A) xs)" 1.18 - "inter A (Coset xs) = foldl (\<lambda>A x. remove x A) A xs" 1.19 - by (simp add: inter project_def, simp add: Diff_eq [symmetric] minus_set) 1.20 + "inter A (Coset xs) = foldr remove xs A" 1.21 + by (simp add: inter project_def) (simp add: Diff_eq [symmetric] minus_set_foldr) 1.22 1.23 lemma subtract_remove [code]: 1.24 - "subtract (Set xs) A = foldl (\<lambda>A x. remove x A) A xs" 1.25 + "subtract (Set xs) A = foldr remove xs A" 1.26 "subtract (Coset xs) A = Set (List.filter (\<lambda>x. x \<in> A) xs)" 1.27 - by (auto simp add: minus_set) 1.28 + by (auto simp add: minus_set_foldr) 1.29 1.30 lemma union_insert [code]: 1.31 - "union (Set xs) A = foldl (\<lambda>A x. insert x A) A xs" 1.32 + "union (Set xs) A = foldr insert xs A" 1.33 "union (Coset xs) A = Coset (List.filter (\<lambda>x. x \<notin> A) xs)" 1.34 - by (auto simp add: union_set) 1.35 + by (auto simp add: union_set_foldr) 1.36 1.37 lemma Inf_inf [code]: 1.38 - "Inf (Set xs) = foldl inf (top :: 'a::complete_lattice) xs" 1.39 + "Inf (Set xs) = foldr inf xs (top :: 'a::complete_lattice)" 1.40 "Inf (Coset []) = (bot :: 'a::complete_lattice)" 1.41 - by (simp_all add: Inf_UNIV Inf_set_fold) 1.42 + by (simp_all add: Inf_UNIV Inf_set_foldr) 1.43 1.44 lemma Sup_sup [code]: 1.45 - "Sup (Set xs) = foldl sup (bot :: 'a::complete_lattice) xs" 1.46 + "Sup (Set xs) = foldr sup xs (bot :: 'a::complete_lattice)" 1.47 "Sup (Coset []) = (top :: 'a::complete_lattice)" 1.48 - by (simp_all add: Sup_UNIV Sup_set_fold) 1.49 + by (simp_all add: Sup_UNIV Sup_set_foldr) 1.50 1.51 lemma Inter_inter [code]: 1.52 - "Inter (Set xs) = foldl inter (Coset []) xs" 1.53 + "Inter (Set xs) = foldr inter xs (Coset [])" 1.54 "Inter (Coset []) = empty" 1.55 unfolding Inter_def Inf_inf by simp_all 1.56 1.57 lemma Union_union [code]: 1.58 - "Union (Set xs) = foldl union empty xs" 1.59 + "Union (Set xs) = foldr union xs empty" 1.60 "Union (Coset []) = Coset []" 1.61 unfolding Union_def Sup_sup by simp_all 1.62