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