merged;

--- a/NEWS	Sat Mar 17 11:23:14 2012 +0100
+++ b/NEWS	Sat Mar 17 11:57:03 2012 +0100
@@ -118,6 +118,8 @@
   Domain_def ~> Domain_unfold
   Range_def ~> Domain_converse [symmetric]
 
+Generalized theorems INF_INT_eq, INF_INT_eq2, SUP_UN_eq, SUP_UN_eq2.
+
 INCOMPATIBILITY.
 
 * Consolidated various theorem names relating to Finite_Set.fold

--- a/src/HOL/Library/Zorn.thy	Sat Mar 17 11:23:14 2012 +0100
+++ b/src/HOL/Library/Zorn.thy	Sat Mar 17 11:57:03 2012 +0100
@@ -12,38 +12,36 @@
 begin
 
 (* Define globally? In Set.thy? *)
-definition chain_subset :: "'a set set \<Rightarrow> bool" ("chain\<^bsub>\<subseteq>\<^esub>") where
-"chain\<^bsub>\<subseteq>\<^esub> C \<equiv> \<forall>A\<in>C.\<forall>B\<in>C. A \<subseteq> B \<or> B \<subseteq> A"
+definition chain_subset :: "'a set set \<Rightarrow> bool" ("chain\<^bsub>\<subseteq>\<^esub>")
+where
+  "chain\<^bsub>\<subseteq>\<^esub> C \<equiv> \<forall>A\<in>C.\<forall>B\<in>C. A \<subseteq> B \<or> B \<subseteq> A"
 
 text{*
   The lemma and section numbers refer to an unpublished article
   \cite{Abrial-Laffitte}.
 *}
 
-definition
-  chain     ::  "'a set set => 'a set set set" where
-  "chain S  = {F. F \<subseteq> S & chain\<^bsub>\<subseteq>\<^esub> F}"
+definition chain :: "'a set set \<Rightarrow> 'a set set set"
+where
+  "chain S = {F. F \<subseteq> S \<and> chain\<^bsub>\<subseteq>\<^esub> F}"
 
-definition
-  super     ::  "['a set set,'a set set] => 'a set set set" where
-  "super S c = {d. d \<in> chain S & c \<subset> d}"
-
-definition
-  maxchain  ::  "'a set set => 'a set set set" where
-  "maxchain S = {c. c \<in> chain S & super S c = {}}"
+definition super :: "'a set set \<Rightarrow> 'a set set \<Rightarrow> 'a set set set"
+where
+  "super S c = {d. d \<in> chain S \<and> c \<subset> d}"
 
-definition
-  succ      ::  "['a set set,'a set set] => 'a set set" where
-  "succ S c =
-    (if c \<notin> chain S | c \<in> maxchain S
-    then c else SOME c'. c' \<in> super S c)"
+definition maxchain  ::  "'a set set \<Rightarrow> 'a set set set"
+where
+  "maxchain S = {c. c \<in> chain S \<and> super S c = {}}"
 
-inductive_set
-  TFin :: "'a set set => 'a set set set"
-  for S :: "'a set set"
-  where
-    succI:        "x \<in> TFin S ==> succ S x \<in> TFin S"
-  | Pow_UnionI:   "Y \<in> Pow(TFin S) ==> Union(Y) \<in> TFin S"
+definition succ :: "'a set set \<Rightarrow> 'a set set \<Rightarrow> 'a set set"
+where
+  "succ S c = (if c \<notin> chain S \<or> c \<in> maxchain S then c else SOME c'. c' \<in> super S c)"
+
+inductive_set TFin :: "'a set set \<Rightarrow> 'a set set set"
+for S :: "'a set set"
+where
+  succI:      "x \<in> TFin S \<Longrightarrow> succ S x \<in> TFin S"
+| Pow_UnionI: "Y \<in> Pow (TFin S) \<Longrightarrow> \<Union>Y \<in> TFin S"
 
 
 subsection{*Mathematical Preamble*}

--- a/src/HOL/Relation.thy	Sat Mar 17 11:23:14 2012 +0100
+++ b/src/HOL/Relation.thy	Sat Mar 17 11:57:03 2012 +0100
@@ -95,6 +95,18 @@
 lemma sup_Un_eq2 [pred_set_conv]: "(\<lambda>x y. (x, y) \<in> R) \<squnion> (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<union> S)"
   by (simp add: sup_fun_def)
 
+lemma INF_INT_eq [pred_set_conv]: "(\<Sqinter>i\<in>S. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Inter>i\<in>S. r i))"
+  by (simp add: fun_eq_iff)
+
+lemma INF_INT_eq2 [pred_set_conv]: "(\<Sqinter>i\<in>S. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Inter>i\<in>S. r i))"
+  by (simp add: fun_eq_iff)
+
+lemma SUP_UN_eq [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Union>i\<in>S. r i))"
+  by (simp add: fun_eq_iff)
+
+lemma SUP_UN_eq2 [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Union>i\<in>S. r i))"
+  by (simp add: fun_eq_iff)
+
 lemma Inf_INT_eq [pred_set_conv]: "\<Sqinter>S = (\<lambda>x. x \<in> INTER S Collect)"
   by (simp add: fun_eq_iff)
 
@@ -119,19 +131,6 @@
 lemma SUP_Sup_eq2 [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x y. (x, y) \<in> i)) = (\<lambda>x y. (x, y) \<in> \<Union>S)"
   by (simp add: fun_eq_iff)
 
-lemma INF_INT_eq [pred_set_conv]: "(\<Sqinter>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Inter>i. r i))"
-  by (simp add: fun_eq_iff)
-
-lemma INF_INT_eq2 [pred_set_conv]: "(\<Sqinter>i\<in>S. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Inter>i\<in>S. r i))"
-  by (simp add: fun_eq_iff)
-
-lemma SUP_UN_eq [pred_set_conv]: "(\<Squnion>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Union>i. r i))"
-  by (simp add: fun_eq_iff)
-
-lemma SUP_UN_eq2 [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Union>i\<in>S. r i))"
-  by (simp add: fun_eq_iff)
-
-
 
 subsection {* Properties of relations *}
 
@@ -277,13 +276,17 @@
   "\<forall>x\<in>S. sym (r x) \<Longrightarrow> sym (INTER S r)"
   by (fast intro: symI elim: symE)
 
-(* FIXME thm sym_INTER [to_pred] *)
+lemma symp_INF:
+  "\<forall>x\<in>S. symp (r x) \<Longrightarrow> symp (INFI S r)"
+  by (fact sym_INTER [to_pred])
 
 lemma sym_UNION:
   "\<forall>x\<in>S. sym (r x) \<Longrightarrow> sym (UNION S r)"
   by (fast intro: symI elim: symE)
 
-(* FIXME thm sym_UNION [to_pred] *)
+lemma symp_SUP:
+  "\<forall>x\<in>S. symp (r x) \<Longrightarrow> symp (SUPR S r)"
+  by (fact sym_UNION [to_pred])
 
 
 subsubsection {* Antisymmetry *}