diff -r d1eaed018e5d -r 41f89d4f9548 Attic/UnusedQuotBase.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/UnusedQuotBase.thy	Wed Feb 10 17:10:52 2010 +0100
@@ -0,0 +1,90 @@
+lemma in_fun:
+  shows "x \<in> ((f ---> g) s) = g (f x \<in> s)"
+  by (simp add: mem_def)
+
+lemma respects_thm:
+  shows "Respects (R1 ===> R2) f = (\<forall>x y. R1 x y \<longrightarrow> R2 (f x) (f y))"
+  unfolding Respects_def
+  by (simp add: expand_fun_eq)
+
+lemma respects_rep_abs:
+  assumes a: "Quotient R1 Abs1 Rep1"
+  and     b: "Respects (R1 ===> R2) f"
+  and     c: "R1 x x"
+  shows "R2 (f (Rep1 (Abs1 x))) (f x)"
+  using a b[simplified respects_thm] c unfolding Quotient_def
+  by blast
+
+lemma respects_mp:
+  assumes a: "Respects (R1 ===> R2) f"
+  and     b: "R1 x y"
+  shows "R2 (f x) (f y)"
+  using a b unfolding Respects_def
+  by simp
+
+lemma respects_o:
+  assumes a: "Respects (R2 ===> R3) f"
+  and     b: "Respects (R1 ===> R2) g"
+  shows "Respects (R1 ===> R3) (f o g)"
+  using a b unfolding Respects_def
+  by simp
+
+lemma fun_rel_eq_rel:
+  assumes q1: "Quotient R1 Abs1 Rep1"
+  and     q2: "Quotient R2 Abs2 Rep2"
+  shows "(R1 ===> R2) f g = ((Respects (R1 ===> R2) f) \<and> (Respects (R1 ===> R2) g)
+                             \<and> ((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g))"
+  using fun_quotient[OF q1 q2] unfolding Respects_def Quotient_def expand_fun_eq
+  by blast
+
+lemma let_babs:
+  "v \<in> r \<Longrightarrow> Let v (Babs r lam) = Let v lam"
+  by (simp add: Babs_def)
+
+lemma fun_rel_equals:
+  assumes q1: "Quotient R1 Abs1 Rep1"
+  and     q2: "Quotient R2 Abs2 Rep2"
+  and     r1: "Respects (R1 ===> R2) f"
+  and     r2: "Respects (R1 ===> R2) g"
+  shows "((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g) = (\<forall>x y. R1 x y \<longrightarrow> R2 (f x) (g y))"
+  apply(rule_tac iffI)
+  apply(rule)+
+  apply (rule apply_rsp'[of "R1" "R2"])
+  apply(subst Quotient_rel[OF fun_quotient[OF q1 q2]])
+  apply auto
+  using fun_quotient[OF q1 q2] r1 r2 unfolding Quotient_def Respects_def
+  apply (metis let_rsp q1)
+  apply (metis fun_rel_eq_rel let_rsp q1 q2 r2)
+  using r1 unfolding Respects_def expand_fun_eq
+  apply(simp (no_asm_use))
+  apply(metis Quotient_rel[OF q2] Quotient_rel_rep[OF q1])
+  done
+
+(* ask Peter: fun_rel_IMP used twice *)
+lemma fun_rel_IMP2:
+  assumes q1: "Quotient R1 Abs1 Rep1"
+  and     q2: "Quotient R2 Abs2 Rep2"
+  and     r1: "Respects (R1 ===> R2) f"
+  and     r2: "Respects (R1 ===> R2) g"
+  and     a:  "(Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g"
+  shows "R1 x y \<Longrightarrow> R2 (f x) (g y)"
+  using q1 q2 r1 r2 a
+  by (simp add: fun_rel_equals)
+
+lemma lambda_rep_abs_rsp:
+  assumes r1: "\<And>r r'. R1 r r' \<Longrightarrow>R1 r (Rep1 (Abs1 r'))"
+  and     r2: "\<And>r r'. R2 r r' \<Longrightarrow>R2 r (Rep2 (Abs2 r'))"
+  shows "(R1 ===> R2) f1 f2 \<Longrightarrow> (R1 ===> R2) f1 ((Abs1 ---> Rep2) ((Rep1 ---> Abs2) f2))"
+  using r1 r2 by auto
+
+(* We use id_simps which includes id_apply; so these 2 theorems can be removed *)
+lemma id_prs:
+  assumes q: "Quotient R Abs Rep"
+  shows "Abs (id (Rep e)) = id e"
+  using Quotient_abs_rep[OF q] by auto
+
+lemma id_rsp:
+  assumes q: "Quotient R Abs Rep"
+  and     a: "R e1 e2"
+  shows "R (id e1) (id e2)"
+  using a by auto