--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy Fri Apr 12 10:10:16 2024 +0200
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy Fri Apr 12 09:58:53 2024 +0100
@@ -36,11 +36,19 @@
by (metis path_connected_continuous_image retract_of_def retraction)
lemma retract_of_simply_connected:
- "\<lbrakk>simply_connected T; S retract_of T\<rbrakk> \<Longrightarrow> simply_connected S"
- apply (simp add: retract_of_def retraction_def Pi_iff, clarify)
- apply (rule simply_connected_retraction_gen)
- apply (force elim!: continuous_on_subset)+
- done
+ assumes T: "simply_connected T" and "S retract_of T"
+ shows "simply_connected S"
+proof -
+ obtain r where r: "retraction T S r"
+ using assms by (metis retract_of_def)
+ have "S \<subseteq> T"
+ by (meson \<open>retraction T S r\<close> retraction)
+ then have "(\<lambda>a. a) \<in> S \<rightarrow> T"
+ by blast
+ then show ?thesis
+ using simply_connected_retraction_gen [OF T]
+ by (metis (no_types) r retraction retraction_refl)
+qed
lemma retract_of_homotopically_trivial:
assumes ts: "T retract_of S"
@@ -56,10 +64,7 @@
then obtain k where "Retracts S r T k"
unfolding Retracts_def using continuous_on_id by blast
then show ?thesis
- apply (rule Retracts.homotopically_trivial_retraction_gen)
- using assms
- apply (force simp: hom)+
- done
+ by (rule Retracts.homotopically_trivial_retraction_gen) (use assms hom in force)+
qed
lemma retract_of_homotopically_trivial_null:
@@ -74,9 +79,11 @@
then obtain k where "Retracts S r T k"
unfolding Retracts_def by fastforce
then show ?thesis
- apply (rule Retracts.homotopically_trivial_retraction_null_gen)
- apply (rule TrueI refl assms that | assumption)+
- done
+ proof (rule Retracts.homotopically_trivial_retraction_null_gen)
+ show "\<And>f. \<lbrakk>continuous_on U f; f \<in> U \<rightarrow> S\<rbrakk>
+ \<Longrightarrow> \<exists>c. homotopic_with_canon (\<lambda>a. True) U S f (\<lambda>x. c)"
+ using hom by blast
+ qed (use assms that in auto)
qed
lemma retraction_openin_vimage_iff:
@@ -101,13 +108,13 @@
assumes "locally connected T" "S retract_of T"
shows "locally connected S"
using assms
- by (metis Abstract_Topology_2.retraction_openin_vimage_iff idempotent_imp_retraction locally_connected_quotient_image retract_ofE)
+ by (metis retraction_openin_vimage_iff idempotent_imp_retraction locally_connected_quotient_image retract_ofE)
lemma retract_of_locally_path_connected:
assumes "locally path_connected T" "S retract_of T"
shows "locally path_connected S"
using assms
- by (metis Abstract_Topology_2.retraction_openin_vimage_iff idempotent_imp_retraction locally_path_connected_quotient_image retract_ofE)
+ by (metis retraction_openin_vimage_iff idempotent_imp_retraction locally_path_connected_quotient_image retract_ofE)
text \<open>A few simple lemmas about deformation retracts\<close>
@@ -137,15 +144,16 @@
then show ?rhs
by (auto simp: retract_of_def retraction_def)
next
- assume ?rhs
- then show ?lhs
- apply (clarsimp simp add: retract_of_def retraction_def)
- apply (rule_tac x=r in exI, simp)
- apply (rule homotopic_with_trans, assumption)
- apply (rule_tac f = "r \<circ> f" and g="r \<circ> id" in homotopic_with_eq)
- apply (rule_tac Y=S in homotopic_with_compose_continuous_left)
+ assume R: ?rhs
+ have "\<And>r f. \<lbrakk>T \<subseteq> S; continuous_on S r; homotopic_with_canon (\<lambda>x. True) S S id f;
+ f \<in> S \<rightarrow> T; r \<in> S \<rightarrow> T; \<forall>x\<in>T. r x = x\<rbrakk>
+ \<Longrightarrow> homotopic_with_canon (\<lambda>x. True) S S f r"
+ apply (rule_tac f = "r \<circ> f" and g="r \<circ> id" in homotopic_with_eq)
+ apply (rule_tac Y=S in homotopic_with_compose_continuous_left)
apply (auto simp: homotopic_with_sym Pi_iff)
done
+ with R homotopic_with_trans show ?lhs
+ unfolding retract_of_def retraction_def by blast
qed
lemma deformation_retract_of_contractible_sing:
@@ -959,7 +967,7 @@
qed }
with ks_f' eq \<open>a \<noteq> f' n\<close> \<open>n \<noteq> 0\<close> show ?thesis
apply (intro ex1I[of _ "f' ` {.. n}"])
- apply auto []
+ apply auto []
apply metis
done
next
@@ -1523,7 +1531,7 @@
(\<forall>x i. P x \<and> Q i \<and> l x i = 1 \<longrightarrow> f x i \<le> x i)"
unfolding all_conj_distrib [symmetric]
apply (subst choice_iff[symmetric])+
- by (metis assms bot_nat_0.extremum nle_le zero_neq_one)
+ by (metis assms choice_iff bot_nat_0.extremum nle_le zero_neq_one)
subsection \<open>Brouwer's fixed point theorem\<close>
@@ -1543,10 +1551,8 @@
by auto
obtain d where
d: "d > 0" "\<And>x. x \<in> cbox 0 One \<Longrightarrow> d \<le> norm (f x - x)"
- apply (rule brouwer_compactness_lemma[OF compact_cbox _ *])
- apply (rule continuous_intros assms)+
- apply blast
- done
+ using brouwer_compactness_lemma[OF compact_cbox _ *] assms
+ by (metis (no_types, lifting) continuous_on_cong continuous_on_diff continuous_on_id)
have *: "\<forall>x. x \<in> cbox 0 One \<longrightarrow> f x \<in> cbox 0 One"
"\<forall>x. x \<in> (cbox 0 One::'a set) \<longrightarrow> (\<forall>i\<in>Basis. True \<longrightarrow> 0 \<le> x \<bullet> i \<and> x \<bullet> i \<le> 1)"
using assms(2)[unfolded image_subset_iff Ball_def]
@@ -1581,8 +1587,7 @@
case False
then show ?thesis
using label [OF \<open>i \<in> Basis\<close>] i(1) x y
- apply (auto simp: inner_diff_left le_Suc_eq)
- by (metis "*")
+ by (smt (verit, ccfv_threshold) inner_diff_left less_one order_le_less)
qed
also have "\<dots> \<le> norm (f y - f x) + norm (y - x)"
by (simp add: add_mono i(2) norm_bound_Basis_le)
@@ -1980,9 +1985,8 @@
then obtain a where "a \<in> S" "a \<notin> T" by blast
define g where "g \<equiv> \<lambda>z. if z \<in> closure S then f z else z"
have "continuous_on (closure S \<union> closure(-S)) g"
- unfolding g_def
- apply (rule continuous_on_cases)
- using fros fid frontier_closures by (auto simp: contf)
+ unfolding g_def using fros fid frontier_closures
+ by (intro continuous_on_cases) (auto simp: contf)
moreover have "closure S \<union> closure(- S) = UNIV"
using closure_Un by fastforce
ultimately have contg: "continuous_on UNIV g" by metis
@@ -2027,10 +2031,8 @@
proof -
have "\<exists>d. 0 < d \<and> (a + d *\<^sub>R l) \<in> rel_frontier S \<and>
(\<forall>e. 0 \<le> e \<and> e < d \<longrightarrow> (a + e *\<^sub>R l) \<in> rel_interior S)"
- if "(a + l) \<in> affine hull S" "l \<noteq> 0" for l
- apply (rule ray_to_rel_frontier [OF \<open>bounded S\<close> arelS])
- apply (rule that)+
- by metis
+ if "(a + l) \<in> affine hull S" "l \<noteq> 0" for l
+ using ray_to_rel_frontier [OF \<open>bounded S\<close> arelS] that by metis
then obtain dd
where dd1: "\<And>l. \<lbrakk>(a + l) \<in> affine hull S; l \<noteq> 0\<rbrakk> \<Longrightarrow> 0 < dd l \<and> (a + dd l *\<^sub>R l) \<in> rel_frontier S"
and dd2: "\<And>l e. \<lbrakk>(a + l) \<in> affine hull S; e < dd l; 0 \<le> e; l \<noteq> 0\<rbrakk>
@@ -2071,11 +2073,11 @@
then have "0 < dd x" and inS: "a + dd x *\<^sub>R x \<in> rel_frontier S"
using dd1 by auto
moreover have "a + dd x *\<^sub>R x \<in> open_segment a (a + k *\<^sub>R x)"
- using k \<open>x \<noteq> 0\<close> \<open>0 < dd x\<close>
- apply (simp add: in_segment)
- apply (rule_tac x = "dd x / k" in exI)
- apply (simp add: that vector_add_divide_simps algebra_simps)
- done
+ unfolding in_segment
+ proof (intro conjI exI)
+ show "a + dd x *\<^sub>R x = (1 - dd x / k) *\<^sub>R a + (dd x / k) *\<^sub>R (a + k *\<^sub>R x)"
+ using k by (simp add: that algebra_simps)
+ qed (use \<open>x \<noteq> 0\<close> \<open>0 < dd x\<close> that in auto)
ultimately show ?thesis
using segsub by (auto simp: rel_frontier_def)
qed
@@ -2094,47 +2096,45 @@
by (blast intro: continuous_on_subset)
show ?thesis
proof
- show "homotopic_with_canon (\<lambda>x. True) (T - {a}) (T - {a}) id (\<lambda>x. a + dd (x - a) *\<^sub>R (x - a))"
+ show "homotopic_with_canon (\<lambda>x. True) (T - {a}) (T - {a}) id (\<lambda>x. a + dd (x-a) *\<^sub>R (x-a))"
proof (rule homotopic_with_linear)
show "continuous_on (T - {a}) id"
by (intro continuous_intros continuous_on_compose)
- show "continuous_on (T - {a}) (\<lambda>x. a + dd (x - a) *\<^sub>R (x - a))"
+ show "continuous_on (T - {a}) (\<lambda>x. a + dd (x-a) *\<^sub>R (x-a))"
using contdd by (simp add: o_def)
- show "closed_segment (id x) (a + dd (x - a) *\<^sub>R (x - a)) \<subseteq> T - {a}"
+ show "closed_segment (id x) (a + dd (x-a) *\<^sub>R (x-a)) \<subseteq> T - {a}"
if "x \<in> T - {a}" for x
proof (clarsimp simp: in_segment, intro conjI)
fix u::real assume u: "0 \<le> u" "u \<le> 1"
- have "a + dd (x - a) *\<^sub>R (x - a) \<in> T"
+ have "a + dd (x-a) *\<^sub>R (x-a) \<in> T"
by (metis DiffD1 DiffD2 add.commute add.right_neutral affS dd1 diff_add_cancel relS singletonI subsetCE that)
- then show "(1 - u) *\<^sub>R x + u *\<^sub>R (a + dd (x - a) *\<^sub>R (x - a)) \<in> T"
+ then show "(1 - u) *\<^sub>R x + u *\<^sub>R (a + dd (x-a) *\<^sub>R (x-a)) \<in> T"
using convexD [OF \<open>convex T\<close>] that u by simp
- have iff: "(1 - u) *\<^sub>R x + u *\<^sub>R (a + d *\<^sub>R (x - a)) = a \<longleftrightarrow>
- (1 - u + u * d) *\<^sub>R (x - a) = 0" for d
+ have iff: "(1 - u) *\<^sub>R x + u *\<^sub>R (a + d *\<^sub>R (x-a)) = a \<longleftrightarrow>
+ (1 - u + u * d) *\<^sub>R (x-a) = 0" for d
by (auto simp: algebra_simps)
have "x \<in> T" "x \<noteq> a" using that by auto
- then have axa: "a + (x - a) \<in> affine hull S"
+ then have axa: "a + (x-a) \<in> affine hull S"
by (metis (no_types) add.commute affS diff_add_cancel rev_subsetD)
- then have "\<not> dd (x - a) \<le> 0 \<and> a + dd (x - a) *\<^sub>R (x - a) \<in> rel_frontier S"
+ then have "\<not> dd (x-a) \<le> 0 \<and> a + dd (x-a) *\<^sub>R (x-a) \<in> rel_frontier S"
using \<open>x \<noteq> a\<close> dd1 by fastforce
- with \<open>x \<noteq> a\<close> show "(1 - u) *\<^sub>R x + u *\<^sub>R (a + dd (x - a) *\<^sub>R (x - a)) \<noteq> a"
+ with \<open>x \<noteq> a\<close> show "(1 - u) *\<^sub>R x + u *\<^sub>R (a + dd (x-a) *\<^sub>R (x-a)) \<noteq> a"
using less_eq_real_def mult_le_0_iff not_less u by (fastforce simp: iff)
qed
qed
- show "retraction (T - {a}) (rel_frontier S) (\<lambda>x. a + dd (x - a) *\<^sub>R (x - a))"
+ show "retraction (T - {a}) (rel_frontier S) (\<lambda>x. a + dd (x-a) *\<^sub>R (x-a))"
proof (simp add: retraction_def, intro conjI ballI)
show "rel_frontier S \<subseteq> T - {a}"
using arelS relS rel_frontier_def by fastforce
- show "continuous_on (T - {a}) (\<lambda>x. a + dd (x - a) *\<^sub>R (x - a))"
+ show "continuous_on (T - {a}) (\<lambda>x. a + dd (x-a) *\<^sub>R (x-a))"
using contdd by (simp add: o_def)
- show "(\<lambda>x. a + dd (x - a) *\<^sub>R (x - a)) \<in> (T - {a}) \<rightarrow> rel_frontier S"
- apply (auto simp: rel_frontier_def)
- apply (metis Diff_subset add.commute affS dd1 diff_add_cancel eq_iff_diff_eq_0 rel_frontier_def subset_iff)
- by (metis DiffE add.commute affS dd1 diff_add_cancel eq_iff_diff_eq_0 rel_frontier_def rev_subsetD)
- show "a + dd (x - a) *\<^sub>R (x - a) = x" if x: "x \<in> rel_frontier S" for x
+ show "(\<lambda>x. a + dd (x-a) *\<^sub>R (x-a)) \<in> (T - {a}) \<rightarrow> rel_frontier S"
+ unfolding Pi_iff using affS dd1 subset_eq by force
+ show "a + dd (x-a) *\<^sub>R (x-a) = x" if x: "x \<in> rel_frontier S" for x
proof -
have "x \<noteq> a"
using that arelS by (auto simp: rel_frontier_def)
- have False if "dd (x - a) < 1"
+ have False if "dd (x-a) < 1"
proof -
have "x \<in> closure S"
using x by (auto simp: rel_frontier_def)
@@ -2142,21 +2142,21 @@
by (metis rel_interior_closure_convex_segment [OF \<open>convex S\<close> arelS])
have xaffS: "x \<in> affine hull S"
using affS relS x by auto
- then have "0 < dd (x - a)" and inS: "a + dd (x - a) *\<^sub>R (x - a) \<in> rel_frontier S"
+ then have "0 < dd (x-a)" and inS: "a + dd (x-a) *\<^sub>R (x-a) \<in> rel_frontier S"
using dd1 by (auto simp: \<open>x \<noteq> a\<close>)
- moreover have "a + dd (x - a) *\<^sub>R (x - a) \<in> open_segment a x"
- using \<open>x \<noteq> a\<close> \<open>0 < dd (x - a)\<close>
- apply (simp add: in_segment)
- apply (rule_tac x = "dd (x - a)" in exI)
- apply (simp add: algebra_simps that)
- done
+ moreover have "a + dd (x-a) *\<^sub>R (x-a) \<in> open_segment a x"
+ unfolding in_segment
+ proof (intro exI conjI)
+ show "a + dd (x-a) *\<^sub>R (x-a) = (1 - dd (x-a)) *\<^sub>R a + (dd (x-a)) *\<^sub>R x"
+ by (simp add: algebra_simps)
+ qed (use \<open>x \<noteq> a\<close> \<open>0 < dd (x-a)\<close> that in auto)
ultimately show ?thesis
using segsub by (auto simp: rel_frontier_def)
qed
- moreover have False if "1 < dd (x - a)"
+ moreover have False if "1 < dd (x-a)"
using x that dd2 [of "x - a" 1] \<open>x \<noteq> a\<close> closure_affine_hull
by (auto simp: rel_frontier_def)
- ultimately have "dd (x - a) = 1" \<comment> \<open>similar to another proof above\<close>
+ ultimately have "dd (x-a) = 1" \<comment> \<open>similar to another proof above\<close>
by fastforce
with that show ?thesis
by (simp add: rel_frontier_def)
@@ -2211,13 +2211,13 @@
subsubsection\<open>Borsuk-style characterization of separation\<close>
lemma continuous_on_Borsuk_map:
- "a \<notin> S \<Longrightarrow> continuous_on S (\<lambda>x. inverse(norm (x - a)) *\<^sub>R (x - a))"
+ "a \<notin> S \<Longrightarrow> continuous_on S (\<lambda>x. inverse(norm (x-a)) *\<^sub>R (x-a))"
by (rule continuous_intros | force)+
lemma Borsuk_map_into_sphere:
- "(\<lambda>x. inverse(norm (x - a)) *\<^sub>R (x - a)) \<in> S \<rightarrow> sphere 0 1 \<longleftrightarrow> (a \<notin> S)"
+ "(\<lambda>x. inverse(norm (x-a)) *\<^sub>R (x-a)) \<in> S \<rightarrow> sphere 0 1 \<longleftrightarrow> (a \<notin> S)"
proof -
- have "\<And>x. \<lbrakk>a \<notin> S; x \<in> S\<rbrakk> \<Longrightarrow> inverse (norm (x - a)) * norm (x - a) = 1"
+ have "\<And>x. \<lbrakk>a \<notin> S; x \<in> S\<rbrakk> \<Longrightarrow> inverse (norm (x-a)) * norm (x-a) = 1"
by (metis left_inverse norm_eq_zero right_minus_eq)
then show ?thesis
by force
@@ -2226,16 +2226,19 @@
lemma Borsuk_maps_homotopic_in_path_component:
assumes "path_component (- S) a b"
shows "homotopic_with_canon (\<lambda>x. True) S (sphere 0 1)
- (\<lambda>x. inverse(norm(x - a)) *\<^sub>R (x - a))
+ (\<lambda>x. inverse(norm(x-a)) *\<^sub>R (x-a))
(\<lambda>x. inverse(norm(x - b)) *\<^sub>R (x - b))"
proof -
- obtain g where "path g" "path_image g \<subseteq> -S" "pathstart g = a" "pathfinish g = b"
+ obtain g where g: "path g" "path_image g \<subseteq> -S" "pathstart g = a" "pathfinish g = b"
using assms by (auto simp: path_component_def)
- then show ?thesis
- apply (simp add: path_def path_image_def pathstart_def pathfinish_def homotopic_with_def)
- apply (rule_tac x = "\<lambda>z. inverse(norm(snd z - (g \<circ> fst)z)) *\<^sub>R (snd z - (g \<circ> fst)z)" in exI)
- apply (rule conjI continuous_intros | erule continuous_on_subset | fastforce simp: divide_simps sphere_def)+
- done
+ define h where "h \<equiv> \<lambda>z. (snd z - (g \<circ> fst) z) /\<^sub>R norm (snd z - (g \<circ> fst) z)"
+ have "continuous_on ({0..1} \<times> S) h"
+ unfolding h_def using g by (intro continuous_intros) (auto simp: path_defs)
+ moreover
+ have "h ` ({0..1} \<times> S) \<subseteq> sphere 0 1"
+ unfolding h_def using g by (auto simp: divide_simps path_defs)
+ ultimately show ?thesis
+ using g by (auto simp: h_def path_defs homotopic_with_def)
qed
lemma non_extensible_Borsuk_map:
@@ -2243,7 +2246,7 @@
assumes "compact S" and cin: "C \<in> components(- S)" and boc: "bounded C" and "a \<in> C"
shows "\<not> (\<exists>g. continuous_on (S \<union> C) g \<and>
g \<in> (S \<union> C) \<rightarrow> sphere 0 1 \<and>
- (\<forall>x \<in> S. g x = inverse(norm(x - a)) *\<^sub>R (x - a)))"
+ (\<forall>x \<in> S. g x = inverse(norm(x-a)) *\<^sub>R (x-a)))"
proof -
have "closed S" using assms by (simp add: compact_imp_closed)
have "C \<subseteq> -S"
@@ -2258,7 +2261,7 @@
{ fix g
assume "continuous_on (S \<union> C) g"
"g \<in> (S \<union> C) \<rightarrow> sphere 0 1"
- and [simp]: "\<And>x. x \<in> S \<Longrightarrow> g x = (x - a) /\<^sub>R norm (x - a)"
+ and [simp]: "\<And>x. x \<in> S \<Longrightarrow> g x = (x-a) /\<^sub>R norm (x-a)"
then have norm_g1[simp]: "\<And>x. x \<in> S \<union> C \<Longrightarrow> norm (g x) = 1"
by force
have cb_eq: "cball a r = (S \<union> connected_component_set (- S) a) \<union>
@@ -2269,12 +2272,12 @@
using \<open>continuous_on (S \<union> C) g\<close> ceq
by (intro continuous_intros) blast
have cont2: "continuous_on (cball a r - connected_component_set (- S) a)
- (\<lambda>x. a + r *\<^sub>R ((x - a) /\<^sub>R norm (x - a)))"
+ (\<lambda>x. a + r *\<^sub>R ((x-a) /\<^sub>R norm (x-a)))"
by (rule continuous_intros | force simp: \<open>a \<notin> S\<close>)+
have 1: "continuous_on (cball a r)
(\<lambda>x. if connected_component (- S) a x
then a + r *\<^sub>R g x
- else a + r *\<^sub>R ((x - a) /\<^sub>R norm (x - a)))"
+ else a + r *\<^sub>R ((x-a) /\<^sub>R norm (x-a)))"
apply (subst cb_eq)
apply (rule continuous_on_cases [OF _ _ cont1 cont2])
using \<open>closed S\<close> ceq cin
@@ -2285,7 +2288,7 @@
have "retraction (cball a r) (sphere a r)
(\<lambda>x. if x \<in> connected_component_set (- S) a
then a + r *\<^sub>R g x
- else a + r *\<^sub>R ((x - a) /\<^sub>R norm (x - a)))"
+ else a + r *\<^sub>R ((x-a) /\<^sub>R norm (x-a)))"
using \<open>0 < r\<close> \<open>a \<notin> S\<close> \<open>a \<in> C\<close> r
by (auto simp: norm_minus_commute retraction_def Pi_iff ceq dist_norm abs_if
mult_less_0_iff divide_simps 1 2)
@@ -2294,7 +2297,7 @@
[OF \<open>0 < r\<close>, of a, unfolded retract_of_def, simplified, rule_format,
of "\<lambda>x. if x \<in> connected_component_set (- S) a
then a + r *\<^sub>R g x
- else a + r *\<^sub>R inverse(norm(x - a)) *\<^sub>R (x - a)"]
+ else a + r *\<^sub>R inverse(norm(x-a)) *\<^sub>R (x-a)"]
by blast
}
then show ?thesis
@@ -2305,10 +2308,8 @@
lemma brouwer_surjective:
fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
- assumes "compact T"
- and "convex T"
- and "T \<noteq> {}"
- and "continuous_on T f"
+ assumes T: "compact T" "convex T" "T \<noteq> {}"
+ and f: "continuous_on T f"
and "\<And>x y. \<lbrakk>x\<in>S; y\<in>T\<rbrakk> \<Longrightarrow> x + (y - f y) \<in> T"
and "x \<in> S"
shows "\<exists>y\<in>T. f y = x"
@@ -2317,11 +2318,10 @@
by (auto simp add: algebra_simps)
show ?thesis
unfolding *
- apply (rule brouwer[OF assms(1-3), of "\<lambda>y. x + (y - f y)"])
- apply (intro continuous_intros)
- using assms
- apply auto
- done
+ proof (rule brouwer[OF T])
+ show "continuous_on T (\<lambda>y. x + (y - f y))"
+ by (intro continuous_intros f)
+ qed (use assms in auto)
qed
lemma brouwer_surjective_cball:
--- a/src/HOL/Library/Groups_Big_Fun.thy Fri Apr 12 10:10:16 2024 +0200
+++ b/src/HOL/Library/Groups_Big_Fun.thy Fri Apr 12 09:58:53 2024 +0100
@@ -22,19 +22,14 @@
lemma expand_superset:
assumes "finite A" and "{a. g a \<noteq> \<^bold>1} \<subseteq> A"
shows "G g = F.F g A"
- apply (simp add: expand_set)
- apply (rule F.same_carrierI [of A])
- apply (simp_all add: assms)
- done
+ using F.mono_neutral_right assms expand_set by fastforce
lemma conditionalize:
assumes "finite A"
shows "F.F g A = G (\<lambda>a. if a \<in> A then g a else \<^bold>1)"
using assms
- apply (simp add: expand_set)
- apply (rule F.same_carrierI [of A])
- apply auto
- done
+ by (smt (verit, ccfv_threshold) Diff_iff F.mono_neutral_cong_right expand_set mem_Collect_eq subsetI)
+
lemma neutral [simp]:
"G (\<lambda>a. \<^bold>1) = \<^bold>1"
@@ -140,30 +135,13 @@
by (auto simp add: finite_cartesian_product_iff)
have *: "G (\<lambda>a. G (g a)) =
(F.F (\<lambda>a. F.F (g a) {b. \<exists>a. g a b \<noteq> \<^bold>1}) {a. \<exists>b. g a b \<noteq> \<^bold>1})"
- apply (subst expand_superset [of "?B"])
- apply (rule \<open>finite ?B\<close>)
- apply auto
- apply (subst expand_superset [of "?A"])
- apply (rule \<open>finite ?A\<close>)
- apply auto
- apply (erule F.not_neutral_contains_not_neutral)
- apply auto
- done
- have "{p. (case p of (a, b) \<Rightarrow> g a b) \<noteq> \<^bold>1} \<subseteq> ?A \<times> ?B"
+ using \<open>finite ?A\<close> \<open>finite ?B\<close> expand_superset
+ by (smt (verit, del_insts) Collect_mono local.cong not_neutral_obtains_not_neutral)
+ have **: "{p. (case p of (a, b) \<Rightarrow> g a b) \<noteq> \<^bold>1} \<subseteq> ?A \<times> ?B"
by auto
- with subset have **: "{p. (case p of (a, b) \<Rightarrow> g a b) \<noteq> \<^bold>1} \<subseteq> C"
- by blast
show ?thesis
- apply (simp add: *)
- apply (simp add: F.cartesian_product)
- apply (subst expand_superset [of C])
- apply (rule \<open>finite C\<close>)
- apply (simp_all add: **)
- apply (rule F.same_carrierI [of C])
- apply (rule \<open>finite C\<close>)
- apply (simp_all add: subset)
- apply auto
- done
+ using \<open>finite C\<close> expand_superset
+ using "*" ** F.cartesian_product fin_prod by force
qed
lemma cartesian_product2:
@@ -231,37 +209,23 @@
fixes r :: "'a :: semiring_0"
assumes "finite {a. g a \<noteq> 0}"
shows "Sum_any g * r = (\<Sum>n. g n * r)"
-proof -
- note assms
- moreover have "{a. g a * r \<noteq> 0} \<subseteq> {a. g a \<noteq> 0}" by auto
- ultimately show ?thesis
- by (simp add: sum_distrib_right Sum_any.expand_superset [of "{a. g a \<noteq> 0}"])
-qed
+ by (metis (mono_tags, lifting) Collect_mono Sum_any.expand_superset assms mult_zero_left sum_distrib_right)
lemma Sum_any_right_distrib:
fixes r :: "'a :: semiring_0"
assumes "finite {a. g a \<noteq> 0}"
shows "r * Sum_any g = (\<Sum>n. r * g n)"
-proof -
- note assms
- moreover have "{a. r * g a \<noteq> 0} \<subseteq> {a. g a \<noteq> 0}" by auto
- ultimately show ?thesis
- by (simp add: sum_distrib_left Sum_any.expand_superset [of "{a. g a \<noteq> 0}"])
-qed
+ by (metis (mono_tags, lifting) Collect_mono Sum_any.expand_superset assms mult_zero_right sum_distrib_left)
lemma Sum_any_product:
fixes f g :: "'b \<Rightarrow> 'a::semiring_0"
assumes "finite {a. f a \<noteq> 0}" and "finite {b. g b \<noteq> 0}"
shows "Sum_any f * Sum_any g = (\<Sum>a. \<Sum>b. f a * g b)"
proof -
- have subset_f: "{a. (\<Sum>b. f a * g b) \<noteq> 0} \<subseteq> {a. f a \<noteq> 0}"
- by rule (simp, rule, auto)
- moreover have subset_g: "\<And>a. {b. f a * g b \<noteq> 0} \<subseteq> {b. g b \<noteq> 0}"
- by rule (simp, rule, auto)
- ultimately show ?thesis using assms
- by (auto simp add: Sum_any.expand_set [of f] Sum_any.expand_set [of g]
- Sum_any.expand_superset [of "{a. f a \<noteq> 0}"] Sum_any.expand_superset [of "{b. g b \<noteq> 0}"]
- sum_product)
+ have "\<forall>a. (\<Sum>b. a * g b) = a * Sum_any g"
+ by (simp add: Sum_any_right_distrib assms(2))
+ then show ?thesis
+ by (simp add: Sum_any_left_distrib assms(1))
qed
lemma Sum_any_eq_zero_iff [simp]:
--- a/src/HOL/Library/Multiset.thy Fri Apr 12 10:10:16 2024 +0200
+++ b/src/HOL/Library/Multiset.thy Fri Apr 12 09:58:53 2024 +0100
@@ -559,10 +559,7 @@
lemma mset_subset_eq_exists_conv: "(A::'a multiset) \<subseteq># B \<longleftrightarrow> (\<exists>C. B = A + C)"
unfolding subseteq_mset_def
- apply (rule iffI)
- apply (rule exI [where x = "B - A"])
- apply (auto intro: multiset_eq_iff [THEN iffD2])
- done
+ by (metis add_diff_cancel_left' count_diff count_union le_Suc_ex le_add_same_cancel1 multiset_eq_iff zero_le)
interpretation subset_mset: ordered_cancel_comm_monoid_diff "(+)" 0 "(\<subseteq>#)" "(\<subset>#)" "(-)"
by standard (simp, fact mset_subset_eq_exists_conv)
@@ -629,14 +626,18 @@
by (metis mset_subset_eqD subsetI)
lemma mset_subset_eq_insertD:
- "add_mset x A \<subseteq># B \<Longrightarrow> x \<in># B \<and> A \<subset># B"
-apply (rule conjI)
- apply (simp add: mset_subset_eqD)
- apply (clarsimp simp: subset_mset_def subseteq_mset_def)
- apply safe
- apply (erule_tac x = a in allE)
- apply (auto split: if_split_asm)
-done
+ assumes "add_mset x A \<subseteq># B"
+ shows "x \<in># B \<and> A \<subset># B"
+proof
+ show "x \<in># B"
+ using assms by (simp add: mset_subset_eqD)
+ have "A \<subseteq># add_mset x A"
+ by (metis (no_types) add_mset_add_single mset_subset_eq_add_left)
+ then have "A \<subset># add_mset x A"
+ by (meson multi_self_add_other_not_self subset_mset.le_imp_less_or_eq)
+ then show "A \<subset># B"
+ using assms subset_mset.strict_trans2 by blast
+qed
lemma mset_subset_insertD:
"add_mset x A \<subset># B \<Longrightarrow> x \<in># B \<and> A \<subset># B"
@@ -653,11 +654,7 @@
lemma insert_subset_eq_iff:
"add_mset a A \<subseteq># B \<longleftrightarrow> a \<in># B \<and> A \<subseteq># B - {#a#}"
- using le_diff_conv2 [of "Suc 0" "count B a" "count A a"]
- apply (auto simp add: subseteq_mset_def not_in_iff Suc_le_eq)
- apply (rule ccontr)
- apply (auto simp add: not_in_iff)
- done
+ using mset_subset_eq_insertD subset_mset.le_diff_conv2 by fastforce
lemma insert_union_subset_iff:
"add_mset a A \<subset># B \<longleftrightarrow> a \<in># B \<and> A \<subset># B - {#a#}"
@@ -723,11 +720,12 @@
by (simp add: union_mset_def)
global_interpretation subset_mset: semilattice_neutr_order \<open>(\<union>#)\<close> \<open>{#}\<close> \<open>(\<supseteq>#)\<close> \<open>(\<supset>#)\<close>
- apply standard
- apply (simp_all add: multiset_eq_iff subseteq_mset_def subset_mset_def max_def)
- apply (auto simp add: le_antisym dest: sym)
- apply (metis nat_le_linear)+
- done
+proof
+ show "\<And>a b. (b \<subseteq># a) = (a = a \<union># b)"
+ by (simp add: Diff_eq_empty_iff_mset union_mset_def)
+ show "\<And>a b. (b \<subset># a) = (a = a \<union># b \<and> a \<noteq> b)"
+ by (metis Diff_eq_empty_iff_mset add_cancel_left_right subset_mset_def union_mset_def)
+qed (auto simp: multiset_eqI union_mset_def)
interpretation subset_mset: semilattice_sup \<open>(\<union>#)\<close> \<open>(\<subseteq>#)\<close> \<open>(\<subset>#)\<close>
proof -
@@ -774,30 +772,8 @@
qed
lemma disjunct_not_in:
- "A \<inter># B = {#} \<longleftrightarrow> (\<forall>a. a \<notin># A \<or> a \<notin># B)" (is "?P \<longleftrightarrow> ?Q")
-proof
- assume ?P
- show ?Q
- proof
- fix a
- from \<open>?P\<close> have "min (count A a) (count B a) = 0"
- by (simp add: multiset_eq_iff)
- then have "count A a = 0 \<or> count B a = 0"
- by (cases "count A a \<le> count B a") (simp_all add: min_def)
- then show "a \<notin># A \<or> a \<notin># B"
- by (simp add: not_in_iff)
- qed
-next
- assume ?Q
- show ?P
- proof (rule multiset_eqI)
- fix a
- from \<open>?Q\<close> have "count A a = 0 \<or> count B a = 0"
- by (auto simp add: not_in_iff)
- then show "count (A \<inter># B) a = count {#} a"
- by auto
- qed
-qed
+ "A \<inter># B = {#} \<longleftrightarrow> (\<forall>a. a \<notin># A \<or> a \<notin># B)"
+ by (metis disjoint_iff set_mset_eq_empty_iff set_mset_inter)
lemma inter_mset_empty_distrib_right: "A \<inter># (B + C) = {#} \<longleftrightarrow> A \<inter># B = {#} \<and> A \<inter># C = {#}"
by (meson disjunct_not_in union_iff)
@@ -1148,15 +1124,7 @@
fix X :: "'a multiset" and A
assume "X \<in> A"
show "Inf A \<subseteq># X"
- proof (rule mset_subset_eqI)
- fix x
- from \<open>X \<in> A\<close> have "A \<noteq> {}" by auto
- hence "count (Inf A) x = (INF X\<in>A. count X x)"
- by (simp add: count_Inf_multiset_nonempty)
- also from \<open>X \<in> A\<close> have "\<dots> \<le> count X x"
- by (intro cInf_lower) simp_all
- finally show "count (Inf A) x \<le> count X x" .
- qed
+ by (metis \<open>X \<in> A\<close> count_Inf_multiset_nonempty empty_iff image_eqI mset_subset_eqI wellorder_Inf_le1)
next
fix X :: "'a multiset" and A
assume nonempty: "A \<noteq> {}" and le: "\<And>Y. Y \<in> A \<Longrightarrow> X \<subseteq># Y"
@@ -1240,8 +1208,7 @@
using that by (auto simp: subseteq_mset_def algebra_simps not_in_iff)
hence "Sup A \<subseteq># Sup A - {#x#}" by (intro subset_mset.cSup_least nonempty)
with \<open>x \<in># Sup A\<close> show False
- by (auto simp: subseteq_mset_def simp flip: count_greater_zero_iff
- dest!: spec[of _ x])
+ using mset_subset_diff_self by fastforce
qed
next
fix x X assume "x \<in> set_mset X" "X \<in> A"
@@ -1253,20 +1220,12 @@
lemma in_Sup_multiset_iff:
assumes "subset_mset.bdd_above A"
shows "x \<in># Sup A \<longleftrightarrow> (\<exists>X\<in>A. x \<in># X)"
-proof -
- from assms have "set_mset (Sup A) = (\<Union>X\<in>A. set_mset X)" by (rule set_mset_Sup)
- also have "x \<in> \<dots> \<longleftrightarrow> (\<exists>X\<in>A. x \<in># X)" by simp
- finally show ?thesis .
-qed
+ by (simp add: assms set_mset_Sup)
lemma in_Sup_multisetD:
assumes "x \<in># Sup A"
shows "\<exists>X\<in>A. x \<in># X"
-proof -
- have "subset_mset.bdd_above A"
- by (rule ccontr) (insert assms, simp_all add: Sup_multiset_unbounded)
- with assms show ?thesis by (simp add: in_Sup_multiset_iff)
-qed
+ using Sup_multiset_unbounded assms in_Sup_multiset_iff by fastforce
interpretation subset_mset: distrib_lattice "(\<inter>#)" "(\<subseteq>#)" "(\<subset>#)" "(\<union>#)"
proof
@@ -1328,11 +1287,7 @@
lemma multiset_filter_mono:
assumes "A \<subseteq># B"
shows "filter_mset f A \<subseteq># filter_mset f B"
-proof -
- from assms[unfolded mset_subset_eq_exists_conv]
- obtain C where B: "B = A + C" by auto
- show ?thesis unfolding B by auto
-qed
+ by (metis assms filter_sup_mset subset_mset.order_iff)
lemma filter_mset_eq_conv:
"filter_mset P M = N \<longleftrightarrow> N \<subseteq># M \<and> (\<forall>b\<in>#N. P b) \<and> (\<forall>a\<in>#M - N. \<not> P a)" (is "?P \<longleftrightarrow> ?Q")
@@ -1421,16 +1376,16 @@
size_multiset_overloaded_def[THEN fun_cong, unfolded size_multiset_eq, simplified]
lemma size_multiset_empty [simp]: "size_multiset f {#} = 0"
-by (simp add: size_multiset_def)
+ by (simp add: size_multiset_def)
lemma size_empty [simp]: "size {#} = 0"
-by (simp add: size_multiset_overloaded_def)
+ by (simp add: size_multiset_overloaded_def)
lemma size_multiset_single : "size_multiset f {#b#} = Suc (f b)"
-by (simp add: size_multiset_eq)
+ by (simp add: size_multiset_eq)
lemma size_single: "size {#b#} = 1"
-by (simp add: size_multiset_overloaded_def size_multiset_single)
+ by (simp add: size_multiset_overloaded_def size_multiset_single)
lemma sum_wcount_Int:
"finite A \<Longrightarrow> sum (wcount f N) (A \<inter> set_mset N) = sum (wcount f N) A"
@@ -1439,20 +1394,18 @@
lemma size_multiset_union [simp]:
"size_multiset f (M + N::'a multiset) = size_multiset f M + size_multiset f N"
-apply (simp add: size_multiset_def sum_Un_nat sum.distrib sum_wcount_Int wcount_union)
-apply (subst Int_commute)
-apply (simp add: sum_wcount_Int)
-done
+ apply (simp add: size_multiset_def sum_Un_nat sum.distrib sum_wcount_Int wcount_union)
+ by (metis add_implies_diff finite_set_mset inf.commute sum_wcount_Int)
lemma size_multiset_add_mset [simp]:
"size_multiset f (add_mset a M) = Suc (f a) + size_multiset f M"
- unfolding add_mset_add_single[of _ M] size_multiset_union by (auto simp: size_multiset_single)
+ by (metis add.commute add_mset_add_single size_multiset_single size_multiset_union)
lemma size_add_mset [simp]: "size (add_mset a A) = Suc (size A)"
-by (simp add: size_multiset_overloaded_def wcount_add_mset)
+ by (simp add: size_multiset_overloaded_def wcount_add_mset)
lemma size_union [simp]: "size (M + N::'a multiset) = size M + size N"
-by (auto simp add: size_multiset_overloaded_def)
+ by (auto simp add: size_multiset_overloaded_def)
lemma size_multiset_eq_0_iff_empty [iff]:
"size_multiset f M = 0 \<longleftrightarrow> M = {#}"
@@ -1462,23 +1415,15 @@
by (auto simp add: size_multiset_overloaded_def)
lemma nonempty_has_size: "(S \<noteq> {#}) = (0 < size S)"
-by (metis gr0I gr_implies_not0 size_empty size_eq_0_iff_empty)
+ by (metis gr0I gr_implies_not0 size_empty size_eq_0_iff_empty)
lemma size_eq_Suc_imp_elem: "size M = Suc n \<Longrightarrow> \<exists>a. a \<in># M"
-apply (unfold size_multiset_overloaded_eq)
-apply (drule sum_SucD)
-apply auto
-done
+ using all_not_in_conv by fastforce
lemma size_eq_Suc_imp_eq_union:
assumes "size M = Suc n"
shows "\<exists>a N. M = add_mset a N"
-proof -
- from assms obtain a where "a \<in># M"
- by (erule size_eq_Suc_imp_elem [THEN exE])
- then have "M = add_mset a (M - {#a#})" by simp
- then show ?thesis by blast
-qed
+ by (metis assms insert_DiffM size_eq_Suc_imp_elem)
lemma size_mset_mono:
fixes A B :: "'a multiset"
@@ -1491,7 +1436,7 @@
qed
lemma size_filter_mset_lesseq[simp]: "size (filter_mset f M) \<le> size M"
-by (rule size_mset_mono[OF multiset_filter_subset])
+ by (rule size_mset_mono[OF multiset_filter_subset])
lemma size_Diff_submset:
"M \<subseteq># M' \<Longrightarrow> size (M' - M) = size M' - size(M::'a multiset)"
@@ -1560,22 +1505,21 @@
qed (simp add: empty)
lemma multi_nonempty_split: "M \<noteq> {#} \<Longrightarrow> \<exists>A a. M = add_mset a A"
-by (induct M) auto
+ by (induct M) auto
lemma multiset_cases [cases type]:
- obtains (empty) "M = {#}"
- | (add) x N where "M = add_mset x N"
+ obtains (empty) "M = {#}" | (add) x N where "M = add_mset x N"
by (induct M) simp_all
lemma multi_drop_mem_not_eq: "c \<in># B \<Longrightarrow> B - {#c#} \<noteq> B"
-by (cases "B = {#}") (auto dest: multi_member_split)
+ by (cases "B = {#}") (auto dest: multi_member_split)
lemma union_filter_mset_complement[simp]:
"\<forall>x. P x = (\<not> Q x) \<Longrightarrow> filter_mset P M + filter_mset Q M = M"
-by (subst multiset_eq_iff) auto
+ by (subst multiset_eq_iff) auto
lemma multiset_partition: "M = {#x \<in># M. P x#} + {#x \<in># M. \<not> P x#}"
-by simp
+ by simp
lemma mset_subset_size: "A \<subset># B \<Longrightarrow> size A < size B"
proof (induct A arbitrary: B)
@@ -1587,8 +1531,7 @@
have "add_mset x A \<subseteq># B"
by (meson add.prems subset_mset_def)
then show ?case
- by (metis (no_types) add.prems add.right_neutral add_diff_cancel_left' leD nat_neq_iff
- size_Diff_submset size_eq_0_iff_empty size_mset_mono subset_mset.le_iff_add subset_mset_def)
+ using add.prems subset_mset.less_eqE by fastforce
qed
lemma size_1_singleton_mset: "size M = 1 \<Longrightarrow> \<exists>a. M = {#a#}"
@@ -1605,19 +1548,17 @@
text \<open>Well-foundedness of strict subset relation\<close>
lemma wf_subset_mset_rel: "wf {(M, N :: 'a multiset). M \<subset># N}"
-apply (rule wf_measure [THEN wf_subset, where f1=size])
-apply (clarsimp simp: measure_def inv_image_def mset_subset_size)
-done
+ using mset_subset_size wfP_def wfP_if_convertible_to_nat by blast
lemma wfP_subset_mset[simp]: "wfP (\<subset>#)"
by (rule wf_subset_mset_rel[to_pred])
lemma full_multiset_induct [case_names less]:
-assumes ih: "\<And>B. \<forall>(A::'a multiset). A \<subset># B \<longrightarrow> P A \<Longrightarrow> P B"
-shows "P B"
-apply (rule wf_subset_mset_rel [THEN wf_induct])
-apply (rule ih, auto)
-done
+ assumes ih: "\<And>B. \<forall>(A::'a multiset). A \<subset># B \<longrightarrow> P A \<Longrightarrow> P B"
+ shows "P B"
+ apply (rule wf_subset_mset_rel [THEN wf_induct])
+ apply (rule ih, auto)
+ done
lemma multi_subset_induct [consumes 2, case_names empty add]:
assumes "F \<subseteq># A"
@@ -1912,9 +1853,7 @@
proof (cases "x \<in># B")
case True
with add.prems have "image_mset f A = image_mset f (B - {#x#}) + C"
- by (smt (verit, del_insts) add.left_commute add_cancel_right_left diff_union_cancelL
- diff_union_single_conv image_mset_union union_mset_add_mset_left
- union_mset_add_mset_right)
+ by (smt (verit) add_mset_add_mset_same_iff image_mset_add_mset insert_DiffM union_mset_add_mset_left)
with add.IH have "\<exists>M3'. A = B - {#x#} + M3' \<and> image_mset f M3' = C"
by (smt (verit, del_insts) True Un_insert_left Un_insert_right add.prems(2) inj_on_insert
insert_DiffM set_mset_add_mset_insert)
@@ -2035,12 +1974,7 @@
lemma set_eq_iff_mset_remdups_eq:
\<open>set x = set y \<longleftrightarrow> mset (remdups x) = mset (remdups y)\<close>
-apply (rule iffI)
-apply (simp add: set_eq_iff_mset_eq_distinct[THEN iffD1])
-apply (drule distinct_remdups [THEN distinct_remdups
- [THEN set_eq_iff_mset_eq_distinct [THEN iffD2]]])
-apply simp
-done
+ using set_eq_iff_mset_eq_distinct by fastforce
lemma mset_eq_imp_distinct_iff:
\<open>distinct xs \<longleftrightarrow> distinct ys\<close> if \<open>mset xs = mset ys\<close>
@@ -2255,14 +2189,14 @@
lemma set_sorted_list_of_multiset [simp]:
"set (sorted_list_of_multiset M) = set_mset M"
-by (induct M) (simp_all add: set_insort_key)
+ by (induct M) (simp_all add: set_insort_key)
lemma sorted_list_of_mset_set [simp]:
"sorted_list_of_multiset (mset_set A) = sorted_list_of_set A"
-by (cases "finite A") (induct A rule: finite_induct, simp_all)
+ by (cases "finite A") (induct A rule: finite_induct, simp_all)
lemma mset_upt [simp]: "mset [m..<n] = mset_set {m..<n}"
- by (induction n) (simp_all add: atLeastLessThanSuc)
+ by (metis distinct_upt mset_set_set set_upt)
lemma image_mset_map_of:
"distinct (map fst xs) \<Longrightarrow> {#the (map_of xs i). i \<in># mset (map fst xs)#} = mset (map snd xs)"
@@ -2308,7 +2242,7 @@
unfolding replicate_mset_def by (induct n) auto
lemma set_mset_replicate_mset_subset[simp]: "set_mset (replicate_mset n x) = (if n = 0 then {} else {x})"
- by (auto split: if_splits)
+ by auto
lemma size_replicate_mset[simp]: "size (replicate_mset n M) = n"
by (induct n, simp_all)
@@ -2530,8 +2464,8 @@
shows "size {#x \<in># M. P x#} < size M"
proof -
have "size (filter_mset P M) \<noteq> size M"
- using assms by (metis add.right_neutral add_diff_cancel_left' count_filter_mset mem_Collect_eq
- multiset_partition nonempty_has_size set_mset_def size_union)
+ using assms
+ by (metis dual_order.strict_iff_order filter_mset_eq_conv mset_subset_size subset_mset.nless_le)
then show ?thesis
by (meson leD nat_neq_iff size_filter_mset_lesseq)
qed
@@ -3956,17 +3890,11 @@
by (force simp: mult1_def)
lemma union_le_mono2: "B < D \<Longrightarrow> C + B < C + (D::'a::preorder multiset)"
-apply (unfold less_multiset_def multp_def mult_def)
-apply (erule trancl_induct)
- apply (blast intro: mult1_union)
-apply (blast intro: mult1_union trancl_trans)
-done
+ unfolding less_multiset_def multp_def mult_def
+ by (induction rule: trancl_induct; blast intro: mult1_union trancl_trans)
lemma union_le_mono1: "B < D \<Longrightarrow> B + C < D + (C::'a::preorder multiset)"
-apply (subst add.commute [of B C])
-apply (subst add.commute [of D C])
-apply (erule union_le_mono2)
-done
+ by (metis add.commute union_le_mono2)
lemma union_less_mono:
fixes A B C D :: "'a::preorder multiset"
@@ -3991,8 +3919,8 @@
definition "ms_weak = ms_strict \<union> Id"
lemma ms_reduction_pair: "reduction_pair (ms_strict, ms_weak)"
-unfolding reduction_pair_def ms_strict_def ms_weak_def pair_less_def
-by (auto intro: wf_mult1 wf_trancl simp: mult_def)
+ unfolding reduction_pair_def ms_strict_def ms_weak_def pair_less_def
+ by (auto intro: wf_mult1 wf_trancl simp: mult_def)
lemma smsI:
"(set_mset A, set_mset B) \<in> max_strict \<Longrightarrow> (Z + A, Z + B) \<in> ms_strict"
@@ -4268,11 +4196,7 @@
lemma [code]: \<comment> \<open>not very efficient, but representation-ignorant!\<close>
"mset_set A = mset (sorted_list_of_set A)"
- apply (cases "finite A")
- apply simp_all
- apply (induct A rule: finite_induct)
- apply simp_all
- done
+ by (metis mset_sorted_list_of_multiset sorted_list_of_mset_set)
declare size_mset [code]
@@ -4313,18 +4237,15 @@
hence id: "mset ys = add_mset x (mset (ys1 @ ys2))"
by auto
show ?thesis unfolding subset_eq_mset_impl.simps
- unfolding Some option.simps split
- unfolding id
- using Cons[of "ys1 @ ys2"]
- unfolding subset_mset_def subseteq_mset_def by auto
+ by (simp add: Some id Cons)
qed
qed
lemma [code]: "mset xs \<subseteq># mset ys \<longleftrightarrow> subset_eq_mset_impl xs ys \<noteq> None"
- using subset_eq_mset_impl[of xs ys] by (cases "subset_eq_mset_impl xs ys", auto)
+ by (simp add: subset_eq_mset_impl)
lemma [code]: "mset xs \<subset># mset ys \<longleftrightarrow> subset_eq_mset_impl xs ys = Some True"
- using subset_eq_mset_impl[of xs ys] by (cases "subset_eq_mset_impl xs ys", auto)
+ using subset_eq_mset_impl by blast
instantiation multiset :: (equal) equal
begin
@@ -4519,14 +4440,10 @@
rel: rel_mset
pred: pred_mset
proof -
- show "image_mset id = id"
- by (rule image_mset.id)
show "image_mset (g \<circ> f) = image_mset g \<circ> image_mset f" for f g
unfolding comp_def by (rule ext) (simp add: comp_def image_mset.compositionality)
show "(\<And>z. z \<in> set_mset X \<Longrightarrow> f z = g z) \<Longrightarrow> image_mset f X = image_mset g X" for f g X
by (induct X) simp_all
- show "set_mset \<circ> image_mset f = (`) f \<circ> set_mset" for f
- by auto
show "card_order natLeq"
by (rule natLeq_card_order)
show "BNF_Cardinal_Arithmetic.cinfinite natLeq"
@@ -4538,34 +4455,15 @@
(auto simp: finite_iff_ordLess_natLeq[symmetric])
show "rel_mset R OO rel_mset S \<le> rel_mset (R OO S)" for R S
unfolding rel_mset_def[abs_def] OO_def
- apply clarify
- subgoal for X Z Y xs ys' ys zs
- apply (drule list_all2_reorder_left_invariance [where xs = ys' and ys = zs and xs' = ys])
- apply (auto intro: list_all2_trans)
- done
- done
+ by (smt (verit, ccfv_SIG) list_all2_reorder_left_invariance list_all2_trans predicate2I)
show "rel_mset R =
(\<lambda>x y. \<exists>z. set_mset z \<subseteq> {(x, y). R x y} \<and>
image_mset fst z = x \<and> image_mset snd z = y)" for R
unfolding rel_mset_def[abs_def]
- apply (rule ext)+
- apply safe
- apply (rule_tac x = "mset (zip xs ys)" in exI;
- auto simp: in_set_zip list_all2_iff simp flip: mset_map)
- apply (rename_tac XY)
- apply (cut_tac X = XY in ex_mset)
- apply (erule exE)
- apply (rename_tac xys)
- apply (rule_tac x = "map fst xys" in exI)
- apply (auto simp: mset_map)
- apply (rule_tac x = "map snd xys" in exI)
- apply (auto simp: mset_map list_all2I subset_eq zip_map_fst_snd)
- done
- show "z \<in> set_mset {#} \<Longrightarrow> False" for z
- by auto
+ by (metis (no_types, lifting) ex_mset list.in_rel mem_Collect_eq mset_map set_mset_mset)
show "pred_mset P = (\<lambda>x. Ball (set_mset x) P)" for P
by (simp add: fun_eq_iff pred_mset_iff)
-qed
+qed auto
inductive rel_mset' :: \<open>('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'b multiset \<Rightarrow> bool\<close>
where
@@ -4609,10 +4507,7 @@
and addL: "\<And>a M N. P M N \<Longrightarrow> P (add_mset a M) N"
and addR: "\<And>a M N. P M N \<Longrightarrow> P M (add_mset a N)"
shows "P M N"
-apply(induct N rule: multiset_induct)
- apply(induct M rule: multiset_induct, rule empty, erule addL)
- apply(induct M rule: multiset_induct, erule addR, erule addR)
-done
+ by (induct N rule: multiset_induct; induct M rule: multiset_induct) (auto simp: assms)
lemma multiset_induct2_size[consumes 1, case_names empty add]:
assumes c: "size M = size N"
--- a/src/HOL/Library/Poly_Mapping.thy Fri Apr 12 10:10:16 2024 +0200
+++ b/src/HOL/Library/Poly_Mapping.thy Fri Apr 12 09:58:53 2024 +0100
@@ -459,7 +459,7 @@
{b. \<exists>a. (f a * g b when k = a + b) \<noteq> 0} \<subseteq> {a. f a \<noteq> 0} \<times> {b. g b \<noteq> 0}"
by auto
ultimately show ?thesis using fin_g
- by (auto simp add: prod_fun_def
+ by (auto simp: prod_fun_def
Sum_any.cartesian_product [of "{a. f a \<noteq> 0} \<times> {b. g b \<noteq> 0}"] Sum_any_right_distrib mult_when)
qed
@@ -526,14 +526,13 @@
have "?lhs k = (\<Sum>(ab, c). (\<Sum>(a, b). f a * g b when ab = a + b) * h c when k = ab + c)"
by (simp add: prod_fun_unfold_prod)
also have "\<dots> = (\<Sum>(ab, c). (\<Sum>(a, b). f a * g b * h c when k = ab + c when ab = a + b))"
- apply (subst Sum_any_left_distrib)
- using fin_fg apply (simp add: split_def)
- apply (subst Sum_any_when_independent [symmetric])
- apply (simp add: when_when when_mult mult_when split_def conj_commute)
+ using fin_fg
+ apply (simp add: Sum_any_left_distrib split_def flip: Sum_any_when_independent)
+ apply (simp add: when_when when_mult mult_when conj_commute)
done
also have "\<dots> = (\<Sum>(ab, c, a, b). f a * g b * h c when k = ab + c when ab = a + b)"
apply (subst Sum_any.cartesian_product2 [of "(?FG' \<times> ?H) \<times> ?FG"])
- apply (auto simp add: finite_cartesian_product_iff fin_fg fin_fg' fin_h dest: mult_not_zero)
+ apply (auto simp: finite_cartesian_product_iff fin_fg fin_fg' fin_h dest: mult_not_zero)
done
also have "\<dots> = (\<Sum>(ab, c, a, b). f a * g b * h c when k = a + b + c when ab = a + b)"
by (rule Sum_any.cong) (simp add: split_def when_def)
@@ -558,7 +557,7 @@
qed
also have "\<dots> = (\<Sum>(a, bc). (\<Sum>(b, c). f a * g b * h c when bc = b + c when k = a + bc))"
apply (subst Sum_any.cartesian_product2 [of "(?F \<times> ?GH') \<times> ?GH"])
- apply (auto simp add: finite_cartesian_product_iff fin_f fin_gh fin_gh' ac_simps dest: mult_not_zero)
+ apply (auto simp: finite_cartesian_product_iff fin_f fin_gh fin_gh' ac_simps dest: mult_not_zero)
done
also have "\<dots> = (\<Sum>(a, bc). f a * (\<Sum>(b, c). g b * h c when bc = b + c) when k = a + bc)"
apply (subst Sum_any_right_distrib)
@@ -580,10 +579,8 @@
assume fin_h: "finite {k. h k \<noteq> 0}"
show "prod_fun (\<lambda>k. f k + g k) h = (\<lambda>k. prod_fun f h k + prod_fun g h k)"
apply (rule ext)
- apply (auto simp add: prod_fun_def algebra_simps)
- apply (subst Sum_any.distrib)
- using fin_f fin_g apply (auto intro: finite_mult_not_eq_zero_rightI)
- done
+ apply (simp add: prod_fun_def algebra_simps)
+ by (simp add: Sum_any.distrib fin_f fin_g finite_mult_not_eq_zero_rightI)
qed
show "a * (b + c) = a * b + a * c"
proof transfer
@@ -593,15 +590,8 @@
assume fin_h: "finite {k. h k \<noteq> 0}"
show "prod_fun f (\<lambda>k. g k + h k) = (\<lambda>k. prod_fun f g k + prod_fun f h k)"
apply (rule ext)
- apply (auto simp add: prod_fun_def Sum_any.distrib algebra_simps when_add_distrib)
- apply (subst Sum_any.distrib)
- apply (simp_all add: algebra_simps)
- apply (auto intro: fin_g fin_h)
- apply (subst Sum_any.distrib)
- apply (simp_all add: algebra_simps)
- using fin_f apply (rule finite_mult_not_eq_zero_rightI)
- using fin_f apply (rule finite_mult_not_eq_zero_rightI)
- done
+ apply (auto simp: prod_fun_def Sum_any.distrib algebra_simps when_add_distrib fin_g fin_h)
+ by (simp add: Sum_any.distrib fin_f finite_mult_not_eq_zero_rightI)
qed
show "0 * a = 0"
by transfer (simp add: prod_fun_def [abs_def])
@@ -632,16 +622,10 @@
using fin_g by auto
from fin_f fin_g have "finite {(a, b). f a \<noteq> 0 \<and> g b \<noteq> 0}" (is "finite ?AB")
by simp
- show "prod_fun f g k = prod_fun g f k"
- apply (simp add: prod_fun_def)
- apply (subst Sum_any_right_distrib)
- apply (rule fin2)
- apply (subst Sum_any_right_distrib)
- apply (rule fin1)
- apply (subst Sum_any.swap [of ?AB])
- apply (fact \<open>finite ?AB\<close>)
- apply (auto simp add: mult_when ac_simps)
- done
+ have "(\<Sum>a. \<Sum>n. f a * (g n when k = a + n)) = (\<Sum>a. \<Sum>n. g a * (f n when k = a + n))"
+ by (subst Sum_any.swap [OF \<open>finite ?AB\<close>]) (auto simp: mult_when ac_simps)
+ then show "prod_fun f g k = prod_fun g f k"
+ by (simp add: prod_fun_def Sum_any_right_distrib [OF fin2] Sum_any_right_distrib [OF fin1])
qed
qed
show "(a + b) * c = a * c + b * c"
@@ -651,12 +635,8 @@
assume fin_g: "finite {k. g k \<noteq> 0}"
assume fin_h: "finite {k. h k \<noteq> 0}"
show "prod_fun (\<lambda>k. f k + g k) h = (\<lambda>k. prod_fun f h k + prod_fun g h k)"
- apply (auto simp add: prod_fun_def fun_eq_iff algebra_simps)
- apply (subst Sum_any.distrib)
- using fin_f apply (rule finite_mult_not_eq_zero_rightI)
- using fin_g apply (rule finite_mult_not_eq_zero_rightI)
- apply simp_all
- done
+ by (auto simp: prod_fun_def fun_eq_iff algebra_simps
+ Sum_any.distrib fin_f fin_g finite_mult_not_eq_zero_rightI)
qed
qed
@@ -720,7 +700,7 @@
lemma lookup_single:
"lookup (single k v) k' = (v when k = k')"
- by transfer rule
+ by (simp add: single.rep_eq)
lemma lookup_single_eq [simp]:
"lookup (single k v) k = v"
@@ -810,11 +790,7 @@
lemma lookup_of_int:
"lookup (of_int l) k = (of_int l when k = 0)"
-proof -
- have "lookup (of_int l) k = lookup (single 0 (of_int l)) k"
- by simp
- then show ?thesis unfolding lookup_single by simp
-qed
+ by (metis lookup_single_not_eq single.rep_eq single_of_int)
subsection \<open>Integral domains\<close>
@@ -841,10 +817,10 @@
by simp
assume "f \<noteq> (\<lambda>a. 0)"
then obtain a where "f a \<noteq> 0"
- by (auto simp add: fun_eq_iff)
+ by (auto simp: fun_eq_iff)
assume "g \<noteq> (\<lambda>b. 0)"
then obtain b where "g b \<noteq> 0"
- by (auto simp add: fun_eq_iff)
+ by (auto simp: fun_eq_iff)
from \<open>f a \<noteq> 0\<close> and \<open>g b \<noteq> 0\<close> have "F \<noteq> {}" and "G \<noteq> {}"
by auto
note Max_F = \<open>finite F\<close> \<open>F \<noteq> {}\<close>
@@ -860,7 +836,7 @@
define q where "q = Max F + Max G"
have "(\<Sum>(a, b). f a * g b when q = a + b) =
(\<Sum>(a, b). f a * g b when q = a + b when a \<in> F \<and> b \<in> G)"
- by (rule Sum_any.cong) (auto simp add: split_def when_def q_def intro: ccontr)
+ by (rule Sum_any.cong) (auto simp: split_def when_def q_def intro: ccontr)
also have "\<dots> =
(\<Sum>(a, b). f a * g b when (Max F, Max G) = (a, b))"
proof (rule Sum_any.cong)
@@ -873,7 +849,7 @@
by auto
show "(case ab of (a, b) \<Rightarrow> f a * g b when q = a + b when a \<in> F \<and> b \<in> G) =
(case ab of (a, b) \<Rightarrow> f a * g b when (Max F, Max G) = (a, b))"
- by (auto simp add: split_def when_def q_def dest: add_strict_mono [of a "Max F" b "Max G"])
+ by (auto simp: split_def when_def q_def dest: add_strict_mono [of a "Max F" b "Max G"])
qed
also have "\<dots> = (\<Sum>ab. (case ab of (a, b) \<Rightarrow> f a * g b) when
(Max F, Max G) = ab)"
@@ -883,7 +859,7 @@
finally have "prod_fun f g q \<noteq> 0"
by (simp add: prod_fun_unfold_prod)
then show "prod_fun f g \<noteq> (\<lambda>k. 0)"
- by (auto simp add: fun_eq_iff)
+ by (auto simp: fun_eq_iff)
qed
qed
@@ -954,7 +930,7 @@
by (blast intro: less_funI)
}
with * show "less_fun (\<lambda>k. h k + f k) (\<lambda>k. h k + g k) \<or> (\<lambda>k. h k + f k) = (\<lambda>k. h k + g k)"
- by (auto simp add: fun_eq_iff)
+ by (auto simp: fun_eq_iff)
qed
instance poly_mapping :: (linorder, "{ordered_comm_monoid_add, ordered_ab_semigroup_add_imp_le, cancel_comm_monoid_add, linorder}") linordered_cancel_ab_semigroup_add
@@ -1036,7 +1012,7 @@
lemma range_one [simp]:
"range 1 = {1}"
- by transfer (auto simp add: when_def)
+ by transfer (auto simp: when_def)
lemma keys_single [simp]:
"keys (single k v) = (if v = 0 then {} else {k})"
@@ -1044,13 +1020,12 @@
lemma range_single [simp]:
"range (single k v) = (if v = 0 then {} else {v})"
- by transfer (auto simp add: when_def)
+ by transfer (auto simp: when_def)
lemma keys_mult:
"keys (f * g) \<subseteq> {a + b | a b. a \<in> keys f \<and> b \<in> keys g}"
apply transfer
- apply (auto simp add: prod_fun_def dest!: mult_not_zero elim!: Sum_any.not_neutral_obtains_not_neutral)
- apply blast
+ apply (force simp: prod_fun_def dest!: mult_not_zero elim!: Sum_any.not_neutral_obtains_not_neutral)
done
lemma setsum_keys_plus_distrib:
@@ -1064,13 +1039,7 @@
proof -
let ?A = "Poly_Mapping.keys p \<union> Poly_Mapping.keys q"
have "?lhs = (\<Sum>k\<in>?A. f k (Poly_Mapping.lookup p k + Poly_Mapping.lookup q k))"
- apply(rule sum.mono_neutral_cong_left)
- apply(simp_all add: Poly_Mapping.keys_add)
- apply(transfer fixing: f)
- apply(auto simp add: hom_0)[1]
- apply(transfer fixing: f)
- apply(auto simp add: hom_0)[1]
- done
+ by(intro sum.mono_neutral_cong_left) (auto simp: sum.mono_neutral_cong_left hom_0 in_keys_iff lookup_add)
also have "\<dots> = (\<Sum>k\<in>?A. f k (Poly_Mapping.lookup p k) + f k (Poly_Mapping.lookup q k))"
by(rule sum.cong)(simp_all add: hom_plus)
also have "\<dots> = (\<Sum>k\<in>?A. f k (Poly_Mapping.lookup p k)) + (\<Sum>k\<in>?A. f k (Poly_Mapping.lookup q k))"
@@ -1138,14 +1107,14 @@
shows "degree f - 1 \<in> keys f"
proof -
from assms have "keys f \<noteq> {}"
- by (auto simp add: degree_def)
+ by (auto simp: degree_def)
then show ?thesis unfolding degree_def
by (simp add: mono_Max_commute [symmetric] mono_Suc)
qed
lemma in_keys_less_degree:
"n \<in> keys f \<Longrightarrow> n < degree f"
-unfolding degree_def by transfer (auto simp add: Max_gr_iff)
+unfolding degree_def by transfer (auto simp: Max_gr_iff)
lemma beyond_degree_lookup_zero:
"degree f \<le> n \<Longrightarrow> lookup f n = 0"
@@ -1307,7 +1276,7 @@
{ fix x
have "prod_fun (\<lambda>k'. s when 0 = k') p x =
(\<Sum>l :: 'a. if l = 0 then s * (\<Sum>q. p q when x = q) else 0)"
- by(auto simp add: prod_fun_def when_def intro: Sum_any.cong simp del: Sum_any.delta)
+ by(auto simp: prod_fun_def when_def intro: Sum_any.cong simp del: Sum_any.delta)
also have "\<dots> = (\<lambda>k. s * p k when p k \<noteq> 0) x" by(simp add: when_def)
also note calculation }
then show "(\<lambda>k. s * p k when p k \<noteq> 0) = prod_fun (\<lambda>k'. s when 0 = k') p"
@@ -1316,10 +1285,10 @@
lemma map_single [simp]:
"(c = 0 \<Longrightarrow> f 0 = 0) \<Longrightarrow> map f (single x c) = single x (f c)"
-by transfer(auto simp add: fun_eq_iff when_def)
+ by transfer(auto simp: fun_eq_iff when_def)
lemma map_eq_zero_iff: "map f p = 0 \<longleftrightarrow> (\<forall>k \<in> keys p. f (lookup p k) = 0)"
-by transfer(auto simp add: fun_eq_iff when_def)
+ by transfer(auto simp: fun_eq_iff when_def)
subsection \<open>Canonical dense representation of @{typ "nat \<Rightarrow>\<^sub>0 'a"}\<close>
@@ -1345,7 +1314,7 @@
proof (transfer, rule ext)
fix n :: nat and v :: 'a
show "nth_default 0 [v] n = (v when 0 = n)"
- by (auto simp add: nth_default_def nth_append)
+ by (auto simp: nth_default_def nth_append)
qed
lemma nth_replicate [simp]:
@@ -1353,7 +1322,7 @@
proof (transfer, rule ext)
fix m n :: nat and v :: 'a
show "nth_default 0 (replicate n 0 @ [v]) m = (v when n = m)"
- by (auto simp add: nth_default_def nth_append)
+ by (auto simp: nth_default_def nth_append)
qed
lemma nth_strip_while [simp]:
@@ -1379,16 +1348,16 @@
{ fix n
assume "nth_default 0 xs n \<noteq> 0"
then have "n < length xs" and "xs ! n \<noteq> 0"
- by (auto simp add: nth_default_def split: if_splits)
+ by (auto simp: nth_default_def split: if_splits)
then have "(n, xs ! n) \<in> {(n, v). (n, v) \<in> set (enumerate 0 xs) \<and> v \<noteq> 0}" (is "?x \<in> ?A")
- by (auto simp add: in_set_conv_nth enumerate_eq_zip)
+ by (auto simp: in_set_conv_nth enumerate_eq_zip)
then have "fst ?x \<in> fst ` ?A"
by blast
then have "n \<in> fst ` {(n, v). (n, v) \<in> set (enumerate 0 xs) \<and> v \<noteq> 0}"
by simp
}
then show "{k. nth_default 0 xs k \<noteq> 0} = fst ` {(n, v). (n, v) \<in> set (enumerate 0 xs) \<and> v \<noteq> 0}"
- by (auto simp add: in_enumerate_iff_nth_default_eq)
+ by (auto simp: in_enumerate_iff_nth_default_eq)
qed
lemma range_nth [simp]:
@@ -1409,16 +1378,16 @@
with * obtain n where n: "n < length xs" "xs ! n \<noteq> 0"
by (fastforce simp add: no_trailing_unfold last_conv_nth neq_Nil_conv)
then have "?bound = Max (Suc ` {k. (k < length xs \<longrightarrow> xs ! k \<noteq> (0::'a)) \<and> k < length xs})"
- by (subst Max_insert) (auto simp add: nth_default_def)
+ by (subst Max_insert) (auto simp: nth_default_def)
also let ?A = "{k. k < length xs \<and> xs ! k \<noteq> 0}"
have "{k. (k < length xs \<longrightarrow> xs ! k \<noteq> (0::'a)) \<and> k < length xs} = ?A" by auto
also have "Max (Suc ` ?A) = Suc (Max ?A)" using n
- by (subst mono_Max_commute [where f = Suc, symmetric]) (auto simp add: mono_Suc)
+ by (subst mono_Max_commute [where f = Suc, symmetric]) (auto simp: mono_Suc)
also {
have "Max ?A \<in> ?A" using n Max_in [of ?A] by fastforce
hence "Suc (Max ?A) \<le> length xs" by simp
moreover from * False have "length xs - 1 \<in> ?A"
- by(auto simp add: no_trailing_unfold last_conv_nth)
+ by(auto simp: no_trailing_unfold last_conv_nth)
hence "length xs - 1 \<le> Max ?A" using Max_ge[of ?A "length xs - 1"] by auto
hence "length xs \<le> Suc (Max ?A)" by simp
ultimately have "Suc (Max ?A) = length xs" by simp }
@@ -1433,7 +1402,7 @@
lemma nth_idem:
"nth (List.map (lookup f) [0..<degree f]) = f"
unfolding degree_def by transfer
- (auto simp add: nth_default_def fun_eq_iff not_less)
+ (auto simp: nth_default_def fun_eq_iff not_less)
lemma nth_idem_bound:
assumes "degree f \<le> n"
@@ -1444,7 +1413,7 @@
then have "[0..<n] = [0..<degree f] @ [degree f..<degree f + m]"
by (simp add: upt_add_eq_append [of 0])
moreover have "List.map (lookup f) [degree f..<degree f + m] = replicate m 0"
- by (rule replicate_eqI) (auto simp add: beyond_degree_lookup_zero)
+ by (rule replicate_eqI) (auto simp: beyond_degree_lookup_zero)
ultimately show ?thesis by (simp add: nth_idem)
qed
@@ -1489,10 +1458,10 @@
from assms have "sorted_list_of_set (set (List.map fst xs)) = List.map fst xs"
unfolding sorted_list_of_set_sort_remdups by (simp add: distinct_remdups_id sort_key_id_if_sorted)
moreover from assms have "keys (the_value xs) = fst ` set xs"
- by transfer (auto simp add: image_def split: option.split dest: set_map_of_compr)
+ by transfer (auto simp: image_def split: option.split dest: set_map_of_compr)
ultimately show ?thesis
unfolding items_def using assms
- by (auto simp add: lookup_the_value intro: map_idI)
+ by (auto simp: lookup_the_value intro: map_idI)
qed
lemma the_value_Nil [simp]:
@@ -1549,7 +1518,7 @@
then have "f k + g (m k) = (\<Sum>k' \<in> ?keys. f k' + g (m k') when k' = k)"
by (simp add: sum.delta when_def)
also have "\<dots> < (\<Sum>k' \<in> ?keys. Suc (f k' + g (m k')))" using *
- by (intro sum_strict_mono) (auto simp add: when_def)
+ by (intro sum_strict_mono) (auto simp: when_def)
also have "\<dots> \<le> g 0 + \<dots>" by simp
finally have "f k + g (m k) < \<dots>" .
then show "f k + g (m k) < g 0 + (\<Sum>k | m k \<noteq> 0. Suc (f k + g (m k)))"
@@ -1599,7 +1568,7 @@
"m = m' \<Longrightarrow> g 0 = g' 0 \<Longrightarrow> (\<And>k. k \<in> keys m' \<Longrightarrow> f k = f' k)
\<Longrightarrow> (\<And>v. v \<in> range m' \<Longrightarrow> g v = g' v)
\<Longrightarrow> poly_mapping_size f g m = poly_mapping_size f' g' m'"
- by (auto simp add: poly_mapping_size_def intro!: sum.cong)
+ by (auto simp: poly_mapping_size_def intro!: sum.cong)
instantiation poly_mapping :: (type, zero) size
begin
@@ -1623,7 +1592,7 @@
lemma mapp_cong [fundef_cong]:
"\<lbrakk> m = m'; \<And>k. k \<in> keys m' \<Longrightarrow> f k (lookup m' k) = f' k (lookup m' k) \<rbrakk>
\<Longrightarrow> mapp f m = mapp f' m'"
- by transfer (auto simp add: fun_eq_iff)
+ by transfer (auto simp: fun_eq_iff)
lemma lookup_mapp:
"lookup (mapp f p) k = (f k (lookup p k) when k \<in> keys p)"
@@ -1688,8 +1657,6 @@
lemma keys_cmul_iff [iff]: "i \<in> Poly_Mapping.keys (frag_cmul c x) \<longleftrightarrow> i \<in> Poly_Mapping.keys x \<and> c \<noteq> 0"
- apply auto
- apply (meson subsetD keys_cmul)
by (metis in_keys_iff lookup_frag_cmul mult_eq_0_iff)
lemma keys_minus [simp]: "Poly_Mapping.keys(-a) = Poly_Mapping.keys a"
@@ -1697,7 +1664,7 @@
lemma keys_diff:
"Poly_Mapping.keys(a - b) \<subseteq> Poly_Mapping.keys a \<union> Poly_Mapping.keys b"
- by (auto simp add: in_keys_iff lookup_minus)
+ by (auto simp: in_keys_iff lookup_minus)
lemma keys_eq_empty [simp]: "Poly_Mapping.keys c = {} \<longleftrightarrow> c = 0"
by (metis in_keys_iff keys_zero lookup_zero poly_mapping_eqI)
@@ -1769,10 +1736,11 @@
by (auto simp: frag_extend_def Poly_Mapping.lookup_add frag_cmul_distrib)
also have "... = (\<Sum>i \<in> Poly_Mapping.keys a \<union> Poly_Mapping.keys b. frag_cmul (poly_mapping.lookup a i) (f i)
+ frag_cmul (poly_mapping.lookup b i) (f i))"
- apply (rule sum.mono_neutral_cong_left)
- using keys_add [of a b]
- apply (auto simp add: in_keys_iff plus_poly_mapping.rep_eq frag_cmul_distrib [symmetric])
- done
+ proof (rule sum.mono_neutral_cong_left)
+ show "\<forall>i\<in>keys a \<union> keys b - keys (a + b).
+ frag_cmul (lookup a i) (f i) + frag_cmul (lookup b i) (f i) = 0"
+ by (metis DiffD2 frag_cmul_distrib frag_cmul_zero in_keys_iff lookup_add)
+ qed (auto simp: keys_add)
also have "... = (frag_extend f a) + (frag_extend f b)"
by (auto simp: * sum.distrib frag_extend_def)
finally show ?thesis .
@@ -1814,9 +1782,15 @@
shows "P(frag_cmul k c)"
proof -
have "P (frag_cmul (int n) c)" for n
- apply (induction n)
- apply (simp_all add: assms frag_cmul_distrib)
- by (metis add.left_neutral add_diff_cancel_right' add_uminus_conv_diff P)
+ proof (induction n)
+ case 0
+ then show ?case
+ by (simp add: assms)
+ next
+ case (Suc n)
+ then show ?case
+ by (metis assms diff_0 diff_minus_eq_add frag_cmul_distrib frag_cmul_one of_nat_Suc)
+ qed
then show ?thesis
by (metis (no_types, opaque_lifting) add_diff_eq assms(2) diff_add_cancel frag_cmul_distrib int_diff_cases)
qed
@@ -1840,14 +1814,11 @@
by simp
have Pfrag: "P (frag_cmul (poly_mapping.lookup c i) (frag_of i))"
by (metis "0" diff frag_closure_minus_cmul insert.prems insert_subset sing subset_iff)
- show ?case
- apply (simp add: insert.hyps)
- apply (subst ab)
- using insert apply (blast intro: assms Pfrag)
- done
+ with insert show ?case
+ by (metis (mono_tags, lifting) "0" ab diff insert_subset sum.insert)
qed
then show ?thesis
- by (subst frag_expansion) (auto simp add: frag_extend_def)
+ by (subst frag_expansion) (auto simp: frag_extend_def)
qed
lemma frag_extend_compose: