# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1712956760 -3600
# Node ID c06c95576ea954652282baa3e4876d3e8be4c6cc
# Parent  83fa23ca40e55c7a8f5e4d539b55ac103d1391dd
Tidied some messy proofs

diff -r 83fa23ca40e5 -r c06c95576ea9 src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Fri Apr 12 09:58:53 2024 +0100
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Fri Apr 12 22:19:20 2024 +0100
@@ -208,7 +208,7 @@
     and nb: "tmbound m t"
     and nle: "m \<le> length bs"
   shows "Itm vs (removen m bs) (decrtm m t) = Itm vs bs t"
-  using bnd nb nle by (induct t rule: tm.induct) (auto simp add: removen_nth)
+  using bnd nb nle by (induct t rule: tm.induct) (auto simp: removen_nth)
 
 primrec tmsubst0:: "tm \<Rightarrow> tm \<Rightarrow> tm"
   where
@@ -276,25 +276,33 @@
   | "tmadd a b = Add a b"
 
 lemma tmadd [simp]: "Itm vs bs (tmadd t s) = Itm vs bs (Add t s)"
-  apply (induct t s rule: tmadd.induct)
-                      apply (simp_all add: Let_def)
-  apply (case_tac "c1 +\<^sub>p c2 = 0\<^sub>p")
-   apply (case_tac "n1 \<le> n2")
-    apply simp_all
-   apply (case_tac "n1 = n2")
-    apply (simp_all add: algebra_simps)
-  apply (simp only: distrib_left [symmetric] polyadd [symmetric])
-  apply simp
-  done
+proof (induct t s rule: tmadd.induct)
+  case (1 n1 c1 r1 n2 c2 r2)
+  show ?case
+  proof (cases "c1 +\<^sub>p c2 = 0\<^sub>p")
+    case 0: True
+    show ?thesis
+    proof (cases "n1 \<le> n2")
+      case True
+      with 0 show ?thesis
+        apply (simp add: 1)
+        by (metis INum_int(2) Ipoly.simps(1) comm_semiring_class.distrib mult_eq_0_iff polyadd)
+    qed (use 0 1 in auto)
+  next
+    case False
+    then show ?thesis
+      using 1 comm_semiring_class.distrib by auto
+  qed
+qed auto
 
 lemma tmadd_nb0[simp]: "tmbound0 t \<Longrightarrow> tmbound0 s \<Longrightarrow> tmbound0 (tmadd t s)"
-  by (induct t s rule: tmadd.induct) (auto simp add: Let_def)
+  by (induct t s rule: tmadd.induct) (auto simp: Let_def)
 
 lemma tmadd_nb[simp]: "tmbound n t \<Longrightarrow> tmbound n s \<Longrightarrow> tmbound n (tmadd t s)"
-  by (induct t s rule: tmadd.induct) (auto simp add: Let_def)
+  by (induct t s rule: tmadd.induct) (auto simp: Let_def)
 
 lemma tmadd_blt[simp]: "tmboundslt n t \<Longrightarrow> tmboundslt n s \<Longrightarrow> tmboundslt n (tmadd t s)"
-  by (induct t s rule: tmadd.induct) (auto simp add: Let_def)
+  by (induct t s rule: tmadd.induct) (auto simp: Let_def)
 
 lemma tmadd_allpolys_npoly[simp]:
   "allpolys isnpoly t \<Longrightarrow> allpolys isnpoly s \<Longrightarrow> allpolys isnpoly (tmadd t s)"
@@ -316,7 +324,7 @@
   by (induct t arbitrary: n rule: tmmul.induct) auto
 
 lemma tmmul_blt[simp]: "tmboundslt n t \<Longrightarrow> tmboundslt n (tmmul t i)"
-  by (induct t arbitrary: i rule: tmmul.induct) (auto simp add: Let_def)
+  by (induct t arbitrary: i rule: tmmul.induct) (auto simp: Let_def)
 
 lemma tmmul_allpolys_npoly[simp]:
   assumes "SORT_CONSTRAINT('a::field_char_0)"
@@ -381,21 +389,19 @@
 lemma polynate_stupid:
   assumes "SORT_CONSTRAINT('a::field_char_0)"
   shows "polynate t = 0\<^sub>p \<Longrightarrow> Ipoly bs t = (0::'a)"
-  apply (subst polynate[symmetric])
-  apply simp
-  done
+  by (metis INum_int(2) Ipoly.simps(1) polynate)
 
 lemma simptm_ci[simp]: "Itm vs bs (simptm t) = Itm vs bs t"
-  by (induct t rule: simptm.induct) (auto simp add: Let_def polynate_stupid)
+  by (induct t rule: simptm.induct) (auto simp: Let_def polynate_stupid)
 
 lemma simptm_tmbound0[simp]: "tmbound0 t \<Longrightarrow> tmbound0 (simptm t)"
-  by (induct t rule: simptm.induct) (auto simp add: Let_def)
+  by (induct t rule: simptm.induct) (auto simp: Let_def)
 
 lemma simptm_nb[simp]: "tmbound n t \<Longrightarrow> tmbound n (simptm t)"
-  by (induct t rule: simptm.induct) (auto simp add: Let_def)
+  by (induct t rule: simptm.induct) (auto simp: Let_def)
 
 lemma simptm_nlt[simp]: "tmboundslt n t \<Longrightarrow> tmboundslt n (simptm t)"
-  by (induct t rule: simptm.induct) (auto simp add: Let_def)
+  by (induct t rule: simptm.induct) (auto simp: Let_def)
 
 lemma [simp]: "isnpoly 0\<^sub>p"
   and [simp]: "isnpoly (C (1, 1))"
@@ -404,7 +410,7 @@
 lemma simptm_allpolys_npoly[simp]:
   assumes "SORT_CONSTRAINT('a::field_char_0)"
   shows "allpolys isnpoly (simptm p)"
-  by (induct p rule: simptm.induct) (auto simp add: Let_def)
+  by (induct p rule: simptm.induct) (auto simp: Let_def)
 
 declare let_cong[fundef_cong del]
 
@@ -422,24 +428,15 @@
 declare let_cong[fundef_cong]
 
 lemma split0_stupid[simp]: "\<exists>x y. (x, y) = split0 p"
-  apply (rule exI[where x="fst (split0 p)"])
-  apply (rule exI[where x="snd (split0 p)"])
-  apply simp
-  done
+  using prod.collapse by blast
 
 lemma split0:
   "tmbound 0 (snd (split0 t)) \<and> Itm vs bs (CNP 0 (fst (split0 t)) (snd (split0 t))) = Itm vs bs t"
-  apply (induct t rule: split0.induct)
-          apply simp
-         apply (simp add: Let_def split_def field_simps)
-        apply (simp add: Let_def split_def field_simps)
-       apply (simp add: Let_def split_def field_simps)
-      apply (simp add: Let_def split_def field_simps)
-     apply (simp add: Let_def split_def field_simps)
-    apply (simp add: Let_def split_def mult.assoc distrib_left[symmetric])
-   apply (simp add: Let_def split_def field_simps)
-  apply (simp add: Let_def split_def field_simps)
-  done
+proof (induct t rule: split0.induct)
+  case (7 c t)
+  then show ?case
+    by (simp add: Let_def split_def mult.assoc flip: distrib_left)
+qed (auto simp: Let_def split_def field_simps)
 
 lemma split0_ci: "split0 t = (c',t') \<Longrightarrow> Itm vs bs t = Itm vs bs (CNP 0 c' t')"
 proof -
@@ -472,21 +469,21 @@
 lemma split0_nb:
   assumes nb: "tmbound n t"
   shows "tmbound n (snd (split0 t))"
-  using nb by (induct t rule: split0.induct) (auto simp add: Let_def split_def)
+  using nb by (induct t rule: split0.induct) (auto simp: Let_def split_def)
 
 lemma split0_blt:
   assumes nb: "tmboundslt n t"
   shows "tmboundslt n (snd (split0 t))"
-  using nb by (induct t rule: split0.induct) (auto simp add: Let_def split_def)
+  using nb by (induct t rule: split0.induct) (auto simp: Let_def split_def)
 
 lemma tmbound_split0: "tmbound 0 t \<Longrightarrow> Ipoly vs (fst (split0 t)) = 0"
-  by (induct t rule: split0.induct) (auto simp add: Let_def split_def)
+  by (induct t rule: split0.induct) (auto simp: Let_def split_def)
 
 lemma tmboundslt_split0: "tmboundslt n t \<Longrightarrow> Ipoly vs (fst (split0 t)) = 0 \<or> n > 0"
-  by (induct t rule: split0.induct) (auto simp add: Let_def split_def)
+  by (induct t rule: split0.induct) (auto simp: Let_def split_def)
 
 lemma tmboundslt0_split0: "tmboundslt 0 t \<Longrightarrow> Ipoly vs (fst (split0 t)) = 0"
-  by (induct t rule: split0.induct) (auto simp add: Let_def split_def)
+  by (induct t rule: split0.induct) (auto simp: Let_def split_def)
 
 lemma allpolys_split0: "allpolys isnpoly p \<Longrightarrow> allpolys isnpoly (snd (split0 p))"
   by (induct p rule: split0.induct) (auto simp  add: isnpoly_def Let_def split_def)
@@ -764,7 +761,7 @@
     from A(1)[OF bnd nb nle] show ?thesis .
   qed
   then show ?case by auto
-qed (auto simp add: decrtm removen_nth)
+qed (auto simp: decrtm removen_nth)
 
 primrec subst0 :: "tm \<Rightarrow> fm \<Rightarrow> fm"
   where
@@ -849,7 +846,7 @@
       by (simp add: incrtm0[where x="x" and bs="bs" and t="t"])
   qed
   then show ?case by simp
-qed (auto simp add: tmsubst)
+qed (auto simp: tmsubst)
 
 lemma subst_nb:
   assumes "tmbound m t"
@@ -926,36 +923,38 @@
   where "evaldjf f ps \<equiv> foldr (djf f) ps F"
 
 lemma djf_Or: "Ifm vs bs (djf f p q) = Ifm vs bs (Or (f p) q)"
-  apply (cases "q = T")
-   apply (simp add: djf_def)
-  apply (cases "q = F")
-   apply (simp add: djf_def)
-  apply (cases "f p")
-              apply (simp_all add: Let_def djf_def)
-  done
+  by (cases "f p") (simp_all add: Let_def djf_def)
 
 lemma evaldjf_ex: "Ifm vs bs (evaldjf f ps) \<longleftrightarrow> (\<exists>p \<in> set ps. Ifm vs bs (f p))"
   by (induct ps) (simp_all add: evaldjf_def djf_Or)
 
 lemma evaldjf_bound0:
-  assumes "\<forall>x\<in> set xs. bound0 (f x)"
+  assumes "\<forall>x \<in> set xs. bound0 (f x)"
   shows "bound0 (evaldjf f xs)"
   using assms
-  apply (induct xs)
-   apply (auto simp add: evaldjf_def djf_def Let_def)
-  apply (case_tac "f a")
-              apply auto
-  done
+proof (induct xs)
+  case Nil
+  then show ?case
+    by (simp add: evaldjf_def)
+next
+  case (Cons a xs)
+  then show ?case
+    by (cases "f a") (simp_all add: evaldjf_def djf_def Let_def)
+qed
 
 lemma evaldjf_qf:
   assumes "\<forall>x\<in> set xs. qfree (f x)"
   shows "qfree (evaldjf f xs)"
   using assms
-  apply (induct xs)
-   apply (auto simp add: evaldjf_def djf_def Let_def)
-  apply (case_tac "f a")
-              apply auto
-  done
+proof (induct xs)
+  case Nil
+  then show ?case
+    by (simp add: evaldjf_def)
+next
+  case (Cons a xs)
+  then show ?case
+    by (cases "f a") (simp_all add: evaldjf_def djf_def Let_def)
+qed
 
 fun disjuncts :: "fm \<Rightarrow> fm list"
   where
@@ -1100,71 +1099,32 @@
 definition "neq p = not (eq p)"
 
 lemma lt: "allpolys isnpoly p \<Longrightarrow> Ifm vs bs (lt p) = Ifm vs bs (Lt p)"
-  apply (simp add: lt_def)
-  apply (cases p)
-        apply simp_all
-  apply (rename_tac poly, case_tac poly)
-         apply (simp_all add: isnpoly_def)
-  done
+  by (auto simp: lt_def isnpoly_def split: tm.split poly.split)
 
 lemma le: "allpolys isnpoly p \<Longrightarrow> Ifm vs bs (le p) = Ifm vs bs (Le p)"
-  apply (simp add: le_def)
-  apply (cases p)
-        apply simp_all
-  apply (rename_tac poly, case_tac poly)
-         apply (simp_all add: isnpoly_def)
-  done
+  by (auto simp: le_def isnpoly_def split: tm.split poly.split)
 
 lemma eq: "allpolys isnpoly p \<Longrightarrow> Ifm vs bs (eq p) = Ifm vs bs (Eq p)"
-  apply (simp add: eq_def)
-  apply (cases p)
-        apply simp_all
-  apply (rename_tac poly, case_tac poly)
-         apply (simp_all add: isnpoly_def)
-  done
+  by (auto simp: eq_def isnpoly_def split: tm.split poly.split)
 
 lemma neq: "allpolys isnpoly p \<Longrightarrow> Ifm vs bs (neq p) = Ifm vs bs (NEq p)"
   by (simp add: neq_def eq)
 
 lemma lt_lin: "tmbound0 p \<Longrightarrow> islin (lt p)"
-  apply (simp add: lt_def)
-  apply (cases p)
-        apply simp_all
-   apply (rename_tac poly, case_tac poly)
-          apply simp_all
-  apply (rename_tac nat a b, case_tac nat)
-   apply simp_all
-  done
+  using islin_stupid
+  by(auto simp: lt_def isnpoly_def split: tm.split poly.split)
 
 lemma le_lin: "tmbound0 p \<Longrightarrow> islin (le p)"
-  apply (simp add: le_def)
-  apply (cases p)
-        apply simp_all
-   apply (rename_tac poly, case_tac poly)
-          apply simp_all
-  apply (rename_tac nat a b, case_tac nat)
-   apply simp_all
-  done
+  using islin_stupid
+  by(auto simp: le_def isnpoly_def split: tm.split poly.split)
 
 lemma eq_lin: "tmbound0 p \<Longrightarrow> islin (eq p)"
-  apply (simp add: eq_def)
-  apply (cases p)
-        apply simp_all
-   apply (rename_tac poly, case_tac poly)
-          apply simp_all
-  apply (rename_tac nat a b, case_tac nat)
-   apply simp_all
-  done
+  using islin_stupid
+  by(auto simp: eq_def isnpoly_def split: tm.split poly.split)
 
 lemma neq_lin: "tmbound0 p \<Longrightarrow> islin (neq p)"
-  apply (simp add: neq_def eq_def)
-  apply (cases p)
-        apply simp_all
-   apply (rename_tac poly, case_tac poly)
-          apply simp_all
-  apply (rename_tac nat a b, case_tac nat)
-   apply simp_all
-  done
+  using islin_stupid
+  by(auto simp: neq_def eq_def isnpoly_def split: tm.split poly.split)
 
 definition "simplt t = (let (c,s) = split0 (simptm t) in if c= 0\<^sub>p then lt s else Lt (CNP 0 c s))"
 definition "simple t = (let (c,s) = split0 (simptm t) in if c= 0\<^sub>p then le s else Le (CNP 0 c s))"
@@ -1176,7 +1136,7 @@
   shows "islin (simplt t)"
   unfolding simplt_def
   using split0_nb0'
-  by (auto simp add: lt_lin Let_def split_def isnpoly_fst_split0[OF simptm_allpolys_npoly]
+  by (auto simp: lt_lin Let_def split_def isnpoly_fst_split0[OF simptm_allpolys_npoly]
       islin_stupid allpolys_split0[OF simptm_allpolys_npoly])
 
 lemma simple_islin [simp]:
@@ -1184,7 +1144,7 @@
   shows "islin (simple t)"
   unfolding simple_def
   using split0_nb0'
-  by (auto simp add: Let_def split_def isnpoly_fst_split0[OF simptm_allpolys_npoly]
+  by (auto simp: Let_def split_def isnpoly_fst_split0[OF simptm_allpolys_npoly]
       islin_stupid allpolys_split0[OF simptm_allpolys_npoly] le_lin)
 
 lemma simpeq_islin [simp]:
@@ -1192,7 +1152,7 @@
   shows "islin (simpeq t)"
   unfolding simpeq_def
   using split0_nb0'
-  by (auto simp add: Let_def split_def isnpoly_fst_split0[OF simptm_allpolys_npoly]
+  by (auto simp: Let_def split_def isnpoly_fst_split0[OF simptm_allpolys_npoly]
       islin_stupid allpolys_split0[OF simptm_allpolys_npoly] eq_lin)
 
 lemma simpneq_islin [simp]:
@@ -1200,7 +1160,7 @@
   shows "islin (simpneq t)"
   unfolding simpneq_def
   using split0_nb0'
-  by (auto simp add: Let_def split_def isnpoly_fst_split0[OF simptm_allpolys_npoly]
+  by (auto simp: Let_def split_def isnpoly_fst_split0[OF simptm_allpolys_npoly]
       islin_stupid allpolys_split0[OF simptm_allpolys_npoly] neq_lin)
 
 lemma really_stupid: "\<not> (\<forall>c1 s'. (c1, s') \<noteq> split0 s)"
@@ -1213,7 +1173,7 @@
     and "allpolys isnpoly (snd (split0 t))"
   using *
   by (induct t rule: split0.induct)
-    (auto simp add: Let_def split_def polyadd_norm polymul_norm polyneg_norm
+    (auto simp: Let_def split_def polyadd_norm polymul_norm polyneg_norm
       polysub_norm really_stupid)
 
 lemma simplt[simp]: "Ifm vs bs (simplt t) = Ifm vs bs (Lt t)"
@@ -1291,44 +1251,24 @@
 qed
 
 lemma lt_nb: "tmbound0 t \<Longrightarrow> bound0 (lt t)"
-  apply (simp add: lt_def)
-  apply (cases t)
-        apply auto
-  apply (rename_tac poly, case_tac poly)
-         apply auto
-  done
+  by(auto simp: lt_def split: tm.split poly.split)
 
 lemma le_nb: "tmbound0 t \<Longrightarrow> bound0 (le t)"
-  apply (simp add: le_def)
-  apply (cases t)
-        apply auto
-  apply (rename_tac poly, case_tac poly)
-         apply auto
-  done
+  by(auto simp: le_def split: tm.split poly.split)
 
 lemma eq_nb: "tmbound0 t \<Longrightarrow> bound0 (eq t)"
-  apply (simp add: eq_def)
-  apply (cases t)
-        apply auto
-  apply (rename_tac poly, case_tac poly)
-         apply auto
-  done
+  by(auto simp: eq_def split: tm.split poly.split)
 
 lemma neq_nb: "tmbound0 t \<Longrightarrow> bound0 (neq t)"
-  apply (simp add: neq_def eq_def)
-  apply (cases t)
-        apply auto
-  apply (rename_tac poly, case_tac poly)
-         apply auto
-  done
-
+  by(auto simp: neq_def eq_def split: tm.split poly.split)
+
+(*THE FOLLOWING PROOFS MIGHT BE COMBINED*)
 lemma simplt_nb[simp]:
-  assumes "SORT_CONSTRAINT('a::field_char_0)"
-  shows "tmbound0 t \<Longrightarrow> bound0 (simplt t)"
+  assumes "SORT_CONSTRAINT('a::field_char_0)" and t: "tmbound0 t"
+  shows "bound0 (simplt t)"
 proof (simp add: simplt_def Let_def split_def)
-  assume "tmbound0 t"
-  then have *: "tmbound0 (simptm t)"
-    by simp
+  have *: "tmbound0 (simptm t)"
+    using t by simp
   let ?c = "fst (split0 (simptm t))"
   from tmbound_split0[OF *[unfolded tmbound0_tmbound_iff[symmetric]]]
   have th: "\<forall>bs. Ipoly bs ?c = Ipoly bs 0\<^sub>p"
@@ -1344,12 +1284,11 @@
 qed
 
 lemma simple_nb[simp]:
-  assumes "SORT_CONSTRAINT('a::field_char_0)"
-  shows "tmbound0 t \<Longrightarrow> bound0 (simple t)"
+  assumes "SORT_CONSTRAINT('a::field_char_0)" and t: "tmbound0 t"
+  shows "bound0 (simple t)"
 proof(simp add: simple_def Let_def split_def)
-  assume "tmbound0 t"
-  then have *: "tmbound0 (simptm t)"
-    by simp
+  have *: "tmbound0 (simptm t)"
+    using t by simp
   let ?c = "fst (split0 (simptm t))"
   from tmbound_split0[OF *[unfolded tmbound0_tmbound_iff[symmetric]]]
   have th: "\<forall>bs. Ipoly bs ?c = Ipoly bs 0\<^sub>p"
@@ -1365,12 +1304,11 @@
 qed
 
 lemma simpeq_nb[simp]:
-  assumes "SORT_CONSTRAINT('a::field_char_0)"
-  shows "tmbound0 t \<Longrightarrow> bound0 (simpeq t)"
+  assumes "SORT_CONSTRAINT('a::field_char_0)" and t: "tmbound0 t"
+  shows "bound0 (simpeq t)"
 proof (simp add: simpeq_def Let_def split_def)
-  assume "tmbound0 t"
-  then have *: "tmbound0 (simptm t)"
-    by simp
+  have *: "tmbound0 (simptm t)"
+    using t by simp
   let ?c = "fst (split0 (simptm t))"
   from tmbound_split0[OF *[unfolded tmbound0_tmbound_iff[symmetric]]]
   have th: "\<forall>bs. Ipoly bs ?c = Ipoly bs 0\<^sub>p"
@@ -1386,12 +1324,11 @@
 qed
 
 lemma simpneq_nb[simp]:
-  assumes "SORT_CONSTRAINT('a::field_char_0)"
-  shows "tmbound0 t \<Longrightarrow> bound0 (simpneq t)"
+  assumes "SORT_CONSTRAINT('a::field_char_0)" and t: "tmbound0 t"
+  shows "bound0 (simpneq t)"
 proof (simp add: simpneq_def Let_def split_def)
-  assume "tmbound0 t"
-  then have *: "tmbound0 (simptm t)"
-    by simp
+  have *: "tmbound0 (simptm t)"
+    using t by simp
   let ?c = "fst (split0 (simptm t))"
   from tmbound_split0[OF *[unfolded tmbound0_tmbound_iff[symmetric]]]
   have th: "\<forall>bs. Ipoly bs ?c = Ipoly bs 0\<^sub>p"
@@ -1419,35 +1356,30 @@
   where "list_disj ps \<equiv> foldr disj ps F"
 
 lemma list_conj: "Ifm vs bs (list_conj ps) = (\<forall>p\<in> set ps. Ifm vs bs p)"
-  by (induct ps) (auto simp add: list_conj_def)
+  by (induct ps) (auto simp: list_conj_def)
 
 lemma list_conj_qf: " \<forall>p\<in> set ps. qfree p \<Longrightarrow> qfree (list_conj ps)"
-  by (induct ps) (auto simp add: list_conj_def)
+  by (induct ps) (auto simp: list_conj_def)
 
 lemma list_disj: "Ifm vs bs (list_disj ps) = (\<exists>p\<in> set ps. Ifm vs bs p)"
-  by (induct ps) (auto simp add: list_disj_def)
+  by (induct ps) (auto simp: list_disj_def)
 
 lemma conj_boundslt: "boundslt n p \<Longrightarrow> boundslt n q \<Longrightarrow> boundslt n (conj p q)"
   unfolding conj_def by auto
 
 lemma conjs_nb: "bound n p \<Longrightarrow> \<forall>q\<in> set (conjs p). bound n q"
-  apply (induct p rule: conjs.induct)
-              apply (unfold conjs.simps)
-              apply (unfold set_append)
-              apply (unfold ball_Un)
-              apply (unfold bound.simps)
-              apply auto
-  done
+proof (induct p rule: conjs.induct)
+  case (1 p q)
+  then show ?case 
+    unfolding conjs.simps bound.simps by fastforce
+qed auto
 
 lemma conjs_boundslt: "boundslt n p \<Longrightarrow> \<forall>q\<in> set (conjs p). boundslt n q"
-  apply (induct p rule: conjs.induct)
-              apply (unfold conjs.simps)
-              apply (unfold set_append)
-              apply (unfold ball_Un)
-              apply (unfold boundslt.simps)
-              apply blast
-             apply simp_all
-  done
+proof (induct p rule: conjs.induct)
+  case (1 p q)
+  then show ?case 
+    unfolding conjs.simps bound.simps by fastforce
+qed auto
 
 lemma list_conj_boundslt: " \<forall>p\<in> set ps. boundslt n p \<Longrightarrow> boundslt n (list_conj ps)"
   by (induct ps) (auto simp: list_conj_def)
@@ -1503,7 +1435,7 @@
   also fix y have "\<dots> = (\<exists>x. (Ifm vs (y#bs) ?cyes) \<and> (Ifm vs (x#bs) ?cno))"
     using bound0_I[OF yes_nb, where bs="bs" and b'="y"] by blast
   also have "\<dots> = (Ifm vs bs (decr0 ?cyes) \<and> Ifm vs bs (E ?cno))"
-    by (auto simp add: decr0[OF yes_nb] simp del: partition_filter_conv)
+    by (auto simp: decr0[OF yes_nb] simp del: partition_filter_conv)
   also have "\<dots> = (Ifm vs bs (conj (decr0 ?cyes) (qe ?cno)))"
     using qe[rule_format, OF no_qf] by auto
   finally have "Ifm vs bs (E p) = Ifm vs bs (CJNB qe p)"
@@ -1546,25 +1478,13 @@
   by (induct p rule: simpfm.induct) auto
 
 lemma lt_qf[simp]: "qfree (lt t)"
-  apply (cases t)
-        apply (auto simp add: lt_def)
-  apply (rename_tac poly, case_tac poly)
-         apply auto
-  done
+  by(auto simp: lt_def split: tm.split poly.split)
 
 lemma le_qf[simp]: "qfree (le t)"
-  apply (cases t)
-        apply (auto simp add: le_def)
-  apply (rename_tac poly, case_tac poly)
-         apply auto
-  done
+  by(auto simp: le_def split: tm.split poly.split)
 
 lemma eq_qf[simp]: "qfree (eq t)"
-  apply (cases t)
-        apply (auto simp add: eq_def)
-  apply (rename_tac poly, case_tac poly)
-         apply auto
-  done
+  by(auto simp: eq_def split: tm.split poly.split)
 
 lemma neq_qf[simp]: "qfree (neq t)"
   by (simp add: neq_def)
@@ -1671,19 +1591,19 @@
   shows "\<exists>z. \<forall>x < z. Ifm vs (x#bs) (minusinf p) \<longleftrightarrow> Ifm vs (x#bs) p"
   using assms
 proof (induct p rule: minusinf.induct)
-  case 1
+  case (1 p q)
+  then obtain zp zq where zp: "\<forall>x<zp. Ifm vs (x # bs) (minusinf p) = Ifm vs (x # bs) p"
+       and zq: "\<forall>x<zq. Ifm vs (x # bs) (minusinf q) = Ifm vs (x # bs) q"
+    by force
   then show ?case
-    apply auto
-    apply (rule_tac x="min z za" in exI)
-    apply auto
-    done
+    by (rule_tac x="min zp zq" in exI) auto
 next
-  case 2
+  case (2 p q)
+  then obtain zp zq where zp: "\<forall>x<zp. Ifm vs (x # bs) (minusinf p) = Ifm vs (x # bs) p"
+       and zq: "\<forall>x<zq. Ifm vs (x # bs) (minusinf q) = Ifm vs (x # bs) q"
+    by force
   then show ?case
-    apply auto
-    apply (rule_tac x="min z za" in exI)
-    apply auto
-    done
+    by (rule_tac x="min zp zq" in exI) auto
 next
   case (3 c e)
   then have nbe: "tmbound0 e"
@@ -1876,19 +1796,19 @@
   shows "\<exists>z. \<forall>x > z. Ifm vs (x#bs) (plusinf p) \<longleftrightarrow> Ifm vs (x#bs) p"
   using assms
 proof (induct p rule: plusinf.induct)
-  case 1
+  case (1 p q)
+  then obtain zp zq where zp: "\<forall>x>zp. Ifm vs (x # bs) (plusinf p) = Ifm vs (x # bs) p"
+       and zq: "\<forall>x>zq. Ifm vs (x # bs) (plusinf q) = Ifm vs (x # bs) q"
+    by force
   then show ?case
-    apply auto
-    apply (rule_tac x="max z za" in exI)
-    apply auto
-    done
+    by (rule_tac x="max zp zq" in exI) auto
 next
-  case 2
+  case (2 p q)
+  then obtain zp zq where zp: "\<forall>x>zp. Ifm vs (x # bs) (plusinf p) = Ifm vs (x # bs) p"
+       and zq: "\<forall>x>zq. Ifm vs (x # bs) (plusinf q) = Ifm vs (x # bs) q"
+    by force
   then show ?case
-    apply auto
-    apply (rule_tac x="max z za" in exI)
-    apply auto
-    done
+    by (rule_tac x="max zp zq" in exI) auto
 next
   case (3 c e)
   then have nbe: "tmbound0 e"
@@ -2072,10 +1992,10 @@
 qed auto
 
 lemma minusinf_nb: "islin p \<Longrightarrow> bound0 (minusinf p)"
-  by (induct p rule: minusinf.induct) (auto simp add: eq_nb lt_nb le_nb)
+  by (induct p rule: minusinf.induct) (auto simp: eq_nb lt_nb le_nb)
 
 lemma plusinf_nb: "islin p \<Longrightarrow> bound0 (plusinf p)"
-  by (induct p rule: minusinf.induct) (auto simp add: eq_nb lt_nb le_nb)
+  by (induct p rule: minusinf.induct) (auto simp: eq_nb lt_nb le_nb)
 
 lemma minusinf_ex:
   assumes lp: "islin p"
@@ -2140,16 +2060,14 @@
       Ipoly vs c < 0 \<and> Ipoly vs c * x \<le> - Itm vs (x#bs) s \<or>
       Ipoly vs c > 0 \<and> Ipoly vs c * x \<ge> - Itm vs (x#bs) s"
     using lp nmi ex
-    apply (induct p rule: minusinf.induct)
-                        apply (auto simp add: eq le lt polyneg_norm)
-      apply (auto simp add: linorder_not_less order_le_less)
-    done
+    by (induct p rule: minusinf.induct)
+       (auto simp: eq le lt polyneg_norm linorder_not_less order_le_less)
   then obtain c s where csU: "(c, s) \<in> set (uset p)"
     and x: "(Ipoly vs c < 0 \<and> Ipoly vs c * x \<le> - Itm vs (x#bs) s) \<or>
       (Ipoly vs c > 0 \<and> Ipoly vs c * x \<ge> - Itm vs (x#bs) s)" by blast
   then have "x \<ge> (- Itm vs (x#bs) s) / Ipoly vs c"
     using divide_le_eq[of "- Itm vs (x#bs) s" "Ipoly vs c" x]
-    by (auto simp add: mult.commute)
+    by (auto simp: mult.commute)
   then show ?thesis
     using csU by auto
 qed
@@ -2183,10 +2101,8 @@
       Ipoly vs c < 0 \<and> Ipoly vs c * x \<ge> - Itm vs (x#bs) s \<or>
       Ipoly vs c > 0 \<and> Ipoly vs c * x \<le> - Itm vs (x#bs) s"
     using lp nmi ex
-    apply (induct p rule: minusinf.induct)
-                        apply (auto simp add: eq le lt polyneg_norm)
-      apply (auto simp add: linorder_not_less order_le_less)
-    done
+    by (induct p rule: minusinf.induct)
+       (auto simp: eq le lt polyneg_norm linorder_not_less order_le_less)
   then obtain c s
     where c_s: "(c, s) \<in> set (uset p)"
       and "Ipoly vs c < 0 \<and> Ipoly vs c * x \<ge> - Itm vs (x#bs) s \<or>
@@ -2194,7 +2110,7 @@
     by blast
   then have "x \<le> (- Itm vs (x#bs) s) / Ipoly vs c"
     using le_divide_eq[of x "- Itm vs (x#bs) s" "Ipoly vs c"]
-    by (auto simp add: mult.commute)
+    by (auto simp: mult.commute)
   then show ?thesis
     using c_s by auto
 qed
@@ -2248,7 +2164,7 @@
     case N: 2
     from px pos_less_divide_eq[OF N, where a="x" and b="-?Nt x s"]
     have px': "x < - ?Nt x s / ?N c"
-      by (auto simp add: not_less field_simps)
+      by (auto simp: not_less field_simps)
     from ycs show ?thesis
     proof
       assume y: "y < - ?Nt x s / ?N c"
@@ -2272,7 +2188,7 @@
     case N: 3
     from px neg_divide_less_eq[OF N, where a="x" and b="-?Nt x s"]
     have px': "x > - ?Nt x s / ?N c"
-      by (auto simp add: not_less field_simps)
+      by (auto simp: not_less field_simps)
     from ycs show ?thesis
     proof
       assume y: "y > - ?Nt x s / ?N c"
@@ -2449,7 +2365,7 @@
     show ?thesis
       by (simp add: field_simps tmbound0_I[OF lin(3), of vs x bs y] sum_eq[symmetric])
   qed
-qed (auto simp add: tmbound0_I[where vs=vs and bs="bs" and b="y" and b'="x"]
+qed (auto simp: tmbound0_I[where vs=vs and bs="bs" and b="y" and b'="x"]
   bound0_I[where vs=vs and bs="bs" and b="y" and b'="x"])
 
 lemma inf_uset:
@@ -3261,7 +3177,7 @@
     Ifm vs (((- Itm vs (x#bs) t /  Ipoly vs c + - Itm vs (x#bs) s / Ipoly vs d) /2)#bs) p"
   using lp
   by (induct p rule: islin.induct)
-    (auto simp add: tmbound0_I
+    (auto simp: tmbound0_I
       [where b = "(- (Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup>) - (Itm vs (x # bs) s / \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>)) / 2"
         and b' = x and bs = bs and vs = vs]
       msubsteq msubstneq msubstlt [OF nc nd] msubstle [OF nc nd])
@@ -3272,7 +3188,7 @@
     and "tmbound0 s"
   shows "bound0 (msubst p ((c,t),(d,s)))"
   using assms
-  by (induct p rule: islin.induct) (auto simp add: msubsteq_nb msubstneq_nb msubstlt_nb msubstle_nb)
+  by (induct p rule: islin.induct) (auto simp: msubsteq_nb msubstneq_nb msubstlt_nb msubstle_nb)
 
 lemma fr_eq_msubst:
   assumes lp: "islin p"
@@ -3315,7 +3231,7 @@
 lemma simpfm_lin:
   assumes "SORT_CONSTRAINT('a::field_char_0)"
   shows "qfree p \<Longrightarrow> islin (simpfm p)"
-  by (induct p rule: simpfm.induct) (auto simp add: conj_lin disj_lin)
+  by (induct p rule: simpfm.induct) (auto simp: conj_lin disj_lin)
 
 definition "ferrack p \<equiv>
   let
@@ -3395,10 +3311,7 @@
     by simp
   also have "\<dots> \<longleftrightarrow> ?rhs"
     using decr0[OF th1, of vs x bs]
-    apply (simp add: ferrack_def Let_def)
-    apply (cases "?mp = T \<or> ?pp = T")
-     apply auto
-    done
+    by (cases "?mp = T \<or> ?pp = T") (auto simp: ferrack_def Let_def)
   finally show ?thesis
     using thqf by blast
 qed
@@ -3468,11 +3381,8 @@
       case z: 4
       from z have ?F
         using ct
-        apply -
-        apply (rule bexI[where x = "(c,t)"])
-         apply simp_all
-        apply (rule bexI[where x = "(d,s)"])
-         apply simp_all
+        apply (intro bexI[where x = "(c,t)"]; simp)
+        apply (intro bexI[where x = "(d,s)"]; simp)
         done
       then show ?thesis by blast
     qed
@@ -3553,7 +3463,7 @@
     Ifm vs (Itm vs (x#bs) t /  Ipoly vs c #bs) p"
   using lp pos
   by (induct p rule: islin.induct)
-    (auto simp add: msubsteq2 msubstltpos[OF pos] msubstlepos[OF pos]
+    (auto simp: msubsteq2 msubstltpos[OF pos] msubstlepos[OF pos]
       tmbound0_I[of _ vs "Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup>" bs x]
       bound0_I[of _ vs "Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup>" bs x] field_simps)
 
@@ -3573,7 +3483,7 @@
   shows "Ifm vs (x#bs) (msubstneg p c t) = Ifm vs (Itm vs (x#bs) t /  Ipoly vs c #bs) p"
   using lp pos
   by (induct p rule: islin.induct)
-    (auto simp add: msubsteq2 msubstltneg[OF pos] msubstleneg[OF pos]
+    (auto simp: msubsteq2 msubstltneg[OF pos] msubstleneg[OF pos]
       tmbound0_I[of _ vs "Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup>" bs x]
       bound0_I[of _ vs "Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup>" bs x] field_simps)
 
@@ -3596,12 +3506,12 @@
     case c: 1
     from c msubstneg_I[OF lp c, of x bs t] lt[OF anc(1), of vs "x#bs"] lt[OF anc(2), of vs "x#bs"]
     show ?thesis
-      by (auto simp add: msubst2_def)
+      by (auto simp: msubst2_def)
   next
     case c: 2
     from c msubstpos_I[OF lp c, of x bs t] lt[OF anc(1), of vs "x#bs"] lt[OF anc(2), of vs "x#bs"]
     show ?thesis
-      by (auto simp add: msubst2_def)
+      by (auto simp: msubst2_def)
   qed
 qed
 
@@ -3624,7 +3534,7 @@
   shows "bound0 (msubstpos p c t)"
   using lp tnb
   by (induct p c t rule: msubstpos.induct)
-    (auto simp add: msubsteq2_nb msubstltpos_nb msubstlepos_nb)
+    (auto simp: msubsteq2_nb msubstltpos_nb msubstlepos_nb)
 
 lemma msubstneg_nb:
   assumes "SORT_CONSTRAINT('a::field_char_0)"
@@ -3633,7 +3543,7 @@
   shows "bound0 (msubstneg p c t)"
   using lp tnb
   by (induct p c t rule: msubstneg.induct)
-    (auto simp add: msubsteq2_nb msubstltneg_nb msubstleneg_nb)
+    (auto simp: msubsteq2_nb msubstltneg_nb msubstleneg_nb)
 
 lemma msubst2_nb:
   assumes "SORT_CONSTRAINT('a::field_char_0)"
@@ -3652,7 +3562,7 @@
   by simp
 
 lemma islin_qf: "islin p \<Longrightarrow> qfree p"
-  by (induct p rule: islin.induct) (auto simp add: bound0_qf)
+  by (induct p rule: islin.induct) (auto simp: bound0_qf)
 
 lemma fr_eq_msubst2:
   assumes lp: "islin p"
@@ -3689,7 +3599,7 @@
         by (simp add: polyneg_norm nn)
       then have nn2: "\<lparr>n *\<^sub>p(C (-2,1)) \<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0" "\<lparr>n \<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0"
         using H(2) nn' nn
-        by (auto simp add: msubst2_def lt zero_less_mult_iff mult_less_0_iff)
+        by (auto simp: msubst2_def lt zero_less_mult_iff mult_less_0_iff)
       from msubst2[OF lp nn nn2(1), of x bs t]
       have "\<lparr>n\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0 \<and> Ifm vs (- Itm vs (x # bs) t / (\<lparr>n\<rparr>\<^sub>p\<^bsup>vs\<^esup> * 2) # bs) p"
         using H(2) nn2 by (simp add: mult_minus2_right)
@@ -3731,7 +3641,7 @@
         by (simp_all add: polyneg_norm nn)
       have nn': "\<lparr>(C (-2, 1) *\<^sub>p c*\<^sub>p d)\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0" "\<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0" "\<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0"
         using H(3)
-        by (auto simp add: msubst2_def lt[OF stupid(1)]
+        by (auto simp: msubst2_def lt[OF stupid(1)]
             lt[OF stupid(2)] zero_less_mult_iff mult_less_0_iff)
       from msubst2[OF lp nn nn'(1), of x bs ] H(3) nn'
       have "\<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0 \<and> \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0 \<and>
@@ -3862,7 +3772,7 @@
     proof
       assume H: ?lhs
       then have z: "\<lparr>C (-2, 1) *\<^sub>p b *\<^sub>p d\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0" "\<lparr>C (-2, 1) *\<^sub>p d *\<^sub>p b\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0"
-        by (auto simp add: msubst2_def lt[OF stupid(3)] lt[OF stupid(1)]
+        by (auto simp: msubst2_def lt[OF stupid(3)] lt[OF stupid(1)]
             mult_less_0_iff zero_less_mult_iff)
       from msubst2[OF lq norm2(1) z(1), of x bs] msubst2[OF lq norm2(2) z(2), of x bs] H
       show ?rhs
@@ -3870,7 +3780,7 @@
     next
       assume H: ?rhs
       then have z: "\<lparr>C (-2, 1) *\<^sub>p b *\<^sub>p d\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0" "\<lparr>C (-2, 1) *\<^sub>p d *\<^sub>p b\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0"
-        by (auto simp add: msubst2_def lt[OF stupid(4)] lt[OF stupid(2)]
+        by (auto simp: msubst2_def lt[OF stupid(4)] lt[OF stupid(2)]
             mult_less_0_iff zero_less_mult_iff)
       from msubst2[OF lq norm2(1) z(1), of x bs] msubst2[OF lq norm2(2) z(2), of x bs] H
       show ?lhs
@@ -3898,13 +3808,16 @@
   also have "\<dots> \<longleftrightarrow> ?I ?R"
     by (simp add: list_disj_def evaldjf_ex split_def)
   also have "\<dots> \<longleftrightarrow> ?rhs"
-    unfolding ferrack2_def
-    apply (cases "?mp = T")
-     apply (simp add: list_disj_def)
-    apply (cases "?pp = T")
-     apply (simp add: list_disj_def)
-    apply (simp_all add: Let_def decr0[OF nb])
-    done
+  proof (cases "?mp = T \<or> ?pp = T")
+    case True
+    then show ?thesis 
+      unfolding ferrack2_def
+      by (force simp add: ferrack2_def list_disj_def)
+  next
+    case False
+    then show ?thesis 
+      by (simp add: ferrack2_def Let_def decr0[OF nb])
+  qed
   finally show ?thesis using decr0_qf[OF nb]
     by (simp add: ferrack2_def Let_def)
 qed
@@ -3915,7 +3828,7 @@
   have this: "\<forall>bs p. qfree p \<longrightarrow> qfree (ferrack2 p) \<and> Ifm vs bs (ferrack2 p) = Ifm vs bs (E p)"
     by blast
   from qelim[OF this, of "prep p" bs] show ?thesis
-    unfolding frpar2_def by (auto simp add: prep)
+    unfolding frpar2_def by (auto simp: prep)
 qed
 
 oracle frpar_oracle =
@@ -4092,57 +4005,9 @@
 \<close> "parametric QE for linear Arithmetic over fields, Version 2"
 
 lemma "\<exists>(x::'a::linordered_field). y \<noteq> -1 \<longrightarrow> (y + 1) * x < 0"
-  apply (frpar type: 'a pars: y)
-  apply (simp add: field_simps)
-  apply (rule spec[where x=y])
-  apply (frpar type: 'a pars: "z::'a")
-  apply simp
-  done
+  by (metis mult.commute neg_less_0_iff_less nonzero_divide_eq_eq sum_eq zero_less_two)
 
 lemma "\<exists>(x::'a::linordered_field). y \<noteq> -1 \<longrightarrow> (y + 1)*x < 0"
-  apply (frpar2 type: 'a pars: y)
-  apply (simp add: field_simps)
-  apply (rule spec[where x=y])
-  apply (frpar2 type: 'a pars: "z::'a")
-  apply simp
-  done
-
-text \<open>Collins/Jones Problem\<close>
-(*
-lemma "\<exists>(r::'a::{linordered_field, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0"
-proof -
-  have "(\<exists>(r::'a::{linordered_field, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0) \<longleftrightarrow> (\<exists>(r::'a::{linordered_field, number_ring}). 0 < r \<and> r < 1 \<and> 0 < 2 *(a^2 + b^2) - (3*(a^2 + b^2)) * r + (2*a)*r \<and> 2*(a^2 + b^2) - (3*(a^2 + b^2) - 4*a + 1)*r - 2*a < 0)" (is "?lhs \<longleftrightarrow> ?rhs")
-by (simp add: field_simps)
-have "?rhs"
-
-  apply (frpar type: "'a::{linordered_field, number_ring}" pars: "a::'a::{linordered_field, number_ring}" "b::'a::{linordered_field, number_ring}")
-  apply (simp add: field_simps)
-oops
-*)
-(*
-lemma "ALL (x::'a::{linordered_field, number_ring}) y. (1 - t)*x \<le> (1+t)*y \<and> (1 - t)*y \<le> (1+t)*x --> 0 \<le> y"
-apply (frpar type: "'a::{linordered_field, number_ring}" pars: "t::'a::{linordered_field, number_ring}")
-oops
-*)
-
-text \<open>Collins/Jones Problem\<close>
-
-(*
-lemma "\<exists>(r::'a::{linordered_field, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0"
-proof -
-  have "(\<exists>(r::'a::{linordered_field, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0) \<longleftrightarrow> (\<exists>(r::'a::{linordered_field, number_ring}). 0 < r \<and> r < 1 \<and> 0 < 2 *(a^2 + b^2) - (3*(a^2 + b^2)) * r + (2*a)*r \<and> 2*(a^2 + b^2) - (3*(a^2 + b^2) - 4*a + 1)*r - 2*a < 0)" (is "?lhs \<longleftrightarrow> ?rhs")
-by (simp add: field_simps)
-have "?rhs"
-  apply (frpar2 type: "'a::{linordered_field, number_ring}" pars: "a::'a::{linordered_field, number_ring}" "b::'a::{linordered_field, number_ring}")
-  apply simp
-oops
-*)
-
-(*
-lemma "ALL (x::'a::{linordered_field, number_ring}) y. (1 - t)*x \<le> (1+t)*y \<and> (1 - t)*y \<le> (1+t)*x --> 0 \<le> y"
-apply (frpar2 type: "'a::{linordered_field, number_ring}" pars: "t::'a::{linordered_field, number_ring}")
-apply (simp add: field_simps linorder_neq_iff[symmetric])
-apply ferrack
-oops
-*)
+  by (metis mult.right_neutral mult_minus1_right neg_0_le_iff_le nle_le not_less sum_eq)
+
 end
diff -r 83fa23ca40e5 -r c06c95576ea9 src/HOL/Decision_Procs/Polynomial_List.thy
--- a/src/HOL/Decision_Procs/Polynomial_List.thy	Fri Apr 12 09:58:53 2024 +0100
+++ b/src/HOL/Decision_Procs/Polynomial_List.thy	Fri Apr 12 22:19:20 2024 +0100
@@ -5,7 +5,8 @@
 section \<open>Univariate Polynomials as lists\<close>
 
 theory Polynomial_List
-imports Complex_Main
+  imports Complex_Main 
+
 begin
 
 text \<open>Application of polynomial as a function.\<close>
@@ -264,13 +265,9 @@
       by blast
     have "r = 0"
       using p0 by (simp only: Cons qr poly_mult poly_add) simp
-    with Cons qr show ?thesis
-      apply -
-      apply (rule exI[where x = q])
-      apply auto
-      apply (cases q)
-      apply auto
-      done
+    with Cons qr have "p = [- a, 1] *** q"
+      by (simp add: local.padd_commut)
+    then show ?thesis ..
   qed
   ultimately show ?thesis using Cons by blast
 qed
@@ -344,11 +341,8 @@
       by blast
     from y have "y = a \<or> poly q y = 0"
       by (simp only: q poly_mult_eq_zero_disj poly_add) (simp add: algebra_simps)
-    with i[of y] y(1) y(2) show ?thesis
-      apply auto
-      apply (erule_tac x = "m" in allE)
-      apply auto
-      done
+    with i[of y] y show ?thesis
+      using le_Suc_eq by auto
   qed
   then show ?case by blast
 qed
@@ -360,12 +354,7 @@
 
 lemma (in idom) poly_roots_finite_lemma1:
   "poly p x \<noteq> poly [] x \<Longrightarrow> \<exists>N i. \<forall>x. poly p x = 0 \<longrightarrow> (\<exists>n::nat. n < N \<and> x = i n)"
-  apply (drule poly_roots_index_length)
-  apply safe
-  apply (rule_tac x = "Suc (length p)" in exI)
-  apply (rule_tac x = i in exI)
-  apply (simp add: less_Suc_eq_le)
-  done
+  by (metis le_imp_less_Suc poly_roots_index_length)
 
 lemma (in idom) idom_finite_lemma:
   assumes "\<forall>x. P x \<longrightarrow> (\<exists>n. n < length j \<and> x = j!n)"
@@ -379,15 +368,8 @@
 
 lemma (in idom) poly_roots_finite_lemma2:
   "poly p x \<noteq> poly [] x \<Longrightarrow> \<exists>i. \<forall>x. poly p x = 0 \<longrightarrow> x \<in> set i"
-  apply (drule poly_roots_index_length)
-  apply safe
-  apply (rule_tac x = "map (\<lambda>n. i n) [0 ..< Suc (length p)]" in exI)
-  apply (auto simp add: image_iff)
-  apply (erule_tac x="x" in allE)
-  apply clarsimp
-  apply (case_tac "n = length p")
-  apply (auto simp add: order_le_less)
-  done
+  using poly_roots_index_length atMost_iff atMost_upto imageI set_map
+  by metis
 
 lemma (in ring_char_0) UNIV_ring_char_0_infinte: "\<not> finite (UNIV :: 'a set)"
 proof
@@ -408,21 +390,12 @@
   (is "?lhs \<longleftrightarrow> ?rhs")
 proof
   show ?rhs if ?lhs
-    using that
-    apply -
-    apply (erule contrapos_np)
-    apply (rule ext)
-    apply (rule ccontr)
-    apply (clarify dest!: poly_roots_finite_lemma2)
-    using finite_subset
   proof -
-    fix x i
-    assume F: "\<not> finite {x. poly p x = 0}"
-      and P: "\<forall>x. poly p x = 0 \<longrightarrow> x \<in> set i"
-    from P have "{x. poly p x = 0} \<subseteq> set i"
-      by auto
-    with finite_subset F show False
-      by auto
+    have False if  F: "\<not> finite {x. poly p x = 0}"
+      and P: "\<forall>x. poly p x = 0 \<longrightarrow> x \<in> set i" for  i
+      by (smt (verit, del_insts) in_set_conv_nth local.idom_finite_lemma that)
+    with that show ?thesis
+      using local.poly_roots_finite_lemma2 by blast
   qed
   show ?lhs if ?rhs
     using UNIV_ring_char_0_infinte that by auto
@@ -473,18 +446,15 @@
 qed
 
 lemma (in idom) poly_exp_eq_zero[simp]: "poly (p %^ n) = poly [] \<longleftrightarrow> poly p = poly [] \<and> n \<noteq> 0"
-  apply (simp only: fun_eq_iff add: HOL.all_simps [symmetric])
-  apply (rule arg_cong [where f = All])
-  apply (rule ext)
-  apply (induct n)
-  apply (auto simp add: poly_exp poly_mult)
-  done
+  by (simp add: local.poly_exp fun_eq_iff)
 
 lemma (in comm_ring_1) poly_prime_eq_zero[simp]: "poly [a, 1] \<noteq> poly []"
-  apply (simp add: fun_eq_iff)
-  apply (rule_tac x = "minus one a" in exI)
-  apply (simp add: add.commute [of a])
-  done
+proof -
+  have "\<exists>x. a + x \<noteq> 0"
+    by (metis add_cancel_left_right zero_neq_one)
+  then show ?thesis
+    by (simp add: fun_eq_iff)
+qed
 
 lemma (in idom) poly_exp_prime_eq_zero: "poly ([a, 1] %^ n) \<noteq> poly []"
   by auto
@@ -492,26 +462,18 @@
 
 text \<open>A more constructive notion of polynomials being trivial.\<close>
 
-lemma (in idom_char_0) poly_zero_lemma': "poly (h # t) = poly [] \<Longrightarrow> h = 0 \<and> poly t = poly []"
-  apply (simp add: fun_eq_iff)
-  apply (case_tac "h = zero")
-  apply (drule_tac [2] x = zero in spec)
-  apply auto
-  apply (cases "poly t = poly []")
-  apply simp
+lemma (in idom_char_0) poly_zero_lemma': 
+  assumes "poly (h # t) = poly []" shows "h = 0 \<and> poly t = poly []"
 proof -
-  fix x
-  assume H: "\<forall>x. x = 0 \<or> poly t x = 0"
-  assume pnz: "poly t \<noteq> poly []"
-  let ?S = "{x. poly t x = 0}"
-  from H have "\<forall>x. x \<noteq> 0 \<longrightarrow> poly t x = 0"
-    by blast
-  then have th: "?S \<supseteq> UNIV - {0}"
-    by auto
-  from poly_roots_finite pnz have th': "finite ?S"
-    by blast
-  from finite_subset[OF th th'] UNIV_ring_char_0_infinte show "poly t x = 0"
-    by simp
+  have "poly t x = 0" if H: "\<forall>x. x = 0 \<or> poly t x = 0" and pnz: "poly t \<noteq> poly []" for x
+  proof -
+    from H have "{x. poly t x = 0} \<supseteq> UNIV - {0}"
+      by auto
+    then show ?thesis
+      using finite_subset local.poly_roots_finite pnz by fastforce
+  qed
+  with assms show ?thesis
+    by (simp add: fun_eq_iff) (metis add_cancel_right_left mult_eq_0_iff)
 qed
 
 lemma (in idom_char_0) poly_zero: "poly p = poly [] \<longleftrightarrow> (\<forall>c \<in> set p. c = 0)"
@@ -520,12 +482,8 @@
   then show ?case by simp
 next
   case Cons
-  show ?case
-    apply (rule iffI)
-    apply (drule poly_zero_lemma')
-    using Cons
-    apply auto
-    done
+  then show ?case
+    by (smt (verit) list.set_intros pmult_by_x poly_entire poly_zero_lemma' set_ConsD)
 qed
 
 lemma (in idom_char_0) poly_0: "\<forall>c \<in> set p. c = 0 \<Longrightarrow> poly p x = 0"
@@ -535,41 +493,33 @@
 text \<open>Basics of divisibility.\<close>
 
 lemma (in idom) poly_primes: "[a, 1] divides (p *** q) \<longleftrightarrow> [a, 1] divides p \<or> [a, 1] divides q"
-  apply (auto simp add: divides_def fun_eq_iff poly_mult poly_add poly_cmult distrib_right [symmetric])
-  apply (drule_tac x = "uminus a" in spec)
-  apply (simp add: poly_linear_divides poly_add poly_cmult distrib_right [symmetric])
-  apply (cases "p = []")
-  apply (rule exI[where x="[]"])
-  apply simp
-  apply (cases "q = []")
-  apply (erule allE[where x="[]"])
-  apply simp
-
-  apply clarsimp
-  apply (cases "\<exists>q. p = a %* q +++ (0 # q)")
-  apply (clarsimp simp add: poly_add poly_cmult)
-  apply (rule_tac x = qa in exI)
-  apply (simp add: distrib_right [symmetric])
-  apply clarsimp
-
-  apply (auto simp add: poly_linear_divides poly_add poly_cmult distrib_right [symmetric])
-  apply (rule_tac x = "pmult qa q" in exI)
-  apply (rule_tac [2] x = "pmult p qa" in exI)
-  apply (auto simp add: poly_add poly_mult poly_cmult ac_simps)
-  done
+proof -
+  have "\<exists>q. \<forall>x. poly p x = (a + x) * poly q x"
+    if "poly p (uminus a) * poly q (uminus a) = (a + (uminus a)) * poly qa (uminus a)"
+      and "\<forall>qa. \<exists>x. poly q x \<noteq> (a + x) * poly qa x"
+    for qa 
+    using that   
+    apply (simp add: poly_linear_divides poly_add)
+    by (metis add_cancel_left_right combine_common_factor mult_eq_0_iff poly.poly_Cons poly.poly_Nil poly_add poly_cmult)
+  moreover have "\<exists>qb. \<forall>x. (a + x) * poly qa x * poly q x = (a + x) * poly qb x" for qa
+    by (metis local.poly_mult mult_assoc)
+  moreover have "\<exists>q. \<forall>x. poly p x * ((a + x) * poly qa x) = (a + x) * poly q x" for qa 
+    by (metis mult.left_commute local.poly_mult)
+  ultimately show ?thesis
+    by (auto simp: divides_def divisors_zero fun_eq_iff poly_mult poly_add poly_cmult simp flip: distrib_right)
+qed
 
 lemma (in comm_semiring_1) poly_divides_refl[simp]: "p divides p"
-  apply (simp add: divides_def)
-  apply (rule_tac x = "[one]" in exI)
-  apply (auto simp add: poly_mult fun_eq_iff)
-  done
+proof -
+  have "poly p = poly (p *** [1])"
+    by (auto simp add: poly_mult fun_eq_iff)
+  then show ?thesis
+    using local.dividesI by blast
+qed
 
 lemma (in comm_semiring_1) poly_divides_trans: "p divides q \<Longrightarrow> q divides r \<Longrightarrow> p divides r"
-  apply (simp add: divides_def)
-  apply safe
-  apply (rule_tac x = "pmult qa qaa" in exI)
-  apply (auto simp add: poly_mult fun_eq_iff mult.assoc)
-  done
+  unfolding divides_def
+  by (metis ext local.poly_mult local.poly_mult_assoc)
 
 lemma (in comm_semiring_1) poly_divides_exp: "m \<le> n \<Longrightarrow> (p %^ m) divides (p %^ n)"
   by (auto simp: le_iff_add divides_def poly_exp_add fun_eq_iff)
@@ -577,34 +527,35 @@
 lemma (in comm_semiring_1) poly_exp_divides: "(p %^ n) divides q \<Longrightarrow> m \<le> n \<Longrightarrow> (p %^ m) divides q"
   by (blast intro: poly_divides_exp poly_divides_trans)
 
-lemma (in comm_semiring_0) poly_divides_add: "p divides q \<Longrightarrow> p divides r \<Longrightarrow> p divides (q +++ r)"
-  apply (auto simp add: divides_def)
-  apply (rule_tac x = "padd qa qaa" in exI)
-  apply (auto simp add: poly_add fun_eq_iff poly_mult distrib_left)
-  done
+lemma (in comm_semiring_0) poly_divides_add:
+  assumes "p divides q" and "p divides r" shows "p divides (q +++ r)"
+proof -
+  have "\<And>qa qb. \<lbrakk>poly q = poly (p *** qa); poly r = poly (p *** qb)\<rbrakk>
+       \<Longrightarrow> poly (q +++ r) = poly (p *** (qa +++ qb))"
+    by (auto simp add: poly_add fun_eq_iff poly_mult distrib_left)
+  with assms show ?thesis
+    by (auto simp add: divides_def)
+qed
 
-lemma (in comm_ring_1) poly_divides_diff: "p divides q \<Longrightarrow> p divides (q +++ r) \<Longrightarrow> p divides r"
-  apply (auto simp add: divides_def)
-  apply (rule_tac x = "padd qaa (poly_minus qa)" in exI)
-  apply (auto simp add: poly_add fun_eq_iff poly_mult poly_minus algebra_simps)
-  done
+lemma (in comm_ring_1) poly_divides_diff:
+  assumes "p divides q" and "p divides (q +++ r)"
+  shows "p divides r"
+proof -
+  have "\<And>qa qb. \<lbrakk>poly q = poly (p *** qa); poly (q +++ r) = poly (p *** qb)\<rbrakk>
+         \<Longrightarrow> poly r = poly (p *** (qb +++ -- qa))"
+  by (auto simp add: poly_add fun_eq_iff poly_mult poly_minus algebra_simps)
+  with assms show ?thesis
+    by (auto simp add: divides_def)
+qed
 
 lemma (in comm_ring_1) poly_divides_diff2: "p divides r \<Longrightarrow> p divides (q +++ r) \<Longrightarrow> p divides q"
-  apply (erule poly_divides_diff)
-  apply (auto simp add: poly_add fun_eq_iff poly_mult divides_def ac_simps)
-  done
+  by (metis local.padd_commut local.poly_divides_diff)
 
 lemma (in semiring_0) poly_divides_zero: "poly p = poly [] \<Longrightarrow> q divides p"
-  apply (simp add: divides_def)
-  apply (rule exI[where x = "[]"])
-  apply (auto simp add: fun_eq_iff poly_mult)
-  done
+  by (metis ext dividesI poly.poly_Nil poly_mult_Nil2)
 
 lemma (in semiring_0) poly_divides_zero2 [simp]: "q divides []"
-  apply (simp add: divides_def)
-  apply (rule_tac x = "[]" in exI)
-  apply (auto simp add: fun_eq_iff)
-  done
+  using local.poly_divides_zero by force
 
 
 text \<open>At last, we can consider the order of a root.\<close>
@@ -629,11 +580,7 @@
     from True[unfolded poly_linear_divides] pN obtain q where q: "p = [-a, 1] *** q"
       by blast
     from q h True have qh: "length q = n" "poly q \<noteq> poly []"
-      apply simp_all
-      apply (simp only: fun_eq_iff)
-      apply (rule ccontr)
-      apply (simp add: fun_eq_iff poly_add poly_cmult)
-      done
+      using h(2) local.poly_entire q by fastforce+
     from Suc.hyps[OF qh] obtain m r where mr: "q = mulexp m [-a,1] r" "poly r a \<noteq> 0"
       by blast
     from mr q have "p = mulexp (Suc m) [-a,1] r \<and> poly r a \<noteq> 0"
@@ -641,12 +588,8 @@
     then show ?thesis by blast
   next
     case False
-    then show ?thesis
-      using Suc.prems
-      apply simp
-      apply (rule exI[where x="0::nat"])
-      apply simp
-      done
+    with Suc.prems show ?thesis
+      by (smt (verit, best) local.mulexp.mulexp_zero)
   qed
 qed
 
@@ -719,12 +662,7 @@
 
 lemma (in idom_char_0) poly_order:
   "poly p \<noteq> poly [] \<Longrightarrow> \<exists>!n. ([-a, 1] %^ n) divides p \<and> \<not> (([-a, 1] %^ Suc n) divides p)"
-  apply (auto intro: poly_order_exists simp add: less_linear simp del: pmult_Cons pexp_Suc)
-  apply (cut_tac x = y and y = n in less_linear)
-  apply (drule_tac m = n in poly_exp_divides)
-  apply (auto dest: Suc_le_eq [THEN iffD2, THEN [2] poly_exp_divides]
-    simp del: pmult_Cons pexp_Suc)
-  done
+  by (meson Suc_le_eq linorder_neqE_nat local.poly_exp_divides poly_order_exists)
 
 
 text \<open>Order\<close>
@@ -736,10 +674,7 @@
   "([-a, 1] %^ n) divides p \<and> \<not> (([-a, 1] %^ Suc n) divides p) \<longleftrightarrow>
     n = order a p \<and> poly p \<noteq> poly []"
   unfolding order_def
-  apply (rule iffI)
-  apply (blast dest: poly_divides_zero intro!: some1_equality [symmetric] poly_order)
-  apply (blast intro!: poly_order [THEN [2] some1_equalityD])
-  done
+  by (metis (no_types, lifting) local.poly_divides_zero local.poly_order someI)
 
 lemma (in idom_char_0) order2:
   "poly p \<noteq> poly [] \<Longrightarrow>
@@ -767,97 +702,89 @@
   by (induct n arbitrary: a p) (auto simp add: divides_def poly_mult simp del: pmult_Cons)
 
 lemma (in idom_char_0) order_root: "poly p a = 0 \<longleftrightarrow> poly p = poly [] \<or> order a p \<noteq> 0"
-  apply (cases "poly p = poly []")
-  apply auto
-  apply (simp add: poly_linear_divides del: pmult_Cons)
-  apply safe
-  apply (drule_tac [!] a = a in order2)
-  apply (rule ccontr)
-  apply (simp add: divides_def poly_mult fun_eq_iff del: pmult_Cons)
-  apply blast
-  using neq0_conv apply (blast intro: lemma_order_root)
-  done
+proof (cases "poly p = poly []")
+  case False
+  then show ?thesis 
+    by (metis (mono_tags, lifting) dividesI lemma_order_root order2 pexp_one poly_linear_divides neq0_conv)
+qed auto
 
 lemma (in idom_char_0) order_divides:
   "([-a, 1] %^ n) divides p \<longleftrightarrow> poly p = poly [] \<or> n \<le> order a p"
-  apply (cases "poly p = poly []")
-  apply auto
-  apply (simp add: divides_def fun_eq_iff poly_mult)
-  apply (rule_tac x = "[]" in exI)
-  apply (auto dest!: order2 [where a=a] intro: poly_exp_divides simp del: pexp_Suc)
-  done
+proof (cases "poly p = poly []")
+  case True
+  then show ?thesis 
+    using local.poly_divides_zero by force
+next
+  case False
+  then show ?thesis 
+    by (meson local.order2 local.poly_exp_divides not_less_eq_eq)
+qed
 
 lemma (in idom_char_0) order_decomp:
-  "poly p \<noteq> poly [] \<Longrightarrow> \<exists>q. poly p = poly (([-a, 1] %^ order a p) *** q) \<and> \<not> [-a, 1] divides q"
-  unfolding divides_def
-  apply (drule order2 [where a = a])
-  apply (simp add: divides_def del: pexp_Suc pmult_Cons)
-  apply safe
-  apply (rule_tac x = q in exI)
-  apply safe
-  apply (drule_tac x = qa in spec)
-  apply (auto simp add: poly_mult fun_eq_iff poly_exp ac_simps simp del: pmult_Cons)
-  done
+  assumes "poly p \<noteq> poly []"
+  shows "\<exists>q. poly p = poly (([-a, 1] %^ order a p) *** q) \<and> \<not> [-a, 1] divides q"
+proof -
+  obtain q where q: "poly p = poly ([- a, 1] %^ order a p *** q)"
+    using assms local.order2 divides_def by blast
+  have False if "poly q = poly ([- a, 1] *** qa)" for qa
+  proof -
+    have "poly p \<noteq> poly ([- a, 1] %^ Suc (order a p) *** qa)"
+      using assms local.divides_def local.order2 by blast
+    with q that show False
+      by (auto simp add: poly_mult ac_simps simp del: pmult_Cons)
+  qed 
+  with q show ?thesis
+    unfolding divides_def by blast
+qed
 
 text \<open>Important composition properties of orders.\<close>
 lemma order_mult:
   fixes a :: "'a::idom_char_0"
-  shows "poly (p *** q) \<noteq> poly [] \<Longrightarrow> order a (p *** q) = order a p + order a q"
-  apply (cut_tac a = a and p = "p *** q" and n = "order a p + order a q" in order)
-  apply (auto simp add: poly_entire simp del: pmult_Cons)
-  apply (drule_tac a = a in order2)+
-  apply safe
-  apply (simp add: divides_def fun_eq_iff poly_exp_add poly_mult del: pmult_Cons, safe)
-  apply (rule_tac x = "qa *** qaa" in exI)
-  apply (simp add: poly_mult ac_simps del: pmult_Cons)
-  apply (drule_tac a = a in order_decomp)+
-  apply safe
-  apply (subgoal_tac "[-a, 1] divides (qa *** qaa) ")
-  apply (simp add: poly_primes del: pmult_Cons)
-  apply (auto simp add: divides_def simp del: pmult_Cons)
-  apply (rule_tac x = qb in exI)
-  apply (subgoal_tac "poly ([-a, 1] %^ (order a p) *** (qa *** qaa)) =
-    poly ([-a, 1] %^ (order a p) *** ([-a, 1] *** qb))")
-  apply (drule poly_mult_left_cancel [THEN iffD1])
-  apply force
-  apply (subgoal_tac "poly ([-a, 1] %^ (order a q) *** ([-a, 1] %^ (order a p) *** (qa *** qaa))) =
-    poly ([-a, 1] %^ (order a q) *** ([-a, 1] %^ (order a p) *** ([-a, 1] *** qb))) ")
-  apply (drule poly_mult_left_cancel [THEN iffD1])
-  apply force
-  apply (simp add: fun_eq_iff poly_exp_add poly_mult ac_simps del: pmult_Cons)
-  done
-
-lemma (in idom_char_0) order_mult:
   assumes "poly (p *** q) \<noteq> poly []"
   shows "order a (p *** q) = order a p + order a q"
-  using assms
-  apply (cut_tac a = a and p = "pmult p q" and n = "order a p + order a q" in order)
-  apply (auto simp add: poly_entire simp del: pmult_Cons)
-  apply (drule_tac a = a in order2)+
-  apply safe
-  apply (simp add: divides_def fun_eq_iff poly_exp_add poly_mult del: pmult_Cons)
-  apply safe
-  apply (rule_tac x = "pmult qa qaa" in exI)
-  apply (simp add: poly_mult ac_simps del: pmult_Cons)
-  apply (drule_tac a = a in order_decomp)+
-  apply safe
-  apply (subgoal_tac "[uminus a, one] divides pmult qa qaa")
-  apply (simp add: poly_primes del: pmult_Cons)
-  apply (auto simp add: divides_def simp del: pmult_Cons)
-  apply (rule_tac x = qb in exI)
-  apply (subgoal_tac "poly (pmult (pexp [uminus a, one] (order a p)) (pmult qa qaa)) =
-    poly (pmult (pexp [uminus a, one] (order a p)) (pmult [uminus a, one] qb))")
-  apply (drule poly_mult_left_cancel [THEN iffD1], force)
-  apply (subgoal_tac "poly (pmult (pexp [uminus a, one] (order a q))
-      (pmult (pexp [uminus a, one] (order a p)) (pmult qa qaa))) =
-    poly (pmult (pexp [uminus a, one] (order a q))
-      (pmult (pexp [uminus a, one] (order a p)) (pmult [uminus a, one] qb)))")
-  apply (drule poly_mult_left_cancel [THEN iffD1], force)
-  apply (simp add: fun_eq_iff poly_exp_add poly_mult ac_simps del: pmult_Cons)
-  done
+proof -
+  have p: "poly p \<noteq> poly []" and q: "poly q \<noteq> poly []"
+    using assms poly_entire by auto
+  obtain p' where p': 
+          "\<And>x. poly p x = poly ([- a, 1] %^ order a p) x * poly p' x"
+          "\<not> [- a, 1] divides p'"
+    by (metis order_decomp p poly_mult)
+  obtain q' where q': 
+          "\<And>x. poly q x = poly ([- a, 1] %^ order a q) x * poly q' x"
+          "\<not> [- a, 1] divides q'"
+    by (metis order_decomp q poly_mult)
+  have "[- a, 1] %^ (order a p + order a q) divides (p *** q)"
+  proof -
+    have *: "poly p x * poly q x =
+          poly ([- a, 1] %^ order a p) x * poly ([- a, 1] %^ order a q) x * poly (p' *** q') x" for x
+      using p' q' by (simp add: poly_mult)
+    then show ?thesis
+      unfolding divides_def  poly_exp_add poly_mult using * by blast
+  qed
+  moreover have False
+    if pq: "order a (p *** q) \<noteq> order a p + order a q"
+      and dv: "[- a, 1] *** [- a, 1] %^ (order a p + order a q) divides (p *** q)"
+  proof -
+    obtain pq' :: "'a list"
+      where pq': "poly (p *** q) = poly ([- a, 1] *** [- a, 1] %^ (order a p + order a q) *** pq')"
+      using dv unfolding divides_def by auto
+    have "poly ([-a, 1] %^ (order a q) *** ([-a, 1] %^ (order a p) *** (p' *** q'))) =
+          poly ([-a, 1] %^ (order a q) *** ([-a, 1] %^ (order a p) *** ([-a, 1] *** pq')))"
+      using p' q' pq pq'
+      by (simp add: fun_eq_iff poly_exp_add poly_mult ac_simps del: pmult_Cons)
+    then have "poly ([-a, 1] %^ (order a p) *** (p' *** q')) = poly ([-a, 1] %^ (order a p) *** ([-a, 1] *** pq'))"
+      by (simp add: poly_mult_left_cancel)
+    then have "[-a, 1] divides (p' *** q')"
+      unfolding divides_def by (meson poly_exp_prime_eq_zero poly_mult_left_cancel)
+    with p' q' show ?thesis
+      by (simp add: poly_primes)
+  qed
+  ultimately show ?thesis
+    by (metis order pexp_Suc)
+qed
 
 lemma (in idom_char_0) order_root2: "poly p \<noteq> poly [] \<Longrightarrow> poly p a = 0 \<longleftrightarrow> order a p \<noteq> 0"
-  by (rule order_root [THEN ssubst]) auto
+  using order_root by presburger
 
 lemma (in semiring_1) pmult_one[simp]: "[1] *** p = p"
   by auto
@@ -866,21 +793,18 @@
   by (simp add: fun_eq_iff)
 
 lemma (in idom_char_0) rsquarefree_decomp:
-  "rsquarefree p \<Longrightarrow> poly p a = 0 \<Longrightarrow> \<exists>q. poly p = poly ([-a, 1] *** q) \<and> poly q a \<noteq> 0"
-  apply (simp add: rsquarefree_def)
-  apply safe
-  apply (frule_tac a = a in order_decomp)
-  apply (drule_tac x = a in spec)
-  apply (drule_tac a = a in order_root2 [symmetric])
-  apply (auto simp del: pmult_Cons)
-  apply (rule_tac x = q in exI, safe)
-  apply (simp add: poly_mult fun_eq_iff)
-  apply (drule_tac p1 = q in poly_linear_divides [THEN iffD1])
-  apply (simp add: divides_def del: pmult_Cons, safe)
-  apply (drule_tac x = "[]" in spec)
-  apply (auto simp add: fun_eq_iff)
-  done
-
+  assumes "rsquarefree p" and "poly p a = 0"
+  shows "\<exists>q. poly p = poly ([-a, 1] *** q) \<and> poly q a \<noteq> 0"
+proof -
+  have "order a p = Suc 0"
+    using assms local.order_root2 rsquarefree_def by force
+  moreover
+  obtain q where "poly p = poly ([- a, 1] %^ order a p *** q)" 
+                 "\<not> [- a, 1] divides q"
+    using assms(1) order_decomp rsquarefree_def by blast
+  ultimately show ?thesis
+    using dividesI poly_linear_divides by auto
+qed
 
 text \<open>Normalization of a polynomial.\<close>
 
@@ -952,28 +876,12 @@
   then show ?case
   proof (induct p)
     case Nil
-    then have "poly [] = poly (c # cs)"
-      by blast
-    then have "poly (c#cs) = poly []"
-      by simp
     then show ?case
-      by (simp only: poly_zero lemma_degree_zero) simp
+      by (metis local.poly_zero_lemma')
   next
     case (Cons d ds)
-    then have eq: "poly (d # ds) = poly (c # cs)"
-      by blast
-    then have eq': "\<And>x. poly (d # ds) x = poly (c # cs) x"
-      by simp
-    then have "poly (d # ds) 0 = poly (c # cs) 0"
-      by blast
-    then have dc: "d = c"
-      by auto
-    with eq have "poly ds = poly cs"
-      unfolding  poly_Cons_eq by simp
-    with Cons.prems have "pnormalize ds = pnormalize cs"
-      by blast
-    with dc show ?case
-      by simp
+    then show ?case
+      by (metis pnormalize.pnormalize_Cons local.poly_Cons_eq)
   qed
 qed
 
@@ -987,15 +895,16 @@
 
 lemma (in semiring_0) last_linear_mul_lemma:
   "last ((a %* p) +++ (x # (b %* p))) = (if p = [] then x else b * last p)"
-  apply (induct p arbitrary: a x b)
-  apply auto
-  subgoal for a p c x b
-    apply (subgoal_tac "padd (cmult c p) (times b a # cmult b p) \<noteq> []")
-    apply simp
-    apply (induct p)
-    apply auto
-    done
-  done
+proof (induct p arbitrary: a x b)
+  case Nil
+  then show ?case by auto
+next
+  case (Cons a p c x b)
+  then have "padd (cmult c p) (times b a # cmult b p) \<noteq> []"
+    by (metis local.padd.padd_Nil local.padd_Cons_Cons neq_Nil_conv)
+  then show ?case
+    by (simp add: local.Cons)
+qed
 
 lemma (in semiring_1) last_linear_mul:
   assumes p: "p \<noteq> []"
@@ -1051,18 +960,11 @@
     case True
     then show ?thesis
       using degree_unique[OF True] by (simp add: degree_def)
-  next
-    case False
-    then show ?thesis
-      by (auto simp add: poly_Nil_ext)
-  qed
+  qed (auto simp add: poly_Nil_ext)
 next
   case (Suc n a p)
   have eq: "poly ([a, 1] %^(Suc n) *** p) = poly ([a, 1] %^ n *** ([a, 1] *** p))"
-    apply (rule ext)
-    apply (simp add: poly_mult poly_add poly_cmult)
-    apply (simp add: ac_simps distrib_left)
-    done
+    by (force simp add: poly_mult poly_add poly_cmult ac_simps distrib_left)
   note deq = degree_unique[OF eq]
   show ?case
   proof (cases "poly p = poly []")
@@ -1080,9 +982,7 @@
     from ap have ap': "poly ([a, 1] *** p) = poly [] \<longleftrightarrow> False"
       by blast
     have th0: "degree ([a, 1]%^n *** ([a, 1] *** p)) = degree ([a, 1] *** p) + n"
-      apply (simp only: Suc.hyps[of a "pmult [a,one] p"] ap')
-      apply simp
-      done
+      unfolding Suc.hyps[of a "pmult [a,one] p"] ap' by simp
     from degree_unique[OF eq] ap False th0 linear_mul_degree[OF False, of a]
     show ?thesis
       by (auto simp del: poly.simps)
@@ -1118,12 +1018,12 @@
   then show ?case by simp
 next
   case (Cons a p)
-  then show ?case
-    apply auto
-    apply (rule_tac y = "\<bar>a\<bar> + \<bar>x * poly p x\<bar>" in order_trans)
-    apply (rule abs_triangle_ineq)
-    apply (auto intro!: mult_mono simp add: abs_mult)
-    done
+  have "\<bar>a + x * poly p x\<bar> \<le> \<bar>a\<bar> + \<bar>x * poly p x\<bar>"
+    using abs_triangle_ineq by blast
+  also have "\<dots> \<le> \<bar>a\<bar> + k * poly (map abs p) k"
+    by (simp add: Cons.hyps Cons.prems abs_mult mult_mono')
+  finally show ?case
+    using Cons by auto
 qed
 
 lemma (in semiring_0) poly_Sing: "poly [c] x = c"