src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy

 next
   case (Cons x xs n m)
   {assume nxs: "n \<ge> length (x#xs)" hence ?case using removen_same[OF nxs] by simp}
   moreover
   {assume nxs: "\<not> (n \<ge> length (x#xs))" 
-    {assume mln: "m < n" hence ?case using prems by (cases m, auto)}
+    {assume mln: "m < n" hence ?case using Cons by (cases m, auto)}
     moreover
     {assume mln: "\<not> (m < n)" 
-      
-      {assume mxs: "m \<le> length (x#xs)" hence ?case using prems by (cases m, auto)}
+      {assume mxs: "m \<le> length (x#xs)" hence ?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))" by auto

           by auto
         hence ?case using nxs mln mxs by auto }
       ultimately have ?case by blast
     }
     ultimately have ?case by blast
-    
-  }      ultimately show ?case by blast
+  } ultimately show ?case by blast
 qed
 
 lemma decrtm: assumes bnd: "tmboundslt (length bs) t" and nb: "tmbound m t" 
   and nle: "m \<le> length bs" 
   shows "Itm vs (removen m bs) (decrtm m t) = Itm vs bs t"
-  using bnd nb nle
-  by (induct t rule: tm.induct, auto simp add: removen_nth)
+  using bnd nb nle by (induct t rule: tm.induct) (auto simp add: removen_nth)
 
 primrec tmsubst0:: "tm \<Rightarrow> tm \<Rightarrow> tm" where
   "tmsubst0 t (CP c) = CP c"
 | "tmsubst0 t (Bound n) = (if n=0 then t else Bound n)"
 | "tmsubst0 t (CNP n c a) = (if n=0 then Add (Mul c t) (tmsubst0 t a) else CNP n c (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:
   shows "Itm vs (x#bs) (tmsubst0 t a) = Itm vs ((Itm vs (x#bs) t)#bs) a"
-by (induct a rule: tm.induct,auto simp add: nth_pos2)
+  by (induct a rule: tm.induct) (auto simp add: nth_pos2)
 
 lemma tmsubst0_nb: "tmbound0 t \<Longrightarrow> tmbound0 (tmsubst0 t a)"
-by (induct a rule: tm.induct,auto simp add: nth_pos2)
+  by (induct a rule: tm.induct) (auto simp add: nth_pos2)
 
 primrec tmsubst:: "nat \<Rightarrow> tm \<Rightarrow> tm \<Rightarrow> tm" where
   "tmsubst n t (CP c) = CP c"
 | "tmsubst n t (Bound m) = (if n=m then t else Bound m)"
 | "tmsubst n t (CNP m c a) = (if n=m then Add (Mul c t) (tmsubst n t a) 

   shows "Ifm vs (bs[n:=x]) p = Ifm vs bs p"
   using bnd nb le tmbound_I[where bs=bs and vs = vs]
 proof(induct p arbitrary: bs n rule: fm.induct)
   case (E p bs n) 
   {fix y
-    from prems have bnd: "boundslt (length (y#bs)) p" 
+    from E have bnd: "boundslt (length (y#bs)) p" 
       and nb: "bound (Suc n) p" and le: "Suc n \<le> length (y#bs)" by simp+
     from E.hyps[OF bnd nb le tmbound_I] have "Ifm vs ((y#bs)[Suc n:=x]) p = Ifm vs (y#bs) p" .   }
   thus ?case by simp 
 next
   case (A p bs n) {fix y
-    from prems have bnd: "boundslt (length (y#bs)) p" 
+    from A have bnd: "boundslt (length (y#bs)) p" 
       and nb: "bound (Suc n) p" and le: "Suc n \<le> length (y#bs)" by simp+
     from A.hyps[OF bnd nb le tmbound_I] have "Ifm vs ((y#bs)[Suc n:=x]) p = Ifm vs (y#bs) p" .   }
   thus ?case by simp 
 qed auto
 

   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
-    from prems have bnd: "boundslt (length (x#bs)) p" and nb: "bound (Suc m) p" 
+    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 prems(4)[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] have "Ifm vs (removen (Suc m) (x#bs)) (decr (Suc m) p) = Ifm vs (x#bs) p".
   } thus ?case by auto 
 next
   case (A p bs m)  
   {fix x
-    from prems have bnd: "boundslt (length (x#bs)) p" and nb: "bound (Suc m) p" 
+    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 prems(4)[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] have "Ifm vs (removen (Suc m) (x#bs)) (decr (Suc m) p) = Ifm vs (x#bs) p".
   } thus ?case by auto
 qed (auto simp add: decrtm removen_nth)
 
 primrec subst0:: "tm \<Rightarrow> fm \<Rightarrow> fm" where
   "subst0 t T = T"

   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 
-    from prems have bn: "boundslt (length (x#bs)) p" by simp 
-      from prems have nlm: "Suc n \<le> length (x#bs)" by simp
-    from prems(3)[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 
+    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 
     hence "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) = Ifm vs (x#bs[n:= Itm vs bs t]) p"
     by (simp add: incrtm0[where x="x" and bs="bs" and t="t"]) }  
 thus ?case by simp 
 next
   case (A p bs n)   
   {fix x 
-    from prems have bn: "boundslt (length (x#bs)) p" by simp 
-      from prems have nlm: "Suc n \<le> length (x#bs)" by simp
-    from prems(3)[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 
+    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 
     hence "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) = Ifm vs (x#bs[n:= Itm vs bs t]) p"
     by (simp add: incrtm0[where x="x" and bs="bs" and t="t"]) }  
 thus ?case by simp 
 qed(auto simp add: tmsubst)
 

   case 1 thus ?case by (auto,rule_tac x="min z za" in exI, auto)
 next
   case 2 thus ?case by (auto,rule_tac x="min z za" in exI, auto)
 next
   case (3 c e) hence nbe: "tmbound0 e" by simp
-  from prems have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
+  from 3 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"
   let ?e = "Itm vs (y#bs) e"
   have "?c=0 \<or> ?c > 0 \<or> ?c < 0" by arith
   moreover {assume "?c = 0" hence ?case 

       hence "Ifm vs (x#bs) (Eq (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Eq (CNP 0 c e)))"
         using tmbound0_I[OF nbe, where b="y" and b'="x"] eqs by auto} hence ?case by auto}
   ultimately show ?case by blast
 next
   case (4 c e)  hence nbe: "tmbound0 e" by simp
-  from prems have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
+  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"
   let ?e = "Itm vs (y#bs) e"
   have "?c=0 \<or> ?c > 0 \<or> ?c < 0" by arith
   moreover {assume "?c = 0" hence ?case using eqs by auto}

       hence "Ifm vs (x#bs) (NEq (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (NEq (CNP 0 c e)))"
         using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] by auto} hence ?case by auto}
   ultimately show ?case by blast
 next
   case (5 c e)  hence nbe: "tmbound0 e" by simp
-  from prems have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
+  from 5 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
   hence nc': "allpolys isnpoly (CP (~\<^sub>p c))" 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"
   let ?e = "Itm vs (y#bs) e"
   have "?c=0 \<or> ?c > 0 \<or> ?c < 0" by arith

       hence "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} hence ?case by auto}
   ultimately show ?case by blast
 next
   case (6 c e)  hence nbe: "tmbound0 e" by simp
-  from prems have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
+  from 6 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
   hence nc': "allpolys isnpoly (CP (~\<^sub>p c))" 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"
   let ?e = "Itm vs (y#bs) e"
   have "?c=0 \<or> ?c > 0 \<or> ?c < 0" by arith

   case 1 thus ?case by (auto,rule_tac x="max z za" in exI, auto)
 next
   case 2 thus ?case by (auto,rule_tac x="max z za" in exI, auto)
 next
   case (3 c e) hence nbe: "tmbound0 e" by simp
-  from prems have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
+  from 3 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"
   let ?e = "Itm vs (y#bs) e"
   have "?c=0 \<or> ?c > 0 \<or> ?c < 0" by arith
   moreover {assume "?c = 0" hence ?case 

       hence "?c * x + ?e < 0" by simp
       hence "Ifm vs (x#bs) (Eq (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (Eq (CNP 0 c e)))"
         using tmbound0_I[OF nbe, where b="y" and b'="x"] eqs by auto} hence ?case by auto}
   ultimately show ?case by blast
 next
-  case (4 c e)  hence nbe: "tmbound0 e" by simp
-  from prems have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
+  case (4 c e) hence 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"
   let ?e = "Itm vs (y#bs) e"
   have "?c=0 \<or> ?c > 0 \<or> ?c < 0" by arith
   moreover {assume "?c = 0" hence ?case using eqs by auto}

       hence "?c * x + ?e < 0" by simp
       hence "Ifm vs (x#bs) (NEq (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (NEq (CNP 0 c e)))"
         using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] by auto} hence ?case by auto}
   ultimately show ?case by blast
 next
-  case (5 c e)  hence nbe: "tmbound0 e" by simp
-  from prems have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
+  case (5 c e) hence nbe: "tmbound0 e" by simp
+  from 5 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
   hence nc': "allpolys isnpoly (CP (~\<^sub>p c))" by (simp add: polyneg_norm)
   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]
   let ?c = "Ipoly vs c"
   let ?e = "Itm vs (y#bs) e"
   have "?c=0 \<or> ?c > 0 \<or> ?c < 0" by arith

       hence "Ifm vs (x#bs) (Lt (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (Lt (CNP 0 c e)))"
         using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] cp by auto} hence ?case by auto}
   ultimately show ?case by blast
 next
   case (6 c e)  hence nbe: "tmbound0 e" by simp
-  from prems have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
+  from 6 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all
   hence nc': "allpolys isnpoly (CP (~\<^sub>p c))" by (simp add: polyneg_norm)
   note eqs = lt[OF nc(1), where ?'a = 'a] eq [OF nc(1), where ?'a = 'a] le[OF nc(2), where ?'a = 'a]
   let ?c = "Ipoly vs c"
   let ?e = "Itm vs (y#bs) e"
   have "?c=0 \<or> ?c > 0 \<or> ?c < 0" by arith