author | paulson |
Mon, 30 Jan 2023 15:24:25 +0000 | |
changeset 77139 | da8a0e7bcac8 |
parent 76217 | 8655344f1cf6 |
permissions | -rw-r--r-- |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
24893
diff
changeset
|
1 |
(* Title: ZF/Perm.thy |
1478 | 2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 3 |
Copyright 1991 University of Cambridge |
4 |
||
5 |
The theory underlying permutation groups |
|
6 |
-- Composition of relations, the identity relation |
|
7 |
-- Injections, surjections, bijections |
|
8 |
-- Lemmas for the Schroeder-Bernstein Theorem |
|
9 |
*) |
|
10 |
||
60770 | 11 |
section\<open>Injections, Surjections, Bijections, Composition\<close> |
13356 | 12 |
|
16417 | 13 |
theory Perm imports func begin |
0 | 14 |
|
24893 | 15 |
definition |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
16 |
(*composition of relations and functions; NOT Suppes's relative product*) |
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
17 |
comp :: "[i,i]\<Rightarrow>i" (infixr \<open>O\<close> 60) where |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
18 |
"r O s \<equiv> {xz \<in> domain(s)*range(r) . |
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
19 |
\<exists>x y z. xz=\<langle>x,z\<rangle> \<and> \<langle>x,y\<rangle>:s \<and> \<langle>y,z\<rangle>:r}" |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
20 |
|
24893 | 21 |
definition |
1806 | 22 |
(*the identity function for A*) |
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
23 |
id :: "i\<Rightarrow>i" where |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
24 |
"id(A) \<equiv> (\<lambda>x\<in>A. x)" |
0 | 25 |
|
24893 | 26 |
definition |
1806 | 27 |
(*one-to-one functions from A to B*) |
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
28 |
inj :: "[i,i]\<Rightarrow>i" where |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
29 |
"inj(A,B) \<equiv> { f \<in> A->B. \<forall>w\<in>A. \<forall>x\<in>A. f`w=f`x \<longrightarrow> w=x}" |
0 | 30 |
|
24893 | 31 |
definition |
1806 | 32 |
(*onto functions from A to B*) |
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
33 |
surj :: "[i,i]\<Rightarrow>i" where |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
34 |
"surj(A,B) \<equiv> { f \<in> A->B . \<forall>y\<in>B. \<exists>x\<in>A. f`x=y}" |
0 | 35 |
|
24893 | 36 |
definition |
1806 | 37 |
(*one-to-one and onto functions*) |
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
38 |
bij :: "[i,i]\<Rightarrow>i" where |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
39 |
"bij(A,B) \<equiv> inj(A,B) \<inter> surj(A,B)" |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
40 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
41 |
|
60770 | 42 |
subsection\<open>Surjective Function Space\<close> |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
43 |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
44 |
lemma surj_is_fun: "f \<in> surj(A,B) \<Longrightarrow> f \<in> A->B" |
76216
9fc34f76b4e8
getting rid of apply (unfold ...)
paulson <lp15@cam.ac.uk>
parents:
76215
diff
changeset
|
45 |
unfolding surj_def |
13176
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 |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
49 |
lemma fun_is_surj: "f \<in> Pi(A,B) \<Longrightarrow> f \<in> surj(A,range(f))" |
76216
9fc34f76b4e8
getting rid of apply (unfold ...)
paulson <lp15@cam.ac.uk>
parents:
76215
diff
changeset
|
50 |
unfolding surj_def |
13176
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 |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
54 |
lemma surj_range: "f \<in> surj(A,B) \<Longrightarrow> range(f)=B" |
76216
9fc34f76b4e8
getting rid of apply (unfold ...)
paulson <lp15@cam.ac.uk>
parents:
76215
diff
changeset
|
55 |
unfolding surj_def |
13176
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 |
|
60770 | 59 |
text\<open>A function with a right inverse is a surjection\<close> |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
60 |
|
46821
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
61 |
lemma f_imp_surjective: |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
62 |
"\<lbrakk>f \<in> A->B; \<And>y. y \<in> B \<Longrightarrow> d(y): A; \<And>y. y \<in> B \<Longrightarrow> f`d(y) = y\<rbrakk> |
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
63 |
\<Longrightarrow> f \<in> surj(A,B)" |
41160
be34449f6cba
Added two theorems about the concept of range. Tidied up the comments.
paulson
parents:
32960
diff
changeset
|
64 |
by (simp add: surj_def, blast) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
65 |
|
46821
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
66 |
lemma lam_surjective: |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
67 |
"\<lbrakk>\<And>x. x \<in> A \<Longrightarrow> c(x): B; |
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
68 |
\<And>y. y \<in> B \<Longrightarrow> d(y): A; |
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
69 |
\<And>y. y \<in> B \<Longrightarrow> c(d(y)) = y |
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
70 |
\<rbrakk> \<Longrightarrow> (\<lambda>x\<in>A. c(x)) \<in> surj(A,B)" |
46821
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
71 |
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
|
72 |
apply (simp_all add: lam_type) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
73 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
74 |
|
60770 | 75 |
text\<open>Cantor's theorem revisited\<close> |
46820 | 76 |
lemma cantor_surj: "f \<notin> surj(A,Pow(A))" |
13180 | 77 |
apply (unfold surj_def, safe) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
78 |
apply (cut_tac cantor) |
46821
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
79 |
apply (best del: subsetI) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
80 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
81 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
82 |
|
60770 | 83 |
subsection\<open>Injective Function Space\<close> |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
84 |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
85 |
lemma inj_is_fun: "f \<in> inj(A,B) \<Longrightarrow> f \<in> A->B" |
76216
9fc34f76b4e8
getting rid of apply (unfold ...)
paulson <lp15@cam.ac.uk>
parents:
76215
diff
changeset
|
86 |
unfolding inj_def |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
87 |
apply (erule CollectD1) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
88 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
89 |
|
60770 | 90 |
text\<open>Good for dealing with sets of pairs, but a bit ugly in use [used in AC]\<close> |
46821
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
91 |
lemma inj_equality: |
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
92 |
"\<lbrakk>\<langle>a,b\<rangle>:f; \<langle>c,b\<rangle>:f; f \<in> inj(A,B)\<rbrakk> \<Longrightarrow> a=c" |
76216
9fc34f76b4e8
getting rid of apply (unfold ...)
paulson <lp15@cam.ac.uk>
parents:
76215
diff
changeset
|
93 |
unfolding inj_def |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
94 |
apply (blast dest: Pair_mem_PiD) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
95 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
96 |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
97 |
lemma inj_apply_equality: "\<lbrakk>f \<in> inj(A,B); f`a=f`b; a \<in> A; b \<in> A\<rbrakk> \<Longrightarrow> a=b" |
13180 | 98 |
by (unfold inj_def, blast) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
99 |
|
60770 | 100 |
text\<open>A function with a left inverse is an injection\<close> |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
101 |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
102 |
lemma f_imp_injective: "\<lbrakk>f \<in> A->B; \<forall>x\<in>A. d(f`x)=x\<rbrakk> \<Longrightarrow> f \<in> inj(A,B)" |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
103 |
apply (simp (no_asm_simp) add: inj_def) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
104 |
apply (blast intro: subst_context [THEN box_equals]) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
105 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
106 |
|
46821
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
107 |
lemma lam_injective: |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
108 |
"\<lbrakk>\<And>x. x \<in> A \<Longrightarrow> c(x): B; |
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
109 |
\<And>x. x \<in> A \<Longrightarrow> d(c(x)) = x\<rbrakk> |
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
110 |
\<Longrightarrow> (\<lambda>x\<in>A. c(x)) \<in> inj(A,B)" |
13784 | 111 |
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
|
112 |
apply (simp_all add: lam_type) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
113 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
114 |
|
60770 | 115 |
subsection\<open>Bijections\<close> |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
116 |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
117 |
lemma bij_is_inj: "f \<in> bij(A,B) \<Longrightarrow> f \<in> inj(A,B)" |
76216
9fc34f76b4e8
getting rid of apply (unfold ...)
paulson <lp15@cam.ac.uk>
parents:
76215
diff
changeset
|
118 |
unfolding bij_def |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
119 |
apply (erule IntD1) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
120 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
121 |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
122 |
lemma bij_is_surj: "f \<in> bij(A,B) \<Longrightarrow> f \<in> surj(A,B)" |
76216
9fc34f76b4e8
getting rid of apply (unfold ...)
paulson <lp15@cam.ac.uk>
parents:
76215
diff
changeset
|
123 |
unfolding bij_def |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
124 |
apply (erule IntD2) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
125 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
126 |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
127 |
lemma bij_is_fun: "f \<in> bij(A,B) \<Longrightarrow> f \<in> A->B" |
46953 | 128 |
by (rule bij_is_inj [THEN inj_is_fun]) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
129 |
|
46821
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
130 |
lemma lam_bijective: |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
131 |
"\<lbrakk>\<And>x. x \<in> A \<Longrightarrow> c(x): B; |
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
132 |
\<And>y. y \<in> B \<Longrightarrow> d(y): A; |
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
133 |
\<And>x. x \<in> A \<Longrightarrow> d(c(x)) = x; |
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
134 |
\<And>y. y \<in> B \<Longrightarrow> c(d(y)) = y |
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
135 |
\<rbrakk> \<Longrightarrow> (\<lambda>x\<in>A. c(x)) \<in> bij(A,B)" |
76216
9fc34f76b4e8
getting rid of apply (unfold ...)
paulson <lp15@cam.ac.uk>
parents:
76215
diff
changeset
|
136 |
unfolding bij_def |
13180 | 137 |
apply (blast intro!: lam_injective lam_surjective) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
138 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
139 |
|
63901 | 140 |
lemma RepFun_bijective: "(\<forall>y\<in>x. \<exists>!y'. f(y') = f(y)) |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
141 |
\<Longrightarrow> (\<lambda>z\<in>{f(y). y \<in> x}. THE y. f(y) = z) \<in> bij({f(y). y \<in> x}, x)" |
13784 | 142 |
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
|
143 |
apply (auto simp add: the_equality2) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
144 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
145 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
146 |
|
60770 | 147 |
subsection\<open>Identity Function\<close> |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
148 |
|
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
149 |
lemma idI [intro!]: "a \<in> A \<Longrightarrow> \<langle>a,a\<rangle> \<in> id(A)" |
76216
9fc34f76b4e8
getting rid of apply (unfold ...)
paulson <lp15@cam.ac.uk>
parents:
76215
diff
changeset
|
150 |
unfolding id_def |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
151 |
apply (erule lamI) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
152 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
153 |
|
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
154 |
lemma idE [elim!]: "\<lbrakk>p \<in> id(A); \<And>x.\<lbrakk>x \<in> A; p=\<langle>x,x\<rangle>\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" |
13180 | 155 |
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
|
156 |
|
46820 | 157 |
lemma id_type: "id(A) \<in> A->A" |
76216
9fc34f76b4e8
getting rid of apply (unfold ...)
paulson <lp15@cam.ac.uk>
parents:
76215
diff
changeset
|
158 |
unfolding id_def |
13180 | 159 |
apply (rule lam_type, assumption) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
160 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
161 |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
162 |
lemma id_conv [simp]: "x \<in> A \<Longrightarrow> id(A)`x = x" |
76216
9fc34f76b4e8
getting rid of apply (unfold ...)
paulson <lp15@cam.ac.uk>
parents:
76215
diff
changeset
|
163 |
unfolding id_def |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
164 |
apply (simp (no_asm_simp)) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
165 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
166 |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
167 |
lemma id_mono: "A<=B \<Longrightarrow> id(A) \<subseteq> id(B)" |
76216
9fc34f76b4e8
getting rid of apply (unfold ...)
paulson <lp15@cam.ac.uk>
parents:
76215
diff
changeset
|
168 |
unfolding id_def |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
169 |
apply (erule lam_mono) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
170 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
171 |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
172 |
lemma id_subset_inj: "A<=B \<Longrightarrow> id(A): inj(A,B)" |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
173 |
apply (simp add: inj_def id_def) |
46821
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
174 |
apply (blast intro: lam_type) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
175 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
176 |
|
45602 | 177 |
lemmas id_inj = subset_refl [THEN id_subset_inj] |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
178 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
179 |
lemma id_surj: "id(A): surj(A,A)" |
76217 | 180 |
unfolding id_def surj_def |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
181 |
apply (simp (no_asm_simp)) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
182 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
183 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
184 |
lemma id_bij: "id(A): bij(A,A)" |
76216
9fc34f76b4e8
getting rid of apply (unfold ...)
paulson <lp15@cam.ac.uk>
parents:
76215
diff
changeset
|
185 |
unfolding bij_def |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
186 |
apply (blast intro: id_inj id_surj) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
187 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
188 |
|
46821
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
189 |
lemma subset_iff_id: "A \<subseteq> B \<longleftrightarrow> id(A) \<in> A->B" |
76216
9fc34f76b4e8
getting rid of apply (unfold ...)
paulson <lp15@cam.ac.uk>
parents:
76215
diff
changeset
|
190 |
unfolding id_def |
13180 | 191 |
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
|
192 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
193 |
|
69593 | 194 |
text\<open>\<^term>\<open>id\<close> as the identity relation\<close> |
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
195 |
lemma id_iff [simp]: "\<langle>x,y\<rangle> \<in> id(A) \<longleftrightarrow> x=y \<and> y \<in> A" |
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
13784
diff
changeset
|
196 |
by auto |
13176
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 |
|
60770 | 199 |
subsection\<open>Converse of a Function\<close> |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
200 |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
201 |
lemma inj_converse_fun: "f \<in> inj(A,B) \<Longrightarrow> converse(f) \<in> range(f)->A" |
76216
9fc34f76b4e8
getting rid of apply (unfold ...)
paulson <lp15@cam.ac.uk>
parents:
76215
diff
changeset
|
202 |
unfolding inj_def |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
203 |
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
|
204 |
apply (erule CollectE) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
205 |
apply (simp (no_asm_simp) add: apply_iff) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
206 |
apply (blast dest: fun_is_rel) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
207 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
208 |
|
60770 | 209 |
text\<open>Equations for converse(f)\<close> |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
210 |
|
60770 | 211 |
text\<open>The premises are equivalent to saying that f is injective...\<close> |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
212 |
lemma left_inverse_lemma: |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
213 |
"\<lbrakk>f \<in> A->B; converse(f): C->A; a \<in> A\<rbrakk> \<Longrightarrow> converse(f)`(f`a) = a" |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
214 |
by (blast intro: apply_Pair apply_equality converseI) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
215 |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
216 |
lemma left_inverse [simp]: "\<lbrakk>f \<in> inj(A,B); a \<in> A\<rbrakk> \<Longrightarrow> converse(f)`(f`a) = a" |
13180 | 217 |
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
|
218 |
|
14883 | 219 |
lemma left_inverse_eq: |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
220 |
"\<lbrakk>f \<in> inj(A,B); f ` x = y; x \<in> A\<rbrakk> \<Longrightarrow> converse(f) ` y = x" |
14883 | 221 |
by auto |
222 |
||
45602 | 223 |
lemmas left_inverse_bij = bij_is_inj [THEN left_inverse] |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
224 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
225 |
lemma right_inverse_lemma: |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
226 |
"\<lbrakk>f \<in> A->B; converse(f): C->A; b \<in> C\<rbrakk> \<Longrightarrow> f`(converse(f)`b) = b" |
46821
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
227 |
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
|
228 |
|
46953 | 229 |
(*Should the premises be f \<in> surj(A,B), b \<in> B for symmetry with left_inverse? |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
230 |
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
|
231 |
lemma right_inverse [simp]: |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
232 |
"\<lbrakk>f \<in> inj(A,B); b \<in> range(f)\<rbrakk> \<Longrightarrow> f`(converse(f)`b) = b" |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
233 |
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
|
234 |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
235 |
lemma right_inverse_bij: "\<lbrakk>f \<in> bij(A,B); b \<in> B\<rbrakk> \<Longrightarrow> f`(converse(f)`b) = b" |
13180 | 236 |
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
|
237 |
|
60770 | 238 |
subsection\<open>Converses of Injections, Surjections, Bijections\<close> |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
239 |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
240 |
lemma inj_converse_inj: "f \<in> inj(A,B) \<Longrightarrow> converse(f): inj(range(f), A)" |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
241 |
apply (rule f_imp_injective) |
46821
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
242 |
apply (erule inj_converse_fun, clarify) |
13180 | 243 |
apply (rule right_inverse) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
244 |
apply assumption |
46821
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
245 |
apply blast |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
246 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
247 |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
248 |
lemma inj_converse_surj: "f \<in> inj(A,B) \<Longrightarrow> converse(f): surj(range(f), A)" |
46821
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
249 |
by (blast intro: f_imp_surjective inj_converse_fun left_inverse inj_is_fun |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
250 |
range_of_fun [THEN apply_type]) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
251 |
|
60770 | 252 |
text\<open>Adding this as an intro! rule seems to cause looping\<close> |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
253 |
lemma bij_converse_bij [TC]: "f \<in> bij(A,B) \<Longrightarrow> converse(f): bij(B,A)" |
76216
9fc34f76b4e8
getting rid of apply (unfold ...)
paulson <lp15@cam.ac.uk>
parents:
76215
diff
changeset
|
254 |
unfolding bij_def |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
255 |
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
|
256 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
257 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
258 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
259 |
|
60770 | 260 |
subsection\<open>Composition of Two Relations\<close> |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
261 |
|
69593 | 262 |
text\<open>The inductive definition package could derive these theorems for \<^term>\<open>r O s\<close>\<close> |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
263 |
|
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
264 |
lemma compI [intro]: "\<lbrakk>\<langle>a,b\<rangle>:s; \<langle>b,c\<rangle>:r\<rbrakk> \<Longrightarrow> \<langle>a,c\<rangle> \<in> r O s" |
13180 | 265 |
by (unfold comp_def, blast) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
266 |
|
46821
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
267 |
lemma compE [elim!]: |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
268 |
"\<lbrakk>xz \<in> r O s; |
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
269 |
\<And>x y z. \<lbrakk>xz=\<langle>x,z\<rangle>; \<langle>x,y\<rangle>:s; \<langle>y,z\<rangle>:r\<rbrakk> \<Longrightarrow> P\<rbrakk> |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
270 |
\<Longrightarrow> P" |
13180 | 271 |
by (unfold comp_def, blast) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
272 |
|
46821
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
273 |
lemma compEpair: |
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
274 |
"\<lbrakk>\<langle>a,c\<rangle> \<in> r O s; |
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
275 |
\<And>y. \<lbrakk>\<langle>a,y\<rangle>:s; \<langle>y,c\<rangle>:r\<rbrakk> \<Longrightarrow> P\<rbrakk> |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
276 |
\<Longrightarrow> P" |
46821
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
277 |
by (erule compE, simp) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
278 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
279 |
lemma converse_comp: "converse(R O S) = converse(S) O converse(R)" |
13180 | 280 |
by blast |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
281 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
282 |
|
60770 | 283 |
subsection\<open>Domain and Range -- see Suppes, Section 3.1\<close> |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
284 |
|
60770 | 285 |
text\<open>Boyer et al., Set Theory in First-Order Logic, JAR 2 (1986), 287-327\<close> |
46820 | 286 |
lemma range_comp: "range(r O s) \<subseteq> range(r)" |
13180 | 287 |
by blast |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
288 |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
289 |
lemma range_comp_eq: "domain(r) \<subseteq> range(s) \<Longrightarrow> range(r O s) = range(r)" |
13180 | 290 |
by (rule range_comp [THEN equalityI], blast) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
291 |
|
46820 | 292 |
lemma domain_comp: "domain(r O s) \<subseteq> domain(s)" |
13180 | 293 |
by blast |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
294 |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
295 |
lemma domain_comp_eq: "range(s) \<subseteq> domain(r) \<Longrightarrow> domain(r O s) = domain(s)" |
13180 | 296 |
by (rule domain_comp [THEN equalityI], blast) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
297 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
298 |
lemma image_comp: "(r O s)``A = r``(s``A)" |
13180 | 299 |
by blast |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
300 |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
301 |
lemma inj_inj_range: "f \<in> inj(A,B) \<Longrightarrow> f \<in> inj(A,range(f))" |
41160
be34449f6cba
Added two theorems about the concept of range. Tidied up the comments.
paulson
parents:
32960
diff
changeset
|
302 |
by (auto simp add: inj_def Pi_iff function_def) |
be34449f6cba
Added two theorems about the concept of range. Tidied up the comments.
paulson
parents:
32960
diff
changeset
|
303 |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
304 |
lemma inj_bij_range: "f \<in> inj(A,B) \<Longrightarrow> f \<in> bij(A,range(f))" |
46821
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
305 |
by (auto simp add: bij_def intro: inj_inj_range inj_is_fun fun_is_surj) |
41160
be34449f6cba
Added two theorems about the concept of range. Tidied up the comments.
paulson
parents:
32960
diff
changeset
|
306 |
|
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
307 |
|
60770 | 308 |
subsection\<open>Other Results\<close> |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
309 |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
310 |
lemma comp_mono: "\<lbrakk>r'<=r; s'<=s\<rbrakk> \<Longrightarrow> (r' O s') \<subseteq> (r O s)" |
13180 | 311 |
by blast |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
312 |
|
60770 | 313 |
text\<open>composition preserves relations\<close> |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
314 |
lemma comp_rel: "\<lbrakk>s<=A*B; r<=B*C\<rbrakk> \<Longrightarrow> (r O s) \<subseteq> A*C" |
13180 | 315 |
by blast |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
316 |
|
60770 | 317 |
text\<open>associative law for composition\<close> |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
318 |
lemma comp_assoc: "(r O s) O t = r O (s O t)" |
13180 | 319 |
by blast |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
320 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
321 |
(*left identity of composition; provable inclusions are |
46821
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
322 |
id(A) O r \<subseteq> r |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
323 |
and \<lbrakk>r<=A*B; B<=C\<rbrakk> \<Longrightarrow> r \<subseteq> id(C) O r *) |
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
324 |
lemma left_comp_id: "r<=A*B \<Longrightarrow> id(B) O r = r" |
13180 | 325 |
by blast |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
326 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
327 |
(*right identity of composition; provable inclusions are |
46820 | 328 |
r O id(A) \<subseteq> r |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
329 |
and \<lbrakk>r<=A*B; A<=C\<rbrakk> \<Longrightarrow> r \<subseteq> r O id(C) *) |
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
330 |
lemma right_comp_id: "r<=A*B \<Longrightarrow> r O id(A) = r" |
13180 | 331 |
by blast |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
332 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
333 |
|
60770 | 334 |
subsection\<open>Composition Preserves Functions, Injections, and Surjections\<close> |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
335 |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
336 |
lemma comp_function: "\<lbrakk>function(g); function(f)\<rbrakk> \<Longrightarrow> function(f O g)" |
13180 | 337 |
by (unfold function_def, blast) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
338 |
|
60770 | 339 |
text\<open>Don't think the premises can be weakened much\<close> |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
340 |
lemma comp_fun: "\<lbrakk>g \<in> A->B; f \<in> B->C\<rbrakk> \<Longrightarrow> (f O g) \<in> A->C" |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
341 |
apply (auto simp add: Pi_def comp_function Pow_iff comp_rel) |
46821
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
342 |
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
|
343 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
344 |
|
46953 | 345 |
(*Thanks to the new definition of "apply", the premise f \<in> B->C is gone!*) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
346 |
lemma comp_fun_apply [simp]: |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
347 |
"\<lbrakk>g \<in> A->B; a \<in> A\<rbrakk> \<Longrightarrow> (f O g)`a = f`(g`a)" |
46821
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
348 |
apply (frule apply_Pair, assumption) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
349 |
apply (simp add: apply_def image_comp) |
46821
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
350 |
apply (blast dest: apply_equality) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
351 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
352 |
|
60770 | 353 |
text\<open>Simplifies compositions of lambda-abstractions\<close> |
46821
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
354 |
lemma comp_lam: |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
355 |
"\<lbrakk>\<And>x. x \<in> A \<Longrightarrow> b(x): B\<rbrakk> |
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
356 |
\<Longrightarrow> (\<lambda>y\<in>B. c(y)) O (\<lambda>x\<in>A. b(x)) = (\<lambda>x\<in>A. c(b(x)))" |
46821
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
357 |
apply (subgoal_tac "(\<lambda>x\<in>A. b(x)) \<in> A -> B") |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
358 |
apply (rule fun_extension) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
359 |
apply (blast intro: comp_fun lam_funtype) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
360 |
apply (rule lam_funtype) |
46821
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
361 |
apply simp |
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
362 |
apply (simp add: lam_type) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
363 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
364 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
365 |
lemma comp_inj: |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
366 |
"\<lbrakk>g \<in> inj(A,B); f \<in> inj(B,C)\<rbrakk> \<Longrightarrow> (f O g) \<in> inj(A,C)" |
46821
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
367 |
apply (frule inj_is_fun [of g]) |
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
368 |
apply (frule inj_is_fun [of f]) |
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
369 |
apply (rule_tac d = "\<lambda>y. converse (g) ` (converse (f) ` y)" in f_imp_injective) |
46821
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
370 |
apply (blast intro: comp_fun, simp) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
371 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
372 |
|
46821
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
373 |
lemma comp_surj: |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
374 |
"\<lbrakk>g \<in> surj(A,B); f \<in> surj(B,C)\<rbrakk> \<Longrightarrow> (f O g) \<in> surj(A,C)" |
76216
9fc34f76b4e8
getting rid of apply (unfold ...)
paulson <lp15@cam.ac.uk>
parents:
76215
diff
changeset
|
375 |
unfolding surj_def |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
376 |
apply (blast intro!: comp_fun comp_fun_apply) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
377 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
378 |
|
46821
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
379 |
lemma comp_bij: |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
380 |
"\<lbrakk>g \<in> bij(A,B); f \<in> bij(B,C)\<rbrakk> \<Longrightarrow> (f O g) \<in> bij(A,C)" |
76216
9fc34f76b4e8
getting rid of apply (unfold ...)
paulson <lp15@cam.ac.uk>
parents:
76215
diff
changeset
|
381 |
unfolding bij_def |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
382 |
apply (blast intro: comp_inj comp_surj) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
383 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
384 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
385 |
|
69593 | 386 |
subsection\<open>Dual Properties of \<^term>\<open>inj\<close> and \<^term>\<open>surj\<close>\<close> |
13356 | 387 |
|
60770 | 388 |
text\<open>Useful for proofs from |
46821
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
389 |
D Pastre. Automatic theorem proving in set theory. |
60770 | 390 |
Artificial Intelligence, 10:1--27, 1978.\<close> |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
391 |
|
46821
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
392 |
lemma comp_mem_injD1: |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
393 |
"\<lbrakk>(f O g): inj(A,C); g \<in> A->B; f \<in> B->C\<rbrakk> \<Longrightarrow> g \<in> inj(A,B)" |
46821
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
394 |
by (unfold inj_def, force) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
395 |
|
46821
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
396 |
lemma comp_mem_injD2: |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
397 |
"\<lbrakk>(f O g): inj(A,C); g \<in> surj(A,B); f \<in> B->C\<rbrakk> \<Longrightarrow> f \<in> inj(B,C)" |
13180 | 398 |
apply (unfold inj_def surj_def, safe) |
13784 | 399 |
apply (rule_tac x1 = x in bspec [THEN bexE]) |
400 |
apply (erule_tac [3] x1 = w in bspec [THEN bexE], assumption+, safe) |
|
67399 | 401 |
apply (rule_tac t = "(`) (g) " in subst_context) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
402 |
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
|
403 |
apply (simp (no_asm_simp)) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
404 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
405 |
|
46821
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
406 |
lemma comp_mem_surjD1: |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
407 |
"\<lbrakk>(f O g): surj(A,C); g \<in> A->B; f \<in> B->C\<rbrakk> \<Longrightarrow> f \<in> surj(B,C)" |
76216
9fc34f76b4e8
getting rid of apply (unfold ...)
paulson <lp15@cam.ac.uk>
parents:
76215
diff
changeset
|
408 |
unfolding surj_def |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
409 |
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
|
410 |
done |
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 |
|
46821
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
413 |
lemma comp_mem_surjD2: |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
414 |
"\<lbrakk>(f O g): surj(A,C); g \<in> A->B; f \<in> inj(B,C)\<rbrakk> \<Longrightarrow> g \<in> surj(A,B)" |
13180 | 415 |
apply (unfold inj_def surj_def, safe) |
46821
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
416 |
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
|
417 |
apply (blast intro: apply_funtype) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
418 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
419 |
|
60770 | 420 |
subsubsection\<open>Inverses of Composition\<close> |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
421 |
|
60770 | 422 |
text\<open>left inverse of composition; one inclusion is |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
423 |
\<^term>\<open>f \<in> A->B \<Longrightarrow> id(A) \<subseteq> converse(f) O f\<close>\<close> |
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
424 |
lemma left_comp_inverse: "f \<in> inj(A,B) \<Longrightarrow> converse(f) O f = id(A)" |
46821
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
425 |
apply (unfold inj_def, clarify) |
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
426 |
apply (rule equalityI) |
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
427 |
apply (auto simp add: apply_iff, blast) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
428 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
429 |
|
60770 | 430 |
text\<open>right inverse of composition; one inclusion is |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
431 |
\<^term>\<open>f \<in> A->B \<Longrightarrow> f O converse(f) \<subseteq> id(B)\<close>\<close> |
46821
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
432 |
lemma right_comp_inverse: |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
433 |
"f \<in> surj(A,B) \<Longrightarrow> f O converse(f) = id(B)" |
46821
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
434 |
apply (simp add: surj_def, clarify) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
435 |
apply (rule equalityI) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
436 |
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
|
437 |
apply (blast intro: apply_Pair) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
438 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
439 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
440 |
|
60770 | 441 |
subsubsection\<open>Proving that a Function is a Bijection\<close> |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
442 |
|
46821
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
443 |
lemma comp_eq_id_iff: |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
444 |
"\<lbrakk>f \<in> A->B; g \<in> B->A\<rbrakk> \<Longrightarrow> f O g = id(B) \<longleftrightarrow> (\<forall>y\<in>B. f`(g`y)=y)" |
13180 | 445 |
apply (unfold id_def, safe) |
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
446 |
apply (drule_tac t = "\<lambda>h. h`y " in subst_context) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
447 |
apply simp |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
448 |
apply (rule fun_extension) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
449 |
apply (blast intro: comp_fun lam_type) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
450 |
apply auto |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
451 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
452 |
|
46821
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
453 |
lemma fg_imp_bijective: |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
454 |
"\<lbrakk>f \<in> A->B; g \<in> B->A; f O g = id(B); g O f = id(A)\<rbrakk> \<Longrightarrow> f \<in> bij(A,B)" |
76216
9fc34f76b4e8
getting rid of apply (unfold ...)
paulson <lp15@cam.ac.uk>
parents:
76215
diff
changeset
|
455 |
unfolding bij_def |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
456 |
apply (simp add: comp_eq_id_iff) |
13180 | 457 |
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
|
458 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
459 |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
460 |
lemma nilpotent_imp_bijective: "\<lbrakk>f \<in> A->A; f O f = id(A)\<rbrakk> \<Longrightarrow> f \<in> bij(A,A)" |
13180 | 461 |
by (blast intro: fg_imp_bijective) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
462 |
|
13180 | 463 |
lemma invertible_imp_bijective: |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
464 |
"\<lbrakk>converse(f): B->A; f \<in> A->B\<rbrakk> \<Longrightarrow> f \<in> bij(A,B)" |
46821
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
465 |
by (simp add: fg_imp_bijective comp_eq_id_iff |
13180 | 466 |
left_inverse_lemma right_inverse_lemma) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
467 |
|
60770 | 468 |
subsubsection\<open>Unions of Functions\<close> |
13356 | 469 |
|
60770 | 470 |
text\<open>See similar theorems in func.thy\<close> |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
471 |
|
60770 | 472 |
text\<open>Theorem by KG, proof by LCP\<close> |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
473 |
lemma inj_disjoint_Un: |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
474 |
"\<lbrakk>f \<in> inj(A,B); g \<in> inj(C,D); B \<inter> D = 0\<rbrakk> |
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
475 |
\<Longrightarrow> (\<lambda>a\<in>A \<union> C. if a \<in> A then f`a else g`a) \<in> inj(A \<union> C, B \<union> D)" |
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
476 |
apply (rule_tac d = "\<lambda>z. if z \<in> B then converse (f) `z else converse (g) `z" |
13180 | 477 |
in lam_injective) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
478 |
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
|
479 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
480 |
|
46821
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
481 |
lemma surj_disjoint_Un: |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
482 |
"\<lbrakk>f \<in> surj(A,B); g \<in> surj(C,D); A \<inter> C = 0\<rbrakk> |
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
483 |
\<Longrightarrow> (f \<union> g) \<in> surj(A \<union> C, B \<union> D)" |
46821
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
484 |
apply (simp add: surj_def fun_disjoint_Un) |
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
485 |
apply (blast dest!: domain_of_fun |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
24893
diff
changeset
|
486 |
intro!: fun_disjoint_apply1 fun_disjoint_apply2) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
487 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
488 |
|
60770 | 489 |
text\<open>A simple, high-level proof; the version for injections follows from it, |
69593 | 490 |
using \<^term>\<open>f \<in> inj(A,B) \<longleftrightarrow> f \<in> bij(A,range(f))\<close>\<close> |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
491 |
lemma bij_disjoint_Un: |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
492 |
"\<lbrakk>f \<in> bij(A,B); g \<in> bij(C,D); A \<inter> C = 0; B \<inter> D = 0\<rbrakk> |
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
493 |
\<Longrightarrow> (f \<union> g) \<in> bij(A \<union> C, B \<union> D)" |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
494 |
apply (rule invertible_imp_bijective) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
495 |
apply (subst converse_Un) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
496 |
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
|
497 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
498 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
499 |
|
60770 | 500 |
subsubsection\<open>Restrictions as Surjections and Bijections\<close> |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
501 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
502 |
lemma surj_image: |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
503 |
"f \<in> Pi(A,B) \<Longrightarrow> f \<in> surj(A, f``A)" |
46821
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
504 |
apply (simp add: surj_def) |
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
505 |
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
|
506 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
507 |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
508 |
lemma surj_image_eq: "f \<in> surj(A, B) \<Longrightarrow> f``A = B" |
47101 | 509 |
by (auto simp add: surj_def image_fun) (blast dest: apply_type) |
510 |
||
46820 | 511 |
lemma restrict_image [simp]: "restrict(f,A) `` B = f `` (A \<inter> B)" |
13180 | 512 |
by (auto simp add: restrict_def) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
513 |
|
46821
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
514 |
lemma restrict_inj: |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
515 |
"\<lbrakk>f \<in> inj(A,B); C<=A\<rbrakk> \<Longrightarrow> restrict(f,C): inj(C,B)" |
76216
9fc34f76b4e8
getting rid of apply (unfold ...)
paulson <lp15@cam.ac.uk>
parents:
76215
diff
changeset
|
516 |
unfolding inj_def |
46821
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
517 |
apply (safe elim!: restrict_type2, auto) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
518 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
519 |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
520 |
lemma restrict_surj: "\<lbrakk>f \<in> Pi(A,B); C<=A\<rbrakk> \<Longrightarrow> restrict(f,C): surj(C, f``C)" |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
521 |
apply (insert restrict_type2 [THEN surj_image]) |
46821
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
522 |
apply (simp add: restrict_image) |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
523 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
524 |
|
46821
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
525 |
lemma restrict_bij: |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
526 |
"\<lbrakk>f \<in> inj(A,B); C<=A\<rbrakk> \<Longrightarrow> restrict(f,C): bij(C, f``C)" |
13180 | 527 |
apply (simp add: inj_def bij_def) |
528 |
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
|
529 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
530 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
531 |
|
60770 | 532 |
subsubsection\<open>Lemmas for Ramsey's Theorem\<close> |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
533 |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
534 |
lemma inj_weaken_type: "\<lbrakk>f \<in> inj(A,B); B<=D\<rbrakk> \<Longrightarrow> f \<in> inj(A,D)" |
76216
9fc34f76b4e8
getting rid of apply (unfold ...)
paulson <lp15@cam.ac.uk>
parents:
76215
diff
changeset
|
535 |
unfolding inj_def |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
536 |
apply (blast intro: fun_weaken_type) |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
537 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
538 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
539 |
lemma inj_succ_restrict: |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
540 |
"\<lbrakk>f \<in> inj(succ(m), A)\<rbrakk> \<Longrightarrow> restrict(f,m) \<in> inj(m, A-{f`m})" |
13269 | 541 |
apply (rule restrict_bij [THEN bij_is_inj, THEN inj_weaken_type], assumption, blast) |
76216
9fc34f76b4e8
getting rid of apply (unfold ...)
paulson <lp15@cam.ac.uk>
parents:
76215
diff
changeset
|
542 |
unfolding inj_def |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
543 |
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
|
544 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
545 |
|
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
546 |
|
46821
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
547 |
lemma inj_extend: |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset
|
548 |
"\<lbrakk>f \<in> inj(A,B); a\<notin>A; b\<notin>B\<rbrakk> |
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76214
diff
changeset
|
549 |
\<Longrightarrow> cons(\<langle>a,b\<rangle>,f) \<in> inj(cons(a,A), cons(b,B))" |
76216
9fc34f76b4e8
getting rid of apply (unfold ...)
paulson <lp15@cam.ac.uk>
parents:
76215
diff
changeset
|
550 |
unfolding inj_def |
13176
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
551 |
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
|
552 |
done |
312bd350579b
conversion of Perm to Isar. Strengthening of comp_fun_apply
paulson
parents:
9570
diff
changeset
|
553 |
|
0 | 554 |
end |