made field_simps "more complete"
authornipkow
Sun Apr 06 17:18:57 2014 +0200 (2014-04-06)
changeset 5644149e95c9ebb59
parent 56432 96b54a96b117
child 56442 681717041f55
made field_simps "more complete"
src/HOL/Fields.thy
     1.1 --- a/src/HOL/Fields.thy	Sat Apr 05 23:56:21 2014 +0200
     1.2 +++ b/src/HOL/Fields.thy	Sun Apr 06 17:18:57 2014 +0200
     1.3 @@ -174,6 +174,14 @@
     1.4    finally show ?thesis .
     1.5  qed
     1.6  
     1.7 +lemma nonzero_neg_divide_eq_eq[field_simps]:
     1.8 +  "b \<noteq> 0 \<Longrightarrow> -(a/b) = c \<longleftrightarrow> -a = c*b"
     1.9 +using nonzero_divide_eq_eq[of b "-a" c] by (simp add: divide_minus_left)
    1.10 +
    1.11 +lemma nonzero_neg_divide_eq_eq2[field_simps]:
    1.12 +  "b \<noteq> 0 \<Longrightarrow> c = -(a/b) \<longleftrightarrow> c*b = -a"
    1.13 +using nonzero_neg_divide_eq_eq[of b a c] by auto
    1.14 +
    1.15  lemma divide_eq_imp: "c \<noteq> 0 \<Longrightarrow> b = a * c \<Longrightarrow> b / c = a"
    1.16    by (simp add: divide_inverse mult_assoc)
    1.17