src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
 changeset 47108 2a1953f0d20d parent 45499 849d697adf1e child 48562 f6d6d58fa318
```     1.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Sat Mar 24 16:27:04 2012 +0100
1.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Sun Mar 25 20:15:39 2012 +0200
1.3 @@ -25,7 +25,7 @@
1.4  | "tmsize (CNP n c a) = 3 + polysize c + tmsize a "
1.5
1.6    (* Semantics of terms tm *)
1.7 -primrec Itm :: "'a::{field_char_0, field_inverse_zero, number_ring} list \<Rightarrow> 'a list \<Rightarrow> tm \<Rightarrow> 'a" where
1.8 +primrec Itm :: "'a::{field_char_0, field_inverse_zero} list \<Rightarrow> 'a list \<Rightarrow> tm \<Rightarrow> 'a" where
1.9    "Itm vs bs (CP c) = (Ipoly vs c)"
1.10  | "Itm vs bs (Bound n) = bs!n"
1.11  | "Itm vs bs (Neg a) = -(Itm vs bs a)"
1.12 @@ -430,7 +430,7 @@
1.13  by (induct p rule: fmsize.induct) simp_all
1.14
1.15    (* Semantics of formulae (fm) *)
1.16 -primrec Ifm ::"'a::{linordered_field_inverse_zero, number_ring} list \<Rightarrow> 'a list \<Rightarrow> fm \<Rightarrow> bool" where
1.17 +primrec Ifm ::"'a::{linordered_field_inverse_zero} list \<Rightarrow> 'a list \<Rightarrow> fm \<Rightarrow> bool" where
1.18    "Ifm vs bs T = True"
1.19  | "Ifm vs bs F = False"
1.20  | "Ifm vs bs (Lt a) = (Itm vs bs a < 0)"
1.21 @@ -1937,7 +1937,7 @@
1.22
1.23      also have "\<dots> \<longleftrightarrow> - (?a * ?s) + 2*?d*?r = 0" using d by simp
1.24      finally have ?thesis using c d
1.25 -      by (simp add: r[of "- (Itm vs (x # bs) s / (2 * \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>))"] msubsteq_def Let_def evaldjf_ex del: one_add_one_is_two)
1.26 +      by (simp add: r[of "- (Itm vs (x # bs) s / (2 * \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>))"] msubsteq_def Let_def evaldjf_ex)
1.27    }
1.28    moreover
1.29    {assume c: "?c \<noteq> 0" and d: "?d=0"
1.30 @@ -1950,7 +1950,7 @@
1.31        by (simp add: field_simps right_distrib[of "2*?c"] del: right_distrib)
1.32      also have "\<dots> \<longleftrightarrow> - (?a * ?t) + 2*?c*?r = 0" using c by simp
1.33      finally have ?thesis using c d
1.34 -      by (simp add: r[of "- (?t/ (2*?c))"] msubsteq_def Let_def evaldjf_ex del: one_add_one_is_two)
1.35 +      by (simp add: r[of "- (?t/ (2*?c))"] msubsteq_def Let_def evaldjf_ex)
1.36    }
1.37    moreover
1.38    {assume c: "?c \<noteq> 0" and d: "?d\<noteq>0" hence dc: "?c * ?d *2 \<noteq> 0" by simp
1.39 @@ -2019,7 +2019,7 @@
1.40
1.41      also have "\<dots> \<longleftrightarrow> - (?a * ?s) + 2*?d*?r \<noteq> 0" using d by simp
1.42      finally have ?thesis using c d
1.43 -      by (simp add: r[of "- (Itm vs (x # bs) s / (2 * \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>))"] msubstneq_def Let_def evaldjf_ex del: one_add_one_is_two)
1.44 +      by (simp add: r[of "- (Itm vs (x # bs) s / (2 * \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>))"] msubstneq_def Let_def evaldjf_ex)
1.45    }
1.46    moreover
1.47    {assume c: "?c \<noteq> 0" and d: "?d=0"
1.48 @@ -2032,7 +2032,7 @@
1.49        by (simp add: field_simps right_distrib[of "2*?c"] del: right_distrib)
1.50      also have "\<dots> \<longleftrightarrow> - (?a * ?t) + 2*?c*?r \<noteq> 0" using c by simp
1.51      finally have ?thesis using c d
1.52 -      by (simp add: r[of "- (?t/ (2*?c))"] msubstneq_def Let_def evaldjf_ex del: one_add_one_is_two)
1.53 +      by (simp add: r[of "- (?t/ (2*?c))"] msubstneq_def Let_def evaldjf_ex)
1.54    }
1.55    moreover
1.56    {assume c: "?c \<noteq> 0" and d: "?d\<noteq>0" hence dc: "?c * ?d *2 \<noteq> 0" by simp
1.57 @@ -2616,10 +2616,10 @@
1.58  using lp tnb
1.59  by (simp add: msubst2_def msubstneg_nb msubstpos_nb conj_nb disj_nb lt_nb simpfm_bound0)
1.60
1.61 -lemma mult_minus2_left: "-2 * (x::'a::number_ring) = - (2 * x)"
1.62 +lemma mult_minus2_left: "-2 * (x::'a::comm_ring_1) = - (2 * x)"
1.63    by simp
1.64
1.65 -lemma mult_minus2_right: "(x::'a::number_ring) * -2 = - (x * 2)"
1.66 +lemma mult_minus2_right: "(x::'a::comm_ring_1) * -2 = - (x * 2)"
1.67    by simp
1.68
1.69  lemma islin_qf: "islin p \<Longrightarrow> qfree p"
1.70 @@ -3005,11 +3005,11 @@
1.71  *} "parametric QE for linear Arithmetic over fields, Version 2"
1.72
1.73
1.74 -lemma "\<exists>(x::'a::{linordered_field_inverse_zero, number_ring}). y \<noteq> -1 \<longrightarrow> (y + 1)*x < 0"
1.75 -  apply (frpar type: "'a::{linordered_field_inverse_zero, number_ring}" pars: "y::'a::{linordered_field_inverse_zero, number_ring}")
1.76 +lemma "\<exists>(x::'a::{linordered_field_inverse_zero}). y \<noteq> -1 \<longrightarrow> (y + 1)*x < 0"
1.77 +  apply (frpar type: "'a::{linordered_field_inverse_zero}" pars: "y::'a::{linordered_field_inverse_zero}")
1.79    apply (rule spec[where x=y])
1.80 -  apply (frpar type: "'a::{linordered_field_inverse_zero, number_ring}" pars: "z::'a::{linordered_field_inverse_zero, number_ring}")
1.81 +  apply (frpar type: "'a::{linordered_field_inverse_zero}" pars: "z::'a::{linordered_field_inverse_zero}")
1.82    by simp
1.83
1.84  text{* Collins/Jones Problem *}
1.85 @@ -3030,11 +3030,11 @@
1.86  oops
1.87  *)
1.88
1.89 -lemma "\<exists>(x::'a::{linordered_field_inverse_zero, number_ring}). y \<noteq> -1 \<longrightarrow> (y + 1)*x < 0"
1.90 -  apply (frpar2 type: "'a::{linordered_field_inverse_zero, number_ring}" pars: "y::'a::{linordered_field_inverse_zero, number_ring}")
1.91 +lemma "\<exists>(x::'a::{linordered_field_inverse_zero}). y \<noteq> -1 \<longrightarrow> (y + 1)*x < 0"
1.92 +  apply (frpar2 type: "'a::{linordered_field_inverse_zero}" pars: "y::'a::{linordered_field_inverse_zero}")