[isabelle-dev] lists_Int_eq

Stefan Berghofer berghofe at in.tum.de
Wed Jan 11 21:46:16 CET 2012

Makarius wrote:
> Its name indicates set operations, but it is now more general:
>   listsp (inf (%x. x : ?A) (%x. x : ?B)) =
>   inf (%x. x : lists ?A) (%x. x : lists ?B)
> The recent change 1898e61e89c4 (berghofe) might be related.  Stefan
> should know what he had in mind.

If you look at the version of the tutorial available on the Isabelle
web page (p. 141)


you will see that it has already been broken for some time, the only
difference being that set union is now printed as "inf", due to the
recent re-introduction of the set type.

When converting the rule listsp_inf_eq to set notation using inf_Int_eq,
the resulting rule has the expected form:

  thm listsp_inf_eq [to_set inf_Int_eq]

They were removed from the pred_set_conv database a while ago by Florian


because they were considered "potentially dangerous", but now that sets
and predicates can be distinguished again, this rule (and the dual rule
sup_Un_eq) could be added again?


More information about the isabelle-dev mailing list