[isabelle-dev] lists_Int_eq

[Stefan Berghofer]

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)

  http://isabelle.in.tum.de/dist/Isabelle2011-1/doc/tutorial.pdf

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

  http://isabelle.in.tum.de/repos/isabelle/rev/7f9e05b3d0fb

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?

Greetings,
Stefan