# HG changeset patch
# User huffman
# Date 1323436445 -3600
# Node ID fe44c0b216efd72f9d2a66c1074143fe2a81cb37
# Parent  16e8e4d33c426d5753459e8ec9dbf3b448b87b5e
remove some duplicate lemmas, simplify some proofs

diff -r 16e8e4d33c42 -r fe44c0b216ef src/HOL/Library/Quotient_List.thy
--- a/src/HOL/Library/Quotient_List.thy	Fri Dec 09 13:42:16 2011 +0100
+++ b/src/HOL/Library/Quotient_List.thy	Fri Dec 09 14:14:05 2011 +0100
@@ -12,15 +12,7 @@
 
 lemma map_id [id_simps]:
   "map id = id"
-  by (simp add: id_def fun_eq_iff map.identity)
-
-lemma list_all2_map1:
-  "list_all2 R (map f xs) ys \<longleftrightarrow> list_all2 (\<lambda>x. R (f x)) xs ys"
-  by (induct xs ys rule: list_induct2') simp_all
-
-lemma list_all2_map2:
-  "list_all2 R xs (map f ys) \<longleftrightarrow> list_all2 (\<lambda>x y. R x (f y)) xs ys"
-  by (induct xs ys rule: list_induct2') simp_all
+  by (fact map.id)
 
 lemma list_all2_eq [id_simps]:
   "list_all2 (op =) = (op =)"
@@ -57,10 +49,9 @@
 proof (rule transpI)
   from assms have *: "\<And>xs ys zs. R xs ys \<Longrightarrow> R ys zs \<Longrightarrow> R xs zs" by (rule transpE)
   fix xs ys zs
-  assume A: "list_all2 R xs ys" "list_all2 R ys zs"
-  then have "length xs = length ys" "length ys = length zs" by (blast dest: list_all2_lengthD)+
-  then show "list_all2 R xs zs" using A
-    by (induct xs ys zs rule: list_induct3) (auto intro: *)
+  assume "list_all2 R xs ys" and "list_all2 R ys zs"
+  then show "list_all2 R xs zs"
+    by (induct arbitrary: zs) (auto simp: list_all2_Cons1 intro: *)
 qed
 
 lemma list_equivp [quot_equiv]:
@@ -158,23 +149,16 @@
   shows "((abs1 ---> abs2 ---> rep1) ---> rep1 ---> (map rep2) ---> abs1) foldl = foldl"
   by (simp add: fun_eq_iff foldl_prs_aux [OF a b])
 
-lemma list_all2_empty:
-  shows "list_all2 R [] b \<Longrightarrow> length b = 0"
-  by (induct b) (simp_all)
-
 (* induct_tac doesn't accept 'arbitrary', so we manually 'spec' *)
 lemma foldl_rsp[quot_respect]:
   assumes q1: "Quotient R1 Abs1 Rep1"
   and     q2: "Quotient R2 Abs2 Rep2"
   shows "((R1 ===> R2 ===> R1) ===> R1 ===> list_all2 R2 ===> R1) foldl foldl"
   apply(auto simp add: fun_rel_def)
-  apply (subgoal_tac "R1 xa ya \<longrightarrow> list_all2 R2 xb yb \<longrightarrow> R1 (foldl x xa xb) (foldl y ya yb)")
-  apply simp
+  apply (erule_tac P="R1 xa ya" in rev_mp)
   apply (rule_tac x="xa" in spec)
   apply (rule_tac x="ya" in spec)
-  apply (rule_tac xs="xb" and ys="yb" in list_induct2)
-  apply (rule list_all2_lengthD)
-  apply (simp_all)
+  apply (erule list_all2_induct, simp_all)
   done
 
 lemma foldr_rsp[quot_respect]:
@@ -182,11 +166,7 @@
   and     q2: "Quotient R2 Abs2 Rep2"
   shows "((R1 ===> R2 ===> R2) ===> list_all2 R1 ===> R2 ===> R2) foldr foldr"
   apply (auto simp add: fun_rel_def)
-  apply(subgoal_tac "R2 xb yb \<longrightarrow> list_all2 R1 xa ya \<longrightarrow> R2 (foldr x xa xb) (foldr y ya yb)")
-  apply simp
-  apply (rule_tac xs="xa" and ys="ya" in list_induct2)
-  apply (rule list_all2_lengthD)
-  apply (simp_all)
+  apply (erule list_all2_induct, simp_all)
   done
 
 lemma list_all2_rsp:
@@ -194,28 +174,9 @@
   and l1: "list_all2 R x y"
   and l2: "list_all2 R a b"
   shows "list_all2 S x a = list_all2 T y b"
-  proof -
-    have a: "length y = length x" by (rule list_all2_lengthD[OF l1, symmetric])
-    have c: "length a = length b" by (rule list_all2_lengthD[OF l2])
-    show ?thesis proof (cases "length x = length a")
-      case True
-      have b: "length x = length a" by fact
-      show ?thesis using a b c r l1 l2 proof (induct rule: list_induct4)
-        case Nil
-        show ?case using assms by simp
-      next
-        case (Cons h t)
-        then show ?case by auto
-      qed
-    next
-      case False
-      have d: "length x \<noteq> length a" by fact
-      then have e: "\<not>list_all2 S x a" using list_all2_lengthD by auto
-      have "length y \<noteq> length b" using d a c by simp
-      then have "\<not>list_all2 T y b" using list_all2_lengthD by auto
-      then show ?thesis using e by simp
-    qed
-  qed
+  using l1 l2
+  by (induct arbitrary: a b rule: list_all2_induct,
+    auto simp: list_all2_Cons1 list_all2_Cons2 r)
 
 lemma [quot_respect]:
   "((R ===> R ===> op =) ===> list_all2 R ===> list_all2 R ===> op =) list_all2 list_all2"
@@ -239,10 +200,7 @@
   assumes a: "x \<in> set a"
   and b: "list_all2 R a b"
   shows "\<exists>y. (y \<in> set b \<and> R x y)"
-proof -
-  have "length a = length b" using b by (rule list_all2_lengthD)
-  then show ?thesis using a b by (induct a b rule: list_induct2) auto
-qed
+  using b a by induct auto
 
 lemma list_all2_refl:
   assumes a: "\<And>x y. R x y = (R x = R y)"