202 apply simp |
202 apply simp |
203 done |
203 done |
204 |
204 |
205 lemma "foldl PLUS x [] = x" |
205 lemma "foldl PLUS x [] = x" |
206 apply(lifting ho_tst) |
206 apply(lifting ho_tst) |
207 apply(tactic {* clean_tac @{context} 1 *}) |
|
208 apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] nil_prs[OF Quotient_my_int]) |
207 apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] nil_prs[OF Quotient_my_int]) |
|
208 apply(tactic {* clean_tac @{context} 1 *}) |
209 done |
209 done |
210 |
210 |
211 lemma ho_tst2: "foldl my_plus x (h # t) \<approx> my_plus h (foldl my_plus x t)" |
211 lemma ho_tst2: "foldl my_plus x (h # t) \<approx> my_plus h (foldl my_plus x t)" |
212 sorry |
212 sorry |
213 |
213 |
214 lemma "foldl PLUS x (h # t) = PLUS h (foldl PLUS x t)" |
214 lemma "foldl PLUS x (h # t) = PLUS h (foldl PLUS x t)" |
215 apply(tactic {* procedure_tac @{context} @{thm ho_tst2} 1 *}) |
215 apply(tactic {* procedure_tac @{context} @{thm ho_tst2} 1 *}) |
216 apply(tactic {* regularize_tac @{context} 1 *}) |
216 apply(tactic {* regularize_tac @{context} 1 *}) |
217 apply(tactic {* all_inj_repabs_tac @{context} 1*}) |
217 apply(tactic {* all_inj_repabs_tac @{context} 1*}) |
218 apply(tactic {* clean_tac @{context} 1 *}) |
|
219 apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] cons_prs[OF Quotient_my_int]) |
218 apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] cons_prs[OF Quotient_my_int]) |
|
219 apply(tactic {* clean_tac @{context} 1 *}) |
220 done |
220 done |
221 |
221 |
222 lemma ho_tst3: "foldl f (s::nat \<times> nat) ([]::(nat \<times> nat) list) = s" |
222 lemma ho_tst3: "foldl f (s::nat \<times> nat) ([]::(nat \<times> nat) list) = s" |
223 by simp |
223 by simp |
224 |
224 |
225 lemma "foldl f (x::my_int) ([]::my_int list) = x" |
225 lemma "foldl f (x::my_int) ([]::my_int list) = x" |
226 apply(tactic {* procedure_tac @{context} @{thm ho_tst3} 1 *}) |
226 apply(tactic {* procedure_tac @{context} @{thm ho_tst3} 1 *}) |
227 apply(tactic {* regularize_tac @{context} 1 *}) |
227 apply(tactic {* regularize_tac @{context} 1 *}) |
228 apply(tactic {* all_inj_repabs_tac @{context} 1*}) |
228 apply(tactic {* all_inj_repabs_tac @{context} 1*}) |
229 (* TODO: does not work when this is added *) |
|
230 (* apply(tactic {* lambda_prs_tac @{context} 1 *})*) |
|
231 apply(tactic {* clean_tac @{context} 1 *}) |
|
232 apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] nil_prs[OF Quotient_my_int]) |
229 apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] nil_prs[OF Quotient_my_int]) |
|
230 apply(tactic {* clean_tac @{context} 1 *}) |
233 done |
231 done |
234 |
232 |
235 lemma lam_tst: "(\<lambda>x. (x, x)) y = (y, (y :: nat \<times> nat))" |
233 lemma lam_tst: "(\<lambda>x. (x, x)) y = (y, (y :: nat \<times> nat))" |
236 by simp |
234 by simp |
237 |
235 |
308 lemma "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)" |
306 lemma "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)" |
309 apply(tactic {* procedure_tac @{context} @{thm lam_tst3a} 1 *}) |
307 apply(tactic {* procedure_tac @{context} @{thm lam_tst3a} 1 *}) |
310 apply(rule impI) |
308 apply(rule impI) |
311 apply(rule lam_tst3a_reg) |
309 apply(rule lam_tst3a_reg) |
312 apply(tactic {* all_inj_repabs_tac @{context} 1*}) |
310 apply(tactic {* all_inj_repabs_tac @{context} 1*}) |
|
311 apply(simp only: babs_prs[OF Quotient_my_int Quotient_my_int]) |
313 apply(tactic {* clean_tac @{context} 1 *}) |
312 apply(tactic {* clean_tac @{context} 1 *}) |
314 apply(simp only: babs_prs[OF Quotient_my_int Quotient_my_int]) |
|
315 done |
313 done |
316 |
314 |
317 lemma lam_tst3b: "(\<lambda>(y :: nat \<times> nat \<Rightarrow> nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat \<Rightarrow> nat \<times> nat). x)" |
315 lemma lam_tst3b: "(\<lambda>(y :: nat \<times> nat \<Rightarrow> nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat \<Rightarrow> nat \<times> nat). x)" |
318 by auto |
316 by auto |
319 |
317 |