194 lemma ho_tst: "foldl my_plus x [] = x" |
194 lemma ho_tst: "foldl my_plus x [] = x" |
195 apply simp |
195 apply simp |
196 done |
196 done |
197 |
197 |
198 |
198 |
199 lemma foldr_prs: |
199 |
200 assumes a: "Quotient R1 abs1 rep1" |
200 |
201 and b: "Quotient R2 abs2 rep2" |
201 |
202 shows "abs2 (foldr ((abs1 ---> abs2 ---> rep2) f) (map rep1 l) (rep2 e)) = foldr f l e" |
|
203 apply (induct l) |
|
204 apply (simp add: Quotient_ABS_REP[OF b]) |
|
205 apply (simp add: Quotient_ABS_REP[OF a] Quotient_ABS_REP[OF b]) |
|
206 done |
|
207 |
|
208 lemma foldl_prs: |
|
209 assumes a: "Quotient R1 abs1 rep1" |
|
210 and b: "Quotient R2 abs2 rep2" |
|
211 shows "abs1 (foldl ((abs1 ---> abs2 ---> rep1) f) (rep1 e) (map rep2 l)) = foldl f e l" |
|
212 apply (induct l arbitrary:e) |
|
213 apply (simp add: Quotient_ABS_REP[OF a]) |
|
214 apply (simp add: Quotient_ABS_REP[OF a] Quotient_ABS_REP[OF b]) |
|
215 done |
|
216 |
|
217 lemma map_prs: |
|
218 assumes a: "Quotient R1 abs1 rep1" |
|
219 and b: "Quotient R2 abs2 rep2" |
|
220 shows "(map abs2) (map ((abs1 ---> rep2) f) (map rep1 l)) = map f l" |
|
221 apply (induct l) |
|
222 apply (simp) |
|
223 apply (simp add: Quotient_ABS_REP[OF a] Quotient_ABS_REP[OF b]) |
|
224 done |
|
225 |
|
226 |
|
227 (* Removed unneeded assumption: "QUOTIENT R abs1 rep1" *) |
|
228 lemma nil_prs: |
|
229 shows "map abs1 [] = []" |
|
230 by simp |
|
231 |
|
232 lemma cons_prs: |
|
233 assumes a: "Quotient R1 abs1 rep1" |
|
234 shows "(map abs1) ((rep1 h) # (map rep1 t)) = h # t" |
|
235 apply (induct t) |
|
236 by (simp_all add: Quotient_ABS_REP[OF a]) |
|
237 |
|
238 lemma cons_rsp[quotient_rsp]: |
|
239 "(op \<approx> ===> list_rel op \<approx> ===> list_rel op \<approx>) op # op #" |
|
240 by simp |
|
241 |
202 |
242 (* I believe it's true. *) |
203 (* I believe it's true. *) |
243 lemma foldl_rsp[quotient_rsp]: |
204 lemma foldl_rsp[quotient_rsp]: |
244 "((op \<approx> ===> op \<approx> ===> op \<approx>) ===> op \<approx> ===> list_rel op \<approx> ===> op \<approx>) foldl foldl" |
205 "((op \<approx> ===> op \<approx> ===> op \<approx>) ===> op \<approx> ===> list_rel op \<approx> ===> op \<approx>) foldl foldl" |
245 apply (simp only: fun_rel.simps) |
206 apply (simp only: fun_rel.simps) |
253 apply (rule allI) |
214 apply (rule allI) |
254 apply (rule impI) |
215 apply (rule impI) |
255 apply (induct_tac xb yb rule: list_induct2) (* To finish I need to give it: arbitrary:xa ya *) |
216 apply (induct_tac xb yb rule: list_induct2) (* To finish I need to give it: arbitrary:xa ya *) |
256 sorry |
217 sorry |
257 |
218 |
258 lemma nil_listrel_rsp[quotient_rsp]: |
|
259 "(list_rel R) [] []" |
|
260 by simp |
|
261 |
|
262 lemma "foldl PLUS x [] = x" |
219 lemma "foldl PLUS x [] = x" |
263 apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *}) |
220 apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *}) |
264 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
221 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
265 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
222 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
|
223 apply(rule nil_rsp) |
|
224 apply(tactic {* quotient_tac @{context} 1*}) |
266 apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int]) |
225 apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int]) |
267 apply(simp only: nil_prs) |
226 apply(simp only: nil_prs[OF Quotient_my_int]) |
268 apply(tactic {* clean_tac @{context} 1 *}) |
227 apply(tactic {* clean_tac @{context} 1 *}) |
269 done |
228 done |
270 |
229 |
271 lemma ho_tst2: "foldl my_plus x (h # t) \<approx> my_plus h (foldl my_plus x t)" |
230 lemma ho_tst2: "foldl my_plus x (h # t) \<approx> my_plus h (foldl my_plus x t)" |
272 sorry |
231 sorry |
273 |
232 |
274 lemma "foldl PLUS x (h # t) = PLUS h (foldl PLUS x t)" |
233 lemma "foldl PLUS x (h # t) = PLUS h (foldl PLUS x t)" |
275 apply(tactic {* procedure_tac @{context} @{thm ho_tst2} 1 *}) |
234 apply(tactic {* procedure_tac @{context} @{thm ho_tst2} 1 *}) |
276 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
235 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
277 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
236 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
|
237 apply(rule cons_rsp) |
|
238 apply(tactic {* quotient_tac @{context} 1 *}) |
278 apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int]) |
239 apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int]) |
279 apply(simp only: cons_prs[OF Quotient_my_int]) |
240 apply(simp only: cons_prs[OF Quotient_my_int]) |
280 apply(tactic {* clean_tac @{context} 1 *}) |
241 apply(tactic {* clean_tac @{context} 1 *}) |
281 done |
242 done |
282 |
243 |