summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Fri, 08 Jan 2016 16:36:41 +0100 | |

changeset 62090 | db9996a84166 |

parent 62089 | 4d38c04957fc |

child 62100 | 7a5754afe170 |

added lemma

src/HOL/List.thy | file | annotate | diff | comparison | revisions |

--- 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>