27 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ x\ xs\ rule{\isacharcolon}\ sep{\isachardot}induct{\isacharparenright}% |
27 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ x\ xs\ rule{\isacharcolon}\ sep{\isachardot}induct{\isacharparenright}% |
28 \begin{isamarkuptxt}% |
28 \begin{isamarkuptxt}% |
29 \noindent |
29 \noindent |
30 The resulting proof state has three subgoals corresponding to the three |
30 The resulting proof state has three subgoals corresponding to the three |
31 clauses for \isa{sep}: |
31 clauses for \isa{sep}: |
32 \begin{isabelle} |
32 \begin{isabelle}% |
33 ~1.~{\isasymAnd}a.~map~f~(sep~(a,~[]))~=~sep~(f~a,~map~f~[])\isanewline |
33 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a{\isachardot}\ map\ f\ {\isacharparenleft}sep\ {\isacharparenleft}a{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sep\ {\isacharparenleft}f\ a{\isacharcomma}\ map\ f\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline |
34 ~2.~{\isasymAnd}a~x.~map~f~(sep~(a,~[x]))~=~sep~(f~a,~map~f~[x])\isanewline |
34 \ {\isadigit{2}}{\isachardot}\ {\isasymAnd}a\ x{\isachardot}\ map\ f\ {\isacharparenleft}sep\ {\isacharparenleft}a{\isacharcomma}\ {\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sep\ {\isacharparenleft}f\ a{\isacharcomma}\ map\ f\ {\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}\isanewline |
35 ~3.~{\isasymAnd}a~x~y~zs.\isanewline |
35 \ {\isadigit{3}}{\isachardot}\ {\isasymAnd}a\ x\ y\ zs{\isachardot}\isanewline |
36 ~~~~~~~map~f~(sep~(a,~y~\#~zs))~=~sep~(f~a,~map~f~(y~\#~zs))~{\isasymLongrightarrow}\isanewline |
36 \ \ \ \ \ \ \ map\ f\ {\isacharparenleft}sep\ {\isacharparenleft}a{\isacharcomma}\ y\ {\isacharhash}\ zs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sep\ {\isacharparenleft}f\ a{\isacharcomma}\ map\ f\ {\isacharparenleft}y\ {\isacharhash}\ zs{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\isanewline |
37 ~~~~~~~map~f~(sep~(a,~x~\#~y~\#~zs))~=~sep~(f~a,~map~f~(x~\#~y~\#~zs))% |
37 \ \ \ \ \ \ \ map\ f\ {\isacharparenleft}sep\ {\isacharparenleft}a{\isacharcomma}\ x\ {\isacharhash}\ y\ {\isacharhash}\ zs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sep\ {\isacharparenleft}f\ a{\isacharcomma}\ map\ f\ {\isacharparenleft}x\ {\isacharhash}\ y\ {\isacharhash}\ zs{\isacharparenright}{\isacharparenright}% |
38 \end{isabelle} |
38 \end{isabelle} |
39 The rest is pure simplification:% |
39 The rest is pure simplification:% |
40 \end{isamarkuptxt}% |
40 \end{isamarkuptxt}% |
41 \isacommand{apply}\ simp{\isacharunderscore}all\isanewline |
41 \isacommand{apply}\ simp{\isacharunderscore}all\isanewline |
42 \isacommand{done}% |
42 \isacommand{done}% |