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