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 


8 
(* One abbreviation for my major simp application *)


9 
fun afs thms = (asm_full_simp_tac (simpset() addsimps thms));


10 
(* strip outer quantifiers and lift implication *)


11 
fun strip i = (REPEAT ((rtac ballI i)


12 
ORELSE (rtac allI i)


13 
ORELSE (rtac impI i)));


14 
(* eresolve but leave the eliminated assumptions (improves unification) *)


15 
goal HOL.thy "!! P. [ P ] ==> P & P";


16 
by (Fast_tac 1);


17 
val double = result();


18 


19 
fun re_tac rule r i = ((rotate_tac (r  1) i)


20 
THEN (dtac double i)


21 
THEN (rotate_tac ~1 i)


22 
THEN (etac conjE i)


23 
THEN (rotate_tac ~1 i)


24 
THEN (etac rule i));


25 


26 
(* individual theorems for convenient use *)


27 
val [p1,p2] = goal HOL.thy "[P == Q; P] ==> Q";


28 
by (fold_goals_tac [p1]);

5318

29 
by (rtac p2 1);

5250

30 
val apply_def = result();


31 


32 
goal HOL.thy "!! P x y. x = y ==> P(x) = P(y)";

5318

33 
by (etac ssubst 1);


34 
by (rtac refl 1);

5250

35 
val extend = result();


36 


37 
val [p1] = goal HOL.thy "P ==> ~~P";

5318

38 
by (rtac notI 1);


39 
by (rtac (p1 RSN(2, notE)) 1);


40 
by (assume_tac 1);

5250

41 
val notnotI = result();


42 


43 
val [p1] = goal Set.thy "? x. x: S ==> S ~= {}";

5318

44 
by (rtac contrapos 1);


45 
by (rtac (p1 RS notnotI) 1);


46 
by (etac ssubst 1);


47 
by (rtac notI 1);


48 
by (etac exE 1);


49 
by (etac emptyE 1);

5250

50 
val ExEl_NotEmpty = result();


51 


52 


53 
val [p1] = goal HOL.thy "~x ==> x = False";


54 
val l1 = (p1 RS (not_def RS apply_def)) RS mp;


55 
val l2 = read_instantiate [("P","x")] FalseE;

5318

56 
by (rtac iffI 1);


57 
by (rtac l1 1);


58 
by (rtac l2 2);


59 
by (assume_tac 1);


60 
by (assume_tac 1);

5250

61 
val NoteqFalseEq = result();


62 


63 
val [p1] = goal HOL.thy "~ (! x. ~P(x)) ==> ? x. P(x)";

5318

64 
by (rtac exCI 1);

5250

65 
(* 1. ! x. ~ P x ==> P ?a *)


66 
val l1 = p1 RS NoteqFalseEq;


67 
(* l1 = (! x. ~ P x) = False *)


68 
val l2 = l1 RS iffD1;


69 
val l3 = l1 RS iffD2;


70 
val l4 = read_instantiate [("P", "P ?a")] FalseE;

5318

71 
by (rtac (l2 RS l4) 1);


72 
by (assume_tac 1);

5250

73 
val NotAllNot_Ex = result();


74 


75 
val [p1] = goal HOL.thy "~(? x. P(x)) ==> ! x. ~ P(x)";

5318

76 
by (rtac notnotD 1);


77 
by (rtac (p1 RS contrapos) 1);


78 
by (rtac NotAllNot_Ex 1);


79 
by (assume_tac 1);

5250

80 
val NotEx_AllNot = result();


81 


82 
goal Set.thy "!!S. ~ (? x. x : S) ==> S = {}";


83 
by (Fast_tac 1);


84 
val NoEl_Empty = result();


85 


86 
goal Set.thy "!!S. S ~= {} ==> ? x. x : S";


87 
by (Fast_tac 1);


88 
val NotEmpty_ExEl = result();


89 


90 
goal PiSets.thy "!!S. S = {} ==> ! x. x ~: S";


91 
by (Fast_tac 1);


92 
val Empty_NoElem = result();


93 


94 


95 
val [q1,q2] = goal HOL.thy "[ b = a ; (P a) ] ==> (P b)";

5318

96 
by (stac q1 1);


97 
by (rtac q2 1);

5250

98 
val forw_subst = result();


99 


100 
val [q1,q2] = goal HOL.thy "[ a = b ; (P a) ] ==> (P b)";

5318

101 
by (rtac (q1 RS subst) 1);


102 
by (rtac q2 1);

5250

103 
val forw_ssubst = result();


104 


105 
goal Prod.thy "((fst A),(fst(snd A)),(fst (snd (snd A))),(snd(snd(snd A)))) = A";

5318

106 
by (rtac (surjective_pairing RS subst) 1);


107 
by (rtac (surjective_pairing RS subst) 1);


108 
by (rtac (surjective_pairing RS subst) 1);


109 
by (rtac refl 1);

5250

110 
val blow4 = result();


111 


112 
goal Prod.thy "!! P a b. (%(a,b). P a b) A ==> P (fst A)(snd A)";


113 
by (Step_tac 1);


114 
by (afs [fst_conv,snd_conv] 1);


115 
val apply_pair = result();


116 


117 
goal Prod.thy "!! P a b c d. (%(a,b,c,d). P a b c d) A \


118 
\ ==> P (fst A)(fst(snd A))(fst (snd (snd A)))(snd(snd(snd A)))";

5318

119 
by (dtac (blow4 RS forw_subst) 1);

5250

120 
by (afs [split_def] 1);


121 
val apply_quadr = result();


122 


123 
goal Prod.thy "!! A B x. x: A Times B ==> x = (fst x, snd x)";

5318

124 
by (rtac (surjective_pairing RS subst) 1);


125 
by (rtac refl 1);

5250

126 
val surj_pair_forw = result();


127 


128 
goal Prod.thy "!! A B x. x: A Times B ==> fst x: A";


129 
by (forward_tac [surj_pair_forw] 1);

5318

130 
by (dtac forw_ssubst 1);


131 
by (assume_tac 1);


132 
by (etac SigmaD1 1);

5250

133 
val TimesE1 = result();


134 


135 
goal Prod.thy "!! A B x. x: A Times B ==> snd x: B";


136 
by (forward_tac [surj_pair_forw] 1);

5318

137 
by (dtac forw_ssubst 1);


138 
by (assume_tac 1);


139 
by (etac SigmaD2 1);

5250

140 
val TimesE2 = result();


141 


142 
(* > and Pi *)


143 


144 
goal PiSets.thy "!! A B. A > B == {f. ! x. if x: A then f(x) : B else f(x) = (@ y. True)}";


145 
by (simp_tac (simpset() addsimps [Pi_def]) 1);


146 
val funcset_def = result();


147 


148 


149 
val [q1,q2] = goal PiSets.thy


150 
"[ !!x. x: A ==> f x: B x; !!x. x ~: A ==> f(x) = (@ y. True)] ==> f: Pi A B";

5318

151 
by (rewtac Pi_def);


152 
by (rtac CollectI 1);


153 
by (rtac allI 1);

5250

154 
by (case_tac "x : A" 1);

5318

155 
by (stac if_P 1);


156 
by (assume_tac 1);


157 
by (etac q1 1);


158 
by (stac if_not_P 1);


159 
by (assume_tac 1);


160 
by (etac q2 1);

5250

161 
val Pi_I = result();


162 


163 
goal PiSets.thy


164 
"!! A f. [ !!x. x: A ==> f x: B; !!x. x ~: A ==> f(x) = (@ y. True)] ==> f: A > B";


165 
by (afs [Pi_I] 1);


166 
val funcsetI = result();


167 


168 
val [q1,q2,q3] = goal PiSets.thy


169 
"[ !! x y. [ x: A; y: B ] ==> f x y: C; \


170 
\ !! x. [ x ~: A ] ==> f x = (@ y. True);\


171 
\ !! x y. [ x : A; y ~: B ] ==> f x y = (@ y. True) ] ==> f: A > B > C";


172 
by (simp_tac (simpset() addsimps [q1,q2,q3,funcsetI]) 1);


173 
val funcsetI2 = result();


174 


175 
goal PiSets.thy "!! f A B. [f: A > B; x: A] ==> f x: B";


176 
by (afs [funcset_def] 1);


177 
val funcsetE1 = result();


178 


179 
goal PiSets.thy "!! f A B. [f: Pi A B; x: A] ==> f x: B x";


180 
by (afs [Pi_def] 1);


181 
val PiE1 = result();


182 


183 
goal PiSets.thy "!! f A B. [f: A > B; x~: A] ==> f x = (@ y. True)";


184 
by (afs [funcset_def] 1);


185 
val funcsetE2 = result();


186 


187 
goal PiSets.thy "!! f A B. [f: Pi A B; x~: A] ==> f x = (@ y. True)";


188 
by (afs [Pi_def] 1);


189 
val PiE2 = result();


190 


191 
goal PiSets.thy "!! f A B. [f: A > B > C; x : A; y ~: B] ==> f x y = (@ y. True)";


192 
by (afs [funcset_def] 1);


193 
val funcset2E2 = result();


194 


195 


196 
goal PiSets.thy "!! f A B C. [ f: A > B > C; x: A; y: B ] ==> f x y: C";


197 
by (afs [funcset_def] 1);


198 
val funcset2E1 = result();


199 


200 
goal PiSets.thy "!! f g A B. [ f: A > B; g: A > B; ! x: A. f x = g x ]\


201 
\ ==> f = g";

5318

202 
by (rtac ext 1);

5250

203 
by (case_tac "x : A" 1);


204 
by (Fast_tac 1);


205 
by (fast_tac (claset() addSDs [funcsetE2] addEs [ssubst]) 1);


206 
val function_extensionality = result();


207 


208 
goal PiSets.thy "!! f g A B. [ f: Pi A B; g: Pi A B; ! x: A. f x = g x ]\


209 
\ ==> f = g";

5318

210 
by (rtac ext 1);

5250

211 
by (case_tac "x : A" 1);


212 
by (Fast_tac 1);


213 
by (fast_tac (claset() addSDs [PiE2] addEs [ssubst]) 1);


214 
val Pi_extensionality = result();


215 


216 
(* compose *)


217 
goal PiSets.thy "!! A B C f g. [ f: A > B; g: B > C ]==> compose A g f: A > C";

5318

218 
by (rtac funcsetI 1);

5250

219 
by (rewrite_goals_tac [compose_def,restrict_def]);


220 
by (afs [funcsetE1] 1);

5318

221 
by (stac if_not_P 1);


222 
by (assume_tac 1);


223 
by (rtac refl 1);

5250

224 
val funcset_compose = result();


225 


226 
goal PiSets.thy "!! A B C f g h. [ f: A > B; g: B > C; h: C > D ]\


227 
\ ==> compose A h (compose A g f) = compose A (compose B h g) f";


228 
by (res_inst_tac [("A","A")] function_extensionality 1);

5318

229 
by (rtac funcset_compose 1);


230 
by (rtac funcset_compose 1);


231 
by (assume_tac 1);


232 
by (assume_tac 1);


233 
by (assume_tac 1);


234 
by (rtac funcset_compose 1);


235 
by (assume_tac 1);


236 
by (rtac funcset_compose 1);


237 
by (assume_tac 1);


238 
by (assume_tac 1);


239 
by (rtac ballI 1);

5250

240 
by (rewrite_goals_tac [compose_def,restrict_def]);


241 
by (afs [funcsetE1,if_P RS ssubst] 1);


242 
val compose_assoc = result();


243 


244 
goal PiSets.thy "!! A B C f g x. [ f: A > B; g: B > C; x: A ]==> compose A g f x = g(f(x))";


245 
by (afs [compose_def, restrict_def, if_P RS ssubst] 1);


246 
val composeE1 = result();


247 


248 
goal PiSets.thy "!! A B C g f.[ f : A > B; f `` A = B; g: B > C; g `` B = C ]\


249 
\ ==> compose A g f `` A = C";

5318

250 
by (rtac equalityI 1);


251 
by (rtac subsetI 1);


252 
by (etac imageE 1);

5250

253 
by (rotate_tac 4 1);

5318

254 
by (etac ssubst 1);


255 
by (rtac (funcset_compose RS funcsetE1) 1);


256 
by (assume_tac 1);


257 
by (assume_tac 1);


258 
by (assume_tac 1);


259 
by (rtac subsetI 1);

5250

260 
by (hyp_subst_tac 1);

5318

261 
by (etac imageE 1);

5250

262 
by (rotate_tac 3 1);

5318

263 
by (etac ssubst 1);


264 
by (etac imageE 1);

5250

265 
by (rotate_tac 3 1);

5318

266 
by (etac ssubst 1);


267 
by (etac (composeE1 RS subst) 1);


268 
by (assume_tac 1);


269 
by (assume_tac 1);


270 
by (rtac imageI 1);


271 
by (assume_tac 1);

5250

272 
val surj_compose = result();


273 


274 


275 
goal PiSets.thy "!! A B C g f.[ f : A > B; g: B > C; f `` A = B; inj_on f A; inj_on g B ]\


276 
\ ==> inj_on (compose A g f) A";

5318

277 
by (rtac inj_onI 1);

5250

278 
by (forward_tac [composeE1] 1);

5318

279 
by (assume_tac 1);


280 
by (assume_tac 1);

5250

281 
by (forward_tac [composeE1] 1);

5318

282 
by (assume_tac 1);

5250

283 
by (rotate_tac 7 1);

5318

284 
by (assume_tac 1);

5250

285 
by (step_tac (claset() addSEs [inj_onD]) 1);


286 
by (rotate_tac 5 1);

5318

287 
by (etac subst 1);


288 
by (etac subst 1);


289 
by (assume_tac 1);


290 
by (etac imageI 1);


291 
by (etac imageI 1);

5250

292 
val inj_on_compose = result();


293 


294 


295 
(* restrict / lam *)


296 
goal PiSets.thy "!! f A B. [ f `` A <= B ] ==> (lam x: A. f x) : A > B";

5318

297 
by (rewtac restrict_def);


298 
by (rtac funcsetI 1);

5250

299 
by (afs [if_P RS ssubst] 1);

5318

300 
by (etac subsetD 1);


301 
by (etac imageI 1);

5250

302 
by (afs [if_not_P RS ssubst] 1);


303 
val restrict_in_funcset = result();


304 


305 
goal PiSets.thy "!! f A B. [ ! x: A. f x: B ] ==> (lam x: A. f x) : A > B";

5318

306 
by (rtac restrict_in_funcset 1);

5250

307 
by (afs [image_def] 1);


308 
by (Step_tac 1);


309 
by (Fast_tac 1);


310 
val restrictI = result();


311 


312 
goal PiSets.thy "!! f A B. [ ! x: A. f x: B x ] ==> (lam x: A. f x) : Pi A B";

5318

313 
by (rewtac restrict_def);


314 
by (rtac Pi_I 1);

5250

315 
by (afs [if_P RS ssubst] 1);


316 
by (Asm_full_simp_tac 1);


317 
val restrictI_Pi = result();


318 


319 
(* The following proof has to be redone *)


320 
goal PiSets.thy "!! f A B C.[ f `` A <= B > C ] ==> (lam x: A. lam y: B. f x y) : A > B > C";

5318

321 
by (rtac restrict_in_funcset 1);

5250

322 
by (afs [image_def] 1);


323 
by (afs [Pi_def,subset_def] 1);


324 
by (afs [restrict_def] 1);


325 
by (Step_tac 1);


326 
by (Asm_full_simp_tac 1);


327 
by (dres_inst_tac [("x","f xa")] spec 1);

5318

328 
by (dtac mp 1);


329 
by (rtac bexI 1);


330 
by (rtac refl 1);


331 
by (assume_tac 1);

5250

332 
by (dres_inst_tac [("x","xb")] spec 1);


333 
by (Asm_full_simp_tac 1);


334 
(* fini 1 *)


335 
by (Asm_full_simp_tac 1);


336 
val restrict_in_funcset2 = result();


337 


338 
goal PiSets.thy "!! f A B C.[ !x: A. ! y: B. f x y: C ] ==> (lam x: A. lam y: B. f x y) : A > B > C";

5318

339 
by (rtac restrict_in_funcset 1);

5250

340 
by (afs [image_def] 1);


341 
by (afs [Pi_def,subset_def] 1);


342 
by (afs [restrict_def] 1);


343 
by (Step_tac 1);


344 
by (Asm_full_simp_tac 1);


345 
by (Asm_full_simp_tac 1);


346 
val restrictI2 = result();


347 


348 


349 
(* goal PiSets.thy "!! f A B. [ f `` A <= UNION A B ] ==> (lam x: A. f x) : Pi A B"; *)


350 


351 
goal PiSets.thy "!! f A B. [ x: A ] ==> (lam y: A. f y) x = f x";


352 
by (afs [restrict_def] 1);


353 
val restrictE1 = result();


354 


355 
goal PiSets.thy "!! f A B. [ x: A; f : A > B ] ==> (lam y: A. f y) x : B";


356 
by (afs [restrictE1,funcsetE1] 1);


357 
val restrictE1a = result();


358 


359 
goal PiSets.thy "!! f A B. [ x ~: A ] ==> (lam y: A. f y) x = (@ y. True)";


360 
by (afs [restrict_def] 1);


361 
val restrictE2 = result();


362 


363 
(* It would be nice to have this, but this doesn't work unfortunately


364 
see PiSets.ML: Pi_subset1


365 
goal PiSets.thy "!! A B. [ A <= B ; ! x: A. f x : C] ==> (lam x: B. f(x)): A > C"; *)


366 


367 
goal PiSets.thy "!! f A B x y. [ x: A; y: B ] ==> \


368 
\ (lam a: A. lam b: B. f a b) x y = f x y";


369 
by (afs [restrictE1] 1);


370 
val restrict2E1 = result();


371 


372 
(* New restrict2E1: *)


373 
goal PiSets.thy "!! A B. [ x : A; y : B x] ==> (lam a:A. lam b: (B a). f a b) x y = f x y" ;


374 
by (afs [restrictE1] 1);


375 
val restrict2E1a = result();


376 


377 
goal PiSets.thy "!! f A B x y. [ x: A; y: B; z: C ] ==> \


378 
\ (lam a: A. lam b: B. lam c: C. f a b c) x y z = f x y z";


379 
by (afs [restrictE1] 1);


380 
val restrict3E1 = result();


381 


382 
goal PiSets.thy "!! f A B x y. [ x: A; y ~: B ] ==> \


383 
\ (lam a: A. lam b: B. f a b) x y = (@ y. True)";


384 
by (afs [restrictE1,restrictE2] 1);


385 
val restrict2E2 = result();


386 


387 


388 
goal PiSets.thy "!! f g A B. [ ! x: A. f x = g x ]\


389 
\ ==> (lam x: A. f x) = (lam x: A. g x)";

5318

390 
by (rtac ext 1);

5250

391 
by (case_tac "x: A" 1);


392 
by (afs [restrictE1] 1);


393 
by (afs [restrictE2] 1);


394 
val restrict_ext = result();


395 


396 
(* Invers *)


397 


398 
goal PiSets.thy "!! f A B.[f `` A = B; x: B ] ==> ? y: A. f y = x";

5318

399 
by (rewtac image_def);


400 
by (dtac equalityD2 1);


401 
by (dtac subsetD 1);


402 
by (assume_tac 1);


403 
by (dtac CollectD 1);


404 
by (etac bexE 1);


405 
by (dtac sym 1);


406 
by (etac bexI 1);


407 
by (assume_tac 1);

5250

408 
val surj_image = result();


409 


410 
val [q1,q2] = goal PiSets.thy "[ f `` A = B; f : A > B ] \


411 
\ ==> (lam x: B. (Inv A f) x) : B > A";

5318

412 
by (rtac restrict_in_funcset 1);


413 
by (rewtac image_def);


414 
by (rtac subsetI 1);


415 
by (dtac CollectD 1);


416 
by (etac bexE 1);


417 
by (etac ssubst 1);


418 
by (dtac (q1 RS surj_image) 1);


419 
by (etac bexE 1);


420 
by (etac subst 1);


421 
by (rewtac Inv_def);

5250

422 
by (res_inst_tac [("Q","f(@ ya. ya : A & f ya = f y) = f y")] conjunct1 1);

5318

423 
by (rtac (q1 RS surj_image RS (Bex_def RS apply_def) RS (Ex_def RS apply_def)) 1);


424 
by (etac (q2 RS funcsetE1) 1);

5250

425 
val Inv_funcset = result();


426 


427 


428 
val [q1,q2,q3] = goal PiSets.thy "[ f: A > B; inj_on f A; f `` A = B ]\


429 
\ ==> ! x: A. (lam y: B. (Inv A f) y)(f x) = x";

5318

430 
by (rtac ballI 1);


431 
by (stac restrictE1 1);


432 
by (etac (q1 RS funcsetE1) 1);


433 
by (rewtac Inv_def);


434 
by (rtac (q2 RS inj_onD) 1);


435 
by (assume_tac 3);

5250

436 
by (res_inst_tac [("P","(@ y. y : A & f y = f x) : A")] conjunct2 1);

5318

437 
by (rtac (q3 RS surj_image RS (Bex_def RS apply_def) RS (Ex_def RS apply_def)) 1);


438 
by (etac (q1 RS funcsetE1) 1);

5250

439 
by (res_inst_tac [("Q","f (@ y. y : A & f y = f x) = f x")] conjunct1 1);

5318

440 
by (rtac (q3 RS surj_image RS (Bex_def RS apply_def) RS (Ex_def RS apply_def)) 1);


441 
by (etac (q1 RS funcsetE1) 1);

5250

442 
val Inv_f_f = result();


443 


444 
val [q1,q2] = goal PiSets.thy "[ f: A > B; f `` A = B ]\


445 
\ ==> ! x: B. f ((lam y: B. (Inv A f y)) x) = x";

5318

446 
by (rtac ballI 1);


447 
by (stac restrictE1 1);


448 
by (assume_tac 1);


449 
by (rewtac Inv_def);

5250

450 
by (res_inst_tac [("P","(@ y. y : A & f y = x) : A")] conjunct2 1);

5318

451 
by (rtac (q2 RS surj_image RS (Bex_def RS apply_def) RS (Ex_def RS apply_def)) 1);


452 
by (assume_tac 1);

5250

453 
val f_Inv_f = result();


454 


455 
val [q1,q2,q3] = goal PiSets.thy "[ f: A > B; inj_on f A; f `` A = B ]\


456 
\ ==> compose A (lam y:B. (Inv A f) y) f = (lam x: A. x)";

5318

457 
by (rtac function_extensionality 1);


458 
by (rtac funcset_compose 1);


459 
by (rtac q1 1);


460 
by (rtac (q1 RS (q3 RS Inv_funcset)) 1);


461 
by (rtac restrict_in_funcset 1);

5250

462 
by (Fast_tac 1);

5318

463 
by (rtac ballI 1);

5250

464 
by (afs [compose_def] 1);

5318

465 
by (stac restrictE1 1);


466 
by (assume_tac 1);


467 
by (stac restrictE1 1);


468 
by (assume_tac 1);


469 
by (etac (q3 RS (q2 RS (q1 RS Inv_f_f)) RS bspec) 1);

5250

470 
val comp_Inv_id = result();


471 


472 


473 
(* Pi and its application @@ *)


474 


475 
goal PiSets.thy "!! A B. (PI x: A. B x) ~= {} ==> ! x: A. B(x) ~= {}";

5318

476 
by (dtac NotEmpty_ExEl 1);


477 
by (etac exE 1);


478 
by (rewtac Pi_def);


479 
by (dtac CollectD 1);


480 
by (rtac ballI 1);


481 
by (rtac ExEl_NotEmpty 1);

5250

482 
by (res_inst_tac [("x","x xa")] exI 1);


483 
by (afs [if_P RS subst] 1);


484 
val Pi_total1 = result();


485 


486 
goal Set.thy "!! M P. ? x: M . P x ==> (~ (! x: M. ~ P x))";


487 
by (Fast_tac 1);


488 
val SetEx_NotNotAll = result();


489 


490 
goal PiSets.thy "!! A B. ? x: A. B(x) = {} ==> (PI x: A. B x) = {}";

5318

491 
by (rtac notnotD 1);


492 
by (rtac (Pi_total1 RSN(2,contrapos)) 1);


493 
by (assume_tac 2);


494 
by (etac SetEx_NotNotAll 1);

5250

495 
val Pi_total2 = result();


496 


497 
val [q1,q2] = goal PiSets.thy "[a : A; Pi A B ~= {} ] ==> (Pi A B) @@ a = B(a)";

5318

498 
by (rewtac Fset_apply_def);


499 
by (rtac equalityI 1);


500 
by (rtac subsetI 1);


501 
by (etac imageE 1);


502 
by (etac ssubst 1);


503 
by (rewtac Pi_def);


504 
by (dtac CollectD 1);


505 
by (dtac spec 1);


506 
by (rtac (q1 RS if_P RS subst) 1);


507 
by (assume_tac 1);


508 
by (rtac subsetI 1);


509 
by (rewtac image_def);


510 
by (rtac CollectI 1);


511 
by (rtac exE 1);


512 
by (rtac (q2 RS NotEmpty_ExEl) 1);

5250

513 
by (res_inst_tac [("x","%y. if (y = a) then x else xa y")] bexI 1);


514 
by (Simp_tac 1);


515 
by (Simp_tac 1);

5318

516 
by (rtac allI 1);

5250

517 
by (case_tac "xb: A" 1);


518 
by (afs [if_P RS ssubst] 1);


519 
by (case_tac "xb = a" 1);


520 
by (afs [if_P RS ssubst] 1);


521 
by (afs [if_not_P RS ssubst] 1);

5318

522 
by (rewtac Pi_def);

5250

523 
by (afs [if_P RS ssubst] 1);


524 
by (afs [if_not_P RS ssubst] 1);


525 
by (case_tac "xb = a" 1);


526 
by (afs [if_P RS ssubst] 1);


527 
by (hyp_subst_tac 1);


528 
by (afs [q1] 1);


529 
by (afs [if_not_P RS ssubst] 1);


530 
val Pi_app_def = result();


531 


532 
goal PiSets.thy "!! a A B C. [ a: A; (PI x: A. PI y: B x. C x y) ~= {} ] ==> (PI y: B a. C a y) ~= {}";

5318

533 
by (dtac NotEmpty_ExEl 1);


534 
by (etac exE 1);


535 
by (rewtac Pi_def);


536 
by (dtac CollectD 1);


537 
by (dtac spec 1);


538 
by (rtac ExEl_NotEmpty 1);


539 
by (rtac exI 1);


540 
by (etac (if_P RS eq_reflection RS apply_def) 1);


541 
by (assume_tac 1);

5250

542 
val NotEmptyPiStep = result();


543 


544 
val [q1,q2,q3] = goal PiSets.thy


545 
"[a : A; b: B a; (PI x: A. PI y: B x. C x y) ~= {} ] ==> (PI x: A. PI y: B x. C x y) @@ a @@ b = C a b";


546 
by (fold_goals_tac [q3 RS (q1 RS NotEmptyPiStep) RS (q2 RS Pi_app_def) RS eq_reflection]);


547 
by (fold_goals_tac [q3 RS (q1 RS Pi_app_def) RS eq_reflection]);

5318

548 
by (rtac refl 1);

5250

549 
val Pi_app2_def = result();


550 


551 
(* Sigma does a better job ( the following is from PiSig.ML) *)


552 
goal PiSets.thy "!! A b a. [ a: A; Pi A B ~= {} ]\


553 
\ ==> Sigma A B ^^ {a} = Pi A B @@ a";

5318

554 
by (stac Pi_app_def 1);


555 
by (assume_tac 1);


556 
by (assume_tac 1);

5250

557 
by (afs [Sigma_def,Domain_def,converse_def,Range_def,Image_def] 1);

5318

558 
by (rewtac Bex_def);

5250

559 
by (Fast_tac 1);


560 
val PiSig_image_eq = result();


561 


562 
goal PiSets.thy "!! A b a. [ a: A ]\


563 
\ ==> Sigma A B ^^ {a} = B a";


564 
by (Fast_tac 1);


565 
val Sigma_app_def = result();


566 


567 
(* Bijection between Pi in terms of => and Pi in terms of Sigma *)


568 
goal PiSets.thy "!! f. f: Pi A B ==> PiBij A B f <= Sigma A B";


569 
by (afs [PiBij_def,Pi_def,restrictE1] 1);

5318

570 
by (rtac subsetI 1);

5250

571 
by (split_all_tac 1);

5318

572 
by (dtac CollectD 1);

5250

573 
by (Asm_full_simp_tac 1);


574 
val PiBij_subset_Sigma = result();


575 


576 
goal PiSets.thy "!! f. f: Pi A B ==> (! x: A. (?! y. (x, y): (PiBij A B f)))";


577 
by (afs [PiBij_def,restrictE1] 1);

5318

578 
by (rtac ballI 1);


579 
by (rtac ex1I 1);


580 
by (assume_tac 2);


581 
by (rtac refl 1);

5250

582 
val PiBij_unique = result();


583 


584 
goal PiSets.thy "!! f. f: Pi A B ==> (! x: A. (?! y. y: B x & (x, y): (PiBij A B f)))";


585 
by (afs [PiBij_def,restrictE1] 1);

5318

586 
by (rtac ballI 1);


587 
by (rtac ex1I 1);


588 
by (etac conjunct2 2);

5250

589 
by (afs [PiE1] 1);


590 
val PiBij_unique2 = result();


591 


592 
goal PiSets.thy "!! f. f: Pi A B ==> PiBij A B f : Graph A B";


593 
by (afs [Graph_def,PiBij_unique,PiBij_subset_Sigma] 1);


594 
val PiBij_in_Graph = result();


595 


596 
goal PiSets.thy "!! A B. PiBij A B: Pi A B > Graph A B";


597 
by (afs [PiBij_def] 1);

5318

598 
by (rtac restrictI 1);

5250

599 
by (strip 1);


600 
by (afs [Graph_def] 1);

5318

601 
by (rtac conjI 1);


602 
by (rtac subsetI 1);

5250

603 
by (strip 2);

5318

604 
by (rtac ex1I 2);


605 
by (rtac refl 2);


606 
by (assume_tac 2);

5250

607 
by (split_all_tac 1);


608 
by (afs [Pi_def] 1);


609 
val PiBij_func = result();


610 


611 
goal PiSets.thy "!! A f g x. [ f: Pi A B; g: Pi A B; \


612 
\ {(x, y). x: A & y = f x} = {(x, y). x: A & y = g x}; x: A ]\


613 
\ ==> f x = g x";

5318

614 
by (etac equalityE 1);


615 
by (rewtac subset_def);

5250

616 
by (dres_inst_tac [("x","(x, f x)")] bspec 1);


617 
by (Fast_tac 1);


618 
by (Fast_tac 1);


619 
val set_eq_lemma = result();


620 


621 
goal PiSets.thy "!! A B. inj_on (PiBij A B) (Pi A B)";

5318

622 
by (rtac inj_onI 1);


623 
by (rtac Pi_extensionality 1);


624 
by (assume_tac 1);


625 
by (assume_tac 1);

5250

626 
by (strip 1);


627 
by (afs [PiBij_def,restrictE1] 1);


628 
by (re_tac set_eq_lemma 2 1);

5318

629 
by (assume_tac 1);


630 
by (assume_tac 2);

5250

631 
by (afs [restrictE1] 1);

5318

632 
by (etac subst 1);

5250

633 
by (afs [restrictE1] 1);


634 
val inj_PiBij = result();


635 


636 
goal HOL.thy "!! P . ?! x. P x ==> ? x. P x";


637 
by (Blast_tac 1);


638 
val Ex1_Ex = result();


639 


640 
goal PiSets.thy "!!A B. PiBij A B `` (Pi A B) = Graph A B";

5318

641 
by (rtac equalityI 1);

5250

642 
by (afs [image_def] 1);

5318

643 
by (rtac subsetI 1);

5250

644 
by (Asm_full_simp_tac 1);

5318

645 
by (etac bexE 1);


646 
by (etac ssubst 1);

5250

647 
by (afs [PiBij_in_Graph] 1);

5318

648 
by (rtac subsetI 1);

5250

649 
by (afs [image_def] 1);


650 
by (res_inst_tac [("x","lam a: A. @ y. (a, y): x")] bexI 1);

5318

651 
by (rtac restrictI_Pi 2);

5250

652 
by (strip 2);

5318

653 
by (rtac ex1E 2);

5250

654 
by (afs [Graph_def] 2);

5318

655 
by (etac conjE 2);


656 
by (dtac bspec 2);


657 
by (assume_tac 2);


658 
by (assume_tac 2);


659 
by (stac select_equality 2);


660 
by (assume_tac 2);

5250

661 
by (Blast_tac 2);


662 
(* gets hung up on by (afs [Graph_def] 2); *)

5318

663 
by (SELECT_GOAL (rewtac Graph_def) 2);

5250

664 
by (Blast_tac 2);


665 
(* x = PiBij A B (lam a:A. @ y. (a, y) : x) *)


666 
by (afs [PiBij_def,Graph_def] 1);

5318

667 
by (stac restrictE1 1);


668 
by (rtac restrictI_Pi 1);

5250

669 
(* again like the old 2. subgoal *)


670 
by (strip 1);

5318

671 
by (rtac ex1E 1);


672 
by (etac conjE 1);


673 
by (dtac bspec 1);


674 
by (assume_tac 1);


675 
by (assume_tac 1);


676 
by (stac select_equality 1);


677 
by (assume_tac 1);

5250

678 
by (Blast_tac 1);


679 
by (Blast_tac 1);


680 
(* *)

5318

681 
by (rtac equalityI 1);


682 
by (rtac subsetI 1);


683 
by (rtac CollectI 1);

5250

684 
by (split_all_tac 1);


685 
by (Simp_tac 1);

5318

686 
by (rtac conjI 1);

5250

687 
by (Blast_tac 1);

5318

688 
by (etac conjE 1);


689 
by (dtac subsetD 1);


690 
by (assume_tac 1);


691 
by (dtac SigmaD1 1);


692 
by (dtac bspec 1);


693 
by (assume_tac 1);


694 
by (stac restrictE1 1);


695 
by (assume_tac 1);


696 
by (rtac sym 1);


697 
by (rtac select_equality 1);


698 
by (assume_tac 1);

5250

699 
by (Blast_tac 1);


700 
(* {(xa,y). xa : A & y = (lam a:A. @ y. (a, y) : x) xa} <= x *)

5318

701 
by (rtac subsetI 1);

5250

702 
by (Asm_full_simp_tac 1);


703 
by (split_all_tac 1);


704 
by (Asm_full_simp_tac 1);

5318

705 
by (etac conjE 1);


706 
by (etac conjE 1);

5250

707 
by (afs [restrictE1] 1);

5318

708 
by (dtac bspec 1);


709 
by (assume_tac 1);


710 
by (dtac Ex1_Ex 1);


711 
by (rewtac Ex_def);


712 
by (assume_tac 1);

5250

713 
val surj_PiBij = result();


714 


715 


716 
goal PiSets.thy "!! A B. [ f: Pi A B ] ==> \


717 
\ (lam y: Graph A B. (Inv (Pi A B)(PiBij A B)) y)(PiBij A B f) = f";

5318

718 
by (rtac (Inv_f_f RS bspec) 1);


719 
by (assume_tac 4);

5250

720 
by (afs [PiBij_func] 1);


721 
by (afs [inj_PiBij] 1);


722 
by (afs [surj_PiBij] 1);


723 
val PiBij_bij1 = result();


724 


725 
goal PiSets.thy "!! A B. [ f: Graph A B ] ==> \


726 
\ (PiBij A B) ((lam y: (Graph A B). (Inv (Pi A B)(PiBij A B)) y) f) = f";

5318

727 
by (rtac (PiBij_func RS (f_Inv_f RS bspec)) 1);

5250

728 
by (afs [surj_PiBij] 1);

5318

729 
by (assume_tac 1);

5250

730 
val PiBij_bij2 = result();


731 


732 
goal PiSets.thy "!! g f. [ ! x. g( f x) = x ] ==> inj f";

5318

733 
by (rtac injI 1);

5250

734 
by (dres_inst_tac [("f","g")] arg_cong 1);


735 
by (forw_inst_tac [("x","x")] spec 1);


736 
by (rotate_tac 2 1);

5318

737 
by (etac subst 1);

5250

738 
by (forw_inst_tac [("x","y")] spec 1);


739 
by (rotate_tac 2 1);

5318

740 
by (etac subst 1);


741 
by (assume_tac 1);

5250

742 
val inj_lemma = result();


743 


744 
goal PiSets.thy "!! g f. [ ! x. g( f x) = x ] ==> surj g";


745 
by (afs [surj_def] 1);

5318

746 
by (rtac allI 1);

5250

747 
by (res_inst_tac [("x","f y")] exI 1);

5318

748 
by (dtac spec 1);


749 
by (etac sym 1);

5250

750 
val surj_lemma = result();


751 


752 
goal PiSets.thy "Pi {} B == {f. !x. f x = (@ y. True)}";


753 
by (afs [Pi_def] 1);


754 
val empty_Pi = result();


755 


756 
goal PiSets.thy "(% x. (@ y. True)) : Pi {} B";


757 
by (afs [empty_Pi] 1);


758 
val empty_Pi_func = result();


759 


760 
goal Set.thy "!! A B. [ A <= B; x ~: B ] ==> x ~: A";


761 
by (Blast_tac 1);


762 
val subsetND = result();


763 


764 


765 
goal PiSets.thy "!! A B C . [ ! x: A. B x <= C x ] ==> Pi A B <= Pi A C";

5318

766 
by (rtac subsetI 1);


767 
by (rtac Pi_I 1);

5250

768 
by (afs [Pi_def] 2);

5318

769 
by (dtac bspec 1);


770 
by (assume_tac 1);


771 
by (etac subsetD 1);

5250

772 
by (afs [PiE1] 1);


773 
val Pi_subset1 = result();
