equal
deleted
inserted
replaced
1 \begin{isabelle}% |
1 \begin{isabelle}% |
2 \isanewline |
2 \isanewline |
3 \isacommand{lemma}~{"}(case~xs~of~[]~{\isasymRightarrow}~[]~|~y\#ys~{\isasymRightarrow}~xs)~=~xs{"}\isanewline |
3 \isacommand{lemma}~{"}(case~xs~of~[]~{\isasymRightarrow}~[]~|~y\#ys~{\isasymRightarrow}~xs)~=~xs{"}\isanewline |
4 \isacommand{apply}(case\_tac~xs)% |
4 \isacommand{apply}(case\_tac~xs)% |
5 \begin{isamarkuptxt}% |
5 \begin{isamarkuptxt}% |
|
6 \noindent |
|
7 results in the proof state |
6 \begin{isabellepar}% |
8 \begin{isabellepar}% |
7 ~1.~xs~=~[]~{\isasymLongrightarrow}~(case~xs~of~[]~{\isasymRightarrow}~[]~|~y~\#~ys~{\isasymRightarrow}~xs)~=~xs\isanewline |
9 ~1.~xs~=~[]~{\isasymLongrightarrow}~(case~xs~of~[]~{\isasymRightarrow}~[]~|~y~\#~ys~{\isasymRightarrow}~xs)~=~xs\isanewline |
8 ~2.~{\isasymAnd}a~list.~xs=a\#list~{\isasymLongrightarrow}~(case~xs~of~[]~{\isasymRightarrow}~[]~|~y\#ys~{\isasymRightarrow}~xs)~=~xs% |
10 ~2.~{\isasymAnd}a~list.~xs=a\#list~{\isasymLongrightarrow}~(case~xs~of~[]~{\isasymRightarrow}~[]~|~y\#ys~{\isasymRightarrow}~xs)~=~xs% |
9 \end{isabellepar}%% |
11 \end{isabellepar}% |
|
12 which is solved automatically:% |
10 \end{isamarkuptxt}% |
13 \end{isamarkuptxt}% |
11 \isacommand{apply}(auto)\isacommand{.}\isanewline |
14 \isacommand{apply}(auto)\isacommand{.}\isanewline |
12 \end{isabelle}% |
15 \end{isabelle}% |