src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy

 (*  Title:      HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
     Author:     Amine Chaieb
 *)
 
-section\<open>A formalization of Ferrante and Rackoff's procedure with polynomial parameters, see Paper in CALCULEMUS 2008\<close>
+section \<open>A formalization of Ferrante and Rackoff's procedure with polynomial parameters, see Paper in CALCULEMUS 2008\<close>
 
 theory Parametric_Ferrante_Rackoff
 imports
   Reflected_Multivariate_Polynomial
   Dense_Linear_Order

 subsection \<open>Terms\<close>
 
 datatype tm = CP poly | Bound nat | Add tm tm | Mul poly tm
   | Neg tm | Sub tm tm | CNP nat poly tm
 
-(* A size for poly to make inductive proofs simpler*)
+text \<open>A size for poly to make inductive proofs simpler.\<close>
 primrec tmsize :: "tm \<Rightarrow> nat"
 where
   "tmsize (CP c) = polysize c"
 | "tmsize (Bound n) = 1"
 | "tmsize (Neg a) = 1 + tmsize a"
 | "tmsize (Add a b) = 1 + tmsize a + tmsize b"
 | "tmsize (Sub a b) = 3 + tmsize a + tmsize b"
 | "tmsize (Mul c a) = 1 + polysize c + tmsize a"
 | "tmsize (CNP n c a) = 3 + polysize c + tmsize a "
 
-(* Semantics of terms tm *)
-primrec Itm :: "'a::{field_char_0, field} list \<Rightarrow> 'a list \<Rightarrow> tm \<Rightarrow> 'a"
+text \<open>Semantics of terms tm.\<close>
+primrec Itm :: "'a::{field_char_0,field} list \<Rightarrow> 'a list \<Rightarrow> tm \<Rightarrow> 'a"
 where
   "Itm vs bs (CP c) = (Ipoly vs c)"
 | "Itm vs bs (Bound n) = bs!n"
 | "Itm vs bs (Neg a) = -(Itm vs bs a)"
 | "Itm vs bs (Add a b) = Itm vs bs a + Itm vs bs b"

 | "tmboundslt n (Neg a) = tmboundslt n a"
 | "tmboundslt n (Add a b) = (tmboundslt n a \<and> tmboundslt n b)"
 | "tmboundslt n (Sub a b) = (tmboundslt n a \<and> tmboundslt n b)"
 | "tmboundslt n (Mul i a) = tmboundslt n a"
 
-primrec tmbound0 :: "tm \<Rightarrow> bool" (* a tm is INDEPENDENT of Bound 0 *)
+primrec tmbound0 :: "tm \<Rightarrow> bool"  -- \<open>a tm is INDEPENDENT of Bound 0\<close>
 where
   "tmbound0 (CP c) = True"
 | "tmbound0 (Bound n) = (n>0)"
 | "tmbound0 (CNP n c a) = (n\<noteq>0 \<and> tmbound0 a)"
 | "tmbound0 (Neg a) = tmbound0 a"

 
 lemma tmbound0_I:
   assumes nb: "tmbound0 a"
   shows "Itm vs (b#bs) a = Itm vs (b'#bs) a"
   using nb
-  by (induct a rule: tm.induct,auto)
-
-primrec tmbound :: "nat \<Rightarrow> tm \<Rightarrow> bool" (* a tm is INDEPENDENT of Bound n *)
+  by (induct a rule: tm.induct) auto
+
+primrec tmbound :: "nat \<Rightarrow> tm \<Rightarrow> bool"  -- \<open>a tm is INDEPENDENT of Bound n\<close>
 where
   "tmbound n (CP c) = True"
 | "tmbound n (Bound m) = (n \<noteq> m)"
 | "tmbound n (CNP m c a) = (n\<noteq>m \<and> tmbound n a)"
 | "tmbound n (Neg a) = tmbound n a"

   by (induct xs arbitrary: n) auto
 
 lemma nth_length_exceeds: "n \<ge> length xs \<Longrightarrow> xs!n = []!(n - length xs)"
   by (induct xs arbitrary: n) auto
 
-lemma removen_length:
-  "length (removen n xs) = (if n \<ge> length xs then length xs else length xs - 1)"
+lemma removen_length: "length (removen n xs) = (if n \<ge> length xs then length xs else length xs - 1)"
   by (induct xs arbitrary: n, auto)
 
 lemma removen_nth:
   "(removen n xs)!m =
     (if n \<ge> length xs then xs!m

      else []!(m - (length xs - 1)))"
 proof (induct xs arbitrary: n m)
   case Nil
   then show ?case by simp
 next
-  case (Cons x xs n m)
-  {
-    assume nxs: "n \<ge> length (x#xs)"
-    then have ?case using removen_same[OF nxs] by simp
-  }
-  moreover
-  {
-    assume nxs: "\<not> (n \<ge> length (x#xs))"
-    {
-      assume mln: "m < n"
-      then have ?case using Cons by (cases m) auto
-    }
-    moreover
-    {
-      assume mln: "\<not> (m < n)"
-      {
-        assume mxs: "m \<le> length (x#xs)"
-        then have ?case using Cons by (cases m) auto
-      }
-      moreover
-      {
-        assume mxs: "\<not> (m \<le> length (x#xs))"
-        have th: "length (removen n (x#xs)) = length xs"
-          using removen_length[where n="n" and xs="x#xs"] nxs by simp
-        with mxs have mxs':"m \<ge> length (removen n (x#xs))"
+  case (Cons x xs)
+  let ?l = "length (x # xs)"
+  consider "n \<ge> ?l" | "n < ?l" by arith
+  then show ?case
+  proof cases
+    case 1 
+    then show ?thesis
+      using removen_same[OF 1] by simp
+  next
+    case 2
+    consider "m < n" | "m \<ge> n" by arith
+    then show ?thesis
+    proof cases
+      case 1
+      then show ?thesis
+        using Cons by (cases m) auto
+    next
+      case 2
+      consider "m \<le> ?l" | "m > ?l" by arith
+      then show ?thesis
+      proof cases
+        case 1
+        then show ?thesis
+          using Cons by (cases m) auto
+      next
+        case 2
+        have th: "length (removen n (x # xs)) = length xs"
+          using removen_length[where n = n and xs= "x # xs"] \<open>n < ?l\<close> by simp
+        with \<open>m > ?l\<close> have "m \<ge> length (removen n (x # xs))"
           by auto
-        then have "(removen n (x#xs))!m = [] ! (m - length xs)"
-          using th nth_length_exceeds[OF mxs'] by auto
-        then have th: "(removen n (x#xs))!m = [] ! (m - (length (x#xs) - 1))"
+        from th nth_length_exceeds[OF this] have "(removen n (x # xs))!m = [] ! (m - length xs)"
+           by auto
+        then have "(removen n (x # xs))!m = [] ! (m - (length (x # xs) - 1))"
           by auto
-        then have ?case
-          using nxs mln mxs by auto
-      }
-      ultimately have ?case by blast
-    }
-    ultimately have ?case by blast
-  }
-  ultimately show ?case by blast
+        then show ?thesis
+          using \<open>n < ?l\<close> \<open>m > ?l\<close> \<open>m > ?l\<close> by auto
+      qed
+    qed
+  qed
 qed
 
 lemma decrtm:
   assumes bnd: "tmboundslt (length bs) t"
     and nb: "tmbound m t"

 | "tmsubst0 t (Neg a) = Neg (tmsubst0 t a)"
 | "tmsubst0 t (Add a b) = Add (tmsubst0 t a) (tmsubst0 t b)"
 | "tmsubst0 t (Sub a b) = Sub (tmsubst0 t a) (tmsubst0 t b)"
 | "tmsubst0 t (Mul i a) = Mul i (tmsubst0 t a)"
 
-lemma tmsubst0: "Itm vs (x#bs) (tmsubst0 t a) = Itm vs ((Itm vs (x#bs) t)#bs) a"
+lemma tmsubst0: "Itm vs (x # bs) (tmsubst0 t a) = Itm vs (Itm vs (x # bs) t # bs) a"
   by (induct a rule: tm.induct) auto
 
 lemma tmsubst0_nb: "tmbound0 t \<Longrightarrow> tmbound0 (tmsubst0 t a)"
   by (induct a rule: tm.induct) auto
 

   by (induct a rule: tm.induct) auto
 
 lemma incrtm0_tmbound: "tmbound n t \<Longrightarrow> tmbound (Suc n) (incrtm0 t)"
   by (induct t) auto
 
-(* Simplification *)
+
+text \<open>Simplification.\<close>
 
 consts tmadd:: "tm \<times> tm \<Rightarrow> tm"
 recdef tmadd "measure (\<lambda>(t,s). size t + size s)"
   "tmadd (CNP n1 c1 r1,CNP n2 c2 r2) =
     (if n1 = n2 then

   "tmadd (t, CNP n2 c2 r2) = CNP n2 c2 (tmadd (t, r2))"
   "tmadd (CP b1, CP b2) = CP (b1 +\<^sub>p b2)"
   "tmadd (a, b) = Add a b"
 
 lemma tmadd[simp]: "Itm vs bs (tmadd (t, s)) = Itm vs bs (Add t s)"
-  apply (induct t s rule: tmadd.induct, simp_all add: Let_def)
-  apply (case_tac "c1 +\<^sub>p c2 = 0\<^sub>p",case_tac "n1 \<le> n2", simp_all)
-  apply (case_tac "n1 = n2", simp_all add: field_simps)
+  apply (induct t s rule: tmadd.induct)
+  apply (simp_all add: Let_def)
+  apply (case_tac "c1 +\<^sub>p c2 = 0\<^sub>p")
+  apply (case_tac "n1 \<le> n2")
+  apply simp_all
+  apply (case_tac "n1 = n2")
+  apply (simp_all add: field_simps)
   apply (simp only: distrib_left[symmetric])
   apply (auto simp del: polyadd simp add: polyadd[symmetric])
   done
 
 lemma tmadd_nb0[simp]: "tmbound0 t \<Longrightarrow> tmbound0 s \<Longrightarrow> tmbound0 (tmadd (t, s))"

 
 lemma tmmul_blt[simp]: "tmboundslt n t \<Longrightarrow> tmboundslt n (tmmul t i)"
   by (induct t arbitrary: i rule: tmmul.induct) (auto simp add: Let_def)
 
 lemma tmmul_allpolys_npoly[simp]:
-  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
+  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   shows "allpolys isnpoly t \<Longrightarrow> isnpoly c \<Longrightarrow> allpolys isnpoly (tmmul t c)"
   by (induct t rule: tmmul.induct) (simp_all add: Let_def polymul_norm)
 
 definition tmneg :: "tm \<Rightarrow> tm"
   where "tmneg t \<equiv> tmmul t (C (- 1,1))"

 
 lemma [simp]: "isnpoly (C (-1, 1))"
   unfolding isnpoly_def by simp
 
 lemma tmneg_allpolys_npoly[simp]:
-  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
+  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   shows "allpolys isnpoly t \<Longrightarrow> allpolys isnpoly (tmneg t)"
   unfolding tmneg_def by auto
 
 lemma tmsub[simp]: "Itm vs bs (tmsub a b) = Itm vs bs (Sub a b)"
   using tmsub_def by simp

 
 lemma tmsub_blt[simp]: "tmboundslt n t \<Longrightarrow> tmboundslt n s \<Longrightarrow> tmboundslt n (tmsub t s)"
   using tmsub_def by simp
 
 lemma tmsub_allpolys_npoly[simp]:
-  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
+  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   shows "allpolys isnpoly t \<Longrightarrow> allpolys isnpoly s \<Longrightarrow> allpolys isnpoly (tmsub t s)"
   unfolding tmsub_def by (simp add: isnpoly_def)
 
 fun simptm :: "tm \<Rightarrow> tm"
 where

     (let i' = polynate i in if i' = 0\<^sub>p then CP 0\<^sub>p else tmmul (simptm t) i')"
 | "simptm (CNP n c t) =
     (let c' = polynate c in if c' = 0\<^sub>p then simptm t else tmadd (CNP n c' (CP 0\<^sub>p ), simptm t))"
 
 lemma polynate_stupid:
-  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
+  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   shows "polynate t = 0\<^sub>p \<Longrightarrow> Ipoly bs t = (0::'a)"
   apply (subst polynate[symmetric])
   apply simp
   done
 

 
 lemma simptm_nlt[simp]: "tmboundslt n t \<Longrightarrow> tmboundslt n (simptm t)"
   by (induct t rule: simptm.induct) (auto simp add: Let_def)
 
 lemma [simp]: "isnpoly 0\<^sub>p"
-  and [simp]: "isnpoly (C(1,1))"
+  and [simp]: "isnpoly (C (1, 1))"
   by (simp_all add: isnpoly_def)
 
 lemma simptm_allpolys_npoly[simp]:
-  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
+  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   shows "allpolys isnpoly (simptm p)"
   by (induct p rule: simptm.induct) (auto simp add: Let_def)
 
 declare let_cong[fundef_cong del]
 
-fun split0 :: "tm \<Rightarrow> (poly \<times> tm)"
+fun split0 :: "tm \<Rightarrow> poly \<times> tm"
 where
   "split0 (Bound 0) = ((1)\<^sub>p, CP 0\<^sub>p)"
 | "split0 (CNP 0 c t) = (let (c', t') = split0 t in (c +\<^sub>p c', t'))"
 | "split0 (Neg t) = (let (c, t') = split0 t in (~\<^sub>p c, Neg t'))"
 | "split0 (CNP n c t) = (let (c', t') = split0 t in (c', CNP n c t'))"

   apply (rule exI[where x="snd (split0 p)"])
   apply simp
   done
 
 lemma split0:
-  "tmbound 0 (snd (split0 t)) \<and> (Itm vs bs (CNP 0 (fst (split0 t)) (snd (split0 t))) = Itm vs bs t)"
+  "tmbound 0 (snd (split0 t)) \<and> Itm vs bs (CNP 0 (fst (split0 t)) (snd (split0 t))) = Itm vs bs t"
   apply (induct t rule: split0.induct)
   apply simp
   apply (simp add: Let_def split_def field_simps)
   apply (simp add: Let_def split_def field_simps)
   apply (simp add: Let_def split_def field_simps)

   show "Itm vs bs t = Itm vs bs (CNP 0 c' t')"
     by simp
 qed
 
 lemma split0_nb0:
-  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
+  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   shows "split0 t = (c',t') \<Longrightarrow>  tmbound 0 t'"
 proof -
   fix c' t'
   assume "split0 t = (c', t')"
   then have "c' = fst (split0 t)" and "t' = snd (split0 t)"

   with conjunct1[OF split0[where t="t"]] show "tmbound 0 t'"
     by simp
 qed
 
 lemma split0_nb0'[simp]:
-  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
+  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   shows "tmbound0 (snd (split0 t))"
   using split0_nb0[of t "fst (split0 t)" "snd (split0 t)"]
   by (simp add: tmbound0_tmbound_iff)
 
 lemma split0_nb:

 
 lemma allpolys_split0: "allpolys isnpoly p \<Longrightarrow> allpolys isnpoly (snd (split0 p))"
   by (induct p rule: split0.induct) (auto simp  add: isnpoly_def Let_def split_def)
 
 lemma isnpoly_fst_split0:
-  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
+  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   shows "allpolys isnpoly p \<Longrightarrow> isnpoly (fst (split0 p))"
   by (induct p rule: split0.induct)
     (auto simp  add: polyadd_norm polysub_norm polyneg_norm polymul_norm Let_def split_def)
 
 
-subsection\<open>Formulae\<close>
+subsection \<open>Formulae\<close>
 
 datatype fm  =  T| F| Le tm | Lt tm | Eq tm | NEq tm|
   NOT fm| And fm fm|  Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm
 
 

 (* several lemmas about fmsize *)
 lemma fmsize_pos[termination_simp]: "fmsize p > 0"
   by (induct p rule: fmsize.induct) simp_all
 
   (* Semantics of formulae (fm) *)
-primrec Ifm ::"'a::{linordered_field} list \<Rightarrow> 'a list \<Rightarrow> fm \<Rightarrow> bool"
+primrec Ifm ::"'a::linordered_field list \<Rightarrow> 'a list \<Rightarrow> fm \<Rightarrow> bool"
 where
   "Ifm vs bs T = True"
 | "Ifm vs bs F = False"
 | "Ifm vs bs (Lt a) = (Itm vs bs a < 0)"
 | "Ifm vs bs (Le a) = (Itm vs bs a \<le> 0)"

     and nle: "m < length bs"
   shows "Ifm vs (removen m bs) (decr m p) = Ifm vs bs p"
   using bnd nb nle
 proof (induct p arbitrary: bs m rule: fm.induct)
   case (E p bs m)
-  { fix x
+  have "Ifm vs (removen (Suc m) (x#bs)) (decr (Suc m) p) = Ifm vs (x#bs) p" for x
+  proof -
     from E
     have bnd: "boundslt (length (x#bs)) p"
       and nb: "bound (Suc m) p"
       and nle: "Suc m < length (x#bs)"
       by auto
-    from E(1)[OF bnd nb nle]
-    have "Ifm vs (removen (Suc m) (x#bs)) (decr (Suc m) p) = Ifm vs (x#bs) p" .
-  }
+    from E(1)[OF bnd nb nle] show ?thesis .
+  qed
   then show ?case by auto
 next
   case (A p bs m)
-  { fix x
+  have "Ifm vs (removen (Suc m) (x#bs)) (decr (Suc m) p) = Ifm vs (x#bs) p" for x
+  proof -
     from A
     have bnd: "boundslt (length (x#bs)) p"
       and nb: "bound (Suc m) p"
       and nle: "Suc m < length (x#bs)"
       by auto
-    from A(1)[OF bnd nb nle]
-    have "Ifm vs (removen (Suc m) (x#bs)) (decr (Suc m) p) = Ifm vs (x#bs) p" .
-  }
+    from A(1)[OF bnd nb nle] show ?thesis .
+  qed
   then show ?case by auto
 qed (auto simp add: decrtm removen_nth)
 
 primrec subst0 :: "tm \<Rightarrow> fm \<Rightarrow> fm"
 where

     and nlm: "n \<le> length bs"
   shows "Ifm vs bs (subst n t p) = Ifm vs (bs[n:= Itm vs bs t]) p"
   using nb nlm
 proof (induct p arbitrary: bs n t rule: fm.induct)
   case (E p bs n)
-  {
-    fix x
+  have "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) =
+        Ifm vs (x#bs[n:= Itm vs bs t]) p" for x
+  proof -
     from E have bn: "boundslt (length (x#bs)) p"
       by simp
     from E have nlm: "Suc n \<le> length (x#bs)"
       by simp
     from E(1)[OF bn nlm]
     have "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) =
         Ifm vs ((x#bs)[Suc n:= Itm vs (x#bs) (incrtm0 t)]) p"
       by simp
-    then have "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) =
-        Ifm vs (x#bs[n:= Itm vs bs t]) p"
+    then show ?thesis
       by (simp add: incrtm0[where x="x" and bs="bs" and t="t"])
-  }
+  qed
   then show ?case by simp
 next
   case (A p bs n)
-  {
-    fix x
+  have "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) =
+        Ifm vs (x#bs[n:= Itm vs bs t]) p" for x
+  proof -
     from A have bn: "boundslt (length (x#bs)) p"
       by simp
     from A have nlm: "Suc n \<le> length (x#bs)"
       by simp
     from A(1)[OF bn nlm]
     have "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) =
         Ifm vs ((x#bs)[Suc n:= Itm vs (x#bs) (incrtm0 t)]) p"
       by simp
-    then have "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) =
-        Ifm vs (x#bs[n:= Itm vs bs t]) p"
+    then show ?thesis
       by (simp add: incrtm0[where x="x" and bs="bs" and t="t"])
-  }
+  qed
   then show ?case by simp
 qed (auto simp add: tmsubst)
 
 lemma subst_nb:
   assumes tnb: "tmbound m t"

 lemma iff_blt[simp]: "boundslt n p \<Longrightarrow> boundslt n q \<Longrightarrow> boundslt n (iff p q)"
   using iff_def by auto
 lemma decr0_qf: "bound0 p \<Longrightarrow> qfree (decr0 p)"
   by (induct p) simp_all
 
-fun isatom :: "fm \<Rightarrow> bool" (* test for atomicity *)
+fun isatom :: "fm \<Rightarrow> bool"  -- \<open>test for atomicity\<close>
 where
   "isatom T = True"
 | "isatom F = True"
 | "isatom (Lt a) = True"
 | "isatom (Le a) = True"

 
 definition evaldjf :: "('a \<Rightarrow> fm) \<Rightarrow> 'a list \<Rightarrow> fm"
   where "evaldjf f ps \<equiv> foldr (djf f) ps F"
 
 lemma djf_Or: "Ifm vs bs (djf f p q) = Ifm vs bs (Or (f p) q)"
-  by (cases "q=T", simp add: djf_def,cases "q=F", simp add: djf_def)
-    (cases "f p", simp_all add: Let_def djf_def)
+  apply (cases "q = T")
+  apply (simp add: djf_def)
+  apply (cases "q = F")
+  apply (simp add: djf_def)
+  apply (cases "f p")
+  apply (simp_all add: Let_def djf_def)
+  done
 
 lemma evaldjf_ex: "Ifm vs bs (evaldjf f ps) \<longleftrightarrow> (\<exists>p \<in> set ps. Ifm vs bs (f p))"
   by (induct ps) (simp_all add: evaldjf_def djf_Or)
 
 lemma evaldjf_bound0:
   assumes nb: "\<forall>x\<in> set xs. bound0 (f x)"
   shows "bound0 (evaldjf f xs)"
-  using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto)
+  using nb
+  apply (induct xs)
+  apply (auto simp add: evaldjf_def djf_def Let_def)
+  apply (case_tac "f a")
+  apply auto
+  done
 
 lemma evaldjf_qf:
   assumes nb: "\<forall>x\<in> set xs. qfree (f x)"
   shows "qfree (evaldjf f xs)"
-  using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto)
+  using nb
+  apply (induct xs)
+  apply (auto simp add: evaldjf_def djf_def Let_def)
+  apply (case_tac "f a")
+  apply auto
+  done
 
 fun disjuncts :: "fm \<Rightarrow> fm list"
 where
   "disjuncts (Or p q) = disjuncts p @ disjuncts q"
 | "disjuncts F = []"

     by (induct p rule:disjuncts.induct) auto
   then show ?thesis
     by (simp only: list_all_iff)
 qed
 
-lemma disjuncts_qf: "qfree p \<Longrightarrow> \<forall>q\<in> set (disjuncts p). qfree q"
-proof-
+lemma disjuncts_qf: "qfree p \<Longrightarrow> \<forall>q \<in> set (disjuncts p). qfree q"
+proof -
   assume qf: "qfree p"
   then have "list_all qfree (disjuncts p)"
     by (induct p rule: disjuncts.induct) auto
   then show ?thesis by (simp only: list_all_iff)
 qed

   "CJNB f p \<equiv>
     (let cjs = conjuncts p;
       (yes, no) = partition bound0 cjs
      in conj (decr0 (list_conj yes)) (f (list_conj no)))"
 
-lemma conjuncts_qf: "qfree p \<Longrightarrow> \<forall>q\<in> set (conjuncts p). qfree q"
+lemma conjuncts_qf: "qfree p \<Longrightarrow> \<forall>q \<in> set (conjuncts p). qfree q"
 proof -
   assume qf: "qfree p"
   then have "list_all qfree (conjuncts p)"
     by (induct p rule: conjuncts.induct) auto
   then show ?thesis

 definition "simple t = (let (c,s) = split0 (simptm t) in if c= 0\<^sub>p then le s else Le (CNP 0 c s))"
 definition "simpeq t = (let (c,s) = split0 (simptm t) in if c= 0\<^sub>p then eq s else Eq (CNP 0 c s))"
 definition "simpneq t = (let (c,s) = split0 (simptm t) in if c= 0\<^sub>p then neq s else NEq (CNP 0 c s))"
 
 lemma simplt_islin[simp]:
-  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
+  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   shows "islin (simplt t)"
   unfolding simplt_def
   using split0_nb0'
   by (auto simp add: lt_lin Let_def split_def isnpoly_fst_split0[OF simptm_allpolys_npoly]
       islin_stupid allpolys_split0[OF simptm_allpolys_npoly])
 
 lemma simple_islin[simp]:
-  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
+  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   shows "islin (simple t)"
   unfolding simple_def
   using split0_nb0'
   by (auto simp add: Let_def split_def isnpoly_fst_split0[OF simptm_allpolys_npoly]
       islin_stupid allpolys_split0[OF simptm_allpolys_npoly] le_lin)
 
 lemma simpeq_islin[simp]:
-  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
+  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   shows "islin (simpeq t)"
   unfolding simpeq_def
   using split0_nb0'
   by (auto simp add: Let_def split_def isnpoly_fst_split0[OF simptm_allpolys_npoly]
       islin_stupid allpolys_split0[OF simptm_allpolys_npoly] eq_lin)
 
 lemma simpneq_islin[simp]:
-  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
+  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   shows "islin (simpneq t)"
   unfolding simpneq_def
   using split0_nb0'
   by (auto simp add: Let_def split_def isnpoly_fst_split0[OF simptm_allpolys_npoly]
       islin_stupid allpolys_split0[OF simptm_allpolys_npoly] neq_lin)
 
 lemma really_stupid: "\<not> (\<forall>c1 s'. (c1, s') \<noteq> split0 s)"
   by (cases "split0 s") auto
 
 lemma split0_npoly:
-  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
+  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
     and n: "allpolys isnpoly t"
   shows "isnpoly (fst (split0 t))"
     and "allpolys isnpoly (snd (split0 t))"
   using n
   by (induct t rule: split0.induct)

 lemma simplt[simp]: "Ifm vs bs (simplt t) = Ifm vs bs (Lt t)"
 proof -
   have n: "allpolys isnpoly (simptm t)"
     by simp
   let ?t = "simptm t"
-  {
-    assume "fst (split0 ?t) = 0\<^sub>p"
-    then have ?thesis
+  show ?thesis
+  proof (cases "fst (split0 ?t) = 0\<^sub>p")
+    case True
+    then show ?thesis
       using split0[of "simptm t" vs bs] lt[OF split0_npoly(2)[OF n], of vs bs]
       by (simp add: simplt_def Let_def split_def lt)
-  }
-  moreover
-  {
-    assume "fst (split0 ?t) \<noteq> 0\<^sub>p"
-    then have ?thesis
-      using  split0[of "simptm t" vs bs]
+  next
+    case False
+    then show ?thesis
+      using split0[of "simptm t" vs bs]
       by (simp add: simplt_def Let_def split_def)
-  }
-  ultimately show ?thesis by blast
+  qed
 qed
 
 lemma simple[simp]: "Ifm vs bs (simple t) = Ifm vs bs (Le t)"
 proof -
   have n: "allpolys isnpoly (simptm t)"
     by simp
   let ?t = "simptm t"
-  {
-    assume "fst (split0 ?t) = 0\<^sub>p"
-    then have ?thesis
+  show ?thesis
+  proof (cases "fst (split0 ?t) = 0\<^sub>p")
+    case True
+    then show ?thesis
       using split0[of "simptm t" vs bs] le[OF split0_npoly(2)[OF n], of vs bs]
       by (simp add: simple_def Let_def split_def le)
-  }
-  moreover
-  {
-    assume "fst (split0 ?t) \<noteq> 0\<^sub>p"
-    then have ?thesis
+  next
+    case False
+    then show ?thesis
       using split0[of "simptm t" vs bs]
       by (simp add: simple_def Let_def split_def)
-  }
-  ultimately show ?thesis by blast
+  qed
 qed
 
 lemma simpeq[simp]: "Ifm vs bs (simpeq t) = Ifm vs bs (Eq t)"
 proof -
   have n: "allpolys isnpoly (simptm t)"
     by simp
   let ?t = "simptm t"
-  {
-    assume "fst (split0 ?t) = 0\<^sub>p"
-    then have ?thesis
+  show ?thesis
+  proof (cases "fst (split0 ?t) = 0\<^sub>p")
+    case True
+    then show ?thesis
       using split0[of "simptm t" vs bs] eq[OF split0_npoly(2)[OF n], of vs bs]
       by (simp add: simpeq_def Let_def split_def)
-  }
-  moreover
-  {
-    assume "fst (split0 ?t) \<noteq> 0\<^sub>p"
-    then have ?thesis using  split0[of "simptm t" vs bs]
+  next
+    case False
+    then show ?thesis using  split0[of "simptm t" vs bs]
       by (simp add: simpeq_def Let_def split_def)
-  }
-  ultimately show ?thesis by blast
+  qed
 qed
 
 lemma simpneq[simp]: "Ifm vs bs (simpneq t) = Ifm vs bs (NEq t)"
 proof -
   have n: "allpolys isnpoly (simptm t)"
     by simp
   let ?t = "simptm t"
-  {
-    assume "fst (split0 ?t) = 0\<^sub>p"
-    then have ?thesis
+  show ?thesis
+  proof (cases "fst (split0 ?t) = 0\<^sub>p")
+    case True
+    then show ?thesis
       using split0[of "simptm t" vs bs] neq[OF split0_npoly(2)[OF n], of vs bs]
       by (simp add: simpneq_def Let_def split_def)
-  }
-  moreover
-  {
-    assume "fst (split0 ?t) \<noteq> 0\<^sub>p"
-    then have ?thesis
+  next
+    case False
+    then show ?thesis
       using split0[of "simptm t" vs bs] by (simp add: simpneq_def Let_def split_def)
-  }
-  ultimately show ?thesis by blast
+  qed
 qed
 
 lemma lt_nb: "tmbound0 t \<Longrightarrow> bound0 (lt t)"
   apply (simp add: lt_def)
   apply (cases t)

   apply (rename_tac poly, case_tac poly)
   apply auto
   done
 
 lemma simplt_nb[simp]:
-  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
+  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   shows "tmbound0 t \<Longrightarrow> bound0 (simplt t)"
 proof (simp add: simplt_def Let_def split_def)
   assume nb: "tmbound0 t"
   then have nb': "tmbound0 (simptm t)"
     by simp

       fst (split0 (simptm t)) = 0\<^sub>p"
     by (simp add: simplt_def Let_def split_def lt_nb)
 qed
 
 lemma simple_nb[simp]:
-  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
+  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   shows "tmbound0 t \<Longrightarrow> bound0 (simple t)"
 proof(simp add: simple_def Let_def split_def)
   assume nb: "tmbound0 t"
   then have nb': "tmbound0 (simptm t)"
     by simp

       fst (split0 (simptm t)) = 0\<^sub>p"
     by (simp add: simplt_def Let_def split_def le_nb)
 qed
 
 lemma simpeq_nb[simp]:
-  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
+  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   shows "tmbound0 t \<Longrightarrow> bound0 (simpeq t)"
 proof (simp add: simpeq_def Let_def split_def)
   assume nb: "tmbound0 t"
   then have nb': "tmbound0 (simptm t)"
     by simp

       fst (split0 (simptm t)) = 0\<^sub>p"
     by (simp add: simpeq_def Let_def split_def eq_nb)
 qed
 
 lemma simpneq_nb[simp]:
-  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
+  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   shows "tmbound0 t \<Longrightarrow> bound0 (simpneq t)"
 proof (simp add: simpneq_def Let_def split_def)
   assume nb: "tmbound0 t"
   then have nb': "tmbound0 (simptm t)"
     by simp

   with qe have cno_qf:"qfree (qe ?cno)"
     and noE: "Ifm vs bs (qe ?cno) = Ifm vs bs (E ?cno)"
     by blast+
   from cno_qf yes_qf have qf: "qfree (CJNB qe p)"
     by (simp add: CJNB_def Let_def split_def)
-  {
-    fix bs
+  have "Ifm vs bs p = ((Ifm vs bs ?cyes) \<and> (Ifm vs bs ?cno))" for bs
+  proof -
     from conjuncts have "Ifm vs bs p = (\<forall>q\<in> set ?cjs. Ifm vs bs q)"
       by blast
     also have "\<dots> = ((\<forall>q\<in> set ?yes. Ifm vs bs q) \<and> (\<forall>q\<in> set ?no. Ifm vs bs q))"
       using partition_set[OF part] by auto
-    finally have "Ifm vs bs p = ((Ifm vs bs ?cyes) \<and> (Ifm vs bs ?cno))"
+    finally show ?thesis
       using list_conj[of vs bs] by simp
-  }
+  qed
   then have "Ifm vs bs (E p) = (\<exists>x. (Ifm vs (x#bs) ?cyes) \<and> (Ifm vs (x#bs) ?cno))"
     by simp
   also fix y have "\<dots> = (\<exists>x. (Ifm vs (y#bs) ?cyes) \<and> (Ifm vs (x#bs) ?cno))"
     using bound0_I[OF yes_nb, where bs="bs" and b'="y"] by blast
   also have "\<dots> = (Ifm vs bs (decr0 ?cyes) \<and> Ifm vs bs (E ?cno))"

 
 lemma simpfm[simp]: "Ifm vs bs (simpfm p) = Ifm vs bs p"
   by (induct p arbitrary: bs rule: simpfm.induct) auto
 
 lemma simpfm_bound0:
-  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
+  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   shows "bound0 p \<Longrightarrow> bound0 (simpfm p)"
   by (induct p rule: simpfm.induct) auto
 
 lemma lt_qf[simp]: "qfree (lt t)"
   apply (cases t)

   apply (auto simp add: eq_def)
   apply (rename_tac poly, case_tac poly)
   apply auto
   done
 
-lemma neq_qf[simp]: "qfree (neq t)" by (simp add: neq_def)
-
-lemma simplt_qf[simp]: "qfree (simplt t)" by (simp add: simplt_def Let_def split_def)
-lemma simple_qf[simp]: "qfree (simple t)" by (simp add: simple_def Let_def split_def)
-lemma simpeq_qf[simp]: "qfree (simpeq t)" by (simp add: simpeq_def Let_def split_def)
-lemma simpneq_qf[simp]: "qfree (simpneq t)" by (simp add: simpneq_def Let_def split_def)
+lemma neq_qf[simp]: "qfree (neq t)"
+  by (simp add: neq_def)
+
+lemma simplt_qf[simp]: "qfree (simplt t)"
+  by (simp add: simplt_def Let_def split_def)
+
+lemma simple_qf[simp]: "qfree (simple t)"
+  by (simp add: simple_def Let_def split_def)
+
+lemma simpeq_qf[simp]: "qfree (simpeq t)"
+  by (simp add: simpeq_def Let_def split_def)
+
+lemma simpneq_qf[simp]: "qfree (simpneq t)"
+  by (simp add: simpneq_def Let_def split_def)
 
 lemma simpfm_qf[simp]: "qfree p \<Longrightarrow> qfree (simpfm p)"
   by (induct p rule: simpfm.induct) auto
 
 lemma disj_lin: "islin p \<Longrightarrow> islin q \<Longrightarrow> islin (disj p q)"
   by (simp add: disj_def)
 lemma conj_lin: "islin p \<Longrightarrow> islin q \<Longrightarrow> islin (conj p q)"
   by (simp add: conj_def)
 
 lemma
-  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
+  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   shows "qfree p \<Longrightarrow> islin (simpfm p)"
   by (induct p rule: simpfm.induct) (simp_all add: conj_lin disj_lin)
 
 consts prep :: "fm \<Rightarrow> fm"
 recdef prep "measure fmsize"

   "prep (Or p q) = disj (prep p) (prep q)"
   "prep (And p q) = conj (prep p) (prep q)"
   "prep (Imp p q) = prep (Or (NOT p) q)"
   "prep (Iff p q) = disj (prep (And p q)) (prep (And (NOT p) (NOT q)))"
   "prep p = p"
-(hints simp add: fmsize_pos)
+  (hints simp add: fmsize_pos)
 
 lemma prep: "Ifm vs bs (prep p) = Ifm vs bs p"
   by (induct p arbitrary: bs rule: prep.induct) auto
 
 
-(* Generic quantifier elimination *)
+text \<open>Generic quantifier elimination.\<close>
 function (sequential) qelim :: "fm \<Rightarrow> (fm \<Rightarrow> fm) \<Rightarrow> fm"
 where
   "qelim (E p) = (\<lambda>qe. DJ (CJNB qe) (qelim p qe))"
 | "qelim (A p) = (\<lambda>qe. not (qe ((qelim (NOT p) qe))))"
 | "qelim (NOT p) = (\<lambda>qe. not (qelim p qe))"
 | "qelim (And p q) = (\<lambda>qe. conj (qelim p qe) (qelim q qe))"
 | "qelim (Or  p q) = (\<lambda>qe. disj (qelim p qe) (qelim q qe))"
 | "qelim (Imp p q) = (\<lambda>qe. imp (qelim p qe) (qelim q qe))"
 | "qelim (Iff p q) = (\<lambda>qe. iff (qelim p qe) (qelim q qe))"
 | "qelim p = (\<lambda>y. simpfm p)"
-by pat_completeness simp_all
+  by pat_completeness simp_all
 termination by (relation "measure fmsize") auto
 
 lemma qelim:
   assumes qe_inv: "\<forall>bs p. qfree p \<longrightarrow> qfree (qe p) \<and> (Ifm vs bs (qe p) = Ifm vs bs (E p))"
   shows "\<And> bs. qfree (qelim p qe) \<and> (Ifm vs bs (qelim p qe) = Ifm vs bs p)"

   by (induct p rule: qelim.induct) auto
 
 
 subsection \<open>Core Procedure\<close>
 
-fun minusinf:: "fm \<Rightarrow> fm" (* Virtual substitution of -\<infinity>*)
+fun minusinf:: "fm \<Rightarrow> fm"  -- \<open>Virtual substitution of -\<infinity>\<close>
 where
   "minusinf (And p q) = conj (minusinf p) (minusinf q)"
 | "minusinf (Or p q) = disj (minusinf p) (minusinf q)"
 | "minusinf (Eq  (CNP 0 c e)) = conj (eq (CP c)) (eq e)"
 | "minusinf (NEq (CNP 0 c e)) = disj (not (eq e)) (not (eq (CP c)))"
 | "minusinf (Lt  (CNP 0 c e)) = disj (conj (eq (CP c)) (lt e)) (lt (CP (~\<^sub>p c)))"
 | "minusinf (Le  (CNP 0 c e)) = disj (conj (eq (CP c)) (le e)) (lt (CP (~\<^sub>p c)))"
 | "minusinf p = p"
 
-fun plusinf:: "fm \<Rightarrow> fm" (* Virtual substitution of +\<infinity>*)
+fun plusinf:: "fm \<Rightarrow> fm"  -- \<open>Virtual substitution of +\<infinity>\<close>
 where
   "plusinf (And p q) = conj (plusinf p) (plusinf q)"
 | "plusinf (Or p q) = disj (plusinf p) (plusinf q)"
 | "plusinf (Eq  (CNP 0 c e)) = conj (eq (CP c)) (eq e)"
 | "plusinf (NEq (CNP 0 c e)) = disj (not (eq e)) (not (eq (CP c)))"

     by simp_all
   note eqs = eq[OF nc(1), where ?'a = 'a] eq[OF nc(2), where ?'a = 'a]
   let ?c = "Ipoly vs c"
   fix y
   let ?e = "Itm vs (y#bs) e"
-  have "?c = 0 \<or> ?c > 0 \<or> ?c < 0" by arith
-  moreover {
-    assume "?c = 0"
-    then have ?case
+  consider "?c = 0" | "?c > 0" | "?c < 0" by arith
+  then show ?case
+  proof cases
+    case 1
+    then show ?thesis
       using eq[OF nc(2), of vs] eq[OF nc(1), of vs] by auto
-  }
-  moreover {
-    assume cp: "?c > 0"
-    {
-      fix x
-      assume xz: "x < -?e / ?c"
-      then have "?c * x < - ?e"
-        using pos_less_divide_eq[OF cp, where a="x" and b="-?e"]
+  next
+    case 2
+    have "Ifm vs (x#bs) (Eq (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Eq (CNP 0 c e)))"
+      if "x < -?e / ?c" for x
+    proof -
+      from that have "?c * x < - ?e"
+        using pos_less_divide_eq[OF \<open>?c > 0\<close>, where a="x" and b="-?e"]
         by (simp add: mult.commute)
       then have "?c * x + ?e < 0"
         by simp
-      then have "Ifm vs (x#bs) (Eq (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Eq (CNP 0 c e)))"
+      then show ?thesis
         using eqs tmbound0_I[OF nbe, where b="y" and b'="x" and vs=vs and bs=bs] by auto
-    }
-    then have ?case by auto
-  }
-  moreover {
-    assume cp: "?c < 0"
-    {
-      fix x
-      assume xz: "x < -?e / ?c"
-      then have "?c * x > - ?e"
-        using neg_less_divide_eq[OF cp, where a="x" and b="-?e"]
+    qed
+    then show ?thesis by auto
+  next
+    case 3
+    have "Ifm vs (x#bs) (Eq (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Eq (CNP 0 c e)))"
+      if "x < -?e / ?c" for x
+    proof -
+      from that have "?c * x > - ?e"
+        using neg_less_divide_eq[OF \<open>?c < 0\<close>, where a="x" and b="-?e"]
         by (simp add: mult.commute)
       then have "?c * x + ?e > 0"
         by simp
-      then have "Ifm vs (x#bs) (Eq (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Eq (CNP 0 c e)))"
+      then show ?thesis
         using tmbound0_I[OF nbe, where b="y" and b'="x"] eqs by auto
-    }
-    then have ?case by auto
-  }
-  ultimately show ?case by blast
+    qed
+    then show ?thesis by auto
+  qed
 next
   case (4 c e)
   then have nbe: "tmbound0 e"
     by simp
   from 4 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e"
     by simp_all
   note eqs = eq[OF nc(1), where ?'a = 'a] eq[OF nc(2), where ?'a = 'a]
   let ?c = "Ipoly vs c"
   fix y
   let ?e = "Itm vs (y#bs) e"
-  have "?c=0 \<or> ?c > 0 \<or> ?c < 0"
+  consider "?c = 0" | "?c > 0" | "?c < 0"
     by arith
-  moreover {
-    assume "?c = 0"
-    then have ?case
+  then show ?case
+  proof cases
+    case 1
+    then show ?thesis
       using eqs by auto
-  }
-  moreover {
-    assume cp: "?c > 0"
-    {
-      fix x
-      assume xz: "x < -?e / ?c"
-      then have "?c * x < - ?e"
-        using pos_less_divide_eq[OF cp, where a="x" and b="-?e"]
+  next
+    case 2
+    have "Ifm vs (x#bs) (NEq (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (NEq (CNP 0 c e)))"
+      if "x < -?e / ?c" for x
+    proof -
+      from that have "?c * x < - ?e"
+        using pos_less_divide_eq[OF \<open>?c > 0\<close>, where a="x" and b="-?e"]
         by (simp add: mult.commute)
       then have "?c * x + ?e < 0"
         by simp
-      then have "Ifm vs (x#bs) (NEq (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (NEq (CNP 0 c e)))"
+      then show ?thesis
         using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] by auto
-    }
-    then have ?case by auto
-  }
-  moreover {
-    assume cp: "?c < 0"
-    {
-      fix x
-      assume xz: "x < -?e / ?c"
-      then have "?c * x > - ?e"
-        using neg_less_divide_eq[OF cp, where a="x" and b="-?e"]
+    qed
+    then show ?thesis by auto
+  next
+    case 3
+    have "Ifm vs (x#bs) (NEq (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (NEq (CNP 0 c e)))"
+      if "x < -?e / ?c" for x
+    proof -
+      from that have "?c * x > - ?e"
+        using neg_less_divide_eq[OF \<open>?c < 0\<close>, where a="x" and b="-?e"]
         by (simp add: mult.commute)
       then have "?c * x + ?e > 0"
         by simp
-      then have "Ifm vs (x#bs) (NEq (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (NEq (CNP 0 c e)))"
+      then show ?thesis
         using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] by auto
-    }
-    then have ?case by auto
-  }
-  ultimately show ?case by blast
+    qed
+    then show ?thesis by auto
+  qed
 next
   case (5 c e)
   then have nbe: "tmbound0 e"
     by simp
   from 5 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e"

     by (simp add: polyneg_norm)
   note eqs = lt[OF nc', where ?'a = 'a] eq [OF nc(1), where ?'a = 'a] lt[OF nc(2), where ?'a = 'a]
   let ?c = "Ipoly vs c"
   fix y
   let ?e = "Itm vs (y#bs) e"
-  have "?c=0 \<or> ?c > 0 \<or> ?c < 0"
+  consider "?c = 0" | "?c > 0" | "?c < 0"
     by arith
-  moreover {
-    assume "?c = 0"
-    then have ?case using eqs by auto
-  }
-  moreover {
-    assume cp: "?c > 0"
-    {
-      fix x
-      assume xz: "x < -?e / ?c"
-      then have "?c * x < - ?e"
-        using pos_less_divide_eq[OF cp, where a="x" and b="-?e"]
+  then show ?case
+  proof cases
+    case 1
+    then show ?thesis using eqs by auto
+  next
+    case 2
+    have "Ifm vs (x#bs) (Lt (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Lt (CNP 0 c e)))"
+      if "x < -?e / ?c" for x
+    proof -
+      from that have "?c * x < - ?e"
+        using pos_less_divide_eq[OF \<open>?c > 0\<close>, where a="x" and b="-?e"]
         by (simp add: mult.commute)
       then have "?c * x + ?e < 0" by simp
-      then have "Ifm vs (x#bs) (Lt (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Lt (CNP 0 c e)))"
-        using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto
-    }
-    then have ?case by auto
-  }
-  moreover {
-    assume cp: "?c < 0"
-    {
-      fix x
-      assume xz: "x < -?e / ?c"
-      then have "?c * x > - ?e"
-        using neg_less_divide_eq[OF cp, where a="x" and b="-?e"]
+      then show ?thesis
+        using tmbound0_I[OF nbe, where b="y" and b'="x"] \<open>?c > 0\<close> eqs by auto
+    qed
+    then show ?thesis by auto
+  next
+    case 3
+    have "Ifm vs (x#bs) (Lt (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Lt (CNP 0 c e)))"
+      if "x < -?e / ?c" for x
+    proof -
+      from that have "?c * x > - ?e"
+        using neg_less_divide_eq[OF \<open>?c < 0\<close>, where a="x" and b="-?e"]
         by (simp add: mult.commute)
       then have "?c * x + ?e > 0"
         by simp
-      then have "Ifm vs (x#bs) (Lt (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Lt (CNP 0 c e)))"
-        using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] cp by auto
-    }
-    then have ?case by auto
-  }
-  ultimately show ?case by blast
+      then show ?thesis
+        using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] \<open>?c < 0\<close> by auto
+    qed
+    then show ?thesis by auto
+  qed
 next
   case (6 c e)
   then have nbe: "tmbound0 e"
     by simp
   from 6 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e"

     by (simp add: polyneg_norm)
   note eqs = lt[OF nc', where ?'a = 'a] eq [OF nc(1), where ?'a = 'a] le[OF nc(2), where ?'a = 'a]
   let ?c = "Ipoly vs c"
   fix y
   let ?e = "Itm vs (y#bs) e"
-  have "?c = 0 \<or> ?c > 0 \<or> ?c < 0" by arith
-  moreover {
-    assume "?c = 0"
-    then have ?case using eqs by auto
-  }
-  moreover {
-    assume cp: "?c > 0"
-    {
-      fix x
-      assume xz: "x < -?e / ?c"
-      then have "?c * x < - ?e"
-        using pos_less_divide_eq[OF cp, where a="x" and b="-?e"]
+  consider "?c = 0" | "?c > 0" | "?c < 0" by arith
+  then show ?case
+  proof cases
+    case 1
+    then show ?thesis using eqs by auto
+  next
+    case 2
+    have "Ifm vs (x#bs) (Le (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Le (CNP 0 c e)))"
+      if "x < -?e / ?c" for x
+    proof -
+      from that have "?c * x < - ?e"
+        using pos_less_divide_eq[OF \<open>?c > 0\<close>, where a="x" and b="-?e"]
         by (simp add: mult.commute)
       then have "?c * x + ?e < 0"
         by simp
-      then have "Ifm vs (x#bs) (Le (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Le (CNP 0 c e)))"
-        using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs
+      then show ?thesis
+        using tmbound0_I[OF nbe, where b="y" and b'="x"] \<open>?c > 0\<close> eqs
         by auto
-    }
-    then have ?case by auto
-  }
-  moreover {
-    assume cp: "?c < 0"
-    {
-      fix x
-      assume xz: "x < -?e / ?c"
-      then have "?c * x > - ?e"
-        using neg_less_divide_eq[OF cp, where a="x" and b="-?e"]
+    qed
+    then show ?thesis by auto
+  next
+    case 3
+    have "Ifm vs (x#bs) (Le (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Le (CNP 0 c e)))"
+      if "x < -?e / ?c" for x
+    proof -
+      from that have "?c * x > - ?e"
+        using neg_less_divide_eq[OF \<open>?c < 0\<close>, where a="x" and b="-?e"]
         by (simp add: mult.commute)
       then have "?c * x + ?e > 0"
         by simp
-      then have "Ifm vs (x#bs) (Le (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Le (CNP 0 c e)))"
-        using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs
+      then show ?thesis
+        using tmbound0_I[OF nbe, where b="y" and b'="x"] \<open>?c < 0\<close> eqs
         by auto
-    }
-    then have ?case by auto
-  }
-  ultimately show ?case by blast
+    qed
+    then show ?thesis by auto
+  qed
 qed auto
 
 lemma plusinf_inf:
   assumes lp: "islin p"
   shows "\<exists>z. \<forall>x > z. Ifm vs (x#bs) (plusinf p) \<longleftrightarrow> Ifm vs (x#bs) p"

 lemma plusinf_uset0:
   assumes lp: "islin p"
     and nmi: "\<not> (Ifm vs (x#bs) (plusinf p))"
     and ex: "Ifm vs (x#bs) p" (is "?I x p")
   shows "\<exists>(c, s) \<in> set (uset p). x \<le> - Itm vs (x#bs) s / Ipoly vs c"
-proof-
+proof -
   have "\<exists>(c, s) \<in> set (uset p).
       Ipoly vs c < 0 \<and> Ipoly vs c * x \<ge> - Itm vs (x#bs) s \<or>
       Ipoly vs c > 0 \<and> Ipoly vs c * x \<le> - Itm vs (x#bs) s"
     using lp nmi ex
     apply (induct p rule: minusinf.induct)

     by blast
   from fr_eq[OF lp, of vs bs x, simplified th'] show ?thesis .
 qed
 
 lemma simpfm_lin:
-  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
+  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   shows "qfree p \<Longrightarrow> islin (simpfm p)"
   by (induct p rule: simpfm.induct) (auto simp add: conj_lin disj_lin)
 
 definition "ferrack p \<equiv>
   let

   using lp tnb
   by (induct p c t rule: msubstpos.induct)
     (auto simp add: msubsteq2_nb msubstltpos_nb msubstlepos_nb)
 
 lemma msubstneg_nb:
-  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
+  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
     and lp: "islin p"
     and tnb: "tmbound0 t"
   shows "bound0 (msubstneg p c t)"
   using lp tnb
   by (induct p c t rule: msubstneg.induct)
     (auto simp add: msubsteq2_nb msubstltneg_nb msubstleneg_nb)
 
 lemma msubst2_nb:
-  assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
+  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
     and lp: "islin p"
     and tnb: "tmbound0 t"
   shows "bound0 (msubst2 p c t)"
   using lp tnb
   by (simp add: msubst2_def msubstneg_nb msubstpos_nb lt_nb simpfm_bound0)

 
 method_setup frpar2 = \<open>
   Parametric_Ferrante_Rackoff.method true
 \<close> "parametric QE for linear Arithmetic over fields, Version 2"
 
-lemma "\<exists>(x::'a::{linordered_field}). y \<noteq> -1 \<longrightarrow> (y + 1) * x < 0"
+lemma "\<exists>(x::'a::linordered_field). y \<noteq> -1 \<longrightarrow> (y + 1) * x < 0"
   apply (frpar type: 'a pars: y)
   apply (simp add: field_simps)
   apply (rule spec[where x=y])
   apply (frpar type: 'a pars: "z::'a")
   apply simp
   done
 
-lemma "\<exists>(x::'a::{linordered_field}). y \<noteq> -1 \<longrightarrow> (y + 1)*x < 0"
+lemma "\<exists>(x::'a::linordered_field). y \<noteq> -1 \<longrightarrow> (y + 1)*x < 0"
   apply (frpar2 type: 'a pars: y)
   apply (simp add: field_simps)
   apply (rule spec[where x=y])
   apply (frpar2 type: 'a pars: "z::'a")
   apply simp
   done
 
-text\<open>Collins/Jones Problem\<close>
+text \<open>Collins/Jones Problem\<close>
 (*
 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"
-proof-
+proof -
   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")
 by (simp add: field_simps)
 have "?rhs"
 
   apply (frpar type: "'a::{linordered_field, number_ring}" pars: "a::'a::{linordered_field, number_ring}" "b::'a::{linordered_field, number_ring}")

 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"
 apply (frpar type: "'a::{linordered_field, number_ring}" pars: "t::'a::{linordered_field, number_ring}")
 oops
 *)
 
-text\<open>Collins/Jones Problem\<close>
+text \<open>Collins/Jones Problem\<close>
 
 (*
 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"
-proof-
+proof -
   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")
 by (simp add: field_simps)
 have "?rhs"
   apply (frpar2 type: "'a::{linordered_field, number_ring}" pars: "a::'a::{linordered_field, number_ring}" "b::'a::{linordered_field, number_ring}")
   apply simp