# HG changeset patch # User Fabian Huch # Date 1658493596 -7200 # Node ID 43f5dfb7fa35b9f301072c8f3d844daab7a7a096 # Parent b87b14e885af5876fe80ee398e80a2448deff0be tuned (some HOL lints, by Yecine Megdiche); diff -r b87b14e885af -r 43f5dfb7fa35 src/HOL/BNF_Wellorder_Constructions.thy --- a/src/HOL/BNF_Wellorder_Constructions.thy Fri Jul 15 09:18:21 2022 +0200 +++ b/src/HOL/BNF_Wellorder_Constructions.thy Fri Jul 22 14:39:56 2022 +0200 @@ -106,12 +106,22 @@ lemma ofilter_Restr_under: assumes WELL: "Well_order r" and OF: "wo_rel.ofilter r A" and IN: "a \ A" shows "under (Restr r A) a = under r a" -using assms wo_rel_def -proof(auto simp add: wo_rel.ofilter_def under_def) - fix b assume *: "a \ A" and "(b,a) \ r" - hence "b \ under r a \ a \ Field r" - unfolding under_def using Field_def by fastforce - thus "b \ A" using * assms by (auto simp add: wo_rel_def wo_rel.ofilter_def) + unfolding wo_rel.ofilter_def under_def +proof + show "{b. (b, a) \ Restr r A} \ {b. (b, a) \ r}" + by auto +next + have "under r a \ A" + proof + fix x + assume *: "x \ under r a" + then have "a \ Field r" + unfolding under_def using Field_def by fastforce + then show "x \ A" using IN assms * + by (auto simp add: wo_rel_def wo_rel.ofilter_def) + qed + then show "{b. (b, a) \ r} \ {b. (b, a) \ Restr r A}" + unfolding under_def using assms by auto qed lemma ofilter_embed: @@ -120,12 +130,13 @@ proof assume *: "wo_rel.ofilter r A" show "A \ Field r \ embed (Restr r A) r id" - proof(unfold embed_def, auto) + unfolding embed_def + proof safe fix a assume "a \ A" thus "a \ Field r" using assms * by (auto simp add: wo_rel_def wo_rel.ofilter_def) next fix a assume "a \ Field (Restr r A)" - thus "bij_betw id (under (Restr r A) a) (under r a)" using assms * + thus "bij_betw id (under (Restr r A) a) (under r (id a))" using assms * by (simp add: ofilter_Restr_under Field_Restr_ofilter) qed next @@ -160,7 +171,8 @@ by (simp add: Well_order_Restr wo_rel_def) (* Main proof *) show ?thesis using WellB assms - proof(auto simp add: wo_rel.ofilter_def under_def) + unfolding wo_rel.ofilter_def under_def ofilter_def + proof safe fix a assume "a \ A" and *: "a \ B" hence "a \ Field r" using OFA Well by (auto simp add: wo_rel.ofilter_def) with * show "a \ Field ?rB" using Field by auto @@ -714,7 +726,7 @@ lemma ordLess_iff_ordIso_Restr: assumes WELL: "Well_order r" and WELL': "Well_order r'" shows "(r' a \ Field r. r' =o Restr r (underS r a))" -proof(auto) +proof safe fix a assume *: "a \ Field r" and **: "r' =o Restr r (underS r a)" hence "Restr r (underS r a) o r') = (\a \ Field r. Restr r (underS r a) o r'" fix a assume "a \ Field r" hence "Restr r (underS r a) dir_image r f" "(b',c') \ dir_image r f" then obtain a b1 b2 c where 1: "a' = f a \ b' = f b1 \ b' = f b2 \ c' = f c" and @@ -953,7 +966,8 @@ lemma antisym_dir_image: assumes AN: "antisym r" and INJ: "inj_on f (Field r)" shows "antisym(dir_image r f)" -proof(unfold antisym_def, auto) +unfolding antisym_def +proof safe fix a' b' assume "(a',b') \ dir_image r f" "(b',a') \ dir_image r f" then obtain a1 b1 a2 b2 where 1: "a' = f a1 \ a' = f a2 \ b' = f b1 \ b' = f b2" and @@ -1096,7 +1110,7 @@ qed next show "Field r \ Field r \ Field (bsqr r)" - proof(auto) + proof safe fix a1 a2 assume "a1 \ Field r" and "a2 \ Field r" hence "((a1,a2),(a1,a2)) \ bsqr r" unfolding bsqr_def by blast thus "(a1,a2) \ Field (bsqr r)" unfolding Field_def by auto @@ -1109,7 +1123,8 @@ lemma bsqr_Trans: assumes "Well_order r" shows "trans (bsqr r)" -proof(unfold trans_def, auto) +unfolding trans_def +proof safe (* Preliminary facts *) have Well: "wo_rel r" using assms wo_rel_def by auto hence Trans: "trans r" using wo_rel.TRANS by auto @@ -1573,12 +1588,11 @@ lemma bij_betw_curr: "bij_betw (curr A) (Func (A \ B) C) (Func A (Func B C))" -unfolding bij_betw_def inj_on_def image_def -apply (intro impI conjI ballI) -apply (erule curr_inj[THEN iffD1], assumption+) -apply auto -apply (erule curr_in) -using curr_surj by blast + unfolding bij_betw_def inj_on_def image_def + apply (intro impI conjI ballI) + apply (erule curr_inj[THEN iffD1], assumption+, safe) + using curr_surj curr_in apply blast+ + done definition Func_map where "Func_map B2 f1 f2 g b2 \ if b2 \ B2 then f1 (g (f2 b2)) else undefined" @@ -1661,7 +1675,7 @@ using j2A2 B1 A2 unfolding j1_def by (fast intro: inv_into_into)+ ultimately show "h \ Func_map B2 f1 f2 ` Func A2 A1" unfolding Func_map_def[abs_def] by auto - qed(insert B1 Func_map[OF _ _ A2(2)], auto) + qed(use B1 Func_map[OF _ _ A2(2)] in auto) qed end diff -r b87b14e885af -r 43f5dfb7fa35 src/HOL/BNF_Wellorder_Relation.thy --- a/src/HOL/BNF_Wellorder_Relation.thy Fri Jul 15 09:18:21 2022 +0200 +++ b/src/HOL/BNF_Wellorder_Relation.thy Fri Jul 22 14:39:56 2022 +0200 @@ -220,27 +220,26 @@ shows "\b. isMinim B b" proof- from spec[OF WF[unfolded wf_eq_minimal[of "r - Id"]], of B] NE obtain b where - *: "b \ B \ (\b'. b' \ b \ (b',b) \ r \ b' \ B)" by auto - show ?thesis - proof(simp add: isMinim_def, rule exI[of _ b], auto) - show "b \ B" using * by simp - next - fix b' assume As: "b' \ B" - hence **: "b \ Field r \ b' \ Field r" using As SUB * by auto - (* *) - from As * have "b' = b \ (b',b) \ r" by auto - moreover - {assume "b' = b" - hence "(b,b') \ r" - using ** REFL by (auto simp add: refl_on_def) - } - moreover - {assume "b' \ b \ (b',b) \ r" - hence "(b,b') \ r" - using ** TOTAL by (auto simp add: total_on_def) - } - ultimately show "(b,b') \ r" by blast + *: "b \ B \ (\b'. b' \ b \ (b',b) \ r \ b' \ B)" by auto + have "\b'. b' \ B \ (b, b') \ r" + proof + fix b' + show "b' \ B \ (b, b') \ r" + proof + assume As: "b' \ B" + hence **: "b \ Field r \ b' \ Field r" using As SUB * by auto + from As * have "b' = b \ (b',b) \ r" by auto + moreover have "b' = b \ (b, b') \ r" + using ** REFL by (auto simp add: refl_on_def) + moreover have "b' \ b \ (b',b) \ r \ (b,b') \ r" + using ** TOTAL by (auto simp add: total_on_def) + ultimately show "(b,b') \ r" by blast + qed qed + then have "isMinim B b" + unfolding isMinim_def using * by auto + then show ?thesis + by auto qed lemma minim_isMinim: @@ -395,16 +394,22 @@ lemma under_ofilter: "ofilter (under a)" -proof(unfold ofilter_def under_def, auto simp add: Field_def) - fix aa x - assume "(aa,a) \ r" "(x,aa) \ r" - thus "(x,a) \ r" - using TRANS trans_def[of r] by blast +proof - + have "\aa x. (aa, a) \ r \ (x, aa) \ r \ (x, a) \ r" + proof - + fix aa x + assume "(aa,a) \ r" "(x,aa) \ r" + then show "(x,a) \ r" + using TRANS trans_def[of r] by blast + qed + then show ?thesis unfolding ofilter_def under_def + by (auto simp add: Field_def) qed lemma underS_ofilter: "ofilter (underS a)" -proof(unfold ofilter_def underS_def under_def, auto simp add: Field_def) + unfolding ofilter_def underS_def under_def +proof safe fix aa assume "(a, aa) \ r" "(aa, a) \ r" and DIFF: "aa \ a" thus False using ANTISYM antisym_def[of r] by blast @@ -412,7 +417,13 @@ fix aa x assume "(aa,a) \ r" "aa \ a" "(x,aa) \ r" thus "(x,a) \ r" - using TRANS trans_def[of r] by blast + using TRANS trans_def[of r] by blast +next + fix x + assume "x \ a" and "(x, a) \ r" + then show "x \ Field r" + unfolding Field_def + by auto qed lemma Field_ofilter: @@ -430,7 +441,7 @@ let ?One = "(\a\Field r. A = underS a)" let ?Two = "(A = Field r)" show "?One \ ?Two" - proof(cases ?Two, simp) + proof(cases ?Two) let ?B = "(Field r) - A" let ?a = "minim ?B" assume "A \ Field r" @@ -445,7 +456,7 @@ have "A = underS ?a" proof show "A \ underS ?a" - proof(unfold underS_def, auto simp add: 4) + proof fix x assume **: "x \ A" hence 11: "x \ Field r" using 5 by auto have 12: "x \ ?a" using 4 ** by auto @@ -458,25 +469,32 @@ hence "?a \ A" using ** 13 by blast with 4 have False by simp } - thus "(x,?a) \ r" by blast + then have "(x,?a) \ r" by blast + thus "x \ underS ?a" + unfolding underS_def by (auto simp add: 12) qed next show "underS ?a \ A" - proof(unfold underS_def, auto) + proof fix x - assume **: "x \ ?a" and ***: "(x,?a) \ r" - hence 11: "x \ Field r" using Field_def by fastforce + assume **: "x \ underS ?a" + hence 11: "x \ Field r" + using Field_def unfolding underS_def by fastforce {assume "x \ A" hence "x \ ?B" using 11 by auto hence "(?a,x) \ r" using 3 minim_least[of ?B x] by blast hence False - using ANTISYM antisym_def[of r] ** *** by auto + using ANTISYM antisym_def[of r] ** unfolding underS_def by auto } thus "x \ A" by blast qed qed ultimately have ?One using 2 by blast thus ?thesis by simp + next + assume "A = Field r" + then show ?thesis + by simp qed qed diff -r b87b14e885af -r 43f5dfb7fa35 src/HOL/Complete_Lattices.thy --- a/src/HOL/Complete_Lattices.thy Fri Jul 15 09:18:21 2022 +0200 +++ b/src/HOL/Complete_Lattices.thy Fri Jul 22 14:39:56 2022 +0200 @@ -988,9 +988,9 @@ by blast lemma disjnt_inj_on_iff: - "\inj_on f (\\); X \ \; Y \ \\ \ disjnt (f ` X) (f ` Y) \ disjnt X Y" - apply (auto simp: disjnt_def) - using inj_on_eq_iff by fastforce + "\inj_on f (\\); X \ \; Y \ \\ \ disjnt (f ` X) (f ` Y) \ disjnt X Y" + unfolding disjnt_def + by safe (use inj_on_eq_iff in \fastforce+\) lemma disjnt_Union1 [simp]: "disjnt (\\) B \ (\A \ \. disjnt A B)" by (auto simp: disjnt_def) diff -r b87b14e885af -r 43f5dfb7fa35 src/HOL/Conditionally_Complete_Lattices.thy --- a/src/HOL/Conditionally_Complete_Lattices.thy Fri Jul 15 09:18:21 2022 +0200 +++ b/src/HOL/Conditionally_Complete_Lattices.thy Fri Jul 22 14:39:56 2022 +0200 @@ -522,31 +522,29 @@ assumes "a < b" and "P a" and "\ P b" shows "\c. a \ c \ c \ b \ (\x. a \ x \ x < c \ P x) \ (\d. (\x. a \ x \ x < d \ P x) \ d \ c)" -proof (rule exI [where x = "Sup {d. \x. a \ x \ x < d \ P x}"], auto) +proof (rule exI [where x = "Sup {d. \x. a \ x \ x < d \ P x}"], safe) show "a \ Sup {d. \c. a \ c \ c < d \ P c}" by (rule cSup_upper, auto simp: bdd_above_def) (metis \a < b\ \\ P b\ linear less_le) next show "Sup {d. \c. a \ c \ c < d \ P c} \ b" - apply (rule cSup_least) - apply auto - apply (metis less_le_not_le) - apply (metis \a \\ P b\ linear less_le) - done + by (rule cSup_least) + (use \a \\ P b\ in \auto simp add: less_le_not_le\) next fix x assume x: "a \ x" and lt: "x < Sup {d. \c. a \ c \ c < d \ P c}" show "P x" - apply (rule less_cSupE [OF lt], auto) - apply (metis less_le_not_le) - apply (metis x) - done + by (rule less_cSupE [OF lt]) (use less_le_not_le x in \auto\) next fix d - assume 0: "\x. a \ x \ x < d \ P x" - thus "d \ Sup {d. \c. a \ c \ c < d \ P c}" - by (rule_tac cSup_upper, auto simp: bdd_above_def) - (metis \a \\ P b\ linear less_le) + assume 0: "\x. a \ x \ x < d \ P x" + then have "d \ {d. \c. a \ c \ c < d \ P c}" + by auto + moreover have "bdd_above {d. \c. a \ c \ c < d \ P c}" + unfolding bdd_above_def using \a \\ P b\ linear + by (simp add: less_le) blast + ultimately show "d \ Sup {d. \c. a \ c \ c < d \ P c}" + by (auto simp: cSup_upper) qed end diff -r b87b14e885af -r 43f5dfb7fa35 src/HOL/Divides.thy --- a/src/HOL/Divides.thy Fri Jul 15 09:18:21 2022 +0200 +++ b/src/HOL/Divides.thy Fri Jul 22 14:39:56 2022 +0200 @@ -40,7 +40,7 @@ lemma unique_quotient_lemma_neg: "b * q' + r' \ b*q + r \ r \ 0 \ b < r \ b < r' \ q \ (q'::int)" - by (rule_tac b = "-b" and r = "-r'" and r' = "-r" in unique_quotient_lemma) auto + using unique_quotient_lemma[where b = "-b" and r = "-r'" and r'="-r"] by auto lemma unique_quotient: "eucl_rel_int a b (q, r) \ eucl_rel_int a b (q', r') \ q = q'" @@ -50,11 +50,15 @@ done lemma unique_remainder: - "eucl_rel_int a b (q, r) \ eucl_rel_int a b (q', r') \ r = r'" -apply (subgoal_tac "q = q'") - apply (simp add: eucl_rel_int_iff) -apply (blast intro: unique_quotient) -done + assumes "eucl_rel_int a b (q, r)" + and "eucl_rel_int a b (q', r')" + shows "r = r'" +proof - + have "q = q'" + using assms by (blast intro: unique_quotient) + then show "r = r'" + using assms by (simp add: eucl_rel_int_iff) +qed lemma eucl_rel_int: "eucl_rel_int k l (k div l, k mod l)" @@ -445,7 +449,7 @@ shows "i mod k = i \ k = 0 \ 0 \ i \ i < k \ i \ 0 \ k < i" proof - have "i mod k = i \ i div k = 0" - by safe (insert div_mult_mod_eq [of i k], auto) + using div_mult_mod_eq [of i k] by safe auto with zdiv_eq_0_iff show ?thesis by simp @@ -482,17 +486,15 @@ by simp next case False - moreover have \0 < k mod l\ \k mod l < 1 + l\ - using \0 < l\ le_imp_0_less False apply auto - using le_less apply fastforce - using pos_mod_bound [of l k] apply linarith - done - with \l > 0\ have \(k mod l - 1) mod l = k mod l - 1\ + moreover have 1: \0 < k mod l\ + using \0 < l\ False le_less by fastforce + moreover have 2: \k mod l < 1 + l\ + using \0 < l\ pos_mod_bound[of l k] by linarith + from 1 2 \l > 0\ have \(k mod l - 1) mod l = k mod l - 1\ by (simp add: zmod_trivial_iff) ultimately show ?thesis - apply (simp only: zmod_zminus1_eq_if) - apply (simp add: mod_eq_0_iff_dvd algebra_simps mod_simps) - done + by (simp only: zmod_zminus1_eq_if) + (simp add: mod_eq_0_iff_dvd algebra_simps mod_simps) qed qed @@ -581,9 +583,12 @@ for k l :: int proof (cases "k = 0 \ l = 0") case False + then have *: "k \ 0" "l \ 0" + by auto + then have "0 \ k div l \ \ k < 0 \ 0 \ l" + by (meson neg_imp_zdiv_neg_iff not_le not_less_iff_gr_or_eq) then show ?thesis - apply (auto simp add: pos_imp_zdiv_nonneg_iff neg_imp_zdiv_nonneg_iff) - by (meson neg_imp_zdiv_neg_iff not_le not_less_iff_gr_or_eq) + using * by (auto simp add: pos_imp_zdiv_nonneg_iff neg_imp_zdiv_nonneg_iff) qed auto lemma mod_int_pos_iff: @@ -672,7 +677,7 @@ lemma nat_mod_eq_lemma: assumes "(x::nat) mod n = y mod n" and "y \ x" shows "\q. x = y + n * q" - using assms by (rule mod_eq_nat1E) rule + using assms by (rule mod_eq_nat1E) (rule exI) lemma nat_mod_eq_iff: "(x::nat) mod n = y mod n \ (\q1 q2. x + n * q1 = y + n * q2)" (is "?lhs = ?rhs") @@ -681,11 +686,25 @@ {assume xy: "x \ y" from H have th: "y mod n = x mod n" by simp from nat_mod_eq_lemma[OF th xy] have ?rhs - apply clarify apply (rule_tac x="q" in exI) by (rule exI[where x="0"], simp)} + proof + fix q + assume "y = x + n * q" + then have "x + n * q = y + n * 0" + by simp + then show "\q1 q2. x + n * q1 = y + n * q2" + by blast + qed} moreover {assume xy: "y \ x" from nat_mod_eq_lemma[OF H xy] have ?rhs - apply clarify apply (rule_tac x="0" in exI) by (rule_tac x="q" in exI, simp)} + proof + fix q + assume "x = y + n * q" + then have "x + n * 0 = y + n * q" + by simp + then show "\q1 q2. x + n * q1 = y + n * q2" + by blast + qed} ultimately show ?rhs using linear[of x y] by blast next assume ?rhs then obtain q1 q2 where q12: "x + n * q1 = y + n * q2" by blast @@ -740,7 +759,7 @@ have mod_w: "a mod (2 * b) = a mod b + b * w" by (simp add: w_def mod_mult2_eq ac_simps) from assms w_exhaust have "w = 1" - by (auto simp add: mod_w) (insert mod_less, auto) + using mod_less by (auto simp add: mod_w) with mod_w have mod: "a mod (2 * b) = a mod b + b" by simp have "2 * (a div (2 * b)) = a div b - w" by (simp add: w_def div_mult2_eq minus_mod_eq_mult_div ac_simps) diff -r b87b14e885af -r 43f5dfb7fa35 src/HOL/Equiv_Relations.thy --- a/src/HOL/Equiv_Relations.thy Fri Jul 15 09:18:21 2022 +0200 +++ b/src/HOL/Equiv_Relations.thy Fri Jul 22 14:39:56 2022 +0200 @@ -264,11 +264,10 @@ assume cd: "(c,d) \ r1" then have "c \ A1" "d \ A1" using \equiv A1 r1\ by (auto elim!: equiv_type [THEN subsetD, THEN SigmaE2]) - with assms show "\ (f c ` r2 `` {a}) = \ (f d ` r2 `` {a})" - proof (simp add: UN_equiv_class congruent2_implies_congruent) - show "f c a = f d a" - using assms cd unfolding congruent2_def equiv_def refl_on_def by blast - qed + moreover have "f c a = f d a" + using assms cd unfolding congruent2_def equiv_def refl_on_def by blast + ultimately show "\ (f c ` r2 `` {a}) = \ (f d ` r2 `` {a})" + using assms by (simp add: UN_equiv_class congruent2_implies_congruent) qed lemma UN_equiv_class2: @@ -368,7 +367,7 @@ assume ?lhs then show ?rhs unfolding proj_def quotient_def - proof clarsimp + proof safe fix y assume y: "y \ A" and "r `` {x} = r `` {y}" moreover have "y \ r `` {y}" diff -r b87b14e885af -r 43f5dfb7fa35 src/HOL/Euclidean_Division.thy --- a/src/HOL/Euclidean_Division.thy Fri Jul 15 09:18:21 2022 +0200 +++ b/src/HOL/Euclidean_Division.thy Fri Jul 22 14:39:56 2022 +0200 @@ -99,7 +99,8 @@ with size_mult_mono'[OF assms(1), of b] have eq: "euclidean_size (a * b) = euclidean_size b" by simp have "a * b dvd b" - by (rule dvd_euclidean_size_eq_imp_dvd [OF _ eq]) (insert assms, simp_all) + by (rule dvd_euclidean_size_eq_imp_dvd [OF _ eq]) + (use assms in simp_all) hence "a * b dvd 1 * b" by simp with \b \ 0\ have "is_unit a" by (subst (asm) dvd_times_right_cancel_iff) with assms(3) show False by contradiction @@ -108,7 +109,7 @@ lemma dvd_imp_size_le: assumes "a dvd b" "b \ 0" shows "euclidean_size a \ euclidean_size b" - using assms by (auto elim!: dvdE simp: size_mult_mono) + using assms by (auto simp: size_mult_mono) lemma dvd_proper_imp_size_less: assumes "a dvd b" "\ b dvd a" "b \ 0" @@ -139,7 +140,7 @@ lemma coprime_mod_left_iff [simp]: "coprime (a mod b) b \ coprime a b" if "b \ 0" - by (rule; rule coprimeI) + by (rule iffI; rule coprimeI) (use that in \auto dest!: dvd_mod_imp_dvd coprime_common_divisor simp add: dvd_mod_iff\) lemma coprime_mod_right_iff [simp]: diff -r b87b14e885af -r 43f5dfb7fa35 src/HOL/Fields.thy --- a/src/HOL/Fields.thy Fri Jul 15 09:18:21 2022 +0200 +++ b/src/HOL/Fields.thy Fri Jul 22 14:39:56 2022 +0200 @@ -286,7 +286,7 @@ lemma inverse_nonzero_iff_nonzero [simp]: "inverse a = 0 \ a = 0" - by rule (fact inverse_zero_imp_zero, simp) + by (rule iffI) (fact inverse_zero_imp_zero, simp) lemma inverse_minus_eq [simp]: "inverse (- a) = - inverse a" @@ -519,7 +519,7 @@ lemma inverse_eq_1_iff [simp]: "inverse x = 1 \ x = 1" - by (insert inverse_eq_iff_eq [of x 1], simp) + using inverse_eq_iff_eq [of x 1] by simp lemma divide_eq_0_iff [simp]: "a / b = 0 \ a = 0 \ b = 0" @@ -647,8 +647,8 @@ lemma negative_imp_inverse_negative: "a < 0 \ inverse a < 0" - by (insert positive_imp_inverse_positive [of "-a"], - simp add: nonzero_inverse_minus_eq less_imp_not_eq) + using positive_imp_inverse_positive [of "-a"] + by (simp add: nonzero_inverse_minus_eq less_imp_not_eq) lemma inverse_le_imp_le: assumes invle: "inverse a \ inverse b" and apos: "0 < a" diff -r b87b14e885af -r 43f5dfb7fa35 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Fri Jul 15 09:18:21 2022 +0200 +++ b/src/HOL/Finite_Set.thy Fri Jul 22 14:39:56 2022 +0200 @@ -1226,7 +1226,7 @@ subsubsection \Expressing set operations via \<^const>\fold\\ lemma comp_fun_commute_const: "comp_fun_commute (\_. f)" - by standard rule + by standard (rule refl) lemma comp_fun_idem_insert: "comp_fun_idem insert" by standard auto @@ -1571,7 +1571,7 @@ global_interpretation card: folding "\_. Suc" 0 defines card = "folding_on.F (\_. Suc) 0" - by standard rule + by standard (rule refl) lemma card_insert_disjoint: "finite A \ x \ A \ card (insert x A) = Suc (card A)" by (fact card.insert) @@ -1824,11 +1824,12 @@ from "2.prems"(1,2,5) "2.hyps"(1,2) have cst: "card s \ card t" by simp from "2.prems"(3) [OF "2.hyps"(1) cst] - obtain f where "f ` s \ t" "inj_on f s" + obtain f where *: "f ` s \ t" "inj_on f s" by blast - with "2.prems"(2) "2.hyps"(2) show ?case - unfolding inj_on_def - by (rule_tac x = "\z. if z = x then y else f z" in exI) auto + let ?g = "(\a. if a = x then y else f a)" + have "?g ` insert x s \ insert y t \ inj_on ?g (insert x s)" + using * "2.prems"(2) "2.hyps"(2) unfolding inj_on_def by auto + then show ?case by (rule exI[where ?x="?g"]) qed qed @@ -2415,7 +2416,7 @@ by (simp add: fS) have "\x \ y; x \ S; z \ S; f x = f y\ \ \x \ S. x \ y \ f z = f x" for z - by (case_tac "z = y \ z = x") auto + by (cases "z = y \ z = x") auto then show "T \ f ` (S - {y})" using h xy x y f by fastforce qed diff -r b87b14e885af -r 43f5dfb7fa35 src/HOL/Fun.thy --- a/src/HOL/Fun.thy Fri Jul 15 09:18:21 2022 +0200 +++ b/src/HOL/Fun.thy Fri Jul 22 14:39:56 2022 +0200 @@ -377,28 +377,30 @@ lemma bij_betw_comp_iff2: assumes bij: "bij_betw f' A' A''" and img: "f ` A \ A'" - shows "bij_betw f A A' \ bij_betw (f' \ f) A A''" - using assms -proof (auto simp add: bij_betw_comp_iff) - assume *: "bij_betw (f' \ f) A A''" - then show "bij_betw f A A'" - using img - proof (auto simp add: bij_betw_def) - assume "inj_on (f' \ f) A" - then show "inj_on f A" - using inj_on_imageI2 by blast + shows "bij_betw f A A' \ bij_betw (f' \ f) A A''" (is "?L \ ?R") +proof + assume "?L" + then show "?R" + using assms by (auto simp add: bij_betw_comp_iff) next - fix a' - assume **: "a' \ A'" - with bij have "f' a' \ A''" - unfolding bij_betw_def by auto - with * obtain a where 1: "a \ A \ f' (f a) = f' a'" - unfolding bij_betw_def by force - with img have "f a \ A'" by auto - with bij ** 1 have "f a = a'" - unfolding bij_betw_def inj_on_def by auto - with 1 show "a' \ f ` A" by auto - qed + assume *: "?R" + have "inj_on (f' \ f) A \ inj_on f A" + using inj_on_imageI2 by blast + moreover have "A' \ f ` A" + proof + fix a' + assume **: "a' \ A'" + with bij have "f' a' \ A''" + unfolding bij_betw_def by auto + with * obtain a where 1: "a \ A \ f' (f a) = f' a'" + unfolding bij_betw_def by force + with img have "f a \ A'" by auto + with bij ** 1 have "f a = a'" + unfolding bij_betw_def inj_on_def by auto + with 1 show "a' \ f ` A" by auto + qed + ultimately show "?L" + using img * by (auto simp add: bij_betw_def) qed lemma bij_betw_inv: @@ -425,7 +427,7 @@ from g [OF a1] a1 g [OF a2] a2 \?g x = ?g y\ show "x = y" by simp qed moreover have "?g ` B = A" - proof (auto simp: image_def) + proof safe fix b assume "b \ B" with s obtain a where P: "?P b a" by blast @@ -435,7 +437,9 @@ assume "a \ A" with s obtain b where P: "?P b a" by blast with s have "b \ B" by blast - with g[OF P] show "\b\B. a = ?g b" by blast + with g[OF P] have "\b\B. a = ?g b" by blast + then show "a \ ?g ` B" + by auto qed ultimately show ?thesis by (auto simp: bij_betw_def) @@ -637,7 +641,7 @@ next assume *: "bij_betw f (A \ {b}) (A' \ {f b})" have "f ` A = A'" - proof auto + proof safe fix a assume **: "a \