src/ZF/Constructible/L_axioms.thy
 changeset 13352 3cd767f8d78b parent 13348 374d05460db4 child 13363 c26eeb000470
```     1.1 --- a/src/ZF/Constructible/L_axioms.thy	Thu Jul 11 17:56:28 2002 +0200
1.2 +++ b/src/ZF/Constructible/L_axioms.thy	Fri Jul 12 11:24:40 2002 +0200
1.3 @@ -563,40 +563,40 @@
1.4  done
1.5
1.6
1.7 -subsubsection{*Function Application, Internalized*}
1.8 +subsubsection{*Big Union, Internalized*}
1.9
1.10 -constdefs fun_apply_fm :: "[i,i,i]=>i"
1.11 -    "fun_apply_fm(f,x,y) ==
1.12 -       Forall(Iff(Exists(And(Member(0,succ(succ(f))),
1.13 -                             pair_fm(succ(succ(x)), 1, 0))),
1.14 -                  Equal(succ(y),0)))"
1.15 +(*  "big_union(M,A,z) == \<forall>x[M]. x \<in> z <-> (\<exists>y[M]. y\<in>A & x \<in> y)" *)
1.16 +constdefs big_union_fm :: "[i,i]=>i"
1.17 +    "big_union_fm(A,z) ==
1.18 +       Forall(Iff(Member(0,succ(z)),
1.19 +                  Exists(And(Member(0,succ(succ(A))), Member(1,0)))))"
1.20
1.21 -lemma fun_apply_type [TC]:
1.22 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> fun_apply_fm(x,y,z) \<in> formula"
1.24 +lemma big_union_type [TC]:
1.25 +     "[| x \<in> nat; y \<in> nat |] ==> big_union_fm(x,y) \<in> formula"
1.27
1.28 -lemma arity_fun_apply_fm [simp]:
1.29 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
1.30 -      ==> arity(fun_apply_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
1.31 -by (simp add: fun_apply_fm_def succ_Un_distrib [symmetric] Un_ac)
1.32 +lemma arity_big_union_fm [simp]:
1.33 +     "[| x \<in> nat; y \<in> nat |]
1.34 +      ==> arity(big_union_fm(x,y)) = succ(x) \<union> succ(y)"
1.35 +by (simp add: big_union_fm_def succ_Un_distrib [symmetric] Un_ac)
1.36
1.37 -lemma sats_fun_apply_fm [simp]:
1.38 -   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
1.39 -    ==> sats(A, fun_apply_fm(x,y,z), env) <->
1.40 -        fun_apply(**A, nth(x,env), nth(y,env), nth(z,env))"
1.41 -by (simp add: fun_apply_fm_def fun_apply_def)
1.42 +lemma sats_big_union_fm [simp]:
1.43 +   "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
1.44 +    ==> sats(A, big_union_fm(x,y), env) <->
1.45 +        big_union(**A, nth(x,env), nth(y,env))"
1.46 +by (simp add: big_union_fm_def big_union_def)
1.47
1.48 -lemma fun_apply_iff_sats:
1.49 -      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
1.50 -          i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
1.51 -       ==> fun_apply(**A, x, y, z) <-> sats(A, fun_apply_fm(i,j,k), env)"
1.52 +lemma big_union_iff_sats:
1.53 +      "[| nth(i,env) = x; nth(j,env) = y;
1.54 +          i \<in> nat; j \<in> nat; env \<in> list(A)|]
1.55 +       ==> big_union(**A, x, y) <-> sats(A, big_union_fm(i,j), env)"
1.56  by simp
1.57
1.58 -theorem fun_apply_reflection:
1.59 -     "REFLECTS[\<lambda>x. fun_apply(L,f(x),g(x),h(x)),
1.60 -               \<lambda>i x. fun_apply(**Lset(i),f(x),g(x),h(x))]"
1.61 -apply (simp only: fun_apply_def setclass_simps)
1.62 -apply (intro FOL_reflections pair_reflection)
1.63 +theorem big_union_reflection:
1.64 +     "REFLECTS[\<lambda>x. big_union(L,f(x),g(x)),
1.65 +               \<lambda>i x. big_union(**Lset(i),f(x),g(x))]"
1.66 +apply (simp only: big_union_def setclass_simps)
1.67 +apply (intro FOL_reflections)
1.68  done
1.69
1.70
1.71 @@ -924,6 +924,47 @@
1.72  done
1.73
1.74
1.75 +subsubsection{*Function Application, Internalized*}
1.76 +
1.77 +(* "fun_apply(M,f,x,y) ==
1.78 +        (\<exists>xs[M]. \<exists>fxs[M].
1.79 +         upair(M,x,x,xs) & image(M,f,xs,fxs) & big_union(M,fxs,y))" *)
1.80 +constdefs fun_apply_fm :: "[i,i,i]=>i"
1.81 +    "fun_apply_fm(f,x,y) ==
1.82 +       Exists(Exists(And(upair_fm(succ(succ(x)), succ(succ(x)), 1),
1.83 +                         And(image_fm(succ(succ(f)), 1, 0),
1.84 +                             big_union_fm(0,succ(succ(y)))))))"
1.85 +
1.86 +lemma fun_apply_type [TC]:
1.87 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> fun_apply_fm(x,y,z) \<in> formula"
1.89 +
1.90 +lemma arity_fun_apply_fm [simp]:
1.91 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
1.92 +      ==> arity(fun_apply_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
1.93 +by (simp add: fun_apply_fm_def succ_Un_distrib [symmetric] Un_ac)
1.94 +
1.95 +lemma sats_fun_apply_fm [simp]:
1.96 +   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
1.97 +    ==> sats(A, fun_apply_fm(x,y,z), env) <->
1.98 +        fun_apply(**A, nth(x,env), nth(y,env), nth(z,env))"
1.99 +by (simp add: fun_apply_fm_def fun_apply_def)
1.100 +
1.101 +lemma fun_apply_iff_sats:
1.102 +      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
1.103 +          i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
1.104 +       ==> fun_apply(**A, x, y, z) <-> sats(A, fun_apply_fm(i,j,k), env)"
1.105 +by simp
1.106 +
1.107 +theorem fun_apply_reflection:
1.108 +     "REFLECTS[\<lambda>x. fun_apply(L,f(x),g(x),h(x)),
1.109 +               \<lambda>i x. fun_apply(**Lset(i),f(x),g(x),h(x))]"
1.110 +apply (simp only: fun_apply_def setclass_simps)
1.111 +apply (intro FOL_reflections upair_reflection image_reflection
1.112 +             big_union_reflection)
1.113 +done
1.114 +
1.115 +
1.116  subsubsection{*The Concept of Relation, Internalized*}
1.117
1.118  (* "is_relation(M,r) ==
1.119 @@ -1036,7 +1077,7 @@
1.120
1.121  lemmas function_reflections =
1.122          empty_reflection upair_reflection pair_reflection union_reflection
1.123 -	cons_reflection successor_reflection
1.124 +	big_union_reflection cons_reflection successor_reflection
1.125          fun_apply_reflection subset_reflection
1.126  	transitive_set_reflection membership_reflection
1.127  	pred_set_reflection domain_reflection range_reflection field_reflection
```