equal
deleted
inserted
replaced
841 |
841 |
842 text\<open>Lemmas \<open>sign_simps\<close> is a first attempt to automate proofs |
842 text\<open>Lemmas \<open>sign_simps\<close> is a first attempt to automate proofs |
843 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 |
843 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 |
844 explosions.\<close> |
844 explosions.\<close> |
845 |
845 |
846 lemmas sign_simps = algebra_simps zero_less_mult_iff mult_less_0_iff |
|
847 |
|
848 lemmas (in -) sign_simps = algebra_simps zero_less_mult_iff mult_less_0_iff |
|
849 |
|
850 (* Only works once linear arithmetic is installed: |
846 (* Only works once linear arithmetic is installed: |
851 text{*An example:*} |
847 text{*An example:*} |
852 lemma fixes a b c d e f :: "'a::linordered_field" |
848 lemma fixes a b c d e f :: "'a::linordered_field" |
853 shows "\<lbrakk>a>b; c<d; e<f; 0 < u \<rbrakk> \<Longrightarrow> |
849 shows "\<lbrakk>a>b; c<d; e<f; 0 < u \<rbrakk> \<Longrightarrow> |
854 ((a-b)*(c-d)*(e-f))/((c-d)*(e-f)*(a-b)) < |
850 ((a-b)*(c-d)*(e-f))/((c-d)*(e-f)*(a-b)) < |