src/ZF/Constructible/Relative.thy

 (*  Title:      ZF/Constructible/Relative.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+                With modifications by E. Gunther, M. Pagano, 
+                and P. Sánchez Terraf
 *)
 
 section \<open>Relativization and Absoluteness\<close>
 
 theory Relative imports ZF begin

 apply (blast intro: Limit_has_succ VfromI Collect_in_Vfrom)
 done
 
 lemma Collect_in_univ:
      "[| X \<in> univ(A);  Transset(A) |] ==> Collect(X,P) \<in> univ(A)"
-by (simp add: univ_def Collect_in_VLimit Limit_nat)
+by (simp add: univ_def Collect_in_VLimit)
 
 lemma "separation(\<lambda>x. x \<in> univ(0), P)"
 apply (simp add: separation_def, clarify)
 apply (rule_tac x = "Collect(z,P)" in bexI)
 apply (blast intro: Collect_in_univ Transset_0)+

 
 text\<open>Powerset axiom\<close>
 
 lemma Pow_in_univ:
      "[| X \<in> univ(A);  Transset(A) |] ==> Pow(X) \<in> univ(A)"
-apply (simp add: univ_def Pow_in_VLimit Limit_nat)
+apply (simp add: univ_def Pow_in_VLimit)
 done
 
 lemma "power_ax(\<lambda>x. x \<in> univ(0))"
 apply (simp add: power_ax_def powerset_def subset_def, clarify)
 apply (rule_tac x="Pow(x)" in bexI)

         \<forall>p[M]. p \<in> r \<longleftrightarrow> (\<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>A & x\<in>y & pair(M,x,y,p)))"
 
 
 subsection\<open>Introducing a Transitive Class Model\<close>
 
+text\<open>The class M is assumed to be transitive and inhabited\<close>
+locale M_trans =
+  fixes M
+  assumes transM:   "[| y\<in>x; M(x) |] ==> M(y)"
+    and M_inhabited: "\<exists>x . M(x)"
+
+lemma (in M_trans) nonempty [simp]:  "M(0)"
+proof -
+  have "M(x) \<longrightarrow> M(0)" for x
+  proof (rule_tac P="\<lambda>w. M(w) \<longrightarrow> M(0)" in eps_induct)
+    {
+    fix x
+    assume "\<forall>y\<in>x. M(y) \<longrightarrow> M(0)" "M(x)"
+    consider (a) "\<exists>y. y\<in>x" | (b) "x=0" by auto
+    then 
+    have "M(x) \<longrightarrow> M(0)" 
+    proof cases
+      case a
+      then show ?thesis using \<open>\<forall>y\<in>x._\<close> \<open>M(x)\<close> transM by auto
+    next
+      case b
+      then show ?thesis by simp
+    qed
+  }
+  then show "M(x) \<longrightarrow> M(0)" if "\<forall>y\<in>x. M(y) \<longrightarrow> M(0)" for x
+    using that by auto
+  qed
+  with M_inhabited
+  show "M(0)" using M_inhabited by blast
+qed
+
 text\<open>The class M is assumed to be transitive and to satisfy some
       relativized ZF axioms\<close>
-locale M_trivial =
-  fixes M
-  assumes transM:           "[| y\<in>x; M(x) |] ==> M(y)"
-      and upair_ax:         "upair_ax(M)"
+locale M_trivial = M_trans +
+  assumes upair_ax:         "upair_ax(M)"
       and Union_ax:         "Union_ax(M)"
-      and power_ax:         "power_ax(M)"
-      and replacement:      "replacement(M,P)"
-      and M_nat [iff]:      "M(nat)"           (*i.e. the axiom of infinity*)
-
-
-text\<open>Automatically discovers the proof using \<open>transM\<close>, \<open>nat_0I\<close>
-and \<open>M_nat\<close>.\<close>
-lemma (in M_trivial) nonempty [simp]: "M(0)"
-by (blast intro: transM)
-
-lemma (in M_trivial) rall_abs [simp]:
+
+lemma (in M_trans) rall_abs [simp]:
      "M(A) ==> (\<forall>x[M]. x\<in>A \<longrightarrow> P(x)) \<longleftrightarrow> (\<forall>x\<in>A. P(x))"
 by (blast intro: transM)
 
-lemma (in M_trivial) rex_abs [simp]:
+lemma (in M_trans) rex_abs [simp]:
      "M(A) ==> (\<exists>x[M]. x\<in>A & P(x)) \<longleftrightarrow> (\<exists>x\<in>A. P(x))"
 by (blast intro: transM)
 
-lemma (in M_trivial) ball_iff_equiv:
+lemma (in M_trans) ball_iff_equiv:
      "M(A) ==> (\<forall>x[M]. (x\<in>A \<longleftrightarrow> P(x))) \<longleftrightarrow>
                (\<forall>x\<in>A. P(x)) & (\<forall>x. P(x) \<longrightarrow> M(x) \<longrightarrow> x\<in>A)"
 by (blast intro: transM)
 
 text\<open>Simplifies proofs of equalities when there's an iff-equality
       available for rewriting, universally quantified over M.
       But it's not the only way to prove such equalities: its
       premises \<^term>\<open>M(A)\<close> and  \<^term>\<open>M(B)\<close> can be too strong.\<close>
-lemma (in M_trivial) M_equalityI:
+lemma (in M_trans) M_equalityI:
      "[| !!x. M(x) ==> x\<in>A \<longleftrightarrow> x\<in>B; M(A); M(B) |] ==> A=B"
-by (blast intro!: equalityI dest: transM)
+by (blast dest: transM)
 
 
 subsubsection\<open>Trivial Absoluteness Proofs: Empty Set, Pairs, etc.\<close>
 
-lemma (in M_trivial) empty_abs [simp]:
+lemma (in M_trans) empty_abs [simp]:
      "M(z) ==> empty(M,z) \<longleftrightarrow> z=0"
 apply (simp add: empty_def)
 apply (blast intro: transM)
 done
 
-lemma (in M_trivial) subset_abs [simp]:
+lemma (in M_trans) subset_abs [simp]:
      "M(A) ==> subset(M,A,B) \<longleftrightarrow> A \<subseteq> B"
 apply (simp add: subset_def)
 apply (blast intro: transM)
 done
 
-lemma (in M_trivial) upair_abs [simp]:
+lemma (in M_trans) upair_abs [simp]:
      "M(z) ==> upair(M,a,b,z) \<longleftrightarrow> z={a,b}"
 apply (simp add: upair_def)
 apply (blast intro: transM)
 done
 
-lemma (in M_trivial) upair_in_M_iff [iff]:
-     "M({a,b}) \<longleftrightarrow> M(a) & M(b)"
-apply (insert upair_ax, simp add: upair_ax_def)
-apply (blast intro: transM)
-done
-
-lemma (in M_trivial) singleton_in_M_iff [iff]:
+lemma (in M_trivial) upair_in_MI [intro!]:
+     " M(a) & M(b) \<Longrightarrow> M({a,b})"
+by (insert upair_ax, simp add: upair_ax_def)
+
+lemma (in M_trans) upair_in_MD [dest!]:
+     "M({a,b}) \<Longrightarrow> M(a) & M(b)"
+  by (blast intro: transM)
+
+lemma (in M_trivial) upair_in_M_iff [simp]:
+  "M({a,b}) \<longleftrightarrow> M(a) & M(b)"
+  by blast
+
+lemma (in M_trivial) singleton_in_MI [intro!]:
+     "M(a) \<Longrightarrow> M({a})"
+  by (insert upair_in_M_iff [of a a], simp)
+
+lemma (in M_trans) singleton_in_MD [dest!]:
+     "M({a}) \<Longrightarrow> M(a)"
+  by (insert upair_in_MD [of a a], simp)
+
+lemma (in M_trivial) singleton_in_M_iff [simp]:
      "M({a}) \<longleftrightarrow> M(a)"
-by (insert upair_in_M_iff [of a a], simp)
-
-lemma (in M_trivial) pair_abs [simp]:
+  by blast
+
+lemma (in M_trans) pair_abs [simp]:
      "M(z) ==> pair(M,a,b,z) \<longleftrightarrow> z=<a,b>"
 apply (simp add: pair_def Pair_def)
 apply (blast intro: transM)
 done
 
-lemma (in M_trivial) pair_in_M_iff [iff]:
+lemma (in M_trans) pair_in_MD [dest!]:
+     "M(<a,b>) \<Longrightarrow> M(a) & M(b)"
+  by (simp add: Pair_def, blast intro: transM)
+
+lemma (in M_trivial) pair_in_MI [intro!]:
+     "M(a) & M(b) \<Longrightarrow> M(<a,b>)"
+  by (simp add: Pair_def)
+
+lemma (in M_trivial) pair_in_M_iff [simp]:
      "M(<a,b>) \<longleftrightarrow> M(a) & M(b)"
-by (simp add: Pair_def)
-
-lemma (in M_trivial) pair_components_in_M:
+  by blast
+
+lemma (in M_trans) pair_components_in_M:
      "[| <x,y> \<in> A; M(A) |] ==> M(x) & M(y)"
-apply (simp add: Pair_def)
-apply (blast dest: transM)
-done
+  by (blast dest: transM)
 
 lemma (in M_trivial) cartprod_abs [simp]:
      "[| M(A); M(B); M(z) |] ==> cartprod(M,A,B,z) \<longleftrightarrow> z = A*B"
 apply (simp add: cartprod_def)
 apply (rule iffI)

 apply (blast dest: transM)
 done
 
 subsubsection\<open>Absoluteness for Unions and Intersections\<close>
 
-lemma (in M_trivial) union_abs [simp]:
+lemma (in M_trans) union_abs [simp]:
      "[| M(a); M(b); M(z) |] ==> union(M,a,b,z) \<longleftrightarrow> z = a \<union> b"
-apply (simp add: union_def)
-apply (blast intro: transM)
-done
-
-lemma (in M_trivial) inter_abs [simp]:
+  unfolding union_def
+  by (blast intro: transM )
+
+lemma (in M_trans) inter_abs [simp]:
      "[| M(a); M(b); M(z) |] ==> inter(M,a,b,z) \<longleftrightarrow> z = a \<inter> b"
-apply (simp add: inter_def)
-apply (blast intro: transM)
-done
-
-lemma (in M_trivial) setdiff_abs [simp]:
+  unfolding inter_def
+  by (blast intro: transM)
+
+lemma (in M_trans) setdiff_abs [simp]:
      "[| M(a); M(b); M(z) |] ==> setdiff(M,a,b,z) \<longleftrightarrow> z = a-b"
-apply (simp add: setdiff_def)
-apply (blast intro: transM)
-done
-
-lemma (in M_trivial) Union_abs [simp]:
+  unfolding setdiff_def
+  by (blast intro: transM)
+
+lemma (in M_trans) Union_abs [simp]:
      "[| M(A); M(z) |] ==> big_union(M,A,z) \<longleftrightarrow> z = \<Union>(A)"
-apply (simp add: big_union_def)
-apply (blast intro!: equalityI dest: transM)
-done
+  unfolding big_union_def
+  by (blast  dest: transM)
 
 lemma (in M_trivial) Union_closed [intro,simp]:
      "M(A) ==> M(\<Union>(A))"
 by (insert Union_ax, simp add: Union_ax_def)
 

 
 lemma (in M_trivial) successor_abs [simp]:
      "[| M(a); M(z) |] ==> successor(M,a,z) \<longleftrightarrow> z = succ(a)"
 by (simp add: successor_def, blast)
 
-lemma (in M_trivial) succ_in_M_iff [iff]:
+lemma (in M_trans) succ_in_MD [dest!]:
+     "M(succ(a)) \<Longrightarrow> M(a)"
+  unfolding succ_def
+  by (blast intro: transM)
+
+lemma (in M_trivial) succ_in_MI [intro!]:
+     "M(a) \<Longrightarrow> M(succ(a))"
+  unfolding succ_def
+  by (blast intro: transM)
+
+lemma (in M_trivial) succ_in_M_iff [simp]:
      "M(succ(a)) \<longleftrightarrow> M(a)"
-apply (simp add: succ_def)
-apply (blast intro: transM)
-done
+  by blast
 
 subsubsection\<open>Absoluteness for Separation and Replacement\<close>
 
-lemma (in M_trivial) separation_closed [intro,simp]:
+lemma (in M_trans) separation_closed [intro,simp]:
      "[| separation(M,P); M(A) |] ==> M(Collect(A,P))"
 apply (insert separation, simp add: separation_def)
 apply (drule rspec, assumption, clarify)
 apply (subgoal_tac "y = Collect(A,P)", blast)
 apply (blast dest: transM)

 
 lemma separation_iff:
      "separation(M,P) \<longleftrightarrow> (\<forall>z[M]. \<exists>y[M]. is_Collect(M,z,P,y))"
 by (simp add: separation_def is_Collect_def)
 
-lemma (in M_trivial) Collect_abs [simp]:
+lemma (in M_trans) Collect_abs [simp]:
      "[| M(A); M(z) |] ==> is_Collect(M,A,P,z) \<longleftrightarrow> z = Collect(A,P)"
-apply (simp add: is_Collect_def)
-apply (blast intro!: equalityI dest: transM)
-done
-
-text\<open>Probably the premise and conclusion are equivalent\<close>
-lemma (in M_trivial) strong_replacementI [rule_format]:
-    "[| \<forall>B[M]. separation(M, %u. \<exists>x[M]. x\<in>B & P(x,u)) |]
-     ==> strong_replacement(M,P)"
-apply (simp add: strong_replacement_def, clarify)
-apply (frule replacementD [OF replacement], assumption, clarify)
-apply (drule_tac x=A in rspec, clarify)
-apply (drule_tac z=Y in separationD, assumption, clarify)
-apply (rule_tac x=y in rexI, force, assumption)
-done
+  unfolding is_Collect_def
+  by (blast dest: transM)
 
 subsubsection\<open>The Operator \<^term>\<open>is_Replace\<close>\<close>
 
 
 lemma is_Replace_cong [cong]:

          z=z' |]
       ==> is_Replace(M, A, %x y. P(x,y), z) \<longleftrightarrow>
           is_Replace(M, A', %x y. P'(x,y), z')"
 by (simp add: is_Replace_def)
 
-lemma (in M_trivial) univalent_Replace_iff:
+lemma (in M_trans) univalent_Replace_iff:
      "[| M(A); univalent(M,A,P);
          !!x y. [| x\<in>A; P(x,y) |] ==> M(y) |]
       ==> u \<in> Replace(A,P) \<longleftrightarrow> (\<exists>x. x\<in>A & P(x,u))"
-apply (simp add: Replace_iff univalent_def)
-apply (blast dest: transM)
-done
+  unfolding Replace_iff univalent_def
+  by (blast dest: transM)
 
 (*The last premise expresses that P takes M to M*)
-lemma (in M_trivial) strong_replacement_closed [intro,simp]:
+lemma (in M_trans) strong_replacement_closed [intro,simp]:
      "[| strong_replacement(M,P); M(A); univalent(M,A,P);
          !!x y. [| x\<in>A; P(x,y) |] ==> M(y) |] ==> M(Replace(A,P))"
 apply (simp add: strong_replacement_def)
 apply (drule_tac x=A in rspec, safe)
 apply (subgoal_tac "Replace(A,P) = Y")

 apply (rule equality_iffI)
 apply (simp add: univalent_Replace_iff)
 apply (blast dest: transM)
 done
 
-lemma (in M_trivial) Replace_abs:
+lemma (in M_trans) Replace_abs:
      "[| M(A); M(z); univalent(M,A,P);
          !!x y. [| x\<in>A; P(x,y) |] ==> M(y)  |]
       ==> is_Replace(M,A,P,z) \<longleftrightarrow> z = Replace(A,P)"
 apply (simp add: is_Replace_def)
 apply (rule iffI)

   Let K be a nonconstructible subset of nat and define
   f(x) = x if x \<in> K and f(x)=0 otherwise.  Then RepFun(nat,f) = cons(0,K), a
   nonconstructible set.  So we cannot assume that M(X) implies M(RepFun(X,f))
   even for f \<in> M -> M.
 *)
-lemma (in M_trivial) RepFun_closed:
+lemma (in M_trans) RepFun_closed:
      "[| strong_replacement(M, \<lambda>x y. y = f(x)); M(A); \<forall>x\<in>A. M(f(x)) |]
       ==> M(RepFun(A,f))"
 apply (simp add: RepFun_def)
 done
 
 lemma Replace_conj_eq: "{y . x \<in> A, x\<in>A & y=f(x)} = {y . x\<in>A, y=f(x)}"
 by simp
 
 text\<open>Better than \<open>RepFun_closed\<close> when having the formula \<^term>\<open>x\<in>A\<close>
       makes relativization easier.\<close>
-lemma (in M_trivial) RepFun_closed2:
+lemma (in M_trans) RepFun_closed2:
      "[| strong_replacement(M, \<lambda>x y. x\<in>A & y = f(x)); M(A); \<forall>x\<in>A. M(f(x)) |]
       ==> M(RepFun(A, %x. f(x)))"
 apply (simp add: RepFun_def)
 apply (frule strong_replacement_closed, assumption)
 apply (auto dest: transM  simp add: Replace_conj_eq univalent_def)

          !!x y. [| x\<in>A; M(x); M(y) |] ==> is_b(x,y) \<longleftrightarrow> is_b'(x,y) |]
       ==> is_lambda(M, A, %x y. is_b(x,y), z) \<longleftrightarrow>
           is_lambda(M, A', %x y. is_b'(x,y), z')"
 by (simp add: is_lambda_def)
 
-lemma (in M_trivial) image_abs [simp]:
+lemma (in M_trans) image_abs [simp]:
      "[| M(r); M(A); M(z) |] ==> image(M,r,A,z) \<longleftrightarrow> z = r``A"
 apply (simp add: image_def)
 apply (rule iffI)
  apply (blast intro!: equalityI dest: transM, blast)
 done
 
+subsubsection\<open>Relativization of Powerset\<close>
+
 text\<open>What about \<open>Pow_abs\<close>?  Powerset is NOT absolute!
       This result is one direction of absoluteness.\<close>
 
-lemma (in M_trivial) powerset_Pow:
+lemma (in M_trans) powerset_Pow:
      "powerset(M, x, Pow(x))"
 by (simp add: powerset_def)
 
 text\<open>But we can't prove that the powerset in \<open>M\<close> includes the
       real powerset.\<close>
-lemma (in M_trivial) powerset_imp_subset_Pow:
+
+lemma (in M_trans) powerset_imp_subset_Pow:
      "[| powerset(M,x,y); M(y) |] ==> y \<subseteq> Pow(x)"
 apply (simp add: powerset_def)
 apply (blast dest: transM)
 done
 
+lemma (in M_trans) powerset_abs:
+  assumes
+     "M(y)"
+  shows
+    "powerset(M,x,y) \<longleftrightarrow> y = {a\<in>Pow(x) . M(a)}"
+proof (intro iffI equalityI)
+  (* First show the converse implication by double inclusion *)
+  assume "powerset(M,x,y)"
+  with \<open>M(y)\<close>  
+  show "y \<subseteq> {a\<in>Pow(x) . M(a)}"
+    using powerset_imp_subset_Pow transM by blast
+  from \<open>powerset(M,x,y)\<close>
+  show "{a\<in>Pow(x) . M(a)} \<subseteq> y"
+    using transM unfolding powerset_def by auto
+next (* we show the direct implication *)
+  assume
+    "y = {a \<in> Pow(x) . M(a)}"
+  then
+  show "powerset(M, x, y)"
+    unfolding powerset_def subset_def using transM by blast
+qed
+
 subsubsection\<open>Absoluteness for the Natural Numbers\<close>
 
 lemma (in M_trivial) nat_into_M [intro]:
      "n \<in> nat ==> M(n)"
 by (induct n rule: nat_induct, simp_all)
 
-lemma (in M_trivial) nat_case_closed [intro,simp]:
+lemma (in M_trans) nat_case_closed [intro,simp]:
   "[|M(k); M(a); \<forall>m[M]. M(b(m))|] ==> M(nat_case(a,b,k))"
 apply (case_tac "k=0", simp)
 apply (case_tac "\<exists>m. k = succ(m)", force)
 apply (simp add: nat_case_def)
 done

 
 
 subsection\<open>Absoluteness for Ordinals\<close>
 text\<open>These results constitute Theorem IV 5.1 of Kunen (page 126).\<close>
 
-lemma (in M_trivial) lt_closed:
+lemma (in M_trans) lt_closed:
      "[| j<i; M(i) |] ==> M(j)"
 by (blast dest: ltD intro: transM)
 
-lemma (in M_trivial) transitive_set_abs [simp]:
+lemma (in M_trans) transitive_set_abs [simp]:
      "M(a) ==> transitive_set(M,a) \<longleftrightarrow> Transset(a)"
 by (simp add: transitive_set_def Transset_def)
 
-lemma (in M_trivial) ordinal_abs [simp]:
+lemma (in M_trans) ordinal_abs [simp]:
      "M(a) ==> ordinal(M,a) \<longleftrightarrow> Ord(a)"
 by (simp add: ordinal_def Ord_def)
 
 lemma (in M_trivial) limit_ordinal_abs [simp]:
      "M(a) ==> limit_ordinal(M,a) \<longleftrightarrow> Limit(a)"

      ==> separation(M,
             \<lambda>x. \<exists>xa[M]. \<exists>xb[M].
                 pair(M,x,a,xa) & xa \<in> r & pair(M,x,b,xb) & xb \<in> r &
                 (\<exists>fx[M]. \<exists>gx[M]. fun_apply(M,f,x,fx) & fun_apply(M,g,x,gx) &
                                    fx \<noteq> gx))"
-
-lemma (in M_basic) cartprod_iff_lemma:
+     and power_ax:         "power_ax(M)"
+
+lemma (in M_trivial) cartprod_iff_lemma:
      "[| M(C);  \<forall>u[M]. u \<in> C \<longleftrightarrow> (\<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}});
          powerset(M, A \<union> B, p1); powerset(M, p1, p2);  M(p2) |]
        ==> C = {u \<in> p2 . \<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}}}"
 apply (simp add: powerset_def)
 apply (rule equalityI, clarify, simp)

 by (simp add: vimage_def)
 
 
 subsubsection\<open>Domain, range and field\<close>
 
-lemma (in M_basic) domain_abs [simp]:
+lemma (in M_trans) domain_abs [simp]:
      "[| M(r); M(z) |] ==> is_domain(M,r,z) \<longleftrightarrow> z = domain(r)"
 apply (simp add: is_domain_def)
 apply (blast intro!: equalityI dest: transM)
 done
 
 lemma (in M_basic) domain_closed [intro,simp]:
      "M(r) ==> M(domain(r))"
 apply (simp add: domain_eq_vimage)
 done
 
-lemma (in M_basic) range_abs [simp]:
+lemma (in M_trans) range_abs [simp]:
      "[| M(r); M(z) |] ==> is_range(M,r,z) \<longleftrightarrow> z = range(r)"
 apply (simp add: is_range_def)
 apply (blast intro!: equalityI dest: transM)
 done
 

 apply (simp add: range_eq_image)
 done
 
 lemma (in M_basic) field_abs [simp]:
      "[| M(r); M(z) |] ==> is_field(M,r,z) \<longleftrightarrow> z = field(r)"
-by (simp add: domain_closed range_closed is_field_def field_def)
+by (simp add: is_field_def field_def)
 
 lemma (in M_basic) field_closed [intro,simp]:
      "M(r) ==> M(field(r))"
-by (simp add: domain_closed range_closed Un_closed field_def)
+by (simp add: field_def)
 
 
 subsubsection\<open>Relations, functions and application\<close>
 
-lemma (in M_basic) relation_abs [simp]:
+lemma (in M_trans) relation_abs [simp]:
      "M(r) ==> is_relation(M,r) \<longleftrightarrow> relation(r)"
 apply (simp add: is_relation_def relation_def)
 apply (blast dest!: bspec dest: pair_components_in_M)+
 done
 
-lemma (in M_basic) function_abs [simp]:
+lemma (in M_trivial) function_abs [simp]:
      "M(r) ==> is_function(M,r) \<longleftrightarrow> function(r)"
 apply (simp add: is_function_def function_def, safe)
    apply (frule transM, assumption)
   apply (blast dest: pair_components_in_M)+
 done

 lemma (in M_basic) apply_abs [simp]:
      "[| M(f); M(x); M(y) |] ==> fun_apply(M,f,x,y) \<longleftrightarrow> f`x = y"
 apply (simp add: fun_apply_def apply_def, blast)
 done
 
-lemma (in M_basic) typed_function_abs [simp]:
+lemma (in M_trivial) typed_function_abs [simp]:
      "[| M(A); M(f) |] ==> typed_function(M,A,B,f) \<longleftrightarrow> f \<in> A -> B"
 apply (auto simp add: typed_function_def relation_def Pi_iff)
 apply (blast dest: pair_components_in_M)+
 done
 
 lemma (in M_basic) injection_abs [simp]:
      "[| M(A); M(f) |] ==> injection(M,A,B,f) \<longleftrightarrow> f \<in> inj(A,B)"
-apply (simp add: injection_def apply_iff inj_def apply_closed)
+apply (simp add: injection_def apply_iff inj_def)
 apply (blast dest: transM [of _ A])
 done
 
 lemma (in M_basic) surjection_abs [simp]:
      "[| M(A); M(B); M(f) |] ==> surjection(M,A,B,f) \<longleftrightarrow> f \<in> surj(A,B)"

       ==> function(z)"
 apply (simp add: restriction_def ball_iff_equiv)
 apply (unfold function_def, blast)
 done
 
-lemma (in M_basic) restriction_abs [simp]:
+lemma (in M_trans) restriction_abs [simp]:
      "[| M(f); M(A); M(z) |]
       ==> restriction(M,f,A,z) \<longleftrightarrow> z = restrict(f,A)"
 apply (simp add: ball_iff_equiv restriction_def restrict_def)
 apply (blast intro!: equalityI dest: transM)
 done
 
 
-lemma (in M_basic) M_restrict_iff:
+lemma (in M_trans) M_restrict_iff:
      "M(r) ==> restrict(r,A) = {z \<in> r . \<exists>x\<in>A. \<exists>y[M]. z = \<langle>x, y\<rangle>}"
 by (simp add: restrict_def, blast dest: transM)
 
 lemma (in M_basic) restrict_closed [intro,simp]:
      "[| M(A); M(r) |] ==> M(restrict(r,A))"
 apply (simp add: M_restrict_iff)
 apply (insert restrict_separation [of A], simp)
 done
 
-lemma (in M_basic) Inter_abs [simp]:
+lemma (in M_trans) Inter_abs [simp]:
      "[| M(A); M(z) |] ==> big_inter(M,A,z) \<longleftrightarrow> z = \<Inter>(A)"
 apply (simp add: big_inter_def Inter_def)
 apply (blast intro!: equalityI dest: transM)
 done
 

 
 lemma Diff_Collect_eq:
      "A - Collect(A,P) = Collect(A, %x. ~ P(x))"
 by blast
 
-lemma (in M_trivial) Collect_rall_eq:
+lemma (in M_trans) Collect_rall_eq:
      "M(Y) ==> Collect(A, %x. \<forall>y[M]. y\<in>Y \<longrightarrow> P(x,y)) =
                (if Y=0 then A else (\<Inter>y \<in> Y. {x \<in> A. P(x,y)}))"
-apply simp
-apply (blast intro!: equalityI dest: transM)
-done
+  by (simp,blast dest: transM)
+
 
 lemma (in M_basic) separation_disj:
      "[|separation(M,P); separation(M,Q)|] ==> separation(M, \<lambda>z. P(z) | Q(z))"
 by (simp del: separation_closed
          add: separation_iff Collect_Un_Collect_eq [symmetric])

      "[|M(Y); \<forall>y[M]. separation(M, \<lambda>x. P(x,y));
         \<forall>z[M]. strong_replacement(M, \<lambda>x y. y = {u \<in> z . P(u,x)})|]
       ==> separation(M, \<lambda>x. \<forall>y[M]. y\<in>Y \<longrightarrow> P(x,y))"
 apply (simp del: separation_closed rall_abs
          add: separation_iff Collect_rall_eq)
-apply (blast intro!: Inter_closed RepFun_closed dest: transM)
+apply (blast intro!:  RepFun_closed dest: transM)
 done
 
 
 subsubsection\<open>Functions and function space\<close>
 
 text\<open>The assumption \<^term>\<open>M(A->B)\<close> is unusual, but essential: in
 all but trivial cases, A->B cannot be expected to belong to \<^term>\<open>M\<close>.\<close>
-lemma (in M_basic) is_funspace_abs [simp]:
+lemma (in M_trivial) is_funspace_abs [simp]:
      "[|M(A); M(B); M(F); M(A->B)|] ==> is_funspace(M,A,B,F) \<longleftrightarrow> F = A->B"
 apply (simp add: is_funspace_def)
 apply (rule iffI)
  prefer 2 apply blast
 apply (rule M_equalityI)