moved various set operations to theory Set (resp. Product_Type)
authorhaftmann
Mon Dec 26 18:32:43 2011 +0100 (2011-12-26)
changeset 45986c9e50153e5ae
parent 45985 2d399a776de2
child 45987 9ba44b49859b
moved various set operations to theory Set (resp. Product_Type)
src/HOL/Library/Cset.thy
src/HOL/Library/More_Set.thy
src/HOL/MicroJava/BV/BVExample.thy
src/HOL/Product_Type.thy
src/HOL/Quotient_Examples/List_Quotient_Cset.thy
src/HOL/Quotient_Examples/Quotient_Cset.thy
src/HOL/Set.thy
     1.1 --- a/src/HOL/Library/Cset.thy	Mon Dec 26 17:40:43 2011 +0100
     1.2 +++ b/src/HOL/Library/Cset.thy	Mon Dec 26 18:32:43 2011 +0100
     1.3 @@ -103,13 +103,13 @@
     1.4  hide_const (open) UNIV
     1.5  
     1.6  definition is_empty :: "'a Cset.set \<Rightarrow> bool" where
     1.7 -  [simp]: "is_empty A \<longleftrightarrow> More_Set.is_empty (set_of A)"
     1.8 +  [simp]: "is_empty A \<longleftrightarrow> Set.is_empty (set_of A)"
     1.9  
    1.10  definition insert :: "'a \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
    1.11    [simp]: "insert x A = Set (Set.insert x (set_of A))"
    1.12  
    1.13  definition remove :: "'a \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
    1.14 -  [simp]: "remove x A = Set (More_Set.remove x (set_of A))"
    1.15 +  [simp]: "remove x A = Set (Set.remove x (set_of A))"
    1.16  
    1.17  definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a Cset.set \<Rightarrow> 'b Cset.set" where
    1.18    [simp]: "map f A = Set (image f (set_of A))"
    1.19 @@ -118,7 +118,7 @@
    1.20    by (simp_all add: fun_eq_iff image_compose)
    1.21  
    1.22  definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
    1.23 -  [simp]: "filter P A = Set (More_Set.project P (set_of A))"
    1.24 +  [simp]: "filter P A = Set (Set.project P (set_of A))"
    1.25  
    1.26  definition forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
    1.27    [simp]: "forall P A \<longleftrightarrow> Ball (set_of A) P"
    1.28 @@ -182,17 +182,17 @@
    1.29  
    1.30  lemma is_empty_simp [simp]:
    1.31    "is_empty A \<longleftrightarrow> set_of A = {}"
    1.32 -  by (simp add: More_Set.is_empty_def)
    1.33 +  by (simp add: Set.is_empty_def)
    1.34  declare is_empty_def [simp del]
    1.35  
    1.36  lemma remove_simp [simp]:
    1.37    "remove x A = Set (set_of A - {x})"
    1.38 -  by (simp add: More_Set.remove_def)
    1.39 +  by (simp add: Set.remove_def)
    1.40  declare remove_def [simp del]
    1.41  
    1.42  lemma filter_simp [simp]:
    1.43    "filter P A = Set {x \<in> set_of A. P x}"
    1.44 -  by (simp add: More_Set.project_def)
    1.45 +  by (simp add: Set.project_def)
    1.46  declare filter_def [simp del]
    1.47  
    1.48  lemma set_of_set [simp]:
    1.49 @@ -297,18 +297,18 @@
    1.50  proof -
    1.51    show "inf A (Cset.set xs) = Cset.set (List.filter (member A) xs)"
    1.52      by (simp add: inter project_def Cset.set_def member_def)
    1.53 -  have *: "\<And>x::'a. Cset.remove = (\<lambda>x. Set \<circ> More_Set.remove x \<circ> set_of)"
    1.54 -    by (simp add: fun_eq_iff More_Set.remove_def)
    1.55 -  have "set_of \<circ> fold (\<lambda>x. Set \<circ> More_Set.remove x \<circ> set_of) xs =
    1.56 -    fold More_Set.remove xs \<circ> set_of"
    1.57 +  have *: "\<And>x::'a. Cset.remove = (\<lambda>x. Set \<circ> Set.remove x \<circ> set_of)"
    1.58 +    by (simp add: fun_eq_iff Set.remove_def)
    1.59 +  have "set_of \<circ> fold (\<lambda>x. Set \<circ> Set.remove x \<circ> set_of) xs =
    1.60 +    fold Set.remove xs \<circ> set_of"
    1.61      by (rule fold_commute) (simp add: fun_eq_iff)
    1.62 -  then have "fold More_Set.remove xs (set_of A) = 
    1.63 -    set_of (fold (\<lambda>x. Set \<circ> More_Set.remove x \<circ> set_of) xs A)"
    1.64 +  then have "fold Set.remove xs (set_of A) = 
    1.65 +    set_of (fold (\<lambda>x. Set \<circ> Set.remove x \<circ> set_of) xs A)"
    1.66      by (simp add: fun_eq_iff)
    1.67    then have "inf A (Cset.coset xs) = fold Cset.remove xs A"
    1.68      by (simp add: Diff_eq [symmetric] minus_set *)
    1.69    moreover have "\<And>x y :: 'a. Cset.remove y \<circ> Cset.remove x = Cset.remove x \<circ> Cset.remove y"
    1.70 -    by (auto simp add: More_Set.remove_def *)
    1.71 +    by (auto simp add: Set.remove_def *)
    1.72    ultimately show "inf A (Cset.coset xs) = foldr Cset.remove xs A"
    1.73      by (simp add: foldr_fold)
    1.74  qed
     2.1 --- a/src/HOL/Library/More_Set.thy	Mon Dec 26 17:40:43 2011 +0100
     2.2 +++ b/src/HOL/Library/More_Set.thy	Mon Dec 26 18:32:43 2011 +0100
     2.3 @@ -7,57 +7,31 @@
     2.4  imports Main More_List
     2.5  begin
     2.6  
     2.7 -subsection {* Various additional set functions *}
     2.8 -
     2.9 -definition is_empty :: "'a set \<Rightarrow> bool" where
    2.10 -  "is_empty A \<longleftrightarrow> A = {}"
    2.11 -
    2.12 -hide_const (open) is_empty
    2.13 -
    2.14 -definition remove :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set" where
    2.15 -  "remove x A = A - {x}"
    2.16 -
    2.17 -hide_const (open) remove
    2.18 -
    2.19  lemma comp_fun_idem_remove:
    2.20 -  "comp_fun_idem More_Set.remove"
    2.21 +  "comp_fun_idem Set.remove"
    2.22  proof -
    2.23 -  have rem: "More_Set.remove = (\<lambda>x A. A - {x})" by (simp add: fun_eq_iff remove_def)
    2.24 +  have rem: "Set.remove = (\<lambda>x A. A - {x})" by (simp add: fun_eq_iff remove_def)
    2.25    show ?thesis by (simp only: comp_fun_idem_remove rem)
    2.26  qed
    2.27  
    2.28  lemma minus_fold_remove:
    2.29    assumes "finite A"
    2.30 -  shows "B - A = Finite_Set.fold More_Set.remove B A"
    2.31 +  shows "B - A = Finite_Set.fold Set.remove B A"
    2.32  proof -
    2.33 -  have rem: "More_Set.remove = (\<lambda>x A. A - {x})" by (simp add: fun_eq_iff remove_def)
    2.34 +  have rem: "Set.remove = (\<lambda>x A. A - {x})" by (simp add: fun_eq_iff remove_def)
    2.35    show ?thesis by (simp only: rem assms minus_fold_remove)
    2.36  qed
    2.37  
    2.38 -definition project :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
    2.39 -  "project P A = {a \<in> A. P a}"
    2.40 -
    2.41 -hide_const (open) project
    2.42 -
    2.43  lemma bounded_Collect_code [code_unfold_post]:
    2.44 -  "{x \<in> A. P x} = More_Set.project P A"
    2.45 +  "{x \<in> A. P x} = Set.project P A"
    2.46    by (simp add: project_def)
    2.47  
    2.48 -definition product :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" where
    2.49 -  "product A B = Sigma A (\<lambda>_. B)"
    2.50 -
    2.51 -hide_const (open) product
    2.52 -
    2.53 -lemma [code_unfold_post]:
    2.54 -  "Sigma A (\<lambda>_. B) = More_Set.product A B"
    2.55 -  by (simp add: product_def)
    2.56 -
    2.57  
    2.58  subsection {* Basic set operations *}
    2.59  
    2.60  lemma is_empty_set:
    2.61 -  "More_Set.is_empty (set xs) \<longleftrightarrow> List.null xs"
    2.62 -  by (simp add: is_empty_def null_def)
    2.63 +  "Set.is_empty (set xs) \<longleftrightarrow> List.null xs"
    2.64 +  by (simp add: Set.is_empty_def null_def)
    2.65  
    2.66  lemma empty_set:
    2.67    "{} = set []"
    2.68 @@ -68,7 +42,7 @@
    2.69    by auto
    2.70  
    2.71  lemma remove_set_compl:
    2.72 -  "More_Set.remove x (- set xs) = - set (List.insert x xs)"
    2.73 +  "Set.remove x (- set xs) = - set (List.insert x xs)"
    2.74    by (auto simp add: remove_def List.insert_def)
    2.75  
    2.76  lemma image_set:
    2.77 @@ -76,7 +50,7 @@
    2.78    by simp
    2.79  
    2.80  lemma project_set:
    2.81 -  "More_Set.project P (set xs) = set (filter P xs)"
    2.82 +  "Set.project P (set xs) = set (filter P xs)"
    2.83    by (auto simp add: project_def)
    2.84  
    2.85  
    2.86 @@ -99,18 +73,18 @@
    2.87  qed
    2.88  
    2.89  lemma minus_set:
    2.90 -  "A - set xs = fold More_Set.remove xs A"
    2.91 +  "A - set xs = fold Set.remove xs A"
    2.92  proof -
    2.93 -  interpret comp_fun_idem More_Set.remove
    2.94 +  interpret comp_fun_idem Set.remove
    2.95      by (fact comp_fun_idem_remove)
    2.96    show ?thesis
    2.97      by (simp add: minus_fold_remove [of _ A] fold_set)
    2.98  qed
    2.99  
   2.100  lemma minus_set_foldr:
   2.101 -  "A - set xs = foldr More_Set.remove xs A"
   2.102 +  "A - set xs = foldr Set.remove xs A"
   2.103  proof -
   2.104 -  have "\<And>x y :: 'a. More_Set.remove y \<circ> More_Set.remove x = More_Set.remove x \<circ> More_Set.remove y"
   2.105 +  have "\<And>x y :: 'a. Set.remove y \<circ> Set.remove x = Set.remove x \<circ> Set.remove y"
   2.106      by (auto simp add: remove_def)
   2.107    then show ?thesis by (simp add: minus_set foldr_fold)
   2.108  qed
   2.109 @@ -135,15 +109,15 @@
   2.110    by (fact eq_iff)
   2.111  
   2.112  lemma inter:
   2.113 -  "A \<inter> B = More_Set.project (\<lambda>x. x \<in> A) B"
   2.114 +  "A \<inter> B = Set.project (\<lambda>x. x \<in> A) B"
   2.115    by (auto simp add: project_def)
   2.116  
   2.117  
   2.118  subsection {* Theorems on relations *}
   2.119  
   2.120  lemma product_code:
   2.121 -  "More_Set.product (set xs) (set ys) = set [(x, y). x \<leftarrow> xs, y \<leftarrow> ys]"
   2.122 -  by (auto simp add: product_def)
   2.123 +  "Product_Type.product (set xs) (set ys) = set [(x, y). x \<leftarrow> xs, y \<leftarrow> ys]"
   2.124 +  by (auto simp add: Product_Type.product_def)
   2.125  
   2.126  lemma Id_on_set:
   2.127    "Id_on (set xs) = set [(x, x). x \<leftarrow> xs]"
   2.128 @@ -177,8 +151,8 @@
   2.129    by (simp_all add: member_def)
   2.130  
   2.131  lemma [code_unfold]:
   2.132 -  "A = {} \<longleftrightarrow> More_Set.is_empty A"
   2.133 -  by (simp add: is_empty_def)
   2.134 +  "A = {} \<longleftrightarrow> Set.is_empty A"
   2.135 +  by (simp add: Set.is_empty_def)
   2.136  
   2.137  declare empty_set [code]
   2.138  
   2.139 @@ -194,8 +168,8 @@
   2.140    by simp_all
   2.141  
   2.142  lemma remove_code [code]:
   2.143 -  "More_Set.remove x (set xs) = set (removeAll x xs)"
   2.144 -  "More_Set.remove x (coset xs) = coset (List.insert x xs)"
   2.145 +  "Set.remove x (set xs) = set (removeAll x xs)"
   2.146 +  "Set.remove x (coset xs) = coset (List.insert x xs)"
   2.147    by (simp_all add: remove_def Compl_insert)
   2.148  
   2.149  declare image_set [code]
   2.150 @@ -221,17 +195,6 @@
   2.151  
   2.152  subsection {* Derived operations *}
   2.153  
   2.154 -instantiation set :: (equal) equal
   2.155 -begin
   2.156 -
   2.157 -definition
   2.158 -  "HOL.equal A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
   2.159 -
   2.160 -instance proof
   2.161 -qed (auto simp add: equal_set_def)
   2.162 -
   2.163 -end
   2.164 -
   2.165  declare subset_eq [code]
   2.166  
   2.167  declare subset [code]
   2.168 @@ -241,11 +204,11 @@
   2.169  
   2.170  lemma inter_code [code]:
   2.171    "A \<inter> set xs = set (List.filter (\<lambda>x. x \<in> A) xs)"
   2.172 -  "A \<inter> coset xs = foldr More_Set.remove xs A"
   2.173 +  "A \<inter> coset xs = foldr Set.remove xs A"
   2.174    by (simp add: inter project_def) (simp add: Diff_eq [symmetric] minus_set_foldr)
   2.175  
   2.176  lemma subtract_code [code]:
   2.177 -  "A - set xs = foldr More_Set.remove xs A"
   2.178 +  "A - set xs = foldr Set.remove xs A"
   2.179    "A - coset xs = set (List.filter (\<lambda>x. x \<in> A) xs)"
   2.180    by (auto simp add: minus_set_foldr)
   2.181  
     3.1 --- a/src/HOL/MicroJava/BV/BVExample.thy	Mon Dec 26 17:40:43 2011 +0100
     3.2 +++ b/src/HOL/MicroJava/BV/BVExample.thy	Mon Dec 26 18:32:43 2011 +0100
     3.3 @@ -451,11 +451,11 @@
     3.4  qed
     3.5  
     3.6  lemma [code]:
     3.7 -  "iter f step ss w = while (\<lambda>(ss, w). \<not> More_Set.is_empty w)
     3.8 +  "iter f step ss w = while (\<lambda>(ss, w). \<not> Set.is_empty w)
     3.9      (\<lambda>(ss, w).
    3.10          let p = some_elem w in propa f (step p (ss ! p)) ss (w - {p}))
    3.11      (ss, w)"
    3.12 -  unfolding iter_def More_Set.is_empty_def some_elem_def ..
    3.13 +  unfolding iter_def Set.is_empty_def some_elem_def ..
    3.14  
    3.15  lemma JVM_sup_unfold [code]:
    3.16   "JVMType.sup S m n = lift2 (Opt.sup
    3.17 @@ -469,14 +469,6 @@
    3.18  lemmas [code] = JType.sup_def [unfolded exec_lub_def] JVM_le_unfold
    3.19  lemmas [code] = lesub_def plussub_def
    3.20  
    3.21 -setup {*
    3.22 -  Code.add_signature_cmd ("More_Set.is_empty", "'a set \<Rightarrow> bool")
    3.23 -  #> Code.add_signature_cmd ("propa", "('s \<Rightarrow> 's \<Rightarrow> 's) \<Rightarrow> (nat \<times> 's) list \<Rightarrow> 's list \<Rightarrow> nat set \<Rightarrow> 's list * nat set") 
    3.24 -  #> Code.add_signature_cmd 
    3.25 -     ("iter", "('s \<Rightarrow> 's \<Rightarrow> 's) \<Rightarrow> (nat \<Rightarrow> 's \<Rightarrow> (nat \<times> 's) list) \<Rightarrow> 's list \<Rightarrow> nat set \<Rightarrow> 's list * nat set")
    3.26 -  #> Code.add_signature_cmd ("unstables", "('s \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> (nat \<Rightarrow> 's \<Rightarrow> (nat \<times> 's) list) \<Rightarrow> 's list \<Rightarrow> nat set") 
    3.27 -*}
    3.28 -
    3.29  lemmas [code] =
    3.30    JType.sup_def [unfolded exec_lub_def]
    3.31    wf_class_code
     4.1 --- a/src/HOL/Product_Type.thy	Mon Dec 26 17:40:43 2011 +0100
     4.2 +++ b/src/HOL/Product_Type.thy	Mon Dec 26 18:32:43 2011 +0100
     4.3 @@ -877,11 +877,11 @@
     4.4    Disjoint union of a family of sets -- Sigma.
     4.5  *}
     4.6  
     4.7 -definition Sigma :: "['a set, 'a => 'b set] => ('a \<times> 'b) set" where
     4.8 +definition Sigma :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> ('a \<times> 'b) set" where
     4.9    Sigma_def: "Sigma A B == UN x:A. UN y:B x. {Pair x y}"
    4.10  
    4.11  abbreviation
    4.12 -  Times :: "['a set, 'b set] => ('a * 'b) set"
    4.13 +  Times :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set"
    4.14      (infixr "<*>" 80) where
    4.15    "A <*> B == Sigma A (%_. B)"
    4.16  
    4.17 @@ -893,6 +893,15 @@
    4.18  
    4.19  hide_const (open) Times
    4.20  
    4.21 +definition product :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" where
    4.22 +  "product A B = Sigma A (\<lambda>_. B)"
    4.23 +
    4.24 +hide_const (open) product
    4.25 +
    4.26 +lemma [code_unfold_post]:
    4.27 +  "Sigma A (\<lambda>_. B) = Product_Type.product A B"
    4.28 +  by (simp add: product_def)
    4.29 +
    4.30  syntax
    4.31    "_Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"  ("(3SIGMA _:_./ _)" [0, 0, 10] 10)
    4.32  translations
     5.1 --- a/src/HOL/Quotient_Examples/List_Quotient_Cset.thy	Mon Dec 26 17:40:43 2011 +0100
     5.2 +++ b/src/HOL/Quotient_Examples/List_Quotient_Cset.thy	Mon Dec 26 18:32:43 2011 +0100
     5.3 @@ -75,7 +75,7 @@
     5.4    "Quotient_Cset.remove x (coset xs) = coset (List.insert x xs)"
     5.5  unfolding coset_def
     5.6  apply descending
     5.7 -apply (simp add: More_Set.remove_def)
     5.8 +apply (simp add: Set.remove_def)
     5.9  apply descending
    5.10  by (simp add: remove_set_compl)
    5.11  
     6.1 --- a/src/HOL/Quotient_Examples/Quotient_Cset.thy	Mon Dec 26 17:40:43 2011 +0100
     6.2 +++ b/src/HOL/Quotient_Examples/Quotient_Cset.thy	Mon Dec 26 18:32:43 2011 +0100
     6.3 @@ -24,11 +24,11 @@
     6.4  lemma [quot_respect]:
     6.5    "(op = ===> set_eq ===> op =) (op \<in>) (op \<in>)"
     6.6    "(op = ===> set_eq) Collect Collect"
     6.7 -  "(set_eq ===> op =) More_Set.is_empty More_Set.is_empty"
     6.8 +  "(set_eq ===> op =) Set.is_empty Set.is_empty"
     6.9    "(op = ===> set_eq ===> set_eq) Set.insert Set.insert"
    6.10 -  "(op = ===> set_eq ===> set_eq) More_Set.remove More_Set.remove"
    6.11 +  "(op = ===> set_eq ===> set_eq) Set.remove Set.remove"
    6.12    "(op = ===> set_eq ===> set_eq) image image"
    6.13 -  "(op = ===> set_eq ===> set_eq) More_Set.project More_Set.project"
    6.14 +  "(op = ===> set_eq ===> set_eq) Set.project Set.project"
    6.15    "(set_eq ===> op =) Ball Ball"
    6.16    "(set_eq ===> op =) Bex Bex"
    6.17    "(set_eq ===> op =) Finite_Set.card Finite_Set.card"
    6.18 @@ -51,15 +51,15 @@
    6.19  quotient_definition "Set :: ('a => bool) => 'a Quotient_Cset.set"
    6.20  is Collect
    6.21  quotient_definition is_empty where "is_empty :: 'a Quotient_Cset.set \<Rightarrow> bool"
    6.22 -is More_Set.is_empty
    6.23 +is Set.is_empty
    6.24  quotient_definition insert where "insert :: 'a \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set"
    6.25  is Set.insert
    6.26  quotient_definition remove where "remove :: 'a \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set"
    6.27 -is More_Set.remove
    6.28 +is Set.remove
    6.29  quotient_definition map where "map :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'b Quotient_Cset.set"
    6.30  is image
    6.31  quotient_definition filter where "filter :: ('a \<Rightarrow> bool) \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set"
    6.32 -is More_Set.project
    6.33 +is Set.project
    6.34  quotient_definition "forall :: 'a Quotient_Cset.set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
    6.35  is Ball
    6.36  quotient_definition "exists :: 'a Quotient_Cset.set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
     7.1 --- a/src/HOL/Set.thy	Mon Dec 26 17:40:43 2011 +0100
     7.2 +++ b/src/HOL/Set.thy	Mon Dec 26 18:32:43 2011 +0100
     7.3 @@ -1791,6 +1791,34 @@
     7.4  hide_const (open) bind
     7.5  
     7.6  
     7.7 +subsubsection {* Operations for execution *}
     7.8 +
     7.9 +definition is_empty :: "'a set \<Rightarrow> bool" where
    7.10 +  "is_empty A \<longleftrightarrow> A = {}"
    7.11 +
    7.12 +hide_const (open) is_empty
    7.13 +
    7.14 +definition remove :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set" where
    7.15 +  "remove x A = A - {x}"
    7.16 +
    7.17 +hide_const (open) remove
    7.18 +
    7.19 +definition project :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
    7.20 +  "project P A = {a \<in> A. P a}"
    7.21 +
    7.22 +hide_const (open) project
    7.23 +
    7.24 +instantiation set :: (equal) equal
    7.25 +begin
    7.26 +
    7.27 +definition
    7.28 +  "HOL.equal A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
    7.29 +
    7.30 +instance proof
    7.31 +qed (auto simp add: equal_set_def)
    7.32 +
    7.33 +end
    7.34 +
    7.35  text {* Misc *}
    7.36  
    7.37  hide_const (open) member not_member