src/HOL/Rat.thy
changeset 57514 bdc2c6b40bf2
parent 57512 cc97b347b301
child 57576 083dfad2727c
     1.1 --- a/src/HOL/Rat.thy	Sat Jul 05 10:09:01 2014 +0200
     1.2 +++ b/src/HOL/Rat.thy	Sat Jul 05 11:01:53 2014 +0200
     1.3 @@ -118,7 +118,7 @@
     1.4  
     1.5  lift_definition plus_rat :: "rat \<Rightarrow> rat \<Rightarrow> rat"
     1.6    is "\<lambda>x y. (fst x * snd y + fst y * snd x, snd x * snd y)"
     1.7 -  by (clarsimp, simp add: distrib_right, simp add: mult_ac)
     1.8 +  by (clarsimp, simp add: distrib_right, simp add: ac_simps)
     1.9  
    1.10  lemma add_rat [simp]:
    1.11    assumes "b \<noteq> 0" and "d \<noteq> 0"
    1.12 @@ -144,7 +144,7 @@
    1.13  
    1.14  lift_definition times_rat :: "rat \<Rightarrow> rat \<Rightarrow> rat"
    1.15    is "\<lambda>x y. (fst x * fst y, snd x * snd y)"
    1.16 -  by (simp add: mult_ac)
    1.17 +  by (simp add: ac_simps)
    1.18  
    1.19  lemma mult_rat [simp]: "Fract a b * Fract c d = Fract (a * c) (b * d)"
    1.20    by transfer simp
    1.21 @@ -271,7 +271,7 @@
    1.22    proof -
    1.23      assume "p * gcd r s = sgn (q * s) * r * gcd p q" and "q * gcd r s = sgn (q * s) * s * gcd p q"
    1.24      then have "(p * gcd r s) * (sgn (q * s) * s * gcd p q) = (q * gcd r s) * (sgn (q * s) * r * gcd p q)" by simp
    1.25 -    with assms show "p * s = q * r" by (auto simp add: mult_ac sgn_times sgn_0_0)
    1.26 +    with assms show "p * s = q * r" by (auto simp add: ac_simps sgn_times sgn_0_0)
    1.27    qed
    1.28    from assms show ?thesis
    1.29      by (auto simp add: normalize_def Let_def dvd_div_div_eq_mult mult.commute sgn_times split: if_splits intro: aux)
    1.30 @@ -413,7 +413,7 @@
    1.31    hence "a * d * b * d = c * b * b * d"
    1.32      by simp
    1.33    hence "a * b * d\<^sup>2 = c * d * b\<^sup>2"
    1.34 -    unfolding power2_eq_square by (simp add: mult_ac)
    1.35 +    unfolding power2_eq_square by (simp add: ac_simps)
    1.36    hence "0 < a * b * d\<^sup>2 \<longleftrightarrow> 0 < c * d * b\<^sup>2"
    1.37      by simp
    1.38    thus "0 < a * b \<longleftrightarrow> 0 < c * d"
    1.39 @@ -434,7 +434,7 @@
    1.40  
    1.41  lemma positive_mult:
    1.42    "positive x \<Longrightarrow> positive y \<Longrightarrow> positive (x * y)"
    1.43 -by transfer (drule (1) mult_pos_pos, simp add: mult_ac)
    1.44 +by transfer (drule (1) mult_pos_pos, simp add: ac_simps)
    1.45  
    1.46  lemma positive_minus:
    1.47    "\<not> positive x \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> positive (- x)"
    1.48 @@ -676,7 +676,7 @@
    1.49  
    1.50  lemma of_rat_mult: "of_rat (a * b) = of_rat a * of_rat b"
    1.51  apply transfer
    1.52 -apply (simp add: divide_inverse nonzero_inverse_mult_distrib mult_ac)
    1.53 +apply (simp add: divide_inverse nonzero_inverse_mult_distrib ac_simps)
    1.54  done
    1.55  
    1.56  lemma nonzero_of_rat_inverse: