*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Proving two real^3 spaces are the same*From*: Timothy McKenzie <tjm1983 at gmail.com>*Date*: Wed, 30 Mar 2011 11:05:34 +1300*In-reply-to*: <0016e6d99b30af72d8049fa34bfc@google.com>*References*: <0016e6d99b30af72d8049fa34bfc@google.com>*User-agent*: KMail/1.13.6 (Linux/2.6.34.8-68.fc13.x86_64; KDE/4.5.5; x86_64; ; )

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. 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. > Thanks > Steve Tim <><

**Attachment:
signature.asc**

**Follow-Ups**:**Re: [isabelle] Proving two real^3 spaces are the same***From:*Brian Huffman

**Re: [isabelle] Proving two real^3 spaces are the same***From:*Johannes Hölzl

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

- Previous by Date: [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: [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