# HG changeset patch # User paulson # Date 1531347865 -3600 # Node ID cedf3480fdadd252f1750e834438716b8784a73d # Parent 3ed4ff0b7ac4b1a3618b3b2f07a50555f8dafbde de-applying (mostly Quotient) diff -r 3ed4ff0b7ac4 -r cedf3480fdad src/HOL/Analysis/Infinite_Products.thy --- a/src/HOL/Analysis/Infinite_Products.thy Wed Jul 11 19:19:00 2018 +0100 +++ b/src/HOL/Analysis/Infinite_Products.thy Wed Jul 11 23:24:25 2018 +0100 @@ -1762,6 +1762,12 @@ by (simp add: add_eq_0_iff convergent_prod_iff_summable_complex) qed +lemma summable_Ln_complex: + fixes z :: "nat \ complex" + assumes "convergent_prod z" "\k. z k \ 0" + shows "summable (\k. Ln (z k))" + using convergent_prod_def assms convergent_prod_iff_summable_complex by blast + subsection\Embeddings from the reals into some complete real normed field\ diff -r 3ed4ff0b7ac4 -r cedf3480fdad src/HOL/Quotient.thy --- a/src/HOL/Quotient.thy Wed Jul 11 19:19:00 2018 +0100 +++ b/src/HOL/Quotient.thy Wed Jul 11 23:24:25 2018 +0100 @@ -410,63 +410,23 @@ shows "((R ===> (=)) ===> (=)) (Bex1_rel R) (Bex1_rel R)" unfolding rel_fun_def by (metis bex1_rel_aux bex1_rel_aux2) - lemma ex1_prs: - assumes a: "Quotient3 R absf repf" + assumes "Quotient3 R absf repf" shows "((absf ---> id) ---> id) (Bex1_rel R) f = Ex1 f" -apply (simp add:) -apply (subst Bex1_rel_def) -apply (subst Bex_def) -apply (subst Ex1_def) -apply simp -apply rule - apply (erule conjE)+ - apply (erule_tac exE) - apply (erule conjE) - apply (subgoal_tac "\y. R y y \ f (absf y) \ R x y") - apply (rule_tac x="absf x" in exI) - apply (simp) - apply rule+ - using a unfolding Quotient3_def - apply metis - apply rule+ - apply (erule_tac x="x" in ballE) - apply (erule_tac x="y" in ballE) - apply simp - apply (simp add: in_respects) - apply (simp add: in_respects) -apply (erule_tac exE) - apply rule - apply (rule_tac x="repf x" in exI) - apply (simp only: in_respects) - apply rule - apply (metis Quotient3_rel_rep[OF a]) -using a unfolding Quotient3_def apply (simp) -apply rule+ -using a unfolding Quotient3_def in_respects -apply metis -done + apply (auto simp: Bex1_rel_def Respects_def) + apply (metis Quotient3_def assms) + apply (metis (full_types) Quotient3_def assms) + by (meson Quotient3_rel assms) lemma bex1_bexeq_reg: shows "(\!x\Respects R. P x) \ (Bex1_rel R (\x. P x))" by (auto simp add: Ex1_def Bex1_rel_def Bex_def Ball_def in_respects) - + lemma bex1_bexeq_reg_eqv: assumes a: "equivp R" shows "(\!x. P x) \ Bex1_rel R P" using equivp_reflp[OF a] - apply (intro impI) - apply (elim ex1E) - apply (rule mp[OF bex1_bexeq_reg]) - apply (rule_tac a="x" in ex1I) - apply (subst in_respects) - apply (rule conjI) - apply assumption - apply assumption - apply clarify - apply (erule_tac x="xa" in allE) - apply simp - done + by (metis (full_types) Bex1_rel_def in_respects) subsection \Various respects and preserve lemmas\ @@ -474,9 +434,7 @@ assumes a: "Quotient3 R Abs Rep" shows "(R ===> R ===> (=)) R R" apply(rule rel_funI)+ - apply(rule equals_rsp[OF a]) - apply(assumption)+ - done + by (meson assms equals_rsp) lemma o_prs: assumes q1: "Quotient3 R1 Abs1 Rep1" @@ -588,6 +546,7 @@ subsection \Quotient composition\ + lemma OOO_quotient3: fixes R1 :: "'a \ 'a \ bool" fixes Abs1 :: "'a \ 'b" and Rep1 :: "'b \ 'a" @@ -599,76 +558,38 @@ assumes Abs1: "\x y. R2' x y \ R1 x x \ R1 y y \ R2 (Abs1 x) (Abs1 y)" assumes Rep1: "\x y. R2 x y \ R2' (Rep1 x) (Rep1 y)" shows "Quotient3 (R1 OO R2' OO R1) (Abs2 \ Abs1) (Rep1 \ Rep2)" -apply (rule Quotient3I) - apply (simp add: o_def Quotient3_abs_rep [OF R2] Quotient3_abs_rep [OF R1]) - apply simp - apply (rule_tac b="Rep1 (Rep2 a)" in relcomppI) - apply (rule Quotient3_rep_reflp [OF R1]) - apply (rule_tac b="Rep1 (Rep2 a)" in relcomppI [rotated]) - apply (rule Quotient3_rep_reflp [OF R1]) - apply (rule Rep1) - apply (rule Quotient3_rep_reflp [OF R2]) - apply safe - apply (rename_tac x y) - apply (drule Abs1) - apply (erule Quotient3_refl2 [OF R1]) - apply (erule Quotient3_refl1 [OF R1]) - apply (drule Quotient3_refl1 [OF R2], drule Rep1) - apply (subgoal_tac "R1 r (Rep1 (Abs1 x))") - apply (rule_tac b="Rep1 (Abs1 x)" in relcomppI, assumption) - apply (erule relcomppI) - apply (erule Quotient3_symp [OF R1, THEN sympD]) - apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2]) - apply (rule conjI, erule Quotient3_refl1 [OF R1]) - apply (rule conjI, rule Quotient3_rep_reflp [OF R1]) - apply (subst Quotient3_abs_rep [OF R1]) - apply (erule Quotient3_rel_abs [OF R1]) - apply (rename_tac x y) - apply (drule Abs1) - apply (erule Quotient3_refl2 [OF R1]) - apply (erule Quotient3_refl1 [OF R1]) - apply (drule Quotient3_refl2 [OF R2], drule Rep1) - apply (subgoal_tac "R1 s (Rep1 (Abs1 y))") - apply (rule_tac b="Rep1 (Abs1 y)" in relcomppI, assumption) - apply (erule relcomppI) - apply (erule Quotient3_symp [OF R1, THEN sympD]) - apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2]) - apply (rule conjI, erule Quotient3_refl2 [OF R1]) - apply (rule conjI, rule Quotient3_rep_reflp [OF R1]) - apply (subst Quotient3_abs_rep [OF R1]) - apply (erule Quotient3_rel_abs [OF R1, THEN sym]) - apply simp - apply (rule Quotient3_rel_abs [OF R2]) - apply (rule Quotient3_rel_abs [OF R1, THEN ssubst], assumption) - apply (rule Quotient3_rel_abs [OF R1, THEN subst], assumption) - apply (erule Abs1) - apply (erule Quotient3_refl2 [OF R1]) - apply (erule Quotient3_refl1 [OF R1]) - apply (rename_tac a b c d) - apply simp - apply (rule_tac b="Rep1 (Abs1 r)" in relcomppI) - apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2]) - apply (rule conjI, erule Quotient3_refl1 [OF R1]) - apply (simp add: Quotient3_abs_rep [OF R1] Quotient3_rep_reflp [OF R1]) - apply (rule_tac b="Rep1 (Abs1 s)" in relcomppI [rotated]) - apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2]) - apply (simp add: Quotient3_abs_rep [OF R1] Quotient3_rep_reflp [OF R1]) - apply (erule Quotient3_refl2 [OF R1]) - apply (rule Rep1) - apply (drule Abs1) - apply (erule Quotient3_refl2 [OF R1]) - apply (erule Quotient3_refl1 [OF R1]) - apply (drule Abs1) - apply (erule Quotient3_refl2 [OF R1]) - apply (erule Quotient3_refl1 [OF R1]) - apply (drule Quotient3_rel_abs [OF R1]) - apply (drule Quotient3_rel_abs [OF R1]) - apply (drule Quotient3_rel_abs [OF R1]) - apply (drule Quotient3_rel_abs [OF R1]) - apply simp - apply (rule Quotient3_rel[symmetric, OF R2, THEN iffD2]) - apply simp -done +proof - + have *: "(R1 OOO R2') r r \ (R1 OOO R2') s s \ (Abs2 \ Abs1) r = (Abs2 \ Abs1) s + \ (R1 OOO R2') r s" for r s + apply safe + subgoal for a b c d + apply simp + apply (rule_tac b="Rep1 (Abs1 r)" in relcomppI) + using Quotient3_refl1 R1 rep_abs_rsp apply fastforce + apply (rule_tac b="Rep1 (Abs1 s)" in relcomppI) + apply (metis (full_types) Rep1 Abs1 Quotient3_rel R2 Quotient3_refl1 [OF R1] Quotient3_refl2 [OF R1] Quotient3_rel_abs [OF R1]) + by (metis Quotient3_rel R1 rep_abs_rsp_left) + subgoal for x y + apply (drule Abs1) + apply (erule Quotient3_refl2 [OF R1]) + apply (erule Quotient3_refl1 [OF R1]) + apply (drule Quotient3_refl1 [OF R2], drule Rep1) + by (metis (full_types) Quotient3_def R1 relcompp.relcompI) + subgoal for x y + apply (drule Abs1) + apply (erule Quotient3_refl2 [OF R1]) + apply (erule Quotient3_refl1 [OF R1]) + apply (drule Quotient3_refl2 [OF R2], drule Rep1) + by (metis (full_types) Quotient3_def R1 relcompp.relcompI) + subgoal for x y + by simp (metis (full_types) Abs1 Quotient3_rel R1 R2) + done + show ?thesis + apply (rule Quotient3I) + using * apply (simp_all add: o_def Quotient3_abs_rep [OF R2] Quotient3_abs_rep [OF R1]) + apply (metis Quotient3_rep_reflp R1 R2 Rep1 relcompp.relcompI) + done +qed lemma OOO_eq_quotient3: fixes R1 :: "'a \ 'a \ bool"