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 copy_type_to_Quotient:
240 assumes "type_definition Rep Abs UNIV"
241 and T_def: "T \<equiv> (\<lambda>x y. Abs x = y)"
242 shows "Quotient (op =) Abs Rep T"
244 interpret type_definition Rep Abs UNIV by fact
245 from Abs_inject Rep_inverse T_def show ?thesis by (auto intro!: QuotientI)
248 lemma copy_type_to_equivp:
249 fixes Abs :: "'a \<Rightarrow> 'b"
250 and Rep :: "'b \<Rightarrow> 'a"
251 assumes "type_definition Rep Abs (UNIV::'a set)"
252 shows "equivp (op=::'a\<Rightarrow>'a\<Rightarrow>bool)"
253 by (rule identity_equivp)
255 lemma invariant_type_to_Quotient:
256 assumes "type_definition Rep Abs {x. P x}"
257 and T_def: "T \<equiv> (\<lambda>x y. (invariant P) x x \<and> Abs x = y)"
258 shows "Quotient (invariant P) Abs Rep T"
260 interpret type_definition Rep Abs "{x. P x}" by fact
261 from Rep Abs_inject Rep_inverse T_def show ?thesis by (auto intro!: QuotientI simp: invariant_def)
264 lemma invariant_type_to_part_equivp:
265 assumes "type_definition Rep Abs {x. P x}"
266 shows "part_equivp (invariant P)"
267 proof (intro part_equivpI)
268 interpret type_definition Rep Abs "{x. P x}" by fact
269 show "\<exists>x. invariant P x x" using Rep by (auto simp: invariant_def)
271 show "symp (invariant P)" by (auto intro: sympI simp: invariant_def)
273 show "transp (invariant P)" by (auto intro: transpI simp: invariant_def)
276 lemma Quotient_to_transfer:
277 assumes "Quotient R Abs Rep T" and "R c c" and "c' \<equiv> Abs c"
279 using assms by (auto dest: Quotient_cr_rel)
281 subsection {* ML setup *}
283 text {* Auxiliary data for the lifting package *}
285 use "Tools/Lifting/lifting_info.ML"
286 setup Lifting_Info.setup
288 declare [[map "fun" = (fun_rel, fun_quotient)]]
290 use "Tools/Lifting/lifting_term.ML"
292 use "Tools/Lifting/lifting_def.ML"
294 use "Tools/Lifting/lifting_setup.ML"
296 hide_const (open) invariant