src/HOL/Groups.thy
changeset 70347 e5cd5471c18a
parent 69605 a96320074298
     1.1 --- a/src/HOL/Groups.thy	Fri Jun 14 08:34:28 2019 +0000
     1.2 +++ b/src/HOL/Groups.thy	Fri Jun 14 08:34:28 2019 +0000
     1.3 @@ -15,8 +15,9 @@
     1.4  subsection \<open>Dynamic facts\<close>
     1.5  
     1.6  named_theorems ac_simps "associativity and commutativity simplification rules"
     1.7 -  and algebra_simps "algebra simplification rules"
     1.8 +  and algebra_simps "algebra simplification rules for rings"
     1.9    and field_simps "algebra simplification rules for fields"
    1.10 +  and sign_simps "algebra simplification rules for comparision with zero"
    1.11  
    1.12  text \<open>
    1.13    The rewrites accumulated in \<open>algebra_simps\<close> deal with the classical
    1.14 @@ -32,6 +33,10 @@
    1.15    can be proved to be non-zero (for equations) or positive/negative (for
    1.16    inequalities). Can be too aggressive and is therefore separate from the more
    1.17    benign \<open>algebra_simps\<close>.
    1.18 +
    1.19 +  Lemmas \<open>sign_simps\<close> is a first attempt to automate proofs
    1.20 +  of positivity/negativity needed for \<open>field_simps\<close>. Have not added \<open>sign_simps\<close> to \<open>field_simps\<close>
    1.21 +  because the former can lead to case explosions.
    1.22  \<close>
    1.23  
    1.24