author | nipkow |
Sat, 08 Aug 1998 14:00:56 +0200 | |
changeset 5281 | f4d16517b360 |
parent 5148 | 74919e8f221c |
child 5305 | 513925de8962 |
permissions | -rw-r--r-- |
1465 | 1 |
(* Title: HOL/Fun |
923 | 2 |
ID: $Id$ |
1465 | 3 |
Author: Tobias Nipkow, Cambridge University Computer Laboratory |
923 | 4 |
Copyright 1993 University of Cambridge |
5 |
||
6 |
Lemmas about functions. |
|
7 |
*) |
|
8 |
||
4656 | 9 |
|
5069 | 10 |
Goal "(f = g) = (!x. f(x)=g(x))"; |
923 | 11 |
by (rtac iffI 1); |
1264 | 12 |
by (Asm_simp_tac 1); |
13 |
by (rtac ext 1 THEN Asm_simp_tac 1); |
|
923 | 14 |
qed "expand_fun_eq"; |
15 |
||
4656 | 16 |
val prems = goal thy |
923 | 17 |
"[| f(x)=u; !!x. P(x) ==> g(f(x)) = x; P(x) |] ==> x=g(u)"; |
18 |
by (rtac (arg_cong RS box_equals) 1); |
|
19 |
by (REPEAT (resolve_tac (prems@[refl]) 1)); |
|
20 |
qed "apply_inverse"; |
|
21 |
||
22 |
||
4656 | 23 |
(** "Axiom" of Choice, proved using the description operator **) |
24 |
||
25 |
goal HOL.thy "!!Q. ALL x. EX y. Q x y ==> EX f. ALL x. Q x (f x)"; |
|
26 |
by (fast_tac (claset() addEs [selectI]) 1); |
|
27 |
qed "choice"; |
|
28 |
||
29 |
goal Set.thy "!!S. ALL x:S. EX y. Q x y ==> EX f. ALL x:S. Q x (f x)"; |
|
30 |
by (fast_tac (claset() addEs [selectI]) 1); |
|
31 |
qed "bchoice"; |
|
32 |
||
33 |
||
923 | 34 |
(*** inj(f): f is a one-to-one function ***) |
35 |
||
4656 | 36 |
val prems = goalw thy [inj_def] |
923 | 37 |
"[| !! x y. f(x) = f(y) ==> x=y |] ==> inj(f)"; |
4089 | 38 |
by (blast_tac (claset() addIs prems) 1); |
923 | 39 |
qed "injI"; |
40 |
||
4656 | 41 |
val [major] = goal thy "(!!x. g(f(x)) = x) ==> inj(f)"; |
923 | 42 |
by (rtac injI 1); |
43 |
by (etac (arg_cong RS box_equals) 1); |
|
44 |
by (rtac major 1); |
|
45 |
by (rtac major 1); |
|
46 |
qed "inj_inverseI"; |
|
47 |
||
4656 | 48 |
val [major,minor] = goalw thy [inj_def] |
923 | 49 |
"[| inj(f); f(x) = f(y) |] ==> x=y"; |
50 |
by (rtac (major RS spec RS spec RS mp) 1); |
|
51 |
by (rtac minor 1); |
|
52 |
qed "injD"; |
|
53 |
||
54 |
(*Useful with the simplifier*) |
|
4656 | 55 |
val [major] = goal thy "inj(f) ==> (f(x) = f(y)) = (x=y)"; |
923 | 56 |
by (rtac iffI 1); |
57 |
by (etac (major RS injD) 1); |
|
58 |
by (etac arg_cong 1); |
|
59 |
qed "inj_eq"; |
|
60 |
||
4656 | 61 |
val [major] = goal thy "inj(f) ==> (@x. f(x)=f(y)) = y"; |
923 | 62 |
by (rtac (major RS injD) 1); |
63 |
by (rtac selectI 1); |
|
64 |
by (rtac refl 1); |
|
65 |
qed "inj_select"; |
|
66 |
||
67 |
(*A one-to-one function has an inverse (given using select).*) |
|
4656 | 68 |
val [major] = goalw thy [inv_def] "inj(f) ==> inv f (f x) = x"; |
923 | 69 |
by (EVERY1 [rtac (major RS inj_select)]); |
2912 | 70 |
qed "inv_f_f"; |
923 | 71 |
|
72 |
(* Useful??? *) |
|
4656 | 73 |
val [oneone,minor] = goal thy |
2912 | 74 |
"[| inj(f); !!y. y: range(f) ==> P(inv f y) |] ==> P(x)"; |
75 |
by (res_inst_tac [("t", "x")] (oneone RS (inv_f_f RS subst)) 1); |
|
923 | 76 |
by (rtac (rangeI RS minor) 1); |
77 |
qed "inj_transfer"; |
|
78 |
||
79 |
||
4830 | 80 |
(*** inj_on f A: f is one-to-one over A ***) |
923 | 81 |
|
4830 | 82 |
val prems = goalw thy [inj_on_def] |
83 |
"(!! x y. [| f(x) = f(y); x:A; y:A |] ==> x=y) ==> inj_on f A"; |
|
4089 | 84 |
by (blast_tac (claset() addIs prems) 1); |
4830 | 85 |
qed "inj_onI"; |
923 | 86 |
|
4656 | 87 |
val [major] = goal thy |
4830 | 88 |
"(!!x. x:A ==> g(f(x)) = x) ==> inj_on f A"; |
89 |
by (rtac inj_onI 1); |
|
923 | 90 |
by (etac (apply_inverse RS trans) 1); |
91 |
by (REPEAT (eresolve_tac [asm_rl,major] 1)); |
|
4830 | 92 |
qed "inj_on_inverseI"; |
923 | 93 |
|
4830 | 94 |
val major::prems = goalw thy [inj_on_def] |
95 |
"[| inj_on f A; f(x)=f(y); x:A; y:A |] ==> x=y"; |
|
923 | 96 |
by (rtac (major RS bspec RS bspec RS mp) 1); |
97 |
by (REPEAT (resolve_tac prems 1)); |
|
4830 | 98 |
qed "inj_onD"; |
923 | 99 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
100 |
Goal "[| inj_on f A; x:A; y:A |] ==> (f(x)=f(y)) = (x=y)"; |
4830 | 101 |
by (blast_tac (claset() addSDs [inj_onD]) 1); |
102 |
qed "inj_on_iff"; |
|
923 | 103 |
|
4656 | 104 |
val major::prems = goal thy |
4830 | 105 |
"[| inj_on f A; ~x=y; x:A; y:A |] ==> ~ f(x)=f(y)"; |
923 | 106 |
by (rtac contrapos 1); |
4830 | 107 |
by (etac (major RS inj_onD) 2); |
923 | 108 |
by (REPEAT (resolve_tac prems 1)); |
4830 | 109 |
qed "inj_on_contraD"; |
923 | 110 |
|
5069 | 111 |
Goalw [inj_on_def] |
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset
|
112 |
"[| A<=B; inj_on f B |] ==> inj_on f A"; |
3341 | 113 |
by (Blast_tac 1); |
4830 | 114 |
qed "subset_inj_on"; |
3341 | 115 |
|
923 | 116 |
|
117 |
(*** Lemmas about inj ***) |
|
118 |
||
5069 | 119 |
Goalw [o_def] |
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset
|
120 |
"[| inj(f); inj_on g (range f) |] ==> inj(g o f)"; |
4830 | 121 |
by (fast_tac (claset() addIs [injI] addEs [injD, inj_onD]) 1); |
923 | 122 |
qed "comp_inj"; |
123 |
||
4830 | 124 |
val [prem] = goal thy "inj(f) ==> inj_on f A"; |
125 |
by (blast_tac (claset() addIs [prem RS injD, inj_onI]) 1); |
|
923 | 126 |
qed "inj_imp"; |
127 |
||
4656 | 128 |
val [prem] = goalw thy [inv_def] "y : range(f) ==> f(inv f y) = y"; |
923 | 129 |
by (EVERY1 [rtac (prem RS rangeE), rtac selectI, etac sym]); |
2912 | 130 |
qed "f_inv_f"; |
923 | 131 |
|
4656 | 132 |
val prems = goal thy |
2912 | 133 |
"[| inv f x=inv f y; x: range(f); y: range(f) |] ==> x=y"; |
134 |
by (rtac (arg_cong RS box_equals) 1); |
|
135 |
by (REPEAT (resolve_tac (prems @ [f_inv_f]) 1)); |
|
136 |
qed "inv_injective"; |
|
137 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
138 |
Goal "[| inj(f); A<=range(f) |] ==> inj_on (inv f) A"; |
4830 | 139 |
by (fast_tac (claset() addIs [inj_onI] |
2912 | 140 |
addEs [inv_injective,injD]) 1); |
4830 | 141 |
qed "inj_on_inv"; |
923 | 142 |
|
5069 | 143 |
Goalw [inj_on_def] |
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset
|
144 |
"[| inj_on f C; A<=C; B<=C |] ==> f``(A Int B) = f``A Int f``B"; |
4059 | 145 |
by (Blast_tac 1); |
4830 | 146 |
qed "inj_on_image_Int"; |
4059 | 147 |
|
5069 | 148 |
Goalw [inj_on_def] |
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset
|
149 |
"[| inj_on f C; A<=C; B<=C |] ==> f``(A-B) = f``A - f``B"; |
4059 | 150 |
by (Blast_tac 1); |
4830 | 151 |
qed "inj_on_image_set_diff"; |
4059 | 152 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
153 |
Goalw [inj_def] "inj f ==> f``(A Int B) = f``A Int f``B"; |
4059 | 154 |
by (Blast_tac 1); |
155 |
qed "image_Int"; |
|
156 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
157 |
Goalw [inj_def] "inj f ==> f``(A-B) = f``A - f``B"; |
4059 | 158 |
by (Blast_tac 1); |
159 |
qed "image_set_diff"; |
|
160 |
||
923 | 161 |
|
4089 | 162 |
val set_cs = claset() delrules [equalityI]; |