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.34    apply (simp add: dvd_eq_mod_eq_0)
    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.139  lemma Nadd_commute:
   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.173    by (simp_all add: normNum_def)
   1.174  
   1.175  lemma normNum_Nadd:
   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.180  lemma Nadd_normNum1[simp]:
   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.189  lemma Nadd_normNum2[simp]:
   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.198  lemma Nadd_assoc:
   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-