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