[isabelle-dev] Lemmas about tranclp and lexn
Tobias Nipkow
nipkow at in.tum.de
Fri Jan 8 16:39:10 CET 2016
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>
More information about the isabelle-dev
mailing list