src/ZF/perm.ML
author clasohm
Thu Sep 16 12:20:38 1993 +0200 (1993-09-16)
changeset 0 a5a9c433f639
child 6 8ce8c4d13d4d
permissions -rw-r--r--
Initial revision
clasohm@0
     1
(*  Title: 	ZF/perm.ML
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1991  University of Cambridge
clasohm@0
     5
clasohm@0
     6
For perm.thy.  The theory underlying permutation groups
clasohm@0
     7
  -- Composition of relations, the identity relation
clasohm@0
     8
  -- Injections, surjections, bijections
clasohm@0
     9
  -- Lemmas for the Schroeder-Bernstein Theorem
clasohm@0
    10
*)
clasohm@0
    11
clasohm@0
    12
open Perm;
clasohm@0
    13
clasohm@0
    14
(** Surjective function space **)
clasohm@0
    15
clasohm@0
    16
goalw Perm.thy [surj_def] "!!f A B. f: surj(A,B) ==> f: A->B";
clasohm@0
    17
by (etac CollectD1 1);
clasohm@0
    18
val surj_is_fun = result();
clasohm@0
    19
clasohm@0
    20
goalw Perm.thy [surj_def] "!!f A B. f : Pi(A,B) ==> f: surj(A,range(f))";
clasohm@0
    21
by (fast_tac (ZF_cs addIs [apply_equality] 
clasohm@0
    22
		    addEs [range_of_fun,domain_type]) 1);
clasohm@0
    23
val fun_is_surj = result();
clasohm@0
    24
clasohm@0
    25
goalw Perm.thy [surj_def] "!!f A B. f: surj(A,B) ==> range(f)=B";
clasohm@0
    26
by (best_tac (ZF_cs addIs [equalityI,apply_Pair] addEs [range_type]) 1);
clasohm@0
    27
val surj_range = result();
clasohm@0
    28
clasohm@0
    29
clasohm@0
    30
(** Injective function space **)
clasohm@0
    31
clasohm@0
    32
goalw Perm.thy [inj_def] "!!f A B. f: inj(A,B) ==> f: A->B";
clasohm@0
    33
by (etac CollectD1 1);
clasohm@0
    34
val inj_is_fun = result();
clasohm@0
    35
clasohm@0
    36
goalw Perm.thy [inj_def]
clasohm@0
    37
    "!!f A B. [| <a,b>:f;  <c,b>:f;  f: inj(A,B) |] ==> a=c";
clasohm@0
    38
by (REPEAT (eresolve_tac [asm_rl, Pair_mem_PiE, CollectE] 1));
clasohm@0
    39
by (fast_tac ZF_cs 1);
clasohm@0
    40
val inj_equality = result();
clasohm@0
    41
clasohm@0
    42
(** Bijections -- simple lemmas but no intro/elim rules -- use unfolding **)
clasohm@0
    43
clasohm@0
    44
goalw Perm.thy [bij_def] "!!f A B. f: bij(A,B) ==> f: inj(A,B)";
clasohm@0
    45
by (etac IntD1 1);
clasohm@0
    46
val bij_is_inj = result();
clasohm@0
    47
clasohm@0
    48
goalw Perm.thy [bij_def] "!!f A B. f: bij(A,B) ==> f: surj(A,B)";
clasohm@0
    49
by (etac IntD2 1);
clasohm@0
    50
val bij_is_surj = result();
clasohm@0
    51
clasohm@0
    52
(* f: bij(A,B) ==> f: A->B *)
clasohm@0
    53
val bij_is_fun = standard (bij_is_inj RS inj_is_fun);
clasohm@0
    54
clasohm@0
    55
(** Identity function **)
clasohm@0
    56
clasohm@0
    57
val [prem] = goalw Perm.thy [id_def] "a:A ==> <a,a> : id(A)";  
clasohm@0
    58
by (rtac (prem RS lamI) 1);
clasohm@0
    59
val idI = result();
clasohm@0
    60
clasohm@0
    61
val major::prems = goalw Perm.thy [id_def]
clasohm@0
    62
    "[| p: id(A);  !!x.[| x:A; p=<x,x> |] ==> P  \
clasohm@0
    63
\    |] ==>  P";  
clasohm@0
    64
by (rtac (major RS lamE) 1);
clasohm@0
    65
by (REPEAT (ares_tac prems 1));
clasohm@0
    66
val idE = result();
clasohm@0
    67
clasohm@0
    68
goalw Perm.thy [id_def] "id(A) : A->A";  
clasohm@0
    69
by (rtac lam_type 1);
clasohm@0
    70
by (assume_tac 1);
clasohm@0
    71
val id_type = result();
clasohm@0
    72
clasohm@0
    73
val [prem] = goalw Perm.thy [id_def] "A<=B ==> id(A) <= id(B)";
clasohm@0
    74
by (rtac (prem RS lam_mono) 1);
clasohm@0
    75
val id_mono = result();
clasohm@0
    76
clasohm@0
    77
goalw Perm.thy [inj_def,id_def] "id(A): inj(A,A)";
clasohm@0
    78
by (REPEAT (ares_tac [CollectI,lam_type] 1));
clasohm@0
    79
by (SIMP_TAC ZF_ss 1);
clasohm@0
    80
val id_inj = result();
clasohm@0
    81
clasohm@0
    82
goalw Perm.thy [id_def,surj_def] "id(A): surj(A,A)";
clasohm@0
    83
by (fast_tac (ZF_cs addIs [lam_type,beta]) 1);
clasohm@0
    84
val id_surj = result();
clasohm@0
    85
clasohm@0
    86
goalw Perm.thy [bij_def] "id(A): bij(A,A)";
clasohm@0
    87
by (fast_tac (ZF_cs addIs [id_inj,id_surj]) 1);
clasohm@0
    88
val id_bij = result();
clasohm@0
    89
clasohm@0
    90
clasohm@0
    91
(** Converse of a relation **)
clasohm@0
    92
clasohm@0
    93
val [prem] = goal Perm.thy "f: inj(A,B) ==> converse(f) : range(f)->A";
clasohm@0
    94
by (rtac (prem RS inj_is_fun RS PiE) 1);
clasohm@0
    95
by (rtac (converse_type RS PiI) 1);
clasohm@0
    96
by (fast_tac ZF_cs 1);
clasohm@0
    97
by (fast_tac (ZF_cs addEs [prem RSN (3,inj_equality)]) 1);
clasohm@0
    98
by flexflex_tac;
clasohm@0
    99
val inj_converse_fun = result();
clasohm@0
   100
clasohm@0
   101
val prems = goalw Perm.thy [surj_def]
clasohm@0
   102
    "f: inj(A,B) ==> converse(f): surj(range(f), A)";
clasohm@0
   103
by (fast_tac (ZF_cs addIs (prems@[inj_converse_fun,apply_Pair,apply_equality,
clasohm@0
   104
			 converseI,inj_is_fun])) 1);
clasohm@0
   105
val inj_converse_surj = result();
clasohm@0
   106
clasohm@0
   107
(*The premises are equivalent to saying that f is injective...*) 
clasohm@0
   108
val prems = goal Perm.thy
clasohm@0
   109
    "[| f: A->B;  converse(f): C->A;  a: A |] ==> converse(f)`(f`a) = a";
clasohm@0
   110
by (fast_tac (ZF_cs addIs (prems@[apply_Pair,apply_equality,converseI])) 1);
clasohm@0
   111
val left_inverse_lemma = result();
clasohm@0
   112
clasohm@0
   113
val prems = goal Perm.thy
clasohm@0
   114
    "[| f: inj(A,B);  a: A |] ==> converse(f)`(f`a) = a";
clasohm@0
   115
by (fast_tac (ZF_cs addIs (prems@
clasohm@0
   116
       [left_inverse_lemma,inj_converse_fun,inj_is_fun])) 1);
clasohm@0
   117
val left_inverse = result();
clasohm@0
   118
clasohm@0
   119
val prems = goal Perm.thy
clasohm@0
   120
    "[| f: A->B;  converse(f): C->A;  b: C |] ==> f`(converse(f)`b) = b";
clasohm@0
   121
by (rtac (apply_Pair RS (converseD RS apply_equality)) 1);
clasohm@0
   122
by (REPEAT (resolve_tac prems 1));
clasohm@0
   123
val right_inverse_lemma = result();
clasohm@0
   124
clasohm@0
   125
val prems = goal Perm.thy
clasohm@0
   126
    "[| f: inj(A,B);  b: range(f) |] ==> f`(converse(f)`b) = b";
clasohm@0
   127
by (rtac right_inverse_lemma 1);
clasohm@0
   128
by (REPEAT (resolve_tac (prems@ [inj_converse_fun,inj_is_fun]) 1));
clasohm@0
   129
val right_inverse = result();
clasohm@0
   130
clasohm@0
   131
val prems = goal Perm.thy
clasohm@0
   132
    "f: inj(A,B) ==> converse(f): inj(range(f), A)";
clasohm@0
   133
bw inj_def;  (*rewrite subgoal but not prems!!*)
clasohm@0
   134
by (cut_facts_tac prems 1);
clasohm@0
   135
by (safe_tac ZF_cs);
clasohm@0
   136
(*apply f to both sides and simplify using right_inverse
clasohm@0
   137
  -- could also use  etac[subst_context RS box_equals]  in this proof *)
clasohm@0
   138
by (rtac simp_equals 2);
clasohm@0
   139
by (REPEAT (eresolve_tac [inj_converse_fun, right_inverse RS sym, ssubst] 1
clasohm@0
   140
     ORELSE ares_tac [refl,rangeI] 1));
clasohm@0
   141
val inj_converse_inj = result();
clasohm@0
   142
clasohm@0
   143
goalw Perm.thy [bij_def] "!!f A B. f: bij(A,B) ==> converse(f): bij(B,A)";
clasohm@0
   144
by (etac IntE 1);
clasohm@0
   145
by (eresolve_tac [(surj_range RS subst)] 1);
clasohm@0
   146
by (rtac IntI 1);
clasohm@0
   147
by (etac inj_converse_inj 1);
clasohm@0
   148
by (etac inj_converse_surj 1);
clasohm@0
   149
val bij_converse_bij = result();
clasohm@0
   150
clasohm@0
   151
clasohm@0
   152
(** Composition of two relations **)
clasohm@0
   153
clasohm@0
   154
(*The inductive definition package could derive these theorems for R o S*)
clasohm@0
   155
clasohm@0
   156
goalw Perm.thy [comp_def] "!!r s. [| <a,b>:s; <b,c>:r |] ==> <a,c> : r O s";
clasohm@0
   157
by (fast_tac ZF_cs 1);
clasohm@0
   158
val compI = result();
clasohm@0
   159
clasohm@0
   160
val prems = goalw Perm.thy [comp_def]
clasohm@0
   161
    "[| xz : r O s;  \
clasohm@0
   162
\       !!x y z. [| xz=<x,z>;  <x,y>:s;  <y,z>:r |] ==> P \
clasohm@0
   163
\    |] ==> P";
clasohm@0
   164
by (cut_facts_tac prems 1);
clasohm@0
   165
by (REPEAT (eresolve_tac [CollectE, exE, conjE] 1 ORELSE ares_tac prems 1));
clasohm@0
   166
val compE = result();
clasohm@0
   167
clasohm@0
   168
val compEpair = 
clasohm@0
   169
    rule_by_tactic (REPEAT_FIRST (etac Pair_inject ORELSE' bound_hyp_subst_tac)
clasohm@0
   170
		    THEN prune_params_tac)
clasohm@0
   171
	(read_instantiate [("xz","<a,c>")] compE);
clasohm@0
   172
clasohm@0
   173
val comp_cs = ZF_cs addIs [compI,idI] addSEs [compE,idE];
clasohm@0
   174
clasohm@0
   175
(** Domain and Range -- see Suppes, section 3.1 **)
clasohm@0
   176
clasohm@0
   177
(*Boyer et al., Set Theory in First-Order Logic, JAR 2 (1986), 287-327*)
clasohm@0
   178
goal Perm.thy "range(r O s) <= range(r)";
clasohm@0
   179
by (fast_tac comp_cs 1);
clasohm@0
   180
val range_comp = result();
clasohm@0
   181
clasohm@0
   182
goal Perm.thy "!!r s. domain(r) <= range(s) ==> range(r O s) = range(r)";
clasohm@0
   183
by (rtac (range_comp RS equalityI) 1);
clasohm@0
   184
by (fast_tac comp_cs 1);
clasohm@0
   185
val range_comp_eq = result();
clasohm@0
   186
clasohm@0
   187
goal Perm.thy "domain(r O s) <= domain(s)";
clasohm@0
   188
by (fast_tac comp_cs 1);
clasohm@0
   189
val domain_comp = result();
clasohm@0
   190
clasohm@0
   191
goal Perm.thy "!!r s. range(s) <= domain(r) ==> domain(r O s) = domain(s)";
clasohm@0
   192
by (rtac (domain_comp RS equalityI) 1);
clasohm@0
   193
by (fast_tac comp_cs 1);
clasohm@0
   194
val domain_comp_eq = result();
clasohm@0
   195
clasohm@0
   196
(** Other results **)
clasohm@0
   197
clasohm@0
   198
goal Perm.thy "!!r s. [| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)";
clasohm@0
   199
by (fast_tac comp_cs 1);
clasohm@0
   200
val comp_mono = result();
clasohm@0
   201
clasohm@0
   202
(*composition preserves relations*)
clasohm@0
   203
goal Perm.thy "!!r s. [| s<=A*B;  r<=B*C |] ==> (r O s) <= A*C";
clasohm@0
   204
by (fast_tac comp_cs 1);
clasohm@0
   205
val comp_rel = result();
clasohm@0
   206
clasohm@0
   207
(*associative law for composition*)
clasohm@0
   208
goal Perm.thy "(r O s) O t = r O (s O t)";
clasohm@0
   209
by (fast_tac (comp_cs addIs [equalityI]) 1);
clasohm@0
   210
val comp_assoc = result();
clasohm@0
   211
clasohm@0
   212
(*left identity of composition; provable inclusions are
clasohm@0
   213
        id(A) O r <= r       
clasohm@0
   214
  and   [| r<=A*B; B<=C |] ==> r <= id(C) O r *)
clasohm@0
   215
goal Perm.thy "!!r A B. r<=A*B ==> id(B) O r = r";
clasohm@0
   216
by (fast_tac (comp_cs addIs [equalityI]) 1);
clasohm@0
   217
val left_comp_id = result();
clasohm@0
   218
clasohm@0
   219
(*right identity of composition; provable inclusions are
clasohm@0
   220
        r O id(A) <= r
clasohm@0
   221
  and   [| r<=A*B; A<=C |] ==> r <= r O id(C) *)
clasohm@0
   222
goal Perm.thy "!!r A B. r<=A*B ==> r O id(A) = r";
clasohm@0
   223
by (fast_tac (comp_cs addIs [equalityI]) 1);
clasohm@0
   224
val right_comp_id = result();
clasohm@0
   225
clasohm@0
   226
clasohm@0
   227
(** Composition preserves functions, injections, and surjections **)
clasohm@0
   228
clasohm@0
   229
goal Perm.thy "!!f g. [| g: A->B;  f: B->C |] ==> (f O g) : A->C";
clasohm@0
   230
by (REPEAT (ares_tac [PiI,comp_rel,ex1I,compI] 1
clasohm@0
   231
     ORELSE eresolve_tac [fun_is_rel,apply_Pair,apply_type] 1));
clasohm@0
   232
by (fast_tac (comp_cs addDs [apply_equality]) 1);
clasohm@0
   233
val comp_func = result();
clasohm@0
   234
clasohm@0
   235
goal Perm.thy "!!f g. [| g: A->B;  f: B->C;  a:A |] ==> (f O g)`a = f`(g`a)";
clasohm@0
   236
by (REPEAT (ares_tac [comp_func,apply_equality,compI,
clasohm@0
   237
		      apply_Pair,apply_type] 1));
clasohm@0
   238
val comp_func_apply = result();
clasohm@0
   239
clasohm@0
   240
goalw Perm.thy [inj_def]
clasohm@0
   241
    "!!f g. [| g: inj(A,B);  f: inj(B,C) |] ==> (f O g) : inj(A,C)";
clasohm@0
   242
by (REPEAT (eresolve_tac [bspec RS bspec RS mp, box_equals] 1
clasohm@0
   243
     ORELSE step_tac (ZF_cs addSIs [comp_func,apply_type,comp_func_apply]) 1));
clasohm@0
   244
val comp_inj = result();
clasohm@0
   245
clasohm@0
   246
goalw Perm.thy [surj_def]
clasohm@0
   247
    "!!f g. [| g: surj(A,B);  f: surj(B,C) |] ==> (f O g) : surj(A,C)";
clasohm@0
   248
by (best_tac (ZF_cs addSIs [comp_func,comp_func_apply]) 1);
clasohm@0
   249
val comp_surj = result();
clasohm@0
   250
clasohm@0
   251
goalw Perm.thy [bij_def]
clasohm@0
   252
    "!!f g. [| g: bij(A,B);  f: bij(B,C) |] ==> (f O g) : bij(A,C)";
clasohm@0
   253
by (fast_tac (ZF_cs addIs [comp_inj,comp_surj]) 1);
clasohm@0
   254
val comp_bij = result();
clasohm@0
   255
clasohm@0
   256
clasohm@0
   257
(** Dual properties of inj and surj -- useful for proofs from
clasohm@0
   258
    D Pastre.  Automatic theorem proving in set theory. 
clasohm@0
   259
    Artificial Intelligence, 10:1--27, 1978. **)
clasohm@0
   260
clasohm@0
   261
goalw Perm.thy [inj_def]
clasohm@0
   262
    "!!f g. [| (f O g): inj(A,C);  g: A->B;  f: B->C |] ==> g: inj(A,B)";
clasohm@0
   263
by (safe_tac comp_cs);
clasohm@0
   264
by (REPEAT (eresolve_tac [asm_rl, bspec RS bspec RS mp] 1));
clasohm@0
   265
by (ASM_SIMP_TAC (ZF_ss addrews [comp_func_apply]) 1);
clasohm@0
   266
val comp_mem_injD1 = result();
clasohm@0
   267
clasohm@0
   268
goalw Perm.thy [inj_def,surj_def]
clasohm@0
   269
    "!!f g. [| (f O g): inj(A,C);  g: surj(A,B);  f: B->C |] ==> f: inj(B,C)";
clasohm@0
   270
by (safe_tac comp_cs);
clasohm@0
   271
by (res_inst_tac [("x1", "x")] (bspec RS bexE) 1);
clasohm@0
   272
by (eres_inst_tac [("x1", "w")] (bspec RS bexE) 3);
clasohm@0
   273
by (REPEAT (assume_tac 1));
clasohm@0
   274
by (safe_tac (comp_cs addSIs ZF_congs));
clasohm@0
   275
by (REPEAT (eresolve_tac [asm_rl, bspec RS bspec RS mp] 1));
clasohm@0
   276
by (ASM_SIMP_TAC (ZF_ss addrews [comp_func_apply]) 1);
clasohm@0
   277
val comp_mem_injD2 = result();
clasohm@0
   278
clasohm@0
   279
goalw Perm.thy [surj_def]
clasohm@0
   280
    "!!f g. [| (f O g): surj(A,C);  g: A->B;  f: B->C |] ==> f: surj(B,C)";
clasohm@0
   281
by (fast_tac (comp_cs addSIs [comp_func_apply RS sym, apply_type]) 1);
clasohm@0
   282
val comp_mem_surjD1 = result();
clasohm@0
   283
clasohm@0
   284
goal Perm.thy
clasohm@0
   285
    "!!f g. [| (f O g)`a = c;  g: A->B;  f: B->C;  a:A |] ==> f`(g`a) = c";
clasohm@0
   286
by (REPEAT (ares_tac [comp_func_apply RS sym RS trans] 1));
clasohm@0
   287
val comp_func_applyD = result();
clasohm@0
   288
clasohm@0
   289
goalw Perm.thy [inj_def,surj_def]
clasohm@0
   290
    "!!f g. [| (f O g): surj(A,C);  g: A->B;  f: inj(B,C) |] ==> g: surj(A,B)";
clasohm@0
   291
by (safe_tac comp_cs);
clasohm@0
   292
by (eres_inst_tac [("x1", "f`y")] (bspec RS bexE) 1);
clasohm@0
   293
by (REPEAT (ares_tac [apply_type] 1 ORELSE dtac comp_func_applyD 1));
clasohm@0
   294
by (best_tac (comp_cs addSIs [apply_type]) 1);
clasohm@0
   295
val comp_mem_surjD2 = result();
clasohm@0
   296
clasohm@0
   297
clasohm@0
   298
(** inverses of composition **)
clasohm@0
   299
clasohm@0
   300
(*left inverse of composition; one inclusion is
clasohm@0
   301
        f: A->B ==> id(A) <= converse(f) O f *)
clasohm@0
   302
val [prem] = goal Perm.thy
clasohm@0
   303
    "f: inj(A,B) ==> converse(f) O f = id(A)";
clasohm@0
   304
val injfD = prem RSN (3,inj_equality);
clasohm@0
   305
by (cut_facts_tac [prem RS inj_is_fun] 1);
clasohm@0
   306
by (fast_tac (comp_cs addIs [equalityI,apply_Pair] 
clasohm@0
   307
		      addEs [domain_type, make_elim injfD]) 1);
clasohm@0
   308
val left_comp_inverse = result();
clasohm@0
   309
clasohm@0
   310
(*right inverse of composition; one inclusion is
clasohm@0
   311
        f: A->B ==> f O converse(f) <= id(B) *)
clasohm@0
   312
val [prem] = goalw Perm.thy [surj_def]
clasohm@0
   313
    "f: surj(A,B) ==> f O converse(f) = id(B)";
clasohm@0
   314
val appfD = (prem RS CollectD1) RSN (3,apply_equality2);
clasohm@0
   315
by (cut_facts_tac [prem] 1);
clasohm@0
   316
by (rtac equalityI 1);
clasohm@0
   317
by (best_tac (comp_cs addEs [domain_type, range_type, make_elim appfD]) 1);
clasohm@0
   318
by (best_tac (comp_cs addIs [apply_Pair]) 1);
clasohm@0
   319
val right_comp_inverse = result();
clasohm@0
   320
clasohm@0
   321
(*Injective case applies converse(f) to both sides then simplifies
clasohm@0
   322
    using left_inverse_lemma*)
clasohm@0
   323
goalw Perm.thy [bij_def,inj_def,surj_def]
clasohm@0
   324
    "!!f A B. [| converse(f): B->A;  f: A->B |] ==> f : bij(A,B)";
clasohm@0
   325
val cf_cong = read_instantiate_sg (sign_of Perm.thy)
clasohm@0
   326
                [("t","%x.?f`x")]   subst_context;
clasohm@0
   327
by (fast_tac (ZF_cs addIs [left_inverse_lemma, right_inverse_lemma, apply_type]
clasohm@0
   328
		    addEs [cf_cong RS box_equals]) 1);
clasohm@0
   329
val invertible_imp_bijective = result();
clasohm@0
   330
clasohm@0
   331
(** Unions of functions -- cf similar theorems on func.ML **)
clasohm@0
   332
clasohm@0
   333
goal Perm.thy "converse(r Un s) = converse(r) Un converse(s)";
clasohm@0
   334
by (rtac equalityI 1);
clasohm@0
   335
by (DEPTH_SOLVE_1 
clasohm@0
   336
      (resolve_tac [Un_least,converse_mono, Un_upper1,Un_upper2] 2));
clasohm@0
   337
by (fast_tac ZF_cs 1);
clasohm@0
   338
val converse_of_Un = result();
clasohm@0
   339
clasohm@0
   340
goalw Perm.thy [surj_def]
clasohm@0
   341
    "!!f g. [| f: surj(A,B);  g: surj(C,D);  A Int C = 0 |] ==> \
clasohm@0
   342
\           (f Un g) : surj(A Un C, B Un D)";
clasohm@0
   343
by (DEPTH_SOLVE_1 (eresolve_tac [fun_disjoint_apply1, fun_disjoint_apply2] 1
clasohm@0
   344
	    ORELSE ball_tac 1
clasohm@0
   345
	    ORELSE (rtac trans 1 THEN atac 2)
clasohm@0
   346
	    ORELSE step_tac (ZF_cs addIs [fun_disjoint_Un]) 1));
clasohm@0
   347
val surj_disjoint_Un = result();
clasohm@0
   348
clasohm@0
   349
(*A simple, high-level proof; the version for injections follows from it,
clasohm@0
   350
  using  f:inj(A,B)<->f:bij(A,range(f))  *)
clasohm@0
   351
goal Perm.thy
clasohm@0
   352
    "!!f g. [| f: bij(A,B);  g: bij(C,D);  A Int C = 0;  B Int D = 0 |] ==> \
clasohm@0
   353
\           (f Un g) : bij(A Un C, B Un D)";
clasohm@0
   354
by (rtac invertible_imp_bijective 1);
clasohm@0
   355
by (rtac (converse_of_Un RS ssubst) 1);
clasohm@0
   356
by (REPEAT (ares_tac [fun_disjoint_Un, bij_is_fun, bij_converse_bij] 1));
clasohm@0
   357
val bij_disjoint_Un = result();
clasohm@0
   358
clasohm@0
   359
clasohm@0
   360
(** Restrictions as surjections and bijections *)
clasohm@0
   361
clasohm@0
   362
val prems = goalw Perm.thy [surj_def]
clasohm@0
   363
    "f: Pi(A,B) ==> f: surj(A, f``A)";
clasohm@0
   364
val rls = apply_equality :: (prems RL [apply_Pair,Pi_type]);
clasohm@0
   365
by (fast_tac (ZF_cs addIs rls) 1);
clasohm@0
   366
val surj_image = result();
clasohm@0
   367
clasohm@0
   368
goal Perm.thy 
clasohm@0
   369
    "!!f. [| f: Pi(C,B);  A<=C |] ==> restrict(f,A)``A = f``A";
clasohm@0
   370
by (rtac equalityI 1);
clasohm@0
   371
by (SELECT_GOAL (rewtac restrict_def) 2);
clasohm@0
   372
by (REPEAT (eresolve_tac [imageE, apply_equality RS subst] 2
clasohm@0
   373
     ORELSE ares_tac [subsetI,lamI,imageI] 2));
clasohm@0
   374
by (REPEAT (ares_tac [image_mono,restrict_subset,subset_refl] 1));
clasohm@0
   375
val restrict_image = result();
clasohm@0
   376
clasohm@0
   377
goalw Perm.thy [inj_def]
clasohm@0
   378
    "!!f. [| f: inj(A,B);  C<=A |] ==> restrict(f,C): inj(C,B)";
clasohm@0
   379
by (safe_tac (ZF_cs addSEs [restrict_type2]));
clasohm@0
   380
by (REPEAT (eresolve_tac [asm_rl, bspec RS bspec RS mp, subsetD,
clasohm@0
   381
                          box_equals, restrict] 1));
clasohm@0
   382
val restrict_inj = result();
clasohm@0
   383
clasohm@0
   384
val prems = goal Perm.thy 
clasohm@0
   385
    "[| f: Pi(A,B);  C<=A |] ==> restrict(f,C): surj(C, f``C)";
clasohm@0
   386
by (rtac (restrict_image RS subst) 1);
clasohm@0
   387
by (rtac (restrict_type2 RS surj_image) 3);
clasohm@0
   388
by (REPEAT (resolve_tac prems 1));
clasohm@0
   389
val restrict_surj = result();
clasohm@0
   390
clasohm@0
   391
goalw Perm.thy [inj_def,bij_def]
clasohm@0
   392
    "!!f. [| f: inj(A,B);  C<=A |] ==> restrict(f,C): bij(C, f``C)";
clasohm@0
   393
by (safe_tac ZF_cs);
clasohm@0
   394
by (REPEAT (eresolve_tac [bspec RS bspec RS mp, subsetD,
clasohm@0
   395
                          box_equals, restrict] 1
clasohm@0
   396
     ORELSE ares_tac [surj_is_fun,restrict_surj] 1));
clasohm@0
   397
val restrict_bij = result();
clasohm@0
   398
clasohm@0
   399
clasohm@0
   400
(*** Lemmas for Ramsey's Theorem ***)
clasohm@0
   401
clasohm@0
   402
goalw Perm.thy [inj_def] "!!f. [| f: inj(A,B);  B<=D |] ==> f: inj(A,D)";
clasohm@0
   403
by (fast_tac (ZF_cs addSEs [fun_weaken_type]) 1);
clasohm@0
   404
val inj_weaken_type = result();
clasohm@0
   405
clasohm@0
   406
val [major] = goal Perm.thy  
clasohm@0
   407
    "[| f: inj(succ(m), A) |] ==> restrict(f,m) : inj(m, A-{f`m})";
clasohm@0
   408
by (rtac (major RS restrict_bij RS bij_is_inj RS inj_weaken_type) 1);
clasohm@0
   409
by (fast_tac ZF_cs 1);
clasohm@0
   410
by (cut_facts_tac [major] 1);
clasohm@0
   411
by (rewtac inj_def);
clasohm@0
   412
by (safe_tac ZF_cs);
clasohm@0
   413
by (etac range_type 1);
clasohm@0
   414
by (assume_tac 1);
clasohm@0
   415
by (dtac apply_equality 1);
clasohm@0
   416
by (assume_tac 1);
clasohm@0
   417
by (res_inst_tac [("a","m")] mem_anti_refl 1);
clasohm@0
   418
by (fast_tac ZF_cs 1);
clasohm@0
   419
val inj_succ_restrict = result();
clasohm@0
   420
clasohm@0
   421
goalw Perm.thy [inj_def]
clasohm@0
   422
    "!!f. [| f: inj(A,B);  ~ a:A;  ~ b:B |]  ==> \
clasohm@0
   423
\         cons(<a,b>,f) : inj(cons(a,A), cons(b,B))";
clasohm@0
   424
(*cannot use safe_tac: must preserve the implication*)
clasohm@0
   425
by (etac CollectE 1);
clasohm@0
   426
by (rtac CollectI 1);
clasohm@0
   427
by (etac fun_extend 1);
clasohm@0
   428
by (REPEAT (ares_tac [ballI] 1));
clasohm@0
   429
by (REPEAT_FIRST (eresolve_tac [consE,ssubst]));
clasohm@0
   430
(*Assumption ALL w:A. ALL x:A. f`w = f`x --> w=x makes ASM_SIMP_TAC loop!*)
clasohm@0
   431
by (ALLGOALS (SIMP_TAC (ZF_ss addrews [fun_extend_apply2,fun_extend_apply1])));
clasohm@0
   432
by (ALLGOALS (fast_tac (ZF_cs addIs [apply_type])));
clasohm@0
   433
val inj_extend = result();