# HG changeset patch
# User haftmann
# Date 1325168084 -3600
# Node ID 49a436ada6a24d0b603a7a6ba8a9ccc09008e371
# Parent  6a86cc88b02f0add6ea9b612ea327b079de5b9b2
added implementation of pred_of_set

diff -r 6a86cc88b02f -r 49a436ada6a2 src/HOL/More_Set.thy
--- a/src/HOL/More_Set.thy	Thu Dec 29 14:23:40 2011 +0100
+++ b/src/HOL/More_Set.thy	Thu Dec 29 15:14:44 2011 +0100
@@ -245,6 +245,29 @@
   "SUPR (set xs) f = foldr (sup \<circ> f) xs bot"
   by (simp add: SUP_def Sup_set_foldr image_set foldr_map del: set_map)
 
+(* 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)
+
 hide_const (open) coset