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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
