src/HOL/List.thy

     by (simp add: assms wf_lexn)
   show "\<And>i j. lexn r i \<noteq> lexn r j \<Longrightarrow> Domain (lexn r i) \<inter> Range (lexn r j) = {}"
     by (metis DomainE Int_emptyI RangeE lexn_length)
 qed
 
-
 lemma lexn_conv:
   "lexn r n =
     {(xs,ys). length xs = n \<and> length ys = n \<and>
     (\<exists>xys x y xs' ys'. xs= xys @ x#xs' \<and> ys= xys @ y # ys' \<and> (x, y) \<in> r)}"
 proof (induction n)

 
 lemma irrefl_lex: "irrefl r \<Longrightarrow> irrefl (lex r)"
   by (meson irrefl_def lex_take_index)
 
 
-
 subsubsection \<open>Lexicographic Ordering\<close>
 
 text \<open>Classical lexicographic ordering on lists, ie. "a" < "ab" < "b".
     This ordering does \emph{not} preserve well-foundedness.
      Author: N. Voelker, March 2005.\<close>

   have "(x,z) \<in> r \<or> x = z \<and> (xs,zs) \<in> lexord r" by blast
   thus ?case unfolding zzs by auto
 qed
 
 lemma lexord_trans:
-    "\<lbrakk> (x, y) \<in> lexord r; (y, z) \<in> lexord r; trans r \<rbrakk> \<Longrightarrow> (x, z) \<in> lexord r"
-by(auto simp: trans_def intro:lexord_partial_trans)
+  "\<lbrakk> (x, y) \<in> lexord r; (y, z) \<in> lexord r; trans r \<rbrakk> \<Longrightarrow> (x, z) \<in> lexord r"
+  by(auto simp: trans_def intro:lexord_partial_trans)
 
 lemma lexord_transI:  "trans r \<Longrightarrow> trans (lexord r)"
-by (rule transI, drule lexord_trans, blast)
+  by (meson lexord_trans transI)
 
 lemma total_lexord: "total r \<Longrightarrow> total (lexord r)"
   unfolding total_on_def
 proof clarsimp
   fix x y

 by (simp add: irrefl_def lexord_irreflexive)
 
 lemma lexord_asym:
   assumes "asym R"
   shows "asym (lexord R)"
-proof
-  from assms obtain "irrefl R" by (blast elim: asym.cases)
-  then show "irrefl (lexord R)" by (rule lexord_irrefl)
-next
+proof 
   fix xs ys
   assume "(xs, ys) \<in> lexord R"
   then show "(ys, xs) \<notin> lexord R"
   proof (induct xs arbitrary: ys)
     case Nil

 proof -
   from \<open>asym R\<close> have "asym (lexord R)" by (rule lexord_asym)
   then show ?thesis by (rule asym.cases) (auto simp add: hyp)
 qed
 
+lemma asym_lex: "asym R \<Longrightarrow> asym (lex R)"
+  by (meson asym.simps irrefl_lex lexord_asym lexord_lex)
+
+lemma asym_lenlex: "asym R \<Longrightarrow> asym (lenlex R)"
+  by (simp add: lenlex_def asym_inv_image asym_less_than asym_lex asym_lex_prod)
+
+lemma lenlex_append1:
+  assumes len: "(us,xs) \<in> lenlex R" and eq: "length vs = length ys" 
+  shows "(us @ vs, xs @ ys) \<in> lenlex R"
+  using len
+proof (induction us)
+  case Nil
+  then show ?case 
+    by (simp add: lenlex_def eq)
+next
+  case (Cons u us)
+  with lex_append_rightI show ?case
+    by (fastforce simp add: lenlex_def eq)
+qed
+
+lemma lenlex_append2 [simp]:
+  assumes "irrefl R"
+  shows "(us @ xs, us @ ys) \<in> lenlex R \<longleftrightarrow> (xs, ys) \<in> lenlex R"
+proof (induction us)
+  case Nil
+  then show ?case 
+    by (simp add: lenlex_def)
+next
+  case (Cons u us)
+  with assms show ?case
+    by (auto simp: lenlex_def irrefl_def)
+qed
 
 text \<open>
   Predicate version of lexicographic order integrated with Isabelle's order type classes.
   Author: Andreas Lochbihler
 \<close>