Re: [isabelle] Algebraic rule collections



After a third study and conversation with Tobias and Fabian, the
situation presents itself as follows:

a) algebra_simps and field_simps are deliberately designed to provide
some kind of decision procedure based on simp rules and ought stay »as
they are« both in naming and content.

b) Currently, sign_simps is an ad-hoc collection consisting of
algebra_simps plus

lemma zero_less_mult_iff [sign_simps]:
  "0 < a * b ⟷ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0"

lemma mult_less_0_iff [sign_simps]:
  "a * b < 0 ⟷ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b"

c) An intermediate post-release step is to turn sign_simps into a proper
collection consisting solely of

lemma zero_less_mult_iff [sign_simps]:
  "0 < a * b ⟷ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0"

lemma mult_less_0_iff [sign_simps]:
  "a * b < 0 ⟷ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b"

and also

lemma zero_le_mult_iff [sign_simps]:
  "0 ≤ a * b ⟷ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0"

lemma mult_le_0_iff [sign_simps]:
  "a * b ≤ 0 ⟷ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b"

d) The specific property of sign_simps and divide_simps is that goals
may be split.  Maybe this can be developed into a schema where each
algebra_simps and field_simps are accompanied by splitting variants,
making sign_simps and divide_simp.  This needs to be discussed.

Cheers,
	Florian

Attachment: signature.asc
Description: OpenPGP digital signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.