1.1 --- a/src/ZF/Constructible/L_axioms.thy Mon Jul 08 11:34:43 2002 +0200
1.2 +++ b/src/ZF/Constructible/L_axioms.thy Mon Jul 08 12:31:16 2002 +0200
1.3 @@ -800,4 +800,220 @@
1.4 by (simp only: is_function_def setclass_simps, fast)
1.5
1.6
1.7 +subsubsection{*Typed Functions*}
1.8 +
1.9 +(* "typed_function(M,A,B,r) ==
1.10 + is_function(M,r) & is_relation(M,r) & is_domain(M,r,A) &
1.11 + (\<forall>u[M]. u\<in>r --> (\<forall>x[M]. \<forall>y[M]. pair(M,x,y,u) --> y\<in>B))" *)
1.12 +
1.13 +constdefs typed_function_fm :: "[i,i,i]=>i"
1.14 + "typed_function_fm(A,B,r) ==
1.15 + And(function_fm(r),
1.16 + And(relation_fm(r),
1.17 + And(domain_fm(r,A),
1.18 + Forall(Implies(Member(0,succ(r)),
1.19 + Forall(Forall(Implies(pair_fm(1,0,2),Member(0,B#+3)))))))))"
1.20 +
1.21 +lemma typed_function_type [TC]:
1.22 + "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> typed_function_fm(x,y,z) \<in> formula"
1.23 +by (simp add: typed_function_fm_def)
1.24 +
1.25 +lemma arity_typed_function_fm [simp]:
1.26 + "[| x \<in> nat; y \<in> nat; z \<in> nat |]
1.27 + ==> arity(typed_function_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
1.28 +by (simp add: typed_function_fm_def succ_Un_distrib [symmetric] Un_ac)
1.29 +
1.30 +lemma sats_typed_function_fm [simp]:
1.31 + "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
1.32 + ==> sats(A, typed_function_fm(x,y,z), env) <->
1.33 + typed_function(**A, nth(x,env), nth(y,env), nth(z,env))"
1.34 +by (simp add: typed_function_fm_def typed_function_def)
1.35 +
1.36 +lemma typed_function_iff_sats:
1.37 + "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
1.38 + i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
1.39 + ==> typed_function(**A, x, y, z) <-> sats(A, typed_function_fm(i,j,k), env)"
1.40 +by simp
1.41 +
1.42 +theorem typed_function_reflection [simplified,intro]:
1.43 + "L_Reflects(?Cl, \<lambda>x. typed_function(L,f(x),g(x),h(x)),
1.44 + \<lambda>i x. typed_function(**Lset(i),f(x),g(x),h(x)))"
1.45 +by (simp only: typed_function_def setclass_simps, fast)
1.46 +
1.47 +
1.48 +
1.49 +subsubsection{*Injections*}
1.50 +
1.51 +(* "injection(M,A,B,f) ==
1.52 + typed_function(M,A,B,f) &
1.53 + (\<forall>x[M]. \<forall>x'[M]. \<forall>y[M]. \<forall>p[M]. \<forall>p'[M].
1.54 + pair(M,x,y,p) --> pair(M,x',y,p') --> p\<in>f --> p'\<in>f --> x=x')" *)
1.55 +constdefs injection_fm :: "[i,i,i]=>i"
1.56 + "injection_fm(A,B,f) ==
1.57 + And(typed_function_fm(A,B,f),
1.58 + Forall(Forall(Forall(Forall(Forall(
1.59 + Implies(pair_fm(4,2,1),
1.60 + Implies(pair_fm(3,2,0),
1.61 + Implies(Member(1,f#+5),
1.62 + Implies(Member(0,f#+5), Equal(4,3)))))))))))"
1.63 +
1.64 +
1.65 +lemma injection_type [TC]:
1.66 + "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> injection_fm(x,y,z) \<in> formula"
1.67 +by (simp add: injection_fm_def)
1.68 +
1.69 +lemma arity_injection_fm [simp]:
1.70 + "[| x \<in> nat; y \<in> nat; z \<in> nat |]
1.71 + ==> arity(injection_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
1.72 +by (simp add: injection_fm_def succ_Un_distrib [symmetric] Un_ac)
1.73 +
1.74 +lemma sats_injection_fm [simp]:
1.75 + "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
1.76 + ==> sats(A, injection_fm(x,y,z), env) <->
1.77 + injection(**A, nth(x,env), nth(y,env), nth(z,env))"
1.78 +by (simp add: injection_fm_def injection_def)
1.79 +
1.80 +lemma injection_iff_sats:
1.81 + "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
1.82 + i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
1.83 + ==> injection(**A, x, y, z) <-> sats(A, injection_fm(i,j,k), env)"
1.84 +by simp
1.85 +
1.86 +theorem injection_reflection [simplified,intro]:
1.87 + "L_Reflects(?Cl, \<lambda>x. injection(L,f(x),g(x),h(x)),
1.88 + \<lambda>i x. injection(**Lset(i),f(x),g(x),h(x)))"
1.89 +by (simp only: injection_def setclass_simps, fast)
1.90 +
1.91 +
1.92 +subsubsection{*Surjections*}
1.93 +
1.94 +(* surjection :: "[i=>o,i,i,i] => o"
1.95 + "surjection(M,A,B,f) ==
1.96 + typed_function(M,A,B,f) &
1.97 + (\<forall>y[M]. y\<in>B --> (\<exists>x[M]. x\<in>A & fun_apply(M,f,x,y)))" *)
1.98 +constdefs surjection_fm :: "[i,i,i]=>i"
1.99 + "surjection_fm(A,B,f) ==
1.100 + And(typed_function_fm(A,B,f),
1.101 + Forall(Implies(Member(0,succ(B)),
1.102 + Exists(And(Member(0,succ(succ(A))),
1.103 + fun_apply_fm(succ(succ(f)),0,1))))))"
1.104 +
1.105 +lemma surjection_type [TC]:
1.106 + "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> surjection_fm(x,y,z) \<in> formula"
1.107 +by (simp add: surjection_fm_def)
1.108 +
1.109 +lemma arity_surjection_fm [simp]:
1.110 + "[| x \<in> nat; y \<in> nat; z \<in> nat |]
1.111 + ==> arity(surjection_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
1.112 +by (simp add: surjection_fm_def succ_Un_distrib [symmetric] Un_ac)
1.113 +
1.114 +lemma sats_surjection_fm [simp]:
1.115 + "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
1.116 + ==> sats(A, surjection_fm(x,y,z), env) <->
1.117 + surjection(**A, nth(x,env), nth(y,env), nth(z,env))"
1.118 +by (simp add: surjection_fm_def surjection_def)
1.119 +
1.120 +lemma surjection_iff_sats:
1.121 + "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
1.122 + i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
1.123 + ==> surjection(**A, x, y, z) <-> sats(A, surjection_fm(i,j,k), env)"
1.124 +by simp
1.125 +
1.126 +theorem surjection_reflection [simplified,intro]:
1.127 + "L_Reflects(?Cl, \<lambda>x. surjection(L,f(x),g(x),h(x)),
1.128 + \<lambda>i x. surjection(**Lset(i),f(x),g(x),h(x)))"
1.129 +by (simp only: surjection_def setclass_simps, fast)
1.130 +
1.131 +
1.132 +
1.133 +subsubsection{*Bijections*}
1.134 +
1.135 +(* bijection :: "[i=>o,i,i,i] => o"
1.136 + "bijection(M,A,B,f) == injection(M,A,B,f) & surjection(M,A,B,f)" *)
1.137 +constdefs bijection_fm :: "[i,i,i]=>i"
1.138 + "bijection_fm(A,B,f) == And(injection_fm(A,B,f), surjection_fm(A,B,f))"
1.139 +
1.140 +lemma bijection_type [TC]:
1.141 + "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> bijection_fm(x,y,z) \<in> formula"
1.142 +by (simp add: bijection_fm_def)
1.143 +
1.144 +lemma arity_bijection_fm [simp]:
1.145 + "[| x \<in> nat; y \<in> nat; z \<in> nat |]
1.146 + ==> arity(bijection_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
1.147 +by (simp add: bijection_fm_def succ_Un_distrib [symmetric] Un_ac)
1.148 +
1.149 +lemma sats_bijection_fm [simp]:
1.150 + "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
1.151 + ==> sats(A, bijection_fm(x,y,z), env) <->
1.152 + bijection(**A, nth(x,env), nth(y,env), nth(z,env))"
1.153 +by (simp add: bijection_fm_def bijection_def)
1.154 +
1.155 +lemma bijection_iff_sats:
1.156 + "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
1.157 + i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
1.158 + ==> bijection(**A, x, y, z) <-> sats(A, bijection_fm(i,j,k), env)"
1.159 +by simp
1.160 +
1.161 +theorem bijection_reflection [simplified,intro]:
1.162 + "L_Reflects(?Cl, \<lambda>x. bijection(L,f(x),g(x),h(x)),
1.163 + \<lambda>i x. bijection(**Lset(i),f(x),g(x),h(x)))"
1.164 +by (simp only: bijection_def setclass_simps, fast)
1.165 +
1.166 +
1.167 +
1.168 +subsubsection{*Order-Isomorphisms*}
1.169 +
1.170 +(* order_isomorphism :: "[i=>o,i,i,i,i,i] => o"
1.171 + "order_isomorphism(M,A,r,B,s,f) ==
1.172 + bijection(M,A,B,f) &
1.173 + (\<forall>x[M]. x\<in>A --> (\<forall>y[M]. y\<in>A -->
1.174 + (\<forall>p[M]. \<forall>fx[M]. \<forall>fy[M]. \<forall>q[M].
1.175 + pair(M,x,y,p) --> fun_apply(M,f,x,fx) --> fun_apply(M,f,y,fy) -->
1.176 + pair(M,fx,fy,q) --> (p\<in>r <-> q\<in>s))))"
1.177 + *)
1.178 +
1.179 +constdefs order_isomorphism_fm :: "[i,i,i,i,i]=>i"
1.180 + "order_isomorphism_fm(A,r,B,s,f) ==
1.181 + And(bijection_fm(A,B,f),
1.182 + Forall(Implies(Member(0,succ(A)),
1.183 + Forall(Implies(Member(0,succ(succ(A))),
1.184 + Forall(Forall(Forall(Forall(
1.185 + Implies(pair_fm(5,4,3),
1.186 + Implies(fun_apply_fm(f#+6,5,2),
1.187 + Implies(fun_apply_fm(f#+6,4,1),
1.188 + Implies(pair_fm(2,1,0),
1.189 + Iff(Member(3,r#+6), Member(0,s#+6)))))))))))))))"
1.190 +
1.191 +lemma order_isomorphism_type [TC]:
1.192 + "[| A \<in> nat; r \<in> nat; B \<in> nat; s \<in> nat; f \<in> nat |]
1.193 + ==> order_isomorphism_fm(A,r,B,s,f) \<in> formula"
1.194 +by (simp add: order_isomorphism_fm_def)
1.195 +
1.196 +lemma arity_order_isomorphism_fm [simp]:
1.197 + "[| A \<in> nat; r \<in> nat; B \<in> nat; s \<in> nat; f \<in> nat |]
1.198 + ==> arity(order_isomorphism_fm(A,r,B,s,f)) =
1.199 + succ(A) \<union> succ(r) \<union> succ(B) \<union> succ(s) \<union> succ(f)"
1.200 +by (simp add: order_isomorphism_fm_def succ_Un_distrib [symmetric] Un_ac)
1.201 +
1.202 +lemma sats_order_isomorphism_fm [simp]:
1.203 + "[| U \<in> nat; r \<in> nat; B \<in> nat; s \<in> nat; f \<in> nat; env \<in> list(A)|]
1.204 + ==> sats(A, order_isomorphism_fm(U,r,B,s,f), env) <->
1.205 + order_isomorphism(**A, nth(U,env), nth(r,env), nth(B,env),
1.206 + nth(s,env), nth(f,env))"
1.207 +by (simp add: order_isomorphism_fm_def order_isomorphism_def)
1.208 +
1.209 +lemma order_isomorphism_iff_sats:
1.210 + "[| nth(i,env) = U; nth(j,env) = r; nth(k,env) = B; nth(j',env) = s;
1.211 + nth(k',env) = f;
1.212 + i \<in> nat; j \<in> nat; k \<in> nat; j' \<in> nat; k' \<in> nat; env \<in> list(A)|]
1.213 + ==> order_isomorphism(**A,U,r,B,s,f) <->
1.214 + sats(A, order_isomorphism_fm(i,j,k,j',k'), env)"
1.215 +by simp
1.216 +
1.217 +theorem order_isomorphism_reflection [simplified,intro]:
1.218 + "L_Reflects(?Cl, \<lambda>x. order_isomorphism(L,f(x),g(x),h(x),g'(x),h'(x)),
1.219 + \<lambda>i x. order_isomorphism(**Lset(i),f(x),g(x),h(x),g'(x),h'(x)))"
1.220 +by (simp only: order_isomorphism_def setclass_simps, fast)
1.221 +
1.222 +
1.223 end