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