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