# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1271343312 -7200
# Node ID 11c6106d778757f5243573bc65099e2c49c696ad
# Parent  b43b22f636659a86518bffe3416fd21a3316f8d6
Respectfullness and preservation of list_rel

diff -r b43b22f63665 -r 11c6106d7787 src/HOL/Library/Quotient_List.thy
--- a/src/HOL/Library/Quotient_List.thy	Thu Apr 15 12:27:14 2010 +0200
+++ b/src/HOL/Library/Quotient_List.thy	Thu Apr 15 16:55:12 2010 +0200
@@ -217,6 +217,52 @@
   apply (simp_all)
   done
 
+lemma list_rel_rsp:
+  assumes r: "\<forall>x y. R x y \<longrightarrow> (\<forall>a b. R a b \<longrightarrow> S x a = T y b)"
+  and l1: "list_rel R x y"
+  and l2: "list_rel R a b"
+  shows "list_rel S x a = list_rel T y b"
+  proof -
+    have a: "length y = length x" by (rule list_rel_len[OF l1, symmetric])
+    have c: "length a = length b" by (rule list_rel_len[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_rel S x a" using list_rel_len by auto
+      have "length y \<noteq> length b" using d a c by simp
+      then have "\<not>list_rel T y b" using list_rel_len by auto
+      then show ?thesis using e by simp
+    qed
+  qed
+
+lemma[quot_respect]:
+  "((R ===> R ===> op =) ===> list_rel R ===> list_rel R ===> op =) list_rel list_rel"
+  by (simp add: list_rel_rsp)
+
+lemma[quot_preserve]:
+  assumes a: "Quotient R abs1 rep1"
+  shows "((abs1 ---> abs1 ---> id) ---> map rep1 ---> map rep1 ---> id) list_rel = list_rel"
+  apply (simp add: expand_fun_eq)
+  apply clarify
+  apply (induct_tac xa xb rule: list_induct2')
+  apply (simp_all add: Quotient_abs_rep[OF a])
+  done
+
+lemma[quot_preserve]:
+  assumes a: "Quotient R abs1 rep1"
+  shows "(list_rel ((rep1 ---> rep1 ---> id) R) l m) = (l = m)"
+  by (induct l m rule: list_induct2') (simp_all add: Quotient_rel_rep[OF a])
+
 lemma list_rel_eq[id_simps]:
   shows "(list_rel (op =)) = (op =)"
   unfolding expand_fun_eq
diff -r b43b22f63665 -r 11c6106d7787 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Apr 15 12:27:14 2010 +0200
+++ b/src/HOL/List.thy	Thu Apr 15 16:55:12 2010 +0200
@@ -513,6 +513,17 @@
     (cases zs, simp_all)
 qed
 
+lemma list_induct4 [consumes 3, case_names Nil Cons]:
+  "length xs = length ys \<Longrightarrow> length ys = length zs \<Longrightarrow> length zs = length ws \<Longrightarrow>
+   P [] [] [] [] \<Longrightarrow> (\<And>x xs y ys z zs w ws. length xs = length ys \<Longrightarrow>
+   length ys = length zs \<Longrightarrow> length zs = length ws \<Longrightarrow> P xs ys zs ws \<Longrightarrow>
+   P (x#xs) (y#ys) (z#zs) (w#ws)) \<Longrightarrow> P xs ys zs ws"
+proof (induct xs arbitrary: ys zs ws)
+  case Nil then show ?case by simp
+next
+  case (Cons x xs ys zs ws) then show ?case by ((cases ys, simp_all), (cases zs,simp_all)) (cases ws, simp_all)
+qed
+
 lemma list_induct2': 
   "\<lbrakk> P [] [];
   \<And>x xs. P (x#xs) [];