Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Comparing pairs

Email Gateway (Aug 19 2022 at 08:51):

From: John Munroe <munddr@gmail.com>
Hi,

With Multivariate_Analysis, does anyone know how I can prove

lemma "((1::real),(2::real)) < (2,4)"

?

Thanks a lot in advance.

John

Email Gateway (Aug 19 2022 at 08:51):

From: Johannes Hölzl <hoelzl@in.tum.de>
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

Last updated: Apr 19 2024 at 16:20 UTC