src/HOL/Library/Quotient_List.thy
changeset 47982 7aa35601ff65
parent 47936 756f30eac792
child 51377 7da251a6c16e
--- a/src/HOL/Library/Quotient_List.thy	Thu May 24 13:56:21 2012 +0200
+++ b/src/HOL/Library/Quotient_List.thy	Thu May 24 14:20:23 2012 +0200
@@ -37,7 +37,7 @@
     by (induct arbitrary: ys, simp, clarsimp simp add: list_all2_Cons1, fast)
 qed
 
-lemma list_reflp[reflp_preserve]:
+lemma list_reflp[reflexivity_rule]:
   assumes "reflp R"
   shows "reflp (list_all2 R)"
 proof (rule reflpI)
@@ -47,6 +47,17 @@
     by (induct xs) (simp_all add: *)
 qed
 
+lemma list_left_total[reflexivity_rule]:
+  assumes "left_total R"
+  shows "left_total (list_all2 R)"
+proof (rule left_totalI)
+  from assms have *: "\<And>xs. \<exists>ys. R xs ys" by (rule left_totalE)
+  fix xs
+  show "\<exists> ys. list_all2 R xs ys"
+    by (induct xs) (simp_all add: * list_all2_Cons1)
+qed
+
+
 lemma list_symp:
   assumes "symp R"
   shows "symp (list_all2 R)"