src/HOL/Library/List_Set.thy
changeset 31846 89c37daebfdd
parent 31807 039893a9a77d
child 31851 c04f8c51d0ab
equal deleted inserted replaced
31824:28f5ed40ecab 31846:89c37daebfdd
    68 lemma remove_set:
    68 lemma remove_set:
    69   "remove x (set xs) = set (remove_all x xs)"
    69   "remove x (set xs) = set (remove_all x xs)"
    70   by (auto simp add: remove_def remove_all_def)
    70   by (auto simp add: remove_def remove_all_def)
    71 
    71 
    72 lemma image_set:
    72 lemma image_set:
    73   "image f (set xs) = set (remdups (map f xs))"
    73   "image f (set xs) = set (map f xs)"
    74   by simp
    74   by simp
    75 
    75 
    76 lemma project_set:
    76 lemma project_set:
    77   "project P (set xs) = set (filter P xs)"
    77   "project P (set xs) = set (filter P xs)"
    78   by (auto simp add: project_def)
    78   by (auto simp add: project_def)