author  haftmann 
Thu, 14 Feb 2013 12:24:42 +0100  
changeset 51112  da97167e03f7 
parent 48891  c0eafbd55de3 
child 51374  84d01fd733cf 
permissions  rwrr 
47308  1 
(* Title: HOL/Lifting.thy 
2 
Author: Brian Huffman and Ondrej Kuncar 

3 
Author: Cezary Kaliszyk and Christian Urban 

4 
*) 

5 

6 
header {* Lifting package *} 

7 

8 
theory Lifting 

51112  9 
imports Equiv_Relations Transfer 
47308  10 
keywords 
11 
"print_quotmaps" "print_quotients" :: diag and 

12 
"lift_definition" :: thy_goal and 

13 
"setup_lifting" :: thy_decl 

14 
begin 

15 

47325  16 
subsection {* Function map *} 
47308  17 

18 
notation map_fun (infixr ">" 55) 

19 

20 
lemma map_fun_id: 

21 
"(id > id) = id" 

22 
by (simp add: fun_eq_iff) 

23 

24 
subsection {* Quotient Predicate *} 

25 

26 
definition 

27 
"Quotient R Abs Rep T \<longleftrightarrow> 

28 
(\<forall>a. Abs (Rep a) = a) \<and> 

29 
(\<forall>a. R (Rep a) (Rep a)) \<and> 

30 
(\<forall>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s) \<and> 

31 
T = (\<lambda>x y. R x x \<and> Abs x = y)" 

32 

33 
lemma QuotientI: 

34 
assumes "\<And>a. Abs (Rep a) = a" 

35 
and "\<And>a. R (Rep a) (Rep a)" 

36 
and "\<And>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s" 

37 
and "T = (\<lambda>x y. R x x \<and> Abs x = y)" 

38 
shows "Quotient R Abs Rep T" 

39 
using assms unfolding Quotient_def by blast 

40 

47536  41 
context 
42 
fixes R Abs Rep T 

47308  43 
assumes a: "Quotient R Abs Rep T" 
47536  44 
begin 
45 

46 
lemma Quotient_abs_rep: "Abs (Rep a) = a" 

47 
using a unfolding Quotient_def 

47308  48 
by simp 
49 

47536  50 
lemma Quotient_rep_reflp: "R (Rep a) (Rep a)" 
51 
using a unfolding Quotient_def 

47308  52 
by blast 
53 

54 
lemma Quotient_rel: 

47536  55 
"R r r \<and> R s s \<and> Abs r = Abs s \<longleftrightarrow> R r s"  {* orientation does not loop on rewriting *} 
56 
using a unfolding Quotient_def 

47308  57 
by blast 
58 

47536  59 
lemma Quotient_cr_rel: "T = (\<lambda>x y. R x x \<and> Abs x = y)" 
47308  60 
using a unfolding Quotient_def 
61 
by blast 

62 

47536  63 
lemma Quotient_refl1: "R r s \<Longrightarrow> R r r" 
64 
using a unfolding Quotient_def 

65 
by fast 

66 

67 
lemma Quotient_refl2: "R r s \<Longrightarrow> R s s" 

68 
using a unfolding Quotient_def 

69 
by fast 

70 

71 
lemma Quotient_rel_rep: "R (Rep a) (Rep b) \<longleftrightarrow> a = b" 

72 
using a unfolding Quotient_def 

73 
by metis 

74 

75 
lemma Quotient_rep_abs: "R r r \<Longrightarrow> R (Rep (Abs r)) r" 

47308  76 
using a unfolding Quotient_def 
77 
by blast 

78 

47937
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47936
diff
changeset

79 
lemma Quotient_rep_abs_fold_unmap: 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47936
diff
changeset

80 
assumes "x' \<equiv> Abs x" and "R x x" and "Rep x' \<equiv> Rep' x'" 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47936
diff
changeset

81 
shows "R (Rep' x') x" 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47936
diff
changeset

82 
proof  
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47936
diff
changeset

83 
have "R (Rep x') x" using assms(12) Quotient_rep_abs by auto 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47936
diff
changeset

84 
then show ?thesis using assms(3) by simp 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47936
diff
changeset

85 
qed 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47936
diff
changeset

86 

70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47936
diff
changeset

87 
lemma Quotient_Rep_eq: 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47936
diff
changeset

88 
assumes "x' \<equiv> Abs x" 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47936
diff
changeset

89 
shows "Rep x' \<equiv> Rep x'" 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47936
diff
changeset

90 
by simp 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47936
diff
changeset

91 

47536  92 
lemma Quotient_rel_abs: "R r s \<Longrightarrow> Abs r = Abs s" 
93 
using a unfolding Quotient_def 

94 
by blast 

95 

47937
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47936
diff
changeset

96 
lemma Quotient_rel_abs2: 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47936
diff
changeset

97 
assumes "R (Rep x) y" 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47936
diff
changeset

98 
shows "x = Abs y" 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47936
diff
changeset

99 
proof  
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47936
diff
changeset

100 
from assms have "Abs (Rep x) = Abs y" by (auto intro: Quotient_rel_abs) 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47936
diff
changeset

101 
then show ?thesis using assms(1) by (simp add: Quotient_abs_rep) 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47936
diff
changeset

102 
qed 
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47936
diff
changeset

103 

47536  104 
lemma Quotient_symp: "symp R" 
47308  105 
using a unfolding Quotient_def using sympI by (metis (full_types)) 
106 

47536  107 
lemma Quotient_transp: "transp R" 
47308  108 
using a unfolding Quotient_def using transpI by (metis (full_types)) 
109 

47536  110 
lemma Quotient_part_equivp: "part_equivp R" 
111 
by (metis Quotient_rep_reflp Quotient_symp Quotient_transp part_equivpI) 

112 

113 
end 

47308  114 

115 
lemma identity_quotient: "Quotient (op =) id id (op =)" 

116 
unfolding Quotient_def by simp 

117 

47652
1b722b100301
move alternative definition lemmas into Lifting.thy;
huffman
parents:
47651
diff
changeset

118 
text {* TODO: Use one of these alternatives as the real definition. *} 
1b722b100301
move alternative definition lemmas into Lifting.thy;
huffman
parents:
47651
diff
changeset

119 

47308  120 
lemma Quotient_alt_def: 
121 
"Quotient R Abs Rep T \<longleftrightarrow> 

122 
(\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and> 

123 
(\<forall>b. T (Rep b) b) \<and> 

124 
(\<forall>x y. R x y \<longleftrightarrow> T x (Abs x) \<and> T y (Abs y) \<and> Abs x = Abs y)" 

125 
apply safe 

126 
apply (simp (no_asm_use) only: Quotient_def, fast) 

127 
apply (simp (no_asm_use) only: Quotient_def, fast) 

128 
apply (simp (no_asm_use) only: Quotient_def, fast) 

129 
apply (simp (no_asm_use) only: Quotient_def, fast) 

130 
apply (simp (no_asm_use) only: Quotient_def, fast) 

131 
apply (simp (no_asm_use) only: Quotient_def, fast) 

132 
apply (rule QuotientI) 

133 
apply simp 

134 
apply metis 

135 
apply simp 

136 
apply (rule ext, rule ext, metis) 

137 
done 

138 

139 
lemma Quotient_alt_def2: 

140 
"Quotient R Abs Rep T \<longleftrightarrow> 

141 
(\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and> 

142 
(\<forall>b. T (Rep b) b) \<and> 

143 
(\<forall>x y. R x y \<longleftrightarrow> T x (Abs y) \<and> T y (Abs x))" 

144 
unfolding Quotient_alt_def by (safe, metis+) 

145 

47652
1b722b100301
move alternative definition lemmas into Lifting.thy;
huffman
parents:
47651
diff
changeset

146 
lemma Quotient_alt_def3: 
1b722b100301
move alternative definition lemmas into Lifting.thy;
huffman
parents:
47651
diff
changeset

147 
"Quotient R Abs Rep T \<longleftrightarrow> 
1b722b100301
move alternative definition lemmas into Lifting.thy;
huffman
parents:
47651
diff
changeset

148 
(\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and> (\<forall>b. T (Rep b) b) \<and> 
1b722b100301
move alternative definition lemmas into Lifting.thy;
huffman
parents:
47651
diff
changeset

149 
(\<forall>x y. R x y \<longleftrightarrow> (\<exists>z. T x z \<and> T y z))" 
1b722b100301
move alternative definition lemmas into Lifting.thy;
huffman
parents:
47651
diff
changeset

150 
unfolding Quotient_alt_def2 by (safe, metis+) 
1b722b100301
move alternative definition lemmas into Lifting.thy;
huffman
parents:
47651
diff
changeset

151 

1b722b100301
move alternative definition lemmas into Lifting.thy;
huffman
parents:
47651
diff
changeset

152 
lemma Quotient_alt_def4: 
1b722b100301
move alternative definition lemmas into Lifting.thy;
huffman
parents:
47651
diff
changeset

153 
"Quotient R Abs Rep T \<longleftrightarrow> 
1b722b100301
move alternative definition lemmas into Lifting.thy;
huffman
parents:
47651
diff
changeset

154 
(\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and> (\<forall>b. T (Rep b) b) \<and> R = T OO conversep T" 
1b722b100301
move alternative definition lemmas into Lifting.thy;
huffman
parents:
47651
diff
changeset

155 
unfolding Quotient_alt_def3 fun_eq_iff by auto 
1b722b100301
move alternative definition lemmas into Lifting.thy;
huffman
parents:
47651
diff
changeset

156 

47308  157 
lemma fun_quotient: 
158 
assumes 1: "Quotient R1 abs1 rep1 T1" 

159 
assumes 2: "Quotient R2 abs2 rep2 T2" 

160 
shows "Quotient (R1 ===> R2) (rep1 > abs2) (abs1 > rep2) (T1 ===> T2)" 

161 
using assms unfolding Quotient_alt_def2 

162 
unfolding fun_rel_def fun_eq_iff map_fun_apply 

163 
by (safe, metis+) 

164 

165 
lemma apply_rsp: 

166 
fixes f g::"'a \<Rightarrow> 'c" 

167 
assumes q: "Quotient R1 Abs1 Rep1 T1" 

168 
and a: "(R1 ===> R2) f g" "R1 x y" 

169 
shows "R2 (f x) (g y)" 

170 
using a by (auto elim: fun_relE) 

171 

172 
lemma apply_rsp': 

173 
assumes a: "(R1 ===> R2) f g" "R1 x y" 

174 
shows "R2 (f x) (g y)" 

175 
using a by (auto elim: fun_relE) 

176 

177 
lemma apply_rsp'': 

178 
assumes "Quotient R Abs Rep T" 

179 
and "(R ===> S) f f" 

180 
shows "S (f (Rep x)) (f (Rep x))" 

181 
proof  

182 
from assms(1) have "R (Rep x) (Rep x)" by (rule Quotient_rep_reflp) 

183 
then show ?thesis using assms(2) by (auto intro: apply_rsp') 

184 
qed 

185 

186 
subsection {* Quotient composition *} 

187 

188 
lemma Quotient_compose: 

189 
assumes 1: "Quotient R1 Abs1 Rep1 T1" 

190 
assumes 2: "Quotient R2 Abs2 Rep2 T2" 

191 
shows "Quotient (T1 OO R2 OO conversep T1) (Abs2 \<circ> Abs1) (Rep1 \<circ> Rep2) (T1 OO T2)" 

47652
1b722b100301
move alternative definition lemmas into Lifting.thy;
huffman
parents:
47651
diff
changeset

192 
using assms unfolding Quotient_alt_def4 by (auto intro!: ext) 
47308  193 

47521
69f95ac85c3d
tuned the setup of lifting; generate transfer rules for typedef and Quotient thms
kuncar
parents:
47501
diff
changeset

194 
lemma equivp_reflp2: 
69f95ac85c3d
tuned the setup of lifting; generate transfer rules for typedef and Quotient thms
kuncar
parents:
47501
diff
changeset

195 
"equivp R \<Longrightarrow> reflp R" 
69f95ac85c3d
tuned the setup of lifting; generate transfer rules for typedef and Quotient thms
kuncar
parents:
47501
diff
changeset

196 
by (erule equivpE) 
69f95ac85c3d
tuned the setup of lifting; generate transfer rules for typedef and Quotient thms
kuncar
parents:
47501
diff
changeset

197 

47544  198 
subsection {* Respects predicate *} 
199 

200 
definition Respects :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set" 

201 
where "Respects R = {x. R x x}" 

202 

203 
lemma in_respects: "x \<in> Respects R \<longleftrightarrow> R x x" 

204 
unfolding Respects_def by simp 

205 

47308  206 
subsection {* Invariant *} 
207 

208 
definition invariant :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" 

209 
where "invariant R = (\<lambda>x y. R x \<and> x = y)" 

210 

211 
lemma invariant_to_eq: 

212 
assumes "invariant P x y" 

213 
shows "x = y" 

214 
using assms by (simp add: invariant_def) 

215 

216 
lemma fun_rel_eq_invariant: 

217 
shows "((invariant R) ===> S) = (\<lambda>f g. \<forall>x. R x \<longrightarrow> S (f x) (g x))" 

218 
by (auto simp add: invariant_def fun_rel_def) 

219 

220 
lemma invariant_same_args: 

221 
shows "invariant P x x \<equiv> P x" 

222 
using assms by (auto simp add: invariant_def) 

223 

47361
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

224 
lemma UNIV_typedef_to_Quotient: 
47308  225 
assumes "type_definition Rep Abs UNIV" 
47361
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

226 
and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)" 
47308  227 
shows "Quotient (op =) Abs Rep T" 
228 
proof  

229 
interpret type_definition Rep Abs UNIV by fact 

47361
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

230 
from Abs_inject Rep_inverse Abs_inverse T_def show ?thesis 
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

231 
by (fastforce intro!: QuotientI fun_eq_iff) 
47308  232 
qed 
233 

47361
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

234 
lemma UNIV_typedef_to_equivp: 
47308  235 
fixes Abs :: "'a \<Rightarrow> 'b" 
236 
and Rep :: "'b \<Rightarrow> 'a" 

237 
assumes "type_definition Rep Abs (UNIV::'a set)" 

238 
shows "equivp (op=::'a\<Rightarrow>'a\<Rightarrow>bool)" 

239 
by (rule identity_equivp) 

240 

47354  241 
lemma typedef_to_Quotient: 
47361
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

242 
assumes "type_definition Rep Abs S" 
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

243 
and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)" 
47501  244 
shows "Quotient (invariant (\<lambda>x. x \<in> S)) Abs Rep T" 
47361
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

245 
proof  
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

246 
interpret type_definition Rep Abs S by fact 
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

247 
from Rep Abs_inject Rep_inverse Abs_inverse T_def show ?thesis 
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

248 
by (auto intro!: QuotientI simp: invariant_def fun_eq_iff) 
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

249 
qed 
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

250 

87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

251 
lemma typedef_to_part_equivp: 
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

252 
assumes "type_definition Rep Abs S" 
47501  253 
shows "part_equivp (invariant (\<lambda>x. x \<in> S))" 
47361
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

254 
proof (intro part_equivpI) 
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

255 
interpret type_definition Rep Abs S by fact 
47501  256 
show "\<exists>x. invariant (\<lambda>x. x \<in> S) x x" using Rep by (auto simp: invariant_def) 
47361
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

257 
next 
47501  258 
show "symp (invariant (\<lambda>x. x \<in> S))" by (auto intro: sympI simp: invariant_def) 
47361
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

259 
next 
47501  260 
show "transp (invariant (\<lambda>x. x \<in> S))" by (auto intro: transpI simp: invariant_def) 
47361
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

261 
qed 
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

262 

87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

263 
lemma open_typedef_to_Quotient: 
47308  264 
assumes "type_definition Rep Abs {x. P x}" 
47354  265 
and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)" 
47308  266 
shows "Quotient (invariant P) Abs Rep T" 
47651  267 
using typedef_to_Quotient [OF assms] by simp 
47308  268 

47361
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

269 
lemma open_typedef_to_part_equivp: 
47308  270 
assumes "type_definition Rep Abs {x. P x}" 
271 
shows "part_equivp (invariant P)" 

47651  272 
using typedef_to_part_equivp [OF assms] by simp 
47308  273 

47376  274 
text {* Generating transfer rules for quotients. *} 
275 

47537  276 
context 
277 
fixes R Abs Rep T 

278 
assumes 1: "Quotient R Abs Rep T" 

279 
begin 

47376  280 

47537  281 
lemma Quotient_right_unique: "right_unique T" 
282 
using 1 unfolding Quotient_alt_def right_unique_def by metis 

283 

284 
lemma Quotient_right_total: "right_total T" 

285 
using 1 unfolding Quotient_alt_def right_total_def by metis 

286 

287 
lemma Quotient_rel_eq_transfer: "(T ===> T ===> op =) R (op =)" 

288 
using 1 unfolding Quotient_alt_def fun_rel_def by simp 

47376  289 

47538  290 
lemma Quotient_abs_induct: 
291 
assumes "\<And>y. R y y \<Longrightarrow> P (Abs y)" shows "P x" 

292 
using 1 assms unfolding Quotient_def by metis 

293 

47544  294 
lemma Quotient_All_transfer: 
295 
"((T ===> op =) ===> op =) (Ball (Respects R)) All" 

296 
unfolding fun_rel_def Respects_def Quotient_cr_rel [OF 1] 

297 
by (auto, metis Quotient_abs_induct) 

298 

299 
lemma Quotient_Ex_transfer: 

300 
"((T ===> op =) ===> op =) (Bex (Respects R)) Ex" 

301 
unfolding fun_rel_def Respects_def Quotient_cr_rel [OF 1] 

302 
by (auto, metis Quotient_rep_reflp [OF 1] Quotient_abs_rep [OF 1]) 

303 

304 
lemma Quotient_forall_transfer: 

305 
"((T ===> op =) ===> op =) (transfer_bforall (\<lambda>x. R x x)) transfer_forall" 

306 
using Quotient_All_transfer 

307 
unfolding transfer_forall_def transfer_bforall_def 

308 
Ball_def [abs_def] in_respects . 

309 

47537  310 
end 
311 

312 
text {* Generating transfer rules for total quotients. *} 

47376  313 

47537  314 
context 
315 
fixes R Abs Rep T 

316 
assumes 1: "Quotient R Abs Rep T" and 2: "reflp R" 

317 
begin 

47376  318 

47537  319 
lemma Quotient_bi_total: "bi_total T" 
320 
using 1 2 unfolding Quotient_alt_def bi_total_def reflp_def by auto 

321 

322 
lemma Quotient_id_abs_transfer: "(op = ===> T) (\<lambda>x. x) Abs" 

323 
using 1 2 unfolding Quotient_alt_def reflp_def fun_rel_def by simp 

324 

47575  325 
lemma Quotient_total_abs_induct: "(\<And>y. P (Abs y)) \<Longrightarrow> P x" 
326 
using 1 2 assms unfolding Quotient_alt_def reflp_def by metis 

327 

47889
29212a4bb866
lifting package produces abs_eq_iff rules for total quotients
huffman
parents:
47777
diff
changeset

328 
lemma Quotient_total_abs_eq_iff: "Abs x = Abs y \<longleftrightarrow> R x y" 
29212a4bb866
lifting package produces abs_eq_iff rules for total quotients
huffman
parents:
47777
diff
changeset

329 
using Quotient_rel [OF 1] 2 unfolding reflp_def by simp 
29212a4bb866
lifting package produces abs_eq_iff rules for total quotients
huffman
parents:
47777
diff
changeset

330 

47537  331 
end 
47376  332 

47368
4c522dff1f4d
add lemmas for generating transfer rules for typedefs
huffman
parents:
47354
diff
changeset

333 
text {* Generating transfer rules for a type defined with @{text "typedef"}. *} 
4c522dff1f4d
add lemmas for generating transfer rules for typedefs
huffman
parents:
47354
diff
changeset

334 

47534
06cc372a80ed
use context block to organize typedef lifting theorems
huffman
parents:
47521
diff
changeset

335 
context 
06cc372a80ed
use context block to organize typedef lifting theorems
huffman
parents:
47521
diff
changeset

336 
fixes Rep Abs A T 
47368
4c522dff1f4d
add lemmas for generating transfer rules for typedefs
huffman
parents:
47354
diff
changeset

337 
assumes type: "type_definition Rep Abs A" 
47534
06cc372a80ed
use context block to organize typedef lifting theorems
huffman
parents:
47521
diff
changeset

338 
assumes T_def: "T \<equiv> (\<lambda>(x::'a) (y::'b). x = Rep y)" 
06cc372a80ed
use context block to organize typedef lifting theorems
huffman
parents:
47521
diff
changeset

339 
begin 
06cc372a80ed
use context block to organize typedef lifting theorems
huffman
parents:
47521
diff
changeset

340 

06cc372a80ed
use context block to organize typedef lifting theorems
huffman
parents:
47521
diff
changeset

341 
lemma typedef_bi_unique: "bi_unique T" 
47368
4c522dff1f4d
add lemmas for generating transfer rules for typedefs
huffman
parents:
47354
diff
changeset

342 
unfolding bi_unique_def T_def 
4c522dff1f4d
add lemmas for generating transfer rules for typedefs
huffman
parents:
47354
diff
changeset

343 
by (simp add: type_definition.Rep_inject [OF type]) 
4c522dff1f4d
add lemmas for generating transfer rules for typedefs
huffman
parents:
47354
diff
changeset

344 

47535
0f94b02fda1c
lifting_setup generates transfer rule for rep of typedefs
huffman
parents:
47534
diff
changeset

345 
lemma typedef_rep_transfer: "(T ===> op =) (\<lambda>x. x) Rep" 
0f94b02fda1c
lifting_setup generates transfer rule for rep of typedefs
huffman
parents:
47534
diff
changeset

346 
unfolding fun_rel_def T_def by simp 
0f94b02fda1c
lifting_setup generates transfer rule for rep of typedefs
huffman
parents:
47534
diff
changeset

347 

47545  348 
lemma typedef_All_transfer: "((T ===> op =) ===> op =) (Ball A) All" 
47534
06cc372a80ed
use context block to organize typedef lifting theorems
huffman
parents:
47521
diff
changeset

349 
unfolding T_def fun_rel_def 
06cc372a80ed
use context block to organize typedef lifting theorems
huffman
parents:
47521
diff
changeset

350 
by (metis type_definition.Rep [OF type] 
06cc372a80ed
use context block to organize typedef lifting theorems
huffman
parents:
47521
diff
changeset

351 
type_definition.Abs_inverse [OF type]) 
06cc372a80ed
use context block to organize typedef lifting theorems
huffman
parents:
47521
diff
changeset

352 

47545  353 
lemma typedef_Ex_transfer: "((T ===> op =) ===> op =) (Bex A) Ex" 
354 
unfolding T_def fun_rel_def 

355 
by (metis type_definition.Rep [OF type] 

356 
type_definition.Abs_inverse [OF type]) 

357 

358 
lemma typedef_forall_transfer: 

47534
06cc372a80ed
use context block to organize typedef lifting theorems
huffman
parents:
47521
diff
changeset

359 
"((T ===> op =) ===> op =) 
06cc372a80ed
use context block to organize typedef lifting theorems
huffman
parents:
47521
diff
changeset

360 
(transfer_bforall (\<lambda>x. x \<in> A)) transfer_forall" 
06cc372a80ed
use context block to organize typedef lifting theorems
huffman
parents:
47521
diff
changeset

361 
unfolding transfer_bforall_def transfer_forall_def Ball_def [symmetric] 
47545  362 
by (rule typedef_All_transfer) 
47534
06cc372a80ed
use context block to organize typedef lifting theorems
huffman
parents:
47521
diff
changeset

363 

06cc372a80ed
use context block to organize typedef lifting theorems
huffman
parents:
47521
diff
changeset

364 
end 
06cc372a80ed
use context block to organize typedef lifting theorems
huffman
parents:
47521
diff
changeset

365 

47368
4c522dff1f4d
add lemmas for generating transfer rules for typedefs
huffman
parents:
47354
diff
changeset

366 
text {* Generating the correspondence rule for a constant defined with 
4c522dff1f4d
add lemmas for generating transfer rules for typedefs
huffman
parents:
47354
diff
changeset

367 
@{text "lift_definition"}. *} 
4c522dff1f4d
add lemmas for generating transfer rules for typedefs
huffman
parents:
47354
diff
changeset

368 

47351  369 
lemma Quotient_to_transfer: 
370 
assumes "Quotient R Abs Rep T" and "R c c" and "c' \<equiv> Abs c" 

371 
shows "T c c'" 

372 
using assms by (auto dest: Quotient_cr_rel) 

373 

47982
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset

374 
text {* Proving reflexivity *} 
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset

375 

7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset

376 
definition left_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" 
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset

377 
where "left_total R \<longleftrightarrow> (\<forall>x. \<exists>y. R x y)" 
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset

378 

7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset

379 
lemma left_totalI: 
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset

380 
"(\<And>x. \<exists>y. R x y) \<Longrightarrow> left_total R" 
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset

381 
unfolding left_total_def by blast 
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset

382 

7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset

383 
lemma left_totalE: 
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset

384 
assumes "left_total R" 
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset

385 
obtains "(\<And>x. \<exists>y. R x y)" 
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset

386 
using assms unfolding left_total_def by blast 
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset

387 

7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset

388 
lemma Quotient_to_left_total: 
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset

389 
assumes q: "Quotient R Abs Rep T" 
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset

390 
and r_R: "reflp R" 
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset

391 
shows "left_total T" 
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset

392 
using r_R Quotient_cr_rel[OF q] unfolding left_total_def by (auto elim: reflpE) 
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset

393 

7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset

394 
lemma reflp_Quotient_composition: 
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset

395 
assumes lt_R1: "left_total R1" 
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset

396 
and r_R2: "reflp R2" 
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset

397 
shows "reflp (R1 OO R2 OO R1\<inverse>\<inverse>)" 
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset

398 
using assms 
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset

399 
proof  
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset

400 
{ 
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset

401 
fix x 
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset

402 
from lt_R1 obtain y where "R1 x y" unfolding left_total_def by blast 
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset

403 
moreover then have "R1\<inverse>\<inverse> y x" by simp 
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset

404 
moreover have "R2 y y" using r_R2 by (auto elim: reflpE) 
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset

405 
ultimately have "(R1 OO R2 OO R1\<inverse>\<inverse>) x x" by auto 
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset

406 
} 
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset

407 
then show ?thesis by (auto intro: reflpI) 
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset

408 
qed 
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset

409 

7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset

410 
lemma reflp_equality: "reflp (op =)" 
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset

411 
by (auto intro: reflpI) 
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset

412 

47308  413 
subsection {* ML setup *} 
414 

48891  415 
ML_file "Tools/Lifting/lifting_util.ML" 
47308  416 

48891  417 
ML_file "Tools/Lifting/lifting_info.ML" 
47308  418 
setup Lifting_Info.setup 
419 

47777
f29e7dcd7c40
use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents:
47698
diff
changeset

420 
declare fun_quotient[quot_map] 
47982
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47937
diff
changeset

421 
lemmas [reflexivity_rule] = reflp_equality reflp_Quotient_composition 
47308  422 

48891  423 
ML_file "Tools/Lifting/lifting_term.ML" 
47308  424 

48891  425 
ML_file "Tools/Lifting/lifting_def.ML" 
47308  426 

48891  427 
ML_file "Tools/Lifting/lifting_setup.ML" 
47308  428 

429 
hide_const (open) invariant 

430 

431 
end 