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.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.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.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.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.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)"
```