src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy

 instance ..
 
 end
 
 text \<open>Semantics of terms tm.\<close>
-primrec Itm :: "'a::{field_char_0,field} list \<Rightarrow> 'a list \<Rightarrow> tm \<Rightarrow> 'a"
+primrec Itm :: "'a::field_char_0 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"

 
 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)"
   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))"
   by (simp add: isnpoly_def)
 
 lemma tmneg_allpolys_npoly[simp]:
-  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+  assumes "SORT_CONSTRAINT('a::field_char_0)"
   shows "allpolys isnpoly t \<Longrightarrow> allpolys isnpoly (tmneg t)"
   by (auto simp: tmneg_def)
 
 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)"
   shows "allpolys isnpoly t \<Longrightarrow> allpolys isnpoly s \<Longrightarrow> allpolys isnpoly (tmsub t s)"
   by (simp add: tmsub_def 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)"
   shows "polynate t = 0\<^sub>p \<Longrightarrow> Ipoly bs t = (0::'a)"
   apply (subst polynate[symmetric])
   apply simp
   done
 

 lemma [simp]: "isnpoly 0\<^sub>p"
   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)"
   shows "allpolys isnpoly (simptm p)"
   by (induct p rule: simptm.induct) (auto simp add: Let_def)
 
 declare let_cong[fundef_cong del]
 

   with split0[where t="t" and bs="bs"] 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)"
   shows "split0 t = (c',t') \<Longrightarrow>  tmbound 0 t'"
 proof -
   fix c' t'
   assume "split0 t = (c', t')"
   then have "c' = fst (split0 t)" "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)"
   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)"
   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)
 
 

 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)"
   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)"
   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)"
   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)"
   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)"
     and *: "allpolys isnpoly t"
   shows "isnpoly (fst (split0 t))"
     and "allpolys isnpoly (snd (split0 t))"
   using *
   by (induct t rule: split0.induct)

   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)"
   shows "tmbound0 t \<Longrightarrow> bound0 (simplt t)"
 proof (simp add: simplt_def Let_def split_def)
   assume "tmbound0 t"
   then have *: "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)"
   shows "tmbound0 t \<Longrightarrow> bound0 (simple t)"
 proof(simp add: simple_def Let_def split_def)
   assume "tmbound0 t"
   then have *: "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)"
   shows "tmbound0 t \<Longrightarrow> bound0 (simpeq t)"
 proof (simp add: simpeq_def Let_def split_def)
   assume "tmbound0 t"
   then have *: "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)"
   shows "tmbound0 t \<Longrightarrow> bound0 (simpneq t)"
 proof (simp add: simpneq_def Let_def split_def)
   assume "tmbound0 t"
   then have *: "tmbound0 (simptm t)"
     by simp

 
 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)"
   shows "bound0 p \<Longrightarrow> bound0 (simpfm p)"
   by (induct p rule: simpfm.induct) auto
 
 lemma lt_qf[simp]: "qfree (lt t)"
   apply (cases t)

 
 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)"
   shows "qfree p \<Longrightarrow> islin (simpfm p)"
   by (induct p rule: simpfm.induct) (simp_all add: conj_lin disj_lin)
 
 fun prep :: "fm \<Rightarrow> fm"
   where

     by blast
   from fr_eq[OF lp, of vs bs x, simplified **] show ?thesis .
 qed
 
 lemma simpfm_lin:
-  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
+  assumes "SORT_CONSTRAINT('a::field_char_0)"
   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)"
     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)"
     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)