reflection for more internal formulas
authorpaulson
Mon Jul 08 12:31:16 2002 +0200 (2002-07-08)
changeset 13309a6adee8ea75a
parent 13308 1dbed9ea764b
child 13310 d694e65127ba
reflection for more internal formulas
src/ZF/Constructible/L_axioms.thy
     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