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
```