author  paulson 
Fri, 05 Jan 2001 10:19:14 +0100  
changeset 10786  04ee73606993 
parent 9969  4753185f1dd2 
child 10797  028d22926a41 
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 

10786  236 
Goal "Domain {} = {}"; 
237 
by (Blast_tac 1); 

238 
qed "Domain_empty"; 

239 
Addsimps [Domain_empty]; 

240 

241 
Goal "Domain (insert (a, b) r) = insert a (Domain r)"; 

242 
by (Blast_tac 1); 

243 
qed "Domain_insert"; 

244 

5608  245 
Goal "Domain Id = UNIV"; 
4644  246 
by (Blast_tac 1); 
5608  247 
qed "Domain_Id"; 
248 
Addsimps [Domain_Id]; 

4644  249 

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

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

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

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

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

254 

5811  255 
Goal "Domain(A Un B) = Domain(A) Un Domain(B)"; 
256 
by (Blast_tac 1); 

257 
qed "Domain_Un_eq"; 

258 

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

260 
by (Blast_tac 1); 

261 
qed "Domain_Int_subset"; 

262 

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

264 
by (Blast_tac 1); 

265 
qed "Domain_Diff_subset"; 

266 

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

269 
qed "Domain_Union"; 

270 

7822  271 
Goal "r <= s ==> Domain r <= Domain s"; 
272 
by (Blast_tac 1); 

273 
qed "Domain_mono"; 

274 

5811  275 

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

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

277 

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

280 
qed "Range_iff"; 

281 

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

284 
qed "RangeI"; 

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

285 

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

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

289 
by (resolve_tac prems 1); 

290 
by (etac converseD 1) ; 

291 
qed "RangeE"; 

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

292 

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

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

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

295 

10786  296 
Goal "Range {} = {}"; 
297 
by (Blast_tac 1); 

298 
qed "Range_empty"; 

299 
Addsimps [Range_empty]; 

300 

301 
Goal "Range (insert (a, b) r) = insert b (Range r)"; 

302 
by (Blast_tac 1); 

303 
qed "Range_insert"; 

304 

5608  305 
Goal "Range Id = UNIV"; 
4644  306 
by (Blast_tac 1); 
5608  307 
qed "Range_Id"; 
308 
Addsimps [Range_Id]; 

4644  309 

5995  310 
Goal "Range (diag A) = A"; 
311 
by Auto_tac; 

312 
qed "Range_diag"; 

313 
Addsimps [Range_diag]; 

314 

5811  315 
Goal "Range(A Un B) = Range(A) Un Range(B)"; 
316 
by (Blast_tac 1); 

317 
qed "Range_Un_eq"; 

318 

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

320 
by (Blast_tac 1); 

321 
qed "Range_Int_subset"; 

322 

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

324 
by (Blast_tac 1); 

325 
qed "Range_Diff_subset"; 

326 

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

329 
qed "Range_Union"; 

330 

5811  331 

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

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

333 

8004  334 
overload_1st_set "Relation.Image"; 
5335  335 

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

338 
qed "Image_iff"; 

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

339 

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

342 
qed "Image_singleton"; 

4673  343 

7031  344 
Goal "(b : r^^{a}) = ((a,b):r)"; 
7007  345 
by (rtac (Image_iff RS trans) 1); 
346 
by (Blast_tac 1); 

347 
qed "Image_singleton_iff"; 

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

348 

4673  349 
AddIffs [Image_singleton_iff]; 
350 

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

353 
qed "ImageI"; 

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

354 

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

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

358 
by (Clarify_tac 1); 

359 
by (rtac (hd prems) 1); 

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

361 
qed "ImageE"; 

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

362 

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

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

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

365 

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

368 
by (Blast_tac 1); 

369 
qed "rev_ImageI"; 

370 

7031  371 
Goal "R^^{} = {}"; 
7007  372 
by (Blast_tac 1); 
373 
qed "Image_empty"; 

4593  374 

375 
Addsimps [Image_empty]; 

376 

5608  377 
Goal "Id ^^ A = A"; 
4601  378 
by (Blast_tac 1); 
5608  379 
qed "Image_Id"; 
4601  380 

5998  381 
Goal "diag A ^^ B = A Int B"; 
5995  382 
by (Blast_tac 1); 
383 
qed "Image_diag"; 

384 

385 
Addsimps [Image_Id, Image_diag]; 

4601  386 

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

389 
qed "Image_Int_subset"; 

4593  390 

7007  391 
Goal "R ^^ (A Un B) = R ^^ A Un R ^^ B"; 
392 
by (Blast_tac 1); 

393 
qed "Image_Un"; 

4593  394 

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

398 
qed "Image_subset"; 

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

399 

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

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

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

404 

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

407 
qed "Image_mono"; 

408 

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

410 
by (Blast_tac 1); 

411 
qed "Image_UN"; 

412 

413 
(*Converse inclusion fails*) 

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

415 
by (Blast_tac 1); 

416 
qed "Image_INT_subset"; 

417 

8004  418 
Goal "(r^^A <= B) = (A <=  ((r^1) ^^ (B)))"; 
419 
by (Blast_tac 1); 

420 
qed "Image_subset_eq"; 

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

421 

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

423 

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

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

428 

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

7031  431 
by Auto_tac; 
8268  432 
qed "univalentD"; 
5231  433 

434 

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

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

436 

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

437 
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

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

439 
qed "Domain_Collect_split"; 
5231  440 

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

441 
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

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

443 
qed "Range_Collect_split"; 
5231  444 

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

445 
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

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

447 
qed "Image_Collect_split"; 
5231  448 

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

449 
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

450 

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

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

452 

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

453 
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

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

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

456 

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

457 
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

458 
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

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

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

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

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

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

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

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

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

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

470 
qed "fun_rel_comp_unique"; 