author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 9969  4753185f1dd2 
child 10786  04ee73606993 
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 
(** Identity relation **) 
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

8 

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

12 

5608  13 
val major::prems = Goalw [Id_def] 
14 
"[ 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

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

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

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

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

20 

5608  21 
Goalw [Id_def] "(a,b):Id = (a=b)"; 
2891  22 
by (Blast_tac 1); 
5608  23 
qed "pair_in_Id_conv"; 
8265  24 
AddIffs [pair_in_Id_conv]; 
1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

25 

6806
43c081a0858d
new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents:
6005
diff
changeset

26 
Goalw [refl_def] "reflexive Id"; 
43c081a0858d
new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents:
6005
diff
changeset

27 
by Auto_tac; 
43c081a0858d
new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents:
6005
diff
changeset

28 
qed "reflexive_Id"; 
43c081a0858d
new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents:
6005
diff
changeset

29 

43c081a0858d
new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents:
6005
diff
changeset

30 
(*A strange result, since Id is also symmetric.*) 
43c081a0858d
new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents:
6005
diff
changeset

31 
Goalw [antisym_def] "antisym Id"; 
43c081a0858d
new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents:
6005
diff
changeset

32 
by Auto_tac; 
43c081a0858d
new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents:
6005
diff
changeset

33 
qed "antisym_Id"; 
43c081a0858d
new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents:
6005
diff
changeset

34 

43c081a0858d
new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents:
6005
diff
changeset

35 
Goalw [trans_def] "trans Id"; 
43c081a0858d
new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents:
6005
diff
changeset

36 
by Auto_tac; 
43c081a0858d
new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents:
6005
diff
changeset

37 
qed "trans_Id"; 
43c081a0858d
new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents:
6005
diff
changeset

38 

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

39 

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

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

41 

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

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

43 

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

44 
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

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

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

47 

9108  48 
bind_thm ("diagI", refl RS diag_eqI > standard); 
5978
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5811
diff
changeset

49 

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

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

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

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

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

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

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

56 
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

57 
qed "diagE"; 
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 
AddSIs [diagI]; 
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5811
diff
changeset

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

61 

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

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

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

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

65 

8703  66 
Goal "diag(A) <= A <*> A"; 
5978
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5811
diff
changeset

67 
by (Blast_tac 1); 
5995  68 
qed "diag_subset_Times"; 
5978
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5811
diff
changeset

69 

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

70 

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

71 

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

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

73 

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

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

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

78 

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

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

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

82 
\ !!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

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

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

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

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

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

88 

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

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

91 
\ !!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

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

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

94 
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

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

96 

5608  97 
AddIs [compI, IdI]; 
98 
AddSEs [compE, IdE]; 

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

99 

5608  100 
Goal "R O Id = R"; 
4673  101 
by (Fast_tac 1); 
5608  102 
qed "R_O_Id"; 
4673  103 

5608  104 
Goal "Id O R = R"; 
4673  105 
by (Fast_tac 1); 
5608  106 
qed "Id_O_R"; 
4673  107 

5608  108 
Addsimps [R_O_Id,Id_O_R]; 
4673  109 

5069  110 
Goal "(R O S) O T = R O (S O T)"; 
4830  111 
by (Blast_tac 1); 
112 
qed "O_assoc"; 

113 

9113  114 
Goalw [trans_def] "trans r ==> r O r <= r"; 
115 
by (Blast_tac 1); 

116 
qed "trans_O_subset"; 

117 

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

118 
Goal "[ r'<=r; s'<=s ] ==> (r' O s') <= (r O s)"; 
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 "comp_mono"; 
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

121 

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

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

125 

6806
43c081a0858d
new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents:
6005
diff
changeset

126 
(** Natural deduction for refl(r) **) 
43c081a0858d
new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents:
6005
diff
changeset

127 

43c081a0858d
new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents:
6005
diff
changeset

128 
val prems = Goalw [refl_def] 
8703  129 
"[ r <= A <*> A; !! x. x:A ==> (x,x):r ] ==> refl A r"; 
6806
43c081a0858d
new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents:
6005
diff
changeset

130 
by (REPEAT (ares_tac (prems@[ballI,conjI]) 1)); 
43c081a0858d
new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents:
6005
diff
changeset

131 
qed "reflI"; 
43c081a0858d
new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents:
6005
diff
changeset

132 

43c081a0858d
new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents:
6005
diff
changeset

133 
Goalw [refl_def] "[ refl A r; a:A ] ==> (a,a):r"; 
43c081a0858d
new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents:
6005
diff
changeset

134 
by (Blast_tac 1); 
43c081a0858d
new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents:
6005
diff
changeset

135 
qed "reflD"; 
43c081a0858d
new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents:
6005
diff
changeset

136 

43c081a0858d
new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents:
6005
diff
changeset

137 
(** Natural deduction for antisym(r) **) 
43c081a0858d
new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents:
6005
diff
changeset

138 

43c081a0858d
new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents:
6005
diff
changeset

139 
val prems = Goalw [antisym_def] 
43c081a0858d
new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents:
6005
diff
changeset

140 
"(!! x y. [ (x,y):r; (y,x):r ] ==> x=y) ==> antisym(r)"; 
43c081a0858d
new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents:
6005
diff
changeset

141 
by (REPEAT (ares_tac (prems@[allI,impI]) 1)); 
43c081a0858d
new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents:
6005
diff
changeset

142 
qed "antisymI"; 
43c081a0858d
new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents:
6005
diff
changeset

143 

43c081a0858d
new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents:
6005
diff
changeset

144 
Goalw [antisym_def] "[ antisym(r); (a,b):r; (b,a):r ] ==> a=b"; 
43c081a0858d
new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents:
6005
diff
changeset

145 
by (Blast_tac 1); 
43c081a0858d
new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents:
6005
diff
changeset

146 
qed "antisymD"; 
43c081a0858d
new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents:
6005
diff
changeset

147 

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

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

149 

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

151 
"(!! 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

152 
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

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

154 

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

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

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

158 

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

160 

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

161 
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

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

164 

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

166 

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

167 
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

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

170 

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

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

174 

4746  175 
(*More general than converseD, as it "splits" the member of the relation*) 
7031  176 

177 
val [major,minor] = Goalw [converse_def] 

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

179 
\ !!x y. [ yx=(y,x); (x,y):r ] ==> P \ 
7031  180 
\ ] ==> P"; 
181 
by (rtac (major RS CollectE) 1); 

182 
by (REPEAT (eresolve_tac [splitE, bexE,exE, conjE, minor] 1)); 

183 
by (assume_tac 1); 

184 
qed "converseE"; 

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

186 

5069  187 
Goalw [converse_def] "(r^1)^1 = r"; 
2891  188 
by (Blast_tac 1); 
4746  189 
qed "converse_converse"; 
190 
Addsimps [converse_converse]; 

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

191 

5069  192 
Goal "(r O s)^1 = s^1 O r^1"; 
4423  193 
by (Blast_tac 1); 
4746  194 
qed "converse_comp"; 
1605  195 

5608  196 
Goal "Id^1 = Id"; 
4644  197 
by (Blast_tac 1); 
5608  198 
qed "converse_Id"; 
199 
Addsimps [converse_Id]; 

4644  200 

5995  201 
Goal "(diag A) ^1 = diag A"; 
202 
by (Blast_tac 1); 

203 
qed "converse_diag"; 

204 
Addsimps [converse_diag]; 

205 

7083  206 
Goalw [refl_def] "refl A r ==> refl A (converse r)"; 
207 
by (Blast_tac 1); 

208 
qed "refl_converse"; 

209 

210 
Goalw [antisym_def] "antisym (converse r) = antisym r"; 

211 
by (Blast_tac 1); 

212 
qed "antisym_converse"; 

213 

214 
Goalw [trans_def] "trans (converse r) = trans r"; 

215 
by (Blast_tac 1); 

216 
qed "trans_converse"; 

217 

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

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

219 

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

222 
qed "Domain_iff"; 

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

223 

7007  224 
Goal "(a,b): r ==> a: Domain(r)"; 
225 
by (etac (exI RS (Domain_iff RS iffD2)) 1) ; 

226 
qed "DomainI"; 

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

227 

7007  228 
val prems= Goal "[ a : Domain(r); !!y. (a,y): r ==> P ] ==> P"; 
229 
by (rtac (Domain_iff RS iffD1 RS exE) 1); 

230 
by (REPEAT (ares_tac prems 1)) ; 

231 
qed "DomainE"; 

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

232 

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

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

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

235 

5608  236 
Goal "Domain Id = UNIV"; 
4644  237 
by (Blast_tac 1); 
5608  238 
qed "Domain_Id"; 
239 
Addsimps [Domain_Id]; 

4644  240 

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

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

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

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

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

245 

5811  246 
Goal "Domain(A Un B) = Domain(A) Un Domain(B)"; 
247 
by (Blast_tac 1); 

248 
qed "Domain_Un_eq"; 

249 

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

251 
by (Blast_tac 1); 

252 
qed "Domain_Int_subset"; 

253 

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

255 
by (Blast_tac 1); 

256 
qed "Domain_Diff_subset"; 

257 

6005  258 
Goal "Domain (Union S) = (UN A:S. Domain A)"; 
259 
by (Blast_tac 1); 

260 
qed "Domain_Union"; 

261 

7822  262 
Goal "r <= s ==> Domain r <= Domain s"; 
263 
by (Blast_tac 1); 

264 
qed "Domain_mono"; 

265 

5811  266 

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

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

268 

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

271 
qed "Range_iff"; 

272 

7031  273 
Goalw [Range_def] "(a,b): r ==> b : Range(r)"; 
274 
by (etac (converseI RS DomainI) 1); 

275 
qed "RangeI"; 

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

276 

7031  277 
val major::prems = Goalw [Range_def] 
278 
"[ b : Range(r); !!x. (x,b): r ==> P ] ==> P"; 

279 
by (rtac (major RS DomainE) 1); 

280 
by (resolve_tac prems 1); 

281 
by (etac converseD 1) ; 

282 
qed "RangeE"; 

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

283 

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

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

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

286 

5608  287 
Goal "Range Id = UNIV"; 
4644  288 
by (Blast_tac 1); 
5608  289 
qed "Range_Id"; 
290 
Addsimps [Range_Id]; 

4644  291 

5995  292 
Goal "Range (diag A) = A"; 
293 
by Auto_tac; 

294 
qed "Range_diag"; 

295 
Addsimps [Range_diag]; 

296 

5811  297 
Goal "Range(A Un B) = Range(A) Un Range(B)"; 
298 
by (Blast_tac 1); 

299 
qed "Range_Un_eq"; 

300 

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

302 
by (Blast_tac 1); 

303 
qed "Range_Int_subset"; 

304 

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

306 
by (Blast_tac 1); 

307 
qed "Range_Diff_subset"; 

308 

6005  309 
Goal "Range (Union S) = (UN A:S. Range A)"; 
310 
by (Blast_tac 1); 

311 
qed "Range_Union"; 

312 

5811  313 

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

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

315 

8004  316 
overload_1st_set "Relation.Image"; 
5335  317 

7031  318 
Goalw [Image_def] "b : r^^A = (? x:A. (x,b):r)"; 
319 
by (Blast_tac 1); 

320 
qed "Image_iff"; 

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

321 

7031  322 
Goalw [Image_def] "r^^{a} = {b. (a,b):r}"; 
323 
by (Blast_tac 1); 

324 
qed "Image_singleton"; 

4673  325 

7031  326 
Goal "(b : r^^{a}) = ((a,b):r)"; 
7007  327 
by (rtac (Image_iff RS trans) 1); 
328 
by (Blast_tac 1); 

329 
qed "Image_singleton_iff"; 

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

330 

4673  331 
AddIffs [Image_singleton_iff]; 
332 

7007  333 
Goalw [Image_def] "[ (a,b): r; a:A ] ==> b : r^^A"; 
334 
by (Blast_tac 1); 

335 
qed "ImageI"; 

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

336 

7031  337 
val major::prems = Goalw [Image_def] 
338 
"[ b: r^^A; !!x.[ (x,b): r; x:A ] ==> P ] ==> P"; 

339 
by (rtac (major RS CollectE) 1); 

340 
by (Clarify_tac 1); 

341 
by (rtac (hd prems) 1); 

342 
by (REPEAT (etac bexE 1 ORELSE ares_tac prems 1)) ; 

343 
qed "ImageE"; 

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

344 

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

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

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

347 

8174  348 
(*This version's more effective when we already have the required "a"*) 
349 
Goal "[ a:A; (a,b): r ] ==> b : r^^A"; 

350 
by (Blast_tac 1); 

351 
qed "rev_ImageI"; 

352 

4593  353 

7031  354 
Goal "R^^{} = {}"; 
7007  355 
by (Blast_tac 1); 
356 
qed "Image_empty"; 

4593  357 

358 
Addsimps [Image_empty]; 

359 

5608  360 
Goal "Id ^^ A = A"; 
4601  361 
by (Blast_tac 1); 
5608  362 
qed "Image_Id"; 
4601  363 

5998  364 
Goal "diag A ^^ B = A Int B"; 
5995  365 
by (Blast_tac 1); 
366 
qed "Image_diag"; 

367 

368 
Addsimps [Image_Id, Image_diag]; 

4601  369 

7007  370 
Goal "R ^^ (A Int B) <= R ^^ A Int R ^^ B"; 
371 
by (Blast_tac 1); 

372 
qed "Image_Int_subset"; 

4593  373 

7007  374 
Goal "R ^^ (A Un B) = R ^^ A Un R ^^ B"; 
375 
by (Blast_tac 1); 

376 
qed "Image_Un"; 

4593  377 

8703  378 
Goal "r <= A <*> B ==> r^^C <= B"; 
7007  379 
by (rtac subsetI 1); 
380 
by (REPEAT (eresolve_tac [asm_rl, ImageE, subsetD RS SigmaD2] 1)) ; 

381 
qed "Image_subset"; 

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

382 

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

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

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

387 

7913  388 
Goal "[ r'<=r; A'<=A ] ==> (r' ^^ A') <= (r ^^ A)"; 
389 
by (Blast_tac 1); 

390 
qed "Image_mono"; 

391 

392 
Goal "(r ^^ (UNION A B)) = (UN x:A.(r ^^ (B x)))"; 

393 
by (Blast_tac 1); 

394 
qed "Image_UN"; 

395 

396 
(*Converse inclusion fails*) 

397 
Goal "(r ^^ (INTER A B)) <= (INT x:A.(r ^^ (B x)))"; 

398 
by (Blast_tac 1); 

399 
qed "Image_INT_subset"; 

400 

8004  401 
Goal "(r^^A <= B) = (A <=  ((r^1) ^^ (B)))"; 
402 
by (Blast_tac 1); 

403 
qed "Image_subset_eq"; 

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

404 

8268  405 
section "univalent"; 
4760
9cdbd5a1d25a
added introduction and elimination rules for Univalent
oheimb
parents:
4746
diff
changeset

406 

8268  407 
Goalw [univalent_def] 
408 
"!x y. (x,y):r > (!z. (x,z):r > y=z) ==> univalent r"; 

7031  409 
by (assume_tac 1); 
8268  410 
qed "univalentI"; 
4760
9cdbd5a1d25a
added introduction and elimination rules for Univalent
oheimb
parents:
4746
diff
changeset

411 

8268  412 
Goalw [univalent_def] 
413 
"[ univalent r; (x,y):r; (x,z):r] ==> y=z"; 

7031  414 
by Auto_tac; 
8268  415 
qed "univalentD"; 
5231  416 

417 

9097
44cd0f9f8e5b
generalized {Domain,Range}_partial_func to {Domain,Range}_Collect_split
paulson
parents:
8703
diff
changeset

418 
(** Graphs given by Collect **) 
44cd0f9f8e5b
generalized {Domain,Range}_partial_func to {Domain,Range}_Collect_split
paulson
parents:
8703
diff
changeset

419 

44cd0f9f8e5b
generalized {Domain,Range}_partial_func to {Domain,Range}_Collect_split
paulson
parents:
8703
diff
changeset

420 
Goal "Domain{(x,y). P x y} = {x. EX y. P x y}"; 
44cd0f9f8e5b
generalized {Domain,Range}_partial_func to {Domain,Range}_Collect_split
paulson
parents:
8703
diff
changeset

421 
by Auto_tac; 
44cd0f9f8e5b
generalized {Domain,Range}_partial_func to {Domain,Range}_Collect_split
paulson
parents:
8703
diff
changeset

422 
qed "Domain_Collect_split"; 
5231  423 

9097
44cd0f9f8e5b
generalized {Domain,Range}_partial_func to {Domain,Range}_Collect_split
paulson
parents:
8703
diff
changeset

424 
Goal "Range{(x,y). P x y} = {y. EX x. P x y}"; 
44cd0f9f8e5b
generalized {Domain,Range}_partial_func to {Domain,Range}_Collect_split
paulson
parents:
8703
diff
changeset

425 
by Auto_tac; 
44cd0f9f8e5b
generalized {Domain,Range}_partial_func to {Domain,Range}_Collect_split
paulson
parents:
8703
diff
changeset

426 
qed "Range_Collect_split"; 
5231  427 

9097
44cd0f9f8e5b
generalized {Domain,Range}_partial_func to {Domain,Range}_Collect_split
paulson
parents:
8703
diff
changeset

428 
Goal "{(x,y). P x y} ^^ A = {y. EX x:A. P x y}"; 
44cd0f9f8e5b
generalized {Domain,Range}_partial_func to {Domain,Range}_Collect_split
paulson
parents:
8703
diff
changeset

429 
by Auto_tac; 
44cd0f9f8e5b
generalized {Domain,Range}_partial_func to {Domain,Range}_Collect_split
paulson
parents:
8703
diff
changeset

430 
qed "Image_Collect_split"; 
5231  431 

9097
44cd0f9f8e5b
generalized {Domain,Range}_partial_func to {Domain,Range}_Collect_split
paulson
parents:
8703
diff
changeset

432 
Addsimps [Domain_Collect_split, Range_Collect_split, Image_Collect_split]; 
7014
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
7007
diff
changeset

433 

11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
7007
diff
changeset

434 
(** Composition of function and relation **) 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
7007
diff
changeset

435 

11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
7007
diff
changeset

436 
Goalw [fun_rel_comp_def] "A <= B ==> fun_rel_comp f A <= fun_rel_comp f B"; 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
7007
diff
changeset

437 
by (Fast_tac 1); 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
7007
diff
changeset

438 
qed "fun_rel_comp_mono"; 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
7007
diff
changeset

439 

11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
7007
diff
changeset

440 
Goalw [fun_rel_comp_def] "! x. ?! y. (f x, y) : R ==> ?! g. g : fun_rel_comp f R"; 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
7007
diff
changeset

441 
by (res_inst_tac [("a","%x. @y. (f x, y) : R")] ex1I 1); 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
7007
diff
changeset

442 
by (rtac CollectI 1); 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
7007
diff
changeset

443 
by (rtac allI 1); 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
7007
diff
changeset

444 
by (etac allE 1); 
9969  445 
by (rtac (some_eq_ex RS iffD2) 1); 
7014
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
7007
diff
changeset

446 
by (etac ex1_implies_ex 1); 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
7007
diff
changeset

447 
by (rtac ext 1); 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
7007
diff
changeset

448 
by (etac CollectE 1); 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
7007
diff
changeset

449 
by (REPEAT (etac allE 1)); 
9969  450 
by (rtac (some1_equality RS sym) 1); 
7014
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
7007
diff
changeset

451 
by (atac 1); 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
7007
diff
changeset

452 
by (atac 1); 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
7007
diff
changeset

453 
qed "fun_rel_comp_unique"; 