Florian Haftmann wrote: > just do something like (unfold mem_def) and your proof will be a mess > since you have switched to the "wrong world".
Like any definition of a primitive operator, mem_def is not really intended to be unfolded by the user, so don't be surprised if your proof is a mess after unfolding this definition. You wouldn't unfold the definitions of logical operators like "conj" or "disj" either, except for proving introduction- or elimination rules for these operators. > * The logical identification of sets and predicates prevents some > reasonable simp rules on predicates: e.g. you cannot have (A |inf| B) x > = A x & B x > because then expressions like "set xs |inter| set ys" behave strangely > if the are eta-expanded (e.g. due to induction). This sounds more like a problem with the underlying infrastructure that should be fixed, rather than working around the problem by introducing new type constructors. Can you give an example of a proof by induction, where eager eta expansion leads to an unnecessarily complicated proof? Greetings, Stefan _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev