Re: [isabelle] problem with opening proof
On 23/05/2009, at 7:13 PM, Makarius wrote:
> 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.
Is there any source I can access that describes this full
understanding of structured proofs?
Generally, I see the structured proof game as coaxing the proof engine
into returning the particular proof state that I feel best explains
the truth of my proposition to the human reader. To this end, I find
intro and elim necessary quite often, when the default reasoning set
returns a proof state that is incomprehensible to a human reader.
Since it is very hard to massage the default set into a manageable
shape it is easiest to use a number of intro, elim and simp methods to
get the desired proof state. Obviously, it is suboptimal to have long
convoluted chains of methods that result in the "obvious" goal state,
since this will tend to make the reader uneasy about the "formal
nonsense" that is meant to be reassuring them about the quality of the
proof being offered. However, it is certainly better than having a
short chain of methods that result it an unintuitive or
incomprehensible or even unexpectedly non-existent proof state.
I still must say, that I can't follow the reasoning behind the way
default/rule is implemented. My confusion is well described by the
following examples, the first of which is a valid proof
a1: "A" and
"A & B"
using a1 a2 ..
a1: "A" and
"A & B"
using a2 a1 ..
and the second of which is not.
This can be seriously annoying when trying to chain facts
assume b1: "B"
have b2: "A"
with b1 show "A & B" ..
IMPORTANT: This email remains the property of the Australian Defence Organisation and is subject to the jurisdiction of section 70 of the CRIMES ACT 1914. If you have received this email in error, you are requested to contact the sender and delete the email.
This archive was generated by a fusion of
Pipermail (Mailman edition) and