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)