src/HOL/Library/Cset.thy
changeset 46146 6baea4fca6bd
parent 46133 d9fe85d3d2cd
child 46884 154dc6ec0041
     1.1 --- a/src/HOL/Library/Cset.thy	Fri Jan 06 21:48:45 2012 +0100
     1.2 +++ b/src/HOL/Library/Cset.thy	Fri Jan 06 21:48:45 2012 +0100
     1.3 @@ -276,7 +276,7 @@
     1.4    fix xs :: "'a list"
     1.5    show "member (Cset.set xs) = member (fold insert xs Cset.empty)"
     1.6      by (simp add: fold_commute_apply [symmetric, where ?h = Set and ?g = Set.insert]
     1.7 -      fun_eq_iff Cset.set_def union_set [symmetric])
     1.8 +      fun_eq_iff Cset.set_def union_set_fold [symmetric])
     1.9  qed
    1.10  
    1.11  lemma single_code [code]:
    1.12 @@ -296,7 +296,7 @@
    1.13    "inf A (Cset.coset xs) = foldr Cset.remove xs A"
    1.14  proof -
    1.15    show "inf A (Cset.set xs) = Cset.set (List.filter (member A) xs)"
    1.16 -    by (simp add: inter project_def Cset.set_def member_def)
    1.17 +    by (simp add: project_def Cset.set_def member_def) auto
    1.18    have *: "\<And>x::'a. Cset.remove = (\<lambda>x. Set \<circ> Set.remove x \<circ> set_of)"
    1.19      by (simp add: fun_eq_iff Set.remove_def)
    1.20    have "set_of \<circ> fold (\<lambda>x. Set \<circ> Set.remove x \<circ> set_of) xs =
    1.21 @@ -306,7 +306,7 @@
    1.22      set_of (fold (\<lambda>x. Set \<circ> Set.remove x \<circ> set_of) xs A)"
    1.23      by (simp add: fun_eq_iff)
    1.24    then have "inf A (Cset.coset xs) = fold Cset.remove xs A"
    1.25 -    by (simp add: Diff_eq [symmetric] minus_set *)
    1.26 +    by (simp add: Diff_eq [symmetric] minus_set_fold *)
    1.27    moreover have "\<And>x y :: 'a. Cset.remove y \<circ> Cset.remove x = Cset.remove x \<circ> Cset.remove y"
    1.28      by (auto simp add: Set.remove_def *)
    1.29    ultimately show "inf A (Cset.coset xs) = foldr Cset.remove xs A"
    1.30 @@ -326,7 +326,7 @@
    1.31      set_of (fold (\<lambda>x. Set \<circ> Set.insert x \<circ> set_of) xs A)"
    1.32      by (simp add: fun_eq_iff)
    1.33    then have "sup (Cset.set xs) A = fold Cset.insert xs A"
    1.34 -    by (simp add: union_set *)
    1.35 +    by (simp add: union_set_fold *)
    1.36    moreover have "\<And>x y :: 'a. Cset.insert y \<circ> Cset.insert x = Cset.insert x \<circ> Cset.insert y"
    1.37      by (auto simp add: *)
    1.38    ultimately show "sup (Cset.set xs) A = foldr Cset.insert xs A"