src/HOL/Library/List_Set.thy
changeset 32880 b8bee63c7202
parent 31851 c04f8c51d0ab
child 33939 fcb50b497763
equal deleted inserted replaced
32878:f8d995b5dd60 32880:b8bee63c7202
    63 
    63 
    64 lemma insert_set:
    64 lemma insert_set:
    65   "Set.insert x (set xs) = set (insert x xs)"
    65   "Set.insert x (set xs) = set (insert x xs)"
    66   by (auto simp add: insert_def)
    66   by (auto simp add: insert_def)
    67 
    67 
       
    68 lemma insert_set_compl:
       
    69   "Set.insert x (- set xs) = - set (List_Set.remove_all x xs)"
       
    70   by (auto simp del: mem_def simp add: remove_all_def)
       
    71 
    68 lemma remove_set:
    72 lemma remove_set:
    69   "remove x (set xs) = set (remove_all x xs)"
    73   "remove x (set xs) = set (remove_all x xs)"
    70   by (auto simp add: remove_def remove_all_def)
    74   by (auto simp add: remove_def remove_all_def)
       
    75 
       
    76 lemma remove_set_compl:
       
    77   "List_Set.remove x (- set xs) = - set (List_Set.insert x xs)"
       
    78   by (auto simp del: mem_def simp add: remove_def List_Set.insert_def)
    71 
    79 
    72 lemma image_set:
    80 lemma image_set:
    73   "image f (set xs) = set (map f xs)"
    81   "image f (set xs) = set (map f xs)"
    74   by simp
    82   by simp
    75 
    83 
    96   show ?thesis
   104   show ?thesis
    97     by (simp add: minus_fold_remove [of _ A] fold_set)
   105     by (simp add: minus_fold_remove [of _ A] fold_set)
    98 qed
   106 qed
    99 
   107 
   100 lemma Inter_set:
   108 lemma Inter_set:
   101   "Inter (set (A # As)) = foldl (op \<inter>) A As"
   109   "Inter (set As) = foldl (op \<inter>) UNIV As"
   102 proof -
   110 proof -
   103   have "finite (set (A # As))" by simp
   111   have "fold (op \<inter>) UNIV (set As) = foldl (\<lambda>y x. x \<inter> y) UNIV As"
   104   moreover have "fold (op \<inter>) UNIV (set (A # As)) = foldl (\<lambda>y x. x \<inter> y) UNIV (A # As)"
       
   105     by (rule fun_left_comm_idem.fold_set, unfold_locales, auto)
   112     by (rule fun_left_comm_idem.fold_set, unfold_locales, auto)
   106   ultimately have "Inter (set (A # As)) = foldl (op \<inter>) UNIV (A # As)"
   113   then show ?thesis
   107     by (simp only: Inter_fold_inter Int_commute)
   114     by (simp only: Inter_fold_inter finite_set Int_commute)
   108   then show ?thesis by simp
       
   109 qed
   115 qed
   110 
   116 
   111 lemma Union_set:
   117 lemma Union_set:
   112   "Union (set As) = foldl (op \<union>) {} As"
   118   "Union (set As) = foldl (op \<union>) {} As"
   113 proof -
   119 proof -
   116   then show ?thesis
   122   then show ?thesis
   117     by (simp only: Union_fold_union finite_set Un_commute)
   123     by (simp only: Union_fold_union finite_set Un_commute)
   118 qed
   124 qed
   119 
   125 
   120 lemma INTER_set:
   126 lemma INTER_set:
   121   "INTER (set (A # As)) f = foldl (\<lambda>B A. f A \<inter> B) (f A) As"
   127   "INTER (set As) f = foldl (\<lambda>B A. f A \<inter> B) UNIV As"
   122 proof -
   128 proof -
   123   have "finite (set (A # As))" by simp
   129   have "fold (\<lambda>A. op \<inter> (f A)) UNIV (set As) = foldl (\<lambda>B A. f A \<inter> B) UNIV As"
   124   moreover have "fold (\<lambda>A. op \<inter> (f A)) UNIV (set (A # As)) = foldl (\<lambda>B A. f A \<inter> B) UNIV (A # As)"
       
   125     by (rule fun_left_comm_idem.fold_set, unfold_locales, auto)
   130     by (rule fun_left_comm_idem.fold_set, unfold_locales, auto)
   126   ultimately have "INTER (set (A # As)) f = foldl (\<lambda>B A. f A \<inter> B) UNIV (A # As)"
   131   then show ?thesis
   127     by (simp only: INTER_fold_inter) 
   132     by (simp only: INTER_fold_inter finite_set)
   128   then show ?thesis by simp
       
   129 qed
   133 qed
   130 
   134 
   131 lemma UNION_set:
   135 lemma UNION_set:
   132   "UNION (set As) f = foldl (\<lambda>B A. f A \<union> B) {} As"
   136   "UNION (set As) f = foldl (\<lambda>B A. f A \<union> B) {} As"
   133 proof -
   137 proof -