equal
deleted
inserted
replaced
1 (* Title: HOL/ex/PiSets.thy |
1 (* Title: HOL/ex/PiSets.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Florian Kammueller, University of Cambridge |
3 Author: Florian Kammueller, University of Cambridge |
4 |
4 |
5 Pi sets and their application. |
5 Pi sets and their application. |
6 *) |
6 *) |
31 by (rtac Pi_extensionality 1); |
31 by (rtac Pi_extensionality 1); |
32 by (assume_tac 1); |
32 by (assume_tac 1); |
33 by (assume_tac 1); |
33 by (assume_tac 1); |
34 by (rotate_tac 1 1); |
34 by (rotate_tac 1 1); |
35 by (asm_full_simp_tac (simpset() addsimps [PiBij_def,restrict_apply1]) 1); |
35 by (asm_full_simp_tac (simpset() addsimps [PiBij_def,restrict_apply1]) 1); |
36 by (blast_tac (claset() addEs [equalityE]) 1); |
36 by (Blast_tac 1); |
37 qed "inj_PiBij"; |
37 qed "inj_PiBij"; |
38 |
38 |
39 |
39 |
40 |
40 |
41 Goal "PiBij A B `` (Pi A B) = Graph A B"; |
41 Goal "PiBij A B `` (Pi A B) = Graph A B"; |