incorporated various theorems from theory More_Set into corpus
authorhaftmann
Fri Jan 06 21:48:45 2012 +0100 (2012-01-06)
changeset 461466baea4fca6bd
parent 46145 0ec0af1c651d
child 46147 2c4d8de91c4c
incorporated various theorems from theory More_Set into corpus
src/HOL/Finite_Set.thy
src/HOL/Library/Cset.thy
src/HOL/More_Set.thy
src/HOL/Set.thy
     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.37        (simp_all add: INF_def inf_left_commute)
    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.46        (simp_all add: SUP_def sup_left_commute)
    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.23      by (simp add: fun_eq_iff)
    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.32      by (simp add: fun_eq_iff)
    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.113    by (simp_all add: member_def)
   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.161    by (simp_all add: Inf_set_foldr)
   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.167    by (simp_all add: Sup_set_foldr)
   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.177    by (simp add: finite_trancl_ntranl)
   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"
    4.27    by (simp add: project_def)
    4.28  
    4.29 +lemma inter_project [code]:
    4.30 +  "A \<inter> B = Set.project (\<lambda>x. x \<in> A) B"
    4.31 +  by (auto simp add: project_def)
    4.32 +
    4.33  instantiation set :: (equal) equal
    4.34  begin
    4.35