author | wenzelm |
Sat, 10 Jun 2017 21:48:02 +0200 | |
changeset 66061 | 880db47fed30 |
parent 65043 | fd753468786f |
child 66453 | cc19f7ca2ed6 |
permissions | -rw-r--r-- |
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 | 3 |
|
4 |
Proving equalities in commutative rings done "right" in Isabelle/HOL. |
|
5 |
*) |
|
6 |
||
60533 | 7 |
section \<open>Proving equalities in commutative rings\<close> |
17516 | 8 |
|
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 | 14 |
begin |
15 |
||
60533 | 16 |
text \<open>Syntax of multivariate polynomials (pol) and polynomial expressions.\<close> |
17516 | 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 | 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 | 31 |
|
60533 | 32 |
text \<open>Interpretation functions for the shadow syntax.\<close> |
17516 | 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 | 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 | 91 |
|
60533 | 92 |
text \<open>Create polynomial normalized polynomials given normalized inputs.\<close> |
17516 | 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 | 95 |
where |
60534 | 96 |
"mkPinj x P = |
97 |
(case P of |
|
98 |
Pc c \<Rightarrow> Pc c |
|
99 |
| Pinj y P \<Rightarrow> Pinj (x + y) P |
|
100 |
| PX p1 y p2 \<Rightarrow> Pinj x P)" |
|
17516 | 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 | 103 |
where |
104 |
"mkPX P i Q = |
|
105 |
(case P of |
|
106 |
Pc c \<Rightarrow> if c = 0 then mkPinj 1 Q else PX P i Q |
|
107 |
| Pinj j R \<Rightarrow> PX P i Q |
|
108 |
| PX P2 i2 Q2 \<Rightarrow> if Q2 = Pc 0 then PX P2 (i + i2) Q else PX P i Q)" |
|
17516 | 109 |
|
60533 | 110 |
text \<open>Defining the basic ring operations on normalized polynomials\<close> |
17516 | 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 | 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 | 171 |
|
60533 | 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 | 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 | 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 | 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 | 197 |
(if n = 0 then Pc 1 |
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 | 200 |
|
60534 | 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 | 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 | 206 |
|
60534 | 207 |
lemma even_pow: "even n \<Longrightarrow> pow n P = pow (n div 2) (sqr P)" |
58712 | 208 |
by (erule evenE) simp |
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 | 211 |
by (erule oddE) simp |
212 |
||
60534 | 213 |
|
60533 | 214 |
text \<open>Normalization of polynomial expressions\<close> |
17516 | 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 | 230 |
|
60533 | 231 |
text \<open>mkPinj preserve semantics\<close> |
17516 | 232 |
lemma mkPinj_ci: "Ipol l (mkPinj a B) = Ipol l (Pinj a B)" |
29667 | 233 |
by (induct B) (auto simp add: mkPinj_def algebra_simps) |
17516 | 234 |
|
60533 | 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 | 238 |
|
60533 | 239 |
text \<open>Correctness theorems for the implemented operations\<close> |
17516 | 240 |
|
60533 | 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 | 244 |
|
60533 | 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 | 247 |
proof (induct P Q arbitrary: l rule: add.induct) |
17516 | 248 |
case (6 x P y Q) |
60708 | 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 | 251 |
proof cases |
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 | 254 |
next |
60708 | 255 |
case 2 |
256 |
with 6 show ?thesis by (simp add: mkPinj_ci) |
|
17516 | 257 |
next |
60708 | 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 | 260 |
qed |
261 |
next |
|
262 |
case (7 x P Q y R) |
|
60534 | 263 |
consider "x = 0" | "x = 1" | "x > 1" by arith |
264 |
then show ?case |
|
265 |
proof cases |
|
266 |
case 1 |
|
267 |
with 7 show ?thesis by simp |
|
268 |
next |
|
269 |
case 2 |
|
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 | 271 |
next |
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 | 274 |
qed |
17516 | 275 |
next |
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 | 278 |
next |
279 |
case (9 P1 x P2 Q1 y Q2) |
|
60534 | 280 |
consider "x = y" | d where "d + x = y" | d where "d + y = x" |
281 |
by atomize_elim arith |
|
282 |
then show ?case |
|
283 |
proof cases |
|
284 |
case 1 |
|
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 | 286 |
next |
60534 | 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 | 289 |
next |
60534 | 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 | 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 | 294 |
|
60533 | 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 | 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 | 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 | 303 |
|
60533 | 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 | 309 |
|
60533 | 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 | 312 |
proof (induct n arbitrary: P rule: less_induct) |
313 |
case (less k) |
|
60708 | 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 | 316 |
proof cases |
317 |
case 1 |
|
60534 | 318 |
then show ?thesis by simp |
20622 | 319 |
next |
60708 | 320 |
case 2 |
58712 | 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 | 323 |
by simp |
17516 | 324 |
show ?thesis |
58712 | 325 |
proof (cases "even k") |
60534 | 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 | 329 |
mult_2 [symmetric] even_two_times_div_two) |
17516 | 330 |
next |
60534 | 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 | 335 |
qed |
336 |
qed |
|
337 |
qed |
|
338 |
||
60533 | 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 | 341 |
by (induct Pe) (simp_all add: add_ci sub_ci mul_ci neg_ci pow_ci) |
342 |
||
60533 | 343 |
text \<open>Reflection lemma: Key to the (incomplete) decision procedure\<close> |
17516 | 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 | 347 |
shows "Ipolex l P1 = Ipolex l P2" |
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 | 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 | 515 |
qed |
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 | 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 | 658 |
ML \<open> |
659 |
val term_of_nat = HOLogic.mk_number @{typ nat} o @{code integer_of_nat}; |
|
660 |
||
661 |
val term_of_int = HOLogic.mk_number @{typ int} o @{code integer_of_int}; |
|
662 |
||
663 |
fun term_of_pol (@{code Pc} k) = @{term Pc} $ term_of_int k |
|
664 |
| term_of_pol (@{code Pinj} (n, p)) = @{term Pinj} $ term_of_nat n $ term_of_pol p |
|
665 |
| term_of_pol (@{code PX} (p, n, q)) = @{term PX} $ term_of_pol p $ term_of_nat n $ term_of_pol q; |
|
666 |
||
667 |
local |
|
668 |
||
669 |
fun pol (ctxt, ct, t) = Thm.mk_binop @{cterm "Pure.eq :: pol \<Rightarrow> pol \<Rightarrow> prop"} |
|
670 |
ct (Thm.cterm_of ctxt t); |
|
64962
bf41e1109db3
Added new / improved tactics for fields and rings
berghofe
parents:
60708
diff
changeset
|
671 |
|
64999 | 672 |
val (_, raw_pol_oracle) = Context.>>> (Context.map_theory_result |
673 |
(Thm.add_oracle (@{binding pnsubstl}, pol))); |
|
674 |
||
675 |
fun pol_oracle ctxt ct t = raw_pol_oracle (ctxt, ct, t); |
|
676 |
||
677 |
in |
|
678 |
||
679 |
val cv = @{computation_conv pol |
|
680 |
terms: pnsubstl mk_monpol_list norm |
|
681 |
nat_of_integer Code_Target_Nat.natural |
|
682 |
"0::nat" "1::nat" "2::nat" "3::nat" |
|
683 |
"0::int" "1::int" "2::int" "3::int" "-1::int" |
|
684 |
datatypes: polex "(polex * polex) list" int integer num} |
|
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 | 686 |
|
687 |
end |
|
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 | 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 | 960 |
|
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 |