author  paulson 
Mon, 11 Oct 1999 10:49:18 +0200  
changeset 7822  09aabe6d04b8 
parent 7083  9663eb2bce05 
child 7913  86be2946bb0b 
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"; 
24 
Addsimps [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 

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

48 
val diagI = refl RS diag_eqI > standard; 
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 

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

66 
Goal "diag(A) <= A Times A"; 
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 

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

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

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

121 

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

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

123 

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

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

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

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

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

128 

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

129 
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

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

131 
qed "reflD"; 
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 
(** Natural deduction for antisym(r) **) 
43c081a0858d
new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents:
6005
diff
changeset

134 

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

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

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

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

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

139 

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

140 
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

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

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

143 

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

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

145 

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

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

148 
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

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

150 

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

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

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

154 

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

156 

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

157 
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

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

160 

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

162 

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

163 
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

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

166 

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

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

170 

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

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

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

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

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

179 
by (assume_tac 1); 

180 
qed "converseE"; 

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

182 

5069  183 
Goalw [converse_def] "(r^1)^1 = r"; 
2891  184 
by (Blast_tac 1); 
4746  185 
qed "converse_converse"; 
186 
Addsimps [converse_converse]; 

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

187 

5069  188 
Goal "(r O s)^1 = s^1 O r^1"; 
4423  189 
by (Blast_tac 1); 
4746  190 
qed "converse_comp"; 
1605  191 

5608  192 
Goal "Id^1 = Id"; 
4644  193 
by (Blast_tac 1); 
5608  194 
qed "converse_Id"; 
195 
Addsimps [converse_Id]; 

4644  196 

5995  197 
Goal "(diag A) ^1 = diag A"; 
198 
by (Blast_tac 1); 

199 
qed "converse_diag"; 

200 
Addsimps [converse_diag]; 

201 

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

204 
qed "refl_converse"; 

205 

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

207 
by (Blast_tac 1); 

208 
qed "antisym_converse"; 

209 

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

211 
by (Blast_tac 1); 

212 
qed "trans_converse"; 

213 

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

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

215 

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

218 
qed "Domain_iff"; 

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

219 

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

222 
qed "DomainI"; 

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

223 

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

226 
by (REPEAT (ares_tac prems 1)) ; 

227 
qed "DomainE"; 

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

228 

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

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

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

231 

5608  232 
Goal "Domain Id = UNIV"; 
4644  233 
by (Blast_tac 1); 
5608  234 
qed "Domain_Id"; 
235 
Addsimps [Domain_Id]; 

4644  236 

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

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

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

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

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

241 

5811  242 
Goal "Domain(A Un B) = Domain(A) Un Domain(B)"; 
243 
by (Blast_tac 1); 

244 
qed "Domain_Un_eq"; 

245 

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

247 
by (Blast_tac 1); 

248 
qed "Domain_Int_subset"; 

249 

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

251 
by (Blast_tac 1); 

252 
qed "Domain_Diff_subset"; 

253 

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

256 
qed "Domain_Union"; 

257 

7822  258 
Goal "r <= s ==> Domain r <= Domain s"; 
259 
by (Blast_tac 1); 

260 
qed "Domain_mono"; 

261 

5811  262 

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

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

264 

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

267 
qed "Range_iff"; 

268 

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

271 
qed "RangeI"; 

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

272 

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

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

276 
by (resolve_tac prems 1); 

277 
by (etac converseD 1) ; 

278 
qed "RangeE"; 

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

279 

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

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

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

282 

5608  283 
Goal "Range Id = UNIV"; 
4644  284 
by (Blast_tac 1); 
5608  285 
qed "Range_Id"; 
286 
Addsimps [Range_Id]; 

4644  287 

5995  288 
Goal "Range (diag A) = A"; 
289 
by Auto_tac; 

290 
qed "Range_diag"; 

291 
Addsimps [Range_diag]; 

292 

5811  293 
Goal "Range(A Un B) = Range(A) Un Range(B)"; 
294 
by (Blast_tac 1); 

295 
qed "Range_Un_eq"; 

296 

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

298 
by (Blast_tac 1); 

299 
qed "Range_Int_subset"; 

300 

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

302 
by (Blast_tac 1); 

303 
qed "Range_Diff_subset"; 

304 

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

307 
qed "Range_Union"; 

308 

5811  309 

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

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

311 

5649  312 
overload_1st_set "Relation.op ^^"; 
5335  313 

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

316 
qed "Image_iff"; 

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

317 

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

320 
qed "Image_singleton"; 

4673  321 

7031  322 
Goal "(b : r^^{a}) = ((a,b):r)"; 
7007  323 
by (rtac (Image_iff RS trans) 1); 
324 
by (Blast_tac 1); 

325 
qed "Image_singleton_iff"; 

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

326 

4673  327 
AddIffs [Image_singleton_iff]; 
328 

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

331 
qed "ImageI"; 

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

332 

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

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

336 
by (Clarify_tac 1); 

337 
by (rtac (hd prems) 1); 

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

339 
qed "ImageE"; 

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

340 

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

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

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

343 

4593  344 

7031  345 
Goal "R^^{} = {}"; 
7007  346 
by (Blast_tac 1); 
347 
qed "Image_empty"; 

4593  348 

349 
Addsimps [Image_empty]; 

350 

5608  351 
Goal "Id ^^ A = A"; 
4601  352 
by (Blast_tac 1); 
5608  353 
qed "Image_Id"; 
4601  354 

5998  355 
Goal "diag A ^^ B = A Int B"; 
5995  356 
by (Blast_tac 1); 
357 
qed "Image_diag"; 

358 

359 
Addsimps [Image_Id, Image_diag]; 

4601  360 

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

363 
qed "Image_Int_subset"; 

4593  364 

7007  365 
Goal "R ^^ (A Un B) = R ^^ A Un R ^^ B"; 
366 
by (Blast_tac 1); 

367 
qed "Image_Un"; 

4593  368 

7007  369 
Goal "r <= A Times B ==> r^^C <= B"; 
370 
by (rtac subsetI 1); 

371 
by (REPEAT (eresolve_tac [asm_rl, ImageE, subsetD RS SigmaD2] 1)) ; 

372 
qed "Image_subset"; 

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

373 

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

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

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

378 

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

379 

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

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

381 

7031  382 
Goalw [Univalent_def] 
383 
"!x y. (x,y):r > (!z. (x,z):r > y=z) ==> Univalent r"; 

384 
by (assume_tac 1); 

385 
qed "UnivalentI"; 

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

386 

7031  387 
Goalw [Univalent_def] 
388 
"[ Univalent r; (x,y):r; (x,z):r] ==> y=z"; 

389 
by Auto_tac; 

390 
qed "UnivalentD"; 

5231  391 

392 

393 
(** Graphs of partial functions **) 

394 

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

396 
by (Blast_tac 1); 

397 
qed "Domain_partial_func"; 

398 

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

400 
by (Blast_tac 1); 

401 
qed "Range_partial_func"; 

402 

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

403 

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

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

405 

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

406 
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

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

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

409 

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

410 
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

411 
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

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

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

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

415 
by (rtac (select_eq_Ex RS iffD2) 1); 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
7007
diff
changeset

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

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

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

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

420 
by (rtac (select1_equality RS sym) 1); 
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
7007
diff
changeset

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

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

423 
qed "fun_rel_comp_unique"; 