diff --git a/src/ZF/Nat.thy b/src/ZF/Nat.thy
--- a/src/ZF/Nat.thy
+++ b/src/ZF/Nat.thy
@@ -1,302 +1,297 @@
 (*  Title:      ZF/Nat.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
 *)
 
 section\<open>The Natural numbers As a Least Fixed Point\<close>
 
 theory Nat imports OrdQuant Bool begin
 
 definition
   nat :: i  where
     "nat == lfp(Inf, %X. {0} \<union> {succ(i). i \<in> X})"
 
 definition
   quasinat :: "i => o"  where
     "quasinat(n) == n=0 | (\<exists>m. n = succ(m))"
 
 definition
   (*Has an unconditional succ case, which is used in "recursor" below.*)
   nat_case :: "[i, i=>i, i]=>i"  where
     "nat_case(a,b,k) == THE y. k=0 & y=a | (\<exists>x. k=succ(x) & y=b(x))"
 
 definition
   nat_rec :: "[i, i, [i,i]=>i]=>i"  where
     "nat_rec(k,a,b) ==
           wfrec(Memrel(nat), k, %n f. nat_case(a, %m. b(m, f`m), n))"
 
   (*Internalized relations on the naturals*)
 
 definition
   Le :: i  where
     "Le == {<x,y>:nat*nat. x \<le> y}"
 
 definition
   Lt :: i  where
     "Lt == {<x, y>:nat*nat. x < y}"
 
 definition
   Ge :: i  where
     "Ge == {<x,y>:nat*nat. y \<le> x}"
 
 definition
   Gt :: i  where
     "Gt == {<x,y>:nat*nat. y < x}"
 
 definition
   greater_than :: "i=>i"  where
     "greater_than(n) == {i \<in> nat. n < i}"
 
 text\<open>No need for a less-than operator: a natural number is its list of
 predecessors!\<close>
 
 
 lemma nat_bnd_mono: "bnd_mono(Inf, %X. {0} \<union> {succ(i). i \<in> X})"
 apply (rule bnd_monoI)
 apply (cut_tac infinity, blast, blast)
 done
 
 (* @{term"nat = {0} \<union> {succ(x). x \<in> nat}"} *)
 lemmas nat_unfold = nat_bnd_mono [THEN nat_def [THEN def_lfp_unfold]]
 
 (** Type checking of 0 and successor **)
 
 lemma nat_0I [iff,TC]: "0 \<in> nat"
 apply (subst nat_unfold)
 apply (rule singletonI [THEN UnI1])
 done
 
 lemma nat_succI [intro!,TC]: "n \<in> nat ==> succ(n) \<in> nat"
 apply (subst nat_unfold)
 apply (erule RepFunI [THEN UnI2])
 done
 
 lemma nat_1I [iff,TC]: "1 \<in> nat"
 by (rule nat_0I [THEN nat_succI])
 
 lemma nat_2I [iff,TC]: "2 \<in> nat"
 by (rule nat_1I [THEN nat_succI])
 
 lemma bool_subset_nat: "bool \<subseteq> nat"
 by (blast elim!: boolE)
 
 lemmas bool_into_nat = bool_subset_nat [THEN subsetD]
 
 
 subsection\<open>Injectivity Properties and Induction\<close>
 
 (*Mathematical induction*)
 lemma nat_induct [case_names 0 succ, induct set: nat]:
     "[| n \<in> nat;  P(0);  !!x. [| x \<in> nat;  P(x) |] ==> P(succ(x)) |] ==> P(n)"
 by (erule def_induct [OF nat_def nat_bnd_mono], blast)
 
 lemma natE:
  assumes "n \<in> nat"
  obtains ("0") "n=0" | (succ) x where "x \<in> nat" "n=succ(x)"
 using assms
 by (rule nat_unfold [THEN equalityD1, THEN subsetD, THEN UnE]) auto
 
 lemma nat_into_Ord [simp]: "n \<in> nat ==> Ord(n)"
 by (erule nat_induct, auto)
 
 (* @{term"i \<in> nat ==> 0 \<le> i"}; same thing as @{term"0<succ(i)"}  *)
 lemmas nat_0_le = nat_into_Ord [THEN Ord_0_le]
 
 (* @{term"i \<in> nat ==> i \<le> i"}; same thing as @{term"i<succ(i)"}  *)
 lemmas nat_le_refl = nat_into_Ord [THEN le_refl]
 
 lemma Ord_nat [iff]: "Ord(nat)"
 apply (rule OrdI)
 apply (erule_tac [2] nat_into_Ord [THEN Ord_is_Transset])
 apply (unfold Transset_def)
 apply (rule ballI)
 apply (erule nat_induct, auto)
 done
 
 lemma Limit_nat [iff]: "Limit(nat)"
 apply (unfold Limit_def)
 apply (safe intro!: ltI Ord_nat)
 apply (erule ltD)
 done
 
 lemma naturals_not_limit: "a \<in> nat ==> ~ Limit(a)"
 by (induct a rule: nat_induct, auto)
 
 lemma succ_natD: "succ(i): nat ==> i \<in> nat"
 by (rule Ord_trans [OF succI1], auto)
 
 lemma nat_succ_iff [iff]: "succ(n): nat \<longleftrightarrow> n \<in> nat"
 by (blast dest!: succ_natD)
 
 lemma nat_le_Limit: "Limit(i) ==> nat \<le> i"
 apply (rule subset_imp_le)
 apply (simp_all add: Limit_is_Ord)
 apply (rule subsetI)
 apply (erule nat_induct)
  apply (erule Limit_has_0 [THEN ltD])
 apply (blast intro: Limit_has_succ [THEN ltD] ltI Limit_is_Ord)
 done
 
 (* [| succ(i): k;  k \<in> nat |] ==> i \<in> k *)
 lemmas succ_in_naturalD = Ord_trans [OF succI1 _ nat_into_Ord]
 
 lemma lt_nat_in_nat: "[| m<n;  n \<in> nat |] ==> m \<in> nat"
 apply (erule ltE)
 apply (erule Ord_trans, assumption, simp)
 done
 
 lemma le_in_nat: "[| m \<le> n; n \<in> nat |] ==> m \<in> nat"
 by (blast dest!: lt_nat_in_nat)
 
 
 subsection\<open>Variations on Mathematical Induction\<close>
 
 (*complete induction*)
 
 lemmas complete_induct = Ord_induct [OF _ Ord_nat, case_names less, consumes 1]
 
-lemmas complete_induct_rule =
-        complete_induct [rule_format, case_names less, consumes 1]
-
-
-lemma nat_induct_from_lemma [rule_format]:
-    "[| n \<in> nat;  m \<in> nat;
-        !!x. [| x \<in> nat;  m \<le> x;  P(x) |] ==> P(succ(x)) |]
-     ==> m \<le> n \<longrightarrow> P(m) \<longrightarrow> P(n)"
-apply (erule nat_induct)
-apply (simp_all add: distrib_simps le0_iff le_succ_iff)
-done
+lemma complete_induct_rule [case_names less, consumes 1]:
+  "i \<in> nat \<Longrightarrow> (\<And>x. x \<in> nat \<Longrightarrow> (\<And>y. y \<in> x \<Longrightarrow> P(y)) \<Longrightarrow> P(x)) \<Longrightarrow> P(i)"
+  using complete_induct [of i P] by simp
 
 (*Induction starting from m rather than 0*)
 lemma nat_induct_from:
-    "[| m \<le> n;  m \<in> nat;  n \<in> nat;
-        P(m);
-        !!x. [| x \<in> nat;  m \<le> x;  P(x) |] ==> P(succ(x)) |]
-     ==> P(n)"
-apply (blast intro: nat_induct_from_lemma)
-done
+  assumes "m \<le> n" "m \<in> nat" "n \<in> nat"
+    and "P(m)"
+    and "!!x. [| x \<in> nat;  m \<le> x;  P(x) |] ==> P(succ(x))"
+  shows "P(n)"
+proof -
+  from assms(3) have "m \<le> n \<longrightarrow> P(m) \<longrightarrow> P(n)"
+    by (rule nat_induct) (use assms(5) in \<open>simp_all add: distrib_simps le_succ_iff\<close>)
+  with assms(1,2,4) show ?thesis by blast
+qed
 
 (*Induction suitable for subtraction and less-than*)
 lemma diff_induct [case_names 0 0_succ succ_succ, consumes 2]:
     "[| m \<in> nat;  n \<in> nat;
         !!x. x \<in> nat ==> P(x,0);
         !!y. y \<in> nat ==> P(0,succ(y));
         !!x y. [| x \<in> nat;  y \<in> nat;  P(x,y) |] ==> P(succ(x),succ(y)) |]
      ==> P(m,n)"
 apply (erule_tac x = m in rev_bspec)
 apply (erule nat_induct, simp)
 apply (rule ballI)
 apply (rename_tac i j)
 apply (erule_tac n=j in nat_induct, auto)
 done
 
 
 (** Induction principle analogous to trancl_induct **)
 
 lemma succ_lt_induct_lemma [rule_format]:
      "m \<in> nat ==> P(m,succ(m)) \<longrightarrow> (\<forall>x\<in>nat. P(m,x) \<longrightarrow> P(m,succ(x))) \<longrightarrow>
                  (\<forall>n\<in>nat. m<n \<longrightarrow> P(m,n))"
 apply (erule nat_induct)
  apply (intro impI, rule nat_induct [THEN ballI])
    prefer 4 apply (intro impI, rule nat_induct [THEN ballI])
 apply (auto simp add: le_iff)
 done
 
 lemma succ_lt_induct:
     "[| m<n;  n \<in> nat;
         P(m,succ(m));
         !!x. [| x \<in> nat;  P(m,x) |] ==> P(m,succ(x)) |]
      ==> P(m,n)"
 by (blast intro: succ_lt_induct_lemma lt_nat_in_nat)
 
 subsection\<open>quasinat: to allow a case-split rule for \<^term>\<open>nat_case\<close>\<close>
 
 text\<open>True if the argument is zero or any successor\<close>
 lemma [iff]: "quasinat(0)"
 by (simp add: quasinat_def)
 
 lemma [iff]: "quasinat(succ(x))"
 by (simp add: quasinat_def)
 
 lemma nat_imp_quasinat: "n \<in> nat ==> quasinat(n)"
 by (erule natE, simp_all)
 
 lemma non_nat_case: "~ quasinat(x) ==> nat_case(a,b,x) = 0"
 by (simp add: quasinat_def nat_case_def)
 
 lemma nat_cases_disj: "k=0 | (\<exists>y. k = succ(y)) | ~ quasinat(k)"
 apply (case_tac "k=0", simp)
 apply (case_tac "\<exists>m. k = succ(m)")
 apply (simp_all add: quasinat_def)
 done
 
 lemma nat_cases:
      "[|k=0 ==> P;  !!y. k = succ(y) ==> P; ~ quasinat(k) ==> P|] ==> P"
 by (insert nat_cases_disj [of k], blast)
 
 (** nat_case **)
 
 lemma nat_case_0 [simp]: "nat_case(a,b,0) = a"
 by (simp add: nat_case_def)
 
 lemma nat_case_succ [simp]: "nat_case(a,b,succ(n)) = b(n)"
 by (simp add: nat_case_def)
 
 lemma nat_case_type [TC]:
     "[| n \<in> nat;  a \<in> C(0);  !!m. m \<in> nat ==> b(m): C(succ(m)) |]
      ==> nat_case(a,b,n) \<in> C(n)"
 by (erule nat_induct, auto)
 
 lemma split_nat_case:
   "P(nat_case(a,b,k)) \<longleftrightarrow>
    ((k=0 \<longrightarrow> P(a)) & (\<forall>x. k=succ(x) \<longrightarrow> P(b(x))) & (~ quasinat(k) \<longrightarrow> P(0)))"
 apply (rule nat_cases [of k])
 apply (auto simp add: non_nat_case)
 done
 
 
 subsection\<open>Recursion on the Natural Numbers\<close>
 
 (** nat_rec is used to define eclose and transrec, then becomes obsolete.
     The operator rec, from arith.thy, has fewer typing conditions **)
 
 lemma nat_rec_0: "nat_rec(0,a,b) = a"
 apply (rule nat_rec_def [THEN def_wfrec, THEN trans])
  apply (rule wf_Memrel)
 apply (rule nat_case_0)
 done
 
 lemma nat_rec_succ: "m \<in> nat ==> nat_rec(succ(m),a,b) = b(m, nat_rec(m,a,b))"
 apply (rule nat_rec_def [THEN def_wfrec, THEN trans])
  apply (rule wf_Memrel)
 apply (simp add: vimage_singleton_iff)
 done
 
 (** The union of two natural numbers is a natural number -- their maximum **)
 
 lemma Un_nat_type [TC]: "[| i \<in> nat; j \<in> nat |] ==> i \<union> j \<in> nat"
 apply (rule Un_least_lt [THEN ltD])
 apply (simp_all add: lt_def)
 done
 
 lemma Int_nat_type [TC]: "[| i \<in> nat; j \<in> nat |] ==> i \<inter> j \<in> nat"
 apply (rule Int_greatest_lt [THEN ltD])
 apply (simp_all add: lt_def)
 done
 
 (*needed to simplify unions over nat*)
 lemma nat_nonempty [simp]: "nat \<noteq> 0"
 by blast
 
 text\<open>A natural number is the set of its predecessors\<close>
 lemma nat_eq_Collect_lt: "i \<in> nat ==> {j\<in>nat. j<i} = i"
 apply (rule equalityI)
 apply (blast dest: ltD)
 apply (auto simp add: Ord_mem_iff_lt)
 apply (blast intro: lt_trans)
 done
 
 lemma Le_iff [iff]: "<x,y> \<in> Le \<longleftrightarrow> x \<le> y & x \<in> nat & y \<in> nat"
 by (force simp add: Le_def)
 
 end
diff --git a/src/ZF/Ordinal.thy b/src/ZF/Ordinal.thy
--- a/src/ZF/Ordinal.thy
+++ b/src/ZF/Ordinal.thy
@@ -1,764 +1,765 @@
 (*  Title:      ZF/Ordinal.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
 *)
 
 section\<open>Transitive Sets and Ordinals\<close>
 
 theory Ordinal imports WF Bool equalities begin
 
 definition
   Memrel        :: "i=>i"  where
     "Memrel(A)   == {z\<in>A*A . \<exists>x y. z=<x,y> & x\<in>y }"
 
 definition
   Transset  :: "i=>o"  where
     "Transset(i) == \<forall>x\<in>i. x<=i"
 
 definition
   Ord  :: "i=>o"  where
     "Ord(i)      == Transset(i) & (\<forall>x\<in>i. Transset(x))"
 
 definition
   lt        :: "[i,i] => o"  (infixl \<open><\<close> 50)   (*less-than on ordinals*)  where
     "i<j         == i\<in>j & Ord(j)"
 
 definition
   Limit         :: "i=>o"  where
     "Limit(i)    == Ord(i) & 0<i & (\<forall>y. y<i \<longrightarrow> succ(y)<i)"
 
 abbreviation
   le  (infixl \<open>\<le>\<close> 50) where
   "x \<le> y == x < succ(y)"
 
 
 subsection\<open>Rules for Transset\<close>
 
 subsubsection\<open>Three Neat Characterisations of Transset\<close>
 
 lemma Transset_iff_Pow: "Transset(A) <-> A<=Pow(A)"
 by (unfold Transset_def, blast)
 
 lemma Transset_iff_Union_succ: "Transset(A) <-> \<Union>(succ(A)) = A"
 apply (unfold Transset_def)
 apply (blast elim!: equalityE)
 done
 
 lemma Transset_iff_Union_subset: "Transset(A) <-> \<Union>(A) \<subseteq> A"
 by (unfold Transset_def, blast)
 
 subsubsection\<open>Consequences of Downwards Closure\<close>
 
 lemma Transset_doubleton_D:
     "[| Transset(C); {a,b}: C |] ==> a\<in>C & b\<in>C"
 by (unfold Transset_def, blast)
 
 lemma Transset_Pair_D:
     "[| Transset(C); <a,b>\<in>C |] ==> a\<in>C & b\<in>C"
 apply (simp add: Pair_def)
 apply (blast dest: Transset_doubleton_D)
 done
 
 lemma Transset_includes_domain:
     "[| Transset(C); A*B \<subseteq> C; b \<in> B |] ==> A \<subseteq> C"
 by (blast dest: Transset_Pair_D)
 
 lemma Transset_includes_range:
     "[| Transset(C); A*B \<subseteq> C; a \<in> A |] ==> B \<subseteq> C"
 by (blast dest: Transset_Pair_D)
 
 subsubsection\<open>Closure Properties\<close>
 
 lemma Transset_0: "Transset(0)"
 by (unfold Transset_def, blast)
 
 lemma Transset_Un:
     "[| Transset(i);  Transset(j) |] ==> Transset(i \<union> j)"
 by (unfold Transset_def, blast)
 
 lemma Transset_Int:
     "[| Transset(i);  Transset(j) |] ==> Transset(i \<inter> j)"
 by (unfold Transset_def, blast)
 
 lemma Transset_succ: "Transset(i) ==> Transset(succ(i))"
 by (unfold Transset_def, blast)
 
 lemma Transset_Pow: "Transset(i) ==> Transset(Pow(i))"
 by (unfold Transset_def, blast)
 
 lemma Transset_Union: "Transset(A) ==> Transset(\<Union>(A))"
 by (unfold Transset_def, blast)
 
 lemma Transset_Union_family:
     "[| !!i. i\<in>A ==> Transset(i) |] ==> Transset(\<Union>(A))"
 by (unfold Transset_def, blast)
 
 lemma Transset_Inter_family:
     "[| !!i. i\<in>A ==> Transset(i) |] ==> Transset(\<Inter>(A))"
 by (unfold Inter_def Transset_def, blast)
 
 lemma Transset_UN:
      "(!!x. x \<in> A ==> Transset(B(x))) ==> Transset (\<Union>x\<in>A. B(x))"
 by (rule Transset_Union_family, auto)
 
 lemma Transset_INT:
      "(!!x. x \<in> A ==> Transset(B(x))) ==> Transset (\<Inter>x\<in>A. B(x))"
 by (rule Transset_Inter_family, auto)
 
 
 subsection\<open>Lemmas for Ordinals\<close>
 
 lemma OrdI:
     "[| Transset(i);  !!x. x\<in>i ==> Transset(x) |]  ==>  Ord(i)"
 by (simp add: Ord_def)
 
 lemma Ord_is_Transset: "Ord(i) ==> Transset(i)"
 by (simp add: Ord_def)
 
 lemma Ord_contains_Transset:
     "[| Ord(i);  j\<in>i |] ==> Transset(j) "
 by (unfold Ord_def, blast)
 
 
 lemma Ord_in_Ord: "[| Ord(i);  j\<in>i |] ==> Ord(j)"
 by (unfold Ord_def Transset_def, blast)
 
 (*suitable for rewriting PROVIDED i has been fixed*)
 lemma Ord_in_Ord': "[| j\<in>i; Ord(i) |] ==> Ord(j)"
 by (blast intro: Ord_in_Ord)
 
 (* Ord(succ(j)) ==> Ord(j) *)
 lemmas Ord_succD = Ord_in_Ord [OF _ succI1]
 
 lemma Ord_subset_Ord: "[| Ord(i);  Transset(j);  j<=i |] ==> Ord(j)"
 by (simp add: Ord_def Transset_def, blast)
 
 lemma OrdmemD: "[| j\<in>i;  Ord(i) |] ==> j<=i"
 by (unfold Ord_def Transset_def, blast)
 
 lemma Ord_trans: "[| i\<in>j;  j\<in>k;  Ord(k) |] ==> i\<in>k"
 by (blast dest: OrdmemD)
 
 lemma Ord_succ_subsetI: "[| i\<in>j;  Ord(j) |] ==> succ(i) \<subseteq> j"
 by (blast dest: OrdmemD)
 
 
 subsection\<open>The Construction of Ordinals: 0, succ, Union\<close>
 
 lemma Ord_0 [iff,TC]: "Ord(0)"
 by (blast intro: OrdI Transset_0)
 
 lemma Ord_succ [TC]: "Ord(i) ==> Ord(succ(i))"
 by (blast intro: OrdI Transset_succ Ord_is_Transset Ord_contains_Transset)
 
 lemmas Ord_1 = Ord_0 [THEN Ord_succ]
 
 lemma Ord_succ_iff [iff]: "Ord(succ(i)) <-> Ord(i)"
 by (blast intro: Ord_succ dest!: Ord_succD)
 
 lemma Ord_Un [intro,simp,TC]: "[| Ord(i); Ord(j) |] ==> Ord(i \<union> j)"
 apply (unfold Ord_def)
 apply (blast intro!: Transset_Un)
 done
 
 lemma Ord_Int [TC]: "[| Ord(i); Ord(j) |] ==> Ord(i \<inter> j)"
 apply (unfold Ord_def)
 apply (blast intro!: Transset_Int)
 done
 
 text\<open>There is no set of all ordinals, for then it would contain itself\<close>
 lemma ON_class: "~ (\<forall>i. i\<in>X <-> Ord(i))"
 proof (rule notI)
   assume X: "\<forall>i. i \<in> X \<longleftrightarrow> Ord(i)"
   have "\<forall>x y. x\<in>X \<longrightarrow> y\<in>x \<longrightarrow> y\<in>X"
     by (simp add: X, blast intro: Ord_in_Ord)
   hence "Transset(X)"
      by (auto simp add: Transset_def)
   moreover have "\<And>x. x \<in> X \<Longrightarrow> Transset(x)"
      by (simp add: X Ord_def)
   ultimately have "Ord(X)" by (rule OrdI)
   hence "X \<in> X" by (simp add: X)
   thus "False" by (rule mem_irrefl)
 qed
 
 subsection\<open>< is 'less Than' for Ordinals\<close>
 
 lemma ltI: "[| i\<in>j;  Ord(j) |] ==> i<j"
 by (unfold lt_def, blast)
 
 lemma ltE:
     "[| i<j;  [| i\<in>j;  Ord(i);  Ord(j) |] ==> P |] ==> P"
 apply (unfold lt_def)
 apply (blast intro: Ord_in_Ord)
 done
 
 lemma ltD: "i<j ==> i\<in>j"
 by (erule ltE, assumption)
 
 lemma not_lt0 [simp]: "~ i<0"
 by (unfold lt_def, blast)
 
 lemma lt_Ord: "j<i ==> Ord(j)"
 by (erule ltE, assumption)
 
 lemma lt_Ord2: "j<i ==> Ord(i)"
 by (erule ltE, assumption)
 
 (* @{term"ja \<le> j ==> Ord(j)"} *)
 lemmas le_Ord2 = lt_Ord2 [THEN Ord_succD]
 
 (* i<0 ==> R *)
 lemmas lt0E = not_lt0 [THEN notE, elim!]
 
 lemma lt_trans [trans]: "[| i<j;  j<k |] ==> i<k"
 by (blast intro!: ltI elim!: ltE intro: Ord_trans)
 
 lemma lt_not_sym: "i<j ==> ~ (j<i)"
 apply (unfold lt_def)
 apply (blast elim: mem_asym)
 done
 
 (* [| i<j;  ~P ==> j<i |] ==> P *)
 lemmas lt_asym = lt_not_sym [THEN swap]
 
 lemma lt_irrefl [elim!]: "i<i ==> P"
 by (blast intro: lt_asym)
 
 lemma lt_not_refl: "~ i<i"
 apply (rule notI)
 apply (erule lt_irrefl)
 done
 
 
 text\<open>Recall that  \<^term>\<open>i \<le> j\<close>  abbreviates  \<^term>\<open>i<succ(j)\<close> !!\<close>
 
 lemma le_iff: "i \<le> j <-> i<j | (i=j & Ord(j))"
 by (unfold lt_def, blast)
 
 (*Equivalently, i<j ==> i < succ(j)*)
 lemma leI: "i<j ==> i \<le> j"
 by (simp add: le_iff)
 
 lemma le_eqI: "[| i=j;  Ord(j) |] ==> i \<le> j"
 by (simp add: le_iff)
 
 lemmas le_refl = refl [THEN le_eqI]
 
 lemma le_refl_iff [iff]: "i \<le> i <-> Ord(i)"
 by (simp (no_asm_simp) add: lt_not_refl le_iff)
 
 lemma leCI: "(~ (i=j & Ord(j)) ==> i<j) ==> i \<le> j"
 by (simp add: le_iff, blast)
 
 lemma leE:
     "[| i \<le> j;  i<j ==> P;  [| i=j;  Ord(j) |] ==> P |] ==> P"
 by (simp add: le_iff, blast)
 
 lemma le_anti_sym: "[| i \<le> j;  j \<le> i |] ==> i=j"
 apply (simp add: le_iff)
 apply (blast elim: lt_asym)
 done
 
 lemma le0_iff [simp]: "i \<le> 0 <-> i=0"
 by (blast elim!: leE)
 
 lemmas le0D = le0_iff [THEN iffD1, dest!]
 
 subsection\<open>Natural Deduction Rules for Memrel\<close>
 
 (*The lemmas MemrelI/E give better speed than [iff] here*)
 lemma Memrel_iff [simp]: "<a,b> \<in> Memrel(A) <-> a\<in>b & a\<in>A & b\<in>A"
 by (unfold Memrel_def, blast)
 
 lemma MemrelI [intro!]: "[| a \<in> b;  a \<in> A;  b \<in> A |] ==> <a,b> \<in> Memrel(A)"
 by auto
 
 lemma MemrelE [elim!]:
     "[| <a,b> \<in> Memrel(A);
         [| a \<in> A;  b \<in> A;  a\<in>b |]  ==> P |]
      ==> P"
 by auto
 
 lemma Memrel_type: "Memrel(A) \<subseteq> A*A"
 by (unfold Memrel_def, blast)
 
 lemma Memrel_mono: "A<=B ==> Memrel(A) \<subseteq> Memrel(B)"
 by (unfold Memrel_def, blast)
 
 lemma Memrel_0 [simp]: "Memrel(0) = 0"
 by (unfold Memrel_def, blast)
 
 lemma Memrel_1 [simp]: "Memrel(1) = 0"
 by (unfold Memrel_def, blast)
 
 lemma relation_Memrel: "relation(Memrel(A))"
 by (simp add: relation_def Memrel_def)
 
 (*The membership relation (as a set) is well-founded.
   Proof idea: show A<=B by applying the foundation axiom to A-B *)
 lemma wf_Memrel: "wf(Memrel(A))"
 apply (unfold wf_def)
 apply (rule foundation [THEN disjE, THEN allI], erule disjI1, blast)
 done
 
 text\<open>The premise \<^term>\<open>Ord(i)\<close> does not suffice.\<close>
 lemma trans_Memrel:
     "Ord(i) ==> trans(Memrel(i))"
 by (unfold Ord_def Transset_def trans_def, blast)
 
 text\<open>However, the following premise is strong enough.\<close>
 lemma Transset_trans_Memrel:
     "\<forall>j\<in>i. Transset(j) ==> trans(Memrel(i))"
 by (unfold Transset_def trans_def, blast)
 
 (*If Transset(A) then Memrel(A) internalizes the membership relation below A*)
 lemma Transset_Memrel_iff:
     "Transset(A) ==> <a,b> \<in> Memrel(A) <-> a\<in>b & b\<in>A"
 by (unfold Transset_def, blast)
 
 
 subsection\<open>Transfinite Induction\<close>
 
 (*Epsilon induction over a transitive set*)
 lemma Transset_induct:
     "[| i \<in> k;  Transset(k);
         !!x.[| x \<in> k;  \<forall>y\<in>x. P(y) |] ==> P(x) |]
      ==>  P(i)"
 apply (simp add: Transset_def)
 apply (erule wf_Memrel [THEN wf_induct2], blast+)
 done
 
 (*Induction over an ordinal*)
-lemmas Ord_induct [consumes 2] = Transset_induct [rule_format, OF _ Ord_is_Transset]
+lemma Ord_induct [consumes 2]:
+  "i \<in> k \<Longrightarrow> Ord(k) \<Longrightarrow> (\<And>x. x \<in> k \<Longrightarrow> (\<And>y. y \<in> x \<Longrightarrow> P(y)) \<Longrightarrow> P(x)) \<Longrightarrow> P(i)"
+  using Transset_induct [OF _ Ord_is_Transset, of i k P] by simp
 
 (*Induction over the class of ordinals -- a useful corollary of Ord_induct*)
-
-lemma trans_induct [rule_format, consumes 1, case_names step]:
-    "[| Ord(i);
-        !!x.[| Ord(x);  \<forall>y\<in>x. P(y) |] ==> P(x) |]
-     ==>  P(i)"
-apply (rule Ord_succ [THEN succI1 [THEN Ord_induct]], assumption)
-apply (blast intro: Ord_succ [THEN Ord_in_Ord])
-done
+lemma trans_induct [consumes 1, case_names step]:
+  "Ord(i) \<Longrightarrow> (\<And>x. Ord(x) \<Longrightarrow> (\<And>y. y \<in> x \<Longrightarrow> P(y)) \<Longrightarrow> P(x)) \<Longrightarrow> P(i)"
+  apply (rule Ord_succ [THEN succI1 [THEN Ord_induct]], assumption)
+  apply (blast intro: Ord_succ [THEN Ord_in_Ord])
+  done
 
 
 section\<open>Fundamental properties of the epsilon ordering (< on ordinals)\<close>
 
 
 subsubsection\<open>Proving That < is a Linear Ordering on the Ordinals\<close>
 
 lemma Ord_linear:
      "Ord(i) \<Longrightarrow> Ord(j) \<Longrightarrow> i\<in>j | i=j | j\<in>i"
 proof (induct i arbitrary: j rule: trans_induct)
   case (step i)
   note step_i = step
   show ?case using \<open>Ord(j)\<close>
     proof (induct j rule: trans_induct)
       case (step j)
       thus ?case using step_i
         by (blast dest: Ord_trans)
     qed
 qed
 
 text\<open>The trichotomy law for ordinals\<close>
 lemma Ord_linear_lt:
  assumes o: "Ord(i)" "Ord(j)"
  obtains (lt) "i<j" | (eq) "i=j" | (gt) "j<i"
 apply (simp add: lt_def)
 apply (rule_tac i1=i and j1=j in Ord_linear [THEN disjE])
 apply (blast intro: o)+
 done
 
 lemma Ord_linear2:
  assumes o: "Ord(i)" "Ord(j)"
  obtains (lt) "i<j" | (ge) "j \<le> i"
 apply (rule_tac i = i and j = j in Ord_linear_lt)
 apply (blast intro: leI le_eqI sym o) +
 done
 
 lemma Ord_linear_le:
  assumes o: "Ord(i)" "Ord(j)"
  obtains (le) "i \<le> j" | (ge) "j \<le> i"
 apply (rule_tac i = i and j = j in Ord_linear_lt)
 apply (blast intro: leI le_eqI o) +
 done
 
 lemma le_imp_not_lt: "j \<le> i ==> ~ i<j"
 by (blast elim!: leE elim: lt_asym)
 
 lemma not_lt_imp_le: "[| ~ i<j;  Ord(i);  Ord(j) |] ==> j \<le> i"
 by (rule_tac i = i and j = j in Ord_linear2, auto)
 
 
 subsubsection \<open>Some Rewrite Rules for \<open><\<close>, \<open>\<le>\<close>\<close>
 
 lemma Ord_mem_iff_lt: "Ord(j) ==> i\<in>j <-> i<j"
 by (unfold lt_def, blast)
 
 lemma not_lt_iff_le: "[| Ord(i);  Ord(j) |] ==> ~ i<j <-> j \<le> i"
 by (blast dest: le_imp_not_lt not_lt_imp_le)
 
 lemma not_le_iff_lt: "[| Ord(i);  Ord(j) |] ==> ~ i \<le> j <-> j<i"
 by (simp (no_asm_simp) add: not_lt_iff_le [THEN iff_sym])
 
 (*This is identical to 0<succ(i) *)
 lemma Ord_0_le: "Ord(i) ==> 0 \<le> i"
 by (erule not_lt_iff_le [THEN iffD1], auto)
 
 lemma Ord_0_lt: "[| Ord(i);  i\<noteq>0 |] ==> 0<i"
 apply (erule not_le_iff_lt [THEN iffD1])
 apply (rule Ord_0, blast)
 done
 
 lemma Ord_0_lt_iff: "Ord(i) ==> i\<noteq>0 <-> 0<i"
 by (blast intro: Ord_0_lt)
 
 
 subsection\<open>Results about Less-Than or Equals\<close>
 
 (** For ordinals, @{term"j\<subseteq>i"} implies @{term"j \<le> i"} (less-than or equals) **)
 
 lemma zero_le_succ_iff [iff]: "0 \<le> succ(x) <-> Ord(x)"
 by (blast intro: Ord_0_le elim: ltE)
 
 lemma subset_imp_le: "[| j<=i;  Ord(i);  Ord(j) |] ==> j \<le> i"
 apply (rule not_lt_iff_le [THEN iffD1], assumption+)
 apply (blast elim: ltE mem_irrefl)
 done
 
 lemma le_imp_subset: "i \<le> j ==> i<=j"
 by (blast dest: OrdmemD elim: ltE leE)
 
 lemma le_subset_iff: "j \<le> i <-> j<=i & Ord(i) & Ord(j)"
 by (blast dest: subset_imp_le le_imp_subset elim: ltE)
 
 lemma le_succ_iff: "i \<le> succ(j) <-> i \<le> j | i=succ(j) & Ord(i)"
 apply (simp (no_asm) add: le_iff)
 apply blast
 done
 
 (*Just a variant of subset_imp_le*)
 lemma all_lt_imp_le: "[| Ord(i);  Ord(j);  !!x. x<j ==> x<i |] ==> j \<le> i"
 by (blast intro: not_lt_imp_le dest: lt_irrefl)
 
 subsubsection\<open>Transitivity Laws\<close>
 
 lemma lt_trans1: "[| i \<le> j;  j<k |] ==> i<k"
 by (blast elim!: leE intro: lt_trans)
 
 lemma lt_trans2: "[| i<j;  j \<le> k |] ==> i<k"
 by (blast elim!: leE intro: lt_trans)
 
 lemma le_trans: "[| i \<le> j;  j \<le> k |] ==> i \<le> k"
 by (blast intro: lt_trans1)
 
 lemma succ_leI: "i<j ==> succ(i) \<le> j"
 apply (rule not_lt_iff_le [THEN iffD1])
 apply (blast elim: ltE leE lt_asym)+
 done
 
 (*Identical to  succ(i) < succ(j) ==> i<j  *)
 lemma succ_leE: "succ(i) \<le> j ==> i<j"
 apply (rule not_le_iff_lt [THEN iffD1])
 apply (blast elim: ltE leE lt_asym)+
 done
 
 lemma succ_le_iff [iff]: "succ(i) \<le> j <-> i<j"
 by (blast intro: succ_leI succ_leE)
 
 lemma succ_le_imp_le: "succ(i) \<le> succ(j) ==> i \<le> j"
 by (blast dest!: succ_leE)
 
 lemma lt_subset_trans: "[| i \<subseteq> j;  j<k;  Ord(i) |] ==> i<k"
 apply (rule subset_imp_le [THEN lt_trans1])
 apply (blast intro: elim: ltE) +
 done
 
 lemma lt_imp_0_lt: "j<i ==> 0<i"
 by (blast intro: lt_trans1 Ord_0_le [OF lt_Ord])
 
 lemma succ_lt_iff: "succ(i) < j <-> i<j & succ(i) \<noteq> j"
 apply auto
 apply (blast intro: lt_trans le_refl dest: lt_Ord)
 apply (frule lt_Ord)
 apply (rule not_le_iff_lt [THEN iffD1])
   apply (blast intro: lt_Ord2)
  apply blast
 apply (simp add: lt_Ord lt_Ord2 le_iff)
 apply (blast dest: lt_asym)
 done
 
 lemma Ord_succ_mem_iff: "Ord(j) ==> succ(i) \<in> succ(j) <-> i\<in>j"
 apply (insert succ_le_iff [of i j])
 apply (simp add: lt_def)
 done
 
 subsubsection\<open>Union and Intersection\<close>
 
 lemma Un_upper1_le: "[| Ord(i); Ord(j) |] ==> i \<le> i \<union> j"
 by (rule Un_upper1 [THEN subset_imp_le], auto)
 
 lemma Un_upper2_le: "[| Ord(i); Ord(j) |] ==> j \<le> i \<union> j"
 by (rule Un_upper2 [THEN subset_imp_le], auto)
 
 (*Replacing k by succ(k') yields the similar rule for le!*)
 lemma Un_least_lt: "[| i<k;  j<k |] ==> i \<union> j < k"
 apply (rule_tac i = i and j = j in Ord_linear_le)
 apply (auto simp add: Un_commute le_subset_iff subset_Un_iff lt_Ord)
 done
 
 lemma Un_least_lt_iff: "[| Ord(i); Ord(j) |] ==> i \<union> j < k  <->  i<k & j<k"
 apply (safe intro!: Un_least_lt)
 apply (rule_tac [2] Un_upper2_le [THEN lt_trans1])
 apply (rule Un_upper1_le [THEN lt_trans1], auto)
 done
 
 lemma Un_least_mem_iff:
     "[| Ord(i); Ord(j); Ord(k) |] ==> i \<union> j \<in> k  <->  i\<in>k & j\<in>k"
 apply (insert Un_least_lt_iff [of i j k])
 apply (simp add: lt_def)
 done
 
 (*Replacing k by succ(k') yields the similar rule for le!*)
 lemma Int_greatest_lt: "[| i<k;  j<k |] ==> i \<inter> j < k"
 apply (rule_tac i = i and j = j in Ord_linear_le)
 apply (auto simp add: Int_commute le_subset_iff subset_Int_iff lt_Ord)
 done
 
 lemma Ord_Un_if:
      "[| Ord(i); Ord(j) |] ==> i \<union> j = (if j<i then i else j)"
 by (simp add: not_lt_iff_le le_imp_subset leI
               subset_Un_iff [symmetric]  subset_Un_iff2 [symmetric])
 
 lemma succ_Un_distrib:
      "[| Ord(i); Ord(j) |] ==> succ(i \<union> j) = succ(i) \<union> succ(j)"
 by (simp add: Ord_Un_if lt_Ord le_Ord2)
 
 lemma lt_Un_iff:
      "[| Ord(i); Ord(j) |] ==> k < i \<union> j <-> k < i | k < j"
 apply (simp add: Ord_Un_if not_lt_iff_le)
 apply (blast intro: leI lt_trans2)+
 done
 
 lemma le_Un_iff:
      "[| Ord(i); Ord(j) |] ==> k \<le> i \<union> j <-> k \<le> i | k \<le> j"
 by (simp add: succ_Un_distrib lt_Un_iff [symmetric])
 
 lemma Un_upper1_lt: "[|k < i; Ord(j)|] ==> k < i \<union> j"
 by (simp add: lt_Un_iff lt_Ord2)
 
 lemma Un_upper2_lt: "[|k < j; Ord(i)|] ==> k < i \<union> j"
 by (simp add: lt_Un_iff lt_Ord2)
 
 (*See also Transset_iff_Union_succ*)
 lemma Ord_Union_succ_eq: "Ord(i) ==> \<Union>(succ(i)) = i"
 by (blast intro: Ord_trans)
 
 
 subsection\<open>Results about Limits\<close>
 
 lemma Ord_Union [intro,simp,TC]: "[| !!i. i\<in>A ==> Ord(i) |] ==> Ord(\<Union>(A))"
 apply (rule Ord_is_Transset [THEN Transset_Union_family, THEN OrdI])
 apply (blast intro: Ord_contains_Transset)+
 done
 
 lemma Ord_UN [intro,simp,TC]:
      "[| !!x. x\<in>A ==> Ord(B(x)) |] ==> Ord(\<Union>x\<in>A. B(x))"
 by (rule Ord_Union, blast)
 
 lemma Ord_Inter [intro,simp,TC]:
     "[| !!i. i\<in>A ==> Ord(i) |] ==> Ord(\<Inter>(A))"
 apply (rule Transset_Inter_family [THEN OrdI])
 apply (blast intro: Ord_is_Transset)
 apply (simp add: Inter_def)
 apply (blast intro: Ord_contains_Transset)
 done
 
 lemma Ord_INT [intro,simp,TC]:
     "[| !!x. x\<in>A ==> Ord(B(x)) |] ==> Ord(\<Inter>x\<in>A. B(x))"
 by (rule Ord_Inter, blast)
 
 
 (* No < version of this theorem: consider that @{term"(\<Union>i\<in>nat.i)=nat"}! *)
 lemma UN_least_le:
     "[| Ord(i);  !!x. x\<in>A ==> b(x) \<le> i |] ==> (\<Union>x\<in>A. b(x)) \<le> i"
 apply (rule le_imp_subset [THEN UN_least, THEN subset_imp_le])
 apply (blast intro: Ord_UN elim: ltE)+
 done
 
 lemma UN_succ_least_lt:
     "[| j<i;  !!x. x\<in>A ==> b(x)<j |] ==> (\<Union>x\<in>A. succ(b(x))) < i"
 apply (rule ltE, assumption)
 apply (rule UN_least_le [THEN lt_trans2])
 apply (blast intro: succ_leI)+
 done
 
 lemma UN_upper_lt:
      "[| a\<in>A;  i < b(a);  Ord(\<Union>x\<in>A. b(x)) |] ==> i < (\<Union>x\<in>A. b(x))"
 by (unfold lt_def, blast)
 
 lemma UN_upper_le:
      "[| a \<in> A;  i \<le> b(a);  Ord(\<Union>x\<in>A. b(x)) |] ==> i \<le> (\<Union>x\<in>A. b(x))"
 apply (frule ltD)
 apply (rule le_imp_subset [THEN subset_trans, THEN subset_imp_le])
 apply (blast intro: lt_Ord UN_upper)+
 done
 
 lemma lt_Union_iff: "\<forall>i\<in>A. Ord(i) ==> (j < \<Union>(A)) <-> (\<exists>i\<in>A. j<i)"
 by (auto simp: lt_def Ord_Union)
 
 lemma Union_upper_le:
      "[| j \<in> J;  i\<le>j;  Ord(\<Union>(J)) |] ==> i \<le> \<Union>J"
 apply (subst Union_eq_UN)
 apply (rule UN_upper_le, auto)
 done
 
 lemma le_implies_UN_le_UN:
     "[| !!x. x\<in>A ==> c(x) \<le> d(x) |] ==> (\<Union>x\<in>A. c(x)) \<le> (\<Union>x\<in>A. d(x))"
 apply (rule UN_least_le)
 apply (rule_tac [2] UN_upper_le)
 apply (blast intro: Ord_UN le_Ord2)+
 done
 
 lemma Ord_equality: "Ord(i) ==> (\<Union>y\<in>i. succ(y)) = i"
 by (blast intro: Ord_trans)
 
 (*Holds for all transitive sets, not just ordinals*)
 lemma Ord_Union_subset: "Ord(i) ==> \<Union>(i) \<subseteq> i"
 by (blast intro: Ord_trans)
 
 
 subsection\<open>Limit Ordinals -- General Properties\<close>
 
 lemma Limit_Union_eq: "Limit(i) ==> \<Union>(i) = i"
 apply (unfold Limit_def)
 apply (fast intro!: ltI elim!: ltE elim: Ord_trans)
 done
 
 lemma Limit_is_Ord: "Limit(i) ==> Ord(i)"
 apply (unfold Limit_def)
 apply (erule conjunct1)
 done
 
 lemma Limit_has_0: "Limit(i) ==> 0 < i"
 apply (unfold Limit_def)
 apply (erule conjunct2 [THEN conjunct1])
 done
 
 lemma Limit_nonzero: "Limit(i) ==> i \<noteq> 0"
 by (drule Limit_has_0, blast)
 
 lemma Limit_has_succ: "[| Limit(i);  j<i |] ==> succ(j) < i"
 by (unfold Limit_def, blast)
 
 lemma Limit_succ_lt_iff [simp]: "Limit(i) ==> succ(j) < i <-> (j<i)"
 apply (safe intro!: Limit_has_succ)
 apply (frule lt_Ord)
 apply (blast intro: lt_trans)
 done
 
 lemma zero_not_Limit [iff]: "~ Limit(0)"
 by (simp add: Limit_def)
 
 lemma Limit_has_1: "Limit(i) ==> 1 < i"
 by (blast intro: Limit_has_0 Limit_has_succ)
 
 lemma increasing_LimitI: "[| 0<l; \<forall>x\<in>l. \<exists>y\<in>l. x<y |] ==> Limit(l)"
 apply (unfold Limit_def, simp add: lt_Ord2, clarify)
 apply (drule_tac i=y in ltD)
 apply (blast intro: lt_trans1 [OF _ ltI] lt_Ord2)
 done
 
 lemma non_succ_LimitI:
   assumes i: "0<i" and nsucc: "\<And>y. succ(y) \<noteq> i"
   shows "Limit(i)"
 proof -
   have Oi: "Ord(i)" using i by (simp add: lt_def)
   { fix y
     assume yi: "y<i"
     hence Osy: "Ord(succ(y))" by (simp add: lt_Ord Ord_succ)
     have "~ i \<le> y" using yi by (blast dest: le_imp_not_lt)
     hence "succ(y) < i" using nsucc [of y]
       by (blast intro: Ord_linear_lt [OF Osy Oi]) }
   thus ?thesis using i Oi by (auto simp add: Limit_def)
 qed
 
 lemma succ_LimitE [elim!]: "Limit(succ(i)) ==> P"
 apply (rule lt_irrefl)
 apply (rule Limit_has_succ, assumption)
 apply (erule Limit_is_Ord [THEN Ord_succD, THEN le_refl])
 done
 
 lemma not_succ_Limit [simp]: "~ Limit(succ(i))"
 by blast
 
 lemma Limit_le_succD: "[| Limit(i);  i \<le> succ(j) |] ==> i \<le> j"
 by (blast elim!: leE)
 
 
 subsubsection\<open>Traditional 3-Way Case Analysis on Ordinals\<close>
 
 lemma Ord_cases_disj: "Ord(i) ==> i=0 | (\<exists>j. Ord(j) & i=succ(j)) | Limit(i)"
 by (blast intro!: non_succ_LimitI Ord_0_lt)
 
 lemma Ord_cases:
  assumes i: "Ord(i)"
  obtains ("0") "i=0" | (succ) j where "Ord(j)" "i=succ(j)" | (limit) "Limit(i)"
 by (insert Ord_cases_disj [OF i], auto)
 
 lemma trans_induct3_raw:
      "[| Ord(i);
          P(0);
          !!x. [| Ord(x);  P(x) |] ==> P(succ(x));
          !!x. [| Limit(x);  \<forall>y\<in>x. P(y) |] ==> P(x)
       |] ==> P(i)"
 apply (erule trans_induct)
 apply (erule Ord_cases, blast+)
 done
 
-lemmas trans_induct3 = trans_induct3_raw [rule_format, case_names 0 succ limit, consumes 1]
+lemma trans_induct3 [case_names 0 succ limit, consumes 1]:
+  "Ord(i) \<Longrightarrow> P(0) \<Longrightarrow> (\<And>x. Ord(x) \<Longrightarrow> P(x) \<Longrightarrow> P(succ(x))) \<Longrightarrow> (\<And>x. Limit(x) \<Longrightarrow> (\<And>y. y \<in> x \<Longrightarrow> P(y)) \<Longrightarrow> P(x)) \<Longrightarrow> P(i)"
+  using trans_induct3_raw [of i P] by simp
 
 text\<open>A set of ordinals is either empty, contains its own union, or its
 union is a limit ordinal.\<close>
 
 lemma Union_le: "[| !!x. x\<in>I ==> x\<le>j; Ord(j) |] ==> \<Union>(I) \<le> j"
   by (auto simp add: le_subset_iff Union_least)
 
 lemma Ord_set_cases:
   assumes I: "\<forall>i\<in>I. Ord(i)"
   shows "I=0 \<or> \<Union>(I) \<in> I \<or> (\<Union>(I) \<notin> I \<and> Limit(\<Union>(I)))"
 proof (cases "\<Union>(I)" rule: Ord_cases)
   show "Ord(\<Union>I)" using I by (blast intro: Ord_Union)
 next
   assume "\<Union>I = 0" thus ?thesis by (simp, blast intro: subst_elem)
 next
   fix j
   assume j: "Ord(j)" and UIj:"\<Union>(I) = succ(j)"
   { assume "\<forall>i\<in>I. i\<le>j"
     hence "\<Union>(I) \<le> j"
       by (simp add: Union_le j)
     hence False
       by (simp add: UIj lt_not_refl) }
   then obtain i where i: "i \<in> I" "succ(j) \<le> i" using I j
     by (atomize, auto simp add: not_le_iff_lt)
   have "\<Union>(I) \<le> succ(j)" using UIj j by auto
   hence "i \<le> succ(j)" using i
     by (simp add: le_subset_iff Union_subset_iff)
   hence "succ(j) = i" using i
     by (blast intro: le_anti_sym)
   hence "succ(j) \<in> I" by (simp add: i)
   thus ?thesis by (simp add: UIj)
 next
   assume "Limit(\<Union>I)" thus ?thesis by auto
 qed
 
 text\<open>If the union of a set of ordinals is a successor, then it is an element of that set.\<close>
 lemma Ord_Union_eq_succD: "[|\<forall>x\<in>X. Ord(x);  \<Union>X = succ(j)|] ==> succ(j) \<in> X"
   by (drule Ord_set_cases, auto)
 
-lemma Limit_Union [rule_format]: "[| I \<noteq> 0;  \<forall>i\<in>I. Limit(i) |] ==> Limit(\<Union>I)"
+lemma Limit_Union [rule_format]: "[| I \<noteq> 0;  (\<And>i. i\<in>I \<Longrightarrow> Limit(i)) |] ==> Limit(\<Union>I)"
 apply (simp add: Limit_def lt_def)
 apply (blast intro!: equalityI)
 done
 
 end
diff --git a/src/ZF/WF.thy b/src/ZF/WF.thy
--- a/src/ZF/WF.thy
+++ b/src/ZF/WF.thy
@@ -1,371 +1,372 @@
 (*  Title:      ZF/WF.thy
     Author:     Tobias Nipkow and Lawrence C Paulson
     Copyright   1994  University of Cambridge
 
 Derived first for transitive relations, and finally for arbitrary WF relations
 via wf_trancl and trans_trancl.
 
 It is difficult to derive this general case directly, using r^+ instead of
 r.  In is_recfun, the two occurrences of the relation must have the same
 form.  Inserting r^+ in the_recfun or wftrec yields a recursion rule with
 r^+ -`` {a} instead of r-``{a}.  This recursion rule is stronger in
 principle, but harder to use, especially to prove wfrec_eclose_eq in
 epsilon.ML.  Expanding out the definition of wftrec in wfrec would yield
 a mess.
 *)
 
 section\<open>Well-Founded Recursion\<close>
 
 theory WF imports Trancl begin
 
 definition
   wf           :: "i=>o"  where
     (*r is a well-founded relation*)
     "wf(r) == \<forall>Z. Z=0 | (\<exists>x\<in>Z. \<forall>y. <y,x>:r \<longrightarrow> ~ y \<in> Z)"
 
 definition
   wf_on        :: "[i,i]=>o"                      (\<open>wf[_]'(_')\<close>)  where
     (*r is well-founded on A*)
     "wf_on(A,r) == wf(r \<inter> A*A)"
 
 definition
   is_recfun    :: "[i, i, [i,i]=>i, i] =>o"  where
     "is_recfun(r,a,H,f) == (f = (\<lambda>x\<in>r-``{a}. H(x, restrict(f, r-``{x}))))"
 
 definition
   the_recfun   :: "[i, i, [i,i]=>i] =>i"  where
     "the_recfun(r,a,H) == (THE f. is_recfun(r,a,H,f))"
 
 definition
   wftrec :: "[i, i, [i,i]=>i] =>i"  where
     "wftrec(r,a,H) == H(a, the_recfun(r,a,H))"
 
 definition
   wfrec :: "[i, i, [i,i]=>i] =>i"  where
     (*public version.  Does not require r to be transitive*)
     "wfrec(r,a,H) == wftrec(r^+, a, %x f. H(x, restrict(f,r-``{x})))"
 
 definition
   wfrec_on     :: "[i, i, i, [i,i]=>i] =>i"       (\<open>wfrec[_]'(_,_,_')\<close>)  where
     "wfrec[A](r,a,H) == wfrec(r \<inter> A*A, a, H)"
 
 
 subsection\<open>Well-Founded Relations\<close>
 
 subsubsection\<open>Equivalences between \<^term>\<open>wf\<close> and \<^term>\<open>wf_on\<close>\<close>
 
 lemma wf_imp_wf_on: "wf(r) ==> wf[A](r)"
 by (unfold wf_def wf_on_def, force)
 
 lemma wf_on_imp_wf: "[|wf[A](r); r \<subseteq> A*A|] ==> wf(r)"
 by (simp add: wf_on_def subset_Int_iff)
 
 lemma wf_on_field_imp_wf: "wf[field(r)](r) ==> wf(r)"
 by (unfold wf_def wf_on_def, fast)
 
 lemma wf_iff_wf_on_field: "wf(r) \<longleftrightarrow> wf[field(r)](r)"
 by (blast intro: wf_imp_wf_on wf_on_field_imp_wf)
 
 lemma wf_on_subset_A: "[| wf[A](r);  B<=A |] ==> wf[B](r)"
 by (unfold wf_on_def wf_def, fast)
 
 lemma wf_on_subset_r: "[| wf[A](r); s<=r |] ==> wf[A](s)"
 by (unfold wf_on_def wf_def, fast)
 
 lemma wf_subset: "[|wf(s); r<=s|] ==> wf(r)"
 by (simp add: wf_def, fast)
 
 subsubsection\<open>Introduction Rules for \<^term>\<open>wf_on\<close>\<close>
 
 text\<open>If every non-empty subset of \<^term>\<open>A\<close> has an \<^term>\<open>r\<close>-minimal element
    then we have \<^term>\<open>wf[A](r)\<close>.\<close>
 lemma wf_onI:
  assumes prem: "!!Z u. [| Z<=A;  u \<in> Z;  \<forall>x\<in>Z. \<exists>y\<in>Z. <y,x>:r |] ==> False"
  shows         "wf[A](r)"
 apply (unfold wf_on_def wf_def)
 apply (rule equals0I [THEN disjCI, THEN allI])
 apply (rule_tac Z = Z in prem, blast+)
 done
 
 text\<open>If \<^term>\<open>r\<close> allows well-founded induction over \<^term>\<open>A\<close>
    then we have \<^term>\<open>wf[A](r)\<close>.   Premise is equivalent to
   \<^prop>\<open>!!B. \<forall>x\<in>A. (\<forall>y. <y,x>: r \<longrightarrow> y \<in> B) \<longrightarrow> x \<in> B ==> A<=B\<close>\<close>
 lemma wf_onI2:
  assumes prem: "!!y B. [| \<forall>x\<in>A. (\<forall>y\<in>A. <y,x>:r \<longrightarrow> y \<in> B) \<longrightarrow> x \<in> B;   y \<in> A |]
                        ==> y \<in> B"
  shows         "wf[A](r)"
 apply (rule wf_onI)
 apply (rule_tac c=u in prem [THEN DiffE])
   prefer 3 apply blast
  apply fast+
 done
 
 
 subsubsection\<open>Well-founded Induction\<close>
 
 text\<open>Consider the least \<^term>\<open>z\<close> in \<^term>\<open>domain(r)\<close> such that
   \<^term>\<open>P(z)\<close> does not hold...\<close>
 lemma wf_induct_raw:
     "[| wf(r);
         !!x.[| \<forall>y. <y,x>: r \<longrightarrow> P(y) |] ==> P(x) |]
      ==> P(a)"
 apply (unfold wf_def)
 apply (erule_tac x = "{z \<in> domain(r). ~ P(z)}" in allE)
 apply blast
 done
 
 lemmas wf_induct = wf_induct_raw [rule_format, consumes 1, case_names step, induct set: wf]
 
 text\<open>The form of this rule is designed to match \<open>wfI\<close>\<close>
 lemma wf_induct2:
     "[| wf(r);  a \<in> A;  field(r)<=A;
         !!x.[| x \<in> A;  \<forall>y. <y,x>: r \<longrightarrow> P(y) |] ==> P(x) |]
      ==>  P(a)"
 apply (erule_tac P="a \<in> A" in rev_mp)
 apply (erule_tac a=a in wf_induct, blast)
 done
 
 lemma field_Int_square: "field(r \<inter> A*A) \<subseteq> A"
 by blast
 
 lemma wf_on_induct_raw [consumes 2, induct set: wf_on]:
     "[| wf[A](r);  a \<in> A;
         !!x.[| x \<in> A;  \<forall>y\<in>A. <y,x>: r \<longrightarrow> P(y) |] ==> P(x)
      |]  ==>  P(a)"
 apply (unfold wf_on_def)
 apply (erule wf_induct2, assumption)
 apply (rule field_Int_square, blast)
 done
 
-lemmas wf_on_induct =
-  wf_on_induct_raw [rule_format, consumes 2, case_names step, induct set: wf_on]
-
+lemma wf_on_induct [consumes 2, case_names step, induct set: wf_on]:
+  "wf[A](r) \<Longrightarrow> a \<in> A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> (\<And>y. y \<in> A \<Longrightarrow> \<langle>y, x\<rangle> \<in> r \<Longrightarrow> P(y)) \<Longrightarrow> P(x)) \<Longrightarrow> P(a)"
+  using wf_on_induct_raw [of A r a P] by simp
 
 text\<open>If \<^term>\<open>r\<close> allows well-founded induction
    then we have \<^term>\<open>wf(r)\<close>.\<close>
 lemma wfI:
     "[| field(r)<=A;
         !!y B. [| \<forall>x\<in>A. (\<forall>y\<in>A. <y,x>:r \<longrightarrow> y \<in> B) \<longrightarrow> x \<in> B;  y \<in> A|]
                ==> y \<in> B |]
      ==>  wf(r)"
 apply (rule wf_on_subset_A [THEN wf_on_field_imp_wf])
 apply (rule wf_onI2)
  prefer 2 apply blast
 apply blast
 done
 
 
 subsection\<open>Basic Properties of Well-Founded Relations\<close>
 
 lemma wf_not_refl: "wf(r) ==> <a,a> \<notin> r"
 by (erule_tac a=a in wf_induct, blast)
 
 lemma wf_not_sym [rule_format]: "wf(r) ==> \<forall>x. <a,x>:r \<longrightarrow> <x,a> \<notin> r"
 by (erule_tac a=a in wf_induct, blast)
 
 (* @{term"[| wf(r);  <a,x> \<in> r;  ~P ==> <x,a> \<in> r |] ==> P"} *)
 lemmas wf_asym = wf_not_sym [THEN swap]
 
 lemma wf_on_not_refl: "[| wf[A](r); a \<in> A |] ==> <a,a> \<notin> r"
 by (erule_tac a=a in wf_on_induct, assumption, blast)
 
-lemma wf_on_not_sym [rule_format]:
-     "[| wf[A](r);  a \<in> A |] ==> \<forall>b\<in>A. <a,b>:r \<longrightarrow> <b,a>\<notin>r"
+lemma wf_on_not_sym:
+     "[| wf[A](r);  a \<in> A |] ==> (\<And>b. b\<in>A \<Longrightarrow> <a,b>:r \<Longrightarrow> <b,a>\<notin>r)"
+apply (atomize (full), intro impI)
 apply (erule_tac a=a in wf_on_induct, assumption, blast)
 done
 
 lemma wf_on_asym:
      "[| wf[A](r);  ~Z ==> <a,b> \<in> r;
          <b,a> \<notin> r ==> Z; ~Z ==> a \<in> A; ~Z ==> b \<in> A |] ==> Z"
 by (blast dest: wf_on_not_sym)
 
 
 (*Needed to prove well_ordI.  Could also reason that wf[A](r) means
   wf(r \<inter> A*A);  thus wf( (r \<inter> A*A)^+ ) and use wf_not_refl *)
 lemma wf_on_chain3:
      "[| wf[A](r); <a,b>:r; <b,c>:r; <c,a>:r; a \<in> A; b \<in> A; c \<in> A |] ==> P"
 apply (subgoal_tac "\<forall>y\<in>A. \<forall>z\<in>A. <a,y>:r \<longrightarrow> <y,z>:r \<longrightarrow> <z,a>:r \<longrightarrow> P",
        blast)
 apply (erule_tac a=a in wf_on_induct, assumption, blast)
 done
 
 
 
 text\<open>transitive closure of a WF relation is WF provided
   \<^term>\<open>A\<close> is downward closed\<close>
 lemma wf_on_trancl:
     "[| wf[A](r);  r-``A \<subseteq> A |] ==> wf[A](r^+)"
 apply (rule wf_onI2)
 apply (frule bspec [THEN mp], assumption+)
 apply (erule_tac a = y in wf_on_induct, assumption)
 apply (blast elim: tranclE, blast)
 done
 
 lemma wf_trancl: "wf(r) ==> wf(r^+)"
 apply (simp add: wf_iff_wf_on_field)
 apply (rule wf_on_subset_A)
  apply (erule wf_on_trancl)
  apply blast
 apply (rule trancl_type [THEN field_rel_subset])
 done
 
 
 text\<open>\<^term>\<open>r-``{a}\<close> is the set of everything under \<^term>\<open>a\<close> in \<^term>\<open>r\<close>\<close>
 
 lemmas underI = vimage_singleton_iff [THEN iffD2]
 lemmas underD = vimage_singleton_iff [THEN iffD1]
 
 
 subsection\<open>The Predicate \<^term>\<open>is_recfun\<close>\<close>
 
 lemma is_recfun_type: "is_recfun(r,a,H,f) ==> f \<in> r-``{a} -> range(f)"
 apply (unfold is_recfun_def)
 apply (erule ssubst)
 apply (rule lamI [THEN rangeI, THEN lam_type], assumption)
 done
 
 lemmas is_recfun_imp_function = is_recfun_type [THEN fun_is_function]
 
 lemma apply_recfun:
     "[| is_recfun(r,a,H,f); <x,a>:r |] ==> f`x = H(x, restrict(f,r-``{x}))"
 apply (unfold is_recfun_def)
   txt\<open>replace f only on the left-hand side\<close>
 apply (erule_tac P = "%x. t(x) = u" for t u in ssubst)
 apply (simp add: underI)
 done
 
 lemma is_recfun_equal [rule_format]:
      "[| wf(r);  trans(r);  is_recfun(r,a,H,f);  is_recfun(r,b,H,g) |]
       ==> <x,a>:r \<longrightarrow> <x,b>:r \<longrightarrow> f`x=g`x"
 apply (frule_tac f = f in is_recfun_type)
 apply (frule_tac f = g in is_recfun_type)
 apply (simp add: is_recfun_def)
 apply (erule_tac a=x in wf_induct)
 apply (intro impI)
 apply (elim ssubst)
 apply (simp (no_asm_simp) add: vimage_singleton_iff restrict_def)
 apply (rule_tac t = "%z. H (x, z)" for x in subst_context)
 apply (subgoal_tac "\<forall>y\<in>r-``{x}. \<forall>z. <y,z>:f \<longleftrightarrow> <y,z>:g")
  apply (blast dest: transD)
 apply (simp add: apply_iff)
 apply (blast dest: transD intro: sym)
 done
 
 lemma is_recfun_cut:
      "[| wf(r);  trans(r);
          is_recfun(r,a,H,f);  is_recfun(r,b,H,g);  <b,a>:r |]
       ==> restrict(f, r-``{b}) = g"
 apply (frule_tac f = f in is_recfun_type)
 apply (rule fun_extension)
   apply (blast dest: transD intro: restrict_type2)
  apply (erule is_recfun_type, simp)
 apply (blast dest: transD intro: is_recfun_equal)
 done
 
 subsection\<open>Recursion: Main Existence Lemma\<close>
 
 lemma is_recfun_functional:
      "[| wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,a,H,g) |]  ==>  f=g"
 by (blast intro: fun_extension is_recfun_type is_recfun_equal)
 
 lemma the_recfun_eq:
     "[| is_recfun(r,a,H,f);  wf(r);  trans(r) |] ==> the_recfun(r,a,H) = f"
 apply (unfold the_recfun_def)
 apply (blast intro: is_recfun_functional)
 done
 
 (*If some f satisfies is_recfun(r,a,H,-) then so does the_recfun(r,a,H) *)
 lemma is_the_recfun:
     "[| is_recfun(r,a,H,f);  wf(r);  trans(r) |]
      ==> is_recfun(r, a, H, the_recfun(r,a,H))"
 by (simp add: the_recfun_eq)
 
 lemma unfold_the_recfun:
      "[| wf(r);  trans(r) |] ==> is_recfun(r, a, H, the_recfun(r,a,H))"
 apply (rule_tac a=a in wf_induct, assumption)
 apply (rename_tac a1)
 apply (rule_tac f = "\<lambda>y\<in>r-``{a1}. wftrec (r,y,H)" in is_the_recfun)
   apply typecheck
 apply (unfold is_recfun_def wftrec_def)
   \<comment> \<open>Applying the substitution: must keep the quantified assumption!\<close>
 apply (rule lam_cong [OF refl])
 apply (drule underD)
 apply (fold is_recfun_def)
 apply (rule_tac t = "%z. H(x, z)" for x in subst_context)
 apply (rule fun_extension)
   apply (blast intro: is_recfun_type)
  apply (rule lam_type [THEN restrict_type2])
   apply blast
  apply (blast dest: transD)
 apply atomize
 apply (frule spec [THEN mp], assumption)
 apply (subgoal_tac "<xa,a1> \<in> r")
  apply (drule_tac x1 = xa in spec [THEN mp], assumption)
 apply (simp add: vimage_singleton_iff
                  apply_recfun is_recfun_cut)
 apply (blast dest: transD)
 done
 
 
 subsection\<open>Unfolding \<^term>\<open>wftrec(r,a,H)\<close>\<close>
 
 lemma the_recfun_cut:
      "[| wf(r);  trans(r);  <b,a>:r |]
       ==> restrict(the_recfun(r,a,H), r-``{b}) = the_recfun(r,b,H)"
 by (blast intro: is_recfun_cut unfold_the_recfun)
 
 (*NOT SUITABLE FOR REWRITING: it is recursive!*)
 lemma wftrec:
     "[| wf(r);  trans(r) |] ==>
           wftrec(r,a,H) = H(a, \<lambda>x\<in>r-``{a}. wftrec(r,x,H))"
 apply (unfold wftrec_def)
 apply (subst unfold_the_recfun [unfolded is_recfun_def])
 apply (simp_all add: vimage_singleton_iff [THEN iff_sym] the_recfun_cut)
 done
 
 
 subsubsection\<open>Removal of the Premise \<^term>\<open>trans(r)\<close>\<close>
 
 (*NOT SUITABLE FOR REWRITING: it is recursive!*)
 lemma wfrec:
     "wf(r) ==> wfrec(r,a,H) = H(a, \<lambda>x\<in>r-``{a}. wfrec(r,x,H))"
 apply (unfold wfrec_def)
 apply (erule wf_trancl [THEN wftrec, THEN ssubst])
  apply (rule trans_trancl)
 apply (rule vimage_pair_mono [THEN restrict_lam_eq, THEN subst_context])
  apply (erule r_into_trancl)
 apply (rule subset_refl)
 done
 
 (*This form avoids giant explosions in proofs.  NOTE USE OF == *)
 lemma def_wfrec:
     "[| !!x. h(x)==wfrec(r,x,H);  wf(r) |] ==>
      h(a) = H(a, \<lambda>x\<in>r-``{a}. h(x))"
 apply simp
 apply (elim wfrec)
 done
 
 lemma wfrec_type:
     "[| wf(r);  a \<in> A;  field(r)<=A;
         !!x u. [| x \<in> A;  u \<in> Pi(r-``{x}, B) |] ==> H(x,u) \<in> B(x)
      |] ==> wfrec(r,a,H) \<in> B(a)"
 apply (rule_tac a = a in wf_induct2, assumption+)
 apply (subst wfrec, assumption)
 apply (simp add: lam_type underD)
 done
 
 
 lemma wfrec_on:
  "[| wf[A](r);  a \<in> A |] ==>
          wfrec[A](r,a,H) = H(a, \<lambda>x\<in>(r-``{a}) \<inter> A. wfrec[A](r,x,H))"
 apply (unfold wf_on_def wfrec_on_def)
 apply (erule wfrec [THEN trans])
 apply (simp add: vimage_Int_square cons_subset_iff)
 done
 
 text\<open>Minimal-element characterization of well-foundedness\<close>
 lemma wf_eq_minimal:
      "wf(r) \<longleftrightarrow> (\<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. <y,z>:r \<longrightarrow> y\<notin>Q))"
 by (unfold wf_def, blast)
 
 end
diff --git a/src/ZF/equalities.thy b/src/ZF/equalities.thy
--- a/src/ZF/equalities.thy
+++ b/src/ZF/equalities.thy
@@ -1,984 +1,984 @@
 (*  Title:      ZF/equalities.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 *)
 
 section\<open>Basic Equalities and Inclusions\<close>
 
 theory equalities imports pair begin
 
 text\<open>These cover union, intersection, converse, domain, range, etc.  Philippe
 de Groote proved many of the inclusions.\<close>
 
 lemma in_mono: "A\<subseteq>B ==> x\<in>A \<longrightarrow> x\<in>B"
 by blast
 
 lemma the_eq_0 [simp]: "(THE x. False) = 0"
 by (blast intro: the_0)
 
 subsection\<open>Bounded Quantifiers\<close>
 text \<open>\medskip
 
   The following are not added to the default simpset because
   (a) they duplicate the body and (b) there are no similar rules for \<open>Int\<close>.\<close>
 
 lemma ball_Un: "(\<forall>x \<in> A\<union>B. P(x)) \<longleftrightarrow> (\<forall>x \<in> A. P(x)) & (\<forall>x \<in> B. P(x))"
   by blast
 
 lemma bex_Un: "(\<exists>x \<in> A\<union>B. P(x)) \<longleftrightarrow> (\<exists>x \<in> A. P(x)) | (\<exists>x \<in> B. P(x))"
   by blast
 
 lemma ball_UN: "(\<forall>z \<in> (\<Union>x\<in>A. B(x)). P(z)) \<longleftrightarrow> (\<forall>x\<in>A. \<forall>z \<in> B(x). P(z))"
   by blast
 
 lemma bex_UN: "(\<exists>z \<in> (\<Union>x\<in>A. B(x)). P(z)) \<longleftrightarrow> (\<exists>x\<in>A. \<exists>z\<in>B(x). P(z))"
   by blast
 
 subsection\<open>Converse of a Relation\<close>
 
 lemma converse_iff [simp]: "<a,b>\<in> converse(r) \<longleftrightarrow> <b,a>\<in>r"
 by (unfold converse_def, blast)
 
 lemma converseI [intro!]: "<a,b>\<in>r ==> <b,a>\<in>converse(r)"
 by (unfold converse_def, blast)
 
 lemma converseD: "<a,b> \<in> converse(r) ==> <b,a> \<in> r"
 by (unfold converse_def, blast)
 
 lemma converseE [elim!]:
     "[| yx \<in> converse(r);
         !!x y. [| yx=<y,x>;  <x,y>\<in>r |] ==> P |]
      ==> P"
 by (unfold converse_def, blast)
 
 lemma converse_converse: "r\<subseteq>Sigma(A,B) ==> converse(converse(r)) = r"
 by blast
 
 lemma converse_type: "r\<subseteq>A*B ==> converse(r)\<subseteq>B*A"
 by blast
 
 lemma converse_prod [simp]: "converse(A*B) = B*A"
 by blast
 
 lemma converse_empty [simp]: "converse(0) = 0"
 by blast
 
 lemma converse_subset_iff:
      "A \<subseteq> Sigma(X,Y) ==> converse(A) \<subseteq> converse(B) \<longleftrightarrow> A \<subseteq> B"
 by blast
 
 
 subsection\<open>Finite Set Constructions Using \<^term>\<open>cons\<close>\<close>
 
 lemma cons_subsetI: "[| a\<in>C; B\<subseteq>C |] ==> cons(a,B) \<subseteq> C"
 by blast
 
 lemma subset_consI: "B \<subseteq> cons(a,B)"
 by blast
 
 lemma cons_subset_iff [iff]: "cons(a,B)\<subseteq>C \<longleftrightarrow> a\<in>C & B\<subseteq>C"
 by blast
 
 (*A safe special case of subset elimination, adding no new variables
   [| cons(a,B) \<subseteq> C; [| a \<in> C; B \<subseteq> C |] ==> R |] ==> R *)
 lemmas cons_subsetE = cons_subset_iff [THEN iffD1, THEN conjE]
 
 lemma subset_empty_iff: "A\<subseteq>0 \<longleftrightarrow> A=0"
 by blast
 
 lemma subset_cons_iff: "C\<subseteq>cons(a,B) \<longleftrightarrow> C\<subseteq>B | (a\<in>C & C-{a} \<subseteq> B)"
 by blast
 
 (* cons_def refers to Upair; reversing the equality LOOPS in rewriting!*)
 lemma cons_eq: "{a} \<union> B = cons(a,B)"
 by blast
 
 lemma cons_commute: "cons(a, cons(b, C)) = cons(b, cons(a, C))"
 by blast
 
 lemma cons_absorb: "a: B ==> cons(a,B) = B"
 by blast
 
 lemma cons_Diff: "a: B ==> cons(a, B-{a}) = B"
 by blast
 
 lemma Diff_cons_eq: "cons(a,B) - C = (if a\<in>C then B-C else cons(a,B-C))"
 by auto
 
-lemma equal_singleton [rule_format]: "[| a: C;  \<forall>y\<in>C. y=b |] ==> C = {b}"
+lemma equal_singleton: "[| a: C;  \<And>y. y \<in>C \<Longrightarrow> y=b |] ==> C = {b}"
 by blast
 
 lemma [simp]: "cons(a,cons(a,B)) = cons(a,B)"
 by blast
 
 (** singletons **)
 
 lemma singleton_subsetI: "a\<in>C ==> {a} \<subseteq> C"
 by blast
 
 lemma singleton_subsetD: "{a} \<subseteq> C  ==>  a\<in>C"
 by blast
 
 
 (** succ **)
 
 lemma subset_succI: "i \<subseteq> succ(i)"
 by blast
 
 (*But if j is an ordinal or is transitive, then @{term"i\<in>j"} implies @{term"i\<subseteq>j"}!
   See @{text"Ord_succ_subsetI}*)
 lemma succ_subsetI: "[| i\<in>j;  i\<subseteq>j |] ==> succ(i)\<subseteq>j"
 by (unfold succ_def, blast)
 
 lemma succ_subsetE:
     "[| succ(i) \<subseteq> j;  [| i\<in>j;  i\<subseteq>j |] ==> P |] ==> P"
 by (unfold succ_def, blast)
 
 lemma succ_subset_iff: "succ(a) \<subseteq> B \<longleftrightarrow> (a \<subseteq> B & a \<in> B)"
 by (unfold succ_def, blast)
 
 
 subsection\<open>Binary Intersection\<close>
 
 (** Intersection is the greatest lower bound of two sets **)
 
 lemma Int_subset_iff: "C \<subseteq> A \<inter> B \<longleftrightarrow> C \<subseteq> A & C \<subseteq> B"
 by blast
 
 lemma Int_lower1: "A \<inter> B \<subseteq> A"
 by blast
 
 lemma Int_lower2: "A \<inter> B \<subseteq> B"
 by blast
 
 lemma Int_greatest: "[| C\<subseteq>A;  C\<subseteq>B |] ==> C \<subseteq> A \<inter> B"
 by blast
 
 lemma Int_cons: "cons(a,B) \<inter> C \<subseteq> cons(a, B \<inter> C)"
 by blast
 
 lemma Int_absorb [simp]: "A \<inter> A = A"
 by blast
 
 lemma Int_left_absorb: "A \<inter> (A \<inter> B) = A \<inter> B"
 by blast
 
 lemma Int_commute: "A \<inter> B = B \<inter> A"
 by blast
 
 lemma Int_left_commute: "A \<inter> (B \<inter> C) = B \<inter> (A \<inter> C)"
 by blast
 
 lemma Int_assoc: "(A \<inter> B) \<inter> C  =  A \<inter> (B \<inter> C)"
 by blast
 
 (*Intersection is an AC-operator*)
 lemmas Int_ac= Int_assoc Int_left_absorb Int_commute Int_left_commute
 
 lemma Int_absorb1: "B \<subseteq> A ==> A \<inter> B = B"
   by blast
 
 lemma Int_absorb2: "A \<subseteq> B ==> A \<inter> B = A"
   by blast
 
 lemma Int_Un_distrib: "A \<inter> (B \<union> C) = (A \<inter> B) \<union> (A \<inter> C)"
 by blast
 
 lemma Int_Un_distrib2: "(B \<union> C) \<inter> A = (B \<inter> A) \<union> (C \<inter> A)"
 by blast
 
 lemma subset_Int_iff: "A\<subseteq>B \<longleftrightarrow> A \<inter> B = A"
 by (blast elim!: equalityE)
 
 lemma subset_Int_iff2: "A\<subseteq>B \<longleftrightarrow> B \<inter> A = A"
 by (blast elim!: equalityE)
 
 lemma Int_Diff_eq: "C\<subseteq>A ==> (A-B) \<inter> C = C-B"
 by blast
 
 lemma Int_cons_left:
      "cons(a,A) \<inter> B = (if a \<in> B then cons(a, A \<inter> B) else A \<inter> B)"
 by auto
 
 lemma Int_cons_right:
      "A \<inter> cons(a, B) = (if a \<in> A then cons(a, A \<inter> B) else A \<inter> B)"
 by auto
 
 lemma cons_Int_distrib: "cons(x, A \<inter> B) = cons(x, A) \<inter> cons(x, B)"
 by auto
 
 subsection\<open>Binary Union\<close>
 
 (** Union is the least upper bound of two sets *)
 
 lemma Un_subset_iff: "A \<union> B \<subseteq> C \<longleftrightarrow> A \<subseteq> C & B \<subseteq> C"
 by blast
 
 lemma Un_upper1: "A \<subseteq> A \<union> B"
 by blast
 
 lemma Un_upper2: "B \<subseteq> A \<union> B"
 by blast
 
 lemma Un_least: "[| A\<subseteq>C;  B\<subseteq>C |] ==> A \<union> B \<subseteq> C"
 by blast
 
 lemma Un_cons: "cons(a,B) \<union> C = cons(a, B \<union> C)"
 by blast
 
 lemma Un_absorb [simp]: "A \<union> A = A"
 by blast
 
 lemma Un_left_absorb: "A \<union> (A \<union> B) = A \<union> B"
 by blast
 
 lemma Un_commute: "A \<union> B = B \<union> A"
 by blast
 
 lemma Un_left_commute: "A \<union> (B \<union> C) = B \<union> (A \<union> C)"
 by blast
 
 lemma Un_assoc: "(A \<union> B) \<union> C  =  A \<union> (B \<union> C)"
 by blast
 
 (*Union is an AC-operator*)
 lemmas Un_ac = Un_assoc Un_left_absorb Un_commute Un_left_commute
 
 lemma Un_absorb1: "A \<subseteq> B ==> A \<union> B = B"
   by blast
 
 lemma Un_absorb2: "B \<subseteq> A ==> A \<union> B = A"
   by blast
 
 lemma Un_Int_distrib: "(A \<inter> B) \<union> C  =  (A \<union> C) \<inter> (B \<union> C)"
 by blast
 
 lemma subset_Un_iff: "A\<subseteq>B \<longleftrightarrow> A \<union> B = B"
 by (blast elim!: equalityE)
 
 lemma subset_Un_iff2: "A\<subseteq>B \<longleftrightarrow> B \<union> A = B"
 by (blast elim!: equalityE)
 
 lemma Un_empty [iff]: "(A \<union> B = 0) \<longleftrightarrow> (A = 0 & B = 0)"
 by blast
 
 lemma Un_eq_Union: "A \<union> B = \<Union>({A, B})"
 by blast
 
 subsection\<open>Set Difference\<close>
 
 lemma Diff_subset: "A-B \<subseteq> A"
 by blast
 
 lemma Diff_contains: "[| C\<subseteq>A;  C \<inter> B = 0 |] ==> C \<subseteq> A-B"
 by blast
 
 lemma subset_Diff_cons_iff: "B \<subseteq> A - cons(c,C)  \<longleftrightarrow>  B\<subseteq>A-C & c \<notin> B"
 by blast
 
 lemma Diff_cancel: "A - A = 0"
 by blast
 
 lemma Diff_triv: "A  \<inter> B = 0 ==> A - B = A"
 by blast
 
 lemma empty_Diff [simp]: "0 - A = 0"
 by blast
 
 lemma Diff_0 [simp]: "A - 0 = A"
 by blast
 
 lemma Diff_eq_0_iff: "A - B = 0 \<longleftrightarrow> A \<subseteq> B"
 by (blast elim: equalityE)
 
 (*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*)
 lemma Diff_cons: "A - cons(a,B) = A - B - {a}"
 by blast
 
 (*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*)
 lemma Diff_cons2: "A - cons(a,B) = A - {a} - B"
 by blast
 
 lemma Diff_disjoint: "A \<inter> (B-A) = 0"
 by blast
 
 lemma Diff_partition: "A\<subseteq>B ==> A \<union> (B-A) = B"
 by blast
 
 lemma subset_Un_Diff: "A \<subseteq> B \<union> (A - B)"
 by blast
 
 lemma double_complement: "[| A\<subseteq>B; B\<subseteq>C |] ==> B-(C-A) = A"
 by blast
 
 lemma double_complement_Un: "(A \<union> B) - (B-A) = A"
 by blast
 
 lemma Un_Int_crazy:
  "(A \<inter> B) \<union> (B \<inter> C) \<union> (C \<inter> A) = (A \<union> B) \<inter> (B \<union> C) \<inter> (C \<union> A)"
 apply blast
 done
 
 lemma Diff_Un: "A - (B \<union> C) = (A-B) \<inter> (A-C)"
 by blast
 
 lemma Diff_Int: "A - (B \<inter> C) = (A-B) \<union> (A-C)"
 by blast
 
 lemma Un_Diff: "(A \<union> B) - C = (A - C) \<union> (B - C)"
 by blast
 
 lemma Int_Diff: "(A \<inter> B) - C = A \<inter> (B - C)"
 by blast
 
 lemma Diff_Int_distrib: "C \<inter> (A-B) = (C \<inter> A) - (C \<inter> B)"
 by blast
 
 lemma Diff_Int_distrib2: "(A-B) \<inter> C = (A \<inter> C) - (B \<inter> C)"
 by blast
 
 (*Halmos, Naive Set Theory, page 16.*)
 lemma Un_Int_assoc_iff: "(A \<inter> B) \<union> C = A \<inter> (B \<union> C)  \<longleftrightarrow>  C\<subseteq>A"
 by (blast elim!: equalityE)
 
 
 subsection\<open>Big Union and Intersection\<close>
 
 (** Big Union is the least upper bound of a set  **)
 
 lemma Union_subset_iff: "\<Union>(A) \<subseteq> C \<longleftrightarrow> (\<forall>x\<in>A. x \<subseteq> C)"
 by blast
 
 lemma Union_upper: "B\<in>A ==> B \<subseteq> \<Union>(A)"
 by blast
 
 lemma Union_least: "[| !!x. x\<in>A ==> x\<subseteq>C |] ==> \<Union>(A) \<subseteq> C"
 by blast
 
 lemma Union_cons [simp]: "\<Union>(cons(a,B)) = a \<union> \<Union>(B)"
 by blast
 
 lemma Union_Un_distrib: "\<Union>(A \<union> B) = \<Union>(A) \<union> \<Union>(B)"
 by blast
 
 lemma Union_Int_subset: "\<Union>(A \<inter> B) \<subseteq> \<Union>(A) \<inter> \<Union>(B)"
 by blast
 
 lemma Union_disjoint: "\<Union>(C) \<inter> A = 0 \<longleftrightarrow> (\<forall>B\<in>C. B \<inter> A = 0)"
 by (blast elim!: equalityE)
 
 lemma Union_empty_iff: "\<Union>(A) = 0 \<longleftrightarrow> (\<forall>B\<in>A. B=0)"
 by blast
 
 lemma Int_Union2: "\<Union>(B) \<inter> A = (\<Union>C\<in>B. C \<inter> A)"
 by blast
 
 (** Big Intersection is the greatest lower bound of a nonempty set **)
 
 lemma Inter_subset_iff: "A\<noteq>0  ==>  C \<subseteq> \<Inter>(A) \<longleftrightarrow> (\<forall>x\<in>A. C \<subseteq> x)"
 by blast
 
 lemma Inter_lower: "B\<in>A ==> \<Inter>(A) \<subseteq> B"
 by blast
 
 lemma Inter_greatest: "[| A\<noteq>0;  !!x. x\<in>A ==> C\<subseteq>x |] ==> C \<subseteq> \<Inter>(A)"
 by blast
 
 (** Intersection of a family of sets  **)
 
 lemma INT_lower: "x\<in>A ==> (\<Inter>x\<in>A. B(x)) \<subseteq> B(x)"
 by blast
 
 lemma INT_greatest: "[| A\<noteq>0;  !!x. x\<in>A ==> C\<subseteq>B(x) |] ==> C \<subseteq> (\<Inter>x\<in>A. B(x))"
 by force
 
 lemma Inter_0 [simp]: "\<Inter>(0) = 0"
 by (unfold Inter_def, blast)
 
 lemma Inter_Un_subset:
      "[| z\<in>A; z\<in>B |] ==> \<Inter>(A) \<union> \<Inter>(B) \<subseteq> \<Inter>(A \<inter> B)"
 by blast
 
 (* A good challenge: Inter is ill-behaved on the empty set *)
 lemma Inter_Un_distrib:
      "[| A\<noteq>0;  B\<noteq>0 |] ==> \<Inter>(A \<union> B) = \<Inter>(A) \<inter> \<Inter>(B)"
 by blast
 
 lemma Union_singleton: "\<Union>({b}) = b"
 by blast
 
 lemma Inter_singleton: "\<Inter>({b}) = b"
 by blast
 
 lemma Inter_cons [simp]:
      "\<Inter>(cons(a,B)) = (if B=0 then a else a \<inter> \<Inter>(B))"
 by force
 
 subsection\<open>Unions and Intersections of Families\<close>
 
 lemma subset_UN_iff_eq: "A \<subseteq> (\<Union>i\<in>I. B(i)) \<longleftrightarrow> A = (\<Union>i\<in>I. A \<inter> B(i))"
 by (blast elim!: equalityE)
 
 lemma UN_subset_iff: "(\<Union>x\<in>A. B(x)) \<subseteq> C \<longleftrightarrow> (\<forall>x\<in>A. B(x) \<subseteq> C)"
 by blast
 
 lemma UN_upper: "x\<in>A ==> B(x) \<subseteq> (\<Union>x\<in>A. B(x))"
 by (erule RepFunI [THEN Union_upper])
 
 lemma UN_least: "[| !!x. x\<in>A ==> B(x)\<subseteq>C |] ==> (\<Union>x\<in>A. B(x)) \<subseteq> C"
 by blast
 
 lemma Union_eq_UN: "\<Union>(A) = (\<Union>x\<in>A. x)"
 by blast
 
 lemma Inter_eq_INT: "\<Inter>(A) = (\<Inter>x\<in>A. x)"
 by (unfold Inter_def, blast)
 
 lemma UN_0 [simp]: "(\<Union>i\<in>0. A(i)) = 0"
 by blast
 
 lemma UN_singleton: "(\<Union>x\<in>A. {x}) = A"
 by blast
 
 lemma UN_Un: "(\<Union>i\<in> A \<union> B. C(i)) = (\<Union>i\<in> A. C(i)) \<union> (\<Union>i\<in>B. C(i))"
 by blast
 
 lemma INT_Un: "(\<Inter>i\<in>I \<union> J. A(i)) =
                (if I=0 then \<Inter>j\<in>J. A(j)
                        else if J=0 then \<Inter>i\<in>I. A(i)
                        else ((\<Inter>i\<in>I. A(i)) \<inter>  (\<Inter>j\<in>J. A(j))))"
 by (simp, blast intro!: equalityI)
 
 lemma UN_UN_flatten: "(\<Union>x \<in> (\<Union>y\<in>A. B(y)). C(x)) = (\<Union>y\<in>A. \<Union>x\<in> B(y). C(x))"
 by blast
 
 (*Halmos, Naive Set Theory, page 35.*)
 lemma Int_UN_distrib: "B \<inter> (\<Union>i\<in>I. A(i)) = (\<Union>i\<in>I. B \<inter> A(i))"
 by blast
 
 lemma Un_INT_distrib: "I\<noteq>0 ==> B \<union> (\<Inter>i\<in>I. A(i)) = (\<Inter>i\<in>I. B \<union> A(i))"
 by auto
 
 lemma Int_UN_distrib2:
      "(\<Union>i\<in>I. A(i)) \<inter> (\<Union>j\<in>J. B(j)) = (\<Union>i\<in>I. \<Union>j\<in>J. A(i) \<inter> B(j))"
 by blast
 
 lemma Un_INT_distrib2: "[| I\<noteq>0;  J\<noteq>0 |] ==>
       (\<Inter>i\<in>I. A(i)) \<union> (\<Inter>j\<in>J. B(j)) = (\<Inter>i\<in>I. \<Inter>j\<in>J. A(i) \<union> B(j))"
 by auto
 
 lemma UN_constant [simp]: "(\<Union>y\<in>A. c) = (if A=0 then 0 else c)"
 by force
 
 lemma INT_constant [simp]: "(\<Inter>y\<in>A. c) = (if A=0 then 0 else c)"
 by force
 
 lemma UN_RepFun [simp]: "(\<Union>y\<in> RepFun(A,f). B(y)) = (\<Union>x\<in>A. B(f(x)))"
 by blast
 
 lemma INT_RepFun [simp]: "(\<Inter>x\<in>RepFun(A,f). B(x))    = (\<Inter>a\<in>A. B(f(a)))"
 by (auto simp add: Inter_def)
 
 lemma INT_Union_eq:
      "0 \<notin> A ==> (\<Inter>x\<in> \<Union>(A). B(x)) = (\<Inter>y\<in>A. \<Inter>x\<in>y. B(x))"
 apply (subgoal_tac "\<forall>x\<in>A. x\<noteq>0")
  prefer 2 apply blast
 apply (force simp add: Inter_def ball_conj_distrib)
 done
 
 lemma INT_UN_eq:
      "(\<forall>x\<in>A. B(x) \<noteq> 0)
       ==> (\<Inter>z\<in> (\<Union>x\<in>A. B(x)). C(z)) = (\<Inter>x\<in>A. \<Inter>z\<in> B(x). C(z))"
 apply (subst INT_Union_eq, blast)
 apply (simp add: Inter_def)
 done
 
 
 (** Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5:
     Union of a family of unions **)
 
 lemma UN_Un_distrib:
      "(\<Union>i\<in>I. A(i) \<union> B(i)) = (\<Union>i\<in>I. A(i))  \<union>  (\<Union>i\<in>I. B(i))"
 by blast
 
 lemma INT_Int_distrib:
      "I\<noteq>0 ==> (\<Inter>i\<in>I. A(i) \<inter> B(i)) = (\<Inter>i\<in>I. A(i)) \<inter> (\<Inter>i\<in>I. B(i))"
 by (blast elim!: not_emptyE)
 
 lemma UN_Int_subset:
      "(\<Union>z\<in>I \<inter> J. A(z)) \<subseteq> (\<Union>z\<in>I. A(z)) \<inter> (\<Union>z\<in>J. A(z))"
 by blast
 
 (** Devlin, page 12, exercise 5: Complements **)
 
 lemma Diff_UN: "I\<noteq>0 ==> B - (\<Union>i\<in>I. A(i)) = (\<Inter>i\<in>I. B - A(i))"
 by (blast elim!: not_emptyE)
 
 lemma Diff_INT: "I\<noteq>0 ==> B - (\<Inter>i\<in>I. A(i)) = (\<Union>i\<in>I. B - A(i))"
 by (blast elim!: not_emptyE)
 
 
 (** Unions and Intersections with General Sum **)
 
 (*Not suitable for rewriting: LOOPS!*)
 lemma Sigma_cons1: "Sigma(cons(a,B), C) = ({a}*C(a)) \<union> Sigma(B,C)"
 by blast
 
 (*Not suitable for rewriting: LOOPS!*)
 lemma Sigma_cons2: "A * cons(b,B) = A*{b} \<union> A*B"
 by blast
 
 lemma Sigma_succ1: "Sigma(succ(A), B) = ({A}*B(A)) \<union> Sigma(A,B)"
 by blast
 
 lemma Sigma_succ2: "A * succ(B) = A*{B} \<union> A*B"
 by blast
 
 lemma SUM_UN_distrib1:
      "(\<Sum>x \<in> (\<Union>y\<in>A. C(y)). B(x)) = (\<Union>y\<in>A. \<Sum>x\<in>C(y). B(x))"
 by blast
 
 lemma SUM_UN_distrib2:
      "(\<Sum>i\<in>I. \<Union>j\<in>J. C(i,j)) = (\<Union>j\<in>J. \<Sum>i\<in>I. C(i,j))"
 by blast
 
 lemma SUM_Un_distrib1:
      "(\<Sum>i\<in>I \<union> J. C(i)) = (\<Sum>i\<in>I. C(i)) \<union> (\<Sum>j\<in>J. C(j))"
 by blast
 
 lemma SUM_Un_distrib2:
      "(\<Sum>i\<in>I. A(i) \<union> B(i)) = (\<Sum>i\<in>I. A(i)) \<union> (\<Sum>i\<in>I. B(i))"
 by blast
 
 (*First-order version of the above, for rewriting*)
 lemma prod_Un_distrib2: "I * (A \<union> B) = I*A \<union> I*B"
 by (rule SUM_Un_distrib2)
 
 lemma SUM_Int_distrib1:
      "(\<Sum>i\<in>I \<inter> J. C(i)) = (\<Sum>i\<in>I. C(i)) \<inter> (\<Sum>j\<in>J. C(j))"
 by blast
 
 lemma SUM_Int_distrib2:
      "(\<Sum>i\<in>I. A(i) \<inter> B(i)) = (\<Sum>i\<in>I. A(i)) \<inter> (\<Sum>i\<in>I. B(i))"
 by blast
 
 (*First-order version of the above, for rewriting*)
 lemma prod_Int_distrib2: "I * (A \<inter> B) = I*A \<inter> I*B"
 by (rule SUM_Int_distrib2)
 
 (*Cf Aczel, Non-Well-Founded Sets, page 115*)
 lemma SUM_eq_UN: "(\<Sum>i\<in>I. A(i)) = (\<Union>i\<in>I. {i} * A(i))"
 by blast
 
 lemma times_subset_iff:
      "(A'*B' \<subseteq> A*B) \<longleftrightarrow> (A' = 0 | B' = 0 | (A'\<subseteq>A) & (B'\<subseteq>B))"
 by blast
 
 lemma Int_Sigma_eq:
      "(\<Sum>x \<in> A'. B'(x)) \<inter> (\<Sum>x \<in> A. B(x)) = (\<Sum>x \<in> A' \<inter> A. B'(x) \<inter> B(x))"
 by blast
 
 (** Domain **)
 
 lemma domain_iff: "a: domain(r) \<longleftrightarrow> (\<exists>y. <a,y>\<in> r)"
 by (unfold domain_def, blast)
 
 lemma domainI [intro]: "<a,b>\<in> r ==> a: domain(r)"
 by (unfold domain_def, blast)
 
 lemma domainE [elim!]:
     "[| a \<in> domain(r);  !!y. <a,y>\<in> r ==> P |] ==> P"
 by (unfold domain_def, blast)
 
 lemma domain_subset: "domain(Sigma(A,B)) \<subseteq> A"
 by blast
 
 lemma domain_of_prod: "b\<in>B ==> domain(A*B) = A"
 by blast
 
 lemma domain_0 [simp]: "domain(0) = 0"
 by blast
 
 lemma domain_cons [simp]: "domain(cons(<a,b>,r)) = cons(a, domain(r))"
 by blast
 
 lemma domain_Un_eq [simp]: "domain(A \<union> B) = domain(A) \<union> domain(B)"
 by blast
 
 lemma domain_Int_subset: "domain(A \<inter> B) \<subseteq> domain(A) \<inter> domain(B)"
 by blast
 
 lemma domain_Diff_subset: "domain(A) - domain(B) \<subseteq> domain(A - B)"
 by blast
 
 lemma domain_UN: "domain(\<Union>x\<in>A. B(x)) = (\<Union>x\<in>A. domain(B(x)))"
 by blast
 
 lemma domain_Union: "domain(\<Union>(A)) = (\<Union>x\<in>A. domain(x))"
 by blast
 
 
 (** Range **)
 
 lemma rangeI [intro]: "<a,b>\<in> r ==> b \<in> range(r)"
 apply (unfold range_def)
 apply (erule converseI [THEN domainI])
 done
 
 lemma rangeE [elim!]: "[| b \<in> range(r);  !!x. <x,b>\<in> r ==> P |] ==> P"
 by (unfold range_def, blast)
 
 lemma range_subset: "range(A*B) \<subseteq> B"
 apply (unfold range_def)
 apply (subst converse_prod)
 apply (rule domain_subset)
 done
 
 lemma range_of_prod: "a\<in>A ==> range(A*B) = B"
 by blast
 
 lemma range_0 [simp]: "range(0) = 0"
 by blast
 
 lemma range_cons [simp]: "range(cons(<a,b>,r)) = cons(b, range(r))"
 by blast
 
 lemma range_Un_eq [simp]: "range(A \<union> B) = range(A) \<union> range(B)"
 by blast
 
 lemma range_Int_subset: "range(A \<inter> B) \<subseteq> range(A) \<inter> range(B)"
 by blast
 
 lemma range_Diff_subset: "range(A) - range(B) \<subseteq> range(A - B)"
 by blast
 
 lemma domain_converse [simp]: "domain(converse(r)) = range(r)"
 by blast
 
 lemma range_converse [simp]: "range(converse(r)) = domain(r)"
 by blast
 
 
 (** Field **)
 
 lemma fieldI1: "<a,b>\<in> r ==> a \<in> field(r)"
 by (unfold field_def, blast)
 
 lemma fieldI2: "<a,b>\<in> r ==> b \<in> field(r)"
 by (unfold field_def, blast)
 
 lemma fieldCI [intro]:
     "(~ <c,a>\<in>r ==> <a,b>\<in> r) ==> a \<in> field(r)"
 apply (unfold field_def, blast)
 done
 
 lemma fieldE [elim!]:
      "[| a \<in> field(r);
          !!x. <a,x>\<in> r ==> P;
          !!x. <x,a>\<in> r ==> P        |] ==> P"
 by (unfold field_def, blast)
 
 lemma field_subset: "field(A*B) \<subseteq> A \<union> B"
 by blast
 
 lemma domain_subset_field: "domain(r) \<subseteq> field(r)"
 apply (unfold field_def)
 apply (rule Un_upper1)
 done
 
 lemma range_subset_field: "range(r) \<subseteq> field(r)"
 apply (unfold field_def)
 apply (rule Un_upper2)
 done
 
 lemma domain_times_range: "r \<subseteq> Sigma(A,B) ==> r \<subseteq> domain(r)*range(r)"
 by blast
 
 lemma field_times_field: "r \<subseteq> Sigma(A,B) ==> r \<subseteq> field(r)*field(r)"
 by blast
 
 lemma relation_field_times_field: "relation(r) ==> r \<subseteq> field(r)*field(r)"
 by (simp add: relation_def, blast)
 
 lemma field_of_prod: "field(A*A) = A"
 by blast
 
 lemma field_0 [simp]: "field(0) = 0"
 by blast
 
 lemma field_cons [simp]: "field(cons(<a,b>,r)) = cons(a, cons(b, field(r)))"
 by blast
 
 lemma field_Un_eq [simp]: "field(A \<union> B) = field(A) \<union> field(B)"
 by blast
 
 lemma field_Int_subset: "field(A \<inter> B) \<subseteq> field(A) \<inter> field(B)"
 by blast
 
 lemma field_Diff_subset: "field(A) - field(B) \<subseteq> field(A - B)"
 by blast
 
 lemma field_converse [simp]: "field(converse(r)) = field(r)"
 by blast
 
 (** The Union of a set of relations is a relation -- Lemma for fun_Union **)
 lemma rel_Union: "(\<forall>x\<in>S. \<exists>A B. x \<subseteq> A*B) ==>
                   \<Union>(S) \<subseteq> domain(\<Union>(S)) * range(\<Union>(S))"
 by blast
 
 (** The Union of 2 relations is a relation (Lemma for fun_Un)  **)
 lemma rel_Un: "[| r \<subseteq> A*B;  s \<subseteq> C*D |] ==> (r \<union> s) \<subseteq> (A \<union> C) * (B \<union> D)"
 by blast
 
 lemma domain_Diff_eq: "[| <a,c> \<in> r; c\<noteq>b |] ==> domain(r-{<a,b>}) = domain(r)"
 by blast
 
 lemma range_Diff_eq: "[| <c,b> \<in> r; c\<noteq>a |] ==> range(r-{<a,b>}) = range(r)"
 by blast
 
 
 subsection\<open>Image of a Set under a Function or Relation\<close>
 
 lemma image_iff: "b \<in> r``A \<longleftrightarrow> (\<exists>x\<in>A. <x,b>\<in>r)"
 by (unfold image_def, blast)
 
 lemma image_singleton_iff: "b \<in> r``{a} \<longleftrightarrow> <a,b>\<in>r"
 by (rule image_iff [THEN iff_trans], blast)
 
 lemma imageI [intro]: "[| <a,b>\<in> r;  a\<in>A |] ==> b \<in> r``A"
 by (unfold image_def, blast)
 
 lemma imageE [elim!]:
     "[| b: r``A;  !!x.[| <x,b>\<in> r;  x\<in>A |] ==> P |] ==> P"
 by (unfold image_def, blast)
 
 lemma image_subset: "r \<subseteq> A*B ==> r``C \<subseteq> B"
 by blast
 
 lemma image_0 [simp]: "r``0 = 0"
 by blast
 
 lemma image_Un [simp]: "r``(A \<union> B) = (r``A) \<union> (r``B)"
 by blast
 
 lemma image_UN: "r `` (\<Union>x\<in>A. B(x)) = (\<Union>x\<in>A. r `` B(x))"
 by blast
 
 lemma Collect_image_eq:
      "{z \<in> Sigma(A,B). P(z)} `` C = (\<Union>x \<in> A. {y \<in> B(x). x \<in> C & P(<x,y>)})"
 by blast
 
 lemma image_Int_subset: "r``(A \<inter> B) \<subseteq> (r``A) \<inter> (r``B)"
 by blast
 
 lemma image_Int_square_subset: "(r \<inter> A*A)``B \<subseteq> (r``B) \<inter> A"
 by blast
 
 lemma image_Int_square: "B\<subseteq>A ==> (r \<inter> A*A)``B = (r``B) \<inter> A"
 by blast
 
 
 (*Image laws for special relations*)
 lemma image_0_left [simp]: "0``A = 0"
 by blast
 
 lemma image_Un_left: "(r \<union> s)``A = (r``A) \<union> (s``A)"
 by blast
 
 lemma image_Int_subset_left: "(r \<inter> s)``A \<subseteq> (r``A) \<inter> (s``A)"
 by blast
 
 
 subsection\<open>Inverse Image of a Set under a Function or Relation\<close>
 
 lemma vimage_iff:
     "a \<in> r-``B \<longleftrightarrow> (\<exists>y\<in>B. <a,y>\<in>r)"
 by (unfold vimage_def image_def converse_def, blast)
 
 lemma vimage_singleton_iff: "a \<in> r-``{b} \<longleftrightarrow> <a,b>\<in>r"
 by (rule vimage_iff [THEN iff_trans], blast)
 
 lemma vimageI [intro]: "[| <a,b>\<in> r;  b\<in>B |] ==> a \<in> r-``B"
 by (unfold vimage_def, blast)
 
 lemma vimageE [elim!]:
     "[| a: r-``B;  !!x.[| <a,x>\<in> r;  x\<in>B |] ==> P |] ==> P"
 apply (unfold vimage_def, blast)
 done
 
 lemma vimage_subset: "r \<subseteq> A*B ==> r-``C \<subseteq> A"
 apply (unfold vimage_def)
 apply (erule converse_type [THEN image_subset])
 done
 
 lemma vimage_0 [simp]: "r-``0 = 0"
 by blast
 
 lemma vimage_Un [simp]: "r-``(A \<union> B) = (r-``A) \<union> (r-``B)"
 by blast
 
 lemma vimage_Int_subset: "r-``(A \<inter> B) \<subseteq> (r-``A) \<inter> (r-``B)"
 by blast
 
 (*NOT suitable for rewriting*)
 lemma vimage_eq_UN: "f -``B = (\<Union>y\<in>B. f-``{y})"
 by blast
 
 lemma function_vimage_Int:
      "function(f) ==> f-``(A \<inter> B) = (f-``A)  \<inter>  (f-``B)"
 by (unfold function_def, blast)
 
 lemma function_vimage_Diff: "function(f) ==> f-``(A-B) = (f-``A) - (f-``B)"
 by (unfold function_def, blast)
 
 lemma function_image_vimage: "function(f) ==> f `` (f-`` A) \<subseteq> A"
 by (unfold function_def, blast)
 
 lemma vimage_Int_square_subset: "(r \<inter> A*A)-``B \<subseteq> (r-``B) \<inter> A"
 by blast
 
 lemma vimage_Int_square: "B\<subseteq>A ==> (r \<inter> A*A)-``B = (r-``B) \<inter> A"
 by blast
 
 
 
 (*Invese image laws for special relations*)
 lemma vimage_0_left [simp]: "0-``A = 0"
 by blast
 
 lemma vimage_Un_left: "(r \<union> s)-``A = (r-``A) \<union> (s-``A)"
 by blast
 
 lemma vimage_Int_subset_left: "(r \<inter> s)-``A \<subseteq> (r-``A) \<inter> (s-``A)"
 by blast
 
 
 (** Converse **)
 
 lemma converse_Un [simp]: "converse(A \<union> B) = converse(A) \<union> converse(B)"
 by blast
 
 lemma converse_Int [simp]: "converse(A \<inter> B) = converse(A) \<inter> converse(B)"
 by blast
 
 lemma converse_Diff [simp]: "converse(A - B) = converse(A) - converse(B)"
 by blast
 
 lemma converse_UN [simp]: "converse(\<Union>x\<in>A. B(x)) = (\<Union>x\<in>A. converse(B(x)))"
 by blast
 
 (*Unfolding Inter avoids using excluded middle on A=0*)
 lemma converse_INT [simp]:
      "converse(\<Inter>x\<in>A. B(x)) = (\<Inter>x\<in>A. converse(B(x)))"
 apply (unfold Inter_def, blast)
 done
 
 
 subsection\<open>Powerset Operator\<close>
 
 lemma Pow_0 [simp]: "Pow(0) = {0}"
 by blast
 
 lemma Pow_insert: "Pow (cons(a,A)) = Pow(A) \<union> {cons(a,X) . X: Pow(A)}"
 apply (rule equalityI, safe)
 apply (erule swap)
 apply (rule_tac a = "x-{a}" in RepFun_eqI, auto)
 done
 
 lemma Un_Pow_subset: "Pow(A) \<union> Pow(B) \<subseteq> Pow(A \<union> B)"
 by blast
 
 lemma UN_Pow_subset: "(\<Union>x\<in>A. Pow(B(x))) \<subseteq> Pow(\<Union>x\<in>A. B(x))"
 by blast
 
 lemma subset_Pow_Union: "A \<subseteq> Pow(\<Union>(A))"
 by blast
 
 lemma Union_Pow_eq [simp]: "\<Union>(Pow(A)) = A"
 by blast
 
 lemma Union_Pow_iff: "\<Union>(A) \<in> Pow(B) \<longleftrightarrow> A \<in> Pow(Pow(B))"
 by blast
 
 lemma Pow_Int_eq [simp]: "Pow(A \<inter> B) = Pow(A) \<inter> Pow(B)"
 by blast
 
 lemma Pow_INT_eq: "A\<noteq>0 ==> Pow(\<Inter>x\<in>A. B(x)) = (\<Inter>x\<in>A. Pow(B(x)))"
 by (blast elim!: not_emptyE)
 
 
 subsection\<open>RepFun\<close>
 
 lemma RepFun_subset: "[| !!x. x\<in>A ==> f(x) \<in> B |] ==> {f(x). x\<in>A} \<subseteq> B"
 by blast
 
 lemma RepFun_eq_0_iff [simp]: "{f(x).x\<in>A}=0 \<longleftrightarrow> A=0"
 by blast
 
 lemma RepFun_constant [simp]: "{c. x\<in>A} = (if A=0 then 0 else {c})"
 by force
 
 
 subsection\<open>Collect\<close>
 
 lemma Collect_subset: "Collect(A,P) \<subseteq> A"
 by blast
 
 lemma Collect_Un: "Collect(A \<union> B, P) = Collect(A,P) \<union> Collect(B,P)"
 by blast
 
 lemma Collect_Int: "Collect(A \<inter> B, P) = Collect(A,P) \<inter> Collect(B,P)"
 by blast
 
 lemma Collect_Diff: "Collect(A - B, P) = Collect(A,P) - Collect(B,P)"
 by blast
 
 lemma Collect_cons: "{x\<in>cons(a,B). P(x)} =
       (if P(a) then cons(a, {x\<in>B. P(x)}) else {x\<in>B. P(x)})"
 by (simp, blast)
 
 lemma Int_Collect_self_eq: "A \<inter> Collect(A,P) = Collect(A,P)"
 by blast
 
 lemma Collect_Collect_eq [simp]:
      "Collect(Collect(A,P), Q) = Collect(A, %x. P(x) & Q(x))"
 by blast
 
 lemma Collect_Int_Collect_eq:
      "Collect(A,P) \<inter> Collect(A,Q) = Collect(A, %x. P(x) & Q(x))"
 by blast
 
 lemma Collect_Union_eq [simp]:
      "Collect(\<Union>x\<in>A. B(x), P) = (\<Union>x\<in>A. Collect(B(x), P))"
 by blast
 
 lemma Collect_Int_left: "{x\<in>A. P(x)} \<inter> B = {x \<in> A \<inter> B. P(x)}"
 by blast
 
 lemma Collect_Int_right: "A \<inter> {x\<in>B. P(x)} = {x \<in> A \<inter> B. P(x)}"
 by blast
 
 lemma Collect_disj_eq: "{x\<in>A. P(x) | Q(x)} = Collect(A, P) \<union> Collect(A, Q)"
 by blast
 
 lemma Collect_conj_eq: "{x\<in>A. P(x) & Q(x)} = Collect(A, P) \<inter> Collect(A, Q)"
 by blast
 
 lemmas subset_SIs = subset_refl cons_subsetI subset_consI
                     Union_least UN_least Un_least
                     Inter_greatest Int_greatest RepFun_subset
                     Un_upper1 Un_upper2 Int_lower1 Int_lower2
 
 ML \<open>
 val subset_cs =
   claset_of (\<^context>
     delrules [@{thm subsetI}, @{thm subsetCE}]
     addSIs @{thms subset_SIs}
     addIs  [@{thm Union_upper}, @{thm Inter_lower}]
     addSEs [@{thm cons_subsetE}]);
 
 val ZF_cs = claset_of (\<^context> delrules [@{thm equalityI}]);
 \<close>
 
 end
 
diff --git a/src/ZF/func.thy b/src/ZF/func.thy
--- a/src/ZF/func.thy
+++ b/src/ZF/func.thy
@@ -1,611 +1,611 @@
 (*  Title:      ZF/func.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 *)
 
 section\<open>Functions, Function Spaces, Lambda-Abstraction\<close>
 
 theory func imports equalities Sum begin
 
 subsection\<open>The Pi Operator: Dependent Function Space\<close>
 
 lemma subset_Sigma_imp_relation: "r \<subseteq> Sigma(A,B) ==> relation(r)"
 by (simp add: relation_def, blast)
 
 lemma relation_converse_converse [simp]:
      "relation(r) ==> converse(converse(r)) = r"
 by (simp add: relation_def, blast)
 
 lemma relation_restrict [simp]:  "relation(restrict(r,A))"
 by (simp add: restrict_def relation_def, blast)
 
 lemma Pi_iff:
     "f \<in> Pi(A,B) \<longleftrightarrow> function(f) & f<=Sigma(A,B) & A<=domain(f)"
 by (unfold Pi_def, blast)
 
 (*For upward compatibility with the former definition*)
 lemma Pi_iff_old:
     "f \<in> Pi(A,B) \<longleftrightarrow> f<=Sigma(A,B) & (\<forall>x\<in>A. \<exists>!y. <x,y>: f)"
 by (unfold Pi_def function_def, blast)
 
 lemma fun_is_function: "f \<in> Pi(A,B) ==> function(f)"
 by (simp only: Pi_iff)
 
 lemma function_imp_Pi:
      "[|function(f); relation(f)|] ==> f \<in> domain(f) -> range(f)"
 by (simp add: Pi_iff relation_def, blast)
 
 lemma functionI:
      "[| !!x y y'. [| <x,y>:r; <x,y'>:r |] ==> y=y' |] ==> function(r)"
 by (simp add: function_def, blast)
 
 (*Functions are relations*)
 lemma fun_is_rel: "f \<in> Pi(A,B) ==> f \<subseteq> Sigma(A,B)"
 by (unfold Pi_def, blast)
 
 lemma Pi_cong:
     "[| A=A';  !!x. x \<in> A' ==> B(x)=B'(x) |] ==> Pi(A,B) = Pi(A',B')"
 by (simp add: Pi_def cong add: Sigma_cong)
 
 (*Sigma_cong, Pi_cong NOT given to Addcongs: they cause
   flex-flex pairs and the "Check your prover" error.  Most
   Sigmas and Pis are abbreviated as * or -> *)
 
 (*Weakening one function type to another; see also Pi_type*)
 lemma fun_weaken_type: "[| f \<in> A->B;  B<=D |] ==> f \<in> A->D"
 by (unfold Pi_def, best)
 
 subsection\<open>Function Application\<close>
 
 lemma apply_equality2: "[| <a,b>: f;  <a,c>: f;  f \<in> Pi(A,B) |] ==> b=c"
 by (unfold Pi_def function_def, blast)
 
 lemma function_apply_equality: "[| <a,b>: f;  function(f) |] ==> f`a = b"
 by (unfold apply_def function_def, blast)
 
 lemma apply_equality: "[| <a,b>: f;  f \<in> Pi(A,B) |] ==> f`a = b"
 apply (unfold Pi_def)
 apply (blast intro: function_apply_equality)
 done
 
 (*Applying a function outside its domain yields 0*)
 lemma apply_0: "a \<notin> domain(f) ==> f`a = 0"
 by (unfold apply_def, blast)
 
 lemma Pi_memberD: "[| f \<in> Pi(A,B);  c \<in> f |] ==> \<exists>x\<in>A.  c = <x,f`x>"
 apply (frule fun_is_rel)
 apply (blast dest: apply_equality)
 done
 
 lemma function_apply_Pair: "[| function(f);  a \<in> domain(f)|] ==> <a,f`a>: f"
 apply (simp add: function_def, clarify)
 apply (subgoal_tac "f`a = y", blast)
 apply (simp add: apply_def, blast)
 done
 
 lemma apply_Pair: "[| f \<in> Pi(A,B);  a \<in> A |] ==> <a,f`a>: f"
 apply (simp add: Pi_iff)
 apply (blast intro: function_apply_Pair)
 done
 
 (*Conclusion is flexible -- use rule_tac or else apply_funtype below!*)
 lemma apply_type [TC]: "[| f \<in> Pi(A,B);  a \<in> A |] ==> f`a \<in> B(a)"
 by (blast intro: apply_Pair dest: fun_is_rel)
 
 (*This version is acceptable to the simplifier*)
 lemma apply_funtype: "[| f \<in> A->B;  a \<in> A |] ==> f`a \<in> B"
 by (blast dest: apply_type)
 
 lemma apply_iff: "f \<in> Pi(A,B) ==> <a,b>: f \<longleftrightarrow> a \<in> A & f`a = b"
 apply (frule fun_is_rel)
 apply (blast intro!: apply_Pair apply_equality)
 done
 
 (*Refining one Pi type to another*)
 lemma Pi_type: "[| f \<in> Pi(A,C);  !!x. x \<in> A ==> f`x \<in> B(x) |] ==> f \<in> Pi(A,B)"
 apply (simp only: Pi_iff)
 apply (blast dest: function_apply_equality)
 done
 
 (*Such functions arise in non-standard datatypes, ZF/ex/Ntree for instance*)
 lemma Pi_Collect_iff:
      "(f \<in> Pi(A, %x. {y \<in> B(x). P(x,y)}))
       \<longleftrightarrow>  f \<in> Pi(A,B) & (\<forall>x\<in>A. P(x, f`x))"
 by (blast intro: Pi_type dest: apply_type)
 
 lemma Pi_weaken_type:
         "[| f \<in> Pi(A,B);  !!x. x \<in> A ==> B(x)<=C(x) |] ==> f \<in> Pi(A,C)"
 by (blast intro: Pi_type dest: apply_type)
 
 
 (** Elimination of membership in a function **)
 
 lemma domain_type: "[| <a,b> \<in> f;  f \<in> Pi(A,B) |] ==> a \<in> A"
 by (blast dest: fun_is_rel)
 
 lemma range_type: "[| <a,b> \<in> f;  f \<in> Pi(A,B) |] ==> b \<in> B(a)"
 by (blast dest: fun_is_rel)
 
 lemma Pair_mem_PiD: "[| <a,b>: f;  f \<in> Pi(A,B) |] ==> a \<in> A & b \<in> B(a) & f`a = b"
 by (blast intro: domain_type range_type apply_equality)
 
 subsection\<open>Lambda Abstraction\<close>
 
 lemma lamI: "a \<in> A ==> <a,b(a)> \<in> (\<lambda>x\<in>A. b(x))"
 apply (unfold lam_def)
 apply (erule RepFunI)
 done
 
 lemma lamE:
     "[| p: (\<lambda>x\<in>A. b(x));  !!x.[| x \<in> A; p=<x,b(x)> |] ==> P
      |] ==>  P"
 by (simp add: lam_def, blast)
 
 lemma lamD: "[| <a,c>: (\<lambda>x\<in>A. b(x)) |] ==> c = b(a)"
 by (simp add: lam_def)
 
 lemma lam_type [TC]:
     "[| !!x. x \<in> A ==> b(x): B(x) |] ==> (\<lambda>x\<in>A. b(x)) \<in> Pi(A,B)"
 by (simp add: lam_def Pi_def function_def, blast)
 
 lemma lam_funtype: "(\<lambda>x\<in>A. b(x)) \<in> A -> {b(x). x \<in> A}"
 by (blast intro: lam_type)
 
 lemma function_lam: "function (\<lambda>x\<in>A. b(x))"
 by (simp add: function_def lam_def)
 
 lemma relation_lam: "relation (\<lambda>x\<in>A. b(x))"
 by (simp add: relation_def lam_def)
 
 lemma beta_if [simp]: "(\<lambda>x\<in>A. b(x)) ` a = (if a \<in> A then b(a) else 0)"
 by (simp add: apply_def lam_def, blast)
 
 lemma beta: "a \<in> A ==> (\<lambda>x\<in>A. b(x)) ` a = b(a)"
 by (simp add: apply_def lam_def, blast)
 
 lemma lam_empty [simp]: "(\<lambda>x\<in>0. b(x)) = 0"
 by (simp add: lam_def)
 
 lemma domain_lam [simp]: "domain(Lambda(A,b)) = A"
 by (simp add: lam_def, blast)
 
 (*congruence rule for lambda abstraction*)
 lemma lam_cong [cong]:
     "[| A=A';  !!x. x \<in> A' ==> b(x)=b'(x) |] ==> Lambda(A,b) = Lambda(A',b')"
 by (simp only: lam_def cong add: RepFun_cong)
 
 lemma lam_theI:
     "(!!x. x \<in> A ==> \<exists>!y. Q(x,y)) ==> \<exists>f. \<forall>x\<in>A. Q(x, f`x)"
 apply (rule_tac x = "\<lambda>x\<in>A. THE y. Q (x,y)" in exI)
 apply simp
 apply (blast intro: theI)
 done
 
 lemma lam_eqE: "[| (\<lambda>x\<in>A. f(x)) = (\<lambda>x\<in>A. g(x));  a \<in> A |] ==> f(a)=g(a)"
 by (fast intro!: lamI elim: equalityE lamE)
 
 
 (*Empty function spaces*)
 lemma Pi_empty1 [simp]: "Pi(0,A) = {0}"
 by (unfold Pi_def function_def, blast)
 
 (*The singleton function*)
 lemma singleton_fun [simp]: "{<a,b>} \<in> {a} -> {b}"
 by (unfold Pi_def function_def, blast)
 
 lemma Pi_empty2 [simp]: "(A->0) = (if A=0 then {0} else 0)"
 by (unfold Pi_def function_def, force)
 
 lemma  fun_space_empty_iff [iff]: "(A->X)=0 \<longleftrightarrow> X=0 & (A \<noteq> 0)"
 apply auto
 apply (fast intro!: equals0I intro: lam_type)
 done
 
 
 subsection\<open>Extensionality\<close>
 
 (*Semi-extensionality!*)
 
 lemma fun_subset:
     "[| f \<in> Pi(A,B);  g \<in> Pi(C,D);  A<=C;
         !!x. x \<in> A ==> f`x = g`x       |] ==> f<=g"
 by (force dest: Pi_memberD intro: apply_Pair)
 
 lemma fun_extension:
     "[| f \<in> Pi(A,B);  g \<in> Pi(A,D);
         !!x. x \<in> A ==> f`x = g`x       |] ==> f=g"
 by (blast del: subsetI intro: subset_refl sym fun_subset)
 
 lemma eta [simp]: "f \<in> Pi(A,B) ==> (\<lambda>x\<in>A. f`x) = f"
 apply (rule fun_extension)
 apply (auto simp add: lam_type apply_type beta)
 done
 
 lemma fun_extension_iff:
      "[| f \<in> Pi(A,B); g \<in> Pi(A,C) |] ==> (\<forall>a\<in>A. f`a = g`a) \<longleftrightarrow> f=g"
 by (blast intro: fun_extension)
 
 (*thm by Mark Staples, proof by lcp*)
 lemma fun_subset_eq: "[| f \<in> Pi(A,B); g \<in> Pi(A,C) |] ==> f \<subseteq> g \<longleftrightarrow> (f = g)"
 by (blast dest: apply_Pair
           intro: fun_extension apply_equality [symmetric])
 
 
 (*Every element of Pi(A,B) may be expressed as a lambda abstraction!*)
 lemma Pi_lamE:
   assumes major: "f \<in> Pi(A,B)"
       and minor: "!!b. [| \<forall>x\<in>A. b(x):B(x);  f = (\<lambda>x\<in>A. b(x)) |] ==> P"
   shows "P"
 apply (rule minor)
 apply (rule_tac [2] eta [symmetric])
 apply (blast intro: major apply_type)+
 done
 
 
 subsection\<open>Images of Functions\<close>
 
 lemma image_lam: "C \<subseteq> A ==> (\<lambda>x\<in>A. b(x)) `` C = {b(x). x \<in> C}"
 by (unfold lam_def, blast)
 
 lemma Repfun_function_if:
      "function(f)
       ==> {f`x. x \<in> C} = (if C \<subseteq> domain(f) then f``C else cons(0,f``C))"
 apply simp
 apply (intro conjI impI)
  apply (blast dest: function_apply_equality intro: function_apply_Pair)
 apply (rule equalityI)
  apply (blast intro!: function_apply_Pair apply_0)
 apply (blast dest: function_apply_equality intro: apply_0 [symmetric])
 done
 
 (*For this lemma and the next, the right-hand side could equivalently
   be written \<Union>x\<in>C. {f`x} *)
 lemma image_function:
      "[| function(f);  C \<subseteq> domain(f) |] ==> f``C = {f`x. x \<in> C}"
 by (simp add: Repfun_function_if)
 
 lemma image_fun: "[| f \<in> Pi(A,B);  C \<subseteq> A |] ==> f``C = {f`x. x \<in> C}"
 apply (simp add: Pi_iff)
 apply (blast intro: image_function)
 done
 
 lemma image_eq_UN:
   assumes f: "f \<in> Pi(A,B)" "C \<subseteq> A" shows "f``C = (\<Union>x\<in>C. {f ` x})"
 by (auto simp add: image_fun [OF f])
 
 lemma Pi_image_cons:
      "[| f \<in> Pi(A,B);  x \<in> A |] ==> f `` cons(x,y) = cons(f`x, f``y)"
 by (blast dest: apply_equality apply_Pair)
 
 
 subsection\<open>Properties of \<^term>\<open>restrict(f,A)\<close>\<close>
 
 lemma restrict_subset: "restrict(f,A) \<subseteq> f"
 by (unfold restrict_def, blast)
 
 lemma function_restrictI:
     "function(f) ==> function(restrict(f,A))"
 by (unfold restrict_def function_def, blast)
 
 lemma restrict_type2: "[| f \<in> Pi(C,B);  A<=C |] ==> restrict(f,A) \<in> Pi(A,B)"
 by (simp add: Pi_iff function_def restrict_def, blast)
 
 lemma restrict: "restrict(f,A) ` a = (if a \<in> A then f`a else 0)"
 by (simp add: apply_def restrict_def, blast)
 
 lemma restrict_empty [simp]: "restrict(f,0) = 0"
 by (unfold restrict_def, simp)
 
 lemma restrict_iff: "z \<in> restrict(r,A) \<longleftrightarrow> z \<in> r & (\<exists>x\<in>A. \<exists>y. z = \<langle>x, y\<rangle>)"
 by (simp add: restrict_def)
 
 lemma restrict_restrict [simp]:
      "restrict(restrict(r,A),B) = restrict(r, A \<inter> B)"
 by (unfold restrict_def, blast)
 
 lemma domain_restrict [simp]: "domain(restrict(f,C)) = domain(f) \<inter> C"
 apply (unfold restrict_def)
 apply (auto simp add: domain_def)
 done
 
 lemma restrict_idem: "f \<subseteq> Sigma(A,B) ==> restrict(f,A) = f"
 by (simp add: restrict_def, blast)
 
 
 (*converse probably holds too*)
 lemma domain_restrict_idem:
      "[| domain(r) \<subseteq> A; relation(r) |] ==> restrict(r,A) = r"
 by (simp add: restrict_def relation_def, blast)
 
 lemma domain_restrict_lam [simp]: "domain(restrict(Lambda(A,f),C)) = A \<inter> C"
 apply (unfold restrict_def lam_def)
 apply (rule equalityI)
 apply (auto simp add: domain_iff)
 done
 
 lemma restrict_if [simp]: "restrict(f,A) ` a = (if a \<in> A then f`a else 0)"
 by (simp add: restrict apply_0)
 
 lemma restrict_lam_eq:
     "A<=C ==> restrict(\<lambda>x\<in>C. b(x), A) = (\<lambda>x\<in>A. b(x))"
 by (unfold restrict_def lam_def, auto)
 
 lemma fun_cons_restrict_eq:
      "f \<in> cons(a, b) -> B ==> f = cons(<a, f ` a>, restrict(f, b))"
 apply (rule equalityI)
  prefer 2 apply (blast intro: apply_Pair restrict_subset [THEN subsetD])
 apply (auto dest!: Pi_memberD simp add: restrict_def lam_def)
 done
 
 
 subsection\<open>Unions of Functions\<close>
 
 (** The Union of a set of COMPATIBLE functions is a function **)
 
 lemma function_Union:
     "[| \<forall>x\<in>S. function(x);
         \<forall>x\<in>S. \<forall>y\<in>S. x<=y | y<=x  |]
      ==> function(\<Union>(S))"
 by (unfold function_def, blast)
 
 lemma fun_Union:
     "[| \<forall>f\<in>S. \<exists>C D. f \<in> C->D;
              \<forall>f\<in>S. \<forall>y\<in>S. f<=y | y<=f  |] ==>
           \<Union>(S) \<in> domain(\<Union>(S)) -> range(\<Union>(S))"
 apply (unfold Pi_def)
 apply (blast intro!: rel_Union function_Union)
 done
 
-lemma gen_relation_Union [rule_format]:
-     "\<forall>f\<in>F. relation(f) \<Longrightarrow> relation(\<Union>(F))"
+lemma gen_relation_Union:
+     "(\<And>f. f\<in>F \<Longrightarrow> relation(f)) \<Longrightarrow> relation(\<Union>(F))"
 by (simp add: relation_def)
 
 
 (** The Union of 2 disjoint functions is a function **)
 
 lemmas Un_rls = Un_subset_iff SUM_Un_distrib1 prod_Un_distrib2
                 subset_trans [OF _ Un_upper1]
                 subset_trans [OF _ Un_upper2]
 
 lemma fun_disjoint_Un:
      "[| f \<in> A->B;  g \<in> C->D;  A \<inter> C = 0  |]
       ==> (f \<union> g) \<in> (A \<union> C) -> (B \<union> D)"
 (*Prove the product and domain subgoals using distributive laws*)
 apply (simp add: Pi_iff extension Un_rls)
 apply (unfold function_def, blast)
 done
 
 lemma fun_disjoint_apply1: "a \<notin> domain(g) ==> (f \<union> g)`a = f`a"
 by (simp add: apply_def, blast)
 
 lemma fun_disjoint_apply2: "c \<notin> domain(f) ==> (f \<union> g)`c = g`c"
 by (simp add: apply_def, blast)
 
 subsection\<open>Domain and Range of a Function or Relation\<close>
 
 lemma domain_of_fun: "f \<in> Pi(A,B) ==> domain(f)=A"
 by (unfold Pi_def, blast)
 
 lemma apply_rangeI: "[| f \<in> Pi(A,B);  a \<in> A |] ==> f`a \<in> range(f)"
 by (erule apply_Pair [THEN rangeI], assumption)
 
 lemma range_of_fun: "f \<in> Pi(A,B) ==> f \<in> A->range(f)"
 by (blast intro: Pi_type apply_rangeI)
 
 subsection\<open>Extensions of Functions\<close>
 
 lemma fun_extend:
      "[| f \<in> A->B;  c\<notin>A |] ==> cons(<c,b>,f) \<in> cons(c,A) -> cons(b,B)"
 apply (frule singleton_fun [THEN fun_disjoint_Un], blast)
 apply (simp add: cons_eq)
 done
 
 lemma fun_extend3:
      "[| f \<in> A->B;  c\<notin>A;  b \<in> B |] ==> cons(<c,b>,f) \<in> cons(c,A) -> B"
 by (blast intro: fun_extend [THEN fun_weaken_type])
 
 lemma extend_apply:
      "c \<notin> domain(f) ==> cons(<c,b>,f)`a = (if a=c then b else f`a)"
 by (auto simp add: apply_def)
 
 lemma fun_extend_apply [simp]:
      "[| f \<in> A->B;  c\<notin>A |] ==> cons(<c,b>,f)`a = (if a=c then b else f`a)"
 apply (rule extend_apply)
 apply (simp add: Pi_def, blast)
 done
 
 lemmas singleton_apply = apply_equality [OF singletonI singleton_fun, simp]
 
 (*For Finite.ML.  Inclusion of right into left is easy*)
 lemma cons_fun_eq:
      "c \<notin> A ==> cons(c,A) -> B = (\<Union>f \<in> A->B. \<Union>b\<in>B. {cons(<c,b>, f)})"
 apply (rule equalityI)
 apply (safe elim!: fun_extend3)
 (*Inclusion of left into right*)
 apply (subgoal_tac "restrict (x, A) \<in> A -> B")
  prefer 2 apply (blast intro: restrict_type2)
 apply (rule UN_I, assumption)
 apply (rule apply_funtype [THEN UN_I])
   apply assumption
  apply (rule consI1)
 apply (simp (no_asm))
 apply (rule fun_extension)
   apply assumption
  apply (blast intro: fun_extend)
 apply (erule consE, simp_all)
 done
 
 lemma succ_fun_eq: "succ(n) -> B = (\<Union>f \<in> n->B. \<Union>b\<in>B. {cons(<n,b>, f)})"
 by (simp add: succ_def mem_not_refl cons_fun_eq)
 
 
 subsection\<open>Function Updates\<close>
 
 definition
   update  :: "[i,i,i] => i"  where
    "update(f,a,b) == \<lambda>x\<in>cons(a, domain(f)). if(x=a, b, f`x)"
 
 nonterminal updbinds and updbind
 
 syntax
 
   (* Let expressions *)
 
   "_updbind"    :: "[i, i] => updbind"               (\<open>(2_ :=/ _)\<close>)
   ""            :: "updbind => updbinds"             (\<open>_\<close>)
   "_updbinds"   :: "[updbind, updbinds] => updbinds" (\<open>_,/ _\<close>)
   "_Update"     :: "[i, updbinds] => i"              (\<open>_/'((_)')\<close> [900,0] 900)
 
 translations
   "_Update (f, _updbinds(b,bs))"  == "_Update (_Update(f,b), bs)"
   "f(x:=y)"                       == "CONST update(f,x,y)"
 
 
 lemma update_apply [simp]: "f(x:=y) ` z = (if z=x then y else f`z)"
 apply (simp add: update_def)
 apply (case_tac "z \<in> domain(f)")
 apply (simp_all add: apply_0)
 done
 
 lemma update_idem: "[| f`x = y;  f \<in> Pi(A,B);  x \<in> A |] ==> f(x:=y) = f"
 apply (unfold update_def)
 apply (simp add: domain_of_fun cons_absorb)
 apply (rule fun_extension)
 apply (best intro: apply_type if_type lam_type, assumption, simp)
 done
 
 
 (* [| f \<in> Pi(A, B); x \<in> A |] ==> f(x := f`x) = f *)
 declare refl [THEN update_idem, simp]
 
 lemma domain_update [simp]: "domain(f(x:=y)) = cons(x, domain(f))"
 by (unfold update_def, simp)
 
 lemma update_type: "[| f \<in> Pi(A,B);  x \<in> A;  y \<in> B(x) |] ==> f(x:=y) \<in> Pi(A, B)"
 apply (unfold update_def)
 apply (simp add: domain_of_fun cons_absorb apply_funtype lam_type)
 done
 
 
 subsection\<open>Monotonicity Theorems\<close>
 
 subsubsection\<open>Replacement in its Various Forms\<close>
 
 (*Not easy to express monotonicity in P, since any "bigger" predicate
   would have to be single-valued*)
 lemma Replace_mono: "A<=B ==> Replace(A,P) \<subseteq> Replace(B,P)"
 by (blast elim!: ReplaceE)
 
 lemma RepFun_mono: "A<=B ==> {f(x). x \<in> A} \<subseteq> {f(x). x \<in> B}"
 by blast
 
 lemma Pow_mono: "A<=B ==> Pow(A) \<subseteq> Pow(B)"
 by blast
 
 lemma Union_mono: "A<=B ==> \<Union>(A) \<subseteq> \<Union>(B)"
 by blast
 
 lemma UN_mono:
     "[| A<=C;  !!x. x \<in> A ==> B(x)<=D(x) |] ==> (\<Union>x\<in>A. B(x)) \<subseteq> (\<Union>x\<in>C. D(x))"
 by blast
 
 (*Intersection is ANTI-monotonic.  There are TWO premises! *)
 lemma Inter_anti_mono: "[| A<=B;  A\<noteq>0 |] ==> \<Inter>(B) \<subseteq> \<Inter>(A)"
 by blast
 
 lemma cons_mono: "C<=D ==> cons(a,C) \<subseteq> cons(a,D)"
 by blast
 
 lemma Un_mono: "[| A<=C;  B<=D |] ==> A \<union> B \<subseteq> C \<union> D"
 by blast
 
 lemma Int_mono: "[| A<=C;  B<=D |] ==> A \<inter> B \<subseteq> C \<inter> D"
 by blast
 
 lemma Diff_mono: "[| A<=C;  D<=B |] ==> A-B \<subseteq> C-D"
 by blast
 
 subsubsection\<open>Standard Products, Sums and Function Spaces\<close>
 
 lemma Sigma_mono [rule_format]:
      "[| A<=C;  !!x. x \<in> A \<longrightarrow> B(x) \<subseteq> D(x) |] ==> Sigma(A,B) \<subseteq> Sigma(C,D)"
 by blast
 
 lemma sum_mono: "[| A<=C;  B<=D |] ==> A+B \<subseteq> C+D"
 by (unfold sum_def, blast)
 
 (*Note that B->A and C->A are typically disjoint!*)
 lemma Pi_mono: "B<=C ==> A->B \<subseteq> A->C"
 by (blast intro: lam_type elim: Pi_lamE)
 
 lemma lam_mono: "A<=B ==> Lambda(A,c) \<subseteq> Lambda(B,c)"
 apply (unfold lam_def)
 apply (erule RepFun_mono)
 done
 
 subsubsection\<open>Converse, Domain, Range, Field\<close>
 
 lemma converse_mono: "r<=s ==> converse(r) \<subseteq> converse(s)"
 by blast
 
 lemma domain_mono: "r<=s ==> domain(r)<=domain(s)"
 by blast
 
 lemmas domain_rel_subset = subset_trans [OF domain_mono domain_subset]
 
 lemma range_mono: "r<=s ==> range(r)<=range(s)"
 by blast
 
 lemmas range_rel_subset = subset_trans [OF range_mono range_subset]
 
 lemma field_mono: "r<=s ==> field(r)<=field(s)"
 by blast
 
 lemma field_rel_subset: "r \<subseteq> A*A ==> field(r) \<subseteq> A"
 by (erule field_mono [THEN subset_trans], blast)
 
 
 subsubsection\<open>Images\<close>
 
 lemma image_pair_mono:
     "[| !! x y. <x,y>:r ==> <x,y>:s;  A<=B |] ==> r``A \<subseteq> s``B"
 by blast
 
 lemma vimage_pair_mono:
     "[| !! x y. <x,y>:r ==> <x,y>:s;  A<=B |] ==> r-``A \<subseteq> s-``B"
 by blast
 
 lemma image_mono: "[| r<=s;  A<=B |] ==> r``A \<subseteq> s``B"
 by blast
 
 lemma vimage_mono: "[| r<=s;  A<=B |] ==> r-``A \<subseteq> s-``B"
 by blast
 
 lemma Collect_mono:
     "[| A<=B;  !!x. x \<in> A ==> P(x) \<longrightarrow> Q(x) |] ==> Collect(A,P) \<subseteq> Collect(B,Q)"
 by blast
 
 (*Used in intr_elim.ML and in individual datatype definitions*)
 lemmas basic_monos = subset_refl imp_refl disj_mono conj_mono ex_mono
                      Collect_mono Part_mono in_mono
 
 (* Useful with simp; contributed by Clemens Ballarin. *)
 
 lemma bex_image_simp:
   "[| f \<in> Pi(X, Y); A \<subseteq> X |]  ==> (\<exists>x\<in>f``A. P(x)) \<longleftrightarrow> (\<exists>x\<in>A. P(f`x))"
   apply safe
    apply rule
     prefer 2 apply assumption
    apply (simp add: apply_equality)
   apply (blast intro: apply_Pair)
   done
 
 lemma ball_image_simp:
   "[| f \<in> Pi(X, Y); A \<subseteq> X |]  ==> (\<forall>x\<in>f``A. P(x)) \<longleftrightarrow> (\<forall>x\<in>A. P(f`x))"
   apply safe
    apply (blast intro: apply_Pair)
   apply (drule bspec) apply assumption
   apply (simp add: apply_equality)
   done
 
 end