1.1 --- a/src/HOL/List.thy	Tue Mar 15 15:49:42 2011 +0100
     1.2 +++ b/src/HOL/List.thy	Tue Mar 15 22:04:02 2011 +0100
     1.3 @@ -4449,28 +4449,48 @@
     1.4    by (simp add: drop_Suc_conv_tl) 
     1.5  
     1.6  -- {* lexord is extension of partial ordering List.lex *} 
     1.7 -lemma lexord_lex: " (x,y) \<in> lex r = ((x,y) \<in> lexord r \<and> length x = length y)"
     1.8 +lemma lexord_lex: "(x,y) \<in> lex r = ((x,y) \<in> lexord r \<and> length x = length y)"
     1.9    apply (rule_tac x = y in spec) 
    1.10    apply (induct_tac x, clarsimp) 
    1.11    by (clarify, case_tac x, simp, force)
    1.12  
    1.13 -lemma lexord_irreflexive: "(! x. (x,x) \<notin> r) \<Longrightarrow> (y,y) \<notin> lexord r"
    1.14 -  by (induct y, auto)
    1.15 +lemma lexord_irreflexive: "ALL x. (x,x) \<notin> r \<Longrightarrow> (xs,xs) \<notin> lexord r"
    1.16 +by (induct xs) auto
    1.17 +
    1.18 +text{* By Ren\'e Thiemann: *}
    1.19 +lemma lexord_partial_trans: 
    1.20 +  "(\<And>x y z. x \<in> set xs \<Longrightarrow> (x,y) \<in> r \<Longrightarrow> (y,z) \<in> r \<Longrightarrow> (x,z) \<in> r)
    1.21 +   \<Longrightarrow>  (xs,ys) \<in> lexord r  \<Longrightarrow>  (ys,zs) \<in> lexord r \<Longrightarrow>  (xs,zs) \<in> lexord r"
    1.22 +proof (induct xs arbitrary: ys zs)
    1.23 +  case Nil
    1.24 +  from Nil(3) show ?case unfolding lexord_def by (cases zs, auto)
    1.25 +next
    1.26 +  case (Cons x xs yys zzs)
    1.27 +  from Cons(3) obtain y ys where yys: "yys = y # ys" unfolding lexord_def
    1.28 +    by (cases yys, auto)
    1.29 +  note Cons = Cons[unfolded yys]
    1.30 +  from Cons(3) have one: "(x,y) \<in> r \<or> x = y \<and> (xs,ys) \<in> lexord r" by auto
    1.31 +  from Cons(4) obtain z zs where zzs: "zzs = z # zs" unfolding lexord_def
    1.32 +    by (cases zzs, auto)
    1.33 +  note Cons = Cons[unfolded zzs]
    1.34 +  from Cons(4) have two: "(y,z) \<in> r \<or> y = z \<and> (ys,zs) \<in> lexord r" by auto
    1.35 +  {
    1.36 +    assume "(xs,ys) \<in> lexord r" and "(ys,zs) \<in> lexord r"
    1.37 +    from Cons(1)[OF _ this] Cons(2)
    1.38 +    have "(xs,zs) \<in> lexord r" by auto
    1.39 +  } note ind1 = this
    1.40 +  {
    1.41 +    assume "(x,y) \<in> r" and "(y,z) \<in> r"
    1.42 +    from Cons(2)[OF _ this] have "(x,z) \<in> r" by auto
    1.43 +  } note ind2 = this
    1.44 +  from one two ind1 ind2
    1.45 +  have "(x,z) \<in> r \<or> x = z \<and> (xs,zs) \<in> lexord r" by blast
    1.46 +  thus ?case unfolding zzs by auto
    1.47 +qed
    1.48  
    1.49  lemma lexord_trans: 
    1.50      "\<lbrakk> (x, y) \<in> lexord r; (y, z) \<in> lexord r; trans r \<rbrakk> \<Longrightarrow> (x, z) \<in> lexord r"
    1.51 -   apply (erule rev_mp)+
    1.52 -   apply (rule_tac x = x in spec) 
    1.53 -  apply (rule_tac x = z in spec) 
    1.54 -  apply ( induct_tac y, simp, clarify)
    1.55 -  apply (case_tac xa, erule ssubst) 
    1.56 -  apply (erule allE, erule allE) -- {* avoid simp recursion *} 
    1.57 -  apply (case_tac x, simp, simp) 
    1.58 -  apply (case_tac x, erule allE, erule allE, simp)
    1.59 -  apply (erule_tac x = listb in allE) 
    1.60 -  apply (erule_tac x = lista in allE, simp)
    1.61 -  apply (unfold trans_def)
    1.62 -  by blast
    1.63 +by(auto simp: trans_def intro:lexord_partial_trans)
    1.64  
    1.65  lemma lexord_transI:  "trans r \<Longrightarrow> trans (lexord r)"
    1.66  by (rule transI, drule lexord_trans, blast)