division ring assumes divide_inverse
authorhaftmann
Wed Feb 10 08:49:26 2010 +0100 (2010-02-10)
changeset 350833246e66b0874
parent 35082 96a21dd3b349
child 35084 e25eedfc15ce
division ring assumes divide_inverse
src/HOL/NSA/StarDef.thy
src/HOL/Rings.thy
     1.1 --- a/src/HOL/NSA/StarDef.thy	Wed Feb 10 08:49:25 2010 +0100
     1.2 +++ b/src/HOL/NSA/StarDef.thy	Wed Feb 10 08:49:26 2010 +0100
     1.3 @@ -893,6 +893,7 @@
     1.4  apply (intro_classes)
     1.5  apply (transfer, erule left_inverse)
     1.6  apply (transfer, erule right_inverse)
     1.7 +apply (transfer, fact divide_inverse)
     1.8  done
     1.9  
    1.10  instance star :: (field) field
     2.1 --- a/src/HOL/Rings.thy	Wed Feb 10 08:49:25 2010 +0100
     2.2 +++ b/src/HOL/Rings.thy	Wed Feb 10 08:49:26 2010 +0100
     2.3 @@ -410,9 +410,14 @@
     2.4  
     2.5  end
     2.6  
     2.7 +class inverse =
     2.8 +  fixes inverse :: "'a \<Rightarrow> 'a"
     2.9 +    and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "'/" 70)
    2.10 +
    2.11  class division_ring = ring_1 + inverse +
    2.12    assumes left_inverse [simp]:  "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
    2.13    assumes right_inverse [simp]: "a \<noteq> 0 \<Longrightarrow> a * inverse a = 1"
    2.14 +  assumes divide_inverse: "a / b = a * inverse b"
    2.15  begin
    2.16  
    2.17  subclass ring_1_no_zero_divisors