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