[isabelle] Proving two real^3 spaces are the same



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"

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]?

Thanks
Steve




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