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