src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy

   apply (case_tac poly, auto)
   done
 
 lemma simplt_nb[simp]:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   shows "tmbound0 t \<Longrightarrow> bound0 (simplt t)"
-  using split0 [of "simptm t" vs bs]
+  using split0 [of "simptm t" "vs::'a list" bs]
 proof(simp add: simplt_def Let_def split_def)
   assume nb: "tmbound0 t"
   hence nb': "tmbound0 (simptm t)" by simp
   let ?c = "fst (split0 (simptm t))"
   from tmbound_split0[OF nb'[unfolded tmbound0_tmbound_iff[symmetric]]]

        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_inverse_zero})"
   shows "tmbound0 t \<Longrightarrow> bound0 (simple t)"
-  using split0 [of "simptm t" vs bs]
+  using split0 [of "simptm t" "vs::'a list" bs]
 proof(simp add: simple_def Let_def split_def)
   assume nb: "tmbound0 t"
   hence nb': "tmbound0 (simptm t)" by simp
   let ?c = "fst (split0 (simptm t))"
   from tmbound_split0[OF nb'[unfolded tmbound0_tmbound_iff[symmetric]]]

        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_inverse_zero})"
   shows "tmbound0 t \<Longrightarrow> bound0 (simpeq t)"
-  using split0 [of "simptm t" vs bs]
+  using split0 [of "simptm t" "vs::'a list" bs]
 proof(simp add: simpeq_def Let_def split_def)
   assume nb: "tmbound0 t"
   hence nb': "tmbound0 (simptm t)" by simp
   let ?c = "fst (split0 (simptm t))"
   from tmbound_split0[OF nb'[unfolded tmbound0_tmbound_iff[symmetric]]]

        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_inverse_zero})"
   shows "tmbound0 t \<Longrightarrow> bound0 (simpneq t)"
-  using split0 [of "simptm t" vs bs]
+  using split0 [of "simptm t" "vs::'a list" bs]
 proof(simp add: simpneq_def Let_def split_def)
   assume nb: "tmbound0 t"
   hence nb': "tmbound0 (simptm t)" by simp
   let ?c = "fst (split0 (simptm t))"
   from tmbound_split0[OF nb'[unfolded tmbound0_tmbound_iff[symmetric]]]