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:
>> 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





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