1 (* Title: HOL/Lifting.thy
2 Author: Brian Huffman and Ondrej Kuncar
3 Author: Cezary Kaliszyk and Christian Urban
6 header {* Lifting package *}
9 imports Plain Equiv_Relations Transfer
11 "print_quotmaps" "print_quotients" :: diag and
12 "lift_definition" :: thy_goal and
13 "setup_lifting" :: thy_decl
15 ("Tools/Lifting/lifting_info.ML")
16 ("Tools/Lifting/lifting_term.ML")
17 ("Tools/Lifting/lifting_def.ML")
18 ("Tools/Lifting/lifting_setup.ML")
21 subsection {* Function map *}
23 notation map_fun (infixr "--->" 55)
27 by (simp add: fun_eq_iff)
29 subsection {* Quotient Predicate *}
32 "Quotient R Abs Rep T \<longleftrightarrow>
33 (\<forall>a. Abs (Rep a) = a) \<and>
34 (\<forall>a. R (Rep a) (Rep a)) \<and>
35 (\<forall>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s) \<and>
36 T = (\<lambda>x y. R x x \<and> Abs x = y)"
39 assumes "\<And>a. Abs (Rep a) = a"
40 and "\<And>a. R (Rep a) (Rep a)"
41 and "\<And>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s"
42 and "T = (\<lambda>x y. R x x \<and> Abs x = y)"
43 shows "Quotient R Abs Rep T"
44 using assms unfolding Quotient_def by blast
46 lemma Quotient_abs_rep:
47 assumes a: "Quotient R Abs Rep T"
48 shows "Abs (Rep a) = a"
50 unfolding Quotient_def
53 lemma Quotient_rep_reflp:
54 assumes a: "Quotient R Abs Rep T"
55 shows "R (Rep a) (Rep a)"
57 unfolding Quotient_def
61 assumes a: "Quotient R Abs Rep T"
62 shows "R r r \<and> R s s \<and> Abs r = Abs s \<longleftrightarrow> R r s" -- {* orientation does not loop on rewriting *}
64 unfolding Quotient_def
67 lemma Quotient_cr_rel:
68 assumes a: "Quotient R Abs Rep T"
69 shows "T = (\<lambda>x y. R x x \<and> Abs x = y)"
71 unfolding Quotient_def
75 assumes a: "Quotient R Abs Rep T"
76 shows "R r s \<Longrightarrow> R r r"
77 using a unfolding Quotient_def
81 assumes a: "Quotient R Abs Rep T"
82 shows "R r s \<Longrightarrow> R s s"
83 using a unfolding Quotient_def
86 lemma Quotient_rel_rep:
87 assumes a: "Quotient R Abs Rep T"
88 shows "R (Rep a) (Rep b) \<longleftrightarrow> a = b"
90 unfolding Quotient_def
93 lemma Quotient_rep_abs:
94 assumes a: "Quotient R Abs Rep T"
95 shows "R r r \<Longrightarrow> R (Rep (Abs r)) r"
96 using a unfolding Quotient_def
99 lemma Quotient_rel_abs:
100 assumes a: "Quotient R Abs Rep T"
101 shows "R r s \<Longrightarrow> Abs r = Abs s"
102 using a unfolding Quotient_def
106 assumes a: "Quotient R Abs Rep T"
108 using a unfolding Quotient_def using sympI by (metis (full_types))
110 lemma Quotient_transp:
111 assumes a: "Quotient R Abs Rep T"
113 using a unfolding Quotient_def using transpI by (metis (full_types))
115 lemma Quotient_part_equivp:
116 assumes a: "Quotient R Abs Rep T"
117 shows "part_equivp R"
118 by (metis Quotient_rep_reflp Quotient_symp Quotient_transp a part_equivpI)
120 lemma identity_quotient: "Quotient (op =) id id (op =)"
121 unfolding Quotient_def by simp
123 lemma Quotient_alt_def:
124 "Quotient R Abs Rep T \<longleftrightarrow>
125 (\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and>
126 (\<forall>b. T (Rep b) b) \<and>
127 (\<forall>x y. R x y \<longleftrightarrow> T x (Abs x) \<and> T y (Abs y) \<and> Abs x = Abs y)"
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 (simp (no_asm_use) only: Quotient_def, fast)
133 apply (simp (no_asm_use) only: Quotient_def, fast)
134 apply (simp (no_asm_use) only: Quotient_def, fast)
135 apply (rule QuotientI)
139 apply (rule ext, rule ext, metis)
142 lemma Quotient_alt_def2:
143 "Quotient R Abs Rep T \<longleftrightarrow>
144 (\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and>
145 (\<forall>b. T (Rep b) b) \<and>
146 (\<forall>x y. R x y \<longleftrightarrow> T x (Abs y) \<and> T y (Abs x))"
147 unfolding Quotient_alt_def by (safe, metis+)
150 assumes 1: "Quotient R1 abs1 rep1 T1"
151 assumes 2: "Quotient R2 abs2 rep2 T2"
152 shows "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2) (T1 ===> T2)"
153 using assms unfolding Quotient_alt_def2
154 unfolding fun_rel_def fun_eq_iff map_fun_apply
158 fixes f g::"'a \<Rightarrow> 'c"
159 assumes q: "Quotient R1 Abs1 Rep1 T1"
160 and a: "(R1 ===> R2) f g" "R1 x y"
161 shows "R2 (f x) (g y)"
162 using a by (auto elim: fun_relE)
165 assumes a: "(R1 ===> R2) f g" "R1 x y"
166 shows "R2 (f x) (g y)"
167 using a by (auto elim: fun_relE)
170 assumes "Quotient R Abs Rep T"
172 shows "S (f (Rep x)) (f (Rep x))"
174 from assms(1) have "R (Rep x) (Rep x)" by (rule Quotient_rep_reflp)
175 then show ?thesis using assms(2) by (auto intro: apply_rsp')
178 subsection {* Quotient composition *}
180 lemma Quotient_compose:
181 assumes 1: "Quotient R1 Abs1 Rep1 T1"
182 assumes 2: "Quotient R2 Abs2 Rep2 T2"
183 shows "Quotient (T1 OO R2 OO conversep T1) (Abs2 \<circ> Abs1) (Rep1 \<circ> Rep2) (T1 OO T2)"
185 from 1 have Abs1: "\<And>a b. T1 a b \<Longrightarrow> Abs1 a = b"
186 unfolding Quotient_alt_def by simp
187 from 1 have Rep1: "\<And>b. T1 (Rep1 b) b"
188 unfolding Quotient_alt_def by simp
189 from 2 have Abs2: "\<And>a b. T2 a b \<Longrightarrow> Abs2 a = b"
190 unfolding Quotient_alt_def by simp
191 from 2 have Rep2: "\<And>b. T2 (Rep2 b) b"
192 unfolding Quotient_alt_def by simp
194 "\<And>x y. R2 x y \<longleftrightarrow> T2 x (Abs2 x) \<and> T2 y (Abs2 y) \<and> Abs2 x = Abs2 y"
195 unfolding Quotient_alt_def by simp
197 unfolding Quotient_alt_def
200 apply (drule Abs1, simp)
202 apply (rule pred_compI)
205 apply (rule pred_compI, assumption)
206 apply (drule Abs1, simp)
207 apply (clarsimp simp add: R2)
208 apply (rule pred_compI, assumption)
209 apply (drule Abs1, simp)+
210 apply (clarsimp simp add: R2)
211 apply (drule Abs1, simp)+
212 apply (clarsimp simp add: R2)
213 apply (rule pred_compI, assumption)
214 apply (rule pred_compI [rotated])
215 apply (erule conversepI)
216 apply (drule Abs1, simp)+
221 subsection {* Invariant *}
223 definition invariant :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
224 where "invariant R = (\<lambda>x y. R x \<and> x = y)"
226 lemma invariant_to_eq:
227 assumes "invariant P x y"
229 using assms by (simp add: invariant_def)
231 lemma fun_rel_eq_invariant:
232 shows "((invariant R) ===> S) = (\<lambda>f g. \<forall>x. R x \<longrightarrow> S (f x) (g x))"
233 by (auto simp add: invariant_def fun_rel_def)
235 lemma invariant_same_args:
236 shows "invariant P x x \<equiv> P x"
237 using assms by (auto simp add: invariant_def)
239 lemma UNIV_typedef_to_Quotient:
240 assumes "type_definition Rep Abs UNIV"
241 and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
242 shows "Quotient (op =) Abs Rep T"
244 interpret type_definition Rep Abs UNIV by fact
245 from Abs_inject Rep_inverse Abs_inverse T_def show ?thesis
246 by (fastforce intro!: QuotientI fun_eq_iff)
249 lemma UNIV_typedef_to_equivp:
250 fixes Abs :: "'a \<Rightarrow> 'b"
251 and Rep :: "'b \<Rightarrow> 'a"
252 assumes "type_definition Rep Abs (UNIV::'a set)"
253 shows "equivp (op=::'a\<Rightarrow>'a\<Rightarrow>bool)"
254 by (rule identity_equivp)
256 lemma typedef_to_Quotient:
257 assumes "type_definition Rep Abs S"
258 and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
259 shows "Quotient (Lifting.invariant (\<lambda>x. x \<in> S)) Abs Rep T"
261 interpret type_definition Rep Abs S by fact
262 from Rep Abs_inject Rep_inverse Abs_inverse T_def show ?thesis
263 by (auto intro!: QuotientI simp: invariant_def fun_eq_iff)
266 lemma typedef_to_part_equivp:
267 assumes "type_definition Rep Abs S"
268 shows "part_equivp (Lifting.invariant (\<lambda>x. x \<in> S))"
269 proof (intro part_equivpI)
270 interpret type_definition Rep Abs S by fact
271 show "\<exists>x. Lifting.invariant (\<lambda>x. x \<in> S) x x" using Rep by (auto simp: invariant_def)
273 show "symp (Lifting.invariant (\<lambda>x. x \<in> S))" by (auto intro: sympI simp: invariant_def)
275 show "transp (Lifting.invariant (\<lambda>x. x \<in> S))" by (auto intro: transpI simp: invariant_def)
278 lemma open_typedef_to_Quotient:
279 assumes "type_definition Rep Abs {x. P x}"
280 and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
281 shows "Quotient (invariant P) Abs Rep T"
283 interpret type_definition Rep Abs "{x. P x}" by fact
284 from Rep Abs_inject Rep_inverse Abs_inverse T_def show ?thesis
285 by (auto intro!: QuotientI simp: invariant_def fun_eq_iff)
288 lemma open_typedef_to_part_equivp:
289 assumes "type_definition Rep Abs {x. P x}"
290 shows "part_equivp (invariant P)"
291 proof (intro part_equivpI)
292 interpret type_definition Rep Abs "{x. P x}" by fact
293 show "\<exists>x. invariant P x x" using Rep by (auto simp: invariant_def)
295 show "symp (invariant P)" by (auto intro: sympI simp: invariant_def)
297 show "transp (invariant P)" by (auto intro: transpI simp: invariant_def)
300 text {* Generating transfer rules for quotients. *}
302 lemma Quotient_right_unique:
303 assumes "Quotient R Abs Rep T" shows "right_unique T"
304 using assms unfolding Quotient_alt_def right_unique_def by metis
306 lemma Quotient_right_total:
307 assumes "Quotient R Abs Rep T" shows "right_total T"
308 using assms unfolding Quotient_alt_def right_total_def by metis
310 lemma Quotient_rel_eq_transfer:
311 assumes "Quotient R Abs Rep T"
312 shows "(T ===> T ===> op =) R (op =)"
313 using assms unfolding Quotient_alt_def fun_rel_def by simp
315 lemma Quotient_bi_total:
316 assumes "Quotient R Abs Rep T" and "reflp R"
318 using assms unfolding Quotient_alt_def bi_total_def reflp_def by auto
320 lemma Quotient_id_abs_transfer:
321 assumes "Quotient R Abs Rep T" and "reflp R"
322 shows "(op = ===> T) (\<lambda>x. x) Abs"
323 using assms unfolding Quotient_alt_def reflp_def fun_rel_def by simp
325 text {* Generating transfer rules for a type defined with @{text "typedef"}. *}
327 lemma typedef_bi_unique:
328 assumes type: "type_definition Rep Abs A"
329 assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
331 unfolding bi_unique_def T_def
332 by (simp add: type_definition.Rep_inject [OF type])
334 lemma typedef_right_total:
335 assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
336 shows "right_total T"
337 unfolding right_total_def T_def by simp
339 lemma copy_type_bi_total:
340 assumes type: "type_definition Rep Abs UNIV"
341 assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
343 unfolding bi_total_def T_def
344 by (metis type_definition.Abs_inverse [OF type] UNIV_I)
346 lemma typedef_transfer_All:
347 assumes type: "type_definition Rep Abs A"
348 assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
349 shows "((T ===> op =) ===> op =) (Ball A) All"
350 unfolding T_def fun_rel_def
351 by (metis type_definition.Rep [OF type]
352 type_definition.Abs_inverse [OF type])
354 lemma typedef_transfer_Ex:
355 assumes type: "type_definition Rep Abs A"
356 assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
357 shows "((T ===> op =) ===> op =) (Bex A) Ex"
358 unfolding T_def fun_rel_def
359 by (metis type_definition.Rep [OF type]
360 type_definition.Abs_inverse [OF type])
362 lemma typedef_transfer_bforall:
363 assumes type: "type_definition Rep Abs A"
364 assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
365 shows "((T ===> op =) ===> op =)
366 (transfer_bforall (\<lambda>x. x \<in> A)) transfer_forall"
367 unfolding transfer_bforall_def transfer_forall_def Ball_def [symmetric]
368 by (rule typedef_transfer_All [OF assms])
370 text {* Generating the correspondence rule for a constant defined with
371 @{text "lift_definition"}. *}
373 lemma Quotient_to_transfer:
374 assumes "Quotient R Abs Rep T" and "R c c" and "c' \<equiv> Abs c"
376 using assms by (auto dest: Quotient_cr_rel)
378 subsection {* ML setup *}
380 text {* Auxiliary data for the lifting package *}
382 use "Tools/Lifting/lifting_info.ML"
383 setup Lifting_Info.setup
385 declare [[map "fun" = (fun_rel, fun_quotient)]]
387 use "Tools/Lifting/lifting_term.ML"
389 use "Tools/Lifting/lifting_def.ML"
391 use "Tools/Lifting/lifting_setup.ML"
393 hide_const (open) invariant