--- a/src/HOL/Library/Equipollence.thy Thu Aug 29 17:47:29 2024 +0200
+++ b/src/HOL/Library/Equipollence.thy Fri Aug 30 10:44:48 2024 +0100
@@ -313,9 +313,7 @@
lemma insert_eqpoll_cong:
"\<lbrakk>A \<approx> B; a \<notin> A; b \<notin> B\<rbrakk> \<Longrightarrow> insert a A \<approx> insert b B"
- apply (rule lepoll_antisym)
- apply (simp add: eqpoll_imp_lepoll insert_lepoll_cong)+
- by (meson eqpoll_imp_lepoll eqpoll_sym insert_lepoll_cong)
+ by (meson eqpoll_imp_lepoll eqpoll_sym insert_lepoll_cong lepoll_antisym)
lemma insert_eqpoll_insert_iff:
"\<lbrakk>a \<notin> A; b \<notin> B\<rbrakk> \<Longrightarrow> insert a A \<approx> insert b B \<longleftrightarrow> A \<approx> B"
@@ -346,8 +344,7 @@
proof (induction A rule: finite_induct)
case (insert x A)
then show ?case
- apply (auto simp: insert_absorb)
- by (metis insert_commute insert_iff insert_lepoll_insertD)
+ by (metis insertI2 insert_lepoll_insert_iff insert_subsetI lepoll_trans subsetI subset_imp_lepoll)
qed auto
@@ -489,9 +486,7 @@
define \<chi> where "\<chi> \<equiv> \<lambda>z. THE x. x \<in> A \<and> z \<in> F x"
have \<chi>: "\<chi> z = x" if "x \<in> A" "z \<in> F x" for x z
unfolding \<chi>_def
- apply (rule the_equality)
- apply (simp add: that)
- by (metis disj disjnt_iff pairwiseD that)
+ by (smt (verit, best) disj disjnt_iff pairwiseD that(1,2) theI_unique)
let ?f = "\<lambda>z. (\<chi> z, b (\<chi> z) z)"
show "inj_on ?f (\<Union>(F ` A))"
unfolding inj_on_def
@@ -562,12 +557,18 @@
qed
lemma lepoll_funcset_right:
- "B \<lesssim> B' \<Longrightarrow> A \<rightarrow>\<^sub>E B \<lesssim> A \<rightarrow>\<^sub>E B'"
- apply (auto simp: lepoll_def inj_on_def)
- apply (rule_tac x = "\<lambda>g. \<lambda>z \<in> A. f(g z)" in exI)
- apply (auto simp: fun_eq_iff)
- apply (metis PiE_E)
- by blast
+ assumes "B \<lesssim> B'" shows "A \<rightarrow>\<^sub>E B \<lesssim> A \<rightarrow>\<^sub>E B'"
+proof -
+ obtain f where f: "inj_on f B" "f ` B \<subseteq> B'"
+ by (meson assms lepoll_def)
+ let ?G = "\<lambda>g. \<lambda>z \<in> A. f(g z)"
+ have "inj_on ?G (A \<rightarrow>\<^sub>E B)"
+ using f by (smt (verit, best) PiE_ext PiE_mem inj_on_def restrict_apply')
+ moreover have "?G ` (A \<rightarrow>\<^sub>E B) \<subseteq> (A \<rightarrow>\<^sub>E B')"
+ using f by fastforce
+ ultimately show ?thesis
+ by (meson lepoll_def)
+qed
lemma lepoll_funcset_left:
assumes "B \<noteq> {}" "A \<lesssim> A'"
@@ -588,10 +589,7 @@
then have "?F k (f x) = ?F l (f x)"
by simp
then show "k x = l x"
- apply (auto simp: h split: if_split_asm)
- apply (metis PiE_arb h k l)
- apply (metis (full_types) PiE_E h k l)
- using fim k l by fastforce
+ by (smt (verit, best) PiE_arb fim h image_subset_iff k l restrict_apply')
next
show "?F ` (A \<rightarrow>\<^sub>E B) \<subseteq> A' \<rightarrow>\<^sub>E B"
using \<open>b \<in> B\<close> by force
@@ -608,13 +606,13 @@
proof -
obtain f where f: "\<And>i. i \<in> A \<Longrightarrow> inj_on (f i) (B i) \<and> (f i) ` B i \<subseteq> C i"
using assms unfolding lepoll_def by metis
- then show ?thesis
- unfolding lepoll_def
- apply (rule_tac x = "\<lambda>g. \<lambda>i \<in> A. f i (g i)" in exI)
- apply (auto simp: inj_on_def)
- apply (rule PiE_ext, auto)
- apply (metis (full_types) PiE_mem restrict_apply')
- by blast
+ let ?G = "\<lambda>g. \<lambda>i \<in> A. f i (g i)"
+ have "inj_on ?G (PiE A B)"
+ by (smt (verit, ccfv_SIG) PiE_ext PiE_iff f inj_on_def restrict_apply')
+ moreover have "?G ` (PiE A B) \<subseteq> (PiE A C)"
+ using f by fastforce
+ ultimately show ?thesis
+ by (meson lepoll_def)
qed
@@ -678,18 +676,15 @@
also have "\<dots> = (UNIV::nat set) \<rightarrow>\<^sub>E (UNIV::bool set)"
by auto
also have "\<dots> \<lesssim> J \<rightarrow>\<^sub>E (UNIV::bool set)"
- apply (rule lepoll_funcset_left)
- using infinite_le_lepoll that by auto
+ by (metis empty_not_UNIV infinite_le_lepoll lepoll_funcset_left that)
also have "\<dots> \<lesssim> Pi\<^sub>E J S"
proof -
- have *: "(UNIV::bool set) \<lesssim> S i" if "i \<in> I" and "\<forall>a. \<not> S i \<subseteq> {a}" for i
+ have *: "(UNIV::bool set) \<lesssim> S i" if "i \<in> I" and \<section>: "\<forall>a. \<not> S i \<subseteq> {a}" for i
proof -
obtain a b where "{a,b} \<subseteq> S i" "a \<noteq> b"
- by (metis \<open>\<forall>a. \<not> S i \<subseteq> {a}\<close> all_not_in_conv empty_subsetI insertCI insert_subset set_eq_subset subsetI)
+ by (metis \<section> empty_subsetI insert_subset subsetI)
then show ?thesis
- apply (clarsimp simp: lepoll_def inj_on_def)
- apply (rule_tac x="\<lambda>x. if x then a else b" in exI, auto)
- done
+ by (metis Set.set_insert UNIV_bool insert_iff insert_lepoll_cong insert_subset singleton_lepoll)
qed
show ?thesis
by (auto simp: * J_def intro: lepoll_PiE)
@@ -727,10 +722,12 @@
have *: "finite (Pi\<^sub>E I S)"
if "finite J" and "\<forall>i\<in>I. finite (S i)"
proof (rule finite_subset)
- show "Pi\<^sub>E I S \<subseteq> ?F"
- apply safe
- using J_def apply blast
+ have "\<And>f j. \<lbrakk>f \<in> Pi\<^sub>E I S; j \<in> J\<rbrakk> \<Longrightarrow> f j \<in> \<Union> (S ` J)"
+ using J_def by blast
+ moreover
+ have "\<And>f j. \<lbrakk>f \<in> Pi\<^sub>E I S; f j \<noteq> (if j \<in> I then a j else undefined)\<rbrakk> \<Longrightarrow> j \<in> J"
by (metis DiffI PiE_E a singletonD)
+ ultimately show "Pi\<^sub>E I S \<subseteq> ?F" by force
show "finite ?F"
proof (rule finite_restricted_funspace [OF \<open>finite J\<close>])
show "finite (\<Union> (S ` J))"
--- a/src/HOL/Library/FSet.thy Thu Aug 29 17:47:29 2024 +0200
+++ b/src/HOL/Library/FSet.thy Fri Aug 30 10:44:48 2024 +0100
@@ -1175,15 +1175,13 @@
lemma atomize_fBall:
"(\<And>x. x |\<in>| A ==> P x) == Trueprop (fBall A (\<lambda>x. P x))"
-apply (simp only: atomize_all atomize_imp)
-apply (rule equal_intr_rule)
- by (transfer, simp)+
+ by (simp add: Set.atomize_ball)
lemma fBall_mono[mono]: "P \<le> Q \<Longrightarrow> fBall S P \<le> fBall S Q"
-by auto
+ by auto
lemma fBex_mono[mono]: "P \<le> Q \<Longrightarrow> fBex S P \<le> fBex S Q"
-by auto
+ by auto
end
@@ -1552,7 +1550,7 @@
lemma fset_strong_cases:
obtains "xs = {||}"
| ys x where "x |\<notin>| ys" and "xs = finsert x ys"
-by transfer blast
+ by auto
lemma fset_induct2:
"P {||} {||} \<Longrightarrow>
@@ -1560,12 +1558,7 @@
(\<And>y ys. y |\<notin>| ys \<Longrightarrow> P {||} (finsert y ys)) \<Longrightarrow>
(\<And>x xs y ys. \<lbrakk>P xs ys; x |\<notin>| xs; y |\<notin>| ys\<rbrakk> \<Longrightarrow> P (finsert x xs) (finsert y ys)) \<Longrightarrow>
P xsa ysa"
- apply (induct xsa arbitrary: ysa)
- apply (induct_tac x rule: fset_induct_stronger)
- apply simp_all
- apply (induct_tac xa rule: fset_induct_stronger)
- apply simp_all
- done
+by (induct xsa arbitrary: ysa; metis fset_induct_stronger)
subsection \<open>Lemmas depending on induction\<close>
@@ -1583,25 +1576,16 @@
lemma rel_fset_alt_def: "rel_fset R = (\<lambda>A B. (\<forall>x.\<exists>y. x|\<in>|A \<longrightarrow> y|\<in>|B \<and> R x y)
\<and> (\<forall>y. \<exists>x. y|\<in>|B \<longrightarrow> x|\<in>|A \<and> R x y))"
-apply (rule ext)+
-apply transfer'
-apply (subst rel_set_def[unfolded fun_eq_iff])
-by blast
+ by transfer' (metis (no_types, opaque_lifting) rel_set_def)
lemma finite_rel_set:
assumes fin: "finite X" "finite Z"
assumes R_S: "rel_set (R OO S) X Z"
shows "\<exists>Y. finite Y \<and> rel_set R X Y \<and> rel_set S Y Z"
proof -
- obtain f where f: "\<forall>x\<in>X. R x (f x) \<and> (\<exists>z\<in>Z. S (f x) z)"
- apply atomize_elim
- apply (subst bchoice_iff[symmetric])
- using R_S[unfolded rel_set_def OO_def] by blast
-
- obtain g where g: "\<forall>z\<in>Z. S (g z) z \<and> (\<exists>x\<in>X. R x (g z))"
- apply atomize_elim
- apply (subst bchoice_iff[symmetric])
- using R_S[unfolded rel_set_def OO_def] by blast
+ obtain f g where f: "\<forall>x\<in>X. R x (f x) \<and> (\<exists>z\<in>Z. S (f x) z)"
+ and g: "\<forall>z\<in>Z. S (g z) z \<and> (\<exists>x\<in>X. R x (g z))"
+ using R_S[unfolded rel_set_def OO_def] by metis
let ?Y = "f ` X \<union> g ` Z"
have "finite ?Y" by (simp add: fin)
@@ -1713,13 +1697,13 @@
lemma ffilter_transfer [transfer_rule]:
assumes "bi_unique A"
shows "((A ===> (=)) ===> rel_fset A ===> rel_fset A) ffilter ffilter"
- using assms unfolding rel_fun_def
- using Lifting_Set.filter_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast
+ using assms Lifting_Set.filter_transfer
+ unfolding rel_fun_def by (metis ffilter.rep_eq rel_fset.rep_eq)
lemma card_transfer [transfer_rule]:
"bi_unique A \<Longrightarrow> (rel_fset A ===> (=)) fcard fcard"
- unfolding rel_fun_def
- using card_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast
+ using card_transfer unfolding rel_fun_def
+ by (metis fcard.rep_eq rel_fset.rep_eq)
end
@@ -1735,13 +1719,10 @@
lemma rel_fset_alt:
"rel_fset R a b \<longleftrightarrow> (\<forall>t \<in> fset a. \<exists>u \<in> fset b. R t u) \<and> (\<forall>t \<in> fset b. \<exists>u \<in> fset a. R u t)"
-by transfer (simp add: rel_set_def)
+ by transfer (simp add: rel_set_def)
lemma fset_to_fset: "finite A \<Longrightarrow> fset (the_inv fset A) = A"
-apply (rule f_the_inv_into_f[unfolded inj_on_def])
-apply (simp add: fset_inject)
-apply (rule range_eqI Abs_fset_inverse[symmetric] CollectI)+
-.
+ by (metis CollectI f_the_inv_into_f fset_cases fset_cong inj_onI rangeI)
lemma rel_fset_aux:
"(\<forall>t \<in> fset a. \<exists>u \<in> fset b. R t u) \<and> (\<forall>u \<in> fset b. \<exists>t \<in> fset a. R t u) \<longleftrightarrow>
@@ -1762,10 +1743,7 @@
qed (auto simp add: *)
next
assume ?R thus ?L unfolding Grp_def relcompp.simps conversep.simps
- apply (simp add: subset_eq Ball_def)
- apply (rule conjI)
- apply (transfer, clarsimp, metis snd_conv)
- by (transfer, clarsimp, metis fst_conv)
+ using Product_Type.Collect_case_prodD by blast
qed
bnf "'a fset"
@@ -1790,7 +1768,7 @@
done
lemma rel_fset_fset: "rel_set \<chi> (fset A1) (fset A2) = rel_fset \<chi> A1 A2"
- by transfer (rule refl)
+ by (simp add: rel_fset.rep_eq)
end
@@ -1802,11 +1780,13 @@
subsection \<open>Size setup\<close>
-context includes fset.lifting begin
+context includes fset.lifting
+begin
lift_definition size_fset :: "('a \<Rightarrow> nat) \<Rightarrow> 'a fset \<Rightarrow> nat" is "\<lambda>f. sum (Suc \<circ> f)" .
end
-instantiation fset :: (type) size begin
+instantiation fset :: (type) size
+begin
definition size_fset where
size_fset_overloaded_def: "size_fset = FSet.size_fset (\<lambda>_. 0)"
instance ..
@@ -1821,8 +1801,8 @@
folded size_fset_overloaded_def])
lemma fset_size_o_map: "inj f \<Longrightarrow> size_fset g \<circ> fimage f = size_fset (g \<circ> f)"
- apply (subst fun_eq_iff)
- including fset.lifting by transfer (auto intro: sum.reindex_cong subset_inj_on)
+ unfolding fun_eq_iff
+ by (simp add: inj_def inj_onI sum.reindex)
setup \<open>
BNF_LFP_Size.register_size_global \<^type_name>\<open>fset\<close> \<^const_name>\<open>size_fset\<close>
@@ -1902,16 +1882,11 @@
subsubsection \<open>Countability\<close>
lemma exists_fset_of_list: "\<exists>xs. fset_of_list xs = S"
-including fset.lifting
-by transfer (rule finite_list)
+ including fset.lifting
+ by transfer (rule finite_list)
lemma fset_of_list_surj[simp, intro]: "surj fset_of_list"
-proof -
- have "x \<in> range fset_of_list" for x :: "'a fset"
- unfolding image_iff
- using exists_fset_of_list by fastforce
- thus ?thesis by auto
-qed
+ by (metis exists_fset_of_list surj_def)
instance fset :: (countable) countable
proof
--- a/src/HOL/Library/Float.thy Thu Aug 29 17:47:29 2024 +0200
+++ b/src/HOL/Library/Float.thy Fri Aug 30 10:44:48 2024 +0100
@@ -103,8 +103,8 @@
by (simp add: float_def) (metis mult_minus_left of_int_minus)
lemma times_float[simp]: "x \<in> float \<Longrightarrow> y \<in> float \<Longrightarrow> x * y \<in> float"
- apply (clarsimp simp: float_def)
- by (metis (no_types, opaque_lifting) of_int_add powr_add mult.assoc mult.left_commute of_int_mult)
+ apply (clarsimp simp: float_def mult_ac)
+ by (metis mult.assoc of_int_mult of_int_add powr_add)
lemma minus_float[simp]: "x \<in> float \<Longrightarrow> y \<in> float \<Longrightarrow> x - y \<in> float"
using plus_float [of x "- y"] by simp
@@ -248,10 +248,7 @@
end
lemma float_numeral[simp]: "real_of_float (numeral x :: float) = numeral x"
-proof (induct x)
- case One
- then show ?case by simp
-qed (metis of_int_numeral real_of_float_of_int_eq)+
+ by (metis of_int_numeral real_of_float_of_int_eq)
lemma transfer_numeral [transfer_rule]:
"rel_fun (=) pcr_float (numeral :: _ \<Rightarrow> real) (numeral :: _ \<Rightarrow> float)"
@@ -525,10 +522,7 @@
then have "mantissa f = m * 2^nat (e - exponent f)"
by linarith
with \<open>exponent f < e\<close> have "2 dvd mantissa f"
- apply (intro dvdI[where k="m * 2^(nat (e-exponent f)) div 2"])
- apply (cases "nat (e - exponent f)")
- apply auto
- done
+ by (force intro: dvdI[where k="m * 2^(nat (e-exponent f)) div 2"])
then show False using mantissa_not_dvd[OF not_0] by simp
qed
ultimately have "real_of_int m = mantissa f * 2^nat (exponent f - e)"
@@ -843,15 +837,7 @@
then have ne: "real_of_int (a mod b) / real_of_int b \<noteq> 0"
using \<open>b \<noteq> 0\<close> by auto
have "\<lceil>real_of_int a / real_of_int b\<rceil> = \<lfloor>real_of_int a / real_of_int b\<rfloor> + 1"
- apply (rule ceiling_eq)
- apply (auto simp flip: floor_divide_of_int_eq)
- proof -
- have "real_of_int \<lfloor>real_of_int a / real_of_int b\<rfloor> \<le> real_of_int a / real_of_int b"
- by simp
- moreover have "real_of_int \<lfloor>real_of_int a / real_of_int b\<rfloor> \<noteq> real_of_int a / real_of_int b"
- by (smt (verit) floor_divide_of_int_eq ne of_int_div_aux)
- ultimately show "real_of_int \<lfloor>real_of_int a / real_of_int b\<rfloor> < real_of_int a / real_of_int b" by arith
- qed
+ by (metis add_cancel_left_right ceiling_altdef floor_divide_of_int_eq ne of_int_div_aux)
then show ?thesis
using \<open>\<not> b dvd a\<close> by simp
qed
@@ -967,11 +953,12 @@
proof -
have "0 \<le> log 2 x - real_of_int \<lfloor>log 2 x\<rfloor>"
by (simp add: algebra_simps)
- with assms
- show ?thesis
- apply (auto simp: truncate_down_def round_down_def mult_powr_eq
+ moreover have "0 \<le> real p - real_of_int \<lfloor>log 2 x\<rfloor> + log 2 x"
+ by linarith
+ ultimately show ?thesis
+ using assms
+ by (auto simp: truncate_down_def round_down_def mult_powr_eq
intro!: ge_one_powr_ge_zero mult_pos_pos)
- by linarith
qed
lemma truncate_down_nonneg: "0 \<le> y \<Longrightarrow> 0 \<le> truncate_down prec y"
@@ -2119,8 +2106,7 @@
assume [simp]: "odd j"
have "power_up prec 0 (Suc (j div 2)) \<le> - power_up prec b (Suc (j div 2))"
if "b < 0" "even (j div 2)"
- apply (rule order_trans[where y=0])
- using IH that by (auto simp: div2_less_self)
+ by (metis Suc_neq_Zero even_Suc neg_0_le_iff_le power_up_eq_zero_iff power_up_nonpos_iff that)
then have "truncate_up prec ((power_up prec a (Suc (j div 2)))\<^sup>2)
\<le> truncate_up prec ((power_up prec b (Suc (j div 2)))\<^sup>2)"
using IH
@@ -2307,9 +2293,7 @@
qualified lemma compute_floor_fl[code]:
"floor_fl (Float m e) = (if 0 \<le> e then Float m e else Float (m div (2 ^ (nat (-e)))) 0)"
apply transfer
- apply (simp add: powr_int floor_divide_of_int_eq)
- apply (metis floor_divide_of_int_eq of_int_eq_numeral_power_cancel_iff)
- done
+ using compute_int_floor_fl int_floor_fl.rep_eq powr_int by auto
end
--- a/src/HOL/Library/FuncSet.thy Thu Aug 29 17:47:29 2024 +0200
+++ b/src/HOL/Library/FuncSet.thy Fri Aug 30 10:44:48 2024 +0100
@@ -259,9 +259,7 @@
by (auto simp add: bij_betw_def inj_on_def compose_eq)
lemma bij_betw_compose: "bij_betw f A B \<Longrightarrow> bij_betw g B C \<Longrightarrow> bij_betw (compose A g f) A C"
- apply (simp add: bij_betw_def compose_eq inj_on_compose)
- apply (auto simp add: compose_def image_def)
- done
+ by (simp add: bij_betw_def inj_on_compose surj_compose)
lemma bij_betw_restrict_eq [simp]: "bij_betw (restrict f A) A B = bij_betw f A B"
by (simp add: bij_betw_def)
@@ -298,15 +296,10 @@
by (unfold inv_into_def) (fast intro: someI2)
lemma compose_inv_into_id: "bij_betw f A B \<Longrightarrow> compose A (\<lambda>y\<in>B. inv_into A f y) f = (\<lambda>x\<in>A. x)"
- apply (simp add: bij_betw_def compose_def)
- apply (rule restrict_ext, auto)
- done
+ by (smt (verit, best) bij_betwE bij_betw_inv_into_left compose_def restrict_apply' restrict_ext)
lemma compose_id_inv_into: "f ` A = B \<Longrightarrow> compose B f (\<lambda>y\<in>B. inv_into A f y) = (\<lambda>x\<in>B. x)"
- apply (simp add: compose_def)
- apply (rule restrict_ext)
- apply (simp add: f_inv_into_f)
- done
+ by (smt (verit, best) compose_def f_inv_into_f restrict_apply' restrict_ext)
lemma extensional_insert[intro, simp]:
assumes "a \<in> extensional (insert i I)"
@@ -538,12 +531,15 @@
"(\<lambda>f. f i) ` (PiE I S) = (if PiE I S = {} then {} else if i \<in> I then S i else {undefined})"
proof -
have "(\<lambda>f. f i) ` Pi\<^sub>E I S = S i" if "i \<in> I" "f \<in> PiE I S" for f
- using that apply auto
- by (rule_tac x="(\<lambda>k. if k=i then x else f k)" in image_eqI) auto
- moreover have "(\<lambda>f. f i) ` Pi\<^sub>E I S = {undefined}" if "f \<in> PiE I S" "i \<notin> I" for f
- using that by (blast intro: PiE_arb [OF that, symmetric])
- ultimately show ?thesis
- by auto
+ proof -
+ have "x \<in> S i \<Longrightarrow> \<exists>f\<in>Pi\<^sub>E I S. x = f i" for x
+ using that
+ by (force intro: bexI [where x="\<lambda>k. if k=i then x else f k"])
+ then show ?thesis
+ using that by force
+ qed
+ then show ?thesis
+ by (smt (verit) PiE_arb equals0I image_cong image_constant image_empty)
qed
lemma PiE_singleton:
@@ -563,9 +559,12 @@
by (metis (mono_tags, lifting) PiE_eq PiE_singleton insert_not_empty restrict_apply' restrict_extensional)
lemma PiE_over_singleton_iff: "(\<Pi>\<^sub>E x\<in>{a}. B x) = (\<Union>b \<in> B a. {\<lambda>x \<in> {a}. b})"
- apply (auto simp: PiE_iff split: if_split_asm)
- apply (metis (no_types, lifting) extensionalityI restrict_apply' restrict_extensional singletonD)
- done
+proof -
+ have "\<And>x. \<lbrakk>x a \<in> B a; x \<in> extensional {a}\<rbrakk> \<Longrightarrow> \<exists>xa\<in>B a. x = (\<lambda>x\<in>{a}. xa)"
+ using PiE_singleton by fastforce
+ then show ?thesis
+ by (auto simp: PiE_iff split: if_split_asm)
+qed
lemma all_PiE_elements:
"(\<forall>z \<in> PiE I S. \<forall>i \<in> I. P i (z i)) \<longleftrightarrow> PiE I S = {} \<or> (\<forall>i \<in> I. \<forall>x \<in> S i. P i x)" (is "?lhs = ?rhs")
@@ -582,7 +581,7 @@
have "(\<lambda>j \<in> I. if j=i then x else f j) \<in> PiE I S"
by (simp add: f that(2))
then have "P i ((\<lambda>j \<in> I. if j=i then x else f j) i)"
- using L that(1) by blast
+ using L that by blast
with that show ?thesis
by simp
qed
@@ -608,26 +607,30 @@
assumes "x \<notin> S"
shows "{f. f \<in> (insert x S) \<rightarrow>\<^sub>E T \<and> inj_on f (insert x S)} =
(\<lambda>(y, g). g(x:=y)) ` {(y, g). y \<in> T \<and> g \<in> S \<rightarrow>\<^sub>E (T - {y}) \<and> inj_on g S}"
- using assms
- apply (auto del: PiE_I PiE_E)
- apply (auto intro: extensional_funcset_fun_upd_inj_onI
- extensional_funcset_fun_upd_extends_rangeI del: PiE_I PiE_E)
- apply (auto simp add: image_iff inj_on_def)
- apply (rule_tac x="xa x" in exI)
- apply (auto intro: PiE_mem del: PiE_I PiE_E)
- apply (rule_tac x="xa(x := undefined)" in exI)
- apply (auto intro!: extensional_funcset_fun_upd_restricts_rangeI)
- apply (auto dest!: PiE_mem split: if_split_asm)
- done
+proof -
+ have "\<And>a f y. \<lbrakk>f \<in> S \<rightarrow>\<^sub>E T - {a}; a = (if y = x then a else f y); y \<in> S\<rbrakk>
+ \<Longrightarrow> False"
+ using assms by (auto dest!: PiE_mem split: if_split_asm)
+ moreover
+ have "\<And>f. \<lbrakk> f \<in> insert x S \<rightarrow>\<^sub>E T; inj_on f S; \<forall>xb\<in>S. f x \<noteq> f xb\<rbrakk>
+ \<Longrightarrow> \<exists>b. b \<in> S \<rightarrow>\<^sub>E T - {f x} \<and> inj_on b S \<and> f = b(x := f x)"
+ unfolding inj_on_def
+ by (smt (verit, ccfv_threshold) PiE_restrict fun_upd_apply fun_upd_triv insert_Diff insert_iff
+ restrict_PiE_iff restrict_upd)
+ ultimately show ?thesis
+ using assms
+ apply (auto simp: image_iff intro: extensional_funcset_fun_upd_inj_onI
+ extensional_funcset_fun_upd_extends_rangeI del: PiE_I PiE_E)
+ apply (smt (verit, best) PiE_cong PiE_mem inj_on_def insertCI)
+ by blast
+qed
lemma extensional_funcset_extend_domain_inj_onI:
assumes "x \<notin> S"
shows "inj_on (\<lambda>(y, g). g(x := y)) {(y, g). y \<in> T \<and> g \<in> S \<rightarrow>\<^sub>E (T - {y}) \<and> inj_on g S}"
using assms
- apply (auto intro!: inj_onI)
- apply (metis fun_upd_same)
- apply (metis assms PiE_arb fun_upd_triv fun_upd_upd)
- done
+ apply (simp add: inj_on_def)
+ by (metis PiE_restrict fun_upd_apply restrict_fupd)
subsubsection \<open>Misc properties of functions, composition and restriction from HOL Light\<close>
--- a/src/HOL/Library/Interval.thy Thu Aug 29 17:47:29 2024 +0200
+++ b/src/HOL/Library/Interval.thy Fri Aug 30 10:44:48 2024 +0100
@@ -564,16 +564,7 @@
using that
apply transfer
apply (clarsimp simp add: Let_def)
- apply (intro conjI)
- apply (metis linear min.coboundedI1 min.coboundedI2 mult_left_mono mult_left_mono_neg order_trans)
- apply (metis linear min.coboundedI1 min.coboundedI2 mult_left_mono mult_left_mono_neg order_trans)
- apply (metis linear min.coboundedI1 min.coboundedI2 mult_left_mono mult_left_mono_neg order_trans)
- apply (metis linear min.coboundedI1 min.coboundedI2 mult_left_mono mult_left_mono_neg order_trans)
- apply (metis linear max.coboundedI1 max.coboundedI2 mult_left_mono mult_left_mono_neg order_trans)
- apply (metis linear max.coboundedI1 max.coboundedI2 mult_left_mono mult_left_mono_neg order_trans)
- apply (metis linear max.coboundedI1 max.coboundedI2 mult_left_mono mult_left_mono_neg order_trans)
- apply (metis linear max.coboundedI1 max.coboundedI2 mult_left_mono mult_left_mono_neg order_trans)
- done
+ by (smt (verit, best) linorder_le_cases max.coboundedI1 max.coboundedI2 min.absorb1 min.coboundedI2 mult_left_mono mult_left_mono_neg)
lemma set_of_distrib_left:
"set_of (B * (A1 + A2)) \<subseteq> set_of (B * A1 + B * A2)"
@@ -595,19 +586,7 @@
"set_of ((A1 + A2) * B) \<subseteq> set_of (A1 * B + A2 * B)"
for A1 A2 B :: "'a::{linordered_ring, real_normed_algebra, linear_continuum_topology} interval"
unfolding set_of_times set_of_plus set_plus_def
- apply clarsimp
- subgoal for b a1 a2
- apply (rule exI[where x="a1 * b"])
- apply (rule conjI)
- subgoal by force
- subgoal
- apply (rule exI[where x="a2 * b"])
- apply (rule conjI)
- subgoal by force
- subgoal by (simp add: algebra_simps)
- done
- done
- done
+ using distrib_right by blast
lemma set_of_mul_inc_left:
"set_of (A * B) \<subseteq> set_of (A' * B)"
@@ -671,10 +650,7 @@
mult_bounds_enclose_zero1 mult_bounds_enclose_zero2)
instance "interval" :: ("{linordered_semiring, zero, times}") mult_zero
- apply standard
- subgoal by transfer auto
- subgoal by transfer auto
- done
+ by (standard; transfer; auto)
lift_definition min_interval::"'a::linorder interval \<Rightarrow> 'a interval \<Rightarrow> 'a interval" is
"\<lambda>(l1, u1). \<lambda>(l2, u2). (min l1 l2, min u1 u2)"
--- a/src/HOL/Library/Numeral_Type.thy Thu Aug 29 17:47:29 2024 +0200
+++ b/src/HOL/Library/Numeral_Type.thy Fri Aug 30 10:44:48 2024 +0100
@@ -135,53 +135,50 @@
begin
lemma size0: "0 < n"
-using size1 by simp
+ using size1 by simp
lemmas definitions =
zero_def one_def add_def mult_def minus_def diff_def
lemma Rep_less_n: "Rep x < n"
-by (rule type_definition.Rep [OF type, simplified, THEN conjunct2])
+ by (rule type_definition.Rep [OF type, simplified, THEN conjunct2])
lemma Rep_le_n: "Rep x \<le> n"
-by (rule Rep_less_n [THEN order_less_imp_le])
+ by (rule Rep_less_n [THEN order_less_imp_le])
lemma Rep_inject_sym: "x = y \<longleftrightarrow> Rep x = Rep y"
-by (rule type_definition.Rep_inject [OF type, symmetric])
+ by (rule type_definition.Rep_inject [OF type, symmetric])
lemma Rep_inverse: "Abs (Rep x) = x"
-by (rule type_definition.Rep_inverse [OF type])
+ by (rule type_definition.Rep_inverse [OF type])
lemma Abs_inverse: "m \<in> {0..<n} \<Longrightarrow> Rep (Abs m) = m"
-by (rule type_definition.Abs_inverse [OF type])
+ by (rule type_definition.Abs_inverse [OF type])
lemma Rep_Abs_mod: "Rep (Abs (m mod n)) = m mod n"
using size0 by (simp add: Abs_inverse)
lemma Rep_Abs_0: "Rep (Abs 0) = 0"
-by (simp add: Abs_inverse size0)
+ by (simp add: Abs_inverse size0)
lemma Rep_0: "Rep 0 = 0"
-by (simp add: zero_def Rep_Abs_0)
+ by (simp add: zero_def Rep_Abs_0)
lemma Rep_Abs_1: "Rep (Abs 1) = 1"
-by (simp add: Abs_inverse size1)
+ by (simp add: Abs_inverse size1)
lemma Rep_1: "Rep 1 = 1"
-by (simp add: one_def Rep_Abs_1)
+ by (simp add: one_def Rep_Abs_1)
lemma Rep_mod: "Rep x mod n = Rep x"
-apply (rule_tac x=x in type_definition.Abs_cases [OF type])
-apply (simp add: type_definition.Abs_inverse [OF type])
-done
+ using type_definition.Abs_cases [OF type]
+ by (metis Abs_inverse atLeastLessThan_iff mod_pos_pos_trivial)
lemmas Rep_simps =
Rep_inject_sym Rep_inverse Rep_Abs_mod Rep_mod Rep_Abs_0 Rep_Abs_1
lemma comm_ring_1: "OFCLASS('a, comm_ring_1_class)"
-apply (intro_classes, unfold definitions)
-apply (simp_all add: Rep_simps mod_simps field_simps)
-done
+ by intro_classes (auto simp: Rep_simps mod_simps field_simps definitions)
end
@@ -192,20 +189,13 @@
begin
lemma of_nat_eq: "of_nat k = Abs (int k mod n)"
-apply (induct k)
-apply (simp add: zero_def)
-apply (simp add: Rep_simps add_def one_def mod_simps ac_simps)
-done
+ by (induct k) (simp_all add: zero_def Rep_simps add_def one_def mod_simps ac_simps)
lemma of_int_eq: "of_int z = Abs (z mod n)"
-apply (cases z rule: int_diff_cases)
-apply (simp add: Rep_simps of_nat_eq diff_def mod_simps)
-done
+ by (cases z rule: int_diff_cases) (simp add: Rep_simps of_nat_eq diff_def mod_simps)
-lemma Rep_numeral:
- "Rep (numeral w) = numeral w mod n"
-using of_int_eq [of "numeral w"]
-by (simp add: Rep_inject_sym Rep_Abs_mod)
+lemma Rep_numeral: "Rep (numeral w) = numeral w mod n"
+ by (metis Rep_Abs_mod of_int_eq of_int_numeral)
lemma iszero_numeral:
"iszero (numeral w::'a) \<longleftrightarrow> numeral w mod n = 0"
@@ -214,14 +204,11 @@
lemma cases:
assumes 1: "\<And>z. \<lbrakk>(x::'a) = of_int z; 0 \<le> z; z < n\<rbrakk> \<Longrightarrow> P"
shows "P"
-apply (cases x rule: type_definition.Abs_cases [OF type])
-apply (rule_tac z="y" in 1)
-apply (simp_all add: of_int_eq)
-done
+ by (metis Rep_inverse Rep_less_n Rep_mod assms of_int_eq pos_mod_sign size0)
lemma induct:
"(\<And>z. \<lbrakk>0 \<le> z; z < n\<rbrakk> \<Longrightarrow> P (of_int z)) \<Longrightarrow> P (x::'a)"
-by (cases x rule: cases) simp
+ by (cases x rule: cases) simp
lemma UNIV_eq: "(UNIV :: 'a set) = Abs ` {0..<n}"
using type type_definition.univ by blast
@@ -304,7 +291,7 @@
mod_type "int CARD('a::finite bit1)"
"Rep_bit1 :: 'a::finite bit1 \<Rightarrow> int"
"Abs_bit1 :: int \<Rightarrow> 'a::finite bit1"
-apply (rule mod_type.intro)
+ apply (rule mod_type.intro)
apply (simp add: type_definition_bit1)
apply (rule one_less_int_card)
apply (rule zero_bit1_def)