[isabelle-dev] sign_simps

[Florian Haftmann]

In c3ca292c1484 src/HOL/Fields.thy, there is a pseudo fact-collection
sign_simps with a comment (from about 2007):

> Lemmas @{text sign_simps} is a first attempt to automate proofs
> of positivity/negativity needed for @{text field_simps}. Have not added @{text
> sign_simps} to @{text field_simps} because the former can lead to case
> explosions.

It is used but not that prominently:

> $ grep -rIPn sign_simps src/HOL ../../afp/devel/thys/
> src/HOL/Multivariate_Analysis/Derivative.thy:686:      linordered_field_class.sign_simps(41) nonzero_mult_divide_cancel_right not_real_square_gt_zero
> src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy:466:    unfolding entropy_chain_rule[symmetric, OF simple_function_finite simple_function_finite] sign_simps
> src/HOL/Fields.thy:816: prefer 2 apply(simp add:sign_simps)
> src/HOL/Fields.thy:818: prefer 2 apply(simp add:sign_simps)
> src/HOL/Decision_Procs/Approximation.thy:244:    hence "0 < m" using assms powr_gt_zero[of 2 e] by (auto simp: sign_simps)
> ../../afp/devel/thys/Affine_Arithmetic/Counterclockwise_2D_Arbitrary.thy:36:  by (auto simp: psi_def lex_def det3_def' not_less sign_simps)
> ../../afp/devel/thys/Affine_Arithmetic/Counterclockwise_2D_Arbitrary.thy:79:  by (auto simp: lex_def prod_eq_iff less_eq_prod_def sign_simps)
> ../../afp/devel/thys/Affine_Arithmetic/Counterclockwise_2D_Arbitrary.thy:229:  by (auto simp: ccw'_def det3_def' lex_def sign_simps)
> ../../afp/devel/thys/Affine_Arithmetic/Counterclockwise_2D_Arbitrary.thy:500:      by (auto simp: lex_def not_less sign_simps y ccw'_def)
> ../../afp/devel/thys/pGCL/Healthiness.thy:114:    from uP have "0 \<le> 1 - P s" by(auto simp:sign_simps)
> ../../afp/devel/thys/pGCL/Healthiness.thy:127:    have "wp g Q s \<le> b" and "0 \<le> 1 - P s" by(auto simp:sign_simps)
> ../../afp/devel/thys/pGCL/Healthiness.thy:147:    moreover from uP have "0 \<le> 1 - P s" by(auto simp:sign_simps)
> ../../afp/devel/thys/pGCL/Healthiness.thy:179:  from uP have nnP: "0 \<le> P s" "0 \<le> 1 - P s" by(auto simp:sign_simps)
> ../../afp/devel/thys/pGCL/Continuity.thy:301:      from up show "0 \<le> 1 - p s" by(auto simp:sign_simps)
> ../../afp/devel/thys/pGCL/Continuity.thy:360:    moreover from up have "0 \<le> (1 - p s)" by(auto simp:sign_simps)
> ../../afp/devel/thys/pGCL/Continuity.thy:374:      moreover from up have "0 \<le> 1 - p s" by(auto simp:sign_simps)
> ../../afp/devel/thys/pGCL/Continuity.thy:440:    moreover from up have "0 \<le> p s" "0 \<le> 1 - p s" by(auto simp:sign_simps)
> ../../afp/devel/thys/pGCL/Continuity.thy:451:    moreover from up have "\<And>s. 0 \<le> p s" "\<And>s. 0 \<le> 1 - p s" by(auto simp:sign_simps)
> ../../afp/devel/thys/pGCL/Continuity.thy:698:          from up have "0 \<le> p y" "0 \<le> 1 - p x" by(auto simp:sign_simps)
> ../../afp/devel/thys/pGCL/Algebra.thy:361:    hence "\<And>s. 0 \<le> ?Pc s" by(auto simp:sign_simps)
> ../../afp/devel/thys/pGCL/Sublinearity.thy:98:        by(auto simp:sign_simps)
> ../../afp/devel/thys/pGCL/Sublinearity.thy:117:      by(auto simp:sign_simps)
> ../../afp/devel/thys/pGCL/WellDefined.thy:335:    using uP by(auto simp:sign_simps)
> ../../afp/devel/thys/LinearQuantifierElim/Thys/FRE.thy:174:      from * have [simp]: "c * (c * (d * (d * 4))) > 0" by (auto simp add: sign_simps)

I see two possibilities:
* Discontinue sign_simps as an comparingly unfruitful attempt.
* Turn sign_simps in a proper fact collection like algebra_simps and
field_simps.  Maybe there are other candidates of splitting rewrite rules?

Any suggestions on that topic?

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 181 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20150214/fb0953ee/attachment-0001.asc>