# HG changeset patch # User Cezary Kaliszyk # Date 1259938257 -3600 # Node ID 57073b0b8fac7bf55b6e29498147ea41f2ce66d9 # Parent 44fa9df44e6f04b2faffa0bfd2ffaa6d0ac93bdc Even more name changes and cleaning diff -r 44fa9df44e6f -r 57073b0b8fac IntEx.thy --- a/IntEx.thy Fri Dec 04 15:41:09 2009 +0100 +++ b/IntEx.thy Fri Dec 04 15:50:57 2009 +0100 @@ -1,7 +1,6 @@ theory IntEx imports QuotMain begin - fun intrel :: "(nat \ nat) \ (nat \ nat) \ bool" (infix "\" 50) @@ -237,12 +236,12 @@ by (simp_all add: Quotient_ABS_REP[OF a]) lemma cons_rsp[quotient_rsp]: - "(op \ ===> LIST_REL op \ ===> LIST_REL op \) op # op #" + "(op \ ===> list_rel op \ ===> list_rel op \) op # op #" by simp (* I believe it's true. *) lemma foldl_rsp[quotient_rsp]: - "((op \ ===> op \ ===> op \) ===> op \ ===> LIST_REL op \ ===> op \) foldl foldl" + "((op \ ===> op \ ===> op \) ===> op \ ===> list_rel op \ ===> op \) foldl foldl" apply (simp only: fun_rel.simps) apply (rule allI) apply (rule allI) @@ -257,7 +256,7 @@ sorry lemma nil_listrel_rsp[quotient_rsp]: - "(LIST_REL R) [] []" + "(list_rel R) [] []" by simp lemma "foldl PLUS x [] = x" diff -r 44fa9df44e6f -r 57073b0b8fac QuotList.thy --- a/QuotList.thy Fri Dec 04 15:41:09 2009 +0100 +++ b/QuotList.thy Fri Dec 04 15:50:57 2009 +0100 @@ -7,15 +7,15 @@ by simp fun - LIST_REL + list_rel where - "LIST_REL R [] [] = True" -| "LIST_REL R (x#xs) [] = False" -| "LIST_REL R [] (x#xs) = False" -| "LIST_REL R (x#xs) (y#ys) = (R x y \ LIST_REL R xs ys)" + "list_rel R [] [] = True" +| "list_rel R (x#xs) [] = False" +| "list_rel R [] (x#xs) = False" +| "list_rel R (x#xs) (y#ys) = (R x y \ list_rel R xs ys)" -lemma LIST_REL_EQ: - shows "LIST_REL (op =) \ (op =)" +lemma list_rel_EQ: + shows "list_rel (op =) \ (op =)" apply(rule eq_reflection) unfolding expand_fun_eq apply(rule allI)+ @@ -23,22 +23,22 @@ 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" + shows "list_rel R x x" by (induct x) (auto simp add: a) lemma LIST_equivp: assumes a: "equivp R" - shows "equivp (LIST_REL R)" + shows "equivp (list_rel R)" unfolding equivp_def apply(rule allI)+ apply(induct_tac x y rule: list_induct2') apply(simp) apply(simp add: expand_fun_eq) -apply(metis LIST_REL.simps(1) LIST_REL.simps(2)) +apply(metis list_rel.simps(1) list_rel.simps(2)) apply(simp add: expand_fun_eq) -apply(metis LIST_REL.simps(1) LIST_REL.simps(2)) +apply(metis list_rel.simps(1) list_rel.simps(2)) apply(simp add: expand_fun_eq) apply(rule iffI) apply(rule allI) @@ -48,21 +48,21 @@ using a apply(unfold equivp_def) apply(auto)[1] -apply(metis LIST_REL.simps(4)) +apply(metis list_rel.simps(4)) done -lemma LIST_REL_REL: +lemma list_rel_REL: assumes q: "Quotient R Abs Rep" - shows "LIST_REL R r s = (LIST_REL R r r \ LIST_REL R s s \ (map Abs r = map Abs s))" + shows "list_rel R r s = (list_rel R r r \ list_rel R s s \ (map Abs r = map Abs s))" apply(induct r s rule: list_induct2') apply(simp_all) using Quotient_REL[OF q] apply(metis) done -lemma LIST_Quotient: +lemma list_quotient: assumes q: "Quotient R Abs Rep" - shows "Quotient (LIST_REL R) (map Abs) (map Rep)" + shows "Quotient (list_rel R) (map Abs) (map Rep)" unfolding Quotient_def apply(rule conjI) apply(rule allI) @@ -76,7 +76,7 @@ apply(simp) apply(simp add: Quotient_REP_reflp[OF q]) apply(rule allI)+ -apply(rule LIST_REL_REL[OF q]) +apply(rule list_rel_REL[OF q]) done lemma CONS_PRS: @@ -86,8 +86,8 @@ lemma CONS_RSP: assumes q: "Quotient R Abs Rep" - and a: "R h1 h2" "LIST_REL R t1 t2" - shows "LIST_REL R (h1#t1) (h2#t2)" + and a: "R h1 h2" "list_rel R t1 t2" + shows "list_rel R (h1#t1) (h2#t2)" using a by (auto) lemma NIL_PRS: @@ -97,7 +97,7 @@ lemma NIL_RSP: assumes q: "Quotient R Abs Rep" - shows "LIST_REL R [] []" + shows "list_rel R [] []" by simp lemma MAP_PRS: @@ -110,9 +110,9 @@ lemma MAP_RSP: assumes q1: "Quotient R1 Abs1 Rep1" and q2: "Quotient R2 Abs2 Rep2" - and a: "(R1 ===> R2) f1 f2" - and b: "LIST_REL R1 l1 l2" - shows "LIST_REL R2 (map f1 l1) (map f2 l2)" + and a: "(R1 ===> R2) f1 f2" + and b: "list_rel R1 l1 l2" + shows "list_rel R2 (map f1 l1) (map f2 l2)" using b a by (induct l1 l2 rule: list_induct2') (simp_all) diff -r 44fa9df44e6f -r 57073b0b8fac QuotMain.thy --- a/QuotMain.thy Fri Dec 04 15:41:09 2009 +0100 +++ b/QuotMain.thy Fri Dec 04 15:50:57 2009 +0100 @@ -141,12 +141,12 @@ (* the auxiliary data for the quotient types *) use "quotient_info.ML" -declare [[map list = (map, LIST_REL)]] +declare [[map list = (map, list_rel)]] declare [[map * = (prod_fun, prod_rel)]] declare [[map "fun" = (fun_map, fun_rel)]] -lemmas [quotient_thm] = - FUN_Quotient LIST_Quotient +lemmas [quotient_thm] = + fun_quotient list_quotient ML {* maps_lookup @{theory} "List.list" *} ML {* maps_lookup @{theory} "*" *} @@ -214,7 +214,7 @@ done lemmas id_simps = - FUN_MAP_I[THEN eq_reflection] + fun_map_id[THEN eq_reflection] id_apply[THEN eq_reflection] id_def[THEN eq_reflection,symmetric] prod_fun_id map_id @@ -610,7 +610,7 @@ val simproc3 = Simplifier.simproc_i thy "" pat3 (K (ball_reg_eqv_range_simproc rel_eqvs)) val simproc4 = Simplifier.simproc_i thy "" pat4 (K (bex_reg_eqv_range_simproc rel_eqvs)) val simp_ctxt = (Simplifier.context ctxt empty_ss) addsimprocs [simproc1, simproc2, simproc3, simproc4] - (* TODO: Make sure that there are no LIST_REL, PAIR_REL etc involved *) + (* TODO: Make sure that there are no list_rel, pair_rel etc involved *) val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) rel_eqvs in ObjectLogic.full_atomize_tac THEN' diff -r 44fa9df44e6f -r 57073b0b8fac QuotScript.thy --- a/QuotScript.thy Fri Dec 04 15:41:09 2009 +0100 +++ b/QuotScript.thy Fri Dec 04 15:50:57 2009 +0100 @@ -121,11 +121,12 @@ where "f ---> g \ fun_map f g" -lemma FUN_MAP_I: +lemma fun_map_id: shows "(id ---> id) = id" by (simp add: expand_fun_eq id_def) -lemma IN_FUN: +(* Not used *) +lemma in_fun: shows "x \ ((f ---> g) s) = g (f x \ s)" by (simp add: mem_def) @@ -143,7 +144,7 @@ "(op =) ===> (op =) \ (op =)" by (rule eq_reflection) (simp add: expand_fun_eq) -lemma FUN_Quotient: +lemma fun_quotient: assumes q1: "Quotient R1 abs1 rep1" and q2: "Quotient R2 abs2 rep2" shows "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)" @@ -224,7 +225,7 @@ 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 *) @@ -246,7 +247,7 @@ 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))