# HG changeset patch
# User wenzelm
# Date 1620656074 -7200
# Node ID 26a1d66b9077bb29af1b9c416ddc26a67bc82930
# Parent  6e85281177df04e21f01a177674c515bd996b841
tuned proofs --- avoid z3, which is absent on arm64-linux;

diff -r 6e85281177df -r 26a1d66b9077 src/HOL/Algebra/Finite_Extensions.thy
--- 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:
diff -r 6e85281177df -r 26a1d66b9077 src/HOL/Data_Structures/Interval_Tree.thy
--- 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"
diff -r 6e85281177df -r 26a1d66b9077 src/HOL/Datatype_Examples/FAE_Sequence.thy
--- 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')"
diff -r 6e85281177df -r 26a1d66b9077 src/HOL/Datatype_Examples/Regex_ACIDZ.thy
--- 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
diff -r 6e85281177df -r 26a1d66b9077 src/HOL/Hoare/Hoare_Logic_Abort.thy
--- 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"
diff -r 6e85281177df -r 26a1d66b9077 src/HOL/Homology/Simplices.thy
--- 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
 
diff -r 6e85281177df -r 26a1d66b9077 src/HOL/Library/Float.thy
--- 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
diff -r 6e85281177df -r 26a1d66b9077 src/HOL/Library/Interval_Float.thy
--- 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
 
 
diff -r 6e85281177df -r 26a1d66b9077 src/HOL/Library/Poly_Mapping.thy
--- 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 -
diff -r 6e85281177df -r 26a1d66b9077 src/HOL/Library/Ramsey.thy
--- 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"