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

lemma
   assumes
     a1: "A" and
     a2: "B"
   shows
     "A & B"
   using a1 a2 ..

lemma
   assumes
     a1: "A" and
     a2: "B"
   shows
     "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"
   -- proof
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 MHonArc.