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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev