author | wenzelm |
Sat, 20 Jun 2015 17:29:51 +0200 | |
changeset 60535 | 25a3c522cc8f |
parent 60533 | 1e7ccd864b62 |
child 60567 | 19c277ea65ae |
permissions | -rw-r--r-- |
31021 | 1 |
(* Author: Bernhard Haeupler |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
2 |
|
17388 | 3 |
This theory is about of the relative completeness of method comm-ring |
4 |
method. As long as the reified atomic polynomials of type 'a pol are |
|
5 |
in normal form, the cring method is complete. |
|
6 |
*) |
|
7 |
||
60533 | 8 |
section \<open>Proof of the relative completeness of method comm-ring\<close> |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
9 |
|
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
10 |
theory Commutative_Ring_Complete |
17508 | 11 |
imports Commutative_Ring |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
12 |
begin |
22742
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
13 |
|
60533 | 14 |
text \<open>Formalization of normal form\<close> |
44779 | 15 |
fun isnorm :: "'a::comm_ring pol \<Rightarrow> bool" |
22742
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
16 |
where |
55754 | 17 |
"isnorm (Pc c) \<longleftrightarrow> True" |
18 |
| "isnorm (Pinj i (Pc c)) \<longleftrightarrow> False" |
|
19 |
| "isnorm (Pinj i (Pinj j Q)) \<longleftrightarrow> False" |
|
20 |
| "isnorm (Pinj 0 P) \<longleftrightarrow> False" |
|
21 |
| "isnorm (Pinj i (PX Q1 j Q2)) \<longleftrightarrow> isnorm (PX Q1 j Q2)" |
|
22 |
| "isnorm (PX P 0 Q) \<longleftrightarrow> False" |
|
23 |
| "isnorm (PX (Pc c) i Q) \<longleftrightarrow> c \<noteq> 0 \<and> isnorm Q" |
|
24 |
| "isnorm (PX (PX P1 j (Pc c)) i Q) \<longleftrightarrow> c \<noteq> 0 \<and> isnorm (PX P1 j (Pc c)) \<and> isnorm Q" |
|
25 |
| "isnorm (PX P i Q) \<longleftrightarrow> isnorm P \<and> isnorm Q" |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
26 |
|
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
27 |
(* Some helpful lemmas *) |
44779 | 28 |
lemma norm_Pinj_0_False: "isnorm (Pinj 0 P) = False" |
29 |
by (cases P) auto |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
30 |
|
44779 | 31 |
lemma norm_PX_0_False: "isnorm (PX (Pc 0) i Q) = False" |
32 |
by (cases i) auto |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
33 |
|
44779 | 34 |
lemma norm_Pinj: "isnorm (Pinj i Q) \<Longrightarrow> isnorm Q" |
35 |
by (cases i) (simp add: norm_Pinj_0_False norm_PX_0_False, cases Q, auto) |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
36 |
|
44779 | 37 |
lemma norm_PX2: "isnorm (PX P i Q) \<Longrightarrow> isnorm Q" |
55754 | 38 |
apply (cases i) |
39 |
apply auto |
|
40 |
apply (cases P) |
|
41 |
apply auto |
|
58259 | 42 |
apply (rename_tac pol2, case_tac pol2) |
55754 | 43 |
apply auto |
44 |
done |
|
44779 | 45 |
|
46 |
lemma norm_PX1: "isnorm (PX P i Q) \<Longrightarrow> isnorm P" |
|
55754 | 47 |
apply (cases i) |
48 |
apply auto |
|
49 |
apply (cases P) |
|
50 |
apply auto |
|
58259 | 51 |
apply (rename_tac pol2, case_tac pol2) |
55754 | 52 |
apply auto |
53 |
done |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
54 |
|
55754 | 55 |
lemma mkPinj_cn: "y \<noteq> 0 \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (mkPinj y Q)" |
44779 | 56 |
apply (auto simp add: mkPinj_def norm_Pinj_0_False split: pol.split) |
58259 | 57 |
apply (rename_tac nat a, case_tac nat, auto simp add: norm_Pinj_0_False) |
58 |
apply (rename_tac pol a, case_tac pol, auto) |
|
44779 | 59 |
apply (case_tac y, auto) |
60 |
done |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
61 |
|
55793 | 62 |
lemma norm_PXtrans: |
55754 | 63 |
assumes A: "isnorm (PX P x Q)" |
55793 | 64 |
and "isnorm Q2" |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
65 |
shows "isnorm (PX P x Q2)" |
44779 | 66 |
proof (cases P) |
67 |
case (PX p1 y p2) |
|
55754 | 68 |
with assms show ?thesis |
69 |
apply (cases x) |
|
70 |
apply auto |
|
71 |
apply (cases p2) |
|
72 |
apply auto |
|
73 |
done |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
74 |
next |
44779 | 75 |
case Pc |
60535 | 76 |
with assms show ?thesis |
77 |
by (cases x) auto |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
78 |
next |
44779 | 79 |
case Pinj |
60535 | 80 |
with assms show ?thesis |
81 |
by (cases x) auto |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
82 |
qed |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
83 |
|
55793 | 84 |
lemma norm_PXtrans2: |
85 |
assumes "isnorm (PX P x Q)" |
|
86 |
and "isnorm Q2" |
|
87 |
shows "isnorm (PX P (Suc (n + x)) Q2)" |
|
88 |
proof (cases P) |
|
89 |
case (PX p1 y p2) |
|
90 |
with assms show ?thesis |
|
91 |
apply (cases x) |
|
92 |
apply auto |
|
93 |
apply (cases p2) |
|
94 |
apply auto |
|
95 |
done |
|
96 |
next |
|
97 |
case Pc |
|
98 |
with assms show ?thesis |
|
99 |
by (cases x) auto |
|
100 |
next |
|
101 |
case Pinj |
|
102 |
with assms show ?thesis |
|
103 |
by (cases x) auto |
|
104 |
qed |
|
105 |
||
60533 | 106 |
text \<open>mkPX conserves normalizedness (@{text "_cn"})\<close> |
55793 | 107 |
lemma mkPX_cn: |
55754 | 108 |
assumes "x \<noteq> 0" |
109 |
and "isnorm P" |
|
55793 | 110 |
and "isnorm Q" |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
111 |
shows "isnorm (mkPX P x Q)" |
55754 | 112 |
proof (cases P) |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
113 |
case (Pc c) |
55754 | 114 |
with assms show ?thesis |
115 |
by (cases x) (auto simp add: mkPinj_cn mkPX_def) |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
116 |
next |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
117 |
case (Pinj i Q) |
55754 | 118 |
with assms show ?thesis |
119 |
by (cases x) (auto simp add: mkPinj_cn mkPX_def) |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
120 |
next |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
121 |
case (PX P1 y P2) |
55793 | 122 |
with assms have Y0: "y > 0" |
123 |
by (cases y) auto |
|
41807 | 124 |
from assms PX have "isnorm P1" "isnorm P2" |
125 |
by (auto simp add: norm_PX1[of P1 y P2] norm_PX2[of P1 y P2]) |
|
126 |
from assms PX Y0 show ?thesis |
|
60535 | 127 |
apply (cases x) |
128 |
apply (auto simp add: mkPX_def norm_PXtrans2[of P1 y _ Q _]) |
|
129 |
apply (cases P2) |
|
130 |
apply auto |
|
131 |
done |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
132 |
qed |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
133 |
|
60533 | 134 |
text \<open>add conserves normalizedness\<close> |
44779 | 135 |
lemma add_cn: "isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<oplus> Q)" |
136 |
proof (induct P Q rule: add.induct) |
|
60535 | 137 |
case 1 |
138 |
then show ?case by simp |
|
139 |
next |
|
44779 | 140 |
case (2 c i P2) |
55793 | 141 |
then show ?case |
60535 | 142 |
apply (cases P2) |
143 |
apply simp_all |
|
144 |
apply (cases i) |
|
145 |
apply simp_all |
|
146 |
done |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
147 |
next |
44779 | 148 |
case (3 i P2 c) |
55793 | 149 |
then show ?case |
60535 | 150 |
apply (cases P2) |
151 |
apply simp_all |
|
152 |
apply (cases i) |
|
153 |
apply simp_all |
|
154 |
done |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
155 |
next |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
156 |
case (4 c P2 i Q2) |
44779 | 157 |
then have "isnorm P2" "isnorm Q2" |
158 |
by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2]) |
|
159 |
with 4 show ?case |
|
60535 | 160 |
apply (cases i) |
161 |
apply simp |
|
162 |
apply (cases P2) |
|
163 |
apply auto |
|
164 |
apply (rename_tac pol2, case_tac pol2) |
|
165 |
apply auto |
|
166 |
done |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
167 |
next |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
168 |
case (5 P2 i Q2 c) |
44779 | 169 |
then have "isnorm P2" "isnorm Q2" |
170 |
by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2]) |
|
171 |
with 5 show ?case |
|
60535 | 172 |
apply (cases i) |
173 |
apply simp |
|
174 |
apply (cases P2) |
|
175 |
apply auto |
|
176 |
apply (rename_tac pol2, case_tac pol2) |
|
177 |
apply auto |
|
178 |
done |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
179 |
next |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
180 |
case (6 x P2 y Q2) |
55793 | 181 |
then have Y0: "y > 0" |
182 |
by (cases y) (auto simp add: norm_Pinj_0_False) |
|
183 |
with 6 have X0: "x > 0" |
|
184 |
by (cases x) (auto simp add: norm_Pinj_0_False) |
|
60535 | 185 |
consider "x < y" | "x = y" | "x > y" by arith |
186 |
then show ?case |
|
187 |
proof cases |
|
188 |
case 1 |
|
189 |
then obtain d where y: "y = d + x" |
|
190 |
by atomize_elim arith |
|
191 |
from 6 have *: "isnorm P2" "isnorm Q2" |
|
44779 | 192 |
by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2]) |
60535 | 193 |
from 6 1 y have "isnorm (Pinj d Q2)" |
44779 | 194 |
by (cases d, simp, cases Q2, auto) |
60535 | 195 |
with 6 X0 y * show ?thesis |
196 |
by (simp add: mkPinj_cn) |
|
197 |
next |
|
198 |
case 2 |
|
44779 | 199 |
from 6 have "isnorm P2" "isnorm Q2" |
200 |
by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2]) |
|
60535 | 201 |
with 2 6 Y0 show ?thesis |
202 |
by (simp add: mkPinj_cn) |
|
203 |
next |
|
204 |
case 3 |
|
205 |
then obtain d where x: "x = d + y" |
|
206 |
by atomize_elim arith |
|
207 |
from 6 have *: "isnorm P2" "isnorm Q2" |
|
44779 | 208 |
by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2]) |
60535 | 209 |
from 6 3 x have "isnorm (Pinj d P2)" |
44779 | 210 |
by (cases d) (simp, cases P2, auto) |
60535 | 211 |
with 3 6 Y0 * x show ?thesis by (simp add: mkPinj_cn) |
212 |
qed |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
213 |
next |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
214 |
case (7 x P2 Q2 y R) |
60535 | 215 |
consider "x = 0" | "x = 1" | d where "x = Suc (Suc d)" |
216 |
by atomize_elim arith |
|
217 |
then show ?case |
|
218 |
proof cases |
|
219 |
case 1 |
|
220 |
with 7 show ?thesis |
|
221 |
by (auto simp add: norm_Pinj_0_False) |
|
222 |
next |
|
223 |
case 2 |
|
44779 | 224 |
from 7 have "isnorm R" "isnorm P2" |
225 |
by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R]) |
|
60535 | 226 |
with 7 2 have "isnorm (R \<oplus> P2)" |
227 |
by simp |
|
228 |
with 7 2 show ?thesis |
|
55793 | 229 |
by (simp add: norm_PXtrans[of Q2 y _]) |
60535 | 230 |
next |
231 |
case 3 |
|
41807 | 232 |
with 7 have NR: "isnorm R" "isnorm P2" |
233 |
by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R]) |
|
60535 | 234 |
with 7 3 have "isnorm (Pinj (x - 1) P2)" |
235 |
by (cases P2) auto |
|
236 |
with 7 3 NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" |
|
237 |
by simp |
|
238 |
with \<open>isnorm (PX Q2 y R)\<close> 3 show ?thesis |
|
55793 | 239 |
by (simp add: norm_PXtrans[of Q2 y _]) |
60535 | 240 |
qed |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
241 |
next |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
242 |
case (8 Q2 y R x P2) |
60535 | 243 |
consider "x = 0" | "x = 1" | "x > 1" |
244 |
by arith |
|
245 |
then show ?case |
|
246 |
proof cases |
|
247 |
case 1 |
|
248 |
with 8 show ?thesis |
|
55793 | 249 |
by (auto simp add: norm_Pinj_0_False) |
60535 | 250 |
next |
251 |
case 2 |
|
55793 | 252 |
with 8 have "isnorm R" "isnorm P2" |
253 |
by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R]) |
|
60535 | 254 |
with 8 2 have "isnorm (R \<oplus> P2)" |
55793 | 255 |
by simp |
60535 | 256 |
with 8 2 show ?thesis |
55793 | 257 |
by (simp add: norm_PXtrans[of Q2 y _]) |
60535 | 258 |
next |
259 |
case 3 |
|
260 |
then obtain d where x: "x = Suc (Suc d)" by atomize_elim arith |
|
41807 | 261 |
with 8 have NR: "isnorm R" "isnorm P2" |
262 |
by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R]) |
|
60535 | 263 |
with 8 x have "isnorm (Pinj (x - 1) P2)" |
55793 | 264 |
by (cases P2) auto |
60535 | 265 |
with 8 3 NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" |
55793 | 266 |
by simp |
60535 | 267 |
with \<open>isnorm (PX Q2 y R)\<close> x show ?thesis |
55793 | 268 |
by (simp add: norm_PXtrans[of Q2 y _]) |
60535 | 269 |
qed |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
270 |
next |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
271 |
case (9 P1 x P2 Q1 y Q2) |
55793 | 272 |
then have Y0: "y > 0" by (cases y) auto |
273 |
with 9 have X0: "x > 0" by (cases x) auto |
|
41807 | 274 |
with 9 have NP1: "isnorm P1" and NP2: "isnorm P2" |
275 |
by (auto simp add: norm_PX1[of P1 _ P2] norm_PX2[of P1 _ P2]) |
|
44779 | 276 |
with 9 have NQ1: "isnorm Q1" and NQ2: "isnorm Q2" |
41807 | 277 |
by (auto simp add: norm_PX1[of Q1 _ Q2] norm_PX2[of Q1 _ Q2]) |
60535 | 278 |
consider "y < x" | "x = y" | "x < y" by arith |
279 |
then show ?case |
|
280 |
proof cases |
|
281 |
case 1 |
|
282 |
then obtain d where x: "x = d + y" |
|
283 |
by atomize_elim arith |
|
55793 | 284 |
have "isnorm (PX P1 d (Pc 0))" |
41807 | 285 |
proof (cases P1) |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
286 |
case (PX p1 y p2) |
60535 | 287 |
with 9 1 x show ?thesis |
55793 | 288 |
by (cases d) (simp, cases p2, auto) |
41807 | 289 |
next |
55793 | 290 |
case Pc |
60535 | 291 |
with 9 1 x show ?thesis |
55793 | 292 |
by (cases d) auto |
41807 | 293 |
next |
55793 | 294 |
case Pinj |
60535 | 295 |
with 9 1 x show ?thesis |
55793 | 296 |
by (cases d) auto |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
297 |
qed |
60535 | 298 |
with 9 NQ1 NP1 NP2 NQ2 1 x have "isnorm (P2 \<oplus> Q2)" "isnorm (PX P1 (x - y) (Pc 0) \<oplus> Q1)" |
55793 | 299 |
by auto |
60535 | 300 |
with Y0 1 x show ?thesis |
55793 | 301 |
by (simp add: mkPX_cn) |
60535 | 302 |
next |
303 |
case 2 |
|
55793 | 304 |
with 9 NP1 NP2 NQ1 NQ2 have "isnorm (P2 \<oplus> Q2)" "isnorm (P1 \<oplus> Q1)" |
305 |
by auto |
|
60535 | 306 |
with 2 Y0 show ?thesis |
55793 | 307 |
by (simp add: mkPX_cn) |
60535 | 308 |
next |
309 |
case 3 |
|
310 |
then obtain d where y: "y = d + x" |
|
311 |
by atomize_elim arith |
|
55793 | 312 |
have "isnorm (PX Q1 d (Pc 0))" |
41807 | 313 |
proof (cases Q1) |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
314 |
case (PX p1 y p2) |
60535 | 315 |
with 9 3 y show ?thesis |
55793 | 316 |
by (cases d) (simp, cases p2, auto) |
41807 | 317 |
next |
55793 | 318 |
case Pc |
60535 | 319 |
with 9 3 y show ?thesis |
55793 | 320 |
by (cases d) auto |
41807 | 321 |
next |
55793 | 322 |
case Pinj |
60535 | 323 |
with 9 3 y show ?thesis |
55793 | 324 |
by (cases d) auto |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
325 |
qed |
60535 | 326 |
with 9 NQ1 NP1 NP2 NQ2 3 y have "isnorm (P2 \<oplus> Q2)" "isnorm (PX Q1 (y - x) (Pc 0) \<oplus> P1)" |
55793 | 327 |
by auto |
60535 | 328 |
with X0 3 y show ?thesis |
55793 | 329 |
by (simp add: mkPX_cn) |
60535 | 330 |
qed |
331 |
qed |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
332 |
|
60533 | 333 |
text \<open>mul concerves normalizedness\<close> |
44779 | 334 |
lemma mul_cn: "isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<otimes> Q)" |
335 |
proof (induct P Q rule: mul.induct) |
|
60535 | 336 |
case 1 |
337 |
then show ?case by simp |
|
338 |
next |
|
55793 | 339 |
case (2 c i P2) |
340 |
then show ?case |
|
60535 | 341 |
apply (cases P2) |
342 |
apply simp_all |
|
343 |
apply (cases i) |
|
344 |
apply (simp_all add: mkPinj_cn) |
|
345 |
done |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
346 |
next |
55793 | 347 |
case (3 i P2 c) |
348 |
then show ?case |
|
60535 | 349 |
apply (cases P2) |
350 |
apply simp_all |
|
351 |
apply (cases i) |
|
352 |
apply (simp_all add: mkPinj_cn) |
|
353 |
done |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
354 |
next |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
355 |
case (4 c P2 i Q2) |
44779 | 356 |
then have "isnorm P2" "isnorm Q2" |
357 |
by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2]) |
|
55793 | 358 |
with 4 show ?case |
60535 | 359 |
apply (cases "c = 0") |
360 |
apply simp_all |
|
361 |
apply (cases "i = 0") |
|
362 |
apply (simp_all add: mkPX_cn) |
|
363 |
done |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
364 |
next |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
365 |
case (5 P2 i Q2 c) |
44779 | 366 |
then have "isnorm P2" "isnorm Q2" |
367 |
by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2]) |
|
41807 | 368 |
with 5 show ?case |
60535 | 369 |
apply (cases "c = 0") |
370 |
apply simp_all |
|
371 |
apply (cases "i = 0") |
|
372 |
apply (simp_all add: mkPX_cn) |
|
373 |
done |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
374 |
next |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
375 |
case (6 x P2 y Q2) |
60535 | 376 |
consider "x < y" | "x = y" | "x > y" by arith |
377 |
then show ?case |
|
378 |
proof cases |
|
379 |
case 1 |
|
380 |
then obtain d where y: "y = d + x" |
|
381 |
by atomize_elim arith |
|
382 |
from 6 have *: "x > 0" |
|
55793 | 383 |
by (cases x) (auto simp add: norm_Pinj_0_False) |
60535 | 384 |
from 6 have **: "isnorm P2" "isnorm Q2" |
55793 | 385 |
by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2]) |
60535 | 386 |
from 6 1 y have "isnorm (Pinj d Q2)" |
387 |
apply (cases d) |
|
388 |
apply simp |
|
389 |
apply (cases Q2) |
|
390 |
apply auto |
|
391 |
done |
|
392 |
with 6 * ** y show ?thesis |
|
393 |
by (simp add: mkPinj_cn) |
|
394 |
next |
|
395 |
case 2 |
|
396 |
from 6 have *: "isnorm P2" "isnorm Q2" |
|
55793 | 397 |
by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2]) |
60535 | 398 |
from 6 have **: "y > 0" |
399 |
by (cases y) (auto simp add: norm_Pinj_0_False) |
|
400 |
with 6 2 * **show ?thesis |
|
401 |
by (simp add: mkPinj_cn) |
|
402 |
next |
|
403 |
case 3 |
|
404 |
then obtain d where x: "x = d + y" |
|
405 |
by atomize_elim arith |
|
406 |
from 6 have *: "y > 0" |
|
55793 | 407 |
by (cases y) (auto simp add: norm_Pinj_0_False) |
60535 | 408 |
from 6 have **: "isnorm P2" "isnorm Q2" |
55793 | 409 |
by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2]) |
60535 | 410 |
from 6 3 x have "isnorm (Pinj d P2)" |
411 |
apply (cases d) |
|
412 |
apply simp |
|
413 |
apply (cases P2) |
|
414 |
apply auto |
|
415 |
done |
|
416 |
with 6 3 * ** x show ?thesis |
|
417 |
by (simp add: mkPinj_cn) |
|
418 |
qed |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
419 |
next |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
420 |
case (7 x P2 Q2 y R) |
41807 | 421 |
then have Y0: "y > 0" by (cases y) auto |
60535 | 422 |
consider "x = 0" | "x = 1" | d where "x = Suc (Suc d)" |
423 |
by atomize_elim arith |
|
424 |
then show ?case |
|
425 |
proof cases |
|
426 |
case 1 |
|
427 |
with 7 show ?thesis |
|
55793 | 428 |
by (auto simp add: norm_Pinj_0_False) |
60535 | 429 |
next |
430 |
case 2 |
|
55793 | 431 |
from 7 have "isnorm R" "isnorm P2" |
432 |
by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R]) |
|
60535 | 433 |
with 7 2 have "isnorm (R \<otimes> P2)" "isnorm Q2" |
55793 | 434 |
by (auto simp add: norm_PX1[of Q2 y R]) |
60535 | 435 |
with 7 2 Y0 show ?thesis |
55793 | 436 |
by (simp add: mkPX_cn) |
60535 | 437 |
next |
438 |
case 3 |
|
439 |
from 7 have *: "isnorm R" "isnorm Q2" |
|
41807 | 440 |
by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R]) |
60535 | 441 |
from 7 3 have "isnorm (Pinj (x - 1) P2)" |
55793 | 442 |
by (cases P2) auto |
60535 | 443 |
with 7 3 * have "isnorm (R \<otimes> Pinj (x - 1) P2)" "isnorm (Pinj x P2 \<otimes> Q2)" |
55793 | 444 |
by auto |
60535 | 445 |
with Y0 3 show ?thesis |
55793 | 446 |
by (simp add: mkPX_cn) |
60535 | 447 |
qed |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
448 |
next |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
449 |
case (8 Q2 y R x P2) |
55793 | 450 |
then have Y0: "y > 0" |
451 |
by (cases y) auto |
|
60535 | 452 |
consider "x = 0" | "x = 1" | d where "x = Suc (Suc d)" |
453 |
by atomize_elim arith |
|
454 |
then show ?case |
|
455 |
proof cases |
|
456 |
case 1 |
|
457 |
with 8 show ?thesis |
|
55793 | 458 |
by (auto simp add: norm_Pinj_0_False) |
60535 | 459 |
next |
460 |
case 2 |
|
55793 | 461 |
from 8 have "isnorm R" "isnorm P2" |
462 |
by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R]) |
|
60535 | 463 |
with 8 2 have "isnorm (R \<otimes> P2)" "isnorm Q2" |
55793 | 464 |
by (auto simp add: norm_PX1[of Q2 y R]) |
60535 | 465 |
with 8 2 Y0 show ?thesis |
55793 | 466 |
by (simp add: mkPX_cn) |
60535 | 467 |
next |
468 |
case 3 |
|
469 |
from 8 have *: "isnorm R" "isnorm Q2" |
|
41807 | 470 |
by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R]) |
60535 | 471 |
from 8 3 have "isnorm (Pinj (x - 1) P2)" |
55793 | 472 |
by (cases P2) auto |
60535 | 473 |
with 8 3 * have "isnorm (R \<otimes> Pinj (x - 1) P2)" "isnorm (Pinj x P2 \<otimes> Q2)" |
55793 | 474 |
by auto |
60535 | 475 |
with Y0 3 show ?thesis |
476 |
by (simp add: mkPX_cn) |
|
477 |
qed |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
478 |
next |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
479 |
case (9 P1 x P2 Q1 y Q2) |
41807 | 480 |
from 9 have X0: "x > 0" by (cases x) auto |
481 |
from 9 have Y0: "y > 0" by (cases y) auto |
|
60535 | 482 |
from 9 have *: "isnorm P1" "isnorm P2" |
55793 | 483 |
by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2]) |
484 |
from 9 have "isnorm Q1" "isnorm Q2" |
|
485 |
by (auto simp add: norm_PX1[of Q1 y Q2] norm_PX2[of Q1 y Q2]) |
|
60535 | 486 |
with 9 * have "isnorm (P1 \<otimes> Q1)" "isnorm (P2 \<otimes> Q2)" |
55793 | 487 |
"isnorm (P1 \<otimes> mkPinj 1 Q2)" "isnorm (Q1 \<otimes> mkPinj 1 P2)" |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
488 |
by (auto simp add: mkPinj_cn) |
41807 | 489 |
with 9 X0 Y0 have |
22742
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
490 |
"isnorm (mkPX (P1 \<otimes> Q1) (x + y) (P2 \<otimes> Q2))" |
55793 | 491 |
"isnorm (mkPX (P1 \<otimes> mkPinj (Suc 0) Q2) x (Pc 0))" |
492 |
"isnorm (mkPX (Q1 \<otimes> mkPinj (Suc 0) P2) y (Pc 0))" |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
493 |
by (auto simp add: mkPX_cn) |
60535 | 494 |
then show ?case |
495 |
by (simp add: add_cn) |
|
496 |
qed |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
497 |
|
60533 | 498 |
text \<open>neg conserves normalizedness\<close> |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
499 |
lemma neg_cn: "isnorm P \<Longrightarrow> isnorm (neg P)" |
22742
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
500 |
proof (induct P) |
60535 | 501 |
case Pc |
502 |
then show ?case by simp |
|
503 |
next |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
504 |
case (Pinj i P2) |
55793 | 505 |
then have "isnorm P2" |
506 |
by (simp add: norm_Pinj[of i P2]) |
|
507 |
with Pinj show ?case |
|
508 |
by (cases P2) (auto, cases i, auto) |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
509 |
next |
41807 | 510 |
case (PX P1 x P2) note PX1 = this |
511 |
from PX have "isnorm P2" "isnorm P1" |
|
512 |
by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2]) |
|
513 |
with PX show ?case |
|
514 |
proof (cases P1) |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
515 |
case (PX p1 y p2) |
55793 | 516 |
with PX1 show ?thesis |
517 |
by (cases x) (auto, cases p2, auto) |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
518 |
next |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
519 |
case Pinj |
55793 | 520 |
with PX1 show ?thesis |
521 |
by (cases x) auto |
|
41807 | 522 |
qed (cases x, auto) |
60535 | 523 |
qed |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
524 |
|
60533 | 525 |
text \<open>sub conserves normalizedness\<close> |
44779 | 526 |
lemma sub_cn: "isnorm p \<Longrightarrow> isnorm q \<Longrightarrow> isnorm (p \<ominus> q)" |
527 |
by (simp add: sub_def add_cn neg_cn) |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
528 |
|
60533 | 529 |
text \<open>sqr conserves normalizizedness\<close> |
44779 | 530 |
lemma sqr_cn: "isnorm P \<Longrightarrow> isnorm (sqr P)" |
41807 | 531 |
proof (induct P) |
44779 | 532 |
case Pc |
533 |
then show ?case by simp |
|
534 |
next |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
535 |
case (Pinj i Q) |
41807 | 536 |
then show ?case |
60535 | 537 |
apply (cases Q) |
538 |
apply (auto simp add: mkPX_cn mkPinj_cn) |
|
539 |
apply (cases i) |
|
540 |
apply (auto simp add: mkPX_cn mkPinj_cn) |
|
541 |
done |
|
55793 | 542 |
next |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
543 |
case (PX P1 x P2) |
55754 | 544 |
then have "x + x \<noteq> 0" "isnorm P2" "isnorm P1" |
60535 | 545 |
apply (cases x) |
546 |
using PX |
|
547 |
apply (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2]) |
|
548 |
done |
|
41807 | 549 |
with PX have "isnorm (mkPX (Pc (1 + 1) \<otimes> P1 \<otimes> mkPinj (Suc 0) P2) x (Pc 0))" |
60535 | 550 |
and "isnorm (mkPX (sqr P1) (x + x) (sqr P2))" |
41807 | 551 |
by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn) |
55793 | 552 |
then show ?case |
553 |
by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn) |
|
44779 | 554 |
qed |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
555 |
|
60533 | 556 |
text \<open>pow conserves normalizedness\<close> |
44779 | 557 |
lemma pow_cn: "isnorm P \<Longrightarrow> isnorm (pow n P)" |
558 |
proof (induct n arbitrary: P rule: less_induct) |
|
559 |
case (less k) |
|
55793 | 560 |
show ?case |
41807 | 561 |
proof (cases "k = 0") |
44779 | 562 |
case True |
563 |
then show ?thesis by simp |
|
564 |
next |
|
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
565 |
case False |
60535 | 566 |
then have K2: "k div 2 < k" |
567 |
by (cases k) auto |
|
568 |
from less have "isnorm (sqr P)" |
|
569 |
by (simp add: sqr_cn) |
|
44779 | 570 |
with less False K2 show ?thesis |
58712 | 571 |
by (cases "even k") (auto simp add: mul_cn elim: evenE oddE) |
44779 | 572 |
qed |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
573 |
qed |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
574 |
|
17388 | 575 |
end |