equal
deleted
inserted
replaced
1 % |
1 \begin{isabelle}% |
2 \begin{isabellebody}% |
|
3 % |
2 % |
4 \begin{isamarkuptext}% |
3 \begin{isamarkuptext}% |
5 Assuming we have defined our function such that Isabelle could prove |
4 Assuming we have defined our function such that Isabelle could prove |
6 termination and that the recursion equations (or some suitable derived |
5 termination and that the recursion equations (or some suitable derived |
7 equations) are simplification rules, we might like to prove something about |
6 equations) are simplification rules, we might like to prove something about |
61 merely says that in order to prove a property \isa{P} of \isa{u} and |
60 merely says that in order to prove a property \isa{P} of \isa{u} and |
62 \isa{v} you need to prove it for the three cases where \isa{v} is the |
61 \isa{v} you need to prove it for the three cases where \isa{v} is the |
63 empty list, the singleton list, and the list with at least two elements |
62 empty list, the singleton list, and the list with at least two elements |
64 (in which case you may assume it holds for the tail of that list).% |
63 (in which case you may assume it holds for the tail of that list).% |
65 \end{isamarkuptext}% |
64 \end{isamarkuptext}% |
66 \end{isabellebody}% |
65 \end{isabelle}% |
67 %%% Local Variables: |
66 %%% Local Variables: |
68 %%% mode: latex |
67 %%% mode: latex |
69 %%% TeX-master: "root" |
68 %%% TeX-master: "root" |
70 %%% End: |
69 %%% End: |