# HG changeset patch
# User haftmann
# Date 1325965463 -3600
# Node ID f58b7f9d39208ef124395e98924c9b6f24b455e5
# Parent  f27cf421500abc49b8b05ac1ad46cf3d6baa7463
massaging of code setup for sets

diff -r f27cf421500a -r f58b7f9d3920 src/HOL/List.thy
--- a/src/HOL/List.thy	Sat Jan 07 20:18:56 2012 +0100
+++ b/src/HOL/List.thy	Sat Jan 07 20:44:23 2012 +0100
@@ -2605,7 +2605,19 @@
   "concat xss = foldr append xss []"
   by (simp add: fold_append_concat_rev foldr_def)
 
-lemma union_set_foldr:
+lemma minus_set_foldr [code]:
+  "A - set xs = foldr Set.remove xs A"
+proof -
+  have "\<And>x y :: 'a. Set.remove y \<circ> Set.remove x = Set.remove x \<circ> Set.remove y"
+    by (auto simp add: remove_def)
+  then show ?thesis by (simp add: minus_set_fold foldr_fold)
+qed
+
+lemma subtract_coset_filter [code]:
+  "A - List.coset xs = set (List.filter (\<lambda>x. x \<in> A) xs)"
+  by auto
+
+lemma union_set_foldr [code]:
   "set xs \<union> A = foldr Set.insert xs A"
 proof -
   have "\<And>x y :: 'a. insert y \<circ> insert x = insert x \<circ> insert y"
@@ -2613,13 +2625,17 @@
   then show ?thesis by (simp add: union_set_fold foldr_fold)
 qed
 
-lemma minus_set_foldr:
-  "A - set xs = foldr Set.remove xs A"
-proof -
-  have "\<And>x y :: 'a. Set.remove y \<circ> Set.remove x = Set.remove x \<circ> Set.remove y"
-    by (auto simp add: remove_def)
-  then show ?thesis by (simp add: minus_set_fold foldr_fold)
-qed
+lemma union_coset_foldr [code]:
+  "List.coset xs \<union> A = List.coset (List.filter (\<lambda>x. x \<notin> A) xs)"
+  by auto
+
+lemma inter_set_filer [code]:
+  "A \<inter> set xs = set (List.filter (\<lambda>x. x \<in> A) xs)"
+  by auto
+
+lemma inter_coset_foldr [code]:
+  "A \<inter> List.coset xs = foldr Set.remove xs A"
+  by (simp add: Diff_eq [symmetric] minus_set_foldr)
 
 lemma (in lattice) Inf_fin_set_foldr [code]:
   "Inf_fin (set (x # xs)) = foldr inf xs x"
@@ -2645,6 +2661,9 @@
   "Sup (set xs) = foldr sup xs bot"
   by (simp add: Sup_set_fold ac_simps foldr_fold fun_eq_iff)
 
+declare Inf_set_foldr [where 'a = "'a set", code] Sup_set_foldr [where 'a = "'a set", code]
+declare Inf_set_foldr [where 'a = "'a Predicate.pred", code] Sup_set_foldr [where 'a = "'a Predicate.pred", code]
+
 lemma (in complete_lattice) INF_set_foldr [code]:
   "INFI (set xs) f = foldr (inf \<circ> f) xs top"
   by (simp only: INF_def Inf_set_foldr foldr_map set_map [symmetric])
@@ -2653,6 +2672,29 @@
   "SUPR (set xs) f = foldr (sup \<circ> f) xs bot"
   by (simp only: SUP_def Sup_set_foldr foldr_map set_map [symmetric])
 
+(* FIXME: better implement conversion by bisection *)
+
+lemma pred_of_set_fold_sup:
+  assumes "finite A"
+  shows "pred_of_set A = Finite_Set.fold sup bot (Predicate.single ` A)" (is "?lhs = ?rhs")
+proof (rule sym)
+  interpret comp_fun_idem "sup :: 'a Predicate.pred \<Rightarrow> 'a Predicate.pred \<Rightarrow> 'a Predicate.pred"
+    by (fact comp_fun_idem_sup)
+  from `finite A` show "?rhs = ?lhs" by (induct A) (auto intro!: pred_eqI)
+qed
+
+lemma pred_of_set_set_fold_sup:
+  "pred_of_set (set xs) = fold sup (map Predicate.single xs) bot"
+proof -
+  interpret comp_fun_idem "sup :: 'a Predicate.pred \<Rightarrow> 'a Predicate.pred \<Rightarrow> 'a Predicate.pred"
+    by (fact comp_fun_idem_sup)
+  show ?thesis by (simp add: pred_of_set_fold_sup fold_set_fold [symmetric])
+qed
+
+lemma pred_of_set_set_foldr_sup [code]:
+  "pred_of_set (set xs) = foldr sup (map Predicate.single xs) bot"
+  by (simp add: pred_of_set_set_fold_sup ac_simps foldr_fold fun_eq_iff)
+
 
 subsubsection {* @{text upt} *}
 
@@ -5538,15 +5580,23 @@
   "{} = set []"
   by simp
 
+lemma UNIV_coset [code]:
+  "UNIV = List.coset []"
+  by simp
+
+lemma compl_set [code]:
+  "- set xs = List.coset xs"
+  by simp
+
+lemma compl_coset [code]:
+  "- List.coset xs = set xs"
+  by simp
+
 lemma [code]:
   "x \<in> set xs \<longleftrightarrow> List.member xs x"
   "x \<in> List.coset xs \<longleftrightarrow> \<not> List.member xs x"
   by (simp_all add: member_def)
 
-lemma UNIV_coset [code]:
-  "UNIV = List.coset []"
-  by simp
-
 lemma insert_code [code]:
   "insert x (set xs) = set (List.insert x xs)"
   "insert x (List.coset xs) = List.coset (removeAll x xs)"
@@ -5557,6 +5607,14 @@
   "Set.remove x (List.coset xs) = List.coset (List.insert x xs)"
   by (simp_all add: remove_def Compl_insert)
 
+lemma project_set [code]:
+  "Set.project P (set xs) = set (filter P xs)"
+  by auto
+
+lemma image_set [code]:
+  "image f (set xs) = set (map f xs)"
+  by simp
+
 lemma Ball_set [code]:
   "Ball (set xs) P \<longleftrightarrow> list_all P xs"
   by (simp add: list_all_iff)
@@ -5573,6 +5631,15 @@
   then show ?thesis by simp
 qed
 
+lemma the_elem_set [code]:
+  "the_elem (set [x]) = x"
+  by simp
+
+lemma Pow_set [code]:
+  "Pow (set []) = {{}}"
+  "Pow (set (x # xs)) = (let A = Pow (set xs) in A \<union> insert x ` A)"
+  by (simp_all add: Pow_insert Let_def)
+
 
 text {* Operations on relations *}
 
diff -r f27cf421500a -r f58b7f9d3920 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Sat Jan 07 20:18:56 2012 +0100
+++ b/src/HOL/Set.thy	Sat Jan 07 20:44:23 2012 +0100
@@ -431,10 +431,6 @@
 lemma bex_triv_one_point2 [simp]: "(EX x:A. a = x) = (a:A)"
   by blast
 
-lemma member_exists [code]:
-  "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. a = x)"
-  by (rule sym) (fact bex_triv_one_point2)
-
 lemma bex_one_point1 [simp]: "(EX x:A. x = a & P x) = (a:A & P a)"
   by blast
 
@@ -1837,10 +1833,6 @@
   "x \<in> Set.project P A \<longleftrightarrow> x \<in> A \<and> P x"
   by (simp add: project_def)
 
-lemma inter_project [code]:
-  "A \<inter> B = Set.project (\<lambda>x. x \<in> A) B"
-  by (auto simp add: project_def)
-
 instantiation set :: (equal) equal
 begin