author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 10352  638e1fc6ca74 
child 12338  de0f4a63baa5 
permissions  rwrr 
10352
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

1 
(* Title: HOL/ex/PER.thy 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

2 
ID: $Id$ 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

3 
Author: Oscar Slotosch and Markus Wenzel, TU Muenchen 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

4 
*) 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

5 

638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

6 
header {* Partial equivalence relations *} 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

7 

638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

8 
theory PER = Main: 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

9 

638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

10 
text {* 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

11 
Higherorder quotients are defined over partial equivalence relations 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

12 
(PERs) instead of total ones. We provide axiomatic type classes 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

13 
@{text "equiv < partial_equiv"} and a type constructor 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

14 
@{text "'a quot"} with basic operations. This development is based 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

15 
on: 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

16 

638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

17 
Oscar Slotosch: \emph{Higher Order Quotients and their Implementation 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

18 
in Isabelle HOL.} Elsa L. Gunter and Amy Felty, editors, Theorem 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

19 
Proving in Higher Order Logics: TPHOLs '97, Springer LNCS 1275, 1997. 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

20 
*} 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

21 

638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

22 

638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

23 
subsection {* Partial equivalence *} 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

24 

638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

25 
text {* 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

26 
Type class @{text partial_equiv} models partial equivalence relations 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

27 
(PERs) using the polymorphic @{text "\<sim> :: 'a => 'a => bool"} relation, 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

28 
which is required to be symmetric and transitive, but not necessarily 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

29 
reflexive. 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

30 
*} 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

31 

638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

32 
consts 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

33 
eqv :: "'a => 'a => bool" (infixl "\<sim>" 50) 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

34 

638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

35 
axclass partial_equiv < "term" 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

36 
partial_equiv_sym [elim?]: "x \<sim> y ==> y \<sim> x" 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

37 
partial_equiv_trans [trans]: "x \<sim> y ==> y \<sim> z ==> x \<sim> z" 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

38 

638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

39 
text {* 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

40 
\medskip The domain of a partial equivalence relation is the set of 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

41 
reflexive elements. Due to symmetry and transitivity this 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

42 
characterizes exactly those elements that are connected with 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

43 
\emph{any} other one. 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

44 
*} 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

45 

638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

46 
constdefs 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

47 
domain :: "'a::partial_equiv set" 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

48 
"domain == {x. x \<sim> x}" 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

49 

638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

50 
lemma domainI [intro]: "x \<sim> x ==> x \<in> domain" 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

51 
by (unfold domain_def) blast 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

52 

638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

53 
lemma domainD [dest]: "x \<in> domain ==> x \<sim> x" 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

54 
by (unfold domain_def) blast 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

55 

638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

56 
theorem domainI' [elim?]: "x \<sim> y ==> x \<in> domain" 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

57 
proof 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

58 
assume xy: "x \<sim> y" 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

59 
also from xy have "y \<sim> x" .. 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

60 
finally show "x \<sim> x" . 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

61 
qed 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

62 

638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

63 

638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

64 
subsection {* Equivalence on function spaces *} 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

65 

638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

66 
text {* 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

67 
The @{text \<sim>} relation is lifted to function spaces. It is 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

68 
important to note that this is \emph{not} the direct product, but a 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

69 
structural one corresponding to the congruence property. 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

70 
*} 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

71 

638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

72 
defs (overloaded) 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

73 
eqv_fun_def: "f \<sim> g == \<forall>x \<in> domain. \<forall>y \<in> domain. x \<sim> y > f x \<sim> g y" 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

74 

638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

75 
lemma partial_equiv_funI [intro?]: 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

76 
"(!!x y. x \<in> domain ==> y \<in> domain ==> x \<sim> y ==> f x \<sim> g y) ==> f \<sim> g" 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

77 
by (unfold eqv_fun_def) blast 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

78 

638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

79 
lemma partial_equiv_funD [dest?]: 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

80 
"f \<sim> g ==> x \<in> domain ==> y \<in> domain ==> x \<sim> y ==> f x \<sim> g y" 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

81 
by (unfold eqv_fun_def) blast 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

82 

638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

83 
text {* 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

84 
The class of partial equivalence relations is closed under function 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

85 
spaces (in \emph{both} argument positions). 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

86 
*} 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

87 

638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

88 
instance fun :: (partial_equiv, partial_equiv) partial_equiv 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

89 
proof 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

90 
fix f g h :: "'a::partial_equiv => 'b::partial_equiv" 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

91 
assume fg: "f \<sim> g" 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

92 
show "g \<sim> f" 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

93 
proof 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

94 
fix x y :: 'a 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

95 
assume x: "x \<in> domain" and y: "y \<in> domain" 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

96 
assume "x \<sim> y" hence "y \<sim> x" .. 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

97 
with fg y x have "f y \<sim> g x" .. 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

98 
thus "g x \<sim> f y" .. 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

99 
qed 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

100 
assume gh: "g \<sim> h" 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

101 
show "f \<sim> h" 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

102 
proof 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

103 
fix x y :: 'a 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

104 
assume x: "x \<in> domain" and y: "y \<in> domain" and "x \<sim> y" 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

105 
with fg have "f x \<sim> g y" .. 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

106 
also from y have "y \<sim> y" .. 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

107 
with gh y y have "g y \<sim> h y" .. 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

108 
finally show "f x \<sim> h y" . 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

109 
qed 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

110 
qed 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

111 

638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

112 

638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

113 
subsection {* Total equivalence *} 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

114 

638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

115 
text {* 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

116 
The class of total equivalence relations on top of PERs. It 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

117 
coincides with the standard notion of equivalence, i.e.\ 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

118 
@{text "\<sim> :: 'a => 'a => bool"} is required to be reflexive, transitive 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

119 
and symmetric. 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

120 
*} 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

121 

638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

122 
axclass equiv < partial_equiv 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

123 
eqv_refl [intro]: "x \<sim> x" 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

124 

638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

125 
text {* 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

126 
On total equivalences all elements are reflexive, and congruence 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

127 
holds unconditionally. 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

128 
*} 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

129 

638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

130 
theorem equiv_domain [intro]: "(x::'a::equiv) \<in> domain" 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

131 
proof 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

132 
show "x \<sim> x" .. 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

133 
qed 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

134 

638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

135 
theorem equiv_cong [dest?]: "f \<sim> g ==> x \<sim> y ==> f x \<sim> g (y::'a::equiv)" 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

136 
proof  
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

137 
assume "f \<sim> g" 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

138 
moreover have "x \<in> domain" .. 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

139 
moreover have "y \<in> domain" .. 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

140 
moreover assume "x \<sim> y" 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

141 
ultimately show ?thesis .. 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

142 
qed 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

143 

638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

144 

638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

145 
subsection {* Quotient types *} 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

146 

638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

147 
text {* 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

148 
The quotient type @{text "'a quot"} consists of all \emph{equivalence 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

149 
classes} over elements of the base type @{typ 'a}. 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

150 
*} 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

151 

638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

152 
typedef 'a quot = "{{x. a \<sim> x} a::'a. True}" 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

153 
by blast 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

154 

638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

155 
lemma quotI [intro]: "{x. a \<sim> x} \<in> quot" 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

156 
by (unfold quot_def) blast 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

157 

638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

158 
lemma quotE [elim]: "R \<in> quot ==> (!!a. R = {x. a \<sim> x} ==> C) ==> C" 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

159 
by (unfold quot_def) blast 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

160 

638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

161 
text {* 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

162 
\medskip Abstracted equivalence classes are the canonical 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

163 
representation of elements of a quotient type. 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

164 
*} 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

165 

638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

166 
constdefs 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

167 
eqv_class :: "('a::partial_equiv) => 'a quot" ("\<lfloor>_\<rfloor>") 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

168 
"\<lfloor>a\<rfloor> == Abs_quot {x. a \<sim> x}" 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

169 

638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

170 
theorem quot_rep: "\<exists>a. A = \<lfloor>a\<rfloor>" 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

171 
proof (cases A) 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

172 
fix R assume R: "A = Abs_quot R" 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

173 
assume "R \<in> quot" hence "\<exists>a. R = {x. a \<sim> x}" by blast 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

174 
with R have "\<exists>a. A = Abs_quot {x. a \<sim> x}" by blast 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

175 
thus ?thesis by (unfold eqv_class_def) 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

176 
qed 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

177 

638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

178 
lemma quot_cases [case_names rep, cases type: quot]: 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

179 
"(!!a. A = \<lfloor>a\<rfloor> ==> C) ==> C" 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

180 
by (insert quot_rep) blast 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

181 

638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

182 

638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

183 
subsection {* Equality on quotients *} 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

184 

638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

185 
text {* 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

186 
Equality of canonical quotient elements corresponds to the original 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

187 
relation as follows. 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

188 
*} 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

189 

638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

190 
theorem eqv_class_eqI [intro]: "a \<sim> b ==> \<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>" 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

191 
proof  
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

192 
assume ab: "a \<sim> b" 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

193 
have "{x. a \<sim> x} = {x. b \<sim> x}" 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

194 
proof (rule Collect_cong) 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

195 
fix x show "(a \<sim> x) = (b \<sim> x)" 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

196 
proof 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

197 
from ab have "b \<sim> a" .. 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

198 
also assume "a \<sim> x" 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

199 
finally show "b \<sim> x" . 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

200 
next 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

201 
note ab 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

202 
also assume "b \<sim> x" 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

203 
finally show "a \<sim> x" . 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

204 
qed 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

205 
qed 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

206 
thus ?thesis by (simp only: eqv_class_def) 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

207 
qed 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

208 

638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

209 
theorem eqv_class_eqD' [dest?]: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor> ==> a \<in> domain ==> a \<sim> b" 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

210 
proof (unfold eqv_class_def) 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

211 
assume "Abs_quot {x. a \<sim> x} = Abs_quot {x. b \<sim> x}" 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

212 
hence "{x. a \<sim> x} = {x. b \<sim> x}" by (simp only: Abs_quot_inject quotI) 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

213 
moreover assume "a \<in> domain" hence "a \<sim> a" .. 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

214 
ultimately have "a \<in> {x. b \<sim> x}" by blast 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

215 
hence "b \<sim> a" by blast 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

216 
thus "a \<sim> b" .. 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

217 
qed 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

218 

638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

219 
theorem eqv_class_eqD [dest?]: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor> ==> a \<sim> (b::'a::equiv)" 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

220 
proof (rule eqv_class_eqD') 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

221 
show "a \<in> domain" .. 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

222 
qed 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

223 

638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

224 
lemma eqv_class_eq' [simp]: "a \<in> domain ==> (\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> b)" 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

225 
by (insert eqv_class_eqI eqv_class_eqD') blast 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

226 

638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

227 
lemma eqv_class_eq [simp]: "(\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> (b::'a::equiv))" 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

228 
by (insert eqv_class_eqI eqv_class_eqD) blast 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

229 

638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

230 

638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

231 
subsection {* Picking representing elements *} 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

232 

638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

233 
constdefs 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

234 
pick :: "'a::partial_equiv quot => 'a" 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

235 
"pick A == SOME a. A = \<lfloor>a\<rfloor>" 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

236 

638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

237 
theorem pick_eqv' [intro?, simp]: "a \<in> domain ==> pick \<lfloor>a\<rfloor> \<sim> a" 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

238 
proof (unfold pick_def) 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

239 
assume a: "a \<in> domain" 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

240 
show "(SOME x. \<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>) \<sim> a" 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

241 
proof (rule someI2) 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

242 
show "\<lfloor>a\<rfloor> = \<lfloor>a\<rfloor>" .. 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

243 
fix x assume "\<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>" 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

244 
hence "a \<sim> x" .. 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

245 
thus "x \<sim> a" .. 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

246 
qed 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

247 
qed 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

248 

638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

249 
theorem pick_eqv [intro, simp]: "pick \<lfloor>a\<rfloor> \<sim> (a::'a::equiv)" 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

250 
proof (rule pick_eqv') 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

251 
show "a \<in> domain" .. 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

252 
qed 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

253 

638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

254 
theorem pick_inverse: "\<lfloor>pick A\<rfloor> = (A::'a::equiv quot)" 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

255 
proof (cases A) 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

256 
fix a assume a: "A = \<lfloor>a\<rfloor>" 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

257 
hence "pick A \<sim> a" by simp 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

258 
hence "\<lfloor>pick A\<rfloor> = \<lfloor>a\<rfloor>" by simp 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

259 
with a show ?thesis by simp 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

260 
qed 
638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

261 

638e1fc6ca74
Partial equivalence relations (leftover from HOL/Quot);
wenzelm
parents:
diff
changeset

262 
end 