src/HOL/Decision_Procs/Commutative_Ring.thy
author haftmann
Mon Jun 05 15:59:41 2017 +0200 (2017-06-05)
changeset 66010 2f7d39285a1a
parent 65043 fd753468786f
child 66453 cc19f7ca2ed6
permissions -rw-r--r--
executable domain membership checks
     1 (*  Title:      HOL/Decision_Procs/Commutative_Ring.thy
     2     Author:     Bernhard Haeupler, Stefan Berghofer, and Amine Chaieb
     3 
     4 Proving equalities in commutative rings done "right" in Isabelle/HOL.
     5 *)
     6 
     7 section \<open>Proving equalities in commutative rings\<close>
     8 
     9 theory Commutative_Ring
    10 imports
    11   Conversions
    12   Algebra_Aux
    13   "~~/src/HOL/Library/Code_Target_Numeral"
    14 begin
    15 
    16 text \<open>Syntax of multivariate polynomials (pol) and polynomial expressions.\<close>
    17 
    18 datatype pol =
    19     Pc int
    20   | Pinj nat pol
    21   | PX pol nat pol
    22 
    23 datatype polex =
    24     Var nat
    25   | Const int
    26   | Add polex polex
    27   | Sub polex polex
    28   | Mul polex polex
    29   | Pow polex nat
    30   | Neg polex
    31 
    32 text \<open>Interpretation functions for the shadow syntax.\<close>
    33 
    34 context cring begin
    35 
    36 definition in_carrier :: "'a list \<Rightarrow> bool" where
    37   "in_carrier xs = (\<forall>x\<in>set xs. x \<in> carrier R)"
    38 
    39 lemma in_carrier_Nil: "in_carrier []"
    40   by (simp add: in_carrier_def)
    41 
    42 lemma in_carrier_Cons: "x \<in> carrier R \<Longrightarrow> in_carrier xs \<Longrightarrow> in_carrier (x # xs)"
    43   by (simp add: in_carrier_def)
    44 
    45 lemma drop_in_carrier [simp]: "in_carrier xs \<Longrightarrow> in_carrier (drop n xs)"
    46   using set_drop_subset [of n xs]
    47   by (auto simp add: in_carrier_def)
    48 
    49 primrec head :: "'a list \<Rightarrow> 'a"
    50 where
    51     "head [] = \<zero>"
    52   | "head (x # xs) = x"
    53 
    54 lemma head_closed [simp]: "in_carrier xs \<Longrightarrow> head xs \<in> carrier R"
    55   by (cases xs) (simp_all add: in_carrier_def)
    56 
    57 primrec Ipol :: "'a list \<Rightarrow> pol \<Rightarrow> 'a"
    58 where
    59     "Ipol l (Pc c) = \<guillemotleft>c\<guillemotright>"
    60   | "Ipol l (Pinj i P) = Ipol (drop i l) P"
    61   | "Ipol l (PX P x Q) = Ipol l P \<otimes> head l (^) x \<oplus> Ipol (drop 1 l) Q"
    62 
    63 lemma Ipol_Pc:
    64   "Ipol l (Pc 0) = \<zero>"
    65   "Ipol l (Pc 1) = \<one>"
    66   "Ipol l (Pc (numeral n)) = \<guillemotleft>numeral n\<guillemotright>"
    67   "Ipol l (Pc (- numeral n)) = \<ominus> \<guillemotleft>numeral n\<guillemotright>"
    68   by simp_all
    69 
    70 lemma Ipol_closed [simp]:
    71   "in_carrier l \<Longrightarrow> Ipol l p \<in> carrier R"
    72   by (induct p arbitrary: l) simp_all
    73 
    74 primrec Ipolex :: "'a list \<Rightarrow> polex \<Rightarrow> 'a"
    75 where
    76     "Ipolex l (Var n) = head (drop n l)"
    77   | "Ipolex l (Const i) = \<guillemotleft>i\<guillemotright>"
    78   | "Ipolex l (Add P Q) = Ipolex l P \<oplus> Ipolex l Q"
    79   | "Ipolex l (Sub P Q) = Ipolex l P \<ominus> Ipolex l Q"
    80   | "Ipolex l (Mul P Q) = Ipolex l P \<otimes> Ipolex l Q"
    81   | "Ipolex l (Pow p n) = Ipolex l p (^) n"
    82   | "Ipolex l (Neg P) = \<ominus> Ipolex l P"
    83 
    84 lemma Ipolex_Const:
    85   "Ipolex l (Const 0) = \<zero>"
    86   "Ipolex l (Const 1) = \<one>"
    87   "Ipolex l (Const (numeral n)) = \<guillemotleft>numeral n\<guillemotright>"
    88   by simp_all
    89 
    90 end
    91 
    92 text \<open>Create polynomial normalized polynomials given normalized inputs.\<close>
    93 
    94 definition mkPinj :: "nat \<Rightarrow> pol \<Rightarrow> pol"
    95 where
    96   "mkPinj x P =
    97     (case P of
    98       Pc c \<Rightarrow> Pc c
    99     | Pinj y P \<Rightarrow> Pinj (x + y) P
   100     | PX p1 y p2 \<Rightarrow> Pinj x P)"
   101 
   102 definition mkPX :: "pol \<Rightarrow> nat \<Rightarrow> pol \<Rightarrow> pol"
   103 where
   104   "mkPX P i Q =
   105     (case P of
   106       Pc c \<Rightarrow> if c = 0 then mkPinj 1 Q else PX P i Q
   107     | Pinj j R \<Rightarrow> PX P i Q
   108     | PX P2 i2 Q2 \<Rightarrow> if Q2 = Pc 0 then PX P2 (i + i2) Q else PX P i Q)"
   109 
   110 text \<open>Defining the basic ring operations on normalized polynomials\<close>
   111 
   112 function add :: "pol \<Rightarrow> pol \<Rightarrow> pol"  (infixl "\<langle>+\<rangle>" 65)
   113 where
   114     "Pc a \<langle>+\<rangle> Pc b = Pc (a + b)"
   115   | "Pc c \<langle>+\<rangle> Pinj i P = Pinj i (P \<langle>+\<rangle> Pc c)"
   116   | "Pinj i P \<langle>+\<rangle> Pc c = Pinj i (P \<langle>+\<rangle> Pc c)"
   117   | "Pc c \<langle>+\<rangle> PX P i Q = PX P i (Q \<langle>+\<rangle> Pc c)"
   118   | "PX P i Q \<langle>+\<rangle> Pc c = PX P i (Q \<langle>+\<rangle> Pc c)"
   119   | "Pinj x P \<langle>+\<rangle> Pinj y Q =
   120       (if x = y then mkPinj x (P \<langle>+\<rangle> Q)
   121        else (if x > y then mkPinj y (Pinj (x - y) P \<langle>+\<rangle> Q)
   122          else mkPinj x (Pinj (y - x) Q \<langle>+\<rangle> P)))"
   123   | "Pinj x P \<langle>+\<rangle> PX Q y R =
   124       (if x = 0 then P \<langle>+\<rangle> PX Q y R
   125        else (if x = 1 then PX Q y (R \<langle>+\<rangle> P)
   126          else PX Q y (R \<langle>+\<rangle> Pinj (x - 1) P)))"
   127   | "PX P x R \<langle>+\<rangle> Pinj y Q =
   128       (if y = 0 then PX P x R \<langle>+\<rangle> Q
   129        else (if y = 1 then PX P x (R \<langle>+\<rangle> Q)
   130          else PX P x (R \<langle>+\<rangle> Pinj (y - 1) Q)))"
   131   | "PX P1 x P2 \<langle>+\<rangle> PX Q1 y Q2 =
   132       (if x = y then mkPX (P1 \<langle>+\<rangle> Q1) x (P2 \<langle>+\<rangle> Q2)
   133        else (if x > y then mkPX (PX P1 (x - y) (Pc 0) \<langle>+\<rangle> Q1) y (P2 \<langle>+\<rangle> Q2)
   134          else mkPX (PX Q1 (y - x) (Pc 0) \<langle>+\<rangle> P1) x (P2 \<langle>+\<rangle> Q2)))"
   135 by pat_completeness auto
   136 termination by (relation "measure (\<lambda>(x, y). size x + size y)") auto
   137 
   138 function mul :: "pol \<Rightarrow> pol \<Rightarrow> pol"  (infixl "\<langle>*\<rangle>" 70)
   139 where
   140     "Pc a \<langle>*\<rangle> Pc b = Pc (a * b)"
   141   | "Pc c \<langle>*\<rangle> Pinj i P =
   142       (if c = 0 then Pc 0 else mkPinj i (P \<langle>*\<rangle> Pc c))"
   143   | "Pinj i P \<langle>*\<rangle> Pc c =
   144       (if c = 0 then Pc 0 else mkPinj i (P \<langle>*\<rangle> Pc c))"
   145   | "Pc c \<langle>*\<rangle> PX P i Q =
   146       (if c = 0 then Pc 0 else mkPX (P \<langle>*\<rangle> Pc c) i (Q \<langle>*\<rangle> Pc c))"
   147   | "PX P i Q \<langle>*\<rangle> Pc c =
   148       (if c = 0 then Pc 0 else mkPX (P \<langle>*\<rangle> Pc c) i (Q \<langle>*\<rangle> Pc c))"
   149   | "Pinj x P \<langle>*\<rangle> Pinj y Q =
   150       (if x = y then mkPinj x (P \<langle>*\<rangle> Q)
   151        else
   152          (if x > y then mkPinj y (Pinj (x - y) P \<langle>*\<rangle> Q)
   153           else mkPinj x (Pinj (y - x) Q \<langle>*\<rangle> P)))"
   154   | "Pinj x P \<langle>*\<rangle> PX Q y R =
   155       (if x = 0 then P \<langle>*\<rangle> PX Q y R
   156        else
   157          (if x = 1 then mkPX (Pinj x P \<langle>*\<rangle> Q) y (R \<langle>*\<rangle> P)
   158           else mkPX (Pinj x P \<langle>*\<rangle> Q) y (R \<langle>*\<rangle> Pinj (x - 1) P)))"
   159   | "PX P x R \<langle>*\<rangle> Pinj y Q =
   160       (if y = 0 then PX P x R \<langle>*\<rangle> Q
   161        else
   162          (if y = 1 then mkPX (Pinj y Q \<langle>*\<rangle> P) x (R \<langle>*\<rangle> Q)
   163           else mkPX (Pinj y Q \<langle>*\<rangle> P) x (R \<langle>*\<rangle> Pinj (y - 1) Q)))"
   164   | "PX P1 x P2 \<langle>*\<rangle> PX Q1 y Q2 =
   165       mkPX (P1 \<langle>*\<rangle> Q1) (x + y) (P2 \<langle>*\<rangle> Q2) \<langle>+\<rangle>
   166         (mkPX (P1 \<langle>*\<rangle> mkPinj 1 Q2) x (Pc 0) \<langle>+\<rangle>
   167           (mkPX (Q1 \<langle>*\<rangle> mkPinj 1 P2) y (Pc 0)))"
   168 by pat_completeness auto
   169 termination by (relation "measure (\<lambda>(x, y). size x + size y)")
   170   (auto simp add: mkPinj_def split: pol.split)
   171 
   172 text \<open>Negation\<close>
   173 primrec neg :: "pol \<Rightarrow> pol"
   174 where
   175     "neg (Pc c) = Pc (- c)"
   176   | "neg (Pinj i P) = Pinj i (neg P)"
   177   | "neg (PX P x Q) = PX (neg P) x (neg Q)"
   178 
   179 text \<open>Subtraction\<close>
   180 definition sub :: "pol \<Rightarrow> pol \<Rightarrow> pol"  (infixl "\<langle>-\<rangle>" 65)
   181 where
   182   "sub P Q = P \<langle>+\<rangle> neg Q"
   183 
   184 text \<open>Square for Fast Exponentiation\<close>
   185 primrec sqr :: "pol \<Rightarrow> pol"
   186 where
   187     "sqr (Pc c) = Pc (c * c)"
   188   | "sqr (Pinj i P) = mkPinj i (sqr P)"
   189   | "sqr (PX A x B) = mkPX (sqr A) (x + x) (sqr B) \<langle>+\<rangle>
   190       mkPX (Pc 2 \<langle>*\<rangle> A \<langle>*\<rangle> mkPinj 1 B) x (Pc 0)"
   191 
   192 text \<open>Fast Exponentiation\<close>
   193 
   194 fun pow :: "nat \<Rightarrow> pol \<Rightarrow> pol"
   195 where
   196   pow_if [simp del]: "pow n P =
   197    (if n = 0 then Pc 1
   198     else if even n then pow (n div 2) (sqr P)
   199     else P \<langle>*\<rangle> pow (n div 2) (sqr P))"
   200 
   201 lemma pow_simps [simp]:
   202   "pow 0 P = Pc 1"
   203   "pow (2 * n) P = pow n (sqr P)"
   204   "pow (Suc (2 * n)) P = P \<langle>*\<rangle> pow n (sqr P)"
   205   by (simp_all add: pow_if)
   206 
   207 lemma even_pow: "even n \<Longrightarrow> pow n P = pow (n div 2) (sqr P)"
   208   by (erule evenE) simp
   209 
   210 lemma odd_pow: "odd n \<Longrightarrow> pow n P = P \<langle>*\<rangle> pow (n div 2) (sqr P)"
   211   by (erule oddE) simp
   212 
   213 
   214 text \<open>Normalization of polynomial expressions\<close>
   215 
   216 primrec norm :: "polex \<Rightarrow> pol"
   217 where
   218     "norm (Var n) =
   219        (if n = 0 then PX (Pc 1) 1 (Pc 0)
   220         else Pinj n (PX (Pc 1) 1 (Pc 0)))"
   221   | "norm (Const i) = Pc i"
   222   | "norm (Add P Q) = norm P \<langle>+\<rangle> norm Q"
   223   | "norm (Sub P Q) = norm P \<langle>-\<rangle> norm Q"
   224   | "norm (Mul P Q) = norm P \<langle>*\<rangle> norm Q"
   225   | "norm (Pow P n) = pow n (norm P)"
   226   | "norm (Neg P) = neg (norm P)"
   227 
   228 context cring
   229 begin
   230 
   231 text \<open>mkPinj preserve semantics\<close>
   232 lemma mkPinj_ci: "Ipol l (mkPinj a B) = Ipol l (Pinj a B)"
   233   by (induct B) (auto simp add: mkPinj_def algebra_simps)
   234 
   235 text \<open>mkPX preserves semantics\<close>
   236 lemma mkPX_ci: "in_carrier l \<Longrightarrow> Ipol l (mkPX A b C) = Ipol l (PX A b C)"
   237   by (cases A) (auto simp add: mkPX_def mkPinj_ci nat_pow_mult [symmetric] m_ac)
   238 
   239 text \<open>Correctness theorems for the implemented operations\<close>
   240 
   241 text \<open>Negation\<close>
   242 lemma neg_ci: "in_carrier l \<Longrightarrow> Ipol l (neg P) = \<ominus> (Ipol l P)"
   243   by (induct P arbitrary: l) (auto simp add: minus_add l_minus)
   244 
   245 text \<open>Addition\<close>
   246 lemma add_ci: "in_carrier l \<Longrightarrow> Ipol l (P \<langle>+\<rangle> Q) = Ipol l P \<oplus> Ipol l Q"
   247 proof (induct P Q arbitrary: l rule: add.induct)
   248   case (6 x P y Q)
   249   consider "x < y" | "x = y" | "x > y" by arith
   250   then show ?case
   251   proof cases
   252     case 1
   253     with 6 show ?thesis by (simp add: mkPinj_ci a_ac)
   254   next
   255     case 2
   256     with 6 show ?thesis by (simp add: mkPinj_ci)
   257   next
   258     case 3
   259     with 6 show ?thesis by (simp add: mkPinj_ci)
   260   qed
   261 next
   262   case (7 x P Q y R)
   263   consider "x = 0" | "x = 1" | "x > 1" by arith
   264   then show ?case
   265   proof cases
   266     case 1
   267     with 7 show ?thesis by simp
   268   next
   269     case 2
   270     with 7 show ?thesis by (simp add: a_ac)
   271   next
   272     case 3
   273     with 7 show ?thesis by (cases x) (simp_all add: a_ac)
   274   qed
   275 next
   276   case (8 P x R y Q)
   277   then show ?case by (simp add: a_ac)
   278 next
   279   case (9 P1 x P2 Q1 y Q2)
   280   consider "x = y" | d where "d + x = y" | d where "d + y = x"
   281     by atomize_elim arith
   282   then show ?case
   283   proof cases
   284     case 1
   285     with 9 show ?thesis by (simp add: mkPX_ci r_distr a_ac m_ac)
   286   next
   287     case 2
   288     with 9 show ?thesis by (auto simp add: mkPX_ci nat_pow_mult [symmetric] r_distr a_ac m_ac)
   289   next
   290     case 3
   291     with 9 show ?thesis by (auto simp add: nat_pow_mult [symmetric] mkPX_ci r_distr a_ac m_ac)
   292   qed
   293 qed (auto simp add: a_ac m_ac)
   294 
   295 text \<open>Multiplication\<close>
   296 lemma mul_ci: "in_carrier l \<Longrightarrow> Ipol l (P \<langle>*\<rangle> Q) = Ipol l P \<otimes> Ipol l Q"
   297   by (induct P Q arbitrary: l rule: mul.induct)
   298     (simp_all add: mkPX_ci mkPinj_ci a_ac m_ac r_distr add_ci nat_pow_mult [symmetric])
   299 
   300 text \<open>Subtraction\<close>
   301 lemma sub_ci: "in_carrier l \<Longrightarrow> Ipol l (P \<langle>-\<rangle> Q) = Ipol l P \<ominus> Ipol l Q"
   302   by (simp add: add_ci neg_ci sub_def minus_eq)
   303 
   304 text \<open>Square\<close>
   305 lemma sqr_ci: "in_carrier ls \<Longrightarrow> Ipol ls (sqr P) = Ipol ls P \<otimes> Ipol ls P"
   306   by (induct P arbitrary: ls)
   307     (simp_all add: add_ci mkPinj_ci mkPX_ci mul_ci l_distr r_distr
   308        a_ac m_ac nat_pow_mult [symmetric] of_int_2)
   309 
   310 text \<open>Power\<close>
   311 lemma pow_ci: "in_carrier ls \<Longrightarrow> Ipol ls (pow n P) = Ipol ls P (^) n"
   312 proof (induct n arbitrary: P rule: less_induct)
   313   case (less k)
   314   consider "k = 0" | "k > 0" by arith
   315   then show ?case
   316   proof cases
   317     case 1
   318     then show ?thesis by simp
   319   next
   320     case 2
   321     then have "k div 2 < k" by arith
   322     with less have *: "Ipol ls (pow (k div 2) (sqr P)) = Ipol ls (sqr P) (^) (k div 2)"
   323       by simp
   324     show ?thesis
   325     proof (cases "even k")
   326       case True
   327       with * \<open>in_carrier ls\<close> show ?thesis
   328         by (simp add: even_pow sqr_ci nat_pow_distr nat_pow_mult
   329           mult_2 [symmetric] even_two_times_div_two)
   330     next
   331       case False
   332       with * \<open>in_carrier ls\<close> show ?thesis
   333         by (simp add: odd_pow mul_ci sqr_ci nat_pow_distr nat_pow_mult
   334           mult_2 [symmetric] trans [OF nat_pow_Suc m_comm, symmetric])
   335     qed
   336   qed
   337 qed
   338 
   339 text \<open>Normalization preserves semantics\<close>
   340 lemma norm_ci: "in_carrier l \<Longrightarrow> Ipolex l Pe = Ipol l (norm Pe)"
   341   by (induct Pe) (simp_all add: add_ci sub_ci mul_ci neg_ci pow_ci)
   342 
   343 text \<open>Reflection lemma: Key to the (incomplete) decision procedure\<close>
   344 lemma norm_eq:
   345   assumes "in_carrier l"
   346   and "norm P1 = norm P2"
   347   shows "Ipolex l P1 = Ipolex l P2"
   348 proof -
   349   from assms have "Ipol l (norm P1) = Ipol l (norm P2)" by simp
   350   with assms show ?thesis by (simp only: norm_ci)
   351 qed
   352 
   353 end
   354 
   355 
   356 text \<open>Monomials\<close>
   357 
   358 datatype mon =
   359     Mc int
   360   | Minj nat mon
   361   | MX nat mon
   362 
   363 primrec (in cring)
   364   Imon :: "'a list \<Rightarrow> mon \<Rightarrow> 'a"
   365 where
   366     "Imon l (Mc c) = \<guillemotleft>c\<guillemotright>"
   367   | "Imon l (Minj i M) = Imon (drop i l) M"
   368   | "Imon l (MX x M) = Imon (drop 1 l) M \<otimes> head l (^) x"
   369 
   370 lemma (in cring) Imon_closed [simp]:
   371   "in_carrier l \<Longrightarrow> Imon l m \<in> carrier R"
   372   by (induct m arbitrary: l) simp_all
   373 
   374 definition
   375   mkMinj :: "nat \<Rightarrow> mon \<Rightarrow> mon" where
   376   "mkMinj i M = (case M of
   377        Mc c \<Rightarrow> Mc c
   378      | Minj j M \<Rightarrow> Minj (i + j) M
   379      | _ \<Rightarrow> Minj i M)"
   380 
   381 definition
   382   Minj_pred :: "nat \<Rightarrow> mon \<Rightarrow> mon" where
   383   "Minj_pred i M = (if i = 1 then M else mkMinj (i - 1) M)"
   384 
   385 primrec mkMX :: "nat \<Rightarrow> mon \<Rightarrow> mon"
   386 where
   387   "mkMX i (Mc c) = MX i (Mc c)"
   388 | "mkMX i (Minj j M) = (if j = 0 then mkMX i M else MX i (Minj_pred j M))"
   389 | "mkMX i (MX j M) = MX (i + j) M"
   390 
   391 lemma (in cring) mkMinj_correct:
   392   "Imon l (mkMinj i M) = Imon l (Minj i M)"
   393   by (simp add: mkMinj_def add.commute split: mon.split)
   394 
   395 lemma (in cring) Minj_pred_correct:
   396   "0 < i \<Longrightarrow> Imon (drop 1 l) (Minj_pred i M) = Imon l (Minj i M)"
   397   by (simp add: Minj_pred_def mkMinj_correct)
   398 
   399 lemma (in cring) mkMX_correct:
   400   "in_carrier l \<Longrightarrow> Imon l (mkMX i M) = Imon l M \<otimes> head l (^) i"
   401   by (induct M) (simp_all add: Minj_pred_correct [simplified] nat_pow_mult [symmetric] m_ac split: mon.split)
   402 
   403 fun cfactor :: "pol \<Rightarrow> int \<Rightarrow> pol \<times> pol"
   404 where
   405   "cfactor (Pc c') c = (Pc (c' mod c), Pc (c' div c))"
   406 | "cfactor (Pinj i P) c =
   407      (let (R, S) = cfactor P c
   408       in (mkPinj i R, mkPinj i S))"
   409 | "cfactor (PX P i Q) c =
   410      (let
   411         (R1, S1) = cfactor P c;
   412         (R2, S2) = cfactor Q c
   413       in (mkPX R1 i R2, mkPX S1 i S2))"
   414 
   415 lemma (in cring) cfactor_correct:
   416   "in_carrier l \<Longrightarrow> Ipol l P = Ipol l (fst (cfactor P c)) \<oplus> \<guillemotleft>c\<guillemotright> \<otimes> Ipol l (snd (cfactor P c))"
   417 proof (induct P c arbitrary: l rule: cfactor.induct)
   418   case (1 c' c)
   419   show ?case
   420     by (simp add: of_int_mult [symmetric] of_int_add [symmetric] del: of_int_mult)
   421 next
   422   case (2 i P c)
   423   then show ?case
   424     by (simp add: mkPinj_ci split_beta)
   425 next
   426   case (3 P i Q c)
   427   from 3(1) 3(2) [OF refl prod.collapse] 3(3)
   428   show ?case
   429     by (simp add: mkPX_ci r_distr a_ac m_ac split_beta)
   430 qed
   431 
   432 fun mfactor :: "pol \<Rightarrow> mon \<Rightarrow> pol \<times> pol"
   433 where
   434   "mfactor P (Mc c) = (if c = 1 then (Pc 0, P) else cfactor P c)"
   435 | "mfactor (Pc d) M = (Pc d, Pc 0)"
   436 | "mfactor (Pinj i P) (Minj j M) =
   437      (if i = j then
   438         let (R, S) = mfactor P M
   439         in (mkPinj i R, mkPinj i S)
   440       else if i < j then
   441         let (R, S) = mfactor P (Minj (j - i) M)
   442         in (mkPinj i R, mkPinj i S)
   443       else (Pinj i P, Pc 0))"
   444 | "mfactor (Pinj i P) (MX j M) = (Pinj i P, Pc 0)"
   445 | "mfactor (PX P i Q) (Minj j M) =
   446      (if j = 0 then mfactor (PX P i Q) M
   447       else
   448         let
   449           (R1, S1) = mfactor P (Minj j M);
   450           (R2, S2) = mfactor Q (Minj_pred j M)
   451         in (mkPX R1 i R2, mkPX S1 i S2))"
   452 | "mfactor (PX P i Q) (MX j M) =
   453      (if i = j then
   454         let (R, S) = mfactor P (mkMinj 1 M)
   455         in (mkPX R i Q, S)
   456       else if i < j then
   457         let (R, S) = mfactor P (MX (j - i) M)
   458         in (mkPX R i Q, S)
   459       else
   460         let (R, S) = mfactor P (mkMinj 1 M)
   461         in (mkPX R i Q, mkPX S (i - j) (Pc 0)))"
   462 
   463 lemmas mfactor_induct = mfactor.induct
   464   [case_names Mc Pc_Minj Pc_MX Pinj_Minj Pinj_MX PX_Minj PX_MX]
   465 
   466 lemma (in cring) mfactor_correct:
   467   "in_carrier l \<Longrightarrow>
   468    Ipol l P =
   469    Ipol l (fst (mfactor P M)) \<oplus>
   470    Imon l M \<otimes> Ipol l (snd (mfactor P M))"
   471 proof (induct P M arbitrary: l rule: mfactor_induct)
   472   case (Mc P c)
   473   then show ?case
   474     by (simp add: cfactor_correct)
   475 next
   476   case (Pc_Minj d i M)
   477   then show ?case
   478     by simp
   479 next
   480   case (Pc_MX d i M)
   481   then show ?case
   482     by simp
   483 next
   484   case (Pinj_Minj i P j M)
   485   then show ?case
   486     by (simp add: mkPinj_ci split_beta)
   487 next
   488   case (Pinj_MX i P j M)
   489   then show ?case
   490     by simp
   491 next
   492   case (PX_Minj P i Q j M)
   493   from PX_Minj(1,2) PX_Minj(3) [OF _ refl prod.collapse] PX_Minj(4)
   494   show ?case
   495     by (simp add: mkPX_ci Minj_pred_correct [simplified] r_distr a_ac m_ac split_beta)
   496 next
   497   case (PX_MX P i Q j M)
   498   from \<open>in_carrier l\<close>
   499   have eq1: "(Imon (drop (Suc 0) l) M \<otimes> head l (^) (j - i)) \<otimes>
   500     Ipol l (snd (mfactor P (MX (j - i) M))) \<otimes> head l (^) i =
   501     Imon (drop (Suc 0) l) M \<otimes>
   502     Ipol l (snd (mfactor P (MX (j - i) M))) \<otimes>
   503     (head l (^) (j - i) \<otimes> head l (^) i)"
   504     by (simp add: m_ac)
   505   from \<open>in_carrier l\<close>
   506   have eq2: "(Imon (drop (Suc 0) l) M \<otimes> head l (^) j) \<otimes>
   507     (Ipol l (snd (mfactor P (mkMinj (Suc 0) M))) \<otimes> head l (^) (i - j)) =
   508     Imon (drop (Suc 0) l) M \<otimes>
   509     Ipol l (snd (mfactor P (mkMinj (Suc 0) M))) \<otimes>
   510     (head l (^) (i - j) \<otimes> head l (^) j)"
   511     by (simp add: m_ac)
   512   from PX_MX \<open>in_carrier l\<close> show ?case
   513     by (simp add: mkPX_ci mkMinj_correct l_distr eq1 eq2 split_beta nat_pow_mult)
   514       (simp add: a_ac m_ac)
   515 qed
   516 
   517 primrec mon_of_pol :: "pol \<Rightarrow> mon option"
   518 where
   519   "mon_of_pol (Pc c) = Some (Mc c)"
   520 | "mon_of_pol (Pinj i P) = (case mon_of_pol P of
   521        None \<Rightarrow> None
   522      | Some M \<Rightarrow> Some (mkMinj i M))"
   523 | "mon_of_pol (PX P i Q) =
   524      (if Q = Pc 0 then (case mon_of_pol P of
   525           None \<Rightarrow> None
   526         | Some M \<Rightarrow> Some (mkMX i M))
   527       else None)"
   528 
   529 lemma (in cring) mon_of_pol_correct:
   530   assumes "in_carrier l"
   531   and "mon_of_pol P = Some M"
   532   shows "Ipol l P = Imon l M"
   533   using assms
   534 proof (induct P arbitrary: M l)
   535   case (PX P1 i P2)
   536   from PX(1,3,4)
   537   show ?case
   538     by (auto simp add: mkMinj_correct mkMX_correct split: if_split_asm option.split_asm)
   539 qed (auto simp add: mkMinj_correct split: option.split_asm)
   540 
   541 fun (in cring) Ipolex_polex_list :: "'a list \<Rightarrow> (polex \<times> polex) list \<Rightarrow> bool"
   542 where
   543   "Ipolex_polex_list l [] = True"
   544 | "Ipolex_polex_list l ((P, Q) # pps) = ((Ipolex l P = Ipolex l Q) \<and> Ipolex_polex_list l pps)"
   545 
   546 fun (in cring) Imon_pol_list :: "'a list \<Rightarrow> (mon \<times> pol) list \<Rightarrow> bool"
   547 where
   548   "Imon_pol_list l [] = True"
   549 | "Imon_pol_list l ((M, P) # mps) = ((Imon l M = Ipol l P) \<and> Imon_pol_list l mps)"
   550 
   551 fun mk_monpol_list :: "(polex \<times> polex) list \<Rightarrow> (mon \<times> pol) list"
   552 where
   553   "mk_monpol_list [] = []"
   554 | "mk_monpol_list ((P, Q) # pps) =
   555      (case mon_of_pol (norm P) of
   556         None \<Rightarrow> mk_monpol_list pps
   557       | Some M \<Rightarrow> (M, norm Q) # mk_monpol_list pps)"
   558 
   559 lemma (in cring) mk_monpol_list_correct:
   560   "in_carrier l \<Longrightarrow> Ipolex_polex_list l pps \<Longrightarrow> Imon_pol_list l (mk_monpol_list pps)"
   561   by (induct pps rule: mk_monpol_list.induct)
   562     (auto split: option.split
   563        simp add: norm_ci [symmetric] mon_of_pol_correct [symmetric])
   564 
   565 definition ponesubst :: "pol \<Rightarrow> mon \<Rightarrow> pol \<Rightarrow> pol option" where
   566   "ponesubst P1 M P2 =
   567      (let (Q, R) = mfactor P1 M
   568       in case R of
   569           Pc c \<Rightarrow> if c = 0 then None else Some (add Q (mul P2 R))
   570         | _ \<Rightarrow> Some (add Q (mul P2 R)))"
   571 
   572 fun pnsubst1 :: "pol \<Rightarrow> mon \<Rightarrow> pol \<Rightarrow> nat \<Rightarrow> pol"
   573 where
   574   "pnsubst1 P1 M P2 n = (case ponesubst P1 M P2 of
   575        None \<Rightarrow> P1
   576      | Some P3 \<Rightarrow> if n = 0 then P3 else pnsubst1 P3 M P2 (n - 1))"
   577 
   578 lemma pnsubst1_0 [simp]: "pnsubst1 P1 M P2 0 = (case ponesubst P1 M P2 of
   579   None \<Rightarrow> P1 | Some P3 \<Rightarrow> P3)"
   580   by (simp split: option.split)
   581 
   582 lemma pnsubst1_Suc [simp]: "pnsubst1 P1 M P2 (Suc n) = (case ponesubst P1 M P2 of
   583   None \<Rightarrow> P1 | Some P3 \<Rightarrow> pnsubst1 P3 M P2 n)"
   584   by (simp split: option.split)
   585 
   586 declare pnsubst1.simps [simp del]
   587 
   588 definition pnsubst :: "pol \<Rightarrow> mon \<Rightarrow> pol \<Rightarrow> nat \<Rightarrow> pol option" where
   589   "pnsubst P1 M P2 n = (case ponesubst P1 M P2 of
   590        None \<Rightarrow> None
   591      | Some P3 \<Rightarrow> Some (pnsubst1 P3 M P2 n))"
   592 
   593 fun psubstl1 :: "pol \<Rightarrow> (mon \<times> pol) list \<Rightarrow> nat \<Rightarrow> pol"
   594 where
   595   "psubstl1 P1 [] n = P1"
   596 | "psubstl1 P1 ((M, P2) # mps) n = psubstl1 (pnsubst1 P1 M P2 n) mps n"
   597 
   598 fun psubstl :: "pol \<Rightarrow> (mon \<times> pol) list \<Rightarrow> nat \<Rightarrow> pol option"
   599 where
   600   "psubstl P1 [] n = None"
   601 | "psubstl P1 ((M, P2) # mps) n = (case pnsubst P1 M P2 n of
   602        None \<Rightarrow> psubstl P1 mps n
   603      | Some P3 \<Rightarrow> Some (psubstl1 P3 mps n))"
   604 
   605 fun pnsubstl :: "pol \<Rightarrow> (mon \<times> pol) list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> pol"
   606 where
   607   "pnsubstl P1 mps m n = (case psubstl P1 mps n of
   608        None \<Rightarrow> P1
   609      | Some P3 \<Rightarrow> if m = 0 then P3 else pnsubstl P3 mps (m - 1) n)"
   610 
   611 lemma pnsubstl_0 [simp]: "pnsubstl P1 mps 0 n = (case psubstl P1 mps n of
   612   None \<Rightarrow> P1 | Some P3 \<Rightarrow> P3)"
   613   by (simp split: option.split)
   614 
   615 lemma pnsubstl_Suc [simp]: "pnsubstl P1 mps (Suc m) n = (case psubstl P1 mps n of
   616   None \<Rightarrow> P1 | Some P3 \<Rightarrow> pnsubstl P3 mps m n)"
   617   by (simp split: option.split)
   618 
   619 declare pnsubstl.simps [simp del]
   620 
   621 lemma (in cring) ponesubst_correct:
   622   "in_carrier l \<Longrightarrow> ponesubst P1 M P2 = Some P3 \<Longrightarrow> Imon l M = Ipol l P2 \<Longrightarrow> Ipol l P1 = Ipol l P3"
   623   by (auto simp add: ponesubst_def split_beta mfactor_correct [of l P1 M]
   624     add_ci mul_ci split: pol.split_asm if_split_asm)
   625 
   626 lemma (in cring) pnsubst1_correct:
   627   "in_carrier l \<Longrightarrow> Imon l M = Ipol l P2 \<Longrightarrow> Ipol l (pnsubst1 P1 M P2 n) = Ipol l P1"
   628   by (induct n arbitrary: P1)
   629     (simp_all add: ponesubst_correct split: option.split)
   630 
   631 lemma (in cring) pnsubst_correct:
   632   "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"
   633   by (auto simp add: pnsubst_def
   634     pnsubst1_correct ponesubst_correct split: option.split_asm)
   635 
   636 lemma (in cring) psubstl1_correct:
   637   "in_carrier l \<Longrightarrow> Imon_pol_list l mps \<Longrightarrow> Ipol l (psubstl1 P1 mps n) = Ipol l P1"
   638   by (induct P1 mps n rule: psubstl1.induct) (simp_all add: pnsubst1_correct)
   639 
   640 lemma (in cring) psubstl_correct:
   641   "in_carrier l \<Longrightarrow> psubstl P1 mps n = Some P2 \<Longrightarrow> Imon_pol_list l mps \<Longrightarrow> Ipol l P1 = Ipol l P2"
   642   by (induct P1 mps n rule: psubstl.induct)
   643     (auto simp add: psubstl1_correct pnsubst_correct split: option.split_asm)
   644 
   645 lemma (in cring) pnsubstl_correct:
   646   "in_carrier l \<Longrightarrow> Imon_pol_list l mps \<Longrightarrow> Ipol l (pnsubstl P1 mps m n) = Ipol l P1"
   647   by (induct m arbitrary: P1)
   648     (simp_all add: psubstl_correct split: option.split)
   649 
   650 lemma (in cring) norm_subst_correct:
   651   "in_carrier l \<Longrightarrow> Ipolex_polex_list l pps \<Longrightarrow>
   652    Ipolex l P = Ipol l (pnsubstl (norm P) (mk_monpol_list pps) m n)"
   653   by (simp add: pnsubstl_correct mk_monpol_list_correct norm_ci)
   654 
   655 lemma in_carrier_trivial: "cring_class.in_carrier l"
   656   by (induct l) (simp_all add: cring_class.in_carrier_def carrier_class)
   657 
   658 ML \<open>
   659 val term_of_nat = HOLogic.mk_number @{typ nat} o @{code integer_of_nat};
   660 
   661 val term_of_int = HOLogic.mk_number @{typ int} o @{code integer_of_int};
   662 
   663 fun term_of_pol (@{code Pc} k) = @{term Pc} $ term_of_int k
   664   | term_of_pol (@{code Pinj} (n, p)) = @{term Pinj} $ term_of_nat n $ term_of_pol p
   665   | term_of_pol (@{code PX} (p, n, q)) = @{term PX} $ term_of_pol p $ term_of_nat n $ term_of_pol q;
   666 
   667 local
   668 
   669 fun pol (ctxt, ct, t) = Thm.mk_binop @{cterm "Pure.eq :: pol \<Rightarrow> pol \<Rightarrow> prop"}
   670   ct (Thm.cterm_of ctxt t);
   671 
   672 val (_, raw_pol_oracle) = Context.>>> (Context.map_theory_result
   673   (Thm.add_oracle (@{binding pnsubstl}, pol)));
   674 
   675 fun pol_oracle ctxt ct t = raw_pol_oracle (ctxt, ct, t);
   676 
   677 in
   678 
   679 val cv = @{computation_conv pol
   680   terms: pnsubstl mk_monpol_list norm
   681     nat_of_integer Code_Target_Nat.natural
   682       "0::nat" "1::nat" "2::nat" "3::nat"
   683       "0::int" "1::int" "2::int" "3::int" "-1::int"
   684   datatypes: polex "(polex * polex) list" int integer num}
   685   (fn ctxt => fn p => fn ct => pol_oracle ctxt ct (term_of_pol p))
   686 
   687 end
   688 \<close>
   689 
   690 ML \<open>
   691 signature RING_TAC =
   692 sig
   693   structure Ring_Simps:
   694   sig
   695     type T
   696     val get: Context.generic -> T
   697     val put: T -> Context.generic -> Context.generic
   698     val map: (T -> T) -> Context.generic -> Context.generic
   699   end
   700   val insert_rules: ((term * 'a) * (term * 'a) -> bool) -> (term * 'a) ->
   701     (term * 'a) Net.net -> (term * 'a) Net.net
   702   val eq_ring_simps:
   703     (term * (thm list * thm list * thm list * thm list * thm * thm)) *
   704     (term * (thm list * thm list * thm list * thm list * thm * thm)) -> bool
   705   val ring_tac: bool -> thm list -> Proof.context -> int -> tactic
   706   val get_matching_rules: Proof.context -> (term * 'a) Net.net -> term -> 'a option
   707   val norm: thm -> thm
   708   val mk_in_carrier: Proof.context -> term -> thm list -> (string * typ) list -> thm
   709   val mk_ring: typ -> term
   710 end
   711 
   712 structure Ring_Tac : RING_TAC =
   713 struct
   714 
   715 fun eq_ring_simps
   716   ((t, (ths1, ths2, ths3, ths4, th5, th)),
   717    (t', (ths1', ths2', ths3', ths4', th5', th'))) =
   718     t aconv t' andalso
   719     eq_list Thm.eq_thm (ths1, ths1') andalso
   720     eq_list Thm.eq_thm (ths2, ths2') andalso
   721     eq_list Thm.eq_thm (ths3, ths3') andalso
   722     eq_list Thm.eq_thm (ths4, ths4') andalso
   723     Thm.eq_thm (th5, th5') andalso
   724     Thm.eq_thm (th, th');
   725 
   726 structure Ring_Simps = Generic_Data
   727 (struct
   728   type T = (term * (thm list * thm list * thm list * thm list * thm * thm)) Net.net
   729   val empty = Net.empty
   730   val extend = I
   731   val merge = Net.merge eq_ring_simps
   732 end);
   733 
   734 fun get_matching_rules ctxt net t = get_first
   735   (fn (p, x) =>
   736      if Pattern.matches (Proof_Context.theory_of ctxt) (p, t) then SOME x else NONE)
   737   (Net.match_term net t);
   738 
   739 fun insert_rules eq (t, x) = Net.insert_term eq (t, (t, x));
   740 
   741 fun norm thm = thm COMP_INCR asm_rl;
   742 
   743 fun get_ring_simps ctxt optcT t =
   744   (case get_matching_rules ctxt (Ring_Simps.get (Context.Proof ctxt)) t of
   745      SOME (ths1, ths2, ths3, ths4, th5, th) =>
   746        let val tr =
   747          Thm.transfer (Proof_Context.theory_of ctxt) #>
   748          (case optcT of NONE => I | SOME cT => inst [cT] [] #> norm)
   749        in (map tr ths1, map tr ths2, map tr ths3, map tr ths4, tr th5, tr th) end
   750    | NONE => error "get_ring_simps: lookup failed");
   751 
   752 fun ring_struct (Const (@{const_name Ring.ring.add}, _) $ R $ _ $ _) = SOME R
   753   | ring_struct (Const (@{const_name Ring.a_minus}, _) $ R $ _ $ _) = SOME R
   754   | ring_struct (Const (@{const_name Group.monoid.mult}, _) $ R $ _ $ _) = SOME R
   755   | ring_struct (Const (@{const_name Ring.a_inv}, _) $ R $ _) = SOME R
   756   | ring_struct (Const (@{const_name Group.pow}, _) $ R $ _ $ _) = SOME R
   757   | ring_struct (Const (@{const_name Ring.ring.zero}, _) $ R) = SOME R
   758   | ring_struct (Const (@{const_name Group.monoid.one}, _) $ R) = SOME R
   759   | ring_struct (Const (@{const_name Algebra_Aux.of_integer}, _) $ R $ _) = SOME R
   760   | ring_struct _ = NONE;
   761 
   762 fun reif_polex vs (Const (@{const_name Ring.ring.add}, _) $ _ $ a $ b) =
   763       @{const Add} $ reif_polex vs a $ reif_polex vs b
   764   | reif_polex vs (Const (@{const_name Ring.a_minus}, _) $ _ $ a $ b) =
   765       @{const Sub} $ reif_polex vs a $ reif_polex vs b
   766   | reif_polex vs (Const (@{const_name Group.monoid.mult}, _) $ _ $ a $ b) =
   767       @{const Mul} $ reif_polex vs a $ reif_polex vs b
   768   | reif_polex vs (Const (@{const_name Ring.a_inv}, _) $ _ $ a) =
   769       @{const Neg} $ reif_polex vs a
   770   | reif_polex vs (Const (@{const_name Group.pow}, _) $ _ $ a $ n) =
   771       @{const Pow} $ reif_polex vs a $ n
   772   | reif_polex vs (Free x) =
   773       @{const Var} $ HOLogic.mk_number HOLogic.natT (find_index (equal x) vs)
   774   | reif_polex vs (Const (@{const_name Ring.ring.zero}, _) $ _) =
   775       @{term "Const 0"}
   776   | reif_polex vs (Const (@{const_name Group.monoid.one}, _) $ _) =
   777       @{term "Const 1"}
   778   | reif_polex vs (Const (@{const_name Algebra_Aux.of_integer}, _) $ _ $ n) =
   779       @{const Const} $ n
   780   | reif_polex _ _ = error "reif_polex: bad expression";
   781 
   782 fun reif_polex' vs (Const (@{const_name Groups.plus}, _) $ a $ b) =
   783       @{const Add} $ reif_polex' vs a $ reif_polex' vs b
   784   | reif_polex' vs (Const (@{const_name Groups.minus}, _) $ a $ b) =
   785       @{const Sub} $ reif_polex' vs a $ reif_polex' vs b
   786   | reif_polex' vs (Const (@{const_name Groups.times}, _) $ a $ b) =
   787       @{const Mul} $ reif_polex' vs a $ reif_polex' vs b
   788   | reif_polex' vs (Const (@{const_name Groups.uminus}, _) $ a) =
   789       @{const Neg} $ reif_polex' vs a
   790   | reif_polex' vs (Const (@{const_name Power.power}, _) $ a $ n) =
   791       @{const Pow} $ reif_polex' vs a $ n
   792   | reif_polex' vs (Free x) =
   793       @{const Var} $ HOLogic.mk_number HOLogic.natT (find_index (equal x) vs)
   794   | reif_polex' vs (Const (@{const_name numeral}, _) $ b) =
   795       @{const Const} $ (@{const numeral (int)} $ b)
   796   | reif_polex' vs (Const (@{const_name zero_class.zero}, _)) = @{term "Const 0"}
   797   | reif_polex' vs (Const (@{const_name one_class.one}, _)) = @{term "Const 1"}
   798   | reif_polex' vs t = error "reif_polex: bad expression";
   799 
   800 fun head_conv (_, _, _, _, head_simp, _) ys =
   801   (case strip_app ys of
   802      (@{const_name Cons}, [y, xs]) => inst [] [y, xs] head_simp);
   803 
   804 fun Ipol_conv (rls as
   805       ([Ipol_simps_1, Ipol_simps_2, Ipol_simps_3,
   806         Ipol_simps_4, Ipol_simps_5, Ipol_simps_6,
   807         Ipol_simps_7], _, _, _, _, _)) =
   808   let
   809     val a = type_of_eqn Ipol_simps_1;
   810     val drop_conv_a = drop_conv a;
   811 
   812     fun conv l p = (case strip_app p of
   813         (@{const_name Pc}, [c]) => (case strip_numeral c of
   814             (@{const_name zero_class.zero}, _) => inst [] [l] Ipol_simps_4
   815           | (@{const_name one_class.one}, _) => inst [] [l] Ipol_simps_5
   816           | (@{const_name numeral}, [m]) => inst [] [l, m] Ipol_simps_6
   817           | (@{const_name uminus}, [m]) => inst [] [l, m] Ipol_simps_7
   818           | _ => inst [] [l, c] Ipol_simps_1)
   819       | (@{const_name Pinj}, [i, P]) =>
   820           transitive'
   821             (inst [] [l, i, P] Ipol_simps_2)
   822             (cong2' conv (args2 drop_conv_a) Thm.reflexive)
   823       | (@{const_name PX}, [P, x, Q]) =>
   824           transitive'
   825             (inst [] [l, P, x, Q] Ipol_simps_3)
   826             (cong2
   827                (cong2
   828                   (args2 conv) (cong2 (args1 (head_conv rls)) Thm.reflexive))
   829                (cong2' conv (args2 drop_conv_a) Thm.reflexive)))
   830   in conv end;
   831 
   832 fun Ipolex_conv (rls as
   833       (_,
   834        [Ipolex_Var, Ipolex_Const, Ipolex_Add,
   835         Ipolex_Sub, Ipolex_Mul, Ipolex_Pow,
   836         Ipolex_Neg, Ipolex_Const_0, Ipolex_Const_1,
   837         Ipolex_Const_numeral], _, _, _, _)) =
   838   let
   839     val a = type_of_eqn Ipolex_Var;
   840     val drop_conv_a = drop_conv a;
   841 
   842     fun conv l r = (case strip_app r of
   843         (@{const_name Var}, [n]) =>
   844           transitive'
   845             (inst [] [l, n] Ipolex_Var)
   846             (cong1' (head_conv rls) (args2 drop_conv_a))
   847       | (@{const_name Const}, [i]) => (case strip_app i of
   848             (@{const_name zero_class.zero}, _) => inst [] [l] Ipolex_Const_0
   849           | (@{const_name one_class.one}, _) => inst [] [l] Ipolex_Const_1
   850           | (@{const_name numeral}, [m]) => inst [] [l, m] Ipolex_Const_numeral
   851           | _ => inst [] [l, i] Ipolex_Const)
   852       | (@{const_name Add}, [P, Q]) =>
   853           transitive'
   854             (inst [] [l, P, Q] Ipolex_Add)
   855             (cong2 (args2 conv) (args2 conv))
   856       | (@{const_name Sub}, [P, Q]) =>
   857           transitive'
   858             (inst [] [l, P, Q] Ipolex_Sub)
   859             (cong2 (args2 conv) (args2 conv))
   860       | (@{const_name Mul}, [P, Q]) =>
   861           transitive'
   862             (inst [] [l, P, Q] Ipolex_Mul)
   863             (cong2 (args2 conv) (args2 conv))
   864       | (@{const_name Pow}, [P, n]) =>
   865           transitive'
   866             (inst [] [l, P, n] Ipolex_Pow)
   867             (cong2 (args2 conv) Thm.reflexive)
   868       | (@{const_name Neg}, [P]) =>
   869           transitive'
   870             (inst [] [l, P] Ipolex_Neg)
   871             (cong1 (args2 conv)))
   872   in conv end;
   873 
   874 fun Ipolex_polex_list_conv (rls as
   875       (_, _,
   876        [Ipolex_polex_list_Nil, Ipolex_polex_list_Cons], _, _, _)) l pps =
   877   (case strip_app pps of
   878      (@{const_name Nil}, []) => inst [] [l] Ipolex_polex_list_Nil
   879    | (@{const_name Cons}, [p, pps']) => (case strip_app p of
   880        (@{const_name Pair}, [P, Q]) =>
   881          transitive'
   882            (inst [] [l, P, Q, pps'] Ipolex_polex_list_Cons)
   883            (cong2
   884               (cong2 (args2 (Ipolex_conv rls)) (args2 (Ipolex_conv rls)))
   885               (args2 (Ipolex_polex_list_conv rls)))));
   886 
   887 fun dest_conj th =
   888   let
   889     val th1 = th RS @{thm conjunct1};
   890     val th2 = th RS @{thm conjunct2}
   891   in
   892     dest_conj th1 @ dest_conj th2
   893   end handle THM _ => [th];
   894 
   895 fun mk_in_carrier ctxt R prems xs =
   896   let
   897     val (_, _, _, [in_carrier_Nil, in_carrier_Cons], _, _) =
   898       get_ring_simps ctxt NONE R;
   899     val props = map fst (Facts.props (Proof_Context.facts_of ctxt)) @ maps dest_conj prems;
   900     val ths = map (fn p as (x, _) =>
   901       (case find_first
   902          ((fn Const (@{const_name Trueprop}, _) $
   903                 (Const (@{const_name Set.member}, _) $
   904                    Free (y, _) $ (Const (@{const_name carrier}, _) $ S)) =>
   905                 x = y andalso R aconv S
   906             | _ => false) o Thm.prop_of) props of
   907          SOME th => th
   908        | NONE => error ("Variable " ^ Syntax.string_of_term ctxt (Free p) ^
   909            " not in carrier"))) xs
   910   in
   911     fold_rev (fn th1 => fn th2 => [th1, th2] MRS in_carrier_Cons)
   912        ths in_carrier_Nil
   913   end;
   914 
   915 fun mk_ring T =
   916   Const (@{const_name cring_class_ops},
   917     Type (@{type_name partial_object_ext}, [T,
   918       Type (@{type_name monoid_ext}, [T,
   919         Type (@{type_name ring_ext}, [T, @{typ unit}])])]));
   920 
   921 val iterations = @{cterm "1000::nat"};
   922 val Trueprop_cong = Thm.combination (Thm.reflexive @{cterm Trueprop});
   923 
   924 fun commutative_ring_conv ctxt prems eqs ct =
   925   let
   926     val cT = Thm.ctyp_of_cterm ct;
   927     val T = Thm.typ_of cT;
   928     val eqs' = map (HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of) eqs;
   929     val xs = filter (equal T o snd) (rev (fold Term.add_frees
   930       (map fst eqs' @ map snd eqs' @ [Thm.term_of ct]) []));
   931     val (R, optcT, prem', reif) = (case ring_struct (Thm.term_of ct) of
   932         SOME R => (R, NONE, mk_in_carrier ctxt R prems xs, reif_polex xs)
   933       | NONE => (mk_ring T, SOME cT, @{thm in_carrier_trivial}, reif_polex' xs));
   934     val rls as (_, _, _, _, _, norm_subst_correct) = get_ring_simps ctxt optcT R;
   935     val cxs = Thm.cterm_of ctxt (HOLogic.mk_list T (map Free xs));
   936     val ceqs = Thm.cterm_of ctxt (HOLogic.mk_list @{typ "polex * polex"}
   937       (map (HOLogic.mk_prod o apply2 reif) eqs'));
   938     val cp = Thm.cterm_of ctxt (reif (Thm.term_of ct));
   939     val prem = Thm.equal_elim
   940       (Trueprop_cong (Thm.symmetric (Ipolex_polex_list_conv rls cxs ceqs)))
   941       (fold_rev (fn th1 => fn th2 => [th1, th2] MRS @{thm conjI})
   942          eqs @{thm TrueI});
   943   in
   944     Thm.transitive
   945       (Thm.symmetric (Ipolex_conv rls cxs cp))
   946       (transitive'
   947          ([prem', prem] MRS inst [] [cxs, ceqs, cp, iterations, iterations]
   948             norm_subst_correct)
   949          (cong2' (Ipol_conv rls)
   950             Thm.reflexive
   951             (cv ctxt)))
   952   end;
   953 
   954 fun ring_tac in_prems thms ctxt =
   955   tactic_of_conv (fn ct =>
   956     (if in_prems then Conv.prems_conv else Conv.concl_conv)
   957       (Logic.count_prems (Thm.term_of ct))
   958       (Conv.arg_conv (Conv.binop_conv (commutative_ring_conv ctxt [] thms))) ct) THEN'
   959   TRY o (assume_tac ctxt ORELSE' resolve_tac ctxt [@{thm refl}]);
   960 
   961 end
   962 \<close>
   963 
   964 context cring begin
   965 
   966 local_setup \<open>
   967 Local_Theory.declaration {syntax = false, pervasive = false}
   968   (fn phi => Ring_Tac.Ring_Simps.map (Ring_Tac.insert_rules Ring_Tac.eq_ring_simps
   969     (Morphism.term phi @{term R},
   970      (Morphism.fact phi @{thms Ipol.simps [meta] Ipol_Pc [meta]},
   971       Morphism.fact phi @{thms Ipolex.simps [meta] Ipolex_Const [meta]},
   972       Morphism.fact phi @{thms Ipolex_polex_list.simps [meta]},
   973       Morphism.fact phi @{thms in_carrier_Nil in_carrier_Cons},
   974       singleton (Morphism.fact phi) @{thm head.simps(2) [meta]},
   975       singleton (Morphism.fact phi) @{thm norm_subst_correct [meta]}))))
   976 \<close>
   977 
   978 end
   979 
   980 method_setup ring = \<open>
   981   Scan.lift (Args.mode "prems") -- Attrib.thms >> (SIMPLE_METHOD' oo uncurry Ring_Tac.ring_tac)
   982 \<close> "simplify equations involving rings"
   983 
   984 end