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