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