|
1 theory QuotList |
|
2 imports QuotScript |
|
3 begin |
|
4 |
|
5 |
|
6 lemma LIST_map_I: |
|
7 shows "map (\<lambda>x. x) = (\<lambda>x. x)" |
|
8 by simp |
|
9 |
|
10 fun |
|
11 LIST_REL |
|
12 where |
|
13 "LIST_REL R [] [] = True" |
|
14 | "LIST_REL R (x#xs) [] = False" |
|
15 | "LIST_REL R [] (x#xs) = False" |
|
16 | "LIST_REL R (x#xs) (y#ys) = (R x y \<and> LIST_REL R xs ys)" |
|
17 |
|
18 lemma LIST_REL_EQ: |
|
19 shows "LIST_REL (op =) = (op =)" |
|
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_EQUIV: |
|
32 assumes a: "EQUIV R" |
|
33 shows "EQUIV (LIST_REL R)" |
|
34 unfolding EQUIV_def |
|
35 apply(rule allI)+ |
|
36 apply(induct_tac x y rule: list_induct2') |
|
37 apply(simp) |
|
38 apply(simp add: expand_fun_eq) |
|
39 apply(metis LIST_REL.simps(1) LIST_REL.simps(2)) |
|
40 apply(simp add: expand_fun_eq) |
|
41 apply(metis LIST_REL.simps(1) LIST_REL.simps(2)) |
|
42 apply(simp add: expand_fun_eq) |
|
43 apply(rule iffI) |
|
44 apply(rule allI) |
|
45 apply(case_tac x) |
|
46 apply(simp) |
|
47 apply(simp) |
|
48 using a |
|
49 apply(unfold EQUIV_def) |
|
50 apply(auto)[1] |
|
51 apply(metis LIST_REL.simps(4)) |
|
52 done |
|
53 |
|
54 lemma LIST_REL_REL: |
|
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))" |
|
57 apply(induct r s rule: list_induct2') |
|
58 apply(simp_all) |
|
59 using QUOTIENT_REL[OF q] |
|
60 apply(metis) |
|
61 done |
|
62 |
|
63 lemma LIST_QUOTIENT: |
|
64 assumes q: "QUOTIENT R Abs Rep" |
|
65 shows "QUOTIENT (LIST_REL R) (map Abs) (map Rep)" |
|
66 unfolding QUOTIENT_def |
|
67 apply(rule conjI) |
|
68 apply(rule allI) |
|
69 apply(induct_tac a) |
|
70 apply(simp) |
|
71 apply(simp add: QUOTIENT_ABS_REP[OF q]) |
|
72 apply(rule conjI) |
|
73 apply(rule allI) |
|
74 apply(induct_tac a) |
|
75 apply(simp) |
|
76 apply(simp) |
|
77 apply(simp add: QUOTIENT_REP_REFL[OF q]) |
|
78 apply(rule allI)+ |
|
79 apply(rule LIST_REL_REL[OF q]) |
|
80 done |
|
81 |
|
82 lemma CONS_PRS: |
|
83 assumes q: "QUOTIENT R Abs Rep" |
|
84 shows "(h#t) = (map Abs) ((Rep h)#(map Rep t))" |
|
85 by (induct t) (simp_all add: QUOTIENT_ABS_REP[OF q]) |
|
86 |
|
87 lemma CONS_RSP: |
|
88 assumes q: "QUOTIENT R Abs Rep" |
|
89 and a: "R h1 h2" "LIST_REL R t1 t2" |
|
90 shows "LIST_REL R (h1#t1) (h2#t2)" |
|
91 using a by (auto) |
|
92 |
|
93 lemma NIL_PRS: |
|
94 assumes q: "QUOTIENT R Abs Rep" |
|
95 shows "[] = (map Abs [])" |
|
96 by (simp) |
|
97 |
|
98 lemma NIL_RSP: |
|
99 assumes q: "QUOTIENT R Abs Rep" |
|
100 shows "LIST_REL R [] []" |
|
101 by simp |
|
102 |
|
103 lemma MAP_PRS: |
|
104 assumes q1: "QUOTIENT R1 Abs1 Rep1" |
|
105 and q2: "QUOTIENT R2 Abs2 Rep2" |
|
106 shows "map f l = (map Abs2) (map ((Abs1 ---> Rep2) f) (map Rep1 l))" |
|
107 by (induct l) |
|
108 (simp_all add: QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2]) |
|
109 |
|
110 lemma MAP_RSP: |
|
111 assumes q1: "QUOTIENT R1 Abs1 Rep1" |
|
112 and q2: "QUOTIENT R2 Abs2 Rep2" |
|
113 and a: "(R1 ===> R2) f1 f2" |
|
114 and b: "LIST_REL R1 l1 l2" |
|
115 shows "LIST_REL R2 (map f1 l1) (map f2 l2)" |
|
116 using b a |
|
117 by (induct l1 l2 rule: list_induct2') |
|
118 (simp_all) |
|
119 |
|
120 |
|
121 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 |