*To*: Timothy McKenzie <tjm1983 at gmail.com>*Subject*: Re: [isabelle] Proving two real^3 spaces are the same*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Tue, 29 Mar 2011 16:56:01 -0700*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <201103301105.48724.tjm1983@gmail.com>*References*: <0016e6d99b30af72d8049fa34bfc@google.com> <201103301105.48724.tjm1983@gmail.com>*Sender*: huffman.brian.c at gmail.com

On Tue, Mar 29, 2011 at 3:05 PM, Timothy McKenzie <tjm1983 at gmail.com> wrote: > On Wed, 30 Mar 2011 07:33:25 s.wong.731 at gmail.com wrote: >> Hi, >> >> If I have two real^3 spaces S1 and S2 as: >> >> axiomatization >> S1 :: "real ^ 2" and >> S2 :: "real ^ 2" where >> r1: "S1 $ 0 = S2 $ 0" and >> r2: "S1 $ 1 = S2 $ 1" and >> r3: "S1 $ 2 = S2 $ 2" > > You've written "real ^ 2" where I think you mean "real ^ 3", but > I'll leave it as it is for illustrative purposes. > >> lemma "S1 = S2" >> >> How would one go about proving the lemma? I suppose I'd need >> Cart_eq, which reads: >> >> lemma Cart_eq: "(x = y) <--> (ALL i. x$i = y$i)" >> >> but it quantifies over all i's. Since S1 and S2 have only 3 >> dimensions, then should i be only in the range [1..3]? > > The "2" in your type "real^2" is a type, not a member of the > natural numbers type (or any other type). You can write any > integer, and if Isabelle believes it's of the type "2", it will be > interpreted as a member of that type by taking its remainder > modulo 2. For example: > > lemma "-6 = (2 :: 2)" by simp > > So your r1 and r3 say exactly the same thing, but Isabelle didn't > complain, because it can interpret them meaningfully. > > So the quantified i in Cart_eq (when applied in your situation) is > an element of the type "2", which has only two elements: "0" and > "1" (or "1" and "2", if you prefer). The trick is to turn this > "ALL i." into a conjunction "x$1 = y$1 & x$2 = y$2", which can be > quickly proven from your r2 and r3. Fortunately, forall_2 can do > just this, so: > > lemma "S1 = S2" > using r2 r3 > by (simp add: Cart_eq forall_2) > > Multivariate_Analysis also has similar lemmas forall_1 and > forall_3 for the types "1" and "3", but not forall_4 or greater. Tim, Thanks for the great explanation of numeral types! > 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) I'm sure Johannes could say more about these changes, but I wanted to point out one benefit: Many lemmas that used to be specific to types "real ^ 'n" are now proved in general for any type in class euclidean_space. This means that users of the Multivariate_Analysis libraries are no longer restricted to using cartesian product types like "real ^ 2" and "real ^ 3". Types like "real * real" and "real * real * real" are also instances of class euclidean_space, and so most of the theorems in the Multivariate_Analysis library will work with them too. I happen to think that ordinary tuples are much easier to work with: For example, "(x, y, z)" is rather nicer than any notation available for type "real ^ 3". Also, it isn't too much trouble to convert back and forth between tuples and the generic "_$$_" notations: lemma fixes x y z :: "real" shows "(x,y,z) $$ 0 = x \<and> (x,y,z) $$ 1 = y \<and> (x,y,z) $$ 2 = z" by (simp add: euclidean_component_def basis_prod_def) - Brian

**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: Re: [isabelle] Proving two real^3 spaces are the same
- Previous by Thread: Re: [isabelle] Proving two real^3 spaces are the same
- Next by Thread: Re: [isabelle] Proving two real^3 spaces are the same
- 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