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