author haftmann Fri Jan 06 21:48:45 2012 +0100 (2012-01-06) changeset 46146 6baea4fca6bd parent 46145 0ec0af1c651d child 46147 2c4d8de91c4c
incorporated various theorems from theory More_Set into corpus
 src/HOL/Finite_Set.thy file | annotate | diff | revisions src/HOL/Library/Cset.thy file | annotate | diff | revisions src/HOL/More_Set.thy file | annotate | diff | revisions src/HOL/Set.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Finite_Set.thy	Fri Jan 06 21:48:45 2012 +0100
1.2 +++ b/src/HOL/Finite_Set.thy	Fri Jan 06 21:48:45 2012 +0100
1.3 @@ -718,7 +718,7 @@
1.4  qed auto
1.5
1.6  lemma comp_fun_idem_remove:
1.7 -  "comp_fun_idem (\<lambda>x A. A - {x})"
1.8 +  "comp_fun_idem Set.remove"
1.9  proof
1.10  qed auto
1.11
1.12 @@ -742,10 +742,11 @@
1.13
1.14  lemma minus_fold_remove:
1.15    assumes "finite A"
1.16 -  shows "B - A = fold (\<lambda>x A. A - {x}) B A"
1.17 +  shows "B - A = fold Set.remove B A"
1.18  proof -
1.19 -  interpret comp_fun_idem "\<lambda>x A. A - {x}" by (fact comp_fun_idem_remove)
1.20 -  from `finite A` show ?thesis by (induct A arbitrary: B) auto
1.21 +  interpret comp_fun_idem Set.remove by (fact comp_fun_idem_remove)
1.22 +  from `finite A` have "fold Set.remove B A = B - A" by (induct A arbitrary: B) auto
1.23 +  then show ?thesis ..
1.24  qed
1.25
1.26  context complete_lattice
1.27 @@ -779,7 +780,7 @@
1.28    shows "Sup A = fold sup bot A"
1.29    using assms sup_Sup_fold_sup [of A bot] by (simp add: sup_absorb2)
1.30
1.31 -lemma inf_INFI_fold_inf:
1.32 +lemma inf_INF_fold_inf:
1.33    assumes "finite A"
1.34    shows "inf B (INFI A f) = fold (inf \<circ> f) B A" (is "?inf = ?fold")
1.35  proof (rule sym)
1.36 @@ -790,7 +791,7 @@
1.38  qed
1.39
1.40 -lemma sup_SUPR_fold_sup:
1.41 +lemma sup_SUP_fold_sup:
1.42    assumes "finite A"
1.43    shows "sup B (SUPR A f) = fold (sup \<circ> f) B A" (is "?sup = ?fold")
1.44  proof (rule sym)
1.45 @@ -801,15 +802,15 @@
1.47  qed
1.48
1.49 -lemma INFI_fold_inf:
1.50 +lemma INF_fold_inf:
1.51    assumes "finite A"
1.52    shows "INFI A f = fold (inf \<circ> f) top A"
1.53 -  using assms inf_INFI_fold_inf [of A top] by simp
1.54 +  using assms inf_INF_fold_inf [of A top] by simp
1.55
1.56 -lemma SUPR_fold_sup:
1.57 +lemma SUP_fold_sup:
1.58    assumes "finite A"
1.59    shows "SUPR A f = fold (sup \<circ> f) bot A"
1.60 -  using assms sup_SUPR_fold_sup [of A bot] by simp
1.61 +  using assms sup_SUP_fold_sup [of A bot] by simp
1.62
1.63  end
1.64
1.65 @@ -2066,10 +2067,10 @@
1.66    assumes fin: "finite (UNIV :: ('a \<Rightarrow> 'b) set)"
1.67    shows "finite (UNIV :: 'b set)"
1.68  proof -
1.69 -  from fin have "finite (range (\<lambda>f :: 'a \<Rightarrow> 'b. f arbitrary))"
1.70 -    by(rule finite_imageI)
1.71 -  moreover have "UNIV = range (\<lambda>f :: 'a \<Rightarrow> 'b. f arbitrary)"
1.72 -    by(rule UNIV_eq_I) auto
1.73 +  from fin have "\<And>arbitrary. finite (range (\<lambda>f :: 'a \<Rightarrow> 'b. f arbitrary))"
1.74 +    by (rule finite_imageI)
1.75 +  moreover have "\<And>arbitrary. UNIV = range (\<lambda>f :: 'a \<Rightarrow> 'b. f arbitrary)"
1.76 +    by (rule UNIV_eq_I) auto
1.77    ultimately show "finite (UNIV :: 'b set)" by simp
1.78  qed
1.79
```
```     2.1 --- a/src/HOL/Library/Cset.thy	Fri Jan 06 21:48:45 2012 +0100
2.2 +++ b/src/HOL/Library/Cset.thy	Fri Jan 06 21:48:45 2012 +0100
2.3 @@ -276,7 +276,7 @@
2.4    fix xs :: "'a list"
2.5    show "member (Cset.set xs) = member (fold insert xs Cset.empty)"
2.6      by (simp add: fold_commute_apply [symmetric, where ?h = Set and ?g = Set.insert]
2.7 -      fun_eq_iff Cset.set_def union_set [symmetric])
2.8 +      fun_eq_iff Cset.set_def union_set_fold [symmetric])
2.9  qed
2.10
2.11  lemma single_code [code]:
2.12 @@ -296,7 +296,7 @@
2.13    "inf A (Cset.coset xs) = foldr Cset.remove xs A"
2.14  proof -
2.15    show "inf A (Cset.set xs) = Cset.set (List.filter (member A) xs)"
2.16 -    by (simp add: inter project_def Cset.set_def member_def)
2.17 +    by (simp add: project_def Cset.set_def member_def) auto
2.18    have *: "\<And>x::'a. Cset.remove = (\<lambda>x. Set \<circ> Set.remove x \<circ> set_of)"
2.19      by (simp add: fun_eq_iff Set.remove_def)
2.20    have "set_of \<circ> fold (\<lambda>x. Set \<circ> Set.remove x \<circ> set_of) xs =
2.21 @@ -306,7 +306,7 @@
2.22      set_of (fold (\<lambda>x. Set \<circ> Set.remove x \<circ> set_of) xs A)"
2.24    then have "inf A (Cset.coset xs) = fold Cset.remove xs A"
2.25 -    by (simp add: Diff_eq [symmetric] minus_set *)
2.26 +    by (simp add: Diff_eq [symmetric] minus_set_fold *)
2.27    moreover have "\<And>x y :: 'a. Cset.remove y \<circ> Cset.remove x = Cset.remove x \<circ> Cset.remove y"
2.28      by (auto simp add: Set.remove_def *)
2.29    ultimately show "inf A (Cset.coset xs) = foldr Cset.remove xs A"
2.30 @@ -326,7 +326,7 @@
2.31      set_of (fold (\<lambda>x. Set \<circ> Set.insert x \<circ> set_of) xs A)"
2.33    then have "sup (Cset.set xs) A = fold Cset.insert xs A"
2.34 -    by (simp add: union_set *)
2.35 +    by (simp add: union_set_fold *)
2.36    moreover have "\<And>x y :: 'a. Cset.insert y \<circ> Cset.insert x = Cset.insert x \<circ> Cset.insert y"
2.37      by (auto simp add: *)
2.38    ultimately show "sup (Cset.set xs) A = foldr Cset.insert xs A"
```
```     3.1 --- a/src/HOL/More_Set.thy	Fri Jan 06 21:48:45 2012 +0100
3.2 +++ b/src/HOL/More_Set.thy	Fri Jan 06 21:48:45 2012 +0100
3.3 @@ -7,26 +7,6 @@
3.4  imports List
3.5  begin
3.6
3.7 -lemma comp_fun_idem_remove:
3.8 -  "comp_fun_idem Set.remove"
3.9 -proof -
3.10 -  have rem: "Set.remove = (\<lambda>x A. A - {x})" by (simp add: fun_eq_iff remove_def)
3.11 -  show ?thesis by (simp only: comp_fun_idem_remove rem)
3.12 -qed
3.13 -
3.14 -lemma minus_fold_remove:
3.15 -  assumes "finite A"
3.16 -  shows "B - A = Finite_Set.fold Set.remove B A"
3.17 -proof -
3.18 -  have rem: "Set.remove = (\<lambda>x A. A - {x})" by (simp add: fun_eq_iff remove_def)
3.19 -  show ?thesis by (simp only: rem assms minus_fold_remove)
3.20 -qed
3.21 -
3.22 -lemma bounded_Collect_code: (* FIXME delete candidate *)
3.23 -  "{x \<in> A. P x} = Set.project P A"
3.24 -  by (simp add: project_def)
3.25 -
3.26 -
3.27  subsection {* Basic set operations *}
3.28
3.29  lemma is_empty_set [code]:
3.30 @@ -37,26 +17,10 @@
3.31    "{} = set []"
3.32    by simp
3.33
3.34 -lemma insert_set_compl:
3.35 -  "insert x (- set xs) = - set (removeAll x xs)"
3.36 -  by auto
3.37 -
3.38 -lemma remove_set_compl:
3.39 -  "Set.remove x (- set xs) = - set (List.insert x xs)"
3.40 -  by (auto simp add: remove_def List.insert_def)
3.41 -
3.42 -lemma image_set:
3.43 -  "image f (set xs) = set (map f xs)"
3.44 -  by simp
3.45 -
3.46 -lemma project_set:
3.47 -  "Set.project P (set xs) = set (filter P xs)"
3.48 -  by (auto simp add: project_def)
3.49 -
3.50
3.51  subsection {* Functorial set operations *}
3.52
3.53 -lemma union_set:
3.54 +lemma union_set_fold:
3.55    "set xs \<union> A = fold Set.insert xs A"
3.56  proof -
3.57    interpret comp_fun_idem Set.insert
3.58 @@ -69,10 +33,10 @@
3.59  proof -
3.60    have "\<And>x y :: 'a. insert y \<circ> insert x = insert x \<circ> insert y"
3.61      by auto
3.62 -  then show ?thesis by (simp add: union_set foldr_fold)
3.63 +  then show ?thesis by (simp add: union_set_fold foldr_fold)
3.64  qed
3.65
3.66 -lemma minus_set:
3.67 +lemma minus_set_fold:
3.68    "A - set xs = fold Set.remove xs A"
3.69  proof -
3.70    interpret comp_fun_idem Set.remove
3.71 @@ -86,56 +50,29 @@
3.72  proof -
3.73    have "\<And>x y :: 'a. Set.remove y \<circ> Set.remove x = Set.remove x \<circ> Set.remove y"
3.74      by (auto simp add: remove_def)
3.75 -  then show ?thesis by (simp add: minus_set foldr_fold)
3.76 +  then show ?thesis by (simp add: minus_set_fold foldr_fold)
3.77  qed
3.78
3.79
3.80 -subsection {* Derived set operations *}
3.81 -
3.82 -lemma member [code]:
3.83 -  "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. a = x)"
3.84 -  by simp
3.85 -
3.86 -lemma subset [code]:
3.87 -  "A \<subset> B \<longleftrightarrow> A \<subseteq> B \<and> \<not> B \<subseteq> A"
3.88 -  by (fact less_le_not_le)
3.89 -
3.90 -lemma set_eq [code]:
3.91 -  "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
3.92 -  by (fact eq_iff)
3.93 -
3.94 -lemma inter [code]:
3.95 -  "A \<inter> B = Set.project (\<lambda>x. x \<in> A) B"
3.96 -  by (auto simp add: project_def)
3.97 -
3.98 -
3.99 -subsection {* Code generator setup *}
3.100 -
3.101 -definition coset :: "'a list \<Rightarrow> 'a set" where
3.102 -  [simp]: "coset xs = - set xs"
3.103 -
3.104 -code_datatype set coset
3.105 -
3.106 -
3.107  subsection {* Basic operations *}
3.108
3.109  lemma [code]:
3.110    "x \<in> set xs \<longleftrightarrow> List.member xs x"
3.111 -  "x \<in> coset xs \<longleftrightarrow> \<not> List.member xs x"
3.112 +  "x \<in> List.coset xs \<longleftrightarrow> \<not> List.member xs x"
3.114
3.115  lemma UNIV_coset [code]:
3.116 -  "UNIV = coset []"
3.117 +  "UNIV = List.coset []"
3.118    by simp
3.119
3.120  lemma insert_code [code]:
3.121    "insert x (set xs) = set (List.insert x xs)"
3.122 -  "insert x (coset xs) = coset (removeAll x xs)"
3.123 +  "insert x (List.coset xs) = List.coset (removeAll x xs)"
3.124    by simp_all
3.125
3.126  lemma remove_code [code]:
3.127    "Set.remove x (set xs) = set (removeAll x xs)"
3.128 -  "Set.remove x (coset xs) = coset (List.insert x xs)"
3.129 +  "Set.remove x (List.coset xs) = List.coset (List.insert x xs)"
3.130    by (simp_all add: remove_def Compl_insert)
3.131
3.132  lemma Ball_set [code]:
3.133 @@ -159,17 +96,17 @@
3.134
3.135  lemma inter_code [code]:
3.136    "A \<inter> set xs = set (List.filter (\<lambda>x. x \<in> A) xs)"
3.137 -  "A \<inter> coset xs = foldr Set.remove xs A"
3.138 -  by (simp add: inter project_def) (simp add: Diff_eq [symmetric] minus_set_foldr)
3.139 +  "A \<inter> List.coset xs = foldr Set.remove xs A"
3.140 +  by (simp add: inter_project project_def) (simp add: Diff_eq [symmetric] minus_set_foldr)
3.141
3.142  lemma subtract_code [code]:
3.143    "A - set xs = foldr Set.remove xs A"
3.144 -  "A - coset xs = set (List.filter (\<lambda>x. x \<in> A) xs)"
3.145 +  "A - List.coset xs = set (List.filter (\<lambda>x. x \<in> A) xs)"
3.146    by (auto simp add: minus_set_foldr)
3.147
3.148  lemma union_code [code]:
3.149    "set xs \<union> A = foldr insert xs A"
3.150 -  "coset xs \<union> A = coset (List.filter (\<lambda>x. x \<notin> A) xs)"
3.151 +  "List.coset xs \<union> A = List.coset (List.filter (\<lambda>x. x \<notin> A) xs)"
3.152    by (auto simp add: union_set_foldr)
3.153
3.154  definition Inf :: "'a::complete_lattice set \<Rightarrow> 'a" where
3.155 @@ -184,12 +121,12 @@
3.156
3.157  lemma Inf_code [code]:
3.158    "More_Set.Inf (set xs) = foldr inf xs top"
3.159 -  "More_Set.Inf (coset []) = bot"
3.160 +  "More_Set.Inf (List.coset []) = bot"
3.162
3.163  lemma Sup_sup [code]:
3.164    "More_Set.Sup (set xs) = foldr sup xs bot"
3.165 -  "More_Set.Sup (coset []) = top"
3.166 +  "More_Set.Sup (List.coset []) = top"
3.168
3.169  (* FIXME: better implement conversion by bisection *)
3.170 @@ -226,7 +163,8 @@
3.171    "Id_on (set xs) = set [(x, x). x \<leftarrow> xs]"
3.172    by (auto simp add: Id_on_def)
3.173
3.174 -lemma trancl_set_ntrancl [code]: "trancl (set xs) = ntrancl (card (set xs) - 1) (set xs)"
3.175 +lemma trancl_set_ntrancl [code]:
3.176 +  "trancl (set xs) = ntrancl (card (set xs) - 1) (set xs)"
3.178
3.179  lemma set_rel_comp [code]:
```
```     4.1 --- a/src/HOL/Set.thy	Fri Jan 06 21:48:45 2012 +0100
4.2 +++ b/src/HOL/Set.thy	Fri Jan 06 21:48:45 2012 +0100
4.3 @@ -431,6 +431,10 @@
4.4  lemma bex_triv_one_point2 [simp]: "(EX x:A. a = x) = (a:A)"
4.5    by blast
4.6
4.7 +lemma member_exists [code]:
4.8 +  "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. a = x)"
4.9 +  by (rule sym) (fact bex_triv_one_point2)
4.10 +
4.11  lemma bex_one_point1 [simp]: "(EX x:A. x = a & P x) = (a:A & P a)"
4.12    by blast
4.13
4.14 @@ -522,6 +526,10 @@
4.15  lemma set_mp: "A \<subseteq> B ==> x:A ==> x:B"
4.16    by (rule subsetD)
4.17
4.18 +lemma subset_not_subset_eq [code]:
4.19 +  "A \<subset> B \<longleftrightarrow> A \<subseteq> B \<and> \<not> B \<subseteq> A"
4.20 +  by (fact less_le_not_le)
4.21 +
4.22  lemma eq_mem_trans: "a=b ==> b \<in> A ==> a \<in> A"
4.23    by simp
4.24
4.25 @@ -1829,6 +1837,10 @@
4.26    "x \<in> Set.project P A \<longleftrightarrow> x \<in> A \<and> P x"