# HG changeset patch # User Cezary Kaliszyk # Date 1259941991 -3600 # Node ID 94deffed619dba2236174b2ab0cd810f74c228ac # Parent c0b13fb70d6d7a49c7e0f6e780382eb834874162 more name cleaning and removing diff -r c0b13fb70d6d -r 94deffed619d LFex.thy --- a/LFex.thy Fri Dec 04 16:40:23 2009 +0100 +++ b/LFex.thy Fri Dec 04 16:53:11 2009 +0100 @@ -219,9 +219,7 @@ ML {* val quot = @{thms Quotient_KIND Quotient_TY Quotient_TRM} val rel_refl = map (fn x => @{thm equivp_reflp} OF [x]) @{thms alpha_equivps} - (*val trans2 = map (fn x => @{thm EQUALS_PRS} OF [x]) quot*) - val reps_same = map (fn x => @{thm Quotient_REL_REP} OF [x]) quot - val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same + val reps_same = map (fn x => @{thm Quotient_rel_rep} OF [x]) quot *} lemma diff -r c0b13fb70d6d -r 94deffed619d QuotList.thy --- a/QuotList.thy Fri Dec 04 16:40:23 2009 +0100 +++ b/QuotList.thy Fri Dec 04 16:53:11 2009 +0100 @@ -52,7 +52,7 @@ apply(induct_tac a) apply(simp) apply(simp) - apply(simp add: Quotient_REP_reflp[OF q]) + apply(simp add: Quotient_rep_reflp[OF q]) apply(rule allI)+ apply(rule list_rel_rel[OF q]) done @@ -114,11 +114,11 @@ (* TODO: Rest are unused *) -lemma LIST_map_id: +lemma list_map_id: shows "map (\x. x) = (\x. x)" by simp -lemma list_rel_EQ: +lemma list_rel_eq: shows "list_rel (op =) \ (op =)" apply(rule eq_reflection) unfolding expand_fun_eq @@ -127,10 +127,9 @@ apply(simp_all) done -lemma list_rel_REFL: +lemma list_rel_refl: assumes a: "\x y. R x y = (R x = R y)" shows "list_rel R x x" by (induct x) (auto simp add: a) - end diff -r c0b13fb70d6d -r 94deffed619d QuotMain.thy --- a/QuotMain.thy Fri Dec 04 16:40:23 2009 +0100 +++ b/QuotMain.thy Fri Dec 04 16:53:11 2009 +0100 @@ -1062,7 +1062,7 @@ - Rewriting with definitions from the argument defs NewConst ----> (rep ---> abs) oldConst - - Quotient_REL_REP: + - Quotient_rel_rep: Rel (Rep x) (Rep y) ----> x = y - ABS_REP @@ -1082,11 +1082,9 @@ val quotients = quotient_rules_get lthy val defs = map (Thm.varifyT o #def) (qconsts_dest thy); val absrep = map (fn x => @{thm Quotient_abs_rep} OF [x]) quotients - val meta_absrep = map (fn x => @{thm eq_reflection} OF [x]) absrep; - val reps_same = map (fn x => @{thm Quotient_REL_REP} OF [x]) quotients - val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same + val reps_same = map (fn x => @{thm Quotient_rel_rep} OF [x]) quotients val simp_ctxt = (Simplifier.context lthy empty_ss) addsimps - (@{thm eq_reflection[OF fun_map.simps]} :: @{thms id_simps} @ meta_absrep @ meta_reps_same @ defs) + (@{thm eq_reflection[OF fun_map.simps]} :: @{thms id_simps} @ absrep @ reps_same @ defs) in EVERY' [ (* (Rep1 ---> Abs2) (\x. Rep2 (f (Abs1 x))) ----> f *) diff -r c0b13fb70d6d -r 94deffed619d QuotScript.thy --- a/QuotScript.thy Fri Dec 04 16:40:23 2009 +0100 +++ b/QuotScript.thy Fri Dec 04 16:53:11 2009 +0100 @@ -28,12 +28,12 @@ by (simp add: equivp_reflp_symp_transp reflp_def) definition - "PART_equivp 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 equivp_IMP_PART_equivp: +lemma equivp_IMP_part_equivp: assumes a: "equivp E" - shows "PART_equivp E" -using a unfolding equivp_def PART_equivp_def + shows "part_equivp E" +using a unfolding equivp_def part_equivp_def by auto definition @@ -47,9 +47,9 @@ using a unfolding Quotient_def by simp -lemma Quotient_REP_reflp: +lemma Quotient_rep_reflp: assumes a: "Quotient E Abs Rep" - shows "E (Rep a) (Rep a)" + shows "E (Rep a) (Rep a)" using a unfolding Quotient_def by blast @@ -59,21 +59,10 @@ using a unfolding Quotient_def by blast -lemma Quotient_REL_ABS: - assumes a: "Quotient E Abs Rep" - shows "E r s \ Abs r = Abs s" -using a unfolding Quotient_def -by blast - -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 -by blast - -lemma Quotient_REL_REP: +lemma Quotient_rel_rep: assumes a: "Quotient R Abs Rep" - shows "R (Rep a) (Rep b) = (a = b)" + shows "R (Rep a) (Rep b) \ (a = b)" +apply (rule eq_reflection) using a unfolding Quotient_def by metis @@ -251,7 +240,7 @@ 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 *) @@ -265,12 +254,6 @@ 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 (rule Quotient_REL_REP[OF q, symmetric]) - lemma equals_rsp: assumes q: "Quotient R Abs Rep" and a: "R xa xb" "R ya yb" @@ -328,14 +311,14 @@ 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]) +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" 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]) +using q a by (metis Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q]) (* ----------------------------------------------------- *) (* Quantifiers: FORALL, EXISTS, EXISTS_UNIQUE, *) @@ -567,5 +550,21 @@ using a unfolding Quotient_def by (metis COMBC_def Collect_def Collect_mem_eq IN_RESPECTS fun_map.simps id_apply) + +(* UNUSED *) +lemma Quotient_rel_abs: + assumes a: "Quotient E Abs Rep" + shows "E r s \ Abs r = Abs s" +using a unfolding Quotient_def +by blast + +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 +by blast + + + end