src/HOL/Decision_Procs/Cooper.thy
 author blanchet Thu Sep 11 18:54:36 2014 +0200 (2014-09-11) changeset 58306 117ba6cbe414 parent 58259 52c35a59bbf5 child 58310 91ea607a34d8 permissions -rw-r--r--
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
1 (*  Title:      HOL/Decision_Procs/Cooper.thy
2     Author:     Amine Chaieb
3 *)
5 theory Cooper
6 imports
7   Complex_Main
8   "~~/src/HOL/Library/Code_Target_Numeral"
9   "~~/src/HOL/Library/Old_Recdef"
10 begin
12 (* Periodicity of dvd *)
14 (*********************************************************************************)
15 (****                            SHADOW SYNTAX AND SEMANTICS                  ****)
16 (*********************************************************************************)
18 datatype_new num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num
19   | Mul int num
21 primrec num_size :: "num \<Rightarrow> nat" -- {* A size for num to make inductive proofs simpler *}
22 where
23   "num_size (C c) = 1"
24 | "num_size (Bound n) = 1"
25 | "num_size (Neg a) = 1 + num_size a"
26 | "num_size (Add a b) = 1 + num_size a + num_size b"
27 | "num_size (Sub a b) = 3 + num_size a + num_size b"
28 | "num_size (CN n c a) = 4 + num_size a"
29 | "num_size (Mul c a) = 1 + num_size a"
31 primrec Inum :: "int list \<Rightarrow> num \<Rightarrow> int"
32 where
33   "Inum bs (C c) = c"
34 | "Inum bs (Bound n) = bs!n"
35 | "Inum bs (CN n c a) = c * (bs!n) + (Inum bs a)"
36 | "Inum bs (Neg a) = -(Inum bs a)"
37 | "Inum bs (Add a b) = Inum bs a + Inum bs b"
38 | "Inum bs (Sub a b) = Inum bs a - Inum bs b"
39 | "Inum bs (Mul c a) = c* Inum bs a"
41 datatype_new fm  =
42   T| F| Lt num| Le num| Gt num| Ge num| Eq num| NEq num| Dvd int num| NDvd int num|
43   NOT fm| And fm fm|  Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm
44   | Closed nat | NClosed nat
47 fun fmsize :: "fm \<Rightarrow> nat"  -- {* A size for fm *}
48 where
49   "fmsize (NOT p) = 1 + fmsize p"
50 | "fmsize (And p q) = 1 + fmsize p + fmsize q"
51 | "fmsize (Or p q) = 1 + fmsize p + fmsize q"
52 | "fmsize (Imp p q) = 3 + fmsize p + fmsize q"
53 | "fmsize (Iff p q) = 3 + 2*(fmsize p + fmsize q)"
54 | "fmsize (E p) = 1 + fmsize p"
55 | "fmsize (A p) = 4+ fmsize p"
56 | "fmsize (Dvd i t) = 2"
57 | "fmsize (NDvd i t) = 2"
58 | "fmsize p = 1"
60 lemma fmsize_pos: "fmsize p > 0"
61   by (induct p rule: fmsize.induct) simp_all
63 primrec Ifm :: "bool list \<Rightarrow> int list \<Rightarrow> fm \<Rightarrow> bool"  -- {* Semantics of formulae (fm) *}
64 where
65   "Ifm bbs bs T \<longleftrightarrow> True"
66 | "Ifm bbs bs F \<longleftrightarrow> False"
67 | "Ifm bbs bs (Lt a) \<longleftrightarrow> Inum bs a < 0"
68 | "Ifm bbs bs (Gt a) \<longleftrightarrow> Inum bs a > 0"
69 | "Ifm bbs bs (Le a) \<longleftrightarrow> Inum bs a \<le> 0"
70 | "Ifm bbs bs (Ge a) \<longleftrightarrow> Inum bs a \<ge> 0"
71 | "Ifm bbs bs (Eq a) \<longleftrightarrow> Inum bs a = 0"
72 | "Ifm bbs bs (NEq a) \<longleftrightarrow> Inum bs a \<noteq> 0"
73 | "Ifm bbs bs (Dvd i b) \<longleftrightarrow> i dvd Inum bs b"
74 | "Ifm bbs bs (NDvd i b) \<longleftrightarrow> \<not> i dvd Inum bs b"
75 | "Ifm bbs bs (NOT p) \<longleftrightarrow> \<not> Ifm bbs bs p"
76 | "Ifm bbs bs (And p q) \<longleftrightarrow> Ifm bbs bs p \<and> Ifm bbs bs q"
77 | "Ifm bbs bs (Or p q) \<longleftrightarrow> Ifm bbs bs p \<or> Ifm bbs bs q"
78 | "Ifm bbs bs (Imp p q) \<longleftrightarrow> (Ifm bbs bs p \<longrightarrow> Ifm bbs bs q)"
79 | "Ifm bbs bs (Iff p q) \<longleftrightarrow> Ifm bbs bs p = Ifm bbs bs q"
80 | "Ifm bbs bs (E p) \<longleftrightarrow> (\<exists>x. Ifm bbs (x # bs) p)"
81 | "Ifm bbs bs (A p) \<longleftrightarrow> (\<forall>x. Ifm bbs (x # bs) p)"
82 | "Ifm bbs bs (Closed n) \<longleftrightarrow> bbs!n"
83 | "Ifm bbs bs (NClosed n) \<longleftrightarrow> \<not> bbs!n"
85 consts prep :: "fm \<Rightarrow> fm"
86 recdef prep "measure fmsize"
87   "prep (E T) = T"
88   "prep (E F) = F"
89   "prep (E (Or p q)) = Or (prep (E p)) (prep (E q))"
90   "prep (E (Imp p q)) = Or (prep (E (NOT p))) (prep (E q))"
91   "prep (E (Iff p q)) = Or (prep (E (And p q))) (prep (E (And (NOT p) (NOT q))))"
92   "prep (E (NOT (And p q))) = Or (prep (E (NOT p))) (prep (E(NOT q)))"
93   "prep (E (NOT (Imp p q))) = prep (E (And p (NOT q)))"
94   "prep (E (NOT (Iff p q))) = Or (prep (E (And p (NOT q)))) (prep (E(And (NOT p) q)))"
95   "prep (E p) = E (prep p)"
96   "prep (A (And p q)) = And (prep (A p)) (prep (A q))"
97   "prep (A p) = prep (NOT (E (NOT p)))"
98   "prep (NOT (NOT p)) = prep p"
99   "prep (NOT (And p q)) = Or (prep (NOT p)) (prep (NOT q))"
100   "prep (NOT (A p)) = prep (E (NOT p))"
101   "prep (NOT (Or p q)) = And (prep (NOT p)) (prep (NOT q))"
102   "prep (NOT (Imp p q)) = And (prep p) (prep (NOT q))"
103   "prep (NOT (Iff p q)) = Or (prep (And p (NOT q))) (prep (And (NOT p) q))"
104   "prep (NOT p) = NOT (prep p)"
105   "prep (Or p q) = Or (prep p) (prep q)"
106   "prep (And p q) = And (prep p) (prep q)"
107   "prep (Imp p q) = prep (Or (NOT p) q)"
108   "prep (Iff p q) = Or (prep (And p q)) (prep (And (NOT p) (NOT q)))"
109   "prep p = p"
110   (hints simp add: fmsize_pos)
112 lemma prep: "Ifm bbs bs (prep p) = Ifm bbs bs p"
113   by (induct p arbitrary: bs rule: prep.induct) auto
116 fun qfree :: "fm \<Rightarrow> bool"  -- {* Quantifier freeness *}
117 where
118   "qfree (E p) \<longleftrightarrow> False"
119 | "qfree (A p) \<longleftrightarrow> False"
120 | "qfree (NOT p) \<longleftrightarrow> qfree p"
121 | "qfree (And p q) \<longleftrightarrow> qfree p \<and> qfree q"
122 | "qfree (Or  p q) \<longleftrightarrow> qfree p \<and> qfree q"
123 | "qfree (Imp p q) \<longleftrightarrow> qfree p \<and> qfree q"
124 | "qfree (Iff p q) \<longleftrightarrow> qfree p \<and> qfree q"
125 | "qfree p \<longleftrightarrow> True"
128 text {* Boundedness and substitution *}
130 primrec numbound0 :: "num \<Rightarrow> bool"  -- {* a num is INDEPENDENT of Bound 0 *}
131 where
132   "numbound0 (C c) \<longleftrightarrow> True"
133 | "numbound0 (Bound n) \<longleftrightarrow> n > 0"
134 | "numbound0 (CN n i a) \<longleftrightarrow> n > 0 \<and> numbound0 a"
135 | "numbound0 (Neg a) \<longleftrightarrow> numbound0 a"
136 | "numbound0 (Add a b) \<longleftrightarrow> numbound0 a \<and> numbound0 b"
137 | "numbound0 (Sub a b) \<longleftrightarrow> numbound0 a \<and> numbound0 b"
138 | "numbound0 (Mul i a) \<longleftrightarrow> numbound0 a"
140 lemma numbound0_I:
141   assumes nb: "numbound0 a"
142   shows "Inum (b # bs) a = Inum (b' # bs) a"
143   using nb by (induct a rule: num.induct) (auto simp add: gr0_conv_Suc)
145 primrec bound0 :: "fm \<Rightarrow> bool" -- {* A Formula is independent of Bound 0 *}
146 where
147   "bound0 T \<longleftrightarrow> True"
148 | "bound0 F \<longleftrightarrow> True"
149 | "bound0 (Lt a) \<longleftrightarrow> numbound0 a"
150 | "bound0 (Le a) \<longleftrightarrow> numbound0 a"
151 | "bound0 (Gt a) \<longleftrightarrow> numbound0 a"
152 | "bound0 (Ge a) \<longleftrightarrow> numbound0 a"
153 | "bound0 (Eq a) \<longleftrightarrow> numbound0 a"
154 | "bound0 (NEq a) \<longleftrightarrow> numbound0 a"
155 | "bound0 (Dvd i a) \<longleftrightarrow> numbound0 a"
156 | "bound0 (NDvd i a) \<longleftrightarrow> numbound0 a"
157 | "bound0 (NOT p) \<longleftrightarrow> bound0 p"
158 | "bound0 (And p q) \<longleftrightarrow> bound0 p \<and> bound0 q"
159 | "bound0 (Or p q) \<longleftrightarrow> bound0 p \<and> bound0 q"
160 | "bound0 (Imp p q) \<longleftrightarrow> bound0 p \<and> bound0 q"
161 | "bound0 (Iff p q) \<longleftrightarrow> bound0 p \<and> bound0 q"
162 | "bound0 (E p) \<longleftrightarrow> False"
163 | "bound0 (A p) \<longleftrightarrow> False"
164 | "bound0 (Closed P) \<longleftrightarrow> True"
165 | "bound0 (NClosed P) \<longleftrightarrow> True"
167 lemma bound0_I:
168   assumes bp: "bound0 p"
169   shows "Ifm bbs (b # bs) p = Ifm bbs (b' # bs) p"
170   using bp numbound0_I[where b="b" and bs="bs" and b'="b'"]
171   by (induct p rule: fm.induct) (auto simp add: gr0_conv_Suc)
173 fun numsubst0 :: "num \<Rightarrow> num \<Rightarrow> num"
174 where
175   "numsubst0 t (C c) = (C c)"
176 | "numsubst0 t (Bound n) = (if n=0 then t else Bound n)"
177 | "numsubst0 t (CN 0 i a) = Add (Mul i t) (numsubst0 t a)"
178 | "numsubst0 t (CN n i a) = CN n i (numsubst0 t a)"
179 | "numsubst0 t (Neg a) = Neg (numsubst0 t a)"
180 | "numsubst0 t (Add a b) = Add (numsubst0 t a) (numsubst0 t b)"
181 | "numsubst0 t (Sub a b) = Sub (numsubst0 t a) (numsubst0 t b)"
182 | "numsubst0 t (Mul i a) = Mul i (numsubst0 t a)"
184 lemma numsubst0_I: "Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b#bs) a)#bs) t"
185   by (induct t rule: numsubst0.induct) (auto simp: nth_Cons')
187 lemma numsubst0_I':
188   "numbound0 a \<Longrightarrow> Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b'#bs) a)#bs) t"
189   by (induct t rule: numsubst0.induct) (auto simp: nth_Cons' numbound0_I[where b="b" and b'="b'"])
191 primrec subst0:: "num \<Rightarrow> fm \<Rightarrow> fm"  -- {* substitue a num into a formula for Bound 0 *}
192 where
193   "subst0 t T = T"
194 | "subst0 t F = F"
195 | "subst0 t (Lt a) = Lt (numsubst0 t a)"
196 | "subst0 t (Le a) = Le (numsubst0 t a)"
197 | "subst0 t (Gt a) = Gt (numsubst0 t a)"
198 | "subst0 t (Ge a) = Ge (numsubst0 t a)"
199 | "subst0 t (Eq a) = Eq (numsubst0 t a)"
200 | "subst0 t (NEq a) = NEq (numsubst0 t a)"
201 | "subst0 t (Dvd i a) = Dvd i (numsubst0 t a)"
202 | "subst0 t (NDvd i a) = NDvd i (numsubst0 t a)"
203 | "subst0 t (NOT p) = NOT (subst0 t p)"
204 | "subst0 t (And p q) = And (subst0 t p) (subst0 t q)"
205 | "subst0 t (Or p q) = Or (subst0 t p) (subst0 t q)"
206 | "subst0 t (Imp p q) = Imp (subst0 t p) (subst0 t q)"
207 | "subst0 t (Iff p q) = Iff (subst0 t p) (subst0 t q)"
208 | "subst0 t (Closed P) = (Closed P)"
209 | "subst0 t (NClosed P) = (NClosed P)"
211 lemma subst0_I:
212   assumes "qfree p"
213   shows "Ifm bbs (b # bs) (subst0 a p) = Ifm bbs (Inum (b # bs) a # bs) p"
214   using assms numsubst0_I[where b="b" and bs="bs" and a="a"]
215   by (induct p) (simp_all add: gr0_conv_Suc)
217 fun decrnum:: "num \<Rightarrow> num"
218 where
219   "decrnum (Bound n) = Bound (n - 1)"
220 | "decrnum (Neg a) = Neg (decrnum a)"
221 | "decrnum (Add a b) = Add (decrnum a) (decrnum b)"
222 | "decrnum (Sub a b) = Sub (decrnum a) (decrnum b)"
223 | "decrnum (Mul c a) = Mul c (decrnum a)"
224 | "decrnum (CN n i a) = (CN (n - 1) i (decrnum a))"
225 | "decrnum a = a"
227 fun decr :: "fm \<Rightarrow> fm"
228 where
229   "decr (Lt a) = Lt (decrnum a)"
230 | "decr (Le a) = Le (decrnum a)"
231 | "decr (Gt a) = Gt (decrnum a)"
232 | "decr (Ge a) = Ge (decrnum a)"
233 | "decr (Eq a) = Eq (decrnum a)"
234 | "decr (NEq a) = NEq (decrnum a)"
235 | "decr (Dvd i a) = Dvd i (decrnum a)"
236 | "decr (NDvd i a) = NDvd i (decrnum a)"
237 | "decr (NOT p) = NOT (decr p)"
238 | "decr (And p q) = And (decr p) (decr q)"
239 | "decr (Or p q) = Or (decr p) (decr q)"
240 | "decr (Imp p q) = Imp (decr p) (decr q)"
241 | "decr (Iff p q) = Iff (decr p) (decr q)"
242 | "decr p = p"
244 lemma decrnum:
245   assumes nb: "numbound0 t"
246   shows "Inum (x # bs) t = Inum bs (decrnum t)"
247   using nb by (induct t rule: decrnum.induct) (auto simp add: gr0_conv_Suc)
249 lemma decr:
250   assumes nb: "bound0 p"
251   shows "Ifm bbs (x # bs) p = Ifm bbs bs (decr p)"
252   using nb by (induct p rule: decr.induct) (simp_all add: gr0_conv_Suc decrnum)
254 lemma decr_qf: "bound0 p \<Longrightarrow> qfree (decr p)"
255   by (induct p) simp_all
257 fun isatom :: "fm \<Rightarrow> bool"  -- {* test for atomicity *}
258 where
259   "isatom T \<longleftrightarrow> True"
260 | "isatom F \<longleftrightarrow> True"
261 | "isatom (Lt a) \<longleftrightarrow> True"
262 | "isatom (Le a) \<longleftrightarrow> True"
263 | "isatom (Gt a) \<longleftrightarrow> True"
264 | "isatom (Ge a) \<longleftrightarrow> True"
265 | "isatom (Eq a) \<longleftrightarrow> True"
266 | "isatom (NEq a) \<longleftrightarrow> True"
267 | "isatom (Dvd i b) \<longleftrightarrow> True"
268 | "isatom (NDvd i b) \<longleftrightarrow> True"
269 | "isatom (Closed P) \<longleftrightarrow> True"
270 | "isatom (NClosed P) \<longleftrightarrow> True"
271 | "isatom p \<longleftrightarrow> False"
273 lemma numsubst0_numbound0:
274   assumes "numbound0 t"
275   shows "numbound0 (numsubst0 t a)"
276   using assms
277   apply (induct a)
278   apply simp_all
279   apply (rename_tac nat a b, case_tac nat)
280   apply simp_all
281   done
283 lemma subst0_bound0:
284   assumes qf: "qfree p"
285     and nb: "numbound0 t"
286   shows "bound0 (subst0 t p)"
287   using qf numsubst0_numbound0[OF nb] by (induct p) auto
289 lemma bound0_qf: "bound0 p \<Longrightarrow> qfree p"
290   by (induct p) simp_all
293 definition djf :: "('a \<Rightarrow> fm) \<Rightarrow> 'a \<Rightarrow> fm \<Rightarrow> fm"
294 where
295   "djf f p q =
296    (if q = T then T
297     else if q = F then f p
298     else
299       let fp = f p
300       in case fp of T \<Rightarrow> T | F \<Rightarrow> q | _ \<Rightarrow> Or (f p) q)"
302 definition evaldjf :: "('a \<Rightarrow> fm) \<Rightarrow> 'a list \<Rightarrow> fm"
303   where "evaldjf f ps = foldr (djf f) ps F"
305 lemma djf_Or: "Ifm bbs bs (djf f p q) = Ifm bbs bs (Or (f p) q)"
306   by (cases "q=T", simp add: djf_def, cases "q = F", simp add: djf_def)
307     (cases "f p", simp_all add: Let_def djf_def)
309 lemma evaldjf_ex: "Ifm bbs bs (evaldjf f ps) \<longleftrightarrow> (\<exists>p \<in> set ps. Ifm bbs bs (f p))"
310   by (induct ps) (simp_all add: evaldjf_def djf_Or)
312 lemma evaldjf_bound0:
313   assumes nb: "\<forall>x\<in> set xs. bound0 (f x)"
314   shows "bound0 (evaldjf f xs)"
315   using nb by (induct xs) (auto simp add: evaldjf_def djf_def Let_def, case_tac "f a", auto)
317 lemma evaldjf_qf:
318   assumes nb: "\<forall>x\<in> set xs. qfree (f x)"
319   shows "qfree (evaldjf f xs)"
320   using nb by (induct xs) (auto simp add: evaldjf_def djf_def Let_def, case_tac "f a", auto)
322 fun disjuncts :: "fm \<Rightarrow> fm list"
323 where
324   "disjuncts (Or p q) = disjuncts p @ disjuncts q"
325 | "disjuncts F = []"
326 | "disjuncts p = [p]"
328 lemma disjuncts: "(\<exists>q \<in> set (disjuncts p). Ifm bbs bs q) \<longleftrightarrow> Ifm bbs bs p"
329   by (induct p rule: disjuncts.induct) auto
331 lemma disjuncts_nb:
332   assumes "bound0 p"
333   shows "\<forall>q \<in> set (disjuncts p). bound0 q"
334 proof -
335   from assms have "list_all bound0 (disjuncts p)"
336     by (induct p rule: disjuncts.induct) auto
337   then show ?thesis
338     by (simp only: list_all_iff)
339 qed
341 lemma disjuncts_qf:
342   assumes "qfree p"
343   shows "\<forall>q \<in> set (disjuncts p). qfree q"
344 proof -
345   from assms have "list_all qfree (disjuncts p)"
346     by (induct p rule: disjuncts.induct) auto
347   then show ?thesis by (simp only: list_all_iff)
348 qed
350 definition DJ :: "(fm \<Rightarrow> fm) \<Rightarrow> fm \<Rightarrow> fm"
351   where "DJ f p = evaldjf f (disjuncts p)"
353 lemma DJ:
354   assumes "\<forall>p q. f (Or p q) = Or (f p) (f q)"
355     and "f F = F"
356   shows "Ifm bbs bs (DJ f p) = Ifm bbs bs (f p)"
357 proof -
358   have "Ifm bbs bs (DJ f p) \<longleftrightarrow> (\<exists>q \<in> set (disjuncts p). Ifm bbs bs (f q))"
359     by (simp add: DJ_def evaldjf_ex)
360   also from assms have "\<dots> = Ifm bbs bs (f p)"
361     by (induct p rule: disjuncts.induct) auto
362   finally show ?thesis .
363 qed
365 lemma DJ_qf:
366   assumes "\<forall>p. qfree p \<longrightarrow> qfree (f p)"
367   shows "\<forall>p. qfree p \<longrightarrow> qfree (DJ f p) "
368 proof clarify
369   fix p
370   assume qf: "qfree p"
371   have th: "DJ f p = evaldjf f (disjuncts p)"
372     by (simp add: DJ_def)
373   from disjuncts_qf[OF qf] have "\<forall>q \<in> set (disjuncts p). qfree q" .
374   with assms have th': "\<forall>q \<in> set (disjuncts p). qfree (f q)"
375     by blast
376   from evaldjf_qf[OF th'] th show "qfree (DJ f p)"
377     by simp
378 qed
380 lemma DJ_qe:
381   assumes qe: "\<forall>bs p. qfree p \<longrightarrow> qfree (qe p) \<and> Ifm bbs bs (qe p) = Ifm bbs bs (E p)"
382   shows "\<forall>bs p. qfree p \<longrightarrow> qfree (DJ qe p) \<and> Ifm bbs bs ((DJ qe p)) = Ifm bbs bs (E p)"
383 proof clarify
384   fix p :: fm
385   fix bs
386   assume qf: "qfree p"
387   from qe have qth: "\<forall>p. qfree p \<longrightarrow> qfree (qe p)"
388     by blast
389   from DJ_qf[OF qth] qf have qfth: "qfree (DJ qe p)"
390     by auto
391   have "Ifm bbs bs (DJ qe p) = (\<exists>q\<in> set (disjuncts p). Ifm bbs bs (qe q))"
392     by (simp add: DJ_def evaldjf_ex)
393   also have "\<dots> \<longleftrightarrow> (\<exists>q \<in> set (disjuncts p). Ifm bbs bs (E q))"
394     using qe disjuncts_qf[OF qf] by auto
395   also have "\<dots> \<longleftrightarrow> Ifm bbs bs (E p)"
396     by (induct p rule: disjuncts.induct) auto
397   finally show "qfree (DJ qe p) \<and> Ifm bbs bs (DJ qe p) = Ifm bbs bs (E p)"
398     using qfth by blast
399 qed
402 text {* Simplification *}
404 text {* Algebraic simplifications for nums *}
406 fun bnds :: "num \<Rightarrow> nat list"
407 where
408   "bnds (Bound n) = [n]"
409 | "bnds (CN n c a) = n # bnds a"
410 | "bnds (Neg a) = bnds a"
411 | "bnds (Add a b) = bnds a @ bnds b"
412 | "bnds (Sub a b) = bnds a @ bnds b"
413 | "bnds (Mul i a) = bnds a"
414 | "bnds a = []"
416 fun lex_ns:: "nat list \<Rightarrow> nat list \<Rightarrow> bool"
417 where
418   "lex_ns [] ms \<longleftrightarrow> True"
419 | "lex_ns ns [] \<longleftrightarrow> False"
420 | "lex_ns (n # ns) (m # ms) \<longleftrightarrow> n < m \<or> (n = m \<and> lex_ns ns ms)"
422 definition lex_bnd :: "num \<Rightarrow> num \<Rightarrow> bool"
423   where "lex_bnd t s = lex_ns (bnds t) (bnds s)"
425 consts numadd:: "num \<times> num \<Rightarrow> num"
426 recdef numadd "measure (\<lambda>(t, s). num_size t + num_size s)"
427   "numadd (CN n1 c1 r1, CN n2 c2 r2) =
428     (if n1 = n2 then
429        let c = c1 + c2
430        in if c = 0 then numadd (r1, r2) else CN n1 c (numadd (r1, r2))
431      else if n1 \<le> n2 then CN n1 c1 (numadd (r1, Add (Mul c2 (Bound n2)) r2))
432      else CN n2 c2 (numadd (Add (Mul c1 (Bound n1)) r1, r2)))"
433   "numadd (CN n1 c1 r1, t) = CN n1 c1 (numadd (r1, t))"
434   "numadd (t, CN n2 c2 r2) = CN n2 c2 (numadd (t, r2))"
435   "numadd (C b1, C b2) = C (b1 + b2)"
436   "numadd (a, b) = Add a b"
438 (*function (sequential)
439   numadd :: "num \<Rightarrow> num \<Rightarrow> num"
440 where
441   "numadd (Add (Mul c1 (Bound n1)) r1) (Add (Mul c2 (Bound n2)) r2) =
442       (if n1 = n2 then (let c = c1 + c2
443       in (if c = 0 then numadd r1 r2 else
444         Add (Mul c (Bound n1)) (numadd r1 r2)))
445       else if n1 \<le> n2 then
446         Add (Mul c1 (Bound n1)) (numadd r1 (Add (Mul c2 (Bound n2)) r2))
447       else
448         Add (Mul c2 (Bound n2)) (numadd (Add (Mul c1 (Bound n1)) r1) r2))"
449   | "numadd (Add (Mul c1 (Bound n1)) r1) t =
450       Add (Mul c1 (Bound n1)) (numadd r1 t)"
451   | "numadd t (Add (Mul c2 (Bound n2)) r2) =
452       Add (Mul c2 (Bound n2)) (numadd t r2)"
453   | "numadd (C b1) (C b2) = C (b1 + b2)"
454   | "numadd a b = Add a b"
455 apply pat_completeness apply auto*)
457 lemma numadd: "Inum bs (numadd (t,s)) = Inum bs (Add t s)"
458   apply (induct t s rule: numadd.induct)
459   apply (simp_all add: Let_def)
460   apply (case_tac "c1 + c2 = 0")
461   apply (case_tac "n1 \<le> n2")
462   apply simp_all
463    apply (case_tac "n1 = n2")
464     apply (simp_all add: algebra_simps)
465   apply (simp add: distrib_right[symmetric])
466   done
468 lemma numadd_nb: "numbound0 t \<Longrightarrow> numbound0 s \<Longrightarrow> numbound0 (numadd (t, s))"
469   by (induct t s rule: numadd.induct) (auto simp add: Let_def)
471 fun nummul :: "int \<Rightarrow> num \<Rightarrow> num"
472 where
473   "nummul i (C j) = C (i * j)"
474 | "nummul i (CN n c t) = CN n (c * i) (nummul i t)"
475 | "nummul i t = Mul i t"
477 lemma nummul: "Inum bs (nummul i t) = Inum bs (Mul i t)"
478   by (induct t arbitrary: i rule: nummul.induct) (auto simp add: algebra_simps numadd)
480 lemma nummul_nb: "numbound0 t \<Longrightarrow> numbound0 (nummul i t)"
481   by (induct t arbitrary: i rule: nummul.induct) (auto simp add: numadd_nb)
483 definition numneg :: "num \<Rightarrow> num"
484   where "numneg t = nummul (- 1) t"
486 definition numsub :: "num \<Rightarrow> num \<Rightarrow> num"
487   where "numsub s t = (if s = t then C 0 else numadd (s, numneg t))"
489 lemma numneg: "Inum bs (numneg t) = Inum bs (Neg t)"
490   using numneg_def nummul by simp
492 lemma numneg_nb: "numbound0 t \<Longrightarrow> numbound0 (numneg t)"
493   using numneg_def nummul_nb by simp
495 lemma numsub: "Inum bs (numsub a b) = Inum bs (Sub a b)"
496   using numneg numadd numsub_def by simp
498 lemma numsub_nb: "numbound0 t \<Longrightarrow> numbound0 s \<Longrightarrow> numbound0 (numsub t s)"
499   using numsub_def numadd_nb numneg_nb by simp
501 fun simpnum :: "num \<Rightarrow> num"
502 where
503   "simpnum (C j) = C j"
504 | "simpnum (Bound n) = CN n 1 (C 0)"
505 | "simpnum (Neg t) = numneg (simpnum t)"
506 | "simpnum (Add t s) = numadd (simpnum t, simpnum s)"
507 | "simpnum (Sub t s) = numsub (simpnum t) (simpnum s)"
508 | "simpnum (Mul i t) = (if i = 0 then C 0 else nummul i (simpnum t))"
509 | "simpnum t = t"
511 lemma simpnum_ci: "Inum bs (simpnum t) = Inum bs t"
512   by (induct t rule: simpnum.induct) (auto simp add: numneg numadd numsub nummul)
514 lemma simpnum_numbound0: "numbound0 t \<Longrightarrow> numbound0 (simpnum t)"
515   by (induct t rule: simpnum.induct) (auto simp add: numadd_nb numsub_nb nummul_nb numneg_nb)
517 fun not :: "fm \<Rightarrow> fm"
518 where
519   "not (NOT p) = p"
520 | "not T = F"
521 | "not F = T"
522 | "not p = NOT p"
524 lemma not: "Ifm bbs bs (not p) = Ifm bbs bs (NOT p)"
525   by (cases p) auto
527 lemma not_qf: "qfree p \<Longrightarrow> qfree (not p)"
528   by (cases p) auto
530 lemma not_bn: "bound0 p \<Longrightarrow> bound0 (not p)"
531   by (cases p) auto
533 definition conj :: "fm \<Rightarrow> fm \<Rightarrow> fm"
534   where
535     "conj p q =
536       (if p = F \<or> q = F then F
537        else if p = T then q
538        else if q = T then p
539        else And p q)"
541 lemma conj: "Ifm bbs bs (conj p q) = Ifm bbs bs (And p q)"
542   by (cases "p = F \<or> q = F", simp_all add: conj_def) (cases p, simp_all)
544 lemma conj_qf: "qfree p \<Longrightarrow> qfree q \<Longrightarrow> qfree (conj p q)"
545   using conj_def by auto
547 lemma conj_nb: "bound0 p \<Longrightarrow> bound0 q \<Longrightarrow> bound0 (conj p q)"
548   using conj_def by auto
550 definition disj :: "fm \<Rightarrow> fm \<Rightarrow> fm"
551   where
552     "disj p q =
553       (if p = T \<or> q = T then T
554        else if p = F then q
555        else if q = F then p
556        else Or p q)"
558 lemma disj: "Ifm bbs bs (disj p q) = Ifm bbs bs (Or p q)"
559   by (cases "p = T \<or> q = T", simp_all add: disj_def) (cases p, simp_all)
561 lemma disj_qf: "qfree p \<Longrightarrow> qfree q \<Longrightarrow> qfree (disj p q)"
562   using disj_def by auto
564 lemma disj_nb: "bound0 p \<Longrightarrow> bound0 q \<Longrightarrow> bound0 (disj p q)"
565   using disj_def by auto
567 definition imp :: "fm \<Rightarrow> fm \<Rightarrow> fm"
568   where
569     "imp p q =
570       (if p = F \<or> q = T then T
571        else if p = T then q
572        else if q = F then not p
573        else Imp p q)"
575 lemma imp: "Ifm bbs bs (imp p q) = Ifm bbs bs (Imp p q)"
576   by (cases "p = F \<or> q = T", simp_all add: imp_def, cases p) (simp_all add: not)
578 lemma imp_qf: "qfree p \<Longrightarrow> qfree q \<Longrightarrow> qfree (imp p q)"
579   using imp_def by (cases "p = F \<or> q = T", simp_all add: imp_def, cases p) (simp_all add: not_qf)
581 lemma imp_nb: "bound0 p \<Longrightarrow> bound0 q \<Longrightarrow> bound0 (imp p q)"
582   using imp_def by (cases "p = F \<or> q = T", simp_all add: imp_def, cases p) simp_all
584 definition iff :: "fm \<Rightarrow> fm \<Rightarrow> fm"
585 where
586   "iff p q =
587     (if p = q then T
588      else if p = not q \<or> not p = q then F
589      else if p = F then not q
590      else if q = F then not p
591      else if p = T then q
592      else if q = T then p
593      else Iff p q)"
595 lemma iff: "Ifm bbs bs (iff p q) = Ifm bbs bs (Iff p q)"
596   by (unfold iff_def, cases "p = q", simp, cases "p = not q", simp add: not)
597     (cases "not p = q", auto simp add: not)
599 lemma iff_qf: "qfree p \<Longrightarrow> qfree q \<Longrightarrow> qfree (iff p q)"
600   by (unfold iff_def, cases "p = q", auto simp add: not_qf)
602 lemma iff_nb: "bound0 p \<Longrightarrow> bound0 q \<Longrightarrow> bound0 (iff p q)"
603   using iff_def by (unfold iff_def, cases "p = q", auto simp add: not_bn)
605 function (sequential) simpfm :: "fm \<Rightarrow> fm"
606 where
607   "simpfm (And p q) = conj (simpfm p) (simpfm q)"
608 | "simpfm (Or p q) = disj (simpfm p) (simpfm q)"
609 | "simpfm (Imp p q) = imp (simpfm p) (simpfm q)"
610 | "simpfm (Iff p q) = iff (simpfm p) (simpfm q)"
611 | "simpfm (NOT p) = not (simpfm p)"
612 | "simpfm (Lt a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if v < 0 then T else F | _ \<Rightarrow> Lt a')"
613 | "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')"
614 | "simpfm (Gt a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if v > 0 then T else F | _ \<Rightarrow> Gt a')"
615 | "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')"
616 | "simpfm (Eq a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if v = 0 then T else F | _ \<Rightarrow> Eq a')"
617 | "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')"
618 | "simpfm (Dvd i a) =
619     (if i = 0 then simpfm (Eq a)
620      else if abs i = 1 then T
621      else let a' = simpnum a in case a' of C v \<Rightarrow> if i dvd v then T else F | _ \<Rightarrow> Dvd i a')"
622 | "simpfm (NDvd i a) =
623     (if i = 0 then simpfm (NEq a)
624      else if abs i = 1 then F
625      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')"
626 | "simpfm p = p"
627   by pat_completeness auto
628 termination by (relation "measure fmsize") auto
630 lemma simpfm: "Ifm bbs bs (simpfm p) = Ifm bbs bs p"
631 proof (induct p rule: simpfm.induct)
632   case (6 a)
633   let ?sa = "simpnum a"
634   from simpnum_ci have sa: "Inum bs ?sa = Inum bs a"
635     by simp
636   {
637     fix v
638     assume "?sa = C v"
639     then have ?case using sa
640       by simp
641   }
642   moreover {
643     assume "\<not> (\<exists>v. ?sa = C v)"
644     then have ?case
645       using sa by (cases ?sa) (simp_all add: Let_def)
646   }
647   ultimately show ?case by blast
648 next
649   case (7 a)
650   let ?sa = "simpnum a"
651   from simpnum_ci have sa: "Inum bs ?sa = Inum bs a"
652     by simp
653   {
654     fix v
655     assume "?sa = C v"
656     then have ?case using sa
657       by simp
658   }
659   moreover {
660     assume "\<not> (\<exists>v. ?sa = C v)"
661     then have ?case
662       using sa by (cases ?sa) (simp_all add: Let_def)
663   }
664   ultimately show ?case by blast
665 next
666   case (8 a)
667   let ?sa = "simpnum a"
668   from simpnum_ci have sa: "Inum bs ?sa = Inum bs a"
669     by simp
670   {
671     fix v
672     assume "?sa = C v"
673     then have ?case using sa
674       by simp
675   }
676   moreover {
677     assume "\<not> (\<exists>v. ?sa = C v)"
678     then have ?case
679       using sa by (cases ?sa) (simp_all add: Let_def)
680   }
681   ultimately show ?case by blast
682 next
683   case (9 a)
684   let ?sa = "simpnum a"
685   from simpnum_ci have sa: "Inum bs ?sa = Inum bs a"
686     by simp
687   {
688     fix v
689     assume "?sa = C v"
690     then have ?case using sa
691       by simp
692   }
693   moreover {
694     assume "\<not> (\<exists>v. ?sa = C v)"
695     then have ?case using sa
696       by (cases ?sa) (simp_all add: Let_def)
697   }
698   ultimately show ?case by blast
699 next
700   case (10 a)
701   let ?sa = "simpnum a"
702   from simpnum_ci have sa: "Inum bs ?sa = Inum bs a"
703     by simp
704   {
705     fix v
706     assume "?sa = C v"
707     then have ?case
708       using sa by simp
709   }
710   moreover {
711     assume "\<not> (\<exists>v. ?sa = C v)"
712     then have ?case
713       using sa by (cases ?sa) (simp_all add: Let_def)
714   }
715   ultimately show ?case by blast
716 next
717   case (11 a)
718   let ?sa = "simpnum a"
719   from simpnum_ci have sa: "Inum bs ?sa = Inum bs a"
720     by simp
721   {
722     fix v
723     assume "?sa = C v"
724     then have ?case using sa
725       by simp
726   }
727   moreover {
728     assume "\<not> (\<exists>v. ?sa = C v)"
729     then have ?case
730       using sa by (cases ?sa) (simp_all add: Let_def)
731   }
732   ultimately show ?case by blast
733 next
734   case (12 i a)
735   let ?sa = "simpnum a"
736   from simpnum_ci have sa: "Inum bs ?sa = Inum bs a"
737     by simp
738   {
739     assume "i = 0"
740     then have ?case using "12.hyps"
741       by (simp add: dvd_def Let_def)
742   }
743   moreover
744   {
745     assume i1: "abs i = 1"
746     from one_dvd[of "Inum bs a"] uminus_dvd_conv[where d="1" and t="Inum bs a"]
747     have ?case
748       using i1
749       apply (cases "i = 0")
750       apply (simp_all add: Let_def)
751       apply (cases "i > 0")
752       apply simp_all
753       done
754   }
755   moreover
756   {
757     assume inz: "i \<noteq> 0" and cond: "abs i \<noteq> 1"
758     {
759       fix v
760       assume "?sa = C v"
761       then have ?case
762         using sa[symmetric] inz cond
763         by (cases "abs i = 1") auto
764     }
765     moreover
766     {
767       assume "\<not> (\<exists>v. ?sa = C v)"
768       then have "simpfm (Dvd i a) = Dvd i ?sa"
769         using inz cond by (cases ?sa) (auto simp add: Let_def)
770       then have ?case
771         using sa by simp
772     }
773     ultimately have ?case by blast
774   }
775   ultimately show ?case by blast
776 next
777   case (13 i a)
778   let ?sa = "simpnum a"
779   from simpnum_ci have sa: "Inum bs ?sa = Inum bs a"
780     by simp
781   {
782     assume "i = 0"
783     then have ?case using "13.hyps"
784       by (simp add: dvd_def Let_def)
785   }
786   moreover
787   {
788     assume i1: "abs i = 1"
789     from one_dvd[of "Inum bs a"] uminus_dvd_conv[where d="1" and t="Inum bs a"]
790     have ?case
791       using i1
792       apply (cases "i = 0")
793       apply (simp_all add: Let_def)
794       apply (cases "i > 0")
795       apply simp_all
796       done
797   }
798   moreover
799   {
800     assume inz: "i \<noteq> 0" and cond: "abs i \<noteq> 1"
801     {
802       fix v
803       assume "?sa = C v"
804       then have ?case
805         using sa[symmetric] inz cond by (cases "abs i = 1") auto
806     }
807     moreover
808     {
809       assume "\<not> (\<exists>v. ?sa = C v)"
810       then have "simpfm (NDvd i a) = NDvd i ?sa"
811         using inz cond by (cases ?sa) (auto simp add: Let_def)
812       then have ?case using sa
813         by simp
814     }
815     ultimately have ?case by blast
816   }
817   ultimately show ?case by blast
818 qed (simp_all add: conj disj imp iff not)
820 lemma simpfm_bound0: "bound0 p \<Longrightarrow> bound0 (simpfm p)"
821 proof (induct p rule: simpfm.induct)
822   case (6 a)
823   then have nb: "numbound0 a" by simp
824   then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
825   then show ?case by (cases "simpnum a") (auto simp add: Let_def)
826 next
827   case (7 a)
828   then have nb: "numbound0 a" by simp
829   then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
830   then show ?case by (cases "simpnum a") (auto simp add: Let_def)
831 next
832   case (8 a)
833   then have nb: "numbound0 a" by simp
834   then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
835   then show ?case by (cases "simpnum a") (auto simp add: Let_def)
836 next
837   case (9 a)
838   then have nb: "numbound0 a" by simp
839   then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
840   then show ?case by (cases "simpnum a") (auto simp add: Let_def)
841 next
842   case (10 a)
843   then have nb: "numbound0 a" by simp
844   then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
845   then show ?case by (cases "simpnum a") (auto simp add: Let_def)
846 next
847   case (11 a)
848   then have nb: "numbound0 a" by simp
849   then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
850   then show ?case by (cases "simpnum a") (auto simp add: Let_def)
851 next
852   case (12 i a)
853   then have nb: "numbound0 a" by simp
854   then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
855   then show ?case by (cases "simpnum a") (auto simp add: Let_def)
856 next
857   case (13 i a)
858   then have nb: "numbound0 a" by simp
859   then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
860   then show ?case by (cases "simpnum a") (auto simp add: Let_def)
861 qed (auto simp add: disj_def imp_def iff_def conj_def not_bn)
863 lemma simpfm_qf: "qfree p \<Longrightarrow> qfree (simpfm p)"
864   by (induct p rule: simpfm.induct, auto simp add: disj_qf imp_qf iff_qf conj_qf not_qf Let_def)
865     (case_tac "simpnum a", auto)+
867 text {* Generic quantifier elimination *}
868 function (sequential) qelim :: "fm \<Rightarrow> (fm \<Rightarrow> fm) \<Rightarrow> fm"
869 where
870   "qelim (E p) = (\<lambda>qe. DJ qe (qelim p qe))"
871 | "qelim (A p) = (\<lambda>qe. not (qe ((qelim (NOT p) qe))))"
872 | "qelim (NOT p) = (\<lambda>qe. not (qelim p qe))"
873 | "qelim (And p q) = (\<lambda>qe. conj (qelim p qe) (qelim q qe))"
874 | "qelim (Or  p q) = (\<lambda>qe. disj (qelim p qe) (qelim q qe))"
875 | "qelim (Imp p q) = (\<lambda>qe. imp (qelim p qe) (qelim q qe))"
876 | "qelim (Iff p q) = (\<lambda>qe. iff (qelim p qe) (qelim q qe))"
877 | "qelim p = (\<lambda>y. simpfm p)"
878   by pat_completeness auto
879 termination by (relation "measure fmsize") auto
881 lemma qelim_ci:
882   assumes qe_inv: "\<forall>bs p. qfree p \<longrightarrow> qfree (qe p) \<and> Ifm bbs bs (qe p) = Ifm bbs bs (E p)"
883   shows "\<And>bs. qfree (qelim p qe) \<and> Ifm bbs bs (qelim p qe) = Ifm bbs bs p"
884   using qe_inv DJ_qe[OF qe_inv]
885   by (induct p rule: qelim.induct)
886     (auto simp add: not disj conj iff imp not_qf disj_qf conj_qf imp_qf iff_qf
887       simpfm simpfm_qf simp del: simpfm.simps)
889 text {* Linearity for fm where Bound 0 ranges over @{text "\<int>"} *}
891 fun zsplit0 :: "num \<Rightarrow> int \<times> num"  -- {* splits the bounded from the unbounded part *}
892 where
893   "zsplit0 (C c) = (0, C c)"
894 | "zsplit0 (Bound n) = (if n = 0 then (1, C 0) else (0, Bound n))"
895 | "zsplit0 (CN n i a) =
896     (let (i', a') =  zsplit0 a
897      in if n = 0 then (i + i', a') else (i', CN n i a'))"
898 | "zsplit0 (Neg a) = (let (i', a') = zsplit0 a in (-i', Neg a'))"
899 | "zsplit0 (Add a b) =
900     (let
901       (ia, a') = zsplit0 a;
902       (ib, b') = zsplit0 b
903      in (ia + ib, Add a' b'))"
904 | "zsplit0 (Sub a b) =
905     (let
906       (ia, a') = zsplit0 a;
907       (ib, b') = zsplit0 b
908      in (ia - ib, Sub a' b'))"
909 | "zsplit0 (Mul i a) = (let (i', a') = zsplit0 a in (i*i', Mul i a'))"
911 lemma zsplit0_I:
912   "\<And>n a. zsplit0 t = (n, a) \<Longrightarrow>
913     (Inum ((x::int) # bs) (CN 0 n a) = Inum (x # bs) t) \<and> numbound0 a"
914   (is "\<And>n a. ?S t = (n,a) \<Longrightarrow> (?I x (CN 0 n a) = ?I x t) \<and> ?N a")
915 proof (induct t rule: zsplit0.induct)
916   case (1 c n a)
917   then show ?case by auto
918 next
919   case (2 m n a)
920   then show ?case by (cases "m = 0") auto
921 next
922   case (3 m i a n a')
923   let ?j = "fst (zsplit0 a)"
924   let ?b = "snd (zsplit0 a)"
925   have abj: "zsplit0 a = (?j, ?b)" by simp
926   {
927     assume "m \<noteq> 0"
928     with 3(1)[OF abj] 3(2) have ?case
929       by (auto simp add: Let_def split_def)
930   }
931   moreover
932   {
933     assume m0: "m = 0"
934     with abj have th: "a' = ?b \<and> n = i + ?j"
935       using 3 by (simp add: Let_def split_def)
936     from abj 3 m0 have th2: "(?I x (CN 0 ?j ?b) = ?I x a) \<and> ?N ?b"
937       by blast
938     from th have "?I x (CN 0 n a') = ?I x (CN 0 (i + ?j) ?b)"
939       by simp
940     also from th2 have "\<dots> = ?I x (CN 0 i (CN 0 ?j ?b))"
941       by (simp add: distrib_right)
942     finally have "?I x (CN 0 n a') = ?I  x (CN 0 i a)"
943       using th2 by simp
944     with th2 th have ?case using m0
945       by blast
946   }
947   ultimately show ?case by blast
948 next
949   case (4 t n a)
950   let ?nt = "fst (zsplit0 t)"
951   let ?at = "snd (zsplit0 t)"
952   have abj: "zsplit0 t = (?nt, ?at)"
953     by simp
954   then have th: "a = Neg ?at \<and> n = - ?nt"
955     using 4 by (simp add: Let_def split_def)
956   from abj 4 have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at"
957     by blast
958   from th2[simplified] th[simplified] show ?case
959     by simp
960 next
961   case (5 s t n a)
962   let ?ns = "fst (zsplit0 s)"
963   let ?as = "snd (zsplit0 s)"
964   let ?nt = "fst (zsplit0 t)"
965   let ?at = "snd (zsplit0 t)"
966   have abjs: "zsplit0 s = (?ns, ?as)"
967     by simp
968   moreover have abjt: "zsplit0 t = (?nt, ?at)"
969     by simp
970   ultimately have th: "a = Add ?as ?at \<and> n = ?ns + ?nt"
971     using 5 by (simp add: Let_def split_def)
972   from abjs[symmetric] have bluddy: "\<exists>x y. (x, y) = zsplit0 s"
973     by blast
974   from 5 have "(\<exists>x y. (x, y) = zsplit0 s) \<longrightarrow>
975     (\<forall>xa xb. zsplit0 t = (xa, xb) \<longrightarrow> Inum (x # bs) (CN 0 xa xb) = Inum (x # bs) t \<and> numbound0 xb)"
976     by auto
977   with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at"
978     by blast
979   from abjs 5 have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as"
980     by blast
981   from th3[simplified] th2[simplified] th[simplified] show ?case
982     by (simp add: distrib_right)
983 next
984   case (6 s t n a)
985   let ?ns = "fst (zsplit0 s)"
986   let ?as = "snd (zsplit0 s)"
987   let ?nt = "fst (zsplit0 t)"
988   let ?at = "snd (zsplit0 t)"
989   have abjs: "zsplit0 s = (?ns, ?as)"
990     by simp
991   moreover have abjt: "zsplit0 t = (?nt, ?at)"
992     by simp
993   ultimately have th: "a = Sub ?as ?at \<and> n = ?ns - ?nt"
994     using 6 by (simp add: Let_def split_def)
995   from abjs[symmetric] have bluddy: "\<exists>x y. (x, y) = zsplit0 s"
996     by blast
997   from 6 have "(\<exists>x y. (x,y) = zsplit0 s) \<longrightarrow>
998     (\<forall>xa xb. zsplit0 t = (xa, xb) \<longrightarrow> Inum (x # bs) (CN 0 xa xb) = Inum (x # bs) t \<and> numbound0 xb)"
999     by auto
1000   with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at"
1001     by blast
1002   from abjs 6 have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as"
1003     by blast
1004   from th3[simplified] th2[simplified] th[simplified] show ?case
1005     by (simp add: left_diff_distrib)
1006 next
1007   case (7 i t n a)
1008   let ?nt = "fst (zsplit0 t)"
1009   let ?at = "snd (zsplit0 t)"
1010   have abj: "zsplit0 t = (?nt,?at)"
1011     by simp
1012   then have th: "a = Mul i ?at \<and> n = i * ?nt"
1013     using 7 by (simp add: Let_def split_def)
1014   from abj 7 have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at"
1015     by blast
1016   then have "?I x (Mul i t) = i * ?I x (CN 0 ?nt ?at)"
1017     by simp
1018   also have "\<dots> = ?I x (CN 0 (i*?nt) (Mul i ?at))"
1019     by (simp add: distrib_left)
1020   finally show ?case using th th2
1021     by simp
1022 qed
1024 consts iszlfm :: "fm \<Rightarrow> bool"  -- {* Linearity test for fm *}
1025 recdef iszlfm "measure size"
1026   "iszlfm (And p q) \<longleftrightarrow> iszlfm p \<and> iszlfm q"
1027   "iszlfm (Or p q) \<longleftrightarrow> iszlfm p \<and> iszlfm q"
1028   "iszlfm (Eq  (CN 0 c e)) \<longleftrightarrow> c > 0 \<and> numbound0 e"
1029   "iszlfm (NEq (CN 0 c e)) \<longleftrightarrow> c > 0 \<and> numbound0 e"
1030   "iszlfm (Lt  (CN 0 c e)) \<longleftrightarrow> c > 0 \<and> numbound0 e"
1031   "iszlfm (Le  (CN 0 c e)) \<longleftrightarrow> c > 0 \<and> numbound0 e"
1032   "iszlfm (Gt  (CN 0 c e)) \<longleftrightarrow> c > 0 \<and> numbound0 e"
1033   "iszlfm (Ge  (CN 0 c e)) \<longleftrightarrow> c > 0 \<and> numbound0 e"
1034   "iszlfm (Dvd i (CN 0 c e)) \<longleftrightarrow> c > 0 \<and> i > 0 \<and> numbound0 e"
1035   "iszlfm (NDvd i (CN 0 c e)) \<longleftrightarrow> c > 0 \<and> i > 0 \<and> numbound0 e"
1036   "iszlfm p \<longleftrightarrow> isatom p \<and> bound0 p"
1038 lemma zlin_qfree: "iszlfm p \<Longrightarrow> qfree p"
1039   by (induct p rule: iszlfm.induct) auto
1041 consts zlfm :: "fm \<Rightarrow> fm"  -- {* Linearity transformation for fm *}
1042 recdef zlfm "measure fmsize"
1043   "zlfm (And p q) = And (zlfm p) (zlfm q)"
1044   "zlfm (Or p q) = Or (zlfm p) (zlfm q)"
1045   "zlfm (Imp p q) = Or (zlfm (NOT p)) (zlfm q)"
1046   "zlfm (Iff p q) = Or (And (zlfm p) (zlfm q)) (And (zlfm (NOT p)) (zlfm (NOT q)))"
1047   "zlfm (Lt a) =
1048     (let (c, r) = zsplit0 a in
1049       if c = 0 then Lt r else
1050       if c > 0 then (Lt (CN 0 c r))
1051       else Gt (CN 0 (- c) (Neg r)))"
1052   "zlfm (Le a) =
1053     (let (c, r) = zsplit0 a in
1054       if c = 0 then Le r
1055       else if c > 0 then Le (CN 0 c r)
1056       else Ge (CN 0 (- c) (Neg r)))"
1057   "zlfm (Gt a) =
1058     (let (c, r) = zsplit0 a in
1059       if c = 0 then Gt r else
1060       if c > 0 then Gt (CN 0 c r)
1061       else Lt (CN 0 (- c) (Neg r)))"
1062   "zlfm (Ge a) =
1063     (let (c, r) = zsplit0 a in
1064       if c = 0 then Ge r
1065       else if c > 0 then Ge (CN 0 c r)
1066       else Le (CN 0 (- c) (Neg r)))"
1067   "zlfm (Eq a) =
1068     (let (c, r) = zsplit0 a in
1069       if c = 0 then Eq r
1070       else if c > 0 then Eq (CN 0 c r)
1071       else Eq (CN 0 (- c) (Neg r)))"
1072   "zlfm (NEq a) =
1073     (let (c, r) = zsplit0 a in
1074       if c = 0 then NEq r
1075       else if c > 0 then NEq (CN 0 c r)
1076       else NEq (CN 0 (- c) (Neg r)))"
1077   "zlfm (Dvd i a) =
1078     (if i = 0 then zlfm (Eq a)
1079      else
1080       let (c, r) = zsplit0 a in
1081         if c = 0 then Dvd (abs i) r
1082         else if c > 0 then Dvd (abs i) (CN 0 c r)
1083         else Dvd (abs i) (CN 0 (- c) (Neg r)))"
1084   "zlfm (NDvd i a) =
1085     (if i = 0 then zlfm (NEq a)
1086      else
1087       let (c, r) = zsplit0 a in
1088         if c = 0 then NDvd (abs i) r
1089         else if c > 0 then NDvd (abs i) (CN 0 c r)
1090         else NDvd (abs i) (CN 0 (- c) (Neg r)))"
1091   "zlfm (NOT (And p q)) = Or (zlfm (NOT p)) (zlfm (NOT q))"
1092   "zlfm (NOT (Or p q)) = And (zlfm (NOT p)) (zlfm (NOT q))"
1093   "zlfm (NOT (Imp p q)) = And (zlfm p) (zlfm (NOT q))"
1094   "zlfm (NOT (Iff p q)) = Or (And(zlfm p) (zlfm(NOT q))) (And (zlfm(NOT p)) (zlfm q))"
1095   "zlfm (NOT (NOT p)) = zlfm p"
1096   "zlfm (NOT T) = F"
1097   "zlfm (NOT F) = T"
1098   "zlfm (NOT (Lt a)) = zlfm (Ge a)"
1099   "zlfm (NOT (Le a)) = zlfm (Gt a)"
1100   "zlfm (NOT (Gt a)) = zlfm (Le a)"
1101   "zlfm (NOT (Ge a)) = zlfm (Lt a)"
1102   "zlfm (NOT (Eq a)) = zlfm (NEq a)"
1103   "zlfm (NOT (NEq a)) = zlfm (Eq a)"
1104   "zlfm (NOT (Dvd i a)) = zlfm (NDvd i a)"
1105   "zlfm (NOT (NDvd i a)) = zlfm (Dvd i a)"
1106   "zlfm (NOT (Closed P)) = NClosed P"
1107   "zlfm (NOT (NClosed P)) = Closed P"
1108   "zlfm p = p" (hints simp add: fmsize_pos)
1110 lemma zlfm_I:
1111   assumes qfp: "qfree p"
1112   shows "Ifm bbs (i # bs) (zlfm p) = Ifm bbs (i # bs) p \<and> iszlfm (zlfm p)"
1113   (is "?I (?l p) = ?I p \<and> ?L (?l p)")
1114   using qfp
1115 proof (induct p rule: zlfm.induct)
1116   case (5 a)
1117   let ?c = "fst (zsplit0 a)"
1118   let ?r = "snd (zsplit0 a)"
1119   have spl: "zsplit0 a = (?c, ?r)"
1120     by simp
1121   from zsplit0_I[OF spl, where x="i" and bs="bs"]
1122   have Ia: "Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r"
1123     by auto
1124   let ?N = "\<lambda>t. Inum (i # bs) t"
1125   from 5 Ia nb show ?case
1126     apply (auto simp add: Let_def split_def algebra_simps)
1127     apply (cases "?r")
1128     apply auto
1129     apply (rename_tac nat a b, case_tac nat)
1130     apply auto
1131     done
1132 next
1133   case (6 a)
1134   let ?c = "fst (zsplit0 a)"
1135   let ?r = "snd (zsplit0 a)"
1136   have spl: "zsplit0 a = (?c, ?r)"
1137     by simp
1138   from zsplit0_I[OF spl, where x="i" and bs="bs"]
1139   have Ia: "Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r"
1140     by auto
1141   let ?N = "\<lambda>t. Inum (i # bs) t"
1142   from 6 Ia nb show ?case
1143     apply (auto simp add: Let_def split_def algebra_simps)
1144     apply (cases "?r")
1145     apply auto
1146     apply (rename_tac nat a b, case_tac nat)
1147     apply auto
1148     done
1149 next
1150   case (7 a)
1151   let ?c = "fst (zsplit0 a)"
1152   let ?r = "snd (zsplit0 a)"
1153   have spl: "zsplit0 a = (?c, ?r)"
1154     by simp
1155   from zsplit0_I[OF spl, where x="i" and bs="bs"]
1156   have Ia: "Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r"
1157     by auto
1158   let ?N = "\<lambda>t. Inum (i # bs) t"
1159   from 7 Ia nb show ?case
1160     apply (auto simp add: Let_def split_def algebra_simps)
1161     apply (cases "?r")
1162     apply auto
1163     apply (rename_tac nat a b, case_tac nat)
1164     apply auto
1165     done
1166 next
1167   case (8 a)
1168   let ?c = "fst (zsplit0 a)"
1169   let ?r = "snd (zsplit0 a)"
1170   have spl: "zsplit0 a = (?c, ?r)"
1171     by simp
1172   from zsplit0_I[OF spl, where x="i" and bs="bs"]
1173   have Ia: "Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r"
1174     by auto
1175   let ?N = "\<lambda>t. Inum (i # bs) t"
1176   from 8 Ia nb show ?case
1177     apply (auto simp add: Let_def split_def algebra_simps)
1178     apply (cases "?r")
1179     apply auto
1180     apply (rename_tac nat a b, case_tac nat)
1181     apply auto
1182     done
1183 next
1184   case (9 a)
1185   let ?c = "fst (zsplit0 a)"
1186   let ?r = "snd (zsplit0 a)"
1187   have spl: "zsplit0 a = (?c, ?r)"
1188     by simp
1189   from zsplit0_I[OF spl, where x="i" and bs="bs"]
1190   have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r"
1191     by auto
1192   let ?N = "\<lambda>t. Inum (i # bs) t"
1193   from 9 Ia nb show ?case
1194     apply (auto simp add: Let_def split_def algebra_simps)
1195     apply (cases "?r")
1196     apply auto
1197     apply (rename_tac nat a b, case_tac nat)
1198     apply auto
1199     done
1200 next
1201   case (10 a)
1202   let ?c = "fst (zsplit0 a)"
1203   let ?r = "snd (zsplit0 a)"
1204   have spl: "zsplit0 a = (?c, ?r)"
1205     by simp
1206   from zsplit0_I[OF spl, where x="i" and bs="bs"]
1207   have Ia: "Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r"
1208     by auto
1209   let ?N = "\<lambda>t. Inum (i # bs) t"
1210   from 10 Ia nb show ?case
1211     apply (auto simp add: Let_def split_def algebra_simps)
1212     apply (cases "?r")
1213     apply auto
1214     apply (rename_tac nat a b, case_tac nat)
1215     apply auto
1216     done
1217 next
1218   case (11 j a)
1219   let ?c = "fst (zsplit0 a)"
1220   let ?r = "snd (zsplit0 a)"
1221   have spl: "zsplit0 a = (?c,?r)"
1222     by simp
1223   from zsplit0_I[OF spl, where x="i" and bs="bs"]
1224   have Ia: "Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r"
1225     by auto
1226   let ?N = "\<lambda>t. Inum (i#bs) t"
1227   have "j = 0 \<or> (j \<noteq> 0 \<and> ?c = 0) \<or> (j \<noteq> 0 \<and> ?c > 0) \<or> (j \<noteq> 0 \<and> ?c < 0)"
1228     by arith
1229   moreover
1230   {
1231     assume "j = 0"
1232     then have z: "zlfm (Dvd j a) = (zlfm (Eq a))"
1233       by (simp add: Let_def)
1234     then have ?case using 11 `j = 0`
1235       by (simp del: zlfm.simps)
1236   }
1237   moreover
1238   {
1239     assume "?c = 0" and "j \<noteq> 0"
1240     then have ?case
1241       using zsplit0_I[OF spl, where x="i" and bs="bs"]
1242     apply (auto simp add: Let_def split_def algebra_simps)
1243     apply (cases "?r")
1244     apply auto
1245     apply (rename_tac nat a b, case_tac nat)
1246     apply auto
1247     done
1248   }
1249   moreover
1250   {
1251     assume cp: "?c > 0" and jnz: "j \<noteq> 0"
1252     then have l: "?L (?l (Dvd j a))"
1253       by (simp add: nb Let_def split_def)
1254     then have ?case
1255       using Ia cp jnz by (simp add: Let_def split_def)
1256   }
1257   moreover
1258   {
1259     assume cn: "?c < 0" and jnz: "j \<noteq> 0"
1260     then have l: "?L (?l (Dvd j a))"
1261       by (simp add: nb Let_def split_def)
1262     then have ?case
1263       using Ia cn jnz dvd_minus_iff[of "abs j" "?c*i + ?N ?r"]
1264       by (simp add: Let_def split_def)
1265   }
1266   ultimately show ?case by blast
1267 next
1268   case (12 j a)
1269   let ?c = "fst (zsplit0 a)"
1270   let ?r = "snd (zsplit0 a)"
1271   have spl: "zsplit0 a = (?c, ?r)"
1272     by simp
1273   from zsplit0_I[OF spl, where x="i" and bs="bs"]
1274   have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r"
1275     by auto
1276   let ?N = "\<lambda>t. Inum (i # bs) t"
1277   have "j = 0 \<or> (j \<noteq> 0 \<and> ?c = 0) \<or> (j \<noteq> 0 \<and> ?c > 0) \<or> (j \<noteq> 0 \<and> ?c < 0)"
1278     by arith
1279   moreover
1280   {
1281     assume "j = 0"
1282     then have z: "zlfm (NDvd j a) = zlfm (NEq a)"
1283       by (simp add: Let_def)
1284     then have ?case
1285       using assms 12 `j = 0` by (simp del: zlfm.simps)
1286   }
1287   moreover
1288   {
1289     assume "?c = 0" and "j \<noteq> 0"
1290     then have ?case
1291       using zsplit0_I[OF spl, where x="i" and bs="bs"]
1292     apply (auto simp add: Let_def split_def algebra_simps)
1293     apply (cases "?r")
1294     apply auto
1295     apply (rename_tac nat a b, case_tac nat)
1296     apply auto
1297     done
1298   }
1299   moreover
1300   {
1301     assume cp: "?c > 0" and jnz: "j \<noteq> 0"
1302     then have l: "?L (?l (Dvd j a))"
1303       by (simp add: nb Let_def split_def)
1304     then have ?case using Ia cp jnz
1305       by (simp add: Let_def split_def)
1306   }
1307   moreover
1308   {
1309     assume cn: "?c < 0" and jnz: "j \<noteq> 0"
1310     then have l: "?L (?l (Dvd j a))"
1311       by (simp add: nb Let_def split_def)
1312     then have ?case
1313       using Ia cn jnz dvd_minus_iff[of "abs j" "?c*i + ?N ?r"]
1314       by (simp add: Let_def split_def)
1315   }
1316   ultimately show ?case by blast
1317 qed auto
1319 consts minusinf :: "fm \<Rightarrow> fm" -- {* Virtual substitution of @{text "-\<infinity>"} *}
1320 recdef minusinf "measure size"
1321   "minusinf (And p q) = And (minusinf p) (minusinf q)"
1322   "minusinf (Or p q) = Or (minusinf p) (minusinf q)"
1323   "minusinf (Eq  (CN 0 c e)) = F"
1324   "minusinf (NEq (CN 0 c e)) = T"
1325   "minusinf (Lt  (CN 0 c e)) = T"
1326   "minusinf (Le  (CN 0 c e)) = T"
1327   "minusinf (Gt  (CN 0 c e)) = F"
1328   "minusinf (Ge  (CN 0 c e)) = F"
1329   "minusinf p = p"
1331 lemma minusinf_qfree: "qfree p \<Longrightarrow> qfree (minusinf p)"
1332   by (induct p rule: minusinf.induct) auto
1334 consts plusinf :: "fm \<Rightarrow> fm"  -- {* Virtual substitution of @{text "+\<infinity>"} *}
1335 recdef plusinf "measure size"
1336   "plusinf (And p q) = And (plusinf p) (plusinf q)"
1337   "plusinf (Or p q) = Or (plusinf p) (plusinf q)"
1338   "plusinf (Eq  (CN 0 c e)) = F"
1339   "plusinf (NEq (CN 0 c e)) = T"
1340   "plusinf (Lt  (CN 0 c e)) = F"
1341   "plusinf (Le  (CN 0 c e)) = F"
1342   "plusinf (Gt  (CN 0 c e)) = T"
1343   "plusinf (Ge  (CN 0 c e)) = T"
1344   "plusinf p = p"
1346 consts \<delta> :: "fm \<Rightarrow> int"  -- {* Compute @{text "lcm {d| N\<^sup>? Dvd c*x+t \<in> p}"} *}
1347 recdef \<delta> "measure size"
1348   "\<delta> (And p q) = lcm (\<delta> p) (\<delta> q)"
1349   "\<delta> (Or p q) = lcm (\<delta> p) (\<delta> q)"
1350   "\<delta> (Dvd i (CN 0 c e)) = i"
1351   "\<delta> (NDvd i (CN 0 c e)) = i"
1352   "\<delta> p = 1"
1354 consts d_\<delta> :: "fm \<Rightarrow> int \<Rightarrow> bool"  -- {* check if a given l divides all the ds above *}
1355 recdef d_\<delta> "measure size"
1356   "d_\<delta> (And p q) = (\<lambda>d. d_\<delta> p d \<and> d_\<delta> q d)"
1357   "d_\<delta> (Or p q) = (\<lambda>d. d_\<delta> p d \<and> d_\<delta> q d)"
1358   "d_\<delta> (Dvd i (CN 0 c e)) = (\<lambda>d. i dvd d)"
1359   "d_\<delta> (NDvd i (CN 0 c e)) = (\<lambda>d. i dvd d)"
1360   "d_\<delta> p = (\<lambda>d. True)"
1362 lemma delta_mono:
1363   assumes lin: "iszlfm p"
1364     and d: "d dvd d'"
1365     and ad: "d_\<delta> p d"
1366   shows "d_\<delta> p d'"
1367   using lin ad
1368 proof (induct p rule: iszlfm.induct)
1369   case (9 i c e)
1370   then show ?case using d
1371     by (simp add: dvd_trans[of "i" "d" "d'"])
1372 next
1373   case (10 i c e)
1374   then show ?case using d
1375     by (simp add: dvd_trans[of "i" "d" "d'"])
1376 qed simp_all
1378 lemma \<delta>:
1379   assumes lin: "iszlfm p"
1380   shows "d_\<delta> p (\<delta> p) \<and> \<delta> p >0"
1381   using lin
1382 proof (induct p rule: iszlfm.induct)
1383   case (1 p q)
1384   let ?d = "\<delta> (And p q)"
1385   from 1 lcm_pos_int have dp: "?d > 0"
1386     by simp
1387   have d1: "\<delta> p dvd \<delta> (And p q)"
1388     using 1 by simp
1389   then have th: "d_\<delta> p ?d"
1390     using delta_mono 1(2,3) by (simp only: iszlfm.simps)
1391   have "\<delta> q dvd \<delta> (And p q)"
1392     using 1 by simp
1393   then have th': "d_\<delta> q ?d"
1394     using delta_mono 1 by (simp only: iszlfm.simps)
1395   from th th' dp show ?case
1396     by simp
1397 next
1398   case (2 p q)
1399   let ?d = "\<delta> (And p q)"
1400   from 2 lcm_pos_int have dp: "?d > 0"
1401     by simp
1402   have "\<delta> p dvd \<delta> (And p q)"
1403     using 2 by simp
1404   then have th: "d_\<delta> p ?d"
1405     using delta_mono 2 by (simp only: iszlfm.simps)
1406   have "\<delta> q dvd \<delta> (And p q)"
1407     using 2 by simp
1408   then have th': "d_\<delta> q ?d"
1409     using delta_mono 2 by (simp only: iszlfm.simps)
1410   from th th' dp show ?case
1411     by simp
1412 qed simp_all
1415 consts a_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> fm"  -- {* adjust the coefficients of a formula *}
1416 recdef a_\<beta> "measure size"
1417   "a_\<beta> (And p q) = (\<lambda>k. And (a_\<beta> p k) (a_\<beta> q k))"
1418   "a_\<beta> (Or p q) = (\<lambda>k. Or (a_\<beta> p k) (a_\<beta> q k))"
1419   "a_\<beta> (Eq  (CN 0 c e)) = (\<lambda>k. Eq (CN 0 1 (Mul (k div c) e)))"
1420   "a_\<beta> (NEq (CN 0 c e)) = (\<lambda>k. NEq (CN 0 1 (Mul (k div c) e)))"
1421   "a_\<beta> (Lt  (CN 0 c e)) = (\<lambda>k. Lt (CN 0 1 (Mul (k div c) e)))"
1422   "a_\<beta> (Le  (CN 0 c e)) = (\<lambda>k. Le (CN 0 1 (Mul (k div c) e)))"
1423   "a_\<beta> (Gt  (CN 0 c e)) = (\<lambda>k. Gt (CN 0 1 (Mul (k div c) e)))"
1424   "a_\<beta> (Ge  (CN 0 c e)) = (\<lambda>k. Ge (CN 0 1 (Mul (k div c) e)))"
1425   "a_\<beta> (Dvd i (CN 0 c e)) =(\<lambda>k. Dvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"
1426   "a_\<beta> (NDvd i (CN 0 c e))=(\<lambda>k. NDvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"
1427   "a_\<beta> p = (\<lambda>k. p)"
1429 consts d_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> bool"  -- {* test if all coeffs c of c divide a given l *}
1430 recdef d_\<beta> "measure size"
1431   "d_\<beta> (And p q) = (\<lambda>k. (d_\<beta> p k) \<and> (d_\<beta> q k))"
1432   "d_\<beta> (Or p q) = (\<lambda>k. (d_\<beta> p k) \<and> (d_\<beta> q k))"
1433   "d_\<beta> (Eq  (CN 0 c e)) = (\<lambda>k. c dvd k)"
1434   "d_\<beta> (NEq (CN 0 c e)) = (\<lambda>k. c dvd k)"
1435   "d_\<beta> (Lt  (CN 0 c e)) = (\<lambda>k. c dvd k)"
1436   "d_\<beta> (Le  (CN 0 c e)) = (\<lambda>k. c dvd k)"
1437   "d_\<beta> (Gt  (CN 0 c e)) = (\<lambda>k. c dvd k)"
1438   "d_\<beta> (Ge  (CN 0 c e)) = (\<lambda>k. c dvd k)"
1439   "d_\<beta> (Dvd i (CN 0 c e)) =(\<lambda>k. c dvd k)"
1440   "d_\<beta> (NDvd i (CN 0 c e))=(\<lambda>k. c dvd k)"
1441   "d_\<beta> p = (\<lambda>k. True)"
1443 consts \<zeta> :: "fm \<Rightarrow> int"  -- {* computes the lcm of all coefficients of x *}
1444 recdef \<zeta> "measure size"
1445   "\<zeta> (And p q) = lcm (\<zeta> p) (\<zeta> q)"
1446   "\<zeta> (Or p q) = lcm (\<zeta> p) (\<zeta> q)"
1447   "\<zeta> (Eq  (CN 0 c e)) = c"
1448   "\<zeta> (NEq (CN 0 c e)) = c"
1449   "\<zeta> (Lt  (CN 0 c e)) = c"
1450   "\<zeta> (Le  (CN 0 c e)) = c"
1451   "\<zeta> (Gt  (CN 0 c e)) = c"
1452   "\<zeta> (Ge  (CN 0 c e)) = c"
1453   "\<zeta> (Dvd i (CN 0 c e)) = c"
1454   "\<zeta> (NDvd i (CN 0 c e))= c"
1455   "\<zeta> p = 1"
1457 consts \<beta> :: "fm \<Rightarrow> num list"
1458 recdef \<beta> "measure size"
1459   "\<beta> (And p q) = (\<beta> p @ \<beta> q)"
1460   "\<beta> (Or p q) = (\<beta> p @ \<beta> q)"
1461   "\<beta> (Eq  (CN 0 c e)) = [Sub (C -1) e]"
1462   "\<beta> (NEq (CN 0 c e)) = [Neg e]"
1463   "\<beta> (Lt  (CN 0 c e)) = []"
1464   "\<beta> (Le  (CN 0 c e)) = []"
1465   "\<beta> (Gt  (CN 0 c e)) = [Neg e]"
1466   "\<beta> (Ge  (CN 0 c e)) = [Sub (C -1) e]"
1467   "\<beta> p = []"
1469 consts \<alpha> :: "fm \<Rightarrow> num list"
1470 recdef \<alpha> "measure size"
1471   "\<alpha> (And p q) = \<alpha> p @ \<alpha> q"
1472   "\<alpha> (Or p q) = \<alpha> p @ \<alpha> q"
1473   "\<alpha> (Eq  (CN 0 c e)) = [Add (C -1) e]"
1474   "\<alpha> (NEq (CN 0 c e)) = [e]"
1475   "\<alpha> (Lt  (CN 0 c e)) = [e]"
1476   "\<alpha> (Le  (CN 0 c e)) = [Add (C -1) e]"
1477   "\<alpha> (Gt  (CN 0 c e)) = []"
1478   "\<alpha> (Ge  (CN 0 c e)) = []"
1479   "\<alpha> p = []"
1481 consts mirror :: "fm \<Rightarrow> fm"
1482 recdef mirror "measure size"
1483   "mirror (And p q) = And (mirror p) (mirror q)"
1484   "mirror (Or p q) = Or (mirror p) (mirror q)"
1485   "mirror (Eq  (CN 0 c e)) = Eq (CN 0 c (Neg e))"
1486   "mirror (NEq (CN 0 c e)) = NEq (CN 0 c (Neg e))"
1487   "mirror (Lt  (CN 0 c e)) = Gt (CN 0 c (Neg e))"
1488   "mirror (Le  (CN 0 c e)) = Ge (CN 0 c (Neg e))"
1489   "mirror (Gt  (CN 0 c e)) = Lt (CN 0 c (Neg e))"
1490   "mirror (Ge  (CN 0 c e)) = Le (CN 0 c (Neg e))"
1491   "mirror (Dvd i (CN 0 c e)) = Dvd i (CN 0 c (Neg e))"
1492   "mirror (NDvd i (CN 0 c e)) = NDvd i (CN 0 c (Neg e))"
1493   "mirror p = p"
1495 text {* Lemmas for the correctness of @{text "\<sigma>_\<rho>"} *}
1497 lemma dvd1_eq1:
1498   fixes x :: int
1499   shows "x > 0 \<Longrightarrow> x dvd 1 \<longleftrightarrow> x = 1"
1500   by simp
1502 lemma minusinf_inf:
1503   assumes linp: "iszlfm p"
1504     and u: "d_\<beta> p 1"
1505   shows "\<exists>z::int. \<forall>x < z. Ifm bbs (x # bs) (minusinf p) = Ifm bbs (x # bs) p"
1506   (is "?P p" is "\<exists>(z::int). \<forall>x < z. ?I x (?M p) = ?I x p")
1507   using linp u
1508 proof (induct p rule: minusinf.induct)
1509   case (1 p q)
1510   then show ?case
1511     by auto (rule_tac x = "min z za" in exI, simp)
1512 next
1513   case (2 p q)
1514   then show ?case
1515     by auto (rule_tac x = "min z za" in exI, simp)
1516 next
1517   case (3 c e)
1518   then have c1: "c = 1" and nb: "numbound0 e"
1519     by simp_all
1520   fix a
1521   from 3 have "\<forall>x<(- Inum (a # bs) e). c * x + Inum (x # bs) e \<noteq> 0"
1522   proof clarsimp
1523     fix x
1524     assume "x < (- Inum (a # bs) e)" and "x + Inum (x # bs) e = 0"
1525     with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
1526     show False by simp
1527   qed
1528   then show ?case by auto
1529 next
1530   case (4 c e)
1531   then have c1: "c = 1" and nb: "numbound0 e"
1532     by simp_all
1533   fix a
1534   from 4 have "\<forall>x < (- Inum (a # bs) e). c * x + Inum (x # bs) e \<noteq> 0"
1535   proof clarsimp
1536     fix x
1537     assume "x < (- Inum (a # bs) e)" and "x + Inum (x # bs) e = 0"
1538     with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
1539     show "False" by simp
1540   qed
1541   then show ?case by auto
1542 next
1543   case (5 c e)
1544   then have c1: "c = 1" and nb: "numbound0 e"
1545     by simp_all
1546   fix a
1547   from 5 have "\<forall>x<(- Inum (a # bs) e). c * x + Inum (x # bs) e < 0"
1548   proof clarsimp
1549     fix x
1550     assume "x < (- Inum (a # bs) e)"
1551     with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
1552     show "x + Inum (x # bs) e < 0"
1553       by simp
1554   qed
1555   then show ?case by auto
1556 next
1557   case (6 c e)
1558   then have c1: "c = 1" and nb: "numbound0 e"
1559     by simp_all
1560   fix a
1561   from 6 have "\<forall>x<(- Inum (a # bs) e). c * x + Inum (x # bs) e \<le> 0"
1562   proof clarsimp
1563     fix x
1564     assume "x < (- Inum (a # bs) e)"
1565     with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
1566     show "x + Inum (x # bs) e \<le> 0" by simp
1567   qed
1568   then show ?case by auto
1569 next
1570   case (7 c e)
1571   then have c1: "c = 1" and nb: "numbound0 e"
1572     by simp_all
1573   fix a
1574   from 7 have "\<forall>x<(- Inum (a # bs) e). \<not> (c * x + Inum (x # bs) e > 0)"
1575   proof clarsimp
1576     fix x
1577     assume "x < - Inum (a # bs) e" and "x + Inum (x # bs) e > 0"
1578     with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
1579     show False by simp
1580   qed
1581   then show ?case by auto
1582 next
1583   case (8 c e)
1584   then have c1: "c = 1" and nb: "numbound0 e"
1585     by simp_all
1586   fix a
1587   from 8 have "\<forall>x<(- Inum (a # bs) e). \<not> c * x + Inum (x # bs) e \<ge> 0"
1588   proof clarsimp
1589     fix x
1590     assume "x < (- Inum (a # bs) e)" and "x + Inum (x # bs) e \<ge> 0"
1591     with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
1592     show False by simp
1593   qed
1594   then show ?case by auto
1595 qed auto
1597 lemma minusinf_repeats:
1598   assumes d: "d_\<delta> p d"
1599     and linp: "iszlfm p"
1600   shows "Ifm bbs ((x - k * d) # bs) (minusinf p) = Ifm bbs (x # bs) (minusinf p)"
1601   using linp d
1602 proof (induct p rule: iszlfm.induct)
1603   case (9 i c e)
1604   then have nbe: "numbound0 e" and id: "i dvd d"
1605     by simp_all
1606   then have "\<exists>k. d = i * k"
1607     by (simp add: dvd_def)
1608   then obtain "di" where di_def: "d = i * di"
1609     by blast
1610   show ?case
1611   proof (simp add: numbound0_I[OF nbe,where bs="bs" and b="x - k * d" and b'="x"] right_diff_distrib,
1612       rule iffI)
1613     assume "i dvd c * x - c * (k * d) + Inum (x # bs) e"
1614       (is "?ri dvd ?rc * ?rx - ?rc * (?rk * ?rd) + ?I x e" is "?ri dvd ?rt")
1615     then have "\<exists>l::int. ?rt = i * l"
1616       by (simp add: dvd_def)
1617     then have "\<exists>l::int. c * x + ?I x e = i * l + c * (k * i * di)"
1618       by (simp add: algebra_simps di_def)
1619     then have "\<exists>l::int. c * x + ?I x e = i* (l + c * k * di)"
1620       by (simp add: algebra_simps)
1621     then have "\<exists>l::int. c * x + ?I x e = i * l"
1622       by blast
1623     then show "i dvd c * x + Inum (x # bs) e"
1624       by (simp add: dvd_def)
1625   next
1626     assume "i dvd c * x + Inum (x # bs) e"  (is "?ri dvd ?rc * ?rx + ?e")
1627     then have "\<exists>l::int. c * x + ?e = i * l"
1628       by (simp add: dvd_def)
1629     then have "\<exists>l::int. c * x - c * (k * d) + ?e = i * l - c * (k * d)"
1630       by simp
1631     then have "\<exists>l::int. c * x - c * (k * d) + ?e = i * l - c * (k * i * di)"
1632       by (simp add: di_def)
1633     then have "\<exists>l::int. c * x - c * (k * d) + ?e = i * (l - c * k * di)"
1634       by (simp add: algebra_simps)
1635     then have "\<exists>l::int. c * x - c * (k * d) + ?e = i * l"
1636       by blast
1637     then show "i dvd c * x - c * (k * d) + Inum (x # bs) e"
1638       by (simp add: dvd_def)
1639   qed
1640 next
1641   case (10 i c e)
1642   then have nbe: "numbound0 e" and id: "i dvd d"
1643     by simp_all
1644   then have "\<exists>k. d = i * k"
1645     by (simp add: dvd_def)
1646   then obtain di where di_def: "d = i * di"
1647     by blast
1648   show ?case
1649   proof (simp add: numbound0_I[OF nbe,where bs="bs" and b="x - k * d" and b'="x"] right_diff_distrib,
1650       rule iffI)
1651     assume "i dvd c * x - c * (k * d) + Inum (x # bs) e"
1652       (is "?ri dvd ?rc * ?rx - ?rc * (?rk * ?rd) + ?I x e" is "?ri dvd ?rt")
1653     then have "\<exists>l::int. ?rt = i * l"
1654       by (simp add: dvd_def)
1655     then have "\<exists>l::int. c * x + ?I x e = i * l + c * (k * i * di)"
1656       by (simp add: algebra_simps di_def)
1657     then have "\<exists>l::int. c * x+ ?I x e = i * (l + c * k * di)"
1658       by (simp add: algebra_simps)
1659     then have "\<exists>l::int. c * x + ?I x e = i * l"
1660       by blast
1661     then show "i dvd c * x + Inum (x # bs) e"
1662       by (simp add: dvd_def)
1663   next
1664     assume "i dvd c * x + Inum (x # bs) e" (is "?ri dvd ?rc * ?rx + ?e")
1665     then have "\<exists>l::int. c * x + ?e = i * l"
1666       by (simp add: dvd_def)
1667     then have "\<exists>l::int. c * x - c * (k * d) + ?e = i * l - c * (k * d)"
1668       by simp
1669     then have "\<exists>l::int. c * x - c * (k * d) + ?e = i * l - c * (k * i * di)"
1670       by (simp add: di_def)
1671     then have "\<exists>l::int. c * x - c * (k * d) + ?e = i * (l - c * k * di)"
1672       by (simp add: algebra_simps)
1673     then have "\<exists>l::int. c * x - c * (k * d) + ?e = i * l"
1674       by blast
1675     then show "i dvd c * x - c * (k * d) + Inum (x # bs) e"
1676       by (simp add: dvd_def)
1677   qed
1678 qed (auto simp add: gr0_conv_Suc numbound0_I[where bs="bs" and b="x - k*d" and b'="x"])
1680 lemma mirror_\<alpha>_\<beta>:
1681   assumes lp: "iszlfm p"
1682   shows "Inum (i # bs) ` set (\<alpha> p) = Inum (i # bs) ` set (\<beta> (mirror p))"
1683   using lp by (induct p rule: mirror.induct) auto
1685 lemma mirror:
1686   assumes lp: "iszlfm p"
1687   shows "Ifm bbs (x # bs) (mirror p) = Ifm bbs ((- x) # bs) p"
1688   using lp
1689 proof (induct p rule: iszlfm.induct)
1690   case (9 j c e)
1691   then have nb: "numbound0 e"
1692     by simp
1693   have "Ifm bbs (x # bs) (mirror (Dvd j (CN 0 c e))) \<longleftrightarrow> j dvd c * x - Inum (x # bs) e"
1694     (is "_ = (j dvd c*x - ?e)") by simp
1695   also have "\<dots> \<longleftrightarrow> j dvd (- (c * x - ?e))"
1696     by (simp only: dvd_minus_iff)
1697   also have "\<dots> \<longleftrightarrow> j dvd (c * (- x)) + ?e"
1698     by (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] ac_simps minus_add_distrib)
1699       (simp add: algebra_simps)
1700   also have "\<dots> = Ifm bbs ((- x) # bs) (Dvd j (CN 0 c e))"
1701     using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"] by simp
1702   finally show ?case .
1703 next
1704   case (10 j c e)
1705   then have nb: "numbound0 e"
1706     by simp
1707   have "Ifm bbs (x # bs) (mirror (Dvd j (CN 0 c e))) \<longleftrightarrow> j dvd c * x - Inum (x # bs) e"
1708     (is "_ = (j dvd c * x - ?e)") by simp
1709   also have "\<dots> \<longleftrightarrow> j dvd (- (c * x - ?e))"
1710     by (simp only: dvd_minus_iff)
1711   also have "\<dots> \<longleftrightarrow> j dvd (c * (- x)) + ?e"
1712     by (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] ac_simps minus_add_distrib)
1713       (simp add: algebra_simps)
1714   also have "\<dots> \<longleftrightarrow> Ifm bbs ((- x) # bs) (Dvd j (CN 0 c e))"
1715     using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"] by simp
1716   finally show ?case by simp
1717 qed (auto simp add: numbound0_I[where bs="bs" and b="x" and b'="- x"] gr0_conv_Suc)
1719 lemma mirror_l: "iszlfm p \<and> d_\<beta> p 1 \<Longrightarrow> iszlfm (mirror p) \<and> d_\<beta> (mirror p) 1"
1720   by (induct p rule: mirror.induct) auto
1722 lemma mirror_\<delta>: "iszlfm p \<Longrightarrow> \<delta> (mirror p) = \<delta> p"
1723   by (induct p rule: mirror.induct) auto
1725 lemma \<beta>_numbound0:
1726   assumes lp: "iszlfm p"
1727   shows "\<forall>b \<in> set (\<beta> p). numbound0 b"
1728   using lp by (induct p rule: \<beta>.induct) auto
1730 lemma d_\<beta>_mono:
1731   assumes linp: "iszlfm p"
1732     and dr: "d_\<beta> p l"
1733     and d: "l dvd l'"
1734   shows "d_\<beta> p l'"
1735   using dr linp dvd_trans[of _ "l" "l'", simplified d]
1736   by (induct p rule: iszlfm.induct) simp_all
1738 lemma \<alpha>_l:
1739   assumes "iszlfm p"
1740   shows "\<forall>b \<in> set (\<alpha> p). numbound0 b"
1741   using assms by (induct p rule: \<alpha>.induct) auto
1743 lemma \<zeta>:
1744   assumes "iszlfm p"
1745   shows "\<zeta> p > 0 \<and> d_\<beta> p (\<zeta> p)"
1746   using assms
1747 proof (induct p rule: iszlfm.induct)
1748   case (1 p q)
1749   from 1 have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)"
1750     by simp
1751   from 1 have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)"
1752     by simp
1753   from 1 d_\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"]
1754       d_\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"]
1755       dl1 dl2
1756   show ?case
1757     by (auto simp add: lcm_pos_int)
1758 next
1759   case (2 p q)
1760   from 2 have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)"
1761     by simp
1762   from 2 have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)"
1763     by simp
1764   from 2 d_\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"]
1765       d_\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"]
1766       dl1 dl2
1767   show ?case
1768     by (auto simp add: lcm_pos_int)
1769 qed (auto simp add: lcm_pos_int)
1771 lemma a_\<beta>:
1772   assumes linp: "iszlfm p"
1773     and d: "d_\<beta> p l"
1774     and lp: "l > 0"
1775   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"
1776   using linp d
1777 proof (induct p rule: iszlfm.induct)
1778   case (5 c e)
1779   then have cp: "c > 0" and be: "numbound0 e" and d': "c dvd l"
1780     by simp_all
1781   from lp cp have clel: "c \<le> l"
1782     by (simp add: zdvd_imp_le [OF d' lp])
1783   from cp have cnz: "c \<noteq> 0"
1784     by simp
1785   have "c div c \<le> l div c"
1786     by (simp add: zdiv_mono1[OF clel cp])
1787   then have ldcp: "0 < l div c"
1788     by (simp add: div_self[OF cnz])
1789   have "c * (l div c) = c * (l div c) + l mod c"
1790     using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
1791   then have cl: "c * (l div c) =l"
1792     using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp
1793   then have "(l * x + (l div c) * Inum (x # bs) e < 0) \<longleftrightarrow>
1794       ((c * (l div c)) * x + (l div c) * Inum (x # bs) e < 0)"
1795     by simp
1796   also have "\<dots> \<longleftrightarrow> (l div c) * (c * x + Inum (x # bs) e) < (l div c) * 0"
1797     by (simp add: algebra_simps)
1798   also have "\<dots> \<longleftrightarrow> c * x + Inum (x # bs) e < 0"
1799     using mult_less_0_iff [where a="(l div c)" and b="c*x + Inum (x # bs) e"] ldcp
1800     by simp
1801   finally show ?case
1802     using numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"] be
1803     by simp
1804 next
1805   case (6 c e)
1806   then have cp: "c > 0" and be: "numbound0 e" and d': "c dvd l"
1807     by simp_all
1808   from lp cp have clel: "c \<le> l"
1809     by (simp add: zdvd_imp_le [OF d' lp])
1810   from cp have cnz: "c \<noteq> 0"
1811     by simp
1812   have "c div c \<le> l div c"
1813     by (simp add: zdiv_mono1[OF clel cp])
1814   then have ldcp:"0 < l div c"
1815     by (simp add: div_self[OF cnz])
1816   have "c * (l div c) = c * (l div c) + l mod c"
1817     using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
1818   then have cl: "c * (l div c) = l"
1819     using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp
1820   then have "l * x + (l div c) * Inum (x # bs) e \<le> 0 \<longleftrightarrow>
1821       (c * (l div c)) * x + (l div c) * Inum (x # bs) e \<le> 0"
1822     by simp
1823   also have "\<dots> \<longleftrightarrow> (l div c) * (c * x + Inum (x # bs) e) \<le> (l div c) * 0"
1824     by (simp add: algebra_simps)
1825   also have "\<dots> \<longleftrightarrow> c * x + Inum (x # bs) e \<le> 0"
1826     using mult_le_0_iff [where a="(l div c)" and b="c*x + Inum (x # bs) e"] ldcp by simp
1827   finally show ?case
1828     using numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"] be by simp
1829 next
1830   case (7 c e)
1831   then have cp: "c > 0" and be: "numbound0 e" and d': "c dvd l"
1832     by simp_all
1833   from lp cp have clel: "c \<le> l"
1834     by (simp add: zdvd_imp_le [OF d' lp])
1835   from cp have cnz: "c \<noteq> 0"
1836     by simp
1837   have "c div c \<le> l div c"
1838     by (simp add: zdiv_mono1[OF clel cp])
1839   then have ldcp: "0 < l div c"
1840     by (simp add: div_self[OF cnz])
1841   have "c * (l div c) = c * (l div c) + l mod c"
1842     using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
1843   then have cl: "c * (l div c) = l"
1844     using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp
1845   then have "l * x + (l div c) * Inum (x # bs) e > 0 \<longleftrightarrow>
1846       (c * (l div c)) * x + (l div c) * Inum (x # bs) e > 0"
1847     by simp
1848   also have "\<dots> \<longleftrightarrow> (l div c) * (c * x + Inum (x # bs) e) > (l div c) * 0"
1849     by (simp add: algebra_simps)
1850   also have "\<dots> \<longleftrightarrow> c * x + Inum (x # bs) e > 0"
1851     using zero_less_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e"] ldcp
1852     by simp
1853   finally show ?case
1854     using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be
1855     by simp
1856 next
1857   case (8 c e)
1858   then have cp: "c > 0" and be: "numbound0 e" and d': "c dvd l"
1859     by simp_all
1860   from lp cp have clel: "c \<le> l"
1861     by (simp add: zdvd_imp_le [OF d' lp])
1862   from cp have cnz: "c \<noteq> 0"
1863     by simp
1864   have "c div c \<le> l div c"
1865     by (simp add: zdiv_mono1[OF clel cp])
1866   then have ldcp: "0 < l div c"
1867     by (simp add: div_self[OF cnz])
1868   have "c * (l div c) = c * (l div c) + l mod c"
1869     using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
1870   then have cl: "c * (l div c) =l"
1871     using zmod_zdiv_equality[where a="l" and b="c", symmetric]
1872     by simp
1873   then have "l * x + (l div c) * Inum (x # bs) e \<ge> 0 \<longleftrightarrow>
1874       (c * (l div c)) * x + (l div c) * Inum (x # bs) e \<ge> 0"
1875     by simp
1876   also have "\<dots> \<longleftrightarrow> (l div c) * (c * x + Inum (x # bs) e) \<ge> (l div c) * 0"
1877     by (simp add: algebra_simps)
1878   also have "\<dots> \<longleftrightarrow> c * x + Inum (x # bs) e \<ge> 0"
1879     using ldcp zero_le_mult_iff [where a="l div c" and b="c*x + Inum (x # bs) e"]
1880     by simp
1881   finally show ?case
1882     using be numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"]
1883     by simp
1884 next
1885   case (3 c e)
1886   then have cp: "c > 0" and be: "numbound0 e" and d': "c dvd l"
1887     by simp_all
1888   from lp cp have clel: "c \<le> l"
1889     by (simp add: zdvd_imp_le [OF d' lp])
1890   from cp have cnz: "c \<noteq> 0"
1891     by simp
1892   have "c div c \<le> l div c"
1893     by (simp add: zdiv_mono1[OF clel cp])
1894   then have ldcp:"0 < l div c"
1895     by (simp add: div_self[OF cnz])
1896   have "c * (l div c) = c * (l div c) + l mod c"
1897     using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
1898   then have cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
1899     by simp
1900   then have "l * x + (l div c) * Inum (x # bs) e = 0 \<longleftrightarrow>
1901       (c * (l div c)) * x + (l div c) * Inum (x # bs) e = 0"
1902     by simp
1903   also have "\<dots> \<longleftrightarrow> (l div c) * (c * x + Inum (x # bs) e) = ((l div c)) * 0"
1904     by (simp add: algebra_simps)
1905   also have "\<dots> \<longleftrightarrow> c * x + Inum (x # bs) e = 0"
1906     using mult_eq_0_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e"] ldcp
1907     by simp
1908   finally show ?case
1909     using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be
1910     by simp
1911 next
1912   case (4 c e)
1913   then have cp: "c > 0" and be: "numbound0 e" and d': "c dvd l"
1914     by simp_all
1915   from lp cp have clel: "c \<le> l"
1916     by (simp add: zdvd_imp_le [OF d' lp])
1917   from cp have cnz: "c \<noteq> 0"
1918     by simp
1919   have "c div c \<le> l div c"
1920     by (simp add: zdiv_mono1[OF clel cp])
1921   then have ldcp:"0 < l div c"
1922     by (simp add: div_self[OF cnz])
1923   have "c * (l div c) = c * (l div c) + l mod c"
1924     using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
1925   then have cl: "c * (l div c) = l"
1926     using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp
1927   then have "l * x + (l div c) * Inum (x # bs) e \<noteq> 0 \<longleftrightarrow>
1928       (c * (l div c)) * x + (l div c) * Inum (x # bs) e \<noteq> 0"
1929     by simp
1930   also have "\<dots> \<longleftrightarrow> (l div c) * (c * x + Inum (x # bs) e) \<noteq> (l div c) * 0"
1931     by (simp add: algebra_simps)
1932   also have "\<dots> \<longleftrightarrow> c * x + Inum (x # bs) e \<noteq> 0"
1933     using zero_le_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e"] ldcp
1934     by simp
1935   finally show ?case
1936     using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be
1937     by simp
1938 next
1939   case (9 j c e)
1940   then have cp: "c > 0" and be: "numbound0 e" and jp: "j > 0" and d': "c dvd l"
1941     by simp_all
1942   from lp cp have clel: "c \<le> l"
1943     by (simp add: zdvd_imp_le [OF d' lp])
1944   from cp have cnz: "c \<noteq> 0" by simp
1945   have "c div c\<le> l div c"
1946     by (simp add: zdiv_mono1[OF clel cp])
1947   then have ldcp:"0 < l div c"
1948     by (simp add: div_self[OF cnz])
1949   have "c * (l div c) = c * (l div c) + l mod c"
1950     using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
1951   then have cl: "c * (l div c) = l"
1952     using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp
1953   then have "(\<exists>k::int. l * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k) \<longleftrightarrow>
1954       (\<exists>k::int. (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)"
1955     by simp
1956   also have "\<dots> \<longleftrightarrow> (\<exists>k::int. (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c) * 0)"
1957     by (simp add: algebra_simps)
1958   also
1959   fix k
1960   have "\<dots> \<longleftrightarrow> (\<exists>k::int. c * x + Inum (x # bs) e - j * k = 0)"
1961     using zero_le_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e - j * k"] ldcp
1962     by simp
1963   also have "\<dots> \<longleftrightarrow> (\<exists>k::int. c * x + Inum (x # bs) e = j * k)"
1964     by simp
1965   finally show ?case
1966     using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"]
1967       be mult_strict_mono[OF ldcp jp ldcp ]
1968     by (simp add: dvd_def)
1969 next
1970   case (10 j c e)
1971   then have cp: "c > 0" and be: "numbound0 e" and jp: "j > 0" and d': "c dvd l"
1972     by simp_all
1973   from lp cp have clel: "c \<le> l"
1974     by (simp add: zdvd_imp_le [OF d' lp])
1975   from cp have cnz: "c \<noteq> 0"
1976     by simp
1977   have "c div c \<le> l div c"
1978     by (simp add: zdiv_mono1[OF clel cp])
1979   then have ldcp: "0 < l div c"
1980     by (simp add: div_self[OF cnz])
1981   have "c * (l div c) = c* (l div c) + l mod c"
1982     using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
1983   then have cl:"c * (l div c) =l"
1984     using zmod_zdiv_equality[where a="l" and b="c", symmetric]
1985     by simp
1986   then have "(\<exists>k::int. l * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k) \<longleftrightarrow>
1987       (\<exists>k::int. (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)"
1988     by simp
1989   also have "\<dots> \<longleftrightarrow> (\<exists>k::int. (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c) * 0)"
1990     by (simp add: algebra_simps)
1991   also
1992   fix k
1993   have "\<dots> \<longleftrightarrow> (\<exists>k::int. c * x + Inum (x # bs) e - j * k = 0)"
1994     using zero_le_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e - j * k"] ldcp
1995     by simp
1996   also have "\<dots> \<longleftrightarrow> (\<exists>k::int. c * x + Inum (x # bs) e = j * k)"
1997     by simp
1998   finally show ?case
1999     using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be
2000       mult_strict_mono[OF ldcp jp ldcp ]
2001     by (simp add: dvd_def)
2002 qed (auto simp add: gr0_conv_Suc numbound0_I[where bs="bs" and b="(l * x)" and b'="x"])
2004 lemma a_\<beta>_ex:
2005   assumes linp: "iszlfm p"
2006     and d: "d_\<beta> p l"
2007     and lp: "l > 0"
2008   shows "(\<exists>x. l dvd x \<and> Ifm bbs (x #bs) (a_\<beta> p l)) \<longleftrightarrow> (\<exists>x::int. Ifm bbs (x#bs) p)"
2009   (is "(\<exists>x. l dvd x \<and> ?P x) \<longleftrightarrow> (\<exists>x. ?P' x)")
2010 proof-
2011   have "(\<exists>x. l dvd x \<and> ?P x) \<longleftrightarrow> (\<exists>x::int. ?P (l * x))"
2012     using unity_coeff_ex[where l="l" and P="?P", simplified] by simp
2013   also have "\<dots> = (\<exists>x::int. ?P' x)"
2014     using a_\<beta>[OF linp d lp] by simp
2015   finally show ?thesis  .
2016 qed
2018 lemma \<beta>:
2019   assumes "iszlfm p"
2020     and "d_\<beta> p 1"
2021     and "d_\<delta> p d"
2022     and dp: "d > 0"
2023     and "\<not> (\<exists>j::int \<in> {1 .. d}. \<exists>b \<in> Inum (a # bs) ` set (\<beta> p). x = b + j)"
2024     and p: "Ifm bbs (x # bs) p" (is "?P x")
2025   shows "?P (x - d)"
2026   using assms
2027 proof (induct p rule: iszlfm.induct)
2028   case (5 c e)
2029   then have c1: "c = 1" and  bn: "numbound0 e"
2030     by simp_all
2031   with dp p c1 numbound0_I[OF bn,where b = "(x - d)" and b' = "x" and bs = "bs"] 5
2032   show ?case by simp
2033 next
2034   case (6 c e)
2035   then have c1: "c = 1" and  bn: "numbound0 e"
2036     by simp_all
2037   with dp p c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] 6
2038   show ?case by simp
2039 next
2040   case (7 c e)
2041   then have p: "Ifm bbs (x # bs) (Gt (CN 0 c e))" and c1: "c=1" and bn: "numbound0 e"
2042     by simp_all
2043   let ?e = "Inum (x # bs) e"
2044   {
2045     assume "(x - d) + ?e > 0"
2046     then have ?case
2047       using c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] by simp
2048   }
2049   moreover
2050   {
2051     assume H: "\<not> (x - d) + ?e > 0"
2052     let ?v = "Neg e"
2053     have vb: "?v \<in> set (\<beta> (Gt (CN 0 c e)))"
2054       by simp
2055     from 7(5)[simplified simp_thms Inum.simps \<beta>.simps list.set bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]]
2056     have nob: "\<not> (\<exists>j\<in> {1 ..d}. x = - ?e + j)"
2057       by auto
2058     from H p have "x + ?e > 0 \<and> x + ?e \<le> d"
2059       by (simp add: c1)
2060     then have "x + ?e \<ge> 1 \<and> x + ?e \<le> d"
2061       by simp
2062     then have "\<exists>j::int \<in> {1 .. d}. j = x + ?e"
2063       by simp
2064     then have "\<exists>j::int \<in> {1 .. d}. x = (- ?e + j)"
2065       by (simp add: algebra_simps)
2066     with nob have ?case
2067       by auto
2068   }
2069   ultimately show ?case
2070     by blast
2071 next
2072   case (8 c e)
2073   then have p: "Ifm bbs (x # bs) (Ge (CN 0 c e))" and c1: "c = 1" and bn: "numbound0 e"
2074     by simp_all
2075   let ?e = "Inum (x # bs) e"
2076   {
2077     assume "(x - d) + ?e \<ge> 0"
2078     then have ?case
2079       using c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"]
2080       by simp
2081   }
2082   moreover
2083   {
2084     assume H: "\<not> (x - d) + ?e \<ge> 0"
2085     let ?v = "Sub (C -1) e"
2086     have vb: "?v \<in> set (\<beta> (Ge (CN 0 c e)))"
2087       by simp
2088     from 8(5)[simplified simp_thms Inum.simps \<beta>.simps list.set bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]]
2089     have nob: "\<not> (\<exists>j\<in> {1 ..d}. x =  - ?e - 1 + j)"
2090       by auto
2091     from H p have "x + ?e \<ge> 0 \<and> x + ?e < d"
2092       by (simp add: c1)
2093     then have "x + ?e +1 \<ge> 1 \<and> x + ?e + 1 \<le> d"
2094       by simp
2095     then have "\<exists>j::int \<in> {1 .. d}. j = x + ?e + 1"
2096       by simp
2097     then have "\<exists>j::int \<in> {1 .. d}. x= - ?e - 1 + j"
2098       by (simp add: algebra_simps)
2099     with nob have ?case
2100       by simp
2101   }
2102   ultimately show ?case
2103     by blast
2104 next
2105   case (3 c e)
2106   then
2107   have p: "Ifm bbs (x #bs) (Eq (CN 0 c e))" (is "?p x")
2108     and c1: "c = 1"
2109     and bn: "numbound0 e"
2110     by simp_all
2111   let ?e = "Inum (x # bs) e"
2112   let ?v="(Sub (C -1) e)"
2113   have vb: "?v \<in> set (\<beta> (Eq (CN 0 c e)))"
2114     by simp
2115   from p have "x= - ?e"
2116     by (simp add: c1) with 3(5)
2117   show ?case
2118     using dp
2119     by simp (erule ballE[where x="1"],
2120       simp_all add:algebra_simps numbound0_I[OF bn,where b="x"and b'="a"and bs="bs"])
2121 next
2122   case (4 c e)
2123   then
2124   have p: "Ifm bbs (x # bs) (NEq (CN 0 c e))" (is "?p x")
2125     and c1: "c = 1"
2126     and bn: "numbound0 e"
2127     by simp_all
2128   let ?e = "Inum (x # bs) e"
2129   let ?v="Neg e"
2130   have vb: "?v \<in> set (\<beta> (NEq (CN 0 c e)))"
2131     by simp
2132   {
2133     assume "x - d + Inum (((x -d)) # bs) e \<noteq> 0"
2134     then have ?case by (simp add: c1)
2135   }
2136   moreover
2137   {
2138     assume H: "x - d + Inum ((x - d) # bs) e = 0"
2139     then have "x = - Inum ((x - d) # bs) e + d"
2140       by simp
2141     then have "x = - Inum (a # bs) e + d"
2142       by (simp add: numbound0_I[OF bn,where b="x - d"and b'="a"and bs="bs"])
2143      with 4(5) have ?case
2144       using dp by simp
2145   }
2146   ultimately show ?case
2147     by blast
2148 next
2149   case (9 j c e)
2150   then
2151   have p: "Ifm bbs (x # bs) (Dvd j (CN 0 c e))" (is "?p x")
2152     and c1: "c = 1"
2153     and bn: "numbound0 e"
2154     by simp_all
2155   let ?e = "Inum (x # bs) e"
2156   from 9 have id: "j dvd d"
2157     by simp
2158   from c1 have "?p x \<longleftrightarrow> j dvd (x + ?e)"
2159     by simp
2160   also have "\<dots> \<longleftrightarrow> j dvd x - d + ?e"
2161     using zdvd_period[OF id, where x="x" and c="-1" and t="?e"]
2162     by simp
2163   finally show ?case
2164     using numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] c1 p
2165     by simp
2166 next
2167   case (10 j c e)
2168   then
2169   have p: "Ifm bbs (x # bs) (NDvd j (CN 0 c e))" (is "?p x")
2170     and c1: "c = 1"
2171     and bn: "numbound0 e"
2172     by simp_all
2173   let ?e = "Inum (x # bs) e"
2174   from 10 have id: "j dvd d"
2175     by simp
2176   from c1 have "?p x \<longleftrightarrow> \<not> j dvd (x + ?e)"
2177     by simp
2178   also have "\<dots> \<longleftrightarrow> \<not> j dvd x - d + ?e"
2179     using zdvd_period[OF id, where x="x" and c="-1" and t="?e"]
2180     by simp
2181   finally show ?case
2182     using numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] c1 p
2183     by simp
2184 qed (auto simp add: numbound0_I[where bs="bs" and b="(x - d)" and b'="x"] gr0_conv_Suc)
2186 lemma \<beta>':
2187   assumes lp: "iszlfm p"
2188   and u: "d_\<beta> p 1"
2189   and d: "d_\<delta> p d"
2190   and dp: "d > 0"
2191   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>
2192     Ifm bbs (x # bs) p \<longrightarrow> Ifm bbs ((x - d) # bs) p" (is "\<forall>x. ?b \<longrightarrow> ?P x \<longrightarrow> ?P (x - d)")
2193 proof clarify
2194   fix x
2195   assume nb: "?b"
2196     and px: "?P x"
2197   then have nb2: "\<not> (\<exists>j::int \<in> {1 .. d}. \<exists>b \<in> Inum (a # bs) ` set (\<beta> p). x = b + j)"
2198     by auto
2199   from  \<beta>[OF lp u d dp nb2 px] show "?P (x -d )" .
2200 qed
2202 lemma cpmi_eq:
2203   fixes P P1 :: "int \<Rightarrow> bool"
2204   assumes "0 < D"
2205     and "\<exists>z. \<forall>x. x < z \<longrightarrow> P x = P1 x"
2206     and "\<forall>x. \<not> (\<exists>j \<in> {1..D}. \<exists>b \<in> B. P (b + j)) \<longrightarrow> P x \<longrightarrow> P (x - D)"
2207     and "\<forall>x k. P1 x = P1 (x - k * D)"
2208   shows "(\<exists>x. P x) \<longleftrightarrow> (\<exists>j \<in> {1..D}. P1 j) \<or> (\<exists>j \<in> {1..D}. \<exists>b \<in> B. P (b + j))"
2209   apply (insert assms)
2210   apply (rule iffI)
2211   prefer 2
2212   apply (drule minusinfinity)
2213   apply assumption+
2214   apply fastforce
2215   apply clarsimp
2216   apply (subgoal_tac "\<And>k. 0 \<le> k \<Longrightarrow> \<forall>x. P x \<longrightarrow> P (x - k * D)")
2217   apply (frule_tac x = x and z=z in decr_lemma)
2218   apply (subgoal_tac "P1 (x - (\<bar>x - z\<bar> + 1) * D)")
2219   prefer 2
2220   apply (subgoal_tac "0 \<le> \<bar>x - z\<bar> + 1")
2221   prefer 2 apply arith
2222    apply fastforce
2223   apply (drule (1)  periodic_finite_ex)
2224   apply blast
2225   apply (blast dest: decr_mult_lemma)
2226   done
2228 theorem cp_thm:
2229   assumes lp: "iszlfm p"
2230     and u: "d_\<beta> p 1"
2231     and d: "d_\<delta> p d"
2232     and dp: "d > 0"
2233   shows "(\<exists>x. Ifm bbs (x # bs) p) \<longleftrightarrow>
2234     (\<exists>j \<in> {1.. d}. Ifm bbs (j # bs) (minusinf p) \<or>
2235       (\<exists>b \<in> set (\<beta> p). Ifm bbs ((Inum (i # bs) b + j) # bs) p))"
2236   (is "(\<exists>x. ?P x) \<longleftrightarrow> (\<exists>j \<in> ?D. ?M j \<or> (\<exists>b \<in> ?B. ?P (?I b + j)))")
2237 proof -
2238   from minusinf_inf[OF lp u]
2239   have th: "\<exists>z. \<forall>x<z. ?P x = ?M x"
2240     by blast
2241   let ?B' = "{?I b | b. b \<in> ?B}"
2242   have BB': "(\<exists>j\<in>?D. \<exists>b \<in> ?B. ?P (?I b + j)) \<longleftrightarrow> (\<exists>j \<in> ?D. \<exists>b \<in> ?B'. ?P (b + j))"
2243     by auto
2244   then have th2: "\<forall>x. \<not> (\<exists>j \<in> ?D. \<exists>b \<in> ?B'. ?P (b + j)) \<longrightarrow> ?P x \<longrightarrow> ?P (x - d)"
2245     using \<beta>'[OF lp u d dp, where a="i" and bbs = "bbs"] by blast
2246   from minusinf_repeats[OF d lp]
2247   have th3: "\<forall>x k. ?M x = ?M (x-k*d)"
2248     by simp
2249   from cpmi_eq[OF dp th th2 th3] BB' show ?thesis
2250     by blast
2251 qed
2253 (* Implement the right hand sides of Cooper's theorem and Ferrante and Rackoff. *)
2254 lemma mirror_ex:
2255   assumes "iszlfm p"
2256   shows "(\<exists>x. Ifm bbs (x#bs) (mirror p)) \<longleftrightarrow> (\<exists>x. Ifm bbs (x#bs) p)"
2257   (is "(\<exists>x. ?I x ?mp) = (\<exists>x. ?I x p)")
2258 proof auto
2259   fix x
2260   assume "?I x ?mp"
2261   then have "?I (- x) p"
2262     using mirror[OF assms] by blast
2263   then show "\<exists>x. ?I x p"
2264     by blast
2265 next
2266   fix x
2267   assume "?I x p"
2268   then have "?I (- x) ?mp"
2269     using mirror[OF assms, where x="- x", symmetric] by auto
2270   then show "\<exists>x. ?I x ?mp"
2271     by blast
2272 qed
2274 lemma cp_thm':
2275   assumes "iszlfm p"
2276     and "d_\<beta> p 1"
2277     and "d_\<delta> p d"
2278     and "d > 0"
2279   shows "(\<exists>x. Ifm bbs (x # bs) p) \<longleftrightarrow>
2280     ((\<exists>j\<in> {1 .. d}. Ifm bbs (j#bs) (minusinf p)) \<or>
2281       (\<exists>j\<in> {1.. d}. \<exists>b\<in> (Inum (i#bs)) ` set (\<beta> p). Ifm bbs ((b + j) # bs) p))"
2282   using cp_thm[OF assms,where i="i"] by auto
2284 definition unit :: "fm \<Rightarrow> fm \<times> num list \<times> int"
2285 where
2286   "unit p =
2287      (let
2288         p' = zlfm p;
2289         l = \<zeta> p';
2290         q = And (Dvd l (CN 0 1 (C 0))) (a_\<beta> p' l);
2291         d = \<delta> q;
2292         B = remdups (map simpnum (\<beta> q));
2293         a = remdups (map simpnum (\<alpha> q))
2294       in if length B \<le> length a then (q, B, d) else (mirror q, a, d))"
2296 lemma unit:
2297   assumes qf: "qfree p"
2298   shows "\<And>q B d. unit p = (q, B, d) \<Longrightarrow>
2299     ((\<exists>x. Ifm bbs (x # bs) p) \<longleftrightarrow> (\<exists>x. Ifm bbs (x # bs) q)) \<and>
2300     (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>
2301     iszlfm q \<and> (\<forall>b\<in> set B. numbound0 b)"
2302 proof -
2303   fix q B d
2304   assume qBd: "unit p = (q,B,d)"
2305   let ?thes = "((\<exists>x. Ifm bbs (x#bs) p) \<longleftrightarrow> (\<exists>x. Ifm bbs (x#bs) q)) \<and>
2306     Inum (i#bs) ` set B = Inum (i#bs) ` set (\<beta> q) \<and>
2307     d_\<beta> q 1 \<and> d_\<delta> q d \<and> 0 < d \<and> iszlfm q \<and> (\<forall>b\<in> set B. numbound0 b)"
2308   let ?I = "\<lambda>x p. Ifm bbs (x#bs) p"
2309   let ?p' = "zlfm p"
2310   let ?l = "\<zeta> ?p'"
2311   let ?q = "And (Dvd ?l (CN 0 1 (C 0))) (a_\<beta> ?p' ?l)"
2312   let ?d = "\<delta> ?q"
2313   let ?B = "set (\<beta> ?q)"
2314   let ?B'= "remdups (map simpnum (\<beta> ?q))"
2315   let ?A = "set (\<alpha> ?q)"
2316   let ?A'= "remdups (map simpnum (\<alpha> ?q))"
2317   from conjunct1[OF zlfm_I[OF qf, where bs="bs"]]
2318   have pp': "\<forall>i. ?I i ?p' = ?I i p" by auto
2319   from conjunct2[OF zlfm_I[OF qf, where bs="bs" and i="i"]]
2320   have lp': "iszlfm ?p'" .
2321   from lp' \<zeta>[where p="?p'"] have lp: "?l >0" and dl: "d_\<beta> ?p' ?l" by auto
2322   from a_\<beta>_ex[where p="?p'" and l="?l" and bs="bs", OF lp' dl lp] pp'
2323   have pq_ex:"(\<exists>(x::int). ?I x p) = (\<exists>x. ?I x ?q)" by simp
2324   from lp' lp a_\<beta>[OF lp' dl lp] have lq:"iszlfm ?q" and uq: "d_\<beta> ?q 1"  by auto
2325   from \<delta>[OF lq] have dp:"?d >0" and dd: "d_\<delta> ?q ?d" by blast+
2326   let ?N = "\<lambda>t. Inum (i#bs) t"
2327   have "?N ` set ?B' = ((?N \<circ> simpnum) ` ?B)"
2328     by auto
2329   also have "\<dots> = ?N ` ?B"
2330     using simpnum_ci[where bs="i#bs"] by auto
2331   finally have BB': "?N ` set ?B' = ?N ` ?B" .
2332   have "?N ` set ?A' = ((?N \<circ> simpnum) ` ?A)"
2333     by auto
2334   also have "\<dots> = ?N ` ?A"
2335     using simpnum_ci[where bs="i#bs"] by auto
2336   finally have AA': "?N ` set ?A' = ?N ` ?A" .
2337   from \<beta>_numbound0[OF lq] have B_nb:"\<forall>b\<in> set ?B'. numbound0 b"
2338     by (simp add: simpnum_numbound0)
2339   from \<alpha>_l[OF lq] have A_nb: "\<forall>b\<in> set ?A'. numbound0 b"
2340     by (simp add: simpnum_numbound0)
2341   {
2342     assume "length ?B' \<le> length ?A'"
2343     then have q: "q = ?q" and "B = ?B'" and d: "d = ?d"
2344       using qBd by (auto simp add: Let_def unit_def)
2345     with BB' B_nb
2346     have b: "?N ` (set B) = ?N ` set (\<beta> q)" and bn: "\<forall>b\<in> set B. numbound0 b"
2347       by simp_all
2348     with pq_ex dp uq dd lq q d have ?thes
2349       by simp
2350   }
2351   moreover
2352   {
2353     assume "\<not> (length ?B' \<le> length ?A')"
2354     then have q:"q=mirror ?q" and "B = ?A'" and d:"d = ?d"
2355       using qBd by (auto simp add: Let_def unit_def)
2356     with AA' mirror_\<alpha>_\<beta>[OF lq] A_nb have b:"?N ` (set B) = ?N ` set (\<beta> q)"
2357       and bn: "\<forall>b\<in> set B. numbound0 b" by simp_all
2358     from mirror_ex[OF lq] pq_ex q
2359     have pqm_eq:"(\<exists>(x::int). ?I x p) = (\<exists>(x::int). ?I x q)"
2360       by simp
2361     from lq uq q mirror_l[where p="?q"]
2362     have lq': "iszlfm q" and uq: "d_\<beta> q 1"
2363       by auto
2364     from \<delta>[OF lq'] mirror_\<delta>[OF lq] q d have dq: "d_\<delta> q d"
2365       by auto
2366     from pqm_eq b bn uq lq' dp dq q dp d have ?thes
2367       by simp
2368   }
2369   ultimately show ?thes by blast
2370 qed
2373 text {* Cooper's Algorithm *}
2375 definition cooper :: "fm \<Rightarrow> fm"
2376 where
2377   "cooper p =
2378     (let
2379       (q, B, d) = unit p;
2380       js = [1..d];
2381       mq = simpfm (minusinf q);
2382       md = evaldjf (\<lambda>j. simpfm (subst0 (C j) mq)) js
2383      in
2384       if md = T then T
2385       else
2386         (let
2387           qd = evaldjf (\<lambda>(b, j). simpfm (subst0 (Add b (C j)) q)) [(b, j). b \<leftarrow> B, j \<leftarrow> js]
2388          in decr (disj md qd)))"
2390 lemma cooper:
2391   assumes qf: "qfree p"
2392   shows "((\<exists>x. Ifm bbs (x#bs) p) = (Ifm bbs bs (cooper p))) \<and> qfree (cooper p)"
2393   (is "(?lhs = ?rhs) \<and> _")
2394 proof -
2395   let ?I = "\<lambda>x p. Ifm bbs (x#bs) p"
2396   let ?q = "fst (unit p)"
2397   let ?B = "fst (snd(unit p))"
2398   let ?d = "snd (snd (unit p))"
2399   let ?js = "[1..?d]"
2400   let ?mq = "minusinf ?q"
2401   let ?smq = "simpfm ?mq"
2402   let ?md = "evaldjf (\<lambda>j. simpfm (subst0 (C j) ?smq)) ?js"
2403   fix i
2404   let ?N = "\<lambda>t. Inum (i#bs) t"
2405   let ?Bjs = "[(b,j). b\<leftarrow>?B,j\<leftarrow>?js]"
2406   let ?qd = "evaldjf (\<lambda>(b,j). simpfm (subst0 (Add b (C j)) ?q)) ?Bjs"
2407   have qbf:"unit p = (?q,?B,?d)" by simp
2408   from unit[OF qf qbf]
2409   have pq_ex: "(\<exists>(x::int). ?I x p) \<longleftrightarrow> (\<exists>(x::int). ?I x ?q)"
2410     and B: "?N ` set ?B = ?N ` set (\<beta> ?q)"
2411     and uq: "d_\<beta> ?q 1"
2412     and dd: "d_\<delta> ?q ?d"
2413     and dp: "?d > 0"
2414     and lq: "iszlfm ?q"
2415     and Bn: "\<forall>b\<in> set ?B. numbound0 b"
2416     by auto
2417   from zlin_qfree[OF lq] have qfq: "qfree ?q" .
2418   from simpfm_qf[OF minusinf_qfree[OF qfq]] have qfmq: "qfree ?smq" .
2419   have jsnb: "\<forall>j \<in> set ?js. numbound0 (C j)"
2420     by simp
2421   then have "\<forall>j\<in> set ?js. bound0 (subst0 (C j) ?smq)"
2422     by (auto simp only: subst0_bound0[OF qfmq])
2423   then have th: "\<forall>j\<in> set ?js. bound0 (simpfm (subst0 (C j) ?smq))"
2424     by (auto simp add: simpfm_bound0)
2425   from evaldjf_bound0[OF th] have mdb: "bound0 ?md"
2426     by simp
2427   from Bn jsnb have "\<forall>(b,j) \<in> set ?Bjs. numbound0 (Add b (C j))"
2428     by simp
2429   then have "\<forall>(b,j) \<in> set ?Bjs. bound0 (subst0 (Add b (C j)) ?q)"
2430     using subst0_bound0[OF qfq] by blast
2431   then have "\<forall>(b,j) \<in> set ?Bjs. bound0 (simpfm (subst0 (Add b (C j)) ?q))"
2432     using simpfm_bound0 by blast
2433   then have th': "\<forall>x \<in> set ?Bjs. bound0 ((\<lambda>(b,j). simpfm (subst0 (Add b (C j)) ?q)) x)"
2434     by auto
2435   from evaldjf_bound0 [OF th'] have qdb: "bound0 ?qd"
2436     by simp
2437   from mdb qdb have mdqdb: "bound0 (disj ?md ?qd)"
2438     unfolding disj_def by (cases "?md = T \<or> ?qd = T") simp_all
2439   from trans [OF pq_ex cp_thm'[OF lq uq dd dp,where i="i"]] B
2440   have "?lhs \<longleftrightarrow> (\<exists>j \<in> {1.. ?d}. ?I j ?mq \<or> (\<exists>b \<in> ?N ` set ?B. Ifm bbs ((b + j) # bs) ?q))"
2441     by auto
2442   also have "\<dots> \<longleftrightarrow> (\<exists>j \<in> {1.. ?d}. ?I j ?mq \<or> (\<exists>b \<in> set ?B. Ifm bbs ((?N b + j) # bs) ?q))"
2443     by simp
2444   also have "\<dots> \<longleftrightarrow> (\<exists>j \<in> {1.. ?d}. ?I j ?mq ) \<or>
2445       (\<exists>j\<in> {1.. ?d}. \<exists>b \<in> set ?B. Ifm bbs ((?N (Add b (C j))) # bs) ?q)"
2446     by (simp only: Inum.simps) blast
2447   also have "\<dots> \<longleftrightarrow> (\<exists>j \<in> {1.. ?d}. ?I j ?smq) \<or>
2448       (\<exists>j \<in> {1.. ?d}. \<exists>b \<in> set ?B. Ifm bbs ((?N (Add b (C j))) # bs) ?q)"
2449     by (simp add: simpfm)
2450   also have "\<dots> \<longleftrightarrow> (\<exists>j\<in> set ?js. (\<lambda>j. ?I i (simpfm (subst0 (C j) ?smq))) j) \<or>
2451       (\<exists>j\<in> set ?js. \<exists>b\<in> set ?B. Ifm bbs ((?N (Add b (C j)))#bs) ?q)"
2452     by (simp only: simpfm subst0_I[OF qfmq] set_upto) auto
2453   also have "\<dots> \<longleftrightarrow> ?I i (evaldjf (\<lambda>j. simpfm (subst0 (C j) ?smq)) ?js) \<or>
2454       (\<exists>j\<in> set ?js. \<exists>b\<in> set ?B. ?I i (subst0 (Add b (C j)) ?q))"
2455     by (simp only: evaldjf_ex subst0_I[OF qfq])
2456   also have "\<dots> \<longleftrightarrow> ?I i ?md \<or>
2457       (\<exists>(b,j) \<in> set ?Bjs. (\<lambda>(b,j). ?I i (simpfm (subst0 (Add b (C j)) ?q))) (b,j))"
2458     by (simp only: simpfm set_concat set_map concat_map_singleton UN_simps) blast
2459   also have "\<dots> \<longleftrightarrow> ?I i ?md \<or> ?I i (evaldjf (\<lambda>(b,j). simpfm (subst0 (Add b (C j)) ?q)) ?Bjs)"
2460     by (simp only: evaldjf_ex[where bs="i#bs" and f="\<lambda>(b,j). simpfm (subst0 (Add b (C j)) ?q)" and ps="?Bjs"])
2461       (auto simp add: split_def)
2462   finally have mdqd: "?lhs \<longleftrightarrow> ?I i ?md \<or> ?I i ?qd"
2463     by simp
2464   also have "\<dots> \<longleftrightarrow> ?I i (disj ?md ?qd)"
2465     by (simp add: disj)
2466   also have "\<dots> \<longleftrightarrow> Ifm bbs bs (decr (disj ?md ?qd))"
2467     by (simp only: decr [OF mdqdb])
2468   finally have mdqd2: "?lhs \<longleftrightarrow> Ifm bbs bs (decr (disj ?md ?qd))" .
2469   {
2470     assume mdT: "?md = T"
2471     then have cT: "cooper p = T"
2472       by (simp only: cooper_def unit_def split_def Let_def if_True) simp
2473     from mdT have lhs: "?lhs"
2474       using mdqd by simp
2475     from mdT have "?rhs"
2476       by (simp add: cooper_def unit_def split_def)
2477     with lhs cT have ?thesis
2478       by simp
2479   }
2480   moreover
2481   {
2482     assume mdT: "?md \<noteq> T"
2483     then have "cooper p = decr (disj ?md ?qd)"
2484       by (simp only: cooper_def unit_def split_def Let_def if_False)
2485     with mdqd2 decr_qf[OF mdqdb] have ?thesis
2486       by simp
2487   }
2488   ultimately show ?thesis by blast
2489 qed
2491 definition pa :: "fm \<Rightarrow> fm"
2492   where "pa p = qelim (prep p) cooper"
2494 theorem mirqe: "Ifm bbs bs (pa p) = Ifm bbs bs p \<and> qfree (pa p)"
2495   using qelim_ci cooper prep by (auto simp add: pa_def)
2497 definition cooper_test :: "unit \<Rightarrow> fm"
2498   where
2499     "cooper_test u =
2500       pa (E (A (Imp (Ge (Sub (Bound 0) (Bound 1)))
2501         (E (E (Eq (Sub (Add (Mul 3 (Bound 1)) (Mul 5 (Bound 0))) (Bound 2))))))))"
2503 ML_val {* @{code cooper_test} () *}
2505 (*code_reflect Cooper_Procedure
2506   functions pa T Bound nat_of_integer integer_of_nat int_of_integer integer_of_int
2507   file "~~/src/HOL/Tools/Qelim/cooper_procedure.ML"*)
2509 oracle linzqe_oracle = {*
2510 let
2512 fun num_of_term vs (t as Free (xn, xT)) =
2513       (case AList.lookup (op =) vs t of
2514         NONE => error "Variable not found in the list!"
2515       | SOME n => @{code Bound} (@{code nat_of_integer} n))
2516   | num_of_term vs @{term "0::int"} = @{code C} (@{code int_of_integer} 0)
2517   | num_of_term vs @{term "1::int"} = @{code C} (@{code int_of_integer} 1)
2518   | num_of_term vs @{term "- 1::int"} = @{code C} (@{code int_of_integer} (~ 1))
2519   | num_of_term vs (@{term "numeral :: _ \<Rightarrow> int"} \$ t) =
2520       @{code C} (@{code int_of_integer} (HOLogic.dest_num t))
2521   | num_of_term vs (@{term "- numeral :: _ \<Rightarrow> int"} \$ t) =
2522       @{code C} (@{code int_of_integer} (~(HOLogic.dest_num t)))
2523   | num_of_term vs (Bound i) = @{code Bound} (@{code nat_of_integer} i)
2524   | num_of_term vs (@{term "uminus :: int \<Rightarrow> int"} \$ t') = @{code Neg} (num_of_term vs t')
2525   | num_of_term vs (@{term "op + :: int \<Rightarrow> int \<Rightarrow> int"} \$ t1 \$ t2) =
2526       @{code Add} (num_of_term vs t1, num_of_term vs t2)
2527   | num_of_term vs (@{term "op - :: int \<Rightarrow> int \<Rightarrow> int"} \$ t1 \$ t2) =
2528       @{code Sub} (num_of_term vs t1, num_of_term vs t2)
2529   | num_of_term vs (@{term "op * :: int \<Rightarrow> int \<Rightarrow> int"} \$ t1 \$ t2) =
2530       (case try HOLogic.dest_number t1 of
2531         SOME (_, i) => @{code Mul} (@{code int_of_integer} i, num_of_term vs t2)
2532       | NONE =>
2533           (case try HOLogic.dest_number t2 of
2534             SOME (_, i) => @{code Mul} (@{code int_of_integer} i, num_of_term vs t1)
2535           | NONE => error "num_of_term: unsupported multiplication"))
2536   | num_of_term vs t = error ("num_of_term: unknown term " ^ Syntax.string_of_term @{context} t);
2538 fun fm_of_term ps vs @{term True} = @{code T}
2539   | fm_of_term ps vs @{term False} = @{code F}
2540   | fm_of_term ps vs (@{term "op < :: int \<Rightarrow> int \<Rightarrow> bool"} \$ t1 \$ t2) =
2541       @{code Lt} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
2542   | fm_of_term ps vs (@{term "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"} \$ t1 \$ t2) =
2543       @{code Le} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
2544   | fm_of_term ps vs (@{term "op = :: int \<Rightarrow> int \<Rightarrow> bool"} \$ t1 \$ t2) =
2545       @{code Eq} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
2546   | fm_of_term ps vs (@{term "op dvd :: int \<Rightarrow> int \<Rightarrow> bool"} \$ t1 \$ t2) =
2547       (case try HOLogic.dest_number t1 of
2548         SOME (_, i) => @{code Dvd} (@{code int_of_integer} i, num_of_term vs t2)
2549       | NONE => error "num_of_term: unsupported dvd")
2550   | fm_of_term ps vs (@{term "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"} \$ t1 \$ t2) =
2551       @{code Iff} (fm_of_term ps vs t1, fm_of_term ps vs t2)
2552   | fm_of_term ps vs (@{term HOL.conj} \$ t1 \$ t2) =
2553       @{code And} (fm_of_term ps vs t1, fm_of_term ps vs t2)
2554   | fm_of_term ps vs (@{term HOL.disj} \$ t1 \$ t2) =
2555       @{code Or} (fm_of_term ps vs t1, fm_of_term ps vs t2)
2556   | fm_of_term ps vs (@{term HOL.implies} \$ t1 \$ t2) =
2557       @{code Imp} (fm_of_term ps vs t1, fm_of_term ps vs t2)
2558   | fm_of_term ps vs (@{term "Not"} \$ t') =
2559       @{code NOT} (fm_of_term ps vs t')
2560   | fm_of_term ps vs (Const (@{const_name Ex}, _) \$ Abs (xn, xT, p)) =
2561       let
2562         val (xn', p') = Syntax_Trans.variant_abs (xn, xT, p);  (* FIXME !? *)
2563         val vs' = (Free (xn', xT), 0) :: map (fn (v, n) => (v, n + 1)) vs;
2564       in @{code E} (fm_of_term ps vs' p) end
2565   | fm_of_term ps vs (Const (@{const_name All}, _) \$ Abs (xn, xT, p)) =
2566       let
2567         val (xn', p') = Syntax_Trans.variant_abs (xn, xT, p);  (* FIXME !? *)
2568         val vs' = (Free (xn', xT), 0) :: map (fn (v, n) => (v, n + 1)) vs;
2569       in @{code A} (fm_of_term ps vs' p) end
2570   | fm_of_term ps vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term @{context} t);
2572 fun term_of_num vs (@{code C} i) = HOLogic.mk_number HOLogic.intT (@{code integer_of_int} i)
2573   | term_of_num vs (@{code Bound} n) =
2574       let
2575         val q = @{code integer_of_nat} n
2576       in fst (the (find_first (fn (_, m) => q = m) vs)) end
2577   | term_of_num vs (@{code Neg} t') = @{term "uminus :: int \<Rightarrow> int"} \$ term_of_num vs t'
2578   | term_of_num vs (@{code Add} (t1, t2)) = @{term "op + :: int \<Rightarrow> int \<Rightarrow> int"} \$
2579       term_of_num vs t1 \$ term_of_num vs t2
2580   | term_of_num vs (@{code Sub} (t1, t2)) = @{term "op - :: int \<Rightarrow> int \<Rightarrow> int"} \$
2581       term_of_num vs t1 \$ term_of_num vs t2
2582   | term_of_num vs (@{code Mul} (i, t2)) = @{term "op * :: int \<Rightarrow> int \<Rightarrow> int"} \$
2583       term_of_num vs (@{code C} i) \$ term_of_num vs t2
2584   | term_of_num vs (@{code CN} (n, i, t)) =
2585       term_of_num vs (@{code Add} (@{code Mul} (i, @{code Bound} n), t));
2587 fun term_of_fm ps vs @{code T} = @{term True}
2588   | term_of_fm ps vs @{code F} = @{term False}
2589   | term_of_fm ps vs (@{code Lt} t) =
2590       @{term "op < :: int \<Rightarrow> int \<Rightarrow> bool"} \$ term_of_num vs t \$ @{term "0::int"}
2591   | term_of_fm ps vs (@{code Le} t) =
2592       @{term "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"} \$ term_of_num vs t \$ @{term "0::int"}
2593   | term_of_fm ps vs (@{code Gt} t) =
2594       @{term "op < :: int \<Rightarrow> int \<Rightarrow> bool"} \$ @{term "0::int"} \$ term_of_num vs t
2595   | term_of_fm ps vs (@{code Ge} t) =
2596       @{term "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"} \$ @{term "0::int"} \$ term_of_num vs t
2597   | term_of_fm ps vs (@{code Eq} t) =
2598       @{term "op = :: int \<Rightarrow> int \<Rightarrow> bool"} \$ term_of_num vs t \$ @{term "0::int"}
2599   | term_of_fm ps vs (@{code NEq} t) =
2600       term_of_fm ps vs (@{code NOT} (@{code Eq} t))
2601   | term_of_fm ps vs (@{code Dvd} (i, t)) =
2602       @{term "op dvd :: int \<Rightarrow> int \<Rightarrow> bool"} \$ term_of_num vs (@{code C} i) \$ term_of_num vs t
2603   | term_of_fm ps vs (@{code NDvd} (i, t)) =
2604       term_of_fm ps vs (@{code NOT} (@{code Dvd} (i, t)))
2605   | term_of_fm ps vs (@{code NOT} t') =
2606       HOLogic.Not \$ term_of_fm ps vs t'
2607   | term_of_fm ps vs (@{code And} (t1, t2)) =
2608       HOLogic.conj \$ term_of_fm ps vs t1 \$ term_of_fm ps vs t2
2609   | term_of_fm ps vs (@{code Or} (t1, t2)) =
2610       HOLogic.disj \$ term_of_fm ps vs t1 \$ term_of_fm ps vs t2
2611   | term_of_fm ps vs (@{code Imp} (t1, t2)) =
2612       HOLogic.imp \$ term_of_fm ps vs t1 \$ term_of_fm ps vs t2
2613   | term_of_fm ps vs (@{code Iff} (t1, t2)) =
2614       @{term "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"} \$ term_of_fm ps vs t1 \$ term_of_fm ps vs t2
2615   | term_of_fm ps vs (@{code Closed} n) =
2616       let
2617         val q = @{code integer_of_nat} n
2618       in (fst o the) (find_first (fn (_, m) => m = q) ps) end
2619   | term_of_fm ps vs (@{code NClosed} n) = term_of_fm ps vs (@{code NOT} (@{code Closed} n));
2621 fun term_bools acc t =
2622   let
2623     val is_op =
2624       member (op =) [@{term HOL.conj}, @{term HOL.disj}, @{term HOL.implies},
2625       @{term "op = :: bool => _"},
2626       @{term "op = :: int => _"}, @{term "op < :: int => _"},
2627       @{term "op <= :: int => _"}, @{term "Not"}, @{term "All :: (int => _) => _"},
2628       @{term "Ex :: (int => _) => _"}, @{term "True"}, @{term "False"}]
2629     fun is_ty t = not (fastype_of t = HOLogic.boolT)
2630   in
2631     (case t of
2632       (l as f \$ a) \$ b =>
2633         if is_ty t orelse is_op t then term_bools (term_bools acc l) b
2634         else insert (op aconv) t acc
2635     | f \$ a =>
2636         if is_ty t orelse is_op t then term_bools (term_bools acc f) a
2637         else insert (op aconv) t acc
2638     | Abs p => term_bools acc (snd (Syntax_Trans.variant_abs p))  (* FIXME !? *)
2639     | _ => if is_ty t orelse is_op t then acc else insert (op aconv) t acc)
2640   end;
2642 in
2643   fn ct =>
2644     let
2645       val thy = Thm.theory_of_cterm ct;
2646       val t = Thm.term_of ct;
2647       val fs = Misc_Legacy.term_frees t;
2648       val bs = term_bools [] t;
2649       val vs = map_index swap fs;
2650       val ps = map_index swap bs;
2651       val t' = (term_of_fm ps vs o @{code pa} o fm_of_term ps vs) t;
2652     in Thm.cterm_of thy (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, t'))) end
2653 end;
2654 *}
2656 ML_file "cooper_tac.ML"
2658 method_setup cooper = {*
2659   Scan.lift (Args.mode "no_quantify") >>
2660     (fn q => fn ctxt => SIMPLE_METHOD' (Cooper_Tac.linz_tac ctxt (not q)))
2661 *} "decision procedure for linear integer arithmetic"
2664 text {* Tests *}
2666 lemma "\<exists>(j::int). \<forall>x\<ge>j. \<exists>a b. x = 3*a+5*b"
2667   by cooper
2669 lemma "\<forall>(x::int) \<ge> 8. \<exists>i j. 5*i + 3*j = x"
2670   by cooper
2672 theorem "(\<forall>(y::int). 3 dvd y) \<Longrightarrow> \<forall>(x::int). b < x \<longrightarrow> a \<le> x"
2673   by cooper
2675 theorem "\<And>(y::int) (z::int) (n::int). 3 dvd z \<Longrightarrow> 2 dvd (y::int) \<Longrightarrow>
2676     (\<exists>(x::int). 2*x = y) \<and> (\<exists>(k::int). 3*k = z)"
2677   by cooper
2679 theorem "\<And>(y::int) (z::int) n. Suc n < 6 \<Longrightarrow> 3 dvd z \<Longrightarrow>
2680     2 dvd (y::int) \<Longrightarrow> (\<exists>(x::int).  2*x = y) \<and> (\<exists>(k::int). 3*k = z)"
2681   by cooper
2683 theorem "\<forall>(x::nat). \<exists>(y::nat). (0::nat) \<le> 5 \<longrightarrow> y = 5 + x"
2684   by cooper
2686 lemma "\<forall>(x::int) \<ge> 8. \<exists>i j. 5*i + 3*j = x"
2687   by cooper
2689 lemma "\<forall>(y::int) (z::int) (n::int).
2690     3 dvd z \<longrightarrow> 2 dvd (y::int) \<longrightarrow> (\<exists>(x::int). 2*x = y) \<and> (\<exists>(k::int). 3*k = z)"
2691   by cooper
2693 lemma "\<forall>(x::int) y. x < y \<longrightarrow> 2 * x + 1 < 2 * y"
2694   by cooper
2696 lemma "\<forall>(x::int) y. 2 * x + 1 \<noteq> 2 * y"
2697   by cooper
2699 lemma "\<exists>(x::int) y. 0 < x \<and> 0 \<le> y \<and> 3 * x - 5 * y = 1"
2700   by cooper
2702 lemma "\<not> (\<exists>(x::int) (y::int) (z::int). 4*x + (-6::int)*y = 1)"
2703   by cooper
2705 lemma "\<forall>(x::int). 2 dvd x \<longrightarrow> (\<exists>(y::int). x = 2*y)"
2706   by cooper
2708 lemma "\<forall>(x::int). 2 dvd x \<longleftrightarrow> (\<exists>(y::int). x = 2*y)"
2709   by cooper
2711 lemma "\<forall>(x::int). 2 dvd x \<longleftrightarrow> (\<forall>(y::int). x \<noteq> 2*y + 1)"
2712   by cooper
2714 lemma "\<not> (\<forall>(x::int).
2715     (2 dvd x \<longleftrightarrow> (\<forall>(y::int). x \<noteq> 2*y+1) \<or>
2716       (\<exists>(q::int) (u::int) i. 3*i + 2*q - u < 17) \<longrightarrow> 0 < x \<or> (\<not> 3 dvd x \<and> x + 8 = 0)))"
2717   by cooper
2719 lemma "\<not> (\<forall>(i::int). 4 \<le> i \<longrightarrow> (\<exists>x y. 0 \<le> x \<and> 0 \<le> y \<and> 3 * x + 5 * y = i))"
2720   by cooper
2722 lemma "\<exists>j. \<forall>(x::int) \<ge> j. \<exists>i j. 5*i + 3*j = x"
2723   by cooper
2725 theorem "(\<forall>(y::int). 3 dvd y) \<Longrightarrow> \<forall>(x::int). b < x \<longrightarrow> a \<le> x"
2726   by cooper
2728 theorem "\<And>(y::int) (z::int) (n::int). 3 dvd z \<Longrightarrow> 2 dvd (y::int) \<Longrightarrow>
2729   (\<exists>(x::int). 2*x = y) \<and> (\<exists>(k::int). 3*k = z)"
2730   by cooper
2732 theorem "\<And>(y::int) (z::int) n. Suc n < 6 \<Longrightarrow> 3 dvd z \<Longrightarrow>
2733     2 dvd (y::int) \<Longrightarrow> (\<exists>(x::int). 2*x = y) \<and> (\<exists>(k::int). 3*k = z)"
2734   by cooper
2736 theorem "\<forall>(x::nat). \<exists>(y::nat). (0::nat) \<le> 5 \<longrightarrow> y = 5 + x"
2737   by cooper
2739 theorem "\<forall>(x::nat). \<exists>(y::nat). y = 5 + x \<or> x div 6 + 1 = 2"
2740   by cooper
2742 theorem "\<exists>(x::int). 0 < x"
2743   by cooper
2745 theorem "\<forall>(x::int) y. x < y \<longrightarrow> 2 * x + 1 < 2 * y"
2746   by cooper
2748 theorem "\<forall>(x::int) y. 2 * x + 1 \<noteq> 2 * y"
2749   by cooper
2751 theorem "\<exists>(x::int) y. 0 < x  & 0 \<le> y  & 3 * x - 5 * y = 1"
2752   by cooper
2754 theorem "\<not> (\<exists>(x::int) (y::int) (z::int). 4*x + (-6::int)*y = 1)"
2755   by cooper
2757 theorem "\<not> (\<exists>(x::int). False)"
2758   by cooper
2760 theorem "\<forall>(x::int). 2 dvd x \<longrightarrow> (\<exists>(y::int). x = 2*y)"
2761   by cooper
2763 theorem "\<forall>(x::int). 2 dvd x \<longrightarrow> (\<exists>(y::int). x = 2*y)"
2764   by cooper
2766 theorem "\<forall>(x::int). 2 dvd x \<longleftrightarrow> (\<exists>(y::int). x = 2*y)"
2767   by cooper
2769 theorem "\<forall>(x::int). 2 dvd x \<longleftrightarrow> (\<forall>(y::int). x \<noteq> 2*y + 1)"
2770   by cooper
2772 theorem
2773   "\<not> (\<forall>(x::int).
2774     (2 dvd x \<longleftrightarrow>
2775       (\<forall>(y::int). x \<noteq> 2*y+1) \<or>
2776       (\<exists>(q::int) (u::int) i. 3*i + 2*q - u < 17)
2777        \<longrightarrow> 0 < x \<or> (\<not> 3 dvd x \<and> x + 8 = 0)))"
2778   by cooper
2780 theorem "\<not> (\<forall>(i::int). 4 \<le> i \<longrightarrow> (\<exists>x y. 0 \<le> x \<and> 0 \<le> y \<and> 3 * x + 5 * y = i))"
2781   by cooper
2783 theorem "\<forall>(i::int). 8 \<le> i \<longrightarrow> (\<exists>x y. 0 \<le> x \<and> 0 \<le> y \<and> 3 * x + 5 * y = i)"
2784   by cooper
2786 theorem "\<exists>(j::int). \<forall>i. j \<le> i \<longrightarrow> (\<exists>x y. 0 \<le> x \<and> 0 \<le> y \<and> 3 * x + 5 * y = i)"
2787   by cooper
2789 theorem "\<not> (\<forall>j (i::int). j \<le> i \<longrightarrow> (\<exists>x y. 0 \<le> x \<and> 0 \<le> y \<and> 3 * x + 5 * y = i))"
2790   by cooper
2792 theorem "(\<exists>m::nat. n = 2 * m) \<longrightarrow> (n + 1) div 2 = n div 2"
2793   by cooper
2795 end