equal
deleted
inserted
replaced
305 |
305 |
306 lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)" |
306 lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)" |
307 by (tactic {* lift_tac @{context} @{thm m2} 1 *}) |
307 by (tactic {* lift_tac @{context} @{thm m2} 1 *}) |
308 |
308 |
309 lemma "INSERT a (INSERT a x) = INSERT a x" |
309 lemma "INSERT a (INSERT a x) = INSERT a x" |
310 apply (tactic {* lift_tac @{context} @{thm list_eq.intros(4)} 1 *}) |
310 apply (tactic {* procedure_tac @{context} @{thm list_eq.intros(4)} 1 *}) |
|
311 apply (regularize) |
|
312 apply (injection) |
|
313 apply (cleaning) |
311 done |
314 done |
312 |
315 |
313 lemma "x = xa \<Longrightarrow> INSERT a x = INSERT a xa" |
316 lemma "x = xa \<Longrightarrow> INSERT a x = INSERT a xa" |
314 apply (tactic {* lift_tac @{context} @{thm list_eq.intros(5)} 1 *}) |
317 apply (tactic {* lift_tac @{context} @{thm list_eq.intros(5)} 1 *}) |
315 done |
318 done |
338 |
341 |
339 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l" |
342 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l" |
340 apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *}) |
343 apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *}) |
341 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *}) |
344 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *}) |
342 apply(tactic {* regularize_tac @{context} 1 *}) |
345 apply(tactic {* regularize_tac @{context} 1 *}) |
343 defer |
346 apply(injection) |
344 apply(tactic {* clean_tac @{context} 1 *}) |
347 apply(tactic {* clean_tac @{context} 1 *}) |
345 apply(tactic {* inj_repabs_tac @{context} 1*})+ |
|
346 done |
348 done |
347 |
349 |
348 lemma list_induct_part: |
350 lemma list_induct_part: |
349 assumes a: "P (x :: 'a list) ([] :: 'c list)" |
351 assumes a: "P (x :: 'a list) ([] :: 'c list)" |
350 assumes b: "\<And>e t. P x t \<Longrightarrow> P x (e # t)" |
352 assumes b: "\<And>e t. P x t \<Longrightarrow> P x (e # t)" |
430 |
432 |
431 lemma ttt2: "(\<lambda>e. ((op @) x ((op #) e []))) = (\<lambda>e. ((op #) e x))" |
433 lemma ttt2: "(\<lambda>e. ((op @) x ((op #) e []))) = (\<lambda>e. ((op #) e x))" |
432 sorry |
434 sorry |
433 |
435 |
434 lemma "(\<lambda>e. (FUNION x (INSERT e EMPTY))) = (\<lambda>e. (INSERT e x))" |
436 lemma "(\<lambda>e. (FUNION x (INSERT e EMPTY))) = (\<lambda>e. (INSERT e x))" |
435 apply (tactic {* procedure_tac @{context} @{thm ttt2} 1 *}) |
437 apply(lifting_setup rule: ttt2) |
436 apply(tactic {* regularize_tac @{context} 1 *}) |
438 apply(regularize) |
437 apply(rule impI) |
439 apply(rule impI) |
438 apply(simp) |
440 apply(simp) |
439 apply(rule allI) |
441 apply(rule allI) |
440 apply(rule list_eq_refl) |
442 apply(rule list_eq_refl) |
441 apply(tactic {* all_inj_repabs_tac @{context} 1*}) |
443 apply(injection) |
442 apply(tactic {* clean_tac @{context} 1 *}) |
444 apply(tactic {* clean_tac @{context} 1 *}) |
443 apply(tactic {* clean_tac @{context} 1 *}) (* TODO: needs lambda_prs twice *) |
445 apply(tactic {* clean_tac @{context} 1 *}) (* TODO: needs lambda_prs twice *) |
444 done |
446 done |
445 |
447 |
446 lemma ttt3: "(\<lambda>x. ((op @) x ((op #) e []))) = (\<lambda>x. ((op #) e x))" |
448 lemma ttt3: "(\<lambda>x. ((op @) x ((op #) e []))) = (\<lambda>x. ((op #) e x))" |