# HG changeset patch
# User wenzelm
# Date 1435007988 -7200
# Node ID ce7030d9191d023d5267b613313a17f9a641ed90
# Parent  48d7b203c0eae5f8d6b073845f0924592670767b
tuned proofs;

diff -r 48d7b203c0ea -r ce7030d9191d src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Mon Jun 22 21:50:56 2015 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Mon Jun 22 23:19:48 2015 +0200
@@ -2,7 +2,7 @@
     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
@@ -18,7 +18,7 @@
 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"
@@ -29,8 +29,8 @@
 | "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"
@@ -60,7 +60,7 @@
 | "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)"
@@ -74,9 +74,9 @@
   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)"
@@ -146,8 +146,7 @@
 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:
@@ -160,44 +159,45 @@
   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:
@@ -217,7 +217,7 @@
 | "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)"
@@ -256,7 +256,8 @@
 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)"
@@ -272,9 +273,13 @@
   "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
@@ -311,7 +316,7 @@
   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)
 
@@ -337,7 +342,7 @@
   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
 
@@ -354,7 +359,7 @@
   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)
 
@@ -371,7 +376,7 @@
     (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
@@ -390,17 +395,17 @@
   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'))"
@@ -420,7 +425,7 @@
   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)
@@ -445,7 +450,7 @@
 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'
@@ -457,7 +462,7 @@
 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)
@@ -485,13 +490,13 @@
   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
@@ -514,7 +519,7 @@
   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"
@@ -731,27 +736,27 @@
   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)
 
@@ -807,8 +812,9 @@
   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)"
@@ -817,15 +823,15 @@
     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)"
@@ -834,10 +840,9 @@
     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)
 
@@ -894,7 +899,7 @@
 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"
@@ -918,8 +923,13 @@
   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)
@@ -927,12 +937,22 @@
 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
@@ -952,8 +972,8 @@
     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
@@ -1026,7 +1046,7 @@
       (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)"
@@ -1146,7 +1166,7 @@
 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'
@@ -1154,7 +1174,7 @@
       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'
@@ -1162,7 +1182,7 @@
       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'
@@ -1170,7 +1190,7 @@
       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'
@@ -1181,7 +1201,7 @@
   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))"
@@ -1195,20 +1215,18 @@
   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)"
@@ -1216,20 +1234,18 @@
   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)"
@@ -1237,19 +1253,17 @@
   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)"
@@ -1257,19 +1271,17 @@
   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)"
@@ -1305,7 +1317,7 @@
   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"
@@ -1326,7 +1338,7 @@
 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"
@@ -1347,7 +1359,7 @@
 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"
@@ -1368,7 +1380,7 @@
 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"
@@ -1474,15 +1486,15 @@
     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))"
@@ -1526,7 +1538,7 @@
   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
 
@@ -1551,12 +1563,20 @@
   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
@@ -1567,7 +1587,7 @@
   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)
 
@@ -1596,13 +1616,13 @@
   "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))"
@@ -1613,7 +1633,7 @@
 | "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:
@@ -1625,7 +1645,7 @@
 
 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)"
@@ -1635,7 +1655,7 @@
 | "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)"
@@ -1673,43 +1693,41 @@
   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"
@@ -1720,44 +1738,42 @@
   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"
@@ -1770,42 +1786,40 @@
   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"
@@ -1818,44 +1832,42 @@
   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:
@@ -2173,7 +2185,7 @@
     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"
@@ -3379,7 +3391,7 @@
 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)
 
@@ -3704,7 +3716,7 @@
     (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)"
@@ -3713,7 +3725,7 @@
     (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)"
@@ -4196,7 +4208,7 @@
   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])
@@ -4204,7 +4216,7 @@
   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])
@@ -4212,10 +4224,10 @@
   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"
@@ -4230,11 +4242,11 @@
 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"