src/HOL/Library/Abstract_Rat.thy
 changeset 36409 d323e7773aa8 parent 36349 39be26d1bc28 child 36411 4cd87067791e
```     1.1 --- a/src/HOL/Library/Abstract_Rat.thy	Mon Apr 26 11:34:19 2010 +0200
1.2 +++ b/src/HOL/Library/Abstract_Rat.thy	Mon Apr 26 15:37:50 2010 +0200
1.3 @@ -184,7 +184,7 @@
1.4
1.5  lemma isnormNum_unique[simp]:
1.6    assumes na: "isnormNum x" and nb: "isnormNum y"
1.7 -  shows "((INum x ::'a::{ring_char_0,field, division_ring_inverse_zero}) = INum y) = (x = y)" (is "?lhs = ?rhs")
1.8 +  shows "((INum x ::'a::{field_char_0, field_inverse_zero}) = INum y) = (x = y)" (is "?lhs = ?rhs")
1.9  proof
1.10    have "\<exists> a b a' b'. x = (a,b) \<and> y = (a',b')" by auto
1.11    then obtain a b a' b' where xy[simp]: "x = (a,b)" "y=(a',b')" by blast
1.12 @@ -217,11 +217,11 @@
1.13  qed
1.14
1.15
1.16 -lemma isnormNum0[simp]: "isnormNum x \<Longrightarrow> (INum x = (0::'a::{ring_char_0, field,division_ring_inverse_zero})) = (x = 0\<^sub>N)"
1.17 +lemma isnormNum0[simp]: "isnormNum x \<Longrightarrow> (INum x = (0::'a::{field_char_0, field_inverse_zero})) = (x = 0\<^sub>N)"
1.18    unfolding INum_int(2)[symmetric]
1.19    by (rule isnormNum_unique, simp_all)
1.20
1.21 -lemma of_int_div_aux: "d ~= 0 ==> ((of_int x)::'a::{field, ring_char_0}) / (of_int d) =
1.22 +lemma of_int_div_aux: "d ~= 0 ==> ((of_int x)::'a::field_char_0) / (of_int d) =
1.23      of_int (x div d) + (of_int (x mod d)) / ((of_int d)::'a)"
1.24  proof -
1.25    assume "d ~= 0"
1.26 @@ -238,14 +238,14 @@
1.27  qed
1.28
1.29  lemma of_int_div: "(d::int) ~= 0 ==> d dvd n ==>
1.30 -    (of_int(n div d)::'a::{field, ring_char_0}) = of_int n / of_int d"
1.31 +    (of_int(n div d)::'a::field_char_0) = of_int n / of_int d"
1.32    apply (frule of_int_div_aux [of d n, where ?'a = 'a])
1.33    apply simp
1.35  done
1.36
1.37
1.38 -lemma normNum[simp]: "INum (normNum x) = (INum x :: 'a::{ring_char_0,field, division_ring_inverse_zero})"
1.39 +lemma normNum[simp]: "INum (normNum x) = (INum x :: 'a::{field_char_0, field_inverse_zero})"
1.40  proof-
1.41    have "\<exists> a b. x = (a,b)" by auto
1.42    then obtain a b where x[simp]: "x = (a,b)" by blast
1.43 @@ -260,7 +260,7 @@
1.44    ultimately show ?thesis by blast
1.45  qed
1.46
1.47 -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")
1.48 +lemma INum_normNum_iff: "(INum x ::'a::{field_char_0, field_inverse_zero}) = INum y \<longleftrightarrow> normNum x = normNum y" (is "?lhs = ?rhs")
1.49  proof -
1.50    have "normNum x = normNum y \<longleftrightarrow> (INum (normNum x) :: 'a) = INum (normNum y)"
1.51      by (simp del: normNum)
1.52 @@ -268,7 +268,7 @@
1.53    finally show ?thesis by simp
1.54  qed
1.55
1.56 -lemma Nadd[simp]: "INum (x +\<^sub>N y) = INum x + (INum y :: 'a :: {ring_char_0,division_ring_inverse_zero,field})"
1.57 +lemma Nadd[simp]: "INum (x +\<^sub>N y) = INum x + (INum y :: 'a :: {field_char_0, field_inverse_zero})"
1.58  proof-
1.59  let ?z = "0:: 'a"
1.60    have " \<exists> a b. x = (a,b)" " \<exists> a' b'. y = (a',b')" by auto
1.61 @@ -300,7 +300,7 @@
1.62    ultimately show ?thesis by blast
1.63  qed
1.64
1.65 -lemma Nmul[simp]: "INum (x *\<^sub>N y) = INum x * (INum y:: 'a :: {ring_char_0,division_ring_inverse_zero,field}) "
1.66 +lemma Nmul[simp]: "INum (x *\<^sub>N y) = INum x * (INum y:: 'a :: {field_char_0, field_inverse_zero}) "
1.67  proof-
1.68    let ?z = "0::'a"
1.69    have " \<exists> a b. x = (a,b)" " \<exists> a' b'. y = (a',b')" by auto
1.70 @@ -323,16 +323,16 @@
1.71  lemma Nneg[simp]: "INum (~\<^sub>N x) = - (INum x ::'a:: field)"
1.72    by (simp add: Nneg_def split_def INum_def)
1.73
1.74 -lemma Nsub[simp]: shows "INum (x -\<^sub>N y) = INum x - (INum y:: 'a :: {ring_char_0,division_ring_inverse_zero,field})"
1.75 +lemma Nsub[simp]: shows "INum (x -\<^sub>N y) = INum x - (INum y:: 'a :: {field_char_0, field_inverse_zero})"
1.76  by (simp add: Nsub_def split_def)
1.77
1.78 -lemma Ninv[simp]: "INum (Ninv x) = (1::'a :: {division_ring_inverse_zero,field}) / (INum x)"
1.79 +lemma Ninv[simp]: "INum (Ninv x) = (1::'a :: field_inverse_zero) / (INum x)"
1.80    by (simp add: Ninv_def INum_def split_def)
1.81
1.82 -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)
1.83 +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)
1.84
1.85  lemma Nlt0_iff[simp]: assumes nx: "isnormNum x"
1.86 -  shows "((INum x :: 'a :: {ring_char_0,division_ring_inverse_zero,linordered_field})< 0) = 0>\<^sub>N x "
1.87 +  shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero})< 0) = 0>\<^sub>N x "
1.88  proof-
1.89    have " \<exists> a b. x = (a,b)" by simp
1.90    then obtain a b where x[simp]:"x = (a,b)" by blast
1.91 @@ -345,7 +345,7 @@
1.92  qed
1.93
1.94  lemma Nle0_iff[simp]:assumes nx: "isnormNum x"
1.95 -  shows "((INum x :: 'a :: {ring_char_0,division_ring_inverse_zero,linordered_field}) \<le> 0) = 0\<ge>\<^sub>N x"
1.96 +  shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero}) \<le> 0) = 0\<ge>\<^sub>N x"
1.97  proof-
1.98    have " \<exists> a b. x = (a,b)" by simp
1.99    then obtain a b where x[simp]:"x = (a,b)" by blast
1.100 @@ -357,7 +357,7 @@
1.101    ultimately show ?thesis by blast
1.102  qed
1.103
1.104 -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"
1.105 +lemma Ngt0_iff[simp]:assumes nx: "isnormNum x" shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero})> 0) = 0<\<^sub>N x"
1.106  proof-
1.107    have " \<exists> a b. x = (a,b)" by simp
1.108    then obtain a b where x[simp]:"x = (a,b)" by blast
1.109 @@ -369,7 +369,7 @@
1.110    ultimately show ?thesis by blast
1.111  qed
1.112  lemma Nge0_iff[simp]:assumes nx: "isnormNum x"
1.113 -  shows "((INum x :: 'a :: {ring_char_0,division_ring_inverse_zero,linordered_field}) \<ge> 0) = 0\<le>\<^sub>N x"
1.114 +  shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero}) \<ge> 0) = 0\<le>\<^sub>N x"
1.115  proof-
1.116    have " \<exists> a b. x = (a,b)" by simp
1.117    then obtain a b where x[simp]:"x = (a,b)" by blast
1.118 @@ -382,7 +382,7 @@
1.119  qed
1.120
1.121  lemma Nlt_iff[simp]: assumes nx: "isnormNum x" and ny: "isnormNum y"
1.122 -  shows "((INum x :: 'a :: {ring_char_0,division_ring_inverse_zero,linordered_field}) < INum y) = (x <\<^sub>N y)"
1.123 +  shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero}) < INum y) = (x <\<^sub>N y)"
1.124  proof-
1.125    let ?z = "0::'a"
1.126    have "((INum x ::'a) < INum y) = (INum (x -\<^sub>N y) < ?z)" using nx ny by simp
1.127 @@ -391,7 +391,7 @@
1.128  qed
1.129
1.130  lemma Nle_iff[simp]: assumes nx: "isnormNum x" and ny: "isnormNum y"
1.131 -  shows "((INum x :: 'a :: {ring_char_0,division_ring_inverse_zero,linordered_field})\<le> INum y) = (x \<le>\<^sub>N y)"
1.132 +  shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero})\<le> INum y) = (x \<le>\<^sub>N y)"
1.133  proof-
1.134    have "((INum x ::'a) \<le> INum y) = (INum (x -\<^sub>N y) \<le> (0::'a))" using nx ny by simp
1.135    also have "\<dots> = (0\<ge>\<^sub>N (x -\<^sub>N y))" using Nle0_iff[OF Nsub_normN[OF ny]] by simp
1.136 @@ -399,7 +399,7 @@
1.137  qed
1.138
1.140 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
1.141 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.142    shows "x +\<^sub>N y = y +\<^sub>N x"
1.143  proof-
1.144    have n: "isnormNum (x +\<^sub>N y)" "isnormNum (y +\<^sub>N x)" by simp_all
1.145 @@ -408,7 +408,7 @@
1.146  qed
1.147
1.148  lemma [simp]:
1.149 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
1.150 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.151    shows "(0, b) +\<^sub>N y = normNum y"
1.152      and "(a, 0) +\<^sub>N y = normNum y"
1.153      and "x +\<^sub>N (0, b) = normNum x"
1.154 @@ -420,7 +420,7 @@
1.155    done
1.156
1.157  lemma normNum_nilpotent_aux[simp]:
1.158 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
1.159 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.160    assumes nx: "isnormNum x"
1.161    shows "normNum x = x"
1.162  proof-
1.163 @@ -432,7 +432,7 @@
1.164  qed
1.165
1.166  lemma normNum_nilpotent[simp]:
1.167 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
1.168 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.169    shows "normNum (normNum x) = normNum x"
1.170    by simp
1.171
1.172 @@ -440,11 +440,11 @@
1.174
1.176 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
1.177 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.178    shows "normNum (x +\<^sub>N y) = x +\<^sub>N y" by simp
1.179
1.181 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
1.182 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.183    shows "normNum x +\<^sub>N y = x +\<^sub>N y"
1.184  proof-
1.185    have n: "isnormNum (normNum x +\<^sub>N y)" "isnormNum (x +\<^sub>N y)" by simp_all
1.186 @@ -454,7 +454,7 @@
1.187  qed
1.188
1.190 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
1.191 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.192    shows "x +\<^sub>N normNum y = x +\<^sub>N y"
1.193  proof-
1.194    have n: "isnormNum (x +\<^sub>N normNum y)" "isnormNum (x +\<^sub>N y)" by simp_all
1.195 @@ -464,7 +464,7 @@
1.196  qed
1.197
1.199 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
1.200 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.201    shows "x +\<^sub>N y +\<^sub>N z = x +\<^sub>N (y +\<^sub>N z)"
1.202  proof-
1.203    have n: "isnormNum (x +\<^sub>N y +\<^sub>N z)" "isnormNum (x +\<^sub>N (y +\<^sub>N z))" by simp_all
1.204 @@ -476,7 +476,7 @@
1.205    by (simp add: Nmul_def split_def Let_def gcd_commute_int mult_commute)
1.206
1.207  lemma Nmul_assoc:
1.208 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
1.209 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.210    assumes nx: "isnormNum x" and ny:"isnormNum y" and nz:"isnormNum z"
1.211    shows "x *\<^sub>N y *\<^sub>N z = x *\<^sub>N (y *\<^sub>N z)"
1.212  proof-
1.213 @@ -487,7 +487,7 @@
1.214  qed
1.215
1.216  lemma Nsub0:
1.217 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
1.218 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.219    assumes x: "isnormNum x" and y:"isnormNum y" shows "(x -\<^sub>N y = 0\<^sub>N) = (x = y)"
1.220  proof-
1.221    { fix h :: 'a
1.222 @@ -502,7 +502,7 @@
1.223    by (simp_all add: Nmul_def Let_def split_def)
1.224
1.225  lemma Nmul_eq0[simp]:
1.226 -  assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})"
1.227 +  assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.228    assumes nx:"isnormNum x" and ny: "isnormNum y"
1.229    shows "(x*\<^sub>N y = 0\<^sub>N) = (x = 0\<^sub>N \<or> y = 0\<^sub>N)"
1.230  proof-
```