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
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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
