[isabelle-dev] Lemmas about tranclp and lexn
Mathias Fleury
Mathias.Fleury at ens-rennes.fr
Wed Dec 30 15:25:44 CET 2015
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>
More information about the isabelle-dev
mailing list