equal
deleted
inserted
replaced
39 ~~~~~~~map~f~(sep~(a,~x~\#~y~\#~zs))~=~sep~(f~a,~map~f~(x~\#~y~\#~zs))% |
39 ~~~~~~~map~f~(sep~(a,~x~\#~y~\#~zs))~=~sep~(f~a,~map~f~(x~\#~y~\#~zs))% |
40 \end{isabellepar}% |
40 \end{isabellepar}% |
41 The rest is pure simplification: |
41 The rest is pure simplification: |
42 *} |
42 *} |
43 |
43 |
44 apply auto.; |
44 by auto; |
45 |
45 |
46 text{* |
46 text{* |
47 Try proving the above lemma by structural induction, and you find that you |
47 Try proving the above lemma by structural induction, and you find that you |
48 need an additional case distinction. What is worse, the names of variables |
48 need an additional case distinction. What is worse, the names of variables |
49 are invented by Isabelle and have nothing to do with the names in the |
49 are invented by Isabelle and have nothing to do with the names in the |