# HG changeset patch # User wenzelm # Date 1723129568 -7200 # Node ID 32073335a8e99db070f599b9ef645b54dc5b5175 # Parent e9beaa28645dfbae431eecba48823515eeea346f tuned proofs; diff -r e9beaa28645d -r 32073335a8e9 src/HOL/Quotient.thy --- a/src/HOL/Quotient.thy Thu Aug 08 16:23:30 2024 +0200 +++ b/src/HOL/Quotient.thy Thu Aug 08 17:06:08 2024 +0200 @@ -268,11 +268,9 @@ assumes a: "equivp R2" shows "(Bex (Respects (R1 ===> R2)) (\f. P (f x)) = Ex (\f. P (f x)))" proof - - { fix f - assume "P (f x)" - have "(\y. f x) \ Respects (R1 ===> R2)" - using a equivp_reflp_symp_transp[of "R2"] - by (auto simp add: Respects_def in_respects rel_fun_def elim: equivpE reflpE) } + have "(\y. f x) \ Respects (R1 ===> R2)" for f + using a equivp_reflp_symp_transp[of "R2"] + by (auto simp add: Respects_def in_respects rel_fun_def elim: equivpE reflpE) then show ?thesis by auto qed @@ -338,12 +336,13 @@ and q2: "Quotient3 R2 Abs2 Rep2" shows "((Rep1 ---> Abs2) (Babs (Respects R1) ((Abs1 ---> Rep2) f))) = f" proof - - { fix x + have "Abs2 (Babs (Respects R1) ((Abs1 ---> Rep2) f) (Rep1 x)) = f x" for x + proof - have "Rep1 x \ Respects R1" by (simp add: in_respects Quotient3_rel_rep[OF q1]) - then have "Abs2 (Babs (Respects R1) ((Abs1 ---> Rep2) f) (Rep1 x)) = f x" + then show ?thesis by (simp add: Babs_def Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2]) - } + qed then show ?thesis by force qed @@ -422,8 +421,7 @@ shows "((absf ---> id) ---> id) (Bex1_rel R) f = Ex1 f" (is "?lhs = ?rhs") using assms - apply (auto simp add: Bex1_rel_def Respects_def) - by (metis (full_types) Quotient3_def)+ + by (auto simp add: Bex1_rel_def Respects_def) (metis (full_types) Quotient3_def)+ lemma bex1_bexeq_reg: shows "(\!x\Respects R. P x) \ (Bex1_rel R (\x. P x))" @@ -440,8 +438,7 @@ lemma quot_rel_rsp: assumes a: "Quotient3 R Abs Rep" shows "(R ===> R ===> (=)) R R" - apply(rule rel_funI)+ - by (meson assms equals_rsp) + by (rule rel_funI)+ (meson assms equals_rsp) lemma o_prs: assumes q1: "Quotient3 R1 Abs1 Rep1" @@ -519,35 +516,33 @@ lemma some_collect: assumes "R r r" shows "R (SOME x. x \ Collect (R r)) = R r" - apply simp - by (metis assms exE_some equivp[simplified part_equivp_def]) + by simp (metis assms exE_some equivp[simplified part_equivp_def]) -lemma Quotient: - shows "Quotient3 R abs rep" +lemma Quotient: "Quotient3 R abs rep" unfolding Quotient3_def abs_def rep_def - proof (intro conjI allI) - fix a r s - show x: "R (SOME x. x \ Rep a) (SOME x. x \ Rep a)" proof - - obtain x where r: "R x x" and rep: "Rep a = Collect (R x)" using rep_prop[of a] by auto - have "R (SOME x. x \ Rep a) x" using r rep some_collect by metis - then have "R x (SOME x. x \ Rep a)" using part_equivp_symp[OF equivp] by fast - then show "R (SOME x. x \ Rep a) (SOME x. x \ Rep a)" - using part_equivp_transp[OF equivp] by (metis \R (SOME x. x \ Rep a) x\) - qed - have "Collect (R (SOME x. x \ Rep a)) = (Rep a)" by (metis some_collect rep_prop) - then show "Abs (Collect (R (SOME x. x \ Rep a))) = a" using rep_inverse by auto - have "R r r \ R s s \ Abs (Collect (R r)) = Abs (Collect (R s)) \ R r = R s" - proof - - assume "R r r" and "R s s" - then have "Abs (Collect (R r)) = Abs (Collect (R s)) \ Collect (R r) = Collect (R s)" - by (metis abs_inverse) - also have "Collect (R r) = Collect (R s) \ (\A x. x \ A) (Collect (R r)) = (\A x. x \ A) (Collect (R s))" - by (rule iffI) simp_all - finally show "Abs (Collect (R r)) = Abs (Collect (R s)) \ R r = R s" by simp - qed - then show "R r s \ R r r \ R s s \ (Abs (Collect (R r)) = Abs (Collect (R s)))" - using equivp[simplified part_equivp_def] by metis - qed +proof (intro conjI allI) + fix a r s + show x: "R (SOME x. x \ Rep a) (SOME x. x \ Rep a)" proof - + obtain x where r: "R x x" and rep: "Rep a = Collect (R x)" using rep_prop[of a] by auto + have "R (SOME x. x \ Rep a) x" using r rep some_collect by metis + then have "R x (SOME x. x \ Rep a)" using part_equivp_symp[OF equivp] by fast + then show "R (SOME x. x \ Rep a) (SOME x. x \ Rep a)" + using part_equivp_transp[OF equivp] by (metis \R (SOME x. x \ Rep a) x\) + qed + have "Collect (R (SOME x. x \ Rep a)) = (Rep a)" by (metis some_collect rep_prop) + then show "Abs (Collect (R (SOME x. x \ Rep a))) = a" using rep_inverse by auto + have "R r r \ R s s \ Abs (Collect (R r)) = Abs (Collect (R s)) \ R r = R s" + proof - + assume "R r r" and "R s s" + then have "Abs (Collect (R r)) = Abs (Collect (R s)) \ Collect (R r) = Collect (R s)" + by (metis abs_inverse) + also have "Collect (R r) = Collect (R s) \ (\A x. x \ A) (Collect (R r)) = (\A x. x \ A) (Collect (R s))" + by (rule iffI) simp_all + finally show "Abs (Collect (R r)) = Abs (Collect (R s)) \ R r = R s" by simp + qed + then show "R r s \ R r r \ R s s \ (Abs (Collect (R r)) = Abs (Collect (R s)))" + using equivp[simplified part_equivp_def] by metis +qed end @@ -576,9 +571,8 @@ using r Quotient3_refl1 R1 rep_abs_rsp by fastforce moreover have "R2' (Rep1 (Abs1 r)) (Rep1 (Abs1 s))" using that - apply simp - apply (metis (full_types) Rep1 Abs1 Quotient3_rel R2 Quotient3_refl1 [OF R1] Quotient3_refl2 [OF R1] Quotient3_rel_abs [OF R1]) - done + by simp (metis (full_types) Rep1 Abs1 Quotient3_rel R2 Quotient3_refl1 [OF R1] + Quotient3_refl2 [OF R1] Quotient3_rel_abs [OF R1]) moreover have "R1 (Rep1 (Abs1 s)) s" by (metis s Quotient3_rel R1 rep_abs_rsp_left) ultimately show ?thesis @@ -616,27 +610,25 @@ subsection \Quotient3 to Quotient\ lemma Quotient3_to_Quotient: -assumes "Quotient3 R Abs Rep" -and "T \ \x y. R x x \ Abs x = y" -shows "Quotient R Abs Rep T" -using assms unfolding Quotient3_def by (intro QuotientI) blast+ + assumes "Quotient3 R Abs Rep" + and "T \ \x y. R x x \ Abs x = y" + shows "Quotient R Abs Rep T" + using assms unfolding Quotient3_def by (intro QuotientI) blast+ lemma Quotient3_to_Quotient_equivp: -assumes q: "Quotient3 R Abs Rep" -and T_def: "T \ \x y. Abs x = y" -and eR: "equivp R" -shows "Quotient R Abs Rep T" + assumes q: "Quotient3 R Abs Rep" + and T_def: "T \ \x y. Abs x = y" + and eR: "equivp R" + shows "Quotient R Abs Rep T" proof (intro QuotientI) - fix a - show "Abs (Rep a) = a" using q by(rule Quotient3_abs_rep) -next - fix a - show "R (Rep a) (Rep a)" using q by(rule Quotient3_rep_reflp) -next - fix r s - show "R r s = (R r r \ R s s \ Abs r = Abs s)" using q by(rule Quotient3_rel[symmetric]) -next - show "T = (\x y. R x x \ Abs x = y)" using T_def equivp_reflp[OF eR] by simp + show "Abs (Rep a) = a" for a + using q by(rule Quotient3_abs_rep) + show "R (Rep a) (Rep a)" for a + using q by(rule Quotient3_rep_reflp) + show "R r s = (R r r \ R s s \ Abs r = Abs s)" for r s + using q by(rule Quotient3_rel[symmetric]) + show "T = (\x y. R x x \ Abs x = y)" + using T_def equivp_reflp[OF eR] by simp qed subsection \ML setup\