add divide_simps
authorhoelzl
Wed Apr 09 09:37:49 2014 +0200 (2014-04-09)
changeset 5648147500d0881f9
parent 56480 093ea91498e6
child 56482 39ac12b655ab
child 56489 884e8f37492c
add divide_simps
src/HOL/Fields.thy
src/HOL/Power.thy
     1.1 --- a/src/HOL/Fields.thy	Wed Apr 09 09:37:48 2014 +0200
     1.2 +++ b/src/HOL/Fields.thy	Wed Apr 09 09:37:49 2014 +0200
     1.3 @@ -23,6 +23,19 @@
     1.4    fixes inverse :: "'a \<Rightarrow> 'a"
     1.5      and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "'/" 70)
     1.6  
     1.7 +text{* Lemmas @{text divide_simps} move division to the outside and eliminates them on (in)equalities. *}
     1.8 +
     1.9 +ML {*
    1.10 +structure Divide_Simps = Named_Thms
    1.11 +(
    1.12 +  val name = @{binding divide_simps}
    1.13 +  val description = "rewrite rules to eliminate divisions"
    1.14 +)
    1.15 +*}
    1.16 +
    1.17 +setup Divide_Simps.setup
    1.18 +
    1.19 +
    1.20  class division_ring = ring_1 + inverse +
    1.21    assumes left_inverse [simp]:  "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
    1.22    assumes right_inverse [simp]: "a \<noteq> 0 \<Longrightarrow> a * inverse a = 1"
    1.23 @@ -131,7 +144,7 @@
    1.24  lemma divide_zero_left [simp]: "0 / a = 0"
    1.25  by (simp add: divide_inverse)
    1.26  
    1.27 -lemma inverse_eq_divide [field_simps]: "inverse a = 1 / a"
    1.28 +lemma inverse_eq_divide [field_simps, divide_simps]: "inverse a = 1 / a"
    1.29  by (simp add: divide_inverse)
    1.30  
    1.31  lemma add_divide_distrib: "(a+b) / c = a/c + b/c"
    1.32 @@ -254,6 +267,23 @@
    1.33    "inverse a = inverse b \<longleftrightarrow> a = b"
    1.34    by (force dest!: inverse_eq_imp_eq)
    1.35  
    1.36 +lemma add_divide_eq_if_simps [divide_simps]:
    1.37 +    "a + b / z = (if z = 0 then a else (a * z + b) / z)"
    1.38 +    "a / z + b = (if z = 0 then b else (a + b * z) / z)"
    1.39 +    "- (a / z) + b = (if z = 0 then b else (-a + b * z) / z)"
    1.40 +    "a - b / z = (if z = 0 then a else (a * z - b) / z)"
    1.41 +    "a / z - b = (if z = 0 then -b else (a - b * z) / z)"
    1.42 +    "- (a / z) - b = (if z = 0 then -b else (- a - b * z) / z)"
    1.43 +  by (simp_all add: add_divide_eq_iff divide_add_eq_iff diff_divide_eq_iff divide_diff_eq_iff
    1.44 +      minus_divide_diff_eq_iff)
    1.45 +
    1.46 +lemma [divide_simps]:
    1.47 +  shows divide_eq_eq: "b / c = a \<longleftrightarrow> (if c \<noteq> 0 then b = a * c else a = 0)"
    1.48 +    and eq_divide_eq: "a = b / c \<longleftrightarrow> (if c \<noteq> 0 then a * c = b else a = 0)"
    1.49 +    and minus_divide_eq_eq: "- (b / c) = a \<longleftrightarrow> (if c \<noteq> 0 then - b = a * c else a = 0)"
    1.50 +    and eq_minus_divide_eq: "a = - (b / c) \<longleftrightarrow> (if c \<noteq> 0 then a * c = - b else a = 0)"
    1.51 +  by (auto simp add:  field_simps)
    1.52 +
    1.53  end
    1.54  
    1.55  subsection {* Fields *}
    1.56 @@ -432,14 +462,6 @@
    1.57  apply (simp add: nonzero_minus_divide_divide) 
    1.58  done
    1.59  
    1.60 -lemma eq_divide_eq:
    1.61 -  "a = b / c \<longleftrightarrow> (if c \<noteq> 0 then a * c = b else a = 0)"
    1.62 -  by (simp add: nonzero_eq_divide_eq)
    1.63 -
    1.64 -lemma divide_eq_eq:
    1.65 -  "b / c = a \<longleftrightarrow> (if c \<noteq> 0 then b = a * c else a = 0)"
    1.66 -  by (force simp add: nonzero_divide_eq_eq)
    1.67 -
    1.68  lemma inverse_eq_1_iff [simp]:
    1.69    "inverse x = 1 \<longleftrightarrow> x = 1"
    1.70    by (insert inverse_eq_iff_eq [of x 1], simp) 
    1.71 @@ -966,11 +988,15 @@
    1.72  lemma inverse_le_1_iff: "inverse x \<le> 1 \<longleftrightarrow> x \<le> 0 \<or> 1 \<le> x"
    1.73    by (simp add: not_less [symmetric] one_less_inverse_iff) 
    1.74  
    1.75 -lemma 
    1.76 +lemma [divide_simps]:
    1.77    shows le_divide_eq: "a \<le> b / c \<longleftrightarrow> (if 0 < c then a * c \<le> b else if c < 0 then b \<le> a * c else a \<le> 0)"
    1.78      and divide_le_eq: "b / c \<le> a \<longleftrightarrow> (if 0 < c then b \<le> a * c else if c < 0 then a * c \<le> b else 0 \<le> a)"
    1.79      and less_divide_eq: "a < b / c \<longleftrightarrow> (if 0 < c then a * c < b else if c < 0 then b < a * c else a < 0)"
    1.80      and divide_less_eq: "b / c < a \<longleftrightarrow> (if 0 < c then b < a * c else if c < 0 then a * c < b else 0 < a)"
    1.81 +    and le_minus_divide_eq: "a \<le> - (b / c) \<longleftrightarrow> (if 0 < c then a * c \<le> - b else if c < 0 then - b \<le> a * c else a \<le> 0)"
    1.82 +    and minus_divide_le_eq: "- (b / c) \<le> a \<longleftrightarrow> (if 0 < c then - b \<le> a * c else if c < 0 then a * c \<le> - b else 0 \<le> a)"
    1.83 +    and less_minus_divide_eq: "a < - (b / c) \<longleftrightarrow> (if 0 < c then a * c < - b else if c < 0 then - b < a * c else  a < 0)"
    1.84 +    and minus_divide_less_eq: "- (b / c) < a \<longleftrightarrow> (if 0 < c then - b < a * c else if c < 0 then a * c < - b else 0 < a)"
    1.85    by (auto simp: field_simps not_less dest: antisym)
    1.86  
    1.87  text {*Division and Signs*}
    1.88 @@ -980,7 +1006,7 @@
    1.89      and divide_less_0_iff: "a / b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b"
    1.90      and zero_le_divide_iff: "0 \<le> a / b \<longleftrightarrow> 0 \<le> a \<and> 0 \<le> b \<or> a \<le> 0 \<and> b \<le> 0"
    1.91      and divide_le_0_iff: "a / b \<le> 0 \<longleftrightarrow> 0 \<le> a \<and> b \<le> 0 \<or> a \<le> 0 \<and> 0 \<le> b"
    1.92 -  by (simp_all add: divide_inverse zero_less_mult_iff mult_less_0_iff zero_le_mult_iff mult_le_0_iff)
    1.93 +  by (auto simp add: divide_simps)
    1.94  
    1.95  text {* Division and the Number One *}
    1.96  
     2.1 --- a/src/HOL/Power.thy	Wed Apr 09 09:37:48 2014 +0200
     2.2 +++ b/src/HOL/Power.thy	Wed Apr 09 09:37:49 2014 +0200
     2.3 @@ -661,7 +661,7 @@
     2.4    "1 / (a::'a::{field_inverse_zero, power}) ^ n =  (1 / a) ^ n"
     2.5    by (simp add: divide_inverse) (rule power_inverse)
     2.6  
     2.7 -lemma power_divide [field_simps]:
     2.8 +lemma power_divide [field_simps, divide_simps]:
     2.9    "(a / b) ^ n = (a::'a::field_inverse_zero) ^ n / b ^ n"
    2.10  apply (cases "b = 0")
    2.11  apply (simp add: power_0_left)