
1 (* Title: HOL/ex/PER.thy 

2 ID: $Id$ 

3 Author: Oscar Slotosch and Markus Wenzel, TU Muenchen 

4 *) 

5 

6 header {* Partial equivalence relations *} 

7 

8 theory PER = Main: 

9 

10 text {* 

11 Higherorder quotients are defined over partial equivalence relations 

12 (PERs) instead of total ones. We provide axiomatic type classes 

13 @{text "equiv < partial_equiv"} and a type constructor 

14 @{text "'a quot"} with basic operations. This development is based 

15 on: 

16 

17 Oscar Slotosch: \emph{Higher Order Quotients and their Implementation 

18 in Isabelle HOL.} Elsa L. Gunter and Amy Felty, editors, Theorem 

19 Proving in Higher Order Logics: TPHOLs '97, Springer LNCS 1275, 1997. 

20 *} 

21 

22 

23 subsection {* Partial equivalence *} 

24 

25 text {* 

26 Type class @{text partial_equiv} models partial equivalence relations 

27 (PERs) using the polymorphic @{text "\<sim> :: 'a => 'a => bool"} relation, 

28 which is required to be symmetric and transitive, but not necessarily 

29 reflexive. 

30 *} 

31 

32 consts 

33 eqv :: "'a => 'a => bool" (infixl "\<sim>" 50) 

34 

35 axclass partial_equiv < "term" 

36 partial_equiv_sym [elim?]: "x \<sim> y ==> y \<sim> x" 

37 partial_equiv_trans [trans]: "x \<sim> y ==> y \<sim> z ==> x \<sim> z" 

38 

39 text {* 

40 \medskip The domain of a partial equivalence relation is the set of 

41 reflexive elements. Due to symmetry and transitivity this 

42 characterizes exactly those elements that are connected with 

43 \emph{any} other one. 

44 *} 

45 

46 constdefs 

47 domain :: "'a::partial_equiv set" 

48 "domain == {x. x \<sim> x}" 

49 

50 lemma domainI [intro]: "x \<sim> x ==> x \<in> domain" 

51 by (unfold domain_def) blast 

52 

53 lemma domainD [dest]: "x \<in> domain ==> x \<sim> x" 

54 by (unfold domain_def) blast 

55 

56 theorem domainI' [elim?]: "x \<sim> y ==> x \<in> domain" 

57 proof 

58 assume xy: "x \<sim> y" 

59 also from xy have "y \<sim> x" .. 

60 finally show "x \<sim> x" . 

61 qed 

62 

63 

64 subsection {* Equivalence on function spaces *} 

65 

66 text {* 

67 The @{text \<sim>} relation is lifted to function spaces. It is 

68 important to note that this is \emph{not} the direct product, but a 

69 structural one corresponding to the congruence property. 

70 *} 

71 

72 defs (overloaded) 

73 eqv_fun_def: "f \<sim> g == \<forall>x \<in> domain. \<forall>y \<in> domain. x \<sim> y > f x \<sim> g y" 

74 

75 lemma partial_equiv_funI [intro?]: 

76 "(!!x y. x \<in> domain ==> y \<in> domain ==> x \<sim> y ==> f x \<sim> g y) ==> f \<sim> g" 

77 by (unfold eqv_fun_def) blast 

78 

79 lemma partial_equiv_funD [dest?]: 

80 "f \<sim> g ==> x \<in> domain ==> y \<in> domain ==> x \<sim> y ==> f x \<sim> g y" 

81 by (unfold eqv_fun_def) blast 

82 

83 text {* 

84 The class of partial equivalence relations is closed under function 

85 spaces (in \emph{both} argument positions). 

86 *} 

87 

88 instance fun :: (partial_equiv, partial_equiv) partial_equiv 

89 proof 

90 fix f g h :: "'a::partial_equiv => 'b::partial_equiv" 

91 assume fg: "f \<sim> g" 

92 show "g \<sim> f" 

93 proof 

94 fix x y :: 'a 

95 assume x: "x \<in> domain" and y: "y \<in> domain" 

96 assume "x \<sim> y" hence "y \<sim> x" .. 

97 with fg y x have "f y \<sim> g x" .. 

98 thus "g x \<sim> f y" .. 

99 qed 

100 assume gh: "g \<sim> h" 

101 show "f \<sim> h" 

102 proof 

103 fix x y :: 'a 

104 assume x: "x \<in> domain" and y: "y \<in> domain" and "x \<sim> y" 

105 with fg have "f x \<sim> g y" .. 

106 also from y have "y \<sim> y" .. 

107 with gh y y have "g y \<sim> h y" .. 

108 finally show "f x \<sim> h y" . 

109 qed 

110 qed 

111 

112 

113 subsection {* Total equivalence *} 

114 

115 text {* 

116 The class of total equivalence relations on top of PERs. It 

117 coincides with the standard notion of equivalence, i.e.\ 

118 @{text "\<sim> :: 'a => 'a => bool"} is required to be reflexive, transitive 

119 and symmetric. 

120 *} 

121 

122 axclass equiv < partial_equiv 

123 eqv_refl [intro]: "x \<sim> x" 

124 

125 text {* 

126 On total equivalences all elements are reflexive, and congruence 

127 holds unconditionally. 

128 *} 

129 

130 theorem equiv_domain [intro]: "(x::'a::equiv) \<in> domain" 

131 proof 

132 show "x \<sim> x" .. 

133 qed 

134 

135 theorem equiv_cong [dest?]: "f \<sim> g ==> x \<sim> y ==> f x \<sim> g (y::'a::equiv)" 

136 proof  

137 assume "f \<sim> g" 

138 moreover have "x \<in> domain" .. 

139 moreover have "y \<in> domain" .. 

140 moreover assume "x \<sim> y" 

141 ultimately show ?thesis .. 

142 qed 

143 

144 

145 subsection {* Quotient types *} 

146 

147 text {* 

148 The quotient type @{text "'a quot"} consists of all \emph{equivalence 

149 classes} over elements of the base type @{typ 'a}. 

150 *} 

151 

152 typedef 'a quot = "{{x. a \<sim> x} a::'a. True}" 

153 by blast 

154 

155 lemma quotI [intro]: "{x. a \<sim> x} \<in> quot" 

156 by (unfold quot_def) blast 

157 

158 lemma quotE [elim]: "R \<in> quot ==> (!!a. R = {x. a \<sim> x} ==> C) ==> C" 

159 by (unfold quot_def) blast 

160 

161 text {* 

162 \medskip Abstracted equivalence classes are the canonical 

163 representation of elements of a quotient type. 

164 *} 

165 

166 constdefs 

167 eqv_class :: "('a::partial_equiv) => 'a quot" ("\<lfloor>_\<rfloor>") 

168 "\<lfloor>a\<rfloor> == Abs_quot {x. a \<sim> x}" 

169 

170 theorem quot_rep: "\<exists>a. A = \<lfloor>a\<rfloor>" 

171 proof (cases A) 

172 fix R assume R: "A = Abs_quot R" 

173 assume "R \<in> quot" hence "\<exists>a. R = {x. a \<sim> x}" by blast 

174 with R have "\<exists>a. A = Abs_quot {x. a \<sim> x}" by blast 

175 thus ?thesis by (unfold eqv_class_def) 

176 qed 

177 

178 lemma quot_cases [case_names rep, cases type: quot]: 

179 "(!!a. A = \<lfloor>a\<rfloor> ==> C) ==> C" 

180 by (insert quot_rep) blast 

181 

182 

183 subsection {* Equality on quotients *} 

184 

185 text {* 

186 Equality of canonical quotient elements corresponds to the original 

187 relation as follows. 

188 *} 

189 

190 theorem eqv_class_eqI [intro]: "a \<sim> b ==> \<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>" 

191 proof  

192 assume ab: "a \<sim> b" 

193 have "{x. a \<sim> x} = {x. b \<sim> x}" 

194 proof (rule Collect_cong) 

195 fix x show "(a \<sim> x) = (b \<sim> x)" 

196 proof 

197 from ab have "b \<sim> a" .. 

198 also assume "a \<sim> x" 

199 finally show "b \<sim> x" . 

200 next 

201 note ab 

202 also assume "b \<sim> x" 

203 finally show "a \<sim> x" . 

204 qed 

205 qed 

206 thus ?thesis by (simp only: eqv_class_def) 

207 qed 

208 

209 theorem eqv_class_eqD' [dest?]: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor> ==> a \<in> domain ==> a \<sim> b" 

210 proof (unfold eqv_class_def) 

211 assume "Abs_quot {x. a \<sim> x} = Abs_quot {x. b \<sim> x}" 

212 hence "{x. a \<sim> x} = {x. b \<sim> x}" by (simp only: Abs_quot_inject quotI) 

213 moreover assume "a \<in> domain" hence "a \<sim> a" .. 

214 ultimately have "a \<in> {x. b \<sim> x}" by blast 

215 hence "b \<sim> a" by blast 

216 thus "a \<sim> b" .. 

217 qed 

218 

219 theorem eqv_class_eqD [dest?]: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor> ==> a \<sim> (b::'a::equiv)" 

220 proof (rule eqv_class_eqD') 

221 show "a \<in> domain" .. 

222 qed 

223 

224 lemma eqv_class_eq' [simp]: "a \<in> domain ==> (\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> b)" 

225 by (insert eqv_class_eqI eqv_class_eqD') blast 

226 

227 lemma eqv_class_eq [simp]: "(\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> (b::'a::equiv))" 

228 by (insert eqv_class_eqI eqv_class_eqD) blast 

229 

230 

231 subsection {* Picking representing elements *} 

232 

233 constdefs 

234 pick :: "'a::partial_equiv quot => 'a" 

235 "pick A == SOME a. A = \<lfloor>a\<rfloor>" 

236 

237 theorem pick_eqv' [intro?, simp]: "a \<in> domain ==> pick \<lfloor>a\<rfloor> \<sim> a" 

238 proof (unfold pick_def) 

239 assume a: "a \<in> domain" 

240 show "(SOME x. \<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>) \<sim> a" 

241 proof (rule someI2) 

242 show "\<lfloor>a\<rfloor> = \<lfloor>a\<rfloor>" .. 

243 fix x assume "\<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>" 

244 hence "a \<sim> x" .. 

245 thus "x \<sim> a" .. 

246 qed 

247 qed 

248 

249 theorem pick_eqv [intro, simp]: "pick \<lfloor>a\<rfloor> \<sim> (a::'a::equiv)" 

250 proof (rule pick_eqv') 

251 show "a \<in> domain" .. 

252 qed 

253 

254 theorem pick_inverse: "\<lfloor>pick A\<rfloor> = (A::'a::equiv quot)" 

255 proof (cases A) 

256 fix a assume a: "A = \<lfloor>a\<rfloor>" 

257 hence "pick A \<sim> a" by simp 

258 hence "\<lfloor>pick A\<rfloor> = \<lfloor>a\<rfloor>" by simp 

259 with a show ?thesis by simp 

260 qed 

261 

262 end 