author | wenzelm |
Tue, 25 Feb 2014 23:12:48 +0100 | |
changeset 55754 | d14072d53c1e |
parent 53374 | a14d2a854c02 |
child 55793 | 52c8f934ea6f |
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 |
||
8 |
header {* Proof of the relative completeness of method comm-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
|
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 |
|
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
14 |
text {* Formalization of normal form *} |
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 |
|
42 |
apply (case_tac pol2) |
|
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 |
|
51 |
apply (case_tac pol2) |
|
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) |
57 |
apply (case_tac nat, auto simp add: norm_Pinj_0_False) |
|
58 |
apply (case_tac pol, auto) |
|
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 |
|
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
|
62 |
lemma norm_PXtrans: |
55754 | 63 |
assumes A: "isnorm (PX P x Q)" |
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 |
76 |
with assms show ?thesis 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
|
77 |
next |
44779 | 78 |
case Pinj |
79 |
with assms show ?thesis 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 |
|
41807 | 82 |
lemma norm_PXtrans2: |
83 |
assumes "isnorm (PX P x Q)" and "isnorm Q2" |
|
55754 | 84 |
shows "isnorm (PX P (Suc (n + x)) Q2)" |
41807 | 85 |
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
|
86 |
case (PX p1 y p2) |
55754 | 87 |
with assms show ?thesis |
88 |
apply (cases x) |
|
89 |
apply auto |
|
90 |
apply (cases p2) |
|
91 |
apply auto |
|
92 |
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
|
93 |
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
|
94 |
case Pc |
41807 | 95 |
with assms show ?thesis 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
|
96 |
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
|
97 |
case Pinj |
41807 | 98 |
with assms show ?thesis 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
|
99 |
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
|
100 |
|
23266 | 101 |
text {* mkPX conserves normalizedness (@{text "_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
|
102 |
lemma mkPX_cn: |
55754 | 103 |
assumes "x \<noteq> 0" |
104 |
and "isnorm P" |
|
105 |
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
|
106 |
shows "isnorm (mkPX P x Q)" |
55754 | 107 |
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
|
108 |
case (Pc c) |
55754 | 109 |
with assms show ?thesis |
110 |
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
|
111 |
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
|
112 |
case (Pinj i Q) |
55754 | 113 |
with assms show ?thesis |
114 |
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
|
115 |
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
|
116 |
case (PX P1 y P2) |
44779 | 117 |
with assms have Y0: "y > 0" by (cases y) auto |
41807 | 118 |
from assms PX have "isnorm P1" "isnorm P2" |
119 |
by (auto simp add: norm_PX1[of P1 y P2] norm_PX2[of P1 y P2]) |
|
120 |
from assms PX Y0 show ?thesis |
|
44779 | 121 |
by (cases x) (auto simp add: mkPX_def norm_PXtrans2[of P1 y _ Q _], 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
|
122 |
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
|
123 |
|
22742
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
124 |
text {* add conserves normalizedness *} |
44779 | 125 |
lemma add_cn: "isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<oplus> Q)" |
126 |
proof (induct P Q rule: add.induct) |
|
127 |
case (2 c i P2) |
|
55754 | 128 |
then show ?case by (cases P2) (simp_all, cases i, simp_all) |
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
|
129 |
next |
44779 | 130 |
case (3 i P2 c) |
55754 | 131 |
then show ?case by (cases P2) (simp_all, cases i, simp_all) |
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 |
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
|
133 |
case (4 c P2 i Q2) |
44779 | 134 |
then have "isnorm P2" "isnorm Q2" |
135 |
by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2]) |
|
136 |
with 4 show ?case |
|
137 |
by (cases i) (simp, cases P2, auto, case_tac pol2, 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
|
138 |
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
|
139 |
case (5 P2 i Q2 c) |
44779 | 140 |
then have "isnorm P2" "isnorm Q2" |
141 |
by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2]) |
|
142 |
with 5 show ?case |
|
143 |
by (cases i) (simp, cases P2, auto, case_tac pol2, 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
|
144 |
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
|
145 |
case (6 x P2 y Q2) |
41807 | 146 |
then have Y0: "y>0" by (cases y) (auto simp add: norm_Pinj_0_False) |
147 |
with 6 have X0: "x>0" by (cases x) (auto simp add: norm_Pinj_0_False) |
|
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
|
148 |
have "x < y \<or> x = y \<or> x > y" by arith |
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
|
149 |
moreover |
55754 | 150 |
{ assume "x < y" |
151 |
then have "\<exists>d. y = d + x" by arith |
|
41807 | 152 |
then obtain d where y: "y = d + x" .. |
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 |
moreover |
41807 | 154 |
note 6 X0 |
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 |
moreover |
44779 | 156 |
from 6 have "isnorm P2" "isnorm Q2" |
157 |
by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ 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
|
158 |
moreover |
44779 | 159 |
from 6 `x < y` y have "isnorm (Pinj d Q2)" |
160 |
by (cases d, simp, cases Q2, auto) |
|
41807 | 161 |
ultimately have ?case by (simp add: mkPinj_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
|
162 |
moreover |
55754 | 163 |
{ assume "x = y" |
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 |
moreover |
44779 | 165 |
from 6 have "isnorm P2" "isnorm Q2" |
166 |
by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ 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
|
167 |
moreover |
41807 | 168 |
note 6 Y0 |
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
|
169 |
ultimately have ?case by (simp add: mkPinj_cn) } |
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
|
170 |
moreover |
55754 | 171 |
{ assume "x > y" then have "\<exists>d. x = d + y" by arith |
41807 | 172 |
then obtain d where x: "x = d + y".. |
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
|
173 |
moreover |
41807 | 174 |
note 6 Y0 |
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 |
moreover |
44779 | 176 |
from 6 have "isnorm P2" "isnorm Q2" |
177 |
by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ 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
|
178 |
moreover |
44779 | 179 |
from 6 `x > y` x have "isnorm (Pinj d P2)" |
180 |
by (cases d) (simp, cases P2, auto) |
|
181 |
ultimately have ?case by (simp add: mkPinj_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
|
182 |
ultimately show ?case by blast |
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
|
183 |
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
|
184 |
case (7 x P2 Q2 y R) |
44779 | 185 |
have "x = 0 \<or> x = 1 \<or> x > 1" by arith |
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
|
186 |
moreover |
41807 | 187 |
{ assume "x = 0" |
188 |
with 7 have ?case by (auto simp add: norm_Pinj_0_False) } |
|
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
|
189 |
moreover |
41807 | 190 |
{ assume "x = 1" |
44779 | 191 |
from 7 have "isnorm R" "isnorm P2" |
192 |
by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R]) |
|
41807 | 193 |
with 7 `x = 1` have "isnorm (R \<oplus> P2)" by simp |
44779 | 194 |
with 7 `x = 1` have ?case |
195 |
by (simp add: norm_PXtrans[of Q2 y _]) } |
|
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
|
196 |
moreover |
55754 | 197 |
{ assume "x > 1" then have "\<exists>d. x=Suc (Suc d)" by arith |
44779 | 198 |
then obtain d where X: "x=Suc (Suc d)" .. |
41807 | 199 |
with 7 have NR: "isnorm R" "isnorm P2" |
200 |
by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R]) |
|
201 |
with 7 X have "isnorm (Pinj (x - 1) P2)" by (cases P2) auto |
|
202 |
with 7 X NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" by simp |
|
44779 | 203 |
with `isnorm (PX Q2 y R)` X have ?case |
204 |
by (simp add: norm_PXtrans[of Q2 y _]) } |
|
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
|
205 |
ultimately show ?case by blast |
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
|
206 |
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
|
207 |
case (8 Q2 y R x P2) |
22742
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
208 |
have "x = 0 \<or> x = 1 \<or> x > 1" by arith |
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 |
moreover |
41807 | 210 |
{ assume "x = 0" with 8 have ?case by (auto simp add: norm_Pinj_0_False) } |
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
|
211 |
moreover |
41807 | 212 |
{ assume "x = 1" |
213 |
with 8 have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R]) |
|
214 |
with 8 `x = 1` have "isnorm (R \<oplus> P2)" by simp |
|
215 |
with 8 `x = 1` have ?case by (simp add: norm_PXtrans[of Q2 y _]) } |
|
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
|
216 |
moreover |
55754 | 217 |
{ assume "x > 1" then have "\<exists>d. x=Suc (Suc d)" by arith |
41807 | 218 |
then obtain d where X: "x = Suc (Suc d)" .. |
219 |
with 8 have NR: "isnorm R" "isnorm P2" |
|
220 |
by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R]) |
|
221 |
with 8 X have "isnorm (Pinj (x - 1) P2)" by (cases P2) auto |
|
222 |
with 8 `x > 1` NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" by simp |
|
223 |
with `isnorm (PX Q2 y R)` X have ?case by (simp add: norm_PXtrans[of Q2 y _]) } |
|
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
|
224 |
ultimately show ?case by blast |
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
|
225 |
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
|
226 |
case (9 P1 x P2 Q1 y Q2) |
41807 | 227 |
then have Y0: "y>0" by (cases y) auto |
228 |
with 9 have X0: "x>0" by (cases x) auto |
|
229 |
with 9 have NP1: "isnorm P1" and NP2: "isnorm P2" |
|
230 |
by (auto simp add: norm_PX1[of P1 _ P2] norm_PX2[of P1 _ P2]) |
|
44779 | 231 |
with 9 have NQ1: "isnorm Q1" and NQ2: "isnorm Q2" |
41807 | 232 |
by (auto simp add: norm_PX1[of Q1 _ Q2] norm_PX2[of Q1 _ 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
|
233 |
have "y < x \<or> x = y \<or> x < y" by arith |
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
|
234 |
moreover |
55754 | 235 |
{ assume sm1: "y < x" then have "\<exists>d. x = d + y" by arith |
41807 | 236 |
then obtain d where sm2: "x = d + y" .. |
237 |
note 9 NQ1 NP1 NP2 NQ2 sm1 sm2 |
|
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
|
238 |
moreover |
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
|
239 |
have "isnorm (PX P1 d (Pc 0))" |
41807 | 240 |
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
|
241 |
case (PX p1 y p2) |
44779 | 242 |
with 9 sm1 sm2 show ?thesis by (cases d) (simp, cases p2, auto) |
41807 | 243 |
next |
244 |
case Pc with 9 sm1 sm2 show ?thesis by (cases d) auto |
|
245 |
next |
|
246 |
case Pinj with 9 sm1 sm2 show ?thesis 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
|
247 |
qed |
22742
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
248 |
ultimately have "isnorm (P2 \<oplus> Q2)" "isnorm (PX P1 (x - y) (Pc 0) \<oplus> Q1)" by auto |
41807 | 249 |
with Y0 sm1 sm2 have ?case by (simp add: mkPX_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
|
250 |
moreover |
41807 | 251 |
{ assume "x = y" |
252 |
with 9 NP1 NP2 NQ1 NQ2 have "isnorm (P2 \<oplus> Q2)" "isnorm (P1 \<oplus> Q1)" by auto |
|
253 |
with `x = y` Y0 have ?case by (simp add: mkPX_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
|
254 |
moreover |
55754 | 255 |
{ assume sm1: "x < y" then have "\<exists>d. y = d + x" by arith |
41807 | 256 |
then obtain d where sm2: "y = d + x" .. |
257 |
note 9 NQ1 NP1 NP2 NQ2 sm1 sm2 |
|
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
|
258 |
moreover |
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
|
259 |
have "isnorm (PX Q1 d (Pc 0))" |
41807 | 260 |
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
|
261 |
case (PX p1 y p2) |
44779 | 262 |
with 9 sm1 sm2 show ?thesis by (cases d) (simp, cases p2, auto) |
41807 | 263 |
next |
264 |
case Pc with 9 sm1 sm2 show ?thesis by (cases d) auto |
|
265 |
next |
|
266 |
case Pinj with 9 sm1 sm2 show ?thesis 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
|
267 |
qed |
22742
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
268 |
ultimately have "isnorm (P2 \<oplus> Q2)" "isnorm (PX Q1 (y - x) (Pc 0) \<oplus> P1)" by auto |
44779 | 269 |
with X0 sm1 sm2 have ?case by (simp add: mkPX_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
|
270 |
ultimately show ?case by blast |
22742
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
271 |
qed simp |
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
|
272 |
|
22742
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
273 |
text {* mul concerves normalizedness *} |
44779 | 274 |
lemma mul_cn: "isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<otimes> Q)" |
275 |
proof (induct P Q rule: mul.induct) |
|
55754 | 276 |
case (2 c i P2) then show ?case |
44779 | 277 |
by (cases P2) (simp_all, cases i, simp_all add: mkPinj_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
|
278 |
next |
55754 | 279 |
case (3 i P2 c) then show ?case |
44779 | 280 |
by (cases P2) (simp_all, cases i, simp_all add: mkPinj_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
|
281 |
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
|
282 |
case (4 c P2 i Q2) |
44779 | 283 |
then have "isnorm P2" "isnorm Q2" |
284 |
by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2]) |
|
41807 | 285 |
with 4 show ?case |
44779 | 286 |
by (cases "c = 0") (simp_all, cases "i = 0", simp_all add: mkPX_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
|
287 |
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
|
288 |
case (5 P2 i Q2 c) |
44779 | 289 |
then have "isnorm P2" "isnorm Q2" |
290 |
by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2]) |
|
41807 | 291 |
with 5 show ?case |
44779 | 292 |
by (cases "c = 0") (simp_all, cases "i = 0", simp_all add: mkPX_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
|
293 |
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
|
294 |
case (6 x P2 y Q2) |
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
|
295 |
have "x < y \<or> x = y \<or> x > y" by arith |
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
|
296 |
moreover |
55754 | 297 |
{ assume "x < y" then have "\<exists>d. y = d + x" by arith |
41807 | 298 |
then obtain d where y: "y = d + x" .. |
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
|
299 |
moreover |
41807 | 300 |
note 6 |
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
|
301 |
moreover |
41807 | 302 |
from 6 have "x > 0" by (cases x) (auto simp add: norm_Pinj_0_False) |
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
|
303 |
moreover |
41807 | 304 |
from 6 have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ 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
|
305 |
moreover |
44779 | 306 |
from 6 `x < y` y have "isnorm (Pinj d Q2)" by (cases d) (simp, cases Q2, auto) |
41807 | 307 |
ultimately have ?case by (simp add: mkPinj_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
|
308 |
moreover |
41807 | 309 |
{ assume "x = y" |
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 |
moreover |
41807 | 311 |
from 6 have "isnorm P2" "isnorm Q2" by(auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ 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
|
312 |
moreover |
41807 | 313 |
from 6 have "y>0" by (cases y) (auto simp add: norm_Pinj_0_False) |
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 |
moreover |
41807 | 315 |
note 6 |
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
|
316 |
ultimately have ?case by (simp add: mkPinj_cn) } |
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
|
317 |
moreover |
55754 | 318 |
{ assume "x > y" then have "\<exists>d. x = d + y" by arith |
41807 | 319 |
then obtain d where x: "x = d + y" .. |
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
|
320 |
moreover |
41807 | 321 |
note 6 |
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
|
322 |
moreover |
41807 | 323 |
from 6 have "y > 0" by (cases y) (auto simp add: norm_Pinj_0_False) |
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
|
324 |
moreover |
41807 | 325 |
from 6 have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ 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
|
326 |
moreover |
44779 | 327 |
from 6 `x > y` x have "isnorm (Pinj d P2)" by (cases d) (simp, 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
|
328 |
ultimately have ?case by (simp add: mkPinj_cn) } |
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
|
329 |
ultimately show ?case by blast |
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
|
330 |
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
|
331 |
case (7 x P2 Q2 y R) |
41807 | 332 |
then have Y0: "y > 0" by (cases y) auto |
333 |
have "x = 0 \<or> x = 1 \<or> x > 1" by arith |
|
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
|
334 |
moreover |
41807 | 335 |
{ assume "x = 0" with 7 have ?case by (auto simp add: norm_Pinj_0_False) } |
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
|
336 |
moreover |
41807 | 337 |
{ assume "x = 1" |
338 |
from 7 have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R]) |
|
339 |
with 7 `x = 1` have "isnorm (R \<otimes> P2)" "isnorm Q2" by (auto simp add: norm_PX1[of Q2 y R]) |
|
340 |
with 7 `x = 1` Y0 have ?case by (simp add: mkPX_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
|
341 |
moreover |
55754 | 342 |
{ assume "x > 1" then have "\<exists>d. x = Suc (Suc d)" by arith |
41807 | 343 |
then obtain d where X: "x = Suc (Suc d)" .. |
344 |
from 7 have NR: "isnorm R" "isnorm Q2" |
|
345 |
by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R]) |
|
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 |
moreover |
41807 | 347 |
from 7 X have "isnorm (Pinj (x - 1) P2)" by (cases P2) auto |
348 |
moreover |
|
349 |
from 7 have "isnorm (Pinj x P2)" by (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
|
350 |
moreover |
41807 | 351 |
note 7 X |
22742
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
352 |
ultimately have "isnorm (R \<otimes> Pinj (x - 1) P2)" "isnorm (Pinj x P2 \<otimes> Q2)" by auto |
41807 | 353 |
with Y0 X have ?case by (simp add: mkPX_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
|
354 |
ultimately show ?case by blast |
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 |
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
|
356 |
case (8 Q2 y R x P2) |
55754 | 357 |
then have Y0: "y > 0" by (cases y) auto |
41807 | 358 |
have "x = 0 \<or> x = 1 \<or> x > 1" by arith |
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
|
359 |
moreover |
41807 | 360 |
{ assume "x = 0" with 8 have ?case by (auto simp add: norm_Pinj_0_False) } |
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
|
361 |
moreover |
41807 | 362 |
{ assume "x = 1" |
363 |
from 8 have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R]) |
|
364 |
with 8 `x = 1` have "isnorm (R \<otimes> P2)" "isnorm Q2" by (auto simp add: norm_PX1[of Q2 y R]) |
|
365 |
with 8 `x = 1` Y0 have ?case by (simp add: mkPX_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
|
366 |
moreover |
55754 | 367 |
{ assume "x > 1" then have "\<exists>d. x = Suc (Suc d)" by arith |
41807 | 368 |
then obtain d where X: "x = Suc (Suc d)" .. |
369 |
from 8 have NR: "isnorm R" "isnorm Q2" |
|
370 |
by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R]) |
|
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
|
371 |
moreover |
41807 | 372 |
from 8 X have "isnorm (Pinj (x - 1) P2)" by (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
|
373 |
moreover |
41807 | 374 |
from 8 X have "isnorm (Pinj x P2)" by (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
|
375 |
moreover |
41807 | 376 |
note 8 X |
22742
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
377 |
ultimately have "isnorm (R \<otimes> Pinj (x - 1) P2)" "isnorm (Pinj x P2 \<otimes> Q2)" by 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
|
378 |
with Y0 X have ?case by (simp add: mkPX_cn) } |
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
|
379 |
ultimately show ?case by blast |
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
|
380 |
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
|
381 |
case (9 P1 x P2 Q1 y Q2) |
41807 | 382 |
from 9 have X0: "x > 0" by (cases x) auto |
383 |
from 9 have Y0: "y > 0" by (cases y) auto |
|
384 |
note 9 |
|
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
|
385 |
moreover |
41807 | 386 |
from 9 have "isnorm P1" "isnorm P2" by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x 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
|
387 |
moreover |
41807 | 388 |
from 9 have "isnorm Q1" "isnorm Q2" by (auto simp add: norm_PX1[of Q1 y Q2] norm_PX2[of Q1 y Q2]) |
22742
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
389 |
ultimately have "isnorm (P1 \<otimes> Q1)" "isnorm (P2 \<otimes> Q2)" |
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
390 |
"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
|
391 |
by (auto simp add: mkPinj_cn) |
41807 | 392 |
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
|
393 |
"isnorm (mkPX (P1 \<otimes> Q1) (x + y) (P2 \<otimes> Q2))" |
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
394 |
"isnorm (mkPX (P1 \<otimes> mkPinj (Suc 0) Q2) x (Pc 0))" |
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
395 |
"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
|
396 |
by (auto simp add: mkPX_cn) |
55754 | 397 |
then show ?case by (simp add: add_cn) |
41807 | 398 |
qed simp |
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
|
399 |
|
22742
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
400 |
text {* neg conserves normalizedness *} |
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
|
401 |
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
|
402 |
proof (induct 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
|
403 |
case (Pinj i P2) |
41807 | 404 |
then have "isnorm P2" by (simp add: norm_Pinj[of i P2]) |
44779 | 405 |
with Pinj show ?case 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
|
406 |
next |
41807 | 407 |
case (PX P1 x P2) note PX1 = this |
408 |
from PX have "isnorm P2" "isnorm P1" |
|
409 |
by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2]) |
|
410 |
with PX show ?case |
|
411 |
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
|
412 |
case (PX p1 y p2) |
44779 | 413 |
with PX1 show ?thesis 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
|
414 |
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
|
415 |
case Pinj |
41807 | 416 |
with PX1 show ?thesis by (cases x) auto |
417 |
qed (cases x, auto) |
|
418 |
qed simp |
|
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 |
|
22742
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
420 |
text {* sub conserves normalizedness *} |
44779 | 421 |
lemma sub_cn: "isnorm p \<Longrightarrow> isnorm q \<Longrightarrow> isnorm (p \<ominus> q)" |
422 |
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
|
423 |
|
22742
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
424 |
text {* sqr conserves normalizizedness *} |
44779 | 425 |
lemma sqr_cn: "isnorm P \<Longrightarrow> isnorm (sqr P)" |
41807 | 426 |
proof (induct P) |
44779 | 427 |
case Pc |
428 |
then show ?case by simp |
|
429 |
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
|
430 |
case (Pinj i Q) |
41807 | 431 |
then show ?case |
44779 | 432 |
by (cases Q) (auto simp add: mkPX_cn mkPinj_cn, cases i, auto simp add: mkPX_cn mkPinj_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
|
433 |
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
|
434 |
case (PX P1 x P2) |
55754 | 435 |
then have "x + x \<noteq> 0" "isnorm P2" "isnorm P1" |
41807 | 436 |
by (cases x, auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2]) |
437 |
with PX have "isnorm (mkPX (Pc (1 + 1) \<otimes> P1 \<otimes> mkPinj (Suc 0) P2) x (Pc 0))" |
|
438 |
and "isnorm (mkPX (sqr P1) (x + x) (sqr P2))" |
|
439 |
by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn) |
|
440 |
then show ?case by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn) |
|
44779 | 441 |
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
|
442 |
|
22742
06165e40e7bd
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
haftmann
parents:
17508
diff
changeset
|
443 |
text {* pow conserves normalizedness *} |
44779 | 444 |
lemma pow_cn: "isnorm P \<Longrightarrow> isnorm (pow n P)" |
445 |
proof (induct n arbitrary: P rule: less_induct) |
|
446 |
case (less k) |
|
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
|
447 |
show ?case |
41807 | 448 |
proof (cases "k = 0") |
44779 | 449 |
case True |
450 |
then show ?thesis by simp |
|
451 |
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
|
452 |
case False |
41807 | 453 |
then have K2: "k div 2 < k" by (cases k) auto |
44779 | 454 |
from less have "isnorm (sqr P)" by (simp add: sqr_cn) |
455 |
with less False K2 show ?thesis |
|
456 |
by (simp add: allE[of _ "(k div 2)" _] allE[of _ "(sqr P)" _], cases k, auto simp add: mul_cn) |
|
457 |
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
|
458 |
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
|
459 |
|
17388 | 460 |
end |