src/HOL/Library/Ring_and_Field.thy
author oheimb
Wed Jan 31 10:15:55 2001 +0100 (2001-01-31)
changeset 11008 f7333f055ef6
parent 10946 c03f7dcee8b2
child 11099 b301d1f72552
permissions -rw-r--r--
improved theory reference in comment
     1 (*  Title:      HOL/Library/Ring_and_Field.thy
     2     ID:         $Id$
     3     Author:     Gertrud Bauer and Markus Wenzel, TU Muenchen
     4 *)
     5 
     6 header {*
     7   \title{Ring and field structures}
     8   \author{Gertrud Bauer and Markus Wenzel}
     9 *}
    10 
    11 theory Ring_and_Field = Main: 
    12 
    13 subsection {* Abstract algebraic structures *}
    14 
    15 axclass ring < zero, plus, minus, times, number
    16   add_assoc: "(a + b) + c = a + (b + c)"
    17   add_commute: "a + b = b + a"
    18   left_zero [simp]: "0 + a = a"
    19   left_minus [simp]: "- a + a = 0"
    20   diff_minus: "a - b = a + (-b)"
    21   zero_number: "0 = #0"
    22 
    23   mult_assoc: "(a * b) * c = a * (b * c)"
    24   mult_commute: "a * b = b * a"
    25   left_one [simp]: "#1 * a = a"
    26 
    27   left_distrib: "(a + b) * c = a * c + b * c"
    28 
    29 axclass ordered_ring < ring, linorder
    30   add_left_mono: "a \<le> b ==> c + a \<le> c + b"
    31   mult_strict_left_mono: "a < b ==> 0 < c ==> c * a < c * b"
    32   abs_if: "\<bar>a\<bar> = (if a < 0 then -a else a)"
    33 
    34 axclass field < ring, inverse
    35   left_inverse [simp]: "a \<noteq> 0 ==> inverse a * a = #1"
    36   divide_inverse: "b \<noteq> 0 ==> a / b = a * inverse b"
    37 
    38 axclass ordered_field < ordered_ring, field
    39 
    40 axclass division_by_zero < zero, inverse
    41   inverse_zero: "inverse 0 = 0"
    42   divide_zero: "a / 0 = 0"
    43 
    44 
    45 
    46 subsection {* Derived rules *}
    47 
    48 subsubsection {* Derived rules for addition *}
    49 
    50 lemma right_zero [simp]: "a + 0 = (a::'a::ring)" 
    51 proof -
    52   have "a + 0 = 0 + a" by (simp only: add_commute)
    53   also have "... = a" by simp
    54   finally show ?thesis .
    55 qed
    56 
    57 lemma add_left_commute: "a + (b + c) = b + (a + (c::'a::ring))"
    58 proof -
    59   have "a + (b + c) = (a + b) + c" by (simp only: add_assoc)
    60   also have "... = (b + a) + c" by (simp only: add_commute)
    61   finally show ?thesis by (simp only: add_assoc) 
    62 qed
    63 
    64 theorems ring_add_ac = add_assoc add_commute add_left_commute
    65 
    66 lemma right_minus [simp]: "a + -(a::'a::ring) = 0" 
    67 proof -
    68   have "a + -a = -a + a" by (simp add: ring_add_ac)
    69   also have "... = 0" by simp
    70   finally show ?thesis .
    71 qed
    72 
    73 lemma right_minus_eq: "(a - b = 0) = (a = (b::'a::ring))"
    74 proof 
    75   have "a = a - b + b" by (simp add: diff_minus ring_add_ac)
    76   also assume "a - b = 0"
    77   finally show "a = b" by simp
    78 next
    79   assume "a = b"
    80   thus "a - b = 0" by (simp add: diff_minus)
    81 qed
    82 
    83 lemma diff_self [simp]: "a - (a::'a::ring) = 0"
    84   by (simp add: diff_minus)
    85 
    86 
    87 subsubsection {* Derived rules for multiplication *}
    88 
    89 lemma right_one [simp]: "a = a * (#1::'a::field)"
    90 proof -
    91   have "a = #1 * a" by simp
    92   also have "... = a * #1" by (simp add: mult_commute)
    93   finally show ?thesis .
    94 qed
    95 
    96 lemma mult_left_commute: "a * (b * c) = b * (a * (c::'a::ring))"
    97 proof -
    98   have "a * (b * c) = (a * b) * c" by (simp only: mult_assoc)
    99   also have "... = (b * a) * c" by (simp only: mult_commute)
   100   finally show ?thesis by (simp only: mult_assoc)
   101 qed
   102 
   103 theorems ring_mult_ac = mult_assoc mult_commute mult_left_commute
   104 
   105 lemma right_inverse [simp]: "a \<noteq> 0 ==>  a * inverse (a::'a::field) = #1" 
   106 proof -
   107   have "a * inverse a = inverse a * a" by (simp add: ring_mult_ac)
   108   also assume "a \<noteq> 0"
   109   hence "inverse a * a = #1" by simp
   110   finally show ?thesis .
   111 qed
   112 
   113 lemma right_inverse_eq: "b \<noteq> 0 ==> (a / b = #1) = (a = (b::'a::field))"
   114 proof 
   115   assume neq: "b \<noteq> 0"
   116   {
   117     hence "a = (a / b) * b" by (simp add: divide_inverse ring_mult_ac)
   118     also assume "a / b = #1"
   119     finally show "a = b" by simp
   120   next
   121     assume "a = b"
   122     with neq show "a / b = #1" by (simp add: divide_inverse)
   123   }
   124 qed
   125 
   126 lemma divide_self [simp]: "a \<noteq> 0 ==> a / (a::'a::field) = #1"
   127   by (simp add: divide_inverse)
   128 
   129 
   130 subsubsection {* Distribution rules *}
   131 
   132 lemma right_distrib: "a * (b + c) = a * b + a * (c::'a::ring)"
   133 proof -
   134   have "a * (b + c) = (b + c) * a" by (simp add: ring_mult_ac)
   135   also have "... = b * a + c * a" by (simp only: left_distrib)
   136   also have "... = a * b + a * c" by (simp add: ring_mult_ac)
   137   finally show ?thesis .
   138 qed
   139 
   140 theorems ring_distrib = right_distrib left_distrib
   141 
   142 end