*To*: Timothy McKenzie <tjm1983 at gmail.com>*Subject*: Re: [isabelle] Proving two real^3 spaces are the same*From*: Johannes Hölzl <hoelzl at in.tum.de>*Date*: Wed, 30 Mar 2011 10:55:34 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <201103301105.48724.tjm1983@gmail.com>*Organization*: Technische Universität München*References*: <0016e6d99b30af72d8049fa34bfc@google.com> <201103301105.48724.tjm1983@gmail.com>

Hi Timothy, Am Mittwoch, den 30.03.2011, 11:05 +1300 schrieb Timothy McKenzie: [..] > I tested all this in Isabelle2009-2. I haven't moved to > Isabelle2011 yet, because my work relies heavily on what I've just > described, and the following in the NEWS file for Isabelle2011 > worried me: > > * Session Multivariate_Analysis: introduced a type class for > euclidean space. Most theorems are now stated in terms of > euclidean spaces instead of finite cartesian products. > > types > real ^ 'n ~> 'a::real_vector > ~> 'a::euclidean_space > ~> 'a::ordered_euclidean_space > (depends on your needs) > > constants > _ $ _ ~> _ $$ _ > \<chi> x. _ ~> \<chi>\<chi> x. _ > CARD('n) ~> DIM('a) > > Also note that the indices are now natural numbers and not from > some finite type. Finite cartesian products of euclidean spaces, > products of euclidean spaces the real and complex numbers are > instantiated to be euclidean_spaces. INCOMPATIBILITY. Did you try Isabelle2011? Of course the type real ^ 'n was not removed, but for most lemmas the constant names changed. 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). 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? > Tim > <>< Greetings, Johannes

**Follow-Ups**:**[isabelle] real^'n in Isabelle2011***From:*Timothy McKenzie

**References**:**[isabelle] Proving two real^3 spaces are the same***From:*s . wong . 731

**Re: [isabelle] Proving two real^3 spaces are the same***From:*Timothy McKenzie

- Previous by Date: Re: [isabelle] Proving two real^3 spaces are the same
- Next by Date: [isabelle] "Coercion inference failed"
- Previous by Thread: Re: [isabelle] Proving two real^3 spaces are the same
- Next by Thread: [isabelle] real^'n in Isabelle2011
- Cl-isabelle-users March 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list