Re: [isabelle] how to use brackets in lemma



Hi

After pressing enter again, i send again the question in ubuntu's firefox.

failed to parse lemma when prove the following

lemma mfold5 [simp]:"mfold5 f [a,b,c,d,e] x = f e (f d (f c (f b (f a x))))"

lemma mfold [simp]:"mfold f [a,b,c] x = f c (f b (f a x))"
apply(simp_all)
apply(auto)
done

Regards,

Martin
> From: tesleft at hotmail.com
> To: gbuday at karolyrobert.hu; isabelle-users at cl.cam.ac.uk
> Date: Wed, 29 Oct 2014 19:37:44 +0800
> Subject: Re: [isabelle] how to use brackets in lemma
> 
> Hi 
> 
> succeed to add new lines in ubuntu's firefox, i send again the question
> 
> failed to parse lemma when prove the following
> would like to see any further usage when continuing adding letters into it
> lemma mfold5 [simp]:"mfold5 f [a,b,c,d,e] x = f e (f d (f c (f b (f a x))))"
> lemma mfold [simp]:"mfold f [a,b,c] x = f c (f b (f a x))"apply(simp_all)apply(auto)donelemma mfoldr [simp]:"mfoldr f [a,b,c] x = f a (f b (f c x))"apply(induct_tac x)apply(auto)donelemma mfoldl [simp]:"mfoldl f x [a,b,c] = f (f (f x a) b) c"apply(induct_tac x)apply(auto)done
> 
> Regards,
> 
> Martin
> > From: tesleft at hotmail.com
> > To: gbuday at karolyrobert.hu; isabelle-users at cl.cam.ac.uk
> > Date: Wed, 29 Oct 2014 19:35:43 +0800
> > Subject: Re: [isabelle] how to use brackets in lemma
> > 
> > Hi  Buday,
> > 
> > i failed to add new lines in outlook.com in window.
> > now i send it again in firefox in ubuntu.
> > 
> > for example:
> > hello
> > hello
> > 
> > Regards,
> > 
> > Martin
> > 
> > > From: tesleft at hotmail.com
> > > To: gbuday at karolyrobert.hu; isabelle-users at cl.cam.ac.uk
> > > Date: Wed, 29 Oct 2014 19:28:19 +0800
> > > Subject: Re: [isabelle] how to use brackets in lemma
> > > 
> > > Hi
> > > I send with outlook.com. How to add new lines? does it mean like programming add "\r\n" at the end?
> > > for example:
> > > hello\r\nhello\r\n
> > > Regards,
> > > Martin
> > > > From: gbuday at karolyrobert.hu
> > > > To: tesleft at hotmail.com; isabelle-users at cl.cam.ac.uk
> > > > Date: Wed, 29 Oct 2014 08:06:35 +0100
> > > > Subject: RE: [isabelle]   how to use brackets in lemma
> > > > 
> > > > Dear Martin,
> > > > 
> > > > please do not send us an Isabelle theory with no new lines, it is not readable.
> > > > 
> > > > Also it is advisable to send a self-containing, working Isabelle theory with only the necessary parts to exhibit your problem. That is also called a minimal example on the Internet.
> > > > 
> > > > - Gergely
> > > > 
> > > > -----Original Message-----
> > > > From: cl-isabelle-users-bounces at lists.cam.ac.uk [mailto:cl-isabelle-users-bounces at lists.cam.ac.uk] On Behalf Of M A
> > > > Sent: Wednesday, October 29, 2014 5:49 AM
> > > > To: isabelle-users at cl.cam.ac.uk
> > > > Subject: [isabelle] how to use brackets in lemma
> > > > 
> > > > Hi
> > > > failed to parse lemma when prove the following would like to see any further usage when continuing adding letters into it lemma mfold5 [simp]:"mfold5 f [a,b,c,d,e] x = f e (f d (f c (f b (f a x))))"
> > > > lemma mfold [simp]:"mfold f [a,b,c] x = f c (f b (f a x))"apply(simp_all)apply(auto)donelemma mfoldr [simp]:"mfoldr f [a,b,c] x = f a (f b (f c x))"apply(induct_tac x)apply(auto)donelemma mfoldl [simp]:"mfoldl f x [a,b,c] = f (f (f x a) b) c"apply(induct_tac x)apply(auto)done Regards,
> > > > Martin 		 	   		  
> > >  		 	   		  
> >  		 	   		  
>  		 	   		  
 		 	   		  


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