# HG changeset patch # User Cezary Kaliszyk # Date 1259935445 -3600 # Node ID f51e2b3e31490d36932615bebc689bdc6cef1c04 # Parent 9b1ad366827f81e01b927d5a51922d862b2f61f6 Naming changes diff -r 9b1ad366827f -r f51e2b3e3149 QuotScript.thy --- a/QuotScript.thy Fri Dec 04 14:35:36 2009 +0100 +++ b/QuotScript.thy Fri Dec 04 15:04:05 2009 +0100 @@ -3,102 +3,106 @@ begin definition - "EQUIV E \ \x y. E x y = (E x = E y)" + "equivp E \ \x y. E x y = (E x = E y)" definition - "REFL E \ \x. E x x" + "reflp E \ \x. E x x" definition - "SYM E \ \x y. E x y \ E y x" + "symp E \ \x y. E x y \ E y x" definition - "TRANS E \ \x y z. E x y \ E y z \ E x z" + "transp E \ \x y z. E x y \ E y z \ E x z" -lemma EQUIV_REFL_SYM_TRANS: - shows "EQUIV E = (REFL E \ SYM E \ TRANS E)" -unfolding EQUIV_def REFL_def SYM_def TRANS_def expand_fun_eq +lemma equivp_reflp_symp_transp: + shows "equivp E = (reflp E \ symp E \ transp E)" +unfolding equivp_def reflp_def symp_def transp_def expand_fun_eq by (blast) -lemma EQUIV_REFL: - shows "EQUIV E \ (\x. E x x)" - by (simp add: EQUIV_REFL_SYM_TRANS REFL_def) +lemma equivp_refl: + shows "equivp R \ (\x. R x x)" + by (simp add: equivp_reflp_symp_transp reflp_def) + +lemma equivp_reflp: + shows "equivp E \ (\x. E x x)" + by (simp add: equivp_reflp_symp_transp reflp_def) definition - "PART_EQUIV E \ (\x. E x x) \ (\x y. E x y = (E x x \ E y y \ (E x = E y)))" + "PART_equivp E \ (\x. E x x) \ (\x y. E x y = (E x x \ E y y \ (E x = E y)))" -lemma EQUIV_IMP_PART_EQUIV: - assumes a: "EQUIV E" - shows "PART_EQUIV E" -using a unfolding EQUIV_def PART_EQUIV_def +lemma equivp_IMP_PART_equivp: + assumes a: "equivp E" + shows "PART_equivp E" +using a unfolding equivp_def PART_equivp_def by auto definition - "QUOTIENT E Abs Rep \ (\a. Abs (Rep a) = a) \ + "Quotient E Abs Rep \ (\a. Abs (Rep a) = a) \ (\a. E (Rep a) (Rep a)) \ (\r s. E r s = (E r r \ E s s \ (Abs r = Abs s)))" -lemma QUOTIENT_ABS_REP: - assumes a: "QUOTIENT E Abs Rep" +lemma Quotient_ABS_REP: + assumes a: "Quotient E Abs Rep" shows "Abs (Rep a) = a" -using a unfolding QUOTIENT_def +using a unfolding Quotient_def by simp -lemma QUOTIENT_REP_REFL: - assumes a: "QUOTIENT E Abs Rep" +lemma Quotient_REP_reflp: + assumes a: "Quotient E Abs Rep" shows "E (Rep a) (Rep a)" -using a unfolding QUOTIENT_def +using a unfolding Quotient_def by blast -lemma QUOTIENT_REL: - assumes a: "QUOTIENT E Abs Rep" +lemma Quotient_REL: + assumes a: "Quotient E Abs Rep" shows " E r s = (E r r \ E s s \ (Abs r = Abs s))" -using a unfolding QUOTIENT_def +using a unfolding Quotient_def by blast -lemma QUOTIENT_REL_ABS: - assumes a: "QUOTIENT E Abs Rep" +lemma Quotient_REL_ABS: + assumes a: "Quotient E Abs Rep" shows "E r s \ Abs r = Abs s" -using a unfolding QUOTIENT_def +using a unfolding Quotient_def by blast -lemma QUOTIENT_REL_ABS_EQ: - assumes a: "QUOTIENT E Abs Rep" +lemma Quotient_REL_ABS_EQ: + assumes a: "Quotient E Abs Rep" shows "E r r \ E s s \ E r s = (Abs r = Abs s)" -using a unfolding QUOTIENT_def +using a unfolding Quotient_def by blast -lemma QUOTIENT_REL_REP: - assumes a: "QUOTIENT R Abs Rep" +lemma Quotient_REL_REP: + assumes a: "Quotient R Abs Rep" shows "R (Rep a) (Rep b) = (a = b)" -using a unfolding QUOTIENT_def +using a unfolding Quotient_def by metis -lemma QUOTIENT_REP_ABS: - assumes a: "QUOTIENT R Abs Rep" +lemma Quotient_REP_ABS: + assumes a: "Quotient R Abs Rep" shows "R r r \ R (Rep (Abs r)) r" -using a unfolding QUOTIENT_def +using a unfolding Quotient_def by blast -lemma IDENTITY_EQUIV: - shows "EQUIV (op =)" -unfolding EQUIV_def +lemma IDENTITY_equivp: + shows "equivp (op =)" +unfolding equivp_def by auto -lemma IDENTITY_QUOTIENT: - shows "QUOTIENT (op =) id id" -unfolding QUOTIENT_def id_def +lemma IDENTITY_Quotient: + shows "Quotient (op =) id id" +unfolding Quotient_def id_def by blast -lemma QUOTIENT_SYM: - assumes a: "QUOTIENT E Abs Rep" - shows "SYM E" -using a unfolding QUOTIENT_def SYM_def +lemma Quotient_symp: + assumes a: "Quotient E Abs Rep" + shows "symp E" +using a unfolding Quotient_def symp_def by metis -lemma QUOTIENT_TRANS: - assumes a: "QUOTIENT E Abs Rep" - shows "TRANS E" -using a unfolding QUOTIENT_def TRANS_def +lemma Quotient_transp: + assumes a: "Quotient E Abs Rep" + shows "transp E" +using a unfolding Quotient_def transp_def by metis fun @@ -139,38 +143,38 @@ "(op =) ===> (op =) \ (op =)" by (rule eq_reflection) (simp add: expand_fun_eq) -lemma FUN_QUOTIENT: - assumes q1: "QUOTIENT R1 abs1 rep1" - and q2: "QUOTIENT R2 abs2 rep2" - shows "QUOTIENT (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)" +lemma FUN_Quotient: + assumes q1: "Quotient R1 abs1 rep1" + and q2: "Quotient R2 abs2 rep2" + shows "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)" proof - have "\a. (rep1 ---> abs2) ((abs1 ---> rep2) a) = a" apply(simp add: expand_fun_eq) using q1 q2 - apply(simp add: QUOTIENT_def) + apply(simp add: Quotient_def) done moreover have "\a. (R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)" apply(auto) - using q1 q2 unfolding QUOTIENT_def + using q1 q2 unfolding Quotient_def apply(metis) done moreover have "\r s. (R1 ===> R2) r s = ((R1 ===> R2) r r \ (R1 ===> R2) s s \ (rep1 ---> abs2) r = (rep1 ---> abs2) s)" apply(auto simp add: expand_fun_eq) - using q1 q2 unfolding QUOTIENT_def + using q1 q2 unfolding Quotient_def apply(metis) - using q1 q2 unfolding QUOTIENT_def + using q1 q2 unfolding Quotient_def apply(metis) - using q1 q2 unfolding QUOTIENT_def + using q1 q2 unfolding Quotient_def apply(metis) - using q1 q2 unfolding QUOTIENT_def + using q1 q2 unfolding Quotient_def apply(metis) done ultimately - show "QUOTIENT (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)" - unfolding QUOTIENT_def by blast + show "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)" + unfolding Quotient_def by blast qed definition @@ -195,11 +199,11 @@ by simp lemma RESPECTS_REP_ABS: - assumes a: "QUOTIENT R1 Abs1 Rep1" + 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 +using a b[simplified RESPECTS_THM] c unfolding Quotient_def by blast lemma RESPECTS_o: @@ -216,18 +220,18 @@ *) lemma FUN_REL_EQ_REL: - assumes q1: "QUOTIENT R1 Abs1 Rep1" - and q2: "QUOTIENT R2 Abs2 Rep2" + assumes q1: "Quotient R1 Abs1 Rep1" + and q2: "Quotient R2 Abs2 Rep2" shows "(R1 ===> R2) f g = ((Respects (R1 ===> R2) f) \ (Respects (R1 ===> R2) g) \ ((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g))" -using FUN_QUOTIENT[OF q1 q2] unfolding Respects_def QUOTIENT_def expand_fun_eq +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: - assumes q1: "QUOTIENT R1 Abs1 Rep1" - and q2: "QUOTIENT R2 Abs2 Rep2" + assumes q1: "Quotient R1 Abs1 Rep1" + and q2: "Quotient R2 Abs2 Rep2" shows "(R1 ===> R2) f g \ R1 x y \ R2 (f x) (g y)" by simp @@ -236,23 +240,23 @@ by simp lemma FUN_REL_EQUALS: - assumes q1: "QUOTIENT R1 Abs1 Rep1" - and q2: "QUOTIENT R2 Abs2 Rep2" + 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) = (\x y. R1 x y \ R2 (f x) (g y))" apply(rule_tac iffI) -using FUN_QUOTIENT[OF q1 q2] r1 r2 unfolding QUOTIENT_def Respects_def +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]) +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" + 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" @@ -260,56 +264,56 @@ 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 *) +(* 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" + assumes q: "Quotient R Abs Rep" shows "(x = y) = R (Rep x) (Rep y)" -by (rule QUOTIENT_REL_REP[OF q, symmetric]) +by (rule Quotient_REL_REP[OF q, symmetric]) lemma equals_rsp: - assumes q: "QUOTIENT R Abs Rep" + assumes q: "Quotient R Abs Rep" and a: "R xa xb" "R ya yb" shows "R xa ya = R xb yb" -using QUOTIENT_SYM[OF q] QUOTIENT_TRANS[OF q] unfolding SYM_def TRANS_def +using Quotient_symp[OF q] Quotient_transp[OF q] unfolding symp_def transp_def using a by blast lemma lambda_prs: - assumes q1: "QUOTIENT R1 Abs1 Rep1" - and q2: "QUOTIENT R2 Abs2 Rep2" + assumes q1: "Quotient R1 Abs1 Rep1" + and q2: "Quotient R2 Abs2 Rep2" shows "(Rep1 ---> Abs2) (\x. Rep2 (f (Abs1 x))) = (\x. f x)" unfolding expand_fun_eq -using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2] +using Quotient_ABS_REP[OF q1] Quotient_ABS_REP[OF q2] by simp lemma lambda_prs1: - assumes q1: "QUOTIENT R1 Abs1 Rep1" - and q2: "QUOTIENT R2 Abs2 Rep2" + assumes q1: "Quotient R1 Abs1 Rep1" + and q2: "Quotient R2 Abs2 Rep2" shows "(Rep1 ---> Abs2) (\x. (Abs1 ---> Rep2) f x) = (\x. f x)" unfolding expand_fun_eq -using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2] +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" + 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] +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" + assumes q1: "Quotient R1 Abs1 Rep1" + and q2: "Quotient R2 Abs2 Rep2" and a: "(R1 ===> R2) f1 f2" shows "(R1 ===> R2) (\x. f1 x) (\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" + assumes q1: "Quotient R1 Abs1 Rep1" + and q2: "Quotient R2 Abs2 Rep2" shows "f = (Rep1 ---> Abs2) ???" *) @@ -320,17 +324,17 @@ using r1 r2 by auto lemma REP_ABS_RSP: - assumes q: "QUOTIENT R Abs Rep" + 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]) +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: - assumes q: "QUOTIENT R Abs Rep" + 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]) +using q a by (metis Quotient_REL[OF q] Quotient_ABS_REP[OF q] Quotient_REP_reflp[OF q]) (* ----------------------------------------------------- *) (* Quantifiers: FORALL, EXISTS, EXISTS_UNIQUE, *) @@ -340,26 +344,26 @@ (* bool theory: COND, LET *) lemma IF_PRS: - assumes q: "QUOTIENT R Abs Rep" + assumes q: "Quotient R Abs Rep" shows "If a b c = Abs (If a (Rep b) (Rep c))" -using QUOTIENT_ABS_REP[OF q] by auto +using Quotient_ABS_REP[OF q] by auto (* ask peter: no use of q *) lemma IF_RSP: - assumes q: "QUOTIENT R Abs Rep" + assumes q: "Quotient R Abs Rep" and a: "a1 = a2" "R b1 b2" "R c1 c2" shows "R (If a1 b1 c1) (If a2 b2 c2)" using a by auto lemma LET_PRS: - assumes q1: "QUOTIENT R1 Abs1 Rep1" - and q2: "QUOTIENT R2 Abs2 Rep2" + assumes q1: "Quotient R1 Abs1 Rep1" + and q2: "Quotient R2 Abs2 Rep2" shows "Let x f = Abs2 (Let (Rep1 x) ((Abs1 ---> Rep2) f))" -using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2] by auto +using Quotient_ABS_REP[OF q1] Quotient_ABS_REP[OF q2] by auto lemma LET_RSP: - assumes q1: "QUOTIENT R1 Abs1 Rep1" - and q2: "QUOTIENT R2 Abs2 Rep2" + assumes q1: "Quotient R1 Abs1 Rep1" + and q2: "Quotient R2 Abs2 Rep2" and a1: "(R1 ===> R2) f g" and a2: "R1 x y" shows "R2 (Let x f) (Let y g)" @@ -376,17 +380,17 @@ (* Not used *) lemma APPLY_PRS: - assumes q1: "QUOTIENT R1 Abs1 Rep1" - and q2: "QUOTIENT R2 Abs2 Rep2" + 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 +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 + so by solving Quotient assumptions we can get a unique R2 that will be provable; which is why we need to use APPLY_RSP *) lemma apply_rsp: - assumes q: "QUOTIENT R1 Abs1 Rep1" + assumes q: "Quotient R1 Abs1 Rep1" and a: "(R1 ===> R2) f g" "R1 x y" shows "R2 ((f::'a\'c) x) ((g::'a\'c) y)" using a by (rule FUN_REL_IMP) @@ -401,29 +405,29 @@ (* We use id_simps which includes id_apply; so these 2 theorems can be removed *) lemma I_PRS: - assumes q: "QUOTIENT R Abs Rep" + assumes q: "Quotient R Abs Rep" shows "id e = Abs (id (Rep e))" -using QUOTIENT_ABS_REP[OF q] by auto +using Quotient_ABS_REP[OF q] by auto lemma I_RSP: - assumes q: "QUOTIENT R Abs Rep" + assumes q: "Quotient R Abs Rep" and a: "R e1 e2" shows "R (id e1) (id e2)" using a by auto lemma o_PRS: - assumes q1: "QUOTIENT R1 Abs1 Rep1" - and q2: "QUOTIENT R2 Abs2 Rep2" - and q3: "QUOTIENT R3 Abs3 Rep3" + assumes q1: "Quotient R1 Abs1 Rep1" + and q2: "Quotient R2 Abs2 Rep2" + and q3: "Quotient R3 Abs3 Rep3" shows "f o g = (Rep1 ---> Abs3) (((Abs2 ---> Rep3) f) o ((Abs1 ---> Rep2) g))" -using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2] QUOTIENT_ABS_REP[OF q3] +using Quotient_ABS_REP[OF q1] Quotient_ABS_REP[OF q2] Quotient_ABS_REP[OF q3] unfolding o_def expand_fun_eq by simp lemma o_RSP: - assumes q1: "QUOTIENT R1 Abs1 Rep1" - and q2: "QUOTIENT R2 Abs2 Rep2" - and q3: "QUOTIENT R3 Abs3 Rep3" + assumes q1: "Quotient R1 Abs1 Rep1" + and q2: "Quotient R2 Abs2 Rep2" + and q3: "Quotient R3 Abs3 Rep3" and a1: "(R2 ===> R3) f1 f2" and a2: "(R1 ===> R2) g1 g2" shows "(R1 ===> R3) (f1 o g1) (f2 o g2)" @@ -435,9 +439,9 @@ lemma COND_PRS: - assumes a: "QUOTIENT R absf repf" + assumes a: "Quotient R absf repf" shows "(if a then b else c) = absf (if a then repf b else repf c)" - using a unfolding QUOTIENT_def by auto + using a unfolding Quotient_def by auto @@ -446,15 +450,15 @@ (* Set of lemmas for regularisation of ball and bex *) lemma ball_reg_eqv: fixes P :: "'a \ bool" - assumes a: "EQUIV R" + assumes a: "equivp R" shows "Ball (Respects R) P = (All P)" - by (metis EQUIV_def IN_RESPECTS a) + by (metis equivp_def IN_RESPECTS a) lemma bex_reg_eqv: fixes P :: "'a \ bool" - assumes a: "EQUIV R" + assumes a: "equivp R" shows "Bex (Respects R) P = (Ex P)" - by (metis EQUIV_def IN_RESPECTS a) + by (metis equivp_def IN_RESPECTS a) lemma ball_reg_right: assumes a: "\x. R x \ P x \ Q x" @@ -467,27 +471,27 @@ by (metis COMBC_def Collect_def Collect_mem_eq a) lemma ball_reg_left: - assumes a: "EQUIV R" + assumes a: "equivp R" shows "(\x. (Q x \ P x)) \ Ball (Respects R) Q \ All P" - by (metis EQUIV_REFL IN_RESPECTS a) + by (metis equivp_reflp IN_RESPECTS a) lemma bex_reg_right: - assumes a: "EQUIV R" + assumes a: "equivp R" shows "(\x. (Q x \ P x)) \ Ex Q \ Bex (Respects R) P" - by (metis EQUIV_REFL IN_RESPECTS a) + by (metis equivp_reflp IN_RESPECTS a) lemma ball_reg_eqv_range: fixes P::"'a \ bool" and x::"'a" - assumes a: "EQUIV R2" + assumes a: "equivp R2" shows "(Ball (Respects (R1 ===> R2)) (\f. P (f x)) = All (\f. P (f x)))" apply(rule iffI) apply(rule allI) apply(drule_tac x="\y. f x" in bspec) apply(simp add: Respects_def IN_RESPECTS) apply(rule impI) - using a EQUIV_REFL_SYM_TRANS[of "R2"] - apply(simp add: REFL_def) + using a equivp_reflp_symp_transp[of "R2"] + apply(simp add: reflp_def) apply(simp) apply(simp) done @@ -495,15 +499,15 @@ lemma bex_reg_eqv_range: fixes P::"'a \ bool" and x::"'a" - assumes a: "EQUIV R2" + assumes a: "equivp R2" shows "(Bex (Respects (R1 ===> R2)) (\f. P (f x)) = Ex (\f. P (f x)))" apply(auto) apply(rule_tac x="\y. f x" in bexI) apply(simp) apply(simp add: Respects_def IN_RESPECTS) apply(rule impI) - using a EQUIV_REFL_SYM_TRANS[of "R2"] - apply(simp add: REFL_def) + using a equivp_reflp_symp_transp[of "R2"] + apply(simp add: reflp_def) done lemma all_reg: @@ -551,15 +555,15 @@ (* 2 lemmas needed for cleaning of quantifiers *) lemma all_prs: - assumes a: "QUOTIENT R absf repf" + assumes a: "Quotient R absf repf" shows "Ball (Respects R) ((absf ---> id) f) = All f" - using a unfolding QUOTIENT_def + using a unfolding Quotient_def by (metis IN_RESPECTS fun_map.simps id_apply) lemma ex_prs: - assumes a: "QUOTIENT R absf repf" + assumes a: "Quotient R absf repf" shows "Bex (Respects R) ((absf ---> id) f) = Ex f" - using a unfolding QUOTIENT_def + using a unfolding Quotient_def by (metis COMBC_def Collect_def Collect_mem_eq IN_RESPECTS fun_map.simps id_apply) end