diff -r f89ee40fbb08 -r 78d828f43cdf Attic/UnusedQuotBase.thy
--- a/Attic/UnusedQuotBase.thy	Sat Dec 17 16:57:25 2011 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,90 +0,0 @@
-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