diff --git a/src/HOL/Decision_Procs/Commutative_Ring.thy b/src/HOL/Decision_Procs/Commutative_Ring.thy
--- a/src/HOL/Decision_Procs/Commutative_Ring.thy
+++ b/src/HOL/Decision_Procs/Commutative_Ring.thy
@@ -1,962 +1,963 @@
 (*  Title:      HOL/Decision_Procs/Commutative_Ring.thy
     Author:     Bernhard Haeupler, Stefan Berghofer, and Amine Chaieb
 
 Proving equalities in commutative rings done "right" in Isabelle/HOL.
 *)
 
 section \<open>Proving equalities in commutative rings\<close>
 
 theory Commutative_Ring
   imports
     Conversions
     Algebra_Aux
     "HOL-Library.Code_Target_Numeral"
 begin
 
 text \<open>Syntax of multivariate polynomials (pol) and polynomial expressions.\<close>
 
 datatype pol =
     Pc int
   | Pinj nat pol
   | PX pol nat pol
 
 datatype polex =
     Var nat
   | Const int
   | Add polex polex
   | Sub polex polex
   | Mul polex polex
   | Pow polex nat
   | Neg polex
 
 text \<open>Interpretation functions for the shadow syntax.\<close>
 
 context cring
 begin
 
 definition in_carrier :: "'a list \<Rightarrow> bool"
   where "in_carrier xs \<longleftrightarrow> (\<forall>x\<in>set xs. x \<in> carrier R)"
 
 lemma in_carrier_Nil: "in_carrier []"
   by (simp add: in_carrier_def)
 
 lemma in_carrier_Cons: "x \<in> carrier R \<Longrightarrow> in_carrier xs \<Longrightarrow> in_carrier (x # xs)"
   by (simp add: in_carrier_def)
 
 lemma drop_in_carrier [simp]: "in_carrier xs \<Longrightarrow> in_carrier (drop n xs)"
   using set_drop_subset [of n xs] by (auto simp add: in_carrier_def)
 
 primrec head :: "'a list \<Rightarrow> 'a"
   where
     "head [] = \<zero>"
   | "head (x # xs) = x"
 
 lemma head_closed [simp]: "in_carrier xs \<Longrightarrow> head xs \<in> carrier R"
   by (cases xs) (simp_all add: in_carrier_def)
 
 primrec Ipol :: "'a list \<Rightarrow> pol \<Rightarrow> 'a"
   where
     "Ipol l (Pc c) = \<guillemotleft>c\<guillemotright>"
   | "Ipol l (Pinj i P) = Ipol (drop i l) P"
   | "Ipol l (PX P x Q) = Ipol l P \<otimes> head l [^] x \<oplus> Ipol (drop 1 l) Q"
 
 lemma Ipol_Pc:
   "Ipol l (Pc 0) = \<zero>"
   "Ipol l (Pc 1) = \<one>"
   "Ipol l (Pc (numeral n)) = \<guillemotleft>numeral n\<guillemotright>"
   "Ipol l (Pc (- numeral n)) = \<ominus> \<guillemotleft>numeral n\<guillemotright>"
   by simp_all
 
 lemma Ipol_closed [simp]: "in_carrier l \<Longrightarrow> Ipol l p \<in> carrier R"
   by (induct p arbitrary: l) simp_all
 
 primrec Ipolex :: "'a list \<Rightarrow> polex \<Rightarrow> 'a"
   where
     "Ipolex l (Var n) = head (drop n l)"
   | "Ipolex l (Const i) = \<guillemotleft>i\<guillemotright>"
   | "Ipolex l (Add P Q) = Ipolex l P \<oplus> Ipolex l Q"
   | "Ipolex l (Sub P Q) = Ipolex l P \<ominus> Ipolex l Q"
   | "Ipolex l (Mul P Q) = Ipolex l P \<otimes> Ipolex l Q"
   | "Ipolex l (Pow p n) = Ipolex l p [^] n"
   | "Ipolex l (Neg P) = \<ominus> Ipolex l P"
 
 lemma Ipolex_Const:
   "Ipolex l (Const 0) = \<zero>"
   "Ipolex l (Const 1) = \<one>"
   "Ipolex l (Const (numeral n)) = \<guillemotleft>numeral n\<guillemotright>"
   by simp_all
 
 end
 
 text \<open>Create polynomial normalized polynomials given normalized inputs.\<close>
 
 definition mkPinj :: "nat \<Rightarrow> pol \<Rightarrow> pol"
   where "mkPinj x P =
     (case P of
       Pc c \<Rightarrow> Pc c
     | Pinj y P \<Rightarrow> Pinj (x + y) P
     | PX p1 y p2 \<Rightarrow> Pinj x P)"
 
 definition mkPX :: "pol \<Rightarrow> nat \<Rightarrow> pol \<Rightarrow> pol"
   where "mkPX P i Q =
     (case P of
       Pc c \<Rightarrow> if c = 0 then mkPinj 1 Q else PX P i Q
     | Pinj j R \<Rightarrow> PX P i Q
     | PX P2 i2 Q2 \<Rightarrow> if Q2 = Pc 0 then PX P2 (i + i2) Q else PX P i Q)"
 
 text \<open>Defining the basic ring operations on normalized polynomials\<close>
 
 function add :: "pol \<Rightarrow> pol \<Rightarrow> pol"  (infixl "\<langle>+\<rangle>" 65)
   where
     "Pc a \<langle>+\<rangle> Pc b = Pc (a + b)"
   | "Pc c \<langle>+\<rangle> Pinj i P = Pinj i (P \<langle>+\<rangle> Pc c)"
   | "Pinj i P \<langle>+\<rangle> Pc c = Pinj i (P \<langle>+\<rangle> Pc c)"
   | "Pc c \<langle>+\<rangle> PX P i Q = PX P i (Q \<langle>+\<rangle> Pc c)"
   | "PX P i Q \<langle>+\<rangle> Pc c = PX P i (Q \<langle>+\<rangle> Pc c)"
   | "Pinj x P \<langle>+\<rangle> Pinj y Q =
       (if x = y then mkPinj x (P \<langle>+\<rangle> Q)
        else (if x > y then mkPinj y (Pinj (x - y) P \<langle>+\<rangle> Q)
          else mkPinj x (Pinj (y - x) Q \<langle>+\<rangle> P)))"
   | "Pinj x P \<langle>+\<rangle> PX Q y R =
       (if x = 0 then P \<langle>+\<rangle> PX Q y R
        else (if x = 1 then PX Q y (R \<langle>+\<rangle> P)
          else PX Q y (R \<langle>+\<rangle> Pinj (x - 1) P)))"
   | "PX P x R \<langle>+\<rangle> Pinj y Q =
       (if y = 0 then PX P x R \<langle>+\<rangle> Q
        else (if y = 1 then PX P x (R \<langle>+\<rangle> Q)
          else PX P x (R \<langle>+\<rangle> Pinj (y - 1) Q)))"
   | "PX P1 x P2 \<langle>+\<rangle> PX Q1 y Q2 =
       (if x = y then mkPX (P1 \<langle>+\<rangle> Q1) x (P2 \<langle>+\<rangle> Q2)
        else (if x > y then mkPX (PX P1 (x - y) (Pc 0) \<langle>+\<rangle> Q1) y (P2 \<langle>+\<rangle> Q2)
          else mkPX (PX Q1 (y - x) (Pc 0) \<langle>+\<rangle> P1) x (P2 \<langle>+\<rangle> Q2)))"
   by pat_completeness auto
 termination by (relation "measure (\<lambda>(x, y). size x + size y)") auto
 
 function mul :: "pol \<Rightarrow> pol \<Rightarrow> pol"  (infixl "\<langle>*\<rangle>" 70)
   where
     "Pc a \<langle>*\<rangle> Pc b = Pc (a * b)"
   | "Pc c \<langle>*\<rangle> Pinj i P =
       (if c = 0 then Pc 0 else mkPinj i (P \<langle>*\<rangle> Pc c))"
   | "Pinj i P \<langle>*\<rangle> Pc c =
       (if c = 0 then Pc 0 else mkPinj i (P \<langle>*\<rangle> Pc c))"
   | "Pc c \<langle>*\<rangle> PX P i Q =
       (if c = 0 then Pc 0 else mkPX (P \<langle>*\<rangle> Pc c) i (Q \<langle>*\<rangle> Pc c))"
   | "PX P i Q \<langle>*\<rangle> Pc c =
       (if c = 0 then Pc 0 else mkPX (P \<langle>*\<rangle> Pc c) i (Q \<langle>*\<rangle> Pc c))"
   | "Pinj x P \<langle>*\<rangle> Pinj y Q =
       (if x = y then mkPinj x (P \<langle>*\<rangle> Q)
        else
          (if x > y then mkPinj y (Pinj (x - y) P \<langle>*\<rangle> Q)
           else mkPinj x (Pinj (y - x) Q \<langle>*\<rangle> P)))"
   | "Pinj x P \<langle>*\<rangle> PX Q y R =
       (if x = 0 then P \<langle>*\<rangle> PX Q y R
        else
          (if x = 1 then mkPX (Pinj x P \<langle>*\<rangle> Q) y (R \<langle>*\<rangle> P)
           else mkPX (Pinj x P \<langle>*\<rangle> Q) y (R \<langle>*\<rangle> Pinj (x - 1) P)))"
   | "PX P x R \<langle>*\<rangle> Pinj y Q =
       (if y = 0 then PX P x R \<langle>*\<rangle> Q
        else
          (if y = 1 then mkPX (Pinj y Q \<langle>*\<rangle> P) x (R \<langle>*\<rangle> Q)
           else mkPX (Pinj y Q \<langle>*\<rangle> P) x (R \<langle>*\<rangle> Pinj (y - 1) Q)))"
   | "PX P1 x P2 \<langle>*\<rangle> PX Q1 y Q2 =
       mkPX (P1 \<langle>*\<rangle> Q1) (x + y) (P2 \<langle>*\<rangle> Q2) \<langle>+\<rangle>
         (mkPX (P1 \<langle>*\<rangle> mkPinj 1 Q2) x (Pc 0) \<langle>+\<rangle>
           (mkPX (Q1 \<langle>*\<rangle> mkPinj 1 P2) y (Pc 0)))"
   by pat_completeness auto
 termination by (relation "measure (\<lambda>(x, y). size x + size y)")
   (auto simp add: mkPinj_def split: pol.split)
 
 text \<open>Negation\<close>
 primrec neg :: "pol \<Rightarrow> pol"
   where
     "neg (Pc c) = Pc (- c)"
   | "neg (Pinj i P) = Pinj i (neg P)"
   | "neg (PX P x Q) = PX (neg P) x (neg Q)"
 
 text \<open>Subtraction\<close>
 definition sub :: "pol \<Rightarrow> pol \<Rightarrow> pol"  (infixl "\<langle>-\<rangle>" 65)
   where "sub P Q = P \<langle>+\<rangle> neg Q"
 
 text \<open>Square for Fast Exponentiation\<close>
 primrec sqr :: "pol \<Rightarrow> pol"
   where
     "sqr (Pc c) = Pc (c * c)"
   | "sqr (Pinj i P) = mkPinj i (sqr P)"
   | "sqr (PX A x B) = mkPX (sqr A) (x + x) (sqr B) \<langle>+\<rangle> mkPX (Pc 2 \<langle>*\<rangle> A \<langle>*\<rangle> mkPinj 1 B) x (Pc 0)"
 
 text \<open>Fast Exponentiation\<close>
 
 fun pow :: "nat \<Rightarrow> pol \<Rightarrow> pol"
   where pow_if [simp del]: "pow n P =
    (if n = 0 then Pc 1
     else if even n then pow (n div 2) (sqr P)
     else P \<langle>*\<rangle> pow (n div 2) (sqr P))"
 
 lemma pow_simps [simp]:
   "pow 0 P = Pc 1"
   "pow (2 * n) P = pow n (sqr P)"
   "pow (Suc (2 * n)) P = P \<langle>*\<rangle> pow n (sqr P)"
   by (simp_all add: pow_if)
 
 lemma even_pow: "even n \<Longrightarrow> pow n P = pow (n div 2) (sqr P)"
   by (erule evenE) simp
 
 lemma odd_pow: "odd n \<Longrightarrow> pow n P = P \<langle>*\<rangle> pow (n div 2) (sqr P)"
   by (erule oddE) simp
 
 
 text \<open>Normalization of polynomial expressions\<close>
 
 primrec norm :: "polex \<Rightarrow> pol"
   where
     "norm (Var n) =
        (if n = 0 then PX (Pc 1) 1 (Pc 0)
         else Pinj n (PX (Pc 1) 1 (Pc 0)))"
   | "norm (Const i) = Pc i"
   | "norm (Add P Q) = norm P \<langle>+\<rangle> norm Q"
   | "norm (Sub P Q) = norm P \<langle>-\<rangle> norm Q"
   | "norm (Mul P Q) = norm P \<langle>*\<rangle> norm Q"
   | "norm (Pow P n) = pow n (norm P)"
   | "norm (Neg P) = neg (norm P)"
 
 context cring
 begin
 
 text \<open>mkPinj preserve semantics\<close>
 lemma mkPinj_ci: "Ipol l (mkPinj a B) = Ipol l (Pinj a B)"
   by (induct B) (auto simp add: mkPinj_def algebra_simps)
 
 text \<open>mkPX preserves semantics\<close>
 lemma mkPX_ci: "in_carrier l \<Longrightarrow> Ipol l (mkPX A b C) = Ipol l (PX A b C)"
   by (cases A) (auto simp add: mkPX_def mkPinj_ci nat_pow_mult [symmetric] m_ac)
 
 text \<open>Correctness theorems for the implemented operations\<close>
 
 text \<open>Negation\<close>
 lemma neg_ci: "in_carrier l \<Longrightarrow> Ipol l (neg P) = \<ominus> (Ipol l P)"
   by (induct P arbitrary: l) (auto simp add: minus_add l_minus)
 
 text \<open>Addition\<close>
 lemma add_ci: "in_carrier l \<Longrightarrow> Ipol l (P \<langle>+\<rangle> Q) = Ipol l P \<oplus> Ipol l Q"
 proof (induct P Q arbitrary: l rule: add.induct)
   case (6 x P y Q)
   consider "x < y" | "x = y" | "x > y" by arith
   then show ?case
   proof cases
     case 1
     with 6 show ?thesis by (simp add: mkPinj_ci a_ac)
   next
     case 2
     with 6 show ?thesis by (simp add: mkPinj_ci)
   next
     case 3
     with 6 show ?thesis by (simp add: mkPinj_ci)
   qed
 next
   case (7 x P Q y R)
   consider "x = 0" | "x = 1" | "x > 1" by arith
   then show ?case
   proof cases
     case 1
     with 7 show ?thesis by simp
   next
     case 2
     with 7 show ?thesis by (simp add: a_ac)
   next
     case 3
     with 7 show ?thesis by (cases x) (simp_all add: a_ac)
   qed
 next
   case (8 P x R y Q)
   then show ?case by (simp add: a_ac)
 next
   case (9 P1 x P2 Q1 y Q2)
   consider "x = y" | d where "d + x = y" | d where "d + y = x"
     by atomize_elim arith
   then show ?case
   proof cases
     case 1
     with 9 show ?thesis by (simp add: mkPX_ci r_distr a_ac m_ac)
   next
     case 2
     with 9 show ?thesis by (auto simp add: mkPX_ci nat_pow_mult [symmetric] r_distr a_ac m_ac)
   next
     case 3
     with 9 show ?thesis by (auto simp add: nat_pow_mult [symmetric] mkPX_ci r_distr a_ac m_ac)
   qed
 qed (auto simp add: a_ac m_ac)
 
 text \<open>Multiplication\<close>
 lemma mul_ci: "in_carrier l \<Longrightarrow> Ipol l (P \<langle>*\<rangle> Q) = Ipol l P \<otimes> Ipol l Q"
   by (induct P Q arbitrary: l rule: mul.induct)
     (simp_all add: mkPX_ci mkPinj_ci a_ac m_ac r_distr add_ci nat_pow_mult [symmetric])
 
 text \<open>Subtraction\<close>
 lemma sub_ci: "in_carrier l \<Longrightarrow> Ipol l (P \<langle>-\<rangle> Q) = Ipol l P \<ominus> Ipol l Q"
   by (simp add: add_ci neg_ci sub_def minus_eq)
 
 text \<open>Square\<close>
 lemma sqr_ci: "in_carrier ls \<Longrightarrow> Ipol ls (sqr P) = Ipol ls P \<otimes> Ipol ls P"
   by (induct P arbitrary: ls)
     (simp_all add: add_ci mkPinj_ci mkPX_ci mul_ci l_distr r_distr
        a_ac m_ac nat_pow_mult [symmetric] of_int_2)
 
 text \<open>Power\<close>
 lemma pow_ci: "in_carrier ls \<Longrightarrow> Ipol ls (pow n P) = Ipol ls P [^] n"
 proof (induct n arbitrary: P rule: less_induct)
   case (less k)
   consider "k = 0" | "k > 0" by arith
   then show ?case
   proof cases
     case 1
     then show ?thesis by simp
   next
     case 2
     then have "k div 2 < k" by arith
     with less have *: "Ipol ls (pow (k div 2) (sqr P)) = Ipol ls (sqr P) [^] (k div 2)"
       by simp
     show ?thesis
     proof (cases "even k")
       case True
       with * \<open>in_carrier ls\<close> show ?thesis
         by (simp add: even_pow sqr_ci nat_pow_distrib nat_pow_mult
           mult_2 [symmetric] even_two_times_div_two)
     next
       case False
       with * \<open>in_carrier ls\<close> show ?thesis
         by (simp add: odd_pow mul_ci sqr_ci nat_pow_distrib nat_pow_mult
           mult_2 [symmetric] trans [OF nat_pow_Suc m_comm, symmetric])
     qed
   qed
 qed
 
 text \<open>Normalization preserves semantics\<close>
 lemma norm_ci: "in_carrier l \<Longrightarrow> Ipolex l Pe = Ipol l (norm Pe)"
   by (induct Pe) (simp_all add: add_ci sub_ci mul_ci neg_ci pow_ci)
 
 text \<open>Reflection lemma: Key to the (incomplete) decision procedure\<close>
 lemma norm_eq:
   assumes "in_carrier l"
   and "norm P1 = norm P2"
   shows "Ipolex l P1 = Ipolex l P2"
 proof -
   from assms have "Ipol l (norm P1) = Ipol l (norm P2)" by simp
   with assms show ?thesis by (simp only: norm_ci)
 qed
 
 end
 
 
 text \<open>Monomials\<close>
 
 datatype mon =
     Mc int
   | Minj nat mon
   | MX nat mon
 
 primrec (in cring) Imon :: "'a list \<Rightarrow> mon \<Rightarrow> 'a"
   where
     "Imon l (Mc c) = \<guillemotleft>c\<guillemotright>"
   | "Imon l (Minj i M) = Imon (drop i l) M"
   | "Imon l (MX x M) = Imon (drop 1 l) M \<otimes> head l [^] x"
 
 lemma (in cring) Imon_closed [simp]: "in_carrier l \<Longrightarrow> Imon l m \<in> carrier R"
   by (induct m arbitrary: l) simp_all
 
 definition mkMinj :: "nat \<Rightarrow> mon \<Rightarrow> mon"
   where "mkMinj i M =
     (case M of
       Mc c \<Rightarrow> Mc c
     | Minj j M \<Rightarrow> Minj (i + j) M
     | _ \<Rightarrow> Minj i M)"
 
 definition Minj_pred :: "nat \<Rightarrow> mon \<Rightarrow> mon"
   where "Minj_pred i M = (if i = 1 then M else mkMinj (i - 1) M)"
 
 primrec mkMX :: "nat \<Rightarrow> mon \<Rightarrow> mon"
   where
     "mkMX i (Mc c) = MX i (Mc c)"
   | "mkMX i (Minj j M) = (if j = 0 then mkMX i M else MX i (Minj_pred j M))"
   | "mkMX i (MX j M) = MX (i + j) M"
 
 lemma (in cring) mkMinj_correct: "Imon l (mkMinj i M) = Imon l (Minj i M)"
   by (simp add: mkMinj_def add.commute split: mon.split)
 
 lemma (in cring) Minj_pred_correct: "0 < i \<Longrightarrow> Imon (drop 1 l) (Minj_pred i M) = Imon l (Minj i M)"
   by (simp add: Minj_pred_def mkMinj_correct)
 
 lemma (in cring) mkMX_correct: "in_carrier l \<Longrightarrow> Imon l (mkMX i M) = Imon l M \<otimes> head l [^] i"
   by (induct M)
     (simp_all add: Minj_pred_correct [simplified] nat_pow_mult [symmetric] m_ac split: mon.split)
 
 fun cfactor :: "pol \<Rightarrow> int \<Rightarrow> pol \<times> pol"
   where
     "cfactor (Pc c') c = (Pc (c' mod c), Pc (c' div c))"
   | "cfactor (Pinj i P) c =
        (let (R, S) = cfactor P c
         in (mkPinj i R, mkPinj i S))"
   | "cfactor (PX P i Q) c =
        (let
           (R1, S1) = cfactor P c;
           (R2, S2) = cfactor Q c
         in (mkPX R1 i R2, mkPX S1 i S2))"
 
 lemma (in cring) cfactor_correct:
   "in_carrier l \<Longrightarrow> Ipol l P = Ipol l (fst (cfactor P c)) \<oplus> \<guillemotleft>c\<guillemotright> \<otimes> Ipol l (snd (cfactor P c))"
 proof (induct P c arbitrary: l rule: cfactor.induct)
   case (1 c' c)
   show ?case
     by (simp add: of_int_mult [symmetric] of_int_add [symmetric] del: of_int_mult)
 next
   case (2 i P c)
   then show ?case
     by (simp add: mkPinj_ci split_beta)
 next
   case (3 P i Q c)
   from 3(1) 3(2) [OF refl prod.collapse] 3(3)
   show ?case
     by (simp add: mkPX_ci r_distr a_ac m_ac split_beta)
 qed
 
 fun mfactor :: "pol \<Rightarrow> mon \<Rightarrow> pol \<times> pol"
   where
     "mfactor P (Mc c) = (if c = 1 then (Pc 0, P) else cfactor P c)"
   | "mfactor (Pc d) M = (Pc d, Pc 0)"
   | "mfactor (Pinj i P) (Minj j M) =
        (if i = j then
           let (R, S) = mfactor P M
           in (mkPinj i R, mkPinj i S)
         else if i < j then
           let (R, S) = mfactor P (Minj (j - i) M)
           in (mkPinj i R, mkPinj i S)
         else (Pinj i P, Pc 0))"
   | "mfactor (Pinj i P) (MX j M) = (Pinj i P, Pc 0)"
   | "mfactor (PX P i Q) (Minj j M) =
        (if j = 0 then mfactor (PX P i Q) M
         else
           let
             (R1, S1) = mfactor P (Minj j M);
             (R2, S2) = mfactor Q (Minj_pred j M)
           in (mkPX R1 i R2, mkPX S1 i S2))"
   | "mfactor (PX P i Q) (MX j M) =
        (if i = j then
           let (R, S) = mfactor P (mkMinj 1 M)
           in (mkPX R i Q, S)
         else if i < j then
           let (R, S) = mfactor P (MX (j - i) M)
           in (mkPX R i Q, S)
         else
           let (R, S) = mfactor P (mkMinj 1 M)
           in (mkPX R i Q, mkPX S (i - j) (Pc 0)))"
 
 lemmas mfactor_induct = mfactor.induct
   [case_names Mc Pc_Minj Pc_MX Pinj_Minj Pinj_MX PX_Minj PX_MX]
 
 lemma (in cring) mfactor_correct:
   "in_carrier l \<Longrightarrow>
    Ipol l P =
    Ipol l (fst (mfactor P M)) \<oplus>
    Imon l M \<otimes> Ipol l (snd (mfactor P M))"
 proof (induct P M arbitrary: l rule: mfactor_induct)
   case (Mc P c)
   then show ?case
     by (simp add: cfactor_correct)
 next
   case (Pc_Minj d i M)
   then show ?case
     by simp
 next
   case (Pc_MX d i M)
   then show ?case
     by simp
 next
   case (Pinj_Minj i P j M)
   then show ?case
     by (simp add: mkPinj_ci split_beta)
 next
   case (Pinj_MX i P j M)
   then show ?case
     by simp
 next
   case (PX_Minj P i Q j M)
   from PX_Minj(1,2) PX_Minj(3) [OF _ refl prod.collapse] PX_Minj(4)
   show ?case
     by (simp add: mkPX_ci Minj_pred_correct [simplified] r_distr a_ac m_ac split_beta)
 next
   case (PX_MX P i Q j M)
   from \<open>in_carrier l\<close>
   have eq1: "(Imon (drop (Suc 0) l) M \<otimes> head l [^] (j - i)) \<otimes>
     Ipol l (snd (mfactor P (MX (j - i) M))) \<otimes> head l [^] i =
     Imon (drop (Suc 0) l) M \<otimes>
     Ipol l (snd (mfactor P (MX (j - i) M))) \<otimes>
     (head l [^] (j - i) \<otimes> head l [^] i)"
     by (simp add: m_ac)
   from \<open>in_carrier l\<close>
   have eq2: "(Imon (drop (Suc 0) l) M \<otimes> head l [^] j) \<otimes>
     (Ipol l (snd (mfactor P (mkMinj (Suc 0) M))) \<otimes> head l [^] (i - j)) =
     Imon (drop (Suc 0) l) M \<otimes>
     Ipol l (snd (mfactor P (mkMinj (Suc 0) M))) \<otimes>
     (head l [^] (i - j) \<otimes> head l [^] j)"
     by (simp add: m_ac)
   from PX_MX \<open>in_carrier l\<close> show ?case
     by (simp add: mkPX_ci mkMinj_correct l_distr eq1 eq2 split_beta nat_pow_mult)
       (simp add: a_ac m_ac)
 qed
 
 primrec mon_of_pol :: "pol \<Rightarrow> mon option"
   where
     "mon_of_pol (Pc c) = Some (Mc c)"
   | "mon_of_pol (Pinj i P) = (case mon_of_pol P of
          None \<Rightarrow> None
        | Some M \<Rightarrow> Some (mkMinj i M))"
   | "mon_of_pol (PX P i Q) =
        (if Q = Pc 0 then (case mon_of_pol P of
             None \<Rightarrow> None
           | Some M \<Rightarrow> Some (mkMX i M))
         else None)"
 
 lemma (in cring) mon_of_pol_correct:
   assumes "in_carrier l"
     and "mon_of_pol P = Some M"
   shows "Ipol l P = Imon l M"
   using assms
 proof (induct P arbitrary: M l)
   case (PX P1 i P2)
   from PX(1,3,4)
   show ?case
     by (auto simp add: mkMinj_correct mkMX_correct split: if_split_asm option.split_asm)
 qed (auto simp add: mkMinj_correct split: option.split_asm)
 
 fun (in cring) Ipolex_polex_list :: "'a list \<Rightarrow> (polex \<times> polex) list \<Rightarrow> bool"
   where
     "Ipolex_polex_list l [] = True"
   | "Ipolex_polex_list l ((P, Q) # pps) = ((Ipolex l P = Ipolex l Q) \<and> Ipolex_polex_list l pps)"
 
 fun (in cring) Imon_pol_list :: "'a list \<Rightarrow> (mon \<times> pol) list \<Rightarrow> bool"
   where
     "Imon_pol_list l [] = True"
   | "Imon_pol_list l ((M, P) # mps) = ((Imon l M = Ipol l P) \<and> Imon_pol_list l mps)"
 
 fun mk_monpol_list :: "(polex \<times> polex) list \<Rightarrow> (mon \<times> pol) list"
   where
     "mk_monpol_list [] = []"
   | "mk_monpol_list ((P, Q) # pps) =
        (case mon_of_pol (norm P) of
           None \<Rightarrow> mk_monpol_list pps
         | Some M \<Rightarrow> (M, norm Q) # mk_monpol_list pps)"
 
 lemma (in cring) mk_monpol_list_correct:
   "in_carrier l \<Longrightarrow> Ipolex_polex_list l pps \<Longrightarrow> Imon_pol_list l (mk_monpol_list pps)"
   by (induct pps rule: mk_monpol_list.induct)
     (auto split: option.split simp add: norm_ci [symmetric] mon_of_pol_correct [symmetric])
 
 definition ponesubst :: "pol \<Rightarrow> mon \<Rightarrow> pol \<Rightarrow> pol option"
   where "ponesubst P1 M P2 =
    (let (Q, R) = mfactor P1 M in
     (case R of
       Pc c \<Rightarrow> if c = 0 then None else Some (add Q (mul P2 R))
     | _ \<Rightarrow> Some (add Q (mul P2 R))))"
 
 fun pnsubst1 :: "pol \<Rightarrow> mon \<Rightarrow> pol \<Rightarrow> nat \<Rightarrow> pol"
   where "pnsubst1 P1 M P2 n =
     (case ponesubst P1 M P2 of
       None \<Rightarrow> P1
     | Some P3 \<Rightarrow> if n = 0 then P3 else pnsubst1 P3 M P2 (n - 1))"
 
 lemma pnsubst1_0 [simp]: "pnsubst1 P1 M P2 0 = (case ponesubst P1 M P2 of
   None \<Rightarrow> P1 | Some P3 \<Rightarrow> P3)"
   by (simp split: option.split)
 
 lemma pnsubst1_Suc [simp]:
   "pnsubst1 P1 M P2 (Suc n) =
     (case ponesubst P1 M P2 of
       None \<Rightarrow> P1
     | Some P3 \<Rightarrow> pnsubst1 P3 M P2 n)"
   by (simp split: option.split)
 
 declare pnsubst1.simps [simp del]
 
 definition pnsubst :: "pol \<Rightarrow> mon \<Rightarrow> pol \<Rightarrow> nat \<Rightarrow> pol option"
   where "pnsubst P1 M P2 n =
     (case ponesubst P1 M P2 of
       None \<Rightarrow> None
     | Some P3 \<Rightarrow> Some (pnsubst1 P3 M P2 n))"
 
 fun psubstl1 :: "pol \<Rightarrow> (mon \<times> pol) list \<Rightarrow> nat \<Rightarrow> pol"
   where
     "psubstl1 P1 [] n = P1"
   | "psubstl1 P1 ((M, P2) # mps) n = psubstl1 (pnsubst1 P1 M P2 n) mps n"
 
 fun psubstl :: "pol \<Rightarrow> (mon \<times> pol) list \<Rightarrow> nat \<Rightarrow> pol option"
   where
     "psubstl P1 [] n = None"
   | "psubstl P1 ((M, P2) # mps) n =
       (case pnsubst P1 M P2 n of
         None \<Rightarrow> psubstl P1 mps n
       | Some P3 \<Rightarrow> Some (psubstl1 P3 mps n))"
 
 fun pnsubstl :: "pol \<Rightarrow> (mon \<times> pol) list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> pol"
   where "pnsubstl P1 mps m n =
     (case psubstl P1 mps n of
       None \<Rightarrow> P1
     | Some P3 \<Rightarrow> if m = 0 then P3 else pnsubstl P3 mps (m - 1) n)"
 
 lemma pnsubstl_0 [simp]:
   "pnsubstl P1 mps 0 n = (case psubstl P1 mps n of None \<Rightarrow> P1 | Some P3 \<Rightarrow> P3)"
   by (simp split: option.split)
 
 lemma pnsubstl_Suc [simp]:
   "pnsubstl P1 mps (Suc m) n = (case psubstl P1 mps n of None \<Rightarrow> P1 | Some P3 \<Rightarrow> pnsubstl P3 mps m n)"
   by (simp split: option.split)
 
 declare pnsubstl.simps [simp del]
 
 lemma (in cring) ponesubst_correct:
   "in_carrier l \<Longrightarrow> ponesubst P1 M P2 = Some P3 \<Longrightarrow> Imon l M = Ipol l P2 \<Longrightarrow> Ipol l P1 = Ipol l P3"
   by (auto simp add: ponesubst_def split_beta mfactor_correct [of l P1 M]
     add_ci mul_ci split: pol.split_asm if_split_asm)
 
 lemma (in cring) pnsubst1_correct:
   "in_carrier l \<Longrightarrow> Imon l M = Ipol l P2 \<Longrightarrow> Ipol l (pnsubst1 P1 M P2 n) = Ipol l P1"
   by (induct n arbitrary: P1)
     (simp_all add: ponesubst_correct split: option.split)
 
 lemma (in cring) pnsubst_correct:
   "in_carrier l \<Longrightarrow> pnsubst P1 M P2 n = Some P3 \<Longrightarrow> Imon l M = Ipol l P2 \<Longrightarrow> Ipol l P1 = Ipol l P3"
   by (auto simp add: pnsubst_def
     pnsubst1_correct ponesubst_correct split: option.split_asm)
 
 lemma (in cring) psubstl1_correct:
   "in_carrier l \<Longrightarrow> Imon_pol_list l mps \<Longrightarrow> Ipol l (psubstl1 P1 mps n) = Ipol l P1"
   by (induct P1 mps n rule: psubstl1.induct) (simp_all add: pnsubst1_correct)
 
 lemma (in cring) psubstl_correct:
   "in_carrier l \<Longrightarrow> psubstl P1 mps n = Some P2 \<Longrightarrow> Imon_pol_list l mps \<Longrightarrow> Ipol l P1 = Ipol l P2"
   by (induct P1 mps n rule: psubstl.induct)
     (auto simp add: psubstl1_correct pnsubst_correct split: option.split_asm)
 
 lemma (in cring) pnsubstl_correct:
   "in_carrier l \<Longrightarrow> Imon_pol_list l mps \<Longrightarrow> Ipol l (pnsubstl P1 mps m n) = Ipol l P1"
   by (induct m arbitrary: P1)
     (simp_all add: psubstl_correct split: option.split)
 
 lemma (in cring) norm_subst_correct:
   "in_carrier l \<Longrightarrow> Ipolex_polex_list l pps \<Longrightarrow>
    Ipolex l P = Ipol l (pnsubstl (norm P) (mk_monpol_list pps) m n)"
   by (simp add: pnsubstl_correct mk_monpol_list_correct norm_ci)
 
 lemma in_carrier_trivial: "cring_class.in_carrier l"
   by (induct l) (simp_all add: cring_class.in_carrier_def carrier_class)
 
 ML \<open>
 val term_of_nat = HOLogic.mk_number \<^Type>\<open>nat\<close> o @{code integer_of_nat};
 
 val term_of_int = HOLogic.mk_number \<^Type>\<open>int\<close> o @{code integer_of_int};
 
 fun term_of_pol (@{code Pc} k) = \<^Const>\<open>Pc\<close> $ term_of_int k
   | term_of_pol (@{code Pinj} (n, p)) = \<^Const>\<open>Pinj\<close> $ term_of_nat n $ term_of_pol p
   | term_of_pol (@{code PX} (p, n, q)) = \<^Const>\<open>PX\<close> $ term_of_pol p $ term_of_nat n $ term_of_pol q;
 
 local
 
-fun pol (ctxt, ct, t) = Thm.mk_binop \<^cterm>\<open>Pure.eq :: pol \<Rightarrow> pol \<Rightarrow> prop\<close>
-  ct (Thm.cterm_of ctxt t);
+fun pol (ctxt, ct, t) =
+  \<^let>\<open>x = ct and y = \<open>Thm.cterm_of ctxt t\<close>
+    in cterm \<open>x \<equiv> y\<close> for x y :: pol\<close>;
 
 val (_, raw_pol_oracle) = Context.>>> (Context.map_theory_result
   (Thm.add_oracle (\<^binding>\<open>pnsubstl\<close>, pol)));
 
 fun pol_oracle ctxt ct t = raw_pol_oracle (ctxt, ct, t);
 
 in
 
 val cv = @{computation_conv pol
   terms: pnsubstl mk_monpol_list norm
     nat_of_integer Code_Target_Nat.natural
       "0::nat" "1::nat" "2::nat" "3::nat"
       "0::int" "1::int" "2::int" "3::int" "-1::int"
   datatypes: polex "(polex * polex) list" int integer num}
   (fn ctxt => fn p => fn ct => pol_oracle ctxt ct (term_of_pol p))
 
 end
 \<close>
 
 ML \<open>
 signature RING_TAC =
 sig
   structure Ring_Simps:
   sig
     type T
     val get: Context.generic -> T
     val put: T -> Context.generic -> Context.generic
     val map: (T -> T) -> Context.generic -> Context.generic
   end
   val insert_rules: ((term * 'a) * (term * 'a) -> bool) -> (term * 'a) ->
     (term * 'a) Net.net -> (term * 'a) Net.net
   val eq_ring_simps:
     (term * (thm list * thm list * thm list * thm list * thm * thm)) *
     (term * (thm list * thm list * thm list * thm list * thm * thm)) -> bool
   val ring_tac: bool -> thm list -> Proof.context -> int -> tactic
   val get_matching_rules: Proof.context -> (term * 'a) Net.net -> term -> 'a option
   val norm: thm -> thm
   val mk_in_carrier: Proof.context -> term -> thm list -> (string * typ) list -> thm
   val mk_ring: typ -> term
 end
 
 structure Ring_Tac : RING_TAC =
 struct
 
 fun eq_ring_simps
   ((t, (ths1, ths2, ths3, ths4, th5, th)),
    (t', (ths1', ths2', ths3', ths4', th5', th'))) =
     t aconv t' andalso
     eq_list Thm.eq_thm (ths1, ths1') andalso
     eq_list Thm.eq_thm (ths2, ths2') andalso
     eq_list Thm.eq_thm (ths3, ths3') andalso
     eq_list Thm.eq_thm (ths4, ths4') andalso
     Thm.eq_thm (th5, th5') andalso
     Thm.eq_thm (th, th');
 
 structure Ring_Simps = Generic_Data
 (struct
   type T = (term * (thm list * thm list * thm list * thm list * thm * thm)) Net.net
   val empty = Net.empty
   val merge = Net.merge eq_ring_simps
 end);
 
 fun get_matching_rules ctxt net t = get_first
   (fn (p, x) =>
      if Pattern.matches (Proof_Context.theory_of ctxt) (p, t) then SOME x else NONE)
   (Net.match_term net t);
 
 fun insert_rules eq (t, x) = Net.insert_term eq (t, (t, x));
 
 fun norm thm = thm COMP_INCR asm_rl;
 
 fun get_ring_simps ctxt optcT t =
   (case get_matching_rules ctxt (Ring_Simps.get (Context.Proof ctxt)) t of
      SOME (ths1, ths2, ths3, ths4, th5, th) =>
        let val tr =
          Thm.transfer' ctxt #>
          (case optcT of NONE => I | SOME cT => inst [cT] [] #> norm)
        in (map tr ths1, map tr ths2, map tr ths3, map tr ths4, tr th5, tr th) end
    | NONE => error "get_ring_simps: lookup failed");
 
 fun ring_struct \<^Const_>\<open>Ring.ring.add _ _ for R _ _\<close> = SOME R
   | ring_struct \<^Const_>\<open>Ring.a_minus _ _ for R _ _\<close> = SOME R
   | ring_struct \<^Const_>\<open>Group.monoid.mult _ _ for R _ _\<close> = SOME R
   | ring_struct \<^Const_>\<open>Ring.a_inv _ _ for R _\<close> = SOME R
   | ring_struct \<^Const_>\<open>Group.pow _ _ _ for R _ _\<close> = SOME R
   | ring_struct \<^Const_>\<open>Ring.ring.zero _ _ for R\<close> = SOME R
   | ring_struct \<^Const_>\<open>Group.monoid.one _ _ for R\<close> = SOME R
   | ring_struct \<^Const_>\<open>Algebra_Aux.of_integer _ _ for R _\<close> = SOME R
   | ring_struct _ = NONE;
 
 fun reif_polex vs \<^Const_>\<open>Ring.ring.add _ _ for _ a b\<close> =
       \<^Const>\<open>Add for \<open>reif_polex vs a\<close> \<open>reif_polex vs b\<close>\<close>
   | reif_polex vs \<^Const_>\<open>Ring.a_minus _ _ for _ a b\<close> =
       \<^Const>\<open>Sub for \<open>reif_polex vs a\<close> \<open>reif_polex vs b\<close>\<close>
   | reif_polex vs \<^Const_>\<open>Group.monoid.mult _ _ for _ a b\<close> =
       \<^Const>\<open>Mul for \<open>reif_polex vs a\<close> \<open>reif_polex vs b\<close>\<close>
   | reif_polex vs \<^Const_>\<open>Ring.a_inv _ _ for _ a\<close> =
       \<^Const>\<open>Neg for \<open>reif_polex vs a\<close>\<close>
   | reif_polex vs \<^Const_>\<open>Group.pow _ _ _ for _ a n\<close> =
       \<^Const>\<open>Pow for \<open>reif_polex vs a\<close> n\<close>
   | reif_polex vs (Free x) =
       \<^Const>\<open>Var for \<open>HOLogic.mk_number HOLogic.natT (find_index (equal x) vs)\<close>\<close>
   | reif_polex _ \<^Const_>\<open>Ring.ring.zero _ _ for _\<close> = \<^term>\<open>Const 0\<close>
   | reif_polex _ \<^Const_>\<open>Group.monoid.one _ _ for _\<close> = \<^term>\<open>Const 1\<close>
   | reif_polex _ \<^Const_>\<open>Algebra_Aux.of_integer _ _ for _ n\<close> = \<^Const>\<open>Const for n\<close>
   | reif_polex _ _ = error "reif_polex: bad expression";
 
 fun reif_polex' vs \<^Const_>\<open>plus _ for a b\<close> = \<^Const>\<open>Add for \<open>reif_polex' vs a\<close> \<open>reif_polex' vs b\<close>\<close>
   | reif_polex' vs \<^Const_>\<open>minus _ for a b\<close> = \<^Const>\<open>Sub for \<open>reif_polex' vs a\<close> \<open>reif_polex' vs b\<close>\<close>
   | reif_polex' vs \<^Const_>\<open>times _ for a b\<close> = \<^Const>\<open>Mul for \<open>reif_polex' vs a\<close> \<open>reif_polex' vs b\<close>\<close>
   | reif_polex' vs \<^Const_>\<open>uminus _ for a\<close> = \<^Const>\<open>Neg for \<open>reif_polex' vs a\<close>\<close>
   | reif_polex' vs \<^Const_>\<open>power _ for a n\<close> = \<^Const>\<open>Pow for \<open>reif_polex' vs a\<close> n\<close>
   | reif_polex' vs (Free x) = \<^Const>\<open>Var for \<open>HOLogic.mk_number \<^Type>\<open>nat\<close> (find_index (equal x) vs)\<close>\<close>
   | reif_polex' _ \<^Const_>\<open>numeral _ for b\<close> = \<^Const>\<open>Const for \<^Const>\<open>numeral \<^Type>\<open>int\<close> for b\<close>\<close>
   | reif_polex' _ \<^Const_>\<open>zero_class.zero _\<close> = \<^term>\<open>Const 0\<close>
   | reif_polex' _ \<^Const_>\<open>one_class.one _\<close> = \<^term>\<open>Const 1\<close>
   | reif_polex' _ t = error "reif_polex: bad expression";
 
 fun head_conv (_, _, _, _, head_simp, _) ys =
   (case strip_app ys of
      (\<^const_name>\<open>Cons\<close>, [y, xs]) => inst [] [y, xs] head_simp);
 
 fun Ipol_conv (rls as
       ([Ipol_simps_1, Ipol_simps_2, Ipol_simps_3,
         Ipol_simps_4, Ipol_simps_5, Ipol_simps_6,
         Ipol_simps_7], _, _, _, _, _)) =
   let
     val a = type_of_eqn Ipol_simps_1;
     val drop_conv_a = drop_conv a;
 
     fun conv l p = (case strip_app p of
         (\<^const_name>\<open>Pc\<close>, [c]) => (case strip_numeral c of
             (\<^const_name>\<open>zero_class.zero\<close>, _) => inst [] [l] Ipol_simps_4
           | (\<^const_name>\<open>one_class.one\<close>, _) => inst [] [l] Ipol_simps_5
           | (\<^const_name>\<open>numeral\<close>, [m]) => inst [] [l, m] Ipol_simps_6
           | (\<^const_name>\<open>uminus\<close>, [m]) => inst [] [l, m] Ipol_simps_7
           | _ => inst [] [l, c] Ipol_simps_1)
       | (\<^const_name>\<open>Pinj\<close>, [i, P]) =>
           transitive'
             (inst [] [l, i, P] Ipol_simps_2)
             (cong2' conv (args2 drop_conv_a) Thm.reflexive)
       | (\<^const_name>\<open>PX\<close>, [P, x, Q]) =>
           transitive'
             (inst [] [l, P, x, Q] Ipol_simps_3)
             (cong2
                (cong2
                   (args2 conv) (cong2 (args1 (head_conv rls)) Thm.reflexive))
                (cong2' conv (args2 drop_conv_a) Thm.reflexive)))
   in conv end;
 
 fun Ipolex_conv (rls as
       (_,
        [Ipolex_Var, Ipolex_Const, Ipolex_Add,
         Ipolex_Sub, Ipolex_Mul, Ipolex_Pow,
         Ipolex_Neg, Ipolex_Const_0, Ipolex_Const_1,
         Ipolex_Const_numeral], _, _, _, _)) =
   let
     val a = type_of_eqn Ipolex_Var;
     val drop_conv_a = drop_conv a;
 
     fun conv l r = (case strip_app r of
         (\<^const_name>\<open>Var\<close>, [n]) =>
           transitive'
             (inst [] [l, n] Ipolex_Var)
             (cong1' (head_conv rls) (args2 drop_conv_a))
       | (\<^const_name>\<open>Const\<close>, [i]) => (case strip_app i of
             (\<^const_name>\<open>zero_class.zero\<close>, _) => inst [] [l] Ipolex_Const_0
           | (\<^const_name>\<open>one_class.one\<close>, _) => inst [] [l] Ipolex_Const_1
           | (\<^const_name>\<open>numeral\<close>, [m]) => inst [] [l, m] Ipolex_Const_numeral
           | _ => inst [] [l, i] Ipolex_Const)
       | (\<^const_name>\<open>Add\<close>, [P, Q]) =>
           transitive'
             (inst [] [l, P, Q] Ipolex_Add)
             (cong2 (args2 conv) (args2 conv))
       | (\<^const_name>\<open>Sub\<close>, [P, Q]) =>
           transitive'
             (inst [] [l, P, Q] Ipolex_Sub)
             (cong2 (args2 conv) (args2 conv))
       | (\<^const_name>\<open>Mul\<close>, [P, Q]) =>
           transitive'
             (inst [] [l, P, Q] Ipolex_Mul)
             (cong2 (args2 conv) (args2 conv))
       | (\<^const_name>\<open>Pow\<close>, [P, n]) =>
           transitive'
             (inst [] [l, P, n] Ipolex_Pow)
             (cong2 (args2 conv) Thm.reflexive)
       | (\<^const_name>\<open>Neg\<close>, [P]) =>
           transitive'
             (inst [] [l, P] Ipolex_Neg)
             (cong1 (args2 conv)))
   in conv end;
 
 fun Ipolex_polex_list_conv (rls as
       (_, _,
        [Ipolex_polex_list_Nil, Ipolex_polex_list_Cons], _, _, _)) l pps =
   (case strip_app pps of
      (\<^const_name>\<open>Nil\<close>, []) => inst [] [l] Ipolex_polex_list_Nil
    | (\<^const_name>\<open>Cons\<close>, [p, pps']) => (case strip_app p of
        (\<^const_name>\<open>Pair\<close>, [P, Q]) =>
          transitive'
            (inst [] [l, P, Q, pps'] Ipolex_polex_list_Cons)
            (cong2
               (cong2 (args2 (Ipolex_conv rls)) (args2 (Ipolex_conv rls)))
               (args2 (Ipolex_polex_list_conv rls)))));
 
 fun dest_conj th =
   let
     val th1 = th RS @{thm conjunct1};
     val th2 = th RS @{thm conjunct2}
   in
     dest_conj th1 @ dest_conj th2
   end handle THM _ => [th];
 
 fun mk_in_carrier ctxt R prems xs =
   let
     val (_, _, _, [in_carrier_Nil, in_carrier_Cons], _, _) =
       get_ring_simps ctxt NONE R;
     val props = map fst (Facts.props (Proof_Context.facts_of ctxt)) @ maps dest_conj prems;
     val ths = map (fn p as (x, _) =>
       (case find_first
          ((fn \<^Const_>\<open>Trueprop
               for \<^Const_>\<open>Set.member _ for \<open>Free (y, _)\<close> \<^Const_>\<open>carrier _ _ for S\<close>\<close>\<close> =>
                 x = y andalso R aconv S
             | _ => false) o Thm.prop_of) props of
          SOME th => th
        | NONE => error ("Variable " ^ Syntax.string_of_term ctxt (Free p) ^
            " not in carrier"))) xs
   in
     fold_rev (fn th1 => fn th2 => [th1, th2] MRS in_carrier_Cons)
        ths in_carrier_Nil
   end;
 
 fun mk_ring T = \<^Const>\<open>cring_class_ops T\<close>;
 
 val iterations = \<^cterm>\<open>1000::nat\<close>;
 val Trueprop_cong = Thm.combination (Thm.reflexive \<^cterm>\<open>Trueprop\<close>);
 
 fun commutative_ring_conv ctxt prems eqs ct =
   let
     val cT = Thm.ctyp_of_cterm ct;
     val T = Thm.typ_of cT;
     val eqs' = map (HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of) eqs;
     val xs = filter (equal T o snd) (rev (fold Term.add_frees
       (map fst eqs' @ map snd eqs' @ [Thm.term_of ct]) []));
     val (R, optcT, prem', reif) = (case ring_struct (Thm.term_of ct) of
         SOME R => (R, NONE, mk_in_carrier ctxt R prems xs, reif_polex xs)
       | NONE => (mk_ring T, SOME cT, @{thm in_carrier_trivial}, reif_polex' xs));
     val rls as (_, _, _, _, _, norm_subst_correct) = get_ring_simps ctxt optcT R;
     val cxs = Thm.cterm_of ctxt (HOLogic.mk_list T (map Free xs));
     val ceqs = Thm.cterm_of ctxt (HOLogic.mk_list \<^typ>\<open>polex \<times> polex\<close>
       (map (HOLogic.mk_prod o apply2 reif) eqs'));
     val cp = Thm.cterm_of ctxt (reif (Thm.term_of ct));
     val prem = Thm.equal_elim
       (Trueprop_cong (Thm.symmetric (Ipolex_polex_list_conv rls cxs ceqs)))
       (fold_rev (fn th1 => fn th2 => [th1, th2] MRS @{thm conjI})
          eqs @{thm TrueI});
   in
     Thm.transitive
       (Thm.symmetric (Ipolex_conv rls cxs cp))
       (transitive'
          ([prem', prem] MRS inst [] [cxs, ceqs, cp, iterations, iterations]
             norm_subst_correct)
          (cong2' (Ipol_conv rls)
             Thm.reflexive
             (cv ctxt)))
   end;
 
 fun ring_tac in_prems thms ctxt =
   tactic_of_conv (fn ct =>
     (if in_prems then Conv.prems_conv else Conv.concl_conv)
       (Logic.count_prems (Thm.term_of ct))
       (Conv.arg_conv (Conv.binop_conv (commutative_ring_conv ctxt [] thms))) ct) THEN'
   TRY o (assume_tac ctxt ORELSE' resolve_tac ctxt [@{thm refl}]);
 
 end
 \<close>
 
 context cring
 begin
 
 local_setup \<open>
 Local_Theory.declaration {syntax = false, pervasive = false}
   (fn phi => Ring_Tac.Ring_Simps.map (Ring_Tac.insert_rules Ring_Tac.eq_ring_simps
     (Morphism.term phi \<^term>\<open>R\<close>,
      (Morphism.fact phi @{thms Ipol.simps [meta] Ipol_Pc [meta]},
       Morphism.fact phi @{thms Ipolex.simps [meta] Ipolex_Const [meta]},
       Morphism.fact phi @{thms Ipolex_polex_list.simps [meta]},
       Morphism.fact phi @{thms in_carrier_Nil in_carrier_Cons},
       singleton (Morphism.fact phi) @{thm head.simps(2) [meta]},
       singleton (Morphism.fact phi) @{thm norm_subst_correct [meta]}))))
 \<close>
 
 end
 
 method_setup ring = \<open>
   Scan.lift (Args.mode "prems") -- Attrib.thms >> (SIMPLE_METHOD' oo uncurry Ring_Tac.ring_tac)
 \<close> "simplify equations involving rings"
 
 end
diff --git a/src/HOL/Decision_Procs/Reflective_Field.thy b/src/HOL/Decision_Procs/Reflective_Field.thy
--- a/src/HOL/Decision_Procs/Reflective_Field.thy
+++ b/src/HOL/Decision_Procs/Reflective_Field.thy
@@ -1,930 +1,930 @@
 (*  Title:      HOL/Decision_Procs/Reflective_Field.thy
     Author:     Stefan Berghofer
 
 Reducing equalities in fields to equalities in rings.
 *)
 
 theory Reflective_Field
   imports Commutative_Ring
 begin
 
 datatype fexpr =
     FCnst int
   | FVar nat
   | FAdd fexpr fexpr
   | FSub fexpr fexpr
   | FMul fexpr fexpr
   | FNeg fexpr
   | FDiv fexpr fexpr
   | FPow fexpr nat
 
 fun (in field) nth_el :: "'a list \<Rightarrow> nat \<Rightarrow> 'a"
   where
     "nth_el [] n = \<zero>"
   | "nth_el (x # xs) 0 = x"
   | "nth_el (x # xs) (Suc n) = nth_el xs n"
 
 lemma (in field) nth_el_Cons: "nth_el (x # xs) n = (if n = 0 then x else nth_el xs (n - 1))"
   by (cases n) simp_all
 
 lemma (in field) nth_el_closed [simp]: "in_carrier xs \<Longrightarrow> nth_el xs n \<in> carrier R"
   by (induct xs n rule: nth_el.induct) (simp_all add: in_carrier_def)
 
 primrec (in field) feval :: "'a list \<Rightarrow> fexpr \<Rightarrow> 'a"
   where
     "feval xs (FCnst c) = \<guillemotleft>c\<guillemotright>"
   | "feval xs (FVar n) = nth_el xs n"
   | "feval xs (FAdd a b) = feval xs a \<oplus> feval xs b"
   | "feval xs (FSub a b) = feval xs a \<ominus> feval xs b"
   | "feval xs (FMul a b) = feval xs a \<otimes> feval xs b"
   | "feval xs (FNeg a) = \<ominus> feval xs a"
   | "feval xs (FDiv a b) = feval xs a \<oslash> feval xs b"
   | "feval xs (FPow a n) = feval xs a [^] n"
 
 lemma (in field) feval_Cnst:
   "feval xs (FCnst 0) = \<zero>"
   "feval xs (FCnst 1) = \<one>"
   "feval xs (FCnst (numeral n)) = \<guillemotleft>numeral n\<guillemotright>"
   by simp_all
 
 datatype pexpr =
     PExpr1 pexpr1
   | PExpr2 pexpr2
 and pexpr1 =
     PCnst int
   | PVar nat
   | PAdd pexpr pexpr
   | PSub pexpr pexpr
   | PNeg pexpr
 and pexpr2 =
     PMul pexpr pexpr
   | PPow pexpr nat
 
 lemma pexpr_cases [case_names PCnst PVar PAdd PSub PNeg PMul PPow]:
   assumes
     "\<And>c. e = PExpr1 (PCnst c) \<Longrightarrow> P"
     "\<And>n. e = PExpr1 (PVar n) \<Longrightarrow> P"
     "\<And>e1 e2. e = PExpr1 (PAdd e1 e2) \<Longrightarrow> P"
     "\<And>e1 e2. e = PExpr1 (PSub e1 e2) \<Longrightarrow> P"
     "\<And>e'. e = PExpr1 (PNeg e') \<Longrightarrow> P"
     "\<And>e1 e2. e = PExpr2 (PMul e1 e2) \<Longrightarrow> P"
     "\<And>e' n. e = PExpr2 (PPow e' n) \<Longrightarrow> P"
   shows P
 proof (cases e)
   case (PExpr1 e')
   then show ?thesis
     apply (cases e')
         apply simp_all
         apply (erule assms)+
     done
 next
   case (PExpr2 e')
   then show ?thesis
     apply (cases e')
      apply simp_all
      apply (erule assms)+
     done
 qed
 
 lemmas pexpr_cases2 = pexpr_cases [case_product pexpr_cases]
 
 fun (in field) peval :: "'a list \<Rightarrow> pexpr \<Rightarrow> 'a"
   where
     "peval xs (PExpr1 (PCnst c)) = \<guillemotleft>c\<guillemotright>"
   | "peval xs (PExpr1 (PVar n)) = nth_el xs n"
   | "peval xs (PExpr1 (PAdd a b)) = peval xs a \<oplus> peval xs b"
   | "peval xs (PExpr1 (PSub a b)) = peval xs a \<ominus> peval xs b"
   | "peval xs (PExpr1 (PNeg a)) = \<ominus> peval xs a"
   | "peval xs (PExpr2 (PMul a b)) = peval xs a \<otimes> peval xs b"
   | "peval xs (PExpr2 (PPow a n)) = peval xs a [^] n"
 
 lemma (in field) peval_Cnst:
   "peval xs (PExpr1 (PCnst 0)) = \<zero>"
   "peval xs (PExpr1 (PCnst 1)) = \<one>"
   "peval xs (PExpr1 (PCnst (numeral n))) = \<guillemotleft>numeral n\<guillemotright>"
   "peval xs (PExpr1 (PCnst (- numeral n))) = \<ominus> \<guillemotleft>numeral n\<guillemotright>"
   by simp_all
 
 lemma (in field) peval_closed [simp]:
   "in_carrier xs \<Longrightarrow> peval xs e \<in> carrier R"
   "in_carrier xs \<Longrightarrow> peval xs (PExpr1 e1) \<in> carrier R"
   "in_carrier xs \<Longrightarrow> peval xs (PExpr2 e2) \<in> carrier R"
   by (induct e and e1 and e2) simp_all
 
 definition npepow :: "pexpr \<Rightarrow> nat \<Rightarrow> pexpr"
   where "npepow e n =
    (if n = 0 then PExpr1 (PCnst 1)
     else if n = 1 then e
     else
       (case e of
         PExpr1 (PCnst c) \<Rightarrow> PExpr1 (PCnst (c ^ n))
       | _ \<Rightarrow> PExpr2 (PPow e n)))"
 
 lemma (in field) npepow_correct:
   "in_carrier xs \<Longrightarrow> peval xs (npepow e n) = peval xs (PExpr2 (PPow e n))"
   by (cases e rule: pexpr_cases) (simp_all add: npepow_def)
 
 fun npemul :: "pexpr \<Rightarrow> pexpr \<Rightarrow> pexpr"
   where "npemul x y =
     (case x of
       PExpr1 (PCnst c) \<Rightarrow>
         if c = 0 then x
         else if c = 1 then y else
           (case y of
             PExpr1 (PCnst d) \<Rightarrow> PExpr1 (PCnst (c * d))
           | _ \<Rightarrow> PExpr2 (PMul x y))
     | PExpr2 (PPow e1 n) \<Rightarrow>
         (case y of
           PExpr2 (PPow e2 m) \<Rightarrow>
             if n = m then npepow (npemul e1 e2) n
             else PExpr2 (PMul x y)
         | PExpr1 (PCnst d) \<Rightarrow>
             if d = 0 then y
             else if d = 1 then x
             else PExpr2 (PMul x y)
         | _ \<Rightarrow> PExpr2 (PMul x y))
     | _ \<Rightarrow>
       (case y of
         PExpr1 (PCnst d) \<Rightarrow>
           if d = 0 then y
           else if d = 1 then x
           else PExpr2 (PMul x y)
       | _ \<Rightarrow> PExpr2 (PMul x y)))"
 
 lemma (in field) npemul_correct:
   "in_carrier xs \<Longrightarrow> peval xs (npemul e1 e2) = peval xs (PExpr2 (PMul e1 e2))"
 proof (induct e1 e2 rule: npemul.induct)
   case (1 x y)
   then show ?case
   proof (cases x y rule: pexpr_cases2)
     case (PPow_PPow e n e' m)
     then show ?thesis
       by (simp del: npemul.simps add: 1 npepow_correct nat_pow_distrib
           npemul.simps [of "PExpr2 (PPow e n)" "PExpr2 (PPow e' m)"])
   qed simp_all
 qed
 
 declare npemul.simps [simp del]
 
 definition npeadd :: "pexpr \<Rightarrow> pexpr \<Rightarrow> pexpr"
   where "npeadd x y =
     (case x of
       PExpr1 (PCnst c) \<Rightarrow>
         if c = 0 then y
         else
           (case y of
             PExpr1 (PCnst d) \<Rightarrow> PExpr1 (PCnst (c + d))
           | _ \<Rightarrow> PExpr1 (PAdd x y))
     | _ \<Rightarrow>
       (case y of
         PExpr1 (PCnst d) \<Rightarrow>
           if d = 0 then x
           else PExpr1 (PAdd x y)
       | _ \<Rightarrow> PExpr1 (PAdd x y)))"
 
 lemma (in field) npeadd_correct:
   "in_carrier xs \<Longrightarrow> peval xs (npeadd e1 e2) = peval xs (PExpr1 (PAdd e1 e2))"
   by (cases e1 e2 rule: pexpr_cases2) (simp_all add: npeadd_def)
 
 definition npesub :: "pexpr \<Rightarrow> pexpr \<Rightarrow> pexpr"
   where "npesub x y =
     (case y of
       PExpr1 (PCnst d) \<Rightarrow>
         if d = 0 then x
         else
           (case x of
             PExpr1 (PCnst c) \<Rightarrow> PExpr1 (PCnst (c - d))
           | _ \<Rightarrow> PExpr1 (PSub x y))
     | _ \<Rightarrow>
       (case x of
         PExpr1 (PCnst c) \<Rightarrow>
           if c = 0 then PExpr1 (PNeg y)
           else PExpr1 (PSub x y)
       | _ \<Rightarrow> PExpr1 (PSub x y)))"
 
 lemma (in field) npesub_correct:
   "in_carrier xs \<Longrightarrow> peval xs (npesub e1 e2) = peval xs (PExpr1 (PSub e1 e2))"
   by (cases e1 e2 rule: pexpr_cases2) (simp_all add: npesub_def)
 
 definition npeneg :: "pexpr \<Rightarrow> pexpr"
   where "npeneg e =
     (case e of
       PExpr1 (PCnst c) \<Rightarrow> PExpr1 (PCnst (- c))
     | _ \<Rightarrow> PExpr1 (PNeg e))"
 
 lemma (in field) npeneg_correct: "peval xs (npeneg e) = peval xs (PExpr1 (PNeg e))"
   by (cases e rule: pexpr_cases) (simp_all add: npeneg_def)
 
 lemma option_pair_cases [case_names None Some]:
   obtains (None) "x = None" | (Some) p q where "x = Some (p, q)"
 proof (cases x)
   case None
   then show ?thesis by (rule that)
 next
   case (Some r)
   then show ?thesis
     by (cases r, simp) (rule that)
 qed
 
 fun isin :: "pexpr \<Rightarrow> nat \<Rightarrow> pexpr \<Rightarrow> nat \<Rightarrow> (nat \<times> pexpr) option"
   where
     "isin e n (PExpr2 (PMul e1 e2)) m =
       (case isin e n e1 m of
         Some (k, e3) \<Rightarrow>
           if k = 0 then Some (0, npemul e3 (npepow e2 m))
           else
             (case isin e k e2 m of
               Some (l, e4) \<Rightarrow> Some (l, npemul e3 e4)
             | None \<Rightarrow> Some (k, npemul e3 (npepow e2 m)))
       | None \<Rightarrow>
           (case isin e n e2 m of
             Some (k, e3) \<Rightarrow> Some (k, npemul (npepow e1 m) e3)
           | None \<Rightarrow> None))"
   | "isin e n (PExpr2 (PPow e' k)) m =
       (if k = 0 then None else isin e n e' (k * m))"
   | "isin (PExpr1 e) n (PExpr1 e') m =
       (if e = e' then
         if n \<ge> m then Some (n - m, PExpr1 (PCnst 1))
         else Some (0, npepow (PExpr1 e) (m - n))
        else None)"
   | "isin (PExpr2 e) n (PExpr1 e') m = None"
 
 lemma (in field) isin_correct:
   assumes "in_carrier xs"
     and "isin e n e' m = Some (p, e'')"
   shows "peval xs (PExpr2 (PPow e' m)) = peval xs (PExpr2 (PMul (PExpr2 (PPow e (n - p))) e''))"
     and "p \<le> n"
   using assms
   by (induct e n e' m arbitrary: p e'' rule: isin.induct)
     (force
        simp add:
          nat_pow_distrib nat_pow_pow nat_pow_mult m_ac
          npemul_correct npepow_correct
        split: option.split_asm prod.split_asm if_split_asm)+
 
 lemma (in field) isin_correct':
   "in_carrier xs \<Longrightarrow> isin e n e' 1 = Some (p, e'') \<Longrightarrow>
     peval xs e' = peval xs e [^] (n - p) \<otimes> peval xs e''"
   "in_carrier xs \<Longrightarrow> isin e n e' 1 = Some (p, e'') \<Longrightarrow> p \<le> n"
   using isin_correct [where m = 1] by simp_all
 
 fun split_aux :: "pexpr \<Rightarrow> nat \<Rightarrow> pexpr \<Rightarrow> pexpr \<times> pexpr \<times> pexpr"
   where
     "split_aux (PExpr2 (PMul e1 e2)) n e =
        (let
           (left1, common1, right1) = split_aux e1 n e;
           (left2, common2, right2) = split_aux e2 n right1
         in (npemul left1 left2, npemul common1 common2, right2))"
   | "split_aux (PExpr2 (PPow e' m)) n e =
        (if m = 0 then (PExpr1 (PCnst 1), PExpr1 (PCnst 1), e)
         else split_aux e' (m * n) e)"
   | "split_aux (PExpr1 e') n e =
        (case isin (PExpr1 e') n e 1 of
           Some (m, e'') \<Rightarrow>
             (if m = 0 then (PExpr1 (PCnst 1), npepow (PExpr1 e') n, e'')
              else (npepow (PExpr1 e') m, npepow (PExpr1 e') (n - m), e''))
         | None \<Rightarrow> (npepow (PExpr1 e') n, PExpr1 (PCnst 1), e))"
 
 hide_const Left Right  (* FIXME !? *)
 
 abbreviation Left :: "pexpr \<Rightarrow> pexpr \<Rightarrow> pexpr"
   where "Left e1 e2 \<equiv> fst (split_aux e1 (Suc 0) e2)"
 
 abbreviation Common :: "pexpr \<Rightarrow> pexpr \<Rightarrow> pexpr"
   where "Common e1 e2 \<equiv> fst (snd (split_aux e1 (Suc 0) e2))"
 
 abbreviation Right :: "pexpr \<Rightarrow> pexpr \<Rightarrow> pexpr"
   where "Right e1 e2 \<equiv> snd (snd (split_aux e1 (Suc 0) e2))"
 
 lemma split_aux_induct [case_names 1 2 3]:
   assumes I1: "\<And>e1 e2 n e. P e1 n e \<Longrightarrow> P e2 n (snd (snd (split_aux e1 n e))) \<Longrightarrow>
     P (PExpr2 (PMul e1 e2)) n e"
   and I2: "\<And>e' m n e. (m \<noteq> 0 \<Longrightarrow> P e' (m * n) e) \<Longrightarrow> P (PExpr2 (PPow e' m)) n e"
   and I3: "\<And>e' n e. P (PExpr1 e') n e"
   shows "P x y z"
 proof (induct x y z rule: split_aux.induct)
   case 1
   from 1(1) 1(2) [OF refl prod.collapse prod.collapse]
   show ?case by (rule I1)
 next
   case 2
   then show ?case by (rule I2)
 next
   case 3
   then show ?case by (rule I3)
 qed
 
 lemma (in field) split_aux_correct:
   "in_carrier xs \<Longrightarrow>
     peval xs (PExpr2 (PPow e\<^sub>1 n)) =
     peval xs (PExpr2 (PMul (fst (split_aux e\<^sub>1 n e\<^sub>2)) (fst (snd (split_aux e\<^sub>1 n e\<^sub>2)))))"
   "in_carrier xs \<Longrightarrow>
     peval xs e\<^sub>2 =
     peval xs (PExpr2 (PMul (snd (snd (split_aux e\<^sub>1 n e\<^sub>2))) (fst (snd (split_aux e\<^sub>1 n e\<^sub>2)))))"
   by (induct e\<^sub>1 n e\<^sub>2 rule: split_aux_induct)
     (auto simp add: split_beta
        nat_pow_distrib nat_pow_pow nat_pow_mult m_ac
        npemul_correct npepow_correct isin_correct'
        split: option.split)
 
 lemma (in field) split_aux_correct':
   "in_carrier xs \<Longrightarrow>
     peval xs e\<^sub>1 = peval xs (Left e\<^sub>1 e\<^sub>2) \<otimes> peval xs (Common e\<^sub>1 e\<^sub>2)"
   "in_carrier xs \<Longrightarrow>
     peval xs e\<^sub>2 = peval xs (Right e\<^sub>1 e\<^sub>2) \<otimes> peval xs (Common e\<^sub>1 e\<^sub>2)"
   using split_aux_correct [where n = 1] by simp_all
 
 fun fnorm :: "fexpr \<Rightarrow> pexpr \<times> pexpr \<times> pexpr list"
   where
     "fnorm (FCnst c) = (PExpr1 (PCnst c), PExpr1 (PCnst 1), [])"
   | "fnorm (FVar n) = (PExpr1 (PVar n), PExpr1 (PCnst 1), [])"
   | "fnorm (FAdd e1 e2) =
        (let
           (xn, xd, xc) = fnorm e1;
           (yn, yd, yc) = fnorm e2;
           (left, common, right) = split_aux xd 1 yd
         in
           (npeadd (npemul xn right) (npemul yn left),
            npemul left (npemul right common),
            List.union xc yc))"
   | "fnorm (FSub e1 e2) =
        (let
           (xn, xd, xc) = fnorm e1;
           (yn, yd, yc) = fnorm e2;
           (left, common, right) = split_aux xd 1 yd
         in
           (npesub (npemul xn right) (npemul yn left),
            npemul left (npemul right common),
            List.union xc yc))"
   | "fnorm (FMul e1 e2) =
        (let
           (xn, xd, xc) = fnorm e1;
           (yn, yd, yc) = fnorm e2;
           (left1, common1, right1) = split_aux xn 1 yd;
           (left2, common2, right2) = split_aux yn 1 xd
         in
           (npemul left1 left2,
            npemul right2 right1,
            List.union xc yc))"
   | "fnorm (FNeg e) =
        (let (n, d, c) = fnorm e
         in (npeneg n, d, c))"
   | "fnorm (FDiv e1 e2) =
        (let
           (xn, xd, xc) = fnorm e1;
           (yn, yd, yc) = fnorm e2;
           (left1, common1, right1) = split_aux xn 1 yn;
           (left2, common2, right2) = split_aux xd 1 yd
         in
           (npemul left1 right2,
            npemul left2 right1,
            List.insert yn (List.union xc yc)))"
   | "fnorm (FPow e m) =
        (let (n, d, c) = fnorm e
         in (npepow n m, npepow d m, c))"
 
 abbreviation Num :: "fexpr \<Rightarrow> pexpr"
   where "Num e \<equiv> fst (fnorm e)"
 
 abbreviation Denom :: "fexpr \<Rightarrow> pexpr"
   where "Denom e \<equiv> fst (snd (fnorm e))"
 
 abbreviation Cond :: "fexpr \<Rightarrow> pexpr list"
   where "Cond e \<equiv> snd (snd (fnorm e))"
 
 primrec (in field) nonzero :: "'a list \<Rightarrow> pexpr list \<Rightarrow> bool"
   where
     "nonzero xs [] \<longleftrightarrow> True"
   | "nonzero xs (p # ps) \<longleftrightarrow> peval xs p \<noteq> \<zero> \<and> nonzero xs ps"
 
 lemma (in field) nonzero_singleton: "nonzero xs [p] = (peval xs p \<noteq> \<zero>)"
   by simp
 
 lemma (in field) nonzero_append: "nonzero xs (ps @ qs) = (nonzero xs ps \<and> nonzero xs qs)"
   by (induct ps) simp_all
 
 lemma (in field) nonzero_idempotent:
   "p \<in> set ps \<Longrightarrow> (peval xs p \<noteq> \<zero> \<and> nonzero xs ps) = nonzero xs ps"
   by (induct ps) auto
 
 lemma (in field) nonzero_insert:
   "nonzero xs (List.insert p ps) = (peval xs p \<noteq> \<zero> \<and> nonzero xs ps)"
   by (simp add: List.insert_def nonzero_idempotent)
 
 lemma (in field) nonzero_union:
   "nonzero xs (List.union ps qs) = (nonzero xs ps \<and> nonzero xs qs)"
   by (induct ps rule: rev_induct)
     (auto simp add: List.union_def nonzero_insert nonzero_append)
 
 lemma (in field) fnorm_correct:
   assumes "in_carrier xs"
     and "nonzero xs (Cond e)"
   shows "feval xs e = peval xs (Num e) \<oslash> peval xs (Denom e)"
     and "peval xs (Denom e) \<noteq> \<zero>"
   using assms
 proof (induct e)
   case (FCnst c)
   {
     case 1
     show ?case by simp
   next
     case 2
     show ?case by simp
   }
 next
   case (FVar n)
   {
     case 1
     then show ?case by simp
   next
     case 2
     show ?case by simp
   }
 next
   case (FAdd e1 e2)
   note split = split_aux_correct' [where xs=xs and e\<^sub>1 = "Denom e1" and e\<^sub>2 = "Denom e2"]
   {
     case 1
     let ?left = "peval xs (Left (Denom e1) (Denom e2))"
     let ?common = "peval xs (Common (Denom e1) (Denom e2))"
     let ?right = "peval xs (Right (Denom e1) (Denom e2))"
     from 1 FAdd have "feval xs (FAdd e1 e2) =
       (?common \<otimes> (peval xs (Num e1) \<otimes> ?right \<oplus> peval xs (Num e2) \<otimes> ?left)) \<oslash>
       (?common \<otimes> (?left \<otimes> (?right \<otimes> ?common)))"
       by (simp add: split_beta split nonzero_union add_frac_eq r_distr m_ac)
     also from 1 FAdd have "\<dots> = peval xs (Num (FAdd e1 e2)) \<oslash> peval xs (Denom (FAdd e1 e2))"
       by (simp add: split_beta split nonzero_union npeadd_correct npemul_correct integral_iff)
     finally show ?case .
   next
     case 2
     with FAdd show ?case
       by (simp add: split_beta split nonzero_union npemul_correct integral_iff)
   }
 next
   case (FSub e1 e2)
   note split = split_aux_correct' [where xs=xs and e\<^sub>1 = "Denom e1" and e\<^sub>2 = "Denom e2"]
   {
     case 1
     let ?left = "peval xs (Left (Denom e1) (Denom e2))"
     let ?common = "peval xs (Common (Denom e1) (Denom e2))"
     let ?right = "peval xs (Right (Denom e1) (Denom e2))"
     from 1 FSub
     have "feval xs (FSub e1 e2) =
       (?common \<otimes> (peval xs (Num e1) \<otimes> ?right \<ominus> peval xs (Num e2) \<otimes> ?left)) \<oslash>
       (?common \<otimes> (?left \<otimes> (?right \<otimes> ?common)))"
       by (simp add: split_beta split nonzero_union diff_frac_eq r_diff_distr m_ac)
     also from 1 FSub have "\<dots> = peval xs (Num (FSub e1 e2)) \<oslash> peval xs (Denom (FSub e1 e2))"
       by (simp add: split_beta split nonzero_union npesub_correct npemul_correct integral_iff)
     finally show ?case .
   next
     case 2
     with FSub show ?case
       by (simp add: split_beta split nonzero_union npemul_correct integral_iff)
   }
 next
   case (FMul e1 e2)
   note split =
     split_aux_correct' [where xs=xs and e\<^sub>1 = "Num e1" and e\<^sub>2 = "Denom e2"]
     split_aux_correct' [where xs=xs and e\<^sub>1 = "Num e2" and e\<^sub>2 = "Denom e1"]
   {
     case 1
     let ?left\<^sub>1 = "peval xs (Left (Num e1) (Denom e2))"
     let ?common\<^sub>1 = "peval xs (Common (Num e1) (Denom e2))"
     let ?right\<^sub>1 = "peval xs (Right (Num e1) (Denom e2))"
     let ?left\<^sub>2 = "peval xs (Left (Num e2) (Denom e1))"
     let ?common\<^sub>2 = "peval xs (Common (Num e2) (Denom e1))"
     let ?right\<^sub>2 = "peval xs (Right (Num e2) (Denom e1))"
     from 1 FMul have "feval xs (FMul e1 e2) =
       ((?common\<^sub>1 \<otimes> ?common\<^sub>2) \<otimes> (?left\<^sub>1 \<otimes> ?left\<^sub>2)) \<oslash>
       ((?common\<^sub>1 \<otimes> ?common\<^sub>2) \<otimes> (?right\<^sub>2 \<otimes> ?right\<^sub>1))"
       by (simp add: split_beta split nonzero_union
         nonzero_divide_divide_eq_left m_ac)
     also from 1 FMul have "\<dots> = peval xs (Num (FMul e1 e2)) \<oslash> peval xs (Denom (FMul e1 e2))"
       by (simp add: split_beta split nonzero_union npemul_correct integral_iff)
     finally show ?case .
   next
     case 2
     with FMul show ?case
       by (simp add: split_beta split nonzero_union npemul_correct integral_iff)
   }
 next
   case (FNeg e)
   {
     case 1
     with FNeg show ?case
       by (simp add: split_beta npeneg_correct)
   next
     case 2
     with FNeg show ?case
       by (simp add: split_beta)
   }
 next
   case (FDiv e1 e2)
   note split =
     split_aux_correct' [where xs=xs and e\<^sub>1 = "Num e1" and e\<^sub>2 = "Num e2"]
     split_aux_correct' [where xs=xs and e\<^sub>1 = "Denom e1" and e\<^sub>2 = "Denom e2"]
   {
     case 1
     let ?left\<^sub>1 = "peval xs (Left (Num e1) (Num e2))"
     let ?common\<^sub>1 = "peval xs (Common (Num e1) (Num e2))"
     let ?right\<^sub>1 = "peval xs (Right (Num e1) (Num e2))"
     let ?left\<^sub>2 = "peval xs (Left (Denom e1) (Denom e2))"
     let ?common\<^sub>2 = "peval xs (Common (Denom e1) (Denom e2))"
     let ?right\<^sub>2 = "peval xs (Right (Denom e1) (Denom e2))"
     from 1 FDiv
     have "feval xs (FDiv e1 e2) =
       ((?common\<^sub>1 \<otimes> ?common\<^sub>2) \<otimes> (?left\<^sub>1 \<otimes> ?right\<^sub>2)) \<oslash>
       ((?common\<^sub>1 \<otimes> ?common\<^sub>2) \<otimes> (?left\<^sub>2 \<otimes> ?right\<^sub>1))"
       by (simp add: split_beta split nonzero_union nonzero_insert
         nonzero_divide_divide_eq m_ac)
     also from 1 FDiv have "\<dots> = peval xs (Num (FDiv e1 e2)) \<oslash> peval xs (Denom (FDiv e1 e2))"
       by (simp add: split_beta split nonzero_union nonzero_insert npemul_correct integral_iff)
     finally show ?case .
   next
     case 2
     with FDiv show ?case
       by (simp add: split_beta split nonzero_union nonzero_insert npemul_correct integral_iff)
   }
 next
   case (FPow e n)
   {
     case 1
     with FPow show ?case
       by (simp add: split_beta nonzero_power_divide npepow_correct)
   next
     case 2
     with FPow show ?case
       by (simp add: split_beta npepow_correct)
   }
 qed
 
 lemma (in field) feval_eq0:
   assumes "in_carrier xs"
     and "fnorm e = (n, d, c)"
     and "nonzero xs c"
     and "peval xs n = \<zero>"
   shows "feval xs e = \<zero>"
   using assms fnorm_correct [of xs e] by simp
 
 lemma (in field) fexpr_in_carrier:
   assumes "in_carrier xs"
     and "nonzero xs (Cond e)"
   shows "feval xs e \<in> carrier R"
   using assms
 proof (induct e)
   case (FDiv e1 e2)
   then have "feval xs e1 \<in> carrier R" "feval xs e2 \<in> carrier R"
     "peval xs (Num e2) \<noteq> \<zero>" "nonzero xs (Cond e2)"
     by (simp_all add: nonzero_union nonzero_insert split: prod.split_asm)
   from \<open>in_carrier xs\<close> \<open>nonzero xs (Cond e2)\<close>
   have "feval xs e2 = peval xs (Num e2) \<oslash> peval xs (Denom e2)"
     by (rule fnorm_correct)
   moreover from \<open>in_carrier xs\<close> \<open>nonzero xs (Cond e2)\<close>
   have "peval xs (Denom e2) \<noteq> \<zero>" by (rule fnorm_correct)
   ultimately have "feval xs e2 \<noteq> \<zero>" using \<open>peval xs (Num e2) \<noteq> \<zero>\<close> \<open>in_carrier xs\<close>
     by (simp add: divide_eq_0_iff)
   with \<open>feval xs e1 \<in> carrier R\<close> \<open>feval xs e2 \<in> carrier R\<close>
   show ?case by simp
 qed (simp_all add: nonzero_union split: prod.split_asm)
 
 lemma (in field) feval_eq:
   assumes "in_carrier xs"
     and "fnorm (FSub e e') = (n, d, c)"
     and "nonzero xs c"
   shows "(feval xs e = feval xs e') = (peval xs n = \<zero>)"
 proof -
   from assms have "nonzero xs (Cond e)" "nonzero xs (Cond e')"
     by (auto simp add: nonzero_union split: prod.split_asm)
   with assms fnorm_correct [of xs "FSub e e'"]
   have "feval xs e \<ominus> feval xs e' = peval xs n \<oslash> peval xs d"
     "peval xs d \<noteq> \<zero>"
     by simp_all
   show ?thesis
   proof
     assume "feval xs e = feval xs e'"
     with \<open>feval xs e \<ominus> feval xs e' = peval xs n \<oslash> peval xs d\<close>
       \<open>in_carrier xs\<close> \<open>nonzero xs (Cond e')\<close>
     have "peval xs n \<oslash> peval xs d = \<zero>"
       by (simp add: fexpr_in_carrier minus_eq r_neg)
     with \<open>peval xs d \<noteq> \<zero>\<close> \<open>in_carrier xs\<close>
     show "peval xs n = \<zero>"
       by (simp add: divide_eq_0_iff)
   next
     assume "peval xs n = \<zero>"
     with \<open>feval xs e \<ominus> feval xs e' = peval xs n \<oslash> peval xs d\<close> \<open>peval xs d \<noteq> \<zero>\<close>
       \<open>nonzero xs (Cond e)\<close> \<open>nonzero xs (Cond e')\<close> \<open>in_carrier xs\<close>
     show "feval xs e = feval xs e'"
       by (simp add: eq_diff0 fexpr_in_carrier)
   qed
 qed
 
 ML \<open>
 val term_of_nat = HOLogic.mk_number \<^Type>\<open>nat\<close> o @{code integer_of_nat};
 
 val term_of_int = HOLogic.mk_number \<^Type>\<open>int\<close> o @{code integer_of_int};
 
 fun term_of_pexpr (@{code PExpr1} x) = \<^Const>\<open>PExpr1\<close> $ term_of_pexpr1 x
   | term_of_pexpr (@{code PExpr2} x) = \<^Const>\<open>PExpr2\<close> $ term_of_pexpr2 x
 and term_of_pexpr1 (@{code PCnst} k) = \<^Const>\<open>PCnst\<close> $ term_of_int k
   | term_of_pexpr1 (@{code PVar} n) = \<^Const>\<open>PVar\<close> $ term_of_nat n
   | term_of_pexpr1 (@{code PAdd} (x, y)) = \<^Const>\<open>PAdd\<close> $ term_of_pexpr x $ term_of_pexpr y
   | term_of_pexpr1 (@{code PSub} (x, y)) = \<^Const>\<open>PSub\<close> $ term_of_pexpr x $ term_of_pexpr y
   | term_of_pexpr1 (@{code PNeg} x) = \<^Const>\<open>PNeg\<close> $ term_of_pexpr x
 and term_of_pexpr2 (@{code PMul} (x, y)) = \<^Const>\<open>PMul\<close> $ term_of_pexpr x $ term_of_pexpr y
   | term_of_pexpr2 (@{code PPow} (x, n)) = \<^Const>\<open>PPow\<close> $ term_of_pexpr x $ term_of_nat n
 
 fun term_of_result (x, (y, zs)) =
   HOLogic.mk_prod (term_of_pexpr x, HOLogic.mk_prod
     (term_of_pexpr y, HOLogic.mk_list \<^Type>\<open>pexpr\<close> (map term_of_pexpr zs)));
 
 local
 
-fun fnorm (ctxt, ct, t) = Thm.mk_binop \<^cterm>\<open>Pure.eq :: pexpr \<times> pexpr \<times> pexpr list \<Rightarrow> pexpr \<times> pexpr \<times> pexpr list \<Rightarrow> prop\<close>
-  ct (Thm.cterm_of ctxt t);
+fun fnorm (ctxt, ct, t) =
+  \<^let>\<open>x = ct and y = \<open>Thm.cterm_of ctxt t\<close>
+    in cterm \<open>x \<equiv> y\<close> for x y :: \<open>pexpr \<times> pexpr \<times> pexpr list\<close>\<close>;
 
 val (_, raw_fnorm_oracle) = Context.>>> (Context.map_theory_result
   (Thm.add_oracle (\<^binding>\<open>fnorm\<close>, fnorm)));
 
 fun fnorm_oracle ctxt ct t = raw_fnorm_oracle (ctxt, ct, t);
 
 in
 
 val cv = @{computation_conv "pexpr \<times> pexpr \<times> pexpr list"
   terms: fnorm nat_of_integer Code_Target_Nat.natural
     "0::nat" "1::nat" "2::nat" "3::nat"
     "0::int" "1::int" "2::int" "3::int" "-1::int"
   datatypes: fexpr int integer num}
   (fn ctxt => fn result => fn ct => fnorm_oracle ctxt ct (term_of_result result))
 
 end
 \<close>
 
 ML \<open>
 signature FIELD_TAC =
 sig
   structure Field_Simps:
   sig
     type T
     val get: Context.generic -> T
     val put: T -> Context.generic -> Context.generic
     val map: (T -> T) -> Context.generic -> Context.generic
   end
   val eq_field_simps:
     (term * (thm list * thm list * thm list * thm * thm)) *
     (term * (thm list * thm list * thm list * thm * thm)) -> bool
   val field_tac: bool -> Proof.context -> int -> tactic
 end
 
 structure Field_Tac : FIELD_TAC =
 struct
 
 open Ring_Tac;
 
 fun field_struct \<^Const_>\<open>Ring.ring.add _ _ for R _ _\<close> = SOME R
   | field_struct \<^Const_>\<open>Ring.a_minus _ _ for R _ _\<close> = SOME R
   | field_struct \<^Const_>\<open>Group.monoid.mult _ _ for R _ _\<close> = SOME R
   | field_struct \<^Const_>\<open>Ring.a_inv _ _ for R _\<close> = SOME R
   | field_struct \<^Const_>\<open>Group.pow _ _ _ for R _ _\<close> = SOME R
   | field_struct \<^Const_>\<open>Algebra_Aux.m_div _ _for R _ _\<close> = SOME R
   | field_struct \<^Const_>\<open>Ring.ring.zero _ _ for R\<close> = SOME R
   | field_struct \<^Const_>\<open>Group.monoid.one _ _ for R\<close> = SOME R
   | field_struct \<^Const_>\<open>Algebra_Aux.of_integer _ _ for R _\<close> = SOME R
   | field_struct _ = NONE;
 
 fun reif_fexpr vs \<^Const_>\<open>Ring.ring.add _ _ for _ a b\<close> =
       \<^Const>\<open>FAdd for \<open>reif_fexpr vs a\<close> \<open>reif_fexpr vs b\<close>\<close>
   | reif_fexpr vs \<^Const_>\<open>Ring.a_minus _ _ for _ a b\<close> =
       \<^Const>\<open>FSub for \<open>reif_fexpr vs a\<close> \<open>reif_fexpr vs b\<close>\<close>
   | reif_fexpr vs \<^Const_>\<open>Group.monoid.mult _ _ for _ a b\<close> =
       \<^Const>\<open>FMul for \<open>reif_fexpr vs a\<close> \<open>reif_fexpr vs b\<close>\<close>
   | reif_fexpr vs \<^Const_>\<open>Ring.a_inv _ _ for _ a\<close> =
       \<^Const>\<open>FNeg for \<open>reif_fexpr vs a\<close>\<close>
   | reif_fexpr vs \<^Const>\<open>Group.pow _ _ _ for _ a n\<close> =
       \<^Const>\<open>FPow for \<open>reif_fexpr vs a\<close> n\<close>
   | reif_fexpr vs \<^Const_>\<open>Algebra_Aux.m_div _ _ for _ a b\<close> =
       \<^Const>\<open>FDiv for \<open>reif_fexpr vs a\<close> \<open>reif_fexpr vs b\<close>\<close>
   | reif_fexpr vs (Free x) =
       \<^Const>\<open>FVar for \<open>HOLogic.mk_number HOLogic.natT (find_index (equal x) vs)\<close>\<close>
   | reif_fexpr vs \<^Const_>\<open>Ring.ring.zero _ _ for _\<close> = \<^term>\<open>FCnst 0\<close>
   | reif_fexpr vs \<^Const_>\<open>Group.monoid.one _ _ for _\<close> = \<^term>\<open>FCnst 1\<close>
   | reif_fexpr vs \<^Const_>\<open>Algebra_Aux.of_integer _ _ for _ n\<close> = \<^Const>\<open>FCnst for n\<close>
   | reif_fexpr _ _ = error "reif_fexpr: bad expression";
 
 fun reif_fexpr' vs \<^Const_>\<open>plus _ for a b\<close> = \<^Const>\<open>FAdd for \<open>reif_fexpr' vs a\<close> \<open>reif_fexpr' vs b\<close>\<close>
   | reif_fexpr' vs \<^Const_>\<open>minus _ for a b\<close> = \<^Const>\<open>FSub for \<open>reif_fexpr' vs a\<close> \<open>reif_fexpr' vs b\<close>\<close>
   | reif_fexpr' vs \<^Const_>\<open>times _ for a b\<close> = \<^Const>\<open>FMul for \<open>reif_fexpr' vs a\<close> \<open>reif_fexpr' vs b\<close>\<close>
   | reif_fexpr' vs \<^Const_>\<open>uminus _ for a\<close> = \<^Const>\<open>FNeg for \<open>reif_fexpr' vs a\<close>\<close>
   | reif_fexpr' vs \<^Const_>\<open>power _ for a n\<close> = \<^Const>\<open>FPow for \<open>reif_fexpr' vs a\<close> n\<close>
   | reif_fexpr' vs \<^Const_>\<open>divide _ for a b\<close> = \<^Const>\<open>FDiv for \<open>reif_fexpr' vs a\<close> \<open>reif_fexpr' vs b\<close>\<close>
   | reif_fexpr' vs (Free x) =
       \<^Const>\<open>FVar for \<open>HOLogic.mk_number HOLogic.natT (find_index (equal x) vs)\<close>\<close>
   | reif_fexpr' vs \<^Const_>\<open>zero_class.zero _\<close> = \<^term>\<open>FCnst 0\<close>
   | reif_fexpr' vs \<^Const_>\<open>one_class.one _\<close> = \<^term>\<open>FCnst 1\<close>
   | reif_fexpr' vs \<^Const_>\<open>numeral _ for b\<close> = \<^Const>\<open>FCnst for \<^Const>\<open>numeral \<^Type>\<open>int\<close> for b\<close>\<close>
   | reif_fexpr' _ _ = error "reif_fexpr: bad expression";
 
 fun eq_field_simps
   ((t, (ths1, ths2, ths3, th4, th)),
    (t', (ths1', ths2', ths3', th4', th'))) =
     t aconv t' andalso
     eq_list Thm.eq_thm (ths1, ths1') andalso
     eq_list Thm.eq_thm (ths2, ths2') andalso
     eq_list Thm.eq_thm (ths3, ths3') andalso
     Thm.eq_thm (th4, th4') andalso
     Thm.eq_thm (th, th');
 
 structure Field_Simps = Generic_Data
 (struct
   type T = (term * (thm list * thm list * thm list * thm * thm)) Net.net
   val empty = Net.empty
   val merge = Net.merge eq_field_simps
 end);
 
 fun get_field_simps ctxt optcT t =
   (case get_matching_rules ctxt (Field_Simps.get (Context.Proof ctxt)) t of
      SOME (ths1, ths2, ths3, th4, th) =>
        let val tr =
          Thm.transfer' ctxt #>
          (case optcT of NONE => I | SOME cT => inst [cT] [] #> norm)
        in (map tr ths1, map tr ths2, map tr ths3, tr th4, tr th) end
    | NONE => error "get_field_simps: lookup failed");
 
 fun nth_el_conv (_, _, _, nth_el_Cons, _) =
   let
     val a = type_of_eqn nth_el_Cons;
     val If_conv_a = If_conv a;
 
     fun conv ys n = (case strip_app ys of
       (\<^const_name>\<open>Cons\<close>, [x, xs]) =>
         transitive'
           (inst [] [x, xs, n] nth_el_Cons)
           (If_conv_a (args2 nat_eq_conv)
              Thm.reflexive
              (cong2' conv Thm.reflexive (args2 nat_minus_conv))))
   in conv end;
 
 fun feval_conv (rls as
       ([feval_simps_1, feval_simps_2, feval_simps_3,
         feval_simps_4, feval_simps_5, feval_simps_6,
         feval_simps_7, feval_simps_8, feval_simps_9,
         feval_simps_10, feval_simps_11],
        _, _, _, _)) =
   let
     val nth_el_conv' = nth_el_conv rls;
 
     fun conv xs x = (case strip_app x of
         (\<^const_name>\<open>FCnst\<close>, [c]) => (case strip_app c of
             (\<^const_name>\<open>zero_class.zero\<close>, _) => inst [] [xs] feval_simps_9
           | (\<^const_name>\<open>one_class.one\<close>, _) => inst [] [xs] feval_simps_10
           | (\<^const_name>\<open>numeral\<close>, [n]) => inst [] [xs, n] feval_simps_11
           | _ => inst [] [xs, c] feval_simps_1)
       | (\<^const_name>\<open>FVar\<close>, [n]) =>
           transitive' (inst [] [xs, n] feval_simps_2) (args2 nth_el_conv')
       | (\<^const_name>\<open>FAdd\<close>, [a, b]) =>
           transitive' (inst [] [xs, a, b] feval_simps_3)
             (cong2 (args2 conv) (args2 conv))
       | (\<^const_name>\<open>FSub\<close>, [a, b]) =>
           transitive' (inst [] [xs, a, b] feval_simps_4)
             (cong2 (args2 conv) (args2 conv))
       | (\<^const_name>\<open>FMul\<close>, [a, b]) =>
           transitive' (inst [] [xs, a, b] feval_simps_5)
             (cong2 (args2 conv) (args2 conv))
       | (\<^const_name>\<open>FNeg\<close>, [a]) =>
           transitive' (inst [] [xs, a] feval_simps_6)
             (cong1 (args2 conv))
       | (\<^const_name>\<open>FDiv\<close>, [a, b]) =>
           transitive' (inst [] [xs, a, b] feval_simps_7)
             (cong2 (args2 conv) (args2 conv))
       | (\<^const_name>\<open>FPow\<close>, [a, n]) =>
           transitive' (inst [] [xs, a, n] feval_simps_8)
             (cong2 (args2 conv) Thm.reflexive))
   in conv end;
 
 fun peval_conv (rls as
       (_,
        [peval_simps_1, peval_simps_2, peval_simps_3,
         peval_simps_4, peval_simps_5, peval_simps_6,
         peval_simps_7, peval_simps_8, peval_simps_9,
         peval_simps_10, peval_simps_11],
        _, _, _)) =
   let
     val nth_el_conv' = nth_el_conv rls;
 
     fun conv xs x = (case strip_app x of
         (\<^const_name>\<open>PExpr1\<close>, [e]) => (case strip_app e of
             (\<^const_name>\<open>PCnst\<close>, [c]) => (case strip_numeral c of
                 (\<^const_name>\<open>zero_class.zero\<close>, _) => inst [] [xs] peval_simps_8
               | (\<^const_name>\<open>one_class.one\<close>, _) => inst [] [xs] peval_simps_9
               | (\<^const_name>\<open>numeral\<close>, [n]) => inst [] [xs, n] peval_simps_10
               | (\<^const_name>\<open>uminus\<close>, [n]) => inst [] [xs, n] peval_simps_11
               | _ => inst [] [xs, c] peval_simps_1)
           | (\<^const_name>\<open>PVar\<close>, [n]) =>
               transitive' (inst [] [xs, n] peval_simps_2) (args2 nth_el_conv')
           | (\<^const_name>\<open>PAdd\<close>, [a, b]) =>
               transitive' (inst [] [xs, a, b] peval_simps_3)
                 (cong2 (args2 conv) (args2 conv))
           | (\<^const_name>\<open>PSub\<close>, [a, b]) =>
               transitive' (inst [] [xs, a, b] peval_simps_4)
                 (cong2 (args2 conv) (args2 conv))
           | (\<^const_name>\<open>PNeg\<close>, [a]) =>
               transitive' (inst [] [xs, a] peval_simps_5)
                 (cong1 (args2 conv)))
       | (\<^const_name>\<open>PExpr2\<close>, [e]) => (case strip_app e of
             (\<^const_name>\<open>PMul\<close>, [a, b]) =>
               transitive' (inst [] [xs, a, b] peval_simps_6)
                 (cong2 (args2 conv) (args2 conv))
           | (\<^const_name>\<open>PPow\<close>, [a, n]) =>
               transitive' (inst [] [xs, a, n] peval_simps_7)
                 (cong2 (args2 conv) Thm.reflexive)))
   in conv end;
 
 fun nonzero_conv (rls as
       (_, _,
        [nonzero_Nil, nonzero_Cons, nonzero_singleton],
        _, _)) =
   let
     val peval_conv' = peval_conv rls;
 
     fun conv xs qs = (case strip_app qs of
         (\<^const_name>\<open>Nil\<close>, []) => inst [] [xs] nonzero_Nil
       | (\<^const_name>\<open>Cons\<close>, [p, ps]) => (case Thm.term_of ps of
             \<^Const_>\<open>Nil _\<close> =>
               transitive' (inst [] [xs, p] nonzero_singleton)
                 (cong1 (cong2 (args2 peval_conv') Thm.reflexive))
           | _ => transitive' (inst [] [xs, p, ps] nonzero_Cons)
               (cong2 (cong1 (cong2 (args2 peval_conv') Thm.reflexive)) (args2 conv))))
   in conv end;
 
 fun field_tac in_prem ctxt =
   SUBGOAL (fn (g, i) =>
     let
       val (prems, concl) = Logic.strip_horn g;
       fun find_eq s = (case s of
           (_ $ \<^Const_>\<open>HOL.eq T for t u\<close>) =>
             (case (field_struct t, field_struct u) of
                (SOME R, _) => SOME ((t, u), R, T, NONE, mk_in_carrier ctxt R [], reif_fexpr)
              | (_, SOME R) => SOME ((t, u), R, T, NONE, mk_in_carrier ctxt R [], reif_fexpr)
              | _ =>
                  if Sign.of_sort (Proof_Context.theory_of ctxt) (T, \<^sort>\<open>field\<close>)
                  then SOME ((t, u), mk_ring T, T, SOME T, K @{thm in_carrier_trivial}, reif_fexpr')
                  else NONE)
         | _ => NONE);
       val ((t, u), R, T, optT, mkic, reif) =
         (case get_first find_eq
            (if in_prem then prems else [concl]) of
            SOME q => q
          | NONE => error "cannot determine field");
       val rls as (_, _, _, _, feval_eq) =
         get_field_simps ctxt (Option.map (Thm.ctyp_of ctxt) optT) R;
       val xs = [] |> Term.add_frees t |> Term.add_frees u |> filter (equal T o snd);
       val cxs = Thm.cterm_of ctxt (HOLogic.mk_list T (map Free xs));
       val ce = Thm.cterm_of ctxt (reif xs t);
       val ce' = Thm.cterm_of ctxt (reif xs u);
-      val fnorm = cv ctxt
-        (Thm.apply \<^cterm>\<open>fnorm\<close> (Thm.apply (Thm.apply \<^cterm>\<open>FSub\<close> ce) ce'));
+      val fnorm = cv ctxt \<^let>\<open>e = ce and e' = ce' in cterm \<open>fnorm (FSub e e')\<close>\<close>;
       val (_, [n, dc]) = strip_app (Thm.rhs_of fnorm);
       val (_, [_, c]) = strip_app dc;
       val th =
         Conv.fconv_rule (Conv.concl_conv 1 (Conv.arg_conv
           (binop_conv
              (binop_conv
                 (K (feval_conv rls cxs ce)) (K (feval_conv rls cxs ce')))
              (Conv.arg1_conv (K (peval_conv rls cxs n))))))
         ([mkic xs,
           HOLogic.mk_obj_eq fnorm,
           HOLogic.mk_obj_eq (nonzero_conv rls cxs c) RS @{thm iffD2}] MRS
          feval_eq);
       val th' = Drule.rotate_prems 1
         (th RS (if in_prem then @{thm iffD1} else @{thm iffD2}));
     in
       if in_prem then
         dresolve_tac ctxt [th'] 1 THEN defer_tac 1
       else
         resolve_tac ctxt [th'] 1
     end);
 
 end
 \<close>
 
 context field
 begin
 
 local_setup \<open>
 Local_Theory.declaration {syntax = false, pervasive = false}
   (fn phi => Field_Tac.Field_Simps.map (Ring_Tac.insert_rules Field_Tac.eq_field_simps
     (Morphism.term phi \<^term>\<open>R\<close>,
      (Morphism.fact phi @{thms feval.simps [meta] feval_Cnst [meta]},
       Morphism.fact phi @{thms peval.simps [meta] peval_Cnst [meta]},
       Morphism.fact phi @{thms nonzero.simps [meta] nonzero_singleton [meta]},
       singleton (Morphism.fact phi) @{thm nth_el_Cons [meta]},
       singleton (Morphism.fact phi) @{thm feval_eq}))))
 \<close>
 
 end
 
 method_setup field = \<open>
   Scan.lift (Args.mode "prems") -- Attrib.thms >> (fn (in_prem, thms) => fn ctxt =>
     SIMPLE_METHOD' (Field_Tac.field_tac in_prem ctxt THEN' Ring_Tac.ring_tac in_prem thms ctxt))
 \<close> "reduce equations over fields to equations over rings"
 
 end
diff --git a/src/HOL/Decision_Procs/langford.ML b/src/HOL/Decision_Procs/langford.ML
--- a/src/HOL/Decision_Procs/langford.ML
+++ b/src/HOL/Decision_Procs/langford.ML
@@ -1,261 +1,260 @@
 (*  Title:      HOL/Decision_Procs/langford.ML
     Author:     Amine Chaieb, TU Muenchen
 *)
 
 signature LANGFORD =
 sig
   val dlo_tac : Proof.context -> int -> tactic
   val dlo_conv : Proof.context -> cterm -> thm
 end
 
 structure Langford: LANGFORD =
 struct
 
 val dest_set =
   let
     fun h acc ct =
       (case Thm.term_of ct of
         \<^Const_>\<open>bot _\<close> => acc
       | \<^Const_>\<open>insert _ for _ _\<close> => h (Thm.dest_arg1 ct :: acc) (Thm.dest_arg ct));
   in h [] end;
 
 fun prove_finite cT u =
   let
     val [th0, th1] = map (Thm.instantiate' [SOME cT] []) @{thms finite.intros}
     fun ins x th =
       Thm.implies_elim
         (Thm.instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg) (Thm.cprop_of th), SOME x] th1) th
   in fold ins u th0 end;
 
 fun simp_rule ctxt =
   Conv.fconv_rule
     (Conv.arg_conv
       (Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms ball_simps simp_thms})));
 
 fun basic_dloqe ctxt stupid dlo_qeth dlo_qeth_nolb dlo_qeth_noub gather ep =
   (case Thm.term_of ep of
     \<^Const_>\<open>Ex _ for _\<close> =>
       let
         val p = Thm.dest_arg ep
         val ths =
           simplify (put_simpset HOL_basic_ss ctxt addsimps gather)
             (Thm.instantiate' [] [SOME p] stupid)
         val (L, U) =
           let val (_, q) = Thm.dest_abs_global (Thm.dest_arg (Thm.rhs_of ths))
           in (Thm.dest_arg1 q |> Thm.dest_arg1, Thm.dest_arg q |> Thm.dest_arg1) end
         fun proveneF S =
           let
             val (a, A) = Thm.dest_comb S |>> Thm.dest_arg
             val cT = Thm.ctyp_of_cterm a
             val ne = Thm.instantiate' [SOME cT] [SOME a, SOME A] @{thm insert_not_empty}
             val f = prove_finite cT (dest_set S)
          in (ne, f) end
 
         val qe =
           (case (Thm.term_of L, Thm.term_of U) of
             (\<^Const_>\<open>bot _\<close>, _) =>
               let val (neU, fU) = proveneF U
               in simp_rule ctxt (Thm.transitive ths (dlo_qeth_nolb OF [neU, fU])) end
           | (_, \<^Const_>\<open>bot _\<close>) =>
               let val (neL,fL) = proveneF L
               in simp_rule ctxt (Thm.transitive ths (dlo_qeth_noub OF [neL, fL])) end
           | _ =>
               let
                 val (neL, fL) = proveneF L
                 val (neU, fU) = proveneF U
               in simp_rule ctxt (Thm.transitive ths (dlo_qeth OF [neL, neU, fL, fU])) end)
       in qe end
   | _ => error "dlo_qe : Not an existential formula");
 
 val all_conjuncts =
   let
     fun h acc ct =
       (case Thm.term_of ct of
         \<^Const>\<open>HOL.conj for _ _\<close> => h (h acc (Thm.dest_arg ct)) (Thm.dest_arg1 ct)
       | _ => ct :: acc)
   in h [] end;
 
 fun conjuncts ct =
   (case Thm.term_of ct of
     \<^Const>\<open>HOL.conj for _ _\<close> => Thm.dest_arg1 ct :: conjuncts (Thm.dest_arg ct)
   | _ => [ct]);
 
 val list_conj =
-  foldr1 (fn (c, c') => Thm.apply (Thm.apply \<^cterm>\<open>HOL.conj\<close> c) c');
+  foldr1 (fn (A, B) => \<^let>\<open>A = A and B = B in cterm \<open>A \<and> B\<close>\<close>);
 
 fun mk_conj_tab th =
   let
     fun h acc th =
       (case Thm.prop_of th of
         \<^Const_>\<open>Trueprop for \<^Const_>\<open>HOL.conj for p q\<close>\<close> =>
           h (h acc (th RS conjunct2)) (th RS conjunct1)
       | \<^Const_>\<open>Trueprop for p\<close> => (p, th) :: acc)
   in fold (Termtab.insert Thm.eq_thm) (h [] th) Termtab.empty end;
 
 fun is_conj \<^Const_>\<open>HOL.conj for _ _\<close> = true
   | is_conj _ = false;
 
 fun prove_conj tab cjs =
   (case cjs of
     [c] =>
       if is_conj (Thm.term_of c)
       then prove_conj tab (conjuncts c)
       else tab c
   | c :: cs => conjI OF [prove_conj tab [c], prove_conj tab cs]);
 
 fun conj_aci_rule eq =
   let
     val (l, r) = Thm.dest_equals eq
     fun tabl c = the (Termtab.lookup (mk_conj_tab (Thm.assume l)) (Thm.term_of c))
     fun tabr c = the (Termtab.lookup (mk_conj_tab (Thm.assume r)) (Thm.term_of c))
     val ll = Thm.dest_arg l
     val rr = Thm.dest_arg r
     val thl  = prove_conj tabl (conjuncts rr) |> Drule.implies_intr_hyps
     val thr  = prove_conj tabr (conjuncts ll) |> Drule.implies_intr_hyps
     val eqI = Thm.instantiate' [] [SOME ll, SOME rr] @{thm iffI}
   in Thm.implies_elim (Thm.implies_elim eqI thl) thr |> mk_meta_eq end;
 
 fun contains x ct =
   member (op aconv) (Misc_Legacy.term_frees (Thm.term_of ct)) (Thm.term_of x);
 
 fun is_eqx x eq =
   (case Thm.term_of eq of
     \<^Const_>\<open>HOL.eq _ for l r\<close> =>
       l aconv Thm.term_of x orelse r aconv Thm.term_of x
   | _ => false);
 
 local
 
 fun proc ctxt ct =
   (case Thm.term_of ct of
     \<^Const_>\<open>Ex _ for \<open>Abs _\<close>\<close> =>
       let
         val e = Thm.dest_fun ct
         val (x,p) = Thm.dest_abs_global (Thm.dest_arg ct)
         val Free (xn, _) = Thm.term_of x
-        val Pp = Thm.apply \<^cterm>\<open>Trueprop\<close> p
         val (eqs,neqs) = List.partition (is_eqx x) (all_conjuncts p)
       in
         (case eqs of
           [] =>
             let
               val (dx, ndx) = List.partition (contains x) neqs
             in
               case ndx of
                 [] => NONE
               | _ =>
-                conj_aci_rule (Thm.mk_binop \<^cterm>\<open>(\<equiv>) :: prop => _\<close> Pp
-                  (Thm.apply \<^cterm>\<open>Trueprop\<close> (list_conj (ndx @ dx))))
+                conj_aci_rule
+                  \<^let>\<open>A = p and B = \<open>list_conj (ndx @ dx)\<close> in cterm \<open>Trueprop A \<equiv> Trueprop B\<close>\<close>
                 |> Thm.abstract_rule xn x
                 |> Drule.arg_cong_rule e
                 |> Conv.fconv_rule
                   (Conv.arg_conv
                     (Simplifier.rewrite
                       (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms ex_simps})))
                 |> SOME
             end
         | _ =>
-            conj_aci_rule (Thm.mk_binop \<^cterm>\<open>(\<equiv>) :: prop => _\<close> Pp
-              (Thm.apply \<^cterm>\<open>Trueprop\<close> (list_conj (eqs @ neqs))))
+            conj_aci_rule
+              \<^let>\<open>A = p and B = \<open>list_conj (eqs @ neqs)\<close> in cterm \<open>Trueprop A \<equiv> Trueprop B\<close>\<close>
             |> Thm.abstract_rule xn x |> Drule.arg_cong_rule e
             |> Conv.fconv_rule
                 (Conv.arg_conv
                   (Simplifier.rewrite
                     (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms ex_simps})))
             |> SOME)
       end
   | _ => NONE);
 
 in
 
 val reduce_ex_simproc =
   Simplifier.make_simproc \<^context> "reduce_ex_simproc"
     {lhss = [\<^term>\<open>\<exists>x. P x\<close>], proc = K proc};
 
 end;
 
 fun raw_dlo_conv ctxt dlo_ss ({qe_bnds, qe_nolb, qe_noub, gst, gs, ...}: Langford_Data.entry) =
   let
     val ctxt' =
       Context_Position.set_visible false (put_simpset dlo_ss ctxt)
         addsimps @{thms dnf_simps} addsimprocs [reduce_ex_simproc]
     val dnfex_conv = Simplifier.rewrite ctxt'
     val pcv =
       Simplifier.rewrite
         (put_simpset dlo_ss ctxt
           addsimps @{thms simp_thms ex_simps all_simps all_not_ex not_all ex_disj_distrib})
     val mk_env = Cterms.list_set_rev o Cterms.build o Drule.add_frees_cterm
   in
     fn p =>
       Qelim.gen_qelim_conv ctxt pcv pcv dnfex_conv cons
         (mk_env p) (K Thm.reflexive) (K Thm.reflexive)
         (K (basic_dloqe ctxt gst qe_bnds qe_nolb qe_noub gs)) p
   end;
 
 val grab_atom_bop =
   let
     fun h ctxt tm =
       (case Thm.term_of tm of
         \<^Const_>\<open>HOL.eq \<^Type>\<open>bool\<close> for _ _\<close> => find_args ctxt tm
       | \<^Const_>\<open>Not for _\<close> => h ctxt (Thm.dest_arg tm)
       | \<^Const_>\<open>All _ for _\<close> => find_body ctxt (Thm.dest_arg tm)
       | \<^Const_>\<open>Pure.all _ for _\<close> => find_body ctxt (Thm.dest_arg tm)
       | \<^Const_>\<open>Ex _ for _\<close> => find_body ctxt (Thm.dest_arg tm)
       | \<^Const_>\<open>HOL.conj for _ _\<close> => find_args ctxt tm
       | \<^Const_>\<open>HOL.disj for _ _\<close> => find_args ctxt tm
       | \<^Const_>\<open>HOL.implies for _ _\<close> => find_args ctxt tm
       | \<^Const_>\<open>Pure.imp for _ _\<close> => find_args ctxt tm
       | \<^Const_>\<open>Pure.eq _ for _ _\<close> => find_args ctxt tm
       | \<^Const_>\<open>Trueprop for _\<close> => h ctxt (Thm.dest_arg tm)
       | _ => Thm.dest_fun2 tm)
     and find_args ctxt tm =
       (h ctxt (Thm.dest_arg tm) handle CTERM _ => h ctxt (Thm.dest_arg1 tm))
     and find_body ctxt b =
       let val ((_, b'), ctxt') = Variable.dest_abs_cterm b ctxt
       in h ctxt' b' end;
   in h end;
 
 fun dlo_instance ctxt tm =
   (fst (Langford_Data.get ctxt), Langford_Data.match ctxt (grab_atom_bop ctxt tm));
 
 fun dlo_conv ctxt tm =
   (case dlo_instance ctxt tm of
     (_, NONE) => raise CTERM ("dlo_conv (langford): no corresponding instance in context!", [tm])
   | (ss, SOME instance) => raw_dlo_conv ctxt ss instance tm);
 
 fun generalize_tac ctxt f = CSUBGOAL (fn (p, _) => PRIMITIVE (fn st =>
   let
     fun all x t =
       Thm.apply (Thm.cterm_of ctxt (Logic.all_const (Thm.typ_of_cterm x))) (Thm.lambda x t)
     val ts = sort Thm.fast_term_ord (f p)
     val p' = fold_rev all ts p
   in Thm.implies_intr p' (Thm.implies_elim st (fold Thm.forall_elim ts (Thm.assume p'))) end));
 
 fun cfrees ats ct =
   let
     val ins = insert (op aconvc)
     fun h acc t =
       (case Thm.term_of t of
         _ $ _ $ _ =>
           if member (op aconvc) ats (Thm.dest_fun2 t)
           then ins (Thm.dest_arg t) (ins (Thm.dest_arg1 t) acc)
           else h (h acc (Thm.dest_arg t)) (Thm.dest_fun t)
       | _ $ _ => h (h acc (Thm.dest_arg t)) (Thm.dest_fun t)
       | Abs _ => Thm.dest_abs_global t ||> h acc |> uncurry (remove (op aconvc))
       | Free _ => if member (op aconvc) ats t then acc else ins t acc
       | Var _ => if member (op aconvc) ats t then acc else ins t acc
       | _ => acc)
   in h [] ct end
 
 fun dlo_tac ctxt = CSUBGOAL (fn (p, i) =>
   (case dlo_instance ctxt p of
     (ss, NONE) => simp_tac (put_simpset ss ctxt) i
   | (ss, SOME instance) =>
       Object_Logic.full_atomize_tac ctxt i THEN
       simp_tac (put_simpset ss ctxt) i
       THEN (CONVERSION Thm.eta_long_conversion) i
       THEN (TRY o generalize_tac ctxt (cfrees (#atoms instance))) i
       THEN Object_Logic.full_atomize_tac ctxt i
       THEN CONVERSION (Object_Logic.judgment_conv ctxt (raw_dlo_conv ctxt ss instance)) i
       THEN (simp_tac (put_simpset ss ctxt) i)));
 end;