# HG changeset patch
# User nipkow
# Date 1452267401 -3600
# Node ID db9996a841669e65ade6eceea30dc18166072511
# Parent  4d38c04957fc5283174322dd317a0234d63e5468
added lemma

diff -r 4d38c04957fc -r db9996a84166 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Jan 08 15:27:16 2016 +0100
+++ b/src/HOL/List.thy	Fri Jan 08 16:36:41 2016 +0100
@@ -5399,6 +5399,72 @@
 apply (case_tac xys, simp_all, blast)
 done
 
+text{* By Mathias Fleury: *}
+lemma lexn_transI:
+  assumes "trans r" shows "trans (lexn r n)"
+unfolding trans_def
+proof (intro allI impI)
+  fix as bs cs
+  assume asbs: "(as, bs) \<in> lexn r n" and bscs: "(bs, cs) \<in> 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) \<in> 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') \<in> 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
+  thus "(as, cs) \<in> 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) \<in> 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) \<in> 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') \<in> r"
+      using abr b'c'r assms unfolding trans_def by blast
+    ultimately show ?thesis using n n' unfolding lexn_conv as bs cs by auto
+  qed
+qed
+
 lemma lex_conv:
   "lex r =
     {(xs,ys). length xs = length ys \<and>