# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1580833155 0
# Node ID 89d05db6dd1f8f22a107c840a9321294d5c6b421
# Parent  6a1c1d1ce6ae6aabd719fc74971ca6a82bc5783c
Simplified, generalised version of Constructible due to E. Gunther, M. Pagano and P. Sánchez Terraf

diff -r 6a1c1d1ce6ae -r 89d05db6dd1f src/ZF/Constructible/AC_in_L.thy
--- a/src/ZF/Constructible/AC_in_L.thy	Tue Feb 04 16:36:49 2020 +0100
+++ b/src/ZF/Constructible/AC_in_L.thy	Tue Feb 04 16:19:15 2020 +0000
@@ -311,7 +311,7 @@
     "well_ord(A,r) ==> well_ord(DPow(A), DPow_r(fn,r,A))"
 apply (simp add: DPow_r_def)
 apply (rule well_ord_measure)
- apply (simp add: DPow_least_def Ord_Least)
+ apply (simp add: DPow_least_def)
 apply (drule DPow_imp_DPow_least, assumption)+
 apply simp
 apply (blast intro: DPow_ord_unique)
@@ -357,7 +357,7 @@
                       Ord_mem_iff_lt)
  apply (blast intro: lt_trans)
 apply (rule_tac x = "succ(lrank(x))" in bexI)
- apply (simp add: Lset_succ_lrank_iff)
+ apply (simp)
 apply (blast intro: Limit_has_succ ltD)
 done
 
diff -r 6a1c1d1ce6ae -r 89d05db6dd1f src/ZF/Constructible/DPow_absolute.thy
--- a/src/ZF/Constructible/DPow_absolute.thy	Tue Feb 04 16:36:49 2020 +0100
+++ b/src/ZF/Constructible/DPow_absolute.thy	Tue Feb 04 16:19:15 2020 +0000
@@ -92,14 +92,13 @@
    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     ==> sats(A, satisfies_fm(x,y,z), env) \<longleftrightarrow>
         is_satisfies(##A, nth(x,env), nth(y,env), nth(z,env))"
-by (simp add: satisfies_fm_def is_satisfies_def sats_satisfies_MH_fm
-              sats_formula_rec_fm)
+by (simp add: satisfies_fm_def is_satisfies_def sats_formula_rec_fm)
 
 lemma satisfies_iff_sats:
       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
           i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
        ==> is_satisfies(##A, x, y, z) \<longleftrightarrow> sats(A, satisfies_fm(i,j,k), env)"
-by (simp add: sats_satisfies_fm)
+by (simp)
 
 theorem satisfies_reflection:
      "REFLECTS[\<lambda>x. is_satisfies(L,f(x),g(x),h(x)),
@@ -294,7 +293,7 @@
    apply (assumption | rule DPow_separation DPow_replacement)+
   done
 
-theorem M_DPow_L: "PROP M_DPow(L)"
+theorem M_DPow_L: "M_DPow(L)"
   apply (rule M_DPow.intro)
    apply (rule M_satisfies_L)
   apply (rule M_DPow_axioms_L)
@@ -443,7 +442,7 @@
       "[| nth(i,env) = x; nth(j,env) = y; 
           i \<in> nat; j \<in> nat; env \<in> list(A)|]
        ==> is_DPow'(##A, x, y) \<longleftrightarrow> sats(A, DPow'_fm(i,j), env)"
-by (simp add: sats_DPow'_fm)
+by (simp)
 
 theorem DPow'_reflection:
      "REFLECTS[\<lambda>x. is_DPow'(L,f(x),g(x)),
@@ -600,7 +599,7 @@
        apply (assumption | rule strong_rep transrec_rep)+
   done
 
-theorem M_Lset_L: "PROP M_Lset(L)"
+theorem M_Lset_L: "M_Lset(L)"
   apply (rule M_Lset.intro) 
    apply (rule M_DPow_L)
   apply (rule M_Lset_axioms_L) 
diff -r 6a1c1d1ce6ae -r 89d05db6dd1f src/ZF/Constructible/Datatype_absolute.thy
--- a/src/ZF/Constructible/Datatype_absolute.thy	Tue Feb 04 16:36:49 2020 +0100
+++ b/src/ZF/Constructible/Datatype_absolute.thy	Tue Feb 04 16:19:15 2020 +0000
@@ -137,7 +137,7 @@
 by (simp add: nat_case_abs [of _ "\<lambda>m. F(g ` m)"]
               relation1_def iterates_MH_def)  
 
-lemma (in M_basic) iterates_imp_wfrec_replacement:
+lemma (in M_trancl) iterates_imp_wfrec_replacement:
   "[|relation1(M,isF,F); n \<in> nat; iterates_replacement(M,isF,v)|] 
    ==> wfrec_replacement(M, \<lambda>n f z. z = nat_case(v, \<lambda>m. F(f`m), n), 
                        Memrel(succ(n)))" 
@@ -148,7 +148,7 @@
       n \<in> nat; M(v); M(z); \<forall>x[M]. M(F(x)) |] 
    ==> is_iterates(M,isF,v,n,z) \<longleftrightarrow> z = iterates(F,n,v)" 
 apply (frule iterates_imp_wfrec_replacement, assumption+)
-apply (simp add: wf_Memrel trans_Memrel relation_Memrel nat_into_M
+apply (simp add: wf_Memrel trans_Memrel relation_Memrel 
                  is_iterates_def relation2_def iterates_MH_abs 
                  iterates_nat_def recursor_def transrec_def 
                  eclose_sing_Ord_eq nat_into_M
@@ -161,7 +161,7 @@
       n \<in> nat; M(v); \<forall>x[M]. M(F(x)) |] 
    ==> M(iterates(F,n,v))"
 apply (frule iterates_imp_wfrec_replacement, assumption+)
-apply (simp add: wf_Memrel trans_Memrel relation_Memrel nat_into_M
+apply (simp add: wf_Memrel trans_Memrel relation_Memrel 
                  relation2_def iterates_MH_abs 
                  iterates_nat_def recursor_def transrec_def 
                  eclose_sing_Ord_eq nat_into_M
@@ -270,7 +270,7 @@
           cartprod(M,X,X,XX) & is_sum(M,XX,X,X3) & 
           is_sum(M,natnatsum,X3,Z)"
 
-lemma (in M_basic) formula_functor_abs [simp]: 
+lemma (in M_trancl) formula_functor_abs [simp]: 
      "[| M(X); M(Z) |] 
       ==> is_formula_functor(M,X,Z) \<longleftrightarrow> 
           Z = ((nat*nat) + (nat*nat)) + (X*X + X)"
@@ -935,13 +935,13 @@
                          is_formula_case (M, is_a, is_b, is_c, is_d),
                          formula_rec_case(a, b, c, d, h))"
 apply (simp (no_asm) add: formula_rec_case_def Relation1_def)
-apply (simp add: formula_case_abs)
+apply (simp)
 done
 
 
 text\<open>This locale packages the premises of the following theorems,
       which is the normal purpose of locales.  It doesn't accumulate
-      constraints on the class \<^term>\<open>M\<close>, as in most of this deveopment.\<close>
+      constraints on the class \<^term>\<open>M\<close>, as in most of this development.\<close>
 locale Formula_Rec = M_eclose +
   fixes a and is_a and b and is_b and c and is_c and d and is_d and MH
   defines
diff -r 6a1c1d1ce6ae -r 89d05db6dd1f src/ZF/Constructible/Formula.thy
--- a/src/ZF/Constructible/Formula.thy	Tue Feb 04 16:36:49 2020 +0100
+++ b/src/ZF/Constructible/Formula.thy	Tue Feb 04 16:19:15 2020 +0000
@@ -162,32 +162,32 @@
 lemma conj_iff_sats:
       "[| P \<longleftrightarrow> sats(A,p,env); Q \<longleftrightarrow> sats(A,q,env); env \<in> list(A)|]
        ==> (P & Q) \<longleftrightarrow> sats(A, And(p,q), env)"
-by (simp add: sats_And_iff)
+by (simp)
 
 lemma disj_iff_sats:
       "[| P \<longleftrightarrow> sats(A,p,env); Q \<longleftrightarrow> sats(A,q,env); env \<in> list(A)|]
        ==> (P | Q) \<longleftrightarrow> sats(A, Or(p,q), env)"
-by (simp add: sats_Or_iff)
+by (simp)
 
 lemma iff_iff_sats:
       "[| P \<longleftrightarrow> sats(A,p,env); Q \<longleftrightarrow> sats(A,q,env); env \<in> list(A)|]
        ==> (P \<longleftrightarrow> Q) \<longleftrightarrow> sats(A, Iff(p,q), env)"
-by (simp add: sats_Forall_iff)
+by (simp)
 
 lemma imp_iff_sats:
       "[| P \<longleftrightarrow> sats(A,p,env); Q \<longleftrightarrow> sats(A,q,env); env \<in> list(A)|]
        ==> (P \<longrightarrow> Q) \<longleftrightarrow> sats(A, Implies(p,q), env)"
-by (simp add: sats_Forall_iff)
+by (simp)
 
 lemma ball_iff_sats:
       "[| !!x. x\<in>A ==> P(x) \<longleftrightarrow> sats(A, p, Cons(x, env)); env \<in> list(A)|]
        ==> (\<forall>x\<in>A. P(x)) \<longleftrightarrow> sats(A, Forall(p), env)"
-by (simp add: sats_Forall_iff)
+by (simp)
 
 lemma bex_iff_sats:
       "[| !!x. x\<in>A ==> P(x) \<longleftrightarrow> sats(A, p, Cons(x, env)); env \<in> list(A)|]
        ==> (\<exists>x\<in>A. P(x)) \<longleftrightarrow> sats(A, Exists(p), env)"
-by (simp add: sats_Exists_iff)
+by (simp)
 
 lemmas FOL_iff_sats =
         mem_iff_sats equal_iff_sats not_iff_sats conj_iff_sats
@@ -451,7 +451,7 @@
   apply typecheck
 apply (rule conjI)
 (*finally check the arity!*)
- apply (simp add: arity_iterates_incr_bv1_eq length_app Un_least_lt_iff)
+ apply (simp add: arity_iterates_incr_bv1_eq Un_least_lt_iff)
  apply (force intro: add_le_self le_trans)
 apply (simp add: arity_sats1_iff formula_add_params1, blast)
 done
diff -r 6a1c1d1ce6ae -r 89d05db6dd1f src/ZF/Constructible/Internalize.thy
--- a/src/ZF/Constructible/Internalize.thy	Tue Feb 04 16:36:49 2020 +0100
+++ b/src/ZF/Constructible/Internalize.thy	Tue Feb 04 16:19:15 2020 +0000
@@ -343,7 +343,7 @@
       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
           i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
        ==> is_Member(##A, x, y, z) \<longleftrightarrow> sats(A, Member_fm(i,j,k), env)"
-by (simp add: sats_Member_fm)
+by (simp)
 
 theorem Member_reflection:
      "REFLECTS[\<lambda>x. is_Member(L,f(x),g(x),h(x)),
@@ -376,7 +376,7 @@
       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
           i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
        ==> is_Equal(##A, x, y, z) \<longleftrightarrow> sats(A, Equal_fm(i,j,k), env)"
-by (simp add: sats_Equal_fm)
+by (simp)
 
 theorem Equal_reflection:
      "REFLECTS[\<lambda>x. is_Equal(L,f(x),g(x),h(x)),
@@ -409,7 +409,7 @@
       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
           i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
        ==> is_Nand(##A, x, y, z) \<longleftrightarrow> sats(A, Nand_fm(i,j,k), env)"
-by (simp add: sats_Nand_fm)
+by (simp)
 
 theorem Nand_reflection:
      "REFLECTS[\<lambda>x. is_Nand(L,f(x),g(x),h(x)),
@@ -440,7 +440,7 @@
       "[| nth(i,env) = x; nth(j,env) = y; 
           i \<in> nat; j \<in> nat; env \<in> list(A)|]
        ==> is_Forall(##A, x, y) \<longleftrightarrow> sats(A, Forall_fm(i,j), env)"
-by (simp add: sats_Forall_fm)
+by (simp)
 
 theorem Forall_reflection:
      "REFLECTS[\<lambda>x. is_Forall(L,f(x),g(x)),
@@ -737,7 +737,7 @@
       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
           i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
        ==> cartprod(##A, x, y, z) \<longleftrightarrow> sats(A, cartprod_fm(i,j,k), env)"
-by (simp add: sats_cartprod_fm)
+by (simp)
 
 theorem cartprod_reflection:
      "REFLECTS[\<lambda>x. cartprod(L,f(x),g(x),h(x)),
@@ -1043,7 +1043,7 @@
       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
           i \<in> nat; j < length(env); k < length(env); env \<in> list(A)|]
        ==> is_eclose_n(##A, x, y, z) \<longleftrightarrow> sats(A, eclose_n_fm(i,j,k), env)"
-by (simp add: sats_eclose_n_fm)
+by (simp)
 
 theorem eclose_n_reflection:
      "REFLECTS[\<lambda>x. is_eclose_n(L, f(x), g(x), h(x)),  
@@ -1186,7 +1186,7 @@
       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
           i \<in> nat; j < length(env); k < length(env); env \<in> list(A)|]
        ==> is_list_N(##A, x, y, z) \<longleftrightarrow> sats(A, list_N_fm(i,j,k), env)"
-by (simp add: sats_list_N_fm)
+by (simp)
 
 theorem list_N_reflection:
      "REFLECTS[\<lambda>x. is_list_N(L, f(x), g(x), h(x)),  
@@ -1336,7 +1336,7 @@
       "[| nth(i,env) = x; nth(j,env) = y; 
           i < length(env); j < length(env); env \<in> list(A)|]
        ==> is_formula_N(##A, x, y) \<longleftrightarrow> sats(A, formula_N_fm(i,j), env)"
-by (simp add: sats_formula_N_fm)
+by (simp)
 
 theorem formula_N_reflection:
      "REFLECTS[\<lambda>x. is_formula_N(L, f(x), g(x)),  
diff -r 6a1c1d1ce6ae -r 89d05db6dd1f src/ZF/Constructible/L_axioms.thy
--- a/src/ZF/Constructible/L_axioms.thy	Tue Feb 04 16:36:49 2020 +0100
+++ b/src/ZF/Constructible/L_axioms.thy	Tue Feb 04 16:19:15 2020 +0000
@@ -78,6 +78,17 @@
 apply (simp_all add: Replace_iff univalent_def, blast)
 done
 
+lemma strong_replacementI [rule_format]:
+    "[| \<forall>B[L]. separation(L, %u. \<exists>x[L]. x\<in>B & P(x,u)) |]
+     ==> strong_replacement(L,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
+
+
 subsection\<open>Instantiating the locale \<open>M_trivial\<close>\<close>
 text\<open>No instances of Separation yet.\<close>
 
@@ -89,14 +100,14 @@
 
 lemmas L_nat = Ord_in_L [OF Ord_nat]
 
-theorem M_trivial_L: "PROP M_trivial(L)"
+theorem M_trivial_L: "M_trivial(L)"
   apply (rule M_trivial.intro)
-       apply (erule (1) transL)
+  apply (rule M_trans.intro)
+    apply (erule (1) transL)
+   apply(rule exI,rule  nonempty)
+  apply (rule M_trivial_axioms.intro)
       apply (rule upair_ax)
-     apply (rule Union_ax)
-    apply (rule power_ax)
-   apply (rule replacement)
-  apply (rule L_nat)
+   apply (rule Union_ax)
   done
 
 interpretation L?: M_trivial L by (rule M_trivial_L)
@@ -352,7 +363,7 @@
       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
           i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
        ==> upair(##A, x, y, z) \<longleftrightarrow> sats(A, upair_fm(i,j,k), env)"
-by (simp add: sats_upair_fm)
+by (simp)
 
 text\<open>Useful? At least it refers to "real" unordered pairs\<close>
 lemma sats_upair_fm2 [simp]:
@@ -394,7 +405,7 @@
       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
           i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
        ==> pair(##A, x, y, z) \<longleftrightarrow> sats(A, pair_fm(i,j,k), env)"
-by (simp add: sats_pair_fm)
+by (simp)
 
 theorem pair_reflection:
      "REFLECTS[\<lambda>x. pair(L,f(x),g(x),h(x)),
@@ -426,7 +437,7 @@
       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
           i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
        ==> union(##A, x, y, z) \<longleftrightarrow> sats(A, union_fm(i,j,k), env)"
-by (simp add: sats_union_fm)
+by (simp)
 
 theorem union_reflection:
      "REFLECTS[\<lambda>x. union(L,f(x),g(x),h(x)),
@@ -671,7 +682,7 @@
       "[| nth(i,env) = U; nth(j,env) = x; nth(k,env) = r; nth(l,env) = B;
           i \<in> nat; j \<in> nat; k \<in> nat; l \<in> nat; env \<in> list(A)|]
        ==> pred_set(##A,U,x,r,B) \<longleftrightarrow> sats(A, pred_set_fm(i,j,k,l), env)"
-by (simp add: sats_pred_set_fm)
+by (simp)
 
 theorem pred_set_reflection:
      "REFLECTS[\<lambda>x. pred_set(L,f(x),g(x),h(x),b(x)),
@@ -815,7 +826,7 @@
       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
           i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
        ==> image(##A, x, y, z) \<longleftrightarrow> sats(A, image_fm(i,j,k), env)"
-by (simp add: sats_image_fm)
+by (simp)
 
 theorem image_reflection:
      "REFLECTS[\<lambda>x. image(L,f(x),g(x),h(x)),
@@ -851,7 +862,7 @@
       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
           i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
        ==> pre_image(##A, x, y, z) \<longleftrightarrow> sats(A, pre_image_fm(i,j,k), env)"
-by (simp add: sats_pre_image_fm)
+by (simp)
 
 theorem pre_image_reflection:
      "REFLECTS[\<lambda>x. pre_image(L,f(x),g(x),h(x)),
diff -r 6a1c1d1ce6ae -r 89d05db6dd1f src/ZF/Constructible/Normal.thy
--- a/src/ZF/Constructible/Normal.thy	Tue Feb 04 16:36:49 2020 +0100
+++ b/src/ZF/Constructible/Normal.thy	Tue Feb 04 16:19:15 2020 +0000
@@ -64,12 +64,12 @@
 apply (simp add: Closed_Unbounded_def Closed_def Unbounded_def Limit_Union, 
        clarify)
 apply (rule_tac x="i++nat" in exI)  
-apply (blast intro: oadd_lt_self oadd_LimitI Limit_nat Limit_has_0) 
+apply (blast intro: oadd_lt_self oadd_LimitI Limit_has_0) 
 done
 
 text\<open>The class of cardinals, \<^term>\<open>Card\<close>, is closed and unbounded.\<close>
 theorem Closed_Unbounded_Card  [simp]: "Closed_Unbounded(Card)"
-apply (simp add: Closed_Unbounded_def Closed_def Unbounded_def Card_Union)
+apply (simp add: Closed_Unbounded_def Closed_def Unbounded_def)
 apply (blast intro: lt_csucc Card_csucc)
 done
 
@@ -101,7 +101,7 @@
 
 lemma (in cub_family) Ord_next_greater:
      "Ord(next_greater(a,x))"
-by (simp add: next_greater_def Ord_Least)
+by (simp add: next_greater_def)
 
 text\<open>\<^term>\<open>next_greater\<close> works as expected: it returns a larger value
 and one that belongs to class \<^term>\<open>P(a)\<close>.\<close>
@@ -146,10 +146,10 @@
 @{subgoals[display,indent=0,margin=65]}
 \<close>
 apply (rule UN_least_le) 
-apply (blast intro: Ord_UN Ord_iterates Ord_sup_greater)  
+apply (blast intro: Ord_iterates Ord_sup_greater)  
 apply (rule_tac a="succ(n)" in UN_upper_le)
 apply (simp_all add: next_greater_le_sup_greater) 
-apply (blast intro: Ord_UN Ord_iterates Ord_sup_greater)  
+apply (blast intro: Ord_iterates Ord_sup_greater)  
 done
 
 lemma (in cub_family) P_omega_sup_greater:
@@ -166,7 +166,7 @@
 apply (simp add: iterates_omega_def)
 apply (rule UN_upper_lt [of 1], simp_all) 
  apply (blast intro: sup_greater_gt) 
-apply (blast intro: Ord_UN Ord_iterates Ord_sup_greater)
+apply (blast intro: Ord_iterates Ord_sup_greater)
 done
 
 lemma (in cub_family) Unbounded_INT: "Unbounded(\<lambda>x. \<forall>a\<in>A. P(a,x))"
@@ -299,7 +299,7 @@
  apply (simp add: mono_le_subset_def, blast intro: leI) 
 txt\<open>Second inclusion:\<close>
 apply (rule UN_least) 
-apply (frule Union_upper_le, blast, blast intro: Ord_Union)
+apply (frule Union_upper_le, blast, blast)
 apply (erule leE, drule ltD, elim UnionE)
  apply (simp add: OUnion_def)
  apply blast+
@@ -327,7 +327,7 @@
 
 lemma Ord_iterates_Normal:
      "[| n\<in>nat;  Normal(F);  Ord(x) |] ==> Ord(F^n (x))"  
-by (simp add: Ord_iterates) 
+by (simp) 
 
 text\<open>THIS RESULT IS UNUSED\<close>
 lemma iterates_omega_Limit:
@@ -337,7 +337,7 @@
 apply (rule increasing_LimitI) 
    \<comment> \<open>this lemma is @{thm increasing_LimitI [no_vars]}\<close>
  apply (blast intro: UN_upper_lt [of "1"]   Normal_imp_Ord
-                     Ord_UN Ord_iterates lt_imp_0_lt
+                     Ord_iterates lt_imp_0_lt
                      iterates_Normal_increasing, clarify)
 apply (rule bexI) 
  apply (blast intro: Ord_in_Ord [OF Ord_iterates_Normal]) 
diff -r 6a1c1d1ce6ae -r 89d05db6dd1f src/ZF/Constructible/Rank.thy
--- a/src/ZF/Constructible/Rank.thy	Tue Feb 04 16:36:49 2020 +0100
+++ b/src/ZF/Constructible/Rank.thy	Tue Feb 04 16:19:15 2020 +0000
@@ -109,7 +109,7 @@
    apply (blast intro: wellordered_subset [OF _ pred_subset]) 
   apply (simp add: trans_pred_pred_eq)
   apply (blast intro: Ord_iso_implies_eq ord_iso_sym ord_iso_trans) 
- apply (simp_all add: pred_iff pred_closed converse_closed comp_closed)
+ apply (simp_all add: pred_iff)
 txt\<open>case \<^term>\<open>j<i\<close> also yields a contradiction\<close>
 apply (frule restrict_ord_iso2, assumption+) 
 apply (frule ord_iso_sym [THEN ord_iso_is_bij, THEN bij_is_fun]) 
@@ -162,7 +162,7 @@
       ==> z \<in> f \<longleftrightarrow>
           (\<exists>a\<in>A. \<exists>x[M]. \<exists>g[M]. z = <a,x> & Ord(x) & 
                                 g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x)))"
-apply (simp add: omap_def Memrel_closed pred_closed) 
+apply (simp add: omap_def) 
 apply (rule iffI)
  apply (drule_tac [2] x=z in rspec)
  apply (drule_tac x=z in rspec)
@@ -222,7 +222,7 @@
 lemma (in M_ordertype) domain_omap:
      "[| omap(M,A,r,f);  M(A); M(r); M(B); M(f) |] 
       ==> domain(f) = obase(M,A,r)"
-apply (simp add: domain_closed obase_def) 
+apply (simp add: obase_def) 
 apply (rule equality_iffI) 
 apply (simp add: domain_iff omap_iff, blast) 
 done
@@ -354,16 +354,14 @@
 apply (simp add: strong_replacement_def) 
 apply (drule_tac x="obase(M,A,r)" in rspec) 
  apply (simp add: obase_exists) 
-apply (simp add: Memrel_closed pred_closed obase_def)
+apply (simp add: obase_def)
 apply (erule impE) 
  apply (clarsimp simp add: univalent_def)
  apply (blast intro: Ord_iso_implies_eq ord_iso_sym ord_iso_trans, clarify)  
 apply (rule_tac x=Y in rexI) 
-apply (simp add: Memrel_closed pred_closed obase_def, blast, assumption)
+apply (simp add: obase_def, blast, assumption)
 done
 
-declare rall_simps [simp] rex_simps [simp]
-
 lemma (in M_ordertype) otype_exists:
      "[| wellordered(M,A,r); M(A); M(r) |] ==> \<exists>i[M]. otype(M,A,r,i)"
 apply (insert omap_exists [of A r])  
@@ -379,7 +377,7 @@
 apply (rename_tac i) 
 apply (subgoal_tac "Ord(i)", blast intro: omap_ord_iso_otype)
 apply (rule Ord_otype) 
-    apply (force simp add: otype_def range_closed) 
+    apply (force simp add: otype_def) 
    apply (simp_all add: wellordered_is_trans_on) 
 done
 
@@ -484,9 +482,9 @@
     ==> is_oadd_fun(M,i,j,a,f) \<longleftrightarrow>
         f \<in> a \<rightarrow> range(f) & (\<forall>x. M(x) \<longrightarrow> x < a \<longrightarrow> f`x = i \<union> f``x)"
 apply (frule lt_Ord) 
-apply (simp add: is_oadd_fun_def Memrel_closed Un_closed 
+apply (simp add: is_oadd_fun_def  
              relation2_def is_recfun_abs [of "%x g. i \<union> g``x"]
-             image_closed is_recfun_iff_equation  
+             is_recfun_iff_equation  
              Ball_def lt_trans [OF ltI, of _ a] lt_Memrel)
 apply (simp add: lt_def) 
 apply (blast dest: transM) 
@@ -559,7 +557,7 @@
 apply (simp add: oadd_eq_if_raw_oadd, clarify) 
 apply (simp add: raw_oadd_eq_oadd) 
 apply (frule exists_oadd_fun [of j i], auto)
-apply (simp add: apply_closed is_oadd_fun_iff_oadd [symmetric]) 
+apply (simp add: is_oadd_fun_iff_oadd [symmetric]) 
 done
 
 
@@ -605,7 +603,7 @@
  prefer 2 apply (simp add: omult_eqns_Not) \<comment> \<open>trivial, non-Ord case\<close>
 apply (erule Ord_cases) 
   apply (simp add: omult_eqns_0)
- apply (simp add: omult_eqns_succ apply_closed oadd_closed) 
+ apply (simp add: omult_eqns_succ) 
 apply (simp add: omult_eqns_Limit) 
 done
 
@@ -642,7 +640,7 @@
 lemma (in M_ord_arith) is_omult_fun_apply_Limit:
     "[| x < j; Limit(x); M(j); M(f); is_omult_fun(M,i,j,f) |] 
      ==> f ` x = (\<Union>y\<in>x. f`y)"
-apply (simp add: is_omult_fun_def omult_eqns_def domain_closed lt_def, clarify)
+apply (simp add: is_omult_fun_def omult_eqns_def lt_def, clarify)
 apply (drule subset_trans [OF OrdmemD], assumption+)  
 apply (simp add: ball_conj_distrib omult_Limit image_function)
 done
@@ -905,7 +903,7 @@
     for  \<open>is_recfun\<close>.\<close>
 apply (rule_tac a=a in rangeI)
 apply (simp add: is_recfun_type [THEN apply_iff] vimage_singleton_iff
-                 r_into_trancl apply_recfun r_into_trancl)
+                 r_into_trancl apply_recfun)
 done
 
 
diff -r 6a1c1d1ce6ae -r 89d05db6dd1f src/ZF/Constructible/Rank_Separation.thy
--- a/src/ZF/Constructible/Rank_Separation.thy	Tue Feb 04 16:36:49 2020 +0100
+++ b/src/ZF/Constructible/Rank_Separation.thy	Tue Feb 04 16:19:15 2020 +0000
@@ -120,7 +120,7 @@
          omap_replacement)+
   done
 
-theorem M_ordertype_L: "PROP M_ordertype(L)"
+theorem M_ordertype_L: "M_ordertype(L)"
   apply (rule M_ordertype.intro)
    apply (rule M_basic_L)
   apply (rule M_ordertype_axioms_L) 
@@ -221,7 +221,7 @@
      wfrank_separation wfrank_strong_replacement Ord_wfrank_separation)+
   done
 
-theorem M_wfrank_L: "PROP M_wfrank(L)"
+theorem M_wfrank_L: "M_wfrank(L)"
   apply (rule M_wfrank.intro)
    apply (rule M_trancl_L)
   apply (rule M_wfrank_axioms_L) 
diff -r 6a1c1d1ce6ae -r 89d05db6dd1f src/ZF/Constructible/Rec_Separation.thy
--- a/src/ZF/Constructible/Rec_Separation.thy	Tue Feb 04 16:36:49 2020 +0100
+++ b/src/ZF/Constructible/Rec_Separation.thy	Tue Feb 04 16:19:15 2020 +0000
@@ -62,7 +62,7 @@
       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
           i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
        ==> rtran_closure_mem(##A, x, y, z) \<longleftrightarrow> sats(A, rtran_closure_mem_fm(i,j,k), env)"
-by (simp add: sats_rtran_closure_mem_fm)
+by (simp)
 
 lemma rtran_closure_mem_reflection:
      "REFLECTS[\<lambda>x. rtran_closure_mem(L,f(x),g(x),h(x)),
@@ -178,10 +178,10 @@
 
 lemma M_trancl_axioms_L: "M_trancl_axioms(L)"
   apply (rule M_trancl_axioms.intro)
-   apply (assumption | rule rtrancl_separation wellfounded_trancl_separation)+
+   apply (assumption | rule rtrancl_separation wellfounded_trancl_separation L_nat)+
   done
 
-theorem M_trancl_L: "PROP M_trancl(L)"
+theorem M_trancl_L: "M_trancl(L)"
 by (rule M_trancl.intro [OF M_basic_L M_trancl_axioms_L])
 
 interpretation L?: M_trancl L by (rule M_trancl_L)
@@ -209,7 +209,7 @@
 apply (rule strong_replacementI)
 apply (rule_tac u="{B,A,n,0,Memrel(succ(n))}" 
          in gen_separation_multi [OF list_replacement1_Reflects], 
-       auto simp add: nonempty)
+       auto)
 apply (rule_tac env="[B,A,n,0,Memrel(succ(n))]" in DPow_LsetI)
 apply (rule sep_rules is_nat_case_iff_sats list_functor_iff_sats
             is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
@@ -231,7 +231,7 @@
 apply (rule strong_replacementI)
 apply (rule_tac u="{A,B,0,nat}" 
          in gen_separation_multi [OF list_replacement2_Reflects], 
-       auto simp add: L_nat nonempty)
+       auto)
 apply (rule_tac env="[A,B,0,nat]" in DPow_LsetI)
 apply (rule sep_rules list_functor_iff_sats is_iterates_iff_sats | simp)+
 done
@@ -260,7 +260,7 @@
 apply (rule strong_replacementI)
 apply (rule_tac u="{B,n,0,Memrel(succ(n))}" 
          in gen_separation_multi [OF formula_replacement1_Reflects], 
-       auto simp add: nonempty)
+       auto)
 apply (rule_tac env="[n,B,0,Memrel(succ(n))]" in DPow_LsetI)
 apply (rule sep_rules is_nat_case_iff_sats formula_functor_iff_sats
             is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
@@ -281,7 +281,7 @@
 apply (rule strong_replacementI)
 apply (rule_tac u="{B,0,nat}" 
          in gen_separation_multi [OF formula_replacement2_Reflects], 
-       auto simp add: nonempty L_nat)
+       auto)
 apply (rule_tac env="[B,0,nat]" in DPow_LsetI)
 apply (rule sep_rules formula_functor_iff_sats is_iterates_iff_sats | simp)+
 done
@@ -316,7 +316,7 @@
       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
           i < length(env); j \<in> nat; k \<in> nat; env \<in> list(A)|]
        ==> is_nth(##A, x, y, z) \<longleftrightarrow> sats(A, nth_fm(i,j,k), env)"
-by (simp add: sats_nth_fm)
+by (simp)
 
 theorem nth_reflection:
      "REFLECTS[\<lambda>x. is_nth(L, f(x), g(x), h(x)),  
@@ -365,7 +365,7 @@
         nth_replacement)+
   done
 
-theorem M_datatypes_L: "PROP M_datatypes(L)"
+theorem M_datatypes_L: "M_datatypes(L)"
   apply (rule M_datatypes.intro)
    apply (rule M_trancl_L)
   apply (rule M_datatypes_axioms_L) 
@@ -415,7 +415,7 @@
 apply (rule strong_replacementI)
 apply (rule_tac u="{A,B,nat}" 
          in gen_separation_multi [OF eclose_replacement2_Reflects],
-       auto simp add: L_nat)
+       auto)
 apply (rule_tac env="[A,B,nat]" in DPow_LsetI)
 apply (rule sep_rules is_iterates_iff_sats big_union_iff_sats | simp)+
 done
@@ -428,7 +428,7 @@
    apply (assumption | rule eclose_replacement1 eclose_replacement2)+
   done
 
-theorem M_eclose_L: "PROP M_eclose(L)"
+theorem M_eclose_L: "M_eclose(L)"
   apply (rule M_eclose.intro)
    apply (rule M_datatypes_L)
   apply (rule M_eclose_axioms_L)
diff -r 6a1c1d1ce6ae -r 89d05db6dd1f src/ZF/Constructible/Reflection.thy
--- a/src/ZF/Constructible/Reflection.thy	Tue Feb 04 16:36:49 2020 +0100
+++ b/src/ZF/Constructible/Reflection.thy	Tue Feb 04 16:19:15 2020 +0000
@@ -121,7 +121,7 @@
      "[| M(z); y\<in>Mset(a); P(<y,z>); Ord(a) |] ==> \<exists>z\<in>Mset(FF(P,a)). P(<y,z>)"
 apply (simp add: FF_def)
 apply (simp_all add: cont_Ord_Union [of concl: Mset]
-                     Mset_cont Mset_mono_le not_emptyI Ord_F0)
+                     Mset_cont Mset_mono_le not_emptyI)
 apply (blast intro: F0_works)
 done
 
diff -r 6a1c1d1ce6ae -r 89d05db6dd1f src/ZF/Constructible/Relative.thy
--- a/src/ZF/Constructible/Relative.thy	Tue Feb 04 16:36:49 2020 +0100
+++ b/src/ZF/Constructible/Relative.thy	Tue Feb 04 16:19:15 2020 +0000
@@ -1,5 +1,7 @@
 (*  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>
@@ -404,7 +406,7 @@
 
 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)
@@ -430,7 +432,7 @@
 
 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))"
@@ -522,32 +524,52 @@
 
 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)
@@ -556,56 +578,76 @@
       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) 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_M_iff [iff]:
+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)
+  by blast
 
-lemma (in M_trivial) pair_abs [simp]:
+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]:
-     "M(<a,b>) \<longleftrightarrow> M(a) & M(b)"
-by (simp add: Pair_def)
+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_components_in_M:
+lemma (in M_trivial) pair_in_M_iff [simp]:
+     "M(<a,b>) \<longleftrightarrow> M(a) & M(b)"
+  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"
@@ -617,29 +659,25 @@
 
 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
+  unfolding union_def
+  by (blast intro: transM )
 
-lemma (in M_trivial) inter_abs [simp]:
+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
+  unfolding inter_def
+  by (blast intro: transM)
 
-lemma (in M_trivial) setdiff_abs [simp]:
+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
+  unfolding setdiff_def
+  by (blast intro: transM)
 
-lemma (in M_trivial) Union_abs [simp]:
+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))"
@@ -661,15 +699,23 @@
      "[| 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)
@@ -681,22 +727,10 @@
      "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>
 
@@ -709,16 +743,15 @@
           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)
@@ -730,7 +763,7 @@
 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)"
@@ -749,7 +782,7 @@
   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)
@@ -760,7 +793,7 @@
 
 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)
@@ -809,35 +842,60 @@
           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)
@@ -873,15 +931,15 @@
 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)
 
@@ -999,8 +1057,9 @@
                 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))"
+     and power_ax:         "power_ax(M)"
 
-lemma (in M_basic) cartprod_iff_lemma:
+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}}}"
@@ -1125,7 +1184,7 @@
 
 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)
@@ -1136,7 +1195,7 @@
 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)
@@ -1149,22 +1208,22 @@
 
 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)
@@ -1180,7 +1239,7 @@
 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)+
@@ -1188,7 +1247,7 @@
 
 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
 
@@ -1242,7 +1301,7 @@
 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)
@@ -1250,7 +1309,7 @@
 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)
 
@@ -1260,7 +1319,7 @@
 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)
@@ -1296,12 +1355,11 @@
      "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))"
@@ -1327,7 +1385,7 @@
       ==> 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
 
 
@@ -1335,7 +1393,7 @@
 
 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)
diff -r 6a1c1d1ce6ae -r 89d05db6dd1f src/ZF/Constructible/Satisfies_absolute.thy
--- a/src/ZF/Constructible/Satisfies_absolute.thy	Tue Feb 04 16:36:49 2020 +0100
+++ b/src/ZF/Constructible/Satisfies_absolute.thy	Tue Feb 04 16:19:15 2020 +0000
@@ -41,7 +41,7 @@
       "[| nth(i,env) = x; nth(j,env) = y; 
           i \<in> nat; j < length(env); env \<in> list(A)|]
        ==> is_depth(##A, x, y) \<longleftrightarrow> sats(A, depth_fm(i,j), env)"
-by (simp add: sats_depth_fm)
+by (simp)
 
 theorem depth_reflection:
      "REFLECTS[\<lambda>x. is_depth(L, f(x), g(x)),  
@@ -443,7 +443,7 @@
                          g ` succ(depth(u)) ` u, g ` succ(depth(v)) ` v),
        \<lambda>u. satisfies_d (A, u, g ` succ(depth(u)) ` u),
        x))"
-by (blast intro: formula_case_closed a_closed b_closed c_closed d_closed) 
+by (blast intro: a_closed b_closed c_closed d_closed) 
 
 lemma (in M_satisfies) fr_lam_replace:
    "[|M(g); M(A)|] ==>
@@ -479,7 +479,7 @@
 
 theorem (in M_satisfies) Formula_Rec_M: 
     "M(A) ==>
-     PROP Formula_Rec(M, satisfies_a(A), satisfies_is_a(M,A), 
+     Formula_Rec(M, satisfies_a(A), satisfies_is_a(M,A), 
                          satisfies_b(A), satisfies_is_b(M,A), 
                          satisfies_c(A), satisfies_is_c(M,A), 
                          satisfies_d(A), satisfies_is_d(M,A))"
@@ -842,7 +842,7 @@
 apply (rule strong_replacementI)
 apply (rule_tac u="{list(A),B,x,y}" 
          in gen_separation_multi [OF Member_Reflects], 
-       auto simp add: nat_into_M list_closed)
+       auto)
 apply (rule_tac env="[list(A),B,x,y]" in DPow_LsetI)
 apply (rule sep_rules nth_iff_sats is_bool_of_o_iff_sats | simp)+
 done
@@ -872,7 +872,7 @@
 apply (rule strong_replacementI)
 apply (rule_tac u="{list(A),B,x,y}" 
          in gen_separation_multi [OF Equal_Reflects], 
-       auto simp add: nat_into_M list_closed)
+       auto)
 apply (rule_tac env="[list(A),B,x,y]" in DPow_LsetI)
 apply (rule sep_rules nth_iff_sats is_bool_of_o_iff_sats | simp)+
 done
@@ -904,7 +904,7 @@
 apply (rule strong_replacementI)
 apply (rule_tac u="{list(A),B,rp,rq}" 
          in gen_separation_multi [OF Nand_Reflects],
-       auto simp add: list_closed)
+       auto)
 apply (rule_tac env="[list(A),B,rp,rq]" in DPow_LsetI)
 apply (rule sep_rules is_and_iff_sats is_not_iff_sats | simp)+
 done
@@ -943,7 +943,7 @@
 apply (rule strong_replacementI)
 apply (rule_tac u="{A,list(A),B,rp}" 
          in gen_separation_multi [OF Forall_Reflects],
-       auto simp add: list_closed)
+       auto)
 apply (rule_tac env="[A,list(A),B,rp]" in DPow_LsetI)
 apply (rule sep_rules is_bool_of_o_iff_sats Cons_iff_sats | simp)+
 done
@@ -1026,7 +1026,7 @@
          formula_rec_replacement formula_rec_lambda_replacement)+
   done
 
-theorem M_satisfies_L: "PROP M_satisfies(L)"
+theorem M_satisfies_L: "M_satisfies(L)"
   apply (rule M_satisfies.intro)
    apply (rule M_eclose_L)
   apply (rule M_satisfies_axioms_L)
diff -r 6a1c1d1ce6ae -r 89d05db6dd1f src/ZF/Constructible/Separation.thy
--- a/src/ZF/Constructible/Separation.thy	Tue Feb 04 16:36:49 2020 +0100
+++ b/src/ZF/Constructible/Separation.thy	Tue Feb 04 16:19:15 2020 +0000
@@ -298,10 +298,10 @@
          Inter_separation Diff_separation cartprod_separation image_separation
          converse_separation restrict_separation
          comp_separation pred_separation Memrel_separation
-         funspace_succ_replacement is_recfun_separation)+
+         funspace_succ_replacement is_recfun_separation power_ax)+
   done
 
-theorem M_basic_L: "PROP M_basic(L)"
+theorem M_basic_L: " M_basic(L)"
 by (rule M_basic.intro [OF M_trivial_L M_basic_axioms_L])
 
 interpretation L?: M_basic L by (rule M_basic_L)
diff -r 6a1c1d1ce6ae -r 89d05db6dd1f src/ZF/Constructible/WF_absolute.thy
--- a/src/ZF/Constructible/WF_absolute.thy	Tue Feb 04 16:36:49 2020 +0100
+++ b/src/ZF/Constructible/WF_absolute.thy	Tue Feb 04 16:19:15 2020 +0000
@@ -82,17 +82,7 @@
   tran_closure :: "[i=>o,i,i] => o" where
     "tran_closure(M,r,t) ==
          \<exists>s[M]. rtran_closure(M,r,s) & composition(M,r,s,t)"
-
-lemma (in M_basic) rtran_closure_mem_iff:
-     "[|M(A); M(r); M(p)|]
-      ==> rtran_closure_mem(M,A,r,p) \<longleftrightarrow>
-          (\<exists>n[M]. n\<in>nat & 
-           (\<exists>f[M]. f \<in> succ(n) -> A &
-            (\<exists>x[M]. \<exists>y[M]. p = <x,y> & f`0 = x & f`n = y) &
-                           (\<forall>i\<in>n. <f`i, f`succ(i)> \<in> r)))"
-by (simp add: rtran_closure_mem_def Ord_succ_mem_iff nat_0_le [THEN ltD]) 
-
-
+    
 locale M_trancl = M_basic +
   assumes rtrancl_separation:
          "[| M(r); M(A) |] ==> separation (M, rtran_closure_mem(M,A,r))"
@@ -101,7 +91,17 @@
           separation (M, \<lambda>x. 
               \<exists>w[M]. \<exists>wx[M]. \<exists>rp[M]. 
                w \<in> Z & pair(M,w,x,wx) & tran_closure(M,r,rp) & wx \<in> rp)"
+      and M_nat [iff] : "M(nat)"
 
+lemma (in M_trancl) rtran_closure_mem_iff:
+     "[|M(A); M(r); M(p)|]
+      ==> rtran_closure_mem(M,A,r,p) \<longleftrightarrow>
+          (\<exists>n[M]. n\<in>nat & 
+           (\<exists>f[M]. f \<in> succ(n) -> A &
+            (\<exists>x[M]. \<exists>y[M]. p = <x,y> & f`0 = x & f`n = y) &
+                           (\<forall>i\<in>n. <f`i, f`succ(i)> \<in> r)))"
+  apply (simp add: rtran_closure_mem_def Ord_succ_mem_iff nat_0_le [THEN ltD]) 
+done
 
 lemma (in M_trancl) rtran_closure_rtrancl:
      "M(r) ==> rtran_closure(M,r,rtrancl(r))"
@@ -130,7 +130,7 @@
 
 lemma (in M_trancl) trancl_closed [intro,simp]:
      "M(r) ==> M(trancl(r))"
-by (simp add: trancl_def comp_closed rtrancl_closed)
+by (simp add: trancl_def)
 
 lemma (in M_trancl) trancl_abs [simp]:
      "[| M(r); M(z) |] ==> tran_closure(M,r,z) \<longleftrightarrow> z = trancl(r)"
@@ -144,7 +144,7 @@
       relativized version.  Original version is on theory WF.\<close>
 lemma "[| wf[A](r);  r-``A \<subseteq> A |] ==> wf[A](r^+)"
 apply (simp add: wf_on_def wf_def)
-apply (safe intro!: equalityI)
+apply (safe)
 apply (drule_tac x = "{x\<in>A. \<exists>w. \<langle>w,x\<rangle> \<in> r^+ & w \<in> Z}" in spec)
 apply (blast elim: tranclE)
 done
diff -r 6a1c1d1ce6ae -r 89d05db6dd1f src/ZF/Constructible/Wellorderings.thy
--- a/src/ZF/Constructible/Wellorderings.thy	Tue Feb 04 16:36:49 2020 +0100
+++ b/src/ZF/Constructible/Wellorderings.thy	Tue Feb 04 16:19:15 2020 +0000
@@ -162,7 +162,7 @@
 lemma (in M_basic) order_isomorphism_abs [simp]: 
      "[| M(A); M(B); M(f) |] 
       ==> order_isomorphism(M,A,r,B,s,f) \<longleftrightarrow> f \<in> ord_iso(A,r,B,s)"
-by (simp add: apply_closed order_isomorphism_def ord_iso_def)
+by (simp add: order_isomorphism_def ord_iso_def)
 
 lemma (in M_basic) pred_set_abs [simp]: 
      "[| M(r); M(B) |] ==> pred_set(M,A,x,r,B) \<longleftrightarrow> B = Order.pred(A,x,r)"