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