src/HOL/Fields.thy
changeset 58776 95e58e04e534
parent 58512 dc4d76dfa8f0
child 58826 2ed2eaabe3df
     1.1 --- a/src/HOL/Fields.thy	Fri Oct 24 15:07:49 2014 +0200
     1.2 +++ b/src/HOL/Fields.thy	Fri Oct 24 15:07:51 2014 +0200
     1.3 @@ -23,11 +23,37 @@
     1.4    fixes inverse :: "'a \<Rightarrow> 'a"
     1.5      and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "'/" 70)
     1.6  
     1.7 +setup {* Sign.add_const_constraint
     1.8 +  (@{const_name "divide"}, SOME @{typ "'a \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
     1.9 +
    1.10 +
    1.11 +context semiring
    1.12 +begin
    1.13 +
    1.14 +lemma [field_simps]:
    1.15 +  shows distrib_left_NO_MATCH: "NO_MATCH a (x / y) \<Longrightarrow> a * (b + c) = a * b + a * c"
    1.16 +    and distrib_right_NO_MATCH: "NO_MATCH c (x / y) \<Longrightarrow> (a + b) * c = a * c + b * c"
    1.17 +  by (rule distrib_left distrib_right)+
    1.18 +
    1.19 +end
    1.20 +
    1.21 +context ring
    1.22 +begin
    1.23 +
    1.24 +lemma [field_simps]:
    1.25 +  shows left_diff_distrib_NO_MATCH: "NO_MATCH c (x / y) \<Longrightarrow> (a - b) * c = a * c - b * c"
    1.26 +    and right_diff_distrib_NO_MATCH: "NO_MATCH a (x / y) \<Longrightarrow> a * (b - c) = a * b - a * c"
    1.27 +  by (rule left_diff_distrib right_diff_distrib)+
    1.28 +
    1.29 +end
    1.30 +
    1.31 +setup {* Sign.add_const_constraint
    1.32 +  (@{const_name "divide"}, SOME @{typ "'a::inverse \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
    1.33 +
    1.34  text{* Lemmas @{text divide_simps} move division to the outside and eliminates them on (in)equalities. *}
    1.35  
    1.36  named_theorems divide_simps "rewrite rules to eliminate divisions"
    1.37  
    1.38 -
    1.39  class division_ring = ring_1 + inverse +
    1.40    assumes left_inverse [simp]:  "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
    1.41    assumes right_inverse [simp]: "a \<noteq> 0 \<Longrightarrow> a * inverse a = 1"