5250
|
1 |
(* Title: HOL/ex/PiSets.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Florian Kammueller, University of Cambridge
|
|
4 |
|
|
5 |
Pi sets and their application.
|
|
6 |
*)
|
|
7 |
|
5845
|
8 |
(*** -> and Pi ***)
|
5250
|
9 |
|
|
10 |
|
5845
|
11 |
val prems = Goalw [Pi_def]
|
|
12 |
"[| !!x. x: A ==> f x: B x; !!x. x ~: A ==> f(x) = (@ y. True)|] \
|
|
13 |
\ ==> f: Pi A B";
|
|
14 |
by (auto_tac (claset(), simpset() addsimps prems));
|
|
15 |
qed "Pi_I";
|
|
16 |
|
|
17 |
val prems = Goal
|
|
18 |
"[| !!x. x: A ==> f x: B; !!x. x ~: A ==> f(x) = (@ y. True)|] ==> f: A -> B";
|
|
19 |
by (blast_tac (claset() addIs Pi_I::prems) 1);
|
|
20 |
qed "funcsetI";
|
5250
|
21 |
|
5845
|
22 |
Goalw [Pi_def] "[|f: Pi A B; x: A|] ==> f x: B x";
|
|
23 |
by Auto_tac;
|
|
24 |
qed "Pi_mem";
|
|
25 |
|
|
26 |
Goalw [Pi_def] "[|f: A -> B; x: A|] ==> f x: B";
|
|
27 |
by Auto_tac;
|
|
28 |
qed "funcset_mem";
|
|
29 |
|
|
30 |
Goalw [Pi_def] "[|f: Pi A B; x~: A|] ==> f x = (@ y. True)";
|
|
31 |
by Auto_tac;
|
|
32 |
qed "apply_arb";
|
5250
|
33 |
|
5845
|
34 |
Goalw [Pi_def] "[| f: Pi A B; g: Pi A B; ! x: A. f x = g x |] ==> f = g";
|
|
35 |
by (rtac ext 1);
|
|
36 |
by Auto_tac;
|
|
37 |
val Pi_extensionality = ballI RSN (3, result());
|
5250
|
38 |
|
5845
|
39 |
(*** compose ***)
|
|
40 |
|
|
41 |
Goalw [Pi_def, compose_def, restrict_def]
|
|
42 |
"[| f: A -> B; g: B -> C |]==> compose A g f: A -> C";
|
|
43 |
by Auto_tac;
|
|
44 |
qed "funcset_compose";
|
5250
|
45 |
|
5845
|
46 |
Goal "[| f: A -> B; g: B -> C; h: C -> D |]\
|
|
47 |
\ ==> compose A h (compose A g f) = compose A (compose B h g) f";
|
|
48 |
by (res_inst_tac [("A","A")] Pi_extensionality 1);
|
|
49 |
by (blast_tac (claset() addIs [funcset_compose]) 1);
|
|
50 |
by (blast_tac (claset() addIs [funcset_compose]) 1);
|
|
51 |
by (rewrite_goals_tac [Pi_def, compose_def, restrict_def]);
|
|
52 |
by Auto_tac;
|
|
53 |
qed "compose_assoc";
|
5250
|
54 |
|
5845
|
55 |
Goal "[| f: A -> B; g: B -> C; x: A |]==> compose A g f x = g(f(x))";
|
|
56 |
by (asm_full_simp_tac (simpset() addsimps [compose_def, restrict_def]) 1);
|
|
57 |
qed "compose_eq";
|
5250
|
58 |
|
5845
|
59 |
Goal "[| f : A -> B; f `` A = B; g: B -> C; g `` B = C |]\
|
|
60 |
\ ==> compose A g f `` A = C";
|
|
61 |
by (auto_tac (claset(),
|
|
62 |
simpset() addsimps [image_def, compose_eq]));
|
|
63 |
qed "surj_compose";
|
5250
|
64 |
|
|
65 |
|
5845
|
66 |
Goal "[| f : A -> B; g: B -> C; f `` A = B; inj_on f A; inj_on g B |]\
|
|
67 |
\ ==> inj_on (compose A g f) A";
|
|
68 |
by (auto_tac (claset(),
|
|
69 |
simpset() addsimps [inj_on_def, compose_eq]));
|
|
70 |
qed "inj_on_compose";
|
5250
|
71 |
|
|
72 |
|
5845
|
73 |
(*** restrict / lam ***)
|
|
74 |
Goal "[| f `` A <= B |] ==> (lam x: A. f x) : A -> B";
|
|
75 |
by (auto_tac (claset(),
|
|
76 |
simpset() addsimps [restrict_def, Pi_def]));
|
|
77 |
qed "restrict_in_funcset";
|
|
78 |
|
|
79 |
val prems = Goalw [restrict_def, Pi_def]
|
|
80 |
"(!!x. x: A ==> f x: B x) ==> (lam x: A. f x) : Pi A B";
|
|
81 |
by (asm_simp_tac (simpset() addsimps prems) 1);
|
|
82 |
qed "restrictI";
|
5250
|
83 |
|
|
84 |
|
5845
|
85 |
Goal "x: A ==> (lam y: A. f y) x = f x";
|
|
86 |
by (asm_simp_tac (simpset() addsimps [restrict_def]) 1);
|
|
87 |
qed "restrict_apply1";
|
5250
|
88 |
|
5845
|
89 |
Goal "[| x: A; f : A -> B |] ==> (lam y: A. f y) x : B";
|
|
90 |
by (asm_full_simp_tac (simpset() addsimps [restrict_apply1,Pi_def]) 1);
|
|
91 |
qed "restrict_apply1_mem";
|
5250
|
92 |
|
5845
|
93 |
Goal "x ~: A ==> (lam y: A. f y) x = (@ y. True)";
|
|
94 |
by (asm_simp_tac (simpset() addsimps [restrict_def]) 1);
|
|
95 |
qed "restrict_apply2";
|
5250
|
96 |
|
|
97 |
|
5845
|
98 |
val prems = Goal
|
|
99 |
"(!!x. x: A ==> f x = g x) ==> (lam x: A. f x) = (lam x: A. g x)";
|
|
100 |
by (rtac ext 1);
|
|
101 |
by (auto_tac (claset(),
|
|
102 |
simpset() addsimps prems@[restrict_def, Pi_def]));
|
|
103 |
qed "restrict_ext";
|
5250
|
104 |
|
|
105 |
|
5845
|
106 |
(*** Inverse ***)
|
5250
|
107 |
|
5845
|
108 |
Goal "[|f `` A = B; x: B |] ==> ? y: A. f y = x";
|
|
109 |
by (Blast_tac 1);
|
|
110 |
qed "surj_image";
|
5250
|
111 |
|
5845
|
112 |
Goalw [Inv_def] "[| f `` A = B; f : A -> B |] \
|
|
113 |
\ ==> (lam x: B. (Inv A f) x) : B -> A";
|
|
114 |
by (fast_tac (claset() addIs [restrict_in_funcset, selectI2]) 1);
|
|
115 |
qed "Inv_funcset";
|
5250
|
116 |
|
|
117 |
|
5845
|
118 |
Goal "[| f: A -> B; inj_on f A; f `` A = B; x: A |] \
|
|
119 |
\ ==> (lam y: B. (Inv A f) y) (f x) = x";
|
|
120 |
by (asm_simp_tac (simpset() addsimps [restrict_apply1, funcset_mem]) 1);
|
|
121 |
by (asm_full_simp_tac (simpset() addsimps [Inv_def, inj_on_def]) 1);
|
|
122 |
by (rtac selectI2 1);
|
|
123 |
by Auto_tac;
|
|
124 |
qed "Inv_f_f";
|
5250
|
125 |
|
5845
|
126 |
Goal "[| f: A -> B; f `` A = B; x: B |] \
|
|
127 |
\ ==> f ((lam y: B. (Inv A f y)) x) = x";
|
|
128 |
by (asm_simp_tac (simpset() addsimps [Inv_def, restrict_apply1]) 1);
|
|
129 |
by (fast_tac (claset() addIs [selectI2]) 1);
|
|
130 |
qed "f_Inv_f";
|
5250
|
131 |
|
5845
|
132 |
Goal "[| f: A -> B; inj_on f A; f `` A = B |]\
|
|
133 |
\ ==> compose A (lam y:B. (Inv A f) y) f = (lam x: A. x)";
|
|
134 |
by (rtac Pi_extensionality 1);
|
|
135 |
by (blast_tac (claset() addIs [funcset_compose, Inv_funcset]) 1);
|
|
136 |
by (blast_tac (claset() addIs [restrict_in_funcset]) 1);
|
|
137 |
by (asm_simp_tac
|
|
138 |
(simpset() addsimps [restrict_apply1, compose_def, Inv_f_f]) 1);
|
|
139 |
qed "compose_Inv_id";
|
5250
|
140 |
|
|
141 |
|
5845
|
142 |
(*** Pi and its application @@ ***)
|
5250
|
143 |
|
5845
|
144 |
Goalw [Pi_def] "[| B(x) = {}; x: A |] ==> (PI x: A. B x) = {}";
|
|
145 |
by Auto_tac;
|
|
146 |
qed "Pi_eq_empty";
|
5250
|
147 |
|
5845
|
148 |
Goal "[| (PI x: A. B x) ~= {}; x: A |] ==> B(x) ~= {}";
|
|
149 |
by (blast_tac (HOL_cs addIs [Pi_eq_empty]) 1);
|
|
150 |
qed "Pi_total1";
|
5250
|
151 |
|
5845
|
152 |
Goal "[| a : A; Pi A B ~= {} |] ==> (Pi A B) @@ a = B(a)";
|
|
153 |
by (auto_tac (claset(), simpset() addsimps [Fset_apply_def, Pi_def]));
|
|
154 |
by (rename_tac "g z" 1);
|
|
155 |
by (res_inst_tac [("x","%y. if (y = a) then z else g y")] exI 1);
|
|
156 |
by (auto_tac (claset(), simpset() addsimps [split_if_mem1, split_if_eq1]));
|
|
157 |
qed "Fset_beta";
|
|
158 |
|
5250
|
159 |
|
5845
|
160 |
(*** Bijection between Pi in terms of => and Pi in terms of Sigma ***)
|
|
161 |
Goal "f: Pi A B ==> PiBij A B f <= Sigma A B";
|
|
162 |
by (auto_tac (claset(),
|
|
163 |
simpset() addsimps [PiBij_def,Pi_def,restrict_apply1]));
|
|
164 |
qed "PiBij_subset_Sigma";
|
5250
|
165 |
|
5845
|
166 |
Goal "f: Pi A B ==> (! x: A. (?! y. (x, y): (PiBij A B f)))";
|
|
167 |
by (auto_tac (claset(),
|
|
168 |
simpset() addsimps [PiBij_def,restrict_apply1]));
|
|
169 |
qed "PiBij_unique";
|
5250
|
170 |
|
5845
|
171 |
Goal "f: Pi A B ==> PiBij A B f : Graph A B";
|
|
172 |
by (asm_simp_tac (simpset() addsimps [Graph_def,PiBij_unique,
|
|
173 |
PiBij_subset_Sigma]) 1);
|
|
174 |
qed "PiBij_in_Graph";
|
5250
|
175 |
|
5845
|
176 |
Goalw [PiBij_def, Graph_def] "PiBij A B: Pi A B -> Graph A B";
|
5318
|
177 |
by (rtac restrictI 1);
|
5845
|
178 |
by (auto_tac (claset(), simpset() addsimps [Pi_def]));
|
|
179 |
qed "PiBij_func";
|
5250
|
180 |
|
5845
|
181 |
Goal "inj_on (PiBij A B) (Pi A B)";
|
5318
|
182 |
by (rtac inj_onI 1);
|
|
183 |
by (rtac Pi_extensionality 1);
|
|
184 |
by (assume_tac 1);
|
|
185 |
by (assume_tac 1);
|
5845
|
186 |
by (rotate_tac 1 1);
|
|
187 |
by (asm_full_simp_tac (simpset() addsimps [PiBij_def,restrict_apply1]) 1);
|
|
188 |
by (blast_tac (claset() addEs [equalityE]) 1);
|
|
189 |
qed "inj_PiBij";
|
5250
|
190 |
|
5845
|
191 |
|
5250
|
192 |
|
5845
|
193 |
Goal "PiBij A B `` (Pi A B) = Graph A B";
|
5318
|
194 |
by (rtac equalityI 1);
|
5521
|
195 |
by (force_tac (claset(), simpset() addsimps [image_def,PiBij_in_Graph]) 1);
|
5318
|
196 |
by (rtac subsetI 1);
|
5845
|
197 |
by (asm_full_simp_tac (simpset() addsimps [image_def]) 1);
|
5250
|
198 |
by (res_inst_tac [("x","lam a: A. @ y. (a, y): x")] bexI 1);
|
5845
|
199 |
by (rtac restrictI 2);
|
|
200 |
by (res_inst_tac [("P", "%xa. (a, xa) : x")] ex1E 2);
|
|
201 |
by (force_tac (claset(), simpset() addsimps [Graph_def]) 2);
|
|
202 |
by (full_simp_tac (simpset() addsimps [Graph_def]) 2);
|
|
203 |
by (stac select_equality 2);
|
5521
|
204 |
by (assume_tac 2);
|
|
205 |
by (Blast_tac 2);
|
|
206 |
by (Blast_tac 2);
|
5250
|
207 |
(* x = PiBij A B (lam a:A. @ y. (a, y) : x) *)
|
5845
|
208 |
by (full_simp_tac (simpset() addsimps [PiBij_def,Graph_def]) 1);
|
|
209 |
by (stac restrict_apply1 1);
|
|
210 |
by (rtac restrictI 1);
|
|
211 |
by (blast_tac (claset() addSDs [[select_eq_Ex, ex1_implies_ex] MRS iffD2]) 1);
|
|
212 |
(** LEVEL 17 **)
|
5318
|
213 |
by (rtac equalityI 1);
|
|
214 |
by (rtac subsetI 1);
|
5845
|
215 |
by (split_all_tac 1);
|
|
216 |
by (subgoal_tac "a: A" 1);
|
|
217 |
by (Blast_tac 2);
|
|
218 |
by (asm_full_simp_tac (simpset() addsimps [restrict_apply1]) 1);
|
|
219 |
(*Blast_tac: PROOF FAILED for depth 5*)
|
|
220 |
by (fast_tac (claset() addSIs [select1_equality RS sym]) 1);
|
5250
|
221 |
(* {(xa,y). xa : A & y = (lam a:A. @ y. (a, y) : x) xa} <= x *)
|
5845
|
222 |
by (Clarify_tac 1);
|
|
223 |
by (asm_full_simp_tac (simpset() addsimps [restrict_apply1]) 1);
|
|
224 |
by (fast_tac (claset() addIs [selectI2]) 1);
|
|
225 |
qed "surj_PiBij";
|
5250
|
226 |
|
5845
|
227 |
Goal "f: Pi A B ==> \
|
|
228 |
\ (lam y: Graph A B. (Inv (Pi A B)(PiBij A B)) y)(PiBij A B f) = f";
|
|
229 |
by (asm_simp_tac
|
|
230 |
(simpset() addsimps [Inv_f_f, PiBij_func, inj_PiBij, surj_PiBij]) 1);
|
|
231 |
qed "PiBij_bij1";
|
5250
|
232 |
|
5845
|
233 |
Goal "[| f: Graph A B |] ==> \
|
5250
|
234 |
\ (PiBij A B) ((lam y: (Graph A B). (Inv (Pi A B)(PiBij A B)) y) f) = f";
|
5845
|
235 |
by (rtac (PiBij_func RS f_Inv_f) 1);
|
|
236 |
by (asm_full_simp_tac (simpset() addsimps [surj_PiBij]) 1);
|
5318
|
237 |
by (assume_tac 1);
|
5845
|
238 |
qed "PiBij_bij2";
|
5250
|
239 |
|
5845
|
240 |
Goal "Pi {} B = {f. !x. f x = (@ y. True)}";
|
|
241 |
by (asm_full_simp_tac (simpset() addsimps [Pi_def]) 1);
|
|
242 |
qed "empty_Pi";
|
5250
|
243 |
|
5845
|
244 |
Goal "(% x. (@ y. True)) : Pi {} B";
|
|
245 |
by (simp_tac (simpset() addsimps [empty_Pi]) 1);
|
|
246 |
qed "empty_Pi_func";
|
5250
|
247 |
|
5845
|
248 |
val [major] = Goalw [Pi_def] "(!!x. x: A ==> B x <= C x) ==> Pi A B <= Pi A C";
|
|
249 |
by (auto_tac (claset(),
|
|
250 |
simpset() addsimps [impOfSubs major]));
|
|
251 |
qed "Pi_mono";
|