Re: [isabelle] Comparing pairs

```Am Donnerstag, den 13.09.2012, 23:29 +0100 schrieb John Munroe:
> Hi,
>
> With Multivariate_Analysis, does anyone know how I can prove
>
> lemma "((1::real),(2::real)) < (2,4)"
>
> ?
>
> Thanks a lot in advance.
>
> John

Hi John,

the products of Euclidean spaces are missing some lemmas. I will add
them to the development version of Isabelle, but they should work with
Isabelle2012:

lemma euclidean_component_prod:
fixes a :: "'a :: euclidean_space" and b :: "'b :: euclidean_space"
shows "(a, b) \$\$ i = (if i < DIM('a) then a \$\$ i else b \$\$ (i - DIM('a)))"
by (simp add: euclidean_component_def basis_prod_def)

lemma less_prod_iff:
fixes a c :: "'a :: ordered_euclidean_space" and b d :: "'b :: ordered_euclidean_space"
shows "(a, b) < (c, d) ⟷ a < c ∧ b < d"
unfolding eucl_less[where 'a='a] eucl_less[where 'a='b] eucl_less[where 'a="'a * 'b"]
proof safe
assume *: "∀i<DIM('a * 'b). (a, b) \$\$ i < (c, d) \$\$ i"

{ fix i assume "i < DIM('a)"
with *[THEN spec, of "i"]
show "a \$\$ i < c \$\$ i"
by (auto simp: euclidean_component_prod) }

{ fix i assume "i < DIM('b)"
with *[THEN spec, of "i + DIM('a)"]
show "b \$\$ i < d \$\$ i"
by (auto simp: euclidean_component_prod) }

qed (auto simp: euclidean_component_prod)

- Johannes

```

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