[isabelle-dev] Some experiences with MicroJava, Jinja, JinjaThreads

2008-07-28 Thread Gerwin Klein
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

[isabelle-dev] Some experiences with MicroJava, Jinja, JinjaThreads

2008-07-28 Thread Florian Haftmann
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

[isabelle-dev] Some experiences with MicroJava, Jinja, JinjaThreads

2008-07-28 Thread Amine Chaieb
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

[isabelle-dev] Some experiences with MicroJava, Jinja, JinjaThreads

2008-07-28 Thread Florian Haftmann
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

[isabelle-dev] Some experiences with MicroJava, Jinja, JinjaThreads

2008-07-28 Thread Tobias Nipkow
> 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

[isabelle-dev] Some experiences with MicroJava, Jinja, JinjaThreads

2008-07-28 Thread Florian Haftmann
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