--- a/src/HOL/Library/Extended_Nat.thy Wed Jan 15 17:48:38 2025 +0100
+++ b/src/HOL/Library/Extended_Nat.thy Thu Jan 16 10:09:33 2025 +0000
@@ -191,10 +191,10 @@
by (simp_all add: eSuc_plus_1 ac_simps)
lemma iadd_Suc: "eSuc m + n = eSuc (m + n)"
- by (simp_all add: eSuc_plus_1 ac_simps)
+ by (simp add: eSuc_plus_1 ac_simps)
lemma iadd_Suc_right: "m + eSuc n = eSuc (m + n)"
- by (simp only: add.commute[of m] iadd_Suc)
+ by (metis add.commute iadd_Suc)
subsection \<open>Multiplication\<close>
@@ -216,29 +216,12 @@
instance
proof
fix a b c :: enat
- show "(a * b) * c = a * (b * c)"
- unfolding times_enat_def zero_enat_def
- by (simp split: enat.split)
- show comm: "a * b = b * a"
- unfolding times_enat_def zero_enat_def
- by (simp split: enat.split)
- show "1 * a = a"
- unfolding times_enat_def zero_enat_def one_enat_def
- by (simp split: enat.split)
show distr: "(a + b) * c = a * c + b * c"
unfolding times_enat_def zero_enat_def
by (simp split: enat.split add: distrib_right)
- show "0 * a = 0"
- unfolding times_enat_def zero_enat_def
- by (simp split: enat.split)
- show "a * 0 = 0"
- unfolding times_enat_def zero_enat_def
- by (simp split: enat.split)
show "a * (b + c) = a * b + a * c"
by (cases a b c rule: enat3_cases) (auto simp: times_enat_def zero_enat_def distrib_left)
- show "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
- by (cases a b rule: enat2_cases) (auto simp: times_enat_def zero_enat_def)
-qed
+qed (auto simp: times_enat_def zero_enat_def one_enat_def split: enat.split)
end
@@ -246,13 +229,10 @@
unfolding eSuc_plus_1 by (simp add: algebra_simps)
lemma mult_eSuc_right: "m * eSuc n = m + m * n"
- unfolding eSuc_plus_1 by (simp add: algebra_simps)
+ by (metis mult.commute mult_eSuc)
lemma of_nat_eq_enat: "of_nat n = enat n"
- apply (induct n)
- apply (simp add: enat_0)
- apply (simp add: plus_1_eSuc eSuc_enat)
- done
+ by (induct n) (auto simp: enat_0 plus_1_eSuc eSuc_enat)
instance enat :: semiring_char_0
proof
@@ -267,7 +247,7 @@
lemma numeral_eq_enat:
"numeral k = enat (numeral k)"
- using of_nat_eq_enat [of "numeral k"] by simp
+ by (metis of_nat_eq_enat of_nat_numeral)
lemma enat_numeral [code_abbrev]:
"enat (numeral k) = numeral k"
@@ -349,11 +329,11 @@
lemma numeral_le_enat_iff[simp]:
shows "numeral m \<le> enat n \<longleftrightarrow> numeral m \<le> n"
-by (auto simp: numeral_eq_enat)
+ by (auto simp: numeral_eq_enat)
lemma numeral_less_enat_iff[simp]:
shows "numeral m < enat n \<longleftrightarrow> numeral m < n"
-by (auto simp: numeral_eq_enat)
+ by (auto simp: numeral_eq_enat)
lemma enat_ord_code [code]:
"enat m \<le> enat n \<longleftrightarrow> m \<le> n"
@@ -472,17 +452,15 @@
by(cases x y rule: enat.exhaust[case_product enat.exhaust]) simp_all
lemma chain_incr: "\<forall>i. \<exists>j. Y i < Y j \<Longrightarrow> \<exists>j. enat k < Y j"
-apply (induct_tac k)
- apply (simp (no_asm) only: enat_0)
- apply (fast intro: le_less_trans [OF zero_le])
-apply (erule exE)
-apply (drule spec)
-apply (erule exE)
-apply (drule ileI1)
-apply (rule eSuc_enat [THEN subst])
-apply (rule exI)
-apply (erule (1) le_less_trans)
-done
+proof (induction k)
+ case 0
+ then show ?case
+ using enat_0 zero_less_iff_neq_zero by fastforce
+next
+ case (Suc k)
+ then show ?case
+ by (meson Suc_ile_eq order_le_less_trans)
+qed
lemma eSuc_max: "eSuc (max x y) = max (eSuc x) (eSuc y)"
by (simp add: eSuc_def split: enat.split)
@@ -490,10 +468,7 @@
lemma eSuc_Max:
assumes "finite A" "A \<noteq> {}"
shows "eSuc (Max A) = Max (eSuc ` A)"
-using assms proof induction
- case (insert x A)
- thus ?case by(cases "A = {}")(simp_all add: eSuc_max)
-qed simp
+ by (simp add: assms mono_Max_commute mono_eSuc)
instantiation enat :: "{order_bot, order_top}"
begin
@@ -511,19 +486,16 @@
shows "finite A"
proof (rule finite_subset)
show "finite (enat ` {..n})" by blast
- have "A \<subseteq> {..enat n}" using le_fin by fastforce
- also have "\<dots> \<subseteq> enat ` {..n}"
- apply (rule subsetI)
- subgoal for x by (cases x) auto
- done
- finally show "A \<subseteq> enat ` {..n}" .
+ have "A \<subseteq> enat ` {..n}"
+ using enat_ile le_fin by fastforce
+ then show "A \<subseteq> enat ` {..n}" .
qed
subsection \<open>Cancellation simprocs\<close>
lemma add_diff_cancel_enat[simp]: "x \<noteq> \<infinity> \<Longrightarrow> x + y - x = (y::enat)"
-by (metis add.commute add.right_neutral add_diff_assoc_enat idiff_self order_refl)
+ by (metis add.commute add.right_neutral add_diff_assoc_enat idiff_self order_refl)
lemma enat_add_left_cancel: "a + b = a + c \<longleftrightarrow> a = (\<infinity>::enat) \<or> b = c"
unfolding plus_enat_def by (simp split: enat.split)
@@ -535,7 +507,7 @@
unfolding plus_enat_def by (simp split: enat.split)
lemma plus_eq_infty_iff_enat: "(m::enat) + n = \<infinity> \<longleftrightarrow> m=\<infinity> \<or> n=\<infinity>"
-using enat_add_left_cancel by fastforce
+ using enat_add_left_cancel by fastforce
ML \<open>
structure Cancel_Enat_Common =
@@ -605,32 +577,21 @@
subsection \<open>Well-ordering\<close>
lemma less_enatE:
- "[| n < enat m; !!k. n = enat k ==> k < m ==> P |] ==> P"
-by (induct n) auto
+ "\<lbrakk>n < enat m; \<And>k. \<lbrakk>n = enat k; k < m\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
+ using enat_iless enat_ord_simps(2) by blast
lemma less_infinityE:
- "[| n < \<infinity>; !!k. n = enat k ==> P |] ==> P"
-by (induct n) auto
+ "\<lbrakk>n < \<infinity>; \<And>k. n = enat k \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
+ by auto
lemma enat_less_induct:
- assumes prem: "\<And>n. \<forall>m::enat. m < n \<longrightarrow> P m \<Longrightarrow> P n" shows "P n"
+ assumes "\<And>n. \<forall>m::enat. m < n \<longrightarrow> P m \<Longrightarrow> P n"
+ shows "P n"
proof -
- have P_enat: "\<And>k. P (enat k)"
- apply (rule nat_less_induct)
- apply (rule prem, clarify)
- apply (erule less_enatE, simp)
- done
- show ?thesis
- proof (induct n)
- fix nat
- show "P (enat nat)" by (rule P_enat)
- next
- show "P \<infinity>"
- apply (rule prem, clarify)
- apply (erule less_infinityE)
- apply (simp add: P_enat)
- done
- qed
+ have "P (enat k)" for k
+ by (induction k rule: less_induct) (metis less_enatE assms)
+ then show ?thesis
+ by (metis enat.exhaust less_infinityE assms)
qed
instance enat :: wellorder
--- a/src/HOL/Library/Poly_Mapping.thy Wed Jan 15 17:48:38 2025 +0100
+++ b/src/HOL/Library/Poly_Mapping.thy Thu Jan 16 10:09:33 2025 +0000
@@ -20,19 +20,13 @@
fixes f :: "'b \<Rightarrow> 'a :: mult_zero"
assumes "finite {a. f a \<noteq> 0}"
shows "finite {a. g a * f a \<noteq> 0}"
-proof -
- have "{a. g a * f a \<noteq> 0} \<subseteq> {a. f a \<noteq> 0}" by auto
- then show ?thesis using assms by (rule finite_subset)
-qed
+ by (metis (mono_tags, lifting) Collect_mono assms mult_zero_right finite_subset)
lemma finite_mult_not_eq_zero_rightI:
fixes f :: "'b \<Rightarrow> 'a :: mult_zero"
assumes "finite {a. f a \<noteq> 0}"
shows "finite {a. f a * g a \<noteq> 0}"
-proof -
- have "{a. f a * g a \<noteq> 0} \<subseteq> {a. f a \<noteq> 0}" by auto
- then show ?thesis using assms by (rule finite_subset)
-qed
+ by (metis (mono_tags, lifting) Collect_mono assms lambda_zero finite_subset)
lemma finite_mult_not_eq_zero_prodI:
fixes f g :: "'a \<Rightarrow> 'b::semiring_0"
@@ -227,10 +221,7 @@
typedef (overloaded) ('a, 'b) poly_mapping (\<open>(_ \<Rightarrow>\<^sub>0 /_)\<close> [1, 0] 0) =
"{f :: 'a \<Rightarrow> 'b::zero. finite {x. f x \<noteq> 0}}"
morphisms lookup Abs_poly_mapping
-proof -
- have "(\<lambda>_::'a. (0 :: 'b)) \<in> ?poly_mapping" by simp
- then show ?thesis by (blast intro!: exI)
-qed
+ using not_finite_existsD by force
declare lookup_inverse [simp]
declare lookup_inject [simp]
@@ -366,9 +357,8 @@
end
-lemma lookup_add:
- "lookup (f + g) k = lookup f k + lookup g k"
- by transfer rule
+lemma lookup_add: "lookup (f + g) k = lookup f k + lookup g k"
+ by (simp add: plus_poly_mapping.rep_eq)
instance poly_mapping :: (type, comm_monoid_add) comm_monoid_add
by intro_classes (transfer, simp add: fun_eq_iff ac_simps)+
@@ -435,13 +425,12 @@
end
-lemma lookup_one:
- "lookup 1 k = (1 when k = 0)"
- by transfer rule
+lemma lookup_one: "lookup 1 k = (1 when k = 0)"
+ by (meson one_poly_mapping.rep_eq)
lemma lookup_one_zero [simp]:
"lookup 1 0 = 1"
- by transfer simp
+ by (simp add: one_poly_mapping.rep_eq)
definition prod_fun :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a::monoid_add \<Rightarrow> 'b::semiring_0"
where
@@ -455,8 +444,9 @@
proof -
let ?C = "{a. f a \<noteq> 0} \<times> {b. g b \<noteq> 0}"
from fin_f fin_g have "finite ?C" by blast
- moreover have "{a. \<exists>b. (f a * g b when k = a + b) \<noteq> 0} \<times>
- {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}"
+ moreover
+ have "{a. \<exists>b. (f a * g b when k = a + b) \<noteq> 0} \<times>
+ {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: prod_fun_def
@@ -653,7 +643,7 @@
show "1 * a = a"
by transfer (simp add: prod_fun_def [abs_def] when_mult)
show "a * 1 = a"
- apply transfer
+ apply transfer
apply (simp add: prod_fun_def [abs_def] Sum_any_right_distrib Sum_any_left_distrib mult_when)
apply (subst when_commute)
apply simp
@@ -705,11 +695,11 @@
lemma lookup_single_eq [simp]:
"lookup (single k v) k = v"
- by transfer simp
+ by (simp add: single.rep_eq)
lemma lookup_single_not_eq:
"k \<noteq> k' \<Longrightarrow> lookup (single k v) k' = 0"
- by transfer simp
+ by (simp add: single.rep_eq)
lemma single_zero [simp]:
"single k 0 = 0"
@@ -749,11 +739,7 @@
lemma lookup_of_nat:
"lookup (of_nat n) k = (of_nat n when k = 0)"
-proof -
- have "lookup (of_nat n) k = lookup (single 0 (of_nat n)) k"
- by simp
- then show ?thesis unfolding lookup_single by simp
-qed
+ by (metis lookup_single lookup_single_not_eq single_of_nat)
lemma of_nat_single:
"of_nat = single 0 \<circ> of_nat"
@@ -923,14 +909,7 @@
fix f g h :: "'a \<Rightarrow> 'b"
assume *: "less_fun f g \<or> f = g"
have "less_fun (\<lambda>k. h k + f k) (\<lambda>k. h k + g k)" if "less_fun f g"
- proof -
- from that obtain k where "f k < g k" "(\<And>k'. k' < k \<Longrightarrow> f k' = g k')"
- by (blast elim!: less_funE)
- then have "h k + f k < h k + g k" "(\<And>k'. k' < k \<Longrightarrow> h k' + f k' = h k' + g k')"
- by simp_all
- then show ?thesis
- by (blast intro: less_funI)
- qed
+ by (metis (no_types, lifting) less_fun_def add_strict_left_mono that)
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: fun_eq_iff)
qed
@@ -986,7 +965,7 @@
have "Set.range f - {0} \<subseteq> f ` {x. f x \<noteq> 0}"
by auto
thus "finite (Set.range f - {0})"
- by(rule finite_subset)(rule finite_imageI[OF *])
+ using "*" finite_surj by blast
qed
lemma in_keys_lookup_in_range [simp]:
@@ -994,7 +973,7 @@
by transfer simp
lemma in_keys_iff: "x \<in> (keys s) = (lookup s x \<noteq> 0)"
- by (transfer, simp)
+ by (simp add: lookup_not_eq_zero_eq_in_keys)
lemma keys_zero [simp]:
"keys 0 = {}"
@@ -1221,9 +1200,9 @@
fix g :: "'c \<Rightarrow> 'd" and p :: "'a \<Rightarrow> 'c"
assume "finite {x. p x \<noteq> 0}"
hence "finite (f ` {y. p (f y) \<noteq> 0})"
- by(rule finite_subset[rotated]) auto
+ by (simp add: rev_finite_subset subset_eq)
thus "finite {x. (p \<circ> f) x \<noteq> 0}" unfolding o_def
- by(rule finite_imageD)(rule subset_inj_on[OF inj_f], simp)
+ by (metis finite_imageD injD inj_f inj_on_def)
qed
end
@@ -1402,7 +1381,7 @@
lemma nth_trailing_zeros [simp]:
"nth (xs @ replicate n 0) = nth xs"
- by transfer simp
+ by (simp add: nth.abs_eq)
lemma nth_idem:
"nth (List.map (lookup f) [0..<degree f]) = f"
@@ -1454,7 +1433,7 @@
lemma lookup_the_value:
"lookup (the_value xs) k = (case map_of xs k of None \<Rightarrow> 0 | Some v \<Rightarrow> v)"
- by transfer rule
+ by (simp add: the_value.rep_eq)
lemma items_the_value:
assumes "sorted (List.map fst xs)" and "distinct (List.map fst xs)" and "0 \<notin> snd ` set xs"
@@ -1552,15 +1531,10 @@
proof -
from assms obtain k where *: "lookup m k = v" "v \<noteq> 0"
by transfer blast
- from * have "k \<in> keys m"
+ then have "k \<in> keys m"
by (simp add: in_keys_iff)
- then show ?thesis
- proof (rule poly_mapping_size_estimation)
- from assms * have "y \<le> g (lookup m k)"
- by simp
- then show "y \<le> f k + g (lookup m k)"
- by simp
- qed
+ with * show ?thesis
+ by (simp add: Poly_Mapping.poly_mapping_size_estimation assms(2) trans_le_add2)
qed
end
@@ -1616,15 +1590,7 @@
by (force simp add: lookup_single_not_eq)
lemma frag_of_nonzero [simp]: "frag_of a \<noteq> 0"
-proof -
- let ?f = "\<lambda>x. if x = a then 1 else (0::int)"
- have "?f \<noteq> (\<lambda>x. 0::int)"
- by (auto simp: fun_eq_iff)
- then have "Poly_Mapping.lookup (Abs_poly_mapping ?f) \<noteq> Poly_Mapping.lookup (Abs_poly_mapping (\<lambda>x. 0))"
- by fastforce
- then show ?thesis
- by (metis lookup_single_eq lookup_zero)
-qed
+ by (metis lookup_single_eq lookup_zero zero_neq_one)
definition frag_cmul :: "int \<Rightarrow> ('a \<Rightarrow>\<^sub>0 int) \<Rightarrow> ('a \<Rightarrow>\<^sub>0 int)"
where "frag_cmul c a = Abs_poly_mapping (\<lambda>x. c * Poly_Mapping.lookup a x)"
@@ -1636,7 +1602,7 @@
by (simp add: frag_cmul_def)
lemma frag_cmul_one [simp]: "frag_cmul 1 x = x"
- by (auto simp: frag_cmul_def Poly_Mapping.poly_mapping.lookup_inverse)
+ by (simp add: frag_cmul_def)
lemma frag_cmul_minus_one [simp]: "frag_cmul (-1) x = -x"
by (simp add: frag_cmul_def uminus_poly_mapping_def poly_mapping_eqI)
@@ -1684,13 +1650,7 @@
by (simp add: frag_cmul_def plus_poly_mapping_def int_distrib)
lemma frag_cmul_distrib2: "frag_cmul c (a+b) = frag_cmul c a + frag_cmul c b"
-proof -
- have "finite {x. poly_mapping.lookup a x + poly_mapping.lookup b x \<noteq> 0}"
- using keys_add [of a b]
- by (metis (no_types, lifting) finite_keys finite_subset keys.rep_eq lookup_add mem_Collect_eq subsetI)
- then show ?thesis
- by (simp add: frag_cmul_def plus_poly_mapping_def int_distrib)
-qed
+ by (simp add: int_distrib(2) lookup_add poly_mapping_eqI)
lemma frag_cmul_diff_distrib: "frag_cmul (a - b) c = frag_cmul a c - frag_cmul b c"
by (auto simp: left_diff_distrib lookup_minus poly_mapping_eqI)