author | haftmann |
Sun, 23 Feb 2014 10:33:43 +0100 | |
changeset 55685 | 3f8bdc5364a9 |
parent 55584 | a879f14b6f95 |
child 55814 | aefa1db74d9d |
permissions | -rw-r--r-- |
30439 | 1 |
(* Title: HOL/Decision_Procs/Cooper.thy |
27456 | 2 |
Author: Amine Chaieb |
3 |
*) |
|
4 |
||
29788 | 5 |
theory Cooper |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
50313
diff
changeset
|
6 |
imports Complex_Main "~~/src/HOL/Library/Code_Target_Numeral" "~~/src/HOL/Library/Old_Recdef" |
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23315
diff
changeset
|
7 |
begin |
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
|
8 |
|
105519771c67
The oracle for 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 |
(* Periodicity of dvd *) |
23315 | 10 |
|
23274 | 11 |
(*********************************************************************************) |
12 |
(**** SHADOW SYNTAX AND SEMANTICS ****) |
|
13 |
(*********************************************************************************) |
|
14 |
||
50313 | 15 |
datatype num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num |
23274 | 16 |
| Mul int num |
17 |
||
50313 | 18 |
primrec num_size :: "num \<Rightarrow> nat" -- {* A size for num to make inductive proofs simpler *} |
19 |
where |
|
23274 | 20 |
"num_size (C c) = 1" |
27456 | 21 |
| "num_size (Bound n) = 1" |
22 |
| "num_size (Neg a) = 1 + num_size a" |
|
23 |
| "num_size (Add a b) = 1 + num_size a + num_size b" |
|
24 |
| "num_size (Sub a b) = 3 + num_size a + num_size b" |
|
25 |
| "num_size (CN n c a) = 4 + num_size a" |
|
26 |
| "num_size (Mul c a) = 1 + num_size a" |
|
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
|
27 |
|
27456 | 28 |
primrec Inum :: "int list \<Rightarrow> num \<Rightarrow> int" where |
23274 | 29 |
"Inum bs (C c) = c" |
27456 | 30 |
| "Inum bs (Bound n) = bs!n" |
31 |
| "Inum bs (CN n c a) = c * (bs!n) + (Inum bs a)" |
|
32 |
| "Inum bs (Neg a) = -(Inum bs a)" |
|
33 |
| "Inum bs (Add a b) = Inum bs a + Inum bs b" |
|
34 |
| "Inum bs (Sub a b) = Inum bs a - Inum bs b" |
|
35 |
| "Inum bs (Mul c a) = c* Inum bs a" |
|
23274 | 36 |
|
50313 | 37 |
datatype fm = |
23274 | 38 |
T| F| Lt num| Le num| Gt num| Ge num| Eq num| NEq num| Dvd int num| NDvd int num| |
50313 | 39 |
NOT fm| And fm fm| Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm |
23274 | 40 |
| Closed nat | NClosed nat |
41 |
||
42 |
||
50313 | 43 |
fun fmsize :: "fm \<Rightarrow> nat" -- {* A size for fm *} |
44 |
where |
|
23274 | 45 |
"fmsize (NOT p) = 1 + fmsize p" |
41837 | 46 |
| "fmsize (And p q) = 1 + fmsize p + fmsize q" |
47 |
| "fmsize (Or p q) = 1 + fmsize p + fmsize q" |
|
48 |
| "fmsize (Imp p q) = 3 + fmsize p + fmsize q" |
|
49 |
| "fmsize (Iff p q) = 3 + 2*(fmsize p + fmsize q)" |
|
50 |
| "fmsize (E p) = 1 + fmsize p" |
|
51 |
| "fmsize (A p) = 4+ fmsize p" |
|
52 |
| "fmsize (Dvd i t) = 2" |
|
53 |
| "fmsize (NDvd i t) = 2" |
|
54 |
| "fmsize p = 1" |
|
50313 | 55 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31952
diff
changeset
|
56 |
lemma fmsize_pos: "fmsize p > 0" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31952
diff
changeset
|
57 |
by (induct p rule: fmsize.induct) 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
|
58 |
|
50313 | 59 |
primrec Ifm :: "bool list \<Rightarrow> int list \<Rightarrow> fm \<Rightarrow> bool" -- {* Semantics of formulae (fm) *} |
60 |
where |
|
23274 | 61 |
"Ifm bbs bs T = True" |
39246 | 62 |
| "Ifm bbs bs F = False" |
63 |
| "Ifm bbs bs (Lt a) = (Inum bs a < 0)" |
|
64 |
| "Ifm bbs bs (Gt a) = (Inum bs a > 0)" |
|
65 |
| "Ifm bbs bs (Le a) = (Inum bs a \<le> 0)" |
|
66 |
| "Ifm bbs bs (Ge a) = (Inum bs a \<ge> 0)" |
|
67 |
| "Ifm bbs bs (Eq a) = (Inum bs a = 0)" |
|
68 |
| "Ifm bbs bs (NEq a) = (Inum bs a \<noteq> 0)" |
|
69 |
| "Ifm bbs bs (Dvd i b) = (i dvd Inum bs b)" |
|
70 |
| "Ifm bbs bs (NDvd i b) = (\<not>(i dvd Inum bs b))" |
|
71 |
| "Ifm bbs bs (NOT p) = (\<not> (Ifm bbs bs p))" |
|
72 |
| "Ifm bbs bs (And p q) = (Ifm bbs bs p \<and> Ifm bbs bs q)" |
|
73 |
| "Ifm bbs bs (Or p q) = (Ifm bbs bs p \<or> Ifm bbs bs q)" |
|
74 |
| "Ifm bbs bs (Imp p q) = ((Ifm bbs bs p) \<longrightarrow> (Ifm bbs bs q))" |
|
75 |
| "Ifm bbs bs (Iff p q) = (Ifm bbs bs p = Ifm bbs bs q)" |
|
50313 | 76 |
| "Ifm bbs bs (E p) = (\<exists>x. Ifm bbs (x#bs) p)" |
77 |
| "Ifm bbs bs (A p) = (\<forall>x. Ifm bbs (x#bs) p)" |
|
39246 | 78 |
| "Ifm bbs bs (Closed n) = bbs!n" |
79 |
| "Ifm bbs bs (NClosed n) = (\<not> bbs!n)" |
|
23274 | 80 |
|
81 |
consts prep :: "fm \<Rightarrow> fm" |
|
82 |
recdef prep "measure fmsize" |
|
83 |
"prep (E T) = T" |
|
84 |
"prep (E F) = F" |
|
85 |
"prep (E (Or p q)) = Or (prep (E p)) (prep (E q))" |
|
86 |
"prep (E (Imp p q)) = Or (prep (E (NOT p))) (prep (E q))" |
|
50313 | 87 |
"prep (E (Iff p q)) = Or (prep (E (And p q))) (prep (E (And (NOT p) (NOT q))))" |
23274 | 88 |
"prep (E (NOT (And p q))) = Or (prep (E (NOT p))) (prep (E(NOT q)))" |
89 |
"prep (E (NOT (Imp p q))) = prep (E (And p (NOT q)))" |
|
90 |
"prep (E (NOT (Iff p q))) = Or (prep (E (And p (NOT q)))) (prep (E(And (NOT p) q)))" |
|
91 |
"prep (E p) = E (prep p)" |
|
92 |
"prep (A (And p q)) = And (prep (A p)) (prep (A q))" |
|
93 |
"prep (A p) = prep (NOT (E (NOT p)))" |
|
94 |
"prep (NOT (NOT p)) = prep p" |
|
95 |
"prep (NOT (And p q)) = Or (prep (NOT p)) (prep (NOT q))" |
|
96 |
"prep (NOT (A p)) = prep (E (NOT p))" |
|
97 |
"prep (NOT (Or p q)) = And (prep (NOT p)) (prep (NOT q))" |
|
98 |
"prep (NOT (Imp p q)) = And (prep p) (prep (NOT q))" |
|
99 |
"prep (NOT (Iff p q)) = Or (prep (And p (NOT q))) (prep (And (NOT p) q))" |
|
100 |
"prep (NOT p) = NOT (prep p)" |
|
101 |
"prep (Or p q) = Or (prep p) (prep q)" |
|
102 |
"prep (And p q) = And (prep p) (prep q)" |
|
103 |
"prep (Imp p q) = prep (Or (NOT p) q)" |
|
104 |
"prep (Iff p q) = Or (prep (And p q)) (prep (And (NOT p) (NOT q)))" |
|
105 |
"prep p = p" |
|
50313 | 106 |
(hints simp add: fmsize_pos) |
107 |
||
23274 | 108 |
lemma prep: "Ifm bbs bs (prep p) = Ifm bbs bs p" |
50313 | 109 |
by (induct p arbitrary: bs rule: prep.induct) auto |
23274 | 110 |
|
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 |
|
50313 | 112 |
fun qfree :: "fm \<Rightarrow> bool" -- {* Quantifier freeness *} |
113 |
where |
|
23274 | 114 |
"qfree (E p) = False" |
41837 | 115 |
| "qfree (A p) = False" |
50313 | 116 |
| "qfree (NOT p) = qfree p" |
117 |
| "qfree (And p q) = (qfree p \<and> qfree q)" |
|
118 |
| "qfree (Or p q) = (qfree p \<and> qfree q)" |
|
119 |
| "qfree (Imp p q) = (qfree p \<and> qfree q)" |
|
41837 | 120 |
| "qfree (Iff p q) = (qfree p \<and> qfree q)" |
121 |
| "qfree p = True" |
|
23274 | 122 |
|
50313 | 123 |
|
124 |
text {* Boundedness and substitution *} |
|
125 |
||
126 |
primrec numbound0 :: "num \<Rightarrow> bool" -- {* a num is INDEPENDENT of Bound 0 *} |
|
127 |
where |
|
23274 | 128 |
"numbound0 (C c) = True" |
39246 | 129 |
| "numbound0 (Bound n) = (n>0)" |
130 |
| "numbound0 (CN n i a) = (n >0 \<and> numbound0 a)" |
|
131 |
| "numbound0 (Neg a) = numbound0 a" |
|
132 |
| "numbound0 (Add a b) = (numbound0 a \<and> numbound0 b)" |
|
50313 | 133 |
| "numbound0 (Sub a b) = (numbound0 a \<and> numbound0 b)" |
39246 | 134 |
| "numbound0 (Mul i a) = numbound0 a" |
23274 | 135 |
|
136 |
lemma numbound0_I: |
|
137 |
assumes nb: "numbound0 a" |
|
138 |
shows "Inum (b#bs) a = Inum (b'#bs) a" |
|
50313 | 139 |
using nb by (induct a rule: num.induct) (auto simp add: gr0_conv_Suc) |
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
|
140 |
|
50313 | 141 |
primrec bound0 :: "fm \<Rightarrow> bool" -- {* A Formula is independent of Bound 0 *} |
142 |
where |
|
23274 | 143 |
"bound0 T = True" |
39246 | 144 |
| "bound0 F = True" |
145 |
| "bound0 (Lt a) = numbound0 a" |
|
146 |
| "bound0 (Le a) = numbound0 a" |
|
147 |
| "bound0 (Gt a) = numbound0 a" |
|
148 |
| "bound0 (Ge a) = numbound0 a" |
|
149 |
| "bound0 (Eq a) = numbound0 a" |
|
150 |
| "bound0 (NEq a) = numbound0 a" |
|
151 |
| "bound0 (Dvd i a) = numbound0 a" |
|
152 |
| "bound0 (NDvd i a) = numbound0 a" |
|
153 |
| "bound0 (NOT p) = bound0 p" |
|
154 |
| "bound0 (And p q) = (bound0 p \<and> bound0 q)" |
|
155 |
| "bound0 (Or p q) = (bound0 p \<and> bound0 q)" |
|
156 |
| "bound0 (Imp p q) = ((bound0 p) \<and> (bound0 q))" |
|
157 |
| "bound0 (Iff p q) = (bound0 p \<and> bound0 q)" |
|
158 |
| "bound0 (E p) = False" |
|
159 |
| "bound0 (A p) = False" |
|
160 |
| "bound0 (Closed P) = True" |
|
161 |
| "bound0 (NClosed P) = True" |
|
50313 | 162 |
|
23274 | 163 |
lemma bound0_I: |
164 |
assumes bp: "bound0 p" |
|
165 |
shows "Ifm bbs (b#bs) p = Ifm bbs (b'#bs) p" |
|
50313 | 166 |
using bp numbound0_I[where b="b" and bs="bs" and b'="b'"] |
167 |
by (induct p rule: fm.induct) (auto simp add: gr0_conv_Suc) |
|
23274 | 168 |
|
50313 | 169 |
fun numsubst0 :: "num \<Rightarrow> num \<Rightarrow> num" |
170 |
where |
|
23274 | 171 |
"numsubst0 t (C c) = (C c)" |
23995
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
172 |
| "numsubst0 t (Bound n) = (if n=0 then t else Bound n)" |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
173 |
| "numsubst0 t (CN 0 i a) = Add (Mul i t) (numsubst0 t a)" |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
174 |
| "numsubst0 t (CN n i a) = CN n i (numsubst0 t a)" |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
175 |
| "numsubst0 t (Neg a) = Neg (numsubst0 t a)" |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
176 |
| "numsubst0 t (Add a b) = Add (numsubst0 t a) (numsubst0 t b)" |
50313 | 177 |
| "numsubst0 t (Sub a b) = Sub (numsubst0 t a) (numsubst0 t b)" |
23995
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
178 |
| "numsubst0 t (Mul i a) = Mul i (numsubst0 t a)" |
23274 | 179 |
|
50313 | 180 |
lemma numsubst0_I: "Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b#bs) a)#bs) t" |
181 |
by (induct t rule: numsubst0.induct) (auto simp: nth_Cons') |
|
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 |
|
23274 | 183 |
lemma numsubst0_I': |
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset
|
184 |
"numbound0 a \<Longrightarrow> Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b'#bs) a)#bs) t" |
50313 | 185 |
by (induct t rule: numsubst0.induct) (auto simp: nth_Cons' numbound0_I[where b="b" and b'="b'"]) |
23274 | 186 |
|
50313 | 187 |
primrec subst0:: "num \<Rightarrow> fm \<Rightarrow> fm" -- {* substitue a num into a formula for Bound 0 *} |
188 |
where |
|
23274 | 189 |
"subst0 t T = T" |
39246 | 190 |
| "subst0 t F = F" |
191 |
| "subst0 t (Lt a) = Lt (numsubst0 t a)" |
|
192 |
| "subst0 t (Le a) = Le (numsubst0 t a)" |
|
193 |
| "subst0 t (Gt a) = Gt (numsubst0 t a)" |
|
194 |
| "subst0 t (Ge a) = Ge (numsubst0 t a)" |
|
195 |
| "subst0 t (Eq a) = Eq (numsubst0 t a)" |
|
196 |
| "subst0 t (NEq a) = NEq (numsubst0 t a)" |
|
197 |
| "subst0 t (Dvd i a) = Dvd i (numsubst0 t a)" |
|
198 |
| "subst0 t (NDvd i a) = NDvd i (numsubst0 t a)" |
|
199 |
| "subst0 t (NOT p) = NOT (subst0 t p)" |
|
200 |
| "subst0 t (And p q) = And (subst0 t p) (subst0 t q)" |
|
201 |
| "subst0 t (Or p q) = Or (subst0 t p) (subst0 t q)" |
|
202 |
| "subst0 t (Imp p q) = Imp (subst0 t p) (subst0 t q)" |
|
203 |
| "subst0 t (Iff p q) = Iff (subst0 t p) (subst0 t q)" |
|
204 |
| "subst0 t (Closed P) = (Closed P)" |
|
205 |
| "subst0 t (NClosed P) = (NClosed P)" |
|
23274 | 206 |
|
50313 | 207 |
lemma subst0_I: |
208 |
assumes qfp: "qfree p" |
|
23274 | 209 |
shows "Ifm bbs (b#bs) (subst0 a p) = Ifm bbs ((Inum (b#bs) a)#bs) p" |
210 |
using qfp numsubst0_I[where b="b" and bs="bs" and a="a"] |
|
23689
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23515
diff
changeset
|
211 |
by (induct p) (simp_all add: gr0_conv_Suc) |
23274 | 212 |
|
50313 | 213 |
fun decrnum:: "num \<Rightarrow> num" |
214 |
where |
|
23274 | 215 |
"decrnum (Bound n) = Bound (n - 1)" |
41837 | 216 |
| "decrnum (Neg a) = Neg (decrnum a)" |
217 |
| "decrnum (Add a b) = Add (decrnum a) (decrnum b)" |
|
218 |
| "decrnum (Sub a b) = Sub (decrnum a) (decrnum b)" |
|
219 |
| "decrnum (Mul c a) = Mul c (decrnum a)" |
|
220 |
| "decrnum (CN n i a) = (CN (n - 1) i (decrnum a))" |
|
221 |
| "decrnum a = a" |
|
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
|
222 |
|
50313 | 223 |
fun decr :: "fm \<Rightarrow> fm" |
224 |
where |
|
23274 | 225 |
"decr (Lt a) = Lt (decrnum a)" |
41837 | 226 |
| "decr (Le a) = Le (decrnum a)" |
227 |
| "decr (Gt a) = Gt (decrnum a)" |
|
228 |
| "decr (Ge a) = Ge (decrnum a)" |
|
229 |
| "decr (Eq a) = Eq (decrnum a)" |
|
230 |
| "decr (NEq a) = NEq (decrnum a)" |
|
231 |
| "decr (Dvd i a) = Dvd i (decrnum a)" |
|
232 |
| "decr (NDvd i a) = NDvd i (decrnum a)" |
|
50313 | 233 |
| "decr (NOT p) = NOT (decr p)" |
41837 | 234 |
| "decr (And p q) = And (decr p) (decr q)" |
235 |
| "decr (Or p q) = Or (decr p) (decr q)" |
|
236 |
| "decr (Imp p q) = Imp (decr p) (decr q)" |
|
237 |
| "decr (Iff p q) = Iff (decr p) (decr q)" |
|
238 |
| "decr p = p" |
|
23274 | 239 |
|
50313 | 240 |
lemma decrnum: |
241 |
assumes nb: "numbound0 t" |
|
23274 | 242 |
shows "Inum (x#bs) t = Inum bs (decrnum t)" |
50313 | 243 |
using nb by (induct t rule: decrnum.induct) (auto simp add: gr0_conv_Suc) |
23274 | 244 |
|
50313 | 245 |
lemma decr: |
246 |
assumes nb: "bound0 p" |
|
23274 | 247 |
shows "Ifm bbs (x#bs) p = Ifm bbs bs (decr p)" |
50313 | 248 |
using nb by (induct p rule: decr.induct) (simp_all add: gr0_conv_Suc decrnum) |
23274 | 249 |
|
250 |
lemma decr_qf: "bound0 p \<Longrightarrow> qfree (decr p)" |
|
50313 | 251 |
by (induct p) simp_all |
23274 | 252 |
|
50313 | 253 |
fun isatom :: "fm \<Rightarrow> bool" -- {* test for atomicity *} |
254 |
where |
|
23274 | 255 |
"isatom T = True" |
41837 | 256 |
| "isatom F = True" |
257 |
| "isatom (Lt a) = True" |
|
258 |
| "isatom (Le a) = True" |
|
259 |
| "isatom (Gt a) = True" |
|
260 |
| "isatom (Ge a) = True" |
|
261 |
| "isatom (Eq a) = True" |
|
262 |
| "isatom (NEq a) = True" |
|
263 |
| "isatom (Dvd i b) = True" |
|
264 |
| "isatom (NDvd i b) = True" |
|
265 |
| "isatom (Closed P) = True" |
|
266 |
| "isatom (NClosed P) = True" |
|
267 |
| "isatom p = 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
|
268 |
|
50313 | 269 |
lemma numsubst0_numbound0: |
270 |
assumes nb: "numbound0 t" |
|
23274 | 271 |
shows "numbound0 (numsubst0 t a)" |
50313 | 272 |
using nb apply (induct a) |
273 |
apply simp_all |
|
274 |
apply (case_tac nat, simp_all) |
|
275 |
done |
|
23274 | 276 |
|
50313 | 277 |
lemma subst0_bound0: |
278 |
assumes qf: "qfree p" and nb: "numbound0 t" |
|
23274 | 279 |
shows "bound0 (subst0 t p)" |
50313 | 280 |
using qf numsubst0_numbound0[OF nb] by (induct p) auto |
23274 | 281 |
|
282 |
lemma bound0_qf: "bound0 p \<Longrightarrow> qfree p" |
|
50313 | 283 |
by (induct p) simp_all |
23274 | 284 |
|
285 |
||
50313 | 286 |
definition djf :: "('a \<Rightarrow> fm) \<Rightarrow> 'a \<Rightarrow> fm \<Rightarrow> fm" |
287 |
where |
|
288 |
"djf f p q = |
|
289 |
(if q = T then T |
|
290 |
else if q = F then f p |
|
291 |
else (let fp = f p in case fp of T \<Rightarrow> T | F \<Rightarrow> q | _ \<Rightarrow> Or (f p) q))" |
|
292 |
||
293 |
definition evaldjf :: "('a \<Rightarrow> fm) \<Rightarrow> 'a list \<Rightarrow> fm" |
|
294 |
where "evaldjf f ps = foldr (djf f) ps F" |
|
23274 | 295 |
|
296 |
lemma djf_Or: "Ifm bbs bs (djf f p q) = Ifm bbs bs (Or (f p) q)" |
|
50313 | 297 |
by (cases "q=T", simp add: djf_def,cases "q=F",simp add: djf_def) |
298 |
(cases "f p", simp_all add: Let_def djf_def) |
|
23274 | 299 |
|
50313 | 300 |
lemma evaldjf_ex: "Ifm bbs bs (evaldjf f ps) = (\<exists>p \<in> set ps. Ifm bbs bs (f p))" |
301 |
by (induct ps) (simp_all add: evaldjf_def djf_Or) |
|
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
|
302 |
|
50313 | 303 |
lemma evaldjf_bound0: |
304 |
assumes nb: "\<forall>x\<in> set xs. bound0 (f x)" |
|
23274 | 305 |
shows "bound0 (evaldjf f xs)" |
55422 | 306 |
using nb by (induct xs) (auto simp add: evaldjf_def djf_def Let_def, case_tac "f a", auto) |
23274 | 307 |
|
50313 | 308 |
lemma evaldjf_qf: |
309 |
assumes nb: "\<forall>x\<in> set xs. qfree (f x)" |
|
23274 | 310 |
shows "qfree (evaldjf f xs)" |
55422 | 311 |
using nb by (induct xs) (auto simp add: evaldjf_def djf_def Let_def, case_tac "f a", 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
|
312 |
|
50313 | 313 |
fun disjuncts :: "fm \<Rightarrow> fm list" |
314 |
where |
|
315 |
"disjuncts (Or p q) = disjuncts p @ disjuncts q" |
|
41837 | 316 |
| "disjuncts F = []" |
317 |
| "disjuncts p = [p]" |
|
23274 | 318 |
|
50313 | 319 |
lemma disjuncts: "(\<exists>q \<in> set (disjuncts p). Ifm bbs bs q) = Ifm bbs bs p" |
320 |
by (induct p rule: disjuncts.induct) auto |
|
23274 | 321 |
|
50313 | 322 |
lemma disjuncts_nb: |
323 |
assumes nb: "bound0 p" |
|
324 |
shows "\<forall>q \<in> set (disjuncts p). bound0 q" |
|
325 |
proof - |
|
326 |
from nb have "list_all bound0 (disjuncts p)" |
|
327 |
by (induct p rule: disjuncts.induct) auto |
|
23274 | 328 |
thus ?thesis by (simp only: list_all_iff) |
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
|
329 |
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
|
330 |
|
50313 | 331 |
lemma disjuncts_qf: |
332 |
assumes qf: "qfree p" |
|
333 |
shows "\<forall>q \<in> set (disjuncts p). qfree q" |
|
334 |
proof - |
|
335 |
from qf have "list_all qfree (disjuncts p)" |
|
336 |
by (induct p rule: disjuncts.induct) auto |
|
23274 | 337 |
thus ?thesis by (simp only: list_all_iff) |
338 |
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
|
339 |
|
50313 | 340 |
definition DJ :: "(fm \<Rightarrow> fm) \<Rightarrow> fm \<Rightarrow> fm" |
341 |
where "DJ f p = evaldjf f (disjuncts 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
|
342 |
|
50313 | 343 |
lemma DJ: |
344 |
assumes fdj: "\<forall>p q. f (Or p q) = Or (f p) (f q)" |
|
345 |
and fF: "f F = F" |
|
23274 | 346 |
shows "Ifm bbs bs (DJ f p) = Ifm bbs bs (f p)" |
50313 | 347 |
proof - |
348 |
have "Ifm bbs bs (DJ f p) = (\<exists>q \<in> set (disjuncts p). Ifm bbs bs (f q))" |
|
349 |
by (simp add: DJ_def evaldjf_ex) |
|
350 |
also have "\<dots> = Ifm bbs bs (f p)" |
|
351 |
using fdj fF by (induct p rule: disjuncts.induct) auto |
|
23274 | 352 |
finally show ?thesis . |
353 |
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
|
354 |
|
50313 | 355 |
lemma DJ_qf: |
356 |
assumes fqf: "\<forall>p. qfree p \<longrightarrow> qfree (f p)" |
|
23274 | 357 |
shows "\<forall>p. qfree p \<longrightarrow> qfree (DJ f p) " |
50313 | 358 |
proof clarify |
359 |
fix p assume qf: "qfree p" |
|
23274 | 360 |
have th: "DJ f p = evaldjf f (disjuncts p)" by (simp add: DJ_def) |
50313 | 361 |
from disjuncts_qf[OF qf] have "\<forall>q\<in> set (disjuncts p). qfree q" . |
362 |
with fqf have th':"\<forall>q\<in> set (disjuncts p). qfree (f q)" by blast |
|
363 |
||
23274 | 364 |
from evaldjf_qf[OF th'] th show "qfree (DJ f p)" by 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
|
365 |
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
|
366 |
|
50313 | 367 |
lemma DJ_qe: |
368 |
assumes qe: "\<forall>bs p. qfree p \<longrightarrow> qfree (qe p) \<and> (Ifm bbs bs (qe p) = Ifm bbs bs (E p))" |
|
369 |
shows "\<forall>bs p. qfree p \<longrightarrow> qfree (DJ qe p) \<and> (Ifm bbs bs ((DJ qe p)) = Ifm bbs bs (E p))" |
|
370 |
proof clarify |
|
371 |
fix p :: fm and bs |
|
23274 | 372 |
assume qf: "qfree p" |
50313 | 373 |
from qe have qth: "\<forall>p. qfree p \<longrightarrow> qfree (qe p)" by blast |
23274 | 374 |
from DJ_qf[OF qth] qf have qfth:"qfree (DJ qe p)" by auto |
50313 | 375 |
have "Ifm bbs bs (DJ qe p) = (\<exists>q\<in> set (disjuncts p). Ifm bbs bs (qe q))" |
23274 | 376 |
by (simp add: DJ_def evaldjf_ex) |
50313 | 377 |
also have "\<dots> = (\<exists>q \<in> set(disjuncts p). Ifm bbs bs (E q))" |
378 |
using qe disjuncts_qf[OF qf] by auto |
|
379 |
also have "\<dots> = Ifm bbs bs (E p)" |
|
380 |
by (induct p rule: disjuncts.induct) auto |
|
381 |
finally show "qfree (DJ qe p) \<and> Ifm bbs bs (DJ qe p) = Ifm bbs bs (E p)" |
|
382 |
using qfth by blast |
|
23274 | 383 |
qed |
50313 | 384 |
|
385 |
||
386 |
text {* Simplification *} |
|
23274 | 387 |
|
50313 | 388 |
text {* Algebraic simplifications for nums *} |
41837 | 389 |
|
50313 | 390 |
fun bnds :: "num \<Rightarrow> nat list" |
391 |
where |
|
23274 | 392 |
"bnds (Bound n) = [n]" |
41837 | 393 |
| "bnds (CN n c a) = n#(bnds a)" |
394 |
| "bnds (Neg a) = bnds a" |
|
395 |
| "bnds (Add a b) = (bnds a)@(bnds b)" |
|
396 |
| "bnds (Sub a b) = (bnds a)@(bnds b)" |
|
397 |
| "bnds (Mul i a) = bnds a" |
|
398 |
| "bnds a = []" |
|
399 |
||
50313 | 400 |
fun lex_ns:: "nat list \<Rightarrow> nat list \<Rightarrow> bool" |
401 |
where |
|
41837 | 402 |
"lex_ns [] ms = True" |
403 |
| "lex_ns ns [] = False" |
|
404 |
| "lex_ns (n#ns) (m#ms) = (n<m \<or> ((n = m) \<and> lex_ns ns ms)) " |
|
23274 | 405 |
|
50313 | 406 |
definition lex_bnd :: "num \<Rightarrow> num \<Rightarrow> bool" |
407 |
where "lex_bnd t s = lex_ns (bnds t) (bnds s)" |
|
408 |
||
409 |
consts numadd:: "num \<times> num \<Rightarrow> num" |
|
410 |
recdef numadd "measure (\<lambda>(t,s). num_size t + num_size s)" |
|
23995
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
411 |
"numadd (CN n1 c1 r1 ,CN n2 c2 r2) = |
50313 | 412 |
(if n1 = n2 then |
413 |
(let c = c1 + c2 |
|
414 |
in if c=0 then numadd (r1, r2) else CN n1 c (numadd (r1, r2))) |
|
415 |
else if n1 \<le> n2 then CN n1 c1 (numadd (r1,Add (Mul c2 (Bound n2)) r2)) |
|
416 |
else CN n2 c2 (numadd (Add (Mul c1 (Bound n1)) r1, r2)))" |
|
417 |
"numadd (CN n1 c1 r1, t) = CN n1 c1 (numadd (r1, t))" |
|
418 |
"numadd (t, CN n2 c2 r2) = CN n2 c2 (numadd (t, r2))" |
|
419 |
"numadd (C b1, C b2) = C (b1 + b2)" |
|
420 |
"numadd (a, b) = Add a b" |
|
23274 | 421 |
|
23689
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23515
diff
changeset
|
422 |
(*function (sequential) |
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23515
diff
changeset
|
423 |
numadd :: "num \<Rightarrow> num \<Rightarrow> num" |
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23515
diff
changeset
|
424 |
where |
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23515
diff
changeset
|
425 |
"numadd (Add (Mul c1 (Bound n1)) r1) (Add (Mul c2 (Bound n2)) r2) = |
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23515
diff
changeset
|
426 |
(if n1 = n2 then (let c = c1 + c2 |
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23515
diff
changeset
|
427 |
in (if c = 0 then numadd r1 r2 else |
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23515
diff
changeset
|
428 |
Add (Mul c (Bound n1)) (numadd r1 r2))) |
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23515
diff
changeset
|
429 |
else if n1 \<le> n2 then |
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23515
diff
changeset
|
430 |
Add (Mul c1 (Bound n1)) (numadd r1 (Add (Mul c2 (Bound n2)) r2)) |
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23515
diff
changeset
|
431 |
else |
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23515
diff
changeset
|
432 |
Add (Mul c2 (Bound n2)) (numadd (Add (Mul c1 (Bound n1)) r1) r2))" |
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23515
diff
changeset
|
433 |
| "numadd (Add (Mul c1 (Bound n1)) r1) t = |
50313 | 434 |
Add (Mul c1 (Bound n1)) (numadd r1 t)" |
23689
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23515
diff
changeset
|
435 |
| "numadd t (Add (Mul c2 (Bound n2)) r2) = |
50313 | 436 |
Add (Mul c2 (Bound n2)) (numadd t r2)" |
23689
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23515
diff
changeset
|
437 |
| "numadd (C b1) (C b2) = C (b1 + b2)" |
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23515
diff
changeset
|
438 |
| "numadd a b = Add a b" |
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23515
diff
changeset
|
439 |
apply pat_completeness apply auto*) |
50313 | 440 |
|
23274 | 441 |
lemma numadd: "Inum bs (numadd (t,s)) = Inum bs (Add t s)" |
50313 | 442 |
apply (induct t s rule: numadd.induct, simp_all add: Let_def) |
443 |
apply (case_tac "c1 + c2 = 0", case_tac "n1 \<le> n2", simp_all) |
|
444 |
apply (case_tac "n1 = n2") |
|
445 |
apply(simp_all add: algebra_simps) |
|
446 |
apply(simp add: distrib_right[symmetric]) |
|
447 |
done |
|
23274 | 448 |
|
50313 | 449 |
lemma numadd_nb: "numbound0 t \<Longrightarrow> numbound0 s \<Longrightarrow> numbound0 (numadd (t, s))" |
450 |
by (induct t s rule: numadd.induct) (auto simp add: Let_def) |
|
23274 | 451 |
|
50313 | 452 |
fun nummul :: "int \<Rightarrow> num \<Rightarrow> num" |
453 |
where |
|
23689
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23515
diff
changeset
|
454 |
"nummul i (C j) = C (i * j)" |
41837 | 455 |
| "nummul i (CN n c t) = CN n (c*i) (nummul i t)" |
456 |
| "nummul i t = Mul i t" |
|
23274 | 457 |
|
50313 | 458 |
lemma nummul: "Inum bs (nummul i t) = Inum bs (Mul i t)" |
459 |
by (induct t arbitrary: i rule: nummul.induct) (auto simp add: algebra_simps numadd) |
|
23274 | 460 |
|
50313 | 461 |
lemma nummul_nb: "numbound0 t \<Longrightarrow> numbound0 (nummul i t)" |
462 |
by (induct t arbitrary: i rule: nummul.induct) (auto simp add: numadd_nb) |
|
23274 | 463 |
|
50313 | 464 |
definition numneg :: "num \<Rightarrow> num" |
465 |
where "numneg t = nummul (- 1) t" |
|
23274 | 466 |
|
50313 | 467 |
definition numsub :: "num \<Rightarrow> num \<Rightarrow> num" |
468 |
where "numsub s t = (if s = t then C 0 else numadd (s, numneg t))" |
|
23274 | 469 |
|
470 |
lemma numneg: "Inum bs (numneg t) = Inum bs (Neg t)" |
|
50313 | 471 |
using numneg_def nummul by simp |
23274 | 472 |
|
473 |
lemma numneg_nb: "numbound0 t \<Longrightarrow> numbound0 (numneg t)" |
|
50313 | 474 |
using numneg_def nummul_nb by simp |
23274 | 475 |
|
476 |
lemma numsub: "Inum bs (numsub a b) = Inum bs (Sub a b)" |
|
50313 | 477 |
using numneg numadd numsub_def by simp |
23274 | 478 |
|
50313 | 479 |
lemma numsub_nb: "numbound0 t \<Longrightarrow> numbound0 s \<Longrightarrow> numbound0 (numsub t s)" |
480 |
using numsub_def numadd_nb numneg_nb by simp |
|
23274 | 481 |
|
50313 | 482 |
fun simpnum :: "num \<Rightarrow> num" |
23689
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23515
diff
changeset
|
483 |
where |
23274 | 484 |
"simpnum (C j) = C j" |
50313 | 485 |
| "simpnum (Bound n) = CN n 1 (C 0)" |
486 |
| "simpnum (Neg t) = numneg (simpnum t)" |
|
487 |
| "simpnum (Add t s) = numadd (simpnum t, simpnum s)" |
|
488 |
| "simpnum (Sub t s) = numsub (simpnum t) (simpnum s)" |
|
489 |
| "simpnum (Mul i t) = (if i = 0 then C 0 else nummul i (simpnum t))" |
|
490 |
| "simpnum t = t" |
|
23274 | 491 |
|
492 |
lemma simpnum_ci: "Inum bs (simpnum t) = Inum bs t" |
|
50313 | 493 |
by (induct t rule: simpnum.induct) (auto simp add: numneg numadd numsub nummul) |
23274 | 494 |
|
50313 | 495 |
lemma simpnum_numbound0: "numbound0 t \<Longrightarrow> numbound0 (simpnum t)" |
496 |
by (induct t rule: simpnum.induct) (auto simp add: numadd_nb numsub_nb nummul_nb numneg_nb) |
|
23274 | 497 |
|
50313 | 498 |
fun not :: "fm \<Rightarrow> fm" |
23689
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23515
diff
changeset
|
499 |
where |
23274 | 500 |
"not (NOT p) = p" |
50313 | 501 |
| "not T = F" |
502 |
| "not F = T" |
|
503 |
| "not p = NOT p" |
|
504 |
||
23274 | 505 |
lemma not: "Ifm bbs bs (not p) = Ifm bbs bs (NOT p)" |
41807 | 506 |
by (cases p) auto |
50313 | 507 |
|
23274 | 508 |
lemma not_qf: "qfree p \<Longrightarrow> qfree (not p)" |
41807 | 509 |
by (cases p) auto |
50313 | 510 |
|
23274 | 511 |
lemma not_bn: "bound0 p \<Longrightarrow> bound0 (not p)" |
41807 | 512 |
by (cases p) auto |
23274 | 513 |
|
50313 | 514 |
definition conj :: "fm \<Rightarrow> fm \<Rightarrow> fm" |
515 |
where |
|
516 |
"conj p q = (if (p = F \<or> q=F) then F else if p=T then q else if q=T then p else And p q)" |
|
517 |
||
23274 | 518 |
lemma conj: "Ifm bbs bs (conj p q) = Ifm bbs bs (And p q)" |
50313 | 519 |
by (cases "p=F \<or> q=F", simp_all add: conj_def) (cases p, simp_all) |
23274 | 520 |
|
50313 | 521 |
lemma conj_qf: "qfree p \<Longrightarrow> qfree q \<Longrightarrow> qfree (conj p q)" |
522 |
using conj_def by auto |
|
23274 | 523 |
|
50313 | 524 |
lemma conj_nb: "bound0 p \<Longrightarrow> bound0 q \<Longrightarrow> bound0 (conj p q)" |
525 |
using conj_def by auto |
|
526 |
||
527 |
definition disj :: "fm \<Rightarrow> fm \<Rightarrow> fm" |
|
528 |
where |
|
529 |
"disj p q = |
|
530 |
(if (p = T \<or> q=T) then T else if p=F then q else if q=F then p else Or p q)" |
|
23274 | 531 |
|
532 |
lemma disj: "Ifm bbs bs (disj p q) = Ifm bbs bs (Or p q)" |
|
50313 | 533 |
by (cases "p=T \<or> q=T", simp_all add: disj_def) (cases p, simp_all) |
534 |
||
23274 | 535 |
lemma disj_qf: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (disj p q)" |
50313 | 536 |
using disj_def by auto |
537 |
||
23274 | 538 |
lemma disj_nb: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (disj p q)" |
50313 | 539 |
using disj_def by auto |
23274 | 540 |
|
50313 | 541 |
definition imp :: "fm \<Rightarrow> fm \<Rightarrow> fm" |
542 |
where |
|
543 |
"imp p q = (if (p = F \<or> q=T) then T else if p=T then q else if q=F then not p else Imp p q)" |
|
544 |
||
23274 | 545 |
lemma imp: "Ifm bbs bs (imp p q) = Ifm bbs bs (Imp p q)" |
50313 | 546 |
by (cases "p=F \<or> q=T", simp_all add: imp_def, cases p) (simp_all add: not) |
547 |
||
548 |
lemma imp_qf: "qfree p \<Longrightarrow> qfree q \<Longrightarrow> qfree (imp p q)" |
|
549 |
using imp_def by (cases "p=F \<or> q=T",simp_all add: imp_def,cases p) (simp_all add: not_qf) |
|
550 |
||
551 |
lemma imp_nb: "bound0 p \<Longrightarrow> bound0 q \<Longrightarrow> bound0 (imp p q)" |
|
552 |
using imp_def by (cases "p=F \<or> q=T",simp_all add: imp_def,cases p) simp_all |
|
23274 | 553 |
|
50313 | 554 |
definition iff :: "fm \<Rightarrow> fm \<Rightarrow> fm" |
555 |
where |
|
556 |
"iff p q = |
|
557 |
(if (p = q) then T |
|
558 |
else if (p = not q \<or> not p = q) then F |
|
559 |
else if p = F then not q |
|
560 |
else if q = F then not p |
|
561 |
else if p = T then q |
|
562 |
else if q = T then p |
|
563 |
else Iff p q)" |
|
564 |
||
23274 | 565 |
lemma iff: "Ifm bbs bs (iff p q) = Ifm bbs bs (Iff p q)" |
50313 | 566 |
by (unfold iff_def,cases "p=q", simp,cases "p=not q", simp add:not) |
567 |
(cases "not p= q", auto simp add:not) |
|
568 |
||
23274 | 569 |
lemma iff_qf: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (iff p q)" |
570 |
by (unfold iff_def,cases "p=q", auto simp add: not_qf) |
|
571 |
||
50313 | 572 |
lemma iff_nb: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (iff p q)" |
573 |
using iff_def by (unfold iff_def,cases "p=q", auto simp add: not_bn) |
|
574 |
||
575 |
function (sequential) simpfm :: "fm \<Rightarrow> fm" |
|
23689
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23515
diff
changeset
|
576 |
where |
23274 | 577 |
"simpfm (And p q) = conj (simpfm p) (simpfm q)" |
50313 | 578 |
| "simpfm (Or p q) = disj (simpfm p) (simpfm q)" |
579 |
| "simpfm (Imp p q) = imp (simpfm p) (simpfm q)" |
|
580 |
| "simpfm (Iff p q) = iff (simpfm p) (simpfm q)" |
|
581 |
| "simpfm (NOT p) = not (simpfm p)" |
|
582 |
| "simpfm (Lt a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v < 0) then T else F | _ \<Rightarrow> Lt a')" |
|
583 |
| "simpfm (Le a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v \<le> 0) then T else F | _ \<Rightarrow> Le a')" |
|
584 |
| "simpfm (Gt a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v > 0) then T else F | _ \<Rightarrow> Gt a')" |
|
585 |
| "simpfm (Ge a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v \<ge> 0) then T else F | _ \<Rightarrow> Ge a')" |
|
586 |
| "simpfm (Eq a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v = 0) then T else F | _ \<Rightarrow> Eq a')" |
|
587 |
| "simpfm (NEq a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v \<noteq> 0) then T else F | _ \<Rightarrow> NEq a')" |
|
588 |
| "simpfm (Dvd i a) = |
|
589 |
(if i=0 then simpfm (Eq a) |
|
590 |
else if (abs i = 1) then T |
|
591 |
else let a' = simpnum a in case a' of C v \<Rightarrow> if (i dvd v) then T else F | _ \<Rightarrow> Dvd i a')" |
|
592 |
| "simpfm (NDvd i a) = |
|
593 |
(if i=0 then simpfm (NEq a) |
|
594 |
else if (abs i = 1) then F |
|
595 |
else let a' = simpnum a in case a' of C v \<Rightarrow> if (\<not>(i dvd v)) then T else F | _ \<Rightarrow> NDvd i a')" |
|
596 |
| "simpfm p = p" |
|
597 |
by pat_completeness auto |
|
23689
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23515
diff
changeset
|
598 |
termination by (relation "measure fmsize") auto |
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23515
diff
changeset
|
599 |
|
23274 | 600 |
lemma simpfm: "Ifm bbs bs (simpfm p) = Ifm bbs bs p" |
601 |
proof(induct p rule: simpfm.induct) |
|
50313 | 602 |
case (6 a) |
603 |
let ?sa = "simpnum a" |
|
604 |
from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp |
|
605 |
{ fix v assume "?sa = C v" hence ?case using sa by simp } |
|
606 |
moreover { |
|
607 |
assume "\<not> (\<exists>v. ?sa = C v)" |
|
608 |
hence ?case using sa by (cases ?sa) (simp_all add: Let_def) |
|
609 |
} |
|
23274 | 610 |
ultimately show ?case by blast |
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
|
611 |
next |
50313 | 612 |
case (7 a) |
613 |
let ?sa = "simpnum a" |
|
23274 | 614 |
from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp |
50313 | 615 |
{ fix v assume "?sa = C v" hence ?case using sa by simp } |
616 |
moreover { |
|
617 |
assume "\<not> (\<exists>v. ?sa = C v)" |
|
618 |
hence ?case using sa by (cases ?sa) (simp_all add: Let_def) |
|
619 |
} |
|
23274 | 620 |
ultimately show ?case by blast |
621 |
next |
|
50313 | 622 |
case (8 a) |
623 |
let ?sa = "simpnum a" |
|
23274 | 624 |
from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp |
50313 | 625 |
{ fix v assume "?sa = C v" hence ?case using sa by simp } |
626 |
moreover { |
|
627 |
assume "\<not> (\<exists>v. ?sa = C v)" |
|
628 |
hence ?case using sa by (cases ?sa) (simp_all add: Let_def) |
|
629 |
} |
|
23274 | 630 |
ultimately show ?case by blast |
631 |
next |
|
50313 | 632 |
case (9 a) |
633 |
let ?sa = "simpnum a" |
|
23274 | 634 |
from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp |
50313 | 635 |
{ fix v assume "?sa = C v" hence ?case using sa by simp } |
636 |
moreover { |
|
637 |
assume "\<not> (\<exists>v. ?sa = C v)" |
|
638 |
hence ?case using sa by (cases ?sa) (simp_all add: Let_def) |
|
639 |
} |
|
23274 | 640 |
ultimately show ?case by blast |
641 |
next |
|
50313 | 642 |
case (10 a) |
643 |
let ?sa = "simpnum a" |
|
23274 | 644 |
from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp |
50313 | 645 |
{ fix v assume "?sa = C v" hence ?case using sa by simp } |
646 |
moreover { |
|
647 |
assume "\<not> (\<exists>v. ?sa = C v)" |
|
648 |
hence ?case using sa by (cases ?sa) (simp_all add: Let_def) |
|
649 |
} |
|
23274 | 650 |
ultimately show ?case by blast |
651 |
next |
|
50313 | 652 |
case (11 a) |
653 |
let ?sa = "simpnum a" |
|
654 |
from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp |
|
655 |
{ fix v assume "?sa = C v" hence ?case using sa by simp } |
|
656 |
moreover { |
|
657 |
assume "\<not> (\<exists>v. ?sa = C v)" |
|
658 |
hence ?case using sa by (cases ?sa) (simp_all add: Let_def) |
|
659 |
} |
|
23274 | 660 |
ultimately show ?case by blast |
661 |
next |
|
50313 | 662 |
case (12 i a) |
663 |
let ?sa = "simpnum a" |
|
664 |
from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp |
|
665 |
{ assume "i=0" hence ?case using "12.hyps" by (simp add: dvd_def Let_def) } |
|
666 |
moreover |
|
667 |
{ assume i1: "abs i = 1" |
|
668 |
from one_dvd[of "Inum bs a"] uminus_dvd_conv[where d="1" and t="Inum bs a"] |
|
669 |
have ?case using i1 |
|
670 |
apply (cases "i=0", simp_all add: Let_def) |
|
671 |
apply (cases "i > 0", simp_all) |
|
672 |
done |
|
673 |
} |
|
674 |
moreover |
|
675 |
{ assume inz: "i\<noteq>0" and cond: "abs i \<noteq> 1" |
|
676 |
{ fix v assume "?sa = C v" |
|
677 |
hence ?case using sa[symmetric] inz cond |
|
678 |
by (cases "abs i = 1") auto } |
|
679 |
moreover { |
|
680 |
assume "\<not> (\<exists>v. ?sa = C v)" |
|
681 |
hence "simpfm (Dvd i a) = Dvd i ?sa" using inz cond |
|
682 |
by (cases ?sa) (auto simp add: Let_def) |
|
683 |
hence ?case using sa by simp } |
|
684 |
ultimately have ?case by blast } |
|
685 |
ultimately show ?case by blast |
|
686 |
next |
|
687 |
case (13 i a) |
|
688 |
let ?sa = "simpnum a" from simpnum_ci |
|
23274 | 689 |
have sa: "Inum bs ?sa = Inum bs a" by simp |
50313 | 690 |
{ assume "i=0" hence ?case using "13.hyps" by (simp add: dvd_def Let_def) } |
691 |
moreover |
|
692 |
{ assume i1: "abs i = 1" |
|
693 |
from one_dvd[of "Inum bs a"] uminus_dvd_conv[where d="1" and t="Inum bs a"] |
|
694 |
have ?case using i1 |
|
695 |
apply (cases "i=0", simp_all add: Let_def) |
|
696 |
apply (cases "i > 0", simp_all) |
|
697 |
done |
|
698 |
} |
|
699 |
moreover |
|
700 |
{ assume inz: "i\<noteq>0" and cond: "abs i \<noteq> 1" |
|
701 |
{ fix v assume "?sa = C v" |
|
702 |
hence ?case using sa[symmetric] inz cond |
|
703 |
by (cases "abs i = 1") auto } |
|
704 |
moreover { |
|
705 |
assume "\<not> (\<exists>v. ?sa = C v)" |
|
706 |
hence "simpfm (NDvd i a) = NDvd i ?sa" using inz cond |
|
707 |
by (cases ?sa) (auto simp add: Let_def) |
|
708 |
hence ?case using sa by simp } |
|
709 |
ultimately have ?case by blast } |
|
23274 | 710 |
ultimately show ?case by blast |
50313 | 711 |
qed (simp_all add: conj disj imp iff not) |
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
|
712 |
|
23274 | 713 |
lemma simpfm_bound0: "bound0 p \<Longrightarrow> bound0 (simpfm p)" |
50313 | 714 |
proof (induct p rule: simpfm.induct) |
23274 | 715 |
case (6 a) hence nb: "numbound0 a" by simp |
716 |
hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb]) |
|
50313 | 717 |
thus ?case by (cases "simpnum a") (auto simp add: Let_def) |
23274 | 718 |
next |
719 |
case (7 a) hence nb: "numbound0 a" by simp |
|
720 |
hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb]) |
|
50313 | 721 |
thus ?case by (cases "simpnum a") (auto simp add: Let_def) |
23274 | 722 |
next |
723 |
case (8 a) hence nb: "numbound0 a" by simp |
|
724 |
hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb]) |
|
50313 | 725 |
thus ?case by (cases "simpnum a") (auto simp add: Let_def) |
23274 | 726 |
next |
727 |
case (9 a) hence nb: "numbound0 a" by simp |
|
728 |
hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb]) |
|
50313 | 729 |
thus ?case by (cases "simpnum a") (auto simp add: Let_def) |
23274 | 730 |
next |
731 |
case (10 a) hence nb: "numbound0 a" by simp |
|
732 |
hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb]) |
|
50313 | 733 |
thus ?case by (cases "simpnum a") (auto simp add: Let_def) |
23274 | 734 |
next |
735 |
case (11 a) hence nb: "numbound0 a" by simp |
|
736 |
hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb]) |
|
50313 | 737 |
thus ?case by (cases "simpnum a") (auto simp add: Let_def) |
23274 | 738 |
next |
739 |
case (12 i a) hence nb: "numbound0 a" by simp |
|
740 |
hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb]) |
|
50313 | 741 |
thus ?case by (cases "simpnum a") (auto simp add: Let_def) |
23274 | 742 |
next |
743 |
case (13 i a) hence nb: "numbound0 a" by simp |
|
744 |
hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb]) |
|
50313 | 745 |
thus ?case by (cases "simpnum a") (auto simp add: Let_def) |
746 |
qed (auto simp add: disj_def imp_def iff_def conj_def not_bn) |
|
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
|
747 |
|
23274 | 748 |
lemma simpfm_qf: "qfree p \<Longrightarrow> qfree (simpfm p)" |
50313 | 749 |
by (induct p rule: simpfm.induct, auto simp add: disj_qf imp_qf iff_qf conj_qf not_qf Let_def) |
750 |
(case_tac "simpnum a", auto)+ |
|
23274 | 751 |
|
50313 | 752 |
text {* Generic quantifier elimination *} |
753 |
function (sequential) qelim :: "fm \<Rightarrow> (fm \<Rightarrow> fm) \<Rightarrow> fm" |
|
754 |
where |
|
755 |
"qelim (E p) = (\<lambda>qe. DJ qe (qelim p qe))" |
|
756 |
| "qelim (A p) = (\<lambda>qe. not (qe ((qelim (NOT p) qe))))" |
|
757 |
| "qelim (NOT p) = (\<lambda>qe. not (qelim p qe))" |
|
758 |
| "qelim (And p q) = (\<lambda>qe. conj (qelim p qe) (qelim q qe))" |
|
759 |
| "qelim (Or p q) = (\<lambda>qe. disj (qelim p qe) (qelim q qe))" |
|
760 |
| "qelim (Imp p q) = (\<lambda>qe. imp (qelim p qe) (qelim q qe))" |
|
761 |
| "qelim (Iff p q) = (\<lambda>qe. iff (qelim p qe) (qelim q qe))" |
|
762 |
| "qelim p = (\<lambda>y. simpfm p)" |
|
763 |
by pat_completeness auto |
|
41837 | 764 |
termination by (relation "measure fmsize") auto |
23689
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23515
diff
changeset
|
765 |
|
23274 | 766 |
lemma qelim_ci: |
50313 | 767 |
assumes qe_inv: "\<forall>bs p. qfree p \<longrightarrow> qfree (qe p) \<and> (Ifm bbs bs (qe p) = Ifm bbs bs (E p))" |
768 |
shows "\<And>bs. qfree (qelim p qe) \<and> (Ifm bbs bs (qelim p qe) = Ifm bbs bs p)" |
|
769 |
using qe_inv DJ_qe[OF qe_inv] |
|
770 |
by(induct p rule: qelim.induct) |
|
771 |
(auto simp add: not disj conj iff imp not_qf disj_qf conj_qf imp_qf iff_qf |
|
772 |
simpfm simpfm_qf simp del: simpfm.simps) |
|
23689
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23515
diff
changeset
|
773 |
|
50313 | 774 |
text {* Linearity for fm where Bound 0 ranges over @{text "\<int>"} *} |
775 |
||
776 |
fun zsplit0 :: "num \<Rightarrow> int \<times> num" -- {* splits the bounded from the unbounded part *} |
|
23689
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23515
diff
changeset
|
777 |
where |
23274 | 778 |
"zsplit0 (C c) = (0,C c)" |
50313 | 779 |
| "zsplit0 (Bound n) = (if n=0 then (1, C 0) else (0,Bound n))" |
780 |
| "zsplit0 (CN n i a) = |
|
781 |
(let (i',a') = zsplit0 a |
|
782 |
in if n=0 then (i+i', a') else (i',CN n i a'))" |
|
783 |
| "zsplit0 (Neg a) = (let (i',a') = zsplit0 a in (-i', Neg a'))" |
|
784 |
| "zsplit0 (Add a b) = (let (ia,a') = zsplit0 a ; |
|
785 |
(ib,b') = zsplit0 b |
|
786 |
in (ia+ib, Add a' b'))" |
|
787 |
| "zsplit0 (Sub a b) = (let (ia,a') = zsplit0 a ; |
|
788 |
(ib,b') = zsplit0 b |
|
789 |
in (ia-ib, Sub a' b'))" |
|
790 |
| "zsplit0 (Mul i a) = (let (i',a') = zsplit0 a in (i*i', Mul i a'))" |
|
23274 | 791 |
|
792 |
lemma zsplit0_I: |
|
50313 | 793 |
shows "\<And>n a. zsplit0 t = (n,a) \<Longrightarrow> (Inum ((x::int) #bs) (CN 0 n a) = Inum (x #bs) t) \<and> numbound0 a" |
794 |
(is "\<And>n a. ?S t = (n,a) \<Longrightarrow> (?I x (CN 0 n a) = ?I x t) \<and> ?N a") |
|
795 |
proof (induct t rule: zsplit0.induct) |
|
796 |
case (1 c n a) thus ?case by auto |
|
23274 | 797 |
next |
798 |
case (2 m n a) thus ?case by (cases "m=0") auto |
|
799 |
next |
|
23995
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
800 |
case (3 m i a n a') |
23274 | 801 |
let ?j = "fst (zsplit0 a)" |
802 |
let ?b = "snd (zsplit0 a)" |
|
50313 | 803 |
have abj: "zsplit0 a = (?j,?b)" by simp |
804 |
{assume "m\<noteq>0" |
|
41807 | 805 |
with 3(1)[OF abj] 3(2) have ?case by (auto simp add: Let_def split_def)} |
23995
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
806 |
moreover |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
807 |
{assume m0: "m =0" |
50313 | 808 |
with abj have th: "a'=?b \<and> n=i+?j" using 3 |
23995
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
809 |
by (simp add: Let_def split_def) |
41807 | 810 |
from abj 3 m0 have th2: "(?I x (CN 0 ?j ?b) = ?I x a) \<and> ?N ?b" by blast |
23995
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
811 |
from th have "?I x (CN 0 n a') = ?I x (CN 0 (i+?j) ?b)" by simp |
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
48891
diff
changeset
|
812 |
also from th2 have "\<dots> = ?I x (CN 0 i (CN 0 ?j ?b))" by (simp add: distrib_right) |
23995
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
813 |
finally have "?I x (CN 0 n a') = ?I x (CN 0 i a)" using th2 by simp |
50313 | 814 |
with th2 th have ?case using m0 by blast} |
23995
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
815 |
ultimately show ?case by blast |
23274 | 816 |
next |
817 |
case (4 t n a) |
|
818 |
let ?nt = "fst (zsplit0 t)" |
|
819 |
let ?at = "snd (zsplit0 t)" |
|
41807 | 820 |
have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a=Neg ?at \<and> n=-?nt" using 4 |
23274 | 821 |
by (simp add: Let_def split_def) |
41807 | 822 |
from abj 4 have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast |
23274 | 823 |
from th2[simplified] th[simplified] show ?case by simp |
824 |
next |
|
825 |
case (5 s t n a) |
|
826 |
let ?ns = "fst (zsplit0 s)" |
|
827 |
let ?as = "snd (zsplit0 s)" |
|
828 |
let ?nt = "fst (zsplit0 t)" |
|
829 |
let ?at = "snd (zsplit0 t)" |
|
50313 | 830 |
have abjs: "zsplit0 s = (?ns,?as)" by simp |
831 |
moreover have abjt: "zsplit0 t = (?nt,?at)" by simp |
|
41807 | 832 |
ultimately have th: "a=Add ?as ?at \<and> n=?ns + ?nt" using 5 |
23274 | 833 |
by (simp add: Let_def split_def) |
50313 | 834 |
from abjs[symmetric] have bluddy: "\<exists>x y. (x,y) = zsplit0 s" by blast |
835 |
from 5 have "(\<exists>x y. (x,y) = zsplit0 s) \<longrightarrow> (\<forall>xa xb. zsplit0 t = (xa, xb) \<longrightarrow> Inum (x # bs) (CN 0 xa xb) = Inum (x # bs) t \<and> numbound0 xb)" by auto |
|
23995
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
836 |
with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast |
41807 | 837 |
from abjs 5 have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as" by blast |
50313 | 838 |
from th3[simplified] th2[simplified] th[simplified] show ?case |
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
48891
diff
changeset
|
839 |
by (simp add: distrib_right) |
23274 | 840 |
next |
841 |
case (6 s t n a) |
|
842 |
let ?ns = "fst (zsplit0 s)" |
|
843 |
let ?as = "snd (zsplit0 s)" |
|
844 |
let ?nt = "fst (zsplit0 t)" |
|
845 |
let ?at = "snd (zsplit0 t)" |
|
50313 | 846 |
have abjs: "zsplit0 s = (?ns,?as)" by simp |
847 |
moreover have abjt: "zsplit0 t = (?nt,?at)" by simp |
|
41807 | 848 |
ultimately have th: "a=Sub ?as ?at \<and> n=?ns - ?nt" using 6 |
23274 | 849 |
by (simp add: Let_def split_def) |
50313 | 850 |
from abjs[symmetric] have bluddy: "\<exists>x y. (x,y) = zsplit0 s" by blast |
851 |
from 6 have "(\<exists>x y. (x,y) = zsplit0 s) \<longrightarrow> |
|
852 |
(\<forall>xa xb. zsplit0 t = (xa, xb) \<longrightarrow> Inum (x # bs) (CN 0 xa xb) = Inum (x # bs) t \<and> numbound0 xb)" |
|
853 |
by auto |
|
23995
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
854 |
with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast |
41807 | 855 |
from abjs 6 have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as" by blast |
50313 | 856 |
from th3[simplified] th2[simplified] th[simplified] show ?case |
23274 | 857 |
by (simp add: left_diff_distrib) |
858 |
next |
|
859 |
case (7 i t n a) |
|
860 |
let ?nt = "fst (zsplit0 t)" |
|
861 |
let ?at = "snd (zsplit0 t)" |
|
50313 | 862 |
have abj: "zsplit0 t = (?nt,?at)" by simp |
863 |
hence th: "a=Mul i ?at \<and> n=i*?nt" using 7 |
|
23274 | 864 |
by (simp add: Let_def split_def) |
41807 | 865 |
from abj 7 have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast |
866 |
hence "?I x (Mul i t) = i * ?I x (CN 0 ?nt ?at)" by simp |
|
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
48891
diff
changeset
|
867 |
also have "\<dots> = ?I x (CN 0 (i*?nt) (Mul i ?at))" by (simp add: distrib_left) |
23274 | 868 |
finally show ?case using th th2 by 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
|
869 |
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
|
870 |
|
50313 | 871 |
consts iszlfm :: "fm \<Rightarrow> bool" -- {* Linearity test for fm *} |
23274 | 872 |
recdef iszlfm "measure size" |
50313 | 873 |
"iszlfm (And p q) = (iszlfm p \<and> iszlfm q)" |
874 |
"iszlfm (Or p q) = (iszlfm p \<and> iszlfm q)" |
|
23995
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
875 |
"iszlfm (Eq (CN 0 c e)) = (c>0 \<and> numbound0 e)" |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
876 |
"iszlfm (NEq (CN 0 c e)) = (c>0 \<and> numbound0 e)" |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
877 |
"iszlfm (Lt (CN 0 c e)) = (c>0 \<and> numbound0 e)" |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
878 |
"iszlfm (Le (CN 0 c e)) = (c>0 \<and> numbound0 e)" |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
879 |
"iszlfm (Gt (CN 0 c e)) = (c>0 \<and> numbound0 e)" |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
880 |
"iszlfm (Ge (CN 0 c e)) = ( c>0 \<and> numbound0 e)" |
50313 | 881 |
"iszlfm (Dvd i (CN 0 c e)) = |
23274 | 882 |
(c>0 \<and> i>0 \<and> numbound0 e)" |
50313 | 883 |
"iszlfm (NDvd i (CN 0 c e))= |
23274 | 884 |
(c>0 \<and> i>0 \<and> numbound0 e)" |
885 |
"iszlfm p = (isatom p \<and> (bound0 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
|
886 |
|
23274 | 887 |
lemma zlin_qfree: "iszlfm p \<Longrightarrow> qfree p" |
888 |
by (induct p rule: iszlfm.induct) 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
|
889 |
|
50313 | 890 |
consts zlfm :: "fm \<Rightarrow> fm" -- {* Linearity transformation for fm *} |
23274 | 891 |
recdef zlfm "measure fmsize" |
892 |
"zlfm (And p q) = And (zlfm p) (zlfm q)" |
|
893 |
"zlfm (Or p q) = Or (zlfm p) (zlfm q)" |
|
894 |
"zlfm (Imp p q) = Or (zlfm (NOT p)) (zlfm q)" |
|
895 |
"zlfm (Iff p q) = Or (And (zlfm p) (zlfm q)) (And (zlfm (NOT p)) (zlfm (NOT q)))" |
|
50313 | 896 |
"zlfm (Lt a) = (let (c,r) = zsplit0 a in |
897 |
if c=0 then Lt r else |
|
23995
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
898 |
if c>0 then (Lt (CN 0 c r)) else (Gt (CN 0 (- c) (Neg r))))" |
50313 | 899 |
"zlfm (Le a) = (let (c,r) = zsplit0 a in |
900 |
if c=0 then Le r else |
|
23995
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
901 |
if c>0 then (Le (CN 0 c r)) else (Ge (CN 0 (- c) (Neg r))))" |
50313 | 902 |
"zlfm (Gt a) = (let (c,r) = zsplit0 a in |
903 |
if c=0 then Gt r else |
|
23995
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
904 |
if c>0 then (Gt (CN 0 c r)) else (Lt (CN 0 (- c) (Neg r))))" |
50313 | 905 |
"zlfm (Ge a) = (let (c,r) = zsplit0 a in |
906 |
if c=0 then Ge r else |
|
23995
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
907 |
if c>0 then (Ge (CN 0 c r)) else (Le (CN 0 (- c) (Neg r))))" |
50313 | 908 |
"zlfm (Eq a) = (let (c,r) = zsplit0 a in |
909 |
if c=0 then Eq r else |
|
23995
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
910 |
if c>0 then (Eq (CN 0 c r)) else (Eq (CN 0 (- c) (Neg r))))" |
50313 | 911 |
"zlfm (NEq a) = (let (c,r) = zsplit0 a in |
912 |
if c=0 then NEq r else |
|
23995
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
913 |
if c>0 then (NEq (CN 0 c r)) else (NEq (CN 0 (- c) (Neg r))))" |
50313 | 914 |
"zlfm (Dvd i a) = (if i=0 then zlfm (Eq a) |
915 |
else (let (c,r) = zsplit0 a in |
|
916 |
if c=0 then (Dvd (abs i) r) else |
|
23995
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
917 |
if c>0 then (Dvd (abs i) (CN 0 c r)) |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
918 |
else (Dvd (abs i) (CN 0 (- c) (Neg r)))))" |
50313 | 919 |
"zlfm (NDvd i a) = (if i=0 then zlfm (NEq a) |
920 |
else (let (c,r) = zsplit0 a in |
|
921 |
if c=0 then (NDvd (abs i) r) else |
|
23995
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
922 |
if c>0 then (NDvd (abs i) (CN 0 c r)) |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
923 |
else (NDvd (abs i) (CN 0 (- c) (Neg r)))))" |
23274 | 924 |
"zlfm (NOT (And p q)) = Or (zlfm (NOT p)) (zlfm (NOT q))" |
925 |
"zlfm (NOT (Or p q)) = And (zlfm (NOT p)) (zlfm (NOT q))" |
|
926 |
"zlfm (NOT (Imp p q)) = And (zlfm p) (zlfm (NOT q))" |
|
927 |
"zlfm (NOT (Iff p q)) = Or (And(zlfm p) (zlfm(NOT q))) (And (zlfm(NOT p)) (zlfm q))" |
|
928 |
"zlfm (NOT (NOT p)) = zlfm p" |
|
929 |
"zlfm (NOT T) = F" |
|
930 |
"zlfm (NOT F) = T" |
|
931 |
"zlfm (NOT (Lt a)) = zlfm (Ge a)" |
|
932 |
"zlfm (NOT (Le a)) = zlfm (Gt a)" |
|
933 |
"zlfm (NOT (Gt a)) = zlfm (Le a)" |
|
934 |
"zlfm (NOT (Ge a)) = zlfm (Lt a)" |
|
935 |
"zlfm (NOT (Eq a)) = zlfm (NEq a)" |
|
936 |
"zlfm (NOT (NEq a)) = zlfm (Eq a)" |
|
937 |
"zlfm (NOT (Dvd i a)) = zlfm (NDvd i a)" |
|
938 |
"zlfm (NOT (NDvd i a)) = zlfm (Dvd i a)" |
|
939 |
"zlfm (NOT (Closed P)) = NClosed P" |
|
940 |
"zlfm (NOT (NClosed P)) = Closed P" |
|
941 |
"zlfm p = p" (hints simp add: fmsize_pos) |
|
942 |
||
943 |
lemma zlfm_I: |
|
944 |
assumes qfp: "qfree p" |
|
945 |
shows "(Ifm bbs (i#bs) (zlfm p) = Ifm bbs (i# bs) p) \<and> iszlfm (zlfm p)" |
|
946 |
(is "(?I (?l p) = ?I p) \<and> ?L (?l p)") |
|
50313 | 947 |
using qfp |
948 |
proof (induct p rule: zlfm.induct) |
|
949 |
case (5 a) |
|
23274 | 950 |
let ?c = "fst (zsplit0 a)" |
951 |
let ?r = "snd (zsplit0 a)" |
|
952 |
have spl: "zsplit0 a = (?c,?r)" by simp |
|
50313 | 953 |
from zsplit0_I[OF spl, where x="i" and bs="bs"] |
954 |
have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto |
|
955 |
let ?N = "\<lambda>t. Inum (i#bs) t" |
|
956 |
from 5 Ia nb show ?case |
|
957 |
apply (auto simp add: Let_def split_def algebra_simps) |
|
41807 | 958 |
apply (cases "?r", auto) |
23995
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
959 |
apply (case_tac nat, auto) |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
960 |
done |
23274 | 961 |
next |
50313 | 962 |
case (6 a) |
23274 | 963 |
let ?c = "fst (zsplit0 a)" |
964 |
let ?r = "snd (zsplit0 a)" |
|
965 |
have spl: "zsplit0 a = (?c,?r)" by simp |
|
50313 | 966 |
from zsplit0_I[OF spl, where x="i" and bs="bs"] |
967 |
have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto |
|
968 |
let ?N = "\<lambda>t. Inum (i#bs) t" |
|
969 |
from 6 Ia nb show ?case |
|
970 |
apply (auto simp add: Let_def split_def algebra_simps) |
|
41807 | 971 |
apply (cases "?r", auto) |
23995
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
972 |
apply (case_tac nat, auto) |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
973 |
done |
23274 | 974 |
next |
50313 | 975 |
case (7 a) |
23274 | 976 |
let ?c = "fst (zsplit0 a)" |
977 |
let ?r = "snd (zsplit0 a)" |
|
978 |
have spl: "zsplit0 a = (?c,?r)" by simp |
|
50313 | 979 |
from zsplit0_I[OF spl, where x="i" and bs="bs"] |
980 |
have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto |
|
981 |
let ?N = "\<lambda>t. Inum (i#bs) t" |
|
982 |
from 7 Ia nb show ?case |
|
983 |
apply (auto simp add: Let_def split_def algebra_simps) |
|
41807 | 984 |
apply (cases "?r", auto) |
23995
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
985 |
apply (case_tac nat, auto) |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
986 |
done |
23274 | 987 |
next |
50313 | 988 |
case (8 a) |
23274 | 989 |
let ?c = "fst (zsplit0 a)" |
990 |
let ?r = "snd (zsplit0 a)" |
|
991 |
have spl: "zsplit0 a = (?c,?r)" by simp |
|
50313 | 992 |
from zsplit0_I[OF spl, where x="i" and bs="bs"] |
993 |
have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto |
|
994 |
let ?N = "\<lambda>t. Inum (i#bs) t" |
|
41807 | 995 |
from 8 Ia nb show ?case |
50313 | 996 |
apply (auto simp add: Let_def split_def algebra_simps) |
41807 | 997 |
apply (cases "?r", auto) |
23995
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
998 |
apply (case_tac nat, auto) |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
999 |
done |
23274 | 1000 |
next |
50313 | 1001 |
case (9 a) |
23274 | 1002 |
let ?c = "fst (zsplit0 a)" |
1003 |
let ?r = "snd (zsplit0 a)" |
|
1004 |
have spl: "zsplit0 a = (?c,?r)" by simp |
|
50313 | 1005 |
from zsplit0_I[OF spl, where x="i" and bs="bs"] |
1006 |
have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto |
|
1007 |
let ?N = "\<lambda>t. Inum (i#bs) t" |
|
41807 | 1008 |
from 9 Ia nb show ?case |
50313 | 1009 |
apply (auto simp add: Let_def split_def algebra_simps) |
41807 | 1010 |
apply (cases "?r", auto) |
23995
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1011 |
apply (case_tac nat, auto) |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1012 |
done |
23274 | 1013 |
next |
50313 | 1014 |
case (10 a) |
23274 | 1015 |
let ?c = "fst (zsplit0 a)" |
1016 |
let ?r = "snd (zsplit0 a)" |
|
1017 |
have spl: "zsplit0 a = (?c,?r)" by simp |
|
50313 | 1018 |
from zsplit0_I[OF spl, where x="i" and bs="bs"] |
1019 |
have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto |
|
1020 |
let ?N = "\<lambda>t. Inum (i#bs) t" |
|
41807 | 1021 |
from 10 Ia nb show ?case |
50313 | 1022 |
apply (auto simp add: Let_def split_def algebra_simps) |
23995
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1023 |
apply (cases "?r",auto) |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1024 |
apply (case_tac nat, auto) |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1025 |
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
|
1026 |
next |
50313 | 1027 |
case (11 j a) |
23274 | 1028 |
let ?c = "fst (zsplit0 a)" |
1029 |
let ?r = "snd (zsplit0 a)" |
|
1030 |
have spl: "zsplit0 a = (?c,?r)" by simp |
|
50313 | 1031 |
from zsplit0_I[OF spl, where x="i" and bs="bs"] |
1032 |
have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto |
|
1033 |
let ?N = "\<lambda>t. Inum (i#bs) t" |
|
23274 | 1034 |
have "j=0 \<or> (j\<noteq>0 \<and> ?c = 0) \<or> (j\<noteq>0 \<and> ?c >0) \<or> (j\<noteq> 0 \<and> ?c<0)" by arith |
1035 |
moreover |
|
50313 | 1036 |
{assume "j=0" hence z: "zlfm (Dvd j a) = (zlfm (Eq a))" by (simp add: Let_def) |
41807 | 1037 |
hence ?case using 11 `j = 0` by (simp del: zlfm.simps) } |
23274 | 1038 |
moreover |
50313 | 1039 |
{assume "?c=0" and "j\<noteq>0" hence ?case |
29700 | 1040 |
using zsplit0_I[OF spl, where x="i" and bs="bs"] |
50313 | 1041 |
apply (auto simp add: Let_def split_def algebra_simps) |
23995
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1042 |
apply (cases "?r",auto) |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1043 |
apply (case_tac nat, auto) |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1044 |
done} |
23274 | 1045 |
moreover |
50313 | 1046 |
{assume cp: "?c > 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))" |
23274 | 1047 |
by (simp add: nb Let_def split_def) |
29700 | 1048 |
hence ?case using Ia cp jnz by (simp add: Let_def split_def)} |
23274 | 1049 |
moreover |
50313 | 1050 |
{assume cn: "?c < 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))" |
23274 | 1051 |
by (simp add: nb Let_def split_def) |
30042 | 1052 |
hence ?case using Ia cn jnz dvd_minus_iff[of "abs j" "?c*i + ?N ?r" ] |
29700 | 1053 |
by (simp add: Let_def split_def) } |
23274 | 1054 |
ultimately show ?case by blast |
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
|
1055 |
next |
50313 | 1056 |
case (12 j a) |
23274 | 1057 |
let ?c = "fst (zsplit0 a)" |
1058 |
let ?r = "snd (zsplit0 a)" |
|
1059 |
have spl: "zsplit0 a = (?c,?r)" by simp |
|
50313 | 1060 |
from zsplit0_I[OF spl, where x="i" and bs="bs"] |
1061 |
have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto |
|
1062 |
let ?N = "\<lambda>t. Inum (i#bs) t" |
|
23274 | 1063 |
have "j=0 \<or> (j\<noteq>0 \<and> ?c = 0) \<or> (j\<noteq>0 \<and> ?c >0) \<or> (j\<noteq> 0 \<and> ?c<0)" by arith |
1064 |
moreover |
|
50313 | 1065 |
{assume "j=0" hence z: "zlfm (NDvd j a) = (zlfm (NEq a))" by (simp add: Let_def) |
41807 | 1066 |
hence ?case using assms 12 `j = 0` by (simp del: zlfm.simps)} |
23274 | 1067 |
moreover |
50313 | 1068 |
{assume "?c=0" and "j\<noteq>0" hence ?case |
29700 | 1069 |
using zsplit0_I[OF spl, where x="i" and bs="bs"] |
50313 | 1070 |
apply (auto simp add: Let_def split_def algebra_simps) |
23995
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1071 |
apply (cases "?r",auto) |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1072 |
apply (case_tac nat, auto) |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1073 |
done} |
23274 | 1074 |
moreover |
50313 | 1075 |
{assume cp: "?c > 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))" |
23274 | 1076 |
by (simp add: nb Let_def split_def) |
29700 | 1077 |
hence ?case using Ia cp jnz by (simp add: Let_def split_def) } |
23274 | 1078 |
moreover |
50313 | 1079 |
{assume cn: "?c < 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))" |
23274 | 1080 |
by (simp add: nb Let_def split_def) |
30042 | 1081 |
hence ?case using Ia cn jnz dvd_minus_iff[of "abs j" "?c*i + ?N ?r"] |
29700 | 1082 |
by (simp add: Let_def split_def)} |
23274 | 1083 |
ultimately show ?case by blast |
1084 |
qed auto |
|
1085 |
||
50313 | 1086 |
consts minusinf :: "fm \<Rightarrow> fm" -- {* Virtual substitution of @{text "-\<infinity>"} *} |
23274 | 1087 |
recdef minusinf "measure size" |
50313 | 1088 |
"minusinf (And p q) = And (minusinf p) (minusinf q)" |
1089 |
"minusinf (Or p q) = Or (minusinf p) (minusinf q)" |
|
23995
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1090 |
"minusinf (Eq (CN 0 c e)) = F" |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1091 |
"minusinf (NEq (CN 0 c e)) = T" |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1092 |
"minusinf (Lt (CN 0 c e)) = T" |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1093 |
"minusinf (Le (CN 0 c e)) = T" |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1094 |
"minusinf (Gt (CN 0 c e)) = F" |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1095 |
"minusinf (Ge (CN 0 c e)) = F" |
23274 | 1096 |
"minusinf p = p" |
1097 |
||
1098 |
lemma minusinf_qfree: "qfree p \<Longrightarrow> qfree (minusinf p)" |
|
50313 | 1099 |
by (induct p rule: minusinf.induct) auto |
23274 | 1100 |
|
50313 | 1101 |
consts plusinf :: "fm \<Rightarrow> fm" -- {* Virtual substitution of @{text "+\<infinity>"} *} |
23274 | 1102 |
recdef plusinf "measure size" |
50313 | 1103 |
"plusinf (And p q) = And (plusinf p) (plusinf q)" |
1104 |
"plusinf (Or p q) = Or (plusinf p) (plusinf q)" |
|
23995
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1105 |
"plusinf (Eq (CN 0 c e)) = F" |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1106 |
"plusinf (NEq (CN 0 c e)) = T" |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1107 |
"plusinf (Lt (CN 0 c e)) = F" |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1108 |
"plusinf (Le (CN 0 c e)) = F" |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1109 |
"plusinf (Gt (CN 0 c e)) = T" |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1110 |
"plusinf (Ge (CN 0 c e)) = T" |
23274 | 1111 |
"plusinf p = p" |
1112 |
||
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51272
diff
changeset
|
1113 |
consts \<delta> :: "fm \<Rightarrow> int" -- {* Compute @{text "lcm {d| N\<^sup>? Dvd c*x+t \<in> p}"} *} |
23274 | 1114 |
recdef \<delta> "measure size" |
50313 | 1115 |
"\<delta> (And p q) = lcm (\<delta> p) (\<delta> q)" |
1116 |
"\<delta> (Or p q) = lcm (\<delta> p) (\<delta> q)" |
|
23995
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1117 |
"\<delta> (Dvd i (CN 0 c e)) = i" |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1118 |
"\<delta> (NDvd i (CN 0 c e)) = i" |
23274 | 1119 |
"\<delta> p = 1" |
1120 |
||
50313 | 1121 |
consts d_\<delta> :: "fm \<Rightarrow> int \<Rightarrow> bool" -- {* check if a given l divides all the ds above *} |
50252 | 1122 |
recdef d_\<delta> "measure size" |
50313 | 1123 |
"d_\<delta> (And p q) = (\<lambda>d. d_\<delta> p d \<and> d_\<delta> q d)" |
1124 |
"d_\<delta> (Or p q) = (\<lambda>d. d_\<delta> p d \<and> d_\<delta> q d)" |
|
1125 |
"d_\<delta> (Dvd i (CN 0 c e)) = (\<lambda>d. i dvd d)" |
|
1126 |
"d_\<delta> (NDvd i (CN 0 c e)) = (\<lambda>d. i dvd d)" |
|
1127 |
"d_\<delta> p = (\<lambda>d. True)" |
|
23274 | 1128 |
|
50313 | 1129 |
lemma delta_mono: |
23274 | 1130 |
assumes lin: "iszlfm p" |
50313 | 1131 |
and d: "d dvd d'" |
1132 |
and ad: "d_\<delta> p d" |
|
50252 | 1133 |
shows "d_\<delta> p d'" |
23274 | 1134 |
using lin ad d |
50313 | 1135 |
proof (induct p rule: iszlfm.induct) |
23274 | 1136 |
case (9 i c e) thus ?case using d |
30042 | 1137 |
by (simp add: dvd_trans[of "i" "d" "d'"]) |
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
|
1138 |
next |
23274 | 1139 |
case (10 i c e) thus ?case using d |
30042 | 1140 |
by (simp add: dvd_trans[of "i" "d" "d'"]) |
23274 | 1141 |
qed 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
|
1142 |
|
50313 | 1143 |
lemma \<delta>: |
1144 |
assumes lin:"iszlfm p" |
|
50252 | 1145 |
shows "d_\<delta> p (\<delta> p) \<and> \<delta> p >0" |
50313 | 1146 |
using lin |
23274 | 1147 |
proof (induct p rule: iszlfm.induct) |
50313 | 1148 |
case (1 p q) |
23274 | 1149 |
let ?d = "\<delta> (And p q)" |
41807 | 1150 |
from 1 lcm_pos_int have dp: "?d >0" by simp |
1151 |
have d1: "\<delta> p dvd \<delta> (And p q)" using 1 by simp |
|
50252 | 1152 |
hence th: "d_\<delta> p ?d" using delta_mono 1(2,3) by(simp only: iszlfm.simps) |
41807 | 1153 |
have "\<delta> q dvd \<delta> (And p q)" using 1 by simp |
50252 | 1154 |
hence th': "d_\<delta> q ?d" using delta_mono 1 by(simp only: iszlfm.simps) |
23984 | 1155 |
from th th' dp show ?case by simp |
23274 | 1156 |
next |
50313 | 1157 |
case (2 p q) |
23274 | 1158 |
let ?d = "\<delta> (And p q)" |
41807 | 1159 |
from 2 lcm_pos_int have dp: "?d >0" by simp |
1160 |
have "\<delta> p dvd \<delta> (And p q)" using 2 by simp |
|
50252 | 1161 |
hence th: "d_\<delta> p ?d" using delta_mono 2 by(simp only: iszlfm.simps) |
41807 | 1162 |
have "\<delta> q dvd \<delta> (And p q)" using 2 by simp |
50252 | 1163 |
hence th': "d_\<delta> q ?d" using delta_mono 2 by(simp only: iszlfm.simps) |
23984 | 1164 |
from th th' dp show ?case by 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
|
1165 |
qed simp_all |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
1166 |
|
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
diff
changeset
|
1167 |
|
50313 | 1168 |
consts a_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> fm" -- {* adjust the coeffitients of a formula *} |
50252 | 1169 |
recdef a_\<beta> "measure size" |
50313 | 1170 |
"a_\<beta> (And p q) = (\<lambda>k. And (a_\<beta> p k) (a_\<beta> q k))" |
1171 |
"a_\<beta> (Or p q) = (\<lambda>k. Or (a_\<beta> p k) (a_\<beta> q k))" |
|
1172 |
"a_\<beta> (Eq (CN 0 c e)) = (\<lambda>k. Eq (CN 0 1 (Mul (k div c) e)))" |
|
1173 |
"a_\<beta> (NEq (CN 0 c e)) = (\<lambda>k. NEq (CN 0 1 (Mul (k div c) e)))" |
|
1174 |
"a_\<beta> (Lt (CN 0 c e)) = (\<lambda>k. Lt (CN 0 1 (Mul (k div c) e)))" |
|
1175 |
"a_\<beta> (Le (CN 0 c e)) = (\<lambda>k. Le (CN 0 1 (Mul (k div c) e)))" |
|
1176 |
"a_\<beta> (Gt (CN 0 c e)) = (\<lambda>k. Gt (CN 0 1 (Mul (k div c) e)))" |
|
1177 |
"a_\<beta> (Ge (CN 0 c e)) = (\<lambda>k. Ge (CN 0 1 (Mul (k div c) e)))" |
|
1178 |
"a_\<beta> (Dvd i (CN 0 c e)) =(\<lambda>k. Dvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))" |
|
1179 |
"a_\<beta> (NDvd i (CN 0 c e))=(\<lambda>k. NDvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))" |
|
1180 |
"a_\<beta> p = (\<lambda>k. 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
|
1181 |
|
50313 | 1182 |
consts d_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> bool" -- {* test if all coeffs c of c divide a given l *} |
50252 | 1183 |
recdef d_\<beta> "measure size" |
50313 | 1184 |
"d_\<beta> (And p q) = (\<lambda>k. (d_\<beta> p k) \<and> (d_\<beta> q k))" |
1185 |
"d_\<beta> (Or p q) = (\<lambda>k. (d_\<beta> p k) \<and> (d_\<beta> q k))" |
|
1186 |
"d_\<beta> (Eq (CN 0 c e)) = (\<lambda>k. c dvd k)" |
|
1187 |
"d_\<beta> (NEq (CN 0 c e)) = (\<lambda>k. c dvd k)" |
|
1188 |
"d_\<beta> (Lt (CN 0 c e)) = (\<lambda>k. c dvd k)" |
|
1189 |
"d_\<beta> (Le (CN 0 c e)) = (\<lambda>k. c dvd k)" |
|
1190 |
"d_\<beta> (Gt (CN 0 c e)) = (\<lambda>k. c dvd k)" |
|
1191 |
"d_\<beta> (Ge (CN 0 c e)) = (\<lambda>k. c dvd k)" |
|
1192 |
"d_\<beta> (Dvd i (CN 0 c e)) =(\<lambda>k. c dvd k)" |
|
1193 |
"d_\<beta> (NDvd i (CN 0 c e))=(\<lambda>k. c dvd k)" |
|
1194 |
"d_\<beta> p = (\<lambda>k. True)" |
|
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
|
1195 |
|
50313 | 1196 |
consts \<zeta> :: "fm \<Rightarrow> int" -- {* computes the lcm of all coefficients of x *} |
23274 | 1197 |
recdef \<zeta> "measure size" |
50313 | 1198 |
"\<zeta> (And p q) = lcm (\<zeta> p) (\<zeta> q)" |
1199 |
"\<zeta> (Or p q) = lcm (\<zeta> p) (\<zeta> q)" |
|
23995
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1200 |
"\<zeta> (Eq (CN 0 c e)) = c" |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1201 |
"\<zeta> (NEq (CN 0 c e)) = c" |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1202 |
"\<zeta> (Lt (CN 0 c e)) = c" |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1203 |
"\<zeta> (Le (CN 0 c e)) = c" |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1204 |
"\<zeta> (Gt (CN 0 c e)) = c" |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1205 |
"\<zeta> (Ge (CN 0 c e)) = c" |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1206 |
"\<zeta> (Dvd i (CN 0 c e)) = c" |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1207 |
"\<zeta> (NDvd i (CN 0 c e))= c" |
23274 | 1208 |
"\<zeta> p = 1" |
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
|
1209 |
|
50313 | 1210 |
consts \<beta> :: "fm \<Rightarrow> num list" |
23274 | 1211 |
recdef \<beta> "measure size" |
50313 | 1212 |
"\<beta> (And p q) = (\<beta> p @ \<beta> q)" |
1213 |
"\<beta> (Or p q) = (\<beta> p @ \<beta> q)" |
|
23995
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1214 |
"\<beta> (Eq (CN 0 c e)) = [Sub (C -1) e]" |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1215 |
"\<beta> (NEq (CN 0 c e)) = [Neg e]" |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1216 |
"\<beta> (Lt (CN 0 c e)) = []" |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1217 |
"\<beta> (Le (CN 0 c e)) = []" |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1218 |
"\<beta> (Gt (CN 0 c e)) = [Neg e]" |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1219 |
"\<beta> (Ge (CN 0 c e)) = [Sub (C -1) e]" |
23274 | 1220 |
"\<beta> p = []" |
19736 | 1221 |
|
50313 | 1222 |
consts \<alpha> :: "fm \<Rightarrow> num list" |
23274 | 1223 |
recdef \<alpha> "measure size" |
50313 | 1224 |
"\<alpha> (And p q) = (\<alpha> p @ \<alpha> q)" |
1225 |
"\<alpha> (Or p q) = (\<alpha> p @ \<alpha> q)" |
|
23995
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1226 |
"\<alpha> (Eq (CN 0 c e)) = [Add (C -1) e]" |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1227 |
"\<alpha> (NEq (CN 0 c e)) = [e]" |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1228 |
"\<alpha> (Lt (CN 0 c e)) = [e]" |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1229 |
"\<alpha> (Le (CN 0 c e)) = [Add (C -1) e]" |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1230 |
"\<alpha> (Gt (CN 0 c e)) = []" |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1231 |
"\<alpha> (Ge (CN 0 c e)) = []" |
23274 | 1232 |
"\<alpha> p = []" |
50313 | 1233 |
|
23274 | 1234 |
consts mirror :: "fm \<Rightarrow> fm" |
1235 |
recdef mirror "measure size" |
|
50313 | 1236 |
"mirror (And p q) = And (mirror p) (mirror q)" |
1237 |
"mirror (Or p q) = Or (mirror p) (mirror q)" |
|
23995
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1238 |
"mirror (Eq (CN 0 c e)) = Eq (CN 0 c (Neg e))" |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1239 |
"mirror (NEq (CN 0 c e)) = NEq (CN 0 c (Neg e))" |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1240 |
"mirror (Lt (CN 0 c e)) = Gt (CN 0 c (Neg e))" |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1241 |
"mirror (Le (CN 0 c e)) = Ge (CN 0 c (Neg e))" |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1242 |
"mirror (Gt (CN 0 c e)) = Lt (CN 0 c (Neg e))" |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1243 |
"mirror (Ge (CN 0 c e)) = Le (CN 0 c (Neg e))" |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1244 |
"mirror (Dvd i (CN 0 c e)) = Dvd i (CN 0 c (Neg e))" |
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1245 |
"mirror (NDvd i (CN 0 c e)) = NDvd i (CN 0 c (Neg e))" |
23274 | 1246 |
"mirror p = p" |
50313 | 1247 |
|
1248 |
text {* Lemmas for the correctness of @{text "\<sigma>_\<rho>"} *} |
|
1249 |
||
23274 | 1250 |
lemma dvd1_eq1: "x >0 \<Longrightarrow> (x::int) dvd 1 = (x = 1)" |
41807 | 1251 |
by 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
|
1252 |
|
23274 | 1253 |
lemma minusinf_inf: |
1254 |
assumes linp: "iszlfm p" |
|
50313 | 1255 |
and u: "d_\<beta> p 1" |
1256 |
shows "\<exists>(z::int). \<forall>x < z. Ifm bbs (x#bs) (minusinf p) = Ifm bbs (x#bs) p" |
|
1257 |
(is "?P p" is "\<exists>(z::int). \<forall>x < z. ?I x (?M p) = ?I x p") |
|
1258 |
using linp u |
|
23274 | 1259 |
proof (induct p rule: minusinf.induct) |
50313 | 1260 |
case (1 p q) thus ?case |
29700 | 1261 |
by auto (rule_tac x="min z za" in exI,simp) |
23274 | 1262 |
next |
50313 | 1263 |
case (2 p q) thus ?case |
29700 | 1264 |
by auto (rule_tac x="min z za" in exI,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
|
1265 |
next |
50313 | 1266 |
case (3 c e) hence c1: "c=1" and nb: "numbound0 e" by simp_all |
26934 | 1267 |
fix a |
50313 | 1268 |
from 3 have "\<forall>x<(- Inum (a#bs) e). c*x + Inum (x#bs) e \<noteq> 0" |
23274 | 1269 |
proof(clarsimp) |
1270 |
fix x assume "x < (- Inum (a#bs) e)" and"x + Inum (x#bs) e = 0" |
|
1271 |
with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"] |
|
1272 |
show "False" by simp |
|
1273 |
qed |
|
1274 |
thus ?case 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
|
1275 |
next |
50313 | 1276 |
case (4 c e) hence c1: "c=1" and nb: "numbound0 e" by simp_all |
26934 | 1277 |
fix a |
50313 | 1278 |
from 4 have "\<forall>x<(- Inum (a#bs) e). c*x + Inum (x#bs) e \<noteq> 0" |
23274 | 1279 |
proof(clarsimp) |
1280 |
fix x assume "x < (- Inum (a#bs) e)" and"x + Inum (x#bs) e = 0" |
|
1281 |
with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"] |
|
1282 |
show "False" by simp |
|
1283 |
qed |
|
1284 |
thus ?case 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
|
1285 |
next |
50313 | 1286 |
case (5 c e) hence c1: "c=1" and nb: "numbound0 e" by simp_all |
26934 | 1287 |
fix a |
50313 | 1288 |
from 5 have "\<forall>x<(- Inum (a#bs) e). c*x + Inum (x#bs) e < 0" |
23274 | 1289 |
proof(clarsimp) |
50313 | 1290 |
fix x assume "x < (- Inum (a#bs) e)" |
23274 | 1291 |
with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"] |
1292 |
show "x + Inum (x#bs) e < 0" by simp |
|
1293 |
qed |
|
1294 |
thus ?case by auto |
|
1295 |
next |
|
50313 | 1296 |
case (6 c e) hence c1: "c=1" and nb: "numbound0 e" by simp_all |
26934 | 1297 |
fix a |
50313 | 1298 |
from 6 have "\<forall>x<(- Inum (a#bs) e). c*x + Inum (x#bs) e \<le> 0" |
23274 | 1299 |
proof(clarsimp) |
50313 | 1300 |
fix x assume "x < (- Inum (a#bs) e)" |
23274 | 1301 |
with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"] |
1302 |
show "x + Inum (x#bs) e \<le> 0" by simp |
|
1303 |
qed |
|
1304 |
thus ?case by auto |
|
1305 |
next |
|
50313 | 1306 |
case (7 c e) hence c1: "c=1" and nb: "numbound0 e" by simp_all |
26934 | 1307 |
fix a |
50313 | 1308 |
from 7 have "\<forall>x<(- Inum (a#bs) e). \<not> (c*x + Inum (x#bs) e > 0)" |
23274 | 1309 |
proof(clarsimp) |
1310 |
fix x assume "x < (- Inum (a#bs) e)" and"x + Inum (x#bs) e > 0" |
|
1311 |
with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"] |
|
1312 |
show "False" by simp |
|
1313 |
qed |
|
1314 |
thus ?case by auto |
|
1315 |
next |
|
50313 | 1316 |
case (8 c e) hence c1: "c=1" and nb: "numbound0 e" by simp_all |
26934 | 1317 |
fix a |
50313 | 1318 |
from 8 have "\<forall>x<(- Inum (a#bs) e). \<not> (c*x + Inum (x#bs) e \<ge> 0)" |
23274 | 1319 |
proof(clarsimp) |
1320 |
fix x assume "x < (- Inum (a#bs) e)" and"x + Inum (x#bs) e \<ge> 0" |
|
1321 |
with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"] |
|
1322 |
show "False" by simp |
|
1323 |
qed |
|
1324 |
thus ?case by auto |
|
1325 |
qed 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
|
1326 |
|
23274 | 1327 |
lemma minusinf_repeats: |
50252 | 1328 |
assumes d: "d_\<delta> p d" and linp: "iszlfm p" |
23274 | 1329 |
shows "Ifm bbs ((x - k*d)#bs) (minusinf p) = Ifm bbs (x #bs) (minusinf p)" |
50313 | 1330 |
using linp d |
1331 |
proof (induct p rule: iszlfm.induct) |
|
1332 |
case (9 i c e) |
|
1333 |
hence nbe: "numbound0 e" and id: "i dvd d" by simp_all |
|
1334 |
hence "\<exists>k. d=i*k" by (simp add: dvd_def) |
|
1335 |
then obtain "di" where di_def: "d=i*di" by blast |
|
1336 |
show ?case |
|
1337 |
proof (simp add: numbound0_I[OF nbe,where bs="bs" and b="x - k * d" and b'="x"] right_diff_distrib, |
|
1338 |
rule iffI) |
|
1339 |
assume "i dvd c * x - c*(k*d) + Inum (x # bs) e" |
|
23274 | 1340 |
(is "?ri dvd ?rc*?rx - ?rc*(?rk*?rd) + ?I x e" is "?ri dvd ?rt") |
50313 | 1341 |
hence "\<exists>(l::int). ?rt = i * l" by (simp add: dvd_def) |
1342 |
hence "\<exists>(l::int). c*x+ ?I x e = i*l+c*(k * i*di)" |
|
1343 |
by (simp add: algebra_simps di_def) |
|
1344 |
hence "\<exists>(l::int). c*x+ ?I x e = i*(l + c*k*di)" |
|
1345 |
by (simp add: algebra_simps) |
|
1346 |
hence "\<exists>(l::int). c*x+ ?I x e = i*l" by blast |
|
1347 |
thus "i dvd c*x + Inum (x # bs) e" by (simp add: dvd_def) |
|
1348 |
next |
|
1349 |
assume "i dvd c*x + Inum (x # bs) e" (is "?ri dvd ?rc*?rx+?e") |
|
1350 |
hence "\<exists>(l::int). c*x+?e = i*l" by (simp add: dvd_def) |
|
1351 |
hence "\<exists>(l::int). c*x - c*(k*d) +?e = i*l - c*(k*d)" by simp |
|
1352 |
hence "\<exists>(l::int). c*x - c*(k*d) +?e = i*l - c*(k*i*di)" by (simp add: di_def) |
|
1353 |
hence "\<exists>(l::int). c*x - c*(k*d) +?e = i*((l - c*k*di))" by (simp add: algebra_simps) |
|
1354 |
hence "\<exists>(l::int). c*x - c * (k*d) +?e = i*l" by blast |
|
1355 |
thus "i dvd c*x - c*(k*d) + Inum (x # bs) e" by (simp add: dvd_def) |
|
1356 |
qed |
|
23274 | 1357 |
next |
50313 | 1358 |
case (10 i c e) |
1359 |
hence nbe: "numbound0 e" and id: "i dvd d" by simp_all |
|
1360 |
hence "\<exists>k. d=i*k" by (simp add: dvd_def) |
|
1361 |
then obtain "di" where di_def: "d=i*di" by blast |
|
1362 |
show ?case |
|
1363 |
proof(simp add: numbound0_I[OF nbe,where bs="bs" and b="x - k * d" and b'="x"] right_diff_distrib, rule iffI) |
|
1364 |
assume "i dvd c * x - c*(k*d) + Inum (x # bs) e" |
|
23274 | 1365 |
(is "?ri dvd ?rc*?rx - ?rc*(?rk*?rd) + ?I x e" is "?ri dvd ?rt") |
50313 | 1366 |
hence "\<exists>(l::int). ?rt = i * l" by (simp add: dvd_def) |
1367 |
hence "\<exists>(l::int). c*x+ ?I x e = i*l+c*(k * i*di)" |
|
1368 |
by (simp add: algebra_simps di_def) |
|
1369 |
hence "\<exists>(l::int). c*x+ ?I x e = i*(l + c*k*di)" |
|
1370 |
by (simp add: algebra_simps) |
|
1371 |
hence "\<exists>(l::int). c*x+ ?I x e = i*l" by blast |
|
1372 |
thus "i dvd c*x + Inum (x # bs) e" by (simp add: dvd_def) |
|
1373 |
next |
|
1374 |
assume |
|
1375 |
"i dvd c*x + Inum (x # bs) e" (is "?ri dvd ?rc*?rx+?e") |
|
1376 |
hence "\<exists>(l::int). c*x+?e = i*l" by (simp add: dvd_def) |
|
1377 |
hence "\<exists>(l::int). c*x - c*(k*d) +?e = i*l - c*(k*d)" by simp |
|
1378 |
hence "\<exists>(l::int). c*x - c*(k*d) +?e = i*l - c*(k*i*di)" by (simp add: di_def) |
|
1379 |
hence "\<exists>(l::int). c*x - c*(k*d) +?e = i*((l - c*k*di))" by (simp add: algebra_simps) |
|
1380 |
hence "\<exists>(l::int). c*x - c * (k*d) +?e = i*l" |
|
1381 |
by blast |
|
1382 |
thus "i dvd c*x - c*(k*d) + Inum (x # bs) e" by (simp add: dvd_def) |
|
1383 |
qed |
|
23689
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23515
diff
changeset
|
1384 |
qed (auto simp add: gr0_conv_Suc numbound0_I[where bs="bs" and b="x - k*d" and b'="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
|
1385 |
|
50252 | 1386 |
lemma mirror_\<alpha>_\<beta>: |
23274 | 1387 |
assumes lp: "iszlfm p" |
1388 |
shows "(Inum (i#bs)) ` set (\<alpha> p) = (Inum (i#bs)) ` set (\<beta> (mirror p))" |
|
50313 | 1389 |
using lp by (induct p rule: mirror.induct) 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
|
1390 |
|
50313 | 1391 |
lemma mirror: |
23274 | 1392 |
assumes lp: "iszlfm p" |
50313 | 1393 |
shows "Ifm bbs (x#bs) (mirror p) = Ifm bbs ((- x)#bs) p" |
1394 |
using lp |
|
1395 |
proof (induct p rule: iszlfm.induct) |
|
1396 |
case (9 j c e) |
|
1397 |
hence nb: "numbound0 e" by simp |
|
1398 |
have "Ifm bbs (x#bs) (mirror (Dvd j (CN 0 c e))) = (j dvd c*x - Inum (x#bs) e)" |
|
1399 |
(is "_ = (j dvd c*x - ?e)") by simp |
|
1400 |
also have "\<dots> = (j dvd (- (c*x - ?e)))" |
|
30042 | 1401 |
by (simp only: dvd_minus_iff) |
23274 | 1402 |
also have "\<dots> = (j dvd (c* (- x)) + ?e)" |
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53168
diff
changeset
|
1403 |
by (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] add_ac minus_add_distrib) |
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53168
diff
changeset
|
1404 |
(simp add: algebra_simps) |
23995
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1405 |
also have "\<dots> = Ifm bbs ((- x)#bs) (Dvd j (CN 0 c e))" |
50313 | 1406 |
using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"] by simp |
23274 | 1407 |
finally show ?case . |
1408 |
next |
|
50313 | 1409 |
case (10 j c e) hence nb: "numbound0 e" by simp |
1410 |
have "Ifm bbs (x#bs) (mirror (Dvd j (CN 0 c e))) = (j dvd c*x - Inum (x#bs) e)" |
|
1411 |
(is "_ = (j dvd c*x - ?e)") by simp |
|
1412 |
also have "\<dots> = (j dvd (- (c*x - ?e)))" |
|
30042 | 1413 |
by (simp only: dvd_minus_iff) |
23274 | 1414 |
also have "\<dots> = (j dvd (c* (- x)) + ?e)" |
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53168
diff
changeset
|
1415 |
by (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] add_ac minus_add_distrib) |
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53168
diff
changeset
|
1416 |
(simp add: algebra_simps) |
23995
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1417 |
also have "\<dots> = Ifm bbs ((- x)#bs) (Dvd j (CN 0 c e))" |
50313 | 1418 |
using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"] by simp |
23274 | 1419 |
finally show ?case by simp |
23689
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23515
diff
changeset
|
1420 |
qed (auto simp add: numbound0_I[where bs="bs" and b="x" and b'="- x"] gr0_conv_Suc) |
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
|
1421 |
|
50313 | 1422 |
lemma mirror_l: "iszlfm p \<and> d_\<beta> p 1 \<Longrightarrow> iszlfm (mirror p) \<and> d_\<beta> (mirror p) 1" |
41807 | 1423 |
by (induct p rule: mirror.induct) 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
|
1424 |
|
23274 | 1425 |
lemma mirror_\<delta>: "iszlfm p \<Longrightarrow> \<delta> (mirror p) = \<delta> p" |
41807 | 1426 |
by (induct p rule: mirror.induct) auto |
23274 | 1427 |
|
50313 | 1428 |
lemma \<beta>_numbound0: |
1429 |
assumes lp: "iszlfm p" |
|
1430 |
shows "\<forall>b\<in> set (\<beta> p). numbound0 b" |
|
41807 | 1431 |
using lp by (induct p rule: \<beta>.induct) 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
|
1432 |
|
50313 | 1433 |
lemma d_\<beta>_mono: |
23274 | 1434 |
assumes linp: "iszlfm p" |
50313 | 1435 |
and dr: "d_\<beta> p l" |
1436 |
and d: "l dvd l'" |
|
50252 | 1437 |
shows "d_\<beta> p l'" |
50313 | 1438 |
using dr linp dvd_trans[of _ "l" "l'", simplified d] |
41807 | 1439 |
by (induct p rule: iszlfm.induct) simp_all |
23274 | 1440 |
|
50313 | 1441 |
lemma \<alpha>_l: |
1442 |
assumes lp: "iszlfm p" |
|
1443 |
shows "\<forall>b \<in> set (\<alpha> p). numbound0 b" |
|
1444 |
using lp by (induct p rule: \<alpha>.induct) 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
|
1445 |
|
50313 | 1446 |
lemma \<zeta>: |
23274 | 1447 |
assumes linp: "iszlfm p" |
50252 | 1448 |
shows "\<zeta> p > 0 \<and> d_\<beta> p (\<zeta> p)" |
50313 | 1449 |
using linp |
1450 |
proof (induct p rule: iszlfm.induct) |
|
23274 | 1451 |
case (1 p q) |
41807 | 1452 |
from 1 have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp |
1453 |
from 1 have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp |
|
50313 | 1454 |
from 1 d_\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"] |
1455 |
d_\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"] |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31730
diff
changeset
|
1456 |
dl1 dl2 show ?case by (auto simp add: lcm_pos_int) |
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
|
1457 |
next |
23274 | 1458 |
case (2 p q) |
41807 | 1459 |
from 2 have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp |
1460 |
from 2 have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp |
|
50313 | 1461 |
from 2 d_\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"] |
1462 |
d_\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"] |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31730
diff
changeset
|
1463 |
dl1 dl2 show ?case by (auto simp add: lcm_pos_int) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31730
diff
changeset
|
1464 |
qed (auto simp add: lcm_pos_int) |
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
|
1465 |
|
50313 | 1466 |
lemma a_\<beta>: |
1467 |
assumes linp: "iszlfm p" and d: "d_\<beta> p l" and lp: "l > 0" |
|
50252 | 1468 |
shows "iszlfm (a_\<beta> p l) \<and> d_\<beta> (a_\<beta> p l) 1 \<and> (Ifm bbs (l*x #bs) (a_\<beta> p l) = Ifm bbs (x#bs) p)" |
50313 | 1469 |
using linp d |
23274 | 1470 |
proof (induct p rule: iszlfm.induct) |
50313 | 1471 |
case (5 c e) |
1472 |
hence cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp_all |
|
1473 |
from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp]) |
|
1474 |
from cp have cnz: "c \<noteq> 0" by simp |
|
1475 |
have "c div c\<le> l div c" |
|
1476 |
by (simp add: zdiv_mono1[OF clel cp]) |
|
1477 |
then have ldcp:"0 < l div c" |
|
1478 |
by (simp add: div_self[OF cnz]) |
|
1479 |
have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] |
|
1480 |
by simp |
|
1481 |
hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] |
|
1482 |
by simp |
|
1483 |
hence "(l*x + (l div c) * Inum (x # bs) e < 0) = |
|
1484 |
((c * (l div c)) * x + (l div c) * Inum (x # bs) e < 0)" |
|
1485 |
by simp |
|
1486 |
also have "\<dots> = ((l div c) * (c*x + Inum (x # bs) e) < (l div c) * 0)" |
|
1487 |
by (simp add: algebra_simps) |
|
1488 |
also have "\<dots> = (c*x + Inum (x # bs) e < 0)" |
|
23274 | 1489 |
using mult_less_0_iff [where a="(l div c)" and b="c*x + Inum (x # bs) e"] ldcp by simp |
50313 | 1490 |
finally show ?case |
1491 |
using numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"] be by 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
|
1492 |
next |
50313 | 1493 |
case (6 c e) |
1494 |
hence cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp_all |
|
1495 |
from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp]) |
|
1496 |
from cp have cnz: "c \<noteq> 0" by simp |
|
1497 |
have "c div c\<le> l div c" |
|
1498 |
by (simp add: zdiv_mono1[OF clel cp]) |
|
1499 |
then have ldcp:"0 < l div c" |
|
1500 |
by (simp add: div_self[OF cnz]) |
|
1501 |
have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] |
|
1502 |
by simp |
|
1503 |
hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] |
|
1504 |
by simp |
|
1505 |
hence "(l*x + (l div c) * Inum (x# bs) e \<le> 0) = |
|
1506 |
((c * (l div c)) * x + (l div c) * Inum (x # bs) e \<le> 0)" by simp |
|
1507 |
also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) \<le> ((l div c)) * 0)" |
|
1508 |
by (simp add: algebra_simps) |
|
1509 |
also have "\<dots> = (c*x + Inum (x # bs) e \<le> 0)" |
|
23274 | 1510 |
using mult_le_0_iff [where a="(l div c)" and b="c*x + Inum (x # bs) e"] ldcp by simp |
50313 | 1511 |
finally show ?case |
1512 |
using numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"] be by 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
|
1513 |
next |
50313 | 1514 |
case (7 c e) |
1515 |
hence cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp_all |
|
1516 |
from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp]) |
|
1517 |
from cp have cnz: "c \<noteq> 0" by simp |
|
1518 |
have "c div c\<le> l div c" |
|
1519 |
by (simp add: zdiv_mono1[OF clel cp]) |
|
1520 |
then have ldcp:"0 < l div c" |
|
1521 |
by (simp add: div_self[OF cnz]) |
|
1522 |
have "c * (l div c) = c* (l div c) + l mod c" |
|
1523 |
using d' dvd_eq_mod_eq_0[of "c" "l"] by simp |
|
1524 |
hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] |
|
1525 |
by simp |
|
1526 |
hence "(l*x + (l div c)* Inum (x # bs) e > 0) = |
|
1527 |
((c * (l div c)) * x + (l div c) * Inum (x # bs) e > 0)" by simp |
|
1528 |
also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) > ((l div c)) * 0)" |
|
1529 |
by (simp add: algebra_simps) |
|
1530 |
also have "\<dots> = (c * x + Inum (x # bs) e > 0)" |
|
23274 | 1531 |
using zero_less_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e"] ldcp by simp |
50313 | 1532 |
finally show ?case |
1533 |
using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be by 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
|
1534 |
next |
50313 | 1535 |
case (8 c e) |
1536 |
hence cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp_all |
|
1537 |
from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp]) |
|
1538 |
from cp have cnz: "c \<noteq> 0" by simp |
|
1539 |
have "c div c\<le> l div c" |
|
1540 |
by (simp add: zdiv_mono1[OF clel cp]) |
|
1541 |
then have ldcp:"0 < l div c" |
|
1542 |
by (simp add: div_self[OF cnz]) |
|
1543 |
have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] |
|
1544 |
by simp |
|
1545 |
hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] |
|
23274 | 1546 |
by simp |
50313 | 1547 |
hence "(l*x + (l div c)* Inum (x # bs) e \<ge> 0) = |
1548 |
((c*(l div c))*x + (l div c)* Inum (x # bs) e \<ge> 0)" by simp |
|
1549 |
also have "\<dots> = ((l div c)*(c*x + Inum (x # bs) e) \<ge> ((l div c)) * 0)" |
|
1550 |
by (simp add: algebra_simps) |
|
1551 |
also have "\<dots> = (c*x + Inum (x # bs) e \<ge> 0)" |
|
1552 |
using ldcp zero_le_mult_iff [where a="l div c" and b="c*x + Inum (x # bs) e"] by simp |
|
1553 |
finally show ?case |
|
1554 |
using be numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"] by 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
|
1555 |
next |
50313 | 1556 |
case (3 c e) |
1557 |
hence cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp_all |
|
1558 |
from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp]) |
|
1559 |
from cp have cnz: "c \<noteq> 0" by simp |
|
1560 |
have "c div c\<le> l div c" |
|
1561 |
by (simp add: zdiv_mono1[OF clel cp]) |
|
1562 |
then have ldcp:"0 < l div c" |
|
1563 |
by (simp add: div_self[OF cnz]) |
|
1564 |
have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] |
|
1565 |
by simp |
|
1566 |
hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] |
|
1567 |
by simp |
|
1568 |
hence "(l * x + (l div c) * Inum (x # bs) e = 0) = |
|
1569 |
((c * (l div c)) * x + (l div c) * Inum (x # bs) e = 0)" by simp |
|
1570 |
also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) = ((l div c)) * 0)" |
|
1571 |
by (simp add: algebra_simps) |
|
1572 |
also have "\<dots> = (c * x + Inum (x # bs) e = 0)" |
|
23274 | 1573 |
using mult_eq_0_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e"] ldcp by simp |
50313 | 1574 |
finally show ?case |
1575 |
using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be by 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
|
1576 |
next |
50313 | 1577 |
case (4 c e) |
1578 |
hence cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp_all |
|
1579 |
from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp]) |
|
1580 |
from cp have cnz: "c \<noteq> 0" by simp |
|
1581 |
have "c div c\<le> l div c" |
|
1582 |
by (simp add: zdiv_mono1[OF clel cp]) |
|
1583 |
then have ldcp:"0 < l div c" |
|
1584 |
by (simp add: div_self[OF cnz]) |
|
1585 |
have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] |
|
1586 |
by simp |
|
1587 |
hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] |
|
1588 |
by simp |
|
1589 |
hence "(l * x + (l div c) * Inum (x # bs) e \<noteq> 0) = |
|
1590 |
((c * (l div c)) * x + (l div c) * Inum (x # bs) e \<noteq> 0)" by simp |
|
1591 |
also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) \<noteq> ((l div c)) * 0)" |
|
1592 |
by (simp add: algebra_simps) |
|
1593 |
also have "\<dots> = (c * x + Inum (x # bs) e \<noteq> 0)" |
|
23274 | 1594 |
using zero_le_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e"] ldcp by simp |
50313 | 1595 |
finally show ?case |
1596 |
using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be by 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
|
1597 |
next |
50313 | 1598 |
case (9 j c e) |
1599 |
hence cp: "c>0" and be: "numbound0 e" and jp: "j > 0" and d': "c dvd l" by simp_all |
|
1600 |
from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp]) |
|
1601 |
from cp have cnz: "c \<noteq> 0" by simp |
|
1602 |
have "c div c\<le> l div c" |
|
1603 |
by (simp add: zdiv_mono1[OF clel cp]) |
|
1604 |
then have ldcp:"0 < l div c" |
|
1605 |
by (simp add: div_self[OF cnz]) |
|
1606 |
have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] |
|
1607 |
by simp |
|
1608 |
hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] |
|
1609 |
by simp |
|
1610 |
hence "(\<exists>(k::int). l * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k) = |
|
1611 |
(\<exists>(k::int). (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)" by simp |
|
1612 |
also have "\<dots> = (\<exists>(k::int). (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c)*0)" |
|
1613 |
by (simp add: algebra_simps) |
|
1614 |
also have "\<dots> = (\<exists>(k::int). c * x + Inum (x # bs) e - j * k = 0)" |
|
1615 |
using zero_le_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e - j * k"] ldcp |
|
1616 |
by simp |
|
1617 |
also have "\<dots> = (\<exists>(k::int). c * x + Inum (x # bs) e = j * k)" by simp |
|
1618 |
finally show ?case |
|
1619 |
using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be mult_strict_mono[OF ldcp jp ldcp ] |
|
1620 |
by (simp add: dvd_def) |
|
1621 |
next |
|
1622 |
case (10 j c e) |
|
1623 |
hence cp: "c>0" and be: "numbound0 e" and jp: "j > 0" and d': "c dvd l" by simp_all |
|
1624 |
from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp]) |
|
1625 |
from cp have cnz: "c \<noteq> 0" by simp |
|
1626 |
have "c div c\<le> l div c" |
|
1627 |
by (simp add: zdiv_mono1[OF clel cp]) |
|
1628 |
then have ldcp:"0 < l div c" |
|
1629 |
by (simp add: div_self[OF cnz]) |
|
1630 |
have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp |
|
1631 |
hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] |
|
1632 |
by simp |
|
1633 |
hence "(\<exists>(k::int). l * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k) = (\<exists>(k::int). (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)" by simp |
|
1634 |
also have "\<dots> = (\<exists>(k::int). (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c)*0)" by (simp add: algebra_simps) |
|
1635 |
also fix k have "\<dots> = (\<exists>(k::int). c * x + Inum (x # bs) e - j * k = 0)" |
|
23274 | 1636 |
using zero_le_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e - j * k"] ldcp by simp |
50313 | 1637 |
also have "\<dots> = (\<exists>(k::int). c * x + Inum (x # bs) e = j * k)" by simp |
23274 | 1638 |
finally show ?case using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be mult_strict_mono[OF ldcp jp ldcp ] by (simp add: dvd_def) |
23689
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23515
diff
changeset
|
1639 |
qed (auto simp add: gr0_conv_Suc numbound0_I[where bs="bs" and b="(l * x)" and b'="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
|
1640 |
|
50252 | 1641 |
lemma a_\<beta>_ex: assumes linp: "iszlfm p" and d: "d_\<beta> p l" and lp: "l>0" |
50313 | 1642 |
shows "(\<exists>x. l dvd x \<and> Ifm bbs (x #bs) (a_\<beta> p l)) = (\<exists>(x::int). Ifm bbs (x#bs) p)" |
1643 |
(is "(\<exists>x. l dvd x \<and> ?P x) = (\<exists>x. ?P' x)") |
|
23274 | 1644 |
proof- |
50313 | 1645 |
have "(\<exists>x. l dvd x \<and> ?P x) = (\<exists>(x::int). ?P (l*x))" |
23274 | 1646 |
using unity_coeff_ex[where l="l" and P="?P", simplified] by simp |
50313 | 1647 |
also have "\<dots> = (\<exists>(x::int). ?P' x)" using a_\<beta>[OF linp d lp] by simp |
1648 |
finally show ?thesis . |
|
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
|
1649 |
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
|
1650 |
|
23274 | 1651 |
lemma \<beta>: |
1652 |
assumes lp: "iszlfm p" |
|
50252 | 1653 |
and u: "d_\<beta> p 1" |
1654 |
and d: "d_\<delta> p d" |
|
23274 | 1655 |
and dp: "d > 0" |
50313 | 1656 |
and nob: "\<not>(\<exists>(j::int) \<in> {1 .. d}. \<exists>b\<in> (Inum (a#bs)) ` set(\<beta> p). x = b + j)" |
23274 | 1657 |
and p: "Ifm bbs (x#bs) p" (is "?P x") |
1658 |
shows "?P (x - d)" |
|
1659 |
using lp u d dp nob p |
|
1660 |
proof(induct p rule: iszlfm.induct) |
|
41807 | 1661 |
case (5 c e) hence c1: "c=1" and bn:"numbound0 e" by simp_all |
1662 |
with dp p c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] 5 |
|
1663 |
show ?case by simp |
|
23274 | 1664 |
next |
41807 | 1665 |
case (6 c e) hence c1: "c=1" and bn:"numbound0 e" by simp_all |
1666 |
with dp p c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] 6 |
|
1667 |
show ?case by simp |
|
23274 | 1668 |
next |
41807 | 1669 |
case (7 c e) hence p: "Ifm bbs (x #bs) (Gt (CN 0 c e))" and c1: "c=1" and bn:"numbound0 e" by simp_all |
1670 |
let ?e = "Inum (x # bs) e" |
|
50313 | 1671 |
{assume "(x-d) +?e > 0" hence ?case using c1 |
41807 | 1672 |
numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] by simp} |
1673 |
moreover |
|
50313 | 1674 |
{assume H: "\<not> (x-d) + ?e > 0" |
41807 | 1675 |
let ?v="Neg e" |
1676 |
have vb: "?v \<in> set (\<beta> (Gt (CN 0 c e)))" by simp |
|
55584 | 1677 |
from 7(5)[simplified simp_thms Inum.simps \<beta>.simps set_simps bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]] |
50313 | 1678 |
have nob: "\<not> (\<exists>j\<in> {1 ..d}. x = - ?e + j)" by auto |
41807 | 1679 |
from H p have "x + ?e > 0 \<and> x + ?e \<le> d" by (simp add: c1) |
1680 |
hence "x + ?e \<ge> 1 \<and> x + ?e \<le> d" by simp |
|
50313 | 1681 |
hence "\<exists>(j::int) \<in> {1 .. d}. j = x + ?e" by simp |
1682 |
hence "\<exists>(j::int) \<in> {1 .. d}. x = (- ?e + j)" |
|
41807 | 1683 |
by (simp add: algebra_simps) |
1684 |
with nob have ?case by auto} |
|
1685 |
ultimately show ?case by blast |
|
23274 | 1686 |
next |
50313 | 1687 |
case (8 c e) hence p: "Ifm bbs (x #bs) (Ge (CN 0 c e))" and c1: "c=1" and bn:"numbound0 e" |
1688 |
by simp_all |
|
23274 | 1689 |
let ?e = "Inum (x # bs) e" |
50313 | 1690 |
{assume "(x-d) +?e \<ge> 0" hence ?case using c1 |
23274 | 1691 |
numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31952
diff
changeset
|
1692 |
by simp} |
23274 | 1693 |
moreover |
50313 | 1694 |
{assume H: "\<not> (x-d) + ?e \<ge> 0" |
23274 | 1695 |
let ?v="Sub (C -1) e" |
23995
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1696 |
have vb: "?v \<in> set (\<beta> (Ge (CN 0 c e)))" by simp |
55584 | 1697 |
from 8(5)[simplified simp_thms Inum.simps \<beta>.simps set_simps bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]] |
50313 | 1698 |
have nob: "\<not> (\<exists>j\<in> {1 ..d}. x = - ?e - 1 + j)" by auto |
23274 | 1699 |
from H p have "x + ?e \<ge> 0 \<and> x + ?e < d" by (simp add: c1) |
1700 |
hence "x + ?e +1 \<ge> 1 \<and> x + ?e + 1 \<le> d" by simp |
|
50313 | 1701 |
hence "\<exists>(j::int) \<in> {1 .. d}. j = x + ?e + 1" by simp |
1702 |
hence "\<exists>(j::int) \<in> {1 .. d}. x= - ?e - 1 + j" by (simp add: algebra_simps) |
|
23274 | 1703 |
with nob have ?case by simp } |
1704 |
ultimately show ?case by blast |
|
1705 |
next |
|
50313 | 1706 |
case (3 c e) hence p: "Ifm bbs (x #bs) (Eq (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" by simp_all |
23274 | 1707 |
let ?e = "Inum (x # bs) e" |
1708 |
let ?v="(Sub (C -1) e)" |
|
23995
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1709 |
have vb: "?v \<in> set (\<beta> (Eq (CN 0 c e)))" by simp |
41807 | 1710 |
from p have "x= - ?e" by (simp add: c1) with 3(5) show ?case using dp |
23274 | 1711 |
by simp (erule ballE[where x="1"], |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31952
diff
changeset
|
1712 |
simp_all add:algebra_simps numbound0_I[OF bn,where b="x"and b'="a"and bs="bs"]) |
23274 | 1713 |
next |
50313 | 1714 |
case (4 c e)hence p: "Ifm bbs (x #bs) (NEq (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" by simp_all |
23274 | 1715 |
let ?e = "Inum (x # bs) e" |
1716 |
let ?v="Neg e" |
|
23995
c34490f1e0ff
Updated proofs; changed shadow syntax to improve (processing) time
chaieb
parents:
23984
diff
changeset
|
1717 |
have vb: "?v \<in> set (\<beta> (NEq (CN 0 c e)))" by simp |
50313 | 1718 |
{assume "x - d + Inum (((x -d)) # bs) e \<noteq> 0" |
23274 | 1719 |
hence ?case by (simp add: c1)} |
1720 |
moreover |
|
1721 |
{assume H: "x - d + Inum (((x -d)) # bs) e = 0" |
|
1722 |
hence "x = - Inum (((x -d)) # bs) e + d" by simp |
|
1723 |
hence "x = - Inum (a # bs) e + d" |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31952
diff
changeset
|
1724 |
by (simp add: numbound0_I[OF bn,where b="x - d"and b'="a"and bs="bs"]) |
41807 | 1725 |
with 4(5) have ?case using dp by simp} |
23274 | 1726 |
ultimately show ?case by blast |
50313 | 1727 |
next |
1728 |
case (9 j c e) hence p: "Ifm bbs (x #bs) (Dvd j (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" by simp_all |
|
23274 | 1729 |
let ?e = "Inum (x # bs) e" |
41807 | 1730 |
from 9 have id: "j dvd d" by simp |
23274 | 1731 |
from c1 have "?p x = (j dvd (x+ ?e))" by simp |
50313 | 1732 |
also have "\<dots> = (j dvd x - d + ?e)" |
23689
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23515
diff
changeset
|
1733 |
using zdvd_period[OF id, where x="x" and c="-1" and t="?e"] by simp |
50313 | 1734 |
finally show ?case |
23274 | 1735 |
using numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] c1 p by simp |
1736 |
next |
|
50313 | 1737 |
case (10 j c e) hence p: "Ifm bbs (x #bs) (NDvd j (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" by simp_all |
23274 | 1738 |
let ?e = "Inum (x # bs) e" |
41807 | 1739 |
from 10 have id: "j dvd d" by simp |
23274 | 1740 |
from c1 have "?p x = (\<not> j dvd (x+ ?e))" by simp |
50313 | 1741 |
also have "\<dots> = (\<not> j dvd x - d + ?e)" |
23689
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23515
diff
changeset
|
1742 |
using zdvd_period[OF id, where x="x" and c="-1" and t="?e"] by simp |
23274 | 1743 |
finally show ?case using numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] c1 p by simp |
23689
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23515
diff
changeset
|
1744 |
qed (auto simp add: numbound0_I[where bs="bs" and b="(x - d)" and b'="x"] gr0_conv_Suc) |
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
|
1745 |
|
50313 | 1746 |
lemma \<beta>': |
23274 | 1747 |
assumes lp: "iszlfm p" |
50252 | 1748 |
and u: "d_\<beta> p 1" |
1749 |
and d: "d_\<delta> p d" |
|
23274 | 1750 |
and dp: "d > 0" |
50313 | 1751 |
shows "\<forall>x. \<not>(\<exists>(j::int) \<in> {1 .. d}. \<exists>b\<in> set(\<beta> p). Ifm bbs ((Inum (a#bs) b + j) #bs) p) \<longrightarrow> Ifm bbs (x#bs) p \<longrightarrow> Ifm bbs ((x - d)#bs) p" (is "\<forall>x. ?b \<longrightarrow> ?P x \<longrightarrow> ?P (x - d)") |
23274 | 1752 |
proof(clarify) |
50313 | 1753 |
fix x |
1754 |
assume nb:"?b" and px: "?P x" |
|
1755 |
hence nb2: "\<not>(\<exists>(j::int) \<in> {1 .. d}. \<exists>b\<in> (Inum (a#bs)) ` set(\<beta> p). x = b + j)" |
|
23274 | 1756 |
by auto |
1757 |
from \<beta>[OF lp u d dp nb2 px] show "?P (x -d )" . |
|
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
|
1758 |
qed |
23315 | 1759 |
lemma cpmi_eq: "0 < D \<Longrightarrow> (EX z::int. ALL x. x < z --> (P x = P1 x)) |
50313 | 1760 |
==> ALL x.~(EX (j::int) : {1..D}. EX (b::int) : B. P(b+j)) --> P (x) --> P (x - D) |
23315 | 1761 |
==> (ALL (x::int). ALL (k::int). ((P1 x)= (P1 (x-k*D)))) |
1762 |
==> (EX (x::int). P(x)) = ((EX (j::int) : {1..D} . (P1(j))) | (EX (j::int) : {1..D}. EX (b::int) : B. P (b+j)))" |
|
1763 |
apply(rule iffI) |
|
1764 |
prefer 2 |
|
1765 |
apply(drule minusinfinity) |
|
1766 |
apply assumption+ |
|
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
44821
diff
changeset
|
1767 |
apply(fastforce) |
23315 | 1768 |
apply clarsimp |
1769 |
apply(subgoal_tac "!!k. 0<=k \<Longrightarrow> !x. P x \<longrightarrow> P (x - k*D)") |
|
1770 |
apply(frule_tac x = x and z=z in decr_lemma) |
|
1771 |
apply(subgoal_tac "P1(x - (\<bar>x - z\<bar> + 1) * D)") |
|
1772 |
prefer 2 |
|
1773 |
apply(subgoal_tac "0 <= (\<bar>x - z\<bar> + 1)") |
|
1774 |
prefer 2 apply arith |
|
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
44821
diff
changeset
|
1775 |
apply fastforce |
23315 | 1776 |
apply(drule (1) periodic_finite_ex) |
1777 |
apply blast |
|
1778 |
apply(blast dest:decr_mult_lemma) |
|
1779 |
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
|
1780 |
|
23274 | 1781 |
theorem cp_thm: |
1782 |
assumes lp: "iszlfm p" |
|
50252 | 1783 |
and u: "d_\<beta> p 1" |
1784 |
and d: "d_\<delta> p d" |
|
23274 | 1785 |
and dp: "d > 0" |
50313 | 1786 |
shows "(\<exists>(x::int). Ifm bbs (x #bs) p) = (\<exists>j\<in> {1.. d}. Ifm bbs (j #bs) (minusinf p) \<or> (\<exists>b \<in> set (\<beta> p). Ifm bbs ((Inum (i#bs) b + j) #bs) p))" |
1787 |
(is "(\<exists>(x::int). ?P (x)) = (\<exists>j\<in> ?D. ?M j \<or> (\<exists>b\<in> ?B. ?P (?I b + j)))") |
|
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
|
1788 |
proof- |
50313 | 1789 |
from minusinf_inf[OF lp u] |
23274 | 1790 |
have th: "\<exists>(z::int). \<forall>x<z. ?P (x) = ?M x" by blast |
1791 |
let ?B' = "{?I b | b. b\<in> ?B}" |
|
50313 | 1792 |
have BB': "(\<exists>j\<in>?D. \<exists>b\<in> ?B. ?P (?I b +j)) = (\<exists>j \<in> ?D. \<exists>b \<in> ?B'. ?P (b + j))" by auto |
1793 |
hence th2: "\<forall>x. \<not> (\<exists>j \<in> ?D. \<exists>b \<in> ?B'. ?P ((b + j))) \<longrightarrow> ?P (x) \<longrightarrow> ?P ((x - d))" |
|
23274 | 1794 |
using \<beta>'[OF lp u d dp, where a="i" and bbs = "bbs"] by blast |
1795 |
from minusinf_repeats[OF d lp] |
|
50313 | 1796 |
have th3: "\<forall>x k. ?M x = ?M (x-k*d)" by simp |
23274 | 1797 |
from cpmi_eq[OF dp th th2 th3] BB' show ?thesis by blast |
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
|
1798 |
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
|
1799 |
|
23274 | 1800 |
(* Implement the right hand sides of Cooper's theorem and Ferrante and Rackoff. *) |
50313 | 1801 |
lemma mirror_ex: |
23274 | 1802 |
assumes lp: "iszlfm p" |
50313 | 1803 |
shows "(\<exists>x. Ifm bbs (x#bs) (mirror p)) = (\<exists>x. Ifm bbs (x#bs) p)" |
1804 |
(is "(\<exists>x. ?I x ?mp) = (\<exists>x. ?I x p)") |
|
23274 | 1805 |
proof(auto) |
1806 |
fix x assume "?I x ?mp" hence "?I (- x) p" using mirror[OF lp] by blast |
|
50313 | 1807 |
thus "\<exists>x. ?I x p" by blast |
23274 | 1808 |
next |
50313 | 1809 |
fix x assume "?I x p" hence "?I (- x) ?mp" |
23274 | 1810 |
using mirror[OF lp, where x="- x", symmetric] by auto |
50313 | 1811 |
thus "\<exists>x. ?I x ?mp" by blast |
23274 | 1812 |
qed |
24349 | 1813 |
|
1814 |
||
50313 | 1815 |
lemma cp_thm': |
23274 | 1816 |
assumes lp: "iszlfm p" |
50252 | 1817 |
and up: "d_\<beta> p 1" and dd: "d_\<delta> p d" and dp: "d > 0" |
50313 | 1818 |
shows "(\<exists>x. Ifm bbs (x#bs) p) = ((\<exists>j\<in> {1 .. d}. Ifm bbs (j#bs) (minusinf p)) \<or> (\<exists>j\<in> {1.. d}. \<exists>b\<in> (Inum (i#bs)) ` set (\<beta> p). Ifm bbs ((b+j)#bs) p))" |
23274 | 1819 |
using cp_thm[OF lp up dd dp,where i="i"] 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
|
1820 |
|
50313 | 1821 |
definition unit :: "fm \<Rightarrow> fm \<times> num list \<times> int" |
1822 |
where |
|
1823 |
"unit p = (let p' = zlfm p ; l = \<zeta> p' ; q = And (Dvd l (CN 0 1 (C 0))) (a_\<beta> p' l); d = \<delta> q; |
|
23274 | 1824 |
B = remdups (map simpnum (\<beta> q)) ; a = remdups (map simpnum (\<alpha> q)) |
1825 |
in if length B \<le> length a then (q,B,d) else (mirror q, a,d))" |
|
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
|
1826 |
|
50313 | 1827 |
lemma unit: |
1828 |
assumes qf: "qfree p" |
|
1829 |
shows "\<And>q B d. unit p = (q,B,d) \<Longrightarrow> ((\<exists>x. Ifm bbs (x#bs) p) = (\<exists>x. Ifm bbs (x#bs) q)) \<and> (Inum (i#bs)) ` set B = (Inum (i#bs)) ` set (\<beta> q) \<and> d_\<beta> q 1 \<and> d_\<delta> q d \<and> d >0 \<and> iszlfm q \<and> (\<forall>b\<in> set B. numbound0 b)" |
|
1830 |
proof - |
|
1831 |
fix q B d |
|
23274 | 1832 |
assume qBd: "unit p = (q,B,d)" |
50313 | 1833 |
let ?thes = "((\<exists>x. Ifm bbs (x#bs) p) = (\<exists>x. Ifm bbs (x#bs) q)) \<and> |
23274 | 1834 |
Inum (i#bs) ` set B = Inum (i#bs) ` set (\<beta> q) \<and> |
50313 | 1835 |
d_\<beta> q 1 \<and> d_\<delta> q d \<and> 0 < d \<and> iszlfm q \<and> (\<forall>b\<in> set B. numbound0 b)" |
1836 |
let ?I = "\<lambda>x p. Ifm bbs (x#bs) p" |
|
23274 | 1837 |
let ?p' = "zlfm p" |
1838 |
let ?l = "\<zeta> ?p'" |
|
50252 | 1839 |
let ?q = "And (Dvd ?l (CN 0 1 (C 0))) (a_\<beta> ?p' ?l)" |
23274 | 1840 |
let ?d = "\<delta> ?q" |
1841 |
let ?B = "set (\<beta> ?q)" |
|
1842 |
let ?B'= "remdups (map simpnum (\<beta> ?q))" |
|
1843 |
let ?A = "set (\<alpha> ?q)" |
|
1844 |
let ?A'= "remdups (map simpnum (\<alpha> ?q))" |
|
50313 | 1845 |
from conjunct1[OF zlfm_I[OF qf, where bs="bs"]] |
1846 |
have pp': "\<forall>i. ?I i ?p' = ?I i p" by auto |
|
23274 | 1847 |
from conjunct2[OF zlfm_I[OF qf, where bs="bs" and i="i"]] |
50313 | 1848 |
have lp': "iszlfm ?p'" . |
50252 | 1849 |
from lp' \<zeta>[where p="?p'"] have lp: "?l >0" and dl: "d_\<beta> ?p' ?l" by auto |
1850 |
from a_\<beta>_ex[where p="?p'" and l="?l" and bs="bs", OF lp' dl lp] pp' |
|
50313 | 1851 |
have pq_ex:"(\<exists>(x::int). ?I x p) = (\<exists>x. ?I x ?q)" by simp |
50252 | 1852 |
from lp' lp a_\<beta>[OF lp' dl lp] have lq:"iszlfm ?q" and uq: "d_\<beta> ?q 1" by auto |
1853 |
from \<delta>[OF lq] have dp:"?d >0" and dd: "d_\<delta> ?q ?d" by blast+ |
|
50313 | 1854 |
let ?N = "\<lambda>t. Inum (i#bs) t" |
1855 |
have "?N ` set ?B' = ((?N o simpnum) ` ?B)" by auto |
|
23274 | 1856 |
also have "\<dots> = ?N ` ?B" using simpnum_ci[where bs="i#bs"] by auto |
1857 |
finally have BB': "?N ` set ?B' = ?N ` ?B" . |
|
50313 | 1858 |
have "?N ` set ?A' = ((?N o simpnum) ` ?A)" by auto |
23274 | 1859 |
also have "\<dots> = ?N ` ?A" using simpnum_ci[where bs="i#bs"] by auto |
1860 |
finally have AA': "?N ` set ?A' = ?N ` ?A" . |
|
50313 | 1861 |
from \<beta>_numbound0[OF lq] have B_nb:"\<forall>b\<in> set ?B'. numbound0 b" |
23274 | 1862 |
by (simp add: simpnum_numbound0) |
50313 | 1863 |
from \<alpha>_l[OF lq] have A_nb: "\<forall>b\<in> set ?A'. numbound0 b" |
23274 | 1864 |
by (simp add: simpnum_numbound0) |
1865 |
{assume "length ?B' \<le> length ?A'" |
|
1866 |
hence q:"q=?q" and "B = ?B'" and d:"d = ?d" |
|
1867 |
using qBd by (auto simp add: Let_def unit_def) |
|
50313 | 1868 |
with BB' B_nb have b: "?N ` (set B) = ?N ` set (\<beta> q)" |
1869 |
and bn: "\<forall>b\<in> set B. numbound0 b" by simp_all |
|
23274 | 1870 |
with pq_ex dp uq dd lq q d have ?thes by simp} |
50313 | 1871 |
moreover |
23274 | 1872 |
{assume "\<not> (length ?B' \<le> length ?A')" |
1873 |
hence q:"q=mirror ?q" and "B = ?A'" and d:"d = ?d" |
|
1874 |
using qBd by (auto simp add: Let_def unit_def) |
|
50313 | 1875 |
with AA' mirror_\<alpha>_\<beta>[OF lq] A_nb have b:"?N ` (set B) = ?N ` set (\<beta> q)" |
1876 |
and bn: "\<forall>b\<in> set B. numbound0 b" by simp_all |
|
1877 |
from mirror_ex[OF lq] pq_ex q |
|
1878 |
have pqm_eq:"(\<exists>(x::int). ?I x p) = (\<exists>(x::int). ?I x q)" by simp |
|
23274 | 1879 |
from lq uq q mirror_l[where p="?q"] |
50252 | 1880 |
have lq': "iszlfm q" and uq: "d_\<beta> q 1" by auto |
1881 |
from \<delta>[OF lq'] mirror_\<delta>[OF lq] q d have dq:"d_\<delta> q d " by auto |
|
23274 | 1882 |
from pqm_eq b bn uq lq' dp dq q dp d have ?thes by simp |
1883 |
} |
|
1884 |
ultimately show ?thes by blast |
|
1885 |
qed |
|
50313 | 1886 |
|
1887 |
||
1888 |
text {* Cooper's Algorithm *} |
|
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
|
1889 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
33063
diff
changeset
|
1890 |
definition cooper :: "fm \<Rightarrow> fm" where |
50313 | 1891 |
"cooper p = |
1892 |
(let |
|
1893 |
(q, B, d) = unit p; |
|
1894 |
js = [1..d]; |
|
1895 |
mq = simpfm (minusinf q); |
|
1896 |
md = evaldjf (\<lambda>j. simpfm (subst0 (C j) mq)) js |
|
1897 |
in |
|
1898 |
if md = T then T |
|
1899 |
else |
|
1900 |
(let |
|
1901 |
qd = evaldjf (\<lambda>(b, j). simpfm (subst0 (Add b (C j)) q)) [(b, j). b \<leftarrow> B, j \<leftarrow> js] |
|
1902 |
in decr (disj md qd)))" |
|
1903 |
||
1904 |
lemma cooper: |
|
1905 |
assumes qf: "qfree p" |
|
1906 |
shows "((\<exists>x. Ifm bbs (x#bs) p) = (Ifm bbs bs (cooper p))) \<and> qfree (cooper p)" |
|
23274 | 1907 |
(is "(?lhs = ?rhs) \<and> _") |
50313 | 1908 |
proof - |
1909 |
let ?I = "\<lambda>x p. Ifm bbs (x#bs) p" |
|
23274 | 1910 |
let ?q = "fst (unit p)" |
1911 |
let ?B = "fst (snd(unit p))" |
|
1912 |
let ?d = "snd (snd (unit p))" |
|
41836 | 1913 |
let ?js = "[1..?d]" |
23274 | 1914 |
let ?mq = "minusinf ?q" |
1915 |
let ?smq = "simpfm ?mq" |
|
50313 | 1916 |
let ?md = "evaldjf (\<lambda>j. simpfm (subst0 (C j) ?smq)) ?js" |
26934 | 1917 |
fix i |
50313 | 1918 |
let ?N = "\<lambda>t. Inum (i#bs) t" |
24336 | 1919 |
let ?Bjs = "[(b,j). b\<leftarrow>?B,j\<leftarrow>?js]" |
50313 | 1920 |
let ?qd = "evaldjf (\<lambda>(b,j). simpfm (subst0 (Add b (C j)) ?q)) ?Bjs" |
23274 | 1921 |
have qbf:"unit p = (?q,?B,?d)" by simp |
50313 | 1922 |
from unit[OF qf qbf] have pq_ex: "(\<exists>(x::int). ?I x p) = (\<exists>(x::int). ?I x ?q)" and |
1923 |
B:"?N ` set ?B = ?N ` set (\<beta> ?q)" and |
|
1924 |
uq:"d_\<beta> ?q 1" and dd: "d_\<delta> ?q ?d" and dp: "?d > 0" and |
|
1925 |
lq: "iszlfm ?q" and |
|
1926 |
Bn: "\<forall>b\<in> set ?B. numbound0 b" by auto |
|
23274 | 1927 |
from zlin_qfree[OF lq] have qfq: "qfree ?q" . |
1928 |
from simpfm_qf[OF minusinf_qfree[OF qfq]] have qfmq: "qfree ?smq". |
|
50313 | 1929 |
have jsnb: "\<forall>j \<in> set ?js. numbound0 (C j)" by simp |
1930 |
hence "\<forall>j\<in> set ?js. bound0 (subst0 (C j) ?smq)" |
|
23274 | 1931 |
by (auto simp only: subst0_bound0[OF qfmq]) |
50313 | 1932 |
hence th: "\<forall>j\<in> set ?js. bound0 (simpfm (subst0 (C j) ?smq))" |
23274 | 1933 |
by (auto simp add: simpfm_bound0) |
50313 | 1934 |
from evaldjf_bound0[OF th] have mdb: "bound0 ?md" by simp |
1935 |
from Bn jsnb have "\<forall>(b,j) \<in> set ?Bjs. numbound0 (Add b (C j))" |
|
23689
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23515
diff
changeset
|
1936 |
by simp |
50313 | 1937 |
hence "\<forall>(b,j) \<in> set ?Bjs. bound0 (subst0 (Add b (C j)) ?q)" |
23274 | 1938 |
using subst0_bound0[OF qfq] by blast |
50313 | 1939 |
hence "\<forall>(b,j) \<in> set ?Bjs. bound0 (simpfm (subst0 (Add b (C j)) ?q))" |
23274 | 1940 |
using simpfm_bound0 by blast |
50313 | 1941 |
hence th': "\<forall>x \<in> set ?Bjs. bound0 ((\<lambda>(b,j). simpfm (subst0 (Add b (C j)) ?q)) x)" |
1942 |
by auto |
|
23274 | 1943 |
from evaldjf_bound0 [OF th'] have qdb: "bound0 ?qd" by simp |
50313 | 1944 |
from mdb qdb |
1945 |
have mdqdb: "bound0 (disj ?md ?qd)" unfolding disj_def by (cases "?md=T \<or> ?qd=T") simp_all |
|
23274 | 1946 |
from trans [OF pq_ex cp_thm'[OF lq uq dd dp,where i="i"]] B |
50313 | 1947 |
have "?lhs = (\<exists>j\<in> {1.. ?d}. ?I j ?mq \<or> (\<exists>b\<in> ?N ` set ?B. Ifm bbs ((b+ j)#bs) ?q))" by auto |
1948 |
also have "\<dots> = (\<exists>j\<in> {1.. ?d}. ?I j ?mq \<or> (\<exists>b\<in> set ?B. Ifm bbs ((?N b+ j)#bs) ?q))" by simp |
|
1949 |
also have "\<dots> = ((\<exists>j\<in> {1.. ?d}. ?I j ?mq ) \<or> |
|
1950 |
(\<exists>j\<in> {1.. ?d}. \<exists>b\<in> set ?B. Ifm bbs ((?N (Add b (C j)))#bs) ?q))" |
|
1951 |
by (simp only: Inum.simps) blast |
|
1952 |
also have "\<dots> = ((\<exists>j\<in> {1.. ?d}. ?I j ?smq ) \<or> |
|
1953 |
(\<exists>j\<in> {1.. ?d}. \<exists>b\<in> set ?B. Ifm bbs ((?N (Add b (C j)))#bs) ?q))" |
|
1954 |
by (simp add: simpfm) |
|
1955 |
also have "\<dots> = ((\<exists>j\<in> set ?js. (\<lambda>j. ?I i (simpfm (subst0 (C j) ?smq))) j) \<or> |
|
1956 |
(\<exists>j\<in> set ?js. \<exists>b\<in> set ?B. Ifm bbs ((?N (Add b (C j)))#bs) ?q))" |
|
41836 | 1957 |
by (simp only: simpfm subst0_I[OF qfmq] set_upto) auto |
50313 | 1958 |
also have "\<dots> = (?I i (evaldjf (\<lambda>j. simpfm (subst0 (C j) ?smq)) ?js) \<or> |
1959 |
(\<exists>j\<in> set ?js. \<exists>b\<in> set ?B. ?I i (subst0 (Add b (C j)) ?q)))" |
|
1960 |
by (simp only: evaldjf_ex subst0_I[OF qfq]) |
|
1961 |
also have "\<dots>= (?I i ?md \<or> (\<exists>(b,j) \<in> set ?Bjs. (\<lambda>(b,j). ?I i (simpfm (subst0 (Add b (C j)) ?q))) (b,j)))" |
|
1962 |
by (simp only: simpfm set_concat set_map concat_map_singleton UN_simps) blast |
|
1963 |
also have "\<dots> = (?I i ?md \<or> (?I i (evaldjf (\<lambda>(b,j). simpfm (subst0 (Add b (C j)) ?q)) ?Bjs)))" |
|
1964 |
by (simp only: evaldjf_ex[where bs="i#bs" and f="\<lambda>(b,j). simpfm (subst0 (Add b (C j)) ?q)" and ps="?Bjs"]) |
|
1965 |
(auto simp add: split_def) |
|
1966 |
finally have mdqd: "?lhs = (?I i ?md \<or> ?I i ?qd)" by simp |
|
23274 | 1967 |
also have "\<dots> = (?I i (disj ?md ?qd))" by (simp add: disj) |
50313 | 1968 |
also have "\<dots> = (Ifm bbs bs (decr (disj ?md ?qd)))" by (simp only: decr [OF mdqdb]) |
1969 |
finally have mdqd2: "?lhs = (Ifm bbs bs (decr (disj ?md ?qd)))" . |
|
1970 |
{ assume mdT: "?md = T" |
|
1971 |
hence cT:"cooper p = T" |
|
23274 | 1972 |
by (simp only: cooper_def unit_def split_def Let_def if_True) simp |
50313 | 1973 |
from mdT have lhs:"?lhs" using mdqd by simp |
23274 | 1974 |
from mdT have "?rhs" by (simp add: cooper_def unit_def split_def) |
1975 |
with lhs cT have ?thesis by 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
|
1976 |
moreover |
50313 | 1977 |
{ assume mdT: "?md \<noteq> T" hence "cooper p = decr (disj ?md ?qd)" |
1978 |
by (simp only: cooper_def unit_def split_def Let_def if_False) |
|
23274 | 1979 |
with mdqd2 decr_qf[OF mdqdb] have ?thesis by 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
|
1980 |
ultimately show ?thesis 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
|
1981 |
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
|
1982 |
|
27456 | 1983 |
definition pa :: "fm \<Rightarrow> fm" where |
1984 |
"pa p = qelim (prep p) cooper" |
|
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
|
1985 |
|
23274 | 1986 |
theorem mirqe: "(Ifm bbs bs (pa p) = Ifm bbs bs p) \<and> qfree (pa p)" |
1987 |
using qelim_ci cooper prep by (auto simp add: pa_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
|
1988 |
|
50313 | 1989 |
definition cooper_test :: "unit \<Rightarrow> fm" |
1990 |
where |
|
1991 |
"cooper_test u = |
|
1992 |
pa (E (A (Imp (Ge (Sub (Bound 0) (Bound 1))) |
|
1993 |
(E (E (Eq (Sub (Add (Mul 3 (Bound 1)) (Mul 5 (Bound 0))) (Bound 2))))))))" |
|
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
|
1994 |
|
51272 | 1995 |
ML_val {* @{code cooper_test} () *} |
27456 | 1996 |
|
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
50313
diff
changeset
|
1997 |
(*code_reflect Cooper_Procedure |
55685 | 1998 |
functions pa T Bound nat_of_integer integer_of_nat int_of_integer integer_of_int |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
50313
diff
changeset
|
1999 |
file "~~/src/HOL/Tools/Qelim/cooper_procedure.ML"*) |
27456 | 2000 |
|
28290 | 2001 |
oracle linzqe_oracle = {* |
27456 | 2002 |
let |
2003 |
||
2004 |
fun num_of_term vs (t as Free (xn, xT)) = (case AList.lookup (op =) vs t |
|
2005 |
of NONE => error "Variable not found in the list!" |
|
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
50313
diff
changeset
|
2006 |
| SOME n => @{code Bound} (@{code nat_of_integer} n)) |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
50313
diff
changeset
|
2007 |
| num_of_term vs @{term "0::int"} = @{code C} (@{code int_of_integer} 0) |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
50313
diff
changeset
|
2008 |
| num_of_term vs @{term "1::int"} = @{code C} (@{code int_of_integer} 1) |
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54230
diff
changeset
|
2009 |
| num_of_term vs @{term "- 1::int"} = @{code C} (@{code int_of_integer} (~ 1)) |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
50313
diff
changeset
|
2010 |
| num_of_term vs (@{term "numeral :: _ \<Rightarrow> int"} $ t) = |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
50313
diff
changeset
|
2011 |
@{code C} (@{code int_of_integer} (HOLogic.dest_num t)) |
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54230
diff
changeset
|
2012 |
| num_of_term vs (@{term "- numeral :: _ \<Rightarrow> int"} $ t) = |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
50313
diff
changeset
|
2013 |
@{code C} (@{code int_of_integer} (~(HOLogic.dest_num t))) |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
50313
diff
changeset
|
2014 |
| num_of_term vs (Bound i) = @{code Bound} (@{code nat_of_integer} i) |
27456 | 2015 |
| num_of_term vs (@{term "uminus :: int \<Rightarrow> int"} $ t') = @{code Neg} (num_of_term vs t') |
2016 |
| num_of_term vs (@{term "op + :: int \<Rightarrow> int \<Rightarrow> int"} $ t1 $ t2) = |
|
2017 |
@{code Add} (num_of_term vs t1, num_of_term vs t2) |
|
2018 |
| num_of_term vs (@{term "op - :: int \<Rightarrow> int \<Rightarrow> int"} $ t1 $ t2) = |
|
2019 |
@{code Sub} (num_of_term vs t1, num_of_term vs t2) |
|
2020 |
| num_of_term vs (@{term "op * :: int \<Rightarrow> int \<Rightarrow> int"} $ t1 $ t2) = |
|
2021 |
(case try HOLogic.dest_number t1 |
|
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
50313
diff
changeset
|
2022 |
of SOME (_, i) => @{code Mul} (@{code int_of_integer} i, num_of_term vs t2) |
27456 | 2023 |
| NONE => (case try HOLogic.dest_number t2 |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
50313
diff
changeset
|
2024 |
of SOME (_, i) => @{code Mul} (@{code int_of_integer} i, num_of_term vs t1) |
27456 | 2025 |
| NONE => error "num_of_term: unsupported multiplication")) |
28264 | 2026 |
| num_of_term vs t = error ("num_of_term: unknown term " ^ Syntax.string_of_term @{context} t); |
27456 | 2027 |
|
2028 |
fun fm_of_term ps vs @{term True} = @{code T} |
|
2029 |
| fm_of_term ps vs @{term False} = @{code F} |
|
2030 |
| fm_of_term ps vs (@{term "op < :: int \<Rightarrow> int \<Rightarrow> bool"} $ t1 $ t2) = |
|
2031 |
@{code Lt} (@{code Sub} (num_of_term vs t1, num_of_term vs t2)) |
|
2032 |
| fm_of_term ps vs (@{term "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"} $ t1 $ t2) = |
|
2033 |
@{code Le} (@{code Sub} (num_of_term vs t1, num_of_term vs t2)) |
|
2034 |
| fm_of_term ps vs (@{term "op = :: int \<Rightarrow> int \<Rightarrow> bool"} $ t1 $ t2) = |
|
50313 | 2035 |
@{code Eq} (@{code Sub} (num_of_term vs t1, num_of_term vs t2)) |
27456 | 2036 |
| fm_of_term ps vs (@{term "op dvd :: int \<Rightarrow> int \<Rightarrow> bool"} $ t1 $ t2) = |
2037 |
(case try HOLogic.dest_number t1 |
|
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
50313
diff
changeset
|
2038 |
of SOME (_, i) => @{code Dvd} (@{code int_of_integer} i, num_of_term vs t2) |
27456 | 2039 |
| NONE => error "num_of_term: unsupported dvd") |
2040 |
| fm_of_term ps vs (@{term "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ t1 $ t2) = |
|
2041 |
@{code Iff} (fm_of_term ps vs t1, fm_of_term ps vs t2) |
|
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset
|
2042 |
| fm_of_term ps vs (@{term HOL.conj} $ t1 $ t2) = |
27456 | 2043 |
@{code And} (fm_of_term ps vs t1, fm_of_term ps vs t2) |
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset
|
2044 |
| fm_of_term ps vs (@{term HOL.disj} $ t1 $ t2) = |
27456 | 2045 |
@{code Or} (fm_of_term ps vs t1, fm_of_term ps vs t2) |
38786
e46e7a9cb622
formerly unnamed infix impliciation now named HOL.implies
haftmann
parents:
38558
diff
changeset
|
2046 |
| fm_of_term ps vs (@{term HOL.implies} $ t1 $ t2) = |
27456 | 2047 |
@{code Imp} (fm_of_term ps vs t1, fm_of_term ps vs t2) |
2048 |
| fm_of_term ps vs (@{term "Not"} $ t') = |
|
2049 |
@{code NOT} (fm_of_term ps vs t') |
|
38558 | 2050 |
| fm_of_term ps vs (Const (@{const_name Ex}, _) $ Abs (xn, xT, p)) = |
27456 | 2051 |
let |
42284 | 2052 |
val (xn', p') = Syntax_Trans.variant_abs (xn, xT, p); (* FIXME !? *) |
27456 | 2053 |
val vs' = (Free (xn', xT), 0) :: map (fn (v, n) => (v, n + 1)) vs; |
2054 |
in @{code E} (fm_of_term ps vs' p) end |
|
38558 | 2055 |
| fm_of_term ps vs (Const (@{const_name All}, _) $ Abs (xn, xT, p)) = |
27456 | 2056 |
let |
42284 | 2057 |
val (xn', p') = Syntax_Trans.variant_abs (xn, xT, p); (* FIXME !? *) |
27456 | 2058 |
val vs' = (Free (xn', xT), 0) :: map (fn (v, n) => (v, n + 1)) vs; |
2059 |
in @{code A} (fm_of_term ps vs' p) end |
|
28264 | 2060 |
| fm_of_term ps vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term @{context} t); |
23515 | 2061 |
|
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
50313
diff
changeset
|
2062 |
fun term_of_num vs (@{code C} i) = HOLogic.mk_number HOLogic.intT (@{code integer_of_int} i) |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
50313
diff
changeset
|
2063 |
| term_of_num vs (@{code Bound} n) = |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
50313
diff
changeset
|
2064 |
let |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
50313
diff
changeset
|
2065 |
val q = @{code integer_of_nat} n |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
50313
diff
changeset
|
2066 |
in fst (the (find_first (fn (_, m) => q = m) vs)) end |
27456 | 2067 |
| term_of_num vs (@{code Neg} t') = @{term "uminus :: int \<Rightarrow> int"} $ term_of_num vs t' |
2068 |
| term_of_num vs (@{code Add} (t1, t2)) = @{term "op + :: int \<Rightarrow> int \<Rightarrow> int"} $ |
|
2069 |
term_of_num vs t1 $ term_of_num vs t2 |
|
2070 |
| term_of_num vs (@{code Sub} (t1, t2)) = @{term "op - :: int \<Rightarrow> int \<Rightarrow> int"} $ |
|
2071 |
term_of_num vs t1 $ term_of_num vs t2 |
|
2072 |
| term_of_num vs (@{code Mul} (i, t2)) = @{term "op * :: int \<Rightarrow> int \<Rightarrow> int"} $ |
|
2073 |
term_of_num vs (@{code C} i) $ term_of_num vs t2 |
|
29788 | 2074 |
| term_of_num vs (@{code CN} (n, i, t)) = term_of_num vs (@{code Add} (@{code Mul} (i, @{code Bound} n), t)); |
27456 | 2075 |
|
50313 | 2076 |
fun term_of_fm ps vs @{code T} = @{term True} |
45740 | 2077 |
| term_of_fm ps vs @{code F} = @{term False} |
27456 | 2078 |
| term_of_fm ps vs (@{code Lt} t) = |
2079 |
@{term "op < :: int \<Rightarrow> int \<Rightarrow> bool"} $ term_of_num vs t $ @{term "0::int"} |
|
2080 |
| term_of_fm ps vs (@{code Le} t) = |
|
2081 |
@{term "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"} $ term_of_num vs t $ @{term "0::int"} |
|
2082 |
| term_of_fm ps vs (@{code Gt} t) = |
|
2083 |
@{term "op < :: int \<Rightarrow> int \<Rightarrow> bool"} $ @{term "0::int"} $ term_of_num vs t |
|
2084 |
| term_of_fm ps vs (@{code Ge} t) = |
|
2085 |
@{term "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"} $ @{term "0::int"} $ term_of_num vs t |
|
2086 |
| term_of_fm ps vs (@{code Eq} t) = |
|
2087 |
@{term "op = :: int \<Rightarrow> int \<Rightarrow> bool"} $ term_of_num vs t $ @{term "0::int"} |
|
2088 |
| term_of_fm ps vs (@{code NEq} t) = |
|
2089 |
term_of_fm ps vs (@{code NOT} (@{code Eq} t)) |
|
2090 |
| term_of_fm ps vs (@{code Dvd} (i, t)) = |
|
2091 |
@{term "op dvd :: int \<Rightarrow> int \<Rightarrow> bool"} $ term_of_num vs (@{code C} i) $ term_of_num vs t |
|
2092 |
| term_of_fm ps vs (@{code NDvd} (i, t)) = |
|
2093 |
term_of_fm ps vs (@{code NOT} (@{code Dvd} (i, t))) |
|
2094 |
| term_of_fm ps vs (@{code NOT} t') = |
|
2095 |
HOLogic.Not $ term_of_fm ps vs t' |
|
2096 |
| term_of_fm ps vs (@{code And} (t1, t2)) = |
|
2097 |
HOLogic.conj $ term_of_fm ps vs t1 $ term_of_fm ps vs t2 |
|
2098 |
| term_of_fm ps vs (@{code Or} (t1, t2)) = |
|
2099 |
HOLogic.disj $ term_of_fm ps vs t1 $ term_of_fm ps vs t2 |
|
2100 |
| term_of_fm ps vs (@{code Imp} (t1, t2)) = |
|
2101 |
HOLogic.imp $ term_of_fm ps vs t1 $ term_of_fm ps vs t2 |
|
2102 |
| term_of_fm ps vs (@{code Iff} (t1, t2)) = |
|
2103 |
@{term "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ term_of_fm ps vs t1 $ term_of_fm ps vs t2 |
|
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
50313
diff
changeset
|
2104 |
| term_of_fm ps vs (@{code Closed} n) = |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
50313
diff
changeset
|
2105 |
let |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
50313
diff
changeset
|
2106 |
val q = @{code integer_of_nat} n |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
50313
diff
changeset
|
2107 |
in (fst o the) (find_first (fn (_, m) => m = q) ps) end |
29788 | 2108 |
| term_of_fm ps vs (@{code NClosed} n) = term_of_fm ps vs (@{code NOT} (@{code Closed} n)); |
27456 | 2109 |
|
2110 |
fun term_bools acc t = |
|
2111 |
let |
|
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset
|
2112 |
val is_op = member (op =) [@{term HOL.conj}, @{term HOL.disj}, @{term HOL.implies}, @{term "op = :: bool => _"}, |
27456 | 2113 |
@{term "op = :: int => _"}, @{term "op < :: int => _"}, |
2114 |
@{term "op <= :: int => _"}, @{term "Not"}, @{term "All :: (int => _) => _"}, |
|
2115 |
@{term "Ex :: (int => _) => _"}, @{term "True"}, @{term "False"}] |
|
50313 | 2116 |
fun is_ty t = not (fastype_of t = HOLogic.boolT) |
27456 | 2117 |
in case t |
50313 | 2118 |
of (l as f $ a) $ b => if is_ty t orelse is_op t then term_bools (term_bools acc l)b |
27456 | 2119 |
else insert (op aconv) t acc |
50313 | 2120 |
| f $ a => if is_ty t orelse is_op t then term_bools (term_bools acc f) a |
27456 | 2121 |
else insert (op aconv) t acc |
42284 | 2122 |
| Abs p => term_bools acc (snd (Syntax_Trans.variant_abs p)) (* FIXME !? *) |
27456 | 2123 |
| _ => if is_ty t orelse is_op t then acc else insert (op aconv) t acc |
2124 |
end; |
|
2125 |
||
28290 | 2126 |
in fn ct => |
2127 |
let |
|
2128 |
val thy = Thm.theory_of_cterm ct; |
|
2129 |
val t = Thm.term_of ct; |
|
44121 | 2130 |
val fs = Misc_Legacy.term_frees t; |
27456 | 2131 |
val bs = term_bools [] t; |
33063 | 2132 |
val vs = map_index swap fs; |
2133 |
val ps = map_index swap bs; |
|
27456 | 2134 |
val t' = (term_of_fm ps vs o @{code pa} o fm_of_term ps vs) t; |
28290 | 2135 |
in (Thm.cterm_of thy o HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end |
27456 | 2136 |
end; |
2137 |
*} |
|
2138 |
||
48891 | 2139 |
ML_file "cooper_tac.ML" |
47432 | 2140 |
|
2141 |
method_setup cooper = {* |
|
53168 | 2142 |
Scan.lift (Args.mode "no_quantify") >> |
47432 | 2143 |
(fn q => fn ctxt => SIMPLE_METHOD' (Cooper_Tac.linz_tac ctxt (not q))) |
2144 |
*} "decision procedure for linear integer arithmetic" |
|
2145 |
||
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
|
2146 |
|
27456 | 2147 |
text {* Tests *} |
2148 |
||
50313 | 2149 |
lemma "\<exists>(j::int). \<forall>x\<ge>j. (\<exists>a b. x = 3*a+5*b)" |
27456 | 2150 |
by cooper |
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
|
2151 |
|
27456 | 2152 |
lemma "ALL (x::int) >=8. EX i j. 5*i + 3*j = x" |
2153 |
by cooper |
|
2154 |
||
23274 | 2155 |
theorem "(\<forall>(y::int). 3 dvd y) ==> \<forall>(x::int). b < x --> a \<le> x" |
2156 |
by cooper |
|
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
|
2157 |
|
23274 | 2158 |
theorem "!! (y::int) (z::int) (n::int). 3 dvd z ==> 2 dvd (y::int) ==> |
2159 |
(\<exists>(x::int). 2*x = y) & (\<exists>(k::int). 3*k = z)" |
|
2160 |
by cooper |
|
2161 |
||
2162 |
theorem "!! (y::int) (z::int) n. Suc(n::nat) < 6 ==> 3 dvd z ==> |
|
2163 |
2 dvd (y::int) ==> (\<exists>(x::int). 2*x = y) & (\<exists>(k::int). 3*k = z)" |
|
2164 |
by cooper |
|
2165 |
||
2166 |
theorem "\<forall>(x::nat). \<exists>(y::nat). (0::nat) \<le> 5 --> y = 5 + x " |
|
2167 |
by cooper |
|
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
|
2168 |
|
27456 | 2169 |
lemma "ALL (x::int) >=8. EX i j. 5*i + 3*j = x" |
50313 | 2170 |
by cooper |
27456 | 2171 |
|
2172 |
lemma "ALL (y::int) (z::int) (n::int). 3 dvd z --> 2 dvd (y::int) --> (EX (x::int). 2*x = y) & (EX (k::int). 3*k = z)" |
|
2173 |
by cooper |
|
2174 |
||
2175 |
lemma "ALL(x::int) y. x < y --> 2 * x + 1 < 2 * y" |
|
2176 |
by cooper |
|
2177 |
||
2178 |
lemma "ALL(x::int) y. 2 * x + 1 ~= 2 * y" |
|
2179 |
by cooper |
|
2180 |
||
2181 |
lemma "EX(x::int) y. 0 < x & 0 <= y & 3 * x - 5 * y = 1" |
|
2182 |
by cooper |
|
2183 |
||
2184 |
lemma "~ (EX(x::int) (y::int) (z::int). 4*x + (-6::int)*y = 1)" |
|
2185 |
by cooper |
|
2186 |
||
2187 |
lemma "ALL(x::int). (2 dvd x) --> (EX(y::int). x = 2*y)" |
|
2188 |
by cooper |
|
2189 |
||
2190 |
lemma "ALL(x::int). (2 dvd x) = (EX(y::int). x = 2*y)" |
|
2191 |
by cooper |
|
2192 |
||
2193 |
lemma "ALL(x::int). ((2 dvd x) = (ALL(y::int). x ~= 2*y + 1))" |
|
2194 |
by cooper |
|
2195 |
||
2196 |
lemma "~ (ALL(x::int). ((2 dvd x) = (ALL(y::int). x ~= 2*y+1) | (EX(q::int) (u::int) i. 3*i + 2*q - u < 17) --> 0 < x | ((~ 3 dvd x) &(x + 8 = 0))))" |
|
2197 |
by cooper |
|
2198 |
||
50313 | 2199 |
lemma "~ (ALL(i::int). 4 <= i --> (EX x y. 0 <= x & 0 <= y & 3 * x + 5 * y = i))" |
23274 | 2200 |
by cooper |
27456 | 2201 |
|
2202 |
lemma "EX j. ALL (x::int) >= j. EX i j. 5*i + 3*j = x" |
|
2203 |
by cooper |
|
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
|
2204 |
|
23274 | 2205 |
theorem "(\<forall>(y::int). 3 dvd y) ==> \<forall>(x::int). b < x --> a \<le> x" |
2206 |
by cooper |
|
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
|
2207 |
|
23274 | 2208 |
theorem "!! (y::int) (z::int) (n::int). 3 dvd z ==> 2 dvd (y::int) ==> |
2209 |
(\<exists>(x::int). 2*x = y) & (\<exists>(k::int). 3*k = z)" |
|
2210 |
by cooper |
|
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
|
2211 |
|
23274 | 2212 |
theorem "!! (y::int) (z::int) n. Suc(n::nat) < 6 ==> 3 dvd z ==> |
2213 |
2 dvd (y::int) ==> (\<exists>(x::int). 2*x = y) & (\<exists>(k::int). 3*k = z)" |
|
2214 |
by cooper |
|
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
|
2215 |
|
23274 | 2216 |
theorem "\<forall>(x::nat). \<exists>(y::nat). (0::nat) \<le> 5 --> y = 5 + x " |
2217 |
by cooper |
|
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
|
2218 |
|
23274 | 2219 |
theorem "\<forall>(x::nat). \<exists>(y::nat). y = 5 + x | x div 6 + 1= 2" |
2220 |
by cooper |
|
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
|
2221 |
|
23274 | 2222 |
theorem "\<exists>(x::int). 0 < x" |
2223 |
by cooper |
|
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
|
2224 |
|
23274 | 2225 |
theorem "\<forall>(x::int) y. x < y --> 2 * x + 1 < 2 * y" |
2226 |
by cooper |
|
50313 | 2227 |
|
23274 | 2228 |
theorem "\<forall>(x::int) y. 2 * x + 1 \<noteq> 2 * y" |
2229 |
by cooper |
|
50313 | 2230 |
|
23274 | 2231 |
theorem "\<exists>(x::int) y. 0 < x & 0 \<le> y & 3 * x - 5 * y = 1" |
2232 |
by cooper |
|
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
|
2233 |
|
23274 | 2234 |
theorem "~ (\<exists>(x::int) (y::int) (z::int). 4*x + (-6::int)*y = 1)" |
2235 |
by cooper |
|
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
|
2236 |
|
23274 | 2237 |
theorem "~ (\<exists>(x::int). False)" |
2238 |
by cooper |
|
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
|
2239 |
|
23274 | 2240 |
theorem "\<forall>(x::int). (2 dvd x) --> (\<exists>(y::int). x = 2*y)" |
50313 | 2241 |
by cooper |
23274 | 2242 |
|
2243 |
theorem "\<forall>(x::int). (2 dvd x) --> (\<exists>(y::int). x = 2*y)" |
|
50313 | 2244 |
by cooper |
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
|
2245 |
|
23274 | 2246 |
theorem "\<forall>(x::int). (2 dvd x) = (\<exists>(y::int). x = 2*y)" |
50313 | 2247 |
by cooper |
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
|
2248 |
|
23274 | 2249 |
theorem "\<forall>(x::int). ((2 dvd x) = (\<forall>(y::int). x \<noteq> 2*y + 1))" |
50313 | 2250 |
by cooper |
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
|
2251 |
|
50313 | 2252 |
theorem "~ (\<forall>(x::int). |
2253 |
((2 dvd x) = (\<forall>(y::int). x \<noteq> 2*y+1) | |
|
23274 | 2254 |
(\<exists>(q::int) (u::int) i. 3*i + 2*q - u < 17) |
2255 |
--> 0 < x | ((~ 3 dvd x) &(x + 8 = 0))))" |
|
2256 |
by cooper |
|
50313 | 2257 |
|
23274 | 2258 |
theorem "~ (\<forall>(i::int). 4 \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i))" |
2259 |
by cooper |
|
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
|
2260 |
|
23274 | 2261 |
theorem "\<forall>(i::int). 8 \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i)" |
2262 |
by cooper |
|
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
|
2263 |
|
23274 | 2264 |
theorem "\<exists>(j::int). \<forall>i. j \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i)" |
2265 |
by cooper |
|
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
|
2266 |
|
23274 | 2267 |
theorem "~ (\<forall>j (i::int). j \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i))" |
2268 |
by cooper |
|
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
|
2269 |
|
23274 | 2270 |
theorem "(\<exists>m::nat. n = 2 * m) --> (n + 1) div 2 = n div 2" |
2271 |
by cooper |
|
17388 | 2272 |
|
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
|
2273 |
end |