src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
changeset 36409 d323e7773aa8
parent 36348 89c54f51f55a
child 37387 3581483cca6c
     1.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Mon Apr 26 11:34:19 2010 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Mon Apr 26 15:37:50 2010 +0200
     1.3 @@ -27,7 +27,7 @@
     1.4    "tmsize (CNP n c a) = 3 + polysize c + tmsize a "
     1.5  
     1.6    (* Semantics of terms tm *)
     1.7 -consts Itm :: "'a::{ring_char_0,division_ring_inverse_zero,field} list \<Rightarrow> 'a list \<Rightarrow> tm \<Rightarrow> 'a"
     1.8 +consts Itm :: "'a::{field_char_0, field_inverse_zero} list \<Rightarrow> 'a list \<Rightarrow> tm \<Rightarrow> 'a"
     1.9  primrec
    1.10    "Itm vs bs (CP c) = (Ipoly vs c)"
    1.11    "Itm vs bs (Bound n) = bs!n"
    1.12 @@ -270,7 +270,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::{ring_char_0,division_ring_inverse_zero, field})"
    1.17 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
    1.18    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)
    1.19  
    1.20  definition tmneg :: "tm \<Rightarrow> tm" where
    1.21 @@ -296,7 +296,7 @@
    1.22  using tmneg_def by simp
    1.23  lemma [simp]: "isnpoly (C (-1,1))" unfolding isnpoly_def by simp
    1.24  lemma tmneg_allpolys_npoly[simp]: 
    1.25 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero, field})"
    1.26 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
    1.27    shows "allpolys isnpoly t \<Longrightarrow> allpolys isnpoly (tmneg t)" 
    1.28    unfolding tmneg_def by auto
    1.29  
    1.30 @@ -310,7 +310,7 @@
    1.31  lemma tmsub_blt[simp]: "\<lbrakk>tmboundslt n t ; tmboundslt n s\<rbrakk> \<Longrightarrow> tmboundslt n (tmsub t s )"
    1.32  using tmsub_def by simp
    1.33  lemma tmsub_allpolys_npoly[simp]: 
    1.34 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero, field})"
    1.35 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
    1.36    shows "allpolys isnpoly t \<Longrightarrow> allpolys isnpoly s \<Longrightarrow> allpolys isnpoly (tmsub t s)" 
    1.37    unfolding tmsub_def by (simp add: isnpoly_def)
    1.38  
    1.39 @@ -324,8 +324,8 @@
    1.40    "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))"
    1.41  
    1.42  lemma polynate_stupid: 
    1.43 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero, field})"
    1.44 -  shows "polynate t = 0\<^sub>p \<Longrightarrow> Ipoly bs t = (0::'a::{ring_char_0,division_ring_inverse_zero, field})" 
    1.45 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
    1.46 +  shows "polynate t = 0\<^sub>p \<Longrightarrow> Ipoly bs t = (0::'a::{field_char_0, field_inverse_zero})" 
    1.47  apply (subst polynate[symmetric])
    1.48  apply simp
    1.49  done
    1.50 @@ -345,7 +345,7 @@
    1.51  lemma [simp]: "isnpoly 0\<^sub>p" and [simp]: "isnpoly (C(1,1))" 
    1.52    by (simp_all add: isnpoly_def)
    1.53  lemma simptm_allpolys_npoly[simp]: 
    1.54 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero, field})"
    1.55 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
    1.56    shows "allpolys isnpoly (simptm p)"
    1.57    by (induct p rule: simptm.induct, auto simp add: Let_def)
    1.58  
    1.59 @@ -387,7 +387,7 @@
    1.60  qed
    1.61  
    1.62  lemma split0_nb0: 
    1.63 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero, field})"
    1.64 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
    1.65    shows "split0 t = (c',t') \<Longrightarrow>  tmbound 0 t'"
    1.66  proof-
    1.67    fix c' t'
    1.68 @@ -395,7 +395,7 @@
    1.69    with conjunct1[OF split0[where t="t"]] show "tmbound 0 t'" by simp
    1.70  qed
    1.71  
    1.72 -lemma split0_nb0'[simp]:   assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero, field})"
    1.73 +lemma split0_nb0'[simp]:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
    1.74    shows "tmbound0 (snd (split0 t))"
    1.75    using split0_nb0[of t "fst (split0 t)" "snd (split0 t)"] by (simp add: tmbound0_tmbound_iff)
    1.76  
    1.77 @@ -418,7 +418,7 @@
    1.78  lemma allpolys_split0: "allpolys isnpoly p \<Longrightarrow> allpolys isnpoly (snd (split0 p))"
    1.79  by (induct p rule: split0.induct, auto simp  add: isnpoly_def Let_def split_def split0_stupid)
    1.80  
    1.81 -lemma isnpoly_fst_split0:   assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero, field})"
    1.82 +lemma isnpoly_fst_split0:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
    1.83    shows 
    1.84    "allpolys isnpoly p \<Longrightarrow> isnpoly (fst (split0 p))"
    1.85    by (induct p rule: split0.induct, 
    1.86 @@ -447,7 +447,7 @@
    1.87  by (induct p rule: fmsize.induct) simp_all
    1.88  
    1.89    (* Semantics of formulae (fm) *)
    1.90 -consts Ifm ::"'a::{division_ring_inverse_zero,linordered_field} list \<Rightarrow> 'a list \<Rightarrow> fm \<Rightarrow> bool"
    1.91 +consts Ifm ::"'a::{linordered_field_inverse_zero} list \<Rightarrow> 'a list \<Rightarrow> fm \<Rightarrow> bool"
    1.92  primrec
    1.93    "Ifm vs bs T = True"
    1.94    "Ifm vs bs F = False"
    1.95 @@ -969,24 +969,24 @@
    1.96  definition "simpeq t = (let (c,s) = split0 (simptm t) in if c= 0\<^sub>p then eq s else Eq (CNP 0 c s))"
    1.97  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.98  
    1.99 -lemma simplt_islin[simp]:   assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
   1.100 +lemma simplt_islin[simp]:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.101    shows "islin (simplt t)"
   1.102    unfolding simplt_def 
   1.103    using split0_nb0'
   1.104  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])
   1.105    
   1.106 -lemma simple_islin[simp]:   assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
   1.107 +lemma simple_islin[simp]:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.108    shows "islin (simple t)"
   1.109    unfolding simple_def 
   1.110    using split0_nb0'
   1.111  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)
   1.112 -lemma simpeq_islin[simp]:   assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
   1.113 +lemma simpeq_islin[simp]:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.114    shows "islin (simpeq t)"
   1.115    unfolding simpeq_def 
   1.116    using split0_nb0'
   1.117  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)
   1.118  
   1.119 -lemma simpneq_islin[simp]:   assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
   1.120 +lemma simpneq_islin[simp]:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.121    shows "islin (simpneq t)"
   1.122    unfolding simpneq_def 
   1.123    using split0_nb0'
   1.124 @@ -994,7 +994,7 @@
   1.125  
   1.126  lemma really_stupid: "\<not> (\<forall>c1 s'. (c1, s') \<noteq> split0 s)"
   1.127    by (cases "split0 s", auto)
   1.128 -lemma split0_npoly:   assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
   1.129 +lemma split0_npoly:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.130    and n: "allpolys isnpoly t"
   1.131    shows "isnpoly (fst (split0 t))" and "allpolys isnpoly (snd (split0 t))"
   1.132    using n
   1.133 @@ -1083,7 +1083,7 @@
   1.134    apply (case_tac poly, auto)
   1.135    done
   1.136  
   1.137 -lemma simplt_nb[simp]:   assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
   1.138 +lemma simplt_nb[simp]:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.139    shows "tmbound0 t \<Longrightarrow> bound0 (simplt t)"
   1.140    using split0 [of "simptm t" vs bs]
   1.141  proof(simp add: simplt_def Let_def split_def)
   1.142 @@ -1100,7 +1100,7 @@
   1.143         fst (split0 (simptm t)) = 0\<^sub>p" by (simp add: simplt_def Let_def split_def lt_nb)
   1.144  qed
   1.145  
   1.146 -lemma simple_nb[simp]:   assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
   1.147 +lemma simple_nb[simp]:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.148    shows "tmbound0 t \<Longrightarrow> bound0 (simple t)"
   1.149    using split0 [of "simptm t" vs bs]
   1.150  proof(simp add: simple_def Let_def split_def)
   1.151 @@ -1117,7 +1117,7 @@
   1.152         fst (split0 (simptm t)) = 0\<^sub>p" by (simp add: simplt_def Let_def split_def le_nb)
   1.153  qed
   1.154  
   1.155 -lemma simpeq_nb[simp]:   assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
   1.156 +lemma simpeq_nb[simp]:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.157    shows "tmbound0 t \<Longrightarrow> bound0 (simpeq t)"
   1.158    using split0 [of "simptm t" vs bs]
   1.159  proof(simp add: simpeq_def Let_def split_def)
   1.160 @@ -1134,7 +1134,7 @@
   1.161         fst (split0 (simptm t)) = 0\<^sub>p" by (simp add: simpeq_def Let_def split_def eq_nb)
   1.162  qed
   1.163  
   1.164 -lemma simpneq_nb[simp]:   assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
   1.165 +lemma simpneq_nb[simp]:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.166    shows "tmbound0 t \<Longrightarrow> bound0 (simpneq t)"
   1.167    using split0 [of "simptm t" vs bs]
   1.168  proof(simp add: simpneq_def Let_def split_def)
   1.169 @@ -1267,7 +1267,7 @@
   1.170  lemma simpfm[simp]: "Ifm vs bs (simpfm p) = Ifm vs bs p"
   1.171  by(induct p arbitrary: bs rule: simpfm.induct, auto)
   1.172  
   1.173 -lemma simpfm_bound0:   assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
   1.174 +lemma simpfm_bound0:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.175    shows "bound0 p \<Longrightarrow> bound0 (simpfm p)"
   1.176  by (induct p rule: simpfm.induct, auto)
   1.177  
   1.178 @@ -1296,7 +1296,7 @@
   1.179  lemma disj_lin: "islin p \<Longrightarrow> islin q \<Longrightarrow> islin (disj p q)" by (simp add: disj_def)
   1.180  lemma conj_lin: "islin p \<Longrightarrow> islin q \<Longrightarrow> islin (conj p q)" by (simp add: conj_def)
   1.181  
   1.182 -lemma   assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
   1.183 +lemma   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.184    shows "qfree p \<Longrightarrow> islin (simpfm p)" 
   1.185    apply (induct p rule: simpfm.induct)
   1.186    apply (simp_all add: conj_lin disj_lin)
   1.187 @@ -2519,7 +2519,7 @@
   1.188  lemma remdps_set[simp]: "set (remdps xs) = set xs"
   1.189    by (induct xs rule: remdps.induct, auto)
   1.190  
   1.191 -lemma simpfm_lin:   assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
   1.192 +lemma simpfm_lin:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   1.193    shows "qfree p \<Longrightarrow> islin (simpfm p)"
   1.194    by (induct p rule: simpfm.induct, auto simp add: conj_lin disj_lin)
   1.195  
   1.196 @@ -2747,12 +2747,12 @@
   1.197  using lp tnb
   1.198  by (induct p c t rule: msubstpos.induct, auto simp add: msubsteq2_nb msubstltpos_nb msubstlepos_nb)
   1.199  
   1.200 -lemma msubstneg_nb: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})" and lp: "islin p" and tnb: "tmbound0 t"
   1.201 +lemma msubstneg_nb: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" and lp: "islin p" and tnb: "tmbound0 t"
   1.202    shows "bound0 (msubstneg p c t)"
   1.203  using lp tnb
   1.204  by (induct p c t rule: msubstneg.induct, auto simp add: msubsteq2_nb msubstltneg_nb msubstleneg_nb)
   1.205  
   1.206 -lemma msubst2_nb: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})" and lp: "islin p" and tnb: "tmbound0 t"
   1.207 +lemma msubst2_nb: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" and lp: "islin p" and tnb: "tmbound0 t"
   1.208    shows "bound0 (msubst2 p c t)"
   1.209  using lp tnb
   1.210  by (simp add: msubst2_def msubstneg_nb msubstpos_nb conj_nb disj_nb lt_nb simpfm_bound0)
   1.211 @@ -3156,54 +3156,54 @@
   1.212  *} "Parametric QE for linear Arithmetic over fields, Version 2"
   1.213  
   1.214  
   1.215 -lemma "\<exists>(x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). y \<noteq> -1 \<longrightarrow> (y + 1)*x < 0"
   1.216 -  apply (frpar type: "'a::{linordered_field, division_ring_inverse_zero, number_ring}" pars: "y::'a::{linordered_field, division_ring_inverse_zero, number_ring}")
   1.217 +lemma "\<exists>(x::'a::{linordered_field_inverse_zero, number_ring}). y \<noteq> -1 \<longrightarrow> (y + 1)*x < 0"
   1.218 +  apply (frpar type: "'a::{linordered_field_inverse_zero, number_ring}" pars: "y::'a::{linordered_field_inverse_zero, number_ring}")
   1.219    apply (simp add: field_simps)
   1.220    apply (rule spec[where x=y])
   1.221 -  apply (frpar type: "'a::{linordered_field, division_ring_inverse_zero, number_ring}" pars: "z::'a::{linordered_field, division_ring_inverse_zero, number_ring}")
   1.222 +  apply (frpar type: "'a::{linordered_field_inverse_zero, number_ring}" pars: "z::'a::{linordered_field_inverse_zero, number_ring}")
   1.223    by simp
   1.224  
   1.225  text{* Collins/Jones Problem *}
   1.226  (*
   1.227 -lemma "\<exists>(r::'a::{linordered_field, division_ring_inverse_zero, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0"
   1.228 +lemma "\<exists>(r::'a::{linordered_field_inverse_zero, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0"
   1.229  proof-
   1.230 -  have "(\<exists>(r::'a::{linordered_field, division_ring_inverse_zero, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0) \<longleftrightarrow> (\<exists>(r::'a::{linordered_field, division_ring_inverse_zero, number_ring}). 0 < r \<and> r < 1 \<and> 0 < 2 *(a^2 + b^2) - (3*(a^2 + b^2)) * r + (2*a)*r \<and> 2*(a^2 + b^2) - (3*(a^2 + b^2) - 4*a + 1)*r - 2*a < 0)" (is "?lhs \<longleftrightarrow> ?rhs")
   1.231 +  have "(\<exists>(r::'a::{linordered_field_inverse_zero, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0) \<longleftrightarrow> (\<exists>(r::'a::{linordered_field_inverse_zero, number_ring}). 0 < r \<and> r < 1 \<and> 0 < 2 *(a^2 + b^2) - (3*(a^2 + b^2)) * r + (2*a)*r \<and> 2*(a^2 + b^2) - (3*(a^2 + b^2) - 4*a + 1)*r - 2*a < 0)" (is "?lhs \<longleftrightarrow> ?rhs")
   1.232  by (simp add: field_simps)
   1.233  have "?rhs"
   1.234  
   1.235 -  apply (frpar type: "'a::{linordered_field, division_ring_inverse_zero, number_ring}" pars: "a::'a::{linordered_field, division_ring_inverse_zero, number_ring}" "b::'a::{linordered_field, division_ring_inverse_zero, number_ring}")
   1.236 +  apply (frpar type: "'a::{linordered_field_inverse_zero, number_ring}" pars: "a::'a::{linordered_field_inverse_zero, number_ring}" "b::'a::{linordered_field_inverse_zero, number_ring}")
   1.237    apply (simp add: field_simps)
   1.238  oops
   1.239  *)
   1.240  (*
   1.241 -lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. (1 - t)*x \<le> (1+t)*y \<and> (1 - t)*y \<le> (1+t)*x --> 0 \<le> y"
   1.242 -apply (frpar type: "'a::{linordered_field, division_ring_inverse_zero, number_ring}" pars: "t::'a::{linordered_field, division_ring_inverse_zero, number_ring}")
   1.243 +lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}) y. (1 - t)*x \<le> (1+t)*y \<and> (1 - t)*y \<le> (1+t)*x --> 0 \<le> y"
   1.244 +apply (frpar type: "'a::{linordered_field_inverse_zero, number_ring}" pars: "t::'a::{linordered_field_inverse_zero, number_ring}")
   1.245  oops
   1.246  *)
   1.247  
   1.248 -lemma "\<exists>(x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). y \<noteq> -1 \<longrightarrow> (y + 1)*x < 0"
   1.249 -  apply (frpar2 type: "'a::{linordered_field, division_ring_inverse_zero, number_ring}" pars: "y::'a::{linordered_field, division_ring_inverse_zero, number_ring}")
   1.250 +lemma "\<exists>(x::'a::{linordered_field_inverse_zero, number_ring}). y \<noteq> -1 \<longrightarrow> (y + 1)*x < 0"
   1.251 +  apply (frpar2 type: "'a::{linordered_field_inverse_zero, number_ring}" pars: "y::'a::{linordered_field_inverse_zero, number_ring}")
   1.252    apply (simp add: field_simps)
   1.253    apply (rule spec[where x=y])
   1.254 -  apply (frpar2 type: "'a::{linordered_field, division_ring_inverse_zero, number_ring}" pars: "z::'a::{linordered_field, division_ring_inverse_zero, number_ring}")
   1.255 +  apply (frpar2 type: "'a::{linordered_field_inverse_zero, number_ring}" pars: "z::'a::{linordered_field_inverse_zero, number_ring}")
   1.256    by simp
   1.257  
   1.258  text{* Collins/Jones Problem *}
   1.259  
   1.260  (*
   1.261 -lemma "\<exists>(r::'a::{linordered_field, division_ring_inverse_zero, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0"
   1.262 +lemma "\<exists>(r::'a::{linordered_field_inverse_zero, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0"
   1.263  proof-
   1.264 -  have "(\<exists>(r::'a::{linordered_field, division_ring_inverse_zero, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0) \<longleftrightarrow> (\<exists>(r::'a::{linordered_field, division_ring_inverse_zero, number_ring}). 0 < r \<and> r < 1 \<and> 0 < 2 *(a^2 + b^2) - (3*(a^2 + b^2)) * r + (2*a)*r \<and> 2*(a^2 + b^2) - (3*(a^2 + b^2) - 4*a + 1)*r - 2*a < 0)" (is "?lhs \<longleftrightarrow> ?rhs")
   1.265 +  have "(\<exists>(r::'a::{linordered_field_inverse_zero, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0) \<longleftrightarrow> (\<exists>(r::'a::{linordered_field_inverse_zero, number_ring}). 0 < r \<and> r < 1 \<and> 0 < 2 *(a^2 + b^2) - (3*(a^2 + b^2)) * r + (2*a)*r \<and> 2*(a^2 + b^2) - (3*(a^2 + b^2) - 4*a + 1)*r - 2*a < 0)" (is "?lhs \<longleftrightarrow> ?rhs")
   1.266  by (simp add: field_simps)
   1.267  have "?rhs"
   1.268 -  apply (frpar2 type: "'a::{linordered_field, division_ring_inverse_zero, number_ring}" pars: "a::'a::{linordered_field, division_ring_inverse_zero, number_ring}" "b::'a::{linordered_field, division_ring_inverse_zero, number_ring}")
   1.269 +  apply (frpar2 type: "'a::{linordered_field_inverse_zero, number_ring}" pars: "a::'a::{linordered_field_inverse_zero, number_ring}" "b::'a::{linordered_field_inverse_zero, number_ring}")
   1.270    apply simp
   1.271  oops
   1.272  *)
   1.273  
   1.274  (*
   1.275 -lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. (1 - t)*x \<le> (1+t)*y \<and> (1 - t)*y \<le> (1+t)*x --> 0 \<le> y"
   1.276 -apply (frpar2 type: "'a::{linordered_field, division_ring_inverse_zero, number_ring}" pars: "t::'a::{linordered_field, division_ring_inverse_zero, number_ring}")
   1.277 +lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}) y. (1 - t)*x \<le> (1+t)*y \<and> (1 - t)*y \<le> (1+t)*x --> 0 \<le> y"
   1.278 +apply (frpar2 type: "'a::{linordered_field_inverse_zero, number_ring}" pars: "t::'a::{linordered_field_inverse_zero, number_ring}")
   1.279  apply (simp add: field_simps linorder_neq_iff[symmetric])
   1.280  apply ferrack
   1.281  oops