author  webertj 
Fri, 19 Oct 2012 15:12:52 +0200  
changeset 49962  a8cc904a6820 
parent 48891  c0eafbd55de3 
child 51112  da97167e03f7 
permissions  rwrr 
41959  1 
(* Title: HOL/Quotient.thy 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

2 
Author: Cezary Kaliszyk and Christian Urban 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

3 
*) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

4 

35294  5 
header {* Definition of Quotient Types *} 
6 

35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

7 
theory Quotient 
47308  8 
imports Plain Hilbert_Choice Equiv_Relations Lifting 
46950
d0181abdbdac
declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents:
46947
diff
changeset

9 
keywords 
47308  10 
"print_quotmapsQ3" "print_quotientsQ3" "print_quotconsts" :: diag and 
46950
d0181abdbdac
declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents:
46947
diff
changeset

11 
"quotient_type" :: thy_goal and "/" and 
47091
d5cd13aca90b
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
kuncar
parents:
46950
diff
changeset

12 
"quotient_definition" :: thy_goal 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

13 
begin 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

14 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

15 
text {* 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

16 
Basic definition for equivalence relations 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

17 
that are represented by predicates. 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

18 
*} 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

19 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

20 
text {* Composition of Relations *} 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

21 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

22 
abbreviation 
40818
b117df72e56b
reorienting iff in Quotient_rel prevents simplifier looping;
haftmann
parents:
40814
diff
changeset

23 
rel_conj :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" (infixr "OOO" 75) 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

24 
where 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

25 
"r1 OOO r2 \<equiv> r1 OO r2 OO r1" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

26 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

27 
lemma eq_comp_r: 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

28 
shows "((op =) OOO R) = R" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

29 
by (auto simp add: fun_eq_iff) 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

30 

35294  31 
subsection {* Quotient Predicate *} 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

32 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

33 
definition 
47308  34 
"Quotient3 R Abs Rep \<longleftrightarrow> 
40814
fa64f6278568
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
40615
diff
changeset

35 
(\<forall>a. Abs (Rep a) = a) \<and> (\<forall>a. R (Rep a) (Rep a)) \<and> 
40818
b117df72e56b
reorienting iff in Quotient_rel prevents simplifier looping;
haftmann
parents:
40814
diff
changeset

36 
(\<forall>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s)" 
b117df72e56b
reorienting iff in Quotient_rel prevents simplifier looping;
haftmann
parents:
40814
diff
changeset

37 

47308  38 
lemma Quotient3I: 
40818
b117df72e56b
reorienting iff in Quotient_rel prevents simplifier looping;
haftmann
parents:
40814
diff
changeset

39 
assumes "\<And>a. Abs (Rep a) = a" 
b117df72e56b
reorienting iff in Quotient_rel prevents simplifier looping;
haftmann
parents:
40814
diff
changeset

40 
and "\<And>a. R (Rep a) (Rep a)" 
b117df72e56b
reorienting iff in Quotient_rel prevents simplifier looping;
haftmann
parents:
40814
diff
changeset

41 
and "\<And>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s" 
47308  42 
shows "Quotient3 R Abs Rep" 
43 
using assms unfolding Quotient3_def by blast 

35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

44 

47308  45 
lemma Quotient3_abs_rep: 
46 
assumes a: "Quotient3 R Abs Rep" 

35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

47 
shows "Abs (Rep a) = a" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

48 
using a 
47308  49 
unfolding Quotient3_def 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

50 
by simp 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

51 

47308  52 
lemma Quotient3_rep_reflp: 
53 
assumes a: "Quotient3 R Abs Rep" 

40814
fa64f6278568
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
40615
diff
changeset

54 
shows "R (Rep a) (Rep a)" 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

55 
using a 
47308  56 
unfolding Quotient3_def 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

57 
by blast 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

58 

47308  59 
lemma Quotient3_rel: 
60 
assumes a: "Quotient3 R Abs Rep" 

40818
b117df72e56b
reorienting iff in Quotient_rel prevents simplifier looping;
haftmann
parents:
40814
diff
changeset

61 
shows "R r r \<and> R s s \<and> Abs r = Abs s \<longleftrightarrow> R r s"  {* orientation does not loop on rewriting *} 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

62 
using a 
47308  63 
unfolding Quotient3_def 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

64 
by blast 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

65 

47308  66 
lemma Quotient3_refl1: 
67 
assumes a: "Quotient3 R Abs Rep" 

47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47094
diff
changeset

68 
shows "R r s \<Longrightarrow> R r r" 
47308  69 
using a unfolding Quotient3_def 
47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47094
diff
changeset

70 
by fast 
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47094
diff
changeset

71 

47308  72 
lemma Quotient3_refl2: 
73 
assumes a: "Quotient3 R Abs Rep" 

47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47094
diff
changeset

74 
shows "R r s \<Longrightarrow> R s s" 
47308  75 
using a unfolding Quotient3_def 
47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47094
diff
changeset

76 
by fast 
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47094
diff
changeset

77 

47308  78 
lemma Quotient3_rel_rep: 
79 
assumes a: "Quotient3 R Abs Rep" 

40818
b117df72e56b
reorienting iff in Quotient_rel prevents simplifier looping;
haftmann
parents:
40814
diff
changeset

80 
shows "R (Rep a) (Rep b) \<longleftrightarrow> a = b" 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

81 
using a 
47308  82 
unfolding Quotient3_def 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

83 
by metis 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

84 

47308  85 
lemma Quotient3_rep_abs: 
86 
assumes a: "Quotient3 R Abs Rep" 

35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

87 
shows "R r r \<Longrightarrow> R (Rep (Abs r)) r" 
47308  88 
using a unfolding Quotient3_def 
89 
by blast 

90 

91 
lemma Quotient3_rel_abs: 

92 
assumes a: "Quotient3 R Abs Rep" 

93 
shows "R r s \<Longrightarrow> Abs r = Abs s" 

94 
using a unfolding Quotient3_def 

35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

95 
by blast 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

96 

47308  97 
lemma Quotient3_symp: 
98 
assumes a: "Quotient3 R Abs Rep" 

40814
fa64f6278568
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
40615
diff
changeset

99 
shows "symp R" 
47308  100 
using a unfolding Quotient3_def using sympI by metis 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

101 

47308  102 
lemma Quotient3_transp: 
103 
assumes a: "Quotient3 R Abs Rep" 

40814
fa64f6278568
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
40615
diff
changeset

104 
shows "transp R" 
47308  105 
using a unfolding Quotient3_def using transpI by (metis (full_types)) 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

106 

47308  107 
lemma Quotient3_part_equivp: 
108 
assumes a: "Quotient3 R Abs Rep" 

109 
shows "part_equivp R" 

110 
by (metis Quotient3_rep_reflp Quotient3_symp Quotient3_transp a part_equivpI) 

111 

112 
lemma identity_quotient3: 

113 
shows "Quotient3 (op =) id id" 

114 
unfolding Quotient3_def id_def 

35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

115 
by blast 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

116 

47308  117 
lemma fun_quotient3: 
118 
assumes q1: "Quotient3 R1 abs1 rep1" 

119 
and q2: "Quotient3 R2 abs2 rep2" 

120 
shows "Quotient3 (R1 ===> R2) (rep1 > abs2) (abs1 > rep2)" 

35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

121 
proof  
47308  122 
have "\<And>a.(rep1 > abs2) ((abs1 > rep2) a) = a" 
123 
using q1 q2 by (simp add: Quotient3_def fun_eq_iff) 

35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

124 
moreover 
47308  125 
have "\<And>a.(R1 ===> R2) ((abs1 > rep2) a) ((abs1 > rep2) a)" 
40466
c6587375088e
type annotations in specifications; fun_rel_def is no simp rule by default; slightly changed fun_map_def; more on predicates on relation functions; proper HOL equations in definitions
haftmann
parents:
40031
diff
changeset

126 
by (rule fun_relI) 
47308  127 
(insert q1 q2 Quotient3_rel_abs [of R1 abs1 rep1] Quotient3_rel_rep [of R2 abs2 rep2], 
128 
simp (no_asm) add: Quotient3_def, simp) 

129 

35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

130 
moreover 
47308  131 
{ 
132 
fix r s 

133 
have "(R1 ===> R2) r s = ((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and> 

35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

134 
(rep1 > abs2) r = (rep1 > abs2) s)" 
47308  135 
proof  
136 

137 
have "(R1 ===> R2) r s \<Longrightarrow> (R1 ===> R2) r r" unfolding fun_rel_def 

138 
using Quotient3_part_equivp[OF q1] Quotient3_part_equivp[OF q2] 

139 
by (metis (full_types) part_equivp_def) 

140 
moreover have "(R1 ===> R2) r s \<Longrightarrow> (R1 ===> R2) s s" unfolding fun_rel_def 

141 
using Quotient3_part_equivp[OF q1] Quotient3_part_equivp[OF q2] 

142 
by (metis (full_types) part_equivp_def) 

143 
moreover have "(R1 ===> R2) r s \<Longrightarrow> (rep1 > abs2) r = (rep1 > abs2) s" 

144 
apply(auto simp add: fun_rel_def fun_eq_iff) using q1 q2 unfolding Quotient3_def by metis 

145 
moreover have "((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and> 

146 
(rep1 > abs2) r = (rep1 > abs2) s) \<Longrightarrow> (R1 ===> R2) r s" 

147 
apply(auto simp add: fun_rel_def fun_eq_iff) using q1 q2 unfolding Quotient3_def 

148 
by (metis map_fun_apply) 

149 

150 
ultimately show ?thesis by blast 

151 
qed 

152 
} 

153 
ultimately show ?thesis by (intro Quotient3I) (assumption+) 

35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

154 
qed 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

155 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

156 
lemma abs_o_rep: 
47308  157 
assumes a: "Quotient3 R Abs Rep" 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

158 
shows "Abs o Rep = id" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

159 
unfolding fun_eq_iff 
47308  160 
by (simp add: Quotient3_abs_rep[OF a]) 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

161 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

162 
lemma equals_rsp: 
47308  163 
assumes q: "Quotient3 R Abs Rep" 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

164 
and a: "R xa xb" "R ya yb" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

165 
shows "R xa ya = R xb yb" 
47308  166 
using a Quotient3_symp[OF q] Quotient3_transp[OF q] 
40814
fa64f6278568
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
40615
diff
changeset

167 
by (blast elim: sympE transpE) 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

168 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

169 
lemma lambda_prs: 
47308  170 
assumes q1: "Quotient3 R1 Abs1 Rep1" 
171 
and q2: "Quotient3 R2 Abs2 Rep2" 

35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

172 
shows "(Rep1 > Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) = (\<lambda>x. f x)" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

173 
unfolding fun_eq_iff 
47308  174 
using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2] 
40814
fa64f6278568
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
40615
diff
changeset

175 
by simp 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

176 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

177 
lemma lambda_prs1: 
47308  178 
assumes q1: "Quotient3 R1 Abs1 Rep1" 
179 
and q2: "Quotient3 R2 Abs2 Rep2" 

35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

180 
shows "(Rep1 > Abs2) (\<lambda>x. (Abs1 > Rep2) f x) = (\<lambda>x. f x)" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

181 
unfolding fun_eq_iff 
47308  182 
using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2] 
40814
fa64f6278568
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
40615
diff
changeset

183 
by simp 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

184 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

185 
lemma rep_abs_rsp: 
47308  186 
assumes q: "Quotient3 R Abs Rep" 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

187 
and a: "R x1 x2" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

188 
shows "R x1 (Rep (Abs x2))" 
47308  189 
using a Quotient3_rel[OF q] Quotient3_abs_rep[OF q] Quotient3_rep_reflp[OF q] 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

190 
by metis 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

191 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

192 
lemma rep_abs_rsp_left: 
47308  193 
assumes q: "Quotient3 R Abs Rep" 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

194 
and a: "R x1 x2" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

195 
shows "R (Rep (Abs x1)) x2" 
47308  196 
using a Quotient3_rel[OF q] Quotient3_abs_rep[OF q] Quotient3_rep_reflp[OF q] 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

197 
by metis 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

198 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

199 
text{* 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

200 
In the following theorem R1 can be instantiated with anything, 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

201 
but we know some of the types of the Rep and Abs functions; 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

202 
so by solving Quotient assumptions we can get a unique R1 that 
35236
fd8231b16203
quote the constant and theorem name with @{text}
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35222
diff
changeset

203 
will be provable; which is why we need to use @{text apply_rsp} and 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

204 
not the primed version *} 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

205 

47308  206 
lemma apply_rspQ3: 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

207 
fixes f g::"'a \<Rightarrow> 'c" 
47308  208 
assumes q: "Quotient3 R1 Abs1 Rep1" 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

209 
and a: "(R1 ===> R2) f g" "R1 x y" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

210 
shows "R2 (f x) (g y)" 
40466
c6587375088e
type annotations in specifications; fun_rel_def is no simp rule by default; slightly changed fun_map_def; more on predicates on relation functions; proper HOL equations in definitions
haftmann
parents:
40031
diff
changeset

211 
using a by (auto elim: fun_relE) 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

212 

47308  213 
lemma apply_rspQ3'': 
214 
assumes "Quotient3 R Abs Rep" 

47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47094
diff
changeset

215 
and "(R ===> S) f f" 
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47094
diff
changeset

216 
shows "S (f (Rep x)) (f (Rep x))" 
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47094
diff
changeset

217 
proof  
47308  218 
from assms(1) have "R (Rep x) (Rep x)" by (rule Quotient3_rep_reflp) 
47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47094
diff
changeset

219 
then show ?thesis using assms(2) by (auto intro: apply_rsp') 
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47094
diff
changeset

220 
qed 
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47094
diff
changeset

221 

35294  222 
subsection {* lemmas for regularisation of ball and bex *} 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

223 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

224 
lemma ball_reg_eqv: 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

225 
fixes P :: "'a \<Rightarrow> bool" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

226 
assumes a: "equivp R" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

227 
shows "Ball (Respects R) P = (All P)" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

228 
using a 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

229 
unfolding equivp_def 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

230 
by (auto simp add: in_respects) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

231 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

232 
lemma bex_reg_eqv: 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

233 
fixes P :: "'a \<Rightarrow> bool" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

234 
assumes a: "equivp R" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

235 
shows "Bex (Respects R) P = (Ex P)" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

236 
using a 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

237 
unfolding equivp_def 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

238 
by (auto simp add: in_respects) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

239 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

240 
lemma ball_reg_right: 
44553
4d39b032a021
avoid intermixing set and predicates; dropped lemmas mem_rsp and mem_prs (now in Quotient_Set.thy)
haftmann
parents:
44413
diff
changeset

241 
assumes a: "\<And>x. x \<in> R \<Longrightarrow> P x \<longrightarrow> Q x" 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

242 
shows "All P \<longrightarrow> Ball R Q" 
44921  243 
using a by fast 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

244 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

245 
lemma bex_reg_left: 
44553
4d39b032a021
avoid intermixing set and predicates; dropped lemmas mem_rsp and mem_prs (now in Quotient_Set.thy)
haftmann
parents:
44413
diff
changeset

246 
assumes a: "\<And>x. x \<in> R \<Longrightarrow> Q x \<longrightarrow> P x" 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

247 
shows "Bex R Q \<longrightarrow> Ex P" 
44921  248 
using a by fast 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

249 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

250 
lemma ball_reg_left: 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

251 
assumes a: "equivp R" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

252 
shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ball (Respects R) Q \<longrightarrow> All P" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

253 
using a by (metis equivp_reflp in_respects) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

254 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

255 
lemma bex_reg_right: 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

256 
assumes a: "equivp R" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

257 
shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ex Q \<longrightarrow> Bex (Respects R) P" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

258 
using a by (metis equivp_reflp in_respects) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

259 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

260 
lemma ball_reg_eqv_range: 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

261 
fixes P::"'a \<Rightarrow> bool" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

262 
and x::"'a" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

263 
assumes a: "equivp R2" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

264 
shows "(Ball (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = All (\<lambda>f. P (f x)))" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

265 
apply(rule iffI) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

266 
apply(rule allI) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

267 
apply(drule_tac x="\<lambda>y. f x" in bspec) 
40466
c6587375088e
type annotations in specifications; fun_rel_def is no simp rule by default; slightly changed fun_map_def; more on predicates on relation functions; proper HOL equations in definitions
haftmann
parents:
40031
diff
changeset

268 
apply(simp add: in_respects fun_rel_def) 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

269 
apply(rule impI) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

270 
using a equivp_reflp_symp_transp[of "R2"] 
40814
fa64f6278568
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
40615
diff
changeset

271 
apply (auto elim: equivpE reflpE) 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

272 
done 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

273 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

274 
lemma bex_reg_eqv_range: 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

275 
assumes a: "equivp R2" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

276 
shows "(Bex (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = Ex (\<lambda>f. P (f x)))" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

277 
apply(auto) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

278 
apply(rule_tac x="\<lambda>y. f x" in bexI) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

279 
apply(simp) 
40466
c6587375088e
type annotations in specifications; fun_rel_def is no simp rule by default; slightly changed fun_map_def; more on predicates on relation functions; proper HOL equations in definitions
haftmann
parents:
40031
diff
changeset

280 
apply(simp add: Respects_def in_respects fun_rel_def) 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

281 
apply(rule impI) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

282 
using a equivp_reflp_symp_transp[of "R2"] 
40814
fa64f6278568
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
40615
diff
changeset

283 
apply (auto elim: equivpE reflpE) 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

284 
done 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

285 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

286 
(* Next four lemmas are unused *) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

287 
lemma all_reg: 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

288 
assumes a: "!x :: 'a. (P x > Q x)" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

289 
and b: "All P" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

290 
shows "All Q" 
44921  291 
using a b by fast 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

292 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

293 
lemma ex_reg: 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

294 
assumes a: "!x :: 'a. (P x > Q x)" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

295 
and b: "Ex P" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

296 
shows "Ex Q" 
44921  297 
using a b by fast 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

298 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

299 
lemma ball_reg: 
44553
4d39b032a021
avoid intermixing set and predicates; dropped lemmas mem_rsp and mem_prs (now in Quotient_Set.thy)
haftmann
parents:
44413
diff
changeset

300 
assumes a: "!x :: 'a. (x \<in> R > P x > Q x)" 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

301 
and b: "Ball R P" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

302 
shows "Ball R Q" 
44921  303 
using a b by fast 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

304 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

305 
lemma bex_reg: 
44553
4d39b032a021
avoid intermixing set and predicates; dropped lemmas mem_rsp and mem_prs (now in Quotient_Set.thy)
haftmann
parents:
44413
diff
changeset

306 
assumes a: "!x :: 'a. (x \<in> R > P x > Q x)" 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

307 
and b: "Bex R P" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

308 
shows "Bex R Q" 
44921  309 
using a b by fast 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

310 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

311 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

312 
lemma ball_all_comm: 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

313 
assumes "\<And>y. (\<forall>x\<in>P. A x y) \<longrightarrow> (\<forall>x. B x y)" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

314 
shows "(\<forall>x\<in>P. \<forall>y. A x y) \<longrightarrow> (\<forall>x. \<forall>y. B x y)" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

315 
using assms by auto 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

316 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

317 
lemma bex_ex_comm: 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

318 
assumes "(\<exists>y. \<exists>x. A x y) \<longrightarrow> (\<exists>y. \<exists>x\<in>P. B x y)" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

319 
shows "(\<exists>x. \<exists>y. A x y) \<longrightarrow> (\<exists>x\<in>P. \<exists>y. B x y)" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

320 
using assms by auto 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

321 

35294  322 
subsection {* Bounded abstraction *} 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

323 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

324 
definition 
40466
c6587375088e
type annotations in specifications; fun_rel_def is no simp rule by default; slightly changed fun_map_def; more on predicates on relation functions; proper HOL equations in definitions
haftmann
parents:
40031
diff
changeset

325 
Babs :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

326 
where 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

327 
"x \<in> p \<Longrightarrow> Babs p m x = m x" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

328 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

329 
lemma babs_rsp: 
47308  330 
assumes q: "Quotient3 R1 Abs1 Rep1" 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

331 
and a: "(R1 ===> R2) f g" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

332 
shows "(R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)" 
40466
c6587375088e
type annotations in specifications; fun_rel_def is no simp rule by default; slightly changed fun_map_def; more on predicates on relation functions; proper HOL equations in definitions
haftmann
parents:
40031
diff
changeset

333 
apply (auto simp add: Babs_def in_respects fun_rel_def) 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

334 
apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1") 
40466
c6587375088e
type annotations in specifications; fun_rel_def is no simp rule by default; slightly changed fun_map_def; more on predicates on relation functions; proper HOL equations in definitions
haftmann
parents:
40031
diff
changeset

335 
using a apply (simp add: Babs_def fun_rel_def) 
c6587375088e
type annotations in specifications; fun_rel_def is no simp rule by default; slightly changed fun_map_def; more on predicates on relation functions; proper HOL equations in definitions
haftmann
parents:
40031
diff
changeset

336 
apply (simp add: in_respects fun_rel_def) 
47308  337 
using Quotient3_rel[OF q] 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

338 
by metis 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

339 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

340 
lemma babs_prs: 
47308  341 
assumes q1: "Quotient3 R1 Abs1 Rep1" 
342 
and q2: "Quotient3 R2 Abs2 Rep2" 

35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

343 
shows "((Rep1 > Abs2) (Babs (Respects R1) ((Abs1 > Rep2) f))) = f" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

344 
apply (rule ext) 
40466
c6587375088e
type annotations in specifications; fun_rel_def is no simp rule by default; slightly changed fun_map_def; more on predicates on relation functions; proper HOL equations in definitions
haftmann
parents:
40031
diff
changeset

345 
apply (simp add:) 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

346 
apply (subgoal_tac "Rep1 x \<in> Respects R1") 
47308  347 
apply (simp add: Babs_def Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2]) 
348 
apply (simp add: in_respects Quotient3_rel_rep[OF q1]) 

35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

349 
done 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

350 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

351 
lemma babs_simp: 
47308  352 
assumes q: "Quotient3 R1 Abs Rep" 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

353 
shows "((R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)) = ((R1 ===> R2) f g)" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

354 
apply(rule iffI) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

355 
apply(simp_all only: babs_rsp[OF q]) 
40466
c6587375088e
type annotations in specifications; fun_rel_def is no simp rule by default; slightly changed fun_map_def; more on predicates on relation functions; proper HOL equations in definitions
haftmann
parents:
40031
diff
changeset

356 
apply(auto simp add: Babs_def fun_rel_def) 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

357 
apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1") 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

358 
apply(metis Babs_def) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

359 
apply (simp add: in_respects) 
47308  360 
using Quotient3_rel[OF q] 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

361 
by metis 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

362 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

363 
(* If a user proves that a particular functional relation 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

364 
is an equivalence this may be useful in regularising *) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

365 
lemma babs_reg_eqv: 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

366 
shows "equivp R \<Longrightarrow> Babs (Respects R) P = P" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

367 
by (simp add: fun_eq_iff Babs_def in_respects equivp_reflp) 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

368 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

369 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

370 
(* 3 lemmas needed for proving repabs_inj *) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

371 
lemma ball_rsp: 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

372 
assumes a: "(R ===> (op =)) f g" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

373 
shows "Ball (Respects R) f = Ball (Respects R) g" 
40466
c6587375088e
type annotations in specifications; fun_rel_def is no simp rule by default; slightly changed fun_map_def; more on predicates on relation functions; proper HOL equations in definitions
haftmann
parents:
40031
diff
changeset

374 
using a by (auto simp add: Ball_def in_respects elim: fun_relE) 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

375 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

376 
lemma bex_rsp: 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

377 
assumes a: "(R ===> (op =)) f g" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

378 
shows "(Bex (Respects R) f = Bex (Respects R) g)" 
40466
c6587375088e
type annotations in specifications; fun_rel_def is no simp rule by default; slightly changed fun_map_def; more on predicates on relation functions; proper HOL equations in definitions
haftmann
parents:
40031
diff
changeset

379 
using a by (auto simp add: Bex_def in_respects elim: fun_relE) 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

380 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

381 
lemma bex1_rsp: 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

382 
assumes a: "(R ===> (op =)) f g" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

383 
shows "Ex1 (\<lambda>x. x \<in> Respects R \<and> f x) = Ex1 (\<lambda>x. x \<in> Respects R \<and> g x)" 
40466
c6587375088e
type annotations in specifications; fun_rel_def is no simp rule by default; slightly changed fun_map_def; more on predicates on relation functions; proper HOL equations in definitions
haftmann
parents:
40031
diff
changeset

384 
using a by (auto elim: fun_relE simp add: Ex1_def in_respects) 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

385 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

386 
(* 2 lemmas needed for cleaning of quantifiers *) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

387 
lemma all_prs: 
47308  388 
assumes a: "Quotient3 R absf repf" 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

389 
shows "Ball (Respects R) ((absf > id) f) = All f" 
47308  390 
using a unfolding Quotient3_def Ball_def in_respects id_apply comp_def map_fun_def 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

391 
by metis 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

392 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

393 
lemma ex_prs: 
47308  394 
assumes a: "Quotient3 R absf repf" 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

395 
shows "Bex (Respects R) ((absf > id) f) = Ex f" 
47308  396 
using a unfolding Quotient3_def Bex_def in_respects id_apply comp_def map_fun_def 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

397 
by metis 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

398 

35294  399 
subsection {* @{text Bex1_rel} quantifier *} 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

400 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

401 
definition 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

402 
Bex1_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

403 
where 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

404 
"Bex1_rel R P \<longleftrightarrow> (\<exists>x \<in> Respects R. P x) \<and> (\<forall>x \<in> Respects R. \<forall>y \<in> Respects R. ((P x \<and> P y) \<longrightarrow> (R x y)))" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

405 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

406 
lemma bex1_rel_aux: 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

407 
"\<lbrakk>\<forall>xa ya. R xa ya \<longrightarrow> x xa = y ya; Bex1_rel R x\<rbrakk> \<Longrightarrow> Bex1_rel R y" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

408 
unfolding Bex1_rel_def 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

409 
apply (erule conjE)+ 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

410 
apply (erule bexE) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

411 
apply rule 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

412 
apply (rule_tac x="xa" in bexI) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

413 
apply metis 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

414 
apply metis 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

415 
apply rule+ 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

416 
apply (erule_tac x="xaa" in ballE) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

417 
prefer 2 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

418 
apply (metis) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

419 
apply (erule_tac x="ya" in ballE) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

420 
prefer 2 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

421 
apply (metis) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

422 
apply (metis in_respects) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

423 
done 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

424 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

425 
lemma bex1_rel_aux2: 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

426 
"\<lbrakk>\<forall>xa ya. R xa ya \<longrightarrow> x xa = y ya; Bex1_rel R y\<rbrakk> \<Longrightarrow> Bex1_rel R x" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

427 
unfolding Bex1_rel_def 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

428 
apply (erule conjE)+ 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

429 
apply (erule bexE) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

430 
apply rule 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

431 
apply (rule_tac x="xa" in bexI) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

432 
apply metis 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

433 
apply metis 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

434 
apply rule+ 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

435 
apply (erule_tac x="xaa" in ballE) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

436 
prefer 2 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

437 
apply (metis) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

438 
apply (erule_tac x="ya" in ballE) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

439 
prefer 2 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

440 
apply (metis) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

441 
apply (metis in_respects) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

442 
done 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

443 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

444 
lemma bex1_rel_rsp: 
47308  445 
assumes a: "Quotient3 R absf repf" 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

446 
shows "((R ===> op =) ===> op =) (Bex1_rel R) (Bex1_rel R)" 
40466
c6587375088e
type annotations in specifications; fun_rel_def is no simp rule by default; slightly changed fun_map_def; more on predicates on relation functions; proper HOL equations in definitions
haftmann
parents:
40031
diff
changeset

447 
apply (simp add: fun_rel_def) 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

448 
apply clarify 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

449 
apply rule 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

450 
apply (simp_all add: bex1_rel_aux bex1_rel_aux2) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

451 
apply (erule bex1_rel_aux2) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

452 
apply assumption 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

453 
done 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

454 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

455 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

456 
lemma ex1_prs: 
47308  457 
assumes a: "Quotient3 R absf repf" 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

458 
shows "((absf > id) > id) (Bex1_rel R) f = Ex1 f" 
40466
c6587375088e
type annotations in specifications; fun_rel_def is no simp rule by default; slightly changed fun_map_def; more on predicates on relation functions; proper HOL equations in definitions
haftmann
parents:
40031
diff
changeset

459 
apply (simp add:) 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

460 
apply (subst Bex1_rel_def) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

461 
apply (subst Bex_def) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

462 
apply (subst Ex1_def) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

463 
apply simp 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

464 
apply rule 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

465 
apply (erule conjE)+ 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

466 
apply (erule_tac exE) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

467 
apply (erule conjE) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

468 
apply (subgoal_tac "\<forall>y. R y y \<longrightarrow> f (absf y) \<longrightarrow> R x y") 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

469 
apply (rule_tac x="absf x" in exI) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

470 
apply (simp) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

471 
apply rule+ 
47308  472 
using a unfolding Quotient3_def 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

473 
apply metis 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

474 
apply rule+ 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

475 
apply (erule_tac x="x" in ballE) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

476 
apply (erule_tac x="y" in ballE) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

477 
apply simp 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

478 
apply (simp add: in_respects) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

479 
apply (simp add: in_respects) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

480 
apply (erule_tac exE) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

481 
apply rule 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

482 
apply (rule_tac x="repf x" in exI) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

483 
apply (simp only: in_respects) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

484 
apply rule 
47308  485 
apply (metis Quotient3_rel_rep[OF a]) 
486 
using a unfolding Quotient3_def apply (simp) 

35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

487 
apply rule+ 
47308  488 
using a unfolding Quotient3_def in_respects 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

489 
apply metis 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

490 
done 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

491 

38702
72fd257f4343
Quotient Package / lemma for regularization of bex1_rel for equivalence relations
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
38317
diff
changeset

492 
lemma bex1_bexeq_reg: 
72fd257f4343
Quotient Package / lemma for regularization of bex1_rel for equivalence relations
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
38317
diff
changeset

493 
shows "(\<exists>!x\<in>Respects R. P x) \<longrightarrow> (Bex1_rel R (\<lambda>x. P x))" 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

494 
apply (simp add: Ex1_def Bex1_rel_def in_respects) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

495 
apply clarify 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

496 
apply auto 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

497 
apply (rule bexI) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

498 
apply assumption 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

499 
apply (simp add: in_respects) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

500 
apply (simp add: in_respects) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

501 
apply auto 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

502 
done 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

503 

38702
72fd257f4343
Quotient Package / lemma for regularization of bex1_rel for equivalence relations
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
38317
diff
changeset

504 
lemma bex1_bexeq_reg_eqv: 
72fd257f4343
Quotient Package / lemma for regularization of bex1_rel for equivalence relations
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
38317
diff
changeset

505 
assumes a: "equivp R" 
72fd257f4343
Quotient Package / lemma for regularization of bex1_rel for equivalence relations
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
38317
diff
changeset

506 
shows "(\<exists>!x. P x) \<longrightarrow> Bex1_rel R P" 
72fd257f4343
Quotient Package / lemma for regularization of bex1_rel for equivalence relations
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
38317
diff
changeset

507 
using equivp_reflp[OF a] 
72fd257f4343
Quotient Package / lemma for regularization of bex1_rel for equivalence relations
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
38317
diff
changeset

508 
apply (intro impI) 
72fd257f4343
Quotient Package / lemma for regularization of bex1_rel for equivalence relations
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
38317
diff
changeset

509 
apply (elim ex1E) 
72fd257f4343
Quotient Package / lemma for regularization of bex1_rel for equivalence relations
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
38317
diff
changeset

510 
apply (rule mp[OF bex1_bexeq_reg]) 
72fd257f4343
Quotient Package / lemma for regularization of bex1_rel for equivalence relations
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
38317
diff
changeset

511 
apply (rule_tac a="x" in ex1I) 
72fd257f4343
Quotient Package / lemma for regularization of bex1_rel for equivalence relations
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
38317
diff
changeset

512 
apply (subst in_respects) 
72fd257f4343
Quotient Package / lemma for regularization of bex1_rel for equivalence relations
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
38317
diff
changeset

513 
apply (rule conjI) 
72fd257f4343
Quotient Package / lemma for regularization of bex1_rel for equivalence relations
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
38317
diff
changeset

514 
apply assumption 
72fd257f4343
Quotient Package / lemma for regularization of bex1_rel for equivalence relations
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
38317
diff
changeset

515 
apply assumption 
72fd257f4343
Quotient Package / lemma for regularization of bex1_rel for equivalence relations
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
38317
diff
changeset

516 
apply clarify 
72fd257f4343
Quotient Package / lemma for regularization of bex1_rel for equivalence relations
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
38317
diff
changeset

517 
apply (erule_tac x="xa" in allE) 
72fd257f4343
Quotient Package / lemma for regularization of bex1_rel for equivalence relations
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
38317
diff
changeset

518 
apply simp 
72fd257f4343
Quotient Package / lemma for regularization of bex1_rel for equivalence relations
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
38317
diff
changeset

519 
done 
72fd257f4343
Quotient Package / lemma for regularization of bex1_rel for equivalence relations
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
38317
diff
changeset

520 

35294  521 
subsection {* Various respects and preserve lemmas *} 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

522 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

523 
lemma quot_rel_rsp: 
47308  524 
assumes a: "Quotient3 R Abs Rep" 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

525 
shows "(R ===> R ===> op =) R R" 
38317
cb8e2ac6397b
deleted duplicate lemma
Christian Urban <urbanc@in.tum.de>
parents:
37986
diff
changeset

526 
apply(rule fun_relI)+ 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

527 
apply(rule equals_rsp[OF a]) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

528 
apply(assumption)+ 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

529 
done 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

530 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

531 
lemma o_prs: 
47308  532 
assumes q1: "Quotient3 R1 Abs1 Rep1" 
533 
and q2: "Quotient3 R2 Abs2 Rep2" 

534 
and q3: "Quotient3 R3 Abs3 Rep3" 

36215
88ff48884d26
respectfullness and preservation of function composition
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36123
diff
changeset

535 
shows "((Abs2 > Rep3) > (Abs1 > Rep2) > (Rep1 > Abs3)) op \<circ> = op \<circ>" 
88ff48884d26
respectfullness and preservation of function composition
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36123
diff
changeset

536 
and "(id > (Abs1 > id) > Rep1 > id) op \<circ> = op \<circ>" 
47308  537 
using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2] Quotient3_abs_rep[OF q3] 
40466
c6587375088e
type annotations in specifications; fun_rel_def is no simp rule by default; slightly changed fun_map_def; more on predicates on relation functions; proper HOL equations in definitions
haftmann
parents:
40031
diff
changeset

538 
by (simp_all add: fun_eq_iff) 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

539 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

540 
lemma o_rsp: 
36215
88ff48884d26
respectfullness and preservation of function composition
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36123
diff
changeset

541 
"((R2 ===> R3) ===> (R1 ===> R2) ===> (R1 ===> R3)) op \<circ> op \<circ>" 
88ff48884d26
respectfullness and preservation of function composition
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36123
diff
changeset

542 
"(op = ===> (R1 ===> op =) ===> R1 ===> op =) op \<circ> op \<circ>" 
44921  543 
by (force elim: fun_relE)+ 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

544 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

545 
lemma cond_prs: 
47308  546 
assumes a: "Quotient3 R absf repf" 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

547 
shows "absf (if a then repf b else repf c) = (if a then b else c)" 
47308  548 
using a unfolding Quotient3_def by auto 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

549 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

550 
lemma if_prs: 
47308  551 
assumes q: "Quotient3 R Abs Rep" 
36123
7f877bbad5b2
add If respectfullness and preservation to Quotient package database
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36116
diff
changeset

552 
shows "(id > Rep > Rep > Abs) If = If" 
47308  553 
using Quotient3_abs_rep[OF q] 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

554 
by (auto simp add: fun_eq_iff) 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

555 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

556 
lemma if_rsp: 
47308  557 
assumes q: "Quotient3 R Abs Rep" 
36123
7f877bbad5b2
add If respectfullness and preservation to Quotient package database
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36116
diff
changeset

558 
shows "(op = ===> R ===> R ===> R) If If" 
44921  559 
by force 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

560 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

561 
lemma let_prs: 
47308  562 
assumes q1: "Quotient3 R1 Abs1 Rep1" 
563 
and q2: "Quotient3 R2 Abs2 Rep2" 

37049
ca1c293e521e
Let rsp and prs in fun_rel/fun_map format
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36276
diff
changeset

564 
shows "(Rep2 > (Abs2 > Rep1) > Abs1) Let = Let" 
47308  565 
using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2] 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

566 
by (auto simp add: fun_eq_iff) 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

567 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

568 
lemma let_rsp: 
37049
ca1c293e521e
Let rsp and prs in fun_rel/fun_map format
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36276
diff
changeset

569 
shows "(R1 ===> (R1 ===> R2) ===> R2) Let Let" 
44921  570 
by (force elim: fun_relE) 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

571 

39669
9e3b035841e4
quotient package: respectfulness and preservation of identity.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39302
diff
changeset

572 
lemma id_rsp: 
9e3b035841e4
quotient package: respectfulness and preservation of identity.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39302
diff
changeset

573 
shows "(R ===> R) id id" 
44921  574 
by auto 
39669
9e3b035841e4
quotient package: respectfulness and preservation of identity.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39302
diff
changeset

575 

9e3b035841e4
quotient package: respectfulness and preservation of identity.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39302
diff
changeset

576 
lemma id_prs: 
47308  577 
assumes a: "Quotient3 R Abs Rep" 
39669
9e3b035841e4
quotient package: respectfulness and preservation of identity.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39302
diff
changeset

578 
shows "(Rep > Abs) id = id" 
47308  579 
by (simp add: fun_eq_iff Quotient3_abs_rep [OF a]) 
39669
9e3b035841e4
quotient package: respectfulness and preservation of identity.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39302
diff
changeset

580 

9e3b035841e4
quotient package: respectfulness and preservation of identity.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
39302
diff
changeset

581 

35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

582 
locale quot_type = 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

583 
fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 
44204
3cdc4176638c
Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
42814
diff
changeset

584 
and Abs :: "'a set \<Rightarrow> 'b" 
3cdc4176638c
Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
42814
diff
changeset

585 
and Rep :: "'b \<Rightarrow> 'a set" 
37493
2377d246a631
Quotient package now uses Partial Equivalence instead place of equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37049
diff
changeset

586 
assumes equivp: "part_equivp R" 
44204
3cdc4176638c
Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
42814
diff
changeset

587 
and rep_prop: "\<And>y. \<exists>x. R x x \<and> Rep y = Collect (R x)" 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

588 
and rep_inverse: "\<And>x. Abs (Rep x) = x" 
44204
3cdc4176638c
Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
42814
diff
changeset

589 
and abs_inverse: "\<And>c. (\<exists>x. ((R x x) \<and> (c = Collect (R x)))) \<Longrightarrow> (Rep (Abs c)) = c" 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

590 
and rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

591 
begin 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

592 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

593 
definition 
40466
c6587375088e
type annotations in specifications; fun_rel_def is no simp rule by default; slightly changed fun_map_def; more on predicates on relation functions; proper HOL equations in definitions
haftmann
parents:
40031
diff
changeset

594 
abs :: "'a \<Rightarrow> 'b" 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

595 
where 
44204
3cdc4176638c
Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
42814
diff
changeset

596 
"abs x = Abs (Collect (R x))" 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

597 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

598 
definition 
40466
c6587375088e
type annotations in specifications; fun_rel_def is no simp rule by default; slightly changed fun_map_def; more on predicates on relation functions; proper HOL equations in definitions
haftmann
parents:
40031
diff
changeset

599 
rep :: "'b \<Rightarrow> 'a" 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

600 
where 
44204
3cdc4176638c
Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
42814
diff
changeset

601 
"rep a = (SOME x. x \<in> Rep a)" 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

602 

44204
3cdc4176638c
Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
42814
diff
changeset

603 
lemma some_collect: 
37493
2377d246a631
Quotient package now uses Partial Equivalence instead place of equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37049
diff
changeset

604 
assumes "R r r" 
44204
3cdc4176638c
Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
42814
diff
changeset

605 
shows "R (SOME x. x \<in> Collect (R r)) = R r" 
3cdc4176638c
Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
42814
diff
changeset

606 
apply simp 
3cdc4176638c
Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
42814
diff
changeset

607 
by (metis assms exE_some equivp[simplified part_equivp_def]) 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

608 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

609 
lemma Quotient: 
47308  610 
shows "Quotient3 R abs rep" 
611 
unfolding Quotient3_def abs_def rep_def 

37493
2377d246a631
Quotient package now uses Partial Equivalence instead place of equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37049
diff
changeset

612 
proof (intro conjI allI) 
2377d246a631
Quotient package now uses Partial Equivalence instead place of equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37049
diff
changeset

613 
fix a r s 
44204
3cdc4176638c
Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
42814
diff
changeset

614 
show x: "R (SOME x. x \<in> Rep a) (SOME x. x \<in> Rep a)" proof  
3cdc4176638c
Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
42814
diff
changeset

615 
obtain x where r: "R x x" and rep: "Rep a = Collect (R x)" using rep_prop[of a] by auto 
3cdc4176638c
Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
42814
diff
changeset

616 
have "R (SOME x. x \<in> Rep a) x" using r rep some_collect by metis 
3cdc4176638c
Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
42814
diff
changeset

617 
then have "R x (SOME x. x \<in> Rep a)" using part_equivp_symp[OF equivp] by fast 
3cdc4176638c
Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
42814
diff
changeset

618 
then show "R (SOME x. x \<in> Rep a) (SOME x. x \<in> Rep a)" 
3cdc4176638c
Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
42814
diff
changeset

619 
using part_equivp_transp[OF equivp] by (metis `R (SOME x. x \<in> Rep a) x`) 
37493
2377d246a631
Quotient package now uses Partial Equivalence instead place of equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37049
diff
changeset

620 
qed 
44204
3cdc4176638c
Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
42814
diff
changeset

621 
have "Collect (R (SOME x. x \<in> Rep a)) = (Rep a)" by (metis some_collect rep_prop) 
3cdc4176638c
Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
42814
diff
changeset

622 
then show "Abs (Collect (R (SOME x. x \<in> Rep a))) = a" using rep_inverse by auto 
3cdc4176638c
Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
42814
diff
changeset

623 
have "R r r \<Longrightarrow> R s s \<Longrightarrow> Abs (Collect (R r)) = Abs (Collect (R s)) \<longleftrightarrow> R r = R s" 
44242  624 
proof  
625 
assume "R r r" and "R s s" 

626 
then have "Abs (Collect (R r)) = Abs (Collect (R s)) \<longleftrightarrow> Collect (R r) = Collect (R s)" 

627 
by (metis abs_inverse) 

628 
also have "Collect (R r) = Collect (R s) \<longleftrightarrow> (\<lambda>A x. x \<in> A) (Collect (R r)) = (\<lambda>A x. x \<in> A) (Collect (R s))" 

629 
by rule simp_all 

630 
finally show "Abs (Collect (R r)) = Abs (Collect (R s)) \<longleftrightarrow> R r = R s" by simp 

631 
qed 

44204
3cdc4176638c
Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
42814
diff
changeset

632 
then show "R r s \<longleftrightarrow> R r r \<and> R s s \<and> (Abs (Collect (R r)) = Abs (Collect (R s)))" 
3cdc4176638c
Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
42814
diff
changeset

633 
using equivp[simplified part_equivp_def] by metis 
3cdc4176638c
Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
42814
diff
changeset

634 
qed 
44242  635 

35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

636 
end 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

637 

47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47094
diff
changeset

638 
subsection {* Quotient composition *} 
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47094
diff
changeset

639 

47308  640 
lemma OOO_quotient3: 
47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47094
diff
changeset

641 
fixes R1 :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47094
diff
changeset

642 
fixes Abs1 :: "'a \<Rightarrow> 'b" and Rep1 :: "'b \<Rightarrow> 'a" 
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47094
diff
changeset

643 
fixes Abs2 :: "'b \<Rightarrow> 'c" and Rep2 :: "'c \<Rightarrow> 'b" 
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47094
diff
changeset

644 
fixes R2' :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47094
diff
changeset

645 
fixes R2 :: "'b \<Rightarrow> 'b \<Rightarrow> bool" 
47308  646 
assumes R1: "Quotient3 R1 Abs1 Rep1" 
647 
assumes R2: "Quotient3 R2 Abs2 Rep2" 

47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47094
diff
changeset

648 
assumes Abs1: "\<And>x y. R2' x y \<Longrightarrow> R1 x x \<Longrightarrow> R1 y y \<Longrightarrow> R2 (Abs1 x) (Abs1 y)" 
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47094
diff
changeset

649 
assumes Rep1: "\<And>x y. R2 x y \<Longrightarrow> R2' (Rep1 x) (Rep1 y)" 
47308  650 
shows "Quotient3 (R1 OO R2' OO R1) (Abs2 \<circ> Abs1) (Rep1 \<circ> Rep2)" 
651 
apply (rule Quotient3I) 

652 
apply (simp add: o_def Quotient3_abs_rep [OF R2] Quotient3_abs_rep [OF R1]) 

47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47094
diff
changeset

653 
apply simp 
47434
b75ce48a93ee
dropped abbreviation "pred_comp"; introduced infix notation "P OO Q" for "relcompp P Q"
griff
parents:
47105
diff
changeset

654 
apply (rule_tac b="Rep1 (Rep2 a)" in relcomppI) 
47308  655 
apply (rule Quotient3_rep_reflp [OF R1]) 
47434
b75ce48a93ee
dropped abbreviation "pred_comp"; introduced infix notation "P OO Q" for "relcompp P Q"
griff
parents:
47105
diff
changeset

656 
apply (rule_tac b="Rep1 (Rep2 a)" in relcomppI [rotated]) 
47308  657 
apply (rule Quotient3_rep_reflp [OF R1]) 
47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47094
diff
changeset

658 
apply (rule Rep1) 
47308  659 
apply (rule Quotient3_rep_reflp [OF R2]) 
47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47094
diff
changeset

660 
apply safe 
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47094
diff
changeset

661 
apply (rename_tac x y) 
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47094
diff
changeset

662 
apply (drule Abs1) 
47308  663 
apply (erule Quotient3_refl2 [OF R1]) 
664 
apply (erule Quotient3_refl1 [OF R1]) 

665 
apply (drule Quotient3_refl1 [OF R2], drule Rep1) 

47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47094
diff
changeset

666 
apply (subgoal_tac "R1 r (Rep1 (Abs1 x))") 
47434
b75ce48a93ee
dropped abbreviation "pred_comp"; introduced infix notation "P OO Q" for "relcompp P Q"
griff
parents:
47105
diff
changeset

667 
apply (rule_tac b="Rep1 (Abs1 x)" in relcomppI, assumption) 
b75ce48a93ee
dropped abbreviation "pred_comp"; introduced infix notation "P OO Q" for "relcompp P Q"
griff
parents:
47105
diff
changeset

668 
apply (erule relcomppI) 
47308  669 
apply (erule Quotient3_symp [OF R1, THEN sympD]) 
670 
apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2]) 

671 
apply (rule conjI, erule Quotient3_refl1 [OF R1]) 

672 
apply (rule conjI, rule Quotient3_rep_reflp [OF R1]) 

673 
apply (subst Quotient3_abs_rep [OF R1]) 

674 
apply (erule Quotient3_rel_abs [OF R1]) 

47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47094
diff
changeset

675 
apply (rename_tac x y) 
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47094
diff
changeset

676 
apply (drule Abs1) 
47308  677 
apply (erule Quotient3_refl2 [OF R1]) 
678 
apply (erule Quotient3_refl1 [OF R1]) 

679 
apply (drule Quotient3_refl2 [OF R2], drule Rep1) 

47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47094
diff
changeset

680 
apply (subgoal_tac "R1 s (Rep1 (Abs1 y))") 
47434
b75ce48a93ee
dropped abbreviation "pred_comp"; introduced infix notation "P OO Q" for "relcompp P Q"
griff
parents:
47105
diff
changeset

681 
apply (rule_tac b="Rep1 (Abs1 y)" in relcomppI, assumption) 
b75ce48a93ee
dropped abbreviation "pred_comp"; introduced infix notation "P OO Q" for "relcompp P Q"
griff
parents:
47105
diff
changeset

682 
apply (erule relcomppI) 
47308  683 
apply (erule Quotient3_symp [OF R1, THEN sympD]) 
684 
apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2]) 

685 
apply (rule conjI, erule Quotient3_refl2 [OF R1]) 

686 
apply (rule conjI, rule Quotient3_rep_reflp [OF R1]) 

687 
apply (subst Quotient3_abs_rep [OF R1]) 

688 
apply (erule Quotient3_rel_abs [OF R1, THEN sym]) 

47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47094
diff
changeset

689 
apply simp 
47308  690 
apply (rule Quotient3_rel_abs [OF R2]) 
691 
apply (rule Quotient3_rel_abs [OF R1, THEN ssubst], assumption) 

692 
apply (rule Quotient3_rel_abs [OF R1, THEN subst], assumption) 

47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47094
diff
changeset

693 
apply (erule Abs1) 
47308  694 
apply (erule Quotient3_refl2 [OF R1]) 
695 
apply (erule Quotient3_refl1 [OF R1]) 

47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47094
diff
changeset

696 
apply (rename_tac a b c d) 
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47094
diff
changeset

697 
apply simp 
47434
b75ce48a93ee
dropped abbreviation "pred_comp"; introduced infix notation "P OO Q" for "relcompp P Q"
griff
parents:
47105
diff
changeset

698 
apply (rule_tac b="Rep1 (Abs1 r)" in relcomppI) 
47308  699 
apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2]) 
700 
apply (rule conjI, erule Quotient3_refl1 [OF R1]) 

701 
apply (simp add: Quotient3_abs_rep [OF R1] Quotient3_rep_reflp [OF R1]) 

47434
b75ce48a93ee
dropped abbreviation "pred_comp"; introduced infix notation "P OO Q" for "relcompp P Q"
griff
parents:
47105
diff
changeset

702 
apply (rule_tac b="Rep1 (Abs1 s)" in relcomppI [rotated]) 
47308  703 
apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2]) 
704 
apply (simp add: Quotient3_abs_rep [OF R1] Quotient3_rep_reflp [OF R1]) 

705 
apply (erule Quotient3_refl2 [OF R1]) 

47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47094
diff
changeset

706 
apply (rule Rep1) 
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47094
diff
changeset

707 
apply (drule Abs1) 
47308  708 
apply (erule Quotient3_refl2 [OF R1]) 
709 
apply (erule Quotient3_refl1 [OF R1]) 

47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47094
diff
changeset

710 
apply (drule Abs1) 
47308  711 
apply (erule Quotient3_refl2 [OF R1]) 
712 
apply (erule Quotient3_refl1 [OF R1]) 

713 
apply (drule Quotient3_rel_abs [OF R1]) 

714 
apply (drule Quotient3_rel_abs [OF R1]) 

715 
apply (drule Quotient3_rel_abs [OF R1]) 

716 
apply (drule Quotient3_rel_abs [OF R1]) 

47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47094
diff
changeset

717 
apply simp 
47308  718 
apply (rule Quotient3_rel[symmetric, OF R2, THEN iffD2]) 
47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47094
diff
changeset

719 
apply simp 
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47094
diff
changeset

720 
done 
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47094
diff
changeset

721 

47308  722 
lemma OOO_eq_quotient3: 
47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47094
diff
changeset

723 
fixes R1 :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47094
diff
changeset

724 
fixes Abs1 :: "'a \<Rightarrow> 'b" and Rep1 :: "'b \<Rightarrow> 'a" 
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47094
diff
changeset

725 
fixes Abs2 :: "'b \<Rightarrow> 'c" and Rep2 :: "'c \<Rightarrow> 'b" 
47308  726 
assumes R1: "Quotient3 R1 Abs1 Rep1" 
727 
assumes R2: "Quotient3 op= Abs2 Rep2" 

728 
shows "Quotient3 (R1 OOO op=) (Abs2 \<circ> Abs1) (Rep1 \<circ> Rep2)" 

47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47094
diff
changeset

729 
using assms 
47308  730 
by (rule OOO_quotient3) auto 
47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47094
diff
changeset

731 

47362
b1f099bdfbba
connect the Quotient package to the Lifting package
kuncar
parents:
47361
diff
changeset

732 
subsection {* Quotient3 to Quotient *} 
b1f099bdfbba
connect the Quotient package to the Lifting package
kuncar
parents:
47361
diff
changeset

733 

b1f099bdfbba
connect the Quotient package to the Lifting package
kuncar
parents:
47361
diff
changeset

734 
lemma Quotient3_to_Quotient: 
b1f099bdfbba
connect the Quotient package to the Lifting package
kuncar
parents:
47361
diff
changeset

735 
assumes "Quotient3 R Abs Rep" 
b1f099bdfbba
connect the Quotient package to the Lifting package
kuncar
parents:
47361
diff
changeset

736 
and "T \<equiv> \<lambda>x y. R x x \<and> Abs x = y" 
b1f099bdfbba
connect the Quotient package to the Lifting package
kuncar
parents:
47361
diff
changeset

737 
shows "Quotient R Abs Rep T" 
b1f099bdfbba
connect the Quotient package to the Lifting package
kuncar
parents:
47361
diff
changeset

738 
using assms unfolding Quotient3_def by (intro QuotientI) blast+ 
47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47094
diff
changeset

739 

47362
b1f099bdfbba
connect the Quotient package to the Lifting package
kuncar
parents:
47361
diff
changeset

740 
lemma Quotient3_to_Quotient_equivp: 
b1f099bdfbba
connect the Quotient package to the Lifting package
kuncar
parents:
47361
diff
changeset

741 
assumes q: "Quotient3 R Abs Rep" 
b1f099bdfbba
connect the Quotient package to the Lifting package
kuncar
parents:
47361
diff
changeset

742 
and T_def: "T \<equiv> \<lambda>x y. Abs x = y" 
b1f099bdfbba
connect the Quotient package to the Lifting package
kuncar
parents:
47361
diff
changeset

743 
and eR: "equivp R" 
b1f099bdfbba
connect the Quotient package to the Lifting package
kuncar
parents:
47361
diff
changeset

744 
shows "Quotient R Abs Rep T" 
b1f099bdfbba
connect the Quotient package to the Lifting package
kuncar
parents:
47361
diff
changeset

745 
proof (intro QuotientI) 
b1f099bdfbba
connect the Quotient package to the Lifting package
kuncar
parents:
47361
diff
changeset

746 
fix a 
b1f099bdfbba
connect the Quotient package to the Lifting package
kuncar
parents:
47361
diff
changeset

747 
show "Abs (Rep a) = a" using q by(rule Quotient3_abs_rep) 
b1f099bdfbba
connect the Quotient package to the Lifting package
kuncar
parents:
47361
diff
changeset

748 
next 
b1f099bdfbba
connect the Quotient package to the Lifting package
kuncar
parents:
47361
diff
changeset

749 
fix a 
b1f099bdfbba
connect the Quotient package to the Lifting package
kuncar
parents:
47361
diff
changeset

750 
show "R (Rep a) (Rep a)" using q by(rule Quotient3_rep_reflp) 
b1f099bdfbba
connect the Quotient package to the Lifting package
kuncar
parents:
47361
diff
changeset

751 
next 
b1f099bdfbba
connect the Quotient package to the Lifting package
kuncar
parents:
47361
diff
changeset

752 
fix r s 
b1f099bdfbba
connect the Quotient package to the Lifting package
kuncar
parents:
47361
diff
changeset

753 
show "R r s = (R r r \<and> R s s \<and> Abs r = Abs s)" using q by(rule Quotient3_rel[symmetric]) 
b1f099bdfbba
connect the Quotient package to the Lifting package
kuncar
parents:
47361
diff
changeset

754 
next 
b1f099bdfbba
connect the Quotient package to the Lifting package
kuncar
parents:
47361
diff
changeset

755 
show "T = (\<lambda>x y. R x x \<and> Abs x = y)" using T_def equivp_reflp[OF eR] by simp 
47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47094
diff
changeset

756 
qed 
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47094
diff
changeset

757 

35294  758 
subsection {* ML setup *} 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

759 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

760 
text {* Auxiliary data for the quotient package *} 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

761 

48891  762 
ML_file "Tools/Quotient/quotient_info.ML" 
41452  763 
setup Quotient_Info.setup 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

764 

47308  765 
declare [[mapQ3 "fun" = (fun_rel, fun_quotient3)]] 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

766 

47308  767 
lemmas [quot_thm] = fun_quotient3 
44553
4d39b032a021
avoid intermixing set and predicates; dropped lemmas mem_rsp and mem_prs (now in Quotient_Set.thy)
haftmann
parents:
44413
diff
changeset

768 
lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp id_rsp 
4d39b032a021
avoid intermixing set and predicates; dropped lemmas mem_rsp and mem_prs (now in Quotient_Set.thy)
haftmann
parents:
44413
diff
changeset

769 
lemmas [quot_preserve] = if_prs o_prs let_prs id_prs 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

770 
lemmas [quot_equiv] = identity_equivp 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

771 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

772 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

773 
text {* Lemmas about simplifying id's. *} 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

774 
lemmas [id_simps] = 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

775 
id_def[symmetric] 
40602  776 
map_fun_id 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

777 
id_apply 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

778 
id_o 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

779 
o_id 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

780 
eq_comp_r 
44413
80d460bc6fa8
Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
44242
diff
changeset

781 
vimage_id 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

782 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

783 
text {* Translation functions for the lifting process. *} 
48891  784 
ML_file "Tools/Quotient/quotient_term.ML" 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

785 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

786 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

787 
text {* Definitions of the quotient types. *} 
48891  788 
ML_file "Tools/Quotient/quotient_type.ML" 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

789 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

790 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

791 
text {* Definitions for quotient constants. *} 
48891  792 
ML_file "Tools/Quotient/quotient_def.ML" 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

793 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

794 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

795 
text {* 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

796 
An auxiliary constant for recording some information 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

797 
about the lifted theorem in a tactic. 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

798 
*} 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

799 
definition 
40466
c6587375088e
type annotations in specifications; fun_rel_def is no simp rule by default; slightly changed fun_map_def; more on predicates on relation functions; proper HOL equations in definitions
haftmann
parents:
40031
diff
changeset

800 
Quot_True :: "'a \<Rightarrow> bool" 
c6587375088e
type annotations in specifications; fun_rel_def is no simp rule by default; slightly changed fun_map_def; more on predicates on relation functions; proper HOL equations in definitions
haftmann
parents:
40031
diff
changeset

801 
where 
c6587375088e
type annotations in specifications; fun_rel_def is no simp rule by default; slightly changed fun_map_def; more on predicates on relation functions; proper HOL equations in definitions
haftmann
parents:
40031
diff
changeset

802 
"Quot_True x \<longleftrightarrow> True" 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

803 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

804 
lemma 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

805 
shows QT_all: "Quot_True (All P) \<Longrightarrow> Quot_True P" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

806 
and QT_ex: "Quot_True (Ex P) \<Longrightarrow> Quot_True P" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

807 
and QT_ex1: "Quot_True (Ex1 P) \<Longrightarrow> Quot_True P" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

808 
and QT_lam: "Quot_True (\<lambda>x. P x) \<Longrightarrow> (\<And>x. Quot_True (P x))" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

809 
and QT_ext: "(\<And>x. Quot_True (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (Quot_True a \<Longrightarrow> f = g)" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

810 
by (simp_all add: Quot_True_def ext) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

811 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

812 
lemma QT_imp: "Quot_True a \<equiv> Quot_True b" 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

813 
by (simp add: Quot_True_def) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

814 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

815 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

816 
text {* Tactics for proving the lifted theorems *} 
48891  817 
ML_file "Tools/Quotient/quotient_tacs.ML" 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

818 

35294  819 
subsection {* Methods / Interface *} 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

820 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

821 
method_setup lifting = 
37593
2505feaf2d70
separated the lifting and descending procedures in the quotient package
Christian Urban <urbanc@in.tum.de>
parents:
37564
diff
changeset

822 
{* Attrib.thms >> (fn thms => fn ctxt => 
46468  823 
SIMPLE_METHOD' (Quotient_Tacs.lift_tac ctxt [] thms)) *} 
42814  824 
{* lift theorems to quotient types *} 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

825 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

826 
method_setup lifting_setup = 
37593
2505feaf2d70
separated the lifting and descending procedures in the quotient package
Christian Urban <urbanc@in.tum.de>
parents:
37564
diff
changeset

827 
{* Attrib.thm >> (fn thm => fn ctxt => 
46468  828 
SIMPLE_METHOD' (Quotient_Tacs.lift_procedure_tac ctxt [] thm)) *} 
42814  829 
{* set up the three goals for the quotient lifting procedure *} 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

830 

37593
2505feaf2d70
separated the lifting and descending procedures in the quotient package
Christian Urban <urbanc@in.tum.de>
parents:
37564
diff
changeset

831 
method_setup descending = 
46468  832 
{* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.descend_tac ctxt [])) *} 
42814  833 
{* decend theorems to the raw level *} 
37593
2505feaf2d70
separated the lifting and descending procedures in the quotient package
Christian Urban <urbanc@in.tum.de>
parents:
37564
diff
changeset

834 

2505feaf2d70
separated the lifting and descending procedures in the quotient package
Christian Urban <urbanc@in.tum.de>
parents:
37564
diff
changeset

835 
method_setup descending_setup = 
46468  836 
{* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.descend_procedure_tac ctxt [])) *} 
42814  837 
{* set up the three goals for the decending theorems *} 
37593
2505feaf2d70
separated the lifting and descending procedures in the quotient package
Christian Urban <urbanc@in.tum.de>
parents:
37564
diff
changeset

838 

45782
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45680
diff
changeset

839 
method_setup partiality_descending = 
46468  840 
{* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.partiality_descend_tac ctxt [])) *} 
45782
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45680
diff
changeset

841 
{* decend theorems to the raw level *} 
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45680
diff
changeset

842 

f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45680
diff
changeset

843 
method_setup partiality_descending_setup = 
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45680
diff
changeset

844 
{* Scan.succeed (fn ctxt => 
46468  845 
SIMPLE_METHOD' (Quotient_Tacs.partiality_descend_procedure_tac ctxt [])) *} 
45782
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45680
diff
changeset

846 
{* set up the three goals for the decending theorems *} 
f82020ca3248
added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents:
45680
diff
changeset

847 

35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

848 
method_setup regularize = 
46468  849 
{* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.regularize_tac ctxt)) *} 
42814  850 
{* prove the regularization goals from the quotient lifting procedure *} 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

851 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

852 
method_setup injection = 
46468  853 
{* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.all_injection_tac ctxt)) *} 
42814  854 
{* prove the rep/abs injection goals from the quotient lifting procedure *} 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

855 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

856 
method_setup cleaning = 
46468  857 
{* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.clean_tac ctxt)) *} 
42814  858 
{* prove the cleaning goals from the quotient lifting procedure *} 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

859 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

860 
attribute_setup quot_lifted = 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

861 
{* Scan.succeed Quotient_Tacs.lifted_attrib *} 
42814  862 
{* lift theorems to quotient types *} 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

863 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

864 
no_notation 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

865 
rel_conj (infixr "OOO" 75) and 
40602  866 
map_fun (infixr ">" 55) and 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

867 
fun_rel (infixr "===>" 55) 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

868 

4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset

869 
end 
47488
be6dd389639d
centralized enriched_type declaration, thanks to insitu available Isar commands
haftmann
parents:
47436
diff
changeset

870 