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(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 |
207 done |
210 |
208 |
211 lemma ho_tst2: "foldl my_plus x (h # t) \<approx> my_plus h (foldl my_plus x t)" |
209 lemma ho_tst2: "foldl my_plus x (h # t) \<approx> my_plus h (foldl my_plus x t)" |
212 sorry |
210 sorry |
213 |
211 |
214 lemma "foldl PLUS x (h # t) = PLUS h (foldl PLUS x t)" |
212 lemma "foldl PLUS x (h # t) = PLUS h (foldl PLUS x t)" |
215 apply(tactic {* procedure_tac @{context} @{thm ho_tst2} 1 *}) |
213 apply(lifting_setup ho_tst2) |
216 apply(tactic {* regularize_tac @{context} 1 *}) |
214 apply(regularize) |
217 apply(tactic {* all_inj_repabs_tac @{context} 1*}) |
215 apply(injection) |
218 apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] cons_prs[OF Quotient_my_int]) |
216 apply(cleaning) |
219 apply(tactic {* clean_tac @{context} 1 *}) |
|
220 done |
217 done |
221 |
218 |
222 lemma ho_tst3: "foldl f (s::nat \<times> nat) ([]::(nat \<times> nat) list) = s" |
219 lemma ho_tst3: "foldl f (s::nat \<times> nat) ([]::(nat \<times> nat) list) = s" |
223 by simp |
220 by simp |
224 |
221 |
225 lemma "foldl f (x::my_int) ([]::my_int list) = x" |
222 lemma "foldl f (x::my_int) ([]::my_int list) = x" |
226 apply(tactic {* procedure_tac @{context} @{thm ho_tst3} 1 *}) |
223 apply(lifting ho_tst3) |
227 apply(tactic {* regularize_tac @{context} 1 *}) |
|
228 apply(tactic {* all_inj_repabs_tac @{context} 1*}) |
|
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 *}) |
|
231 done |
224 done |
232 |
225 |
233 lemma lam_tst: "(\<lambda>x. (x, x)) y = (y, (y :: nat \<times> nat))" |
226 lemma lam_tst: "(\<lambda>x. (x, x)) y = (y, (y :: nat \<times> nat))" |
234 by simp |
227 by simp |
235 |
228 |
236 (* Don't know how to keep the goal non-contracted... *) |
229 (* Don't know how to keep the goal non-contracted... *) |
237 lemma "(\<lambda>x. (x, x)) (y::my_int) = (y, y)" |
230 lemma "(\<lambda>x. (x, x)) (y::my_int) = (y, y)" |
238 apply(tactic {* procedure_tac @{context} @{thm lam_tst} 1 *}) |
231 apply(lifting lam_tst) |
239 apply(tactic {* regularize_tac @{context} 1 *}) |
|
240 apply(tactic {* all_inj_repabs_tac @{context} 1*}) |
|
241 apply(tactic {* clean_tac @{context} 1 *}) |
|
242 apply(simp add: pair_prs) |
|
243 done |
232 done |
244 |
233 |
245 lemma lam_tst2: "(\<lambda>(y :: nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat). x)" |
234 lemma lam_tst2: "(\<lambda>(y :: nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat). x)" |
246 by simp |
235 by simp |
247 |
236 |
306 lemma "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)" |
295 lemma "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)" |
307 apply(tactic {* procedure_tac @{context} @{thm lam_tst3a} 1 *}) |
296 apply(tactic {* procedure_tac @{context} @{thm lam_tst3a} 1 *}) |
308 apply(rule impI) |
297 apply(rule impI) |
309 apply(rule lam_tst3a_reg) |
298 apply(rule lam_tst3a_reg) |
310 apply(tactic {* all_inj_repabs_tac @{context} 1*}) |
299 apply(tactic {* all_inj_repabs_tac @{context} 1*}) |
311 apply(simp only: babs_prs[OF Quotient_my_int Quotient_my_int]) |
|
312 apply(tactic {* clean_tac @{context} 1 *}) |
300 apply(tactic {* clean_tac @{context} 1 *}) |
313 done |
301 done |
314 |
302 |
315 lemma lam_tst3b: "(\<lambda>(y :: nat \<times> nat \<Rightarrow> nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat \<Rightarrow> nat \<times> nat). x)" |
303 lemma lam_tst3b: "(\<lambda>(y :: nat \<times> nat \<Rightarrow> nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat \<Rightarrow> nat \<times> nat). x)" |
316 by auto |
304 by auto |
317 |
305 |
318 lemma "(\<lambda>(y :: my_int => my_int). y) = (\<lambda>(x :: my_int => my_int). x)" |
306 lemma "(\<lambda>(y :: my_int => my_int). y) = (\<lambda>(x :: my_int => my_int). x)" |
319 apply(tactic {* procedure_tac @{context} @{thm lam_tst3b} 1 *}) |
307 apply(lifting lam_tst3b) |
320 apply(rule impI) |
308 apply(rule impI) |
321 apply (rule babs_rsp[OF fun_quotient[OF Quotient_my_int Quotient_my_int]]) |
309 apply(rule babs_rsp[OF fun_quotient[OF Quotient_my_int Quotient_my_int]]) |
322 apply (simp add: id_rsp) |
310 apply(simp add: id_rsp) |
323 apply(tactic {* all_inj_repabs_tac @{context} 1*}) |
|
324 apply(tactic {* clean_tac @{context} 1 *}) |
|
325 apply(subst babs_prs) |
|
326 apply(tactic {* quotient_tac @{context} 1 *}) |
|
327 apply(tactic {* quotient_tac @{context} 1 *}) |
|
328 apply(subst babs_prs) |
|
329 apply(tactic {* quotient_tac @{context} 1 *}) |
|
330 apply(tactic {* quotient_tac @{context} 1 *}) |
|
331 apply(rule refl) |
|
332 done |
311 done |
333 |
312 |
334 term map |
313 term map |
335 |
314 |
336 lemma lam_tst4: "map (\<lambda>x. my_plus x (0,0)) l = l" |
315 lemma lam_tst4: "map (\<lambda>x. my_plus x (0,0)) l = l" |