author | obua |
Thu, 16 Feb 2006 04:17:19 +0100 | |
changeset 19067 | c0321d7d6b3d |
parent 16417 | 9bc16273c2d4 |
child 24893 | b8ef7afe3a6b |
permissions | -rw-r--r-- |
1478 | 1 |
(* Title: ZF/perm |
0 | 2 |
ID: $Id$ |
1478 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 4 |
Copyright 1991 University of Cambridge |
5 |
||
6 |
The theory underlying permutation groups |
|
7 |
-- Composition of relations, the identity relation |
|
8 |
-- Injections, surjections, bijections |
|
9 |
-- Lemmas for the Schroeder-Bernstein Theorem |
|
10 |
*) |
|
11 |
||
13356 | 12 |
header{*Injections, Surjections, Bijections, Composition*} |
13 |
||
16417 | 14 |
theory Perm imports func begin |
0 | 15 |
|
1806 | 16 |
constdefs |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
17 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
18 |
(*composition of relations and functions; NOT Suppes's relative product*) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
19 |
comp :: "[i,i]=>i" (infixr "O" 60) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
20 |
"r O s == {xz : domain(s)*range(r) . |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
21 |
EX x y z. xz=<x,z> & <x,y>:s & <y,z>:r}" |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
22 |
|
1806 | 23 |
(*the identity function for A*) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
24 |
id :: "i=>i" |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
25 |
"id(A) == (lam x:A. x)" |
0 | 26 |
|
1806 | 27 |
(*one-to-one functions from A to B*) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
28 |
inj :: "[i,i]=>i" |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
29 |
"inj(A,B) == { f: A->B. ALL w:A. ALL x:A. f`w=f`x --> w=x}" |
0 | 30 |
|
1806 | 31 |
(*onto functions from A to B*) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
32 |
surj :: "[i,i]=>i" |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
33 |
"surj(A,B) == { f: A->B . ALL y:B. EX x:A. f`x=y}" |
0 | 34 |
|
1806 | 35 |
(*one-to-one and onto functions*) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
36 |
bij :: "[i,i]=>i" |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
37 |
"bij(A,B) == inj(A,B) Int surj(A,B)" |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
38 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
39 |
|
13356 | 40 |
subsection{*Surjections*} |
41 |
||
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
42 |
(** Surjective function space **) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
43 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
44 |
lemma surj_is_fun: "f: surj(A,B) ==> f: A->B" |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
45 |
apply (unfold surj_def) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
46 |
apply (erule CollectD1) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
47 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
48 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
49 |
lemma fun_is_surj: "f : Pi(A,B) ==> f: surj(A,range(f))" |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
50 |
apply (unfold surj_def) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
51 |
apply (blast intro: apply_equality range_of_fun domain_type) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
52 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
53 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
54 |
lemma surj_range: "f: surj(A,B) ==> range(f)=B" |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
55 |
apply (unfold surj_def) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
56 |
apply (best intro: apply_Pair elim: range_type) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
57 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
58 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
59 |
(** A function with a right inverse is a surjection **) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
60 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
61 |
lemma f_imp_surjective: |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
62 |
"[| f: A->B; !!y. y:B ==> d(y): A; !!y. y:B ==> f`d(y) = y |] |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
63 |
==> f: surj(A,B)" |
13180 | 64 |
apply (simp add: surj_def, blast) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
65 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
66 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
67 |
lemma lam_surjective: |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
68 |
"[| !!x. x:A ==> c(x): B; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
69 |
!!y. y:B ==> d(y): A; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
70 |
!!y. y:B ==> c(d(y)) = y |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
71 |
|] ==> (lam x:A. c(x)) : surj(A,B)" |
13784 | 72 |
apply (rule_tac d = d in f_imp_surjective) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
73 |
apply (simp_all add: lam_type) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
74 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
75 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
76 |
(*Cantor's theorem revisited*) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
77 |
lemma cantor_surj: "f ~: surj(A,Pow(A))" |
13180 | 78 |
apply (unfold surj_def, safe) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
79 |
apply (cut_tac cantor) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
80 |
apply (best del: subsetI) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
81 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
82 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
83 |
|
13356 | 84 |
subsection{*Injections*} |
85 |
||
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
86 |
(** Injective function space **) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
87 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
88 |
lemma inj_is_fun: "f: inj(A,B) ==> f: A->B" |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
89 |
apply (unfold inj_def) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
90 |
apply (erule CollectD1) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
91 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
92 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
93 |
(*Good for dealing with sets of pairs, but a bit ugly in use [used in AC]*) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
94 |
lemma inj_equality: |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
95 |
"[| <a,b>:f; <c,b>:f; f: inj(A,B) |] ==> a=c" |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
96 |
apply (unfold inj_def) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
97 |
apply (blast dest: Pair_mem_PiD) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
98 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
99 |
|
13513 | 100 |
lemma inj_apply_equality: "[| f:inj(A,B); f`a=f`b; a:A; b:A |] ==> a=b" |
13180 | 101 |
by (unfold inj_def, blast) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
102 |
|
13513 | 103 |
|
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
104 |
(** A function with a left inverse is an injection **) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
105 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
106 |
lemma f_imp_injective: "[| f: A->B; ALL x:A. d(f`x)=x |] ==> f: inj(A,B)" |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
107 |
apply (simp (no_asm_simp) add: inj_def) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
108 |
apply (blast intro: subst_context [THEN box_equals]) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
109 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
110 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
111 |
lemma lam_injective: |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
112 |
"[| !!x. x:A ==> c(x): B; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
113 |
!!x. x:A ==> d(c(x)) = x |] |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
114 |
==> (lam x:A. c(x)) : inj(A,B)" |
13784 | 115 |
apply (rule_tac d = d in f_imp_injective) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
116 |
apply (simp_all add: lam_type) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
117 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
118 |
|
13356 | 119 |
subsection{*Bijections*} |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
120 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
121 |
lemma bij_is_inj: "f: bij(A,B) ==> f: inj(A,B)" |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
122 |
apply (unfold bij_def) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
123 |
apply (erule IntD1) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
124 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
125 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
126 |
lemma bij_is_surj: "f: bij(A,B) ==> f: surj(A,B)" |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
127 |
apply (unfold bij_def) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
128 |
apply (erule IntD2) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
129 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
130 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
131 |
(* f: bij(A,B) ==> f: A->B *) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
132 |
lemmas bij_is_fun = bij_is_inj [THEN inj_is_fun, standard] |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
133 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
134 |
lemma lam_bijective: |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
135 |
"[| !!x. x:A ==> c(x): B; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
136 |
!!y. y:B ==> d(y): A; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
137 |
!!x. x:A ==> d(c(x)) = x; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
138 |
!!y. y:B ==> c(d(y)) = y |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
139 |
|] ==> (lam x:A. c(x)) : bij(A,B)" |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
140 |
apply (unfold bij_def) |
13180 | 141 |
apply (blast intro!: lam_injective lam_surjective) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
142 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
143 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
144 |
lemma RepFun_bijective: "(ALL y : x. EX! y'. f(y') = f(y)) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
145 |
==> (lam z:{f(y). y:x}. THE y. f(y) = z) : bij({f(y). y:x}, x)" |
13784 | 146 |
apply (rule_tac d = f in lam_bijective) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
147 |
apply (auto simp add: the_equality2) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
148 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
149 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
150 |
|
13356 | 151 |
subsection{*Identity Function*} |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
152 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
153 |
lemma idI [intro!]: "a:A ==> <a,a> : id(A)" |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
154 |
apply (unfold id_def) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
155 |
apply (erule lamI) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
156 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
157 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
158 |
lemma idE [elim!]: "[| p: id(A); !!x.[| x:A; p=<x,x> |] ==> P |] ==> P" |
13180 | 159 |
by (simp add: id_def lam_def, blast) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
160 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
161 |
lemma id_type: "id(A) : A->A" |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
162 |
apply (unfold id_def) |
13180 | 163 |
apply (rule lam_type, assumption) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
164 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
165 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
166 |
lemma id_conv [simp]: "x:A ==> id(A)`x = x" |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
167 |
apply (unfold id_def) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
168 |
apply (simp (no_asm_simp)) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
169 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
170 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
171 |
lemma id_mono: "A<=B ==> id(A) <= id(B)" |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
172 |
apply (unfold id_def) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
173 |
apply (erule lam_mono) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
174 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
175 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
176 |
lemma id_subset_inj: "A<=B ==> id(A): inj(A,B)" |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
177 |
apply (simp add: inj_def id_def) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
178 |
apply (blast intro: lam_type) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
179 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
180 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
181 |
lemmas id_inj = subset_refl [THEN id_subset_inj, standard] |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
182 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
183 |
lemma id_surj: "id(A): surj(A,A)" |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
184 |
apply (unfold id_def surj_def) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
185 |
apply (simp (no_asm_simp)) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
186 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
187 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
188 |
lemma id_bij: "id(A): bij(A,A)" |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
189 |
apply (unfold bij_def) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
190 |
apply (blast intro: id_inj id_surj) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
191 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
192 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
193 |
lemma subset_iff_id: "A <= B <-> id(A) : A->B" |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
194 |
apply (unfold id_def) |
13180 | 195 |
apply (force intro!: lam_type dest: apply_type) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
196 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
197 |
|
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
13784
diff
changeset
|
198 |
text{*@{term id} as the identity relation*} |
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
13784
diff
changeset
|
199 |
lemma id_iff [simp]: "<x,y> \<in> id(A) <-> x=y & y \<in> A" |
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
13784
diff
changeset
|
200 |
by auto |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
201 |
|
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
13784
diff
changeset
|
202 |
|
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
13784
diff
changeset
|
203 |
|
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
13784
diff
changeset
|
204 |
subsection{*Converse of a Function*} |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
205 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
206 |
lemma inj_converse_fun: "f: inj(A,B) ==> converse(f) : range(f)->A" |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
207 |
apply (unfold inj_def) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
208 |
apply (simp (no_asm_simp) add: Pi_iff function_def) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
209 |
apply (erule CollectE) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
210 |
apply (simp (no_asm_simp) add: apply_iff) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
211 |
apply (blast dest: fun_is_rel) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
212 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
213 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
214 |
(** Equations for converse(f) **) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
215 |
|
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
13784
diff
changeset
|
216 |
text{*The premises are equivalent to saying that f is injective...*} |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
217 |
lemma left_inverse_lemma: |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
218 |
"[| f: A->B; converse(f): C->A; a: A |] ==> converse(f)`(f`a) = a" |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
219 |
by (blast intro: apply_Pair apply_equality converseI) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
220 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
221 |
lemma left_inverse [simp]: "[| f: inj(A,B); a: A |] ==> converse(f)`(f`a) = a" |
13180 | 222 |
by (blast intro: left_inverse_lemma inj_converse_fun inj_is_fun) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
223 |
|
14883 | 224 |
lemma left_inverse_eq: |
225 |
"[|f \<in> inj(A,B); f ` x = y; x \<in> A|] ==> converse(f) ` y = x" |
|
226 |
by auto |
|
227 |
||
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
228 |
lemmas left_inverse_bij = bij_is_inj [THEN left_inverse, standard] |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
229 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
230 |
lemma right_inverse_lemma: |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
231 |
"[| f: A->B; converse(f): C->A; b: C |] ==> f`(converse(f)`b) = b" |
14883 | 232 |
by (rule apply_Pair [THEN converseD [THEN apply_equality]], auto) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
233 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
234 |
(*Should the premises be f:surj(A,B), b:B for symmetry with left_inverse? |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
235 |
No: they would not imply that converse(f) was a function! *) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
236 |
lemma right_inverse [simp]: |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
237 |
"[| f: inj(A,B); b: range(f) |] ==> f`(converse(f)`b) = b" |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
238 |
by (blast intro: right_inverse_lemma inj_converse_fun inj_is_fun) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
239 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
240 |
lemma right_inverse_bij: "[| f: bij(A,B); b: B |] ==> f`(converse(f)`b) = b" |
13180 | 241 |
by (force simp add: bij_def surj_range) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
242 |
|
13356 | 243 |
subsection{*Converses of Injections, Surjections, Bijections*} |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
244 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
245 |
lemma inj_converse_inj: "f: inj(A,B) ==> converse(f): inj(range(f), A)" |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
246 |
apply (rule f_imp_injective) |
13180 | 247 |
apply (erule inj_converse_fun, clarify) |
248 |
apply (rule right_inverse) |
|
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
249 |
apply assumption |
13180 | 250 |
apply blast |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
251 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
252 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
253 |
lemma inj_converse_surj: "f: inj(A,B) ==> converse(f): surj(range(f), A)" |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
254 |
by (blast intro: f_imp_surjective inj_converse_fun left_inverse inj_is_fun |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
255 |
range_of_fun [THEN apply_type]) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
256 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
257 |
(*Adding this as an intro! rule seems to cause looping*) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
258 |
lemma bij_converse_bij [TC]: "f: bij(A,B) ==> converse(f): bij(B,A)" |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
259 |
apply (unfold bij_def) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
260 |
apply (fast elim: surj_range [THEN subst] inj_converse_inj inj_converse_surj) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
261 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
262 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
263 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
264 |
|
13356 | 265 |
subsection{*Composition of Two Relations*} |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
266 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
267 |
(*The inductive definition package could derive these theorems for (r O s)*) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
268 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
269 |
lemma compI [intro]: "[| <a,b>:s; <b,c>:r |] ==> <a,c> : r O s" |
13180 | 270 |
by (unfold comp_def, blast) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
271 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
272 |
lemma compE [elim!]: |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
273 |
"[| xz : r O s; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
274 |
!!x y z. [| xz=<x,z>; <x,y>:s; <y,z>:r |] ==> P |] |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
275 |
==> P" |
13180 | 276 |
by (unfold comp_def, blast) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
277 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
278 |
lemma compEpair: |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
279 |
"[| <a,c> : r O s; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
280 |
!!y. [| <a,y>:s; <y,c>:r |] ==> P |] |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
281 |
==> P" |
13180 | 282 |
by (erule compE, simp) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
283 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
284 |
lemma converse_comp: "converse(R O S) = converse(S) O converse(R)" |
13180 | 285 |
by blast |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
286 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
287 |
|
13356 | 288 |
subsection{*Domain and Range -- see Suppes, Section 3.1*} |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
289 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
290 |
(*Boyer et al., Set Theory in First-Order Logic, JAR 2 (1986), 287-327*) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
291 |
lemma range_comp: "range(r O s) <= range(r)" |
13180 | 292 |
by blast |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
293 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
294 |
lemma range_comp_eq: "domain(r) <= range(s) ==> range(r O s) = range(r)" |
13180 | 295 |
by (rule range_comp [THEN equalityI], blast) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
296 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
297 |
lemma domain_comp: "domain(r O s) <= domain(s)" |
13180 | 298 |
by blast |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
299 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
300 |
lemma domain_comp_eq: "range(s) <= domain(r) ==> domain(r O s) = domain(s)" |
13180 | 301 |
by (rule domain_comp [THEN equalityI], blast) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
302 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
303 |
lemma image_comp: "(r O s)``A = r``(s``A)" |
13180 | 304 |
by blast |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
305 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
306 |
|
13356 | 307 |
subsection{*Other Results*} |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
308 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
309 |
lemma comp_mono: "[| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)" |
13180 | 310 |
by blast |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
311 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
312 |
(*composition preserves relations*) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
313 |
lemma comp_rel: "[| s<=A*B; r<=B*C |] ==> (r O s) <= A*C" |
13180 | 314 |
by blast |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
315 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
316 |
(*associative law for composition*) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
317 |
lemma comp_assoc: "(r O s) O t = r O (s O t)" |
13180 | 318 |
by blast |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
319 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
320 |
(*left identity of composition; provable inclusions are |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
321 |
id(A) O r <= r |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
322 |
and [| r<=A*B; B<=C |] ==> r <= id(C) O r *) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
323 |
lemma left_comp_id: "r<=A*B ==> id(B) O r = r" |
13180 | 324 |
by blast |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
325 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
326 |
(*right identity of composition; provable inclusions are |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
327 |
r O id(A) <= r |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
328 |
and [| r<=A*B; A<=C |] ==> r <= r O id(C) *) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
329 |
lemma right_comp_id: "r<=A*B ==> r O id(A) = r" |
13180 | 330 |
by blast |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
331 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
332 |
|
13356 | 333 |
subsection{*Composition Preserves Functions, Injections, and Surjections*} |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
334 |
|
13180 | 335 |
lemma comp_function: "[| function(g); function(f) |] ==> function(f O g)" |
336 |
by (unfold function_def, blast) |
|
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
337 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
338 |
(*Don't think the premises can be weakened much*) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
339 |
lemma comp_fun: "[| g: A->B; f: B->C |] ==> (f O g) : A->C" |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
340 |
apply (auto simp add: Pi_def comp_function Pow_iff comp_rel) |
13180 | 341 |
apply (subst range_rel_subset [THEN domain_comp_eq], auto) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
342 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
343 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
344 |
(*Thanks to the new definition of "apply", the premise f: B->C is gone!*) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
345 |
lemma comp_fun_apply [simp]: |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
346 |
"[| g: A->B; a:A |] ==> (f O g)`a = f`(g`a)" |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
347 |
apply (frule apply_Pair, assumption) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
348 |
apply (simp add: apply_def image_comp) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
349 |
apply (blast dest: apply_equality) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
350 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
351 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
352 |
(*Simplifies compositions of lambda-abstractions*) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
353 |
lemma comp_lam: |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
354 |
"[| !!x. x:A ==> b(x): B |] |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
355 |
==> (lam y:B. c(y)) O (lam x:A. b(x)) = (lam x:A. c(b(x)))" |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
356 |
apply (subgoal_tac "(lam x:A. b(x)) : A -> B") |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
357 |
apply (rule fun_extension) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
358 |
apply (blast intro: comp_fun lam_funtype) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
359 |
apply (rule lam_funtype) |
13180 | 360 |
apply simp |
361 |
apply (simp add: lam_type) |
|
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
362 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
363 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
364 |
lemma comp_inj: |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
365 |
"[| g: inj(A,B); f: inj(B,C) |] ==> (f O g) : inj(A,C)" |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
366 |
apply (frule inj_is_fun [of g]) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
367 |
apply (frule inj_is_fun [of f]) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
368 |
apply (rule_tac d = "%y. converse (g) ` (converse (f) ` y)" in f_imp_injective) |
13180 | 369 |
apply (blast intro: comp_fun, simp) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
370 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
371 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
372 |
lemma comp_surj: |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
373 |
"[| g: surj(A,B); f: surj(B,C) |] ==> (f O g) : surj(A,C)" |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
374 |
apply (unfold surj_def) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
375 |
apply (blast intro!: comp_fun comp_fun_apply) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
376 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
377 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
378 |
lemma comp_bij: |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
379 |
"[| g: bij(A,B); f: bij(B,C) |] ==> (f O g) : bij(A,C)" |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
380 |
apply (unfold bij_def) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
381 |
apply (blast intro: comp_inj comp_surj) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
382 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
383 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
384 |
|
13356 | 385 |
subsection{*Dual Properties of @{term inj} and @{term surj}*} |
386 |
||
387 |
text{*Useful for proofs from |
|
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
388 |
D Pastre. Automatic theorem proving in set theory. |
13356 | 389 |
Artificial Intelligence, 10:1--27, 1978.*} |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
390 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
391 |
lemma comp_mem_injD1: |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
392 |
"[| (f O g): inj(A,C); g: A->B; f: B->C |] ==> g: inj(A,B)" |
13356 | 393 |
by (unfold inj_def, force) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
394 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
395 |
lemma comp_mem_injD2: |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
396 |
"[| (f O g): inj(A,C); g: surj(A,B); f: B->C |] ==> f: inj(B,C)" |
13180 | 397 |
apply (unfold inj_def surj_def, safe) |
13784 | 398 |
apply (rule_tac x1 = x in bspec [THEN bexE]) |
399 |
apply (erule_tac [3] x1 = w in bspec [THEN bexE], assumption+, safe) |
|
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
400 |
apply (rule_tac t = "op ` (g) " in subst_context) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
401 |
apply (erule asm_rl bspec [THEN bspec, THEN mp])+ |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
402 |
apply (simp (no_asm_simp)) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
403 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
404 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
405 |
lemma comp_mem_surjD1: |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
406 |
"[| (f O g): surj(A,C); g: A->B; f: B->C |] ==> f: surj(B,C)" |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
407 |
apply (unfold surj_def) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
408 |
apply (blast intro!: comp_fun_apply [symmetric] apply_funtype) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
409 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
410 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
411 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
412 |
lemma comp_mem_surjD2: |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
413 |
"[| (f O g): surj(A,C); g: A->B; f: inj(B,C) |] ==> g: surj(A,B)" |
13180 | 414 |
apply (unfold inj_def surj_def, safe) |
415 |
apply (drule_tac x = "f`y" in bspec, auto) |
|
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
416 |
apply (blast intro: apply_funtype) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
417 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
418 |
|
13356 | 419 |
subsubsection{*Inverses of Composition*} |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
420 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
421 |
(*left inverse of composition; one inclusion is |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
422 |
f: A->B ==> id(A) <= converse(f) O f *) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
423 |
lemma left_comp_inverse: "f: inj(A,B) ==> converse(f) O f = id(A)" |
13180 | 424 |
apply (unfold inj_def, clarify) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
425 |
apply (rule equalityI) |
13180 | 426 |
apply (auto simp add: apply_iff, blast) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
427 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
428 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
429 |
(*right inverse of composition; one inclusion is |
13180 | 430 |
f: A->B ==> f O converse(f) <= id(B) *) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
431 |
lemma right_comp_inverse: |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
432 |
"f: surj(A,B) ==> f O converse(f) = id(B)" |
13180 | 433 |
apply (simp add: surj_def, clarify) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
434 |
apply (rule equalityI) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
435 |
apply (best elim: domain_type range_type dest: apply_equality2) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
436 |
apply (blast intro: apply_Pair) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
437 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
438 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
439 |
|
13356 | 440 |
subsubsection{*Proving that a Function is a Bijection*} |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
441 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
442 |
lemma comp_eq_id_iff: |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
443 |
"[| f: A->B; g: B->A |] ==> f O g = id(B) <-> (ALL y:B. f`(g`y)=y)" |
13180 | 444 |
apply (unfold id_def, safe) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
445 |
apply (drule_tac t = "%h. h`y " in subst_context) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
446 |
apply simp |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
447 |
apply (rule fun_extension) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
448 |
apply (blast intro: comp_fun lam_type) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
449 |
apply auto |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
450 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
451 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
452 |
lemma fg_imp_bijective: |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
453 |
"[| f: A->B; g: B->A; f O g = id(B); g O f = id(A) |] ==> f : bij(A,B)" |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
454 |
apply (unfold bij_def) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
455 |
apply (simp add: comp_eq_id_iff) |
13180 | 456 |
apply (blast intro: f_imp_injective f_imp_surjective apply_funtype) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
457 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
458 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
459 |
lemma nilpotent_imp_bijective: "[| f: A->A; f O f = id(A) |] ==> f : bij(A,A)" |
13180 | 460 |
by (blast intro: fg_imp_bijective) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
461 |
|
13180 | 462 |
lemma invertible_imp_bijective: |
463 |
"[| converse(f): B->A; f: A->B |] ==> f : bij(A,B)" |
|
464 |
by (simp add: fg_imp_bijective comp_eq_id_iff |
|
465 |
left_inverse_lemma right_inverse_lemma) |
|
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
466 |
|
13356 | 467 |
subsubsection{*Unions of Functions*} |
468 |
||
469 |
text{*See similar theorems in func.thy*} |
|
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
470 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
471 |
(*Theorem by KG, proof by LCP*) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
472 |
lemma inj_disjoint_Un: |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
473 |
"[| f: inj(A,B); g: inj(C,D); B Int D = 0 |] |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
474 |
==> (lam a: A Un C. if a:A then f`a else g`a) : inj(A Un C, B Un D)" |
13180 | 475 |
apply (rule_tac d = "%z. if z:B then converse (f) `z else converse (g) `z" |
476 |
in lam_injective) |
|
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
477 |
apply (auto simp add: inj_is_fun [THEN apply_type]) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
478 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
479 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
480 |
lemma surj_disjoint_Un: |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
481 |
"[| f: surj(A,B); g: surj(C,D); A Int C = 0 |] |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
482 |
==> (f Un g) : surj(A Un C, B Un D)" |
13180 | 483 |
apply (simp add: surj_def fun_disjoint_Un) |
484 |
apply (blast dest!: domain_of_fun |
|
485 |
intro!: fun_disjoint_apply1 fun_disjoint_apply2) |
|
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
486 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
487 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
488 |
(*A simple, high-level proof; the version for injections follows from it, |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
489 |
using f:inj(A,B) <-> f:bij(A,range(f)) *) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
490 |
lemma bij_disjoint_Un: |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
491 |
"[| f: bij(A,B); g: bij(C,D); A Int C = 0; B Int D = 0 |] |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
492 |
==> (f Un g) : bij(A Un C, B Un D)" |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
493 |
apply (rule invertible_imp_bijective) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
494 |
apply (subst converse_Un) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
495 |
apply (auto intro: fun_disjoint_Un bij_is_fun bij_converse_bij) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
496 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
497 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
498 |
|
13356 | 499 |
subsubsection{*Restrictions as Surjections and Bijections*} |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
500 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
501 |
lemma surj_image: |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
502 |
"f: Pi(A,B) ==> f: surj(A, f``A)" |
13180 | 503 |
apply (simp add: surj_def) |
504 |
apply (blast intro: apply_equality apply_Pair Pi_type) |
|
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
505 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
506 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
507 |
lemma restrict_image [simp]: "restrict(f,A) `` B = f `` (A Int B)" |
13180 | 508 |
by (auto simp add: restrict_def) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
509 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
510 |
lemma restrict_inj: |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
511 |
"[| f: inj(A,B); C<=A |] ==> restrict(f,C): inj(C,B)" |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
512 |
apply (unfold inj_def) |
13180 | 513 |
apply (safe elim!: restrict_type2, auto) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
514 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
515 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
516 |
lemma restrict_surj: "[| f: Pi(A,B); C<=A |] ==> restrict(f,C): surj(C, f``C)" |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
517 |
apply (insert restrict_type2 [THEN surj_image]) |
13180 | 518 |
apply (simp add: restrict_image) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
519 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
520 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
521 |
lemma restrict_bij: |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
522 |
"[| f: inj(A,B); C<=A |] ==> restrict(f,C): bij(C, f``C)" |
13180 | 523 |
apply (simp add: inj_def bij_def) |
524 |
apply (blast intro: restrict_surj surj_is_fun) |
|
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
525 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
526 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
527 |
|
13356 | 528 |
subsubsection{*Lemmas for Ramsey's Theorem*} |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
529 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
530 |
lemma inj_weaken_type: "[| f: inj(A,B); B<=D |] ==> f: inj(A,D)" |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
531 |
apply (unfold inj_def) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
532 |
apply (blast intro: fun_weaken_type) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
533 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
534 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
535 |
lemma inj_succ_restrict: |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
536 |
"[| f: inj(succ(m), A) |] ==> restrict(f,m) : inj(m, A-{f`m})" |
13269 | 537 |
apply (rule restrict_bij [THEN bij_is_inj, THEN inj_weaken_type], assumption, blast) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
538 |
apply (unfold inj_def) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
539 |
apply (fast elim: range_type mem_irrefl dest: apply_equality) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
540 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
541 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
542 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
543 |
lemma inj_extend: |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
544 |
"[| f: inj(A,B); a~:A; b~:B |] |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
545 |
==> cons(<a,b>,f) : inj(cons(a,A), cons(b,B))" |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
546 |
apply (unfold inj_def) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
547 |
apply (force intro: apply_type simp add: fun_extend) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
548 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
549 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
550 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
551 |
ML |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
552 |
{* |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
553 |
val comp_def = thm "comp_def"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
554 |
val id_def = thm "id_def"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
555 |
val inj_def = thm "inj_def"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
556 |
val surj_def = thm "surj_def"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
557 |
val bij_def = thm "bij_def"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
558 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
559 |
val surj_is_fun = thm "surj_is_fun"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
560 |
val fun_is_surj = thm "fun_is_surj"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
561 |
val surj_range = thm "surj_range"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
562 |
val f_imp_surjective = thm "f_imp_surjective"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
563 |
val lam_surjective = thm "lam_surjective"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
564 |
val cantor_surj = thm "cantor_surj"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
565 |
val inj_is_fun = thm "inj_is_fun"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
566 |
val inj_equality = thm "inj_equality"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
567 |
val inj_apply_equality = thm "inj_apply_equality"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
568 |
val f_imp_injective = thm "f_imp_injective"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
569 |
val lam_injective = thm "lam_injective"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
570 |
val bij_is_inj = thm "bij_is_inj"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
571 |
val bij_is_surj = thm "bij_is_surj"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
572 |
val bij_is_fun = thm "bij_is_fun"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
573 |
val lam_bijective = thm "lam_bijective"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
574 |
val RepFun_bijective = thm "RepFun_bijective"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
575 |
val idI = thm "idI"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
576 |
val idE = thm "idE"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
577 |
val id_type = thm "id_type"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
578 |
val id_conv = thm "id_conv"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
579 |
val id_mono = thm "id_mono"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
580 |
val id_subset_inj = thm "id_subset_inj"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
581 |
val id_inj = thm "id_inj"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
582 |
val id_surj = thm "id_surj"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
583 |
val id_bij = thm "id_bij"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
584 |
val subset_iff_id = thm "subset_iff_id"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
585 |
val inj_converse_fun = thm "inj_converse_fun"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
586 |
val left_inverse = thm "left_inverse"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
587 |
val left_inverse_bij = thm "left_inverse_bij"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
588 |
val right_inverse = thm "right_inverse"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
589 |
val right_inverse_bij = thm "right_inverse_bij"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
590 |
val inj_converse_inj = thm "inj_converse_inj"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
591 |
val inj_converse_surj = thm "inj_converse_surj"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
592 |
val bij_converse_bij = thm "bij_converse_bij"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
593 |
val compI = thm "compI"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
594 |
val compE = thm "compE"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
595 |
val compEpair = thm "compEpair"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
596 |
val converse_comp = thm "converse_comp"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
597 |
val range_comp = thm "range_comp"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
598 |
val range_comp_eq = thm "range_comp_eq"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
599 |
val domain_comp = thm "domain_comp"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
600 |
val domain_comp_eq = thm "domain_comp_eq"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
601 |
val image_comp = thm "image_comp"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
602 |
val comp_mono = thm "comp_mono"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
603 |
val comp_rel = thm "comp_rel"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
604 |
val comp_assoc = thm "comp_assoc"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
605 |
val left_comp_id = thm "left_comp_id"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
606 |
val right_comp_id = thm "right_comp_id"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
607 |
val comp_function = thm "comp_function"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
608 |
val comp_fun = thm "comp_fun"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
609 |
val comp_fun_apply = thm "comp_fun_apply"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
610 |
val comp_lam = thm "comp_lam"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
611 |
val comp_inj = thm "comp_inj"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
612 |
val comp_surj = thm "comp_surj"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
613 |
val comp_bij = thm "comp_bij"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
614 |
val comp_mem_injD1 = thm "comp_mem_injD1"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
615 |
val comp_mem_injD2 = thm "comp_mem_injD2"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
616 |
val comp_mem_surjD1 = thm "comp_mem_surjD1"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
617 |
val comp_mem_surjD2 = thm "comp_mem_surjD2"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
618 |
val left_comp_inverse = thm "left_comp_inverse"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
619 |
val right_comp_inverse = thm "right_comp_inverse"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
620 |
val comp_eq_id_iff = thm "comp_eq_id_iff"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
621 |
val fg_imp_bijective = thm "fg_imp_bijective"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
622 |
val nilpotent_imp_bijective = thm "nilpotent_imp_bijective"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
623 |
val invertible_imp_bijective = thm "invertible_imp_bijective"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
624 |
val inj_disjoint_Un = thm "inj_disjoint_Un"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
625 |
val surj_disjoint_Un = thm "surj_disjoint_Un"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
626 |
val bij_disjoint_Un = thm "bij_disjoint_Un"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
627 |
val surj_image = thm "surj_image"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
628 |
val restrict_image = thm "restrict_image"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
629 |
val restrict_inj = thm "restrict_inj"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
630 |
val restrict_surj = thm "restrict_surj"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
631 |
val restrict_bij = thm "restrict_bij"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
632 |
val inj_weaken_type = thm "inj_weaken_type"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
633 |
val inj_succ_restrict = thm "inj_succ_restrict"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
634 |
val inj_extend = thm "inj_extend"; |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
635 |
*} |
0 | 636 |
|
637 |
end |