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