[isabelle-dev] Lemmas about tranclp and lexn

[Tobias Nipkow]

I added lexn_transI.

Thanks
Tobias

On 30/12/2015 15:25, Mathias Fleury wrote:
> Dear list,
>
> I stumbled upon some lemmas that have a counterpart in Isabelle (like
> rtranclp_mono vs tranclp_mono), but are not included. Is there a reason why the
> following lemmas are not included in Isabelle?
>
> rtranclp vs tranclp:
>
>   * there is a rtranclp_mono "r ≤ s ==> r^** ≤ s^**", but no tranclp_mono. Given
>     the tranclp_mono, it should probably be:
>
>
>     lemma tranclp_mono:
>        "r⇧+⇧+ a b ⟹ r ≤ s ⟹ s⇧+⇧+ a b"
>          using rtranclp_mono by (auto dest!: tranclpD intro: rtranclp_into_tranclp2)
>
>
>   * there is a rtranclp_idemp and a rtrancl_idemp marked as simp "(r^**)^** =
>     r^**", but no trancl_idemp nor tranclp_idemp
>
>
>     lemma trancl_idemp: "(r⇧+)⇧+ = r⇧+"
>        by simp
>
>     lemmas tranclp_idemp = trancl_idemp[to_pred]
>
>
> Transitivity of lexord vs lexn:
>
>   * there is a lexord_transI "trans r ⟹ trans (lexord r)", but no lexn_transI
>
>
>     (I have not been able to factor the case distinction below; the proof uses
>     the new consider keyword)
>
>
>     lemma lexn_transI:
>        assumes trans: "trans r"
>        shows "trans (lexn r n)"
>          unfolding trans_def
>     proof (intro allI impI)
>        fix as bs cs
>        assume asbs: "(as, bs) ∈ lexn r n" and bscs: "(bs, cs) ∈ lexn r n"
>
>        obtain abs a b as' bs' where
>          n: "length as = n" and "length bs = n" and
>          as: "as = abs @ a # as'" and
>          bs: "bs = abs @ b # bs'" and
>          abr: "(a, b) ∈ r"
>          using asbs unfolding lexn_conv by blast
>
>        obtain bcs b' c' cs' bs' where
>          n': "length cs = n" and "length bs = n" and
>          bs': "bs = bcs @ b' # bs'" and
>          cs: "cs = bcs @ c' # cs'" and
>          b'c'r: "(b', c') ∈ r"
>          using bscs unfolding lexn_conv by blast
>        consider (le) "length bcs < length abs"
>          | (eq) "length bcs = length abs"
>          | (ge) "length bcs > length abs" by linarith
>        then show "(as, cs) ∈ lexn r n"
>          proof cases
>            let ?k = "length bcs"
>            case le
>            hence "as ! ?k = bs ! ?k" unfolding as bs by (simp add: nth_append)
>            hence "(as ! ?k, cs ! ?k) ∈ r" using b'c'r unfolding bs' cs by auto
>            moreover
>              have "length bcs < length as" using le unfolding as by simp
>              from id_take_nth_drop[OF this] have "as = take ?k as @ as ! ?k #
>     drop (Suc ?k) as" .
>            moreover
>              have "length bcs < length cs" unfolding cs by simp
>              from id_take_nth_drop[OF this] have "cs = take ?k cs @ cs ! ?k #
>     drop (Suc ?k) cs" .
>            moreover have "take ?k as = take ?k cs"
>              using le arg_cong[OF bs, of "take (length bcs)"] unfolding cs as
>     bs' by auto
>            ultimately show ?thesis using n n' unfolding lexn_conv by auto
>          next
>            let ?k = "length abs"
>            case ge
>            hence "bs ! ?k = cs ! ?k" unfolding bs' cs by (simp add: nth_append)
>            hence "(as ! ?k, cs ! ?k) ∈ r" using abr unfolding as bs by auto
>            moreover
>              have "length abs < length as" using ge unfolding as by simp
>              from id_take_nth_drop[OF this] have "as = take ?k as @ as ! ?k #
>     drop (Suc ?k) as" .
>            moreover
>              have "length abs < length cs" using n n' unfolding as by simp
>              from id_take_nth_drop[OF this] have "cs = take ?k cs @ cs ! ?k #
>     drop (Suc ?k) cs" .
>            moreover have "take ?k as = take ?k cs"
>              using ge arg_cong[OF bs', of "take (length abs)"] unfolding cs as
>     bs by auto
>            ultimately show ?thesis using n n' unfolding lexn_conv by auto
>          next
>            let ?k = "length abs"
>            case eq
>            hence "abs = bcs" "b = b'" using bs bs' by auto
>            moreover hence "(a, c') ∈ r" using abr b'c'r trans unfolding
>     trans_def by blast
>            ultimately show ?thesis using n n' unfolding lexn_conv as bs cs by auto
>          qed
>     qed
>
>
>
> Best regards,
>
> Mathias
>
>
> _______________________________________________
> 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: 5132 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20160108/952218d2/attachment-0001.p7s>