src/ZF/Coind/Map.ML
author lcp
Thu Apr 06 12:22:26 1995 +0200 (1995-04-06)
changeset 1020 76d72126a9e7
parent 915 6dae0daf57b7
child 1075 848bf2e18dff
permissions -rw-r--r--
Modified proofs for new hyp_subst_tac, and simplified them.
     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 qed "mapQU";
    54 
    55 (* ############################################################ *)
    56 (* Monotonicity                                                 *)
    57 (* ############################################################ *)
    58 
    59 goalw Map.thy [PMap_def,TMap_def] "!!A.B<=C ==> PMap(A,B)<=PMap(A,C)";
    60 by (fast_tac ZF_cs 1);
    61 qed "map_mono";
    62 
    63 (* Rename to pmap_mono *)
    64 
    65 (* ############################################################ *)
    66 (* Introduction Rules                                           *)
    67 (* ############################################################ *)
    68 
    69 (** map_emp **)
    70 
    71 goalw Map.thy [map_emp_def,PMap_def,TMap_def] "map_emp:PMap(A,B)";
    72 by (safe_tac ZF_cs);
    73 by (rtac image_02 1);
    74 qed "pmap_empI";
    75 
    76 (** map_owr **)
    77 
    78 
    79 goalw Map.thy [map_owr_def,PMap_def,TMap_def] 
    80   "!! A.[| m:PMap(A,B); a:A; b:B |]  ==> map_owr(m,a,b):PMap(A,B)";
    81 by (safe_tac ZF_cs);
    82 by (asm_full_simp_tac if_ss 1 THEN fast_tac ZF_cs 1);
    83 by (fast_tac ZF_cs 1);
    84 by (asm_full_simp_tac (ZF_ss addsimps [if_iff]) 1);
    85 by (fast_tac ZF_cs 1);
    86 by (rtac (excluded_middle RS disjE) 1);
    87 by (etac image_Sigma1 1);
    88 by (safe_tac upair_cs);    (*This claset knows nothing about domain(m).*)
    89 by (asm_full_simp_tac (ZF_ss addsimps [qbeta]) 1);
    90 by (asm_simp_tac (ZF_ss addsimps [qbeta] setloop split_tac [expand_if]) 1);
    91 by (safe_tac FOL_cs);
    92 by (asm_full_simp_tac (ZF_ss addsimps [qbeta]) 1);
    93 by (dres_inst_tac [("psi", "?uu ~: B")] asm_rl 1);
    94 by (asm_full_simp_tac (ZF_ss addsimps [qbeta]) 1);
    95 by (fast_tac ZF_cs 1);
    96 qed "pmap_owrI";
    97 
    98 (** map_app **)
    99 
   100 goalw Map.thy [TMap_def,map_app_def] 
   101   "!!m.[| m:TMap(A,B); a:domain(m) |] ==> map_app(m,a) ~=0";
   102 by (etac domainE 1);
   103 by (dtac imageI 1);
   104 by (fast_tac ZF_cs 1);
   105 by (etac not_emptyI 1);
   106 qed "tmap_app_notempty";
   107 
   108 goalw Map.thy [TMap_def,map_app_def,domain_def] 
   109   "!!m.[| m:TMap(A,B); a:domain(m) |] ==> map_app(m,a):B";
   110 by (fast_tac eq_cs 1);
   111 qed "tmap_appI";
   112 
   113 goalw Map.thy [PMap_def]
   114   "!!m.[| m:PMap(A,B); a:domain(m) |] ==> map_app(m,a):B";
   115 by (forward_tac [tmap_app_notempty] 1); 
   116 by (assume_tac 1);
   117 by (dtac tmap_appI 1); 
   118 by (assume_tac 1);
   119 by (fast_tac ZF_cs 1);
   120 qed "pmap_appI";
   121 
   122 (** domain **)
   123 
   124 goalw Map.thy [TMap_def]
   125   "!!m.[| m:TMap(A,B); a:domain(m) |] ==> a:A";
   126 by (fast_tac eq_cs 1);
   127 qed "tmap_domainD";
   128 
   129 goalw Map.thy [PMap_def,TMap_def]
   130   "!!m.[| m:PMap(A,B); a:domain(m) |] ==> a:A";
   131 by (fast_tac eq_cs 1);
   132 qed "pmap_domainD";
   133 
   134 (* ############################################################ *)
   135 (* Equalitites                                                  *)
   136 (* ############################################################ *)
   137 
   138 (** Domain **)
   139 
   140 (* Lemmas *)
   141 
   142 goal Map.thy  "domain(UN x:A.B(x)) = (UN x:A.domain(B(x)))";
   143 by (fast_tac eq_cs 1);
   144 qed "domain_UN";
   145 
   146 goal Map.thy  "domain(Sigma(A,B)) = {x:A.EX y.y:B(x)}";
   147 by (simp_tac (ZF_ss addsimps [domain_UN,domain_0,domain_cons]) 1);
   148 by (fast_tac eq_cs 1);
   149 qed "domain_Sigma";
   150 
   151 (* Theorems *)
   152 
   153 goalw Map.thy [map_emp_def] "domain(map_emp) = 0";
   154 by (fast_tac eq_cs 1);
   155 qed "map_domain_emp";
   156 
   157 goalw Map.thy [map_owr_def] 
   158   "!!a.b ~= 0 ==> domain(map_owr(f,a,b)) = {a} Un domain(f)";
   159 by (simp_tac (if_ss addsimps [domain_Sigma]) 1);
   160 by (rtac equalityI 1);
   161 by (fast_tac eq_cs 1);
   162 by (rtac subsetI 1);
   163 by (rtac CollectI 1);
   164 by (assume_tac 1);
   165 by (etac UnE' 1);
   166 by (etac singletonE 1);
   167 by (asm_simp_tac if_ss 1);
   168 by (fast_tac eq_cs 1);
   169 by (etac notsingletonE 1);
   170 by (asm_simp_tac if_ss 1);
   171 by (fast_tac eq_cs 1);
   172 qed "map_domain_owr";
   173 
   174 (** Application **)
   175 
   176 goalw Map.thy [map_app_def,map_owr_def] 
   177   "map_app(map_owr(f,a,b),a) = b";
   178 by (rtac (qbeta RS ssubst) 1);
   179 by (fast_tac ZF_cs 1);
   180 by (simp_tac if_ss 1);
   181 qed "map_app_owr1";
   182 
   183 goalw Map.thy [map_app_def,map_owr_def] 
   184   "!!a.c ~= a ==> map_app(map_owr(f,a,b),c)= map_app(f,c)";
   185 by (rtac (excluded_middle RS disjE) 1);
   186 by (rtac (qbeta_emp RS ssubst) 1);
   187 by (assume_tac 1);
   188 by (fast_tac eq_cs 1);
   189 by (etac (qbeta RS ssubst) 1);
   190 by (asm_simp_tac if_ss 1);
   191 qed "map_app_owr2";
   192 
   193 
   194 
   195 
   196 
   197 
   198 
   199 
   200 
   201 
   202 
   203 
   204 
   205 
   206 
   207 
   208 
   209 
   210 
   211 
   212 
   213 
   214 
   215 
   216 
   217 
   218 
   219 
   220 
   221 
   222 
   223 
   224 
   225 
   226 
   227 
   228 
   229 
   230 
   231 
   232