author  paulson 
Fri, 27 Nov 1998 10:40:29 +0100  
changeset 5978  fa2c2dd74f8c 
parent 5811  0867068942e6 
child 5995  450cd1f0270b 
permissions  rwrr 
1465  1 
(* Title: Relation.ML 
1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

2 
ID: $Id$ 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1842
diff
changeset

3 
Authors: Lawrence C Paulson, Cambridge University Computer Laboratory 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1842
diff
changeset

4 
Copyright 1996 University of Cambridge 
1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

5 
*) 
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

6 

64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

7 
open Relation; 
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

8 

64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

9 
(** Identity relation **) 
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

10 

5608  11 
Goalw [Id_def] "(a,a) : Id"; 
2891  12 
by (Blast_tac 1); 
5608  13 
qed "IdI"; 
1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

14 

5608  15 
val major::prems = Goalw [Id_def] 
16 
"[ p: Id; !!x.[ p = (x,x) ] ==> P \ 

1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

17 
\ ] ==> P"; 
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

18 
by (rtac (major RS CollectE) 1); 
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

19 
by (etac exE 1); 
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

20 
by (eresolve_tac prems 1); 
5608  21 
qed "IdE"; 
1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

22 

5608  23 
Goalw [Id_def] "(a,b):Id = (a=b)"; 
2891  24 
by (Blast_tac 1); 
5608  25 
qed "pair_in_Id_conv"; 
26 
Addsimps [pair_in_Id_conv]; 

1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

27 

64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

28 

5978
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5811
diff
changeset

29 
(** Diagonal relation: indentity restricted to some set **) 
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5811
diff
changeset

30 

fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5811
diff
changeset

31 
(*** Equality : the diagonal relation ***) 
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5811
diff
changeset

32 

fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5811
diff
changeset

33 
Goalw [diag_def] "[ a=b; a:A ] ==> (a,b) : diag(A)"; 
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5811
diff
changeset

34 
by (Blast_tac 1); 
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5811
diff
changeset

35 
qed "diag_eqI"; 
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5811
diff
changeset

36 

fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5811
diff
changeset

37 
val diagI = refl RS diag_eqI > standard; 
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5811
diff
changeset

38 

fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5811
diff
changeset

39 
(*The general elimination rule*) 
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5811
diff
changeset

40 
val major::prems = Goalw [diag_def] 
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5811
diff
changeset

41 
"[ c : diag(A); \ 
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5811
diff
changeset

42 
\ !!x y. [ x:A; c = (x,x) ] ==> P \ 
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5811
diff
changeset

43 
\ ] ==> P"; 
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5811
diff
changeset

44 
by (rtac (major RS UN_E) 1); 
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5811
diff
changeset

45 
by (REPEAT (eresolve_tac [asm_rl,singletonE] 1 ORELSE resolve_tac prems 1)); 
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5811
diff
changeset

46 
qed "diagE"; 
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5811
diff
changeset

47 

fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5811
diff
changeset

48 
AddSIs [diagI]; 
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5811
diff
changeset

49 
AddSEs [diagE]; 
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5811
diff
changeset

50 

fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5811
diff
changeset

51 
Goal "((x,y) : diag A) = (x=y & x : A)"; 
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5811
diff
changeset

52 
by (Blast_tac 1); 
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5811
diff
changeset

53 
qed "diag_iff"; 
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5811
diff
changeset

54 

fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5811
diff
changeset

55 
Goal "diag(A) <= A Times A"; 
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5811
diff
changeset

56 
by (Blast_tac 1); 
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5811
diff
changeset

57 
qed "diag_subset_Sigma"; 
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5811
diff
changeset

58 

fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5811
diff
changeset

59 

fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5811
diff
changeset

60 

1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

61 
(** Composition of two relations **) 
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

62 

5069  63 
Goalw [comp_def] 
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset

64 
"[ (a,b):s; (b,c):r ] ==> (a,c) : r O s"; 
2891  65 
by (Blast_tac 1); 
1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

66 
qed "compI"; 
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

67 

64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

68 
(*proof requires higherlevel assumptions or a delaying of hyp_subst_tac*) 
5316  69 
val prems = Goalw [comp_def] 
1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

70 
"[ xz : r O s; \ 
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

71 
\ !!x y z. [ xz = (x,z); (x,y):s; (y,z):r ] ==> P \ 
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

72 
\ ] ==> P"; 
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

73 
by (cut_facts_tac prems 1); 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1842
diff
changeset

74 
by (REPEAT (eresolve_tac [CollectE, splitE, exE, conjE] 1 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1842
diff
changeset

75 
ORELSE ares_tac prems 1)); 
1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

76 
qed "compE"; 
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

77 

5316  78 
val prems = Goal 
1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

79 
"[ (a,c) : r O s; \ 
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

80 
\ !!y. [ (a,y):s; (y,c):r ] ==> P \ 
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

81 
\ ] ==> P"; 
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

82 
by (rtac compE 1); 
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

83 
by (REPEAT (ares_tac prems 1 ORELSE eresolve_tac [Pair_inject,ssubst] 1)); 
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

84 
qed "compEpair"; 
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

85 

5608  86 
AddIs [compI, IdI]; 
87 
AddSEs [compE, IdE]; 

1754
852093aeb0ab
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1694
diff
changeset

88 

5608  89 
Goal "R O Id = R"; 
4673  90 
by (Fast_tac 1); 
5608  91 
qed "R_O_Id"; 
4673  92 

5608  93 
Goal "Id O R = R"; 
4673  94 
by (Fast_tac 1); 
5608  95 
qed "Id_O_R"; 
4673  96 

5608  97 
Addsimps [R_O_Id,Id_O_R]; 
4673  98 

5069  99 
Goal "(R O S) O T = R O (S O T)"; 
4830  100 
by (Blast_tac 1); 
101 
qed "O_assoc"; 

102 

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

103 
Goal "[ r'<=r; s'<=s ] ==> (r' O s') <= (r O s)"; 
2891  104 
by (Blast_tac 1); 
1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

105 
qed "comp_mono"; 
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

106 

5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset

107 
Goal "[ s <= A Times B; r <= B Times C ] ==> (r O s) <= A Times C"; 
2891  108 
by (Blast_tac 1); 
1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

109 
qed "comp_subset_Sigma"; 
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

110 

64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

111 
(** Natural deduction for trans(r) **) 
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

112 

5316  113 
val prems = Goalw [trans_def] 
1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

114 
"(!! x y z. [ (x,y):r; (y,z):r ] ==> (x,z):r) ==> trans(r)"; 
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

115 
by (REPEAT (ares_tac (prems@[allI,impI]) 1)); 
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

116 
qed "transI"; 
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

117 

5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset

118 
Goalw [trans_def] "[ trans(r); (a,b):r; (b,c):r ] ==> (a,c):r"; 
2891  119 
by (Blast_tac 1); 
1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

120 
qed "transD"; 
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

121 

3439  122 
(** Natural deduction for r^1 **) 
1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

123 

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

124 
Goalw [converse_def] "((a,b): r^1) = ((b,a):r)"; 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1842
diff
changeset

125 
by (Simp_tac 1); 
4746  126 
qed "converse_iff"; 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1842
diff
changeset

127 

4746  128 
AddIffs [converse_iff]; 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1842
diff
changeset

129 

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

130 
Goalw [converse_def] "(a,b):r ==> (b,a): r^1"; 
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1128
diff
changeset

131 
by (Simp_tac 1); 
4746  132 
qed "converseI"; 
1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

133 

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

134 
Goalw [converse_def] "(a,b) : r^1 ==> (b,a) : r"; 
2891  135 
by (Blast_tac 1); 
4746  136 
qed "converseD"; 
1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

137 

4746  138 
(*More general than converseD, as it "splits" the member of the relation*) 
139 
qed_goalw "converseE" thy [converse_def] 

3439  140 
"[ yx : r^1; \ 
1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

141 
\ !!x y. [ yx=(y,x); (x,y):r ] ==> P \ 
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

142 
\ ] ==> P" 
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

143 
(fn [major,minor]=> 
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

144 
[ (rtac (major RS CollectE) 1), 
1454
d0266c81a85e
Streamlined defs in Relation and added new intro/elim rules to do with
nipkow
parents:
1264
diff
changeset

145 
(REPEAT (eresolve_tac [splitE, bexE,exE, conjE, minor] 1)), 
1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

146 
(assume_tac 1) ]); 
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

147 

4746  148 
AddSEs [converseE]; 
1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

149 

5069  150 
Goalw [converse_def] "(r^1)^1 = r"; 
2891  151 
by (Blast_tac 1); 
4746  152 
qed "converse_converse"; 
153 
Addsimps [converse_converse]; 

3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
2891
diff
changeset

154 

5069  155 
Goal "(r O s)^1 = s^1 O r^1"; 
4423  156 
by (Blast_tac 1); 
4746  157 
qed "converse_comp"; 
1605  158 

5608  159 
Goal "Id^1 = Id"; 
4644  160 
by (Blast_tac 1); 
5608  161 
qed "converse_Id"; 
162 
Addsimps [converse_Id]; 

4644  163 

1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

164 
(** Domain **) 
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

165 

5811  166 
Goalw [Domain_def] "a: Domain(r) = (EX y. (a,y): r)"; 
167 
by (Blast_tac 1); 

168 
qed "Domain_iff"; 

1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

169 

4673  170 
qed_goal "DomainI" thy "!!a b r. (a,b): r ==> a: Domain(r)" 
1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

171 
(fn _ => [ (etac (exI RS (Domain_iff RS iffD2)) 1) ]); 
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

172 

4673  173 
qed_goal "DomainE" thy 
1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

174 
"[ a : Domain(r); !!y. (a,y): r ==> P ] ==> P" 
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

175 
(fn prems=> 
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

176 
[ (rtac (Domain_iff RS iffD1 RS exE) 1), 
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

177 
(REPEAT (ares_tac prems 1)) ]); 
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

178 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1842
diff
changeset

179 
AddIs [DomainI]; 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1842
diff
changeset

180 
AddSEs [DomainE]; 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1842
diff
changeset

181 

5608  182 
Goal "Domain Id = UNIV"; 
4644  183 
by (Blast_tac 1); 
5608  184 
qed "Domain_Id"; 
185 
Addsimps [Domain_Id]; 

4644  186 

5978
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5811
diff
changeset

187 
Goal "Domain (diag A) = A"; 
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5811
diff
changeset

188 
by Auto_tac; 
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5811
diff
changeset

189 
qed "Domain_diag"; 
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5811
diff
changeset

190 
Addsimps [Domain_diag]; 
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5811
diff
changeset

191 

5811  192 
Goal "Domain(A Un B) = Domain(A) Un Domain(B)"; 
193 
by (Blast_tac 1); 

194 
qed "Domain_Un_eq"; 

195 

196 
Goal "Domain(A Int B) <= Domain(A) Int Domain(B)"; 

197 
by (Blast_tac 1); 

198 
qed "Domain_Int_subset"; 

199 

200 
Goal "Domain(A)  Domain(B) <= Domain(A  B)"; 

201 
by (Blast_tac 1); 

202 
qed "Domain_Diff_subset"; 

203 

204 

1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

205 
(** Range **) 
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

206 

5811  207 
Goalw [Domain_def, Range_def] "a: Range(r) = (EX y. (y,a): r)"; 
208 
by (Blast_tac 1); 

209 
qed "Range_iff"; 

210 

4673  211 
qed_goalw "RangeI" thy [Range_def] "!!a b r.(a,b): r ==> b : Range(r)" 
4746  212 
(fn _ => [ (etac (converseI RS DomainI) 1) ]); 
1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

213 

4673  214 
qed_goalw "RangeE" thy [Range_def] 
1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

215 
"[ b : Range(r); !!x. (x,b): r ==> P ] ==> P" 
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

216 
(fn major::prems=> 
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

217 
[ (rtac (major RS DomainE) 1), 
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

218 
(resolve_tac prems 1), 
4746  219 
(etac converseD 1) ]); 
1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

220 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1842
diff
changeset

221 
AddIs [RangeI]; 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1842
diff
changeset

222 
AddSEs [RangeE]; 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1842
diff
changeset

223 

5608  224 
Goal "Range Id = UNIV"; 
4644  225 
by (Blast_tac 1); 
5608  226 
qed "Range_Id"; 
227 
Addsimps [Range_Id]; 

4644  228 

5811  229 
Goal "Range(A Un B) = Range(A) Un Range(B)"; 
230 
by (Blast_tac 1); 

231 
qed "Range_Un_eq"; 

232 

233 
Goal "Range(A Int B) <= Range(A) Int Range(B)"; 

234 
by (Blast_tac 1); 

235 
qed "Range_Int_subset"; 

236 

237 
Goal "Range(A)  Range(B) <= Range(A  B)"; 

238 
by (Blast_tac 1); 

239 
qed "Range_Diff_subset"; 

240 

241 

1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

242 
(*** Image of a set under a relation ***) 
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

243 

5649  244 
overload_1st_set "Relation.op ^^"; 
5335  245 

4673  246 
qed_goalw "Image_iff" thy [Image_def] 
1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

247 
"b : r^^A = (? x:A. (x,b):r)" 
2891  248 
(fn _ => [ Blast_tac 1 ]); 
1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

249 

4673  250 
qed_goalw "Image_singleton" thy [Image_def] 
251 
"r^^{a} = {b. (a,b):r}" 

252 
(fn _ => [ Blast_tac 1 ]); 

253 

254 
qed_goal "Image_singleton_iff" thy 

1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

255 
"(b : r^^{a}) = ((a,b):r)" 
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

256 
(fn _ => [ rtac (Image_iff RS trans) 1, 
2891  257 
Blast_tac 1 ]); 
1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

258 

4673  259 
AddIffs [Image_singleton_iff]; 
260 

261 
qed_goalw "ImageI" thy [Image_def] 

1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

262 
"!!a b r. [ (a,b): r; a:A ] ==> b : r^^A" 
2891  263 
(fn _ => [ (Blast_tac 1)]); 
1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

264 

4673  265 
qed_goalw "ImageE" thy [Image_def] 
1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

266 
"[ b: r^^A; !!x.[ (x,b): r; x:A ] ==> P ] ==> P" 
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

267 
(fn major::prems=> 
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

268 
[ (rtac (major RS CollectE) 1), 
3718  269 
(Clarify_tac 1), 
1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

270 
(rtac (hd prems) 1), 
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

271 
(REPEAT (etac bexE 1 ORELSE ares_tac prems 1)) ]); 
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

272 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1842
diff
changeset

273 
AddIs [ImageI]; 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1842
diff
changeset

274 
AddSEs [ImageE]; 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1842
diff
changeset

275 

4593  276 

4673  277 
qed_goal "Image_empty" thy 
4593  278 
"R^^{} = {}" 
279 
(fn _ => [ Blast_tac 1 ]); 

280 

281 
Addsimps [Image_empty]; 

282 

5608  283 
Goal "Id ^^ A = A"; 
4601  284 
by (Blast_tac 1); 
5608  285 
qed "Image_Id"; 
4601  286 

5608  287 
Addsimps [Image_Id]; 
4601  288 

4673  289 
qed_goal "Image_Int_subset" thy 
4593  290 
"R ^^ (A Int B) <= R ^^ A Int R ^^ B" 
291 
(fn _ => [ Blast_tac 1 ]); 

292 

4733
2c984ac036f5
New theorem Image_eq_UN; deleted the silly vimage_inverse_Image
paulson
parents:
4673
diff
changeset

293 
qed_goal "Image_Un" thy "R ^^ (A Un B) = R ^^ A Un R ^^ B" 
4593  294 
(fn _ => [ Blast_tac 1 ]); 
295 

4733
2c984ac036f5
New theorem Image_eq_UN; deleted the silly vimage_inverse_Image
paulson
parents:
4673
diff
changeset

296 
qed_goal "Image_subset" thy "!!A B r. r <= A Times B ==> r^^C <= B" 
1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

297 
(fn _ => 
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

298 
[ (rtac subsetI 1), 
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

299 
(REPEAT (eresolve_tac [asm_rl, ImageE, subsetD RS SigmaD2] 1)) ]); 
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

300 

4733
2c984ac036f5
New theorem Image_eq_UN; deleted the silly vimage_inverse_Image
paulson
parents:
4673
diff
changeset

301 
(*NOT suitable for rewriting*) 
5069  302 
Goal "r^^B = (UN y: B. r^^{y})"; 
4673  303 
by (Blast_tac 1); 
4733
2c984ac036f5
New theorem Image_eq_UN; deleted the silly vimage_inverse_Image
paulson
parents:
4673
diff
changeset

304 
qed "Image_eq_UN"; 
4760
9cdbd5a1d25a
added introduction and elimination rules for Univalent
oheimb
parents:
4746
diff
changeset

305 

9cdbd5a1d25a
added introduction and elimination rules for Univalent
oheimb
parents:
4746
diff
changeset

306 

9cdbd5a1d25a
added introduction and elimination rules for Univalent
oheimb
parents:
4746
diff
changeset

307 
section "Univalent"; 
9cdbd5a1d25a
added introduction and elimination rules for Univalent
oheimb
parents:
4746
diff
changeset

308 

9cdbd5a1d25a
added introduction and elimination rules for Univalent
oheimb
parents:
4746
diff
changeset

309 
qed_goalw "UnivalentI" Relation.thy [Univalent_def] 
9cdbd5a1d25a
added introduction and elimination rules for Univalent
oheimb
parents:
4746
diff
changeset

310 
"!!r. !x y. (x,y):r > (!z. (x,z):r > y=z) ==> Univalent r" (K [atac 1]); 
9cdbd5a1d25a
added introduction and elimination rules for Univalent
oheimb
parents:
4746
diff
changeset

311 

9cdbd5a1d25a
added introduction and elimination rules for Univalent
oheimb
parents:
4746
diff
changeset

312 
qed_goalw "UnivalentD" Relation.thy [Univalent_def] 
9cdbd5a1d25a
added introduction and elimination rules for Univalent
oheimb
parents:
4746
diff
changeset

313 
"!!r. [ Univalent r; (x,y):r; (x,z):r] ==> y=z" (K [Auto_tac]); 
5231  314 

315 

316 
(** Graphs of partial functions **) 

317 

318 
Goal "Domain{(x,y). y = f x & P x} = {x. P x}"; 

319 
by (Blast_tac 1); 

320 
qed "Domain_partial_func"; 

321 

322 
Goal "Range{(x,y). y = f x & P x} = f``{x. P x}"; 

323 
by (Blast_tac 1); 

324 
qed "Range_partial_func"; 

325 