src/HOL/Ring_and_Field.thy
changeset 24748 ee0a0eb6b738
parent 24515 d4dc5dc2db98
child 25062 af5ef0d4d655
     1.1 --- a/src/HOL/Ring_and_Field.thy	Fri Sep 28 10:35:53 2007 +0200
     1.2 +++ b/src/HOL/Ring_and_Field.thy	Sat Sep 29 08:58:51 2007 +0200
     1.3 @@ -153,7 +153,7 @@
     1.4  qed
     1.5  
     1.6  class field = comm_ring_1 + inverse +
     1.7 -  assumes field_inverse:  "a \<noteq> 0 \<Longrightarrow> inverse a \<^loc>* a = \<^loc>1"
     1.8 +  assumes field_inverse:  "a \<noteq> \<^loc>0 \<Longrightarrow> inverse a \<^loc>* a = \<^loc>1"
     1.9    assumes divide_inverse: "a \<^loc>/ b = a \<^loc>* inverse b"
    1.10  
    1.11  instance field \<subseteq> division_ring
    1.12 @@ -211,8 +211,8 @@
    1.13  lemmas ring_simps = group_simps ring_distribs
    1.14  
    1.15  class mult_mono = times + zero + ord +
    1.16 -  assumes mult_left_mono: "a \<sqsubseteq> b \<Longrightarrow> \<^loc>0 \<sqsubseteq> c \<Longrightarrow> c \<^loc>* a \<sqsubseteq> c \<^loc>* b"
    1.17 -  assumes mult_right_mono: "a \<sqsubseteq> b \<Longrightarrow> \<^loc>0 \<sqsubseteq> c \<Longrightarrow> a \<^loc>* c \<sqsubseteq> b \<^loc>* c"
    1.18 +  assumes mult_left_mono: "a \<^loc>\<le> b \<Longrightarrow> \<^loc>0 \<^loc>\<le> c \<Longrightarrow> c \<^loc>* a \<^loc>\<le> c \<^loc>* b"
    1.19 +  assumes mult_right_mono: "a \<^loc>\<le> b \<Longrightarrow> \<^loc>0 \<^loc>\<le> c \<Longrightarrow> a \<^loc>* c \<^loc>\<le> b \<^loc>* c"
    1.20  
    1.21  class pordered_semiring = mult_mono + semiring_0 + pordered_ab_semigroup_add 
    1.22  
    1.23 @@ -228,8 +228,8 @@
    1.24  instance ordered_semiring \<subseteq> pordered_cancel_semiring ..
    1.25  
    1.26  class ordered_semiring_strict = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add +
    1.27 -  assumes mult_strict_left_mono: "a \<sqsubset> b \<Longrightarrow> \<^loc>0 \<sqsubset> c \<Longrightarrow> c \<^loc>* a \<sqsubset> c \<^loc>* b"
    1.28 -  assumes mult_strict_right_mono: "a \<sqsubset> b \<Longrightarrow> \<^loc>0 \<sqsubset> c \<Longrightarrow> a \<^loc>* c \<sqsubset> b \<^loc>* c"
    1.29 +  assumes mult_strict_left_mono: "a \<^loc>< b \<Longrightarrow> \<^loc>0 \<^loc>< c \<Longrightarrow> c \<^loc>* a \<^loc>< c \<^loc>* b"
    1.30 +  assumes mult_strict_right_mono: "a \<^loc>< b \<Longrightarrow> \<^loc>0 \<^loc>< c \<Longrightarrow> a \<^loc>* c \<^loc>< b \<^loc>* c"
    1.31  
    1.32  instance ordered_semiring_strict \<subseteq> semiring_0_cancel ..
    1.33  
    1.34 @@ -246,7 +246,7 @@
    1.35  qed
    1.36  
    1.37  class mult_mono1 = times + zero + ord +
    1.38 -  assumes mult_mono: "a \<sqsubseteq> b \<Longrightarrow> \<^loc>0 \<sqsubseteq> c \<Longrightarrow> c \<^loc>* a \<sqsubseteq> c \<^loc>* b"
    1.39 +  assumes mult_mono: "a \<^loc>\<le> b \<Longrightarrow> \<^loc>0 \<^loc>\<le> c \<Longrightarrow> c \<^loc>* a \<^loc>\<le> c \<^loc>* b"
    1.40  
    1.41  class pordered_comm_semiring = comm_semiring_0
    1.42    + pordered_ab_semigroup_add + mult_mono1
    1.43 @@ -257,7 +257,7 @@
    1.44  instance pordered_cancel_comm_semiring \<subseteq> pordered_comm_semiring ..
    1.45  
    1.46  class ordered_comm_semiring_strict = comm_semiring_0 + ordered_cancel_ab_semigroup_add +
    1.47 -  assumes mult_strict_mono: "a \<sqsubset> b \<Longrightarrow> \<^loc>0 \<sqsubset> c \<Longrightarrow> c \<^loc>* a \<sqsubset> c \<^loc>* b"
    1.48 +  assumes mult_strict_mono: "a \<^loc>< b \<Longrightarrow> \<^loc>0 \<^loc>< c \<Longrightarrow> c \<^loc>* a \<^loc>< c \<^loc>* b"
    1.49  
    1.50  instance pordered_comm_semiring \<subseteq> pordered_semiring
    1.51  proof
    1.52 @@ -297,10 +297,10 @@
    1.53  instance lordered_ring \<subseteq> lordered_ab_group_join ..
    1.54  
    1.55  class abs_if = minus + ord + zero + abs +
    1.56 -  assumes abs_if: "abs a = (if a \<sqsubset> 0 then (uminus a) else a)"
    1.57 +  assumes abs_if: "abs a = (if a \<^loc>< \<^loc>0 then (uminus a) else a)"
    1.58  
    1.59  class sgn_if = sgn + zero + one + minus + ord +
    1.60 -assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 \<sqsubset> x then 1 else uminus 1)"
    1.61 +  assumes sgn_if: "sgn x = (if x = \<^loc>0 then \<^loc>0 else if \<^loc>0 \<^loc>< x then \<^loc>1 else uminus \<^loc>1)"
    1.62  
    1.63  (* The "strict" suffix can be seen as describing the combination of ordered_ring and no_zero_divisors.
    1.64     Basically, ordered_ring + no_zero_divisors = ordered_ring_strict.
    1.65 @@ -327,7 +327,7 @@
    1.66  
    1.67  class ordered_semidom = comm_semiring_1_cancel + ordered_comm_semiring_strict +
    1.68    (*previously ordered_semiring*)
    1.69 -  assumes zero_less_one [simp]: "\<^loc>0 \<sqsubset> \<^loc>1"
    1.70 +  assumes zero_less_one [simp]: "\<^loc>0 \<^loc>< \<^loc>1"
    1.71  
    1.72  lemma pos_add_strict:
    1.73    fixes a b c :: "'a\<Colon>ordered_semidom"