Stream: General

Topic: simproc for boolean algebra broken?

irvin (Mar 30 2025 at 06:21):

I may be wrong but it appears that the simproc for boolean_algebra are broken.
Small example

lemma "(A ⊔ B) ⊔ A = A ⊔ (B :: 'a :: boolean_algebra)"
  apply simp (*fails*)
oops

irvin (Mar 30 2025 at 12:01):

Nevermind it appears that the simpproc only deals with
cancelling out negations.
lemma "(A ⊔ B) ⊔ - A = (B :: 'a :: boolean_algebra)"
supply [[simp_trace]]
apply (simp ) (*simplifies to ⊤ = B *)

Last updated: Apr 03 2025 at 20:22 UTC