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