--- a/src/HOL/Binomial.thy Tue Mar 31 16:49:41 2015 +0100
+++ b/src/HOL/Binomial.thy Tue Mar 31 21:54:32 2015 +0200
@@ -549,11 +549,7 @@
(if n = 0 then 1 else (setprod (\<lambda>i. a - of_nat i) {0 .. n - 1}) / (fact n))"
lemma gbinomial_0 [simp]: "a gchoose 0 = 1" "0 gchoose (Suc n) = 0"
- apply (simp_all add: gbinomial_def)
- apply (subgoal_tac "(\<Prod>i\<Colon>nat\<in>{0\<Colon>nat..n}. - of_nat i) = (0::'b)")
- apply (simp del:setprod_zero_iff)
- apply simp
- done
+ by (simp_all add: gbinomial_def)
lemma gbinomial_pochhammer: "a gchoose n = (- 1) ^ n * pochhammer (- a) n / (fact n)"
proof (cases "n = 0")
@@ -721,7 +717,7 @@
Alternative definition of the binomial coefficient as @{term "\<Prod>i<k. (n - i) / (k - i)"} *}
lemma gbinomial_altdef_of_nat:
fixes k :: nat
- and x :: "'a :: {field_char_0,field_inverse_zero}"
+ and x :: "'a :: {field_char_0,field}"
shows "x gchoose k = (\<Prod>i<k. (x - of_nat i) / of_nat (k - i) :: 'a)"
proof -
have "(x gchoose k) = (\<Prod>i<k. x - of_nat i) / of_nat (fact k)"
@@ -735,7 +731,7 @@
lemma gbinomial_ge_n_over_k_pow_k:
fixes k :: nat
- and x :: "'a :: linordered_field_inverse_zero"
+ and x :: "'a :: linordered_field"
assumes "of_nat k \<le> x"
shows "(x / of_nat k :: 'a) ^ k \<le> x gchoose k"
proof -
@@ -765,7 +761,7 @@
text{*Versions of the theorems above for the natural-number version of "choose"*}
lemma binomial_altdef_of_nat:
fixes n k :: nat
- and x :: "'a :: {field_char_0,field_inverse_zero}" --{*the point is to constrain @{typ 'a}*}
+ and x :: "'a :: {field_char_0,field}" --{*the point is to constrain @{typ 'a}*}
assumes "k \<le> n"
shows "of_nat (n choose k) = (\<Prod>i<k. of_nat (n - i) / of_nat (k - i) :: 'a)"
using assms
@@ -773,7 +769,7 @@
lemma binomial_ge_n_over_k_pow_k:
fixes k n :: nat
- and x :: "'a :: linordered_field_inverse_zero"
+ and x :: "'a :: linordered_field"
assumes "k \<le> n"
shows "(of_nat n / of_nat k :: 'a) ^ k \<le> of_nat (n choose k)"
by (simp add: assms gbinomial_ge_n_over_k_pow_k binomial_gbinomial of_nat_diff)
--- a/src/HOL/Complex.thy Tue Mar 31 16:49:41 2015 +0100
+++ b/src/HOL/Complex.thy Tue Mar 31 21:54:32 2015 +0200
@@ -55,7 +55,7 @@
subsection {* Multiplication and Division *}
-instantiation complex :: field_inverse_zero
+instantiation complex :: field
begin
primcorec one_complex where
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Tue Mar 31 16:49:41 2015 +0100
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Tue Mar 31 21:54:32 2015 +0200
@@ -30,7 +30,7 @@
| "tmsize (CNP n c a) = 3 + polysize c + tmsize a "
(* Semantics of terms tm *)
-primrec Itm :: "'a::{field_char_0, field_inverse_zero} list \<Rightarrow> 'a list \<Rightarrow> tm \<Rightarrow> 'a"
+primrec Itm :: "'a::{field_char_0, field} list \<Rightarrow> 'a list \<Rightarrow> tm \<Rightarrow> 'a"
where
"Itm vs bs (CP c) = (Ipoly vs c)"
| "Itm vs bs (Bound n) = bs!n"
@@ -311,7 +311,7 @@
by (induct t arbitrary: i rule: tmmul.induct) (auto simp add: Let_def)
lemma tmmul_allpolys_npoly[simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
shows "allpolys isnpoly t \<Longrightarrow> isnpoly c \<Longrightarrow> allpolys isnpoly (tmmul t c)"
by (induct t rule: tmmul.induct) (simp_all add: Let_def polymul_norm)
@@ -337,7 +337,7 @@
unfolding isnpoly_def by simp
lemma tmneg_allpolys_npoly[simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
shows "allpolys isnpoly t \<Longrightarrow> allpolys isnpoly (tmneg t)"
unfolding tmneg_def by auto
@@ -354,7 +354,7 @@
using tmsub_def by simp
lemma tmsub_allpolys_npoly[simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
shows "allpolys isnpoly t \<Longrightarrow> allpolys isnpoly s \<Longrightarrow> allpolys isnpoly (tmsub t s)"
unfolding tmsub_def by (simp add: isnpoly_def)
@@ -371,7 +371,7 @@
(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::{field_char_0, field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
shows "polynate t = 0\<^sub>p \<Longrightarrow> Ipoly bs t = (0::'a)"
apply (subst polynate[symmetric])
apply simp
@@ -394,7 +394,7 @@
by (simp_all add: isnpoly_def)
lemma simptm_allpolys_npoly[simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
shows "allpolys isnpoly (simptm p)"
by (induct p rule: simptm.induct) (auto simp add: Let_def)
@@ -445,7 +445,7 @@
qed
lemma split0_nb0:
- assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
shows "split0 t = (c',t') \<Longrightarrow> tmbound 0 t'"
proof -
fix c' t'
@@ -457,7 +457,7 @@
qed
lemma split0_nb0'[simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
shows "tmbound0 (snd (split0 t))"
using split0_nb0[of t "fst (split0 t)" "snd (split0 t)"]
by (simp add: tmbound0_tmbound_iff)
@@ -485,7 +485,7 @@
by (induct p rule: split0.induct) (auto simp add: isnpoly_def Let_def split_def)
lemma isnpoly_fst_split0:
- assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
shows "allpolys isnpoly p \<Longrightarrow> isnpoly (fst (split0 p))"
by (induct p rule: split0.induct)
(auto simp add: polyadd_norm polysub_norm polyneg_norm polymul_norm Let_def split_def)
@@ -514,7 +514,7 @@
by (induct p rule: fmsize.induct) simp_all
(* Semantics of formulae (fm) *)
-primrec Ifm ::"'a::{linordered_field_inverse_zero} list \<Rightarrow> 'a list \<Rightarrow> fm \<Rightarrow> bool"
+primrec Ifm ::"'a::{linordered_field} list \<Rightarrow> 'a list \<Rightarrow> fm \<Rightarrow> bool"
where
"Ifm vs bs T = True"
| "Ifm vs bs F = False"
@@ -1146,7 +1146,7 @@
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::{field_char_0, field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
shows "islin (simplt t)"
unfolding simplt_def
using split0_nb0'
@@ -1154,7 +1154,7 @@
islin_stupid allpolys_split0[OF simptm_allpolys_npoly])
lemma simple_islin[simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
shows "islin (simple t)"
unfolding simple_def
using split0_nb0'
@@ -1162,7 +1162,7 @@
islin_stupid allpolys_split0[OF simptm_allpolys_npoly] le_lin)
lemma simpeq_islin[simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
shows "islin (simpeq t)"
unfolding simpeq_def
using split0_nb0'
@@ -1170,7 +1170,7 @@
islin_stupid allpolys_split0[OF simptm_allpolys_npoly] eq_lin)
lemma simpneq_islin[simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
shows "islin (simpneq t)"
unfolding simpneq_def
using split0_nb0'
@@ -1181,7 +1181,7 @@
by (cases "split0 s") auto
lemma split0_npoly:
- assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
and n: "allpolys isnpoly t"
shows "isnpoly (fst (split0 t))"
and "allpolys isnpoly (snd (split0 t))"
@@ -1305,7 +1305,7 @@
done
lemma simplt_nb[simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
shows "tmbound0 t \<Longrightarrow> bound0 (simplt t)"
proof (simp add: simplt_def Let_def split_def)
assume nb: "tmbound0 t"
@@ -1326,7 +1326,7 @@
qed
lemma simple_nb[simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
shows "tmbound0 t \<Longrightarrow> bound0 (simple t)"
proof(simp add: simple_def Let_def split_def)
assume nb: "tmbound0 t"
@@ -1347,7 +1347,7 @@
qed
lemma simpeq_nb[simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
shows "tmbound0 t \<Longrightarrow> bound0 (simpeq t)"
proof (simp add: simpeq_def Let_def split_def)
assume nb: "tmbound0 t"
@@ -1368,7 +1368,7 @@
qed
lemma simpneq_nb[simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
shows "tmbound0 t \<Longrightarrow> bound0 (simpneq t)"
proof (simp add: simpneq_def Let_def split_def)
assume nb: "tmbound0 t"
@@ -1526,7 +1526,7 @@
by (induct p arbitrary: bs rule: simpfm.induct) auto
lemma simpfm_bound0:
- assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
shows "bound0 p \<Longrightarrow> bound0 (simpfm p)"
by (induct p rule: simpfm.induct) auto
@@ -1567,7 +1567,7 @@
by (simp add: conj_def)
lemma
- assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
shows "qfree p \<Longrightarrow> islin (simpfm p)"
by (induct p rule: simpfm.induct) (simp_all add: conj_lin disj_lin)
@@ -3379,7 +3379,7 @@
qed
lemma simpfm_lin:
- assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
shows "qfree p \<Longrightarrow> islin (simpfm p)"
by (induct p rule: simpfm.induct) (auto simp add: conj_lin disj_lin)
@@ -3704,7 +3704,7 @@
(auto simp add: msubsteq2_nb msubstltpos_nb msubstlepos_nb)
lemma msubstneg_nb:
- assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
and lp: "islin p"
and tnb: "tmbound0 t"
shows "bound0 (msubstneg p c t)"
@@ -3713,7 +3713,7 @@
(auto simp add: msubsteq2_nb msubstltneg_nb msubstleneg_nb)
lemma msubst2_nb:
- assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
and lp: "islin p"
and tnb: "tmbound0 t"
shows "bound0 (msubst2 p c t)"
@@ -4196,7 +4196,7 @@
Parametric_Ferrante_Rackoff.method true
*} "parametric QE for linear Arithmetic over fields, Version 2"
-lemma "\<exists>(x::'a::{linordered_field_inverse_zero}). y \<noteq> -1 \<longrightarrow> (y + 1) * x < 0"
+lemma "\<exists>(x::'a::{linordered_field}). y \<noteq> -1 \<longrightarrow> (y + 1) * x < 0"
apply (frpar type: 'a pars: y)
apply (simp add: field_simps)
apply (rule spec[where x=y])
@@ -4204,7 +4204,7 @@
apply simp
done
-lemma "\<exists>(x::'a::{linordered_field_inverse_zero}). y \<noteq> -1 \<longrightarrow> (y + 1)*x < 0"
+lemma "\<exists>(x::'a::{linordered_field}). y \<noteq> -1 \<longrightarrow> (y + 1)*x < 0"
apply (frpar2 type: 'a pars: y)
apply (simp add: field_simps)
apply (rule spec[where x=y])
@@ -4214,38 +4214,38 @@
text{* Collins/Jones Problem *}
(*
-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"
+lemma "\<exists>(r::'a::{linordered_field, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0"
proof-
- 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")
+ have "(\<exists>(r::'a::{linordered_field, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0) \<longleftrightarrow> (\<exists>(r::'a::{linordered_field, number_ring}). 0 < r \<and> r < 1 \<and> 0 < 2 *(a^2 + b^2) - (3*(a^2 + b^2)) * r + (2*a)*r \<and> 2*(a^2 + b^2) - (3*(a^2 + b^2) - 4*a + 1)*r - 2*a < 0)" (is "?lhs \<longleftrightarrow> ?rhs")
by (simp add: field_simps)
have "?rhs"
- 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 (frpar type: "'a::{linordered_field, number_ring}" pars: "a::'a::{linordered_field, number_ring}" "b::'a::{linordered_field, number_ring}")
apply (simp add: field_simps)
oops
*)
(*
-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}")
+lemma "ALL (x::'a::{linordered_field, number_ring}) y. (1 - t)*x \<le> (1+t)*y \<and> (1 - t)*y \<le> (1+t)*x --> 0 \<le> y"
+apply (frpar type: "'a::{linordered_field, number_ring}" pars: "t::'a::{linordered_field, number_ring}")
oops
*)
text{* Collins/Jones Problem *}
(*
-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"
+lemma "\<exists>(r::'a::{linordered_field, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0"
proof-
- 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")
+ have "(\<exists>(r::'a::{linordered_field, number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0) \<longleftrightarrow> (\<exists>(r::'a::{linordered_field, number_ring}). 0 < r \<and> r < 1 \<and> 0 < 2 *(a^2 + b^2) - (3*(a^2 + b^2)) * r + (2*a)*r \<and> 2*(a^2 + b^2) - (3*(a^2 + b^2) - 4*a + 1)*r - 2*a < 0)" (is "?lhs \<longleftrightarrow> ?rhs")
by (simp add: field_simps)
have "?rhs"
- 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 (frpar2 type: "'a::{linordered_field, number_ring}" pars: "a::'a::{linordered_field, number_ring}" "b::'a::{linordered_field, number_ring}")
apply simp
oops
*)
(*
-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}")
+lemma "ALL (x::'a::{linordered_field, number_ring}) y. (1 - t)*x \<le> (1+t)*y \<and> (1 - t)*y \<le> (1+t)*x --> 0 \<le> y"
+apply (frpar2 type: "'a::{linordered_field, number_ring}" pars: "t::'a::{linordered_field, number_ring}")
apply (simp add: field_simps linorder_neq_iff[symmetric])
apply ferrack
oops
--- a/src/HOL/Decision_Procs/Rat_Pair.thy Tue Mar 31 16:49:41 2015 +0100
+++ b/src/HOL/Decision_Procs/Rat_Pair.thy Tue Mar 31 21:54:32 2015 +0200
@@ -156,7 +156,7 @@
lemma isnormNum_unique[simp]:
assumes na: "isnormNum x" and nb: "isnormNum y"
- shows "((INum x ::'a::{field_char_0, field_inverse_zero}) = INum y) = (x = y)" (is "?lhs = ?rhs")
+ shows "((INum x ::'a::{field_char_0, field}) = INum y) = (x = y)" (is "?lhs = ?rhs")
proof
obtain a b where x: "x = (a, b)" by (cases x)
obtain a' b' where y: "y = (a', b')" by (cases y)
@@ -190,7 +190,7 @@
lemma isnormNum0[simp]:
- "isnormNum x \<Longrightarrow> (INum x = (0::'a::{field_char_0, field_inverse_zero})) = (x = 0\<^sub>N)"
+ "isnormNum x \<Longrightarrow> (INum x = (0::'a::{field_char_0, field})) = (x = 0\<^sub>N)"
unfolding INum_int(2)[symmetric]
by (rule isnormNum_unique) simp_all
@@ -213,7 +213,7 @@
(of_int(n div d)::'a::field_char_0) = of_int n / of_int d"
using of_int_div_aux [of d n, where ?'a = 'a] by simp
-lemma normNum[simp]: "INum (normNum x) = (INum x :: 'a::{field_char_0, field_inverse_zero})"
+lemma normNum[simp]: "INum (normNum x) = (INum x :: 'a::{field_char_0, field})"
proof -
obtain a b where x: "x = (a, b)" by (cases x)
{ assume "a = 0 \<or> b = 0"
@@ -228,7 +228,7 @@
qed
lemma INum_normNum_iff:
- "(INum x ::'a::{field_char_0, field_inverse_zero}) = INum y \<longleftrightarrow> normNum x = normNum y"
+ "(INum x ::'a::{field_char_0, field}) = INum y \<longleftrightarrow> normNum x = normNum y"
(is "?lhs = ?rhs")
proof -
have "normNum x = normNum y \<longleftrightarrow> (INum (normNum x) :: 'a) = INum (normNum y)"
@@ -237,7 +237,7 @@
finally show ?thesis by simp
qed
-lemma Nadd[simp]: "INum (x +\<^sub>N y) = INum x + (INum y :: 'a :: {field_char_0, field_inverse_zero})"
+lemma Nadd[simp]: "INum (x +\<^sub>N y) = INum x + (INum y :: 'a :: {field_char_0, field})"
proof -
let ?z = "0:: 'a"
obtain a b where x: "x = (a, b)" by (cases x)
@@ -274,7 +274,7 @@
ultimately show ?thesis by blast
qed
-lemma Nmul[simp]: "INum (x *\<^sub>N y) = INum x * (INum y:: 'a :: {field_char_0, field_inverse_zero})"
+lemma Nmul[simp]: "INum (x *\<^sub>N y) = INum x * (INum y:: 'a :: {field_char_0, field})"
proof -
let ?z = "0::'a"
obtain a b where x: "x = (a, b)" by (cases x)
@@ -298,18 +298,18 @@
lemma Nneg[simp]: "INum (~\<^sub>N x) = - (INum x ::'a:: field)"
by (simp add: Nneg_def split_def INum_def)
-lemma Nsub[simp]: "INum (x -\<^sub>N y) = INum x - (INum y:: 'a :: {field_char_0, field_inverse_zero})"
+lemma Nsub[simp]: "INum (x -\<^sub>N y) = INum x - (INum y:: 'a :: {field_char_0, field})"
by (simp add: Nsub_def split_def)
-lemma Ninv[simp]: "INum (Ninv x) = (1::'a :: field_inverse_zero) / (INum x)"
+lemma Ninv[simp]: "INum (Ninv x) = (1::'a :: field) / (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 :: {field_char_0, field_inverse_zero})"
+lemma Ndiv[simp]: "INum (x \<div>\<^sub>N y) = INum x / (INum y ::'a :: {field_char_0, field})"
by (simp add: Ndiv_def)
lemma Nlt0_iff[simp]:
assumes nx: "isnormNum x"
- shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero})< 0) = 0>\<^sub>N x"
+ shows "((INum x :: 'a :: {field_char_0, linordered_field})< 0) = 0>\<^sub>N x"
proof -
obtain a b where x: "x = (a, b)" by (cases x)
{ assume "a = 0" hence ?thesis by (simp add: x Nlt0_def INum_def) }
@@ -323,7 +323,7 @@
lemma Nle0_iff[simp]:
assumes nx: "isnormNum x"
- shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero}) \<le> 0) = 0\<ge>\<^sub>N x"
+ shows "((INum x :: 'a :: {field_char_0, linordered_field}) \<le> 0) = 0\<ge>\<^sub>N x"
proof -
obtain a b where x: "x = (a, b)" by (cases x)
{ assume "a = 0" hence ?thesis by (simp add: x Nle0_def INum_def) }
@@ -337,7 +337,7 @@
lemma Ngt0_iff[simp]:
assumes nx: "isnormNum x"
- shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero})> 0) = 0<\<^sub>N x"
+ shows "((INum x :: 'a :: {field_char_0, linordered_field})> 0) = 0<\<^sub>N x"
proof -
obtain a b where x: "x = (a, b)" by (cases x)
{ assume "a = 0" hence ?thesis by (simp add: x Ngt0_def INum_def) }
@@ -351,7 +351,7 @@
lemma Nge0_iff[simp]:
assumes nx: "isnormNum x"
- shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero}) \<ge> 0) = 0\<le>\<^sub>N x"
+ shows "((INum x :: 'a :: {field_char_0, linordered_field}) \<ge> 0) = 0\<le>\<^sub>N x"
proof -
obtain a b where x: "x = (a, b)" by (cases x)
{ assume "a = 0" hence ?thesis by (simp add: x Nge0_def INum_def) }
@@ -365,7 +365,7 @@
lemma Nlt_iff[simp]:
assumes nx: "isnormNum x" and ny: "isnormNum y"
- shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero}) < INum y) = (x <\<^sub>N y)"
+ shows "((INum x :: 'a :: {field_char_0, linordered_field}) < INum y) = (x <\<^sub>N y)"
proof -
let ?z = "0::'a"
have "((INum x ::'a) < INum y) = (INum (x -\<^sub>N y) < ?z)"
@@ -377,7 +377,7 @@
lemma Nle_iff[simp]:
assumes nx: "isnormNum x" and ny: "isnormNum y"
- shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero})\<le> INum y) = (x \<le>\<^sub>N y)"
+ shows "((INum x :: 'a :: {field_char_0, linordered_field})\<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
@@ -387,7 +387,7 @@
qed
lemma Nadd_commute:
- assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
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
@@ -396,7 +396,7 @@
qed
lemma [simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
shows "(0, b) +\<^sub>N y = normNum y"
and "(a, 0) +\<^sub>N y = normNum y"
and "x +\<^sub>N (0, b) = normNum x"
@@ -408,7 +408,7 @@
done
lemma normNum_nilpotent_aux[simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
assumes nx: "isnormNum x"
shows "normNum x = x"
proof -
@@ -419,7 +419,7 @@
qed
lemma normNum_nilpotent[simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
shows "normNum (normNum x) = normNum x"
by simp
@@ -427,11 +427,11 @@
by (simp_all add: normNum_def)
lemma normNum_Nadd:
- assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
shows "normNum (x +\<^sub>N y) = x +\<^sub>N y" by simp
lemma Nadd_normNum1[simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
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
@@ -441,7 +441,7 @@
qed
lemma Nadd_normNum2[simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
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
@@ -451,7 +451,7 @@
qed
lemma Nadd_assoc:
- assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
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
@@ -463,7 +463,7 @@
by (simp add: Nmul_def split_def Let_def gcd_commute_int mult.commute)
lemma Nmul_assoc:
- assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
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 -
@@ -474,7 +474,7 @@
qed
lemma Nsub0:
- assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
assumes x: "isnormNum x" and y: "isnormNum y"
shows "x -\<^sub>N y = 0\<^sub>N \<longleftrightarrow> x = y"
proof -
@@ -490,7 +490,7 @@
by (simp_all add: Nmul_def Let_def split_def)
lemma Nmul_eq0[simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0, field})"
assumes nx: "isnormNum x" and ny: "isnormNum y"
shows "x*\<^sub>N y = 0\<^sub>N \<longleftrightarrow> x = 0\<^sub>N \<or> y = 0\<^sub>N"
proof -
--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Tue Mar 31 16:49:41 2015 +0100
+++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Tue Mar 31 21:54:32 2015 +0200
@@ -235,7 +235,7 @@
subsection{* Semantics of the polynomial representation *}
-primrec Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{field_char_0,field_inverse_zero,power}"
+primrec Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{field_char_0,field,power}"
where
"Ipoly bs (C c) = INum c"
| "Ipoly bs (Bound n) = bs!n"
@@ -246,7 +246,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::{field_char_0,field_inverse_zero,power}"
+abbreviation Ipoly_syntax :: "poly \<Rightarrow> 'a list \<Rightarrow>'a::{field_char_0,field,power}"
("\<lparr>_\<rparr>\<^sub>p\<^bsup>_\<^esup>")
where "\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<equiv> Ipoly bs p"
@@ -481,7 +481,7 @@
qed simp_all
lemma polymul_properties:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
and np: "isnpolyh p n0"
and nq: "isnpolyh q n1"
and m: "m \<le> min n0 n1"
@@ -670,23 +670,23 @@
by (induct p q rule: polymul.induct) (auto simp add: field_simps)
lemma polymul_normh:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
shows "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> isnpolyh (p *\<^sub>p q) (min n0 n1)"
using polymul_properties(1) by blast
lemma polymul_eq0_iff:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
shows "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> p *\<^sub>p q = 0\<^sub>p \<longleftrightarrow> p = 0\<^sub>p \<or> q = 0\<^sub>p"
using polymul_properties(2) by blast
lemma polymul_degreen:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
shows "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> m \<le> min n0 n1 \<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)"
by (fact polymul_properties(3))
lemma polymul_norm:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
shows "isnpoly p \<Longrightarrow> isnpoly q \<Longrightarrow> isnpoly (polymul p q)"
using polymul_normh[of "p" "0" "q" "0"] isnpoly_def by simp
@@ -699,7 +699,7 @@
lemma monic_eqI:
assumes np: "isnpolyh p n0"
shows "INum (headconst p) * Ipoly bs (fst (monic p)) =
- (Ipoly bs p ::'a::{field_char_0,field_inverse_zero, power})"
+ (Ipoly bs p ::'a::{field_char_0,field, power})"
unfolding monic_def Let_def
proof (cases "headconst p = 0\<^sub>N", simp_all add: headconst_zero[OF np])
let ?h = "headconst p"
@@ -750,13 +750,13 @@
using polyadd_norm polyneg_norm by (simp add: polysub_def)
lemma polysub_same_0[simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
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_char_0,field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
shows "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> p -\<^sub>p q = 0\<^sub>p \<longleftrightarrow> p = q"
unfolding polysub_def split_def fst_conv snd_conv
by (induct p q arbitrary: n0 n1 rule:polyadd.induct)
@@ -765,7 +765,7 @@
text{* polypow is a power function and preserves normal forms *}
lemma polypow[simp]:
- "Ipoly bs (polypow n p) = (Ipoly bs p :: 'a::{field_char_0,field_inverse_zero}) ^ n"
+ "Ipoly bs (polypow n p) = (Ipoly bs p :: 'a::{field_char_0,field}) ^ n"
proof (induct n rule: polypow.induct)
case 1
then show ?case
@@ -806,7 +806,7 @@
qed
lemma polypow_normh:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
shows "isnpolyh p n \<Longrightarrow> isnpolyh (polypow k p) n"
proof (induct k arbitrary: n rule: polypow.induct)
case 1
@@ -826,18 +826,18 @@
qed
lemma polypow_norm:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
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_char_0,field_inverse_zero})"
+ "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{field_char_0,field})"
by (induct p rule:polynate.induct) auto
lemma polynate_norm[simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
shows "isnpoly (polynate p)"
by (induct p rule: polynate.induct)
(simp_all add: polyadd_norm polymul_norm polysub_norm polyneg_norm polypow_norm,
@@ -868,7 +868,7 @@
using assms by (induct k arbitrary: p) auto
lemma funpow_shift1:
- "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0,field_inverse_zero}) =
+ "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0,field}) =
Ipoly bs (Mul (Pw (Bound 0) n) p)"
by (induct n arbitrary: p) (simp_all add: shift1_isnpoly shift1)
@@ -876,7 +876,7 @@
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_char_0,field_inverse_zero}) =
+ "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0,field}) =
Ipoly bs (funpow n shift1 (1)\<^sub>p *\<^sub>p p)"
by (simp add: funpow_shift1)
@@ -886,7 +886,7 @@
lemma behead:
assumes "isnpolyh p n"
shows "Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) =
- (Ipoly bs p :: 'a :: {field_char_0,field_inverse_zero})"
+ (Ipoly bs p :: 'a :: {field_char_0,field})"
using assms
proof (induct p arbitrary: n rule: behead.induct)
case (1 c p n)
@@ -1160,7 +1160,7 @@
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::{field_char_0,field_inverse_zero, power})"
+ and eq :"\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a::{field_char_0,field, power})"
shows "p = 0\<^sub>p"
using nq eq
proof (induct "maxindex p" arbitrary: p n0 rule: less_induct)
@@ -1242,7 +1242,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::{field_char_0,field_inverse_zero,power})) \<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,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>"
then have "\<forall>bs.\<lparr>p -\<^sub>p q\<rparr>\<^sub>p\<^bsup>bs\<^esup>= (0::'a)"
@@ -1257,7 +1257,7 @@
text{* consequences of unicity on the algorithms for polynomial normalization *}
lemma polyadd_commute:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
and np: "isnpolyh p n0"
and nq: "isnpolyh q n1"
shows "p +\<^sub>p q = q +\<^sub>p p"
@@ -1271,7 +1271,7 @@
by simp
lemma polyadd_0[simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
and np: "isnpolyh p n0"
shows "p +\<^sub>p 0\<^sub>p = p"
and "0\<^sub>p +\<^sub>p p = p"
@@ -1279,7 +1279,7 @@
isnpolyh_unique[OF polyadd_normh[OF zero_normh np] np] by simp_all
lemma polymul_1[simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
and np: "isnpolyh p n0"
shows "p *\<^sub>p (1)\<^sub>p = p"
and "(1)\<^sub>p *\<^sub>p p = p"
@@ -1287,7 +1287,7 @@
isnpolyh_unique[OF polymul_normh[OF one_normh np] np] by simp_all
lemma polymul_0[simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
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"
@@ -1295,27 +1295,27 @@
isnpolyh_unique[OF polymul_normh[OF zero_normh np] zero_normh] by simp_all
lemma polymul_commute:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
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::{field_char_0,field_inverse_zero, power}"]
+ where ?'a = "'a::{field_char_0,field, power}"]
by simp
declare polyneg_polyneg [simp]
lemma isnpolyh_polynate_id [simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
and np: "isnpolyh p n0"
shows "polynate p = p"
- using isnpolyh_unique[where ?'a= "'a::{field_char_0,field_inverse_zero}",
+ using isnpolyh_unique[where ?'a= "'a::{field_char_0,field}",
OF polynate_norm[of p, unfolded isnpoly_def] np]
- polynate[where ?'a = "'a::{field_char_0,field_inverse_zero}"]
+ polynate[where ?'a = "'a::{field_char_0,field}"]
by simp
lemma polynate_idempotent[simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
shows "polynate (polynate p) = polynate p"
using isnpolyh_polynate_id[OF polynate_norm[of p, unfolded isnpoly_def]] .
@@ -1323,7 +1323,7 @@
unfolding poly_nate_def polypoly'_def ..
lemma poly_nate_poly:
- "poly (poly_nate bs p) = (\<lambda>x:: 'a ::{field_char_0,field_inverse_zero}. \<lparr>p\<rparr>\<^sub>p\<^bsup>x # bs\<^esup>)"
+ "poly (poly_nate bs p) = (\<lambda>x:: 'a ::{field_char_0,field}. \<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
@@ -1362,7 +1362,7 @@
qed
lemma degree_polysub_samehead:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
and np: "isnpolyh p n0"
and nq: "isnpolyh q n1"
and h: "head p = head q"
@@ -1531,7 +1531,7 @@
done
lemma polymul_head_polyeq:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
shows "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> p \<noteq> 0\<^sub>p \<Longrightarrow> q \<noteq> 0\<^sub>p \<Longrightarrow> head (p *\<^sub>p q) = head p *\<^sub>p head q"
proof (induct p q arbitrary: n0 n1 rule: polymul.induct)
case (2 c c' n' p' n0 n1)
@@ -1634,7 +1634,7 @@
by (induct p arbitrary: n0 rule: polyneg.induct) auto
lemma degree_polymul:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
and np: "isnpolyh p n0"
and nq: "isnpolyh q n1"
shows "degree (p *\<^sub>p q) \<le> degree p + degree q"
@@ -1650,7 +1650,7 @@
subsection {* Correctness of polynomial pseudo division *}
lemma polydivide_aux_properties:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
and np: "isnpolyh p n0"
and ns: "isnpolyh s n1"
and ap: "head p = a"
@@ -1745,24 +1745,24 @@
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_char_0,field_inverse_zero} list.
+ from asp have "\<forall>bs :: 'a::{field_char_0,field} 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
- then have "\<forall>bs :: 'a::{field_char_0,field_inverse_zero} list.
+ then have "\<forall>bs :: 'a::{field_char_0,field} 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)
- then have "\<forall>bs :: 'a::{field_char_0,field_inverse_zero} list.
+ then have "\<forall>bs :: 'a::{field_char_0,field} 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)
- then have "\<forall>bs:: 'a::{field_char_0,field_inverse_zero} list.
+ then have "\<forall>bs:: 'a::{field_char_0,field} 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)
- then have "\<forall>bs:: 'a::{field_char_0,field_inverse_zero} list.
+ then have "\<forall>bs:: 'a::{field_char_0,field} 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
@@ -1784,10 +1784,10 @@
moreover
{
assume spz:"s -\<^sub>p ?p' = 0\<^sub>p"
- 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'"
+ from spz isnpolyh_unique[OF polysub_normh[OF ns np'], where q="0\<^sub>p", symmetric, where ?'a = "'a::{field_char_0,field}"]
+ have "\<forall>bs:: 'a::{field_char_0,field} list. Ipoly bs s = Ipoly bs ?p'"
by simp
- then have "\<forall>bs:: 'a::{field_char_0,field_inverse_zero} list. Ipoly bs s = Ipoly bs (?xdn *\<^sub>p p)"
+ then have "\<forall>bs:: 'a::{field_char_0,field} list. Ipoly bs s = Ipoly bs (?xdn *\<^sub>p p)"
using np nxdn
apply simp
apply (simp only: funpow_shift1_1)
@@ -1861,7 +1861,7 @@
from kk' have kk'': "Suc (k' - Suc k) = k' - k"
by arith
{
- fix bs :: "'a::{field_char_0,field_inverse_zero} list"
+ fix bs :: "'a::{field_char_0,field} 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
@@ -1875,7 +1875,7 @@
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)
}
- then have ieq:"\<forall>bs :: 'a::{field_char_0,field_inverse_zero} list.
+ then have ieq:"\<forall>bs :: 'a::{field_char_0,field} 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
@@ -1900,7 +1900,7 @@
{
assume spz: "a *\<^sub>p s -\<^sub>p (?b *\<^sub>p ?p') = 0\<^sub>p"
{
- fix bs :: "'a::{field_char_0,field_inverse_zero} list"
+ fix bs :: "'a::{field_char_0,field} 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
@@ -1909,10 +1909,10 @@
then have "Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))"
by simp
}
- then have hth: "\<forall>bs :: 'a::{field_char_0,field_inverse_zero} list.
+ then have hth: "\<forall>bs :: 'a::{field_char_0,field} 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_char_0,field_inverse_zero}", OF polymul_normh[OF head_isnpolyh[OF np] ns]
+ using isnpolyh_unique[where ?'a = "'a::{field_char_0,field}", 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
@@ -1945,7 +1945,7 @@
qed
lemma polydivide_properties:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
and np: "isnpolyh p n0"
and ns: "isnpolyh s n1"
and pnz: "p \<noteq> 0\<^sub>p"
@@ -2112,12 +2112,12 @@
lemma swapnorm:
assumes nbs: "n < length bs"
and mbs: "m < length bs"
- shows "((Ipoly bs (swapnorm n m t) :: 'a::{field_char_0,field_inverse_zero})) =
+ shows "((Ipoly bs (swapnorm n m t) :: 'a::{field_char_0,field})) =
Ipoly ((bs[n:= bs!m])[m:= bs!n]) t"
using swap[OF assms] swapnorm_def by simp
lemma swapnorm_isnpoly [simp]:
- assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})"
+ assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
shows "isnpoly (swapnorm n m p)"
unfolding swapnorm_def by simp
--- a/src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy Tue Mar 31 16:49:41 2015 +0100
+++ b/src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy Tue Mar 31 21:54:32 2015 +0200
@@ -7,147 +7,147 @@
begin
lemma
- "\<exists>(y::'a::{linordered_field_inverse_zero}) <2. x + 3* y < 0 \<and> x - y >0"
+ "\<exists>(y::'a::{linordered_field}) <2. x + 3* y < 0 \<and> x - y >0"
by ferrack
-lemma "~ (ALL x (y::'a::{linordered_field_inverse_zero}). x < y --> 10*x < 11*y)"
+lemma "~ (ALL x (y::'a::{linordered_field}). x < y --> 10*x < 11*y)"
by ferrack
-lemma "ALL (x::'a::{linordered_field_inverse_zero}) y. x < y --> (10*(x + 5*y + -1) < 60*y)"
+lemma "ALL (x::'a::{linordered_field}) y. x < y --> (10*(x + 5*y + -1) < 60*y)"
by ferrack
-lemma "EX (x::'a::{linordered_field_inverse_zero}) y. x ~= y --> x < y"
+lemma "EX (x::'a::{linordered_field}) y. x ~= y --> x < y"
by ferrack
-lemma "EX (x::'a::{linordered_field_inverse_zero}) y. (x ~= y & 10*x ~= 9*y & 10*x < y) --> x < y"
+lemma "EX (x::'a::{linordered_field}) y. (x ~= y & 10*x ~= 9*y & 10*x < y) --> x < y"
by ferrack
-lemma "ALL (x::'a::{linordered_field_inverse_zero}) y. (x ~= y & 5*x <= y) --> 500*x <= 100*y"
+lemma "ALL (x::'a::{linordered_field}) y. (x ~= y & 5*x <= y) --> 500*x <= 100*y"
by ferrack
-lemma "ALL (x::'a::{linordered_field_inverse_zero}). (EX (y::'a::{linordered_field_inverse_zero}). 4*x + 3*y <= 0 & 4*x + 3*y >= -1)"
+lemma "ALL (x::'a::{linordered_field}). (EX (y::'a::{linordered_field}). 4*x + 3*y <= 0 & 4*x + 3*y >= -1)"
by ferrack
-lemma "ALL (x::'a::{linordered_field_inverse_zero}) < 0. (EX (y::'a::{linordered_field_inverse_zero}) > 0. 7*x + y > 0 & x - y <= 9)"
+lemma "ALL (x::'a::{linordered_field}) < 0. (EX (y::'a::{linordered_field}) > 0. 7*x + y > 0 & x - y <= 9)"
by ferrack
-lemma "EX (x::'a::{linordered_field_inverse_zero}). (0 < x & x < 1) --> (ALL y > 1. x + y ~= 1)"
+lemma "EX (x::'a::{linordered_field}). (0 < x & x < 1) --> (ALL y > 1. x + y ~= 1)"
by ferrack
-lemma "EX x. (ALL (y::'a::{linordered_field_inverse_zero}). y < 2 --> 2*(y - x) \<le> 0 )"
+lemma "EX x. (ALL (y::'a::{linordered_field}). y < 2 --> 2*(y - x) \<le> 0 )"
by ferrack
-lemma "ALL (x::'a::{linordered_field_inverse_zero}). x < 10 | x > 20 | (EX y. y>= 0 & y <= 10 & x+y = 20)"
+lemma "ALL (x::'a::{linordered_field}). x < 10 | x > 20 | (EX y. y>= 0 & y <= 10 & x+y = 20)"
by ferrack
-lemma "ALL (x::'a::{linordered_field_inverse_zero}) y z. x + y < z --> y >= z --> x < 0"
+lemma "ALL (x::'a::{linordered_field}) y z. x + y < z --> y >= z --> x < 0"
by ferrack
-lemma "EX (x::'a::{linordered_field_inverse_zero}) y z. x + 7*y < 5* z & 5*y >= 7*z & x < 0"
+lemma "EX (x::'a::{linordered_field}) y z. x + 7*y < 5* z & 5*y >= 7*z & x < 0"
by ferrack
-lemma "ALL (x::'a::{linordered_field_inverse_zero}) y z. abs (x + y) <= z --> (abs z = z)"
+lemma "ALL (x::'a::{linordered_field}) y z. abs (x + y) <= z --> (abs z = z)"
by ferrack
-lemma "EX (x::'a::{linordered_field_inverse_zero}) y z. x + 7*y - 5* z < 0 & 5*y + 7*z + 3*x < 0"
+lemma "EX (x::'a::{linordered_field}) y z. x + 7*y - 5* z < 0 & 5*y + 7*z + 3*x < 0"
by ferrack
-lemma "ALL (x::'a::{linordered_field_inverse_zero}) 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}) 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_inverse_zero}) y. x < y --> (EX z>0. x+z = y)"
+lemma "ALL (x::'a::{linordered_field}) y. x < y --> (EX z>0. x+z = y)"
by ferrack
-lemma "ALL (x::'a::{linordered_field_inverse_zero}) y. x < y --> (EX z>0. x+z = y)"
+lemma "ALL (x::'a::{linordered_field}) y. x < y --> (EX z>0. x+z = y)"
by ferrack
-lemma "ALL (x::'a::{linordered_field_inverse_zero}) y. (EX z>0. abs (x - y) <= z )"
+lemma "ALL (x::'a::{linordered_field}) y. (EX z>0. abs (x - y) <= z )"
by ferrack
-lemma "EX (x::'a::{linordered_field_inverse_zero}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))"
+lemma "EX (x::'a::{linordered_field}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))"
by ferrack
-lemma "EX (x::'a::{linordered_field_inverse_zero}) y. (ALL z>=0. abs (3*x+7*y) <= 2*z + 1)"
+lemma "EX (x::'a::{linordered_field}) y. (ALL z>=0. abs (3*x+7*y) <= 2*z + 1)"
by ferrack
-lemma "EX (x::'a::{linordered_field_inverse_zero}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))"
+lemma "EX (x::'a::{linordered_field}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))"
by ferrack
-lemma "EX (x::'a::{linordered_field_inverse_zero})>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})>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_inverse_zero}). 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}). 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_inverse_zero}). (EX y > abs (23*x - 9). (ALL z > abs (3*y - 19* abs x). x+z > 2*y))"
+lemma "ALL (x::'a::{linordered_field}). (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_inverse_zero}). (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}). (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_inverse_zero}). abs x < 100 & (ALL y > x. (EX z<2*y - x. 5*x - 3*y <= 7*z))"
+lemma "EX (x::'a::{linordered_field}). 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_inverse_zero}) 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}) 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_inverse_zero}) y z w. 5*x + 3*z - 17*w + abs (y - 8*x + z) <= 89"
+lemma "EX (x::'a::{linordered_field}) y z w. 5*x + 3*z - 17*w + abs (y - 8*x + z) <= 89"
by ferrack
-lemma "EX (x::'a::{linordered_field_inverse_zero}) 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}) 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_inverse_zero}) 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}) 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_inverse_zero}) y z. (EX w >= (x+y+z). w <= abs x + abs y + abs z)"
+lemma "ALL (x::'a::{linordered_field}) y z. (EX w >= (x+y+z). w <= abs x + abs y + abs z)"
by ferrack
-lemma "~(ALL (x::'a::{linordered_field_inverse_zero}). (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}). (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_inverse_zero}) y. (EX z w. abs (x-y) = (z-w) & z*1234 < 233*x & w ~= y)"
+lemma "ALL (x::'a::{linordered_field}) y. (EX z w. abs (x-y) = (z-w) & z*1234 < 233*x & w ~= y)"
by ferrack
-lemma "ALL (x::'a::{linordered_field_inverse_zero}). (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}). (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_inverse_zero}) y z. (ALL w >= abs (x+y+z). w >= abs x + abs y + abs z)"
+lemma "EX (x::'a::{linordered_field}) 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_inverse_zero}) y. (EX w >= (x+y+z). w <= abs x + abs y + abs z))"
+lemma "EX z. (ALL (x::'a::{linordered_field}) y. (EX w >= (x+y+z). w <= abs x + abs y + abs z))"
by ferrack
-lemma "EX z. (ALL (x::'a::{linordered_field_inverse_zero}) < abs z. (EX y w. x< y & x < z & x> w & 3*x < w + y))"
+lemma "EX z. (ALL (x::'a::{linordered_field}) < abs z. (EX y w. x< y & x < z & x> w & 3*x < w + y))"
by ferrack
-lemma "ALL (x::'a::{linordered_field_inverse_zero}) y. (EX z. (ALL w. abs (x-y) = abs (z-w) --> z < x & w ~= y))"
+lemma "ALL (x::'a::{linordered_field}) 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_inverse_zero}). (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}). (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_inverse_zero}) z. (ALL w >= 13*x - 4*z. (EX y. w >= abs x + abs y + z))"
+lemma "EX (x::'a::{linordered_field}) z. (ALL w >= 13*x - 4*z. (EX y. w >= abs x + abs y + z))"
by ferrack
-lemma "EX (x::'a::{linordered_field_inverse_zero}). (ALL y < x. (EX z > (x+y).
+lemma "EX (x::'a::{linordered_field}). (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_inverse_zero}). (ALL y. (EX z > y.
+lemma "EX (x::'a::{linordered_field}). (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_inverse_zero}) 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}) 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_inverse_zero}). (EX y. (ALL z>19. y <= x + z & (EX w. abs (y - x) < w)))"
+lemma "ALL (x::'a::{linordered_field}). (EX y. (ALL z>19. y <= x + z & (EX w. abs (y - x) < w)))"
by ferrack
-lemma "ALL (x::'a::{linordered_field_inverse_zero}). (EX y. (ALL z>19. y <= x + z & (EX w. abs (x + z) < w - y)))"
+lemma "ALL (x::'a::{linordered_field}). (EX y. (ALL z>19. y <= x + z & (EX w. abs (x + z) < w - y)))"
by ferrack
-lemma "ALL (x::'a::{linordered_field_inverse_zero}). (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}). (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/Deriv.thy Tue Mar 31 16:49:41 2015 +0100
+++ b/src/HOL/Deriv.thy Tue Mar 31 21:54:32 2015 +0200
@@ -698,10 +698,17 @@
(auto simp: setsum_right_distrib mult_commute_abs dest: has_field_derivative_imp_has_derivative)
lemma DERIV_inverse'[derivative_intros]:
- "(f has_field_derivative D) (at x within s) \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow>
- ((\<lambda>x. inverse (f x)) has_field_derivative - (inverse (f x) * D * inverse (f x))) (at x within s)"
- by (rule has_derivative_imp_has_field_derivative[OF has_derivative_inverse])
- (auto dest: has_field_derivative_imp_has_derivative)
+ assumes "(f has_field_derivative D) (at x within s)"
+ and "f x \<noteq> 0"
+ shows "((\<lambda>x. inverse (f x)) has_field_derivative - (inverse (f x) * D * inverse (f x))) (at x within s)"
+proof -
+ have "(f has_derivative (\<lambda>x. x * D)) = (f has_derivative op * D)"
+ by (rule arg_cong [of "\<lambda>x. x * D"]) (simp add: fun_eq_iff)
+ with assms have "(f has_derivative (\<lambda>x. x * D)) (at x within s)"
+ by (auto dest!: has_field_derivative_imp_has_derivative)
+ then show ?thesis using `f x \<noteq> 0`
+ by (auto intro: has_derivative_imp_has_field_derivative has_derivative_inverse)
+qed
text {* Power of @{text "-1"} *}
--- a/src/HOL/Enum.thy Tue Mar 31 16:49:41 2015 +0100
+++ b/src/HOL/Enum.thy Tue Mar 31 21:54:32 2015 +0200
@@ -683,7 +683,7 @@
instance finite_2 :: complete_linorder ..
-instantiation finite_2 :: "{field_inverse_zero, abs_if, ring_div, sgn_if, semiring_div}" begin
+instantiation finite_2 :: "{field, abs_if, ring_div, sgn_if, semiring_div}" begin
definition [simp]: "0 = a\<^sub>1"
definition [simp]: "1 = a\<^sub>2"
definition "x + y = (case (x, y) of (a\<^sub>1, a\<^sub>1) \<Rightarrow> a\<^sub>1 | (a\<^sub>2, a\<^sub>2) \<Rightarrow> a\<^sub>1 | _ \<Rightarrow> a\<^sub>2)"
@@ -807,7 +807,7 @@
instance finite_3 :: complete_linorder ..
-instantiation finite_3 :: "{field_inverse_zero, abs_if, ring_div, semiring_div, sgn_if}" begin
+instantiation finite_3 :: "{field, abs_if, ring_div, semiring_div, sgn_if}" begin
definition [simp]: "0 = a\<^sub>1"
definition [simp]: "1 = a\<^sub>2"
definition
--- a/src/HOL/Fields.thy Tue Mar 31 16:49:41 2015 +0100
+++ b/src/HOL/Fields.thy Tue Mar 31 21:54:32 2015 +0200
@@ -56,6 +56,7 @@
assumes left_inverse [simp]: "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
assumes right_inverse [simp]: "a \<noteq> 0 \<Longrightarrow> a * inverse a = 1"
assumes divide_inverse: "a / b = a * inverse b"
+ assumes inverse_zero [simp]: "inverse 0 = 0"
begin
subclass ring_1_no_zero_divisors
@@ -239,12 +240,6 @@
"z \<noteq> 0 \<Longrightarrow> - (x / z) - y = (- x - y * z) / z"
by (simp add: divide_diff_eq_iff[symmetric])
-end
-
-class division_ring_inverse_zero = division_ring +
- assumes inverse_zero [simp]: "inverse 0 = 0"
-begin
-
lemma divide_zero [simp]:
"a / 0 = 0"
by (simp add: divide_inverse)
@@ -307,6 +302,7 @@
class field = comm_ring_1 + inverse +
assumes field_inverse: "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
assumes field_divide_inverse: "a / b = a * inverse b"
+ assumes field_inverse_zero: "inverse 0 = 0"
begin
subclass division_ring
@@ -318,6 +314,9 @@
next
fix a b :: 'a
show "a / b = a * inverse b" by (rule field_divide_inverse)
+next
+ show "inverse 0 = 0"
+ by (fact field_inverse_zero)
qed
subclass idom ..
@@ -395,15 +394,6 @@
lemma divide_minus1 [simp]: "x / - 1 = - x"
using nonzero_minus_divide_right [of "1" x] by simp
-end
-
-class field_inverse_zero = field +
- assumes field_inverse_zero: "inverse 0 = 0"
-begin
-
-subclass division_ring_inverse_zero proof
-qed (fact field_inverse_zero)
-
text{*This version builds in division by zero while also re-orienting
the right-hand side.*}
lemma inverse_mult_distrib [simp]:
@@ -963,11 +953,6 @@
then show "t \<le> y" by (simp add: algebra_simps)
qed
-end
-
-class linordered_field_inverse_zero = linordered_field + field_inverse_zero
-begin
-
lemma inverse_positive_iff_positive [simp]:
"(0 < inverse a) = (0 < a)"
apply (cases "a = 0", simp)
--- a/src/HOL/Groups_Big.thy Tue Mar 31 16:49:41 2015 +0100
+++ b/src/HOL/Groups_Big.thy Tue Mar 31 21:54:32 2015 +0200
@@ -1158,11 +1158,11 @@
(setprod f (A - {a})) = (if a \<in> A then setprod f A / f a else setprod f A)"
by (induct A rule: finite_induct) (auto simp add: insert_Diff_if)
-lemma (in field_inverse_zero) setprod_inversef:
+lemma (in field) setprod_inversef:
"finite A \<Longrightarrow> setprod (inverse \<circ> f) A = inverse (setprod f A)"
by (induct A rule: finite_induct) simp_all
-lemma (in field_inverse_zero) setprod_dividef:
+lemma (in field) setprod_dividef:
"finite A \<Longrightarrow> (\<Prod>x\<in>A. f x / g x) = setprod f A / setprod g A"
using setprod_inversef [of A g] by (simp add: divide_inverse setprod.distrib)
--- a/src/HOL/Library/BigO.thy Tue Mar 31 16:49:41 2015 +0100
+++ b/src/HOL/Library/BigO.thy Tue Mar 31 21:54:32 2015 +0200
@@ -489,7 +489,7 @@
shows "c \<noteq> 0 \<Longrightarrow> f \<in> O(\<lambda>x. c * f x)"
apply (simp add: bigo_def)
apply (rule_tac x = "abs (inverse c)" in exI)
- apply (simp add: abs_mult [symmetric] mult.assoc [symmetric])
+ apply (simp add: abs_mult mult.assoc [symmetric])
done
lemma bigo_const_mult4:
@@ -519,11 +519,7 @@
apply (rule_tac x = "\<lambda>y. inverse c * x y" in exI)
apply (simp add: mult.assoc [symmetric] abs_mult)
apply (rule_tac x = "abs (inverse c) * ca" in exI)
- apply (rule allI)
- apply (subst mult.assoc)
- apply (rule mult_left_mono)
- apply (erule spec)
- apply force
+ apply auto
done
lemma bigo_const_mult6 [intro]: "(\<lambda>x. c) *o O(f) \<subseteq> O(f)"
--- a/src/HOL/Library/Bit.thy Tue Mar 31 16:49:41 2015 +0100
+++ b/src/HOL/Library/Bit.thy Tue Mar 31 21:54:32 2015 +0200
@@ -98,7 +98,7 @@
subsection {* Type @{typ bit} forms a field *}
-instantiation bit :: field_inverse_zero
+instantiation bit :: field
begin
definition plus_bit_def:
--- a/src/HOL/Library/Formal_Power_Series.thy Tue Mar 31 16:49:41 2015 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy Tue Mar 31 21:54:32 2015 +0200
@@ -3628,7 +3628,7 @@
subsection {* Hypergeometric series *}
-definition "F as bs (c::'a::{field_char_0,field_inverse_zero}) =
+definition "F as bs (c::'a::{field_char_0,field}) =
Abs_fps (\<lambda>n. (foldl (\<lambda>r a. r* pochhammer a n) 1 as * c^n) /
(foldl (\<lambda>r b. r * pochhammer b n) 1 bs * of_nat (fact n)))"
@@ -3711,11 +3711,11 @@
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,field_inverse_zero}) $ k =
+ "F [- of_nat n] [- of_nat (n + m)] (c::'a::{field_char_0,field}) $ k =
(if k \<le> 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,field_inverse_zero}) $ k =
+ "F [- of_nat m] [- of_nat (m + n)] (c::'a::{field_char_0,field}) $ k =
(if k \<le> m then
pochhammer (- of_nat m) k * c ^ k / (pochhammer (- of_nat (m + n)) k * of_nat (fact k))
else 0)"
--- a/src/HOL/Library/Fraction_Field.thy Tue Mar 31 16:49:41 2015 +0100
+++ b/src/HOL/Library/Fraction_Field.thy Tue Mar 31 21:54:32 2015 +0200
@@ -224,7 +224,7 @@
end
-instantiation fract :: (idom) field_inverse_zero
+instantiation fract :: (idom) field
begin
definition inverse_fract_def:
@@ -428,7 +428,7 @@
end
-instance fract :: (linordered_idom) linordered_field_inverse_zero
+instance fract :: (linordered_idom) linordered_field
proof
fix q r s :: "'a fract"
assume "q \<le> r"
--- a/src/HOL/Limits.thy Tue Mar 31 16:49:41 2015 +0100
+++ b/src/HOL/Limits.thy Tue Mar 31 21:54:32 2015 +0200
@@ -1062,7 +1062,7 @@
unfolding filterlim_def at_top_to_right filtermap_filtermap ..
lemma filterlim_inverse_at_infinity:
- fixes x :: "_ \<Rightarrow> 'a\<Colon>{real_normed_div_algebra, division_ring_inverse_zero}"
+ fixes x :: "_ \<Rightarrow> 'a\<Colon>{real_normed_div_algebra, division_ring}"
shows "filterlim inverse at_infinity (at (0::'a))"
unfolding filterlim_at_infinity[OF order_refl]
proof safe
@@ -1074,7 +1074,7 @@
qed
lemma filterlim_inverse_at_iff:
- fixes g :: "'a \<Rightarrow> 'b\<Colon>{real_normed_div_algebra, division_ring_inverse_zero}"
+ fixes g :: "'a \<Rightarrow> 'b\<Colon>{real_normed_div_algebra, division_ring}"
shows "(LIM x F. inverse (g x) :> at 0) \<longleftrightarrow> (LIM x F. g x :> at_infinity)"
unfolding filterlim_def filtermap_filtermap[symmetric]
proof
@@ -1099,7 +1099,7 @@
lemma at_to_infinity:
- fixes x :: "'a \<Colon> {real_normed_field,field_inverse_zero}"
+ fixes x :: "'a \<Colon> {real_normed_field,field}"
shows "(at (0::'a)) = filtermap inverse at_infinity"
proof (rule antisym)
have "(inverse ---> (0::'a)) at_infinity"
@@ -1117,12 +1117,12 @@
qed
lemma lim_at_infinity_0:
- fixes l :: "'a :: {real_normed_field,field_inverse_zero}"
+ fixes l :: "'a :: {real_normed_field,field}"
shows "(f ---> l) at_infinity \<longleftrightarrow> ((f o inverse) ---> l) (at (0::'a))"
by (simp add: tendsto_compose_filtermap at_to_infinity filtermap_filtermap)
lemma lim_zero_infinity:
- fixes l :: "'a :: {real_normed_field,field_inverse_zero}"
+ fixes l :: "'a :: {real_normed_field,field}"
shows "((\<lambda>x. f(1 / x)) ---> l) (at (0::'a)) \<Longrightarrow> (f ---> l) at_infinity"
by (simp add: inverse_eq_divide lim_at_infinity_0 comp_def)
@@ -1241,7 +1241,7 @@
qed
lemma tendsto_divide_0:
- fixes f :: "_ \<Rightarrow> 'a\<Colon>{real_normed_div_algebra, division_ring_inverse_zero}"
+ fixes f :: "_ \<Rightarrow> 'a\<Colon>{real_normed_div_algebra, division_ring}"
assumes f: "(f ---> c) F"
assumes g: "LIM x F. g x :> at_infinity"
shows "((\<lambda>x. f x / g x) ---> 0) F"
--- a/src/HOL/Metis_Examples/Big_O.thy Tue Mar 31 16:49:41 2015 +0100
+++ b/src/HOL/Metis_Examples/Big_O.thy Tue Mar 31 21:54:32 2015 +0200
@@ -333,8 +333,7 @@
also have "... <= O((\<lambda>x. 1 / f x) * (f * g))"
by (rule bigo_mult2)
also have "(\<lambda>x. 1 / f x) * (f * g) = g"
- apply (simp add: func_times)
- by (metis (lifting, no_types) a ext mult.commute nonzero_divide_eq_eq)
+ by (simp add: fun_eq_iff a)
finally have "(\<lambda>x. (1\<Colon>'b) / f x) * h : O(g)".
then have "f * ((\<lambda>x. (1\<Colon>'b) / f x) * h) : f *o O(g)"
by auto
@@ -458,8 +457,8 @@
using F3 by metis
hence "\<exists>(v\<Colon>'a) (u\<Colon>'a) SKF\<^sub>7\<Colon>'a \<Rightarrow> 'b. \<bar>inverse c\<bar> * \<bar>g (SKF\<^sub>7 (u * v))\<bar> \<le> u * (v * \<bar>f (SKF\<^sub>7 (u * v))\<bar>)"
by (metis mult_left_mono)
- thus "\<exists>ca\<Colon>'a. \<forall>x\<Colon>'b. \<bar>inverse c\<bar> * \<bar>g x\<bar> \<le> ca * \<bar>f x\<bar>"
- using A2 F4 by (metis mult.assoc mult_left_mono)
+ then show "\<exists>ca\<Colon>'a. \<forall>x\<Colon>'b. inverse \<bar>c\<bar> * \<bar>g x\<bar> \<le> ca * \<bar>f x\<bar>"
+ using A2 F4 by (metis F1 `0 < \<bar>inverse c\<bar>` linordered_field_class.sign_simps(23) mult_le_cancel_left_pos)
qed
lemma bigo_const_mult6 [intro]: "(\<lambda>x. c) *o O(f) <= O(f)"
--- a/src/HOL/Multivariate_Analysis/Determinants.thy Tue Mar 31 16:49:41 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Determinants.thy Tue Mar 31 21:54:32 2015 +0200
@@ -64,7 +64,7 @@
(* FIXME: In Finite_Set there is a useless further assumption *)
lemma setprod_inversef:
- "finite A \<Longrightarrow> setprod (inverse \<circ> f) A = (inverse (setprod f A) :: 'a:: field_inverse_zero)"
+ "finite A \<Longrightarrow> setprod (inverse \<circ> f) A = (inverse (setprod f A) :: 'a:: field)"
apply (erule finite_induct)
apply (simp)
apply simp
--- a/src/HOL/Multivariate_Analysis/PolyRoots.thy Tue Mar 31 16:49:41 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/PolyRoots.thy Tue Mar 31 21:54:32 2015 +0200
@@ -17,7 +17,7 @@
by (simp only: one_diff_power_eq [of "Suc n" x] lessThan_Suc_atMost)
lemma setsum_gp0:
- fixes x :: "'a::{comm_ring,division_ring_inverse_zero}"
+ fixes x :: "'a::{comm_ring,division_ring}"
shows "(\<Sum>i\<le>n. x^i) = (if x = 1 then of_nat(n + 1) else (1 - x^Suc n) / (1 - x))"
using setsum_gp_basic[of x n]
by (simp add: real_of_nat_def mult.commute divide_simps)
@@ -55,7 +55,7 @@
qed
lemma setsum_gp:
- fixes x :: "'a::{comm_ring,division_ring_inverse_zero}"
+ fixes x :: "'a::{comm_ring,division_ring}"
shows "(\<Sum>i=m..n. x^i) =
(if n < m then 0
else if x = 1 then of_nat((n + 1) - m)
@@ -65,14 +65,14 @@
by (metis eq_iff_diff_eq_0 mult.commute nonzero_divide_eq_eq)
lemma setsum_gp_offset:
- fixes x :: "'a::{comm_ring,division_ring_inverse_zero}"
+ fixes x :: "'a::{comm_ring,division_ring}"
shows "(\<Sum>i=m..m+n. x^i) =
(if x = 1 then of_nat n + 1 else x^m * (1 - x^Suc n) / (1 - x))"
using setsum_gp [of x m "m+n"]
by (auto simp: power_add algebra_simps)
lemma setsum_gp_strict:
- fixes x :: "'a::{comm_ring,division_ring_inverse_zero}"
+ fixes x :: "'a::{comm_ring,division_ring}"
shows "(\<Sum>i<n. x^i) = (if x = 1 then of_nat n else (1 - x^n) / (1 - x))"
by (induct n) (auto simp: algebra_simps divide_simps)
--- a/src/HOL/NSA/HDeriv.thy Tue Mar 31 16:49:41 2015 +0100
+++ b/src/HOL/NSA/HDeriv.thy Tue Mar 31 21:54:32 2015 +0200
@@ -366,7 +366,7 @@
done
ultimately have "(inverse (star_of x + h) - inverse (star_of x)) / h \<approx>
- (inverse (star_of x) * inverse (star_of x))"
- using assms by (simp add: nonzero_inverse_mult_distrib [symmetric] nonzero_inverse_minus_eq [symmetric])
+ using assms by simp
} then show ?thesis by (simp add: nsderiv_def)
qed
--- a/src/HOL/NSA/HyperDef.thy Tue Mar 31 16:49:41 2015 +0100
+++ b/src/HOL/NSA/HyperDef.thy Tue Mar 31 21:54:32 2015 +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} 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, field_inverse_zero} star)"
+ (of_hypreal x / of_hypreal y :: 'a::{real_field, field} star)"
by transfer (rule of_real_divide)
lemma of_hypreal_eq_iff [simp]:
@@ -445,7 +445,7 @@
by transfer (rule field_power_not_zero)
lemma hyperpow_inverse:
- "\<And>r n. r \<noteq> (0::'a::field_inverse_zero star)
+ "\<And>r n. r \<noteq> (0::'a::field star)
\<Longrightarrow> inverse (r pow n) = (inverse r) pow n"
by transfer (rule power_inverse)
--- a/src/HOL/NSA/NSA.thy Tue Mar 31 16:49:41 2015 +0100
+++ b/src/HOL/NSA/NSA.thy Tue Mar 31 21:54:32 2015 +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} star.
hnorm (inverse a) = inverse (hnorm a)"
by transfer (rule norm_inverse)
lemma hnorm_divide:
- "\<And>a b::'a::{real_normed_field, field_inverse_zero} star.
+ "\<And>a b::'a::{real_normed_field, field} star.
hnorm (a / b) = hnorm a / hnorm b"
by transfer (rule norm_divide)
--- a/src/HOL/NSA/StarDef.thy Tue Mar 31 16:49:41 2015 +0100
+++ b/src/HOL/NSA/StarDef.thy Tue Mar 31 21:54:32 2015 +0200
@@ -881,20 +881,14 @@
apply (transfer, erule left_inverse)
apply (transfer, erule right_inverse)
apply (transfer, fact divide_inverse)
+apply (transfer, fact inverse_zero)
done
-instance star :: (division_ring_inverse_zero) division_ring_inverse_zero
-by (intro_classes, transfer, rule inverse_zero)
-
instance star :: (field) field
apply (intro_classes)
apply (transfer, erule left_inverse)
apply (transfer, rule divide_inverse)
-done
-
-instance star :: (field_inverse_zero) field_inverse_zero
-apply intro_classes
-apply (rule inverse_zero)
+apply (transfer, fact inverse_zero)
done
instance star :: (ordered_semiring) ordered_semiring
@@ -937,7 +931,6 @@
instance star :: (linordered_idom) linordered_idom ..
instance star :: (linordered_field) linordered_field ..
-instance star :: (linordered_field_inverse_zero) linordered_field_inverse_zero ..
subsection {* Power *}
--- a/src/HOL/Num.thy Tue Mar 31 16:49:41 2015 +0100
+++ b/src/HOL/Num.thy Tue Mar 31 21:54:32 2015 +0200
@@ -1075,7 +1075,7 @@
subsection {* Particular lemmas concerning @{term 2} *}
-context linordered_field_inverse_zero
+context linordered_field
begin
lemma half_gt_zero_iff:
--- a/src/HOL/Numeral_Simprocs.thy Tue Mar 31 16:49:41 2015 +0100
+++ b/src/HOL/Numeral_Simprocs.thy Tue Mar 31 21:54:32 2015 +0200
@@ -115,8 +115,8 @@
{* fn phi => Numeral_Simprocs.combine_numerals *}
simproc_setup field_combine_numerals
- ("(i::'a::{field_inverse_zero,ring_char_0}) + j"
- |"(i::'a::{field_inverse_zero,ring_char_0}) - j") =
+ ("(i::'a::{field,ring_char_0}) + j"
+ |"(i::'a::{field,ring_char_0}) - j") =
{* fn phi => Numeral_Simprocs.field_combine_numerals *}
simproc_setup inteq_cancel_numerals
@@ -174,9 +174,9 @@
{* fn phi => Numeral_Simprocs.div_cancel_numeral_factor *}
simproc_setup divide_cancel_numeral_factor
- ("((l::'a::{field_inverse_zero,ring_char_0}) * m) / n"
- |"(l::'a::{field_inverse_zero,ring_char_0}) / (m * n)"
- |"((numeral v)::'a::{field_inverse_zero,ring_char_0}) / (numeral w)") =
+ ("((l::'a::{field,ring_char_0}) * m) / n"
+ |"(l::'a::{field,ring_char_0}) / (m * n)"
+ |"((numeral v)::'a::{field,ring_char_0}) / (numeral w)") =
{* fn phi => Numeral_Simprocs.divide_cancel_numeral_factor *}
simproc_setup ring_eq_cancel_factor
@@ -209,8 +209,8 @@
{* fn phi => Numeral_Simprocs.dvd_cancel_factor *}
simproc_setup divide_cancel_factor
- ("((l::'a::field_inverse_zero) * m) / n"
- |"(l::'a::field_inverse_zero) / (m * n)") =
+ ("((l::'a::field) * m) / n"
+ |"(l::'a::field) / (m * n)") =
{* fn phi => Numeral_Simprocs.divide_cancel_factor *}
ML_file "Tools/nat_numeral_simprocs.ML"
--- a/src/HOL/Power.thy Tue Mar 31 16:49:41 2015 +0100
+++ b/src/HOL/Power.thy Tue Mar 31 21:54:32 2015 +0200
@@ -705,7 +705,7 @@
text{*Perhaps these should be simprules.*}
lemma power_inverse:
- fixes a :: "'a::division_ring_inverse_zero"
+ fixes a :: "'a::division_ring"
shows "inverse (a ^ n) = inverse a ^ n"
apply (cases "a = 0")
apply (simp add: power_0_left)
@@ -713,11 +713,11 @@
done (* TODO: reorient or rename to inverse_power *)
lemma power_one_over:
- "1 / (a::'a::{field_inverse_zero, power}) ^ n = (1 / a) ^ n"
+ "1 / (a::'a::{field, power}) ^ n = (1 / a) ^ n"
by (simp add: divide_inverse) (rule power_inverse)
lemma power_divide [field_simps, divide_simps]:
- "(a / b) ^ n = (a::'a::field_inverse_zero) ^ n / b ^ n"
+ "(a / b) ^ n = (a::'a::field) ^ n / b ^ n"
apply (cases "b = 0")
apply (simp add: power_0_left)
apply (rule nonzero_power_divide)
--- a/src/HOL/Probability/Bochner_Integration.thy Tue Mar 31 16:49:41 2015 +0100
+++ b/src/HOL/Probability/Bochner_Integration.thy Tue Mar 31 21:54:32 2015 +0200
@@ -676,7 +676,7 @@
has_bochner_integral_bounded_linear[OF bounded_linear_divide]
lemma has_bochner_integral_divide_zero[intro]:
- fixes c :: "_::{real_normed_field, field_inverse_zero, second_countable_topology}"
+ fixes c :: "_::{real_normed_field, field, second_countable_topology}"
shows "(c \<noteq> 0 \<Longrightarrow> has_bochner_integral M f x) \<Longrightarrow> has_bochner_integral M (\<lambda>x. f x / c) (x / c)"
using has_bochner_integral_divide by (cases "c = 0") auto
@@ -990,7 +990,7 @@
unfolding integrable.simps by fastforce
lemma integrable_divide_zero[simp, intro]:
- fixes c :: "_::{real_normed_field, field_inverse_zero, second_countable_topology}"
+ fixes c :: "_::{real_normed_field, field, second_countable_topology}"
shows "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integrable M (\<lambda>x. f x / c)"
unfolding integrable.simps by fastforce
@@ -1098,7 +1098,7 @@
by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_inner_right)
lemma integral_divide_zero[simp]:
- fixes c :: "_::{real_normed_field, field_inverse_zero, second_countable_topology}"
+ fixes c :: "_::{real_normed_field, field, second_countable_topology}"
shows "integral\<^sup>L M (\<lambda>x. f x / c) = integral\<^sup>L M f / c"
by (rule integral_bounded_linear'[OF bounded_linear_divide bounded_linear_mult_left[of c]]) simp
--- a/src/HOL/Probability/Interval_Integral.thy Tue Mar 31 16:49:41 2015 +0100
+++ b/src/HOL/Probability/Interval_Integral.thy Tue Mar 31 21:54:32 2015 +0200
@@ -220,7 +220,7 @@
by (simp add: interval_lebesgue_integrable_def)
lemma interval_lebesgue_integrable_divide [intro, simp]:
- fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, field_inverse_zero, second_countable_topology}"
+ fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, field, second_countable_topology}"
shows "(c \<noteq> 0 \<Longrightarrow> interval_lebesgue_integrable M a b f) \<Longrightarrow>
interval_lebesgue_integrable M a b (\<lambda>x. f x / c)"
by (simp add: interval_lebesgue_integrable_def)
@@ -238,7 +238,7 @@
by (simp add: interval_lebesgue_integral_def)
lemma interval_lebesgue_integral_divide [simp]:
- fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, field_inverse_zero, second_countable_topology}"
+ fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, field, second_countable_topology}"
shows "interval_lebesgue_integral M a b (\<lambda>x. f x / c) =
interval_lebesgue_integral M a b f / c"
by (simp add: interval_lebesgue_integral_def)
--- a/src/HOL/Probability/Set_Integral.thy Tue Mar 31 16:49:41 2015 +0100
+++ b/src/HOL/Probability/Set_Integral.thy Tue Mar 31 21:54:32 2015 +0200
@@ -125,7 +125,7 @@
by (subst integral_mult_left_zero[symmetric]) (auto intro!: integral_cong)
lemma set_integral_divide_zero [simp]:
- fixes a :: "'a::{real_normed_field, field_inverse_zero, second_countable_topology}"
+ fixes a :: "'a::{real_normed_field, field, second_countable_topology}"
shows "LINT t:A|M. f t / a = (LINT t:A|M. f t) / a"
by (subst integral_divide_zero[symmetric], intro integral_cong)
(auto split: split_indicator)
@@ -150,7 +150,7 @@
using integrable_mult_left[of a M "\<lambda>x. indicator A x *\<^sub>R f x"] by simp
lemma set_integrable_divide [simp, intro]:
- fixes a :: "'a::{real_normed_field, field_inverse_zero, second_countable_topology}"
+ fixes a :: "'a::{real_normed_field, field, second_countable_topology}"
assumes "a \<noteq> 0 \<Longrightarrow> set_integrable M A f"
shows "set_integrable M A (\<lambda>t. f t / a)"
proof -
--- a/src/HOL/Quotient_Examples/Quotient_Rat.thy Tue Mar 31 16:49:41 2015 +0100
+++ b/src/HOL/Quotient_Examples/Quotient_Rat.thy Tue Mar 31 21:54:32 2015 +0200
@@ -161,7 +161,7 @@
apply auto
done
-instantiation rat :: field_inverse_zero begin
+instantiation rat :: field begin
fun rat_inverse_raw where
"rat_inverse_raw (a :: int, b :: int) = (if a = 0 then (0, 1) else (b, a))"
--- a/src/HOL/Rat.thy Tue Mar 31 16:49:41 2015 +0100
+++ b/src/HOL/Rat.thy Tue Mar 31 21:54:32 2015 +0200
@@ -101,7 +101,7 @@
shows "P q"
using assms by (cases q) simp
-instantiation rat :: field_inverse_zero
+instantiation rat :: field
begin
lift_definition zero_rat :: "rat" is "(0, 1)"
@@ -441,7 +441,7 @@
"\<not> positive x \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> positive (- x)"
by transfer (force simp: neq_iff zero_less_mult_iff mult_less_0_iff)
-instantiation rat :: linordered_field_inverse_zero
+instantiation rat :: linordered_field
begin
definition
@@ -689,7 +689,7 @@
done
lemma of_rat_inverse:
- "(of_rat (inverse a)::'a::{field_char_0, field_inverse_zero}) =
+ "(of_rat (inverse a)::'a::{field_char_0, field}) =
inverse (of_rat a)"
by (cases "a = 0", simp_all add: nonzero_of_rat_inverse)
@@ -698,7 +698,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, field_inverse_zero})
+ "(of_rat (a / b)::'a::{field_char_0, field})
= of_rat a / of_rat b"
by (cases "b = 0") (simp_all add: nonzero_of_rat_divide)
@@ -875,7 +875,7 @@
done
lemma Rats_inverse [simp]:
- fixes a :: "'a::{field_char_0, field_inverse_zero}"
+ fixes a :: "'a::{field_char_0, field}"
shows "a \<in> Rats \<Longrightarrow> inverse a \<in> Rats"
apply (auto simp add: Rats_def)
apply (rule range_eqI)
@@ -891,7 +891,7 @@
done
lemma Rats_divide [simp]:
- fixes a b :: "'a::{field_char_0, field_inverse_zero}"
+ fixes a b :: "'a::{field_char_0, field}"
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/Real.thy Tue Mar 31 16:49:41 2015 +0100
+++ b/src/HOL/Real.thy Tue Mar 31 21:54:32 2015 +0200
@@ -393,7 +393,7 @@
lemma Domainp_pcr_real [transfer_domain_rule]: "Domainp pcr_real = cauchy"
by (simp add: real.domain_eq realrel_def)
-instantiation real :: field_inverse_zero
+instantiation real :: field
begin
lift_definition zero_real :: "real" is "\<lambda>n. 0"
@@ -575,7 +575,7 @@
apply (drule (1) cauchy_not_vanishes_cases, safe, fast, fast)
done
-instantiation real :: linordered_field_inverse_zero
+instantiation real :: linordered_field
begin
definition
--- a/src/HOL/Real_Vector_Spaces.thy Tue Mar 31 16:49:41 2015 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy Tue Mar 31 21:54:32 2015 +0200
@@ -221,7 +221,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}"
shows "inverse (scaleR a x) = scaleR (inverse a) (inverse x)"
apply (case_tac "a = 0", simp)
apply (case_tac "x = 0", simp)
@@ -270,7 +270,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})"
by (simp add: of_real_def inverse_scaleR_distrib)
lemma nonzero_of_real_divide:
@@ -280,7 +280,7 @@
lemma of_real_divide [simp]:
"of_real (x / y) =
- (of_real x / of_real y :: 'a::{real_field, field_inverse_zero})"
+ (of_real x / of_real y :: 'a::{real_field, field})"
by (simp add: divide_inverse)
lemma of_real_power [simp]:
@@ -398,7 +398,7 @@
done
lemma Reals_inverse:
- fixes a :: "'a::{real_div_algebra, division_ring_inverse_zero}"
+ fixes a :: "'a::{real_div_algebra, division_ring}"
shows "a \<in> Reals \<Longrightarrow> inverse a \<in> Reals"
apply (auto simp add: Reals_def)
apply (rule range_eqI)
@@ -406,7 +406,7 @@
done
lemma Reals_inverse_iff [simp]:
- fixes x:: "'a :: {real_div_algebra, division_ring_inverse_zero}"
+ fixes x:: "'a :: {real_div_algebra, division_ring}"
shows "inverse x \<in> \<real> \<longleftrightarrow> x \<in> \<real>"
by (metis Reals_inverse inverse_inverse_eq)
@@ -419,7 +419,7 @@
done
lemma Reals_divide [simp]:
- fixes a b :: "'a::{real_field, field_inverse_zero}"
+ fixes a b :: "'a::{real_field, field}"
shows "\<lbrakk>a \<in> Reals; b \<in> Reals\<rbrakk> \<Longrightarrow> a / b \<in> Reals"
apply (auto simp add: Reals_def)
apply (rule range_eqI)
@@ -819,7 +819,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}"
shows "norm (inverse a) = inverse (norm a)"
apply (case_tac "a = 0", simp)
apply (erule nonzero_norm_inverse)
@@ -831,7 +831,7 @@
by (simp add: divide_inverse norm_mult nonzero_norm_inverse)
lemma norm_divide:
- fixes a b :: "'a::{real_normed_field, field_inverse_zero}"
+ fixes a b :: "'a::{real_normed_field, field}"
shows "norm (a / b) = norm a / norm b"
by (simp add: divide_inverse norm_mult norm_inverse)
--- a/src/HOL/Tools/numeral_simprocs.ML Tue Mar 31 16:49:41 2015 +0100
+++ b/src/HOL/Tools/numeral_simprocs.ML Tue Mar 31 21:54:32 2015 +0200
@@ -449,12 +449,12 @@
val field_divide_cancel_numeral_factor =
[prep_simproc @{theory}
("field_divide_cancel_numeral_factor",
- ["((l::'a::field_inverse_zero) * m) / n",
- "(l::'a::field_inverse_zero) / (m * n)",
- "((numeral v)::'a::field_inverse_zero) / (numeral w)",
- "((numeral v)::'a::field_inverse_zero) / (- numeral w)",
- "((- numeral v)::'a::field_inverse_zero) / (numeral w)",
- "((- numeral v)::'a::field_inverse_zero) / (- numeral w)"],
+ ["((l::'a::field) * m) / n",
+ "(l::'a::field) / (m * n)",
+ "((numeral v)::'a::field) / (numeral w)",
+ "((numeral v)::'a::field) / (- numeral w)",
+ "((- numeral v)::'a::field) / (numeral w)",
+ "((- numeral v)::'a::field) / (- numeral w)"],
DivideCancelNumeralFactor.proc)];
val field_cancel_numeral_factors =
--- a/src/HOL/Transcendental.thy Tue Mar 31 16:49:41 2015 +0100
+++ b/src/HOL/Transcendental.thy Tue Mar 31 21:54:32 2015 +0200
@@ -2231,7 +2231,7 @@
lemma ln_powr_bound: "1 <= x ==> 0 < a ==> ln x <= (x powr a) / a"
by (metis less_eq_real_def ln_less_self mult_imp_le_div_pos ln_powr mult.commute
- order.strict_trans2 powr_gt_zero zero_less_one)
+ powr_gt_zero)
lemma ln_powr_bound2:
assumes "1 < x" and "0 < a"
@@ -3109,29 +3109,29 @@
shows "cos(w) * cos(z) = (cos(w - z) + cos(w + z)) / 2"
by (simp add: cos_diff cos_add)
-lemma sin_plus_sin: (*FIXME field_inverse_zero should not be necessary*)
- fixes w :: "'a::{real_normed_field,banach,field_inverse_zero}"
+lemma sin_plus_sin: (*FIXME field should not be necessary*)
+ fixes w :: "'a::{real_normed_field,banach,field}"
shows "sin(w) + sin(z) = 2 * sin((w + z) / 2) * cos((w - z) / 2)"
apply (simp add: mult.assoc sin_times_cos)
apply (simp add: field_simps)
done
lemma sin_diff_sin:
- fixes w :: "'a::{real_normed_field,banach,field_inverse_zero}"
+ fixes w :: "'a::{real_normed_field,banach,field}"
shows "sin(w) - sin(z) = 2 * sin((w - z) / 2) * cos((w + z) / 2)"
apply (simp add: mult.assoc sin_times_cos)
apply (simp add: field_simps)
done
lemma cos_plus_cos:
- fixes w :: "'a::{real_normed_field,banach,field_inverse_zero}"
+ fixes w :: "'a::{real_normed_field,banach,field}"
shows "cos(w) + cos(z) = 2 * cos((w + z) / 2) * cos((w - z) / 2)"
apply (simp add: mult.assoc cos_times_cos)
apply (simp add: field_simps)
done
lemma cos_diff_cos:
- fixes w :: "'a::{real_normed_field,banach,field_inverse_zero}"
+ fixes w :: "'a::{real_normed_field,banach,field}"
shows "cos(w) - cos(z) = 2 * sin((w + z) / 2) * sin((z - w) / 2)"
apply (simp add: mult.assoc sin_times_sin)
apply (simp add: field_simps)
@@ -3671,12 +3671,12 @@
where "tan = (\<lambda>x. sin x / cos x)"
lemma tan_of_real:
- fixes XXX :: "'a::{real_normed_field,banach,field_inverse_zero}"
+ fixes XXX :: "'a::{real_normed_field,banach}"
shows "of_real(tan x) = (tan(of_real x) :: 'a)"
by (simp add: tan_def sin_of_real cos_of_real)
lemma tan_in_Reals [simp]:
- fixes z :: "'a::{real_normed_field,banach,field_inverse_zero}"
+ fixes z :: "'a::{real_normed_field,banach}"
shows "z \<in> \<real> \<Longrightarrow> tan z \<in> \<real>"
by (simp add: tan_def)
@@ -3730,7 +3730,7 @@
qed
lemma tan_half:
- fixes x :: "'a::{real_normed_field,banach,field_inverse_zero}"
+ fixes x :: "'a::{real_normed_field,banach,field}"
shows "tan x = sin (2 * x) / (cos (2 * x) + 1)"
unfolding tan_def sin_double cos_double sin_squared_eq
by (simp add: power2_eq_square)
@@ -4137,7 +4137,7 @@
by (simp add: eq_divide_eq)
lemma tan_sec:
- fixes x :: "'a::{real_normed_field,banach,field_inverse_zero}"
+ fixes x :: "'a::{real_normed_field,banach,field}"
shows "cos x \<noteq> 0 \<Longrightarrow> 1 + (tan x)\<^sup>2 = (inverse (cos x))\<^sup>2"
apply (rule power_inverse [THEN subst])
apply (rule_tac c1 = "(cos x)\<^sup>2" in mult_right_cancel [THEN iffD1])
--- a/src/HOL/ex/Dedekind_Real.thy Tue Mar 31 16:49:41 2015 +0100
+++ b/src/HOL/ex/Dedekind_Real.thy Tue Mar 31 21:54:32 2015 +0200
@@ -1435,7 +1435,7 @@
subsection{*The Real Numbers form a Field*}
-instance real :: field_inverse_zero
+instance real :: field
proof
fix x y z :: real
show "x \<noteq> 0 ==> inverse x * x = 1" by (rule real_mult_inverse_left)
@@ -1574,7 +1574,7 @@
subsection{*The Reals Form an Ordered Field*}
-instance real :: linordered_field_inverse_zero
+instance real :: linordered_field
proof
fix x y z :: real
show "x \<le> y ==> z + x \<le> z + y" by (rule real_add_left_mono)
--- a/src/HOL/ex/Simproc_Tests.thy Tue Mar 31 16:49:41 2015 +0100
+++ b/src/HOL/ex/Simproc_Tests.thy Tue Mar 31 21:54:32 2015 +0200
@@ -279,7 +279,7 @@
subsection {* @{text divide_cancel_numeral_factor} *}
notepad begin
- fix x y z :: "'a::{field_inverse_zero,ring_char_0}"
+ fix x y z :: "'a::{field,ring_char_0}"
{
assume "(3*x) / (4*y) = z" have "(9*x) / (12 * y) = z"
by (tactic {* test @{context} [@{simproc divide_cancel_numeral_factor}] *}) fact
@@ -346,13 +346,13 @@
}
end
-lemma shows "a*(b*c)/(y*z) = d*(b::'a::linordered_field_inverse_zero)*(x*a)/z"
+lemma shows "a*(b*c)/(y*z) = d*(b::'a::linordered_field)*(x*a)/z"
oops -- "FIXME: need simproc to cover this case"
subsection {* @{text divide_cancel_factor} *}
notepad begin
- fix a b c d k uu x y :: "'a::field_inverse_zero"
+ fix a b c d k uu x y :: "'a::field"
{
assume "(if k = 0 then 0 else x / y) = uu"
have "(x*k) / (k*y) = uu"
@@ -373,7 +373,7 @@
end
lemma
- fixes a b c d x y z :: "'a::linordered_field_inverse_zero"
+ fixes a b c d x y z :: "'a::linordered_field"
shows "a*(b*c)/(y*z) = d*(b)*(x*a)/z"
oops -- "FIXME: need simproc to cover this case"
@@ -420,7 +420,7 @@
subsection {* @{text field_combine_numerals} *}
notepad begin
- fix x y z uu :: "'a::{field_inverse_zero,ring_char_0}"
+ fix x y z uu :: "'a::{field,ring_char_0}"
{
assume "5 / 6 * x = uu" have "x / 2 + x / 3 = uu"
by (tactic {* test @{context} [@{simproc field_combine_numerals}] *}) fact
@@ -442,7 +442,7 @@
end
lemma
- fixes x :: "'a::{linordered_field_inverse_zero}"
+ fixes x :: "'a::{linordered_field}"
shows "2/3 * x + x / 3 = uu"
apply (tactic {* test @{context} [@{simproc field_combine_numerals}] *})?
oops -- "FIXME: test fails"