src/ZF/Coind/Map.ML
author lcp
Mon Feb 27 18:12:21 1995 +0100 (1995-02-27)
changeset 915 6dae0daf57b7
child 1020 76d72126a9e7
permissions -rw-r--r--
New example by Jacob Frost, tidied by lcp
     1 (*  Title: 	ZF/Coind/Map.ML
     2     ID:         $Id$
     3     Author: 	Jacob Frost, Cambridge University Computer Laboratory
     4     Copyright   1995  University of Cambridge
     5 *)
     6 
     7 open Map;
     8 
     9 (* ############################################################ *)
    10 (* Lemmas                                                       *)
    11 (* ############################################################ *)
    12 
    13 goal Map.thy "!!A. a:A ==> Sigma(A,B)``{a} = B(a)";
    14 by (fast_tac eq_cs 1);
    15 qed "qbeta";
    16 
    17 goal Map.thy "!!A. a~:A ==> Sigma(A,B)``{a} = 0";
    18 by (fast_tac eq_cs 1);
    19 qed "qbeta_emp";
    20 
    21 goal Map.thy "!!A.a ~: A ==> Sigma(A,B)``{a}=0";
    22 by (fast_tac eq_cs 1);
    23 qed "image_Sigma1";
    24 
    25 goal Map.thy "0``A = 0";
    26 by (fast_tac eq_cs 1);
    27 qed "image_02";
    28 
    29 (* ############################################################ *)
    30 (* Inclusion in Quine Universes                                 *)
    31 (* ############################################################ *)
    32 
    33 (* Lemmas *)
    34 
    35 goalw Map.thy [quniv_def]
    36     "!!A. A <= univ(X) ==> Pow(A * Union(quniv(X))) <= quniv(X)";
    37 by (rtac Pow_mono 1);
    38 by (rtac ([Sigma_mono, product_univ] MRS subset_trans) 1);
    39 by (etac subset_trans 1);
    40 by (rtac (arg_subset_eclose RS univ_mono) 1);
    41 by (simp_tac (ZF_ss addsimps [Union_Pow_eq]) 1);
    42 qed "MapQU_lemma";
    43 
    44 (* Theorems *)
    45 
    46 val prems = goalw Map.thy [PMap_def,TMap_def]
    47   "[| m:PMap(A,quniv(B)); !!x.x:A ==> x:univ(B) |] ==> m:quniv(B)";
    48 by (cut_facts_tac prems 1);
    49 by (rtac (MapQU_lemma RS subsetD) 1);
    50 by (rtac subsetI 1);
    51 by (eresolve_tac prems 1);
    52 by (fast_tac ZF_cs 1);
    53 by flexflex_tac;
    54 qed "mapQU";
    55 
    56 (* ############################################################ *)
    57 (* Monotonicity                                                 *)
    58 (* ############################################################ *)
    59 
    60 goalw Map.thy [PMap_def,TMap_def] "!!A.B<=C ==> PMap(A,B)<=PMap(A,C)";
    61 by (fast_tac ZF_cs 1);
    62 by (flexflex_tac);
    63 qed "map_mono";
    64 
    65 (* Rename to pmap_mono *)
    66 
    67 (* ############################################################ *)
    68 (* Introduction Rules                                           *)
    69 (* ############################################################ *)
    70 
    71 (** map_emp **)
    72 
    73 goalw Map.thy [map_emp_def,PMap_def,TMap_def] "map_emp:PMap(A,B)";
    74 by (safe_tac ZF_cs);
    75 by (rtac image_02 1);
    76 qed "pmap_empI";
    77 
    78 (** map_owr **)
    79 
    80 goalw Map.thy [map_owr_def,PMap_def,TMap_def] 
    81   "!! A.[| m:PMap(A,B); a:A; b:B |]  ==> map_owr(m,a,b):PMap(A,B)";
    82 by (safe_tac ZF_cs);
    83 
    84 by (asm_full_simp_tac if_ss 1);
    85 by (fast_tac ZF_cs 1);
    86 
    87 by (fast_tac ZF_cs 1);
    88 
    89 by (rtac (excluded_middle RS disjE) 1);
    90 by (dtac (if_not_P RS subst) 1);
    91 by (assume_tac 1);
    92 by (fast_tac ZF_cs 1);
    93 by (hyp_subst_tac 1);
    94 by (asm_full_simp_tac if_ss 1);
    95 by (fast_tac ZF_cs 1);
    96 
    97 by (rtac (excluded_middle RS disjE) 1);
    98 by (etac image_Sigma1 1);
    99 by (rtac (qbeta RS ssubst) 1);
   100 by (assume_tac 1);
   101 by (dtac map_lem1 1);
   102 by (etac qbeta 1);
   103 by (etac UnE'  1);
   104 by (etac singletonE 1);
   105 by (hyp_subst_tac 1);
   106 by (asm_full_simp_tac (if_ss addsimps [qbeta]) 1);
   107 by (etac notsingletonE 1);
   108 by (dtac map_lem1 1);
   109 by (rtac if_not_P 1);
   110 by (assume_tac 1);
   111 by (asm_full_simp_tac (if_ss addsimps [qbeta]) 1);
   112 by (fast_tac ZF_cs 1);
   113 qed "pmap_owrI";
   114 
   115 (** map_app **)
   116 
   117 goalw Map.thy [TMap_def,map_app_def] 
   118   "!!m.[| m:TMap(A,B); a:domain(m) |] ==> map_app(m,a) ~=0";
   119 by (etac domainE 1);
   120 by (dtac imageI 1);
   121 by (fast_tac ZF_cs 1);
   122 by (etac not_emptyI 1);
   123 qed "tmap_app_notempty";
   124 
   125 goalw Map.thy [TMap_def,map_app_def,domain_def] 
   126   "!!m.[| m:TMap(A,B); a:domain(m) |] ==> map_app(m,a):B";
   127 by (fast_tac eq_cs 1);
   128 qed "tmap_appI";
   129 
   130 goalw Map.thy [PMap_def]
   131   "!!m.[| m:PMap(A,B); a:domain(m) |] ==> map_app(m,a):B";
   132 by (forward_tac [tmap_app_notempty] 1); 
   133 by (assume_tac 1);
   134 by (dtac tmap_appI 1); 
   135 by (assume_tac 1);
   136 by (fast_tac ZF_cs 1);
   137 qed "pmap_appI";
   138 
   139 (** domain **)
   140 
   141 goalw Map.thy [TMap_def]
   142   "!!m.[| m:TMap(A,B); a:domain(m) |] ==> a:A";
   143 by (fast_tac eq_cs 1);
   144 qed "tmap_domainD";
   145 
   146 goalw Map.thy [PMap_def,TMap_def]
   147   "!!m.[| m:PMap(A,B); a:domain(m) |] ==> a:A";
   148 by (fast_tac eq_cs 1);
   149 qed "pmap_domainD";
   150 
   151 (* ############################################################ *)
   152 (* Equalitites                                                  *)
   153 (* ############################################################ *)
   154 
   155 (** Domain **)
   156 
   157 (* Lemmas *)
   158 
   159 goal Map.thy  "domain(UN x:A.B(x)) = (UN x:A.domain(B(x)))";
   160 by (fast_tac eq_cs 1);
   161 qed "domain_UN";
   162 
   163 goal Map.thy  "domain(Sigma(A,B)) = {x:A.EX y.y:B(x)}";
   164 by (simp_tac (ZF_ss addsimps [domain_UN,domain_0,domain_cons]) 1);
   165 by (fast_tac eq_cs 1);
   166 qed "domain_Sigma";
   167 
   168 (* Theorems *)
   169 
   170 goalw Map.thy [map_emp_def] "domain(map_emp) = 0";
   171 by (fast_tac eq_cs 1);
   172 qed "map_domain_emp";
   173 
   174 goalw Map.thy [map_owr_def] 
   175   "!!a.b ~= 0 ==> domain(map_owr(f,a,b)) = {a} Un domain(f)";
   176 by (simp_tac (if_ss addsimps [domain_Sigma]) 1);
   177 by (rtac equalityI 1);
   178 by (fast_tac eq_cs 1);
   179 by (rtac subsetI 1);
   180 by (rtac CollectI 1);
   181 by (assume_tac 1);
   182 by (etac UnE' 1);
   183 by (etac singletonE 1);
   184 by (asm_simp_tac if_ss 1);
   185 by (fast_tac eq_cs 1);
   186 by (etac notsingletonE 1);
   187 by (asm_simp_tac if_ss 1);
   188 by (fast_tac eq_cs 1);
   189 qed "map_domain_owr";
   190 
   191 (** Application **)
   192 
   193 goalw Map.thy [map_app_def,map_owr_def] 
   194   "map_app(map_owr(f,a,b),a) = b";
   195 by (rtac (qbeta RS ssubst) 1);
   196 by (fast_tac ZF_cs 1);
   197 by (simp_tac if_ss 1);
   198 qed "map_app_owr1";
   199 
   200 goalw Map.thy [map_app_def,map_owr_def] 
   201   "!!a.c ~= a ==> map_app(map_owr(f,a,b),c)= map_app(f,c)";
   202 by (rtac (excluded_middle RS disjE) 1);
   203 by (rtac (qbeta_emp RS ssubst) 1);
   204 by (assume_tac 1);
   205 by (fast_tac eq_cs 1);
   206 by (etac (qbeta RS ssubst) 1);
   207 by (asm_simp_tac if_ss 1);
   208 qed "map_app_owr2";
   209 
   210 
   211 
   212 
   213 
   214 
   215 
   216 
   217 
   218 
   219 
   220 
   221 
   222 
   223 
   224 
   225 
   226 
   227 
   228 
   229 
   230 
   231 
   232 
   233 
   234 
   235 
   236 
   237 
   238 
   239 
   240 
   241 
   242 
   243 
   244 
   245 
   246 
   247 
   248 
   249