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