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"
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and