# HG changeset patch
# User kuncar
# Date 1349794678 -7200
# Node ID 73ab6d4a9236fc44fb920a1562cd506ac0195223
# Parent  5073cb632b6c9a80df531c28a75742631f0485fe
rename Set.project to Set.filter - more appropriate name

diff -r 5073cb632b6c -r 73ab6d4a9236 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Tue Oct 09 15:31:45 2012 +0200
+++ b/src/HOL/Finite_Set.thy	Tue Oct 09 16:57:58 2012 +0200
@@ -865,10 +865,10 @@
 
 lemma project_filter:
   assumes "finite A"
-  shows "Set.project P A = filter P A"
+  shows "Set.filter P A = filter P A"
 using assms
 by (induct A) 
-  (auto simp add: filter_def project_def comp_fun_commute.fold_insert[OF comp_fun_commute_filter_fold])
+  (auto simp add: filter_def Set.filter_def comp_fun_commute.fold_insert[OF comp_fun_commute_filter_fold])
 
 lemma image_fold_insert:
   assumes "finite A"
diff -r 5073cb632b6c -r 73ab6d4a9236 src/HOL/Library/RBT_Set.thy
--- a/src/HOL/Library/RBT_Set.thy	Tue Oct 09 15:31:45 2012 +0200
+++ b/src/HOL/Library/RBT_Set.thy	Tue Oct 09 16:57:58 2012 +0200
@@ -49,7 +49,7 @@
   "UNIV = UNIV" ..
 
 lemma [code, code del]:
-  "Set.project = Set.project" ..
+  "Set.filter = Set.filter" ..
 
 lemma [code, code del]:
   "image = image" ..
@@ -602,8 +602,8 @@
   "A - Coset t = rbt_filter (\<lambda>k. k \<in> A) t"
 by (simp add: inter_Set[simplified Int_commute])
 
-lemma project_Set [code]:
-  "Set.project P (Set t) = (rbt_filter P t)"
+lemma filter_Set [code]:
+  "Set.filter P (Set t) = (rbt_filter P t)"
 by (auto simp add: project_filter finite_filter_rbt_filter)
 
 lemma image_Set [code]:
diff -r 5073cb632b6c -r 73ab6d4a9236 src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Oct 09 15:31:45 2012 +0200
+++ b/src/HOL/List.thy	Tue Oct 09 16:57:58 2012 +0200
@@ -5627,8 +5627,8 @@
   "Set.remove x (List.coset xs) = List.coset (List.insert x xs)"
   by (simp_all add: remove_def Compl_insert)
 
-lemma project_set [code]:
-  "Set.project P (set xs) = set (filter P xs)"
+lemma filter_set [code]:
+  "Set.filter P (set xs) = set (filter P xs)"
   by auto
 
 lemma image_set [code]:
diff -r 5073cb632b6c -r 73ab6d4a9236 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Tue Oct 09 15:31:45 2012 +0200
+++ b/src/HOL/Set.thy	Tue Oct 09 16:57:58 2012 +0200
@@ -1825,14 +1825,14 @@
   "x \<in> Set.remove y A \<longleftrightarrow> x \<in> A \<and> x \<noteq> y"
   by (simp add: remove_def)
 
-definition project :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
-  [code_abbrev]: "project P A = {a \<in> A. P a}"
-
-hide_const (open) project
-
-lemma member_project [simp]:
-  "x \<in> Set.project P A \<longleftrightarrow> x \<in> A \<and> P x"
-  by (simp add: project_def)
+definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
+  [code_abbrev]: "filter P A = {a \<in> A. P a}"
+
+hide_const (open) filter
+
+lemma member_filter [simp]:
+  "x \<in> Set.filter P A \<longleftrightarrow> x \<in> A \<and> P x"
+  by (simp add: filter_def)
 
 instantiation set :: (equal) equal
 begin
diff -r 5073cb632b6c -r 73ab6d4a9236 src/HOL/ex/Executable_Relation.thy
--- a/src/HOL/ex/Executable_Relation.thy	Tue Oct 09 15:31:45 2012 +0200
+++ b/src/HOL/ex/Executable_Relation.thy	Tue Oct 09 16:57:58 2012 +0200
@@ -46,7 +46,7 @@
 by transfer auto
 
 lemma [code]:
-   "relcomp (Rel X R) (Rel Y S) = Rel (X Int Y) (Set.project (%(x, y). y : Y) R Un (Set.project (%(x, y). x : X) S Un R O S))"
+   "relcomp (Rel X R) (Rel Y S) = Rel (X Int Y) (Set.filter (%(x, y). y : Y) R Un (Set.filter (%(x, y). x : X) S Un R O S))"
 by transfer (auto simp add: Id_on_eqI relcomp.simps)
 
 lemma [code]: