src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
author wenzelm
Fri Mar 06 15:58:56 2015 +0100 (2015-03-06)
changeset 59621 291934bac95e
parent 59582 0fbed69ff081
child 59867 58043346ca64
permissions -rw-r--r--
Thm.cterm_of and Thm.ctyp_of operate on local context;
     1 (*  Title:      HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
     2     Author:     Amine Chaieb
     3 *)
     4 
     5 section{* A formalization of Ferrante and Rackoff's procedure with polynomial parameters, see Paper in CALCULEMUS 2008 *}
     6 
     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
    15 
    16 subsection {* Terms *}
    17 
    18 datatype tm = CP poly | Bound nat | Add tm tm | Mul poly tm
    19   | Neg tm | Sub tm tm | CNP nat poly tm
    20 
    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 "
    31 
    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"
    42 
    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"
    52 
    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"
    62 
    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"
    72 
    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)
    78 
    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"
    88 
    89 lemma tmbound0_tmbound_iff: "tmbound 0 t = tmbound0 t"
    90   by (induct t) auto
    91 
    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
    99 
   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"
   109 
   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"
   119 
   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
   124 
   125 lemma incrtm0: "Itm vs (x#bs) (incrtm0 t) = Itm vs bs t"
   126   by (induct t rule: decrtm0.induct) simp_all
   127 
   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))"
   137 
   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)))"
   142 
   143 lemma removen_same: "n \<ge> length xs \<Longrightarrow> removen n xs = xs"
   144   by (induct xs arbitrary: n) auto
   145 
   146 lemma nth_length_exceeds: "n \<ge> length xs \<Longrightarrow> xs!n = []!(n - length xs)"
   147   by (induct xs arbitrary: n) auto
   148 
   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)
   152 
   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
   202 
   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)
   209 
   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)"
   219 
   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
   222 
   223 lemma tmsubst0_nb: "tmbound0 t \<Longrightarrow> tmbound0 (tmsubst0 t a)"
   224   by (induct a rule: tm.induct) auto
   225 
   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)"
   236 
   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
   243 
   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
   249 
   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
   255 
   256 lemma incrtm0_tmbound: "tmbound n t \<Longrightarrow> tmbound (Suc n) (incrtm0 t)"
   257   by (induct t) auto
   258 
   259 (* Simplification *)
   260 
   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)"
   272   "tmadd (a, b) = Add a b"
   273 
   274 lemma tmadd[simp]: "Itm vs bs (tmadd (t, s)) = Itm vs bs (Add t s)"
   275   apply (induct t s rule: tmadd.induct, simp_all add: Let_def)
   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])
   279   apply (auto simp del: polyadd simp add: polyadd[symmetric])
   280   done
   281 
   282 lemma tmadd_nb0[simp]: "tmbound0 t \<Longrightarrow> tmbound0 s \<Longrightarrow> tmbound0 (tmadd (t, s))"
   283   by (induct t s rule: tmadd.induct) (auto simp add: Let_def)
   284 
   285 lemma tmadd_nb[simp]: "tmbound n t \<Longrightarrow> tmbound n s \<Longrightarrow> tmbound n (tmadd (t, s))"
   286   by (induct t s rule: tmadd.induct) (auto simp add: Let_def)
   287 
   288 lemma tmadd_blt[simp]: "tmboundslt n t \<Longrightarrow> tmboundslt n s \<Longrightarrow> tmboundslt n (tmadd (t, s))"
   289   by (induct t s rule: tmadd.induct) (auto simp add: Let_def)
   290 
   291 lemma tmadd_allpolys_npoly[simp]:
   292   "allpolys isnpoly t \<Longrightarrow> allpolys isnpoly s \<Longrightarrow> allpolys isnpoly (tmadd(t, s))"
   293   by (induct t s rule: tmadd.induct) (simp_all add: Let_def polyadd_norm)
   294 
   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)"
   300 
   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)
   303 
   304 lemma tmmul_nb0[simp]: "tmbound0 t \<Longrightarrow> tmbound0 (tmmul t i)"
   305   by (induct t arbitrary: i rule: tmmul.induct) auto
   306 
   307 lemma tmmul_nb[simp]: "tmbound n t \<Longrightarrow> tmbound n (tmmul t i)"
   308   by (induct t arbitrary: n rule: tmmul.induct) auto
   309 
   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)
   312 
   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)
   317 
   318 definition tmneg :: "tm \<Rightarrow> tm"
   319   where "tmneg t \<equiv> tmmul t (C (- 1,1))"
   320 
   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))"
   323 
   324 lemma tmneg[simp]: "Itm vs bs (tmneg t) = Itm vs bs (Neg t)"
   325   using tmneg_def[of t] by simp
   326 
   327 lemma tmneg_nb0[simp]: "tmbound0 t \<Longrightarrow> tmbound0 (tmneg t)"
   328   using tmneg_def by simp
   329 
   330 lemma tmneg_nb[simp]: "tmbound n t \<Longrightarrow> tmbound n (tmneg t)"
   331   using tmneg_def by simp
   332 
   333 lemma tmneg_blt[simp]: "tmboundslt n t \<Longrightarrow> tmboundslt n (tmneg t)"
   334   using tmneg_def by simp
   335 
   336 lemma [simp]: "isnpoly (C (-1, 1))"
   337   unfolding isnpoly_def by simp
   338 
   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
   343 
   344 lemma tmsub[simp]: "Itm vs bs (tmsub a b) = Itm vs bs (Sub a b)"
   345   using tmsub_def by simp
   346 
   347 lemma tmsub_nb0[simp]: "tmbound0 t \<Longrightarrow> tmbound0 s \<Longrightarrow> tmbound0 (tmsub t s)"
   348   using tmsub_def by simp
   349 
   350 lemma tmsub_nb[simp]: "tmbound n t \<Longrightarrow> tmbound n s \<Longrightarrow> tmbound n (tmsub t s)"
   351   using tmsub_def by simp
   352 
   353 lemma tmsub_blt[simp]: "tmboundslt n t \<Longrightarrow> tmboundslt n s \<Longrightarrow> tmboundslt n (tmsub t s)"
   354   using tmsub_def by simp
   355 
   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)
   360 
   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)"
   366 | "simptm (Add t s) = tmadd (simptm t,simptm s)"
   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))"
   372 
   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
   379 
   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)
   382 
   383 lemma simptm_tmbound0[simp]: "tmbound0 t \<Longrightarrow> tmbound0 (simptm t)"
   384   by (induct t rule: simptm.induct) (auto simp add: Let_def)
   385 
   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)
   388 
   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)
   391 
   392 lemma [simp]: "isnpoly 0\<^sub>p"
   393   and [simp]: "isnpoly (C(1,1))"
   394   by (simp_all add: isnpoly_def)
   395 
   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)
   400 
   401 declare let_cong[fundef_cong del]
   402 
   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)"
   413 
   414 declare let_cong[fundef_cong]
   415 
   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
   421 
   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
   435 
   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
   446 
   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
   458 
   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)"]
   463   by (simp add: tmbound0_tmbound_iff)
   464 
   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)
   469 
   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)
   474 
   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)
   477 
   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)
   480 
   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)
   483 
   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)
   486 
   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)
   491     (auto simp  add: polyadd_norm polysub_norm polyneg_norm polymul_norm Let_def split_def)
   492 
   493 
   494 subsection{* Formulae *}
   495 
   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
   498 
   499 
   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"
   511 
   512 (* several lemmas about fmsize *)
   513 lemma fmsize_pos[termination_simp]: "fmsize p > 0"
   514   by (induct p rule: fmsize.induct) simp_all
   515 
   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)"
   532 
   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"
   544 
   545 lemma not[simp]: "Ifm vs bs (not p) = Ifm vs bs (NOT p)"
   546   by (induct p rule: not.induct) auto
   547 
   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)"
   556 
   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)
   559 
   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)"
   568 
   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)
   571 
   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)"
   579 
   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)
   582 
   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)"
   593 
   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)
   596 
   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"
   608 
   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"
   625 
   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"
   640 
   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
   646 
   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"
   662 
   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
   690 
   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"
   703 
   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)
   709 
   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)"
   725 
   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)
   757 
   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"
   773 
   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
   779 
   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
   786 
   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)"
   802 
   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)
   843 
   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
   849 
   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
   858 
   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
   867 
   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
   876 
   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
   885 
   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
   896 
   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"
   906 
   907 lemma bound0_qf: "bound0 p \<Longrightarrow> qfree p"
   908   by (induct p) simp_all
   909 
   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))"
   916 
   917 definition evaldjf :: "('a \<Rightarrow> fm) \<Rightarrow> 'a list \<Rightarrow> fm"
   918   where "evaldjf f ps \<equiv> foldr (djf f) ps F"
   919 
   920 lemma djf_Or: "Ifm vs bs (djf f p q) = Ifm vs bs (Or (f p) q)"
   921   by (cases "q=T", simp add: djf_def,cases "q=F", simp add: djf_def)
   922     (cases "f p", simp_all add: Let_def djf_def)
   923 
   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)
   926 
   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)
   931 
   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)
   936 
   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]"
   942 
   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
   945 
   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
   954 
   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
   962 
   963 definition DJ :: "(fm \<Rightarrow> fm) \<Rightarrow> fm \<Rightarrow> fm"
   964   where "DJ f p \<equiv> evaldjf f (disjuncts p)"
   965 
   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
   977 
   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)"
   985     by (simp add: DJ_def)
   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
   992 
   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
  1012 
  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]"
  1018 
  1019 definition list_conj :: "fm list \<Rightarrow> fm"
  1020   where "list_conj ps \<equiv> foldr conj ps T"
  1021 
  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)))"
  1028 
  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
  1037 
  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
  1040 
  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
  1049 
  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"
  1062 
  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, rename_tac nat a b, case_tac nat, auto)+
  1070 
  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)"
  1075 
  1076 lemma lt: "allpolys isnpoly p \<Longrightarrow> Ifm vs bs (lt p) = Ifm vs bs (Lt p)"
  1077   apply (simp add: lt_def)
  1078   apply (cases p)
  1079   apply simp_all
  1080   apply (rename_tac poly, case_tac poly)
  1081   apply (simp_all add: isnpoly_def)
  1082   done
  1083 
  1084 lemma le: "allpolys isnpoly p \<Longrightarrow> Ifm vs bs (le p) = Ifm vs bs (Le p)"
  1085   apply (simp add: le_def)
  1086   apply (cases p)
  1087   apply simp_all
  1088   apply (rename_tac poly, case_tac poly)
  1089   apply (simp_all add: isnpoly_def)
  1090   done
  1091 
  1092 lemma eq: "allpolys isnpoly p \<Longrightarrow> Ifm vs bs (eq p) = Ifm vs bs (Eq p)"
  1093   apply (simp add: eq_def)
  1094   apply (cases p)
  1095   apply simp_all
  1096   apply (rename_tac poly, case_tac poly)
  1097   apply (simp_all add: isnpoly_def)
  1098   done
  1099 
  1100 lemma neq: "allpolys isnpoly p \<Longrightarrow> Ifm vs bs (neq p) = Ifm vs bs (NEq p)"
  1101   by (simp add: neq_def eq)
  1102 
  1103 lemma lt_lin: "tmbound0 p \<Longrightarrow> islin (lt p)"
  1104   apply (simp add: lt_def)
  1105   apply (cases p)
  1106   apply simp_all
  1107   apply (rename_tac poly, case_tac poly)
  1108   apply simp_all
  1109   apply (rename_tac nat a b, case_tac nat)
  1110   apply simp_all
  1111   done
  1112 
  1113 lemma le_lin: "tmbound0 p \<Longrightarrow> islin (le p)"
  1114   apply (simp add: le_def)
  1115   apply (cases p)
  1116   apply simp_all
  1117   apply (rename_tac poly, case_tac poly)
  1118   apply simp_all
  1119   apply (rename_tac nat a b, case_tac nat)
  1120   apply simp_all
  1121   done
  1122 
  1123 lemma eq_lin: "tmbound0 p \<Longrightarrow> islin (eq p)"
  1124   apply (simp add: eq_def)
  1125   apply (cases p)
  1126   apply simp_all
  1127   apply (rename_tac poly, case_tac poly)
  1128   apply simp_all
  1129   apply (rename_tac nat a b, case_tac nat)
  1130   apply simp_all
  1131   done
  1132 
  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 (rename_tac poly, case_tac poly)
  1138   apply simp_all
  1139   apply (rename_tac nat a b, case_tac nat)
  1140   apply simp_all
  1141   done
  1142 
  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))"
  1147 
  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])
  1155 
  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)
  1163 
  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)
  1171 
  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)
  1179 
  1180 lemma really_stupid: "\<not> (\<forall>c1 s'. (c1, s') \<noteq> split0 s)"
  1181   by (cases "split0 s") auto
  1182 
  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)
  1190     (auto simp add: Let_def split_def polyadd_norm polymul_norm polyneg_norm
  1191       polysub_norm really_stupid)
  1192 
  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
  1213 
  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
  1234 
  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
  1254 
  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
  1274 
  1275 lemma lt_nb: "tmbound0 t \<Longrightarrow> bound0 (lt t)"
  1276   apply (simp add: lt_def)
  1277   apply (cases t)
  1278   apply auto
  1279   apply (rename_tac poly, case_tac poly)
  1280   apply auto
  1281   done
  1282 
  1283 lemma le_nb: "tmbound0 t \<Longrightarrow> bound0 (le t)"
  1284   apply (simp add: le_def)
  1285   apply (cases t)
  1286   apply auto
  1287   apply (rename_tac poly, case_tac poly)
  1288   apply auto
  1289   done
  1290 
  1291 lemma eq_nb: "tmbound0 t \<Longrightarrow> bound0 (eq t)"
  1292   apply (simp add: eq_def)
  1293   apply (cases t)
  1294   apply auto
  1295   apply (rename_tac poly, case_tac poly)
  1296   apply auto
  1297   done
  1298 
  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 (rename_tac poly, case_tac poly)
  1304   apply auto
  1305   done
  1306 
  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"
  1320     by (simp_all add: isnpoly_def)
  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
  1327 
  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"
  1341     by (simp_all add: isnpoly_def)
  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
  1348 
  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"
  1362     by (simp_all add: isnpoly_def)
  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
  1369 
  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"
  1383     by (simp_all add: isnpoly_def)
  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
  1390 
  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]"
  1396 
  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
  1399 
  1400 definition list_disj :: "fm list \<Rightarrow> fm"
  1401   where "list_disj ps \<equiv> foldr disj ps F"
  1402 
  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)
  1405 
  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)
  1408 
  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)
  1411 
  1412 lemma conj_boundslt: "boundslt n p \<Longrightarrow> boundslt n q \<Longrightarrow> boundslt n (conj p q)"
  1413   unfolding conj_def by auto
  1414 
  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
  1423 
  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
  1433 
  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
  1437 
  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
  1444 
  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
  1447 
  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"
  1464     by (simp add: list_conj_nb')
  1465   then have yes_qf: "qfree (decr0 ?cyes)"
  1466     by (simp add: decr0_qf)
  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"
  1471     by (simp add: list_conj_qf)
  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
  1499 
  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"
  1524 
  1525 lemma simpfm[simp]: "Ifm vs bs (simpfm p) = Ifm vs bs p"
  1526   by (induct p arbitrary: bs rule: simpfm.induct) auto
  1527 
  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
  1532 
  1533 lemma lt_qf[simp]: "qfree (lt t)"
  1534   apply (cases t)
  1535   apply (auto simp add: lt_def)
  1536   apply (rename_tac poly, case_tac poly)
  1537   apply auto
  1538   done
  1539 
  1540 lemma le_qf[simp]: "qfree (le t)"
  1541   apply (cases t)
  1542   apply (auto simp add: le_def)
  1543   apply (rename_tac poly, case_tac poly)
  1544   apply auto
  1545   done
  1546 
  1547 lemma eq_qf[simp]: "qfree (eq t)"
  1548   apply (cases t)
  1549   apply (auto simp add: eq_def)
  1550   apply (rename_tac poly, case_tac poly)
  1551   apply auto
  1552   done
  1553 
  1554 lemma neq_qf[simp]: "qfree (neq t)" by (simp add: neq_def)
  1555 
  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)
  1560 
  1561 lemma simpfm_qf[simp]: "qfree p \<Longrightarrow> qfree (simpfm p)"
  1562   by (induct p rule: simpfm.induct) auto
  1563 
  1564 lemma disj_lin: "islin p \<Longrightarrow> islin q \<Longrightarrow> islin (disj p q)"
  1565   by (simp add: disj_def)
  1566 lemma conj_lin: "islin p \<Longrightarrow> islin q \<Longrightarrow> islin (conj p q)"
  1567   by (simp add: conj_def)
  1568 
  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)
  1573 
  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"
  1599 (hints simp add: fmsize_pos)
  1600 
  1601 lemma prep: "Ifm vs bs (prep p) = Ifm vs bs p"
  1602   by (induct p arbitrary: bs rule: prep.induct) auto
  1603 
  1604 
  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
  1618 
  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
  1624 
  1625 
  1626 subsection {* Core Procedure *}
  1627 
  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"
  1637 
  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"
  1647 
  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"]
  1689         by (simp add: mult.commute)
  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"]
  1704         by (simp add: mult.commute)
  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"]
  1737         by (simp add: mult.commute)
  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"]
  1752         by (simp add: mult.commute)
  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))"
  1768     by (simp add: polyneg_norm)
  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"]
  1786         by (simp add: mult.commute)
  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"]
  1800         by (simp add: mult.commute)
  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))"
  1816     by (simp add: polyneg_norm)
  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"]
  1833         by (simp add: mult.commute)
  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"]
  1849         by (simp add: mult.commute)
  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
  1860 
  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"]
  1902         by (simp add: mult.commute)
  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"]
  1917         by (simp add: mult.commute)
  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"]
  1947         by (simp add: mult.commute)
  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"]
  1962         by (simp add: mult.commute)
  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))"
  1978     by (simp add: polyneg_norm)
  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"]
  1995         by (simp add: mult.commute)
  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"]
  2010         by (simp add: mult.commute)
  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))"
  2026     by (simp add: polyneg_norm)
  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"]
  2043         by (simp add: mult.commute)
  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"]
  2058         by (simp add: mult.commute)
  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
  2068 
  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)
  2071 
  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)
  2074 
  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
  2093 
  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
  2112 
  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 = []"
  2122 
  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
  2127 
  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
  2151 
  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
  2169 
  2170 
  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
  2195 
  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
  2213 
  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"
  2252         by (simp add: field_simps)
  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"
  2281         by (simp add: field_simps)
  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"
  2330         by (simp add: field_simps)
  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"
  2353       by (simp add: field_simps)
  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"
  2359         by (simp add: field_simps)
  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"
  2403       by (simp add: field_simps)
  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"
  2433       by (simp add: field_simps)
  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"])
  2484 
  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
  2604 
  2605 (* The Ferrante - Rackoff Theorem *)
  2606 
  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
  2647 
  2648 
  2649 section {* First implementation : Naive by encoding all case splits locally *}
  2650 
  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)]"
  2658 
  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
  2673     by (simp add: msubsteq_def)
  2674 qed
  2675 
  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)"
  2748       by (simp add: field_simps)
  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
  2766 
  2767 
  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)]"
  2775 
  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
  2790     by (simp add: msubstneq_def)
  2791 qed
  2792 
  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)"
  2866       by (simp add: field_simps)
  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
  2884 
  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)]"
  2896 
  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
  2915     by (simp add: msubstlt_def)
  2916 qed
  2917 
  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)"
  2955       by (simp add: field_simps)
  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)"
  2980       by (simp add: field_simps)
  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"
  3000       by (simp add: zero_less_mult_iff)
  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)"
  3004       by (simp add: field_simps)
  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"
  3026       by (simp add: mult_less_0_iff)
  3027     from d have th: "(- ?t / ?c + - ?s / ?d)/2 = - ?t / (2 * ?c)"
  3028       by (simp add: field_simps)
  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"
  3049       by (simp add: zero_less_mult_iff)
  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)"
  3053       by (simp add: field_simps)
  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"
  3075       by (simp add: mult_less_0_iff)
  3076     from c have th: "(- ?t / ?c + - ?s / ?d)/2 = - ?s / (2*?d)"
  3077       by (simp add: field_simps)
  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
  3096 
  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)]"
  3108 
  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
  3127     by (simp add: msubstle_def)
  3128 qed
  3129 
  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)"
  3169       by (simp add: field_simps)
  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"
  3189       by (simp add: mult_less_0_iff field_simps add_neg_neg add_pos_pos)
  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)"
  3194       by (simp add: field_simps)
  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"
  3214       by (simp add: zero_less_mult_iff)
  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)"
  3218       by (simp add: field_simps)
  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"
  3240       by (simp add: mult_less_0_iff)
  3241     from d have th: "(- ?t / ?c + - ?s / ?d)/2 = - ?t / (2*?c)"
  3242       by (simp add: field_simps)
  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"
  3263       by (simp add: zero_less_mult_iff)
  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)"
  3267       by (simp add: field_simps)
  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"
  3289       by (simp add: mult_less_0_iff)
  3290     from c have th: "(- ?t / ?c + - ?s / ?d)/2 = - ?s / (2*?d)"
  3291       by (simp add: field_simps)
  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
  3310 
  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"
  3320 
  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)
  3329     (auto simp add: tmbound0_I
  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])
  3333 
  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)
  3341 
  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
  3380 
  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)
  3385 
  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 ))))"
  3396 
  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)))"
  3425       by (simp add: field_simps)
  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)"
  3459     by (simp add: evaldjf_ex)
  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
  3471 
  3472 definition "frpar p = simpfm (qelim p ferrack)"
  3473 
  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
  3482 
  3483 
  3484 section {* Second implemenation: Case splits not local *}
  3485 
  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"
  3520       by (simp add: field_simps)
  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
  3566 
  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)))"
  3572 
  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)
  3580 
  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)
  3588 
  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)
  3596 
  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]
  3603   by (simp add: msubstltneg_def field_simps del: minus_add_distrib)
  3604 
  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]
  3611   by (simp add: msubstleneg_def field_simps del: minus_add_distrib)
  3612 
  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"
  3622 
  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)
  3633 
  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"
  3643 
  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)
  3653 
  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)))"
  3659 
  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))"
  3668     by (simp_all add: polyneg_norm)
  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
  3684 
  3685 lemma msubsteq2_nb: "tmbound0 t \<Longrightarrow> islin (Eq (CNP 0 a r)) \<Longrightarrow> bound0 (msubsteq2 c t a r)"
  3686   by (simp add: msubsteq2_def)
  3687 
  3688 lemma msubstltpos_nb: "tmbound0 t \<Longrightarrow> islin (Lt (CNP 0 a r)) \<Longrightarrow> bound0 (msubstltpos c t a r)"
  3689   by (simp add: msubstltpos_def)
  3690 lemma msubstltneg_nb: "tmbound0 t \<Longrightarrow> islin (Lt (CNP 0 a r)) \<Longrightarrow> bound0 (msubstltneg c t a r)"
  3691   by (simp add: msubstltneg_def)
  3692 
  3693 lemma msubstlepos_nb: "tmbound0 t \<Longrightarrow> islin (Le (CNP 0 a r)) \<Longrightarrow> bound0 (msubstlepos c t a r)"
  3694   by (simp add: msubstlepos_def)
  3695 lemma msubstleneg_nb: "tmbound0 t \<Longrightarrow> islin (Le (CNP 0 a r)) \<Longrightarrow> bound0 (msubstleneg c t a r)"
  3696   by (simp add: msubstleneg_def)
  3697 
  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)
  3705 
  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)
  3714 
  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)
  3722 
  3723 lemma mult_minus2_left: "-2 * (x::'a::comm_ring_1) = - (2 * x)"
  3724   by simp
  3725 
  3726 lemma mult_minus2_right: "(x::'a::comm_ring_1) * -2 = - (x * 2)"
  3727   by simp
  3728 
  3729 lemma islin_qf: "islin p \<Longrightarrow> qfree p"
  3730   by (induct p rule: islin.induct) (auto simp add: bound0_qf)
  3731 
  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))"
  3748     by (simp add: isnpoly_def)
  3749   note eq0 = subst0[OF islin_qf[OF lp], of vs x bs "CP 0\<^sub>p", simplified]
  3750 
  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"
  3814         by (simp add: add_divide_distrib diff_divide_distrib mult_minus2_left mult.commute)
  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)))"
  3831         by (simp add: diff_divide_distrib add_divide_distrib mult_minus2_left mult.commute)
  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
  3838 
  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)]))"
  3858 
  3859 definition "frpar2 p = simpfm (qelim (prep p) ferrack2)"
  3860 
  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))"
  3926 
  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
  3950         by (simp add: field_simps)
  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
  3958         by (simp add: field_simps)
  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
  3963 
  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)))"
  3974     by (simp add: split_def)
  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")
  3984     apply (simp add: list_disj_def)
  3985     apply (cases "?pp = T")
  3986     apply (simp add: list_disj_def)
  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
  3992 
  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
  4002 
  4003 oracle frpar_oracle = {*
  4004 let
  4005 
  4006 fun binopT T = T --> T --> T;
  4007 fun relT T = T --> T --> @{typ bool};
  4008 
  4009 val mk_C = @{code C} o apply2 @{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};
  4012 
  4013 val dest_num = snd o HOLogic.dest_number;
  4014 
  4015 fun try_dest_num t = SOME ((snd o HOLogic.dest_number) t)
  4016   handle TERM _ => NONE;
  4017 
  4018 fun dest_nat (t as Const (@{const_name Suc}, _)) = HOLogic.dest_nat t
  4019   | dest_nat t = dest_num t;
  4020 
  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;
  4025 
  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));
  4042 
  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));
  4054 
  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";
  4082 
  4083 fun term_of_num T ps (@{code poly.C} (a, b)) =
  4084       let
  4085         val (c, d) = apply2 (@{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)));
  4107 
  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));
  4120 
  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";
  4146 
  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;
  4154 
  4155 in
  4156 
  4157   fn (ctxt, alternative, ty, ps, ct) =>
  4158     Thm.cterm_of ctxt
  4159       (frpar_procedure alternative ty ps (Thm.term_of ct))
  4160 
  4161 end
  4162 *}
  4163 
  4164 ML {*
  4165 structure Parametric_Ferrante_Rackoff =
  4166 struct
  4167 
  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);
  4174 
  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;
  4187 
  4188 end;
  4189 *}
  4190 
  4191 method_setup frpar = {*
  4192   Parametric_Ferrante_Rackoff.method false
  4193 *} "parametric QE for linear Arithmetic over fields"
  4194 
  4195 method_setup frpar2 = {*
  4196   Parametric_Ferrante_Rackoff.method true
  4197 *} "parametric QE for linear Arithmetic over fields, Version 2"
  4198 
  4199 lemma "\<exists>(x::'a::{linordered_field_inverse_zero}). y \<noteq> -1 \<longrightarrow> (y + 1) * x < 0"
  4200   apply (frpar type: 'a pars: y)
  4201   apply (simp add: field_simps)
  4202   apply (rule spec[where x=y])
  4203   apply (frpar type: 'a pars: "z::'a")
  4204   apply simp
  4205   done
  4206 
  4207 lemma "\<exists>(x::'a::{linordered_field_inverse_zero}). y \<noteq> -1 \<longrightarrow> (y + 1)*x < 0"
  4208   apply (frpar2 type: 'a pars: y)
  4209   apply (simp add: field_simps)
  4210   apply (rule spec[where x=y])
  4211   apply (frpar2 type: 'a pars: "z::'a")
  4212   apply simp
  4213   done
  4214 
  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")
  4220 by (simp add: field_simps)
  4221 have "?rhs"
  4222 
  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}")
  4224   apply (simp add: field_simps)
  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 *)
  4232 
  4233 text{* Collins/Jones Problem *}
  4234 
  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")
  4239 by (simp add: field_simps)
  4240 have "?rhs"
  4241   apply (frpar2 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}")
  4242   apply simp
  4243 oops
  4244 *)
  4245 
  4246 (*
  4247 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"
  4248 apply (frpar2 type: "'a::{linordered_field_inverse_zero, number_ring}" pars: "t::'a::{linordered_field_inverse_zero, number_ring}")
  4249 apply (simp add: field_simps linorder_neq_iff[symmetric])
  4250 apply ferrack
  4251 oops
  4252 *)
  4253 end