Dear Christian,

They are useful, I have added them (and slightly modified the names):


On 25/08/2017 06:55, Christian Sternagel wrote:
Dear list,

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

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


isabelle-dev mailing list

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

isabelle-dev mailing list

Reply via email to