Hi Andreas, see now http://isabelle.in.tum.de/reports/Isabelle/rev/8fcbfce2a2a9
for a uniform approach.
Hope this fits,
Florian
On 11.06.2014 09:22, Andreas Lochbihler wrote:
> Hi Florian,
>
> the simproc unit_eq in
>
> http://isabelle.in.tum.de/repos/isabelle/file/697e0fad9337/src/HOL/Product_Type.thy#l78
>
>
> rewrites anything of type unit to (), so there's no need to declare the
> definitions introduced in 697e0fad9337 as [simp]. One could declare
> sup_unit_def, inf_unit_def, Sup_unit_def, and Inf_unit_def as [abs_def,
> simp] such that they get unfolded even if they are applied only
> partially, but I don't know whether that is a good thing to have.
> (Admittedly, the definition of uminus has this [simp] declaration, so
> it's a bit unconsistent at the moment).
>
> Andreas
>
> On 10/06/14 23:02, Florian Haftmann wrote:
>> Hi Andreas,
>>
>> I'm wondering whether there is a deliberate reason to declare top, bot
>> etc. on unit not as simp by default. Since there is only one element of
>> unit, proof goals after simp should be trivial…
>>
>> Florian
>>
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
