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