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