[isabelle-dev] some results about "lex"

[Christian Sternagel]

Dear list,

maybe the following results about "lex" are worthwhile to add to the
library?

lemma lex_append_right:
  "(xs, ys) ∈ lex r ⟹ length vs = length us ⟹ (xs @ us, ys @ vs) ∈ lex r"
  by (force simp: lex_def lexn_conv)

lemma lex_append_left:
  "(ys, zs) ∈ lex r ⟹ (xs @ ys, xs @ zs) ∈ lex r"
  by (induct xs) auto

lemma lex_take_index:
  assumes "(xs, ys) ∈ lex r"
  obtains i where "i < length xs" and "i < length ys" and "take i xs =
take i ys"
    and "(xs ! i, ys ! i) ∈ r"
proof -
  obtain n us x xs' y ys' where "(xs, ys) ∈ lexn r n" and "length xs =
n" and "length ys = n"
    and "xs = us @ x # xs'" and "ys = us @ y # ys'" and "(x, y) ∈ r"
    using assms by (fastforce simp: lex_def lexn_conv)
  then show ?thesis by (intro that [of "length us"]) auto
qed

cheers

chris