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.23 -by (simp add: fun_apply_fm_def) 
    1.24 +lemma big_union_type [TC]:
    1.25 +     "[| x \<in> nat; y \<in> nat |] ==> big_union_fm(x,y) \<in> formula"
    1.26 +by (simp add: big_union_fm_def) 
    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.88 +by (simp add: fun_apply_fm_def) 
    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