src/ZF/perm.ML
author wenzelm
Sat, 15 Apr 2000 15:00:57 +0200
changeset 8717 20c42415c07d
parent 218 be834b9a0c72
permissions -rw-r--r--
plain ASCII;
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
218
be834b9a0c72 ZF/perm/image_comp: new
lcp
parents: 37
diff changeset
   197
goal Perm.thy "(r O s)``A = r``(s``A)";
be834b9a0c72 ZF/perm/image_comp: new
lcp
parents: 37
diff changeset
   198
by (fast_tac (comp_cs addIs [equalityI]) 1);
be834b9a0c72 ZF/perm/image_comp: new
lcp
parents: 37
diff changeset
   199
val image_comp = result();
be834b9a0c72 ZF/perm/image_comp: new
lcp
parents: 37
diff changeset
   200
be834b9a0c72 ZF/perm/image_comp: new
lcp
parents: 37
diff changeset
   201
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   202
(** Other results **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   203
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   204
goal Perm.thy "!!r s. [| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   205
by (fast_tac comp_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   206
val comp_mono = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   207
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   208
(*composition preserves relations*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   209
goal Perm.thy "!!r s. [| s<=A*B;  r<=B*C |] ==> (r O s) <= A*C";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   210
by (fast_tac comp_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   211
val comp_rel = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   212
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   213
(*associative law for composition*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   214
goal Perm.thy "(r O s) O t = r O (s O t)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   215
by (fast_tac (comp_cs addIs [equalityI]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   216
val comp_assoc = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   217
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   218
(*left identity of composition; provable inclusions are
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   219
        id(A) O r <= r       
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   220
  and   [| r<=A*B; B<=C |] ==> r <= id(C) O r *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   221
goal Perm.thy "!!r A B. r<=A*B ==> id(B) O r = r";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   222
by (fast_tac (comp_cs addIs [equalityI]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   223
val left_comp_id = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   224
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   225
(*right identity of composition; provable inclusions are
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   226
        r O id(A) <= r
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   227
  and   [| r<=A*B; A<=C |] ==> r <= r O id(C) *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   228
goal Perm.thy "!!r A B. r<=A*B ==> r O id(A) = r";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   229
by (fast_tac (comp_cs addIs [equalityI]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   230
val right_comp_id = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   231
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   232
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   233
(** Composition preserves functions, injections, and surjections **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   234
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   235
goal Perm.thy "!!f g. [| g: A->B;  f: B->C |] ==> (f O g) : A->C";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   236
by (REPEAT (ares_tac [PiI,comp_rel,ex1I,compI] 1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   237
     ORELSE eresolve_tac [fun_is_rel,apply_Pair,apply_type] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   238
by (fast_tac (comp_cs addDs [apply_equality]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   239
val comp_func = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   240
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   241
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
   242
by (REPEAT (ares_tac [comp_func,apply_equality,compI,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   243
		      apply_Pair,apply_type] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   244
val comp_func_apply = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   245
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   246
goalw Perm.thy [inj_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   247
    "!!f g. [| g: inj(A,B);  f: inj(B,C) |] ==> (f O g) : inj(A,C)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   248
by (REPEAT (eresolve_tac [bspec RS bspec RS mp, box_equals] 1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   249
     ORELSE step_tac (ZF_cs addSIs [comp_func,apply_type,comp_func_apply]) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   250
val comp_inj = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   251
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   252
goalw Perm.thy [surj_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   253
    "!!f g. [| g: surj(A,B);  f: surj(B,C) |] ==> (f O g) : surj(A,C)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   254
by (best_tac (ZF_cs addSIs [comp_func,comp_func_apply]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   255
val comp_surj = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   256
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   257
goalw Perm.thy [bij_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   258
    "!!f g. [| g: bij(A,B);  f: bij(B,C) |] ==> (f O g) : bij(A,C)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   259
by (fast_tac (ZF_cs addIs [comp_inj,comp_surj]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   260
val comp_bij = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   261
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   262
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   263
(** Dual properties of inj and surj -- useful for proofs from
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   264
    D Pastre.  Automatic theorem proving in set theory. 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   265
    Artificial Intelligence, 10:1--27, 1978. **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   266
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   267
goalw Perm.thy [inj_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   268
    "!!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
   269
by (safe_tac comp_cs);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   270
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
   271
by (asm_simp_tac (FOL_ss addsimps [comp_func_apply]) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   272
val comp_mem_injD1 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   273
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   274
goalw Perm.thy [inj_def,surj_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   275
    "!!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
   276
by (safe_tac comp_cs);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   277
by (res_inst_tac [("x1", "x")] (bspec RS bexE) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   278
by (eres_inst_tac [("x1", "w")] (bspec RS bexE) 3);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   279
by (REPEAT (assume_tac 1));
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   280
by (safe_tac comp_cs);
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   281
by (res_inst_tac [("t", "op `(g)")] subst_context 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   282
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
   283
by (asm_simp_tac (FOL_ss addsimps [comp_func_apply]) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   284
val comp_mem_injD2 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   285
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   286
goalw Perm.thy [surj_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   287
    "!!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
   288
by (fast_tac (comp_cs addSIs [comp_func_apply RS sym, apply_type]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   289
val comp_mem_surjD1 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   290
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   291
goal Perm.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   292
    "!!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
   293
by (REPEAT (ares_tac [comp_func_apply RS sym RS trans] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   294
val comp_func_applyD = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   295
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   296
goalw Perm.thy [inj_def,surj_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   297
    "!!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
   298
by (safe_tac comp_cs);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   299
by (eres_inst_tac [("x1", "f`y")] (bspec RS bexE) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   300
by (REPEAT (ares_tac [apply_type] 1 ORELSE dtac comp_func_applyD 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   301
by (best_tac (comp_cs addSIs [apply_type]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   302
val comp_mem_surjD2 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   303
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   304
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   305
(** inverses of composition **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   306
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   307
(*left inverse of composition; one inclusion is
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   308
        f: A->B ==> id(A) <= converse(f) O f *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   309
val [prem] = goal Perm.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   310
    "f: inj(A,B) ==> converse(f) O f = id(A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   311
val injfD = prem RSN (3,inj_equality);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   312
by (cut_facts_tac [prem RS inj_is_fun] 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   313
by (fast_tac (comp_cs addIs [equalityI,apply_Pair] 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   314
		      addEs [domain_type, make_elim injfD]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   315
val left_comp_inverse = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   316
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   317
(*right inverse of composition; one inclusion is
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   318
        f: A->B ==> f O converse(f) <= id(B) *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   319
val [prem] = goalw Perm.thy [surj_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   320
    "f: surj(A,B) ==> f O converse(f) = id(B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   321
val appfD = (prem RS CollectD1) RSN (3,apply_equality2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   322
by (cut_facts_tac [prem] 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   323
by (rtac equalityI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   324
by (best_tac (comp_cs addEs [domain_type, range_type, make_elim appfD]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   325
by (best_tac (comp_cs addIs [apply_Pair]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   326
val right_comp_inverse = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   327
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   328
(*Injective case applies converse(f) to both sides then simplifies
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   329
    using left_inverse_lemma*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   330
goalw Perm.thy [bij_def,inj_def,surj_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   331
    "!!f A B. [| converse(f): B->A;  f: A->B |] ==> f : bij(A,B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   332
val cf_cong = read_instantiate_sg (sign_of Perm.thy)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   333
                [("t","%x.?f`x")]   subst_context;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   334
by (fast_tac (ZF_cs addIs [left_inverse_lemma, right_inverse_lemma, apply_type]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   335
		    addEs [cf_cong RS box_equals]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   336
val invertible_imp_bijective = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   337
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   338
(** Unions of functions -- cf similar theorems on func.ML **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   339
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   340
goal Perm.thy "converse(r Un s) = converse(r) Un converse(s)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   341
by (rtac equalityI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   342
by (DEPTH_SOLVE_1 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   343
      (resolve_tac [Un_least,converse_mono, Un_upper1,Un_upper2] 2));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   344
by (fast_tac ZF_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   345
val converse_of_Un = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   346
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   347
goalw Perm.thy [surj_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   348
    "!!f g. [| f: surj(A,B);  g: surj(C,D);  A Int C = 0 |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   349
\           (f Un g) : surj(A Un C, B Un D)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   350
by (DEPTH_SOLVE_1 (eresolve_tac [fun_disjoint_apply1, fun_disjoint_apply2] 1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   351
	    ORELSE ball_tac 1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   352
	    ORELSE (rtac trans 1 THEN atac 2)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   353
	    ORELSE step_tac (ZF_cs addIs [fun_disjoint_Un]) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   354
val surj_disjoint_Un = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   355
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   356
(*A simple, high-level proof; the version for injections follows from it,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   357
  using  f:inj(A,B)<->f:bij(A,range(f))  *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   358
goal Perm.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   359
    "!!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
   360
\           (f Un g) : bij(A Un C, B Un D)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   361
by (rtac invertible_imp_bijective 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   362
by (rtac (converse_of_Un RS ssubst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   363
by (REPEAT (ares_tac [fun_disjoint_Un, bij_is_fun, bij_converse_bij] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   364
val bij_disjoint_Un = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   365
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   366
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   367
(** Restrictions as surjections and bijections *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   368
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   369
val prems = goalw Perm.thy [surj_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   370
    "f: Pi(A,B) ==> f: surj(A, f``A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   371
val rls = apply_equality :: (prems RL [apply_Pair,Pi_type]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   372
by (fast_tac (ZF_cs addIs rls) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   373
val surj_image = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   374
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   375
goal Perm.thy 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   376
    "!!f. [| f: Pi(C,B);  A<=C |] ==> restrict(f,A)``A = f``A";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   377
by (rtac equalityI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   378
by (SELECT_GOAL (rewtac restrict_def) 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   379
by (REPEAT (eresolve_tac [imageE, apply_equality RS subst] 2
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   380
     ORELSE ares_tac [subsetI,lamI,imageI] 2));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   381
by (REPEAT (ares_tac [image_mono,restrict_subset,subset_refl] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   382
val restrict_image = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   383
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   384
goalw Perm.thy [inj_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   385
    "!!f. [| f: inj(A,B);  C<=A |] ==> restrict(f,C): inj(C,B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   386
by (safe_tac (ZF_cs addSEs [restrict_type2]));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   387
by (REPEAT (eresolve_tac [asm_rl, bspec RS bspec RS mp, subsetD,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   388
                          box_equals, restrict] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   389
val restrict_inj = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   390
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   391
val prems = goal Perm.thy 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   392
    "[| f: Pi(A,B);  C<=A |] ==> restrict(f,C): surj(C, f``C)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   393
by (rtac (restrict_image RS subst) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   394
by (rtac (restrict_type2 RS surj_image) 3);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   395
by (REPEAT (resolve_tac prems 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   396
val restrict_surj = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   397
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   398
goalw Perm.thy [inj_def,bij_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   399
    "!!f. [| f: inj(A,B);  C<=A |] ==> restrict(f,C): bij(C, f``C)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   400
by (safe_tac ZF_cs);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   401
by (REPEAT (eresolve_tac [bspec RS bspec RS mp, subsetD,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   402
                          box_equals, restrict] 1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   403
     ORELSE ares_tac [surj_is_fun,restrict_surj] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   404
val restrict_bij = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   405
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   406
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   407
(*** Lemmas for Ramsey's Theorem ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   408
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   409
goalw Perm.thy [inj_def] "!!f. [| f: inj(A,B);  B<=D |] ==> f: inj(A,D)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   410
by (fast_tac (ZF_cs addSEs [fun_weaken_type]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   411
val inj_weaken_type = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   412
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   413
val [major] = goal Perm.thy  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   414
    "[| f: inj(succ(m), A) |] ==> restrict(f,m) : inj(m, A-{f`m})";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   415
by (rtac (major RS restrict_bij RS bij_is_inj RS inj_weaken_type) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   416
by (fast_tac ZF_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   417
by (cut_facts_tac [major] 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   418
by (rewtac inj_def);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   419
by (safe_tac ZF_cs);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   420
by (etac range_type 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   421
by (assume_tac 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   422
by (dtac apply_equality 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   423
by (assume_tac 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   424
by (res_inst_tac [("a","m")] mem_anti_refl 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   425
by (fast_tac ZF_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   426
val inj_succ_restrict = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   427
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   428
goalw Perm.thy [inj_def]
37
cebe01deba80 added ~: for "not in"
lcp
parents: 6
diff changeset
   429
    "!!f. [| f: inj(A,B);  a~:A;  b~:B |]  ==> \
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   430
\         cons(<a,b>,f) : inj(cons(a,A), cons(b,B))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   431
(*cannot use safe_tac: must preserve the implication*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   432
by (etac CollectE 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   433
by (rtac CollectI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   434
by (etac fun_extend 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   435
by (REPEAT (ares_tac [ballI] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   436
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
   437
(*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
   438
  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
   439
by (ALLGOALS (asm_simp_tac 
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   440
	      (FOL_ss addsimps [fun_extend_apply2,fun_extend_apply1])));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   441
by (ALLGOALS (fast_tac (ZF_cs addIs [apply_type])));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   442
val inj_extend = result();