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