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.