src/ZF/Perm.ML
author paulson
Mon Dec 28 16:59:28 1998 +0100 (1998-12-28)
changeset 6053 8a1059aa01f0
parent 5529 4a54acae6a15
child 6068 2d8f3e1f1151
permissions -rw-r--r--
new inductive, datatype and primrec packages, etc.
clasohm@1461
     1
(*  Title:      ZF/Perm.ML
clasohm@0
     2
    ID:         $Id$
clasohm@1461
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1991  University of Cambridge
clasohm@0
     5
lcp@735
     6
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
paulson@5137
    16
Goalw [surj_def] "f: surj(A,B) ==> f: A->B";
clasohm@0
    17
by (etac CollectD1 1);
clasohm@760
    18
qed "surj_is_fun";
clasohm@0
    19
paulson@5137
    20
Goalw [surj_def] "f : Pi(A,B) ==> f: surj(A,range(f))";
wenzelm@4091
    21
by (blast_tac (claset() addIs [apply_equality, range_of_fun, domain_type]) 1);
clasohm@760
    22
qed "fun_is_surj";
clasohm@0
    23
paulson@5137
    24
Goalw [surj_def] "f: surj(A,B) ==> range(f)=B";
wenzelm@4091
    25
by (best_tac (claset() addIs [apply_Pair] addEs [range_type]) 1);
clasohm@760
    26
qed "surj_range";
clasohm@0
    27
lcp@502
    28
(** A function with a right inverse is a surjection **)
lcp@502
    29
lcp@502
    30
val prems = goalw Perm.thy [surj_def]
lcp@502
    31
    "[| f: A->B;  !!y. y:B ==> d(y): A;  !!y. y:B ==> f`d(y) = y \
lcp@502
    32
\    |] ==> f: surj(A,B)";
wenzelm@4091
    33
by (blast_tac (claset() addIs prems) 1);
clasohm@760
    34
qed "f_imp_surjective";
lcp@502
    35
paulson@5321
    36
val prems = Goal
clasohm@1461
    37
    "[| !!x. x:A ==> c(x): B;           \
clasohm@1461
    38
\       !!y. y:B ==> d(y): A;           \
clasohm@1461
    39
\       !!y. y:B ==> c(d(y)) = y        \
wenzelm@3840
    40
\    |] ==> (lam x:A. c(x)) : surj(A,B)";
lcp@502
    41
by (res_inst_tac [("d", "d")] f_imp_surjective 1);
paulson@5529
    42
by (ALLGOALS (asm_simp_tac (simpset() addsimps [lam_type]@prems) ));
clasohm@760
    43
qed "lam_surjective";
lcp@502
    44
lcp@735
    45
(*Cantor's theorem revisited*)
wenzelm@5067
    46
Goalw [surj_def] "f ~: surj(A,Pow(A))";
paulson@4152
    47
by Safe_tac;
lcp@735
    48
by (cut_facts_tac [cantor] 1);
lcp@735
    49
by (fast_tac subset_cs 1);
clasohm@760
    50
qed "cantor_surj";
lcp@735
    51
clasohm@0
    52
clasohm@0
    53
(** Injective function space **)
clasohm@0
    54
paulson@5137
    55
Goalw [inj_def] "f: inj(A,B) ==> f: A->B";
clasohm@0
    56
by (etac CollectD1 1);
clasohm@760
    57
qed "inj_is_fun";
clasohm@0
    58
paulson@1787
    59
(*Good for dealing with sets of pairs, but a bit ugly in use [used in AC]*)
wenzelm@5067
    60
Goalw [inj_def]
paulson@5147
    61
    "[| <a,b>:f;  <c,b>:f;  f: inj(A,B) |] ==> a=c";
clasohm@0
    62
by (REPEAT (eresolve_tac [asm_rl, Pair_mem_PiE, CollectE] 1));
paulson@3016
    63
by (Blast_tac 1);
clasohm@760
    64
qed "inj_equality";
clasohm@0
    65
paulson@5137
    66
Goalw [inj_def] "[| f:inj(A,B);  a:A;  b:A;  f`a=f`b |] ==> a=b";
paulson@3016
    67
by (Blast_tac 1);
lcp@826
    68
val inj_apply_equality = result();
lcp@826
    69
lcp@484
    70
(** A function with a left inverse is an injection **)
lcp@484
    71
paulson@5137
    72
Goal "[| f: A->B;  ALL x:A. d(f`x)=x |] ==> f: inj(A,B)";
wenzelm@4091
    73
by (asm_simp_tac (simpset() addsimps [inj_def]) 1);
paulson@6053
    74
by (blast_tac (claset() addIs [subst_context RS box_equals]) 1);
paulson@1787
    75
bind_thm ("f_imp_injective", ballI RSN (2,result()));
lcp@484
    76
paulson@5321
    77
val prems = Goal
clasohm@1461
    78
    "[| !!x. x:A ==> c(x): B;           \
clasohm@1461
    79
\       !!x. x:A ==> d(c(x)) = x        \
wenzelm@3840
    80
\    |] ==> (lam x:A. c(x)) : inj(A,B)";
lcp@484
    81
by (res_inst_tac [("d", "d")] f_imp_injective 1);
paulson@5529
    82
by (ALLGOALS (asm_simp_tac (simpset() addsimps [lam_type]@prems)));
clasohm@760
    83
qed "lam_injective";
lcp@484
    84
lcp@484
    85
(** Bijections **)
clasohm@0
    86
paulson@5137
    87
Goalw [bij_def] "f: bij(A,B) ==> f: inj(A,B)";
clasohm@0
    88
by (etac IntD1 1);
clasohm@760
    89
qed "bij_is_inj";
clasohm@0
    90
paulson@5137
    91
Goalw [bij_def] "f: bij(A,B) ==> f: surj(A,B)";
clasohm@0
    92
by (etac IntD2 1);
clasohm@760
    93
qed "bij_is_surj";
clasohm@0
    94
clasohm@0
    95
(* f: bij(A,B) ==> f: A->B *)
clasohm@782
    96
bind_thm ("bij_is_fun", (bij_is_inj RS inj_is_fun));
clasohm@0
    97
lcp@502
    98
val prems = goalw Perm.thy [bij_def]
clasohm@1461
    99
    "[| !!x. x:A ==> c(x): B;           \
clasohm@1461
   100
\       !!y. y:B ==> d(y): A;           \
clasohm@1461
   101
\       !!x. x:A ==> d(c(x)) = x;       \
clasohm@1461
   102
\       !!y. y:B ==> c(d(y)) = y        \
wenzelm@3840
   103
\    |] ==> (lam x:A. c(x)) : bij(A,B)";
lcp@502
   104
by (REPEAT (ares_tac (prems @ [IntI, lam_injective, lam_surjective]) 1));
clasohm@760
   105
qed "lam_bijective";
lcp@502
   106
paulson@5284
   107
Goal "(ALL y : x. EX! y'. f(y') = f(y))  \
paulson@5284
   108
\     ==> (lam z:{f(y). y:x}. THE y. f(y) = z) : bij({f(y). y:x}, x)";
paulson@5284
   109
by (res_inst_tac [("d","f")] lam_bijective 1);
paulson@5284
   110
by (auto_tac (claset(),
paulson@5284
   111
	      simpset() addsimps [the_equality2]));
paulson@5284
   112
qed "RepFun_bijective";
paulson@5284
   113
lcp@6
   114
clasohm@0
   115
(** Identity function **)
clasohm@0
   116
clasohm@0
   117
val [prem] = goalw Perm.thy [id_def] "a:A ==> <a,a> : id(A)";  
clasohm@0
   118
by (rtac (prem RS lamI) 1);
clasohm@760
   119
qed "idI";
clasohm@0
   120
clasohm@0
   121
val major::prems = goalw Perm.thy [id_def]
clasohm@0
   122
    "[| p: id(A);  !!x.[| x:A; p=<x,x> |] ==> P  \
clasohm@0
   123
\    |] ==>  P";  
clasohm@0
   124
by (rtac (major RS lamE) 1);
clasohm@0
   125
by (REPEAT (ares_tac prems 1));
clasohm@760
   126
qed "idE";
clasohm@0
   127
wenzelm@5067
   128
Goalw [id_def] "id(A) : A->A";  
clasohm@0
   129
by (rtac lam_type 1);
clasohm@0
   130
by (assume_tac 1);
clasohm@760
   131
qed "id_type";
clasohm@0
   132
paulson@5137
   133
Goalw [id_def] "x:A ==> id(A)`x = x";
paulson@2469
   134
by (Asm_simp_tac 1);
paulson@2469
   135
qed "id_conv";
paulson@2469
   136
paulson@2469
   137
Addsimps [id_conv];
lcp@826
   138
clasohm@0
   139
val [prem] = goalw Perm.thy [id_def] "A<=B ==> id(A) <= id(B)";
clasohm@0
   140
by (rtac (prem RS lam_mono) 1);
clasohm@760
   141
qed "id_mono";
clasohm@0
   142
paulson@5143
   143
Goalw [inj_def,id_def] "A<=B ==> id(A): inj(A,B)";
clasohm@0
   144
by (REPEAT (ares_tac [CollectI,lam_type] 1));
lcp@435
   145
by (etac subsetD 1 THEN assume_tac 1);
paulson@2469
   146
by (Simp_tac 1);
clasohm@760
   147
qed "id_subset_inj";
lcp@435
   148
lcp@435
   149
val id_inj = subset_refl RS id_subset_inj;
clasohm@0
   150
wenzelm@5067
   151
Goalw [id_def,surj_def] "id(A): surj(A,A)";
wenzelm@4091
   152
by (blast_tac (claset() addIs [lam_type, beta]) 1);
clasohm@760
   153
qed "id_surj";
clasohm@0
   154
wenzelm@5067
   155
Goalw [bij_def] "id(A): bij(A,A)";
wenzelm@4091
   156
by (blast_tac (claset() addIs [id_inj, id_surj]) 1);
clasohm@760
   157
qed "id_bij";
clasohm@0
   158
wenzelm@5067
   159
Goalw [id_def] "A <= B <-> id(A) : A->B";
wenzelm@4091
   160
by (fast_tac (claset() addSIs [lam_type] addDs [apply_type] 
wenzelm@4091
   161
                      addss (simpset())) 1);
clasohm@760
   162
qed "subset_iff_id";
lcp@517
   163
clasohm@0
   164
lcp@502
   165
(*** Converse of a function ***)
clasohm@0
   166
paulson@5137
   167
Goalw [inj_def] "f: inj(A,B) ==> converse(f) : range(f)->A";
wenzelm@4091
   168
by (asm_simp_tac (simpset() addsimps [Pi_iff, function_def]) 1);
paulson@2033
   169
by (etac CollectE 1);
wenzelm@4091
   170
by (asm_simp_tac (simpset() addsimps [apply_iff]) 1);
wenzelm@4091
   171
by (blast_tac (claset() addDs [fun_is_rel]) 1);
clasohm@760
   172
qed "inj_converse_fun";
clasohm@0
   173
lcp@502
   174
(** Equations for converse(f) **)
clasohm@0
   175
clasohm@0
   176
(*The premises are equivalent to saying that f is injective...*) 
paulson@5268
   177
Goal "[| f: A->B;  converse(f): C->A;  a: A |] ==> converse(f)`(f`a) = a";
wenzelm@4091
   178
by (blast_tac (claset() addIs [apply_Pair, apply_equality, converseI]) 1);
clasohm@760
   179
qed "left_inverse_lemma";
clasohm@0
   180
paulson@5268
   181
Goal "[| f: inj(A,B);  a: A |] ==> converse(f)`(f`a) = a";
wenzelm@4091
   182
by (blast_tac (claset() addIs [left_inverse_lemma, inj_converse_fun,
paulson@3016
   183
			      inj_is_fun]) 1);
clasohm@760
   184
qed "left_inverse";
clasohm@0
   185
lcp@435
   186
val left_inverse_bij = bij_is_inj RS left_inverse;
lcp@435
   187
paulson@5321
   188
Goal "[| f: A->B;  converse(f): C->A;  b: C |] ==> f`(converse(f)`b) = b";
clasohm@0
   189
by (rtac (apply_Pair RS (converseD RS apply_equality)) 1);
paulson@5321
   190
by (REPEAT (assume_tac 1));
clasohm@760
   191
qed "right_inverse_lemma";
clasohm@0
   192
lcp@502
   193
(*Should the premises be f:surj(A,B), b:B for symmetry with left_inverse?
lcp@502
   194
  No: they would not imply that converse(f) was a function! *)
paulson@5137
   195
Goal "[| f: inj(A,B);  b: range(f) |] ==> f`(converse(f)`b) = b";
clasohm@0
   196
by (rtac right_inverse_lemma 1);
lcp@435
   197
by (REPEAT (ares_tac [inj_converse_fun,inj_is_fun] 1));
clasohm@760
   198
qed "right_inverse";
clasohm@0
   199
paulson@2469
   200
(*Cannot add [left_inverse, right_inverse] to default simpset: there are too
paulson@2469
   201
  many ways of expressing sufficient conditions.*)
paulson@2469
   202
paulson@5137
   203
Goal "[| f: bij(A,B);  b: B |] ==> f`(converse(f)`b) = b";
wenzelm@4091
   204
by (fast_tac (claset() addss
wenzelm@4091
   205
	      (simpset() addsimps [bij_def, right_inverse, surj_range])) 1);
clasohm@760
   206
qed "right_inverse_bij";
lcp@435
   207
lcp@502
   208
(** Converses of injections, surjections, bijections **)
lcp@502
   209
paulson@5137
   210
Goal "f: inj(A,B) ==> converse(f): inj(range(f), A)";
clasohm@1461
   211
by (rtac f_imp_injective 1);
clasohm@1461
   212
by (etac inj_converse_fun 1);
clasohm@1461
   213
by (rtac right_inverse 1);
lcp@502
   214
by (REPEAT (assume_tac 1));
clasohm@760
   215
qed "inj_converse_inj";
clasohm@0
   216
paulson@5137
   217
Goal "f: inj(A,B) ==> converse(f): surj(range(f), A)";
wenzelm@4091
   218
by (blast_tac (claset() addIs [f_imp_surjective, inj_converse_fun, left_inverse,
paulson@3016
   219
			      inj_is_fun, range_of_fun RS apply_type]) 1);
clasohm@760
   220
qed "inj_converse_surj";
lcp@502
   221
paulson@5137
   222
Goalw [bij_def] "f: bij(A,B) ==> converse(f): bij(B,A)";
wenzelm@4091
   223
by (fast_tac (claset() addEs [surj_range RS subst, inj_converse_inj,
paulson@3016
   224
			      inj_converse_surj]) 1);
clasohm@760
   225
qed "bij_converse_bij";
paulson@2469
   226
(*Adding this as an SI seems to cause looping*)
clasohm@0
   227
clasohm@0
   228
clasohm@0
   229
(** Composition of two relations **)
clasohm@0
   230
lcp@791
   231
(*The inductive definition package could derive these theorems for (r O s)*)
clasohm@0
   232
paulson@5137
   233
Goalw [comp_def] "[| <a,b>:s; <b,c>:r |] ==> <a,c> : r O s";
paulson@3016
   234
by (Blast_tac 1);
clasohm@760
   235
qed "compI";
clasohm@0
   236
clasohm@0
   237
val prems = goalw Perm.thy [comp_def]
clasohm@0
   238
    "[| xz : r O s;  \
clasohm@0
   239
\       !!x y z. [| xz=<x,z>;  <x,y>:s;  <y,z>:r |] ==> P \
clasohm@0
   240
\    |] ==> P";
clasohm@0
   241
by (cut_facts_tac prems 1);
clasohm@0
   242
by (REPEAT (eresolve_tac [CollectE, exE, conjE] 1 ORELSE ares_tac prems 1));
clasohm@760
   243
qed "compE";
clasohm@0
   244
paulson@2688
   245
bind_thm ("compEpair", 
clasohm@0
   246
    rule_by_tactic (REPEAT_FIRST (etac Pair_inject ORELSE' bound_hyp_subst_tac)
clasohm@1461
   247
                    THEN prune_params_tac)
paulson@2688
   248
        (read_instantiate [("xz","<a,c>")] compE));
clasohm@0
   249
paulson@2469
   250
AddSIs [idI];
paulson@2469
   251
AddIs  [compI];
paulson@2469
   252
AddSEs [compE,idE];
clasohm@0
   253
paulson@5202
   254
Goal "converse(R O S) = converse(S) O converse(R)";
paulson@5202
   255
by (Blast_tac 1);
paulson@5202
   256
qed "converse_comp";
paulson@5202
   257
paulson@5202
   258
clasohm@0
   259
(** Domain and Range -- see Suppes, section 3.1 **)
clasohm@0
   260
clasohm@0
   261
(*Boyer et al., Set Theory in First-Order Logic, JAR 2 (1986), 287-327*)
wenzelm@5067
   262
Goal "range(r O s) <= range(r)";
paulson@3016
   263
by (Blast_tac 1);
clasohm@760
   264
qed "range_comp";
clasohm@0
   265
paulson@5137
   266
Goal "domain(r) <= range(s) ==> range(r O s) = range(r)";
clasohm@0
   267
by (rtac (range_comp RS equalityI) 1);
paulson@3016
   268
by (Blast_tac 1);
clasohm@760
   269
qed "range_comp_eq";
clasohm@0
   270
wenzelm@5067
   271
Goal "domain(r O s) <= domain(s)";
paulson@3016
   272
by (Blast_tac 1);
clasohm@760
   273
qed "domain_comp";
clasohm@0
   274
paulson@5137
   275
Goal "range(s) <= domain(r) ==> domain(r O s) = domain(s)";
clasohm@0
   276
by (rtac (domain_comp RS equalityI) 1);
paulson@3016
   277
by (Blast_tac 1);
clasohm@760
   278
qed "domain_comp_eq";
clasohm@0
   279
wenzelm@5067
   280
Goal "(r O s)``A = r``(s``A)";
paulson@3016
   281
by (Blast_tac 1);
clasohm@760
   282
qed "image_comp";
lcp@218
   283
lcp@218
   284
clasohm@0
   285
(** Other results **)
clasohm@0
   286
paulson@5137
   287
Goal "[| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)";
paulson@3016
   288
by (Blast_tac 1);
clasohm@760
   289
qed "comp_mono";
clasohm@0
   290
clasohm@0
   291
(*composition preserves relations*)
paulson@5137
   292
Goal "[| s<=A*B;  r<=B*C |] ==> (r O s) <= A*C";
paulson@3016
   293
by (Blast_tac 1);
clasohm@760
   294
qed "comp_rel";
clasohm@0
   295
clasohm@0
   296
(*associative law for composition*)
wenzelm@5067
   297
Goal "(r O s) O t = r O (s O t)";
paulson@3016
   298
by (Blast_tac 1);
clasohm@760
   299
qed "comp_assoc";
clasohm@0
   300
clasohm@0
   301
(*left identity of composition; provable inclusions are
clasohm@0
   302
        id(A) O r <= r       
clasohm@0
   303
  and   [| r<=A*B; B<=C |] ==> r <= id(C) O r *)
paulson@5137
   304
Goal "r<=A*B ==> id(B) O r = r";
paulson@3016
   305
by (Blast_tac 1);
clasohm@760
   306
qed "left_comp_id";
clasohm@0
   307
clasohm@0
   308
(*right identity of composition; provable inclusions are
clasohm@0
   309
        r O id(A) <= r
clasohm@0
   310
  and   [| r<=A*B; A<=C |] ==> r <= r O id(C) *)
paulson@5137
   311
Goal "r<=A*B ==> r O id(A) = r";
paulson@3016
   312
by (Blast_tac 1);
clasohm@760
   313
qed "right_comp_id";
clasohm@0
   314
clasohm@0
   315
clasohm@0
   316
(** Composition preserves functions, injections, and surjections **)
clasohm@0
   317
wenzelm@5067
   318
Goalw [function_def]
paulson@5147
   319
    "[| function(g);  function(f) |] ==> function(f O g)";
paulson@3016
   320
by (Blast_tac 1);
clasohm@760
   321
qed "comp_function";
lcp@693
   322
paulson@5137
   323
Goal "[| g: A->B;  f: B->C |] ==> (f O g) : A->C";
paulson@1787
   324
by (asm_full_simp_tac
wenzelm@4091
   325
    (simpset() addsimps [Pi_def, comp_function, Pow_iff, comp_rel]
paulson@1787
   326
           setloop etac conjE) 1);
paulson@2033
   327
by (stac (range_rel_subset RS domain_comp_eq) 1 THEN assume_tac 2);
paulson@3016
   328
by (Blast_tac 1);
clasohm@760
   329
qed "comp_fun";
clasohm@0
   330
paulson@5137
   331
Goal "[| g: A->B;  f: B->C;  a:A |] ==> (f O g)`a = f`(g`a)";
lcp@435
   332
by (REPEAT (ares_tac [comp_fun,apply_equality,compI,
clasohm@1461
   333
                      apply_Pair,apply_type] 1));
clasohm@760
   334
qed "comp_fun_apply";
clasohm@0
   335
paulson@2469
   336
Addsimps [comp_fun_apply];
paulson@2469
   337
lcp@862
   338
(*Simplifies compositions of lambda-abstractions*)
paulson@5321
   339
val [prem] = Goal
clasohm@1461
   340
    "[| !!x. x:A ==> b(x): B    \
wenzelm@3840
   341
\    |] ==> (lam y:B. c(y)) O (lam x:A. b(x)) = (lam x:A. c(b(x)))";
clasohm@1461
   342
by (rtac fun_extension 1);
clasohm@1461
   343
by (rtac comp_fun 1);
clasohm@1461
   344
by (rtac lam_funtype 2);
lcp@862
   345
by (typechk_tac (prem::ZF_typechecks));
wenzelm@4091
   346
by (asm_simp_tac (simpset() 
oheimb@2637
   347
             setSolver type_auto_tac [lam_type, lam_funtype, prem]) 1);
lcp@862
   348
qed "comp_lam";
lcp@862
   349
paulson@5137
   350
Goal "[| g: inj(A,B);  f: inj(B,C) |] ==> (f O g) : inj(A,C)";
lcp@502
   351
by (res_inst_tac [("d", "%y. converse(g) ` (converse(f) ` y)")]
lcp@502
   352
    f_imp_injective 1);
lcp@502
   353
by (REPEAT (ares_tac [comp_fun, inj_is_fun] 1));
wenzelm@4091
   354
by (asm_simp_tac (simpset()  addsimps [left_inverse] 
oheimb@2637
   355
                        setSolver type_auto_tac [inj_is_fun, apply_type]) 1);
clasohm@760
   356
qed "comp_inj";
clasohm@0
   357
wenzelm@5067
   358
Goalw [surj_def]
paulson@5147
   359
    "[| g: surj(A,B);  f: surj(B,C) |] ==> (f O g) : surj(A,C)";
wenzelm@4091
   360
by (blast_tac (claset() addSIs [comp_fun,comp_fun_apply]) 1);
clasohm@760
   361
qed "comp_surj";
clasohm@0
   362
wenzelm@5067
   363
Goalw [bij_def]
paulson@5147
   364
    "[| g: bij(A,B);  f: bij(B,C) |] ==> (f O g) : bij(A,C)";
wenzelm@4091
   365
by (blast_tac (claset() addIs [comp_inj,comp_surj]) 1);
clasohm@760
   366
qed "comp_bij";
clasohm@0
   367
clasohm@0
   368
clasohm@0
   369
(** Dual properties of inj and surj -- useful for proofs from
clasohm@0
   370
    D Pastre.  Automatic theorem proving in set theory. 
clasohm@0
   371
    Artificial Intelligence, 10:1--27, 1978. **)
clasohm@0
   372
wenzelm@5067
   373
Goalw [inj_def]
paulson@5147
   374
    "[| (f O g): inj(A,C);  g: A->B;  f: B->C |] ==> g: inj(A,B)";
paulson@4152
   375
by Safe_tac;
clasohm@0
   376
by (REPEAT (eresolve_tac [asm_rl, bspec RS bspec RS mp] 1));
wenzelm@4091
   377
by (asm_simp_tac (simpset() ) 1);
clasohm@760
   378
qed "comp_mem_injD1";
clasohm@0
   379
wenzelm@5067
   380
Goalw [inj_def,surj_def]
paulson@5147
   381
    "[| (f O g): inj(A,C);  g: surj(A,B);  f: B->C |] ==> f: inj(B,C)";
paulson@4152
   382
by Safe_tac;
clasohm@0
   383
by (res_inst_tac [("x1", "x")] (bspec RS bexE) 1);
clasohm@0
   384
by (eres_inst_tac [("x1", "w")] (bspec RS bexE) 3);
clasohm@0
   385
by (REPEAT (assume_tac 1));
paulson@4152
   386
by Safe_tac;
lcp@6
   387
by (res_inst_tac [("t", "op `(g)")] subst_context 1);
clasohm@0
   388
by (REPEAT (eresolve_tac [asm_rl, bspec RS bspec RS mp] 1));
wenzelm@4091
   389
by (asm_simp_tac (simpset() ) 1);
clasohm@760
   390
qed "comp_mem_injD2";
clasohm@0
   391
wenzelm@5067
   392
Goalw [surj_def]
paulson@5147
   393
    "[| (f O g): surj(A,C);  g: A->B;  f: B->C |] ==> f: surj(B,C)";
wenzelm@4091
   394
by (blast_tac (claset() addSIs [comp_fun_apply RS sym, apply_funtype]) 1);
clasohm@760
   395
qed "comp_mem_surjD1";
clasohm@0
   396
paulson@5268
   397
Goal "[| (f O g)`a = c;  g: A->B;  f: B->C;  a:A |] ==> f`(g`a) = c";
lcp@435
   398
by (REPEAT (ares_tac [comp_fun_apply RS sym RS trans] 1));
clasohm@760
   399
qed "comp_fun_applyD";
clasohm@0
   400
wenzelm@5067
   401
Goalw [inj_def,surj_def]
paulson@5147
   402
    "[| (f O g): surj(A,C);  g: A->B;  f: inj(B,C) |] ==> g: surj(A,B)";
paulson@4152
   403
by Safe_tac;
clasohm@0
   404
by (eres_inst_tac [("x1", "f`y")] (bspec RS bexE) 1);
lcp@435
   405
by (REPEAT (ares_tac [apply_type] 1 ORELSE dtac comp_fun_applyD 1));
wenzelm@4091
   406
by (blast_tac (claset() addSIs [apply_funtype]) 1);
clasohm@760
   407
qed "comp_mem_surjD2";
clasohm@0
   408
clasohm@0
   409
clasohm@0
   410
(** inverses of composition **)
clasohm@0
   411
clasohm@0
   412
(*left inverse of composition; one inclusion is
clasohm@0
   413
        f: A->B ==> id(A) <= converse(f) O f *)
paulson@5137
   414
Goalw [inj_def] "f: inj(A,B) ==> converse(f) O f = id(A)";
wenzelm@4091
   415
by (fast_tac (claset() addIs [apply_Pair] 
paulson@1787
   416
                      addEs [domain_type]
wenzelm@4091
   417
               addss (simpset() addsimps [apply_iff])) 1);
clasohm@760
   418
qed "left_comp_inverse";
clasohm@0
   419
clasohm@0
   420
(*right inverse of composition; one inclusion is
clasohm@1461
   421
                f: A->B ==> f O converse(f) <= id(B) 
lcp@735
   422
*)
clasohm@0
   423
val [prem] = goalw Perm.thy [surj_def]
clasohm@0
   424
    "f: surj(A,B) ==> f O converse(f) = id(B)";
clasohm@0
   425
val appfD = (prem RS CollectD1) RSN (3,apply_equality2);
clasohm@0
   426
by (cut_facts_tac [prem] 1);
clasohm@0
   427
by (rtac equalityI 1);
wenzelm@4091
   428
by (best_tac (claset() addEs [domain_type, range_type, make_elim appfD]) 1);
wenzelm@4091
   429
by (blast_tac (claset() addIs [apply_Pair]) 1);
clasohm@760
   430
qed "right_comp_inverse";
clasohm@0
   431
lcp@435
   432
(** Proving that a function is a bijection **)
lcp@435
   433
wenzelm@5067
   434
Goalw [id_def]
paulson@5147
   435
    "[| f: A->B;  g: B->A |] ==> \
lcp@435
   436
\             f O g = id(B) <-> (ALL y:B. f`(g`y)=y)";
paulson@4152
   437
by Safe_tac;
wenzelm@3840
   438
by (dres_inst_tac [("t", "%h. h`y ")] subst_context 1);
paulson@2469
   439
by (Asm_full_simp_tac 1);
lcp@437
   440
by (rtac fun_extension 1);
lcp@435
   441
by (REPEAT (ares_tac [comp_fun, lam_type] 1));
paulson@4477
   442
by Auto_tac;
clasohm@760
   443
qed "comp_eq_id_iff";
lcp@435
   444
wenzelm@5067
   445
Goalw [bij_def]
paulson@5147
   446
    "[| f: A->B;  g: B->A;  f O g = id(B);  g O f = id(A) \
lcp@435
   447
\             |] ==> f : bij(A,B)";
wenzelm@4091
   448
by (asm_full_simp_tac (simpset() addsimps [comp_eq_id_iff]) 1);
lcp@502
   449
by (REPEAT (ares_tac [conjI, f_imp_injective, f_imp_surjective] 1
lcp@502
   450
       ORELSE eresolve_tac [bspec, apply_type] 1));
clasohm@760
   451
qed "fg_imp_bijective";
lcp@435
   452
paulson@5137
   453
Goal "[| f: A->A;  f O f = id(A) |] ==> f : bij(A,A)";
lcp@435
   454
by (REPEAT (ares_tac [fg_imp_bijective] 1));
clasohm@760
   455
qed "nilpotent_imp_bijective";
lcp@435
   456
paulson@5137
   457
Goal "[| converse(f): B->A;  f: A->B |] ==> f : bij(A,B)";
wenzelm@4091
   458
by (asm_simp_tac (simpset() addsimps [fg_imp_bijective, comp_eq_id_iff, 
clasohm@1461
   459
                                  left_inverse_lemma, right_inverse_lemma]) 1);
clasohm@760
   460
qed "invertible_imp_bijective";
clasohm@0
   461
clasohm@0
   462
(** Unions of functions -- cf similar theorems on func.ML **)
clasohm@0
   463
paulson@1709
   464
(*Theorem by KG, proof by LCP*)
paulson@5466
   465
Goal "[| f: inj(A,B);  g: inj(C,D);  B Int D = 0 |] \
paulson@5466
   466
\     ==> (lam a: A Un C. if(a:A, f`a, g`a)) : inj(A Un C, B Un D)";
paulson@1709
   467
by (res_inst_tac [("d","%z. if(z:B, converse(f)`z, converse(g)`z)")]
paulson@1709
   468
        lam_injective 1);
paulson@1709
   469
by (ALLGOALS 
wenzelm@4091
   470
    (asm_simp_tac (simpset() addsimps [inj_is_fun RS apply_type, left_inverse] 
paulson@5116
   471
                         setloop (split_tac [split_if] ORELSE' etac UnE))));
paulson@5466
   472
by (blast_tac (claset() addIs [inj_is_fun RS apply_type]) 1);
paulson@1709
   473
qed "inj_disjoint_Un";
paulson@1610
   474
wenzelm@5067
   475
Goalw [surj_def]
paulson@5147
   476
    "[| f: surj(A,B);  g: surj(C,D);  A Int C = 0 |] ==> \
clasohm@0
   477
\           (f Un g) : surj(A Un C, B Un D)";
wenzelm@4091
   478
by (blast_tac (claset() addIs [fun_disjoint_apply1, fun_disjoint_apply2,
paulson@3016
   479
			      fun_disjoint_Un, trans]) 1);
clasohm@760
   480
qed "surj_disjoint_Un";
clasohm@0
   481
clasohm@0
   482
(*A simple, high-level proof; the version for injections follows from it,
lcp@502
   483
  using  f:inj(A,B) <-> f:bij(A,range(f))  *)
paulson@5268
   484
Goal "[| f: bij(A,B);  g: bij(C,D);  A Int C = 0;  B Int D = 0 |] ==> \
clasohm@0
   485
\           (f Un g) : bij(A Un C, B Un D)";
clasohm@0
   486
by (rtac invertible_imp_bijective 1);
paulson@2033
   487
by (stac converse_Un 1);
clasohm@0
   488
by (REPEAT (ares_tac [fun_disjoint_Un, bij_is_fun, bij_converse_bij] 1));
clasohm@760
   489
qed "bij_disjoint_Un";
clasohm@0
   490
clasohm@0
   491
clasohm@0
   492
(** Restrictions as surjections and bijections *)
clasohm@0
   493
clasohm@0
   494
val prems = goalw Perm.thy [surj_def]
clasohm@0
   495
    "f: Pi(A,B) ==> f: surj(A, f``A)";
clasohm@0
   496
val rls = apply_equality :: (prems RL [apply_Pair,Pi_type]);
wenzelm@4091
   497
by (fast_tac (claset() addIs rls) 1);
clasohm@760
   498
qed "surj_image";
clasohm@0
   499
paulson@5137
   500
Goal "[| f: Pi(C,B);  A<=C |] ==> restrict(f,A)``A = f``A";
clasohm@0
   501
by (rtac equalityI 1);
clasohm@0
   502
by (SELECT_GOAL (rewtac restrict_def) 2);
clasohm@0
   503
by (REPEAT (eresolve_tac [imageE, apply_equality RS subst] 2
clasohm@0
   504
     ORELSE ares_tac [subsetI,lamI,imageI] 2));
clasohm@0
   505
by (REPEAT (ares_tac [image_mono,restrict_subset,subset_refl] 1));
clasohm@760
   506
qed "restrict_image";
clasohm@0
   507
wenzelm@5067
   508
Goalw [inj_def]
paulson@5147
   509
    "[| f: inj(A,B);  C<=A |] ==> restrict(f,C): inj(C,B)";
wenzelm@4091
   510
by (safe_tac (claset() addSEs [restrict_type2]));
clasohm@0
   511
by (REPEAT (eresolve_tac [asm_rl, bspec RS bspec RS mp, subsetD,
clasohm@0
   512
                          box_equals, restrict] 1));
clasohm@760
   513
qed "restrict_inj";
clasohm@0
   514
paulson@5321
   515
Goal "[| f: Pi(A,B);  C<=A |] ==> restrict(f,C): surj(C, f``C)";
clasohm@0
   516
by (rtac (restrict_image RS subst) 1);
clasohm@0
   517
by (rtac (restrict_type2 RS surj_image) 3);
paulson@5321
   518
by (REPEAT (assume_tac 1));
clasohm@760
   519
qed "restrict_surj";
clasohm@0
   520
wenzelm@5067
   521
Goalw [inj_def,bij_def]
paulson@5147
   522
    "[| f: inj(A,B);  C<=A |] ==> restrict(f,C): bij(C, f``C)";
wenzelm@4091
   523
by (blast_tac (claset() addSIs [restrict, restrict_surj]
paulson@3016
   524
		       addIs [box_equals, surj_is_fun]) 1);
clasohm@760
   525
qed "restrict_bij";
clasohm@0
   526
clasohm@0
   527
clasohm@0
   528
(*** Lemmas for Ramsey's Theorem ***)
clasohm@0
   529
paulson@5137
   530
Goalw [inj_def] "[| f: inj(A,B);  B<=D |] ==> f: inj(A,D)";
wenzelm@4091
   531
by (blast_tac (claset() addIs [fun_weaken_type]) 1);
clasohm@760
   532
qed "inj_weaken_type";
clasohm@0
   533
clasohm@0
   534
val [major] = goal Perm.thy  
clasohm@0
   535
    "[| f: inj(succ(m), A) |] ==> restrict(f,m) : inj(m, A-{f`m})";
clasohm@0
   536
by (rtac (major RS restrict_bij RS bij_is_inj RS inj_weaken_type) 1);
paulson@3016
   537
by (Blast_tac 1);
clasohm@0
   538
by (cut_facts_tac [major] 1);
clasohm@0
   539
by (rewtac inj_def);
wenzelm@4091
   540
by (fast_tac (claset() addEs [range_type, mem_irrefl] 
paulson@2469
   541
	              addDs [apply_equality]) 1);
clasohm@760
   542
qed "inj_succ_restrict";
clasohm@0
   543
wenzelm@5067
   544
Goalw [inj_def]
paulson@5147
   545
    "[| f: inj(A,B);  a~:A;  b~:B |]  ==> \
clasohm@0
   546
\         cons(<a,b>,f) : inj(cons(a,A), cons(b,B))";
oheimb@5525
   547
by (force_tac (claset() addIs [apply_type],
oheimb@5525
   548
               simpset() addsimps [fun_extend, fun_extend_apply2,
oheimb@5525
   549
						fun_extend_apply1]) 1);
clasohm@760
   550
qed "inj_extend";
paulson@1787
   551