src/ZF/Coind/Map.ML
changeset 915 6dae0daf57b7
child 1020 76d72126a9e7
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/ZF/Coind/Map.ML	Mon Feb 27 18:12:21 1995 +0100
     1.3 @@ -0,0 +1,249 @@
     1.4 +(*  Title: 	ZF/Coind/Map.ML
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Jacob Frost, Cambridge University Computer Laboratory
     1.7 +    Copyright   1995  University of Cambridge
     1.8 +*)
     1.9 +
    1.10 +open Map;
    1.11 +
    1.12 +(* ############################################################ *)
    1.13 +(* Lemmas                                                       *)
    1.14 +(* ############################################################ *)
    1.15 +
    1.16 +goal Map.thy "!!A. a:A ==> Sigma(A,B)``{a} = B(a)";
    1.17 +by (fast_tac eq_cs 1);
    1.18 +qed "qbeta";
    1.19 +
    1.20 +goal Map.thy "!!A. a~:A ==> Sigma(A,B)``{a} = 0";
    1.21 +by (fast_tac eq_cs 1);
    1.22 +qed "qbeta_emp";
    1.23 +
    1.24 +goal Map.thy "!!A.a ~: A ==> Sigma(A,B)``{a}=0";
    1.25 +by (fast_tac eq_cs 1);
    1.26 +qed "image_Sigma1";
    1.27 +
    1.28 +goal Map.thy "0``A = 0";
    1.29 +by (fast_tac eq_cs 1);
    1.30 +qed "image_02";
    1.31 +
    1.32 +(* ############################################################ *)
    1.33 +(* Inclusion in Quine Universes                                 *)
    1.34 +(* ############################################################ *)
    1.35 +
    1.36 +(* Lemmas *)
    1.37 +
    1.38 +goalw Map.thy [quniv_def]
    1.39 +    "!!A. A <= univ(X) ==> Pow(A * Union(quniv(X))) <= quniv(X)";
    1.40 +by (rtac Pow_mono 1);
    1.41 +by (rtac ([Sigma_mono, product_univ] MRS subset_trans) 1);
    1.42 +by (etac subset_trans 1);
    1.43 +by (rtac (arg_subset_eclose RS univ_mono) 1);
    1.44 +by (simp_tac (ZF_ss addsimps [Union_Pow_eq]) 1);
    1.45 +qed "MapQU_lemma";
    1.46 +
    1.47 +(* Theorems *)
    1.48 +
    1.49 +val prems = goalw Map.thy [PMap_def,TMap_def]
    1.50 +  "[| m:PMap(A,quniv(B)); !!x.x:A ==> x:univ(B) |] ==> m:quniv(B)";
    1.51 +by (cut_facts_tac prems 1);
    1.52 +by (rtac (MapQU_lemma RS subsetD) 1);
    1.53 +by (rtac subsetI 1);
    1.54 +by (eresolve_tac prems 1);
    1.55 +by (fast_tac ZF_cs 1);
    1.56 +by flexflex_tac;
    1.57 +qed "mapQU";
    1.58 +
    1.59 +(* ############################################################ *)
    1.60 +(* Monotonicity                                                 *)
    1.61 +(* ############################################################ *)
    1.62 +
    1.63 +goalw Map.thy [PMap_def,TMap_def] "!!A.B<=C ==> PMap(A,B)<=PMap(A,C)";
    1.64 +by (fast_tac ZF_cs 1);
    1.65 +by (flexflex_tac);
    1.66 +qed "map_mono";
    1.67 +
    1.68 +(* Rename to pmap_mono *)
    1.69 +
    1.70 +(* ############################################################ *)
    1.71 +(* Introduction Rules                                           *)
    1.72 +(* ############################################################ *)
    1.73 +
    1.74 +(** map_emp **)
    1.75 +
    1.76 +goalw Map.thy [map_emp_def,PMap_def,TMap_def] "map_emp:PMap(A,B)";
    1.77 +by (safe_tac ZF_cs);
    1.78 +by (rtac image_02 1);
    1.79 +qed "pmap_empI";
    1.80 +
    1.81 +(** map_owr **)
    1.82 +
    1.83 +goalw Map.thy [map_owr_def,PMap_def,TMap_def] 
    1.84 +  "!! A.[| m:PMap(A,B); a:A; b:B |]  ==> map_owr(m,a,b):PMap(A,B)";
    1.85 +by (safe_tac ZF_cs);
    1.86 +
    1.87 +by (asm_full_simp_tac if_ss 1);
    1.88 +by (fast_tac ZF_cs 1);
    1.89 +
    1.90 +by (fast_tac ZF_cs 1);
    1.91 +
    1.92 +by (rtac (excluded_middle RS disjE) 1);
    1.93 +by (dtac (if_not_P RS subst) 1);
    1.94 +by (assume_tac 1);
    1.95 +by (fast_tac ZF_cs 1);
    1.96 +by (hyp_subst_tac 1);
    1.97 +by (asm_full_simp_tac if_ss 1);
    1.98 +by (fast_tac ZF_cs 1);
    1.99 +
   1.100 +by (rtac (excluded_middle RS disjE) 1);
   1.101 +by (etac image_Sigma1 1);
   1.102 +by (rtac (qbeta RS ssubst) 1);
   1.103 +by (assume_tac 1);
   1.104 +by (dtac map_lem1 1);
   1.105 +by (etac qbeta 1);
   1.106 +by (etac UnE'  1);
   1.107 +by (etac singletonE 1);
   1.108 +by (hyp_subst_tac 1);
   1.109 +by (asm_full_simp_tac (if_ss addsimps [qbeta]) 1);
   1.110 +by (etac notsingletonE 1);
   1.111 +by (dtac map_lem1 1);
   1.112 +by (rtac if_not_P 1);
   1.113 +by (assume_tac 1);
   1.114 +by (asm_full_simp_tac (if_ss addsimps [qbeta]) 1);
   1.115 +by (fast_tac ZF_cs 1);
   1.116 +qed "pmap_owrI";
   1.117 +
   1.118 +(** map_app **)
   1.119 +
   1.120 +goalw Map.thy [TMap_def,map_app_def] 
   1.121 +  "!!m.[| m:TMap(A,B); a:domain(m) |] ==> map_app(m,a) ~=0";
   1.122 +by (etac domainE 1);
   1.123 +by (dtac imageI 1);
   1.124 +by (fast_tac ZF_cs 1);
   1.125 +by (etac not_emptyI 1);
   1.126 +qed "tmap_app_notempty";
   1.127 +
   1.128 +goalw Map.thy [TMap_def,map_app_def,domain_def] 
   1.129 +  "!!m.[| m:TMap(A,B); a:domain(m) |] ==> map_app(m,a):B";
   1.130 +by (fast_tac eq_cs 1);
   1.131 +qed "tmap_appI";
   1.132 +
   1.133 +goalw Map.thy [PMap_def]
   1.134 +  "!!m.[| m:PMap(A,B); a:domain(m) |] ==> map_app(m,a):B";
   1.135 +by (forward_tac [tmap_app_notempty] 1); 
   1.136 +by (assume_tac 1);
   1.137 +by (dtac tmap_appI 1); 
   1.138 +by (assume_tac 1);
   1.139 +by (fast_tac ZF_cs 1);
   1.140 +qed "pmap_appI";
   1.141 +
   1.142 +(** domain **)
   1.143 +
   1.144 +goalw Map.thy [TMap_def]
   1.145 +  "!!m.[| m:TMap(A,B); a:domain(m) |] ==> a:A";
   1.146 +by (fast_tac eq_cs 1);
   1.147 +qed "tmap_domainD";
   1.148 +
   1.149 +goalw Map.thy [PMap_def,TMap_def]
   1.150 +  "!!m.[| m:PMap(A,B); a:domain(m) |] ==> a:A";
   1.151 +by (fast_tac eq_cs 1);
   1.152 +qed "pmap_domainD";
   1.153 +
   1.154 +(* ############################################################ *)
   1.155 +(* Equalitites                                                  *)
   1.156 +(* ############################################################ *)
   1.157 +
   1.158 +(** Domain **)
   1.159 +
   1.160 +(* Lemmas *)
   1.161 +
   1.162 +goal Map.thy  "domain(UN x:A.B(x)) = (UN x:A.domain(B(x)))";
   1.163 +by (fast_tac eq_cs 1);
   1.164 +qed "domain_UN";
   1.165 +
   1.166 +goal Map.thy  "domain(Sigma(A,B)) = {x:A.EX y.y:B(x)}";
   1.167 +by (simp_tac (ZF_ss addsimps [domain_UN,domain_0,domain_cons]) 1);
   1.168 +by (fast_tac eq_cs 1);
   1.169 +qed "domain_Sigma";
   1.170 +
   1.171 +(* Theorems *)
   1.172 +
   1.173 +goalw Map.thy [map_emp_def] "domain(map_emp) = 0";
   1.174 +by (fast_tac eq_cs 1);
   1.175 +qed "map_domain_emp";
   1.176 +
   1.177 +goalw Map.thy [map_owr_def] 
   1.178 +  "!!a.b ~= 0 ==> domain(map_owr(f,a,b)) = {a} Un domain(f)";
   1.179 +by (simp_tac (if_ss addsimps [domain_Sigma]) 1);
   1.180 +by (rtac equalityI 1);
   1.181 +by (fast_tac eq_cs 1);
   1.182 +by (rtac subsetI 1);
   1.183 +by (rtac CollectI 1);
   1.184 +by (assume_tac 1);
   1.185 +by (etac UnE' 1);
   1.186 +by (etac singletonE 1);
   1.187 +by (asm_simp_tac if_ss 1);
   1.188 +by (fast_tac eq_cs 1);
   1.189 +by (etac notsingletonE 1);
   1.190 +by (asm_simp_tac if_ss 1);
   1.191 +by (fast_tac eq_cs 1);
   1.192 +qed "map_domain_owr";
   1.193 +
   1.194 +(** Application **)
   1.195 +
   1.196 +goalw Map.thy [map_app_def,map_owr_def] 
   1.197 +  "map_app(map_owr(f,a,b),a) = b";
   1.198 +by (rtac (qbeta RS ssubst) 1);
   1.199 +by (fast_tac ZF_cs 1);
   1.200 +by (simp_tac if_ss 1);
   1.201 +qed "map_app_owr1";
   1.202 +
   1.203 +goalw Map.thy [map_app_def,map_owr_def] 
   1.204 +  "!!a.c ~= a ==> map_app(map_owr(f,a,b),c)= map_app(f,c)";
   1.205 +by (rtac (excluded_middle RS disjE) 1);
   1.206 +by (rtac (qbeta_emp RS ssubst) 1);
   1.207 +by (assume_tac 1);
   1.208 +by (fast_tac eq_cs 1);
   1.209 +by (etac (qbeta RS ssubst) 1);
   1.210 +by (asm_simp_tac if_ss 1);
   1.211 +qed "map_app_owr2";
   1.212 +
   1.213 +
   1.214 +
   1.215 +
   1.216 +
   1.217 +
   1.218 +
   1.219 +
   1.220 +
   1.221 +
   1.222 +
   1.223 +
   1.224 +
   1.225 +
   1.226 +
   1.227 +
   1.228 +
   1.229 +
   1.230 +
   1.231 +
   1.232 +
   1.233 +
   1.234 +
   1.235 +
   1.236 +
   1.237 +
   1.238 +
   1.239 +
   1.240 +
   1.241 +
   1.242 +
   1.243 +
   1.244 +
   1.245 +
   1.246 +
   1.247 +
   1.248 +
   1.249 +
   1.250 +
   1.251 +
   1.252 +