1 theory QuotList |
1 theory QuotList |
2 imports QuotScript List |
2 imports QuotScript List |
3 begin |
3 begin |
4 |
|
5 lemma LIST_map_id: |
|
6 shows "map (\<lambda>x. x) = (\<lambda>x. x)" |
|
7 by simp |
|
8 |
4 |
9 fun |
5 fun |
10 list_rel |
6 list_rel |
11 where |
7 where |
12 "list_rel R [] [] = True" |
8 "list_rel R [] [] = True" |
13 | "list_rel R (x#xs) [] = False" |
9 | "list_rel R (x#xs) [] = False" |
14 | "list_rel R [] (x#xs) = False" |
10 | "list_rel R [] (x#xs) = False" |
15 | "list_rel R (x#xs) (y#ys) = (R x y \<and> list_rel R xs ys)" |
11 | "list_rel R (x#xs) (y#ys) = (R x y \<and> list_rel R xs ys)" |
16 |
12 |
17 lemma list_rel_EQ: |
13 lemma list_equivp: |
18 shows "list_rel (op =) \<equiv> (op =)" |
|
19 apply(rule eq_reflection) |
|
20 unfolding expand_fun_eq |
|
21 apply(rule allI)+ |
|
22 apply(induct_tac x xa rule: list_induct2') |
|
23 apply(simp_all) |
|
24 done |
|
25 |
|
26 lemma list_rel_REFL: |
|
27 assumes a: "\<And>x y. R x y = (R x = R y)" |
|
28 shows "list_rel R x x" |
|
29 by (induct x) (auto simp add: a) |
|
30 |
|
31 lemma LIST_equivp: |
|
32 assumes a: "equivp R" |
14 assumes a: "equivp R" |
33 shows "equivp (list_rel R)" |
15 shows "equivp (list_rel R)" |
34 unfolding equivp_def |
16 unfolding equivp_def |
35 apply(rule allI)+ |
17 apply(rule allI)+ |
36 apply(induct_tac x y rule: list_induct2') |
18 apply(induct_tac x y rule: list_induct2') |
37 apply(simp) |
19 apply(simp_all add: expand_fun_eq) |
38 apply(simp add: expand_fun_eq) |
20 apply(metis list_rel.simps(1) list_rel.simps(2)) |
39 apply(metis list_rel.simps(1) list_rel.simps(2)) |
21 apply(metis list_rel.simps(1) list_rel.simps(2)) |
40 apply(simp add: expand_fun_eq) |
22 apply(rule iffI) |
41 apply(metis list_rel.simps(1) list_rel.simps(2)) |
23 apply(rule allI) |
42 apply(simp add: expand_fun_eq) |
24 apply(case_tac x) |
43 apply(rule iffI) |
25 apply(simp_all) |
44 apply(rule allI) |
26 using a |
45 apply(case_tac x) |
27 apply(unfold equivp_def) |
46 apply(simp) |
28 apply(auto)[1] |
47 apply(simp) |
29 apply(metis list_rel.simps(4)) |
48 using a |
30 done |
49 apply(unfold equivp_def) |
|
50 apply(auto)[1] |
|
51 apply(metis list_rel.simps(4)) |
|
52 done |
|
53 |
31 |
54 lemma list_rel_REL: |
32 lemma list_rel_rel: |
55 assumes q: "Quotient R Abs Rep" |
33 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))" |
34 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') |
35 apply(induct r s rule: list_induct2') |
58 apply(simp_all) |
36 apply(simp_all) |
59 using Quotient_REL[OF q] |
37 using Quotient_rel[OF q] |
60 apply(metis) |
38 apply(metis) |
61 done |
39 done |
62 |
40 |
63 lemma list_quotient: |
41 lemma list_quotient: |
64 assumes q: "Quotient R Abs Rep" |
42 assumes q: "Quotient R Abs Rep" |
65 shows "Quotient (list_rel R) (map Abs) (map Rep)" |
43 shows "Quotient (list_rel R) (map Abs) (map Rep)" |
66 unfolding Quotient_def |
44 unfolding Quotient_def |
67 apply(rule conjI) |
45 apply(rule conjI) |
68 apply(rule allI) |
46 apply(rule allI) |
69 apply(induct_tac a) |
47 apply(induct_tac a) |
70 apply(simp) |
48 apply(simp) |
71 apply(simp add: Quotient_ABS_REP[OF q]) |
49 apply(simp add: Quotient_ABS_REP[OF q]) |
72 apply(rule conjI) |
50 apply(rule conjI) |
73 apply(rule allI) |
51 apply(rule allI) |
74 apply(induct_tac a) |
52 apply(induct_tac a) |
75 apply(simp) |
53 apply(simp) |
76 apply(simp) |
54 apply(simp) |
77 apply(simp add: Quotient_REP_reflp[OF q]) |
55 apply(simp add: Quotient_REP_reflp[OF q]) |
78 apply(rule allI)+ |
56 apply(rule allI)+ |
79 apply(rule list_rel_REL[OF q]) |
57 apply(rule list_rel_rel[OF q]) |
80 done |
58 done |
|
59 |
|
60 |
|
61 |
|
62 |
|
63 |
|
64 |
|
65 (* Rest is not used *) |
|
66 |
81 |
67 |
82 lemma CONS_PRS: |
68 lemma CONS_PRS: |
83 assumes q: "Quotient R Abs Rep" |
69 assumes q: "Quotient R Abs Rep" |
84 shows "(h#t) = (map Abs) ((Rep h)#(map Rep t))" |
70 shows "(h#t) = (map Abs) ((Rep h)#(map Rep t))" |
85 by (induct t) (simp_all add: Quotient_ABS_REP[OF q]) |
71 by (induct t) (simp_all add: Quotient_ABS_REP[OF q]) |
116 using b a |
102 using b a |
117 by (induct l1 l2 rule: list_induct2') |
103 by (induct l1 l2 rule: list_induct2') |
118 (simp_all) |
104 (simp_all) |
119 |
105 |
120 |
106 |
|
107 |
|
108 lemma LIST_map_id: |
|
109 shows "map (\<lambda>x. x) = (\<lambda>x. x)" |
|
110 by simp |
|
111 |
|
112 lemma list_rel_EQ: |
|
113 shows "list_rel (op =) \<equiv> (op =)" |
|
114 apply(rule eq_reflection) |
|
115 unfolding expand_fun_eq |
|
116 apply(rule allI)+ |
|
117 apply(induct_tac x xa rule: list_induct2') |
|
118 apply(simp_all) |
|
119 done |
|
120 |
|
121 lemma list_rel_REFL: |
|
122 assumes a: "\<And>x y. R x y = (R x = R y)" |
|
123 shows "list_rel R x x" |
|
124 by (induct x) (auto simp add: a) |
|
125 |
|
126 |
121 end |
127 end |
122 |
|
123 (* |
|
124 val LENGTH_PRS = store_thm |
|
125 ("LENGTH_PRS", |
|
126 (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> |
|
127 !l. LENGTH l = LENGTH (MAP rep l)--), |
|
128 |
|
129 val LENGTH_RSP = store_thm |
|
130 ("LENGTH_RSP", |
|
131 (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> |
|
132 !l1 l2. |
|
133 (LIST_REL R) l1 l2 ==> |
|
134 (LENGTH l1 = LENGTH l2)--), |
|
135 val APPEND_PRS = store_thm |
|
136 ("APPEND_PRS", |
|
137 (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> |
|
138 !l m. APPEND l m = MAP abs (APPEND (MAP rep l) (MAP rep m))--), |
|
139 |
|
140 val APPEND_RSP = store_thm |
|
141 ("APPEND_RSP", |
|
142 (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> |
|
143 !l1 l2 m1 m2. |
|
144 (LIST_REL R) l1 l2 /\ (LIST_REL R) m1 m2 ==> |
|
145 (LIST_REL R) (APPEND l1 m1) (APPEND l2 m2)--), |
|
146 val FLAT_PRS = store_thm |
|
147 ("FLAT_PRS", |
|
148 (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> |
|
149 !l. FLAT l = MAP abs (FLAT (MAP (MAP rep) l))--), |
|
150 |
|
151 val FLAT_RSP = store_thm |
|
152 ("FLAT_RSP", |
|
153 (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> |
|
154 !l1 l2. |
|
155 LIST_REL (LIST_REL R) l1 l2 ==> |
|
156 (LIST_REL R) (FLAT l1) (FLAT l2)--), |
|
157 |
|
158 val REVERSE_PRS = store_thm |
|
159 ("REVERSE_PRS", |
|
160 (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> |
|
161 !l. REVERSE l = MAP abs (REVERSE (MAP rep l))--), |
|
162 |
|
163 val REVERSE_RSP = store_thm |
|
164 ("REVERSE_RSP", |
|
165 (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> |
|
166 !l1 l2. |
|
167 LIST_REL R l1 l2 ==> |
|
168 (LIST_REL R) (REVERSE l1) (REVERSE l2)--), |
|
169 |
|
170 val FILTER_PRS = store_thm |
|
171 ("FILTER_PRS", |
|
172 (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> |
|
173 !P l. FILTER P l = (MAP abs) (FILTER ((abs --> I) P) (MAP rep l)) |
|
174 --), |
|
175 |
|
176 val FILTER_RSP = store_thm |
|
177 ("FILTER_RSP", |
|
178 (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> |
|
179 !P1 P2 l1 l2. |
|
180 (R ===> $=) P1 P2 /\ (LIST_REL R) l1 l2 ==> |
|
181 (LIST_REL R) (FILTER P1 l1) (FILTER P2 l2)--), |
|
182 |
|
183 val NULL_PRS = store_thm |
|
184 ("NULL_PRS", |
|
185 (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> |
|
186 !l. NULL l = NULL (MAP rep l)--), |
|
187 |
|
188 val NULL_RSP = store_thm |
|
189 ("NULL_RSP", |
|
190 (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> |
|
191 !l1 l2. |
|
192 LIST_REL R l1 l2 ==> |
|
193 (NULL l1 = NULL l2)--), |
|
194 |
|
195 val SOME_EL_PRS = store_thm |
|
196 ("SOME_EL_PRS", |
|
197 (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> |
|
198 !l P. SOME_EL P l = SOME_EL ((abs --> I) P) (MAP rep l)--), |
|
199 |
|
200 val SOME_EL_RSP = store_thm |
|
201 ("SOME_EL_RSP", |
|
202 (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> |
|
203 !l1 l2 P1 P2. |
|
204 (R ===> $=) P1 P2 /\ (LIST_REL R) l1 l2 ==> |
|
205 (SOME_EL P1 l1 = SOME_EL P2 l2)--), |
|
206 |
|
207 val ALL_EL_PRS = store_thm |
|
208 ("ALL_EL_PRS", |
|
209 (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> |
|
210 !l P. ALL_EL P l = ALL_EL ((abs --> I) P) (MAP rep l)--), |
|
211 |
|
212 val ALL_EL_RSP = store_thm |
|
213 ("ALL_EL_RSP", |
|
214 (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> |
|
215 !l1 l2 P1 P2. |
|
216 (R ===> $=) P1 P2 /\ (LIST_REL R) l1 l2 ==> |
|
217 (ALL_EL P1 l1 = ALL_EL P2 l2)--), |
|
218 |
|
219 val FOLDL_PRS = store_thm |
|
220 ("FOLDL_PRS", |
|
221 (--!R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==> |
|
222 !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==> |
|
223 !l f e. FOLDL f e l = |
|
224 abs1 (FOLDL ((abs1 --> abs2 --> rep1) f) |
|
225 (rep1 e) |
|
226 (MAP rep2 l))--), |
|
227 |
|
228 val FOLDL_RSP = store_thm |
|
229 ("FOLDL_RSP", |
|
230 (--!R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==> |
|
231 !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==> |
|
232 !l1 l2 f1 f2 e1 e2. |
|
233 (R1 ===> R2 ===> R1) f1 f2 /\ |
|
234 R1 e1 e2 /\ (LIST_REL R2) l1 l2 ==> |
|
235 R1 (FOLDL f1 e1 l1) (FOLDL f2 e2 l2)--), |
|
236 |
|
237 val FOLDR_PRS = store_thm |
|
238 ("FOLDR_PRS", |
|
239 (--!R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==> |
|
240 !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==> |
|
241 !l f e. FOLDR f e l = |
|
242 abs2 (FOLDR ((abs1 --> abs2 --> rep2) f) |
|
243 (rep2 e) |
|
244 (MAP rep1 l))--), |
|
245 |
|
246 val FOLDR_RSP = store_thm |
|
247 ("FOLDR_RSP", |
|
248 (--!R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==> |
|
249 !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==> |
|
250 !l1 l2 f1 f2 e1 e2. |
|
251 (R1 ===> R2 ===> R2) f1 f2 /\ |
|
252 R2 e1 e2 /\ (LIST_REL R1) l1 l2 ==> |
|
253 R2 (FOLDR f1 e1 l1) (FOLDR f2 e2 l2)--), |
|
254 *) |
|
255 |
|