author  paulson 
Mon, 30 Nov 1998 10:43:35 +0100  
changeset 5995  450cd1f0270b 
parent 5978  fa2c2dd74f8c 
child 5998  b2ecd577b8a3 
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); 
5995  57 
qed "diag_subset_Times"; 
5978
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 

5995  164 
Goal "(diag A) ^1 = diag A"; 
165 
by (Blast_tac 1); 

166 
qed "converse_diag"; 

167 
Addsimps [converse_diag]; 

168 

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

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

170 

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

173 
qed "Domain_iff"; 

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

174 

4673  175 
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

176 
(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

177 

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

179 
"[ 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

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

181 
[ (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

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

183 

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

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

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

186 

5608  187 
Goal "Domain Id = UNIV"; 
4644  188 
by (Blast_tac 1); 
5608  189 
qed "Domain_Id"; 
190 
Addsimps [Domain_Id]; 

4644  191 

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

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

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

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

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

196 

5811  197 
Goal "Domain(A Un B) = Domain(A) Un Domain(B)"; 
198 
by (Blast_tac 1); 

199 
qed "Domain_Un_eq"; 

200 

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

202 
by (Blast_tac 1); 

203 
qed "Domain_Int_subset"; 

204 

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

206 
by (Blast_tac 1); 

207 
qed "Domain_Diff_subset"; 

208 

209 

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

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

211 

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

214 
qed "Range_iff"; 

215 

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

218 

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

220 
"[ 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

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

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

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

225 

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

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

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

228 

5608  229 
Goal "Range Id = UNIV"; 
4644  230 
by (Blast_tac 1); 
5608  231 
qed "Range_Id"; 
232 
Addsimps [Range_Id]; 

4644  233 

5995  234 
Goal "Range (diag A) = A"; 
235 
by Auto_tac; 

236 
qed "Range_diag"; 

237 
Addsimps [Range_diag]; 

238 

5811  239 
Goal "Range(A Un B) = Range(A) Un Range(B)"; 
240 
by (Blast_tac 1); 

241 
qed "Range_Un_eq"; 

242 

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

244 
by (Blast_tac 1); 

245 
qed "Range_Int_subset"; 

246 

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

248 
by (Blast_tac 1); 

249 
qed "Range_Diff_subset"; 

250 

251 

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

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

253 

5649  254 
overload_1st_set "Relation.op ^^"; 
5335  255 

4673  256 
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

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

259 

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

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

263 

264 
qed_goal "Image_singleton_iff" thy 

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

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

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

268 

4673  269 
AddIffs [Image_singleton_iff]; 
270 

271 
qed_goalw "ImageI" thy [Image_def] 

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

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

274 

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

276 
"[ 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

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

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

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

281 
(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

282 

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

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

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

285 

4593  286 

4673  287 
qed_goal "Image_empty" thy 
4593  288 
"R^^{} = {}" 
289 
(fn _ => [ Blast_tac 1 ]); 

290 

291 
Addsimps [Image_empty]; 

292 

5608  293 
Goal "Id ^^ A = A"; 
4601  294 
by (Blast_tac 1); 
5608  295 
qed "Image_Id"; 
4601  296 

5995  297 
Goal "B<=A ==> diag A ^^ B = B"; 
298 
by (Blast_tac 1); 

299 
qed "Image_diag"; 

300 

301 
Addsimps [Image_Id, Image_diag]; 

4601  302 

4673  303 
qed_goal "Image_Int_subset" thy 
4593  304 
"R ^^ (A Int B) <= R ^^ A Int R ^^ B" 
305 
(fn _ => [ Blast_tac 1 ]); 

306 

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

307 
qed_goal "Image_Un" thy "R ^^ (A Un B) = R ^^ A Un R ^^ B" 
4593  308 
(fn _ => [ Blast_tac 1 ]); 
309 

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

310 
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

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

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

313 
(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

314 

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

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

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

319 

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

320 

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

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

322 

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

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

324 
"!!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

325 

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

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

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

329 

330 
(** Graphs of partial functions **) 

331 

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

333 
by (Blast_tac 1); 

334 
qed "Domain_partial_func"; 

335 

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

337 
by (Blast_tac 1); 

338 
qed "Range_partial_func"; 

339 