[isabelle-dev] some results about "lex"

[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
> 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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5156 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20170825/e004524d/attachment.bin>