--- a/src/HOL/Big_Operators.thy Mon Apr 26 11:34:19 2010 +0200
+++ b/src/HOL/Big_Operators.thy Mon Apr 26 15:37:50 2010 +0200
@@ -1033,12 +1033,12 @@
by (erule finite_induct) (auto simp add: insert_Diff_if)
lemma setprod_inversef:
- fixes f :: "'b \<Rightarrow> 'a::{field,division_ring_inverse_zero}"
+ fixes f :: "'b \<Rightarrow> 'a::field_inverse_zero"
shows "finite A ==> setprod (inverse \<circ> f) A = inverse (setprod f A)"
by (erule finite_induct) auto
lemma setprod_dividef:
- fixes f :: "'b \<Rightarrow> 'a::{field,division_ring_inverse_zero}"
+ fixes f :: "'b \<Rightarrow> 'a::field_inverse_zero"
shows "finite A
==> setprod (%x. f x / g x) A = setprod f A / setprod g A"
apply (subgoal_tac
--- a/src/HOL/Complex.thy Mon Apr 26 11:34:19 2010 +0200
+++ b/src/HOL/Complex.thy Mon Apr 26 15:37:50 2010 +0200
@@ -99,7 +99,7 @@
subsection {* Multiplication and Division *}
-instantiation complex :: "{field, division_ring_inverse_zero}"
+instantiation complex :: field_inverse_zero
begin
definition
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Mon Apr 26 11:34:19 2010 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Mon Apr 26 15:37:50 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_ring_inverse_zero,field} list \<Rightarrow> 'a list \<Rightarrow> tm \<Rightarrow> 'a"
+consts Itm :: "'a::{field_char_0, field_inverse_zero} list \<Rightarrow> 'a list \<Rightarrow> tm \<Rightarrow> 'a"
primrec
"Itm vs bs (CP c) = (Ipoly vs c)"
"Itm vs bs (Bound n) = bs!n"
@@ -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_ring_inverse_zero, field})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
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_ring_inverse_zero, field})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
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_ring_inverse_zero, field})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
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_ring_inverse_zero, field})"
- shows "polynate t = 0\<^sub>p \<Longrightarrow> Ipoly bs t = (0::'a::{ring_char_0,division_ring_inverse_zero, field})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
+ shows "polynate t = 0\<^sub>p \<Longrightarrow> Ipoly bs t = (0::'a::{field_char_0, field_inverse_zero})"
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_ring_inverse_zero, field})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
shows "allpolys isnpoly (simptm p)"
by (induct p rule: simptm.induct, auto simp add: Let_def)
@@ -387,7 +387,7 @@
qed
lemma split0_nb0:
- assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero, field})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
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_ring_inverse_zero, field})"
+lemma split0_nb0'[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
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_ring_inverse_zero, field})"
+lemma isnpoly_fst_split0: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
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_ring_inverse_zero,linordered_field} list \<Rightarrow> 'a list \<Rightarrow> fm \<Rightarrow> bool"
+consts Ifm ::"'a::{linordered_field_inverse_zero} 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_ring_inverse_zero,field})"
+lemma simplt_islin[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
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_ring_inverse_zero,field})"
+lemma simple_islin[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
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_ring_inverse_zero,field})"
+lemma simpeq_islin[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
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_ring_inverse_zero,field})"
+lemma simpneq_islin[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
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_ring_inverse_zero,field})"
+lemma split0_npoly: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
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_ring_inverse_zero,field})"
+lemma simplt_nb[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
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_ring_inverse_zero,field})"
+lemma simple_nb[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
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_ring_inverse_zero,field})"
+lemma simpeq_nb[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
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_ring_inverse_zero,field})"
+lemma simpneq_nb[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
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_ring_inverse_zero,field})"
+lemma simpfm_bound0: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
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_ring_inverse_zero,field})"
+lemma assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
shows "qfree p \<Longrightarrow> islin (simpfm p)"
apply (induct p rule: simpfm.induct)
apply (simp_all add: conj_lin disj_lin)
@@ -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_ring_inverse_zero,field})"
+lemma simpfm_lin: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
shows "qfree p \<Longrightarrow> islin (simpfm p)"
by (induct p rule: simpfm.induct, auto simp add: conj_lin disj_lin)
@@ -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_ring_inverse_zero,field})" and lp: "islin p" and tnb: "tmbound0 t"
+lemma msubstneg_nb: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 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_ring_inverse_zero,field})" and lp: "islin p" and tnb: "tmbound0 t"
+lemma msubst2_nb: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 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)
@@ -3156,54 +3156,54 @@
*} "Parametric QE for linear Arithmetic over fields, Version 2"
-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}")
+lemma "\<exists>(x::'a::{linordered_field_inverse_zero, number_ring}). y \<noteq> -1 \<longrightarrow> (y + 1)*x < 0"
+ apply (frpar type: "'a::{linordered_field_inverse_zero, number_ring}" pars: "y::'a::{linordered_field_inverse_zero, number_ring}")
apply (simp add: field_simps)
apply (rule spec[where x=y])
- apply (frpar type: "'a::{linordered_field, division_ring_inverse_zero, number_ring}" pars: "z::'a::{linordered_field, division_ring_inverse_zero, number_ring}")
+ apply (frpar type: "'a::{linordered_field_inverse_zero, number_ring}" pars: "z::'a::{linordered_field_inverse_zero, number_ring}")
by simp
text{* Collins/Jones Problem *}
(*
-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"
+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"
proof-
- 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")
+ 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")
by (simp add: field_simps)
have "?rhs"
- 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 (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}")
apply (simp add: field_simps)
oops
*)
(*
-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}")
+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"
+apply (frpar type: "'a::{linordered_field_inverse_zero, number_ring}" pars: "t::'a::{linordered_field_inverse_zero, number_ring}")
oops
*)
-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}")
+lemma "\<exists>(x::'a::{linordered_field_inverse_zero, number_ring}). y \<noteq> -1 \<longrightarrow> (y + 1)*x < 0"
+ apply (frpar2 type: "'a::{linordered_field_inverse_zero, number_ring}" pars: "y::'a::{linordered_field_inverse_zero, number_ring}")
apply (simp add: field_simps)
apply (rule spec[where x=y])
- apply (frpar2 type: "'a::{linordered_field, division_ring_inverse_zero, number_ring}" pars: "z::'a::{linordered_field, division_ring_inverse_zero, number_ring}")
+ apply (frpar2 type: "'a::{linordered_field_inverse_zero, number_ring}" pars: "z::'a::{linordered_field_inverse_zero, number_ring}")
by simp
text{* Collins/Jones Problem *}
(*
-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"
+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"
proof-
- 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")
+ 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")
by (simp add: field_simps)
have "?rhs"
- 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 (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}")
apply simp
oops
*)
(*
-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}")
+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"
+apply (frpar2 type: "'a::{linordered_field_inverse_zero, number_ring}" pars: "t::'a::{linordered_field_inverse_zero, number_ring}")
apply (simp add: field_simps linorder_neq_iff[symmetric])
apply ferrack
oops
--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Mon Apr 26 11:34:19 2010 +0200
+++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Mon Apr 26 15:37:50 2010 +0200
@@ -230,7 +230,7 @@
subsection{* Semantics of the polynomial representation *}
-consts Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{ring_char_0,power,division_ring_inverse_zero,field}"
+consts Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{field_char_0, field_inverse_zero, power}"
primrec
"Ipoly bs (C c) = INum c"
"Ipoly bs (Bound n) = bs!n"
@@ -241,7 +241,7 @@
"Ipoly bs (Pw t n) = (Ipoly bs t) ^ n"
"Ipoly bs (CN c n p) = (Ipoly bs c) + (bs!n)*(Ipoly bs p)"
abbreviation
- Ipoly_syntax :: "poly \<Rightarrow> 'a list \<Rightarrow>'a::{ring_char_0,power,division_ring_inverse_zero,field}" ("\<lparr>_\<rparr>\<^sub>p\<^bsup>_\<^esup>")
+ Ipoly_syntax :: "poly \<Rightarrow> 'a list \<Rightarrow>'a::{field_char_0, field_inverse_zero, power}" ("\<lparr>_\<rparr>\<^sub>p\<^bsup>_\<^esup>")
where "\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<equiv> Ipoly bs p"
lemma Ipoly_CInt: "Ipoly bs (C (i,1)) = of_int i"
@@ -394,7 +394,7 @@
qed simp_all
lemma polymul_properties:
- assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
and np: "isnpolyh p n0" and nq: "isnpolyh q n1" and m: "m \<le> min n0 n1"
shows "isnpolyh (p *\<^sub>p q) (min n0 n1)"
and "(p *\<^sub>p q = 0\<^sub>p) = (p = 0\<^sub>p \<or> q = 0\<^sub>p)"
@@ -568,19 +568,19 @@
by(induct p q rule: polymul.induct, auto simp add: field_simps)
lemma polymul_normh:
- assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
shows "\<lbrakk>isnpolyh p n0 ; isnpolyh q n1\<rbrakk> \<Longrightarrow> isnpolyh (p *\<^sub>p q) (min n0 n1)"
using polymul_properties(1) by blast
lemma polymul_eq0_iff:
- assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
shows "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1\<rbrakk> \<Longrightarrow> (p *\<^sub>p q = 0\<^sub>p) = (p = 0\<^sub>p \<or> q = 0\<^sub>p) "
using polymul_properties(2) by blast
lemma polymul_degreen:
- assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
shows "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1 ; m \<le> min n0 n1\<rbrakk> \<Longrightarrow> degreen (p *\<^sub>p q) m = (if (p = 0\<^sub>p \<or> q = 0\<^sub>p) then 0 else degreen p m + degreen q m)"
using polymul_properties(3) by blast
lemma polymul_norm:
- assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
shows "\<lbrakk> isnpoly p; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polymul (p,q))"
using polymul_normh[of "p" "0" "q" "0"] isnpoly_def by simp
@@ -591,7 +591,7 @@
by (induct p arbitrary: n0, auto)
lemma monic_eqI: assumes np: "isnpolyh p n0"
- shows "INum (headconst p) * Ipoly bs (fst (monic p)) = (Ipoly bs p ::'a::{ring_char_0,power,division_ring_inverse_zero,field})"
+ shows "INum (headconst p) * Ipoly bs (fst (monic p)) = (Ipoly bs p ::'a::{field_char_0, field_inverse_zero, power})"
unfolding monic_def Let_def
proof(cases "headconst p = 0\<^sub>N", simp_all add: headconst_zero[OF np])
let ?h = "headconst p"
@@ -629,13 +629,13 @@
lemma polysub_norm: "\<lbrakk> isnpoly p; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polysub(p,q))"
using polyadd_norm polyneg_norm by (simp add: polysub_def)
-lemma polysub_same_0[simp]: assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
+lemma polysub_same_0[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
shows "isnpolyh p n0 \<Longrightarrow> polysub (p, p) = 0\<^sub>p"
unfolding polysub_def split_def fst_conv snd_conv
by (induct p arbitrary: n0,auto simp add: Let_def Nsub0[simplified Nsub_def])
lemma polysub_0:
- assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
shows "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1\<rbrakk> \<Longrightarrow> (p -\<^sub>p q = 0\<^sub>p) = (p = q)"
unfolding polysub_def split_def fst_conv snd_conv
apply (induct p q arbitrary: n0 n1 rule:polyadd.induct, simp_all add: Nsub0[simplified Nsub_def])
@@ -657,7 +657,7 @@
done
text{* polypow is a power function and preserves normal forms *}
-lemma polypow[simp]: "Ipoly bs (polypow n p) = ((Ipoly bs p :: 'a::{field, division_ring_inverse_zero, ring_char_0})) ^ n"
+lemma polypow[simp]: "Ipoly bs (polypow n p) = ((Ipoly bs p :: 'a::{field_char_0, field_inverse_zero})) ^ n"
proof(induct n rule: polypow.induct)
case 1 thus ?case by simp
next
@@ -688,7 +688,7 @@
qed
lemma polypow_normh:
- assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
shows "isnpolyh p n \<Longrightarrow> isnpolyh (polypow k p) n"
proof (induct k arbitrary: n rule: polypow.induct)
case (2 k n)
@@ -701,17 +701,17 @@
qed auto
lemma polypow_norm:
- assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
shows "isnpoly p \<Longrightarrow> isnpoly (polypow k p)"
by (simp add: polypow_normh isnpoly_def)
text{* Finally the whole normalization*}
-lemma polynate[simp]: "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{field, division_ring_inverse_zero, ring_char_0})"
+lemma polynate[simp]: "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{field_char_0, field_inverse_zero})"
by (induct p rule:polynate.induct, auto)
lemma polynate_norm[simp]:
- assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
shows "isnpoly (polynate p)"
by (induct p rule: polynate.induct, simp_all add: polyadd_norm polymul_norm polysub_norm polyneg_norm polypow_norm) (simp_all add: isnpoly_def)
@@ -736,14 +736,14 @@
shows "isnpolyh (funpow k f p) n"
using f np by (induct k arbitrary: p, auto)
-lemma funpow_shift1: "(Ipoly bs (funpow n shift1 p) :: 'a :: {field, division_ring_inverse_zero, ring_char_0}) = Ipoly bs (Mul (Pw (Bound 0) n) p)"
+lemma funpow_shift1: "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0, field_inverse_zero}) = Ipoly bs (Mul (Pw (Bound 0) n) p)"
by (induct n arbitrary: p, simp_all add: shift1_isnpoly shift1 power_Suc )
lemma shift1_isnpolyh: "isnpolyh p n0 \<Longrightarrow> p\<noteq> 0\<^sub>p \<Longrightarrow> isnpolyh (shift1 p) 0"
using isnpolyh_mono[where n="n0" and n'="0" and p="p"] by (simp add: shift1_def)
lemma funpow_shift1_1:
- "(Ipoly bs (funpow n shift1 p) :: 'a :: {field, division_ring_inverse_zero, ring_char_0}) = Ipoly bs (funpow n shift1 1\<^sub>p *\<^sub>p p)"
+ "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0, field_inverse_zero}) = Ipoly bs (funpow n shift1 1\<^sub>p *\<^sub>p p)"
by (simp add: funpow_shift1)
lemma poly_cmul[simp]: "Ipoly bs (poly_cmul c p) = Ipoly bs (Mul (C c) p)"
@@ -751,7 +751,7 @@
lemma behead:
assumes np: "isnpolyh p n"
- shows "Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) = (Ipoly bs p :: 'a :: {field, division_ring_inverse_zero, ring_char_0})"
+ shows "Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) = (Ipoly bs p :: 'a :: {field_char_0, field_inverse_zero})"
using np
proof (induct p arbitrary: n rule: behead.induct)
case (1 c p n) hence pn: "isnpolyh p n" by simp
@@ -981,7 +981,7 @@
by (simp add: head_eq_headn0)
lemma isnpolyh_zero_iff:
- assumes nq: "isnpolyh p n0" and eq :"\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a::{ring_char_0,power,division_ring_inverse_zero,field})"
+ assumes nq: "isnpolyh p n0" and eq :"\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a::{field_char_0, field_inverse_zero, power})"
shows "p = 0\<^sub>p"
using nq eq
proof (induct "maxindex p" arbitrary: p n0 rule: less_induct)
@@ -1033,7 +1033,7 @@
lemma isnpolyh_unique:
assumes np:"isnpolyh p n0" and nq: "isnpolyh q n1"
- shows "(\<forall>bs. \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (\<lparr>q\<rparr>\<^sub>p\<^bsup>bs\<^esup> :: 'a::{ring_char_0,power,division_ring_inverse_zero,field})) \<longleftrightarrow> p = q"
+ shows "(\<forall>bs. \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (\<lparr>q\<rparr>\<^sub>p\<^bsup>bs\<^esup> :: 'a::{field_char_0, field_inverse_zero, power})) \<longleftrightarrow> p = q"
proof(auto)
assume H: "\<forall>bs. (\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> ::'a)= \<lparr>q\<rparr>\<^sub>p\<^bsup>bs\<^esup>"
hence "\<forall>bs.\<lparr>p -\<^sub>p q\<rparr>\<^sub>p\<^bsup>bs\<^esup>= (0::'a)" by simp
@@ -1046,50 +1046,50 @@
text{* consequenses of unicity on the algorithms for polynomial normalization *}
-lemma polyadd_commute: assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
+lemma polyadd_commute: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
and np: "isnpolyh p n0" and nq: "isnpolyh q n1" shows "p +\<^sub>p q = q +\<^sub>p p"
using isnpolyh_unique[OF polyadd_normh[OF np nq] polyadd_normh[OF nq np]] by simp
lemma zero_normh: "isnpolyh 0\<^sub>p n" by simp
lemma one_normh: "isnpolyh 1\<^sub>p n" by simp
lemma polyadd_0[simp]:
- assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
and np: "isnpolyh p n0" shows "p +\<^sub>p 0\<^sub>p = p" and "0\<^sub>p +\<^sub>p p = p"
using isnpolyh_unique[OF polyadd_normh[OF np zero_normh] np]
isnpolyh_unique[OF polyadd_normh[OF zero_normh np] np] by simp_all
lemma polymul_1[simp]:
- assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
and np: "isnpolyh p n0" shows "p *\<^sub>p 1\<^sub>p = p" and "1\<^sub>p *\<^sub>p p = p"
using isnpolyh_unique[OF polymul_normh[OF np one_normh] np]
isnpolyh_unique[OF polymul_normh[OF one_normh np] np] by simp_all
lemma polymul_0[simp]:
- assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
and np: "isnpolyh p n0" shows "p *\<^sub>p 0\<^sub>p = 0\<^sub>p" and "0\<^sub>p *\<^sub>p p = 0\<^sub>p"
using isnpolyh_unique[OF polymul_normh[OF np zero_normh] zero_normh]
isnpolyh_unique[OF polymul_normh[OF zero_normh np] zero_normh] by simp_all
lemma polymul_commute:
- assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
and np:"isnpolyh p n0" and nq: "isnpolyh q n1"
shows "p *\<^sub>p q = q *\<^sub>p p"
-using isnpolyh_unique[OF polymul_normh[OF np nq] polymul_normh[OF nq np], where ?'a = "'a\<Colon>{ring_char_0,power,division_ring_inverse_zero,field}"] by simp
+using isnpolyh_unique[OF polymul_normh[OF np nq] polymul_normh[OF nq np], where ?'a = "'a\<Colon>{field_char_0, field_inverse_zero, power}"] by simp
declare polyneg_polyneg[simp]
lemma isnpolyh_polynate_id[simp]:
- assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
and np:"isnpolyh p n0" shows "polynate p = p"
- using isnpolyh_unique[where ?'a= "'a::{field, division_ring_inverse_zero, ring_char_0}", OF polynate_norm[of p, unfolded isnpoly_def] np] polynate[where ?'a = "'a::{field, division_ring_inverse_zero, ring_char_0}"] by simp
+ using isnpolyh_unique[where ?'a= "'a::{field_char_0, field_inverse_zero}", OF polynate_norm[of p, unfolded isnpoly_def] np] polynate[where ?'a = "'a::{field_char_0, field_inverse_zero}"] by simp
lemma polynate_idempotent[simp]:
- assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
shows "polynate (polynate p) = polynate p"
using isnpolyh_polynate_id[OF polynate_norm[of p, unfolded isnpoly_def]] .
lemma poly_nate_polypoly': "poly_nate bs p = polypoly' bs (polynate p)"
unfolding poly_nate_def polypoly'_def ..
-lemma poly_nate_poly: shows "poly (poly_nate bs p) = (\<lambda>x:: 'a ::{field, division_ring_inverse_zero, ring_char_0}. \<lparr>p\<rparr>\<^sub>p\<^bsup>x # bs\<^esup>)"
+lemma poly_nate_poly: shows "poly (poly_nate bs p) = (\<lambda>x:: 'a ::{field_char_0, field_inverse_zero}. \<lparr>p\<rparr>\<^sub>p\<^bsup>x # bs\<^esup>)"
using polypoly'_poly[OF polynate_norm[unfolded isnpoly_def], symmetric, of bs p]
unfolding poly_nate_polypoly' by (auto intro: ext)
@@ -1116,7 +1116,7 @@
qed
lemma degree_polysub_samehead:
- assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
and np: "isnpolyh p n0" and nq: "isnpolyh q n1" and h: "head p = head q"
and d: "degree p = degree q"
shows "degree (p -\<^sub>p q) < degree p \<or> (p -\<^sub>p q = 0\<^sub>p)"
@@ -1226,7 +1226,7 @@
done
lemma polymul_head_polyeq:
- assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
shows "\<lbrakk>isnpolyh p n0; isnpolyh q n1 ; p \<noteq> 0\<^sub>p ; q \<noteq> 0\<^sub>p \<rbrakk> \<Longrightarrow> head (p *\<^sub>p q) = head p *\<^sub>p head q"
proof (induct p q arbitrary: n0 n1 rule: polymul.induct)
case (2 a b c' n' p' n0 n1)
@@ -1300,7 +1300,7 @@
by (induct p arbitrary: n0 rule: polyneg.induct, auto)
lemma degree_polymul:
- assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
and np: "isnpolyh p n0" and nq: "isnpolyh q n1"
shows "degree (p *\<^sub>p q) \<le> degree p + degree q"
using polymul_degreen[OF np nq, where m="0"] degree_eq_degreen0 by simp
@@ -1344,7 +1344,7 @@
qed
lemma polydivide_aux_properties:
- assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
and np: "isnpolyh p n0" and ns: "isnpolyh s n1"
and ap: "head p = a" and ndp: "degree p = n" and pnz: "p \<noteq> 0\<^sub>p"
shows "polydivide_aux_dom (a,n,p,k,s) \<and>
@@ -1415,19 +1415,19 @@
from polyadd_normh[OF polymul_normh[OF np
polyadd_normh[OF polymul_normh[OF nakk' nxdn] nq]] nr']
have nqr': "isnpolyh (p *\<^sub>p (?akk' *\<^sub>p ?xdn +\<^sub>p q) +\<^sub>p r) 0" by simp
- from asp have "\<forall> (bs:: 'a::{field, division_ring_inverse_zero, ring_char_0} list). Ipoly bs (a^\<^sub>p (k' - k) *\<^sub>p (s -\<^sub>p ?p')) =
+ from asp have "\<forall> (bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a^\<^sub>p (k' - k) *\<^sub>p (s -\<^sub>p ?p')) =
Ipoly bs (p *\<^sub>p q +\<^sub>p r)" by simp
- hence " \<forall>(bs:: 'a::{field, division_ring_inverse_zero, ring_char_0} list). Ipoly bs (a^\<^sub>p (k' - k)*\<^sub>p s) =
+ hence " \<forall>(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a^\<^sub>p (k' - k)*\<^sub>p s) =
Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs ?p' + Ipoly bs p * Ipoly bs q + Ipoly bs r"
by (simp add: field_simps)
- hence " \<forall>(bs:: 'a::{field, division_ring_inverse_zero, ring_char_0} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
+ hence " \<forall>(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 1\<^sub>p *\<^sub>p p)
+ Ipoly bs p * Ipoly bs q + Ipoly bs r"
by (auto simp only: funpow_shift1_1)
- hence "\<forall>(bs:: 'a::{field, division_ring_inverse_zero, ring_char_0} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
+ hence "\<forall>(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
Ipoly bs p * (Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 1\<^sub>p)
+ Ipoly bs q) + Ipoly bs r" by (simp add: field_simps)
- hence "\<forall>(bs:: 'a::{field, division_ring_inverse_zero, ring_char_0} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
+ hence "\<forall>(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
Ipoly bs (p *\<^sub>p ((a^\<^sub>p (k' - k)) *\<^sub>p (funpow (degree s - n) shift1 1\<^sub>p) +\<^sub>p q) +\<^sub>p r)" by simp
with isnpolyh_unique[OF nakks' nqr']
have "a ^\<^sub>p (k' - k) *\<^sub>p s =
@@ -1444,9 +1444,9 @@
apply (simp) by (rule polydivide_aux_real_domintros, simp_all)
have dom: ?dths apply (rule polydivide_aux_real_domintros)
using ba dn' domsp by simp_all
- from spz isnpolyh_unique[OF polysub_normh[OF ns np'], where q="0\<^sub>p", symmetric, where ?'a = "'a::{field, division_ring_inverse_zero, ring_char_0}"]
- have " \<forall>(bs:: 'a::{field, division_ring_inverse_zero, ring_char_0} list). Ipoly bs s = Ipoly bs ?p'" by simp
- hence "\<forall>(bs:: 'a::{field, division_ring_inverse_zero, ring_char_0} list). Ipoly bs s = Ipoly bs (?xdn *\<^sub>p p)" using np nxdn apply simp
+ from spz isnpolyh_unique[OF polysub_normh[OF ns np'], where q="0\<^sub>p", symmetric, where ?'a = "'a::{field_char_0, field_inverse_zero}"]
+ have " \<forall>(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs s = Ipoly bs ?p'" by simp
+ hence "\<forall>(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs s = Ipoly bs (?xdn *\<^sub>p p)" using np nxdn apply simp
by (simp only: funpow_shift1_1) simp
hence sp': "s = ?xdn *\<^sub>p p" using isnpolyh_unique[OF ns polymul_normh[OF nxdn np]] by blast
{assume h1: "polydivide_aux (a,n,p,k,s) = (k',r)"
@@ -1501,7 +1501,7 @@
and dr: "degree r = 0 \<or> degree r < degree p"
and qr: "a ^\<^sub>p (k' - Suc k) *\<^sub>p ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) = p *\<^sub>p q +\<^sub>p r" by auto
from kk' have kk'':"Suc (k' - Suc k) = k' - k" by arith
- {fix bs:: "'a::{field, division_ring_inverse_zero, ring_char_0} list"
+ {fix bs:: "'a::{field_char_0, field_inverse_zero} list"
from qr isnpolyh_unique[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - Suc k", simplified ap] nasbp', symmetric]
have "Ipoly bs (a ^\<^sub>p (k' - Suc k) *\<^sub>p ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p'))) = Ipoly bs (p *\<^sub>p q +\<^sub>p r)" by simp
@@ -1511,7 +1511,7 @@
by (simp add:kk'' funpow_shift1_1[where n="degree s - n" and p="p"])
hence "Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = Ipoly bs p * (Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?xdn) + Ipoly bs r"
by (simp add: field_simps)}
- hence ieq:"\<forall>(bs :: 'a::{field, division_ring_inverse_zero, ring_char_0} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
+ hence ieq:"\<forall>(bs :: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
Ipoly bs (p *\<^sub>p (q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)) +\<^sub>p r)" by auto
let ?q = "q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)"
from polyadd_normh[OF nq polymul_normh[OF polymul_normh[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - Suc k"] head_isnpolyh[OF ns], simplified ap ] nxdn]]
@@ -1532,17 +1532,17 @@
apply (simp) by (rule polydivide_aux_real_domintros, simp_all)
have dom: ?dths using sz ba dn' domsp
by - (rule polydivide_aux_real_domintros, simp_all)
- {fix bs :: "'a::{field, division_ring_inverse_zero, ring_char_0} list"
+ {fix bs :: "'a::{field_char_0, field_inverse_zero} list"
from isnpolyh_unique[OF nth, where ?'a="'a" and q="0\<^sub>p",simplified,symmetric] spz
have "Ipoly bs (a*\<^sub>p s) = Ipoly bs ?b * Ipoly bs ?p'" by simp
hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (?b *\<^sub>p ?xdn) * Ipoly bs p"
by (simp add: funpow_shift1_1[where n="degree s - n" and p="p"])
hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" by simp
}
- hence hth: "\<forall> (bs:: 'a::{field, division_ring_inverse_zero, ring_char_0} list). Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" ..
+ hence hth: "\<forall> (bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" ..
from hth
have asq: "a *\<^sub>p s = p *\<^sub>p (?b *\<^sub>p ?xdn)"
- using isnpolyh_unique[where ?'a = "'a::{field, division_ring_inverse_zero, ring_char_0}", OF polymul_normh[OF head_isnpolyh[OF np] ns]
+ using isnpolyh_unique[where ?'a = "'a::{field_char_0, field_inverse_zero}", OF polymul_normh[OF head_isnpolyh[OF np] ns]
polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]],
simplified ap] by simp
{assume h1: "polydivide_aux (a,n,p,k,s) = (k', r)"
@@ -1566,7 +1566,7 @@
qed
lemma polydivide_properties:
- assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
and np: "isnpolyh p n0" and ns: "isnpolyh s n1" and pnz: "p \<noteq> 0\<^sub>p"
shows "(\<exists> k r. polydivide s p = (k,r) \<and> (\<exists>nr. isnpolyh r nr) \<and> (degree r = 0 \<or> degree r < degree p)
\<and> (\<exists>q n1. isnpolyh q n1 \<and> ((polypow k (head p)) *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)))"
@@ -1698,11 +1698,11 @@
definition "swapnorm n m t = polynate (swap n m t)"
lemma swapnorm: assumes nbs: "n < length bs" and mbs: "m < length bs"
- shows "((Ipoly bs (swapnorm n m t) :: 'a\<Colon>{field, division_ring_inverse_zero, ring_char_0})) = Ipoly ((bs[n:= bs!m])[m:= bs!n]) t"
+ shows "((Ipoly bs (swapnorm n m t) :: 'a\<Colon>{field_char_0, field_inverse_zero})) = Ipoly ((bs[n:= bs!m])[m:= bs!n]) t"
using swap[OF prems] swapnorm_def by simp
lemma swapnorm_isnpoly[simp]:
- assumes "SORT_CONSTRAINT('a::{field, division_ring_inverse_zero, ring_char_0})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
shows "isnpoly (swapnorm n m p)"
unfolding swapnorm_def by simp
--- a/src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy Mon Apr 26 11:34:19 2010 +0200
+++ b/src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy Mon Apr 26 15:37:50 2010 +0200
@@ -7,147 +7,147 @@
begin
lemma
- "\<exists>(y::'a::{linordered_field, division_ring_inverse_zero, number_ring}) <2. x + 3* y < 0 \<and> x - y >0"
+ "\<exists>(y::'a::{linordered_field_inverse_zero, number_ring}) <2. x + 3* y < 0 \<and> x - y >0"
by ferrack
-lemma "~ (ALL x (y::'a::{linordered_field, division_ring_inverse_zero, number_ring}). x < y --> 10*x < 11*y)"
+lemma "~ (ALL x (y::'a::{linordered_field_inverse_zero, number_ring}). x < y --> 10*x < 11*y)"
by ferrack
-lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. x < y --> (10*(x + 5*y + -1) < 60*y)"
+lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}) y. x < y --> (10*(x + 5*y + -1) < 60*y)"
by ferrack
-lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. x ~= y --> x < y"
+lemma "EX (x::'a::{linordered_field_inverse_zero, number_ring}) y. x ~= y --> x < y"
by ferrack
-lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. (x ~= y & 10*x ~= 9*y & 10*x < y) --> x < y"
+lemma "EX (x::'a::{linordered_field_inverse_zero, number_ring}) y. (x ~= y & 10*x ~= 9*y & 10*x < y) --> x < y"
by ferrack
-lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. (x ~= y & 5*x <= y) --> 500*x <= 100*y"
+lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}) y. (x ~= y & 5*x <= y) --> 500*x <= 100*y"
by ferrack
-lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). (EX (y::'a::{linordered_field, division_ring_inverse_zero, number_ring}). 4*x + 3*y <= 0 & 4*x + 3*y >= -1)"
+lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}). (EX (y::'a::{linordered_field_inverse_zero, number_ring}). 4*x + 3*y <= 0 & 4*x + 3*y >= -1)"
by ferrack
-lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) < 0. (EX (y::'a::{linordered_field, division_ring_inverse_zero, number_ring}) > 0. 7*x + y > 0 & x - y <= 9)"
+lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}) < 0. (EX (y::'a::{linordered_field_inverse_zero, number_ring}) > 0. 7*x + y > 0 & x - y <= 9)"
by ferrack
-lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). (0 < x & x < 1) --> (ALL y > 1. x + y ~= 1)"
+lemma "EX (x::'a::{linordered_field_inverse_zero, number_ring}). (0 < x & x < 1) --> (ALL y > 1. x + y ~= 1)"
by ferrack
-lemma "EX x. (ALL (y::'a::{linordered_field, division_ring_inverse_zero, number_ring}). y < 2 --> 2*(y - x) \<le> 0 )"
+lemma "EX x. (ALL (y::'a::{linordered_field_inverse_zero, number_ring}). y < 2 --> 2*(y - x) \<le> 0 )"
by ferrack
-lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). x < 10 | x > 20 | (EX y. y>= 0 & y <= 10 & x+y = 20)"
+lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}). x < 10 | x > 20 | (EX y. y>= 0 & y <= 10 & x+y = 20)"
by ferrack
-lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y z. x + y < z --> y >= z --> x < 0"
+lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}) y z. x + y < z --> y >= z --> x < 0"
by ferrack
-lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y z. x + 7*y < 5* z & 5*y >= 7*z & x < 0"
+lemma "EX (x::'a::{linordered_field_inverse_zero, number_ring}) y z. x + 7*y < 5* z & 5*y >= 7*z & x < 0"
by ferrack
-lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y z. abs (x + y) <= z --> (abs z = z)"
+lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}) y z. abs (x + y) <= z --> (abs z = z)"
by ferrack
-lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y z. x + 7*y - 5* z < 0 & 5*y + 7*z + 3*x < 0"
+lemma "EX (x::'a::{linordered_field_inverse_zero, number_ring}) y z. x + 7*y - 5* z < 0 & 5*y + 7*z + 3*x < 0"
by ferrack
-lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y z. (abs (5*x+3*y+z) <= 5*x+3*y+z & abs (5*x+3*y+z) >= - (5*x+3*y+z)) | (abs (5*x+3*y+z) >= 5*x+3*y+z & abs (5*x+3*y+z) <= - (5*x+3*y+z))"
+lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}) y z. (abs (5*x+3*y+z) <= 5*x+3*y+z & abs (5*x+3*y+z) >= - (5*x+3*y+z)) | (abs (5*x+3*y+z) >= 5*x+3*y+z & abs (5*x+3*y+z) <= - (5*x+3*y+z))"
by ferrack
-lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. x < y --> (EX z>0. x+z = y)"
+lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}) y. x < y --> (EX z>0. x+z = y)"
by ferrack
-lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. x < y --> (EX z>0. x+z = y)"
+lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}) y. x < y --> (EX z>0. x+z = y)"
by ferrack
-lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. (EX z>0. abs (x - y) <= z )"
+lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}) y. (EX z>0. abs (x - y) <= z )"
by ferrack
-lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))"
+lemma "EX (x::'a::{linordered_field_inverse_zero, number_ring}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))"
by ferrack
-lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. (ALL z>=0. abs (3*x+7*y) <= 2*z + 1)"
+lemma "EX (x::'a::{linordered_field_inverse_zero, number_ring}) y. (ALL z>=0. abs (3*x+7*y) <= 2*z + 1)"
by ferrack
-lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))"
+lemma "EX (x::'a::{linordered_field_inverse_zero, number_ring}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))"
by ferrack
-lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring})>0. (ALL y. (EX z. 13* abs z \<noteq> abs (12*y - x) & 5*x - 3*(abs y) <= 7*z))"
+lemma "EX (x::'a::{linordered_field_inverse_zero, number_ring})>0. (ALL y. (EX z. 13* abs z \<noteq> abs (12*y - x) & 5*x - 3*(abs y) <= 7*z))"
by ferrack
-lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). abs (4*x + 17) < 4 & (ALL y . abs (x*34 - 34*y - 9) \<noteq> 0 \<longrightarrow> (EX z. 5*x - 3*abs y <= 7*z))"
+lemma "EX (x::'a::{linordered_field_inverse_zero, number_ring}). abs (4*x + 17) < 4 & (ALL y . abs (x*34 - 34*y - 9) \<noteq> 0 \<longrightarrow> (EX z. 5*x - 3*abs y <= 7*z))"
by ferrack
-lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). (EX y > abs (23*x - 9). (ALL z > abs (3*y - 19* abs x). x+z > 2*y))"
+lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}). (EX y > abs (23*x - 9). (ALL z > abs (3*y - 19* abs x). x+z > 2*y))"
by ferrack
-lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). (EX y< abs (3*x - 1). (ALL z >= (3*abs x - 1). abs (12*x - 13*y + 19*z) > abs (23*x) ))"
+lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}). (EX y< abs (3*x - 1). (ALL z >= (3*abs x - 1). abs (12*x - 13*y + 19*z) > abs (23*x) ))"
by ferrack
-lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). abs x < 100 & (ALL y > x. (EX z<2*y - x. 5*x - 3*y <= 7*z))"
+lemma "EX (x::'a::{linordered_field_inverse_zero, number_ring}). abs x < 100 & (ALL y > x. (EX z<2*y - x. 5*x - 3*y <= 7*z))"
by ferrack
-lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y z w. 7*x<3*y --> 5*y < 7*z --> z < 2*w --> 7*(2*w-x) > 2*y"
+lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}) y z w. 7*x<3*y --> 5*y < 7*z --> z < 2*w --> 7*(2*w-x) > 2*y"
by ferrack
-lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y z w. 5*x + 3*z - 17*w + abs (y - 8*x + z) <= 89"
+lemma "EX (x::'a::{linordered_field_inverse_zero, number_ring}) y z w. 5*x + 3*z - 17*w + abs (y - 8*x + z) <= 89"
by ferrack
-lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y z w. 5*x + 3*z - 17*w + 7* (y - 8*x + z) <= max y (7*z - x + w)"
+lemma "EX (x::'a::{linordered_field_inverse_zero, number_ring}) y z w. 5*x + 3*z - 17*w + 7* (y - 8*x + z) <= max y (7*z - x + w)"
by ferrack
-lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)"
+lemma "EX (x::'a::{linordered_field_inverse_zero, number_ring}) y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)"
by ferrack
-lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y z. (EX w >= (x+y+z). w <= abs x + abs y + abs z)"
+lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}) y z. (EX w >= (x+y+z). w <= abs x + abs y + abs z)"
by ferrack
-lemma "~(ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). (EX y z w. 3* x + z*4 = 3*y & x + y < z & x> w & 3*x < w + y))"
+lemma "~(ALL (x::'a::{linordered_field_inverse_zero, number_ring}). (EX y z w. 3* x + z*4 = 3*y & x + y < z & x> w & 3*x < w + y))"
by ferrack
-lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. (EX z w. abs (x-y) = (z-w) & z*1234 < 233*x & w ~= y)"
+lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}) y. (EX z w. abs (x-y) = (z-w) & z*1234 < 233*x & w ~= y)"
by ferrack
-lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). (EX y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w))"
+lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}). (EX y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w))"
by ferrack
-lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y z. (ALL w >= abs (x+y+z). w >= abs x + abs y + abs z)"
+lemma "EX (x::'a::{linordered_field_inverse_zero, number_ring}) y z. (ALL w >= abs (x+y+z). w >= abs x + abs y + abs z)"
by ferrack
-lemma "EX z. (ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. (EX w >= (x+y+z). w <= abs x + abs y + abs z))"
+lemma "EX z. (ALL (x::'a::{linordered_field_inverse_zero, number_ring}) y. (EX w >= (x+y+z). w <= abs x + abs y + abs z))"
by ferrack
-lemma "EX z. (ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) < abs z. (EX y w. x< y & x < z & x> w & 3*x < w + y))"
+lemma "EX z. (ALL (x::'a::{linordered_field_inverse_zero, number_ring}) < abs z. (EX y w. x< y & x < z & x> w & 3*x < w + y))"
by ferrack
-lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y. (EX z. (ALL w. abs (x-y) = abs (z-w) --> z < x & w ~= y))"
+lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}) y. (EX z. (ALL w. abs (x-y) = abs (z-w) --> z < x & w ~= y))"
by ferrack
-lemma "EX y. (ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). (EX z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)))"
+lemma "EX y. (ALL (x::'a::{linordered_field_inverse_zero, number_ring}). (EX z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)))"
by ferrack
-lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) z. (ALL w >= 13*x - 4*z. (EX y. w >= abs x + abs y + z))"
+lemma "EX (x::'a::{linordered_field_inverse_zero, number_ring}) z. (ALL w >= 13*x - 4*z. (EX y. w >= abs x + abs y + z))"
by ferrack
-lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). (ALL y < x. (EX z > (x+y).
+lemma "EX (x::'a::{linordered_field_inverse_zero, number_ring}). (ALL y < x. (EX z > (x+y).
(ALL w. 5*w + 10*x - z >= y --> w + 7*x + 3*z >= 2*y)))"
by ferrack
-lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). (ALL y. (EX z > y.
+lemma "EX (x::'a::{linordered_field_inverse_zero, number_ring}). (ALL y. (EX z > y.
(ALL w . w < 13 --> w + 10*x - z >= y --> 5*w + 7*x + 13*z >= 2*y)))"
by ferrack
-lemma "EX (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}) y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)"
+lemma "EX (x::'a::{linordered_field_inverse_zero, number_ring}) y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)"
by ferrack
-lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). (EX y. (ALL z>19. y <= x + z & (EX w. abs (y - x) < w)))"
+lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}). (EX y. (ALL z>19. y <= x + z & (EX w. abs (y - x) < w)))"
by ferrack
-lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). (EX y. (ALL z>19. y <= x + z & (EX w. abs (x + z) < w - y)))"
+lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}). (EX y. (ALL z>19. y <= x + z & (EX w. abs (x + z) < w - y)))"
by ferrack
-lemma "ALL (x::'a::{linordered_field, division_ring_inverse_zero, number_ring}). (EX y. abs y ~= abs x & (ALL z> max x y. (EX w. w ~= y & w ~= z & 3*w - z >= x + y)))"
+lemma "ALL (x::'a::{linordered_field_inverse_zero, number_ring}). (EX y. abs y ~= abs x & (ALL z> max x y. (EX w. w ~= y & w ~= z & 3*w - z >= x + y)))"
by ferrack
end
--- a/src/HOL/Fields.thy Mon Apr 26 11:34:19 2010 +0200
+++ b/src/HOL/Fields.thy Mon Apr 26 15:37:50 2010 +0200
@@ -129,22 +129,20 @@
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_ring_inverse_zero})"
- proof cases
- assume "a \<noteq> 0 & b \<noteq> 0"
- thus ?thesis by (simp add: nonzero_inverse_mult_distrib mult_ac)
- next
- assume "~ (a \<noteq> 0 & b \<noteq> 0)"
- thus ?thesis by force
- qed
+ "inverse (a * b) = inverse a * inverse b"
+proof cases
+ assume "a \<noteq> 0 & b \<noteq> 0"
+ thus ?thesis by (simp add: nonzero_inverse_mult_distrib mult_ac)
+next
+ assume "~ (a \<noteq> 0 & b \<noteq> 0)"
+ thus ?thesis by force
+qed
lemma inverse_divide [simp]:
- "inverse (a/b) = b / (a::'a::{field,division_ring_inverse_zero})"
+ "inverse (a / b) = b / a"
by (simp add: divide_inverse mult_commute)
@@ -155,86 +153,88 @@
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_ring_inverse_zero})"
+ "c \<noteq> 0 \<Longrightarrow> (c * a) / (c * b) = a / b"
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_ring_inverse_zero})"
+ "c \<noteq> 0 \<Longrightarrow> (a * c) / (b * c) = a / b"
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_ring_inverse_zero})"
-by (simp add: divide_inverse mult_ac)
+lemma divide_divide_eq_right [simp, no_atp]:
+ "a / (b / c) = (a * c) / b"
+ by (simp add: divide_inverse mult_ac)
-lemma divide_divide_eq_left [simp,no_atp]:
- "(a / b) / (c::'a::{field,division_ring_inverse_zero}) = a / (b*c)"
-by (simp add: divide_inverse mult_assoc)
+lemma divide_divide_eq_left [simp, no_atp]:
+ "(a / b) / c = 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_ring_inverse_zero}"
-shows "(c*a) / (c*b) = (if c=0 then 0 else a/b)"
-by (simp add: mult_divide_mult_cancel_left)
+lemma mult_divide_mult_cancel_left_if [simp,no_atp]:
+ 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_ring_inverse_zero})"
-by (simp add: divide_inverse)
+lemma minus_divide_right:
+ "- (a / b) = a / - b"
+ by (simp add: divide_inverse)
lemma divide_minus_right [simp, no_atp]:
- "a / -(b::'a::{field,division_ring_inverse_zero}) = -(a / b)"
-by (simp add: divide_inverse)
+ "a / - b = - (a / b)"
+ by (simp add: divide_inverse)
lemma minus_divide_divide:
- "(-a)/(-b) = a / (b::'a::{field,division_ring_inverse_zero})"
+ "(- a) / (- b) = a / b"
apply (cases "b=0", simp)
apply (simp add: nonzero_minus_divide_divide)
done
lemma eq_divide_eq:
- "((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)
+ "a = b / c \<longleftrightarrow> (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_ring_inverse_zero})) = (if c\<noteq>0 then b = a*c else a=0)"
-by (force simp add: nonzero_divide_eq_eq)
+ "b / c = a \<longleftrightarrow> (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_ring_inverse_zero}))"
-by (insert inverse_eq_iff_eq [of x 1], simp)
+ "inverse x = 1 \<longleftrightarrow> x = 1"
+ 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_ring_inverse_zero}))"
-by (simp add: divide_inverse)
+lemma divide_eq_0_iff [simp, no_atp]:
+ "a / b = 0 \<longleftrightarrow> a = 0 \<or> b = 0"
+ by (simp add: divide_inverse)
-lemma divide_cancel_right [simp,no_atp]:
- "(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_right [simp, no_atp]:
+ "a / c = b / c \<longleftrightarrow> c = 0 \<or> a = b"
+ 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_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 \<longleftrightarrow> c = 0 \<or> a = b"
+ 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_ring_inverse_zero}))"
-apply (cases "b=0", simp)
-apply (simp add: right_inverse_eq)
-done
+lemma divide_eq_1_iff [simp, no_atp]:
+ "a / b = 1 \<longleftrightarrow> b \<noteq> 0 \<and> a = b"
+ 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_ring_inverse_zero}))"
-by (simp add: eq_commute [of 1])
+lemma one_eq_divide_iff [simp, no_atp]:
+ "1 = a / b \<longleftrightarrow> b \<noteq> 0 \<and> a = b"
+ by (simp add: eq_commute [of 1])
+
+end
text {* Ordered Fields *}
@@ -650,39 +650,37 @@
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_ring_inverse_zero}))"
+ else a \<le> 0)"
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_ring_inverse_zero}))"
+ "(0 < inverse a) = (0 < a)"
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_ring_inverse_zero}))"
+ "(inverse a < 0) = (a < 0)"
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_ring_inverse_zero}))"
-by (simp add: linorder_not_less [symmetric])
+ "0 \<le> inverse a \<longleftrightarrow> 0 \<le> a"
+ by (simp add: not_less [symmetric])
lemma inverse_nonpositive_iff_nonpositive [simp]:
- "(inverse a \<le> 0) = (a \<le> (0::'a::{linordered_field,division_ring_inverse_zero}))"
-by (simp add: linorder_not_less [symmetric])
+ "inverse a \<le> 0 \<longleftrightarrow> a \<le> 0"
+ by (simp add: not_less [symmetric])
lemma one_less_inverse_iff:
- "(1 < inverse x) = (0 < x & x < (1::'a::{linordered_field,division_ring_inverse_zero}))"
+ "1 < inverse x \<longleftrightarrow> 0 < x \<and> x < 1"
proof cases
assume "0 < x"
with inverse_less_iff_less [OF zero_less_one, of x]
@@ -692,7 +690,7 @@
have "~ (1 < inverse x)"
proof
assume "1 < inverse x"
- also with notless have "... \<le> 0" by (simp add: linorder_not_less)
+ also with notless have "... \<le> 0" by simp
also have "... < 1" by (rule zero_less_one)
finally show False by auto
qed
@@ -700,62 +698,69 @@
qed
lemma one_le_inverse_iff:
- "(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)
+ "1 \<le> inverse x \<longleftrightarrow> 0 < x \<and> x \<le> 1"
+proof (cases "x = 1")
+ case True then show ?thesis by simp
+next
+ case False then have "inverse x \<noteq> 1" by simp
+ then have "1 \<noteq> inverse x" by blast
+ then have "1 \<le> inverse x \<longleftrightarrow> 1 < inverse x" by (simp add: le_less)
+ with False show ?thesis by (auto simp add: one_less_inverse_iff)
+qed
lemma inverse_less_1_iff:
- "(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)
+ "inverse x < 1 \<longleftrightarrow> x \<le> 0 \<or> 1 < x"
+ by (simp add: 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_ring_inverse_zero}))"
-by (simp add: linorder_not_less [symmetric] one_less_inverse_iff)
+ "inverse x \<le> 1 \<longleftrightarrow> x \<le> 0 \<or> 1 \<le> x"
+ by (simp add: 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_ring_inverse_zero}))"
+ else 0 \<le> a)"
apply (cases "c=0", simp)
-apply (force simp add: pos_divide_le_eq neg_divide_le_eq linorder_neq_iff)
+apply (force simp add: pos_divide_le_eq neg_divide_le_eq)
done
lemma less_divide_eq:
"(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_ring_inverse_zero}))"
+ else a < 0)"
apply (cases "c=0", simp)
-apply (force simp add: pos_less_divide_eq neg_less_divide_eq linorder_neq_iff)
+apply (force simp add: pos_less_divide_eq neg_less_divide_eq)
done
lemma divide_less_eq:
"(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_ring_inverse_zero}))"
+ else 0 < a)"
apply (cases "c=0", simp)
-apply (force simp add: pos_divide_less_eq neg_divide_less_eq linorder_neq_iff)
+apply (force simp add: pos_divide_less_eq neg_divide_less_eq)
done
text {*Division and Signs*}
lemma zero_less_divide_iff:
- "((0::'a::{linordered_field,division_ring_inverse_zero}) < a/b) = (0 < a & 0 < b | a < 0 & b < 0)"
+ "(0 < 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_ring_inverse_zero})) =
+ "(a/b < 0) =
(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_ring_inverse_zero}) \<le> a/b) =
+ "(0 \<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_ring_inverse_zero})) =
+ "(a/b \<le> 0) =
(0 \<le> a & b \<le> 0 | a \<le> 0 & 0 \<le> b)"
by (simp add: divide_inverse mult_le_0_iff)
@@ -764,13 +769,13 @@
text{*Simplify expressions equated with 1*}
lemma zero_eq_1_divide_iff [simp,no_atp]:
- "((0::'a::{linordered_field,division_ring_inverse_zero}) = 1/a) = (a = 0)"
+ "(0 = 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_ring_inverse_zero})) = (a = 0)"
+ "(1/a = 0) = (a = 0)"
apply (cases "a=0", simp)
apply (insert zero_neq_one [THEN not_sym])
apply (auto simp add: nonzero_divide_eq_eq)
@@ -788,16 +793,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_ring_inverse_zero})"
-by (force simp add: divide_strict_right_mono order_le_less)
+ "[|a \<le> b; 0 \<le> c|] ==> a/c \<le> b/c"
+by (force simp add: divide_strict_right_mono le_less)
-lemma divide_right_mono_neg: "(a::'a::{linordered_field,division_ring_inverse_zero}) <= b
+lemma divide_right_mono_neg: "a <= 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_ring_inverse_zero}) <= b
+lemma divide_left_mono_neg: "a <= b
==> c <= 0 ==> 0 < a * b ==> c / a <= c / b"
apply (drule divide_left_mono [of _ _ "- c"])
apply (auto simp add: mult_commute)
@@ -808,99 +813,84 @@
text{*Simplify quotients that are compared with the value 1.*}
lemma le_divide_eq_1 [no_atp]:
- fixes a :: "'a :: {linordered_field,division_ring_inverse_zero}"
- shows "(1 \<le> b / a) = ((0 < a & a \<le> b) | (a < 0 & b \<le> a))"
+ "(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_ring_inverse_zero}"
- shows "(b / a \<le> 1) = ((0 < a & b \<le> a) | (a < 0 & a \<le> b) | a=0)"
+ "(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_ring_inverse_zero}"
- shows "(1 < b / a) = ((0 < a & a < b) | (a < 0 & b < a))"
+ "(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_ring_inverse_zero}"
- shows "(b / a < 1) = ((0 < a & b < a) | (a < 0 & a < b) | a=0)"
+ "(b / a < 1) = ((0 < a & b < a) | (a < 0 & a < b) | a=0)"
by (auto simp add: divide_less_eq)
text {*Conditional Simplification Rules: No Case Splits*}
lemma le_divide_eq_1_pos [simp,no_atp]:
- fixes a :: "'a :: {linordered_field,division_ring_inverse_zero}"
- shows "0 < a \<Longrightarrow> (1 \<le> b/a) = (a \<le> b)"
+ "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_ring_inverse_zero}"
- shows "a < 0 \<Longrightarrow> (1 \<le> b/a) = (b \<le> a)"
+ "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_ring_inverse_zero}"
- shows "0 < a \<Longrightarrow> (b/a \<le> 1) = (b \<le> a)"
+ "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_ring_inverse_zero}"
- shows "a < 0 \<Longrightarrow> (b/a \<le> 1) = (a \<le> b)"
+ "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_ring_inverse_zero}"
- shows "0 < a \<Longrightarrow> (1 < b/a) = (a < b)"
+ "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_ring_inverse_zero}"
- shows "a < 0 \<Longrightarrow> (1 < b/a) = (b < a)"
+ "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_ring_inverse_zero}"
- shows "0 < a \<Longrightarrow> (b/a < 1) = (b < a)"
+ "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_ring_inverse_zero}"
- shows "a < 0 \<Longrightarrow> b/a < 1 <-> a < b"
+ "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_ring_inverse_zero}"
- shows "(1 = b/a) = ((a \<noteq> 0 & a = b))"
+ "(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_ring_inverse_zero}"
- shows "(b/a = 1) = ((a \<noteq> 0 & a = b))"
+ "(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_ring_inverse_zero})\<bar> =
+ "\<bar>inverse a\<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_ring_inverse_zero})\<bar> = \<bar>a\<bar> / \<bar>b\<bar>"
+ "\<bar>a / b\<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_ring_inverse_zero}) < y ==>
+lemma abs_div_pos: "0 < 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_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")
@@ -916,6 +906,8 @@
finally show ?thesis .
qed
+end
+
code_modulename SML
Fields Arith
--- a/src/HOL/Groebner_Basis.thy Mon Apr 26 11:34:19 2010 +0200
+++ b/src/HOL/Groebner_Basis.thy Mon Apr 26 15:37:50 2010 +0200
@@ -473,21 +473,21 @@
interpretation class_fieldgb:
fieldgb "op +" "op *" "op ^" "0::'a::{field,number_ring}" "1" "op -" "uminus" "op /" "inverse" apply (unfold_locales) by (simp_all add: divide_inverse)
-lemma divide_Numeral1: "(x::'a::{field,number_ring}) / Numeral1 = x" by simp
-lemma divide_Numeral0: "(x::'a::{field,number_ring, division_ring_inverse_zero}) / Numeral0 = 0"
+lemma divide_Numeral1: "(x::'a::{field, number_ring}) / Numeral1 = x" by simp
+lemma divide_Numeral0: "(x::'a::{field_inverse_zero, number_ring}) / Numeral0 = 0"
by simp
-lemma mult_frac_frac: "((x::'a::{field,division_ring_inverse_zero}) / y) * (z / w) = (x*z) / (y*w)"
+lemma mult_frac_frac: "((x::'a::field_inverse_zero) / y) * (z / w) = (x*z) / (y*w)"
by simp
-lemma mult_frac_num: "((x::'a::{field, division_ring_inverse_zero}) / y) * z = (x*z) / y"
+lemma mult_frac_num: "((x::'a::field_inverse_zero) / y) * z = (x*z) / y"
by simp
-lemma mult_num_frac: "((x::'a::{field, division_ring_inverse_zero}) / y) * z = (x*z) / y"
+lemma mult_num_frac: "((x::'a::field_inverse_zero) / y) * z = (x*z) / y"
by simp
lemma Numeral1_eq1_nat: "(1::nat) = Numeral1" by simp
-lemma add_frac_num: "y\<noteq> 0 \<Longrightarrow> (x::'a::{field, division_ring_inverse_zero}) / y + z = (x + z*y) / y"
+lemma add_frac_num: "y\<noteq> 0 \<Longrightarrow> (x::'a::field_inverse_zero) / y + z = (x + z*y) / y"
by (simp add: add_divide_distrib)
-lemma add_num_frac: "y\<noteq> 0 \<Longrightarrow> z + (x::'a::{field, division_ring_inverse_zero}) / y = (x + z*y) / y"
+lemma add_num_frac: "y\<noteq> 0 \<Longrightarrow> z + (x::'a::field_inverse_zero) / y = (x + z*y) / y"
by (simp add: add_divide_distrib)
ML {*
--- a/src/HOL/Int.thy Mon Apr 26 11:34:19 2010 +0200
+++ b/src/HOL/Int.thy Mon Apr 26 15:37:50 2010 +0200
@@ -1995,15 +1995,15 @@
text{*Division By @{text "-1"}*}
lemma divide_minus1 [simp]:
- "x/-1 = -(x::'a::{field,division_ring_inverse_zero,number_ring})"
+ "x/-1 = -(x::'a::{field_inverse_zero, number_ring})"
by simp
lemma minus1_divide [simp]:
- "-1 / (x::'a::{field,division_ring_inverse_zero,number_ring}) = - (1/x)"
+ "-1 / (x::'a::{field_inverse_zero, number_ring}) = - (1/x)"
by (simp add: divide_inverse)
lemma half_gt_zero_iff:
- "(0 < r/2) = (0 < (r::'a::{linordered_field,division_ring_inverse_zero,number_ring}))"
+ "(0 < r/2) = (0 < (r::'a::{linordered_field_inverse_zero,number_ring}))"
by auto
lemmas half_gt_zero [simp] = half_gt_zero_iff [THEN iffD2, standard]
--- a/src/HOL/Library/Abstract_Rat.thy Mon Apr 26 11:34:19 2010 +0200
+++ b/src/HOL/Library/Abstract_Rat.thy Mon Apr 26 15:37:50 2010 +0200
@@ -184,7 +184,7 @@
lemma isnormNum_unique[simp]:
assumes na: "isnormNum x" and nb: "isnormNum y"
- shows "((INum x ::'a::{ring_char_0,field, division_ring_inverse_zero}) = INum y) = (x = y)" (is "?lhs = ?rhs")
+ shows "((INum x ::'a::{field_char_0, field_inverse_zero}) = INum y) = (x = y)" (is "?lhs = ?rhs")
proof
have "\<exists> a b a' b'. x = (a,b) \<and> y = (a',b')" by auto
then obtain a b a' b' where xy[simp]: "x = (a,b)" "y=(a',b')" by blast
@@ -217,11 +217,11 @@
qed
-lemma isnormNum0[simp]: "isnormNum x \<Longrightarrow> (INum x = (0::'a::{ring_char_0, field,division_ring_inverse_zero})) = (x = 0\<^sub>N)"
+lemma isnormNum0[simp]: "isnormNum x \<Longrightarrow> (INum x = (0::'a::{field_char_0, field_inverse_zero})) = (x = 0\<^sub>N)"
unfolding INum_int(2)[symmetric]
by (rule isnormNum_unique, simp_all)
-lemma of_int_div_aux: "d ~= 0 ==> ((of_int x)::'a::{field, ring_char_0}) / (of_int d) =
+lemma of_int_div_aux: "d ~= 0 ==> ((of_int x)::'a::field_char_0) / (of_int d) =
of_int (x div d) + (of_int (x mod d)) / ((of_int d)::'a)"
proof -
assume "d ~= 0"
@@ -238,14 +238,14 @@
qed
lemma of_int_div: "(d::int) ~= 0 ==> d dvd n ==>
- (of_int(n div d)::'a::{field, ring_char_0}) = of_int n / of_int d"
+ (of_int(n div d)::'a::field_char_0) = of_int n / of_int d"
apply (frule of_int_div_aux [of d n, where ?'a = 'a])
apply simp
apply (simp add: dvd_eq_mod_eq_0)
done
-lemma normNum[simp]: "INum (normNum x) = (INum x :: 'a::{ring_char_0,field, division_ring_inverse_zero})"
+lemma normNum[simp]: "INum (normNum x) = (INum x :: 'a::{field_char_0, field_inverse_zero})"
proof-
have "\<exists> a b. x = (a,b)" by auto
then obtain a b where x[simp]: "x = (a,b)" by blast
@@ -260,7 +260,7 @@
ultimately show ?thesis by blast
qed
-lemma INum_normNum_iff: "(INum x ::'a::{field, division_ring_inverse_zero, ring_char_0}) = INum y \<longleftrightarrow> normNum x = normNum y" (is "?lhs = ?rhs")
+lemma INum_normNum_iff: "(INum x ::'a::{field_char_0, field_inverse_zero}) = INum y \<longleftrightarrow> normNum x = normNum y" (is "?lhs = ?rhs")
proof -
have "normNum x = normNum y \<longleftrightarrow> (INum (normNum x) :: 'a) = INum (normNum y)"
by (simp del: normNum)
@@ -268,7 +268,7 @@
finally show ?thesis by simp
qed
-lemma Nadd[simp]: "INum (x +\<^sub>N y) = INum x + (INum y :: 'a :: {ring_char_0,division_ring_inverse_zero,field})"
+lemma Nadd[simp]: "INum (x +\<^sub>N y) = INum x + (INum y :: 'a :: {field_char_0, field_inverse_zero})"
proof-
let ?z = "0:: 'a"
have " \<exists> a b. x = (a,b)" " \<exists> a' b'. y = (a',b')" by auto
@@ -300,7 +300,7 @@
ultimately show ?thesis by blast
qed
-lemma Nmul[simp]: "INum (x *\<^sub>N y) = INum x * (INum y:: 'a :: {ring_char_0,division_ring_inverse_zero,field}) "
+lemma Nmul[simp]: "INum (x *\<^sub>N y) = INum x * (INum y:: 'a :: {field_char_0, field_inverse_zero}) "
proof-
let ?z = "0::'a"
have " \<exists> a b. x = (a,b)" " \<exists> a' b'. y = (a',b')" by auto
@@ -323,16 +323,16 @@
lemma Nneg[simp]: "INum (~\<^sub>N x) = - (INum x ::'a:: field)"
by (simp add: Nneg_def split_def INum_def)
-lemma Nsub[simp]: shows "INum (x -\<^sub>N y) = INum x - (INum y:: 'a :: {ring_char_0,division_ring_inverse_zero,field})"
+lemma Nsub[simp]: shows "INum (x -\<^sub>N y) = INum x - (INum y:: 'a :: {field_char_0, field_inverse_zero})"
by (simp add: Nsub_def split_def)
-lemma Ninv[simp]: "INum (Ninv x) = (1::'a :: {division_ring_inverse_zero,field}) / (INum x)"
+lemma Ninv[simp]: "INum (Ninv x) = (1::'a :: field_inverse_zero) / (INum x)"
by (simp add: Ninv_def INum_def split_def)
-lemma Ndiv[simp]: "INum (x \<div>\<^sub>N y) = INum x / (INum y ::'a :: {ring_char_0, division_ring_inverse_zero,field})" by (simp add: Ndiv_def)
+lemma Ndiv[simp]: "INum (x \<div>\<^sub>N y) = INum x / (INum y ::'a :: {field_char_0, field_inverse_zero})" by (simp add: Ndiv_def)
lemma Nlt0_iff[simp]: assumes nx: "isnormNum x"
- shows "((INum x :: 'a :: {ring_char_0,division_ring_inverse_zero,linordered_field})< 0) = 0>\<^sub>N x "
+ shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero})< 0) = 0>\<^sub>N x "
proof-
have " \<exists> a b. x = (a,b)" by simp
then obtain a b where x[simp]:"x = (a,b)" by blast
@@ -345,7 +345,7 @@
qed
lemma Nle0_iff[simp]:assumes nx: "isnormNum x"
- shows "((INum x :: 'a :: {ring_char_0,division_ring_inverse_zero,linordered_field}) \<le> 0) = 0\<ge>\<^sub>N x"
+ shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero}) \<le> 0) = 0\<ge>\<^sub>N x"
proof-
have " \<exists> a b. x = (a,b)" by simp
then obtain a b where x[simp]:"x = (a,b)" by blast
@@ -357,7 +357,7 @@
ultimately show ?thesis by blast
qed
-lemma Ngt0_iff[simp]:assumes nx: "isnormNum x" shows "((INum x :: 'a :: {ring_char_0,division_ring_inverse_zero,linordered_field})> 0) = 0<\<^sub>N x"
+lemma Ngt0_iff[simp]:assumes nx: "isnormNum x" shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero})> 0) = 0<\<^sub>N x"
proof-
have " \<exists> a b. x = (a,b)" by simp
then obtain a b where x[simp]:"x = (a,b)" by blast
@@ -369,7 +369,7 @@
ultimately show ?thesis by blast
qed
lemma Nge0_iff[simp]:assumes nx: "isnormNum x"
- shows "((INum x :: 'a :: {ring_char_0,division_ring_inverse_zero,linordered_field}) \<ge> 0) = 0\<le>\<^sub>N x"
+ shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero}) \<ge> 0) = 0\<le>\<^sub>N x"
proof-
have " \<exists> a b. x = (a,b)" by simp
then obtain a b where x[simp]:"x = (a,b)" by blast
@@ -382,7 +382,7 @@
qed
lemma Nlt_iff[simp]: assumes nx: "isnormNum x" and ny: "isnormNum y"
- shows "((INum x :: 'a :: {ring_char_0,division_ring_inverse_zero,linordered_field}) < INum y) = (x <\<^sub>N y)"
+ shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero}) < INum y) = (x <\<^sub>N y)"
proof-
let ?z = "0::'a"
have "((INum x ::'a) < INum y) = (INum (x -\<^sub>N y) < ?z)" using nx ny by simp
@@ -391,7 +391,7 @@
qed
lemma Nle_iff[simp]: assumes nx: "isnormNum x" and ny: "isnormNum y"
- shows "((INum x :: 'a :: {ring_char_0,division_ring_inverse_zero,linordered_field})\<le> INum y) = (x \<le>\<^sub>N y)"
+ shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero})\<le> INum y) = (x \<le>\<^sub>N y)"
proof-
have "((INum x ::'a) \<le> INum y) = (INum (x -\<^sub>N y) \<le> (0::'a))" using nx ny by simp
also have "\<dots> = (0\<ge>\<^sub>N (x -\<^sub>N y))" using Nle0_iff[OF Nsub_normN[OF ny]] by simp
@@ -399,7 +399,7 @@
qed
lemma Nadd_commute:
- assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
shows "x +\<^sub>N y = y +\<^sub>N x"
proof-
have n: "isnormNum (x +\<^sub>N y)" "isnormNum (y +\<^sub>N x)" by simp_all
@@ -408,7 +408,7 @@
qed
lemma [simp]:
- assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
shows "(0, b) +\<^sub>N y = normNum y"
and "(a, 0) +\<^sub>N y = normNum y"
and "x +\<^sub>N (0, b) = normNum x"
@@ -420,7 +420,7 @@
done
lemma normNum_nilpotent_aux[simp]:
- assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
assumes nx: "isnormNum x"
shows "normNum x = x"
proof-
@@ -432,7 +432,7 @@
qed
lemma normNum_nilpotent[simp]:
- assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
shows "normNum (normNum x) = normNum x"
by simp
@@ -440,11 +440,11 @@
by (simp_all add: normNum_def)
lemma normNum_Nadd:
- assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
shows "normNum (x +\<^sub>N y) = x +\<^sub>N y" by simp
lemma Nadd_normNum1[simp]:
- assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
shows "normNum x +\<^sub>N y = x +\<^sub>N y"
proof-
have n: "isnormNum (normNum x +\<^sub>N y)" "isnormNum (x +\<^sub>N y)" by simp_all
@@ -454,7 +454,7 @@
qed
lemma Nadd_normNum2[simp]:
- assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
shows "x +\<^sub>N normNum y = x +\<^sub>N y"
proof-
have n: "isnormNum (x +\<^sub>N normNum y)" "isnormNum (x +\<^sub>N y)" by simp_all
@@ -464,7 +464,7 @@
qed
lemma Nadd_assoc:
- assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
shows "x +\<^sub>N y +\<^sub>N z = x +\<^sub>N (y +\<^sub>N z)"
proof-
have n: "isnormNum (x +\<^sub>N y +\<^sub>N z)" "isnormNum (x +\<^sub>N (y +\<^sub>N z))" by simp_all
@@ -476,7 +476,7 @@
by (simp add: Nmul_def split_def Let_def gcd_commute_int mult_commute)
lemma Nmul_assoc:
- assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
assumes nx: "isnormNum x" and ny:"isnormNum y" and nz:"isnormNum z"
shows "x *\<^sub>N y *\<^sub>N z = x *\<^sub>N (y *\<^sub>N z)"
proof-
@@ -487,7 +487,7 @@
qed
lemma Nsub0:
- assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
assumes x: "isnormNum x" and y:"isnormNum y" shows "(x -\<^sub>N y = 0\<^sub>N) = (x = y)"
proof-
{ fix h :: 'a
@@ -502,7 +502,7 @@
by (simp_all add: Nmul_def Let_def split_def)
lemma Nmul_eq0[simp]:
- assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
assumes nx:"isnormNum x" and ny: "isnormNum y"
shows "(x*\<^sub>N y = 0\<^sub>N) = (x = 0\<^sub>N \<or> y = 0\<^sub>N)"
proof-
--- a/src/HOL/Library/Bit.thy Mon Apr 26 11:34:19 2010 +0200
+++ b/src/HOL/Library/Bit.thy Mon Apr 26 15:37:50 2010 +0200
@@ -49,7 +49,7 @@
subsection {* Type @{typ bit} forms a field *}
-instantiation bit :: "{field, division_ring_inverse_zero}"
+instantiation bit :: field_inverse_zero
begin
definition plus_bit_def:
--- a/src/HOL/Library/Formal_Power_Series.thy Mon Apr 26 11:34:19 2010 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy Mon Apr 26 15:37:50 2010 +0200
@@ -28,7 +28,7 @@
text{* Definition of the basic elements 0 and 1 and the basic operations of addition, negation and multiplication *}
-instantiation fps :: (zero) zero
+instantiation fps :: (zero) zero
begin
definition fps_zero_def:
@@ -40,7 +40,7 @@
lemma fps_zero_nth [simp]: "0 $ n = 0"
unfolding fps_zero_def by simp
-instantiation fps :: ("{one,zero}") one
+instantiation fps :: ("{one, zero}") one
begin
definition fps_one_def:
@@ -2649,7 +2649,7 @@
text{* The generalized binomial theorem as a consequence of @{thm E_add_mult} *}
lemma gbinomial_theorem:
- "((a::'a::{field_char_0, division_ring_inverse_zero})+b) ^ n = (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n-k))"
+ "((a::'a::{field_char_0, field_inverse_zero})+b) ^ n = (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n-k))"
proof-
from E_add_mult[of a b]
have "(E (a + b)) $ n = (E a * E b)$n" by simp
@@ -3252,7 +3252,7 @@
subsection {* Hypergeometric series *}
-definition "F as bs (c::'a::{field_char_0, division_ring_inverse_zero}) = Abs_fps (%n. (foldl (%r a. r* pochhammer a n) 1 as * c^n)/ (foldl (%r b. r * pochhammer b n) 1 bs * of_nat (fact n)))"
+definition "F as bs (c::'a::{field_char_0, field_inverse_zero}) = Abs_fps (%n. (foldl (%r a. r* pochhammer a n) 1 as * c^n)/ (foldl (%r b. r * pochhammer b n) 1 bs * of_nat (fact n)))"
lemma F_nth[simp]: "F as bs c $ n = (foldl (%r a. r* pochhammer a n) 1 as * c^n)/ (foldl (%r b. r * pochhammer b n) 1 bs * of_nat (fact n))"
by (simp add: F_def)
@@ -3321,9 +3321,9 @@
by (simp add: fps_eq_iff fps_integral_def)
lemma F_minus_nat:
- "F [- of_nat n] [- of_nat (n + m)] (c::'a::{field_char_0, division_ring_inverse_zero}) $ k = (if k <= n then pochhammer (- of_nat n) k * c ^ k /
+ "F [- of_nat n] [- of_nat (n + m)] (c::'a::{field_char_0, field_inverse_zero}) $ k = (if k <= n then pochhammer (- of_nat n) k * c ^ k /
(pochhammer (- of_nat (n + m)) k * of_nat (fact k)) else 0)"
- "F [- of_nat m] [- of_nat (m + n)] (c::'a::{field_char_0, division_ring_inverse_zero}) $ k = (if k <= m then pochhammer (- of_nat m) k * c ^ k /
+ "F [- of_nat m] [- of_nat (m + n)] (c::'a::{field_char_0, field_inverse_zero}) $ k = (if k <= m then pochhammer (- of_nat m) k * c ^ k /
(pochhammer (- of_nat (m + n)) k * of_nat (fact k)) else 0)"
by (auto simp add: pochhammer_eq_0_iff)
--- a/src/HOL/Library/Fraction_Field.thy Mon Apr 26 11:34:19 2010 +0200
+++ b/src/HOL/Library/Fraction_Field.thy Mon Apr 26 15:37:50 2010 +0200
@@ -232,7 +232,7 @@
thm mult_eq_0_iff
end
-instantiation fract :: (idom) field
+instantiation fract :: (idom) field_inverse_zero
begin
definition
@@ -263,16 +263,13 @@
next
fix q r :: "'a fract"
show "q / r = q * inverse r" by (simp add: divide_fract_def)
+next
+ show "inverse 0 = (0:: 'a fract)" by (simp add: fract_expand)
+ (simp add: fract_collapse)
qed
end
-instance fract :: (idom) division_ring_inverse_zero
-proof
- show "inverse 0 = (0:: 'a fract)" by (simp add: fract_expand)
- (simp add: fract_collapse)
-qed
-
subsubsection {* The ordered field of fractions over an ordered idom *}
--- a/src/HOL/Multivariate_Analysis/Determinants.thy Mon Apr 26 11:34:19 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Determinants.thy Mon Apr 26 15:37:50 2010 +0200
@@ -55,7 +55,7 @@
done
(* FIXME: In Finite_Set there is a useless further assumption *)
-lemma setprod_inversef: "finite A ==> setprod (inverse \<circ> f) A = (inverse (setprod f A) :: 'a:: {division_ring_inverse_zero, field})"
+lemma setprod_inversef: "finite A ==> setprod (inverse \<circ> f) A = (inverse (setprod f A) :: 'a:: field_inverse_zero)"
apply (erule finite_induct)
apply (simp)
apply simp
--- a/src/HOL/NSA/HyperDef.thy Mon Apr 26 11:34:19 2010 +0200
+++ b/src/HOL/NSA/HyperDef.thy Mon Apr 26 15:37:50 2010 +0200
@@ -140,12 +140,12 @@
lemma of_hypreal_inverse [simp]:
"\<And>x. of_hypreal (inverse x) =
- inverse (of_hypreal x :: 'a::{real_div_algebra,division_ring_inverse_zero} star)"
+ inverse (of_hypreal x :: 'a::{real_div_algebra, division_ring_inverse_zero} star)"
by transfer (rule of_real_inverse)
lemma of_hypreal_divide [simp]:
"\<And>x y. of_hypreal (x / y) =
- (of_hypreal x / of_hypreal y :: 'a::{real_field,division_ring_inverse_zero} star)"
+ (of_hypreal x / of_hypreal y :: 'a::{real_field, field_inverse_zero} star)"
by transfer (rule of_real_divide)
lemma of_hypreal_eq_iff [simp]:
@@ -454,7 +454,7 @@
by transfer (rule field_power_not_zero)
lemma hyperpow_inverse:
- "\<And>r n. r \<noteq> (0::'a::{division_ring_inverse_zero,field} star)
+ "\<And>r n. r \<noteq> (0::'a::field_inverse_zero star)
\<Longrightarrow> inverse (r pow n) = (inverse r) pow n"
by transfer (rule power_inverse)
--- a/src/HOL/NSA/NSA.thy Mon Apr 26 11:34:19 2010 +0200
+++ b/src/HOL/NSA/NSA.thy Mon Apr 26 15:37:50 2010 +0200
@@ -145,12 +145,12 @@
by transfer (rule nonzero_norm_inverse)
lemma hnorm_inverse:
- "\<And>a::'a::{real_normed_div_algebra,division_ring_inverse_zero} star.
+ "\<And>a::'a::{real_normed_div_algebra, division_ring_inverse_zero} star.
hnorm (inverse a) = inverse (hnorm a)"
by transfer (rule norm_inverse)
lemma hnorm_divide:
- "\<And>a b::'a::{real_normed_field,division_ring_inverse_zero} star.
+ "\<And>a b::'a::{real_normed_field, field_inverse_zero} star.
hnorm (a / b) = hnorm a / hnorm b"
by transfer (rule norm_divide)
--- a/src/HOL/Power.thy Mon Apr 26 11:34:19 2010 +0200
+++ b/src/HOL/Power.thy Mon Apr 26 15:37:50 2010 +0200
@@ -392,27 +392,26 @@
by (induct n)
(auto simp add: no_zero_divisors elim: contrapos_pp)
-lemma power_diff:
- fixes a :: "'a::field"
+lemma (in field) power_diff:
assumes nz: "a \<noteq> 0"
shows "n \<le> m \<Longrightarrow> a ^ (m - n) = a ^ m / a ^ n"
- by (induct m n rule: diff_induct) (simp_all add: nz)
+ by (induct m n rule: diff_induct) (simp_all add: nz field_power_not_zero)
text{*Perhaps these should be simprules.*}
lemma power_inverse:
- fixes a :: "'a::{division_ring,division_ring_inverse_zero,power}"
- shows "inverse (a ^ n) = (inverse a) ^ n"
+ fixes a :: "'a::division_ring_inverse_zero"
+ shows "inverse (a ^ n) = inverse a ^ n"
apply (cases "a = 0")
apply (simp add: power_0_left)
apply (simp add: nonzero_power_inverse)
done (* TODO: reorient or rename to inverse_power *)
lemma power_one_over:
- "1 / (a::'a::{field,division_ring_inverse_zero, power}) ^ n = (1 / a) ^ n"
+ "1 / (a::'a::{field_inverse_zero, power}) ^ n = (1 / a) ^ n"
by (simp add: divide_inverse) (rule power_inverse)
lemma power_divide:
- "(a / b) ^ n = (a::'a::{field,division_ring_inverse_zero}) ^ n / b ^ n"
+ "(a / b) ^ n = (a::'a::field_inverse_zero) ^ n / b ^ n"
apply (cases "b = 0")
apply (simp add: power_0_left)
apply (rule nonzero_power_divide)
--- a/src/HOL/Rat.thy Mon Apr 26 11:34:19 2010 +0200
+++ b/src/HOL/Rat.thy Mon Apr 26 15:37:50 2010 +0200
@@ -411,7 +411,7 @@
subsubsection {* The field of rational numbers *}
-instantiation rat :: field
+instantiation rat :: field_inverse_zero
begin
definition
@@ -440,13 +440,10 @@
next
fix q r :: rat
show "q / r = q * inverse r" by (simp add: divide_rat_def)
-qed
+qed (simp add: rat_number_expand, simp add: rat_number_collapse)
end
-instance rat :: division_ring_inverse_zero proof
-qed (simp add: rat_number_expand, simp add: rat_number_collapse)
-
subsubsection {* Various *}
@@ -624,7 +621,7 @@
end
-instance rat :: linordered_field
+instance rat :: linordered_field_inverse_zero
proof
fix q r s :: rat
show "q \<le> r ==> s + q \<le> s + r"
@@ -724,8 +721,7 @@
by (cases "b = 0", simp, simp add: of_int_rat)
moreover have "0 \<le> Fract (a mod b) b \<and> Fract (a mod b) b < 1"
unfolding Fract_of_int_quotient
- by (rule linorder_cases [of b 0])
- (simp add: divide_nonpos_neg, simp, simp add: divide_nonneg_pos)
+ by (rule linorder_cases [of b 0]) (simp add: divide_nonpos_neg, simp, simp add: divide_nonneg_pos)
ultimately show ?thesis by simp
qed
@@ -818,7 +814,7 @@
done
lemma of_rat_inverse:
- "(of_rat (inverse a)::'a::{field_char_0,division_ring_inverse_zero}) =
+ "(of_rat (inverse a)::'a::{field_char_0, field_inverse_zero}) =
inverse (of_rat a)"
by (cases "a = 0", simp_all add: nonzero_of_rat_inverse)
@@ -827,7 +823,7 @@
by (simp add: divide_inverse of_rat_mult nonzero_of_rat_inverse)
lemma of_rat_divide:
- "(of_rat (a / b)::'a::{field_char_0,division_ring_inverse_zero})
+ "(of_rat (a / b)::'a::{field_char_0, field_inverse_zero})
= of_rat a / of_rat b"
by (cases "b = 0") (simp_all add: nonzero_of_rat_divide)
@@ -968,7 +964,7 @@
done
lemma Rats_inverse [simp]:
- fixes a :: "'a::{field_char_0,division_ring_inverse_zero}"
+ fixes a :: "'a::{field_char_0, field_inverse_zero}"
shows "a \<in> Rats \<Longrightarrow> inverse a \<in> Rats"
apply (auto simp add: Rats_def)
apply (rule range_eqI)
@@ -984,7 +980,7 @@
done
lemma Rats_divide [simp]:
- fixes a b :: "'a::{field_char_0,division_ring_inverse_zero}"
+ fixes a b :: "'a::{field_char_0, field_inverse_zero}"
shows "\<lbrakk>a \<in> Rats; b \<in> Rats\<rbrakk> \<Longrightarrow> a / b \<in> Rats"
apply (auto simp add: Rats_def)
apply (rule range_eqI)
--- a/src/HOL/RealDef.thy Mon Apr 26 11:34:19 2010 +0200
+++ b/src/HOL/RealDef.thy Mon Apr 26 15:37:50 2010 +0200
@@ -266,22 +266,15 @@
subsection{*The Real Numbers form a Field*}
-instance real :: field
+lemma INVERSE_ZERO: "inverse 0 = (0::real)"
+by (simp add: real_inverse_def)
+
+instance real :: field_inverse_zero
proof
fix x y z :: real
show "x \<noteq> 0 ==> inverse x * x = 1" by (rule real_mult_inverse_left)
show "x / y = x * inverse y" by (simp add: real_divide_def)
-qed
-
-
-text{*Inverse of zero! Useful to simplify certain equations*}
-
-lemma INVERSE_ZERO: "inverse 0 = (0::real)"
-by (simp add: real_inverse_def)
-
-instance real :: division_ring_inverse_zero
-proof
- show "inverse 0 = (0::real)" by (rule INVERSE_ZERO)
+ show "inverse 0 = (0::real)" by (fact INVERSE_ZERO)
qed
@@ -426,6 +419,9 @@
by (simp only: real_sgn_def)
qed
+instance real :: linordered_field_inverse_zero proof
+qed (fact INVERSE_ZERO)
+
text{*The function @{term real_of_preal} requires many proofs, but it seems
to be essential for proving completeness of the reals from that of the
positive reals.*}
--- a/src/HOL/RealVector.thy Mon Apr 26 11:34:19 2010 +0200
+++ b/src/HOL/RealVector.thy Mon Apr 26 15:37:50 2010 +0200
@@ -207,7 +207,7 @@
by (rule inverse_unique, simp)
lemma inverse_scaleR_distrib:
- fixes x :: "'a::{real_div_algebra,division_ring_inverse_zero}"
+ fixes x :: "'a::{real_div_algebra, division_ring_inverse_zero}"
shows "inverse (scaleR a x) = scaleR (inverse a) (inverse x)"
apply (case_tac "a = 0", simp)
apply (case_tac "x = 0", simp)
@@ -250,7 +250,7 @@
lemma of_real_inverse [simp]:
"of_real (inverse x) =
- inverse (of_real x :: 'a::{real_div_algebra,division_ring_inverse_zero})"
+ inverse (of_real x :: 'a::{real_div_algebra, division_ring_inverse_zero})"
by (simp add: of_real_def inverse_scaleR_distrib)
lemma nonzero_of_real_divide:
@@ -260,7 +260,7 @@
lemma of_real_divide [simp]:
"of_real (x / y) =
- (of_real x / of_real y :: 'a::{real_field,division_ring_inverse_zero})"
+ (of_real x / of_real y :: 'a::{real_field, field_inverse_zero})"
by (simp add: divide_inverse)
lemma of_real_power [simp]:
@@ -370,7 +370,7 @@
done
lemma Reals_inverse [simp]:
- fixes a :: "'a::{real_div_algebra,division_ring_inverse_zero}"
+ fixes a :: "'a::{real_div_algebra, division_ring_inverse_zero}"
shows "a \<in> Reals \<Longrightarrow> inverse a \<in> Reals"
apply (auto simp add: Reals_def)
apply (rule range_eqI)
@@ -386,7 +386,7 @@
done
lemma Reals_divide [simp]:
- fixes a b :: "'a::{real_field,division_ring_inverse_zero}"
+ fixes a b :: "'a::{real_field, field_inverse_zero}"
shows "\<lbrakk>a \<in> Reals; b \<in> Reals\<rbrakk> \<Longrightarrow> a / b \<in> Reals"
apply (auto simp add: Reals_def)
apply (rule range_eqI)
@@ -726,7 +726,7 @@
done
lemma norm_inverse:
- fixes a :: "'a::{real_normed_div_algebra,division_ring_inverse_zero}"
+ fixes a :: "'a::{real_normed_div_algebra, division_ring_inverse_zero}"
shows "norm (inverse a) = inverse (norm a)"
apply (case_tac "a = 0", simp)
apply (erule nonzero_norm_inverse)
@@ -738,7 +738,7 @@
by (simp add: divide_inverse norm_mult nonzero_norm_inverse)
lemma norm_divide:
- fixes a b :: "'a::{real_normed_field,division_ring_inverse_zero}"
+ fixes a b :: "'a::{real_normed_field, field_inverse_zero}"
shows "norm (a / b) = norm a / norm b"
by (simp add: divide_inverse norm_mult norm_inverse)
--- a/src/HOL/Series.thy Mon Apr 26 11:34:19 2010 +0200
+++ b/src/HOL/Series.thy Mon Apr 26 15:37:50 2010 +0200
@@ -381,7 +381,7 @@
shows "norm x < 1 \<Longrightarrow> summable (\<lambda>n. x ^ n)"
by (rule geometric_sums [THEN sums_summable])
-lemma half: "0 < 1 / (2::'a::{number_ring,division_ring_inverse_zero,linordered_field})"
+lemma half: "0 < 1 / (2::'a::{number_ring,linordered_field_inverse_zero})"
by arith
lemma power_half_series: "(\<lambda>n. (1/2::real)^Suc n) sums 1"
--- a/src/HOL/Tools/numeral_simprocs.ML Mon Apr 26 11:34:19 2010 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML Mon Apr 26 15:37:50 2010 +0200
@@ -332,8 +332,8 @@
val field_combine_numerals =
Arith_Data.prep_simproc @{theory}
("field_combine_numerals",
- ["(i::'a::{number_ring,field,division_ring_inverse_zero}) + j",
- "(i::'a::{number_ring,field,division_ring_inverse_zero}) - j"],
+ ["(i::'a::{field_inverse_zero, number_ring}) + j",
+ "(i::'a::{field_inverse_zero, number_ring}) - j"],
K FieldCombineNumerals.proc);
(** Constant folding for multiplication in semirings **)
@@ -442,9 +442,9 @@
"(l::'a::{semiring_div,number_ring}) div (m * n)"],
K DivCancelNumeralFactor.proc),
("divide_cancel_numeral_factor",
- ["((l::'a::{division_ring_inverse_zero,field,number_ring}) * m) / n",
- "(l::'a::{division_ring_inverse_zero,field,number_ring}) / (m * n)",
- "((number_of v)::'a::{division_ring_inverse_zero,field,number_ring}) / (number_of w)"],
+ ["((l::'a::{field_inverse_zero,number_ring}) * m) / n",
+ "(l::'a::{field_inverse_zero,number_ring}) / (m * n)",
+ "((number_of v)::'a::{field_inverse_zero,number_ring}) / (number_of w)"],
K DivideCancelNumeralFactor.proc)];
val field_cancel_numeral_factors =
@@ -454,9 +454,9 @@
"(l::'a::{field,number_ring}) = m * n"],
K EqCancelNumeralFactor.proc),
("field_cancel_numeral_factor",
- ["((l::'a::{division_ring_inverse_zero,field,number_ring}) * m) / n",
- "(l::'a::{division_ring_inverse_zero,field,number_ring}) / (m * n)",
- "((number_of v)::'a::{division_ring_inverse_zero,field,number_ring}) / (number_of w)"],
+ ["((l::'a::{field_inverse_zero,number_ring}) * m) / n",
+ "(l::'a::{field_inverse_zero,number_ring}) / (m * n)",
+ "((number_of v)::'a::{field_inverse_zero,number_ring}) / (number_of w)"],
K DivideCancelNumeralFactor.proc)]
@@ -598,8 +598,8 @@
["((l::'a::idom) * m) dvd n", "(l::'a::idom) dvd (m * n)"],
K DvdCancelFactor.proc),
("divide_cancel_factor",
- ["((l::'a::{division_ring_inverse_zero,field}) * m) / n",
- "(l::'a::{division_ring_inverse_zero,field}) / (m * n)"],
+ ["((l::'a::field_inverse_zero) * m) / n",
+ "(l::'a::field_inverse_zero) / (m * n)"],
K DivideCancelFactor.proc)];
end;