|
1 (* Title: HOL/ex/PiSets.ML |
|
2 ID: $Id$ |
|
3 Author: Florian Kammueller, University of Cambridge |
|
4 |
|
5 Pi sets and their application. |
|
6 *) |
|
7 |
|
8 (*** Bijection between Pi in terms of => and Pi in terms of Sigma ***) |
|
9 Goal "f \\<in> Pi A B ==> PiBij A B f <= Sigma A B"; |
|
10 by (auto_tac (claset(), simpset() addsimps [PiBij_def,Pi_def])); |
|
11 qed "PiBij_subset_Sigma"; |
|
12 |
|
13 Goal "f \\<in> Pi A B ==> \\<forall>x \\<in> A. \\<exists>!y. (x, y) \\<in> (PiBij A B f)"; |
|
14 by (auto_tac (claset(), simpset() addsimps [PiBij_def])); |
|
15 qed "PiBij_unique"; |
|
16 |
|
17 Goal "f \\<in> Pi A B ==> PiBij A B f \\<in> Graph A B"; |
|
18 by (asm_simp_tac (simpset() addsimps [Graph_def,PiBij_unique, |
|
19 PiBij_subset_Sigma]) 1); |
|
20 qed "PiBij_in_Graph"; |
|
21 |
|
22 Goalw [PiBij_def, Graph_def] "PiBij A B \\<in> Pi A B \\<rightarrow> Graph A B"; |
|
23 by (rtac restrictI 1); |
|
24 by (auto_tac (claset(), simpset() addsimps [Pi_def])); |
|
25 qed "PiBij_func"; |
|
26 |
|
27 Goal "inj_on (PiBij A B) (Pi A B)"; |
|
28 by (rtac inj_onI 1); |
|
29 by (rtac Pi_extensionality 1); |
|
30 by (assume_tac 1); |
|
31 by (assume_tac 1); |
|
32 by (asm_full_simp_tac (simpset() addsimps [PiBij_def]) 1); |
|
33 by (Blast_tac 1); |
|
34 qed "inj_PiBij"; |
|
35 |
|
36 |
|
37 Goal "x \\<in> Graph A B \\<Longrightarrow> (lam a:A. SOME y. (a, y) \\<in> x) \\<in> Pi A B"; |
|
38 by (rtac restrictI 1); |
|
39 by (res_inst_tac [("P", "%xa. (a, xa)\\<in>x")] ex1E 1); |
|
40 by (force_tac (claset(), simpset() addsimps [Graph_def]) 1); |
|
41 by (full_simp_tac (simpset() addsimps [Graph_def]) 1); |
|
42 by (stac some_equality 1); |
|
43 by (assume_tac 1); |
|
44 by (Blast_tac 1); |
|
45 by (Blast_tac 1); |
|
46 qed "in_Graph_imp_in_Pi"; |
|
47 |
|
48 Goal "PiBij A B ` (Pi A B) = Graph A B"; |
|
49 by (rtac equalityI 1); |
|
50 by (force_tac (claset(), simpset() addsimps [PiBij_in_Graph]) 1); |
|
51 by (rtac subsetI 1); |
|
52 by (rtac image_eqI 1); |
|
53 by (etac in_Graph_imp_in_Pi 2); |
|
54 (* x = PiBij A B (lam a:A. @ y. (a, y)\\<in>x) *) |
|
55 by (asm_simp_tac (simpset() addsimps [in_Graph_imp_in_Pi, PiBij_def]) 1); |
|
56 by (auto_tac (claset(), simpset() addsimps [some1_equality, Graph_def])); |
|
57 by (fast_tac (claset() addIs [someI2]) 1); |
|
58 qed "surj_PiBij"; |
|
59 |
|
60 Goal "f \\<in> Pi A B ==> Inv (Pi A B) (PiBij A B) (PiBij A B f) = f"; |
|
61 by (asm_simp_tac (simpset() addsimps [Inv_f_f, inj_PiBij]) 1); |
|
62 qed "PiBij_bij1"; |
|
63 |
|
64 Goal "f \\<in> Graph A B ==> PiBij A B (Inv (Pi A B) (PiBij A B) f) = f"; |
|
65 by (asm_simp_tac (simpset() addsimps [f_Inv_f, surj_PiBij]) 1); |
|
66 qed "PiBij_bij2"; |