equal
deleted
inserted
replaced
29 apply(induct_tac x xs rule: sep.induct); |
29 apply(induct_tac x xs rule: sep.induct); |
30 |
30 |
31 txt{*\noindent |
31 txt{*\noindent |
32 The resulting proof state has three subgoals corresponding to the three |
32 The resulting proof state has three subgoals corresponding to the three |
33 clauses for @{term"sep"}: |
33 clauses for @{term"sep"}: |
34 \begin{isabelle} |
34 @{subgoals[display,indent=0]} |
35 ~1.~{\isasymAnd}a.~map~f~(sep~(a,~[]))~=~sep~(f~a,~map~f~[])\isanewline |
|
36 ~2.~{\isasymAnd}a~x.~map~f~(sep~(a,~[x]))~=~sep~(f~a,~map~f~[x])\isanewline |
|
37 ~3.~{\isasymAnd}a~x~y~zs.\isanewline |
|
38 ~~~~~~~map~f~(sep~(a,~y~\#~zs))~=~sep~(f~a,~map~f~(y~\#~zs))~{\isasymLongrightarrow}\isanewline |
|
39 ~~~~~~~map~f~(sep~(a,~x~\#~y~\#~zs))~=~sep~(f~a,~map~f~(x~\#~y~\#~zs))% |
|
40 \end{isabelle} |
|
41 The rest is pure simplification: |
35 The rest is pure simplification: |
42 *} |
36 *} |
43 |
37 |
44 apply simp_all; |
38 apply simp_all; |
45 done |
39 done |