src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
 author wenzelm Wed Feb 26 17:12:07 2014 +0100 (2014-02-26) changeset 55768 72c6ce5aea2a parent 55754 d14072d53c1e child 56410 a14831ac3023 permissions -rw-r--r--
tuned specifications and proofs;
1 (*  Title:      HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
2     Author:     Amine Chaieb
3 *)
5 header{* A formalization of Ferrante and Rackoff's procedure with polynomial parameters, see Paper in CALCULEMUS 2008 *}
7 theory Parametric_Ferrante_Rackoff
8 imports
9   Reflected_Multivariate_Polynomial
10   Dense_Linear_Order
11   DP_Library
12   "~~/src/HOL/Library/Code_Target_Numeral"
13   "~~/src/HOL/Library/Old_Recdef"
14 begin
16 subsection {* Terms *}
18 datatype tm = CP poly | Bound nat | Add tm tm | Mul poly tm
19   | Neg tm | Sub tm tm | CNP nat poly tm
21 (* A size for poly to make inductive proofs simpler*)
22 primrec tmsize :: "tm \<Rightarrow> nat"
23 where
24   "tmsize (CP c) = polysize c"
25 | "tmsize (Bound n) = 1"
26 | "tmsize (Neg a) = 1 + tmsize a"
27 | "tmsize (Add a b) = 1 + tmsize a + tmsize b"
28 | "tmsize (Sub a b) = 3 + tmsize a + tmsize b"
29 | "tmsize (Mul c a) = 1 + polysize c + tmsize a"
30 | "tmsize (CNP n c a) = 3 + polysize c + tmsize a "
32 (* Semantics of terms tm *)
33 primrec Itm :: "'a::{field_char_0, field_inverse_zero} list \<Rightarrow> 'a list \<Rightarrow> tm \<Rightarrow> 'a"
34 where
35   "Itm vs bs (CP c) = (Ipoly vs c)"
36 | "Itm vs bs (Bound n) = bs!n"
37 | "Itm vs bs (Neg a) = -(Itm vs bs a)"
38 | "Itm vs bs (Add a b) = Itm vs bs a + Itm vs bs b"
39 | "Itm vs bs (Sub a b) = Itm vs bs a - Itm vs bs b"
40 | "Itm vs bs (Mul c a) = (Ipoly vs c) * Itm vs bs a"
41 | "Itm vs bs (CNP n c t) = (Ipoly vs c)*(bs!n) + Itm vs bs t"
43 fun allpolys :: "(poly \<Rightarrow> bool) \<Rightarrow> tm \<Rightarrow> bool"
44 where
45   "allpolys P (CP c) = P c"
46 | "allpolys P (CNP n c p) = (P c \<and> allpolys P p)"
47 | "allpolys P (Mul c p) = (P c \<and> allpolys P p)"
48 | "allpolys P (Neg p) = allpolys P p"
49 | "allpolys P (Add p q) = (allpolys P p \<and> allpolys P q)"
50 | "allpolys P (Sub p q) = (allpolys P p \<and> allpolys P q)"
51 | "allpolys P p = True"
53 primrec tmboundslt :: "nat \<Rightarrow> tm \<Rightarrow> bool"
54 where
55   "tmboundslt n (CP c) = True"
56 | "tmboundslt n (Bound m) = (m < n)"
57 | "tmboundslt n (CNP m c a) = (m < n \<and> tmboundslt n a)"
58 | "tmboundslt n (Neg a) = tmboundslt n a"
59 | "tmboundslt n (Add a b) = (tmboundslt n a \<and> tmboundslt n b)"
60 | "tmboundslt n (Sub a b) = (tmboundslt n a \<and> tmboundslt n b)"
61 | "tmboundslt n (Mul i a) = tmboundslt n a"
63 primrec tmbound0 :: "tm \<Rightarrow> bool" (* a tm is INDEPENDENT of Bound 0 *)
64 where
65   "tmbound0 (CP c) = True"
66 | "tmbound0 (Bound n) = (n>0)"
67 | "tmbound0 (CNP n c a) = (n\<noteq>0 \<and> tmbound0 a)"
68 | "tmbound0 (Neg a) = tmbound0 a"
69 | "tmbound0 (Add a b) = (tmbound0 a \<and> tmbound0 b)"
70 | "tmbound0 (Sub a b) = (tmbound0 a \<and> tmbound0 b)"
71 | "tmbound0 (Mul i a) = tmbound0 a"
73 lemma tmbound0_I:
74   assumes nb: "tmbound0 a"
75   shows "Itm vs (b#bs) a = Itm vs (b'#bs) a"
76   using nb
77   by (induct a rule: tm.induct,auto)
79 primrec tmbound :: "nat \<Rightarrow> tm \<Rightarrow> bool" (* a tm is INDEPENDENT of Bound n *)
80 where
81   "tmbound n (CP c) = True"
82 | "tmbound n (Bound m) = (n \<noteq> m)"
83 | "tmbound n (CNP m c a) = (n\<noteq>m \<and> tmbound n a)"
84 | "tmbound n (Neg a) = tmbound n a"
85 | "tmbound n (Add a b) = (tmbound n a \<and> tmbound n b)"
86 | "tmbound n (Sub a b) = (tmbound n a \<and> tmbound n b)"
87 | "tmbound n (Mul i a) = tmbound n a"
89 lemma tmbound0_tmbound_iff: "tmbound 0 t = tmbound0 t"
90   by (induct t) auto
92 lemma tmbound_I:
93   assumes bnd: "tmboundslt (length bs) t"
94     and nb: "tmbound n t"
95     and le: "n \<le> length bs"
96   shows "Itm vs (bs[n:=x]) t = Itm vs bs t"
97   using nb le bnd
98   by (induct t rule: tm.induct) auto
100 fun decrtm0 :: "tm \<Rightarrow> tm"
101 where
102   "decrtm0 (Bound n) = Bound (n - 1)"
103 | "decrtm0 (Neg a) = Neg (decrtm0 a)"
104 | "decrtm0 (Add a b) = Add (decrtm0 a) (decrtm0 b)"
105 | "decrtm0 (Sub a b) = Sub (decrtm0 a) (decrtm0 b)"
106 | "decrtm0 (Mul c a) = Mul c (decrtm0 a)"
107 | "decrtm0 (CNP n c a) = CNP (n - 1) c (decrtm0 a)"
108 | "decrtm0 a = a"
110 fun incrtm0 :: "tm \<Rightarrow> tm"
111 where
112   "incrtm0 (Bound n) = Bound (n + 1)"
113 | "incrtm0 (Neg a) = Neg (incrtm0 a)"
114 | "incrtm0 (Add a b) = Add (incrtm0 a) (incrtm0 b)"
115 | "incrtm0 (Sub a b) = Sub (incrtm0 a) (incrtm0 b)"
116 | "incrtm0 (Mul c a) = Mul c (incrtm0 a)"
117 | "incrtm0 (CNP n c a) = CNP (n + 1) c (incrtm0 a)"
118 | "incrtm0 a = a"
120 lemma decrtm0:
121   assumes nb: "tmbound0 t"
122   shows "Itm vs (x # bs) t = Itm vs bs (decrtm0 t)"
123   using nb by (induct t rule: decrtm0.induct) simp_all
125 lemma incrtm0: "Itm vs (x#bs) (incrtm0 t) = Itm vs bs t"
126   by (induct t rule: decrtm0.induct) simp_all
128 primrec decrtm :: "nat \<Rightarrow> tm \<Rightarrow> tm"
129 where
130   "decrtm m (CP c) = (CP c)"
131 | "decrtm m (Bound n) = (if n < m then Bound n else Bound (n - 1))"
132 | "decrtm m (Neg a) = Neg (decrtm m a)"
133 | "decrtm m (Add a b) = Add (decrtm m a) (decrtm m b)"
134 | "decrtm m (Sub a b) = Sub (decrtm m a) (decrtm m b)"
135 | "decrtm m (Mul c a) = Mul c (decrtm m a)"
136 | "decrtm m (CNP n c a) = (if n < m then CNP n c (decrtm m a) else CNP (n - 1) c (decrtm m a))"
138 primrec removen :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
139 where
140   "removen n [] = []"
141 | "removen n (x#xs) = (if n=0 then xs else (x#(removen (n - 1) xs)))"
143 lemma removen_same: "n \<ge> length xs \<Longrightarrow> removen n xs = xs"
144   by (induct xs arbitrary: n) auto
146 lemma nth_length_exceeds: "n \<ge> length xs \<Longrightarrow> xs!n = []!(n - length xs)"
147   by (induct xs arbitrary: n) auto
149 lemma removen_length:
150   "length (removen n xs) = (if n \<ge> length xs then length xs else length xs - 1)"
151   by (induct xs arbitrary: n, auto)
153 lemma removen_nth:
154   "(removen n xs)!m =
155     (if n \<ge> length xs then xs!m
156      else if m < n then xs!m
157      else if m \<le> length xs then xs!(Suc m)
158      else []!(m - (length xs - 1)))"
159 proof (induct xs arbitrary: n m)
160   case Nil
161   then show ?case by simp
162 next
163   case (Cons x xs n m)
164   {
165     assume nxs: "n \<ge> length (x#xs)"
166     then have ?case using removen_same[OF nxs] by simp
167   }
168   moreover
169   {
170     assume nxs: "\<not> (n \<ge> length (x#xs))"
171     {
172       assume mln: "m < n"
173       then have ?case using Cons by (cases m) auto
174     }
175     moreover
176     {
177       assume mln: "\<not> (m < n)"
178       {
179         assume mxs: "m \<le> length (x#xs)"
180         then have ?case using Cons by (cases m) auto
181       }
182       moreover
183       {
184         assume mxs: "\<not> (m \<le> length (x#xs))"
185         have th: "length (removen n (x#xs)) = length xs"
186           using removen_length[where n="n" and xs="x#xs"] nxs by simp
187         with mxs have mxs':"m \<ge> length (removen n (x#xs))"
188           by auto
189         then have "(removen n (x#xs))!m = [] ! (m - length xs)"
190           using th nth_length_exceeds[OF mxs'] by auto
191         then have th: "(removen n (x#xs))!m = [] ! (m - (length (x#xs) - 1))"
192           by auto
193         then have ?case
194           using nxs mln mxs by auto
195       }
196       ultimately have ?case by blast
197     }
198     ultimately have ?case by blast
199   }
200   ultimately show ?case by blast
201 qed
203 lemma decrtm:
204   assumes bnd: "tmboundslt (length bs) t"
205     and nb: "tmbound m t"
206     and nle: "m \<le> length bs"
207   shows "Itm vs (removen m bs) (decrtm m t) = Itm vs bs t"
208   using bnd nb nle by (induct t rule: tm.induct) (auto simp add: removen_nth)
210 primrec tmsubst0:: "tm \<Rightarrow> tm \<Rightarrow> tm"
211 where
212   "tmsubst0 t (CP c) = CP c"
213 | "tmsubst0 t (Bound n) = (if n=0 then t else Bound n)"
214 | "tmsubst0 t (CNP n c a) = (if n=0 then Add (Mul c t) (tmsubst0 t a) else CNP n c (tmsubst0 t a))"
215 | "tmsubst0 t (Neg a) = Neg (tmsubst0 t a)"
216 | "tmsubst0 t (Add a b) = Add (tmsubst0 t a) (tmsubst0 t b)"
217 | "tmsubst0 t (Sub a b) = Sub (tmsubst0 t a) (tmsubst0 t b)"
218 | "tmsubst0 t (Mul i a) = Mul i (tmsubst0 t a)"
220 lemma tmsubst0: "Itm vs (x#bs) (tmsubst0 t a) = Itm vs ((Itm vs (x#bs) t)#bs) a"
221   by (induct a rule: tm.induct) auto
223 lemma tmsubst0_nb: "tmbound0 t \<Longrightarrow> tmbound0 (tmsubst0 t a)"
224   by (induct a rule: tm.induct) auto
226 primrec tmsubst:: "nat \<Rightarrow> tm \<Rightarrow> tm \<Rightarrow> tm"
227 where
228   "tmsubst n t (CP c) = CP c"
229 | "tmsubst n t (Bound m) = (if n=m then t else Bound m)"
230 | "tmsubst n t (CNP m c a) =
231     (if n = m then Add (Mul c t) (tmsubst n t a) else CNP m c (tmsubst n t a))"
232 | "tmsubst n t (Neg a) = Neg (tmsubst n t a)"
233 | "tmsubst n t (Add a b) = Add (tmsubst n t a) (tmsubst n t b)"
234 | "tmsubst n t (Sub a b) = Sub (tmsubst n t a) (tmsubst n t b)"
235 | "tmsubst n t (Mul i a) = Mul i (tmsubst n t a)"
237 lemma tmsubst:
238   assumes nb: "tmboundslt (length bs) a"
239     and nlt: "n \<le> length bs"
240   shows "Itm vs bs (tmsubst n t a) = Itm vs (bs[n:= Itm vs bs t]) a"
241   using nb nlt
242   by (induct a rule: tm.induct) auto
244 lemma tmsubst_nb0:
245   assumes tnb: "tmbound0 t"
246   shows "tmbound0 (tmsubst 0 t a)"
247   using tnb
248   by (induct a rule: tm.induct) auto
250 lemma tmsubst_nb:
251   assumes tnb: "tmbound m t"
252   shows "tmbound m (tmsubst m t a)"
253   using tnb
254   by (induct a rule: tm.induct) auto
256 lemma incrtm0_tmbound: "tmbound n t \<Longrightarrow> tmbound (Suc n) (incrtm0 t)"
257   by (induct t) auto
259 (* Simplification *)
261 consts tmadd:: "tm \<times> tm \<Rightarrow> tm"
262 recdef tmadd "measure (\<lambda>(t,s). size t + size s)"
263   "tmadd (CNP n1 c1 r1,CNP n2 c2 r2) =
264     (if n1 = n2 then
265       let c = c1 +\<^sub>p c2
266       in if c = 0\<^sub>p then tmadd(r1,r2) else CNP n1 c (tmadd (r1, r2))
267     else if n1 \<le> n2 then (CNP n1 c1 (tmadd (r1,CNP n2 c2 r2)))
268     else (CNP n2 c2 (tmadd (CNP n1 c1 r1, r2))))"
269   "tmadd (CNP n1 c1 r1, t) = CNP n1 c1 (tmadd (r1, t))"
270   "tmadd (t, CNP n2 c2 r2) = CNP n2 c2 (tmadd (t, r2))"
271   "tmadd (CP b1, CP b2) = CP (b1 +\<^sub>p b2)"
276   apply (case_tac "c1 +\<^sub>p c2 = 0\<^sub>p",case_tac "n1 \<le> n2", simp_all)
277   apply (case_tac "n1 = n2", simp_all add: field_simps)
278   apply (simp only: distrib_left[symmetric])
280   done
282 lemma tmadd_nb0[simp]: "tmbound0 t \<Longrightarrow> tmbound0 s \<Longrightarrow> tmbound0 (tmadd (t, s))"
285 lemma tmadd_nb[simp]: "tmbound n t \<Longrightarrow> tmbound n s \<Longrightarrow> tmbound n (tmadd (t, s))"
288 lemma tmadd_blt[simp]: "tmboundslt n t \<Longrightarrow> tmboundslt n s \<Longrightarrow> tmboundslt n (tmadd (t, s))"
292   "allpolys isnpoly t \<Longrightarrow> allpolys isnpoly s \<Longrightarrow> allpolys isnpoly (tmadd(t, s))"
295 fun tmmul:: "tm \<Rightarrow> poly \<Rightarrow> tm"
296 where
297   "tmmul (CP j) = (\<lambda>i. CP (i *\<^sub>p j))"
298 | "tmmul (CNP n c a) = (\<lambda>i. CNP n (i *\<^sub>p c) (tmmul a i))"
299 | "tmmul t = (\<lambda>i. Mul i t)"
301 lemma tmmul[simp]: "Itm vs bs (tmmul t i) = Itm vs bs (Mul i t)"
302   by (induct t arbitrary: i rule: tmmul.induct) (simp_all add: field_simps)
304 lemma tmmul_nb0[simp]: "tmbound0 t \<Longrightarrow> tmbound0 (tmmul t i)"
305   by (induct t arbitrary: i rule: tmmul.induct) auto
307 lemma tmmul_nb[simp]: "tmbound n t \<Longrightarrow> tmbound n (tmmul t i)"
308   by (induct t arbitrary: n rule: tmmul.induct) auto
310 lemma tmmul_blt[simp]: "tmboundslt n t \<Longrightarrow> tmboundslt n (tmmul t i)"
311   by (induct t arbitrary: i rule: tmmul.induct) (auto simp add: Let_def)
313 lemma tmmul_allpolys_npoly[simp]:
314   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
315   shows "allpolys isnpoly t \<Longrightarrow> isnpoly c \<Longrightarrow> allpolys isnpoly (tmmul t c)"
316   by (induct t rule: tmmul.induct) (simp_all add: Let_def polymul_norm)
318 definition tmneg :: "tm \<Rightarrow> tm"
319   where "tmneg t \<equiv> tmmul t (C (- 1,1))"
321 definition tmsub :: "tm \<Rightarrow> tm \<Rightarrow> tm"
322   where "tmsub s t \<equiv> (if s = t then CP 0\<^sub>p else tmadd (s, tmneg t))"
324 lemma tmneg[simp]: "Itm vs bs (tmneg t) = Itm vs bs (Neg t)"
325   using tmneg_def[of t] by simp
327 lemma tmneg_nb0[simp]: "tmbound0 t \<Longrightarrow> tmbound0 (tmneg t)"
328   using tmneg_def by simp
330 lemma tmneg_nb[simp]: "tmbound n t \<Longrightarrow> tmbound n (tmneg t)"
331   using tmneg_def by simp
333 lemma tmneg_blt[simp]: "tmboundslt n t \<Longrightarrow> tmboundslt n (tmneg t)"
334   using tmneg_def by simp
336 lemma [simp]: "isnpoly (C (-1, 1))"
337   unfolding isnpoly_def by simp
339 lemma tmneg_allpolys_npoly[simp]:
340   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
341   shows "allpolys isnpoly t \<Longrightarrow> allpolys isnpoly (tmneg t)"
342   unfolding tmneg_def by auto
344 lemma tmsub[simp]: "Itm vs bs (tmsub a b) = Itm vs bs (Sub a b)"
345   using tmsub_def by simp
347 lemma tmsub_nb0[simp]: "tmbound0 t \<Longrightarrow> tmbound0 s \<Longrightarrow> tmbound0 (tmsub t s)"
348   using tmsub_def by simp
350 lemma tmsub_nb[simp]: "tmbound n t \<Longrightarrow> tmbound n s \<Longrightarrow> tmbound n (tmsub t s)"
351   using tmsub_def by simp
353 lemma tmsub_blt[simp]: "tmboundslt n t \<Longrightarrow> tmboundslt n s \<Longrightarrow> tmboundslt n (tmsub t s)"
354   using tmsub_def by simp
356 lemma tmsub_allpolys_npoly[simp]:
357   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
358   shows "allpolys isnpoly t \<Longrightarrow> allpolys isnpoly s \<Longrightarrow> allpolys isnpoly (tmsub t s)"
359   unfolding tmsub_def by (simp add: isnpoly_def)
361 fun simptm :: "tm \<Rightarrow> tm"
362 where
363   "simptm (CP j) = CP (polynate j)"
364 | "simptm (Bound n) = CNP n (1)\<^sub>p (CP 0\<^sub>p)"
365 | "simptm (Neg t) = tmneg (simptm t)"
367 | "simptm (Sub t s) = tmsub (simptm t) (simptm s)"
368 | "simptm (Mul i t) =
369     (let i' = polynate i in if i' = 0\<^sub>p then CP 0\<^sub>p else tmmul (simptm t) i')"
370 | "simptm (CNP n c t) =
371     (let c' = polynate c in if c' = 0\<^sub>p then simptm t else tmadd (CNP n c' (CP 0\<^sub>p ), simptm t))"
373 lemma polynate_stupid:
374   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
375   shows "polynate t = 0\<^sub>p \<Longrightarrow> Ipoly bs t = (0::'a)"
376   apply (subst polynate[symmetric])
377   apply simp
378   done
380 lemma simptm_ci[simp]: "Itm vs bs (simptm t) = Itm vs bs t"
381   by (induct t rule: simptm.induct) (auto simp add: Let_def polynate_stupid)
383 lemma simptm_tmbound0[simp]: "tmbound0 t \<Longrightarrow> tmbound0 (simptm t)"
384   by (induct t rule: simptm.induct) (auto simp add: Let_def)
386 lemma simptm_nb[simp]: "tmbound n t \<Longrightarrow> tmbound n (simptm t)"
387   by (induct t rule: simptm.induct) (auto simp add: Let_def)
389 lemma simptm_nlt[simp]: "tmboundslt n t \<Longrightarrow> tmboundslt n (simptm t)"
390   by (induct t rule: simptm.induct) (auto simp add: Let_def)
392 lemma [simp]: "isnpoly 0\<^sub>p"
393   and [simp]: "isnpoly (C(1,1))"
396 lemma simptm_allpolys_npoly[simp]:
397   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
398   shows "allpolys isnpoly (simptm p)"
399   by (induct p rule: simptm.induct) (auto simp add: Let_def)
401 declare let_cong[fundef_cong del]
403 fun split0 :: "tm \<Rightarrow> (poly \<times> tm)"
404 where
405   "split0 (Bound 0) = ((1)\<^sub>p, CP 0\<^sub>p)"
406 | "split0 (CNP 0 c t) = (let (c', t') = split0 t in (c +\<^sub>p c', t'))"
407 | "split0 (Neg t) = (let (c, t') = split0 t in (~\<^sub>p c, Neg t'))"
408 | "split0 (CNP n c t) = (let (c', t') = split0 t in (c', CNP n c t'))"
409 | "split0 (Add s t) = (let (c1, s') = split0 s; (c2, t') = split0 t in (c1 +\<^sub>p c2, Add s' t'))"
410 | "split0 (Sub s t) = (let (c1, s') = split0 s; (c2, t') = split0 t in (c1 -\<^sub>p c2, Sub s' t'))"
411 | "split0 (Mul c t) = (let (c', t') = split0 t in (c *\<^sub>p c', Mul c t'))"
412 | "split0 t = (0\<^sub>p, t)"
414 declare let_cong[fundef_cong]
416 lemma split0_stupid[simp]: "\<exists>x y. (x, y) = split0 p"
417   apply (rule exI[where x="fst (split0 p)"])
418   apply (rule exI[where x="snd (split0 p)"])
419   apply simp
420   done
422 lemma split0:
423   "tmbound 0 (snd (split0 t)) \<and> (Itm vs bs (CNP 0 (fst (split0 t)) (snd (split0 t))) = Itm vs bs t)"
424   apply (induct t rule: split0.induct)
425   apply simp
426   apply (simp add: Let_def split_def field_simps)
427   apply (simp add: Let_def split_def field_simps)
428   apply (simp add: Let_def split_def field_simps)
429   apply (simp add: Let_def split_def field_simps)
430   apply (simp add: Let_def split_def field_simps)
431   apply (simp add: Let_def split_def mult_assoc distrib_left[symmetric])
432   apply (simp add: Let_def split_def field_simps)
433   apply (simp add: Let_def split_def field_simps)
434   done
436 lemma split0_ci: "split0 t = (c',t') \<Longrightarrow> Itm vs bs t = Itm vs bs (CNP 0 c' t')"
437 proof -
438   fix c' t'
439   assume "split0 t = (c', t')"
440   then have "c' = fst (split0 t)" and "t' = snd (split0 t)"
441     by auto
442   with split0[where t="t" and bs="bs"]
443   show "Itm vs bs t = Itm vs bs (CNP 0 c' t')"
444     by simp
445 qed
447 lemma split0_nb0:
448   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
449   shows "split0 t = (c',t') \<Longrightarrow>  tmbound 0 t'"
450 proof -
451   fix c' t'
452   assume "split0 t = (c', t')"
453   then have "c' = fst (split0 t)" and "t' = snd (split0 t)"
454     by auto
455   with conjunct1[OF split0[where t="t"]] show "tmbound 0 t'"
456     by simp
457 qed
459 lemma split0_nb0'[simp]:
460   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
461   shows "tmbound0 (snd (split0 t))"
462   using split0_nb0[of t "fst (split0 t)" "snd (split0 t)"]
465 lemma split0_nb:
466   assumes nb: "tmbound n t"
467   shows "tmbound n (snd (split0 t))"
468   using nb by (induct t rule: split0.induct) (auto simp add: Let_def split_def)
470 lemma split0_blt:
471   assumes nb: "tmboundslt n t"
472   shows "tmboundslt n (snd (split0 t))"
473   using nb by (induct t rule: split0.induct) (auto simp add: Let_def split_def)
475 lemma tmbound_split0: "tmbound 0 t \<Longrightarrow> Ipoly vs (fst (split0 t)) = 0"
476   by (induct t rule: split0.induct) (auto simp add: Let_def split_def)
478 lemma tmboundslt_split0: "tmboundslt n t \<Longrightarrow> Ipoly vs (fst (split0 t)) = 0 \<or> n > 0"
479   by (induct t rule: split0.induct) (auto simp add: Let_def split_def)
481 lemma tmboundslt0_split0: "tmboundslt 0 t \<Longrightarrow> Ipoly vs (fst (split0 t)) = 0"
482   by (induct t rule: split0.induct) (auto simp add: Let_def split_def)
484 lemma allpolys_split0: "allpolys isnpoly p \<Longrightarrow> allpolys isnpoly (snd (split0 p))"
485   by (induct p rule: split0.induct) (auto simp  add: isnpoly_def Let_def split_def)
487 lemma isnpoly_fst_split0:
488   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
489   shows "allpolys isnpoly p \<Longrightarrow> isnpoly (fst (split0 p))"
490   by (induct p rule: split0.induct)
494 subsection{* Formulae *}
496 datatype fm  =  T| F| Le tm | Lt tm | Eq tm | NEq tm|
497   NOT fm| And fm fm|  Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm
500 (* A size for fm *)
501 fun fmsize :: "fm \<Rightarrow> nat"
502 where
503   "fmsize (NOT p) = 1 + fmsize p"
504 | "fmsize (And p q) = 1 + fmsize p + fmsize q"
505 | "fmsize (Or p q) = 1 + fmsize p + fmsize q"
506 | "fmsize (Imp p q) = 3 + fmsize p + fmsize q"
507 | "fmsize (Iff p q) = 3 + 2*(fmsize p + fmsize q)"
508 | "fmsize (E p) = 1 + fmsize p"
509 | "fmsize (A p) = 4+ fmsize p"
510 | "fmsize p = 1"
512 (* several lemmas about fmsize *)
513 lemma fmsize_pos[termination_simp]: "fmsize p > 0"
514   by (induct p rule: fmsize.induct) simp_all
516   (* Semantics of formulae (fm) *)
517 primrec Ifm ::"'a::{linordered_field_inverse_zero} list \<Rightarrow> 'a list \<Rightarrow> fm \<Rightarrow> bool"
518 where
519   "Ifm vs bs T = True"
520 | "Ifm vs bs F = False"
521 | "Ifm vs bs (Lt a) = (Itm vs bs a < 0)"
522 | "Ifm vs bs (Le a) = (Itm vs bs a \<le> 0)"
523 | "Ifm vs bs (Eq a) = (Itm vs bs a = 0)"
524 | "Ifm vs bs (NEq a) = (Itm vs bs a \<noteq> 0)"
525 | "Ifm vs bs (NOT p) = (\<not> (Ifm vs bs p))"
526 | "Ifm vs bs (And p q) = (Ifm vs bs p \<and> Ifm vs bs q)"
527 | "Ifm vs bs (Or p q) = (Ifm vs bs p \<or> Ifm vs bs q)"
528 | "Ifm vs bs (Imp p q) = ((Ifm vs bs p) \<longrightarrow> (Ifm vs bs q))"
529 | "Ifm vs bs (Iff p q) = (Ifm vs bs p = Ifm vs bs q)"
530 | "Ifm vs bs (E p) = (\<exists>x. Ifm vs (x#bs) p)"
531 | "Ifm vs bs (A p) = (\<forall>x. Ifm vs (x#bs) p)"
533 fun not:: "fm \<Rightarrow> fm"
534 where
535   "not (NOT (NOT p)) = not p"
536 | "not (NOT p) = p"
537 | "not T = F"
538 | "not F = T"
539 | "not (Lt t) = Le (tmneg t)"
540 | "not (Le t) = Lt (tmneg t)"
541 | "not (Eq t) = NEq t"
542 | "not (NEq t) = Eq t"
543 | "not p = NOT p"
545 lemma not[simp]: "Ifm vs bs (not p) = Ifm vs bs (NOT p)"
546   by (induct p rule: not.induct) auto
548 definition conj :: "fm \<Rightarrow> fm \<Rightarrow> fm"
549 where
550   "conj p q \<equiv>
551     (if p = F \<or> q = F then F
552      else if p = T then q
553      else if q = T then p
554      else if p = q then p
555      else And p q)"
557 lemma conj[simp]: "Ifm vs bs (conj p q) = Ifm vs bs (And p q)"
558   by (cases "p=F \<or> q=F", simp_all add: conj_def) (cases p, simp_all)
560 definition disj :: "fm \<Rightarrow> fm \<Rightarrow> fm"
561 where
562   "disj p q \<equiv>
563     (if (p = T \<or> q = T) then T
564      else if p = F then q
565      else if q = F then p
566      else if p = q then p
567      else Or p q)"
569 lemma disj[simp]: "Ifm vs bs (disj p q) = Ifm vs bs (Or p q)"
570   by (cases "p = T \<or> q = T", simp_all add: disj_def) (cases p, simp_all)
572 definition imp :: "fm \<Rightarrow> fm \<Rightarrow> fm"
573 where
574   "imp p q \<equiv>
575     (if p = F \<or> q = T \<or> p = q then T
576      else if p = T then q
577      else if q = F then not p
578      else Imp p q)"
580 lemma imp[simp]: "Ifm vs bs (imp p q) = Ifm vs bs (Imp p q)"
581   by (cases "p = F \<or> q = T") (simp_all add: imp_def)
583 definition iff :: "fm \<Rightarrow> fm \<Rightarrow> fm"
584 where
585   "iff p q \<equiv>
586    (if p = q then T
587     else if p = NOT q \<or> NOT p = q then F
588     else if p = F then not q
589     else if q = F then not p
590     else if p = T then q
591     else if q = T then p
592     else Iff p q)"
594 lemma iff[simp]: "Ifm vs bs (iff p q) = Ifm vs bs (Iff p q)"
595   by (unfold iff_def, cases "p = q", simp, cases "p = NOT q", simp) (cases "NOT p= q", auto)
597 (* Quantifier freeness *)
598 fun qfree:: "fm \<Rightarrow> bool"
599 where
600   "qfree (E p) = False"
601 | "qfree (A p) = False"
602 | "qfree (NOT p) = qfree p"
603 | "qfree (And p q) = (qfree p \<and> qfree q)"
604 | "qfree (Or  p q) = (qfree p \<and> qfree q)"
605 | "qfree (Imp p q) = (qfree p \<and> qfree q)"
606 | "qfree (Iff p q) = (qfree p \<and> qfree q)"
607 | "qfree p = True"
609 (* Boundedness and substitution *)
610 primrec boundslt :: "nat \<Rightarrow> fm \<Rightarrow> bool"
611 where
612   "boundslt n T = True"
613 | "boundslt n F = True"
614 | "boundslt n (Lt t) = tmboundslt n t"
615 | "boundslt n (Le t) = tmboundslt n t"
616 | "boundslt n (Eq t) = tmboundslt n t"
617 | "boundslt n (NEq t) = tmboundslt n t"
618 | "boundslt n (NOT p) = boundslt n p"
619 | "boundslt n (And p q) = (boundslt n p \<and> boundslt n q)"
620 | "boundslt n (Or p q) = (boundslt n p \<and> boundslt n q)"
621 | "boundslt n (Imp p q) = ((boundslt n p) \<and> (boundslt n q))"
622 | "boundslt n (Iff p q) = (boundslt n p \<and> boundslt n q)"
623 | "boundslt n (E p) = boundslt (Suc n) p"
624 | "boundslt n (A p) = boundslt (Suc n) p"
626 fun bound0:: "fm \<Rightarrow> bool" (* A Formula is independent of Bound 0 *)
627 where
628   "bound0 T = True"
629 | "bound0 F = True"
630 | "bound0 (Lt a) = tmbound0 a"
631 | "bound0 (Le a) = tmbound0 a"
632 | "bound0 (Eq a) = tmbound0 a"
633 | "bound0 (NEq a) = tmbound0 a"
634 | "bound0 (NOT p) = bound0 p"
635 | "bound0 (And p q) = (bound0 p \<and> bound0 q)"
636 | "bound0 (Or p q) = (bound0 p \<and> bound0 q)"
637 | "bound0 (Imp p q) = ((bound0 p) \<and> (bound0 q))"
638 | "bound0 (Iff p q) = (bound0 p \<and> bound0 q)"
639 | "bound0 p = False"
641 lemma bound0_I:
642   assumes bp: "bound0 p"
643   shows "Ifm vs (b#bs) p = Ifm vs (b'#bs) p"
644   using bp tmbound0_I[where b="b" and bs="bs" and b'="b'"]
645   by (induct p rule: bound0.induct) auto
647 primrec bound:: "nat \<Rightarrow> fm \<Rightarrow> bool" (* A Formula is independent of Bound n *)
648 where
649   "bound m T = True"
650 | "bound m F = True"
651 | "bound m (Lt t) = tmbound m t"
652 | "bound m (Le t) = tmbound m t"
653 | "bound m (Eq t) = tmbound m t"
654 | "bound m (NEq t) = tmbound m t"
655 | "bound m (NOT p) = bound m p"
656 | "bound m (And p q) = (bound m p \<and> bound m q)"
657 | "bound m (Or p q) = (bound m p \<and> bound m q)"
658 | "bound m (Imp p q) = ((bound m p) \<and> (bound m q))"
659 | "bound m (Iff p q) = (bound m p \<and> bound m q)"
660 | "bound m (E p) = bound (Suc m) p"
661 | "bound m (A p) = bound (Suc m) p"
663 lemma bound_I:
664   assumes bnd: "boundslt (length bs) p"
665     and nb: "bound n p"
666     and le: "n \<le> length bs"
667   shows "Ifm vs (bs[n:=x]) p = Ifm vs bs p"
668   using bnd nb le tmbound_I[where bs=bs and vs = vs]
669 proof (induct p arbitrary: bs n rule: fm.induct)
670   case (E p bs n)
671   {
672     fix y
673     from E have bnd: "boundslt (length (y#bs)) p"
674       and nb: "bound (Suc n) p" and le: "Suc n \<le> length (y#bs)" by simp+
675     from E.hyps[OF bnd nb le tmbound_I] have "Ifm vs ((y#bs)[Suc n:=x]) p = Ifm vs (y#bs) p" .
676   }
677   then show ?case by simp
678 next
679   case (A p bs n)
680   {
681     fix y
682     from A have bnd: "boundslt (length (y#bs)) p"
683       and nb: "bound (Suc n) p"
684       and le: "Suc n \<le> length (y#bs)"
685       by simp_all
686     from A.hyps[OF bnd nb le tmbound_I] have "Ifm vs ((y#bs)[Suc n:=x]) p = Ifm vs (y#bs) p" .
687   }
688   then show ?case by simp
689 qed auto
691 fun decr0 :: "fm \<Rightarrow> fm"
692 where
693   "decr0 (Lt a) = Lt (decrtm0 a)"
694 | "decr0 (Le a) = Le (decrtm0 a)"
695 | "decr0 (Eq a) = Eq (decrtm0 a)"
696 | "decr0 (NEq a) = NEq (decrtm0 a)"
697 | "decr0 (NOT p) = NOT (decr0 p)"
698 | "decr0 (And p q) = conj (decr0 p) (decr0 q)"
699 | "decr0 (Or p q) = disj (decr0 p) (decr0 q)"
700 | "decr0 (Imp p q) = imp (decr0 p) (decr0 q)"
701 | "decr0 (Iff p q) = iff (decr0 p) (decr0 q)"
702 | "decr0 p = p"
704 lemma decr0:
705   assumes nb: "bound0 p"
706   shows "Ifm vs (x#bs) p = Ifm vs bs (decr0 p)"
707   using nb
708   by (induct p rule: decr0.induct) (simp_all add: decrtm0)
710 primrec decr :: "nat \<Rightarrow> fm \<Rightarrow> fm"
711 where
712   "decr m T = T"
713 | "decr m F = F"
714 | "decr m (Lt t) = (Lt (decrtm m t))"
715 | "decr m (Le t) = (Le (decrtm m t))"
716 | "decr m (Eq t) = (Eq (decrtm m t))"
717 | "decr m (NEq t) = (NEq (decrtm m t))"
718 | "decr m (NOT p) = NOT (decr m p)"
719 | "decr m (And p q) = conj (decr m p) (decr m q)"
720 | "decr m (Or p q) = disj (decr m p) (decr m q)"
721 | "decr m (Imp p q) = imp (decr m p) (decr m q)"
722 | "decr m (Iff p q) = iff (decr m p) (decr m q)"
723 | "decr m (E p) = E (decr (Suc m) p)"
724 | "decr m (A p) = A (decr (Suc m) p)"
726 lemma decr:
727   assumes bnd: "boundslt (length bs) p"
728     and nb: "bound m p"
729     and nle: "m < length bs"
730   shows "Ifm vs (removen m bs) (decr m p) = Ifm vs bs p"
731   using bnd nb nle
732 proof (induct p arbitrary: bs m rule: fm.induct)
733   case (E p bs m)
734   { fix x
735     from E
736     have bnd: "boundslt (length (x#bs)) p"
737       and nb: "bound (Suc m) p"
738       and nle: "Suc m < length (x#bs)"
739       by auto
740     from E(1)[OF bnd nb nle]
741     have "Ifm vs (removen (Suc m) (x#bs)) (decr (Suc m) p) = Ifm vs (x#bs) p" .
742   }
743   then show ?case by auto
744 next
745   case (A p bs m)
746   { fix x
747     from A
748     have bnd: "boundslt (length (x#bs)) p"
749       and nb: "bound (Suc m) p"
750       and nle: "Suc m < length (x#bs)"
751       by auto
752     from A(1)[OF bnd nb nle]
753     have "Ifm vs (removen (Suc m) (x#bs)) (decr (Suc m) p) = Ifm vs (x#bs) p" .
754   }
755   then show ?case by auto
756 qed (auto simp add: decrtm removen_nth)
758 primrec subst0 :: "tm \<Rightarrow> fm \<Rightarrow> fm"
759 where
760   "subst0 t T = T"
761 | "subst0 t F = F"
762 | "subst0 t (Lt a) = Lt (tmsubst0 t a)"
763 | "subst0 t (Le a) = Le (tmsubst0 t a)"
764 | "subst0 t (Eq a) = Eq (tmsubst0 t a)"
765 | "subst0 t (NEq a) = NEq (tmsubst0 t a)"
766 | "subst0 t (NOT p) = NOT (subst0 t p)"
767 | "subst0 t (And p q) = And (subst0 t p) (subst0 t q)"
768 | "subst0 t (Or p q) = Or (subst0 t p) (subst0 t q)"
769 | "subst0 t (Imp p q) = Imp (subst0 t p)  (subst0 t q)"
770 | "subst0 t (Iff p q) = Iff (subst0 t p) (subst0 t q)"
771 | "subst0 t (E p) = E p"
772 | "subst0 t (A p) = A p"
774 lemma subst0:
775   assumes qf: "qfree p"
776   shows "Ifm vs (x # bs) (subst0 t p) = Ifm vs ((Itm vs (x # bs) t) # bs) p"
777   using qf tmsubst0[where x="x" and bs="bs" and t="t"]
778   by (induct p rule: fm.induct) auto
780 lemma subst0_nb:
781   assumes bp: "tmbound0 t"
782     and qf: "qfree p"
783   shows "bound0 (subst0 t p)"
784   using qf tmsubst0_nb[OF bp] bp
785   by (induct p rule: fm.induct) auto
787 primrec subst:: "nat \<Rightarrow> tm \<Rightarrow> fm \<Rightarrow> fm"
788 where
789   "subst n t T = T"
790 | "subst n t F = F"
791 | "subst n t (Lt a) = Lt (tmsubst n t a)"
792 | "subst n t (Le a) = Le (tmsubst n t a)"
793 | "subst n t (Eq a) = Eq (tmsubst n t a)"
794 | "subst n t (NEq a) = NEq (tmsubst n t a)"
795 | "subst n t (NOT p) = NOT (subst n t p)"
796 | "subst n t (And p q) = And (subst n t p) (subst n t q)"
797 | "subst n t (Or p q) = Or (subst n t p) (subst n t q)"
798 | "subst n t (Imp p q) = Imp (subst n t p)  (subst n t q)"
799 | "subst n t (Iff p q) = Iff (subst n t p) (subst n t q)"
800 | "subst n t (E p) = E (subst (Suc n) (incrtm0 t) p)"
801 | "subst n t (A p) = A (subst (Suc n) (incrtm0 t) p)"
803 lemma subst:
804   assumes nb: "boundslt (length bs) p"
805     and nlm: "n \<le> length bs"
806   shows "Ifm vs bs (subst n t p) = Ifm vs (bs[n:= Itm vs bs t]) p"
807   using nb nlm
808 proof (induct p arbitrary: bs n t rule: fm.induct)
809   case (E p bs n)
810   {
811     fix x
812     from E have bn: "boundslt (length (x#bs)) p"
813       by simp
814     from E have nlm: "Suc n \<le> length (x#bs)"
815       by simp
816     from E(1)[OF bn nlm]
817     have "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) =
818         Ifm vs ((x#bs)[Suc n:= Itm vs (x#bs) (incrtm0 t)]) p"
819       by simp
820     then have "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) =
821         Ifm vs (x#bs[n:= Itm vs bs t]) p"
822       by (simp add: incrtm0[where x="x" and bs="bs" and t="t"])
823   }
824   then show ?case by simp
825 next
826   case (A p bs n)
827   {
828     fix x
829     from A have bn: "boundslt (length (x#bs)) p"
830       by simp
831     from A have nlm: "Suc n \<le> length (x#bs)"
832       by simp
833     from A(1)[OF bn nlm]
834     have "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) =
835         Ifm vs ((x#bs)[Suc n:= Itm vs (x#bs) (incrtm0 t)]) p"
836       by simp
837     then have "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) =
838         Ifm vs (x#bs[n:= Itm vs bs t]) p"
839       by (simp add: incrtm0[where x="x" and bs="bs" and t="t"])
840   }
841   then show ?case by simp
842 qed (auto simp add: tmsubst)
844 lemma subst_nb:
845   assumes tnb: "tmbound m t"
846   shows "bound m (subst m t p)"
847   using tnb tmsubst_nb incrtm0_tmbound
848   by (induct p arbitrary: m t rule: fm.induct) auto
850 lemma not_qf[simp]: "qfree p \<Longrightarrow> qfree (not p)"
851   by (induct p rule: not.induct) auto
852 lemma not_bn0[simp]: "bound0 p \<Longrightarrow> bound0 (not p)"
853   by (induct p rule: not.induct) auto
854 lemma not_nb[simp]: "bound n p \<Longrightarrow> bound n (not p)"
855   by (induct p rule: not.induct) auto
856 lemma not_blt[simp]: "boundslt n p \<Longrightarrow> boundslt n (not p)"
857   by (induct p rule: not.induct) auto
859 lemma conj_qf[simp]: "qfree p \<Longrightarrow> qfree q \<Longrightarrow> qfree (conj p q)"
860   using conj_def by auto
861 lemma conj_nb0[simp]: "bound0 p \<Longrightarrow> bound0 q \<Longrightarrow> bound0 (conj p q)"
862   using conj_def by auto
863 lemma conj_nb[simp]: "bound n p \<Longrightarrow> bound n q \<Longrightarrow> bound n (conj p q)"
864   using conj_def by auto
865 lemma conj_blt[simp]: "boundslt n p \<Longrightarrow> boundslt n q \<Longrightarrow> boundslt n (conj p q)"
866   using conj_def by auto
868 lemma disj_qf[simp]: "qfree p \<Longrightarrow> qfree q \<Longrightarrow> qfree (disj p q)"
869   using disj_def by auto
870 lemma disj_nb0[simp]: "bound0 p \<Longrightarrow> bound0 q \<Longrightarrow> bound0 (disj p q)"
871   using disj_def by auto
872 lemma disj_nb[simp]: "bound n p \<Longrightarrow> bound n q \<Longrightarrow> bound n (disj p q)"
873   using disj_def by auto
874 lemma disj_blt[simp]: "boundslt n p \<Longrightarrow> boundslt n q \<Longrightarrow> boundslt n (disj p q)"
875   using disj_def by auto
877 lemma imp_qf[simp]: "qfree p \<Longrightarrow> qfree q \<Longrightarrow> qfree (imp p q)"
878   using imp_def by (cases "p = F \<or> q = T") (simp_all add: imp_def)
879 lemma imp_nb0[simp]: "bound0 p \<Longrightarrow> bound0 q \<Longrightarrow> bound0 (imp p q)"
880   using imp_def by (cases "p = F \<or> q = T \<or> p = q") (simp_all add: imp_def)
881 lemma imp_nb[simp]: "bound n p \<Longrightarrow> bound n q \<Longrightarrow> bound n (imp p q)"
882   using imp_def by (cases "p = F \<or> q = T \<or> p = q") (simp_all add: imp_def)
883 lemma imp_blt[simp]: "boundslt n p \<Longrightarrow> boundslt n q \<Longrightarrow> boundslt n (imp p q)"
884   using imp_def by auto
886 lemma iff_qf[simp]: "qfree p \<Longrightarrow> qfree q \<Longrightarrow> qfree (iff p q)"
887   unfolding iff_def by (cases "p = q") auto
888 lemma iff_nb0[simp]: "bound0 p \<Longrightarrow> bound0 q \<Longrightarrow> bound0 (iff p q)"
889   using iff_def unfolding iff_def by (cases "p = q") auto
890 lemma iff_nb[simp]: "bound n p \<Longrightarrow> bound n q \<Longrightarrow> bound n (iff p q)"
891   using iff_def unfolding iff_def by (cases "p = q") auto
892 lemma iff_blt[simp]: "boundslt n p \<Longrightarrow> boundslt n q \<Longrightarrow> boundslt n (iff p q)"
893   using iff_def by auto
894 lemma decr0_qf: "bound0 p \<Longrightarrow> qfree (decr0 p)"
895   by (induct p) simp_all
897 fun isatom :: "fm \<Rightarrow> bool" (* test for atomicity *)
898 where
899   "isatom T = True"
900 | "isatom F = True"
901 | "isatom (Lt a) = True"
902 | "isatom (Le a) = True"
903 | "isatom (Eq a) = True"
904 | "isatom (NEq a) = True"
905 | "isatom p = False"
907 lemma bound0_qf: "bound0 p \<Longrightarrow> qfree p"
908   by (induct p) simp_all
910 definition djf :: "('a \<Rightarrow> fm) \<Rightarrow> 'a \<Rightarrow> fm \<Rightarrow> fm"
911 where
912   "djf f p q \<equiv>
913     (if q = T then T
914      else if q = F then f p
915      else (let fp = f p in case fp of T \<Rightarrow> T | F \<Rightarrow> q | _ \<Rightarrow> Or (f p) q))"
917 definition evaldjf :: "('a \<Rightarrow> fm) \<Rightarrow> 'a list \<Rightarrow> fm"
918   where "evaldjf f ps \<equiv> foldr (djf f) ps F"
920 lemma djf_Or: "Ifm vs bs (djf f p q) = Ifm vs bs (Or (f p) q)"
922     (cases "f p", simp_all add: Let_def djf_def)
924 lemma evaldjf_ex: "Ifm vs bs (evaldjf f ps) \<longleftrightarrow> (\<exists>p \<in> set ps. Ifm vs bs (f p))"
925   by (induct ps) (simp_all add: evaldjf_def djf_Or)
927 lemma evaldjf_bound0:
928   assumes nb: "\<forall>x\<in> set xs. bound0 (f x)"
929   shows "bound0 (evaldjf f xs)"
930   using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto)
932 lemma evaldjf_qf:
933   assumes nb: "\<forall>x\<in> set xs. qfree (f x)"
934   shows "qfree (evaldjf f xs)"
935   using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto)
937 fun disjuncts :: "fm \<Rightarrow> fm list"
938 where
939   "disjuncts (Or p q) = disjuncts p @ disjuncts q"
940 | "disjuncts F = []"
941 | "disjuncts p = [p]"
943 lemma disjuncts: "(\<exists>q \<in> set (disjuncts p). Ifm vs bs q) = Ifm vs bs p"
944   by (induct p rule: disjuncts.induct) auto
946 lemma disjuncts_nb: "bound0 p \<Longrightarrow> \<forall>q \<in> set (disjuncts p). bound0 q"
947 proof -
948   assume nb: "bound0 p"
949   then have "list_all bound0 (disjuncts p)"
950     by (induct p rule:disjuncts.induct) auto
951   then show ?thesis
952     by (simp only: list_all_iff)
953 qed
955 lemma disjuncts_qf: "qfree p \<Longrightarrow> \<forall>q\<in> set (disjuncts p). qfree q"
956 proof-
957   assume qf: "qfree p"
958   then have "list_all qfree (disjuncts p)"
959     by (induct p rule: disjuncts.induct) auto
960   then show ?thesis by (simp only: list_all_iff)
961 qed
963 definition DJ :: "(fm \<Rightarrow> fm) \<Rightarrow> fm \<Rightarrow> fm"
964   where "DJ f p \<equiv> evaldjf f (disjuncts p)"
966 lemma DJ:
967   assumes fdj: "\<forall>p q. Ifm vs bs (f (Or p q)) = Ifm vs bs (Or (f p) (f q))"
968     and fF: "f F = F"
969   shows "Ifm vs bs (DJ f p) = Ifm vs bs (f p)"
970 proof -
971   have "Ifm vs bs (DJ f p) = (\<exists>q \<in> set (disjuncts p). Ifm vs bs (f q))"
972     by (simp add: DJ_def evaldjf_ex)
973   also have "\<dots> = Ifm vs bs (f p)"
974     using fdj fF by (induct p rule: disjuncts.induct) auto
975   finally show ?thesis .
976 qed
978 lemma DJ_qf:
979   assumes fqf: "\<forall>p. qfree p \<longrightarrow> qfree (f p)"
980   shows "\<forall>p. qfree p \<longrightarrow> qfree (DJ f p)"
981 proof clarify
982   fix  p
983   assume qf: "qfree p"
984   have th: "DJ f p = evaldjf f (disjuncts p)"
986   from disjuncts_qf[OF qf] have "\<forall>q\<in> set (disjuncts p). qfree q" .
987   with fqf have th':"\<forall>q\<in> set (disjuncts p). qfree (f q)"
988     by blast
989   from evaldjf_qf[OF th'] th show "qfree (DJ f p)"
990     by simp
991 qed
993 lemma DJ_qe:
994   assumes qe: "\<forall>bs p. qfree p \<longrightarrow> qfree (qe p) \<and> (Ifm vs bs (qe p) = Ifm vs bs (E p))"
995   shows "\<forall>bs p. qfree p \<longrightarrow> qfree (DJ qe p) \<and> (Ifm vs bs ((DJ qe p)) = Ifm vs bs (E p))"
996 proof clarify
997   fix p :: fm and bs
998   assume qf: "qfree p"
999   from qe have qth: "\<forall>p. qfree p \<longrightarrow> qfree (qe p)"
1000     by blast
1001   from DJ_qf[OF qth] qf have qfth:"qfree (DJ qe p)"
1002     by auto
1003   have "Ifm vs bs (DJ qe p) \<longleftrightarrow> (\<exists>q\<in> set (disjuncts p). Ifm vs bs (qe q))"
1004     by (simp add: DJ_def evaldjf_ex)
1005   also have "\<dots> = (\<exists>q \<in> set(disjuncts p). Ifm vs bs (E q))"
1006     using qe disjuncts_qf[OF qf] by auto
1007   also have "\<dots> = Ifm vs bs (E p)"
1008     by (induct p rule: disjuncts.induct) auto
1009   finally show "qfree (DJ qe p) \<and> Ifm vs bs (DJ qe p) = Ifm vs bs (E p)"
1010     using qfth by blast
1011 qed
1013 fun conjuncts :: "fm \<Rightarrow> fm list"
1014 where
1015   "conjuncts (And p q) = conjuncts p @ conjuncts q"
1016 | "conjuncts T = []"
1017 | "conjuncts p = [p]"
1019 definition list_conj :: "fm list \<Rightarrow> fm"
1020   where "list_conj ps \<equiv> foldr conj ps T"
1022 definition CJNB :: "(fm \<Rightarrow> fm) \<Rightarrow> fm \<Rightarrow> fm"
1023 where
1024   "CJNB f p \<equiv>
1025     (let cjs = conjuncts p;
1026       (yes, no) = partition bound0 cjs
1027      in conj (decr0 (list_conj yes)) (f (list_conj no)))"
1029 lemma conjuncts_qf: "qfree p \<Longrightarrow> \<forall>q\<in> set (conjuncts p). qfree q"
1030 proof -
1031   assume qf: "qfree p"
1032   then have "list_all qfree (conjuncts p)"
1033     by (induct p rule: conjuncts.induct) auto
1034   then show ?thesis
1035     by (simp only: list_all_iff)
1036 qed
1038 lemma conjuncts: "(\<forall>q\<in> set (conjuncts p). Ifm vs bs q) = Ifm vs bs p"
1039   by (induct p rule: conjuncts.induct) auto
1041 lemma conjuncts_nb: "bound0 p \<Longrightarrow> \<forall>q\<in> set (conjuncts p). bound0 q"
1042 proof -
1043   assume nb: "bound0 p"
1044   then have "list_all bound0 (conjuncts p)"
1045     by (induct p rule:conjuncts.induct) auto
1046   then show ?thesis
1047     by (simp only: list_all_iff)
1048 qed
1050 fun islin :: "fm \<Rightarrow> bool"
1051 where
1052   "islin (And p q) = (islin p \<and> islin q \<and> p \<noteq> T \<and> p \<noteq> F \<and> q \<noteq> T \<and> q \<noteq> F)"
1053 | "islin (Or p q) = (islin p \<and> islin q \<and> p \<noteq> T \<and> p \<noteq> F \<and> q \<noteq> T \<and> q \<noteq> F)"
1054 | "islin (Eq (CNP 0 c s)) = (isnpoly c \<and> c \<noteq> 0\<^sub>p \<and> tmbound0 s \<and> allpolys isnpoly s)"
1055 | "islin (NEq (CNP 0 c s)) = (isnpoly c \<and> c \<noteq> 0\<^sub>p \<and> tmbound0 s \<and> allpolys isnpoly s)"
1056 | "islin (Lt (CNP 0 c s)) = (isnpoly c \<and> c \<noteq> 0\<^sub>p \<and> tmbound0 s \<and> allpolys isnpoly s)"
1057 | "islin (Le (CNP 0 c s)) = (isnpoly c \<and> c \<noteq> 0\<^sub>p \<and> tmbound0 s \<and> allpolys isnpoly s)"
1058 | "islin (NOT p) = False"
1059 | "islin (Imp p q) = False"
1060 | "islin (Iff p q) = False"
1061 | "islin p = bound0 p"
1063 lemma islin_stupid:
1064   assumes nb: "tmbound0 p"
1065   shows "islin (Lt p)"
1066     and "islin (Le p)"
1067     and "islin (Eq p)"
1068     and "islin (NEq p)"
1069   using nb by (cases p, auto, case_tac nat, auto)+
1071 definition "lt p = (case p of CP (C c) \<Rightarrow> if 0>\<^sub>N c then T else F| _ \<Rightarrow> Lt p)"
1072 definition "le p = (case p of CP (C c) \<Rightarrow> if 0\<ge>\<^sub>N c then T else F | _ \<Rightarrow> Le p)"
1073 definition "eq p = (case p of CP (C c) \<Rightarrow> if c = 0\<^sub>N then T else F | _ \<Rightarrow> Eq p)"
1074 definition "neq p = not (eq p)"
1076 lemma lt: "allpolys isnpoly p \<Longrightarrow> Ifm vs bs (lt p) = Ifm vs bs (Lt p)"
1078   apply (cases p)
1079   apply simp_all
1080   apply (case_tac poly)
1082   done
1084 lemma le: "allpolys isnpoly p \<Longrightarrow> Ifm vs bs (le p) = Ifm vs bs (Le p)"
1086   apply (cases p)
1087   apply simp_all
1088   apply (case_tac poly)
1090   done
1092 lemma eq: "allpolys isnpoly p \<Longrightarrow> Ifm vs bs (eq p) = Ifm vs bs (Eq p)"
1094   apply (cases p)
1095   apply simp_all
1096   apply (case_tac poly)
1098   done
1100 lemma neq: "allpolys isnpoly p \<Longrightarrow> Ifm vs bs (neq p) = Ifm vs bs (NEq p)"
1101   by (simp add: neq_def eq)
1103 lemma lt_lin: "tmbound0 p \<Longrightarrow> islin (lt p)"
1105   apply (cases p)
1106   apply simp_all
1107   apply (case_tac poly)
1108   apply simp_all
1109   apply (case_tac nat)
1110   apply simp_all
1111   done
1113 lemma le_lin: "tmbound0 p \<Longrightarrow> islin (le p)"
1115   apply (cases p)
1116   apply simp_all
1117   apply (case_tac poly)
1118   apply simp_all
1119   apply (case_tac nat)
1120   apply simp_all
1121   done
1123 lemma eq_lin: "tmbound0 p \<Longrightarrow> islin (eq p)"
1125   apply (cases p)
1126   apply simp_all
1127   apply (case_tac poly)
1128   apply simp_all
1129   apply (case_tac nat)
1130   apply simp_all
1131   done
1133 lemma neq_lin: "tmbound0 p \<Longrightarrow> islin (neq p)"
1134   apply (simp add: neq_def eq_def)
1135   apply (cases p)
1136   apply simp_all
1137   apply (case_tac poly)
1138   apply simp_all
1139   apply (case_tac nat)
1140   apply simp_all
1141   done
1143 definition "simplt t = (let (c,s) = split0 (simptm t) in if c= 0\<^sub>p then lt s else Lt (CNP 0 c s))"
1144 definition "simple t = (let (c,s) = split0 (simptm t) in if c= 0\<^sub>p then le s else Le (CNP 0 c s))"
1145 definition "simpeq t = (let (c,s) = split0 (simptm t) in if c= 0\<^sub>p then eq s else Eq (CNP 0 c s))"
1146 definition "simpneq t = (let (c,s) = split0 (simptm t) in if c= 0\<^sub>p then neq s else NEq (CNP 0 c s))"
1148 lemma simplt_islin[simp]:
1149   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1150   shows "islin (simplt t)"
1151   unfolding simplt_def
1152   using split0_nb0'
1153   by (auto simp add: lt_lin Let_def split_def isnpoly_fst_split0[OF simptm_allpolys_npoly]
1154       islin_stupid allpolys_split0[OF simptm_allpolys_npoly])
1156 lemma simple_islin[simp]:
1157   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1158   shows "islin (simple t)"
1159   unfolding simple_def
1160   using split0_nb0'
1161   by (auto simp add: Let_def split_def isnpoly_fst_split0[OF simptm_allpolys_npoly]
1162       islin_stupid allpolys_split0[OF simptm_allpolys_npoly] le_lin)
1164 lemma simpeq_islin[simp]:
1165   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1166   shows "islin (simpeq t)"
1167   unfolding simpeq_def
1168   using split0_nb0'
1169   by (auto simp add: Let_def split_def isnpoly_fst_split0[OF simptm_allpolys_npoly]
1170       islin_stupid allpolys_split0[OF simptm_allpolys_npoly] eq_lin)
1172 lemma simpneq_islin[simp]:
1173   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1174   shows "islin (simpneq t)"
1175   unfolding simpneq_def
1176   using split0_nb0'
1177   by (auto simp add: Let_def split_def isnpoly_fst_split0[OF simptm_allpolys_npoly]
1178       islin_stupid allpolys_split0[OF simptm_allpolys_npoly] neq_lin)
1180 lemma really_stupid: "\<not> (\<forall>c1 s'. (c1, s') \<noteq> split0 s)"
1181   by (cases "split0 s") auto
1183 lemma split0_npoly:
1184   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1185     and n: "allpolys isnpoly t"
1186   shows "isnpoly (fst (split0 t))"
1187     and "allpolys isnpoly (snd (split0 t))"
1188   using n
1189   by (induct t rule: split0.induct)
1191       polysub_norm really_stupid)
1193 lemma simplt[simp]: "Ifm vs bs (simplt t) = Ifm vs bs (Lt t)"
1194 proof -
1195   have n: "allpolys isnpoly (simptm t)"
1196     by simp
1197   let ?t = "simptm t"
1198   {
1199     assume "fst (split0 ?t) = 0\<^sub>p"
1200     then have ?thesis
1201       using split0[of "simptm t" vs bs] lt[OF split0_npoly(2)[OF n], of vs bs]
1202       by (simp add: simplt_def Let_def split_def lt)
1203   }
1204   moreover
1205   {
1206     assume "fst (split0 ?t) \<noteq> 0\<^sub>p"
1207     then have ?thesis
1208       using  split0[of "simptm t" vs bs]
1209       by (simp add: simplt_def Let_def split_def)
1210   }
1211   ultimately show ?thesis by blast
1212 qed
1214 lemma simple[simp]: "Ifm vs bs (simple t) = Ifm vs bs (Le t)"
1215 proof -
1216   have n: "allpolys isnpoly (simptm t)"
1217     by simp
1218   let ?t = "simptm t"
1219   {
1220     assume "fst (split0 ?t) = 0\<^sub>p"
1221     then have ?thesis
1222       using split0[of "simptm t" vs bs] le[OF split0_npoly(2)[OF n], of vs bs]
1223       by (simp add: simple_def Let_def split_def le)
1224   }
1225   moreover
1226   {
1227     assume "fst (split0 ?t) \<noteq> 0\<^sub>p"
1228     then have ?thesis
1229       using split0[of "simptm t" vs bs]
1230       by (simp add: simple_def Let_def split_def)
1231   }
1232   ultimately show ?thesis by blast
1233 qed
1235 lemma simpeq[simp]: "Ifm vs bs (simpeq t) = Ifm vs bs (Eq t)"
1236 proof -
1237   have n: "allpolys isnpoly (simptm t)"
1238     by simp
1239   let ?t = "simptm t"
1240   {
1241     assume "fst (split0 ?t) = 0\<^sub>p"
1242     then have ?thesis
1243       using split0[of "simptm t" vs bs] eq[OF split0_npoly(2)[OF n], of vs bs]
1244       by (simp add: simpeq_def Let_def split_def)
1245   }
1246   moreover
1247   {
1248     assume "fst (split0 ?t) \<noteq> 0\<^sub>p"
1249     then have ?thesis using  split0[of "simptm t" vs bs]
1250       by (simp add: simpeq_def Let_def split_def)
1251   }
1252   ultimately show ?thesis by blast
1253 qed
1255 lemma simpneq[simp]: "Ifm vs bs (simpneq t) = Ifm vs bs (NEq t)"
1256 proof -
1257   have n: "allpolys isnpoly (simptm t)"
1258     by simp
1259   let ?t = "simptm t"
1260   {
1261     assume "fst (split0 ?t) = 0\<^sub>p"
1262     then have ?thesis
1263       using split0[of "simptm t" vs bs] neq[OF split0_npoly(2)[OF n], of vs bs]
1264       by (simp add: simpneq_def Let_def split_def)
1265   }
1266   moreover
1267   {
1268     assume "fst (split0 ?t) \<noteq> 0\<^sub>p"
1269     then have ?thesis
1270       using split0[of "simptm t" vs bs] by (simp add: simpneq_def Let_def split_def)
1271   }
1272   ultimately show ?thesis by blast
1273 qed
1275 lemma lt_nb: "tmbound0 t \<Longrightarrow> bound0 (lt t)"
1277   apply (cases t)
1278   apply auto
1279   apply (case_tac poly)
1280   apply auto
1281   done
1283 lemma le_nb: "tmbound0 t \<Longrightarrow> bound0 (le t)"
1285   apply (cases t)
1286   apply auto
1287   apply (case_tac poly)
1288   apply auto
1289   done
1291 lemma eq_nb: "tmbound0 t \<Longrightarrow> bound0 (eq t)"
1293   apply (cases t)
1294   apply auto
1295   apply (case_tac poly)
1296   apply auto
1297   done
1299 lemma neq_nb: "tmbound0 t \<Longrightarrow> bound0 (neq t)"
1300   apply (simp add: neq_def eq_def)
1301   apply (cases t)
1302   apply auto
1303   apply (case_tac poly)
1304   apply auto
1305   done
1307 lemma simplt_nb[simp]:
1308   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1309   shows "tmbound0 t \<Longrightarrow> bound0 (simplt t)"
1310 proof (simp add: simplt_def Let_def split_def)
1311   assume nb: "tmbound0 t"
1312   then have nb': "tmbound0 (simptm t)"
1313     by simp
1314   let ?c = "fst (split0 (simptm t))"
1315   from tmbound_split0[OF nb'[unfolded tmbound0_tmbound_iff[symmetric]]]
1316   have th: "\<forall>bs. Ipoly bs ?c = Ipoly bs 0\<^sub>p"
1317     by auto
1318   from isnpoly_fst_split0[OF simptm_allpolys_npoly[of t]]
1319   have ths: "isnpolyh ?c 0" "isnpolyh 0\<^sub>p 0"
1321   from iffD1[OF isnpolyh_unique[OF ths] th]
1322   have "fst (split0 (simptm t)) = 0\<^sub>p" .
1323   then show "(fst (split0 (simptm t)) = 0\<^sub>p \<longrightarrow> bound0 (lt (snd (split0 (simptm t))))) \<and>
1324       fst (split0 (simptm t)) = 0\<^sub>p"
1325     by (simp add: simplt_def Let_def split_def lt_nb)
1326 qed
1328 lemma simple_nb[simp]:
1329   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1330   shows "tmbound0 t \<Longrightarrow> bound0 (simple t)"
1331 proof(simp add: simple_def Let_def split_def)
1332   assume nb: "tmbound0 t"
1333   then have nb': "tmbound0 (simptm t)"
1334     by simp
1335   let ?c = "fst (split0 (simptm t))"
1336   from tmbound_split0[OF nb'[unfolded tmbound0_tmbound_iff[symmetric]]]
1337   have th: "\<forall>bs. Ipoly bs ?c = Ipoly bs 0\<^sub>p"
1338     by auto
1339   from isnpoly_fst_split0[OF simptm_allpolys_npoly[of t]]
1340   have ths: "isnpolyh ?c 0" "isnpolyh 0\<^sub>p 0"
1342   from iffD1[OF isnpolyh_unique[OF ths] th]
1343   have "fst (split0 (simptm t)) = 0\<^sub>p" .
1344   then show "(fst (split0 (simptm t)) = 0\<^sub>p \<longrightarrow> bound0 (le (snd (split0 (simptm t))))) \<and>
1345       fst (split0 (simptm t)) = 0\<^sub>p"
1346     by (simp add: simplt_def Let_def split_def le_nb)
1347 qed
1349 lemma simpeq_nb[simp]:
1350   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1351   shows "tmbound0 t \<Longrightarrow> bound0 (simpeq t)"
1352 proof (simp add: simpeq_def Let_def split_def)
1353   assume nb: "tmbound0 t"
1354   then have nb': "tmbound0 (simptm t)"
1355     by simp
1356   let ?c = "fst (split0 (simptm t))"
1357   from tmbound_split0[OF nb'[unfolded tmbound0_tmbound_iff[symmetric]]]
1358   have th: "\<forall>bs. Ipoly bs ?c = Ipoly bs 0\<^sub>p"
1359     by auto
1360   from isnpoly_fst_split0[OF simptm_allpolys_npoly[of t]]
1361   have ths: "isnpolyh ?c 0" "isnpolyh 0\<^sub>p 0"
1363   from iffD1[OF isnpolyh_unique[OF ths] th]
1364   have "fst (split0 (simptm t)) = 0\<^sub>p" .
1365   then show "(fst (split0 (simptm t)) = 0\<^sub>p \<longrightarrow> bound0 (eq (snd (split0 (simptm t))))) \<and>
1366       fst (split0 (simptm t)) = 0\<^sub>p"
1367     by (simp add: simpeq_def Let_def split_def eq_nb)
1368 qed
1370 lemma simpneq_nb[simp]:
1371   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1372   shows "tmbound0 t \<Longrightarrow> bound0 (simpneq t)"
1373 proof (simp add: simpneq_def Let_def split_def)
1374   assume nb: "tmbound0 t"
1375   then have nb': "tmbound0 (simptm t)"
1376     by simp
1377   let ?c = "fst (split0 (simptm t))"
1378   from tmbound_split0[OF nb'[unfolded tmbound0_tmbound_iff[symmetric]]]
1379   have th: "\<forall>bs. Ipoly bs ?c = Ipoly bs 0\<^sub>p"
1380     by auto
1381   from isnpoly_fst_split0[OF simptm_allpolys_npoly[of t]]
1382   have ths: "isnpolyh ?c 0" "isnpolyh 0\<^sub>p 0"
1384   from iffD1[OF isnpolyh_unique[OF ths] th]
1385   have "fst (split0 (simptm t)) = 0\<^sub>p" .
1386   then show "(fst (split0 (simptm t)) = 0\<^sub>p \<longrightarrow> bound0 (neq (snd (split0 (simptm t))))) \<and>
1387       fst (split0 (simptm t)) = 0\<^sub>p"
1388     by (simp add: simpneq_def Let_def split_def neq_nb)
1389 qed
1391 fun conjs :: "fm \<Rightarrow> fm list"
1392 where
1393   "conjs (And p q) = conjs p @ conjs q"
1394 | "conjs T = []"
1395 | "conjs p = [p]"
1397 lemma conjs_ci: "(\<forall>q \<in> set (conjs p). Ifm vs bs q) = Ifm vs bs p"
1398   by (induct p rule: conjs.induct) auto
1400 definition list_disj :: "fm list \<Rightarrow> fm"
1401   where "list_disj ps \<equiv> foldr disj ps F"
1403 lemma list_conj: "Ifm vs bs (list_conj ps) = (\<forall>p\<in> set ps. Ifm vs bs p)"
1404   by (induct ps) (auto simp add: list_conj_def)
1406 lemma list_conj_qf: " \<forall>p\<in> set ps. qfree p \<Longrightarrow> qfree (list_conj ps)"
1407   by (induct ps) (auto simp add: list_conj_def)
1409 lemma list_disj: "Ifm vs bs (list_disj ps) = (\<exists>p\<in> set ps. Ifm vs bs p)"
1410   by (induct ps) (auto simp add: list_disj_def)
1412 lemma conj_boundslt: "boundslt n p \<Longrightarrow> boundslt n q \<Longrightarrow> boundslt n (conj p q)"
1413   unfolding conj_def by auto
1415 lemma conjs_nb: "bound n p \<Longrightarrow> \<forall>q\<in> set (conjs p). bound n q"
1416   apply (induct p rule: conjs.induct)
1417   apply (unfold conjs.simps)
1418   apply (unfold set_append)
1419   apply (unfold ball_Un)
1420   apply (unfold bound.simps)
1421   apply auto
1422   done
1424 lemma conjs_boundslt: "boundslt n p \<Longrightarrow> \<forall>q\<in> set (conjs p). boundslt n q"
1425   apply (induct p rule: conjs.induct)
1426   apply (unfold conjs.simps)
1427   apply (unfold set_append)
1428   apply (unfold ball_Un)
1429   apply (unfold boundslt.simps)
1430   apply blast
1431   apply simp_all
1432   done
1434 lemma list_conj_boundslt: " \<forall>p\<in> set ps. boundslt n p \<Longrightarrow> boundslt n (list_conj ps)"
1435   unfolding list_conj_def
1436   by (induct ps) auto
1438 lemma list_conj_nb:
1439   assumes bnd: "\<forall>p\<in> set ps. bound n p"
1440   shows "bound n (list_conj ps)"
1441   using bnd
1442   unfolding list_conj_def
1443   by (induct ps) auto
1445 lemma list_conj_nb': "\<forall>p\<in>set ps. bound0 p \<Longrightarrow> bound0 (list_conj ps)"
1446   unfolding list_conj_def by (induct ps) auto
1448 lemma CJNB_qe:
1449   assumes qe: "\<forall>bs p. qfree p \<longrightarrow> qfree (qe p) \<and> (Ifm vs bs (qe p) = Ifm vs bs (E p))"
1450   shows "\<forall>bs p. qfree p \<longrightarrow> qfree (CJNB qe p) \<and> (Ifm vs bs ((CJNB qe p)) = Ifm vs bs (E p))"
1451 proof clarify
1452   fix bs p
1453   assume qfp: "qfree p"
1454   let ?cjs = "conjuncts p"
1455   let ?yes = "fst (partition bound0 ?cjs)"
1456   let ?no = "snd (partition bound0 ?cjs)"
1457   let ?cno = "list_conj ?no"
1458   let ?cyes = "list_conj ?yes"
1459   have part: "partition bound0 ?cjs = (?yes,?no)"
1460     by simp
1461   from partition_P[OF part] have "\<forall>q\<in> set ?yes. bound0 q"
1462     by blast
1463   then have yes_nb: "bound0 ?cyes"
1465   then have yes_qf: "qfree (decr0 ?cyes)"
1467   from conjuncts_qf[OF qfp] partition_set[OF part]
1468   have " \<forall>q\<in> set ?no. qfree q"
1469     by auto
1470   then have no_qf: "qfree ?cno"
1472   with qe have cno_qf:"qfree (qe ?cno)"
1473     and noE: "Ifm vs bs (qe ?cno) = Ifm vs bs (E ?cno)"
1474     by blast+
1475   from cno_qf yes_qf have qf: "qfree (CJNB qe p)"
1476     by (simp add: CJNB_def Let_def split_def)
1477   {
1478     fix bs
1479     from conjuncts have "Ifm vs bs p = (\<forall>q\<in> set ?cjs. Ifm vs bs q)"
1480       by blast
1481     also have "\<dots> = ((\<forall>q\<in> set ?yes. Ifm vs bs q) \<and> (\<forall>q\<in> set ?no. Ifm vs bs q))"
1482       using partition_set[OF part] by auto
1483     finally have "Ifm vs bs p = ((Ifm vs bs ?cyes) \<and> (Ifm vs bs ?cno))"
1484       using list_conj[of vs bs] by simp
1485   }
1486   then have "Ifm vs bs (E p) = (\<exists>x. (Ifm vs (x#bs) ?cyes) \<and> (Ifm vs (x#bs) ?cno))"
1487     by simp
1488   also fix y have "\<dots> = (\<exists>x. (Ifm vs (y#bs) ?cyes) \<and> (Ifm vs (x#bs) ?cno))"
1489     using bound0_I[OF yes_nb, where bs="bs" and b'="y"] by blast
1490   also have "\<dots> = (Ifm vs bs (decr0 ?cyes) \<and> Ifm vs bs (E ?cno))"
1491     by (auto simp add: decr0[OF yes_nb] simp del: partition_filter_conv)
1492   also have "\<dots> = (Ifm vs bs (conj (decr0 ?cyes) (qe ?cno)))"
1493     using qe[rule_format, OF no_qf] by auto
1494   finally have "Ifm vs bs (E p) = Ifm vs bs (CJNB qe p)"
1495     by (simp add: Let_def CJNB_def split_def)
1496   with qf show "qfree (CJNB qe p) \<and> Ifm vs bs (CJNB qe p) = Ifm vs bs (E p)"
1497     by blast
1498 qed
1500 consts simpfm :: "fm \<Rightarrow> fm"
1501 recdef simpfm "measure fmsize"
1502   "simpfm (Lt t) = simplt (simptm t)"
1503   "simpfm (Le t) = simple (simptm t)"
1504   "simpfm (Eq t) = simpeq(simptm t)"
1505   "simpfm (NEq t) = simpneq(simptm t)"
1506   "simpfm (And p q) = conj (simpfm p) (simpfm q)"
1507   "simpfm (Or p q) = disj (simpfm p) (simpfm q)"
1508   "simpfm (Imp p q) = disj (simpfm (NOT p)) (simpfm q)"
1509   "simpfm (Iff p q) =
1510     disj (conj (simpfm p) (simpfm q)) (conj (simpfm (NOT p)) (simpfm (NOT q)))"
1511   "simpfm (NOT (And p q)) = disj (simpfm (NOT p)) (simpfm (NOT q))"
1512   "simpfm (NOT (Or p q)) = conj (simpfm (NOT p)) (simpfm (NOT q))"
1513   "simpfm (NOT (Imp p q)) = conj (simpfm p) (simpfm (NOT q))"
1514   "simpfm (NOT (Iff p q)) =
1515     disj (conj (simpfm p) (simpfm (NOT q))) (conj (simpfm (NOT p)) (simpfm q))"
1516   "simpfm (NOT (Eq t)) = simpneq t"
1517   "simpfm (NOT (NEq t)) = simpeq t"
1518   "simpfm (NOT (Le t)) = simplt (Neg t)"
1519   "simpfm (NOT (Lt t)) = simple (Neg t)"
1520   "simpfm (NOT (NOT p)) = simpfm p"
1521   "simpfm (NOT T) = F"
1522   "simpfm (NOT F) = T"
1523   "simpfm p = p"
1525 lemma simpfm[simp]: "Ifm vs bs (simpfm p) = Ifm vs bs p"
1526   by (induct p arbitrary: bs rule: simpfm.induct) auto
1528 lemma simpfm_bound0:
1529   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1530   shows "bound0 p \<Longrightarrow> bound0 (simpfm p)"
1531   by (induct p rule: simpfm.induct) auto
1533 lemma lt_qf[simp]: "qfree (lt t)"
1534   apply (cases t)
1535   apply (auto simp add: lt_def)
1536   apply (case_tac poly)
1537   apply auto
1538   done
1540 lemma le_qf[simp]: "qfree (le t)"
1541   apply (cases t)
1542   apply (auto simp add: le_def)
1543   apply (case_tac poly)
1544   apply auto
1545   done
1547 lemma eq_qf[simp]: "qfree (eq t)"
1548   apply (cases t)
1549   apply (auto simp add: eq_def)
1550   apply (case_tac poly)
1551   apply auto
1552   done
1554 lemma neq_qf[simp]: "qfree (neq t)" by (simp add: neq_def)
1556 lemma simplt_qf[simp]: "qfree (simplt t)" by (simp add: simplt_def Let_def split_def)
1557 lemma simple_qf[simp]: "qfree (simple t)" by (simp add: simple_def Let_def split_def)
1558 lemma simpeq_qf[simp]: "qfree (simpeq t)" by (simp add: simpeq_def Let_def split_def)
1559 lemma simpneq_qf[simp]: "qfree (simpneq t)" by (simp add: simpneq_def Let_def split_def)
1561 lemma simpfm_qf[simp]: "qfree p \<Longrightarrow> qfree (simpfm p)"
1562   by (induct p rule: simpfm.induct) auto
1564 lemma disj_lin: "islin p \<Longrightarrow> islin q \<Longrightarrow> islin (disj p q)"
1566 lemma conj_lin: "islin p \<Longrightarrow> islin q \<Longrightarrow> islin (conj p q)"
1569 lemma
1570   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1571   shows "qfree p \<Longrightarrow> islin (simpfm p)"
1572   by (induct p rule: simpfm.induct) (simp_all add: conj_lin disj_lin)
1574 consts prep :: "fm \<Rightarrow> fm"
1575 recdef prep "measure fmsize"
1576   "prep (E T) = T"
1577   "prep (E F) = F"
1578   "prep (E (Or p q)) = disj (prep (E p)) (prep (E q))"
1579   "prep (E (Imp p q)) = disj (prep (E (NOT p))) (prep (E q))"
1580   "prep (E (Iff p q)) = disj (prep (E (And p q))) (prep (E (And (NOT p) (NOT q))))"
1581   "prep (E (NOT (And p q))) = disj (prep (E (NOT p))) (prep (E(NOT q)))"
1582   "prep (E (NOT (Imp p q))) = prep (E (And p (NOT q)))"
1583   "prep (E (NOT (Iff p q))) = disj (prep (E (And p (NOT q)))) (prep (E(And (NOT p) q)))"
1584   "prep (E p) = E (prep p)"
1585   "prep (A (And p q)) = conj (prep (A p)) (prep (A q))"
1586   "prep (A p) = prep (NOT (E (NOT p)))"
1587   "prep (NOT (NOT p)) = prep p"
1588   "prep (NOT (And p q)) = disj (prep (NOT p)) (prep (NOT q))"
1589   "prep (NOT (A p)) = prep (E (NOT p))"
1590   "prep (NOT (Or p q)) = conj (prep (NOT p)) (prep (NOT q))"
1591   "prep (NOT (Imp p q)) = conj (prep p) (prep (NOT q))"
1592   "prep (NOT (Iff p q)) = disj (prep (And p (NOT q))) (prep (And (NOT p) q))"
1593   "prep (NOT p) = not (prep p)"
1594   "prep (Or p q) = disj (prep p) (prep q)"
1595   "prep (And p q) = conj (prep p) (prep q)"
1596   "prep (Imp p q) = prep (Or (NOT p) q)"
1597   "prep (Iff p q) = disj (prep (And p q)) (prep (And (NOT p) (NOT q)))"
1598   "prep p = p"
1601 lemma prep: "Ifm vs bs (prep p) = Ifm vs bs p"
1602   by (induct p arbitrary: bs rule: prep.induct) auto
1605 (* Generic quantifier elimination *)
1606 function (sequential) qelim :: "fm \<Rightarrow> (fm \<Rightarrow> fm) \<Rightarrow> fm"
1607 where
1608   "qelim (E p) = (\<lambda>qe. DJ (CJNB qe) (qelim p qe))"
1609 | "qelim (A p) = (\<lambda>qe. not (qe ((qelim (NOT p) qe))))"
1610 | "qelim (NOT p) = (\<lambda>qe. not (qelim p qe))"
1611 | "qelim (And p q) = (\<lambda>qe. conj (qelim p qe) (qelim q qe))"
1612 | "qelim (Or  p q) = (\<lambda>qe. disj (qelim p qe) (qelim q qe))"
1613 | "qelim (Imp p q) = (\<lambda>qe. imp (qelim p qe) (qelim q qe))"
1614 | "qelim (Iff p q) = (\<lambda>qe. iff (qelim p qe) (qelim q qe))"
1615 | "qelim p = (\<lambda>y. simpfm p)"
1616 by pat_completeness simp_all
1617 termination by (relation "measure fmsize") auto
1619 lemma qelim:
1620   assumes qe_inv: "\<forall>bs p. qfree p \<longrightarrow> qfree (qe p) \<and> (Ifm vs bs (qe p) = Ifm vs bs (E p))"
1621   shows "\<And> bs. qfree (qelim p qe) \<and> (Ifm vs bs (qelim p qe) = Ifm vs bs p)"
1622   using qe_inv DJ_qe[OF CJNB_qe[OF qe_inv]]
1623   by (induct p rule: qelim.induct) auto
1626 subsection {* Core Procedure *}
1628 fun minusinf:: "fm \<Rightarrow> fm" (* Virtual substitution of -\<infinity>*)
1629 where
1630   "minusinf (And p q) = conj (minusinf p) (minusinf q)"
1631 | "minusinf (Or p q) = disj (minusinf p) (minusinf q)"
1632 | "minusinf (Eq  (CNP 0 c e)) = conj (eq (CP c)) (eq e)"
1633 | "minusinf (NEq (CNP 0 c e)) = disj (not (eq e)) (not (eq (CP c)))"
1634 | "minusinf (Lt  (CNP 0 c e)) = disj (conj (eq (CP c)) (lt e)) (lt (CP (~\<^sub>p c)))"
1635 | "minusinf (Le  (CNP 0 c e)) = disj (conj (eq (CP c)) (le e)) (lt (CP (~\<^sub>p c)))"
1636 | "minusinf p = p"
1638 fun plusinf:: "fm \<Rightarrow> fm" (* Virtual substitution of +\<infinity>*)
1639 where
1640   "plusinf (And p q) = conj (plusinf p) (plusinf q)"
1641 | "plusinf (Or p q) = disj (plusinf p) (plusinf q)"
1642 | "plusinf (Eq  (CNP 0 c e)) = conj (eq (CP c)) (eq e)"
1643 | "plusinf (NEq (CNP 0 c e)) = disj (not (eq e)) (not (eq (CP c)))"
1644 | "plusinf (Lt  (CNP 0 c e)) = disj (conj (eq (CP c)) (lt e)) (lt (CP c))"
1645 | "plusinf (Le  (CNP 0 c e)) = disj (conj (eq (CP c)) (le e)) (lt (CP c))"
1646 | "plusinf p = p"
1648 lemma minusinf_inf:
1649   assumes lp: "islin p"
1650   shows "\<exists>z. \<forall>x < z. Ifm vs (x#bs) (minusinf p) \<longleftrightarrow> Ifm vs (x#bs) p"
1651   using lp
1652 proof (induct p rule: minusinf.induct)
1653   case 1
1654   then show ?case
1655     apply auto
1656     apply (rule_tac x="min z za" in exI)
1657     apply auto
1658     done
1659 next
1660   case 2
1661   then show ?case
1662     apply auto
1663     apply (rule_tac x="min z za" in exI)
1664     apply auto
1665     done
1666 next
1667   case (3 c e)
1668   then have nbe: "tmbound0 e"
1669     by simp
1670   from 3 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e"
1671     by simp_all
1672   note eqs = eq[OF nc(1), where ?'a = 'a] eq[OF nc(2), where ?'a = 'a]
1673   let ?c = "Ipoly vs c"
1674   fix y
1675   let ?e = "Itm vs (y#bs) e"
1676   have "?c = 0 \<or> ?c > 0 \<or> ?c < 0" by arith
1677   moreover {
1678     assume "?c = 0"
1679     then have ?case
1680       using eq[OF nc(2), of vs] eq[OF nc(1), of vs] by auto
1681   }
1682   moreover {
1683     assume cp: "?c > 0"
1684     {
1685       fix x
1686       assume xz: "x < -?e / ?c"
1687       then have "?c * x < - ?e"
1688         using pos_less_divide_eq[OF cp, where a="x" and b="-?e"]
1690       then have "?c * x + ?e < 0"
1691         by simp
1692       then have "Ifm vs (x#bs) (Eq (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Eq (CNP 0 c e)))"
1693         using eqs tmbound0_I[OF nbe, where b="y" and b'="x" and vs=vs and bs=bs] by auto
1694     }
1695     then have ?case by auto
1696   }
1697   moreover {
1698     assume cp: "?c < 0"
1699     {
1700       fix x
1701       assume xz: "x < -?e / ?c"
1702       then have "?c * x > - ?e"
1703         using neg_less_divide_eq[OF cp, where a="x" and b="-?e"]
1705       then have "?c * x + ?e > 0"
1706         by simp
1707       then have "Ifm vs (x#bs) (Eq (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Eq (CNP 0 c e)))"
1708         using tmbound0_I[OF nbe, where b="y" and b'="x"] eqs by auto
1709     }
1710     then have ?case by auto
1711   }
1712   ultimately show ?case by blast
1713 next
1714   case (4 c e)
1715   then have nbe: "tmbound0 e"
1716     by simp
1717   from 4 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e"
1718     by simp_all
1719   note eqs = eq[OF nc(1), where ?'a = 'a] eq[OF nc(2), where ?'a = 'a]
1720   let ?c = "Ipoly vs c"
1721   fix y
1722   let ?e = "Itm vs (y#bs) e"
1723   have "?c=0 \<or> ?c > 0 \<or> ?c < 0"
1724     by arith
1725   moreover {
1726     assume "?c = 0"
1727     then have ?case
1728       using eqs by auto
1729   }
1730   moreover {
1731     assume cp: "?c > 0"
1732     {
1733       fix x
1734       assume xz: "x < -?e / ?c"
1735       then have "?c * x < - ?e"
1736         using pos_less_divide_eq[OF cp, where a="x" and b="-?e"]
1738       then have "?c * x + ?e < 0"
1739         by simp
1740       then have "Ifm vs (x#bs) (NEq (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (NEq (CNP 0 c e)))"
1741         using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] by auto
1742     }
1743     then have ?case by auto
1744   }
1745   moreover {
1746     assume cp: "?c < 0"
1747     {
1748       fix x
1749       assume xz: "x < -?e / ?c"
1750       then have "?c * x > - ?e"
1751         using neg_less_divide_eq[OF cp, where a="x" and b="-?e"]
1753       then have "?c * x + ?e > 0"
1754         by simp
1755       then have "Ifm vs (x#bs) (NEq (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (NEq (CNP 0 c e)))"
1756         using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] by auto
1757     }
1758     then have ?case by auto
1759   }
1760   ultimately show ?case by blast
1761 next
1762   case (5 c e)
1763   then have nbe: "tmbound0 e"
1764     by simp
1765   from 5 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e"
1766     by simp_all
1767   then have nc': "allpolys isnpoly (CP (~\<^sub>p c))"
1769   note eqs = lt[OF nc', where ?'a = 'a] eq [OF nc(1), where ?'a = 'a] lt[OF nc(2), where ?'a = 'a]
1770   let ?c = "Ipoly vs c"
1771   fix y
1772   let ?e = "Itm vs (y#bs) e"
1773   have "?c=0 \<or> ?c > 0 \<or> ?c < 0"
1774     by arith
1775   moreover {
1776     assume "?c = 0"
1777     then have ?case using eqs by auto
1778   }
1779   moreover {
1780     assume cp: "?c > 0"
1781     {
1782       fix x
1783       assume xz: "x < -?e / ?c"
1784       then have "?c * x < - ?e"
1785         using pos_less_divide_eq[OF cp, where a="x" and b="-?e"]
1787       then have "?c * x + ?e < 0" by simp
1788       then have "Ifm vs (x#bs) (Lt (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Lt (CNP 0 c e)))"
1789         using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto
1790     }
1791     then have ?case by auto
1792   }
1793   moreover {
1794     assume cp: "?c < 0"
1795     {
1796       fix x
1797       assume xz: "x < -?e / ?c"
1798       then have "?c * x > - ?e"
1799         using neg_less_divide_eq[OF cp, where a="x" and b="-?e"]
1801       then have "?c * x + ?e > 0"
1802         by simp
1803       then have "Ifm vs (x#bs) (Lt (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Lt (CNP 0 c e)))"
1804         using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] cp by auto
1805     }
1806     then have ?case by auto
1807   }
1808   ultimately show ?case by blast
1809 next
1810   case (6 c e)
1811   then have nbe: "tmbound0 e"
1812     by simp
1813   from 6 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e"
1814     by simp_all
1815   then have nc': "allpolys isnpoly (CP (~\<^sub>p c))"
1817   note eqs = lt[OF nc', where ?'a = 'a] eq [OF nc(1), where ?'a = 'a] le[OF nc(2), where ?'a = 'a]
1818   let ?c = "Ipoly vs c"
1819   fix y
1820   let ?e = "Itm vs (y#bs) e"
1821   have "?c = 0 \<or> ?c > 0 \<or> ?c < 0" by arith
1822   moreover {
1823     assume "?c = 0"
1824     then have ?case using eqs by auto
1825   }
1826   moreover {
1827     assume cp: "?c > 0"
1828     {
1829       fix x
1830       assume xz: "x < -?e / ?c"
1831       then have "?c * x < - ?e"
1832         using pos_less_divide_eq[OF cp, where a="x" and b="-?e"]
1834       then have "?c * x + ?e < 0"
1835         by simp
1836       then have "Ifm vs (x#bs) (Le (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Le (CNP 0 c e)))"
1837         using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs
1838         by auto
1839     }
1840     then have ?case by auto
1841   }
1842   moreover {
1843     assume cp: "?c < 0"
1844     {
1845       fix x
1846       assume xz: "x < -?e / ?c"
1847       then have "?c * x > - ?e"
1848         using neg_less_divide_eq[OF cp, where a="x" and b="-?e"]
1850       then have "?c * x + ?e > 0"
1851         by simp
1852       then have "Ifm vs (x#bs) (Le (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Le (CNP 0 c e)))"
1853         using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs
1854         by auto
1855     }
1856     then have ?case by auto
1857   }
1858   ultimately show ?case by blast
1859 qed auto
1861 lemma plusinf_inf:
1862   assumes lp: "islin p"
1863   shows "\<exists>z. \<forall>x > z. Ifm vs (x#bs) (plusinf p) \<longleftrightarrow> Ifm vs (x#bs) p"
1864   using lp
1865 proof (induct p rule: plusinf.induct)
1866   case 1
1867   then show ?case
1868     apply auto
1869     apply (rule_tac x="max z za" in exI)
1870     apply auto
1871     done
1872 next
1873   case 2
1874   then show ?case
1875     apply auto
1876     apply (rule_tac x="max z za" in exI)
1877     apply auto
1878     done
1879 next
1880   case (3 c e)
1881   then have nbe: "tmbound0 e"
1882     by simp
1883   from 3 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e"
1884     by simp_all
1885   note eqs = eq[OF nc(1), where ?'a = 'a] eq[OF nc(2), where ?'a = 'a]
1886   let ?c = "Ipoly vs c"
1887   fix y
1888   let ?e = "Itm vs (y#bs) e"
1889   have "?c=0 \<or> ?c > 0 \<or> ?c < 0" by arith
1890   moreover {
1891     assume "?c = 0"
1892     then have ?case
1893       using eq[OF nc(2), of vs] eq[OF nc(1), of vs] by auto
1894   }
1895   moreover {
1896     assume cp: "?c > 0"
1897     {
1898       fix x
1899       assume xz: "x > -?e / ?c"
1900       then have "?c * x > - ?e"
1901         using pos_divide_less_eq[OF cp, where a="x" and b="-?e"]
1903       then have "?c * x + ?e > 0"
1904         by simp
1905       then have "Ifm vs (x#bs) (Eq (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (Eq (CNP 0 c e)))"
1906         using eqs tmbound0_I[OF nbe, where b="y" and b'="x" and vs=vs and bs=bs] by auto
1907     }
1908     then have ?case by auto
1909   }
1910   moreover {
1911     assume cp: "?c < 0"
1912     {
1913       fix x
1914       assume xz: "x > -?e / ?c"
1915       then have "?c * x < - ?e"
1916         using neg_divide_less_eq[OF cp, where a="x" and b="-?e"]
1918       then have "?c * x + ?e < 0" by simp
1919       then have "Ifm vs (x#bs) (Eq (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (Eq (CNP 0 c e)))"
1920         using tmbound0_I[OF nbe, where b="y" and b'="x"] eqs by auto
1921     }
1922     then have ?case by auto
1923   }
1924   ultimately show ?case by blast
1925 next
1926   case (4 c e)
1927   then have nbe: "tmbound0 e"
1928     by simp
1929   from 4 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e"
1930     by simp_all
1931   note eqs = eq[OF nc(1), where ?'a = 'a] eq[OF nc(2), where ?'a = 'a]
1932   let ?c = "Ipoly vs c"
1933   fix y
1934   let ?e = "Itm vs (y#bs) e"
1935   have "?c=0 \<or> ?c > 0 \<or> ?c < 0" by arith
1936   moreover {
1937     assume "?c = 0"
1938     then have ?case using eqs by auto
1939   }
1940   moreover {
1941     assume cp: "?c > 0"
1942     {
1943       fix x
1944       assume xz: "x > -?e / ?c"
1945       then have "?c * x > - ?e"
1946         using pos_divide_less_eq[OF cp, where a="x" and b="-?e"]
1948       then have "?c * x + ?e > 0"
1949         by simp
1950       then have "Ifm vs (x#bs) (NEq (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (NEq (CNP 0 c e)))"
1951         using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] by auto
1952     }
1953     then have ?case by auto
1954   }
1955   moreover {
1956     assume cp: "?c < 0"
1957     {
1958       fix x
1959       assume xz: "x > -?e / ?c"
1960       then have "?c * x < - ?e"
1961         using neg_divide_less_eq[OF cp, where a="x" and b="-?e"]
1963       then have "?c * x + ?e < 0"
1964         by simp
1965       then have "Ifm vs (x#bs) (NEq (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (NEq (CNP 0 c e)))"
1966         using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] by auto
1967     }
1968     then have ?case by auto
1969   }
1970   ultimately show ?case by blast
1971 next
1972   case (5 c e)
1973   then have nbe: "tmbound0 e"
1974     by simp
1975   from 5 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e"
1976     by simp_all
1977   then have nc': "allpolys isnpoly (CP (~\<^sub>p c))"
1979   note eqs = lt[OF nc(1), where ?'a = 'a] lt[OF nc', where ?'a = 'a] eq [OF nc(1), where ?'a = 'a] lt[OF nc(2), where ?'a = 'a]
1980   let ?c = "Ipoly vs c"
1981   fix y
1982   let ?e = "Itm vs (y#bs) e"
1983   have "?c = 0 \<or> ?c > 0 \<or> ?c < 0" by arith
1984   moreover {
1985     assume "?c = 0"
1986     then have ?case using eqs by auto
1987   }
1988   moreover {
1989     assume cp: "?c > 0"
1990     {
1991       fix x
1992       assume xz: "x > -?e / ?c"
1993       then have "?c * x > - ?e"
1994         using pos_divide_less_eq[OF cp, where a="x" and b="-?e"]
1996       then have "?c * x + ?e > 0"
1997         by simp
1998       then have "Ifm vs (x#bs) (Lt (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (Lt (CNP 0 c e)))"
1999         using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto
2000     }
2001     then have ?case by auto
2002   }
2003   moreover {
2004     assume cp: "?c < 0"
2005     {
2006       fix x
2007       assume xz: "x > -?e / ?c"
2008       then have "?c * x < - ?e"
2009         using neg_divide_less_eq[OF cp, where a="x" and b="-?e"]
2011       then have "?c * x + ?e < 0"
2012         by simp
2013       then have "Ifm vs (x#bs) (Lt (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (Lt (CNP 0 c e)))"
2014         using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] cp by auto
2015     }
2016     then have ?case by auto
2017   }
2018   ultimately show ?case by blast
2019 next
2020   case (6 c e)
2021   then have nbe: "tmbound0 e"
2022     by simp
2023   from 6 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e"
2024     by simp_all
2025   then have nc': "allpolys isnpoly (CP (~\<^sub>p c))"
2027   note eqs = lt[OF nc(1), where ?'a = 'a] eq [OF nc(1), where ?'a = 'a] le[OF nc(2), where ?'a = 'a]
2028   let ?c = "Ipoly vs c"
2029   fix y
2030   let ?e = "Itm vs (y#bs) e"
2031   have "?c = 0 \<or> ?c > 0 \<or> ?c < 0" by arith
2032   moreover {
2033     assume "?c = 0"
2034     then have ?case using eqs by auto
2035   }
2036   moreover {
2037     assume cp: "?c > 0"
2038     {
2039       fix x
2040       assume xz: "x > -?e / ?c"
2041       then have "?c * x > - ?e"
2042         using pos_divide_less_eq[OF cp, where a="x" and b="-?e"]
2044       then have "?c * x + ?e > 0"
2045         by simp
2046       then have "Ifm vs (x#bs) (Le (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (Le (CNP 0 c e)))"
2047         using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto
2048     }
2049     then have ?case by auto
2050   }
2051   moreover {
2052     assume cp: "?c < 0"
2053     {
2054       fix x
2055       assume xz: "x > -?e / ?c"
2056       then have "?c * x < - ?e"
2057         using neg_divide_less_eq[OF cp, where a="x" and b="-?e"]
2059       then have "?c * x + ?e < 0"
2060         by simp
2061       then have "Ifm vs (x#bs) (Le (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (Le (CNP 0 c e)))"
2062         using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto
2063     }
2064     then have ?case by auto
2065   }
2066   ultimately show ?case by blast
2067 qed auto
2069 lemma minusinf_nb: "islin p \<Longrightarrow> bound0 (minusinf p)"
2070   by (induct p rule: minusinf.induct) (auto simp add: eq_nb lt_nb le_nb)
2072 lemma plusinf_nb: "islin p \<Longrightarrow> bound0 (plusinf p)"
2073   by (induct p rule: minusinf.induct) (auto simp add: eq_nb lt_nb le_nb)
2075 lemma minusinf_ex:
2076   assumes lp: "islin p"
2077     and ex: "Ifm vs (x#bs) (minusinf p)"
2078   shows "\<exists>x. Ifm vs (x#bs) p"
2079 proof -
2080   from bound0_I [OF minusinf_nb[OF lp], where bs ="bs"] ex
2081   have th: "\<forall>x. Ifm vs (x#bs) (minusinf p)"
2082     by auto
2083   from minusinf_inf[OF lp, where bs="bs"]
2084   obtain z where z: "\<forall>x<z. Ifm vs (x # bs) (minusinf p) = Ifm vs (x # bs) p"
2085     by blast
2086   from th have "Ifm vs ((z - 1)#bs) (minusinf p)"
2087     by simp
2088   moreover have "z - 1 < z"
2089     by simp
2090   ultimately show ?thesis
2091     using z by auto
2092 qed
2094 lemma plusinf_ex:
2095   assumes lp: "islin p"
2096     and ex: "Ifm vs (x#bs) (plusinf p)"
2097   shows "\<exists>x. Ifm vs (x#bs) p"
2098 proof -
2099   from bound0_I [OF plusinf_nb[OF lp], where bs ="bs"] ex
2100   have th: "\<forall>x. Ifm vs (x#bs) (plusinf p)"
2101     by auto
2102   from plusinf_inf[OF lp, where bs="bs"]
2103   obtain z where z: "\<forall>x>z. Ifm vs (x # bs) (plusinf p) = Ifm vs (x # bs) p"
2104     by blast
2105   from th have "Ifm vs ((z + 1)#bs) (plusinf p)"
2106     by simp
2107   moreover have "z + 1 > z"
2108     by simp
2109   ultimately show ?thesis
2110     using z by auto
2111 qed
2113 fun uset :: "fm \<Rightarrow> (poly \<times> tm) list"
2114 where
2115   "uset (And p q) = uset p @ uset q"
2116 | "uset (Or p q) = uset p @ uset q"
2117 | "uset (Eq (CNP 0 a e)) = [(a, e)]"
2118 | "uset (Le (CNP 0 a e)) = [(a, e)]"
2119 | "uset (Lt (CNP 0 a e)) = [(a, e)]"
2120 | "uset (NEq (CNP 0 a e)) = [(a, e)]"
2121 | "uset p = []"
2123 lemma uset_l:
2124   assumes lp: "islin p"
2125   shows "\<forall>(c,s) \<in> set (uset p). isnpoly c \<and> c \<noteq> 0\<^sub>p \<and> tmbound0 s \<and> allpolys isnpoly s"
2126   using lp by (induct p rule: uset.induct) auto
2128 lemma minusinf_uset0:
2129   assumes lp: "islin p"
2130     and nmi: "\<not> (Ifm vs (x#bs) (minusinf p))"
2131     and ex: "Ifm vs (x#bs) p" (is "?I x p")
2132   shows "\<exists>(c, s) \<in> set (uset p). x \<ge> - Itm vs (x#bs) s / Ipoly vs c"
2133 proof -
2134   have "\<exists>(c, s) \<in> set (uset p).
2135       Ipoly vs c < 0 \<and> Ipoly vs c * x \<le> - Itm vs (x#bs) s \<or>
2136       Ipoly vs c > 0 \<and> Ipoly vs c * x \<ge> - Itm vs (x#bs) s"
2137     using lp nmi ex
2138     apply (induct p rule: minusinf.induct)
2139     apply (auto simp add: eq le lt polyneg_norm)
2140     apply (auto simp add: linorder_not_less order_le_less)
2141     done
2142   then obtain c s where csU: "(c, s) \<in> set (uset p)"
2143     and x: "(Ipoly vs c < 0 \<and> Ipoly vs c * x \<le> - Itm vs (x#bs) s) \<or>
2144       (Ipoly vs c > 0 \<and> Ipoly vs c * x \<ge> - Itm vs (x#bs) s)" by blast
2145   then have "x \<ge> (- Itm vs (x#bs) s) / Ipoly vs c"
2146     using divide_le_eq[of "- Itm vs (x#bs) s" "Ipoly vs c" x]
2147     by (auto simp add: mult_commute)
2148   then show ?thesis
2149     using csU by auto
2150 qed
2152 lemma minusinf_uset:
2153   assumes lp: "islin p"
2154     and nmi: "\<not> (Ifm vs (a#bs) (minusinf p))"
2155     and ex: "Ifm vs (x#bs) p" (is "?I x p")
2156   shows "\<exists>(c,s) \<in> set (uset p). x \<ge> - Itm vs (a#bs) s / Ipoly vs c"
2157 proof -
2158   from nmi have nmi': "\<not> Ifm vs (x#bs) (minusinf p)"
2159     by (simp add: bound0_I[OF minusinf_nb[OF lp], where b=x and b'=a])
2160   from minusinf_uset0[OF lp nmi' ex]
2161   obtain c s where csU: "(c,s) \<in> set (uset p)"
2162     and th: "x \<ge> - Itm vs (x#bs) s / Ipoly vs c"
2163     by blast
2164   from uset_l[OF lp, rule_format, OF csU] have nb: "tmbound0 s"
2165     by simp
2166   from th tmbound0_I[OF nb, of vs x bs a] csU show ?thesis
2167     by auto
2168 qed
2171 lemma plusinf_uset0:
2172   assumes lp: "islin p"
2173     and nmi: "\<not> (Ifm vs (x#bs) (plusinf p))"
2174     and ex: "Ifm vs (x#bs) p" (is "?I x p")
2175   shows "\<exists>(c, s) \<in> set (uset p). x \<le> - Itm vs (x#bs) s / Ipoly vs c"
2176 proof-
2177   have "\<exists>(c, s) \<in> set (uset p).
2178       Ipoly vs c < 0 \<and> Ipoly vs c * x \<ge> - Itm vs (x#bs) s \<or>
2179       Ipoly vs c > 0 \<and> Ipoly vs c * x \<le> - Itm vs (x#bs) s"
2180     using lp nmi ex
2181     apply (induct p rule: minusinf.induct)
2182     apply (auto simp add: eq le lt polyneg_norm)
2183     apply (auto simp add: linorder_not_less order_le_less)
2184     done
2185   then obtain c s where csU: "(c, s) \<in> set (uset p)"
2186     and x: "Ipoly vs c < 0 \<and> Ipoly vs c * x \<ge> - Itm vs (x#bs) s \<or>
2187       Ipoly vs c > 0 \<and> Ipoly vs c * x \<le> - Itm vs (x#bs) s"
2188     by blast
2189   then have "x \<le> (- Itm vs (x#bs) s) / Ipoly vs c"
2190     using le_divide_eq[of x "- Itm vs (x#bs) s" "Ipoly vs c"]
2191     by (auto simp add: mult_commute)
2192   then show ?thesis
2193     using csU by auto
2194 qed
2196 lemma plusinf_uset:
2197   assumes lp: "islin p"
2198     and nmi: "\<not> (Ifm vs (a#bs) (plusinf p))"
2199     and ex: "Ifm vs (x#bs) p" (is "?I x p")
2200   shows "\<exists>(c,s) \<in> set (uset p). x \<le> - Itm vs (a#bs) s / Ipoly vs c"
2201 proof -
2202   from nmi have nmi': "\<not> (Ifm vs (x#bs) (plusinf p))"
2203     by (simp add: bound0_I[OF plusinf_nb[OF lp], where b=x and b'=a])
2204   from plusinf_uset0[OF lp nmi' ex]
2205   obtain c s where csU: "(c,s) \<in> set (uset p)"
2206     and th: "x \<le> - Itm vs (x#bs) s / Ipoly vs c"
2207     by blast
2208   from uset_l[OF lp, rule_format, OF csU] have nb: "tmbound0 s"
2209     by simp
2210   from th tmbound0_I[OF nb, of vs x bs a] csU show ?thesis
2211     by auto
2212 qed
2214 lemma lin_dense:
2215   assumes lp: "islin p"
2216     and noS: "\<forall>t. l < t \<and> t< u \<longrightarrow> t \<notin> (\<lambda>(c,t). - Itm vs (x#bs) t / Ipoly vs c) ` set (uset p)"
2217       (is "\<forall>t. _ \<and> _ \<longrightarrow> t \<notin> (\<lambda>(c,t). - ?Nt x t / ?N c) ` ?U p")
2218     and lx: "l < x" and xu:"x < u" and px:" Ifm vs (x#bs) p"
2219     and ly: "l < y" and yu: "y < u"
2220   shows "Ifm vs (y#bs) p"
2221   using lp px noS
2222 proof (induct p rule: islin.induct)
2223   case (5 c s)
2224   from "5.prems"
2225   have lin: "isnpoly c" "c \<noteq> 0\<^sub>p" "tmbound0 s" "allpolys isnpoly s"
2226     and px: "Ifm vs (x # bs) (Lt (CNP 0 c s))"
2227     and noS: "\<forall>t. l < t \<and> t < u \<longrightarrow> t \<noteq> - Itm vs (x # bs) s / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup>"
2228     by simp_all
2229   from ly yu noS have yne: "y \<noteq> - ?Nt x s / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup>"
2230     by simp
2231   then have ycs: "y < - ?Nt x s / ?N c \<or> y > -?Nt x s / ?N c"
2232     by auto
2233   have ccs: "?N c = 0 \<or> ?N c < 0 \<or> ?N c > 0"
2234     by dlo
2235   moreover
2236   {
2237     assume "?N c = 0"
2238     then have ?case
2239       using px by (simp add: tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"])
2240   }
2241   moreover
2242   {
2243     assume c: "?N c > 0"
2244     from px pos_less_divide_eq[OF c, where a="x" and b="-?Nt x s"]
2245     have px': "x < - ?Nt x s / ?N c"
2246       by (auto simp add: not_less field_simps)
2247     {
2248       assume y: "y < - ?Nt x s / ?N c"
2249       then have "y * ?N c < - ?Nt x s"
2250         by (simp add: pos_less_divide_eq[OF c, where a="y" and b="-?Nt x s", symmetric])
2251       then have "?N c * y + ?Nt x s < 0"
2253       then have ?case using tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"]
2254         by simp
2255     }
2256     moreover
2257     {
2258       assume y: "y > -?Nt x s / ?N c"
2259       with yu have eu: "u > - ?Nt x s / ?N c"
2260         by auto
2261       with noS ly yu have th: "- ?Nt x s / ?N c \<le> l"
2262         by (cases "- ?Nt x s / ?N c > l") auto
2263       with lx px' have False
2264         by simp
2265       then have ?case ..
2266     }
2267     ultimately have ?case
2268       using ycs by blast
2269   }
2270   moreover
2271   {
2272     assume c: "?N c < 0"
2273     from px neg_divide_less_eq[OF c, where a="x" and b="-?Nt x s"]
2274     have px': "x > - ?Nt x s / ?N c"
2275       by (auto simp add: not_less field_simps)
2276     {
2277       assume y: "y > - ?Nt x s / ?N c"
2278       then have "y * ?N c < - ?Nt x s"
2279         by (simp add: neg_divide_less_eq[OF c, where a="y" and b="-?Nt x s", symmetric])
2280       then have "?N c * y + ?Nt x s < 0"
2282       then have ?case using tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"]
2283         by simp
2284     }
2285     moreover
2286     {
2287       assume y: "y < -?Nt x s / ?N c"
2288       with ly have eu: "l < - ?Nt x s / ?N c"
2289         by auto
2290       with noS ly yu have th: "- ?Nt x s / ?N c \<ge> u"
2291         by (cases "- ?Nt x s / ?N c < u") auto
2292       with xu px' have False
2293         by simp
2294       then have ?case ..
2295     }
2296     ultimately have ?case
2297       using ycs by blast
2298   }
2299   ultimately show ?case
2300     by blast
2301 next
2302   case (6 c s)
2303   from "6.prems"
2304   have lin: "isnpoly c" "c \<noteq> 0\<^sub>p" "tmbound0 s" "allpolys isnpoly s"
2305     and px: "Ifm vs (x # bs) (Le (CNP 0 c s))"
2306     and noS: "\<forall>t. l < t \<and> t < u \<longrightarrow> t \<noteq> - Itm vs (x # bs) s / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup>"
2307     by simp_all
2308   from ly yu noS have yne: "y \<noteq> - ?Nt x s / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup>"
2309     by simp
2310   then have ycs: "y < - ?Nt x s / ?N c \<or> y > -?Nt x s / ?N c"
2311     by auto
2312   have ccs: "?N c = 0 \<or> ?N c < 0 \<or> ?N c > 0" by dlo
2313   moreover
2314   {
2315     assume "?N c = 0"
2316     then have ?case
2317       using px by (simp add: tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"])
2318   }
2319   moreover
2320   {
2321     assume c: "?N c > 0"
2322     from px pos_le_divide_eq[OF c, where a="x" and b="-?Nt x s"]
2323     have px': "x \<le> - ?Nt x s / ?N c"
2324       by (simp add: not_less field_simps)
2325     {
2326       assume y: "y < - ?Nt x s / ?N c"
2327       then have "y * ?N c < - ?Nt x s"
2328         by (simp add: pos_less_divide_eq[OF c, where a="y" and b="-?Nt x s", symmetric])
2329       then have "?N c * y + ?Nt x s < 0"
2331       then have ?case
2332         using tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"] by simp
2333     }
2334     moreover
2335     {
2336       assume y: "y > -?Nt x s / ?N c"
2337       with yu have eu: "u > - ?Nt x s / ?N c"
2338         by auto
2339       with noS ly yu have th: "- ?Nt x s / ?N c \<le> l"
2340         by (cases "- ?Nt x s / ?N c > l") auto
2341       with lx px' have False
2342         by simp
2343       then have ?case ..
2344     }
2345     ultimately have ?case
2346       using ycs by blast
2347   }
2348   moreover
2349   {
2350     assume c: "?N c < 0"
2351     from px neg_divide_le_eq[OF c, where a="x" and b="-?Nt x s"]
2352     have px': "x >= - ?Nt x s / ?N c"
2354     {
2355       assume y: "y > - ?Nt x s / ?N c"
2356       then have "y * ?N c < - ?Nt x s"
2357         by (simp add: neg_divide_less_eq[OF c, where a="y" and b="-?Nt x s", symmetric])
2358       then have "?N c * y + ?Nt x s < 0"
2360       then have ?case
2361         using tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"] by simp
2362     }
2363     moreover
2364     {
2365       assume y: "y < -?Nt x s / ?N c"
2366       with ly have eu: "l < - ?Nt x s / ?N c"
2367         by auto
2368       with noS ly yu have th: "- ?Nt x s / ?N c \<ge> u"
2369         by (cases "- ?Nt x s / ?N c < u") auto
2370       with xu px' have False by simp
2371       then have ?case ..
2372     }
2373     ultimately have ?case
2374       using ycs by blast
2375   }
2376   ultimately show ?case
2377     by blast
2378 next
2379   case (3 c s)
2380   from "3.prems"
2381   have lin: "isnpoly c" "c \<noteq> 0\<^sub>p" "tmbound0 s" "allpolys isnpoly s"
2382     and px: "Ifm vs (x # bs) (Eq (CNP 0 c s))"
2383     and noS: "\<forall>t. l < t \<and> t < u \<longrightarrow> t \<noteq> - Itm vs (x # bs) s / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup>"
2384     by simp_all
2385   from ly yu noS have yne: "y \<noteq> - ?Nt x s / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup>"
2386     by simp
2387   then have ycs: "y < - ?Nt x s / ?N c \<or> y > -?Nt x s / ?N c"
2388     by auto
2389   have ccs: "?N c = 0 \<or> ?N c < 0 \<or> ?N c > 0" by dlo
2390   moreover
2391   {
2392     assume "?N c = 0"
2393     then have ?case
2394       using px by (simp add: tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"])
2395   }
2396   moreover
2397   {
2398     assume c: "?N c > 0"
2399     then have cnz: "?N c \<noteq> 0"
2400       by simp
2401     from px eq_divide_eq[of "x" "-?Nt x s" "?N c"] cnz
2402     have px': "x = - ?Nt x s / ?N c"
2404     {
2405       assume y: "y < -?Nt x s / ?N c"
2406       with ly have eu: "l < - ?Nt x s / ?N c"
2407         by auto
2408       with noS ly yu have th: "- ?Nt x s / ?N c \<ge> u"
2409         by (cases "- ?Nt x s / ?N c < u") auto
2410       with xu px' have False by simp
2411       then have ?case ..
2412     }
2413     moreover
2414     {
2415       assume y: "y > -?Nt x s / ?N c"
2416       with yu have eu: "u > - ?Nt x s / ?N c"
2417         by auto
2418       with noS ly yu have th: "- ?Nt x s / ?N c \<le> l"
2419         by (cases "- ?Nt x s / ?N c > l") auto
2420       with lx px' have False by simp
2421       then have ?case ..
2422     }
2423     ultimately have ?case
2424       using ycs by blast
2425   }
2426   moreover
2427   {
2428     assume c: "?N c < 0"
2429     then have cnz: "?N c \<noteq> 0"
2430       by simp
2431     from px eq_divide_eq[of "x" "-?Nt x s" "?N c"] cnz
2432     have px': "x = - ?Nt x s / ?N c"
2434     {
2435       assume y: "y < -?Nt x s / ?N c"
2436       with ly have eu: "l < - ?Nt x s / ?N c"
2437         by auto
2438       with noS ly yu have th: "- ?Nt x s / ?N c \<ge> u"
2439         by (cases "- ?Nt x s / ?N c < u") auto
2440       with xu px' have False by simp
2441       then have ?case ..
2442     }
2443     moreover
2444     {
2445       assume y: "y > -?Nt x s / ?N c"
2446       with yu have eu: "u > - ?Nt x s / ?N c"
2447         by auto
2448       with noS ly yu have th: "- ?Nt x s / ?N c \<le> l"
2449         by (cases "- ?Nt x s / ?N c > l") auto
2450       with lx px' have False by simp
2451       then have ?case ..
2452     }
2453     ultimately have ?case using ycs by blast
2454   }
2455   ultimately show ?case by blast
2456 next
2457     case (4 c s)
2458   from "4.prems"
2459   have lin: "isnpoly c" "c \<noteq> 0\<^sub>p" "tmbound0 s" "allpolys isnpoly s"
2460     and px: "Ifm vs (x # bs) (NEq (CNP 0 c s))"
2461     and noS: "\<forall>t. l < t \<and> t < u \<longrightarrow> t \<noteq> - Itm vs (x # bs) s / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup>"
2462     by simp_all
2463   from ly yu noS have yne: "y \<noteq> - ?Nt x s / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup>"
2464     by simp
2465   then have ycs: "y < - ?Nt x s / ?N c \<or> y > -?Nt x s / ?N c"
2466     by auto
2467   have ccs: "?N c = 0 \<or> ?N c \<noteq> 0" by dlo
2468   moreover
2469   {
2470     assume "?N c = 0"
2471     then have ?case
2472       using px by (simp add: tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"])
2473   }
2474   moreover
2475   {
2476     assume c: "?N c \<noteq> 0"
2477     from yne c eq_divide_eq[of "y" "- ?Nt x s" "?N c"]
2478     have ?case
2479       by (simp add: field_simps tmbound0_I[OF lin(3), of vs x bs y] sum_eq[symmetric])
2480   }
2481   ultimately show ?case
2482     by blast
2483 qed (auto simp add: tmbound0_I[where vs=vs and bs="bs" and b="y" and b'="x"] bound0_I[where vs=vs and bs="bs" and b="y" and b'="x"])
2485 lemma inf_uset:
2486   assumes lp: "islin p"
2487     and nmi: "\<not> (Ifm vs (x#bs) (minusinf p))" (is "\<not> (Ifm vs (x#bs) (?M p))")
2488     and npi: "\<not> (Ifm vs (x#bs) (plusinf p))" (is "\<not> (Ifm vs (x#bs) (?P p))")
2489     and ex: "\<exists>x.  Ifm vs (x#bs) p" (is "\<exists>x. ?I x p")
2490   shows "\<exists>(c, t) \<in> set (uset p). \<exists>(d, s) \<in> set (uset p).
2491     ?I ((- Itm vs (x#bs) t / Ipoly vs c + - Itm vs (x#bs) s / Ipoly vs d) / 2) p"
2492 proof -
2493   let ?Nt = "\<lambda>x t. Itm vs (x#bs) t"
2494   let ?N = "Ipoly vs"
2495   let ?U = "set (uset p)"
2496   from ex obtain a where pa: "?I a p"
2497     by blast
2498   from bound0_I[OF minusinf_nb[OF lp], where bs="bs" and b="x" and b'="a"] nmi
2499   have nmi': "\<not> (?I a (?M p))"
2500     by simp
2501   from bound0_I[OF plusinf_nb[OF lp], where bs="bs" and b="x" and b'="a"] npi
2502   have npi': "\<not> (?I a (?P p))"
2503     by simp
2504   have "\<exists>(c,t) \<in> set (uset p). \<exists>(d,s) \<in> set (uset p). ?I ((- ?Nt a t/?N c + - ?Nt a s /?N d) / 2) p"
2505   proof -
2506     let ?M = "(\<lambda>(c,t). - ?Nt a t / ?N c) ` ?U"
2507     have fM: "finite ?M"
2508       by auto
2509     from minusinf_uset[OF lp nmi pa] plusinf_uset[OF lp npi pa]
2510     have "\<exists>(c, t) \<in> set (uset p). \<exists>(d, s) \<in> set (uset p).
2511         a \<le> - ?Nt x t / ?N c \<and> a \<ge> - ?Nt x s / ?N d"
2512       by blast
2513     then obtain "c" "t" "d" "s"
2514       where ctU: "(c,t) \<in> ?U"
2515         and dsU: "(d,s) \<in> ?U"
2516         and xs1: "a \<le> - ?Nt x s / ?N d"
2517         and tx1: "a \<ge> - ?Nt x t / ?N c"
2518       by blast
2519     from uset_l[OF lp] ctU dsU tmbound0_I[where bs="bs" and b="x" and b'="a"] xs1 tx1
2520     have xs: "a \<le> - ?Nt a s / ?N d" and tx: "a \<ge> - ?Nt a t / ?N c"
2521       by auto
2522     from ctU have Mne: "?M \<noteq> {}" by auto
2523     then have Une: "?U \<noteq> {}" by simp
2524     let ?l = "Min ?M"
2525     let ?u = "Max ?M"
2526     have linM: "?l \<in> ?M"
2527       using fM Mne by simp
2528     have uinM: "?u \<in> ?M"
2529       using fM Mne by simp
2530     have ctM: "- ?Nt a t / ?N c \<in> ?M"
2531       using ctU by auto
2532     have dsM: "- ?Nt a s / ?N d \<in> ?M"
2533       using dsU by auto
2534     have lM: "\<forall>t\<in> ?M. ?l \<le> t"
2535       using Mne fM by auto
2536     have Mu: "\<forall>t\<in> ?M. t \<le> ?u"
2537       using Mne fM by auto
2538     have "?l \<le> - ?Nt a t / ?N c"
2539       using ctM Mne by simp
2540     then have lx: "?l \<le> a"
2541       using tx by simp
2542     have "- ?Nt a s / ?N d \<le> ?u"
2543       using dsM Mne by simp
2544     then have xu: "a \<le> ?u"
2545       using xs by simp
2546     from finite_set_intervals2[where P="\<lambda>x. ?I x p",OF pa lx xu linM uinM fM lM Mu]
2547     have "(\<exists>s\<in> ?M. ?I s p) \<or>
2548       (\<exists>t1\<in> ?M. \<exists>t2 \<in> ?M. (\<forall>y. t1 < y \<and> y < t2 \<longrightarrow> y \<notin> ?M) \<and> t1 < a \<and> a < t2 \<and> ?I a p)" .
2549     moreover {
2550       fix u
2551       assume um: "u\<in> ?M"
2552         and pu: "?I u p"
2553       then have "\<exists>(nu,tu) \<in> ?U. u = - ?Nt a tu / ?N nu"
2554         by auto
2555       then obtain tu nu where tuU: "(nu, tu) \<in> ?U"
2556         and tuu:"u= - ?Nt a tu / ?N nu"
2557         by blast
2558       from pu tuu have "?I (((- ?Nt a tu / ?N nu) + (- ?Nt a tu / ?N nu)) / 2) p"
2559         by simp
2560       with tuU have ?thesis by blast
2561     }
2562     moreover {
2563       assume "\<exists>t1\<in> ?M. \<exists>t2 \<in> ?M. (\<forall>y. t1 < y \<and> y < t2 \<longrightarrow> y \<notin> ?M) \<and> t1 < a \<and> a < t2 \<and> ?I a p"
2564       then obtain t1 t2
2565         where t1M: "t1 \<in> ?M"
2566           and t2M: "t2\<in> ?M"
2567           and noM: "\<forall>y. t1 < y \<and> y < t2 \<longrightarrow> y \<notin> ?M"
2568           and t1x: "t1 < a"
2569           and xt2: "a < t2"
2570           and px: "?I a p"
2571         by blast
2572       from t1M have "\<exists>(t1n, t1u) \<in> ?U. t1 = - ?Nt a t1u / ?N t1n"
2573         by auto
2574       then obtain t1u t1n where t1uU: "(t1n, t1u) \<in> ?U"
2575         and t1u: "t1 = - ?Nt a t1u / ?N t1n"
2576         by blast
2577       from t2M have "\<exists>(t2n, t2u) \<in> ?U. t2 = - ?Nt a t2u / ?N t2n"
2578         by auto
2579       then obtain t2u t2n where t2uU: "(t2n, t2u) \<in> ?U"
2580         and t2u: "t2 = - ?Nt a t2u / ?N t2n"
2581         by blast
2582       from t1x xt2 have t1t2: "t1 < t2" by simp
2583       let ?u = "(t1 + t2) / 2"
2584       from less_half_sum[OF t1t2] gt_half_sum[OF t1t2] have t1lu: "t1 < ?u" and ut2: "?u < t2"
2585         by auto
2586       from lin_dense[OF lp noM t1x xt2 px t1lu ut2] have "?I ?u p" .
2587       with t1uU t2uU t1u t2u have ?thesis by blast
2588     }
2589     ultimately show ?thesis by blast
2590   qed
2591   then obtain l n s  m
2592     where lnU: "(n, l) \<in> ?U"
2593       and smU:"(m,s) \<in> ?U"
2594       and pu: "?I ((- ?Nt a l / ?N n + - ?Nt a s / ?N m) / 2) p"
2595     by blast
2596   from lnU smU uset_l[OF lp] have nbl: "tmbound0 l" and nbs: "tmbound0 s"
2597     by auto
2598   from tmbound0_I[OF nbl, where bs="bs" and b="a" and b'="x"]
2599     tmbound0_I[OF nbs, where bs="bs" and b="a" and b'="x"] pu
2600   have "?I ((- ?Nt x l / ?N n + - ?Nt x s / ?N m) / 2) p"
2601     by simp
2602   with lnU smU show ?thesis by auto
2603 qed
2605 (* The Ferrante - Rackoff Theorem *)
2607 theorem fr_eq:
2608   assumes lp: "islin p"
2609   shows "(\<exists>x. Ifm vs (x#bs) p) \<longleftrightarrow>
2610     (Ifm vs (x#bs) (minusinf p) \<or>
2611      Ifm vs (x#bs) (plusinf p) \<or>
2612      (\<exists>(n, t) \<in> set (uset p). \<exists>(m, s) \<in> set (uset p).
2613        Ifm vs (((- Itm vs (x#bs) t /  Ipoly vs n + - Itm vs (x#bs) s / Ipoly vs m) / 2)#bs) p))"
2614   (is "(\<exists>x. ?I x p) = (?M \<or> ?P \<or> ?F)" is "?E = ?D")
2615 proof
2616   assume px: "\<exists>x. ?I x p"
2617   have "?M \<or> ?P \<or> (\<not> ?M \<and> \<not> ?P)"
2618     by blast
2619   moreover {
2620     assume "?M \<or> ?P"
2621     then have "?D" by blast
2622   }
2623   moreover {
2624     assume nmi: "\<not> ?M"
2625       and npi: "\<not> ?P"
2626     from inf_uset[OF lp nmi npi] have ?F
2627       using px by blast
2628     then have ?D by blast
2629   }
2630   ultimately show ?D by blast
2631 next
2632   assume ?D
2633   moreover {
2634     assume m: ?M
2635     from minusinf_ex[OF lp m] have ?E .
2636   }
2637   moreover {
2638     assume p: ?P
2639     from plusinf_ex[OF lp p] have ?E .
2640   }
2641   moreover {
2642     assume f: ?F
2643     then have ?E by blast
2644   }
2645   ultimately show ?E by blast
2646 qed
2649 section {* First implementation : Naive by encoding all case splits locally *}
2651 definition "msubsteq c t d s a r =
2652   evaldjf (split conj)
2653   [(let cd = c *\<^sub>p d
2654     in (NEq (CP cd), Eq (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))),
2655    (conj (Eq (CP c)) (NEq (CP d)), Eq (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
2656    (conj (NEq (CP c)) (Eq (CP d)), Eq (Add (Mul (~\<^sub>p a) t) (Mul ((2)\<^sub>p *\<^sub>p c) r))),
2657    (conj (Eq (CP c)) (Eq (CP d)), Eq r)]"
2659 lemma msubsteq_nb:
2660   assumes lp: "islin (Eq (CNP 0 a r))"
2661     and t: "tmbound0 t"
2662     and s: "tmbound0 s"
2663   shows "bound0 (msubsteq c t d s a r)"
2664 proof -
2665   have th: "\<forall>x \<in> set
2666     [(let cd = c *\<^sub>p d
2667       in (NEq (CP cd), Eq (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))),
2668      (conj (Eq (CP c)) (NEq (CP d)), Eq (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
2669      (conj (NEq (CP c)) (Eq (CP d)), Eq (Add (Mul (~\<^sub>p a) t) (Mul ((2)\<^sub>p *\<^sub>p c) r))),
2670      (conj (Eq (CP c)) (Eq (CP d)), Eq r)]. bound0 (split conj x)"
2671     using lp by (simp add: Let_def t s)
2672   from evaldjf_bound0[OF th] show ?thesis
2674 qed
2676 lemma msubsteq:
2677   assumes lp: "islin (Eq (CNP 0 a r))"
2678   shows "Ifm vs (x#bs) (msubsteq c t d s a r) =
2679     Ifm vs (((- Itm vs (x#bs) t /  Ipoly vs c + - Itm vs (x#bs) s / Ipoly vs d) / 2)#bs) (Eq (CNP 0 a r))"
2680   (is "?lhs = ?rhs")
2681 proof -
2682   let ?Nt = "\<lambda>x t. Itm vs (x#bs) t"
2683   let ?N = "\<lambda>p. Ipoly vs p"
2684   let ?c = "?N c"
2685   let ?d = "?N d"
2686   let ?t = "?Nt x t"
2687   let ?s = "?Nt x s"
2688   let ?a = "?N a"
2689   let ?r = "?Nt x r"
2690   from lp have lin:"isnpoly a" "a \<noteq> 0\<^sub>p" "tmbound0 r" "allpolys isnpoly r"
2691     by simp_all
2692   note r= tmbound0_I[OF lin(3), of vs _ bs x]
2693   have cd_cs: "?c * ?d \<noteq> 0 \<or> (?c = 0 \<and> ?d = 0) \<or> (?c = 0 \<and> ?d \<noteq> 0) \<or> (?c \<noteq> 0 \<and> ?d = 0)"
2694     by auto
2695   moreover
2696   {
2697     assume c: "?c = 0"
2698       and d: "?d=0"
2699     then have ?thesis
2700       by (simp add: r[of 0] msubsteq_def Let_def evaldjf_ex)
2701   }
2702   moreover
2703   {
2704     assume c: "?c = 0"
2705       and d: "?d\<noteq>0"
2706     from c have th: "(- ?t / ?c + - ?s / ?d)/2 = -?s / (2*?d)"
2707       by simp
2708     have "?rhs = Ifm vs (-?s / (2*?d) # bs) (Eq (CNP 0 a r))"
2709       by (simp only: th)
2710     also have "\<dots> \<longleftrightarrow> ?a * (-?s / (2*?d)) + ?r = 0"
2711       by (simp add: r[of "- (Itm vs (x # bs) s / (2 * \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>))"])
2712     also have "\<dots> \<longleftrightarrow> 2 * ?d * (?a * (-?s / (2*?d)) + ?r) = 0"
2713       using d mult_cancel_left[of "2*?d" "(?a * (-?s / (2*?d)) + ?r)" 0] by simp
2714     also have "\<dots> \<longleftrightarrow> (- ?a * ?s) * (2*?d / (2*?d)) + 2 * ?d * ?r= 0"
2715       by (simp add: field_simps distrib_left[of "2*?d"] del: distrib_left)
2716     also have "\<dots> \<longleftrightarrow> - (?a * ?s) + 2*?d*?r = 0"
2717       using d by simp
2718     finally have ?thesis
2719       using c d
2720       by (simp add: r[of "- (Itm vs (x # bs) s / (2 * \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>))"] msubsteq_def Let_def evaldjf_ex)
2721   }
2722   moreover
2723   {
2724     assume c: "?c \<noteq> 0"
2725       and d: "?d = 0"
2726     from d have th: "(- ?t / ?c + - ?s / ?d)/2 = -?t / (2 * ?c)"
2727       by simp
2728     have "?rhs = Ifm vs (-?t / (2*?c) # bs) (Eq (CNP 0 a r))"
2729       by (simp only: th)
2730     also have "\<dots> \<longleftrightarrow> ?a * (-?t / (2*?c)) + ?r = 0"
2731       by (simp add: r[of "- (?t/ (2 * ?c))"])
2732     also have "\<dots> \<longleftrightarrow> 2 * ?c * (?a * (-?t / (2 * ?c)) + ?r) = 0"
2733       using c mult_cancel_left[of "2 * ?c" "(?a * (-?t / (2 * ?c)) + ?r)" 0] by simp
2734     also have "\<dots> \<longleftrightarrow> (?a * -?t)* (2 * ?c) / (2 * ?c) + 2 * ?c * ?r= 0"
2735       by (simp add: field_simps distrib_left[of "2 * ?c"] del: distrib_left)
2736     also have "\<dots> \<longleftrightarrow> - (?a * ?t) + 2 * ?c * ?r = 0" using c by simp
2737     finally have ?thesis using c d
2738       by (simp add: r[of "- (?t/ (2 * ?c))"] msubsteq_def Let_def evaldjf_ex)
2739   }
2740   moreover
2741   {
2742     assume c: "?c \<noteq> 0"
2743       and d: "?d \<noteq> 0"
2744     then have dc: "?c * ?d * 2 \<noteq> 0"
2745       by simp
2746     from add_frac_eq[OF c d, of "- ?t" "- ?s"]
2747     have th: "(- ?t / ?c + - ?s / ?d)/2 = - (?d * ?t + ?c* ?s )/ (2 * ?c * ?d)"
2749     have "?rhs \<longleftrightarrow> Ifm vs (- (?d * ?t + ?c* ?s )/ (2*?c*?d) # bs) (Eq (CNP 0 a r))"
2750       by (simp only: th)
2751     also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r = 0"
2752       by (simp add: r [of "(- (?d * ?t) - (?c *?s)) / (2 * ?c * ?d)"])
2753     also have "\<dots> \<longleftrightarrow> (2 * ?c * ?d) * (?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r) = 0"
2754       using c d mult_cancel_left[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2 * ?c * ?d)) + ?r" 0]
2755       by simp
2756     also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2 * ?c * ?d * ?r = 0"
2757       using nonzero_mult_divide_cancel_left [OF dc] c d
2758       by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
2759     finally  have ?thesis using c d
2760       by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"]
2761           msubsteq_def Let_def evaldjf_ex field_simps)
2762   }
2763   ultimately show ?thesis
2764     by blast
2765 qed
2768 definition "msubstneq c t d s a r =
2769   evaldjf (split conj)
2770   [(let cd = c *\<^sub>p d
2771     in (NEq (CP cd), NEq (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))),
2772    (conj (Eq (CP c)) (NEq (CP d)), NEq (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
2773    (conj (NEq (CP c)) (Eq (CP d)), NEq (Add (Mul (~\<^sub>p a) t) (Mul ((2)\<^sub>p *\<^sub>p c) r))),
2774    (conj (Eq (CP c)) (Eq (CP d)), NEq r)]"
2776 lemma msubstneq_nb:
2777   assumes lp: "islin (NEq (CNP 0 a r))"
2778     and t: "tmbound0 t"
2779     and s: "tmbound0 s"
2780   shows "bound0 (msubstneq c t d s a r)"
2781 proof -
2782   have th: "\<forall>x\<in> set
2783    [(let cd = c *\<^sub>p d
2784      in (NEq (CP cd), NEq (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))),
2785     (conj (Eq (CP c)) (NEq (CP d)), NEq (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
2786     (conj (NEq (CP c)) (Eq (CP d)), NEq (Add (Mul (~\<^sub>p a) t) (Mul ((2)\<^sub>p *\<^sub>p c) r))),
2787     (conj (Eq (CP c)) (Eq (CP d)), NEq r)]. bound0 (split conj x)"
2788     using lp by (simp add: Let_def t s)
2789   from evaldjf_bound0[OF th] show ?thesis
2791 qed
2793 lemma msubstneq:
2794   assumes lp: "islin (Eq (CNP 0 a r))"
2795   shows "Ifm vs (x#bs) (msubstneq c t d s a r) =
2796     Ifm vs (((- Itm vs (x#bs) t /  Ipoly vs c + - Itm vs (x#bs) s / Ipoly vs d) /2)#bs) (NEq (CNP 0 a r))"
2797   (is "?lhs = ?rhs")
2798 proof -
2799   let ?Nt = "\<lambda>x t. Itm vs (x#bs) t"
2800   let ?N = "\<lambda>p. Ipoly vs p"
2801   let ?c = "?N c"
2802   let ?d = "?N d"
2803   let ?t = "?Nt x t"
2804   let ?s = "?Nt x s"
2805   let ?a = "?N a"
2806   let ?r = "?Nt x r"
2807   from lp have lin:"isnpoly a" "a \<noteq> 0\<^sub>p" "tmbound0 r" "allpolys isnpoly r"
2808     by simp_all
2809   note r = tmbound0_I[OF lin(3), of vs _ bs x]
2810   have cd_cs: "?c * ?d \<noteq> 0 \<or> (?c = 0 \<and> ?d = 0) \<or> (?c = 0 \<and> ?d \<noteq> 0) \<or> (?c \<noteq> 0 \<and> ?d = 0)"
2811     by auto
2812   moreover
2813   {
2814     assume c: "?c = 0"
2815       and d: "?d=0"
2816     then have ?thesis
2817       by (simp add: r[of 0] msubstneq_def Let_def evaldjf_ex)
2818   }
2819   moreover
2820   {
2821     assume c: "?c = 0"
2822       and d: "?d\<noteq>0"
2823     from c have th: "(- ?t / ?c + - ?s / ?d)/2 = -?s / (2 * ?d)"
2824       by simp
2825     have "?rhs = Ifm vs (-?s / (2*?d) # bs) (NEq (CNP 0 a r))"
2826       by (simp only: th)
2827     also have "\<dots> \<longleftrightarrow> ?a * (-?s / (2*?d)) + ?r \<noteq> 0"
2828       by (simp add: r[of "- (Itm vs (x # bs) s / (2 * \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>))"])
2829     also have "\<dots> \<longleftrightarrow> 2*?d * (?a * (-?s / (2*?d)) + ?r) \<noteq> 0"
2830       using d mult_cancel_left[of "2*?d" "(?a * (-?s / (2*?d)) + ?r)" 0] by simp
2831     also have "\<dots> \<longleftrightarrow> (- ?a * ?s) * (2*?d / (2*?d)) + 2*?d*?r\<noteq> 0"
2832       by (simp add: field_simps distrib_left[of "2*?d"] del: distrib_left)
2833     also have "\<dots> \<longleftrightarrow> - (?a * ?s) + 2*?d*?r \<noteq> 0"
2834       using d by simp
2835     finally have ?thesis
2836       using c d
2837       by (simp add: r[of "- (Itm vs (x # bs) s / (2 * \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>))"] msubstneq_def Let_def evaldjf_ex)
2838   }
2839   moreover
2840   {
2841     assume c: "?c \<noteq> 0"
2842       and d: "?d=0"
2843     from d have th: "(- ?t / ?c + - ?s / ?d)/2 = -?t / (2*?c)"
2844       by simp
2845     have "?rhs = Ifm vs (-?t / (2*?c) # bs) (NEq (CNP 0 a r))"
2846       by (simp only: th)
2847     also have "\<dots> \<longleftrightarrow> ?a * (-?t / (2*?c)) + ?r \<noteq> 0"
2848       by (simp add: r[of "- (?t/ (2 * ?c))"])
2849     also have "\<dots> \<longleftrightarrow> 2*?c * (?a * (-?t / (2*?c)) + ?r) \<noteq> 0"
2850       using c mult_cancel_left[of "2*?c" "(?a * (-?t / (2*?c)) + ?r)" 0] by simp
2851     also have "\<dots> \<longleftrightarrow> (?a * -?t)* (2*?c) / (2*?c) + 2*?c*?r \<noteq> 0"
2852       by (simp add: field_simps distrib_left[of "2*?c"] del: distrib_left)
2853     also have "\<dots> \<longleftrightarrow> - (?a * ?t) + 2*?c*?r \<noteq> 0"
2854       using c by simp
2855     finally have ?thesis
2856       using c d by (simp add: r[of "- (?t/ (2*?c))"] msubstneq_def Let_def evaldjf_ex)
2857   }
2858   moreover
2859   {
2860     assume c: "?c \<noteq> 0"
2861       and d: "?d \<noteq> 0"
2862     then have dc: "?c * ?d *2 \<noteq> 0"
2863       by simp
2864     from add_frac_eq[OF c d, of "- ?t" "- ?s"]
2865     have th: "(- ?t / ?c + - ?s / ?d)/2 = - (?d * ?t + ?c * ?s )/ (2 * ?c * ?d)"
2867     have "?rhs \<longleftrightarrow> Ifm vs (- (?d * ?t + ?c* ?s )/ (2*?c*?d) # bs) (NEq (CNP 0 a r))"
2868       by (simp only: th)
2869     also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r \<noteq> 0"
2870       by (simp add: r [of "(- (?d * ?t) - (?c *?s)) / (2 * ?c * ?d)"])
2871     also have "\<dots> \<longleftrightarrow> (2 * ?c * ?d) * (?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r) \<noteq> 0"
2872       using c d mult_cancel_left[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r" 0]
2873       by simp
2874     also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2*?c*?d*?r \<noteq> 0"
2875       using nonzero_mult_divide_cancel_left[OF dc] c d
2876       by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
2877     finally have ?thesis
2878       using c d
2879       by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"]
2880           msubstneq_def Let_def evaldjf_ex field_simps)
2881   }
2882   ultimately show ?thesis by blast
2883 qed
2885 definition "msubstlt c t d s a r =
2886   evaldjf (split conj)
2887   [(let cd = c *\<^sub>p d
2888     in (lt (CP (~\<^sub>p cd)), Lt (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))),
2889    (let cd = c *\<^sub>p d
2890     in (lt (CP cd), Lt (Sub (Mul a (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))),
2891    (conj (lt (CP (~\<^sub>p c))) (Eq (CP d)), Lt (Add (Mul (~\<^sub>p a) t) (Mul ((2)\<^sub>p *\<^sub>p c) r))),
2892    (conj (lt (CP c)) (Eq (CP d)), Lt (Sub (Mul a t) (Mul ((2)\<^sub>p *\<^sub>p c) r))),
2893    (conj (lt (CP (~\<^sub>p d))) (Eq (CP c)), Lt (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
2894    (conj (lt (CP d)) (Eq (CP c)), Lt (Sub (Mul a s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
2895    (conj (Eq (CP c)) (Eq (CP d)), Lt r)]"
2897 lemma msubstlt_nb:
2898   assumes lp: "islin (Lt (CNP 0 a r))"
2899     and t: "tmbound0 t"
2900     and s: "tmbound0 s"
2901   shows "bound0 (msubstlt c t d s a r)"
2902 proof -
2903   have th: "\<forall>x\<in> set
2904   [(let cd = c *\<^sub>p d
2905     in (lt (CP (~\<^sub>p cd)), Lt (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))),
2906    (let cd = c *\<^sub>p d
2907     in (lt (CP cd), Lt (Sub (Mul a (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))),
2908    (conj (lt (CP (~\<^sub>p c))) (Eq (CP d)), Lt (Add (Mul (~\<^sub>p a) t) (Mul ((2)\<^sub>p *\<^sub>p c) r))),
2909    (conj (lt (CP c)) (Eq (CP d)), Lt (Sub (Mul a t) (Mul ((2)\<^sub>p *\<^sub>p c) r))),
2910    (conj (lt (CP (~\<^sub>p d))) (Eq (CP c)), Lt (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
2911    (conj (lt (CP d)) (Eq (CP c)), Lt (Sub (Mul a s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
2912    (conj (Eq (CP c)) (Eq (CP d)), Lt r)]. bound0 (split conj x)"
2913     using lp by (simp add: Let_def t s lt_nb)
2914   from evaldjf_bound0[OF th] show ?thesis
2916 qed
2918 lemma msubstlt:
2919   assumes nc: "isnpoly c"
2920     and nd: "isnpoly d"
2921     and lp: "islin (Lt (CNP 0 a r))"
2922   shows "Ifm vs (x#bs) (msubstlt c t d s a r) \<longleftrightarrow>
2923     Ifm vs (((- Itm vs (x#bs) t /  Ipoly vs c + - Itm vs (x#bs) s / Ipoly vs d) /2)#bs) (Lt (CNP 0 a r))"
2924   (is "?lhs = ?rhs")
2925 proof -
2926   let ?Nt = "\<lambda>x t. Itm vs (x#bs) t"
2927   let ?N = "\<lambda>p. Ipoly vs p"
2928   let ?c = "?N c"
2929   let ?d = "?N d"
2930   let ?t = "?Nt x t"
2931   let ?s = "?Nt x s"
2932   let ?a = "?N a"
2933   let ?r = "?Nt x r"
2934   from lp have lin:"isnpoly a" "a \<noteq> 0\<^sub>p" "tmbound0 r" "allpolys isnpoly r"
2935     by simp_all
2936   note r = tmbound0_I[OF lin(3), of vs _ bs x]
2937   have cd_cs: "?c * ?d < 0 \<or> ?c * ?d > 0 \<or> (?c = 0 \<and> ?d = 0) \<or> (?c = 0 \<and> ?d < 0) \<or> (?c = 0 \<and> ?d > 0) \<or> (?c < 0 \<and> ?d = 0) \<or> (?c > 0 \<and> ?d = 0)"
2938     by auto
2939   moreover
2940   {
2941     assume c: "?c=0" and d: "?d=0"
2942     then have ?thesis
2943       using nc nd by (simp add: polyneg_norm lt r[of 0] msubstlt_def Let_def evaldjf_ex)
2944   }
2945   moreover
2946   {
2947     assume dc: "?c*?d > 0"
2948     from dc have dc': "2*?c *?d > 0"
2949       by simp
2950     then have c:"?c \<noteq> 0" and d: "?d \<noteq> 0"
2951       by auto
2952     from dc' have dc'': "\<not> 2*?c *?d < 0" by simp
2953     from add_frac_eq[OF c d, of "- ?t" "- ?s"]
2954     have th: "(- ?t / ?c + - ?s / ?d)/2 = - (?d * ?t + ?c* ?s )/ (2 * ?c * ?d)"
2956     have "?rhs \<longleftrightarrow> Ifm vs (- (?d * ?t + ?c* ?s )/ (2*?c*?d) # bs) (Lt (CNP 0 a r))"
2957       by (simp only: th)
2958     also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r < 0"
2959       by (simp add: r[of "(- (?d * ?t) - (?c *?s)) / (2 * ?c * ?d)"])
2960     also have "\<dots> \<longleftrightarrow> (2 * ?c * ?d) * (?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r) < 0"
2961       using dc' dc''
2962         mult_less_cancel_left_disj[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r" 0]
2963       by simp
2964     also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2*?c*?d*?r < 0"
2965       using nonzero_mult_divide_cancel_left[of "2*?c*?d"] c d
2966       by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
2967     finally  have ?thesis using dc c d  nc nd dc'
2968       by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"]
2969           msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
2970   }
2971   moreover
2972   {
2973     assume dc: "?c * ?d < 0"
2974     from dc have dc': "2*?c *?d < 0"
2975       by (simp add: mult_less_0_iff field_simps)
2976     then have c:"?c \<noteq> 0" and d: "?d \<noteq> 0"
2977       by auto
2978     from add_frac_eq[OF c d, of "- ?t" "- ?s"]
2979     have th: "(- ?t / ?c + - ?s / ?d)/2 = - (?d * ?t + ?c* ?s )/ (2 * ?c * ?d)"
2981     have "?rhs \<longleftrightarrow> Ifm vs (- (?d * ?t + ?c* ?s )/ (2 * ?c * ?d) # bs) (Lt (CNP 0 a r))"
2982       by (simp only: th)
2983     also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )/ (2 * ?c * ?d)) + ?r < 0"
2984       by (simp add: r[of "(- (?d * ?t) - (?c *?s)) / (2 * ?c * ?d)"])
2985     also have "\<dots> \<longleftrightarrow> (2 * ?c * ?d) * (?a * (- (?d * ?t + ?c * ?s )/ (2 * ?c * ?d)) + ?r) > 0"
2986       using dc' order_less_not_sym[OF dc']
2987         mult_less_cancel_left_disj[of "2 * ?c * ?d" 0 "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r"]
2988       by simp
2989     also have "\<dots> \<longleftrightarrow> ?a * ((?d * ?t + ?c* ?s )) - 2 * ?c * ?d * ?r < 0"
2990       using nonzero_mult_divide_cancel_left[of "2 * ?c * ?d"] c d
2991       by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
2992     finally have ?thesis using dc c d nc nd
2993       by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"]
2994           msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
2995   }
2996   moreover
2997   {
2998     assume c: "?c > 0" and d: "?d = 0"
2999     from c have c'': "2*?c > 0"
3001     from c have c': "2 * ?c \<noteq> 0"
3002       by simp
3003     from d have th: "(- ?t / ?c + - ?s / ?d)/2 = - ?t / (2 * ?c)"
3005     have "?rhs \<longleftrightarrow> Ifm vs (- ?t / (2 * ?c) # bs) (Lt (CNP 0 a r))"
3006       by (simp only: th)
3007     also have "\<dots> \<longleftrightarrow> ?a * (- ?t / (2 * ?c))+ ?r < 0"
3008       by (simp add: r[of "- (?t / (2 * ?c))"])
3009     also have "\<dots> \<longleftrightarrow> 2 * ?c * (?a * (- ?t / (2 * ?c))+ ?r) < 0"
3010       using c mult_less_cancel_left_disj[of "2 * ?c" "?a* (- ?t / (2*?c))+ ?r" 0] c' c''
3011         order_less_not_sym[OF c'']
3012       by simp
3013     also have "\<dots> \<longleftrightarrow> - ?a * ?t + 2 * ?c * ?r < 0"
3014       using nonzero_mult_divide_cancel_left[OF c'] c
3015       by (simp add: algebra_simps diff_divide_distrib less_le del: distrib_right)
3016     finally have ?thesis using c d nc nd
3017       by (simp add: r[of "- (?t / (2*?c))"] msubstlt_def Let_def evaldjf_ex field_simps
3018           lt polyneg_norm polymul_norm)
3019   }
3020   moreover
3021   {
3022     assume c: "?c < 0" and d: "?d = 0"
3023     then have c': "2 * ?c \<noteq> 0"
3024       by simp
3025     from c have c'': "2 * ?c < 0"
3027     from d have th: "(- ?t / ?c + - ?s / ?d)/2 = - ?t / (2 * ?c)"
3029     have "?rhs \<longleftrightarrow> Ifm vs (- ?t / (2*?c) # bs) (Lt (CNP 0 a r))"
3030       by (simp only: th)
3031     also have "\<dots> \<longleftrightarrow> ?a * (- ?t / (2*?c))+ ?r < 0"
3032       by (simp add: r[of "- (?t / (2*?c))"])
3033     also have "\<dots> \<longleftrightarrow> 2 * ?c * (?a * (- ?t / (2 * ?c))+ ?r) > 0"
3034       using c order_less_not_sym[OF c''] less_imp_neq[OF c''] c''
3035         mult_less_cancel_left_disj[of "2 * ?c" 0 "?a* (- ?t / (2*?c))+ ?r"]
3036       by simp
3037     also have "\<dots> \<longleftrightarrow> ?a*?t -  2*?c *?r < 0"
3038       using nonzero_mult_divide_cancel_left[OF c'] c order_less_not_sym[OF c'']
3039           less_imp_neq[OF c''] c''
3040         by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
3041     finally have ?thesis using c d nc nd
3042       by (simp add: r[of "- (?t / (2*?c))"] msubstlt_def Let_def evaldjf_ex field_simps
3043           lt polyneg_norm polymul_norm)
3044   }
3045   moreover
3046   {
3047     assume c: "?c = 0" and d: "?d > 0"
3048     from d have d'': "2 * ?d > 0"
3050     from d have d': "2 * ?d \<noteq> 0"
3051       by simp
3052     from c have th: "(- ?t / ?c + - ?s / ?d)/2 = - ?s / (2 * ?d)"
3054     have "?rhs \<longleftrightarrow> Ifm vs (- ?s / (2 * ?d) # bs) (Lt (CNP 0 a r))"
3055       by (simp only: th)
3056     also have "\<dots> \<longleftrightarrow> ?a * (- ?s / (2 * ?d))+ ?r < 0"
3057       by (simp add: r[of "- (?s / (2 * ?d))"])
3058     also have "\<dots> \<longleftrightarrow> 2 * ?d * (?a * (- ?s / (2 * ?d))+ ?r) < 0"
3059       using d mult_less_cancel_left_disj[of "2 * ?d" "?a * (- ?s / (2 * ?d))+ ?r" 0] d' d''
3060         order_less_not_sym[OF d'']
3061       by simp
3062     also have "\<dots> \<longleftrightarrow> - ?a * ?s+  2 * ?d * ?r < 0"
3063       using nonzero_mult_divide_cancel_left[OF d'] d
3064       by (simp add: algebra_simps diff_divide_distrib less_le del: distrib_right)
3065     finally have ?thesis using c d nc nd
3066       by (simp add: r[of "- (?s / (2*?d))"] msubstlt_def Let_def evaldjf_ex field_simps
3067           lt polyneg_norm polymul_norm)
3068   }
3069   moreover
3070   {
3071     assume c: "?c = 0" and d: "?d < 0"
3072     then have d': "2 * ?d \<noteq> 0"
3073       by simp
3074     from d have d'': "2 * ?d < 0"
3076     from c have th: "(- ?t / ?c + - ?s / ?d)/2 = - ?s / (2*?d)"
3078     have "?rhs \<longleftrightarrow> Ifm vs (- ?s / (2 * ?d) # bs) (Lt (CNP 0 a r))"
3079       by (simp only: th)
3080     also have "\<dots> \<longleftrightarrow> ?a * (- ?s / (2 * ?d)) + ?r < 0"
3081       by (simp add: r[of "- (?s / (2 * ?d))"])
3082     also have "\<dots> \<longleftrightarrow> 2 * ?d * (?a * (- ?s / (2 * ?d)) + ?r) > 0"
3083       using d order_less_not_sym[OF d''] less_imp_neq[OF d''] d''
3084         mult_less_cancel_left_disj[of "2 * ?d" 0 "?a* (- ?s / (2*?d))+ ?r"]
3085       by simp
3086     also have "\<dots> \<longleftrightarrow> ?a * ?s -  2 * ?d * ?r < 0"
3087       using nonzero_mult_divide_cancel_left[OF d'] d order_less_not_sym[OF d'']
3088           less_imp_neq[OF d''] d''
3089         by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
3090     finally have ?thesis using c d nc nd
3091       by (simp add: r[of "- (?s / (2*?d))"] msubstlt_def Let_def evaldjf_ex field_simps
3092           lt polyneg_norm polymul_norm)
3093   }
3094   ultimately show ?thesis by blast
3095 qed
3097 definition "msubstle c t d s a r =
3098   evaldjf (split conj)
3099    [(let cd = c *\<^sub>p d
3100      in (lt (CP (~\<^sub>p cd)), Le (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))),
3101     (let cd = c *\<^sub>p d
3102      in (lt (CP cd), Le (Sub (Mul a (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))),
3103     (conj (lt (CP (~\<^sub>p c))) (Eq (CP d)), Le (Add (Mul (~\<^sub>p a) t) (Mul ((2)\<^sub>p *\<^sub>p c) r))),
3104     (conj (lt (CP c)) (Eq (CP d)), Le (Sub (Mul a t) (Mul ((2)\<^sub>p *\<^sub>p c) r))),
3105     (conj (lt (CP (~\<^sub>p d))) (Eq (CP c)), Le (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
3106     (conj (lt (CP d)) (Eq (CP c)), Le (Sub (Mul a s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
3107     (conj (Eq (CP c)) (Eq (CP d)), Le r)]"
3109 lemma msubstle_nb:
3110   assumes lp: "islin (Le (CNP 0 a r))"
3111     and t: "tmbound0 t"
3112     and s: "tmbound0 s"
3113   shows "bound0 (msubstle c t d s a r)"
3114 proof -
3115   have th: "\<forall>x\<in> set
3116    [(let cd = c *\<^sub>p d
3117      in (lt (CP (~\<^sub>p cd)), Le (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))),
3118     (let cd = c *\<^sub>p d
3119      in (lt (CP cd), Le (Sub (Mul a (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))),
3120     (conj (lt (CP (~\<^sub>p c))) (Eq (CP d)) , Le (Add (Mul (~\<^sub>p a) t) (Mul ((2)\<^sub>p *\<^sub>p c) r))),
3121     (conj (lt (CP c)) (Eq (CP d)) , Le (Sub (Mul a t) (Mul ((2)\<^sub>p *\<^sub>p c) r))),
3122     (conj (lt (CP (~\<^sub>p d))) (Eq (CP c)) , Le (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
3123     (conj (lt (CP d)) (Eq (CP c)) , Le (Sub (Mul a s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
3124     (conj (Eq (CP c)) (Eq (CP d)) , Le r)]. bound0 (split conj x)"
3125     using lp by (simp add: Let_def t s lt_nb)
3126   from evaldjf_bound0[OF th] show ?thesis
3128 qed
3130 lemma msubstle:
3131   assumes nc: "isnpoly c"
3132     and nd: "isnpoly d"
3133     and lp: "islin (Le (CNP 0 a r))"
3134   shows "Ifm vs (x#bs) (msubstle c t d s a r) \<longleftrightarrow>
3135     Ifm vs (((- Itm vs (x#bs) t /  Ipoly vs c + - Itm vs (x#bs) s / Ipoly vs d) /2)#bs) (Le (CNP 0 a r))"
3136   (is "?lhs = ?rhs")
3137 proof -
3138   let ?Nt = "\<lambda>x t. Itm vs (x#bs) t"
3139   let ?N = "\<lambda>p. Ipoly vs p"
3140   let ?c = "?N c"
3141   let ?d = "?N d"
3142   let ?t = "?Nt x t"
3143   let ?s = "?Nt x s"
3144   let ?a = "?N a"
3145   let ?r = "?Nt x r"
3146   from lp have lin:"isnpoly a" "a \<noteq> 0\<^sub>p" "tmbound0 r" "allpolys isnpoly r"
3147     by simp_all
3148   note r = tmbound0_I[OF lin(3), of vs _ bs x]
3149   have cd_cs: "?c * ?d < 0 \<or> ?c * ?d > 0 \<or> (?c = 0 \<and> ?d = 0) \<or> (?c = 0 \<and> ?d < 0) \<or> (?c = 0 \<and> ?d > 0) \<or> (?c < 0 \<and> ?d = 0) \<or> (?c > 0 \<and> ?d = 0)"
3150     by auto
3151   moreover
3152   {
3153     assume c: "?c = 0" and d: "?d = 0"
3154     then have ?thesis
3155       using nc nd
3156       by (simp add: polyneg_norm polymul_norm lt r[of 0] msubstle_def Let_def evaldjf_ex)
3157   }
3158   moreover
3159   {
3160     assume dc: "?c * ?d > 0"
3161     from dc have dc': "2 * ?c * ?d > 0"
3162       by simp
3163     then have c: "?c \<noteq> 0" and d: "?d \<noteq> 0"
3164       by auto
3165     from dc' have dc'': "\<not> 2 * ?c * ?d < 0"
3166       by simp
3167     from add_frac_eq[OF c d, of "- ?t" "- ?s"]
3168     have th: "(- ?t / ?c + - ?s / ?d)/2 = - (?d * ?t + ?c * ?s )/ (2 * ?c * ?d)"
3170     have "?rhs \<longleftrightarrow> Ifm vs (- (?d * ?t + ?c* ?s )/ (2*?c*?d) # bs) (Le (CNP 0 a r))"
3171       by (simp only: th)
3172     also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r \<le> 0"
3173       by (simp add: r[of "(- (?d * ?t) - (?c *?s)) / (2 * ?c * ?d)"])
3174     also have "\<dots> \<longleftrightarrow> (2 * ?c * ?d) * (?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r) \<le> 0"
3175       using dc' dc''
3176         mult_le_cancel_left[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r" 0]
3177       by simp
3178     also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2*?c*?d*?r \<le> 0"
3179       using nonzero_mult_divide_cancel_left[of "2*?c*?d"] c d
3180       by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
3181     finally  have ?thesis using dc c d  nc nd dc'
3182       by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"] msubstle_def
3183           Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
3184   }
3185   moreover
3186   {
3187     assume dc: "?c * ?d < 0"
3188     from dc have dc': "2 * ?c * ?d < 0"
3190     then have c: "?c \<noteq> 0" and d: "?d \<noteq> 0"
3191       by auto
3192     from add_frac_eq[OF c d, of "- ?t" "- ?s"]
3193     have th: "(- ?t / ?c + - ?s / ?d)/2 = - (?d * ?t + ?c* ?s )/ (2 * ?c * ?d)"
3195     have "?rhs \<longleftrightarrow> Ifm vs (- (?d * ?t + ?c* ?s )/ (2*?c*?d) # bs) (Le (CNP 0 a r))"
3196       by (simp only: th)
3197     also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r \<le> 0"
3198       by (simp add: r[of "(- (?d * ?t) - (?c *?s)) / (2 * ?c * ?d)"])
3199     also have "\<dots> \<longleftrightarrow> (2 * ?c * ?d) * (?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r) \<ge> 0"
3200       using dc' order_less_not_sym[OF dc']
3201         mult_le_cancel_left[of "2 * ?c * ?d" 0 "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r"]
3202       by simp
3203     also have "\<dots> \<longleftrightarrow> ?a * ((?d * ?t + ?c* ?s )) - 2 * ?c * ?d * ?r \<le> 0"
3204       using nonzero_mult_divide_cancel_left[of "2 * ?c * ?d"] c d
3205       by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
3206     finally  have ?thesis using dc c d  nc nd
3207       by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"] msubstle_def
3208           Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
3209   }
3210   moreover
3211   {
3212     assume c: "?c > 0" and d: "?d = 0"
3213     from c have c'': "2 * ?c > 0"
3215     from c have c': "2 * ?c \<noteq> 0"
3216       by simp
3217     from d have th: "(- ?t / ?c + - ?s / ?d)/2 = - ?t / (2*?c)"
3219     have "?rhs \<longleftrightarrow> Ifm vs (- ?t / (2 * ?c) # bs) (Le (CNP 0 a r))"
3220       by (simp only: th)
3221     also have "\<dots> \<longleftrightarrow> ?a * (- ?t / (2 * ?c))+ ?r \<le> 0"
3222       by (simp add: r[of "- (?t / (2 * ?c))"])
3223     also have "\<dots> \<longleftrightarrow> 2 * ?c * (?a * (- ?t / (2 * ?c))+ ?r) \<le> 0"
3224       using c mult_le_cancel_left[of "2 * ?c" "?a* (- ?t / (2*?c))+ ?r" 0] c' c''
3225         order_less_not_sym[OF c'']
3226       by simp
3227     also have "\<dots> \<longleftrightarrow> - ?a*?t+  2*?c *?r \<le> 0"
3228       using nonzero_mult_divide_cancel_left[OF c'] c
3229       by (simp add: algebra_simps diff_divide_distrib less_le del: distrib_right)
3230     finally have ?thesis using c d nc nd
3231       by (simp add: r[of "- (?t / (2*?c))"] msubstle_def Let_def
3232           evaldjf_ex field_simps lt polyneg_norm polymul_norm)
3233   }
3234   moreover
3235   {
3236     assume c: "?c < 0" and d: "?d = 0"
3237     then have c': "2 * ?c \<noteq> 0"
3238       by simp
3239     from c have c'': "2 * ?c < 0"
3241     from d have th: "(- ?t / ?c + - ?s / ?d)/2 = - ?t / (2*?c)"
3243     have "?rhs \<longleftrightarrow> Ifm vs (- ?t / (2 * ?c) # bs) (Le (CNP 0 a r))"
3244       by (simp only: th)
3245     also have "\<dots> \<longleftrightarrow> ?a * (- ?t / (2*?c))+ ?r \<le> 0"
3246       by (simp add: r[of "- (?t / (2*?c))"])
3247     also have "\<dots> \<longleftrightarrow> 2 * ?c * (?a * (- ?t / (2 * ?c))+ ?r) \<ge> 0"
3248       using c order_less_not_sym[OF c''] less_imp_neq[OF c''] c''
3249         mult_le_cancel_left[of "2 * ?c" 0 "?a* (- ?t / (2*?c))+ ?r"]
3250       by simp
3251     also have "\<dots> \<longleftrightarrow> ?a * ?t - 2 * ?c * ?r \<le> 0"
3252       using nonzero_mult_divide_cancel_left[OF c'] c order_less_not_sym[OF c'']
3253           less_imp_neq[OF c''] c''
3254         by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
3255     finally have ?thesis using c d nc nd
3256       by (simp add: r[of "- (?t / (2*?c))"] msubstle_def Let_def
3257           evaldjf_ex field_simps lt polyneg_norm polymul_norm)
3258   }
3259   moreover
3260   {
3261     assume c: "?c = 0" and d: "?d > 0"
3262     from d have d'': "2 * ?d > 0"
3264     from d have d': "2 * ?d \<noteq> 0"
3265       by simp
3266     from c have th: "(- ?t / ?c + - ?s / ?d)/2 = - ?s / (2 * ?d)"
3268     have "?rhs \<longleftrightarrow> Ifm vs (- ?s / (2 * ?d) # bs) (Le (CNP 0 a r))"
3269       by (simp only: th)
3270     also have "\<dots> \<longleftrightarrow> ?a * (- ?s / (2 * ?d))+ ?r \<le> 0"
3271       by (simp add: r[of "- (?s / (2*?d))"])
3272     also have "\<dots> \<longleftrightarrow> 2 * ?d * (?a * (- ?s / (2 * ?d)) + ?r) \<le> 0"
3273       using d mult_le_cancel_left[of "2 * ?d" "?a* (- ?s / (2*?d))+ ?r" 0] d' d''
3274         order_less_not_sym[OF d'']
3275       by simp
3276     also have "\<dots> \<longleftrightarrow> - ?a * ?s + 2 * ?d * ?r \<le> 0"
3277       using nonzero_mult_divide_cancel_left[OF d'] d
3278       by (simp add: algebra_simps diff_divide_distrib less_le del: distrib_right)
3279     finally have ?thesis using c d nc nd
3280       by (simp add: r[of "- (?s / (2*?d))"] msubstle_def Let_def
3281           evaldjf_ex field_simps lt polyneg_norm polymul_norm)
3282   }
3283   moreover
3284   {
3285     assume c: "?c = 0" and d: "?d < 0"
3286     then have d': "2 * ?d \<noteq> 0"
3287       by simp
3288     from d have d'': "2 * ?d < 0"
3290     from c have th: "(- ?t / ?c + - ?s / ?d)/2 = - ?s / (2*?d)"
3292     have "?rhs \<longleftrightarrow> Ifm vs (- ?s / (2*?d) # bs) (Le (CNP 0 a r))"
3293       by (simp only: th)
3294     also have "\<dots> \<longleftrightarrow> ?a* (- ?s / (2*?d))+ ?r \<le> 0"
3295       by (simp add: r[of "- (?s / (2*?d))"])
3296     also have "\<dots> \<longleftrightarrow> 2*?d * (?a* (- ?s / (2*?d))+ ?r) \<ge> 0"
3297       using d order_less_not_sym[OF d''] less_imp_neq[OF d''] d''
3298         mult_le_cancel_left[of "2 * ?d" 0 "?a* (- ?s / (2*?d))+ ?r"]
3299       by simp
3300     also have "\<dots> \<longleftrightarrow> ?a * ?s -  2 * ?d * ?r \<le> 0"
3301       using nonzero_mult_divide_cancel_left[OF d'] d order_less_not_sym[OF d'']
3302           less_imp_neq[OF d''] d''
3303         by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
3304     finally have ?thesis using c d nc nd
3305       by (simp add: r[of "- (?s / (2*?d))"] msubstle_def Let_def
3306           evaldjf_ex field_simps lt polyneg_norm polymul_norm)
3307   }
3308   ultimately show ?thesis by blast
3309 qed
3311 fun msubst :: "fm \<Rightarrow> (poly \<times> tm) \<times> (poly \<times> tm) \<Rightarrow> fm"
3312 where
3313   "msubst (And p q) ((c, t), (d, s)) = conj (msubst p ((c,t),(d,s))) (msubst q ((c, t), (d, s)))"
3314 | "msubst (Or p q) ((c, t), (d, s)) = disj (msubst p ((c,t),(d,s))) (msubst q ((c, t), (d, s)))"
3315 | "msubst (Eq (CNP 0 a r)) ((c, t), (d, s)) = msubsteq c t d s a r"
3316 | "msubst (NEq (CNP 0 a r)) ((c, t), (d, s)) = msubstneq c t d s a r"
3317 | "msubst (Lt (CNP 0 a r)) ((c, t), (d, s)) = msubstlt c t d s a r"
3318 | "msubst (Le (CNP 0 a r)) ((c, t), (d, s)) = msubstle c t d s a r"
3319 | "msubst p ((c, t), (d, s)) = p"
3321 lemma msubst_I:
3322   assumes lp: "islin p"
3323     and nc: "isnpoly c"
3324     and nd: "isnpoly d"
3325   shows "Ifm vs (x#bs) (msubst p ((c,t),(d,s))) =
3326     Ifm vs (((- Itm vs (x#bs) t /  Ipoly vs c + - Itm vs (x#bs) s / Ipoly vs d) /2)#bs) p"
3327   using lp
3328   by (induct p rule: islin.induct)
3330       [where b = "(- (Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup>) - (Itm vs (x # bs) s / \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>)) / 2"
3331         and b' = x and bs = bs and vs = vs]
3332       msubsteq msubstneq msubstlt [OF nc nd] msubstle [OF nc nd])
3334 lemma msubst_nb:
3335   assumes lp: "islin p"
3336     and t: "tmbound0 t"
3337     and s: "tmbound0 s"
3338   shows "bound0 (msubst p ((c,t),(d,s)))"
3339   using lp t s
3340   by (induct p rule: islin.induct, auto simp add: msubsteq_nb msubstneq_nb msubstlt_nb msubstle_nb)
3342 lemma fr_eq_msubst:
3343   assumes lp: "islin p"
3344   shows "(\<exists>x. Ifm vs (x#bs) p) \<longleftrightarrow>
3345     (Ifm vs (x#bs) (minusinf p) \<or>
3346      Ifm vs (x#bs) (plusinf p) \<or>
3347      (\<exists>(c, t) \<in> set (uset p). \<exists>(d, s) \<in> set (uset p).
3348       Ifm vs (x#bs) (msubst p ((c, t), (d, s)))))"
3349   (is "(\<exists>x. ?I x p) = (?M \<or> ?P \<or> ?F)" is "?E = ?D")
3350 proof -
3351   from uset_l[OF lp]
3352   have th: "\<forall>(c, s)\<in>set (uset p). isnpoly c \<and> tmbound0 s"
3353     by blast
3354   {
3355     fix c t d s
3356     assume ctU: "(c, t) \<in>set (uset p)"
3357       and dsU: "(d,s) \<in>set (uset p)"
3358       and pts: "Ifm vs ((- Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup> + - Itm vs (x # bs) s / \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>) / 2 # bs) p"
3359     from th[rule_format, OF ctU] th[rule_format, OF dsU] have norm:"isnpoly c" "isnpoly d"
3360       by simp_all
3361     from msubst_I[OF lp norm, of vs x bs t s] pts
3362     have "Ifm vs (x # bs) (msubst p ((c, t), d, s))" ..
3363   }
3364   moreover
3365   {
3366     fix c t d s
3367     assume ctU: "(c, t) \<in> set (uset p)"
3368       and dsU: "(d,s) \<in>set (uset p)"
3369       and pts: "Ifm vs (x # bs) (msubst p ((c, t), d, s))"
3370     from th[rule_format, OF ctU] th[rule_format, OF dsU] have norm:"isnpoly c" "isnpoly d"
3371       by simp_all
3372     from msubst_I[OF lp norm, of vs x bs t s] pts
3373     have "Ifm vs ((- Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup> + - Itm vs (x # bs) s / \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>) / 2 # bs) p" ..
3374   }
3375   ultimately have th': "(\<exists>(c, t) \<in> set (uset p). \<exists>(d, s) \<in> set (uset p).
3376       Ifm vs ((- Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup> + - Itm vs (x # bs) s / \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>) / 2 # bs) p) \<longleftrightarrow> ?F"
3377     by blast
3378   from fr_eq[OF lp, of vs bs x, simplified th'] show ?thesis .
3379 qed
3381 lemma simpfm_lin:
3382   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
3383   shows "qfree p \<Longrightarrow> islin (simpfm p)"
3384   by (induct p rule: simpfm.induct) (auto simp add: conj_lin disj_lin)
3386 definition "ferrack p \<equiv>
3387   let
3388     q = simpfm p;
3389     mp = minusinf q;
3390     pp = plusinf q
3391   in
3392     if (mp = T \<or> pp = T) then T
3393     else
3394      (let U = alluopairs (remdups (uset  q))
3395       in decr0 (disj mp (disj pp (evaldjf (simpfm o (msubst q)) U ))))"
3397 lemma ferrack:
3398   assumes qf: "qfree p"
3399   shows "qfree (ferrack p) \<and> Ifm vs bs (ferrack p) = Ifm vs bs (E p)"
3400   (is "_ \<and> ?rhs = ?lhs")
3401 proof -
3402   let ?I = "\<lambda>x p. Ifm vs (x#bs) p"
3403   let ?N = "\<lambda>t. Ipoly vs t"
3404   let ?Nt = "\<lambda>x t. Itm vs (x#bs) t"
3405   let ?q = "simpfm p"
3406   let ?U = "remdups(uset ?q)"
3407   let ?Up = "alluopairs ?U"
3408   let ?mp = "minusinf ?q"
3409   let ?pp = "plusinf ?q"
3410   fix x
3411   let ?I = "\<lambda>p. Ifm vs (x#bs) p"
3412   from simpfm_lin[OF qf] simpfm_qf[OF qf] have lq: "islin ?q" and q_qf: "qfree ?q" .
3413   from minusinf_nb[OF lq] plusinf_nb[OF lq] have mp_nb: "bound0 ?mp" and pp_nb: "bound0 ?pp" .
3414   from bound0_qf[OF mp_nb] bound0_qf[OF pp_nb] have mp_qf: "qfree ?mp" and pp_qf: "qfree ?pp" .
3415   from uset_l[OF lq] have U_l: "\<forall>(c, s)\<in>set ?U. isnpoly c \<and> c \<noteq> 0\<^sub>p \<and> tmbound0 s \<and> allpolys isnpoly s"
3416     by simp
3417   {
3418     fix c t d s
3419     assume ctU: "(c, t) \<in> set ?U"
3420       and dsU: "(d,s) \<in> set ?U"
3421     from U_l ctU dsU have norm: "isnpoly c" "isnpoly d"
3422       by auto
3423     from msubst_I[OF lq norm, of vs x bs t s] msubst_I[OF lq norm(2,1), of vs x bs s t]
3424     have "?I (msubst ?q ((c,t),(d,s))) = ?I (msubst ?q ((d,s),(c,t)))"
3426   }
3427   then have th0: "\<forall>x \<in> set ?U. \<forall>y \<in> set ?U. ?I (msubst ?q (x, y)) \<longleftrightarrow> ?I (msubst ?q (y, x))"
3428     by auto
3429   {
3430     fix x
3431     assume xUp: "x \<in> set ?Up"
3432     then obtain c t d s
3433       where ctU: "(c, t) \<in> set ?U"
3434         and dsU: "(d,s) \<in> set ?U"
3435         and x: "x = ((c, t),(d, s))"
3436       using alluopairs_set1[of ?U] by auto
3437     from U_l[rule_format, OF ctU] U_l[rule_format, OF dsU]
3438     have nbs: "tmbound0 t" "tmbound0 s" by simp_all
3439     from simpfm_bound0[OF msubst_nb[OF lq nbs, of c d]]
3440     have "bound0 ((simpfm o (msubst (simpfm p))) x)"
3441       using x by simp
3442   }
3443   with evaldjf_bound0[of ?Up "(simpfm o (msubst (simpfm p)))"]
3444   have "bound0 (evaldjf (simpfm o (msubst (simpfm p))) ?Up)" by blast
3445   with mp_nb pp_nb
3446   have th1: "bound0 (disj ?mp (disj ?pp (evaldjf (simpfm o (msubst ?q)) ?Up )))"
3447     by simp
3448   from decr0_qf[OF th1] have thqf: "qfree (ferrack p)"
3449     by (simp add: ferrack_def Let_def)
3450   have "?lhs \<longleftrightarrow> (\<exists>x. Ifm vs (x#bs) ?q)"
3451     by simp
3452   also have "\<dots> \<longleftrightarrow> ?I ?mp \<or> ?I ?pp \<or>
3453       (\<exists>(c, t)\<in>set ?U. \<exists>(d, s)\<in>set ?U. ?I (msubst (simpfm p) ((c, t), d, s)))"
3454     using fr_eq_msubst[OF lq, of vs bs x] by simp
3455   also have "\<dots> \<longleftrightarrow> ?I ?mp \<or> ?I ?pp \<or>
3456       (\<exists>(x, y) \<in> set ?Up. ?I ((simpfm \<circ> msubst ?q) (x, y)))"
3457     using alluopairs_bex[OF th0] by simp
3458   also have "\<dots> \<longleftrightarrow> ?I ?mp \<or> ?I ?pp \<or> ?I (evaldjf (simpfm \<circ> msubst ?q) ?Up)"
3460   also have "\<dots> \<longleftrightarrow> ?I (disj ?mp (disj ?pp (evaldjf (simpfm \<circ> msubst ?q) ?Up)))"
3461     by simp
3462   also have "\<dots> \<longleftrightarrow> ?rhs"
3463     using decr0[OF th1, of vs x bs]
3464     apply (simp add: ferrack_def Let_def)
3465     apply (cases "?mp = T \<or> ?pp = T")
3466     apply auto
3467     done
3468   finally show ?thesis
3469     using thqf by blast
3470 qed
3472 definition "frpar p = simpfm (qelim p ferrack)"
3474 lemma frpar: "qfree (frpar p) \<and> (Ifm vs bs (frpar p) \<longleftrightarrow> Ifm vs bs p)"
3475 proof -
3476   from ferrack
3477   have th: "\<forall>bs p. qfree p \<longrightarrow> qfree (ferrack p) \<and> Ifm vs bs (ferrack p) = Ifm vs bs (E p)"
3478     by blast
3479   from qelim[OF th, of p bs] show ?thesis
3480     unfolding frpar_def by auto
3481 qed
3484 section {* Second implemenation: Case splits not local *}
3486 lemma fr_eq2:
3487   assumes lp: "islin p"
3488   shows "(\<exists>x. Ifm vs (x#bs) p) \<longleftrightarrow>
3489    (Ifm vs (x#bs) (minusinf p) \<or>
3490     Ifm vs (x#bs) (plusinf p) \<or>
3491     Ifm vs (0#bs) p \<or>
3492     (\<exists>(n, t) \<in> set (uset p).
3493       Ipoly vs n \<noteq> 0 \<and> Ifm vs ((- Itm vs (x#bs) t /  (Ipoly vs n * 2))#bs) p) \<or>
3494       (\<exists>(n, t) \<in> set (uset p). \<exists>(m, s) \<in> set (uset p).
3495         Ipoly vs n \<noteq> 0 \<and>
3496         Ipoly vs m \<noteq> 0 \<and>
3497         Ifm vs (((- Itm vs (x#bs) t /  Ipoly vs n + - Itm vs (x#bs) s / Ipoly vs m) /2)#bs) p))"
3498   (is "(\<exists>x. ?I x p) = (?M \<or> ?P \<or> ?Z \<or> ?U \<or> ?F)" is "?E = ?D")
3499 proof
3500   assume px: "\<exists>x. ?I x p"
3501   have "?M \<or> ?P \<or> (\<not> ?M \<and> \<not> ?P)" by blast
3502   moreover {
3503     assume "?M \<or> ?P"
3504     then have "?D" by blast
3505   }
3506   moreover {
3507     assume nmi: "\<not> ?M"
3508       and npi: "\<not> ?P"
3509     from inf_uset[OF lp nmi npi, OF px]
3510     obtain c t d s where ct:
3511       "(c, t) \<in> set (uset p)"
3512       "(d, s) \<in> set (uset p)"
3513       "?I ((- Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup> + - Itm vs (x # bs) s / \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>) / (1 + 1)) p"
3514       by auto
3515     let ?c = "\<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup>"
3516     let ?d = "\<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>"
3517     let ?s = "Itm vs (x # bs) s"
3518     let ?t = "Itm vs (x # bs) t"
3519     have eq2: "\<And>(x::'a). x + x = 2 * x"
3521     {
3522       assume "?c = 0 \<and> ?d = 0"
3523       with ct have ?D by simp
3524     }
3525     moreover
3526     {
3527       assume z: "?c = 0" "?d \<noteq> 0"
3528       from z have ?D using ct by auto
3529     }
3530     moreover
3531     {
3532       assume z: "?c \<noteq> 0" "?d = 0"
3533       with ct have ?D by auto
3534     }
3535     moreover
3536     {
3537       assume z: "?c \<noteq> 0" "?d \<noteq> 0"
3538       from z have ?F using ct
3539         apply -
3540         apply (rule bexI[where x = "(c,t)"])
3541         apply simp_all
3542         apply (rule bexI[where x = "(d,s)"])
3543         apply simp_all
3544         done
3545       then have ?D by blast
3546     }
3547     ultimately have ?D by auto
3548   }
3549   ultimately show "?D" by blast
3550 next
3551   assume "?D"
3552   moreover {
3553     assume m: "?M"
3554     from minusinf_ex[OF lp m] have "?E" .
3555   }
3556   moreover {
3557     assume p: "?P"
3558     from plusinf_ex[OF lp p] have "?E" .
3559   }
3560   moreover {
3561     assume f:"?F"
3562     then have "?E" by blast
3563   }
3564   ultimately show "?E" by blast
3565 qed
3567 definition "msubsteq2 c t a b = Eq (Add (Mul a t) (Mul c b))"
3568 definition "msubstltpos c t a b = Lt (Add (Mul a t) (Mul c b))"
3569 definition "msubstlepos c t a b = Le (Add (Mul a t) (Mul c b))"
3570 definition "msubstltneg c t a b = Lt (Neg (Add (Mul a t) (Mul c b)))"
3571 definition "msubstleneg c t a b = Le (Neg (Add (Mul a t) (Mul c b)))"
3573 lemma msubsteq2:
3574   assumes nz: "Ipoly vs c \<noteq> 0"
3575     and l: "islin (Eq (CNP 0 a b))"
3576   shows "Ifm vs (x#bs) (msubsteq2 c t a b) =
3577     Ifm vs (((Itm vs (x#bs) t /  Ipoly vs c ))#bs) (Eq (CNP 0 a b))"
3578   using nz l tmbound0_I[of b vs x bs "Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup>", symmetric]
3579   by (simp add: msubsteq2_def field_simps)
3581 lemma msubstltpos:
3582   assumes nz: "Ipoly vs c > 0"
3583     and l: "islin (Lt (CNP 0 a b))"
3584   shows "Ifm vs (x#bs) (msubstltpos c t a b) =
3585     Ifm vs (((Itm vs (x#bs) t / Ipoly vs c ))#bs) (Lt (CNP 0 a b))"
3586   using nz l tmbound0_I[of b vs x bs "Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup>", symmetric]
3587   by (simp add: msubstltpos_def field_simps)
3589 lemma msubstlepos:
3590   assumes nz: "Ipoly vs c > 0"
3591     and l: "islin (Le (CNP 0 a b))"
3592   shows "Ifm vs (x#bs) (msubstlepos c t a b) =
3593     Ifm vs (((Itm vs (x#bs) t /  Ipoly vs c ))#bs) (Le (CNP 0 a b))"
3594   using nz l tmbound0_I[of b vs x bs "Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup>", symmetric]
3595   by (simp add: msubstlepos_def field_simps)
3597 lemma msubstltneg:
3598   assumes nz: "Ipoly vs c < 0"
3599     and l: "islin (Lt (CNP 0 a b))"
3600   shows "Ifm vs (x#bs) (msubstltneg c t a b) =
3601     Ifm vs (((Itm vs (x#bs) t /  Ipoly vs c ))#bs) (Lt (CNP 0 a b))"
3602   using nz l tmbound0_I[of b vs x bs "Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup>", symmetric]
3605 lemma msubstleneg:
3606   assumes nz: "Ipoly vs c < 0"
3607     and l: "islin (Le (CNP 0 a b))"
3608   shows "Ifm vs (x#bs) (msubstleneg c t a b) =
3609     Ifm vs (((Itm vs (x#bs) t /  Ipoly vs c ))#bs) (Le (CNP 0 a b))"
3610   using nz l tmbound0_I[of b vs x bs "Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup>", symmetric]
3613 fun msubstpos :: "fm \<Rightarrow> poly \<Rightarrow> tm \<Rightarrow> fm"
3614 where
3615   "msubstpos (And p q) c t = And (msubstpos p c t) (msubstpos q c t)"
3616 | "msubstpos (Or p q) c t = Or (msubstpos p c t) (msubstpos q c t)"
3617 | "msubstpos (Eq (CNP 0 a r)) c t = msubsteq2 c t a r"
3618 | "msubstpos (NEq (CNP 0 a r)) c t = NOT (msubsteq2 c t a r)"
3619 | "msubstpos (Lt (CNP 0 a r)) c t = msubstltpos c t a r"
3620 | "msubstpos (Le (CNP 0 a r)) c t = msubstlepos c t a r"
3621 | "msubstpos p c t = p"
3623 lemma msubstpos_I:
3624   assumes lp: "islin p"
3625     and pos: "Ipoly vs c > 0"
3626   shows "Ifm vs (x#bs) (msubstpos p c t) =
3627     Ifm vs (Itm vs (x#bs) t /  Ipoly vs c #bs) p"
3628   using lp pos
3629   by (induct p rule: islin.induct)
3630     (auto simp add: msubsteq2 msubstltpos[OF pos] msubstlepos[OF pos]
3631       tmbound0_I[of _ vs "Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup>" bs x]
3632       bound0_I[of _ vs "Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup>" bs x] field_simps)
3634 fun msubstneg :: "fm \<Rightarrow> poly \<Rightarrow> tm \<Rightarrow> fm"
3635 where
3636   "msubstneg (And p q) c t = And (msubstneg p c t) (msubstneg q c t)"
3637 | "msubstneg (Or p q) c t = Or (msubstneg p c t) (msubstneg q c t)"
3638 | "msubstneg (Eq (CNP 0 a r)) c t = msubsteq2 c t a r"
3639 | "msubstneg (NEq (CNP 0 a r)) c t = NOT (msubsteq2 c t a r)"
3640 | "msubstneg (Lt (CNP 0 a r)) c t = msubstltneg c t a r"
3641 | "msubstneg (Le (CNP 0 a r)) c t = msubstleneg c t a r"
3642 | "msubstneg p c t = p"
3644 lemma msubstneg_I:
3645   assumes lp: "islin p"
3646     and pos: "Ipoly vs c < 0"
3647   shows "Ifm vs (x#bs) (msubstneg p c t) = Ifm vs (Itm vs (x#bs) t /  Ipoly vs c #bs) p"
3648   using lp pos
3649   by (induct p rule: islin.induct)
3650     (auto simp add: msubsteq2 msubstltneg[OF pos] msubstleneg[OF pos]
3651       tmbound0_I[of _ vs "Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup>" bs x]
3652       bound0_I[of _ vs "Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup>" bs x] field_simps)
3654 definition
3655   "msubst2 p c t =
3656     disj
3657       (conj (lt (CP (polyneg c))) (simpfm (msubstpos p c t)))
3658       (conj (lt (CP c)) (simpfm (msubstneg p c t)))"
3660 lemma msubst2:
3661   assumes lp: "islin p"
3662     and nc: "isnpoly c"
3663     and nz: "Ipoly vs c \<noteq> 0"
3664   shows "Ifm vs (x#bs) (msubst2 p c t) = Ifm vs (Itm vs (x#bs) t /  Ipoly vs c #bs) p"
3665 proof -
3666   let ?c = "Ipoly vs c"
3667   from nc have anc: "allpolys isnpoly (CP c)" "allpolys isnpoly (CP (~\<^sub>p c))"
3669   from nz have "?c > 0 \<or> ?c < 0" by arith
3670   moreover
3671   {
3672     assume c: "?c < 0"
3673     from c msubstneg_I[OF lp c, of x bs t] lt[OF anc(1), of vs "x#bs"] lt[OF anc(2), of vs "x#bs"]
3674     have ?thesis by (auto simp add: msubst2_def)
3675   }
3676   moreover
3677   {
3678     assume c: "?c > 0"
3679     from c msubstpos_I[OF lp c, of x bs t] lt[OF anc(1), of vs "x#bs"] lt[OF anc(2), of vs "x#bs"]
3680     have ?thesis by (auto simp add: msubst2_def)
3681   }
3682   ultimately show ?thesis by blast
3683 qed
3685 lemma msubsteq2_nb: "tmbound0 t \<Longrightarrow> islin (Eq (CNP 0 a r)) \<Longrightarrow> bound0 (msubsteq2 c t a r)"
3688 lemma msubstltpos_nb: "tmbound0 t \<Longrightarrow> islin (Lt (CNP 0 a r)) \<Longrightarrow> bound0 (msubstltpos c t a r)"
3690 lemma msubstltneg_nb: "tmbound0 t \<Longrightarrow> islin (Lt (CNP 0 a r)) \<Longrightarrow> bound0 (msubstltneg c t a r)"
3693 lemma msubstlepos_nb: "tmbound0 t \<Longrightarrow> islin (Le (CNP 0 a r)) \<Longrightarrow> bound0 (msubstlepos c t a r)"
3695 lemma msubstleneg_nb: "tmbound0 t \<Longrightarrow> islin (Le (CNP 0 a r)) \<Longrightarrow> bound0 (msubstleneg c t a r)"
3698 lemma msubstpos_nb:
3699   assumes lp: "islin p"
3700     and tnb: "tmbound0 t"
3701   shows "bound0 (msubstpos p c t)"
3702   using lp tnb
3703   by (induct p c t rule: msubstpos.induct)
3704     (auto simp add: msubsteq2_nb msubstltpos_nb msubstlepos_nb)
3706 lemma msubstneg_nb:
3707   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
3708     and lp: "islin p"
3709     and tnb: "tmbound0 t"
3710   shows "bound0 (msubstneg p c t)"
3711   using lp tnb
3712   by (induct p c t rule: msubstneg.induct)
3713     (auto simp add: msubsteq2_nb msubstltneg_nb msubstleneg_nb)
3715 lemma msubst2_nb:
3716   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
3717     and lp: "islin p"
3718     and tnb: "tmbound0 t"
3719   shows "bound0 (msubst2 p c t)"
3720   using lp tnb
3721   by (simp add: msubst2_def msubstneg_nb msubstpos_nb lt_nb simpfm_bound0)
3723 lemma mult_minus2_left: "-2 * (x::'a::comm_ring_1) = - (2 * x)"
3724   by simp
3726 lemma mult_minus2_right: "(x::'a::comm_ring_1) * -2 = - (x * 2)"
3727   by simp
3729 lemma islin_qf: "islin p \<Longrightarrow> qfree p"
3730   by (induct p rule: islin.induct) (auto simp add: bound0_qf)
3732 lemma fr_eq_msubst2:
3733   assumes lp: "islin p"
3734   shows "(\<exists>x. Ifm vs (x#bs) p) \<longleftrightarrow>
3735     ((Ifm vs (x#bs) (minusinf p)) \<or>
3736      (Ifm vs (x#bs) (plusinf p)) \<or>
3737      Ifm vs (x#bs) (subst0 (CP 0\<^sub>p) p) \<or>
3738      (\<exists>(n, t) \<in> set (uset p).
3739       Ifm vs (x# bs) (msubst2 p (n *\<^sub>p (C (-2,1))) t)) \<or>
3740       (\<exists>(c, t) \<in> set (uset p). \<exists>(d, s) \<in> set (uset p).
3741         Ifm vs (x#bs) (msubst2 p (C (-2, 1) *\<^sub>p c*\<^sub>p d) (Add (Mul d t) (Mul c s)))))"
3742   (is "(\<exists>x. ?I x p) = (?M \<or> ?P \<or> ?Pz \<or> ?PU \<or> ?F)" is "?E = ?D")
3743 proof -
3744   from uset_l[OF lp] have th: "\<forall>(c, s)\<in>set (uset p). isnpoly c \<and> tmbound0 s"
3745     by blast
3746   let ?I = "\<lambda>p. Ifm vs (x#bs) p"
3747   have n2: "isnpoly (C (-2,1))"
3749   note eq0 = subst0[OF islin_qf[OF lp], of vs x bs "CP 0\<^sub>p", simplified]
3751   have eq1: "(\<exists>(n, t) \<in> set (uset p). ?I (msubst2 p (n *\<^sub>p (C (-2,1))) t)) \<longleftrightarrow>
3752     (\<exists>(n, t) \<in> set (uset p).
3753       \<lparr>n\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0 \<and>
3754       Ifm vs (- Itm vs (x # bs) t / (\<lparr>n\<rparr>\<^sub>p\<^bsup>vs\<^esup> * 2) # bs) p)"
3755   proof -
3756     {
3757       fix n t
3758       assume H: "(n, t) \<in> set (uset p)" "?I(msubst2 p (n *\<^sub>p C (-2, 1)) t)"
3759       from H(1) th have "isnpoly n"
3760         by blast
3761       then have nn: "isnpoly (n *\<^sub>p (C (-2,1)))"
3762         by (simp_all add: polymul_norm n2)
3763       have nn': "allpolys isnpoly (CP (~\<^sub>p (n *\<^sub>p C (-2, 1))))"
3764         by (simp add: polyneg_norm nn)
3765       then have nn2: "\<lparr>n *\<^sub>p(C (-2,1)) \<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0" "\<lparr>n \<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0"
3766         using H(2) nn' nn
3767         by (auto simp add: msubst2_def lt zero_less_mult_iff mult_less_0_iff)
3768       from msubst2[OF lp nn nn2(1), of x bs t]
3769       have "\<lparr>n\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0 \<and> Ifm vs (- Itm vs (x # bs) t / (\<lparr>n\<rparr>\<^sub>p\<^bsup>vs\<^esup> * 2) # bs) p"
3770         using H(2) nn2 by (simp add: mult_minus2_right)
3771     }
3772     moreover
3773     {
3774       fix n t
3775       assume H:
3776         "(n, t) \<in> set (uset p)" "\<lparr>n\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0"
3777         "Ifm vs (- Itm vs (x # bs) t / (\<lparr>n\<rparr>\<^sub>p\<^bsup>vs\<^esup> * 2) # bs) p"
3778       from H(1) th have "isnpoly n"
3779         by blast
3780       then have nn: "isnpoly (n *\<^sub>p (C (-2,1)))" "\<lparr>n *\<^sub>p(C (-2,1)) \<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0"
3781         using H(2) by (simp_all add: polymul_norm n2)
3782       from msubst2[OF lp nn, of x bs t] have "?I (msubst2 p (n *\<^sub>p (C (-2,1))) t)"
3783         using H(2,3) by (simp add: mult_minus2_right)
3784     }
3785     ultimately show ?thesis by blast
3786   qed
3787   have eq2: "(\<exists>(c, t) \<in> set (uset p). \<exists>(d, s) \<in> set (uset p).
3788       Ifm vs (x#bs) (msubst2 p (C (-2, 1) *\<^sub>p c*\<^sub>p d) (Add (Mul d t) (Mul c s)))) \<longleftrightarrow>
3789     (\<exists>(n, t)\<in>set (uset p). \<exists>(m, s)\<in>set (uset p).
3790       \<lparr>n\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0 \<and>
3791       \<lparr>m\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0 \<and>
3792       Ifm vs ((- Itm vs (x # bs) t / \<lparr>n\<rparr>\<^sub>p\<^bsup>vs\<^esup> + - Itm vs (x # bs) s / \<lparr>m\<rparr>\<^sub>p\<^bsup>vs\<^esup>) / 2 # bs) p)"
3793   proof -
3794     {
3795       fix c t d s
3796       assume H:
3797         "(c,t) \<in> set (uset p)" "(d,s) \<in> set (uset p)"
3798         "Ifm vs (x#bs) (msubst2 p (C (-2, 1) *\<^sub>p c*\<^sub>p d) (Add (Mul d t) (Mul c s)))"
3799       from H(1,2) th have "isnpoly c" "isnpoly d"
3800         by blast+
3801       then have nn: "isnpoly (C (-2, 1) *\<^sub>p c*\<^sub>p d)"
3802         by (simp_all add: polymul_norm n2)
3803       have stupid:
3804           "allpolys isnpoly (CP (~\<^sub>p (C (-2, 1) *\<^sub>p c *\<^sub>p d)))"
3805           "allpolys isnpoly (CP ((C (-2, 1) *\<^sub>p c *\<^sub>p d)))"
3806         by (simp_all add: polyneg_norm nn)
3807       have nn': "\<lparr>(C (-2, 1) *\<^sub>p c*\<^sub>p d)\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0" "\<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0" "\<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0"
3808         using H(3)
3809         by (auto simp add: msubst2_def lt[OF stupid(1)]
3810             lt[OF stupid(2)] zero_less_mult_iff mult_less_0_iff)
3811       from msubst2[OF lp nn nn'(1), of x bs ] H(3) nn'
3812       have "\<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0 \<and> \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0 \<and>
3813           Ifm vs ((- Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup> + - Itm vs (x # bs) s / \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>) / 2 # bs) p"
3815     }
3816     moreover
3817     {
3818       fix c t d s
3819       assume H:
3820         "(c, t) \<in> set (uset p)"
3821         "(d, s) \<in> set (uset p)"
3822         "\<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0"
3823         "\<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0"
3824         "Ifm vs ((- Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup> + - Itm vs (x # bs) s / \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>) / 2 # bs) p"
3825       from H(1,2) th have "isnpoly c" "isnpoly d"
3826         by blast+
3827       then have nn: "isnpoly (C (-2, 1) *\<^sub>p c*\<^sub>p d)" "\<lparr>(C (-2, 1) *\<^sub>p c*\<^sub>p d)\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0"
3828         using H(3,4) by (simp_all add: polymul_norm n2)
3829       from msubst2[OF lp nn, of x bs ] H(3,4,5)
3830       have "Ifm vs (x#bs) (msubst2 p (C (-2, 1) *\<^sub>p c*\<^sub>p d) (Add (Mul d t) (Mul c s)))"
3832     }
3833     ultimately show ?thesis by blast
3834   qed
3835   from fr_eq2[OF lp, of vs bs x] show ?thesis
3836     unfolding eq0 eq1 eq2 by blast
3837 qed
3839 definition
3840   "ferrack2 p \<equiv>
3841     let
3842       q = simpfm p;
3843       mp = minusinf q;
3844       pp = plusinf q
3845     in
3846       if (mp = T \<or> pp = T) then T
3847       else
3848        (let U = remdups (uset  q)
3849         in
3850           decr0
3851             (list_disj
3852               [mp,
3853                pp,
3854                simpfm (subst0 (CP 0\<^sub>p) q),
3855                evaldjf (\<lambda>(c, t). msubst2 q (c *\<^sub>p C (-2, 1)) t) U,
3856                evaldjf (\<lambda>((b, a),(d, c)).
3857                 msubst2 q (C (-2, 1) *\<^sub>p b*\<^sub>p d) (Add (Mul d a) (Mul b c))) (alluopairs U)]))"
3859 definition "frpar2 p = simpfm (qelim (prep p) ferrack2)"
3861 lemma ferrack2:
3862   assumes qf: "qfree p"
3863   shows "qfree (ferrack2 p) \<and> Ifm vs bs (ferrack2 p) = Ifm vs bs (E p)"
3864   (is "_ \<and> (?rhs = ?lhs)")
3865 proof -
3866   let ?J = "\<lambda>x p. Ifm vs (x#bs) p"
3867   let ?N = "\<lambda>t. Ipoly vs t"
3868   let ?Nt = "\<lambda>x t. Itm vs (x#bs) t"
3869   let ?q = "simpfm p"
3870   let ?qz = "subst0 (CP 0\<^sub>p) ?q"
3871   let ?U = "remdups(uset ?q)"
3872   let ?Up = "alluopairs ?U"
3873   let ?mp = "minusinf ?q"
3874   let ?pp = "plusinf ?q"
3875   fix x
3876   let ?I = "\<lambda>p. Ifm vs (x#bs) p"
3877   from simpfm_lin[OF qf] simpfm_qf[OF qf] have lq: "islin ?q" and q_qf: "qfree ?q" .
3878   from minusinf_nb[OF lq] plusinf_nb[OF lq] have mp_nb: "bound0 ?mp" and pp_nb: "bound0 ?pp" .
3879   from bound0_qf[OF mp_nb] bound0_qf[OF pp_nb] have mp_qf: "qfree ?mp" and pp_qf: "qfree ?pp" .
3880   from uset_l[OF lq]
3881   have U_l: "\<forall>(c, s)\<in>set ?U. isnpoly c \<and> c \<noteq> 0\<^sub>p \<and> tmbound0 s \<and> allpolys isnpoly s"
3882     by simp
3883   have bnd0: "\<forall>x \<in> set ?U. bound0 ((\<lambda>(c,t). msubst2 ?q (c *\<^sub>p C (-2, 1)) t) x)"
3884   proof -
3885     {
3886       fix c t
3887       assume ct: "(c, t) \<in> set ?U"
3888       then have tnb: "tmbound0 t"
3889         using U_l by blast
3890       from msubst2_nb[OF lq tnb]
3891       have "bound0 ((\<lambda>(c,t). msubst2 ?q (c *\<^sub>p C (-2, 1)) t) (c,t))" by simp
3892     }
3893     then show ?thesis by auto
3894   qed
3895   have bnd1: "\<forall>x \<in> set ?Up. bound0 ((\<lambda>((b, a), (d, c)).
3896     msubst2 ?q (C (-2, 1) *\<^sub>p b*\<^sub>p d) (Add (Mul d a) (Mul b c))) x)"
3897   proof -
3898     {
3899       fix b a d c
3900       assume badc: "((b,a),(d,c)) \<in> set ?Up"
3901       from badc U_l alluopairs_set1[of ?U]
3902       have nb: "tmbound0 (Add (Mul d a) (Mul b c))"
3903         by auto
3904       from msubst2_nb[OF lq nb]
3905       have "bound0 ((\<lambda>((b, a),(d, c)).
3906           msubst2 ?q (C (-2, 1) *\<^sub>p b*\<^sub>p d) (Add (Mul d a) (Mul b c))) ((b,a),(d,c)))"
3907         by simp
3908     }
3909     then show ?thesis by auto
3910   qed
3911   have stupid: "bound0 F"
3912     by simp
3913   let ?R =
3914     "list_disj
3915      [?mp,
3916       ?pp,
3917       simpfm (subst0 (CP 0\<^sub>p) ?q),
3918       evaldjf (\<lambda>(c,t). msubst2 ?q (c *\<^sub>p C (-2, 1)) t) ?U,
3919       evaldjf (\<lambda>((b,a),(d,c)).
3920         msubst2 ?q (C (-2, 1) *\<^sub>p b*\<^sub>p d) (Add (Mul d a) (Mul b c))) (alluopairs ?U)]"
3921   from subst0_nb[of "CP 0\<^sub>p" ?q] q_qf
3922     evaldjf_bound0[OF bnd1] evaldjf_bound0[OF bnd0] mp_nb pp_nb stupid
3923   have nb: "bound0 ?R"
3924     by (simp add: list_disj_def simpfm_bound0)
3925   let ?s = "\<lambda>((b, a),(d, c)). msubst2 ?q (C (-2, 1) *\<^sub>p b*\<^sub>p d) (Add (Mul d a) (Mul b c))"
3927   {
3928     fix b a d c
3929     assume baU: "(b,a) \<in> set ?U" and dcU: "(d,c) \<in> set ?U"
3930     from U_l baU dcU have norm: "isnpoly b" "isnpoly d" "isnpoly (C (-2, 1))"
3931       by auto (simp add: isnpoly_def)
3932     have norm2: "isnpoly (C (-2, 1) *\<^sub>p b*\<^sub>p d)" "isnpoly (C (-2, 1) *\<^sub>p d*\<^sub>p b)"
3933       using norm by (simp_all add: polymul_norm)
3934     have stupid:
3935         "allpolys isnpoly (CP (C (-2, 1) *\<^sub>p b *\<^sub>p d))"
3936         "allpolys isnpoly (CP (C (-2, 1) *\<^sub>p d *\<^sub>p b))"
3937         "allpolys isnpoly (CP (~\<^sub>p(C (-2, 1) *\<^sub>p b *\<^sub>p d)))"
3938         "allpolys isnpoly (CP (~\<^sub>p(C (-2, 1) *\<^sub>p d*\<^sub>p b)))"
3939       by (simp_all add: polyneg_norm norm2)
3940     have "?I (msubst2 ?q (C (-2, 1) *\<^sub>p b*\<^sub>p d) (Add (Mul d a) (Mul b c))) =
3941         ?I (msubst2 ?q (C (-2, 1) *\<^sub>p d*\<^sub>p b) (Add (Mul b c) (Mul d a)))"
3942       (is "?lhs \<longleftrightarrow> ?rhs")
3943     proof
3944       assume H: ?lhs
3945       then have z: "\<lparr>C (-2, 1) *\<^sub>p b *\<^sub>p d\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0" "\<lparr>C (-2, 1) *\<^sub>p d *\<^sub>p b\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0"
3946         by (auto simp add: msubst2_def lt[OF stupid(3)] lt[OF stupid(1)]
3947             mult_less_0_iff zero_less_mult_iff)
3948       from msubst2[OF lq norm2(1) z(1), of x bs] msubst2[OF lq norm2(2) z(2), of x bs] H
3949       show ?rhs
3951     next
3952       assume H: ?rhs
3953       then have z: "\<lparr>C (-2, 1) *\<^sub>p b *\<^sub>p d\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0" "\<lparr>C (-2, 1) *\<^sub>p d *\<^sub>p b\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0"
3954         by (auto simp add: msubst2_def lt[OF stupid(4)] lt[OF stupid(2)]
3955             mult_less_0_iff zero_less_mult_iff)
3956       from msubst2[OF lq norm2(1) z(1), of x bs] msubst2[OF lq norm2(2) z(2), of x bs] H
3957       show ?lhs
3959     qed
3960   }
3961   then have th0: "\<forall>x \<in> set ?U. \<forall>y \<in> set ?U. ?I (?s (x, y)) \<longleftrightarrow> ?I (?s (y, x))"
3962     by auto
3964   have "?lhs \<longleftrightarrow> (\<exists>x. Ifm vs (x#bs) ?q)"
3965     by simp
3966   also have "\<dots> \<longleftrightarrow> ?I ?mp \<or> ?I ?pp \<or> ?I (subst0 (CP 0\<^sub>p) ?q) \<or>
3967       (\<exists>(n, t) \<in> set ?U. ?I (msubst2 ?q (n *\<^sub>p C (-2, 1)) t)) \<or>
3968       (\<exists>(b, a) \<in> set ?U. \<exists>(d, c) \<in> set ?U.
3969         ?I (msubst2 ?q (C (-2, 1) *\<^sub>p b*\<^sub>p d) (Add (Mul d a) (Mul b c))))"
3970     using fr_eq_msubst2[OF lq, of vs bs x] by simp
3971   also have "\<dots> \<longleftrightarrow> ?I ?mp \<or> ?I ?pp \<or> ?I (subst0 (CP 0\<^sub>p) ?q) \<or>
3972       (\<exists>(n, t) \<in> set ?U. ?I (msubst2 ?q (n *\<^sub>p C (-2, 1)) t)) \<or>
3973       (\<exists>x \<in> set ?U. \<exists>y \<in>set ?U. ?I (?s (x, y)))"
3975   also have "\<dots> \<longleftrightarrow> ?I ?mp \<or> ?I ?pp \<or> ?I (subst0 (CP 0\<^sub>p) ?q) \<or>
3976       (\<exists>(n, t) \<in> set ?U. ?I (msubst2 ?q (n *\<^sub>p C (-2, 1)) t)) \<or>
3977       (\<exists>(x, y) \<in> set ?Up. ?I (?s (x, y)))"
3978     using alluopairs_bex[OF th0] by simp
3979   also have "\<dots> \<longleftrightarrow> ?I ?R"
3980     by (simp add: list_disj_def evaldjf_ex split_def)
3981   also have "\<dots> \<longleftrightarrow> ?rhs"
3982     unfolding ferrack2_def
3983     apply (cases "?mp = T")
3985     apply (cases "?pp = T")
3987     apply (simp_all add: Let_def decr0[OF nb])
3988     done
3989   finally show ?thesis using decr0_qf[OF nb]
3990     by (simp add: ferrack2_def Let_def)
3991 qed
3993 lemma frpar2: "qfree (frpar2 p) \<and> (Ifm vs bs (frpar2 p) \<longleftrightarrow> Ifm vs bs p)"
3994 proof -
3995   from ferrack2
3996   have th: "\<forall>bs p. qfree p \<longrightarrow> qfree (ferrack2 p) \<and> Ifm vs bs (ferrack2 p) = Ifm vs bs (E p)"
3997     by blast
3998   from qelim[OF th, of "prep p" bs]
3999   show ?thesis
4000     unfolding frpar2_def by (auto simp add: prep)
4001 qed
4003 oracle frpar_oracle = {*
4004 let
4006 fun binopT T = T --> T --> T;
4007 fun relT T = T --> T --> @{typ bool};
4009 val mk_C = @{code C} o pairself @{code int_of_integer};
4010 val mk_poly_Bound = @{code poly.Bound} o @{code nat_of_integer};
4011 val mk_Bound = @{code Bound} o @{code nat_of_integer};
4013 val dest_num = snd o HOLogic.dest_number;
4015 fun try_dest_num t = SOME ((snd o HOLogic.dest_number) t)
4016   handle TERM _ => NONE;
4018 fun dest_nat (t as Const (@{const_name Suc}, _)) = HOLogic.dest_nat t
4019   | dest_nat t = dest_num t;
4021 fun the_index ts t =
4022   let
4023     val k = find_index (fn t' => t aconv t') ts;
4024   in if k < 0 then raise General.Subscript else k end;
4026 fun num_of_term ps (Const (@{const_name Groups.uminus}, _) \$ t) =
4027       @{code poly.Neg} (num_of_term ps t)
4028   | num_of_term ps (Const (@{const_name Groups.plus}, _) \$ a \$ b) =
4029       @{code poly.Add} (num_of_term ps a, num_of_term ps b)
4030   | num_of_term ps (Const (@{const_name Groups.minus}, _) \$ a \$ b) =
4031       @{code poly.Sub} (num_of_term ps a, num_of_term ps b)
4032   | num_of_term ps (Const (@{const_name Groups.times}, _) \$ a \$ b) =
4033       @{code poly.Mul} (num_of_term ps a, num_of_term ps b)
4034   | num_of_term ps (Const (@{const_name Power.power}, _) \$ a \$ n) =
4035       @{code poly.Pw} (num_of_term ps a, @{code nat_of_integer} (dest_nat n))
4036   | num_of_term ps (Const (@{const_name Fields.divide}, _) \$ a \$ b) =
4037       mk_C (dest_num a, dest_num b)
4038   | num_of_term ps t =
4039       (case try_dest_num t of
4040         SOME k => mk_C (k, 1)
4041       | NONE => mk_poly_Bound (the_index ps t));
4043 fun tm_of_term fs ps (Const(@{const_name Groups.uminus}, _) \$ t) =
4044       @{code Neg} (tm_of_term fs ps t)
4045   | tm_of_term fs ps (Const(@{const_name Groups.plus}, _) \$ a \$ b) =
4046       @{code Add} (tm_of_term fs ps a, tm_of_term fs ps b)
4047   | tm_of_term fs ps (Const(@{const_name Groups.minus}, _) \$ a \$ b) =
4048       @{code Sub} (tm_of_term fs ps a, tm_of_term fs ps b)
4049   | tm_of_term fs ps (Const(@{const_name Groups.times}, _) \$ a \$ b) =
4050       @{code Mul} (num_of_term ps a, tm_of_term fs ps b)
4051   | tm_of_term fs ps t = (@{code CP} (num_of_term ps t)
4052       handle TERM _ => mk_Bound (the_index fs t)
4053         | General.Subscript => mk_Bound (the_index fs t));
4055 fun fm_of_term fs ps @{term True} = @{code T}
4056   | fm_of_term fs ps @{term False} = @{code F}
4057   | fm_of_term fs ps (Const (@{const_name Not}, _) \$ p) =
4058       @{code NOT} (fm_of_term fs ps p)
4059   | fm_of_term fs ps (Const (@{const_name HOL.conj}, _) \$ p \$ q) =
4060       @{code And} (fm_of_term fs ps p, fm_of_term fs ps q)
4061   | fm_of_term fs ps (Const (@{const_name HOL.disj}, _) \$ p \$ q) =
4062       @{code Or} (fm_of_term fs ps p, fm_of_term fs ps q)
4063   | fm_of_term fs ps (Const (@{const_name HOL.implies}, _) \$ p \$ q) =
4064       @{code Imp} (fm_of_term fs ps p, fm_of_term fs ps q)
4065   | fm_of_term fs ps (@{term HOL.iff} \$ p \$ q) =
4066       @{code Iff} (fm_of_term fs ps p, fm_of_term fs ps q)
4067   | fm_of_term fs ps (Const (@{const_name HOL.eq}, T) \$ p \$ q) =
4068       @{code Eq} (@{code Sub} (tm_of_term fs ps p, tm_of_term fs ps q))
4069   | fm_of_term fs ps (Const (@{const_name Orderings.less}, _) \$ p \$ q) =
4070       @{code Lt} (@{code Sub} (tm_of_term fs ps p, tm_of_term fs ps q))
4071   | fm_of_term fs ps (Const (@{const_name Orderings.less_eq}, _) \$ p \$ q) =
4072       @{code Le} (@{code Sub} (tm_of_term fs ps p, tm_of_term fs ps q))
4073   | fm_of_term fs ps (Const (@{const_name Ex}, _) \$ Abs (abs as (_, xT, _))) =
4074       let
4075         val (xn', p') = Syntax_Trans.variant_abs abs;  (* FIXME !? *)
4076       in @{code E} (fm_of_term (Free (xn', xT) :: fs) ps p') end
4077   | fm_of_term fs ps (Const (@{const_name All},_) \$ Abs (abs as (_, xT, _))) =
4078       let
4079         val (xn', p') = Syntax_Trans.variant_abs abs;  (* FIXME !? *)
4080       in @{code A} (fm_of_term (Free (xn', xT) :: fs) ps p') end
4081   | fm_of_term fs ps _ = error "fm_of_term";
4083 fun term_of_num T ps (@{code poly.C} (a, b)) =
4084       let
4085         val (c, d) = pairself (@{code integer_of_int}) (a, b)
4086       in
4087         (if d = 1 then HOLogic.mk_number T c
4088         else if d = 0 then Const (@{const_name Groups.zero}, T)
4089         else
4090           Const (@{const_name Fields.divide}, binopT T) \$
4091             HOLogic.mk_number T c \$ HOLogic.mk_number T d)
4092       end
4093   | term_of_num T ps (@{code poly.Bound} i) = nth ps (@{code integer_of_nat} i)
4094   | term_of_num T ps (@{code poly.Add} (a, b)) =
4095       Const (@{const_name Groups.plus}, binopT T) \$ term_of_num T ps a \$ term_of_num T ps b
4096   | term_of_num T ps (@{code poly.Mul} (a, b)) =
4097       Const (@{const_name Groups.times}, binopT T) \$ term_of_num T ps a \$ term_of_num T ps b
4098   | term_of_num T ps (@{code poly.Sub} (a, b)) =
4099       Const (@{const_name Groups.minus}, binopT T) \$ term_of_num T ps a \$ term_of_num T ps b
4100   | term_of_num T ps (@{code poly.Neg} a) =
4101       Const (@{const_name Groups.uminus}, T --> T) \$ term_of_num T ps a
4102   | term_of_num T ps (@{code poly.Pw} (a, n)) =
4103       Const (@{const_name Power.power}, T --> @{typ nat} --> T) \$
4104         term_of_num T ps a \$ HOLogic.mk_number HOLogic.natT (@{code integer_of_nat} n)
4105   | term_of_num T ps (@{code poly.CN} (c, n, p)) =
4106       term_of_num T ps (@{code poly.Add} (c, @{code poly.Mul} (@{code poly.Bound} n, p)));
4108 fun term_of_tm T fs ps (@{code CP} p) = term_of_num T ps p
4109   | term_of_tm T fs ps (@{code Bound} i) = nth fs (@{code integer_of_nat} i)
4110   | term_of_tm T fs ps (@{code Add} (a, b)) =
4111       Const (@{const_name Groups.plus}, binopT T) \$ term_of_tm T fs ps a \$ term_of_tm T fs ps b
4112   | term_of_tm T fs ps (@{code Mul} (a, b)) =
4113       Const (@{const_name Groups.times}, binopT T) \$ term_of_num T ps a \$ term_of_tm T fs ps b
4114   | term_of_tm T fs ps (@{code Sub} (a, b)) =
4115       Const (@{const_name Groups.minus}, binopT T) \$ term_of_tm T fs ps a \$ term_of_tm T fs ps b
4116   | term_of_tm T fs ps (@{code Neg} a) =
4117       Const (@{const_name Groups.uminus}, T --> T) \$ term_of_tm T fs ps a
4118   | term_of_tm T fs ps (@{code CNP} (n, c, p)) =
4119       term_of_tm T fs ps (@{code Add} (@{code Mul} (c, @{code Bound} n), p));
4121 fun term_of_fm T fs ps @{code T} = @{term True}
4122   | term_of_fm T fs ps @{code F} = @{term False}
4123   | term_of_fm T fs ps (@{code NOT} p) = @{term Not} \$ term_of_fm T fs ps p
4124   | term_of_fm T fs ps (@{code And} (p, q)) =
4125       @{term HOL.conj} \$ term_of_fm T fs ps p \$ term_of_fm T fs ps q
4126   | term_of_fm T fs ps (@{code Or} (p, q)) =
4127       @{term HOL.disj} \$ term_of_fm T fs ps p \$ term_of_fm T fs ps q
4128   | term_of_fm T fs ps (@{code Imp} (p, q)) =
4129       @{term HOL.implies} \$ term_of_fm T fs ps p \$ term_of_fm T fs ps q
4130   | term_of_fm T fs ps (@{code Iff} (p, q)) =
4131       @{term HOL.iff} \$ term_of_fm T fs ps p \$ term_of_fm T fs ps q
4132   | term_of_fm T fs ps (@{code Lt} p) =
4133       Const (@{const_name Orderings.less}, relT T) \$
4134         term_of_tm T fs ps p \$ Const (@{const_name Groups.zero}, T)
4135   | term_of_fm T fs ps (@{code Le} p) =
4136       Const (@{const_name Orderings.less_eq}, relT T) \$
4137         term_of_tm T fs ps p \$ Const (@{const_name Groups.zero}, T)
4138   | term_of_fm T fs ps (@{code Eq} p) =
4139       Const (@{const_name HOL.eq}, relT T) \$
4140         term_of_tm T fs ps p \$ Const (@{const_name Groups.zero}, T)
4141   | term_of_fm T fs ps (@{code NEq} p) =
4142       @{term Not} \$
4143         (Const (@{const_name HOL.eq}, relT T) \$
4144           term_of_tm T fs ps p \$ Const (@{const_name Groups.zero}, T))
4145   | term_of_fm T fs ps _ = error "term_of_fm: quantifiers";
4147 fun frpar_procedure alternative T ps fm =
4148   let
4149     val frpar = if alternative then @{code frpar2} else @{code frpar};
4150     val fs = subtract (op aconv) (map Free (Term.add_frees fm [])) ps;
4151     val eval = term_of_fm T fs ps o frpar o fm_of_term fs ps;
4152     val t = HOLogic.dest_Trueprop fm;
4153   in HOLogic.mk_Trueprop (HOLogic.mk_eq (t, eval t)) end;
4155 in
4157   fn (ctxt, alternative, ty, ps, ct) =>
4158     cterm_of (Proof_Context.theory_of ctxt)
4159       (frpar_procedure alternative ty ps (term_of ct))
4161 end
4162 *}
4164 ML {*
4165 structure Parametric_Ferrante_Rackoff =
4166 struct
4168 fun tactic ctxt alternative T ps =
4169   Object_Logic.full_atomize_tac ctxt
4170   THEN' CSUBGOAL (fn (g, i) =>
4171     let
4172       val th = frpar_oracle (ctxt, alternative, T, ps, g);
4173     in rtac (th RS iffD2) i end);
4175 fun method alternative =
4176   let
4177     fun keyword k = Scan.lift (Args.\$\$\$ k -- Args.colon) >> K ();
4178     val parsN = "pars";
4179     val typN = "type";
4180     val any_keyword = keyword parsN || keyword typN;
4181     val terms = Scan.repeat (Scan.unless any_keyword Args.term);
4182     val typ = Scan.unless any_keyword Args.typ;
4183   in
4184     (keyword typN |-- typ) -- (keyword parsN |-- terms) >>
4185       (fn (T, ps) => fn ctxt => SIMPLE_METHOD' (tactic ctxt alternative T ps))
4186   end;
4188 end;
4189 *}
4191 method_setup frpar = {*
4192   Parametric_Ferrante_Rackoff.method false
4193 *} "parametric QE for linear Arithmetic over fields"
4195 method_setup frpar2 = {*
4196   Parametric_Ferrante_Rackoff.method true
4197 *} "parametric QE for linear Arithmetic over fields, Version 2"
4199 lemma "\<exists>(x::'a::{linordered_field_inverse_zero}). y \<noteq> -1 \<longrightarrow> (y + 1) * x < 0"
4200   apply (frpar type: 'a pars: y)
4202   apply (rule spec[where x=y])
4203   apply (frpar type: 'a pars: "z::'a")
4204   apply simp
4205   done
4207 lemma "\<exists>(x::'a::{linordered_field_inverse_zero}). y \<noteq> -1 \<longrightarrow> (y + 1)*x < 0"
4208   apply (frpar2 type: 'a pars: y)
4210   apply (rule spec[where x=y])
4211   apply (frpar2 type: 'a pars: "z::'a")
4212   apply simp
4213   done
4215 text{* Collins/Jones Problem *}
4216 (*
4217 lemma "\<exists>(r::'a::{linordered_field_inverse_zero, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0"
4218 proof-
4219   have "(\<exists>(r::'a::{linordered_field_inverse_zero, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0) \<longleftrightarrow> (\<exists>(r::'a::{linordered_field_inverse_zero, number_ring}). 0 < r \<and> r < 1 \<and> 0 < 2 *(a^2 + b^2) - (3*(a^2 + b^2)) * r + (2*a)*r \<and> 2*(a^2 + b^2) - (3*(a^2 + b^2) - 4*a + 1)*r - 2*a < 0)" (is "?lhs \<longleftrightarrow> ?rhs")
4221 have "?rhs"
4223   apply (frpar type: "'a::{linordered_field_inverse_zero, number_ring}" pars: "a::'a::{linordered_field_inverse_zero, number_ring}" "b::'a::{linordered_field_inverse_zero, number_ring}")
4225 oops
4226 *)
4227 (*
4228 lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}) y. (1 - t)*x \<le> (1+t)*y \<and> (1 - t)*y \<le> (1+t)*x --> 0 \<le> y"
4229 apply (frpar type: "'a::{linordered_field_inverse_zero, number_ring}" pars: "t::'a::{linordered_field_inverse_zero, number_ring}")
4230 oops
4231 *)
4233 text{* Collins/Jones Problem *}
4235 (*
4236 lemma "\<exists>(r::'a::{linordered_field_inverse_zero, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0"
4237 proof-
4238   have "(\<exists>(r::'a::{linordered_field_inverse_zero, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0) \<longleftrightarrow> (\<exists>(r::'a::{linordered_field_inverse_zero, number_ring}). 0 < r \<and> r < 1 \<and> 0 < 2 *(a^2 + b^2) - (3*(a^2 + b^2)) * r + (2*a)*r \<and> 2*(a^2 + b^2) - (3*(a^2 + b^2) - 4*a + 1)*r - 2*a < 0)" (is "?lhs \<longleftrightarrow> ?rhs")