Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] HOL/Set.thy lemma suggestion

view this post on Zulip Email Gateway (Aug 22 2022 at 17:44):

From: Jørgen Villadsen <jovi@dtu.dk>
Hi,

Could the following useful result from the AFP FOL-Fitting entry be added to Isabelle?

lemma set_inter_compl_diff: <- A ∩ B = B - A> unfolding Diff_eq using Int_commute .

If so should it be a simp rule?

Best regards, Jørgen

view this post on Zulip Email Gateway (Aug 22 2022 at 17:45):

From: Lawrence Paulson <lp15@cam.ac.uk>
It’s not obvious to me why this rewrite should be done by default. The RHS is not clearly simpler than the LHS.

Larry Paulson

Last updated: Nov 21 2024 at 12:39 UTC