--- a/QuotMain.thy	Fri Dec 04 16:53:11 2009 +0100
+++ b/QuotMain.thy	Fri Dec 04 17:15:55 2009 +0100
@@ -460,7 +460,7 @@
 fun equiv_tac rel_eqvs =
   REPEAT_ALL_NEW (FIRST' 
     [resolve_tac rel_eqvs,
-     rtac @{thm IDENTITY_equivp},
+     rtac @{thm identity_equivp},
      rtac @{thm list_equivp}])
 *}
 
@@ -724,7 +724,7 @@
 ML {*
 fun quotient_tac ctxt =
   REPEAT_ALL_NEW (FIRST'
-    [rtac @{thm IDENTITY_Quotient},
+    [rtac @{thm identity_quotient},
      resolve_tac (quotient_rules_get ctxt)])
 *}
 
@@ -895,7 +895,7 @@
       val (ty_a, ty_b) = dest_fun_type (fastype_of abs);
       val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b];
       val t_inst = map (SOME o (cterm_of thy)) [rel, abs, rep];
-      val thm = Drule.instantiate' ty_inst t_inst @{thm REP_ABS_RSP}
+      val thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp}
       val te = solve_quotient_assums context thm
       val t_inst = map (SOME o (cterm_of thy)) [lhs, rhs];
       val thm = Drule.instantiate' [] t_inst te

--- a/QuotScript.thy	Fri Dec 04 16:53:11 2009 +0100
+++ b/QuotScript.thy	Fri Dec 04 17:15:55 2009 +0100
@@ -72,12 +72,12 @@
 using a unfolding Quotient_def
 by blast
 
-lemma IDENTITY_equivp:
+lemma identity_equivp:
   shows "equivp (op =)"
 unfolding equivp_def
 by auto
 
-lemma IDENTITY_Quotient:
+lemma identity_quotient:
   shows "Quotient (op =) id id"
 unfolding Quotient_def id_def
 by blast
@@ -114,11 +114,6 @@
   shows "(id ---> id) = id"
 by (simp add: expand_fun_eq id_def)
 
-(* Not used *)
-lemma in_fun:
-  shows "x \<in> ((f ---> g) s) = g (f x \<in> s)"
-by (simp add: mem_def)
-
 fun
   fun_rel
 where
@@ -172,51 +167,10 @@
 where
   "Respects R x \<equiv> (R x x)"
 
-lemma IN_RESPECTS:
+lemma in_respects:
   shows "(x \<in> Respects R) = R x x"
 unfolding mem_def Respects_def by simp
 
-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_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_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_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
-
-(*
-definition
-  "RES_EXISTS_EQUIV R P \<equiv> (\<exists>x \<in> Respects R. P x) \<and> 
-                          (\<forall>x\<in> Respects R. \<forall>y\<in> Respects R. P x \<and> P y \<longrightarrow> R x y)"
-*)
-
-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
-
 (* TODO: it is the same as APPLY_RSP *)
 (* q1 and q2 not used; see next lemma *)
 lemma fun_rel_MP:
@@ -229,30 +183,6 @@
   shows "(R1 ===> R2) f g \<Longrightarrow> R1 x y \<Longrightarrow> R2 (f x) (g y)"
 by simp
 
-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)
-using fun_quotient[OF q1 q2] r1 r2 unfolding Quotient_def Respects_def
-apply(metis fun_rel_IMP)
-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 equals_rsp:
   assumes q: "Quotient R Abs Rep"
@@ -277,44 +207,7 @@
 using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
 by simp
 
-(* Not used since applic_prs proves a version for an arbitrary number of arguments *)
-lemma APP_PRS:
-  assumes q1: "Quotient R1 abs1 rep1"
-  and     q2: "Quotient R2 abs2 rep2"
-  shows "abs2 ((abs1 ---> rep2) f (rep1 x)) = f x"
-unfolding expand_fun_eq
-using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
-by simp
-
-(* Ask Peter: assumption q1 and q2 not used and lemma is the 'identity' *)
-lemma LAMBDA_RSP:
-  assumes q1: "Quotient R1 Abs1 Rep1"
-  and     q2: "Quotient R2 Abs2 Rep2"
-  and     a: "(R1 ===> R2) f1 f2"
-  shows "(R1 ===> R2) (\<lambda>x. f1 x) (\<lambda>y. f2 y)"
-by (rule a)
-
-(* ASK Peter about next four lemmas in quotientScript
-lemma ABSTRACT_PRS:
-  assumes q1: "Quotient R1 Abs1 Rep1"
-  and     q2: "Quotient R2 Abs2 Rep2"
-  shows "f = (Rep1 ---> Abs2) ???"
-*)
-
-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
-
-lemma REP_ABS_RSP:
-  assumes q: "Quotient R Abs Rep"
-  and     a: "R x1 x2"
-  shows "R x1 (Rep (Abs x2))"
-using q a by (metis Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q])
-
-(* Not used *)
-lemma REP_ABS_RSP_LEFT:
+lemma rep_abs_rsp:
   assumes q: "Quotient R Abs Rep"
   and     a: "R x1 x2"
   shows "R x1 (Rep (Abs x2))"
@@ -362,13 +255,6 @@
 
 (* FUNCTION APPLICATION *)
 
-(* Not used *)
-lemma APPLY_PRS:
-  assumes q1: "Quotient R1 Abs1 Rep1"
-  and     q2: "Quotient R2 Abs2 Rep2"
-  shows "f x = Abs2 (((Abs1 ---> Rep2) f) (Rep1 x))"
-using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] by auto
-
 (* In the following theorem R1 can be instantiated with anything,
    but we know some of the types of the Rep and Abs functions;
    so by solving Quotient assumptions we can get a unique R2 that
@@ -436,13 +322,13 @@
   fixes P :: "'a \<Rightarrow> bool"
   assumes a: "equivp R"
   shows "Ball (Respects R) P = (All P)"
-  by (metis equivp_def IN_RESPECTS a)
+  by (metis equivp_def in_respects a)
 
 lemma bex_reg_eqv:
   fixes P :: "'a \<Rightarrow> bool"
   assumes a: "equivp R"
   shows "Bex (Respects R) P = (Ex P)"
-  by (metis equivp_def IN_RESPECTS a)
+  by (metis equivp_def in_respects a)
 
 lemma ball_reg_right:
   assumes a: "\<And>x. R x \<Longrightarrow> P x \<longrightarrow> Q x"
@@ -457,12 +343,12 @@
 lemma ball_reg_left:
   assumes a: "equivp R"
   shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ball (Respects R) Q \<longrightarrow> All P"
-  by (metis equivp_reflp IN_RESPECTS a)
+  by (metis equivp_reflp in_respects a)
 
 lemma bex_reg_right:
   assumes a: "equivp R"
   shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ex Q \<longrightarrow> Bex (Respects R) P"
-  by (metis equivp_reflp IN_RESPECTS a)
+  by (metis equivp_reflp in_respects a)
 
 lemma ball_reg_eqv_range:
   fixes P::"'a \<Rightarrow> bool"
@@ -472,7 +358,7 @@
   apply(rule iffI)
   apply(rule allI)
   apply(drule_tac x="\<lambda>y. f x" in bspec)
-  apply(simp add: Respects_def IN_RESPECTS)
+  apply(simp add: Respects_def in_respects)
   apply(rule impI)
   using a equivp_reflp_symp_transp[of "R2"]
   apply(simp add: reflp_def)
@@ -488,7 +374,7 @@
   apply(auto)
   apply(rule_tac x="\<lambda>y. f x" in bexI)
   apply(simp)
-  apply(simp add: Respects_def IN_RESPECTS)
+  apply(simp add: Respects_def in_respects)
   apply(rule impI)
   using a equivp_reflp_symp_transp[of "R2"]
   apply(simp add: reflp_def)
@@ -530,25 +416,25 @@
 lemma ball_rsp:
   assumes a: "(R ===> (op =)) f g"
   shows "Ball (Respects R) f = Ball (Respects R) g"
-  using a by (simp add: Ball_def IN_RESPECTS)
+  using a by (simp add: Ball_def in_respects)
 
 lemma bex_rsp:
   assumes a: "(R ===> (op =)) f g"
   shows "(Bex (Respects R) f = Bex (Respects R) g)"
-  using a by (simp add: Bex_def IN_RESPECTS)
+  using a by (simp add: Bex_def in_respects)
 
 (* 2 lemmas needed for cleaning of quantifiers *)
 lemma all_prs:
   assumes a: "Quotient R absf repf"
   shows "Ball (Respects R) ((absf ---> id) f) = All f"
   using a unfolding Quotient_def
-  by (metis IN_RESPECTS fun_map.simps id_apply)
+  by (metis in_respects fun_map.simps id_apply)
 
 lemma ex_prs:
   assumes a: "Quotient R absf repf"
   shows "Bex (Respects R) ((absf ---> id) f) = Ex f"
   using a unfolding Quotient_def
-  by (metis COMBC_def Collect_def Collect_mem_eq IN_RESPECTS fun_map.simps id_apply)
+  by (metis COMBC_def Collect_def Collect_mem_eq in_respects fun_map.simps id_apply)
 
 
 (* UNUSED *)
@@ -564,6 +450,107 @@
 using a unfolding Quotient_def
 by blast
 
+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
+
+(* Not used since in the end we just unfold fun_map *)
+lemma APP_PRS:
+  assumes q1: "Quotient R1 abs1 rep1"
+  and     q2: "Quotient R2 abs2 rep2"
+  shows "abs2 ((abs1 ---> rep2) f (rep1 x)) = f x"
+unfolding expand_fun_eq
+using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
+by simp
+
+(* Ask Peter: assumption q1 and q2 not used and lemma is the 'identity' *)
+lemma LAMBDA_RSP:
+  assumes q1: "Quotient R1 Abs1 Rep1"
+  and     q2: "Quotient R2 Abs2 Rep2"
+  and     a: "(R1 ===> R2) f1 f2"
+  shows "(R1 ===> R2) (\<lambda>x. f1 x) (\<lambda>y. f2 y)"
+by (rule a)
+
+(* ASK Peter about next four lemmas in quotientScript
+lemma ABSTRACT_PRS:
+  assumes q1: "Quotient R1 Abs1 Rep1"
+  and     q2: "Quotient R2 Abs2 Rep2"
+  shows "f = (Rep1 ---> Abs2) ???"
+*)
+
+
+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)
+using fun_quotient[OF q1 q2] r1 r2 unfolding Quotient_def Respects_def
+apply(metis fun_rel_IMP)
+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
+
+(* Not used *)
+lemma rep_abs_rsp_left:
+  assumes q: "Quotient R Abs Rep"
+  and     a: "R x1 x2"
+  shows "R x1 (Rep (Abs x2))"
+using q a by (metis Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q])
 
 
 end