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 by auto; |
44 by simp_all; |
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 |
56 where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the |
56 where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the |
57 name of a function that takes an $n$-tuple. Usually the subgoal will |
57 name of a function that takes an $n$-tuple. Usually the subgoal will |
58 contain the term $f~x@1~\dots~x@n$ but this need not be the case. The |
58 contain the term $f~x@1~\dots~x@n$ but this need not be the case. The |
59 induction rules do not mention $f$ at all. For example \isa{sep.induct} |
59 induction rules do not mention $f$ at all. For example \isa{sep.induct} |
60 \begin{isabellepar}% |
60 \begin{isabellepar}% |
61 {\isasymlbrakk}~{\isasymAnd}a.~?P~a~[];\isanewline |
61 {\isasymlbrakk}~{\isasymAnd}a.~P~a~[];\isanewline |
62 ~~{\isasymAnd}a~x.~?P~a~[x];\isanewline |
62 ~~{\isasymAnd}a~x.~P~a~[x];\isanewline |
63 ~~{\isasymAnd}a~x~y~zs.~?P~a~(y~\#~zs)~{\isasymLongrightarrow}~?P~a~(x~\#~y~\#~zs){\isasymrbrakk}\isanewline |
63 ~~{\isasymAnd}a~x~y~zs.~P~a~(y~\#~zs)~{\isasymLongrightarrow}~P~a~(x~\#~y~\#~zs){\isasymrbrakk}\isanewline |
64 {\isasymLongrightarrow}~?P~?u~?v% |
64 {\isasymLongrightarrow}~P~u~v% |
65 \end{isabellepar}% |
65 \end{isabellepar}% |
66 merely says that in order to prove a property \isa{?P} of \isa{?u} and |
66 merely says that in order to prove a property \isa{P} of \isa{u} and |
67 \isa{?v} you need to prove it for the three cases where \isa{?v} is the |
67 \isa{v} you need to prove it for the three cases where \isa{v} is the |
68 empty list, the singleton list, and the list with at least two elements |
68 empty list, the singleton list, and the list with at least two elements |
69 (in which case you may assume it holds for the tail of that list). |
69 (in which case you may assume it holds for the tail of that list). |
70 *} |
70 *} |
71 |
71 |
72 (*<*) |
72 (*<*) |