# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1259579660 -3600
# Node ID 020e27417b59882e38630a8cdf77f0f685f369e8
# Parent  44a70e69ef92962bddecbdb9aeb4740d4a66f507
More code cleaning

diff -r 44a70e69ef92 -r 020e27417b59 FSet.thy
--- a/FSet.thy	Mon Nov 30 11:53:20 2009 +0100
+++ b/FSet.thy	Mon Nov 30 12:14:20 2009 +0100
@@ -505,20 +505,20 @@
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
-apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *})
+apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *})
 apply assumption
 apply (rule refl)
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
-apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *})
+apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *})
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* REPEAT_ALL_NEW (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
-apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *})
+apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *})
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
diff -r 44a70e69ef92 -r 020e27417b59 QuotMain.thy
--- a/QuotMain.thy	Mon Nov 30 11:53:20 2009 +0100
+++ b/QuotMain.thy	Mon Nov 30 12:14:20 2009 +0100
@@ -947,7 +947,7 @@
 
     (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *)
     (* observe ---> *) 
-    NDT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt 
+    NDT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP} ctxt 
                   THEN' (RANGE [SOLVES' (quotient_tac quot_thms)]))),
 
     (* R (t $ \<dots>) (t' $ \<dots>) ----> APPLY_RSP   provided type of t needs lifting *)
diff -r 44a70e69ef92 -r 020e27417b59 QuotScript.thy
--- a/QuotScript.thy	Mon Nov 30 11:53:20 2009 +0100
+++ b/QuotScript.thy	Mon Nov 30 12:14:20 2009 +0100
@@ -68,14 +68,14 @@
 by blast
 
 lemma QUOTIENT_REL_REP:
-  assumes a: "QUOTIENT E Abs Rep"
-  shows "E (Rep a) (Rep b) = (a = b)"
+  assumes a: "QUOTIENT R Abs Rep"
+  shows "R (Rep a) (Rep b) = (a = b)"
 using a unfolding QUOTIENT_def
 by metis
 
 lemma QUOTIENT_REP_ABS:
-  assumes a: "QUOTIENT E Abs Rep"
-  shows "E r r \<Longrightarrow> E (Rep (Abs r)) r"
+  assumes a: "QUOTIENT R Abs Rep"
+  shows "R r r \<Longrightarrow> R (Rep (Abs r)) r"
 using a unfolding QUOTIENT_def
 by blast
 
@@ -260,10 +260,11 @@
 using q1 q2 r1 r2 a
 by (simp add: FUN_REL_EQUALS)
 
+(* We don't use it, it is exactly the same as QUOTIENT_REL_REP but wrong way *)
 lemma EQUALS_PRS:
   assumes q: "QUOTIENT R Abs Rep"
   shows "(x = y) = R (Rep x) (Rep y)"
-by (simp add: QUOTIENT_REL_REP[OF q]) 
+by (rule QUOTIENT_REL_REP[OF q, symmetric])
 
 lemma EQUALS_RSP:
   assumes q: "QUOTIENT R Abs Rep"
@@ -286,8 +287,9 @@
   shows "(\<lambda>x. f x) = (Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x)"
 unfolding expand_fun_eq
 using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2]
-by (simp)
+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"
@@ -321,25 +323,21 @@
   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_REFL[OF q])
+
+(* Not used *)
+lemma REP_ABS_RSP_LEFT:
+  assumes q: "QUOTIENT R Abs Rep"
+  and     a: "R x1 x2"
   and   "R (Rep (Abs x1)) x2"
-proof -
-  show "R x1 (Rep (Abs x2))" 
-    using q a by (metis QUOTIENT_REL[OF q] QUOTIENT_ABS_REP[OF q] QUOTIENT_REP_REFL[OF q])
-next
-  show "R (Rep (Abs x1)) x2"
-    using q a by (metis QUOTIENT_REL[OF q] QUOTIENT_ABS_REP[OF q] QUOTIENT_REP_REFL[OF q] QUOTIENT_SYM[of q])
-qed
+  shows "R x1 (Rep (Abs x2))"
+using q a by (metis QUOTIENT_REL[OF q] QUOTIENT_ABS_REP[OF q] QUOTIENT_REP_REFL[OF q] QUOTIENT_SYM[of q])
 
 (* ----------------------------------------------------- *)
 (* Quantifiers: FORALL, EXISTS, EXISTS_UNIQUE,           *)
 (*              RES_FORALL, RES_EXISTS, RES_EXISTS_EQUIV *)
 (* ----------------------------------------------------- *)
 
-(* what is RES_FORALL *)
-(*--`!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
-         !f. $! f = RES_FORALL (respects R) ((abs --> I) f)`--*)
-(*as peter here *)
-
 (* bool theory: COND, LET *)
 
 lemma IF_PRS:
@@ -399,6 +397,7 @@
 
 (* combinators: I, K, o, C, W *)
 
+(* We use id_simps which includes id_apply; so these 2 theorems can be removed *)
 lemma I_PRS:
   assumes q: "QUOTIENT R Abs Rep"
   shows "id e = Abs (id (Rep e))"