src/HOL/Library/Abstract_Rat.thy
 changeset 35028 108662d50512 parent 33657 a4179bf442d1 child 36349 39be26d1bc28
```     1.1 --- a/src/HOL/Library/Abstract_Rat.thy	Fri Feb 05 14:33:31 2010 +0100
1.2 +++ b/src/HOL/Library/Abstract_Rat.thy	Fri Feb 05 14:33:50 2010 +0100
1.3 @@ -332,7 +332,7 @@
1.4  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.5
1.6  lemma Nlt0_iff[simp]: assumes nx: "isnormNum x"
1.7 -  shows "((INum x :: 'a :: {ring_char_0,division_by_zero,ordered_field})< 0) = 0>\<^sub>N x "
1.8 +  shows "((INum x :: 'a :: {ring_char_0,division_by_zero,linordered_field})< 0) = 0>\<^sub>N x "
1.9  proof-
1.10    have " \<exists> a b. x = (a,b)" by simp
1.11    then obtain a b where x[simp]:"x = (a,b)" by blast
1.12 @@ -345,7 +345,7 @@
1.13  qed
1.14
1.15  lemma Nle0_iff[simp]:assumes nx: "isnormNum x"
1.16 -  shows "((INum x :: 'a :: {ring_char_0,division_by_zero,ordered_field}) \<le> 0) = 0\<ge>\<^sub>N x"
1.17 +  shows "((INum x :: 'a :: {ring_char_0,division_by_zero,linordered_field}) \<le> 0) = 0\<ge>\<^sub>N x"
1.18  proof-
1.19    have " \<exists> a b. x = (a,b)" by simp
1.20    then obtain a b where x[simp]:"x = (a,b)" by blast
1.21 @@ -357,7 +357,7 @@
1.22    ultimately show ?thesis by blast
1.23  qed
1.24
1.25 -lemma Ngt0_iff[simp]:assumes nx: "isnormNum x" shows "((INum x :: 'a :: {ring_char_0,division_by_zero,ordered_field})> 0) = 0<\<^sub>N x"
1.26 +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.27  proof-
1.28    have " \<exists> a b. x = (a,b)" by simp
1.29    then obtain a b where x[simp]:"x = (a,b)" by blast
1.30 @@ -369,7 +369,7 @@
1.31    ultimately show ?thesis by blast
1.32  qed
1.33  lemma Nge0_iff[simp]:assumes nx: "isnormNum x"
1.34 -  shows "((INum x :: 'a :: {ring_char_0,division_by_zero,ordered_field}) \<ge> 0) = 0\<le>\<^sub>N x"
1.35 +  shows "((INum x :: 'a :: {ring_char_0,division_by_zero,linordered_field}) \<ge> 0) = 0\<le>\<^sub>N x"
1.36  proof-
1.37    have " \<exists> a b. x = (a,b)" by simp
1.38    then obtain a b where x[simp]:"x = (a,b)" by blast
1.39 @@ -382,7 +382,7 @@
1.40  qed
1.41
1.42  lemma Nlt_iff[simp]: assumes nx: "isnormNum x" and ny: "isnormNum y"
1.43 -  shows "((INum x :: 'a :: {ring_char_0,division_by_zero,ordered_field}) < INum y) = (x <\<^sub>N y)"
1.44 +  shows "((INum x :: 'a :: {ring_char_0,division_by_zero,linordered_field}) < INum y) = (x <\<^sub>N y)"
1.45  proof-
1.46    let ?z = "0::'a"
1.47    have "((INum x ::'a) < INum y) = (INum (x -\<^sub>N y) < ?z)" using nx ny by simp
1.48 @@ -391,7 +391,7 @@
1.49  qed
1.50
1.51  lemma Nle_iff[simp]: assumes nx: "isnormNum x" and ny: "isnormNum y"
1.52 -  shows "((INum x :: 'a :: {ring_char_0,division_by_zero,ordered_field})\<le> INum y) = (x \<le>\<^sub>N y)"
1.53 +  shows "((INum x :: 'a :: {ring_char_0,division_by_zero,linordered_field})\<le> INum y) = (x \<le>\<^sub>N y)"
1.54  proof-
1.55    have "((INum x ::'a) \<le> INum y) = (INum (x -\<^sub>N y) \<le> (0::'a))" using nx ny by simp
1.56    also have "\<dots> = (0\<ge>\<^sub>N (x -\<^sub>N y))" using Nle0_iff[OF Nsub_normN[OF ny]] by simp
```