src/HOL/Set.thy
changeset 45986 c9e50153e5ae
parent 45959 184d36538e51
child 46026 83caa4f4bd56
     1.1 --- a/src/HOL/Set.thy	Mon Dec 26 17:40:43 2011 +0100
     1.2 +++ b/src/HOL/Set.thy	Mon Dec 26 18:32:43 2011 +0100
     1.3 @@ -1791,6 +1791,34 @@
     1.4  hide_const (open) bind
     1.5  
     1.6  
     1.7 +subsubsection {* Operations for execution *}
     1.8 +
     1.9 +definition is_empty :: "'a set \<Rightarrow> bool" where
    1.10 +  "is_empty A \<longleftrightarrow> A = {}"
    1.11 +
    1.12 +hide_const (open) is_empty
    1.13 +
    1.14 +definition remove :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set" where
    1.15 +  "remove x A = A - {x}"
    1.16 +
    1.17 +hide_const (open) remove
    1.18 +
    1.19 +definition project :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
    1.20 +  "project P A = {a \<in> A. P a}"
    1.21 +
    1.22 +hide_const (open) project
    1.23 +
    1.24 +instantiation set :: (equal) equal
    1.25 +begin
    1.26 +
    1.27 +definition
    1.28 +  "HOL.equal A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
    1.29 +
    1.30 +instance proof
    1.31 +qed (auto simp add: equal_set_def)
    1.32 +
    1.33 +end
    1.34 +
    1.35  text {* Misc *}
    1.36  
    1.37  hide_const (open) member not_member