renamed M_triv_axioms to M_trivial and M_axioms to M_basic
authorpaulson
Tue Sep 10 16:51:31 2002 +0200 (2002-09-10)
changeset 135641500a2e48d44
parent 13563 7d6c9817c432
child 13565 40e4755e57f7
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
src/ZF/Constructible/Datatype_absolute.thy
src/ZF/Constructible/L_axioms.thy
src/ZF/Constructible/Rec_Separation.thy
src/ZF/Constructible/Relative.thy
src/ZF/Constructible/Separation.thy
src/ZF/Constructible/WF_absolute.thy
src/ZF/Constructible/WFrec.thy
src/ZF/Constructible/Wellorderings.thy
     1.1 --- a/src/ZF/Constructible/Datatype_absolute.thy	Tue Sep 10 16:47:17 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Datatype_absolute.thy	Tue Sep 10 16:51:31 2002 +0200
     1.3 @@ -126,13 +126,13 @@
     1.4        \<forall>n[M]. n\<in>nat --> 
     1.5           wfrec_replacement(M, iterates_MH(M,isF,v), Memrel(succ(n)))"
     1.6  
     1.7 -lemma (in M_axioms) iterates_MH_abs:
     1.8 +lemma (in M_basic) iterates_MH_abs:
     1.9    "[| relativize1(M,isF,F); M(n); M(g); M(z) |] 
    1.10     ==> iterates_MH(M,isF,v,n,g,z) <-> z = nat_case(v, \<lambda>m. F(g`m), n)"
    1.11  by (simp add: nat_case_abs [of _ "\<lambda>m. F(g ` m)"]
    1.12                relativize1_def iterates_MH_def)  
    1.13  
    1.14 -lemma (in M_axioms) iterates_imp_wfrec_replacement:
    1.15 +lemma (in M_basic) iterates_imp_wfrec_replacement:
    1.16    "[|relativize1(M,isF,F); n \<in> nat; iterates_replacement(M,isF,v)|] 
    1.17     ==> wfrec_replacement(M, \<lambda>n f z. z = nat_case(v, \<lambda>m. F(f`m), n), 
    1.18                         Memrel(succ(n)))" 
    1.19 @@ -210,7 +210,7 @@
    1.20          \<exists>n1[M]. \<exists>AX[M]. 
    1.21           number1(M,n1) & cartprod(M,A,X,AX) & is_sum(M,n1,AX,Z)"
    1.22  
    1.23 -lemma (in M_axioms) list_functor_abs [simp]: 
    1.24 +lemma (in M_basic) list_functor_abs [simp]: 
    1.25       "[| M(A); M(X); M(Z) |] ==> is_list_functor(M,A,X,Z) <-> (Z = {0} + A*X)"
    1.26  by (simp add: is_list_functor_def singleton_0 nat_into_M)
    1.27  
    1.28 @@ -266,7 +266,7 @@
    1.29            cartprod(M,X,X,XX) & is_sum(M,XX,X,X3) & 
    1.30            is_sum(M,natnatsum,X3,Z)"
    1.31  
    1.32 -lemma (in M_axioms) formula_functor_abs [simp]: 
    1.33 +lemma (in M_basic) formula_functor_abs [simp]: 
    1.34       "[| M(X); M(Z) |] 
    1.35        ==> is_formula_functor(M,X,Z) <-> 
    1.36            Z = ((nat*nat) + (nat*nat)) + (X*X + X)"
    1.37 @@ -323,7 +323,7 @@
    1.38    
    1.39  text{*Express @{term list_rec} without using @{term rank} or @{term Vset},
    1.40  neither of which is absolute.*}
    1.41 -lemma (in M_triv_axioms) list_rec_eq:
    1.42 +lemma (in M_trivial) list_rec_eq:
    1.43    "l \<in> list(A) ==>
    1.44     list_rec(a,g,l) = 
    1.45     transrec (succ(length(l)),
    1.46 @@ -728,7 +728,7 @@
    1.47  done
    1.48  
    1.49  text{*Proof is trivial since @{term length} returns natural numbers.*}
    1.50 -lemma (in M_triv_axioms) length_closed [intro,simp]:
    1.51 +lemma (in M_trivial) length_closed [intro,simp]:
    1.52       "l \<in> list(A) ==> M(length(l))"
    1.53  by (simp add: nat_into_M) 
    1.54  
    1.55 @@ -744,7 +744,7 @@
    1.56  apply (simp add: tl'_Cons iterates_commute) 
    1.57  done
    1.58  
    1.59 -lemma (in M_axioms) iterates_tl'_closed:
    1.60 +lemma (in M_basic) iterates_tl'_closed:
    1.61       "[|n \<in> nat; M(x)|] ==> M(tl'^n (x))"
    1.62  apply (induct_tac n, simp) 
    1.63  apply (simp add: tl'_Cons tl'_closed) 
    1.64 @@ -785,11 +785,11 @@
    1.65      "is_Member(M,x,y,Z) ==
    1.66  	\<exists>p[M]. \<exists>u[M]. pair(M,x,y,p) & is_Inl(M,p,u) & is_Inl(M,u,Z)"
    1.67  
    1.68 -lemma (in M_triv_axioms) Member_abs [simp]:
    1.69 +lemma (in M_trivial) Member_abs [simp]:
    1.70       "[|M(x); M(y); M(Z)|] ==> is_Member(M,x,y,Z) <-> (Z = Member(x,y))"
    1.71  by (simp add: is_Member_def Member_def)
    1.72  
    1.73 -lemma (in M_triv_axioms) Member_in_M_iff [iff]:
    1.74 +lemma (in M_trivial) Member_in_M_iff [iff]:
    1.75       "M(Member(x,y)) <-> M(x) & M(y)"
    1.76  by (simp add: Member_def) 
    1.77  
    1.78 @@ -799,11 +799,11 @@
    1.79      "is_Equal(M,x,y,Z) ==
    1.80  	\<exists>p[M]. \<exists>u[M]. pair(M,x,y,p) & is_Inr(M,p,u) & is_Inl(M,u,Z)"
    1.81  
    1.82 -lemma (in M_triv_axioms) Equal_abs [simp]:
    1.83 +lemma (in M_trivial) Equal_abs [simp]:
    1.84       "[|M(x); M(y); M(Z)|] ==> is_Equal(M,x,y,Z) <-> (Z = Equal(x,y))"
    1.85  by (simp add: is_Equal_def Equal_def)
    1.86  
    1.87 -lemma (in M_triv_axioms) Equal_in_M_iff [iff]: "M(Equal(x,y)) <-> M(x) & M(y)"
    1.88 +lemma (in M_trivial) Equal_in_M_iff [iff]: "M(Equal(x,y)) <-> M(x) & M(y)"
    1.89  by (simp add: Equal_def) 
    1.90  
    1.91  constdefs
    1.92 @@ -812,11 +812,11 @@
    1.93      "is_Nand(M,x,y,Z) ==
    1.94  	\<exists>p[M]. \<exists>u[M]. pair(M,x,y,p) & is_Inl(M,p,u) & is_Inr(M,u,Z)"
    1.95  
    1.96 -lemma (in M_triv_axioms) Nand_abs [simp]:
    1.97 +lemma (in M_trivial) Nand_abs [simp]:
    1.98       "[|M(x); M(y); M(Z)|] ==> is_Nand(M,x,y,Z) <-> (Z = Nand(x,y))"
    1.99  by (simp add: is_Nand_def Nand_def)
   1.100  
   1.101 -lemma (in M_triv_axioms) Nand_in_M_iff [iff]: "M(Nand(x,y)) <-> M(x) & M(y)"
   1.102 +lemma (in M_trivial) Nand_in_M_iff [iff]: "M(Nand(x,y)) <-> M(x) & M(y)"
   1.103  by (simp add: Nand_def) 
   1.104  
   1.105  constdefs
   1.106 @@ -824,11 +824,11 @@
   1.107       --{* because @{term "Forall(x) \<equiv> Inr(Inr(p))"}*}
   1.108      "is_Forall(M,p,Z) == \<exists>u[M]. is_Inr(M,p,u) & is_Inr(M,u,Z)"
   1.109  
   1.110 -lemma (in M_triv_axioms) Forall_abs [simp]:
   1.111 +lemma (in M_trivial) Forall_abs [simp]:
   1.112       "[|M(x); M(Z)|] ==> is_Forall(M,x,Z) <-> (Z = Forall(x))"
   1.113  by (simp add: is_Forall_def Forall_def)
   1.114  
   1.115 -lemma (in M_triv_axioms) Forall_in_M_iff [iff]: "M(Forall(x)) <-> M(x)"
   1.116 +lemma (in M_trivial) Forall_in_M_iff [iff]: "M(Forall(x)) <-> M(x)"
   1.117  by (simp add: Forall_def)
   1.118  
   1.119  
   1.120 @@ -890,7 +890,7 @@
   1.121  done
   1.122  
   1.123  text{*Proof is trivial since @{term depth} returns natural numbers.*}
   1.124 -lemma (in M_triv_axioms) depth_closed [intro,simp]:
   1.125 +lemma (in M_trivial) depth_closed [intro,simp]:
   1.126       "p \<in> formula ==> M(depth(p))"
   1.127  by (simp add: nat_into_M) 
   1.128  
   1.129 @@ -916,7 +916,7 @@
   1.130  text{*Unfold @{term formula_rec} to @{term formula_rec_case}.
   1.131       Express @{term formula_rec} without using @{term rank} or @{term Vset},
   1.132  neither of which is absolute.*}
   1.133 -lemma (in M_triv_axioms) formula_rec_eq:
   1.134 +lemma (in M_trivial) formula_rec_eq:
   1.135    "p \<in> formula ==>
   1.136     formula_rec(a,b,c,d,p) = 
   1.137     transrec (succ(depth(p)),
     2.1 --- a/src/ZF/Constructible/L_axioms.thy	Tue Sep 10 16:47:17 2002 +0200
     2.2 +++ b/src/ZF/Constructible/L_axioms.thy	Tue Sep 10 16:51:31 2002 +0200
     2.3 @@ -8,7 +8,7 @@
     2.4  
     2.5  theory L_axioms = Formula + Relative + Reflection + MetaExists:
     2.6  
     2.7 -text {* The class L satisfies the premises of locale @{text M_triv_axioms} *}
     2.8 +text {* The class L satisfies the premises of locale @{text M_trivial} *}
     2.9  
    2.10  lemma transL: "[| y\<in>x; L(x) |] ==> L(y)"
    2.11  apply (insert Transset_Lset)
    2.12 @@ -80,7 +80,7 @@
    2.13  apply (simp_all add: Replace_iff univalent_def, blast)
    2.14  done
    2.15  
    2.16 -subsection{*Instantiating the locale @{text M_triv_axioms}*}
    2.17 +subsection{*Instantiating the locale @{text M_trivial}*}
    2.18  text{*No instances of Separation yet.*}
    2.19  
    2.20  lemma Lset_mono_le: "mono_le_subset(Lset)"
    2.21 @@ -93,8 +93,8 @@
    2.22  
    2.23  lemmas L_nat = Ord_in_L [OF Ord_nat]
    2.24  
    2.25 -theorem M_triv_axioms_L: "PROP M_triv_axioms(L)"
    2.26 -  apply (rule M_triv_axioms.intro)
    2.27 +theorem M_trivial_L: "PROP M_trivial(L)"
    2.28 +  apply (rule M_trivial.intro)
    2.29          apply (erule (1) transL)
    2.30         apply (rule nonempty)
    2.31        apply (rule upair_ax)
    2.32 @@ -104,50 +104,50 @@
    2.33    apply (rule L_nat)
    2.34    done
    2.35  
    2.36 -lemmas rall_abs = M_triv_axioms.rall_abs [OF M_triv_axioms_L]
    2.37 -  and rex_abs = M_triv_axioms.rex_abs [OF M_triv_axioms_L]
    2.38 -  and ball_iff_equiv = M_triv_axioms.ball_iff_equiv [OF M_triv_axioms_L]
    2.39 -  and M_equalityI = M_triv_axioms.M_equalityI [OF M_triv_axioms_L]
    2.40 -  and empty_abs = M_triv_axioms.empty_abs [OF M_triv_axioms_L]
    2.41 -  and subset_abs = M_triv_axioms.subset_abs [OF M_triv_axioms_L]
    2.42 -  and upair_abs = M_triv_axioms.upair_abs [OF M_triv_axioms_L]
    2.43 -  and upair_in_M_iff = M_triv_axioms.upair_in_M_iff [OF M_triv_axioms_L]
    2.44 -  and singleton_in_M_iff = M_triv_axioms.singleton_in_M_iff [OF M_triv_axioms_L]
    2.45 -  and pair_abs = M_triv_axioms.pair_abs [OF M_triv_axioms_L]
    2.46 -  and pair_in_M_iff = M_triv_axioms.pair_in_M_iff [OF M_triv_axioms_L]
    2.47 -  and pair_components_in_M = M_triv_axioms.pair_components_in_M [OF M_triv_axioms_L]
    2.48 -  and cartprod_abs = M_triv_axioms.cartprod_abs [OF M_triv_axioms_L]
    2.49 -  and union_abs = M_triv_axioms.union_abs [OF M_triv_axioms_L]
    2.50 -  and inter_abs = M_triv_axioms.inter_abs [OF M_triv_axioms_L]
    2.51 -  and setdiff_abs = M_triv_axioms.setdiff_abs [OF M_triv_axioms_L]
    2.52 -  and Union_abs = M_triv_axioms.Union_abs [OF M_triv_axioms_L]
    2.53 -  and Union_closed = M_triv_axioms.Union_closed [OF M_triv_axioms_L]
    2.54 -  and Un_closed = M_triv_axioms.Un_closed [OF M_triv_axioms_L]
    2.55 -  and cons_closed = M_triv_axioms.cons_closed [OF M_triv_axioms_L]
    2.56 -  and successor_abs = M_triv_axioms.successor_abs [OF M_triv_axioms_L]
    2.57 -  and succ_in_M_iff = M_triv_axioms.succ_in_M_iff [OF M_triv_axioms_L]
    2.58 -  and separation_closed = M_triv_axioms.separation_closed [OF M_triv_axioms_L]
    2.59 -  and strong_replacementI = M_triv_axioms.strong_replacementI [OF M_triv_axioms_L]
    2.60 -  and strong_replacement_closed = M_triv_axioms.strong_replacement_closed [OF M_triv_axioms_L]
    2.61 -  and RepFun_closed = M_triv_axioms.RepFun_closed [OF M_triv_axioms_L]
    2.62 -  and lam_closed = M_triv_axioms.lam_closed [OF M_triv_axioms_L]
    2.63 -  and image_abs = M_triv_axioms.image_abs [OF M_triv_axioms_L]
    2.64 -  and powerset_Pow = M_triv_axioms.powerset_Pow [OF M_triv_axioms_L]
    2.65 -  and powerset_imp_subset_Pow = M_triv_axioms.powerset_imp_subset_Pow [OF M_triv_axioms_L]
    2.66 -  and nat_into_M = M_triv_axioms.nat_into_M [OF M_triv_axioms_L]
    2.67 -  and nat_case_closed = M_triv_axioms.nat_case_closed [OF M_triv_axioms_L]
    2.68 -  and Inl_in_M_iff = M_triv_axioms.Inl_in_M_iff [OF M_triv_axioms_L]
    2.69 -  and Inr_in_M_iff = M_triv_axioms.Inr_in_M_iff [OF M_triv_axioms_L]
    2.70 -  and lt_closed = M_triv_axioms.lt_closed [OF M_triv_axioms_L]
    2.71 -  and transitive_set_abs = M_triv_axioms.transitive_set_abs [OF M_triv_axioms_L]
    2.72 -  and ordinal_abs = M_triv_axioms.ordinal_abs [OF M_triv_axioms_L]
    2.73 -  and limit_ordinal_abs = M_triv_axioms.limit_ordinal_abs [OF M_triv_axioms_L]
    2.74 -  and successor_ordinal_abs = M_triv_axioms.successor_ordinal_abs [OF M_triv_axioms_L]
    2.75 -  and finite_ordinal_abs = M_triv_axioms.finite_ordinal_abs [OF M_triv_axioms_L]
    2.76 -  and omega_abs = M_triv_axioms.omega_abs [OF M_triv_axioms_L]
    2.77 -  and number1_abs = M_triv_axioms.number1_abs [OF M_triv_axioms_L]
    2.78 -  and number2_abs = M_triv_axioms.number2_abs [OF M_triv_axioms_L]
    2.79 -  and number3_abs = M_triv_axioms.number3_abs [OF M_triv_axioms_L]
    2.80 +lemmas rall_abs = M_trivial.rall_abs [OF M_trivial_L]
    2.81 +  and rex_abs = M_trivial.rex_abs [OF M_trivial_L]
    2.82 +  and ball_iff_equiv = M_trivial.ball_iff_equiv [OF M_trivial_L]
    2.83 +  and M_equalityI = M_trivial.M_equalityI [OF M_trivial_L]
    2.84 +  and empty_abs = M_trivial.empty_abs [OF M_trivial_L]
    2.85 +  and subset_abs = M_trivial.subset_abs [OF M_trivial_L]
    2.86 +  and upair_abs = M_trivial.upair_abs [OF M_trivial_L]
    2.87 +  and upair_in_M_iff = M_trivial.upair_in_M_iff [OF M_trivial_L]
    2.88 +  and singleton_in_M_iff = M_trivial.singleton_in_M_iff [OF M_trivial_L]
    2.89 +  and pair_abs = M_trivial.pair_abs [OF M_trivial_L]
    2.90 +  and pair_in_M_iff = M_trivial.pair_in_M_iff [OF M_trivial_L]
    2.91 +  and pair_components_in_M = M_trivial.pair_components_in_M [OF M_trivial_L]
    2.92 +  and cartprod_abs = M_trivial.cartprod_abs [OF M_trivial_L]
    2.93 +  and union_abs = M_trivial.union_abs [OF M_trivial_L]
    2.94 +  and inter_abs = M_trivial.inter_abs [OF M_trivial_L]
    2.95 +  and setdiff_abs = M_trivial.setdiff_abs [OF M_trivial_L]
    2.96 +  and Union_abs = M_trivial.Union_abs [OF M_trivial_L]
    2.97 +  and Union_closed = M_trivial.Union_closed [OF M_trivial_L]
    2.98 +  and Un_closed = M_trivial.Un_closed [OF M_trivial_L]
    2.99 +  and cons_closed = M_trivial.cons_closed [OF M_trivial_L]
   2.100 +  and successor_abs = M_trivial.successor_abs [OF M_trivial_L]
   2.101 +  and succ_in_M_iff = M_trivial.succ_in_M_iff [OF M_trivial_L]
   2.102 +  and separation_closed = M_trivial.separation_closed [OF M_trivial_L]
   2.103 +  and strong_replacementI = M_trivial.strong_replacementI [OF M_trivial_L]
   2.104 +  and strong_replacement_closed = M_trivial.strong_replacement_closed [OF M_trivial_L]
   2.105 +  and RepFun_closed = M_trivial.RepFun_closed [OF M_trivial_L]
   2.106 +  and lam_closed = M_trivial.lam_closed [OF M_trivial_L]
   2.107 +  and image_abs = M_trivial.image_abs [OF M_trivial_L]
   2.108 +  and powerset_Pow = M_trivial.powerset_Pow [OF M_trivial_L]
   2.109 +  and powerset_imp_subset_Pow = M_trivial.powerset_imp_subset_Pow [OF M_trivial_L]
   2.110 +  and nat_into_M = M_trivial.nat_into_M [OF M_trivial_L]
   2.111 +  and nat_case_closed = M_trivial.nat_case_closed [OF M_trivial_L]
   2.112 +  and Inl_in_M_iff = M_trivial.Inl_in_M_iff [OF M_trivial_L]
   2.113 +  and Inr_in_M_iff = M_trivial.Inr_in_M_iff [OF M_trivial_L]
   2.114 +  and lt_closed = M_trivial.lt_closed [OF M_trivial_L]
   2.115 +  and transitive_set_abs = M_trivial.transitive_set_abs [OF M_trivial_L]
   2.116 +  and ordinal_abs = M_trivial.ordinal_abs [OF M_trivial_L]
   2.117 +  and limit_ordinal_abs = M_trivial.limit_ordinal_abs [OF M_trivial_L]
   2.118 +  and successor_ordinal_abs = M_trivial.successor_ordinal_abs [OF M_trivial_L]
   2.119 +  and finite_ordinal_abs = M_trivial.finite_ordinal_abs [OF M_trivial_L]
   2.120 +  and omega_abs = M_trivial.omega_abs [OF M_trivial_L]
   2.121 +  and number1_abs = M_trivial.number1_abs [OF M_trivial_L]
   2.122 +  and number2_abs = M_trivial.number2_abs [OF M_trivial_L]
   2.123 +  and number3_abs = M_trivial.number3_abs [OF M_trivial_L]
   2.124  
   2.125  declare rall_abs [simp]
   2.126  declare rex_abs [simp]
     3.1 --- a/src/ZF/Constructible/Rec_Separation.thy	Tue Sep 10 16:47:17 2002 +0200
     3.2 +++ b/src/ZF/Constructible/Rec_Separation.thy	Tue Sep 10 16:51:31 2002 +0200
     3.3 @@ -212,7 +212,7 @@
     3.4  
     3.5  theorem M_trancl_L: "PROP M_trancl(L)"
     3.6  by (rule M_trancl.intro
     3.7 -         [OF M_triv_axioms_L M_axioms_axioms_L M_trancl_axioms_L])
     3.8 +         [OF M_trivial_L M_basic_axioms_L M_trancl_axioms_L])
     3.9  
    3.10  lemmas iterates_abs = M_trancl.iterates_abs [OF M_trancl_L]
    3.11    and rtran_closure_rtrancl = M_trancl.rtran_closure_rtrancl [OF M_trancl_L]
     4.1 --- a/src/ZF/Constructible/Relative.thy	Tue Sep 10 16:47:17 2002 +0200
     4.2 +++ b/src/ZF/Constructible/Relative.thy	Tue Sep 10 16:51:31 2002 +0200
     4.3 @@ -465,7 +465,7 @@
     4.4  
     4.5  text{*The class M is assumed to be transitive and to satisfy some
     4.6        relativized ZF axioms*}
     4.7 -locale M_triv_axioms =
     4.8 +locale M_trivial =
     4.9    fixes M
    4.10    assumes transM:           "[| y\<in>x; M(x) |] ==> M(y)"
    4.11        and nonempty [simp]:  "M(0)"
    4.12 @@ -475,73 +475,73 @@
    4.13        and replacement:      "replacement(M,P)"
    4.14        and M_nat [iff]:      "M(nat)"           (*i.e. the axiom of infinity*)
    4.15  
    4.16 -lemma (in M_triv_axioms) rall_abs [simp]: 
    4.17 +lemma (in M_trivial) rall_abs [simp]: 
    4.18       "M(A) ==> (\<forall>x[M]. x\<in>A --> P(x)) <-> (\<forall>x\<in>A. P(x))" 
    4.19  by (blast intro: transM) 
    4.20  
    4.21 -lemma (in M_triv_axioms) rex_abs [simp]: 
    4.22 +lemma (in M_trivial) rex_abs [simp]: 
    4.23       "M(A) ==> (\<exists>x[M]. x\<in>A & P(x)) <-> (\<exists>x\<in>A. P(x))" 
    4.24  by (blast intro: transM) 
    4.25  
    4.26 -lemma (in M_triv_axioms) ball_iff_equiv: 
    4.27 +lemma (in M_trivial) ball_iff_equiv: 
    4.28       "M(A) ==> (\<forall>x[M]. (x\<in>A <-> P(x))) <-> 
    4.29                 (\<forall>x\<in>A. P(x)) & (\<forall>x. P(x) --> M(x) --> x\<in>A)" 
    4.30  by (blast intro: transM)
    4.31  
    4.32  text{*Simplifies proofs of equalities when there's an iff-equality
    4.33        available for rewriting, universally quantified over M. *}
    4.34 -lemma (in M_triv_axioms) M_equalityI: 
    4.35 +lemma (in M_trivial) M_equalityI: 
    4.36       "[| !!x. M(x) ==> x\<in>A <-> x\<in>B; M(A); M(B) |] ==> A=B"
    4.37  by (blast intro!: equalityI dest: transM) 
    4.38  
    4.39  
    4.40  subsubsection{*Trivial Absoluteness Proofs: Empty Set, Pairs, etc.*}
    4.41  
    4.42 -lemma (in M_triv_axioms) empty_abs [simp]: 
    4.43 +lemma (in M_trivial) empty_abs [simp]: 
    4.44       "M(z) ==> empty(M,z) <-> z=0"
    4.45  apply (simp add: empty_def)
    4.46  apply (blast intro: transM) 
    4.47  done
    4.48  
    4.49 -lemma (in M_triv_axioms) subset_abs [simp]: 
    4.50 +lemma (in M_trivial) subset_abs [simp]: 
    4.51       "M(A) ==> subset(M,A,B) <-> A \<subseteq> B"
    4.52  apply (simp add: subset_def) 
    4.53  apply (blast intro: transM) 
    4.54  done
    4.55  
    4.56 -lemma (in M_triv_axioms) upair_abs [simp]: 
    4.57 +lemma (in M_trivial) upair_abs [simp]: 
    4.58       "M(z) ==> upair(M,a,b,z) <-> z={a,b}"
    4.59  apply (simp add: upair_def) 
    4.60  apply (blast intro: transM) 
    4.61  done
    4.62  
    4.63 -lemma (in M_triv_axioms) upair_in_M_iff [iff]:
    4.64 +lemma (in M_trivial) upair_in_M_iff [iff]:
    4.65       "M({a,b}) <-> M(a) & M(b)"
    4.66  apply (insert upair_ax, simp add: upair_ax_def) 
    4.67  apply (blast intro: transM) 
    4.68  done
    4.69  
    4.70 -lemma (in M_triv_axioms) singleton_in_M_iff [iff]:
    4.71 +lemma (in M_trivial) singleton_in_M_iff [iff]:
    4.72       "M({a}) <-> M(a)"
    4.73  by (insert upair_in_M_iff [of a a], simp) 
    4.74  
    4.75 -lemma (in M_triv_axioms) pair_abs [simp]: 
    4.76 +lemma (in M_trivial) pair_abs [simp]: 
    4.77       "M(z) ==> pair(M,a,b,z) <-> z=<a,b>"
    4.78  apply (simp add: pair_def ZF.Pair_def)
    4.79  apply (blast intro: transM) 
    4.80  done
    4.81  
    4.82 -lemma (in M_triv_axioms) pair_in_M_iff [iff]:
    4.83 +lemma (in M_trivial) pair_in_M_iff [iff]:
    4.84       "M(<a,b>) <-> M(a) & M(b)"
    4.85  by (simp add: ZF.Pair_def)
    4.86  
    4.87 -lemma (in M_triv_axioms) pair_components_in_M:
    4.88 +lemma (in M_trivial) pair_components_in_M:
    4.89       "[| <x,y> \<in> A; M(A) |] ==> M(x) & M(y)"
    4.90  apply (simp add: Pair_def)
    4.91  apply (blast dest: transM) 
    4.92  done
    4.93  
    4.94 -lemma (in M_triv_axioms) cartprod_abs [simp]: 
    4.95 +lemma (in M_trivial) cartprod_abs [simp]: 
    4.96       "[| M(A); M(B); M(z) |] ==> cartprod(M,A,B,z) <-> z = A*B"
    4.97  apply (simp add: cartprod_def)
    4.98  apply (rule iffI) 
    4.99 @@ -551,51 +551,51 @@
   4.100  
   4.101  subsubsection{*Absoluteness for Unions and Intersections*}
   4.102  
   4.103 -lemma (in M_triv_axioms) union_abs [simp]: 
   4.104 +lemma (in M_trivial) union_abs [simp]: 
   4.105       "[| M(a); M(b); M(z) |] ==> union(M,a,b,z) <-> z = a Un b"
   4.106  apply (simp add: union_def) 
   4.107  apply (blast intro: transM) 
   4.108  done
   4.109  
   4.110 -lemma (in M_triv_axioms) inter_abs [simp]: 
   4.111 +lemma (in M_trivial) inter_abs [simp]: 
   4.112       "[| M(a); M(b); M(z) |] ==> inter(M,a,b,z) <-> z = a Int b"
   4.113  apply (simp add: inter_def) 
   4.114  apply (blast intro: transM) 
   4.115  done
   4.116  
   4.117 -lemma (in M_triv_axioms) setdiff_abs [simp]: 
   4.118 +lemma (in M_trivial) setdiff_abs [simp]: 
   4.119       "[| M(a); M(b); M(z) |] ==> setdiff(M,a,b,z) <-> z = a-b"
   4.120  apply (simp add: setdiff_def) 
   4.121  apply (blast intro: transM) 
   4.122  done
   4.123  
   4.124 -lemma (in M_triv_axioms) Union_abs [simp]: 
   4.125 +lemma (in M_trivial) Union_abs [simp]: 
   4.126       "[| M(A); M(z) |] ==> big_union(M,A,z) <-> z = Union(A)"
   4.127  apply (simp add: big_union_def) 
   4.128  apply (blast intro!: equalityI dest: transM) 
   4.129  done
   4.130  
   4.131 -lemma (in M_triv_axioms) Union_closed [intro,simp]:
   4.132 +lemma (in M_trivial) Union_closed [intro,simp]:
   4.133       "M(A) ==> M(Union(A))"
   4.134  by (insert Union_ax, simp add: Union_ax_def) 
   4.135  
   4.136 -lemma (in M_triv_axioms) Un_closed [intro,simp]:
   4.137 +lemma (in M_trivial) Un_closed [intro,simp]:
   4.138       "[| M(A); M(B) |] ==> M(A Un B)"
   4.139  by (simp only: Un_eq_Union, blast) 
   4.140  
   4.141 -lemma (in M_triv_axioms) cons_closed [intro,simp]:
   4.142 +lemma (in M_trivial) cons_closed [intro,simp]:
   4.143       "[| M(a); M(A) |] ==> M(cons(a,A))"
   4.144  by (subst cons_eq [symmetric], blast) 
   4.145  
   4.146 -lemma (in M_triv_axioms) cons_abs [simp]: 
   4.147 +lemma (in M_trivial) cons_abs [simp]: 
   4.148       "[| M(b); M(z) |] ==> is_cons(M,a,b,z) <-> z = cons(a,b)"
   4.149  by (simp add: is_cons_def, blast intro: transM)  
   4.150  
   4.151 -lemma (in M_triv_axioms) successor_abs [simp]: 
   4.152 +lemma (in M_trivial) successor_abs [simp]: 
   4.153       "[| M(a); M(z) |] ==> successor(M,a,z) <-> z = succ(a)"
   4.154  by (simp add: successor_def, blast)  
   4.155  
   4.156 -lemma (in M_triv_axioms) succ_in_M_iff [iff]:
   4.157 +lemma (in M_trivial) succ_in_M_iff [iff]:
   4.158       "M(succ(a)) <-> M(a)"
   4.159  apply (simp add: succ_def) 
   4.160  apply (blast intro: transM) 
   4.161 @@ -603,7 +603,7 @@
   4.162  
   4.163  subsubsection{*Absoluteness for Separation and Replacement*}
   4.164  
   4.165 -lemma (in M_triv_axioms) separation_closed [intro,simp]:
   4.166 +lemma (in M_trivial) separation_closed [intro,simp]:
   4.167       "[| separation(M,P); M(A) |] ==> M(Collect(A,P))"
   4.168  apply (insert separation, simp add: separation_def) 
   4.169  apply (drule rspec, assumption, clarify) 
   4.170 @@ -615,14 +615,14 @@
   4.171       "separation(M,P) <-> (\<forall>z[M]. \<exists>y[M]. is_Collect(M,z,P,y))"
   4.172  by (simp add: separation_def is_Collect_def) 
   4.173  
   4.174 -lemma (in M_triv_axioms) Collect_abs [simp]: 
   4.175 +lemma (in M_trivial) Collect_abs [simp]: 
   4.176       "[| M(A); M(z) |] ==> is_Collect(M,A,P,z) <-> z = Collect(A,P)"
   4.177  apply (simp add: is_Collect_def)
   4.178  apply (blast intro!: equalityI dest: transM)
   4.179  done
   4.180  
   4.181  text{*Probably the premise and conclusion are equivalent*}
   4.182 -lemma (in M_triv_axioms) strong_replacementI [rule_format]:
   4.183 +lemma (in M_trivial) strong_replacementI [rule_format]:
   4.184      "[| \<forall>A[M]. separation(M, %u. \<exists>x[M]. x\<in>A & P(x,u)) |]
   4.185       ==> strong_replacement(M,P)"
   4.186  apply (simp add: strong_replacement_def, clarify) 
   4.187 @@ -645,7 +645,7 @@
   4.188            is_Replace(M, A', %x y. P'(x,y), z')" 
   4.189  by (simp add: is_Replace_def) 
   4.190  
   4.191 -lemma (in M_triv_axioms) univalent_Replace_iff: 
   4.192 +lemma (in M_trivial) univalent_Replace_iff: 
   4.193       "[| M(A); univalent(M,A,P);
   4.194           !!x y. [| x\<in>A; P(x,y) |] ==> M(y) |] 
   4.195        ==> u \<in> Replace(A,P) <-> (\<exists>x. x\<in>A & P(x,u))"
   4.196 @@ -654,7 +654,7 @@
   4.197  done
   4.198  
   4.199  (*The last premise expresses that P takes M to M*)
   4.200 -lemma (in M_triv_axioms) strong_replacement_closed [intro,simp]:
   4.201 +lemma (in M_trivial) strong_replacement_closed [intro,simp]:
   4.202       "[| strong_replacement(M,P); M(A); univalent(M,A,P); 
   4.203           !!x y. [| x\<in>A; P(x,y) |] ==> M(y) |] ==> M(Replace(A,P))"
   4.204  apply (simp add: strong_replacement_def) 
   4.205 @@ -666,7 +666,7 @@
   4.206  apply (blast dest: transM) 
   4.207  done
   4.208  
   4.209 -lemma (in M_triv_axioms) Replace_abs: 
   4.210 +lemma (in M_trivial) Replace_abs: 
   4.211       "[| M(A); M(z); univalent(M,A,P); strong_replacement(M, P);
   4.212           !!x y. [| x\<in>A; P(x,y) |] ==> M(y)  |] 
   4.213        ==> is_Replace(M,A,P,z) <-> z = Replace(A,P)"
   4.214 @@ -683,7 +683,7 @@
   4.215    nonconstructible set.  So we cannot assume that M(X) implies M(RepFun(X,f))
   4.216    even for f : M -> M.
   4.217  *)
   4.218 -lemma (in M_triv_axioms) RepFun_closed:
   4.219 +lemma (in M_trivial) RepFun_closed:
   4.220       "[| strong_replacement(M, \<lambda>x y. y = f(x)); M(A); \<forall>x\<in>A. M(f(x)) |]
   4.221        ==> M(RepFun(A,f))"
   4.222  apply (simp add: RepFun_def) 
   4.223 @@ -696,7 +696,7 @@
   4.224  
   4.225  text{*Better than @{text RepFun_closed} when having the formula @{term "x\<in>A"}
   4.226        makes relativization easier.*}
   4.227 -lemma (in M_triv_axioms) RepFun_closed2:
   4.228 +lemma (in M_trivial) RepFun_closed2:
   4.229       "[| strong_replacement(M, \<lambda>x y. x\<in>A & y = f(x)); M(A); \<forall>x\<in>A. M(f(x)) |]
   4.230        ==> M(RepFun(A, %x. f(x)))"
   4.231  apply (simp add: RepFun_def)
   4.232 @@ -712,20 +712,20 @@
   4.233         \<forall>p[M]. p \<in> z <->
   4.234          (\<exists>u[M]. \<exists>v[M]. u\<in>A & pair(M,u,v,p) & is_b(u,v))"
   4.235  
   4.236 -lemma (in M_triv_axioms) lam_closed:
   4.237 +lemma (in M_trivial) lam_closed:
   4.238       "[| strong_replacement(M, \<lambda>x y. y = <x,b(x)>); M(A); \<forall>x\<in>A. M(b(x)) |]
   4.239        ==> M(\<lambda>x\<in>A. b(x))"
   4.240  by (simp add: lam_def, blast intro: RepFun_closed dest: transM) 
   4.241  
   4.242  text{*Better than @{text lam_closed}: has the formula @{term "x\<in>A"}*}
   4.243 -lemma (in M_triv_axioms) lam_closed2:
   4.244 +lemma (in M_trivial) lam_closed2:
   4.245    "[|strong_replacement(M, \<lambda>x y. x\<in>A & y = \<langle>x, b(x)\<rangle>);
   4.246       M(A); \<forall>m[M]. m\<in>A --> M(b(m))|] ==> M(Lambda(A,b))"
   4.247  apply (simp add: lam_def)
   4.248  apply (blast intro: RepFun_closed2 dest: transM)  
   4.249  done
   4.250  
   4.251 -lemma (in M_triv_axioms) lambda_abs2 [simp]: 
   4.252 +lemma (in M_trivial) lambda_abs2 [simp]: 
   4.253       "[| strong_replacement(M, \<lambda>x y. x\<in>A & y = \<langle>x, b(x)\<rangle>);
   4.254           Relativize1(M,A,is_b,b); M(A); \<forall>m[M]. m\<in>A --> M(b(m)); M(z) |] 
   4.255        ==> is_lambda(M,A,is_b,z) <-> z = Lambda(A,b)"
   4.256 @@ -744,7 +744,7 @@
   4.257            is_lambda(M, A', %x y. is_b'(x,y), z')" 
   4.258  by (simp add: is_lambda_def) 
   4.259  
   4.260 -lemma (in M_triv_axioms) image_abs [simp]: 
   4.261 +lemma (in M_trivial) image_abs [simp]: 
   4.262       "[| M(r); M(A); M(z) |] ==> image(M,r,A,z) <-> z = r``A"
   4.263  apply (simp add: image_def)
   4.264  apply (rule iffI) 
   4.265 @@ -754,13 +754,13 @@
   4.266  text{*What about @{text Pow_abs}?  Powerset is NOT absolute!
   4.267        This result is one direction of absoluteness.*}
   4.268  
   4.269 -lemma (in M_triv_axioms) powerset_Pow: 
   4.270 +lemma (in M_trivial) powerset_Pow: 
   4.271       "powerset(M, x, Pow(x))"
   4.272  by (simp add: powerset_def)
   4.273  
   4.274  text{*But we can't prove that the powerset in @{text M} includes the
   4.275        real powerset.*}
   4.276 -lemma (in M_triv_axioms) powerset_imp_subset_Pow: 
   4.277 +lemma (in M_trivial) powerset_imp_subset_Pow: 
   4.278       "[| powerset(M,x,y); M(y) |] ==> y <= Pow(x)"
   4.279  apply (simp add: powerset_def) 
   4.280  apply (blast dest: transM) 
   4.281 @@ -768,22 +768,22 @@
   4.282  
   4.283  subsubsection{*Absoluteness for the Natural Numbers*}
   4.284  
   4.285 -lemma (in M_triv_axioms) nat_into_M [intro]:
   4.286 +lemma (in M_trivial) nat_into_M [intro]:
   4.287       "n \<in> nat ==> M(n)"
   4.288  by (induct n rule: nat_induct, simp_all)
   4.289  
   4.290 -lemma (in M_triv_axioms) nat_case_closed [intro,simp]:
   4.291 +lemma (in M_trivial) nat_case_closed [intro,simp]:
   4.292    "[|M(k); M(a); \<forall>m[M]. M(b(m))|] ==> M(nat_case(a,b,k))"
   4.293  apply (case_tac "k=0", simp) 
   4.294  apply (case_tac "\<exists>m. k = succ(m)", force)
   4.295  apply (simp add: nat_case_def) 
   4.296  done
   4.297  
   4.298 -lemma (in M_triv_axioms) quasinat_abs [simp]: 
   4.299 +lemma (in M_trivial) quasinat_abs [simp]: 
   4.300       "M(z) ==> is_quasinat(M,z) <-> quasinat(z)"
   4.301  by (auto simp add: is_quasinat_def quasinat_def)
   4.302  
   4.303 -lemma (in M_triv_axioms) nat_case_abs [simp]: 
   4.304 +lemma (in M_trivial) nat_case_abs [simp]: 
   4.305       "[| relativize1(M,is_b,b); M(k); M(z) |] 
   4.306        ==> is_nat_case(M,a,is_b,k,z) <-> z = nat_case(a,b,k)"
   4.307  apply (case_tac "quasinat(k)") 
   4.308 @@ -808,26 +808,26 @@
   4.309  subsection{*Absoluteness for Ordinals*}
   4.310  text{*These results constitute Theorem IV 5.1 of Kunen (page 126).*}
   4.311  
   4.312 -lemma (in M_triv_axioms) lt_closed:
   4.313 +lemma (in M_trivial) lt_closed:
   4.314       "[| j<i; M(i) |] ==> M(j)" 
   4.315  by (blast dest: ltD intro: transM) 
   4.316  
   4.317 -lemma (in M_triv_axioms) transitive_set_abs [simp]: 
   4.318 +lemma (in M_trivial) transitive_set_abs [simp]: 
   4.319       "M(a) ==> transitive_set(M,a) <-> Transset(a)"
   4.320  by (simp add: transitive_set_def Transset_def)
   4.321  
   4.322 -lemma (in M_triv_axioms) ordinal_abs [simp]: 
   4.323 +lemma (in M_trivial) ordinal_abs [simp]: 
   4.324       "M(a) ==> ordinal(M,a) <-> Ord(a)"
   4.325  by (simp add: ordinal_def Ord_def)
   4.326  
   4.327 -lemma (in M_triv_axioms) limit_ordinal_abs [simp]: 
   4.328 +lemma (in M_trivial) limit_ordinal_abs [simp]: 
   4.329       "M(a) ==> limit_ordinal(M,a) <-> Limit(a)" 
   4.330  apply (unfold Limit_def limit_ordinal_def) 
   4.331  apply (simp add: Ord_0_lt_iff) 
   4.332  apply (simp add: lt_def, blast) 
   4.333  done
   4.334  
   4.335 -lemma (in M_triv_axioms) successor_ordinal_abs [simp]: 
   4.336 +lemma (in M_trivial) successor_ordinal_abs [simp]: 
   4.337       "M(a) ==> successor_ordinal(M,a) <-> Ord(a) & (\<exists>b[M]. a = succ(b))"
   4.338  apply (simp add: successor_ordinal_def, safe)
   4.339  apply (drule Ord_cases_disj, auto) 
   4.340 @@ -840,7 +840,7 @@
   4.341  lemma naturals_not_limit: "a \<in> nat ==> ~ Limit(a)"
   4.342  by (induct a rule: nat_induct, auto)
   4.343  
   4.344 -lemma (in M_triv_axioms) finite_ordinal_abs [simp]: 
   4.345 +lemma (in M_trivial) finite_ordinal_abs [simp]: 
   4.346       "M(a) ==> finite_ordinal(M,a) <-> a \<in> nat"
   4.347  apply (simp add: finite_ordinal_def)
   4.348  apply (blast intro: finite_Ord_is_nat intro: nat_into_Ord 
   4.349 @@ -856,21 +856,21 @@
   4.350  apply (erule nat_le_Limit)
   4.351  done
   4.352  
   4.353 -lemma (in M_triv_axioms) omega_abs [simp]: 
   4.354 +lemma (in M_trivial) omega_abs [simp]: 
   4.355       "M(a) ==> omega(M,a) <-> a = nat"
   4.356  apply (simp add: omega_def) 
   4.357  apply (blast intro: Limit_non_Limit_implies_nat dest: naturals_not_limit)
   4.358  done
   4.359  
   4.360 -lemma (in M_triv_axioms) number1_abs [simp]: 
   4.361 +lemma (in M_trivial) number1_abs [simp]: 
   4.362       "M(a) ==> number1(M,a) <-> a = 1"
   4.363  by (simp add: number1_def) 
   4.364  
   4.365 -lemma (in M_triv_axioms) number2_abs [simp]: 
   4.366 +lemma (in M_trivial) number2_abs [simp]: 
   4.367       "M(a) ==> number2(M,a) <-> a = succ(1)"
   4.368  by (simp add: number2_def) 
   4.369  
   4.370 -lemma (in M_triv_axioms) number3_abs [simp]: 
   4.371 +lemma (in M_trivial) number3_abs [simp]: 
   4.372       "M(a) ==> number3(M,a) <-> a = succ(succ(1))"
   4.373  by (simp add: number3_def) 
   4.374  
   4.375 @@ -893,13 +893,13 @@
   4.376      natnumber :: "[i=>o,i,i] => o"
   4.377        "natnumber(M,n,x) == natnumber_aux(M,n)`x = 1"
   4.378  
   4.379 -  lemma (in M_triv_axioms) [simp]: 
   4.380 +  lemma (in M_trivial) [simp]: 
   4.381         "natnumber(M,0,x) == x=0"
   4.382  *)
   4.383  
   4.384  subsection{*Some instances of separation and strong replacement*}
   4.385  
   4.386 -locale M_axioms = M_triv_axioms +
   4.387 +locale M_basic = M_trivial +
   4.388  assumes Inter_separation:
   4.389       "M(A) ==> separation(M, \<lambda>x. \<forall>y[M]. y\<in>A --> x\<in>y)"
   4.390    and Diff_separation:
   4.391 @@ -960,7 +960,7 @@
   4.392                  (\<exists>fx[M]. \<exists>gx[M]. fun_apply(M,f,x,fx) & fun_apply(M,g,x,gx) & 
   4.393                                     fx \<noteq> gx))"
   4.394  
   4.395 -lemma (in M_axioms) cartprod_iff_lemma:
   4.396 +lemma (in M_basic) cartprod_iff_lemma:
   4.397       "[| M(C);  \<forall>u[M]. u \<in> C <-> (\<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}}); 
   4.398           powerset(M, A \<union> B, p1); powerset(M, p1, p2);  M(p2) |]
   4.399         ==> C = {u \<in> p2 . \<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}}}"
   4.400 @@ -973,7 +973,7 @@
   4.401  apply (frule transM, assumption, force) 
   4.402  done
   4.403  
   4.404 -lemma (in M_axioms) cartprod_iff:
   4.405 +lemma (in M_basic) cartprod_iff:
   4.406       "[| M(A); M(B); M(C) |] 
   4.407        ==> cartprod(M,A,B,C) <-> 
   4.408            (\<exists>p1 p2. M(p1) & M(p2) & powerset(M,A Un B,p1) & powerset(M,p1,p2) &
   4.409 @@ -991,7 +991,7 @@
   4.410  apply (blast intro: cartprod_iff_lemma) 
   4.411  done
   4.412  
   4.413 -lemma (in M_axioms) cartprod_closed_lemma:
   4.414 +lemma (in M_basic) cartprod_closed_lemma:
   4.415       "[| M(A); M(B) |] ==> \<exists>C[M]. cartprod(M,A,B,C)"
   4.416  apply (simp del: cartprod_abs add: cartprod_iff)
   4.417  apply (insert power_ax, simp add: power_ax_def) 
   4.418 @@ -1008,38 +1008,38 @@
   4.419  
   4.420  text{*All the lemmas above are necessary because Powerset is not absolute.
   4.421        I should have used Replacement instead!*}
   4.422 -lemma (in M_axioms) cartprod_closed [intro,simp]: 
   4.423 +lemma (in M_basic) cartprod_closed [intro,simp]: 
   4.424       "[| M(A); M(B) |] ==> M(A*B)"
   4.425  by (frule cartprod_closed_lemma, assumption, force)
   4.426  
   4.427 -lemma (in M_axioms) sum_closed [intro,simp]: 
   4.428 +lemma (in M_basic) sum_closed [intro,simp]: 
   4.429       "[| M(A); M(B) |] ==> M(A+B)"
   4.430  by (simp add: sum_def)
   4.431  
   4.432 -lemma (in M_axioms) sum_abs [simp]:
   4.433 +lemma (in M_basic) sum_abs [simp]:
   4.434       "[| M(A); M(B); M(Z) |] ==> is_sum(M,A,B,Z) <-> (Z = A+B)"
   4.435  by (simp add: is_sum_def sum_def singleton_0 nat_into_M)
   4.436  
   4.437 -lemma (in M_triv_axioms) Inl_in_M_iff [iff]:
   4.438 +lemma (in M_trivial) Inl_in_M_iff [iff]:
   4.439       "M(Inl(a)) <-> M(a)"
   4.440  by (simp add: Inl_def) 
   4.441  
   4.442 -lemma (in M_triv_axioms) Inl_abs [simp]:
   4.443 +lemma (in M_trivial) Inl_abs [simp]:
   4.444       "M(Z) ==> is_Inl(M,a,Z) <-> (Z = Inl(a))"
   4.445  by (simp add: is_Inl_def Inl_def)
   4.446  
   4.447 -lemma (in M_triv_axioms) Inr_in_M_iff [iff]:
   4.448 +lemma (in M_trivial) Inr_in_M_iff [iff]:
   4.449       "M(Inr(a)) <-> M(a)"
   4.450  by (simp add: Inr_def) 
   4.451  
   4.452 -lemma (in M_triv_axioms) Inr_abs [simp]:
   4.453 +lemma (in M_trivial) Inr_abs [simp]:
   4.454       "M(Z) ==> is_Inr(M,a,Z) <-> (Z = Inr(a))"
   4.455  by (simp add: is_Inr_def Inr_def)
   4.456  
   4.457  
   4.458  subsubsection {*converse of a relation*}
   4.459  
   4.460 -lemma (in M_axioms) M_converse_iff:
   4.461 +lemma (in M_basic) M_converse_iff:
   4.462       "M(r) ==> 
   4.463        converse(r) = 
   4.464        {z \<in> Union(Union(r)) * Union(Union(r)). 
   4.465 @@ -1050,13 +1050,13 @@
   4.466  apply (blast dest: transM) 
   4.467  done
   4.468  
   4.469 -lemma (in M_axioms) converse_closed [intro,simp]: 
   4.470 +lemma (in M_basic) converse_closed [intro,simp]: 
   4.471       "M(r) ==> M(converse(r))"
   4.472  apply (simp add: M_converse_iff)
   4.473  apply (insert converse_separation [of r], simp)
   4.474  done
   4.475  
   4.476 -lemma (in M_axioms) converse_abs [simp]: 
   4.477 +lemma (in M_basic) converse_abs [simp]: 
   4.478       "[| M(r); M(z) |] ==> is_converse(M,r,z) <-> z = converse(r)"
   4.479  apply (simp add: is_converse_def)
   4.480  apply (rule iffI)
   4.481 @@ -1069,105 +1069,105 @@
   4.482  
   4.483  subsubsection {*image, preimage, domain, range*}
   4.484  
   4.485 -lemma (in M_axioms) image_closed [intro,simp]: 
   4.486 +lemma (in M_basic) image_closed [intro,simp]: 
   4.487       "[| M(A); M(r) |] ==> M(r``A)"
   4.488  apply (simp add: image_iff_Collect)
   4.489  apply (insert image_separation [of A r], simp) 
   4.490  done
   4.491  
   4.492 -lemma (in M_axioms) vimage_abs [simp]: 
   4.493 +lemma (in M_basic) vimage_abs [simp]: 
   4.494       "[| M(r); M(A); M(z) |] ==> pre_image(M,r,A,z) <-> z = r-``A"
   4.495  apply (simp add: pre_image_def)
   4.496  apply (rule iffI) 
   4.497   apply (blast intro!: equalityI dest: transM, blast) 
   4.498  done
   4.499  
   4.500 -lemma (in M_axioms) vimage_closed [intro,simp]: 
   4.501 +lemma (in M_basic) vimage_closed [intro,simp]: 
   4.502       "[| M(A); M(r) |] ==> M(r-``A)"
   4.503  by (simp add: vimage_def)
   4.504  
   4.505  
   4.506  subsubsection{*Domain, range and field*}
   4.507  
   4.508 -lemma (in M_axioms) domain_abs [simp]: 
   4.509 +lemma (in M_basic) domain_abs [simp]: 
   4.510       "[| M(r); M(z) |] ==> is_domain(M,r,z) <-> z = domain(r)"
   4.511  apply (simp add: is_domain_def) 
   4.512  apply (blast intro!: equalityI dest: transM) 
   4.513  done
   4.514  
   4.515 -lemma (in M_axioms) domain_closed [intro,simp]: 
   4.516 +lemma (in M_basic) domain_closed [intro,simp]: 
   4.517       "M(r) ==> M(domain(r))"
   4.518  apply (simp add: domain_eq_vimage)
   4.519  done
   4.520  
   4.521 -lemma (in M_axioms) range_abs [simp]: 
   4.522 +lemma (in M_basic) range_abs [simp]: 
   4.523       "[| M(r); M(z) |] ==> is_range(M,r,z) <-> z = range(r)"
   4.524  apply (simp add: is_range_def)
   4.525  apply (blast intro!: equalityI dest: transM)
   4.526  done
   4.527  
   4.528 -lemma (in M_axioms) range_closed [intro,simp]: 
   4.529 +lemma (in M_basic) range_closed [intro,simp]: 
   4.530       "M(r) ==> M(range(r))"
   4.531  apply (simp add: range_eq_image)
   4.532  done
   4.533  
   4.534 -lemma (in M_axioms) field_abs [simp]: 
   4.535 +lemma (in M_basic) field_abs [simp]: 
   4.536       "[| M(r); M(z) |] ==> is_field(M,r,z) <-> z = field(r)"
   4.537  by (simp add: domain_closed range_closed is_field_def field_def)
   4.538  
   4.539 -lemma (in M_axioms) field_closed [intro,simp]: 
   4.540 +lemma (in M_basic) field_closed [intro,simp]: 
   4.541       "M(r) ==> M(field(r))"
   4.542  by (simp add: domain_closed range_closed Un_closed field_def) 
   4.543  
   4.544  
   4.545  subsubsection{*Relations, functions and application*}
   4.546  
   4.547 -lemma (in M_axioms) relation_abs [simp]: 
   4.548 +lemma (in M_basic) relation_abs [simp]: 
   4.549       "M(r) ==> is_relation(M,r) <-> relation(r)"
   4.550  apply (simp add: is_relation_def relation_def) 
   4.551  apply (blast dest!: bspec dest: pair_components_in_M)+
   4.552  done
   4.553  
   4.554 -lemma (in M_axioms) function_abs [simp]: 
   4.555 +lemma (in M_basic) function_abs [simp]: 
   4.556       "M(r) ==> is_function(M,r) <-> function(r)"
   4.557  apply (simp add: is_function_def function_def, safe) 
   4.558     apply (frule transM, assumption) 
   4.559    apply (blast dest: pair_components_in_M)+
   4.560  done
   4.561  
   4.562 -lemma (in M_axioms) apply_closed [intro,simp]: 
   4.563 +lemma (in M_basic) apply_closed [intro,simp]: 
   4.564       "[|M(f); M(a)|] ==> M(f`a)"
   4.565  by (simp add: apply_def)
   4.566  
   4.567 -lemma (in M_axioms) apply_abs [simp]: 
   4.568 +lemma (in M_basic) apply_abs [simp]: 
   4.569       "[| M(f); M(x); M(y) |] ==> fun_apply(M,f,x,y) <-> f`x = y"
   4.570  apply (simp add: fun_apply_def apply_def, blast) 
   4.571  done
   4.572  
   4.573 -lemma (in M_axioms) typed_function_abs [simp]: 
   4.574 +lemma (in M_basic) typed_function_abs [simp]: 
   4.575       "[| M(A); M(f) |] ==> typed_function(M,A,B,f) <-> f \<in> A -> B"
   4.576  apply (auto simp add: typed_function_def relation_def Pi_iff) 
   4.577  apply (blast dest: pair_components_in_M)+
   4.578  done
   4.579  
   4.580 -lemma (in M_axioms) injection_abs [simp]: 
   4.581 +lemma (in M_basic) injection_abs [simp]: 
   4.582       "[| M(A); M(f) |] ==> injection(M,A,B,f) <-> f \<in> inj(A,B)"
   4.583  apply (simp add: injection_def apply_iff inj_def apply_closed)
   4.584  apply (blast dest: transM [of _ A]) 
   4.585  done
   4.586  
   4.587 -lemma (in M_axioms) surjection_abs [simp]: 
   4.588 +lemma (in M_basic) surjection_abs [simp]: 
   4.589       "[| M(A); M(B); M(f) |] ==> surjection(M,A,B,f) <-> f \<in> surj(A,B)"
   4.590  by (simp add: surjection_def surj_def)
   4.591  
   4.592 -lemma (in M_axioms) bijection_abs [simp]: 
   4.593 +lemma (in M_basic) bijection_abs [simp]: 
   4.594       "[| M(A); M(B); M(f) |] ==> bijection(M,A,B,f) <-> f \<in> bij(A,B)"
   4.595  by (simp add: bijection_def bij_def)
   4.596  
   4.597  
   4.598  subsubsection{*Composition of relations*}
   4.599  
   4.600 -lemma (in M_axioms) M_comp_iff:
   4.601 +lemma (in M_basic) M_comp_iff:
   4.602       "[| M(r); M(s) |] 
   4.603        ==> r O s = 
   4.604            {xz \<in> domain(s) * range(r).  
   4.605 @@ -1179,13 +1179,13 @@
   4.606   apply  (blast dest:  transM)+
   4.607  done
   4.608  
   4.609 -lemma (in M_axioms) comp_closed [intro,simp]: 
   4.610 +lemma (in M_basic) comp_closed [intro,simp]: 
   4.611       "[| M(r); M(s) |] ==> M(r O s)"
   4.612  apply (simp add: M_comp_iff)
   4.613  apply (insert comp_separation [of r s], simp) 
   4.614  done
   4.615  
   4.616 -lemma (in M_axioms) composition_abs [simp]: 
   4.617 +lemma (in M_basic) composition_abs [simp]: 
   4.618       "[| M(r); M(s); M(t) |] 
   4.619        ==> composition(M,r,s,t) <-> t = r O s"
   4.620  apply safe
   4.621 @@ -1200,7 +1200,7 @@
   4.622  done
   4.623  
   4.624  text{*no longer needed*}
   4.625 -lemma (in M_axioms) restriction_is_function: 
   4.626 +lemma (in M_basic) restriction_is_function: 
   4.627       "[| restriction(M,f,A,z); function(f); M(f); M(A); M(z) |] 
   4.628        ==> function(z)"
   4.629  apply (rotate_tac 1)
   4.630 @@ -1208,7 +1208,7 @@
   4.631  apply (unfold function_def, blast) 
   4.632  done
   4.633  
   4.634 -lemma (in M_axioms) restriction_abs [simp]: 
   4.635 +lemma (in M_basic) restriction_abs [simp]: 
   4.636       "[| M(f); M(A); M(z) |] 
   4.637        ==> restriction(M,f,A,z) <-> z = restrict(f,A)"
   4.638  apply (simp add: ball_iff_equiv restriction_def restrict_def)
   4.639 @@ -1216,39 +1216,39 @@
   4.640  done
   4.641  
   4.642  
   4.643 -lemma (in M_axioms) M_restrict_iff:
   4.644 +lemma (in M_basic) M_restrict_iff:
   4.645       "M(r) ==> restrict(r,A) = {z \<in> r . \<exists>x\<in>A. \<exists>y[M]. z = \<langle>x, y\<rangle>}"
   4.646  by (simp add: restrict_def, blast dest: transM)
   4.647  
   4.648 -lemma (in M_axioms) restrict_closed [intro,simp]: 
   4.649 +lemma (in M_basic) restrict_closed [intro,simp]: 
   4.650       "[| M(A); M(r) |] ==> M(restrict(r,A))"
   4.651  apply (simp add: M_restrict_iff)
   4.652  apply (insert restrict_separation [of A], simp) 
   4.653  done
   4.654  
   4.655 -lemma (in M_axioms) Inter_abs [simp]: 
   4.656 +lemma (in M_basic) Inter_abs [simp]: 
   4.657       "[| M(A); M(z) |] ==> big_inter(M,A,z) <-> z = Inter(A)"
   4.658  apply (simp add: big_inter_def Inter_def) 
   4.659  apply (blast intro!: equalityI dest: transM) 
   4.660  done
   4.661  
   4.662 -lemma (in M_axioms) Inter_closed [intro,simp]:
   4.663 +lemma (in M_basic) Inter_closed [intro,simp]:
   4.664       "M(A) ==> M(Inter(A))"
   4.665  by (insert Inter_separation, simp add: Inter_def)
   4.666  
   4.667 -lemma (in M_axioms) Int_closed [intro,simp]:
   4.668 +lemma (in M_basic) Int_closed [intro,simp]:
   4.669       "[| M(A); M(B) |] ==> M(A Int B)"
   4.670  apply (subgoal_tac "M({A,B})")
   4.671  apply (frule Inter_closed, force+) 
   4.672  done
   4.673  
   4.674 -lemma (in M_axioms) Diff_closed [intro,simp]:
   4.675 +lemma (in M_basic) Diff_closed [intro,simp]:
   4.676       "[|M(A); M(B)|] ==> M(A-B)"
   4.677  by (insert Diff_separation, simp add: Diff_def)
   4.678  
   4.679  subsubsection{*Some Facts About Separation Axioms*}
   4.680  
   4.681 -lemma (in M_axioms) separation_conj:
   4.682 +lemma (in M_basic) separation_conj:
   4.683       "[|separation(M,P); separation(M,Q)|] ==> separation(M, \<lambda>z. P(z) & Q(z))"
   4.684  by (simp del: separation_closed
   4.685           add: separation_iff Collect_Int_Collect_eq [symmetric]) 
   4.686 @@ -1262,24 +1262,24 @@
   4.687       "A - Collect(A,P) = Collect(A, %x. ~ P(x))"
   4.688  by blast
   4.689  
   4.690 -lemma (in M_triv_axioms) Collect_rall_eq:
   4.691 +lemma (in M_trivial) Collect_rall_eq:
   4.692       "M(Y) ==> Collect(A, %x. \<forall>y[M]. y\<in>Y --> P(x,y)) = 
   4.693                 (if Y=0 then A else (\<Inter>y \<in> Y. {x \<in> A. P(x,y)}))"
   4.694  apply simp 
   4.695  apply (blast intro!: equalityI dest: transM) 
   4.696  done
   4.697  
   4.698 -lemma (in M_axioms) separation_disj:
   4.699 +lemma (in M_basic) separation_disj:
   4.700       "[|separation(M,P); separation(M,Q)|] ==> separation(M, \<lambda>z. P(z) | Q(z))"
   4.701  by (simp del: separation_closed
   4.702           add: separation_iff Collect_Un_Collect_eq [symmetric]) 
   4.703  
   4.704 -lemma (in M_axioms) separation_neg:
   4.705 +lemma (in M_basic) separation_neg:
   4.706       "separation(M,P) ==> separation(M, \<lambda>z. ~P(z))"
   4.707  by (simp del: separation_closed
   4.708           add: separation_iff Diff_Collect_eq [symmetric]) 
   4.709  
   4.710 -lemma (in M_axioms) separation_imp:
   4.711 +lemma (in M_basic) separation_imp:
   4.712       "[|separation(M,P); separation(M,Q)|] 
   4.713        ==> separation(M, \<lambda>z. P(z) --> Q(z))"
   4.714  by (simp add: separation_neg separation_disj not_disj_iff_imp [symmetric]) 
   4.715 @@ -1287,7 +1287,7 @@
   4.716  text{*This result is a hint of how little can be done without the Reflection 
   4.717    Theorem.  The quantifier has to be bounded by a set.  We also need another
   4.718    instance of Separation!*}
   4.719 -lemma (in M_axioms) separation_rall:
   4.720 +lemma (in M_basic) separation_rall:
   4.721       "[|M(Y); \<forall>y[M]. separation(M, \<lambda>x. P(x,y)); 
   4.722          \<forall>z[M]. strong_replacement(M, \<lambda>x y. y = {u \<in> z . P(u,x)})|]
   4.723        ==> separation(M, \<lambda>x. \<forall>y[M]. y\<in>Y --> P(x,y))" 
   4.724 @@ -1300,7 +1300,7 @@
   4.725  subsubsection{*Functions and function space*}
   4.726  
   4.727  text{*M contains all finite functions*}
   4.728 -lemma (in M_axioms) finite_fun_closed_lemma [rule_format]: 
   4.729 +lemma (in M_basic) finite_fun_closed_lemma [rule_format]: 
   4.730       "[| n \<in> nat; M(A) |] ==> \<forall>f \<in> n -> A. M(f)"
   4.731  apply (induct_tac n, simp)
   4.732  apply (rule ballI)  
   4.733 @@ -1312,13 +1312,13 @@
   4.734  apply (blast intro: apply_funtype transM restrict_type2) 
   4.735  done
   4.736  
   4.737 -lemma (in M_axioms) finite_fun_closed [rule_format]: 
   4.738 +lemma (in M_basic) finite_fun_closed [rule_format]: 
   4.739       "[| f \<in> n -> A; n \<in> nat; M(A) |] ==> M(f)"
   4.740  by (blast intro: finite_fun_closed_lemma) 
   4.741  
   4.742  text{*The assumption @{term "M(A->B)"} is unusual, but essential: in 
   4.743  all but trivial cases, A->B cannot be expected to belong to @{term M}.*}
   4.744 -lemma (in M_axioms) is_funspace_abs [simp]:
   4.745 +lemma (in M_basic) is_funspace_abs [simp]:
   4.746       "[|M(A); M(B); M(F); M(A->B)|] ==> is_funspace(M,A,B,F) <-> F = A->B";
   4.747  apply (simp add: is_funspace_def)
   4.748  apply (rule iffI)
   4.749 @@ -1327,7 +1327,7 @@
   4.750    apply simp_all
   4.751  done
   4.752  
   4.753 -lemma (in M_axioms) succ_fun_eq2:
   4.754 +lemma (in M_basic) succ_fun_eq2:
   4.755       "[|M(B); M(n->B)|] ==>
   4.756        succ(n) -> B = 
   4.757        \<Union>{z. p \<in> (n->B)*B, \<exists>f[M]. \<exists>b[M]. p = <f,b> & z = {cons(<n,b>, f)}}"
   4.758 @@ -1335,7 +1335,7 @@
   4.759  apply (blast dest: transM)  
   4.760  done
   4.761  
   4.762 -lemma (in M_axioms) funspace_succ:
   4.763 +lemma (in M_basic) funspace_succ:
   4.764       "[|M(n); M(B); M(n->B) |] ==> M(succ(n) -> B)"
   4.765  apply (insert funspace_succ_replacement [of n], simp) 
   4.766  apply (force simp add: succ_fun_eq2 univalent_def) 
   4.767 @@ -1343,7 +1343,7 @@
   4.768  
   4.769  text{*@{term M} contains all finite function spaces.  Needed to prove the
   4.770  absoluteness of transitive closure.*}
   4.771 -lemma (in M_axioms) finite_funspace_closed [intro,simp]:
   4.772 +lemma (in M_basic) finite_funspace_closed [intro,simp]:
   4.773       "[|n\<in>nat; M(B)|] ==> M(n->B)"
   4.774  apply (induct_tac n, simp)
   4.775  apply (simp add: funspace_succ nat_into_M) 
   4.776 @@ -1368,37 +1368,37 @@
   4.777     "is_or(M,a,b,z) == (number1(M,a)  & number1(M,z)) | 
   4.778                        (~number1(M,a) & z=b)"
   4.779  
   4.780 -lemma (in M_triv_axioms) bool_of_o_abs [simp]: 
   4.781 +lemma (in M_trivial) bool_of_o_abs [simp]: 
   4.782       "M(z) ==> is_bool_of_o(M,P,z) <-> z = bool_of_o(P)" 
   4.783  by (simp add: is_bool_of_o_def bool_of_o_def) 
   4.784  
   4.785  
   4.786 -lemma (in M_triv_axioms) not_abs [simp]: 
   4.787 +lemma (in M_trivial) not_abs [simp]: 
   4.788       "[| M(a); M(z)|] ==> is_not(M,a,z) <-> z = not(a)"
   4.789  by (simp add: Bool.not_def cond_def is_not_def) 
   4.790  
   4.791 -lemma (in M_triv_axioms) and_abs [simp]: 
   4.792 +lemma (in M_trivial) and_abs [simp]: 
   4.793       "[| M(a); M(b); M(z)|] ==> is_and(M,a,b,z) <-> z = a and b"
   4.794  by (simp add: Bool.and_def cond_def is_and_def) 
   4.795  
   4.796 -lemma (in M_triv_axioms) or_abs [simp]: 
   4.797 +lemma (in M_trivial) or_abs [simp]: 
   4.798       "[| M(a); M(b); M(z)|] ==> is_or(M,a,b,z) <-> z = a or b"
   4.799  by (simp add: Bool.or_def cond_def is_or_def)
   4.800  
   4.801  
   4.802 -lemma (in M_triv_axioms) bool_of_o_closed [intro,simp]:
   4.803 +lemma (in M_trivial) bool_of_o_closed [intro,simp]:
   4.804       "M(bool_of_o(P))"
   4.805  by (simp add: bool_of_o_def) 
   4.806  
   4.807 -lemma (in M_triv_axioms) and_closed [intro,simp]:
   4.808 +lemma (in M_trivial) and_closed [intro,simp]:
   4.809       "[| M(p); M(q) |] ==> M(p and q)"
   4.810  by (simp add: and_def cond_def) 
   4.811  
   4.812 -lemma (in M_triv_axioms) or_closed [intro,simp]:
   4.813 +lemma (in M_trivial) or_closed [intro,simp]:
   4.814       "[| M(p); M(q) |] ==> M(p or q)"
   4.815  by (simp add: or_def cond_def) 
   4.816  
   4.817 -lemma (in M_triv_axioms) not_closed [intro,simp]:
   4.818 +lemma (in M_trivial) not_closed [intro,simp]:
   4.819       "M(p) ==> M(not(p))"
   4.820  by (simp add: Bool.not_def cond_def) 
   4.821  
   4.822 @@ -1416,16 +1416,16 @@
   4.823      "is_Cons(M,a,l,Z) == \<exists>p[M]. pair(M,a,l,p) & is_Inr(M,p,Z)"
   4.824  
   4.825  
   4.826 -lemma (in M_triv_axioms) Nil_in_M [intro,simp]: "M(Nil)"
   4.827 +lemma (in M_trivial) Nil_in_M [intro,simp]: "M(Nil)"
   4.828  by (simp add: Nil_def)
   4.829  
   4.830 -lemma (in M_triv_axioms) Nil_abs [simp]: "M(Z) ==> is_Nil(M,Z) <-> (Z = Nil)"
   4.831 +lemma (in M_trivial) Nil_abs [simp]: "M(Z) ==> is_Nil(M,Z) <-> (Z = Nil)"
   4.832  by (simp add: is_Nil_def Nil_def)
   4.833  
   4.834 -lemma (in M_triv_axioms) Cons_in_M_iff [iff]: "M(Cons(a,l)) <-> M(a) & M(l)"
   4.835 +lemma (in M_trivial) Cons_in_M_iff [iff]: "M(Cons(a,l)) <-> M(a) & M(l)"
   4.836  by (simp add: Cons_def) 
   4.837  
   4.838 -lemma (in M_triv_axioms) Cons_abs [simp]:
   4.839 +lemma (in M_trivial) Cons_abs [simp]:
   4.840       "[|M(a); M(l); M(Z)|] ==> is_Cons(M,a,l,Z) <-> (Z = Cons(a,l))"
   4.841  by (simp add: is_Cons_def Cons_def)
   4.842  
   4.843 @@ -1499,18 +1499,18 @@
   4.844       "xs \<in> list(A) ==>list_case'(a,b,xs) = list_case(a,b,xs)"
   4.845  by (erule list.cases, simp_all)
   4.846  
   4.847 -lemma (in M_axioms) list_case'_closed [intro,simp]:
   4.848 +lemma (in M_basic) list_case'_closed [intro,simp]:
   4.849    "[|M(k); M(a); \<forall>x[M]. \<forall>y[M]. M(b(x,y))|] ==> M(list_case'(a,b,k))"
   4.850  apply (case_tac "quasilist(k)") 
   4.851   apply (simp add: quasilist_def, force) 
   4.852  apply (simp add: non_list_case) 
   4.853  done
   4.854  
   4.855 -lemma (in M_triv_axioms) quasilist_abs [simp]: 
   4.856 +lemma (in M_trivial) quasilist_abs [simp]: 
   4.857       "M(z) ==> is_quasilist(M,z) <-> quasilist(z)"
   4.858  by (auto simp add: is_quasilist_def quasilist_def)
   4.859  
   4.860 -lemma (in M_triv_axioms) list_case_abs [simp]: 
   4.861 +lemma (in M_trivial) list_case_abs [simp]: 
   4.862       "[| relativize2(M,is_b,b); M(k); M(z) |] 
   4.863        ==> is_list_case(M,a,is_b,k,z) <-> z = list_case'(a,b,k)"
   4.864  apply (case_tac "quasilist(k)") 
   4.865 @@ -1525,14 +1525,14 @@
   4.866  
   4.867  subsubsection{*The Modified Operators @{term hd'} and @{term tl'}*}
   4.868  
   4.869 -lemma (in M_triv_axioms) is_hd_Nil: "is_hd(M,[],Z) <-> empty(M,Z)"
   4.870 +lemma (in M_trivial) is_hd_Nil: "is_hd(M,[],Z) <-> empty(M,Z)"
   4.871  by (simp add: is_hd_def)
   4.872  
   4.873 -lemma (in M_triv_axioms) is_hd_Cons:
   4.874 +lemma (in M_trivial) is_hd_Cons:
   4.875       "[|M(a); M(l)|] ==> is_hd(M,Cons(a,l),Z) <-> Z = a"
   4.876  by (force simp add: is_hd_def) 
   4.877  
   4.878 -lemma (in M_triv_axioms) hd_abs [simp]:
   4.879 +lemma (in M_trivial) hd_abs [simp]:
   4.880       "[|M(x); M(y)|] ==> is_hd(M,x,y) <-> y = hd'(x)"
   4.881  apply (simp add: hd'_def)
   4.882  apply (intro impI conjI)
   4.883 @@ -1541,14 +1541,14 @@
   4.884  apply (elim disjE exE, auto)
   4.885  done 
   4.886  
   4.887 -lemma (in M_triv_axioms) is_tl_Nil: "is_tl(M,[],Z) <-> Z = []"
   4.888 +lemma (in M_trivial) is_tl_Nil: "is_tl(M,[],Z) <-> Z = []"
   4.889  by (simp add: is_tl_def)
   4.890  
   4.891 -lemma (in M_triv_axioms) is_tl_Cons:
   4.892 +lemma (in M_trivial) is_tl_Cons:
   4.893       "[|M(a); M(l)|] ==> is_tl(M,Cons(a,l),Z) <-> Z = l"
   4.894  by (force simp add: is_tl_def) 
   4.895  
   4.896 -lemma (in M_triv_axioms) tl_abs [simp]:
   4.897 +lemma (in M_trivial) tl_abs [simp]:
   4.898       "[|M(x); M(y)|] ==> is_tl(M,x,y) <-> y = tl'(x)"
   4.899  apply (simp add: tl'_def)
   4.900  apply (intro impI conjI)
   4.901 @@ -1557,7 +1557,7 @@
   4.902  apply (elim disjE exE, auto)
   4.903  done 
   4.904  
   4.905 -lemma (in M_triv_axioms) relativize1_tl: "relativize1(M, is_tl(M), tl')"  
   4.906 +lemma (in M_trivial) relativize1_tl: "relativize1(M, is_tl(M), tl')"  
   4.907  by (simp add: relativize1_def)
   4.908  
   4.909  lemma hd'_Nil: "hd'([]) = 0"
   4.910 @@ -1577,7 +1577,7 @@
   4.911  apply (simp_all add: tl'_Nil) 
   4.912  done
   4.913  
   4.914 -lemma (in M_axioms) tl'_closed: "M(x) ==> M(tl'(x))"
   4.915 +lemma (in M_basic) tl'_closed: "M(x) ==> M(tl'(x))"
   4.916  apply (simp add: tl'_def)
   4.917  apply (force simp add: quasilist_def)
   4.918  done
     5.1 --- a/src/ZF/Constructible/Separation.thy	Tue Sep 10 16:47:17 2002 +0200
     5.2 +++ b/src/ZF/Constructible/Separation.thy	Tue Sep 10 16:51:31 2002 +0200
     5.3 @@ -8,7 +8,7 @@
     5.4  
     5.5  theory Separation = L_axioms + WF_absolute:
     5.6  
     5.7 -text{*This theory proves all instances needed for locale @{text "M_axioms"}*}
     5.8 +text{*This theory proves all instances needed for locale @{text "M_basic"}*}
     5.9  
    5.10  text{*Helps us solve for de Bruijn indices!*}
    5.11  lemma nth_ConsI: "[|nth(n,l) = x; n \<in> nat|] ==> nth(succ(n), Cons(a,l)) = x"
    5.12 @@ -470,12 +470,12 @@
    5.13  done
    5.14  
    5.15  
    5.16 -subsection{*Instantiating the locale @{text M_axioms}*}
    5.17 +subsection{*Instantiating the locale @{text M_basic}*}
    5.18  text{*Separation (and Strong Replacement) for basic set-theoretic constructions
    5.19  such as intersection, Cartesian Product and image.*}
    5.20  
    5.21 -lemma M_axioms_axioms_L: "M_axioms_axioms(L)"
    5.22 -  apply (rule M_axioms_axioms.intro)
    5.23 +lemma M_basic_axioms_L: "M_basic_axioms(L)"
    5.24 +  apply (rule M_basic_axioms.intro)
    5.25         apply (assumption | rule
    5.26  	 Inter_separation Diff_separation cartprod_separation image_separation
    5.27  	 converse_separation restrict_separation
    5.28 @@ -485,114 +485,114 @@
    5.29  	 omap_replacement is_recfun_separation)+
    5.30    done
    5.31  
    5.32 -theorem M_axioms_L: "PROP M_axioms(L)"
    5.33 -by (rule M_axioms.intro [OF M_triv_axioms_L M_axioms_axioms_L])
    5.34 +theorem M_basic_L: "PROP M_basic(L)"
    5.35 +by (rule M_basic.intro [OF M_trivial_L M_basic_axioms_L])
    5.36  
    5.37  
    5.38 -lemmas cartprod_iff = M_axioms.cartprod_iff [OF M_axioms_L]
    5.39 -  and cartprod_closed = M_axioms.cartprod_closed [OF M_axioms_L]
    5.40 -  and sum_closed = M_axioms.sum_closed [OF M_axioms_L]
    5.41 -  and M_converse_iff = M_axioms.M_converse_iff [OF M_axioms_L]
    5.42 -  and converse_closed = M_axioms.converse_closed [OF M_axioms_L]
    5.43 -  and converse_abs = M_axioms.converse_abs [OF M_axioms_L]
    5.44 -  and image_closed = M_axioms.image_closed [OF M_axioms_L]
    5.45 -  and vimage_abs = M_axioms.vimage_abs [OF M_axioms_L]
    5.46 -  and vimage_closed = M_axioms.vimage_closed [OF M_axioms_L]
    5.47 -  and domain_abs = M_axioms.domain_abs [OF M_axioms_L]
    5.48 -  and domain_closed = M_axioms.domain_closed [OF M_axioms_L]
    5.49 -  and range_abs = M_axioms.range_abs [OF M_axioms_L]
    5.50 -  and range_closed = M_axioms.range_closed [OF M_axioms_L]
    5.51 -  and field_abs = M_axioms.field_abs [OF M_axioms_L]
    5.52 -  and field_closed = M_axioms.field_closed [OF M_axioms_L]
    5.53 -  and relation_abs = M_axioms.relation_abs [OF M_axioms_L]
    5.54 -  and function_abs = M_axioms.function_abs [OF M_axioms_L]
    5.55 -  and apply_closed = M_axioms.apply_closed [OF M_axioms_L]
    5.56 -  and apply_abs = M_axioms.apply_abs [OF M_axioms_L]
    5.57 -  and typed_function_abs = M_axioms.typed_function_abs [OF M_axioms_L]
    5.58 -  and injection_abs = M_axioms.injection_abs [OF M_axioms_L]
    5.59 -  and surjection_abs = M_axioms.surjection_abs [OF M_axioms_L]
    5.60 -  and bijection_abs = M_axioms.bijection_abs [OF M_axioms_L]
    5.61 -  and M_comp_iff = M_axioms.M_comp_iff [OF M_axioms_L]
    5.62 -  and comp_closed = M_axioms.comp_closed [OF M_axioms_L]
    5.63 -  and composition_abs = M_axioms.composition_abs [OF M_axioms_L]
    5.64 -  and restriction_is_function = M_axioms.restriction_is_function [OF M_axioms_L]
    5.65 -  and restriction_abs = M_axioms.restriction_abs [OF M_axioms_L]
    5.66 -  and M_restrict_iff = M_axioms.M_restrict_iff [OF M_axioms_L]
    5.67 -  and restrict_closed = M_axioms.restrict_closed [OF M_axioms_L]
    5.68 -  and Inter_abs = M_axioms.Inter_abs [OF M_axioms_L]
    5.69 -  and Inter_closed = M_axioms.Inter_closed [OF M_axioms_L]
    5.70 -  and Int_closed = M_axioms.Int_closed [OF M_axioms_L]
    5.71 -  and finite_fun_closed = M_axioms.finite_fun_closed [OF M_axioms_L]
    5.72 -  and is_funspace_abs = M_axioms.is_funspace_abs [OF M_axioms_L]
    5.73 -  and succ_fun_eq2 = M_axioms.succ_fun_eq2 [OF M_axioms_L]
    5.74 -  and funspace_succ = M_axioms.funspace_succ [OF M_axioms_L]
    5.75 -  and finite_funspace_closed = M_axioms.finite_funspace_closed [OF M_axioms_L]
    5.76 +lemmas cartprod_iff = M_basic.cartprod_iff [OF M_basic_L]
    5.77 +  and cartprod_closed = M_basic.cartprod_closed [OF M_basic_L]
    5.78 +  and sum_closed = M_basic.sum_closed [OF M_basic_L]
    5.79 +  and M_converse_iff = M_basic.M_converse_iff [OF M_basic_L]
    5.80 +  and converse_closed = M_basic.converse_closed [OF M_basic_L]
    5.81 +  and converse_abs = M_basic.converse_abs [OF M_basic_L]
    5.82 +  and image_closed = M_basic.image_closed [OF M_basic_L]
    5.83 +  and vimage_abs = M_basic.vimage_abs [OF M_basic_L]
    5.84 +  and vimage_closed = M_basic.vimage_closed [OF M_basic_L]
    5.85 +  and domain_abs = M_basic.domain_abs [OF M_basic_L]
    5.86 +  and domain_closed = M_basic.domain_closed [OF M_basic_L]
    5.87 +  and range_abs = M_basic.range_abs [OF M_basic_L]
    5.88 +  and range_closed = M_basic.range_closed [OF M_basic_L]
    5.89 +  and field_abs = M_basic.field_abs [OF M_basic_L]
    5.90 +  and field_closed = M_basic.field_closed [OF M_basic_L]
    5.91 +  and relation_abs = M_basic.relation_abs [OF M_basic_L]
    5.92 +  and function_abs = M_basic.function_abs [OF M_basic_L]
    5.93 +  and apply_closed = M_basic.apply_closed [OF M_basic_L]
    5.94 +  and apply_abs = M_basic.apply_abs [OF M_basic_L]
    5.95 +  and typed_function_abs = M_basic.typed_function_abs [OF M_basic_L]
    5.96 +  and injection_abs = M_basic.injection_abs [OF M_basic_L]
    5.97 +  and surjection_abs = M_basic.surjection_abs [OF M_basic_L]
    5.98 +  and bijection_abs = M_basic.bijection_abs [OF M_basic_L]
    5.99 +  and M_comp_iff = M_basic.M_comp_iff [OF M_basic_L]
   5.100 +  and comp_closed = M_basic.comp_closed [OF M_basic_L]
   5.101 +  and composition_abs = M_basic.composition_abs [OF M_basic_L]
   5.102 +  and restriction_is_function = M_basic.restriction_is_function [OF M_basic_L]
   5.103 +  and restriction_abs = M_basic.restriction_abs [OF M_basic_L]
   5.104 +  and M_restrict_iff = M_basic.M_restrict_iff [OF M_basic_L]
   5.105 +  and restrict_closed = M_basic.restrict_closed [OF M_basic_L]
   5.106 +  and Inter_abs = M_basic.Inter_abs [OF M_basic_L]
   5.107 +  and Inter_closed = M_basic.Inter_closed [OF M_basic_L]
   5.108 +  and Int_closed = M_basic.Int_closed [OF M_basic_L]
   5.109 +  and finite_fun_closed = M_basic.finite_fun_closed [OF M_basic_L]
   5.110 +  and is_funspace_abs = M_basic.is_funspace_abs [OF M_basic_L]
   5.111 +  and succ_fun_eq2 = M_basic.succ_fun_eq2 [OF M_basic_L]
   5.112 +  and funspace_succ = M_basic.funspace_succ [OF M_basic_L]
   5.113 +  and finite_funspace_closed = M_basic.finite_funspace_closed [OF M_basic_L]
   5.114  
   5.115 -lemmas is_recfun_equal = M_axioms.is_recfun_equal [OF M_axioms_L]
   5.116 -  and is_recfun_cut = M_axioms.is_recfun_cut [OF M_axioms_L]
   5.117 -  and is_recfun_functional = M_axioms.is_recfun_functional [OF M_axioms_L]
   5.118 -  and is_recfun_relativize = M_axioms.is_recfun_relativize [OF M_axioms_L]
   5.119 -  and is_recfun_restrict = M_axioms.is_recfun_restrict [OF M_axioms_L]
   5.120 -  and univalent_is_recfun = M_axioms.univalent_is_recfun [OF M_axioms_L]
   5.121 -  and exists_is_recfun_indstep = M_axioms.exists_is_recfun_indstep [OF M_axioms_L]
   5.122 -  and wellfounded_exists_is_recfun = M_axioms.wellfounded_exists_is_recfun [OF M_axioms_L]
   5.123 -  and wf_exists_is_recfun = M_axioms.wf_exists_is_recfun [OF M_axioms_L]
   5.124 -  and is_recfun_abs = M_axioms.is_recfun_abs [OF M_axioms_L]
   5.125 -  and irreflexive_abs = M_axioms.irreflexive_abs [OF M_axioms_L]
   5.126 -  and transitive_rel_abs = M_axioms.transitive_rel_abs [OF M_axioms_L]
   5.127 -  and linear_rel_abs = M_axioms.linear_rel_abs [OF M_axioms_L]
   5.128 -  and wellordered_is_trans_on = M_axioms.wellordered_is_trans_on [OF M_axioms_L]
   5.129 -  and wellordered_is_linear = M_axioms.wellordered_is_linear [OF M_axioms_L]
   5.130 -  and wellordered_is_wellfounded_on = M_axioms.wellordered_is_wellfounded_on [OF M_axioms_L]
   5.131 -  and wellfounded_imp_wellfounded_on = M_axioms.wellfounded_imp_wellfounded_on [OF M_axioms_L]
   5.132 -  and wellfounded_on_subset_A = M_axioms.wellfounded_on_subset_A [OF M_axioms_L]
   5.133 -  and wellfounded_on_iff_wellfounded = M_axioms.wellfounded_on_iff_wellfounded [OF M_axioms_L]
   5.134 -  and wellfounded_on_imp_wellfounded = M_axioms.wellfounded_on_imp_wellfounded [OF M_axioms_L]
   5.135 -  and wellfounded_on_field_imp_wellfounded = M_axioms.wellfounded_on_field_imp_wellfounded [OF M_axioms_L]
   5.136 -  and wellfounded_iff_wellfounded_on_field = M_axioms.wellfounded_iff_wellfounded_on_field [OF M_axioms_L]
   5.137 -  and wellfounded_induct = M_axioms.wellfounded_induct [OF M_axioms_L]
   5.138 -  and wellfounded_on_induct = M_axioms.wellfounded_on_induct [OF M_axioms_L]
   5.139 -  and wellfounded_on_induct2 = M_axioms.wellfounded_on_induct2 [OF M_axioms_L]
   5.140 -  and linear_imp_relativized = M_axioms.linear_imp_relativized [OF M_axioms_L]
   5.141 -  and trans_on_imp_relativized = M_axioms.trans_on_imp_relativized [OF M_axioms_L]
   5.142 -  and wf_on_imp_relativized = M_axioms.wf_on_imp_relativized [OF M_axioms_L]
   5.143 -  and wf_imp_relativized = M_axioms.wf_imp_relativized [OF M_axioms_L]
   5.144 -  and well_ord_imp_relativized = M_axioms.well_ord_imp_relativized [OF M_axioms_L]
   5.145 -  and order_isomorphism_abs = M_axioms.order_isomorphism_abs [OF M_axioms_L]
   5.146 -  and pred_set_abs = M_axioms.pred_set_abs [OF M_axioms_L]
   5.147 +lemmas is_recfun_equal = M_basic.is_recfun_equal [OF M_basic_L]
   5.148 +  and is_recfun_cut = M_basic.is_recfun_cut [OF M_basic_L]
   5.149 +  and is_recfun_functional = M_basic.is_recfun_functional [OF M_basic_L]
   5.150 +  and is_recfun_relativize = M_basic.is_recfun_relativize [OF M_basic_L]
   5.151 +  and is_recfun_restrict = M_basic.is_recfun_restrict [OF M_basic_L]
   5.152 +  and univalent_is_recfun = M_basic.univalent_is_recfun [OF M_basic_L]
   5.153 +  and exists_is_recfun_indstep = M_basic.exists_is_recfun_indstep [OF M_basic_L]
   5.154 +  and wellfounded_exists_is_recfun = M_basic.wellfounded_exists_is_recfun [OF M_basic_L]
   5.155 +  and wf_exists_is_recfun = M_basic.wf_exists_is_recfun [OF M_basic_L]
   5.156 +  and is_recfun_abs = M_basic.is_recfun_abs [OF M_basic_L]
   5.157 +  and irreflexive_abs = M_basic.irreflexive_abs [OF M_basic_L]
   5.158 +  and transitive_rel_abs = M_basic.transitive_rel_abs [OF M_basic_L]
   5.159 +  and linear_rel_abs = M_basic.linear_rel_abs [OF M_basic_L]
   5.160 +  and wellordered_is_trans_on = M_basic.wellordered_is_trans_on [OF M_basic_L]
   5.161 +  and wellordered_is_linear = M_basic.wellordered_is_linear [OF M_basic_L]
   5.162 +  and wellordered_is_wellfounded_on = M_basic.wellordered_is_wellfounded_on [OF M_basic_L]
   5.163 +  and wellfounded_imp_wellfounded_on = M_basic.wellfounded_imp_wellfounded_on [OF M_basic_L]
   5.164 +  and wellfounded_on_subset_A = M_basic.wellfounded_on_subset_A [OF M_basic_L]
   5.165 +  and wellfounded_on_iff_wellfounded = M_basic.wellfounded_on_iff_wellfounded [OF M_basic_L]
   5.166 +  and wellfounded_on_imp_wellfounded = M_basic.wellfounded_on_imp_wellfounded [OF M_basic_L]
   5.167 +  and wellfounded_on_field_imp_wellfounded = M_basic.wellfounded_on_field_imp_wellfounded [OF M_basic_L]
   5.168 +  and wellfounded_iff_wellfounded_on_field = M_basic.wellfounded_iff_wellfounded_on_field [OF M_basic_L]
   5.169 +  and wellfounded_induct = M_basic.wellfounded_induct [OF M_basic_L]
   5.170 +  and wellfounded_on_induct = M_basic.wellfounded_on_induct [OF M_basic_L]
   5.171 +  and wellfounded_on_induct2 = M_basic.wellfounded_on_induct2 [OF M_basic_L]
   5.172 +  and linear_imp_relativized = M_basic.linear_imp_relativized [OF M_basic_L]
   5.173 +  and trans_on_imp_relativized = M_basic.trans_on_imp_relativized [OF M_basic_L]
   5.174 +  and wf_on_imp_relativized = M_basic.wf_on_imp_relativized [OF M_basic_L]
   5.175 +  and wf_imp_relativized = M_basic.wf_imp_relativized [OF M_basic_L]
   5.176 +  and well_ord_imp_relativized = M_basic.well_ord_imp_relativized [OF M_basic_L]
   5.177 +  and order_isomorphism_abs = M_basic.order_isomorphism_abs [OF M_basic_L]
   5.178 +  and pred_set_abs = M_basic.pred_set_abs [OF M_basic_L]
   5.179  
   5.180 -lemmas pred_closed = M_axioms.pred_closed [OF M_axioms_L]
   5.181 -  and membership_abs = M_axioms.membership_abs [OF M_axioms_L]
   5.182 -  and M_Memrel_iff = M_axioms.M_Memrel_iff [OF M_axioms_L]
   5.183 -  and Memrel_closed = M_axioms.Memrel_closed [OF M_axioms_L]
   5.184 -  and wellordered_iso_predD = M_axioms.wellordered_iso_predD [OF M_axioms_L]
   5.185 -  and wellordered_iso_pred_eq = M_axioms.wellordered_iso_pred_eq [OF M_axioms_L]
   5.186 -  and wellfounded_on_asym = M_axioms.wellfounded_on_asym [OF M_axioms_L]
   5.187 -  and wellordered_asym = M_axioms.wellordered_asym [OF M_axioms_L]
   5.188 -  and ord_iso_pred_imp_lt = M_axioms.ord_iso_pred_imp_lt [OF M_axioms_L]
   5.189 -  and obase_iff = M_axioms.obase_iff [OF M_axioms_L]
   5.190 -  and omap_iff = M_axioms.omap_iff [OF M_axioms_L]
   5.191 -  and omap_unique = M_axioms.omap_unique [OF M_axioms_L]
   5.192 -  and omap_yields_Ord = M_axioms.omap_yields_Ord [OF M_axioms_L]
   5.193 -  and otype_iff = M_axioms.otype_iff [OF M_axioms_L]
   5.194 -  and otype_eq_range = M_axioms.otype_eq_range [OF M_axioms_L]
   5.195 -  and Ord_otype = M_axioms.Ord_otype [OF M_axioms_L]
   5.196 -  and domain_omap = M_axioms.domain_omap [OF M_axioms_L]
   5.197 -  and omap_subset = M_axioms.omap_subset [OF M_axioms_L]
   5.198 -  and omap_funtype = M_axioms.omap_funtype [OF M_axioms_L]
   5.199 -  and wellordered_omap_bij = M_axioms.wellordered_omap_bij [OF M_axioms_L]
   5.200 -  and omap_ord_iso = M_axioms.omap_ord_iso [OF M_axioms_L]
   5.201 -  and Ord_omap_image_pred = M_axioms.Ord_omap_image_pred [OF M_axioms_L]
   5.202 -  and restrict_omap_ord_iso = M_axioms.restrict_omap_ord_iso [OF M_axioms_L]
   5.203 -  and obase_equals = M_axioms.obase_equals [OF M_axioms_L]
   5.204 -  and omap_ord_iso_otype = M_axioms.omap_ord_iso_otype [OF M_axioms_L]
   5.205 -  and obase_exists = M_axioms.obase_exists [OF M_axioms_L]
   5.206 -  and omap_exists = M_axioms.omap_exists [OF M_axioms_L]
   5.207 -  and otype_exists = M_axioms.otype_exists [OF M_axioms_L]
   5.208 -  and omap_ord_iso_otype' = M_axioms.omap_ord_iso_otype' [OF M_axioms_L]
   5.209 -  and ordertype_exists = M_axioms.ordertype_exists [OF M_axioms_L]
   5.210 -  and relativized_imp_well_ord = M_axioms.relativized_imp_well_ord [OF M_axioms_L]
   5.211 -  and well_ord_abs = M_axioms.well_ord_abs [OF M_axioms_L]
   5.212 +lemmas pred_closed = M_basic.pred_closed [OF M_basic_L]
   5.213 +  and membership_abs = M_basic.membership_abs [OF M_basic_L]
   5.214 +  and M_Memrel_iff = M_basic.M_Memrel_iff [OF M_basic_L]
   5.215 +  and Memrel_closed = M_basic.Memrel_closed [OF M_basic_L]
   5.216 +  and wellordered_iso_predD = M_basic.wellordered_iso_predD [OF M_basic_L]
   5.217 +  and wellordered_iso_pred_eq = M_basic.wellordered_iso_pred_eq [OF M_basic_L]
   5.218 +  and wellfounded_on_asym = M_basic.wellfounded_on_asym [OF M_basic_L]
   5.219 +  and wellordered_asym = M_basic.wellordered_asym [OF M_basic_L]
   5.220 +  and ord_iso_pred_imp_lt = M_basic.ord_iso_pred_imp_lt [OF M_basic_L]
   5.221 +  and obase_iff = M_basic.obase_iff [OF M_basic_L]
   5.222 +  and omap_iff = M_basic.omap_iff [OF M_basic_L]
   5.223 +  and omap_unique = M_basic.omap_unique [OF M_basic_L]
   5.224 +  and omap_yields_Ord = M_basic.omap_yields_Ord [OF M_basic_L]
   5.225 +  and otype_iff = M_basic.otype_iff [OF M_basic_L]
   5.226 +  and otype_eq_range = M_basic.otype_eq_range [OF M_basic_L]
   5.227 +  and Ord_otype = M_basic.Ord_otype [OF M_basic_L]
   5.228 +  and domain_omap = M_basic.domain_omap [OF M_basic_L]
   5.229 +  and omap_subset = M_basic.omap_subset [OF M_basic_L]
   5.230 +  and omap_funtype = M_basic.omap_funtype [OF M_basic_L]
   5.231 +  and wellordered_omap_bij = M_basic.wellordered_omap_bij [OF M_basic_L]
   5.232 +  and omap_ord_iso = M_basic.omap_ord_iso [OF M_basic_L]
   5.233 +  and Ord_omap_image_pred = M_basic.Ord_omap_image_pred [OF M_basic_L]
   5.234 +  and restrict_omap_ord_iso = M_basic.restrict_omap_ord_iso [OF M_basic_L]
   5.235 +  and obase_equals = M_basic.obase_equals [OF M_basic_L]
   5.236 +  and omap_ord_iso_otype = M_basic.omap_ord_iso_otype [OF M_basic_L]
   5.237 +  and obase_exists = M_basic.obase_exists [OF M_basic_L]
   5.238 +  and omap_exists = M_basic.omap_exists [OF M_basic_L]
   5.239 +  and otype_exists = M_basic.otype_exists [OF M_basic_L]
   5.240 +  and omap_ord_iso_otype' = M_basic.omap_ord_iso_otype' [OF M_basic_L]
   5.241 +  and ordertype_exists = M_basic.ordertype_exists [OF M_basic_L]
   5.242 +  and relativized_imp_well_ord = M_basic.relativized_imp_well_ord [OF M_basic_L]
   5.243 +  and well_ord_abs = M_basic.well_ord_abs [OF M_basic_L]
   5.244  
   5.245  declare cartprod_closed [intro, simp]
   5.246  declare sum_closed [intro, simp]
     6.1 --- a/src/ZF/Constructible/WF_absolute.thy	Tue Sep 10 16:47:17 2002 +0200
     6.2 +++ b/src/ZF/Constructible/WF_absolute.thy	Tue Sep 10 16:51:31 2002 +0200
     6.3 @@ -139,7 +139,7 @@
     6.4      "tran_closure(M,r,t) ==
     6.5           \<exists>s[M]. rtran_closure(M,r,s) & composition(M,r,s,t)"
     6.6  
     6.7 -lemma (in M_axioms) rtran_closure_mem_iff:
     6.8 +lemma (in M_basic) rtran_closure_mem_iff:
     6.9       "[|M(A); M(r); M(p)|]
    6.10        ==> rtran_closure_mem(M,A,r,p) <->
    6.11            (\<exists>n[M]. n\<in>nat & 
    6.12 @@ -149,7 +149,7 @@
    6.13  by (simp add: rtran_closure_mem_def Ord_succ_mem_iff nat_0_le [THEN ltD]) 
    6.14  
    6.15  
    6.16 -locale M_trancl = M_axioms +
    6.17 +locale M_trancl = M_basic +
    6.18    assumes rtrancl_separation:
    6.19  	 "[| M(r); M(A) |] ==> separation (M, rtran_closure_mem(M,A,r))"
    6.20        and wellfounded_trancl_separation:
     7.1 --- a/src/ZF/Constructible/WFrec.thy	Tue Sep 10 16:47:17 2002 +0200
     7.2 +++ b/src/ZF/Constructible/WFrec.thy	Tue Sep 10 16:51:31 2002 +0200
     7.3 @@ -74,7 +74,7 @@
     7.4  
     7.5  subsection{*Reworking of the Recursion Theory Within @{term M}*}
     7.6  
     7.7 -lemma (in M_axioms) is_recfun_separation':
     7.8 +lemma (in M_basic) is_recfun_separation':
     7.9      "[| f \<in> r -`` {a} \<rightarrow> range(f); g \<in> r -`` {b} \<rightarrow> range(g);
    7.10          M(r); M(f); M(g); M(a); M(b) |] 
    7.11       ==> separation(M, \<lambda>x. \<not> (\<langle>x, a\<rangle> \<in> r \<longrightarrow> \<langle>x, b\<rangle> \<in> r \<longrightarrow> f ` x = g ` x))"
    7.12 @@ -89,7 +89,7 @@
    7.13        The last three M-premises are redundant because of @{term "M(r)"}, 
    7.14        but without them we'd have to undertake
    7.15        more work to set up the induction formula.*}
    7.16 -lemma (in M_axioms) is_recfun_equal [rule_format]: 
    7.17 +lemma (in M_basic) is_recfun_equal [rule_format]: 
    7.18      "[|is_recfun(r,a,H,f);  is_recfun(r,b,H,g);  
    7.19         wellfounded(M,r);  trans(r);
    7.20         M(f); M(g); M(r); M(x); M(a); M(b) |] 
    7.21 @@ -112,7 +112,7 @@
    7.22  apply (blast intro: transD sym) 
    7.23  done
    7.24  
    7.25 -lemma (in M_axioms) is_recfun_cut: 
    7.26 +lemma (in M_basic) is_recfun_cut: 
    7.27      "[|is_recfun(r,a,H,f);  is_recfun(r,b,H,g);  
    7.28         wellfounded(M,r); trans(r); 
    7.29         M(f); M(g); M(r); <b,a> \<in> r |]   
    7.30 @@ -124,7 +124,7 @@
    7.31  apply (blast intro: is_recfun_equal transD dest: transM) 
    7.32  done
    7.33  
    7.34 -lemma (in M_axioms) is_recfun_functional:
    7.35 +lemma (in M_basic) is_recfun_functional:
    7.36       "[|is_recfun(r,a,H,f);  is_recfun(r,a,H,g);  
    7.37         wellfounded(M,r); trans(r); M(f); M(g); M(r) |] ==> f=g"
    7.38  apply (rule fun_extension)
    7.39 @@ -133,7 +133,7 @@
    7.40  done 
    7.41  
    7.42  text{*Tells us that @{text is_recfun} can (in principle) be relativized.*}
    7.43 -lemma (in M_axioms) is_recfun_relativize:
    7.44 +lemma (in M_basic) is_recfun_relativize:
    7.45    "[| M(r); M(f); \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |] 
    7.46     ==> is_recfun(r,a,H,f) <->
    7.47         (\<forall>z[M]. z \<in> f <-> 
    7.48 @@ -154,7 +154,7 @@
    7.49  apply (simp add: is_recfun_imp_function function_restrictI) 
    7.50  done
    7.51  
    7.52 -lemma (in M_axioms) is_recfun_restrict:
    7.53 +lemma (in M_basic) is_recfun_restrict:
    7.54       "[| wellfounded(M,r); trans(r); is_recfun(r,x,H,f); \<langle>y,x\<rangle> \<in> r; 
    7.55         M(r); M(f); 
    7.56         \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |]
    7.57 @@ -171,7 +171,7 @@
    7.58  apply (blast intro: apply_recfun dest: transD)
    7.59  done
    7.60   
    7.61 -lemma (in M_axioms) restrict_Y_lemma:
    7.62 +lemma (in M_basic) restrict_Y_lemma:
    7.63     "[| wellfounded(M,r); trans(r); M(r);
    7.64         \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g));  M(Y);
    7.65         \<forall>b[M]. 
    7.66 @@ -201,7 +201,7 @@
    7.67  done
    7.68  
    7.69  text{*For typical applications of Replacement for recursive definitions*}
    7.70 -lemma (in M_axioms) univalent_is_recfun:
    7.71 +lemma (in M_basic) univalent_is_recfun:
    7.72       "[|wellfounded(M,r); trans(r); M(r)|]
    7.73        ==> univalent (M, A, \<lambda>x p. 
    7.74                \<exists>y[M]. p = \<langle>x,y\<rangle> & (\<exists>f[M]. is_recfun(r,x,H,f) & y = H(x,f)))"
    7.75 @@ -212,7 +212,7 @@
    7.76  
    7.77  text{*Proof of the inductive step for @{text exists_is_recfun}, since
    7.78        we must prove two versions.*}
    7.79 -lemma (in M_axioms) exists_is_recfun_indstep:
    7.80 +lemma (in M_basic) exists_is_recfun_indstep:
    7.81      "[|\<forall>y. \<langle>y, a1\<rangle> \<in> r --> (\<exists>f[M]. is_recfun(r, y, H, f)); 
    7.82         wellfounded(M,r); trans(r); M(r); M(a1);
    7.83         strong_replacement(M, \<lambda>x z. 
    7.84 @@ -245,7 +245,7 @@
    7.85  
    7.86  text{*Relativized version, when we have the (currently weaker) premise
    7.87        @{term "wellfounded(M,r)"}*}
    7.88 -lemma (in M_axioms) wellfounded_exists_is_recfun:
    7.89 +lemma (in M_basic) wellfounded_exists_is_recfun:
    7.90      "[|wellfounded(M,r);  trans(r);  
    7.91         separation(M, \<lambda>x. ~ (\<exists>f[M]. is_recfun(r, x, H, f)));
    7.92         strong_replacement(M, \<lambda>x z. 
    7.93 @@ -257,7 +257,7 @@
    7.94  apply (rule exists_is_recfun_indstep, assumption+)
    7.95  done
    7.96  
    7.97 -lemma (in M_axioms) wf_exists_is_recfun [rule_format]:
    7.98 +lemma (in M_basic) wf_exists_is_recfun [rule_format]:
    7.99      "[|wf(r);  trans(r);  M(r);  
   7.100         strong_replacement(M, \<lambda>x z. 
   7.101           \<exists>y[M]. \<exists>g[M]. pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); 
   7.102 @@ -291,7 +291,7 @@
   7.103          strong_replacement(M, 
   7.104               \<lambda>x z. \<exists>y[M]. pair(M,x,y,z) & is_wfrec(M,MH,r,x,y))"
   7.105  
   7.106 -lemma (in M_axioms) is_recfun_abs:
   7.107 +lemma (in M_basic) is_recfun_abs:
   7.108       "[| \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g));  M(r); M(a); M(f); 
   7.109           relativize2(M,MH,H) |] 
   7.110        ==> M_is_recfun(M,MH,r,a,f) <-> is_recfun(r,a,H,f)"
   7.111 @@ -306,7 +306,7 @@
   7.112        ==> M_is_recfun(M,MH,r,a,f) <-> M_is_recfun(M,MH',r',a',f')"
   7.113  by (simp add: M_is_recfun_def) 
   7.114  
   7.115 -lemma (in M_axioms) is_wfrec_abs:
   7.116 +lemma (in M_basic) is_wfrec_abs:
   7.117       "[| \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)); 
   7.118           relativize2(M,MH,H);  M(r); M(a); M(z) |]
   7.119        ==> is_wfrec(M,MH,r,a,z) <-> 
   7.120 @@ -314,7 +314,7 @@
   7.121  by (simp add: is_wfrec_def relativize2_def is_recfun_abs)
   7.122  
   7.123  text{*Relating @{term wfrec_replacement} to native constructs*}
   7.124 -lemma (in M_axioms) wfrec_replacement':
   7.125 +lemma (in M_basic) wfrec_replacement':
   7.126    "[|wfrec_replacement(M,MH,r);
   7.127       \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)); 
   7.128       relativize2(M,MH,H);  M(r)|] 
   7.129 @@ -381,7 +381,7 @@
   7.130                    fun_apply(M,f,j,fj) & fj = k"
   7.131  
   7.132  
   7.133 -locale M_ord_arith = M_axioms +
   7.134 +locale M_ord_arith = M_basic +
   7.135    assumes oadd_strong_replacement:
   7.136     "[| M(i); M(j) |] ==>
   7.137      strong_replacement(M, 
     8.1 --- a/src/ZF/Constructible/Wellorderings.thy	Tue Sep 10 16:47:17 2002 +0200
     8.2 +++ b/src/ZF/Constructible/Wellorderings.thy	Tue Sep 10 16:51:31 2002 +0200
     8.3 @@ -49,63 +49,63 @@
     8.4  
     8.5  subsubsection {*Trivial absoluteness proofs*}
     8.6  
     8.7 -lemma (in M_axioms) irreflexive_abs [simp]: 
     8.8 +lemma (in M_basic) irreflexive_abs [simp]: 
     8.9       "M(A) ==> irreflexive(M,A,r) <-> irrefl(A,r)"
    8.10  by (simp add: irreflexive_def irrefl_def)
    8.11  
    8.12 -lemma (in M_axioms) transitive_rel_abs [simp]: 
    8.13 +lemma (in M_basic) transitive_rel_abs [simp]: 
    8.14       "M(A) ==> transitive_rel(M,A,r) <-> trans[A](r)"
    8.15  by (simp add: transitive_rel_def trans_on_def)
    8.16  
    8.17 -lemma (in M_axioms) linear_rel_abs [simp]: 
    8.18 +lemma (in M_basic) linear_rel_abs [simp]: 
    8.19       "M(A) ==> linear_rel(M,A,r) <-> linear(A,r)"
    8.20  by (simp add: linear_rel_def linear_def)
    8.21  
    8.22 -lemma (in M_axioms) wellordered_is_trans_on: 
    8.23 +lemma (in M_basic) wellordered_is_trans_on: 
    8.24      "[| wellordered(M,A,r); M(A) |] ==> trans[A](r)"
    8.25  by (auto simp add: wellordered_def)
    8.26  
    8.27 -lemma (in M_axioms) wellordered_is_linear: 
    8.28 +lemma (in M_basic) wellordered_is_linear: 
    8.29      "[| wellordered(M,A,r); M(A) |] ==> linear(A,r)"
    8.30  by (auto simp add: wellordered_def)
    8.31  
    8.32 -lemma (in M_axioms) wellordered_is_wellfounded_on: 
    8.33 +lemma (in M_basic) wellordered_is_wellfounded_on: 
    8.34      "[| wellordered(M,A,r); M(A) |] ==> wellfounded_on(M,A,r)"
    8.35  by (auto simp add: wellordered_def)
    8.36  
    8.37 -lemma (in M_axioms) wellfounded_imp_wellfounded_on: 
    8.38 +lemma (in M_basic) wellfounded_imp_wellfounded_on: 
    8.39      "[| wellfounded(M,r); M(A) |] ==> wellfounded_on(M,A,r)"
    8.40  by (auto simp add: wellfounded_def wellfounded_on_def)
    8.41  
    8.42 -lemma (in M_axioms) wellfounded_on_subset_A:
    8.43 +lemma (in M_basic) wellfounded_on_subset_A:
    8.44       "[| wellfounded_on(M,A,r);  B<=A |] ==> wellfounded_on(M,B,r)"
    8.45  by (simp add: wellfounded_on_def, blast)
    8.46  
    8.47  
    8.48  subsubsection {*Well-founded relations*}
    8.49  
    8.50 -lemma  (in M_axioms) wellfounded_on_iff_wellfounded:
    8.51 +lemma  (in M_basic) wellfounded_on_iff_wellfounded:
    8.52       "wellfounded_on(M,A,r) <-> wellfounded(M, r \<inter> A*A)"
    8.53  apply (simp add: wellfounded_on_def wellfounded_def, safe)
    8.54   apply blast 
    8.55  apply (drule_tac x=x in rspec, assumption, blast) 
    8.56  done
    8.57  
    8.58 -lemma (in M_axioms) wellfounded_on_imp_wellfounded:
    8.59 +lemma (in M_basic) wellfounded_on_imp_wellfounded:
    8.60       "[|wellfounded_on(M,A,r); r \<subseteq> A*A|] ==> wellfounded(M,r)"
    8.61  by (simp add: wellfounded_on_iff_wellfounded subset_Int_iff)
    8.62  
    8.63 -lemma (in M_axioms) wellfounded_on_field_imp_wellfounded:
    8.64 +lemma (in M_basic) wellfounded_on_field_imp_wellfounded:
    8.65       "wellfounded_on(M, field(r), r) ==> wellfounded(M,r)"
    8.66  by (simp add: wellfounded_def wellfounded_on_iff_wellfounded, fast)
    8.67  
    8.68 -lemma (in M_axioms) wellfounded_iff_wellfounded_on_field:
    8.69 +lemma (in M_basic) wellfounded_iff_wellfounded_on_field:
    8.70       "M(r) ==> wellfounded(M,r) <-> wellfounded_on(M, field(r), r)"
    8.71  by (blast intro: wellfounded_imp_wellfounded_on
    8.72                   wellfounded_on_field_imp_wellfounded)
    8.73  
    8.74  (*Consider the least z in domain(r) such that P(z) does not hold...*)
    8.75 -lemma (in M_axioms) wellfounded_induct: 
    8.76 +lemma (in M_basic) wellfounded_induct: 
    8.77       "[| wellfounded(M,r); M(a); M(r); separation(M, \<lambda>x. ~P(x));  
    8.78           \<forall>x. M(x) & (\<forall>y. <y,x> \<in> r --> P(y)) --> P(x) |]
    8.79        ==> P(a)";
    8.80 @@ -114,7 +114,7 @@
    8.81  apply (blast dest: transM)+
    8.82  done
    8.83  
    8.84 -lemma (in M_axioms) wellfounded_on_induct: 
    8.85 +lemma (in M_basic) wellfounded_on_induct: 
    8.86       "[| a\<in>A;  wellfounded_on(M,A,r);  M(A);  
    8.87         separation(M, \<lambda>x. x\<in>A --> ~P(x));  
    8.88         \<forall>x\<in>A. M(x) & (\<forall>y\<in>A. <y,x> \<in> r --> P(y)) --> P(x) |]
    8.89 @@ -126,7 +126,7 @@
    8.90  
    8.91  text{*The assumption @{term "r \<subseteq> A*A"} justifies strengthening the induction
    8.92        hypothesis by removing the restriction to @{term A}.*}
    8.93 -lemma (in M_axioms) wellfounded_on_induct2: 
    8.94 +lemma (in M_basic) wellfounded_on_induct2: 
    8.95       "[| a\<in>A;  wellfounded_on(M,A,r);  M(A);  r \<subseteq> A*A;  
    8.96         separation(M, \<lambda>x. x\<in>A --> ~P(x));  
    8.97         \<forall>x\<in>A. M(x) & (\<forall>y. <y,x> \<in> r --> P(y)) --> P(x) |]
    8.98 @@ -136,27 +136,27 @@
    8.99  
   8.100  subsubsection {*Kunen's lemma IV 3.14, page 123*}
   8.101  
   8.102 -lemma (in M_axioms) linear_imp_relativized: 
   8.103 +lemma (in M_basic) linear_imp_relativized: 
   8.104       "linear(A,r) ==> linear_rel(M,A,r)" 
   8.105  by (simp add: linear_def linear_rel_def) 
   8.106  
   8.107 -lemma (in M_axioms) trans_on_imp_relativized: 
   8.108 +lemma (in M_basic) trans_on_imp_relativized: 
   8.109       "trans[A](r) ==> transitive_rel(M,A,r)" 
   8.110  by (unfold transitive_rel_def trans_on_def, blast) 
   8.111  
   8.112 -lemma (in M_axioms) wf_on_imp_relativized: 
   8.113 +lemma (in M_basic) wf_on_imp_relativized: 
   8.114       "wf[A](r) ==> wellfounded_on(M,A,r)" 
   8.115  apply (simp add: wellfounded_on_def wf_def wf_on_def, clarify) 
   8.116  apply (drule_tac x=x in spec, blast) 
   8.117  done
   8.118  
   8.119 -lemma (in M_axioms) wf_imp_relativized: 
   8.120 +lemma (in M_basic) wf_imp_relativized: 
   8.121       "wf(r) ==> wellfounded(M,r)" 
   8.122  apply (simp add: wellfounded_def wf_def, clarify) 
   8.123  apply (drule_tac x=x in spec, blast) 
   8.124  done
   8.125  
   8.126 -lemma (in M_axioms) well_ord_imp_relativized: 
   8.127 +lemma (in M_basic) well_ord_imp_relativized: 
   8.128       "well_ord(A,r) ==> wellordered(M,A,r)" 
   8.129  by (simp add: wellordered_def well_ord_def tot_ord_def part_ord_def
   8.130         linear_imp_relativized trans_on_imp_relativized wf_on_imp_relativized)
   8.131 @@ -164,24 +164,24 @@
   8.132  
   8.133  subsection{* Relativized versions of order-isomorphisms and order types *}
   8.134  
   8.135 -lemma (in M_axioms) order_isomorphism_abs [simp]: 
   8.136 +lemma (in M_basic) order_isomorphism_abs [simp]: 
   8.137       "[| M(A); M(B); M(f) |] 
   8.138        ==> order_isomorphism(M,A,r,B,s,f) <-> f \<in> ord_iso(A,r,B,s)"
   8.139  by (simp add: apply_closed order_isomorphism_def ord_iso_def)
   8.140  
   8.141 -lemma (in M_axioms) pred_set_abs [simp]: 
   8.142 +lemma (in M_basic) pred_set_abs [simp]: 
   8.143       "[| M(r); M(B) |] ==> pred_set(M,A,x,r,B) <-> B = Order.pred(A,x,r)"
   8.144  apply (simp add: pred_set_def Order.pred_def)
   8.145  apply (blast dest: transM) 
   8.146  done
   8.147  
   8.148 -lemma (in M_axioms) pred_closed [intro,simp]: 
   8.149 +lemma (in M_basic) pred_closed [intro,simp]: 
   8.150       "[| M(A); M(r); M(x) |] ==> M(Order.pred(A,x,r))"
   8.151  apply (simp add: Order.pred_def) 
   8.152  apply (insert pred_separation [of r x], simp) 
   8.153  done
   8.154  
   8.155 -lemma (in M_axioms) membership_abs [simp]: 
   8.156 +lemma (in M_basic) membership_abs [simp]: 
   8.157       "[| M(r); M(A) |] ==> membership(M,A,r) <-> r = Memrel(A)"
   8.158  apply (simp add: membership_def Memrel_def, safe)
   8.159    apply (rule equalityI) 
   8.160 @@ -194,14 +194,14 @@
   8.161   apply auto 
   8.162  done
   8.163  
   8.164 -lemma (in M_axioms) M_Memrel_iff:
   8.165 +lemma (in M_basic) M_Memrel_iff:
   8.166       "M(A) ==> 
   8.167        Memrel(A) = {z \<in> A*A. \<exists>x[M]. \<exists>y[M]. z = \<langle>x,y\<rangle> & x \<in> y}"
   8.168  apply (simp add: Memrel_def) 
   8.169  apply (blast dest: transM)
   8.170  done 
   8.171  
   8.172 -lemma (in M_axioms) Memrel_closed [intro,simp]: 
   8.173 +lemma (in M_basic) Memrel_closed [intro,simp]: 
   8.174       "M(A) ==> M(Memrel(A))"
   8.175  apply (simp add: M_Memrel_iff) 
   8.176  apply (insert Memrel_separation, simp)
   8.177 @@ -233,7 +233,7 @@
   8.178  
   8.179  text{*Inductive argument for Kunen's Lemma 6.1, etc.
   8.180        Simple proof from Halmos, page 72*}
   8.181 -lemma  (in M_axioms) wellordered_iso_subset_lemma: 
   8.182 +lemma  (in M_basic) wellordered_iso_subset_lemma: 
   8.183       "[| wellordered(M,A,r);  f \<in> ord_iso(A,r, A',r);  A'<= A;  y \<in> A;  
   8.184         M(A);  M(f);  M(r) |] ==> ~ <f`y, y> \<in> r"
   8.185  apply (unfold wellordered_def ord_iso_def)
   8.186 @@ -247,7 +247,7 @@
   8.187  
   8.188  text{*Kunen's Lemma 6.1: there's no order-isomorphism to an initial segment
   8.189        of a well-ordering*}
   8.190 -lemma (in M_axioms) wellordered_iso_predD:
   8.191 +lemma (in M_basic) wellordered_iso_predD:
   8.192       "[| wellordered(M,A,r);  f \<in> ord_iso(A, r, Order.pred(A,x,r), r);  
   8.193         M(A);  M(f);  M(r) |] ==> x \<notin> A"
   8.194  apply (rule notI) 
   8.195 @@ -260,7 +260,7 @@
   8.196  done
   8.197  
   8.198  
   8.199 -lemma (in M_axioms) wellordered_iso_pred_eq_lemma:
   8.200 +lemma (in M_basic) wellordered_iso_pred_eq_lemma:
   8.201       "[| f \<in> \<langle>Order.pred(A,y,r), r\<rangle> \<cong> \<langle>Order.pred(A,x,r), r\<rangle>;
   8.202         wellordered(M,A,r); x\<in>A; y\<in>A; M(A); M(f); M(r) |] ==> <x,y> \<notin> r"
   8.203  apply (frule wellordered_is_trans_on, assumption)
   8.204 @@ -273,7 +273,7 @@
   8.205  
   8.206  
   8.207  text{*Simple consequence of Lemma 6.1*}
   8.208 -lemma (in M_axioms) wellordered_iso_pred_eq:
   8.209 +lemma (in M_basic) wellordered_iso_pred_eq:
   8.210       "[| wellordered(M,A,r);
   8.211         f \<in> ord_iso(Order.pred(A,a,r), r, Order.pred(A,c,r), r);   
   8.212         M(A);  M(f);  M(r);  a\<in>A;  c\<in>A |] ==> a=c"
   8.213 @@ -285,21 +285,21 @@
   8.214  apply (blast dest: wellordered_iso_pred_eq_lemma)+ 
   8.215  done
   8.216  
   8.217 -lemma (in M_axioms) wellfounded_on_asym:
   8.218 +lemma (in M_basic) wellfounded_on_asym:
   8.219       "[| wellfounded_on(M,A,r);  <a,x>\<in>r;  a\<in>A; x\<in>A;  M(A) |] ==> <x,a>\<notin>r"
   8.220  apply (simp add: wellfounded_on_def) 
   8.221  apply (drule_tac x="{x,a}" in rspec) 
   8.222  apply (blast dest: transM)+
   8.223  done
   8.224  
   8.225 -lemma (in M_axioms) wellordered_asym:
   8.226 +lemma (in M_basic) wellordered_asym:
   8.227       "[| wellordered(M,A,r);  <a,x>\<in>r;  a\<in>A; x\<in>A;  M(A) |] ==> <x,a>\<notin>r"
   8.228  by (simp add: wellordered_def, blast dest: wellfounded_on_asym)
   8.229  
   8.230  
   8.231  text{*Surely a shorter proof using lemmas in @{text Order}?
   8.232       Like @{text well_ord_iso_preserving}?*}
   8.233 -lemma (in M_axioms) ord_iso_pred_imp_lt:
   8.234 +lemma (in M_basic) ord_iso_pred_imp_lt:
   8.235       "[| f \<in> ord_iso(Order.pred(A,x,r), r, i, Memrel(i));
   8.236         g \<in> ord_iso(Order.pred(A,y,r), r, j, Memrel(j));
   8.237         wellordered(M,A,r);  x \<in> A;  y \<in> A; M(A); M(r); M(f); M(g); M(j);
   8.238 @@ -372,7 +372,7 @@
   8.239  
   8.240  
   8.241  
   8.242 -lemma (in M_axioms) obase_iff:
   8.243 +lemma (in M_basic) obase_iff:
   8.244       "[| M(A); M(r); M(z) |] 
   8.245        ==> obase(M,A,r,z) <-> 
   8.246            z = {a\<in>A. \<exists>x[M]. \<exists>g[M]. Ord(x) & 
   8.247 @@ -387,7 +387,7 @@
   8.248  
   8.249  text{*Can also be proved with the premise @{term "M(z)"} instead of
   8.250        @{term "M(f)"}, but that version is less useful.*}
   8.251 -lemma (in M_axioms) omap_iff:
   8.252 +lemma (in M_basic) omap_iff:
   8.253       "[| omap(M,A,r,f); M(A); M(r); M(f) |] 
   8.254        ==> z \<in> f <->
   8.255        (\<exists>a\<in>A. \<exists>x[M]. \<exists>g[M]. z = <a,x> & Ord(x) & 
   8.256 @@ -400,18 +400,18 @@
   8.257   apply (blast dest: transM)+
   8.258  done
   8.259  
   8.260 -lemma (in M_axioms) omap_unique:
   8.261 +lemma (in M_basic) omap_unique:
   8.262       "[| omap(M,A,r,f); omap(M,A,r,f'); M(A); M(r); M(f); M(f') |] ==> f' = f" 
   8.263  apply (rule equality_iffI) 
   8.264  apply (simp add: omap_iff) 
   8.265  done
   8.266  
   8.267 -lemma (in M_axioms) omap_yields_Ord:
   8.268 +lemma (in M_basic) omap_yields_Ord:
   8.269       "[| omap(M,A,r,f); \<langle>a,x\<rangle> \<in> f; M(a); M(x) |]  ==> Ord(x)"
   8.270  apply (simp add: omap_def, blast) 
   8.271  done
   8.272  
   8.273 -lemma (in M_axioms) otype_iff:
   8.274 +lemma (in M_basic) otype_iff:
   8.275       "[| otype(M,A,r,i); M(A); M(r); M(i) |] 
   8.276        ==> x \<in> i <-> 
   8.277            (M(x) & Ord(x) & 
   8.278 @@ -423,7 +423,7 @@
   8.279  apply (simp add: omap_iff, blast)
   8.280  done
   8.281  
   8.282 -lemma (in M_axioms) otype_eq_range:
   8.283 +lemma (in M_basic) otype_eq_range:
   8.284       "[| omap(M,A,r,f); otype(M,A,r,i); M(A); M(r); M(f); M(i) |] 
   8.285        ==> i = range(f)"
   8.286  apply (auto simp add: otype_def omap_iff)
   8.287 @@ -431,7 +431,7 @@
   8.288  done
   8.289  
   8.290  
   8.291 -lemma (in M_axioms) Ord_otype:
   8.292 +lemma (in M_basic) Ord_otype:
   8.293       "[| otype(M,A,r,i); trans[A](r); M(A); M(r); M(i) |] ==> Ord(i)"
   8.294  apply (rotate_tac 1) 
   8.295  apply (rule OrdI) 
   8.296 @@ -452,7 +452,7 @@
   8.297  apply (blast intro: restrict_ord_iso ord_iso_sym ltI dest: transM)
   8.298  done
   8.299  
   8.300 -lemma (in M_axioms) domain_omap:
   8.301 +lemma (in M_basic) domain_omap:
   8.302       "[| omap(M,A,r,f);  obase(M,A,r,B); M(A); M(r); M(B); M(f) |] 
   8.303        ==> domain(f) = B"
   8.304  apply (rotate_tac 2) 
   8.305 @@ -461,7 +461,7 @@
   8.306  apply (simp add: domain_iff omap_iff, blast) 
   8.307  done
   8.308  
   8.309 -lemma (in M_axioms) omap_subset: 
   8.310 +lemma (in M_basic) omap_subset: 
   8.311       "[| omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i); 
   8.312         M(A); M(r); M(f); M(B); M(i) |] ==> f \<subseteq> B * i"
   8.313  apply (rotate_tac 3, clarify) 
   8.314 @@ -469,7 +469,7 @@
   8.315  apply (force simp add: otype_iff) 
   8.316  done
   8.317  
   8.318 -lemma (in M_axioms) omap_funtype: 
   8.319 +lemma (in M_basic) omap_funtype: 
   8.320       "[| omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i); 
   8.321         M(A); M(r); M(f); M(B); M(i) |] ==> f \<in> B -> i"
   8.322  apply (rotate_tac 3) 
   8.323 @@ -478,7 +478,7 @@
   8.324  done
   8.325  
   8.326  
   8.327 -lemma (in M_axioms) wellordered_omap_bij:
   8.328 +lemma (in M_basic) wellordered_omap_bij:
   8.329       "[| wellordered(M,A,r); omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i); 
   8.330         M(A); M(r); M(f); M(B); M(i) |] ==> f \<in> bij(B,i)"
   8.331  apply (insert omap_funtype [of A r f B i]) 
   8.332 @@ -492,7 +492,7 @@
   8.333  
   8.334  
   8.335  text{*This is not the final result: we must show @{term "oB(A,r) = A"}*}
   8.336 -lemma (in M_axioms) omap_ord_iso:
   8.337 +lemma (in M_basic) omap_ord_iso:
   8.338       "[| wellordered(M,A,r); omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i); 
   8.339         M(A); M(r); M(f); M(B); M(i) |] ==> f \<in> ord_iso(B,r,i,Memrel(i))"
   8.340  apply (rule ord_isoI)
   8.341 @@ -513,7 +513,7 @@
   8.342  apply (blast dest: ord_iso_pred_imp_lt ltD elim: mem_asym) 
   8.343  done
   8.344  
   8.345 -lemma (in M_axioms) Ord_omap_image_pred:
   8.346 +lemma (in M_basic) Ord_omap_image_pred:
   8.347       "[| wellordered(M,A,r); omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i); 
   8.348         M(A); M(r); M(f); M(B); M(i); b \<in> A |] ==> Ord(f `` Order.pred(A,b,r))"
   8.349  apply (frule wellordered_is_trans_on, assumption)
   8.350 @@ -539,7 +539,7 @@
   8.351  apply (auto simp add: obase_iff)
   8.352  done
   8.353  
   8.354 -lemma (in M_axioms) restrict_omap_ord_iso:
   8.355 +lemma (in M_basic) restrict_omap_ord_iso:
   8.356       "[| wellordered(M,A,r); omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i); 
   8.357         D \<subseteq> B; M(A); M(r); M(f); M(B); M(i) |] 
   8.358        ==> restrict(f,D) \<in> (\<langle>D,r\<rangle> \<cong> \<langle>f``D, Memrel(f``D)\<rangle>)"
   8.359 @@ -550,7 +550,7 @@
   8.360  apply (drule ord_iso_sym, simp) 
   8.361  done
   8.362  
   8.363 -lemma (in M_axioms) obase_equals: 
   8.364 +lemma (in M_basic) obase_equals: 
   8.365       "[| wellordered(M,A,r); omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i);
   8.366         M(A); M(r); M(f); M(B); M(i) |] ==> B = A"
   8.367  apply (rotate_tac 4)
   8.368 @@ -570,21 +570,21 @@
   8.369  
   8.370  text{*Main result: @{term om} gives the order-isomorphism 
   8.371        @{term "\<langle>A,r\<rangle> \<cong> \<langle>i, Memrel(i)\<rangle>"} *}
   8.372 -theorem (in M_axioms) omap_ord_iso_otype:
   8.373 +theorem (in M_basic) omap_ord_iso_otype:
   8.374       "[| wellordered(M,A,r); omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i);
   8.375         M(A); M(r); M(f); M(B); M(i) |] ==> f \<in> ord_iso(A, r, i, Memrel(i))"
   8.376  apply (frule omap_ord_iso, assumption+) 
   8.377  apply (frule obase_equals, assumption+, blast) 
   8.378  done 
   8.379  
   8.380 -lemma (in M_axioms) obase_exists:
   8.381 +lemma (in M_basic) obase_exists:
   8.382       "[| M(A); M(r) |] ==> \<exists>z[M]. obase(M,A,r,z)"
   8.383  apply (simp add: obase_def) 
   8.384  apply (insert obase_separation [of A r])
   8.385  apply (simp add: separation_def)  
   8.386  done
   8.387  
   8.388 -lemma (in M_axioms) omap_exists:
   8.389 +lemma (in M_basic) omap_exists:
   8.390       "[| M(A); M(r) |] ==> \<exists>z[M]. omap(M,A,r,z)"
   8.391  apply (insert obase_exists [of A r]) 
   8.392  apply (simp add: omap_def) 
   8.393 @@ -601,7 +601,7 @@
   8.394  
   8.395  declare rall_simps [simp] rex_simps [simp]
   8.396  
   8.397 -lemma (in M_axioms) otype_exists:
   8.398 +lemma (in M_basic) otype_exists:
   8.399       "[| wellordered(M,A,r); M(A); M(r) |] ==> \<exists>i[M]. otype(M,A,r,i)"
   8.400  apply (insert omap_exists [of A r])  
   8.401  apply (simp add: otype_def, safe)
   8.402 @@ -609,7 +609,7 @@
   8.403  apply blast+
   8.404  done
   8.405  
   8.406 -theorem (in M_axioms) omap_ord_iso_otype':
   8.407 +theorem (in M_basic) omap_ord_iso_otype':
   8.408       "[| wellordered(M,A,r); M(A); M(r) |]
   8.409        ==> \<exists>f[M]. (\<exists>i[M]. Ord(i) & f \<in> ord_iso(A, r, i, Memrel(i)))"
   8.410  apply (insert obase_exists [of A r] omap_exists [of A r] otype_exists [of A r], simp, clarify)
   8.411 @@ -620,7 +620,7 @@
   8.412     apply (simp_all add: wellordered_is_trans_on) 
   8.413  done
   8.414  
   8.415 -lemma (in M_axioms) ordertype_exists:
   8.416 +lemma (in M_basic) ordertype_exists:
   8.417       "[| wellordered(M,A,r); M(A); M(r) |]
   8.418        ==> \<exists>f[M]. (\<exists>i[M]. Ord(i) & f \<in> ord_iso(A, r, i, Memrel(i)))"
   8.419  apply (insert obase_exists [of A r] omap_exists [of A r] otype_exists [of A r], simp, clarify)
   8.420 @@ -632,7 +632,7 @@
   8.421  done
   8.422  
   8.423  
   8.424 -lemma (in M_axioms) relativized_imp_well_ord: 
   8.425 +lemma (in M_basic) relativized_imp_well_ord: 
   8.426       "[| wellordered(M,A,r); M(A); M(r) |] ==> well_ord(A,r)" 
   8.427  apply (insert ordertype_exists [of A r], simp)
   8.428  apply (blast intro: well_ord_ord_iso well_ord_Memrel)  
   8.429 @@ -641,13 +641,13 @@
   8.430  subsection {*Kunen's theorem 5.4, poage 127*}
   8.431  
   8.432  text{*(a) The notion of Wellordering is absolute*}
   8.433 -theorem (in M_axioms) well_ord_abs [simp]: 
   8.434 +theorem (in M_basic) well_ord_abs [simp]: 
   8.435       "[| M(A); M(r) |] ==> wellordered(M,A,r) <-> well_ord(A,r)" 
   8.436  by (blast intro: well_ord_imp_relativized relativized_imp_well_ord)  
   8.437  
   8.438  
   8.439  text{*(b) Order types are absolute*}
   8.440 -lemma (in M_axioms) 
   8.441 +lemma (in M_basic) 
   8.442       "[| wellordered(M,A,r); f \<in> ord_iso(A, r, i, Memrel(i));
   8.443         M(A); M(r); M(f); M(i); Ord(i) |] ==> i = ordertype(A,r)"
   8.444  by (blast intro: Ord_ordertype relativized_imp_well_ord ordertype_ord_iso