Dear Christian,
They are useful, I have added them (and slightly modified the names):
http://isabelle.in.tum.de/repos/isabelle/rev/5df7a346f07b
Thanks
Tobias
On 25/08/2017 06:55, Christian Sternagel wrote:
Dear list,
maybe the following results about "lex" are worthwhile to add to the
libra
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"
