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.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.161
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.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.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.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-
```