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