Re: [isabelle] problem with opening proof



On Fri, 22 May 2009, Chris Capel wrote:

"proof" is short for "proof default", where the "default" method performs:

In the Isar documentation it says "Unless given explicitly by the
user, the default initial method is “rule”". Is this inaccurate?

The manual is indeed less accurate than the true source text. Conceptually, 'proof' without argument performs a "default" step, but the method of that name is essentially dynamically rebound by some later stages (2 times in Isabelle/HOL).

The main idea of a default step is represented by the Pure "rule" method; the later additions for type classes and classical reasoning can be ignored for now.


I suppose if the mode is not proof(chain) then default is the same as rule? And otherwise it's the same as erule?

No, method "rule" is always just that. Any proper Isar method is sensitive to the facts being chained. Thus chaining + rule acts like an elimination, and no chaining + rule like a plain introduction.

The variants "erule" etc. are from a slightly different (tactical) layer, which are never required in properly structured Isar proofs.


But why does it also fail for "proof (rule exI)"? What's the difference between rule and intro that allows the latter to succeed?

The "intro" method repeatedly unfolds introduction rules. As a weakly structured tool, it merely inserts facts into the goal initially, without taking them a seriously as "rule". This is analogous to "simp", "auto" etc.

You should be able to ignore the "intro" and "elim" methods most of the time -- they stem from a very early stage of Isar when structured proofs were not fully understood yet.


	Makarius


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.