src/HOL/Quotient.thy
 author huffman Thu Aug 11 09:11:15 2011 -0700 (2011-08-11) changeset 44165 d26a45f3c835 parent 42814 5af15f1e2ef6 child 44204 3cdc4176638c permissions -rw-r--r--
remove lemma stupid_ext
1 (*  Title:      HOL/Quotient.thy
2     Author:     Cezary Kaliszyk and Christian Urban
3 *)
5 header {* Definition of Quotient Types *}
7 theory Quotient
8 imports Plain Hilbert_Choice Equiv_Relations
9 uses
10   ("Tools/Quotient/quotient_info.ML")
11   ("Tools/Quotient/quotient_typ.ML")
12   ("Tools/Quotient/quotient_def.ML")
13   ("Tools/Quotient/quotient_term.ML")
14   ("Tools/Quotient/quotient_tacs.ML")
15 begin
17 text {*
18   Basic definition for equivalence relations
19   that are represented by predicates.
20 *}
22 text {* Composition of Relations *}
24 abbreviation
25   rel_conj :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" (infixr "OOO" 75)
26 where
27   "r1 OOO r2 \<equiv> r1 OO r2 OO r1"
29 lemma eq_comp_r:
30   shows "((op =) OOO R) = R"
31   by (auto simp add: fun_eq_iff)
33 subsection {* Respects predicate *}
35 definition
36   Respects :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set"
37 where
38   "Respects R x = R x x"
40 lemma in_respects:
41   shows "x \<in> Respects R \<longleftrightarrow> R x x"
42   unfolding mem_def Respects_def
43   by simp
45 subsection {* Function map and function relation *}
47 notation map_fun (infixr "--->" 55)
49 lemma map_fun_id:
50   "(id ---> id) = id"
51   by (simp add: fun_eq_iff)
53 definition
54   fun_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> bool" (infixr "===>" 55)
55 where
56   "fun_rel R1 R2 = (\<lambda>f g. \<forall>x y. R1 x y \<longrightarrow> R2 (f x) (g y))"
58 lemma fun_relI [intro]:
59   assumes "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"
60   shows "(R1 ===> R2) f g"
61   using assms by (simp add: fun_rel_def)
63 lemma fun_relE:
64   assumes "(R1 ===> R2) f g" and "R1 x y"
65   obtains "R2 (f x) (g y)"
66   using assms by (simp add: fun_rel_def)
68 lemma fun_rel_eq:
69   shows "((op =) ===> (op =)) = (op =)"
70   by (auto simp add: fun_eq_iff elim: fun_relE)
73 subsection {* Quotient Predicate *}
75 definition
76   "Quotient R Abs Rep \<longleftrightarrow>
77      (\<forall>a. Abs (Rep a) = a) \<and> (\<forall>a. R (Rep a) (Rep a)) \<and>
78      (\<forall>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s)"
80 lemma QuotientI:
81   assumes "\<And>a. Abs (Rep a) = a"
82     and "\<And>a. R (Rep a) (Rep a)"
83     and "\<And>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s"
84   shows "Quotient R Abs Rep"
85   using assms unfolding Quotient_def by blast
87 lemma Quotient_abs_rep:
88   assumes a: "Quotient R Abs Rep"
89   shows "Abs (Rep a) = a"
90   using a
91   unfolding Quotient_def
92   by simp
94 lemma Quotient_rep_reflp:
95   assumes a: "Quotient R Abs Rep"
96   shows "R (Rep a) (Rep a)"
97   using a
98   unfolding Quotient_def
99   by blast
101 lemma Quotient_rel:
102   assumes a: "Quotient R Abs Rep"
103   shows "R r r \<and> R s s \<and> Abs r = Abs s \<longleftrightarrow> R r s" -- {* orientation does not loop on rewriting *}
104   using a
105   unfolding Quotient_def
106   by blast
108 lemma Quotient_rel_rep:
109   assumes a: "Quotient R Abs Rep"
110   shows "R (Rep a) (Rep b) \<longleftrightarrow> a = b"
111   using a
112   unfolding Quotient_def
113   by metis
115 lemma Quotient_rep_abs:
116   assumes a: "Quotient R Abs Rep"
117   shows "R r r \<Longrightarrow> R (Rep (Abs r)) r"
118   using a unfolding Quotient_def
119   by blast
121 lemma Quotient_rel_abs:
122   assumes a: "Quotient R Abs Rep"
123   shows "R r s \<Longrightarrow> Abs r = Abs s"
124   using a unfolding Quotient_def
125   by blast
127 lemma Quotient_symp:
128   assumes a: "Quotient R Abs Rep"
129   shows "symp R"
130   using a unfolding Quotient_def using sympI by metis
132 lemma Quotient_transp:
133   assumes a: "Quotient R Abs Rep"
134   shows "transp R"
135   using a unfolding Quotient_def using transpI by metis
137 lemma identity_quotient:
138   shows "Quotient (op =) id id"
139   unfolding Quotient_def id_def
140   by blast
142 lemma fun_quotient:
143   assumes q1: "Quotient R1 abs1 rep1"
144   and     q2: "Quotient R2 abs2 rep2"
145   shows "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)"
146 proof -
147   have "\<And>a. (rep1 ---> abs2) ((abs1 ---> rep2) a) = a"
148     using q1 q2 by (simp add: Quotient_def fun_eq_iff)
149   moreover
150   have "\<And>a. (R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)"
151     by (rule fun_relI)
152       (insert q1 q2 Quotient_rel_abs [of R1 abs1 rep1] Quotient_rel_rep [of R2 abs2 rep2],
153         simp (no_asm) add: Quotient_def, simp)
154   moreover
155   have "\<And>r s. (R1 ===> R2) r s = ((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and>
156         (rep1 ---> abs2) r  = (rep1 ---> abs2) s)"
157     apply(auto simp add: fun_rel_def fun_eq_iff)
158     using q1 q2 unfolding Quotient_def
159     apply(metis)
160     using q1 q2 unfolding Quotient_def
161     apply(metis)
162     using q1 q2 unfolding Quotient_def
163     apply(metis)
164     using q1 q2 unfolding Quotient_def
165     apply(metis)
166     done
167   ultimately
168   show "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)"
169     unfolding Quotient_def by blast
170 qed
172 lemma abs_o_rep:
173   assumes a: "Quotient R Abs Rep"
174   shows "Abs o Rep = id"
175   unfolding fun_eq_iff
176   by (simp add: Quotient_abs_rep[OF a])
178 lemma equals_rsp:
179   assumes q: "Quotient R Abs Rep"
180   and     a: "R xa xb" "R ya yb"
181   shows "R xa ya = R xb yb"
182   using a Quotient_symp[OF q] Quotient_transp[OF q]
183   by (blast elim: sympE transpE)
185 lemma lambda_prs:
186   assumes q1: "Quotient R1 Abs1 Rep1"
187   and     q2: "Quotient R2 Abs2 Rep2"
188   shows "(Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) = (\<lambda>x. f x)"
189   unfolding fun_eq_iff
190   using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
191   by simp
193 lemma lambda_prs1:
194   assumes q1: "Quotient R1 Abs1 Rep1"
195   and     q2: "Quotient R2 Abs2 Rep2"
196   shows "(Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x) = (\<lambda>x. f x)"
197   unfolding fun_eq_iff
198   using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
199   by simp
201 lemma rep_abs_rsp:
202   assumes q: "Quotient R Abs Rep"
203   and     a: "R x1 x2"
204   shows "R x1 (Rep (Abs x2))"
205   using a Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q]
206   by metis
208 lemma rep_abs_rsp_left:
209   assumes q: "Quotient R Abs Rep"
210   and     a: "R x1 x2"
211   shows "R (Rep (Abs x1)) x2"
212   using a Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q]
213   by metis
215 text{*
216   In the following theorem R1 can be instantiated with anything,
217   but we know some of the types of the Rep and Abs functions;
218   so by solving Quotient assumptions we can get a unique R1 that
219   will be provable; which is why we need to use @{text apply_rsp} and
220   not the primed version *}
222 lemma apply_rsp:
223   fixes f g::"'a \<Rightarrow> 'c"
224   assumes q: "Quotient R1 Abs1 Rep1"
225   and     a: "(R1 ===> R2) f g" "R1 x y"
226   shows "R2 (f x) (g y)"
227   using a by (auto elim: fun_relE)
229 lemma apply_rsp':
230   assumes a: "(R1 ===> R2) f g" "R1 x y"
231   shows "R2 (f x) (g y)"
232   using a by (auto elim: fun_relE)
234 subsection {* lemmas for regularisation of ball and bex *}
236 lemma ball_reg_eqv:
237   fixes P :: "'a \<Rightarrow> bool"
238   assumes a: "equivp R"
239   shows "Ball (Respects R) P = (All P)"
240   using a
241   unfolding equivp_def
242   by (auto simp add: in_respects)
244 lemma bex_reg_eqv:
245   fixes P :: "'a \<Rightarrow> bool"
246   assumes a: "equivp R"
247   shows "Bex (Respects R) P = (Ex P)"
248   using a
249   unfolding equivp_def
250   by (auto simp add: in_respects)
252 lemma ball_reg_right:
253   assumes a: "\<And>x. R x \<Longrightarrow> P x \<longrightarrow> Q x"
254   shows "All P \<longrightarrow> Ball R Q"
255   using a by (metis Collect_def Collect_mem_eq)
257 lemma bex_reg_left:
258   assumes a: "\<And>x. R x \<Longrightarrow> Q x \<longrightarrow> P x"
259   shows "Bex R Q \<longrightarrow> Ex P"
260   using a by (metis Collect_def Collect_mem_eq)
262 lemma ball_reg_left:
263   assumes a: "equivp R"
264   shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ball (Respects R) Q \<longrightarrow> All P"
265   using a by (metis equivp_reflp in_respects)
267 lemma bex_reg_right:
268   assumes a: "equivp R"
269   shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ex Q \<longrightarrow> Bex (Respects R) P"
270   using a by (metis equivp_reflp in_respects)
272 lemma ball_reg_eqv_range:
273   fixes P::"'a \<Rightarrow> bool"
274   and x::"'a"
275   assumes a: "equivp R2"
276   shows   "(Ball (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = All (\<lambda>f. P (f x)))"
277   apply(rule iffI)
278   apply(rule allI)
279   apply(drule_tac x="\<lambda>y. f x" in bspec)
280   apply(simp add: in_respects fun_rel_def)
281   apply(rule impI)
282   using a equivp_reflp_symp_transp[of "R2"]
283   apply (auto elim: equivpE reflpE)
284   done
286 lemma bex_reg_eqv_range:
287   assumes a: "equivp R2"
288   shows   "(Bex (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = Ex (\<lambda>f. P (f x)))"
289   apply(auto)
290   apply(rule_tac x="\<lambda>y. f x" in bexI)
291   apply(simp)
292   apply(simp add: Respects_def in_respects fun_rel_def)
293   apply(rule impI)
294   using a equivp_reflp_symp_transp[of "R2"]
295   apply (auto elim: equivpE reflpE)
296   done
298 (* Next four lemmas are unused *)
299 lemma all_reg:
300   assumes a: "!x :: 'a. (P x --> Q x)"
301   and     b: "All P"
302   shows "All Q"
303   using a b by (metis)
305 lemma ex_reg:
306   assumes a: "!x :: 'a. (P x --> Q x)"
307   and     b: "Ex P"
308   shows "Ex Q"
309   using a b by metis
311 lemma ball_reg:
312   assumes a: "!x :: 'a. (R x --> P x --> Q x)"
313   and     b: "Ball R P"
314   shows "Ball R Q"
315   using a b by (metis Collect_def Collect_mem_eq)
317 lemma bex_reg:
318   assumes a: "!x :: 'a. (R x --> P x --> Q x)"
319   and     b: "Bex R P"
320   shows "Bex R Q"
321   using a b by (metis Collect_def Collect_mem_eq)
324 lemma ball_all_comm:
325   assumes "\<And>y. (\<forall>x\<in>P. A x y) \<longrightarrow> (\<forall>x. B x y)"
326   shows "(\<forall>x\<in>P. \<forall>y. A x y) \<longrightarrow> (\<forall>x. \<forall>y. B x y)"
327   using assms by auto
329 lemma bex_ex_comm:
330   assumes "(\<exists>y. \<exists>x. A x y) \<longrightarrow> (\<exists>y. \<exists>x\<in>P. B x y)"
331   shows "(\<exists>x. \<exists>y. A x y) \<longrightarrow> (\<exists>x\<in>P. \<exists>y. B x y)"
332   using assms by auto
334 subsection {* Bounded abstraction *}
336 definition
337   Babs :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
338 where
339   "x \<in> p \<Longrightarrow> Babs p m x = m x"
341 lemma babs_rsp:
342   assumes q: "Quotient R1 Abs1 Rep1"
343   and     a: "(R1 ===> R2) f g"
344   shows      "(R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)"
345   apply (auto simp add: Babs_def in_respects fun_rel_def)
346   apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1")
347   using a apply (simp add: Babs_def fun_rel_def)
348   apply (simp add: in_respects fun_rel_def)
349   using Quotient_rel[OF q]
350   by metis
352 lemma babs_prs:
353   assumes q1: "Quotient R1 Abs1 Rep1"
354   and     q2: "Quotient R2 Abs2 Rep2"
355   shows "((Rep1 ---> Abs2) (Babs (Respects R1) ((Abs1 ---> Rep2) f))) = f"
356   apply (rule ext)
357   apply (simp add:)
358   apply (subgoal_tac "Rep1 x \<in> Respects R1")
359   apply (simp add: Babs_def Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
360   apply (simp add: in_respects Quotient_rel_rep[OF q1])
361   done
363 lemma babs_simp:
364   assumes q: "Quotient R1 Abs Rep"
365   shows "((R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)) = ((R1 ===> R2) f g)"
366   apply(rule iffI)
367   apply(simp_all only: babs_rsp[OF q])
368   apply(auto simp add: Babs_def fun_rel_def)
369   apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1")
370   apply(metis Babs_def)
371   apply (simp add: in_respects)
372   using Quotient_rel[OF q]
373   by metis
375 (* If a user proves that a particular functional relation
376    is an equivalence this may be useful in regularising *)
377 lemma babs_reg_eqv:
378   shows "equivp R \<Longrightarrow> Babs (Respects R) P = P"
379   by (simp add: fun_eq_iff Babs_def in_respects equivp_reflp)
382 (* 3 lemmas needed for proving repabs_inj *)
383 lemma ball_rsp:
384   assumes a: "(R ===> (op =)) f g"
385   shows "Ball (Respects R) f = Ball (Respects R) g"
386   using a by (auto simp add: Ball_def in_respects elim: fun_relE)
388 lemma bex_rsp:
389   assumes a: "(R ===> (op =)) f g"
390   shows "(Bex (Respects R) f = Bex (Respects R) g)"
391   using a by (auto simp add: Bex_def in_respects elim: fun_relE)
393 lemma bex1_rsp:
394   assumes a: "(R ===> (op =)) f g"
395   shows "Ex1 (\<lambda>x. x \<in> Respects R \<and> f x) = Ex1 (\<lambda>x. x \<in> Respects R \<and> g x)"
396   using a by (auto elim: fun_relE simp add: Ex1_def in_respects)
398 (* 2 lemmas needed for cleaning of quantifiers *)
399 lemma all_prs:
400   assumes a: "Quotient R absf repf"
401   shows "Ball (Respects R) ((absf ---> id) f) = All f"
402   using a unfolding Quotient_def Ball_def in_respects id_apply comp_def map_fun_def
403   by metis
405 lemma ex_prs:
406   assumes a: "Quotient R absf repf"
407   shows "Bex (Respects R) ((absf ---> id) f) = Ex f"
408   using a unfolding Quotient_def Bex_def in_respects id_apply comp_def map_fun_def
409   by metis
411 subsection {* @{text Bex1_rel} quantifier *}
413 definition
414   Bex1_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
415 where
416   "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)))"
418 lemma bex1_rel_aux:
419   "\<lbrakk>\<forall>xa ya. R xa ya \<longrightarrow> x xa = y ya; Bex1_rel R x\<rbrakk> \<Longrightarrow> Bex1_rel R y"
420   unfolding Bex1_rel_def
421   apply (erule conjE)+
422   apply (erule bexE)
423   apply rule
424   apply (rule_tac x="xa" in bexI)
425   apply metis
426   apply metis
427   apply rule+
428   apply (erule_tac x="xaa" in ballE)
429   prefer 2
430   apply (metis)
431   apply (erule_tac x="ya" in ballE)
432   prefer 2
433   apply (metis)
434   apply (metis in_respects)
435   done
437 lemma bex1_rel_aux2:
438   "\<lbrakk>\<forall>xa ya. R xa ya \<longrightarrow> x xa = y ya; Bex1_rel R y\<rbrakk> \<Longrightarrow> Bex1_rel R x"
439   unfolding Bex1_rel_def
440   apply (erule conjE)+
441   apply (erule bexE)
442   apply rule
443   apply (rule_tac x="xa" in bexI)
444   apply metis
445   apply metis
446   apply rule+
447   apply (erule_tac x="xaa" in ballE)
448   prefer 2
449   apply (metis)
450   apply (erule_tac x="ya" in ballE)
451   prefer 2
452   apply (metis)
453   apply (metis in_respects)
454   done
456 lemma bex1_rel_rsp:
457   assumes a: "Quotient R absf repf"
458   shows "((R ===> op =) ===> op =) (Bex1_rel R) (Bex1_rel R)"
459   apply (simp add: fun_rel_def)
460   apply clarify
461   apply rule
462   apply (simp_all add: bex1_rel_aux bex1_rel_aux2)
463   apply (erule bex1_rel_aux2)
464   apply assumption
465   done
468 lemma ex1_prs:
469   assumes a: "Quotient R absf repf"
470   shows "((absf ---> id) ---> id) (Bex1_rel R) f = Ex1 f"
471 apply (simp add:)
472 apply (subst Bex1_rel_def)
473 apply (subst Bex_def)
474 apply (subst Ex1_def)
475 apply simp
476 apply rule
477  apply (erule conjE)+
478  apply (erule_tac exE)
479  apply (erule conjE)
480  apply (subgoal_tac "\<forall>y. R y y \<longrightarrow> f (absf y) \<longrightarrow> R x y")
481   apply (rule_tac x="absf x" in exI)
482   apply (simp)
483   apply rule+
484   using a unfolding Quotient_def
485   apply metis
486  apply rule+
487  apply (erule_tac x="x" in ballE)
488   apply (erule_tac x="y" in ballE)
489    apply simp
490   apply (simp add: in_respects)
491  apply (simp add: in_respects)
492 apply (erule_tac exE)
493  apply rule
494  apply (rule_tac x="repf x" in exI)
495  apply (simp only: in_respects)
496   apply rule
497  apply (metis Quotient_rel_rep[OF a])
498 using a unfolding Quotient_def apply (simp)
499 apply rule+
500 using a unfolding Quotient_def in_respects
501 apply metis
502 done
504 lemma bex1_bexeq_reg:
505   shows "(\<exists>!x\<in>Respects R. P x) \<longrightarrow> (Bex1_rel R (\<lambda>x. P x))"
506   apply (simp add: Ex1_def Bex1_rel_def in_respects)
507   apply clarify
508   apply auto
509   apply (rule bexI)
510   apply assumption
511   apply (simp add: in_respects)
512   apply (simp add: in_respects)
513   apply auto
514   done
516 lemma bex1_bexeq_reg_eqv:
517   assumes a: "equivp R"
518   shows "(\<exists>!x. P x) \<longrightarrow> Bex1_rel R P"
519   using equivp_reflp[OF a]
520   apply (intro impI)
521   apply (elim ex1E)
522   apply (rule mp[OF bex1_bexeq_reg])
523   apply (rule_tac a="x" in ex1I)
524   apply (subst in_respects)
525   apply (rule conjI)
526   apply assumption
527   apply assumption
528   apply clarify
529   apply (erule_tac x="xa" in allE)
530   apply simp
531   done
533 subsection {* Various respects and preserve lemmas *}
535 lemma quot_rel_rsp:
536   assumes a: "Quotient R Abs Rep"
537   shows "(R ===> R ===> op =) R R"
538   apply(rule fun_relI)+
539   apply(rule equals_rsp[OF a])
540   apply(assumption)+
541   done
543 lemma o_prs:
544   assumes q1: "Quotient R1 Abs1 Rep1"
545   and     q2: "Quotient R2 Abs2 Rep2"
546   and     q3: "Quotient R3 Abs3 Rep3"
547   shows "((Abs2 ---> Rep3) ---> (Abs1 ---> Rep2) ---> (Rep1 ---> Abs3)) op \<circ> = op \<circ>"
548   and   "(id ---> (Abs1 ---> id) ---> Rep1 ---> id) op \<circ> = op \<circ>"
549   using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] Quotient_abs_rep[OF q3]
550   by (simp_all add: fun_eq_iff)
552 lemma o_rsp:
553   "((R2 ===> R3) ===> (R1 ===> R2) ===> (R1 ===> R3)) op \<circ> op \<circ>"
554   "(op = ===> (R1 ===> op =) ===> R1 ===> op =) op \<circ> op \<circ>"
555   by (auto intro!: fun_relI elim: fun_relE)
557 lemma cond_prs:
558   assumes a: "Quotient R absf repf"
559   shows "absf (if a then repf b else repf c) = (if a then b else c)"
560   using a unfolding Quotient_def by auto
562 lemma if_prs:
563   assumes q: "Quotient R Abs Rep"
564   shows "(id ---> Rep ---> Rep ---> Abs) If = If"
565   using Quotient_abs_rep[OF q]
566   by (auto simp add: fun_eq_iff)
568 lemma if_rsp:
569   assumes q: "Quotient R Abs Rep"
570   shows "(op = ===> R ===> R ===> R) If If"
571   by (auto intro!: fun_relI)
573 lemma let_prs:
574   assumes q1: "Quotient R1 Abs1 Rep1"
575   and     q2: "Quotient R2 Abs2 Rep2"
576   shows "(Rep2 ---> (Abs2 ---> Rep1) ---> Abs1) Let = Let"
577   using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
578   by (auto simp add: fun_eq_iff)
580 lemma let_rsp:
581   shows "(R1 ===> (R1 ===> R2) ===> R2) Let Let"
582   by (auto intro!: fun_relI elim: fun_relE)
584 lemma mem_rsp:
585   shows "(R1 ===> (R1 ===> R2) ===> R2) op \<in> op \<in>"
586   by (auto intro!: fun_relI elim: fun_relE simp add: mem_def)
588 lemma mem_prs:
589   assumes a1: "Quotient R1 Abs1 Rep1"
590   and     a2: "Quotient R2 Abs2 Rep2"
591   shows "(Rep1 ---> (Abs1 ---> Rep2) ---> Abs2) op \<in> = op \<in>"
592   by (simp add: fun_eq_iff mem_def Quotient_abs_rep[OF a1] Quotient_abs_rep[OF a2])
594 lemma id_rsp:
595   shows "(R ===> R) id id"
596   by (auto intro: fun_relI)
598 lemma id_prs:
599   assumes a: "Quotient R Abs Rep"
600   shows "(Rep ---> Abs) id = id"
601   by (simp add: fun_eq_iff Quotient_abs_rep [OF a])
604 locale quot_type =
605   fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
606   and   Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
607   and   Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)"
608   assumes equivp: "part_equivp R"
609   and     rep_prop: "\<And>y. \<exists>x. R x x \<and> Rep y = R x"
610   and     rep_inverse: "\<And>x. Abs (Rep x) = x"
611   and     abs_inverse: "\<And>c. (\<exists>x. ((R x x) \<and> (c = R x))) \<Longrightarrow> (Rep (Abs c)) = c"
612   and     rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)"
613 begin
615 definition
616   abs :: "'a \<Rightarrow> 'b"
617 where
618   "abs x = Abs (R x)"
620 definition
621   rep :: "'b \<Rightarrow> 'a"
622 where
623   "rep a = Eps (Rep a)"
625 lemma homeier5:
626   assumes a: "R r r"
627   shows "Rep (Abs (R r)) = R r"
628   apply (subst abs_inverse)
629   using a by auto
631 theorem homeier6:
632   assumes a: "R r r"
633   and b: "R s s"
634   shows "Abs (R r) = Abs (R s) \<longleftrightarrow> R r = R s"
635   by (metis a b homeier5)
637 theorem homeier8:
638   assumes "R r r"
639   shows "R (Eps (R r)) = R r"
640   using assms equivp[simplified part_equivp_def]
641   apply clarify
642   by (metis assms exE_some)
644 lemma Quotient:
645   shows "Quotient R abs rep"
646   unfolding Quotient_def abs_def rep_def
647   proof (intro conjI allI)
648     fix a r s
649     show "Abs (R (Eps (Rep a))) = a"
650       using [[metis_new_skolemizer = false]]
651       by (metis equivp exE_some part_equivp_def rep_inverse rep_prop)
652     show "R r s \<longleftrightarrow> R r r \<and> R s s \<and> (Abs (R r) = Abs (R s))"
653       by (metis homeier6 equivp[simplified part_equivp_def])
654     show "R (Eps (Rep a)) (Eps (Rep a))" proof -
655       obtain x where r: "R x x" and rep: "Rep a = R x" using rep_prop[of a] by auto
656       have "R (Eps (R x)) x" using homeier8 r by simp
657       then have "R x (Eps (R x))" using part_equivp_symp[OF equivp] by fast
658       then have "R (Eps (R x)) (Eps (R x))" using homeier8[OF r] by simp
659       then show "R (Eps (Rep a)) (Eps (Rep a))" using rep by simp
660     qed
661   qed
663 end
666 subsection {* ML setup *}
668 text {* Auxiliary data for the quotient package *}
670 use "Tools/Quotient/quotient_info.ML"
671 setup Quotient_Info.setup
673 declare [[map "fun" = (map_fun, fun_rel)]]
675 lemmas [quot_thm] = fun_quotient
676 lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp mem_rsp id_rsp
677 lemmas [quot_preserve] = if_prs o_prs let_prs mem_prs id_prs
678 lemmas [quot_equiv] = identity_equivp
681 text {* Lemmas about simplifying id's. *}
682 lemmas [id_simps] =
683   id_def[symmetric]
684   map_fun_id
685   id_apply
686   id_o
687   o_id
688   eq_comp_r
690 text {* Translation functions for the lifting process. *}
691 use "Tools/Quotient/quotient_term.ML"
694 text {* Definitions of the quotient types. *}
695 use "Tools/Quotient/quotient_typ.ML"
698 text {* Definitions for quotient constants. *}
699 use "Tools/Quotient/quotient_def.ML"
702 text {*
703   An auxiliary constant for recording some information
704   about the lifted theorem in a tactic.
705 *}
706 definition
707   Quot_True :: "'a \<Rightarrow> bool"
708 where
709   "Quot_True x \<longleftrightarrow> True"
711 lemma
712   shows QT_all: "Quot_True (All P) \<Longrightarrow> Quot_True P"
713   and   QT_ex:  "Quot_True (Ex P) \<Longrightarrow> Quot_True P"
714   and   QT_ex1: "Quot_True (Ex1 P) \<Longrightarrow> Quot_True P"
715   and   QT_lam: "Quot_True (\<lambda>x. P x) \<Longrightarrow> (\<And>x. Quot_True (P x))"
716   and   QT_ext: "(\<And>x. Quot_True (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (Quot_True a \<Longrightarrow> f = g)"
717   by (simp_all add: Quot_True_def ext)
719 lemma QT_imp: "Quot_True a \<equiv> Quot_True b"
720   by (simp add: Quot_True_def)
723 text {* Tactics for proving the lifted theorems *}
724 use "Tools/Quotient/quotient_tacs.ML"
726 subsection {* Methods / Interface *}
728 method_setup lifting =
729   {* Attrib.thms >> (fn thms => fn ctxt =>
730        SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_tac ctxt [] thms))) *}
731   {* lift theorems to quotient types *}
733 method_setup lifting_setup =
734   {* Attrib.thm >> (fn thm => fn ctxt =>
735        SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_procedure_tac ctxt [] thm))) *}
736   {* set up the three goals for the quotient lifting procedure *}
738 method_setup descending =
739   {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.descend_tac ctxt []))) *}
740   {* decend theorems to the raw level *}
742 method_setup descending_setup =
743   {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.descend_procedure_tac ctxt []))) *}
744   {* set up the three goals for the decending theorems *}
746 method_setup regularize =
747   {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.regularize_tac ctxt))) *}
748   {* prove the regularization goals from the quotient lifting procedure *}
750 method_setup injection =
751   {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.all_injection_tac ctxt))) *}
752   {* prove the rep/abs injection goals from the quotient lifting procedure *}
754 method_setup cleaning =
755   {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.clean_tac ctxt))) *}
756   {* prove the cleaning goals from the quotient lifting procedure *}
758 attribute_setup quot_lifted =
759   {* Scan.succeed Quotient_Tacs.lifted_attrib *}
760   {* lift theorems to quotient types *}
762 no_notation
763   rel_conj (infixr "OOO" 75) and
764   map_fun (infixr "--->" 55) and
765   fun_rel (infixr "===>" 55)
767 end