src/HOL/UNITY/ListOrder.thy
changeset 32235 8f9b8d14fc9f
parent 30198 922f944f03b2
child 32960 69916a850301
     1.1 --- a/src/HOL/UNITY/ListOrder.thy	Mon Jul 27 17:36:30 2009 +0200
     1.2 +++ b/src/HOL/UNITY/ListOrder.thy	Mon Jul 27 21:47:41 2009 +0200
     1.3 @@ -117,7 +117,7 @@
     1.4  (*Lemma proving transitivity and more*)
     1.5  lemma genPrefix_trans_O [rule_format]: 
     1.6       "(x, y) : genPrefix r  
     1.7 -      ==> ALL z. (y,z) : genPrefix s --> (x, z) : genPrefix (s O r)"
     1.8 +      ==> ALL z. (y,z) : genPrefix s --> (x, z) : genPrefix (r O s)"
     1.9  apply (erule genPrefix.induct)
    1.10    prefer 3 apply (blast dest: append_genPrefix)
    1.11   prefer 2 apply (blast intro: genPrefix.prepend, blast)
    1.12 @@ -134,13 +134,15 @@
    1.13  lemma prefix_genPrefix_trans [rule_format]: 
    1.14       "[| x<=y;  (y,z) : genPrefix r |] ==> (x, z) : genPrefix r"
    1.15  apply (unfold prefix_def)
    1.16 -apply (subst R_O_Id [symmetric], erule genPrefix_trans_O, assumption)
    1.17 +apply (drule genPrefix_trans_O, assumption)
    1.18 +apply simp
    1.19  done
    1.20  
    1.21  lemma genPrefix_prefix_trans [rule_format]: 
    1.22       "[| (x,y) : genPrefix r;  y<=z |] ==> (x,z) : genPrefix r"
    1.23  apply (unfold prefix_def)
    1.24 -apply (subst Id_O_R [symmetric], erule genPrefix_trans_O, assumption)
    1.25 +apply (drule genPrefix_trans_O, assumption)
    1.26 +apply simp
    1.27  done
    1.28  
    1.29  lemma trans_genPrefix: "trans r ==> trans (genPrefix r)"