[isabelle-dev] Lemmas about tranclp and lexn

[Mathias Fleury]

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
-------------- n�chster Teil --------------
Ein Dateianhang mit HTML-Daten wurde abgetrennt...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20151230/62a8203e/attachment.html>