1.1 --- a/src/HOL/Library/Quotient_List.thy	Thu May 24 13:56:21 2012 +0200
     1.2 +++ b/src/HOL/Library/Quotient_List.thy	Thu May 24 14:20:23 2012 +0200
     1.3 @@ -37,7 +37,7 @@
     1.4      by (induct arbitrary: ys, simp, clarsimp simp add: list_all2_Cons1, fast)
     1.5  qed
     1.6  
     1.7 -lemma list_reflp[reflp_preserve]:
     1.8 +lemma list_reflp[reflexivity_rule]:
     1.9    assumes "reflp R"
    1.10    shows "reflp (list_all2 R)"
    1.11  proof (rule reflpI)
    1.12 @@ -47,6 +47,17 @@
    1.13      by (induct xs) (simp_all add: *)
    1.14  qed
    1.15  
    1.16 +lemma list_left_total[reflexivity_rule]:
    1.17 +  assumes "left_total R"
    1.18 +  shows "left_total (list_all2 R)"
    1.19 +proof (rule left_totalI)
    1.20 +  from assms have *: "\<And>xs. \<exists>ys. R xs ys" by (rule left_totalE)
    1.21 +  fix xs
    1.22 +  show "\<exists> ys. list_all2 R xs ys"
    1.23 +    by (induct xs) (simp_all add: * list_all2_Cons1)
    1.24 +qed
    1.25 +
    1.26 +
    1.27  lemma list_symp:
    1.28    assumes "symp R"
    1.29    shows "symp (list_all2 R)"