merged

--- a/src/HOL/Complete_Lattices.thy	Thu Dec 29 17:43:40 2011 +0100
+++ b/src/HOL/Complete_Lattices.thy	Thu Dec 29 17:43:54 2011 +0100
@@ -928,11 +928,15 @@
   "Set.bind A f = UNION A f"
   by (simp add: bind_def UNION_eq)
 
+lemma member_bind [simp]:
+  "x \<in> Set.bind P f \<longleftrightarrow> x \<in> UNION P f "
+  by (simp add: bind_UNION)
+
 lemma Union_image_eq [simp]:
   "\<Union>(B ` A) = (\<Union>x\<in>A. B x)"
   by (rule sym) (fact SUP_def)
 
-lemma UN_iff [simp]: "(b \<in> (\<Union>x\<in>A. B x)) = (\<exists>x\<in>A. b \<in> B x)"
+lemma UN_iff [simp]: "b \<in> (\<Union>x\<in>A. B x) \<longleftrightarrow> (\<exists>x\<in>A. b \<in> B x)"
   by (auto simp add: SUP_def image_def)
 
 lemma UN_I [intro]: "a \<in> A \<Longrightarrow> b \<in> B a \<Longrightarrow> b \<in> (\<Union>x\<in>A. B x)"

--- a/src/HOL/More_Set.thy	Thu Dec 29 17:43:40 2011 +0100
+++ b/src/HOL/More_Set.thy	Thu Dec 29 17:43:54 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
 
 

--- a/src/HOL/Predicate.thy	Thu Dec 29 17:43:40 2011 +0100
+++ b/src/HOL/Predicate.thy	Thu Dec 29 17:43:54 2011 +0100
@@ -411,6 +411,10 @@
   "(\<And>w. eval P w \<longleftrightarrow> eval Q w) \<Longrightarrow> P = Q"
   by (cases P, cases Q) (auto simp add: fun_eq_iff)
 
+lemma pred_eq_iff:
+  "P = Q \<Longrightarrow> (\<And>w. eval P w \<longleftrightarrow> eval Q w)"
+  by (simp add: pred_eqI)
+
 instantiation pred :: (type) complete_lattice
 begin
 
@@ -816,7 +820,7 @@
   by (auto simp add: fun_eq_iff elim: supE intro: supI1 supI2)
 qed
 
-lemma eval_code [code]: "eval (Seq f) = member (f ())"
+lemma eval_code [(* FIXME declare simp *)code]: "eval (Seq f) = member (f ())"
   unfolding Seq_def by (rule sym, rule eval_member)
 
 lemma single_code [code]:
@@ -1017,6 +1021,42 @@
 end;
 *}
 
+text {* Conversion from and to sets *}
+
+definition pred_of_set :: "'a set \<Rightarrow> 'a pred" where
+  "pred_of_set = Pred \<circ> (\<lambda>A x. x \<in> A)"
+
+lemma eval_pred_of_set [simp]:
+  "eval (pred_of_set A) x \<longleftrightarrow> x \<in>A"
+  by (simp add: pred_of_set_def)
+
+definition set_of_pred :: "'a pred \<Rightarrow> 'a set" where
+  "set_of_pred = Collect \<circ> eval"
+
+lemma member_set_of_pred [simp]:
+  "x \<in> set_of_pred P \<longleftrightarrow> Predicate.eval P x"
+  by (simp add: set_of_pred_def)
+
+definition set_of_seq :: "'a seq \<Rightarrow> 'a set" where
+  "set_of_seq = set_of_pred \<circ> pred_of_seq"
+
+lemma member_set_of_seq [simp]:
+  "x \<in> set_of_seq xq = Predicate.member xq x"
+  by (simp add: set_of_seq_def eval_member)
+
+lemma of_pred_code [code]:
+  "set_of_pred (Predicate.Seq f) = (case f () of
+     Predicate.Empty \<Rightarrow> {}
+   | Predicate.Insert x P \<Rightarrow> insert x (set_of_pred P)
+   | Predicate.Join P xq \<Rightarrow> set_of_pred P \<union> set_of_seq xq)"
+  by (auto split: seq.split simp add: eval_code)
+
+lemma of_seq_code [code]:
+  "set_of_seq Predicate.Empty = {}"
+  "set_of_seq (Predicate.Insert x P) = insert x (set_of_pred P)"
+  "set_of_seq (Predicate.Join P xq) = set_of_pred P \<union> set_of_seq xq"
+  by auto
+
 no_notation
   bot ("\<bottom>") and
   top ("\<top>") and

--- a/src/HOL/Set.thy	Thu Dec 29 17:43:40 2011 +0100
+++ b/src/HOL/Set.thy	Thu Dec 29 17:43:54 2011 +0100
@@ -1790,6 +1790,22 @@
 
 hide_const (open) bind
 
+lemma bind_bind:
+  fixes A :: "'a set"
+  shows "Set.bind (Set.bind A B) C = Set.bind A (\<lambda>x. Set.bind (B x) C)"
+  by (auto simp add: bind_def)
+
+lemma empty_bind [simp]:
+  "Set.bind {} B = {}"
+  by (simp add: bind_def)
+
+lemma nonempty_bind_const:
+  "A \<noteq> {} \<Longrightarrow> Set.bind A (\<lambda>_. B) = B"
+  by (auto simp add: bind_def)
+
+lemma bind_const: "Set.bind A (\<lambda>_. B) = (if A = {} then {} else B)"
+  by (auto simp add: bind_def)
+
 
 subsubsection {* Operations for execution *}