equal
deleted
inserted
replaced
257 |
257 |
258 lemma nil_listrel_rsp[quot_rsp]: |
258 lemma nil_listrel_rsp[quot_rsp]: |
259 "(LIST_REL R) [] []" |
259 "(LIST_REL R) [] []" |
260 by simp |
260 by simp |
261 |
261 |
|
262 thm LAMBDA_PRS[no_vars] |
|
263 thm all_prs[no_vars] |
|
264 |
|
265 lemma test_all_prs: |
|
266 "\<lbrakk>QUOTIENT R absf repf; f = g\<rbrakk> \<Longrightarrow> Ball (Respects R) ((absf ---> id) f) = All g" |
|
267 apply(drule all_prs) |
|
268 apply(simp) |
|
269 done |
|
270 |
|
271 lemma test: |
|
272 "\<lbrakk>QUOTIENT R1 Abs1 Rep1; QUOTIENT R2 Abs2 Rep2; |
|
273 (\<lambda>x. Rep2 (f (Abs1 x))) = lhs \<rbrakk> \<Longrightarrow> (Rep1 ---> Abs2) lhs = f" |
|
274 apply - |
|
275 thm LAMBDA_PRS |
|
276 apply(drule LAMBDA_PRS) |
|
277 apply(assumption) |
|
278 apply(auto) |
|
279 done |
|
280 |
|
281 |
262 lemma "foldl PLUS x [] = x" |
282 lemma "foldl PLUS x [] = x" |
263 apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *}) |
283 apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *}) |
264 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
284 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
265 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
285 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
266 apply(simp only: foldl_prs[OF QUOTIENT_my_int QUOTIENT_my_int]) |
286 apply(simp only: foldl_prs[OF QUOTIENT_my_int QUOTIENT_my_int]) |
267 apply(simp only: nil_prs) |
287 apply(simp only: nil_prs) |
|
288 apply(rule test_all_prs) |
|
289 apply(tactic {* rtac quot 1 *}) |
268 apply(tactic {* clean_tac @{context} [quot] defs 1 *}) |
290 apply(tactic {* clean_tac @{context} [quot] defs 1 *}) |
269 done |
291 done |
270 |
292 |
271 lemma ho_tst2: "foldl my_plus x (h # t) \<approx> my_plus h (foldl my_plus x t)" |
293 lemma ho_tst2: "foldl my_plus x (h # t) \<approx> my_plus h (foldl my_plus x t)" |
272 sorry |
294 sorry |