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.78    apply (simp add: field_simps)
    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}")
    1.93    apply (simp add: field_simps)
    1.94    apply (rule spec[where x=y])
    1.95 -  apply (frpar2 type: "'a::{linordered_field_inverse_zero, number_ring}" pars: "z::'a::{linordered_field_inverse_zero, number_ring}")
    1.96 +  apply (frpar2 type: "'a::{linordered_field_inverse_zero}" pars: "z::'a::{linordered_field_inverse_zero}")
    1.97    by simp
    1.98  
    1.99  text{* Collins/Jones Problem *}