--- a/src/HOL/Algebra/Finite_Extensions.thy Mon May 10 14:28:37 2021 +0200
+++ b/src/HOL/Algebra/Finite_Extensions.thy Mon May 10 16:14:34 2021 +0200
@@ -616,15 +616,33 @@
using assms simple_extension_is_subring by (induct xs) (auto)
corollary (in domain) finite_extension_mem:
- assumes "subring K R" "set xs \<subseteq> carrier R" shows "set xs \<subseteq> finite_extension K xs"
-proof -
- { fix x xs assume "x \<in> carrier R" "set xs \<subseteq> carrier R"
- hence "x \<in> finite_extension K (x # xs)"
- using simple_extension_mem[OF finite_extension_is_subring[OF assms(1), of xs]] by simp }
- note aux_lemma = this
- show ?thesis
- using aux_lemma finite_extension_incl_aux[OF subringE(1)[OF assms(1)]] assms(2)
- by (induct xs) (simp, smt insert_subset list.simps(15) subset_trans)
+ assumes subring: "subring K R"
+ shows "set xs \<subseteq> carrier R \<Longrightarrow> set xs \<subseteq> finite_extension K xs"
+proof (induct xs)
+ case Nil
+ then show ?case by simp
+next
+ case (Cons a xs)
+ from Cons(2) have a: "a \<in> carrier R" and xs: "set xs \<subseteq> carrier R" by auto
+ show ?case
+ proof
+ fix x assume "x \<in> set (a # xs)"
+ then consider "x = a" | "x \<in> set xs" by auto
+ then show "x \<in> finite_extension K (a # xs)"
+ proof cases
+ case 1
+ with a have "x \<in> carrier R" by simp
+ with xs have "x \<in> finite_extension K (x # xs)"
+ using simple_extension_mem[OF finite_extension_is_subring[OF subring]] by simp
+ with 1 show ?thesis by simp
+ next
+ case 2
+ with Cons have *: "x \<in> finite_extension K xs" by auto
+ from a xs have "finite_extension K xs \<subseteq> finite_extension K (a # xs)"
+ by (rule finite_extension_incl_aux[OF subringE(1)[OF subring]])
+ with * show ?thesis by auto
+ qed
+ qed
qed
corollary (in domain) finite_extension_minimal:
--- a/src/HOL/Data_Structures/Interval_Tree.thy Mon May 10 14:28:37 2021 +0200
+++ b/src/HOL/Data_Structures/Interval_Tree.thy Mon May 10 16:14:34 2021 +0200
@@ -50,7 +50,7 @@
show b: "x \<le> x"
by (simp add: ivl_less_eq)
show c: "x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z"
- by (smt ivl_less_eq dual_order.trans less_trans)
+ using ivl_less_eq by fastforce
show d: "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y"
using ivl_less_eq a ivl_inj ivl_less by fastforce
show e: "x \<le> y \<or> y \<le> x"
--- a/src/HOL/Datatype_Examples/FAE_Sequence.thy Mon May 10 14:28:37 2021 +0200
+++ b/src/HOL/Datatype_Examples/FAE_Sequence.thy Mon May 10 16:14:34 2021 +0200
@@ -114,7 +114,10 @@
lemma fseq_at_infinite_Inr:
"\<lbrakk>infinite (fseq_at f x); fseq_eq (map_fseq Inr f) g\<rbrakk> \<Longrightarrow> \<exists>x'\<in>set_fseq g. x \<in> Basic_BNFs.setr x'"
- by transfer(auto simp add: seq_at_def vimage_def; smt (z3) finite_nat_set_iff_bounded_le mem_Collect_eq setr.intros)
+ apply transfer
+ apply (auto simp add: seq_at_def vimage_def)
+ apply (smt (verit, ccfv_SIG) finite_subset mem_Collect_eq setr.simps subsetI)
+ done
lemma fseq_at_Inr_infinite:
assumes "\<And>g. fseq_eq (map_fseq Inr f) g \<longrightarrow> (\<exists>x'\<in>set_fseq g. x \<in> Basic_BNFs.setr x')"
--- a/src/HOL/Datatype_Examples/Regex_ACIDZ.thy Mon May 10 14:28:37 2021 +0200
+++ b/src/HOL/Datatype_Examples/Regex_ACIDZ.thy Mon May 10 16:14:34 2021 +0200
@@ -204,7 +204,7 @@
next
case (d r t)
then show ?case
- by (smt (z3) ACIDZ.d R distribute.simps(3) elim_zeros.simps(2) elim_zeros.simps(3) elim_zeros_distribute_idem z)
+ by (smt (verit, ccfv_SIG) ACIDZ.d R elim_zeros.simps(2) elim_zeros_distribute_Zero elim_zeros_distribute_idem z)
next
case (A r r' s s')
then show ?case
@@ -212,7 +212,7 @@
next
case (C r r' s)
then show ?case
- by (smt (z3) ACIDZ.C elim_zeros.simps(2,3) z elim_zeros_ACIDZ_Zero)
+ by (smt (verit, best) ACIDZ.C R elim_zeros.simps(2) elim_zeros_ACIDZ_Zero z)
qed (auto simp: Let_def)
lemma AA': "r ~ r' \<Longrightarrow> s ~ s' \<Longrightarrow> t = elim_zeros (Alt r' s') \<Longrightarrow> Alt r s ~ t"
@@ -437,7 +437,7 @@
qed
private lemma CZ: "Conc Zero r ~~ Zero"
- by (smt (z3) R elim_zeros.simps(2) elim_zeros.simps(3) r_into_equivclp z)
+ by (metis R distribute.simps(3) elim_zeros.simps(3) elim_zeros_distribute_Zero r_into_equivclp z)
private lemma AZ: "Alt Zero r ~~ r"
by (smt (verit, ccfv_threshold) converse_r_into_equivclp converse_rtranclp_into_rtranclp
--- a/src/HOL/Hoare/Hoare_Logic_Abort.thy Mon May 10 14:28:37 2021 +0200
+++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy Mon May 10 16:14:34 2021 +0200
@@ -62,7 +62,7 @@
lemma tc_implies_pc:
"ValidTC p c q \<Longrightarrow> Valid p c q"
- by (smt Sem_deterministic ValidTC_def Valid_def image_iff)
+ by (smt (verit) Sem_deterministic ValidTC_def Valid_def image_iff)
lemma tc_extract_function:
"ValidTC p c q \<Longrightarrow> \<exists>f . \<forall>s . s \<in> p \<longrightarrow> f s \<in> q"
--- a/src/HOL/Homology/Simplices.thy Mon May 10 14:28:37 2021 +0200
+++ b/src/HOL/Homology/Simplices.thy Mon May 10 16:14:34 2021 +0200
@@ -2347,7 +2347,8 @@
show "chain_boundary (Suc p) (?h p c) + ?h (p - Suc 0) (chain_boundary p c) = (singular_subdivision p ^^ Suc n) c - c"
using chain_boundary_singular_subdivision [of "Suc p" X]
apply (simp add: chain_boundary_add f5 h k algebra_simps)
- by (smt add.assoc add.commute diff_add_cancel h(4) k(4) sc singular_subdivision_add)
+ apply (smt (verit, ccfv_threshold) add.commute add_diff_eq diff_add_cancel diff_diff_eq2 h(4) k(4) sc singular_subdivision_add)
+ done
qed (auto simp: k h singular_subdivision_diff)
qed
--- a/src/HOL/Library/Float.thy Mon May 10 14:28:37 2021 +0200
+++ b/src/HOL/Library/Float.thy Mon May 10 16:14:34 2021 +0200
@@ -2122,7 +2122,7 @@
proof cases
assume [simp]: "even j"
have "a * power_down prec a j \<le> b * power_down prec b j"
- by (smt IH(1) IH(2) \<open>even j\<close> lessI mult_mono' mult_mono_nonpos_nonneg power_down_even_nonneg)
+ by (metis IH(1) IH(2) \<open>even j\<close> lessI linear mult_mono mult_mono' mult_mono_nonpos_nonneg power_down_even_nonneg)
then have "truncate_down (Suc prec) (a * power_down prec a j) \<le> truncate_down (Suc prec) (b * power_down prec b j)"
by (auto intro!: truncate_down_mono simp: abs_le_square_iff[symmetric] abs_real_def)
then show ?thesis
@@ -2193,7 +2193,7 @@
proof cases
assume [simp]: "even j"
have "a * power_up prec a j \<le> b * power_up prec b j"
- by (smt IH(1) IH(2) \<open>even j\<close> lessI mult_mono' mult_mono_nonpos_nonneg power_up_even_nonneg)
+ by (metis IH(1) IH(2) \<open>even j\<close> lessI linear mult_mono mult_mono' mult_mono_nonpos_nonneg power_up_even_nonneg)
then have "truncate_up prec (a * power_up prec a j) \<le> truncate_up prec (b * power_up prec b j)"
by (auto intro!: truncate_up_mono simp: abs_le_square_iff[symmetric] abs_real_def)
then show ?thesis
--- a/src/HOL/Library/Interval_Float.thy Mon May 10 14:28:37 2021 +0200
+++ b/src/HOL/Library/Interval_Float.thy Mon May 10 16:14:34 2021 +0200
@@ -298,7 +298,7 @@
using Cons(1)[OF \<open>xs all_in Is\<close>]
split_correct[OF \<open>x' \<in>\<^sub>r I\<close>]
apply (auto simp add: list_ex_iff set_of_eq)
- by (smt length_Cons less_Suc_eq_0_disj nth_Cons_0 nth_Cons_Suc x_decomp)
+ by (smt (verit, ccfv_SIG) One_nat_def Suc_pred \<open>x \<noteq> []\<close> le_simps(3) length_greater_0_conv length_tl linorder_not_less list.sel(3) neq0_conv nth_Cons' x_decomp)
qed simp
--- a/src/HOL/Library/Poly_Mapping.thy Mon May 10 14:28:37 2021 +0200
+++ b/src/HOL/Library/Poly_Mapping.thy Mon May 10 16:14:34 2021 +0200
@@ -1796,7 +1796,7 @@
lemma keys_frag_extend: "Poly_Mapping.keys(frag_extend f c) \<subseteq> (\<Union>x \<in> Poly_Mapping.keys c. Poly_Mapping.keys(f x))"
unfolding frag_extend_def
- by (smt SUP_mono' keys_cmul keys_sum order_trans)
+ using keys_sum by fastforce
lemma frag_expansion: "a = frag_extend frag_of a"
proof -
--- a/src/HOL/Library/Ramsey.thy Mon May 10 14:28:37 2021 +0200
+++ b/src/HOL/Library/Ramsey.thy Mon May 10 16:14:34 2021 +0200
@@ -595,7 +595,7 @@
then obtain u where u: "bij_betw u {..<q} U"
using ex_bij_betw_nat_finite lessThan_atLeast0 by (fastforce simp add: nsets_def)
then have Usub: "U \<subseteq> {..<p}"
- by (smt \<open>U \<in> nsets {..<p} q\<close> mem_Collect_eq nsets_def)
+ by (smt (verit) U mem_Collect_eq nsets_def)
have u_nsets: "u ` X \<in> nsets {..<p} n" if "X \<in> nsets {..<q} n" for X n
proof -
have "inj_on u X"