1.1 --- a/src/HOL/Library/Fset.thy	Sun Jan 31 14:51:30 2010 +0100
     1.2 +++ b/src/HOL/Library/Fset.thy	Sun Jan 31 14:51:31 2010 +0100
     1.3 @@ -126,17 +126,18 @@
     1.4    [simp]: "insert x A = Fset (Set.insert x (member A))"
     1.5  
     1.6  lemma insert_Set [code]:
     1.7 -  "insert x (Set xs) = Set (List_Set.insert x xs)"
     1.8 -  "insert x (Coset xs) = Coset (remove_all x xs)"
     1.9 -  by (simp_all add: Set_def Coset_def insert_set insert_set_compl)
    1.10 +  "insert x (Set xs) = Set (List.insert x xs)"
    1.11 +  "insert x (Coset xs) = Coset (removeAll x xs)"
    1.12 +  by (simp_all add: Set_def Coset_def set_insert)
    1.13  
    1.14  definition remove :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
    1.15    [simp]: "remove x A = Fset (List_Set.remove x (member A))"
    1.16  
    1.17  lemma remove_Set [code]:
    1.18 -  "remove x (Set xs) = Set (remove_all x xs)"
    1.19 -  "remove x (Coset xs) = Coset (List_Set.insert x xs)"
    1.20 -  by (simp_all add: Set_def Coset_def remove_set remove_set_compl)
    1.21 +  "remove x (Set xs) = Set (removeAll x xs)"
    1.22 +  "remove x (Coset xs) = Coset (List.insert x xs)"
    1.23 +  by (simp_all add: Set_def Coset_def remove_set_compl)
    1.24 +    (simp add: List_Set.remove_def)
    1.25  
    1.26  definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" where
    1.27    [simp]: "map f A = Fset (image f (member A))"
    1.28 @@ -203,7 +204,7 @@
    1.29      by (simp add: inter project_def Set_def)
    1.30    have "foldl (\<lambda>A x. List_Set.remove x A) (member A) xs =
    1.31      member (foldl (\<lambda>A x. Fset (List_Set.remove x (member A))) A xs)"
    1.32 -    by (rule foldl_apply_inv) simp
    1.33 +    by (rule foldl_apply) (simp add: expand_fun_eq)
    1.34    then show "inf A (Coset xs) = foldl (\<lambda>A x. remove x A) A xs"
    1.35      by (simp add: Diff_eq [symmetric] minus_set)
    1.36  qed
    1.37 @@ -214,7 +215,7 @@
    1.38  proof -
    1.39    have "foldl (\<lambda>A x. List_Set.remove x A) (member A) xs =
    1.40      member (foldl (\<lambda>A x. Fset (List_Set.remove x (member A))) A xs)"
    1.41 -    by (rule foldl_apply_inv) simp
    1.42 +    by (rule foldl_apply) (simp add: expand_fun_eq)
    1.43    then show "A - Set xs = foldl (\<lambda>A x. remove x A) A xs"
    1.44      by (simp add: minus_set)
    1.45    show "A - Coset xs = Set (List.filter (member A) xs)"
    1.46 @@ -227,7 +228,7 @@
    1.47  proof -
    1.48    have "foldl (\<lambda>A x. Set.insert x A) (member A) xs =
    1.49      member (foldl (\<lambda>A x. Fset (Set.insert x (member A))) A xs)"
    1.50 -    by (rule foldl_apply_inv) simp
    1.51 +    by (rule foldl_apply) (simp add: expand_fun_eq)
    1.52    then show "sup (Set xs) A = foldl (\<lambda>A x. insert x A) A xs"
    1.53      by (simp add: union_set)
    1.54    show "sup (Coset xs) A = Coset (List.filter (Not \<circ> member A) xs)"