Florian Haftmann wrote:
> A) Archaic, hardly readable and fragile proof techniques:
> * unfolding definitions of predicates over logical formulae instead of
> proper intro/elim-rules
There was some discussion on this already, and I'd agree with Tobias and Amine
that it's just a matter of ta
mples.
Florian
-- next part --
A non-text attachment was scrubbed...
Name: florian.haftmann.vcf
Type: text/x-vcard
Size: 654 bytes
Desc: not available
Url :
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20080728/49235e69/attachment.vc
I don't see why this argument yields an "iff" proof of your conjecture.
Many definitions have to be made in object logic and unfolding them is
often exactly what you need to prove the goal. I have also experienced
that often "folding", i.e. unfolding the symmetric of the definition)
plays an im
ions) to the meta logic connectives.
Florian
-- next part --
A non-text attachment was scrubbed...
Name: florian.haftmann.vcf
Type: text/x-vcard
Size: 654 bytes
Desc: not available
Url :
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/2008072
> The three obfuscating issues were:
>
> A) Archaic, hardly readable and fragile proof techniques:
> * unfolding definitions of predicates over logical formulae instead of
> proper intro/elim-rules
This is mere dogma. It is perfectly standard to reason about logical
concepts by unfolding t
rmail/isabelle-dev/attachments/20080728/c6c73631/attachment.vcf
-- next part --
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 185 bytes
Desc: OpenPGP digital signature
Url :
https://mailmanbroy.informatik.tu-muenchen.de/pipe
