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