src/HOL/Library/List_Set.thy
changeset 32880 b8bee63c7202
parent 31851 c04f8c51d0ab
child 33939 fcb50b497763
     1.1 --- a/src/HOL/Library/List_Set.thy	Mon Oct 05 17:28:59 2009 +0100
     1.2 +++ b/src/HOL/Library/List_Set.thy	Tue Oct 06 15:59:12 2009 +0200
     1.3 @@ -65,10 +65,18 @@
     1.4    "Set.insert x (set xs) = set (insert x xs)"
     1.5    by (auto simp add: insert_def)
     1.6  
     1.7 +lemma insert_set_compl:
     1.8 +  "Set.insert x (- set xs) = - set (List_Set.remove_all x xs)"
     1.9 +  by (auto simp del: mem_def simp add: remove_all_def)
    1.10 +
    1.11  lemma remove_set:
    1.12    "remove x (set xs) = set (remove_all x xs)"
    1.13    by (auto simp add: remove_def remove_all_def)
    1.14  
    1.15 +lemma remove_set_compl:
    1.16 +  "List_Set.remove x (- set xs) = - set (List_Set.insert x xs)"
    1.17 +  by (auto simp del: mem_def simp add: remove_def List_Set.insert_def)
    1.18 +
    1.19  lemma image_set:
    1.20    "image f (set xs) = set (map f xs)"
    1.21    by simp
    1.22 @@ -98,14 +106,12 @@
    1.23  qed
    1.24  
    1.25  lemma Inter_set:
    1.26 -  "Inter (set (A # As)) = foldl (op \<inter>) A As"
    1.27 +  "Inter (set As) = foldl (op \<inter>) UNIV As"
    1.28  proof -
    1.29 -  have "finite (set (A # As))" by simp
    1.30 -  moreover have "fold (op \<inter>) UNIV (set (A # As)) = foldl (\<lambda>y x. x \<inter> y) UNIV (A # As)"
    1.31 +  have "fold (op \<inter>) UNIV (set As) = foldl (\<lambda>y x. x \<inter> y) UNIV As"
    1.32      by (rule fun_left_comm_idem.fold_set, unfold_locales, auto)
    1.33 -  ultimately have "Inter (set (A # As)) = foldl (op \<inter>) UNIV (A # As)"
    1.34 -    by (simp only: Inter_fold_inter Int_commute)
    1.35 -  then show ?thesis by simp
    1.36 +  then show ?thesis
    1.37 +    by (simp only: Inter_fold_inter finite_set Int_commute)
    1.38  qed
    1.39  
    1.40  lemma Union_set:
    1.41 @@ -118,14 +124,12 @@
    1.42  qed
    1.43  
    1.44  lemma INTER_set:
    1.45 -  "INTER (set (A # As)) f = foldl (\<lambda>B A. f A \<inter> B) (f A) As"
    1.46 +  "INTER (set As) f = foldl (\<lambda>B A. f A \<inter> B) UNIV As"
    1.47  proof -
    1.48 -  have "finite (set (A # As))" by simp
    1.49 -  moreover have "fold (\<lambda>A. op \<inter> (f A)) UNIV (set (A # As)) = foldl (\<lambda>B A. f A \<inter> B) UNIV (A # As)"
    1.50 +  have "fold (\<lambda>A. op \<inter> (f A)) UNIV (set As) = foldl (\<lambda>B A. f A \<inter> B) UNIV As"
    1.51      by (rule fun_left_comm_idem.fold_set, unfold_locales, auto)
    1.52 -  ultimately have "INTER (set (A # As)) f = foldl (\<lambda>B A. f A \<inter> B) UNIV (A # As)"
    1.53 -    by (simp only: INTER_fold_inter) 
    1.54 -  then show ?thesis by simp
    1.55 +  then show ?thesis
    1.56 +    by (simp only: INTER_fold_inter finite_set)
    1.57  qed
    1.58  
    1.59  lemma UNION_set: