Re: [isabelle] Proving two real^3 spaces are the same
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:
>> If I have two real^3 spaces S1 and S2 as:
>> 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.
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.
> 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:
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)
This archive was generated by a fusion of
Pipermail (Mailman edition) and