|
1 (* Title: HOL/Inverse_Image.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1998 University of Cambridge |
|
5 |
|
6 Inverse image of a function |
|
7 *) |
|
8 |
|
9 (** Basic rules **) |
|
10 |
|
11 Goalw [vimage_def] "(a : f-``B) = (f a : B)"; |
|
12 by (Blast_tac 1) ; |
|
13 qed "vimage_eq"; |
|
14 |
|
15 Addsimps [vimage_eq]; |
|
16 |
|
17 Goal "(a : f-``{b}) = (f a = b)"; |
|
18 by (simp_tac (simpset() addsimps [vimage_eq]) 1) ; |
|
19 qed "vimage_singleton_eq"; |
|
20 |
|
21 Goalw [vimage_def] |
|
22 "!!A B f. [| f a = b; b:B |] ==> a : f-``B"; |
|
23 by (Blast_tac 1) ; |
|
24 qed "vimageI"; |
|
25 |
|
26 Goalw [vimage_def] "f a : A ==> a : f -`` A"; |
|
27 by (Fast_tac 1); |
|
28 qed "vimageI2"; |
|
29 |
|
30 val major::prems = Goalw [vimage_def] |
|
31 "[| a: f-``B; !!x.[| f a = x; x:B |] ==> P |] ==> P"; |
|
32 by (rtac (major RS CollectE) 1); |
|
33 by (blast_tac (claset() addIs prems) 1) ; |
|
34 qed "vimageE"; |
|
35 |
|
36 Goalw [vimage_def] "a : f -`` A ==> f a : A"; |
|
37 by (Fast_tac 1); |
|
38 qed "vimageD"; |
|
39 |
|
40 AddIs [vimageI]; |
|
41 AddSEs [vimageE]; |
|
42 |
|
43 |
|
44 (*** Equations ***) |
|
45 |
|
46 Goal "f-``{} = {}"; |
|
47 by (Blast_tac 1); |
|
48 qed "vimage_empty"; |
|
49 |
|
50 Goal "f-``(-A) = -(f-``A)"; |
|
51 by (Blast_tac 1); |
|
52 qed "vimage_Compl"; |
|
53 |
|
54 Goal "f-``(A Un B) = (f-``A) Un (f-``B)"; |
|
55 by (Blast_tac 1); |
|
56 qed "vimage_Un"; |
|
57 |
|
58 Goal "f -`` (A Int B) = (f -`` A) Int (f -`` B)"; |
|
59 by (Fast_tac 1); |
|
60 qed "vimage_Int"; |
|
61 |
|
62 Goal "f -`` (Union A) = (UN X:A. f -`` X)"; |
|
63 by (Blast_tac 1); |
|
64 qed "vimage_Union"; |
|
65 |
|
66 Goal "f-``(UN x:A. B x) = (UN x:A. f -`` B x)"; |
|
67 by (Blast_tac 1); |
|
68 qed "vimage_UN"; |
|
69 |
|
70 Goal "f-``(INT x:A. B x) = (INT x:A. f -`` B x)"; |
|
71 by (Blast_tac 1); |
|
72 qed "vimage_INT"; |
|
73 |
|
74 Goal "f -`` Collect P = {y. P (f y)}"; |
|
75 by (Blast_tac 1); |
|
76 qed "vimage_Collect_eq"; |
|
77 Addsimps [vimage_Collect_eq]; |
|
78 |
|
79 (*A strange result used in Tools/inductive_package*) |
|
80 val prems = Goal "(!!x. P (f x) = Q x) ==> f -`` (Collect P) = Collect Q"; |
|
81 by (force_tac (claset(), simpset() addsimps prems) 1); |
|
82 qed "vimage_Collect"; |
|
83 |
|
84 Addsimps [vimage_empty, vimage_Un, vimage_Int]; |
|
85 |
|
86 (*NOT suitable for rewriting because of the recurrence of {a}*) |
|
87 Goal "f-``(insert a B) = (f-``{a}) Un (f-``B)"; |
|
88 by (Blast_tac 1); |
|
89 qed "vimage_insert"; |
|
90 |
|
91 Goal "f-``(A-B) = (f-``A) - (f-``B)"; |
|
92 by (Blast_tac 1); |
|
93 qed "vimage_Diff"; |
|
94 |
|
95 Goal "f-``UNIV = UNIV"; |
|
96 by (Blast_tac 1); |
|
97 qed "vimage_UNIV"; |
|
98 Addsimps [vimage_UNIV]; |
|
99 |
|
100 (*NOT suitable for rewriting*) |
|
101 Goal "f-``B = (UN y: B. f-``{y})"; |
|
102 by (Blast_tac 1); |
|
103 qed "vimage_eq_UN"; |
|
104 |
|
105 (*monotonicity*) |
|
106 Goal "A<=B ==> f-``A <= f-``B"; |
|
107 by (Blast_tac 1); |
|
108 qed "vimage_mono"; |