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