--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Mon Apr 26 11:34:15 2010 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Mon Apr 26 11:34:15 2010 +0200
@@ -27,7 +27,7 @@
"tmsize (CNP n c a) = 3 + polysize c + tmsize a "
(* Semantics of terms tm *)
-consts Itm :: "'a::{ring_char_0,division_by_zero,field} list \<Rightarrow> 'a list \<Rightarrow> tm \<Rightarrow> 'a"
+consts Itm :: "'a::{ring_char_0,division_ring_inverse_zero,field} list \<Rightarrow> 'a list \<Rightarrow> tm \<Rightarrow> 'a"
primrec
"Itm vs bs (CP c) = (Ipoly vs c)"
"Itm vs bs (Bound n) = bs!n"
@@ -239,7 +239,7 @@
lemma tmadd[simp]: "Itm vs bs (tmadd (t,s)) = Itm vs bs (Add t s)"
apply (induct t s rule: tmadd.induct, simp_all add: Let_def)
apply (case_tac "c1 +\<^sub>p c2 = 0\<^sub>p",case_tac "n1 \<le> n2", simp_all)
-apply (case_tac "n1 = n2", simp_all add: ring_simps)
+apply (case_tac "n1 = n2", simp_all add: field_simps)
apply (simp only: right_distrib[symmetric])
by (auto simp del: polyadd simp add: polyadd[symmetric])
@@ -259,7 +259,7 @@
"tmmul t = (\<lambda> i. Mul i t)"
lemma tmmul[simp]: "Itm vs bs (tmmul t i) = Itm vs bs (Mul i t)"
-by (induct t arbitrary: i rule: tmmul.induct, simp_all add: ring_simps)
+by (induct t arbitrary: i rule: tmmul.induct, simp_all add: field_simps)
lemma tmmul_nb0[simp]: "tmbound0 t \<Longrightarrow> tmbound0 (tmmul t i)"
by (induct t arbitrary: i rule: tmmul.induct, auto )
@@ -270,7 +270,7 @@
by (induct t arbitrary: i rule: tmmul.induct, auto simp add: Let_def)
lemma tmmul_allpolys_npoly[simp]:
- assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero, field})"
+ assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero, field})"
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)
definition tmneg :: "tm \<Rightarrow> tm" where
@@ -296,7 +296,7 @@
using tmneg_def by simp
lemma [simp]: "isnpoly (C (-1,1))" unfolding isnpoly_def by simp
lemma tmneg_allpolys_npoly[simp]:
- assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero, field})"
+ assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero, field})"
shows "allpolys isnpoly t \<Longrightarrow> allpolys isnpoly (tmneg t)"
unfolding tmneg_def by auto
@@ -310,7 +310,7 @@
lemma tmsub_blt[simp]: "\<lbrakk>tmboundslt n t ; tmboundslt n s\<rbrakk> \<Longrightarrow> tmboundslt n (tmsub t s )"
using tmsub_def by simp
lemma tmsub_allpolys_npoly[simp]:
- assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero, field})"
+ assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero, field})"
shows "allpolys isnpoly t \<Longrightarrow> allpolys isnpoly s \<Longrightarrow> allpolys isnpoly (tmsub t s)"
unfolding tmsub_def by (simp add: isnpoly_def)
@@ -324,8 +324,8 @@
"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))"
lemma polynate_stupid:
- assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero, field})"
- shows "polynate t = 0\<^sub>p \<Longrightarrow> Ipoly bs t = (0::'a::{ring_char_0,division_by_zero, field})"
+ assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero, field})"
+ shows "polynate t = 0\<^sub>p \<Longrightarrow> Ipoly bs t = (0::'a::{ring_char_0,division_ring_inverse_zero, field})"
apply (subst polynate[symmetric])
apply simp
done
@@ -345,7 +345,7 @@
lemma [simp]: "isnpoly 0\<^sub>p" and [simp]: "isnpoly (C(1,1))"
by (simp_all add: isnpoly_def)
lemma simptm_allpolys_npoly[simp]:
- assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero, field})"
+ assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero, field})"
shows "allpolys isnpoly (simptm p)"
by (induct p rule: simptm.induct, auto simp add: Let_def)
@@ -369,14 +369,14 @@
"tmbound 0 (snd (split0 t)) \<and> (Itm vs bs (CNP 0 (fst (split0 t)) (snd (split0 t))) = Itm vs bs t)"
apply (induct t rule: split0.induct)
apply simp
- apply (simp add: Let_def split_def ring_simps)
- apply (simp add: Let_def split_def ring_simps)
- apply (simp add: Let_def split_def ring_simps)
- apply (simp add: Let_def split_def ring_simps)
- apply (simp add: Let_def split_def ring_simps)
+ apply (simp add: Let_def split_def field_simps)
+ apply (simp add: Let_def split_def field_simps)
+ apply (simp add: Let_def split_def field_simps)
+ apply (simp add: Let_def split_def field_simps)
+ apply (simp add: Let_def split_def field_simps)
apply (simp add: Let_def split_def mult_assoc right_distrib[symmetric])
- apply (simp add: Let_def split_def ring_simps)
- apply (simp add: Let_def split_def ring_simps)
+ apply (simp add: Let_def split_def field_simps)
+ apply (simp add: Let_def split_def field_simps)
done
lemma split0_ci: "split0 t = (c',t') \<Longrightarrow> Itm vs bs t = Itm vs bs (CNP 0 c' t')"
@@ -387,7 +387,7 @@
qed
lemma split0_nb0:
- assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero, field})"
+ assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero, field})"
shows "split0 t = (c',t') \<Longrightarrow> tmbound 0 t'"
proof-
fix c' t'
@@ -395,7 +395,7 @@
with conjunct1[OF split0[where t="t"]] show "tmbound 0 t'" by simp
qed
-lemma split0_nb0'[simp]: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero, field})"
+lemma split0_nb0'[simp]: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero, field})"
shows "tmbound0 (snd (split0 t))"
using split0_nb0[of t "fst (split0 t)" "snd (split0 t)"] by (simp add: tmbound0_tmbound_iff)
@@ -418,7 +418,7 @@
lemma allpolys_split0: "allpolys isnpoly p \<Longrightarrow> allpolys isnpoly (snd (split0 p))"
by (induct p rule: split0.induct, auto simp add: isnpoly_def Let_def split_def split0_stupid)
-lemma isnpoly_fst_split0: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero, field})"
+lemma isnpoly_fst_split0: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero, field})"
shows
"allpolys isnpoly p \<Longrightarrow> isnpoly (fst (split0 p))"
by (induct p rule: split0.induct,
@@ -447,7 +447,7 @@
by (induct p rule: fmsize.induct) simp_all
(* Semantics of formulae (fm) *)
-consts Ifm ::"'a::{division_by_zero,linordered_field} list \<Rightarrow> 'a list \<Rightarrow> fm \<Rightarrow> bool"
+consts Ifm ::"'a::{division_ring_inverse_zero,linordered_field} list \<Rightarrow> 'a list \<Rightarrow> fm \<Rightarrow> bool"
primrec
"Ifm vs bs T = True"
"Ifm vs bs F = False"
@@ -969,24 +969,24 @@
definition "simpeq t = (let (c,s) = split0 (simptm t) in if c= 0\<^sub>p then eq s else Eq (CNP 0 c s))"
definition "simpneq t = (let (c,s) = split0 (simptm t) in if c= 0\<^sub>p then neq s else NEq (CNP 0 c s))"
-lemma simplt_islin[simp]: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
+lemma simplt_islin[simp]: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
shows "islin (simplt t)"
unfolding simplt_def
using split0_nb0'
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])
-lemma simple_islin[simp]: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
+lemma simple_islin[simp]: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
shows "islin (simple t)"
unfolding simple_def
using split0_nb0'
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)
-lemma simpeq_islin[simp]: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
+lemma simpeq_islin[simp]: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
shows "islin (simpeq t)"
unfolding simpeq_def
using split0_nb0'
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)
-lemma simpneq_islin[simp]: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
+lemma simpneq_islin[simp]: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
shows "islin (simpneq t)"
unfolding simpneq_def
using split0_nb0'
@@ -994,7 +994,7 @@
lemma really_stupid: "\<not> (\<forall>c1 s'. (c1, s') \<noteq> split0 s)"
by (cases "split0 s", auto)
-lemma split0_npoly: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
+lemma split0_npoly: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
and n: "allpolys isnpoly t"
shows "isnpoly (fst (split0 t))" and "allpolys isnpoly (snd (split0 t))"
using n
@@ -1083,7 +1083,7 @@
apply (case_tac poly, auto)
done
-lemma simplt_nb[simp]: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
+lemma simplt_nb[simp]: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
shows "tmbound0 t \<Longrightarrow> bound0 (simplt t)"
using split0 [of "simptm t" vs bs]
proof(simp add: simplt_def Let_def split_def)
@@ -1100,7 +1100,7 @@
fst (split0 (simptm t)) = 0\<^sub>p" by (simp add: simplt_def Let_def split_def lt_nb)
qed
-lemma simple_nb[simp]: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
+lemma simple_nb[simp]: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
shows "tmbound0 t \<Longrightarrow> bound0 (simple t)"
using split0 [of "simptm t" vs bs]
proof(simp add: simple_def Let_def split_def)
@@ -1117,7 +1117,7 @@
fst (split0 (simptm t)) = 0\<^sub>p" by (simp add: simplt_def Let_def split_def le_nb)
qed
-lemma simpeq_nb[simp]: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
+lemma simpeq_nb[simp]: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
shows "tmbound0 t \<Longrightarrow> bound0 (simpeq t)"
using split0 [of "simptm t" vs bs]
proof(simp add: simpeq_def Let_def split_def)
@@ -1134,7 +1134,7 @@
fst (split0 (simptm t)) = 0\<^sub>p" by (simp add: simpeq_def Let_def split_def eq_nb)
qed
-lemma simpneq_nb[simp]: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
+lemma simpneq_nb[simp]: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
shows "tmbound0 t \<Longrightarrow> bound0 (simpneq t)"
using split0 [of "simptm t" vs bs]
proof(simp add: simpneq_def Let_def split_def)
@@ -1267,7 +1267,7 @@
lemma simpfm[simp]: "Ifm vs bs (simpfm p) = Ifm vs bs p"
by(induct p arbitrary: bs rule: simpfm.induct, auto)
-lemma simpfm_bound0: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
+lemma simpfm_bound0: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
shows "bound0 p \<Longrightarrow> bound0 (simpfm p)"
by (induct p rule: simpfm.induct, auto)
@@ -1296,7 +1296,7 @@
lemma disj_lin: "islin p \<Longrightarrow> islin q \<Longrightarrow> islin (disj p q)" by (simp add: disj_def)
lemma conj_lin: "islin p \<Longrightarrow> islin q \<Longrightarrow> islin (conj p q)" by (simp add: conj_def)
-lemma assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
+lemma assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
shows "qfree p \<Longrightarrow> islin (simpfm p)"
apply (induct p rule: simpfm.induct)
apply (simp_all add: conj_lin disj_lin)
@@ -1698,11 +1698,11 @@
{assume c: "?N c > 0"
from px pos_less_divide_eq[OF c, where a="x" and b="-?Nt x s"]
have px': "x < - ?Nt x s / ?N c"
- by (auto simp add: not_less ring_simps)
+ by (auto simp add: not_less field_simps)
{assume y: "y < - ?Nt x s / ?N c"
hence "y * ?N c < - ?Nt x s"
by (simp add: pos_less_divide_eq[OF c, where a="y" and b="-?Nt x s", symmetric])
- hence "?N c * y + ?Nt x s < 0" by (simp add: ring_simps)
+ hence "?N c * y + ?Nt x s < 0" by (simp add: field_simps)
hence ?case using tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"] by simp}
moreover
{assume y: "y > -?Nt x s / ?N c"
@@ -1715,11 +1715,11 @@
{assume c: "?N c < 0"
from px neg_divide_less_eq[OF c, where a="x" and b="-?Nt x s"]
have px': "x > - ?Nt x s / ?N c"
- by (auto simp add: not_less ring_simps)
+ by (auto simp add: not_less field_simps)
{assume y: "y > - ?Nt x s / ?N c"
hence "y * ?N c < - ?Nt x s"
by (simp add: neg_divide_less_eq[OF c, where a="y" and b="-?Nt x s", symmetric])
- hence "?N c * y + ?Nt x s < 0" by (simp add: ring_simps)
+ hence "?N c * y + ?Nt x s < 0" by (simp add: field_simps)
hence ?case using tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"] by simp}
moreover
{assume y: "y < -?Nt x s / ?N c"
@@ -1743,11 +1743,11 @@
moreover
{assume c: "?N c > 0"
from px pos_le_divide_eq[OF c, where a="x" and b="-?Nt x s"]
- have px': "x <= - ?Nt x s / ?N c" by (simp add: not_less ring_simps)
+ have px': "x <= - ?Nt x s / ?N c" by (simp add: not_less field_simps)
{assume y: "y < - ?Nt x s / ?N c"
hence "y * ?N c < - ?Nt x s"
by (simp add: pos_less_divide_eq[OF c, where a="y" and b="-?Nt x s", symmetric])
- hence "?N c * y + ?Nt x s < 0" by (simp add: ring_simps)
+ hence "?N c * y + ?Nt x s < 0" by (simp add: field_simps)
hence ?case using tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"] by simp}
moreover
{assume y: "y > -?Nt x s / ?N c"
@@ -1759,11 +1759,11 @@
moreover
{assume c: "?N c < 0"
from px neg_divide_le_eq[OF c, where a="x" and b="-?Nt x s"]
- have px': "x >= - ?Nt x s / ?N c" by (simp add: ring_simps)
+ have px': "x >= - ?Nt x s / ?N c" by (simp add: field_simps)
{assume y: "y > - ?Nt x s / ?N c"
hence "y * ?N c < - ?Nt x s"
by (simp add: neg_divide_less_eq[OF c, where a="y" and b="-?Nt x s", symmetric])
- hence "?N c * y + ?Nt x s < 0" by (simp add: ring_simps)
+ hence "?N c * y + ?Nt x s < 0" by (simp add: field_simps)
hence ?case using tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"] by simp}
moreover
{assume y: "y < -?Nt x s / ?N c"
@@ -1787,7 +1787,7 @@
moreover
{assume c: "?N c > 0" hence cnz: "?N c \<noteq> 0" by simp
from px eq_divide_eq[of "x" "-?Nt x s" "?N c"] cnz
- have px': "x = - ?Nt x s / ?N c" by (simp add: ring_simps)
+ have px': "x = - ?Nt x s / ?N c" by (simp add: field_simps)
{assume y: "y < -?Nt x s / ?N c"
with ly have eu: "l < - ?Nt x s / ?N c" by auto
with noS ly yu have th: "- ?Nt x s / ?N c \<ge> u" by (cases "- ?Nt x s / ?N c < u", auto)
@@ -1802,7 +1802,7 @@
moreover
{assume c: "?N c < 0" hence cnz: "?N c \<noteq> 0" by simp
from px eq_divide_eq[of "x" "-?Nt x s" "?N c"] cnz
- have px': "x = - ?Nt x s / ?N c" by (simp add: ring_simps)
+ have px': "x = - ?Nt x s / ?N c" by (simp add: field_simps)
{assume y: "y < -?Nt x s / ?N c"
with ly have eu: "l < - ?Nt x s / ?N c" by auto
with noS ly yu have th: "- ?Nt x s / ?N c \<ge> u" by (cases "- ?Nt x s / ?N c < u", auto)
@@ -1829,7 +1829,7 @@
moreover
{assume c: "?N c \<noteq> 0"
from yne c eq_divide_eq[of "y" "- ?Nt x s" "?N c"] have ?case
- by (simp add: ring_simps tmbound0_I[OF lin(3), of vs x bs y] sum_eq[symmetric]) }
+ by (simp add: field_simps tmbound0_I[OF lin(3), of vs x bs y] sum_eq[symmetric]) }
ultimately show ?case by blast
qed (auto simp add: nth_pos2 tmbound0_I[where vs=vs and bs="bs" and b="y" and b'="x"] bound0_I[where vs=vs and bs="bs" and b="y" and b'="x"])
@@ -1844,7 +1844,7 @@
lemma half_sum_eq: "(u + u) / (1+1) = (u::'a::{linordered_field})"
proof-
- have "(u + u) = (1 + 1) * u" by (simp add: ring_simps)
+ have "(u + u) = (1 + 1) * u" by (simp add: field_simps)
hence "(u + u) / (1+1) = (1 + 1)*u / (1 + 1)" by simp
with nonzero_mult_divide_cancel_left[OF one_plus_one_nonzero, of u] show ?thesis by simp
qed
@@ -1987,7 +1987,7 @@
also have "\<dots> \<longleftrightarrow> (1 + 1)*?d * (?a * (-?s / ((1 + 1)*?d)) + ?r) = 0"
using d mult_cancel_left[of "(1 + 1)*?d" "(?a * (-?s / ((1 + 1)*?d)) + ?r)" 0] by simp
also have "\<dots> \<longleftrightarrow> (- ?a * ?s) * ((1 + 1)*?d / ((1 + 1)*?d)) + (1 + 1)*?d*?r= 0"
- by (simp add: ring_simps right_distrib[of "(1 + 1)*?d"] del: right_distrib)
+ by (simp add: field_simps right_distrib[of "(1 + 1)*?d"] del: right_distrib)
also have "\<dots> \<longleftrightarrow> - (?a * ?s) + (1 + 1)*?d*?r = 0" using d by simp
finally have ?thesis using c d
@@ -2003,7 +2003,7 @@
also have "\<dots> \<longleftrightarrow> (1 + 1)*?c * (?a * (-?t / ((1 + 1)*?c)) + ?r) = 0"
using c mult_cancel_left[of "(1 + 1)*?c" "(?a * (-?t / ((1 + 1)*?c)) + ?r)" 0] by simp
also have "\<dots> \<longleftrightarrow> (?a * -?t)* ((1 + 1)*?c) / ((1 + 1)*?c) + (1 + 1)*?c*?r= 0"
- by (simp add: ring_simps right_distrib[of "(1 + 1)*?c"] del: right_distrib)
+ by (simp add: field_simps right_distrib[of "(1 + 1)*?c"] del: right_distrib)
also have "\<dots> \<longleftrightarrow> - (?a * ?t) + (1 + 1)*?c*?r = 0" using c by simp
finally have ?thesis using c d
apply (simp add: r[of "- (?t/ ((1 + 1)*?c))"] msubsteq_def Let_def evaldjf_ex del: one_add_one_is_two)
@@ -2014,19 +2014,19 @@
{assume c: "?c \<noteq> 0" and d: "?d\<noteq>0" hence dc: "?c * ?d *(1 + 1) \<noteq> 0" by simp
from add_frac_eq[OF c d, of "- ?t" "- ?s"]
have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d)"
- by (simp add: ring_simps)
+ by (simp add: field_simps)
have "?rhs \<longleftrightarrow> Ifm vs (- (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d) # bs) (Eq (CNP 0 a r))" by (simp only: th)
also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d)) + ?r = 0"
by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / ((1 + 1) * ?c * ?d)"])
also have "\<dots> \<longleftrightarrow> ((1 + 1) * ?c * ?d) * (?a * (- (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d)) + ?r) =0 "
using c d mult_cancel_left[of "(1 + 1) * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ ((1 + 1)*?c*?d)) + ?r" 0] by simp
also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + (1 + 1)*?c*?d*?r =0"
- using nonzero_mult_divide_cancel_left[OF dc] c d
- by (simp add: ring_simps diff_divide_distrib del: left_distrib)
+ using nonzero_mult_divide_cancel_left [OF dc] c d
+ by (simp add: algebra_simps diff_divide_distrib del: left_distrib)
finally have ?thesis using c d
- apply (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / ((1 + 1) * ?c * ?d)"] msubsteq_def Let_def evaldjf_ex ring_simps)
+ apply (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / ((1 + 1) * ?c * ?d)"] msubsteq_def Let_def evaldjf_ex field_simps)
apply (simp only: one_add_one_is_two[symmetric] of_int_add)
- apply (simp add: ring_simps)
+ apply (simp add: field_simps)
done }
ultimately show ?thesis by blast
qed
@@ -2075,7 +2075,7 @@
also have "\<dots> \<longleftrightarrow> (1 + 1)*?d * (?a * (-?s / ((1 + 1)*?d)) + ?r) \<noteq> 0"
using d mult_cancel_left[of "(1 + 1)*?d" "(?a * (-?s / ((1 + 1)*?d)) + ?r)" 0] by simp
also have "\<dots> \<longleftrightarrow> (- ?a * ?s) * ((1 + 1)*?d / ((1 + 1)*?d)) + (1 + 1)*?d*?r\<noteq> 0"
- by (simp add: ring_simps right_distrib[of "(1 + 1)*?d"] del: right_distrib)
+ by (simp add: field_simps right_distrib[of "(1 + 1)*?d"] del: right_distrib)
also have "\<dots> \<longleftrightarrow> - (?a * ?s) + (1 + 1)*?d*?r \<noteq> 0" using d by simp
finally have ?thesis using c d
@@ -2091,7 +2091,7 @@
also have "\<dots> \<longleftrightarrow> (1 + 1)*?c * (?a * (-?t / ((1 + 1)*?c)) + ?r) \<noteq> 0"
using c mult_cancel_left[of "(1 + 1)*?c" "(?a * (-?t / ((1 + 1)*?c)) + ?r)" 0] by simp
also have "\<dots> \<longleftrightarrow> (?a * -?t)* ((1 + 1)*?c) / ((1 + 1)*?c) + (1 + 1)*?c*?r \<noteq> 0"
- by (simp add: ring_simps right_distrib[of "(1 + 1)*?c"] del: right_distrib)
+ by (simp add: field_simps right_distrib[of "(1 + 1)*?c"] del: right_distrib)
also have "\<dots> \<longleftrightarrow> - (?a * ?t) + (1 + 1)*?c*?r \<noteq> 0" using c by simp
finally have ?thesis using c d
apply (simp add: r[of "- (?t/ ((1 + 1)*?c))"] msubstneq_def Let_def evaldjf_ex del: one_add_one_is_two)
@@ -2102,7 +2102,7 @@
{assume c: "?c \<noteq> 0" and d: "?d\<noteq>0" hence dc: "?c * ?d *(1 + 1) \<noteq> 0" by simp
from add_frac_eq[OF c d, of "- ?t" "- ?s"]
have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d)"
- by (simp add: ring_simps)
+ by (simp add: field_simps)
have "?rhs \<longleftrightarrow> Ifm vs (- (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d) # bs) (NEq (CNP 0 a r))" by (simp only: th)
also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d)) + ?r \<noteq> 0"
by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / ((1 + 1) * ?c * ?d)"])
@@ -2110,11 +2110,11 @@
using c d mult_cancel_left[of "(1 + 1) * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ ((1 + 1)*?c*?d)) + ?r" 0] by simp
also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + (1 + 1)*?c*?d*?r \<noteq> 0"
using nonzero_mult_divide_cancel_left[OF dc] c d
- by (simp add: ring_simps diff_divide_distrib del: left_distrib)
+ by (simp add: algebra_simps diff_divide_distrib del: left_distrib)
finally have ?thesis using c d
- apply (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / ((1 + 1) * ?c * ?d)"] msubstneq_def Let_def evaldjf_ex ring_simps)
+ apply (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / ((1 + 1) * ?c * ?d)"] msubstneq_def Let_def evaldjf_ex field_simps)
apply (simp only: one_add_one_is_two[symmetric] of_int_add)
- apply (simp add: ring_simps)
+ apply (simp add: field_simps)
done }
ultimately show ?thesis by blast
qed
@@ -2169,7 +2169,7 @@
from dc' have dc'': "\<not> (1 + 1)*?c *?d < 0" by simp
from add_frac_eq[OF c d, of "- ?t" "- ?s"]
have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d)"
- by (simp add: ring_simps)
+ by (simp add: field_simps)
have "?rhs \<longleftrightarrow> Ifm vs (- (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d) # bs) (Lt (CNP 0 a r))" by (simp only: th)
also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d)) + ?r < 0"
by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / ((1 + 1) * ?c * ?d)"])
@@ -2178,11 +2178,11 @@
using dc' dc'' mult_less_cancel_left_disj[of "(1 + 1) * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ ((1 + 1)*?c*?d)) + ?r" 0] by simp
also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + (1 + 1)*?c*?d*?r < 0"
using nonzero_mult_divide_cancel_left[of "(1 + 1)*?c*?d"] c d
- by (simp add: ring_simps diff_divide_distrib del: left_distrib)
+ by (simp add: algebra_simps diff_divide_distrib del: left_distrib)
finally have ?thesis using dc c d nc nd dc'
- apply (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / ((1 + 1) * ?c * ?d)"] msubstlt_def Let_def evaldjf_ex ring_simps lt polyneg_norm polymul_norm)
+ apply (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / ((1 + 1) * ?c * ?d)"] msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
apply (simp only: one_add_one_is_two[symmetric] of_int_add)
- by (simp add: ring_simps order_less_not_sym[OF dc])}
+ by (simp add: field_simps order_less_not_sym[OF dc])}
moreover
{assume dc: "?c*?d < 0"
@@ -2191,7 +2191,7 @@
hence c:"?c \<noteq> 0" and d: "?d\<noteq> 0" by auto
from add_frac_eq[OF c d, of "- ?t" "- ?s"]
have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d)"
- by (simp add: ring_simps)
+ by (simp add: field_simps)
have "?rhs \<longleftrightarrow> Ifm vs (- (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d) # bs) (Lt (CNP 0 a r))" by (simp only: th)
also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d)) + ?r < 0"
by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / ((1 + 1) * ?c * ?d)"])
@@ -2201,78 +2201,78 @@
using dc' order_less_not_sym[OF dc'] mult_less_cancel_left_disj[of "(1 + 1) * ?c * ?d" 0 "?a * (- (?d * ?t + ?c* ?s)/ ((1 + 1)*?c*?d)) + ?r"] by simp
also have "\<dots> \<longleftrightarrow> ?a * ((?d * ?t + ?c* ?s )) - (1 + 1)*?c*?d*?r < 0"
using nonzero_mult_divide_cancel_left[of "(1 + 1)*?c*?d"] c d
- by (simp add: ring_simps diff_divide_distrib del: left_distrib)
+ by (simp add: algebra_simps diff_divide_distrib del: left_distrib)
finally have ?thesis using dc c d nc nd
- apply (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / ((1 + 1) * ?c * ?d)"] msubstlt_def Let_def evaldjf_ex ring_simps lt polyneg_norm polymul_norm)
+ apply (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / ((1 + 1) * ?c * ?d)"] msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
apply (simp only: one_add_one_is_two[symmetric] of_int_add)
- by (simp add: ring_simps order_less_not_sym[OF dc]) }
+ by (simp add: field_simps order_less_not_sym[OF dc]) }
moreover
{assume c: "?c > 0" and d: "?d=0"
from c have c'': "(1 + 1)*?c > 0" by (simp add: zero_less_mult_iff)
from c have c': "(1 + 1)*?c \<noteq> 0" by simp
- from d have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - ?t / ((1 + 1)*?c)" by (simp add: ring_simps)
+ from d have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - ?t / ((1 + 1)*?c)" by (simp add: field_simps)
have "?rhs \<longleftrightarrow> Ifm vs (- ?t / ((1 + 1)*?c) # bs) (Lt (CNP 0 a r))" by (simp only: th)
also have "\<dots> \<longleftrightarrow> ?a* (- ?t / ((1 + 1)*?c))+ ?r < 0" by (simp add: r[of "- (?t / ((1 + 1)*?c))"])
also have "\<dots> \<longleftrightarrow> (1 + 1)*?c * (?a* (- ?t / ((1 + 1)*?c))+ ?r) < 0"
using c mult_less_cancel_left_disj[of "(1 + 1) * ?c" "?a* (- ?t / ((1 + 1)*?c))+ ?r" 0] c' c'' order_less_not_sym[OF c''] by simp
also have "\<dots> \<longleftrightarrow> - ?a*?t+ (1 + 1)*?c *?r < 0"
using nonzero_mult_divide_cancel_left[OF c'] c
- by (simp add: ring_simps diff_divide_distrib less_le del: left_distrib)
+ by (simp add: algebra_simps diff_divide_distrib less_le del: left_distrib)
finally have ?thesis using c d nc nd
- apply(simp add: r[of "- (?t / ((1 + 1)*?c))"] msubstlt_def Let_def evaldjf_ex ring_simps lt polyneg_norm polymul_norm)
+ apply(simp add: r[of "- (?t / ((1 + 1)*?c))"] msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
apply (simp only: one_add_one_is_two[symmetric] of_int_add)
using c order_less_not_sym[OF c] less_imp_neq[OF c]
- by (simp add: ring_simps ) }
+ by (simp add: field_simps ) }
moreover
{assume c: "?c < 0" and d: "?d=0" hence c': "(1 + 1)*?c \<noteq> 0" by simp
from c have c'': "(1 + 1)*?c < 0" by (simp add: mult_less_0_iff)
- from d have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - ?t / ((1 + 1)*?c)" by (simp add: ring_simps)
+ from d have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - ?t / ((1 + 1)*?c)" by (simp add: field_simps)
have "?rhs \<longleftrightarrow> Ifm vs (- ?t / ((1 + 1)*?c) # bs) (Lt (CNP 0 a r))" by (simp only: th)
also have "\<dots> \<longleftrightarrow> ?a* (- ?t / ((1 + 1)*?c))+ ?r < 0" by (simp add: r[of "- (?t / ((1 + 1)*?c))"])
also have "\<dots> \<longleftrightarrow> (1 + 1)*?c * (?a* (- ?t / ((1 + 1)*?c))+ ?r) > 0"
using c order_less_not_sym[OF c''] less_imp_neq[OF c''] c'' mult_less_cancel_left_disj[of "(1 + 1) * ?c" 0 "?a* (- ?t / ((1 + 1)*?c))+ ?r"] by simp
also have "\<dots> \<longleftrightarrow> ?a*?t - (1 + 1)*?c *?r < 0"
using nonzero_mult_divide_cancel_left[OF c'] c order_less_not_sym[OF c''] less_imp_neq[OF c''] c''
- by (simp add: ring_simps diff_divide_distrib del: left_distrib)
+ by (simp add: algebra_simps diff_divide_distrib del: left_distrib)
finally have ?thesis using c d nc nd
- apply(simp add: r[of "- (?t / ((1 + 1)*?c))"] msubstlt_def Let_def evaldjf_ex ring_simps lt polyneg_norm polymul_norm)
+ apply(simp add: r[of "- (?t / ((1 + 1)*?c))"] msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
apply (simp only: one_add_one_is_two[symmetric] of_int_add)
using c order_less_not_sym[OF c] less_imp_neq[OF c]
- by (simp add: ring_simps ) }
+ by (simp add: field_simps ) }
moreover
moreover
{assume c: "?c = 0" and d: "?d>0"
from d have d'': "(1 + 1)*?d > 0" by (simp add: zero_less_mult_iff)
from d have d': "(1 + 1)*?d \<noteq> 0" by simp
- from c have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - ?s / ((1 + 1)*?d)" by (simp add: ring_simps)
+ from c have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - ?s / ((1 + 1)*?d)" by (simp add: field_simps)
have "?rhs \<longleftrightarrow> Ifm vs (- ?s / ((1 + 1)*?d) # bs) (Lt (CNP 0 a r))" by (simp only: th)
also have "\<dots> \<longleftrightarrow> ?a* (- ?s / ((1 + 1)*?d))+ ?r < 0" by (simp add: r[of "- (?s / ((1 + 1)*?d))"])
also have "\<dots> \<longleftrightarrow> (1 + 1)*?d * (?a* (- ?s / ((1 + 1)*?d))+ ?r) < 0"
using d mult_less_cancel_left_disj[of "(1 + 1) * ?d" "?a* (- ?s / ((1 + 1)*?d))+ ?r" 0] d' d'' order_less_not_sym[OF d''] by simp
also have "\<dots> \<longleftrightarrow> - ?a*?s+ (1 + 1)*?d *?r < 0"
using nonzero_mult_divide_cancel_left[OF d'] d
- by (simp add: ring_simps diff_divide_distrib less_le del: left_distrib)
+ by (simp add: algebra_simps diff_divide_distrib less_le del: left_distrib)
finally have ?thesis using c d nc nd
- apply(simp add: r[of "- (?s / ((1 + 1)*?d))"] msubstlt_def Let_def evaldjf_ex ring_simps lt polyneg_norm polymul_norm)
+ apply(simp add: r[of "- (?s / ((1 + 1)*?d))"] msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
apply (simp only: one_add_one_is_two[symmetric] of_int_add)
using d order_less_not_sym[OF d] less_imp_neq[OF d]
- by (simp add: ring_simps ) }
+ by (simp add: field_simps) }
moreover
{assume c: "?c = 0" and d: "?d<0" hence d': "(1 + 1)*?d \<noteq> 0" by simp
from d have d'': "(1 + 1)*?d < 0" by (simp add: mult_less_0_iff)
- from c have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - ?s / ((1 + 1)*?d)" by (simp add: ring_simps)
+ from c have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - ?s / ((1 + 1)*?d)" by (simp add: field_simps)
have "?rhs \<longleftrightarrow> Ifm vs (- ?s / ((1 + 1)*?d) # bs) (Lt (CNP 0 a r))" by (simp only: th)
also have "\<dots> \<longleftrightarrow> ?a* (- ?s / ((1 + 1)*?d))+ ?r < 0" by (simp add: r[of "- (?s / ((1 + 1)*?d))"])
also have "\<dots> \<longleftrightarrow> (1 + 1)*?d * (?a* (- ?s / ((1 + 1)*?d))+ ?r) > 0"
using d order_less_not_sym[OF d''] less_imp_neq[OF d''] d'' mult_less_cancel_left_disj[of "(1 + 1) * ?d" 0 "?a* (- ?s / ((1 + 1)*?d))+ ?r"] by simp
also have "\<dots> \<longleftrightarrow> ?a*?s - (1 + 1)*?d *?r < 0"
using nonzero_mult_divide_cancel_left[OF d'] d order_less_not_sym[OF d''] less_imp_neq[OF d''] d''
- by (simp add: ring_simps diff_divide_distrib del: left_distrib)
+ by (simp add: algebra_simps diff_divide_distrib del: left_distrib)
finally have ?thesis using c d nc nd
- apply(simp add: r[of "- (?s / ((1 + 1)*?d))"] msubstlt_def Let_def evaldjf_ex ring_simps lt polyneg_norm polymul_norm)
+ apply(simp add: r[of "- (?s / ((1 + 1)*?d))"] msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
apply (simp only: one_add_one_is_two[symmetric] of_int_add)
using d order_less_not_sym[OF d] less_imp_neq[OF d]
- by (simp add: ring_simps ) }
+ by (simp add: field_simps ) }
ultimately show ?thesis by blast
qed
@@ -2325,7 +2325,7 @@
from dc' have dc'': "\<not> (1 + 1)*?c *?d < 0" by simp
from add_frac_eq[OF c d, of "- ?t" "- ?s"]
have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d)"
- by (simp add: ring_simps)
+ by (simp add: field_simps)
have "?rhs \<longleftrightarrow> Ifm vs (- (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d) # bs) (Le (CNP 0 a r))" by (simp only: th)
also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d)) + ?r <= 0"
by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / ((1 + 1) * ?c * ?d)"])
@@ -2334,11 +2334,11 @@
using dc' dc'' mult_le_cancel_left[of "(1 + 1) * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ ((1 + 1)*?c*?d)) + ?r" 0] by simp
also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + (1 + 1)*?c*?d*?r <= 0"
using nonzero_mult_divide_cancel_left[of "(1 + 1)*?c*?d"] c d
- by (simp add: ring_simps diff_divide_distrib del: left_distrib)
+ by (simp add: algebra_simps diff_divide_distrib del: left_distrib)
finally have ?thesis using dc c d nc nd dc'
- apply (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / ((1 + 1) * ?c * ?d)"] msubstle_def Let_def evaldjf_ex ring_simps lt polyneg_norm polymul_norm)
+ apply (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / ((1 + 1) * ?c * ?d)"] msubstle_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
apply (simp only: one_add_one_is_two[symmetric] of_int_add)
- by (simp add: ring_simps order_less_not_sym[OF dc])}
+ by (simp add: field_simps order_less_not_sym[OF dc])}
moreover
{assume dc: "?c*?d < 0"
@@ -2347,7 +2347,7 @@
hence c:"?c \<noteq> 0" and d: "?d\<noteq> 0" by auto
from add_frac_eq[OF c d, of "- ?t" "- ?s"]
have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d)"
- by (simp add: ring_simps)
+ by (simp add: field_simps)
have "?rhs \<longleftrightarrow> Ifm vs (- (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d) # bs) (Le (CNP 0 a r))" by (simp only: th)
also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )/ ((1 + 1)*?c*?d)) + ?r <= 0"
by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / ((1 + 1) * ?c * ?d)"])
@@ -2357,78 +2357,78 @@
using dc' order_less_not_sym[OF dc'] mult_le_cancel_left[of "(1 + 1) * ?c * ?d" 0 "?a * (- (?d * ?t + ?c* ?s)/ ((1 + 1)*?c*?d)) + ?r"] by simp
also have "\<dots> \<longleftrightarrow> ?a * ((?d * ?t + ?c* ?s )) - (1 + 1)*?c*?d*?r <= 0"
using nonzero_mult_divide_cancel_left[of "(1 + 1)*?c*?d"] c d
- by (simp add: ring_simps diff_divide_distrib del: left_distrib)
+ by (simp add: algebra_simps diff_divide_distrib del: left_distrib)
finally have ?thesis using dc c d nc nd
- apply (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / ((1 + 1) * ?c * ?d)"] msubstle_def Let_def evaldjf_ex ring_simps lt polyneg_norm polymul_norm)
+ apply (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / ((1 + 1) * ?c * ?d)"] msubstle_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
apply (simp only: one_add_one_is_two[symmetric] of_int_add)
- by (simp add: ring_simps order_less_not_sym[OF dc]) }
+ by (simp add: field_simps order_less_not_sym[OF dc]) }
moreover
{assume c: "?c > 0" and d: "?d=0"
from c have c'': "(1 + 1)*?c > 0" by (simp add: zero_less_mult_iff)
from c have c': "(1 + 1)*?c \<noteq> 0" by simp
- from d have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - ?t / ((1 + 1)*?c)" by (simp add: ring_simps)
+ from d have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - ?t / ((1 + 1)*?c)" by (simp add: field_simps)
have "?rhs \<longleftrightarrow> Ifm vs (- ?t / ((1 + 1)*?c) # bs) (Le (CNP 0 a r))" by (simp only: th)
also have "\<dots> \<longleftrightarrow> ?a* (- ?t / ((1 + 1)*?c))+ ?r <= 0" by (simp add: r[of "- (?t / ((1 + 1)*?c))"])
also have "\<dots> \<longleftrightarrow> (1 + 1)*?c * (?a* (- ?t / ((1 + 1)*?c))+ ?r) <= 0"
using c mult_le_cancel_left[of "(1 + 1) * ?c" "?a* (- ?t / ((1 + 1)*?c))+ ?r" 0] c' c'' order_less_not_sym[OF c''] by simp
also have "\<dots> \<longleftrightarrow> - ?a*?t+ (1 + 1)*?c *?r <= 0"
using nonzero_mult_divide_cancel_left[OF c'] c
- by (simp add: ring_simps diff_divide_distrib less_le del: left_distrib)
+ by (simp add: algebra_simps diff_divide_distrib less_le del: left_distrib)
finally have ?thesis using c d nc nd
- apply(simp add: r[of "- (?t / ((1 + 1)*?c))"] msubstle_def Let_def evaldjf_ex ring_simps lt polyneg_norm polymul_norm)
+ apply(simp add: r[of "- (?t / ((1 + 1)*?c))"] msubstle_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
apply (simp only: one_add_one_is_two[symmetric] of_int_add)
using c order_less_not_sym[OF c] less_imp_neq[OF c]
- by (simp add: ring_simps ) }
+ by (simp add: field_simps ) }
moreover
{assume c: "?c < 0" and d: "?d=0" hence c': "(1 + 1)*?c \<noteq> 0" by simp
from c have c'': "(1 + 1)*?c < 0" by (simp add: mult_less_0_iff)
- from d have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - ?t / ((1 + 1)*?c)" by (simp add: ring_simps)
+ from d have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - ?t / ((1 + 1)*?c)" by (simp add: field_simps)
have "?rhs \<longleftrightarrow> Ifm vs (- ?t / ((1 + 1)*?c) # bs) (Le (CNP 0 a r))" by (simp only: th)
also have "\<dots> \<longleftrightarrow> ?a* (- ?t / ((1 + 1)*?c))+ ?r <= 0" by (simp add: r[of "- (?t / ((1 + 1)*?c))"])
also have "\<dots> \<longleftrightarrow> (1 + 1)*?c * (?a* (- ?t / ((1 + 1)*?c))+ ?r) >= 0"
using c order_less_not_sym[OF c''] less_imp_neq[OF c''] c'' mult_le_cancel_left[of "(1 + 1) * ?c" 0 "?a* (- ?t / ((1 + 1)*?c))+ ?r"] by simp
also have "\<dots> \<longleftrightarrow> ?a*?t - (1 + 1)*?c *?r <= 0"
using nonzero_mult_divide_cancel_left[OF c'] c order_less_not_sym[OF c''] less_imp_neq[OF c''] c''
- by (simp add: ring_simps diff_divide_distrib del: left_distrib)
+ by (simp add: algebra_simps diff_divide_distrib del: left_distrib)
finally have ?thesis using c d nc nd
- apply(simp add: r[of "- (?t / ((1 + 1)*?c))"] msubstle_def Let_def evaldjf_ex ring_simps lt polyneg_norm polymul_norm)
+ apply(simp add: r[of "- (?t / ((1 + 1)*?c))"] msubstle_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
apply (simp only: one_add_one_is_two[symmetric] of_int_add)
using c order_less_not_sym[OF c] less_imp_neq[OF c]
- by (simp add: ring_simps ) }
+ by (simp add: field_simps ) }
moreover
moreover
{assume c: "?c = 0" and d: "?d>0"
from d have d'': "(1 + 1)*?d > 0" by (simp add: zero_less_mult_iff)
from d have d': "(1 + 1)*?d \<noteq> 0" by simp
- from c have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - ?s / ((1 + 1)*?d)" by (simp add: ring_simps)
+ from c have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - ?s / ((1 + 1)*?d)" by (simp add: field_simps)
have "?rhs \<longleftrightarrow> Ifm vs (- ?s / ((1 + 1)*?d) # bs) (Le (CNP 0 a r))" by (simp only: th)
also have "\<dots> \<longleftrightarrow> ?a* (- ?s / ((1 + 1)*?d))+ ?r <= 0" by (simp add: r[of "- (?s / ((1 + 1)*?d))"])
also have "\<dots> \<longleftrightarrow> (1 + 1)*?d * (?a* (- ?s / ((1 + 1)*?d))+ ?r) <= 0"
using d mult_le_cancel_left[of "(1 + 1) * ?d" "?a* (- ?s / ((1 + 1)*?d))+ ?r" 0] d' d'' order_less_not_sym[OF d''] by simp
also have "\<dots> \<longleftrightarrow> - ?a*?s+ (1 + 1)*?d *?r <= 0"
using nonzero_mult_divide_cancel_left[OF d'] d
- by (simp add: ring_simps diff_divide_distrib less_le del: left_distrib)
+ by (simp add: algebra_simps diff_divide_distrib less_le del: left_distrib)
finally have ?thesis using c d nc nd
- apply(simp add: r[of "- (?s / ((1 + 1)*?d))"] msubstle_def Let_def evaldjf_ex ring_simps lt polyneg_norm polymul_norm)
+ apply(simp add: r[of "- (?s / ((1 + 1)*?d))"] msubstle_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
apply (simp only: one_add_one_is_two[symmetric] of_int_add)
using d order_less_not_sym[OF d] less_imp_neq[OF d]
- by (simp add: ring_simps ) }
+ by (simp add: field_simps ) }
moreover
{assume c: "?c = 0" and d: "?d<0" hence d': "(1 + 1)*?d \<noteq> 0" by simp
from d have d'': "(1 + 1)*?d < 0" by (simp add: mult_less_0_iff)
- from c have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - ?s / ((1 + 1)*?d)" by (simp add: ring_simps)
+ from c have th: "(- ?t / ?c + - ?s / ?d)/(1 + 1) = - ?s / ((1 + 1)*?d)" by (simp add: field_simps)
have "?rhs \<longleftrightarrow> Ifm vs (- ?s / ((1 + 1)*?d) # bs) (Le (CNP 0 a r))" by (simp only: th)
also have "\<dots> \<longleftrightarrow> ?a* (- ?s / ((1 + 1)*?d))+ ?r <= 0" by (simp add: r[of "- (?s / ((1 + 1)*?d))"])
also have "\<dots> \<longleftrightarrow> (1 + 1)*?d * (?a* (- ?s / ((1 + 1)*?d))+ ?r) >= 0"
using d order_less_not_sym[OF d''] less_imp_neq[OF d''] d'' mult_le_cancel_left[of "(1 + 1) * ?d" 0 "?a* (- ?s / ((1 + 1)*?d))+ ?r"] by simp
also have "\<dots> \<longleftrightarrow> ?a*?s - (1 + 1)*?d *?r <= 0"
using nonzero_mult_divide_cancel_left[OF d'] d order_less_not_sym[OF d''] less_imp_neq[OF d''] d''
- by (simp add: ring_simps diff_divide_distrib del: left_distrib)
+ by (simp add: algebra_simps diff_divide_distrib del: left_distrib)
finally have ?thesis using c d nc nd
- apply(simp add: r[of "- (?s / ((1 + 1)*?d))"] msubstle_def Let_def evaldjf_ex ring_simps lt polyneg_norm polymul_norm)
+ apply(simp add: r[of "- (?s / ((1 + 1)*?d))"] msubstle_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
apply (simp only: one_add_one_is_two[symmetric] of_int_add)
using d order_less_not_sym[OF d] less_imp_neq[OF d]
- by (simp add: ring_simps ) }
+ by (simp add: field_simps ) }
ultimately show ?thesis by blast
qed
@@ -2519,7 +2519,7 @@
lemma remdps_set[simp]: "set (remdps xs) = set xs"
by (induct xs rule: remdps.induct, auto)
-lemma simpfm_lin: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
+lemma simpfm_lin: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
shows "qfree p \<Longrightarrow> islin (simpfm p)"
by (induct p rule: simpfm.induct, auto simp add: conj_lin disj_lin)
@@ -2551,7 +2551,7 @@
{fix c t d s assume ctU: "(c,t) \<in> set ?U" and dsU: "(d,s) \<in> set ?U"
from U_l ctU dsU have norm: "isnpoly c" "isnpoly d" by auto
from msubst_I[OF lq norm, of vs x bs t s] msubst_I[OF lq norm(2,1), of vs x bs s t]
- have "?I (msubst ?q ((c,t),(d,s))) = ?I (msubst ?q ((d,s),(c,t)))" by (simp add: ring_simps)}
+ have "?I (msubst ?q ((c,t),(d,s))) = ?I (msubst ?q ((d,s),(c,t)))" by (simp add: field_simps)}
hence th0: "\<forall>x \<in> set ?U. \<forall>y \<in> set ?U. ?I (msubst ?q (x, y)) \<longleftrightarrow> ?I (msubst ?q (y, x))" by clarsimp
{fix x assume xUp: "x \<in> set ?Up"
then obtain c t d s where ctU: "(c,t) \<in> set ?U" and dsU: "(d,s) \<in> set ?U"
@@ -2616,7 +2616,7 @@
let ?s = "Itm vs (x # bs) s"
let ?t = "Itm vs (x # bs) t"
have eq2: "\<And>(x::'a). x + x = (1 + 1) * x"
- by (simp add: ring_simps)
+ by (simp add: field_simps)
{assume "?c = 0 \<and> ?d = 0"
with ct have ?D by simp}
moreover
@@ -2747,12 +2747,12 @@
using lp tnb
by (induct p c t rule: msubstpos.induct, auto simp add: msubsteq2_nb msubstltpos_nb msubstlepos_nb)
-lemma msubstneg_nb: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})" and lp: "islin p" and tnb: "tmbound0 t"
+lemma msubstneg_nb: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})" and lp: "islin p" and tnb: "tmbound0 t"
shows "bound0 (msubstneg p c t)"
using lp tnb
by (induct p c t rule: msubstneg.induct, auto simp add: msubsteq2_nb msubstltneg_nb msubstleneg_nb)
-lemma msubst2_nb: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})" and lp: "islin p" and tnb: "tmbound0 t"
+lemma msubst2_nb: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})" and lp: "islin p" and tnb: "tmbound0 t"
shows "bound0 (msubst2 p c t)"
using lp tnb
by (simp add: msubst2_def msubstneg_nb msubstpos_nb conj_nb disj_nb lt_nb simpfm_bound0)
@@ -2899,14 +2899,14 @@
by (auto simp add: msubst2_def lt[OF stupid(3)] lt[OF stupid(1)] mult_less_0_iff zero_less_mult_iff)
from msubst2[OF lq norm2(1) z(1), of x bs]
msubst2[OF lq norm2(2) z(2), of x bs] H
- show ?rhs by (simp add: ring_simps)
+ show ?rhs by (simp add: field_simps)
next
assume H: ?rhs
hence z: "\<lparr>C (-2, 1) *\<^sub>p b *\<^sub>p d\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0" "\<lparr>C (-2, 1) *\<^sub>p d *\<^sub>p b\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0"
by (auto simp add: msubst2_def lt[OF stupid(4)] lt[OF stupid(2)] mult_less_0_iff zero_less_mult_iff)
from msubst2[OF lq norm2(1) z(1), of x bs]
msubst2[OF lq norm2(2) z(2), of x bs] H
- show ?lhs by (simp add: ring_simps)
+ show ?lhs by (simp add: field_simps)
qed}
hence th0: "\<forall>x \<in> set ?U. \<forall>y \<in> set ?U. ?I (?s (x, y)) \<longleftrightarrow> ?I (?s (y, x))"
by clarsimp
@@ -3156,54 +3156,54 @@
*} "Parametric QE for linear Arithmetic over fields, Version 2"
-lemma "\<exists>(x::'a::{division_by_zero,linordered_field,number_ring}). y \<noteq> -1 \<longrightarrow> (y + 1)*x < 0"
- apply (frpar type: "'a::{division_by_zero,linordered_field,number_ring}" pars: "y::'a::{division_by_zero,linordered_field,number_ring}")
- apply (simp add: ring_simps)
+lemma "\<exists>(x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). y \<noteq> -1 \<longrightarrow> (y + 1)*x < 0"
+ apply (frpar type: "'a::{linordered_field, division_ring_inverse_zero, number_ring}" pars: "y::'a::{linordered_field, division_ring_inverse_zero, number_ring}")
+ apply (simp add: field_simps)
apply (rule spec[where x=y])
- apply (frpar type: "'a::{division_by_zero,linordered_field,number_ring}" pars: "z::'a::{division_by_zero,linordered_field,number_ring}")
+ apply (frpar type: "'a::{linordered_field, division_ring_inverse_zero, number_ring}" pars: "z::'a::{linordered_field, division_ring_inverse_zero, number_ring}")
by simp
text{* Collins/Jones Problem *}
(*
-lemma "\<exists>(r::'a::{division_by_zero,linordered_field,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"
+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"
proof-
- have "(\<exists>(r::'a::{division_by_zero,linordered_field,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::{division_by_zero,linordered_field,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")
-by (simp add: ring_simps)
+ 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")
+by (simp add: field_simps)
have "?rhs"
- apply (frpar type: "'a::{division_by_zero,linordered_field,number_ring}" pars: "a::'a::{division_by_zero,linordered_field,number_ring}" "b::'a::{division_by_zero,linordered_field,number_ring}")
- apply (simp add: ring_simps)
+ 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}")
+ apply (simp add: field_simps)
oops
*)
(*
-lemma "ALL (x::'a::{division_by_zero,linordered_field,number_ring}) y. (1 - t)*x \<le> (1+t)*y \<and> (1 - t)*y \<le> (1+t)*x --> 0 \<le> y"
-apply (frpar type: "'a::{division_by_zero,linordered_field,number_ring}" pars: "t::'a::{division_by_zero,linordered_field,number_ring}")
+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"
+apply (frpar type: "'a::{linordered_field, division_ring_inverse_zero, number_ring}" pars: "t::'a::{linordered_field, division_ring_inverse_zero, number_ring}")
oops
*)
-lemma "\<exists>(x::'a::{division_by_zero,linordered_field,number_ring}). y \<noteq> -1 \<longrightarrow> (y + 1)*x < 0"
- apply (frpar2 type: "'a::{division_by_zero,linordered_field,number_ring}" pars: "y::'a::{division_by_zero,linordered_field,number_ring}")
- apply (simp add: ring_simps)
+lemma "\<exists>(x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). y \<noteq> -1 \<longrightarrow> (y + 1)*x < 0"
+ apply (frpar2 type: "'a::{linordered_field, division_ring_inverse_zero, number_ring}" pars: "y::'a::{linordered_field, division_ring_inverse_zero, number_ring}")
+ apply (simp add: field_simps)
apply (rule spec[where x=y])
- apply (frpar2 type: "'a::{division_by_zero,linordered_field,number_ring}" pars: "z::'a::{division_by_zero,linordered_field,number_ring}")
+ apply (frpar2 type: "'a::{linordered_field, division_ring_inverse_zero, number_ring}" pars: "z::'a::{linordered_field, division_ring_inverse_zero, number_ring}")
by simp
text{* Collins/Jones Problem *}
(*
-lemma "\<exists>(r::'a::{division_by_zero,linordered_field,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"
+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"
proof-
- have "(\<exists>(r::'a::{division_by_zero,linordered_field,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::{division_by_zero,linordered_field,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")
-by (simp add: ring_simps)
+ 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")
+by (simp add: field_simps)
have "?rhs"
- apply (frpar2 type: "'a::{division_by_zero,linordered_field,number_ring}" pars: "a::'a::{division_by_zero,linordered_field,number_ring}" "b::'a::{division_by_zero,linordered_field,number_ring}")
+ 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}")
apply simp
oops
*)
(*
-lemma "ALL (x::'a::{division_by_zero,linordered_field,number_ring}) y. (1 - t)*x \<le> (1+t)*y \<and> (1 - t)*y \<le> (1+t)*x --> 0 \<le> y"
-apply (frpar2 type: "'a::{division_by_zero,linordered_field,number_ring}" pars: "t::'a::{division_by_zero,linordered_field,number_ring}")
+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"
+apply (frpar2 type: "'a::{linordered_field, division_ring_inverse_zero, number_ring}" pars: "t::'a::{linordered_field, division_ring_inverse_zero, number_ring}")
apply (simp add: field_simps linorder_neq_iff[symmetric])
apply ferrack
oops
--- a/src/HOL/Fields.thy Mon Apr 26 11:34:15 2010 +0200
+++ b/src/HOL/Fields.thy Mon Apr 26 11:34:15 2010 +0200
@@ -13,20 +13,6 @@
imports Rings
begin
-text{* Lemmas @{text field_simps} multiply with denominators in (in)equations
-if they can be proved to be non-zero (for equations) or positive/negative
-(for inequations). Can be too aggressive and is therefore separate from the
-more benign @{text algebra_simps}. *}
-
-ML {*
-structure Field_Simps = Named_Thms(
- val name = "field_simps"
- val description = "algebra simplification rules for fields"
-)
-*}
-
-setup Field_Simps.setup
-
class field = comm_ring_1 + inverse +
assumes field_inverse: "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
assumes field_divide_inverse: "a / b = a * inverse b"
@@ -110,51 +96,45 @@
"\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (a * c) / (c * b) = a / b"
using nonzero_mult_divide_mult_cancel_right [of b c a] by (simp add: mult_ac)
-lemma add_divide_eq_iff:
+lemma add_divide_eq_iff [field_simps]:
"z \<noteq> 0 \<Longrightarrow> x + y / z = (z * x + y) / z"
by (simp add: add_divide_distrib)
-lemma divide_add_eq_iff:
+lemma divide_add_eq_iff [field_simps]:
"z \<noteq> 0 \<Longrightarrow> x / z + y = (x + z * y) / z"
by (simp add: add_divide_distrib)
-lemma diff_divide_eq_iff:
+lemma diff_divide_eq_iff [field_simps]:
"z \<noteq> 0 \<Longrightarrow> x - y / z = (z * x - y) / z"
by (simp add: diff_divide_distrib)
-lemma divide_diff_eq_iff:
+lemma divide_diff_eq_iff [field_simps]:
"z \<noteq> 0 \<Longrightarrow> x / z - y = (x - z * y) / z"
by (simp add: diff_divide_distrib)
-lemmas field_eq_simps [field_simps, no_atp] = algebra_simps
- (* pull / out*)
- add_divide_eq_iff divide_add_eq_iff
- diff_divide_eq_iff divide_diff_eq_iff
- (* multiply eqn *)
- nonzero_eq_divide_eq nonzero_divide_eq_eq
- times_divide_eq_left times_divide_eq_right
-
-text{*An example:*}
-lemma "\<lbrakk>a\<noteq>b; c\<noteq>d; e\<noteq>f\<rbrakk> \<Longrightarrow> ((a-b)*(c-d)*(e-f))/((c-d)*(e-f)*(a-b)) = 1"
-apply(subgoal_tac "(c-d)*(e-f)*(a-b) \<noteq> 0")
- apply(simp add:field_eq_simps)
-apply(simp)
-done
-
lemma diff_frac_eq:
"y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> x / y - w / z = (x * z - w * y) / (y * z)"
- by (simp add: field_eq_simps times_divide_eq)
+ by (simp add: field_simps)
lemma frac_eq_eq:
"y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> (x / y = w / z) = (x * z = w * y)"
- by (simp add: field_eq_simps times_divide_eq)
+ by (simp add: field_simps)
+
+end
+
+class field_inverse_zero = field +
+ assumes field_inverse_zero: "inverse 0 = 0"
+begin
+
+subclass division_ring_inverse_zero proof
+qed (fact field_inverse_zero)
end
text{*This version builds in division by zero while also re-orienting
the right-hand side.*}
lemma inverse_mult_distrib [simp]:
- "inverse(a*b) = inverse(a) * inverse(b::'a::{field,division_by_zero})"
+ "inverse(a*b) = inverse(a) * inverse(b::'a::{field,division_ring_inverse_zero})"
proof cases
assume "a \<noteq> 0 & b \<noteq> 0"
thus ?thesis by (simp add: nonzero_inverse_mult_distrib mult_ac)
@@ -164,7 +144,7 @@
qed
lemma inverse_divide [simp]:
- "inverse (a/b) = b / (a::'a::{field,division_by_zero})"
+ "inverse (a/b) = b / (a::'a::{field,division_ring_inverse_zero})"
by (simp add: divide_inverse mult_commute)
@@ -175,85 +155,85 @@
because the latter are covered by a simproc. *}
lemma mult_divide_mult_cancel_left:
- "c\<noteq>0 ==> (c*a) / (c*b) = a / (b::'a::{field,division_by_zero})"
+ "c\<noteq>0 ==> (c*a) / (c*b) = a / (b::'a::{field,division_ring_inverse_zero})"
apply (cases "b = 0")
apply simp_all
done
lemma mult_divide_mult_cancel_right:
- "c\<noteq>0 ==> (a*c) / (b*c) = a / (b::'a::{field,division_by_zero})"
+ "c\<noteq>0 ==> (a*c) / (b*c) = a / (b::'a::{field,division_ring_inverse_zero})"
apply (cases "b = 0")
apply simp_all
done
lemma divide_divide_eq_right [simp,no_atp]:
- "a / (b/c) = (a*c) / (b::'a::{field,division_by_zero})"
+ "a / (b/c) = (a*c) / (b::'a::{field,division_ring_inverse_zero})"
by (simp add: divide_inverse mult_ac)
lemma divide_divide_eq_left [simp,no_atp]:
- "(a / b) / (c::'a::{field,division_by_zero}) = a / (b*c)"
+ "(a / b) / (c::'a::{field,division_ring_inverse_zero}) = a / (b*c)"
by (simp add: divide_inverse mult_assoc)
text {*Special Cancellation Simprules for Division*}
lemma mult_divide_mult_cancel_left_if[simp,no_atp]:
-fixes c :: "'a :: {field,division_by_zero}"
+fixes c :: "'a :: {field,division_ring_inverse_zero}"
shows "(c*a) / (c*b) = (if c=0 then 0 else a/b)"
by (simp add: mult_divide_mult_cancel_left)
text {* Division and Unary Minus *}
-lemma minus_divide_right: "- (a/b) = a / -(b::'a::{field,division_by_zero})"
+lemma minus_divide_right: "- (a/b) = a / -(b::'a::{field,division_ring_inverse_zero})"
by (simp add: divide_inverse)
lemma divide_minus_right [simp, no_atp]:
- "a / -(b::'a::{field,division_by_zero}) = -(a / b)"
+ "a / -(b::'a::{field,division_ring_inverse_zero}) = -(a / b)"
by (simp add: divide_inverse)
lemma minus_divide_divide:
- "(-a)/(-b) = a / (b::'a::{field,division_by_zero})"
+ "(-a)/(-b) = a / (b::'a::{field,division_ring_inverse_zero})"
apply (cases "b=0", simp)
apply (simp add: nonzero_minus_divide_divide)
done
lemma eq_divide_eq:
- "((a::'a::{field,division_by_zero}) = b/c) = (if c\<noteq>0 then a*c = b else a=0)"
+ "((a::'a::{field,division_ring_inverse_zero}) = b/c) = (if c\<noteq>0 then a*c = b else a=0)"
by (simp add: nonzero_eq_divide_eq)
lemma divide_eq_eq:
- "(b/c = (a::'a::{field,division_by_zero})) = (if c\<noteq>0 then b = a*c else a=0)"
+ "(b/c = (a::'a::{field,division_ring_inverse_zero})) = (if c\<noteq>0 then b = a*c else a=0)"
by (force simp add: nonzero_divide_eq_eq)
lemma inverse_eq_1_iff [simp]:
- "(inverse x = 1) = (x = (1::'a::{field,division_by_zero}))"
+ "(inverse x = 1) = (x = (1::'a::{field,division_ring_inverse_zero}))"
by (insert inverse_eq_iff_eq [of x 1], simp)
lemma divide_eq_0_iff [simp,no_atp]:
- "(a/b = 0) = (a=0 | b=(0::'a::{field,division_by_zero}))"
+ "(a/b = 0) = (a=0 | b=(0::'a::{field,division_ring_inverse_zero}))"
by (simp add: divide_inverse)
lemma divide_cancel_right [simp,no_atp]:
- "(a/c = b/c) = (c = 0 | a = (b::'a::{field,division_by_zero}))"
+ "(a/c = b/c) = (c = 0 | a = (b::'a::{field,division_ring_inverse_zero}))"
apply (cases "c=0", simp)
apply (simp add: divide_inverse)
done
lemma divide_cancel_left [simp,no_atp]:
- "(c/a = c/b) = (c = 0 | a = (b::'a::{field,division_by_zero}))"
+ "(c/a = c/b) = (c = 0 | a = (b::'a::{field,division_ring_inverse_zero}))"
apply (cases "c=0", simp)
apply (simp add: divide_inverse)
done
lemma divide_eq_1_iff [simp,no_atp]:
- "(a/b = 1) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
+ "(a/b = 1) = (b \<noteq> 0 & a = (b::'a::{field,division_ring_inverse_zero}))"
apply (cases "b=0", simp)
apply (simp add: right_inverse_eq)
done
lemma one_eq_divide_iff [simp,no_atp]:
- "(1 = a/b) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
+ "(1 = a/b) = (b \<noteq> 0 & a = (b::'a::{field,division_ring_inverse_zero}))"
by (simp add: eq_commute [of 1])
@@ -405,7 +385,7 @@
"a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> inverse a \<le> inverse b \<longleftrightarrow> b \<le> a"
by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg)
-lemma pos_le_divide_eq: "0 < c ==> (a \<le> b/c) = (a*c \<le> b)"
+lemma pos_le_divide_eq [field_simps]: "0 < c ==> (a \<le> b/c) = (a*c \<le> b)"
proof -
assume less: "0<c"
hence "(a \<le> b/c) = (a*c \<le> (b/c)*c)"
@@ -415,7 +395,7 @@
finally show ?thesis .
qed
-lemma neg_le_divide_eq: "c < 0 ==> (a \<le> b/c) = (b \<le> a*c)"
+lemma neg_le_divide_eq [field_simps]: "c < 0 ==> (a \<le> b/c) = (b \<le> a*c)"
proof -
assume less: "c<0"
hence "(a \<le> b/c) = ((b/c)*c \<le> a*c)"
@@ -425,7 +405,7 @@
finally show ?thesis .
qed
-lemma pos_less_divide_eq:
+lemma pos_less_divide_eq [field_simps]:
"0 < c ==> (a < b/c) = (a*c < b)"
proof -
assume less: "0<c"
@@ -436,7 +416,7 @@
finally show ?thesis .
qed
-lemma neg_less_divide_eq:
+lemma neg_less_divide_eq [field_simps]:
"c < 0 ==> (a < b/c) = (b < a*c)"
proof -
assume less: "c<0"
@@ -447,7 +427,7 @@
finally show ?thesis .
qed
-lemma pos_divide_less_eq:
+lemma pos_divide_less_eq [field_simps]:
"0 < c ==> (b/c < a) = (b < a*c)"
proof -
assume less: "0<c"
@@ -458,7 +438,7 @@
finally show ?thesis .
qed
-lemma neg_divide_less_eq:
+lemma neg_divide_less_eq [field_simps]:
"c < 0 ==> (b/c < a) = (a*c < b)"
proof -
assume less: "c<0"
@@ -469,7 +449,7 @@
finally show ?thesis .
qed
-lemma pos_divide_le_eq: "0 < c ==> (b/c \<le> a) = (b \<le> a*c)"
+lemma pos_divide_le_eq [field_simps]: "0 < c ==> (b/c \<le> a) = (b \<le> a*c)"
proof -
assume less: "0<c"
hence "(b/c \<le> a) = ((b/c)*c \<le> a*c)"
@@ -479,7 +459,7 @@
finally show ?thesis .
qed
-lemma neg_divide_le_eq: "c < 0 ==> (b/c \<le> a) = (a*c \<le> b)"
+lemma neg_divide_le_eq [field_simps]: "c < 0 ==> (b/c \<le> a) = (a*c \<le> b)"
proof -
assume less: "c<0"
hence "(b/c \<le> a) = (a*c \<le> (b/c)*c)"
@@ -489,19 +469,15 @@
finally show ?thesis .
qed
-lemmas [field_simps, no_atp] =
- (* multiply ineqn *)
- pos_divide_less_eq neg_divide_less_eq
- pos_less_divide_eq neg_less_divide_eq
- pos_divide_le_eq neg_divide_le_eq
- pos_le_divide_eq neg_le_divide_eq
-
text{* Lemmas @{text sign_simps} is a first attempt to automate proofs
of positivity/negativity needed for @{text field_simps}. Have not added @{text
sign_simps} to @{text field_simps} because the former can lead to case
explosions. *}
-lemmas sign_simps[no_atp] = group_simps
+lemmas sign_simps [no_atp] = algebra_simps
+ zero_less_mult_iff mult_less_0_iff
+
+lemmas (in -) sign_simps [no_atp] = algebra_simps
zero_less_mult_iff mult_less_0_iff
(* Only works once linear arithmetic is installed:
@@ -667,37 +643,46 @@
end
+class linordered_field_inverse_zero = linordered_field +
+ assumes linordered_field_inverse_zero: "inverse 0 = 0"
+begin
+
+subclass field_inverse_zero proof
+qed (fact linordered_field_inverse_zero)
+
+end
+
lemma le_divide_eq:
"(a \<le> b/c) =
(if 0 < c then a*c \<le> b
else if c < 0 then b \<le> a*c
- else a \<le> (0::'a::{linordered_field,division_by_zero}))"
+ else a \<le> (0::'a::{linordered_field,division_ring_inverse_zero}))"
apply (cases "c=0", simp)
apply (force simp add: pos_le_divide_eq neg_le_divide_eq linorder_neq_iff)
done
lemma inverse_positive_iff_positive [simp]:
- "(0 < inverse a) = (0 < (a::'a::{linordered_field,division_by_zero}))"
+ "(0 < inverse a) = (0 < (a::'a::{linordered_field,division_ring_inverse_zero}))"
apply (cases "a = 0", simp)
apply (blast intro: inverse_positive_imp_positive positive_imp_inverse_positive)
done
lemma inverse_negative_iff_negative [simp]:
- "(inverse a < 0) = (a < (0::'a::{linordered_field,division_by_zero}))"
+ "(inverse a < 0) = (a < (0::'a::{linordered_field,division_ring_inverse_zero}))"
apply (cases "a = 0", simp)
apply (blast intro: inverse_negative_imp_negative negative_imp_inverse_negative)
done
lemma inverse_nonnegative_iff_nonnegative [simp]:
- "(0 \<le> inverse a) = (0 \<le> (a::'a::{linordered_field,division_by_zero}))"
+ "(0 \<le> inverse a) = (0 \<le> (a::'a::{linordered_field,division_ring_inverse_zero}))"
by (simp add: linorder_not_less [symmetric])
lemma inverse_nonpositive_iff_nonpositive [simp]:
- "(inverse a \<le> 0) = (a \<le> (0::'a::{linordered_field,division_by_zero}))"
+ "(inverse a \<le> 0) = (a \<le> (0::'a::{linordered_field,division_ring_inverse_zero}))"
by (simp add: linorder_not_less [symmetric])
lemma one_less_inverse_iff:
- "(1 < inverse x) = (0 < x & x < (1::'a::{linordered_field,division_by_zero}))"
+ "(1 < inverse x) = (0 < x & x < (1::'a::{linordered_field,division_ring_inverse_zero}))"
proof cases
assume "0 < x"
with inverse_less_iff_less [OF zero_less_one, of x]
@@ -715,22 +700,22 @@
qed
lemma one_le_inverse_iff:
- "(1 \<le> inverse x) = (0 < x & x \<le> (1::'a::{linordered_field,division_by_zero}))"
+ "(1 \<le> inverse x) = (0 < x & x \<le> (1::'a::{linordered_field,division_ring_inverse_zero}))"
by (force simp add: order_le_less one_less_inverse_iff)
lemma inverse_less_1_iff:
- "(inverse x < 1) = (x \<le> 0 | 1 < (x::'a::{linordered_field,division_by_zero}))"
+ "(inverse x < 1) = (x \<le> 0 | 1 < (x::'a::{linordered_field,division_ring_inverse_zero}))"
by (simp add: linorder_not_le [symmetric] one_le_inverse_iff)
lemma inverse_le_1_iff:
- "(inverse x \<le> 1) = (x \<le> 0 | 1 \<le> (x::'a::{linordered_field,division_by_zero}))"
+ "(inverse x \<le> 1) = (x \<le> 0 | 1 \<le> (x::'a::{linordered_field,division_ring_inverse_zero}))"
by (simp add: linorder_not_less [symmetric] one_less_inverse_iff)
lemma divide_le_eq:
"(b/c \<le> a) =
(if 0 < c then b \<le> a*c
else if c < 0 then a*c \<le> b
- else 0 \<le> (a::'a::{linordered_field,division_by_zero}))"
+ else 0 \<le> (a::'a::{linordered_field,division_ring_inverse_zero}))"
apply (cases "c=0", simp)
apply (force simp add: pos_divide_le_eq neg_divide_le_eq linorder_neq_iff)
done
@@ -739,7 +724,7 @@
"(a < b/c) =
(if 0 < c then a*c < b
else if c < 0 then b < a*c
- else a < (0::'a::{linordered_field,division_by_zero}))"
+ else a < (0::'a::{linordered_field,division_ring_inverse_zero}))"
apply (cases "c=0", simp)
apply (force simp add: pos_less_divide_eq neg_less_divide_eq linorder_neq_iff)
done
@@ -748,7 +733,7 @@
"(b/c < a) =
(if 0 < c then b < a*c
else if c < 0 then a*c < b
- else 0 < (a::'a::{linordered_field,division_by_zero}))"
+ else 0 < (a::'a::{linordered_field,division_ring_inverse_zero}))"
apply (cases "c=0", simp)
apply (force simp add: pos_divide_less_eq neg_divide_less_eq linorder_neq_iff)
done
@@ -756,21 +741,21 @@
text {*Division and Signs*}
lemma zero_less_divide_iff:
- "((0::'a::{linordered_field,division_by_zero}) < a/b) = (0 < a & 0 < b | a < 0 & b < 0)"
+ "((0::'a::{linordered_field,division_ring_inverse_zero}) < a/b) = (0 < a & 0 < b | a < 0 & b < 0)"
by (simp add: divide_inverse zero_less_mult_iff)
lemma divide_less_0_iff:
- "(a/b < (0::'a::{linordered_field,division_by_zero})) =
+ "(a/b < (0::'a::{linordered_field,division_ring_inverse_zero})) =
(0 < a & b < 0 | a < 0 & 0 < b)"
by (simp add: divide_inverse mult_less_0_iff)
lemma zero_le_divide_iff:
- "((0::'a::{linordered_field,division_by_zero}) \<le> a/b) =
+ "((0::'a::{linordered_field,division_ring_inverse_zero}) \<le> a/b) =
(0 \<le> a & 0 \<le> b | a \<le> 0 & b \<le> 0)"
by (simp add: divide_inverse zero_le_mult_iff)
lemma divide_le_0_iff:
- "(a/b \<le> (0::'a::{linordered_field,division_by_zero})) =
+ "(a/b \<le> (0::'a::{linordered_field,division_ring_inverse_zero})) =
(0 \<le> a & b \<le> 0 | a \<le> 0 & 0 \<le> b)"
by (simp add: divide_inverse mult_le_0_iff)
@@ -779,13 +764,13 @@
text{*Simplify expressions equated with 1*}
lemma zero_eq_1_divide_iff [simp,no_atp]:
- "((0::'a::{linordered_field,division_by_zero}) = 1/a) = (a = 0)"
+ "((0::'a::{linordered_field,division_ring_inverse_zero}) = 1/a) = (a = 0)"
apply (cases "a=0", simp)
apply (auto simp add: nonzero_eq_divide_eq)
done
lemma one_divide_eq_0_iff [simp,no_atp]:
- "(1/a = (0::'a::{linordered_field,division_by_zero})) = (a = 0)"
+ "(1/a = (0::'a::{linordered_field,division_ring_inverse_zero})) = (a = 0)"
apply (cases "a=0", simp)
apply (insert zero_neq_one [THEN not_sym])
apply (auto simp add: nonzero_divide_eq_eq)
@@ -803,16 +788,16 @@
declare divide_le_0_1_iff [simp,no_atp]
lemma divide_right_mono:
- "[|a \<le> b; 0 \<le> c|] ==> a/c \<le> b/(c::'a::{linordered_field,division_by_zero})"
+ "[|a \<le> b; 0 \<le> c|] ==> a/c \<le> b/(c::'a::{linordered_field,division_ring_inverse_zero})"
by (force simp add: divide_strict_right_mono order_le_less)
-lemma divide_right_mono_neg: "(a::'a::{linordered_field,division_by_zero}) <= b
+lemma divide_right_mono_neg: "(a::'a::{linordered_field,division_ring_inverse_zero}) <= b
==> c <= 0 ==> b / c <= a / c"
apply (drule divide_right_mono [of _ _ "- c"])
apply auto
done
-lemma divide_left_mono_neg: "(a::'a::{linordered_field,division_by_zero}) <= b
+lemma divide_left_mono_neg: "(a::'a::{linordered_field,division_ring_inverse_zero}) <= b
==> c <= 0 ==> 0 < a * b ==> c / a <= c / b"
apply (drule divide_left_mono [of _ _ "- c"])
apply (auto simp add: mult_commute)
@@ -823,22 +808,22 @@
text{*Simplify quotients that are compared with the value 1.*}
lemma le_divide_eq_1 [no_atp]:
- fixes a :: "'a :: {linordered_field,division_by_zero}"
+ fixes a :: "'a :: {linordered_field,division_ring_inverse_zero}"
shows "(1 \<le> b / a) = ((0 < a & a \<le> b) | (a < 0 & b \<le> a))"
by (auto simp add: le_divide_eq)
lemma divide_le_eq_1 [no_atp]:
- fixes a :: "'a :: {linordered_field,division_by_zero}"
+ fixes a :: "'a :: {linordered_field,division_ring_inverse_zero}"
shows "(b / a \<le> 1) = ((0 < a & b \<le> a) | (a < 0 & a \<le> b) | a=0)"
by (auto simp add: divide_le_eq)
lemma less_divide_eq_1 [no_atp]:
- fixes a :: "'a :: {linordered_field,division_by_zero}"
+ fixes a :: "'a :: {linordered_field,division_ring_inverse_zero}"
shows "(1 < b / a) = ((0 < a & a < b) | (a < 0 & b < a))"
by (auto simp add: less_divide_eq)
lemma divide_less_eq_1 [no_atp]:
- fixes a :: "'a :: {linordered_field,division_by_zero}"
+ fixes a :: "'a :: {linordered_field,division_ring_inverse_zero}"
shows "(b / a < 1) = ((0 < a & b < a) | (a < 0 & a < b) | a=0)"
by (auto simp add: divide_less_eq)
@@ -846,76 +831,76 @@
text {*Conditional Simplification Rules: No Case Splits*}
lemma le_divide_eq_1_pos [simp,no_atp]:
- fixes a :: "'a :: {linordered_field,division_by_zero}"
+ fixes a :: "'a :: {linordered_field,division_ring_inverse_zero}"
shows "0 < a \<Longrightarrow> (1 \<le> b/a) = (a \<le> b)"
by (auto simp add: le_divide_eq)
lemma le_divide_eq_1_neg [simp,no_atp]:
- fixes a :: "'a :: {linordered_field,division_by_zero}"
+ fixes a :: "'a :: {linordered_field,division_ring_inverse_zero}"
shows "a < 0 \<Longrightarrow> (1 \<le> b/a) = (b \<le> a)"
by (auto simp add: le_divide_eq)
lemma divide_le_eq_1_pos [simp,no_atp]:
- fixes a :: "'a :: {linordered_field,division_by_zero}"
+ fixes a :: "'a :: {linordered_field,division_ring_inverse_zero}"
shows "0 < a \<Longrightarrow> (b/a \<le> 1) = (b \<le> a)"
by (auto simp add: divide_le_eq)
lemma divide_le_eq_1_neg [simp,no_atp]:
- fixes a :: "'a :: {linordered_field,division_by_zero}"
+ fixes a :: "'a :: {linordered_field,division_ring_inverse_zero}"
shows "a < 0 \<Longrightarrow> (b/a \<le> 1) = (a \<le> b)"
by (auto simp add: divide_le_eq)
lemma less_divide_eq_1_pos [simp,no_atp]:
- fixes a :: "'a :: {linordered_field,division_by_zero}"
+ fixes a :: "'a :: {linordered_field,division_ring_inverse_zero}"
shows "0 < a \<Longrightarrow> (1 < b/a) = (a < b)"
by (auto simp add: less_divide_eq)
lemma less_divide_eq_1_neg [simp,no_atp]:
- fixes a :: "'a :: {linordered_field,division_by_zero}"
+ fixes a :: "'a :: {linordered_field,division_ring_inverse_zero}"
shows "a < 0 \<Longrightarrow> (1 < b/a) = (b < a)"
by (auto simp add: less_divide_eq)
lemma divide_less_eq_1_pos [simp,no_atp]:
- fixes a :: "'a :: {linordered_field,division_by_zero}"
+ fixes a :: "'a :: {linordered_field,division_ring_inverse_zero}"
shows "0 < a \<Longrightarrow> (b/a < 1) = (b < a)"
by (auto simp add: divide_less_eq)
lemma divide_less_eq_1_neg [simp,no_atp]:
- fixes a :: "'a :: {linordered_field,division_by_zero}"
+ fixes a :: "'a :: {linordered_field,division_ring_inverse_zero}"
shows "a < 0 \<Longrightarrow> b/a < 1 <-> a < b"
by (auto simp add: divide_less_eq)
lemma eq_divide_eq_1 [simp,no_atp]:
- fixes a :: "'a :: {linordered_field,division_by_zero}"
+ fixes a :: "'a :: {linordered_field,division_ring_inverse_zero}"
shows "(1 = b/a) = ((a \<noteq> 0 & a = b))"
by (auto simp add: eq_divide_eq)
lemma divide_eq_eq_1 [simp,no_atp]:
- fixes a :: "'a :: {linordered_field,division_by_zero}"
+ fixes a :: "'a :: {linordered_field,division_ring_inverse_zero}"
shows "(b/a = 1) = ((a \<noteq> 0 & a = b))"
by (auto simp add: divide_eq_eq)
lemma abs_inverse [simp]:
- "\<bar>inverse (a::'a::{linordered_field,division_by_zero})\<bar> =
+ "\<bar>inverse (a::'a::{linordered_field,division_ring_inverse_zero})\<bar> =
inverse \<bar>a\<bar>"
apply (cases "a=0", simp)
apply (simp add: nonzero_abs_inverse)
done
lemma abs_divide [simp]:
- "\<bar>a / (b::'a::{linordered_field,division_by_zero})\<bar> = \<bar>a\<bar> / \<bar>b\<bar>"
+ "\<bar>a / (b::'a::{linordered_field,division_ring_inverse_zero})\<bar> = \<bar>a\<bar> / \<bar>b\<bar>"
apply (cases "b=0", simp)
apply (simp add: nonzero_abs_divide)
done
-lemma abs_div_pos: "(0::'a::{linordered_field,division_by_zero}) < y ==>
+lemma abs_div_pos: "(0::'a::{linordered_field,division_ring_inverse_zero}) < y ==>
\<bar>x\<bar> / y = \<bar>x / y\<bar>"
apply (subst abs_divide)
apply (simp add: order_less_imp_le)
done
lemma field_le_mult_one_interval:
- fixes x :: "'a\<Colon>{linordered_field,division_by_zero}"
+ fixes x :: "'a\<Colon>{linordered_field,division_ring_inverse_zero}"
assumes *: "\<And>z. \<lbrakk> 0 < z ; z < 1 \<rbrakk> \<Longrightarrow> z * x \<le> y"
shows "x \<le> y"
proof (cases "0 < x")