--- a/src/ZF/Constructible/Datatype_absolute.thy Thu Jul 11 17:56:28 2002 +0200
+++ b/src/ZF/Constructible/Datatype_absolute.thy Fri Jul 12 11:24:40 2002 +0200
@@ -95,9 +95,9 @@
lemma (in M_trancl) iterates_relativize:
"[|n \<in> nat; M(v); \<forall>x[M]. M(F(x));
strong_replacement(M,
- \<lambda>x z. \<exists>y[M]. \<exists>g[M]. pair(M, x, y, z) &
- is_recfun (Memrel(succ(n)), x,
- \<lambda>n f. nat_case(v, \<lambda>m. F(f`m), n), g) &
+ \<lambda>x z. \<exists>y[M]. \<exists>g[M]. pair(M,x,y,z) &
+ M_is_recfun(M, \<lambda>n f z. z = nat_case(v, \<lambda>m. F(f`m), n),
+ Memrel(succ(n)), x, g) &
y = nat_case(v, \<lambda>m. F(g`m), x))|]
==> iterates(F,n,v) = z <->
(\<exists>g[M]. is_recfun(Memrel(succ(n)), n,
@@ -105,7 +105,8 @@
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)
+ wf_Memrel trans_Memrel relation_Memrel
+ is_recfun_abs [of "\<lambda>n g. nat_case(v, \<lambda>m. F(g`m), n)"])
lemma (in M_wfrank) iterates_closed [intro,simp]:
"[|n \<in> nat; M(v); \<forall>x[M]. M(F(x));
@@ -126,8 +127,9 @@
\<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) ==
+ list_functor_case :: "[i=>o,i,i,i,i] => o"
+ --{*Abbreviation for the definition of lists below*}
+ "list_functor_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)"
@@ -136,6 +138,12 @@
"[| 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)
+lemma (in M_axioms) list_functor_case_abs:
+ "[| M(A); M(n); M(y); M(g) |]
+ ==> list_functor_case(M,A,g,n,y) <->
+ y = nat_case(0, \<lambda>m. {0} + A * g`m, n)"
+by (simp add: list_functor_case_def nat_into_M)
+
locale M_datatypes = M_wfrank +
assumes list_replacement1:
@@ -144,10 +152,9 @@
\<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))"
+ M_is_recfun(M, \<lambda>n f z. list_functor_case(M,A,f,n,z),
+ memr, x, g) &
+ list_functor_case(M,A,g,x,y))"
(*THEY NEED RELATIVIZATION*)
and list_replacement2:
"M(A) ==> strong_replacement(M, \<lambda>x y. y = (\<lambda>X. {0} + A * X)^x (0))"
@@ -162,7 +169,7 @@
\<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
+apply (simp add: nat_into_M list_functor_case_abs
is_recfun_abs [of "\<lambda>n f. nat_case(0, \<lambda>m. {0} + A * f`m, n)"])
done
--- a/src/ZF/Constructible/L_axioms.thy Thu Jul 11 17:56:28 2002 +0200
+++ b/src/ZF/Constructible/L_axioms.thy Fri Jul 12 11:24:40 2002 +0200
@@ -563,40 +563,40 @@
done
-subsubsection{*Function Application, Internalized*}
+subsubsection{*Big Union, Internalized*}
-constdefs fun_apply_fm :: "[i,i,i]=>i"
- "fun_apply_fm(f,x,y) ==
- Forall(Iff(Exists(And(Member(0,succ(succ(f))),
- pair_fm(succ(succ(x)), 1, 0))),
- Equal(succ(y),0)))"
+(* "big_union(M,A,z) == \<forall>x[M]. x \<in> z <-> (\<exists>y[M]. y\<in>A & x \<in> y)" *)
+constdefs big_union_fm :: "[i,i]=>i"
+ "big_union_fm(A,z) ==
+ Forall(Iff(Member(0,succ(z)),
+ Exists(And(Member(0,succ(succ(A))), Member(1,0)))))"
-lemma fun_apply_type [TC]:
- "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> fun_apply_fm(x,y,z) \<in> formula"
-by (simp add: fun_apply_fm_def)
+lemma big_union_type [TC]:
+ "[| x \<in> nat; y \<in> nat |] ==> big_union_fm(x,y) \<in> formula"
+by (simp add: big_union_fm_def)
-lemma arity_fun_apply_fm [simp]:
- "[| x \<in> nat; y \<in> nat; z \<in> nat |]
- ==> arity(fun_apply_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
-by (simp add: fun_apply_fm_def succ_Un_distrib [symmetric] Un_ac)
+lemma arity_big_union_fm [simp]:
+ "[| x \<in> nat; y \<in> nat |]
+ ==> arity(big_union_fm(x,y)) = succ(x) \<union> succ(y)"
+by (simp add: big_union_fm_def succ_Un_distrib [symmetric] Un_ac)
-lemma sats_fun_apply_fm [simp]:
- "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
- ==> sats(A, fun_apply_fm(x,y,z), env) <->
- fun_apply(**A, nth(x,env), nth(y,env), nth(z,env))"
-by (simp add: fun_apply_fm_def fun_apply_def)
+lemma sats_big_union_fm [simp]:
+ "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
+ ==> sats(A, big_union_fm(x,y), env) <->
+ big_union(**A, nth(x,env), nth(y,env))"
+by (simp add: big_union_fm_def big_union_def)
-lemma fun_apply_iff_sats:
- "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
- i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
- ==> fun_apply(**A, x, y, z) <-> sats(A, fun_apply_fm(i,j,k), env)"
+lemma big_union_iff_sats:
+ "[| nth(i,env) = x; nth(j,env) = y;
+ i \<in> nat; j \<in> nat; env \<in> list(A)|]
+ ==> big_union(**A, x, y) <-> sats(A, big_union_fm(i,j), env)"
by simp
-theorem fun_apply_reflection:
- "REFLECTS[\<lambda>x. fun_apply(L,f(x),g(x),h(x)),
- \<lambda>i x. fun_apply(**Lset(i),f(x),g(x),h(x))]"
-apply (simp only: fun_apply_def setclass_simps)
-apply (intro FOL_reflections pair_reflection)
+theorem big_union_reflection:
+ "REFLECTS[\<lambda>x. big_union(L,f(x),g(x)),
+ \<lambda>i x. big_union(**Lset(i),f(x),g(x))]"
+apply (simp only: big_union_def setclass_simps)
+apply (intro FOL_reflections)
done
@@ -924,6 +924,47 @@
done
+subsubsection{*Function Application, Internalized*}
+
+(* "fun_apply(M,f,x,y) ==
+ (\<exists>xs[M]. \<exists>fxs[M].
+ upair(M,x,x,xs) & image(M,f,xs,fxs) & big_union(M,fxs,y))" *)
+constdefs fun_apply_fm :: "[i,i,i]=>i"
+ "fun_apply_fm(f,x,y) ==
+ Exists(Exists(And(upair_fm(succ(succ(x)), succ(succ(x)), 1),
+ And(image_fm(succ(succ(f)), 1, 0),
+ big_union_fm(0,succ(succ(y)))))))"
+
+lemma fun_apply_type [TC]:
+ "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> fun_apply_fm(x,y,z) \<in> formula"
+by (simp add: fun_apply_fm_def)
+
+lemma arity_fun_apply_fm [simp]:
+ "[| x \<in> nat; y \<in> nat; z \<in> nat |]
+ ==> arity(fun_apply_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
+by (simp add: fun_apply_fm_def succ_Un_distrib [symmetric] Un_ac)
+
+lemma sats_fun_apply_fm [simp]:
+ "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
+ ==> sats(A, fun_apply_fm(x,y,z), env) <->
+ fun_apply(**A, nth(x,env), nth(y,env), nth(z,env))"
+by (simp add: fun_apply_fm_def fun_apply_def)
+
+lemma fun_apply_iff_sats:
+ "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
+ i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
+ ==> fun_apply(**A, x, y, z) <-> sats(A, fun_apply_fm(i,j,k), env)"
+by simp
+
+theorem fun_apply_reflection:
+ "REFLECTS[\<lambda>x. fun_apply(L,f(x),g(x),h(x)),
+ \<lambda>i x. fun_apply(**Lset(i),f(x),g(x),h(x))]"
+apply (simp only: fun_apply_def setclass_simps)
+apply (intro FOL_reflections upair_reflection image_reflection
+ big_union_reflection)
+done
+
+
subsubsection{*The Concept of Relation, Internalized*}
(* "is_relation(M,r) ==
@@ -1036,7 +1077,7 @@
lemmas function_reflections =
empty_reflection upair_reflection pair_reflection union_reflection
- cons_reflection successor_reflection
+ big_union_reflection cons_reflection successor_reflection
fun_apply_reflection subset_reflection
transitive_set_reflection membership_reflection
pred_set_reflection domain_reflection range_reflection field_reflection
--- a/src/ZF/Constructible/Rec_Separation.thy Thu Jul 11 17:56:28 2002 +0200
+++ b/src/ZF/Constructible/Rec_Separation.thy Fri Jul 12 11:24:40 2002 +0200
@@ -196,8 +196,8 @@
subsection{*Well-Founded Recursion!*}
-(* M_is_recfun :: "[i=>o, i, i, [i,i,i]=>o, i] => o"
- "M_is_recfun(M,r,a,MH,f) ==
+(* M_is_recfun :: "[i=>o, [i,i,i]=>o, i, i, i] => o"
+ "M_is_recfun(M,MH,r,a,f) ==
\<forall>z[M]. z \<in> f <->
5 4 3 2 1 0
(\<exists>x[M]. \<exists>y[M]. \<exists>xa[M]. \<exists>sx[M]. \<exists>r_sx[M]. \<exists>f_r_sx[M].
@@ -252,7 +252,7 @@
shows
"[|x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
==> sats(A, is_recfun_fm(p,x,y,z), env) <->
- M_is_recfun(**A, nth(x,env), nth(y,env), MH, nth(z,env))"
+ M_is_recfun(**A, MH, nth(x,env), nth(y,env), nth(z,env))"
by (simp add: is_recfun_fm_def M_is_recfun_def MH_iff_sats [THEN iff_sym])
lemma is_recfun_iff_sats:
@@ -261,15 +261,15 @@
sats(A, p(x,y,z), env));
nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
- ==> M_is_recfun(**A, x, y, MH, z) <-> sats(A, is_recfun_fm(p,i,j,k), env)"
+ ==> M_is_recfun(**A, MH, x, y, z) <-> sats(A, is_recfun_fm(p,i,j,k), env)"
by (simp add: sats_is_recfun_fm [of A MH])
theorem is_recfun_reflection:
assumes MH_reflection:
"!!f g h. REFLECTS[\<lambda>x. MH(L, f(x), g(x), h(x)),
\<lambda>i x. MH(**Lset(i), f(x), g(x), h(x))]"
- shows "REFLECTS[\<lambda>x. M_is_recfun(L, f(x), g(x), MH(L), h(x)),
- \<lambda>i x. M_is_recfun(**Lset(i), f(x), g(x), MH(**Lset(i)), h(x))]"
+ shows "REFLECTS[\<lambda>x. M_is_recfun(L, MH(L), f(x), g(x), h(x)),
+ \<lambda>i x. M_is_recfun(**Lset(i), MH(**Lset(i)), f(x), g(x), h(x))]"
apply (simp (no_asm_use) only: M_is_recfun_def setclass_simps)
apply (intro FOL_reflections function_reflections
restriction_reflection MH_reflection)
@@ -279,15 +279,17 @@
lemma wfrank_Reflects:
"REFLECTS[\<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) -->
- ~ (\<exists>f[L]. M_is_recfun(L, rplus, x, %x f y. is_range(L,f,y), f)),
+ ~ (\<exists>f[L]. M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f)),
\<lambda>i x. \<forall>rplus \<in> Lset(i). tran_closure(**Lset(i),r,rplus) -->
- ~ (\<exists>f \<in> Lset(i). M_is_recfun(**Lset(i), rplus, x, %x f y. is_range(**Lset(i),f,y), f))]"
+ ~ (\<exists>f \<in> Lset(i).
+ M_is_recfun(**Lset(i), %x f y. is_range(**Lset(i),f,y),
+ rplus, x, f))]"
by (intro FOL_reflections function_reflections is_recfun_reflection tran_closure_reflection)
lemma wfrank_separation:
"L(r) ==>
separation (L, \<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) -->
- ~ (\<exists>f[L]. M_is_recfun(L, rplus, x, %x f y. is_range(L,f,y), f)))"
+ ~ (\<exists>f[L]. M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f)))"
apply (rule separation_CollectI)
apply (rule_tac A="{r,z}" in subset_LsetE, blast )
apply (rule ReflectsE [OF wfrank_Reflects], assumption)
@@ -309,12 +311,12 @@
"REFLECTS[\<lambda>z. \<exists>x[L]. x \<in> A &
(\<forall>rplus[L]. tran_closure(L,r,rplus) -->
(\<exists>y[L]. \<exists>f[L]. pair(L,x,y,z) &
- M_is_recfun(L, rplus, x, %x f y. is_range(L,f,y), f) &
+ M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f) &
is_range(L,f,y))),
\<lambda>i z. \<exists>x \<in> Lset(i). x \<in> A &
(\<forall>rplus \<in> Lset(i). tran_closure(**Lset(i),r,rplus) -->
(\<exists>y \<in> Lset(i). \<exists>f \<in> Lset(i). pair(**Lset(i),x,y,z) &
- M_is_recfun(**Lset(i), rplus, x, %x f y. is_range(**Lset(i),f,y), f) &
+ M_is_recfun(**Lset(i), %x f y. is_range(**Lset(i),f,y), rplus, x, f) &
is_range(**Lset(i),f,y)))]"
by (intro FOL_reflections function_reflections fun_plus_reflections
is_recfun_reflection tran_closure_reflection)
@@ -325,7 +327,7 @@
strong_replacement(L, \<lambda>x z.
\<forall>rplus[L]. tran_closure(L,r,rplus) -->
(\<exists>y[L]. \<exists>f[L]. pair(L,x,y,z) &
- M_is_recfun(L, rplus, x, %x f y. is_range(L,f,y), f) &
+ M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f) &
is_range(L,f,y)))"
apply (rule strong_replacementI)
apply (rule rallI)
@@ -351,12 +353,13 @@
"REFLECTS[\<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) -->
~ (\<forall>f[L]. \<forall>rangef[L].
is_range(L,f,rangef) -->
- M_is_recfun(L, rplus, x, \<lambda>x f y. is_range(L,f,y), f) -->
+ M_is_recfun(L, \<lambda>x f y. is_range(L,f,y), rplus, x, f) -->
ordinal(L,rangef)),
\<lambda>i x. \<forall>rplus \<in> Lset(i). tran_closure(**Lset(i),r,rplus) -->
~ (\<forall>f \<in> Lset(i). \<forall>rangef \<in> Lset(i).
is_range(**Lset(i),f,rangef) -->
- M_is_recfun(**Lset(i), rplus, x, \<lambda>x f y. is_range(**Lset(i),f,y), f) -->
+ M_is_recfun(**Lset(i), \<lambda>x f y. is_range(**Lset(i),f,y),
+ rplus, x, f) -->
ordinal(**Lset(i),rangef))]"
by (intro FOL_reflections function_reflections is_recfun_reflection
tran_closure_reflection ordinal_reflection)
@@ -367,7 +370,7 @@
\<forall>rplus[L]. tran_closure(L,r,rplus) -->
~ (\<forall>f[L]. \<forall>rangef[L].
is_range(L,f,rangef) -->
- M_is_recfun(L, rplus, x, \<lambda>x f y. is_range(L,f,y), f) -->
+ M_is_recfun(L, \<lambda>x f y. is_range(L,f,y), rplus, x, f) -->
ordinal(L,rangef)))"
apply (rule separation_CollectI)
apply (rule_tac A="{r,z}" in subset_LsetE, blast )
--- a/src/ZF/Constructible/Relative.thy Thu Jul 11 17:56:28 2002 +0200
+++ b/src/ZF/Constructible/Relative.thy Fri Jul 12 11:24:40 2002 +0200
@@ -96,7 +96,8 @@
fun_apply :: "[i=>o,i,i,i] => o"
"fun_apply(M,f,x,y) ==
- (\<forall>y'[M]. (\<exists>u[M]. u\<in>f & pair(M,x,y',u)) <-> y=y')"
+ (\<exists>xs[M]. \<exists>fxs[M].
+ upair(M,x,x,xs) & image(M,f,xs,fxs) & big_union(M,fxs,y))"
typed_function :: "[i=>o,i,i,i] => o"
"typed_function(M,A,B,r) ==
@@ -646,6 +647,13 @@
apply (simp_all add: b_abs)
done
+(*Needed? surely better to replace by nat_case?*)
+lemma (in M_triv_axioms) is_nat_case_cong [cong]:
+ "[| a = a'; k = k'; z = z'; M(z');
+ !!x y. [| M(x); M(y) |] ==> is_b(x,y) <-> is_b'(x,y) |]
+ ==> is_nat_case(M, a, is_b, k, z) <-> is_nat_case(M, a', is_b', k', z')"
+by (simp add: is_nat_case_def)
+
lemma (in M_triv_axioms) Inl_in_M_iff [iff]:
"M(Inl(a)) <-> M(a)"
by (simp add: Inl_def)
@@ -970,18 +978,12 @@
"[|M(f); M(a)|] ==> M(f`a)"
by (simp add: apply_def)
-lemma (in M_axioms) apply_abs:
- "[| function(f); M(f); M(y) |]
- ==> fun_apply(M,f,x,y) <-> x \<in> domain(f) & f`x = y"
-apply (simp add: fun_apply_def)
-apply (blast intro: function_apply_equality function_apply_Pair)
+lemma (in M_axioms) apply_abs [simp]:
+ "[| M(f); M(x); M(y) |] ==> fun_apply(M,f,x,y) <-> f`x = y"
+apply (simp add: fun_apply_def apply_def)
+apply (blast intro: elim:);
done
-lemma (in M_axioms) typed_apply_abs:
- "[| f \<in> A -> B; M(f); M(y) |]
- ==> fun_apply(M,f,x,y) <-> x \<in> A & f`x = y"
-by (simp add: apply_abs fun_is_function domain_of_fun)
-
lemma (in M_axioms) typed_function_abs [simp]:
"[| M(A); M(f) |] ==> typed_function(M,A,B,f) <-> f \<in> A -> B"
apply (auto simp add: typed_function_def relation_def Pi_iff)
@@ -996,7 +998,7 @@
lemma (in M_axioms) surjection_abs [simp]:
"[| M(A); M(B); M(f) |] ==> surjection(M,A,B,f) <-> f \<in> surj(A,B)"
-by (simp add: typed_apply_abs surjection_def surj_def)
+by (simp add: surjection_def surj_def)
lemma (in M_axioms) bijection_abs [simp]:
"[| M(A); M(B); M(f) |] ==> bijection(M,A,B,f) <-> f \<in> bij(A,B)"
--- a/src/ZF/Constructible/Separation.thy Thu Jul 11 17:56:28 2002 +0200
+++ b/src/ZF/Constructible/Separation.thy Fri Jul 12 11:24:40 2002 +0200
@@ -503,7 +503,6 @@
bind_thm ("function_abs", axiomsL (thm "M_axioms.function_abs"));
bind_thm ("apply_closed", axiomsL (thm "M_axioms.apply_closed"));
bind_thm ("apply_abs", axiomsL (thm "M_axioms.apply_abs"));
-bind_thm ("typed_apply_abs", axiomsL (thm "M_axioms.typed_apply_abs"));
bind_thm ("typed_function_abs", axiomsL (thm "M_axioms.typed_function_abs"));
bind_thm ("injection_abs", axiomsL (thm "M_axioms.injection_abs"));
bind_thm ("surjection_abs", axiomsL (thm "M_axioms.surjection_abs"));
--- a/src/ZF/Constructible/WF_absolute.thy Thu Jul 11 17:56:28 2002 +0200
+++ b/src/ZF/Constructible/WF_absolute.thy Fri Jul 12 11:24:40 2002 +0200
@@ -140,9 +140,8 @@
(\<exists>f[M]. f \<in> succ(n) -> A &
(\<exists>x[M]. \<exists>y[M]. p = <x,y> & f`0 = x & f`n = y) &
(\<forall>i\<in>n. <f`i, f`succ(i)> \<in> r)))"
-apply (simp add: rtran_closure_mem_def typed_apply_abs
- Ord_succ_mem_iff nat_0_le [THEN ltD], blast)
-done
+by (simp add: rtran_closure_mem_def Ord_succ_mem_iff nat_0_le [THEN ltD])
+
locale M_trancl = M_axioms +
assumes rtrancl_separation:
@@ -237,13 +236,13 @@
"M(r) ==>
separation (M, \<lambda>x.
\<forall>rplus[M]. tran_closure(M,r,rplus) -->
- ~ (\<exists>f[M]. M_is_recfun(M, rplus, x, %x f y. is_range(M,f,y), f)))"
+ ~ (\<exists>f[M]. M_is_recfun(M, %x f y. is_range(M,f,y), rplus, x, f)))"
and wfrank_strong_replacement:
"M(r) ==>
strong_replacement(M, \<lambda>x z.
\<forall>rplus[M]. tran_closure(M,r,rplus) -->
(\<exists>y[M]. \<exists>f[M]. pair(M,x,y,z) &
- M_is_recfun(M, rplus, x, %x f y. is_range(M,f,y), f) &
+ M_is_recfun(M, %x f y. is_range(M,f,y), rplus, x, f) &
is_range(M,f,y)))"
and Ord_wfrank_separation:
"M(r) ==>
@@ -251,7 +250,7 @@
\<forall>rplus[M]. tran_closure(M,r,rplus) -->
~ (\<forall>f[M]. \<forall>rangef[M].
is_range(M,f,rangef) -->
- M_is_recfun(M, rplus, x, \<lambda>x f y. is_range(M,f,y), f) -->
+ M_is_recfun(M, \<lambda>x f y. is_range(M,f,y), rplus, x, f) -->
ordinal(M,rangef)))"
text{*Proving that the relativized instances of Separation or Replacement
--- a/src/ZF/Constructible/WFrec.thy Thu Jul 11 17:56:28 2002 +0200
+++ b/src/ZF/Constructible/WFrec.thy Fri Jul 12 11:24:40 2002 +0200
@@ -69,7 +69,7 @@
M(r); M(f); M(g); M(a); M(b) |]
==> separation(M, \<lambda>x. \<not> (\<langle>x, a\<rangle> \<in> r \<longrightarrow> \<langle>x, b\<rangle> \<in> r \<longrightarrow> f ` x = g ` x))"
apply (insert is_recfun_separation [of r f g a b])
-apply (simp add: typed_apply_abs vimage_singleton_iff)
+apply (simp add: vimage_singleton_iff)
done
text{*Stated using @{term "trans(r)"} rather than
@@ -275,8 +275,8 @@
done
constdefs
- M_is_recfun :: "[i=>o, i, i, [i,i,i]=>o, i] => o"
- "M_is_recfun(M,r,a,MH,f) ==
+ M_is_recfun :: "[i=>o, [i,i,i]=>o, i, i, i] => o"
+ "M_is_recfun(M,MH,r,a,f) ==
\<forall>z[M]. z \<in> f <->
(\<exists>x[M]. \<exists>y[M]. \<exists>xa[M]. \<exists>sx[M]. \<exists>r_sx[M]. \<exists>f_r_sx[M].
pair(M,x,y,z) & pair(M,x,a,xa) & upair(M,x,x,sx) &
@@ -286,7 +286,7 @@
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)"
+ ==> M_is_recfun(M,MH,r,a,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)
@@ -295,7 +295,7 @@
lemma M_is_recfun_cong [cong]:
"[| r = r'; a = a'; f = f';
!!x g y. [| M(x); M(g); M(y) |] ==> MH(x,g,y) <-> MH'(x,g,y) |]
- ==> M_is_recfun(M,r,a,MH,f) <-> M_is_recfun(M,r',a',MH',f')"
+ ==> M_is_recfun(M,MH,r,a,f) <-> M_is_recfun(M,MH',r',a',f')"
by (simp add: M_is_recfun_def)
@@ -308,9 +308,9 @@
"is_oadd_fun(M,i,j,x,f) ==
(\<forall>sj msj. M(sj) --> M(msj) -->
successor(M,j,sj) --> membership(M,sj,msj) -->
- M_is_recfun(M, msj, x,
+ M_is_recfun(M,
%x g y. \<exists>gx[M]. image(M,g,x,gx) & union(M,i,gx,y),
- f))"
+ msj, x, f))"
is_oadd :: "[i=>o,i,i,i] => o"
"is_oadd(M,i,j,k) ==
@@ -422,14 +422,9 @@
apply (blast intro: lt_trans ltI lt_Ord)
done
-lemma (in M_ord_arith) oadd_abs_fun_apply_iff:
- "[| M(i); M(J); M(f); M(k); j<J; is_oadd_fun(M,i,J,J,f) |]
- ==> fun_apply(M,f,j,k) <-> f`j = k"
-by (force simp add: lt_def is_oadd_fun_iff subsetD typed_apply_abs)
-
lemma (in M_ord_arith) Ord_oadd_abs:
"[| M(i); M(j); M(k); Ord(i); Ord(j) |] ==> is_oadd(M,i,j,k) <-> k = i++j"
-apply (simp add: is_oadd_def oadd_abs_fun_apply_iff is_oadd_fun_iff_oadd)
+apply (simp add: is_oadd_def is_oadd_fun_iff_oadd)
apply (frule exists_oadd_fun [of j i], blast+)
done
@@ -547,14 +542,9 @@
apply (blast intro: lt_trans ltI lt_Ord)
done
-lemma (in M_ord_arith) omult_abs_fun_apply_iff:
- "[| M(i); M(J); M(f); M(k); j<J; is_omult_fun(M,i,J,f) |]
- ==> fun_apply(M,f,j,k) <-> f`j = k"
-by (auto simp add: lt_def is_omult_fun_def subsetD apply_abs)
-
lemma (in M_ord_arith) omult_abs:
"[| M(i); M(j); M(k); Ord(i); Ord(j) |] ==> is_omult(M,i,j,k) <-> k = i**j"
-apply (simp add: is_omult_def omult_abs_fun_apply_iff is_omult_fun_eq_omult)
+apply (simp add: is_omult_def is_omult_fun_eq_omult)
apply (frule exists_omult_fun [of j i], blast+)
done
--- a/src/ZF/Constructible/Wellorderings.thy Thu Jul 11 17:56:28 2002 +0200
+++ b/src/ZF/Constructible/Wellorderings.thy Fri Jul 12 11:24:40 2002 +0200
@@ -161,9 +161,7 @@
lemma (in M_axioms) order_isomorphism_abs [simp]:
"[| M(A); M(B); M(f) |]
==> order_isomorphism(M,A,r,B,s,f) <-> f \<in> ord_iso(A,r,B,s)"
-by (simp add: typed_apply_abs [OF bij_is_fun] apply_closed
- order_isomorphism_def ord_iso_def)
-
+by (simp add: apply_closed order_isomorphism_def ord_iso_def)
lemma (in M_axioms) pred_set_abs [simp]:
"[| M(r); M(B) |] ==> pred_set(M,A,x,r,B) <-> B = Order.pred(A,x,r)"
@@ -236,7 +234,7 @@
apply (elim conjE CollectE)
apply (erule wellfounded_on_induct, assumption+)
apply (insert well_ord_iso_separation [of A f r])
- apply (simp add: typed_apply_abs [OF bij_is_fun] apply_closed, clarify)
+ apply (simp, clarify)
apply (drule_tac a = x in bij_is_fun [THEN apply_type], assumption, blast)
done