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

[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 important role in many proofs. Using pure natural deduction for 
this, yields much less readable proofs, and I even believe more fragile, 
since as soon as you change the definition a little bit, you need a 
different natural deduction rule.

Quite often you have simple definitions, but many of them. I don't think 
you want the user to tackle all these just by intro/elim. That's not 
practical at all.

Amine.

Florian Haftmann wrote:
> Tobias Nipkow wrote:
>>> 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 their definitions. If this is considered
>> "archaic", we should force all Isabelle users to take vows to serve the
>> church of natural deduction and renounce all other means of proof as
>> heresy.
> 
> Ignore the moody "archaic" but not the "fragile".  IMHO the problem
> enters the stage iff such unfold series occur in larger apply scripts
> because then these become more cluttered due to the need of breaking
> down the object logic level connectives (stemming from the unfolded
> definitions) to the meta logic connectives.
> 
> 	Florian
> 
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev