src/HOL/Library/List_Set.thy
changeset 34977 27ceb64d41ea
parent 34007 aea892559fc5
child 37023 efc202e1677e
     1.1 --- a/src/HOL/Library/List_Set.thy	Sun Jan 31 14:51:31 2010 +0100
     1.2 +++ b/src/HOL/Library/List_Set.thy	Sun Jan 31 14:51:32 2010 +0100
     1.3 @@ -7,15 +7,6 @@
     1.4  imports Main
     1.5  begin
     1.6  
     1.7 -subsection {* Various additional list functions *}
     1.8 -
     1.9 -definition insert :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    1.10 -  "insert x xs = (if x \<in> set xs then xs else x # xs)"
    1.11 -
    1.12 -definition remove_all :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    1.13 -  "remove_all x xs = filter (Not o op = x) xs"
    1.14 -
    1.15 -
    1.16  subsection {* Various additional set functions *}
    1.17  
    1.18  definition is_empty :: "'a set \<Rightarrow> bool" where
    1.19 @@ -61,21 +52,13 @@
    1.20    "{} = set []"
    1.21    by simp
    1.22  
    1.23 -lemma insert_set:
    1.24 -  "Set.insert x (set xs) = set (insert x xs)"
    1.25 -  by (auto simp add: insert_def)
    1.26 -
    1.27  lemma insert_set_compl:
    1.28 -  "Set.insert x (- set xs) = - set (List_Set.remove_all x xs)"
    1.29 -  by (auto simp del: mem_def simp add: remove_all_def)
    1.30 -
    1.31 -lemma remove_set:
    1.32 -  "remove x (set xs) = set (remove_all x xs)"
    1.33 -  by (auto simp add: remove_def remove_all_def)
    1.34 +  "insert x (- set xs) = - set (removeAll x xs)"
    1.35 +  by auto
    1.36  
    1.37  lemma remove_set_compl:
    1.38 -  "List_Set.remove x (- set xs) = - set (List_Set.insert x xs)"
    1.39 -  by (auto simp del: mem_def simp add: remove_def List_Set.insert_def)
    1.40 +  "remove x (- set xs) = - set (List.insert x xs)"
    1.41 +  by (auto simp del: mem_def simp add: remove_def List.insert_def)
    1.42  
    1.43  lemma image_set:
    1.44    "image f (set xs) = set (map f xs)"
    1.45 @@ -128,7 +111,4 @@
    1.46    "A \<inter> B = project (\<lambda>x. x \<in> A) B"
    1.47    by (auto simp add: project_def)
    1.48  
    1.49 -
    1.50 -hide (open) const insert
    1.51 -
    1.52  end
    1.53 \ No newline at end of file