[isabelle] real^'n in Isabelle2011



On Wed, 30 Mar 2011 21:55:34 Johannes Hölzl wrote:
> Did you try Isabelle2011? Of course the type real ^ 'n was not
> removed, but for most lemmas the constant names changed.

No, I haven't tried it yet.  I keep changing my mind about how 
much work it might require to make my project work with 
Isabelle2011.  Perhaps I should just try it.

> Either you rewrite your terms (which is mostly Search &
> Replace) or you try to stay with the "real ^ 'n" constants and
> use the simplifier to rewrite them at each proof (but I'm not
> sure how well this approach works).
> 
> Alternatively we could try to add the real^'n version of all
> changed lemmas back (by specialising the lemmas about
> euclidean spaces).

I often think my work would have been simpler if Isabelle2011 
existed when I started (in early 2009).  As well as the recent 
introduction of euclidean_space, the quotient types introduced in 
Isabelle2009-2 might have helped if they had existed earlier.  But 
Isabelle is still improving, so I'll just have to be glad that 
these features are available now, for future work.

> When we introduced this changes I were not aware of any
> existing work using Multivariate_Analysis. Hence we did not
> care about backwards compatibility. But we can try to add
> compatibility lemmas so you can port your work to the next
> Isabelle release. Is your work available anywhere? Is it
> possible to take a look at it?

My work is still a work in progress (for a Master's thesis), but 
if you want, I could send you off-list the current files, or 
perhaps I could try to figure out how to give you at least read-
only access to my subversion repository.

> Greetings,
>   Johannes

Thanks for your help.

Tim
<><

Attachment: signature.asc
Description: This is a digitally signed message part.



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