wneuper/isa: comparison src/ZF/Constructible/Datatype

equal deleted inserted replaced

-:7d6c9817c432
+:1500a2e48d44
 iterates_replacement :: "[i=>o, [i,i]=>o, i] => o"
 "iterates_replacement(M,isF,v) ==
 \<forall>n[M]. n\<in>nat -->
 wfrec_replacement(M, iterates_MH(M,isF,v), Memrel(succ(n)))"
-lemma (in M_axioms) iterates_MH_abs:
+lemma (in M_basic) iterates_MH_abs:
 "[| relativize1(M,isF,F); M(n); M(g); M(z) |]
 ==> iterates_MH(M,isF,v,n,g,z) <-> z = nat_case(v, \<lambda>m. F(g`m), n)"
 by (simp add: nat_case_abs [of _ "\<lambda>m. F(g ` m)"]
 relativize1_def iterates_MH_def)
-lemma (in M_axioms) iterates_imp_wfrec_replacement:
+lemma (in M_basic) iterates_imp_wfrec_replacement:
 "[|relativize1(M,isF,F); n \<in> nat; iterates_replacement(M,isF,v)|]
 ==> wfrec_replacement(M, \<lambda>n f z. z = nat_case(v, \<lambda>m. F(f`m), n),
 Memrel(succ(n)))"
 by (simp add: iterates_replacement_def iterates_MH_abs)
 is_list_functor :: "[i=>o,i,i,i] => o"
 "is_list_functor(M,A,X,Z) ==
 \<exists>n1[M]. \<exists>AX[M].
 number1(M,n1) & cartprod(M,A,X,AX) & is_sum(M,n1,AX,Z)"
-lemma (in M_axioms) list_functor_abs [simp]:
+lemma (in M_basic) list_functor_abs [simp]:
 "[| M(A); M(X); M(Z) |] ==> is_list_functor(M,A,X,Z) <-> (Z = {0} + A*X)"
 by (simp add: is_list_functor_def singleton_0 nat_into_M)
 subsection {*formulas without univ*}
 omega(M,nat') & cartprod(M,nat',nat',natnat) &
 is_sum(M,natnat,natnat,natnatsum) &
 cartprod(M,X,X,XX) & is_sum(M,XX,X,X3) &
 is_sum(M,natnatsum,X3,Z)"
-lemma (in M_axioms) formula_functor_abs [simp]:
+lemma (in M_basic) formula_functor_abs [simp]:
 "[| M(X); M(Z) |]
 ==> is_formula_functor(M,X,Z) <->
 Z = ((nat*nat) + (nat*nat)) + (X*X + X)"
 by (simp add: is_formula_functor_def)
 apply (blast intro: list_imp_list_N)
 done
 text{*Express @{term list_rec} without using @{term rank} or @{term Vset},
 neither of which is absolute.*}
-lemma (in M_triv_axioms) list_rec_eq:
+lemma (in M_trivial) list_rec_eq:
 "l \<in> list(A) ==>
 list_rec(a,g,l) =
 transrec (succ(length(l)),
 \<lambda>x h. Lambda (list(A),
 list_case' (a,
 apply (blast intro: list_imp_list_N nat_into_Ord list_N_imp_eq_length
 dest: list_N_imp_length_lt)
 done
 text{*Proof is trivial since @{term length} returns natural numbers.*}
-lemma (in M_triv_axioms) length_closed [intro,simp]:
+lemma (in M_trivial) length_closed [intro,simp]:
 "l \<in> list(A) ==> M(length(l))"
 by (simp add: nat_into_M)
 subsection {*Absoluteness for @{term nth}*}
 apply (erule natE)
 apply (simp add: hd'_Cons)
 apply (simp add: tl'_Cons iterates_commute)
 done
-lemma (in M_axioms) iterates_tl'_closed:
+lemma (in M_basic) iterates_tl'_closed:
 "[|n \<in> nat; M(x)|] ==> M(tl'^n (x))"
 apply (induct_tac n, simp)
 apply (simp add: tl'_Cons tl'_closed)
 done
 is_Member :: "[i=>o,i,i,i] => o"
 --{* because @{term "Member(x,y) \<equiv> Inl(Inl(\<langle>x,y\<rangle>))"}*}
 "is_Member(M,x,y,Z) ==
 	\<exists>p[M]. \<exists>u[M]. pair(M,x,y,p) & is_Inl(M,p,u) & is_Inl(M,u,Z)"
-lemma (in M_triv_axioms) Member_abs [simp]:
+lemma (in M_trivial) Member_abs [simp]:
 "[|M(x); M(y); M(Z)|] ==> is_Member(M,x,y,Z) <-> (Z = Member(x,y))"
 by (simp add: is_Member_def Member_def)
-lemma (in M_triv_axioms) Member_in_M_iff [iff]:
+lemma (in M_trivial) Member_in_M_iff [iff]:
 "M(Member(x,y)) <-> M(x) & M(y)"
 by (simp add: Member_def)
 constdefs
 is_Equal :: "[i=>o,i,i,i] => o"
 --{* because @{term "Equal(x,y) \<equiv> Inl(Inr(\<langle>x,y\<rangle>))"}*}
 "is_Equal(M,x,y,Z) ==
 	\<exists>p[M]. \<exists>u[M]. pair(M,x,y,p) & is_Inr(M,p,u) & is_Inl(M,u,Z)"
-lemma (in M_triv_axioms) Equal_abs [simp]:
+lemma (in M_trivial) Equal_abs [simp]:
 "[|M(x); M(y); M(Z)|] ==> is_Equal(M,x,y,Z) <-> (Z = Equal(x,y))"
 by (simp add: is_Equal_def Equal_def)
-lemma (in M_triv_axioms) Equal_in_M_iff [iff]: "M(Equal(x,y)) <-> M(x) & M(y)"
+lemma (in M_trivial) Equal_in_M_iff [iff]: "M(Equal(x,y)) <-> M(x) & M(y)"
 by (simp add: Equal_def)
 constdefs
 is_Nand :: "[i=>o,i,i,i] => o"
 --{* because @{term "Nand(x,y) \<equiv> Inr(Inl(\<langle>x,y\<rangle>))"}*}
 "is_Nand(M,x,y,Z) ==
 	\<exists>p[M]. \<exists>u[M]. pair(M,x,y,p) & is_Inl(M,p,u) & is_Inr(M,u,Z)"
-lemma (in M_triv_axioms) Nand_abs [simp]:
+lemma (in M_trivial) Nand_abs [simp]:
 "[|M(x); M(y); M(Z)|] ==> is_Nand(M,x,y,Z) <-> (Z = Nand(x,y))"
 by (simp add: is_Nand_def Nand_def)
-lemma (in M_triv_axioms) Nand_in_M_iff [iff]: "M(Nand(x,y)) <-> M(x) & M(y)"
+lemma (in M_trivial) Nand_in_M_iff [iff]: "M(Nand(x,y)) <-> M(x) & M(y)"
 by (simp add: Nand_def)
 constdefs
 is_Forall :: "[i=>o,i,i] => o"
 --{* because @{term "Forall(x) \<equiv> Inr(Inr(p))"}*}
 "is_Forall(M,p,Z) == \<exists>u[M]. is_Inr(M,p,u) & is_Inr(M,u,Z)"
-lemma (in M_triv_axioms) Forall_abs [simp]:
+lemma (in M_trivial) Forall_abs [simp]:
 "[|M(x); M(Z)|] ==> is_Forall(M,x,Z) <-> (Z = Forall(x))"
 by (simp add: is_Forall_def Forall_def)
-lemma (in M_triv_axioms) Forall_in_M_iff [iff]: "M(Forall(x)) <-> M(x)"
+lemma (in M_trivial) Forall_in_M_iff [iff]: "M(Forall(x)) <-> M(x)"
 by (simp add: Forall_def)
 subsection {*Absoluteness for @{term formula_rec}*}
 apply (blast intro: formula_imp_formula_N nat_into_Ord formula_N_imp_eq_depth
 dest: formula_N_imp_depth_lt)
 done
 text{*Proof is trivial since @{term depth} returns natural numbers.*}
-lemma (in M_triv_axioms) depth_closed [intro,simp]:
+lemma (in M_trivial) depth_closed [intro,simp]:
 "p \<in> formula ==> M(depth(p))"
 by (simp add: nat_into_M)
 subsection {*Absoluteness for @{term formula_rec}*}
 successor(M,dp,i) & fun_apply(M,f,p,z) & is_transrec(M,MH,i,f)"
 text{*Unfold @{term formula_rec} to @{term formula_rec_case}.
 Express @{term formula_rec} without using @{term rank} or @{term Vset},
 neither of which is absolute.*}
-lemma (in M_triv_axioms) formula_rec_eq:
+lemma (in M_trivial) formula_rec_eq:
 "p \<in> formula ==>
 formula_rec(a,b,c,d,p) =
 transrec (succ(depth(p)),
 \<lambda>x h. Lambda (formula, formula_rec_case(a,b,c,d,h))) ` p"
 apply (simp add: formula_rec_case_def)

changeset 13564	1500a2e48d44
parent 13557	6061d0045409
child 13615	449a70d88b38