src/HOL/Library/Cset.thy
changeset 44563 01b2732cf4ad
parent 44558 cc878a312673
child 45970 b6d0cff57d96
     1.1 --- a/src/HOL/Library/Cset.thy	Sun Aug 28 08:13:58 2011 +0200
     1.2 +++ b/src/HOL/Library/Cset.thy	Sun Aug 28 08:43:25 2011 +0200
     1.3 @@ -295,59 +295,55 @@
     1.4    "- Cset.coset xs = Cset.set xs"
     1.5    by (simp add: Cset.set_def Cset.coset_def)
     1.6  
     1.7 -lemma member_cset_of:
     1.8 -  "member = set_of"
     1.9 -  by (rule ext)+ (simp add: member_def mem_def)
    1.10 -
    1.11  lemma inter_project:
    1.12    "inf A (Cset.set xs) = Cset.set (List.filter (Cset.member A) xs)"
    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 -  have *: "\<And>x::'a. Cset.remove = (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member)"
    1.18 -    by (simp add: fun_eq_iff More_Set.remove_def member_cset_of)
    1.19 -  have "member \<circ> fold (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member) xs =
    1.20 -    fold More_Set.remove xs \<circ> member"
    1.21 -    by (rule fold_commute) (simp add: fun_eq_iff mem_def)
    1.22 -  then have "fold More_Set.remove xs (member A) = 
    1.23 -    member (fold (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member) xs A)"
    1.24 +  have *: "\<And>x::'a. Cset.remove = (\<lambda>x. Set \<circ> More_Set.remove x \<circ> set_of)"
    1.25 +    by (simp add: fun_eq_iff More_Set.remove_def)
    1.26 +  have "set_of \<circ> fold (\<lambda>x. Set \<circ> More_Set.remove x \<circ> set_of) xs =
    1.27 +    fold More_Set.remove xs \<circ> set_of"
    1.28 +    by (rule fold_commute) (simp add: fun_eq_iff)
    1.29 +  then have "fold More_Set.remove xs (set_of A) = 
    1.30 +    set_of (fold (\<lambda>x. Set \<circ> More_Set.remove x \<circ> set_of) xs A)"
    1.31      by (simp add: fun_eq_iff)
    1.32    then have "inf A (Cset.coset xs) = fold Cset.remove xs A"
    1.33 -    by (simp add: Diff_eq [symmetric] minus_set * member_cset_of)
    1.34 +    by (simp add: Diff_eq [symmetric] minus_set *)
    1.35    moreover have "\<And>x y :: 'a. Cset.remove y \<circ> Cset.remove x = Cset.remove x \<circ> Cset.remove y"
    1.36 -    by (auto simp add: More_Set.remove_def * member_cset_of)
    1.37 +    by (auto simp add: More_Set.remove_def *)
    1.38    ultimately show "inf A (Cset.coset xs) = foldr Cset.remove xs A"
    1.39      by (simp add: foldr_fold)
    1.40  qed
    1.41  
    1.42 +lemma union_insert:
    1.43 +  "sup (Cset.set xs) A = foldr Cset.insert xs A"
    1.44 +  "sup (Cset.coset xs) A = Cset.coset (List.filter (Not \<circ> member A) xs)"
    1.45 +proof -
    1.46 +  have *: "\<And>x::'a. Cset.insert = (\<lambda>x. Set \<circ> Set.insert x \<circ> set_of)"
    1.47 +    by (simp add: fun_eq_iff)
    1.48 +  have "set_of \<circ> fold (\<lambda>x. Set \<circ> Set.insert x \<circ> set_of) xs =
    1.49 +    fold Set.insert xs \<circ> set_of"
    1.50 +    by (rule fold_commute) (simp add: fun_eq_iff)
    1.51 +  then have "fold Set.insert xs (set_of A) =
    1.52 +    set_of (fold (\<lambda>x. Set \<circ> Set.insert x \<circ> set_of) xs A)"
    1.53 +    by (simp add: fun_eq_iff)
    1.54 +  then have "sup (Cset.set xs) A = fold Cset.insert xs A"
    1.55 +    by (simp add: union_set *)
    1.56 +  moreover have "\<And>x y :: 'a. Cset.insert y \<circ> Cset.insert x = Cset.insert x \<circ> Cset.insert y"
    1.57 +    by (auto simp add: *)
    1.58 +  ultimately show "sup (Cset.set xs) A = foldr Cset.insert xs A"
    1.59 +    by (simp add: foldr_fold)
    1.60 +  show "sup (Cset.coset xs) A = Cset.coset (List.filter (Not \<circ> member A) xs)"
    1.61 +    by (auto simp add: Cset.coset_def Cset.member_def)
    1.62 +qed
    1.63 +
    1.64  lemma subtract_remove:
    1.65    "A - Cset.set xs = foldr Cset.remove xs A"
    1.66    "A - Cset.coset xs = Cset.set (List.filter (member A) xs)"
    1.67    by (simp_all only: diff_eq compl_set compl_coset inter_project)
    1.68  
    1.69 -lemma union_insert:
    1.70 -  "sup (Cset.set xs) A = foldr Cset.insert xs A"
    1.71 -  "sup (Cset.coset xs) A = Cset.coset (List.filter (Not \<circ> member A) xs)"
    1.72 -proof -
    1.73 -  have *: "\<And>x::'a. Cset.insert = (\<lambda>x. Set \<circ> Set.insert x \<circ> member)"
    1.74 -    by (simp add: fun_eq_iff member_cset_of)
    1.75 -  have "member \<circ> fold (\<lambda>x. Set \<circ> Set.insert x \<circ> member) xs =
    1.76 -    fold Set.insert xs \<circ> member"
    1.77 -    by (rule fold_commute) (simp add: fun_eq_iff mem_def)
    1.78 -  then have "fold Set.insert xs (member A) =
    1.79 -    member (fold (\<lambda>x. Set \<circ> Set.insert x \<circ> member) xs A)"
    1.80 -    by (simp add: fun_eq_iff)
    1.81 -  then have "sup (Cset.set xs) A = fold Cset.insert xs A"
    1.82 -    by (simp add: union_set * member_cset_of)
    1.83 -  moreover have "\<And>x y :: 'a. Cset.insert y \<circ> Cset.insert x = Cset.insert x \<circ> Cset.insert y"
    1.84 -    by (auto simp add: * member_cset_of)
    1.85 -  ultimately show "sup (Cset.set xs) A = foldr Cset.insert xs A"
    1.86 -    by (simp add: foldr_fold)
    1.87 -  show "sup (Cset.coset xs) A = Cset.coset (List.filter (Not \<circ> member A) xs)"
    1.88 -    by (auto simp add: Cset.coset_def member_cset_of mem_def)
    1.89 -qed
    1.90 -
    1.91  context complete_lattice
    1.92  begin
    1.93