src/HOL/Fields.thy
changeset 70344 050104f01bf9
parent 70343 e54caaa38ad9
child 70356 4a327c061870
equal deleted inserted replaced
70343:e54caaa38ad9 70344:050104f01bf9
   898 
   898 
   899 lemma frac_le_eq:
   899 lemma frac_le_eq:
   900   "y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> x / y \<le> w / z \<longleftrightarrow> (x * z - w * y) / (y * z) \<le> 0"
   900   "y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> x / y \<le> w / z \<longleftrightarrow> (x * z - w * y) / (y * z) \<le> 0"
   901   by (subst le_iff_diff_le_0) (simp add: diff_frac_eq )
   901   by (subst le_iff_diff_le_0) (simp add: diff_frac_eq )
   902 
   902 
   903 text\<open>Lemmas \<open>sign_simps\<close> is a first attempt to automate proofs
       
   904 of positivity/negativity needed for \<open>field_simps\<close>. Have not added \<open>sign_simps\<close> to \<open>field_simps\<close> because the former can lead to case
       
   905 explosions.\<close>
       
   906 
       
   907 lemma divide_pos_pos[simp]:
   903 lemma divide_pos_pos[simp]:
   908   "0 < x ==> 0 < y ==> 0 < x / y"
   904   "0 < x ==> 0 < y ==> 0 < x / y"
   909 by(simp add:field_simps)
   905 by(simp add:field_simps)
   910 
   906 
   911 lemma divide_nonneg_pos:
   907 lemma divide_nonneg_pos: