rename Set.project to Set.filter - more appropriate name
authorkuncar
Tue Oct 09 16:57:58 2012 +0200 (2012-10-09)
changeset 4975773ab6d4a9236
parent 49746 5073cb632b6c
child 49758 718f10c8bbfc
rename Set.project to Set.filter - more appropriate name
src/HOL/Finite_Set.thy
src/HOL/Library/RBT_Set.thy
src/HOL/List.thy
src/HOL/Set.thy
src/HOL/ex/Executable_Relation.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Tue Oct 09 15:31:45 2012 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Tue Oct 09 16:57:58 2012 +0200
     1.3 @@ -865,10 +865,10 @@
     1.4  
     1.5  lemma project_filter:
     1.6    assumes "finite A"
     1.7 -  shows "Set.project P A = filter P A"
     1.8 +  shows "Set.filter P A = filter P A"
     1.9  using assms
    1.10  by (induct A) 
    1.11 -  (auto simp add: filter_def project_def comp_fun_commute.fold_insert[OF comp_fun_commute_filter_fold])
    1.12 +  (auto simp add: filter_def Set.filter_def comp_fun_commute.fold_insert[OF comp_fun_commute_filter_fold])
    1.13  
    1.14  lemma image_fold_insert:
    1.15    assumes "finite A"
     2.1 --- a/src/HOL/Library/RBT_Set.thy	Tue Oct 09 15:31:45 2012 +0200
     2.2 +++ b/src/HOL/Library/RBT_Set.thy	Tue Oct 09 16:57:58 2012 +0200
     2.3 @@ -49,7 +49,7 @@
     2.4    "UNIV = UNIV" ..
     2.5  
     2.6  lemma [code, code del]:
     2.7 -  "Set.project = Set.project" ..
     2.8 +  "Set.filter = Set.filter" ..
     2.9  
    2.10  lemma [code, code del]:
    2.11    "image = image" ..
    2.12 @@ -602,8 +602,8 @@
    2.13    "A - Coset t = rbt_filter (\<lambda>k. k \<in> A) t"
    2.14  by (simp add: inter_Set[simplified Int_commute])
    2.15  
    2.16 -lemma project_Set [code]:
    2.17 -  "Set.project P (Set t) = (rbt_filter P t)"
    2.18 +lemma filter_Set [code]:
    2.19 +  "Set.filter P (Set t) = (rbt_filter P t)"
    2.20  by (auto simp add: project_filter finite_filter_rbt_filter)
    2.21  
    2.22  lemma image_Set [code]:
     3.1 --- a/src/HOL/List.thy	Tue Oct 09 15:31:45 2012 +0200
     3.2 +++ b/src/HOL/List.thy	Tue Oct 09 16:57:58 2012 +0200
     3.3 @@ -5627,8 +5627,8 @@
     3.4    "Set.remove x (List.coset xs) = List.coset (List.insert x xs)"
     3.5    by (simp_all add: remove_def Compl_insert)
     3.6  
     3.7 -lemma project_set [code]:
     3.8 -  "Set.project P (set xs) = set (filter P xs)"
     3.9 +lemma filter_set [code]:
    3.10 +  "Set.filter P (set xs) = set (filter P xs)"
    3.11    by auto
    3.12  
    3.13  lemma image_set [code]:
     4.1 --- a/src/HOL/Set.thy	Tue Oct 09 15:31:45 2012 +0200
     4.2 +++ b/src/HOL/Set.thy	Tue Oct 09 16:57:58 2012 +0200
     4.3 @@ -1825,14 +1825,14 @@
     4.4    "x \<in> Set.remove y A \<longleftrightarrow> x \<in> A \<and> x \<noteq> y"
     4.5    by (simp add: remove_def)
     4.6  
     4.7 -definition project :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
     4.8 -  [code_abbrev]: "project P A = {a \<in> A. P a}"
     4.9 -
    4.10 -hide_const (open) project
    4.11 -
    4.12 -lemma member_project [simp]:
    4.13 -  "x \<in> Set.project P A \<longleftrightarrow> x \<in> A \<and> P x"
    4.14 -  by (simp add: project_def)
    4.15 +definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
    4.16 +  [code_abbrev]: "filter P A = {a \<in> A. P a}"
    4.17 +
    4.18 +hide_const (open) filter
    4.19 +
    4.20 +lemma member_filter [simp]:
    4.21 +  "x \<in> Set.filter P A \<longleftrightarrow> x \<in> A \<and> P x"
    4.22 +  by (simp add: filter_def)
    4.23  
    4.24  instantiation set :: (equal) equal
    4.25  begin
     5.1 --- a/src/HOL/ex/Executable_Relation.thy	Tue Oct 09 15:31:45 2012 +0200
     5.2 +++ b/src/HOL/ex/Executable_Relation.thy	Tue Oct 09 16:57:58 2012 +0200
     5.3 @@ -46,7 +46,7 @@
     5.4  by transfer auto
     5.5  
     5.6  lemma [code]:
     5.7 -   "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))"
     5.8 +   "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))"
     5.9  by transfer (auto simp add: Id_on_eqI relcomp.simps)
    5.10  
    5.11  lemma [code]: