# HG changeset patch
# User berghofe
# Date 1485687588 -3600
# Node ID bf41e1109db34b3ceef21847ebd9a1052603b33a
# Parent  d19a5579ffb8737f04b664aeac5de77a31f1c379
Added new / improved tactics for fields and rings

diff -r d19a5579ffb8 -r bf41e1109db3 src/HOL/Decision_Procs/Algebra_Aux.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Decision_Procs/Algebra_Aux.thy	Sun Jan 29 11:59:48 2017 +0100
@@ -0,0 +1,505 @@
+(*  Title:      HOL/Decision_Procs/Algebra_Aux.thy
+    Author:     Stefan Berghofer
+*)
+
+section \<open>Things that can be added to the Algebra library\<close>
+
+theory Algebra_Aux
+imports "~~/src/HOL/Algebra/Ring"
+begin
+
+definition of_natural :: "('a, 'm) ring_scheme \<Rightarrow> nat \<Rightarrow> 'a" ("\<guillemotleft>_\<guillemotright>\<^sub>\<nat>\<index>") where
+  "\<guillemotleft>n\<guillemotright>\<^sub>\<nat>\<^bsub>R\<^esub> = (op \<oplus>\<^bsub>R\<^esub> \<one>\<^bsub>R\<^esub> ^^ n) \<zero>\<^bsub>R\<^esub>"
+
+definition of_integer :: "('a, 'm) ring_scheme \<Rightarrow> int \<Rightarrow> 'a" ("\<guillemotleft>_\<guillemotright>\<index>") where
+  "\<guillemotleft>i\<guillemotright>\<^bsub>R\<^esub> = (if 0 \<le> i then \<guillemotleft>nat i\<guillemotright>\<^sub>\<nat>\<^bsub>R\<^esub> else \<ominus>\<^bsub>R\<^esub> \<guillemotleft>nat (- i)\<guillemotright>\<^sub>\<nat>\<^bsub>R\<^esub>)"
+
+context ring begin
+
+lemma of_nat_0 [simp]: "\<guillemotleft>0\<guillemotright>\<^sub>\<nat> = \<zero>"
+  by (simp add: of_natural_def)
+
+lemma of_nat_Suc [simp]: "\<guillemotleft>Suc n\<guillemotright>\<^sub>\<nat> = \<one> \<oplus> \<guillemotleft>n\<guillemotright>\<^sub>\<nat>"
+  by (simp add: of_natural_def)
+
+lemma of_int_0 [simp]: "\<guillemotleft>0\<guillemotright> = \<zero>"
+  by (simp add: of_integer_def)
+
+lemma of_nat_closed [simp]: "\<guillemotleft>n\<guillemotright>\<^sub>\<nat> \<in> carrier R"
+  by (induct n) simp_all
+
+lemma of_int_closed [simp]: "\<guillemotleft>i\<guillemotright> \<in> carrier R"
+  by (simp add: of_integer_def)
+
+lemma of_int_minus [simp]: "\<guillemotleft>- i\<guillemotright> = \<ominus> \<guillemotleft>i\<guillemotright>"
+  by (simp add: of_integer_def)
+
+lemma of_nat_add [simp]: "\<guillemotleft>m + n\<guillemotright>\<^sub>\<nat> = \<guillemotleft>m\<guillemotright>\<^sub>\<nat> \<oplus> \<guillemotleft>n\<guillemotright>\<^sub>\<nat>"
+  by (induct m) (simp_all add: a_ac)
+
+lemma of_nat_diff [simp]: "n \<le> m \<Longrightarrow> \<guillemotleft>m - n\<guillemotright>\<^sub>\<nat> = \<guillemotleft>m\<guillemotright>\<^sub>\<nat> \<ominus> \<guillemotleft>n\<guillemotright>\<^sub>\<nat>"
+proof (induct m arbitrary: n)
+  case (Suc m)
+  note Suc' = this
+  show ?case
+  proof (cases n)
+    case (Suc k)
+    with Suc' have "\<guillemotleft>Suc m - Suc k\<guillemotright>\<^sub>\<nat> = \<guillemotleft>m\<guillemotright>\<^sub>\<nat> \<ominus> \<guillemotleft>k\<guillemotright>\<^sub>\<nat>" by simp
+    also have "\<dots> = \<one> \<oplus> \<ominus> \<one> \<oplus> (\<guillemotleft>m\<guillemotright>\<^sub>\<nat> \<ominus> \<guillemotleft>k\<guillemotright>\<^sub>\<nat>)"
+      by (simp add: r_neg)
+    also have "\<dots> = \<guillemotleft>Suc m\<guillemotright>\<^sub>\<nat> \<ominus> \<guillemotleft>Suc k\<guillemotright>\<^sub>\<nat>"
+      by (simp add: minus_eq minus_add a_ac)
+    finally show ?thesis using Suc by simp
+  qed (simp add: minus_eq)
+qed (simp add: minus_eq)
+
+lemma of_int_add [simp]: "\<guillemotleft>i + j\<guillemotright> = \<guillemotleft>i\<guillemotright> \<oplus> \<guillemotleft>j\<guillemotright>"
+proof (cases "0 \<le> i")
+  case True
+  show ?thesis
+  proof (cases "0 \<le> j")
+    case True
+    with `0 \<le> i` show ?thesis by (simp add: of_integer_def nat_add_distrib)
+  next
+    case False
+    show ?thesis
+    proof (cases "0 \<le> i + j")
+      case True
+      then have "\<guillemotleft>i + j\<guillemotright> = \<guillemotleft>nat (i - (- j))\<guillemotright>\<^sub>\<nat>"
+        by (simp add: of_integer_def)
+      also from True `0 \<le> i` `\<not> 0 \<le> j`
+      have "nat (i - (- j)) = nat i - nat (- j)"
+        by (simp add: nat_diff_distrib)
+      finally show ?thesis using True `0 \<le> i` `\<not> 0 \<le> j`
+        by (simp add: minus_eq of_integer_def)
+    next
+      case False
+      then have "\<guillemotleft>i + j\<guillemotright> = \<ominus> \<guillemotleft>nat (- j - i)\<guillemotright>\<^sub>\<nat>"
+        by (simp add: of_integer_def) (simp only: diff_conv_add_uminus add_ac)
+      also from False `0 \<le> i` `\<not> 0 \<le> j`
+      have "nat (- j - i) = nat (- j) - nat i"
+        by (simp add: nat_diff_distrib)
+      finally show ?thesis using False `0 \<le> i` `\<not> 0 \<le> j`
+        by (simp add: minus_eq minus_add a_ac of_integer_def)
+    qed
+  qed
+next
+  case False
+  show ?thesis
+  proof (cases "0 \<le> j")
+    case True
+    show ?thesis
+    proof (cases "0 \<le> i + j")
+      case True
+      then have "\<guillemotleft>i + j\<guillemotright> = \<guillemotleft>nat (j - (- i))\<guillemotright>\<^sub>\<nat>"
+        by (simp add: of_integer_def add_ac)
+      also from True `\<not> 0 \<le> i` `0 \<le> j`
+      have "nat (j - (- i)) = nat j - nat (- i)"
+        by (simp add: nat_diff_distrib)
+      finally show ?thesis using True `\<not> 0 \<le> i` `0 \<le> j`
+        by (simp add: minus_eq minus_add a_ac of_integer_def)
+    next
+      case False
+      then have "\<guillemotleft>i + j\<guillemotright> = \<ominus> \<guillemotleft>nat (- i - j)\<guillemotright>\<^sub>\<nat>"
+        by (simp add: of_integer_def)
+      also from False `\<not> 0 \<le> i` `0 \<le> j`
+      have "nat (- i - j) = nat (- i) - nat j"
+        by (simp add: nat_diff_distrib)
+      finally show ?thesis using False `\<not> 0 \<le> i` `0 \<le> j`
+        by (simp add: minus_eq minus_add of_integer_def)
+    qed
+  next
+    case False
+    with `\<not> 0 \<le> i` show ?thesis
+      by (simp add: of_integer_def nat_add_distrib minus_add diff_conv_add_uminus
+        del: add_uminus_conv_diff uminus_add_conv_diff)
+  qed
+qed
+
+lemma of_int_diff [simp]: "\<guillemotleft>i - j\<guillemotright> = \<guillemotleft>i\<guillemotright> \<ominus> \<guillemotleft>j\<guillemotright>"
+  by (simp only: diff_conv_add_uminus of_int_add) (simp add: minus_eq)
+
+lemma of_nat_mult [simp]: "\<guillemotleft>i * j\<guillemotright>\<^sub>\<nat> = \<guillemotleft>i\<guillemotright>\<^sub>\<nat> \<otimes> \<guillemotleft>j\<guillemotright>\<^sub>\<nat>"
+  by (induct i) (simp_all add: l_distr)
+
+lemma of_int_mult [simp]: "\<guillemotleft>i * j\<guillemotright> = \<guillemotleft>i\<guillemotright> \<otimes> \<guillemotleft>j\<guillemotright>"
+proof (cases "0 \<le> i")
+  case True
+  show ?thesis
+  proof (cases "0 \<le> j")
+    case True
+    with `0 \<le> i` show ?thesis
+      by (simp add: of_integer_def nat_mult_distrib zero_le_mult_iff)
+  next
+    case False
+    with `0 \<le> i` show ?thesis
+      by (simp add: of_integer_def zero_le_mult_iff
+        minus_mult_right nat_mult_distrib r_minus
+        del: minus_mult_right [symmetric])
+  qed
+next
+  case False
+  show ?thesis
+  proof (cases "0 \<le> j")
+    case True
+    with `\<not> 0 \<le> i` show ?thesis
+      by (simp add: of_integer_def zero_le_mult_iff
+        minus_mult_left nat_mult_distrib l_minus
+        del: minus_mult_left [symmetric])
+  next
+    case False
+    with `\<not> 0 \<le> i` show ?thesis
+      by (simp add: of_integer_def zero_le_mult_iff
+        minus_mult_minus [of i j, symmetric] nat_mult_distrib
+        l_minus r_minus
+        del: minus_mult_minus
+        minus_mult_left [symmetric] minus_mult_right [symmetric])
+  qed
+qed
+
+lemma of_int_1 [simp]: "\<guillemotleft>1\<guillemotright> = \<one>"
+  by (simp add: of_integer_def)
+
+lemma of_int_2: "\<guillemotleft>2\<guillemotright> = \<one> \<oplus> \<one>"
+  by (simp add: of_integer_def numeral_2_eq_2)
+
+lemma minus_0_r [simp]: "x \<in> carrier R \<Longrightarrow> x \<ominus> \<zero> = x"
+  by (simp add: minus_eq)
+
+lemma minus_0_l [simp]: "x \<in> carrier R \<Longrightarrow> \<zero> \<ominus> x = \<ominus> x"
+  by (simp add: minus_eq)
+
+lemma eq_diff0:
+  assumes "x \<in> carrier R" "y \<in> carrier R"
+  shows "(x \<ominus> y = \<zero>) = (x = y)"
+proof
+  assume "x \<ominus> y = \<zero>"
+  with assms have "x \<oplus> (\<ominus> y \<oplus> y) = y"
+    by (simp add: minus_eq a_assoc [symmetric])
+  with assms show "x = y" by (simp add: l_neg)
+next
+  assume "x = y"
+  with assms show "x \<ominus> y = \<zero>" by (simp add: minus_eq r_neg)
+qed
+
+lemma power2_eq_square: "x \<in> carrier R \<Longrightarrow> x (^) (2::nat) = x \<otimes> x"
+  by (simp add: numeral_eq_Suc)
+
+lemma eq_neg_iff_add_eq_0:
+  assumes "x \<in> carrier R" "y \<in> carrier R"
+  shows "(x = \<ominus> y) = (x \<oplus> y = \<zero>)"
+proof
+  assume "x = \<ominus> y"
+  with assms show "x \<oplus> y = \<zero>" by (simp add: l_neg)
+next
+  assume "x \<oplus> y = \<zero>"
+  with assms have "x \<oplus> (y \<oplus> \<ominus> y) = \<zero> \<oplus> \<ominus> y"
+    by (simp add: a_assoc [symmetric])
+  with assms show "x = \<ominus> y"
+    by (simp add: r_neg)
+qed
+
+lemma neg_equal_iff_equal:
+  assumes x: "x \<in> carrier R" and y: "y \<in> carrier R"
+  shows "(\<ominus> x = \<ominus> y) = (x = y)"
+proof
+  assume "\<ominus> x = \<ominus> y"
+  then have "\<ominus> (\<ominus> x) = \<ominus> (\<ominus> y)" by simp
+  with x y show "x = y" by simp
+next
+  assume "x = y"
+  then show "\<ominus> x = \<ominus> y" by simp
+qed
+
+lemma neg_equal_swap:
+  assumes x: "x \<in> carrier R" and y: "y \<in> carrier R"
+  shows "(\<ominus> x = y) = (x = \<ominus> y)"
+  using assms neg_equal_iff_equal [of x "\<ominus> y"]
+  by simp
+
+lemma mult2: "x \<in> carrier R \<Longrightarrow> x \<oplus> x = \<guillemotleft>2\<guillemotright> \<otimes> x"
+  by (simp add: of_int_2 l_distr)
+
+end
+
+lemma (in cring) of_int_power [simp]: "\<guillemotleft>i ^ n\<guillemotright> = \<guillemotleft>i\<guillemotright> (^) n"
+  by (induct n) (simp_all add: m_ac)
+
+definition cring_class_ops :: "'a::comm_ring_1 ring" where
+  "cring_class_ops \<equiv> \<lparr>carrier = UNIV, mult = op *, one = 1, zero = 0, add = op +\<rparr>"
+
+lemma cring_class: "cring cring_class_ops"
+  apply unfold_locales
+  apply (auto simp add: cring_class_ops_def ring_distribs Units_def)
+  apply (rule_tac x="- x" in exI)
+  apply simp
+  done
+
+lemma carrier_class: "x \<in> carrier cring_class_ops"
+  by (simp add: cring_class_ops_def)
+
+lemma zero_class: "\<zero>\<^bsub>cring_class_ops\<^esub> = 0"
+  by (simp add: cring_class_ops_def)
+
+lemma one_class: "\<one>\<^bsub>cring_class_ops\<^esub> = 1"
+  by (simp add: cring_class_ops_def)
+
+lemma plus_class: "x \<oplus>\<^bsub>cring_class_ops\<^esub> y = x + y"
+  by (simp add: cring_class_ops_def)
+
+lemma times_class: "x \<otimes>\<^bsub>cring_class_ops\<^esub> y = x * y"
+  by (simp add: cring_class_ops_def)
+
+lemma uminus_class: "\<ominus>\<^bsub>cring_class_ops\<^esub> x = - x"
+  apply (simp add: a_inv_def m_inv_def cring_class_ops_def)
+  apply (rule the_equality)
+  apply (simp_all add: eq_neg_iff_add_eq_0)
+  done
+
+lemma minus_class: "x \<ominus>\<^bsub>cring_class_ops\<^esub> y = x - y"
+  by (simp add: a_minus_def carrier_class plus_class uminus_class)
+
+lemma power_class: "x (^)\<^bsub>cring_class_ops\<^esub> n = x ^ n"
+  by (induct n) (simp_all add: one_class times_class
+    monoid.nat_pow_0 [OF comm_monoid.axioms(1) [OF cring.axioms(2) [OF cring_class]]]
+    monoid.nat_pow_Suc [OF comm_monoid.axioms(1) [OF cring.axioms(2) [OF cring_class]]])
+
+lemma of_nat_class: "\<guillemotleft>n\<guillemotright>\<^sub>\<nat>\<^bsub>cring_class_ops\<^esub> = of_nat n"
+  by (induct n) (simp_all add: cring_class_ops_def of_natural_def)
+
+lemma of_int_class: "\<guillemotleft>i\<guillemotright>\<^bsub>cring_class_ops\<^esub> = of_int i"
+  by (simp add: of_integer_def of_nat_class uminus_class)
+
+lemmas class_simps = zero_class one_class plus_class minus_class uminus_class
+  times_class power_class of_nat_class of_int_class carrier_class
+
+interpretation cring_class: cring "cring_class_ops::'a::comm_ring_1 ring"
+  rewrites
+    "(\<zero>\<^bsub>cring_class_ops\<^esub>::'a) = 0" and
+    "(\<one>\<^bsub>cring_class_ops\<^esub>::'a) = 1" and
+    "(x::'a) \<oplus>\<^bsub>cring_class_ops\<^esub> y = x + y" and
+    "(x::'a) \<otimes>\<^bsub>cring_class_ops\<^esub> y = x * y" and
+    "\<ominus>\<^bsub>cring_class_ops\<^esub> (x::'a) = - x" and
+    "(x::'a) \<ominus>\<^bsub>cring_class_ops\<^esub> y = x - y" and
+    "(x::'a) (^)\<^bsub>cring_class_ops\<^esub> n = x ^ n" and
+    "\<guillemotleft>n\<guillemotright>\<^sub>\<nat>\<^bsub>cring_class_ops\<^esub> = of_nat n" and
+    "((\<guillemotleft>i\<guillemotright>\<^bsub>cring_class_ops\<^esub>)::'a) = of_int i" and
+    "(Int.of_int (numeral m)::'a) = numeral m"
+  by (simp_all add: cring_class class_simps)
+
+lemma (in domain) nat_pow_eq_0_iff [simp]:
+  "a \<in> carrier R \<Longrightarrow> (a (^) (n::nat) = \<zero>) = (a = \<zero> \<and> n \<noteq> 0)"
+  by (induct n) (auto simp add: integral_iff)
+
+lemma (in domain) square_eq_iff:
+  assumes "x \<in> carrier R" "y \<in> carrier R"
+  shows "(x \<otimes> x = y \<otimes> y) = (x = y \<or> x = \<ominus> y)"
+proof
+  assume "x \<otimes> x = y \<otimes> y"
+  with assms have "(x \<ominus> y) \<otimes> (x \<oplus> y) = x \<otimes> y \<oplus> \<ominus> (x \<otimes> y) \<oplus> (y \<otimes> y \<oplus> \<ominus> (y \<otimes> y))"
+    by (simp add: r_distr l_distr minus_eq r_minus m_comm a_ac)
+  with assms show "x = y \<or> x = \<ominus> y"
+    by (simp add: integral_iff eq_neg_iff_add_eq_0 eq_diff0 r_neg)
+next
+  assume "x = y \<or> x = \<ominus> y"
+  with assms show "x \<otimes> x = y \<otimes> y" by (auto simp add: l_minus r_minus)
+qed
+
+definition
+  m_div :: "('a, 'b) ring_scheme \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<oslash>\<index>" 70) where
+  "x \<oslash>\<^bsub>G\<^esub> y = (if y = \<zero>\<^bsub>G\<^esub> then \<zero>\<^bsub>G\<^esub> else x \<otimes>\<^bsub>G\<^esub> inv\<^bsub>G\<^esub> y)"
+
+context field
+begin
+
+lemma inv_closed [simp]: "x \<in> carrier R \<Longrightarrow> x \<noteq> \<zero> \<Longrightarrow> inv x \<in> carrier R"
+  by (simp add: field_Units)
+
+lemma l_inv [simp]: "x \<in> carrier R \<Longrightarrow> x \<noteq> \<zero> \<Longrightarrow> inv x \<otimes> x = \<one>"
+  by (simp add: field_Units)
+
+lemma r_inv [simp]: "x \<in> carrier R \<Longrightarrow> x \<noteq> \<zero> \<Longrightarrow> x \<otimes> inv x = \<one>"
+  by (simp add: field_Units)
+
+lemma inverse_unique:
+  assumes a: "a \<in> carrier R"
+  and b: "b \<in> carrier R"
+  and ab: "a \<otimes> b = \<one>"
+  shows "inv a = b"
+proof -
+  have "a \<noteq> \<zero>" using ab b by (cases "a = \<zero>") simp_all
+  moreover with a have "inv a \<otimes> (a \<otimes> b) = inv a" by (simp add: ab)
+  ultimately show ?thesis using a b by (simp add: m_assoc [symmetric])
+qed
+
+lemma nonzero_inverse_inverse_eq:
+  "a \<in> carrier R \<Longrightarrow> a \<noteq> \<zero> \<Longrightarrow> inv (inv a) = a"
+  by (rule inverse_unique) simp_all
+
+lemma inv_1 [simp]: "inv \<one> = \<one>"
+  by (rule inverse_unique) simp_all
+
+lemma nonzero_inverse_mult_distrib:
+  assumes "a \<in> carrier R" and "b \<in> carrier R" and "a \<noteq> \<zero>" and "b \<noteq> \<zero>"
+  shows "inv (a \<otimes> b) = inv b \<otimes> inv a"
+proof -
+  have "a \<otimes> (b \<otimes> inv b) \<otimes> inv a = \<one>" using assms by simp
+  hence eq: "a \<otimes> b \<otimes> (inv b \<otimes> inv a) = \<one>" using assms
+    by (simp only: m_assoc m_closed inv_closed assms)
+  from inverse_unique [OF _ _ eq] assms
+  show ?thesis by simp
+qed
+
+lemma nonzero_imp_inverse_nonzero:
+  assumes "a \<in> carrier R" and "a \<noteq> \<zero>"
+  shows "inv a \<noteq> \<zero>"
+proof
+  assume ianz: "inv a = \<zero>"
+  from assms
+  have "\<one> = a \<otimes> inv a" by simp
+  also with assms have "... = \<zero>" by (simp add: ianz)
+  finally have "\<one> = \<zero>" .
+  thus False by (simp add: eq_commute)
+qed
+
+lemma nonzero_divide_divide_eq_left:
+  "a \<in> carrier R \<Longrightarrow> b \<in> carrier R \<Longrightarrow> c \<in> carrier R \<Longrightarrow> b \<noteq> \<zero> \<Longrightarrow> c \<noteq> \<zero> \<Longrightarrow>
+   a \<oslash> b \<oslash> c = a \<oslash> (b \<otimes> c)"
+  by (simp add: m_div_def nonzero_inverse_mult_distrib m_ac integral_iff)
+
+lemma nonzero_times_divide_eq:
+  "a \<in> carrier R \<Longrightarrow> b \<in> carrier R \<Longrightarrow> c \<in> carrier R \<Longrightarrow> d \<in> carrier R \<Longrightarrow>
+   b \<noteq> \<zero> \<Longrightarrow> d \<noteq> \<zero> \<Longrightarrow> (a \<oslash> b) \<otimes> (c \<oslash> d) = (a \<otimes> c) \<oslash> (b \<otimes> d)"
+  by (simp add: m_div_def nonzero_inverse_mult_distrib m_ac integral_iff)
+
+lemma nonzero_divide_divide_eq:
+  "a \<in> carrier R \<Longrightarrow> b \<in> carrier R \<Longrightarrow> c \<in> carrier R \<Longrightarrow> d \<in> carrier R \<Longrightarrow>
+   b \<noteq> \<zero> \<Longrightarrow> c \<noteq> \<zero> \<Longrightarrow> d \<noteq> \<zero> \<Longrightarrow> (a \<oslash> b) \<oslash> (c \<oslash> d) = (a \<otimes> d) \<oslash> (b \<otimes> c)"
+  by (simp add: m_div_def nonzero_inverse_mult_distrib
+    nonzero_imp_inverse_nonzero nonzero_inverse_inverse_eq m_ac integral_iff)
+
+lemma divide_1 [simp]: "x \<in> carrier R \<Longrightarrow> x \<oslash> \<one> = x"
+  by (simp add: m_div_def)
+
+lemma add_frac_eq:
+  assumes "x \<in> carrier R" and "y \<in> carrier R" and "z \<in> carrier R" and "w \<in> carrier R"
+  and "y \<noteq> \<zero>" and "z \<noteq> \<zero>"
+  shows "x \<oslash> y \<oplus> w \<oslash> z = (x \<otimes> z \<oplus> w \<otimes> y) \<oslash> (y \<otimes> z)"
+proof -
+  from assms
+  have "x \<oslash> y \<oplus> w \<oslash> z = x \<otimes> inv y \<otimes> (z \<otimes> inv z) \<oplus> w \<otimes> inv z \<otimes> (y \<otimes> inv y)"
+    by (simp add: m_div_def)
+  also from assms have "\<dots> = (x \<otimes> z \<oplus> w \<otimes> y) \<oslash> (y \<otimes> z)"
+    by (simp add: m_div_def nonzero_inverse_mult_distrib r_distr m_ac integral_iff del: r_inv)
+  finally show ?thesis .
+qed
+
+lemma div_closed [simp]:
+  "x \<in> carrier R \<Longrightarrow> y \<in> carrier R \<Longrightarrow> y \<noteq> \<zero> \<Longrightarrow> x \<oslash> y \<in> carrier R"
+  by (simp add: m_div_def)
+
+lemma minus_divide_left [simp]:
+  "a \<in> carrier R \<Longrightarrow> b \<in> carrier R \<Longrightarrow> b \<noteq> \<zero> \<Longrightarrow> \<ominus> (a \<oslash> b) = \<ominus> a \<oslash> b"
+  by (simp add: m_div_def l_minus)
+
+lemma diff_frac_eq:
+  assumes "x \<in> carrier R" and "y \<in> carrier R" and "z \<in> carrier R" and "w \<in> carrier R"
+  and "y \<noteq> \<zero>" and "z \<noteq> \<zero>"
+  shows "x \<oslash> y \<ominus> w \<oslash> z = (x \<otimes> z \<ominus> w \<otimes> y) \<oslash> (y \<otimes> z)"
+  using assms
+  by (simp add: minus_eq l_minus add_frac_eq)
+
+lemma nonzero_mult_divide_mult_cancel_left [simp]:
+  assumes "a \<in> carrier R" and "b \<in> carrier R" and "c \<in> carrier R"
+  and "b \<noteq> \<zero>" and "c \<noteq> \<zero>"
+  shows "(c \<otimes> a) \<oslash> (c \<otimes> b) = a \<oslash> b"
+proof -
+  from assms have "(c \<otimes> a) \<oslash> (c \<otimes> b) = c \<otimes> a \<otimes> (inv b \<otimes> inv c)"
+    by (simp add: m_div_def nonzero_inverse_mult_distrib integral_iff)
+  also from assms have "\<dots> =  a \<otimes> inv b \<otimes> (inv c \<otimes> c)"
+    by (simp add: m_ac)
+  also from assms have "\<dots> =  a \<otimes> inv b" by simp
+  finally show ?thesis using assms by (simp add: m_div_def)
+qed
+
+lemma times_divide_eq_left [simp]:
+  "a \<in> carrier R \<Longrightarrow> b \<in> carrier R \<Longrightarrow> c \<in> carrier R \<Longrightarrow> c \<noteq> \<zero> \<Longrightarrow>
+   (b \<oslash> c) \<otimes> a = b \<otimes> a \<oslash> c"
+  by (simp add: m_div_def m_ac)
+
+lemma times_divide_eq_right [simp]:
+  "a \<in> carrier R \<Longrightarrow> b \<in> carrier R \<Longrightarrow> c \<in> carrier R \<Longrightarrow> c \<noteq> \<zero> \<Longrightarrow>
+   a \<otimes> (b \<oslash> c) = a \<otimes> b \<oslash> c"
+  by (simp add: m_div_def m_ac)
+
+lemma nonzero_power_divide:
+  "a \<in> carrier R \<Longrightarrow> b \<in> carrier R \<Longrightarrow> b \<noteq> \<zero> \<Longrightarrow>
+   (a \<oslash> b) (^) (n::nat) = a (^) n \<oslash> b (^) n"
+  by (induct n) (simp_all add: nonzero_divide_divide_eq_left)
+
+lemma r_diff_distr:
+  "x \<in> carrier R \<Longrightarrow> y \<in> carrier R \<Longrightarrow> z \<in> carrier R \<Longrightarrow>
+   z \<otimes> (x \<ominus> y) = z \<otimes> x \<ominus> z \<otimes> y"
+  by (simp add: minus_eq r_distr r_minus)
+
+lemma divide_zero_left [simp]:
+  "a \<in> carrier R \<Longrightarrow> a \<noteq> \<zero> \<Longrightarrow> \<zero> \<oslash> a = \<zero>"
+  by (simp add: m_div_def)
+
+lemma divide_self: "a \<in> carrier R \<Longrightarrow> a \<noteq> \<zero> \<Longrightarrow> a \<oslash> a = \<one>"
+  by (simp add: m_div_def)
+
+lemma divide_eq_0_iff:
+  assumes "a \<in> carrier R"
+  and "b \<in> carrier R"
+  and "b \<noteq> \<zero>"
+  shows "(a \<oslash> b = \<zero>) = (a = \<zero>)"
+proof
+  assume "a = \<zero>"
+  with assms show "a \<oslash> b = \<zero>" by simp
+next
+  assume "a \<oslash> b = \<zero>"
+  with assms have "b \<otimes> (a \<oslash> b) = b \<otimes> \<zero>" by simp
+  also from assms have "b \<otimes> (a \<oslash> b) = b \<otimes> a \<oslash> b" by simp
+  also from assms have "b \<otimes> a = a \<otimes> b" by (simp add: m_comm)
+  also from assms have "a \<otimes> b \<oslash> b = a \<otimes> (b \<oslash> b)" by simp
+  also from assms have "b \<oslash> b = \<one>" by (simp add: divide_self)
+  finally show "a = \<zero>" using assms by simp
+qed
+
+end
+
+lemma field_class: "field (cring_class_ops::'a::field ring)"
+  apply unfold_locales
+  apply (simp_all add: cring_class_ops_def)
+  apply (auto simp add: Units_def)
+  apply (rule_tac x="1 / x" in exI)
+  apply simp
+  done
+
+lemma div_class: "(x::'a::field) \<oslash>\<^bsub>cring_class_ops\<^esub> y = x / y"
+  apply (simp add: m_div_def m_inv_def class_simps)
+  apply (rule impI)
+  apply (rule ssubst [OF the_equality, of _ "1 / y"])
+  apply simp_all
+  apply (drule conjunct2)
+  apply (drule_tac f="\<lambda>x. x / y" in arg_cong)
+  apply simp
+  done
+
+interpretation field_class: field "cring_class_ops::'a::field ring"
+  rewrites
+    "(\<zero>\<^bsub>cring_class_ops\<^esub>::'a) = 0" and
+    "(\<one>\<^bsub>cring_class_ops\<^esub>::'a) = 1" and
+    "(x::'a) \<oplus>\<^bsub>cring_class_ops\<^esub> y = x + y" and
+    "(x::'a) \<otimes>\<^bsub>cring_class_ops\<^esub> y = x * y" and
+    "\<ominus>\<^bsub>cring_class_ops\<^esub> (x::'a) = - x" and
+    "(x::'a) \<ominus>\<^bsub>cring_class_ops\<^esub> y = x - y" and
+    "(x::'a) (^)\<^bsub>cring_class_ops\<^esub> n = x ^ n" and
+    "\<guillemotleft>n\<guillemotright>\<^sub>\<nat>\<^bsub>cring_class_ops\<^esub> = of_nat n" and
+    "((\<guillemotleft>i\<guillemotright>\<^bsub>cring_class_ops\<^esub>)::'a) = of_int i" and
+    "(x::'a) \<oslash>\<^bsub>cring_class_ops\<^esub> y = x / y" and
+    "(Int.of_int (numeral m)::'a) = numeral m"
+  by (simp_all add: field_class class_simps div_class)
+
+end
diff -r d19a5579ffb8 -r bf41e1109db3 src/HOL/Decision_Procs/Commutative_Ring.thy
--- a/src/HOL/Decision_Procs/Commutative_Ring.thy	Sun Jan 29 11:49:48 2017 +0100
+++ b/src/HOL/Decision_Procs/Commutative_Ring.thy	Sun Jan 29 11:59:48 2017 +0100
@@ -1,4 +1,5 @@
-(*  Author:     Bernhard Haeupler
+(*  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.
 *)
@@ -6,44 +7,91 @@
 section \<open>Proving equalities in commutative rings\<close>
 
 theory Commutative_Ring
-imports Main
+imports
+  Conversions
+  Algebra_Aux
+  "~~/src/HOL/Library/Code_Target_Numeral"
 begin
 
 text \<open>Syntax of multivariate polynomials (pol) and polynomial expressions.\<close>
 
-datatype 'a pol =
-    Pc 'a
-  | Pinj nat "'a pol"
-  | PX "'a pol" nat "'a pol"
+datatype pol =
+    Pc int
+  | Pinj nat pol
+  | PX pol nat pol
 
-datatype 'a polex =
-    Pol "'a pol"
-  | Add "'a polex" "'a polex"
-  | Sub "'a polex" "'a polex"
-  | Mul "'a polex" "'a polex"
-  | Pow "'a polex" nat
-  | Neg "'a polex"
+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>
 
-primrec Ipol :: "'a::comm_ring_1 list \<Rightarrow> 'a pol \<Rightarrow> 'a"
+context cring begin
+
+definition in_carrier :: "'a list \<Rightarrow> bool" where
+  "in_carrier xs = (\<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
-    "Ipol l (Pc c) = c"
+    "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 * (hd l)^x + Ipol (drop 1 l) Q"
+  | "Ipol l (PX P x Q) = Ipol l P \<otimes> head l (^) x \<oplus> Ipol (drop 1 l) Q"
 
-primrec Ipolex :: "'a::comm_ring_1 list \<Rightarrow> 'a polex \<Rightarrow> 'a"
+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 (Pol P) = Ipol l P"
-  | "Ipolex l (Add P Q) = Ipolex l P + Ipolex l Q"
-  | "Ipolex l (Sub P Q) = Ipolex l P - Ipolex l Q"
-  | "Ipolex l (Mul P Q) = Ipolex l P * Ipolex l Q"
-  | "Ipolex l (Pow p n) = Ipolex l p ^ n"
-  | "Ipolex l (Neg P) = - Ipolex l P"
+    "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> 'a pol \<Rightarrow> 'a pol"
+definition mkPinj :: "nat \<Rightarrow> pol \<Rightarrow> pol"
 where
   "mkPinj x P =
     (case P of
@@ -51,7 +99,7 @@
     | Pinj y P \<Rightarrow> Pinj (x + y) P
     | PX p1 y p2 \<Rightarrow> Pinj x P)"
 
-definition mkPX :: "'a::comm_ring pol \<Rightarrow> nat \<Rightarrow> 'a pol \<Rightarrow> 'a pol"
+definition mkPX :: "pol \<Rightarrow> nat \<Rightarrow> pol \<Rightarrow> pol"
 where
   "mkPX P i Q =
     (case P of
@@ -61,151 +109,154 @@
 
 text \<open>Defining the basic ring operations on normalized polynomials\<close>
 
-lemma pol_size_nz[simp]: "size (p :: 'a pol) \<noteq> 0"
-  by (cases p) simp_all
-
-function add :: "'a::comm_ring pol \<Rightarrow> 'a pol \<Rightarrow> 'a pol"  (infixl "\<oplus>" 65)
+function add :: "pol \<Rightarrow> pol \<Rightarrow> pol"  (infixl "\<langle>+\<rangle>" 65)
 where
-  "Pc a \<oplus> Pc b = Pc (a + b)"
-| "Pc c \<oplus> Pinj i P = Pinj i (P \<oplus> Pc c)"
-| "Pinj i P \<oplus> Pc c = Pinj i (P \<oplus> Pc c)"
-| "Pc c \<oplus> PX P i Q = PX P i (Q \<oplus> Pc c)"
-| "PX P i Q \<oplus> Pc c = PX P i (Q \<oplus> Pc c)"
-| "Pinj x P \<oplus> Pinj y Q =
-    (if x = y then mkPinj x (P \<oplus> Q)
-     else (if x > y then mkPinj y (Pinj (x - y) P \<oplus> Q)
-       else mkPinj x (Pinj (y - x) Q \<oplus> P)))"
-| "Pinj x P \<oplus> PX Q y R =
-    (if x = 0 then P \<oplus> PX Q y R
-     else (if x = 1 then PX Q y (R \<oplus> P)
-       else PX Q y (R \<oplus> Pinj (x - 1) P)))"
-| "PX P x R \<oplus> Pinj y Q =
-    (if y = 0 then PX P x R \<oplus> Q
-     else (if y = 1 then PX P x (R \<oplus> Q)
-       else PX P x (R \<oplus> Pinj (y - 1) Q)))"
-| "PX P1 x P2 \<oplus> PX Q1 y Q2 =
-    (if x = y then mkPX (P1 \<oplus> Q1) x (P2 \<oplus> Q2)
-     else (if x > y then mkPX (PX P1 (x - y) (Pc 0) \<oplus> Q1) y (P2 \<oplus> Q2)
-       else mkPX (PX Q1 (y-x) (Pc 0) \<oplus> P1) x (P2 \<oplus> Q2)))"
+    "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 :: "'a::comm_ring pol \<Rightarrow> 'a pol \<Rightarrow> 'a pol"  (infixl "\<otimes>" 70)
+function mul :: "pol \<Rightarrow> pol \<Rightarrow> pol"  (infixl "\<langle>*\<rangle>" 70)
 where
-  "Pc a \<otimes> Pc b = Pc (a * b)"
-| "Pc c \<otimes> Pinj i P =
-    (if c = 0 then Pc 0 else mkPinj i (P \<otimes> Pc c))"
-| "Pinj i P \<otimes> Pc c =
-    (if c = 0 then Pc 0 else mkPinj i (P \<otimes> Pc c))"
-| "Pc c \<otimes> PX P i Q =
-    (if c = 0 then Pc 0 else mkPX (P \<otimes> Pc c) i (Q \<otimes> Pc c))"
-| "PX P i Q \<otimes> Pc c =
-    (if c = 0 then Pc 0 else mkPX (P \<otimes> Pc c) i (Q \<otimes> Pc c))"
-| "Pinj x P \<otimes> Pinj y Q =
-    (if x = y then mkPinj x (P \<otimes> Q)
-     else
-       (if x > y then mkPinj y (Pinj (x-y) P \<otimes> Q)
-        else mkPinj x (Pinj (y - x) Q \<otimes> P)))"
-| "Pinj x P \<otimes> PX Q y R =
-    (if x = 0 then P \<otimes> PX Q y R
-     else
-       (if x = 1 then mkPX (Pinj x P \<otimes> Q) y (R \<otimes> P)
-        else mkPX (Pinj x P \<otimes> Q) y (R \<otimes> Pinj (x - 1) P)))"
-| "PX P x R \<otimes> Pinj y Q =
-    (if y = 0 then PX P x R \<otimes> Q
-     else
-       (if y = 1 then mkPX (Pinj y Q \<otimes> P) x (R \<otimes> Q)
-        else mkPX (Pinj y Q \<otimes> P) x (R \<otimes> Pinj (y - 1) Q)))"
-| "PX P1 x P2 \<otimes> PX Q1 y Q2 =
-    mkPX (P1 \<otimes> Q1) (x + y) (P2 \<otimes> Q2) \<oplus>
-      (mkPX (P1 \<otimes> mkPinj 1 Q2) x (Pc 0) \<oplus>
-        (mkPX (Q1 \<otimes> mkPinj 1 P2) y (Pc 0)))"
+    "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 :: "'a::comm_ring pol \<Rightarrow> 'a pol"
+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)"
+    "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>Substraction\<close>
-definition sub :: "'a::comm_ring pol \<Rightarrow> 'a pol \<Rightarrow> 'a pol"  (infixl "\<ominus>" 65)
-  where "sub P Q = P \<oplus> 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 Exponentation\<close>
-primrec sqr :: "'a::comm_ring_1 pol \<Rightarrow> 'a pol"
+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) \<oplus> mkPX (Pc (1 + 1) \<otimes> A \<otimes> mkPinj 1 B) x (Pc 0)"
+    "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 Exponentation\<close>
+text \<open>Fast Exponentiation\<close>
 
-fun pow :: "nat \<Rightarrow> 'a::comm_ring_1 pol \<Rightarrow> 'a pol"
+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 \<otimes> 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 \<otimes> 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 \<otimes> pow (n div 2) (sqr P)"
+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 :: "'a::comm_ring_1 polex \<Rightarrow> 'a pol"
+primrec norm :: "polex \<Rightarrow> pol"
 where
-  "norm (Pol P) = P"
-| "norm (Add P Q) = norm P \<oplus> norm Q"
-| "norm (Sub P Q) = norm P \<ominus> norm Q"
-| "norm (Mul P Q) = norm P \<otimes> norm Q"
-| "norm (Pow P n) = pow n (norm P)"
-| "norm (Neg P) = neg (norm P)"
+    "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: "Ipol l (mkPX A b C) = Ipol l (PX A b C)"
-  by (cases A) (auto simp add: mkPX_def mkPinj_ci power_add algebra_simps)
+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: "Ipol l (neg P) = -(Ipol l P)"
-  by (induct P arbitrary: l) auto
+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: "Ipol l (P \<oplus> Q) = Ipol l P + Ipol l Q"
+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
+  then show ?case
   proof cases
     case 1
-    with 6 show ?thesis by (simp add: mkPinj_ci algebra_simps)
+    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 algebra_simps)
+    with 6 show ?thesis by (simp add: mkPinj_ci)
   qed
 next
   case (7 x P Q y R)
@@ -216,14 +267,14 @@
     with 7 show ?thesis by simp
   next
     case 2
-    with 7 show ?thesis by (simp add: algebra_simps)
+    with 7 show ?thesis by (simp add: a_ac)
   next
     case 3
-    from 7 show ?thesis by (cases x) simp_all
+    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
+  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"
@@ -231,80 +282,696 @@
   then show ?case
   proof cases
     case 1
-    with 9 show ?thesis by (simp add: mkPX_ci algebra_simps)
+    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 power_add algebra_simps)
+    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: power_add mkPX_ci algebra_simps)
+    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: algebra_simps)
+qed (auto simp add: a_ac m_ac)
 
 text \<open>Multiplication\<close>
-lemma mul_ci: "Ipol l (P \<otimes> Q) = Ipol l P * Ipol l Q"
+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 algebra_simps add_ci power_add)
+    (simp_all add: mkPX_ci mkPinj_ci a_ac m_ac r_distr add_ci nat_pow_mult [symmetric])
 
-text \<open>Substraction\<close>
-lemma sub_ci: "Ipol l (P \<ominus> Q) = Ipol l P - Ipol l Q"
-  by (simp add: add_ci neg_ci sub_def)
+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: "Ipol ls (sqr P) = Ipol ls P * Ipol ls P"
+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 algebra_simps power_add)
+    (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: "Ipol ls (pow n P) = Ipol ls P ^ n"
+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
+  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)"
+    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 * show ?thesis
-        by (simp add: even_pow sqr_ci power_mult_distrib power_add [symmetric]
+      with * \<open>in_carrier ls\<close> show ?thesis
+        by (simp add: even_pow sqr_ci nat_pow_distr nat_pow_mult
           mult_2 [symmetric] even_two_times_div_two)
     next
       case False
-      with * show ?thesis
-        by (simp add: odd_pow mul_ci sqr_ci power_mult_distrib power_add [symmetric]
-          mult_2 [symmetric] power_Suc [symmetric])
+      with * \<open>in_carrier ls\<close> show ?thesis
+        by (simp add: odd_pow mul_ci sqr_ci nat_pow_distr 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: "Ipolex l Pe = Ipol l (norm Pe)"
+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 "norm P1 = norm P2"
+  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)"
+  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
-  then show ?thesis
-    by (simp only: norm_ci)
+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)"
 
-ML_file "commutative_ring_tac.ML"
+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)
+
+code_reflect Ring_Code
+  datatypes pol = Pc | Pinj | PX
+  and polex = Var | Const | Add | Sub | Mul | Pow | Neg
+  and nat and int
+  functions norm pnsubstl mk_monpol_list
+    Nat.zero_nat_inst.zero_nat Nat.one_nat_inst.one_nat
+    Nat.minus_nat_inst.minus_nat Nat.times_nat_inst.times_nat nat_of_integer integer_of_nat
+    Int.zero_int_inst.zero_int Int.one_int_inst.one_int
+    Int.uminus_int_inst.uminus_int
+    int_of_integer
+    term_of_pol_inst.term_of_pol
+    term_of_polex_inst.term_of_polex
+    equal_pol_inst.equal_pol
+
+definition ring_codegen_aux :: "pol itself" where
+  "ring_codegen_aux = (Code_Evaluation.TERM_OF_EQUAL::pol itself)"
+
+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 extend = I
+  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;
 
-method_setup comm_ring = \<open>
-  Scan.succeed (SIMPLE_METHOD' o Commutative_Ring_Tac.tac)
-\<close> "reflective decision procedure for equalities over commutative rings"
+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 (Proof_Context.theory_of 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 (@{const_name Ring.ring.add}, _) $ R $ _ $ _) = SOME R
+  | ring_struct (Const (@{const_name Ring.a_minus}, _) $ R $ _ $ _) = SOME R
+  | ring_struct (Const (@{const_name Group.monoid.mult}, _) $ R $ _ $ _) = SOME R
+  | ring_struct (Const (@{const_name Ring.a_inv}, _) $ R $ _) = SOME R
+  | ring_struct (Const (@{const_name Group.pow}, _) $ R $ _ $ _) = SOME R
+  | ring_struct (Const (@{const_name Ring.ring.zero}, _) $ R) = SOME R
+  | ring_struct (Const (@{const_name Group.monoid.one}, _) $ R) = SOME R
+  | ring_struct (Const (@{const_name Algebra_Aux.of_integer}, _) $ R $ _) = SOME R
+  | ring_struct _ = NONE;
+
+fun reif_polex vs (Const (@{const_name Ring.ring.add}, _) $ _ $ a $ b) =
+      @{const Add} $ reif_polex vs a $ reif_polex vs b
+  | reif_polex vs (Const (@{const_name Ring.a_minus}, _) $ _ $ a $ b) =
+      @{const Sub} $ reif_polex vs a $ reif_polex vs b
+  | reif_polex vs (Const (@{const_name Group.monoid.mult}, _) $ _ $ a $ b) =
+      @{const Mul} $ reif_polex vs a $ reif_polex vs b
+  | reif_polex vs (Const (@{const_name Ring.a_inv}, _) $ _ $ a) =
+      @{const Neg} $ reif_polex vs a
+  | reif_polex vs (Const (@{const_name Group.pow}, _) $ _ $ a $ n) =
+      @{const Pow} $ reif_polex vs a $ n
+  | reif_polex vs (Free x) =
+      @{const Var} $ HOLogic.mk_number HOLogic.natT (find_index (equal x) vs)
+  | reif_polex vs (Const (@{const_name Ring.ring.zero}, _) $ _) =
+      @{term "Const 0"}
+  | reif_polex vs (Const (@{const_name Group.monoid.one}, _) $ _) =
+      @{term "Const 1"}
+  | reif_polex vs (Const (@{const_name Algebra_Aux.of_integer}, _) $ _ $ n) =
+      @{const Const} $ n
+  | reif_polex _ _ = error "reif_polex: bad expression";
+
+fun reif_polex' vs (Const (@{const_name Groups.plus}, _) $ a $ b) =
+      @{const Add} $ reif_polex' vs a $ reif_polex' vs b
+  | reif_polex' vs (Const (@{const_name Groups.minus}, _) $ a $ b) =
+      @{const Sub} $ reif_polex' vs a $ reif_polex' vs b
+  | reif_polex' vs (Const (@{const_name Groups.times}, _) $ a $ b) =
+      @{const Mul} $ reif_polex' vs a $ reif_polex' vs b
+  | reif_polex' vs (Const (@{const_name Groups.uminus}, _) $ a) =
+      @{const Neg} $ reif_polex' vs a
+  | reif_polex' vs (Const (@{const_name Power.power}, _) $ a $ n) =
+      @{const Pow} $ reif_polex' vs a $ n
+  | reif_polex' vs (Free x) =
+      @{const Var} $ HOLogic.mk_number HOLogic.natT (find_index (equal x) vs)
+  | reif_polex' vs (Const (@{const_name numeral}, _) $ b) =
+      @{const Const} $ (@{const numeral (int)} $ b)
+  | reif_polex' vs (Const (@{const_name zero_class.zero}, _)) = @{term "Const 0"}
+  | reif_polex' vs (Const (@{const_name one_class.one}, _)) = @{term "Const 1"}
+  | reif_polex' vs t = error "reif_polex: bad expression";
+
+fun head_conv (_, _, _, _, head_simp, _) ys =
+  (case strip_app ys of
+     (@{const_name Cons}, [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 Pc}, [c]) => (case strip_numeral c of
+            (@{const_name zero_class.zero}, _) => inst [] [l] Ipol_simps_4
+          | (@{const_name one_class.one}, _) => inst [] [l] Ipol_simps_5
+          | (@{const_name numeral}, [m]) => inst [] [l, m] Ipol_simps_6
+          | (@{const_name uminus}, [m]) => inst [] [l, m] Ipol_simps_7
+          | _ => inst [] [l, c] Ipol_simps_1)
+      | (@{const_name Pinj}, [i, P]) =>
+          transitive'
+            (inst [] [l, i, P] Ipol_simps_2)
+            (cong2' conv (args2 drop_conv_a) Thm.reflexive)
+      | (@{const_name PX}, [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 Var}, [n]) =>
+          transitive'
+            (inst [] [l, n] Ipolex_Var)
+            (cong1' (head_conv rls) (args2 drop_conv_a))
+      | (@{const_name Const}, [i]) => (case strip_app i of
+            (@{const_name zero_class.zero}, _) => inst [] [l] Ipolex_Const_0
+          | (@{const_name one_class.one}, _) => inst [] [l] Ipolex_Const_1
+          | (@{const_name numeral}, [m]) => inst [] [l, m] Ipolex_Const_numeral
+          | _ => inst [] [l, i] Ipolex_Const)
+      | (@{const_name Add}, [P, Q]) =>
+          transitive'
+            (inst [] [l, P, Q] Ipolex_Add)
+            (cong2 (args2 conv) (args2 conv))
+      | (@{const_name Sub}, [P, Q]) =>
+          transitive'
+            (inst [] [l, P, Q] Ipolex_Sub)
+            (cong2 (args2 conv) (args2 conv))
+      | (@{const_name Mul}, [P, Q]) =>
+          transitive'
+            (inst [] [l, P, Q] Ipolex_Mul)
+            (cong2 (args2 conv) (args2 conv))
+      | (@{const_name Pow}, [P, n]) =>
+          transitive'
+            (inst [] [l, P, n] Ipolex_Pow)
+            (cong2 (args2 conv) Thm.reflexive)
+      | (@{const_name Neg}, [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 Nil}, []) => inst [] [l] Ipolex_polex_list_Nil
+   | (@{const_name Cons}, [p, pps']) => (case strip_app p of
+       (@{const_name Pair}, [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 (@{const_name Trueprop}, _) $
+                (Const (@{const_name Set.member}, _) $
+                   Free (y, _) $ (Const (@{const_name carrier}, _) $ S)) =>
+                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 (@{const_name cring_class_ops},
+    Type (@{type_name partial_object_ext}, [T,
+      Type (@{type_name monoid_ext}, [T,
+        Type (@{type_name ring_ext}, [T, @{typ unit}])])]));
+
+val iterations = @{cterm "1000::nat"};
+val Trueprop_cong = Thm.combination (Thm.reflexive @{cterm Trueprop});
+
+val cv = Code_Evaluation.static_conv
+  {ctxt = @{context},
+   consts =
+     [@{const_name pnsubstl},
+      @{const_name norm},
+      @{const_name mk_monpol_list},
+      @{const_name ring_codegen_aux}]};
+
+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 "polex * polex"}
+      (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 R},
+     (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 -r d19a5579ffb8 -r bf41e1109db3 src/HOL/Decision_Procs/Commutative_Ring_Complete.thy
--- a/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy	Sun Jan 29 11:49:48 2017 +0100
+++ b/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy	Sun Jan 29 11:59:48 2017 +0100
@@ -1,8 +1,8 @@
 (*  Author:     Bernhard Haeupler
 
-This theory is about of the relative completeness of method comm-ring
-method.  As long as the reified atomic polynomials of type 'a pol are
-in normal form, the cring method is complete.
+This theory is about of the relative completeness of the ring
+method.  As long as the reified atomic polynomials of type pol are
+in normal form, the ring method is complete.
 *)
 
 section \<open>Proof of the relative completeness of method comm-ring\<close>
@@ -12,7 +12,7 @@
 begin
 
 text \<open>Formalization of normal form\<close>
-fun isnorm :: "'a::comm_ring pol \<Rightarrow> bool"
+fun isnorm :: "pol \<Rightarrow> bool"
 where
   "isnorm (Pc c) \<longleftrightarrow> True"
 | "isnorm (Pinj i (Pc c)) \<longleftrightarrow> False"
@@ -130,7 +130,7 @@
 qed
 
 text \<open>add conserves normalizedness\<close>
-lemma add_cn: "isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<oplus> Q)"
+lemma add_cn: "isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<langle>+\<rangle> Q)"
 proof (induct P Q rule: add.induct)
   case 1
   then show ?case by simp
@@ -219,7 +219,7 @@
     case x: 2
     from 7 have "isnorm R" "isnorm P2"
       by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
-    with 7 x have "isnorm (R \<oplus> P2)"
+    with 7 x have "isnorm (R \<langle>+\<rangle> P2)"
       by simp
     with 7 x show ?thesis
       by (simp add: norm_PXtrans[of Q2 y _])
@@ -229,7 +229,7 @@
       by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
     with 7 x have "isnorm (Pinj (x - 1) P2)"
       by (cases P2) auto
-    with 7 x NR have "isnorm (R \<oplus> Pinj (x - 1) P2)"
+    with 7 x NR have "isnorm (R \<langle>+\<rangle> Pinj (x - 1) P2)"
       by simp
     with \<open>isnorm (PX Q2 y R)\<close> x show ?thesis
       by (simp add: norm_PXtrans[of Q2 y _])
@@ -247,7 +247,7 @@
     case x: 2
     with 8 have "isnorm R" "isnorm P2"
       by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
-    with 8 x have "isnorm (R \<oplus> P2)"
+    with 8 x have "isnorm (R \<langle>+\<rangle> P2)"
       by simp
     with 8 x show ?thesis
       by (simp add: norm_PXtrans[of Q2 y _])
@@ -258,7 +258,7 @@
       by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
     with 8 x have "isnorm (Pinj (x - 1) P2)"
       by (cases P2) auto
-    with 8 x NR have "isnorm (R \<oplus> Pinj (x - 1) P2)"
+    with 8 x NR have "isnorm (R \<langle>+\<rangle> Pinj (x - 1) P2)"
       by simp
     with \<open>isnorm (PX Q2 y R)\<close> x show ?thesis
       by (simp add: norm_PXtrans[of Q2 y _])
@@ -291,13 +291,13 @@
       with 9 xy x show ?thesis
         by (cases d) auto
     qed
-    with 9 NQ1 NP1 NP2 NQ2 xy x have "isnorm (P2 \<oplus> Q2)" "isnorm (PX P1 (x - y) (Pc 0) \<oplus> Q1)"
+    with 9 NQ1 NP1 NP2 NQ2 xy x have "isnorm (P2 \<langle>+\<rangle> Q2)" "isnorm (PX P1 (x - y) (Pc 0) \<langle>+\<rangle> Q1)"
       by auto
     with Y0 xy x show ?thesis
       by (simp add: mkPX_cn)
   next
     case xy: 2
-    with 9 NP1 NP2 NQ1 NQ2 have "isnorm (P2 \<oplus> Q2)" "isnorm (P1 \<oplus> Q1)"
+    with 9 NP1 NP2 NQ1 NQ2 have "isnorm (P2 \<langle>+\<rangle> Q2)" "isnorm (P1 \<langle>+\<rangle> Q1)"
       by auto
     with xy Y0 show ?thesis
       by (simp add: mkPX_cn)
@@ -319,7 +319,7 @@
       with 9 xy y show ?thesis
         by (cases d) auto
     qed
-    with 9 NQ1 NP1 NP2 NQ2 xy y have "isnorm (P2 \<oplus> Q2)" "isnorm (PX Q1 (y - x) (Pc 0) \<oplus> P1)"
+    with 9 NQ1 NP1 NP2 NQ2 xy y have "isnorm (P2 \<langle>+\<rangle> Q2)" "isnorm (PX Q1 (y - x) (Pc 0) \<langle>+\<rangle> P1)"
       by auto
     with X0 xy y show ?thesis
       by (simp add: mkPX_cn)
@@ -327,7 +327,7 @@
 qed
 
 text \<open>mul concerves normalizedness\<close>
-lemma mul_cn: "isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<otimes> Q)"
+lemma mul_cn: "isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<langle>*\<rangle> Q)"
 proof (induct P Q rule: mul.induct)
   case 1
   then show ?case by simp
@@ -426,7 +426,7 @@
     case x: 2
     from 7 have "isnorm R" "isnorm P2"
       by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
-    with 7 x have "isnorm (R \<otimes> P2)" "isnorm Q2"
+    with 7 x have "isnorm (R \<langle>*\<rangle> P2)" "isnorm Q2"
       by (auto simp add: norm_PX1[of Q2 y R])
     with 7 x Y0 show ?thesis
       by (simp add: mkPX_cn)
@@ -436,7 +436,7 @@
       by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R])
     from 7 x have "isnorm (Pinj (x - 1) P2)"
       by (cases P2) auto
-    with 7 x * have "isnorm (R \<otimes> Pinj (x - 1) P2)" "isnorm (Pinj x P2 \<otimes> Q2)"
+    with 7 x * have "isnorm (R \<langle>*\<rangle> Pinj (x - 1) P2)" "isnorm (Pinj x P2 \<langle>*\<rangle> Q2)"
       by auto
     with Y0 x show ?thesis
       by (simp add: mkPX_cn)
@@ -456,7 +456,7 @@
     case x: 2
     from 8 have "isnorm R" "isnorm P2"
       by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
-    with 8 x have "isnorm (R \<otimes> P2)" "isnorm Q2"
+    with 8 x have "isnorm (R \<langle>*\<rangle> P2)" "isnorm Q2"
       by (auto simp add: norm_PX1[of Q2 y R])
     with 8 x Y0 show ?thesis
       by (simp add: mkPX_cn)
@@ -466,7 +466,7 @@
       by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R])
     from 8 x have "isnorm (Pinj (x - 1) P2)"
       by (cases P2) auto
-    with 8 x * have "isnorm (R \<otimes> Pinj (x - 1) P2)" "isnorm (Pinj x P2 \<otimes> Q2)"
+    with 8 x * have "isnorm (R \<langle>*\<rangle> Pinj (x - 1) P2)" "isnorm (Pinj x P2 \<langle>*\<rangle> Q2)"
       by auto
     with Y0 x show ?thesis
       by (simp add: mkPX_cn)
@@ -479,13 +479,13 @@
     by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
   from 9 have "isnorm Q1" "isnorm Q2"
     by (auto simp add: norm_PX1[of Q1 y Q2] norm_PX2[of Q1 y Q2])
-  with 9 * have "isnorm (P1 \<otimes> Q1)" "isnorm (P2 \<otimes> Q2)"
-    "isnorm (P1 \<otimes> mkPinj 1 Q2)" "isnorm (Q1 \<otimes> mkPinj 1 P2)"
+  with 9 * have "isnorm (P1 \<langle>*\<rangle> Q1)" "isnorm (P2 \<langle>*\<rangle> Q2)"
+    "isnorm (P1 \<langle>*\<rangle> mkPinj 1 Q2)" "isnorm (Q1 \<langle>*\<rangle> mkPinj 1 P2)"
     by (auto simp add: mkPinj_cn)
   with 9 X0 Y0 have
-    "isnorm (mkPX (P1 \<otimes> Q1) (x + y) (P2 \<otimes> Q2))"
-    "isnorm (mkPX (P1 \<otimes> mkPinj (Suc 0) Q2) x (Pc 0))"
-    "isnorm (mkPX (Q1 \<otimes> mkPinj (Suc 0) P2) y (Pc 0))"
+    "isnorm (mkPX (P1 \<langle>*\<rangle> Q1) (x + y) (P2 \<langle>*\<rangle> Q2))"
+    "isnorm (mkPX (P1 \<langle>*\<rangle> mkPinj (Suc 0) Q2) x (Pc 0))"
+    "isnorm (mkPX (Q1 \<langle>*\<rangle> mkPinj (Suc 0) P2) y (Pc 0))"
     by (auto simp add: mkPX_cn)
   then show ?case
     by (simp add: add_cn)
@@ -519,7 +519,7 @@
 qed
 
 text \<open>sub conserves normalizedness\<close>
-lemma sub_cn: "isnorm p \<Longrightarrow> isnorm q \<Longrightarrow> isnorm (p \<ominus> q)"
+lemma sub_cn: "isnorm p \<Longrightarrow> isnorm q \<Longrightarrow> isnorm (p \<langle>-\<rangle> q)"
   by (simp add: sub_def add_cn neg_cn)
 
 text \<open>sqr conserves normalizizedness\<close>
@@ -542,7 +542,7 @@
     using PX
     apply (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
     done
-  with PX have "isnorm (mkPX (Pc (1 + 1) \<otimes> P1 \<otimes> mkPinj (Suc 0) P2) x (Pc 0))"
+  with PX have "isnorm (mkPX (Pc (1 + 1) \<langle>*\<rangle> P1 \<langle>*\<rangle> mkPinj (Suc 0) P2) x (Pc 0))"
     and "isnorm (mkPX (sqr P1) (x + x) (sqr P2))"
     by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)
   then show ?case
diff -r d19a5579ffb8 -r bf41e1109db3 src/HOL/Decision_Procs/Conversions.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Decision_Procs/Conversions.thy	Sun Jan 29 11:59:48 2017 +0100
@@ -0,0 +1,844 @@
+(*  Title:      HOL/Decision_Procs/Conversions.thy
+    Author:     Stefan Berghofer
+*)
+
+theory Conversions
+imports Main
+begin
+
+ML {*
+fun tactic_of_conv cv i st =
+  if i > Thm.nprems_of st then Seq.empty
+  else Seq.single (Conv.gconv_rule cv i st);
+
+fun binop_conv cv cv' = Conv.combination_conv (Conv.arg_conv cv) cv';
+*}
+
+ML {*
+fun err s ct =
+   error (s ^ ": " ^ Syntax.string_of_term_global (Thm.theory_of_cterm ct) (Thm.term_of ct));
+*}
+
+attribute_setup meta =
+  {* Scan.succeed (fn (ctxt, th) => (NONE, SOME (mk_meta_eq th))) *}
+  {* convert equality to meta equality *}
+
+ML {*
+fun mk_obj_eq th = th RS @{thm meta_eq_to_obj_eq};
+
+fun strip_app ct = ct |> Drule.strip_comb |>> Thm.term_of |>> dest_Const |>> fst;
+
+fun inst cTs cts th =
+  Thm.instantiate' (map SOME cTs) (map SOME cts) th;
+
+fun transitive' eq eq' = Thm.transitive eq (eq' (Thm.rhs_of eq));
+
+fun type_of_eqn eqn = Thm.ctyp_of_cterm (Thm.dest_arg1 (Thm.cprop_of eqn));
+
+fun cong1 conv ct =
+  Thm.combination (Thm.reflexive (Thm.dest_fun ct)) (conv (Thm.dest_arg ct));
+
+fun cong1' conv' conv ct =
+  let val eqn = conv (Thm.dest_arg ct)
+  in
+    Thm.transitive
+      (Thm.combination (Thm.reflexive (Thm.dest_fun ct)) eqn)
+      (conv' (Thm.rhs_of eqn))
+  end;
+
+fun cong2 conv1 conv2 ct =
+  Thm.combination
+    (Thm.combination
+       (Thm.reflexive (Thm.dest_fun2 ct))
+       (conv1 (Thm.dest_arg1 ct)))
+    (conv2 (Thm.dest_arg ct));
+
+fun cong2' conv conv1 conv2 ct =
+  let
+    val eqn1 = conv1 (Thm.dest_arg1 ct);
+    val eqn2 = conv2 (Thm.dest_arg ct)
+  in
+    Thm.transitive
+      (Thm.combination
+         (Thm.combination (Thm.reflexive (Thm.dest_fun2 ct)) eqn1)
+         eqn2)
+      (conv (Thm.rhs_of eqn1) (Thm.rhs_of eqn2))
+  end;
+
+fun cong2'' conv eqn1 eqn2 =
+  let val eqn3 = conv (Thm.rhs_of eqn1) (Thm.rhs_of eqn2)
+  in
+    Thm.transitive
+      (Thm.combination
+         (Thm.combination (Thm.reflexive (Thm.dest_fun2 (Thm.lhs_of eqn3))) eqn1)
+         eqn2)
+      eqn3
+  end;
+
+fun args1 conv ct = conv (Thm.dest_arg ct);
+fun args2 conv ct = conv (Thm.dest_arg1 ct) (Thm.dest_arg ct);
+*}
+
+ML {*
+fun strip_numeral ct = (case strip_app ct of
+    (@{const_name uminus}, [n]) => (case strip_app n of
+      (@{const_name numeral}, [b]) => (@{const_name uminus}, [b])
+    | _ => ("", []))
+  | x => x);
+*}
+
+lemma nat_minus1_eq: "nat (- 1) = 0"
+  by simp
+
+ML {*
+fun nat_conv i = (case strip_app i of
+    (@{const_name zero_class.zero}, []) => @{thm nat_0 [meta]}
+  | (@{const_name one_class.one}, []) => @{thm transfer_nat_int_numerals(2) [meta, symmetric]}
+  | (@{const_name numeral}, [b]) => inst [] [b] @{thm nat_numeral [meta]}
+  | (@{const_name uminus}, [b]) => (case strip_app b of
+      (@{const_name one_class.one}, []) => @{thm nat_minus1_eq [meta]}
+    | (@{const_name numeral}, [b']) => inst [] [b'] @{thm nat_neg_numeral [meta]}));
+*}
+
+ML {*
+fun add_num_conv b b' = (case (strip_app b, strip_app b') of
+    ((@{const_name Num.One}, []), (@{const_name Num.One}, [])) =>
+      @{thm add_num_simps(1) [meta]}
+  | ((@{const_name Num.One}, []), (@{const_name Num.Bit0}, [n])) =>
+      inst [] [n] @{thm add_num_simps(2) [meta]}
+  | ((@{const_name Num.One}, []), (@{const_name Num.Bit1}, [n])) =>
+      transitive'
+        (inst [] [n] @{thm add_num_simps(3) [meta]})
+        (cong1 (args2 add_num_conv))
+  | ((@{const_name Num.Bit0}, [m]), (@{const_name Num.One}, [])) =>
+      inst [] [m] @{thm add_num_simps(4) [meta]}
+  | ((@{const_name Num.Bit0}, [m]), (@{const_name Num.Bit0}, [n])) =>
+      transitive'
+        (inst [] [m, n] @{thm add_num_simps(5) [meta]})
+        (cong1 (args2 add_num_conv))
+  | ((@{const_name Num.Bit0}, [m]), (@{const_name Num.Bit1}, [n])) =>
+      transitive'
+        (inst [] [m, n] @{thm add_num_simps(6) [meta]})
+        (cong1 (args2 add_num_conv))
+  | ((@{const_name Num.Bit1}, [m]), (@{const_name Num.One}, [])) =>
+      transitive'
+        (inst [] [m] @{thm add_num_simps(7) [meta]})
+        (cong1 (args2 add_num_conv))
+  | ((@{const_name Num.Bit1}, [m]), (@{const_name Num.Bit0}, [n])) =>
+      transitive'
+        (inst [] [m, n] @{thm add_num_simps(8) [meta]})
+        (cong1 (args2 add_num_conv))
+  | ((@{const_name Num.Bit1}, [m]), (@{const_name Num.Bit1}, [n])) =>
+      transitive'
+        (inst [] [m, n] @{thm add_num_simps(9) [meta]})
+        (cong1 (cong2' add_num_conv (args2 add_num_conv) Thm.reflexive)));
+*}
+
+ML {*
+fun BitM_conv m = (case strip_app m of
+    (@{const_name Num.One}, []) => @{thm BitM.simps(1) [meta]}
+  | (@{const_name Num.Bit0}, [n]) =>
+      transitive'
+        (inst [] [n] @{thm BitM.simps(2) [meta]})
+        (cong1 (args1 BitM_conv))
+  | (@{const_name Num.Bit1}, [n]) =>
+      inst [] [n] @{thm BitM.simps(3) [meta]});
+*}
+
+lemma dbl_neg_numeral:
+  "Num.dbl (- Num.numeral k) = - Num.numeral (Num.Bit0 k)"
+  by simp
+
+ML {*
+fun dbl_conv a =
+  let
+    val dbl_neg_numeral_a = inst [a] [] @{thm dbl_neg_numeral [meta]};
+    val dbl_0_a = inst [a] [] @{thm dbl_simps(2) [meta]};
+    val dbl_numeral_a = inst [a] [] @{thm dbl_simps(5) [meta]}
+  in
+    fn n =>
+      case strip_numeral n of
+        (@{const_name zero_class.zero}, []) => dbl_0_a
+      | (@{const_name numeral}, [k]) => inst [] [k] dbl_numeral_a
+      | (@{const_name uminus}, [k]) => inst [] [k] dbl_neg_numeral_a
+  end;
+*}
+
+lemma dbl_inc_neg_numeral:
+  "Num.dbl_inc (- Num.numeral k) = - Num.numeral (Num.BitM k)"
+  by simp
+
+ML {*
+fun dbl_inc_conv a =
+  let
+    val dbl_inc_neg_numeral_a = inst [a] [] @{thm dbl_inc_neg_numeral [meta]};
+    val dbl_inc_0_a = inst [a] [] @{thm dbl_inc_simps(2) [folded numeral_One, meta]};
+    val dbl_inc_numeral_a = inst [a] [] @{thm dbl_inc_simps(5) [meta]};
+  in
+    fn n =>
+      case strip_numeral n of
+        (@{const_name zero_class.zero}, []) => dbl_inc_0_a
+      | (@{const_name numeral}, [k]) => inst [] [k] dbl_inc_numeral_a
+      | (@{const_name uminus}, [k]) =>
+          transitive'
+            (inst [] [k] dbl_inc_neg_numeral_a)
+            (cong1 (cong1 (args1 BitM_conv)))
+  end;
+*}
+
+lemma dbl_dec_neg_numeral:
+  "Num.dbl_dec (- Num.numeral k) = - Num.numeral (Num.Bit1 k)"
+  by simp
+
+ML {*
+fun dbl_dec_conv a =
+  let
+    val dbl_dec_neg_numeral_a = inst [a] [] @{thm dbl_dec_neg_numeral [meta]};
+    val dbl_dec_0_a = inst [a] [] @{thm dbl_dec_simps(2) [folded numeral_One, meta]};
+    val dbl_dec_numeral_a = inst [a] [] @{thm dbl_dec_simps(5) [meta]};
+  in
+    fn n =>
+      case strip_numeral n of
+        (@{const_name zero_class.zero}, []) => dbl_dec_0_a
+      | (@{const_name uminus}, [k]) => inst [] [k] dbl_dec_neg_numeral_a
+      | (@{const_name numeral}, [k]) =>
+          transitive'
+            (inst [] [k] dbl_dec_numeral_a)
+            (cong1 (args1 BitM_conv))
+  end;
+*}
+
+ML {*
+fun sub_conv a =
+  let
+    val [sub_One_One, sub_One_Bit0, sub_One_Bit1,
+         sub_Bit0_One, sub_Bit1_One, sub_Bit0_Bit0,
+         sub_Bit0_Bit1, sub_Bit1_Bit0, sub_Bit1_Bit1] =
+      map (inst [a] []) @{thms sub_num_simps [meta]};
+    val dbl_conv_a = dbl_conv a;
+    val dbl_inc_conv_a = dbl_inc_conv a;
+    val dbl_dec_conv_a = dbl_dec_conv a;
+
+    fun conv m n = (case (strip_app m, strip_app n) of
+        ((@{const_name Num.One}, []), (@{const_name Num.One}, [])) =>
+          sub_One_One
+      | ((@{const_name Num.One}, []), (@{const_name Num.Bit0}, [l])) =>
+          transitive'
+            (inst [] [l] sub_One_Bit0)
+            (cong1 (cong1 (args1 BitM_conv)))
+      | ((@{const_name Num.One}, []), (@{const_name Num.Bit1}, [l])) =>
+          inst [] [l] sub_One_Bit1
+      | ((@{const_name Num.Bit0}, [k]), (@{const_name Num.One}, [])) =>
+          transitive'
+            (inst [] [k] sub_Bit0_One)
+            (cong1 (args1 BitM_conv))
+      | ((@{const_name Num.Bit1}, [k]), (@{const_name Num.One}, [])) =>
+          inst [] [k] sub_Bit1_One
+      | ((@{const_name Num.Bit0}, [k]), (@{const_name Num.Bit0}, [l])) =>
+          transitive'
+            (inst [] [k, l] sub_Bit0_Bit0)
+            (cong1' dbl_conv_a (args2 conv))
+      | ((@{const_name Num.Bit0}, [k]), (@{const_name Num.Bit1}, [l])) =>
+          transitive'
+            (inst [] [k, l] sub_Bit0_Bit1)
+            (cong1' dbl_dec_conv_a (args2 conv))
+      | ((@{const_name Num.Bit1}, [k]), (@{const_name Num.Bit0}, [l])) =>
+          transitive'
+            (inst [] [k, l] sub_Bit1_Bit0)
+            (cong1' dbl_inc_conv_a (args2 conv))
+      | ((@{const_name Num.Bit1}, [k]), (@{const_name Num.Bit1}, [l])) =>
+          transitive'
+            (inst [] [k, l] sub_Bit1_Bit1)
+            (cong1' dbl_conv_a (args2 conv)))
+  in conv end;
+*}
+
+ML {*
+fun expand1 a =
+  let val numeral_1_eq_1_a = inst [a] [] @{thm numeral_One [meta, symmetric]}
+  in
+    fn n =>
+      case Thm.term_of n of
+        Const (@{const_name one_class.one}, _) => numeral_1_eq_1_a
+      | Const (@{const_name uminus}, _) $ Const (@{const_name one_class.one}, _) =>
+          Thm.combination (Thm.reflexive (Thm.dest_fun n)) numeral_1_eq_1_a
+      | Const (@{const_name zero_class.zero}, _) => Thm.reflexive n
+      | Const (@{const_name numeral}, _) $ _ => Thm.reflexive n
+      | Const (@{const_name uminus}, _) $
+          (Const (@{const_name numeral}, _) $ _) => Thm.reflexive n
+      | _ => err "expand1" n
+  end;
+
+fun norm1_eq a =
+  let val numeral_1_eq_1_a = inst [a] [] @{thm numeral_One [meta]}
+  in
+    fn eq =>
+      case Thm.term_of (Thm.rhs_of eq) of
+        Const (@{const_name Num.numeral}, _) $ Const (@{const_name Num.One}, _) =>
+          Thm.transitive eq numeral_1_eq_1_a
+      | Const (@{const_name uminus}, _) $
+          (Const (@{const_name Num.numeral}, _) $ Const (@{const_name Num.One}, _)) =>
+            Thm.transitive eq
+              (Thm.combination (Thm.reflexive (Thm.dest_fun (Thm.rhs_of eq)))
+                 numeral_1_eq_1_a)
+      | _ => eq
+  end;
+*}
+
+ML {*
+fun plus_conv f a =
+  let
+    val add_0_a = inst [a] [] @{thm add_0 [meta]};
+    val add_0_right_a = inst [a] [] @{thm add_0_right [meta]};
+    val numeral_plus_numeral_a = inst [a] [] @{thm numeral_plus_numeral [meta]};
+    val expand1_a = expand1 a;
+
+    fun conv m n = (case (strip_app m, strip_app n) of
+        ((@{const_name zero_class.zero}, []), _) => inst [] [n] add_0_a
+      | (_, (@{const_name zero_class.zero}, [])) => inst [] [m] add_0_right_a
+      | ((@{const_name numeral}, [m]), (@{const_name numeral}, [n])) =>
+          transitive'
+            (inst [] [m, n] numeral_plus_numeral_a)
+            (cong1 (args2 add_num_conv))
+      | _ => cong2'' (f conv) (expand1_a m) (expand1_a n))
+  in f conv end;
+
+val nat_plus_conv = plus_conv I @{ctyp nat};
+*}
+
+lemma neg_numeral_plus_neg_numeral:
+  "- Num.numeral m + - Num.numeral n = (- Num.numeral (m + n) ::'a::neg_numeral)"
+  by simp
+
+ML {*
+fun plus_neg_conv a =
+  let
+    val numeral_plus_neg_numeral_a =
+      inst [a] [] @{thm add_neg_numeral_simps(1) [meta]};
+    val neg_numeral_plus_numeral_a =
+      inst [a] [] @{thm add_neg_numeral_simps(2) [meta]};
+    val neg_numeral_plus_neg_numeral_a =
+      inst [a] [] @{thm neg_numeral_plus_neg_numeral [meta]};
+    val sub_conv_a = sub_conv a;
+  in
+    fn conv => fn m => fn n => 
+      case (strip_numeral m, strip_numeral n) of
+        ((@{const_name Num.numeral}, [m]), (@{const_name uminus}, [n])) =>
+          Thm.transitive
+            (inst [] [m, n] numeral_plus_neg_numeral_a)
+            (sub_conv_a m n)
+      | ((@{const_name uminus}, [m]), (@{const_name Num.numeral}, [n])) =>
+          Thm.transitive
+            (inst [] [m, n] neg_numeral_plus_numeral_a)
+            (sub_conv_a n m)
+      | ((@{const_name uminus}, [m]), (@{const_name uminus}, [n])) =>
+          transitive'
+            (inst [] [m, n] neg_numeral_plus_neg_numeral_a)
+            (cong1 (cong1 (args2 add_num_conv)))
+      | _ => conv m n
+  end;
+
+fun plus_conv' a = norm1_eq a oo plus_conv (plus_neg_conv a) a;
+
+val int_plus_conv = plus_conv' @{ctyp int};
+*}
+
+lemma minus_one: "- 1 = - 1" by simp
+lemma minus_numeral: "- numeral b = - numeral b" by simp
+
+ML {*
+fun uminus_conv a =
+  let
+    val minus_zero_a = inst [a] [] @{thm minus_zero [meta]};
+    val minus_one_a = inst [a] [] @{thm minus_one [meta]};
+    val minus_numeral_a = inst [a] [] @{thm minus_numeral [meta]};
+    val minus_minus_a = inst [a] [] @{thm minus_minus [meta]}
+  in
+    fn n =>
+      case strip_app n of
+        (@{const_name zero_class.zero}, []) => minus_zero_a
+      | (@{const_name one_class.one}, []) => minus_one_a
+      | (@{const_name Num.numeral}, [m]) => inst [] [m] minus_numeral_a
+      | (@{const_name uminus}, [m]) => inst [] [m] minus_minus_a
+  end;
+
+val int_neg_conv = uminus_conv @{ctyp int};
+*}
+
+ML {*
+fun minus_conv a =
+  let
+    val [numeral_minus_numeral_a, numeral_minus_neg_numeral_a,
+         neg_numeral_minus_numeral_a, neg_numeral_minus_neg_numeral_a] =
+      map (inst [a] []) @{thms diff_numeral_simps [meta]};
+    val diff_0_a = inst [a] [] @{thm diff_0 [meta]};
+    val diff_0_right_a = inst [a] [] @{thm diff_0_right [meta]};
+    val sub_conv_a = sub_conv a;
+    val uminus_conv_a = uminus_conv a;
+    val expand1_a = expand1 a;
+    val norm1_eq_a = norm1_eq a;
+
+    fun conv m n = (case (strip_numeral m, strip_numeral n) of
+        ((@{const_name zero_class.zero}, []), _) =>
+          Thm.transitive (inst [] [n] diff_0_a) (uminus_conv_a n)
+      | (_, (@{const_name zero_class.zero}, [])) => inst [] [m] diff_0_right_a
+      | ((@{const_name Num.numeral}, [m]), (@{const_name Num.numeral}, [n])) =>
+          Thm.transitive
+            (inst [] [m, n] numeral_minus_numeral_a)
+            (sub_conv_a m n)
+      | ((@{const_name Num.numeral}, [m]), (@{const_name uminus}, [n])) =>
+          transitive'
+            (inst [] [m, n] numeral_minus_neg_numeral_a)
+            (cong1 (args2 add_num_conv))
+      | ((@{const_name uminus}, [m]), (@{const_name Num.numeral}, [n])) =>
+          transitive'
+            (inst [] [m, n] neg_numeral_minus_numeral_a)
+            (cong1 (cong1 (args2 add_num_conv)))
+      | ((@{const_name uminus}, [m]), (@{const_name uminus}, [n])) =>
+          Thm.transitive
+            (inst [] [m, n] neg_numeral_minus_neg_numeral_a)
+            (sub_conv_a n m)
+      | _ => cong2'' conv (expand1_a m) (expand1_a n))
+  in norm1_eq_a oo conv end;
+
+val int_minus_conv = minus_conv @{ctyp int};
+*}
+
+ML {*
+val int_numeral = Thm.apply @{cterm "numeral :: num \<Rightarrow> int"};
+
+val nat_minus_refl = Thm.reflexive @{cterm "minus :: nat \<Rightarrow> nat \<Rightarrow> nat"};
+
+val expand1_nat = expand1 @{ctyp nat};
+
+fun nat_minus_conv m n = (case (strip_app m, strip_app n) of
+    ((@{const_name zero_class.zero}, []), _) =>
+      inst [] [n] @{thm diff_0_eq_0 [meta]}
+  | (_, (@{const_name zero_class.zero}, [])) =>
+      inst [] [m] @{thm minus_nat.diff_0 [meta]}
+  | ((@{const_name numeral}, [m]), (@{const_name numeral}, [n])) =>
+      transitive'
+        (inst [] [m, n] @{thm diff_nat_numeral [meta]})
+        (cong1' nat_conv (args2 int_minus_conv))
+  | _ => cong2'' nat_minus_conv (expand1_nat m) (expand1_nat n));
+*}
+
+ML {*
+fun mult_num_conv m n = (case (strip_app m, strip_app n) of
+    (_, (@{const_name Num.One}, [])) =>
+      inst [] [m] @{thm mult_num_simps(1) [meta]}
+  | ((@{const_name Num.One}, []), _) =>
+      inst [] [n] @{thm mult_num_simps(2) [meta]}
+  | ((@{const_name Num.Bit0}, [m]), (@{const_name Num.Bit0}, [n])) =>
+      transitive'
+        (inst [] [m, n] @{thm mult_num_simps(3) [meta]})
+        (cong1 (cong1 (args2 mult_num_conv)))
+  | ((@{const_name Num.Bit0}, [m]), (@{const_name Num.Bit1}, [n'])) =>
+      transitive'
+        (inst [] [m, n'] @{thm mult_num_simps(4) [meta]})
+        (cong1 (args2 mult_num_conv))
+  | ((@{const_name Num.Bit1}, [m']), (@{const_name Num.Bit0}, [n])) =>
+      transitive'
+        (inst [] [m', n] @{thm mult_num_simps(5) [meta]})
+        (cong1 (args2 mult_num_conv))
+  | ((@{const_name Num.Bit1}, [m]), (@{const_name Num.Bit1}, [n])) =>
+      transitive'
+        (inst [] [m, n] @{thm mult_num_simps(6) [meta]})
+        (cong1 (cong2' add_num_conv
+           (args2 add_num_conv)
+           (cong1 (args2 mult_num_conv)))));
+*}
+
+ML {*
+fun mult_conv f a =
+  let
+    val mult_zero_left_a = inst [a] [] @{thm mult_zero_left [meta]};
+    val mult_zero_right_a = inst [a] [] @{thm mult_zero_right [meta]};
+    val numeral_times_numeral_a = inst [a] [] @{thm numeral_times_numeral [meta]};
+    val expand1_a = expand1 a;
+    val norm1_eq_a = norm1_eq a;
+
+    fun conv m n = (case (strip_app m, strip_app n) of
+        ((@{const_name zero_class.zero}, []), _) => inst [] [n] mult_zero_left_a
+      | (_, (@{const_name zero_class.zero}, [])) => inst [] [m] mult_zero_right_a
+      | ((@{const_name numeral}, [m]), (@{const_name numeral}, [n])) =>
+          transitive'
+            (inst [] [m, n] numeral_times_numeral_a)
+            (cong1 (args2 mult_num_conv))
+      | _ => cong2'' (f conv) (expand1_a m) (expand1_a n))
+  in norm1_eq_a oo f conv end;
+
+val nat_mult_conv = mult_conv I @{ctyp nat};
+*}
+
+ML {*
+fun mult_neg_conv a =
+  let
+    val [neg_numeral_times_neg_numeral_a, neg_numeral_times_numeral_a,
+         numeral_times_neg_numeral_a] =
+      map (inst [a] []) @{thms mult_neg_numeral_simps [meta]};
+  in
+    fn conv => fn m => fn n =>
+      case (strip_numeral m, strip_numeral n) of
+        ((@{const_name uminus}, [m]), (@{const_name uminus}, [n])) =>
+          transitive'
+            (inst [] [m, n] neg_numeral_times_neg_numeral_a)
+            (cong1 (args2 mult_num_conv))
+      | ((@{const_name uminus}, [m]), (@{const_name numeral}, [n])) =>
+          transitive'
+            (inst [] [m, n] neg_numeral_times_numeral_a)
+            (cong1 (cong1 (args2 mult_num_conv)))
+      | ((@{const_name numeral}, [m]), (@{const_name uminus}, [n])) =>
+          transitive'
+            (inst [] [m, n] numeral_times_neg_numeral_a)
+            (cong1 (cong1 (args2 mult_num_conv)))
+      | _ => conv m n
+  end;
+
+fun mult_conv' a = mult_conv (mult_neg_conv a) a;
+
+val int_mult_conv = mult_conv' @{ctyp int};
+*}
+
+ML {*
+fun eq_num_conv m n = (case (strip_app m, strip_app n) of
+    ((@{const_name Num.One}, []), (@{const_name Num.One}, [])) =>
+      @{thm eq_num_simps(1) [meta]}
+  | ((@{const_name Num.One}, []), (@{const_name Num.Bit0}, [n])) =>
+      inst [] [n] @{thm eq_num_simps(2) [meta]}
+  | ((@{const_name Num.One}, []), (@{const_name Num.Bit1}, [n])) =>
+      inst [] [n] @{thm eq_num_simps(3) [meta]}
+  | ((@{const_name Num.Bit0}, [m]), (@{const_name Num.One}, [])) =>
+      inst [] [m] @{thm eq_num_simps(4) [meta]}
+  | ((@{const_name Num.Bit1}, [m]), (@{const_name Num.One}, [])) =>
+      inst [] [m] @{thm eq_num_simps(5) [meta]}
+  | ((@{const_name Num.Bit0}, [m]), (@{const_name Num.Bit0}, [n])) =>
+      Thm.transitive
+        (inst [] [m, n] @{thm eq_num_simps(6) [meta]})
+        (eq_num_conv m n)
+  | ((@{const_name Num.Bit0}, [m]), (@{const_name Num.Bit1}, [n])) =>
+      inst [] [m, n] @{thm eq_num_simps(7) [meta]}
+  | ((@{const_name Num.Bit1}, [m]), (@{const_name Num.Bit0}, [n])) =>
+      inst [] [m, n] @{thm eq_num_simps(8) [meta]}
+  | ((@{const_name Num.Bit1}, [m]), (@{const_name Num.Bit1}, [n])) =>
+      Thm.transitive
+        (inst [] [m, n] @{thm eq_num_simps(9) [meta]})
+        (eq_num_conv m n));
+*}
+
+ML {*
+fun eq_conv f a =
+  let
+    val zero_eq_zero_a = inst [a] [] @{thm refl [of 0, THEN Eq_TrueI]};
+    val zero_neq_numeral_a =
+      inst [a] [] @{thm zero_neq_numeral [THEN Eq_FalseI]};
+    val numeral_neq_zero_a =
+      inst [a] [] @{thm numeral_neq_zero [THEN Eq_FalseI]};
+    val numeral_eq_iff_a = inst [a] [] @{thm numeral_eq_iff [meta]};
+    val expand1_a = expand1 a;
+
+    fun conv m n = (case (strip_app m, strip_app n) of
+        ((@{const_name zero_class.zero}, []), (@{const_name zero_class.zero}, [])) =>
+          zero_eq_zero_a
+      | ((@{const_name zero_class.zero}, []), (@{const_name numeral}, [n])) =>
+          inst [] [n] zero_neq_numeral_a
+      | ((@{const_name numeral}, [m]), (@{const_name zero_class.zero}, [])) =>
+          inst [] [m] numeral_neq_zero_a
+      | ((@{const_name numeral}, [m]), (@{const_name numeral}, [n])) =>
+          Thm.transitive
+            (inst [] [m, n] numeral_eq_iff_a)
+            (eq_num_conv m n)
+      | _ => cong2'' (f conv) (expand1_a m) (expand1_a n))
+  in f conv end;
+
+val nat_eq_conv = eq_conv I @{ctyp nat};
+*}
+
+ML {*
+fun eq_neg_conv a =
+  let
+    val neg_numeral_neq_zero_a =
+      inst [a] [] @{thm neg_numeral_neq_zero [THEN Eq_FalseI]};
+    val zero_neq_neg_numeral_a =
+      inst [a] [] @{thm zero_neq_neg_numeral [THEN Eq_FalseI]};
+    val neg_numeral_neq_numeral_a =
+      inst [a] [] @{thm neg_numeral_neq_numeral [THEN Eq_FalseI]};
+    val numeral_neq_neg_numeral_a =
+      inst [a] [] @{thm numeral_neq_neg_numeral [THEN Eq_FalseI]};
+    val neg_numeral_eq_iff_a = inst [a] [] @{thm neg_numeral_eq_iff [meta]}
+  in
+    fn conv => fn m => fn n => 
+      case (strip_numeral m, strip_numeral n) of
+        ((@{const_name uminus}, [m]), (@{const_name zero_class.zero}, [])) =>
+          inst [] [m] neg_numeral_neq_zero_a
+      | ((@{const_name zero_class.zero}, []), (@{const_name uminus}, [n])) =>
+          inst [] [n] zero_neq_neg_numeral_a
+      | ((@{const_name Num.numeral}, [m]), (@{const_name uminus}, [n])) =>
+          inst [] [m, n] numeral_neq_neg_numeral_a
+      | ((@{const_name uminus}, [m]), (@{const_name Num.numeral}, [n])) =>
+          inst [] [m, n] neg_numeral_neq_numeral_a
+      | ((@{const_name uminus}, [m]), (@{const_name uminus}, [n])) =>
+          Thm.transitive
+            (inst [] [m, n] neg_numeral_eq_iff_a)
+            (eq_num_conv m n)
+      | _ => conv m n
+  end;
+
+fun eq_conv' a = eq_conv (eq_neg_conv a) a;
+
+val int_eq_conv = eq_conv' @{ctyp int};
+*}
+
+ML {*
+fun le_num_conv m n = (case (strip_app m, strip_app n) of
+    ((@{const_name Num.One}, []), _) =>
+      inst [] [n] @{thm le_num_simps(1) [meta]}
+  | ((@{const_name Num.Bit0}, [m]), (@{const_name Num.One}, [])) =>
+      inst [] [m] @{thm le_num_simps(2) [meta]}
+  | ((@{const_name Num.Bit1}, [m]), (@{const_name Num.One}, [])) =>
+      inst [] [m] @{thm le_num_simps(3) [meta]}
+  | ((@{const_name Num.Bit0}, [m]), (@{const_name Num.Bit0}, [n])) =>
+      Thm.transitive
+        (inst [] [m, n] @{thm le_num_simps(4) [meta]})
+        (le_num_conv m n)
+  | ((@{const_name Num.Bit0}, [m]), (@{const_name Num.Bit1}, [n])) =>
+      Thm.transitive
+        (inst [] [m, n] @{thm le_num_simps(5) [meta]})
+        (le_num_conv m n)
+  | ((@{const_name Num.Bit1}, [m]), (@{const_name Num.Bit1}, [n])) =>
+      Thm.transitive
+        (inst [] [m, n] @{thm le_num_simps(6) [meta]})
+        (le_num_conv m n)
+  | ((@{const_name Num.Bit1}, [m]), (@{const_name Num.Bit0}, [n])) =>
+      Thm.transitive
+        (inst [] [m, n] @{thm le_num_simps(7) [meta]})
+        (less_num_conv m n))
+
+and less_num_conv m n = (case (strip_app m, strip_app n) of
+    (_, (@{const_name Num.One}, [])) =>
+      inst [] [m] @{thm less_num_simps(1) [meta]}
+  | ((@{const_name Num.One}, []), (@{const_name Num.Bit0}, [n])) =>
+      inst [] [n] @{thm less_num_simps(2) [meta]}
+  | ((@{const_name Num.One}, []), (@{const_name Num.Bit1}, [n])) =>
+      inst [] [n] @{thm less_num_simps(3) [meta]}
+  | ((@{const_name Num.Bit0}, [m]), (@{const_name Num.Bit0}, [n])) =>
+      Thm.transitive
+        (inst [] [m, n] @{thm less_num_simps(4) [meta]})
+        (less_num_conv m n)
+  | ((@{const_name Num.Bit0}, [m]), (@{const_name Num.Bit1}, [n])) =>
+      Thm.transitive
+        (inst [] [m, n] @{thm less_num_simps(5) [meta]})
+        (le_num_conv m n)
+  | ((@{const_name Num.Bit1}, [m]), (@{const_name Num.Bit1}, [n])) =>
+      Thm.transitive
+        (inst [] [m, n] @{thm less_num_simps(6) [meta]})
+        (less_num_conv m n)
+  | ((@{const_name Num.Bit1}, [m]), (@{const_name Num.Bit0}, [n])) =>
+      Thm.transitive
+        (inst [] [m, n] @{thm less_num_simps(7) [meta]})
+        (less_num_conv m n));
+*}
+
+ML {*
+fun le_conv f a =
+  let
+    val zero_le_zero_a = inst [a] [] @{thm order_refl [of 0, THEN Eq_TrueI]};
+    val zero_le_numeral_a =
+      inst [a] [] @{thm zero_le_numeral [THEN Eq_TrueI]};
+    val not_numeral_le_zero_a =
+      inst [a] [] @{thm not_numeral_le_zero [THEN Eq_FalseI]};
+    val numeral_le_iff_a = inst [a] [] @{thm numeral_le_iff [meta]};
+    val expand1_a = expand1 a;
+
+    fun conv m n = (case (strip_app m, strip_app n) of
+        ((@{const_name zero_class.zero}, []), (@{const_name zero_class.zero}, [])) =>
+          zero_le_zero_a
+      | ((@{const_name zero_class.zero}, []), (@{const_name numeral}, [n])) =>
+          inst [] [n] zero_le_numeral_a
+      | ((@{const_name numeral}, [m]), (@{const_name zero_class.zero}, [])) =>
+          inst [] [m] not_numeral_le_zero_a
+      | ((@{const_name numeral}, [m]), (@{const_name numeral}, [n])) =>
+          Thm.transitive
+            (inst [] [m, n] numeral_le_iff_a)
+            (le_num_conv m n)
+      | _ => cong2'' (f conv) (expand1_a m) (expand1_a n))
+  in f conv end;
+
+val nat_le_conv = le_conv I @{ctyp nat};
+*}
+
+ML {*
+fun le_neg_conv a =
+  let
+    val neg_numeral_le_zero_a =
+      inst [a] [] @{thm neg_numeral_le_zero [THEN Eq_TrueI]};
+    val not_zero_le_neg_numeral_a =
+      inst [a] [] @{thm not_zero_le_neg_numeral [THEN Eq_FalseI]};
+    val neg_numeral_le_numeral_a =
+      inst [a] [] @{thm neg_numeral_le_numeral [THEN Eq_TrueI]};
+    val not_numeral_le_neg_numeral_a =
+      inst [a] [] @{thm not_numeral_le_neg_numeral [THEN Eq_FalseI]};
+    val neg_numeral_le_iff_a = inst [a] [] @{thm neg_numeral_le_iff [meta]}
+  in
+    fn conv => fn m => fn n => 
+      case (strip_numeral m, strip_numeral n) of
+        ((@{const_name uminus}, [m]), (@{const_name zero_class.zero}, [])) =>
+          inst [] [m] neg_numeral_le_zero_a
+      | ((@{const_name zero_class.zero}, []), (@{const_name uminus}, [n])) =>
+          inst [] [n] not_zero_le_neg_numeral_a
+      | ((@{const_name Num.numeral}, [m]), (@{const_name uminus}, [n])) =>
+          inst [] [m, n] not_numeral_le_neg_numeral_a
+      | ((@{const_name uminus}, [m]), (@{const_name Num.numeral}, [n])) =>
+          inst [] [m, n] neg_numeral_le_numeral_a
+      | ((@{const_name uminus}, [m]), (@{const_name uminus}, [n])) =>
+          Thm.transitive
+            (inst [] [m, n] neg_numeral_le_iff_a)
+            (le_num_conv n m)
+      | _ => conv m n
+  end;
+
+fun le_conv' a = le_conv (le_neg_conv a) a;
+
+val int_le_conv = le_conv' @{ctyp int};
+*}
+
+ML {*
+fun less_conv f a =
+  let
+    val not_zero_less_zero_a = inst [a] [] @{thm less_irrefl [of 0, THEN Eq_FalseI]};
+    val zero_less_numeral_a =
+      inst [a] [] @{thm zero_less_numeral [THEN Eq_TrueI]};
+    val not_numeral_less_zero_a =
+      inst [a] [] @{thm not_numeral_less_zero [THEN Eq_FalseI]};
+    val numeral_less_iff_a = inst [a] [] @{thm numeral_less_iff [meta]};
+    val expand1_a = expand1 a;
+
+    fun conv m n = (case (strip_app m, strip_app n) of
+        ((@{const_name zero_class.zero}, []), (@{const_name zero_class.zero}, [])) =>
+          not_zero_less_zero_a
+      | ((@{const_name zero_class.zero}, []), (@{const_name numeral}, [n])) =>
+          inst [] [n] zero_less_numeral_a
+      | ((@{const_name numeral}, [m]), (@{const_name zero_class.zero}, [])) =>
+          inst [] [m] not_numeral_less_zero_a
+      | ((@{const_name numeral}, [m]), (@{const_name numeral}, [n])) =>
+          Thm.transitive
+            (inst [] [m, n] numeral_less_iff_a)
+            (less_num_conv m n)
+      | _ => cong2'' (f conv) (expand1_a m) (expand1_a n))
+  in f conv end;
+
+val nat_less_conv = less_conv I @{ctyp nat};
+*}
+
+ML {*
+fun less_neg_conv a =
+  let
+    val neg_numeral_less_zero_a =
+      inst [a] [] @{thm neg_numeral_less_zero [THEN Eq_TrueI]};
+    val not_zero_less_neg_numeral_a =
+      inst [a] [] @{thm not_zero_less_neg_numeral [THEN Eq_FalseI]};
+    val neg_numeral_less_numeral_a =
+      inst [a] [] @{thm neg_numeral_less_numeral [THEN Eq_TrueI]};
+    val not_numeral_less_neg_numeral_a =
+      inst [a] [] @{thm not_numeral_less_neg_numeral [THEN Eq_FalseI]};
+    val neg_numeral_less_iff_a = inst [a] [] @{thm neg_numeral_less_iff [meta]}
+  in
+    fn conv => fn m => fn n => 
+      case (strip_numeral m, strip_numeral n) of
+        ((@{const_name uminus}, [m]), (@{const_name zero_class.zero}, [])) =>
+          inst [] [m] neg_numeral_less_zero_a
+      | ((@{const_name zero_class.zero}, []), (@{const_name uminus}, [n])) =>
+          inst [] [n] not_zero_less_neg_numeral_a
+      | ((@{const_name Num.numeral}, [m]), (@{const_name uminus}, [n])) =>
+          inst [] [m, n] not_numeral_less_neg_numeral_a
+      | ((@{const_name uminus}, [m]), (@{const_name Num.numeral}, [n])) =>
+          inst [] [m, n] neg_numeral_less_numeral_a
+      | ((@{const_name uminus}, [m]), (@{const_name uminus}, [n])) =>
+          Thm.transitive
+            (inst [] [m, n] neg_numeral_less_iff_a)
+            (less_num_conv n m)
+      | _ => conv m n
+  end;
+
+fun less_conv' a = less_conv (less_neg_conv a) a;
+
+val int_less_conv = less_conv' @{ctyp int};
+*}
+
+ML {*
+fun If_conv a =
+  let
+    val if_True = inst [a] [] @{thm if_True [meta]};
+    val if_False = inst [a] [] @{thm if_False [meta]}
+  in
+    fn p => fn x => fn y => fn ct =>
+      case strip_app ct of
+        (@{const_name If}, [cb, cx, cy]) =>
+          let
+            val p_eq = p cb
+            val eq = Thm.combination (Thm.reflexive (Thm.dest_fun (Thm.dest_fun2 ct))) p_eq
+          in
+            case Thm.term_of (Thm.rhs_of p_eq) of
+              Const (@{const_name True}, _) =>
+                let
+                  val x_eq = x cx;
+                  val cx = Thm.rhs_of x_eq;
+                in
+                  Thm.transitive
+                    (Thm.combination
+                       (Thm.combination eq x_eq)
+                       (Thm.reflexive cy))
+                    (inst [] [cx, cy] if_True)
+                end
+            | Const (@{const_name False}, _) =>
+                let
+                  val y_eq = y cy;
+                  val cy = Thm.rhs_of y_eq;
+                in
+                  Thm.transitive
+                    (Thm.combination
+                       (Thm.combination eq (Thm.reflexive cx))
+                       y_eq)
+                    (inst [] [cx, cy] if_False)
+                end
+            | _ => err "If_conv" (Thm.rhs_of p_eq)
+          end
+  end;
+*}
+
+ML {*
+fun drop_conv a =
+  let
+    val drop_0_a = inst [a] [] @{thm drop_0 [meta]};
+    val drop_Cons_a = inst [a] [] @{thm drop_Cons' [meta]};
+    val If_conv_a = If_conv (type_of_eqn drop_0_a);
+
+    fun conv n ys = (case Thm.term_of n of
+        Const (@{const_name zero_class.zero}, _) => inst [] [ys] drop_0_a
+      | _ => (case strip_app ys of
+          (@{const_name Cons}, [x, xs]) =>
+            transitive'
+              (inst [] [n, x, xs] drop_Cons_a)
+              (If_conv_a (args2 nat_eq_conv)
+                 Thm.reflexive
+                 (cong2' conv (args2 nat_minus_conv) Thm.reflexive))))
+  in conv end;
+*}
+
+ML {*
+fun nth_conv a =
+  let
+    val nth_Cons_a = inst [a] [] @{thm nth_Cons' [meta]};
+    val If_conv_a = If_conv a;
+
+    fun conv ys n = (case strip_app ys of
+        (@{const_name Cons}, [x, xs]) =>
+          transitive'
+            (inst [] [x, xs, n] nth_Cons_a)
+            (If_conv_a (args2 nat_eq_conv)
+               Thm.reflexive
+               (cong2' conv Thm.reflexive (args2 nat_minus_conv))))
+  in conv end;
+*}
+
+end
diff -r d19a5579ffb8 -r bf41e1109db3 src/HOL/Decision_Procs/Reflective_Field.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Decision_Procs/Reflective_Field.thy	Sun Jan 29 11:59:48 2017 +0100
@@ -0,0 +1,941 @@
+(*  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 add: 1 npepow_correct nat_pow_distr
+      npemul.simps [of "PExpr2 (PPow e n)" "PExpr2 (PPow e' m)"]
+      del: npemul.simps)
+  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]:
+  assumes
+    "x = None \<Longrightarrow> P"
+    "\<And>p q. x = Some (p, q) \<Longrightarrow> P"
+  shows P
+proof (cases x)
+  case None
+  then show ?thesis by (rule assms)
+next
+  case (Some r)
+  then show ?thesis
+    apply (cases r)
+    apply simp
+    by (rule assms)
+qed
+
+fun isin :: "pexpr \<Rightarrow> nat \<Rightarrow> pexpr \<Rightarrow> nat \<Rightarrow> (nat * 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 >= 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''))"
+    "p \<le> n"
+  using assms
+  by (induct e n e' m arbitrary: p e'' rule: isin.induct)
+    (force
+       simp add:
+         nat_pow_distr 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
+
+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_distr 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 [] = True"
+| "nonzero xs (p # ps) = (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 `in_carrier xs` `nonzero xs (Cond e2)`
+  have "feval xs e2 = peval xs (Num e2) \<oslash> peval xs (Denom e2)"
+    by (rule fnorm_correct)
+  moreover from `in_carrier xs` `nonzero xs (Cond e2)`
+  have "peval xs (Denom e2) \<noteq> \<zero>" by (rule fnorm_correct)
+  ultimately have "feval xs e2 \<noteq> \<zero>" using `peval xs (Num e2) \<noteq> \<zero>` `in_carrier xs`
+    by (simp add: divide_eq_0_iff)
+  with `feval xs e1 \<in> carrier R` `feval xs e2 \<in> carrier R`
+  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 `feval xs e \<ominus> feval xs e' = peval xs n \<oslash> peval xs d`
+      `in_carrier xs` `nonzero xs (Cond e')`
+    have "peval xs n \<oslash> peval xs d = \<zero>"
+      by (simp add: fexpr_in_carrier minus_eq r_neg)
+    with `peval xs d \<noteq> \<zero>` `in_carrier xs`
+    show "peval xs n = \<zero>"
+      by (simp add: divide_eq_0_iff)
+  next
+    assume "peval xs n = \<zero>"
+    with `feval xs e \<ominus> feval xs e' = peval xs n \<oslash> peval xs d` `peval xs d \<noteq> \<zero>`
+      `nonzero xs (Cond e)` `nonzero xs (Cond e')` `in_carrier xs`
+    show "feval xs e = feval xs e'"
+      by (simp add: eq_diff0 fexpr_in_carrier)
+  qed
+qed
+
+code_reflect Field_Code
+  datatypes fexpr = FCnst | FVar | FAdd | FSub | FMul | FNeg | FDiv | FPow
+  and pexpr = PExpr1 | PExpr2
+  and pexpr1 = PCnst | PVar | PAdd | PSub | PNeg
+  and pexpr2 = PMul | PPow
+  functions fnorm
+    term_of_fexpr_inst.term_of_fexpr
+    term_of_pexpr_inst.term_of_pexpr
+    equal_pexpr_inst.equal_pexpr
+
+definition field_codegen_aux :: "(pexpr \<times> pexpr list) itself" where
+  "field_codegen_aux = (Code_Evaluation.TERM_OF_EQUAL::(pexpr \<times> pexpr list) itself)"
+
+ML {*
+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 (@{const_name Ring.ring.add}, _) $ R $ _ $ _) = SOME R
+  | field_struct (Const (@{const_name Ring.a_minus}, _) $ R $ _ $ _) = SOME R
+  | field_struct (Const (@{const_name Group.monoid.mult}, _) $ R $ _ $ _) = SOME R
+  | field_struct (Const (@{const_name Ring.a_inv}, _) $ R $ _) = SOME R
+  | field_struct (Const (@{const_name Group.pow}, _) $ R $ _ $ _) = SOME R
+  | field_struct (Const (@{const_name Algebra_Aux.m_div}, _) $ R $ _ $ _) = SOME R
+  | field_struct (Const (@{const_name Ring.ring.zero}, _) $ R) = SOME R
+  | field_struct (Const (@{const_name Group.monoid.one}, _) $ R) = SOME R
+  | field_struct (Const (@{const_name Algebra_Aux.of_integer}, _) $ R $ _) = SOME R
+  | field_struct _ = NONE;
+
+fun reif_fexpr vs (Const (@{const_name Ring.ring.add}, _) $ _ $ a $ b) =
+      @{const FAdd} $ reif_fexpr vs a $ reif_fexpr vs b
+  | reif_fexpr vs (Const (@{const_name Ring.a_minus}, _) $ _ $ a $ b) =
+      @{const FSub} $ reif_fexpr vs a $ reif_fexpr vs b
+  | reif_fexpr vs (Const (@{const_name Group.monoid.mult}, _) $ _ $ a $ b) =
+      @{const FMul} $ reif_fexpr vs a $ reif_fexpr vs b
+  | reif_fexpr vs (Const (@{const_name Ring.a_inv}, _) $ _ $ a) =
+      @{const FNeg} $ reif_fexpr vs a
+  | reif_fexpr vs (Const (@{const_name Group.pow}, _) $ _ $ a $ n) =
+      @{const FPow} $ reif_fexpr vs a $ n
+  | reif_fexpr vs (Const (@{const_name Algebra_Aux.m_div}, _) $ _ $ a $ b) =
+      @{const FDiv} $ reif_fexpr vs a $ reif_fexpr vs b
+  | reif_fexpr vs (Free x) =
+      @{const FVar} $ HOLogic.mk_number HOLogic.natT (find_index (equal x) vs)
+  | reif_fexpr vs (Const (@{const_name Ring.ring.zero}, _) $ _) =
+      @{term "FCnst 0"}
+  | reif_fexpr vs (Const (@{const_name Group.monoid.one}, _) $ _) =
+      @{term "FCnst 1"}
+  | reif_fexpr vs (Const (@{const_name Algebra_Aux.of_integer}, _) $ _ $ n) =
+      @{const FCnst} $ n
+  | reif_fexpr _ _ = error "reif_fexpr: bad expression";
+
+fun reif_fexpr' vs (Const (@{const_name Groups.plus}, _) $ a $ b) =
+      @{const FAdd} $ reif_fexpr' vs a $ reif_fexpr' vs b
+  | reif_fexpr' vs (Const (@{const_name Groups.minus}, _) $ a $ b) =
+      @{const FSub} $ reif_fexpr' vs a $ reif_fexpr' vs b
+  | reif_fexpr' vs (Const (@{const_name Groups.times}, _) $ a $ b) =
+      @{const FMul} $ reif_fexpr' vs a $ reif_fexpr' vs b
+  | reif_fexpr' vs (Const (@{const_name Groups.uminus}, _) $ a) =
+      @{const FNeg} $ reif_fexpr' vs a
+  | reif_fexpr' vs (Const (@{const_name Power.power}, _) $ a $ n) =
+      @{const FPow} $ reif_fexpr' vs a $ n
+  | reif_fexpr' vs (Const (@{const_name divide}, _) $ a $ b) =
+      @{const FDiv} $ reif_fexpr' vs a $ reif_fexpr' vs b
+  | reif_fexpr' vs (Free x) =
+      @{const FVar} $ HOLogic.mk_number HOLogic.natT (find_index (equal x) vs)
+  | reif_fexpr' vs (Const (@{const_name zero_class.zero}, _)) =
+      @{term "FCnst 0"}
+  | reif_fexpr' vs (Const (@{const_name one_class.one}, _)) =
+      @{term "FCnst 1"}
+  | reif_fexpr' vs (Const (@{const_name numeral}, _) $ b) =
+      @{const FCnst} $ (@{const numeral (int)} $ b)
+  | 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 extend = I
+  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 (Proof_Context.theory_of 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 Cons}, [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 FCnst}, [c]) => (case strip_app c of
+            (@{const_name zero_class.zero}, _) => inst [] [xs] feval_simps_9
+          | (@{const_name one_class.one}, _) => inst [] [xs] feval_simps_10
+          | (@{const_name numeral}, [n]) => inst [] [xs, n] feval_simps_11
+          | _ => inst [] [xs, c] feval_simps_1)
+      | (@{const_name FVar}, [n]) =>
+          transitive' (inst [] [xs, n] feval_simps_2) (args2 nth_el_conv')
+      | (@{const_name FAdd}, [a, b]) =>
+          transitive' (inst [] [xs, a, b] feval_simps_3)
+            (cong2 (args2 conv) (args2 conv))
+      | (@{const_name FSub}, [a, b]) =>
+          transitive' (inst [] [xs, a, b] feval_simps_4)
+            (cong2 (args2 conv) (args2 conv))
+      | (@{const_name FMul}, [a, b]) =>
+          transitive' (inst [] [xs, a, b] feval_simps_5)
+            (cong2 (args2 conv) (args2 conv))
+      | (@{const_name FNeg}, [a]) =>
+          transitive' (inst [] [xs, a] feval_simps_6)
+            (cong1 (args2 conv))
+      | (@{const_name FDiv}, [a, b]) =>
+          transitive' (inst [] [xs, a, b] feval_simps_7)
+            (cong2 (args2 conv) (args2 conv))
+      | (@{const_name FPow}, [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 PExpr1}, [e]) => (case strip_app e of
+            (@{const_name PCnst}, [c]) => (case strip_numeral c of
+                (@{const_name zero_class.zero}, _) => inst [] [xs] peval_simps_8
+              | (@{const_name one_class.one}, _) => inst [] [xs] peval_simps_9
+              | (@{const_name numeral}, [n]) => inst [] [xs, n] peval_simps_10
+              | (@{const_name uminus}, [n]) => inst [] [xs, n] peval_simps_11
+              | _ => inst [] [xs, c] peval_simps_1)
+          | (@{const_name PVar}, [n]) =>
+              transitive' (inst [] [xs, n] peval_simps_2) (args2 nth_el_conv')
+          | (@{const_name PAdd}, [a, b]) =>
+              transitive' (inst [] [xs, a, b] peval_simps_3)
+                (cong2 (args2 conv) (args2 conv))
+          | (@{const_name PSub}, [a, b]) =>
+              transitive' (inst [] [xs, a, b] peval_simps_4)
+                (cong2 (args2 conv) (args2 conv))
+          | (@{const_name PNeg}, [a]) =>
+              transitive' (inst [] [xs, a] peval_simps_5)
+                (cong1 (args2 conv)))
+      | (@{const_name PExpr2}, [e]) => (case strip_app e of
+            (@{const_name PMul}, [a, b]) =>
+              transitive' (inst [] [xs, a, b] peval_simps_6)
+                (cong2 (args2 conv) (args2 conv))
+          | (@{const_name PPow}, [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 Nil}, []) => inst [] [xs] nonzero_Nil
+      | (@{const_name Cons}, [p, ps]) => (case Thm.term_of ps of
+            Const (@{const_name Nil}, _) =>
+              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;
+
+val cv = Code_Evaluation.static_conv
+  {ctxt = @{context},
+   consts =
+     [@{const_name nat_of_integer},
+      @{const_name fnorm}, @{const_name field_codegen_aux}]};
+
+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 (@{const_name HOL.eq}, Type (_, [T, _])) $ t $ u)) =>
+            (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 field})
+                 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 fnorm} (Thm.apply (Thm.apply @{cterm FSub} ce) ce'));
+      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,
+          mk_obj_eq fnorm,
+          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
+*}
+
+context field begin
+
+local_setup {*
+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 R},
+     (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}))))
+*}
+
+end
+
+method_setup field = {*
+  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))
+*} "reduce equations over fields to equations over rings"
+
+end
diff -r d19a5579ffb8 -r bf41e1109db3 src/HOL/Decision_Procs/commutative_ring_tac.ML
--- a/src/HOL/Decision_Procs/commutative_ring_tac.ML	Sun Jan 29 11:49:48 2017 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,106 +0,0 @@
-(*  Title:      HOL/Decision_Procs/commutative_ring_tac.ML
-    Author:     Amine Chaieb
-
-Tactic for solving equalities over commutative rings.
-*)
-
-signature COMMUTATIVE_RING_TAC =
-sig
-  val tac: Proof.context -> int -> tactic
-end
-
-structure Commutative_Ring_Tac: COMMUTATIVE_RING_TAC =
-struct
-
-(* Zero and One of the commutative ring *)
-fun cring_zero T = Const (@{const_name Groups.zero}, T);
-fun cring_one T = Const (@{const_name Groups.one}, T);
-
-(* reification functions *)
-(* add two polynom expressions *)
-fun polT t = Type (@{type_name Commutative_Ring.pol}, [t]);
-fun polexT t = Type (@{type_name Commutative_Ring.polex}, [t]);
-
-(* pol *)
-fun pol_Pc t =
-  Const (@{const_name Commutative_Ring.pol.Pc}, t --> polT t);
-fun pol_Pinj t =
-  Const (@{const_name Commutative_Ring.pol.Pinj}, HOLogic.natT --> polT t --> polT t);
-fun pol_PX t =
-  Const (@{const_name Commutative_Ring.pol.PX}, polT t --> HOLogic.natT --> polT t --> polT t);
-
-(* polex *)
-fun polex_add t =
-  Const (@{const_name Commutative_Ring.polex.Add}, polexT t --> polexT t --> polexT t);
-fun polex_sub t =
-  Const (@{const_name Commutative_Ring.polex.Sub}, polexT t --> polexT t --> polexT t);
-fun polex_mul t =
-  Const (@{const_name Commutative_Ring.polex.Mul}, polexT t --> polexT t --> polexT t);
-fun polex_neg t =
-  Const (@{const_name Commutative_Ring.polex.Neg}, polexT t --> polexT t);
-fun polex_pol t =
-  Const (@{const_name Commutative_Ring.polex.Pol}, polT t --> polexT t);
-fun polex_pow t =
-  Const (@{const_name Commutative_Ring.polex.Pow}, polexT t --> HOLogic.natT --> polexT t);
-
-(* reification of polynoms : primitive cring expressions *)
-fun reif_pol T vs (t as Free _) =
-      let
-        val one = @{term "1::nat"};
-        val i = find_index (fn t' => t' = t) vs
-      in
-        if i = 0 then
-          pol_PX T $ (pol_Pc T $ cring_one T) $ one $ (pol_Pc T $ cring_zero T)
-        else
-          pol_Pinj T $ HOLogic.mk_nat i $
-            (pol_PX T $ (pol_Pc T $ cring_one T) $ one $ (pol_Pc T $ cring_zero T))
-        end
-  | reif_pol T _ t = pol_Pc T $ t;
-
-(* reification of polynom expressions *)
-fun reif_polex T vs (Const (@{const_name Groups.plus}, _) $ a $ b) =
-      polex_add T $ reif_polex T vs a $ reif_polex T vs b
-  | reif_polex T vs (Const (@{const_name Groups.minus}, _) $ a $ b) =
-      polex_sub T $ reif_polex T vs a $ reif_polex T vs b
-  | reif_polex T vs (Const (@{const_name Groups.times}, _) $ a $ b) =
-      polex_mul T $ reif_polex T vs a $ reif_polex T vs b
-  | reif_polex T vs (Const (@{const_name Groups.uminus}, _) $ a) =
-      polex_neg T $ reif_polex T vs a
-  | reif_polex T vs (Const (@{const_name Power.power}, _) $ a $ n) =
-      polex_pow T $ reif_polex T vs a $ n
-  | reif_polex T vs t = polex_pol T $ reif_pol T vs t;
-
-(* reification of the equation *)
-val cr_sort = @{sort comm_ring_1};
-
-fun reif_eq ctxt (eq as Const (@{const_name HOL.eq}, Type (@{type_name fun}, [T, _])) $ lhs $ rhs) =
-      if Sign.of_sort (Proof_Context.theory_of ctxt) (T, cr_sort) then
-        let
-          val fs = Misc_Legacy.term_frees eq;
-          val cvs = Thm.cterm_of ctxt (HOLogic.mk_list T fs);
-          val clhs = Thm.cterm_of ctxt (reif_polex T fs lhs);
-          val crhs = Thm.cterm_of ctxt (reif_polex T fs rhs);
-          val ca = Thm.ctyp_of ctxt T;
-        in (ca, cvs, clhs, crhs) end
-      else error ("reif_eq: not an equation over " ^ Syntax.string_of_sort ctxt cr_sort)
-  | reif_eq _ _ = error "reif_eq: not an equation";
-
-(* The cring tactic *)
-(* Attention: You have to make sure that no t^0 is in the goal!! *)
-(* Use simply rewriting t^0 = 1 *)
-val cring_simps =
-  @{thms mkPX_def mkPinj_def sub_def power_add even_iff_mod_2_eq_zero pow_if power_add [symmetric]};
-
-fun tac ctxt = SUBGOAL (fn (g, i) =>
-  let
-    val cring_ctxt = ctxt addsimps cring_simps;  (*FIXME really the full simpset!?*)
-    val (ca, cvs, clhs, crhs) = reif_eq ctxt (HOLogic.dest_Trueprop g);
-    val norm_eq_th = (* may collapse to True *)
-      simplify cring_ctxt (Thm.instantiate' [SOME ca] [SOME clhs, SOME crhs, SOME cvs] @{thm norm_eq});
-  in
-    cut_tac norm_eq_th i
-    THEN (simp_tac cring_ctxt i)
-    THEN TRY(simp_tac cring_ctxt i)
-  end);
-
-end;
diff -r d19a5579ffb8 -r bf41e1109db3 src/HOL/Decision_Procs/ex/Commutative_Ring_Ex.thy
--- a/src/HOL/Decision_Procs/ex/Commutative_Ring_Ex.thy	Sun Jan 29 11:49:48 2017 +0100
+++ b/src/HOL/Decision_Procs/ex/Commutative_Ring_Ex.thy	Sun Jan 29 11:59:48 2017 +0100
@@ -1,49 +1,134 @@
-(*  Author:     Bernhard Haeupler *)
+(*  Title:      HOL/Decision_Procs/ex/Commutative_Ring_Ex.thy
+    Author:     Bernhard Haeupler, Stefan Berghofer
+*)
 
-section \<open>Some examples demonstrating the comm-ring method\<close>
+section \<open>Some examples demonstrating the ring and field methods\<close>
 
 theory Commutative_Ring_Ex
-imports "../Commutative_Ring"
+imports "../Reflective_Field"
 begin
 
-lemma "4*(x::int)^5*y^3*x^2*3 + x*z + 3^5 = 12*x^7*y^3 + z*x + 243"
-  by comm_ring
+lemma "4 * (x::int) ^ 5 * y ^ 3 * x ^ 2 * 3 + x * z + 3 ^ 5 = 12 * x ^ 7 * y ^ 3 + z * x + 243"
+  by ring
+
+lemma (in cring)
+  assumes "x \<in> carrier R" "y \<in> carrier R" "z \<in> carrier R"
+  shows "\<guillemotleft>4\<guillemotright> \<otimes> x (^) (5::nat) \<otimes> y (^) (3::nat) \<otimes> x (^) (2::nat) \<otimes> \<guillemotleft>3\<guillemotright> \<oplus> x \<otimes> z \<oplus> \<guillemotleft>3\<guillemotright> (^) (5::nat) =
+    \<guillemotleft>12\<guillemotright> \<otimes> x (^) (7::nat) \<otimes> y (^) (3::nat) \<oplus> z \<otimes> x \<oplus> \<guillemotleft>243\<guillemotright>"
+  by ring
+
+lemma "((x::int) + y) ^ 2  = x ^ 2 + y ^ 2 + 2 * x * y"
+  by ring
 
-lemma "((x::int) + y)^2  = x^2 + y^2 + 2*x*y"
-  by comm_ring
+lemma (in cring)
+  assumes "x \<in> carrier R" "y \<in> carrier R"
+  shows "(x \<oplus> y) (^) (2::nat)  = x (^) (2::nat) \<oplus> y (^) (2::nat) \<oplus> \<guillemotleft>2\<guillemotright> \<otimes> x \<otimes> y"
+  by ring
+
+lemma "((x::int) + y) ^ 3 = x ^ 3 + y ^ 3 + 3 * x ^ 2 * y + 3 * y ^ 2 * x"
+  by ring
 
-lemma "((x::int) + y)^3  = x^3 + y^3 + 3*x^2*y + 3*y^2*x"
-  by comm_ring
+lemma (in cring)
+  assumes "x \<in> carrier R" "y \<in> carrier R"
+  shows "(x \<oplus> y) (^) (3::nat) =
+    x (^) (3::nat) \<oplus> y (^) (3::nat) \<oplus> \<guillemotleft>3\<guillemotright> \<otimes> x (^) (2::nat) \<otimes> y \<oplus> \<guillemotleft>3\<guillemotright> \<otimes> y (^) (2::nat) \<otimes> x"
+  by ring
+
+lemma "((x::int) - y) ^ 3 = x ^ 3 + 3 * x * y ^ 2 + (- 3) * y * x ^ 2 - y ^ 3"
+  by ring
 
-lemma "((x::int) - y)^3  = x^3 + 3*x*y^2 + (-3)*y*x^2 - y^3"
-  by comm_ring
+lemma (in cring)
+  assumes "x \<in> carrier R" "y \<in> carrier R"
+  shows "(x \<ominus> y) (^) (3::nat) =
+    x (^) (3::nat) \<oplus> \<guillemotleft>3\<guillemotright> \<otimes> x \<otimes> y (^) (2::nat) \<oplus> (\<ominus> \<guillemotleft>3\<guillemotright>) \<otimes> y \<otimes> x (^) (2::nat) \<ominus> y (^) (3::nat)"
+  by ring
+
+lemma "((x::int) - y) ^ 2 = x ^ 2 + y ^ 2 - 2 * x * y"
+  by ring
+
+lemma (in cring)
+  assumes "x \<in> carrier R" "y \<in> carrier R"
+  shows "(x \<ominus> y) (^) (2::nat) = x (^) (2::nat) \<oplus> y (^) (2::nat) \<ominus> \<guillemotleft>2\<guillemotright> \<otimes> x \<otimes> y"
+  by ring
 
-lemma "((x::int) - y)^2  = x^2 + y^2 - 2*x*y"
-  by comm_ring
+lemma " ((a::int) + b + c) ^ 2 = a ^ 2 + b ^ 2 + c ^ 2 + 2 * a * b + 2 * b * c + 2 * a * c"
+  by ring
+
+lemma (in cring)
+  assumes "a \<in> carrier R" "b \<in> carrier R" "c \<in> carrier R"
+  shows " (a \<oplus> b \<oplus> c) (^) (2::nat) =
+    a (^) (2::nat) \<oplus> b (^) (2::nat) \<oplus> c (^) (2::nat) \<oplus> \<guillemotleft>2\<guillemotright> \<otimes> a \<otimes> b \<oplus> \<guillemotleft>2\<guillemotright> \<otimes> b \<otimes> c \<oplus> \<guillemotleft>2\<guillemotright> \<otimes> a \<otimes> c"
+  by ring
 
-lemma " ((a::int) + b + c)^2 = a^2 + b^2 + c^2 + 2*a*b + 2*b*c + 2*a*c"
-  by comm_ring
+lemma "((a::int) - b - c) ^ 2 = a ^ 2 + b ^ 2 + c ^ 2 - 2 * a * b + 2 * b * c - 2 * a * c"
+  by ring
+
+lemma (in cring)
+  assumes "a \<in> carrier R" "b \<in> carrier R" "c \<in> carrier R"
+  shows "(a \<ominus> b \<ominus> c) (^) (2::nat) =
+    a (^) (2::nat) \<oplus> b (^) (2::nat) \<oplus> c (^) (2::nat) \<ominus> \<guillemotleft>2\<guillemotright> \<otimes> a \<otimes> b \<oplus> \<guillemotleft>2\<guillemotright> \<otimes> b \<otimes> c \<ominus> \<guillemotleft>2\<guillemotright> \<otimes> a \<otimes> c"
+  by ring
 
-lemma "((a::int) - b - c)^2 = a^2 + b^2 + c^2 - 2*a*b + 2*b*c - 2*a*c"
-  by comm_ring
+lemma "(a::int) * b + a * c = a * (b + c)"
+  by ring
+
+lemma (in cring)
+  assumes "a \<in> carrier R" "b \<in> carrier R" "c \<in> carrier R"
+  shows "a \<otimes> b \<oplus> a \<otimes> c = a \<otimes> (b \<oplus> c)"
+  by ring
+
+lemma "(a::int) ^ 2 - b ^ 2 = (a - b) * (a + b)"
+  by ring
 
-lemma "(a::int)*b + a*c = a*(b+c)"
-  by comm_ring
+lemma (in cring)
+  assumes "a \<in> carrier R" "b \<in> carrier R"
+  shows "a (^) (2::nat) \<ominus> b (^) (2::nat) = (a \<ominus> b) \<otimes> (a \<oplus> b)"
+  by ring
+
+lemma "(a::int) ^ 3 - b ^ 3 = (a - b) * (a ^ 2 + a * b + b ^ 2)"
+  by ring
 
-lemma "(a::int)^2 - b^2 = (a - b) * (a + b)"
-  by comm_ring
+lemma (in cring)
+  assumes "a \<in> carrier R" "b \<in> carrier R"
+  shows "a (^) (3::nat) \<ominus> b (^) (3::nat) = (a \<ominus> b) \<otimes> (a (^) (2::nat) \<oplus> a \<otimes> b \<oplus> b (^) (2::nat))"
+  by ring
+
+lemma "(a::int) ^ 3 + b ^ 3 = (a + b) * (a ^ 2 - a * b + b ^ 2)"
+  by ring
 
-lemma "(a::int)^3 - b^3 = (a - b) * (a^2 + a*b + b^2)"
-  by comm_ring
+lemma (in cring)
+  assumes "a \<in> carrier R" "b \<in> carrier R"
+  shows "a (^) (3::nat) \<oplus> b (^) (3::nat) = (a \<oplus> b) \<otimes> (a (^) (2::nat) \<ominus> a \<otimes> b \<oplus> b (^) (2::nat))"
+  by ring
 
-lemma "(a::int)^3 + b^3 = (a + b) * (a^2 - a*b + b^2)"
-  by comm_ring
+lemma "(a::int) ^ 4 - b ^ 4 = (a - b) * (a + b) * (a ^ 2 + b ^ 2)"
+  by ring
+
+lemma (in cring)
+  assumes "a \<in> carrier R" "b \<in> carrier R"
+  shows "a (^) (4::nat) \<ominus> b (^) (4::nat) = (a \<ominus> b) \<otimes> (a \<oplus> b) \<otimes> (a (^) (2::nat) \<oplus> b (^) (2::nat))"
+  by ring
 
-lemma "(a::int)^4 - b^4 = (a - b) * (a + b)*(a^2 + b^2)"
-  by comm_ring
+lemma "(a::int) ^ 10 - b ^ 10 =
+  (a - b) * (a ^ 9 + a ^ 8 * b + a ^ 7 * b ^ 2 + a ^ 6 * b ^ 3 + a ^ 5 * b ^ 4 +
+    a ^ 4 * b ^ 5 + a ^ 3 * b ^ 6 + a ^ 2 * b ^ 7 + a * b ^ 8 + b ^ 9)"
+  by ring
 
-lemma "(a::int)^10 - b^10 =
-  (a - b) * (a^9 + a^8*b + a^7*b^2 + a^6*b^3 + a^5*b^4 + a^4*b^5 + a^3*b^6 + a^2*b^7 + a*b^8 + b^9)"
-  by comm_ring
+lemma (in cring)
+  assumes "a \<in> carrier R" "b \<in> carrier R"
+  shows "a (^) (10::nat) \<ominus> b (^) (10::nat) =
+  (a \<ominus> b) \<otimes> (a (^) (9::nat) \<oplus> a (^) (8::nat) \<otimes> b \<oplus> a (^) (7::nat) \<otimes> b (^) (2::nat) \<oplus>
+    a (^) (6::nat) \<otimes> b (^) (3::nat) \<oplus> a (^) (5::nat) \<otimes> b (^) (4::nat) \<oplus>
+    a (^) (4::nat) \<otimes> b (^) (5::nat) \<oplus> a (^) (3::nat) \<otimes> b (^) (6::nat) \<oplus>
+    a (^) (2::nat) \<otimes> b (^) (7::nat) \<oplus> a \<otimes> b (^) (8::nat) \<oplus> b (^) (9::nat))"
+  by ring
+
+lemma "(x::'a::field) \<noteq> 0 \<Longrightarrow> (1 - 1 / x) * x - x + 1 = 0"
+  by field
+
+lemma (in field)
+  assumes "x \<in> carrier R"
+  shows "x \<noteq> \<zero> \<Longrightarrow> (\<one> \<ominus> \<one> \<oslash> x) \<otimes> x \<ominus> x \<oplus> \<one> = \<zero>"
+  by field
 
 end