src/HOL/Decision_Procs/Commutative_Ring.thy
author nipkow
Tue Feb 23 16:25:08 2016 +0100 (2016-02-23)
changeset 62390 842917225d56
parent 60708 f425e80a3eb0
child 64962 bf41e1109db3
permissions -rw-r--r--
more canonical names
haftmann@28952
     1
(*  Author:     Bernhard Haeupler
wenzelm@17516
     2
wenzelm@17516
     3
Proving equalities in commutative rings done "right" in Isabelle/HOL.
wenzelm@17516
     4
*)
wenzelm@17516
     5
wenzelm@60533
     6
section \<open>Proving equalities in commutative rings\<close>
wenzelm@17516
     7
wenzelm@17516
     8
theory Commutative_Ring
haftmann@58770
     9
imports Main
wenzelm@17516
    10
begin
wenzelm@17516
    11
wenzelm@60533
    12
text \<open>Syntax of multivariate polynomials (pol) and polynomial expressions.\<close>
wenzelm@17516
    13
blanchet@58310
    14
datatype 'a pol =
wenzelm@17516
    15
    Pc 'a
wenzelm@17516
    16
  | Pinj nat "'a pol"
wenzelm@17516
    17
  | PX "'a pol" nat "'a pol"
wenzelm@17516
    18
blanchet@58310
    19
datatype 'a polex =
wenzelm@20622
    20
    Pol "'a pol"
wenzelm@17516
    21
  | Add "'a polex" "'a polex"
wenzelm@17516
    22
  | Sub "'a polex" "'a polex"
wenzelm@17516
    23
  | Mul "'a polex" "'a polex"
wenzelm@17516
    24
  | Pow "'a polex" nat
wenzelm@17516
    25
  | Neg "'a polex"
wenzelm@17516
    26
wenzelm@60533
    27
text \<open>Interpretation functions for the shadow syntax.\<close>
wenzelm@17516
    28
wenzelm@60534
    29
primrec Ipol :: "'a::comm_ring_1 list \<Rightarrow> 'a pol \<Rightarrow> 'a"
haftmann@22742
    30
where
haftmann@22742
    31
    "Ipol l (Pc c) = c"
haftmann@22742
    32
  | "Ipol l (Pinj i P) = Ipol (drop i l) P"
haftmann@22742
    33
  | "Ipol l (PX P x Q) = Ipol l P * (hd l)^x + Ipol (drop 1 l) Q"
wenzelm@17516
    34
wenzelm@60534
    35
primrec Ipolex :: "'a::comm_ring_1 list \<Rightarrow> 'a polex \<Rightarrow> 'a"
haftmann@22742
    36
where
haftmann@22742
    37
    "Ipolex l (Pol P) = Ipol l P"
haftmann@22742
    38
  | "Ipolex l (Add P Q) = Ipolex l P + Ipolex l Q"
haftmann@22742
    39
  | "Ipolex l (Sub P Q) = Ipolex l P - Ipolex l Q"
haftmann@22742
    40
  | "Ipolex l (Mul P Q) = Ipolex l P * Ipolex l Q"
haftmann@22742
    41
  | "Ipolex l (Pow p n) = Ipolex l p ^ n"
haftmann@22742
    42
  | "Ipolex l (Neg P) = - Ipolex l P"
wenzelm@17516
    43
wenzelm@60533
    44
text \<open>Create polynomial normalized polynomials given normalized inputs.\<close>
wenzelm@17516
    45
wenzelm@55754
    46
definition mkPinj :: "nat \<Rightarrow> 'a pol \<Rightarrow> 'a pol"
wenzelm@55754
    47
where
wenzelm@60534
    48
  "mkPinj x P =
wenzelm@60534
    49
    (case P of
wenzelm@60534
    50
      Pc c \<Rightarrow> Pc c
wenzelm@60534
    51
    | Pinj y P \<Rightarrow> Pinj (x + y) P
wenzelm@60534
    52
    | PX p1 y p2 \<Rightarrow> Pinj x P)"
wenzelm@17516
    53
wenzelm@55754
    54
definition mkPX :: "'a::comm_ring pol \<Rightarrow> nat \<Rightarrow> 'a pol \<Rightarrow> 'a pol"
wenzelm@55754
    55
where
wenzelm@55754
    56
  "mkPX P i Q =
wenzelm@55754
    57
    (case P of
wenzelm@55754
    58
      Pc c \<Rightarrow> if c = 0 then mkPinj 1 Q else PX P i Q
wenzelm@55754
    59
    | Pinj j R \<Rightarrow> PX P i Q
wenzelm@55754
    60
    | PX P2 i2 Q2 \<Rightarrow> if Q2 = Pc 0 then PX P2 (i + i2) Q else PX P i Q)"
wenzelm@17516
    61
wenzelm@60533
    62
text \<open>Defining the basic ring operations on normalized polynomials\<close>
wenzelm@17516
    63
blanchet@58259
    64
lemma pol_size_nz[simp]: "size (p :: 'a pol) \<noteq> 0"
blanchet@58259
    65
  by (cases p) simp_all
blanchet@58259
    66
wenzelm@55754
    67
function add :: "'a::comm_ring pol \<Rightarrow> 'a pol \<Rightarrow> 'a pol"  (infixl "\<oplus>" 65)
haftmann@22742
    68
where
wenzelm@55754
    69
  "Pc a \<oplus> Pc b = Pc (a + b)"
wenzelm@55754
    70
| "Pc c \<oplus> Pinj i P = Pinj i (P \<oplus> Pc c)"
wenzelm@55754
    71
| "Pinj i P \<oplus> Pc c = Pinj i (P \<oplus> Pc c)"
wenzelm@55754
    72
| "Pc c \<oplus> PX P i Q = PX P i (Q \<oplus> Pc c)"
wenzelm@55754
    73
| "PX P i Q \<oplus> Pc c = PX P i (Q \<oplus> Pc c)"
wenzelm@55754
    74
| "Pinj x P \<oplus> Pinj y Q =
wenzelm@55754
    75
    (if x = y then mkPinj x (P \<oplus> Q)
wenzelm@55754
    76
     else (if x > y then mkPinj y (Pinj (x - y) P \<oplus> Q)
wenzelm@55754
    77
       else mkPinj x (Pinj (y - x) Q \<oplus> P)))"
wenzelm@55754
    78
| "Pinj x P \<oplus> PX Q y R =
wenzelm@55754
    79
    (if x = 0 then P \<oplus> PX Q y R
wenzelm@55754
    80
     else (if x = 1 then PX Q y (R \<oplus> P)
wenzelm@55754
    81
       else PX Q y (R \<oplus> Pinj (x - 1) P)))"
wenzelm@55754
    82
| "PX P x R \<oplus> Pinj y Q =
wenzelm@55754
    83
    (if y = 0 then PX P x R \<oplus> Q
wenzelm@55754
    84
     else (if y = 1 then PX P x (R \<oplus> Q)
wenzelm@55754
    85
       else PX P x (R \<oplus> Pinj (y - 1) Q)))"
wenzelm@55754
    86
| "PX P1 x P2 \<oplus> PX Q1 y Q2 =
wenzelm@55754
    87
    (if x = y then mkPX (P1 \<oplus> Q1) x (P2 \<oplus> Q2)
wenzelm@55754
    88
     else (if x > y then mkPX (PX P1 (x - y) (Pc 0) \<oplus> Q1) y (P2 \<oplus> Q2)
wenzelm@55754
    89
       else mkPX (PX Q1 (y-x) (Pc 0) \<oplus> P1) x (P2 \<oplus> Q2)))"
haftmann@22742
    90
by pat_completeness auto
haftmann@22742
    91
termination by (relation "measure (\<lambda>(x, y). size x + size y)") auto
wenzelm@17516
    92
wenzelm@60534
    93
function mul :: "'a::comm_ring pol \<Rightarrow> 'a pol \<Rightarrow> 'a pol"  (infixl "\<otimes>" 70)
haftmann@22742
    94
where
wenzelm@55754
    95
  "Pc a \<otimes> Pc b = Pc (a * b)"
wenzelm@55754
    96
| "Pc c \<otimes> Pinj i P =
wenzelm@55754
    97
    (if c = 0 then Pc 0 else mkPinj i (P \<otimes> Pc c))"
wenzelm@55754
    98
| "Pinj i P \<otimes> Pc c =
wenzelm@55754
    99
    (if c = 0 then Pc 0 else mkPinj i (P \<otimes> Pc c))"
wenzelm@55754
   100
| "Pc c \<otimes> PX P i Q =
wenzelm@55754
   101
    (if c = 0 then Pc 0 else mkPX (P \<otimes> Pc c) i (Q \<otimes> Pc c))"
wenzelm@55754
   102
| "PX P i Q \<otimes> Pc c =
wenzelm@55754
   103
    (if c = 0 then Pc 0 else mkPX (P \<otimes> Pc c) i (Q \<otimes> Pc c))"
wenzelm@55754
   104
| "Pinj x P \<otimes> Pinj y Q =
wenzelm@60534
   105
    (if x = y then mkPinj x (P \<otimes> Q)
wenzelm@60534
   106
     else
wenzelm@55754
   107
       (if x > y then mkPinj y (Pinj (x-y) P \<otimes> Q)
wenzelm@60534
   108
        else mkPinj x (Pinj (y - x) Q \<otimes> P)))"
wenzelm@55754
   109
| "Pinj x P \<otimes> PX Q y R =
wenzelm@60534
   110
    (if x = 0 then P \<otimes> PX Q y R
wenzelm@60534
   111
     else
wenzelm@55754
   112
       (if x = 1 then mkPX (Pinj x P \<otimes> Q) y (R \<otimes> P)
wenzelm@60534
   113
        else mkPX (Pinj x P \<otimes> Q) y (R \<otimes> Pinj (x - 1) P)))"
wenzelm@55754
   114
| "PX P x R \<otimes> Pinj y Q =
wenzelm@60534
   115
    (if y = 0 then PX P x R \<otimes> Q
wenzelm@60534
   116
     else
wenzelm@55754
   117
       (if y = 1 then mkPX (Pinj y Q \<otimes> P) x (R \<otimes> Q)
wenzelm@60534
   118
        else mkPX (Pinj y Q \<otimes> P) x (R \<otimes> Pinj (y - 1) Q)))"
wenzelm@55754
   119
| "PX P1 x P2 \<otimes> PX Q1 y Q2 =
wenzelm@55754
   120
    mkPX (P1 \<otimes> Q1) (x + y) (P2 \<otimes> Q2) \<oplus>
wenzelm@55754
   121
      (mkPX (P1 \<otimes> mkPinj 1 Q2) x (Pc 0) \<oplus>
wenzelm@55754
   122
        (mkPX (Q1 \<otimes> mkPinj 1 P2) y (Pc 0)))"
haftmann@22742
   123
by pat_completeness auto
haftmann@22742
   124
termination by (relation "measure (\<lambda>(x, y). size x + size y)")
haftmann@22742
   125
  (auto simp add: mkPinj_def split: pol.split)
wenzelm@17516
   126
wenzelm@60533
   127
text \<open>Negation\<close>
wenzelm@60534
   128
primrec neg :: "'a::comm_ring pol \<Rightarrow> 'a pol"
haftmann@22742
   129
where
wenzelm@55754
   130
  "neg (Pc c) = Pc (-c)"
wenzelm@55754
   131
| "neg (Pinj i P) = Pinj i (neg P)"
wenzelm@55754
   132
| "neg (PX P x Q) = PX (neg P) x (neg Q)"
wenzelm@17516
   133
wenzelm@60533
   134
text \<open>Substraction\<close>
wenzelm@60534
   135
definition sub :: "'a::comm_ring pol \<Rightarrow> 'a pol \<Rightarrow> 'a pol"  (infixl "\<ominus>" 65)
wenzelm@55754
   136
  where "sub P Q = P \<oplus> neg Q"
wenzelm@17516
   137
wenzelm@60533
   138
text \<open>Square for Fast Exponentation\<close>
wenzelm@60534
   139
primrec sqr :: "'a::comm_ring_1 pol \<Rightarrow> 'a pol"
haftmann@22742
   140
where
wenzelm@55754
   141
  "sqr (Pc c) = Pc (c * c)"
wenzelm@55754
   142
| "sqr (Pinj i P) = mkPinj i (sqr P)"
wenzelm@55754
   143
| "sqr (PX A x B) =
wenzelm@55754
   144
    mkPX (sqr A) (x + x) (sqr B) \<oplus> mkPX (Pc (1 + 1) \<otimes> A \<otimes> mkPinj 1 B) x (Pc 0)"
wenzelm@17516
   145
wenzelm@60533
   146
text \<open>Fast Exponentation\<close>
haftmann@58710
   147
wenzelm@60534
   148
fun pow :: "nat \<Rightarrow> 'a::comm_ring_1 pol \<Rightarrow> 'a pol"
haftmann@22742
   149
where
haftmann@58710
   150
  pow_if [simp del]: "pow n P =
wenzelm@60534
   151
   (if n = 0 then Pc 1
wenzelm@60534
   152
    else if even n then pow (n div 2) (sqr P)
haftmann@22742
   153
    else P \<otimes> pow (n div 2) (sqr P))"
wenzelm@17516
   154
wenzelm@60534
   155
lemma pow_simps [simp]:
haftmann@58710
   156
  "pow 0 P = Pc 1"
haftmann@58712
   157
  "pow (2 * n) P = pow n (sqr P)"
haftmann@58712
   158
  "pow (Suc (2 * n)) P = P \<otimes> pow n (sqr P)"
haftmann@58710
   159
  by (simp_all add: pow_if)
wenzelm@17516
   160
wenzelm@60534
   161
lemma even_pow: "even n \<Longrightarrow> pow n P = pow (n div 2) (sqr P)"
haftmann@58712
   162
  by (erule evenE) simp
haftmann@58712
   163
wenzelm@60534
   164
lemma odd_pow: "odd n \<Longrightarrow> pow n P = P \<otimes> pow (n div 2) (sqr P)"
haftmann@58712
   165
  by (erule oddE) simp
haftmann@58712
   166
wenzelm@60534
   167
wenzelm@60533
   168
text \<open>Normalization of polynomial expressions\<close>
wenzelm@17516
   169
wenzelm@60534
   170
primrec norm :: "'a::comm_ring_1 polex \<Rightarrow> 'a pol"
haftmann@22742
   171
where
wenzelm@55754
   172
  "norm (Pol P) = P"
wenzelm@55754
   173
| "norm (Add P Q) = norm P \<oplus> norm Q"
wenzelm@55754
   174
| "norm (Sub P Q) = norm P \<ominus> norm Q"
wenzelm@55754
   175
| "norm (Mul P Q) = norm P \<otimes> norm Q"
wenzelm@55754
   176
| "norm (Pow P n) = pow n (norm P)"
wenzelm@55754
   177
| "norm (Neg P) = neg (norm P)"
wenzelm@17516
   178
wenzelm@60533
   179
text \<open>mkPinj preserve semantics\<close>
wenzelm@17516
   180
lemma mkPinj_ci: "Ipol l (mkPinj a B) = Ipol l (Pinj a B)"
nipkow@29667
   181
  by (induct B) (auto simp add: mkPinj_def algebra_simps)
wenzelm@17516
   182
wenzelm@60533
   183
text \<open>mkPX preserves semantics\<close>
wenzelm@17516
   184
lemma mkPX_ci: "Ipol l (mkPX A b C) = Ipol l (PX A b C)"
nipkow@29667
   185
  by (cases A) (auto simp add: mkPX_def mkPinj_ci power_add algebra_simps)
wenzelm@17516
   186
wenzelm@60533
   187
text \<open>Correctness theorems for the implemented operations\<close>
wenzelm@17516
   188
wenzelm@60533
   189
text \<open>Negation\<close>
wenzelm@20622
   190
lemma neg_ci: "Ipol l (neg P) = -(Ipol l P)"
wenzelm@20622
   191
  by (induct P arbitrary: l) auto
wenzelm@17516
   192
wenzelm@60533
   193
text \<open>Addition\<close>
haftmann@22742
   194
lemma add_ci: "Ipol l (P \<oplus> Q) = Ipol l P + Ipol l Q"
wenzelm@20622
   195
proof (induct P Q arbitrary: l rule: add.induct)
wenzelm@17516
   196
  case (6 x P y Q)
wenzelm@60708
   197
  consider "x < y" | "x = y" | "x > y" by arith
wenzelm@60708
   198
  then
wenzelm@17516
   199
  show ?case
wenzelm@60708
   200
  proof cases
wenzelm@60708
   201
    case 1
wenzelm@60708
   202
    with 6 show ?thesis by (simp add: mkPinj_ci algebra_simps)
wenzelm@17516
   203
  next
wenzelm@60708
   204
    case 2
wenzelm@60708
   205
    with 6 show ?thesis by (simp add: mkPinj_ci)
wenzelm@17516
   206
  next
wenzelm@60708
   207
    case 3
wenzelm@60708
   208
    with 6 show ?thesis by (simp add: mkPinj_ci algebra_simps)
wenzelm@17516
   209
  qed
wenzelm@17516
   210
next
wenzelm@17516
   211
  case (7 x P Q y R)
wenzelm@60534
   212
  consider "x = 0" | "x = 1" | "x > 1" by arith
wenzelm@60534
   213
  then show ?case
wenzelm@60534
   214
  proof cases
wenzelm@60534
   215
    case 1
wenzelm@60534
   216
    with 7 show ?thesis by simp
wenzelm@60534
   217
  next
wenzelm@60534
   218
    case 2
wenzelm@60534
   219
    with 7 show ?thesis by (simp add: algebra_simps)
wenzelm@60534
   220
  next
wenzelm@60534
   221
    case 3
wenzelm@60534
   222
    from 7 show ?thesis by (cases x) simp_all
wenzelm@60534
   223
  qed
wenzelm@17516
   224
next
wenzelm@17516
   225
  case (8 P x R y Q)
wenzelm@60534
   226
  then show ?case by simp
wenzelm@17516
   227
next
wenzelm@17516
   228
  case (9 P1 x P2 Q1 y Q2)
wenzelm@60534
   229
  consider "x = y" | d where "d + x = y" | d where "d + y = x"
wenzelm@60534
   230
    by atomize_elim arith
wenzelm@60534
   231
  then show ?case
wenzelm@60534
   232
  proof cases
wenzelm@60534
   233
    case 1
wenzelm@60534
   234
    with 9 show ?thesis by (simp add: mkPX_ci algebra_simps)
wenzelm@17516
   235
  next
wenzelm@60534
   236
    case 2
wenzelm@60534
   237
    with 9 show ?thesis by (auto simp add: mkPX_ci power_add algebra_simps)
wenzelm@17516
   238
  next
wenzelm@60534
   239
    case 3
wenzelm@60534
   240
    with 9 show ?thesis by (auto simp add: power_add mkPX_ci algebra_simps)
wenzelm@17516
   241
  qed
nipkow@29667
   242
qed (auto simp add: algebra_simps)
wenzelm@17516
   243
wenzelm@60533
   244
text \<open>Multiplication\<close>
haftmann@22742
   245
lemma mul_ci: "Ipol l (P \<otimes> Q) = Ipol l P * Ipol l Q"
wenzelm@20622
   246
  by (induct P Q arbitrary: l rule: mul.induct)
nipkow@29667
   247
    (simp_all add: mkPX_ci mkPinj_ci algebra_simps add_ci power_add)
wenzelm@17516
   248
wenzelm@60533
   249
text \<open>Substraction\<close>
haftmann@22742
   250
lemma sub_ci: "Ipol l (P \<ominus> Q) = Ipol l P - Ipol l Q"
wenzelm@17516
   251
  by (simp add: add_ci neg_ci sub_def)
wenzelm@17516
   252
wenzelm@60533
   253
text \<open>Square\<close>
haftmann@22742
   254
lemma sqr_ci: "Ipol ls (sqr P) = Ipol ls P * Ipol ls P"
haftmann@22742
   255
  by (induct P arbitrary: ls)
nipkow@29667
   256
    (simp_all add: add_ci mkPinj_ci mkPX_ci mul_ci algebra_simps power_add)
wenzelm@17516
   257
wenzelm@60533
   258
text \<open>Power\<close>
haftmann@22742
   259
lemma pow_ci: "Ipol ls (pow n P) = Ipol ls P ^ n"
haftmann@58712
   260
proof (induct n arbitrary: P rule: less_induct)
haftmann@58712
   261
  case (less k)
wenzelm@60708
   262
  consider "k = 0" | "k > 0" by arith
wenzelm@60708
   263
  then
wenzelm@17516
   264
  show ?case
wenzelm@60708
   265
  proof cases
wenzelm@60708
   266
    case 1
wenzelm@60534
   267
    then show ?thesis by simp
wenzelm@20622
   268
  next
wenzelm@60708
   269
    case 2
haftmann@58712
   270
    then have "k div 2 < k" by arith
haftmann@58712
   271
    with less have *: "Ipol ls (pow (k div 2) (sqr P)) = Ipol ls (sqr P) ^ (k div 2)"
haftmann@58712
   272
      by simp
wenzelm@17516
   273
    show ?thesis
haftmann@58712
   274
    proof (cases "even k")
wenzelm@60534
   275
      case True
wenzelm@60534
   276
      with * show ?thesis
wenzelm@60534
   277
        by (simp add: even_pow sqr_ci power_mult_distrib power_add [symmetric]
wenzelm@60534
   278
          mult_2 [symmetric] even_two_times_div_two)
wenzelm@17516
   279
    next
wenzelm@60534
   280
      case False
wenzelm@60534
   281
      with * show ?thesis
wenzelm@60534
   282
        by (simp add: odd_pow mul_ci sqr_ci power_mult_distrib power_add [symmetric]
wenzelm@60534
   283
          mult_2 [symmetric] power_Suc [symmetric])
wenzelm@17516
   284
    qed
wenzelm@17516
   285
  qed
wenzelm@17516
   286
qed
wenzelm@17516
   287
wenzelm@60533
   288
text \<open>Normalization preserves semantics\<close>
wenzelm@20622
   289
lemma norm_ci: "Ipolex l Pe = Ipol l (norm Pe)"
wenzelm@17516
   290
  by (induct Pe) (simp_all add: add_ci sub_ci mul_ci neg_ci pow_ci)
wenzelm@17516
   291
wenzelm@60533
   292
text \<open>Reflection lemma: Key to the (incomplete) decision procedure\<close>
wenzelm@17516
   293
lemma norm_eq:
wenzelm@20622
   294
  assumes "norm P1 = norm P2"
wenzelm@17516
   295
  shows "Ipolex l P1 = Ipolex l P2"
wenzelm@17516
   296
proof -
wenzelm@60534
   297
  from assms have "Ipol l (norm P1) = Ipol l (norm P2)"
wenzelm@60534
   298
    by simp
wenzelm@60534
   299
  then show ?thesis
wenzelm@60534
   300
    by (simp only: norm_ci)
wenzelm@17516
   301
qed
wenzelm@17516
   302
wenzelm@17516
   303
wenzelm@48891
   304
ML_file "commutative_ring_tac.ML"
wenzelm@47432
   305
wenzelm@60533
   306
method_setup comm_ring = \<open>
wenzelm@47432
   307
  Scan.succeed (SIMPLE_METHOD' o Commutative_Ring_Tac.tac)
wenzelm@60533
   308
\<close> "reflective decision procedure for equalities over commutative rings"
wenzelm@17516
   309
wenzelm@17516
   310
end