src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
changeset 68442 477b3f7067c9
parent 67399 eab6ce8368fa
child 69214 74455459973d
     1.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Thu Jun 14 10:51:12 2018 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Thu Jun 14 15:45:53 2018 +0200
     1.3 @@ -35,7 +35,7 @@
     1.4  end
     1.5  
     1.6  text \<open>Semantics of terms tm.\<close>
     1.7 -primrec Itm :: "'a::{field_char_0,field} list \<Rightarrow> 'a list \<Rightarrow> tm \<Rightarrow> 'a"
     1.8 +primrec Itm :: "'a::field_char_0 list \<Rightarrow> 'a list \<Rightarrow> tm \<Rightarrow> 'a"
     1.9    where
    1.10      "Itm vs bs (CP c) = (Ipoly vs c)"
    1.11    | "Itm vs bs (Bound n) = bs!n"
    1.12 @@ -319,7 +319,7 @@
    1.13    by (induct t arbitrary: i rule: tmmul.induct) (auto simp add: Let_def)
    1.14  
    1.15  lemma tmmul_allpolys_npoly[simp]:
    1.16 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
    1.17 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
    1.18    shows "allpolys isnpoly t \<Longrightarrow> isnpoly c \<Longrightarrow> allpolys isnpoly (tmmul t c)"
    1.19    by (induct t rule: tmmul.induct) (simp_all add: Let_def polymul_norm)
    1.20  
    1.21 @@ -345,7 +345,7 @@
    1.22    by (simp add: isnpoly_def)
    1.23  
    1.24  lemma tmneg_allpolys_npoly[simp]:
    1.25 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
    1.26 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
    1.27    shows "allpolys isnpoly t \<Longrightarrow> allpolys isnpoly (tmneg t)"
    1.28    by (auto simp: tmneg_def)
    1.29  
    1.30 @@ -362,7 +362,7 @@
    1.31    using tmsub_def by simp
    1.32  
    1.33  lemma tmsub_allpolys_npoly[simp]:
    1.34 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
    1.35 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
    1.36    shows "allpolys isnpoly t \<Longrightarrow> allpolys isnpoly s \<Longrightarrow> allpolys isnpoly (tmsub t s)"
    1.37    by (simp add: tmsub_def isnpoly_def)
    1.38  
    1.39 @@ -379,7 +379,7 @@
    1.40        (let c' = polynate c in if c' = 0\<^sub>p then simptm t else tmadd (CNP n c' (CP 0\<^sub>p)) (simptm t))"
    1.41  
    1.42  lemma polynate_stupid:
    1.43 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
    1.44 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
    1.45    shows "polynate t = 0\<^sub>p \<Longrightarrow> Ipoly bs t = (0::'a)"
    1.46    apply (subst polynate[symmetric])
    1.47    apply simp
    1.48 @@ -402,7 +402,7 @@
    1.49    by (simp_all add: isnpoly_def)
    1.50  
    1.51  lemma simptm_allpolys_npoly[simp]:
    1.52 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
    1.53 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
    1.54    shows "allpolys isnpoly (simptm p)"
    1.55    by (induct p rule: simptm.induct) (auto simp add: Let_def)
    1.56  
    1.57 @@ -452,7 +452,7 @@
    1.58  qed
    1.59  
    1.60  lemma split0_nb0:
    1.61 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
    1.62 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
    1.63    shows "split0 t = (c',t') \<Longrightarrow>  tmbound 0 t'"
    1.64  proof -
    1.65    fix c' t'
    1.66 @@ -464,7 +464,7 @@
    1.67  qed
    1.68  
    1.69  lemma split0_nb0'[simp]:
    1.70 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
    1.71 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
    1.72    shows "tmbound0 (snd (split0 t))"
    1.73    using split0_nb0[of t "fst (split0 t)" "snd (split0 t)"]
    1.74    by (simp add: tmbound0_tmbound_iff)
    1.75 @@ -492,7 +492,7 @@
    1.76    by (induct p rule: split0.induct) (auto simp  add: isnpoly_def Let_def split_def)
    1.77  
    1.78  lemma isnpoly_fst_split0:
    1.79 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
    1.80 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
    1.81    shows "allpolys isnpoly p \<Longrightarrow> isnpoly (fst (split0 p))"
    1.82    by (induct p rule: split0.induct)
    1.83      (auto simp  add: polyadd_norm polysub_norm polyneg_norm polymul_norm Let_def split_def)
    1.84 @@ -1172,7 +1172,7 @@
    1.85  definition "simpneq t = (let (c,s) = split0 (simptm t) in if c= 0\<^sub>p then neq s else NEq (CNP 0 c s))"
    1.86  
    1.87  lemma simplt_islin [simp]:
    1.88 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
    1.89 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
    1.90    shows "islin (simplt t)"
    1.91    unfolding simplt_def
    1.92    using split0_nb0'
    1.93 @@ -1180,7 +1180,7 @@
    1.94        islin_stupid allpolys_split0[OF simptm_allpolys_npoly])
    1.95  
    1.96  lemma simple_islin [simp]:
    1.97 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
    1.98 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
    1.99    shows "islin (simple t)"
   1.100    unfolding simple_def
   1.101    using split0_nb0'
   1.102 @@ -1188,7 +1188,7 @@
   1.103        islin_stupid allpolys_split0[OF simptm_allpolys_npoly] le_lin)
   1.104  
   1.105  lemma simpeq_islin [simp]:
   1.106 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   1.107 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
   1.108    shows "islin (simpeq t)"
   1.109    unfolding simpeq_def
   1.110    using split0_nb0'
   1.111 @@ -1196,7 +1196,7 @@
   1.112        islin_stupid allpolys_split0[OF simptm_allpolys_npoly] eq_lin)
   1.113  
   1.114  lemma simpneq_islin [simp]:
   1.115 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   1.116 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
   1.117    shows "islin (simpneq t)"
   1.118    unfolding simpneq_def
   1.119    using split0_nb0'
   1.120 @@ -1207,7 +1207,7 @@
   1.121    by (cases "split0 s") auto
   1.122  
   1.123  lemma split0_npoly:
   1.124 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   1.125 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
   1.126      and *: "allpolys isnpoly t"
   1.127    shows "isnpoly (fst (split0 t))"
   1.128      and "allpolys isnpoly (snd (split0 t))"
   1.129 @@ -1323,7 +1323,7 @@
   1.130    done
   1.131  
   1.132  lemma simplt_nb[simp]:
   1.133 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   1.134 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
   1.135    shows "tmbound0 t \<Longrightarrow> bound0 (simplt t)"
   1.136  proof (simp add: simplt_def Let_def split_def)
   1.137    assume "tmbound0 t"
   1.138 @@ -1344,7 +1344,7 @@
   1.139  qed
   1.140  
   1.141  lemma simple_nb[simp]:
   1.142 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   1.143 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
   1.144    shows "tmbound0 t \<Longrightarrow> bound0 (simple t)"
   1.145  proof(simp add: simple_def Let_def split_def)
   1.146    assume "tmbound0 t"
   1.147 @@ -1365,7 +1365,7 @@
   1.148  qed
   1.149  
   1.150  lemma simpeq_nb[simp]:
   1.151 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   1.152 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
   1.153    shows "tmbound0 t \<Longrightarrow> bound0 (simpeq t)"
   1.154  proof (simp add: simpeq_def Let_def split_def)
   1.155    assume "tmbound0 t"
   1.156 @@ -1386,7 +1386,7 @@
   1.157  qed
   1.158  
   1.159  lemma simpneq_nb[simp]:
   1.160 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   1.161 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
   1.162    shows "tmbound0 t \<Longrightarrow> bound0 (simpneq t)"
   1.163  proof (simp add: simpneq_def Let_def split_def)
   1.164    assume "tmbound0 t"
   1.165 @@ -1541,7 +1541,7 @@
   1.166    by (induct p arbitrary: bs rule: simpfm.induct) auto
   1.167  
   1.168  lemma simpfm_bound0:
   1.169 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   1.170 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
   1.171    shows "bound0 p \<Longrightarrow> bound0 (simpfm p)"
   1.172    by (induct p rule: simpfm.induct) auto
   1.173  
   1.174 @@ -1591,7 +1591,7 @@
   1.175    by (simp add: conj_def)
   1.176  
   1.177  lemma
   1.178 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   1.179 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
   1.180    shows "qfree p \<Longrightarrow> islin (simpfm p)"
   1.181    by (induct p rule: simpfm.induct) (simp_all add: conj_lin disj_lin)
   1.182  
   1.183 @@ -3313,7 +3313,7 @@
   1.184  qed
   1.185  
   1.186  lemma simpfm_lin:
   1.187 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   1.188 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
   1.189    shows "qfree p \<Longrightarrow> islin (simpfm p)"
   1.190    by (induct p rule: simpfm.induct) (auto simp add: conj_lin disj_lin)
   1.191  
   1.192 @@ -3627,7 +3627,7 @@
   1.193      (auto simp add: msubsteq2_nb msubstltpos_nb msubstlepos_nb)
   1.194  
   1.195  lemma msubstneg_nb:
   1.196 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   1.197 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
   1.198      and lp: "islin p"
   1.199      and tnb: "tmbound0 t"
   1.200    shows "bound0 (msubstneg p c t)"
   1.201 @@ -3636,7 +3636,7 @@
   1.202      (auto simp add: msubsteq2_nb msubstltneg_nb msubstleneg_nb)
   1.203  
   1.204  lemma msubst2_nb:
   1.205 -  assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   1.206 +  assumes "SORT_CONSTRAINT('a::field_char_0)"
   1.207      and lp: "islin p"
   1.208      and tnb: "tmbound0 t"
   1.209    shows "bound0 (msubst2 p c t)"