author  hoelzl 
Wed, 11 Mar 2009 10:58:18 +0100  
changeset 30439  57c68b3af2ea 
parent 30042  31039ee583fa 
child 31715  2eb55a82acd9 
permissions  rwrr 
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 (ji+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 (iaib, 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(34) 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</ 