Right, thanks for setting me straight. This is less invasive than I thought.
So the remaining question is, are we happy with replacements like %x. Suc _ + x ~> Suc _ + _ and proper eta contraction. Both would return potentially more matches, but not fewer. For eta contraction, we can argue that Isabelle usually operates on eta-contracted terms anyway, so this behaviour shouldn’t be too surprising. The abstraction expansion would basically mean you can’t search for abstractions at all any more. I.e. even something like (%_. _) would be expanded into (_ _). That’s not necessarily catastrophic, but probably counter-intuitive. Has anyone apart from me ever searched for an abstraction that was not an abbreviation? If yes, why? Cheers, Gerwin > On 27.11.2014, at 18:36, Florian Haftmann > <florian.haftm...@informatik.tu-muenchen.de> wrote: > > Hi Gerwin, > >> Do I read find_eta.txt right that the eta expansion is applied to all > patterns? If yes, then that is a problem, because now partially applied > constants won’t be found any more (i.e. the occurrence of `Suc` in `map > Suc ?xs` would be missed if you make it always search for `Suc _`). > > It is not eta-expansion. It is an expansion of abstractions, e.g. > > %f. inj_on f UNIV ~> inj_on _ UNIV > > but not > > Suc ~/~> Suc _ > >> Also, always eta-contracting the pattern is not necessarily a good idea. >> The user might have specifically used the non-contracted form to exclude >> matches she is not interested in >> (e.g. might specifically not want `map Suc ?xs`). > > It is proper eta-contraction and thus only affecting abstractions. E.g. > > %n. Suc n ~> Suc > > but not > > Suc _ ~/~> Suc > > I played a little bit in my head with the semantic consequences and > judged them quite consistent and convenient. But maybe I have > overlooked significant counterexamples. > > Cheers, > Florian > > -- > > PGP available: > http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de > _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
