src/ZF/Constructible/Datatype_absolute.thy
changeset 13564 1500a2e48d44
parent 13557 6061d0045409
child 13615 449a70d88b38
     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)),