Re: [isabelle-dev] some results about "lex"

2017-08-25 Thread Tobias Nipkow
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

[isabelle-dev] some results about "lex"

2017-08-24 Thread 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"