author  paulson 
Wed, 08 Sep 1999 15:39:52 +0200  
changeset 7516  a1d476251238 
parent 7031  972b5f62f476 
child 7823  742715638a01 
permissions  rwrr 
4648  1 
(* Title: HOL/Vimage 
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 

7031  11 
Goalw [vimage_def] "(a : f``B) = (f a : B)"; 
12 
by (Blast_tac 1) ; 

13 
qed "vimage_eq"; 

4648  14 

4680  15 
Addsimps [vimage_eq]; 
16 

7031  17 
Goal "(a : f``{b}) = (f a = b)"; 
18 
by (simp_tac (simpset() addsimps [vimage_eq]) 1) ; 

19 
qed "vimage_singleton_eq"; 

4648  20 

7031  21 
Goalw [vimage_def] 
22 
"!!A B f. [ f a = b; b:B ] ==> a : f``B"; 

23 
by (Blast_tac 1) ; 

24 
qed "vimageI"; 

4648  25 

5095
4436c62efceb
Added additional theorems needed for inductive definitions.
berghofe
parents:
5069
diff
changeset

26 
Goalw [vimage_def] "f a : A ==> a : f `` A"; 
4436c62efceb
Added additional theorems needed for inductive definitions.
berghofe
parents:
5069
diff
changeset

27 
by (Fast_tac 1); 
4436c62efceb
Added additional theorems needed for inductive definitions.
berghofe
parents:
5069
diff
changeset

28 
qed "vimageI2"; 
4436c62efceb
Added additional theorems needed for inductive definitions.
berghofe
parents:
5069
diff
changeset

29 

7031  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"; 

4648  35 

5095
4436c62efceb
Added additional theorems needed for inductive definitions.
berghofe
parents:
5069
diff
changeset

36 
Goalw [vimage_def] "a : f `` A ==> f a : A"; 
4436c62efceb
Added additional theorems needed for inductive definitions.
berghofe
parents:
5069
diff
changeset

37 
by (Fast_tac 1); 
4436c62efceb
Added additional theorems needed for inductive definitions.
berghofe
parents:
5069
diff
changeset

38 
qed "vimageD"; 
4436c62efceb
Added additional theorems needed for inductive definitions.
berghofe
parents:
5069
diff
changeset

39 

4648  40 
AddIs [vimageI]; 
41 
AddSEs [vimageE]; 

42 

43 

44 
(*** Simple equalities ***) 

45 

5069  46 
Goal "f``{} = {}"; 
4648  47 
by (Blast_tac 1); 
48 
qed "vimage_empty"; 

49 

5490  50 
Goal "f``(A) = (f``A)"; 
4660  51 
by (Blast_tac 1); 
52 
qed "vimage_Compl"; 

53 

5069  54 
Goal "f``(A Un B) = (f``A) Un (f``B)"; 
4648  55 
by (Blast_tac 1); 
56 
qed "vimage_Un"; 

57 

5095
4436c62efceb
Added additional theorems needed for inductive definitions.
berghofe
parents:
5069
diff
changeset

58 
Goal "f `` (A Int B) = (f `` A) Int (f `` B)"; 
4436c62efceb
Added additional theorems needed for inductive definitions.
berghofe
parents:
5069
diff
changeset

59 
by (Fast_tac 1); 
4436c62efceb
Added additional theorems needed for inductive definitions.
berghofe
parents:
5069
diff
changeset

60 
qed "vimage_Int"; 
4436c62efceb
Added additional theorems needed for inductive definitions.
berghofe
parents:
5069
diff
changeset

61 

5069  62 
Goal "f``(UN x:A. B x) = (UN x:A. f `` B x)"; 
4674  63 
by (Blast_tac 1); 
64 
qed "vimage_UN"; 

65 

5095
4436c62efceb
Added additional theorems needed for inductive definitions.
berghofe
parents:
5069
diff
changeset

66 
bind_thm ("vimage_Collect", allI RS prove_goalw thy [vimage_def] 
4436c62efceb
Added additional theorems needed for inductive definitions.
berghofe
parents:
5069
diff
changeset

67 
"! x. P (f x) = Q x ==> f `` (Collect P) = Collect Q" 
4436c62efceb
Added additional theorems needed for inductive definitions.
berghofe
parents:
5069
diff
changeset

68 
(fn prems => [cut_facts_tac prems 1, Fast_tac 1])); 
4436c62efceb
Added additional theorems needed for inductive definitions.
berghofe
parents:
5069
diff
changeset

69 

4436c62efceb
Added additional theorems needed for inductive definitions.
berghofe
parents:
5069
diff
changeset

70 
Addsimps [vimage_empty, vimage_Un, vimage_Int]; 
4660  71 

4648  72 
(*NOT suitable for rewriting because of the recurrence of {a}*) 
5069  73 
Goal "f``(insert a B) = (f``{a}) Un (f``B)"; 
4648  74 
by (Blast_tac 1); 
75 
qed "vimage_insert"; 

76 

5069  77 
Goal "f``(AB) = (f``A)  (f``B)"; 
4738  78 
by (Blast_tac 1); 
79 
qed "vimage_Diff"; 

4648  80 

5069  81 
Goal "f``UNIV = UNIV"; 
4648  82 
by (Blast_tac 1); 
83 
qed "vimage_UNIV"; 

84 
Addsimps [vimage_UNIV]; 

85 

5069  86 
Goal "(UN x:A. f `` B x) = f `` (UN x:A. B x)"; 
4648  87 
by (Blast_tac 1); 
88 
qed "UN_vimage"; 

89 
Addsimps [UN_vimage]; 

90 

4734  91 
(*NOT suitable for rewriting*) 
5069  92 
Goal "f``B = (UN y: B. f``{y})"; 
4734  93 
by (Blast_tac 1); 
94 
qed "vimage_eq_UN"; 

95 

4648  96 

97 
(** monotonicity **) 

98 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5122
diff
changeset

99 
Goal "A<=B ==> f``A <= f``B"; 
4648  100 
by (Blast_tac 1); 
101 
qed "vimage_mono"; 