26 lemma LIST_REL_REFL: |
26 lemma LIST_REL_REFL: |
27 assumes a: "\<And>x y. R x y = (R x = R y)" |
27 assumes a: "\<And>x y. R x y = (R x = R y)" |
28 shows "LIST_REL R x x" |
28 shows "LIST_REL R x x" |
29 by (induct x) (auto simp add: a) |
29 by (induct x) (auto simp add: a) |
30 |
30 |
31 lemma LIST_EQUIV: |
31 lemma LIST_equivp: |
32 assumes a: "EQUIV R" |
32 assumes a: "equivp R" |
33 shows "EQUIV (LIST_REL R)" |
33 shows "equivp (LIST_REL R)" |
34 unfolding EQUIV_def |
34 unfolding equivp_def |
35 apply(rule allI)+ |
35 apply(rule allI)+ |
36 apply(induct_tac x y rule: list_induct2') |
36 apply(induct_tac x y rule: list_induct2') |
37 apply(simp) |
37 apply(simp) |
38 apply(simp add: expand_fun_eq) |
38 apply(simp add: expand_fun_eq) |
39 apply(metis LIST_REL.simps(1) LIST_REL.simps(2)) |
39 apply(metis LIST_REL.simps(1) LIST_REL.simps(2)) |
44 apply(rule allI) |
44 apply(rule allI) |
45 apply(case_tac x) |
45 apply(case_tac x) |
46 apply(simp) |
46 apply(simp) |
47 apply(simp) |
47 apply(simp) |
48 using a |
48 using a |
49 apply(unfold EQUIV_def) |
49 apply(unfold equivp_def) |
50 apply(auto)[1] |
50 apply(auto)[1] |
51 apply(metis LIST_REL.simps(4)) |
51 apply(metis LIST_REL.simps(4)) |
52 done |
52 done |
53 |
53 |
54 lemma LIST_REL_REL: |
54 lemma LIST_REL_REL: |
55 assumes q: "QUOTIENT R Abs Rep" |
55 assumes q: "Quotient R Abs Rep" |
56 shows "LIST_REL R r s = (LIST_REL R r r \<and> LIST_REL R s s \<and> (map Abs r = map Abs s))" |
56 shows "LIST_REL R r s = (LIST_REL R r r \<and> LIST_REL R s s \<and> (map Abs r = map Abs s))" |
57 apply(induct r s rule: list_induct2') |
57 apply(induct r s rule: list_induct2') |
58 apply(simp_all) |
58 apply(simp_all) |
59 using QUOTIENT_REL[OF q] |
59 using Quotient_REL[OF q] |
60 apply(metis) |
60 apply(metis) |
61 done |
61 done |
62 |
62 |
63 lemma LIST_QUOTIENT: |
63 lemma LIST_Quotient: |
64 assumes q: "QUOTIENT R Abs Rep" |
64 assumes q: "Quotient R Abs Rep" |
65 shows "QUOTIENT (LIST_REL R) (map Abs) (map Rep)" |
65 shows "Quotient (LIST_REL R) (map Abs) (map Rep)" |
66 unfolding QUOTIENT_def |
66 unfolding Quotient_def |
67 apply(rule conjI) |
67 apply(rule conjI) |
68 apply(rule allI) |
68 apply(rule allI) |
69 apply(induct_tac a) |
69 apply(induct_tac a) |
70 apply(simp) |
70 apply(simp) |
71 apply(simp add: QUOTIENT_ABS_REP[OF q]) |
71 apply(simp add: Quotient_ABS_REP[OF q]) |
72 apply(rule conjI) |
72 apply(rule conjI) |
73 apply(rule allI) |
73 apply(rule allI) |
74 apply(induct_tac a) |
74 apply(induct_tac a) |
75 apply(simp) |
75 apply(simp) |
76 apply(simp) |
76 apply(simp) |
77 apply(simp add: QUOTIENT_REP_REFL[OF q]) |
77 apply(simp add: Quotient_REP_reflp[OF q]) |
78 apply(rule allI)+ |
78 apply(rule allI)+ |
79 apply(rule LIST_REL_REL[OF q]) |
79 apply(rule LIST_REL_REL[OF q]) |
80 done |
80 done |
81 |
81 |
82 lemma CONS_PRS: |
82 lemma CONS_PRS: |
83 assumes q: "QUOTIENT R Abs Rep" |
83 assumes q: "Quotient R Abs Rep" |
84 shows "(h#t) = (map Abs) ((Rep h)#(map Rep t))" |
84 shows "(h#t) = (map Abs) ((Rep h)#(map Rep t))" |
85 by (induct t) (simp_all add: QUOTIENT_ABS_REP[OF q]) |
85 by (induct t) (simp_all add: Quotient_ABS_REP[OF q]) |
86 |
86 |
87 lemma CONS_RSP: |
87 lemma CONS_RSP: |
88 assumes q: "QUOTIENT R Abs Rep" |
88 assumes q: "Quotient R Abs Rep" |
89 and a: "R h1 h2" "LIST_REL R t1 t2" |
89 and a: "R h1 h2" "LIST_REL R t1 t2" |
90 shows "LIST_REL R (h1#t1) (h2#t2)" |
90 shows "LIST_REL R (h1#t1) (h2#t2)" |
91 using a by (auto) |
91 using a by (auto) |
92 |
92 |
93 lemma NIL_PRS: |
93 lemma NIL_PRS: |
94 assumes q: "QUOTIENT R Abs Rep" |
94 assumes q: "Quotient R Abs Rep" |
95 shows "[] = (map Abs [])" |
95 shows "[] = (map Abs [])" |
96 by (simp) |
96 by (simp) |
97 |
97 |
98 lemma NIL_RSP: |
98 lemma NIL_RSP: |
99 assumes q: "QUOTIENT R Abs Rep" |
99 assumes q: "Quotient R Abs Rep" |
100 shows "LIST_REL R [] []" |
100 shows "LIST_REL R [] []" |
101 by simp |
101 by simp |
102 |
102 |
103 lemma MAP_PRS: |
103 lemma MAP_PRS: |
104 assumes q1: "QUOTIENT R1 Abs1 Rep1" |
104 assumes q1: "Quotient R1 Abs1 Rep1" |
105 and q2: "QUOTIENT R2 Abs2 Rep2" |
105 and q2: "Quotient R2 Abs2 Rep2" |
106 shows "map f l = (map Abs2) (map ((Abs1 ---> Rep2) f) (map Rep1 l))" |
106 shows "map f l = (map Abs2) (map ((Abs1 ---> Rep2) f) (map Rep1 l))" |
107 by (induct l) |
107 by (induct l) |
108 (simp_all add: QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2]) |
108 (simp_all add: Quotient_ABS_REP[OF q1] Quotient_ABS_REP[OF q2]) |
109 |
109 |
110 lemma MAP_RSP: |
110 lemma MAP_RSP: |
111 assumes q1: "QUOTIENT R1 Abs1 Rep1" |
111 assumes q1: "Quotient R1 Abs1 Rep1" |
112 and q2: "QUOTIENT R2 Abs2 Rep2" |
112 and q2: "Quotient R2 Abs2 Rep2" |
113 and a: "(R1 ===> R2) f1 f2" |
113 and a: "(R1 ===> R2) f1 f2" |
114 and b: "LIST_REL R1 l1 l2" |
114 and b: "LIST_REL R1 l1 l2" |
115 shows "LIST_REL R2 (map f1 l1) (map f2 l2)" |
115 shows "LIST_REL R2 (map f1 l1) (map f2 l2)" |
116 using b a |
116 using b a |
117 by (induct l1 l2 rule: list_induct2') |
117 by (induct l1 l2 rule: list_induct2') |