equal
deleted
inserted
replaced
428 |
428 |
429 lemma ttt2: "(\<lambda>e. ((op @) x ((op #) e []))) = (\<lambda>e. ((op #) e x))" |
429 lemma ttt2: "(\<lambda>e. ((op @) x ((op #) e []))) = (\<lambda>e. ((op #) e x))" |
430 sorry |
430 sorry |
431 |
431 |
432 lemma "(\<lambda>e. (FUNION x (INSERT e EMPTY))) = (\<lambda>e. (INSERT e x))" |
432 lemma "(\<lambda>e. (FUNION x (INSERT e EMPTY))) = (\<lambda>e. (INSERT e x))" |
433 apply (tactic {* procedure_tac @{context} @{thm ttt2} 1 *}) |
433 apply(lifting ttt2) |
434 apply(tactic {* regularize_tac @{context} 1 *}) |
434 apply(regularize) |
435 apply(rule impI) |
435 apply(rule impI) |
436 apply(simp) |
436 apply(simp) |
437 apply(rule allI) |
437 apply(rule allI) |
438 apply(rule list_eq_refl) |
438 apply(rule list_eq_refl) |
439 apply(tactic {* all_inj_repabs_tac @{context} 1*}) |
|
440 apply(tactic {* clean_tac @{context} 1 *}) |
|
441 apply(tactic {* clean_tac @{context} 1 *}) (* TODO: needs lambda_prs twice *) |
|
442 done |
439 done |
443 |
440 |
444 lemma ttt3: "(\<lambda>x. ((op @) x ((op #) e []))) = (\<lambda>x. ((op #) e x))" |
441 lemma ttt3: "(\<lambda>x. ((op @) x ((op #) e []))) = (\<lambda>x. ((op #) e x))" |
445 sorry |
442 sorry |
446 |
443 |