--- a/src/ZF/Constructible/Datatype_absolute.thy Thu Jul 11 16:57:14 2002 +0200
+++ b/src/ZF/Constructible/Datatype_absolute.thy Thu Jul 11 17:18:28 2002 +0200
@@ -105,8 +105,7 @@
z = nat_case(v, \<lambda>m. F(g`m), n))"
by (simp add: iterates_nat_def recursor_def transrec_def
eclose_sing_Ord_eq trans_wfrec_relativize nat_into_M
- wf_Memrel trans_Memrel relation_Memrel nat_case_closed)
-
+ wf_Memrel trans_Memrel relation_Memrel)
lemma (in M_wfrank) iterates_closed [intro,simp]:
"[|n \<in> nat; M(v); \<forall>x[M]. M(F(x));
@@ -121,32 +120,54 @@
wf_Memrel trans_Memrel relation_Memrel nat_case_closed)
+constdefs
+ 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)"
+
+ is_list_case :: "[i=>o,i,i,i,i] => o"
+ "is_list_case(M,A,g,x,y) ==
+ is_nat_case(M, 0,
+ \<lambda>m u. \<exists>gm[M]. fun_apply(M,g,m,gm) & is_list_functor(M,A,gm,u),
+ x, y)"
+
+lemma (in M_axioms) 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)
+
+
locale M_datatypes = M_wfrank +
-(*THEY NEED RELATIVIZATION*)
assumes list_replacement1:
- "[|M(A); n \<in> nat|] ==>
- strong_replacement(M,
- \<lambda>x z. \<exists>y[M]. \<exists>g[M]. \<exists>sucn[M]. \<exists>memr[M].
- pair(M,x,y,z) & successor(M,n,sucn) &
- membership(M,sucn,memr) &
- is_recfun (memr, x,
- \<lambda>n f. nat_case(0, \<lambda>m. {0} + A \<times> f`m, n), g) &
- y = nat_case(0, \<lambda>m. {0} + A \<times> g`m, x))"
+ "[|M(A); n \<in> nat|] ==>
+ strong_replacement(M,
+ \<lambda>x z. \<exists>y[M]. \<exists>g[M]. \<exists>sucn[M]. \<exists>memr[M].
+ pair(M,x,y,z) & successor(M,n,sucn) &
+ membership(M,sucn,memr) &
+ M_is_recfun (M, memr, x,
+ \<lambda>n f z. z = nat_case(0, \<lambda>m. {0} + A * f`m, n), g) &
+ is_nat_case(M, 0,
+ \<lambda>m u. is_list_functor(M,A,g`m,u), x, y))"
+(*THEY NEED RELATIVIZATION*)
and list_replacement2:
- "M(A) ==> strong_replacement(M, \<lambda>x y. y = (\<lambda>X. {0} + A \<times> X)^x (0))"
+ "M(A) ==> strong_replacement(M, \<lambda>x y. y = (\<lambda>X. {0} + A * X)^x (0))"
+
lemma (in M_datatypes) list_replacement1':
"[|M(A); n \<in> nat|]
==> strong_replacement
- (M, \<lambda>x y. \<exists>z[M]. y = \<langle>x,z\<rangle> &
+ (M, \<lambda>x z. \<exists>y[M]. z = \<langle>x,y\<rangle> &
(\<exists>g[M]. is_recfun (Memrel(succ(n)), x,
- \<lambda>n f. nat_case(0, \<lambda>m. {0} + A \<times> f`m, n), g) &
- z = nat_case(0, \<lambda>m. {0} + A \<times> g ` m, x)))"
-by (insert list_replacement1, simp add: nat_into_M)
+ \<lambda>n f. nat_case(0, \<lambda>m. {0} + A * f`m, n), g) &
+ y = nat_case(0, \<lambda>m. {0} + A * g ` m, x)))"
+apply (insert list_replacement1 [of A n], simp add: nat_into_M)
+apply (simp add: nat_into_M apply_abs
+ is_recfun_abs [of "\<lambda>n f. nat_case(0, \<lambda>m. {0} + A * f`m, n)"])
+done
lemma (in M_datatypes) list_replacement2':
- "M(A) ==> strong_replacement(M, \<lambda>x y. y = (\<lambda>X. {0} + A \<times> X)^x (0))"
+ "M(A) ==> strong_replacement(M, \<lambda>x y. y = (\<lambda>X. {0} + A * X)^x (0))"
by (insert list_replacement2, simp add: nat_into_M)
--- a/src/ZF/Constructible/Relative.thy Thu Jul 11 16:57:14 2002 +0200
+++ b/src/ZF/Constructible/Relative.thy Thu Jul 11 17:18:28 2002 +0200
@@ -49,6 +49,12 @@
"cartprod(M,A,B,z) ==
\<forall>u[M]. u \<in> z <-> (\<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>B & pair(M,x,y,u)))"
+ is_sum :: "[i=>o,i,i,i] => o"
+ "is_sum(M,A,B,Z) ==
+ \<exists>A0[M]. \<exists>n1[M]. \<exists>s1[M]. \<exists>B1[M].
+ number1(M,n1) & cartprod(M,n1,A,A0) & upair(M,n1,n1,s1) &
+ cartprod(M,s1,B,B1) & union(M,A0,B1,Z)"
+
is_converse :: "[i=>o,i,i] => o"
"is_converse(M,r,z) ==
\<forall>x[M]. x \<in> z <->
@@ -163,6 +169,15 @@
number3 :: "[i=>o,i] => o"
"number3(M,a) == (\<exists>x[M]. number2(M,x) & successor(M,x,a))"
+ is_quasinat :: "[i=>o,i] => o"
+ "is_quasinat(M,z) == empty(M,z) | (\<exists>m[M]. successor(M,m,z))"
+
+ is_nat_case :: "[i=>o, i, [i,i]=>o, i, i] => o"
+ "is_nat_case(M, a, is_b, k, z) ==
+ (empty(M,k) --> z=a) &
+ (\<forall>m[M]. successor(M,m,k) --> is_b(m,z)) &
+ (is_quasinat(M,k) | z=0)"
+
subsection {*The relativized ZF axioms*}
constdefs
@@ -607,13 +622,30 @@
"n \<in> nat ==> M(n)"
by (induct n rule: nat_induct, simp_all)
-lemma (in M_triv_axioms) nat_case_closed:
+lemma (in M_triv_axioms) nat_case_closed [intro,simp]:
"[|M(k); M(a); \<forall>m[M]. M(b(m))|] ==> M(nat_case(a,b,k))"
apply (case_tac "k=0", simp)
apply (case_tac "\<exists>m. k = succ(m)", force)
apply (simp add: nat_case_def)
done
+lemma (in M_triv_axioms) quasinat_abs [simp]:
+ "M(z) ==> is_quasinat(M,z) <-> quasinat(z)"
+by (auto simp add: is_quasinat_def quasinat_def)
+
+lemma (in M_triv_axioms) nat_case_abs [simp]:
+ assumes b_abs: "!!x y. M(x) --> M(y) --> (is_b(x,y) <-> y = b(x))"
+ shows
+ "[| M(k); M(z) |] ==> is_nat_case(M,a,is_b,k,z) <-> z = nat_case(a,b,k)"
+apply (case_tac "quasinat(k)")
+ prefer 2
+ apply (simp add: is_nat_case_def non_nat_case)
+ apply (force simp add: quasinat_def)
+apply (simp add: quasinat_def is_nat_case_def)
+apply (elim disjE exE)
+ apply (simp_all add: b_abs)
+done
+
lemma (in M_triv_axioms) Inl_in_M_iff [iff]:
"M(Inl(a)) <-> M(a)"
by (simp add: Inl_def)
@@ -831,6 +863,10 @@
"[| M(A); M(B) |] ==> M(A+B)"
by (simp add: sum_def)
+lemma (in M_axioms) sum_abs [simp]:
+ "[| M(A); M(B); M(Z) |] ==> is_sum(M,A,B,Z) <-> (Z = A+B)"
+by (simp add: is_sum_def sum_def singleton_0 nat_into_M)
+
subsubsection {*converse of a relation*}
@@ -1096,4 +1132,5 @@
apply (simp add: funspace_succ nat_into_M)
done
+
end
--- a/src/ZF/Constructible/Separation.thy Thu Jul 11 16:57:14 2002 +0200
+++ b/src/ZF/Constructible/Separation.thy Thu Jul 11 17:18:28 2002 +0200
@@ -536,7 +536,7 @@
bind_thm ("exists_is_recfun_indstep", axiomsL (thm "M_axioms.exists_is_recfun_indstep"));
bind_thm ("wellfounded_exists_is_recfun", axiomsL (thm "M_axioms.wellfounded_exists_is_recfun"));
bind_thm ("wf_exists_is_recfun", axiomsL (thm "M_axioms.wf_exists_is_recfun"));
-bind_thm ("is_recfun_iff_M", axiomsL (thm "M_axioms.is_recfun_iff_M"));
+bind_thm ("is_recfun_abs", axiomsL (thm "M_axioms.is_recfun_abs"));
bind_thm ("irreflexive_abs", axiomsL (thm "M_axioms.irreflexive_abs"));
bind_thm ("transitive_rel_abs", axiomsL (thm "M_axioms.transitive_rel_abs"));
bind_thm ("linear_rel_abs", axiomsL (thm "M_axioms.linear_rel_abs"));
--- a/src/ZF/Constructible/WF_absolute.thy Thu Jul 11 16:57:14 2002 +0200
+++ b/src/ZF/Constructible/WF_absolute.thy Thu Jul 11 17:18:28 2002 +0200
@@ -262,7 +262,7 @@
separation
(M, \<lambda>x. ~ (\<exists>f[M]. is_recfun(r^+, x, %x f. range(f), f)))"
apply (insert wfrank_separation [of r])
-apply (simp add: is_recfun_iff_M [of concl: _ _ "%x. range", THEN iff_sym])
+apply (simp add: is_recfun_abs [of "%x. range"])
done
lemma (in M_wfrank) wfrank_strong_replacement':
@@ -271,7 +271,7 @@
pair(M,x,y,z) & is_recfun(r^+, x, %x f. range(f), f) &
y = range(f))"
apply (insert wfrank_strong_replacement [of r])
-apply (simp add: is_recfun_iff_M [of concl: _ _ "%x. range", THEN iff_sym])
+apply (simp add: is_recfun_abs [of "%x. range"])
done
lemma (in M_wfrank) Ord_wfrank_separation':
@@ -279,7 +279,7 @@
separation (M, \<lambda>x.
~ (\<forall>f[M]. is_recfun(r^+, x, \<lambda>x. range, f) --> Ord(range(f))))"
apply (insert Ord_wfrank_separation [of r])
-apply (simp add: is_recfun_iff_M [of concl: _ _ "%x. range", THEN iff_sym])
+apply (simp add: is_recfun_abs [of "%x. range"])
done
text{*This function, defined using replacement, is a rank function for
--- a/src/ZF/Constructible/WFrec.thy Thu Jul 11 16:57:14 2002 +0200
+++ b/src/ZF/Constructible/WFrec.thy Thu Jul 11 17:18:28 2002 +0200
@@ -283,10 +283,10 @@
pre_image(M,r,sx,r_sx) & restriction(M,f,r_sx,f_r_sx) &
xa \<in> r & MH(x, f_r_sx, y))"
-lemma (in M_axioms) is_recfun_iff_M:
- "[| M(r); M(a); M(f); \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g));
- \<forall>x g y. M(x) --> M(g) --> M(y) --> MH(x,g,y) <-> y = H(x,g) |] ==>
- is_recfun(r,a,H,f) <-> M_is_recfun(M,r,a,MH,f)"
+lemma (in M_axioms) is_recfun_abs:
+ "[| \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)); M(r); M(a); M(f);
+ \<forall>x g y. M(x) --> M(g) --> M(y) --> MH(x,g,y) <-> y = H(x,g) |]
+ ==> M_is_recfun(M,r,a,MH,f) <-> is_recfun(r,a,H,f)"
apply (simp add: M_is_recfun_def is_recfun_relativize)
apply (rule rall_cong)
apply (blast dest: transM)
@@ -300,7 +300,7 @@
constdefs
- (*This expresses ordinal addition as a formula in the LAST. It also
+ (*This expresses ordinal addition in the language of ZF. It also
provides an abbreviation that can be used in the instance of strong
replacement below. Here j is used to define the relation, namely
Memrel(succ(j)), while x determines the domain of f.*)
@@ -367,7 +367,7 @@
f \<in> a \<rightarrow> range(f) & (\<forall>x. M(x) --> x < a --> f`x = i Un f``x)"
apply (frule lt_Ord)
apply (simp add: is_oadd_fun_def Memrel_closed Un_closed
- is_recfun_iff_M [of concl: _ _ "%x g. i Un g``x", THEN iff_sym]
+ is_recfun_abs [of "%x g. i Un g``x"]
image_closed is_recfun_iff_equation
Ball_def lt_trans [OF ltI, of _ a] lt_Memrel)
apply (simp add: lt_def)
@@ -382,8 +382,7 @@
(\<exists>g[M]. is_recfun(Memrel(succ(j)),x,%x g. i Un g``x,g) &
y = i Un g``x))"
apply (insert oadd_strong_replacement [of i j])
-apply (simp add: Memrel_closed Un_closed image_closed is_oadd_fun_def
- is_recfun_iff_M)
+apply (simp add: is_oadd_fun_def is_recfun_abs [of "%x g. i Un g``x"])
done