# 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 "\x y :: 'a. Set.remove y \ Set.remove x = Set.remove x \ 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 (\x. x \ A) xs)"
+ by auto
+
+lemma union_set_foldr [code]:
"set xs \ A = foldr Set.insert xs A"
proof 
have "\x y :: 'a. insert y \ insert x = insert x \ 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 "\x y :: 'a. Set.remove y \ Set.remove x = Set.remove x \ 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 \ A = List.coset (List.filter (\x. x \ A) xs)"
+ by auto
+
+lemma inter_set_filer [code]:
+ "A \ set xs = set (List.filter (\x. x \ A) xs)"
+ by auto
+
+lemma inter_coset_foldr [code]:
+ "A \ 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 \ 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 \ 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 \ 'a Predicate.pred \ '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 \ 'a Predicate.pred \ '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 \ set xs \ List.member xs x"
"x \ List.coset xs \ \ 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 \ 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 \ 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 \ A \ (\x\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 \ Set.project P A \ x \ A \ P x"
by (simp add: project_def)
lemma inter_project [code]:
 "A \ B = Set.project (\x. x \ A) B"
 by (auto simp add: project_def)

instantiation set :: (equal) equal
begin